cprover
Loading...
Searching...
No Matches
havoc_loops.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Havoc Loops
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "havoc_loops.h"
13
16
18
19#include "function_assigns.h"
20#include "havoc_utils.h"
21#include "loop_utils.h"
22
56
59 const loopt &loop)
60{
61 assert(!loop.empty());
62
63 // first find out what can get changed in the loop
64 assignst assigns;
65 get_assigns(loop, assigns);
66
67 // build the havocking code
69 havoc_utilst havoc_gen(assigns);
70 havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code);
71
72 // Now havoc at the loop head. Use insert_swap to
73 // preserve jumps to loop head.
75
76 // compute the loop exit
78 get_loop_exit(loop);
79
80 // divert all gotos to the loop head to the loop exit
81 for(loopt::const_iterator
82 l_it=loop.begin(); l_it!=loop.end(); l_it++)
83 {
84 goto_programt::instructiont &instruction=**l_it;
85 if(instruction.is_goto())
86 {
87 for(goto_programt::targetst::iterator
88 t_it=instruction.targets.begin();
89 t_it!=instruction.targets.end();
90 t_it++)
91 {
92 if(*t_it==loop_head)
93 *t_it=loop_exit; // divert
94 }
95 }
96 }
97
98 // remove skips
100}
101
102void havoc_loopst::get_assigns(const loopt &loop, assignst &assigns)
103{
104 for(const auto &instruction_it : loop)
106}
107
109{
110 // iterate over the (natural) loops in the function
111
112 for(const auto &loop : natural_loops.loop_map)
113 havoc_loop(loop.first, loop.second);
114}
115
116void havoc_loops(goto_modelt &goto_model)
117{
118 function_assignst function_assigns(goto_model.goto_functions);
119
120 for(auto &gf_entry : goto_model.goto_functions.function_map)
121 havoc_loopst(function_assigns, gf_entry.second);
122}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
void get_assigns(const local_may_aliast &local_may_alias, const goto_programt::const_targett, assignst &)
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
targetst targets
The list of successor instructions.
A generic container class for the GOTO intermediate representation of one function.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
const natural_loops_mutablet::natural_loopt loopt
void havoc_loop(const goto_programt::targett loop_head, const loopt &)
void get_assigns(const loopt &, assignst &)
goto_functiont & goto_function
local_may_aliast local_may_alias
goto_functionst::goto_functiont goto_functiont
function_assignst & function_assigns
natural_loops_mutablet natural_loops
std::set< exprt > assignst
havoc_loopst(function_assignst &_function_assigns, goto_functiont &_goto_function)
loop_mapt loop_map
Compute objects assigned to in a function.
void havoc_loops(goto_modelt &goto_model)
Havoc Loops.
Utilities for building havoc code for expressions.
Field-insensitive, location-sensitive may-alias analysis.
goto_programt::targett get_loop_exit(const loopt &loop)
Helper functions for k-induction and loop invariants.
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
Program Transformation.