cprover
bmc_util.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bounded Model Checking Utilities
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H
13 #define CPROVER_GOTO_CHECKER_BMC_UTIL_H
14 
15 #include <chrono>
16 #include <memory>
17 
21 
23 #include "properties.h"
24 
27 class goto_tracet;
28 class memory_model_baset;
29 class message_handlert;
30 class namespacet;
31 class optionst;
32 class symex_bmct;
34 struct trace_optionst;
36 
38  symex_target_equationt &equation,
39  decision_proceduret &decision_procedure,
41 
46 
49 
51  goto_tracet &,
52  const namespacet &,
53  const symex_target_equationt &,
54  const decision_proceduret &,
56 
58  const goto_tracet &,
59  const namespacet &,
60  const trace_optionst &,
62 
63 void output_graphml(const goto_tracet &, const namespacet &, const optionst &);
64 void output_graphml(
65  const symex_target_equationt &,
66  const namespacet &,
67  const optionst &);
68 
69 std::unique_ptr<memory_model_baset>
70 get_memory_model(const optionst &options, const namespacet &);
71 
72 void setup_symex(
73  symex_bmct &,
74  const namespacet &,
75  const optionst &,
77 
78 void slice(
79  symex_bmct &,
80  symex_target_equationt &symex_target_equation,
81  const namespacet &,
82  const optionst &,
84 
90  symex_bmct &symex,
91  symex_target_equationt &equation,
92  const optionst &options,
93  const namespacet &ns,
94  ui_message_handlert &ui_message_handler);
95 
104  const std::string &cov_out,
105  const abstract_goto_modelt &goto_model,
106  const symex_bmct &symex,
107  ui_message_handlert &ui_message_handler);
108 
116  propertiest &properties,
117  std::unordered_set<irep_idt> &updated_properties,
118  const symex_target_equationt &equation);
119 
127  propertiest &properties,
128  std::unordered_set<irep_idt> &updated_properties);
129 
137  propertiest &properties,
138  std::unordered_set<irep_idt> &updated_properties);
139 
149 std::chrono::duration<double> prepare_property_decider(
150  propertiest &properties,
151  symex_target_equationt &equation,
152  goto_symex_property_decidert &property_decider,
153  ui_message_handlert &ui_message_handler);
154 
167  propertiest &properties,
168  goto_symex_property_decidert &property_decider,
169  ui_message_handlert &ui_message_handler,
170  std::chrono::duration<double> solver_runtime,
171  bool set_pass = true);
172 
173 // clang-format off
174 #define OPT_BMC \
175  "(program-only)" \
176  "(show-byte-ops)" \
177  "(show-loops)" \
178  "(show-vcc)" \
179  "(show-goto-symex-steps)" \
180  "(show-points-to-sets)" \
181  "(slice-formula)" \
182  "(unwinding-assertions)" \
183  "(no-unwinding-assertions)" \
184  "(no-pretty-names)" \
185  "(no-self-loops-to-assumptions)" \
186  "(partial-loops)" \
187  "(paths):" \
188  "(show-symex-strategies)" \
189  "(depth):" \
190  "(unwind):" \
191  "(max-field-sensitivity-array-size):" \
192  "(no-array-field-sensitivity)" \
193  "(graphml-witness):" \
194  "(unwindset):" \
195  "(symex-complexity-limit):" \
196  "(symex-complexity-failed-child-loops-limit):" \
197  "(incremental-loop):" \
198  "(unwind-min):" \
199  "(unwind-max):" \
200  "(ignore-properties-before-unwind-min)"
201 
202 #define HELP_BMC \
203  " --paths [strategy] explore paths one at a time\n" \
204  " --show-symex-strategies list strategies for use with --paths\n" \
205  " --show-goto-symex-steps show which steps symex travels, includes\n" \
206  " diagnostic information\n" \
207  " --show-points-to-sets show points-to sets for\n" \
208  " pointer dereference. Requires --json-ui.\n" \
209  " --program-only only show program expression\n" \
210  " --show-byte-ops show all byte extracts and updates\n" \
211  " --show-loops show the loops in the program\n" \
212  " --depth nr limit search depth\n" \
213  " --max-field-sensitivity-array-size M\n" \
214  " maximum size M of arrays for which field\n" \
215  " sensitivity will be applied to array,\n" \
216  " the default is 64\n" \
217  " --no-array-field-sensitivity\n" \
218  " deactivate field sensitivity for arrays, " \
219  "this is\n" \
220  " equivalent to setting the maximum field \n" \
221  " sensitivity size for arrays to 0\n" \
222  " --unwind nr unwind nr times\n" \
223  " --unwindset L:B,... unwind loop L with a bound of B\n" \
224  " (use --show-loops to get the loop IDs)\n" \
225  " --incremental-loop L check properties after each unwinding\n" \
226  " of loop L\n" \
227  " (use --show-loops to get the loop IDs)\n" \
228  " --unwind-min nr start incremental-loop after nr unwindings\n" \
229  " but before solving that iteration. If for\n" \
230  " example it is 1, then the loop will be\n" \
231  " unwound once, and immediately checked.\n" \
232  " Note: this means for min-unwind 1 or\n"\
233  " 0 all properties are checked.\n" \
234  " --unwind-max nr stop incremental-loop after nr unwindings\n" \
235  " --ignore-properties-before-unwind-min\n" \
236  " do not check properties before unwind-min\n" \
237  " when using incremental-loop\n" \
238  " --show-vcc show the verification conditions\n" \
239  " --slice-formula remove assignments unrelated to property\n" \
240  " --unwinding-assertions generate unwinding assertions (cannot be\n" \
241  " used with --cover or --partial-loops)\n" \
242  " --partial-loops permit paths with partial loops\n" \
243  " --no-self-loops-to-assumptions\n" \
244  " do not simplify while(1){} to assume(0)\n" \
245  " --no-pretty-names do not simplify identifiers\n" \
246  " --symex-complexity-limit N how complex (N) a path can become before\n" \
247  " symex abandons it. Currently uses guard\n" \
248  " size to calculate complexity. \n" \
249  " --symex-complexity-failed-child-loops-limit N\n" \
250  " how many child branches (N) in an\n" \
251  " iteration are allowed to fail due to\n" \
252  " complexity violations before the loop\n" \
253  " gets blacklisted\n" \
254  " --graphml-witness filename write the witness in GraphML format to filename\n" // NOLINT(*)
255 // clang-format on
256 
257 #endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H
std::chrono::duration< double > prepare_property_decider(propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider, ui_message_handlert &ui_message_handler)
Converts the equation and sets up the property decider, but does not call solve.
Definition: bmc_util.cpp:356
void run_property_decider(incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, ui_message_handlert &ui_message_handler, std::chrono::duration< double > solver_runtime, bool set_pass=true)
Runs the property decider to solve the equation.
Definition: bmc_util.cpp:380
void slice(symex_bmct &, symex_target_equationt &symex_target_equation, const namespacet &, const optionst &, ui_message_handlert &)
Definition: bmc_util.cpp:197
void output_coverage_report(const std::string &cov_out, const abstract_goto_modelt &goto_model, const symex_bmct &symex, ui_message_handlert &ui_message_handler)
Output a coverage report as generated by symex_coveraget if cov_out is non-empty.
Definition: bmc_util.cpp:305
void setup_symex(symex_bmct &, const namespacet &, const optionst &, ui_message_handlert &)
Definition: bmc_util.cpp:178
std::unique_ptr< memory_model_baset > get_memory_model(const optionst &options, const namespacet &)
Definition: bmc_util.cpp:162
void update_status_of_unknown_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of UNKNOWN properties to PASS.
Definition: bmc_util.cpp:289
void output_graphml(const goto_tracet &, const namespacet &, const optionst &)
outputs an error witness in graphml format
Definition: bmc_util.cpp:107
void update_properties_status_from_symex_target_equation(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation)
Sets property status to PASS for properties whose conditions are constant true in the equation.
Definition: bmc_util.cpp:237
void output_error_trace(const goto_tracet &, const namespacet &, const trace_optionst &, ui_message_handlert &)
Definition: bmc_util.cpp:65
void message_building_error_trace(messaget &)
Outputs a message that an error trace is being built.
Definition: bmc_util.cpp:36
void update_status_of_not_checked_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of NOT_CHECKED properties to PASS.
Definition: bmc_util.cpp:273
ssa_step_predicatet ssa_step_matches_failing_property(const irep_idt &property_id)
Returns a function that checks whether an SSA step is an assertion with property_id.
Definition: bmc_util.cpp:55
void convert_symex_target_equation(symex_target_equationt &equation, decision_proceduret &decision_procedure, message_handlert &message_handler)
Definition: bmc_util.cpp:150
void postprocess_equation(symex_bmct &symex, symex_target_equationt &equation, const optionst &options, const namespacet &ns, ui_message_handlert &ui_message_handler)
Post process the equation.
Definition: bmc_util.cpp:321
void build_error_trace(goto_tracet &, const namespacet &, const symex_target_equationt &, const decision_proceduret &, ui_message_handlert &)
Definition: bmc_util.cpp:41
Traces of GOTO Programs.
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> ssa_step_predicatet
Abstract interface to eager or lazy GOTO models.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Provides management of goal variables that encode properties.
Trace of a GOTO program.
Definition: goto_trace.h:177
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
message_handlert * message_handler
Definition: ui_message.h:47
Incremental Goto Checker Interface.
Storage of symbolic execution paths to resume.
Properties.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
Safety Checker Interface.
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:221