cprover
constant_abstract_value.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
9 #include <array>
11 #include <langapi/language_util.h>
12 #include <util/arith_tools.h>
13 #include <util/ieee_float.h>
14 #include <util/namespace.h>
15 #include <util/simplify_expr.h>
16 #include <util/std_expr.h>
17 #include <util/type.h>
18 
19 #include "abstract_environment.h"
21 
23 {
24 public:
25  explicit constant_index_ranget(const exprt &val)
27  {
28  }
29 };
30 
32 {
33  return std::make_shared<constant_index_ranget>(val);
34 }
35 
37  : abstract_value_objectt(t), value()
38 {
39 }
40 
42  const typet &t,
43  bool tp,
44  bool bttm)
45  : abstract_value_objectt(t, tp, bttm), value()
46 {
47 }
48 
50  const exprt &e,
51  const abstract_environmentt &environment,
52  const namespacet &ns)
53  : abstract_value_objectt(e.type(), false, false), value(e)
54 {
55 }
56 
59 {
60  exprt val = to_constant();
61  if(!val.is_constant())
63 
64  return make_constant_index_range(val);
65 }
66 
68  const exprt &expr,
69  const std::vector<abstract_object_pointert> &operands,
70  const abstract_environmentt &environment,
71  const namespacet &ns) const
72 {
73  // try finding the rounding mode. If it's not constant, try
74  // seeing if we can get the same result with all rounding modes
75  auto rounding_mode_symbol =
76  symbol_exprt(CPROVER_PREFIX "rounding_mode", signedbv_typet(32));
77  auto rounding_mode_value = environment.eval(rounding_mode_symbol, ns);
78  auto rounding_mode_constant = rounding_mode_value->to_constant();
79  if(rounding_mode_constant.is_nil())
80  {
81  return try_transform_expr_with_all_rounding_modes(expr, environment, ns);
82  }
83 
84  exprt adjusted_expr = expr;
85  adjust_float_expressions(adjusted_expr, ns);
86  exprt constant_replaced_expr = adjusted_expr;
87  constant_replaced_expr.operands().clear();
88 
89  // Two passes over the expression - one for simplification,
90  // another to check if there are any top subexpressions left
91  for(const exprt &op : adjusted_expr.operands())
92  {
93  abstract_object_pointert lhs_abstract_object = environment.eval(op, ns);
94  const exprt &lhs_value = lhs_abstract_object->to_constant();
95  if(lhs_value.is_nil())
96  {
97  // do not give up if a sub-expression is not a constant,
98  // because the whole expression may still be simplified in some cases
99  constant_replaced_expr.operands().push_back(op);
100  }
101  else
102  {
103  // rebuild the operands list with constant versions of
104  // any symbols
105  constant_replaced_expr.operands().push_back(lhs_value);
106  }
107  }
108  exprt simplified = simplify_expr(constant_replaced_expr, ns);
109 
110  for(const exprt &op : simplified.operands())
111  {
112  abstract_object_pointert lhs_abstract_object = environment.eval(op, ns);
113  const exprt &lhs_value = lhs_abstract_object->to_constant();
114  if(lhs_value.is_nil())
115  {
116  return environment.abstract_object_factory(
117  simplified.type(), ns, true, false);
118  }
119  }
120 
121  return environment.abstract_object_factory(simplified.type(), simplified, ns);
122 }
123 
126  const exprt &expr,
127  const abstract_environmentt &environment,
128  const namespacet &ns) const
129 {
130  const symbol_exprt rounding_mode_symbol =
131  symbol_exprt(CPROVER_PREFIX "rounding_mode", signedbv_typet(32));
132  // NOLINTNEXTLINE (whitespace/braces)
133  auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
134  // NOLINTNEXTLINE (whitespace/braces)
138  // NOLINTNEXTLINE (whitespace/braces)
140  std::vector<abstract_object_pointert> possible_results;
141  for(auto current_rounding_mode : rounding_modes)
142  {
143  abstract_environmentt child_env(environment);
144  child_env.assign(
145  rounding_mode_symbol,
146  child_env.abstract_object_factory(
147  signedbv_typet(32),
148  from_integer(
149  mp_integer(static_cast<unsigned long>(current_rounding_mode)),
150  signedbv_typet(32)),
151  ns),
152  ns);
153 
154  // Dummy vector as the called expression_transform() ignores it
155  std::vector<abstract_object_pointert> dummy;
156  possible_results.push_back(
157  expression_transform(expr, dummy, child_env, ns));
158  }
159  auto first = possible_results.front()->to_constant();
160  for(auto const &possible_result : possible_results)
161  {
162  auto current = possible_result->to_constant();
163  if(current.is_nil() || current != first)
164  {
165  return environment.abstract_object_factory(expr.type(), ns, true, false);
166  }
167  }
168  return possible_results.front();
169 }
170 
172 {
173  if(!is_top() && !is_bottom())
174  {
175  return this->value;
176  }
177  else
178  {
180  }
181 }
182 
184  std::ostream &out,
185  const ai_baset &ai,
186  const namespacet &ns) const
187 {
188  if(!is_top() && !is_bottom())
189  {
191  }
192  else
193  {
194  abstract_objectt::output(out, ai, ns);
195  }
196 }
197 
200 {
202  std::dynamic_pointer_cast<const constant_abstract_valuet>(other);
203  if(cast_other)
204  {
205  return merge_constant_constant(cast_other);
206  }
207  else
208  {
209  // TODO(tkiley): How do we set the result to be toppish? Does it matter?
210  return abstract_objectt::merge(other);
211  }
212 }
213 
215  const constant_abstract_value_pointert &other) const
216 {
217  if(is_bottom())
218  {
219  return std::make_shared<constant_abstract_valuet>(*other);
220  }
221  else
222  {
223  // Can we actually merge these value
224  if(value == other->value)
225  {
226  return shared_from_this();
227  }
228  else
229  {
230  return abstract_objectt::merge(other);
231  }
232  }
233 }
234 
236  abstract_object_statisticst &statistics,
237  abstract_object_visitedt &visited,
238  const abstract_environmentt &env,
239  const namespacet &ns) const
240 {
241  abstract_objectt::get_statistics(statistics, visited, env, ns);
242  ++statistics.number_of_constants;
243  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
244 }
An abstract version of a program environment.
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
index_range_ptrt make_indeterminate_index_range()
std::shared_ptr< index_ranget > index_range_ptrt
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
virtual exprt to_constant() const
Converts to a constant expression if possible.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
abstract_object_pointert merge_constant_constant(const constant_abstract_value_pointert &other) const
Merges another constant abstract value into this one.
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
sharing_ptrt< constant_abstract_valuet > constant_abstract_value_pointert
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Attempts to do a constant/constant merge if both are constants, otherwise falls back to the parent me...
index_range_ptrt index_range(const namespacet &ns) const override
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_object_pointert try_transform_expr_with_all_rounding_modes(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) const
constant_index_ranget(const exprt &val)
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
operandst & operands()
Definition: expr.h:96
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:128
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:127
bool is_nil() const
Definition: irep.h:387
static memory_sizet from_bytes(std::size_t bytes)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1272
Expression to hold a symbol (variable)
Definition: std_expr.h:81
The type of an expression, extends irept.
Definition: type.h:28
index_range_ptrt make_constant_index_range(const exprt &val)
An abstraction of a single value that just stores a constant.
#define CPROVER_PREFIX
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
BigInt mp_integer
Definition: mp_arith.h:19
exprt simplify_expr(exprt src, const namespacet &ns)
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
Defines typet, type_with_subtypet and type_with_subtypest.