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>
18 #include <util/pointer_expr.h>
21 #include <util/prefix.h>
22 #include <util/simplify_expr.h>
23 #include <util/std_expr.h>
24 
26 {
27  return expr.type().get_bool(ID_C_dynamic) ||
28  (expr.id() == ID_symbol &&
29  has_prefix(
30  id2string(to_symbol_expr(expr).get_identifier()),
32 }
33 
34 void pointer_logict::get_dynamic_objects(std::vector<std::size_t> &o) const
35 {
36  o.clear();
37  std::size_t nr=0;
38 
39  for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++nr)
40  if(is_dynamic_object(*it))
41  o.push_back(nr);
42 }
43 
44 std::size_t pointer_logict::add_object(const exprt &expr)
45 {
46  // remove any index/member
47 
48  if(expr.id()==ID_index)
49  {
50  return add_object(to_index_expr(expr).array());
51  }
52  else if(expr.id()==ID_member)
53  {
54  return add_object(to_member_expr(expr).compound());
55  }
56 
57  return objects.number(expr);
58 }
59 
61  std::size_t object,
62  const pointer_typet &type) const
63 {
64  pointert pointer(object, 0);
65  return pointer_expr(pointer, type);
66 }
67 
69  const pointert &pointer,
70  const pointer_typet &type) const
71 {
72  if(pointer.object==null_object) // NULL?
73  {
74  if(pointer.offset==0)
75  {
76  return null_pointer_exprt(type);
77  }
78  else
79  {
80  null_pointer_exprt null(type);
81  return plus_exprt(null,
83  }
84  }
85  else if(pointer.object==invalid_object) // INVALID?
86  {
87  return constant_exprt("INVALID", type);
88  }
89 
90  if(pointer.object>=objects.size())
91  {
92  return constant_exprt("INVALID-" + std::to_string(pointer.object), type);
93  }
94 
95  const exprt &object_expr=objects[pointer.object];
96 
97  typet subtype = type.subtype();
98  // This is a gcc extension.
99  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
100  if(subtype.id() == ID_empty)
101  subtype = char_type();
102  if(object_expr.id() == ID_string_constant)
103  {
104  subtype = object_expr.type();
105 
106  // a string constant must be array-typed with fixed size
107  const array_typet &array_type = to_array_type(object_expr.type());
108  mp_integer array_size =
109  numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
110  if(array_size > pointer.offset)
111  {
112  to_array_type(subtype).size() =
113  from_integer(array_size - pointer.offset, array_type.size().type());
114  }
115  }
116  auto deep_object_opt =
117  get_subexpression_at_offset(object_expr, pointer.offset, subtype, ns);
118  CHECK_RETURN(deep_object_opt.has_value());
119  exprt deep_object = deep_object_opt.value();
120  simplify(deep_object, ns);
121  if(
122  deep_object.id() != ID_byte_extract_little_endian &&
123  deep_object.id() != ID_byte_extract_big_endian)
124  {
126  address_of_exprt(deep_object), type);
127  }
128 
129  const byte_extract_exprt &be = to_byte_extract_expr(deep_object);
130  const address_of_exprt base(be.op());
131  if(be.offset().is_zero())
132  return typecast_exprt::conditional_cast(base, type);
133 
134  const auto object_size = pointer_offset_size(be.op().type(), ns);
135  if(object_size.has_value() && *object_size <= 1)
136  {
138  plus_exprt(base, from_integer(pointer.offset, pointer_diff_type())),
139  type);
140  }
141  else if(object_size.has_value() && pointer.offset % *object_size == 0)
142  {
144  plus_exprt(
145  base, from_integer(pointer.offset / *object_size, pointer_diff_type())),
146  type);
147  }
148  else
149  {
151  plus_exprt(
154  type);
155  }
156 }
157 
159 {
160  // add NULL
161  null_object=objects.number(exprt(ID_NULL));
163 
164  // add INVALID
165  invalid_object=objects.number(exprt("INVALID"));
166 }
167 
169 {
170 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
bitvector_typet char_type()
Definition: c_types.cpp:114
Operator to return the address of an object.
Definition: pointer_expr.h:341
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:771
Expression of type type extracted from some object op starting at position offset (given in number of...
A constant literal expression.
Definition: std_expr.h:2753
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:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irep_idt & id() const
Definition: irep.h:407
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The null pointer constant.
Definition: pointer_expr.h:703
number_type number(const key_type &a)
Definition: numbering.h:37
const_iterator cend() const
Definition: numbering.h:106
size_type size() const
Definition: numbering.h:66
const_iterator cbegin() const
Definition: numbering.h:93
The plus expression Associativity is not specified.
Definition: std_expr.h:914
void get_dynamic_objects(std::vector< std::size_t > &objects) const
std::size_t invalid_object
Definition: pointer_logic.h:75
numberingt< exprt, irep_hash > objects
Definition: pointer_logic.h:26
std::size_t null_object
Definition: pointer_logic.h:75
std::size_t add_object(const exprt &expr)
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
const namespacet & ns
Definition: pointer_logic.h:74
bool is_dynamic_object(const exprt &expr) const
pointer_logict(const namespacet &_ns)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
Semantic type conversion.
Definition: std_expr.h:1866
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
API to expression classes for Pointers.
Pointer Logic.
optionalt< 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.
Pointer Logic.
exprt object_size(const exprt &pointer)
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
bool simplify(exprt &expr, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
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
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.