CONTRACTS: Avoid single conjunction in contracts instrumentation

feliperodri · feliperodri · commit 7c1f67a45acc · 2022-10-03T17:00:30.000Z
Currently, requires and ensures clauses are always combined into
a single conjunction. The resulting clause is then used to create
a single assertion or assumption, which makes really difficult
to debug issues with large function contracts. This commit
preserves the source location of the clauses by creating one
assertion/assumption for each clause in the function contract
(i.e., either requires or ensures).

Signed-off-by: Felipe R. Monteiro &lt;felisous@amazon.com&gt;
diff --git a/regression/contracts/assigns-replace-ignored-return-value/test.desc b/regression/contracts/assigns-replace-ignored-return-value/test.desc
@@ -1,6 +1,8 @@
 CORE
 main.c
 --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
+^\[bar.precondition.\d+\] line \d+ Check bar's requires clause in foo: SUCCESS$
+^\[baz.precondition.\d+\] line \d+ Check baz's requires clause in foo: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/assigns-replace-malloc-zero/test.desc b/regression/contracts/assigns-replace-malloc-zero/test.desc
@@ -1,6 +1,7 @@
 CORE
 main.c
 --replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null
+^\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$
diff --git a/regression/contracts/history-pointer-replace-04/test.desc b/regression/contracts/history-pointer-replace-04/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-^\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
+^\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion p->y \!\= 7: FAILURE$
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/quantifiers-exists-both-replace/test.desc b/regression/contracts/quantifiers-exists-both-replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
+^\[f1.precondition.\d+\] line \d+ Check f1's requires clause in main: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-exists-requires-replace/test.desc b/regression/contracts/quantifiers-exists-requires-replace/test.desc
@@ -3,8 +3,8 @@ main.c
 --replace-call-with-contract f1 --replace-call-with-contract f2
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
-^\[f2.precondition.\d+\] line \d+ Check requires clause: FAILURE$
+^\[f1.precondition.\d+\] line \d+ Check f1's requires clause in main: SUCCESS$
+^\[f2.precondition.\d+\] line \d+ Check f2's requires clause in main: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-both-replace/test.desc b/regression/contracts/quantifiers-forall-both-replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
+^\[f1.precondition.\d+\] line \d+ Check f1's requires clause in main: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-forall-requires-replace/test.desc b/regression/contracts/quantifiers-forall-requires-replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.precondition.\d+\] line \d+ Check requires clause: SUCCESS$
+^\[f1.precondition.\d+\] line \d+ Check f1's requires clause in main: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/test_aliasing_replace/test.desc b/regression/contracts/test_aliasing_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-\[foo.precondition.\d+\] line \d+ Check requires clause: FAILURE
+\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: FAILURE
 \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/test_array_memory_replace/test.desc b/regression/contracts/test_array_memory_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS
+\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion n\[9\] == 113: SUCCESS
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/test_array_memory_too_small_replace/test.desc b/regression/contracts/test_array_memory_too_small_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-\[foo.precondition.\d+\] line \d+ Check requires clause: FAILURE
+\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: FAILURE
 \[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/test_possibly_aliased_arguments/test.desc b/regression/contracts/test_possibly_aliased_arguments/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract sub_ptr_values
 ^EXIT=0$
 ^SIGNAL=0$
-\[sub_ptr_values.precondition.\d+\] line \d+ Check requires clause: SUCCESS
+\[sub_ptr_values.precondition.\d+\] line \d+ Check sub\_ptr\_values's requires clause in main: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/test_scalar_memory_replace/test.desc b/regression/contracts/test_scalar_memory_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS
+\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \_\_CPROVER\_r\_ok\(n, sizeof\(int\)\): SUCCESS
 \[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/test_struct_replace/test.desc b/regression/contracts/test_struct_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[foo.precondition.\d+\] line \d+ Check requires clause: SUCCESS
+\[foo.precondition.\d+\] line \d+ Check foo's requires clause in main: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion rval \=\= x->baz \+ x->qux: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \*x \=\= \*y: SUCCESS
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/variant_multidimensional_ackermann/test.desc b/regression/contracts/variant_multidimensional_ackermann/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --apply-loop-contracts --replace-call-with-contract ackermann
-^\[ackermann.precondition\.\d+\] line 17 Check requires clause: SUCCESS$
-^\[ackermann.precondition\.\d+\] line 17 Check requires clause: SUCCESS$
+^\[ackermann.precondition\.\d+\] line 9 Check ackermann's requires clause in main: SUCCESS$
+^\[ackermann.precondition\.\d+\] line 34 Check ackermann's requires clause in ackermann: SUCCESS$
 ^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$
 ^\[ackermann\.\d+\] line 21 Check that loop invariant is preserved: SUCCESS$
 ^\[ackermann\.\d+\] line 21 Check decreases clause on loop iteration: SUCCESS$
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
