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 
15 
16 #include <limits>
17 
18 #include <util/source_location.h>
19 #include <util/simplify_expr.h>
20 
22  message_handlert &mh,
23  const symbol_tablet &outer_symbol_table,
24  symex_target_equationt &_target,
25  const optionst &options,
26  path_storaget &path_storage)
27  : goto_symext(mh, outer_symbol_table, _target, options, path_storage),
28  record_coverage(false),
29  symex_coverage(ns)
30 {
31 }
32 
35  const get_goto_functiont &get_goto_function,
36  statet &state)
37 {
38  const source_locationt &source_location=state.source.pc->source_location;
39 
40  if(!source_location.is_nil() && last_source_location!=source_location)
41  {
42  log.debug() << "BMC at " << source_location.as_string()
43  << " (depth " << state.depth << ')' << log.eom;
44 
45  last_source_location=source_location;
46  }
47 
48  const goto_programt::const_targett cur_pc=state.source.pc;
49  const guardt cur_guard=state.guard;
50 
51  if(!state.guard.is_false() &&
52  state.source.pc->is_assume() &&
53  simplify_expr(state.source.pc->guard, ns).is_false())
54  {
55  log.statistics() << "aborting path on assume(false) at "
56  << state.source.pc->source_location << " thread "
57  << state.source.thread_nr;
58 
59  const irep_idt &c=state.source.pc->source_location.get_comment();
60  if(!c.empty())
61  log.statistics() << ": " << c;
62 
63  log.statistics() << log.eom;
64  }
65 
66  goto_symext::symex_step(get_goto_function, state);
67 
68  if(record_coverage &&
69  // avoid an invalid iterator in state.source.pc
70  (!cur_pc->is_end_function() ||
71  cur_pc->function!=goto_functionst::entry_point()))
72  {
73  // forward goto will effectively be covered via phi function,
74  // which does not invoke symex_step; as symex_step is called
75  // before merge_gotos, also state.guard will be false (we have
76  // taken an impossible transition); thus we synthesize a
77  // transition from the goto instruction to its target to make
78  // sure the goto is considered covered
79  if(cur_pc->is_goto() &&
80  cur_pc->get_target()!=state.source.pc &&
81  cur_pc->guard.is_true())
82  symex_coverage.covered(cur_pc, cur_pc->get_target());
83  else if(!state.guard.is_false())
84  symex_coverage.covered(cur_pc, state.source.pc);
85  }
86 }
87 
89  const statet::goto_statet &goto_state,
90  statet &state)
91 {
92  const goto_programt::const_targett prev_pc=goto_state.source.pc;
93  const guardt prev_guard=goto_state.guard;
94 
95  goto_symext::merge_goto(goto_state, state);
96 
97  PRECONDITION(prev_pc->is_goto());
98  if(record_coverage &&
99  // could the branch possibly be taken?
100  !prev_guard.is_false() &&
101  !state.guard.is_false() &&
102  // branches only, no single-successor goto
103  !prev_pc->guard.is_true())
104  symex_coverage.covered(prev_pc, state.source.pc);
105 }
106 
108  const symex_targett::sourcet &source,
109  unsigned unwind)
110 {
111  const irep_idt id=goto_programt::loop_id(*source.pc);
112 
113  tvt abort_unwind_decision;
114  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
115 
116  for(auto handler : loop_unwind_handlers)
117  {
118  abort_unwind_decision =
119  handler(
120  source.pc->function,
121  source.pc->loop_number,
122  unwind,
123  this_loop_limit);
124  if(abort_unwind_decision.is_known())
125  break;
126  }
127 
128  // If no handler gave an opinion, use standard command-line --unwindset
129  // / --unwind options to decide:
130  if(abort_unwind_decision.is_unknown())
131  {
132  auto limit=unwindset.get_limit(id, source.thread_nr);
133 
134  if(!limit.has_value())
135  abort_unwind_decision = tvt(false);
136  else
137  abort_unwind_decision = tvt(unwind >= *limit);
138  }
139 
140  INVARIANT(
141  abort_unwind_decision.is_known(), "unwind decision should be taken by now");
142  bool abort = abort_unwind_decision.is_true();
143 
144  log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
145  << " iteration " << unwind;
146 
147  if(this_loop_limit!=std::numeric_limits<unsigned>::max())
148  log.statistics() << " (" << this_loop_limit << " max)";
149 
150  log.statistics() << " " << source.pc->source_location << " thread "
151  << source.thread_nr << log.eom;
152 
153  return abort;
154 }
155 
157  const irep_idt &id,
158  const unsigned thread_nr,
159  unsigned unwind)
160 {
161  tvt abort_unwind_decision;
162  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
163 
164  for(auto handler : recursion_unwind_handlers)
165  {
166  abort_unwind_decision = handler(id, unwind, this_loop_limit);
167  if(abort_unwind_decision.is_known())
168  break;
169  }
170 
171  // If no handler gave an opinion, use standard command-line --unwindset
172  // / --unwind options to decide:
173  if(abort_unwind_decision.is_unknown())
174  {
175  auto limit=unwindset.get_limit(id, thread_nr);
176 
177  if(!limit.has_value())
178  abort_unwind_decision = tvt(false);
179  else
180  abort_unwind_decision = tvt(unwind > *limit);
181  }
182 
183  INVARIANT(
184  abort_unwind_decision.is_known(), "unwind decision should be taken by now");
185  bool abort = abort_unwind_decision.is_true();
186 
187  if(unwind>0 || abort)
188  {
189  const symbolt &symbol=ns.lookup(id);
190 
191  log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion "
192  << symbol.display_name() << " iteration " << unwind;
193 
194  if(this_loop_limit!=std::numeric_limits<unsigned>::max())
195  log.statistics() << " (" << this_loop_limit << " max)";
196 
197  log.statistics() << log.eom;
198  }
199 
200  return abort;
201 }
202 
203 void symex_bmct::no_body(const irep_idt &identifier)
204 {
205  if(body_warnings.insert(identifier).second)
206  {
207  log.warning() << "**** WARNING: no body for function " << identifier
208  << log.eom;
209  }
210 }
bool is_nil() const
Definition: irep.h:102
Generate Equation using Symbolic Execution.
goto_programt::const_targett pc
Definition: symex_target.h:32
exprt simplify_expr(const exprt &src, const namespacet &ns)
std::unordered_set< irep_idt > body_warnings
Definition: symex_bmc.h:117
bool record_coverage
Definition: symex_bmc.h:82
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
Definition: symex_bmc.cpp:107
std::string as_string() const
bool is_false() const
Definition: expr.cpp:131
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
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:343
Definition: guard.h:19
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:84
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
Definition: symex_main.cpp:295
unsigned depth
distance from entry
mstreamt & warning() const
Definition: message.h:307
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:237
bool is_known() const
Definition: threeval.h:28
symex_coveraget symex_coverage
Definition: symex_bmc.h:119
messaget log
Definition: goto_symex.h:241
Definition: threeval.h:19
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:398
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:583
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
Definition: symex_bmc.cpp:88
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:24
bool is_true() const
Definition: threeval.h:25
const irep_idt & display_name() const
Definition: symbol.h:57
The main class for the forward symbolic simulator.
Definition: goto_symex.h:46
static irep_idt entry_point()
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
Definition: symex_bmc.cpp:156
symex_bmct(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)
Definition: symex_bmc.cpp:21
Bounded Model Checking for ANSI-C.
virtual void symex_step(const get_goto_functiont &get_goto_function, statet &state)
show progress
Definition: symex_bmc.cpp:34
mstreamt & debug() const
Definition: message.h:332
source_locationt last_source_location
Definition: symex_bmc.h:36
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:64
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
bool empty() const
Definition: dstring.h:61
symex_targett::sourcet source
mstreamt & statistics() const
Definition: message.h:322
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
bool is_unknown() const
Definition: threeval.h:27
unwindsett unwindset
Definition: symex_bmc.h:84
virtual void no_body(const irep_idt &identifier)
Definition: symex_bmc.cpp:203
symex_targett::sourcet source