cprover
Loading...
Searching...
No Matches
build_analyzer.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto-Analyzer Command Line Option Processing
4
5Author: Martin Brain, martin.brain@cs.ox.ac.uk
6
7\*******************************************************************/
8
9#include "build_analyzer.h"
10
11#include <analyses/ai.h>
22
24
25#include <util/options.h>
26
29std::unique_ptr<ai_baset> build_analyzer(
30 const optionst &options,
31 const goto_modelt &goto_model,
32 const namespacet &ns,
34{
35 auto vsd_config = vsd_configt::from_options(options);
36 auto vs_object_factory =
38
39 // These support all of the option categories
40 if(
41 options.get_bool_option("recursive-interprocedural") ||
42 options.get_bool_option("three-way-merge"))
43 {
44 // Build the history factory
45 std::unique_ptr<ai_history_factory_baset> hf = nullptr;
46 if(options.get_bool_option("ahistorical"))
47 {
50 }
51 else if(options.get_bool_option("call-stack"))
52 {
54 options.get_unsigned_int_option("call-stack-recursion-limit"));
55 }
56 else if(options.get_bool_option("local-control-flow-history"))
57 {
59 options.get_bool_option("local-control-flow-history-forward"),
60 options.get_bool_option("local-control-flow-history-backward"),
61 options.get_unsigned_int_option("local-control-flow-history-limit"));
62 }
63
64 // Build the domain factory
65 std::unique_ptr<ai_domain_factory_baset> df = nullptr;
66 if(options.get_bool_option("constants"))
67 {
70 }
71 else if(options.get_bool_option("intervals"))
72 {
75 }
76 else if(options.get_bool_option("vsd"))
77 {
79 vs_object_factory, vsd_config);
80 }
81 // non-null is not fully supported, despite the historical options
82 // dependency-graph is quite heavily tied to the legacy-ait infrastructure
83 // dependency-graph-vs is very similar to dependency-graph
84
85 // Build the storage object
86 std::unique_ptr<ai_storage_baset> st = nullptr;
87 if(options.get_bool_option("one-domain-per-history"))
88 {
90 }
91 else if(options.get_bool_option("one-domain-per-location"))
92 {
94 }
95
96 // Only try to build the abstract interpreter if all the parts have been
97 // correctly specified and configured
98 if(hf != nullptr && df != nullptr && st != nullptr)
99 {
100 if(options.get_bool_option("recursive-interprocedural"))
101 {
103 std::move(hf), std::move(df), std::move(st), mh);
104 }
105 else if(options.get_bool_option("three-way-merge"))
106 {
107 // Only works with VSD
108 if(options.get_bool_option("vsd"))
109 {
111 std::move(hf), std::move(df), std::move(st), mh);
112 }
113 }
114 }
115 }
116 else if(options.get_bool_option("legacy-ait"))
117 {
118 if(options.get_bool_option("constants"))
119 {
120 // constant_propagator_ait derives from ait<constant_propagator_domaint>
122 goto_model.goto_functions);
123 }
124 else if(options.get_bool_option("dependence-graph"))
125 {
127 }
128 else if(options.get_bool_option("dependence-graph-vs"))
129 {
131 goto_model.goto_functions, ns, vs_object_factory, vsd_config, mh);
132 }
133 else if(options.get_bool_option("vsd"))
134 {
136 vs_object_factory, vsd_config);
138 }
139 else if(options.get_bool_option("intervals"))
140 {
142 }
143#if 0
144 // Not actually implemented, despite the option...
145 else if(options.get_bool_option("non-null"))
146 {
148 }
149#endif
150 }
151 else if(options.get_bool_option("legacy-concurrent"))
152 {
153#if 0
154 // Very few domains can work with this interpreter
155 // as it requires that changes to the domain are
156 // 'non-revertable' and it has merge shared
157 if(options.get_bool_option("dependence-graph"))
158 {
160 }
161#endif
162 }
163
164 // Construction failed due to configuration errors
165 return nullptr;
166}
Abstract Interpretation.
std::unique_ptr< ai_baset > build_analyzer(const optionst &options, const goto_modelt &goto_model, const namespacet &ns, message_handlert &mh)
Ideally this should be a pure function of options.
History for tracking the call stack and performing interprocedural analysis.
An easy factory implementation for histories that don't need parameters.
Definition ai_history.h:255
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
unsigned int get_unsigned_int_option(const std::string &option) const
Definition options.cpp:56
bool get_bool_option(const std::string &option) const
Definition options.cpp:44
static variable_sensitivity_object_factory_ptrt configured_with(const vsd_configt &options)
Constant propagation.
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
Symbol Table + CFG.
Interval Domain.
Track function-local control flow for loop unwinding and path senstivity.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
Options.
static vsd_configt from_options(const optionst &options)
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
Captures the user-supplied configuration for VSD, determining which domain abstractions are used,...
A forked and modified version of analyses/dependence_graph.
There are different ways of handling arrays, structures, unions and pointers.
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...