CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
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();
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
53
54 auto next = p_call_site->step(
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(
75 p_call,
79 no_caller_history, // Not needed as p_call already has the info
80 ns,
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...
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
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?
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(
125 *(storage->abstract_traces_before(l_return_site)),
126 p_call_site); // Because it is a return edge!
128 {
129 log.progress() << "blocked by history" << messaget::eom;
130 continue; // Can't return -- no need to merge
131 }
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!
143
144 const std::unique_ptr<statet> ptr_s_callee_end_copy(
146 auto tmp =
147 dynamic_cast<variable_sensitivity_domaint *>(&(*ptr_s_callee_end_copy));
148 INVARIANT(tmp != nullptr, "Three-way merge requires domain support");
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(
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(
166 auto tmp2 =
167 dynamic_cast<variable_sensitivity_domaint *>(&(*ptr_call_site_working));
168 INVARIANT(tmp2 != nullptr, "Three-way merge requires domain support");
170
171 log.progress() << "three way merge... ";
172 s_call_site_working.merge_three_way_function_return(
174
175 log.progress() << "merging... ";
176 if(
179 !s_working.is_bottom()))
180 {
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}
goto_programt::const_targett locationt
Definition ai.h:124
std::unique_ptr< ai_storage_baset > storage
Definition ai.h:511
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
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const
Returns all of the histories that have reached the start of the instruction.
Definition ai.h:194
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
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
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
ai_history_baset::trace_ptrt trace_ptrt
Definition ai.h:121
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
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition ai.h:414
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
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
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.
unsigned get_verbosity() const
Definition message.h:53
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
@ 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:91
double log(double x)
Definition math.c:2449
#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.