CBMC
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 
17 
19 #include "properties.h"
20 
21 #include <chrono> // IWYU pragma: keep
22 #include <memory>
23 
26 class goto_tracet;
27 class memory_model_baset;
28 class message_handlert;
29 class namespacet;
30 class optionst;
31 class symex_bmct;
33 struct trace_optionst;
35 
37  symex_target_equationt &equation,
38  decision_proceduret &decision_procedure,
40 
45 
48 
50  goto_tracet &,
51  const namespacet &,
52  const symex_target_equationt &,
53  const decision_proceduret &,
55 
57  const goto_tracet &,
58  const namespacet &,
59  const trace_optionst &,
61 
62 void output_graphml(const goto_tracet &, const namespacet &, const optionst &);
63 void output_graphml(
64  const symex_target_equationt &,
65  const namespacet &,
66  const optionst &);
67 
68 std::unique_ptr<memory_model_baset>
69 get_memory_model(const optionst &options, const namespacet &);
70 
71 void setup_symex(
72  symex_bmct &,
73  const namespacet &,
74  const optionst &,
76 
77 void slice(
78  symex_bmct &,
79  symex_target_equationt &symex_target_equation,
80  const namespacet &,
81  const optionst &,
83 
89  symex_bmct &symex,
90  symex_target_equationt &equation,
91  const optionst &options,
92  const namespacet &ns,
93  ui_message_handlert &ui_message_handler);
94 
103  const std::string &cov_out,
104  const abstract_goto_modelt &goto_model,
105  const symex_bmct &symex,
106  ui_message_handlert &ui_message_handler);
107 
115  propertiest &properties,
116  std::unordered_set<irep_idt> &updated_properties,
117  const symex_target_equationt &equation);
118 
126  propertiest &properties,
127  std::unordered_set<irep_idt> &updated_properties);
128 
136  propertiest &properties,
137  std::unordered_set<irep_idt> &updated_properties);
138 
148 std::chrono::duration<double> prepare_property_decider(
149  propertiest &properties,
150  symex_target_equationt &equation,
151  goto_symex_property_decidert &property_decider,
152  ui_message_handlert &ui_message_handler);
153 
166  propertiest &properties,
167  goto_symex_property_decidert &property_decider,
168  ui_message_handlert &ui_message_handler,
169  std::chrono::duration<double> solver_runtime,
170  bool set_pass = true);
171 
172 #define OPT_BMC \
173  "(program-only)" \
174  "(show-byte-ops)" \
175  "(show-vcc)" \
176  "(show-goto-symex-steps)" \
177  "(show-points-to-sets)" \
178  "(slice-formula)" \
179  "(unwinding-assertions)" \
180  "(no-unwinding-assertions)" \
181  "(no-self-loops-to-assumptions)" \
182  "(partial-loops)" \
183  "(paths):" \
184  "(show-symex-strategies)" \
185  "(depth):" \
186  "(max-field-sensitivity-array-size):" \
187  "(no-array-field-sensitivity)" \
188  "(graphml-witness):" \
189  "(symex-complexity-limit):" \
190  "(symex-complexity-failed-child-loops-limit):" \
191  "(incremental-loop):" \
192  "(unwind-min):" \
193  "(unwind-max):" \
194  "(ignore-properties-before-unwind-min)" \
195  "(symex-cache-dereferences)" OPT_UNWINDSET
196 
197 #define HELP_BMC \
198  " {y--paths} [strategy] \t explore paths one at a time\n" \
199  " {y--show-symex-strategies} \t list strategies for use with {y--paths}\n" \
200  " {y--show-goto-symex-steps} \t show which steps symex travels, includes " \
201  "diagnostic information\n" \
202  " {y--show-points-to-sets} \t show points-to sets for pointer dereference. " \
203  "Requires {y--json-ui}.\n" \
204  " {y--program-only} \t only show program expression\n" \
205  " {y--show-byte-ops} \t show all byte extracts and updates\n" \
206  " {y--depth} {unr} \t limit search depth\n" \
207  " {y--max-field-sensitivity-array-size} {uM} \t " \
208  "maximum size {uM} of arrays for which field sensitivity will be " \
209  "applied to array, the default is 64\n" \
210  " {y--no-array-field-sensitivity} \t " \
211  "deactivate field sensitivity for arrays, this is equivalent to setting " \
212  "the maximum field sensitivity size for arrays to 0\n" HELP_UNWINDSET \
213  " {y--incremental-loop} {uL} \t " \
214  "check properties after each unwinding of loop {uL} (use {y--show-loops} " \
215  "to get the loop IDs)\n" \
216  " {y--unwind-min} {unr} \t " \
217  "start incremental-loop after {unr} unwindings but before solving that " \
218  "iteration. If for example it is 1, then the loop will be unwound once, " \
219  "and immediately checked. Note: this means for {y--unwind-min} 1 or 0 all " \
220  "properties are checked.\n" \
221  " {y--unwind-max} {unr} \t stop incremental-loop after {unr} unwindings\n" \
222  " {y--ignore-properties-before-unwind-min} \t " \
223  "do not check properties before unwind-min when using " \
224  "{y--incremental-loop}\n" \
225  " {y--show-vcc} \t show the verification conditions\n" \
226  " {y--slice-formula} \t remove assignments unrelated to property\n" \
227  " {y--unwinding-assertions} \t generate unwinding assertions (cannot be " \
228  "used with {y--cover})\n" \
229  " {y--partial-loops} \t permit paths with partial loops\n" \
230  " {y--no-self-loops-to-assumptions} \t do not simplify while(1){ {}} to " \
231  "assume(0)\n" \
232  " {y--symex-complexity-limit} {uN} \t " \
233  "how complex ({uN}) a path can become before symex abandons it. Currently " \
234  "uses guard size to calculate complexity.\n" \
235  " {y--symex-complexity-failed-child-loops-limit} {uN} \t " \
236  "how many child branches ({uN}) in an iteration are allowed to fail due to " \
237  "complexity violations before the loop gets blacklisted\n" \
238  " {y--graphml-witness} {ufilename} \t write the witness in GraphML format " \
239  "to {ufilename}\n" \
240  " {y--symex-cache-dereferences} \t enable caching of repeated " \
241  "dereferences\n"
242 
243 #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:358
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:382
void slice(symex_bmct &, symex_target_equationt &symex_target_equation, const namespacet &, const optionst &, ui_message_handlert &)
Definition: bmc_util.cpp:198
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:306
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:290
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:238
void output_error_trace(const goto_tracet &, const namespacet &, const trace_optionst &, ui_message_handlert &)
Definition: bmc_util.cpp:64
void message_building_error_trace(messaget &)
Outputs a message that an error trace is being built.
Definition: bmc_util.cpp:35
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:274
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:54
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:322
void build_error_trace(goto_tracet &, const namespacet &, const symex_target_equationt &, const decision_proceduret &, ui_message_handlert &)
Definition: bmc_util.cpp:40
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.
An interface for a decision procedure for satisfiability problems.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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:49
Incremental Goto Checker Interface.
Properties.
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:221
Loop unwinding.