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