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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
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:41
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
typet
The type of an expression, extends irept.
Definition: type.h:28
and_exprt
Boolean AND.
Definition: std_expr.h:1835
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:55
let_exprt::validate
static void validate(const exprt &, validation_modet)
Definition: std_expr.cpp:121
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:50
mathematical_types.h
Mathematical types.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
byte_operators.h
Expression classes for byte-level operators.
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:29
or_exprt
Boolean OR.
Definition: std_expr.h:1943
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:511
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:2579
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:2940
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:88
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:563
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
false_exprt
The Boolean constant false.
Definition: std_expr.h:2726
simplify_expr.h
expr_util.h
Deprecated expression utility functions.
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:23
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
struct_exprt::component
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:69
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
std_expr.h
API to expression classes.
let_exprt::binding
binding_exprt & binding()
Definition: std_expr.h:2844
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2676
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
c_types.h