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 
24  const exprt &expr,
25  const namespacet &ns)
26 {
27  if(expr.id()==ID_floatbv_plus ||
28  expr.id()==ID_floatbv_minus ||
29  expr.id()==ID_floatbv_mult ||
30  expr.id()==ID_floatbv_div ||
31  expr.id()==ID_floatbv_div ||
32  expr.id()==ID_floatbv_rem ||
33  expr.id()==ID_floatbv_typecast)
34  return false;
35 
36  const typet &type=ns.follow(expr.type());
37 
38  if(type.id()==ID_floatbv ||
39  (type.id()==ID_complex &&
40  ns.follow(type.subtype()).id()==ID_floatbv))
41  {
42  if(expr.id()==ID_plus || expr.id()==ID_minus ||
43  expr.id()==ID_mult || expr.id()==ID_div ||
44  expr.id()==ID_rem)
45  return true;
46  }
47 
48  if(expr.id()==ID_typecast)
49  {
50  const typecast_exprt &typecast_expr=to_typecast_expr(expr);
51 
52  const typet &src_type=typecast_expr.op().type();
53  const typet &dest_type=typecast_expr.type();
54 
55  if(dest_type.id()==ID_floatbv &&
56  src_type.id()==ID_floatbv)
57  return true;
58  else if(dest_type.id()==ID_floatbv &&
59  (src_type.id()==ID_c_bool ||
60  src_type.id()==ID_signedbv ||
61  src_type.id()==ID_unsignedbv ||
62  src_type.id()==ID_c_enum_tag))
63  return true;
64  else if((dest_type.id()==ID_signedbv ||
65  dest_type.id()==ID_unsignedbv ||
66  dest_type.id()==ID_c_enum_tag) &&
67  src_type.id()==ID_floatbv)
68  return true;
69  }
70 
71  forall_operands(it, expr)
73  return true;
74 
75  return false;
76 }
77 
81  exprt &expr,
82  const namespacet &ns)
83 {
85  return;
86 
87  Forall_operands(it, expr)
88  adjust_float_expressions(*it, ns);
89 
90  const typet &type=ns.follow(expr.type());
91 
92  if(type.id()==ID_floatbv ||
93  (type.id()==ID_complex &&
94  ns.follow(type.subtype()).id()==ID_floatbv))
95  {
96  symbol_exprt rounding_mode=
97  ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
98 
99  rounding_mode.add_source_location()=expr.source_location();
100 
101  if(expr.id()==ID_plus || expr.id()==ID_minus ||
102  expr.id()==ID_mult || expr.id()==ID_div ||
103  expr.id()==ID_rem)
104  {
105  // make sure we have binary expressions
106  if(expr.operands().size()>2)
107  expr=make_binary(expr);
108 
109  assert(expr.operands().size()==2);
110 
111  // now add rounding mode
112  expr.id(expr.id()==ID_plus?ID_floatbv_plus:
113  expr.id()==ID_minus?ID_floatbv_minus:
114  expr.id()==ID_mult?ID_floatbv_mult:
115  expr.id()==ID_div?ID_floatbv_div:
116  expr.id()==ID_rem?ID_floatbv_rem:
117  irep_idt());
118 
119  expr.operands().resize(3);
120  expr.op2()=rounding_mode;
121  }
122  }
123 
124  if(expr.id()==ID_typecast)
125  {
126  const typecast_exprt &typecast_expr=to_typecast_expr(expr);
127 
128  const typet &src_type=typecast_expr.op().type();
129  const typet &dest_type=typecast_expr.type();
130 
131  symbol_exprt rounding_mode=
132  ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
133 
134  rounding_mode.add_source_location()=expr.source_location();
135 
136  if(dest_type.id()==ID_floatbv &&
137  src_type.id()==ID_floatbv)
138  {
139  // Casts from bigger to smaller float-type might round.
140  // For smaller to bigger it is strictly redundant but
141  // we leave this optimisation until later to simplify
142  // the representation.
143  expr.id(ID_floatbv_typecast);
144  expr.operands().resize(2);
145  expr.op1()=rounding_mode;
146  }
147  else if(dest_type.id()==ID_floatbv &&
148  (src_type.id()==ID_c_bool ||
149  src_type.id()==ID_signedbv ||
150  src_type.id()==ID_unsignedbv ||
151  src_type.id()==ID_c_enum_tag))
152  {
153  // casts from integer to float-type might round
154  expr.id(ID_floatbv_typecast);
155  expr.operands().resize(2);
156  expr.op1()=rounding_mode;
157  }
158  else if((dest_type.id()==ID_signedbv ||
159  dest_type.id()==ID_unsignedbv ||
160  dest_type.id()==ID_c_enum_tag) &&
161  src_type.id()==ID_floatbv)
162  {
163  // In C, casts from float to integer always round to zero,
164  // irrespectively of the rounding mode that is currently set.
165  // We will have to consider other programming languages
166  // eventually.
167 
168  /* ISO 9899:1999
169  * 6.3.1.4 Real floating and integer
170  * 1 When a finite value of real floating type is converted
171  * to an integer type other than _Bool, the fractional part
172  * is discarded (i.e., the value is truncated toward zero).
173  */
174  expr.id(ID_floatbv_typecast);
175  expr.operands().resize(2);
176  expr.op1()=
177  from_integer(ieee_floatt::ROUND_TO_ZERO, rounding_mode.type());
178  }
179  }
180 }
181 
183  goto_functionst::goto_functiont &goto_function,
184  const namespacet &ns)
185 {
186  Forall_goto_program_instructions(it, goto_function.body)
187  {
188  adjust_float_expressions(it->code, ns);
189  adjust_float_expressions(it->guard, ns);
190  }
191 }
192 
194  goto_functionst &goto_functions,
195  const namespacet &ns)
196 {
197  Forall_goto_functions(it, goto_functions)
198  adjust_float_expressions(it->second, ns);
199 }
200 
202 {
203  namespacet ns(goto_model.symbol_table);
205 }
The type of an expression.
Definition: type.h:22
Symbolic Execution.
semantic type conversion
Definition: std_expr.h:2111
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
const irep_idt & id() const
Definition: irep.h:189
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
const typet & follow(const typet &) const
Definition: namespace.cpp:55
void adjust_float_expressions(exprt &expr, const namespacet &ns)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
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
#define Forall_operands(it, expr)
Definition: expr.h:23
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:31
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:22
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
static bool have_to_adjust_float_expressions(const exprt &expr, const namespacet &ns)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130