Merge pull request #8093 from NlightNFotis/new_flags_on_clean

Enable default analysis flags for CBMC version 6.0+
diffblue · Dec 13, 2023 · 41af31c · 41af31c
2 parents 9459ea5 + 9747f61
commit 41af31c
Show file tree

Hide file tree

Showing 48 changed files with 360 additions and 93 deletions.
diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1
@@ -8,6 +8,12 @@ cbmc \- Bounded Model Checker for C/C++ and Java programs
 
 .B cbmc [--all-properties] \fIfile.c\fB ...
 
+.B cbmc [--no-standard-checks] \fIfile.c\fB ...
+
+.B cbmc [--no-standard-checks] [--pointer-check] \fIfile.c\fB ...
+
+.B cbmc [--no-bounds-check] \fIfile.c\fB ...
+
 .B goto-cc [-I \fIinclude-path\fB] [-c] \fIfile.c\fB [-o \fIoutfile.o\fB]
 
 .B goto-instrument \fIinfile\fB \fIoutfile\fR
@@ -41,8 +47,79 @@ The usual flow is to (1) translate source into a GOTO binary using
 goto-cc, then (2) perform instrumentation with goto-instrument, and
 finally (3) perform the analysis with cbmc.
 .SH OPTIONS
+.SS "Standard Checks"
+From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
+apply some checks to the program by default (called the "standard checks"), with the
+aim to provide a better user experience for a non-expert user of the tool. These checks are:
+.TP
+\fB\-\-pointer\-check\fR
+enable pointer checks
+.TP
+\fB\-\-bounds\-check\fR
+enable array bounds checks
+.TP
+\fB\-\-undefined\-shift\-check\fR
+check shift greater than bit\-width
+.TP
+\fB\-\-div\-by\-zero\-check\fR
+enable division by zero checks
+.TP
+\fB\-\-pointer\-primitive\-check\fR
+checks that all pointers in pointer primitives are valid or null
+.TP
+\fB\-\-signed\-overflow\-check\fR
+enable signed arithmetic over\- and underflow checks
+.TP
+\fB\-\-malloc\-may\-fail\fR
+allow malloc calls to return a null pointer
+.TP
+\fB\-\-malloc\-fail\-null\fR
+set malloc failure mode to return null
+.TP
+\fB\-\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
+generate unwinding assertions (cannot be
+used with \fB\-\-cover\fR)
+.PP
+These checks can all be deactivated at once by using the \fB\-\-no\-standard\-checks\fR flag
+like in the header example, or individually, by prepending a \fBno\-\fR before the flag, like
+so:
+.TP
+\fB\-\-no\-pointer\-check\fR
+disable pointer checks
+.TP
+\fB\-\-no\-bounds\-check\fR
+disable array bounds checks
+.TP
+\fB\-\-no\-undefined\-shift\-check\fR
+do not perform check for shift greater than bit\-width
+.TP
+\fB\-\-no\-div\-by\-zero\-check\fR
+disable division by zero checks
+.TP
+\fB\-\-no\-pointer\-primitive\-check\fR
+do not check that all pointers in pointer primitives are valid or null
+.TP
+\fB\-\-no\-signed\-overflow\-check\fR
+disable signed arithmetic over\- and underflow checks
+.TP
+\fB\-\-no\-malloc\-may\-fail\fR
+do not allow malloc calls to fail by default
+.TP
+\fB\-\-no\-malloc\-fail\-null\fR
+do not set malloc failure mode to return null pointer
+.TP
+\fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
+do not generate unwinding assertions (cannot be
+used with \fB\-\-cover\fR)
+.PP
+If an already set flag is re-set, like calling \fB\-\-pointer\-check\fR
+when default checks are already on, the flag is simply ignored.
 .SS "Analysis options:"
 .TP
+\fB\-\-no\-standard\-checks\fR
+disable the standard (default) checks applied to a C/GOTO program
+(see above for more information)
+.TP
 \fB\-\-show\-properties\fR
 show the properties, but don't run analysis
 .TP

diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1
@@ -8,6 +8,12 @@ goto-analyzer \- Data-flow analysis for C programs and goto binaries
 
 .B goto\-analyzer [options] file.c|file.gb
 
