diff --git a/regression/goto-analyzer/constant_propagation_floating_point_div/main.c b/regression/goto-analyzer/constant_propagation_floating_point_div/main.c new file mode 100644 index 00000000000..f80f5f042d4 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_floating_point_div/main.c @@ -0,0 +1,9 @@ +#include + +#define ROUND_F(x) ((int)((x) + 0.5f)) +int eight = ROUND_F(100.0f / 12.0f); + +int main() +{ + assert(eight == 8); +} diff --git a/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc b/regression/goto-analyzer/constant_propagation_floating_point_div/test.desc new file mode 100644 index 00000000000..2fc631c1933 --- /dev/null +++ b/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 diff --git a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c new file mode 100644 index 00000000000..6b1e90e3427 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/main.c @@ -0,0 +1,27 @@ +#include +#include +#include + +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); +} diff --git a/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc b/regression/goto-analyzer/constant_propagation_nondet_rounding_mode/test.desc new file mode 100644 index 00000000000..12b4b6443a2 --- /dev/null +++ b/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 diff --git a/regression/goto-analyzer/constant_propagation_rounding_mode/main.c b/regression/goto-analyzer/constant_propagation_rounding_mode/main.c new file mode 100644 index 00000000000..ace3fe60eb5 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_rounding_mode/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-analyzer/constant_propagation_rounding_mode/test.desc b/regression/goto-analyzer/constant_propagation_rounding_mode/test.desc new file mode 100644 index 00000000000..c7c1e94639c --- /dev/null +++ b/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 diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index bbf20546b68..452e8355a93 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -16,6 +16,7 @@ Author: Peter Schrammel #include #endif +#include #include #include #include @@ -23,6 +24,9 @@ Author: Peter Schrammel #include +#include +#include + 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{ + // 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); + } } } } diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 0fc4796e8b7..e32a14bc0f2 100644 --- a/src/analyses/constant_propagator.h +++ b/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 diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index bedc9ae667d..35069fc9665 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -49,7 +50,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/clobber/Makefile b/src/clobber/Makefile index aa195f87233..4f9562e354b 100644 --- a/src/clobber/Makefile +++ b/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) \ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 04cd02412d1..296d3965782 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -56,6 +56,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #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"); diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index 9325b323c64..648aa90b9a2 100644 --- a/src/goto-diff/Makefile +++ b/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) \ diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 889fee4c0ed..e32b36ae50b 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -24,6 +24,7 @@ Author: Peter Schrammel #include +#include #include #include #include @@ -45,7 +46,6 @@ Author: Peter Schrammel #include #include -#include #include diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index c90d750b1d9..98d2cc2a47f 100644 --- a/src/goto-programs/Makefile +++ b/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 \ diff --git a/src/goto-symex/adjust_float_expressions.cpp b/src/goto-programs/adjust_float_expressions.cpp similarity index 99% rename from src/goto-symex/adjust_float_expressions.cpp rename to src/goto-programs/adjust_float_expressions.cpp index 89abaf65757..c7163c8b19b 100644 --- a/src/goto-symex/adjust_float_expressions.cpp +++ b/src/goto-programs/adjust_float_expressions.cpp @@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include "goto_model.h" static bool have_to_adjust_float_expressions( const exprt &expr, diff --git a/src/goto-symex/adjust_float_expressions.h b/src/goto-programs/adjust_float_expressions.h similarity index 79% rename from src/goto-symex/adjust_float_expressions.h rename to src/goto-programs/adjust_float_expressions.h index bd011641d54..eaa5417b75d 100644 --- a/src/goto-symex/adjust_float_expressions.h +++ b/src/goto-programs/adjust_float_expressions.h @@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com /// \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 @@ -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 diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index dc4c73f3c15..79e2084a297 100644 --- a/src/goto-symex/Makefile +++ b/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 \ diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 2be5ebd63c6..328dc639156 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -41,8 +42,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include #include #include diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h index 2127c89386a..52ece8d191f 100644 --- a/src/util/ieee_float.h +++ b/src/util/ieee_float.h @@ -14,10 +14,14 @@ Author: Daniel Kroening, kroening@kroening.com #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: