cprover
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 : 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 {
41 }
42
43protected:
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 assignst assigns;
96 get_assigns(local_may_alias, loop, assigns);
97
98 // build the havocking code
99 goto_programt havoc_code;
100 havoc_utilst havoc_gen(assigns);
101 havoc_gen.append_full_havoc_code(loop_head->source_location(), 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(
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->turn_into_assume();
135 }
136
137 // assume the loop condition has become false
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 for(auto &gf_entry : goto_model.goto_functions.function_map)
168 k_inductiont(gf_entry.first, gf_entry.second, base_case, step_case, k);
169}
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:180
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:934
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
instructionst::iterator targett
Definition: goto_program.h:592
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
void append_full_havoc_code(const source_locationt location, goto_programt &dest) const
Append goto instructions to havoc the full assigns set.
Definition: havoc_utils.cpp:21
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
Utilities for building havoc code for expressions.
std::set< exprt > assignst
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.
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:72
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:88
Program Transformation.
Loop unwinding.