Float constant propagation must observe rounding modes

regression/goto-instrument/constant_propagation_float_rounding_unsound/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+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;
+}

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

src/analyses/constant_propagator.cpp

@@ -19,6 +19,7 @@ Author: Peter Schrammel
 #endif
 
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
@@ -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

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;

unit/analyses/constant_propagator.cpp

@@ -7,9 +7,11 @@ Author: Diffblue Ltd
 \*******************************************************************/
 
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
 #include <util/c_types.h>
 #include <util/mathematical_types.h>
 #include <util/prefix.h>
+#include <util/std_expr.h>
 
 #include <analyses/constant_propagator.h>
 #include <ansi-c/goto-conversion/goto_convert_functions.h>
@@ -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));
+      }
+    }
+  }
+}