cprover
adjust_float_expressions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/cprover_prefix.h>
15 #include <util/expr_util.h>
16 #include <util/std_expr.h>
17 #include <util/symbol.h>
18 #include <util/ieee_float.h>
19 #include <util/arith_tools.h>
20 
21 #include "goto_model.h"
22 
23 static bool have_to_adjust_float_expressions(const exprt &expr)
24 {
25  if(expr.id()==ID_floatbv_plus ||
26  expr.id()==ID_floatbv_minus ||
27  expr.id()==ID_floatbv_mult ||
28  expr.id()==ID_floatbv_div ||
29  expr.id()==ID_floatbv_div ||
30  expr.id()==ID_floatbv_rem ||
31  expr.id()==ID_floatbv_typecast)
32  return false;
33 
34  const typet &type = expr.type();
35 
36  if(
37  type.id() == ID_floatbv ||
38  (type.id() == ID_complex && type.subtype().id() == ID_floatbv))
39  {
40  if(expr.id()==ID_plus || expr.id()==ID_minus ||
41  expr.id()==ID_mult || expr.id()==ID_div ||
42  expr.id()==ID_rem)
43  return true;
44  }
45 
46  if(expr.id()==ID_typecast)
47  {
48  const typecast_exprt &typecast_expr=to_typecast_expr(expr);
49 
50  const typet &src_type=typecast_expr.op().type();
51  const typet &dest_type=typecast_expr.type();
52 
53  if(dest_type.id()==ID_floatbv &&
54  src_type.id()==ID_floatbv)
55  return true;
56  else if(dest_type.id()==ID_floatbv &&
57  (src_type.id()==ID_c_bool ||
58  src_type.id()==ID_signedbv ||
59  src_type.id()==ID_unsignedbv ||
60  src_type.id()==ID_c_enum_tag))
61  return true;
62  else if((dest_type.id()==ID_signedbv ||
63  dest_type.id()==ID_unsignedbv ||
64  dest_type.id()==ID_c_enum_tag) &&
65  src_type.id()==ID_floatbv)
66  return true;
67  }
68 
69  forall_operands(it, expr)
71  return true;
72 
73  return false;
74 }
75 
78 void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
79 {
81  return;
82 
83  // recursive call
84  for(auto &op : expr.operands())
85  adjust_float_expressions(op, rounding_mode);
86 
87  const typet &type = expr.type();
88 
89  if(
90  type.id() == ID_floatbv ||
91  (type.id() == ID_complex && type.subtype().id() == ID_floatbv))
92  {
93  if(expr.id()==ID_plus || expr.id()==ID_minus ||
94  expr.id()==ID_mult || expr.id()==ID_div ||
95  expr.id()==ID_rem)
96  {
98  expr.operands().size() >= 2,
99  "arithmetic operations must have two or more operands");
100 
101  // make sure we have binary expressions
102  if(expr.operands().size()>2)
103  {
104  expr=make_binary(expr);
105  CHECK_RETURN(expr.operands().size() == 2);
106  }
107 
108  // now add rounding mode
109  expr.id(expr.id()==ID_plus?ID_floatbv_plus:
110  expr.id()==ID_minus?ID_floatbv_minus:
111  expr.id()==ID_mult?ID_floatbv_mult:
112  expr.id()==ID_div?ID_floatbv_div:
113  expr.id()==ID_rem?ID_floatbv_rem:
114  irep_idt());
115 
116  expr.operands().resize(3);
117  expr.op2()=rounding_mode;
118  }
119  }
120 
121  if(expr.id()==ID_typecast)
122  {
123  const typecast_exprt &typecast_expr=to_typecast_expr(expr);
124 
125  const typet &src_type=typecast_expr.op().type();
126  const typet &dest_type=typecast_expr.type();
127 
128  if(dest_type.id()==ID_floatbv &&
129  src_type.id()==ID_floatbv)
130  {
131  // Casts from bigger to smaller float-type might round.
132  // For smaller to bigger it is strictly redundant but
133  // we leave this optimisation until later to simplify
134  // the representation.
135  expr.id(ID_floatbv_typecast);
136  expr.operands().resize(2);
137  expr.op1()=rounding_mode;
138  }
139  else if(dest_type.id()==ID_floatbv &&
140  (src_type.id()==ID_c_bool ||
141  src_type.id()==ID_signedbv ||
142  src_type.id()==ID_unsignedbv ||
143  src_type.id()==ID_c_enum_tag))
144  {
145  // casts from integer to float-type might round
146  expr.id(ID_floatbv_typecast);
147  expr.operands().resize(2);
148  expr.op1()=rounding_mode;
149  }
150  else if((dest_type.id()==ID_signedbv ||
151  dest_type.id()==ID_unsignedbv ||
152  dest_type.id()==ID_c_enum_tag) &&
153  src_type.id()==ID_floatbv)
154  {
155  // In C, casts from float to integer always round to zero,
156  // irrespectively of the rounding mode that is currently set.
157  // We will have to consider other programming languages
158  // eventually.
159 
160  /* ISO 9899:1999
161  * 6.3.1.4 Real floating and integer
162  * 1 When a finite value of real floating type is converted
163  * to an integer type other than _Bool, the fractional part
164  * is discarded (i.e., the value is truncated toward zero).
165  */
166  expr.id(ID_floatbv_typecast);
167  expr.operands().resize(2);
168  expr.op1()=
169  from_integer(ieee_floatt::ROUND_TO_ZERO, rounding_mode.type());
170  }
171  }
172 }
173 
177 {
179  return;
180 
181  symbol_exprt rounding_mode =
182  ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
183 
184  rounding_mode.add_source_location() = expr.source_location();
185 
186  adjust_float_expressions(expr, rounding_mode);
187 }
188 
190  goto_functionst::goto_functiont &goto_function,
191  const namespacet &ns)
192 {
193  Forall_goto_program_instructions(it, goto_function.body)
194  {
195  adjust_float_expressions(it->code, ns);
196  adjust_float_expressions(it->guard, ns);
197  }
198 }
199 
201  goto_functionst &goto_functions,
202  const namespacet &ns)
203 {
204  Forall_goto_functions(it, goto_functions)
205  adjust_float_expressions(it->second, ns);
206 }
207 
209 {
210  namespacet ns(goto_model.symbol_table);
212 }
The type of an expression, extends irept.
Definition: type.h:27
Symbolic Execution.
Semantic type conversion.
Definition: std_expr.h:2277
static bool have_to_adjust_float_expressions(const exprt &expr)
Symbol table entry.
#define CPROVER_PREFIX
const exprt & op() const
Definition: std_expr.h:371
Deprecated expression utility functions.
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
const irep_idt & id() const
Definition: irep.h:259
Symbol Table + CFG.
API to expression classes.
exprt & op1()
Definition: expr.h:87
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
#define forall_operands(it, expr)
Definition: expr.h:20
A collection of goto functions.
Base class for all expressions.
Definition: expr.h:54
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:228
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
source_locationt & add_source_location()
Definition: expr.h:233
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:143
exprt & op2()
Definition: expr.h:90
dstringt irep_idt
Definition: irep.h:32
const typet & subtype() const
Definition: type.h:38
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:36
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166