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  Forall_goto_functions(it, goto_model.goto_functions)
125  havoc_loopst(function_modifies, it->second);
126 }
goto_functiont::body
goto_programt body
Definition: goto_function.h:30
function_modifiest
Definition: function_modifies.h:19
havoc_loops.h
Havoc Loops.
havoc_loopst::get_modifies
void get_modifies(const loopt &, modifiest &)
Definition: havoc_loops.cpp:104
havoc_loopst
Definition: havoc_loops.cpp:25
havoc_loopst::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: havoc_loops.cpp:27
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:85
goto_modelt
Definition: goto_model.h:26
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:306
local_may_aliast
Definition: local_may_alias.h:26
havoc_loopst::havoc_loopst
havoc_loopst(function_modifiest &_function_modifies, goto_functiont &_goto_function)
Definition: havoc_loops.cpp:29
function_modifies.h
Modifies.
havoc_loopst::goto_function
goto_functiont & goto_function
Definition: havoc_loops.cpp:41
loop_templatet::const_iterator
loop_instructionst::const_iterator const_iterator
Definition: loop_analysis.h:46
havoc_loopst::loopt
const natural_loops_mutablet::natural_loopt loopt
Definition: havoc_loops.cpp:47
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
get_loop_exit
goto_programt::targett get_loop_exit(const loopt &loop)
Definition: loop_utils.cpp:19
havoc_loopst::modifiest
std::set< exprt > modifiest
Definition: havoc_loops.cpp:46
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
havoc_loopst::natural_loops
natural_loops_mutablet natural_loops
Definition: havoc_loops.cpp:44
natural_loops_templatet< goto_programt, goto_programt::targett >
havoc_loopst::local_may_alias
local_may_aliast local_may_alias
Definition: havoc_loops.cpp:42
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
loop_utils.h
Helper functions for k-induction and loop invariants.
goto_programt::instructiont::is_goto
bool is_goto() const
Definition: goto_program.h:458
natural_loops_templatet< goto_programt, goto_programt::targett >::natural_loopt
parentt::loopt natural_loopt
Definition: natural_loops.h:52
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
havoc_loopst::havoc_loops
void havoc_loops()
Definition: havoc_loops.cpp:112
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
function_modifiest::get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
Definition: function_modifies.cpp:18
natural_loops.h
Compute natural loops in a goto_function.
havoc_loopst::havoc_loop
void havoc_loop(const goto_programt::targett loop_head, const loopt &)
Definition: havoc_loops.cpp:60
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
havoc_loopst::function_modifies
function_modifiest & function_modifies
Definition: havoc_loops.cpp:43
havoc_loops
void havoc_loops(goto_modelt &goto_model)
Definition: havoc_loops.cpp:120
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
remove_skip.h
Program Transformation.
build_havoc_code
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:37
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
std_expr.h
API to expression classes.
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
loop_analysist::loop_map
loop_mapt loop_map
Definition: loop_analysis.h:88