+.B goto\-analyzer [--no-standard-checks] \fIfile.c\fB ...
+
+.B goto\-analyzer [--no-standard-checks] [--pointer-check] \fIfile.c\fB ...
+
+.B goto\-analyzer [--no-bounds-check] \fIfile.c\fB ...
+
 .SH DESCRIPTION
 .B goto-analyzer
 is an abstract interpreter which uses the same
@@ -494,6 +500,10 @@ list loaded goto functions
 show the properties, but don't run analysis
 .SS "Program instrumentation options:"
 .TP
+\fB\-\-no\-standard\-checks\fR
+disable the standard (default) checks applied to a C/GOTO program
+(see below for more information)
+.TP
 \fB\-\-property\fR id
 enable selected properties only
 .TP
@@ -569,6 +579,73 @@ set malloc failure mode to return null
 .TP
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
+.SS "Standard Checks"
+From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
+apply some checks to the program by default (called the "standard checks"), with the
+aim to provide a better user experience for a non-expert user of the tool. These checks are:
+.TP
+\fB\-\-pointer\-check\fR
+enable pointer checks
+.TP
+\fB\-\-bounds\-check\fR
+enable array bounds checks
+.TP
+\fB\-\-undefined\-shift\-check\fR
+check shift greater than bit\-width
+.TP
+\fB\-\-div\-by\-zero\-check\fR
+enable division by zero checks
+.TP
+\fB\-\-pointer\-primitive\-check\fR
+checks that all pointers in pointer primitives are valid or null
+.TP
+\fB\-\-signed\-overflow\-check\fR
+enable signed arithmetic over\- and underflow checks
+.TP
+\fB\-\-malloc\-may\-fail\fR
+allow malloc calls to return a null pointer
+.TP
+\fB\-\-malloc\-fail\-null\fR
+set malloc failure mode to return null
+.TP
+\fB\-\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
+generate unwinding assertions (cannot be
+used with \fB\-\-cover\fR)
+.PP
+These checks can all be deactivated at once by using the \fB\-\-no\-standard\-checks\fR flag
+like in the header example, or individually, by prepending a \fBno\-\fR before the flag, like
+so:
+.TP
+\fB\-\-no\-pointer\-check\fR
+disable pointer checks
+.TP
+\fB\-\-no\-bounds\-check\fR
+disable array bounds checks
+.TP
+\fB\-\-no\-undefined\-shift\-check\fR
+do not perform check for shift greater than bit\-width
+.TP
+\fB\-\-no\-div\-by\-zero\-check\fR
+disable division by zero checks
+.TP
+\fB\-\-no\-pointer\-primitive\-check\fR
+do not check that all pointers in pointer primitives are valid or null
+.TP
+\fB\-\-no\-signed\-overflow\-check\fR
+disable signed arithmetic over\- and underflow checks
+.TP
+\fB\-\-no\-malloc\-may\-fail\fR
+do not allow malloc calls to fail by default
+.TP
+\fB\-\-no\-malloc\-fail\-null\fR
+do not set malloc failure mode to return null pointer
+.TP
+\fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
+do not generate unwinding assertions (cannot be
+used with \fB\-\-cover\fR)
+.PP
+If an already set flag is re-set, like calling \fB\-\-pointer\-check\fR
+when default checks are already on, the flag is simply ignored.
 .SS "Other options:"
 .TP
 \fB\-\-validate\-goto\-model\fR

diff --git a/regression/acceleration/accelerate.sh b/regression/acceleration/accelerate.sh
@@ -16,7 +16,7 @@ is_windows=$4
 shift 4
 
 cfile=""
-cbmcargs=""
+cbmcargs="--no-standard-checks"
 
 # create the temporary directory relative to the current directory, thus
 # avoiding file names that start with a "/", which confuses goto-cl (Windows)

diff --git a/regression/book-examples/CMakeLists.txt b/regression/book-examples/CMakeLists.txt
@@ -13,27 +13,27 @@ else()
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
+    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
 )
 
 add_test_pl_profile(
     "book-examples-paths-lifo"
-    "$<TARGET_FILE:cbmc> --paths lifo"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --paths lifo"
     "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
     "CORE"
 )
 
 add_test_pl_profile(
     "book-examples-cprover-smt2"
-    "$<TARGET_FILE:cbmc> --cprover-smt2"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --cprover-smt2"
     "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
     "CORE"
 )
 
 # If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
 add_test_pl_profile(
   "book-examples-new-smt-backend"
-  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
+  "$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'"
   "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
   "CORE"
 )

