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 <analyses/natural_loops.h>
16 
18 
19 #include "function_modifies.h"
20 #include "havoc_utils.h"
21 #include "loop_utils.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 get_modifies(
55  const loopt &,
56  modifiest &);
57 };
58 
60  const goto_programt::targett loop_head,
61  const loopt &loop)
62 {
63  assert(!loop.empty());
64 
65  // first find out what can get changed in the loop
66  modifiest modifies;
67  get_modifies(loop, modifies);
68 
69  // build the havocking code
70  goto_programt havoc_code;
71  append_havoc_code(loop_head->source_location, modifies, havoc_code);
72 
73  // Now havoc at the loop head. Use insert_swap to
74  // preserve jumps to loop head.
75  goto_function.body.insert_before_swap(loop_head, havoc_code);
76 
77  // compute the loop exit
78  goto_programt::targett loop_exit=
79  get_loop_exit(loop);
80 
81  // divert all gotos to the loop head to the loop exit
83  l_it=loop.begin(); l_it!=loop.end(); l_it++)
84  {
85  goto_programt::instructiont &instruction=**l_it;
86  if(instruction.is_goto())
87  {
88  for(goto_programt::targetst::iterator
89  t_it=instruction.targets.begin();
90  t_it!=instruction.targets.end();
91  t_it++)
92  {
93  if(*t_it==loop_head)
94  *t_it=loop_exit; // divert
95  }
96  }
97  }
98 
99  // remove skips
101 }
102 
104  const loopt &loop,
105  modifiest &modifies)
106 {
107  for(const auto &instruction_it : loop)
108  function_modifies.get_modifies(local_may_alias, instruction_it, modifies);
109 }
110 
112 {
113  // iterate over the (natural) loops in the function
114 
115  for(const auto &loop : natural_loops.loop_map)
116  havoc_loop(loop.first, loop.second);
117 }
118 
119 void havoc_loops(goto_modelt &goto_model)
120 {
121  function_modifiest function_modifies(goto_model.goto_functions);
122 
123  for(auto &gf_entry : goto_model.goto_functions.function_map)
124  havoc_loopst(function_modifies, gf_entry.second);
125 }
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: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:178
targetst targets
The list of successor instructions.
Definition: goto_program.h:468
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:673
instructionst::iterator targett
Definition: goto_program.h:646
void havoc_loops()
void get_modifies(const loopt &, modifiest &)
const natural_loops_mutablet::natural_loopt loopt
Definition: havoc_loops.cpp:46
void havoc_loop(const goto_programt::targett loop_head, const loopt &)
Definition: havoc_loops.cpp:59
goto_functiont & goto_function
Definition: havoc_loops.cpp:40
havoc_loopst(function_modifiest &_function_modifies, goto_functiont &_goto_function)
Definition: havoc_loops.cpp:28
local_may_aliast local_may_alias
Definition: havoc_loops.cpp:41
function_modifiest & function_modifies
Definition: havoc_loops.cpp:42
goto_functionst::goto_functiont goto_functiont
Definition: havoc_loops.cpp:26
natural_loops_mutablet natural_loops
Definition: havoc_loops.cpp:43
std::set< exprt > modifiest
Definition: havoc_loops.cpp:45
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.
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
Definition: havoc_utils.cpp:73
Utilities for building havoc code for expressions.
Field-insensitive, location-sensitive may-alias analysis.
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:21
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:86
Program Transformation.