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_assigns.h"
20 #include "havoc_utils.h"
21 #include "loop_utils.h"
22 
24 {
25 public:
27 
29  function_assignst &_function_assigns,
30  goto_functiont &_goto_function)
31  : goto_function(_goto_function),
32  local_may_alias(_goto_function),
33  function_assigns(_function_assigns),
34  natural_loops(_goto_function.body)
35  {
36  havoc_loops();
37  }
38 
39 protected:
44 
45  typedef std::set<exprt> assignst;
47 
48  void havoc_loops();
49 
50  void havoc_loop(
51  const goto_programt::targett loop_head,
52  const loopt &);
53 
54  void get_assigns(const loopt &, assignst &);
55 };
56 
58  const goto_programt::targett loop_head,
59  const loopt &loop)
60 {
61  assert(!loop.empty());
62 
63  // first find out what can get changed in the loop
64  assignst assigns;
65  get_assigns(loop, assigns);
66 
67  // build the havocking code
68  goto_programt havoc_code;
69  havoc_utilst havoc_gen(assigns);
70  havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code);
71 
72  // Now havoc at the loop head. Use insert_swap to
73  // preserve jumps to loop head.
74  goto_function.body.insert_before_swap(loop_head, havoc_code);
75 
76  // compute the loop exit
77  goto_programt::targett loop_exit=
78  get_loop_exit(loop);
79 
80  // divert all gotos to the loop head to the loop exit
82  l_it=loop.begin(); l_it!=loop.end(); l_it++)
83  {
84  goto_programt::instructiont &instruction=**l_it;
85  if(instruction.is_goto())
86  {
87  for(goto_programt::targetst::iterator
88  t_it=instruction.targets.begin();
89  t_it!=instruction.targets.end();
90  t_it++)
91  {
92  if(*t_it==loop_head)
93  *t_it=loop_exit; // divert
94  }
95  }
96  }
97 
98  // remove skips
100 }
101 
102 void havoc_loopst::get_assigns(const loopt &loop, assignst &assigns)
103 {
104  for(const auto &instruction_it : loop)
105  function_assigns.get_assigns(local_may_alias, instruction_it, assigns);
106 }
107 
109 {
110  // iterate over the (natural) loops in the function
111 
112  for(const auto &loop : natural_loops.loop_map)
113  havoc_loop(loop.first, loop.second);
114 }
115 
116 void havoc_loops(goto_modelt &goto_model)
117 {
118  function_assignst function_assigns(goto_model.goto_functions);
119 
120  for(auto &gf_entry : goto_model.goto_functions.function_map)
121  havoc_loopst(function_assigns, gf_entry.second);
122 }
void get_assigns(const local_may_aliast &local_may_alias, const goto_programt::const_targett, assignst &)
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:180
targetst targets
The list of successor instructions.
Definition: goto_program.h:403
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
instructionst::iterator targett
Definition: goto_program.h:592
void havoc_loops()
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:57
void get_assigns(const loopt &, assignst &)
goto_functiont & goto_function
Definition: havoc_loops.cpp:40
local_may_aliast local_may_alias
Definition: havoc_loops.cpp:41
goto_functionst::goto_functiont goto_functiont
Definition: havoc_loops.cpp:26
function_assignst & function_assigns
Definition: havoc_loops.cpp:42
natural_loops_mutablet natural_loops
Definition: havoc_loops.cpp:43
std::set< exprt > assignst
Definition: havoc_loops.cpp:45
havoc_loopst(function_assignst &_function_assigns, goto_functiont &_goto_function)
Definition: havoc_loops.cpp:28
void append_full_havoc_code(const source_locationt location, goto_programt &dest) const
Append goto instructions to havoc the full assigns set.
Definition: havoc_utils.cpp:21
loop_mapt loop_map
Definition: loop_analysis.h:88
loop_instructionst::const_iterator const_iterator
Definition: loop_analysis.h:46
Compute objects assigned to in a function.
void havoc_loops(goto_modelt &goto_model)
Havoc Loops.
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:88
Program Transformation.