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 #include "loop_utils.h"
23 
25 {
26 public:
28 
30  function_modifiest &_function_modifies,
31  goto_functiont &_goto_function):
32  goto_function(_goto_function),
33  local_may_alias(_goto_function),
34  function_modifies(_function_modifies),
35  natural_loops(_goto_function.body)
36  {
37  havoc_loops();
38  }
39 
40 protected:
45 
46  typedef std::set<exprt> modifiest;
48 
49  void havoc_loops();
50 
51  void havoc_loop(
52  const goto_programt::targett loop_head,
53  const loopt &);
54 
55  void get_modifies(
56  const loopt &,
57  modifiest &);
58 };
59 
61  const goto_programt::targett loop_head,
62  const loopt &loop)
63 {
64  assert(!loop.empty());
65 
66  // first find out what can get changed in the loop
67  modifiest modifies;
68  get_modifies(loop, modifies);
69 
70  // build the havocking code
71  goto_programt havoc_code;
72  build_havoc_code(loop_head, modifies, havoc_code);
73 
74  // Now havoc at the loop head. Use insert_swap to
75  // preserve jumps to loop head.
76  goto_function.body.insert_before_swap(loop_head, havoc_code);
77 
78  // compute the loop exit
79  goto_programt::targett loop_exit=
80  get_loop_exit(loop);
81 
82  // divert all gotos to the loop head to the loop exit
84  l_it=loop.begin(); l_it!=loop.end(); l_it++)
85  {
86  goto_programt::instructiont &instruction=**l_it;
87  if(instruction.is_goto())
88  {
89  for(goto_programt::targetst::iterator
90  t_it=instruction.targets.begin();
91  t_it!=instruction.targets.end();
92  t_it++)
93  {
94  if(*t_it==loop_head)
95  *t_it=loop_exit; // divert
96  }
97  }
98  }
99 
100  // remove skips
102 }
103 
105  const loopt &loop,
106  modifiest &modifies)
107 {
108  for(const auto &instruction_it : loop)
109  function_modifies.get_modifies(local_may_alias, instruction_it, modifies);
110 }
111 
113 {
114  // iterate over the (natural) loops in the function
115 
116  for(const auto &loop : natural_loops.loop_map)
117  havoc_loop(loop.first, loop.second);
118 }
119 
120 void havoc_loops(goto_modelt &goto_model)
121 {
122  function_modifiest function_modifies(goto_model.goto_functions);
123 
124  for(auto &gf_entry : goto_model.goto_functions.function_map)
125  havoc_loopst(function_modifies, gf_entry.second);
126 }
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
goto_programt body
Definition: goto_function.h:29
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
targetst targets
The list of successor instructions.
Definition: goto_program.h:371
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:577
instructionst::iterator targett
Definition: goto_program.h:550
void havoc_loops()
void get_modifies(const loopt &, modifiest &)
const natural_loops_mutablet::natural_loopt loopt
Definition: havoc_loops.cpp:47
void havoc_loop(const goto_programt::targett loop_head, const loopt &)
Definition: havoc_loops.cpp:60
goto_functiont & goto_function
Definition: havoc_loops.cpp:41
havoc_loopst(function_modifiest &_function_modifies, goto_functiont &_goto_function)
Definition: havoc_loops.cpp:29
local_may_aliast local_may_alias
Definition: havoc_loops.cpp:42
function_modifiest & function_modifies
Definition: havoc_loops.cpp:43
goto_functionst::goto_functiont goto_functiont
Definition: havoc_loops.cpp:27
natural_loops_mutablet natural_loops
Definition: havoc_loops.cpp:44
std::set< exprt > modifiest
Definition: havoc_loops.cpp:46
loop_mapt loop_map
Definition: loop_analysis.h:88
loop_instructionst::const_iterator const_iterator
Definition: loop_analysis.h:46
void havoc_loops(goto_modelt &goto_model)
Havoc Loops.
Field-insensitive, location-sensitive may-alias analysis.
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:20
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:38
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
Definition: remove_skip.cpp:85
Program Transformation.
API to expression classes.