summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/AbsyExpr.cs200
-rw-r--r--Source/Core/AbsyQuant.cs22
-rw-r--r--Source/Core/Parser.cs5
3 files changed, 188 insertions, 39 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 4a7db752..7b4900f2 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -31,9 +31,10 @@ namespace Microsoft.Boogie {
[ContractClass(typeof(ExprContracts))]
public abstract class Expr : Absy {
- public Expr(IToken/*!*/ tok)
+ public Expr(IToken/*!*/ tok, bool immutable)
: base(tok) {
Contract.Requires(tok != null);
+ this.Immutable = immutable;
}
public void Emit(TokenTextWriter stream) {
@@ -41,6 +42,32 @@ namespace Microsoft.Boogie {
Emit(stream, 0, false);
}
+ /// <summary>
+ /// If true the client is making a promise that this Expr will be
+ /// treated immutably (i.e. once constructed it is never changed).
+ /// This is currently not enforced but it should be!
+ ///
+ /// This allows the Expr's hash code to be cached making calls to
+ /// GetHashCode() very cheap.
+ /// </summary>
+ /// <value><c>true</c> if immutable; otherwise, <c>false</c>.</value>
+ public bool Immutable {
+ get;
+ private set;
+ }
+
+ /// <summary>
+ /// Computes the hash code of this Expr skipping any cache.
+ ///
+ /// Sub classes should place their implementation of computing their hashcode
+ /// here (making sure to call ComputeHashCode() and not GetHashCode() on Expr)
+ /// and have GetHashCode() use a cached result from ComputeHashCode() if the
+ /// Expr was constructed to be immutable.
+ /// </summary>
+ /// <returns>The hash code.</returns>
+ public abstract int ComputeHashCode();
+ protected int CachedHashCode = 0;
+
public abstract void Emit(TokenTextWriter/*!*/ wr, int contextBindingStrength, bool fragileContext);
[Pure]
@@ -424,7 +451,7 @@ namespace Microsoft.Boogie {
}
[ContractClassFor(typeof(Expr))]
public abstract class ExprContracts : Expr {
- public ExprContracts() :base(null){
+ public ExprContracts() :base(null, /*immutable=*/ false){
}
public override void Emit(TokenTextWriter wr, int contextBindingStrength, bool fragileContext) {
@@ -456,11 +483,13 @@ namespace Microsoft.Boogie {
/// </summary>
/// <param name="tok"></param>
/// <param name="b"></param>
- public LiteralExpr(IToken/*!*/ tok, bool b)
- : base(tok) {
+ public LiteralExpr(IToken/*!*/ tok, bool b, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Val = b;
Type = Type.Bool;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
/// <summary>
@@ -468,11 +497,13 @@ namespace Microsoft.Boogie {
/// </summary>
/// <param name="tok"></param>
/// <param name="v"></param>
- public LiteralExpr(IToken/*!*/ tok, BigNum v)
- : base(tok) {
+ public LiteralExpr(IToken/*!*/ tok, BigNum v, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Val = v;
Type = Type.Int;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
/// <summary>
@@ -480,22 +511,26 @@ namespace Microsoft.Boogie {
/// </summary>
/// <param name="tok"></param>
/// <param name="v"></param>
- public LiteralExpr(IToken/*!*/ tok, BigDec v)
- : base(tok) {
+ public LiteralExpr(IToken/*!*/ tok, BigDec v, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Val = v;
Type = Type.Real;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
/// <summary>
/// Creates a literal expression for the bitvector value "v".
/// </summary>
- public LiteralExpr(IToken/*!*/ tok, BigNum v, int b)
- : base(tok) {
+ public LiteralExpr(IToken/*!*/ tok, BigNum v, int b, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(0 <= b);
Val = new BvConst(v, b);
Type = Type.GetBvType(b);
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
[Pure]
@@ -509,10 +544,20 @@ namespace Microsoft.Boogie {
LiteralExpr other = (LiteralExpr)obj;
return object.Equals(this.Val, other.Val);
}
+
[Pure]
public override int GetHashCode() {
+ if (Immutable)
+ return this.CachedHashCode;
+ else
+ return ComputeHashCode();
+ }
+
+ [Pure]
+ public override int ComputeHashCode() {
return this.Val.GetHashCode();
}
+
public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
//Contract.Requires(stream != null);
stream.SetToken(this);
@@ -686,6 +731,7 @@ namespace Microsoft.Boogie {
}
public class IdentifierExpr : Expr {
+ // FIXME: Protect these fields
public string/*!*/ Name; // identifier symbol
public Variable Decl; // identifier declaration
[ContractInvariantMethod]
@@ -701,11 +747,13 @@ namespace Microsoft.Boogie {
/// </summary>
/// <param name="tok"></param>
/// <param name="name"></param>
- internal IdentifierExpr(IToken/*!*/ tok, string/*!*/ name)
- : base(tok) {
+ internal IdentifierExpr(IToken/*!*/ tok, string/*!*/ name, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Name = name;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
/// <summary>
/// Creates an unresolved identifier expression.
@@ -713,13 +761,15 @@ namespace Microsoft.Boogie {
/// <param name="tok"></param>
/// <param name="name"></param>
/// <param name="type"></param>
- public IdentifierExpr(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type)
- : base(tok) {
+ public IdentifierExpr(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
Name = name;
Type = type;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
/// <summary>
@@ -727,13 +777,15 @@ namespace Microsoft.Boogie {
/// </summary>
/// <param name="tok"></param>
/// <param name="d"></param>
- public IdentifierExpr(IToken/*!*/ tok, Variable/*!*/ d)
- : base(tok) {
+ public IdentifierExpr(IToken/*!*/ tok, Variable/*!*/ d, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(d != null);
Name = cce.NonNull(d.Name);
Decl = d;
Type = d.TypedIdent.Type;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
[Pure]
[Reads(ReadsAttribute.Reads.Nothing)]
@@ -746,12 +798,22 @@ namespace Microsoft.Boogie {
IdentifierExpr other = (IdentifierExpr)obj;
return object.Equals(this.Name, other.Name) && object.Equals(this.Decl, other.Decl);
}
+
[Pure]
public override int GetHashCode() {
+ if (Immutable)
+ return this.CachedHashCode;
+ else
+ return ComputeHashCode();
+ }
+
+ [Pure]
+ public override int ComputeHashCode() {
int h = this.Name == null ? 0 : this.Name.GetHashCode();
h ^= this.Decl == null ? 0 : this.Decl.GetHashCode();
return h;
}
+
public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
//Contract.Requires(stream != null);
if (CommandLineOptions.Clo.PrintWithUniqueASTIds && !stream.UseForComputingChecksums) {
@@ -848,17 +910,20 @@ namespace Microsoft.Boogie {
public class OldExpr : Expr
{
+ // FIXME: protect this field
public Expr/*!*/ Expr;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Expr != null);
}
- public OldExpr(IToken/*!*/ tok, Expr/*!*/ expr)
- : base(tok) {
+ public OldExpr(IToken/*!*/ tok, Expr/*!*/ expr, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
Expr = expr;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
[Pure]
[Reads(ReadsAttribute.Reads.Nothing)]
@@ -873,8 +938,16 @@ namespace Microsoft.Boogie {
}
[Pure]
public override int GetHashCode() {
- return this.Expr == null ? 0 : this.Expr.GetHashCode();
+ if (Immutable)
+ return this.CachedHashCode;
+ else
+ return ComputeHashCode ();
+ }
+ public override int ComputeHashCode() {
+ // FIXME: This is wrong, it's as if the OldExpr node isn't there at all
+ return this.Expr == null ? 0 : this.Expr.ComputeHashCode();
}
+
public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
//Contract.Requires(stream != null);
stream.Write(this, "old(");
@@ -2110,8 +2183,10 @@ namespace Microsoft.Boogie {
public class NAryExpr : Expr {
[Additive]
[Peer]
+ // FIXME: Protect these fields
public IAppliable/*!*/ Fun;
- public List<Expr>/*!*/ Args;
+ public List<Expr> Args;
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Fun != null);
@@ -2124,14 +2199,16 @@ namespace Microsoft.Boogie {
public TypeParamInstantiation TypeParameters = null;
[Captured]
- public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, List<Expr>/*!*/ args)
- : base(tok) {
+ public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, List<Expr>/*!*/ args, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(fun != null);
Contract.Requires(args != null);
Fun = fun;
Args = args;
Contract.Assert(Contract.ForAll(0, args.Count, index => args[index] != null));
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
[Pure]
[Reads(ReadsAttribute.Reads.Nothing)]
@@ -2144,13 +2221,22 @@ namespace Microsoft.Boogie {
NAryExpr other = (NAryExpr)obj;
return object.Equals(this.Fun, other.Fun) && this.Args.SequenceEqual(other.Args);
}
+
[Pure]
public override int GetHashCode() {
+ if (Immutable)
+ return this.CachedHashCode;
+ else
+ return ComputeHashCode();
+ }
+
+ [Pure]
+ public override int ComputeHashCode() {
int h = this.Fun.GetHashCode();
// DO NOT USE Args.GetHashCode() because that uses Object.GetHashCode() which uses references
// We want structural equality
foreach (var arg in Args) {
- h = (97*h) + arg.GetHashCode();
+ h = (97*h) + arg.ComputeHashCode();
}
return h;
}
@@ -2658,15 +2744,39 @@ namespace Microsoft.Boogie {
Contract.Invariant(cce.NonNullElements(Blocks));
}
- public CodeExpr(List<Variable>/*!*/ localVariables, List<Block/*!*/>/*!*/ blocks)
- : base(Token.NoToken) {
+ public CodeExpr(List<Variable>/*!*/ localVariables, List<Block/*!*/>/*!*/ blocks, bool immutable=false)
+ : base(Token.NoToken, immutable) {
Contract.Requires(localVariables != null);
Contract.Requires(cce.NonNullElements(blocks));
Contract.Requires(0 < blocks.Count);
LocVars = localVariables;
Blocks = blocks;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
+ }
+
+ // FIXME: This seems wrong we don't want reference equality, we want structural equality
+ [Pure]
+ public override bool Equals(object obj)
+ {
+ return base.Equals(obj);
+ }
+
+ [Pure]
+ public override int GetHashCode()
+ {
+ if (Immutable)
+ return CachedHashCode;
+ else
+ return ComputeHashCode();
+ }
+
+ [Pure]
+ public override int ComputeHashCode() {
+ return base.GetHashCode();
}
+
public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
//Contract.Requires(freeVars != null);
// Treat a BlockEexpr as if it has no free variables at all
@@ -2748,6 +2858,7 @@ namespace Microsoft.Boogie {
}
public class BvExtractExpr : Expr {
+ // FIXME: Protect these fields
public /*readonly--except in StandardVisitor*/ Expr/*!*/ Bitvector;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -2756,13 +2867,15 @@ namespace Microsoft.Boogie {
public readonly int Start, End;
- public BvExtractExpr(IToken/*!*/ tok, Expr/*!*/ bv, int end, int start)
- : base(tok) {
+ public BvExtractExpr(IToken/*!*/ tok, Expr/*!*/ bv, int end, int start, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(bv != null);
Bitvector = bv;
Start = start;
End = end;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
[Pure]
@@ -2777,9 +2890,18 @@ namespace Microsoft.Boogie {
return object.Equals(this.Bitvector, other.Bitvector) &&
this.Start.Equals(other.Start) && this.End.Equals(other.End);
}
+
[Pure]
public override int GetHashCode() {
- int h = this.Bitvector.GetHashCode();
+ if (Immutable)
+ return CachedHashCode;
+ else
+ return ComputeHashCode();
+ }
+
+ [Pure]
+ public override int ComputeHashCode() {
+ int h = this.Bitvector.ComputeHashCode();
h ^= Start * 17 ^ End * 13;
return h;
}
@@ -2847,6 +2969,7 @@ namespace Microsoft.Boogie {
}
public class BvConcatExpr : Expr {
+ // FIXME: Protect these fields
public /*readonly--except in StandardVisitor*/ Expr/*!*/ E0, E1;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -2855,13 +2978,15 @@ namespace Microsoft.Boogie {
}
- public BvConcatExpr(IToken/*!*/ tok, Expr/*!*/ e0, Expr/*!*/ e1)
- : base(tok) {
+ public BvConcatExpr(IToken/*!*/ tok, Expr/*!*/ e0, Expr/*!*/ e1, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(e0 != null);
Contract.Requires(e1 != null);
E0 = e0;
E1 = e1;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
[Pure]
@@ -2875,11 +3000,22 @@ namespace Microsoft.Boogie {
BvConcatExpr other = (BvConcatExpr)obj;
return object.Equals(this.E0, other.E0) && object.Equals(this.E1, other.E1);
}
+
[Pure]
- public override int GetHashCode() {
- int h = this.E0.GetHashCode() ^ this.E1.GetHashCode() * 17;
+ public override int GetHashCode()
+ {
+ if (Immutable)
+ return CachedHashCode;
+ else
+ return ComputeHashCode();
+ }
+
+ [Pure]
+ public override int ComputeHashCode() {
+ int h = this.E0.ComputeHashCode() ^ this.E1.ComputeHashCode() * 17;
return h;
}
+
public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
//Contract.Requires(stream != null);
stream.SetToken(this);
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 86338d30..f7665a07 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -58,9 +58,8 @@ namespace Microsoft.Boogie {
}
public BinderExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
- List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)
- : base(tok)
- {
+ List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable=false)
+ : base(tok, immutable) {
Contract.Requires(tok != null);
Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
@@ -70,6 +69,8 @@ namespace Microsoft.Boogie {
Dummies = dummies;
Attributes = kv;
Body = body;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
}
abstract public BinderKind Kind {
@@ -110,9 +111,18 @@ namespace Microsoft.Boogie {
}
[Pure]
- public override int GetHashCode() {
+ public override int GetHashCode()
+ {
+ if (Immutable)
+ return CachedHashCode;
+ else
+ return ComputeHashCode();
+ }
+
+ [Pure]
+ public override int ComputeHashCode() {
// Note, we don't hash triggers and attributes
-
+
// DO NOT USE Dummies.GetHashCode() because we want structurally
// identical Expr to have the same hash code **not** identical references
// to have the same hash code.
@@ -121,7 +131,7 @@ namespace Microsoft.Boogie {
h = ( 53 * h ) + dummyVar.GetHashCode();
}
- h ^= this.Body.GetHashCode();
+ h ^= this.Body.ComputeHashCode();
// DO NOT USE TypeParameters.GetHashCode() because we want structural
// identical Expr to have the same hash code **not** identical references
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 25be7f27..9a0bab51 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -117,7 +117,7 @@ private class BvBounds : Expr {
public BigNum Lower;
public BigNum Upper;
public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper)
- : base(tok) {
+ : base(tok, /*immutable=*/ false) {
Contract.Requires(tok != null);
this.Lower = lower;
this.Upper = upper;
@@ -132,6 +132,9 @@ private class BvBounds : Expr {
Contract.Assert(false);throw new cce.UnreachableException();
}
public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) { Contract.Assert(false);throw new cce.UnreachableException(); }
+ public override int ComputeHashCode() {
+ return base.GetHashCode();
+ }
}
/*--------------------------------------------------------------------------*/
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 08:24:59 +0000