From cbeac20670125179246c253777f33aad943f8176 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 29 Jan 2015 08:53:44 +0000 Subject: Fix ForAllExpr, ExistsExpr and LambdaExpr constructors so it is possible to set them as immutable (not currently enforced for these Expr types). --- Source/Core/AbsyQuant.cs | 40 +++++++++++++------------- Source/UnitTests/CoreTests/ExprImmutability.cs | 39 ++++++++++++++++++++++++- 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/*!*/ typeParameters, - List/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable=false) + List/*!*/ 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/*!*/ typeParams, - List/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body) - : base(tok, typeParams, dummies, kv, triggers, body) { + List/*!*/ 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 dummies, Trigger triggers, Expr body) - : base(tok, new List(), dummies, null, triggers, body) { + public ForallExpr(IToken tok, List dummies, Trigger triggers, Expr body, bool immutable=false) + : base(tok, new List(), 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 dummies, Expr body) - : base(tok, new List(), dummies, null, null, body) { + public ForallExpr(IToken tok, List dummies, Expr body, bool immutable=false) + : base(tok, new List(), 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 typeParams, List dummies, Expr body) - : base(tok, typeParams, dummies, null, null, body) { + public ForallExpr(IToken tok, List typeParams, List 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/*!*/ typeParams, List/*!*/ 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 dummies, Trigger triggers, Expr body) - : base(tok, new List(), dummies, null, triggers, body) { + public ExistsExpr(IToken tok, List dummies, Trigger triggers, Expr body, bool immutable=false) + : base(tok, new List(), 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 dummies, Expr body) - : base(tok, new List(), dummies, null, null, body) { + public ExistsExpr(IToken tok, List dummies, Expr body, bool immutable=false) + : base(tok, new List(), 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/*!*/ typeParameters, - List/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body) - : base(tok, typeParameters, dummies, kv, body) { + List/*!*/ 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/*!*/ typeParameters, - List/*!*/ dummies, QKeyValue kv, Expr/*!*/ body) - : base(tok, typeParameters, dummies, kv, body) { + List/*!*/ 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 () {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 () {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(), new List() { x, y}, + null, body, /*immutable=*/true); + Assert.AreEqual(lambda.ComputeHashCode(), lambda.GetHashCode()); + } + + // Runtime immutability enforcement + [Test(), ExpectedException(typeof(InvalidOperationException))] public void IdentifierExprName() { -- cgit v1.2.3