Merge pull request #2979 from diffblue/quantifier-sideeffects

check for side effects in quantifiers

Author: tautschnig

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

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$
+--

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

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)
   {