Merge pull request #2081 from hannes-steffenhagen-diffblue/floating_p…

…oint_simplificiation

Floating point simplification for goto-analyzer constants domain

regression/goto-analyzer/constant_propagation_floating_point_div/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+#define ROUND_F(x) ((int)((x) + 0.5f))
+int eight = ROUND_F(100.0f / 12.0f);
+
+int main()
+{
+  assert(eight == 8);
+}

regression/goto-analyzer/constant_propagation_floating_point_div/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--constants --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file main.c line 8 function main, assertion eight == 8: Success$
+--
+^warning: ignoring

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

regression/goto-analyzer/constant_propagation_rounding_mode/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-analyzer/constant_propagation_rounding_mode/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--constants --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] file main.c line 9 function main, assertion rounded_up - 0.1f >= 0: Success
+^\[main.assertion.2\] file main.c line 10 function main, assertion rounded_down - 0.1f < 0: Success
+--
+^warning: ignoring

src/analyses/constant_propagator.cpp

@@ -16,13 +16,17 @@ 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 <algorithm>
+#include <array>
+
 void constant_propagator_domaint::assign_rec(
   valuest &values,
   const exprt &lhs,
@@ -35,8 +39,7 @@ void constant_propagator_domaint::assign_rec(
   const symbol_exprt &s=to_symbol_expr(lhs);
 
   exprt tmp=rhs;
-  values.replace_const(tmp);
-  simplify(tmp, ns);
+  partial_evaluate(tmp, ns);
 
   if(tmp.is_constant())
     values.set_to(s, tmp);
@@ -99,10 +102,10 @@ void constant_propagator_domaint::transform(
     // Comparing iterators is safe as the target must be within the same list
     // of instructions because this is a GOTO.
     if(from->get_target()==to)
-      g=simplify_expr(from->guard, ns);
+      g = from->guard;
     else
-      g=simplify_expr(not_exprt(from->guard), ns);
-
+      g = not_exprt(from->guard);
+    partial_evaluate(g, ns);
     if(g.is_false())
      values.set_to_bottom();
     else
@@ -269,10 +272,7 @@ bool constant_propagator_domaint::ai_simplify(
   exprt &condition,
   const namespacet &ns) const
 {
-  bool b=values.replace_const.replace(condition);
-  b&=simplify(condition, ns);
-
-  return b;
+  return partial_evaluate(condition, ns);
 }
 
 
@@ -504,6 +504,74 @@ bool constant_propagator_domaint::merge(
   return values.merge(other.values);
 }
 
+/// Attempt to evaluate expression using domain knowledge
+/// This function changes the expression that is passed into it.
+/// \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::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
+{
+  bool did_not_change_anything = values.replace_const.replace(expr);
+  did_not_change_anything &= simplify(expr, ns);
+  return did_not_change_anything;
+}
+
 void constant_propagator_ait::replace(
   goto_functionst &goto_functions,
   const namespacet &ns)
@@ -529,38 +597,34 @@ void constant_propagator_ait::replace(
 
     if(it->is_goto() || it->is_assume() || it->is_assert())
     {
-      s_it->second.values.replace_const(it->guard);
-      simplify(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.values.replace_const(rhs);
-      simplify(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())
     {
-      s_it->second.values.replace_const(
-        to_code_function_call(it->code).function());
-
-      simplify(to_code_function_call(it->code).function(), ns);
+      exprt &function = to_code_function_call(it->code).function();
+      s_it->second.partial_evaluate(function, ns);
 
       exprt::operandst &args=
         to_code_function_call(it->code).arguments();
 
-      for(exprt::operandst::iterator o_it=args.begin();
-          o_it!=args.end(); ++o_it)
+      for(auto &arg : args)
       {
-        s_it->second.values.replace_const(*o_it);
-        simplify(*o_it, ns);
+        s_it->second.partial_evaluate(arg, ns);
       }
     }
     else if(it->is_other())
     {
       if(it->code.get_statement()==ID_expression)
-        s_it->second.values.replace_const(it->code);
+      {
+        s_it->second.partial_evaluate(it->code, ns);
+      }
     }
   }
 }

src/analyses/constant_propagator.h

@@ -138,6 +138,8 @@ class constant_propagator_domaint:public ai_domain_baset
 
   valuest values;
 
+  bool partial_evaluate(exprt &expr, const namespacet &ns) const;
+
 protected:
   void assign_rec(
     valuest &values,
@@ -147,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

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/c_preprocess.h>
 
+#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>
@@ -49,7 +50,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/string_instrumentation.h>
 
 #include <goto-symex/rewrite_union.h>
-#include <goto-symex/adjust_float_expressions.h>
 
 #include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/full_slicer.h>

src/clobber/Makefile

@@ -13,7 +13,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../assembler/assembler$(LIBEXT) \
        ../solvers/solvers$(LIBEXT) \
        ../util/util$(LIBEXT) \
-       ../goto-symex/adjust_float_expressions$(OBJEXT) \
        ../goto-symex/rewrite_union$(OBJEXT) \
        ../pointer-analysis/dereference$(OBJEXT) \
        ../goto-instrument/dump_c$(OBJEXT) \

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/goto-diff/Makefile

@@ -25,7 +25,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
       ../goto-instrument/cover_instrument_other$(OBJEXT) \
       ../goto-instrument/cover_util$(OBJEXT) \
-      ../goto-symex/adjust_float_expressions$(OBJEXT) \
       ../goto-symex/rewrite_union$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \

src/goto-diff/goto_diff_parse_options.cpp

@@ -24,6 +24,7 @@ Author: Peter Schrammel
 
 #include <langapi/language.h>
 
+#include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/mm_io.h>
@@ -45,7 +46,6 @@ Author: Peter Schrammel
 #include <goto-programs/link_to_library.h>
 
 #include <goto-symex/rewrite_union.h>
-#include <goto-symex/adjust_float_expressions.h>
 
 #include <goto-instrument/cover.h>
 

src/goto-programs/Makefile

@@ -1,4 +1,5 @@
-SRC = basic_blocks.cpp \
+SRC = adjust_float_expressions.cpp \
+      basic_blocks.cpp \
       builtin_functions.cpp \
       class_hierarchy.cpp \
       class_identifier.cpp \

src/goto-symex/adjust_float_expressions.cpp → src/goto-programs/adjust_float_expressions.cpp

@@ -18,7 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/ieee_float.h>
 #include <util/arith_tools.h>
 
-#include <goto-programs/goto_model.h>
+#include "goto_model.h"
 
 static bool have_to_adjust_float_expressions(
   const exprt &expr,

src/goto-symex/adjust_float_expressions.h → src/goto-programs/adjust_float_expressions.h

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Symbolic Execution
 
-#ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
-#define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
+#ifndef CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
+#define CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H
 
 #include <goto-programs/goto_functions.h>
 
@@ -31,4 +31,4 @@ void adjust_float_expressions(
   const namespacet &ns);
 void adjust_float_expressions(goto_modelt &goto_model);
 
-#endif // CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
+#endif // CPROVER_GOTO_PROGRAMS_ADJUST_FLOAT_EXPRESSIONS_H

src/goto-symex/Makefile

@@ -1,5 +1,4 @@
-SRC = adjust_float_expressions.cpp \
-      auto_objects.cpp \
+SRC = auto_objects.cpp \
       build_goto_trace.cpp \
       goto_symex.cpp \
       goto_symex_state.cpp \