diff --git a/.clang-format b/.clang-format index ae801bc8..fdd2d857 100644 --- a/.clang-format +++ b/.clang-format @@ -1,6 +1,6 @@ --- AccessModifierOffset: '-2' -AlignAfterOpenBracket: Align +AlignAfterOpenBracket: AlwaysBreak AlignConsecutiveAssignments: 'false' AlignConsecutiveDeclarations: 'false' AlignEscapedNewlinesLeft: 'false' diff --git a/lib/cbmc b/lib/cbmc index 96f499a2..7c65269c 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit 96f499a2ac53064fb7695eaa1a937e827148f69a +Subproject commit 7c65269cfbdf9cb8d9ee9ad2a4cd1b145a4aa1da diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index 70ca2279..1016deab 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -1023,7 +1023,7 @@ bool twols_parse_optionst::process_goto_program( remove_returns(goto_model); if(options.get_bool_option("competition-mode")) - assert_no_atexit(goto_model); + assert_no_unsupported_function_calls(goto_model); // now do full inlining, if requested if(options.get_bool_option("inline")) @@ -1045,7 +1045,7 @@ bool twols_parse_optionst::process_goto_program( } if(options.get_bool_option("competition-mode")) - assert_no_builtin_functions(goto_model); + assert_no_unsupported_functions(goto_model); make_scanf_nondet(goto_model); diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index 5eb2319e..bdee884a 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -185,8 +185,8 @@ class twols_parse_optionst: void remove_dead_goto(goto_modelt &goto_model); void memory_assert_info(goto_modelt &goto_model); void handle_freed_ptr_compare(goto_modelt &goto_model); - void assert_no_builtin_functions(goto_modelt &goto_model); - void assert_no_atexit(goto_modelt &goto_model); + void assert_no_unsupported_functions(goto_modelt &goto_model); + void assert_no_unsupported_function_calls(goto_modelt &goto_model); void fix_goto_targets(goto_modelt &goto_model); void make_assertions_false(goto_modelt &goto_model); void make_symbolic_array_indices(goto_modelt &goto_model); diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp index 73917e0d..a692ea3b 100644 --- a/src/2ls/preprocessing_util.cpp +++ b/src/2ls/preprocessing_util.cpp @@ -22,6 +22,8 @@ Author: Peter Schrammel #include "2ls_parse_options.h" +#define NOT_MATH_FUN(call, fun) call != fun &&call != fun "f" && call != fun "l" + void twols_parse_optionst::inline_main(goto_modelt &goto_model) { irep_idt start=goto_functionst::entry_point(); @@ -653,9 +655,12 @@ void twols_parse_optionst::handle_freed_ptr_compare(goto_modelt &goto_model) } } -/// Add assertions preventing analysis of programs using GCC builtin functions -/// that are not supported and can cause false results. -void twols_parse_optionst::assert_no_builtin_functions(goto_modelt &goto_model) +/// Fail if the program contains any functions that 2LS does not currently +/// support. These include: +/// - builtin gcc functions +/// - longjmp (not supported by CBMC) +void twols_parse_optionst::assert_no_unsupported_functions( + goto_modelt &goto_model) { forall_goto_program_instructions( i_it, @@ -666,6 +671,7 @@ void twols_parse_optionst::assert_no_builtin_functions(goto_modelt &goto_model) assert( name.find("__builtin_")==std::string::npos && name.find("__CPROVER_overflow")==std::string::npos); + assert(name != "longjmp" && name != "_longjmp" && name != "siglongjmp"); if(i_it->is_assign()) { @@ -674,9 +680,13 @@ void twols_parse_optionst::assert_no_builtin_functions(goto_modelt &goto_model) } } -/// Prevents usage of atexit function which is not supported, yet -/// Must be called before inlining since it will lose the calls -void twols_parse_optionst::assert_no_atexit(goto_modelt &goto_model) +/// Fail if the program contains a call to an unsupported function. These +/// include the atexit function and advanced math functions from math.h ( +/// these are either not defined in CBMC at all, or defined very imprecisely, +/// e.g. the result of cos is in <-1, 1> without any further information). +/// Must be called before inlining since it will lose the calls. +void twols_parse_optionst::assert_no_unsupported_function_calls( + goto_modelt &goto_model) { for(const auto &f_it : goto_model.goto_functions.function_map) { @@ -689,6 +699,23 @@ void twols_parse_optionst::assert_no_atexit(goto_modelt &goto_model) continue; auto &name=id2string(to_symbol_expr(function).get_identifier()); assert(name!="atexit"); + assert( + // Trigonometry + NOT_MATH_FUN(name, "cos") && NOT_MATH_FUN(name, "acos") && + NOT_MATH_FUN(name, "sin") && NOT_MATH_FUN(name, "asin") && + NOT_MATH_FUN(name, "tan") && NOT_MATH_FUN(name, "atan") && + NOT_MATH_FUN(name, "atan2") && + // Hyperbolic + NOT_MATH_FUN(name, "cosh") && NOT_MATH_FUN(name, "acosh") && + NOT_MATH_FUN(name, "sinh") && NOT_MATH_FUN(name, "asinh") && + NOT_MATH_FUN(name, "tanh") && NOT_MATH_FUN(name, "atanh") && + // Exponential + NOT_MATH_FUN(name, "exp") && NOT_MATH_FUN(name, "exp2") && + NOT_MATH_FUN(name, "expm1") && NOT_MATH_FUN(name, "log") && + NOT_MATH_FUN(name, "log10") && NOT_MATH_FUN(name, "log2") && + NOT_MATH_FUN(name, "log1p") && + // Other + NOT_MATH_FUN(name, "erf")); } } } diff --git a/src/config.inc b/src/config.inc index 1505da16..acb8c7c4 100644 --- a/src/config.inc +++ b/src/config.inc @@ -3,7 +3,7 @@ CPROVER_DIR = ../../lib/cbmc # Variables you may want to override # Enable warnings -CXXFLAGS += -Wall -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic +CXXFLAGS += -Wall -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-c++20-compat -Wno-strict-aliasing -pedantic # Select optimisation or debug #CXXFLAGS += -O2 diff --git a/src/domains/template_generator_base.h b/src/domains/template_generator_base.h index 76be7f51..cb68f7ed 100644 --- a/src/domains/template_generator_base.h +++ b/src/domains/template_generator_base.h @@ -46,15 +46,6 @@ class template_generator_baset:public messaget { } - virtual void operator()( - unsigned _domain_number, - const local_SSAt &SSA, - bool forward=true) - { - domain_number=_domain_number; - assert(false); - } - virtual var_sett all_vars(); inline domaint *domain() diff --git a/src/domains/template_generator_callingcontext.h b/src/domains/template_generator_callingcontext.h index 730d2b07..6aec151c 100644 --- a/src/domains/template_generator_callingcontext.h +++ b/src/domains/template_generator_callingcontext.h @@ -27,12 +27,12 @@ class template_generator_callingcontextt:public template_generator_baset { } - virtual void operator()( + void operator()( unsigned _domain_number, const local_SSAt &SSA, local_SSAt::nodest::const_iterator n_it, local_SSAt::nodet::function_callst::const_iterator f_it, - bool forward=true); + bool forward = true); virtual var_sett callingcontext_vars(); diff --git a/src/domains/template_generator_ranking.h b/src/domains/template_generator_ranking.h index d83e642a..df64b0fb 100644 --- a/src/domains/template_generator_ranking.h +++ b/src/domains/template_generator_ranking.h @@ -28,10 +28,10 @@ class template_generator_rankingt:public template_generator_baset { } - virtual void operator()( + void operator()( unsigned _domain_number, const local_SSAt &SSA, - bool forward=true); + bool forward = true); protected: void collect_variables_ranking( diff --git a/src/domains/template_generator_summary.h b/src/domains/template_generator_summary.h index 6d1d04c2..5bbbf9a1 100644 --- a/src/domains/template_generator_summary.h +++ b/src/domains/template_generator_summary.h @@ -28,10 +28,10 @@ class template_generator_summaryt:public template_generator_baset { } - virtual void operator()( + void operator()( unsigned _domain_number, const local_SSAt &SSA, - bool forward=true); + bool forward = true); virtual var_sett inout_vars(); virtual var_sett loop_vars();