cprover
instrument_preconditions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Move preconditions of a function
4  to the call-site of the function
5 
6 Author: Daniel Kroening
7 
8 Date: September 2017
9 
10 \*******************************************************************/
11 
13 
14 #include <util/replace_symbol.h>
15 
16 #include "goto_model.h"
17 
18 std::vector<goto_programt::const_targett> get_preconditions(
19  const symbol_exprt &function,
20  const goto_functionst &goto_functions)
21 {
22  const irep_idt &identifier=function.get_identifier();
23 
24  auto f_it=goto_functions.function_map.find(identifier);
25  if(f_it==goto_functions.function_map.end())
26  return {};
27 
28  const auto &body=f_it->second.body;
29 
30  std::vector<goto_programt::const_targett> result;
31 
32  for(auto i_it=body.instructions.begin();
33  i_it!=body.instructions.end();
34  i_it++)
35  {
36  if(i_it->is_location() ||
37  i_it->is_skip())
38  continue; // ignore
39 
40  if(i_it->is_assert() &&
41  i_it->source_location.get_property_class()==ID_precondition)
42  result.push_back(i_it);
43  else
44  break; // preconditions must be at the front
45  }
46 
47  return result;
48 }
49 
51 {
52  for(auto &instruction : goto_program.instructions)
53  {
54  if(instruction.is_location() ||
55  instruction.is_skip())
56  continue; // ignore
57 
58  if(instruction.is_assert() &&
59  instruction.source_location.get_property_class()==ID_precondition)
60  instruction.type=LOCATION;
61  else
62  break; // preconditions must be at the front
63  }
64 }
65 
67  const exprt &lhs,
68  const exprt &function,
69  const exprt::operandst &arguments,
70  const namespacet &ns)
71 {
72  PRECONDITION(function.id() == ID_symbol);
73  const symbolt &s = ns.lookup(to_symbol_expr(function));
74  const auto &code_type=to_code_type(s.type);
75  const auto &parameters=code_type.parameters();
76 
77  replace_symbolt result;
78  std::size_t count=0;
79  for(const auto &p : parameters)
80  {
81  if(!p.get_identifier().empty() && arguments.size() > count)
82  {
83  const exprt a =
84  typecast_exprt::conditional_cast(arguments[count], p.type());
85  result.insert(symbol_exprt(p.get_identifier(), p.type()), a);
86  }
87  count++;
88  }
89 
90  return result;
91 }
92 
94  const goto_modelt &goto_model,
95  goto_programt &goto_program)
96 {
97  const namespacet ns(goto_model.symbol_table);
98 
99  for(auto it=goto_program.instructions.begin();
100  it!=goto_program.instructions.end();
101  it++)
102  {
103  if(it->is_function_call())
104  {
105  // does the function we call have preconditions?
106  if(as_const(*it).call_function().id() == ID_symbol)
107  {
108  auto preconditions = get_preconditions(
109  to_symbol_expr(as_const(*it).call_function()),
110  goto_model.goto_functions);
111 
112  source_locationt source_location=it->source_location;
113 
115  as_const(*it).call_lhs(),
116  as_const(*it).call_function(),
117  as_const(*it).call_arguments(),
118  ns);
119 
120  // add before the call, with location of the call
121  for(const auto &p : preconditions)
122  {
123  goto_program.insert_before_swap(it);
124  exprt instance = p->get_condition();
125  r(instance);
126  *it = goto_programt::make_assertion(instance, source_location);
127  it->source_location.set_property_class(ID_precondition_instance);
128  it->source_location.set_comment(p->source_location.get_comment());
129  it++;
130  }
131  }
132  }
133  }
134 }
135 
137 {
138  // add at call site
139  for(auto &f_it : goto_model.goto_functions.function_map)
141  goto_model,
142  f_it.second.body);
143 
144  // now remove the preconditions
145  for(auto &f_it : goto_model.goto_functions.function_map)
146  remove_preconditions(f_it.second.body);
147  // The above may leave some locations uninitialized, this update is a
148  // sanity to check to ensure the goto model and functions are correct
149  // for later passes.
150  // Note that only the first loop is the one known to leave locations
151  // uninitialized.
152  goto_model.goto_functions.update();
153 }
154 
156 {
157  remove_preconditions(goto_function.body);
158 }
159 
161 {
162  for(auto &f_it : goto_model.goto_functions.function_map)
163  remove_preconditions(f_it.second);
164 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functiont::body
goto_programt body
Definition: goto_function.h:26
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
instrument_preconditions.h
replace_symbol.h
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
get_preconditions
std::vector< goto_programt::const_targett > get_preconditions(const symbol_exprt &function, const goto_functionst &goto_functions)
Definition: instrument_preconditions.cpp:18
instrument_preconditions
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Definition: instrument_preconditions.cpp:93
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
replace_symbolt::insert
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
Definition: replace_symbol.cpp:24
source_locationt
Definition: source_location.h:19
remove_preconditions
void remove_preconditions(goto_programt &goto_program)
Definition: instrument_preconditions.cpp:50
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_functionst::update
void update()
Definition: goto_functions.h:83
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
r
static int8_t r
Definition: irep_hash.h:60
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:673
LOCATION
@ LOCATION
Definition: goto_program.h:39
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25
actuals_replace_map
replace_symbolt actuals_replace_map(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, const namespacet &ns)
Definition: instrument_preconditions.cpp:66