CBMC
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 "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 
24 void constant_exprt::check(const exprt &expr, const validation_modet vm)
25 {
26  DATA_CHECK(
27  vm, !expr.has_operands(), "constant expression must not have operands");
28 
29  DATA_CHECK(
30  vm,
32  !id2string(to_constant_expr(expr).get_value()).empty(),
33  "bitvector constant must have a non-empty value");
34 
35  DATA_CHECK(
36  vm,
40  .find_first_not_of("0123456789ABCDEF") == std::string::npos,
41  "negative bitvector constant must use two's complement");
42 
43  DATA_CHECK(
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.
76 template <typename T>
77 auto 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 
97 const exprt &
98 struct_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 =
121  type_try_dynamic_cast<struct_union_typet>(compound_type);
122  DATA_CHECK(
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 
130  DATA_CHECK(
131  vm,
132  component.is_not_nil(),
133  "member component '" + id2string(member_expr.get_component_name()) +
134  "' must exist on addressed type");
135 
136  DATA_CHECK(
137  vm,
138  component.type() == member_expr.type(),
139  "member expression's type must match the addressed struct or union "
140  "component");
141 }
142 
143 void 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 
149  DATA_CHECK(
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  {
157  DATA_CHECK(
158  vm,
159  binding.first.id() == ID_symbol,
160  "let binding symbols must be symbols");
161 
162  DATA_CHECK(
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'
191  auto substitute_result = substitute_symbols(substitutions, 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 
199 exprt 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 }
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
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition: std_expr.cpp:169
variablest & variables()
Definition: std_expr.h:3073
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
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: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.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:66
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: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 constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2992
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2886
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:899
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