cprover
Loading...
Searching...
No Matches
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
23
25write_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;
78 get_which_side_integral(expr, base, offset);
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
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{
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
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 {
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
199 }
200 }
202 return std::move(top_expr);
203}
204
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,
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 = {
272 if(integral_types.find(binary_e.lhs().type().id()) != integral_types.cend())
273 {
275 out_base_expr = binary_e.rhs();
277 }
278 else if(
279 integral_types.find(binary_e.rhs().type().id()) != integral_types.cend())
280 {
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)
unsignedbv_typet unsigned_long_int_type()
Definition c_types.cpp:104
signedbv_typet signed_size_type()
Definition c_types.cpp:84
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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 & index()
Definition std_expr.h:1363
const irep_idt & id() const
Definition irep.h:396
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:2874
The unary minus expression.
Definition std_expr.h:390
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.
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.
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.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
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:2751
Represents a stack of write operations to an addressable memory location.