Try all rounding modes when domain is unknown

For rounding modes in constant propagator domain

Author: hannes-steffenhagen-diffblue

regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c

@@ -0,0 +1,27 @@
+#include <fenv.h>
+#include <stdio.h>
+#include <assert.h>
+
+int nondet_rounding_mode(void);
+
+int main(void)
+{
+  // slightly bigger than 0.1
+  float f = 1.0f / 10.0f;
+
+  // now we don't know what rounding mode we're in
+  __CPROVER_rounding_mode = nondet_rounding_mode();
+  // depending on rounding mode 1.0f/10.0f could
+  // be greater or smaller than 0.1
+
+  // definitely not smaller than -0.1
+  assert((1.0f / 10.0f) - f < -0.1f);
+  // might be smaller than 0
+  assert((1.0f / 10.0f) - f < 0.0f);
+  // definitely smaller or equal to 0
+  assert((1.0f / 10.0f) - f <= 0.0f);
+  // might be greater or equal to 0
+  assert((1.0f / 10.0f) - f >= 0.0f);
+  // definitely not greater than 0
+  assert((1.0f / 10.0f) - f > 0.0f);
+}

regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] file main.c line 18 function main, assertion \(1.0f / 10.0f\) - f < -0.1f: Failure \(if reachable\)
+\[main.assertion.2\] file main.c line 20 function main, assertion \(1.0f / 10.0f\) - f < 0.0f: Unknown
+\[main.assertion.3\] file main.c line 22 function main, assertion \(1.0f / 10.0f\) - f <= 0.0f: Success
+\[main.assertion.4\] file main.c line 24 function main, assertion \(1.0f / 10.0f\) - f >= 0.0f: Unknown
+\[main.assertion.5\] file main.c line 26 function main, assertion \(1.0f / 10.0f\) - f > 0.0f: Failure \(if reachable\)
+
+--
+^warning: ignoring

src/analyses/constant_propagator.cpp

@@ -23,6 +23,10 @@ Author: Peter Schrammel
 
 #include <langapi/language_util.h>
 #include <goto-programs/adjust_float_expressions.h>
+#include <util/ieee_float.h>
+
+#include <algorithm>
+#include <array>
 
 void constant_propagator_domaint::assign_rec(
   valuest &values,
@@ -510,7 +514,46 @@ bool constant_propagator_domaint::try_evaluate(
   exprt &expr,
   const namespacet &ns) const
 {
+  const irep_idt ID_rounding_mode = CPROVER_PREFIX "rounding_mode";
   adjust_float_expressions(expr, ns);
+
+  // if the current rounding mode is top we can
+  // still get a non-top result by trying all rounding
+  // modes and checking if the results are all the same
+  if(!values.is_constant(symbol_exprt(ID_rounding_mode)))
+  {
+    // NOLINTNEXTLINE (whitespace/braces)
+    auto rounding_modes = std::array<ieee_floatt::rounding_modet, 4>{
+      // NOLINTNEXTLINE (whitespace/braces)
+      {ieee_floatt::ROUND_TO_EVEN,
+       ieee_floatt::ROUND_TO_ZERO,
+       ieee_floatt::ROUND_TO_MINUS_INF,
+       // NOLINTNEXTLINE (whitespace/braces)
+       ieee_floatt::ROUND_TO_PLUS_INF}};
+    // instead of 4, we could write rounding_modes.size() here
+    // if we dropped Visual Studio 2013 support (no constexpr)
+    std::array<exprt, 4> possible_results;
+    for(std::size_t i = 0; i < possible_results.size(); ++i)
+    {
+      constant_propagator_domaint child(*this);
+      child.values.set_to(
+        ID_rounding_mode, from_integer(rounding_modes[i], integer_typet()));
+      possible_results[i] = expr;
+      if(child.try_evaluate(possible_results[i], ns))
+      {
+        return true;
+      }
+    }
+    for(auto const &possible_result : possible_results)
+    {
+      if(possible_result != possible_results.front())
+      {
+        return true;
+      }
+    }
+    expr = possible_results.front();
+    return false;
+  }
   bool did_not_change_anything = values.replace_const.replace(expr);
   did_not_change_anything &= simplify(expr, ns);
   return did_not_change_anything;