cprover
Loading...
Searching...
No Matches
k_induction.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: k-induction
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "k_induction.h"
13
16
18
19#include "havoc_utils.h"
20#include "loop_utils.h"
21#include "unwind.h"
22
24{
25public:
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 {
43 }
44
45protected:
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(
82 goto_function.body,
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(
113 goto_function.body,
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
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 {
176 gf_entry.first,
177 gf_entry.second,
178 base_case,
179 step_case,
180 k,
181 namespacet{goto_model.symbol_table});
182 }
183}
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...
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
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.
const bool base_case
natural_loops_mutablet natural_loops
local_may_aliast local_may_alias
const unsigned k
goto_functiont & goto_function
const bool step_case
k_inductiont(const irep_idt &_function_id, goto_functiont &_goto_function, bool _base_case, bool _step_case, unsigned _k, const namespacet &ns)
const namespacet & ns
const irep_idt & function_id
void process_loop(const goto_programt::targett loop_head, const loopt &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Definition havoc_utils.h:24
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)
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
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.
natural_loops_templatet< goto_programt, goto_programt::targett, goto_programt::target_less_than > natural_loops_mutablet
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
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.
dstringt irep_idt