cprover
symex_bmc.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Bounded Model Checking for ANSI-C
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "symex_bmc.h"
13
14#include <limits>
15
16#include <util/simplify_expr.h>
18
20
23 const symbol_tablet &outer_symbol_table,
25 const optionst &options,
26 path_storaget &path_storage,
27 guard_managert &guard_manager,
28 unwindsett &unwindset)
30 mh,
31 outer_symbol_table,
32 _target,
33 options,
34 path_storage,
35 guard_manager),
36 record_coverage(!options.get_option("symex-coverage-report").empty()),
37 havoc_bodyless_functions(
38 options.get_bool_option("havoc-undefined-functions")),
39 unwindset(unwindset),
40 symex_coverage(ns)
41{
42}
43
46 const get_goto_functiont &get_goto_function,
47 statet &state)
48{
49 const source_locationt &source_location = state.source.pc->source_location();
50
51 if(!source_location.is_nil() && last_source_location != source_location)
52 {
53 log.debug() << "BMC at " << source_location.as_string() << " (depth "
54 << state.depth << ')' << log.eom;
55
56 last_source_location = source_location;
57 }
58
59 const goto_programt::const_targett cur_pc = state.source.pc;
60 const guardt cur_guard = state.guard;
61
62 if(
63 !state.guard.is_false() && state.source.pc->is_assume() &&
64 simplify_expr(state.source.pc->condition(), ns).is_false())
65 {
66 log.statistics() << "aborting path on assume(false) at "
67 << state.source.pc->source_location() << " thread "
68 << state.source.thread_nr;
69
70 const irep_idt &c = state.source.pc->source_location().get_comment();
71 if(!c.empty())
72 log.statistics() << ": " << c;
73
74 log.statistics() << log.eom;
75 }
76
78
79 if(
81 // avoid an invalid iterator in state.source.pc
82 (!cur_pc->is_end_function() ||
84 {
85 // forward goto will effectively be covered via phi function,
86 // which does not invoke symex_step; as symex_step is called
87 // before merge_gotos, also state.guard will be false (we have
88 // taken an impossible transition); thus we synthesize a
89 // transition from the goto instruction to its target to make
90 // sure the goto is considered covered
91 if(
92 cur_pc->is_goto() && cur_pc->get_target() != state.source.pc &&
93 cur_pc->condition().is_true())
94 symex_coverage.covered(cur_pc, cur_pc->get_target());
95 else if(!state.guard.is_false())
96 symex_coverage.covered(cur_pc, state.source.pc);
97 }
98}
99
101 const symex_targett::sourcet &prev_source,
102 goto_statet &&goto_state,
103 statet &state)
104{
105 const goto_programt::const_targett prev_pc = prev_source.pc;
106 const guardt prev_guard = goto_state.guard;
107
108 goto_symext::merge_goto(prev_source, std::move(goto_state), state);
109
110 PRECONDITION(prev_pc->is_goto());
111 if(
113 // could the branch possibly be taken?
114 !prev_guard.is_false() && !state.guard.is_false() &&
115 // branches only, no single-successor goto
116 !prev_pc->condition().is_true())
117 symex_coverage.covered(prev_pc, state.source.pc);
118}
119
121 const symex_targett::sourcet &source,
122 const call_stackt &context,
123 unsigned unwind)
124{
125 const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc);
126
127 tvt abort_unwind_decision;
128 unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
129
130 for(auto handler : loop_unwind_handlers)
131 {
132 abort_unwind_decision =
133 handler(context, source.pc->loop_number, unwind, this_loop_limit);
134 if(abort_unwind_decision.is_known())
135 break;
136 }
137
138 // If no handler gave an opinion, use standard command-line --unwindset
139 // / --unwind options to decide:
140 if(abort_unwind_decision.is_unknown())
141 {
142 auto limit = unwindset.get_limit(id, source.thread_nr);
143
144 if(!limit.has_value())
145 abort_unwind_decision = tvt(false);
146 else
147 abort_unwind_decision = tvt(unwind >= *limit);
148 }
149
150 INVARIANT(
151 abort_unwind_decision.is_known(), "unwind decision should be taken by now");
152 bool abort = abort_unwind_decision.is_true();
153
154 log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
155 << " iteration " << unwind;
156
157 if(this_loop_limit != std::numeric_limits<unsigned>::max())
158 log.statistics() << " (" << this_loop_limit << " max)";
159
160 log.statistics() << " " << source.pc->source_location() << " thread "
161 << source.thread_nr << log.eom;
162
163 return abort;
164}
165
167 const irep_idt &id,
168 unsigned thread_nr,
169 unsigned unwind)
170{
171 tvt abort_unwind_decision;
172 unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
173
174 for(auto handler : recursion_unwind_handlers)
175 {
176 abort_unwind_decision = handler(id, unwind, this_loop_limit);
177 if(abort_unwind_decision.is_known())
178 break;
179 }
180
181 // If no handler gave an opinion, use standard command-line --unwindset
182 // / --unwind options to decide:
183 if(abort_unwind_decision.is_unknown())
184 {
185 auto limit = unwindset.get_limit(id, thread_nr);
186
187 if(!limit.has_value())
188 abort_unwind_decision = tvt(false);
189 else
190 abort_unwind_decision = tvt(unwind > *limit);
191 }
192
193 INVARIANT(
194 abort_unwind_decision.is_known(), "unwind decision should be taken by now");
195 bool abort = abort_unwind_decision.is_true();
196
197 if(unwind > 0 || abort)
198 {
199 const symbolt &symbol = ns.lookup(id);
200
201 log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion "
202 << symbol.display_name() << " iteration " << unwind;
203
204 if(this_loop_limit != std::numeric_limits<unsigned>::max())
205 log.statistics() << " (" << this_loop_limit << " max)";
206
207 log.statistics() << log.eom;
208 }
209
210 return abort;
211}
212
213void symex_bmct::no_body(const irep_idt &identifier)
214{
215 if(body_warnings.insert(identifier).second)
216 {
217 log.warning() << "**** WARNING: no body for function " << identifier;
218
220 {
221 log.warning()
222 << "; assigning non-deterministic values to any pointer arguments";
223 }
224 log.warning() << log.eom;
225 }
226}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:781
instructionst::const_iterator const_targett
Definition: goto_program.h:593
Container for data that varies per program point, e.g.
Definition: goto_state.h:32
guardt guard
Definition: goto_state.h:58
unsigned depth
Distance from entry.
Definition: goto_state.h:35
Central data structure: state.
symex_targett::sourcet source
The main class for the forward symbolic simulator.
Definition: goto_symex.h:35
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
Definition: symex_main.cpp:493
virtual void symex_step(const get_goto_functiont &get_goto_function, statet &state)
Called for each step in the symbolic execution This calls print_symex_step to print symex's current i...
Definition: symex_main.cpp:592
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:243
virtual void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state)
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
Definition: symex_goto.cpp:678
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
Definition: goto_symex.h:82
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:263
bool is_false() const
Definition: guard_expr.h:65
bool is_nil() const
Definition: irep.h:376
mstreamt & debug() const
Definition: message.h:429
mstreamt & statistics() const
Definition: message.h:419
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:38
std::string as_string() const
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
const bool havoc_bodyless_functions
Definition: symex_bmc.h:83
symex_coveraget symex_coverage
Definition: symex_bmc.h:117
bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind) override
Definition: symex_bmc.cpp:166
std::vector< loop_unwind_handlert > loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
Definition: symex_bmc.h:89
unwindsett & unwindset
Definition: symex_bmc.h:85
void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state) override
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
Definition: symex_bmc.cpp:100
source_locationt last_source_location
Definition: symex_bmc.h:36
std::unordered_set< irep_idt > body_warnings
Definition: symex_bmc.h:115
void no_body(const irep_idt &identifier) override
Log a warning that a function has no body.
Definition: symex_bmc.cpp:213
std::vector< recursion_unwind_handlert > recursion_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
Definition: symex_bmc.h:93
symex_bmct(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager, unwindsett &unwindset)
Definition: symex_bmc.cpp:21
void symex_step(const get_goto_functiont &get_goto_function, statet &state) override
show progress
Definition: symex_bmc.cpp:45
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
Definition: symex_bmc.cpp:120
const bool record_coverage
Definition: symex_bmc.h:82
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: threeval.h:20
bool is_known() const
Definition: threeval.h:28
bool is_unknown() const
Definition: threeval.h:27
bool is_true() const
Definition: threeval.h:25
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:183
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
goto_programt::const_targett pc
Definition: symex_target.h:42
Bounded Model Checking for ANSI-C.
Loop unwinding.