From f9c5faf7ceb63062dcacf81d0f77a6a232ae57b1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 17 Jul 2018 17:01:05 +0100 Subject: [PATCH 1/2] adjust_float_expressions can now take a rounding mode argument --- .../adjust_float_expressions.cpp | 58 ++++++++++--------- src/goto-programs/adjust_float_expressions.h | 2 + 2 files changed, 32 insertions(+), 28 deletions(-) diff --git a/src/goto-programs/adjust_float_expressions.cpp b/src/goto-programs/adjust_float_expressions.cpp index c7163c8b19b..1b2c6cc5ca3 100644 --- a/src/goto-programs/adjust_float_expressions.cpp +++ b/src/goto-programs/adjust_float_expressions.cpp @@ -20,9 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_model.h" -static bool have_to_adjust_float_expressions( - const exprt &expr, - const namespacet &ns) +static bool have_to_adjust_float_expressions(const exprt &expr) { if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus || @@ -33,11 +31,11 @@ static bool have_to_adjust_float_expressions( expr.id()==ID_floatbv_typecast) return false; - const typet &type=ns.follow(expr.type()); + const typet &type = expr.type(); - if(type.id()==ID_floatbv || - (type.id()==ID_complex && - ns.follow(type.subtype()).id()==ID_floatbv)) + if( + type.id() == ID_floatbv || + (type.id() == ID_complex && type.subtype().id() == ID_floatbv)) { if(expr.id()==ID_plus || expr.id()==ID_minus || expr.id()==ID_mult || expr.id()==ID_div || @@ -69,7 +67,7 @@ static bool have_to_adjust_float_expressions( } forall_operands(it, expr) - if(have_to_adjust_float_expressions(*it, ns)) + if(have_to_adjust_float_expressions(*it)) return true; return false; @@ -77,27 +75,21 @@ static bool have_to_adjust_float_expressions( /// This adds the rounding mode to floating-point operations, including those in /// vectors and complex numbers. -void adjust_float_expressions( - exprt &expr, - const namespacet &ns) +void adjust_float_expressions(exprt &expr, const exprt &rounding_mode) { - if(!have_to_adjust_float_expressions(expr, ns)) + if(!have_to_adjust_float_expressions(expr)) return; - Forall_operands(it, expr) - adjust_float_expressions(*it, ns); + // recursive call + for(auto &op : expr.operands()) + adjust_float_expressions(op, rounding_mode); - const typet &type=ns.follow(expr.type()); + const typet &type = expr.type(); - if(type.id()==ID_floatbv || - (type.id()==ID_complex && - ns.follow(type.subtype()).id()==ID_floatbv)) + if( + type.id() == ID_floatbv || + (type.id() == ID_complex && type.subtype().id() == ID_floatbv)) { - symbol_exprt rounding_mode= - ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr(); - - rounding_mode.add_source_location()=expr.source_location(); - if(expr.id()==ID_plus || expr.id()==ID_minus || expr.id()==ID_mult || expr.id()==ID_div || expr.id()==ID_rem) @@ -128,11 +120,6 @@ void adjust_float_expressions( const typet &src_type=typecast_expr.op().type(); const typet &dest_type=typecast_expr.type(); - symbol_exprt rounding_mode= - ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr(); - - rounding_mode.add_source_location()=expr.source_location(); - if(dest_type.id()==ID_floatbv && src_type.id()==ID_floatbv) { @@ -179,6 +166,21 @@ void adjust_float_expressions( } } +/// This adds the rounding mode to floating-point operations, including those in +/// vectors and complex numbers. +void adjust_float_expressions(exprt &expr, const namespacet &ns) +{ + if(!have_to_adjust_float_expressions(expr)) + return; + + symbol_exprt rounding_mode = + ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr(); + + rounding_mode.add_source_location() = expr.source_location(); + + adjust_float_expressions(expr, rounding_mode); +} + void adjust_float_expressions( goto_functionst::goto_functiont &goto_function, const namespacet &ns) diff --git a/src/goto-programs/adjust_float_expressions.h b/src/goto-programs/adjust_float_expressions.h index eaa5417b75d..393bd5b056f 100644 --- a/src/goto-programs/adjust_float_expressions.h +++ b/src/goto-programs/adjust_float_expressions.h @@ -22,6 +22,8 @@ void adjust_float_expressions( exprt &expr, const namespacet &ns); +void adjust_float_expressions(exprt &expr, const exprt &rounding_mode); + void adjust_float_expressions( goto_functionst::goto_functiont &goto_function, const namespacet &ns); From 8edc5ee762328b9a1f5397efc169512498e5d6e5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 17 Jul 2018 17:07:41 +0100 Subject: [PATCH 2/2] C front-end: constant folding for floating-point --- regression/cbmc/switch7/main.c | 23 +++++++++++++++++++++++ regression/cbmc/switch7/test.desc | 8 ++++++++ src/ansi-c/c_typecheck_expr.cpp | 9 +++++++++ 3 files changed, 40 insertions(+) create mode 100644 regression/cbmc/switch7/main.c create mode 100644 regression/cbmc/switch7/test.desc diff --git a/regression/cbmc/switch7/main.c b/regression/cbmc/switch7/main.c new file mode 100644 index 00000000000..27093537787 --- /dev/null +++ b/regression/cbmc/switch7/main.c @@ -0,0 +1,23 @@ +// These need to be constant-folded at compile time + +#define C1 (int)(0. / 1. + 0.5) +#define C2 (int)(1. / 1. + 0.5) + +int nondet_int(); + +int main(void) +{ + int i = nondet_int(); + + switch(i) + { + case C1: + break; + + case C2: + break; + + default: + break; + } +} diff --git a/regression/cbmc/switch7/test.desc b/regression/cbmc/switch7/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/switch7/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index c33bcfbefa8..b21c7792a82 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -24,6 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "builtin_factory.h" #include "c_typecast.h" #include "c_qualifiers.h" @@ -3372,6 +3374,13 @@ void c_typecheck_baset::typecheck_side_effect_assignment( void c_typecheck_baset::make_constant(exprt &expr) { + // Floating-point expressions may require a rounding mode. + // ISO 9899:1999 F.7.2 says that the default is "round to nearest". + // Some compilers have command-line options to override. + const auto rounding_mode = + from_integer(ieee_floatt::ROUND_TO_EVEN, signed_int_type()); + adjust_float_expressions(expr, rounding_mode); + simplify(expr, *this); if(!expr.is_constant() &&