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/source_location.h>
17 #include <util/simplify_expr.h>
18 
20  const namespacet &_ns,
21  symbol_tablet &_new_symbol_table,
22  symex_targett &_target):
23  goto_symext(_ns, _new_symbol_table, _target),
24  record_coverage(false),
25  max_unwind_is_set(false),
26  symex_coverage(_ns)
27 {
28 }
29 
32  const goto_functionst &goto_functions,
33  statet &state)
34 {
35  const source_locationt &source_location=state.source.pc->source_location;
36 
37  if(!source_location.is_nil() && last_source_location!=source_location)
38  {
39  debug() << "BMC at file " << source_location.get_file()
40  << " line " << source_location.get_line()
41  << " function " << source_location.get_function()
42  << eom;
43 
44  last_source_location=source_location;
45  }
46 
47  const goto_programt::const_targett cur_pc=state.source.pc;
48  const guardt cur_guard=state.guard;
49 
50  if(!state.guard.is_false() &&
51  state.source.pc->is_assume() &&
52  simplify_expr(state.source.pc->guard, ns).is_false())
53  {
54  statistics() << "aborting path on assume(false) at "
55  << state.source.pc->source_location
56  << " thread " << state.source.thread_nr;
57 
58  const irep_idt &c=state.source.pc->source_location.get_comment();
59  if(!c.empty())
60  statistics() << ": " << c;
61 
62  statistics() << eom;
63  }
64 
65  goto_symext::symex_step(goto_functions, state);
66 
67  if(record_coverage &&
68  // avoid an invalid iterator in state.source.pc
69  (!cur_pc->is_end_function() ||
70  cur_pc->function!=goto_functions.entry_point()))
71  {
72  // forward goto will effectively be covered via phi function,
73  // which does not invoke symex_step; as symex_step is called
74  // before merge_gotos, also state.guard will be false (we have
75  // taken an impossible transition); thus we synthesize a
76  // transition from the goto instruction to its target to make
77  // sure the goto is considered covered
78  if(cur_pc->is_goto() &&
79  cur_pc->get_target()!=state.source.pc &&
80  cur_pc->guard.is_true())
81  symex_coverage.covered(cur_pc, cur_pc->get_target());
82  else if(!state.guard.is_false())
83  symex_coverage.covered(cur_pc, state.source.pc);
84  }
85 }
86 
88  const statet::goto_statet &goto_state,
89  statet &state)
90 {
91  const goto_programt::const_targett prev_pc=goto_state.source.pc;
92  const guardt prev_guard=goto_state.guard;
93 
94  goto_symext::merge_goto(goto_state, state);
95 
96  assert(prev_pc->is_goto());
97  if(record_coverage &&
98  // could the branch possibly be taken?
99  !prev_guard.is_false() &&
100  !state.guard.is_false() &&
101  // branches only, no single-successor goto
102  !prev_pc->guard.is_true())
103  symex_coverage.covered(prev_pc, state.source.pc);
104 }
105 
107  const symex_targett::sourcet &source,
108  unsigned unwind)
109 {
110  const irep_idt id=goto_programt::loop_id(source.pc);
111 
112  // We use the most specific limit we have,
113  // and 'infinity' when we have none.
114 
115  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
116 
117  loop_limitst &this_thread_limits=
119 
120  loop_limitst::const_iterator l_it=this_thread_limits.find(id);
121  if(l_it!=this_thread_limits.end())
122  this_loop_limit=l_it->second;
123  else
124  {
125  l_it=loop_limits.find(id);
126  if(l_it!=loop_limits.end())
127  this_loop_limit=l_it->second;
128  else if(max_unwind_is_set)
129  this_loop_limit=max_unwind;
130  }
131 
132  bool abort=unwind>=this_loop_limit;
133 
134  statistics() << (abort?"Not unwinding":"Unwinding")
135  << " loop " << id << " iteration "
136  << unwind;
137 
138  if(this_loop_limit!=std::numeric_limits<unsigned>::max())
139  statistics() << " (" << this_loop_limit << " max)";
140 
141  statistics() << " " << source.pc->source_location
142  << " thread " << source.thread_nr << eom;
143 
144  return abort;
145 }
146 
148  const irep_idt &id,
149  const unsigned thread_nr,
150  unsigned unwind)
151 {
152  // We use the most specific limit we have,
153  // and 'infinity' when we have none.
154 
155  unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
156 
157  loop_limitst &this_thread_limits=
158  thread_loop_limits[thread_nr];
159 
160  loop_limitst::const_iterator l_it=this_thread_limits.find(id);
161  if(l_it!=this_thread_limits.end())
162  this_loop_limit=l_it->second;
163  else
164  {
165  l_it=loop_limits.find(id);
166  if(l_it!=loop_limits.end())
167  this_loop_limit=l_it->second;
168  else if(max_unwind_is_set)
169  this_loop_limit=max_unwind;
170  }
171 
172  bool abort=unwind>this_loop_limit;
173 
174  if(unwind>0 || abort)
175  {
176  const symbolt &symbol=ns.lookup(id);
177 
178  statistics() << (abort?"Not unwinding":"Unwinding")
179  << " recursion "
180  << symbol.display_name()
181  << " iteration " << unwind;
182 
183  if(this_loop_limit!=std::numeric_limits<unsigned>::max())
184  statistics() << " (" << this_loop_limit << " max)";
185 
186  statistics() << eom;
187  }
188 
189  return abort;
190 }
191 
192 void symex_bmct::no_body(const irep_idt &identifier)
193 {
194  if(body_warnings.insert(identifier).second)
195  {
196  warning() <<
197  "**** WARNING: no body for function " << identifier << eom;
198  }
199 }
mstreamt & warning()
Definition: message.h:228
static irep_idt loop_id(const_targett target)
Human-readable loop name.
bool is_nil() const
Definition: irep.h:103
goto_programt::const_targett pc
Definition: symex_target.h:32
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
Definition: symex_goto.cpp:234
exprt simplify_expr(const exprt &src, const namespacet &ns)
bool record_coverage
Definition: symex_bmc.h:64
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
Definition: symex_bmc.cpp:106
const irep_idt & get_function() const
bool is_false() const
Definition: expr.cpp:140
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:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void symex_step(const goto_functionst &goto_functions, statet &state)
execute just one step
Definition: symex_main.cpp:188
instructionst::const_iterator const_targett
const irep_idt & get_line() const
symex_coveraget symex_coverage
Definition: symex_bmc.h:107
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
Definition: symex_bmc.cpp:87
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
thread_loop_limitst thread_loop_limits
Definition: symex_bmc.h:80
mstreamt & statistics()
Definition: message.h:243
loop_limitst loop_limits
Definition: symex_bmc.h:77
bool max_unwind_is_set
Definition: symex_bmc.h:74
const irep_idt & display_name() const
Definition: symbol.h:60
The main class for the forward symbolic simulator.
Definition: goto_symex.h:41
mstreamt & debug()
Definition: message.h:253
const irep_idt & get_file() const
unsigned max_unwind
Definition: symex_bmc.h:73
std::unordered_map< irep_idt, unsigned, irep_id_hash > loop_limitst
Definition: symex_bmc.h:76
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
Definition: symex_bmc.cpp:147
Bounded Model Checking for ANSI-C.
source_locationt last_source_location
Definition: symex_bmc.h:32
std::unordered_set< irep_idt, irep_id_hash > body_warnings
Definition: symex_bmc.h:105
virtual void symex_step(const goto_functionst &goto_functions, statet &state)
show progress
Definition: symex_bmc.cpp:31
symex_bmct(const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)
Definition: symex_bmc.cpp:19
const namespacet & ns
Definition: goto_symex.h:104
bool empty() const
Definition: dstring.h:61
symex_targett::sourcet source
virtual void no_body(const irep_idt &identifier)
Definition: symex_bmc.cpp:192
symex_targett::sourcet source