Protect E0 and E1 in BvConcatExpr if Expr is immutable.

2 files changed, 45 insertions, 4 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 75f2c519..2427d856 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -3080,8 +3080,29 @@ namespace Microsoft.Boogie {
   }

 

   public class BvConcatExpr : Expr {

-    // FIXME: Protect these fields

-    public /*readonly--except in StandardVisitor*/ Expr/*!*/ E0, E1;

+    private /*readonly--except in StandardVisitor*/ Expr/*!*/ _E0, _E1;

+    public Expr E0 {

+      get {

+        return _E0;

+      }

+      set {

+        if (Immutable)

+           throw new InvalidOperationException("Can't change E0 reference on immutable Expr");

+

+        _E0 = value;

+      }

+    }

+    public Expr E1 {

+      get {

+        return _E1;

+      }

+      set {

+        if (Immutable)

+          throw new InvalidOperationException("Can't change E1 reference on immutable Expr");

+

+        _E1 = value;

+      }

+    }

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(E0 != null);

@@ -3094,8 +3115,8 @@ namespace Microsoft.Boogie {
       Contract.Requires(tok != null);

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      E0 = e0;

-      E1 = e1;

+      _E0 = e0;

+      _E1 = e1;

       if (immutable)

         CachedHashCode = ComputeHashCode();

     }

diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs
index a26f8b8b..98e7158f 100644
--- a/Source/UnitTests/CoreTests/ExprImmutability.cs
+++ b/Source/UnitTests/CoreTests/ExprImmutability.cs
@@ -249,6 +249,26 @@ namespace CoreTests
                 null, body, /*immutable=*/true);
             lambda.Body = Expr.Lt(xId, yId); // Changing the body of an immutable ExistsExpr should fail
         }
+
+        [Test(), ExpectedException(typeof(InvalidOperationException))]
+        public void ProtectedBvConcatExprLhs()
+        {
+            var lhs = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 32, /*immutable=*/true);
+            var rhs = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1), 32, /*immutable=*/true);
+            var concat = new BvConcatExpr(Token.NoToken, lhs, rhs,/* immutable=*/true);
+            Assert.IsTrue(concat.Immutable);
+            concat.E0 = rhs; // Should throw
+        }
+
+        [Test(), ExpectedException(typeof(InvalidOperationException))]
+        public void ProtectedBvConcatExprRhs()
+        {
+            var lhs = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(0), 32, /*immutable=*/true);
+            var rhs = new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1), 32, /*immutable=*/true);
+            var concat = new BvConcatExpr(Token.NoToken, lhs, rhs,/* immutable=*/true);
+            Assert.IsTrue(concat.Immutable);
+            concat.E1 = lhs; // Should throw
+        }
     }
 }