From 05a2b9219a56c898992ce620d7e5ad96b0a4aa78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Fri, 24 Nov 2023 18:43:24 +0100 Subject: [PATCH 1/6] Make clang-format break after bracket --- .clang-format | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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' From 3ec0b299795725a8ba17543142e700947211e79a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Mon, 20 Nov 2023 22:03:13 +0100 Subject: [PATCH 2/6] Suppress C++20-compat warnings The warnings (errors due to -Werror) are coming from CBMC. The issue has been introduced in gcc 13 and is now fixed on CBMC develop branch in commit 3a6cef0 which can't be cleanly applied to the version that 2LS is currently using. With no current plans to migrate to C++-20, we can ignore the warning for now. --- src/config.inc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From acc954c6a2b7985827b3994a62cc4e36e5d10ccc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Mon, 20 Nov 2023 22:06:18 +0100 Subject: [PATCH 3/6] Update CBMC for cstdint includes --- lib/cbmc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 780de4d7221cb6884f0d338352598cad83ecc4f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Mon, 20 Nov 2023 22:06:28 +0100 Subject: [PATCH 4/6] Make template_generator::operator() non-virtual The API is different across the various template generators and the method is always called directly on the given template generator type, i.e. in a non-virtual way. Therefore, there is no need to implement this method as virtual. --- src/domains/template_generator_base.h | 9 --------- src/domains/template_generator_callingcontext.h | 4 ++-- src/domains/template_generator_ranking.h | 4 ++-- src/domains/template_generator_summary.h | 4 ++-- 4 files changed, 6 insertions(+), 15 deletions(-) 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(); From cebfcb71348f5e75ac31fc6aa1b09a9e35d78c78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Mon, 20 Nov 2023 22:59:23 +0100 Subject: [PATCH 5/6] Assert that no longjmp is used --- src/2ls/2ls_parse_options.cpp | 2 +- src/2ls/2ls_parse_options.h | 2 +- src/2ls/preprocessing_util.cpp | 10 +++++++--- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index 70ca2279..d0e3898b 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -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..329a2738 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -185,7 +185,7 @@ 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_unsupported_functions(goto_modelt &goto_model); void assert_no_atexit(goto_modelt &goto_model); void fix_goto_targets(goto_modelt &goto_model); void make_assertions_false(goto_modelt &goto_model); diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp index 73917e0d..a23215f1 100644 --- a/src/2ls/preprocessing_util.cpp +++ b/src/2ls/preprocessing_util.cpp @@ -653,9 +653,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 +669,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()) { From 651828d89c0003c1289a3619b1a3808f987d13aa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Tue, 21 Nov 2023 12:01:24 +0100 Subject: [PATCH 6/6] Fail on advanced math functions --- src/2ls/2ls_parse_options.cpp | 2 +- src/2ls/2ls_parse_options.h | 2 +- src/2ls/preprocessing_util.cpp | 29 ++++++++++++++++++++++++++--- 3 files changed, 28 insertions(+), 5 deletions(-) diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index d0e3898b..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")) diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index 329a2738..bdee884a 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -186,7 +186,7 @@ class twols_parse_optionst: void memory_assert_info(goto_modelt &goto_model); void handle_freed_ptr_compare(goto_modelt &goto_model); void assert_no_unsupported_functions(goto_modelt &goto_model); - void assert_no_atexit(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 a23215f1..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(); @@ -678,9 +680,13 @@ void twols_parse_optionst::assert_no_unsupported_functions( } } -/// 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) { @@ -693,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")); } } }