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