cprover
havoc_loops.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Havoc Loops
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "havoc_loops.h"
13 
14 #include <util/std_expr.h>
15 
16 #include <analyses/natural_loops.h>
18 
20 
21 #include "function_modifies.h"
22 
24 {
25 public:
27 
29  function_modifiest &_function_modifies,
30  goto_functiont &_goto_function):
31  goto_function(_goto_function),
32  local_may_alias(_goto_function),
33  function_modifies(_function_modifies),
34  natural_loops(_goto_function.body)
35  {
36  havoc_loops();
37  }
38 
39 protected:
44 
45  typedef std::set<exprt> modifiest;
47 
48  void havoc_loops();
49 
50  void havoc_loop(
51  const goto_programt::targett loop_head,
52  const loopt &);
53 
54  void build_havoc_code(
55  const goto_programt::targett loop_head,
56  const modifiest &modifies,
57  goto_programt &dest);
58 
59  void get_modifies(
60  const loopt &,
61  modifiest &);
62 
64 };
65 
67 {
68  assert(!loop.empty());
69 
70  // find the last instruction in the loop
71  std::map<unsigned, goto_programt::targett> loop_map;
72 
73  for(loopt::const_iterator l_it=loop.begin();
74  l_it!=loop.end();
75  l_it++)
76  loop_map[(*l_it)->location_number]=*l_it;
77 
78  // get the one with the highest number
79  goto_programt::targett last=(--loop_map.end())->second;
80 
81  return ++last;
82 }
83 
85  const goto_programt::targett loop_head,
86  const modifiest &modifies,
87  goto_programt &dest)
88 {
89  for(modifiest::const_iterator
90  m_it=modifies.begin();
91  m_it!=modifies.end();
92  m_it++)
93  {
94  exprt lhs=*m_it;
96 
98  t->function=loop_head->function;
99  t->source_location=loop_head->source_location;
100  t->code=code_assignt(lhs, rhs);
101  t->code.add_source_location()=loop_head->source_location;
102  }
103 }
104 
106  const goto_programt::targett loop_head,
107  const loopt &loop)
108 {
109  assert(!loop.empty());
110 
111  // first find out what can get changed in the loop
112  modifiest modifies;
113  get_modifies(loop, modifies);
114 
115  // build the havocking code
116  goto_programt havoc_code;
117  build_havoc_code(loop_head, modifies, havoc_code);
118 
119  // Now havoc at the loop head. Use insert_swap to
120  // preserve jumps to loop head.
121  goto_function.body.insert_before_swap(loop_head, havoc_code);
122 
123  // compute the loop exit
124  goto_programt::targett loop_exit=
125  get_loop_exit(loop);
126 
127  // divert all gotos to the loop head to the loop exit
128  for(loopt::const_iterator
129  l_it=loop.begin(); l_it!=loop.end(); l_it++)
130  {
131  goto_programt::instructiont &instruction=**l_it;
132  if(instruction.is_goto())
133  {
134  for(goto_programt::targetst::iterator
135  t_it=instruction.targets.begin();
136  t_it!=instruction.targets.end();
137  t_it++)
138  {
139  if(*t_it==loop_head)
140  *t_it=loop_exit; // divert
141  }
142  }
143  }
144 
145  // remove skips
147 }
148 
150  const loopt &loop,
151  modifiest &modifies)
152 {
153  for(loopt::const_iterator
154  i_it=loop.begin(); i_it!=loop.end(); i_it++)
155  {
156  const goto_programt::instructiont &instruction=**i_it;
157 
158  if(instruction.is_assign())
159  {
160  const exprt &lhs=to_code_assign(instruction.code).lhs();
161  function_modifies.get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
162  }
163  else if(instruction.is_function_call())
164  {
165  const code_function_callt &code_function_call=
166  to_code_function_call(instruction.code);
167  const exprt &lhs=code_function_call.lhs();
168 
169  // return value assignment
170  if(lhs.is_not_nil())
172  local_may_alias, *i_it, lhs, modifies);
173 
174  function_modifies(code_function_call.function(), modifies);
175  }
176  }
177 }
178 
180 {
181  // iterate over the (natural) loops in the function
182 
183  for(const auto &loop : natural_loops.loop_map)
184  havoc_loop(loop.first, loop.second);
185 }
186 
187 void havoc_loops(goto_modelt &goto_model)
188 {
189  function_modifiest function_modifies(goto_model.goto_functions);
190 
191  Forall_goto_functions(it, goto_model.goto_functions)
192  havoc_loopst(function_modifies, it->second);
193 }
bool is_not_nil() const
Definition: irep.h:103
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
void get_modifies(const loopt &, modifiest &)
goto_programt body
Definition: goto_function.h:23
typet & type()
Definition: expr.h:56
targetst targets
The list of successor instructions.
Definition: goto_program.h:198
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
havoc_loopst(function_modifiest &_function_modifies, goto_functiont &_goto_function)
Definition: havoc_loops.cpp:28
exprt & lhs()
Definition: std_code.h:208
local_may_aliast local_may_alias
Definition: havoc_loops.cpp:41
instructionst::iterator targett
Definition: goto_program.h:397
void get_modifies_lhs(const local_may_aliast &, const goto_programt::const_targett, const exprt &lhs, modifiest &)
API to expression classes.
std::set< exprt > modifiest
Definition: havoc_loops.cpp:45
::goto_functiont goto_functiont
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
A function call.
Definition: std_code.h:828
Havoc Loops.
natural_loops_mutablet natural_loops
Definition: havoc_loops.cpp:43
void havoc_loops()
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
const natural_loops_mutablet::natural_loopt loopt
Definition: havoc_loops.cpp:46
void havoc_loops(goto_modelt &goto_model)
exprt & function()
Definition: std_code.h:848
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
goto_functionst::goto_functiont goto_functiont
Definition: havoc_loops.cpp:26
goto_functiont & goto_function
Definition: havoc_loops.cpp:40
#define Forall_goto_functions(it, functions)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: havoc_loops.cpp:84
void havoc_loop(const goto_programt::targett loop_head, const loopt &)
function_modifiest & function_modifies
Definition: havoc_loops.cpp:42
Compute natural loops in a goto_function.
Program Transformation.
goto_programt::targett get_loop_exit(const loopt &)
Definition: havoc_loops.cpp:66
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Assignment.
Definition: std_code.h:195
Field-insensitive, location-sensitive may-alias analysis.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879