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 <util/std_expr.h>
15 
16 #include <analyses/natural_loops.h>
18 
20 
21 #include "unwind.h"
22 #include "loop_utils.h"
23 
25 {
26 public:
28 
30  goto_functiont &_goto_function,
31  bool _base_case, bool _step_case,
32  unsigned _k):
33  goto_function(_goto_function),
34  local_may_alias(_goto_function),
35  natural_loops(_goto_function.body),
36  base_case(_base_case), step_case(_step_case), k(_k)
37  {
38  k_induction();
39  }
40 
41 protected:
45 
46  const bool base_case, step_case;
47  const unsigned k;
48 
49  void k_induction();
50 
51  void process_loop(
52  const goto_programt::targett loop_head,
53  const loopt &);
54 };
55 
57  const goto_programt::targett loop_head,
58  const loopt &loop)
59 {
60  assert(!loop.empty());
61 
62  // save the loop guard
63  const exprt loop_guard=loop_head->guard;
64 
65  // compute the loop exit
66  goto_programt::targett loop_exit=
67  get_loop_exit(loop);
68 
69  if(base_case)
70  {
71  // now unwind k times
72  goto_unwindt goto_unwind;
73  goto_unwind.unwind(goto_function.body, loop_head, loop_exit, k,
75 
76  // assume the loop condition has become false
78  assume.guard=loop_guard;
79  goto_function.body.insert_before_swap(loop_exit, assume);
80  }
81 
82  if(step_case)
83  {
84  // step case
85 
86  // find out what can get changed in the loop
87  modifiest modifies;
88  get_modifies(local_may_alias, loop, modifies);
89 
90  // build the havocking code
91  goto_programt havoc_code;
92  build_havoc_code(loop_head, modifies, havoc_code);
93 
94  // unwind to get k+1 copies
95  std::vector<goto_programt::targett> iteration_points;
96 
97  goto_unwindt goto_unwind;
98  goto_unwind.unwind(
100  loop_head,
101  loop_exit,
102  k+1,
104  iteration_points);
105 
106  // we can remove everything up to the first assertion
107  for(goto_programt::targett t=loop_head; t!=loop_exit; t++)
108  {
109  if(t->is_assert())
110  break;
111  t->make_skip();
112  }
113 
114  // now turn any assertions in iterations 0..k-1 into assumptions
115  assert(iteration_points.size()==k+1);
116 
117  assert(k>=1);
118  goto_programt::targett end=iteration_points[k-1];
119 
120  for(goto_programt::targett t=loop_head; t!=end; t++)
121  {
122  assert(t!=goto_function.body.instructions.end());
123  if(t->is_assert())
124  t->type=ASSUME;
125  }
126 
127  // assume the loop condition has become false
129  assume.guard=loop_guard;
130  goto_function.body.insert_before_swap(loop_exit, assume);
131 
132  // Now havoc at the loop head. Use insert_swap to
133  // preserve jumps to loop head.
134  goto_function.body.insert_before_swap(loop_head, havoc_code);
135  }
136 
137  // remove skips
139 }
140 
142 {
143  // iterate over the (natural) loops in the function
144 
145  for(natural_loops_mutablet::loop_mapt::const_iterator
146  l_it=natural_loops.loop_map.begin();
147  l_it!=natural_loops.loop_map.end();
148  l_it++)
149  process_loop(l_it->first, l_it->second);
150 }
151 
153  goto_modelt &goto_model,
154  bool base_case, bool step_case,
155  unsigned k)
156 {
157  Forall_goto_functions(it, goto_model.goto_functions)
158  k_inductiont(it->second, base_case, step_case, k);
159 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
goto_functionst::goto_functiont goto_functiont
Definition: k_induction.cpp:27
local_may_aliast local_may_alias
Definition: k_induction.cpp:43
void process_loop(const goto_programt::targett loop_head, const loopt &)
Definition: k_induction.cpp:56
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
goto_programt body
Definition: goto_function.h:23
const natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
goto_functiont & goto_function
Definition: k_induction.cpp:42
const unsigned k
Definition: k_induction.cpp:47
k_inductiont(goto_functiont &_goto_function, bool _base_case, bool _step_case, unsigned _k)
Definition: k_induction.cpp:29
k-induction
natural_loops_mutablet natural_loops
Definition: k_induction.cpp:44
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const bool step_case
Definition: k_induction.cpp:46
instructionst::iterator targett
Definition: goto_program.h:397
const bool base_case
Definition: k_induction.cpp:46
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:19
::goto_functiont goto_functiont
std::set< exprt > modifiest
Definition: loop_utils.h:17
Helper functions for k-induction and loop invariants.
Loop unwinding.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void k_induction()
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:88
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
Base class for all expressions.
Definition: expr.h:42
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
#define Forall_goto_functions(it, functions)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:37
Compute natural loops in a goto_function.
Program Transformation.
void unwind(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:79
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Field-insensitive, location-sensitive may-alias analysis.