diff --git a/regression/book-examples/Makefile b/regression/book-examples/Makefile
@@ -10,27 +10,27 @@ GCC_ONLY =
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
 
 test-cprover-smt2:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --cprover-smt2" \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
 					  -s cprover-smt2 $(GCC_ONLY)
 
 test-z3:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --z3" \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
 					  -s z3 $(GCC_ONLY)
 
 test-paths-lifo:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --paths lifo" \
 					  -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
 					  -s paths-lifo $(GCC_ONLY)
 
 test-new-smt-backend:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" \
 					  -X no-new-smt \
 					  -s new-smt-backend $(GCC_ONLY)
 

diff --git a/regression/cbmc-concurrency/CMakeLists.txt b/regression/cbmc-concurrency/CMakeLists.txt
@@ -1,11 +1,11 @@
 if((NOT WIN32) AND (NOT APPLE))
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
 )
 else()
 add_test_pl_profile(
     "cbmc-concurrency"
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
     "-C;-X;pthread"
     "CORE"
 )

diff --git a/regression/cbmc-concurrency/Makefile b/regression/cbmc-concurrency/Makefile
@@ -10,10 +10,10 @@ ifeq ($(filter-out OSX MSVC,$(BUILD_ENV_)),)
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(no_pthread)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(no_pthread)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(no_pthread)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(no_pthread)
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;

diff --git a/regression/cbmc-cover/CMakeLists.txt b/regression/cbmc-cover/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
+    "$<TARGET_FILE:cbmc> --no-standard-checks"
 )
diff --git a/regression/cbmc-cover/Makefile b/regression/cbmc-cover/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks"
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks"
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;

diff --git a/regression/cbmc-cpp/CMakeLists.txt b/regression/cbmc-cpp/CMakeLists.txt
@@ -5,5 +5,5 @@ else()
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only}
+    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation" ${gcc_only}
 )
diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile
@@ -8,10 +8,10 @@ ifeq ($(BUILD_ENV_),MSVC)
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(excluded_tests)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(excluded_tests)
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;

diff --git a/regression/cbmc-incr-oneloop/CMakeLists.txt b/regression/cbmc-incr-oneloop/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "perl ../timeout.pl 8 $<TARGET_FILE:cbmc> --slice-formula"
+    "perl ../timeout.pl 8 $<TARGET_FILE:cbmc> --no-standard-checks --slice-formula"
 )
diff --git a/regression/cbmc-incr-oneloop/Makefile b/regression/cbmc-incr-oneloop/Makefile
@@ -2,10 +2,10 @@ default: tests.log
 
 # Note the `perl -e` serves the purpose of providing timeout
 test:
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --no-standard-checks --slice-formula"
 
 tests.log: ../test.pl
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --no-standard-checks --slice-formula"
 
 clean:
 	@$(RM) *.log

diff --git a/regression/cbmc-incr-smt2/CMakeLists.txt b/regression/cbmc-incr-smt2/CMakeLists.txt
@@ -1,13 +1,13 @@
 add_test_pl_profile(
     "cbmc-incr-smt2-z3"
-    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
     "-C;-s;new-smt-z3"
     "CORE"
 )
 
 add_test_pl_profile(
     "cbmc-incr-smt2-cvc5"
-    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
     "-C;-s;new-smt-cvc5"
     "CORE"
 )
diff --git a/regression/cbmc-incr-smt2/Makefile b/regression/cbmc-incr-smt2/Makefile
@@ -6,10 +6,10 @@ include ../../src/common
 test: test.z3 test.cvc5
 
 test.z3:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
 
 test.cvc5:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../test.pl test
 

diff --git a/regression/cbmc-incr/CMakeLists.txt b/regression/cbmc-incr/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "perl ../timeout.pl 30 $<TARGET_FILE:cbmc> --incremental --magic-numbers"
+    "perl ../timeout.pl 30 $<TARGET_FILE:cbmc> --no-standard-checks --incremental --magic-numbers"
 )
diff --git a/regression/cbmc-incr/Makefile b/regression/cbmc-incr/Makefile
@@ -1,6 +1,6 @@
 default: tests.log
 
-PARAM = --incremental --magic-numbers
+PARAM = --incremental --magic-numbers --no-standard-checks
 # --refine   --slice-formula
 
 test: