//----------------------------------------------------------------------------- // // Copyright (C) Microsoft Corporation. All Rights Reserved. // //----------------------------------------------------------------------------- using System; using System.Collections.Generic; using System.Linq; using System.Numerics; using System.Diagnostics.Contracts; using Microsoft.Boogie; namespace Microsoft.Dafny { public class Resolver { readonly BuiltIns builtIns; readonly ErrorReporter reporter; ModuleSignature moduleInfo = null; FreshIdGenerator defaultTempVarIdGenerator; string FreshTempVarName(string prefix, ICodeContext context) { var decl = context as Declaration; if (decl != null) { return decl.IdGenerator.FreshId(prefix); } // TODO(wuestholz): Is the following code ever needed? if (defaultTempVarIdGenerator == null) { defaultTempVarIdGenerator = new FreshIdGenerator(); } return defaultTempVarIdGenerator.FreshId(prefix); } interface IAmbiguousThing { /// /// Returns a plural number of non-null Thing's /// ISet Pool { get; } } class AmbiguousThingHelper where Thing : class { public static Thing Create(ModuleDefinition m, Thing a, Thing b, IEqualityComparer eq, out ISet s) { Contract.Requires(a != null); Contract.Requires(b != null); Contract.Requires(eq != null); Contract.Ensures(Contract.Result() != null || (Contract.ValueAtReturn(out s) != null || 2 <= Contract.ValueAtReturn(out s).Count)); s = null; if (eq.Equals(a, b)) { return a; } ISet sa = a is IAmbiguousThing ? ((IAmbiguousThing)a).Pool : new HashSet() { a }; ISet sb = b is IAmbiguousThing ? ((IAmbiguousThing)b).Pool : new HashSet() { b }; var union = new HashSet(sa.Union(sb, eq)); if (sa.Count == union.Count) { // sb is a subset of sa return a; } else if (sb.Count == union.Count) { // sa is a subset of sb return b; } else { s = union; Contract.Assert(2 <= s.Count); return null; } } public static string Name(ISet s, Func name) { Contract.Requires(s != null); Contract.Requires(s.Count != 0); string nm = null; foreach (var thing in s) { string n = name(thing); if (nm == null) { nm = n; } else { nm += "/" + n; } } return nm; } public static string ModuleNames(IAmbiguousThing amb, Func moduleName) { Contract.Requires(amb != null); Contract.Ensures(Contract.Result() != null); string nm = null; foreach (var d in amb.Pool) { if (nm == null) { nm = moduleName(d); } else { nm += ", " + moduleName(d); } } return nm; } } class AmbiguousTopLevelDecl : TopLevelDecl, IAmbiguousThing // only used with "classes" { public static TopLevelDecl Create(ModuleDefinition m, TopLevelDecl a, TopLevelDecl b) { ISet s; var t = AmbiguousThingHelper.Create(m, a, b, new Eq(), out s); return t ?? new AmbiguousTopLevelDecl(m, AmbiguousThingHelper.Name(s, tld => tld.Name), s); } class Eq : IEqualityComparer { public bool Equals(TopLevelDecl d0, TopLevelDecl d1) { // We'd like to resolve any AliasModuleDecl to whatever module they refer to. // It seems that the only way to do that is to look at alias.Signature.ModuleDef, // but that is a ModuleDefinition, which is not a TopLevelDecl. Therefore, we // convert to a ModuleDefinition anything that might refer to something that an // AliasModuleDecl can refer to; this is AliasModuleDecl and LiteralModuleDecl. object a = d0 is ModuleDecl ? ((ModuleDecl)d0).Dereference() : d0; object b = d1 is ModuleDecl ? ((ModuleDecl)d1).Dereference() : d1; return a == b; } public int GetHashCode(TopLevelDecl d) { object a = d is ModuleDecl ? ((ModuleDecl)d).Dereference() : d; return a.GetHashCode(); } } public override string WhatKind { get { return Pool.First().WhatKind; } } readonly ISet Pool = new HashSet(); ISet IAmbiguousThing.Pool { get { return Pool; } } private AmbiguousTopLevelDecl(ModuleDefinition m, string name, ISet pool) : base(pool.First().tok, name, m, new List(), null) { Contract.Requires(name != null); Contract.Requires(pool != null && 2 <= pool.Count); Pool = pool; } public string ModuleNames() { return AmbiguousThingHelper.ModuleNames(this, d => d.Module.Name); } } class AmbiguousMemberDecl : MemberDecl, IAmbiguousThing // only used with "classes" { public static MemberDecl Create(ModuleDefinition m, MemberDecl a, MemberDecl b) { ISet s; var t = AmbiguousThingHelper.Create(m, a, b, new Eq(), out s); return t ?? new AmbiguousMemberDecl(m, AmbiguousThingHelper.Name(s, member => member.Name), s); } class Eq : IEqualityComparer { public bool Equals(MemberDecl d0, MemberDecl d1) { return d0 == d1; } public int GetHashCode(MemberDecl d) { return d.GetHashCode(); } } public override string WhatKind { get { return Pool.First().WhatKind; } } readonly ISet Pool = new HashSet(); ISet IAmbiguousThing.Pool { get { return Pool; } } private AmbiguousMemberDecl(ModuleDefinition m, string name, ISet pool) : base(pool.First().tok, name, true, pool.First().IsGhost, null) { Contract.Requires(name != null); Contract.Requires(pool != null && 2 <= pool.Count); Pool = pool; } public string ModuleNames() { return AmbiguousThingHelper.ModuleNames(this, d => d.EnclosingClass.Module.Name); } } readonly Dictionary> classMembers = new Dictionary>(); readonly Dictionary> datatypeMembers = new Dictionary>(); readonly Dictionary> datatypeCtors = new Dictionary>(); enum BasicTypeVariety { Bool = 0, Int, Real, None } // note, these are ordered, so they can be used as indices into basicTypeMembers readonly Dictionary[] basicTypeMembers = new Dictionary[] { new Dictionary(), new Dictionary(), new Dictionary() }; readonly Graph dependencies = new Graph(); private ModuleSignature systemNameInfo = null; private bool useCompileSignatures = false; public Resolver(Program prog) { Contract.Requires(prog != null); builtIns = prog.BuiltIns; reporter = prog.reporter; // Populate the members of the basic types var trunc = new SpecialField(Token.NoToken, "Trunc", "ToBigInteger()", "", "", false, false, false, Type.Int, null); basicTypeMembers[(int)BasicTypeVariety.Real].Add(trunc.Name, trunc); } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(builtIns != null); Contract.Invariant(cce.NonNullElements(dependencies)); Contract.Invariant(cce.NonNullDictionaryAndValues(classMembers) && Contract.ForAll(classMembers.Values, v => cce.NonNullDictionaryAndValues(v))); Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v))); } /// /// Check that now two modules that are being compiled have the same CompileName. /// /// This could happen if they are given the same name using the 'extern' declaration modifier. /// /// The Dafny program being compiled. void CheckDupModuleNames(Program prog) { // Check that none of the modules have the same CompileName. Dictionary compileNameMap = new Dictionary(); foreach (ModuleDefinition m in prog.CompileModules) { if (m.IsAbstract) { // the purpose of an abstract module is to skip compilation continue; } string compileName = m.CompileName; ModuleDefinition priorModDef; if (compileNameMap.TryGetValue(compileName, out priorModDef)) { reporter.Error(MessageSource.Resolver, m.tok, "Modules '{0}' and '{1}' both have CompileName '{2}'.", priorModDef.tok.val, m.tok.val, compileName); } else { compileNameMap.Add(compileName, m); } } } public void ResolveProgram(Program prog) { Contract.Requires(prog != null); var origErrorCount = reporter.Count(ErrorLevel.Error); //TODO: This is used further below, but not in the >0 comparisons in the next few lines. Is that right? var bindings = new ModuleBindings(null); var b = BindModuleNames(prog.DefaultModuleDef, bindings); bindings.BindName("_module", prog.DefaultModule, b); if (reporter.Count(ErrorLevel.Error) > 0) { return; } // if there were errors, then the implict ModuleBindings data structure invariant // is violated, so Processing dependencies will not succeed. ProcessDependencies(prog.DefaultModule, b, dependencies); // check for cycles in the import graph List cycle = dependencies.TryFindCycle(); if (cycle != null) { var cy = Util.Comma(" -> ", cycle, m => m.Name); reporter.Error(MessageSource.Resolver, cycle[0], "module definition contains a cycle (note: parent modules implicitly depend on submodules): {0}", cy); } if (reporter.Count(ErrorLevel.Error) > 0) { return; } // give up on trying to resolve anything else // fill in module heights List sortedDecls = dependencies.TopologicallySortedComponents(); int h = 0; foreach (ModuleDecl m in sortedDecls) { m.Height = h; if (m is LiteralModuleDecl) { var mdef = ((LiteralModuleDecl)m).ModuleDef; mdef.Height = h; prog.Modules.Add(mdef); } h++; } var rewriters = new List(); var refinementTransformer = new RefinementTransformer(prog); rewriters.Add(refinementTransformer); rewriters.Add(new AutoContractsRewriter(reporter)); var opaqueRewriter = new OpaqueFunctionRewriter(this.reporter); rewriters.Add(new AutoReqFunctionRewriter(this.reporter, opaqueRewriter)); rewriters.Add(opaqueRewriter); rewriters.Add(new TimeLimitRewriter(reporter)); rewriters.Add(new ForallStmtRewriter(reporter)); if (DafnyOptions.O.AutoTriggers) { rewriters.Add(new QuantifierSplittingRewriter(reporter)); rewriters.Add(new TriggerGeneratingRewriter(reporter)); } rewriters.Add(new InductionRewriter(reporter)); systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false); prog.CompileModules.Add(prog.BuiltIns.SystemModule); // first, we need to detect which top-level modules have exclusive refinement relationships. foreach (ModuleDecl decl in sortedDecls) { if (decl is LiteralModuleDecl) { var literalDecl = (LiteralModuleDecl)decl; var m = literalDecl.ModuleDef; if (m.RefinementBaseRoot != null) { if (m.IsExclusiveRefinement) { foreach (var d in sortedDecls) { // refinement dependencies won't be later in the sorted module list than the one we're looking at. if (Object.ReferenceEquals(d, decl)) { break; } if (d is LiteralModuleDecl) { var ld = (LiteralModuleDecl)d; // currently, only exclusive refinements of top-level modules are supported. if (string.Equals(m.RefinementBaseName[0].val, m.RefinementBaseRoot.Name, StringComparison.InvariantCulture) && string.Equals(m.RefinementBaseName[0].val, ld.ModuleDef.Name, StringComparison.InvariantCulture)) { ld.ModuleDef.ExclusiveRefinementCount += 1; } } } } } } } foreach (var decl in sortedDecls) { if (decl is LiteralModuleDecl) { // The declaration is a literal module, so it has members and such that we need // to resolve. First we do refinement transformation. Then we construct the signature // of the module. This is the public, externally visible signature. Then we add in // everything that the system defines, as well as any "import" (i.e. "opened" modules) // directives (currently not supported, but this is where we would do it.) This signature, // which is only used while resolving the members of the module is stored in the (basically) // global variable moduleInfo. Then the signatures of the module members are resolved, followed // by the bodies. var literalDecl = (LiteralModuleDecl)decl; var m = literalDecl.ModuleDef; var errorCount = reporter.Count(ErrorLevel.Error); foreach (var r in rewriters) { r.PreResolve(m); } literalDecl.Signature = RegisterTopLevelDecls(m, true); literalDecl.Signature.Refines = refinementTransformer.RefinedSig; var sig = literalDecl.Signature; // set up environment var preResolveErrorCount = reporter.Count(ErrorLevel.Error); ResolveModuleDefinition(m, sig); ResolveModuleExport(literalDecl, sig); foreach (var r in rewriters) { if (reporter.Count(ErrorLevel.Error) != preResolveErrorCount) { break; } r.PostResolve(m); } if (reporter.Count(ErrorLevel.Error) == errorCount && !m.IsAbstract) { // compilation should only proceed if everything is good, including the signature (which preResolveErrorCount does not include); Contract.Assert(!useCompileSignatures); useCompileSignatures = true; // set Resolver-global flag to indicate that Signatures should be followed to their CompiledSignature var oldErrorsOnly = reporter.ErrorsOnly; reporter.ErrorsOnly = true; // turn off warning reporting for the clone var nw = new Cloner().CloneModuleDefinition(m, m.CompileName + "_Compile"); var compileSig = RegisterTopLevelDecls(nw, true); compileSig.Refines = refinementTransformer.RefinedSig; sig.CompileSignature = compileSig; ResolveModuleDefinition(nw, compileSig); prog.CompileModules.Add(nw); useCompileSignatures = false; // reset the flag reporter.ErrorsOnly = oldErrorsOnly; } } else if (decl is AliasModuleDecl) { var alias = (AliasModuleDecl)decl; // resolve the path ModuleSignature p; if (ResolvePath(alias.Root, alias.Path, out p, reporter)) { alias.Signature = p; } else { alias.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature } } else if (decl is ModuleFacadeDecl) { var abs = (ModuleFacadeDecl)decl; ModuleSignature p; if (ResolvePath(abs.Root, abs.Path, out p, reporter)) { abs.OriginalSignature = p; // ModuleDefinition.ExclusiveRefinement may not be set at this point but ExclusiveRefinementCount will be. if (0 == abs.Root.Signature.ModuleDef.ExclusiveRefinementCount) { abs.Signature = MakeAbstractSignature(p, abs.FullCompileName, abs.Height, prog.Modules); ModuleSignature compileSig; if (abs.CompilePath != null) { if (ResolvePath(abs.CompileRoot, abs.CompilePath, out compileSig, reporter)) { if (refinementTransformer.CheckIsRefinement(compileSig, p)) { abs.Signature.CompileSignature = compileSig; } else { reporter.Error(MessageSource.Resolver, abs.CompilePath[0], "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of " + Util.Comma(".", abs.Path, x => x.val)); } abs.Signature.IsAbstract = compileSig.IsAbstract; // always keep the ghost information, to supress a spurious error message when the compile module isn't actually a refinement } } } else { abs.Signature = p; } } else { abs.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature } } else if (decl is ModuleExportDecl) { ModuleExportDecl export = (ModuleExportDecl)decl; export.Signature = new ModuleSignature(); export.Signature.IsAbstract = false; export.Signature.ModuleDef = null; } else { Contract.Assert(false); } Contract.Assert(decl.Signature != null); } if (reporter.Count(ErrorLevel.Error) != origErrorCount) { // do nothing else return; } // compute IsRecursive bit for mutually recursive functions and methods foreach (var module in prog.Modules) { foreach (var clbl in ModuleDefinition.AllCallables(module.TopLevelDecls)) { if (clbl is Function) { var fn = (Function)clbl; if (!fn.IsRecursive) { // note, self-recursion has already been determined int n = module.CallGraph.GetSCCSize(fn); if (2 <= n) { // the function is mutually recursive (note, the SCC does not determine self recursion) fn.IsRecursive = true; } } if (fn.IsRecursive && fn is FixpointPredicate) { // this means the corresponding prefix predicate is also recursive var prefixPred = ((FixpointPredicate)fn).PrefixPredicate; if (prefixPred != null) { prefixPred.IsRecursive = true; } } } else { var m = (Method)clbl; if (!m.IsRecursive) { // note, self-recursion has already been determined int n = module.CallGraph.GetSCCSize(m); if (2 <= n) { // the function is mutually recursive (note, the SCC does not determine self recursion) m.IsRecursive = true; } } } } foreach (var r in rewriters) { r.PostCyclicityResolve(module); } } // fill in default decreases clauses: for functions and methods, and for loops FillInDefaultDecreasesClauses(prog); foreach (var module in prog.Modules) { foreach (var clbl in ModuleDefinition.AllItersAndCallables(module.TopLevelDecls)) { Statement body = null; if (clbl is Method) { body = ((Method)clbl).Body; } else if (clbl is IteratorDecl) { body = ((IteratorDecl)clbl).Body; } if (body != null) { var c = new FillInDefaultLoopDecreases_Visitor(this, clbl); c.Visit(body); } } } foreach (var module in prog.Modules) { foreach (var iter in ModuleDefinition.AllIteratorDecls(module.TopLevelDecls)) { reporter.Info(MessageSource.Resolver, iter.tok, Printer.IteratorClassToString(iter)); } } // fill in other additional information foreach (var module in prog.Modules) { foreach (var clbl in ModuleDefinition.AllItersAndCallables(module.TopLevelDecls)) { Statement body = null; if (clbl is Method) { body = ((Method)clbl).Body; } else if (clbl is IteratorDecl) { body = ((IteratorDecl)clbl).Body; } if (body != null) { var c = new ReportOtherAdditionalInformation_Visitor(this); c.Visit(body); } } } // Determine, for each function, whether someone tries to adjust its fuel parameter foreach (var module in prog.Modules) { CheckForFuelAdjustments(module.tok, module.Attributes, module); foreach (var clbl in ModuleDefinition.AllItersAndCallables(module.TopLevelDecls)) { Statement body = null; if (clbl is Method) { body = ((Method)clbl).Body; CheckForFuelAdjustments(clbl.Tok,((Method)clbl).Attributes, module); } else if (clbl is IteratorDecl) { body = ((IteratorDecl)clbl).Body; CheckForFuelAdjustments(clbl.Tok, ((IteratorDecl)clbl).Attributes, module); } else if (clbl is Function) { CheckForFuelAdjustments(clbl.Tok, ((Function)clbl).Attributes, module); var c = new FuelAdjustment_Visitor(this); var bodyExpr = ((Function)clbl).Body; if (bodyExpr != null) { c.Visit(bodyExpr, new FuelAdjustment_Context(module)); } } if (body != null) { var c = new FuelAdjustment_Visitor(this); c.Visit(body, new FuelAdjustment_Context(module)); } } } CheckDupModuleNames(prog); } void FillInDefaultDecreasesClauses(Program prog) { Contract.Requires(prog != null); foreach (var module in prog.Modules) { foreach (var clbl in ModuleDefinition.AllCallables(module.TopLevelDecls)) { ICallable m; string s; if (clbl is FixpointLemma) { var prefixLemma = ((FixpointLemma)clbl).PrefixLemma; m = prefixLemma; s = prefixLemma.Name + " "; } else { m = clbl; s = ""; } var anyChangeToDecreases = FillInDefaultDecreases(m, true); if (anyChangeToDecreases || m.InferredDecreases || m is PrefixLemma) { bool showIt = false; if (m is Function) { // show the inferred decreases clause only if it will ever matter, i.e., if the function is recursive showIt = ((Function)m).IsRecursive; } else if (m is PrefixLemma) { // always show the decrease clause, since at the very least it will start with "_k", which the programmer did not write explicitly showIt = true; } else { showIt = ((Method)m).IsRecursive; } if (showIt) { s += "decreases " + Util.Comma(", ", m.Decreases.Expressions, Printer.ExprToString); // Note, in the following line, we use the location information for "clbl", not "m". These // are the same, except in the case where "clbl" is a CoLemma and "m" is a prefix lemma. reporter.Info(MessageSource.Resolver, clbl.Tok, s); } } } } } /// /// Return "true" if this routine makes any change to the decreases clause. If the decreases clause /// starts off essentially empty and a default is provided, then clbl.InferredDecreases is also set /// to true. /// bool FillInDefaultDecreases(ICallable clbl, bool addPrefixInCoClusters) { Contract.Requires(clbl != null); if (clbl is FixpointPredicate) { // fixpoint-predicates don't have decreases clauses return false; } var anyChangeToDecreases = false; var decr = clbl.Decreases.Expressions; if (DafnyOptions.O.Dafnycc) { if (decr.Count > 1) { reporter.Error(MessageSource.Resolver, decr[1].tok, "In dafnycc mode, only one decreases expression is allowed"); } // In dafnycc mode, only consider first argument if (decr.Count == 0 && clbl.Ins.Count > 0) { var p = clbl.Ins[0]; if (!(p is ImplicitFormal) && p.Type.IsOrdered) { var ie = new IdentifierExpr(p.tok, p.Name); ie.Var = p; ie.Type = p.Type; // resolve it here decr.Add(ie); return true; } } return false; } if (decr.Count == 0 || (clbl is PrefixLemma && decr.Count == 1)) { // The default for a function starts with the function's reads clause, if any if (clbl is Function) { var fn = (Function)clbl; if (fn.Reads.Count != 0) { // start the default lexicographic tuple with the reads clause var r = FrameToObjectSet(fn.Reads); decr.Add(AutoGeneratedExpression.Create(r)); anyChangeToDecreases = true; } } // Add one component for each parameter, unless the parameter's type is one that // doesn't appear useful to orderings. foreach (var p in clbl.Ins) { if (!(p is ImplicitFormal) && p.Type.IsOrdered) { var ie = new IdentifierExpr(p.tok, p.Name); ie.Var = p; ie.Type = p.Type; // resolve it here decr.Add(AutoGeneratedExpression.Create(ie)); anyChangeToDecreases = true; } } clbl.InferredDecreases = true; // this indicates that finding a default decreases clause was attempted } if (addPrefixInCoClusters && clbl is Function) { var fn = (Function)clbl; switch (fn.CoClusterTarget) { case Function.CoCallClusterInvolvement.None: break; case Function.CoCallClusterInvolvement.IsMutuallyRecursiveTarget: // prefix: decreases 0, clbl.Decreases.Expressions.Insert(0, Expression.CreateIntLiteral(fn.tok, 0)); anyChangeToDecreases = true; break; case Function.CoCallClusterInvolvement.CoRecursiveTargetAllTheWay: // prefix: decreases 1, clbl.Decreases.Expressions.Insert(0, Expression.CreateIntLiteral(fn.tok, 1)); anyChangeToDecreases = true; break; default: Contract.Assume(false); // unexpected case break; } } return anyChangeToDecreases; } public static Expression FrameArrowToObjectSet(Expression e, FreshIdGenerator idGen) { var arrTy = e.Type.AsArrowType; if (arrTy != null) { var bvars = new List(); var bexprs = new List(); foreach (var t in arrTy.Args) { var bv = new BoundVar(e.tok, idGen.FreshId("_x"), t); bvars.Add(bv); bexprs.Add(new IdentifierExpr(e.tok, bv.Name) { Type = bv.Type, Var = bv }); } var oVar = new BoundVar(e.tok, idGen.FreshId("_o"), new ObjectType()); var obj = new IdentifierExpr(e.tok, oVar.Name) { Type = oVar.Type, Var = oVar }; bvars.Add(oVar); return new SetComprehension(e.tok, true, bvars, new BinaryExpr(e.tok, BinaryExpr.Opcode.In, obj, new ApplyExpr(e.tok, e, bexprs) { Type = new SetType(true, new ObjectType()) }) { ResolvedOp = BinaryExpr.ResolvedOpcode.InSet, Type = Type.Bool }, obj, null) { Type = new SetType(true, new ObjectType()) }; } else { return e; } } public static Expression FrameToObjectSet(List fexprs) { Contract.Requires(fexprs != null); Contract.Ensures(Contract.Result() != null); List sets = new List(); List singletons = null; var idGen = new FreshIdGenerator(); foreach (FrameExpression fe in fexprs) { Contract.Assert(fe != null); if (fe.E is WildcardExpr) { // drop wildcards altogether } else { Expression e = FrameArrowToObjectSet(fe.E, idGen); // keep only fe.E, drop any fe.Field designation Contract.Assert(e.Type != null); // should have been resolved already var eType = e.Type.NormalizeExpand(); if (eType.IsRefType) { // e represents a singleton set if (singletons == null) { singletons = new List(); } singletons.Add(e); } else if (eType is SeqType) { // e represents a sequence // Add: set x :: x in e var bv = new BoundVar(e.tok, idGen.FreshId("_s2s_"), ((SeqType)eType).Arg); var bvIE = new IdentifierExpr(e.tok, bv.Name); bvIE.Var = bv; // resolve here bvIE.Type = bv.Type; // resolve here var sInE = new BinaryExpr(e.tok, BinaryExpr.Opcode.In, bvIE, e); sInE.ResolvedOp = BinaryExpr.ResolvedOpcode.InSeq; // resolve here sInE.Type = Type.Bool; // resolve here var s = new SetComprehension(e.tok, true, new List() { bv }, sInE, bvIE, null); s.Type = new SetType(true, new ObjectType()); // resolve here sets.Add(s); } else { // e is already a set Contract.Assert(eType is SetType); sets.Add(e); } } } if (singletons != null) { Expression display = new SetDisplayExpr(singletons[0].tok, true, singletons); display.Type = new SetType(true, new ObjectType()); // resolve here sets.Add(display); } if (sets.Count == 0) { Expression emptyset = new SetDisplayExpr(Token.NoToken, true, new List()); emptyset.Type = new SetType(true, new ObjectType()); // resolve here return emptyset; } else { Expression s = sets[0]; for (int i = 1; i < sets.Count; i++) { BinaryExpr union = new BinaryExpr(s.tok, BinaryExpr.Opcode.Add, s, sets[i]); union.ResolvedOp = BinaryExpr.ResolvedOpcode.Union; // resolve here union.Type = new SetType(true, new ObjectType()); // resolve here s = union; } return s; } } private void ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) { Contract.Requires(AllTypeConstraints.Count == 0); Contract.Ensures(AllTypeConstraints.Count == 0); moduleInfo = MergeSignature(sig, systemNameInfo); // resolve var datatypeDependencies = new Graph(); var codatatypeDependencies = new Graph(); int prevErrorCount = reporter.Count(ErrorLevel.Error); ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies, codatatypeDependencies); Contract.Assert(AllTypeConstraints.Count == 0); // signature resolution does not add any type constraints ResolveAttributes(m.Attributes, new ResolveOpts(new NoContext(m.Module), false)); // Must follow ResolveTopLevelDecls_Signatures, in case attributes refer to members SolveAllTypeConstraints(); // solve any type constraints entailed by the attributes if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { ResolveTopLevelDecls_Core(m.TopLevelDecls, datatypeDependencies, codatatypeDependencies); } } // Resolve the exports and detect cycles. private void ResolveModuleExport(LiteralModuleDecl literalDecl, ModuleSignature sig) { ModuleDefinition m = literalDecl.ModuleDef; literalDecl.DefaultExport = sig; Graph exportDependencies = new Graph(); foreach (TopLevelDecl toplevel in m.TopLevelDecls) { if (toplevel is ModuleExportDecl) { ModuleExportDecl d = (ModuleExportDecl) toplevel; exportDependencies.AddVertex(d); foreach (string s in d.Extends) { TopLevelDecl top; if (sig.TopLevels.TryGetValue(s, out top) && top is ModuleExportDecl) { ModuleExportDecl extend = (ModuleExportDecl) top; d.ExtendDecls.Add(extend); exportDependencies.AddEdge(d, extend); } else { reporter.Error(MessageSource.Resolver, m.tok, s + " must be an export of" + m + " to be extended"); } } foreach (ExportSignature export in d.Exports) { // check to see if it is a datatype or a member or // static function or method in the enclosing module or its imports TopLevelDecl decl; MemberDecl member; string name = export.Name; if (sig.TopLevels.TryGetValue(name, out decl)) { // Member of the enclosing module export.Decl = decl; } else if (sig.StaticMembers.TryGetValue(name, out member)) { export.Decl = member; } else { reporter.Error(MessageSource.Resolver, d.tok, name + " must be a member of " + m + " to be exported"); } } } } // detect cycles in the extend var cycle = exportDependencies.TryFindCycle(); if (cycle != null) { var cy = Util.Comma(" -> ", cycle, c => c.Name); reporter.Error(MessageSource.Resolver, cycle[0], "module export contains a cycle: {0}", cy); return; } // fill in the exports for the extends. List sortedDecls = exportDependencies.TopologicallySortedComponents(); ModuleExportDecl defaultExport = null; foreach (ModuleExportDecl decl in sortedDecls) { if (decl.IsDefault) { if (defaultExport == null) { defaultExport = decl; } else { reporter.Error(MessageSource.Resolver, m.tok, "more than one default export declared: {0}, {1}", defaultExport, decl); } } // fill in export signature ModuleSignature signature = decl.Signature; foreach (ModuleExportDecl extend in decl.ExtendDecls) { ModuleSignature s = extend.Signature; foreach (var kv in s.TopLevels) { if (!signature.TopLevels.ContainsKey(kv.Key)) { signature.TopLevels.Add(kv.Key, kv.Value); } } foreach (var kv in s.Ctors) { if (!signature.Ctors.ContainsKey(kv.Key)) { signature.Ctors.Add(kv.Key, kv.Value); } } foreach (var kv in s.StaticMembers) { if (!signature.StaticMembers.ContainsKey(kv.Key)) { signature.StaticMembers.Add(kv.Key, kv.Value); } } } foreach (ExportSignature export in decl.Exports) { if (export.Decl is TopLevelDecl) { signature.TopLevels.Add(export.Name, (TopLevelDecl)export.Decl); } else if (export.Decl is MemberDecl) { signature.StaticMembers.Add(export.Name, (MemberDecl)export.Decl); } } } // set the default export if it exists, otherwise, default is export everything if (defaultExport != null) { literalDecl.DefaultExport = defaultExport.Signature; } } public class ModuleBindings { private ModuleBindings parent; private Dictionary modules; private Dictionary bindings; public ModuleBindings(ModuleBindings p) { parent = p; modules = new Dictionary(); bindings = new Dictionary(); } public bool BindName(string name, ModuleDecl subModule, ModuleBindings b) { if (modules.ContainsKey(name)) { return false; } else { modules.Add(name, subModule); bindings.Add(name, b); return true; } } public bool TryLookup(IToken name, out ModuleDecl m) { Contract.Requires(name != null); if (modules.TryGetValue(name.val, out m)) { return true; } else if (parent != null) { return parent.TryLookup(name, out m); } else return false; } public bool TryLookupIgnore(IToken name, out ModuleDecl m, ModuleDecl ignore) { Contract.Requires(name != null); if (modules.TryGetValue(name.val, out m) && m != ignore) { return true; } else if (parent != null) { return parent.TryLookup(name, out m); } else return false; } public IEnumerable ModuleList { get { return modules.Values; } } public ModuleBindings SubBindings(string name) { ModuleBindings v = null; bindings.TryGetValue(name, out v); return v; } } private ModuleBindings BindModuleNames(ModuleDefinition moduleDecl, ModuleBindings parentBindings) { var bindings = new ModuleBindings(parentBindings); foreach (var tld in moduleDecl.TopLevelDecls) { if (tld is LiteralModuleDecl) { var subdecl = (LiteralModuleDecl)tld; var subBindings = BindModuleNames(subdecl.ModuleDef, bindings); if (!bindings.BindName(subdecl.Name, subdecl, subBindings)) { reporter.Error(MessageSource.Resolver, subdecl.tok, "Duplicate module name: {0}", subdecl.Name); } } else if (tld is ModuleFacadeDecl) { var subdecl = (ModuleFacadeDecl)tld; if (!bindings.BindName(subdecl.Name, subdecl, null)) { reporter.Error(MessageSource.Resolver, subdecl.tok, "Duplicate module name: {0}", subdecl.Name); } } else if (tld is AliasModuleDecl) { var subdecl = (AliasModuleDecl)tld; if (!bindings.BindName(subdecl.Name, subdecl, null)) { reporter.Error(MessageSource.Resolver, subdecl.tok, "Duplicate module name: {0}", subdecl.Name); } } } return bindings; } private void ProcessDependenciesDefinition(ModuleDecl decl, ModuleDefinition m, ModuleBindings bindings, Graph dependencies) { if (m.RefinementBaseName != null) { ModuleDecl other; if (!bindings.TryLookup(m.RefinementBaseName[0], out other)) { reporter.Error(MessageSource.Resolver, m.RefinementBaseName[0], "module {0} named as refinement base does not exist", m.RefinementBaseName[0].val); } else if (other is LiteralModuleDecl && ((LiteralModuleDecl)other).ModuleDef == m) { reporter.Error(MessageSource.Resolver, m.RefinementBaseName[0], "module cannot refine itself: {0}", m.RefinementBaseName[0].val); } else { Contract.Assert(other != null); // follows from postcondition of TryGetValue dependencies.AddEdge(decl, other); m.RefinementBaseRoot = other; } } foreach (var toplevel in m.TopLevelDecls) { if (toplevel is ModuleDecl) { var d = (ModuleDecl)toplevel; dependencies.AddEdge(decl, d); var subbindings = bindings.SubBindings(d.Name); ProcessDependencies(d, subbindings ?? bindings, dependencies); } } } private void ProcessDependencies(ModuleDecl moduleDecl, ModuleBindings bindings, Graph dependencies) { dependencies.AddVertex(moduleDecl); if (moduleDecl is LiteralModuleDecl) { ProcessDependenciesDefinition(moduleDecl, ((LiteralModuleDecl)moduleDecl).ModuleDef, bindings, dependencies); } else if (moduleDecl is AliasModuleDecl) { var alias = moduleDecl as AliasModuleDecl; ModuleDecl root; if (!bindings.TryLookupIgnore(alias.Path[0], out root, alias)) reporter.Error(MessageSource.Resolver, alias.tok, ModuleNotFoundErrorMessage(0, alias.Path)); else { dependencies.AddEdge(moduleDecl, root); alias.Root = root; } } else if (moduleDecl is ModuleFacadeDecl) { var abs = moduleDecl as ModuleFacadeDecl; ModuleDecl root; if (!bindings.TryLookup(abs.Path[0], out root)) reporter.Error(MessageSource.Resolver, abs.tok, ModuleNotFoundErrorMessage(0, abs.Path)); else { dependencies.AddEdge(moduleDecl, root); abs.Root = root; } if (abs.CompilePath != null) { if (!bindings.TryLookup(abs.CompilePath[0], out root)) reporter.Error(MessageSource.Resolver, abs.tok, ModuleNotFoundErrorMessage(0, abs.CompilePath)); else { dependencies.AddEdge(moduleDecl, root); abs.CompileRoot = root; } } } } private static string ModuleNotFoundErrorMessage(int i, List path) { Contract.Requires(path != null); Contract.Requires(0 <= i && i < path.Count); return "module " + path[i].val + " does not exist" + (1 < path.Count ? " (position " + i.ToString() + " in path " + Util.Comma(".", path, x => x.val) + ")" : ""); } public static ModuleSignature MergeSignature(ModuleSignature m, ModuleSignature system) { var info = new ModuleSignature(); // add the system-declared information, among which we know there are no duplicates foreach (var kv in system.TopLevels) { info.TopLevels.Add(kv.Key, kv.Value); } foreach (var kv in system.Ctors) { info.Ctors.Add(kv.Key, kv.Value); } // add for the module itself foreach (var kv in m.TopLevels) { info.TopLevels[kv.Key] = kv.Value; } foreach (var kv in m.Ctors) { info.Ctors[kv.Key] = kv.Value; } foreach (var kv in m.StaticMembers) { info.StaticMembers[kv.Key] = kv.Value; } info.IsAbstract = m.IsAbstract; return info; } ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImports) { Contract.Requires(moduleDef != null); var sig = new ModuleSignature(); sig.ModuleDef = moduleDef; sig.IsAbstract = moduleDef.IsAbstract; List declarations = moduleDef.TopLevelDecls; // First go through and add anything from the opened imports foreach (var im in declarations) { if (im is ModuleDecl && ((ModuleDecl)im).Opened) { var s = GetSignature(((ModuleDecl)im).Signature); if (useImports || DafnyOptions.O.IronDafny) { // classes: foreach (var kv in s.TopLevels) { // IronDafny: we need to pull the members of the opened module's _default class in so that they can be merged. if (useImports || string.Equals(kv.Key, "_default", StringComparison.InvariantCulture)) { TopLevelDecl d; if (sig.TopLevels.TryGetValue(kv.Key, out d)) { bool resolved = false; if (DafnyOptions.O.IronDafny) { // sometimes, we need to compare two type synonyms in order to come up with a decision regarding substitution. var aliased1 = Object.ReferenceEquals(kv.Value, d); if (!aliased1) { var a = d; while (a.ExclusiveRefinement != null) { a = a.ExclusiveRefinement; } var b = kv.Value; while (b.ExclusiveRefinement != null) { b = b.ExclusiveRefinement; } if (a is TypeSynonymDecl && b is TypeSynonymDecl) { aliased1 = UnifyTypes(((TypeSynonymDecl)a).Rhs, ((TypeSynonymDecl)b).Rhs); } else { aliased1 = Object.ReferenceEquals(a, b); } } if (aliased1 || Object.ReferenceEquals(kv.Value.ClonedFrom, d) || Object.ReferenceEquals(d.ClonedFrom, kv.Value) || Object.ReferenceEquals(kv.Value.ExclusiveRefinement, d)) { sig.TopLevels[kv.Key] = kv.Value; resolved = true; } } if (!resolved) { sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value); } } else { sig.TopLevels.Add(kv.Key, kv.Value); } } } } if (useImports) { // constructors: foreach (var kv in s.Ctors) { Tuple pair; if (sig.Ctors.TryGetValue(kv.Key, out pair)) { // The same ctor can be imported from two different imports (e.g "diamond" imports), in which case, // they are not duplicates. if (!Object.ReferenceEquals(kv.Value.Item1, pair.Item1) && (!DafnyOptions.O.IronDafny || (!Object.ReferenceEquals(kv.Value.Item1.ClonedFrom, pair.Item1) && !Object.ReferenceEquals(kv.Value.Item1, pair.Item1.ClonedFrom)))) { // mark it as a duplicate sig.Ctors[kv.Key] = new Tuple(pair.Item1, true); } } else { // add new sig.Ctors.Add(kv.Key, kv.Value); } } } if (useImports || DafnyOptions.O.IronDafny) { // static members: foreach (var kv in s.StaticMembers) { MemberDecl md; if (sig.StaticMembers.TryGetValue(kv.Key, out md)) { var resolved = false; if (DafnyOptions.O.IronDafny) { var aliased0 = Object.ReferenceEquals(kv.Value, md) || Object.ReferenceEquals(kv.Value.ClonedFrom, md) || Object.ReferenceEquals(md.ClonedFrom, kv.Value); var aliased1 = aliased0; if (!aliased0) { var a = kv.Value.EnclosingClass; while (a != null && (a.ExclusiveRefinement != null || a.ClonedFrom != null)) { if (a.ClonedFrom != null) { a = (TopLevelDecl)a.ClonedFrom; } else { Contract.Assert(a.ExclusiveRefinement != null); a = a.ExclusiveRefinement; } } var b = md.EnclosingClass; while (b != null && (b.ExclusiveRefinement != null || b.ClonedFrom != null)) { if (b.ClonedFrom != null) { b = (TopLevelDecl)b.ClonedFrom; } else { Contract.Assert(b.ExclusiveRefinement != null); b = b.ExclusiveRefinement; } } aliased1 = Object.ReferenceEquals(a, b); } if (aliased0 || aliased1) { if (kv.Value.EnclosingClass != null && md.EnclosingClass != null && md.EnclosingClass.ExclusiveRefinement != null && !Object.ReferenceEquals( kv.Value.EnclosingClass.ExclusiveRefinement, md.EnclosingClass)) { sig.StaticMembers[kv.Key] = kv.Value; } resolved = true; } } if (!resolved) { sig.StaticMembers[kv.Key] = AmbiguousMemberDecl.Create(moduleDef, md, kv.Value); } } else { // add new sig.StaticMembers.Add(kv.Key, kv.Value); } } } } } // second go through and overriding anything from the opened imports with the ones from the refinementBase if (useImports && moduleDef.RefinementBaseSig != null) { foreach (var kv in moduleDef.RefinementBaseSig.TopLevels) { sig.TopLevels[kv.Key] = kv.Value; } foreach (var kv in moduleDef.RefinementBaseSig.StaticMembers) { sig.StaticMembers[kv.Key] = kv.Value; } } // This is solely used to detect duplicates amongst the various e Dictionary toplevels = new Dictionary(); // Now add the things present foreach (TopLevelDecl d in declarations) { Contract.Assert(d != null); // register the class/datatype/module name if (toplevels.ContainsKey(d.Name)) { reporter.Error(MessageSource.Resolver, d, "Duplicate name of top-level declaration: {0}", d.Name); } else { toplevels[d.Name] = d; sig.TopLevels[d.Name] = d; } if (d is ModuleDecl) { // nothing to do } else if (d is OpaqueTypeDecl) { // nothing more to register } else if (d is TypeSynonymDecl) { // nothing more to register } else if (d is NewtypeDecl) { // nothing more to register } else if (d is IteratorDecl) { var iter = (IteratorDecl)d; // register the names of the implicit members var members = new Dictionary(); classMembers.Add(iter, members); // First, register the iterator's in- and out-parameters as readonly fields foreach (var p in iter.Ins) { if (members.ContainsKey(p.Name)) { reporter.Error(MessageSource.Resolver, p, "Name of in-parameter is used by another member of the iterator: {0}", p.Name); } else { var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, false, p.Type, null); field.EnclosingClass = iter; // resolve here members.Add(p.Name, field); iter.Members.Add(field); } } foreach (var p in iter.Outs) { if (members.ContainsKey(p.Name)) { reporter.Error(MessageSource.Resolver, p, "Name of yield-parameter is used by another member of the iterator: {0}", p.Name); } else { var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, true, true, p.Type, null); field.EnclosingClass = iter; // resolve here iter.OutsFields.Add(field); members.Add(p.Name, field); iter.Members.Add(field); } } foreach (var p in iter.Outs) { var nm = p.Name + "s"; if (members.ContainsKey(nm)) { reporter.Error(MessageSource.Resolver, p.tok, "Name of implicit yield-history variable '{0}' is already used by another member of the iterator", p.Name); } else { var tp = new SeqType(p.Type.IsSubrangeType ? new IntType() : p.Type); var field = new SpecialField(p.tok, nm, nm, "", "", true, true, false, tp, null); field.EnclosingClass = iter; // resolve here iter.OutsHistoryFields.Add(field); // for now, just record this field (until all parameters have been added as members) } } // now that already-used 'ys' names have been checked for, add these yield-history variables iter.OutsHistoryFields.ForEach(f => { members.Add(f.Name, f); iter.Members.Add(f); }); // add the additional special variables as fields iter.Member_Reads = new SpecialField(iter.tok, "_reads", "_reads", "", "", true, false, false, new SetType(true, new ObjectType()), null); iter.Member_Modifies = new SpecialField(iter.tok, "_modifies", "_modifies", "", "", true, false, false, new SetType(true, new ObjectType()), null); iter.Member_New = new SpecialField(iter.tok, "_new", "_new", "", "", true, true, true, new SetType(true, new ObjectType()), null); foreach (var field in new List() { iter.Member_Reads, iter.Member_Modifies, iter.Member_New }) { field.EnclosingClass = iter; // resolve here members.Add(field.Name, field); iter.Members.Add(field); } // finally, add special variables to hold the components of the (explicit or implicit) decreases clause FillInDefaultDecreases(iter, false); // create the fields; unfortunately, we don't know their types yet, so we'll just insert type proxies for now var i = 0; foreach (var p in iter.Decreases.Expressions) { var nm = "_decreases" + i; var field = new SpecialField(p.tok, nm, nm, "", "", true, false, false, new InferredTypeProxy(), null); field.EnclosingClass = iter; // resolve here iter.DecreasesFields.Add(field); members.Add(field.Name, field); iter.Members.Add(field); i++; } // Note, the typeArgs parameter to the following Method/Predicate constructors is passed in as the empty list. What that is // saying is that the Method/Predicate does not take any type parameters over and beyond what the enclosing type (namely, the // iterator type) does. // --- here comes the constructor var init = new Constructor(iter.tok, "_ctor", new List(), iter.Ins, new List(), new Specification(new List(), null), new List(), new Specification(new List(), null), null, null, null); // --- here comes predicate Valid() var valid = new Predicate(iter.tok, "Valid", false, true, true, new List(), new List(), new List(), new List(), new List(), new Specification(new List(), null), null, Predicate.BodyOriginKind.OriginalOrInherited, null, null); // --- here comes method MoveNext var moveNext = new Method(iter.tok, "MoveNext", false, false, new List(), new List(), new List() { new Formal(iter.tok, "more", Type.Bool, false, false) }, new List(), new Specification(new List(), null), new List(), new Specification(new List(), null), null, null, null); // add these implicit members to the class init.EnclosingClass = iter; valid.EnclosingClass = iter; moveNext.EnclosingClass = iter; iter.HasConstructor = true; iter.Member_Init = init; iter.Member_Valid = valid; iter.Member_MoveNext = moveNext; MemberDecl member; if (members.TryGetValue(init.Name, out member)) { reporter.Error(MessageSource.Resolver, member.tok, "member name '{0}' is already predefined for this iterator", init.Name); } else { members.Add(init.Name, init); iter.Members.Add(init); } // If the name of the iterator is "Valid" or "MoveNext", one of the following will produce an error message. That // error message may not be as clear as it could be, but the situation also seems unlikely to ever occur in practice. if (members.TryGetValue("Valid", out member)) { reporter.Error(MessageSource.Resolver, member.tok, "member name 'Valid' is already predefined for iterators"); } else { members.Add(valid.Name, valid); iter.Members.Add(valid); } if (members.TryGetValue("MoveNext", out member)) { reporter.Error(MessageSource.Resolver, member.tok, "member name 'MoveNext' is already predefined for iterators"); } else { members.Add(moveNext.Name, moveNext); iter.Members.Add(moveNext); } } else if (d is ClassDecl) { ClassDecl cl = (ClassDecl)d; // register the names of the class members var members = new Dictionary(); classMembers.Add(cl, members); foreach (MemberDecl m in cl.Members) { if (!members.ContainsKey(m.Name)) { members.Add(m.Name, m); if (m is Constructor) { if (cl is TraitDecl) { reporter.Error(MessageSource.Resolver, m.tok, "a trait is not allowed to declare a constructor"); } else { cl.HasConstructor = true; } } else if (m is FixpointPredicate || m is FixpointLemma) { var extraName = m.Name + "#"; MemberDecl extraMember; var cloner = new Cloner(); var formals = new List(); var k = new ImplicitFormal(m.tok, "_k", new NatType(), true, false); formals.Add(k); if (m is FixpointPredicate) { var cop = (FixpointPredicate)m; formals.AddRange(cop.Formals.ConvertAll(cloner.CloneFormal)); List tyvars = cop.TypeArgs.ConvertAll(cloner.CloneTypeParam); // create prefix predicate cop.PrefixPredicate = new PrefixPredicate(cop.tok, extraName, cop.HasStaticKeyword, cop.IsProtected, tyvars, k, formals, cop.Req.ConvertAll(cloner.CloneExpr), cop.Reads.ConvertAll(cloner.CloneFrameExpr), cop.Ens.ConvertAll(cloner.CloneExpr), new Specification(new List() { new IdentifierExpr(cop.tok, k.Name) }, null), cop.Body, null, cop); extraMember = cop.PrefixPredicate; // In the call graph, add an edge from P# to P, since this will have the desired effect of detecting unwanted cycles. moduleDef.CallGraph.AddEdge(cop.PrefixPredicate, cop); } else { var com = (FixpointLemma)m; // _k has already been added to 'formals', so append the original formals formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal)); // prepend _k to the given decreases clause var decr = new List(); decr.Add(new IdentifierExpr(com.tok, k.Name)); decr.AddRange(com.Decreases.Expressions.ConvertAll(cloner.CloneExpr)); // Create prefix lemma. Note that the body is not cloned, but simply shared. // For a colemma, the postconditions are filled in after the colemma's postconditions have been resolved. // For an inductive lemma, the preconditions are filled in after the inductive lemma's preconditions have been resolved. var req = com is CoLemma ? com.Req.ConvertAll(cloner.CloneMayBeFreeExpr) : new List(); var ens = com is CoLemma ? new List() : com.Ens.ConvertAll(cloner.CloneMayBeFreeExpr); com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.HasStaticKeyword, com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal), req, cloner.CloneSpecFrameExpr(com.Mod), ens, new Specification(decr, null), null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the colemma is known cloner.CloneAttributes(com.Attributes), com); extraMember = com.PrefixLemma; // In the call graph, add an edge from M# to M, since this will have the desired effect of detecting unwanted cycles. moduleDef.CallGraph.AddEdge(com.PrefixLemma, com); } members.Add(extraName, extraMember); } } else if (m is Constructor && !((Constructor)m).HasName) { reporter.Error(MessageSource.Resolver, m, "More than one anonymous constructor"); } else { reporter.Error(MessageSource.Resolver, m, "Duplicate member name: {0}", m.Name); } } if (cl.IsDefaultClass) { foreach (MemberDecl m in cl.Members) { Contract.Assert(!m.HasStaticKeyword || DafnyOptions.O.AllowGlobals); // note, the IsStatic value isn't available yet; when it becomes available, we expect it will have the value 'true' if (m is Function || m is Method) { sig.StaticMembers[m.Name] = m; } } } } else { DatatypeDecl dt = (DatatypeDecl)d; // register the names of the constructors var ctors = new Dictionary(); datatypeCtors.Add(dt, ctors); // ... and of the other members var members = new Dictionary(); datatypeMembers.Add(dt, members); foreach (DatatypeCtor ctor in dt.Ctors) { if (ctor.Name.EndsWith("?")) { reporter.Error(MessageSource.Resolver, ctor, "a datatype constructor name is not allowed to end with '?'"); } else if (ctors.ContainsKey(ctor.Name)) { reporter.Error(MessageSource.Resolver, ctor, "Duplicate datatype constructor name: {0}", ctor.Name); } else { ctors.Add(ctor.Name, ctor); // create and add the query "method" (field, really) string queryName = ctor.Name + "?"; var query = new SpecialField(ctor.tok, queryName, "is_" + ctor.CompileName, "", "", false, false, false, Type.Bool, null); query.EnclosingClass = dt; // resolve here members.Add(queryName, query); ctor.QueryField = query; // also register the constructor name globally Tuple pair; if (sig.Ctors.TryGetValue(ctor.Name, out pair)) { // mark it as a duplicate sig.Ctors[ctor.Name] = new Tuple(pair.Item1, true); } else { // add new sig.Ctors.Add(ctor.Name, new Tuple(ctor, false)); } } } // add deconstructors now (that is, after the query methods have been added) foreach (DatatypeCtor ctor in dt.Ctors) { foreach (var formal in ctor.Formals) { bool nameError = false; if (formal.HasName && members.ContainsKey(formal.Name)) { reporter.Error(MessageSource.Resolver, ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name); nameError = true; } var dtor = new DatatypeDestructor(formal.tok, ctor, formal, formal.Name, "dtor_" + formal.CompileName, "", "", formal.IsGhost, formal.Type, null); dtor.EnclosingClass = dt; // resolve here if (!nameError && formal.HasName) { members.Add(formal.Name, dtor); } ctor.Destructors.Add(dtor); } } } } return sig; } private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, List mods) { var mod = new ModuleDefinition(Token.NoToken, Name + ".Abs", true, true, /*isExclusiveRefinement:*/ false, null, null, null, false); mod.ClonedFrom = p.ModuleDef; mod.Height = Height; foreach (var kv in p.TopLevels) { mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name)); } var sig = RegisterTopLevelDecls(mod, true); sig.Refines = p.Refines; sig.CompileSignature = p; sig.IsAbstract = p.IsAbstract; sig.ExclusiveRefinement = p.ExclusiveRefinement; mods.Add(mod); ResolveModuleDefinition(mod, sig); return sig; } TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m, List mods, string Name) { Contract.Requires(d != null); Contract.Requires(m != null); if (d is ModuleFacadeDecl) { var abs = (ModuleFacadeDecl)d; var sig = MakeAbstractSignature(abs.OriginalSignature, Name + "." + abs.Name, abs.Height, mods); var a = new ModuleFacadeDecl(abs.Path, abs.tok, m, abs.CompilePath, abs.Opened); a.Signature = sig; a.OriginalSignature = abs.OriginalSignature; return a; } else { return new ClonerButDropMethodBodies().CloneDeclaration(d, m); } } public static bool ResolvePath(ModuleDecl root, List Path, out ModuleSignature p, ErrorReporter reporter) { if (Path.Count == 1 && root is LiteralModuleDecl) { // use the default export when the importing the root LiteralModuleDecl decl = (LiteralModuleDecl)root; p = decl.DefaultExport; return true; } p = root.Signature; int i = 1; while (i < Path.Count) { ModuleSignature pp; if (p.FindSubmodule(Path[i].val, out pp)) { p = pp; i++; } else { reporter.Error(MessageSource.Resolver, Path[i], ModuleNotFoundErrorMessage(i, Path)); break; } } return i == Path.Count; } public void ResolveTopLevelDecls_Signatures(ModuleDefinition def, List/*!*/ declarations, Graph/*!*/ datatypeDependencies, Graph/*!*/ codatatypeDependencies) { Contract.Requires(declarations != null); Contract.Requires(datatypeDependencies != null); Contract.Requires(codatatypeDependencies != null); // resolve the trait names that a class extends and register the trait members in the classes that inherit them foreach (TopLevelDecl d in declarations) { var cl = d as ClassDecl; if (cl != null) { RegisterInheritedMembers(cl); } } var typeRedirectionDependencies = new Graph(); foreach (TopLevelDecl d in declarations) { if (DafnyOptions.O.IronDafny && d.Module.IsExclusiveRefinement) { var refinementOf = def.RefinementBase.TopLevelDecls.Find( i => String.Equals(i.Name, d.Name, StringComparison.InvariantCulture)); if (refinementOf != null && refinementOf.ExclusiveRefinement == null) { refinementOf.ExclusiveRefinement = d; } } Contract.Assert(d != null); allTypeParameters.PushMarker(); ResolveTypeParameters(d.TypeArgs, true, d); if (d is OpaqueTypeDecl) { // nothing to do } else if (d is TypeSynonymDecl) { var syn = (TypeSynonymDecl)d; ResolveType(syn.tok, syn.Rhs, syn, ResolveTypeOptionEnum.AllowPrefix, syn.TypeArgs); syn.Rhs.ForeachTypeComponent(ty => { var s = ty.AsRedirectingType; if (s != null) { typeRedirectionDependencies.AddEdge(syn, s); } }); } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; ResolveType(dd.tok, dd.BaseType, dd, ResolveTypeOptionEnum.DontInfer, null); dd.BaseType.ForeachTypeComponent(ty => { var s = ty.AsRedirectingType; if (s != null) { typeRedirectionDependencies.AddEdge(dd, s); } }); } else if (d is IteratorDecl) { ResolveIteratorSignature((IteratorDecl)d); } else if (d is ClassDecl) { ResolveClassMemberTypes((ClassDecl)d); } else if (d is ModuleDecl) { var decl = (ModuleDecl)d; if (!def.IsAbstract) { if (decl.Signature.IsAbstract) { if (// _module is allowed to contain abstract modules, but not be abstract itself. Note this presents a challenge to // trusted verification, as toplevels can't be trusted if they invoke abstract module members. !def.IsDefaultModule // [IronDafny] it's possbile for an abstract module to have an exclusive refinement, so it no longer makes sense to disallow this. && !DafnyOptions.O.IronDafny) reporter.Error(MessageSource.Resolver, d.tok, "an abstract module can only be imported into other abstract modules, not a concrete one."); } else { // physical modules are allowed everywhere } } else { // everything is allowed in an abstract module } } else { ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies, codatatypeDependencies); } allTypeParameters.PopMarker(); } // Now that all traits have been resolved, let classes inherit the trait members foreach (var d in declarations) { var cl = d as ClassDecl; if (cl != null) { InheritTraitMembers(cl); } } // perform acyclicity test on type synonyms var cycle = typeRedirectionDependencies.TryFindCycle(); if (cycle != null) { Contract.Assert(cycle.Count != 0); var erste = cycle[0]; reporter.Error(MessageSource.Resolver, erste.Tok, "Cycle among redirecting types (newtypes, type synonyms): {0} -> {1}", Util.Comma(" -> ", cycle, syn => syn.Name), erste.Name); } } static readonly List NativeTypes = new List() { new NativeType("byte", 0, 0x100, "", true), new NativeType("sbyte", -0x80, 0x80, "", true), new NativeType("ushort", 0, 0x10000, "", true), new NativeType("short", -0x8000, 0x8000, "", true), new NativeType("uint", 0, 0x100000000, "U", false), new NativeType("int", -0x80000000, 0x80000000, "", false), new NativeType("ulong", 0, new BigInteger(0x100000000) * new BigInteger(0x100000000), "UL", false), new NativeType("long", Int64.MinValue, 0x8000000000000000, "L", false), }; public void ResolveTopLevelDecls_Core(List/*!*/ declarations, Graph/*!*/ datatypeDependencies, Graph/*!*/ codatatypeDependencies) { Contract.Requires(declarations != null); Contract.Requires(cce.NonNullElements(datatypeDependencies)); Contract.Requires(cce.NonNullElements(codatatypeDependencies)); Contract.Requires(AllTypeConstraints.Count == 0); Contract.Ensures(AllTypeConstraints.Count == 0); int prevErrorCount = reporter.Count(ErrorLevel.Error); // ---------------------------------- Pass 0 ---------------------------------- // This pass resolves names, introduces (and may solve) type constraints, and // builds the module's call graph. // For 'newtype' declarations, it also checks that all types were fully // determined. // ---------------------------------------------------------------------------- // Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations // First, resolve the newtype declarations and the constraint clauses, including filling in .ResolvedOp fields. This is needed for the // resolution of the other declarations, because those other declarations may invoke DiscoverBounds, which looks at the .Constraint field // of any newtypes involved. DiscoverBounds is called on quantifiers (but only in non-ghost contexts) and set comprehensions (in all // contexts). The constraints of newtypes are ghost, so DiscoverBounds is not going to be called on any quantifiers they may contain. // However, the constraints may contain set comprehensions. For this reason, we postpone the DiscoverBounds checks on set comprehensions. foreach (TopLevelDecl d in declarations) { Contract.Assert(d != null); if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; ResolveAttributes(d.Attributes, new ResolveOpts(new NoContext(d.Module), false)); // this check can be done only after it has been determined that the redirected types do not involve cycles if (!dd.BaseType.IsNumericBased()) { reporter.Error(MessageSource.Resolver, dd.tok, "newtypes must be based on some numeric type (got {0})", dd.BaseType); } // type check the constraint, if any if (dd.Var != null) { Contract.Assert(object.ReferenceEquals(dd.Var.Type, dd.BaseType)); // follows from NewtypeDecl invariant Contract.Assert(dd.Constraint != null); // follows from NewtypeDecl invariant scope.PushMarker(); var added = scope.Push(dd.Var.Name, dd.Var); Contract.Assert(added == Scope.PushResult.Success); ResolveType(dd.Var.tok, dd.Var.Type, dd, ResolveTypeOptionEnum.DontInfer, null); ResolveExpression(dd.Constraint, new ResolveOpts(dd, false)); Contract.Assert(dd.Constraint.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(dd.Constraint.Type, Type.Bool, dd.Constraint, "newtype constraint must be of type bool (instead got {0})", dd.Constraint.Type); SolveAllTypeConstraints(); if (!CheckTypeInference_Visitor.IsDetermined(dd.BaseType.NormalizeExpand())) { reporter.Error(MessageSource.Resolver, dd.tok, "newtype's base type is not fully determined; add an explicit type for '{0}'", dd.Var.Name); } CheckTypeInference(dd.Constraint, dd); scope.PopMarker(); } } } // Now, we're ready for the other declarations. foreach (TopLevelDecl d in declarations) { Contract.Assert(AllTypeConstraints.Count == 0); if (d is TraitDecl && d.TypeArgs.Count > 0) { reporter.Error(MessageSource.Resolver, d, "sorry, traits with type parameters are not supported"); } allTypeParameters.PushMarker(); ResolveTypeParameters(d.TypeArgs, false, d); if (!(d is IteratorDecl)) { // Note, attributes of iterators are resolved by ResolvedIterator, after registering any names in the iterator signature ResolveAttributes(d.Attributes, new ResolveOpts(new NoContext(d.Module), false)); } if (d is IteratorDecl) { var iter = (IteratorDecl)d; ResolveIterator(iter); ResolveClassMemberBodies(iter); // resolve the automatically generated members } else if (d is ClassDecl) { var cl = (ClassDecl)d; ResolveClassMemberBodies(cl); } allTypeParameters.PopMarker(); } // ---------------------------------- Pass 1 ---------------------------------- // This pass: // * checks that type inference was able to determine all types // * fills in the .ResolvedOp field of binary expressions // * discovers bounds for: // - forall statements // - set comprehensions // - map comprehensions // - quantifier expressions // - assign-such-that statements // - compilable let-such-that expressions // - newtype constraints // For each statement body that it successfully typed, this pass also: // * computes ghost interests // * determines/checks tail-recursion. // ---------------------------------------------------------------------------- Dictionary nativeTypeMap = new Dictionary(); foreach (var nativeType in NativeTypes) { nativeTypeMap.Add(nativeType.Name, nativeType); } if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { // Check that type inference went well everywhere; this will also fill in the .ResolvedOp field in binary expressions foreach (TopLevelDecl d in declarations) { if (d is IteratorDecl) { var iter = (IteratorDecl)d; var prevErrCnt = reporter.Count(ErrorLevel.Error); iter.Members.Iter(CheckTypeInference_Member); if (prevErrCnt == reporter.Count(ErrorLevel.Error)) { iter.SubExpressions.Iter(e => CheckExpression(e, this, iter)); } if (iter.Body != null) { CheckTypeInference(iter.Body, iter); if (prevErrCnt == reporter.Count(ErrorLevel.Error)) { ComputeGhostInterest(iter.Body, false, iter); CheckExpression(iter.Body, this, iter); } } } else if (d is ClassDecl) { var cl = (ClassDecl)d; foreach (var member in cl.Members) { var prevErrCnt = reporter.Count(ErrorLevel.Error); CheckTypeInference_Member(member); if (prevErrCnt == reporter.Count(ErrorLevel.Error)) { if (member is Method) { var m = (Method)member; if (m.Body != null) { ComputeGhostInterest(m.Body, m.IsGhost, m); CheckExpression(m.Body, this, m); DetermineTailRecursion(m); } } else if (member is Function) { var f = (Function)member; if (!f.IsGhost && f.Body != null) { CheckIsCompilable(f.Body); } DetermineTailRecursion(f); } if (prevErrCnt == reporter.Count(ErrorLevel.Error) && member is ICodeContext) { member.SubExpressions.Iter(e => CheckExpression(e, this, (ICodeContext)member)); } } } } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (dd.Var != null) { Contract.Assert(dd.Constraint != null); CheckExpression(dd.Constraint, this, dd); } FigureOutNativeType(dd, nativeTypeMap); } } } // ---------------------------------- Pass 2 ---------------------------------- // This pass fills in various additional information. // ---------------------------------------------------------------------------- if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { // fill in the postconditions and bodies of prefix lemmas foreach (var com in ModuleDefinition.AllFixpointLemmas(declarations)) { var prefixLemma = com.PrefixLemma; if (prefixLemma == null) { continue; // something went wrong during registration of the prefix lemma (probably a duplicated fixpoint-lemma name) } var k = prefixLemma.Ins[0]; var focalPredicates = new HashSet(); if (com is CoLemma) { // compute the postconditions of the prefix lemma Contract.Assume(prefixLemma.Ens.Count == 0); // these are not supposed to have been filled in before foreach (var p in com.Ens) { var coConclusions = new HashSet(); CollectFriendlyCallsInFixpointLemmaSpecification(p.E, true, coConclusions, true); var subst = new FixpointLemmaSpecificationSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this.reporter, true); var post = subst.CloneExpr(p.E); prefixLemma.Ens.Add(new MaybeFreeExpression(post, p.IsFree)); foreach (var e in coConclusions) { var fce = e as FunctionCallExpr; if (fce != null) { // the other possibility is that "e" is a BinaryExpr focalPredicates.Add((CoPredicate)fce.Function); } } } } else { // compute the preconditions of the prefix lemma Contract.Assume(prefixLemma.Req.Count == 0); // these are not supposed to have been filled in before foreach (var p in com.Req) { var antecedents = new HashSet(); CollectFriendlyCallsInFixpointLemmaSpecification(p.E, true, antecedents, false); var subst = new FixpointLemmaSpecificationSubstituter(antecedents, new IdentifierExpr(k.tok, k.Name), this.reporter, false); var pre = subst.CloneExpr(p.E); prefixLemma.Req.Add(new MaybeFreeExpression(pre, p.IsFree)); foreach (var e in antecedents) { var fce = (FunctionCallExpr)e; // we expect "antecedents" to contain only FunctionCallExpr's focalPredicates.Add((InductivePredicate)fce.Function); } } } reporter.Info(MessageSource.Resolver, com.tok, string.Format("{0} specialized for {1}", com.PrefixLemma.Name, Util.Comma(focalPredicates, p => p.Name))); // Compute the statement body of the prefix lemma Contract.Assume(prefixLemma.Body == null); // this is not supposed to have been filled in before if (com.Body != null) { var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1)); var subst = new FixpointLemmaBodyCloner(com, kMinusOne, focalPredicates, this.reporter); var mainBody = subst.CloneBlockStmt(com.Body); var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name)); var condBody = new IfStmt(com.BodyStartTok, mainBody.EndTok, false, kPositive, mainBody, null); prefixLemma.Body = new BlockStmt(com.tok, condBody.EndTok, new List() { condBody }); } // The prefix lemma now has all its components, so it's finally time we resolve it currentClass = (ClassDecl)prefixLemma.EnclosingClass; allTypeParameters.PushMarker(); ResolveTypeParameters(currentClass.TypeArgs, false, currentClass); ResolveTypeParameters(prefixLemma.TypeArgs, false, prefixLemma); ResolveMethod(prefixLemma); allTypeParameters.PopMarker(); currentClass = null; CheckTypeInference_Member(prefixLemma); } } // Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) { if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) { // do the following check once per SCC, so call it on each SCC representative SccStratosphereCheck(dtd, datatypeDependencies); DetermineEqualitySupport(dtd, datatypeDependencies); } } // Set the SccRepr field of codatatypes foreach (var repr in codatatypeDependencies.TopologicallySortedComponents()) { foreach (var codt in codatatypeDependencies.GetSCC(repr)) { codt.SscRepr = repr; } } if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { // because CheckCoCalls requires the given expression to have been successfully resolved // Perform the guardedness check on co-datatypes foreach (var repr in ModuleDefinition.AllFunctionSCCs(declarations)) { var module = repr.EnclosingModule; bool dealsWithCodatatypes = false; foreach (var m in module.CallGraph.GetSCC(repr)) { var f = m as Function; if (f != null && f.ResultType.InvolvesCoDatatype) { dealsWithCodatatypes = true; break; } } var coCandidates = new List(); var hasIntraClusterCallsInDestructiveContexts = false; foreach (var m in module.CallGraph.GetSCC(repr)) { var f = m as Function; if (f != null && f.Body != null) { var checker = new CoCallResolution(f, dealsWithCodatatypes); checker.CheckCoCalls(f.Body); coCandidates.AddRange(checker.FinalCandidates); hasIntraClusterCallsInDestructiveContexts |= checker.HasIntraClusterCallsInDestructiveContexts; } else if (f == null) { // the SCC contains a method, which we always consider to be a destructive context hasIntraClusterCallsInDestructiveContexts = true; } } if (coCandidates.Count != 0) { if (hasIntraClusterCallsInDestructiveContexts) { foreach (var c in coCandidates) { c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext; } } else { foreach (var c in coCandidates) { c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.Yes; c.EnclosingCoConstructor.IsCoCall = true; reporter.Info(MessageSource.Resolver, c.CandidateCall.tok, "co-recursive call"); } // Finally, fill in the CoClusterTarget field // Start by setting all the CoClusterTarget fields to CoRecursiveTargetAllTheWay. foreach (var m in module.CallGraph.GetSCC(repr)) { var f = (Function)m; // the cast is justified on account of that we allow co-recursive calls only in clusters that have no methods at all f.CoClusterTarget = Function.CoCallClusterInvolvement.CoRecursiveTargetAllTheWay; } // Then change the field to IsMutuallyRecursiveTarget whenever we see a non-self recursive non-co-recursive call foreach (var m in module.CallGraph.GetSCC(repr)) { var f = (Function)m; // cast is justified just like above foreach (var call in f.AllCalls) { if (call.CoCall != FunctionCallExpr.CoCallResolution.Yes && call.Function != f && ModuleDefinition.InSameSCC(f, call.Function)) { call.Function.CoClusterTarget = Function.CoCallClusterInvolvement.IsMutuallyRecursiveTarget; } } } } } } // Inferred required equality support for datatypes and for Function and Method signatures // First, do datatypes until a fixpoint is reached bool inferredSomething; do { inferredSomething = false; foreach (var d in declarations) { if (d is DatatypeDecl) { var dt = (DatatypeDecl)d; foreach (var tp in dt.TypeArgs) { if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { // here's our chance to infer the need for equality support foreach (var ctor in dt.Ctors) { foreach (var arg in ctor.Formals) { if (InferRequiredEqualitySupport(tp, arg.Type)) { tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; inferredSomething = true; goto DONE_DT; // break out of the doubly-nested loop } } } DONE_DT: ; } } } } } while (inferredSomething); // Now do it for Function and Method signatures foreach (var d in declarations) { if (d is IteratorDecl) { var iter = (IteratorDecl)d; var done = false; foreach (var tp in iter.TypeArgs) { if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { // here's our chance to infer the need for equality support foreach (var p in iter.Ins) { if (InferRequiredEqualitySupport(tp, p.Type)) { tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; done = true; break; } } foreach (var p in iter.Outs) { if (done) break; if (InferRequiredEqualitySupport(tp, p.Type)) { tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; break; } } } } } else if (d is ClassDecl) { var cl = (ClassDecl)d; foreach (var member in cl.Members) { if (!member.IsGhost) { if (member is Function) { var f = (Function)member; foreach (var tp in f.TypeArgs) { if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { // here's our chance to infer the need for equality support if (InferRequiredEqualitySupport(tp, f.ResultType)) { tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; } else { foreach (var p in f.Formals) { if (InferRequiredEqualitySupport(tp, p.Type)) { tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; break; } } } } } } else if (member is Method) { var m = (Method)member; bool done = false; foreach (var tp in m.TypeArgs) { if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) { // here's our chance to infer the need for equality support foreach (var p in m.Ins) { if (InferRequiredEqualitySupport(tp, p.Type)) { tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; done = true; break; } } foreach (var p in m.Outs) { if (done) break; if (InferRequiredEqualitySupport(tp, p.Type)) { tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; break; } } } } } } } } } // Check that all == and != operators in non-ghost contexts are applied to equality-supporting types. // Note that this check can only be done after determining which expressions are ghosts. foreach (var d in declarations) { if (d is IteratorDecl) { var iter = (IteratorDecl)d; foreach (var p in iter.Ins) { if (!p.IsGhost) { CheckEqualityTypes_Type(p.tok, p.Type); } } foreach (var p in iter.Outs) { if (!p.IsGhost) { CheckEqualityTypes_Type(p.tok, p.Type); } } if (iter.Body != null) { CheckEqualityTypes_Stmt(iter.Body); } } else if (d is ClassDecl) { var cl = (ClassDecl)d; foreach (var member in cl.Members) { if (!member.IsGhost) { if (member is Field) { var f = (Field)member; CheckEqualityTypes_Type(f.tok, f.Type); } else if (member is Function) { var f = (Function)member; foreach (var p in f.Formals) { if (!p.IsGhost) { CheckEqualityTypes_Type(p.tok, p.Type); } } CheckEqualityTypes_Type(f.tok, f.ResultType); if (f.Body != null) { CheckEqualityTypes(f.Body); } } else if (member is Method) { var m = (Method)member; foreach (var p in m.Ins) { if (!p.IsGhost) { CheckEqualityTypes_Type(p.tok, p.Type); } } foreach (var p in m.Outs) { if (!p.IsGhost) { CheckEqualityTypes_Type(p.tok, p.Type); } } if (m.Body != null) { CheckEqualityTypes_Stmt(m.Body); } } } } } else if (d is DatatypeDecl) { var dt = (DatatypeDecl)d; foreach (var ctor in dt.Ctors) { foreach (var p in ctor.Formals) { if (!p.IsGhost) { CheckEqualityTypes_Type(p.tok, p.Type); } } } } } // Check that fixpoint-predicates are not recursive with non-fixpoint-predicate functions (and only // with fixpoint-predicates of the same polarity), and // check that colemmas are not recursive with non-colemma methods. // Also, check that newtypes sit in their own SSC. foreach (var d in declarations) { if (d is ClassDecl) { foreach (var member in ((ClassDecl)d).Members) { if (member is FixpointPredicate) { var fn = (FixpointPredicate)member; // Check here for the presence of any 'ensures' clauses, which are not allowed (because we're not sure // of their soundness) if (fn.Ens.Count != 0) { reporter.Error(MessageSource.Resolver, fn.Ens[0].tok, "a {0} is not allowed to declare any ensures clause", member.WhatKind); } // Also check for 'reads' clauses if (fn.Reads.Count != 0) { reporter.Error(MessageSource.Resolver, fn.Reads[0].tok, "a {0} is not allowed to declare any reads clause", member.WhatKind); // (why?) } if (fn.Body != null) { FixpointPredicateChecks(fn.Body, fn, CallingPosition.Positive); } } else if (member is FixpointLemma) { var m = (FixpointLemma)member; if (m.Body != null) { FixpointLemmaChecks(m.Body, m); } } } } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (dd.Module.CallGraph.GetSCCSize(dd) != 1) { var cycle = Util.Comma(" -> ", dd.Module.CallGraph.GetSCC(dd), clbl => clbl.NameRelativeToModule); reporter.Error(MessageSource.Resolver, dd.tok, "recursive dependency involving a newtype: " + cycle); } } } } } private void FigureOutNativeType(NewtypeDecl dd, Dictionary nativeTypeMap) { Contract.Requires(dd != null); Contract.Requires(nativeTypeMap != null); bool? boolNativeType = null; NativeType stringNativeType = null; object nativeTypeAttr = true; bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr, new Attributes.MatchingValueOption[] { Attributes.MatchingValueOption.Empty, Attributes.MatchingValueOption.Bool, Attributes.MatchingValueOption.String }, err => reporter.Error(MessageSource.Resolver, dd, err)); if (hasNativeTypeAttr) { if (nativeTypeAttr is bool) { boolNativeType = (bool)nativeTypeAttr; } else { string keyString = (string)nativeTypeAttr; if (nativeTypeMap.ContainsKey(keyString)) { stringNativeType = nativeTypeMap[keyString]; } else { reporter.Error(MessageSource.Resolver, dd, "Unsupported nativeType {0}", keyString); } } } if (stringNativeType != null || boolNativeType == true) { if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) { reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used on integral types"); } if (dd.Var == null) { reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used if newtype specifies a constraint"); } } if (dd.Var != null) { Func GetConst = null; GetConst = (Expression e) => { int m = 1; BinaryExpr bin = e as BinaryExpr; if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) { m = -1; e = bin.E1; } LiteralExpr l = e as LiteralExpr; if (l != null && l.Value is BigInteger) { return m * (BigInteger)l.Value; } return null; }; var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint); List potentialNativeTypes = (stringNativeType != null) ? new List { stringNativeType } : (boolNativeType == false) ? new List() : NativeTypes; foreach (var nt in potentialNativeTypes) { bool lowerOk = false; bool upperOk = false; foreach (var bound in bounds) { if (bound is ComprehensionExpr.IntBoundedPool) { var bnd = (ComprehensionExpr.IntBoundedPool)bound; if (bnd.LowerBound != null) { BigInteger? lower = GetConst(bnd.LowerBound); if (lower != null && nt.LowerBound <= lower) { lowerOk = true; } } if (bnd.UpperBound != null) { BigInteger? upper = GetConst(bnd.UpperBound); if (upper != null && upper <= nt.UpperBound) { upperOk = true; } } } } if (lowerOk && upperOk) { dd.NativeType = nt; break; } } if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) { reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type. " + "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'"); } if (dd.NativeType != null && stringNativeType == null) { reporter.Info(MessageSource.Resolver, dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}"); } } } /// /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be /// untenable. If this is immediately known not to be untenable, false is returned. /// private bool ConstrainTypes(Type ty, Type expected, TopLevelDecl declForToken, string msg, params object[] args) { Contract.Requires(ty != null); Contract.Requires(expected != null); Contract.Requires(declForToken != null); Contract.Requires(msg != null); Contract.Requires(args != null); return ConstrainTypes(ty, expected, declForToken.tok, msg, args); } /// /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be /// untenable. If this is immediately known not to be untenable, false is returned. /// private bool ConstrainTypes(Type ty, Type expected, MemberDecl declForToken, string msg, params object[] args) { Contract.Requires(ty != null); Contract.Requires(expected != null); Contract.Requires(declForToken != null); Contract.Requires(msg != null); Contract.Requires(args != null); return ConstrainTypes(ty, expected, declForToken.tok, msg, args); } /// /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be /// untenable. If this is immediately known not to be untenable, false is returned. /// private bool ConstrainTypes(Type ty, Type expected, Statement stmtForToken, string msg, params object[] args) { Contract.Requires(ty != null); Contract.Requires(expected != null); Contract.Requires(stmtForToken != null); Contract.Requires(msg != null); Contract.Requires(args != null); return ConstrainTypes(ty, expected, stmtForToken.Tok, msg, args); } /// /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be /// untenable. If this is immediately known not to be untenable, false is returned. /// private bool ConstrainTypes(Type ty, Type expected, Expression exprForToken, string msg, params object[] args) { Contract.Requires(ty != null); Contract.Requires(expected != null); Contract.Requires(exprForToken != null); Contract.Requires(msg != null); Contract.Requires(args != null); return ConstrainTypes(ty, expected, exprForToken.tok, msg, args); } /// /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be /// untenable. If this is immediately known not to be untenable, false is returned. /// private bool ConstrainTypes(Type ty, Type expected, IToken tok, string msg, params object[] args) { Contract.Requires(ty != null); Contract.Requires(expected != null); Contract.Requires(tok != null); Contract.Requires(msg != null); Contract.Requires(args != null); #if LAZY_TYPE_CHECKING var c = new TypeConstraint(ty, expected, tok, msg, args); AllTypeConstraints.Add(c); return true; #else if (!UnifyTypes(ty, expected)) { reporter.Error(MessageSource.Resolver, tok, msg, args); return false; } return true; #endif } public List AllTypeConstraints = new List(); /// /// Solves or simplifies as many type constraints as possible /// void PartiallySolveTypeConstraints() { var remainingConstraints = new List(); foreach (var constraint in AllTypeConstraints) { if (!constraint.CheckTenable(this)) { remainingConstraints.Add(constraint); } } AllTypeConstraints = remainingConstraints; } /// /// Attempts to fully solve all type constraints. Upon success, returns "true". /// Upon failure, reports errors and returns "false". /// Clears all constraints. /// bool SolveAllTypeConstraints() { PartiallySolveTypeConstraints(); foreach (var constraint in AllTypeConstraints) { constraint.ReportAsError(reporter); } var success = AllTypeConstraints.Count == 0; AllTypeConstraints.Clear(); return success; } public class TypeConstraint { readonly Type Ty; readonly Type Expected; readonly IToken Tok; readonly string Msg; readonly object[] MsgArgs; public TypeConstraint(Type ty, Type expected, IToken tok, string msg, object[] msgArgs) { Ty = ty; Expected = expected; Tok = tok; Msg = msg; MsgArgs = msgArgs; } /// /// Returns "true" if constraint is tenable, "false" otherwise. /// /// public bool CheckTenable(Resolver resolver) { Contract.Requires(resolver != null); return resolver.UnifyTypes(Ty, Expected); } public void ReportAsError(ErrorReporter reporter) { Contract.Requires(reporter != null); reporter.Error(MessageSource.Resolver, Tok, Msg, MsgArgs); } } // ------------------------------------------------------------------------------------------------------ // ----- Visitors --------------------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region Visitors class ResolverBottomUpVisitor : BottomUpVisitor { protected Resolver resolver; public ResolverBottomUpVisitor(Resolver resolver) { Contract.Requires(resolver != null); this.resolver = resolver; } } abstract class ResolverTopDownVisitor : TopDownVisitor { protected Resolver resolver; public ResolverTopDownVisitor(Resolver resolver) { Contract.Requires(resolver != null); this.resolver = resolver; } } #endregion Visitors // ------------------------------------------------------------------------------------------------------ // ----- CheckTypeInference ----------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region CheckTypeInference private void CheckTypeInference_Member(MemberDecl member) { if (member is Method) { var m = (Method)member; m.Req.Iter(mfe => CheckTypeInference_MaybeFreeExpression(mfe, m)); m.Ens.Iter(mfe => CheckTypeInference_MaybeFreeExpression(mfe, m)); CheckTypeInference_Specification_FrameExpr(m.Mod, m); CheckTypeInference_Specification_Expr(m.Decreases, m); if (m.Body != null) { CheckTypeInference(m.Body, m); } } else if (member is Function) { var f = (Function)member; var errorCount = reporter.Count(ErrorLevel.Error); f.Req.Iter(e => CheckTypeInference(e, f)); f.Ens.Iter(e => CheckTypeInference(e, f)); f.Reads.Iter(fe => CheckTypeInference(fe.E, f)); CheckTypeInference_Specification_Expr(f.Decreases, f); if (f.Body != null) { CheckTypeInference(f.Body, f); } if (errorCount == reporter.Count(ErrorLevel.Error) && f is FixpointPredicate) { var cop = (FixpointPredicate)f; CheckTypeInference_Member(cop.PrefixPredicate); } } } private void CheckTypeInference_MaybeFreeExpression(MaybeFreeExpression mfe, ICodeContext codeContext) { Contract.Requires(mfe != null); Contract.Requires(codeContext != null); foreach (var e in Attributes.SubExpressions(mfe.Attributes)) { CheckTypeInference(e, codeContext); } CheckTypeInference(mfe.E, codeContext); } private void CheckTypeInference_Specification_Expr(Specification spec, ICodeContext codeContext) { Contract.Requires(spec != null); Contract.Requires(codeContext != null); foreach (var e in Attributes.SubExpressions(spec.Attributes)) { CheckTypeInference(e, codeContext); } spec.Expressions.Iter(e => CheckTypeInference(e, codeContext)); } private void CheckTypeInference_Specification_FrameExpr(Specification spec, ICodeContext codeContext) { Contract.Requires(spec != null); Contract.Requires(codeContext != null); foreach (var e in Attributes.SubExpressions(spec.Attributes)) { CheckTypeInference(e, codeContext); } spec.Expressions.Iter(fe => CheckTypeInference(fe.E, codeContext)); } void CheckTypeInference(Expression expr, ICodeContext codeContext) { Contract.Requires(expr != null); Contract.Requires(codeContext != null); PartiallySolveTypeConstraints(); var c = new CheckTypeInference_Visitor(this, codeContext); c.Visit(expr); } void CheckTypeInference(Statement stmt, ICodeContext codeContext) { Contract.Requires(stmt != null); Contract.Requires(codeContext != null); var c = new CheckTypeInference_Visitor(this, codeContext); c.Visit(stmt); } class CheckTypeInference_Visitor : ResolverBottomUpVisitor { readonly ICodeContext codeContext; public CheckTypeInference_Visitor(Resolver resolver, ICodeContext codeContext) : base(resolver) { Contract.Requires(resolver != null); Contract.Requires(codeContext != null); this.codeContext = codeContext; } protected override void VisitOneStmt(Statement stmt) { if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; foreach (var local in s.Locals) { CheckTypeIsDetermined(local.Tok, local.Type, "local variable"); } } else if (stmt is LetStmt) { var s = (LetStmt)stmt; s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); List missingBounds; s.Bounds = DiscoverBestBounds_MultipleVars(s.BoundVars, s.Range, true, true, out missingBounds); } else if (stmt is AssignSuchThatStmt) { var s = (AssignSuchThatStmt)stmt; if (s.AssumeToken == null) { var varLhss = new List(); foreach (var lhs in s.Lhss) { var ide = (IdentifierExpr)lhs.Resolved; // successful resolution implies all LHS's are IdentifierExpr's varLhss.Add(ide.Var); } List missingBounds; var bestBounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, false, out missingBounds); if (missingBounds.Count != 0) { s.MissingBounds = missingBounds; // so that an error message can be produced during compilation } else { Contract.Assert(bestBounds != null); s.Bounds = bestBounds; } } } else if (stmt is CalcStmt) { var s = (CalcStmt)stmt; // The resolution of the calc statement builds up .Steps and .Result, which are of the form E0 OP E1, where // E0 and E1 are expressions from .Lines. These additional expressions still need to have their .ResolvedOp // fields filled in, so we visit them (but not their subexpressions) here. foreach (var e in s.Steps) { VisitOneExpr(e); } VisitOneExpr(s.Result); } } protected override void VisitOneExpr(Expression expr) { if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; foreach (var bv in e.BoundVars) { if (!IsDetermined(bv.Type.Normalize())) { resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly", bv.Name); } } // apply bounds discovery to quantifiers, finite sets, and finite maps string what = null; Expression whereToLookForBounds = null; bool polarity = true; if (e is QuantifierExpr) { what = "quantifier"; whereToLookForBounds = ((QuantifierExpr)e).LogicalBody(); polarity = e is ExistsExpr; } else if (e is SetComprehension) { what = "set comprehension"; whereToLookForBounds = e.Range; } else if (e is MapComprehension) { what = "map comprehension"; whereToLookForBounds = e.Range; } else { Contract.Assume(e is LambdaExpr); // otherwise, unexpected ComprehensionExpr } if (whereToLookForBounds != null) { List missingBounds; e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, whereToLookForBounds, polarity, true, out missingBounds); if (missingBounds.Count != 0) { e.MissingBounds = missingBounds; if ((e is SetComprehension && !((SetComprehension)e).Finite) || (e is MapComprehension && !((MapComprehension)e).Finite)) { // a possibly infinite set/map has no restrictions on its range (unless it's used in a compilable context, which is checked later) } else if (e is QuantifierExpr) { // a quantifier has no restrictions on its range (unless it's used in a compilable context, which is checked later) } else if (e is SetComprehension && e.Type.HasFinitePossibleValues) { // This means the set is finite, regardless of if the Range is bounded. So, we don't give any error here. // However, if this expression is used in a non-ghost context (which is not yet known at this stage of // resolution), the resolver will generate an error about that later. } else { // we cannot be sure that the set/map really is finite foreach (var bv in missingBounds) { resolver.reporter.Error(MessageSource.Resolver, e, "a {0} must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'", what, bv.Name); } } } if (codeContext is Function && e.Bounds != null) { // functions are not allowed to depend on the set of allocated objects Contract.Assert(e.Bounds.Count == e.BoundVars.Count); for (int i = 0; i < e.Bounds.Count; i++) { var bound = e.Bounds[i] as ComprehensionExpr.RefBoundedPool; if (bound != null) { var bv = e.BoundVars[i]; resolver.reporter.Error(MessageSource.Resolver, expr, "a {0} involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{1}'", what, bv.Name); } } } } } else if (expr is MemberSelectExpr) { var e = (MemberSelectExpr)expr; if (e.Member is Function || e.Member is Method) { foreach (var p in e.TypeApplication) { if (!IsDetermined(p.Normalize())) { resolver.reporter.Error(MessageSource.Resolver, e.tok, "type '{0}' to the {2} '{1}' is not determined", p, e.Member.Name, e.Member.WhatKind); } } } } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; foreach (var p in e.TypeArgumentSubstitutions) { if (!IsDetermined(p.Value.Normalize())) { resolver.reporter.Error(MessageSource.Resolver, e.tok, "type variable '{0}' in the function call to '{1}' could not be determined{2}", p.Key.Name, e.Name, (e.Name.StartsWith("reveal_") || e.Name.EndsWith("_FULL")) ? ". If you are making an opaque function, make sure that the function can be called." : "" ); } } } else if (expr is LetExpr) { var e = (LetExpr)expr; foreach (var p in e.LHSs) { foreach (var x in p.Vars) { if (!IsDetermined(x.Type.Normalize())) { resolver.reporter.Error(MessageSource.Resolver, e.tok, "the type of the bound variable '{0}' could not be determined", x.Name); } } } } else if (expr is IdentifierExpr) { // by specializing for IdentifierExpr, error messages will be clearer CheckTypeIsDetermined(expr.tok, expr.Type, "variable"); } else if (CheckTypeIsDetermined(expr.tok, expr.Type, "expression")) { var bin = expr as BinaryExpr; if (bin != null) { bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type); } } } /// /// This method checks to see if 't' has been determined and returns the result. /// However, if t denotes an int-based or real-based type, then t is set to int or real, /// respectively, here. Similarly, if t is an unresolved type for "null", then t /// is set to "object". /// public static bool IsDetermined(Type t) { Contract.Requires(t != null); Contract.Requires(!(t is TypeProxy) || ((TypeProxy)t).T == null); // If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively if (t is OperationTypeProxy) { var proxy = (OperationTypeProxy)t; if (proxy.JustInts) { proxy.T = Type.Int; return true; } else if (proxy.JustReals) { proxy.T = Type.Real; return true; } } else if (t is ObjectTypeProxy) { var proxy = (ObjectTypeProxy)t; proxy.T = new ObjectType(); return true; } // all other proxies indicate the type has not yet been determined, provided their type parameters have been return !(t is TypeProxy) && t.TypeArgs.All(tt => IsDetermined(tt.Normalize())); } ISet UnderspecifiedTypeProxies = new HashSet(); bool CheckTypeIsDetermined(IToken tok, Type t, string what) { Contract.Requires(tok != null); Contract.Requires(t != null); Contract.Requires(what != null); t = t.NormalizeExpand(); // If the type specifies an arbitrary int-based or real-based type, just fill it in with int or real, respectively; // similarly, if t refers to the type of "null", set its type to be "object". if (t is OperationTypeProxy) { var proxy = (OperationTypeProxy)t; if (proxy.JustInts) { proxy.T = Type.Int; return true; } else if (proxy.JustReals) { proxy.T = Type.Real; return true; } } else if (t is ObjectTypeProxy) { var proxy = (ObjectTypeProxy)t; proxy.T = new ObjectType(); return true; } if (t is TypeProxy) { var proxy = (TypeProxy)t; if (!UnderspecifiedTypeProxies.Contains(proxy)) { // report an error for this TypeProxy only once resolver.reporter.Error(MessageSource.Resolver, tok, "the type of this {0} is underspecified", what); UnderspecifiedTypeProxies.Add(proxy); } return false; } // Recurse on type arguments: if (t is MapType) { return CheckTypeIsDetermined(tok, ((MapType)t).Range, what) && CheckTypeIsDetermined(tok, ((MapType)t).Domain, what); } else if (t is CollectionType) { return CheckTypeIsDetermined(tok, ((CollectionType)t).Arg, what); } else if (t is UserDefinedType) { return t.TypeArgs.All(rg => CheckTypeIsDetermined(tok, rg, what)); } else { return true; } } } #endregion CheckTypeInference // ------------------------------------------------------------------------------------------------------ // ----- CheckExpression -------------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region CheckExpression /// /// This method computes ghost interests in the statement portion of StmtExpr's and /// checks for hint restrictions in any CalcStmt. /// void CheckExpression(Expression expr, Resolver resolver, ICodeContext codeContext) { Contract.Requires(expr != null); Contract.Requires(resolver != null); Contract.Requires(codeContext != null); var v = new CheckExpression_Visitor(resolver, codeContext); v.Visit(expr); } /// /// This method computes ghost interests in the statement portion of StmtExpr's and /// checks for hint restrictions in any CalcStmt. /// void CheckExpression(Statement stmt, Resolver resolver, ICodeContext codeContext) { Contract.Requires(stmt != null); Contract.Requires(resolver != null); Contract.Requires(codeContext != null); var v = new CheckExpression_Visitor(resolver, codeContext); v.Visit(stmt); } class CheckExpression_Visitor : ResolverBottomUpVisitor { readonly ICodeContext CodeContext; public CheckExpression_Visitor(Resolver resolver, ICodeContext codeContext) : base(resolver) { Contract.Requires(resolver != null); Contract.Requires(codeContext != null); CodeContext = codeContext; } protected override void VisitOneExpr(Expression expr) { if (expr is StmtExpr) { var e = (StmtExpr)expr; resolver.ComputeGhostInterest(e.S, true, CodeContext); } } protected override void VisitOneStmt(Statement stmt) { if (stmt is CalcStmt) { var s = (CalcStmt)stmt; foreach (var h in s.Hints) { resolver.CheckHintRestrictions(h, new HashSet()); } } } } #endregion // ------------------------------------------------------------------------------------------------------ // ----- CheckTailRecursive ----------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region CheckTailRecursive enum TailRecursionStatus { NotTailRecursive, // contains code that makes the enclosing method body not tail recursive (in way that is supported) CanBeFollowedByAnything, // the code just analyzed does not do any recursive calls TailCallSpent, // the method body is tail recursive, provided that all code that follows it in the method body is ghost } /// /// Checks if "stmts" can be considered tail recursive, and (provided "reportsError" is true) reports an error if not. /// Note, the current implementation is rather conservative in its analysis; upon need, the /// algorithm could be improved. /// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method. /// /// The incoming value of "tailCall" is not used, but it's nevertheless a 'ref' parameter to allow the /// body to return the incoming value or to omit assignments to it. /// If the return value is CanBeFollowedByAnything, "tailCall" is unchanged. /// If the return value is TailCallSpent, "tailCall" shows one of the calls where the tail call was spent. (Note, /// there could be several if the statements have branches.) /// If the return value is NoTailRecursive, "tailCall" could be anything. In this case, an error /// message has been reported (provided "reportsErrors" is true). /// TailRecursionStatus CheckTailRecursive(List stmts, Method enclosingMethod, ref CallStmt tailCall, bool reportErrors) { Contract.Requires(stmts != null); var status = TailRecursionStatus.CanBeFollowedByAnything; foreach (var s in stmts) { if (!s.IsGhost) { if (s is ReturnStmt && ((ReturnStmt)s).hiddenUpdate == null) { return status; } if (status == TailRecursionStatus.TailCallSpent) { // a tail call cannot be followed by non-ghost code if (reportErrors) { reporter.Error(MessageSource.Resolver, tailCall.Tok, "this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code"); } return TailRecursionStatus.NotTailRecursive; } status = CheckTailRecursive(s, enclosingMethod, ref tailCall, reportErrors); if (status == TailRecursionStatus.NotTailRecursive) { return status; } } } return status; } void DetermineTailRecursion(Function f) { Contract.Requires(f != null); bool tail = true; if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) { reporter.Error(MessageSource.Resolver, f.tok, "sorry, tail-call functions are not supported"); } } void DetermineTailRecursion(Method m) { Contract.Requires(m != null); bool tail = true; bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail); if (hasTailRecursionPreference && !tail) { // the user specifically requested no tail recursion, so do nothing else } else if (hasTailRecursionPreference && tail && m.IsGhost) { reporter.Error(MessageSource.Resolver, m.tok, "tail recursion can be specified only for methods that will be compiled, not for ghost methods"); } else { var module = m.EnclosingClass.Module; var sccSize = module.CallGraph.GetSCCSize(m); if (hasTailRecursionPreference && 2 <= sccSize) { reporter.Error(MessageSource.Resolver, m.tok, "sorry, tail-call optimizations are not supported for mutually recursive methods"); } else if (hasTailRecursionPreference || sccSize == 1) { CallStmt tailCall = null; var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference); if (status != TailRecursionStatus.NotTailRecursive) { m.IsTailRecursive = true; if (tailCall != null) { // this means there was at least one recursive call reporter.Info(MessageSource.Resolver, m.tok, "tail recursive"); } } } } } /// /// See CheckTailRecursive(List Statement, ...), including its description of "tailCall". /// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method. /// TailRecursionStatus CheckTailRecursive(Statement stmt, Method enclosingMethod, ref CallStmt tailCall, bool reportErrors) { Contract.Requires(stmt != null); if (stmt.IsGhost) { return TailRecursionStatus.NotTailRecursive; } if (stmt is PrintStmt) { } else if (stmt is BreakStmt) { } else if (stmt is ReturnStmt) { var s = (ReturnStmt)stmt; if (s.hiddenUpdate != null) { return CheckTailRecursive(s.hiddenUpdate, enclosingMethod, ref tailCall, reportErrors); } } else if (stmt is AssignStmt) { } else if (stmt is ModifyStmt) { var s = (ModifyStmt)stmt; if (s.Body != null) { return CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors); } } else if (stmt is CallStmt) { var s = (CallStmt)stmt; if (s.Method == enclosingMethod) { // It's a recursive call. It can be considered a tail call only if the LHS of the call are the // formal out-parameters of the method for (int i = 0; i < s.Lhs.Count; i++) { var formal = enclosingMethod.Outs[i]; if (!formal.IsGhost) { var lhs = s.Lhs[i] as IdentifierExpr; if (lhs != null && lhs.Var == formal) { // all is good } else { if (reportErrors) { reporter.Error(MessageSource.Resolver, s.Tok, "the recursive call to '{0}' is not tail recursive because the actual out-parameter {1} is not the formal out-parameter '{2}'", s.Method.Name, i, formal.Name); } return TailRecursionStatus.NotTailRecursive; } } } tailCall = s; return TailRecursionStatus.TailCallSpent; } } else if (stmt is BlockStmt) { var s = (BlockStmt)stmt; return CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors); } else if (stmt is IfStmt) { var s = (IfStmt)stmt; var stThen = CheckTailRecursive(s.Thn, enclosingMethod, ref tailCall, reportErrors); if (stThen == TailRecursionStatus.NotTailRecursive) { return stThen; } var stElse = s.Els == null ? TailRecursionStatus.CanBeFollowedByAnything : CheckTailRecursive(s.Els, enclosingMethod, ref tailCall, reportErrors); if (stElse == TailRecursionStatus.NotTailRecursive) { return stElse; } else if (stThen == TailRecursionStatus.TailCallSpent || stElse == TailRecursionStatus.TailCallSpent) { return TailRecursionStatus.TailCallSpent; } } else if (stmt is AlternativeStmt) { var s = (AlternativeStmt)stmt; var status = TailRecursionStatus.CanBeFollowedByAnything; foreach (var alt in s.Alternatives) { var st = CheckTailRecursive(alt.Body, enclosingMethod, ref tailCall, reportErrors); if (st == TailRecursionStatus.NotTailRecursive) { return st; } else if (st == TailRecursionStatus.TailCallSpent) { status = st; } } return status; } else if (stmt is WhileStmt) { var s = (WhileStmt)stmt; var status = TailRecursionStatus.NotTailRecursive; if (s.Body != null) { status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors); } if (status != TailRecursionStatus.CanBeFollowedByAnything) { if (status == TailRecursionStatus.NotTailRecursive) { // an error has already been reported } else if (reportErrors) { reporter.Error(MessageSource.Resolver, tailCall.Tok, "a recursive call inside a loop is not recognized as being a tail call"); } return TailRecursionStatus.NotTailRecursive; } } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; foreach (var alt in s.Alternatives) { var status = CheckTailRecursive(alt.Body, enclosingMethod, ref tailCall, reportErrors); if (status != TailRecursionStatus.CanBeFollowedByAnything) { if (status == TailRecursionStatus.NotTailRecursive) { // an error has already been reported } else if (reportErrors) { reporter.Error(MessageSource.Resolver, tailCall.Tok, "a recursive call inside a loop is not recognized as being a tail call"); } return TailRecursionStatus.NotTailRecursive; } } } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; var status = TailRecursionStatus.NotTailRecursive; if (s.Body != null) { status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors); } if (status != TailRecursionStatus.CanBeFollowedByAnything) { if (status == TailRecursionStatus.NotTailRecursive) { // an error has already been reported } else if (reportErrors) { reporter.Error(MessageSource.Resolver, tailCall.Tok, "a recursive call inside a forall statement is not a tail call"); } return TailRecursionStatus.NotTailRecursive; } } else if (stmt is MatchStmt) { var s = (MatchStmt)stmt; var status = TailRecursionStatus.CanBeFollowedByAnything; foreach (var kase in s.Cases) { var st = CheckTailRecursive(kase.Body, enclosingMethod, ref tailCall, reportErrors); if (st == TailRecursionStatus.NotTailRecursive) { return st; } else if (st == TailRecursionStatus.TailCallSpent) { status = st; } } return status; } else if (stmt is AssignSuchThatStmt) { } else if (stmt is UpdateStmt) { var s = (UpdateStmt)stmt; return CheckTailRecursive(s.ResolvedStatements, enclosingMethod, ref tailCall, reportErrors); } else if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; if (s.Update != null) { return CheckTailRecursive(s.Update, enclosingMethod, ref tailCall, reportErrors); } } else if (stmt is LetStmt) { } else { Contract.Assert(false); // unexpected statement type } return TailRecursionStatus.CanBeFollowedByAnything; } #endregion CheckTailRecursive // ------------------------------------------------------------------------------------------------------ // ----- FuelAdjustmentChecks --------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region FuelAdjustmentChecks protected void CheckForFuelAdjustments(IToken tok, Attributes attrs, ModuleDefinition currentModule) { List> results = Attributes.FindAllExpressions(attrs, "fuel"); if (results != null) { foreach (List args in results) { if (args != null && args.Count >= 2) { // Try to extract the function from the first argument MemberSelectExpr selectExpr = args[0].Resolved as MemberSelectExpr; if (selectExpr != null) { Function f = selectExpr.Member as Function; if (f != null) { f.IsFueled = true; if (f.IsProtected && currentModule != f.EnclosingClass.Module) { reporter.Error(MessageSource.Resolver, tok, "cannot adjust fuel for protected function {0} from another module", f.Name); } } } } } } } public class FuelAdjustment_Context { public ModuleDefinition currentModule; public FuelAdjustment_Context(ModuleDefinition currentModule) { this.currentModule = currentModule; } } class FuelAdjustment_Visitor : ResolverTopDownVisitor { public FuelAdjustment_Visitor(Resolver resolver) : base(resolver) { Contract.Requires(resolver != null); } protected override bool VisitOneStmt(Statement stmt, ref FuelAdjustment_Context st) { resolver.CheckForFuelAdjustments(stmt.Tok, stmt.Attributes, st.currentModule); return true; } } #endregion FuelAdjustmentChecks // ------------------------------------------------------------------------------------------------------ // ----- FixpointPredicateChecks ------------------------------------------------------------------------ // ------------------------------------------------------------------------------------------------------ #region FixpointPredicateChecks enum CallingPosition { Positive, Negative, Neither } static CallingPosition Invert(CallingPosition cp) { switch (cp) { case CallingPosition.Positive: return CallingPosition.Negative; case CallingPosition.Negative: return CallingPosition.Positive; default: return CallingPosition.Neither; } } class FindFriendlyCalls_Visitor : ResolverTopDownVisitor { public readonly bool IsCoContext; public FindFriendlyCalls_Visitor(Resolver resolver, bool co) : base(resolver) { Contract.Requires(resolver != null); this.IsCoContext = co; } protected override bool VisitOneExpr(Expression expr, ref CallingPosition cp) { if (expr is UnaryOpExpr) { var e = (UnaryOpExpr)expr; if (e.Op == UnaryOpExpr.Opcode.Not) { // for the sub-parts, use Invert(cp) cp = Invert(cp); return true; } } else if (expr is BinaryExpr) { var e = (BinaryExpr)expr; switch (e.ResolvedOp) { case BinaryExpr.ResolvedOpcode.And: case BinaryExpr.ResolvedOpcode.Or: return true; // do the sub-parts with the same "cp" case BinaryExpr.ResolvedOpcode.Imp: Visit(e.E0, Invert(cp)); Visit(e.E1, cp); return false; // don't recurse (again) on the sub-parts default: break; } } else if (expr is MatchExpr) { var e = (MatchExpr)expr; Visit(e.Source, CallingPosition.Neither); var theCp = cp; e.Cases.Iter(kase => Visit(kase.Body, theCp)); return false; } else if (expr is ITEExpr) { var e = (ITEExpr)expr; Visit(e.Test, CallingPosition.Neither); Visit(e.Thn, cp); Visit(e.Els, cp); return false; } else if (expr is LetExpr) { var e = (LetExpr)expr; foreach (var rhs in e.RHSs) { Visit(rhs, CallingPosition.Neither); } var cpBody = cp; if (!e.Exact) { // a let-such-that expression introduces an existential that may depend on the _k in an inductive/co predicate, so we disallow recursive calls in the body of the let-such-that if (IsCoContext && cp == CallingPosition.Positive) { cpBody = CallingPosition.Neither; } else if (!IsCoContext && cp == CallingPosition.Negative) { cpBody = CallingPosition.Neither; } } Visit(e.Body, cpBody); return false; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution var cpos = IsCoContext ? cp : Invert(cp); if ((cpos == CallingPosition.Positive && e is ExistsExpr) || (cpos == CallingPosition.Negative && e is ForallExpr)) { if (e.MissingBounds != null && e.MissingBounds.Count != 0) { // To ensure continuity of fixpoint predicates, don't allow calls under an existential (resp. universal) quantifier // for co-predicates (resp. inductive predicates). cp = CallingPosition.Neither; } } Visit(e.LogicalBody(), cp); return false; } else if (expr is StmtExpr) { var e = (StmtExpr)expr; Visit(e.E, cp); Visit(e.S, CallingPosition.Neither); return false; } else if (expr is ConcreteSyntaxExpression) { // do the sub-parts with the same "cp" return true; } // do the sub-parts with cp := Neither cp = CallingPosition.Neither; return true; } } class FixpointPredicateChecks_Visitor : FindFriendlyCalls_Visitor { readonly FixpointPredicate context; public FixpointPredicateChecks_Visitor(Resolver resolver, FixpointPredicate context) : base(resolver, context is CoPredicate) { Contract.Requires(resolver != null); Contract.Requires(context != null); this.context = context; } protected override bool VisitOneExpr(Expression expr, ref CallingPosition cp) { if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; if (ModuleDefinition.InSameSCC(context, e.Function)) { var article = context is InductivePredicate ? "an" : "a"; // we're looking at a recursive call if (!(context is InductivePredicate ? e.Function is InductivePredicate : e.Function is CoPredicate)) { resolver.reporter.Error(MessageSource.Resolver, e, "a recursive call from {0} {1} can go only to other {1}s", article, context.WhatKind); } else if (cp != CallingPosition.Positive) { var msg = string.Format("{0} {1} can be called recursively only in positive positions", article, context.WhatKind); if (cp == CallingPosition.Neither) { // this may be inside an non-friendly quantifier msg += string.Format(" and cannot sit inside an unbounded {0} quantifier", context is InductivePredicate ? "universal" : "existential"); } else { // the fixpoint-call is not inside an quantifier, so don't bother mentioning the part of existentials/universals in the error message } resolver.reporter.Error(MessageSource.Resolver, e, msg); } else { e.CoCall = FunctionCallExpr.CoCallResolution.Yes; resolver.reporter.Info(MessageSource.Resolver, e.tok, e.Function.Name + "#[_k - 1]"); } } // do the sub-parts with cp := Neither cp = CallingPosition.Neither; return true; } return base.VisitOneExpr(expr, ref cp); } protected override bool VisitOneStmt(Statement stmt, ref CallingPosition st) { if (stmt is CallStmt) { var s = (CallStmt)stmt; if (ModuleDefinition.InSameSCC(context, s.Method)) { // we're looking at a recursive call var article = context is InductivePredicate ? "an" : "a"; resolver.reporter.Error(MessageSource.Resolver, stmt.Tok, "a recursive call from {0} {1} can go only to other {1}s", article, context.WhatKind); } // do the sub-parts with the same "cp" return true; } else { return base.VisitOneStmt(stmt, ref st); } } } void FixpointPredicateChecks(Expression expr, FixpointPredicate context, CallingPosition cp) { Contract.Requires(expr != null); Contract.Requires(context != null); var v = new FixpointPredicateChecks_Visitor(this, context); v.Visit(expr, cp); } #endregion FixpointPredicateChecks // ------------------------------------------------------------------------------------------------------ // ----- FixpointLemmaChecks ---------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region FixpointLemmaChecks class FixpointLemmaChecks_Visitor : ResolverBottomUpVisitor { FixpointLemma context; public FixpointLemmaChecks_Visitor(Resolver resolver, FixpointLemma context) : base(resolver) { Contract.Requires(resolver != null); Contract.Requires(context != null); this.context = context; } protected override void VisitOneStmt(Statement stmt) { if (stmt is CallStmt) { var s = (CallStmt)stmt; if (s.Method is FixpointLemma || s.Method is PrefixLemma) { // all is cool } else { // the call goes from a fixpoint-lemma context to a non-fixpoint-lemma callee if (ModuleDefinition.InSameSCC(context, s.Method)) { // we're looking at a recursive call (to a non-fixpoint-lemma) var article = context is InductiveLemma ? "an" : "a"; resolver.reporter.Error(MessageSource.Resolver, s.Tok, "a recursive call from {0} {1} can go only to other {1}s and prefix lemmas", article, context.WhatKind); } } } } protected override void VisitOneExpr(Expression expr) { if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; // the call goes from a colemma context to a non-colemma callee if (ModuleDefinition.InSameSCC(context, e.Function)) { // we're looking at a recursive call (to a non-colemma) resolver.reporter.Error(MessageSource.Resolver, e.tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas"); } } } } void FixpointLemmaChecks(Statement stmt, FixpointLemma context) { Contract.Requires(stmt != null); Contract.Requires(context != null); var v = new FixpointLemmaChecks_Visitor(this, context); v.Visit(stmt); } #endregion FixpointLemmaChecks // ------------------------------------------------------------------------------------------------------ // ----- CheckEqualityTypes ----------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region CheckEqualityTypes class CheckEqualityTypes_Visitor : ResolverTopDownVisitor { public CheckEqualityTypes_Visitor(Resolver resolver) : base(resolver) { Contract.Requires(resolver != null); } protected override bool VisitOneStmt(Statement stmt, ref bool st) { if (stmt.IsGhost) { return false; // no need to recurse to sub-parts, since all sub-parts must be ghost as well } else if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; foreach (var v in s.Locals) { CheckEqualityTypes_Type(v.Tok, v.Type); } } else if (stmt is LetStmt) { var s = (LetStmt)stmt; foreach (var v in s.BoundVars) { CheckEqualityTypes_Type(v.Tok, v.Type); } } else if (stmt is WhileStmt) { var s = (WhileStmt)stmt; // don't recurse on the specification parts, which are ghost if (s.Guard != null) { Visit(s.Guard, st); } // don't recurse on the body, if it's a dirty loop if (s.Body != null) { Visit(s.Body, st); } return false; } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; // don't recurse on the specification parts, which are ghost foreach (var alt in s.Alternatives) { Visit(alt.Guard, st); foreach (var ss in alt.Body) { Visit(ss, st); } } return false; } else if (stmt is CallStmt) { var s = (CallStmt)stmt; Contract.Assert(s.Method.TypeArgs.Count <= s.MethodSelect.TypeArgumentSubstitutions().Count); var i = 0; foreach (var formalTypeArg in s.Method.TypeArgs) { var actualTypeArg = s.MethodSelect.TypeArgumentSubstitutions()[formalTypeArg]; if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, s.Tok, "type parameter {0} ({1}) passed to method {2} must support equality (got {3}){4}", i, formalTypeArg.Name, s.Method.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg)); } i++; } // recursively visit all subexpressions (which are all actual parameters) passed in for non-ghost formal parameters Contract.Assert(s.Lhs.Count == s.Method.Outs.Count); i = 0; foreach (var ee in s.Lhs) { if (!s.Method.Outs[i].IsGhost) { Visit(ee, st); } i++; } Visit(s.Receiver, st); Contract.Assert(s.Args.Count == s.Method.Ins.Count); i = 0; foreach (var ee in s.Args) { if (!s.Method.Ins[i].IsGhost) { Visit(ee, st); } i++; } return false; // we've done what there is to be done } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; foreach (var v in s.BoundVars) { CheckEqualityTypes_Type(v.Tok, v.Type); } // do substatements and subexpressions, except attributes and ensures clauses, since they are not compiled foreach (var ss in s.SubStatements) { Visit(ss, st); } if (s.Range != null) { Visit(s.Range, st); } return false; // we're done } return true; } protected override bool VisitOneExpr(Expression expr, ref bool st) { if (expr is BinaryExpr) { var e = (BinaryExpr)expr; var t0 = e.E0.Type.NormalizeExpand(); var t1 = e.E1.Type.NormalizeExpand(); switch (e.Op) { case BinaryExpr.Opcode.Eq: case BinaryExpr.Opcode.Neq: // First, check a special case: a datatype value (like Nil) that takes no parameters var e0 = e.E0.Resolved as DatatypeValue; var e1 = e.E1.Resolved as DatatypeValue; if (e0 != null && e0.Arguments.Count == 0) { // that's cool } else if (e1 != null && e1.Arguments.Count == 0) { // oh yeah! } else if (!t0.SupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0)); } else if (!t1.SupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, e.E1, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1)); } break; default: switch (e.ResolvedOp) { // Note, all operations on sets, multisets, and maps are guaranteed to work because of restrictions placed on how // these types are instantiated. (Except: This guarantee does not apply to equality on maps, because the Range type // of maps is not restricted, only the Domain type. However, the equality operator is checked above.) case BinaryExpr.ResolvedOpcode.InSeq: case BinaryExpr.ResolvedOpcode.NotInSeq: case BinaryExpr.ResolvedOpcode.Prefix: case BinaryExpr.ResolvedOpcode.ProperPrefix: if (!t1.SupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, e.E1, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1)); } else if (!t0.SupportsEquality) { if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet || e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSeq) { resolver.reporter.Error(MessageSource.Resolver, e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0)); } else { resolver.reporter.Error(MessageSource.Resolver, e.E0, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0)); } } break; default: break; } break; } } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; foreach (var bv in e.BoundVars) { CheckEqualityTypes_Type(bv.tok, bv.Type); } } else if (expr is LetExpr) { var e = (LetExpr)expr; foreach (var bv in e.BoundVars) { CheckEqualityTypes_Type(bv.tok, bv.Type); } } else if (expr is MemberSelectExpr) { var e = (MemberSelectExpr)expr; if (e.Member is Function || e.Member is Method) { var i = 0; foreach (var tp in ((ICallable)e.Member).TypeArgs) { var actualTp = e.TypeApplication[e.Member.EnclosingClass.TypeArgs.Count + i]; if (tp.MustSupportEquality && !actualTp.SupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, e.tok, "type parameter {0} ({1}) passed to {5} '{2}' must support equality (got {3}){4}", i, tp.Name, e.Member.Name, actualTp, TypeEqualityErrorMessageHint(actualTp), e.Member.WhatKind); } i++; } } } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; Contract.Assert(e.Function.TypeArgs.Count <= e.TypeArgumentSubstitutions.Count); var i = 0; foreach (var formalTypeArg in e.Function.TypeArgs) { var actualTypeArg = e.TypeArgumentSubstitutions[formalTypeArg]; if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, e.tok, "type parameter {0} ({1}) passed to function {2} must support equality (got {3}){4}", i, formalTypeArg.Name, e.Function.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg)); } i++; } // recursively visit all subexpressions (which are all actual parameters) passed in for non-ghost formal parameters Visit(e.Receiver, st); Contract.Assert(e.Args.Count == e.Function.Formals.Count); i = 0; foreach (var ee in e.Args) { if (!e.Function.Formals[i].IsGhost) { Visit(ee, st); } i++; } return false; // we've done what there is to be done } else if (expr is SetDisplayExpr || expr is MultiSetDisplayExpr || expr is MapDisplayExpr || expr is MultiSetFormingExpr || expr is StaticReceiverExpr) { // This catches other expressions whose type may potentially be illegal CheckEqualityTypes_Type(expr.tok, expr.Type); } return true; } public void CheckEqualityTypes_Type(IToken tok, Type type) { Contract.Requires(tok != null); Contract.Requires(type != null); type = type.NormalizeExpand(); if (type is BasicType) { // fine } else if (type is SetType) { var st = (SetType)type; var argType = st.Arg; if (!argType.SupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, tok, "{2}set argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType), st.Finite ? "" : "i"); } CheckEqualityTypes_Type(tok, argType); } else if (type is MultiSetType) { var argType = ((MultiSetType)type).Arg; if (!argType.SupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, tok, "multiset argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType)); } CheckEqualityTypes_Type(tok, argType); } else if (type is MapType) { var mt = (MapType)type; if (!mt.Domain.SupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, tok, "{2}map domain type must support equality (got {0}){1}", mt.Domain, TypeEqualityErrorMessageHint(mt.Domain), mt.Finite ? "" : "i"); } CheckEqualityTypes_Type(tok, mt.Domain); CheckEqualityTypes_Type(tok, mt.Range); } else if (type is SeqType) { Type argType = ((SeqType)type).Arg; CheckEqualityTypes_Type(tok, argType); } else if (type is UserDefinedType) { var udt = (UserDefinedType)type; List formalTypeArgs = null; if (udt.ResolvedClass != null) { formalTypeArgs = udt.ResolvedClass.TypeArgs; } else if (udt.ResolvedParam is OpaqueType_AsParameter) { var t = (OpaqueType_AsParameter)udt.ResolvedParam; formalTypeArgs = t.TypeArgs; } if (formalTypeArgs == null) { Contract.Assert(udt.TypeArgs.Count == 0); } else { Contract.Assert(formalTypeArgs.Count == udt.TypeArgs.Count); var i = 0; foreach (var argType in udt.TypeArgs) { var formalTypeArg = formalTypeArgs[i]; if (formalTypeArg.MustSupportEquality && !argType.SupportsEquality) { resolver.reporter.Error(MessageSource.Resolver, tok, "type parameter {0} ({1}) passed to type {2} must support equality (got {3}){4}", i, formalTypeArg.Name, udt.ResolvedClass.Name, argType, TypeEqualityErrorMessageHint(argType)); } CheckEqualityTypes_Type(tok, argType); i++; } } } else if (type is TypeProxy) { // the type was underconstrained; this is checked elsewhere, but it is not in violation of the equality-type test } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } } string TypeEqualityErrorMessageHint(Type argType) { Contract.Requires(argType != null); var tp = argType.AsTypeParameter; if (tp != null) { return string.Format(" (perhaps try declaring type parameter '{0}' on line {1} as '{0}(==)', which says it can only be instantiated with a type that supports equality)", tp.Name, tp.tok.line); } return ""; } } void CheckEqualityTypes_Stmt(Statement stmt) { Contract.Requires(stmt != null); var v = new CheckEqualityTypes_Visitor(this); v.Visit(stmt, false); } void CheckEqualityTypes(Expression expr) { Contract.Requires(expr != null); var v = new CheckEqualityTypes_Visitor(this); v.Visit(expr, false); } public void CheckEqualityTypes_Type(IToken tok, Type type) { Contract.Requires(tok != null); Contract.Requires(type != null); var v = new CheckEqualityTypes_Visitor(this); v.CheckEqualityTypes_Type(tok, type); } #endregion CheckEqualityTypes // ------------------------------------------------------------------------------------------------------ // ----- ComputeGhostInterest --------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region ComputeGhostInterest public void ComputeGhostInterest(Statement stmt, bool mustBeErasable, ICodeContext codeContext) { Contract.Requires(stmt != null); Contract.Requires(codeContext != null); var visitor = new GhostInterest_Visitor(codeContext, this); visitor.Visit(stmt, mustBeErasable); } class GhostInterest_Visitor { readonly ICodeContext codeContext; readonly Resolver resolver; public GhostInterest_Visitor(ICodeContext codeContext, Resolver resolver) { Contract.Requires(codeContext != null); Contract.Requires(resolver != null); this.codeContext = codeContext; this.resolver = resolver; } protected void Error(Statement stmt, string msg, params object[] msgArgs) { Contract.Requires(stmt != null); Contract.Requires(msg != null); Contract.Requires(msgArgs != null); resolver.reporter.Error(MessageSource.Resolver, stmt, msg, msgArgs); } protected void Error(Expression expr, string msg, params object[] msgArgs) { Contract.Requires(expr != null); Contract.Requires(msg != null); Contract.Requires(msgArgs != null); resolver.reporter.Error(MessageSource.Resolver, expr, msg, msgArgs); } protected void Error(IToken tok, string msg, params object[] msgArgs) { Contract.Requires(tok != null); Contract.Requires(msg != null); Contract.Requires(msgArgs != null); resolver.reporter.Error(MessageSource.Resolver, tok, msg, msgArgs); } /// /// This method does three things, in order: /// 0. Sets .IsGhost to "true" if the statement is ghost. This often depends on some guard of the statement /// (like the guard of an "if" statement) or the LHS of the statement (if it is an assignment). /// Note, if "mustBeErasable", then the statement is already in a ghost context. /// statement itself is ghost) or and the statement assigns to a non-ghost field /// 1. Determines if the statement and all its subparts are legal under its computed .IsGhost setting. /// 2. ``Upgrades'' .IsGhost to "true" if, after investigation of the substatements of the statement, it /// turns out that the statement can be erased during compilation. /// Notes: /// * Both step (0) and step (2) sets the .IsGhost field. What step (0) does affects only the /// rules of resolution, whereas step (2) makes a note for the later compilation phase. /// * It is important to do step (0) before step (1)--that is, it is important to set the statement's ghost /// status before descending into its sub-statements--because break statements look at the ghost status of /// its enclosing statements. /// * The method called by a StmtExpr must be ghost; however, this is checked elsewhere. For /// this reason, it is not necessary to visit all subexpressions, unless the subexpression /// matter for the ghost checking/recording of "stmt". /// public void Visit(Statement stmt, bool mustBeErasable) { Contract.Requires(stmt != null); Contract.Assume(!codeContext.IsGhost || mustBeErasable); // (this is really a precondition) codeContext.IsGhost ==> mustBeErasable if (stmt is PredicateStmt) { stmt.IsGhost = true; } else if (stmt is PrintStmt) { var s = (PrintStmt)stmt; if (mustBeErasable) { Error(stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)"); } else { s.Args.Iter(resolver.CheckIsCompilable); } } else if (stmt is BreakStmt) { var s = (BreakStmt)stmt; s.IsGhost = mustBeErasable; if (s.IsGhost && !s.TargetStmt.IsGhost) { var targetIsLoop = s.TargetStmt is WhileStmt || s.TargetStmt is AlternativeLoopStmt; Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure")); } } else if (stmt is ProduceStmt) { var s = (ProduceStmt)stmt; var kind = stmt is YieldStmt ? "yield" : "return"; if (mustBeErasable && !codeContext.IsGhost) { Error(stmt, "{0} statement is not allowed in this context (because it is guarded by a specification-only expression)", kind); } if (s.hiddenUpdate != null) { Visit(s.hiddenUpdate, mustBeErasable); } } else if (stmt is AssignSuchThatStmt) { var s = (AssignSuchThatStmt)stmt; s.IsGhost = mustBeErasable || s.AssumeToken != null || s.Lhss.Any(AssignStmt.LhsIsToGhost); if (mustBeErasable && !codeContext.IsGhost) { foreach (var lhs in s.Lhss) { var gk = AssignStmt.LhsIsToGhost_Which(lhs); if (gk != AssignStmt.NonGhostKind.IsGhost) { Error(lhs, "cannot assign to {0} in a ghost context", AssignStmt.NonGhostKind_To_String(gk)); } } } else if (!mustBeErasable && s.AssumeToken == null && resolver.UsesSpecFeatures(s.Expr)) { foreach (var lhs in s.Lhss) { var gk = AssignStmt.LhsIsToGhost_Which(lhs); if (gk != AssignStmt.NonGhostKind.IsGhost) { Error(lhs, "{0} cannot be assigned a value that depends on a ghost", AssignStmt.NonGhostKind_To_String(gk)); } } } } else if (stmt is UpdateStmt) { var s = (UpdateStmt)stmt; s.ResolvedStatements.Iter(ss => Visit(ss, mustBeErasable)); s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost); } else if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; if (mustBeErasable) { foreach (var local in s.Locals) { // a local variable in a specification-only context might as well be ghost local.IsGhost = true; } } s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost); if (s.Update != null) { Visit(s.Update, mustBeErasable); } } else if (stmt is LetStmt) { var s = (LetStmt)stmt; if (mustBeErasable) { foreach (var bv in s.BoundVars) { bv.IsGhost = true; } } s.IsGhost = s.BoundVars.All(v => v.IsGhost); } else if (stmt is AssignStmt) { var s = (AssignStmt)stmt; var lhs = s.Lhs.Resolved; var gk = AssignStmt.LhsIsToGhost_Which(lhs); if (gk == AssignStmt.NonGhostKind.IsGhost) { s.IsGhost = true; if (s.Rhs is TypeRhs) { Error(s.Rhs.Tok, "'new' is not allowed in ghost contexts"); } } else if (gk == AssignStmt.NonGhostKind.Variable && codeContext.IsGhost) { // cool } else if (mustBeErasable) { Error(stmt, "Assignment to {0} is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)", AssignStmt.NonGhostKind_To_String(gk)); } else if (s.Rhs is ExprRhs) { var rhs = (ExprRhs)s.Rhs; resolver.CheckIsCompilable(rhs.Expr); } else if (s.Rhs is HavocRhs) { // cool } else { var rhs = (TypeRhs)s.Rhs; if (rhs.ArrayDimensions != null) { foreach (var dim in rhs.ArrayDimensions) { resolver.CheckIsCompilable(dim); } } if (rhs.InitCall != null) { foreach (var arg in rhs.InitCall.Args) { resolver.CheckIsCompilable(arg); } } } } else if (stmt is CallStmt) { var s = (CallStmt)stmt; var callee = s.Method; Contract.Assert(callee != null); // follows from the invariant of CallStmt s.IsGhost = callee.IsGhost; // check in-parameters if (mustBeErasable) { if (!s.IsGhost) { Error(s, "only ghost methods can be called from this context"); } } else { resolver.CheckIsCompilable(s.Receiver); int j; if (!callee.IsGhost) { j = 0; foreach (var e in s.Args) { Contract.Assume(j < callee.Ins.Count); // this should have already been checked by the resolver if (!callee.Ins[j].IsGhost) { resolver.CheckIsCompilable(e); } j++; } } j = 0; foreach (var e in s.Lhs) { var resolvedLhs = e.Resolved; if (callee.IsGhost || callee.Outs[j].IsGhost) { // LHS must denote a ghost if (resolvedLhs is IdentifierExpr) { var ll = (IdentifierExpr)resolvedLhs; if (!ll.Var.IsGhost) { if (ll is AutoGhostIdentifierExpr && ll.Var is LocalVariable) { // the variable was actually declared in this statement, so auto-declare it as ghost ((LocalVariable)ll.Var).MakeGhost(); } else { Error(s, "actual out-parameter {0} is required to be a ghost variable", j); } } } else if (resolvedLhs is MemberSelectExpr) { var ll = (MemberSelectExpr)resolvedLhs; if (!ll.Member.IsGhost) { Error(s, "actual out-parameter {0} is required to be a ghost field", j); } } else { // this is an array update, and arrays are always non-ghost Error(s, "actual out-parameter {0} is required to be a ghost variable", j); } } j++; } } } else if (stmt is BlockStmt) { var s = (BlockStmt)stmt; s.IsGhost = mustBeErasable; // set .IsGhost before descending into substatements (since substatements may do a 'break' out of this block) s.Body.Iter(ss => Visit(ss, mustBeErasable)); s.IsGhost = s.IsGhost || s.Body.All(ss => ss.IsGhost); // mark the block statement as ghost if all its substatements are ghost } else if (stmt is IfStmt) { var s = (IfStmt)stmt; s.IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard)); Visit(s.Thn, s.IsGhost); if (s.Els != null) { Visit(s.Els, s.IsGhost); } // if both branches were all ghost, then we can mark the enclosing statement as ghost as well s.IsGhost = s.IsGhost || (s.Thn.IsGhost && (s.Els == null || s.Els.IsGhost)); } else if (stmt is AlternativeStmt) { var s = (AlternativeStmt)stmt; s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard)); s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost))); s.IsGhost = s.IsGhost || s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost)); } else if (stmt is WhileStmt) { var s = (WhileStmt)stmt; s.IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard)); if (s.IsGhost && s.Decreases.Expressions.Exists(e => e is WildcardExpr)) { Error(s, "'decreases *' is not allowed on ghost loops"); } if (s.IsGhost && s.Mod.Expressions != null) { s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); } if (s.Body != null) { Visit(s.Body, s.IsGhost); } s.IsGhost = s.IsGhost || s.Body == null || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Body.IsGhost); } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard)); if (s.IsGhost && s.Decreases.Expressions.Exists(e => e is WildcardExpr)) { Error(s, "'decreases *' is not allowed on ghost loops"); } if (s.IsGhost && s.Mod.Expressions != null) { s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); } s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost))); s.IsGhost = s.IsGhost || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost))); } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; s.IsGhost = mustBeErasable || s.Kind != ForallStmt.ParBodyKind.Assign || resolver.UsesSpecFeatures(s.Range); if (s.Body != null) { Visit(s.Body, s.IsGhost); } s.IsGhost = s.IsGhost || s.Body == null || s.Body.IsGhost; } else if (stmt is ModifyStmt) { var s = (ModifyStmt)stmt; s.IsGhost = mustBeErasable; if (s.IsGhost) { s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); } if (s.Body != null) { Visit(s.Body, mustBeErasable); } } else if (stmt is CalcStmt) { var s = (CalcStmt)stmt; s.IsGhost = true; foreach (var h in s.Hints) { Visit(h, true); } } else if (stmt is MatchStmt) { var s = (MatchStmt)stmt; s.IsGhost = mustBeErasable || resolver.UsesSpecFeatures(s.Source); s.Cases.Iter(kase => kase.Body.Iter(ss => Visit(ss, s.IsGhost))); s.IsGhost = s.IsGhost || s.Cases.All(kase => kase.Body.All(ss => ss.IsGhost)); } else if (stmt is SkeletonStatement) { var s = (SkeletonStatement)stmt; s.IsGhost = mustBeErasable; if (s.S != null) { Visit(s.S, mustBeErasable); s.IsGhost = s.IsGhost || s.S.IsGhost; } } else { Contract.Assert(false); throw new cce.UnreachableException(); } } } #endregion // ------------------------------------------------------------------------------------------------------ // ----- FillInDefaultLoopDecreases --------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region FillInDefaultLoopDecreases class FillInDefaultLoopDecreases_Visitor : ResolverBottomUpVisitor { readonly ICallable EnclosingMethod; public FillInDefaultLoopDecreases_Visitor(Resolver resolver, ICallable enclosingMethod) : base(resolver) { Contract.Requires(resolver != null); Contract.Requires(enclosingMethod != null); EnclosingMethod = enclosingMethod; } protected override void VisitOneStmt(Statement stmt) { if (stmt is WhileStmt) { var s = (WhileStmt)stmt; resolver.FillInDefaultLoopDecreases(s, s.Guard, s.Decreases.Expressions, EnclosingMethod); } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; resolver.FillInDefaultLoopDecreases(s, null, s.Decreases.Expressions, EnclosingMethod); } } } #endregion FillInDefaultLoopDecreases // ------------------------------------------------------------------------------------------------------ // ----- ReportMoreAdditionalInformation ---------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region ReportOtherAdditionalInformation_Visitor class ReportOtherAdditionalInformation_Visitor : ResolverBottomUpVisitor { public ReportOtherAdditionalInformation_Visitor(Resolver resolver) : base(resolver) { Contract.Requires(resolver != null); } protected override void VisitOneStmt(Statement stmt) { if (stmt is ForallStmt) { var s = (ForallStmt)stmt; if (s.Kind == ForallStmt.ParBodyKind.Call) { var cs = (CallStmt)s.S0; // show the callee's postcondition as the postcondition of the 'forall' statement // TODO: The following substitutions do not correctly take into consideration variable capture; hence, what the hover text displays may be misleading var argsSubstMap = new Dictionary(); // maps formal arguments to actuals Contract.Assert(cs.Method.Ins.Count == cs.Args.Count); for (int i = 0; i < cs.Method.Ins.Count; i++) { argsSubstMap.Add(cs.Method.Ins[i], cs.Args[i]); } var substituter = new Translator.AlphaConverting_Substituter(cs.Receiver, argsSubstMap, new Dictionary(), new Translator(resolver.reporter)); foreach (var ens in cs.Method.Ens) { var p = substituter.Substitute(ens.E); // substitute the call's actuals for the method's formals resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(p)); } } } } } #endregion ReportOtherAdditionalInformation_Visitor // ------------------------------------------------------------------------------------------------------ // ------------------------------------------------------------------------------------------------------ // ------------------------------------------------------------------------------------------------------ bool InferRequiredEqualitySupport(TypeParameter tp, Type type) { Contract.Requires(tp != null); Contract.Requires(type != null); type = type.NormalizeExpand(); if (type is BasicType) { } else if (type is SetType) { var st = (SetType)type; return st.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, st.Arg); } else if (type is MultiSetType) { var ms = (MultiSetType)type; return ms.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, ms.Arg); } else if (type is MapType) { var mt = (MapType)type; return mt.Domain.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, mt.Domain) || InferRequiredEqualitySupport(tp, mt.Range); } else if (type is SeqType) { var sq = (SeqType)type; return InferRequiredEqualitySupport(tp, sq.Arg); } else if (type is UserDefinedType) { var udt = (UserDefinedType)type; List formalTypeArgs = null; if (udt.ResolvedClass != null) { formalTypeArgs = udt.ResolvedClass.TypeArgs; } else if (udt.ResolvedParam is OpaqueType_AsParameter) { var t = (OpaqueType_AsParameter)udt.ResolvedParam; formalTypeArgs = t.TypeArgs; } if (formalTypeArgs == null) { Contract.Assert(udt.TypeArgs.Count == 0); } else { Contract.Assert(formalTypeArgs.Count == udt.TypeArgs.Count); var i = 0; foreach (var argType in udt.TypeArgs) { var formalTypeArg = formalTypeArgs[i]; if ((formalTypeArg.MustSupportEquality && argType.AsTypeParameter == tp) || InferRequiredEqualitySupport(tp, argType)) { return true; } i++; } } } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } return false; } ClassDecl currentClass; Method currentMethod; readonly Scope/*!*/ allTypeParameters = new Scope(); readonly Scope/*!*/ scope = new Scope(); Scope/*!*/ labeledStatements = new Scope(); List loopStack = new List(); // the enclosing loops (from which it is possible to break out) /// /// This method resolves the types that have been given after the 'extends' keyword. Then, it populates /// the string->MemberDecl table for "cl" to make sure that all inherited names are accounted for. Further /// checks are done later, elsewhere. /// void RegisterInheritedMembers(ClassDecl cl) { Contract.Requires(cl != null); Contract.Requires(currentClass == null); Contract.Ensures(currentClass == null); currentClass = cl; if (cl.TraitsTyp.Count > 0 && cl.TypeArgs.Count > 0) { reporter.Error(MessageSource.Resolver, cl.tok, "sorry, traits are currently supported only for classes that take no type arguments"); // TODO: do the work to remove this limitation } // Resolve names of traits extended foreach (var tt in cl.TraitsTyp) { var prevErrorCount = reporter.Count(ErrorLevel.Error); ResolveType(cl.tok, tt, new NoContext(cl.Module), ResolveTypeOptionEnum.DontInfer, null); if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { var udt = tt as UserDefinedType; if (udt != null && udt.ResolvedClass is TraitDecl) { var trait = (TraitDecl)udt.ResolvedClass; //disallowing inheritance in multi module case if (cl.Module != trait.Module) { reporter.Error(MessageSource.Resolver, udt.tok, "class '{0}' is in a different module than trait '{1}'. A class may only extend a trait in the same module.", cl.Name, trait.FullName); } else { // all is good cl.TraitsObj.Add(trait); } } else { reporter.Error(MessageSource.Resolver, udt != null ? udt.tok : cl.tok, "a class can only extend traits (found '{0}')", tt); } } } // Inherit members from traits. What we do here is simply to register names, and in particular to register // names that are no already in the class. var members = classMembers[cl]; foreach (var trait in cl.TraitsObj) { foreach (var traitMember in trait.Members) { MemberDecl classMember; if (members.TryGetValue(traitMember.Name, out classMember)) { // the class already declares or inherits a member with this name, so we take no further action at this time } else { // register the trait member in the class members.Add(traitMember.Name, traitMember); } } } currentClass = null; } /// /// Assumes type parameters have already been pushed /// void ResolveClassMemberTypes(ClassDecl cl) { Contract.Requires(cl != null); Contract.Requires(currentClass == null); Contract.Ensures(currentClass == null); currentClass = cl; foreach (MemberDecl member in cl.Members) { member.EnclosingClass = cl; if (member is Field) { // In the following, we pass in a NoContext, because any cycle formed by newtype constraints would have to // involve a non-null object in order to get to the field and its type, and there is no way in a newtype constraint // to obtain a non-null object. ResolveType(member.tok, ((Field)member).Type, new NoContext(cl.Module), ResolveTypeOptionEnum.DontInfer, null); } else if (member is Function) { var f = (Function)member; var ec = reporter.Count(ErrorLevel.Error); allTypeParameters.PushMarker(); ResolveTypeParameters(f.TypeArgs, true, f); ResolveFunctionSignature(f); allTypeParameters.PopMarker(); if (f is FixpointPredicate && ec == reporter.Count(ErrorLevel.Error)) { var ff = ((FixpointPredicate)f).PrefixPredicate; ff.EnclosingClass = cl; allTypeParameters.PushMarker(); ResolveTypeParameters(ff.TypeArgs, true, ff); ResolveFunctionSignature(ff); allTypeParameters.PopMarker(); } } else if (member is Method) { var m = (Method)member; var ec = reporter.Count(ErrorLevel.Error); allTypeParameters.PushMarker(); ResolveTypeParameters(m.TypeArgs, true, m); ResolveMethodSignature(m); allTypeParameters.PopMarker(); var com = m as FixpointLemma; if (com != null && com.PrefixLemma != null && ec == reporter.Count(ErrorLevel.Error)) { var mm = com.PrefixLemma; // resolve signature of the prefix lemma mm.EnclosingClass = cl; allTypeParameters.PushMarker(); ResolveTypeParameters(mm.TypeArgs, true, mm); ResolveMethodSignature(mm); allTypeParameters.PopMarker(); } } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type } } currentClass = null; } void InheritTraitMembers(ClassDecl cl) { Contract.Requires(cl != null); var refinementTransformer = new RefinementTransformer(reporter); //merging class members with parent members if any var clMembers = classMembers[cl]; foreach (TraitDecl trait in cl.TraitsObj) { //merging current class members with the inheriting trait foreach (var traitMember in trait.Members) { var clMember = clMembers[traitMember.Name]; if (clMember == traitMember) { // The member is the one inherited from the trait (and the class does not itself define a member with this name). This // is fine for fields and for functions and methods with bodies. However, for a body-less function or method, the class // is required to at least redeclare the member with its signature. (It should also provide a stronger specification, // but that will be checked by the verifier. And it should also have a body, but that will be checked by the compiler.) if (traitMember is Field) { var field = (Field)traitMember; if (!field.IsGhost) { cl.InheritedMembers.Add(field); } } else if (traitMember is Function) { var func = (Function)traitMember; if (func.Body == null) { reporter.Error(MessageSource.Resolver, cl.tok, "class '{0}' does not implement trait function '{1}.{2}'", cl.Name, trait.Name, traitMember.Name); } else if (!func.IsGhost && !func.IsStatic) { cl.InheritedMembers.Add(func); } } else if (traitMember is Method) { var method = (Method)traitMember; if (method.Body == null) { reporter.Error(MessageSource.Resolver, cl.tok, "class '{0}' does not implement trait method '{1}.{2}'", cl.Name, trait.Name, traitMember.Name); } else if (!method.IsGhost && !method.IsStatic) { cl.InheritedMembers.Add(method); } } } else if (clMember.EnclosingClass != cl) { // The class inherits the member from two places reporter.Error(MessageSource.Resolver, clMember.tok, "member name '{0}' in class '{1}' inherited from both traits '{2}' and '{3}'", traitMember.Name, cl.Name, clMember.EnclosingClass.Name, trait.Name); } else if (traitMember is Field) { // The class is not allowed to do anything with the field other than silently inherit it. if (clMember is Field) { reporter.Error(MessageSource.Resolver, clMember.tok, "field '{0}' is inherited from trait '{1}' and is not allowed to be re-declared", traitMember.Name, trait.Name); } else { reporter.Error(MessageSource.Resolver, clMember.tok, "member name '{0}' in class '{1}' clashes with inherited field from trait '{2}'", traitMember.Name, cl.Name, trait.Name); } } else if (traitMember is Method) { var traitMethod = (Method)traitMember; if (traitMethod.Body != null) { // The method was defined in the trait, so the class is not allowed to do anything with the method other than silently inherit it. reporter.Error(MessageSource.Resolver, clMember.tok, "member '{0}' in class '{1}' overrides fully defined method inherited from trait '{2}'", clMember.Name, cl.Name, trait.Name); } else if (!(clMember is Method)) { reporter.Error(MessageSource.Resolver, clMember.tok, "non-method member '{0}' overrides method '{1}' inherited from trait '{2}'", clMember.Name, traitMethod.Name, trait.Name); } else { var classMethod = (Method)clMember; classMethod.OverriddenMethod = traitMethod; //adding a call graph edge from the trait method to that of class cl.Module.CallGraph.AddEdge(traitMethod, classMethod); refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod); var traitMethodAllowsNonTermination = Contract.Exists(traitMethod.Decreases.Expressions, e => e is WildcardExpr); var classMethodAllowsNonTermination = Contract.Exists(classMethod.Decreases.Expressions, e => e is WildcardExpr); if (classMethodAllowsNonTermination && !traitMethodAllowsNonTermination) { reporter.Error(MessageSource.Resolver, classMethod.tok, "not allowed to override a terminating method with a possibly non-terminating method ('{0}')", classMethod.Name); } } } else if (traitMember is Function) { var traitFunction = (Function)traitMember; if (traitFunction.Body != null) { // The function was defined in the trait, so the class is not allowed to do anything with the function other than silently inherit it. reporter.Error(MessageSource.Resolver, clMember.tok, "member '{0}' in class '{1}' overrides fully defined function inherited from trait '{2}'", clMember.Name, cl.Name, trait.Name); } else if (!(clMember is Function)) { reporter.Error(MessageSource.Resolver, clMember.tok, "non-function member '{0}' overrides function '{1}' inherited from trait '{2}'", clMember.Name, traitFunction.Name, trait.Name); } else { var classFunction = (Function)clMember; classFunction.OverriddenFunction = traitFunction; //adding a call graph edge from the trait method to that of class cl.Module.CallGraph.AddEdge(traitFunction, classFunction); refinementTransformer.CheckOverride_FunctionParameters(classFunction, traitFunction); } } else { Contract.Assert(false); // unexpected member } } } } /// /// Assumes type parameters have already been pushed, and that all types in class members have been resolved /// void ResolveClassMemberBodies(ClassDecl cl) { Contract.Requires(cl != null); Contract.Requires(currentClass == null); Contract.Ensures(currentClass == null); currentClass = cl; foreach (MemberDecl member in cl.Members) { if (member is Field) { ResolveAttributes(member.Attributes, new ResolveOpts(new NoContext(currentClass.Module), false)); // nothing more to do } else if (member is Function) { var f = (Function)member; var ec = reporter.Count(ErrorLevel.Error); allTypeParameters.PushMarker(); ResolveTypeParameters(f.TypeArgs, false, f); ResolveFunction(f); allTypeParameters.PopMarker(); if (f is FixpointPredicate && ec == reporter.Count(ErrorLevel.Error)) { var ff = ((FixpointPredicate)f).PrefixPredicate; allTypeParameters.PushMarker(); ResolveTypeParameters(ff.TypeArgs, false, ff); ResolveFunction(ff); allTypeParameters.PopMarker(); } } else if (member is Method) { var m = (Method)member; var ec = reporter.Count(ErrorLevel.Error); allTypeParameters.PushMarker(); ResolveTypeParameters(m.TypeArgs, false, m); ResolveMethod(m); allTypeParameters.PopMarker(); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type } } currentClass = null; } /// /// Assumes type parameters have already been pushed /// void ResolveCtorTypes(DatatypeDecl/*!*/ dt, Graph/*!*/ dependencies, Graph/*!*/ coDependencies) { Contract.Requires(dt != null); Contract.Requires(dependencies != null); Contract.Requires(coDependencies != null); foreach (DatatypeCtor ctor in dt.Ctors) { ctor.EnclosingDatatype = dt; allTypeParameters.PushMarker(); ResolveCtorSignature(ctor, dt.TypeArgs); allTypeParameters.PopMarker(); if (dt is IndDatatypeDecl) { // The dependencies of interest among inductive datatypes are all (inductive data)types mentioned in the parameter types var idt = (IndDatatypeDecl)dt; dependencies.AddVertex(idt); foreach (Formal p in ctor.Formals) { AddDatatypeDependencyEdge(idt, p.Type, dependencies); } } else { // The dependencies of interest among codatatypes are just the top-level types of parameters. var codt = (CoDatatypeDecl)dt; coDependencies.AddVertex(codt); foreach (var p in ctor.Formals) { var co = p.Type.AsCoDatatype; if (co != null && codt.Module == co.Module) { coDependencies.AddEdge(codt, co); } } } } } void AddDatatypeDependencyEdge(IndDatatypeDecl dt, Type tp, Graph dependencies) { Contract.Requires(dt != null); Contract.Requires(tp != null); Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies)); tp = tp.NormalizeExpand(); var dependee = tp.AsIndDatatype; if (dependee != null && dt.Module == dependee.Module) { dependencies.AddEdge(dt, dependee); foreach (var ta in ((UserDefinedType)tp).TypeArgs) { AddDatatypeDependencyEdge(dt, ta, dependencies); } } } /// /// Check that the SCC of 'startingPoint' can be carved up into stratospheres in such a way that each /// datatype has some value that can be constructed from datatypes in lower stratospheres only. /// The algorithm used here is quadratic in the number of datatypes in the SCC. Since that number is /// deemed to be rather small, this seems okay. /// /// As a side effect of this checking, the DefaultCtor field is filled in (for every inductive datatype /// that passes the check). It may be that several constructors could be used as the default, but /// only the first one encountered as recorded. This particular choice is slightly more than an /// implementation detail, because it affects how certain cycles among inductive datatypes (having /// to do with the types used to instantiate type parameters of datatypes) are used. /// /// The role of the SCC here is simply to speed up this method. It would still be correct if the /// equivalence classes in the given SCC were unions of actual SCC's. In particular, this method /// would still work if "dependencies" consisted of one large SCC containing all the inductive /// datatypes in the module. /// void SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph/*!*/ dependencies) { Contract.Requires(startingPoint != null); Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies)); var scc = dependencies.GetSCC(startingPoint); int totalCleared = 0; while (true) { int clearedThisRound = 0; foreach (var dt in scc) { if (dt.DefaultCtor != null) { // previously cleared } else if (ComputeDefaultCtor(dt)) { Contract.Assert(dt.DefaultCtor != null); // should have been set by the successful call to StratosphereCheck) clearedThisRound++; totalCleared++; } } if (totalCleared == scc.Count) { // all is good return; } else if (clearedThisRound != 0) { // some progress was made, so let's keep going } else { // whatever is in scc-cleared now failed to pass the test foreach (var dt in scc) { if (dt.DefaultCtor == null) { reporter.Error(MessageSource.Resolver, dt, "because of cyclic dependencies among constructor argument types, no instances of datatype '{0}' can be constructed", dt.Name); } } return; } } } /// /// Check that the datatype has some constructor all whose argument types can be constructed. /// Returns 'true' and sets dt.DefaultCtor if that is the case. /// bool ComputeDefaultCtor(IndDatatypeDecl dt) { Contract.Requires(dt != null); Contract.Requires(dt.DefaultCtor == null); // the intention is that this method be called only when DefaultCtor hasn't already been set Contract.Ensures(!Contract.Result() || dt.DefaultCtor != null); // Stated differently, check that there is some constuctor where no argument type goes to the same stratum. DatatypeCtor defaultCtor = null; List lastTypeParametersUsed = null; foreach (DatatypeCtor ctor in dt.Ctors) { List typeParametersUsed = new List(); foreach (Formal p in ctor.Formals) { if (!CheckCanBeConstructed(p.Type, typeParametersUsed)) { // the argument type (has a component which) is not yet known to be constructable goto NEXT_OUTER_ITERATION; } } // this constructor satisfies the requirements, check to see if it is a better fit than the // one found so far. By "better" it means fewer type arguments. Between the ones with // the same number of the type arguments, pick the one shows first. if (defaultCtor == null || typeParametersUsed.Count < lastTypeParametersUsed.Count) { defaultCtor = ctor; lastTypeParametersUsed = typeParametersUsed; } NEXT_OUTER_ITERATION: { } } if (defaultCtor != null) { dt.DefaultCtor = defaultCtor; dt.TypeParametersUsedInConstructionByDefaultCtor = new bool[dt.TypeArgs.Count]; for (int i = 0; i < dt.TypeArgs.Count; i++) { dt.TypeParametersUsedInConstructionByDefaultCtor[i] = lastTypeParametersUsed.Contains(dt.TypeArgs[i]); } return true; } // no constructor satisfied the requirements, so this is an illegal datatype declaration return false; } bool CheckCanBeConstructed(Type tp, List typeParametersUsed) { tp = tp.NormalizeExpand(); var dependee = tp.AsIndDatatype; if (dependee == null) { // the type is not an inductive datatype, which means it is always possible to construct it if (tp.IsTypeParameter) { typeParametersUsed.Add(((UserDefinedType)tp).ResolvedParam); } return true; } else if (dependee.DefaultCtor == null) { // the type is an inductive datatype that we don't yet know how to construct return false; } // also check the type arguments of the inductive datatype Contract.Assert(((UserDefinedType)tp).TypeArgs.Count == dependee.TypeParametersUsedInConstructionByDefaultCtor.Length); var i = 0; foreach (var ta in ((UserDefinedType)tp).TypeArgs) { // note, "tp" is known to be a UserDefinedType, because that follows from tp being an inductive datatype if (dependee.TypeParametersUsedInConstructionByDefaultCtor[i] && !CheckCanBeConstructed(ta, typeParametersUsed)) { return false; } i++; } return true; } void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph/*!*/ dependencies) { Contract.Requires(startingPoint != null); Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies)); var scc = dependencies.GetSCC(startingPoint); // First, the simple case: If any parameter of any inductive datatype in the SCC is of a codatatype type, then // the whole SCC is incapable of providing the equality operation. Also, if any parameter of any inductive datatype // is a ghost, then the whole SCC is incapable of providing the equality operation. foreach (var dt in scc) { Contract.Assume(dt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed); foreach (var ctor in dt.Ctors) { foreach (var arg in ctor.Formals) { var anotherIndDt = arg.Type.AsIndDatatype; if (arg.IsGhost || (anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || arg.Type.IsCoDatatype || arg.Type.IsArrowType || arg.Type.IsIMapType || arg.Type.IsISetType) { // arg.Type is known never to support equality // So, go around the entire SCC and record what we learnt foreach (var ddtt in scc) { ddtt.EqualitySupport = IndDatatypeDecl.ES.Never; } return; // we are done } } } } // Now for the more involved case: we need to determine which type parameters determine equality support for each datatype in the SCC // We start by seeing where each datatype's type parameters are used in a place known to determine equality support. bool thingsChanged = false; foreach (var dt in scc) { if (dt.TypeArgs.Count == 0) { // if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors continue; } foreach (var ctor in dt.Ctors) { foreach (var arg in ctor.Formals) { var typeArg = arg.Type.AsTypeParameter; if (typeArg != null) { typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true; thingsChanged = true; } else { var otherDt = arg.Type.AsIndDatatype; if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) { // datatype is in a different SCC var otherUdt = (UserDefinedType)arg.Type.NormalizeExpand(); var i = 0; foreach (var otherTp in otherDt.TypeArgs) { if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) { var tp = otherUdt.TypeArgs[i].AsTypeParameter; if (tp != null) { tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true; thingsChanged = true; } } } } } } } } // Then we propagate this information up through the SCC while (thingsChanged) { thingsChanged = false; foreach (var dt in scc) { if (dt.TypeArgs.Count == 0) { // if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors continue; } foreach (var ctor in dt.Ctors) { foreach (var arg in ctor.Formals) { var otherDt = arg.Type.AsIndDatatype; if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed) { // otherDt lives in the same SCC var otherUdt = (UserDefinedType)arg.Type.NormalizeExpand(); var i = 0; foreach (var otherTp in otherDt.TypeArgs) { if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) { var tp = otherUdt.TypeArgs[i].AsTypeParameter; if (tp != null && !tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) { tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true; thingsChanged = true; } } i++; } } } } } } // Now that we have computed the .NecessaryForEqualitySupportOfSurroundingInductiveDatatype values, mark the datatypes as ones // where equality support should be checked by looking at the type arguments. foreach (var dt in scc) { dt.EqualitySupport = IndDatatypeDecl.ES.ConsultTypeArguments; } } void ResolveAttributes(Attributes attrs, ResolveOpts opts) { Contract.Requires(opts != null); // order does not matter much for resolution, so resolve them in reverse order foreach (var attr in attrs.AsEnumerable()) { if (attr.Args != null) { foreach (var arg in attr.Args) { Contract.Assert(arg != null); int prevErrors = reporter.Count(ErrorLevel.Error); ResolveExpression(arg, opts); if (prevErrors == reporter.Count(ErrorLevel.Error)) { CheckTypeInference(arg, opts.codeContext); } } } } } void ResolveTypeParameters(List/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) { Contract.Requires(tparams != null); Contract.Requires(parent != null); // push non-duplicated type parameter names int index = 0; foreach (TypeParameter tp in tparams) { if (emitErrors) { // we're seeing this TypeParameter for the first time tp.Parent = parent; tp.PositionalIndex = index; } var r = allTypeParameters.Push(tp.Name, tp); if (emitErrors) { if (r == Scope.PushResult.Duplicate) { reporter.Error(MessageSource.Resolver, tp, "Duplicate type-parameter name: {0}", tp.Name); } else if (r == Scope.PushResult.Shadow) { reporter.Warning(MessageSource.Resolver, tp.tok, "Shadowed type-parameter name: {0}", tp.Name); } } } } void ScopePushAndReport(Scope scope, IVariable v, string kind) { Contract.Requires(scope != null); Contract.Requires(v != null); Contract.Requires(kind != null); ScopePushAndReport(scope, v.Name, v, v.Tok, kind); } void ScopePushAndReport(Scope scope, string name, Thing thing, IToken tok, string kind) where Thing : class { Contract.Requires(scope != null); Contract.Requires(name != null); Contract.Requires(thing != null); Contract.Requires(tok != null); Contract.Requires(kind != null); var r = scope.Push(name, thing); switch (r) { case Scope.PushResult.Success: break; case Scope.PushResult.Duplicate: reporter.Error(MessageSource.Resolver, tok, "Duplicate {0} name: {1}", kind, name); break; case Scope.PushResult.Shadow: reporter.Warning(MessageSource.Resolver, tok, "Shadowed {0} name: {1}", kind, name); break; } } /// /// Assumes type parameters have already been pushed /// void ResolveFunctionSignature(Function f) { Contract.Requires(f != null); scope.PushMarker(); if (f.SignatureIsOmitted) { reporter.Error(MessageSource.Resolver, f, "function signature can be omitted only in refining functions"); } var option = f.TypeArgs.Count == 0 ? new ResolveTypeOption(f) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix); foreach (Formal p in f.Formals) { ScopePushAndReport(scope, p, "parameter"); ResolveType(p.tok, p.Type, f, option, f.TypeArgs); } ResolveType(f.tok, f.ResultType, f, option, f.TypeArgs); scope.PopMarker(); } /// /// Assumes type parameters have already been pushed /// void ResolveFunction(Function f) { Contract.Requires(f != null); scope.PushMarker(); if (f.IsStatic) { scope.AllowInstance = false; } foreach (Formal p in f.Formals) { scope.Push(p.Name, p); } ResolveAttributes(f.Attributes, new ResolveOpts(f, false)); foreach (Expression r in f.Req) { ResolveExpression(r, new ResolveOpts(f, false)); Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(r.Type, Type.Bool, r, "Precondition must be a boolean (got {0})", r.Type); } foreach (FrameExpression fr in f.Reads) { ResolveFrameExpression(fr, true, f); } foreach (Expression r in f.Ens) { ResolveExpression(r, new ResolveOpts(f, false)); // since this is a function, the postcondition is still a one-state predicate Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(r.Type, Type.Bool, r, "Postcondition must be a boolean (got {0})", r.Type); } ResolveAttributes(f.Decreases.Attributes, new ResolveOpts(f, false)); foreach (Expression r in f.Decreases.Expressions) { ResolveExpression(r, new ResolveOpts(f, false)); // any type is fine } SolveAllTypeConstraints(); if (f.Body != null) { var prevErrorCount = reporter.Count(ErrorLevel.Error); ResolveExpression(f.Body, new ResolveOpts(f, false)); SolveAllTypeConstraints(); Contract.Assert(f.Body.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(f.Body.Type, f.ResultType, f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type); } scope.PopMarker(); } /// /// /// /// True indicates "reads", false indicates "modifies". void ResolveFrameExpression(FrameExpression fe, bool readsFrame, ICodeContext codeContext) { Contract.Requires(fe != null); Contract.Requires(codeContext != null); ResolveExpression(fe.E, new ResolveOpts(codeContext, false)); Type t = fe.E.Type; Contract.Assert(t != null); // follows from postcondition of ResolveExpression var arrTy = t.AsArrowType; if (arrTy != null) { t = arrTy.Result; } var collType = t.AsCollectionType; if (collType != null) { t = collType.Arg; } if (!ConstrainTypes(t, new ObjectType(), fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", readsFrame ? "reads" : "modifies", fe.E.Type)) { } else if (fe.FieldName != null) { NonProxyType nptype; MemberDecl member = ResolveMember(fe.E.tok, t, fe.FieldName, out nptype); UserDefinedType ctype = (UserDefinedType)nptype; // correctness of cast follows from the DenotesClass test above if (member == null) { // error has already been reported by ResolveMember } else if (!(member is Field)) { reporter.Error(MessageSource.Resolver, fe.E, "member {0} in type {1} does not refer to a field", fe.FieldName, ctype.Name); } else { Contract.Assert(ctype != null && ctype.ResolvedClass != null); // follows from postcondition of ResolveMember fe.Field = (Field)member; } } } /// /// This method can be called even if the resolution of "fe" failed; in that case, this method will /// not issue any error message. /// void DisallowNonGhostFieldSpecifiers(FrameExpression fe) { Contract.Requires(fe != null); if (fe.Field != null && !fe.Field.IsGhost) { reporter.Error(MessageSource.Resolver, fe.E, "in a ghost context, only ghost fields can be mentioned as modifies frame targets ({0})", fe.FieldName); } } /// /// Assumes type parameters have already been pushed /// void ResolveMethodSignature(Method m) { Contract.Requires(m != null); scope.PushMarker(); if (m.SignatureIsOmitted) { reporter.Error(MessageSource.Resolver, m, "method signature can be omitted only in refining methods"); } var option = m.TypeArgs.Count == 0 ? new ResolveTypeOption(m) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix); // resolve in-parameters foreach (Formal p in m.Ins) { ScopePushAndReport(scope, p, "parameter"); ResolveType(p.tok, p.Type, m, option, m.TypeArgs); } // resolve out-parameters foreach (Formal p in m.Outs) { ScopePushAndReport(scope, p, "parameter"); ResolveType(p.tok, p.Type, m, option, m.TypeArgs); } scope.PopMarker(); } /// /// Assumes type parameters have already been pushed /// void ResolveMethod(Method m) { Contract.Requires(m != null); try { currentMethod = m; // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported scope.PushMarker(); if (m.IsStatic) { scope.AllowInstance = false; } foreach (Formal p in m.Ins) { scope.Push(p.Name, p); } // Start resolving specification... foreach (MaybeFreeExpression e in m.Req) { ResolveAttributes(e.Attributes, new ResolveOpts(m, false)); ResolveExpression(e.E, new ResolveOpts(m, false)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Precondition must be a boolean (got {0})", e.E.Type); } ResolveAttributes(m.Mod.Attributes, new ResolveOpts(m, false)); foreach (FrameExpression fe in m.Mod.Expressions) { ResolveFrameExpression(fe, false, m); if (m is Lemma || m is FixpointLemma) { reporter.Error(MessageSource.Resolver, fe.tok, "{0}s are not allowed to have modifies clauses", m.WhatKind); } else if (m.IsGhost) { DisallowNonGhostFieldSpecifiers(fe); } } ResolveAttributes(m.Decreases.Attributes, new ResolveOpts(m, false)); foreach (Expression e in m.Decreases.Expressions) { ResolveExpression(e, new ResolveOpts(m, false)); // any type is fine } // Add out-parameters to a new scope that will also include the outermost-level locals of the body // Don't care about any duplication errors among the out-parameters, since they have already been reported scope.PushMarker(); if (m is FixpointLemma && m.Outs.Count != 0) { reporter.Error(MessageSource.Resolver, m.Outs[0].tok, "{0}s are not allowed to have out-parameters", m.WhatKind); } else { foreach (Formal p in m.Outs) { scope.Push(p.Name, p); } } // ... continue resolving specification foreach (MaybeFreeExpression e in m.Ens) { ResolveAttributes(e.Attributes, new ResolveOpts(m, true)); ResolveExpression(e.E, new ResolveOpts(m, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Postcondition must be a boolean (got {0})", e.E.Type); } SolveAllTypeConstraints(); // Resolve body if (m.Body != null) { var com = m as FixpointLemma; if (com != null && com.PrefixLemma != null) { // The body may mentioned the implicitly declared parameter _k. Throw it into the // scope before resolving the body. var k = com.PrefixLemma.Ins[0]; scope.Push(k.Name, k); // we expect no name conflict for _k } ResolveBlockStatement(m.Body, m); SolveAllTypeConstraints(); } // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas) ResolveAttributes(m.Attributes, new ResolveOpts(m, false)); scope.PopMarker(); // for the out-parameters and outermost-level locals scope.PopMarker(); // for the in-parameters } finally { currentMethod = null; } } void ResolveCtorSignature(DatatypeCtor ctor, List dtTypeArguments) { Contract.Requires(ctor != null); Contract.Requires(ctor.EnclosingDatatype != null); Contract.Requires(dtTypeArguments != null); foreach (Formal p in ctor.Formals) { // In the following, we pass in a NoContext, because any cycle formed by newtype constraints would have to // involve a non-null object in order to get to the field and its type, and there is no way in a newtype constraint // to obtain a non-null object. ResolveType(p.tok, p.Type, new NoContext(ctor.EnclosingDatatype.Module), ResolveTypeOptionEnum.AllowPrefix, dtTypeArguments); } } /// /// Assumes type parameters have already been pushed /// void ResolveIteratorSignature(IteratorDecl iter) { Contract.Requires(iter != null); scope.PushMarker(); if (iter.SignatureIsOmitted) { reporter.Error(MessageSource.Resolver, iter, "iterator signature can be omitted only in refining methods"); } var option = iter.TypeArgs.Count == 0 ? new ResolveTypeOption(iter) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix); // resolve the types of the parameters foreach (var p in iter.Ins.Concat(iter.Outs)) { ResolveType(p.tok, p.Type, iter, option, iter.TypeArgs); } // resolve the types of the added fields (in case some of these types would cause the addition of default type arguments) foreach (var p in iter.OutsHistoryFields) { ResolveType(p.tok, p.Type, iter, option, iter.TypeArgs); } scope.PopMarker(); } /// /// Assumes type parameters have already been pushed /// void ResolveIterator(IteratorDecl iter) { Contract.Requires(iter != null); Contract.Requires(currentClass == null); Contract.Ensures(currentClass == null); var initialErrorCount = reporter.Count(ErrorLevel.Error); // Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported scope.PushMarker(); scope.AllowInstance = false; // disallow 'this' from use, which means that the special fields and methods added are not accessible in the syntactically given spec iter.Ins.ForEach(p => scope.Push(p.Name, p)); // Start resolving specification... // we start with the decreases clause, because the _decreases fields were only given type proxies before; we'll know // the types only after resolving the decreases clause (and it may be that some of resolution has already seen uses of // these fields; so, with no further ado, here we go Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count); for (int i = 0; i < iter.Decreases.Expressions.Count; i++) { var e = iter.Decreases.Expressions[i]; ResolveExpression(e, new ResolveOpts(iter, false)); // any type is fine, but associate this type with the corresponding _decreases field var d = iter.DecreasesFields[i]; // If the following type constraint does not hold, then: Bummer, there was a use--and a bad use--of the field before, so this won't be the best of error messages ConstrainTypes(d.Type, e.Type, e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type); } foreach (FrameExpression fe in iter.Reads.Expressions) { ResolveFrameExpression(fe, true, iter); } foreach (FrameExpression fe in iter.Modifies.Expressions) { ResolveFrameExpression(fe, false, iter); } foreach (MaybeFreeExpression e in iter.Requires) { ResolveExpression(e.E, new ResolveOpts(iter, false)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Precondition must be a boolean (got {0})", e.E.Type); } scope.PopMarker(); // for the in-parameters // We resolve the rest of the specification in an instance context. So mentions of the in- or yield-parameters // get resolved as field dereferences (with an implicit "this") scope.PushMarker(); currentClass = iter; Contract.Assert(scope.AllowInstance); foreach (MaybeFreeExpression e in iter.YieldRequires) { ResolveExpression(e.E, new ResolveOpts(iter, false)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Yield precondition must be a boolean (got {0})", e.E.Type); } foreach (MaybeFreeExpression e in iter.YieldEnsures) { ResolveExpression(e.E, new ResolveOpts(iter, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type); } foreach (MaybeFreeExpression e in iter.Ensures) { ResolveExpression(e.E, new ResolveOpts(iter, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(e.E.Type, Type.Bool, e.E, "Postcondition must be a boolean (got {0})", e.E.Type); } ResolveAttributes(iter.Attributes, new ResolveOpts(iter, false)); var postSpecErrorCount = reporter.Count(ErrorLevel.Error); // Resolve body if (iter.Body != null) { ResolveBlockStatement(iter.Body, iter); } currentClass = null; scope.PopMarker(); // pop off the AllowInstance setting if (postSpecErrorCount == initialErrorCount) { CreateIteratorMethodSpecs(iter); } } /// /// Assumes the specification of the iterator itself has been successfully resolved. /// void CreateIteratorMethodSpecs(IteratorDecl iter) { Contract.Requires(iter != null); // ---------- here comes the constructor ---------- // same requires clause as the iterator itself iter.Member_Init.Req.AddRange(iter.Requires); // modifies this; iter.Member_Init.Mod.Expressions.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null)); var ens = iter.Member_Init.Ens; foreach (var p in iter.Ins) { // ensures this.x == x; ens.Add(new MaybeFreeExpression(new BinaryExpr(p.tok, BinaryExpr.Opcode.Eq, new MemberSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new IdentifierExpr(p.tok, p.Name)))); } foreach (var p in iter.OutsHistoryFields) { // ensures this.ys == []; ens.Add(new MaybeFreeExpression(new BinaryExpr(p.tok, BinaryExpr.Opcode.Eq, new MemberSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new SeqDisplayExpr(p.tok, new List())))); } // ensures this.Valid(); var valid_call = new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List()); ens.Add(new MaybeFreeExpression(valid_call)); // ensures this._reads == old(ReadsClause); var modSetSingletons = new List(); Expression frameSet = new SetDisplayExpr(iter.tok, true, modSetSingletons); foreach (var fr in iter.Reads.Expressions) { if (fr.FieldName != null) { reporter.Error(MessageSource.Resolver, fr.tok, "sorry, a reads clause for an iterator is not allowed to designate specific fields"); } else if (fr.E.Type.IsRefType) { modSetSingletons.Add(fr.E); } else { frameSet = new BinaryExpr(fr.tok, BinaryExpr.Opcode.Add, frameSet, fr.E); } } ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_reads"), new OldExpr(iter.tok, frameSet)))); // ensures this._modifies == old(ModifiesClause); modSetSingletons = new List(); frameSet = new SetDisplayExpr(iter.tok, true, modSetSingletons); foreach (var fr in iter.Modifies.Expressions) { if (fr.FieldName != null) { reporter.Error(MessageSource.Resolver, fr.tok, "sorry, a modifies clause for an iterator is not allowed to designate specific fields"); } else if (fr.E.Type.IsRefType) { modSetSingletons.Add(fr.E); } else { frameSet = new BinaryExpr(fr.tok, BinaryExpr.Opcode.Add, frameSet, fr.E); } } ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"), new OldExpr(iter.tok, frameSet)))); // ensures this._new == {}; ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), new SetDisplayExpr(iter.tok, true, new List())))); // ensures this._decreases0 == old(DecreasesClause[0]) && ...; Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count); for (int i = 0; i < iter.Decreases.Expressions.Count; i++) { var p = iter.Decreases.Expressions[i]; ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), iter.DecreasesFields[i].Name), new OldExpr(iter.tok, p)))); } // ---------- here comes predicate Valid() ---------- var reads = iter.Member_Valid.Reads; reads.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null)); // reads this; reads.Add(new FrameExpression(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_reads"), null)); // reads this._reads; reads.Add(new FrameExpression(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null)); // reads this._new; // ---------- here comes method MoveNext() ---------- // requires this.Valid(); var req = iter.Member_MoveNext.Req; valid_call = new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List()); req.Add(new MaybeFreeExpression(valid_call)); // requires YieldRequires; req.AddRange(iter.YieldRequires); // modifies this, this._modifies, this._new; var mod = iter.Member_MoveNext.Mod.Expressions; mod.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null)); mod.Add(new FrameExpression(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"), null)); mod.Add(new FrameExpression(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null)); // ensures fresh(_new - old(_new)); ens = iter.Member_MoveNext.Ens; ens.Add(new MaybeFreeExpression(new UnaryOpExpr(iter.tok, UnaryOpExpr.Opcode.Fresh, new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), new OldExpr(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new")))))); // ensures more ==> this.Valid(); valid_call = new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List()); ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, new IdentifierExpr(iter.tok, "more"), valid_call))); // ensures this.ys == if more then old(this.ys) + [this.y] else old(this.ys); Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count); for (int i = 0; i < iter.OutsFields.Count; i++) { var y = iter.OutsFields[i]; var ys = iter.OutsHistoryFields[i]; var ite = new ITEExpr(iter.tok, new IdentifierExpr(iter.tok, "more"), new BinaryExpr(iter.tok, BinaryExpr.Opcode.Add, new OldExpr(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)), new SeqDisplayExpr(iter.tok, new List() { new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), y.Name) })), new OldExpr(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name))); var eq = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name), ite); ens.Add(new MaybeFreeExpression(eq)); } // ensures more ==> YieldEnsures; foreach (var ye in iter.YieldEnsures) { ens.Add(new MaybeFreeExpression( new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, new IdentifierExpr(iter.tok, "more"), ye.E), ye.IsFree)); } // ensures !more ==> Ensures; foreach (var e in iter.Ensures) { ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, new UnaryOpExpr(iter.tok, UnaryOpExpr.Opcode.Not, new IdentifierExpr(iter.tok, "more")), e.E), e.IsFree)); } // decreases this._decreases0, this._decreases1, ...; Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count); for (int i = 0; i < iter.Decreases.Expressions.Count; i++) { var p = iter.Decreases.Expressions[i]; iter.Member_MoveNext.Decreases.Expressions.Add(new MemberSelectExpr(p.tok, new ThisExpr(p.tok), iter.DecreasesFields[i].Name)); } iter.Member_MoveNext.Decreases.Attributes = iter.Decreases.Attributes; } // Like the ResolveTypeOptionEnum, but iff the case of AllowPrefixExtend, it also // contains a pointer to its Parent class, to fill in default type parameters properly. public class ResolveTypeOption { public readonly ResolveTypeOptionEnum Opt; public readonly TypeParameter.ParentType Parent; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant((Opt == ResolveTypeOptionEnum.AllowPrefixExtend) == (Parent != null)); } public ResolveTypeOption(ResolveTypeOptionEnum opt) { Contract.Requires(opt != ResolveTypeOptionEnum.AllowPrefixExtend); Parent = null; Opt = opt; } public ResolveTypeOption(TypeParameter.ParentType parent) { Contract.Requires(parent != null); Opt = ResolveTypeOptionEnum.AllowPrefixExtend; Parent = parent; } } /// /// If ResolveType/ResolveTypeLenient encounters a (datatype or class) type "C" with no supplied arguments, then /// the ResolveTypeOption says what to do. The last three options take a List as a parameter, which (would have /// been supplied as an argument if C# had datatypes instead of just enums, but since C# doesn't) is supplied /// as another parameter (called 'defaultTypeArguments') to ResolveType/ResolveTypeLenient. /// public enum ResolveTypeOptionEnum { /// /// never infer type arguments /// DontInfer, /// /// create a new InferredTypeProxy type for each needed argument /// InferTypeProxies, /// /// if at most defaultTypeArguments.Count type arguments are needed, use a prefix of defaultTypeArguments /// AllowPrefix, /// /// same as AllowPrefix, but if more than defaultTypeArguments.Count type arguments are needed, first /// extend defaultTypeArguments to a sufficient length /// AllowPrefixExtend, } /// /// See ResolveTypeOption for a description of the option/defaultTypeArguments parameters. /// public void ResolveType(IToken tok, Type type, ICodeContext context, ResolveTypeOptionEnum eopt, List defaultTypeArguments) { Contract.Requires(tok != null); Contract.Requires(type != null); Contract.Requires(context != null); Contract.Requires(eopt != ResolveTypeOptionEnum.AllowPrefixExtend); ResolveType(tok, type, context, new ResolveTypeOption(eopt), defaultTypeArguments); } public void ResolveType(IToken tok, Type type, ICodeContext context, ResolveTypeOption option, List defaultTypeArguments) { Contract.Requires(tok != null); Contract.Requires(type != null); Contract.Requires(context != null); Contract.Requires(option != null); Contract.Requires((option.Opt == ResolveTypeOptionEnum.DontInfer || option.Opt == ResolveTypeOptionEnum.InferTypeProxies) == (defaultTypeArguments == null)); var r = ResolveTypeLenient(tok, type, context, option, defaultTypeArguments, false); Contract.Assert(r == null); } public class ResolveTypeReturn { public readonly Type ReplacementType; public readonly ExprDotName LastComponent; public ResolveTypeReturn(Type replacementType, ExprDotName lastComponent) { Contract.Requires(replacementType != null); Contract.Requires(lastComponent != null); ReplacementType = replacementType; LastComponent = lastComponent; } } /// /// See ResolveTypeOption for a description of the option/defaultTypeArguments parameters. /// One more thing: if "allowDanglingDotName" is true, then if the resolution would have produced /// an error message that could have been avoided if "type" denoted an identifier sequence one /// shorter, then return an unresolved replacement type where the identifier sequence is one /// shorter. (In all other cases, the method returns null.) /// public ResolveTypeReturn ResolveTypeLenient(IToken tok, Type type, ICodeContext context, ResolveTypeOption option, List defaultTypeArguments, bool allowDanglingDotName) { Contract.Requires(tok != null); Contract.Requires(type != null); Contract.Requires(context != null); Contract.Requires((option.Opt == ResolveTypeOptionEnum.DontInfer || option.Opt == ResolveTypeOptionEnum.InferTypeProxies) == (defaultTypeArguments == null)); if (type is BasicType) { // nothing to resolve } else if (type is MapType) { var mt = (MapType)type; var errorCount = reporter.Count(ErrorLevel.Error); int typeArgumentCount = 0; if (mt.HasTypeArg()) { ResolveType(tok, mt.Domain, context, option, defaultTypeArguments); ResolveType(tok, mt.Range, context, option, defaultTypeArguments); typeArgumentCount = 2; } else if (option.Opt != ResolveTypeOptionEnum.DontInfer) { var inferredTypeArgs = new List(); FillInTypeArguments(tok, 2, inferredTypeArgs, defaultTypeArguments, option); Contract.Assert(inferredTypeArgs.Count <= 2); if (inferredTypeArgs.Count != 0) { mt.SetTypeArg(inferredTypeArgs[0]); typeArgumentCount++; } if (inferredTypeArgs.Count == 2) { mt.SetRangetype(inferredTypeArgs[1]); typeArgumentCount++; } } // defaults and auto have been applied; check if we now have the right number of arguments if (2 != typeArgumentCount) { reporter.Error(MessageSource.Resolver, tok, "Wrong number of type arguments ({0} instead of 2) passed to type: {1}", typeArgumentCount, mt.CollectionTypeName); // add proxy types, to make sure that MapType will have have a non-null Arg/Domain and Range if (typeArgumentCount == 0) { mt.SetTypeArg(new InferredTypeProxy()); } mt.SetRangetype(new InferredTypeProxy()); } if (errorCount == reporter.Count(ErrorLevel.Error) && (mt.Domain.IsSubrangeType || mt.Range.IsSubrangeType)) { reporter.Error(MessageSource.Resolver, tok, "sorry, cannot instantiate collection type with a subrange type"); } } else if (type is CollectionType) { var t = (CollectionType)type; var errorCount = reporter.Count(ErrorLevel.Error); if (t.HasTypeArg()) { ResolveType(tok, t.Arg, context, option, defaultTypeArguments); } else if (option.Opt != ResolveTypeOptionEnum.DontInfer) { var inferredTypeArgs = new List(); FillInTypeArguments(tok, 1, inferredTypeArgs, defaultTypeArguments, option); if (inferredTypeArgs.Count != 0) { Contract.Assert(inferredTypeArgs.Count == 1); t.SetTypeArg(inferredTypeArgs[0]); } } if (!t.HasTypeArg()) { // defaults and auto have been applied; check if we now have the right number of arguments reporter.Error(MessageSource.Resolver, tok, "Wrong number of type arguments (0 instead of 1) passed to type: {0}", t.CollectionTypeName); // add a proxy type, to make sure that CollectionType will have have a non-null Arg t.SetTypeArg(new InferredTypeProxy()); } if (errorCount == reporter.Count(ErrorLevel.Error) && t.Arg.IsSubrangeType) { reporter.Error(MessageSource.Resolver, tok, "sorry, cannot instantiate collection type with a subrange type"); } } else if (type is UserDefinedType) { var t = (UserDefinedType)type; if (t.ResolvedClass != null || t.ResolvedParam != null) { // Apparently, this type has already been resolved return null; } var prevErrorCount = reporter.Count(ErrorLevel.Error); if (t.NamePath is ExprDotName) { var ret = ResolveDotSuffix_Type((ExprDotName)t.NamePath, new ResolveOpts(context, true), allowDanglingDotName, option, defaultTypeArguments); if (ret != null) { return ret; } } else { var s = (NameSegment)t.NamePath; ResolveNameSegment_Type(s, new ResolveOpts(context, true), option, defaultTypeArguments); } if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { var r = t.NamePath.Resolved as Resolver_IdentifierExpr; if (r == null || !(r.Type is Resolver_IdentifierExpr.ResolverType_Type)) { reporter.Error(MessageSource.Resolver, t.tok, "expected type"); } else if (r.Type is Resolver_IdentifierExpr.ResolverType_Type && r.TypeParamDecl != null) { t.ResolvedParam = r.TypeParamDecl; } else if (r.Type is Resolver_IdentifierExpr.ResolverType_Type) { var d = r.Decl; if (d is OpaqueTypeDecl) { var dd = (OpaqueTypeDecl)d; if (dd.Module.ClonedFrom != null && dd.Module.ClonedFrom.ExclusiveRefinement != null) { t.ResolvedParam = ((OpaqueTypeDecl)dd.ClonedFrom).TheType; t.ResolvedClass = d; // Store the decl, so the compiler will generate the fully qualified name } else { t.ResolvedParam = ((OpaqueTypeDecl)d).TheType; // resolve like a type parameter, and it may have type parameters if it's an opaque type t.ResolvedClass = d; // Store the decl, so the compiler will generate the fully qualified name } } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (DafnyOptions.O.IronDafny) { while (dd.ClonedFrom != null) { dd = (NewtypeDecl)d.ClonedFrom; } } var caller = context as ICallable; if (caller != null) { caller.EnclosingModule.CallGraph.AddEdge(caller, dd); if (caller == dd) { // detect self-loops here, since they don't show up in the graph's SSC methods reporter.Error(MessageSource.Resolver, dd.tok, "recursive dependency involving a newtype: {0} -> {0}", dd.Name); } } t.ResolvedClass = dd; } else { // d is a class or datatype, and it may have type parameters t.ResolvedClass = d; } if (option.Opt == ResolveTypeOptionEnum.DontInfer) { // don't add anything } else if (d.TypeArgs.Count != t.TypeArgs.Count && t.TypeArgs.Count == 0) { FillInTypeArguments(t.tok, d.TypeArgs.Count, t.TypeArgs, defaultTypeArguments, option); } // defaults and auto have been applied; check if we now have the right number of arguments if (d.TypeArgs.Count != t.TypeArgs.Count) { reporter.Error(MessageSource.Resolver, t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to {2}: {3}", t.TypeArgs.Count, d.TypeArgs.Count, d.WhatKind, t.Name); } } } } else if (type is TypeProxy) { TypeProxy t = (TypeProxy)type; if (t.T != null) { ResolveType(tok, t.T, context, option, defaultTypeArguments); } } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } return null; } /// /// Adds to "typeArgs" a list of "n" type arguments, possibly extending "defaultTypeArguments". /// static void FillInTypeArguments(IToken tok, int n, List typeArgs, List defaultTypeArguments, ResolveTypeOption option) { Contract.Requires(tok != null); Contract.Requires(0 <= n); Contract.Requires(typeArgs != null && typeArgs.Count == 0); if (option.Opt == ResolveTypeOptionEnum.InferTypeProxies) { // add type arguments that will be inferred for (int i = 0; i < n; i++) { typeArgs.Add(new InferredTypeProxy()); } } else if (option.Opt == ResolveTypeOptionEnum.AllowPrefix && defaultTypeArguments.Count < n) { // there aren't enough default arguments, so don't do anything } else { // we'll add arguments if (option.Opt == ResolveTypeOptionEnum.AllowPrefixExtend) { // extend defaultTypeArguments, if needed for (int i = defaultTypeArguments.Count; i < n; i++) { var tp = new TypeParameter(tok, "_T" + i, i, option.Parent); defaultTypeArguments.Add(tp); } } Contract.Assert(n <= defaultTypeArguments.Count); // automatically supply a prefix of the arguments from defaultTypeArguments for (int i = 0; i < n; i++) { typeArgs.Add(new UserDefinedType(defaultTypeArguments[i])); } } } public bool UnifyTypes(Type a, Type b) { Contract.Requires(a != null); Contract.Requires(b != null); a = a.NormalizeExpand(); b = b.NormalizeExpand(); if (a is TypeProxy) { // merge a and b (cycles are avoided even if b is a TypeProxy, since we have got to the bottom of both a and b) return AssignProxy((TypeProxy)a, b); } else if (b is TypeProxy) { // merge a and b return AssignProxy((TypeProxy)b, a); } #if !NO_CHEAP_OBJECT_WORKAROUND if (a is ObjectType || b is ObjectType) { // TODO: remove this temporary hack var other = a is ObjectType ? b : a; if (!other.IsRefType) { return false; } // allow anything else with object; this is BOGUS return true; } #endif // Now, a and b are non-proxies and stand for the same things as the original a and b, respectively. if (a is BoolType) { return b is BoolType; } else if (a is CharType) { return b is CharType; } else if (a is IntType) { return b is IntType; } else if (a is RealType) { return b is RealType; } else if (a is ObjectType) { return b is ObjectType; } else if (a is SetType) { return b is SetType && ((SetType)a).Finite == ((SetType)b).Finite && UnifyTypes(((SetType)a).Arg, ((SetType)b).Arg); } else if (a is MultiSetType) { return b is MultiSetType && UnifyTypes(((MultiSetType)a).Arg, ((MultiSetType)b).Arg); } else if (a is MapType) { return b is MapType && ((MapType)a).Finite == ((MapType)b).Finite && UnifyTypes(((MapType)a).Domain, ((MapType)b).Domain) && UnifyTypes(((MapType)a).Range, ((MapType)b).Range); } else if (a is SeqType) { return b is SeqType && UnifyTypes(((SeqType)a).Arg, ((SeqType)b).Arg); } else if (a is UserDefinedType || b is UserDefinedType) { if (!(a is UserDefinedType) && b is UserDefinedType) { var x = a; a = b; b = x; } var aa = (UserDefinedType)a; var rca = aa.ResolvedClass; // traits are currently unfriendly to irondafny features. if (DafnyOptions.O.IronDafny && !(rca is TraitDecl)) { if (rca != null) { while (rca.ClonedFrom != null || rca.ExclusiveRefinement != null) { if (rca.ClonedFrom != null) { rca = (TopLevelDecl)rca.ClonedFrom; } else { Contract.Assert(rca.ExclusiveRefinement != null); rca = rca.ExclusiveRefinement; } } } } if (!(b is UserDefinedType)) { return DafnyOptions.O.IronDafny && rca is TypeSynonymDecl && UnifyTypes(((TypeSynonymDecl)rca).Rhs, b); } var bb = (UserDefinedType)b; var rcb = bb.ResolvedClass; // traits are currently unfriendly to irondafny features. if (DafnyOptions.O.IronDafny && !(rca is TraitDecl) && !(rcb is TraitDecl)) { if (rcb != null) { while (rcb.ClonedFrom != null || rcb.ExclusiveRefinement != null) { if (rcb.ClonedFrom != null) { rcb = (TopLevelDecl)rcb.ClonedFrom; } else { Contract.Assert(rcb.ExclusiveRefinement != null); rcb = rcb.ExclusiveRefinement; } } } if (rca is TypeSynonymDecl || rcb is TypeSynonymDecl) { var aaa = a; var bbb = b; if (rca is TypeSynonymDecl) { aaa = ((TypeSynonymDecl)rca).Rhs; } if (rcb is TypeSynonymDecl) { bbb = ((TypeSynonymDecl)rcb).Rhs; } return UnifyTypes(aaa, bbb); } } if (rca != null && Object.ReferenceEquals(rca, rcb)) { // these are both resolved class/datatype types Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count); bool successSoFar = true; for (int i = 0; successSoFar && i < aa.TypeArgs.Count; i++) { successSoFar = UnifyTypes(aa.TypeArgs[i], bb.TypeArgs[i]); } return successSoFar; } else if (rcb is TraitDecl && rca is TraitDecl) { return rca == rcb; } else if (rcb is ClassDecl && rca is TraitDecl) { return ((ClassDecl)rcb).TraitsObj.Contains(rca); } else if (rca is ClassDecl && rcb is TraitDecl) { return ((ClassDecl)rca).TraitsObj.Contains(rcb); } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) { // type parameters if (aa.TypeArgs.Count != bb.TypeArgs.Count) { return false; } else { bool successSoFar = true; for (int i = 0; i < aa.TypeArgs.Count; i++) { if (!UnifyTypes(aa.TypeArgs[i], bb.TypeArgs[i])) { successSoFar = false; } } return successSoFar; } } else { // something is wrong; either aa or bb wasn't properly resolved, or they don't unify return false; } } else if (a is Resolver_IdentifierExpr.ResolverType_Type) { return b is Resolver_IdentifierExpr.ResolverType_Type; } else if (a is Resolver_IdentifierExpr.ResolverType_Module) { return b is Resolver_IdentifierExpr.ResolverType_Module; } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } } bool AssignProxy(TypeProxy proxy, Type t) { Contract.Requires(proxy != null); Contract.Requires(t != null); Contract.Requires(proxy.T == null); Contract.Requires(!(t is TypeProxy) || ((TypeProxy)t).T == null); //modifies proxy.T, ((TypeProxy)t).T; // might also change t.T if t is a proxy Contract.Ensures(Contract.Result() == (proxy == t || proxy.T != null || (t is TypeProxy && ((TypeProxy)t).T != null))); if (proxy == t) { // they are already in the same equivalence class return true; } else if (proxy is UnrestrictedTypeProxy) { // it's fine to redirect proxy to t (done below) } else if (t is UnrestrictedTypeProxy) { // merge proxy and t by redirecting t to proxy, rather than the other way around ((TypeProxy)t).T = proxy; return true; } else if (t is RestrictedTypeProxy) { // Both proxy and t are restricted type proxies. To simplify unification, order proxy and t // according to their types. RestrictedTypeProxy r0 = (RestrictedTypeProxy)proxy; RestrictedTypeProxy r1 = (RestrictedTypeProxy)t; if (r0.OrderID <= r1.OrderID) { return AssignRestrictedProxies(r0, r1); } else { return AssignRestrictedProxies(r1, r0); } // In the remaining cases, proxy is a restricted proxy and t is a non-proxy } else if (proxy is DatatypeProxy) { var dtp = (DatatypeProxy)proxy; if (!dtp.Co && t.NormalizeExpand().IsIndDatatype) { // all is fine, proxy can be redirected to t } else if (dtp.Co && t.IsCoDatatype) { // all is fine, proxy can be redirected to t } else if (dtp.TypeVariableOK && t.IsTypeParameter) { // looking good } else { return false; } } else if (proxy is ObjectTypeProxy) { if (t is ArrowType) { return false; } else if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) { // all is fine, proxy can be redirected to t } else { return false; } } else if (proxy is CollectionTypeProxy) { CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy; if (t is CollectionType) { if (!UnifyTypes(collProxy.Arg, ((CollectionType)t).Arg)) { return false; } } else { return false; } } else if (proxy is OperationTypeProxy) { var opProxy = (OperationTypeProxy)proxy; if (opProxy.AllowInts && t.IsNumericBased(Type.NumericPersuation.Int)) { // fine } else if (opProxy.AllowReals && t.IsNumericBased(Type.NumericPersuation.Real)) { // fine } else if (opProxy.AllowChar && t is CharType) { // fine } else if (opProxy.AllowSetVarieties && ((t is SetType && ((SetType)t).Finite) || t is MultiSetType)) { // fine } else if (opProxy.AllowISet && (t is SetType && !((SetType)t).Finite)) { // fine } else if (opProxy.AllowSeq && t is SeqType) { // fine } else { return false; } } else if (proxy is IndexableTypeProxy) { var iProxy = (IndexableTypeProxy)proxy; if (t is SeqType) { if (!UnifyTypes(iProxy.Domain, new OperationTypeProxy(true, false, false, false, false, false))) { return false; } else if (!UnifyTypes(iProxy.Range, ((SeqType)t).Arg)) { return false; } else if (!UnifyTypes(iProxy.Arg, iProxy.Range)) { return false; } } else if (iProxy.AllowArray && t.IsArrayType && t.AsArrayType.Dims == 1) { Type elType = UserDefinedType.ArrayElementType(t); if (!UnifyTypes(iProxy.Domain, new OperationTypeProxy(true, false, false, false, false, false))) { return false; } else if (!UnifyTypes(iProxy.Range, elType)) { return false; } else if (!UnifyTypes(iProxy.Arg, iProxy.Range)) { return false; } } else if (iProxy.AllowMap && t is MapType && ((MapType)t).Finite) { if (!UnifyTypes(iProxy.Domain, ((MapType)t).Domain)) { return false; } else if (!UnifyTypes(iProxy.Range, ((MapType)t).Range)) { return false; } else if (!UnifyTypes(iProxy.Arg, iProxy.Domain)) { return false; } } else if (iProxy.AllowIMap && t is MapType && !((MapType)t).Finite) { if (!UnifyTypes(iProxy.Domain, ((MapType)t).Domain)) { return false; } else if (!UnifyTypes(iProxy.Range, ((MapType)t).Range)) { return false; } else if (!UnifyTypes(iProxy.Arg, iProxy.Domain)) { return false; } } else if (t is MultiSetType) { if (!UnifyTypes(iProxy.Domain, ((MultiSetType)t).Arg)) { return false; } else if (!UnifyTypes(iProxy.Range, new OperationTypeProxy(true, false, false, false, false, false))) { return false; } else if (!UnifyTypes(iProxy.Arg, iProxy.Domain)) { return false; } } else { return false; } } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected proxy type } // do the merge, but never infer a subrange type if (t is NatType) { proxy.T = Type.Int; } else { return AssignProxyAfterCycleCheck(proxy, t); } return true; } bool AssignProxyAfterCycleCheck(TypeProxy proxy, Type t) { Contract.Requires(proxy != null && proxy.T == null); Contract.Requires(t != null); if (TypeArgumentsIncludeProxy(t, proxy)) { return false; } else { proxy.T = t; return true; } } bool TypeArgumentsIncludeProxy(Type t, TypeProxy proxy) { Contract.Requires(t != null); Contract.Requires(proxy != null); foreach (var ta in t.TypeArgs) { var a = ta.Normalize(); if (a == proxy || TypeArgumentsIncludeProxy(a, proxy)) { return true; } } return false; } bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b) { Contract.Requires(a != null); Contract.Requires(b != null); Contract.Requires(a != b); Contract.Requires(a.T == null && b.T == null); Contract.Requires(a.OrderID <= b.OrderID); //modifies a.T, b.T; Contract.Ensures(!Contract.Result() || a.T != null || b.T != null); if (a is DatatypeProxy) { if (b is DatatypeProxy && ((DatatypeProxy)a).Co == ((DatatypeProxy)b).Co) { // all is fine a.T = b; return true; } else { return false; } } else if (a is ObjectTypeProxy) { if (b is ObjectTypeProxy) { // all is fine a.T = b; return true; } else if (b is IndexableTypeProxy && ((IndexableTypeProxy)b).AllowArray) { var ib = (IndexableTypeProxy)b; // the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type // Note, we're calling ResolvedArrayType here, which in turn calls ResolveType on ib.Arg. However, we // don't need to worry about what ICodeContext we're passing in, because ib.Arg should already have been // resolved. var c = ResolvedArrayType(Token.NoToken, 1, ib.Arg, new DontUseICallable()); return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c) && UnifyTypes(ib.Arg, ib.Range); } else { return false; } } else if (a is CollectionTypeProxy) { if (b is CollectionTypeProxy) { var argUnificationSuccess = UnifyTypes(((CollectionTypeProxy)a).Arg, ((CollectionTypeProxy)b).Arg); if (argUnificationSuccess) { a.T = b; } return argUnificationSuccess; } else if (b is OperationTypeProxy) { var proxy = (OperationTypeProxy)b; if (proxy.AllowSeq && proxy.AllowSetVarieties && proxy.AllowISet) { b.T = a; // a is a stronger constraint than b } else { // a says set,seq and b says numeric,set; the intersection is set var c = new SetType(true, ((CollectionTypeProxy)a).Arg); return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c); } return true; } else if (b is IndexableTypeProxy) { var pa = (CollectionTypeProxy)a; var ib = (IndexableTypeProxy)b; // pa is: // set(Arg) or iset(Arg) or multiset(Arg) or seq(Arg) or map(Arg, anyRange) or imap(Arg, anyRange) // ib is: // multiset(Arg) or // seq(Arg) or // if AllowMap, map(Domain, Arg), or // if AllowIMap, imap(Domain, Arg), or // if AllowArray, array(Arg) // Their intersection is: if (ib.AllowArray) { var c = new IndexableTypeProxy(ib.Domain, ib.Range, ib.Arg, ib.AllowMap, ib.AllowIMap, false); ib.T = c; ib = c; } pa.T = ib; return UnifyTypes(pa.Arg, ib.Arg); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type } } else if (a is OperationTypeProxy) { var pa = (OperationTypeProxy)a; if (b is OperationTypeProxy) { var pb = (OperationTypeProxy)b; var i = pa.AllowInts && pb.AllowInts; var r = pa.AllowReals && pb.AllowReals; var h = pa.AllowChar && pb.AllowChar; var q = pa.AllowSeq && pb.AllowSeq; var s = pa.AllowSetVarieties && pb.AllowSetVarieties; var t = pa.AllowISet && pb.AllowISet; if (!i && !r && !h && !q && !s && !t) { // over-constrained return false; } else if (i == pa.AllowInts && r == pa.AllowReals && h == pa.AllowChar && q == pa.AllowSeq && s == pa.AllowSetVarieties && t == pa.AllowISet) { b.T = a; // a has the stronger requirement } else if (i == pb.AllowInts && r == pb.AllowReals && h == pb.AllowChar && q == pb.AllowSeq && s == pb.AllowSetVarieties && t == pb.AllowISet) { a.T = b; // b has the stronger requirement } else { Type c = !i && !r && h && !q && !s && !t? new CharType() : (Type)new OperationTypeProxy(i, r, h, q, s, t); // the calls to AssignProxyAfterCycleCheck are needed only when c is a non-proxy type, but it doesn't // hurt to do them in both cases return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c); } return true; } else { var ib = (IndexableTypeProxy)b; // cast justification: else we have unexpected restricted-proxy type // a is: possibly numeric, possibly char, possibly seq, possibly set or multiset // b is: seq, multiset, possibly map, possibly array -- with some constraints about the type parameterization // So, the intersection could include multiset and seq. if (pa.AllowSetVarieties && !pa.AllowSeq) { // strengthen a and b to a multiset type var c = new MultiSetType(ib.Arg); return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c); } else if (pa.AllowSeq && !pa.AllowSetVarieties) { // strengthen a and b to a sequence type var c = new SeqType(ib.Arg); return AssignProxyAfterCycleCheck(a, c) && AssignProxyAfterCycleCheck(b, c); } else if (!pa.AllowSeq && !pa.AllowSetVarieties) { // over-constrained return false; } else { Contract.Assert(pa.AllowSeq && pa.AllowSetVarieties); // the only case left if (ib.AllowMap || ib.AllowIMap || ib.AllowArray) { var c = new IndexableTypeProxy(ib.Domain, ib.Range, ib.Arg, false, false, false); a.T = c; b.T = c; } else { a.T = b; } return true; } } } else if (a is IndexableTypeProxy) { var ia = (IndexableTypeProxy)a; var ib = (IndexableTypeProxy)b; // cast justification: else we have unexpected restricted-proxy type var am = ia.AllowMap && ib.AllowMap; var aim = ia.AllowIMap && ib.AllowIMap; var ar = ia.AllowArray && ib.AllowArray; if (am == ia.AllowMap && aim == ia.AllowIMap && ar == ia.AllowArray) { b.T = a; // a has the stronger requirement } else if (am == ib.AllowMap && aim == ib.AllowIMap && ar == ib.AllowArray) { a.T = b; // b has the stronger requirement } else { var c = new IndexableTypeProxy(ia.Domain, ia.Range, ia.Arg, am, aim, ar); a.T = c; b.T = c; } return UnifyTypes(ia.Domain, ib.Domain) && UnifyTypes(ia.Range, ib.Range) && UnifyTypes(ia.Arg, ib.Arg); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type } } /// /// Returns a resolved type denoting an array type with dimension "dims" and element type "arg". /// Callers are expected to provide "arg" as an already resolved type. (Note, a proxy type is resolved-- /// only types that contain identifiers stand the possibility of not being resolved.) /// Type ResolvedArrayType(IToken tok, int dims, Type arg, ICodeContext context) { Contract.Requires(tok != null); Contract.Requires(1 <= dims); Contract.Requires(arg != null); var at = builtIns.ArrayType(tok, dims, new List { arg }, false); ResolveType(tok, at, context, ResolveTypeOptionEnum.DontInfer, null); return at; } public void ResolveStatement(Statement stmt, ICodeContext codeContext) { Contract.Requires(stmt != null); Contract.Requires(codeContext != null); if (!(stmt is ForallStmt)) { // forall statements do their own attribute resolution below ResolveAttributes(stmt.Attributes, new ResolveOpts(codeContext, true)); } if (stmt is PredicateStmt) { PredicateStmt s = (PredicateStmt)stmt; ResolveExpression(s.Expr, new ResolveOpts(codeContext, true)); Contract.Assert(s.Expr.Type != null); // follows from postcondition of ResolveExpression ConstrainTypes(s.Expr.Type, Type.Bool, s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type); } else if (stmt is PrintStmt) { var s = (PrintStmt)stmt; var opts = new ResolveOpts(codeContext, false); s.Args.Iter(e => ResolveExpression(e, opts)); } else if (stmt is BreakStmt) { var s = (BreakStmt)stmt; if (s.TargetLabel != null) { Statement target = labeledStatements.Find(s.TargetLabel); if (target == null) { reporter.Error(MessageSource.Resolver, s, "break label is undefined or not in scope: {0}", s.TargetLabel); } else { s.TargetStmt = target; } } else { if (loopStack.Count < s.BreakCount) { reporter.Error(MessageSource.Resolver, s, "trying to break out of more loop levels than there are enclosing loops"); } else { Statement target = loopStack[loopStack.Count - s.BreakCount]; if (target.Labels == null) { // make sure there is a label, because the compiler and translator will want to see a unique ID target.Labels = new LList