|
| 1 | +/*******************************************************************\ |
| 2 | +
|
| 3 | +Module: Goto-Analyzer Command Line Option Processing |
| 4 | +
|
| 5 | +Author: Martin Brain, [email protected] |
| 6 | +
|
| 7 | +\*******************************************************************/ |
| 8 | + |
| 9 | +#include "build_analyzer.h" |
| 10 | + |
| 11 | +#include <analyses/ai.h> |
| 12 | +#include <analyses/call_stack_history.h> |
| 13 | +#include <analyses/constant_propagator.h> |
| 14 | +#include <analyses/dependence_graph.h> |
| 15 | +#include <analyses/goto_check.h> |
| 16 | +#include <analyses/interval_domain.h> |
| 17 | +#include <analyses/is_threaded.h> |
| 18 | +#include <analyses/local_control_flow_history.h> |
| 19 | +#include <analyses/local_may_alias.h> |
| 20 | +#include <analyses/variable-sensitivity/three_way_merge_abstract_interpreter.h> |
| 21 | +#include <analyses/variable-sensitivity/variable_sensitivity_configuration.h> |
| 22 | +#include <analyses/variable-sensitivity/variable_sensitivity_dependence_graph.h> |
| 23 | +#include <analyses/variable-sensitivity/variable_sensitivity_domain.h> |
| 24 | +#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h> |
| 25 | + |
| 26 | +#include <goto-programs/goto_model.h> |
| 27 | + |
| 28 | +#include <util/namespace.h> |
| 29 | +#include <util/options.h> |
| 30 | + |
| 31 | +/// Ideally this should be a pure function of options. |
| 32 | +/// However at the moment some domains require the goto_model or parts of it |
| 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 = |
| 40 | + variable_sensitivity_object_factoryt::configured_with(vsd_config); |
| 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< |
| 52 | + ai_history_factory_default_constructort<ahistoricalt>>(); |
| 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< |
| 72 | + ai_domain_factory_default_constructort<constant_propagator_domaint>>(); |
| 73 | + } |
| 74 | + else if(options.get_bool_option("intervals")) |
| 75 | + { |
| 76 | + df = util_make_unique< |
| 77 | + ai_domain_factory_default_constructort<interval_domaint>>(); |
| 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 | +} |
0 commit comments