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(!options.get_option("symex-coverage-report").empty()),
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(
70  // avoid an invalid iterator in state.source.pc
71  (!cur_pc->is_end_function() ||
73  {
74  // forward goto will effectively be covered via phi function,
75  // which does not invoke symex_step; as symex_step is called
76  // before merge_gotos, also state.guard will be false (we have
77  // taken an impossible transition); thus we synthesize a
78  // transition from the goto instruction to its target to make
79  // sure the goto is considered covered
80  if(cur_pc->is_goto() &&
81  cur_pc->get_target()!=state.source.pc &&
82  cur_pc->guard.is_true())
83  symex_coverage.covered(cur_pc, cur_pc->get_target());
84  else if(!state.guard.is_false())
85  symex_coverage.covered(cur_pc, state.source.pc);
86  }
87 }
88 
90  const statet::goto_statet &goto_state,
91  statet &state)
92 {
93  const goto_programt::const_targett prev_pc=goto_state.source.pc;
94  const guardt prev_guard=goto_state.guard;
95 
96  goto_symext::merge_goto(goto_state, state);
97 
98  PRECONDITION(prev_pc->is_goto());
99  if(record_coverage &&
100  // could the branch possibly be taken?
101  !prev_guard.is_false() &&
102  !state.guard.is_false() &&
103  // branches only, no single-successor goto
104  !prev_pc->guard.is_true())
105  symex_coverage.covered(prev_pc, state.source.pc);
106 }
107 
109  const symex_targett::sourcet &source,
110  const goto_symex_statet::call_stackt &context,
111  unsigned unwind)
112 {
113  const irep_idt id=goto_programt::loop_id(*source.pc);
114 
115  tvt abort_unwind_decision;
116  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
117 
118  for(auto handler : loop_unwind_handlers)
119  {
120  abort_unwind_decision =
121  handler(context, source.pc->loop_number, unwind, this_loop_limit);
122  if(abort_unwind_decision.is_known())
123  break;
124  }
125 
126  // If no handler gave an opinion, use standard command-line --unwindset
127  // / --unwind options to decide:
128  if(abort_unwind_decision.is_unknown())
129  {
130  auto limit=unwindset.get_limit(id, source.thread_nr);
131 
132  if(!limit.has_value())
133  abort_unwind_decision = tvt(false);
134  else
135  abort_unwind_decision = tvt(unwind >= *limit);
136  }
137 
138  INVARIANT(
139  abort_unwind_decision.is_known(), "unwind decision should be taken by now");
140  bool abort = abort_unwind_decision.is_true();
141 
142  log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
143  << " iteration " << unwind;
144 
145  if(this_loop_limit!=std::numeric_limits<unsigned>::max())
146  log.statistics() << " (" << this_loop_limit << " max)";
147 
148  log.statistics() << " " << source.pc->source_location << " thread "
149  << source.thread_nr << log.eom;
150 
151  return abort;
152 }
153 
155  const irep_idt &id,
156  const unsigned thread_nr,
157  unsigned unwind)
158 {
159  tvt abort_unwind_decision;
160  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
161 
162  for(auto handler : recursion_unwind_handlers)
163  {
164  abort_unwind_decision = handler(id, unwind, this_loop_limit);
165  if(abort_unwind_decision.is_known())
166  break;
167  }
168 
169  // If no handler gave an opinion, use standard command-line --unwindset
170  // / --unwind options to decide:
171  if(abort_unwind_decision.is_unknown())
172  {
173  auto limit=unwindset.get_limit(id, thread_nr);
174 
175  if(!limit.has_value())
176  abort_unwind_decision = tvt(false);
177  else
178  abort_unwind_decision = tvt(unwind > *limit);
179  }
180 
181  INVARIANT(
182  abort_unwind_decision.is_known(), "unwind decision should be taken by now");
183  bool abort = abort_unwind_decision.is_true();
184 
185  if(unwind>0 || abort)
186  {
187  const symbolt &symbol=ns.lookup(id);
188 
189  log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " recursion "
190  << symbol.display_name() << " iteration " << unwind;
191 
192  if(this_loop_limit!=std::numeric_limits<unsigned>::max())
193  log.statistics() << " (" << this_loop_limit << " max)";
194 
195  log.statistics() << log.eom;
196  }
197 
198  return abort;
199 }
200 
201 void symex_bmct::no_body(const irep_idt &identifier)
202 {
203  if(body_warnings.insert(identifier).second)
204  {
205  log.warning() << "**** WARNING: no body for function " << identifier
206  << log.eom;
207  }
208 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_target_equation.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
source_locationt::as_string
std::string as_string() const
Definition: source_location.h:27
goto_symext::symex_step
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
Definition: symex_main.cpp:325
goto_symex_statet::guard
guardt guard
Definition: goto_symex_state.h:57
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:89
symex_bmct::unwindset
unwindsett unwindset
Definition: symex_bmc.h:85
optionst
Definition: options.h:22
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:41
path_storaget
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:24
goto_symex_statet
Definition: goto_symex_state.h:34
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:37
symex_bmct::merge_goto
void merge_goto(const statet::goto_statet &goto_state, statet &state) override
Definition: symex_bmc.cpp:89
symex_bmct::record_coverage
const bool record_coverage
Definition: symex_bmc.h:83
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:58
tvt::is_unknown
bool is_unknown() const
Definition: threeval.h:27
messaget::eom
static eomt eom
Definition: message.h:284
symex_bmct::body_warnings
std::unordered_set< irep_idt > body_warnings
Definition: symex_bmc.h:113
simplify_expr
exprt simplify_expr(const exprt &src, const namespacet &ns)
Definition: simplify_expr.cpp:2325
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
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:93
symex_bmct::get_unwind_recursion
bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind) override
Definition: symex_bmc.cpp:154
unwindsett::get_limit
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:64
goto_symext::log
messaget log
Definition: goto_symex.h:219
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
guardt
Definition: guard.h:19
goto_symex_statet::depth
unsigned depth
distance from entry
Definition: goto_symex_state.h:55
goto_symext
The main class for the forward symbolic simulator.
Definition: goto_symex.h:78
symex_coveraget::covered
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
Definition: symex_coverage.h:35
source_location.h
symex_bmct::should_stop_unwind
bool should_stop_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind) override
Definition: symex_bmc.cpp:108
goto_programt::loop_id
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:619
irept::is_nil
bool is_nil() const
Definition: irep.h:172
message_handlert
Definition: message.h:24
symex_bmct::symex_coverage
symex_coveraget symex_coverage
Definition: symex_bmc.h:115
dstringt::empty
bool empty() const
Definition: dstring.h:75
goto_symex_statet::goto_statet::guard
guardt guard
Definition: goto_symex_state.h:117
goto_symex_statet::call_stackt
std::vector< framet > call_stackt
Definition: goto_symex_state.h:201
tvt
Definition: threeval.h:19
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:35
source_locationt
Definition: source_location.h:20
simplify_expr.h
goto_symex_statet::goto_statet
Definition: goto_symex_state.h:111
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:215
symex_targett::sourcet::function
irep_idt function
Definition: symex_target.h:38
goto_symex_statet::goto_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:118
symex_bmct::symex_step
void symex_step(const get_goto_functiont &get_goto_function, statet &state) override
show progress
Definition: symex_bmc.cpp:34
symbolt
Symbol table entry.
Definition: symbol.h:27
goto_symext::get_goto_functiont
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:109
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
goto_symext::merge_goto
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:321
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
messaget::debug
mstreamt & debug() const
Definition: message.h:416
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
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)
Definition: symex_bmc.cpp:21
messaget::warning
mstreamt & warning() const
Definition: message.h:391
symex_bmct::no_body
void no_body(const irep_idt &identifier) override
Definition: symex_bmc.cpp:201
symex_bmct::last_source_location
source_locationt last_source_location
Definition: symex_bmc.h:36
symex_bmc.h
validation_modet::INVARIANT
@ INVARIANT
tvt::is_true
bool is_true() const
Definition: threeval.h:25
messaget::statistics
mstreamt & statistics() const
Definition: message.h:406