CBMC
Loading...
Searching...
No Matches
std_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "std_expr.h"
10
11#include "config.h"
12#include "namespace.h"
13#include "pointer_expr.h"
14#include "range.h"
15#include "substitute_symbols.h"
16
17#include <map>
18
20{
21 const std::string val=id2string(get_value());
22 return val.find_first_not_of('0')==std::string::npos;
23}
24
26{
27 if(type().id() != ID_pointer)
28 return false;
29
30 if(get_value() == ID_NULL)
31 return true;
32
33 // We used to support "0" (when NULL_is_zero), but really front-ends should
34 // resolve this and generate ID_NULL instead.
36 !value_is_zero_string() || !config.ansi_c.NULL_is_zero,
37 "front-end should use ID_NULL");
38 return false;
39}
40
41void constant_exprt::check(const exprt &expr, const validation_modet vm)
42{
43 nullary_exprt::check(expr, vm);
44
45 const auto value = expr.get(ID_value);
46
48 vm,
49 !can_cast_type<bitvector_typet>(expr.type()) || !value.empty(),
50 "bitvector constant must have a non-empty value");
51
53 vm,
56 expr.type().id() == ID_verilog_unsignedbv ||
57 expr.type().id() == ID_verilog_signedbv ||
58 id2string(value).find_first_not_of("0123456789ABCDEF") ==
59 std::string::npos,
60 "negative bitvector constant must use two's complement");
61
63 vm,
65 expr.type().id() == ID_verilog_unsignedbv ||
66 expr.type().id() == ID_verilog_signedbv || value == ID_0 ||
67 id2string(value)[0] != '0',
68 "bitvector constant must not have leading zeros");
69}
70
72{
73 if(op.empty())
74 return false_exprt();
75 else if(op.size()==1)
76 return op.front();
77 else
78 {
79 return or_exprt(exprt::operandst(op));
80 }
81}
82
84{
85 PRECONDITION(a.is_boolean() && b.is_boolean());
86 if(b.is_constant())
87 {
89 return false_exprt{};
90 return a;
91 }
92 if(a.is_constant())
93 {
95 return false_exprt{};
96 return b;
97 }
98 if(b.id() == ID_and)
99 {
100 b.add_to_operands(std::move(a));
101 return b;
102 }
103 return and_exprt{std::move(a), std::move(b)};
104}
105
107{
108 if(op.empty())
109 return true_exprt();
110 else if(op.size()==1)
111 return op.front();
112 else if(op.size() == 2)
113 return conjunction(op[0], op[1]);
114 else
115 {
116 return and_exprt(exprt::operandst(op));
117 }
118}
119
120// Implementation of struct_exprt::component for const / non const overloads.
121template <typename T>
122auto component(T &struct_expr, const irep_idt &name, const namespacet &ns)
123 -> decltype(struct_expr.op0())
124{
125 static_assert(
126 std::is_base_of<struct_exprt, T>::value, "T must be a struct_exprt.");
128 struct_expr.type().id() == ID_struct_tag
129 ? ns.follow_tag(to_struct_tag_type(struct_expr.type()))
130 : to_struct_type(struct_expr.type());
131 const auto index = struct_type.component_number(name);
133 index < struct_expr.operands().size(),
134 "component matching index should exist");
135 return struct_expr.operands()[index];
136}
137
140{
141 return ::component(*this, name, ns);
142}
143
145const exprt &
146struct_exprt::component(const irep_idt &name, const namespacet &ns) const
147{
148 return ::component(*this, name, ns);
149}
150
159 const exprt &expr,
160 const namespacet &ns,
161 const validation_modet vm)
162{
163 check(expr, vm);
164
165 const auto &member_expr = to_member_expr(expr);
166
167 const typet &compound_type = member_expr.compound().type();
168 const auto *struct_union_type =
169 (compound_type.id() == ID_struct_tag || compound_type.id() == ID_union_tag)
170 ? &ns.follow_tag(to_struct_or_union_tag_type(compound_type))
173 vm,
174 struct_union_type != nullptr,
175 "member must address a struct, union or compatible type");
176
177 const auto &component =
178 struct_union_type->get_component(member_expr.get_component_name());
179
181 vm,
182 component.is_not_nil(),
183 "member component '" + id2string(member_expr.get_component_name()) +
184 "' must exist on addressed type");
185
187 vm,
188 component.type() == member_expr.type(),
189 "member expression's type must match the addressed struct or union "
190 "component");
191}
192
193void let_exprt::validate(const exprt &expr, const validation_modet vm)
194{
195 check(expr, vm);
196
197 const auto &let_expr = to_let_expr(expr);
198
200 vm,
201 let_expr.values().size() == let_expr.variables().size(),
202 "number of variables must match number of values");
203
204 for(const auto &binding :
205 make_range(let_expr.variables()).zip(let_expr.values()))
206 {
208 vm,
209 binding.first.id() == ID_symbol,
210 "let binding symbols must be symbols");
211
213 vm,
214 binding.first.type() == binding.second.type(),
215 "let bindings must be type consistent");
216 }
217}
218
220{
222 PRECONDITION(!designators.empty());
223
224 with_exprt result{exprt{}, exprt{}, exprt{}};
225 exprt *dest = &result;
226
227 for(const auto &expr : designators)
228 {
229 with_exprt tmp{exprt{}, exprt{}, exprt{}};
230
231 if(expr.id() == ID_index_designator)
232 {
233 tmp.where() = to_index_designator(expr).index();
234 }
235 else if(expr.id() == ID_member_designator)
236 {
237 // irep_idt component_name=
238 // to_member_designator(*it).get_component_name();
239 }
240 else
242
243 *dest = tmp;
244 dest = &to_with_expr(*dest).new_value();
245 }
246
247 return result;
248}
249
251{
252 // number of values must match the number of bound variables
253 auto &variables = this->variables();
254 PRECONDITION(variables.size() == values.size());
255
256 std::map<symbol_exprt, exprt> value_map;
257
258 for(std::size_t i = 0; i < variables.size(); i++)
259 {
260 // types must match
261 PRECONDITION(variables[i].type() == values[i].type());
262 value_map[variables[i]] = values[i];
263 }
264
265 // build a substitution map
266 std::map<irep_idt, exprt> substitutions;
267
268 for(std::size_t i = 0; i < variables.size(); i++)
269 substitutions[variables[i].get_identifier()] = values[i];
270
271 // now recurse downwards and substitute in 'where'
273
274 if(substitute_result.has_value())
275 return substitute_result.value();
276 else
277 return where(); // trivial case, variables not used
278}
279
280exprt binding_exprt::instantiate(const variablest &new_variables) const
281{
282 std::vector<exprt> values;
283 values.reserve(new_variables.size());
284 for(const auto &new_variable : new_variables)
285 values.push_back(new_variable);
286 return instantiate(values);
287}
288
290{
291 INVARIANT(
292 operands().size() % 2 == 0, "cond must have even number of operands");
293
294 exprt result = nil_exprt();
295
296 auto &operands = this->operands();
297
298 // functional version -- go backwards
299 for(std::size_t i = operands.size(); i != 0; i -= 2)
300 {
301 INVARIANT(
302 i >= 2,
303 "since the number of operands is even if i is nonzero it must be "
304 "greater than two");
305
306 const exprt &cond = operands[i - 2];
307 const exprt &value = operands[i - 1];
308
309 if(result.is_nil())
310 result = value;
311 else
312 result = if_exprt{cond, value, std::move(result)};
313 }
314
315 return result;
316}
configt config
Definition config.cpp:25
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:650
exprt & where()
Definition std_expr.h:3266
variablest & variables()
Definition std_expr.h:3256
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:250
std::vector< symbol_exprt > variablest
Definition std_expr.h:3237
exprt lower() const
Definition std_expr.cpp:289
struct configt::ansi_ct ansi_c
const irep_idt & get_value() const
Definition std_expr.h:3126
bool value_is_zero_string() const
Definition std_expr.cpp:19
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition std_expr.cpp:25
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.cpp:41
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The Boolean constant false.
Definition std_expr.h:3200
The trinary if-then-else operator.
Definition std_expr.h:2502
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:193
binding_exprt & binding()
Definition std_expr.h:3360
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
Definition std_expr.cpp:158
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:3031
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3209
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:29
Boolean OR.
Definition std_expr.h:2275
exprt & component(const irep_idt &name, const namespacet &ns)
Definition std_expr.cpp:139
Structure type, corresponds to C style structs.
Definition std_types.h:231
The Boolean constant true.
Definition std_expr.h:3191
The type of an expression, extends irept.
Definition type.h:29
with_exprt make_with_expr() const
converts an update expr into a (possibly nested) with expression
Definition std_expr.cpp:219
exprt::operandst & designator()
Definition std_expr.h:2809
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
bool is_false(const literalt &l)
Definition literal.h:197
API to expression classes for Pointers.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:71
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:122
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:83
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3456
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition std_expr.h:2714
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3173
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2661
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition std_types.h:478
std::optional< exprt > substitute_symbols(const std::map< irep_idt, exprt > &substitutions, exprt src)
Substitute free occurrences of the variables given by their identifiers in the keys of the map in the...
Symbol Substitution.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
validation_modet