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 std::vector<goto_programt::const_targett> get_preconditions(
17  const symbol_exprt &function,
18  const goto_functionst &goto_functions)
19 {
20  const irep_idt &identifier=function.get_identifier();
21 
22  auto f_it=goto_functions.function_map.find(identifier);
23  if(f_it==goto_functions.function_map.end())
24  return {};
25 
26  const auto &body=f_it->second.body;
27 
28  std::vector<goto_programt::const_targett> result;
29 
30  for(auto i_it=body.instructions.begin();
31  i_it!=body.instructions.end();
32  i_it++)
33  {
34  if(i_it->is_location() ||
35  i_it->is_skip())
36  continue; // ignore
37 
38  if(i_it->is_assert() &&
39  i_it->source_location.get_property_class()==ID_precondition)
40  result.push_back(i_it);
41  else
42  break; // preconditions must be at the front
43  }
44 
45  return result;
46 }
47 
49 {
50  for(auto &instruction : goto_program.instructions)
51  {
52  if(instruction.is_location() ||
53  instruction.is_skip())
54  continue; // ignore
55 
56  if(instruction.is_assert() &&
57  instruction.source_location.get_property_class()==ID_precondition)
58  instruction.type=LOCATION;
59  else
60  break; // preconditions must be at the front
61  }
62 }
63 
65  const code_function_callt &call,
66  const namespacet &ns)
67 {
68  PRECONDITION(call.function().id()==ID_symbol);
69  const symbolt &s=ns.lookup(to_symbol_expr(call.function()));
70  const auto &code_type=to_code_type(s.type);
71  const auto &parameters=code_type.parameters();
72  const auto &arguments=call.arguments();
73 
74  replace_symbolt result;
75  std::size_t count=0;
76  for(const auto &p : parameters)
77  {
78  if(!p.get_identifier().empty() && arguments.size() > count)
79  {
80  const exprt a =
81  typecast_exprt::conditional_cast(arguments[count], p.type());
82  result.insert(symbol_exprt(p.get_identifier(), p.type()), a);
83  }
84  count++;
85  }
86 
87  return result;
88 }
89 
91  const goto_modelt &goto_model,
92  goto_programt &goto_program)
93 {
94  const namespacet ns(goto_model.symbol_table);
95 
96  for(auto it=goto_program.instructions.begin();
97  it!=goto_program.instructions.end();
98  it++)
99  {
100  if(it->is_function_call())
101  {
102  // does the function we call have preconditions?
103  const auto &call = it->get_function_call();
104 
105  if(call.function().id()==ID_symbol)
106  {
107  auto preconditions=
108  get_preconditions(to_symbol_expr(call.function()),
109  goto_model.goto_functions);
110 
111  source_locationt source_location=it->source_location;
112 
114 
115  // add before the call, with location of the call
116  for(const auto &p : preconditions)
117  {
118  goto_program.insert_before_swap(it);
119  exprt instance = p->get_condition();
120  r(instance);
121  *it = goto_programt::make_assertion(instance, source_location);
122  it->source_location.set_property_class(ID_precondition_instance);
123  it->source_location.set_comment(p->source_location.get_comment());
124  it++;
125  }
126  }
127  }
128  }
129 }
130 
132 {
133  // add at call site
134  for(auto &f_it : goto_model.goto_functions.function_map)
136  goto_model,
137  f_it.second.body);
138 
139  // now remove the preconditions
140  for(auto &f_it : goto_model.goto_functions.function_map)
141  remove_preconditions(f_it.second.body);
142 }
143 
145 {
146  remove_preconditions(goto_function.body);
147 }
148 
150 {
151  for(auto &f_it : goto_model.goto_functions.function_map)
152  remove_preconditions(f_it.second);
153 }
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:30
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
instrument_preconditions.h
replace_symbol.h
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
get_preconditions
std::vector< goto_programt::const_targett > get_preconditions(const symbol_exprt &function, const goto_functionst &goto_functions)
Definition: instrument_preconditions.cpp:16
instrument_preconditions
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
Definition: instrument_preconditions.cpp:90
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
actuals_replace_map
replace_symbolt actuals_replace_map(const code_function_callt &call, const namespacet &ns)
Definition: instrument_preconditions.cpp:64
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
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
source_locationt
Definition: source_location.h:20
remove_preconditions
void remove_preconditions(goto_programt &goto_program)
Definition: instrument_preconditions.cpp:48
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
r
static int8_t r
Definition: irep_hash.h:59
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
LOCATION
@ LOCATION
Definition: goto_program.h:41
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25