//----------------------------------------------------------------------------- // // 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 ResolutionErrorReporter { public int ErrorCount = 0; /// /// This method is virtual, because it is overridden in the VSX plug-in for Dafny. /// public virtual void Error(IToken tok, string msg, params object[] args) { Contract.Requires(tok != null); Contract.Requires(msg != null); ConsoleColor col = Console.ForegroundColor; Console.ForegroundColor = ConsoleColor.Red; Console.WriteLine("{0}({1},{2}): Error: {3}", DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1, string.Format(msg, args)); Console.ForegroundColor = col; ErrorCount++; } public void Error(Declaration d, string msg, params object[] args) { Contract.Requires(d != null); Contract.Requires(msg != null); Error(d.tok, msg, args); } public void Error(Statement s, string msg, params object[] args) { Contract.Requires(s != null); Contract.Requires(msg != null); Error(s.Tok, msg, args); } public void Error(NonglobalVariable v, string msg, params object[] args) { Contract.Requires(v != null); Contract.Requires(msg != null); Error(v.tok, msg, args); } public void Error(Expression e, string msg, params object[] args) { Contract.Requires(e != null); Contract.Requires(msg != null); Error(e.tok, msg, args); } public void Warning(IToken tok, string msg, params object[] args) { Contract.Requires(tok != null); Contract.Requires(msg != null); ConsoleColor col = Console.ForegroundColor; Console.ForegroundColor = ConsoleColor.Yellow; Console.WriteLine("{0}({1},{2}): Warning: {3}", DafnyOptions.Clo.UseBaseNameForFileName ? System.IO.Path.GetFileName(tok.filename) : tok.filename, tok.line, tok.col - 1, string.Format(msg, args)); Console.ForegroundColor = col; } } public struct AdditionalInformation { public IToken Token; public string Text; public int Length; } public class Resolver : ResolutionErrorReporter { readonly BuiltIns builtIns; ModuleSignature moduleInfo = null; public Action AdditionalInformationReporter; internal void ReportAdditionalInformation(IToken token, string text, int length) { Contract.Requires(token != null); Contract.Requires(text != null); Contract.Requires(0 <= length); if (AdditionalInformationReporter != null) { AdditionalInformationReporter(new AdditionalInformation { Token = token, Text = text, Length = length }); } } class AmbiguousTopLevelDecl : TopLevelDecl // only used with "classes" { readonly TopLevelDecl A; readonly TopLevelDecl B; public AmbiguousTopLevelDecl(ModuleDefinition m, TopLevelDecl a, TopLevelDecl b) : base(a.tok, a.Name + "/" + b.Name, m, new List(), null) { A = a; B = b; } public string ModuleNames() { string nm; if (A is AmbiguousTopLevelDecl) { nm = ((AmbiguousTopLevelDecl)A).ModuleNames(); } else { nm = A.Module.Name; } if (B is AmbiguousTopLevelDecl) { nm += ", " + ((AmbiguousTopLevelDecl)B).ModuleNames(); } else { nm += ", " + B.Module.Name; } return nm; } } class AmbiguousMemberDecl : MemberDecl // only used with "classes" { readonly MemberDecl A; readonly MemberDecl B; public AmbiguousMemberDecl(ModuleDefinition m, MemberDecl a, MemberDecl b) : base(a.tok, a.Name + "/" + b.Name, a.IsStatic, a.IsGhost, null) { A = a; B = b; } public string ModuleNames() { string nm; if (A is AmbiguousMemberDecl) { nm = ((AmbiguousMemberDecl)A).ModuleNames(); } else { nm = A.EnclosingClass.Module.Name; } if (B is AmbiguousMemberDecl) { nm += ", " + ((AmbiguousMemberDecl)B).ModuleNames(); } else { nm += ", " + B.EnclosingClass.Module.Name; } return nm; } } //Dictionary> allDatatypeCtors; readonly Dictionary> classMembers = new Dictionary>(); readonly Dictionary> datatypeMembers = new Dictionary>(); readonly Dictionary> datatypeCtors = new Dictionary>(); readonly Graph dependencies = new Graph(); private ModuleSignature systemNameInfo = null; private bool useCompileSignatures = false; private RefinementTransformer refinementTransformer = null; public Resolver(Program prog) { Contract.Requires(prog != null); builtIns = prog.BuiltIns; } [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))); } public void ResolveProgram(Program prog) { Contract.Requires(prog != null); var origErrorCount = ErrorCount; var bindings = new ModuleBindings(null); var b = BindModuleNames(prog.DefaultModuleDef, bindings); bindings.BindName("_module", prog.DefaultModule, b); if (ErrorCount > 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); Error(cycle[0], "module definition contains a cycle (note: parent modules implicitly depend on submodules): {0}", cy); } if (ErrorCount > 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(this, AdditionalInformationReporter, prog); rewriters.Add(refinementTransformer); rewriters.Add(new AutoContractsRewriter()); var opaqueRewriter = new OpaqueFunctionRewriter(); rewriters.Add(new AutoReqFunctionRewriter(this, opaqueRewriter)); rewriters.Add(opaqueRewriter); systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false); prog.CompileModules.Add(prog.BuiltIns.SystemModule); 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 = ErrorCount; 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 = ErrorCount; ResolveModuleDefinition(m, sig); foreach (var r in rewriters) { if (ErrorCount != preResolveErrorCount) { break; } r.PostResolve(m); } if (ErrorCount == 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 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 } } else if (decl is AliasModuleDecl) { var alias = (AliasModuleDecl)decl; // resolve the path ModuleSignature p; if (ResolvePath(alias.Root, alias.Path, out p, this)) { 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, this)) { abs.Signature = MakeAbstractSignature(p, abs.FullCompileName, abs.Height, prog.Modules); abs.OriginalSignature = p; ModuleSignature compileSig; if (abs.CompilePath != null) { if (ResolvePath(abs.CompileRoot, abs.CompilePath, out compileSig, this)) { if (refinementTransformer.CheckIsRefinement(compileSig, p)) { abs.Signature.CompileSignature = compileSig; } else { Error(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.IsGhost = compileSig.IsGhost; // always keep the ghost information, to supress a spurious error message when the compile module isn't actually a refinement } } } else { abs.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature } } else { Contract.Assert(false); } Contract.Assert(decl.Signature != null); } if (ErrorCount != 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 CoPredicate) { // this means the corresponding prefix predicate is also recursive var prefixPred = ((CoPredicate)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)) { ReportAdditionalInformation(iter.tok, Printer.IteratorClassToString(iter), iter.Name.Length); } } // 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); } } } } 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 CoLemma) { var prefixLemma = ((CoLemma)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 "; if (m.Decreases.Expressions.Count != 0) { string sep = ""; foreach (var d in m.Decreases.Expressions) { s += sep + Printer.ExprToString(d); sep = ", "; } } s += ";"; // always terminate with a semi-colon, even in the case of an empty decreases clause // 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. ReportAdditionalInformation(clbl.Tok, s, clbl.Tok.val.Length); } } } } } /// /// 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 CoPredicate) { // copredicates don't have decreases clauses return false; } var anyChangeToDecreases = false; var decr = clbl.Decreases.Expressions; 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, ref int tmpCounter) { var arrTy = e.Type as ArrowType; if (arrTy != null) { var bvars = new List(); var bexprs = new List(); foreach (var t in arrTy.Args) { var bv = new BoundVar(e.tok, "_x" + tmpCounter++, t); bvars.Add(bv); bexprs.Add(new IdentifierExpr(e.tok, bv.Name) { Type = bv.Type, Var = bv }); } var oVar = new BoundVar(e.tok, "_o" + tmpCounter++, new ObjectType()); var obj = new IdentifierExpr(e.tok, oVar.Name) { Type = oVar.Type, Var = oVar }; bvars.Add(oVar); return new SetComprehension(e.tok, bvars, new BinaryExpr(e.tok, BinaryExpr.Opcode.In, obj, new ApplyExpr(e.tok, e.tok, e, bexprs) { Type = new SetType(new ObjectType()) }) { ResolvedOp = BinaryExpr.ResolvedOpcode.InSet, Type = Type.Bool }, obj) { Type = new SetType(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; int tmpVarCount = 0; foreach (FrameExpression fe in fexprs) { Contract.Assert(fe != null); if (fe.E is WildcardExpr) { // drop wildcards altogether } else { Expression e = FrameArrowToObjectSet(fe.E, ref tmpVarCount); // 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, "_s2s_" + tmpVarCount, ((SeqType)eType).Arg); tmpVarCount++; 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, new List() { bv }, sInE, bvIE); s.Type = new SetType(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, singletons); display.Type = new SetType(new ObjectType()); // resolve here sets.Add(display); } if (sets.Count == 0) { Expression emptyset = new SetDisplayExpr(Token.NoToken, new List()); emptyset.Type = new SetType(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(new ObjectType()); // resolve here s = union; } return s; } } private void ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) { moduleInfo = MergeSignature(sig, systemNameInfo); // resolve var datatypeDependencies = new Graph(); var codatatypeDependencies = new Graph(); int prevErrorCount = ErrorCount; ResolveAttributes(m.Attributes, false, new NoContext(m.Module)); ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies, codatatypeDependencies); if (ErrorCount == prevErrorCount) { ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies, codatatypeDependencies); } } 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)) { Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name); } } else if (tld is ModuleFacadeDecl) { var subdecl = (ModuleFacadeDecl)tld; if (!bindings.BindName(subdecl.Name, subdecl, null)) { Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name); } } else if (tld is AliasModuleDecl) { var subdecl = (AliasModuleDecl)tld; if (!bindings.BindName(subdecl.Name, subdecl, null)) { Error(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)) { Error(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) { Error(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)) Error(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)) Error(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)) Error(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.IsGhost = m.IsGhost; return info; } ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImports) { Contract.Requires(moduleDef != null); var sig = new ModuleSignature(); sig.ModuleDef = moduleDef; sig.IsGhost = moduleDef.IsAbstract; List declarations = moduleDef.TopLevelDecls; if (useImports) { // 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); // classes: foreach (var kv in s.TopLevels) { TopLevelDecl d; if (sig.TopLevels.TryGetValue(kv.Key, out d)) { sig.TopLevels[kv.Key] = new AmbiguousTopLevelDecl(moduleDef, d, kv.Value); } else { sig.TopLevels.Add(kv.Key, kv.Value); } } // constructors: foreach (var kv in s.Ctors) { Tuple pair; if (sig.Ctors.TryGetValue(kv.Key, out pair)) { // mark it as a duplicate sig.Ctors[kv.Key] = new Tuple(pair.Item1, true); } else { // add new sig.Ctors.Add(kv.Key, kv.Value); } } // static members: foreach (var kv in s.StaticMembers) { MemberDecl md; if (sig.StaticMembers.TryGetValue(kv.Key, out md)) { sig.StaticMembers[kv.Key] = new AmbiguousMemberDecl(moduleDef, md, kv.Value); } else { // add new sig.StaticMembers.Add(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)) { Error(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 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)) { Error(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)) { Error(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)) { Error(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(new ObjectType()), null); iter.Member_Modifies = new SpecialField(iter.tok, "_modifies", "_modifies", "", "", true, false, false, new SetType(new ObjectType()), null); iter.Member_New = new SpecialField(iter.tok, "_new", "_new", "", "", true, true, true, new SetType(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, new List(), iter.tok, 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)) { Error(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)) { Error(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)) { Error(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); bool hasConstructor = false; foreach (MemberDecl m in cl.Members) { if (!members.ContainsKey(m.Name)) { members.Add(m.Name, m); if (m is CoPredicate || m is CoLemma) { 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 CoPredicate) { var cop = (CoPredicate)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.IsStatic, tyvars, cop.OpenParen, 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 = (CoLemma)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. com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.IsStatic, com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal), com.Req.ConvertAll(cloner.CloneMayBeFreeExpr), cloner.CloneSpecFrameExpr(com.Mod), new List(), // Note, the postconditions are filled in after the colemma's postconditions have been resolved 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) { Error(m, "More than one default constructor"); } else { Error(m, "Duplicate member name: {0}", m.Name); } if (m is Constructor) { hasConstructor = true; } } cl.HasConstructor = hasConstructor; if (cl is TraitDecl && cl.HasConstructor) { Error(cl, "a trait is not allowed to declare a constructor"); } if (cl.IsDefaultClass) { foreach (MemberDecl m in cl.Members) { if (m.IsStatic && (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("?")) { Error(ctor, "a datatype constructor name is not allowed to end with '?'"); } else if (ctors.ContainsKey(ctor.Name)) { Error(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)) { Error(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, null, null, null, false); mod.Height = Height; foreach (var kv in p.TopLevels) { mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name)); } var sig = RegisterTopLevelDecls(mod, false); sig.Refines = p.Refines; sig.CompileSignature = p; sig.IsGhost = p.IsGhost; 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 OpaqueTypeDecl) { var dd = (OpaqueTypeDecl)d; return new OpaqueTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), null); } else if (d is TypeSynonymDecl) { var dd = (TypeSynonymDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); return new TypeSynonymDecl(dd.tok, dd.Name, tps, m, CloneType(dd.Rhs), null); } else if (d is TupleTypeDecl) { var dd = (TupleTypeDecl)d; return new TupleTypeDecl(dd.Dims, dd.Module); } else if (d is IndDatatypeDecl) { var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var ctors = dd.Ctors.ConvertAll(CloneCtor); var dt = new IndDatatypeDecl(dd.tok, dd.Name, m, tps, ctors, null); return dt; } else if (d is CoDatatypeDecl) { var dd = (CoDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var ctors = dd.Ctors.ConvertAll(CloneCtor); var dt = new CoDatatypeDecl(dd.tok, dd.Name, m, tps, ctors, null); return dt; } else if (d is ClassDecl) { var dd = (ClassDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var mm = dd.Members.ConvertAll(CloneMember); List trait = null; if (dd is DefaultClassDecl) { return new DefaultClassDecl(m, mm); } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null,trait); } else if (d is ModuleDecl) { if (d is LiteralModuleDecl) { return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m); } else if (d is AliasModuleDecl) { var a = (AliasModuleDecl)d; var alias = new AliasModuleDecl(a.Path, a.tok, m, a.Opened); alias.ModuleReference = a.ModuleReference; alias.Signature = a.Signature; return alias; } else 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 { Contract.Assert(false); // unexpected declaration return null; // to please compiler } } else { Contract.Assert(false); // unexpected declaration return null; // to please compiler } } MemberDecl CloneMember(MemberDecl member) { if (member is Field) { Contract.Assert(!(member is SpecialField)); // we don't expect a SpecialField to be cloned (or do we?) var f = (Field)member; return new Field(f.tok, f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), null); } else if (member is Function) { var f = (Function)member; return CloneFunction(f.tok, f, f.IsGhost); } else { var m = (Method)member; return CloneMethod(m); } } TypeParameter CloneTypeParam(TypeParameter tp) { return new TypeParameter(tp.tok, tp.Name); } DatatypeCtor CloneCtor(DatatypeCtor ct) { return new DatatypeCtor(ct.tok, ct.Name, ct.Formals.ConvertAll(CloneFormal), null); } Formal CloneFormal(Formal formal) { return new Formal(formal.tok, formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost); } Type CloneType(Type t) { if (t is BasicType) { return t; } else if (t is SetType) { var tt = (SetType)t; return new SetType(CloneType(tt.Arg)); } else if (t is SeqType) { var tt = (SeqType)t; return new SeqType(CloneType(tt.Arg)); } else if (t is MultiSetType) { var tt = (MultiSetType)t; return new MultiSetType(CloneType(tt.Arg)); } else if (t is MapType) { var tt = (MapType)t; return new MapType(CloneType(tt.Domain), CloneType(tt.Range)); } else if (t is ArrowType) { var tt = (ArrowType)t; return new ArrowType(tt.Args.ConvertAll(CloneType), CloneType(tt.Result)); } else if (t is UserDefinedType) { var tt = (UserDefinedType)t; return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => x)); } else if (t is InferredTypeProxy) { return new InferredTypeProxy(); } else if (t is ParamTypeProxy) { var tt = (ParamTypeProxy)t; return new ParamTypeProxy(CloneTypeParam(tt.orig)); } else { Contract.Assert(false); // unexpected type (e.g., no other type proxies are expected at this time) return null; // to please compiler } } Function CloneFunction(IToken tok, Function f, bool isGhost) { var tps = f.TypeArgs.ConvertAll(CloneTypeParam); var formals = f.Formals.ConvertAll(CloneFormal); var req = f.Req.ConvertAll(CloneExpr); var reads = f.Reads.ConvertAll(CloneFrameExpr); var decreases = CloneSpecExpr(f.Decreases); var ens = f.Ens.ConvertAll(CloneExpr); Expression body = CloneExpr(f.Body); if (f is Predicate) { return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, null, null); } else if (f is CoPredicate) { return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals, req, reads, ens, body, null, null); } else { return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType), req, reads, ens, decreases, body, null, null); } } Method CloneMethod(Method m) { Contract.Requires(m != null); var tps = m.TypeArgs.ConvertAll(CloneTypeParam); var ins = m.Ins.ConvertAll(CloneFormal); var req = m.Req.ConvertAll(CloneMayBeFreeExpr); var mod = CloneSpecFrameExpr(m.Mod); var decreases = CloneSpecExpr(m.Decreases); var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr); if (m is Constructor) { return new Constructor(m.tok, m.Name, tps, ins, req, mod, ens, decreases, null, null, null); } else if (m is CoLemma) { return new CoLemma(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), req, mod, ens, decreases, null, null, null); } else if (m is Lemma) { return new Lemma(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), req, mod, ens, decreases, null, null, null); } else { return new Method(m.tok, m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal), req, mod, ens, decreases, null, null, null); } } Specification CloneSpecExpr(Specification spec) { var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr); return new Specification(ee, null); } Specification CloneSpecFrameExpr(Specification frame) { var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr); return new Specification(ee, null); } FrameExpression CloneFrameExpr(FrameExpression frame) { return new FrameExpression(frame.tok, CloneExpr(frame.E), frame.FieldName); } MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) { return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree); } BoundVar CloneBoundVar(BoundVar bv) { return new BoundVar(bv.tok, bv.Name, CloneType(bv.Type)); } // ToDo: Remove this and use cloner Expression CloneExpr(Expression expr) { if (expr == null) { return null; } else if (expr is LiteralExpr) { var e = (LiteralExpr)expr; if (e is StaticReceiverExpr) { return new StaticReceiverExpr(e.tok, CloneType(e.Type)); } else if (e.Value == null) { return new LiteralExpr(e.tok); } else if (e.Value is bool) { return new LiteralExpr(e.tok, (bool)e.Value); } else if (e.Value is Basetypes.BigDec) { return new LiteralExpr(e.tok, (Basetypes.BigDec)e.Value); } else { return new LiteralExpr(e.tok, (BigInteger)e.Value); } } else if (expr is ThisExpr) { if (expr is ImplicitThisExpr) { return new ImplicitThisExpr(expr.tok); } else { return new ThisExpr(expr.tok); } } else if (expr is IdentifierExpr) { var e = (IdentifierExpr)expr; return new IdentifierExpr(e.tok, e.Name); } else if (expr is DatatypeValue) { var e = (DatatypeValue)expr; return new DatatypeValue(e.tok, e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr)); } else if (expr is DisplayExpression) { DisplayExpression e = (DisplayExpression)expr; if (expr is SetDisplayExpr) { return new SetDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr)); } else if (expr is MultiSetDisplayExpr) { return new MultiSetDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr)); } else { Contract.Assert(expr is SeqDisplayExpr); return new SeqDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr)); } } else if (expr is MapDisplayExpr) { MapDisplayExpr e = (MapDisplayExpr)expr; List pp = new List(); foreach (ExpressionPair p in e.Elements) { pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B))); } return new MapDisplayExpr(expr.tok, pp); } else if (expr is ExprDotName) { var e = (ExprDotName)expr; return new ExprDotName(e.tok, CloneExpr(e.Obj), e.SuffixName); } else if (expr is MemberSelectExpr) { var e = (MemberSelectExpr)expr; return new MemberSelectExpr(e.tok, CloneExpr(e.Obj), e.MemberName); } else if (expr is SeqSelectExpr) { var e = (SeqSelectExpr)expr; return new SeqSelectExpr(e.tok, e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1)); } else if (expr is MultiSelectExpr) { var e = (MultiSelectExpr)expr; return new MultiSelectExpr(e.tok, CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr)); } else if (expr is SeqUpdateExpr) { var e = (SeqUpdateExpr)expr; return new SeqUpdateExpr(e.tok, CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value)); } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; return new FunctionCallExpr(e.tok, e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : (e.OpenParen), e.Args.ConvertAll(CloneExpr)); } else if (expr is OldExpr) { var e = (OldExpr)expr; return new OldExpr(e.tok, CloneExpr(e.E)); } else if (expr is MultiSetFormingExpr) { var e = (MultiSetFormingExpr)expr; return new MultiSetFormingExpr(e.tok, CloneExpr(e.E)); } else if (expr is UnaryOpExpr) { var e = (UnaryOpExpr)expr; return new UnaryOpExpr(e.tok, e.Op, CloneExpr(e.E)); } else if (expr is ConversionExpr) { var e = (ConversionExpr)expr; return new ConversionExpr(e.tok, CloneExpr(e.E), CloneType(e.ToType)); } else if (expr is BinaryExpr) { var e = (BinaryExpr)expr; return new BinaryExpr(e.tok, e.Op, CloneExpr(e.E0), CloneExpr(e.E1)); } else if (expr is TernaryExpr) { var e = (TernaryExpr)expr; return new TernaryExpr(e.tok, e.Op, CloneExpr(e.E0), CloneExpr(e.E1), CloneExpr(e.E2)); } else if (expr is ChainingExpression) { var e = (ChainingExpression)expr; return CloneExpr(e.E); // just clone the desugaring, since it's already available } else if (expr is LetExpr) { var e = (LetExpr)expr; return new LetExpr(e.tok, e.LHSs.ConvertAll(CloneCasePattern), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body), e.Exact); } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; var tk = e.tok; var bvs = e.BoundVars.ConvertAll(CloneBoundVar); var range = CloneExpr(e.Range); var term = CloneExpr(e.Term); if (e is QuantifierExpr) { var q = (QuantifierExpr)e; var tvs = q.TypeArgs.ConvertAll(CloneTypeParam); if (e is ForallExpr) { return new ForallExpr(tk, tvs, bvs, range, term, null); } else if (e is ExistsExpr) { return new ExistsExpr(tk, tvs, bvs, range, term, null); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected quantifier expression } } else if (e is MapComprehension) { return new MapComprehension(tk, bvs, range, term); } else if (e is LambdaExpr) { var l = (LambdaExpr)e; return new LambdaExpr(tk, l.OneShot, bvs, range, l.Reads.ConvertAll(CloneFrameExpr), term); } else { Contract.Assert(e is SetComprehension); return new SetComprehension(tk, bvs, range, term); } } else if (expr is WildcardExpr) { return new WildcardExpr(expr.tok); } else if (expr is StmtExpr) { var e = (StmtExpr)expr; return new StmtExpr(e.tok, (new Cloner()).CloneStmt(e.S), CloneExpr(e.E)); } else if (expr is ITEExpr) { var e = (ITEExpr)expr; return new ITEExpr(e.tok, CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els)); } else if (expr is AutoGeneratedExpression) { var e = (AutoGeneratedExpression)expr; var a = CloneExpr(e.E); return new AutoGeneratedExpression(e.tok, a); } else if (expr is ParensExpression) { var e = (ParensExpression)expr; return CloneExpr(e.E); // skip the parentheses in the clone } else if (expr is IdentifierSequence) { var e = (IdentifierSequence)expr; var aa = e.Arguments == null ? null : e.Arguments.ConvertAll(CloneExpr); return new IdentifierSequence(e.Tokens.ConvertAll(tk => (tk)), e.OpenParen == null ? null : (e.OpenParen), aa); } else if (expr is MatchExpr) { var e = (MatchExpr)expr; return new MatchExpr(e.tok, CloneExpr(e.Source), e.Cases.ConvertAll(c => new MatchCaseExpr(c.tok, c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))), e.UsesOptionalBraces); } else if (expr is NegationExpression) { var e = (NegationExpression)expr; return new NegationExpression(e.tok, CloneExpr(e.E)); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression } } public CasePattern CloneCasePattern(CasePattern pat) { Contract.Requires(pat != null); if (pat.Var != null) { return new CasePattern(pat.tok, CloneBoundVar(pat.Var)); } else if (pat.Arguments == null) { return new CasePattern(pat.tok, pat.Id, null); } else { return new CasePattern(pat.tok, pat.Id, pat.Arguments.ConvertAll(CloneCasePattern)); } } public static bool ResolvePath(ModuleDecl root, List Path, out ModuleSignature p, ResolutionErrorReporter reporter) { Contract.Requires(reporter != null); 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(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); var typeSynonymDependencies = new Graph(); foreach (TopLevelDecl d in declarations) { 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, ResolveTypeOptionEnum.AllowPrefix, syn.TypeArgs); syn.Rhs.ForeachTypeComponent(ty => { var s = ty.AsTypeSynonym; if (s != null) { typeSynonymDependencies.AddEdge(syn, 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.IsGhost) { if (!(def.IsDefaultModule)) // _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. Error(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 = typeSynonymDependencies.TryFindCycle(); if (cycle != null) { Contract.Assert(cycle.Count != 0); var erste = cycle[0]; Error(erste.tok, "Cycle among type synonyms: {0} -> {1}", Util.Comma(" -> ", cycle, syn => syn.Name), erste.Name); } } public void ResolveTopLevelDecls_Meat(List/*!*/ declarations, Graph/*!*/ datatypeDependencies, Graph/*!*/ codatatypeDependencies) { Contract.Requires(declarations != null); Contract.Requires(cce.NonNullElements(datatypeDependencies)); Contract.Requires(cce.NonNullElements(codatatypeDependencies)); int prevErrorCount = ErrorCount; // Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations foreach (TopLevelDecl d in declarations) { Contract.Assert(d != null); if (d is TraitDecl && d.TypeArgs != null && d.TypeArgs.Count > 0) { Error(d, "a trait cannot declare type parameters"); } 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, false, new NoContext(d.Module)); } 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(); } if (ErrorCount == 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; iter.Members.Iter(CheckTypeInference_Member); if (iter.Body != null) { CheckTypeInference(iter.Body); } } else if (d is ClassDecl) { var cl = (ClassDecl)d; cl.Members.Iter(CheckTypeInference_Member); } } } if (ErrorCount == prevErrorCount) { // fill in the postconditions and bodies of prefix lemmas foreach (var com in ModuleDefinition.AllCoLemmas(declarations)) { var prefixLemma = com.PrefixLemma; if (prefixLemma == null) { continue; // something went wrong during registration of the prefix lemma (probably a duplicated colemma name) } Contract.Assume(prefixLemma.Ens.Count == 0 && prefixLemma.Body == null); // these are not supposed to have been filled in before // compute the postconditions of the prefix lemma var k = prefixLemma.Ins[0]; foreach (var p in com.Ens) { var coConclusions = new HashSet(); CheckCoLemmaConclusions(p.E, true, coConclusions); var subst = new CoLemmaPostconditionSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this); var post = subst.CloneExpr(p.E); prefixLemma.Ens.Add(new MaybeFreeExpression(post, p.IsFree)); } // Compute the statement body of the prefix lemma 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 CoLemmaBodyCloner(com, kMinusOne, this); 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, 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 (ErrorCount == 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; ReportAdditionalInformation(c.CandidateCall.tok, "co-recursive call", c.CandidateCall.Name.Length); } // 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 copredicates are not recursive with non-copredicate functions, and // check that colemmas are not recursive with non-colemma methods. foreach (var d in declarations) { if (d is ClassDecl) { foreach (var member in ((ClassDecl)d).Members) { if (member is CoPredicate) { var fn = (CoPredicate)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) { Error(fn.Ens[0].tok, "a copredicate is not allowed to declare any ensures clause"); } // Also check for 'reads' clauses if (fn.Reads.Count != 0) { Error(fn.Reads[0].tok, "a copredicate is not allowed to declare any reads clause"); // (why?) } if (fn.Body != null) { CoPredicateChecks(fn.Body, fn, CallingPosition.Positive); } } else if (member is CoLemma) { var m = (CoLemma)member; if (m.Body != null) { CoLemmaChecks(m.Body, m); } } } } } } } // ------------------------------------------------------------------------------------------------------ // ----- Visitors --------------------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region Visitors class ResolverBottomUpVisitor : BottomUpVisitor { protected Resolver resolver; public ResolverBottomUpVisitor(Resolver resolver) { Contract.Requires(resolver != null); this.resolver = resolver; } public void Error(IToken tok, string msg, params object[] args) { Contract.Requires(tok != null); Contract.Requires(msg != null); Contract.Requires(args != null); resolver.Error(tok, msg, args); } public void Error(Expression expr, string msg, params object[] args) { Contract.Requires(expr != null); Contract.Requires(msg != null); Contract.Requires(args != null); Error(expr.tok, msg, args); } } abstract class ResolverTopDownVisitor : TopDownVisitor { Resolver resolver; public ResolverTopDownVisitor(Resolver resolver) { Contract.Requires(resolver != null); this.resolver = resolver; } protected void Error(IToken tok, string msg, params object[] args) { Contract.Requires(tok != null); Contract.Requires(msg != null); Contract.Requires(args != null); resolver.Error(tok, msg, args); } protected void Error(Expression expr, string msg, params object[] args) { Contract.Requires(expr != null); Contract.Requires(msg != null); Contract.Requires(args != null); Error(expr.tok, msg, args); } protected void ReportAdditionalInformation(IToken tok, string text, int length) { Contract.Requires(tok != null); resolver.ReportAdditionalInformation(tok, text, length); } } #endregion Visitors // ------------------------------------------------------------------------------------------------------ // ----- CheckTypeInference ----------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region CheckTypeInference private void CheckTypeInference_Member(MemberDecl member) { if (member is Method) { var m = (Method)member; m.Req.Iter(CheckTypeInference_MaybeFreeExpression); m.Ens.Iter(CheckTypeInference_MaybeFreeExpression); CheckTypeInference_Specification_FrameExpr(m.Mod); CheckTypeInference_Specification_Expr(m.Decreases); if (m.Body != null) { CheckTypeInference(m.Body); 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) { Error(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) { Error(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 ReportAdditionalInformation(m.tok, "tail recursive", m.Name.Length); } } } } } if (!m.IsTailRecursive && m.Body != null && Contract.Exists(m.Decreases.Expressions, e => e is WildcardExpr)) { Error(m.Decreases.Expressions[0].tok, "'decreases *' is allowed only on tail-recursive methods"); } } else if (member is Function) { var f = (Function)member; var errorCount = ErrorCount; f.Req.Iter(CheckTypeInference); f.Ens.Iter(CheckTypeInference); f.Reads.Iter(fe => CheckTypeInference(fe.E)); CheckTypeInference_Specification_Expr(f.Decreases); if (f.Body != null) { CheckTypeInference(f.Body); bool tail = true; if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) { Error(f.tok, "sorry, tail-call functions are not supported"); } } if (errorCount == ErrorCount && f is CoPredicate) { var cop = (CoPredicate)f; CheckTypeInference_Member(cop.PrefixPredicate); } } } private void CheckTypeInference_MaybeFreeExpression(MaybeFreeExpression mfe) { Contract.Requires(mfe != null); foreach (var e in Attributes.SubExpressions(mfe.Attributes)) { CheckTypeInference(e); } CheckTypeInference(mfe.E); } private void CheckTypeInference_Specification_Expr(Specification spec) { Contract.Requires(spec != null); foreach (var e in Attributes.SubExpressions(spec.Attributes)) { CheckTypeInference(e); } spec.Expressions.Iter(CheckTypeInference); } private void CheckTypeInference_Specification_FrameExpr(Specification spec) { Contract.Requires(spec != null); foreach (var e in Attributes.SubExpressions(spec.Attributes)) { CheckTypeInference(e); } spec.Expressions.Iter(fe => CheckTypeInference(fe.E)); } void CheckTypeInference(Expression expr) { Contract.Requires(expr != null); var c = new CheckTypeInference_Visitor(this); c.Visit(expr); } void CheckTypeInference(Statement stmt) { Contract.Requires(stmt != null); var c = new CheckTypeInference_Visitor(this); c.Visit(stmt); } class CheckTypeInference_Visitor : ResolverBottomUpVisitor { public CheckTypeInference_Visitor(Resolver resolver) : base(resolver) { Contract.Requires(resolver != null); } 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 ForallStmt) { var s = (ForallStmt)stmt; s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); } else if (stmt is CallStmt) { var s = (CallStmt)stmt; foreach (var p in s.TypeArgumentSubstitutions) { if (p.Value.Normalize() is TypeProxy) { Error(stmt.Tok, "type variable '{0}' in the method call to '{1}' could not determined", p.Key.Name, s.MethodName); } } } } protected override void VisitOneExpr(Expression expr) { if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; if (e != null) { foreach (var bv in e.BoundVars) { if (bv.Type.Normalize() is TypeProxy) { Error(bv.tok, "type of bound variable '{0}' could not determined; please specify the type explicitly", bv.Name); } } } } else if (expr is MemberSelectExpr) { var e = (MemberSelectExpr)expr; if (e.Member is Function) { foreach (var p in e.TypeApplication) { if (p.Normalize() is TypeProxy) { Error(e.tok, "type '{0}' to the function '{1}' is not determined", p, e.Member.Name); } } } } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; foreach (var p in e.TypeArgumentSubstitutions) { if (p.Value.Normalize() is TypeProxy) { Error(e.tok, "type variable '{0}' in the function call to '{1}' could not determined{2}", p.Key.Name, e.Name, (e.Name.Contains("reveal_") || e.Name.Contains("_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 (x.Type.Normalize() is TypeProxy) { Error(e.tok, "the type of the bound variable '{0}' could not be determined", x.Name); } } } } else if (expr is MapDisplayExpr) { CheckTypeIsDetermined(expr.tok, expr.Type, "map constructor", true); } else if (expr is DisplayExpression) { CheckTypeIsDetermined(expr.tok, expr.Type, "collection constructor", true); } else if (CheckTypeIsDetermined(expr.tok, expr.Type, "expression")) { var bin = expr as BinaryExpr; if (bin != null) { bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type); } } } bool CheckTypeIsDetermined(IToken tok, Type t, string what, bool aggressive = false) { Contract.Requires(tok != null); Contract.Requires(t != null); Contract.Requires(what != null); t = t.NormalizeExpand(); if (t is TypeProxy && (aggressive || !(t is InferredTypeProxy || t is ParamTypeProxy || t is ObjectTypeProxy))) { Error(tok, "the type of this {0} is underspecified, but it cannot be an opaque type.", what); return false; } else if (aggressive && t is MapType) { return CheckTypeIsDetermined(tok, ((MapType)t).Range, what, aggressive) && CheckTypeIsDetermined(tok, ((MapType)t).Domain, what, aggressive); } else if (aggressive && t is CollectionType) { return CheckTypeIsDetermined(tok, ((CollectionType)t).Arg, what, aggressive); } else if (aggressive && t is UserDefinedType) { return t.TypeArgs.All(rg => CheckTypeIsDetermined(tok, rg, what, aggressive)); } else { return true; } } } #endregion CheckTypeInference // ------------------------------------------------------------------------------------------------------ // ----- 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) { Error(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; } /// /// 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) { Error(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 = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors); if (status != TailRecursionStatus.CanBeFollowedByAnything) { if (status == TailRecursionStatus.NotTailRecursive) { // an error has already been reported } else if (reportErrors) { Error(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) { Error(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) { Error(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 { Contract.Assert(false); // unexpected statement type } return TailRecursionStatus.CanBeFollowedByAnything; } #endregion CheckTailRecursive // ------------------------------------------------------------------------------------------------------ // ----- CoPredicateChecks ------------------------------------------------------------------------------ // ------------------------------------------------------------------------------------------------------ #region CoPredicateChecks 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 CoPredicateChecks_Visitor : ResolverTopDownVisitor { public readonly CoPredicate context; public CoPredicateChecks_Visitor(Resolver resolver, CoPredicate context) : base(resolver) { 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)) { // we're looking at a recursive call if (!(e.Function is CoPredicate)) { Error(e, "a recursive call from a copredicate can go only to other copredicates"); } else if (cp != CallingPosition.Positive) { var msg = "a copredicate can be called recursively only in positive positions"; if (cp == CallingPosition.Neither) { // this may be inside an existential quantifier msg += " and cannot sit inside an unbounded existential quantifier"; } else { // the co-call is not inside an existential quantifier, so don't bother mentioning the part of existentials in the error message } Error(e, msg); } else { e.CoCall = FunctionCallExpr.CoCallResolution.Yes; ReportAdditionalInformation(e.tok, e.Function.Name + "#[_k - 1]", e.Function.Name.Length); } } // fall through to do the subexpressions (with cp := Neither) } else 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); } // note, a let-such-that expression introduces an existential that may depend on the _k in a copredicate, so we disallow recursive copredicate calls in the body of the let-such-that Visit(e.Body, e.Exact ? cp : CallingPosition.Neither); return false; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; if ((cp == CallingPosition.Positive && e is ExistsExpr) || (cp == CallingPosition.Negative && e is ForallExpr)) { if (e.MissingBounds != null && e.MissingBounds.Count != 0) { // Don't allow any co-recursive calls under an existential with an unbounded range, because that can be unsound. 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; } 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 Error(stmt.Tok, "a recursive call from a copredicate can go only to other copredicates"); } // do the sub-parts with the same "cp" return true; } else { return base.VisitOneStmt(stmt, ref st); } } } void CoPredicateChecks(Expression expr, CoPredicate context, CallingPosition cp) { Contract.Requires(expr != null); Contract.Requires(context != null); var v = new CoPredicateChecks_Visitor(this, context); v.Visit(expr, cp); } #endregion CoPredicateChecks // ------------------------------------------------------------------------------------------------------ // ----- CoLemmaChecks ---------------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region CoLemmaChecks class CoLemmaChecks_Visitor : ResolverBottomUpVisitor { CoLemma context; public CoLemmaChecks_Visitor(Resolver resolver, CoLemma 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 CoLemma || s.Method is PrefixLemma) { // all is cool } else { // the call goes from a colemma context to a non-colemma callee if (ModuleDefinition.InSameSCC(context, s.Method)) { // we're looking at a recursive call (to a non-colemma) Error(s.Tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas"); } } } } 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) Error(e.tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas"); } } } } void CoLemmaChecks(Statement stmt, CoLemma context) { Contract.Requires(stmt != null); Contract.Requires(context != null); var v = new CoLemmaChecks_Visitor(this, context); v.Visit(stmt); } #endregion CoLemmaChecks // ------------------------------------------------------------------------------------------------------ // ----- 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 WhileStmt) { var s = (WhileStmt)stmt; // don't recurse on the specification parts, which are ghost if (s.Guard != null) { Visit(s.Guard, st); } 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.TypeArgumentSubstitutions.Count); var i = 0; foreach (var formalTypeArg in s.Method.TypeArgs) { var actualTypeArg = s.TypeArgumentSubstitutions[formalTypeArg]; if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) { Error(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); } } 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) { Error(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) { Error(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) { Error(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) { Error(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 { Error(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 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) { Error(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) { // 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 argType = ((SetType)type).Arg; if (!argType.SupportsEquality) { Error(tok, "set argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType)); } CheckEqualityTypes_Type(tok, argType); } else if (type is MultiSetType) { var argType = ((MultiSetType)type).Arg; if (!argType.SupportsEquality) { Error(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) { Error(tok, "map domain type must support equality (got {0}){1}", mt.Domain, TypeEqualityErrorMessageHint(mt.Domain)); } 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) { Error(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 // ------------------------------------------------------------------------------------------------------ // ----- 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()); foreach (var ens in cs.Method.Ens) { var p = substituter.Substitute(ens.E); // substitute the call's actuals for the method's formals resolver.ReportAdditionalInformation(s.Tok, "ensures " + Printer.ExprToString(p) + ";", s.Tok.val.Length); } } } } } #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) readonly Dictionary inSpecOnlyContext = new Dictionary(); // invariant: domain contain union of the domains of "labeledStatements" and "loopStack" /// /// 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; // Resolve names of traits extended if (cl.TraitId != null) { var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val); if (trait == null) { Error(cl.TraitId, "unresolved identifier: {0}", cl.TraitId.val); } else if (!(trait is TraitDecl)) { Error(cl.TraitId, "identifier '{0}' does not denote a trait", cl.TraitId.val); } else { //disallowing inheritance in multi module case string clModName = cl.Module.CompileName.Replace("_Compile", string.Empty); string traitModName = trait.Module.CompileName.Replace("_Compile", string.Empty); if (clModName != traitModName) { Error(cl.TraitId, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module", cl.FullName, trait.FullName)); } else { cl.Trait = (TraitDecl)trait; } } } foreach (MemberDecl member in cl.Members) { member.EnclosingClass = cl; if (member is Field) { ResolveType(member.tok, ((Field)member).Type, ResolveTypeOptionEnum.DontInfer, null); } else if (member is Function) { var f = (Function)member; var ec = ErrorCount; allTypeParameters.PushMarker(); ResolveTypeParameters(f.TypeArgs, true, f); ResolveFunctionSignature(f); allTypeParameters.PopMarker(); if (f is CoPredicate && ec == ErrorCount) { var ff = ((CoPredicate)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 = ErrorCount; allTypeParameters.PushMarker(); ResolveTypeParameters(m.TypeArgs, true, m); ResolveMethodSignature(m); allTypeParameters.PopMarker(); var com = m as CoLemma; if (com != null && com.PrefixLemma != null && ec == ErrorCount) { 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); //merging class members with parent members if any if (cl.Trait != null) { var clMembers = classMembers[cl]; var traitMembers = classMembers[cl.Trait]; //merging current class members with the inheriting trait foreach (KeyValuePair traitMem in traitMembers) { MemberDecl clMember; if (clMembers.TryGetValue(traitMem.Key, out clMember)) { //check if the signature of the members are equal and the member is body-less if (traitMem.Value is Method) { Method traitMethod = (Method)traitMem.Value; // TODO: should check that the class member is also a method, and the same kind of method Method classMethod = (Method)clMember; //refinementTransformer.CheckMethodsAreRefinements(classMethod, traitMethod); if (traitMethod.Body != null && !clMembers[classMethod.CompileName].Inherited) //if the existing method in the class is not that inherited one from the parent Error(classMethod, "a class cannot override implemented methods"); else { classMethod.OverriddenMethod = traitMethod; //adding a call graph edge from the trait method to that of class cl.Module.CallGraph.AddEdge(traitMethod, classMethod); //checking specifications //class method must provide its own specifications in case the overriden method has provided any if ((classMethod.Req == null || classMethod.Req.Count == 0) && (classMethod.OverriddenMethod.Req != null && classMethod.OverriddenMethod.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req { Error(classMethod, "Method must provide its own Requires clauses anew"); } if ((classMethod.Ens == null || classMethod.Ens.Count == 0) && (classMethod.OverriddenMethod.Ens != null && classMethod.OverriddenMethod.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens { Error(classMethod, "Method must provide its own Ensures clauses anew"); } if ((classMethod.Mod == null || classMethod.Mod.Expressions == null || classMethod.Mod.Expressions.Count == 0) && (classMethod.OverriddenMethod.Mod != null && classMethod.OverriddenMethod.Mod.Expressions != null && classMethod.OverriddenMethod.Mod.Expressions.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod { Error(classMethod, "Method must provide its own Modifies clauses anew"); } if ((classMethod.Decreases == null || classMethod.Decreases.Expressions == null || classMethod.Decreases.Expressions.Count == 0) && (classMethod.OverriddenMethod.Decreases != null && classMethod.OverriddenMethod.Decreases.Expressions != null && classMethod.OverriddenMethod.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases { Error(classMethod, "Method must provide its own Decreases clauses anew"); } } } else if (traitMem.Value is Function) { Function traitFunction = (Function)traitMem.Value; Function classFunction = (Function)clMember; //refinementTransformer.CheckFunctionsAreRefinements(classFunction, traitFunction); if (traitFunction.Body != null && !classMembers[cl][classFunction.CompileName].Inherited) Error(classFunction, "a class cannot override implemented functions"); else { classFunction.OverriddenFunction = traitFunction; //adding a call graph edge from the trait method to that of class cl.Module.CallGraph.AddEdge(traitFunction, classFunction); //checking specifications //class function must provide its own specifications in case the overriden function has provided any if ((classFunction.Req == null || classFunction.Req.Count == 0) && (classFunction.OverriddenFunction.Req != null && classFunction.OverriddenFunction.Req.Count > 0)) //it means m.OverriddenMethod.Req => m.Req { Error(classFunction, "Function must provide its own Requires clauses anew"); } if ((classFunction.Ens == null || classFunction.Ens.Count == 0) && (classFunction.OverriddenFunction.Ens != null && classFunction.OverriddenFunction.Ens.Count > 0)) //it means m.OverriddenMethod.Ens => m.Ens { Error(classFunction, "Function must provide its own Ensures clauses anew"); } if ((classFunction.Reads == null || classFunction.Reads.Count == 0) && (classFunction.OverriddenFunction.Reads != null && classFunction.OverriddenFunction.Reads.Count > 0)) //it means m.OverriddenMethod.Mod => m.Mod { Error(classFunction, "Function must provide its own Reads clauses anew"); } if ((classFunction.Decreases == null || classFunction.Decreases.Expressions == null || classFunction.Decreases.Expressions.Count == 0) && (classFunction.OverriddenFunction.Decreases != null && classFunction.OverriddenFunction.Decreases.Expressions != null && classFunction.OverriddenFunction.Decreases.Expressions.Count > 0)) //it means m.OverriddenMethod.Decreases => m.Decreases { Error(classFunction, "Function must provide its own Decreases clauses anew"); } } } else if (traitMem.Value is Field) { Field traitField = (Field)traitMem.Value; Field classField = (Field)clMember; if (!clMembers[classField.CompileName].Inherited) Error(classField, "member in the class has been already inherited from its parent trait"); } } else { //the member is not already in the class // enter the trait member in the symbol table for the class clMembers.Add(traitMem.Key, traitMem.Value); } }//foreach //checking to make sure all body-less methods/functions have been implemented in the child class if (refinementTransformer == null) refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, null); foreach (MemberDecl traitMember in cl.Trait.Members.Where(mem => mem is Function || mem is Method)) { if (traitMember is Function) { Function traitFunc = (Function)traitMember; if (traitFunc.Body == null) //we do this check only if trait function body is null { var classMem = cl.Members.Where(clMem => clMem is Function).FirstOrDefault(clMem => ((Function)clMem).Body != null && clMem.CompileName == traitMember.CompileName); if (classMem != null) { Function classFunc = (Function)classMem; refinementTransformer.CheckOverride_FunctionParameters(classFunc, traitFunc); } else if (!cl.Module.IsAbstract && traitFunc.Body == null && classMem == null) Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitFunc.CompileName); } } if (traitMember is Method) { Method traitMethod = (Method)traitMember; if (traitMethod.Body == null) //we do this check only if trait method body is null { var classMem = cl.Members.Where(clMem => clMem is Method).FirstOrDefault(clMem => ((Method)clMem).Body != null && clMem.CompileName == traitMember.CompileName); if (classMem != null) { Method classMethod = (Method)classMem; refinementTransformer.CheckOverride_MethodParameters(classMethod, traitMethod); } if (!cl.Module.IsAbstract && traitMethod.Body == null && classMem == null) Error(cl, "class: {0} does not implement trait member: {1}", cl.CompileName, traitMethod.CompileName); } } } } } /// /// 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, false, new NoContext(currentClass.Module)); // nothing more to do } else if (member is Function) { var f = (Function)member; var ec = ErrorCount; allTypeParameters.PushMarker(); ResolveTypeParameters(f.TypeArgs, false, f); ResolveFunction(f); allTypeParameters.PopMarker(); if (f is CoPredicate && ec == ErrorCount) { var ff = ((CoPredicate)f).PrefixPredicate; allTypeParameters.PushMarker(); ResolveTypeParameters(ff.TypeArgs, false, ff); ResolveFunction(ff); allTypeParameters.PopMarker(); } } else if (member is Method) { var m = (Method)member; var ec = ErrorCount; 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) { Error(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. foreach (DatatypeCtor ctor in dt.Ctors) { var 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, so the datatype is allowed dt.DefaultCtor = ctor; dt.TypeParametersUsedInConstructionByDefaultCtor = new bool[dt.TypeArgs.Count]; for (int i = 0; i < dt.TypeArgs.Count; i++) { dt.TypeParametersUsedInConstructionByDefaultCtor[i] = typeParametersUsed.Contains(dt.TypeArgs[i]); } return true; NEXT_OUTER_ITERATION: { } } // 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 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, bool twoState, ICodeContext codeContext) { // order does not matter much for resolution, so resolve them in reverse order for (; attrs != null; attrs = attrs.Prev) { if (attrs.Args != null) { ResolveAttributeArgs(attrs.Args, twoState, codeContext, true); } } } void ResolveAttributeArgs(List/*!*/ args, bool twoState, ICodeContext codeContext, bool allowGhosts) { Contract.Requires(args != null); foreach (Attributes.Argument aa in args) { Contract.Assert(aa != null); if (aa.E != null) { ResolveExpression(aa.E, twoState, codeContext); if (!allowGhosts) { CheckIsNonGhost(aa.E); } } } } 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; } if (!allTypeParameters.Push(tp.Name, tp) && emitErrors) { Error(tp, "Duplicate type-parameter name: {0}", tp.Name); } } } /// /// Assumes type parameters have already been pushed /// void ResolveFunctionSignature(Function f) { Contract.Requires(f != null); scope.PushMarker(); if (f.SignatureIsOmitted) { Error(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) { if (!scope.Push(p.Name, p)) { Error(p, "Duplicate parameter name: {0}", p.Name); } ResolveType(p.tok, p.Type, option, f.TypeArgs); } ResolveType(f.tok, f.ResultType, 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, false, f); foreach (Expression r in f.Req) { ResolveExpression(r, false, f); Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(r.Type, Type.Bool)) { Error(r, "Precondition must be a boolean (got {0})", r.Type); } } foreach (FrameExpression fr in f.Reads) { ResolveFrameExpression(fr, "reads", f.IsGhost, f); } foreach (Expression r in f.Ens) { ResolveExpression(r, false, f); // since this is a function, the postcondition is still a one-state predicate Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(r.Type, Type.Bool)) { Error(r, "Postcondition must be a boolean (got {0})", r.Type); } } ResolveAttributes(f.Decreases.Attributes, false, f); foreach (Expression r in f.Decreases.Expressions) { ResolveExpression(r, false, f); // any type is fine } if (f.Body != null) { var prevErrorCount = ErrorCount; ResolveExpression(f.Body, false, f); if (!f.IsGhost && prevErrorCount == ErrorCount) { CheckIsNonGhost(f.Body); } Contract.Assert(f.Body.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(f.Body.Type, f.ResultType)) { Error(f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type); } } scope.PopMarker(); } void ResolveFrameExpression(FrameExpression fe, string kind, bool isGhostContext, ICodeContext codeContext) { Contract.Requires(fe != null); Contract.Requires(kind != null); Contract.Requires(codeContext != null); ResolveExpression(fe.E, false, codeContext); Type t = fe.E.Type; Contract.Assert(t != null); // follows from postcondition of ResolveExpression var collType = t.AsCollectionType; if (collType != null) { t = collType.Arg; } if (!UnifyTypes(t, new ObjectType())) { Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, 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)) { Error(fe.E, "member {0} in type {1} does not refer to a field", fe.FieldName, ctype.Name); } else if (isGhostContext && !member.IsGhost) { Error(fe.E, "in a ghost context, only ghost fields can be mentioned as frame targets ({0})", fe.FieldName); } else { Contract.Assert(ctype != null && ctype.ResolvedClass != null); // follows from postcondition of ResolveMember fe.Field = (Field)member; } } } /// /// Assumes type parameters have already been pushed /// void ResolveMethodSignature(Method m) { Contract.Requires(m != null); scope.PushMarker(); if (m.SignatureIsOmitted) { Error(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) { if (!scope.Push(p.Name, p)) { Error(p, "Duplicate parameter name: {0}", p.Name); } ResolveType(p.tok, p.Type, option, m.TypeArgs); } // resolve out-parameters foreach (Formal p in m.Outs) { if (!scope.Push(p.Name, p)) { Error(p, "Duplicate parameter name: {0}", p.Name); } ResolveType(p.tok, p.Type, 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, false, m); ResolveExpression(e.E, false, m); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E.Type, Type.Bool)) { Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type); } } ResolveAttributes(m.Mod.Attributes, false, m); foreach (FrameExpression fe in m.Mod.Expressions) { ResolveFrameExpression(fe, "modifies", m.IsGhost, m); if (m is Lemma) { Error(fe.tok, "lemmas are not allowed to have modifies clauses"); } else if (m is CoLemma) { Error(fe.tok, "colemmas are not allowed to have modifies clauses"); } } ResolveAttributes(m.Decreases.Attributes, false, m); foreach (Expression e in m.Decreases.Expressions) { ResolveExpression(e, false, m); // any type is fine if (m.IsGhost && e is WildcardExpr) { Error(e, "'decreases *' is not allowed on ghost methods"); } } // 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 CoLemma && m.Outs.Count != 0) { Error(m.Outs[0].tok, "colemmas are not allowed to have out-parameters"); } else { foreach (Formal p in m.Outs) { scope.Push(p.Name, p); } } // ... continue resolving specification foreach (MaybeFreeExpression e in m.Ens) { ResolveAttributes(e.Attributes, true, m); ResolveExpression(e.E, true, m); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E.Type, Type.Bool)) { Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type); } } // Resolve body if (m.Body != null) { var com = m as CoLemma; 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 } var codeContext = m; ResolveBlockStatement(m.Body, m.IsGhost, codeContext); } // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas) ResolveAttributes(m.Attributes, false, m); 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(dtTypeArguments != null); ResolveTypeOption option = dtTypeArguments.Count == 0 ? new ResolveTypeOption(ctor) : new ResolveTypeOption(ResolveTypeOptionEnum.AllowPrefix); foreach (Formal p in ctor.Formals) { ResolveType(p.tok, p.Type, option, dtTypeArguments); } } /// /// Assumes type parameters have already been pushed /// void ResolveIteratorSignature(IteratorDecl iter) { Contract.Requires(iter != null); scope.PushMarker(); if (iter.SignatureIsOmitted) { Error(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, 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, 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 = ErrorCount; // 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, false, iter); // any type is fine, but associate this type with the corresponding _decreases field var d = iter.DecreasesFields[i]; if (!UnifyTypes(d.Type, e.Type)) { // bummer, there was a use--and a bad use--of the field before, so this won't be the best of error messages Error(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, "reads", false, iter); } foreach (FrameExpression fe in iter.Modifies.Expressions) { ResolveFrameExpression(fe, "modifies", false, iter); } foreach (MaybeFreeExpression e in iter.Requires) { ResolveExpression(e.E, false, iter); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E.Type, Type.Bool)) { Error(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, false, iter); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E.Type, Type.Bool)) { Error(e.E, "Yield precondition must be a boolean (got {0})", e.E.Type); } } foreach (MaybeFreeExpression e in iter.YieldEnsures) { ResolveExpression(e.E, true, iter); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E.Type, Type.Bool)) { Error(e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type); } } foreach (MaybeFreeExpression e in iter.Ensures) { ResolveExpression(e.E, true, iter); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E.Type, Type.Bool)) { Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type); } } ResolveAttributes(iter.Attributes, false, iter); var postSpecErrorCount = ErrorCount; // Resolve body if (iter.Body != null) { ResolveBlockStatement(iter.Body, false, 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, modSetSingletons); foreach (var fr in iter.Reads.Expressions) { if (fr.FieldName != null) { Error(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, modSetSingletons); foreach (var fr in iter.Modifies.Expressions) { if (fr.FieldName != null) { Error(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, 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, ResolveTypeOptionEnum eopt, List defaultTypeArguments) { Contract.Requires(eopt != ResolveTypeOptionEnum.AllowPrefixExtend); ResolveType(tok, type, new ResolveTypeOption(eopt), defaultTypeArguments); } public void ResolveType(IToken tok, Type type, ResolveTypeOption option, List defaultTypeArguments) { Contract.Requires(option != null); Contract.Requires((option.Opt == ResolveTypeOptionEnum.DontInfer || option.Opt == ResolveTypeOptionEnum.InferTypeProxies) == (defaultTypeArguments == null)); var r = ResolveTypeLenient(tok, type, option, defaultTypeArguments, false); Contract.Assert(r == null); } public class ResolveTypeReturn { public readonly Type ReplacementType; public readonly string LastName; public readonly IToken LastToken; public ResolveTypeReturn(Type replacementType, string lastName, IToken lastToken) { Contract.Requires(replacementType != null); Contract.Requires(lastName != null); Contract.Requires(lastToken != null); ReplacementType = replacementType; LastName = lastName; LastToken = lastToken; } } /// /// See ResolveTypeOption for a description of the option/defaultTypeArguments parameters. /// One more thing: if "allowShortenedPath" 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, ResolveTypeOption option, List defaultTypeArguments, bool allowShortenedPath) { Contract.Requires(tok != null); Contract.Requires(type != 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; int typeArgumentCount = 0; if (mt.HasTypeArg()) { ResolveType(tok, mt.Domain, option, defaultTypeArguments); ResolveType(tok, mt.Range, 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) { Error(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 (mt.Domain.IsSubrangeType || mt.Range.IsSubrangeType) { Error(tok, "sorry, cannot instantiate collection type with a subrange type"); } } else if (type is CollectionType) { var t = (CollectionType)type; if (t.HasTypeArg()) { ResolveType(tok, t.Arg, 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 Error(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 (t.Arg.IsSubrangeType) { Error(tok, "sorry, cannot instantiate collection type with a subrange type"); } } else if (type is UserDefinedType) { var t = (UserDefinedType)type; var isArrow = t is ArrowType; if (!isArrow && (t.ResolvedClass != null || t.ResolvedParam != null)) { // Apparently, this type has already been resolved return null; } foreach (Type tt in t.TypeArgs) { ResolveType(t.tok, tt, option, defaultTypeArguments); if (tt.IsSubrangeType && !isArrow) { Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type"); } } if (isArrow) { return null; // Done already, all arrow types are resolved at construction time } TypeParameter tp = t.Path.Count == 0 ? allTypeParameters.Find(t.Name) : null; if (tp != null) { if (t.TypeArgs.Count == 0) { t.ResolvedParam = tp; } else { Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name); } } else { TopLevelDecl d = null; int j; var sig = moduleInfo; for (j = 0; j < t.Path.Count; j++) { ModuleSignature submodule; if (sig.FindSubmodule(t.Path[j].val, out submodule)) { sig = GetSignature(submodule); } else { // maybe the last component of t.Path is actually the type name if (allowShortenedPath && t.TypeArgs.Count == 0 && j == t.Path.Count - 1 && sig.TopLevels.TryGetValue(t.Path[j].val, out d)) { // move the last component of t.Path to t.tok/t.name, tell the caller about this, and continue var reducedPath = new List(); for (int i = 0; i < j; i++) { reducedPath.Add(t.Path[i]); } return new ResolveTypeReturn(new UserDefinedType(t.Path[j], t.Path[j].val, t.TypeArgs, reducedPath), t.Name, t.tok); } else { Error(t.Path[j], ModuleNotFoundErrorMessage(j, t.Path)); } break; } } if (j == t.Path.Count) { if (!sig.TopLevels.TryGetValue(t.Name, out d)) { if (j == 0) { if (option.Opt == ResolveTypeOptionEnum.AllowPrefixExtend && t.TypeArgs.Count == 0) { tp = new TypeParameter(tok, t.Name, defaultTypeArguments.Count, option.Parent); defaultTypeArguments.Add(tp); t.ResolvedParam = tp; allTypeParameters.Push(t.Name, tp); } else { Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)", t.Name); } } else { Error(t.tok, "Undeclared type {0} in module {1}", t.Name, t.Path[t.Path.Count - 1].val); } } } else { // error has already been reported } if (d == null) { // error has been reported above } else if (d is AmbiguousTopLevelDecl) { Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames()); } else { string what; if (d is OpaqueTypeDecl) { what = "opaque type"; t.ResolvedParam = ((OpaqueTypeDecl)d).TheType; // resolve like a type parameter, and it may have type parameters if it's an opaque type } else { // d is a class or datatype, and it may have type parameters what = "class/datatype"; 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) { Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to {2}: {3}", t.TypeArgs.Count, d.TypeArgs.Count, what, t.Name); } } } } else if (type is TypeProxy) { TypeProxy t = (TypeProxy)type; if (t.T != null) { ResolveType(tok, t.T, 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++) { var typeArg = new UserDefinedType(tok, defaultTypeArguments[i].Name, new List(), null); typeArg.ResolvedParam = defaultTypeArguments[i]; // resolve "typeArg" here typeArgs.Add(typeArg); } } } 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 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 && 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 && 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) { if (!(b is UserDefinedType)) { return false; } var aa = (UserDefinedType)a; var bb = (UserDefinedType)b; if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) { // 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 ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl)) { return ((ClassDecl)bb.ResolvedClass).Trait.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName; } else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl)) { return ((ClassDecl)aa.ResolvedClass).Trait.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName; } 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 { 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 { 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) { OperationTypeProxy opProxy = (OperationTypeProxy)proxy; if (t is IntType || t is RealType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) { // this is the expected case } else { return false; } } else if (proxy is IndexableTypeProxy) { var iProxy = (IndexableTypeProxy)proxy; if (t is SeqType) { if (!UnifyTypes(iProxy.Domain, Type.Int)) { 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, Type.Int)) { return false; } else if (!UnifyTypes(iProxy.Range, elType)) { return false; } else if (!UnifyTypes(iProxy.Arg, iProxy.Range)) { return false; } } else if (t is MapType) { 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, Type.Int)) { 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 { proxy.T = t; } return true; } 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 a.T = ResolvedArrayType(Token.NoToken, 1, ib.Arg); b.T = a.T; return UnifyTypes(ib.Arg, ib.Range); } else { return false; } } else if (a is CollectionTypeProxy) { if (b is CollectionTypeProxy) { a.T = b; return UnifyTypes(((CollectionTypeProxy)a).Arg, ((CollectionTypeProxy)b).Arg); } else if (b is OperationTypeProxy) { if (((OperationTypeProxy)b).AllowSeq) { b.T = a; // a is a stronger constraint than b } else { // a says set,seq and b says int,set; the intersection is set a.T = new SetType(((CollectionTypeProxy)a).Arg); b.T = a.T; } return true; } else if (b is IndexableTypeProxy) { CollectionTypeProxy pa = (CollectionTypeProxy)a; var ib = (IndexableTypeProxy)b; // pa is: // set(Arg) or multiset(Arg) or seq(Arg) or map(Arg, anyRange) // pb is: // seq(Arg) or multiset(Arg) or map(Domain, Arg), or // if AllowArray, array(Arg) // Their intersection is: if (ib.AllowArray) { var c = new IndexableTypeProxy(ib.Domain, ib.Range, ib.Arg, 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) { if (pa.AllowSeq) { a.T = b; // a has the weaker requirement } else { b.T = a; // a has the stronger requirement } return true; } else { var pb = (IndexableTypeProxy)b; // cast justification: else we have unexpected restricted-proxy type // a is: int or set or multiset or seq // b is: seq, multiset, map, or possibly array if (!pa.AllowSeq) { // strengthen a and b to a multiset type b.T = new MultiSetType(pb.Arg); a.T = b.T; return true; } else { // strengthen a and b to a sequence type b.T = new SeqType(pb.Arg); // TODO: the type is really *either* a seq or a multiset a.T = b.T; return true; } } } else if (a is IndexableTypeProxy) { var ia = (IndexableTypeProxy)a; var ib = (IndexableTypeProxy)b; // cast justification: else we have unexpected restricted-proxy type if (ia.AllowArray) { a.T = b; // a has the weaker requirement } else { b.T = a; // a has the strong requirement } 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) { 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, ResolveTypeOptionEnum.DontInfer, null); return at; } /// /// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it /// at run time. That means it must not have any side effects on non-ghost variables, for example. /// public void ResolveStatement(Statement stmt, bool specContextOnly, ICodeContext codeContext) { Contract.Requires(stmt != null); Contract.Requires(codeContext != null); ResolveAttributes(stmt.Attributes, true, codeContext); if (stmt is PredicateStmt) { PredicateStmt s = (PredicateStmt)stmt; ResolveAttributes(s.Attributes, false, codeContext); s.IsGhost = true; ResolveExpression(s.Expr, true, codeContext); Contract.Assert(s.Expr.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(s.Expr.Type, Type.Bool)) { Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type); } } else if (stmt is PrintStmt) { PrintStmt s = (PrintStmt)stmt; ResolveAttributeArgs(s.Args, false, codeContext, false); if (specContextOnly) { 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 if (stmt is BreakStmt) { var s = (BreakStmt)stmt; if (s.TargetLabel != null) { Statement target = labeledStatements.Find(s.TargetLabel); if (target == null) { Error(s, "break label is undefined or not in scope: {0}", s.TargetLabel); } else { s.TargetStmt = target; bool targetIsLoop = target is WhileStmt || target is AlternativeLoopStmt; if (specContextOnly && !s.TargetStmt.IsGhost && !inSpecOnlyContext[s.TargetStmt]) { Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure")); } } } else { if (loopStack.Count < s.BreakCount) { Error(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