CBMC
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  const namespacet &ns)
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  ns(ns)
41  {
42  k_induction();
43  }
44 
45 protected:
50 
51  const bool base_case, step_case;
52  const unsigned k;
53 
54  const namespacet &ns;
55 
56  void k_induction();
57 
58  void process_loop(
59  const goto_programt::targett loop_head,
60  const loopt &);
61 };
62 
64  const goto_programt::targett loop_head,
65  const loopt &loop)
66 {
67  PRECONDITION(!loop.empty());
68 
69  // save the loop guard
70  const exprt loop_guard = loop_head->condition();
71 
72  // compute the loop exit
73  goto_programt::targett loop_exit=
74  get_loop_exit(loop);
75 
76  if(base_case)
77  {
78  // now unwind k times
79  goto_unwindt goto_unwind;
80  goto_unwind.unwind(
83  loop_head,
84  loop_exit,
85  k,
87 
88  // assume the loop condition has become false
91  goto_function.body.insert_before_swap(loop_exit, assume);
92  }
93 
94  if(step_case)
95  {
96  // step case
97 
98  // find out what can get changed in the loop
99  assignst assigns;
100  get_assigns(local_may_alias, loop, assigns);
101 
102  // build the havocking code
103  goto_programt havoc_code;
104  havoc_utilst havoc_gen(assigns, ns);
105  havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code);
106 
107  // unwind to get k+1 copies
108  std::vector<goto_programt::targett> iteration_points;
109 
110  goto_unwindt goto_unwind;
111  goto_unwind.unwind(
112  function_id,
114  loop_head,
115  loop_exit,
116  k + 1,
118  iteration_points);
119 
120  // we can remove everything up to the first assertion
121  for(goto_programt::targett t=loop_head; t!=loop_exit; t++)
122  {
123  if(t->is_assert())
124  break;
125  t->turn_into_skip();
126  }
127 
128  // now turn any assertions in iterations 0..k-1 into assumptions
130  iteration_points.size() == k + 1, "number of iteration points");
131 
132  DATA_INVARIANT(k >= 1, "at least one iteration");
133  goto_programt::targett end=iteration_points[k-1];
134 
135  for(goto_programt::targett t=loop_head; t!=end; t++)
136  {
138  t != goto_function.body.instructions.end(), "t is in range");
139  if(t->is_assert())
140  t->turn_into_assume();
141  }
142 
143  // assume the loop condition has become false
145  goto_programt::make_assumption(loop_guard);
146  goto_function.body.insert_before_swap(loop_exit, assume);
147 
148  // Now havoc at the loop head. Use insert_swap to
149  // preserve jumps to loop head.
150  goto_function.body.insert_before_swap(loop_head, havoc_code);
151  }
152 
153  // remove skips
155 }
156 
158 {
159  // iterate over the (natural) loops in the function
160 
161  for(natural_loops_mutablet::loop_mapt::const_iterator
162  l_it=natural_loops.loop_map.begin();
163  l_it!=natural_loops.loop_map.end();
164  l_it++)
165  process_loop(l_it->first, l_it->second);
166 }
167 
169  goto_modelt &goto_model,
170  bool base_case, bool step_case,
171  unsigned k)
172 {
173  for(auto &gf_entry : goto_model.goto_functions.function_map)
174  {
175  k_inductiont(
176  gf_entry.first,
177  gf_entry.second,
178  base_case,
179  step_case,
180  k,
181  namespacet{goto_model.symbol_table});
182  }
183 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
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:34
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:945
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
instructionst::iterator targett
Definition: goto_program.h:614
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:84
void append_full_havoc_code(const source_locationt location, goto_programt &dest)
Append goto instructions to havoc the full assigns set.
Definition: havoc_utils.cpp:21
const bool base_case
Definition: k_induction.cpp:51
natural_loops_mutablet natural_loops
Definition: k_induction.cpp:49
local_may_aliast local_may_alias
Definition: k_induction.cpp:48
const unsigned k
Definition: k_induction.cpp:52
goto_functiont & goto_function
Definition: k_induction.cpp:47
const bool step_case
Definition: k_induction.cpp:51
k_inductiont(const irep_idt &_function_id, goto_functiont &_goto_function, bool _base_case, bool _step_case, unsigned _k, const namespacet &ns)
Definition: k_induction.cpp:26
const namespacet & ns
Definition: k_induction.cpp:54
const irep_idt & function_id
Definition: k_induction.cpp:46
void process_loop(const goto_programt::targett loop_head, const loopt &)
Definition: k_induction.cpp:63
void k_induction()
loop_mapt loop_map
Definition: loop_analysis.h:88
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Definition: havoc_utils.h:22
void k_induction(goto_modelt &goto_model, bool base_case, bool step_case, unsigned k)
k-induction
Field-insensitive, location-sensitive may-alias analysis.
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:21
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Definition: loop_utils.cpp:90
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:87
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Loop unwinding.