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()!=irep_idt() &&
79  arguments.size()>count)
80  {
81  exprt a=arguments[count];
82  if(a.type()!=p.type())
83  a=typecast_exprt(a, p.type());
84  symbol_exprt s(p.get_identifier(), p.type());
85  result.insert(s, 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  const auto &call=to_code_function_call(it->code);
107 
108  if(call.function().id()==ID_symbol)
109  {
110  auto preconditions=
111  get_preconditions(to_symbol_expr(call.function()),
112  goto_model.goto_functions);
113 
114  source_locationt source_location=it->source_location;
115  irep_idt function=it->function;
116 
118 
119  // add before the call, with location of the call
120  for(const auto &p : preconditions)
121  {
122  goto_program.insert_before_swap(it);
123  exprt instance=p->guard;
124  r(instance);
125  it->make_assertion(instance);
126  it->function=function;
127  it->source_location=source_location;
128  it->source_location.set_property_class(ID_precondition_instance);
129  it->source_location.set_comment(p->source_location.get_comment());
130  it++;
131  }
132  }
133  }
134  }
135 }
136 
138 {
139  // add at call site
140  for(auto &f_it : goto_model.goto_functions.function_map)
142  goto_model,
143  f_it.second.body);
144 
145  // now remove the preconditions
146  for(auto &f_it : goto_model.goto_functions.function_map)
147  remove_preconditions(f_it.second.body);
148 }
149 
151 {
152  remove_preconditions(goto_function.body);
153 }
154 
156 {
157  for(auto &f_it : goto_model.goto_functions.function_map)
158  remove_preconditions(f_it.second);
159 }
Semantic type conversion.
Definition: std_expr.h:2277
static int8_t r
Definition: irep_hash.h:59
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...
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
void set_property_class(const irep_idt &property_class)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
goto_programt body
Definition: goto_function.h:29
function_mapt function_map
void remove_preconditions(goto_programt &goto_program)
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
const irep_idt & id() const
Definition: irep.h:259
argumentst & arguments()
Definition: std_code.h:1109
Replace expression or type symbols by an expression or type, respectively.
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
size_t size() const
Definition: dstring.h:91
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
exprt & function()
Definition: std_code.h:1099
Base class for all expressions.
Definition: expr.h:54
Expression to hold a symbol (variable)
Definition: std_expr.h:143
dstringt irep_idt
Definition: irep.h:32
std::vector< goto_programt::const_targett > get_preconditions(const symbol_exprt &function, const goto_functionst &goto_functions)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
replace_symbolt actuals_replace_map(const code_function_callt &call, const namespacet &ns)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173