Merge pull request #8605 from qinheping/quantifiers-with-statement-expressions

Handle quantifiers with statement expressions

Author: tautschnig

regression/cbmc/Quantifiers-statement-expression/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+  // clang-format off
+  // no side effects!
+  int j = 0;
+  //assert(j++);
+  //assert(({int i = 0; while(i <3) i++; i <3;}));
+  int a[5] = {0 , 0, 0, 0, 0};
+  assert(__CPROVER_forall { int i;  ({ int j = i; i=i; if(i < 0 || i >4) i = 1;  ( a[i] < 5); }) });
+  // clang-format on
+
+  return 0;
+}

regression/cbmc/Quantifiers-statement-expression/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Quantifiers-statement-expression2/main.c

@@ -0,0 +1,16 @@
+int main()
+{
+  int b[2];
+  int c[2];
+
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
+  __CPROVER_assume( __CPROVER_forall { char i; ({ _Bool flag = (i>=0 && i<2); flag ==> b[i]>=10 && b[i]<=10; }) } );
+  __CPROVER_assume( __CPROVER_forall { unsigned i; ({ _Bool flag = (i>=0 && i<2); flag ==> c[i]>=10 && c[i]<=10; }) } );
+  // clang-format on
+
+  assert(b[0] == 10 && b[1] == 10);
+  assert(c[0] == 10 && c[1] == 10);
+
+  return 0;
+}

regression/cbmc/Quantifiers-statement-expression2/test.desc

@@ -0,0 +1,11 @@
+CORE no-new-smt
+main.c
+
+^\*\* Results:$
+^\[main.assertion.1\] line 12 assertion b\[.*0\] == 10 && b\[.*1\] == 10: SUCCESS$
+^\[main.assertion.2\] line 13 assertion c\[.*0\] == 10 && c\[.*1\] == 10: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Quantifiers1/quantifier-with-function-call.c

@@ -0,0 +1,14 @@
+int func()
+{
+  return 1;
+}
+
+int main()
+{
+  // clang-format off
+  // no side effects!
+  assert(__CPROVER_forall { int i; func() });
+  // clang-format on
+
+  return 0;
+}

regression/cbmc/Quantifiers1/quantifier-with-function-call.desc

@@ -0,0 +1,8 @@
+CORE
+quantifier-with-function-call.c
+
+^EXIT=6$
+^SIGNAL=0$
+quantifier must not contain function calls
+--
+^warning: ignoring

regression/cbmc/Quantifiers1/quantifier-with-side-effect.c

@@ -1,13 +1,9 @@
-int func()
-{
-  return 1;
-}
-
 int main()
 {
+  int j = 0;
   // clang-format off
   // no side effects!
-  assert(__CPROVER_forall { int i; func() });
+  assert(__CPROVER_forall { int i; ({ j = 1; j; }) });
   // clang-format on
 
   return 0;

regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc

@@ -1,8 +1,8 @@
 CORE
 quantifier-with-side-effect.c
 
-^EXIT=6$
+^EXIT=(127|134)$
 ^SIGNAL=0$
-^file .* line 10 function main: quantifier must not contain side effects$
+^Invariant check failed
+^Reason: quantifier must not contain side effects
 --
-^warning: ignoring

regression/contracts-dfcc/quantifiers-exists-both-enforce/with_statement_expression.c

@@ -0,0 +1,20 @@
+// clang-format off
+int f1(int *arr)
+  __CPROVER_requires(__CPROVER_exists {
+    int i;
+    ({(0 <= i && i < 8) && arr[i] == 0;})
+  })
+  __CPROVER_ensures(__CPROVER_exists {
+    int i;
+    ({(0 <= i && i < 8) && arr[i] == 0;})
+  })
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[8];
+  f1(arr);
+}

regression/contracts-dfcc/quantifiers-exists-both-enforce/with_statement_expression.desc

@@ -0,0 +1,16 @@
+CORE
+with_statement_expression.c
+--dfcc main --enforce-contract f1
+^EXIT=0$
+^SIGNAL=0$
+^\[f1.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::f1 for function f1)?: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists within both
+positive and negative contexts (ENSURES and REQUIRES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the ENSURES clause being enforced in this case,
+are supported only if the quantifier is bound to a constant range.

regression/contracts-dfcc/quantifiers-exists-both-replace/with_statement_expression.c

@@ -0,0 +1,42 @@
+#include <stdlib.h>
+
+#define MAX_LEN 8
+
+// clang-format off
+int f1(int *arr, int len)
+  __CPROVER_requires(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // constant bounds for explicit unrolling with SAT backend
+      ({ (0 <= i && i < MAX_LEN) && (
+        // actual symbolic bound for `i`
+        i < len && arr[i] == 0
+      ); })
+    }
+  )
+  __CPROVER_ensures(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // constant bounds for explicit unrolling with SAT backend
+      ({ (0 <= i && i < MAX_LEN) && (
+        // actual symbolic bound for `i`
+        i < len && arr[i] == 0
+      ); })
+    }
+  )
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int len;
+  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+
+  int *arr = malloc(len);
+  if(len > 0)
+    arr[0] = 0;
+
+  f1(arr, len);
+}

regression/contracts-dfcc/quantifiers-exists-both-replace/with_statement_expression.desc

@@ -0,0 +1,16 @@
+CORE
+with_statement_expression.c
+--no-malloc-may-fail --dfcc main --replace-call-with-contract f1 _ --no-standard-checks
+^EXIT=0$
+^SIGNAL=0$
+^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists within both
+positive and negative contexts (ENSURES and REQUIRES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the REQUIRES clause being replaced in this case,
+are supported only if the quantifier is bound to a constant range.

regression/validate-trace-xml-schema/check.py

@@ -74,7 +74,8 @@
     # the SAT back-end only
     ['integer-assignments1', 'test.desc'],
     # this test is expected to abort, thus producing invalid XML
-    ['String_Abstraction17', 'test.desc']
+    ['String_Abstraction17', 'test.desc'],
+    ['Quantifiers1', 'quantifier-with-side-effect.desc']
 ]))
 
 # TODO maybe consider looking them up on PATH, but direct paths are

src/ansi-c/c_typecheck_expr.cpp

@@ -316,10 +316,16 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
       }
     }
 
-    if(has_subexpr(where, ID_side_effect))
+    if(has_subexpr(
+         where,
+         [&](const exprt &subexpr)
+         {
+           return can_cast_expr<side_effect_exprt>(subexpr) &&
+                  can_cast_expr<side_effect_expr_function_callt>(subexpr);
+         }))
     {
       error().source_location = expr.source_location();
-      error() << "quantifier must not contain side effects" << eom;
+      error() << "quantifier must not contain function calls" << eom;
       throw 0;
     }