cprover
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 "namespace.h"
12#include "pointer_expr.h"
13#include "range.h"
14#include "substitute_symbols.h"
15
16#include <map>
17
19{
20 const std::string val=id2string(get_value());
21 return val.find_first_not_of('0')==std::string::npos;
22}
23
24void constant_exprt::check(const exprt &expr, const validation_modet vm)
25{
27 vm, !expr.has_operands(), "constant expression must not have operands");
28
30 vm,
32 !id2string(to_constant_expr(expr).get_value()).empty(),
33 "bitvector constant must have a non-empty value");
34
36 vm,
40 .find_first_not_of("0123456789ABCDEF") == std::string::npos,
41 "negative bitvector constant must use two's complement");
42
44 vm,
46 to_constant_expr(expr).get_value() == ID_0 ||
47 id2string(to_constant_expr(expr).get_value())[0] != '0',
48 "bitvector constant must not have leading zeros");
49}
50
52{
53 if(op.empty())
54 return false_exprt();
55 else if(op.size()==1)
56 return op.front();
57 else
58 {
59 return or_exprt(exprt::operandst(op));
60 }
61}
62
64{
65 if(op.empty())
66 return true_exprt();
67 else if(op.size()==1)
68 return op.front();
69 else
70 {
71 return and_exprt(exprt::operandst(op));
72 }
73}
74
75// Implementation of struct_exprt::component for const / non const overloads.
76template <typename T>
77auto component(T &struct_expr, const irep_idt &name, const namespacet &ns)
78 -> decltype(struct_expr.op0())
79{
80 static_assert(
81 std::is_base_of<struct_exprt, T>::value, "T must be a struct_exprt.");
82 const auto index =
83 to_struct_type(ns.follow(struct_expr.type())).component_number(name);
85 index < struct_expr.operands().size(),
86 "component matching index should exist");
87 return struct_expr.operands()[index];
88}
89
92{
93 return ::component(*this, name, ns);
94}
95
97const exprt &
98struct_exprt::component(const irep_idt &name, const namespacet &ns) const
99{
100 return ::component(*this, name, ns);
101}
102
111 const exprt &expr,
112 const namespacet &ns,
113 const validation_modet vm)
114{
115 check(expr, vm);
116
117 const auto &member_expr = to_member_expr(expr);
118
119 const typet &compound_type = ns.follow(member_expr.compound().type());
120 const auto *struct_union_type =
123 vm,
124 struct_union_type != nullptr,
125 "member must address a struct, union or compatible type");
126
127 const auto &component =
128 struct_union_type->get_component(member_expr.get_component_name());
129
131 vm,
132 component.is_not_nil(),
133 "member component '" + id2string(member_expr.get_component_name()) +
134 "' must exist on addressed type");
135
137 vm,
138 component.type() == member_expr.type(),
139 "member expression's type must match the addressed struct or union "
140 "component");
141}
142
143void let_exprt::validate(const exprt &expr, const validation_modet vm)
144{
145 check(expr, vm);
146
147 const auto &let_expr = to_let_expr(expr);
148
150 vm,
151 let_expr.values().size() == let_expr.variables().size(),
152 "number of variables must match number of values");
153
154 for(const auto &binding :
155 make_range(let_expr.variables()).zip(let_expr.values()))
156 {
158 vm,
159 binding.first.id() == ID_symbol,
160 "let binding symbols must be symbols");
161
163 vm,
164 binding.first.type() == binding.second.type(),
165 "let bindings must be type consistent");
166 }
167}
168
170{
171 // number of values must match the number of bound variables
172 auto &variables = this->variables();
173 PRECONDITION(variables.size() == values.size());
174
175 std::map<symbol_exprt, exprt> value_map;
176
177 for(std::size_t i = 0; i < variables.size(); i++)
178 {
179 // types must match
180 PRECONDITION(variables[i].type() == values[i].type());
181 value_map[variables[i]] = values[i];
182 }
183
184 // build a substitution map
185 std::map<irep_idt, exprt> substitutions;
186
187 for(std::size_t i = 0; i < variables.size(); i++)
188 substitutions[variables[i].get_identifier()] = values[i];
189
190 // now recurse downwards and substitute in 'where'
192
193 if(substitute_result.has_value())
194 return substitute_result.value();
195 else
196 return where(); // trivial case, variables not used
197}
198
199exprt binding_exprt::instantiate(const variablest &new_variables) const
200{
201 std::vector<exprt> values;
202 values.reserve(new_variables.size());
203 for(const auto &new_variable : new_variables)
204 values.push_back(new_variable);
205 return instantiate(values);
206}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Boolean AND.
Definition std_expr.h:2071
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:595
exprt & where()
Definition std_expr.h:3083
variablest & variables()
Definition std_expr.h:3073
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:169
std::vector< symbol_exprt > variablest
Definition std_expr.h:3054
const irep_idt & get_value() const
Definition std_expr.h:2950
bool value_is_zero_string() const
Definition std_expr.cpp:18
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.cpp:24
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:91
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3017
const irep_idt & id() const
Definition irep.h:396
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:143
binding_exprt & binding()
Definition std_expr.h:3177
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:110
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2853
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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
Boolean OR.
Definition std_expr.h:2179
exprt & component(const irep_idt &name, const namespacet &ns)
Definition std_expr.cpp:91
The Boolean constant true.
Definition std_expr.h:3008
The type of an expression, extends irept.
Definition type.h:29
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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:524
#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
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:63
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:51
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:77
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3273
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
optionalt< 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