cprover
Loading...
Searching...
No Matches
bmc_util.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Bounded Model Checking Utilities
4
5Author: 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
19
21
23#include "properties.h"
24
27class goto_tracet;
30class namespacet;
31class optionst;
32class symex_bmct;
34struct trace_optionst;
36
38 symex_target_equationt &equation,
39 decision_proceduret &decision_procedure,
41
46
49
52 const namespacet &,
54 const decision_proceduret &,
56
58 const goto_tracet &,
59 const namespacet &,
60 const trace_optionst &,
62
63void output_graphml(const goto_tracet &, const namespacet &, const optionst &);
66 const namespacet &,
67 const optionst &);
68
69std::unique_ptr<memory_model_baset>
70get_memory_model(const optionst &options, const namespacet &);
71
72void setup_symex(
73 symex_bmct &,
74 const namespacet &,
75 const optionst &,
77
78void slice(
79 symex_bmct &,
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
149std::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-vcc)" \
178 "(show-goto-symex-steps)" \
179 "(show-points-to-sets)" \
180 "(slice-formula)" \
181 "(unwinding-assertions)" \
182 "(no-unwinding-assertions)" \
183 "(no-pretty-names)" \
184 "(no-self-loops-to-assumptions)" \
185 "(partial-loops)" \
186 "(paths):" \
187 "(show-symex-strategies)" \
188 "(depth):" \
189 "(max-field-sensitivity-array-size):" \
190 "(no-array-field-sensitivity)" \
191 "(graphml-witness):" \
192 "(symex-complexity-limit):" \
193 "(symex-complexity-failed-child-loops-limit):" \
194 "(incremental-loop):" \
195 "(unwind-min):" \
196 "(unwind-max):" \
197 "(ignore-properties-before-unwind-min)" \
198 "(symex-cache-dereferences)" \
199 OPT_UNWINDSET \
200
201#define HELP_BMC \
202 " --paths [strategy] explore paths one at a time\n" \
203 " --show-symex-strategies list strategies for use with --paths\n" \
204 " --show-goto-symex-steps show which steps symex travels, includes\n" \
205 " diagnostic information\n" \
206 " --show-points-to-sets show points-to sets for\n" \
207 " pointer dereference. Requires --json-ui.\n" \
208 " --program-only only show program expression\n" \
209 " --show-byte-ops show all byte extracts and updates\n" \
210 " --depth nr limit search depth\n" \
211 " --max-field-sensitivity-array-size M\n" \
212 " maximum size M of arrays for which field\n" \
213 " sensitivity will be applied to array,\n" \
214 " the default is 64\n" \
215 " --no-array-field-sensitivity\n" \
216 " deactivate field sensitivity for arrays, " \
217 "this is\n" \
218 " equivalent to setting the maximum field \n" \
219 " sensitivity size for arrays to 0\n" \
220 HELP_UNWINDSET \
221 " --incremental-loop L check properties after each unwinding\n" \
222 " of loop L\n" \
223 " (use --show-loops to get the loop IDs)\n" \
224 " --unwind-min nr start incremental-loop after nr unwindings\n" \
225 " but before solving that iteration. If for\n" \
226 " example it is 1, then the loop will be\n" \
227 " unwound once, and immediately checked.\n" \
228 " Note: this means for min-unwind 1 or\n"\
229 " 0 all properties are checked.\n" \
230 " --unwind-max nr stop incremental-loop after nr unwindings\n" \
231 " --ignore-properties-before-unwind-min\n" \
232 " do not check properties before unwind-min\n" \
233 " when using incremental-loop\n" \
234 " --show-vcc show the verification conditions\n" \
235 " --slice-formula remove assignments unrelated to property\n" \
236 " --unwinding-assertions generate unwinding assertions (cannot be\n" \
237 " used with --cover or --partial-loops)\n" \
238 " --partial-loops permit paths with partial loops\n" \
239 " --no-self-loops-to-assumptions\n" \
240 " do not simplify while(1){} to assume(0)\n" \
241 " --no-pretty-names do not simplify identifiers\n" \
242 " --symex-complexity-limit N how complex (N) a path can become before\n" \
243 " symex abandons it. Currently uses guard\n" \
244 " size to calculate complexity. \n" \
245 " --symex-complexity-failed-child-loops-limit N\n" \
246 " how many child branches (N) in an\n" \
247 " iteration are allowed to fail due to\n" \
248 " complexity violations before the loop\n" \
249 " gets blacklisted\n" \
250 " --graphml-witness filename write the witness in GraphML format to filename\n" /* NOLINT(*) */ \
251 " --symex-cache-dereferences enable caching of repeated dereferences" \
252// clang-format on
253
254#endif // CPROVER_GOTO_CHECKER_BMC_UTIL_H
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:199
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:307
void setup_symex(symex_bmct &, const namespacet &, const optionst &, ui_message_handlert &)
Definition bmc_util.cpp:179
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 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:291
void output_graphml(const goto_tracet &, const namespacet &, const optionst &)
outputs an error witness in graphml format
Definition bmc_util.cpp:108
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:239
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:275
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
std::unique_ptr< memory_model_baset > get_memory_model(const optionst &options, const namespacet &)
Definition bmc_util.cpp:163
void convert_symex_target_equation(symex_target_equationt &equation, decision_proceduret &decision_procedure, message_handlert &message_handler)
Definition bmc_util.cpp:151
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:323
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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:175
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:91
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:219
Loop unwinding.