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 }
goto_functiont::body
goto_programt body
Definition: goto_function.h:26
function_modifiest
Definition: function_modifies.h:23
havoc_loops.h
Havoc Loops.
havoc_loopst::get_modifies
void get_modifies(const loopt &, modifiest &)
Definition: havoc_loops.cpp:103
havoc_loopst
Definition: havoc_loops.cpp:24
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
goto_modelt
Definition: goto_model.h:26
havoc_utils.h
Utilities for building havoc code for expressions.
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:468
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
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:28
function_modifies.h
Modifies.
havoc_loopst::goto_function
goto_functiont & goto_function
Definition: havoc_loops.cpp:40
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:46
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:21
havoc_loopst::modifiest
std::set< exprt > modifiest
Definition: havoc_loops.cpp:45
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
havoc_loopst::natural_loops
natural_loops_mutablet natural_loops
Definition: havoc_loops.cpp:43
natural_loops_templatet< goto_programt, goto_programt::targett >
havoc_loopst::local_may_alias
local_may_aliast local_may_alias
Definition: havoc_loops.cpp:41
loop_utils.h
Helper functions for k-induction and loop invariants.
goto_programt::instructiont::is_goto
bool is_goto() const
Definition: goto_program.h:527
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:27
havoc_loopst::havoc_loops
void havoc_loops()
Definition: havoc_loops.cpp:111
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:20
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:59
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
havoc_loopst::function_modifies
function_modifiest & function_modifies
Definition: havoc_loops.cpp:42
append_havoc_code
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
Definition: havoc_utils.cpp:73
havoc_loops
void havoc_loops(goto_modelt &goto_model)
Definition: havoc_loops.cpp:119
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:673
remove_skip.h
Program Transformation.
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
loop_analysist::loop_map
loop_mapt loop_map
Definition: loop_analysis.h:88