From a3fa91130b2b0d93cc1ccb363cf1c8947a479bcc Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Tue, 18 Sep 2018 15:33:16 +0100
Subject: [PATCH] check for side effects in quantifiers in the front-end

This fixes a failed attempt to check for quantifiers during goto conversion
by checking earlier in the C front-end.
---
 .../Quantifiers1/quantifier-with-side-effect.c | 14 ++++++++++++++
 .../quantifier-with-side-effect.desc           |  7 +++++++
 src/ansi-c/c_typecheck_expr.cpp                |  8 ++++++++
 src/goto-programs/goto_clean_expr.cpp          | 18 +++++-------------
 4 files changed, 34 insertions(+), 13 deletions(-)
 create mode 100644 regression/cbmc/Quantifiers1/quantifier-with-side-effect.c
 create mode 100644 regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc

diff --git a/regression/cbmc/Quantifiers1/quantifier-with-side-effect.c b/regression/cbmc/Quantifiers1/quantifier-with-side-effect.c
new file mode 100644
index 00000000000..ac1b9010295
--- /dev/null
+++ b/regression/cbmc/Quantifiers1/quantifier-with-side-effect.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;
+}
diff --git a/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc b/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc
new file mode 100644
index 00000000000..144a4c31572
--- /dev/null
+++ b/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc
@@ -0,0 +1,7 @@
+CORE
+quantifier-with-side-effect.c
+
+^EXIT=6$
+^SIGNAL=0$
+^file .* line 10 function main: quantifier must not contain side effects$
+--
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 3040eb60c41..c152f14d5c8 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_util.h>
 #include <util/ieee_float.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -299,6 +300,13 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
       throw 0;
     }
 
+    if(has_subexpr(expr.op1(), ID_side_effect))
+    {
+      err_location(expr);
+      error() << "quantifier must not contain side effects" << eom;
+      throw 0;
+    }
+
     // replace declaration by symbol expression
     symbol_exprt bound=to_symbol_expr(expr.op0().op0());
     expr.op0().swap(bound);
diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp
index 43b906ff6b4..0a18294351a 100644
--- a/src/goto-programs/goto_clean_expr.cpp
+++ b/src/goto-programs/goto_clean_expr.cpp
@@ -11,10 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_convert_class.h"
 
+#include <util/cprover_prefix.h>
+#include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
-#include <util/cprover_prefix.h>
 
 #include <util/c_types.h>
 
@@ -405,18 +406,9 @@ void goto_convertt::clean_expr(
   }
   else if(expr.id()==ID_forall || expr.id()==ID_exists)
   {
-    assert(expr.operands().size()==2);
-    // check if there are side-effects
-    goto_programt tmp;
-    clean_expr(expr.op1(), tmp, mode, true);
-    if(tmp.instructions.empty())
-    {
-      error().source_location=expr.find_source_location();
-      error() << "no side-effects in quantified expressions allowed"
-              << eom;
-      throw 0;
-    }
-    return;
+    DATA_INVARIANT(
+      !has_subexpr(expr, ID_side_effect),
+      "the front-end should check quantified expressions for side-effects");
   }
   else if(expr.id()==ID_address_of)
   {