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 
14 #include <iostream>
15 
16 #include <ansi-c/expr2c.h>
17 
19  const expr_sett &targets,
20  expr_sett &cone)
21 {
22  if(program.instructions.empty())
23  {
24  cone=targets;
25  return;
26  }
27 
28  for(goto_programt::instructionst::const_reverse_iterator
29  rit=program.instructions.rbegin();
30  rit != program.instructions.rend();
31  ++rit)
32  {
33  expr_sett curr; // =targets;
34  expr_sett next;
35 
36  if(rit == program.instructions.rbegin())
37  {
38  curr=targets;
39  }
40  else
41  {
42  get_succs(rit, curr);
43  }
44 
45  cone_of_influence(*rit, curr, next);
46 
47  cone_map[rit->location_number]=next;
48 
49 #ifdef DEBUG
50  std::cout << "Previous cone: \n";
51 
52  for(const auto &expr : curr)
53  std::cout << expr2c(expr, ns) << " ";
54 
55  std::cout << "\nCurrent cone: \n";
56 
57  for(const auto &expr : next)
58  std::cout << expr2c(expr, ns) << " ";
59 
60  std::cout << '\n';
61 #endif
62  }
63 
64  cone=cone_map[program.instructions.front().location_number];
65 }
66 
68  const exprt &target,
69  expr_sett &cone)
70 {
71  expr_sett s;
72  s.insert(target);
73  cone_of_influence(s, cone);
74 }
75 
77  goto_programt::instructionst::const_reverse_iterator rit,
78  expr_sett &targets)
79 {
80  if(rit == program.instructions.rbegin())
81  {
82  return;
83  }
84 
85  goto_programt::instructionst::const_reverse_iterator next=rit;
86  --next;
87 
88  if(rit->is_goto())
89  {
90  if(!rit->get_condition().is_false())
91  {
92  // Branch can be taken.
93  for(goto_programt::targetst::const_iterator t=rit->targets.begin();
94  t != rit->targets.end();
95  ++t)
96  {
97  unsigned int loc=(*t)->location_number;
98  expr_sett &s=cone_map[loc];
99  targets.insert(s.begin(), s.end());
100  }
101  }
102 
103  if(rit->get_condition().is_true())
104  {
105  return;
106  }
107  }
108  else if(rit->is_assume() || rit->is_assert())
109  {
110  if(rit->get_condition().is_false())
111  {
112  return;
113  }
114  }
115 
116  unsigned int loc=next->location_number;
117  expr_sett &s=cone_map[loc];
118  targets.insert(s.begin(), s.end());
119 }
120 
123  const expr_sett &curr,
124  expr_sett &next)
125 {
126  next.insert(curr.begin(), curr.end());
127 
128  if(i.is_assign())
129  {
130  const code_assignt &assignment=to_code_assign(i.code);
131  expr_sett lhs_syms;
132  bool care=false;
133 
134  gather_rvalues(assignment.lhs(), lhs_syms);
135 
136  for(const auto &expr : lhs_syms)
137  if(curr.find(expr)!=curr.end())
138  {
139  care=true;
140  break;
141  }
142 
143  next.erase(assignment.lhs());
144 
145  if(care)
146  {
147  gather_rvalues(assignment.rhs(), next);
148  }
149  }
150 }
151 
153 {
154  if(expr.id() == ID_symbol ||
155  expr.id() == ID_index ||
156  expr.id() == ID_member ||
157  expr.id() == ID_dereference)
158  {
159  rvals.insert(expr);
160  }
161  else
162  {
163  forall_operands(it, expr)
164  {
165  gather_rvalues(*it, rvals);
166  }
167  }
168 }
cone_of_influencet::program
const goto_programt & program
Definition: cone_of_influence.h:51
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
cone_of_influencet::cone_of_influence
void cone_of_influence(const expr_sett &targets, expr_sett &cone)
Definition: cone_of_influence.cpp:18
exprt
Base class for all expressions.
Definition: expr.h:53
cone_of_influencet::gather_rvalues
void gather_rvalues(const exprt &expr, expr_sett &rvals)
Definition: cone_of_influence.cpp:152
cone_of_influencet::ns
const namespacet ns
Definition: cone_of_influence.h:52
cone_of_influencet::cone_map
cone_mapt cone_map
Definition: cone_of_influence.h:49
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3878
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: cone_of_influence.h:21
irept::id
const irep_idt & id() const
Definition: irep.h:418
cone_of_influencet::get_succs
void get_succs(goto_programt::instructionst::const_reverse_iterator rit, expr_sett &targets)
Definition: cone_of_influence.cpp:76
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
cone_of_influence.h
Loop Acceleration.
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:460
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179