cprover
pointer_logic.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Logic
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "pointer_logic.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/byte_operators.h>
16 #include <util/c_types.h>
17 #include <util/invariant.h>
19 #include <util/prefix.h>
20 #include <util/simplify_expr.h>
21 #include <util/std_expr.h>
22 
24 {
25  if(expr.type().get_bool(ID_C_dynamic))
26  return true;
27 
28  if(expr.id()==ID_symbol)
29  if(has_prefix(id2string(to_symbol_expr(expr).get_identifier()),
30  "symex_dynamic::"))
31  return true;
32 
33  return false;
34 }
35 
36 void pointer_logict::get_dynamic_objects(std::vector<std::size_t> &o) const
37 {
38  o.clear();
39  std::size_t nr=0;
40 
42  it=objects.begin();
43  it!=objects.end();
44  it++, nr++)
45  if(is_dynamic_object(*it))
46  o.push_back(nr);
47 }
48 
49 std::size_t pointer_logict::add_object(const exprt &expr)
50 {
51  // remove any index/member
52 
53  if(expr.id()==ID_index)
54  {
55  return add_object(to_index_expr(expr).array());
56  }
57  else if(expr.id()==ID_member)
58  {
59  return add_object(to_member_expr(expr).compound());
60  }
61 
62  return objects.number(expr);
63 }
64 
66  std::size_t object,
67  const pointer_typet &type) const
68 {
69  pointert pointer(object, 0);
70  return pointer_expr(pointer, type);
71 }
72 
74  const pointert &pointer,
75  const pointer_typet &type) const
76 {
77  if(pointer.object==null_object) // NULL?
78  {
79  if(pointer.offset==0)
80  {
81  null_pointer_exprt result(type);
82  return std::move(result);
83  }
84  else
85  {
86  null_pointer_exprt null(type);
87  return plus_exprt(null,
89  }
90  }
91  else if(pointer.object==invalid_object) // INVALID?
92  {
93  return constant_exprt("INVALID", type);
94  }
95 
96  if(pointer.object>=objects.size())
97  {
98  return constant_exprt("INVALID-" + std::to_string(pointer.object), type);
99  }
100 
101  const exprt &object_expr=objects[pointer.object];
102 
103  typet subtype = type.subtype();
104  // This is a gcc extension.
105  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
106  if(subtype.id() == ID_empty)
107  subtype = char_type();
108  exprt deep_object =
109  get_subexpression_at_offset(object_expr, pointer.offset, subtype, ns);
110  CHECK_RETURN(deep_object.is_not_nil());
111  simplify(deep_object, ns);
112  if(deep_object.id() != byte_extract_id())
114  address_of_exprt(deep_object), type);
115 
116  const byte_extract_exprt &be = to_byte_extract_expr(deep_object);
117  const address_of_exprt base(be.op());
118  if(be.offset().is_zero())
119  return typecast_exprt::conditional_cast(base, type);
120 
121  const auto object_size = pointer_offset_size(be.op().type(), ns);
122  if(object_size.has_value() && *object_size <= 1)
123  {
125  plus_exprt(base, from_integer(pointer.offset, pointer_diff_type())),
126  type);
127  }
128  else if(object_size.has_value() && pointer.offset % *object_size == 0)
129  {
131  plus_exprt(
132  base, from_integer(pointer.offset / *object_size, pointer_diff_type())),
133  type);
134  }
135  else
136  {
138  plus_exprt(
141  type);
142  }
143 }
144 
146 {
147  // add NULL
148  null_object=objects.number(exprt(ID_NULL));
150 
151  // add INVALID
152  invalid_object=objects.number(exprt("INVALID"));
153 }
154 
156 {
157 }
The type of an expression, extends irept.
Definition: type.h:27
Semantic type conversion.
Definition: std_expr.h:2277
number_type number(const key_type &a)
Definition: numbering.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
size_type size() const
Definition: numbering.h:66
The null pointer constant.
Definition: std_expr.h:4471
typet & type()
Return the type of the expression.
Definition: expr.h:68
void get_dynamic_objects(std::vector< std::size_t > &objects) const
A constant literal expression.
Definition: std_expr.h:4384
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
const namespacet & ns
Definition: pointer_logic.h:75
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:259
Expression classes for byte-level operators.
exprt get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
The pointer type These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (they ...
Definition: std_types.h:1507
iterator begin()
Definition: numbering.h:85
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
bool is_dynamic_object(const exprt &expr) const
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
Operator to return the address of an object.
Definition: std_expr.h:3255
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
typename data_typet::const_iterator const_iterator
Definition: numbering.h:35
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2291
Pointer Logic.
pointer_logict(const namespacet &_ns)
objectst objects
Definition: pointer_logic.h:27
Base class for all expressions.
Definition: expr.h:54
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
iterator end()
Definition: numbering.h:98
Pointer Logic.
const typet & subtype() const
Definition: type.h:38
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
std::size_t add_object(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
bitvector_typet char_type()
Definition: c_types.cpp:114
std::size_t null_object
Definition: pointer_logic.h:76
bool simplify(exprt &expr, const namespacet &ns)
std::size_t invalid_object
Definition: pointer_logic.h:76
irep_idt byte_extract_id()