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 <util/namespace.h>
12 
13 #include "arith_tools.h"
14 #include "byte_operators.h"
15 #include "c_types.h"
16 #include "expr_util.h"
17 #include "mathematical_types.h"
18 #include "namespace.h"
19 #include "pointer_offset_size.h"
20 #include "range.h"
21 #include "simplify_expr.h"
22 
24 {
25  const std::string val=id2string(get_value());
26  return val.find_first_not_of('0')==std::string::npos;
27 }
28 
30 {
31  if(op.empty())
32  return false_exprt();
33  else if(op.size()==1)
34  return op.front();
35  else
36  {
37  return or_exprt(exprt::operandst(op));
38  }
39 }
40 
42 {
43  if(op.empty())
44  return true_exprt();
45  else if(op.size()==1)
46  return op.front();
47  else
48  {
49  return and_exprt(exprt::operandst(op));
50  }
51 }
52 
53 // Implementation of struct_exprt::component for const / non const overloads.
54 template <typename T>
55 auto component(T &struct_expr, const irep_idt &name, const namespacet &ns)
56  -> decltype(struct_expr.op0())
57 {
58  static_assert(
59  std::is_base_of<struct_exprt, T>::value, "T must be a struct_exprt.");
60  const auto index =
61  to_struct_type(ns.follow(struct_expr.type())).component_number(name);
63  index < struct_expr.operands().size(),
64  "component matching index should exist");
65  return struct_expr.operands()[index];
66 }
67 
70 {
71  return ::component(*this, name, ns);
72 }
73 
75 const exprt &
76 struct_exprt::component(const irep_idt &name, const namespacet &ns) const
77 {
78  return ::component(*this, name, ns);
79 }
80 
89  const exprt &expr,
90  const namespacet &ns,
91  const validation_modet vm)
92 {
93  check(expr, vm);
94 
95  const auto &member_expr = to_member_expr(expr);
96 
97  const typet &compound_type = ns.follow(member_expr.compound().type());
98  const auto *struct_union_type =
99  type_try_dynamic_cast<struct_union_typet>(compound_type);
100  DATA_CHECK(
101  vm,
102  struct_union_type != nullptr,
103  "member must address a struct, union or compatible type");
104 
105  const auto &component =
106  struct_union_type->get_component(member_expr.get_component_name());
107 
108  DATA_CHECK(
109  vm,
110  component.is_not_nil(),
111  "member component '" + id2string(member_expr.get_component_name()) +
112  "' must exist on addressed type");
113 
114  DATA_CHECK(
115  vm,
116  component.type() == member_expr.type(),
117  "member expression's type must match the addressed struct or union "
118  "component");
119 }
120 
121 void let_exprt::validate(const exprt &expr, const validation_modet vm)
122 {
123  check(expr, vm);
124 
125  const auto &let_expr = to_let_expr(expr);
126 
127  DATA_CHECK(
128  vm,
129  let_expr.values().size() == let_expr.variables().size(),
130  "number of variables must match number of values");
131 
132  for(const auto &binding :
133  make_range(let_expr.variables()).zip(let_expr.values()))
134  {
135  DATA_CHECK(
136  vm,
137  binding.first.id() == ID_symbol,
138  "let binding symbols must be symbols");
139 
140  DATA_CHECK(
141  vm,
142  binding.first.type() == binding.second.type(),
143  "let bindings must be type consistent");
144  }
145 }
Expression classes for byte-level operators.
Boolean AND.
Definition: std_expr.h:1835
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:563
const irep_idt & get_value() const
Definition: std_expr.h:2676
bool value_is_zero_string() const
Definition: std_expr.cpp:23
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2726
const irep_idt & id() const
Definition: irep.h:407
static void validate(const exprt &, validation_modet)
Definition: std_expr.cpp:121
binding_exprt & binding()
Definition: std_expr.h:2844
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:88
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2579
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Boolean OR.
Definition: std_expr.h:1943
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:69
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:50
The Boolean constant true.
Definition: std_expr.h:2717
The type of an expression, extends irept.
Definition: type.h:28
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
Mathematical types.
Pointer Logic.
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:511
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:41
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:29
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
API to expression classes.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:2940
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
#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