CBMC
Loading...
Searching...
No Matches
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 <util/simplify_expr.h>
16
18
20
21#include <limits>
22
25 const symbol_tablet &outer_symbol_table,
27 const optionst &options,
28 path_storaget &path_storage,
29 guard_managert &guard_manager,
30 unwindsett &unwindset)
32 mh,
33 outer_symbol_table,
34 _target,
35 options,
36 path_storage,
37 guard_manager),
38 last_source_location(source_locationt::nil()),
39 record_coverage(!options.get_option("symex-coverage-report").empty()),
40 unwindset(unwindset),
41 symex_coverage(ns)
42{
44 if(init_symbol)
46
48 msg.status() << "Starting Bounded Model Checking" << messaget::eom;
49}
50
53 const get_goto_functiont &get_goto_function,
54 statet &state)
55{
56 const source_locationt &source_location = state.source.pc->source_location();
57
58 if(!source_location.is_nil() && last_source_location != source_location)
59 {
60 log.debug() << "BMC at " << source_location.as_string() << " (depth "
61 << state.depth << ')' << log.eom;
62
63 last_source_location = source_location;
64 }
65
67 const guardt cur_guard = state.guard;
68
69 if(
70 !state.guard.is_false() && state.source.pc->is_assume() &&
71 simplify_expr(state.source.pc->condition(), ns).is_false())
72 {
73 log.statistics() << "aborting path on assume(false) at "
74 << state.source.pc->source_location() << " thread "
75 << state.source.thread_nr;
76
77 const irep_idt &c = state.source.pc->source_location().get_comment();
78 if(!c.empty())
79 log.statistics() << ": " << c;
80
81 log.statistics() << log.eom;
82 }
83
85
86 if(
88 // avoid an invalid iterator in state.source.pc
89 (!cur_pc->is_end_function() ||
91 {
92 // forward goto will effectively be covered via phi function,
93 // which does not invoke symex_step; as symex_step is called
94 // before merge_gotos, also state.guard will be false (we have
95 // taken an impossible transition); thus we synthesize a
96 // transition from the goto instruction to its target to make
97 // sure the goto is considered covered
98 if(
99 cur_pc->is_goto() && cur_pc->get_target() != state.source.pc &&
100 cur_pc->condition().is_true())
101 symex_coverage.covered(cur_pc, cur_pc->get_target());
102 else if(!state.guard.is_false())
104 }
105}
106
110 statet &state)
111{
113 const guardt prev_guard = goto_state.guard;
114
116
117 PRECONDITION(prev_pc->is_goto());
118 if(
120 // could the branch possibly be taken?
121 !prev_guard.is_false() && !state.guard.is_false() &&
122 // branches only, no single-successor goto
123 !prev_pc->condition().is_true())
125}
126
128 const symex_targett::sourcet &source,
129 const call_stackt &context,
130 unsigned unwind)
131{
132 const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc);
133
135 unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
136
137 for(auto handler : loop_unwind_handlers)
138 {
140 handler(context, source.pc->loop_number, unwind, this_loop_limit);
141 if(abort_unwind_decision.is_known())
142 break;
143 }
144
145 // If no handler gave an opinion, use standard command-line --unwindset
146 // / --unwind options to decide:
147 if(abort_unwind_decision.is_unknown())
148 {
149 auto limit = unwindset.get_limit(id, source.thread_nr);
150
151 if(!limit.has_value())
152 abort_unwind_decision = tvt(false);
153 else
154 abort_unwind_decision = tvt(unwind >= *limit);
155 }
156
157 INVARIANT(
158 abort_unwind_decision.is_known(), "unwind decision should be taken by now");
159 bool abort = abort_unwind_decision.is_true();
160
161 log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
162 << " iteration " << unwind;
163
164 if(this_loop_limit != std::numeric_limits<unsigned>::max())
165 log.statistics() << " (" << this_loop_limit << " max)";
166
167 log.statistics() << " " << source.pc->source_location() << " thread "
168 << source.thread_nr << log.eom;
169
170 return abort;
171}
172
174 const irep_idt &id,
175 unsigned thread_nr,
176 unsigned unwind)
177{
179 unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
180
182 {
184 if(abort_unwind_decision.is_known())
185 break;
186 }
187
188 // If no handler gave an opinion, use standard command-line --unwindset
189 // / --unwind options to decide:
190 if(abort_unwind_decision.is_unknown())
191 {
192 auto limit = unwindset.get_limit(id, thread_nr);
193
194 if(!limit.has_value())
195 abort_unwind_decision = tvt(false);
196 else
197 abort_unwind_decision = tvt(unwind > *limit);
198 }
199
200 INVARIANT(
201 abort_unwind_decision.is_known(), "unwind decision should be taken by now");
202 bool abort = abort_unwind_decision.is_true();
203
204 if(unwind > 0 || abort)
205 {
206 const symbolt &symbol = ns.lookup(id);
207
208 log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion "
209 << symbol.display_name() << " iteration " << unwind;
210
211 if(this_loop_limit != std::numeric_limits<unsigned>::max())
212 log.statistics() << " (" << this_loop_limit << " max)";
213
214 log.statistics() << log.eom;
215 }
216
217 return abort;
218}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
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.
instructionst::const_iterator const_targett
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:38
const symbol_table_baset & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition goto_symex.h:247
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Definition goto_symex.h:240
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 ...
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...
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition goto_symex.h:256
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...
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:94
messaget log
The messaget to write log messages to.
Definition goto_symex.h:276
bool is_false() const
Definition guard_expr.h:65
bool is_nil() const
Definition irep.h:368
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & debug() const
Definition message.h:421
mstreamt & statistics() const
Definition message.h:411
static eomt eom
Definition message.h:289
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Storage for symbolic execution paths to be resumed later.
std::string as_string() const
The symbol table.
Symbol table entry.
Definition symbol.h:28
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
symex_coveraget symex_coverage
Definition symex_bmc.h:112
bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind) override
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:88
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...
source_locationt last_source_location
Definition symex_bmc.h:36
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:92
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:23
void symex_step(const get_goto_functiont &get_goto_function, statet &state) override
show progress
Definition symex_bmc.cpp:52
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
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
std::optional< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
static std::unordered_set< irep_idt > init_symbol(const symbolt &sym, code_blockt &code_block, symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define INITIALIZE_FUNCTION
void abort(void)
Definition stdlib.c:128
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.
goto_programt::const_targett pc
Bounded Model Checking for ANSI-C.
Loop unwinding.