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