cprover
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 "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.
47 template <typename T>
48 auto 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 
68 const exprt &
69 struct_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 =
92  type_try_dynamic_cast<struct_union_typet>(compound_type);
93  DATA_CHECK(
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 
101  DATA_CHECK(
102  vm,
103  component.is_not_nil(),
104  "member component '" + id2string(member_expr.get_component_name()) +
105  "' must exist on addressed type");
106 
107  DATA_CHECK(
108  vm,
109  component.type() == member_expr.type(),
110  "member expression's type must match the addressed struct or union "
111  "component");
112 }
113 
114 void 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 
120  DATA_CHECK(
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  {
128  DATA_CHECK(
129  vm,
130  binding.first.id() == ID_symbol,
131  "let binding symbols must be symbols");
132 
133  DATA_CHECK(
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  {
146  auto s_it = substitutions.find(to_symbol_expr(src).get_identifier());
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
159  auto new_substitutions = substitutions;
160  for(const auto &variable : binding_expr.variables())
161  new_substitutions.erase(variable.get_identifier());
162 
163  auto op_result =
164  substitute_symbols_rec(new_substitutions, binding_expr.where());
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
181  auto new_substitutions = 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  {
189  auto op_result = substitute_symbols_rec(new_substitutions, op);
190 
191  if(op_result.has_value())
192  {
193  op = op_result.value();
194  op_changed = true;
195  }
196  }
197 
198  auto op_result =
199  substitute_symbols_rec(new_substitutions, binding_expr.where());
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  {
219  auto op_result = substitute_symbols_rec(substitutions, op);
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++)
253  substitutions[variables[i].get_identifier()] = values[i];
254 
255  // now recurse downwards and substitute in 'where'
256  auto substitute_result = substitute_symbols_rec(substitutions, 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 
264 exprt 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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
conjunction
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
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
typet
The type of an expression, extends irept.
Definition: type.h:28
and_exprt
Boolean AND.
Definition: std_expr.h:1920
exprt
Base class for all expressions.
Definition: expr.h:54
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
let_exprt::validate
static void validate(const exprt &, validation_modet)
Definition: std_expr.cpp:114
namespace.h
struct_union_typet::component_number
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:32
binding_exprt::variables
variablest & variables()
Definition: std_expr.h:2867
substitute_symbols_rec
static optionalt< exprt > substitute_symbols_rec(const std::map< irep_idt, exprt > &substitutions, exprt src)
Definition: std_expr.cpp:140
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
disjunction
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
or_exprt
Boolean OR.
Definition: std_expr.h:2028
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
member_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2664
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3043
binding_exprt::variablest
std::vector< symbol_exprt > variablest
Definition: std_expr.h:2848
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
member_exprt::validate
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
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::id
const irep_idt & id() const
Definition: irep.h:407
binary_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:562
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
binding_exprt
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:2846
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
binding_exprt::where
exprt & where()
Definition: std_expr.h:2877
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:16
binding_exprt::instantiate
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition: std_expr.cpp:234
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
struct_exprt::component
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:62
exprt::operands
operandst & operands()
Definition: expr.h:92
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
to_binding_expr
const binding_exprt & to_binding_expr(const exprt &expr)
Cast an exprt to a binding_exprt.
Definition: std_expr.h:2908
std_expr.h
API to expression classes.
let_exprt::binding
binding_exprt & binding()
Definition: std_expr.h:2947
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2761
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524