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/simplify_expr.h>
21 #include <util/std_expr.h>
22 
24 write_stackt::write_stackt() : stack(), top_stack(true)
25 {
26 }
27 
33  const exprt &expr,
34  const abstract_environmentt &environment,
35  const namespacet &ns)
36 {
37  top_stack = false;
38  if(expr.type().id() == ID_array)
39  {
40  // We are assigning an array to a pointer, which is equivalent to assigning
41  // the first element of that arary
42  // &(expr)[0]
45  environment,
46  ns);
47  }
48  else
49  {
50  construct_stack_to_pointer(expr, environment, ns);
51  }
52 }
53 
59  const exprt &expr,
60  const abstract_environmentt &environment,
61  const namespacet &ns)
62 {
63  PRECONDITION(expr.type().id() == ID_pointer);
64 
65  if(expr.id() == ID_address_of)
66  {
67  // resovle reminder, can either be a symbol, member or index of
68  // otherwise unsupported
70  to_address_of_expr(expr).object(), environment, ns);
71  }
72  else if(expr.id() == ID_plus || expr.id() == ID_minus)
73  {
74  exprt base;
75  exprt offset;
76  const integral_resultt &which_side =
77  get_which_side_integral(expr, base, offset);
78  INVARIANT(
80  "An offset must be an integral amount");
81 
82  if(expr.id() == ID_minus)
83  {
84  // can't get a valid pointer by subtracting from a constant number
85  if(which_side == integral_resultt::LHS_INTEGRAL)
86  {
87  top_stack = true;
88  return;
89  }
90  offset = unary_minus_exprt(offset);
91  }
92 
93  abstract_object_pointert offset_value = environment.eval(offset, ns);
94 
96  std::make_shared<offset_entryt>(offset_value), environment, ns);
97 
98  // Build the pointer part
99  construct_stack_to_pointer(base, environment, ns);
100 
101  if(!top_stack)
102  {
103  // check the symbol at the bottom of the stack
104  std::shared_ptr<const write_stack_entryt> entry = *stack.cbegin();
105  INVARIANT(
106  entry->get_access_expr().id() == ID_symbol,
107  "The base should be an addressable location (i.e. symbol)");
108 
109  if(entry->get_access_expr().type().id() != ID_array)
110  {
111  top_stack = true;
112  }
113  }
114  }
115  else
116  {
117  // unknown expression type - play it safe and set to top
118  top_stack = true;
119  }
120 }
121 
128  const exprt &expr,
129  const abstract_environmentt &environment,
130  const namespacet &ns)
131 {
132  if(!top_stack)
133  {
134  if(expr.id() == ID_member)
135  {
136  add_to_stack(std::make_shared<simple_entryt>(expr), environment, ns);
138  to_member_expr(expr).struct_op(), environment, ns);
139  }
140  else if(expr.id() == ID_symbol)
141  {
142  add_to_stack(std::make_shared<simple_entryt>(expr), environment, ns);
143  }
144  else if(expr.id() == ID_index)
145  {
146  construct_stack_to_array_index(to_index_expr(expr), environment, ns);
147  }
148  else
149  {
150  top_stack = true;
151  }
152  }
153 }
154 
160  const index_exprt &index_expr,
161  const abstract_environmentt &environment,
162  const namespacet &ns)
163 {
164  abstract_object_pointert offset_value =
165  environment.eval(index_expr.index(), ns);
166 
167  add_to_stack(std::make_shared<offset_entryt>(offset_value), environment, ns);
168  construct_stack_to_lvalue(index_expr.array(), environment, ns);
169 }
170 
175 {
176  // A top stack is useless and its expression should not be evaluated
178  exprt access_expr = nil_exprt();
179  for(const std::shared_ptr<write_stack_entryt> &entry : stack)
180  {
181  exprt new_expr = entry->get_access_expr();
182  if(access_expr.id() == ID_nil)
183  {
184  access_expr = new_expr;
185  }
186  else
187  {
188  if(new_expr.operands().size() == 0)
189  {
190  new_expr.operands().resize(1);
191  }
192  new_expr.operands()[0] = access_expr;
193 
194  // If neccesary, complete the type of the new access expression
195  entry->adjust_access_type(new_expr);
196 
197  access_expr = new_expr;
198  }
199  }
200  address_of_exprt top_expr(access_expr);
201  return std::move(top_expr);
202 }
203 
208 {
209  return top_stack;
210 }
211 
218  std::shared_ptr<write_stack_entryt> entry_pointer,
219  const abstract_environmentt environment,
220  const namespacet &ns)
221 {
222  if(
223  stack.empty() ||
224  !stack.front()->try_squash_in(entry_pointer, environment, ns))
225  {
226  stack.insert(stack.begin(), entry_pointer);
227  }
228 }
229 
238  const exprt &expr,
239  exprt &out_base_expr,
240  exprt &out_integral_expr)
241 {
242  PRECONDITION(expr.operands().size() == 2);
243  const auto binary_e = to_binary_expr(expr);
244  static const std::unordered_set<irep_idt, irep_id_hash> integral_types = {
245  ID_signedbv, ID_unsignedbv, ID_integer};
246  if(integral_types.find(binary_e.lhs().type().id()) != integral_types.cend())
247  {
248  out_integral_expr = binary_e.lhs();
249  out_base_expr = binary_e.rhs();
251  }
252  else if(
253  integral_types.find(binary_e.rhs().type().id()) != integral_types.cend())
254  {
255  out_integral_expr = binary_e.rhs();
256  out_base_expr = binary_e.lhs();
258  }
259  else
260  {
261  out_integral_expr.make_nil();
262  out_base_expr.make_nil();
264  }
265 }
write_stackt::integral_resultt::LHS_INTEGRAL
@ LHS_INTEGRAL
write_stack.h
Represents a stack of write operations to an addressable memory location.
write_stackt::is_top_value
bool is_top_value() const
Is the stack representing an unknown value and hence can't be written to or read from.
Definition: write_stack.cpp:207
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
arith_tools.h
irept::make_nil
void make_nil()
Definition: irep.h:464
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
write_stackt::integral_resultt::RHS_INTEGRAL
@ RHS_INTEGRAL
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
write_stack_entryt::get_access_expr
virtual exprt get_access_expr() const =0
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
write_stackt::top_stack
bool top_stack
Definition: write_stack.h:68
write_stackt::construct_stack_to_lvalue
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.
Definition: write_stack.cpp:127
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
pointer_expr.h
API to expression classes for Pointers.
index_exprt::index
exprt & index()
Definition: std_expr.h:1269
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:391
index_exprt::array
exprt & array()
Definition: std_expr.h:1259
abstract_environmentt::eval
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
Definition: abstract_environment.cpp:37
irept::id
const irep_idt & id() const
Definition: irep.h:407
write_stackt::construct_stack_to_pointer
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:58
simplify_expr.h
write_stackt::get_which_side_integral
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,...
Definition: write_stack.cpp:237
write_stackt::construct_stack_to_array_index
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.
Definition: write_stack.cpp:159
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
write_stackt::integral_resultt::NEITHER_INTEGRAL
@ NEITHER_INTEGRAL
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
exprt::operands
operandst & operands()
Definition: expr.h:96
index_exprt
Array index operator.
Definition: std_expr.h:1243
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
write_stackt::integral_resultt
integral_resultt
Definition: write_stack.h:56
write_stackt::write_stackt
write_stackt()
Build a topstack.
Definition: write_stack.cpp:24
write_stackt::add_to_stack
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.
Definition: write_stack.cpp:217
write_stackt::to_expression
exprt to_expression() const
Convert the stack to an expression that can be used to write to.
Definition: write_stack.cpp:174
std_expr.h
API to expression classes.
write_stackt::stack
continuation_stack_storet stack
Definition: write_stack.h:67
c_types.h