Merge pull request #6810 from tautschnig/bugfixes/binding

Extend support for binding expressions beyond quantifiers

Author: tautschnig

src/goto-symex/symex_clean_expr.cpp

@@ -212,7 +212,7 @@ void goto_symext::lift_lets(statet &state, exprt &rhs)
 
       it.next_sibling_or_parent();
     }
-    else if(it->id() == ID_exists || it->id() == ID_forall)
+    else if(can_cast_expr<binding_exprt>(*it))
     {
       // expressions within exists/forall may depend on bound variables, we
       // cannot safely lift let expressions out of those, just skip

src/goto-symex/symex_dereference.cpp

@@ -249,16 +249,16 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
 /// goto_symext::address_arithmetic) and certain common expression patterns
 /// such as `&struct.flexible_array[0]` (see inline comments in code).
 /// Note that \p write is used to alter behaviour when this function is
-/// operating on the LHS of an assignment. Similarly \p is_in_quantifier
-/// indicates when the dereference is inside a quantifier (related to scoping
-/// when dereference caching is enabled).
+/// operating on the LHS of an assignment. Similarly \p is_in_binding_expression
+/// indicates when the dereference is inside a binding expression (related to
+/// scoping when dereference caching is enabled).
 /// For full details of this method's pointer replacement and potential side-
 /// effects see \ref goto_symext::dereference
 void goto_symext::dereference_rec(
   exprt &expr,
   statet &state,
   bool write,
-  bool is_in_quantifier)
+  bool is_in_binding_expression)
 {
   if(expr.id()==ID_dereference)
   {
@@ -281,7 +281,7 @@ void goto_symext::dereference_rec(
     tmp1.swap(to_dereference_expr(expr).pointer());
 
     // first make sure there are no dereferences in there
-    dereference_rec(tmp1, state, false, is_in_quantifier);
+    dereference_rec(tmp1, state, false, is_in_binding_expression);
 
     // Depending on the nature of the pointer expression, the recursive deref
     // operation might have introduced a construct such as
@@ -345,7 +345,7 @@ void goto_symext::dereference_rec(
     //     (p == &something ? something : ...))
     // Otherwise we should just return it unchanged.
     if(
-      symex_config.cache_dereferences && !write && !is_in_quantifier &&
+      symex_config.cache_dereferences && !write && !is_in_binding_expression &&
       (tmp2.id() == ID_if || tmp2.id() == ID_let))
     {
       expr = cache_dereference(tmp2, state);
@@ -372,7 +372,7 @@ void goto_symext::dereference_rec(
     tmp.add_source_location()=expr.source_location();
 
     // recursive call
-    dereference_rec(tmp, state, write, is_in_quantifier);
+    dereference_rec(tmp, state, write, is_in_binding_expression);
 
     expr.swap(tmp);
   }
@@ -406,18 +406,22 @@ void goto_symext::dereference_rec(
       expr = address_of_exprt(index_exprt(
         to_address_of_expr(tc_op).object(), from_integer(0, c_index_type())));
 
-      dereference_rec(expr, state, write, is_in_quantifier);
+      dereference_rec(expr, state, write, is_in_binding_expression);
     }
     else
     {
-      dereference_rec(tc_op, state, write, is_in_quantifier);
+      dereference_rec(tc_op, state, write, is_in_binding_expression);
     }
   }
   else
   {
-    bool is_quantifier = expr.id() == ID_forall || expr.id() == ID_exists;
+    bool is_binding_expression =
+      can_cast_expr<binding_exprt>(expr) || can_cast_expr<let_exprt>(expr);
     Forall_operands(it, expr)
-      dereference_rec(*it, state, write, is_in_quantifier || is_quantifier);
+    {
+      dereference_rec(
+        *it, state, write, is_in_binding_expression || is_binding_expression);
+    }
   }
 }
 

src/util/std_expr.h

@@ -3099,6 +3099,13 @@ class binding_exprt : public binary_exprt
   exprt instantiate(const variablest &) const;
 };
 
+template <>
+inline bool can_cast_expr<binding_exprt>(const exprt &base)
+{
+  return base.id() == ID_forall || base.id() == ID_exists ||
+         base.id() == ID_lambda || base.id() == ID_array_comprehension;
+}
+
 inline void validate_expr(const binding_exprt &binding_expr)
 {
   validate_operands(