CBMC
three_way_merge_abstract_interpreter.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Variable sensitivity domain
4 
5 Author: Martin Brain, martin.brain@cs.ox.ac.uk
6 
7 Date: 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"
84  << messaget::eom;
85 
86  // do we need to do/re-do the fixedpoint of the body?
87  if(new_data)
88  fixedpoint(
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.
192  if(message_handler.get_verbosity() >= messaget::message_levelt::M_DEBUG)
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
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 std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
Definition: ai.h:505
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
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
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
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
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.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
unsigned get_verbosity() const
Definition: message.h:54
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static eomt eom
Definition: message.h:297
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.
double log(double x)
Definition: math.c:2776
#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
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
There are different ways of handling arrays, structures, unions and pointers.