Fix ForAllExpr, ExistsExpr and LambdaExpr constructors so it is possible

to set them as immutable (not currently enforced for these Expr types).

2 files changed, 58 insertions, 21 deletions

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index f7665a07..62c3f8bf 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -35,7 +35,7 @@ namespace Microsoft.Boogie {
         throw new NotImplementedException();

       }

     }

-    public BinderExprContracts():base(null,null,null,null,null){

+    public BinderExprContracts():base(null,null,null,null,null,false){

   }

 

     public override Type ShallowType {

@@ -58,7 +58,7 @@ namespace Microsoft.Boogie {
     }

 

     public BinderExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,

-                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable=false)

+                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable)

       : base(tok, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParameters != null);

@@ -547,30 +547,30 @@ namespace Microsoft.Boogie {
 

   public class ForallExpr : QuantifierExpr {

     public ForallExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams,

-                      List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)

-      : base(tok, typeParams, dummies, kv, triggers, body) {

+                      List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false)

+      : base(tok, typeParams, dummies, kv, triggers, body, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParams != null);

       Contract.Requires(dummies != null);

       Contract.Requires(body != null);

       Contract.Requires(dummies.Count + typeParams.Count > 0);

     }

-    public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body)

-      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body) {

+    public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false)

+      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

-    public ForallExpr(IToken tok, List<Variable> dummies, Expr body)

-      : base(tok, new List<TypeVariable>(), dummies, null, null, body) {

+    public ForallExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable=false)

+      : base(tok, new List<TypeVariable>(), dummies, null, null, body, immutable) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

-    public ForallExpr(IToken tok, List<TypeVariable> typeParams, List<Variable> dummies, Expr body)

-      : base(tok, typeParams, dummies, null, null, body) {

+    public ForallExpr(IToken tok, List<TypeVariable> typeParams, List<Variable> dummies, Expr body, bool immutable=false)

+      : base(tok, typeParams, dummies, null, null, body, immutable) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(typeParams != null);

@@ -593,23 +593,23 @@ namespace Microsoft.Boogie {
 

   public class ExistsExpr : QuantifierExpr {

     public ExistsExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ dummies,

-                      QKeyValue kv, Trigger triggers, Expr/*!*/ body)

-      : base(tok, typeParams, dummies, kv, triggers, body) {

+                      QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false)

+      : base(tok, typeParams, dummies, kv, triggers, body, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParams != null);

       Contract.Requires(dummies != null);

       Contract.Requires(body != null);

       Contract.Requires(dummies.Count + typeParams.Count > 0);

     }

-    public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body)

-      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body) {

+    public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false)

+      : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

       Contract.Requires(dummies.Count > 0);

     }

-    public ExistsExpr(IToken tok, List<Variable> dummies, Expr body)

-      : base(tok, new List<TypeVariable>(), dummies, null, null, body) {

+    public ExistsExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable=false)

+      : base(tok, new List<TypeVariable>(), dummies, null, null, body, immutable) {

       Contract.Requires(body != null);

       Contract.Requires(dummies != null);

       Contract.Requires(tok != null);

@@ -640,8 +640,8 @@ namespace Microsoft.Boogie {
     public readonly int SkolemId;

 

     public QuantifierExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,

-                          List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)

-      : base(tok, typeParameters, dummies, kv, body) {

+                          List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable)

+      : base(tok, typeParameters, dummies, kv, body, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParameters != null);

       Contract.Requires(dummies != null);

@@ -844,8 +844,8 @@ namespace Microsoft.Boogie {
 

   public class LambdaExpr : BinderExpr {

     public LambdaExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,

-                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)

-      : base(tok, typeParameters, dummies, kv, body) {

+                      List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable=false)

+      : base(tok, typeParameters, dummies, kv, body, immutable) {

       Contract.Requires(tok != null);

       Contract.Requires(typeParameters != null);

       Contract.Requires(dummies != null);

diff --git a/Source/UnitTests/CoreTests/ExprImmutability.cs b/Source/UnitTests/CoreTests/ExprImmutability.cs
index aff0acea..f3225b0f 100644
--- a/Source/UnitTests/CoreTests/ExprImmutability.cs
+++ b/Source/UnitTests/CoreTests/ExprImmutability.cs
@@ -11,9 +11,46 @@ namespace CoreTests
 
         public void Error(IToken tok, string msg)
         {
-            Assert.Fail (msg);
+            Assert.Fail(msg);
         }
 
+        // Cached hashcode checkers
+        [Test()]
+        public void CachedHashCodeForAllExpr()
+        {
+            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 body = Expr.Gt (new IdentifierExpr (Token.NoToken, x, /*immutable=*/true),
+                new IdentifierExpr(Token.NoToken, y, /*immutable=*/true));
+            var forAll = new ForallExpr(Token.NoToken, new List<Variable> () {x, y }, body, /*immutable=*/ true);
+            Assert.AreEqual(forAll.ComputeHashCode(), forAll.GetHashCode());
+        }
+
+        [Test()]
+        public void CachedHashCodeExistsExpr()
+        {
+            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 body = Expr.Gt (new IdentifierExpr (Token.NoToken, x, /*immutable=*/true),
+                new IdentifierExpr(Token.NoToken, y, /*immutable=*/true));
+            var exists = new ExistsExpr(Token.NoToken, new List<Variable> () {x, y }, body, /*immutable=*/ true);
+            Assert.AreEqual(exists.ComputeHashCode(), exists.GetHashCode());
+        }
+
+        [Test()]
+        public void CachedHashCodeLambdaExpr()
+        {
+            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 body = Expr.Gt (new IdentifierExpr (Token.NoToken, x, /*immutable=*/true),
+                new IdentifierExpr(Token.NoToken, y, /*immutable=*/true));
+            var lambda = new LambdaExpr(Token.NoToken, new List<TypeVariable>(), new List<Variable>() { x, y},
+                null, body, /*immutable=*/true);
+            Assert.AreEqual(lambda.ComputeHashCode(), lambda.GetHashCode());
+        }
+
+        // Runtime immutability enforcement
+
         [Test(), ExpectedException(typeof(InvalidOperationException))]
         public void IdentifierExprName()
         {