diff --git a/regression/goto-instrument/constant_propagation_float_rounding_unsound/main.c b/regression/goto-instrument/constant_propagation_float_rounding_unsound/main.c new file mode 100644 index 00000000000..ace3fe60eb5 --- /dev/null +++ b/regression/goto-instrument/constant_propagation_float_rounding_unsound/main.c @@ -0,0 +1,12 @@ +#include + +int main(void) +{ + __CPROVER_rounding_mode = 0; + float rounded_up = 1.0f / 10.0f; + __CPROVER_rounding_mode = 1; + float rounded_down = 1.0f / 10.0f; + assert(rounded_up - 0.1f >= 0); + assert(rounded_down - 0.1f < 0); + return 0; +} diff --git a/regression/goto-instrument/constant_propagation_float_rounding_unsound/test.desc b/regression/goto-instrument/constant_propagation_float_rounding_unsound/test.desc new file mode 100644 index 00000000000..b85fba3f005 --- /dev/null +++ b/regression/goto-instrument/constant_propagation_float_rounding_unsound/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--constant-propagator --inline --add-library +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index c57466bea2c..c8a087d49fe 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -19,6 +19,7 @@ Author: Peter Schrammel #endif #include +#include #include #include #include @@ -166,6 +167,17 @@ void constant_propagator_domaint::transform( { const exprt &lhs = from->assign_lhs(); const exprt &rhs = from->assign_rhs(); + + // If we're assigning to the rounding mode, invalidate all + // floating-point constants as they may have been computed + // with a different rounding mode + if( + lhs.id() == ID_symbol && + to_symbol_expr(lhs).get_identifier() == rounding_mode_identifier()) + { + values.invalidate_floatbv_constants(ns); + } + assign_rec(values, lhs, rhs, ns, cp, true); } else if(from->is_assume()) @@ -495,6 +507,28 @@ void constant_propagator_domaint::valuest::set_dirty_to_top( } } +void constant_propagator_domaint::valuest::invalidate_floatbv_constants( + const namespacet &ns) +{ + typedef replace_symbolt::expr_mapt expr_mapt; + expr_mapt &expr_map = replace_const.get_expr_map(); + + for(expr_mapt::iterator it = expr_map.begin(); it != expr_map.end();) + { + const irep_idt id = it->first; + const symbolt &symbol = ns.lookup(id); + + // Remove any variable with floating-point type, as its value + // may have been computed with a different rounding mode + if(symbol.type.id() == ID_floatbv) + { + it = replace_const.erase(it); + } + else + it++; + } +} + void constant_propagator_domaint::valuest::output( std::ostream &out, const namespacet &ns) const diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index fd249904404..866fba29530 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -118,6 +118,8 @@ class constant_propagator_domaint:public ai_domain_baset void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns); + void invalidate_floatbv_constants(const namespacet &ns); + bool is_constant(const exprt &expr, const namespacet &ns) const; bool is_constant(const irep_idt &id, const namespacet &ns) const; diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp index b6961b99a0f..e86ae893ff1 100644 --- a/unit/analyses/constant_propagator.cpp +++ b/unit/analyses/constant_propagator.cpp @@ -7,9 +7,11 @@ Author: Diffblue Ltd \*******************************************************************/ #include +#include #include #include #include +#include #include #include @@ -331,3 +333,95 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") } } } + +SCENARIO( + "constant_propagator_rounding_mode", + "[core][analyses][constant_propagator]") +{ + GIVEN( + "A GOTO program with floating-point operations and rounding mode changes") + { + goto_modelt goto_model; + namespacet ns(goto_model.symbol_table); + + // Create the program: + // __CPROVER_rounding_mode = 0; + // float f1 = 1.0f / 10.0f; + // __CPROVER_rounding_mode = 1; + // float f2 = 1.0f / 10.0f; + + symbolt rounding_mode{"__CPROVER_rounding_mode", integer_typet(), ID_C}; + symbolt local_f1{"f1", float_type(), ID_C}; + symbolt local_f2{"f2", float_type(), ID_C}; + + code_blockt code( + {code_declt(local_f1.symbol_expr()), + code_declt(local_f2.symbol_expr()), + code_assignt( + rounding_mode.symbol_expr(), constant_exprt("0", integer_typet())), + code_assignt( + local_f1.symbol_expr(), + div_exprt( + constant_exprt("1", float_type()), + constant_exprt("10", float_type()))), + code_assignt( + rounding_mode.symbol_expr(), constant_exprt("1", integer_typet())), + code_assignt( + local_f2.symbol_expr(), + div_exprt( + constant_exprt("1", float_type()), + constant_exprt("10", float_type())))}); + + symbolt main_function_symbol{"main", code_typet({}, empty_typet()), ID_C}; + main_function_symbol.value = code; + + goto_model.symbol_table.add(rounding_mode); + goto_model.symbol_table.add(local_f1); + goto_model.symbol_table.add(local_f2); + goto_model.symbol_table.add(main_function_symbol); + + goto_convert(goto_model, null_message_handler); + + const goto_functiont &main_function = goto_model.get_goto_function("main"); + + // Find the instruction after the second rounding mode assignment + goto_programt::const_targett test_instruction = + main_function.body.instructions.begin(); + int rounding_mode_assignments = 0; + while(test_instruction != main_function.body.instructions.end()) + { + if( + test_instruction->is_assign() && + test_instruction->assign_lhs() == rounding_mode.symbol_expr()) + { + ++rounding_mode_assignments; + if(rounding_mode_assignments == 2) + { + ++test_instruction; + break; + } + } + ++test_instruction; + } + + REQUIRE(test_instruction != main_function.body.instructions.end()); + + WHEN("We apply constant propagation") + { + constant_propagator_ait constant_propagator(main_function); + constant_propagator(main_function_symbol.name, main_function, ns); + + THEN( + "The propagator should NOT have f1 as a constant, because " + "the rounding mode changed") + { + const auto &final_domain = constant_propagator[test_instruction]; + + // f1 should not be constant at this point because the rounding + // mode changed after it was computed + REQUIRE_FALSE( + final_domain.values.is_constant(local_f1.symbol_expr(), ns)); + } + } + } +}