cprover
k_induction.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: k-induction
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "k_induction.h"
13 
14 #include <analyses/natural_loops.h>
16 
18 
19 #include "havoc_utils.h"
20 #include "loop_utils.h"
21 #include "unwind.h"
22 
24 {
25 public:
27  const irep_idt &_function_id,
28  goto_functiont &_goto_function,
29  bool _base_case,
30  bool _step_case,
31  unsigned _k)
32  : function_id(_function_id),
33  goto_function(_goto_function),
34  local_may_alias(_goto_function),
35  natural_loops(_goto_function.body),
36  base_case(_base_case),
37  step_case(_step_case),
38  k(_k)
39  {
40  k_induction();
41  }
42 
43 protected:
48 
49  const bool base_case, step_case;
50  const unsigned k;
51 
52  void k_induction();
53 
54  void process_loop(
55  const goto_programt::targett loop_head,
56  const loopt &);
57 };
58 
60  const goto_programt::targett loop_head,
61  const loopt &loop)
62 {
63  assert(!loop.empty());
64 
65  // save the loop guard
66  const exprt loop_guard=loop_head->guard;
67 
68  // compute the loop exit
69  goto_programt::targett loop_exit=
70  get_loop_exit(loop);
71 
72  if(base_case)
73  {
74  // now unwind k times
75  goto_unwindt goto_unwind;
76  goto_unwind.unwind(
79  loop_head,
80  loop_exit,
81  k,
83 
84  // assume the loop condition has become false
87  goto_function.body.insert_before_swap(loop_exit, assume);
88  }
89 
90  if(step_case)
91  {
92  // step case
93 
94  // find out what can get changed in the loop
95  modifiest modifies;
96  get_modifies(local_may_alias, loop, modifies);
97 
98  // build the havocking code
99  goto_programt havoc_code;
100  append_havoc_code(loop_head->source_location, modifies, havoc_code);
101 
102  // unwind to get k+1 copies
103  std::vector<goto_programt::targett> iteration_points;
104 
105  goto_unwindt goto_unwind;
106  goto_unwind.unwind(
107  function_id,
109  loop_head,
110  loop_exit,
111  k + 1,
113  iteration_points);
114 
115  // we can remove everything up to the first assertion
116  for(goto_programt::targett t=loop_head; t!=loop_exit; t++)
117  {
118  if(t->is_assert())
119  break;
120  t->turn_into_skip();
121  }
122 
123  // now turn any assertions in iterations 0..k-1 into assumptions
124  assert(iteration_points.size()==k+1);
125 
126  assert(k>=1);
127  goto_programt::targett end=iteration_points[k-1];
128 
129  for(goto_programt::targett t=loop_head; t!=end; t++)
130  {
131  assert(t!=goto_function.body.instructions.end());
132  if(t->is_assert())
133  t->type=ASSUME;
134  }
135 
136  // assume the loop condition has become false
138  goto_programt::make_assumption(loop_guard);
139  goto_function.body.insert_before_swap(loop_exit, assume);
140 
141  // Now havoc at the loop head. Use insert_swap to
142  // preserve jumps to loop head.
143  goto_function.body.insert_before_swap(loop_head, havoc_code);
144  }
145 
146  // remove skips
148 }
149 
151 {
152  // iterate over the (natural) loops in the function
153 
154  for(natural_loops_mutablet::loop_mapt::const_iterator
155  l_it=natural_loops.loop_map.begin();
156  l_it!=natural_loops.loop_map.end();
157  l_it++)
158  process_loop(l_it->first, l_it->second);
159 }
160 
162  goto_modelt &goto_model,
163  bool base_case, bool step_case,
164  unsigned k)
165 {
166  for(auto &gf_entry : goto_model.goto_functions.function_map)
167  k_inductiont(gf_entry.first, gf_entry.second, base_case, step_case, k);
168 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:673
instructionst::iterator targett
Definition: goto_program.h:646
void unwind(const irep_idt &function_id, goto_programt &goto_program, const goto_programt::const_targett loop_head, const goto_programt::const_targett loop_exit, const unsigned k, const unwind_strategyt unwind_strategy)
Definition: unwind.cpp:82
k_inductiont(const irep_idt &_function_id, goto_functiont &_goto_function, bool _base_case, bool _step_case, unsigned _k)
Definition: k_induction.cpp:26
const bool base_case
Definition: k_induction.cpp:49
natural_loops_mutablet natural_loops
Definition: k_induction.cpp:47
local_may_aliast local_may_alias
Definition: k_induction.cpp:46
const unsigned k
Definition: k_induction.cpp:50
goto_functiont & goto_function
Definition: k_induction.cpp:45
const bool step_case
Definition: k_induction.cpp:49
const irep_idt & function_id
Definition: k_induction.cpp:44
void process_loop(const goto_programt::targett loop_head, const loopt &)
Definition: k_induction.cpp:59
void k_induction()
loop_mapt loop_map
Definition: loop_analysis.h:88
@ ASSUME
Definition: goto_program.h:33
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
Definition: havoc_utils.cpp:73
Utilities for building havoc code for expressions.
std::set< exprt > modifiest
Definition: havoc_utils.h:23
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
k-induction
Field-insensitive, location-sensitive may-alias analysis.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:68
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:21
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
Compute natural loops in a goto_function.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
Program Transformation.
Loop unwinding.