//----------------------------------------------------------------------------- // // Copyright (C) Microsoft Corporation. All Rights Reserved. // //----------------------------------------------------------------------------- using System; using System.Text; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Numerics; using Microsoft.Boogie; namespace Microsoft.Dafny { public class Program { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Name != null); Contract.Invariant(cce.NonNullElements(Modules)); } public readonly string Name; public readonly List/*!*/ Modules; public readonly BuiltIns BuiltIns; public Program(string name, [Captured] List/*!*/ modules, [Captured] BuiltIns builtIns) { Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(modules)); Name = name; Modules = modules; BuiltIns = builtIns; } } public class BuiltIns { public readonly ModuleDecl SystemModule = new ModuleDecl(Token.NoToken, "_System", false, null, new List(), null); Dictionary arrayTypeDecls = new Dictionary(); public BuiltIns() { // create class 'object' ClassDecl obj = new ClassDecl(Token.NoToken, "object", SystemModule, new List(), new List(), null); SystemModule.TopLevelDecls.Add(obj); // add one-dimensional arrays, since they may arise during type checking UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true); } public UserDefinedType ArrayType(int dims, Type arg) { return ArrayType(Token.NoToken, dims, arg, false); } public UserDefinedType ArrayType(IToken tok, int dims, Type arg, bool allowCreationOfNewClass) { Contract.Requires(tok != null); Contract.Requires(1 <= dims); Contract.Requires(arg != null); Contract.Ensures(Contract.Result() != null); List typeArgs = new List(); typeArgs.Add(arg); UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null); if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) { ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule); for (int d = 0; d < dims; d++) { string name = dims == 1 ? "Length" : "Length" + d; string compiledName = dims == 1 ? "Length" : "GetLength(" + d + ")"; Field len = new SpecialField(Token.NoToken, name, compiledName, "new BigInteger(", ")", false, false, Type.Int, null); len.EnclosingClass = arrayClass; // resolve here arrayClass.Members.Add(len); } arrayTypeDecls.Add(dims, arrayClass); SystemModule.TopLevelDecls.Add(arrayClass); } udt.ResolvedClass = arrayTypeDecls[dims]; return udt; } public static string ArrayClassName(int dims) { Contract.Requires(1 <= dims); if (dims == 1) { return "array"; } else { return "array" + dims; } } } public class Attributes { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Name != null); Contract.Invariant(cce.NonNullElements(Args)); } public readonly string Name; /*Frozen*/ public readonly List/*!*/ Args; public readonly Attributes Prev; public Attributes(string name, [Captured] List/*!*/ args, Attributes prev) { Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(args)); Name = name; Args = args; Prev = prev; } public static bool Contains(Attributes attrs, string nm) { Contract.Requires(nm != null); for (; attrs != null; attrs = attrs.Prev) { if (attrs.Name == nm) { return true; } } return false; } /// /// Returns true if "nm" is a specified attribute. If it is, then: /// - if the attribute is {:nm true}, then value==true /// - if the attribute is {:nm false}, then value==false /// - if the attribute is anything else, then value returns as whatever it was passed in as. /// public static bool ContainsBool(Attributes attrs, string nm, ref bool value) { Contract.Requires(nm != null); for (; attrs != null; attrs = attrs.Prev) { if (attrs.Name == nm) { if (attrs.Args.Count == 1) { var arg = attrs.Args[0].E as LiteralExpr; if (arg != null && arg.Value is bool) { value = (bool)arg.Value; } } return true; } } return false; } public class Argument { public readonly IToken Tok; public readonly string S; public readonly Expression E; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Tok != null); Contract.Invariant((S == null) != (E == null)); } public Argument(IToken tok, string s) { Contract.Requires(tok != null); Contract.Requires(s != null); Tok = tok; S = s; } public Argument(IToken tok, Expression e) { Contract.Requires(tok != null); Contract.Requires(e != null); Tok = tok; E = e; } } } // ------------------------------------------------------------------------------------------------------ public abstract class Type { public static readonly BoolType Bool = new BoolType(); public static readonly IntType Int = new IntType(); /// /// Used in error situations in order to reduce further error messages. /// //[Pure(false)] public static Type Flexible { get { Contract.Ensures(Contract.Result() != null); return new InferredTypeProxy(); } } /// /// Return the most constrained version of "this". /// /// public Type Normalize() { Contract.Ensures(Contract.Result() != null); Type type = this; while (true) { TypeProxy pt = type as TypeProxy; if (pt != null && pt.T != null) { type = pt.T; } else { return type; } } } public bool IsSubrangeType { get { return this is NatType; } } public bool IsRefType { get { if (this is ObjectType) { return true; } else { UserDefinedType udt = this as UserDefinedType; return udt != null && udt.ResolvedParam == null && udt.ResolvedClass is ClassDecl; } } } public bool IsArrayType { get { return AsArrayType != null; } } public ArrayClassDecl/*?*/ AsArrayType { get { UserDefinedType udt = UserDefinedType.DenotesClass(this); return udt == null ? null : udt.ResolvedClass as ArrayClassDecl; } } public bool IsDatatype { get { return AsDatatype != null; } } public DatatypeDecl AsDatatype { get { UserDefinedType udt = this as UserDefinedType; if (udt == null) { return null; } else { return udt.ResolvedClass as DatatypeDecl; } } } public bool IsIndDatatype { get { return AsIndDatatype != null; } } public IndDatatypeDecl AsIndDatatype { get { UserDefinedType udt = this as UserDefinedType; if (udt == null) { return null; } else { return udt.ResolvedClass as IndDatatypeDecl; } } } public bool IsCoDatatype { get { return AsCoDatatype != null; } } public CoDatatypeDecl AsCoDatatype { get { UserDefinedType udt = this as UserDefinedType; if (udt == null) { return null; } else { return udt.ResolvedClass as CoDatatypeDecl; } } } public bool InvolvesCoDatatype { get { return IsCoDatatype; // TODO: should really check structure of the type recursively } } public bool IsTypeParameter { get { return AsTypeParameter != null; } } public TypeParameter AsTypeParameter { get { UserDefinedType ct = this as UserDefinedType; return ct == null ? null : ct.ResolvedParam; } } public virtual bool SupportsEquality { get { return true; } } } /// /// A NonProxy type is a fully constrained type. It may contain members. /// public abstract class NonProxyType : Type { } public abstract class BasicType : NonProxyType { } public class BoolType : BasicType { [Pure] public override string ToString() { return "bool"; } } public class IntType : BasicType { [Pure] public override string ToString() { return "int"; } } public class NatType : IntType { [Pure] public override string ToString() { return "nat"; } } public class ObjectType : BasicType { [Pure] public override string ToString() { return "object"; } } public abstract class CollectionType : NonProxyType { public readonly Type Arg; // denotes the Domain type for a Map [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Arg != null); } public CollectionType(Type arg) { Contract.Requires(arg != null); this.Arg = arg; } public override bool SupportsEquality { get { return Arg.SupportsEquality; } } } public class SetType : CollectionType { public SetType(Type arg) : base(arg) { Contract.Requires(arg != null); } [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); Contract.Assume(cce.IsPeerConsistent(Arg)); return "set<" + base.Arg + ">"; } } public class MultiSetType : CollectionType { public MultiSetType(Type arg) : base(arg) { Contract.Requires(arg != null); } [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); Contract.Assume(cce.IsPeerConsistent(Arg)); return "multiset<" + base.Arg + ">"; } } public class SeqType : CollectionType { public SeqType(Type arg) : base(arg) { Contract.Requires(arg != null); } [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); Contract.Assume(cce.IsPeerConsistent(Arg)); return "seq<" + base.Arg + ">"; } } public class MapType : CollectionType { public Type Range; public MapType(Type domain, Type range) : base(domain) { Contract.Requires(domain != null && range != null); Range = range; } public Type Domain { get { return Arg; } } [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); Contract.Assume(cce.IsPeerConsistent(Domain)); Contract.Assume(cce.IsPeerConsistent(Range)); return "map<" + Domain +", " + Range + ">"; } } public class UserDefinedType : NonProxyType { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(tok != null); Contract.Invariant(Name != null); Contract.Invariant(cce.NonNullElements(TypeArgs)); } public readonly IToken ModuleName; // may be null public readonly IToken tok; // token of the Name public readonly string Name; [Rep] public readonly List/*!*/ TypeArgs; public string FullName { get { if (ResolvedClass != null && !ResolvedClass.Module.IsDefaultModule) { return ResolvedClass.Module.Name + "." + Name; } else { return Name; } } } string compileName; public string CompileName { get { if (compileName == null) { compileName = NonglobalVariable.CompilerizeName(Name); } return compileName; } } public string FullCompileName { get { if (ResolvedClass != null && !ResolvedClass.Module.IsDefaultModule) { return ResolvedClass.Module.CompileName + "." + CompileName; } else { return CompileName; } } } public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List/*!*/ typeArgs, IToken moduleName) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); this.ModuleName = moduleName; this.tok = tok; this.Name = name; this.TypeArgs = typeArgs; } /// /// This constructor constructs a resolved class type /// public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, TopLevelDecl/*!*/ cd, [Captured] List/*!*/ typeArgs) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cd != null); Contract.Requires(cce.NonNullElements(typeArgs)); this.tok = tok; this.Name = name; this.TypeArgs = typeArgs; this.ResolvedClass = cd; } /// /// This constructor constructs a resolved type parameter /// public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, TypeParameter/*!*/ tp) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(tp != null); this.tok = tok; this.Name = name; this.TypeArgs = new List(); this.ResolvedParam = tp; } /// /// If type denotes a resolved class type, then return that class type. /// Otherwise, return null. /// public static UserDefinedType DenotesClass(Type/*!*/ type) { Contract.Requires(type != null); Contract.Ensures(Contract.Result() == null || Contract.Result().ResolvedClass is ClassDecl); type = type.Normalize(); UserDefinedType ct = type as UserDefinedType; if (ct != null && ct.ResolvedClass is ClassDecl) { return ct; } else { return null; } } public static Type ArrayElementType(Type type) { Contract.Requires(type.IsArrayType); Contract.Requires(type != null); Contract.Ensures(Contract.Result() != null); UserDefinedType udt = DenotesClass(type); Contract.Assert(udt != null); Contract.Assert(udt.TypeArgs.Count == 1); // holds true of all array types return udt.TypeArgs[0]; } [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); string s = Name; if (ModuleName != null) { s = ModuleName.val + "." + s; } if (TypeArgs.Count != 0) { string sep = "<"; foreach (Type t in TypeArgs) { Contract.Assume(cce.IsPeerConsistent(t)); s += sep + t; sep = ","; } s += ">"; } return s; } public override bool SupportsEquality { get { if (ResolvedClass is ClassDecl) { return true; } else if (ResolvedClass is CoDatatypeDecl) { return false; } else if (ResolvedClass is IndDatatypeDecl) { var dt = (IndDatatypeDecl)ResolvedClass; Contract.Assume(dt.EqualitySupport != IndDatatypeDecl.ES.NotYetComputed); if (dt.EqualitySupport == IndDatatypeDecl.ES.Never) { return false; } Contract.Assert(dt.TypeArgs.Count == TypeArgs.Count); var i = 0; foreach (var tp in dt.TypeArgs) { if (tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && !TypeArgs[i].SupportsEquality) { return false; } i++; } return true; } else if (ResolvedParam != null) { return ResolvedParam.MustSupportEquality; } Contract.Assume(false); // the SupportsEquality getter requires the Type to have been successfully resolved return true; } } } public abstract class TypeProxy : Type { public Type T; // filled in during resolution internal TypeProxy() { } [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); Contract.Assume(T == null || cce.IsPeerConsistent(T)); return T == null ? "?" : T.ToString(); } public override bool SupportsEquality { get { if (T != null) { return T.SupportsEquality; } else { return base.SupportsEquality; } } } } public abstract class UnrestrictedTypeProxy : TypeProxy { } /// /// This proxy stands for any type. /// public class InferredTypeProxy : UnrestrictedTypeProxy { } /// /// This proxy stands for any type, but it originates from an instantiated type parameter. /// public class ParamTypeProxy : UnrestrictedTypeProxy { TypeParameter orig; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(orig != null); } public ParamTypeProxy(TypeParameter orig) { Contract.Requires(orig != null); this.orig = orig; } } public abstract class RestrictedTypeProxy : TypeProxy { /// /// The OrderID is used to simplify the unification code. Each restricted type proxy should use its /// own OrderID. /// public abstract int OrderID { get; } } /// /// This proxy stands for any datatype. /// public class DatatypeProxy : RestrictedTypeProxy { public override int OrderID { get { return 0; } } } /// /// This proxy stands for object or any class/array type. /// public class ObjectTypeProxy : RestrictedTypeProxy { public override int OrderID { get { return 1; } } } /// /// This proxy stands for: /// set(Arg) or seq(Arg) or map(Arg, Range) /// public class CollectionTypeProxy : RestrictedTypeProxy { public readonly Type Arg; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Arg != null); } public CollectionTypeProxy(Type arg) { Contract.Requires(arg != null); Arg = arg; } public override int OrderID { get { return 2; } } } /// /// This proxy stands for either: /// int or set or multiset or seq /// if AllowSeq, or: /// int or set or multiset /// if !AllowSeq. /// public class OperationTypeProxy : RestrictedTypeProxy { public readonly bool AllowSeq; public OperationTypeProxy(bool allowSeq) { AllowSeq = allowSeq; } public override int OrderID { get { return 3; } } } /// /// This proxy stands for: /// seq(Arg) or array(Arg) or map(Arg, Range) /// public class IndexableTypeProxy : RestrictedTypeProxy { public readonly Type Arg, Domain; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Arg != null); } public IndexableTypeProxy(Type arg, Type domain) { Contract.Requires(arg != null); Arg = arg; Domain = domain; } public override int OrderID { get { return 4; } } } // ------------------------------------------------------------------------------------------------------ public abstract class Declaration { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(tok != null); Contract.Invariant(Name != null); } public IToken/*!*/ tok; public IToken BodyStartTok = Token.NoToken; public IToken BodyEndTok = Token.NoToken; public readonly string/*!*/ Name; string compileName; public string CompileName { get { if (compileName == null) { compileName = NonglobalVariable.CompilerizeName(Name); } return compileName; } } public readonly Attributes Attributes; public Declaration(IToken tok, string name, Attributes attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); this.tok = tok; this.Name = name; this.Attributes = attributes; } [Pure] public override string ToString() { Contract.Ensures(Contract.Result() != null); return Name; } } public class TypeParameter : Declaration { public interface ParentType { } [Peer] ParentType parent; public ParentType Parent { get { return parent; } [param: Captured] set { Contract.Requires(Parent == null); // set it only once Contract.Requires(value != null); // BUGBUG: The following line is a workaround to tell the verifier that 'value' is not of an Immutable type. // A proper solution would be to be able to express that in the program (in a specification or attribute) or // to be able to declare 'parent' as [PeerOrImmutable]. Contract.Requires(value is TopLevelDecl || value is Function || value is Method || value is DatatypeCtor); //modifies parent; parent = value; } } public enum EqualitySupportValue { Required, InferredRequired, Unspecified } public EqualitySupportValue EqualitySupport; // the resolver may change this value from Unspecified to InferredRequired (for some signatures that may immediately imply that equality support is required) public bool MustSupportEquality { get { return EqualitySupport != EqualitySupportValue.Unspecified; } } public bool NecessaryForEqualitySupportOfSurroundingInductiveDatatype = false; // computed during resolution; relevant only when Parent denotes an IndDatatypeDecl public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified) : base(tok, name, null) { Contract.Requires(tok != null); Contract.Requires(name != null); EqualitySupport = equalitySupport; } } public class ModuleDecl : Declaration { public readonly string RefinementBaseName; // null if no refinement base public ModuleDecl RefinementBase; // filled in during resolution (null if no refinement base) public readonly List/*!*/ ImportNames; // contains no duplicates public readonly List/*!*/ Imports = new List(); // filled in during resolution, contains no duplicates public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that public readonly Graph CallGraph = new Graph(); // filled in during resolution public int Height; // height in the topological sorting of modules; filled in during resolution public readonly bool IsGhost; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(ImportNames)); Contract.Invariant(cce.NonNullElements(TopLevelDecls)); Contract.Invariant(CallGraph != null); } public ModuleDecl(IToken tok, string name, bool isGhost, string refinementBase, [Captured] List/*!*/ imports, Attributes attributes) : base(tok, name, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(imports)); RefinementBaseName = refinementBase; // set "ImportNames" to "imports" minus any duplicates ImportNames = new List(); foreach (var nm in imports) { if (!ImportNames.Contains(nm)) { ImportNames.Add(nm); } } IsGhost = isGhost; } public virtual bool IsDefaultModule { get { return false; } } } public class DefaultModuleDecl : ModuleDecl { public DefaultModuleDecl() : base(Token.NoToken, "_default", false, null, new List(), null) { } public override bool IsDefaultModule { get { return true; } } } public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType { public readonly ModuleDecl Module; public readonly List/*!*/ TypeArgs; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Module != null); Contract.Invariant(cce.NonNullElements(TypeArgs)); } public TopLevelDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List/*!*/ typeArgs, Attributes attributes) : base(tok, name, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(cce.NonNullElements(typeArgs)); Module = module; TypeArgs = typeArgs; } public string FullName { get { return Module.Name + "." + Name; } } public string FullCompileName { get { return Module.CompileName + "." + CompileName; } } } public class ClassDecl : TopLevelDecl { public readonly List/*!*/ Members; public bool HasConstructor; // filled in (early) during resolution; true iff there exists a member that is a Constructor [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(Members)); } public ClassDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List/*!*/ typeArgs, [Captured] List/*!*/ members, Attributes attributes) : base(tok, name, module, typeArgs, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Requires(cce.NonNullElements(members)); Members = members; } public virtual bool IsDefaultClass { get { return false; } } } public class DefaultClassDecl : ClassDecl { public DefaultClassDecl(ModuleDecl/*!*/ module, [Captured] List/*!*/ members) : base(Token.NoToken, "_default", module, new List(), members, null) { Contract.Requires(module != null); Contract.Requires(cce.NonNullElements(members)); } public override bool IsDefaultClass { get { return true; } } } public class ArrayClassDecl : ClassDecl { public readonly int Dims; public ArrayClassDecl(int dims, ModuleDecl module) : base(Token.NoToken, BuiltIns.ArrayClassName(dims), module, new List(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}), new List(), null) { Contract.Requires(1 <= dims); Contract.Requires(module != null); Dims = dims; } } public abstract class DatatypeDecl : TopLevelDecl { public readonly List/*!*/ Ctors; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(Ctors)); Contract.Invariant(1 <= Ctors.Count); } public DatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List/*!*/ typeArgs, [Captured] List/*!*/ ctors, Attributes attributes) : base(tok, name, module, typeArgs, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Requires(cce.NonNullElements(ctors)); Contract.Requires(1 <= ctors.Count); Ctors = ctors; } } public class IndDatatypeDecl : DatatypeDecl { public DatatypeCtor DefaultCtor; // set during resolution public bool[] TypeParametersUsedInConstructionByDefaultCtor; // set during resolution; has same length as the number of type arguments public enum ES { NotYetComputed, Never, ConsultTypeArguments } public ES EqualitySupport = ES.NotYetComputed; public IndDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List/*!*/ typeArgs, [Captured] List/*!*/ ctors, Attributes attributes) : base(tok, name, module, typeArgs, ctors, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Requires(cce.NonNullElements(ctors)); Contract.Requires(1 <= ctors.Count); } } public class CoDatatypeDecl : DatatypeDecl { public CoDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List/*!*/ typeArgs, [Captured] List/*!*/ ctors, Attributes attributes) : base(tok, name, module, typeArgs, ctors, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Requires(cce.NonNullElements(ctors)); Contract.Requires(1 <= ctors.Count); } } public class DatatypeCtor : Declaration, TypeParameter.ParentType { public readonly List/*!*/ Formals; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(Formals)); Contract.Invariant(Destructors != null); Contract.Invariant( Destructors.Count == 0 || // this is until resolution Destructors.Count == Formals.Count); // after resolution } // TODO: One could imagine having a precondition on datatype constructors public DatatypeDecl EnclosingDatatype; // filled in during resolution public SpecialField QueryField; // filled in during resolution public List Destructors = new List(); // contents filled in during resolution public DatatypeCtor(IToken/*!*/ tok, string/*!*/ name, [Captured] List/*!*/ formals, Attributes attributes) : base(tok, name, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(formals)); this.Formals = formals; } public string FullName { get { Contract.Requires(EnclosingDatatype != null); Contract.Ensures(Contract.Result() != null); return "#" + EnclosingDatatype.FullName + "." + Name; } } } public abstract class MemberDecl : Declaration { public readonly bool IsStatic; public readonly bool IsGhost; public TopLevelDecl EnclosingClass; // filled in during resolution public MemberDecl(IToken tok, string name, bool isStatic, bool isGhost, Attributes attributes) : base(tok, name, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); IsStatic = isStatic; IsGhost = isGhost; } /// /// Returns className+"."+memberName. Available only after resolution. /// public string FullName { get { Contract.Requires(EnclosingClass != null); Contract.Ensures(Contract.Result() != null); return EnclosingClass.FullName + "." + Name; } } public string FullCompileName { get { Contract.Requires(EnclosingClass != null); Contract.Ensures(Contract.Result() != null); return EnclosingClass.FullCompileName + "." + CompileName; } } } public class Field : MemberDecl { public readonly bool IsMutable; public readonly Type Type; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Type != null); } public Field(IToken tok, string name, bool isGhost, Type type, Attributes attributes) : this(tok, name, isGhost, true, type, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(type != null); } public Field(IToken tok, string name, bool isGhost, bool isMutable, Type type, Attributes attributes) : base(tok, name, false, isGhost, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(type != null); IsMutable = isMutable; Type = type; } } public class SpecialField : Field { public readonly string CompiledName; public readonly string PreString; public readonly string PostString; public SpecialField(IToken tok, string name, string compiledName, string preString, string postString, bool isGhost, bool isMutable, Type type, Attributes attributes) : base(tok, name, isGhost, isMutable, type, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(compiledName != null); Contract.Requires(preString != null); Contract.Requires(postString != null); Contract.Requires(type != null); CompiledName = compiledName; PreString = preString; PostString = postString; } } public class DatatypeDestructor : SpecialField { public readonly DatatypeCtor EnclosingCtor; public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, string name, string compiledName, string preString, string postString, bool isGhost, Type type, Attributes attributes) : base(tok, name, compiledName, preString, postString, isGhost, false, type, attributes) { EnclosingCtor = enclosingCtor; } } public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType { public readonly TypeParameter TheType; public TypeParameter.EqualitySupportValue EqualitySupport { get { return TheType.EqualitySupport; } } public bool MustSupportEquality { get { return TheType.MustSupportEquality; } } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(TheType != null && Name == TheType.Name); } public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, TypeParameter.EqualitySupportValue equalitySupport, Attributes attributes) : base(tok, name, module, new List(), attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); TheType = new TypeParameter(tok, name, equalitySupport); } } [ContractClass(typeof(IVariableContracts))] public interface IVariable { string/*!*/ Name { get; } string/*!*/ UniqueName { get; } string/*!*/ CompileName { get; } Type/*!*/ Type { get; } bool IsMutable { get; } bool IsGhost { get; } } [ContractClassFor(typeof(IVariable))] public abstract class IVariableContracts : IVariable { public string Name { get { Contract.Ensures(Contract.Result() != null); throw new NotImplementedException(); } } public string UniqueName { get { Contract.Ensures(Contract.Result() != null); throw new NotImplementedException(); } } public string CompileName { get { Contract.Ensures(Contract.Result() != null); throw new NotImplementedException(); } } public Type Type { get { Contract.Ensures(Contract.Result() != null); throw new NotImplementedException(); } } public bool IsMutable { get { throw new NotImplementedException(); } } public bool IsGhost { get { throw new NotImplementedException(); } } } public abstract class NonglobalVariable : IVariable { public readonly IToken tok; readonly string name; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(tok != null); Contract.Invariant(name != null); Contract.Invariant(type != null); } public string Name { get { Contract.Ensures(Contract.Result() != null); return name; } } readonly int varId = varIdCount++; public string UniqueName { get { Contract.Ensures(Contract.Result() != null); return name + "#" + varId; } } static char[] specialChars = new char[] { '\'', '_', '?', '\\' }; public static string CompilerizeName(string nm) { string name = null; int i = 0; while (true) { int j = nm.IndexOfAny(specialChars, i); if (j == -1) { if (i == 0) { return nm; // this is the common case } else { return name + nm.Substring(i); } } else { string nxt = nm.Substring(i, j); name = name == null ? nxt : name + nxt; switch (nm[j]) { case '\'': name += "_k"; break; case '_': name += "__"; break; case '?': name += "_q"; break; case '\\': name += "_b"; break; default: Contract.Assume(false); // unexpected character break; } i = j + 1; if (i == nm.Length) { return name; } } } } protected string compileName; public virtual string CompileName { get { if (compileName == null) { compileName = string.Format("_{0}_{1}", varId, CompilerizeName(name)); } return compileName; } } Type type; //[Pure(false)] // TODO: if Type gets the status of [Frozen], then this attribute is not needed public Type/*!*/ Type { get { Contract.Ensures(Contract.Result() != null); return type.Normalize(); } } public abstract bool IsMutable { get; } bool isGhost; // readonly, except for BoundVar's of match expressions/statements during resolution public bool IsGhost { get { return isGhost; } set { isGhost = value; } } public NonglobalVariable(IToken tok, string name, Type type, bool isGhost) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(type != null); this.tok = tok; this.name = name; this.type = type; this.isGhost = isGhost; } internal static int varIdCount; // this varIdCount is used for both NonglobalVariable's and VarDecl's. } public class Formal : NonglobalVariable { public readonly bool InParam; // true to in-parameter, false for out-parameter public override bool IsMutable { get { return !InParam; } } public Formal(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type, bool inParam, bool isGhost) : base(tok, name, type, isGhost) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(type != null); InParam = inParam; } public bool HasName { get { return !Name.StartsWith("#"); } } public override string CompileName { get { if (compileName == null) { compileName = CompilerizeName(Name); } return compileName; } } } /// /// A "ThisSurrogate" is used during translation time to make the treatment of the receiver more similar to /// the treatment of other in-parameters. /// public class ThisSurrogate : Formal { public ThisSurrogate(IToken tok, Type type) : base(tok, "this", type, true, false) { Contract.Requires(tok != null); Contract.Requires(type != null); } } public class BoundVar : NonglobalVariable { public override bool IsMutable { get { return false; } } public BoundVar(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type) : base(tok, name, type, false) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(type != null); } } public class Function : MemberDecl, TypeParameter.ParentType { public bool IsRecursive; // filled in during resolution public readonly List/*!*/ TypeArgs; public readonly IToken OpenParen; // can be null (for predicates), if there are no formals public readonly List/*!*/ Formals; public readonly Type/*!*/ ResultType; public readonly List/*!*/ Req; public readonly List/*!*/ Reads; public readonly List/*!*/ Ens; public readonly Specification/*!*/ Decreases; public Expression Body; // an extended expression; Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution public readonly bool SignatureIsOmitted; // is "false" for all Function objects that survive into resolution [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(TypeArgs)); Contract.Invariant(cce.NonNullElements(Formals)); Contract.Invariant(ResultType != null); Contract.Invariant(cce.NonNullElements(Req)); Contract.Invariant(cce.NonNullElements(Reads)); Contract.Invariant(cce.NonNullElements(Ens)); Contract.Invariant(Decreases != null); } /// /// Note, functions are "ghost" by default; a non-ghost function is called a "function method". /// public Function(IToken tok, string name, bool isStatic, bool isGhost, List typeArgs, IToken openParen, List formals, Type resultType, List req, List reads, List ens, Specification decreases, Expression body, Attributes attributes, bool signatureOmitted) : base(tok, name, isStatic, isGhost, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Requires(cce.NonNullElements(formals)); Contract.Requires(resultType != null); Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(decreases != null); this.TypeArgs = typeArgs; this.OpenParen = openParen; this.Formals = formals; this.ResultType = resultType; this.Req = req; this.Reads = reads; this.Ens = ens; this.Decreases = decreases; this.Body = body; this.SignatureIsOmitted = signatureOmitted; } } public class Predicate : Function { public readonly bool BodyIsExtended; // says that this predicate definition is a refinement extension of a predicate definition is a refining module public Predicate(IToken tok, string name, bool isStatic, bool isGhost, List typeArgs, IToken openParen, List formals, List req, List reads, List ens, Specification decreases, Expression body, bool bodyIsExtended, Attributes attributes, bool signatureOmitted) : base(tok, name, isStatic, isGhost, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureOmitted) { Contract.Requires(!bodyIsExtended || body != null); BodyIsExtended = bodyIsExtended; } } public class Method : MemberDecl, TypeParameter.ParentType { public readonly bool SignatureIsOmitted; public readonly List/*!*/ TypeArgs; public readonly List/*!*/ Ins; public readonly List/*!*/ Outs; public readonly List/*!*/ Req; public readonly Specification/*!*/ Mod; public readonly List/*!*/ Ens; public readonly Specification/*!*/ Decreases; public BlockStmt Body; // Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(TypeArgs)); Contract.Invariant(cce.NonNullElements(Ins)); Contract.Invariant(cce.NonNullElements(Outs)); Contract.Invariant(cce.NonNullElements(Req)); Contract.Invariant(Mod != null); Contract.Invariant(cce.NonNullElements(Ens)); Contract.Invariant(Decreases != null); } public Method(IToken tok, string name, bool isStatic, bool isGhost, [Captured] List/*!*/ typeArgs, [Captured] List/*!*/ ins, [Captured] List/*!*/ outs, [Captured] List/*!*/ req, [Captured] Specification/*!*/ mod, [Captured] List/*!*/ ens, [Captured] Specification/*!*/ decreases, [Captured] BlockStmt body, Attributes attributes, bool signatureOmitted) : base(tok, name, isStatic, isGhost, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Requires(cce.NonNullElements(ins)); Contract.Requires(cce.NonNullElements(outs)); Contract.Requires(cce.NonNullElements(req)); Contract.Requires(mod != null); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(decreases != null); this.TypeArgs = typeArgs; this.Ins = ins; this.Outs = outs; this.Req = req; this.Mod = mod; this.Ens = ens; this.Decreases = decreases; this.Body = body; this.SignatureIsOmitted = signatureOmitted; } } public class Constructor : Method { public Constructor(IToken tok, string name, [Captured] List/*!*/ typeArgs, [Captured] List/*!*/ ins, [Captured] List/*!*/ req, [Captured] Specification/*!*/ mod, [Captured] List/*!*/ ens, [Captured] Specification/*!*/ decreases, [Captured] BlockStmt body, Attributes attributes, bool signatureOmitted) : base(tok, name, false, false, typeArgs, ins, new List(), req, mod, ens, decreases, body, attributes, signatureOmitted) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Requires(cce.NonNullElements(ins)); Contract.Requires(cce.NonNullElements(req)); Contract.Requires(mod != null); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(decreases != null); } } // ------------------------------------------------------------------------------------------------------ public abstract class Statement { public readonly IToken Tok; public LList