cprover
Loading...
Searching...
No Matches
flatten_ok_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Flatten OK Expressions
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
9#include "flatten_ok_expr.h"
10
11#include <util/c_types.h>
12
13#include "state.h"
14
16{
17 const auto &state = ok_expr.state();
18 const auto &pointer = ok_expr.address();
19 const auto &size = ok_expr.size();
20
21 // X_ok(p, s) <-->
22 // live_object(p)
23 // ∧ offset(p)+s≤object_size(p)
24 // ∧ writeable_object(p) if applicable
25
26 auto live_object = state_live_object_exprt(state, pointer);
27
28 auto writeable_object = state_writeable_object_exprt(state, pointer);
29
30 auto ssize_type = signed_size_type();
31 auto offset = pointer_offset_exprt(pointer, ssize_type);
32
33 auto size_type = ::size_type();
34
35 // extend one bit, to cover overflow case
36 auto size_type_ext = unsignedbv_typet(size_type.get_width() + 1);
37
38 auto object_size = state_object_size_exprt(state, pointer, size_type);
39
40 auto object_size_casted = typecast_exprt(object_size, size_type_ext);
41
42 auto offset_casted_to_unsigned =
44 auto offset_extended =
45 typecast_exprt::conditional_cast(offset_casted_to_unsigned, size_type_ext);
46 auto size_casted = typecast_exprt::conditional_cast(size, size_type_ext);
47 auto upper = binary_relation_exprt(
48 plus_exprt(offset_extended, size_casted), ID_le, object_size_casted);
49
50 auto conjunction = and_exprt(live_object, upper);
51
52 if(ok_expr.id() == ID_state_w_ok || ok_expr.id() == ID_state_rw_ok)
53 conjunction.add_to_operands(std::move(writeable_object));
54
55 return std::move(conjunction);
56}
unsignedbv_typet size_type()
Definition c_types.cpp:50
signedbv_typet signed_size_type()
Definition c_types.cpp:66
Boolean AND.
Definition std_expr.h:2125
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Base class for all expressions.
Definition expr.h:56
const irep_idt & id() const
Definition irep.h:388
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The offset (in bytes) of a pointer relative to the object.
const exprt & size() const
Definition state.h:857
const exprt & address() const
Definition state.h:847
const exprt & state() const
Definition state.h:837
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
Fixed-width bit-vector with unsigned binary interpretation.
exprt flatten(const state_ok_exprt &ok_expr)
exprt object_size(const exprt &pointer)
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:83