//----------------------------------------------------------------------------- // // 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}", 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}", tok.filename, tok.line, tok.col - 1, string.Format(msg, args)); Console.ForegroundColor = col; } } public class Resolver : ResolutionErrorReporter { readonly BuiltIns builtIns; //Dictionary/*!*/ classes; // can map to AmbiguousTopLevelDecl //Dictionary importedNames; // the imported modules, as a map. ModuleSignature moduleInfo = null; 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; 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 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 refinementTransformer = new RefinementTransformer(this, prog); IRewriter rewriter = new AutoContractsRewriter(); systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false); 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; ModuleSignature refinedSig = null; if (m.RefinementBaseRoot != null) { if (ResolvePath(m.RefinementBaseRoot, m.RefinementBaseName, out refinedSig)) { if (refinedSig.ModuleDef != null) { m.RefinementBase = refinedSig.ModuleDef; refinementTransformer.PreResolve(m); } else { Error(m.RefinementBaseName[0], "module ({0}) named as refinement base is not a literal module or simple reference to a literal module", Util.Comma(".", m.RefinementBaseName, x => x.val)); } } else { Error(m.RefinementBaseName[0], "module ({0}) named as refinement base does not exist", Util.Comma(".", m.RefinementBaseName, x => x.val)); } } if (errorCount == ErrorCount) { rewriter.PreResolve(m); } literalDecl.Signature = RegisterTopLevelDecls(m, true); literalDecl.Signature.Refines = refinedSig; var sig = literalDecl.Signature; // set up environment var preResolveErrorCount = ErrorCount; ResolveModuleDefinition(m, sig); if (ErrorCount == preResolveErrorCount) { refinementTransformer.PostResolve(m); // give rewriter a chance to do processing rewriter.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 = 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)) { 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)) { 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)) { 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); } // compute IsRecursive bit for mutually recursive functions foreach (ModuleDefinition m in prog.Modules) { foreach (var fn in ModuleDefinition.AllFunctions(m.TopLevelDecls)) { if (!fn.IsRecursive) { // note, self-recursion has already been determined int n = m.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; } } } } } private void ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) { moduleInfo = MergeSignature(sig, systemNameInfo); // resolve var datatypeDependencies = new Graph(); var codatatypeDependencies = new Graph(); int prevErrorCount = ErrorCount; 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 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 ArbitraryTypeDecl) { // 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 bool inferredDecreases; var decr = Translator.MethodDecreasesWithDefault(iter, out inferredDecreases); if (inferredDecreases) { iter.InferredDecreases = true; Contract.Assert(iter.Decreases.Expressions.Count == 0); iter.Decreases.Expressions.AddRange(decr); } // 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, false); // --- 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, false); // --- 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, false); // 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 CoMethod) { 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)); // create prefix predicate cop.PrefixPredicate = new PrefixPredicate(cop.tok, extraName, cop.IsStatic, cop.TypeArgs.ConvertAll(cloner.CloneTypeParam), 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 = (CoMethod)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 method. Note that the body is not cloned, but simply shared. com.PrefixMethod = new PrefixMethod(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 comethod'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 comethod is known cloner.CloneAttributes(com.Attributes), com); extraMember = com.PrefixMethod; // 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.PrefixMethod, 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.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.Name, "", "", 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, 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 ArbitraryTypeDecl) { var dd = (ArbitraryTypeDecl)d; return new ArbitraryTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, null); } 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); if (dd is DefaultClassDecl) { return new DefaultClassDecl(m, mm); } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null); } 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 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 { 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, false); } else if (f is CoPredicate) { return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals, req, reads, ens, body, null, false); } else { return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType), req, reads, ens, decreases, body, null, false); } } 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, false); } else if (m is CoMethod) { return new CoMethod(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal), req, mod, ens, decreases, null, null, false); } else { return new Method(m.tok, m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal), req, mod, ens, decreases, null, null, false); } } 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.Value == null) { return new LiteralExpr(e.tok); } else if (e.Value is bool) { return new LiteralExpr(e.tok, (bool)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 FieldSelectExpr) { var e = (FieldSelectExpr)expr; return new FieldSelectExpr(e.tok, CloneExpr(e.Obj), e.FieldName); } 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 FreshExpr) { var e = (FreshExpr)expr; return new FreshExpr(e.tok, CloneExpr(e.E)); } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; return new UnaryExpr(e.tok, e.Op, CloneExpr(e.E)); } 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.Vars.ConvertAll(CloneBoundVar), 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 ForallExpr) { return new ForallExpr(tk, bvs, range, term, null); } else if (e is ExistsExpr) { return new ExistsExpr(tk, bvs, range, term, null); } else if (e is MapComprehension) { return new MapComprehension(tk, bvs, range, 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 PredicateExpr) { var e = (PredicateExpr)expr; if (e is AssertExpr) { return new AssertExpr(e.tok, CloneExpr(e.Guard), CloneExpr(e.Body)); } else { Contract.Assert(e is AssumeExpr); return new AssumeExpr(e.tok, CloneExpr(e.Guard), CloneExpr(e.Body)); } } else if (expr is CalcExpr) { var e = (CalcExpr)expr; return new CalcExpr(e.tok, (CalcStmt)((new Cloner()).CloneStmt(e.Guard)), CloneExpr(e.Body), (AssumeExpr)CloneExpr(e.AsAssumeExpr)); } 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 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)))); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression } } private bool ResolvePath(ModuleDecl root, List Path, out ModuleSignature p) { p = root.Signature; int i = 1; while (i < Path.Count) { ModuleSignature pp; if (p.FindSubmodule(Path[i].val, out pp)) { p = pp; i++; } else { 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); foreach (TopLevelDecl d in declarations) { Contract.Assert(d != null); allTypeParameters.PushMarker(); ResolveTypeParameters(d.TypeArgs, true, d); if (d is ArbitraryTypeDecl) { // nothing to do } 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(); } } 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 the type parameters of all top-level type declarations foreach (TopLevelDecl d in declarations) { Contract.Assert(d != null); allTypeParameters.PushMarker(); ResolveTypeParameters(d.TypeArgs, false, d); 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; ResolveAttributes(cl.Attributes, false, new NoContext(cl.Module)); ResolveClassMemberBodies(cl); } allTypeParameters.PopMarker(); } if (ErrorCount == prevErrorCount) { // fill in the postconditions and bodies of prefix methods foreach (var com in ModuleDefinition.AllCoMethods(declarations)) { var prefixMethod = com.PrefixMethod; if (prefixMethod == null) { continue; // something went wrong during registration of the prefix method (probably a duplicated comethod name) } Contract.Assume(prefixMethod.Ens.Count == 0 && prefixMethod.Body == null); // there are not supposed have have been filled in before // compute the postconditions of the prefix method var k = prefixMethod.Ins[0]; foreach (var p in com.Ens) { var coConclusions = new HashSet(); CheckCoMethodConclusions(p.E, true, coConclusions); var subst = new CoMethodPostconditionSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name)); var post = subst.CloneExpr(p.E); prefixMethod.Ens.Add(new MaybeFreeExpression(post, p.IsFree)); } // Compute the statement body of the prefix method 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 CoMethodBodyCloner(com, kMinusOne); 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, kPositive, mainBody, null); prefixMethod.Body = new BlockStmt(com.tok, new List() { condBody }); } // The prefix method now has all its components, so it's finally time we resolve it currentClass = (ClassDecl)prefixMethod.EnclosingClass; allTypeParameters.PushMarker(); ResolveTypeParameters(currentClass.TypeArgs, false, currentClass); ResolveTypeParameters(prefixMethod.TypeArgs, false, prefixMethod); ResolveMethod(prefixMethod); allTypeParameters.PopMarker(); currentClass = null; } foreach (TopLevelDecl d in declarations) { if (d is ClassDecl) { foreach (var member in ((ClassDecl)d).Members) { if (member is Method) { var m = (Method)member; m.Req.Iter(mfe => CheckTypeInference(mfe.E)); m.Ens.Iter(mfe => CheckTypeInference(mfe.E)); m.Mod.Expressions.Iter(fe => CheckTypeInference(fe.E)); m.Decreases.Expressions.Iter(CheckTypeInference); 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 (!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; f.Req.Iter(CheckTypeInference); f.Ens.Iter(CheckTypeInference); f.Reads.Iter(fe => CheckTypeInference(fe.E)); f.Decreases.Expressions.Iter(CheckTypeInference); 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"); } } } } } } } // 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 fn in ModuleDefinition.AllFunctions(declarations)) { var module = fn.EnclosingClass.Module; if (fn.Body != null && module.CallGraph.GetSCCRepresentative(fn) == fn) { bool dealsWithCodatatypes = false; foreach (var m in module.CallGraph.GetSCC(fn)) { var f = (Function)m; if (f.ResultType.InvolvesCoDatatype) { dealsWithCodatatypes = true; break; } } foreach (var m in module.CallGraph.GetSCC(fn)) { var f = (Function)m; var checker = new CoCallResolution(f, dealsWithCodatatypes); checker.CheckCoCalls(f.Body); } } } // 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; 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; goto DONE; } } foreach (var p in iter.Outs) { if (InferRequiredEqualitySupport(tp, p.Type)) { tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; goto DONE; } } DONE: ; } } } 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; 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; goto DONE; } } foreach (var p in m.Outs) { if (InferRequiredEqualitySupport(tp, p.Type)) { tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired; goto DONE; } } DONE: ; } } } } } } } // 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 comethods are not recursive with non-comethod 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 CoMethod) { var m = (CoMethod)member; if (m.Body != null) { CoMethodChecks(m.Body, m); } } } } } } } 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 && !stmt.IsGhost); 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 VarDecl) { } 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 = 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 ConcreteSyntaxStatement) { var s = (ConcreteSyntaxStatement)stmt; return CheckTailRecursive(s.ResolvedStatements, enclosingMethod, ref tailCall, reportErrors); } else { Contract.Assert(false); // unexpected statement type } return TailRecursionStatus.CanBeFollowedByAnything; } 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; } } void CoPredicateChecks(Expression expr, CoPredicate context, CallingPosition cp) { Contract.Requires(expr != null); Contract.Requires(context != null); if (expr is ConcreteSyntaxExpression) { var e = (ConcreteSyntaxExpression)expr; CoPredicateChecks(e.Resolved, context, cp); return; } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; var moduleCaller = context.EnclosingClass.Module; var moduleCallee = e.Function.EnclosingClass.Module; if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(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 recursive copredicate call can only be done in positive positions"; if (cp == CallingPosition.Neither) { // this may be inside a msg += " and cannot sit inside an 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; } } // fall through to do the subexpressions } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; if (e.Op == UnaryExpr.Opcode.Not) { CoPredicateChecks(e.E, context, Invert(cp)); return; } } else if (expr is BinaryExpr) { var e = (BinaryExpr)expr; switch (e.ResolvedOp) { case BinaryExpr.ResolvedOpcode.And: case BinaryExpr.ResolvedOpcode.Or: CoPredicateChecks(e.E0, context, cp); CoPredicateChecks(e.E1, context, cp); return; case BinaryExpr.ResolvedOpcode.Imp: CoPredicateChecks(e.E0, context, Invert(cp)); CoPredicateChecks(e.E1, context, cp); return; default: break; } } else if (expr is MatchExpr) { var e = (MatchExpr)expr; CoPredicateChecks(e.Source, context, CallingPosition.Neither); e.Cases.Iter(kase => CoPredicateChecks(kase.Body, context, cp)); return; } else if (expr is ITEExpr) { var e = (ITEExpr)expr; CoPredicateChecks(e.Test, context, CallingPosition.Neither); CoPredicateChecks(e.Thn, context, cp); CoPredicateChecks(e.Els, context, cp); return; } else if (expr is LetExpr) { var e = (LetExpr)expr; foreach (var rhs in e.RHSs) { CoPredicateChecks(rhs, context, 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 CoPredicateChecks(e.Body, context, e.Exact ? cp : CallingPosition.Neither); return; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; if ((cp == CallingPosition.Positive && e is ExistsExpr) || (cp == CallingPosition.Negative && e is ForallExpr)) { // Don't allow any co-recursive calls under an existential, because that can be unsound. // (Actually, I think we could be more liberal here--we could allow this if the range is finite.) cp = CallingPosition.Neither; } if (e.Range != null) { CoPredicateChecks(e.Range, context, e is ExistsExpr ? Invert(cp) : cp); } CoPredicateChecks(e.Term, context, cp); return; } expr.SubExpressions.Iter(ee => CoPredicateChecks(ee, context, CallingPosition.Neither)); } void CoMethodChecks(Statement stmt, CoMethod context) { Contract.Requires(stmt != null); Contract.Requires(context != null); if (stmt is CallStmt) { var s = (CallStmt)stmt; if (s.Method is CoMethod || s.Method is PrefixMethod) { // all is cool } else { // the call goes from a comethod context to a non-comethod callee var moduleCaller = context.EnclosingClass.Module; var moduleCallee = s.Method.EnclosingClass.Module; if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) { // we're looking at a recursive call (to a non-comethod) Error(s, "a recursive call from a comethod can go only to other comethods and prefix methods"); } } } else { stmt.SubStatements.Iter(ss => CoMethodChecks(ss, context)); } } void CheckEqualityTypes_Stmt(Statement stmt) { Contract.Requires(stmt != null); if (stmt.IsGhost) { return; } else if (stmt is PrintStmt) { var s = (PrintStmt)stmt; foreach (var arg in s.Args) { if (arg.E != null) { CheckEqualityTypes(arg.E); } } } else if (stmt is BreakStmt) { } else if (stmt is ProduceStmt) { var s = (ProduceStmt)stmt; if (s.rhss != null) { s.rhss.Iter(CheckEqualityTypes_Rhs); } } else if (stmt is AssignStmt) { AssignStmt s = (AssignStmt)stmt; CheckEqualityTypes(s.Lhs); CheckEqualityTypes_Rhs(s.Rhs); } else if (stmt is VarDecl) { var s = (VarDecl)stmt; s.SubStatements.Iter(CheckEqualityTypes_Stmt); } else if (stmt is CallStmt) { var s = (CallStmt)stmt; CheckEqualityTypes(s.Receiver); s.Args.Iter(CheckEqualityTypes); s.Lhs.Iter(CheckEqualityTypes); 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++; } } else if (stmt is BlockStmt) { var s = (BlockStmt)stmt; s.Body.Iter(CheckEqualityTypes_Stmt); } else if (stmt is IfStmt) { var s = (IfStmt)stmt; if (s.Guard != null) { CheckEqualityTypes(s.Guard); } s.SubStatements.Iter(CheckEqualityTypes_Stmt); } else if (stmt is AlternativeStmt) { var s = (AlternativeStmt)stmt; foreach (var alt in s.Alternatives) { CheckEqualityTypes(alt.Guard); alt.Body.Iter(CheckEqualityTypes_Stmt); } } else if (stmt is WhileStmt) { var s = (WhileStmt)stmt; if (s.Guard != null) { CheckEqualityTypes(s.Guard); } CheckEqualityTypes_Stmt(s.Body); } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; foreach (var alt in s.Alternatives) { CheckEqualityTypes(alt.Guard); alt.Body.Iter(CheckEqualityTypes_Stmt); } } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; CheckEqualityTypes(s.Range); CheckEqualityTypes_Stmt(s.Body); } else if (stmt is MatchStmt) { var s = (MatchStmt)stmt; CheckEqualityTypes(s.Source); foreach (MatchCaseStmt mc in s.Cases) { mc.Body.Iter(CheckEqualityTypes_Stmt); } } else if (stmt is ConcreteSyntaxStatement) { var s = (ConcreteSyntaxStatement)stmt; s.ResolvedStatements.Iter(CheckEqualityTypes_Stmt); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } } void CheckEqualityTypes_Rhs(AssignmentRhs rhs) { Contract.Requires(rhs != null); rhs.SubExpressions.Iter(CheckEqualityTypes); rhs.SubStatements.Iter(CheckEqualityTypes_Stmt); } void CheckEqualityTypes(Expression expr) { Contract.Requires(expr != null); if (expr is BinaryExpr) { var e = (BinaryExpr)expr; var t0 = e.E0.Type.Normalize(); var t1 = e.E1.Type.Normalize(); 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.Vars) { 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++; } } foreach (var ee in expr.SubExpressions) { CheckEqualityTypes(ee); } } void CheckEqualityTypes_Type(IToken tok, Type type) { Contract.Requires(tok != null); Contract.Requires(type != null); type = type.Normalize(); 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; if (udt.ResolvedClass != null) { Contract.Assert(udt.ResolvedClass.TypeArgs.Count == udt.TypeArgs.Count); var i = 0; foreach (var argType in udt.TypeArgs) { var formalTypeArg = udt.ResolvedClass.TypeArgs[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 { Contract.Assert(udt.TypeArgs.Count == 0); // TypeParameters have no type arguments } } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } } void CheckTypeIsDetermined(IToken tok, Type t, string what) { Contract.Requires(tok != null); Contract.Requires(t != null); Contract.Requires(what != null); t = t.Normalize(); if (t is TypeProxy && !(t is InferredTypeProxy || t is ParamTypeProxy || t is ObjectTypeProxy)) { Error(tok, "the type of this {0} is underspecified, but it cannot be an arbitrary type.", what); } } void CheckTypeInference(Expression e) { if (e == null) return; e.SubExpressions.Iter(CheckTypeInference); var ce = e as ComprehensionExpr; if (ce != null) { foreach (var bv in ce.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); } } } CheckTypeIsDetermined(e.tok, e.Type, "expression"); } void CheckTypeInference(Statement stmt) { Contract.Requires(stmt != null); if (stmt is PrintStmt) { var s = (PrintStmt)stmt; s.Args.Iter(arg => CheckTypeInference(arg.E)); } else if (stmt is BreakStmt) { } else if (stmt is ProduceStmt) { var s = (ProduceStmt)stmt; if (s.rhss != null) { s.rhss.Iter(rhs => rhs.SubExpressions.Iter(e => CheckTypeInference(e))); } } else if (stmt is AssignStmt) { AssignStmt s = (AssignStmt)stmt; CheckTypeInference(s.Lhs); s.Rhs.SubExpressions.Iter(e => { CheckTypeInference(e); }); } else if (stmt is VarDecl) { var s = (VarDecl)stmt; s.SubStatements.Iter(CheckTypeInference); CheckTypeIsDetermined(s.Tok, s.Type, "local variable"); } else if (stmt is CallStmt) { var s = (CallStmt)stmt; CheckTypeInference(s.Receiver); s.Args.Iter(e => CheckTypeInference(e)); s.Lhs.Iter(e => CheckTypeInference(e)); } else if (stmt is BlockStmt) { var s = (BlockStmt)stmt; s.Body.Iter(CheckTypeInference); } else if (stmt is IfStmt) { var s = (IfStmt)stmt; if (s.Guard != null) { CheckTypeInference(s.Guard); } s.SubStatements.Iter(CheckTypeInference); } else if (stmt is AlternativeStmt) { var s = (AlternativeStmt)stmt; foreach (var alt in s.Alternatives) { CheckTypeInference(alt.Guard); alt.Body.Iter(CheckTypeInference); } } else if (stmt is WhileStmt) { var s = (WhileStmt)stmt; if (s.Guard != null) { CheckTypeInference(s.Guard); } CheckTypeInference(s.Body); } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; foreach (var alt in s.Alternatives) { CheckTypeInference(alt.Guard); alt.Body.Iter(CheckTypeInference); } } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; CheckTypeInference(s.Range); CheckTypeInference(s.Body); s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); } else if (stmt is CalcStmt) { var s = (CalcStmt)stmt; s.SubExpressions.Iter(e => CheckTypeInference(e)); s.SubStatements.Iter(CheckTypeInference); } else if (stmt is MatchStmt) { var s = (MatchStmt)stmt; CheckTypeInference(s.Source); foreach (MatchCaseStmt mc in s.Cases) { mc.Body.Iter(CheckTypeInference); } } else if (stmt is ConcreteSyntaxStatement) { var s = (ConcreteSyntaxStatement)stmt; s.ResolvedStatements.Iter(CheckTypeInference); } else if (stmt is PredicateStmt) { CheckTypeInference(((PredicateStmt)stmt).Expr); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } } 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 ""; } bool InferRequiredEqualitySupport(TypeParameter tp, Type type) { Contract.Requires(tp != null); Contract.Requires(type != null); type = type.Normalize(); 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; if (udt.ResolvedClass != null) { var i = 0; foreach (var argType in udt.TypeArgs) { var formalTypeArg = udt.ResolvedClass.TypeArgs[i]; if ((formalTypeArg.MustSupportEquality && argType.AsTypeParameter == tp) || InferRequiredEqualitySupport(tp, argType)) { return true; } i++; } } else { Contract.Assert(udt.TypeArgs.Count == 0); // TypeParameters have no type arguments } } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } return false; } ClassDecl currentClass; Function currentFunction; 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; foreach (MemberDecl member in cl.Members) { member.EnclosingClass = cl; if (member is Field) { ResolveType(member.tok, ((Field)member).Type, ResolveTypeOption.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 CoMethod; if (com != null && com.PrefixMethod != null && ec == ErrorCount) { var mm = com.PrefixMethod; // resolve signature of the prefix method 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; } /// /// 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)); 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) { 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. 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 ((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.Normalize(); 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.Normalize(); 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) { Contract.Assert(tp != null); 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 ? ResolveTypeOption.AllowPrefixExtend : ResolveTypeOption.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); Contract.Requires(currentFunction == null); Contract.Ensures(currentFunction == null); scope.PushMarker(); currentFunction = f; if (f.IsStatic) { scope.AllowInstance = false; } foreach (Formal p in f.Formals) { scope.Push(p.Name, p); } ResolveAttributes(f.Attributes, false, new NoContext(currentClass.Module)); foreach (Expression r in f.Req) { ResolveExpression(r, false, new NoContext(currentFunction.EnclosingClass.Module)); 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"); } foreach (Expression r in f.Ens) { ResolveExpression(r, false, new NoContext(currentClass.Module)); // 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); } } foreach (Expression r in f.Decreases.Expressions) { ResolveExpression(r, false, new NoContext(currentClass.Module)); // any type is fine } if (f.Body != null) { var prevErrorCount = ErrorCount; List matchVarContext = new List(f.Formals); ResolveExpression(f.Body, false, new NoContext(currentClass.Module), matchVarContext); if (!f.IsGhost) { 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); } } currentFunction = null; scope.PopMarker(); } void ResolveFrameExpression(FrameExpression fe, string kind) { Contract.Requires(fe != null); Contract.Requires(kind != null); ResolveExpression(fe.E, false, new NoContext(moduleInfo.ModuleDef)); Type t = fe.E.Type; Contract.Assert(t != null); // follows from postcondition of ResolveExpression if (t is CollectionType) { t = ((CollectionType)t).Arg; } if (t is ObjectType) { // fine, as long as there's no field name if (fe.FieldName != null) { Error(fe.E, "type '{0}' does not contain a field named '{1}'", t, fe.FieldName); } } else if (UserDefinedType.DenotesClass(t) != null) { // fine type 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, cce.NonNull(ctype).Name); } else { Contract.Assert(ctype != null && ctype.ResolvedClass != null); // follows from postcondition of ResolveMember fe.Field = (Field)member; } } } else { Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type); } } /// /// 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 ? ResolveTypeOption.AllowPrefixExtend : ResolveTypeOption.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); // 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) { 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); } } foreach (FrameExpression fe in m.Mod.Expressions) { ResolveFrameExpression(fe, "modifies"); if (m is CoMethod) { Error(fe.tok, "comethods are not allowed to have modifies clauses"); } } 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(); foreach (Formal p in m.Outs) { scope.Push(p.Name, p); } // ... continue resolving specification foreach (MaybeFreeExpression e in m.Ens) { 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 CoMethod; if (com != null && com.PrefixMethod != null) { // The body may mentioned the implicitly declared parameter _k. Throw it into the // scope before resolving the body. var k = com.PrefixMethod.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 comethods) ResolveAttributes(m.Attributes, false, m); scope.PopMarker(); // for the out-parameters and outermost-level locals scope.PopMarker(); // for the in-parameters } void ResolveCtorSignature(DatatypeCtor ctor, List dtTypeArguments) { Contract.Requires(ctor != null); Contract.Requires(dtTypeArguments != null); foreach (Formal p in ctor.Formals) { ResolveType(p.tok, p.Type, ResolveTypeOption.AllowExact, 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 ? ResolveTypeOption.AllowPrefixExtend : ResolveTypeOption.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"); } foreach (FrameExpression fe in iter.Modifies.Expressions) { ResolveFrameExpression(fe, "modifies"); } 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 FieldSelectExpr(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 FieldSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new SeqDisplayExpr(p.tok, new List())))); } // ensures this.Valid(); ens.Add(new MaybeFreeExpression(new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List()))); // 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 FieldSelectExpr(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 FieldSelectExpr(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 FieldSelectExpr(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 FieldSelectExpr(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 FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_reads"), null)); // reads this._reads; reads.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null)); // reads this._new; // ---------- here comes method MoveNext() ---------- // requires this.Valid(); var req = iter.Member_MoveNext.Req; req.Add(new MaybeFreeExpression(new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List()))); // 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 FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"), null)); mod.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null)); // ensures fresh(_new - old(_new)); ens = iter.Member_MoveNext.Ens; ens.Add(new MaybeFreeExpression(new FreshExpr(iter.tok, new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new")))))); // ensures more ==> this.Valid(); ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, new IdentifierExpr(iter.tok, "more"), new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List())))); // 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 FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)), new SeqDisplayExpr(iter.tok, new List() { new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), y.Name) })), new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name))); var eq = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new FieldSelectExpr(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 UnaryExpr(iter.tok, UnaryExpr.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 FieldSelectExpr(p.tok, new ThisExpr(p.tok), iter.DecreasesFields[i].Name)); } iter.Member_MoveNext.Decreases.Attributes = iter.Decreases.Attributes; } /// /// 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 ResolveTypeOption { /// /// never infer type arguments /// DontInfer, /// /// create a new InferredTypeProxy type for each needed argument /// InferTypeProxies, /// /// if exactly defaultTypeArguments.Count type arguments are needed, use defaultTypeArguments /// AllowExact, /// /// 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, ResolveTypeOption option, List defaultTypeArguments) { Contract.Requires((option == ResolveTypeOption.DontInfer || option == ResolveTypeOption.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 == ResolveTypeOption.DontInfer || option == ResolveTypeOption.InferTypeProxies) == (defaultTypeArguments == null)); if (type is BasicType) { // nothing to resolve } else if (type is MapType) { MapType mt = (MapType)type; ResolveType(tok, mt.Domain, option, defaultTypeArguments); ResolveType(tok, mt.Range, option, defaultTypeArguments); 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; var argType = t.Arg; ResolveType(tok, argType, option, defaultTypeArguments); if (argType.IsSubrangeType) { Error(tok, "sorry, cannot instantiate collection type with a subrange type"); } } else if (type is UserDefinedType) { UserDefinedType t = (UserDefinedType)type; foreach (Type tt in t.TypeArgs) { ResolveType(t.tok, tt, option, defaultTypeArguments); if (tt.IsSubrangeType) { Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type"); } } 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 if (t.ResolvedClass == null) { // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string') 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) 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 if (d is ArbitraryTypeDecl) { t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType; // resolve like a type parameter } else { // d is a class or datatype, and it may have type parameters t.ResolvedClass = d; if (option == ResolveTypeOption.DontInfer) { // don't add anything } else if (d.TypeArgs.Count != t.TypeArgs.Count && t.TypeArgs.Count == 0) { if (option == ResolveTypeOption.InferTypeProxies) { // add type arguments that will be inferred for (int i = 0; i < d.TypeArgs.Count; i++) { t.TypeArgs.Add(new InferredTypeProxy()); } } else if (option == ResolveTypeOption.AllowExact && defaultTypeArguments.Count != d.TypeArgs.Count) { // the number of default arguments is not exactly what we need, so don't add anything } else if (option == ResolveTypeOption.AllowPrefix && defaultTypeArguments.Count < d.TypeArgs.Count) { // there aren't enough default arguments, so don't do anything } else { // we'll add arguments if (option == ResolveTypeOption.AllowPrefixExtend) { // extend defaultTypeArguments, if needed for (int i = defaultTypeArguments.Count; i < d.TypeArgs.Count; i++) { defaultTypeArguments.Add(new TypeParameter(t.tok, "_T" + i)); } } Contract.Assert(d.TypeArgs.Count <= defaultTypeArguments.Count); // automatically supply a prefix of the arguments from defaultTypeArguments for (int i = 0; i < d.TypeArgs.Count; i++) { var typeArg = new UserDefinedType(t.tok, defaultTypeArguments[i].Name, new List(), null); typeArg.ResolvedParam = defaultTypeArguments[i]; // resolve "typeArg" here t.TypeArgs.Add(typeArg); } } } // 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 class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, 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; } public bool UnifyTypes(Type a, Type b) { Contract.Requires(a != null); Contract.Requires(b != null); while (a is TypeProxy) { TypeProxy proxy = (TypeProxy)a; if (proxy.T == null) { // merge a and b; to avoid cycles, first get to the bottom of b while (b is TypeProxy && ((TypeProxy)b).T != null) { b = ((TypeProxy)b).T; } return AssignProxy(proxy, b); } else { a = proxy.T; } } while (b is TypeProxy) { TypeProxy proxy = (TypeProxy)b; if (proxy.T == null) { // merge a and b (we have already got to the bottom of a) return AssignProxy(proxy, a); } else { b = proxy.T; } } #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 is BoolType || other is IntType || other is SetType || other is SeqType || other.IsDatatype) { 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 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; } UserDefinedType aa = (UserDefinedType)a; UserDefinedType 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; i < aa.TypeArgs.Count; i++) { if (!UnifyTypes(aa.TypeArgs[i], bb.TypeArgs[i])) { successSoFar = false; } } return successSoFar; } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) { // these are both resolved type parameters Contract.Assert(aa.TypeArgs.Count == 0 && bb.TypeArgs.Count == 0); return true; } 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.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 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 SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) { // this is the expected case } else { return false; } } else if (proxy is IndexableTypeProxy) { IndexableTypeProxy iProxy = (IndexableTypeProxy)proxy; if (t is SeqType) { if (!UnifyTypes(iProxy.Arg, ((SeqType)t).Arg)) { return false; } if (!UnifyTypes(iProxy.Domain, Type.Int)) { return false; } } else if (t.IsArrayType && (t.AsArrayType).Dims == 1) { Type elType = UserDefinedType.ArrayElementType(t); if (!UnifyTypes(iProxy.Arg, elType)) { return false; } if (!UnifyTypes(iProxy.Domain, Type.Int)) { return false; } } else if (t is MapType) { if (!UnifyTypes(iProxy.Arg, ((MapType)t).Range)) { return false; } if (!UnifyTypes(iProxy.Domain, ((MapType)t).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) { // the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type a.T = builtIns.ArrayType(1, ((IndexableTypeProxy)b).Arg); b.T = a.T; return true; } 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; IndexableTypeProxy pb = (IndexableTypeProxy)b; // a and b could be a map or a sequence return true; } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type } } else if (a is OperationTypeProxy) { OperationTypeProxy pa = (OperationTypeProxy)a; if (b is OperationTypeProxy) { if (!pa.AllowSeq || ((OperationTypeProxy)b).AllowSeq) { b.T = a; } else { a.T = b; // b has the stronger requirement } return true; } else { IndexableTypeProxy pb = (IndexableTypeProxy)b; // cast justification: lse we have unexpected restricted-proxy type if (pa.AllowSeq) { // strengthen a and b to a sequence type b.T = new SeqType(pb.Arg); a.T = b.T; return true; } else { return false; } } } else if (a is IndexableTypeProxy) { Contract.Assert(b is IndexableTypeProxy); // else we have unexpected restricted-proxy type a.T = b; return UnifyTypes(((IndexableTypeProxy)a).Arg, ((IndexableTypeProxy)b).Arg); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type } } /// /// "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); 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