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{
26 nullary_exprt::check(expr, vm);
27
28 const auto value = expr.get(ID_value);
29
31 vm,
32 !can_cast_type<bitvector_typet>(expr.type()) || !value.empty(),
33 "bitvector constant must have a non-empty value");
34
36 vm,
39 expr.type().id() == ID_verilog_unsignedbv ||
40 expr.type().id() == ID_verilog_signedbv ||
41 id2string(value).find_first_not_of("0123456789ABCDEF") ==
42 std::string::npos,
43 "negative bitvector constant must use two's complement");
44
46 vm,
48 expr.type().id() == ID_verilog_unsignedbv ||
49 expr.type().id() == ID_verilog_signedbv || value == ID_0 ||
50 id2string(value)[0] != '0',
51 "bitvector constant must not have leading zeros");
52}
53
55{
56 if(op.empty())
57 return false_exprt();
58 else if(op.size()==1)
59 return op.front();
60 else
61 {
62 return or_exprt(exprt::operandst(op));
63 }
64}
65
67{
68 if(op.empty())
69 return true_exprt();
70 else if(op.size()==1)
71 return op.front();
72 else
73 {
74 return and_exprt(exprt::operandst(op));
75 }
76}
77
78// Implementation of struct_exprt::component for const / non const overloads.
79template <typename T>
80auto component(T &struct_expr, const irep_idt &name, const namespacet &ns)
81 -> decltype(struct_expr.op0())
82{
83 static_assert(
84 std::is_base_of<struct_exprt, T>::value, "T must be a struct_exprt.");
85 const struct_typet &struct_type =
86 struct_expr.type().id() == ID_struct_tag
87 ? ns.follow_tag(to_struct_tag_type(struct_expr.type()))
88 : to_struct_type(struct_expr.type());
89 const auto index = struct_type.component_number(name);
91 index < struct_expr.operands().size(),
92 "component matching index should exist");
93 return struct_expr.operands()[index];
94}
95
98{
99 return ::component(*this, name, ns);
100}
101
103const exprt &
104struct_exprt::component(const irep_idt &name, const namespacet &ns) const
105{
106 return ::component(*this, name, ns);
107}
108
117 const exprt &expr,
118 const namespacet &ns,
119 const validation_modet vm)
120{
121 check(expr, vm);
122
123 const auto &member_expr = to_member_expr(expr);
124
125 const typet &compound_type = member_expr.compound().type();
126 const auto *struct_union_type =
127 (compound_type.id() == ID_struct_tag || compound_type.id() == ID_union_tag)
128 ? &ns.follow_tag(to_struct_or_union_tag_type(compound_type))
131 vm,
132 struct_union_type != nullptr,
133 "member must address a struct, union or compatible type");
134
135 const auto &component =
136 struct_union_type->get_component(member_expr.get_component_name());
137
139 vm,
140 component.is_not_nil(),
141 "member component '" + id2string(member_expr.get_component_name()) +
142 "' must exist on addressed type");
143
145 vm,
146 component.type() == member_expr.type(),
147 "member expression's type must match the addressed struct or union "
148 "component");
149}
150
151void let_exprt::validate(const exprt &expr, const validation_modet vm)
152{
153 check(expr, vm);
154
155 const auto &let_expr = to_let_expr(expr);
156
158 vm,
159 let_expr.values().size() == let_expr.variables().size(),
160 "number of variables must match number of values");
161
162 for(const auto &binding :
163 make_range(let_expr.variables()).zip(let_expr.values()))
164 {
166 vm,
167 binding.first.id() == ID_symbol,
168 "let binding symbols must be symbols");
169
171 vm,
172 binding.first.type() == binding.second.type(),
173 "let bindings must be type consistent");
174 }
175}
176
178{
179 // number of values must match the number of bound variables
180 auto &variables = this->variables();
181 PRECONDITION(variables.size() == values.size());
182
183 std::map<symbol_exprt, exprt> value_map;
184
185 for(std::size_t i = 0; i < variables.size(); i++)
186 {
187 // types must match
188 PRECONDITION(variables[i].type() == values[i].type());
189 value_map[variables[i]] = values[i];
190 }
191
192 // build a substitution map
193 std::map<irep_idt, exprt> substitutions;
194
195 for(std::size_t i = 0; i < variables.size(); i++)
196 substitutions[variables[i].get_identifier()] = values[i];
197
198 // now recurse downwards and substitute in 'where'
199 auto substitute_result = substitute_symbols(substitutions, where());
200
201 if(substitute_result.has_value())
202 return substitute_result.value();
203 else
204 return where(); // trivial case, variables not used
205}
206
207exprt binding_exprt::instantiate(const variablest &new_variables) const
208{
209 std::vector<exprt> values;
210 values.reserve(new_variables.size());
211 for(const auto &new_variable : new_variables)
212 values.push_back(new_variable);
213 return instantiate(values);
214}
Boolean AND.
Definition std_expr.h:2120
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:650
exprt & where()
Definition std_expr.h:3130
variablest & variables()
Definition std_expr.h:3120
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:177
std::vector< symbol_exprt > variablest
Definition std_expr.h:3101
const irep_idt & get_value() const
Definition std_expr.h:2995
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: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
The Boolean constant false.
Definition std_expr.h:3064
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
static void validate(const exprt &, validation_modet)
Definition std_expr.cpp:151
binding_exprt & binding()
Definition std_expr.h:3224
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:116
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:2900
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:29
Boolean OR.
Definition std_expr.h:2228
exprt & component(const irep_idt &name, const namespacet &ns)
Definition std_expr.cpp:97
Structure type, corresponds to C style structs.
Definition std_types.h:231
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:46
The Boolean constant true.
Definition std_expr.h:3055
The type of an expression, extends irept.
Definition type.h:29
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
Definition expr_cast.h:135
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
API to expression classes for Pointers.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
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 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:66
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:54
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:80
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3320
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2933
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
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition std_types.h:943
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