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/message.h>
26#include <util/options.h>
27
30std::unique_ptr<ai_baset> build_analyzer(
31 const optionst &options,
32 const goto_modelt &goto_model,
33 const namespacet &ns,
35{
39
40 // These support all of the option categories
41 if(
42 options.get_bool_option("recursive-interprocedural") ||
43 options.get_bool_option("three-way-merge"))
44 {
45 // Build the history factory
46 std::unique_ptr<ai_history_factory_baset> hf = nullptr;
47 if(options.get_bool_option("ahistorical"))
48 {
51 }
52 else if(options.get_bool_option("call-stack"))
53 {
55 options.get_unsigned_int_option("call-stack-recursion-limit"));
56 }
57 else if(options.get_bool_option("local-control-flow-history"))
58 {
60 options.get_bool_option("local-control-flow-history-forward"),
61 options.get_bool_option("local-control-flow-history-backward"),
62 options.get_unsigned_int_option("local-control-flow-history-limit"));
63 }
64
65 // Build the domain factory
66 std::unique_ptr<ai_domain_factory_baset> df = nullptr;
67 if(options.get_bool_option("constants"))
68 {
71 }
72 else if(options.get_bool_option("intervals"))
73 {
76 }
77 else if(options.get_bool_option("vsd"))
78 {
81 }
82 // non-null is not fully supported, despite the historical options
83 // dependency-graph is quite heavily tied to the legacy-ait infrastructure
84 // dependency-graph-vs is very similar to dependency-graph
85
86 // Build the storage object
87 std::unique_ptr<ai_storage_baset> st = nullptr;
88 if(options.get_bool_option("one-domain-per-history"))
89 {
91 }
92 else if(options.get_bool_option("one-domain-per-location"))
93 {
95 }
96
97 // Only try to build the abstract interpreter if all the parts have been
98 // correctly specified and configured
99 if(hf != nullptr && df != nullptr && st != nullptr)
100 {
101 if(options.get_bool_option("recursive-interprocedural"))
102 {
104 std::move(hf), std::move(df), std::move(st), mh);
105 }
106 else if(options.get_bool_option("three-way-merge"))
107 {
108 // Only works with VSD
109 if(options.get_bool_option("vsd"))
110 {
112 std::move(hf), std::move(df), std::move(st), mh);
113 }
114 }
115 }
116 }
117 else if(options.get_bool_option("legacy-ait"))
118 {
119 if(options.get_bool_option("constants"))
120 {
121 // constant_propagator_ait derives from ait<constant_propagator_domaint>
123 goto_model.goto_functions);
124 }
125 else if(options.get_bool_option("dependence-graph"))
126 {
128 }
129 else if(options.get_bool_option("dependence-graph-vs"))
130 {
133 }
134 else if(options.get_bool_option("vsd"))
135 {
139 }
140 else if(options.get_bool_option("intervals"))
141 {
143 }
144#if 0
145 // Not actually implemented, despite the option...
146 else if(options.get_bool_option("non-null"))
147 {
149 }
150#endif
151 }
152 else if(options.get_bool_option("legacy-concurrent"))
153 {
154#if 0
155 // Very few domains can work with this interpreter
156 // as it requires that changes to the domain are
157 // 'non-revertable' and it has merge shared
158 if(options.get_bool_option("dependence-graph"))
159 {
161 }
162#endif
163 }
164
165 // Construction failed due to configuration errors
166 return nullptr;
167}
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
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...