cprover
cone_of_influence.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: 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_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
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