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 "namespace.h"
17 #include "pointer_offset_size.h"
18 #include "std_types.h"
19 
21 {
22  const std::string val=id2string(get_value());
23  return val.find_first_not_of('0')==std::string::npos;
24 }
25 
27 {
28  if(op.empty())
29  return false_exprt();
30  else if(op.size()==1)
31  return op.front();
32  else
33  {
34  or_exprt result;
35  result.operands()=op;
36  return result;
37  }
38 }
39 
40 void dynamic_object_exprt::set_instance(unsigned int instance)
41 {
42  op0()=from_integer(instance, typet(ID_natural));
43 }
44 
46 {
47  return std::stoul(id2string(to_constant_expr(op0()).get_value()));
48 }
49 
51 {
52  if(op.empty())
53  return true_exprt();
54  else if(op.size()==1)
55  return op.front();
56  else
57  {
58  and_exprt result;
59  result.operands()=op;
60  return result;
61  }
62 }
63 
66  const namespacet &ns,
67  const exprt &expr,
69 {
70  if(expr.id()==ID_index)
71  {
72  const index_exprt &index=to_index_expr(expr);
73 
74  build_object_descriptor_rec(ns, index.array(), dest);
75 
76  exprt sub_size=size_of_expr(expr.type(), ns);
77  assert(sub_size.is_not_nil());
78 
79  dest.offset()=
80  plus_exprt(dest.offset(),
82  typecast_exprt(sub_size, index_type())));
83  }
84  else if(expr.id()==ID_member)
85  {
86  const member_exprt &member=to_member_expr(expr);
87  const exprt &struct_op=member.struct_op();
88 
89  build_object_descriptor_rec(ns, struct_op, dest);
90 
91  exprt offset=member_offset_expr(member, ns);
92  assert(offset.is_not_nil());
93 
94  dest.offset()=
95  plus_exprt(dest.offset(),
96  typecast_exprt(offset, index_type()));
97  }
98  else if(expr.id()==ID_byte_extract_little_endian ||
99  expr.id()==ID_byte_extract_big_endian)
100  {
102 
103  dest.object()=be.op();
104 
105  build_object_descriptor_rec(ns, be.op(), dest);
106 
107  dest.offset()=
108  plus_exprt(dest.offset(),
109  typecast_exprt(to_byte_extract_expr(expr).offset(),
110  index_type()));
111  }
112  else if(expr.id()==ID_typecast)
113  {
114  const typecast_exprt &tc=to_typecast_expr(expr);
115 
116  dest.object()=tc.op();
117 
118  build_object_descriptor_rec(ns, tc.op(), dest);
119  }
120 }
121 
124  const exprt &expr,
125  const namespacet &ns)
126 {
127  assert(object().id()==ID_unknown);
128  object()=expr;
129 
130  if(offset().id()==ID_unknown)
132 
133  build_object_descriptor_rec(ns, expr, *this);
134 
135  assert(root_object().type().id()!=ID_empty);
136 }
137 
139 {
140  return constant_exprt(std::to_string(v), integer_typet());
141 }
142 
144  const exprt &_src,
145  const irep_idt &_id,
146  const std::size_t _distance):
147  binary_exprt(_src, _id, integer_constant(_distance))
148 {
149 }
150 
152  const exprt &_src,
153  const std::size_t _index):
155  _src, ID_extractbit, integer_constant(_index))
156 {
157 }
158 
160  const exprt &_src,
161  const std::size_t _upper,
162  const std::size_t _lower,
163  const typet &_type):
164  exprt(ID_extractbits, _type)
165 {
166  assert(_upper>=_lower);
167  operands().resize(3);
168  src()=_src;
169  upper()=integer_constant(_upper);
170  lower()=integer_constant(_lower);
171 }
172 
173 /*******************************************************************\
174 
175 Function: address_of_exprt::address_of_exprt
176 
177  Inputs:
178 
179  Outputs:
180 
181  Purpose:
182 
183 \*******************************************************************/
184 
186  unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
187 {
188 }
The type of an expression.
Definition: type.h:20
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
exprt size_of_expr(const typet &type, const namespacet &ns)
semantic type conversion
Definition: std_expr.h:1725
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:104
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
boolean OR
Definition: std_expr.h:1968
exprt & op0()
Definition: expr.h:84
unsigned int get_instance() const
Definition: std_expr.cpp:45
exprt & lower()
Definition: std_expr.h:2539
shift_exprt(const irep_idt &_id)
Definition: std_expr.h:2230
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
const irep_idt & get_value() const
Definition: std_expr.h:3702
const exprt & root_object() const
Definition: std_expr.h:1600
typet & type()
Definition: expr.h:60
A constant literal expression.
Definition: std_expr.h:3685
exprt & op()
Definition: std_expr.h:1739
bool value_is_zero_string() const
Definition: std_expr.cpp:20
Extract member of struct or union.
Definition: std_expr.h:3214
void set_instance(unsigned int instance)
Definition: std_expr.cpp:40
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:50
const irep_idt & id() const
Definition: irep.h:189
Expression classes for byte-level operators.
The boolean constant true.
Definition: std_expr.h:3742
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:65
A generic base class for binary expressions.
Definition: std_expr.h:471
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:123
exprt & src()
Definition: std_expr.h:2529
boolean AND
Definition: std_expr.h:1852
API to expression classes.
Generic base class for unary expressions.
Definition: std_expr.h:221
TO_BE_DOCUMENTED.
Definition: namespace.h:62
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1578
The plus expression.
Definition: std_expr.h:702
exprt & upper()
Definition: std_expr.h:2534
bitvector_typet index_type()
Definition: c_types.cpp:15
The boolean constant false.
Definition: std_expr.h:3753
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:26
std::vector< exprt > operandst
Definition: expr.h:49
binary multiplication
Definition: std_expr.h:806
Pointer Logic.
Unbounded, signed integers.
Definition: std_types.h:69
API to type classes.
exprt & index()
Definition: std_expr.h:1208
static constant_exprt integer_constant(unsigned v)
Definition: std_expr.cpp:138
Base class for all expressions.
Definition: expr.h:46
const exprt & struct_op() const
Definition: std_expr.h:3270
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:546
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
operandst & operands()
Definition: expr.h:70
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:1198
array index operator
Definition: std_expr.h:1170