Skip to content

Commit 2cd4154

Browse files
remi-delmas-3000remi-delmas-3000
authored
Merge pull request #7242 from remi-delmas-3000/rebase-dfcc-fix-regression
CONTRACTS: Dynamic frame condition checking
2 parents 7b4b59a + e22a788 commit 2cd4154

File tree

577 files changed

+21303
-476
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

577 files changed

+21303
-476
lines changed

‎doc/cprover-manual/contracts-requires-and-ensures.md

Lines changed: 0 additions & 136 deletions
This file was deleted.

‎doc/man/goto-instrument.1

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1003,6 +1003,12 @@ replace calls to \fIfun\fR with \fIfun\fR's contract
10031003
.TP
10041004
\fB\-\-enforce\-contract\fR \fIfun\fR
10051005
wrap \fIfun\fR with an assertion of its contract
1006+
.TP
1007+
\fB\-\-enforce\-contract\-rec\fR \fIfun\fR
1008+
wrap \fIfun\fR with an assertion of its contract that can handle recursive calls
1009+
.TP
1010+
\fB\-\-dfcc\fR \fIfun\fR
1011+
instrument dynamic frame condition checks method using \fIfun\fR as entry point
10061012
.SS "User-interface options:"
10071013
.TP
10081014
\fB\-\-flush\fR

‎regression/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,7 @@ add_subdirectory(goto-analyzer-simplify)
6565
add_subdirectory(statement-list)
6666
add_subdirectory(systemc)
6767
add_subdirectory(contracts)
68+
add_subdirectory(contracts-dfcc)
6869
add_subdirectory(acceleration)
6970
add_subdirectory(k-induction)
7071
add_subdirectory(goto-harness)

‎regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ DIRS = cbmc \
3838
statement-list \
3939
systemc \
4040
contracts \
41+
contracts-dfcc \
4142
acceleration \
4243
k-induction \
4344
goto-harness \

‎regression/contracts-dfcc/CMakeLists.txt

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
if(WIN32)
2+
set(is_windows true)
3+
else()
4+
set(is_windows false)
5+
endif()
6+
7+
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
8+
set(gcc_only -X gcc-only)
9+
set(gcc_only_string "-X;gcc-only;")
10+
else()
11+
set(gcc_only "")
12+
set(gcc_only_string "")
13+
endif()
14+
15+
16+
add_test_pl_tests(
17+
"${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
18+
)
19+
20+
## Enabling these causes a very significant increase in the time taken to run the regressions
21+
22+
#add_test_pl_profile(
23+
# "cbmc-z3"
24+
# "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> '$<TARGET_FILE:cbmc> --z3' ${is_windows}"
25+
# "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-z3-backend;-X;thorough-z3-backend;${gcc_only_string}-s;z3"
26+
# "CORE"
27+
#)
28+
29+
#add_test_pl_profile(
30+
# "cbmc-cprover-smt2"
31+
# "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> '$<TARGET_FILE:cbmc> --cprover-smt2' ${is_windows}"
32+
# "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt2-backend;-X;thorough-cprover-smt2-backend;${gcc_only_string}-s;cprover-smt2"
33+
# "CORE"
34+
#)
35+
36+
# solver appears on the PATH in Windows already
37+
#if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
38+
# set_property(
39+
# TEST "cbmc-cprover-smt2-CORE"
40+
# PROPERTY ENVIRONMENT
41+
# "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
42+
# )
43+
#endif()

‎regression/contracts-dfcc/Makefile

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
default: test
2+
3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
exe=../../../src/goto-cc/goto-cl
8+
is_windows=true
9+
GCC_ONLY = -X gcc-only
10+
else
11+
exe=../../../src/goto-cc/goto-cc
12+
is_windows=false
13+
GCC_ONLY =
14+
endif
15+
16+
test:
17+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X smt-backend $(GCC_ONLY)
18+
19+
test-cprover-smt2:
20+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument "../../../src/cbmc/cbmc --cprover-smt2" $(is_windows)' \
21+
-X broken-smt-backend -X thorough-smt-backend \
22+
-X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
23+
-s cprover-smt2 $(GCC_ONLY)
24+
25+
test-z3:
26+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument "../../../src/cbmc/cbmc --z3" $(is_windows)' \
27+
-X broken-smt-backend -X thorough-smt-backend \
28+
-X broken-z3-smt-backend -X thorough-z3-smt-backend \
29+
-s z3 $(GCC_ONLY)
30+
31+
tests.log: ../test.pl test
32+
33+
34+
clean:
35+
@for dir in *; do \
36+
$(RM) tests.log; \
37+
if [ -d "$$dir" ]; then \
38+
cd "$$dir"; \
39+
$(RM) *.out *.gb *.smt2; \
40+
cd ..; \
41+
fi \
42+
done

‎regression/contracts-dfcc/assigns-enforce-malloc-zero/main.c

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
#include <stdlib.h>
2+
3+
// returns the index at which the write was performed if any
4+
// -1 otherwise
5+
int foo(char *a, int size)
6+
// clang-format off
7+
__CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
8+
__CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size))
9+
__CPROVER_assigns(a: __CPROVER_object_whole(a))
10+
__CPROVER_ensures(
11+
a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
12+
// clang-format on
13+
{
14+
if(!a)
15+
return -1;
16+
int i;
17+
if(0 <= i && i < size)
18+
{
19+
a[i] = 0;
20+
return i;
21+
}
22+
return -1;
23+
}
24+
25+
int main()
26+
{
27+
size_t size;
28+
char *a;
29+
foo(a, size);
30+
return 0;
31+
}

‎regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--dfcc main --enforce-contract foo _ --malloc-may-fail --malloc-fail-null
4+
^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
This test checks that objects of size zero or __CPROVER_max_malloc_size
10+
do not cause spurious falsifications in assigns clause instrumentation
11+
in contract enforcement mode.

0 commit comments

Comments
 (0)