cprover
cone_of_influence.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #include "cone_of_influence.h"
13 
15  const expr_sett &targets,
16  expr_sett &cone)
17 {
18  if(program.instructions.empty())
19  {
20  cone=targets;
21  return;
22  }
23 
24  for(goto_programt::instructionst::const_reverse_iterator
25  rit=program.instructions.rbegin();
26  rit != program.instructions.rend();
27  ++rit)
28  {
29  expr_sett curr; // =targets;
30  expr_sett next;
31 
32  if(rit == program.instructions.rbegin())
33  {
34  curr=targets;
35  }
36  else
37  {
38  get_succs(rit, curr);
39  }
40 
41  cone_of_influence(*rit, curr, next);
42 
43  cone_map[rit->location_number]=next;
44 
45 #ifdef DEBUG
46  std::cout << "Previous cone: \n";
47 
48  for(const auto &expr : curr)
49  std::cout << expr2c(expr, ns) << " ";
50 
51  std::cout << "\nCurrent cone: \n";
52 
53  for(const auto &expr : next)
54  std::cout << expr2c(expr, ns) << " ";
55 
56  std::cout << '\n';
57 #endif
58  }
59 
60  cone=cone_map[program.instructions.front().location_number];
61 }
62 
64  const exprt &target,
65  expr_sett &cone)
66 {
67  expr_sett s;
68  s.insert(target);
69  cone_of_influence(s, cone);
70 }
71 
73  goto_programt::instructionst::const_reverse_iterator rit,
74  expr_sett &targets)
75 {
76  if(rit == program.instructions.rbegin())
77  {
78  return;
79  }
80 
81  goto_programt::instructionst::const_reverse_iterator next=rit;
82  --next;
83 
84  if(rit->is_goto())
85  {
86  if(!rit->get_condition().is_false())
87  {
88  // Branch can be taken.
89  for(goto_programt::targetst::const_iterator t=rit->targets.begin();
90  t != rit->targets.end();
91  ++t)
92  {
93  unsigned int loc=(*t)->location_number;
94  expr_sett &s=cone_map[loc];
95  targets.insert(s.begin(), s.end());
96  }
97  }
98 
99  if(rit->get_condition().is_true())
100  {
101  return;
102  }
103  }
104  else if(rit->is_assume() || rit->is_assert())
105  {
106  if(rit->get_condition().is_false())
107  {
108  return;
109  }
110  }
111 
112  unsigned int loc=next->location_number;
113  expr_sett &s=cone_map[loc];
114  targets.insert(s.begin(), s.end());
115 }
116 
119  const expr_sett &curr,
120  expr_sett &next)
121 {
122  next.insert(curr.begin(), curr.end());
123 
124  if(i.is_assign())
125  {
126  expr_sett lhs_syms;
127  bool care=false;
128 
129  gather_rvalues(i.assign_lhs(), lhs_syms);
130 
131  for(const auto &expr : lhs_syms)
132  if(curr.find(expr)!=curr.end())
133  {
134  care=true;
135  break;
136  }
137 
138  next.erase(i.assign_lhs());
139 
140  if(care)
141  {
142  gather_rvalues(i.assign_rhs(), next);
143  }
144  }
145 }
146 
148 {
149  if(expr.id() == ID_symbol ||
150  expr.id() == ID_index ||
151  expr.id() == ID_member ||
152  expr.id() == ID_dereference)
153  {
154  rvals.insert(expr);
155  }
156  else
157  {
158  forall_operands(it, expr)
159  {
160  gather_rvalues(*it, rvals);
161  }
162  }
163 }
const goto_programt & program
void get_succs(goto_programt::instructionst::const_reverse_iterator rit, expr_sett &targets)
const namespacet ns
void cone_of_influence(const expr_sett &targets, expr_sett &cone)
void gather_rvalues(const exprt &expr, expr_sett &rvals)
Base class for all expressions.
Definition: expr.h:54
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
const irep_idt & id() const
Definition: irep.h:396
Loop Acceleration.
std::unordered_set< exprt, irep_hash > expr_sett
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4011
#define forall_operands(it, expr)
Definition: expr.h:18