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  {
97  // make sure we have binary expressions
98  if(expr.operands().size()>2)
99  expr=make_binary(expr);
100 
101  assert(expr.operands().size()==2);
102 
103  // now add rounding mode
104  expr.id(expr.id()==ID_plus?ID_floatbv_plus:
105  expr.id()==ID_minus?ID_floatbv_minus:
106  expr.id()==ID_mult?ID_floatbv_mult:
107  expr.id()==ID_div?ID_floatbv_div:
108  expr.id()==ID_rem?ID_floatbv_rem:
109  irep_idt());
110 
111  expr.operands().resize(3);
112  expr.op2()=rounding_mode;
113  }
114  }
115 
116  if(expr.id()==ID_typecast)
117  {
118  const typecast_exprt &typecast_expr=to_typecast_expr(expr);
119 
120  const typet &src_type=typecast_expr.op().type();
121  const typet &dest_type=typecast_expr.type();
122 
123  if(dest_type.id()==ID_floatbv &&
124  src_type.id()==ID_floatbv)
125  {
126  // Casts from bigger to smaller float-type might round.
127  // For smaller to bigger it is strictly redundant but
128  // we leave this optimisation until later to simplify
129  // the representation.
130  expr.id(ID_floatbv_typecast);
131  expr.operands().resize(2);
132  expr.op1()=rounding_mode;
133  }
134  else if(dest_type.id()==ID_floatbv &&
135  (src_type.id()==ID_c_bool ||
136  src_type.id()==ID_signedbv ||
137  src_type.id()==ID_unsignedbv ||
138  src_type.id()==ID_c_enum_tag))
139  {
140  // casts from integer to float-type might round
141  expr.id(ID_floatbv_typecast);
142  expr.operands().resize(2);
143  expr.op1()=rounding_mode;
144  }
145  else if((dest_type.id()==ID_signedbv ||
146  dest_type.id()==ID_unsignedbv ||
147  dest_type.id()==ID_c_enum_tag) &&
148  src_type.id()==ID_floatbv)
149  {
150  // In C, casts from float to integer always round to zero,
151  // irrespectively of the rounding mode that is currently set.
152  // We will have to consider other programming languages
153  // eventually.
154 
155  /* ISO 9899:1999
156  * 6.3.1.4 Real floating and integer
157  * 1 When a finite value of real floating type is converted
158  * to an integer type other than _Bool, the fractional part
159  * is discarded (i.e., the value is truncated toward zero).
160  */
161  expr.id(ID_floatbv_typecast);
162  expr.operands().resize(2);
163  expr.op1()=
164  from_integer(ieee_floatt::ROUND_TO_ZERO, rounding_mode.type());
165  }
166  }
167 }
168 
172 {
174  return;
175 
176  symbol_exprt rounding_mode =
177  ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
178 
179  rounding_mode.add_source_location() = expr.source_location();
180 
181  adjust_float_expressions(expr, rounding_mode);
182 }
183 
185  goto_functionst::goto_functiont &goto_function,
186  const namespacet &ns)
187 {
188  Forall_goto_program_instructions(it, goto_function.body)
189  {
190  adjust_float_expressions(it->code, ns);
191  adjust_float_expressions(it->guard, ns);
192  }
193 }
194 
196  goto_functionst &goto_functions,
197  const namespacet &ns)
198 {
199  Forall_goto_functions(it, goto_functions)
200  adjust_float_expressions(it->second, ns);
201 }
202 
204 {
205  namespacet ns(goto_model.symbol_table);
207 }
The type of an expression.
Definition: type.h:22
Symbolic Execution.
semantic type conversion
Definition: std_expr.h:2111
static bool have_to_adjust_float_expressions(const exprt &expr)
Symbol table entry.
#define CPROVER_PREFIX
const exprt & op() const
Definition: std_expr.h:340
Deprecated expression utility functions.
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
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:75
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
#define forall_operands(it, expr)
Definition: expr.h:17
Base class for all expressions.
Definition: expr.h:42
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:125
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
source_locationt & add_source_location()
Definition: expr.h:130
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
dstringt irep_idt
Definition: irep.h:32
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
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:35
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136