cprover
assigns.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Specify write set in function contracts.
4 
5 Author: Felipe R. Monteiro
6 
7 Date: July 2021
8 
9 \*******************************************************************/
10 
13 
14 #include "assigns.h"
15 
17 
18 #include <util/arith_tools.h>
19 #include <util/c_types.h>
21 
23  const exprt &object,
24  code_contractst &contract,
25  messaget &log_parameter,
26  const irep_idt &function_id)
27  : pointer_object(pointer_for(object)),
28  contract(contract),
29  init_block(),
30  log(log_parameter),
31  target(typet()),
32  target_id(object.id())
33 {
34  INVARIANT(
35  pointer_object.type().id() == ID_pointer,
36  "Assigns clause targets should be stored as pointer expressions.");
37  const symbolt &function_symbol = contract.ns.lookup(function_id);
38 
39  // Declare a new symbol to stand in for the reference
40  symbolt standin_symbol = contract.new_tmp_symbol(
42  function_symbol.location,
43  function_symbol.mode);
44 
45  target = standin_symbol.symbol_expr();
46 
47  // Build standin variable initialization block
50  code_assignt(target, pointer_object), function_symbol.location));
51 }
52 
54 {
55 }
56 
57 std::vector<symbol_exprt> assigns_clause_targett::temporary_declarations() const
58 {
59  std::vector<symbol_exprt> result;
60  result.push_back(target);
61  return result;
62 }
63 
65 {
66  exprt::operandst condition;
67  exprt lhs_ptr = (lhs.id() == ID_address_of) ? to_address_of_expr(lhs).object()
68  : pointer_for(lhs);
69 
70  // __CPROVER_same_object(lhs, target)
71  condition.push_back(same_object(lhs_ptr, target));
72 
73  // If assigns target was a dereference, comparing objects is enough
74  if(target_id == ID_dereference)
75  {
76  return conjunction(condition);
77  }
78 
79  const exprt lhs_offset = pointer_offset(lhs_ptr);
80  const exprt target_offset = pointer_offset(target);
81 
82  // __CPROVER_offset(lhs) >= __CPROVER_offset(target)
83  condition.push_back(binary_relation_exprt(lhs_offset, ID_ge, target_offset));
84 
85  const exprt region_lhs = plus_exprt(
87  size_of_expr(lhs.type(), contract.ns).value(), lhs_offset.type()),
88  lhs_offset);
89 
90  const exprt region_target = plus_exprt(
93  target_offset.type()),
94  target_offset);
95 
96  // (sizeof(lhs) + __CPROVER_offset(lhs)) <=
97  // (sizeof(target) + __CPROVER_offset(target))
98  condition.push_back(binary_relation_exprt(region_lhs, ID_le, region_target));
99 
100  return conjunction(condition);
101 }
102 
104  const assigns_clause_targett &called_target)
105 {
106  return same_object(called_target.get_direct_pointer(), target);
107 }
108 
110 {
111  return pointer_object;
112 }
113 
115 {
116  return init_block;
117 }
118 
120  const exprt &assigns,
121  code_contractst &contract,
122  const irep_idt function_id,
123  messaget log_parameter)
124  : assigns(assigns),
125  parent(contract),
126  function_id(function_id),
127  log(log_parameter)
128 {
129  for(exprt target : assigns.operands())
130  {
131  add_target(target);
132  }
133 }
134 
136 {
137  for(assigns_clause_targett *target : targets)
138  {
139  delete target;
140  }
141 }
142 
144 {
146  (target.id() == ID_address_of)
147  ? to_index_expr(to_address_of_expr(target).object()).array()
148  : target,
149  parent,
150  log,
151  function_id);
152  targets.push_back(new_target);
153  return new_target;
154 }
155 
157 {
158  goto_programt result;
159  for(assigns_clause_targett *target : targets)
160  {
161  for(goto_programt::instructiont inst :
162  target->get_init_block().instructions)
163  {
164  result.add(goto_programt::instructiont(inst));
165  }
166  }
167  return result;
168 }
169 
171 {
172  goto_programt dead_statements;
173  for(assigns_clause_targett *target : targets)
174  {
175  for(symbol_exprt symbol : target->temporary_declarations())
176  {
177  dead_statements.add(
178  goto_programt::make_dead(symbol, symbol.source_location()));
179  }
180  }
181  return dead_statements;
182 }
183 
185 {
186  modifiest modifies;
187  for(const auto &t : targets)
188  modifies.insert(to_address_of_expr(t->get_direct_pointer()).object());
189 
190  goto_programt havoc_statements;
191  append_havoc_code(assigns.source_location(), modifies, havoc_statements);
192  return havoc_statements;
193 }
194 
196 {
197  // If write set is empty, no assignment is allowed.
198  if(targets.empty())
199  {
200  return false_exprt();
201  }
202 
203  exprt::operandst condition;
204  for(assigns_clause_targett *target : targets)
205  {
206  condition.push_back(target->alias_expression(lhs));
207  }
208  return disjunction(condition);
209 }
210 
212  const assigns_clauset &called_assigns)
213 {
214  if(called_assigns.targets.empty())
215  {
216  return true_exprt();
217  }
218 
219  bool first_clause = true;
220  exprt result = true_exprt();
221  for(assigns_clause_targett *called_target : called_assigns.targets)
222  {
223  bool first_iter = true;
224  exprt current_target_compatible = false_exprt();
225  for(assigns_clause_targett *target : targets)
226  {
227  if(first_iter)
228  {
229  // TODO: Optimize the validation below and remove code duplication
230  // See GitHub issue #6105 for further details
231 
232  // Validating the called target through __CPROVER_w_ok() is
233  // only useful when the called target is a dereference
234  const auto &called_target_ptr = called_target->get_direct_pointer();
235  if(
236  to_address_of_expr(called_target_ptr).object().id() == ID_dereference)
237  {
238  // or_exprt is short-circuited, therefore
239  // target->compatible_expression(*called_target) would not be
240  // checked on invalid called_targets.
241  current_target_compatible = or_exprt(
243  called_target_ptr, from_integer(0, unsigned_int_type()))),
244  target->compatible_expression(*called_target));
245  }
246  else
247  {
248  current_target_compatible =
249  target->compatible_expression(*called_target);
250  }
251  first_iter = false;
252  }
253  else
254  {
255  current_target_compatible = or_exprt(
256  current_target_compatible,
257  target->compatible_expression(*called_target));
258  }
259  }
260  if(first_clause)
261  {
262  result = current_target_compatible;
263  first_clause = false;
264  }
265  else
266  {
267  exprt::operandst conjuncts;
268  conjuncts.push_back(result);
269  conjuncts.push_back(current_target_compatible);
270  result = conjunction(conjuncts);
271  }
272  }
273 
274  return result;
275 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Specify write set in function contracts.
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
exprt & object()
Definition: pointer_expr.h:350
A base class for assigns clause targets.
Definition: assigns.h:23
assigns_clause_targett(const exprt &object, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
Definition: assigns.cpp:22
symbol_exprt target
Definition: assigns.h:48
exprt alias_expression(const exprt &lhs)
Definition: assigns.cpp:64
const exprt & get_direct_pointer() const
Definition: assigns.cpp:109
std::vector< symbol_exprt > temporary_declarations() const
Definition: assigns.cpp:57
const exprt pointer_object
Definition: assigns.h:44
goto_programt init_block
Definition: assigns.h:46
exprt compatible_expression(const assigns_clause_targett &called_target)
Definition: assigns.cpp:103
const irep_idt & target_id
Definition: assigns.h:49
goto_programt & get_init_block()
Definition: assigns.cpp:114
const code_contractst & contract
Definition: assigns.h:45
static exprt pointer_for(const exprt &object)
Definition: assigns.h:38
goto_programt havoc_code()
Definition: assigns.cpp:184
exprt alias_expression(const exprt &lhs)
Definition: assigns.cpp:195
code_contractst & parent
Definition: assigns.h:75
goto_programt init_block()
Definition: assigns.cpp:156
const exprt & assigns
Definition: assigns.h:70
const irep_idt function_id
Definition: assigns.h:76
assigns_clause_targett * add_target(exprt target)
Definition: assigns.cpp:143
exprt compatible_expression(const assigns_clauset &called_assigns)
Definition: assigns.cpp:211
messaget log
Definition: assigns.h:77
std::vector< assigns_clause_targett * > targets
Definition: assigns.h:72
goto_programt dead_stmts()
Definition: assigns.cpp:170
assigns_clauset(const exprt &assigns, code_contractst &contract, const irep_idt function_id, messaget log_parameter)
Definition: assigns.cpp:119
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
A codet representing an assignment in the program.
Definition: std_code.h:293
namespacet ns
Definition: contracts.h:134
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &mode)
Definition: contracts.cpp:645
Operator to dereference a pointer.
Definition: pointer_expr.h:628
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2811
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:985
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:978
const irep_idt & id() const
Definition: irep.h:407
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Boolean negation.
Definition: std_expr.h:2127
Boolean OR.
Definition: std_expr.h:2028
The plus expression Associativity is not specified.
Definition: std_expr.h:914
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Symbol table entry.
Definition: symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2802
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:761
void append_havoc_code(const source_locationt source_location, const modifiest &modifies, goto_programt &dest)
Definition: havoc_utils.cpp:73
Utilities for building havoc code for expressions.
std::set< exprt > modifiest
Definition: havoc_utils.h:23
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:34
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382