summaryrefslogtreecommitdiff
path: root/Source/Core/AbsyQuant.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/AbsyQuant.cs')
-rw-r--r--Source/Core/AbsyQuant.cs1883
1 files changed, 953 insertions, 930 deletions
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 2258e553..3a27eddf 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -1,930 +1,953 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-//---------------------------------------------------------------------------------------------
-// BoogiePL - AbsyQuant.cs
-//---------------------------------------------------------------------------------------------
-
-namespace Microsoft.Boogie {
- using System;
- using System.Collections;
- using System.Diagnostics;
- using System.Collections.Generic;
- using System.Linq;
- using Microsoft.Boogie.AbstractInterpretation;
- using System.Diagnostics.Contracts;
- using Microsoft.Basetypes;
-
- using Set = GSet<object>;
-
- //---------------------------------------------------------------------
- // Quantifiers and general binders
- //---------------------------------------------------------------------
-
- public enum BinderKind {
- Forall,
- Exists,
- Lambda
- }
- [ContractClassFor(typeof(BinderExpr))]
- abstract class BinderExprContracts : BinderExpr {
- public override BinderKind Kind {
- get {
- throw new NotImplementedException();
- }
- }
- public BinderExprContracts():base(null,null,null,null,null,false){
- }
-
- public override Type ShallowType {
- get {
- throw new NotImplementedException();
- }
- }
- }
- [ContractClass(typeof(BinderExprContracts))]
- public abstract class BinderExpr : Expr {
- public List<TypeVariable>/*!*/ TypeParameters;
- public List<Variable>/*!*/ Dummies;
- public QKeyValue Attributes;
- // 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);
- Contract.Invariant(Dummies != null);
- Contract.Invariant(Body != null);
- }
-
- public BinderExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
- List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable)
- : base(tok, immutable) {
- Contract.Requires(tok != null);
- Contract.Requires(typeParameters != null);
- Contract.Requires(dummies != null);
- Contract.Requires(body != null);
- Contract.Requires(dummies.Count + typeParameters.Count > 0);
- TypeParameters = typeParameters;
- Dummies = dummies;
- Attributes = kv;
- _Body = body;
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- abstract public BinderKind Kind {
- get;
- }
-
- protected static bool CompareAttributesAndTriggers = false;
-
- public static bool EqualWithAttributesAndTriggers(object a, object b) {
- CompareAttributesAndTriggers = true;
- var res = object.Equals(a, b);
- Contract.Assert(CompareAttributesAndTriggers);
- CompareAttributesAndTriggers = false;
- return res;
- }
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- return BinderEquals(obj);
- }
-
- public bool BinderEquals(object obj) {
- if (obj == null) {
- return false;
- }
- if (!(obj is BinderExpr) ||
- this.Kind != ((BinderExpr) obj).Kind) {
- return false;
- }
-
- var other = (BinderExpr) obj;
-
- return this.TypeParameters.SequenceEqual(other.TypeParameters)
- && this.Dummies.SequenceEqual(other.Dummies)
- && (!CompareAttributesAndTriggers || object.Equals(this.Attributes, other.Attributes))
- && object.Equals(this.Body, other.Body);
- }
-
- [Pure]
- 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.
- int h = 0;
- foreach (var dummyVar in this.Dummies) {
- h = ( 53 * h ) + dummyVar.GetHashCode();
- }
-
- h ^= this.Body.GetHashCode();
-
- // DO NOT USE TypeParameters.GetHashCode() because we want structural
- // identical Expr to have the same hash code **not** identical references
- // to have the same hash code.
- int h2 = 0;
- foreach (var typeParam in this.TypeParameters) {
- h2 = ( 97 * h2 ) + typeParam.GetHashCode();
- }
-
- h = h * 5 + h2;
- h *= ((int)Kind + 1);
- return h;
- }
-
- protected virtual void EmitTypeHint(TokenTextWriter stream) {
- Contract.Requires(stream != null);
- }
-
- protected virtual void EmitTriggers(TokenTextWriter stream) {
- Contract.Requires(stream != null);
- }
-
- public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
- //Contract.Requires(stream != null);
- stream.push();
- stream.Write(this, "({0}", Kind.ToString().ToLower());
- this.EmitTypeHint(stream);
- Type.EmitOptionalTypeParams(stream, TypeParameters);
- stream.Write(this, " ");
- this.Dummies.Emit(stream, true);
- stream.Write(" :: ");
- stream.sep();
- for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
- kv.Emit(stream);
- stream.Write(" ");
- }
- this.EmitTriggers(stream);
- stream.sep();
-
- this.Body.Emit(stream);
- stream.Write(")");
- stream.pop();
- }
-
- protected virtual void ResolveTriggers(ResolutionContext rc) {
- Contract.Requires(rc != null);
- }
-
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- if (rc.TriggerMode) {
- rc.Error(this, "quantifiers are not allowed in triggers");
- }
-
- int previousTypeBinderState = rc.TypeBinderState;
- try {
- foreach (TypeVariable/*!*/ v in TypeParameters) {
- Contract.Assert(v != null);
- rc.AddTypeBinder(v);
- }
-
- rc.PushVarContext();
- foreach (Variable/*!*/ v in Dummies) {
- Contract.Assert(v != null);
- v.Register(rc);
- v.Resolve(rc);
- }
- for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
- kv.Resolve(rc);
- }
- this.ResolveTriggers(rc);
- Body.Resolve(rc);
- rc.PopVarContext();
-
- // establish a canonical order of the type parameters
- this.TypeParameters = Type.SortTypeParams(TypeParameters, new List<Type>(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()), null);
-
- } finally {
- rc.TypeBinderState = previousTypeBinderState;
- }
- }
-
- public override void ComputeFreeVariables(Set freeVars) {
- //Contract.Requires(freeVars != null);
- ComputeBinderFreeVariables(TypeParameters, Dummies, Body, Attributes, freeVars);
- }
-
- public static void ComputeBinderFreeVariables(List<TypeVariable> typeParameters, List<Variable> dummies, Expr body, QKeyValue attributes, Set freeVars) {
- Contract.Requires(dummies != null);
- Contract.Requires(body != null);
-
- foreach (var v in dummies) {
- Contract.Assert(v != null);
- Contract.Assert(!freeVars[v]);
- }
- body.ComputeFreeVariables(freeVars);
- for (var a = attributes; a != null; a = a.Next) {
- foreach (var o in a.Params) {
- var e = o as Expr;
- if (e != null) {
- e.ComputeFreeVariables(freeVars);
- }
- }
- }
- foreach (var v in dummies) {
- freeVars.AddRange(v.TypedIdent.Type.FreeVariables);
- }
- freeVars.RemoveRange(dummies);
- freeVars.RemoveRange(typeParameters);
- }
-
- protected List<TypeVariable> GetUnmentionedTypeParameters() {
- Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);
- List<TypeVariable>/*!*/ dummyParameters = Type.FreeVariablesIn(new List<Type>(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()));
- Contract.Assert(dummyParameters != null);
- List<TypeVariable>/*!*/ unmentionedParameters = new List<TypeVariable>();
- foreach (TypeVariable/*!*/ var in TypeParameters) {
- Contract.Assert(var != null);
- if (!dummyParameters.Contains(var))
- unmentionedParameters.Add(var);
- }
- return unmentionedParameters;
- }
- }
-
- public class QKeyValue : Absy {
- public readonly string/*!*/ Key;
- private readonly List<object/*!*/>/*!*/ _params; // each element is either a string or an Expr
-
- public void AddParam(object p)
- {
- Contract.Requires(p != null);
- this._params.Add(p);
- }
-
- public void AddParams(IEnumerable<object> ps)
- {
- Contract.Requires(cce.NonNullElements(ps));
- this._params.AddRange(ps);
- }
-
- public void ClearParams()
- {
- this._params.Clear();
- }
-
- public IList<object> Params
- {
- get
- {
- Contract.Ensures(cce.NonNullElements(Contract.Result<IList<object>>()));
- Contract.Ensures(Contract.Result<IList<object>>().IsReadOnly);
- return this._params.AsReadOnly();
- }
- }
-
- public QKeyValue Next;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Key != null);
- Contract.Invariant(cce.NonNullElements(this._params));
- }
-
- public QKeyValue(IToken tok, string key, IList<object/*!*/>/*!*/ parameters, QKeyValue next)
- : base(tok) {
- Contract.Requires(key != null);
- Contract.Requires(tok != null);
- Contract.Requires(cce.NonNullElements(parameters));
- Key = key;
- this._params = new List<object>(parameters);
- Next = next;
- }
-
- public void Emit(TokenTextWriter stream) {
- Contract.Requires(stream != null);
- stream.Write("{:");
- stream.Write(Key);
- string sep = " ";
- foreach (object p in Params) {
- stream.Write(sep);
- sep = ", ";
- if (p is string) {
- stream.Write("\"");
- stream.Write((string)p);
- stream.Write("\"");
- } else {
- ((Expr)p).Emit(stream);
- }
- }
- stream.Write("}");
- }
-
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- foreach (object p in Params) {
- if (p is Expr) {
- ((Expr)p).Resolve(rc);
- }
- }
- }
-
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- foreach (object p in Params) {
- if (p is Expr) {
- ((Expr)p).Typecheck(tc);
- }
- }
- }
- public void AddLast(QKeyValue other) {
- Contract.Requires(other != null);
- QKeyValue current = this;
- while (current.Next != null) {
- current = current.Next;
- }
- current.Next = other;
- }
- // Look for {:name string} in list of attributes.
- [Pure]
- public static string FindStringAttribute(QKeyValue kv, string name) {
- Contract.Requires(name != null);
- for (; kv != null; kv = kv.Next) {
- if (kv.Key == name) {
- if (kv.Params.Count == 1 && kv.Params[0] is string) {
- return (string)kv.Params[0];
- }
- }
- }
- return null;
- }
- // Look for {:name expr} in list of attributes.
- public static Expr FindExprAttribute(QKeyValue kv, string name) {
- Contract.Requires(name != null);
- for (; kv != null; kv = kv.Next) {
- if (kv.Key == name) {
- if (kv.Params.Count == 1 && kv.Params[0] is Expr) {
- return (Expr)kv.Params[0];
- }
- }
- }
- return null;
- }
- // Return 'true' if {:name true} or {:name} is an attribute in 'kv'
- public static bool FindBoolAttribute(QKeyValue kv, string name) {
- Contract.Requires(name != null);
- for (; kv != null; kv = kv.Next) {
- if (kv.Key == name) {
- return kv.Params.Count == 0 ||
- (kv.Params.Count == 1 && kv.Params[0] is LiteralExpr && ((LiteralExpr)kv.Params[0]).IsTrue);
- }
- }
- return false;
- }
-
- public static int FindIntAttribute(QKeyValue kv, string name, int defl) {
- Contract.Requires(name != null);
- Expr e = FindExprAttribute(kv, name);
- LiteralExpr l = e as LiteralExpr;
- if (l != null && l.isBigNum)
- return l.asBigNum.ToIntSafe;
- return defl;
- }
-
- public override Absy Clone() {
- List<object> newParams = new List<object>();
- foreach (object o in Params)
- newParams.Add(o);
- return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue)Next.Clone());
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- return visitor.VisitQKeyValue(this);
- }
-
- public override bool Equals(object obj) {
- var other = obj as QKeyValue;
- if (other == null) {
- return false;
- } else {
- return Key == other.Key && object.Equals(Params, other.Params) &&
- (Next == null
- ? other.Next == null
- : object.Equals(Next, other.Next));
- }
- }
-
- public override int GetHashCode() {
- throw new NotImplementedException();
- }
- }
-
- public class Trigger : Absy {
- public readonly bool Pos;
- [Rep]
- private List<Expr>/*!*/ tr;
-
- public IList<Expr>/*!*/ Tr
- {
- get
- {
- Contract.Ensures(Contract.Result<IList<Expr>>() != null);
- Contract.Ensures(Contract.Result<IList<Expr>>().Count >= 1);
- Contract.Ensures(this.Pos || Contract.Result<IList<Expr>>().Count == 1);
- return this.tr.AsReadOnly();
- }
- set
- {
- Contract.Requires(value != null);
- Contract.Requires(value.Count >= 1);
- Contract.Requires(this.Pos || value.Count == 1);
- this.tr = new List<Expr>(value);
- }
- }
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(this.tr != null);
- Contract.Invariant(this.tr.Count >= 1);
- Contract.Invariant(Pos || this.tr.Count == 1);
- }
-
- public Trigger Next;
-
- public Trigger(IToken/*!*/ tok, bool pos, IEnumerable<Expr>/*!*/ tr, Trigger next = null)
- : base(tok) {
- Contract.Requires(tok != null);
- Contract.Requires(tr != null);
- Contract.Requires(tr.Count() >= 1);
- Contract.Requires(pos || tr.Count() == 1);
- this.Pos = pos;
- this.Tr = new List<Expr>(tr);
- this.Next = next;
- }
-
- public void Emit(TokenTextWriter stream) {
- Contract.Requires(stream != null);
- stream.SetToken(this);
- Contract.Assert(this.Tr.Count >= 1);
- string/*!*/ sep = Pos ? "{ " : "{:nopats ";
- foreach (Expr/*!*/ e in this.Tr) {
- Contract.Assert(e != null);
- stream.Write(sep);
- sep = ", ";
- e.Emit(stream);
- }
- stream.Write(" }");
- }
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- rc.TriggerMode = true;
- foreach (Expr/*!*/ e in this.Tr) {
- Contract.Assert(e != null);
- e.Resolve(rc);
-
- // just a variable by itself is not allowed
- if (e is IdentifierExpr) {
- rc.Error(e, "a matching pattern must be more than just a variable by itself: {0}", e);
- }
-
- // the free-variable check is performed in the surrounding quantifier expression (because that's
- // where the bound variables are known)
- }
- rc.TriggerMode = false;
- }
-
- /// <summary>
- /// Add to "freeVars" the free variables in the triggering expressions.
- /// </summary>
- public void ComputeFreeVariables(Set /*Variable*/ freeVars) {
- Contract.Requires(freeVars != null);
- foreach (Expr/*!*/ e in this.Tr) {
- Contract.Assert(e != null);
- e.ComputeFreeVariables(freeVars);
- }
- }
-
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- foreach (Expr/*!*/ e in this.Tr) {
- Contract.Assert(e != null);
- e.Typecheck(tc);
- }
- }
-
- public void AddLast(Trigger other) {
- Trigger current = this;
- while (current.Next != null) {
- current = current.Next;
- }
- current.Next = other;
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitTrigger(this);
- }
-
- public override bool Equals(object obj) {
- var other = obj as Trigger;
- if (other == null) {
- return false;
- } else {
- return this.Tr.SequenceEqual(other.Tr) &&
- (Next == null ? other.Next == null : object.Equals(Next, other.Next));
- }
- }
-
- public override int GetHashCode() {
- throw new NotImplementedException();
- }
- }
-
- public class ForallExpr : QuantifierExpr {
- public ForallExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams,
- 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, 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, 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, bool immutable=false)
- : base(tok, typeParams, dummies, null, null, body, immutable) {
- Contract.Requires(body != null);
- Contract.Requires(dummies != null);
- Contract.Requires(typeParams != null);
- Contract.Requires(tok != null);
- Contract.Requires(dummies.Count + typeParams.Count > 0);
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitForallExpr(this);
- }
-
- public override BinderKind Kind {
- get {
- return BinderKind.Forall;
- }
- }
- }
-
- public class ExistsExpr : QuantifierExpr {
- public ExistsExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams, 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 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, 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 override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitExistsExpr(this);
- }
-
- public override BinderKind Kind {
- get {
- return BinderKind.Exists;
- }
- }
- }
-
- public abstract class QuantifierExpr : BinderExpr {
- public Trigger Triggers;
-
- static int SkolemIds = -1;
- public static int GetNextSkolemId() {
- return System.Threading.Interlocked.Increment(ref SkolemIds);
- }
-
- public readonly int SkolemId;
-
- public QuantifierExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
- 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);
- Contract.Requires(body != null);
- Contract.Requires(dummies.Count + typeParameters.Count > 0);
-
- Contract.Assert((this is ForallExpr) || (this is ExistsExpr));
-
- Triggers = triggers;
- SkolemId = GetNextSkolemId();
- }
-
- protected override void EmitTriggers(TokenTextWriter stream) {
- //Contract.Requires(stream != null);
- stream.push();
- for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
- tr.Emit(stream);
- stream.Write(" ");
- stream.sep();
- }
- stream.pop();
- }
-
- // if the user says ( forall x :: forall y :: ... ) and specifies *no* triggers, we transform it to
- // (forall x, y :: ... ) which may help the prover to pick trigger terms
- //
- // (Note: there used to be a different criterion here, which allowed merging when triggers were specified, which could cause prover errors due to resulting unbound variables in the triggers)
- private void MergeAdjecentQuantifier() {
- QuantifierExpr qbody = Body as QuantifierExpr;
- if (!(qbody != null && (qbody is ForallExpr) == (this is ForallExpr) && Triggers == null)) {
- return;
- }
- qbody.MergeAdjecentQuantifier();
- if (this.Triggers != null || qbody.Triggers != null) {
- return;
- }
- Body = qbody.Body;
- TypeParameters.AddRange(qbody.TypeParameters);
- Dummies.AddRange(qbody.Dummies);
- Triggers = qbody.Triggers;
- if (qbody.Attributes != null) {
- if (Attributes == null) {
- Attributes = qbody.Attributes;
- } else {
- QKeyValue p = Attributes;
- while (p.Next != null) {
- p = p.Next;
- }
- p.Next = qbody.Attributes;
- }
- }
- }
-
- #region never triggers
- private class NeverTriggerCollector : ReadOnlyVisitor {
- QuantifierExpr/*!*/ parent;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(parent != null);
- }
-
- public NeverTriggerCollector(QuantifierExpr p) {
- Contract.Requires(p != null);
- parent = p;
- }
-
- public override Expr VisitNAryExpr(NAryExpr node) {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<Expr>() != null);
- FunctionCall fn = node.Fun as FunctionCall;
- if (fn != null && cce.NonNull(fn.Func).NeverTrigger) {
- parent.Triggers = new Trigger(fn.Func.tok, false, new List<Expr> { node} , parent.Triggers);
- }
- return base.VisitNAryExpr(node);
- }
- public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) {
- // don't go into quantifier expression or its triggers, since the terms in there may have more bound variables
- // (note, with only the VisitBinderExpr override below, we'd still be visiting triggers, which we don't want to do)
- return node;
- }
- public override BinderExpr VisitBinderExpr(BinderExpr node) {
- // don't go into binder expression, since the terms in there may have more bound variables
- return node;
- }
- }
-
- private bool neverTriggerApplied;
- private void ApplyNeverTriggers() {
- if (neverTriggerApplied) {
- return;
- }
- neverTriggerApplied = true;
-
- for (Trigger t = Triggers; t != null; t = t.Next) {
- if (t.Pos) {
- return;
- }
- }
-
- NeverTriggerCollector visitor = new NeverTriggerCollector(this);
- visitor.VisitExpr(Body);
- }
- #endregion
-
- protected override void ResolveTriggers(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
- int prevErrorCount = rc.ErrorCount;
- tr.Resolve(rc);
- if (prevErrorCount == rc.ErrorCount) {
- // for positive triggers, make sure all bound variables are mentioned
- if (tr.Pos) {
- Set /*Variable*/ freeVars = new Set /*Variable*/ ();
- tr.ComputeFreeVariables(freeVars);
- foreach (Variable/*!*/ v in Dummies) {
- Contract.Assert(v != null);
- if (!freeVars[v]) {
- rc.Error(tr, "trigger must mention all quantified variables, but does not mention: {0}", v);
- }
- }
- }
- }
- }
- }
-
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- int oldErrorCount = rc.ErrorCount;
-
- this.MergeAdjecentQuantifier();
-
- base.Resolve(rc);
-
- if (oldErrorCount == rc.ErrorCount) {
- this.ApplyNeverTriggers();
- }
- }
-
-
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
- kv.Typecheck(tc);
- }
- for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
- tr.Typecheck(tc);
- }
- Body.Typecheck(tc);
- Contract.Assert(Body.Type != null); // follows from postcondition of Expr.Typecheck
- if (!Body.Type.Unify(Type.Bool)) {
- tc.Error(this, "quantifier body must be of type bool");
- }
- this.Type = Type.Bool;
-
- // Check that type parameters occur in the types of the
- // dummies, or otherwise in the triggers. This can only be
- // done after typechecking
- List<TypeVariable>/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();
- Contract.Assert(unmentionedParameters != null);
-
- if (unmentionedParameters.Count > 0) {
- // all the type parameters that do not occur in dummy types
- // have to occur in triggers
-
- for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
- // for positive triggers, make sure all bound variables are mentioned
- if (tr.Pos) {
- Set /*Variable*/ freeVars = new Set /*Variable*/ ();
- tr.ComputeFreeVariables(freeVars);
- foreach (TypeVariable/*!*/ v in unmentionedParameters) {
- Contract.Assert(v != null);
- if (!freeVars[v])
- tc.Error(tr,
- "trigger does not mention {0}, which does not occur in variables types either",
- v);
- }
- }
- }
- }
- }
- public override Type/*!*/ ShallowType {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- return Type.Bool;
- }
- }
-
- public override bool Equals(object obj) {
- var other = obj as QuantifierExpr;
- if (other == null) {
- return false;
- } else {
- return this.BinderEquals(obj) &&
- (!CompareAttributesAndTriggers || object.Equals(Triggers, other.Triggers));
- }
- }
- }
-
-
- public class LambdaExpr : BinderExpr {
- public LambdaExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
- 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);
- Contract.Requires(body != null);
- Contract.Requires(dummies.Count + typeParameters.Count > 0);
- }
-
- public override BinderKind Kind {
- get {
- return BinderKind.Lambda;
- }
- }
-
- public override void Resolve(ResolutionContext rc) {
- //Contract.Requires(rc != null);
- base.Resolve(rc);
- }
-
- public override void Typecheck(TypecheckingContext tc) {
- //Contract.Requires(tc != null);
- for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
- kv.Typecheck(tc);
- }
- Body.Typecheck(tc);
- Contract.Assert(Body.Type != null); // follows from postcondition of Expr.Typecheck
-
- List<Type>/*!*/ argTypes = new List<Type>();
- foreach (Variable/*!*/ v in Dummies) {
- Contract.Assert(v != null);
- argTypes.Add(v.TypedIdent.Type);
- }
- this.Type = new MapType(this.tok, this.TypeParameters, argTypes, Body.Type);
-
- // Check that type parameters occur in the types of the
- // dummies, or otherwise in the triggers. This can only be
- // done after typechecking
- List<TypeVariable>/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();
- Contract.Assert(unmentionedParameters != null);
-
- if (unmentionedParameters.Count > 0) {
- tc.Error(this, "the type variable {0} does not occur in types of the lambda parameters", unmentionedParameters[0]);
- }
- }
-
- private Type mapType;
- public override Type/*!*/ ShallowType {
- get {
- Contract.Ensures(Contract.Result<Type>() != null);
-
- if (mapType == null) {
- List<Type>/*!*/ argTypes = new List<Type>();
- foreach (Variable/*!*/ v in Dummies) {
- Contract.Assert(v != null);
- argTypes.Add(v.TypedIdent.Type);
- }
- mapType = new MapType(this.tok, this.TypeParameters, argTypes, Body.ShallowType);
- }
-
- return mapType;
- }
- }
-
- public override Absy StdDispatch(StandardVisitor visitor) {
- //Contract.Requires(visitor != null);
- Contract.Ensures(Contract.Result<Absy>() != null);
- return visitor.VisitLambdaExpr(this);
- }
-
- }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+//---------------------------------------------------------------------------------------------
+// BoogiePL - AbsyQuant.cs
+//---------------------------------------------------------------------------------------------
+
+namespace Microsoft.Boogie {
+ using System;
+ using System.Collections;
+ using System.Diagnostics;
+ using System.Collections.Generic;
+ using System.Linq;
+ using Microsoft.Boogie.AbstractInterpretation;
+ using System.Diagnostics.Contracts;
+ using Microsoft.Basetypes;
+
+ using Set = GSet<object>;
+
+ //---------------------------------------------------------------------
+ // Quantifiers and general binders
+ //---------------------------------------------------------------------
+
+ public enum BinderKind {
+ Forall,
+ Exists,
+ Lambda
+ }
+ [ContractClassFor(typeof(BinderExpr))]
+ abstract class BinderExprContracts : BinderExpr {
+ public override BinderKind Kind {
+ get {
+ throw new NotImplementedException();
+ }
+ }
+ public BinderExprContracts():base(null,null,null,null,null,false){
+ }
+
+ public override Type ShallowType {
+ get {
+ throw new NotImplementedException();
+ }
+ }
+ }
+ [ContractClass(typeof(BinderExprContracts))]
+ public abstract class BinderExpr : Expr {
+ public List<TypeVariable>/*!*/ TypeParameters;
+ public List<Variable>/*!*/ Dummies;
+ public QKeyValue Attributes;
+ // 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);
+ Contract.Invariant(Dummies != null);
+ Contract.Invariant(Body != null);
+ }
+
+ public BinderExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
+ List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable)
+ : base(tok, immutable) {
+ Contract.Requires(tok != null);
+ Contract.Requires(typeParameters != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(body != null);
+ Contract.Requires(dummies.Count + typeParameters.Count > 0);
+ TypeParameters = typeParameters;
+ Dummies = dummies;
+ Attributes = kv;
+ _Body = body;
+ if (immutable)
+ CachedHashCode = ComputeHashCode();
+ }
+
+ abstract public BinderKind Kind {
+ get;
+ }
+
+ protected static bool CompareAttributesAndTriggers = false;
+
+ public static bool EqualWithAttributesAndTriggers(object a, object b) {
+ CompareAttributesAndTriggers = true;
+ var res = object.Equals(a, b);
+ Contract.Assert(CompareAttributesAndTriggers);
+ CompareAttributesAndTriggers = false;
+ return res;
+ }
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ return BinderEquals(obj);
+ }
+
+ public bool BinderEquals(object obj) {
+ if (obj == null) {
+ return false;
+ }
+ if (!(obj is BinderExpr) ||
+ this.Kind != ((BinderExpr) obj).Kind) {
+ return false;
+ }
+
+ var other = (BinderExpr) obj;
+
+ return this.TypeParameters.SequenceEqual(other.TypeParameters)
+ && this.Dummies.SequenceEqual(other.Dummies)
+ && (!CompareAttributesAndTriggers || object.Equals(this.Attributes, other.Attributes))
+ && object.Equals(this.Body, other.Body);
+ }
+
+ [Pure]
+ 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.
+ int h = 0;
+ foreach (var dummyVar in this.Dummies) {
+ h = ( 53 * h ) + dummyVar.GetHashCode();
+ }
+
+ h ^= this.Body.GetHashCode();
+
+ // DO NOT USE TypeParameters.GetHashCode() because we want structural
+ // identical Expr to have the same hash code **not** identical references
+ // to have the same hash code.
+ int h2 = 0;
+ foreach (var typeParam in this.TypeParameters) {
+ h2 = ( 97 * h2 ) + typeParam.GetHashCode();
+ }
+
+ h = h * 5 + h2;
+ h *= ((int)Kind + 1);
+ return h;
+ }
+
+ protected virtual void EmitTypeHint(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
+ }
+
+ protected virtual void EmitTriggers(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
+ }
+
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
+ stream.push();
+ stream.Write(this, "({0}", Kind.ToString().ToLower());
+ this.EmitTypeHint(stream);
+ Type.EmitOptionalTypeParams(stream, TypeParameters);
+ stream.Write(this, " ");
+ this.Dummies.Emit(stream, true);
+ stream.Write(" :: ");
+ stream.sep();
+ for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
+ kv.Emit(stream);
+ stream.Write(" ");
+ }
+ this.EmitTriggers(stream);
+ stream.sep();
+
+ this.Body.Emit(stream);
+ stream.Write(")");
+ stream.pop();
+ }
+
+ protected virtual void ResolveTriggers(ResolutionContext rc) {
+ Contract.Requires(rc != null);
+ }
+
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ if (rc.TriggerMode) {
+ rc.Error(this, "quantifiers are not allowed in triggers");
+ }
+
+ int previousTypeBinderState = rc.TypeBinderState;
+ try {
+ foreach (TypeVariable/*!*/ v in TypeParameters) {
+ Contract.Assert(v != null);
+ rc.AddTypeBinder(v);
+ }
+
+ rc.PushVarContext();
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
+ v.Register(rc);
+ v.Resolve(rc);
+ }
+ for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
+ kv.Resolve(rc);
+ }
+ this.ResolveTriggers(rc);
+ Body.Resolve(rc);
+ rc.PopVarContext();
+
+ // establish a canonical order of the type parameters
+ this.TypeParameters = Type.SortTypeParams(TypeParameters, new List<Type>(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()), null);
+
+ } finally {
+ rc.TypeBinderState = previousTypeBinderState;
+ }
+ }
+
+ public override void ComputeFreeVariables(Set freeVars) {
+ //Contract.Requires(freeVars != null);
+ ComputeBinderFreeVariables(TypeParameters, Dummies, Body, Attributes, freeVars);
+ }
+
+ public static void ComputeBinderFreeVariables(List<TypeVariable> typeParameters, List<Variable> dummies, Expr body, QKeyValue attributes, Set freeVars) {
+ Contract.Requires(dummies != null);
+ Contract.Requires(body != null);
+
+ foreach (var v in dummies) {
+ Contract.Assert(v != null);
+ Contract.Assert(!freeVars[v]);
+ }
+ body.ComputeFreeVariables(freeVars);
+ for (var a = attributes; a != null; a = a.Next) {
+ foreach (var o in a.Params) {
+ var e = o as Expr;
+ if (e != null) {
+ e.ComputeFreeVariables(freeVars);
+ }
+ }
+ }
+ foreach (var v in dummies) {
+ freeVars.AddRange(v.TypedIdent.Type.FreeVariables);
+ }
+ freeVars.RemoveRange(dummies);
+ freeVars.RemoveRange(typeParameters);
+ }
+
+ protected List<TypeVariable> GetUnmentionedTypeParameters() {
+ Contract.Ensures(Contract.Result<List<TypeVariable>>() != null);
+ List<TypeVariable>/*!*/ dummyParameters = Type.FreeVariablesIn(new List<Type>(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()));
+ Contract.Assert(dummyParameters != null);
+ List<TypeVariable>/*!*/ unmentionedParameters = new List<TypeVariable>();
+ foreach (TypeVariable/*!*/ var in TypeParameters) {
+ Contract.Assert(var != null);
+ if (!dummyParameters.Contains(var))
+ unmentionedParameters.Add(var);
+ }
+ return unmentionedParameters;
+ }
+ }
+
+ public class QKeyValue : Absy {
+ public readonly string/*!*/ Key;
+ private readonly List<object/*!*/>/*!*/ _params; // each element is either a string or an Expr
+
+ public void AddParam(object p)
+ {
+ Contract.Requires(p != null);
+ this._params.Add(p);
+ }
+
+ public void AddParams(IEnumerable<object> ps)
+ {
+ Contract.Requires(cce.NonNullElements(ps));
+ this._params.AddRange(ps);
+ }
+
+ public void ClearParams()
+ {
+ this._params.Clear();
+ }
+
+ public IList<object> Params
+ {
+ get
+ {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IList<object>>()));
+ Contract.Ensures(Contract.Result<IList<object>>().IsReadOnly);
+ return this._params.AsReadOnly();
+ }
+ }
+
+ public QKeyValue Next;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Key != null);
+ Contract.Invariant(cce.NonNullElements(this._params));
+ }
+
+ public QKeyValue(IToken tok, string key, IList<object/*!*/>/*!*/ parameters, QKeyValue next)
+ : base(tok) {
+ Contract.Requires(key != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(cce.NonNullElements(parameters));
+ Key = key;
+ this._params = new List<object>(parameters);
+ Next = next;
+ }
+
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
+ stream.Write("{:");
+ stream.Write(Key);
+ string sep = " ";
+ foreach (object p in Params) {
+ stream.Write(sep);
+ sep = ", ";
+ if (p is string) {
+ stream.Write("\"");
+ stream.Write((string)p);
+ stream.Write("\"");
+ } else {
+ ((Expr)p).Emit(stream);
+ }
+ }
+ stream.Write("}");
+ }
+
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+
+ if ((Key == "minimize" || Key == "maximize") && Params.Count != 1)
+ {
+ rc.Error(this, "attributes :minimize and :maximize accept only one argument");
+ }
+
+ if (Key == "verified_under" && Params.Count != 1)
+ {
+ rc.Error(this, "attribute :verified_under accepts only one argument");
+ }
+
+ foreach (object p in Params) {
+ if (p is Expr) {
+ ((Expr)p).Resolve(rc);
+ }
+ }
+ }
+
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ foreach (object p in Params) {
+ var expr = p as Expr;
+ if (expr != null) {
+ expr.Typecheck(tc);
+ }
+ if ((Key == "minimize" || Key == "maximize")
+ && (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv)))
+ {
+ tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv");
+ break;
+ }
+ if (Key == "verified_under" && (expr == null || !expr.Type.IsBool))
+ {
+ tc.Error(this, "attribute :verified_under accepts only one argument of type bool");
+ break;
+ }
+ }
+ }
+ public void AddLast(QKeyValue other) {
+ Contract.Requires(other != null);
+ QKeyValue current = this;
+ while (current.Next != null) {
+ current = current.Next;
+ }
+ current.Next = other;
+ }
+ // Look for {:name string} in list of attributes.
+ [Pure]
+ public static string FindStringAttribute(QKeyValue kv, string name) {
+ Contract.Requires(name != null);
+ for (; kv != null; kv = kv.Next) {
+ if (kv.Key == name) {
+ if (kv.Params.Count == 1 && kv.Params[0] is string) {
+ return (string)kv.Params[0];
+ }
+ }
+ }
+ return null;
+ }
+ // Look for {:name expr} in list of attributes.
+ public static Expr FindExprAttribute(QKeyValue kv, string name) {
+ Contract.Requires(name != null);
+ for (; kv != null; kv = kv.Next) {
+ if (kv.Key == name) {
+ if (kv.Params.Count == 1 && kv.Params[0] is Expr) {
+ return (Expr)kv.Params[0];
+ }
+ }
+ }
+ return null;
+ }
+ // Return 'true' if {:name true} or {:name} is an attribute in 'kv'
+ public static bool FindBoolAttribute(QKeyValue kv, string name) {
+ Contract.Requires(name != null);
+ for (; kv != null; kv = kv.Next) {
+ if (kv.Key == name) {
+ return kv.Params.Count == 0 ||
+ (kv.Params.Count == 1 && kv.Params[0] is LiteralExpr && ((LiteralExpr)kv.Params[0]).IsTrue);
+ }
+ }
+ return false;
+ }
+
+ public static int FindIntAttribute(QKeyValue kv, string name, int defl) {
+ Contract.Requires(name != null);
+ Expr e = FindExprAttribute(kv, name);
+ LiteralExpr l = e as LiteralExpr;
+ if (l != null && l.isBigNum)
+ return l.asBigNum.ToIntSafe;
+ return defl;
+ }
+
+ public override Absy Clone() {
+ List<object> newParams = new List<object>();
+ foreach (object o in Params)
+ newParams.Add(o);
+ return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue)Next.Clone());
+ }
+
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ return visitor.VisitQKeyValue(this);
+ }
+
+ public override bool Equals(object obj) {
+ var other = obj as QKeyValue;
+ if (other == null) {
+ return false;
+ } else {
+ return Key == other.Key && object.Equals(Params, other.Params) &&
+ (Next == null
+ ? other.Next == null
+ : object.Equals(Next, other.Next));
+ }
+ }
+
+ public override int GetHashCode() {
+ throw new NotImplementedException();
+ }
+ }
+
+ public class Trigger : Absy {
+ public readonly bool Pos;
+ [Rep]
+ private List<Expr>/*!*/ tr;
+
+ public IList<Expr>/*!*/ Tr
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<IList<Expr>>() != null);
+ Contract.Ensures(Contract.Result<IList<Expr>>().Count >= 1);
+ Contract.Ensures(this.Pos || Contract.Result<IList<Expr>>().Count == 1);
+ return this.tr.AsReadOnly();
+ }
+ set
+ {
+ Contract.Requires(value != null);
+ Contract.Requires(value.Count >= 1);
+ Contract.Requires(this.Pos || value.Count == 1);
+ this.tr = new List<Expr>(value);
+ }
+ }
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(this.tr != null);
+ Contract.Invariant(this.tr.Count >= 1);
+ Contract.Invariant(Pos || this.tr.Count == 1);
+ }
+
+ public Trigger Next;
+
+ public Trigger(IToken/*!*/ tok, bool pos, IEnumerable<Expr>/*!*/ tr, Trigger next = null)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(tr != null);
+ Contract.Requires(tr.Count() >= 1);
+ Contract.Requires(pos || tr.Count() == 1);
+ this.Pos = pos;
+ this.Tr = new List<Expr>(tr);
+ this.Next = next;
+ }
+
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
+ stream.SetToken(this);
+ Contract.Assert(this.Tr.Count >= 1);
+ string/*!*/ sep = Pos ? "{ " : "{:nopats ";
+ foreach (Expr/*!*/ e in this.Tr) {
+ Contract.Assert(e != null);
+ stream.Write(sep);
+ sep = ", ";
+ e.Emit(stream);
+ }
+ stream.Write(" }");
+ }
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ rc.TriggerMode = true;
+ foreach (Expr/*!*/ e in this.Tr) {
+ Contract.Assert(e != null);
+ e.Resolve(rc);
+
+ // just a variable by itself is not allowed
+ if (e is IdentifierExpr) {
+ rc.Error(e, "a matching pattern must be more than just a variable by itself: {0}", e);
+ }
+
+ // the free-variable check is performed in the surrounding quantifier expression (because that's
+ // where the bound variables are known)
+ }
+ rc.TriggerMode = false;
+ }
+
+ /// <summary>
+ /// Add to "freeVars" the free variables in the triggering expressions.
+ /// </summary>
+ public void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ Contract.Requires(freeVars != null);
+ foreach (Expr/*!*/ e in this.Tr) {
+ Contract.Assert(e != null);
+ e.ComputeFreeVariables(freeVars);
+ }
+ }
+
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ foreach (Expr/*!*/ e in this.Tr) {
+ Contract.Assert(e != null);
+ e.Typecheck(tc);
+ }
+ }
+
+ public void AddLast(Trigger other) {
+ Trigger current = this;
+ while (current.Next != null) {
+ current = current.Next;
+ }
+ current.Next = other;
+ }
+
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+ return visitor.VisitTrigger(this);
+ }
+
+ public override bool Equals(object obj) {
+ var other = obj as Trigger;
+ if (other == null) {
+ return false;
+ } else {
+ return this.Tr.SequenceEqual(other.Tr) &&
+ (Next == null ? other.Next == null : object.Equals(Next, other.Next));
+ }
+ }
+
+ public override int GetHashCode() {
+ throw new NotImplementedException();
+ }
+ }
+
+ public class ForallExpr : QuantifierExpr {
+ public ForallExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams,
+ 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, 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, 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, bool immutable=false)
+ : base(tok, typeParams, dummies, null, null, body, immutable) {
+ Contract.Requires(body != null);
+ Contract.Requires(dummies != null);
+ Contract.Requires(typeParams != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(dummies.Count + typeParams.Count > 0);
+ }
+
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+ return visitor.VisitForallExpr(this);
+ }
+
+ public override BinderKind Kind {
+ get {
+ return BinderKind.Forall;
+ }
+ }
+ }
+
+ public class ExistsExpr : QuantifierExpr {
+ public ExistsExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams, 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 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, 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 override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+ return visitor.VisitExistsExpr(this);
+ }
+
+ public override BinderKind Kind {
+ get {
+ return BinderKind.Exists;
+ }
+ }
+ }
+
+ public abstract class QuantifierExpr : BinderExpr {
+ public Trigger Triggers;
+
+ static int SkolemIds = -1;
+ public static int GetNextSkolemId() {
+ return System.Threading.Interlocked.Increment(ref SkolemIds);
+ }
+
+ public readonly int SkolemId;
+
+ public QuantifierExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
+ 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);
+ Contract.Requires(body != null);
+ Contract.Requires(dummies.Count + typeParameters.Count > 0);
+
+ Contract.Assert((this is ForallExpr) || (this is ExistsExpr));
+
+ Triggers = triggers;
+ SkolemId = GetNextSkolemId();
+ }
+
+ protected override void EmitTriggers(TokenTextWriter stream) {
+ //Contract.Requires(stream != null);
+ stream.push();
+ for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
+ tr.Emit(stream);
+ stream.Write(" ");
+ stream.sep();
+ }
+ stream.pop();
+ }
+
+ // if the user says ( forall x :: forall y :: ... ) and specifies *no* triggers, we transform it to
+ // (forall x, y :: ... ) which may help the prover to pick trigger terms
+ //
+ // (Note: there used to be a different criterion here, which allowed merging when triggers were specified, which could cause prover errors due to resulting unbound variables in the triggers)
+ private void MergeAdjecentQuantifier() {
+ QuantifierExpr qbody = Body as QuantifierExpr;
+ if (!(qbody != null && (qbody is ForallExpr) == (this is ForallExpr) && Triggers == null)) {
+ return;
+ }
+ qbody.MergeAdjecentQuantifier();
+ if (this.Triggers != null || qbody.Triggers != null) {
+ return;
+ }
+ Body = qbody.Body;
+ TypeParameters.AddRange(qbody.TypeParameters);
+ Dummies.AddRange(qbody.Dummies);
+ Triggers = qbody.Triggers;
+ if (qbody.Attributes != null) {
+ if (Attributes == null) {
+ Attributes = qbody.Attributes;
+ } else {
+ QKeyValue p = Attributes;
+ while (p.Next != null) {
+ p = p.Next;
+ }
+ p.Next = qbody.Attributes;
+ }
+ }
+ }
+
+ #region never triggers
+ private class NeverTriggerCollector : ReadOnlyVisitor {
+ QuantifierExpr/*!*/ parent;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(parent != null);
+ }
+
+ public NeverTriggerCollector(QuantifierExpr p) {
+ Contract.Requires(p != null);
+ parent = p;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node) {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ FunctionCall fn = node.Fun as FunctionCall;
+ if (fn != null && cce.NonNull(fn.Func).NeverTrigger) {
+ parent.Triggers = new Trigger(fn.Func.tok, false, new List<Expr> { node} , parent.Triggers);
+ }
+ return base.VisitNAryExpr(node);
+ }
+ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) {
+ // don't go into quantifier expression or its triggers, since the terms in there may have more bound variables
+ // (note, with only the VisitBinderExpr override below, we'd still be visiting triggers, which we don't want to do)
+ return node;
+ }
+ public override BinderExpr VisitBinderExpr(BinderExpr node) {
+ // don't go into binder expression, since the terms in there may have more bound variables
+ return node;
+ }
+ }
+
+ private bool neverTriggerApplied;
+ private void ApplyNeverTriggers() {
+ if (neverTriggerApplied) {
+ return;
+ }
+ neverTriggerApplied = true;
+
+ for (Trigger t = Triggers; t != null; t = t.Next) {
+ if (t.Pos) {
+ return;
+ }
+ }
+
+ NeverTriggerCollector visitor = new NeverTriggerCollector(this);
+ visitor.VisitExpr(Body);
+ }
+ #endregion
+
+ protected override void ResolveTriggers(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
+ int prevErrorCount = rc.ErrorCount;
+ tr.Resolve(rc);
+ if (prevErrorCount == rc.ErrorCount) {
+ // for positive triggers, make sure all bound variables are mentioned
+ if (tr.Pos) {
+ Set /*Variable*/ freeVars = new Set /*Variable*/ ();
+ tr.ComputeFreeVariables(freeVars);
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
+ if (!freeVars[v]) {
+ rc.Error(tr, "trigger must mention all quantified variables, but does not mention: {0}", v);
+ }
+ }
+ }
+ }
+ }
+ }
+
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ int oldErrorCount = rc.ErrorCount;
+
+ this.MergeAdjecentQuantifier();
+
+ base.Resolve(rc);
+
+ if (oldErrorCount == rc.ErrorCount) {
+ this.ApplyNeverTriggers();
+ }
+ }
+
+
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
+ kv.Typecheck(tc);
+ }
+ for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
+ tr.Typecheck(tc);
+ }
+ Body.Typecheck(tc);
+ Contract.Assert(Body.Type != null); // follows from postcondition of Expr.Typecheck
+ if (!Body.Type.Unify(Type.Bool)) {
+ tc.Error(this, "quantifier body must be of type bool");
+ }
+ this.Type = Type.Bool;
+
+ // Check that type parameters occur in the types of the
+ // dummies, or otherwise in the triggers. This can only be
+ // done after typechecking
+ List<TypeVariable>/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();
+ Contract.Assert(unmentionedParameters != null);
+
+ if (unmentionedParameters.Count > 0) {
+ // all the type parameters that do not occur in dummy types
+ // have to occur in triggers
+
+ for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
+ // for positive triggers, make sure all bound variables are mentioned
+ if (tr.Pos) {
+ Set /*Variable*/ freeVars = new Set /*Variable*/ ();
+ tr.ComputeFreeVariables(freeVars);
+ foreach (TypeVariable/*!*/ v in unmentionedParameters) {
+ Contract.Assert(v != null);
+ if (!freeVars[v])
+ tc.Error(tr,
+ "trigger does not mention {0}, which does not occur in variables types either",
+ v);
+ }
+ }
+ }
+ }
+ }
+ public override Type/*!*/ ShallowType {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ return Type.Bool;
+ }
+ }
+
+ public override bool Equals(object obj) {
+ var other = obj as QuantifierExpr;
+ if (other == null) {
+ return false;
+ } else {
+ return this.BinderEquals(obj) &&
+ (!CompareAttributesAndTriggers || object.Equals(Triggers, other.Triggers));
+ }
+ }
+ }
+
+
+ public class LambdaExpr : BinderExpr {
+ public LambdaExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
+ 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);
+ Contract.Requires(body != null);
+ Contract.Requires(dummies.Count + typeParameters.Count > 0);
+ }
+
+ public override BinderKind Kind {
+ get {
+ return BinderKind.Lambda;
+ }
+ }
+
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ base.Resolve(rc);
+ }
+
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
+ kv.Typecheck(tc);
+ }
+ Body.Typecheck(tc);
+ Contract.Assert(Body.Type != null); // follows from postcondition of Expr.Typecheck
+
+ List<Type>/*!*/ argTypes = new List<Type>();
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
+ argTypes.Add(v.TypedIdent.Type);
+ }
+ this.Type = new MapType(this.tok, this.TypeParameters, argTypes, Body.Type);
+
+ // Check that type parameters occur in the types of the
+ // dummies, or otherwise in the triggers. This can only be
+ // done after typechecking
+ List<TypeVariable>/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();
+ Contract.Assert(unmentionedParameters != null);
+
+ if (unmentionedParameters.Count > 0) {
+ tc.Error(this, "the type variable {0} does not occur in types of the lambda parameters", unmentionedParameters[0]);
+ }
+ }
+
+ private Type mapType;
+ public override Type/*!*/ ShallowType {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ if (mapType == null) {
+ List<Type>/*!*/ argTypes = new List<Type>();
+ foreach (Variable/*!*/ v in Dummies) {
+ Contract.Assert(v != null);
+ argTypes.Add(v.TypedIdent.Type);
+ }
+ mapType = new MapType(this.tok, this.TypeParameters, argTypes, Body.ShallowType);
+ }
+
+ return mapType;
+ }
+ }
+
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+ return visitor.VisitLambdaExpr(this);
+ }
+
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 12:29:48 +0000