cprover
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 
46  // Histories for call_site and callee_start are easy
47  trace_ptrt p_call_site = p_call;
48 
49  auto next = p_call_site->step(
50  l_callee_start,
51  *(storage->abstract_traces_before(l_callee_start)),
54  {
55  // Unexpected...
56  // We can't three-way merge without a callee start so
57  return false;
58  }
59  trace_ptrt p_callee_start = next.second;
60 
61  // Handle the function call recursively
62  {
63  working_sett catch_working_set; // The starting trace for the next fixpoint
64 
65  // Do the edge from the call site to the beginning of the function
66  // (This will compute p_callee_start but that is OK)
67  bool new_data = visit_edge(
68  calling_function_id,
69  p_call,
70  callee_function_id,
71  l_callee_start,
73  no_caller_history, // Not needed as p_call already has the info
74  ns,
75  catch_working_set);
76 
77  // do we need to do/re-do the fixedpoint of the body?
78  if(new_data)
79  fixedpoint(
80  get_next(catch_working_set), // Should be p_callee_start...
81  callee_function_id,
82  callee,
83  goto_functions,
84  ns);
85  }
86 
87  // Now we can give histories for the return part
88 
89  // Find the histories at the end of the function
90  auto traces = storage->abstract_traces_before(l_callee_end);
91 
92  bool new_data = false; // Whether we have changed a domain in the caller
93 
94  // As with recursive-interprocedural, there are potentially multiple histories
95  // at the end, or maybe none. Only some of these will be 'descendents' of
96  // p_call_site and p_callee_start
97  for(auto p_callee_end : *traces)
98  {
99  // First off, is it even reachable?
100  const statet &s_callee_end = get_state(p_callee_end);
101 
102  if(s_callee_end.is_bottom())
103  continue; // Unreachable in callee -- no need to merge
104 
105  // Can it return to p_call_site?
106  auto return_step = p_callee_end->step(
107  l_return_site,
108  *(storage->abstract_traces_before(l_return_site)),
109  p_call_site); // Because it is a return edge!
110  if(return_step.first == ai_history_baset::step_statust::BLOCKED)
111  continue; // Can't return -- no need to merge
112 
113  // The fourth history!
114  trace_ptrt p_return_site = return_step.second;
115 
116  const std::unique_ptr<statet> ptr_s_callee_end_copy(
117  make_temporary_state(s_callee_end));
118  auto tmp =
119  dynamic_cast<variable_sensitivity_domaint *>(&(*ptr_s_callee_end_copy));
120  INVARIANT(tmp != nullptr, "Three-way merge requires domain support");
121  variable_sensitivity_domaint &s_working = *tmp;
122 
123  // Apply transformer
124  // This is for an end_function instruction which normally doesn't do much
125  // but in VSD it does, so this cannot be omitted.
126  s_working.transform(
127  callee_function_id,
128  p_callee_end,
129  calling_function_id,
130  p_return_site,
131  *this,
132  ns);
133 
134  // TODO : this is probably needed to avoid three_way_merge modifying one of
135  // its arguments as it goes. A better solution would be to refactor
136  // merge_three_way_function_return.
137  const std::unique_ptr<statet> ptr_s_working_copy(
138  make_temporary_state(s_working));
139 
141  get_state(p_call_site),
142  get_state(p_callee_start),
143  *ptr_s_working_copy,
144  ns);
145 
146  if(
147  merge(s_working, p_callee_end, p_return_site) ||
148  (return_step.first == ai_history_baset::step_statust::NEW &&
149  !s_working.is_bottom()))
150  {
151  put_in_working_set(working_set, p_return_site);
152  new_data = true;
153  }
154  }
155 
156  return new_data;
157 }
goto_programt::const_targett locationt
Definition: ai.h:127
std::unique_ptr< ai_storage_baset > storage
Definition: ai.h:512
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:320
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
Definition: ai.h:506
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:225
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai.h:124
void put_in_working_set(working_sett &working_set, trace_ptrt t)
Definition: ai.h:420
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
Definition: ai.cpp:207
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition: ai.h:415
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:499
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:516
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:59
virtual bool is_bottom() const =0
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:37
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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.
bool is_bottom() const override
Find out if the domain is currently unreachable.
virtual void merge_three_way_function_return(const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
Perform a context aware merge of the changes that have been applied between function_start and the cu...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
An abstract interpreter, based on the default recursive-interprocedural that uses variable sensitivit...
There are different ways of handling arrays, structures, unions and pointers.