Merge pull request #176 from FrNecas/fnecas-svcomp-24

SV-COMP 24 fixes
diffblue · Oct 12, 2024 · 9a9ad37 · 9a9ad37
2 parents c572aa1 + 651828d
commit 9a9ad37
Show file tree

Hide file tree

Showing 10 changed files with 46 additions and 28 deletions.
diff --git 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
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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();
+1 −0		src/goto-programs/name_mangler.cpp
+1 −0		src/goto-programs/osx_fat_reader.h
+2 −0		src/solvers/prop/prop.h
+2 −0		src/solvers/smt2/smt2_conv.cpp
+3 −2		src/util/ieee_float.cpp
+3 −2		src/util/unicode.cpp