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 <assert.h>
+#include <fenv.h>
+#include <stdio.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

@@ -16,13 +16,16 @@ Author: Peter Schrammel
 #include <util/format_expr.h>
 #endif
 
+#include <util/ieee_float.h>
 #include <util/find_symbols.h>
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
 #include <util/cprover_prefix.h>
 
 #include <langapi/language_util.h>
-#include <goto-programs/adjust_float_expressions.h>
+
+#include <algorithm>
+#include <array>
 
 void constant_propagator_domaint::assign_rec(
   valuest &values,
@@ -36,7 +39,7 @@ void constant_propagator_domaint::assign_rec(
   const symbol_exprt &s=to_symbol_expr(lhs);
 
   exprt tmp=rhs;
-  try_evaluate(tmp, ns);
+  partial_evaluate(tmp, ns);
 
   if(tmp.is_constant())
     values.set_to(s, tmp);
@@ -102,7 +105,7 @@ void constant_propagator_domaint::transform(
       g = from->guard;
     else
       g = not_exprt(from->guard);
-    try_evaluate(g, ns);
+    partial_evaluate(g, ns);
     if(g.is_false())
      values.set_to_bottom();
     else
@@ -269,7 +272,7 @@ bool constant_propagator_domaint::ai_simplify(
   exprt &condition,
   const namespacet &ns) const
 {
-  return try_evaluate(condition, ns);
+  return partial_evaluate(condition, ns);
 }
 
 
@@ -506,11 +509,64 @@ bool constant_propagator_domaint::merge(
 /// \param expr The expression to evaluate
 /// \param ns The namespace for symbols in the expression
 /// \return True if the expression is unchanged, false otherwise
-bool constant_propagator_domaint::try_evaluate(
+bool constant_propagator_domaint::partial_evaluate(
+  exprt &expr,
+  const namespacet &ns) const
+{
+  // 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_cprover_rounding_mode_str)))
+  {
+    return partial_evaluate_with_all_rounding_modes(expr, ns);
+  }
+  return replace_constants_and_simplify(expr, ns);
+}
+
+/// Attempt to evaluate an expression in all rounding modes.
+///
+/// If the result is the same for all rounding modes, change
+/// expr to that result and return false. Otherwise, return true.
+bool constant_propagator_domaint::partial_evaluate_with_all_rounding_modes(
+  exprt &expr,
+  const namespacet &ns) const
+{ // 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}};
+  exprt first_result;
+  for(std::size_t i = 0; i < rounding_modes.size(); ++i)
+  {
+    constant_propagator_domaint child(*this);
+    child.values.set_to(
+      ID_cprover_rounding_mode_str,
+      from_integer(rounding_modes[i], integer_typet()));
+    exprt result = expr;
+    if(child.replace_constants_and_simplify(result, ns))
+    {
+      return true;
+    }
+    else if(i == 0)
+    {
+      first_result = result;
+    }
+    else if(result != first_result)
+    {
+      return true;
+    }
+  }
+  expr = first_result;
+  return false;
+}
+
+bool constant_propagator_domaint::replace_constants_and_simplify(
   exprt &expr,
   const namespacet &ns) const
 {
-  adjust_float_expressions(expr, ns);
   bool did_not_change_anything = values.replace_const.replace(expr);
   did_not_change_anything &= simplify(expr, ns);
   return did_not_change_anything;
@@ -541,33 +597,33 @@ void constant_propagator_ait::replace(
 
     if(it->is_goto() || it->is_assume() || it->is_assert())
     {
-      s_it->second.try_evaluate(it->guard, ns);
+      s_it->second.partial_evaluate(it->guard, ns);
     }
     else if(it->is_assign())
     {
       exprt &rhs=to_code_assign(it->code).rhs();
-      s_it->second.try_evaluate(rhs, ns);
+      s_it->second.partial_evaluate(rhs, ns);
       if(rhs.id()==ID_constant)
         rhs.add_source_location()=it->code.op0().source_location();
     }
     else if(it->is_function_call())
     {
       exprt &function = to_code_function_call(it->code).function();
-      s_it->second.try_evaluate(function, ns);
+      s_it->second.partial_evaluate(function, ns);
 
       exprt::operandst &args=
         to_code_function_call(it->code).arguments();
 
       for(auto &arg : args)
       {
-        s_it->second.try_evaluate(arg, ns);
+        s_it->second.partial_evaluate(arg, ns);
       }
     }
     else if(it->is_other())
     {
       if(it->code.get_statement()==ID_expression)
       {
-        s_it->second.try_evaluate(it->code, ns);
+        s_it->second.partial_evaluate(it->code, ns);
       }
     }
   }

src/analyses/constant_propagator.h

@@ -138,7 +138,7 @@ class constant_propagator_domaint:public ai_domain_baset
 
   valuest values;
 
-  bool try_evaluate(exprt &expr, const namespacet &ns) const;
+  bool partial_evaluate(exprt &expr, const namespacet &ns) const;
 
 protected:
   void assign_rec(
@@ -149,6 +149,12 @@ class constant_propagator_domaint:public ai_domain_baset
   bool two_way_propagate_rec(
     const exprt &expr,
     const namespacet &ns);
+
+  bool partial_evaluate_with_all_rounding_modes(
+    exprt &expr,
+    const namespacet &ns) const;
+
+  bool replace_constants_and_simplify(exprt &expr, const namespacet &ns) const;
 };
 
 class constant_propagator_ait:public ait<constant_propagator_domaint>

src/cbmc/cbmc_parse_options.cpp

@@ -27,7 +27,6 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/c_preprocess.h>
 
 #include <goto-programs/adjust_float_expressions.h>
-#include <goto-programs/convert_nondet.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -56,6 +56,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/exit_codes.h>
 
 #include <cbmc/version.h>
+#include <goto-programs/adjust_float_expressions.h>
 
 #include "taint_analysis.h"
 #include "unreachable_instructions.h"
@@ -477,6 +478,7 @@ int goto_analyzer_parse_optionst::doit()
 /// Depending on the command line mode, run one of the analysis tasks
 int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 {
+  adjust_float_expressions(goto_model);
   if(options.get_bool_option("taint"))
   {
     std::string taint_file=cmdline.get_value("taint");

src/jbmc/jbmc_parse_options.cpp

@@ -27,7 +27,6 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/ansi_c_language.h>
 
 #include <goto-programs/adjust_float_expressions.h>
-#include <goto-programs/convert_nondet.h>
 #include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>

src/util/ieee_float.h

@@ -14,10 +14,14 @@ Author: Daniel Kroening, [email protected]
 
 #include "mp_arith.h"
 #include "format_spec.h"
+#include "irep.h"
+#include "cprover_prefix.h"
 
 class constant_exprt;
 class floatbv_typet;
 
+const char ID_cprover_rounding_mode_str[] = CPROVER_PREFIX "rounding_mode";
+
 class ieee_float_spect
 {
 public: