cprover
Loading...
Searching...
No Matches
three_way_merge_abstract_interpreter.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Variable sensitivity domain
4
5Author: Martin Brain, martin.brain@cs.ox.ac.uk
6
7Date: August 2020
8
9\*******************************************************************/
10
21
24
26 const irep_idt &calling_function_id,
27 trace_ptrt p_call,
28 locationt l_return,
29 const irep_idt &callee_function_id,
30 working_sett &working_set,
31 const goto_programt &callee,
32 const goto_functionst &goto_functions,
33 const namespacet &ns)
34{
35 // There are four locations that matter.
36 locationt l_call_site = p_call->current_location();
37 locationt l_callee_start = callee.instructions.begin();
38 locationt l_callee_end = --callee.instructions.end();
39 locationt l_return_site = l_return;
40
41 PRECONDITION(l_call_site->is_function_call());
43 l_callee_end->is_end_function(),
44 "The last instruction of a goto_program must be END_FUNCTION");
45
47 log.progress() << "ai_three_way_merget::visit_edge_function_call"
48 << " from " << l_call_site->location_number << " to "
49 << l_callee_start->location_number << messaget::eom;
50
51 // Histories for call_site and callee_start are easy
52 trace_ptrt p_call_site = p_call;
53
54 auto next = p_call_site->step(
55 l_callee_start,
56 *(storage->abstract_traces_before(l_callee_start)),
59 {
60 // Unexpected...
61 // We can't three-way merge without a callee start so
62 log.progress() << "Blocked by history step!" << messaget::eom;
63 return false;
64 }
65 trace_ptrt p_callee_start = next.second;
66
67 // Handle the function call recursively
68 {
69 working_sett catch_working_set; // The starting trace for the next fixpoint
70
71 // Do the edge from the call site to the beginning of the function
72 // (This will compute p_callee_start but that is OK)
73 bool new_data = visit_edge(
74 calling_function_id,
75 p_call,
76 callee_function_id,
77 l_callee_start,
79 no_caller_history, // Not needed as p_call already has the info
80 ns,
81 catch_working_set);
82
83 log.progress() << "Handle " << callee_function_id << " recursively"
85
86 // do we need to do/re-do the fixedpoint of the body?
87 if(new_data)
89 get_next(catch_working_set), // Should be p_callee_start...
90 callee_function_id,
91 callee,
92 goto_functions,
93 ns);
94 }
95
96 // Now we can give histories for the return part
97 log.progress() << "Handle return edges" << messaget::eom;
98
99 // Find the histories at the end of the function
100 auto traces = storage->abstract_traces_before(l_callee_end);
101
102 bool new_data = false; // Whether we have changed a domain in the caller
103
104 // As with recursive-interprocedural, there are potentially multiple histories
105 // at the end, or maybe none. Only some of these will be 'descendents' of
106 // p_call_site and p_callee_start
107 for(auto p_callee_end : *traces)
108 {
109 log.progress() << "ai_three_way_merget::visit_edge_function_call edge from "
110 << l_callee_end->location_number << " to "
111 << l_return_site->location_number << "... ";
112
113 // First off, is it even reachable?
114 const statet &s_callee_end = get_state(p_callee_end);
115
116 if(s_callee_end.is_bottom())
117 {
118 log.progress() << "unreachable on this trace" << messaget::eom;
119 continue; // Unreachable in callee -- no need to merge
120 }
121
122 // Can it return to p_call_site?
123 auto return_step = p_callee_end->step(
124 l_return_site,
125 *(storage->abstract_traces_before(l_return_site)),
126 p_call_site); // Because it is a return edge!
127 if(return_step.first == ai_history_baset::step_statust::BLOCKED)
128 {
129 log.progress() << "blocked by history" << messaget::eom;
130 continue; // Can't return -- no need to merge
131 }
132 else if(return_step.first == ai_history_baset::step_statust::NEW)
133 {
134 log.progress() << "gives a new history... ";
135 }
136 else
137 {
138 log.progress() << "merges with existing history... ";
139 }
140
141 // The fourth history!
142 trace_ptrt p_return_site = return_step.second;
143
144 const std::unique_ptr<statet> ptr_s_callee_end_copy(
145 make_temporary_state(s_callee_end));
146 auto tmp =
147 dynamic_cast<variable_sensitivity_domaint *>(&(*ptr_s_callee_end_copy));
148 INVARIANT(tmp != nullptr, "Three-way merge requires domain support");
149 variable_sensitivity_domaint &s_working = *tmp;
150
151 // Apply transformer
152 // This is for an end_function instruction which normally doesn't do much
153 // but in VSD it does, so this cannot be omitted.
154 log.progress() << "applying transformer... ";
155 s_working.transform(
156 callee_function_id,
157 p_callee_end,
158 calling_function_id,
159 p_return_site,
160 *this,
161 ns);
162
163 // The base for the three way merge is the call site
164 const std::unique_ptr<statet> ptr_call_site_working(
165 make_temporary_state(get_state(p_call_site)));
166 auto tmp2 =
167 dynamic_cast<variable_sensitivity_domaint *>(&(*ptr_call_site_working));
168 INVARIANT(tmp2 != nullptr, "Three-way merge requires domain support");
169 variable_sensitivity_domaint &s_call_site_working = *tmp2;
170
171 log.progress() << "three way merge... ";
172 s_call_site_working.merge_three_way_function_return(
173 get_state(p_callee_start), s_working, ns);
174
175 log.progress() << "merging... ";
176 if(
177 merge(s_call_site_working, p_callee_end, p_return_site) ||
178 (return_step.first == ai_history_baset::step_statust::NEW &&
179 !s_working.is_bottom()))
180 {
181 put_in_working_set(working_set, p_return_site);
182 log.progress() << "result queued." << messaget::eom;
183 new_data = true;
184 }
185 else
186 {
187 log.progress() << "domain unchanged." << messaget::eom;
188 }
189
190 // Branch because printing some histories and domains can be expensive
191 // esp. if the output is then just discarded and this is a critical path.
193 {
194 log.debug() << "p_callee_end = ";
195 p_callee_end->output(log.debug());
196 log.debug() << messaget::eom;
197
198 log.debug() << "s_callee_end = ";
199 s_callee_end.output(log.debug(), *this, ns);
200 log.debug() << messaget::eom;
201
202 log.debug() << "p_return_site = ";
203 p_return_site->output(log.debug());
204 log.debug() << messaget::eom;
205
206 log.debug() << "s_working = ";
207 s_working.output(log.debug(), *this, ns);
208 log.debug() << messaget::eom;
209 }
210 }
211
212 return new_data;
213}
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition ai.h:414
ai_history_baset::trace_ptrt trace_ptrt
Definition ai.h:121
std::unique_ptr< ai_storage_baset > storage
Definition ai.h:511
goto_programt::const_targett locationt
Definition ai.h:124
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
Definition ai.h:515
bool visit_edge(const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set)
Definition ai.cpp:328
message_handlert & message_handler
Definition ai.h:521
virtual bool fixedpoint(trace_ptrt starting_trace, const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Run the fixedpoint algorithm until it reaches a fixed point.
Definition ai.cpp:229
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
Definition ai.h:505
void put_in_working_set(working_sett &working_set, trace_ptrt t)
Definition ai.h:419
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
Definition ai.cpp:211
virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)
Merge the state src, flowing from tracet from to tracet to, into the state currently stored for trace...
Definition ai.h:498
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:54
virtual bool is_bottom() const =0
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const
Definition ai_domain.h:104
A history object is an abstraction / representation of the control-flow part of a set of traces.
Definition ai_history.h:37
static const trace_ptrt no_caller_history
Definition ai_history.h:121
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const =0
Returns all of the histories that have reached the start of the instruction.
bool visit_edge_function_call(const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
unsigned get_verbosity() const
Definition message.h:53
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & debug() const
Definition message.h:421
mstreamt & progress() const
Definition message.h:416
@ M_DEBUG
Definition message.h:170
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) override
Compute the abstract transformer for a single instruction.
virtual void merge_three_way_function_return(const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
Merges just the things that have changes between "function_start" and "function_end" into "this".
bool is_bottom() const override
Find out if the domain is currently unreachable.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
There are different ways of handling arrays, structures, unions and pointers.