Protect the body of ForAllExpr, ExistsExpr and LambdaExpr when they

are immutable. Add unit tests to check this.

2 files changed, 51 insertions, 2 deletions

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 62c3f8bf..1bd16e4a 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -49,7 +49,19 @@ namespace Microsoft.Boogie {
     public List<TypeVariable>/*!*/ TypeParameters;

     public List<Variable>/*!*/ Dummies;

     public QKeyValue Attributes;

-    public Expr/*!*/ Body;

+    // FIXME: Protect the above Fields

+    public Expr _Body;

+    public Expr/*!*/ Body {

+      get {

+        return _Body;

+      }

+      set {

+        if (Immutable)

+          throw new InvalidOperationException ("Cannot change the Body of an immutable BinderExpr");

+

+        _Body = value;

+      }

+    }

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(TypeParameters != null);

@@ -68,7 +80,7 @@ namespace Microsoft.Boogie {
       TypeParameters = typeParameters;

       Dummies = dummies;

       Attributes = kv;

-      Body = body;

+      _Body = body;

       if (immutable)

         CachedHashCode = ComputeHashCode();

     }

diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs
index f3225b0f..9a9536c1 100644
--- a/Source/UnitTests/CoreTests/ExprImmutability.cs
+++ b/Source/UnitTests/CoreTests/ExprImmutability.cs
@@ -140,6 +140,43 @@ namespace CoreTests
             var e = GetUnTypedImmutableNAry();
             e.Fun = new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.Sub);
         }
+
+        [Test(), ExpectedException(typeof(InvalidOperationException))]
+        public void ProtectedForAllExprBody()
+        {
+            var x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int));
+            var y = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int));
+            var xId = new IdentifierExpr(Token.NoToken, x, /*immutable=*/true);
+            var yId = new IdentifierExpr(Token.NoToken, y, /*immutable=*/true);
+            var body = Expr.Gt(xId, yId);
+            var forAll = new ForallExpr(Token.NoToken, new List<Variable> () { x, y }, body, /*immutable=*/true);
+            forAll.Body = Expr.Lt(xId, yId); // Changing the body of an immutable ForAllExpr should fail
+        }
+
+        [Test(), ExpectedException(typeof(InvalidOperationException))]
+        public void ProtectedExistsExprBody()
+        {
+            var x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int));
+            var y = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int));
+            var xId = new IdentifierExpr(Token.NoToken, x, /*immutable=*/true);
+            var yId = new IdentifierExpr(Token.NoToken, y, /*immutable=*/true);
+            var body = Expr.Gt(xId, yId);
+            var exists = new ExistsExpr(Token.NoToken, new List<Variable> () { x, y }, body, /*immutable=*/true);
+            exists.Body = Expr.Lt(xId, yId); // Changing the body of an immutable ExistsExpr should fail
+        }
+
+        [Test(), ExpectedException(typeof(InvalidOperationException))]
+        public void ProtectedLambdaExprBody()
+        {
+            var x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int));
+            var y = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", BasicType.Int));
+            var xId = new IdentifierExpr(Token.NoToken, x, /*immutable=*/true);
+            var yId = new IdentifierExpr(Token.NoToken, y, /*immutable=*/true);
+            var body = Expr.Gt(xId, yId);
+            var lambda = new LambdaExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable>() { x, y},
+                null, body, /*immutable=*/true);
+            lambda.Body = Expr.Lt(xId, yId); // Changing the body of an immutable ExistsExpr should fail
+        }
     }
 }