cprover
symex_bmc_incremental_one_loop.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Incremental Bounded Model Checking for ANSI-C
4 
5 Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include <limits>
10 
12 
13 #include <util/structured_data.h>
14 
16  message_handlert &message_handler,
17  const symbol_tablet &outer_symbol_table,
18  symex_target_equationt &target,
19  const optionst &options,
20  path_storaget &path_storage,
21  guard_managert &guard_manager,
22  ui_message_handlert::uit output_ui)
23  : symex_bmct(
24  message_handler,
25  outer_symbol_table,
26  target,
27  options,
28  path_storage,
29  guard_manager),
30  incr_loop_id(options.get_option("incremental-loop")),
31  incr_max_unwind(
32  options.is_set("unwind-max") ? options.get_signed_int_option("unwind-max")
33  : std::numeric_limits<unsigned>::max()),
34  incr_min_unwind(
35  options.is_set("unwind-min") ? options.get_signed_int_option("unwind-min")
36  : 0),
37  output_ui(output_ui)
38 {
39  // the intended behaviour is to stop asserts that are violated before the
40  // unwind
41  // therefore if the min-unwind is 1, then we do one unwind and immediately
42  // start checking for properties
44  incr_min_unwind > 1 &&
45  options.get_bool_option("ignore-properties-before-unwind-min");
46 }
47 
49  const symex_targett::sourcet &source,
50  const call_stackt &context,
51  unsigned unwind)
52 {
53  const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc);
54 
55  tvt abort_unwind_decision;
56  unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
57 
58  // use the incremental limits if it is the specified incremental loop
59  if(id == incr_loop_id)
60  {
61  this_loop_limit = incr_max_unwind;
62  if(unwind + 1 >= incr_min_unwind)
63  ignore_assertions = false;
64 
65  abort_unwind_decision = tvt(unwind >= this_loop_limit);
66  }
67  else
68  {
69  for(auto handler : loop_unwind_handlers)
70  {
71  abort_unwind_decision =
72  handler(context, source.pc->loop_number, unwind, this_loop_limit);
73  if(abort_unwind_decision.is_known())
74  break;
75  }
76 
77  // If no handler gave an opinion, use standard command-line --unwindset
78  // / --unwind options to decide:
79  if(abort_unwind_decision.is_unknown())
80  {
81  auto limit = unwindset.get_limit(id, source.thread_nr);
82 
83  if(!limit.has_value())
84  abort_unwind_decision = tvt(false);
85  else
86  abort_unwind_decision = tvt(unwind >= *limit);
87  }
88  }
89 
90  INVARIANT(
91  abort_unwind_decision.is_known(), "unwind decision should be taken by now");
92  bool abort = abort_unwind_decision.is_true();
93 
94  log_unwinding(unwind);
95  log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
96  << " iteration " << unwind;
97 
98  if(this_loop_limit != std::numeric_limits<unsigned>::max())
99  log.statistics() << " (" << this_loop_limit << " max)";
100 
101  log.statistics() << " " << source.pc->source_location << " thread "
102  << source.thread_nr << log.eom;
103 
104  return abort;
105 }
106 
111  const irep_idt &loop_id,
112  unsigned unwind)
113 {
114  if(unwind < incr_min_unwind)
115  return false;
116 
117  // loop specified by incremental-loop
118  return (loop_id == incr_loop_id);
119 }
120 
122  const get_goto_functiont &get_goto_function,
123  symbol_tablet &new_symbol_table)
124 {
126 
127  symex_with_state(*state, get_goto_function, new_symbol_table);
128 
129  return should_pause_symex;
130 }
131 
133  const get_goto_functiont &get_goto_function)
134 {
135  should_pause_symex = false;
136 
137  symex_with_state(*state, get_goto_function, state->symbol_table);
138 
139  return should_pause_symex;
140 }
142 {
143  structured_datat data{{{labelt({"current", "unwinding"}),
145  json_numbert{std::to_string(unwind)})}}};
146  log.statistics() << data;
147 }
goto_symext::symex_with_state
virtual void symex_with_state(statet &state, const get_goto_functiont &get_goto_functions, symbol_tablet &new_symbol_table)
Symbolically execute the entire program starting from entry point.
Definition: symex_main.cpp:325
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
json_numbert
Definition: json.h:291
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
structured_data_entryt::data_node
static structured_data_entryt data_node(const jsont &data)
Definition: structured_data.cpp:64
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
symex_bmc_incremental_one_loop.h
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
data
Definition: kdev_t.h:24
goto_symext::ignore_assertions
bool ignore_assertions
If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.
Definition: goto_symex.h:156
symex_bmc_incremental_one_loopt::check_break
bool check_break(const irep_idt &loop_id, unsigned unwind) override
Defines condition for interrupting symbolic execution for incremental BMC.
Definition: symex_bmc_incremental_one_loop.cpp:110
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:38
tvt::is_unknown
bool is_unknown() const
Definition: threeval.h:27
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
messaget::eom
static eomt eom
Definition: message.h:297
call_stackt
Definition: call_stack.h:15
goto_symext::initialize_entry_point_state
std::unique_ptr< statet > initialize_entry_point_state(const get_goto_functiont &get_goto_function)
Initialize the symbolic execution and the given state with the beginning of the entry point function.
Definition: symex_main.cpp:404
tvt::is_known
bool is_known() const
Definition: threeval.h:28
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
ui_message_handlert::uit
uit
Definition: ui_message.h:24
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
symex_bmc_incremental_one_loopt::state
std::unique_ptr< goto_symext::statet > state
Definition: symex_bmc_incremental_one_loop.h:40
labelt
Definition: structured_data.h:17
message_handlert
Definition: message.h:28
symex_bmc_incremental_one_loopt::incr_max_unwind
const unsigned incr_max_unwind
Definition: symex_bmc_incremental_one_loop.h:37
tvt
Definition: threeval.h:20
structured_datat
A way of representing nested key/value data.
Definition: structured_data.h:74
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_bmc_incremental_one_loopt::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_incremental_one_loop.cpp:48
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
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_bmc_incremental_one_loopt::incr_min_unwind
const unsigned incr_min_unwind
Definition: symex_bmc_incremental_one_loop.h:38
symex_bmc_incremental_one_loopt::incr_loop_id
const irep_idt incr_loop_id
Definition: symex_bmc_incremental_one_loop.h:36
symex_bmc_incremental_one_loopt::resume
bool resume(const get_goto_functiont &get_goto_function)
Return true if symex can be resumed.
Definition: symex_bmc_incremental_one_loop.cpp:132
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_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt
symex_bmc_incremental_one_loopt(message_handlert &, const symbol_tablet &outer_symbol_table, symex_target_equationt &, const optionst &, path_storaget &, guard_managert &, ui_message_handlert::uit output_ui)
Definition: symex_bmc_incremental_one_loop.cpp:15
symex_bmct
Definition: symex_bmc.h:24
structured_data.h
symex_bmc_incremental_one_loopt::log_unwinding
void log_unwinding(unsigned unwind)
Definition: symex_bmc_incremental_one_loop.cpp:141
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
symex_bmc_incremental_one_loopt::from_entry_point_of
bool from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
Return true if symex can be resumed.
Definition: symex_bmc_incremental_one_loop.cpp:121
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:39
tvt::is_true
bool is_true() const
Definition: threeval.h:25
messaget::statistics
mstreamt & statistics() const
Definition: message.h:419
goto_symext::should_pause_symex
bool should_pause_symex
Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution ...
Definition: goto_symex.h:152