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 "range.h"
13
14#include <map>
15
17{
18 const std::string val=id2string(get_value());
19 return val.find_first_not_of('0')==std::string::npos;
20}
21
23{
24 if(op.empty())
25 return false_exprt();
26 else if(op.size()==1)
27 return op.front();
28 else
29 {
30 return or_exprt(exprt::operandst(op));
31 }
32}
33
35{
36 if(op.empty())
37 return true_exprt();
38 else if(op.size()==1)
39 return op.front();
40 else
41 {
42 return and_exprt(exprt::operandst(op));
43 }
44}
45
46// Implementation of struct_exprt::component for const / non const overloads.
47template <typename T>
48auto component(T &struct_expr, const irep_idt &name, const namespacet &ns)
49 -> decltype(struct_expr.op0())
50{
51 static_assert(
52 std::is_base_of<struct_exprt, T>::value, "T must be a struct_exprt.");
53 const auto index =
54 to_struct_type(ns.follow(struct_expr.type())).component_number(name);
56 index < struct_expr.operands().size(),
57 "component matching index should exist");
58 return struct_expr.operands()[index];
59}
60
63{
64 return ::component(*this, name, ns);
65}
66
68const exprt &
69struct_exprt::component(const irep_idt &name, const namespacet &ns) const
70{
71 return ::component(*this, name, ns);
72}
73
82 const exprt &expr,
83 const namespacet &ns,
84 const validation_modet vm)
85{
86 check(expr, vm);
87
88 const auto &member_expr = to_member_expr(expr);
89
90 const typet &compound_type = ns.follow(member_expr.compound().type());
91 const auto *struct_union_type =
94 vm,
95 struct_union_type != nullptr,
96 "member must address a struct, union or compatible type");
97
98 const auto &component =
99 struct_union_type->get_component(member_expr.get_component_name());
100
102 vm,
103 component.is_not_nil(),
104 "member component '" + id2string(member_expr.get_component_name()) +
105 "' must exist on addressed type");
106
108 vm,
109 component.type() == member_expr.type(),
110 "member expression's type must match the addressed struct or union "
111 "component");
112}
113
114void let_exprt::validate(const exprt &expr, const validation_modet vm)
115{
116 check(expr, vm);
117
118 const auto &let_expr = to_let_expr(expr);
119
121 vm,
122 let_expr.values().size() == let_expr.variables().size(),
123 "number of variables must match number of values");
124
125 for(const auto &binding :
126 make_range(let_expr.variables()).zip(let_expr.values()))
127 {
129 vm,
130 binding.first.id() == ID_symbol,
131 "let binding symbols must be symbols");
132
134 vm,
135 binding.first.type() == binding.second.type(),
136 "let bindings must be type consistent");
137 }
138}
139
141 const std::map<irep_idt, exprt> &substitutions,
142 exprt src)
143{
144 if(src.id() == ID_symbol)
145 {
147 if(s_it == substitutions.end())
148 return {};
149 else
150 return s_it->second;
151 }
152 else if(
153 src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
154 {
155 const auto &binding_expr = to_binding_expr(src);
156
157 // bindings may be nested,
158 // which may hide some of our substitutions
160 for(const auto &variable : binding_expr.variables())
161 new_substitutions.erase(variable.get_identifier());
162
163 auto op_result =
165 if(op_result.has_value())
166 return binding_exprt(
167 src.id(),
168 binding_expr.variables(),
169 op_result.value(),
170 binding_expr.type());
171 else
172 return {};
173 }
174 else if(src.id() == ID_let)
175 {
176 auto new_let_expr = to_let_expr(src); // copy
177 const auto &binding_expr = to_let_expr(src).binding();
178
179 // bindings may be nested,
180 // which may hide some of our substitutions
182 for(const auto &variable : binding_expr.variables())
183 new_substitutions.erase(variable.get_identifier());
184
185 bool op_changed = false;
186
187 for(auto &op : new_let_expr.values())
188 {
190
191 if(op_result.has_value())
192 {
193 op = op_result.value();
194 op_changed = true;
195 }
196 }
197
198 auto op_result =
200 if(op_result.has_value())
201 {
202 new_let_expr.where() = op_result.value();
203 op_changed = true;
204 }
205
206 if(op_changed)
207 return std::move(new_let_expr);
208 else
209 return {};
210 }
211
212 if(!src.has_operands())
213 return {};
214
215 bool op_changed = false;
216
217 for(auto &op : src.operands())
218 {
220
221 if(op_result.has_value())
222 {
223 op = op_result.value();
224 op_changed = true;
225 }
226 }
227
228 if(op_changed)
229 return src;
230 else
231 return {};
232}
233
235{
236 // number of values must match the number of bound variables
237 auto &variables = this->variables();
238 PRECONDITION(variables.size() == values.size());
239
240 std::map<symbol_exprt, exprt> value_map;
241
242 for(std::size_t i = 0; i < variables.size(); i++)
243 {
244 // types must match
245 PRECONDITION(variables[i].type() == values[i].type());
246 value_map[variables[i]] = values[i];
247 }
248
249 // build a substitution map
250 std::map<irep_idt, exprt> substitutions;
251
252 for(std::size_t i = 0; i < variables.size(); i++)
254
255 // now recurse downwards and substitute in 'where'
257
258 if(substitute_result.has_value())
259 return substitute_result.value();
260 else
261 return where(); // trivial case, variables not used
262}
263
264exprt binding_exprt::instantiate(const variablest &new_variables) const
265{
266 std::vector<exprt> values;
267 values.reserve(new_variables.size());
268 for(const auto &new_variable : new_variables)
269 values.push_back(new_variable);
270 return instantiate(values);
271}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Boolean AND.
Definition std_expr.h:1974
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:562
A base class for variable bindings (quantifiers, let, lambda)
Definition std_expr.h:2900
exprt & where()
Definition std_expr.h:2931
variablest & variables()
Definition std_expr.h:2921
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:234
std::vector< symbol_exprt > variablest
Definition std_expr.h:2902
const irep_idt & get_value() const
Definition std_expr.h:2815
bool value_is_zero_string() const
Definition std_expr.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:89
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
The Boolean constant false.
Definition std_expr.h:2865
const irep_idt & id() const
Definition irep.h:396
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:114
binding_exprt & binding()
Definition std_expr.h:3001
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:81
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2718
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:2082
exprt & component(const irep_idt &name, const namespacet &ns)
Definition std_expr.cpp:62
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition std_types.cpp:40
The Boolean constant true.
Definition std_expr.h:2856
The type of an expression, extends irept.
Definition type.h:29
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#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:34
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:22
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:48
static optionalt< exprt > substitute_symbols_rec(const std::map< irep_idt, exprt > &substitutions, exprt src)
Definition std_expr.cpp:140
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3097
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition std_expr.h:2962
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
#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