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