cprover
std_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "std_expr.h"
10 
11 #include <cassert>
12 
13 #include "arith_tools.h"
14 #include "byte_operators.h"
15 #include "c_types.h"
16 #include "pointer_offset_size.h"
17 
19 {
20  const std::string val=id2string(get_value());
21  return val.find_first_not_of('0')==std::string::npos;
22 }
23 
25 {
26  if(op.empty())
27  return false_exprt();
28  else if(op.size()==1)
29  return op.front();
30  else
31  {
32  or_exprt result;
33  result.operands()=op;
34  return result;
35  }
36 }
37 
38 void dynamic_object_exprt::set_instance(unsigned int instance)
39 {
40  op0()=from_integer(instance, typet(ID_natural));
41 }
42 
44 {
45  return std::stoul(id2string(to_constant_expr(op0()).get_value()));
46 }
47 
49 {
50  if(op.empty())
51  return true_exprt();
52  else if(op.size()==1)
53  return op.front();
54  else
55  {
56  and_exprt result;
57  result.operands()=op;
58  return result;
59  }
60 }
61 
64  const namespacet &ns,
65  const exprt &expr,
67 {
68  if(expr.id()==ID_index)
69  {
70  const index_exprt &index=to_index_expr(expr);
71 
72  build_object_descriptor_rec(ns, index.array(), dest);
73 
74  exprt sub_size=size_of_expr(expr.type(), ns);
75  assert(sub_size.is_not_nil());
76 
77  dest.offset()=
78  plus_exprt(dest.offset(),
80  typecast_exprt(sub_size, index_type())));
81  }
82  else if(expr.id()==ID_member)
83  {
84  const member_exprt &member=to_member_expr(expr);
85  const exprt &struct_op=member.struct_op();
86 
87  build_object_descriptor_rec(ns, struct_op, dest);
88 
89  exprt offset=member_offset_expr(member, ns);
90  assert(offset.is_not_nil());
91 
92  dest.offset()=
93  plus_exprt(dest.offset(),
94  typecast_exprt(offset, index_type()));
95  }
96  else if(expr.id()==ID_byte_extract_little_endian ||
97  expr.id()==ID_byte_extract_big_endian)
98  {
100 
101  dest.object()=be.op();
102 
103  build_object_descriptor_rec(ns, be.op(), dest);
104 
105  dest.offset()=
106  plus_exprt(dest.offset(),
107  typecast_exprt(to_byte_extract_expr(expr).offset(),
108  index_type()));
109  }
110  else if(expr.id()==ID_typecast)
111  {
112  const typecast_exprt &tc=to_typecast_expr(expr);
113 
114  dest.object()=tc.op();
115 
116  build_object_descriptor_rec(ns, tc.op(), dest);
117  }
118 }
119 
122  const exprt &expr,
123  const namespacet &ns)
124 {
125  assert(object().id()==ID_unknown);
126  object()=expr;
127 
128  if(offset().id()==ID_unknown)
130 
131  build_object_descriptor_rec(ns, expr, *this);
132 
133  assert(root_object().type().id()!=ID_empty);
134 }
135 
137  const exprt &_src,
138  const irep_idt &_id,
139  const std::size_t _distance):
140  binary_exprt(_src, _id, from_integer(_distance, integer_typet()))
141 {
142 }
143 
145  const exprt &_src,
146  const std::size_t _index):
148  _src, ID_extractbit, from_integer(_index, integer_typet()))
149 {
150 }
151 
153  const exprt &_src,
154  const std::size_t _upper,
155  const std::size_t _lower,
156  const typet &_type):
157  exprt(ID_extractbits, _type)
158 {
159  assert(_upper>=_lower);
160  operands().resize(3);
161  src()=_src;
162  upper()=from_integer(_upper, integer_typet());
163  lower()=from_integer(_lower, integer_typet());
164 }
165 
167  unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
168 {
169 }
The type of an expression.
Definition: type.h:22
exprt size_of_expr(const typet &type, const namespacet &ns)
semantic type conversion
Definition: std_expr.h:2111
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
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
boolean OR
Definition: std_expr.h:2391
exprt & op0()
Definition: expr.h:72
const exprt & op() const
Definition: std_expr.h:340
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:166
unsigned int get_instance() const
Definition: std_expr.cpp:43
exprt & lower()
Definition: std_expr.h:3104
shift_exprt(const irep_idt &_id)
Definition: std_expr.h:2768
const irep_idt & get_value() const
Definition: std_expr.h:4439
const exprt & root_object() const
Definition: std_expr.h:1966
typet & type()
Definition: expr.h:56
bool value_is_zero_string() const
Definition: std_expr.cpp:18
Extract member of struct or union.
Definition: std_expr.h:3869
void set_instance(unsigned int instance)
Definition: std_expr.cpp:38
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
const irep_idt & id() const
Definition: irep.h:259
Expression classes for byte-level operators.
The boolean constant true.
Definition: std_expr.h:4486
static void build_object_descriptor_rec(const namespacet &ns, const exprt &expr, object_descriptor_exprt &dest)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:63
A generic base class for binary expressions.
Definition: std_expr.h:649
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:121
exprt & src()
Definition: std_expr.h:3094
boolean AND
Definition: std_expr.h:2255
API to expression classes.
Generic base class for unary expressions.
Definition: std_expr.h:303
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
The plus expression.
Definition: std_expr.h:893
exprt & upper()
Definition: std_expr.h:3099
bitvector_typet index_type()
Definition: c_types.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
The boolean constant false.
Definition: std_expr.h:4497
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:24
std::vector< exprt > operandst
Definition: expr.h:45
binary multiplication
Definition: std_expr.h:1017
Pointer Logic.
Unbounded, signed integers.
Definition: std_types.h:70
exprt & index()
Definition: std_expr.h:1496
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3909
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:730
operandst & operands()
Definition: expr.h:66
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)
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
array index operator
Definition: std_expr.h:1462