Fix: Handle quantifiers with statement expressions in CBMC

This commit addresses the issue of handling quantifiers that contain statement expressions in CBMC. Previously, quantifiers without side effects were not supported.

Changes include:
- Added logic to handle quantifiers with statement expressions in `goto_clean_expr.cpp`.
- Updated `c_typecheck_expr.cpp` to allow quantifiers with statement expressions.
- Introduced new tests to verify the correct handling of quantifiers with statement expressions.

Author: qinheping

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;
     }