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;
95  exprt rhs =
97 
99  t->function=loop_head->function;
100  t->source_location=loop_head->source_location;
101  t->code=code_assignt(lhs, rhs);
102  t->code.add_source_location()=loop_head->source_location;
103  }
104 }
105 
107  const goto_programt::targett loop_head,
108  const loopt &loop)
109 {
110  assert(!loop.empty());
111 
112  // first find out what can get changed in the loop
113  modifiest modifies;
114  get_modifies(loop, modifies);
115 
116  // build the havocking code
117  goto_programt havoc_code;
118  build_havoc_code(loop_head, modifies, havoc_code);
119 
120  // Now havoc at the loop head. Use insert_swap to
121  // preserve jumps to loop head.
122  goto_function.body.insert_before_swap(loop_head, havoc_code);
123 
124  // compute the loop exit
125  goto_programt::targett loop_exit=
126  get_loop_exit(loop);
127 
128  // divert all gotos to the loop head to the loop exit
129  for(loopt::const_iterator
130  l_it=loop.begin(); l_it!=loop.end(); l_it++)
131  {
132  goto_programt::instructiont &instruction=**l_it;
133  if(instruction.is_goto())
134  {
135  for(goto_programt::targetst::iterator
136  t_it=instruction.targets.begin();
137  t_it!=instruction.targets.end();
138  t_it++)
139  {
140  if(*t_it==loop_head)
141  *t_it=loop_exit; // divert
142  }
143  }
144  }
145 
146  // remove skips
148 }
149 
151  const loopt &loop,
152  modifiest &modifies)
153 {
154  for(loopt::const_iterator
155  i_it=loop.begin(); i_it!=loop.end(); i_it++)
156  {
157  const goto_programt::instructiont &instruction=**i_it;
158 
159  if(instruction.is_assign())
160  {
161  const exprt &lhs=to_code_assign(instruction.code).lhs();
162  function_modifies.get_modifies_lhs(local_may_alias, *i_it, lhs, modifies);
163  }
164  else if(instruction.is_function_call())
165  {
166  const code_function_callt &code_function_call=
167  to_code_function_call(instruction.code);
168  const exprt &lhs=code_function_call.lhs();
169 
170  // return value assignment
171  if(lhs.is_not_nil())
173  local_may_alias, *i_it, lhs, modifies);
174 
175  function_modifies(code_function_call.function(), modifies);
176  }
177  }
178 }
179 
181 {
182  // iterate over the (natural) loops in the function
183 
184  for(const auto &loop : natural_loops.loop_map)
185  havoc_loop(loop.first, loop.second);
186 }
187 
188 void havoc_loops(goto_modelt &goto_model)
189 {
190  function_modifiest function_modifies(goto_model.goto_functions);
191 
192  Forall_goto_functions(it, goto_model.goto_functions)
193  havoc_loopst(function_modifies, it->second);
194 }
goto_functiont::body
goto_programt body
Definition: goto_function.h:29
function_modifiest
Definition: function_modifies.h:18
havoc_loops.h
havoc_loopst::get_modifies
void get_modifies(const loopt &, modifiest &)
Definition: havoc_loops.cpp:150
havoc_loopst
Definition: havoc_loops.cpp:23
havoc_loopst::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: havoc_loops.cpp:26
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:203
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
local_may_aliast
Definition: local_may_alias.h:25
havoc_loopst::havoc_loopst
havoc_loopst(function_modifiest &_function_modifies, goto_functiont &_goto_function)
Definition: havoc_loops.cpp:28
function_modifies.h
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
havoc_loopst::goto_function
goto_functiont & goto_function
Definition: havoc_loops.cpp:40
local_may_alias.h
goto_programt::instructiont::code
codet code
Definition: goto_program.h:181
typet::source_location
const source_locationt & source_location() const
Definition: type.h:62
havoc_loopst::loopt
const typedef natural_loops_mutablet::natural_loopt loopt
Definition: havoc_loops.cpp:46
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
havoc_loopst::modifiest
std::set< exprt > modifiest
Definition: havoc_loops.cpp:45
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
havoc_loopst::natural_loops
natural_loops_mutablet natural_loops
Definition: havoc_loops.cpp:43
havoc_loopst::build_havoc_code
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: havoc_loops.cpp:84
natural_loops_templatet< goto_programt, goto_programt::targett >
havoc_loopst::local_may_alias
local_may_aliast local_may_alias
Definition: havoc_loops.cpp:41
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
goto_programt::instructiont::is_goto
bool is_goto() const
Definition: goto_program.h:305
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
ASSIGN
Definition: goto_program.h:46
havoc_loopst::havoc_loops
void havoc_loops()
Definition: havoc_loops.cpp:180
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
natural_loops.h
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:307
havoc_loopst::havoc_loop
void havoc_loop(const goto_programt::targett loop_head, const loopt &)
Definition: havoc_loops.cpp:106
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
havoc_loopst::function_modifies
function_modifiest & function_modifies
Definition: havoc_loops.cpp:42
havoc_loops
void havoc_loops(goto_modelt &goto_model)
Definition: havoc_loops.cpp:188
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
remove_skip.h
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
loopt
const typedef natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:308
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
natural_loops_templatet::loop_map
loop_mapt loop_map
Definition: natural_loops.h:54
havoc_loopst::get_loop_exit
goto_programt::targett get_loop_exit(const loopt &)
Definition: havoc_loops.cpp:66
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
natural_loops_templatet< goto_programt, goto_programt::targett >::natural_loopt
std::set< goto_programt::targett > natural_loopt
Definition: natural_loops.h:49
function_modifiest::get_modifies_lhs
void get_modifies_lhs(const local_may_aliast &, const goto_programt::const_targett, const exprt &lhs, modifiest &)
Definition: function_modifies.cpp:16