cprover
write_stack.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Variable Sensitivity Domain
4 
5  Author: DiffBlue Limited.
6 
7 \*******************************************************************/
8 
12 
13 #include "write_stack.h"
14 
15 #include <unordered_set>
16 
17 #include <util/arith_tools.h>
18 #include <util/c_types.h>
19 #include <util/pointer_expr.h>
20 #include <util/std_expr.h>
21 
22 #include "abstract_environment.h"
23 
25 write_stackt::write_stackt() : stack(), top_stack(true)
26 {
27 }
28 
34  const exprt &expr,
35  const abstract_environmentt &environment,
36  const namespacet &ns)
37 {
38  top_stack = false;
39  if(expr.type().id() == ID_array)
40  {
41  // We are assigning an array to a pointer, which is equivalent to assigning
42  // the first element of that array
43  // &(expr)[0]
46  environment,
47  ns);
48  }
49  else
50  {
51  construct_stack_to_pointer(expr, environment, ns);
52  }
53 }
54 
60  const exprt &expr,
61  const abstract_environmentt &environment,
62  const namespacet &ns)
63 {
64  PRECONDITION(expr.type().id() == ID_pointer);
65 
66  if(expr.id() == ID_address_of)
67  {
68  // resovle reminder, can either be a symbol, member or index of
69  // otherwise unsupported
71  to_address_of_expr(expr).object(), environment, ns);
72  }
73  else if(expr.id() == ID_plus || expr.id() == ID_minus)
74  {
75  exprt base;
76  exprt offset;
77  const integral_resultt &which_side =
78  get_which_side_integral(expr, base, offset);
79  INVARIANT(
81  "An offset must be an integral amount");
82 
83  if(expr.id() == ID_minus)
84  {
85  // can't get a valid pointer by subtracting from a constant number
86  if(which_side == integral_resultt::LHS_INTEGRAL)
87  {
88  top_stack = true;
89  return;
90  }
91  offset = unary_minus_exprt(offset);
92  }
93 
94  abstract_object_pointert offset_value = environment.eval(offset, ns);
95 
97  std::make_shared<offset_entryt>(offset_value), environment, ns);
98 
99  // Build the pointer part
100  construct_stack_to_pointer(base, environment, ns);
101 
102  if(!top_stack)
103  {
104  // check the symbol at the bottom of the stack
105  std::shared_ptr<const write_stack_entryt> entry = *stack.cbegin();
106  INVARIANT(
107  entry->get_access_expr().id() == ID_symbol,
108  "The base should be an addressable location (i.e. symbol)");
109 
110  if(entry->get_access_expr().type().id() != ID_array)
111  {
112  top_stack = true;
113  }
114  }
115  }
116  else
117  {
118  // unknown expression type - play it safe and set to top
119  top_stack = true;
120  }
121 }
122 
129  const exprt &expr,
130  const abstract_environmentt &environment,
131  const namespacet &ns)
132 {
133  if(!top_stack)
134  {
135  if(expr.id() == ID_member)
136  {
137  add_to_stack(std::make_shared<simple_entryt>(expr), environment, ns);
139  to_member_expr(expr).struct_op(), environment, ns);
140  }
141  else if(expr.id() == ID_symbol || expr.id() == ID_dynamic_object)
142  {
143  add_to_stack(std::make_shared<simple_entryt>(expr), environment, ns);
144  }
145  else if(expr.id() == ID_index)
146  {
147  construct_stack_to_array_index(to_index_expr(expr), environment, ns);
148  }
149  else
150  {
151  top_stack = true;
152  }
153  }
154 }
155 
161  const index_exprt &index_expr,
162  const abstract_environmentt &environment,
163  const namespacet &ns)
164 {
165  abstract_object_pointert offset_value =
166  environment.eval(index_expr.index(), ns);
167 
168  add_to_stack(std::make_shared<offset_entryt>(offset_value), environment, ns);
169  construct_stack_to_lvalue(index_expr.array(), environment, ns);
170 }
171 
176 {
177  // A top stack is useless and its expression should not be evaluated
179  exprt access_expr = nil_exprt();
180  for(const std::shared_ptr<write_stack_entryt> &entry : stack)
181  {
182  exprt new_expr = entry->get_access_expr();
183  if(access_expr.id() == ID_nil)
184  {
185  access_expr = new_expr;
186  }
187  else
188  {
189  if(new_expr.operands().size() == 0)
190  {
191  new_expr.operands().resize(1);
192  }
193  new_expr.operands()[0] = access_expr;
194 
195  // If necessary, complete the type of the new access expression
196  entry->adjust_access_type(new_expr);
197 
198  access_expr = new_expr;
199  }
200  }
201  address_of_exprt top_expr(access_expr);
202  return std::move(top_expr);
203 }
204 
205 size_t write_stackt::depth() const
206 {
207  return stack.size();
208 }
209 
211 {
213  return stack[depth]->get_access_expr();
214 }
215 
217 {
219  auto const &access = stack.back()->get_access_expr();
220 
221  if(access.id() == ID_member || access.id() == ID_symbol)
222  return access;
223 
224  if(access.id() == ID_index)
225  return to_index_expr(access).index();
226 
228 }
229 
234 {
235  return top_stack;
236 }
237 
244  std::shared_ptr<write_stack_entryt> entry_pointer,
245  const abstract_environmentt environment,
246  const namespacet &ns)
247 {
248  if(
249  stack.empty() ||
250  !stack.front()->try_squash_in(entry_pointer, environment, ns))
251  {
252  stack.insert(stack.begin(), entry_pointer);
253  }
254 }
255 
264  const exprt &expr,
265  exprt &out_base_expr,
266  exprt &out_integral_expr)
267 {
268  PRECONDITION(expr.operands().size() == 2);
269  const auto binary_e = to_binary_expr(expr);
270  static const std::unordered_set<irep_idt, irep_id_hash> integral_types = {
271  ID_signedbv, ID_unsignedbv, ID_integer};
272  if(integral_types.find(binary_e.lhs().type().id()) != integral_types.cend())
273  {
274  out_integral_expr = binary_e.lhs();
275  out_base_expr = binary_e.rhs();
277  }
278  else if(
279  integral_types.find(binary_e.rhs().type().id()) != integral_types.cend())
280  {
281  out_integral_expr = binary_e.rhs();
282  out_base_expr = binary_e.lhs();
284  }
285  else
286  {
287  out_integral_expr.make_nil();
288  out_base_expr.make_nil();
290  }
291 }
An abstract version of a program environment.
sharing_ptrt< class abstract_objectt > abstract_object_pointert
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
unsignedbv_typet unsigned_long_int_type()
Definition: c_types.cpp:94
signedbv_typet signed_size_type()
Definition: c_types.cpp:74
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
Operator to return the address of an object.
Definition: pointer_expr.h:341
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1344
exprt & index()
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:465
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2820
The unary minus expression.
Definition: std_expr.h:390
bool top_stack
Definition: write_stack.h:72
void construct_stack_to_array_index(const index_exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Construct a stack for an array position l-value.
exprt target_expression(size_t depth) const
exprt offset_expression() const
static integral_resultt get_which_side_integral(const exprt &expr, exprt &out_base_expr, exprt &out_integral_expr)
Utility function to find out which side of a binary operation has an integral type,...
void construct_stack_to_lvalue(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Construct a stack up to a specific l-value (i.e.
write_stackt()
Build a topstack.
Definition: write_stack.cpp:25
bool is_top_value() const
Is the stack representing an unknown value and hence can't be written to or read from.
exprt to_expression() const
Convert the stack to an expression that can be used to write to.
void construct_stack_to_pointer(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Add to the stack the elements to get to a pointer.
Definition: write_stack.cpp:59
size_t depth() const
continuation_stack_storet stack
Definition: write_stack.h:71
void add_to_stack(std::shared_ptr< write_stack_entryt > entry_pointer, const abstract_environmentt environment, const namespacet &ns)
Add an element to the top of the stack.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
Represents a stack of write operations to an addressable memory location.