diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 6706 |
1 files changed, 6706 insertions, 0 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs new file mode 100644 index 00000000..a876864e --- /dev/null +++ b/Source/Dafny/Resolver.cs @@ -0,0 +1,6706 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+
+ /// <summary>
+ /// This method is virtual, because it is overridden in the VSX plug-in for Dafny.
+ /// </summary>
+ 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<string/*!*/,TopLevelDecl/*!*/>/*!*/ classes; // can map to AmbiguousTopLevelDecl
+ //Dictionary<string, ModuleDecl> 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<TypeParameter>(), 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<string/*!*/, Tuple<DatatypeCtor, bool>> allDatatypeCtors;
+
+ readonly Dictionary<ClassDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ classMembers = new Dictionary<ClassDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();
+ readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ datatypeMembers = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();
+ readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>/*!*/ datatypeCtors = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>();
+ readonly Graph<ModuleDecl/*!*/>/*!*/ dependencies = new Graph<ModuleDecl/*!*/>();
+ 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<ModuleDecl> 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<ModuleDecl> 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;
+ rewriter.PreResolve(m);
+ 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));
+ }
+ }
+ literalDecl.Signature = RegisterTopLevelDecls(m, true);
+ literalDecl.Signature.Refines = refinedSig;
+ var sig = literalDecl.Signature;
+ // set up environment
+ var preResolveErrorCount = ErrorCount;
+ useCompileSignatures = false;
+ ResolveModuleDefinition(m, sig);
+ if (ErrorCount == preResolveErrorCount) {
+ refinementTransformer.PostResolve(m);
+ // give rewriter a chance to do processing
+ rewriter.PostResolve(m);
+ }
+ if (ErrorCount == errorCount && !m.IsGhost) {
+ // compilation should only proceed if everything is good, including the signature (which preResolveErrorCount does not include);
+ var nw = (new Cloner()).CloneModuleDefinition(m, m.CompileName + "_Compile");
+ var compileSig = RegisterTopLevelDecls(nw, true);
+ compileSig.Refines = refinedSig;
+ sig.CompileSignature = compileSig;
+ useCompileSignatures = true;
+ ResolveModuleDefinition(nw, compileSig);
+ prog.CompileModules.Add(nw);
+ }
+ } 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 AbstractModuleDecl) {
+ var abs = (AbstractModuleDecl)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;
+ }
+ }
+ }
+ }
+ }
+
+ private void ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) {
+ moduleInfo = MergeSignature(sig, systemNameInfo);
+ // resolve
+ var datatypeDependencies = new Graph<IndDatatypeDecl>();
+ int prevErrorCount = ErrorCount;
+ ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies);
+ if (ErrorCount == prevErrorCount) {
+ ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
+ }
+ }
+
+
+ public class ModuleBindings
+ {
+ private ModuleBindings parent;
+ private Dictionary<string, ModuleDecl> modules;
+ private Dictionary<string, ModuleBindings> bindings;
+
+ public ModuleBindings(ModuleBindings p) {
+ parent = p;
+ modules = new Dictionary<string, ModuleDecl>();
+ bindings = new Dictionary<string, ModuleBindings>();
+ }
+ 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<ModuleDecl> 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 AbstractModuleDecl) {
+ var subdecl = (AbstractModuleDecl)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<ModuleDecl> dependencies) {
+ if (m.RefinementBaseName != null) {
+ ModuleDecl other;
+ if (!bindings.TryLookup(m.RefinementBaseName[0], out other)) {
+ Error(m, "module {0} named as refinement base does not exist", m.RefinementBaseName[0].val);
+ } else if (other is LiteralModuleDecl && ((LiteralModuleDecl)other).ModuleDef == m) {
+ Error(m, "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<ModuleDecl> 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 AbstractModuleDecl) {
+ var abs = moduleDecl as AbstractModuleDecl;
+ 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<IToken> path) {
+ 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.IsGhost;
+ List<TopLevelDecl> 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 = ((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<DatatypeCtor, bool> pair;
+ if (sig.Ctors.TryGetValue(kv.Key, out pair)) {
+ // mark it as a duplicate
+ sig.Ctors[kv.Key] = new Tuple<DatatypeCtor, bool>(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<string, TopLevelDecl> toplevels = new Dictionary<string, TopLevelDecl>();
+ // 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<string, MemberDecl>();
+ 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<Field>() { 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, iter.Name, new List<TypeParameter>(), iter.Ins,
+ new List<MaybeFreeExpression>(),
+ new Specification<FrameExpression>(new List<FrameExpression>(), null),
+ new List<MaybeFreeExpression>(),
+ new Specification<Expression>(new List<Expression>(), null),
+ null, null, false);
+ // --- here comes predicate Valid()
+ var valid = new Predicate(iter.tok, "Valid", false, true, new List<TypeParameter>(), iter.tok,
+ new List<Formal>(),
+ new List<Expression>(),
+ new List<FrameExpression>(),
+ new List<Expression>(),
+ new Specification<Expression>(new List<Expression>(), null),
+ null, Predicate.BodyOriginKind.OriginalOrInherited, null, false);
+ // --- here comes method MoveNext
+ var moveNext = new Method(iter.tok, "MoveNext", false, false, new List<TypeParameter>(),
+ new List<Formal>(), new List<Formal>() { new Formal(iter.tok, "more", Type.Bool, false, false) },
+ new List<MaybeFreeExpression>(),
+ new Specification<FrameExpression>(new List<FrameExpression>(), null),
+ new List<MaybeFreeExpression>(),
+ new Specification<Expression>(new List<Expression>(), 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<string, MemberDecl>();
+ classMembers.Add(cl, members);
+
+ bool hasConstructor = false;
+ foreach (MemberDecl m in cl.Members) {
+ if (members.ContainsKey(m.Name)) {
+ Error(m, "Duplicate member name: {0}", m.Name);
+ } else {
+ members.Add(m.Name, m);
+ }
+ 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<string, DatatypeCtor>();
+ datatypeCtors.Add(dt, ctors);
+ // ... and of the other members
+ var members = new Dictionary<string, MemberDecl>();
+ 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<DatatypeCtor, bool> pair;
+ if (sig.Ctors.TryGetValue(ctor.Name, out pair)) {
+ // mark it as a duplicate
+ sig.Ctors[ctor.Name] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);
+ } else {
+ // add new
+ sig.Ctors.Add(ctor.Name, new Tuple<DatatypeCtor, bool>(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) {
+ SpecialField dtor = null;
+ if (formal.HasName) {
+ if (members.ContainsKey(formal.Name)) {
+ Error(ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);
+ } else {
+ dtor = new DatatypeDestructor(formal.tok, ctor, formal, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);
+ dtor.EnclosingClass = dt; // resolve here
+ members.Add(formal.Name, dtor);
+ }
+ }
+ ctor.Destructors.Add(dtor);
+ }
+ }
+ }
+ }
+ return sig;
+ }
+
+ private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, List<ModuleDefinition> 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<ModuleDefinition> 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 AbstractModuleDecl) {
+ var abs = (AbstractModuleDecl)d;
+ var sig = MakeAbstractSignature(abs.OriginalSignature, Name + "." + abs.Name, abs.Height, mods);
+ var a = new AbstractModuleDecl(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 {
+ 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<Expression> CloneSpecExpr(Specification<Expression> spec) {
+ var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr);
+ return new Specification<Expression>(ee, null);
+ }
+ Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {
+ var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr);
+ return new Specification<FrameExpression>(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));
+ }
+ 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<ExpressionPair> pp = new List<ExpressionPair>();
+ 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 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));
+
+ } 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 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<IToken> 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<TopLevelDecl/*!*/>/*!*/ declarations, Graph<IndDatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
+ Contract.Requires(declarations != null);
+ Contract.Requires(datatypeDependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(datatypeDependencies));
+ 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.IsGhost) {
+ if (decl.Signature.IsGhost)
+ {
+ if (!(def.IsDefaultModule)) // _module is allowed to contain ghost modules, but not be ghost itself. Note this presents a challenge to
+ // trusted verification, as toplevels can't be trusted if they invoke ghost module members.
+ Error(d.tok, "ghost modules can only be imported into other ghost modules, not physical ones.");
+ } else {
+ // physical modules are allowed everywhere
+ }
+ } else {
+ // everything is allowed in a ghost module
+ }
+ } else {
+ ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies);
+ }
+ allTypeParameters.PopMarker();
+ }
+ }
+
+ public void ResolveTopLevelDecls_Meat(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<IndDatatypeDecl/*!*/>/*!*/ datatypeDependencies) {
+ Contract.Requires(declarations != null);
+ Contract.Requires(cce.NonNullElements(datatypeDependencies));
+
+ 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;
+ allTypeParameters.PushMarker();
+ ResolveTypeParameters(iter.TypeArgs, false, iter);
+ ResolveIterator(iter);
+ allTypeParameters.PopMarker();
+ ResolveClassMemberBodies(iter); // resolve the automatically generated members
+
+ } else if (d is ClassDecl) {
+ var cl = (ClassDecl)d;
+ ResolveAttributes(cl.Attributes, false);
+ ResolveClassMemberBodies(cl);
+ }
+ allTypeParameters.PopMarker();
+ }
+
+ if (ErrorCount == prevErrorCount) {
+ foreach (TopLevelDecl d in declarations) {
+ if (d is ClassDecl) {
+ foreach (var member in ((ClassDecl)d).Members) {
+ if (member is Method) {
+ var m = (Method)member;
+ 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;
+ 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);
+ }
+ }
+
+ 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.
+ foreach (var fn in ModuleDefinition.AllFunctions(declarations)) {
+ if (fn.Body != null && (fn is CoPredicate || fn.IsRecursive)) {
+ CoPredicateChecks(fn.Body, fn, CallingPosition.Positive);
+ }
+ }
+ }
+ }
+
+ 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
+ }
+
+ /// <summary>
+ /// 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).
+ /// </summary>
+ TailRecursionStatus CheckTailRecursive(List<Statement> 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;
+ }
+
+ /// <summary>
+ /// See CheckTailRecursive(List Statement, ...), including its description of "tailCall".
+ /// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method.
+ /// </summary>
+ 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 ParallelStmt) {
+ var s = (ParallelStmt)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 parallel 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, Function 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 (context is CoPredicate) {
+ if (!(e.Function is CoPredicate)) {
+ Error(e, "a recursive call from a copredicate can go only to other copredicates");
+ } else if (cp != CallingPosition.Positive) {
+ Error(e, "a recursive copredicate call can only be done in positive positions");
+ }
+ } else if (e.Function is CoPredicate) {
+ Error(e, "a recursive call from a non-copredicate can go only to other non-copredicates");
+ }
+ }
+ // 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);
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ CoPredicateChecks(e.Body, context, cp);
+ return;
+ } else if (expr is QuantifierExpr) {
+ var e = (QuantifierExpr)expr;
+ 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 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 ParallelStmt) {
+ var s = (ParallelStmt)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
+ }
+ }
+
+ bool CheckTypeInference(Expression e) {
+ if (e == null) return false;
+ foreach (Expression se in e.SubExpressions) {
+ if (CheckTypeInference(se))
+ return true;
+ }
+ if (e.Type is TypeProxy && !(e.Type is InferredTypeProxy || e.Type is ParamTypeProxy || e.Type is ObjectTypeProxy)) {
+ Error(e.tok, "the type of this expression is underspecified, but it cannot be an arbitrary type.");
+ return true;
+ }
+ return false;
+ }
+ 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);
+ if (s.Type is TypeProxy && !(s.Type is InferredTypeProxy || s.Type is ParamTypeProxy || s.Type is ObjectTypeProxy)) {
+ Error(s.Tok, "the type of this expression is underspecified, but it cannot be an arbitrary type.");
+ }
+ } 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 ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+ CheckTypeInference(s.Range);
+ CheckTypeInference(s.Body);
+ } else if (stmt is CalcStmt) {
+ // NadiaToDo: is this correct?
+ 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<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();
+ readonly Scope<IVariable>/*!*/ scope = new Scope<IVariable>();
+ Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
+ List<Statement> loopStack = new List<Statement>(); // the enclosing loops (from which it is possible to break out)
+ readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>(); // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
+
+
+ /// <summary>
+ /// Assumes type parameters have already been pushed
+ /// </summary>
+ 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, null, false);
+
+ } else if (member is Function) {
+ Function f = (Function)member;
+ allTypeParameters.PushMarker();
+ ResolveTypeParameters(f.TypeArgs, true, f);
+ ResolveFunctionSignature(f);
+ allTypeParameters.PopMarker();
+
+ } else if (member is Method) {
+ Method m = (Method)member;
+ allTypeParameters.PushMarker();
+ ResolveTypeParameters(m.TypeArgs, true, m);
+ ResolveMethodSignature(m);
+ allTypeParameters.PopMarker();
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type
+ }
+ }
+ currentClass = null;
+ }
+
+ /// <summary>
+ /// Assumes type parameters have already been pushed, and that all types in class members have been resolved
+ /// </summary>
+ 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);
+ // nothing more to do
+
+ } else if (member is Function) {
+ Function f = (Function)member;
+ allTypeParameters.PushMarker();
+ ResolveTypeParameters(f.TypeArgs, false, f);
+ ResolveFunction(f);
+ allTypeParameters.PopMarker();
+
+ } else if (member is Method) {
+ Method m = (Method)member;
+ allTypeParameters.PushMarker();
+ ResolveTypeParameters(m.TypeArgs, false, m);
+ ResolveMethod(m);
+ allTypeParameters.PopMarker();
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type
+ }
+ }
+ currentClass = null;
+ }
+
+ /// <summary>
+ /// Assumes type parameters have already been pushed
+ /// </summary>
+ void ResolveCtorTypes(DatatypeDecl/*!*/ dt, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies) {
+ Contract.Requires(dt != null);
+ Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
+ foreach (DatatypeCtor ctor in dt.Ctors) {
+
+ ctor.EnclosingDatatype = dt;
+
+ allTypeParameters.PushMarker();
+ ResolveCtorSignature(ctor, dt.TypeArgs);
+ allTypeParameters.PopMarker();
+
+ if (dt is IndDatatypeDecl) {
+ var idt = (IndDatatypeDecl)dt;
+ dependencies.AddVertex(idt);
+ foreach (Formal p in ctor.Formals) {
+ AddDatatypeDependencyEdge(idt, p.Type, dependencies);
+ }
+ }
+ }
+ }
+
+ void AddDatatypeDependencyEdge(IndDatatypeDecl/*!*/ dt, Type/*!*/ tp, Graph<IndDatatypeDecl/*!*/>/*!*/ 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((IndDatatypeDecl)dt, dependee);
+ foreach (var ta in ((UserDefinedType)tp).TypeArgs) {
+ AddDatatypeDependencyEdge(dt, ta, dependencies);
+ }
+ }
+ }
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ void SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph<IndDatatypeDecl/*!*/>/*!*/ 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;
+ }
+ }
+ }
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ 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<bool>() || 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<TypeParameter>();
+ 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<TypeParameter> 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<IndDatatypeDecl/*!*/>/*!*/ 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) {
+ // 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, true);
+ }
+ }
+ }
+
+ void ResolveAttributeArgs(List<Attributes.Argument/*!*/>/*!*/ args, bool twoState, bool allowGhosts) {
+ Contract.Requires(args != null);
+ foreach (Attributes.Argument aa in args) {
+ Contract.Assert(aa != null);
+ if (aa.E != null) {
+ ResolveExpression(aa.E, twoState);
+ if (!allowGhosts) {
+ CheckIsNonGhost(aa.E);
+ }
+ }
+ }
+ }
+
+ void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ 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);
+ }
+ }
+ }
+
+ /// <summary>
+ /// Assumes type parameters have already been pushed
+ /// </summary>
+ 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 defaultTypeArguments = f.TypeArgs.Count == 0 ? f.TypeArgs : null;
+ 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, defaultTypeArguments, true);
+ }
+ ResolveType(f.tok, f.ResultType, defaultTypeArguments, true);
+ scope.PopMarker();
+ }
+
+ /// <summary>
+ /// Assumes type parameters have already been pushed
+ /// </summary>
+ 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);
+ foreach (Expression r in f.Req) {
+ ResolveExpression(r, false);
+ 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); // 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);
+ // any type is fine
+ }
+ if (f.Body != null) {
+ var prevErrorCount = ErrorCount;
+ List<IVariable> matchVarContext = new List<IVariable>(f.Formals);
+ ResolveExpression(f.Body, false, 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);
+ 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);
+ }
+ }
+
+ /// <summary>
+ /// Assumes type parameters have already been pushed
+ /// </summary>
+ 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 defaultTypeArguments = m.TypeArgs.Count == 0 ? m.TypeArgs : null;
+ // 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, defaultTypeArguments, true);
+ }
+ // 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, defaultTypeArguments, true);
+ }
+ scope.PopMarker();
+ }
+
+ /// <summary>
+ /// Assumes type parameters have already been pushed
+ /// </summary>
+ 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);
+ 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");
+ }
+
+ foreach (Expression e in m.Decreases.Expressions) {
+ ResolveExpression(e, false);
+ // 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);
+ }
+
+ // attributes are allowed to mention both in- and out-parameters
+ ResolveAttributes(m.Attributes, false);
+
+ // ... continue resolving specification
+ foreach (MaybeFreeExpression e in m.Ens) {
+ ResolveExpression(e.E, true);
+ 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) {
+ ResolveBlockStatement(m.Body, m.IsGhost, m);
+ }
+
+ scope.PopMarker(); // for the out-parameters and outermost-level locals
+ scope.PopMarker(); // for the in-parameters
+ }
+
+ void ResolveCtorSignature(DatatypeCtor ctor, List<TypeParameter> dtTypeArguments) {
+ Contract.Requires(ctor != null);
+ Contract.Requires(dtTypeArguments != null);
+ foreach (Formal p in ctor.Formals) {
+ ResolveType(p.tok, p.Type, dtTypeArguments, false);
+ }
+ }
+
+ /// <summary>
+ /// Assumes type parameters have already been pushed
+ /// </summary>
+ 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 defaultTypeArguments = iter.TypeArgs.Count == 0 ? iter.TypeArgs : null;
+ // resolve the types of the parameters
+ foreach (var p in iter.Ins.Concat(iter.Outs)) {
+ ResolveType(p.tok, p.Type, defaultTypeArguments, true);
+ }
+ // 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, defaultTypeArguments, true);
+ }
+ scope.PopMarker();
+ }
+
+ /// <summary>
+ /// Assumes type parameters have already been pushed
+ /// </summary>
+ 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<n> 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);
+ // any type is fine, but associate this type with the corresponding _decreases<n> 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);
+ 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);
+ 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);
+ 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);
+ 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);
+
+ 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);
+ }
+ }
+
+ /// <summary>
+ /// Assumes the specification of the iterator itself has been successfully resolved.
+ /// </summary>
+ 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<Expression>()))));
+ }
+ // ensures this.Valid();
+ ens.Add(new MaybeFreeExpression(new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List<Expression>())));
+ // ensures this._reads == old(ReadsClause);
+ var modSetSingletons = new List<Expression>();
+ 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<Expression>();
+ 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<Expression>()))));
+ // 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<Expression>())));
+ // 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<Expression>()))));
+ // 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<Expression>() { 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;
+ }
+
+ /// <summary>
+ /// If ResolveType encounters a type "T" that takes type arguments but wasn't given any, then:
+ /// * If "defaultTypeArguments" is non-null and "defaultTypeArgument.Count" equals the number
+ /// of type arguments that "T" expects, then use these default type arguments as "T"'s arguments.
+ /// * If "allowAutoTypeArguments" is true, then infer "T"'s arguments.
+ /// * If "defaultTypeArguments" is non-null AND "allowAutoTypeArguments" is true, then enough
+ /// type parameters will be added to "defaultTypeArguments" to have at least as many type
+ /// parameters as "T" expects, and then a prefix of the "defaultTypeArguments" will be supplied
+ /// as arguments to "T".
+ /// </summary>
+ public void ResolveType(IToken tok, Type type, List<TypeParameter> defaultTypeArguments, bool allowAutoTypeArguments) {
+ Contract.Requires(tok != null);
+ Contract.Requires(type != null);
+ if (type is BasicType) {
+ // nothing to resolve
+ } else if (type is MapType) {
+ MapType mt = (MapType)type;
+ ResolveType(tok, mt.Domain, defaultTypeArguments, allowAutoTypeArguments);
+ ResolveType(tok, mt.Range, defaultTypeArguments, allowAutoTypeArguments);
+ 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, defaultTypeArguments, allowAutoTypeArguments);
+ 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, defaultTypeArguments, allowAutoTypeArguments);
+ 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 = 0;
+ var sig = moduleInfo;
+ while (j < t.Path.Count) {
+ if (sig.FindSubmodule(t.Path[j].val, out sig)) {
+ j++;
+ sig = GetSignature(sig);
+ } 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 (d.TypeArgs.Count != t.TypeArgs.Count && t.TypeArgs.Count == 0) {
+ if (allowAutoTypeArguments && defaultTypeArguments == null) {
+ // add type arguments that will be inferred
+ for (int i = 0; i < d.TypeArgs.Count; i++) {
+ t.TypeArgs.Add(new InferredTypeProxy());
+ }
+ } else if (defaultTypeArguments != null) {
+ // add specific type arguments, drawn from defaultTypeArguments (which may have to be extended)
+ if (allowAutoTypeArguments) {
+ // add to defaultTypeArguments the necessary number of arguments
+ for (int i = defaultTypeArguments.Count; i < d.TypeArgs.Count; i++) {
+ defaultTypeArguments.Add(new TypeParameter(t.tok, "_T" + i));
+ }
+ }
+ if (allowAutoTypeArguments || d.TypeArgs.Count == defaultTypeArguments.Count) {
+ 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<Type>(), 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, defaultTypeArguments, allowAutoTypeArguments);
+ }
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
+ }
+ }
+
+ 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<bool>() == (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) {
+ if (t.IsIndDatatype) {
+ // 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<bool>() || a.T != null || b.T != null);
+
+ if (a is DatatypeProxy) {
+ if (b is DatatypeProxy) {
+ // 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<T>,seq<T> and b says int,set; the intersection is set<T>
+ 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
+ }
+ }
+
+ /// <summary>
+ /// "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.
+ /// </summary>
+ 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);
+ s.IsGhost = true;
+ ResolveExpression(s.Expr, true);
+ 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, 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<Label>(new Label(target.Tok, null), null);
+ }
+ s.TargetStmt = target;
+ if (specContextOnly && !target.IsGhost && !inSpecOnlyContext[target]) {
+ Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost loop");
+ }
+ }
+ }
+
+ } else if (stmt is ProduceStmt) {
+ var kind = stmt is YieldStmt ? "yield" : "return";
+ if (stmt is YieldStmt && !(codeContext is IteratorDecl)) {
+ Error(stmt, "yield statement is allowed only in iterators");
+ } else if (stmt is ReturnStmt && !(codeContext is Method)) {
+ Error(stmt, "return statement is allowed only in method");
+ } else if (specContextOnly && !codeContext.IsGhost) {
+ Error(stmt, "{0} statement is not allowed in this context (because it is guarded by a specification-only expression)", kind);
+ }
+ var s = (ProduceStmt)stmt;
+ if (s.rhss != null) {
+ if (codeContext.Outs.Count != s.rhss.Count)
+ Error(s, "number of {2} parameters does not match declaration (found {0}, expected {1})", s.rhss.Count, codeContext.Outs.Count, kind);
+ else {
+ Contract.Assert(s.rhss.Count > 0);
+ // Create a hidden update statement using the out-parameter formals, resolve the RHS, and check that the RHS is good.
+ List<Expression> formals = new List<Expression>();
+ int i = 0;
+ foreach (Formal f in codeContext.Outs) {
+ IdentifierExpr ident = new IdentifierExpr(f.tok, f.Name);
+ ident.Var = f;
+ ident.Type = ident.Var.Type;
+ Contract.Assert(f.Type != null);
+ formals.Add(ident);
+ // link the receiver parameter properly:
+ if (s.rhss[i] is TypeRhs) {
+ var r = (TypeRhs)s.rhss[i];
+ if (r.InitCall != null) {
+ r.InitCall.Receiver = ident;
+ }
+ }
+ i++;
+ }
+ s.hiddenUpdate = new UpdateStmt(s.Tok, formals, s.rhss, true);
+ // resolving the update statement will check for return/yield statement specifics.
+ ResolveStatement(s.hiddenUpdate, specContextOnly, codeContext);
+ }
+ } else {// this is a regular return/yield statement.
+ s.hiddenUpdate = null;
+ }
+ } else if (stmt is ConcreteUpdateStatement) {
+ ResolveUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext);
+ } else if (stmt is VarDeclStmt) {
+ var s = (VarDeclStmt)stmt;
+ foreach (var vd in s.Lhss) {
+ ResolveStatement(vd, specContextOnly, codeContext);
+ s.ResolvedStatements.Add(vd);
+ }
+ if (s.Update != null) {
+ ResolveStatement(s.Update, specContextOnly, codeContext);
+ s.ResolvedStatements.Add(s.Update);
+ }
+
+ } else if (stmt is AssignStmt) {
+ AssignStmt s = (AssignStmt)stmt;
+ int prevErrorCount = ErrorCount;
+ if (s.Lhs is SeqSelectExpr) {
+ ResolveSeqSelectExpr((SeqSelectExpr)s.Lhs, true, false); // allow ghosts for now, tighted up below
+ } else {
+ ResolveExpression(s.Lhs, true); // allow ghosts for now, tighted up below
+ }
+ bool lhsResolvedSuccessfully = ErrorCount == prevErrorCount;
+ Contract.Assert(s.Lhs.Type != null); // follows from postcondition of ResolveExpression
+ // check that LHS denotes a mutable variable or a field
+ bool lvalueIsGhost = false;
+ var lhs = s.Lhs.Resolved;
+ if (lhs is IdentifierExpr) {
+ IVariable var = ((IdentifierExpr)lhs).Var;
+ if (var == null) {
+ // the LHS didn't resolve correctly; some error would already have been reported
+ } else {
+ lvalueIsGhost = var.IsGhost || codeContext.IsGhost;
+ if (!var.IsMutable) {
+ Error(stmt, "LHS of assignment must denote a mutable variable or field");
+ }
+ if (!lvalueIsGhost && specContextOnly) {
+ Error(stmt, "Assignment to non-ghost variable 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 (lhs is FieldSelectExpr) {
+ var fse = (FieldSelectExpr)lhs;
+ if (fse.Field != null) { // otherwise, an error was reported above
+ lvalueIsGhost = fse.Field.IsGhost;
+ if (!lvalueIsGhost) {
+ if (specContextOnly) {
+ Error(stmt, "Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ } else {
+ // It is now that we wish we would have resolved s.Lhs to not allow ghosts. Too late, so we do
+ // the next best thing.
+ if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) {
+ Error(stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver");
+ }
+ }
+ }
+ if (!fse.Field.IsUserMutable) {
+ Error(stmt, "LHS of assignment does not denote a mutable field");
+ }
+ }
+ } else if (lhs is SeqSelectExpr) {
+ var slhs = (SeqSelectExpr)lhs;
+ // LHS is fine, provided the "sequence" is really an array
+ if (lhsResolvedSuccessfully) {
+ Contract.Assert(slhs.Seq.Type != null);
+ if (!UnifyTypes(slhs.Seq.Type, builtIns.ArrayType(1, new InferredTypeProxy()))) {
+ Error(slhs.Seq, "LHS of array assignment must denote an array element (found {0})", slhs.Seq.Type);
+ }
+ if (specContextOnly) {
+ Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ }
+ if (!slhs.SelectOne) {
+ Error(stmt, "cannot assign to a range of array elements (try the 'parallel' statement)");
+ }
+ }
+
+ } else if (lhs is MultiSelectExpr) {
+ if (specContextOnly) {
+ Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ }
+
+ } else {
+ Error(stmt, "LHS of assignment must denote a mutable variable or field");
+ }
+
+ s.IsGhost = lvalueIsGhost;
+ Type lhsType = s.Lhs.Type;
+ if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
+ Error(stmt, "cannot assign to a range of array elements (try the 'parallel' statement)");
+ //lhsType = UserDefinedType.ArrayElementType(lhsType);
+ } else {
+ if (s.Rhs is ExprRhs) {
+ ExprRhs rr = (ExprRhs)s.Rhs;
+ ResolveExpression(rr.Expr, true);
+ if (!lvalueIsGhost) {
+ CheckIsNonGhost(rr.Expr);
+ }
+ Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(lhsType, rr.Expr.Type)) {
+ Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType);
+ }
+ } else if (s.Rhs is TypeRhs) {
+ TypeRhs rr = (TypeRhs)s.Rhs;
+ Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, codeContext);
+ if (!lvalueIsGhost) {
+ if (rr.ArrayDimensions != null) {
+ foreach (var dim in rr.ArrayDimensions) {
+ CheckIsNonGhost(dim);
+ }
+ }
+ if (rr.InitCall != null) {
+ foreach (var arg in rr.InitCall.Args) {
+ CheckIsNonGhost(arg);
+ }
+ }
+ }
+ if (!UnifyTypes(lhsType, t)) {
+ Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType);
+ }
+ } else if (s.Rhs is HavocRhs) {
+ // nothing else to do
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS
+ }
+ }
+ } else if (stmt is VarDecl) {
+ VarDecl s = (VarDecl)stmt;
+ if (s.OptionalType != null) {
+ ResolveType(stmt.Tok, s.OptionalType, null, true);
+ s.type = s.OptionalType;
+ }
+ // now that the declaration has been processed, add the name to the scope
+ if (!scope.Push(s.Name, s)) {
+ Error(s, "Duplicate local-variable name: {0}", s.Name);
+ }
+ if (specContextOnly) {
+ // a local variable in a specification-only context might as well be ghost
+ s.IsGhost = true;
+ }
+
+ } else if (stmt is CallStmt) {
+ CallStmt s = (CallStmt)stmt;
+ ResolveCallStmt(s, specContextOnly, codeContext, null);
+
+ } else if (stmt is BlockStmt) {
+ scope.PushMarker();
+ ResolveBlockStatement((BlockStmt)stmt, specContextOnly, codeContext);
+ scope.PopMarker();
+
+ } else if (stmt is IfStmt) {
+ IfStmt s = (IfStmt)stmt;
+ bool branchesAreSpecOnly = specContextOnly;
+ if (s.Guard != null) {
+ int prevErrorCount = ErrorCount;
+ ResolveExpression(s.Guard, true);
+ Contract.Assert(s.Guard.Type != null); // follows from postcondition of ResolveExpression
+ bool successfullyResolved = ErrorCount == prevErrorCount;
+ if (!UnifyTypes(s.Guard.Type, Type.Bool)) {
+ Error(s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
+ }
+ if (!specContextOnly && successfullyResolved) {
+ branchesAreSpecOnly = UsesSpecFeatures(s.Guard);
+ }
+ }
+ s.IsGhost = branchesAreSpecOnly;
+ ResolveStatement(s.Thn, branchesAreSpecOnly, codeContext);
+ if (s.Els != null) {
+ ResolveStatement(s.Els, branchesAreSpecOnly, codeContext);
+ }
+
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, null, codeContext);
+
+ } else if (stmt is WhileStmt) {
+ WhileStmt s = (WhileStmt)stmt;
+ bool bodyMustBeSpecOnly = specContextOnly;
+ if (s.Guard != null) {
+ int prevErrorCount = ErrorCount;
+ ResolveExpression(s.Guard, true);
+ Contract.Assert(s.Guard.Type != null); // follows from postcondition of ResolveExpression
+ bool successfullyResolved = ErrorCount == prevErrorCount;
+ if (!UnifyTypes(s.Guard.Type, Type.Bool)) {
+ Error(s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
+ }
+ if (!specContextOnly && successfullyResolved) {
+ bodyMustBeSpecOnly = UsesSpecFeatures(s.Guard);
+ }
+ }
+
+ foreach (MaybeFreeExpression inv in s.Invariants) {
+ ResolveExpression(inv.E, true);
+ Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(inv.E.Type, Type.Bool)) {
+ Error(inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);
+ }
+ }
+
+ foreach (Expression e in s.Decreases.Expressions) {
+ ResolveExpression(e, true);
+ if (bodyMustBeSpecOnly && e is WildcardExpr) {
+ Error(e, "'decreases *' is not allowed on ghost loops");
+ }
+ // any type is fine
+ }
+
+ if (s.Mod.Expressions != null) {
+ foreach (FrameExpression fe in s.Mod.Expressions) {
+ ResolveFrameExpression(fe, "modifies");
+ }
+ }
+ s.IsGhost = bodyMustBeSpecOnly;
+ loopStack.Add(s); // push
+ if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map
+ inSpecOnlyContext.Add(s, specContextOnly);
+ }
+
+ ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);
+ loopStack.RemoveAt(loopStack.Count - 1); // pop
+
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, s, codeContext);
+ foreach (MaybeFreeExpression inv in s.Invariants) {
+ ResolveExpression(inv.E, true);
+ Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(inv.E.Type, Type.Bool)) {
+ Error(inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);
+ }
+ }
+
+ foreach (Expression e in s.Decreases.Expressions) {
+ ResolveExpression(e, true);
+ if (s.IsGhost && e is WildcardExpr) {
+ Error(e, "'decreases *' is not allowed on ghost loops");
+ }
+ // any type is fine
+ }
+
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+
+ int prevErrorCount = ErrorCount;
+ scope.PushMarker();
+ foreach (BoundVar v in s.BoundVars) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate bound-variable name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type, null, true);
+ }
+ ResolveExpression(s.Range, true);
+ Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(s.Range.Type, Type.Bool)) {
+ Error(stmt, "range restriction in parallel statement must be of type bool (instead got {0})", s.Range.Type);
+ }
+ foreach (var ens in s.Ens) {
+ ResolveExpression(ens.E, true);
+ Contract.Assert(ens.E.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(ens.E.Type, Type.Bool)) {
+ Error(ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type);
+ }
+ }
+ // Since the range and postconditions are more likely to infer the types of the bound variables, resolve them
+ // first (above) and only then resolve the attributes (below).
+ ResolveAttributes(s.Attributes, true);
+
+ bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == ErrorCount && UsesSpecFeatures(s.Range));
+ if (!bodyMustBeSpecOnly && prevErrorCount == ErrorCount) {
+ var missingBounds = new List<BoundVar>();
+ s.Bounds = DiscoverBounds(s.Tok, s.BoundVars, s.Range, true, false, missingBounds);
+ if (missingBounds.Count != 0) {
+ bodyMustBeSpecOnly = true;
+ }
+ }
+ s.IsGhost = bodyMustBeSpecOnly;
+
+ // clear the labels for the duration of checking the body, because break statements are not allowed to leave a parallel statement
+ var prevLblStmts = labeledStatements;
+ var prevLoopStack = loopStack;
+ labeledStatements = new Scope<Statement>();
+ loopStack = new List<Statement>();
+ ResolveStatement(s.Body, bodyMustBeSpecOnly, codeContext);
+ labeledStatements = prevLblStmts;
+ loopStack = prevLoopStack;
+ scope.PopMarker();
+
+ if (prevErrorCount == ErrorCount) {
+ // determine the Kind and run some additional checks on the body
+ if (s.Ens.Count != 0) {
+ // The only supported kind with ensures clauses is Proof.
+ s.Kind = ParallelStmt.ParBodyKind.Proof;
+ } else {
+ // There are two special cases:
+ // * Assign, which is the only kind of the parallel statement that allows a heap update.
+ // * Call, which is a single call statement with no side effects or output parameters.
+ // The effect of Assign and the postcondition of Call will be seen outside the parallel
+ // statement.
+ Statement s0 = s.S0;
+ if (s0 is AssignStmt) {
+ s.Kind = ParallelStmt.ParBodyKind.Assign;
+ } else if (s0 is CallStmt) {
+ s.Kind = ParallelStmt.ParBodyKind.Call;
+ } else {
+ s.Kind = ParallelStmt.ParBodyKind.Proof;
+ if (s.Body is BlockStmt && ((BlockStmt)s.Body).Body.Count == 0) {
+ // an empty statement, so don't produce any warning
+ } else {
+ Warning(s.Tok, "the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause");
+ }
+ }
+ }
+ CheckParallelBodyRestrictions(s.Body, s.Kind);
+ }
+
+ } else if (stmt is CalcStmt) {
+ var prevErrorCount = ErrorCount;
+ CalcStmt s = (CalcStmt)stmt;
+ s.IsGhost = true;
+ if (s.Lines.Count > 0) {
+ var resOp = s.Op;
+ var e0 = s.Lines.First();
+ ResolveExpression(e0, true);
+ Contract.Assert(e0.Type != null); // follows from postcondition of ResolveExpression
+ for (int i = 1; i < s.Lines.Count; i++) {
+ var e1 = s.Lines[i];
+ ResolveExpression(e1, true);
+ Contract.Assert(e1.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e0.Type, e1.Type)) {
+ Error(e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type);
+ } else {
+ BinaryExpr step;
+ var op = s.CustomOps[i - 1];
+ if (op == null) {
+ step = new BinaryExpr(e0.tok, s.Op, e0, e1); // Use calc-wide operator
+ } else {
+ step = new BinaryExpr(e0.tok, (BinaryExpr.Opcode)op, e0, e1); // Use custom line operator
+ Contract.Assert(CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op) != null); // This was checked during parsing
+ resOp = (BinaryExpr.Opcode)CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op);
+ }
+ ResolveExpression(step, true);
+ s.Steps.Add(step);
+ }
+ e0 = e1;
+ }
+ foreach (var h in s.Hints) {
+ ResolveStatement(h, true, codeContext);
+ }
+ if (prevErrorCount == ErrorCount && s.Steps.Count > 0) {
+ // do not build Result if there were errors, as it might be ill-typed and produce unnecessary resolution errors
+ s.Result = new BinaryExpr(s.Tok, resOp, s.Lines.First(), s.Lines.Last());
+ ResolveExpression(s.Result, true);
+ }
+ }
+ Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);
+ Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == 0 || s.Result != null);
+
+ } else if (stmt is MatchStmt) {
+ MatchStmt s = (MatchStmt)stmt;
+ bool bodyIsSpecOnly = specContextOnly;
+ int prevErrorCount = ErrorCount;
+ ResolveExpression(s.Source, true);
+ Contract.Assert(s.Source.Type != null); // follows from postcondition of ResolveExpression
+ bool successfullyResolved = ErrorCount == prevErrorCount;
+ if (!specContextOnly && successfullyResolved) {
+ bodyIsSpecOnly = UsesSpecFeatures(s.Source);
+ }
+ UserDefinedType sourceType = null;
+ DatatypeDecl dtd = null;
+ Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
+ if (s.Source.Type.IsDatatype) {
+ sourceType = (UserDefinedType)s.Source.Type;
+ dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
+ }
+ Dictionary<string, DatatypeCtor> ctors;
+ if (dtd == null) {
+ Error(s.Source, "the type of the match source expression must be a datatype (instead found {0})", s.Source.Type);
+ ctors = null;
+ } else {
+ Contract.Assert(sourceType != null); // dtd and sourceType are set together above
+ ctors = datatypeCtors[dtd];
+ Contract.Assert(ctors != null); // dtd should have been inserted into datatypeCtors during a previous resolution stage
+
+ // build the type-parameter substitution map for this use of the datatype
+ for (int i = 0; i < dtd.TypeArgs.Count; i++) {
+ subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
+ }
+ }
+ s.IsGhost = bodyIsSpecOnly;
+
+ Dictionary<string, object> memberNamesUsed = new Dictionary<string, object>(); // this is really a set
+ foreach (MatchCaseStmt mc in s.Cases) {
+ DatatypeCtor ctor = null;
+ if (ctors != null) {
+ Contract.Assert(dtd != null);
+ if (!ctors.TryGetValue(mc.Id, out ctor)) {
+ Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);
+ } else {
+ Contract.Assert(ctor != null); // follows from postcondition of TryGetValue
+ mc.Ctor = ctor;
+ if (ctor.Formals.Count != mc.Arguments.Count) {
+ Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count);
+ }
+ if (memberNamesUsed.ContainsKey(mc.Id)) {
+ Error(mc.tok, "member {0} appears in more than one case", mc.Id);
+ } else {
+ memberNamesUsed.Add(mc.Id, null); // add mc.Id to the set of names used
+ }
+ }
+ }
+ scope.PushMarker();
+ int i = 0;
+ foreach (BoundVar v in mc.Arguments) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate parameter name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type, null, true);
+ if (ctor != null && i < ctor.Formals.Count) {
+ Formal formal = ctor.Formals[i];
+ Type st = SubstType(formal.Type, subst);
+ if (!UnifyTypes(v.Type, st)) {
+ Error(stmt, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
+ }
+ v.IsGhost = formal.IsGhost;
+ }
+ i++;
+ }
+ foreach (Statement ss in mc.Body) {
+ ResolveStatement(ss, bodyIsSpecOnly, codeContext);
+ }
+ scope.PopMarker();
+ }
+ if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {
+ // We could complain about the syntactic omission of constructors:
+ // Error(stmt, "match statement does not cover all constructors");
+ // but instead we let the verifier do a semantic check.
+ // So, for now, record the missing constructors:
+ foreach (var ctr in dtd.Ctors) {
+ if (!memberNamesUsed.ContainsKey(ctr.Name)) {
+ s.MissingCases.Add(ctr);
+ }
+ }
+ Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);
+ }
+
+
+ } else if (stmt is SkeletonStatement) {
+ var s = (SkeletonStatement)stmt;
+ Error(s.Tok, "skeleton statements are allowed only in refining methods");
+ // nevertheless, resolve the underlying statement; hey, why not
+ if (s.S != null) {
+ ResolveStatement(s.S, specContextOnly, codeContext);
+ }
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException();
+ }
+ }
+ private void ResolveUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, ICodeContext codeContext) {
+ Contract.Requires(codeContext != null);
+
+ int prevErrorCount = ErrorCount;
+ // First, resolve all LHS's and expression-looking RHS's.
+ SeqSelectExpr arrayRangeLhs = null;
+ var update = s as UpdateStmt;
+
+ foreach (var lhs in s.Lhss) {
+ var ec = ErrorCount;
+ if (lhs is SeqSelectExpr) {
+ var sse = (SeqSelectExpr)lhs;
+ ResolveSeqSelectExpr(sse, true, true);
+ if (arrayRangeLhs == null && !sse.SelectOne) {
+ arrayRangeLhs = sse;
+ }
+ } else {
+ ResolveExpression(lhs, true);
+ }
+ if (update == null && ec == ErrorCount && specContextOnly && !AssignStmt.LhsIsToGhost(lhs)) {
+ Error(lhs, "cannot assign to non-ghost variable in a ghost context");
+ }
+ }
+ IToken firstEffectfulRhs = null;
+ CallRhs callRhs = null;
+ // Resolve RHSs
+ if (update == null) {
+ var suchThat = (AssignSuchThatStmt)s; // this is the other possible subclass
+ ResolveExpression(suchThat.Expr, true);
+ if (suchThat.AssumeToken == null) {
+ // to ease in the verification, only allow local variables as LHSs
+ var lhsNames = new Dictionary<string, object>();
+ foreach (var lhs in s.Lhss) {
+ if (!(lhs.Resolved is IdentifierExpr)) {
+ Error(lhs, "the assign-such-that statement currently only supports local-variable LHSs");
+ } else {
+ var ie = (IdentifierExpr)lhs.Resolved;
+ if (lhsNames.ContainsKey(ie.Name)) {
+ // disallow same LHS.
+ Error(s, "duplicate variable in left-hand side of assign-such-that statement: {0}", ie.Name);
+ } else {
+ lhsNames.Add(ie.Name, null);
+ }
+ }
+ }
+ }
+ } else {
+ foreach (var rhs in update.Rhss) {
+ bool isEffectful;
+ if (rhs is TypeRhs) {
+ var tr = (TypeRhs)rhs;
+ ResolveTypeRhs(tr, s, specContextOnly, codeContext);
+ isEffectful = tr.InitCall != null;
+ } else if (rhs is HavocRhs) {
+ isEffectful = false;
+ } else {
+ var er = (ExprRhs)rhs;
+ if (er.Expr is IdentifierSequence) {
+ var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true);
+ isEffectful = cRhs != null;
+ callRhs = callRhs ?? cRhs;
+ } else if (er.Expr is FunctionCallExpr) {
+ var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true);
+ isEffectful = cRhs != null;
+ callRhs = callRhs ?? cRhs;
+ } else {
+ ResolveExpression(er.Expr, true);
+ isEffectful = false;
+ }
+ }
+ if (isEffectful && firstEffectfulRhs == null) {
+ firstEffectfulRhs = rhs.Tok;
+ }
+ }
+ }
+ // check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)
+ var lhsNameSet = new Dictionary<string, object>();
+ foreach (var lhs in s.Lhss) {
+ var ie = lhs.Resolved as IdentifierExpr;
+ if (ie != null) {
+ if (lhsNameSet.ContainsKey(ie.Name)) {
+ if (callRhs != null)
+ // only allow same LHS in a multiassignment, not a call statement
+ Error(s, "duplicate variable in left-hand side of call statement: {0}", ie.Name);
+ } else {
+ lhsNameSet.Add(ie.Name, null);
+ }
+ }
+ }
+ if (update != null) {
+ // figure out what kind of UpdateStmt this is
+ if (firstEffectfulRhs == null) {
+ if (s.Lhss.Count == 0) {
+ Contract.Assert(update.Rhss.Count == 1); // guaranteed by the parser
+ Error(s, "expected method call, found expression");
+ } else if (s.Lhss.Count != update.Rhss.Count) {
+ Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count);
+ } else if (arrayRangeLhs != null && s.Lhss.Count != 1) {
+ Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment");
+ } else if (ErrorCount == prevErrorCount) {
+ // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)
+ for (int i = 0; i < s.Lhss.Count; i++) {
+ var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, update.Rhss[i]);
+ s.ResolvedStatements.Add(a);
+ }
+ }
+
+ } else if (update.CanMutateKnownState) {
+ if (1 < update.Rhss.Count) {
+ Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");
+ } else { // it might be ok, if it is a TypeRhs
+ Contract.Assert(update.Rhss.Count == 1);
+ if (callRhs != null) {
+ Error(callRhs.Tok, "cannot have method call in return statement.");
+ } else {
+ // we have a TypeRhs
+ Contract.Assert(update.Rhss[0] is TypeRhs);
+ var tr = (TypeRhs)update.Rhss[0];
+ Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.
+ if (tr.CanAffectPreviouslyKnownExpressions) {
+ Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");
+ }
+ var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, tr);
+ s.ResolvedStatements.Add(a);
+ }
+ }
+
+ } else {
+ // if there was an effectful RHS, that must be the only RHS
+ if (update.Rhss.Count != 1) {
+ Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");
+ } else if (arrayRangeLhs != null) {
+ Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");
+ } else if (callRhs == null) {
+ // must be a single TypeRhs
+ if (s.Lhss.Count != 1) {
+ Contract.Assert(2 <= s.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
+ Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count);
+ } else if (ErrorCount == prevErrorCount) {
+ var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, update.Rhss[0]);
+ s.ResolvedStatements.Add(a);
+ }
+ } else {
+ // a call statement
+ if (ErrorCount == prevErrorCount) {
+ var resolvedLhss = new List<Expression>();
+ foreach (var ll in s.Lhss) {
+ resolvedLhss.Add(ll.Resolved);
+ }
+ var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);
+ s.ResolvedStatements.Add(a);
+ }
+ }
+ }
+ }
+
+ foreach (var a in s.ResolvedStatements) {
+ ResolveStatement(a, specContextOnly, codeContext);
+ }
+ s.IsGhost = s.ResolvedStatements.TrueForAll(ss => ss.IsGhost);
+ }
+
+ bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, ICodeContext codeContext) {
+ Contract.Requires(alternatives != null);
+ Contract.Requires(codeContext != null);
+
+ bool isGhost = specContextOnly;
+ // first, resolve the guards, which tells us whether or not the entire statement is a ghost statement
+ foreach (var alternative in alternatives) {
+ int prevErrorCount = ErrorCount;
+ ResolveExpression(alternative.Guard, true);
+ Contract.Assert(alternative.Guard.Type != null); // follows from postcondition of ResolveExpression
+ bool successfullyResolved = ErrorCount == prevErrorCount;
+ if (!UnifyTypes(alternative.Guard.Type, Type.Bool)) {
+ Error(alternative.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, alternative.Guard.Type);
+ }
+ if (!specContextOnly && successfullyResolved) {
+ isGhost = isGhost || UsesSpecFeatures(alternative.Guard);
+ }
+ }
+
+ if (loopToCatchBreaks != null) {
+ loopStack.Add(loopToCatchBreaks); // push
+ if (loopToCatchBreaks.Labels == null) { // otherwise, "loopToCatchBreak" is already in "inSpecOnlyContext" map
+ inSpecOnlyContext.Add(loopToCatchBreaks, specContextOnly);
+ }
+ }
+ foreach (var alternative in alternatives) {
+ scope.PushMarker();
+ foreach (Statement ss in alternative.Body) {
+ ResolveStatement(ss, isGhost, codeContext);
+ }
+ scope.PopMarker();
+ }
+ if (loopToCatchBreaks != null) {
+ loopStack.RemoveAt(loopStack.Count - 1); // pop
+ }
+
+ return isGhost;
+ }
+
+ /// <summary>
+ /// Resolves the given call statement.
+ /// Assumes all LHSs have already been resolved (and checked for mutability).
+ /// </summary>
+ void ResolveCallStmt(CallStmt s, bool specContextOnly, ICodeContext codeContext, Type receiverType) {
+ Contract.Requires(s != null);
+ Contract.Requires(codeContext != null);
+ bool isInitCall = receiverType != null;
+
+ // resolve receiver
+ ResolveReceiver(s.Receiver, true);
+ Contract.Assert(s.Receiver.Type != null); // follows from postcondition of ResolveExpression
+ if (receiverType == null) {
+ receiverType = s.Receiver.Type;
+ }
+ // resolve the method name
+ NonProxyType nptype;
+ MemberDecl member = ResolveMember(s.Tok, receiverType, s.MethodName, out nptype);
+ Method callee = null;
+ if (member == null) {
+ // error has already been reported by ResolveMember
+ } else if (member is Method) {
+ s.Method = (Method)member;
+ callee = s.Method;
+ if (!isInitCall && callee is Constructor) {
+ Error(s, "a constructor is only allowed to be called when an object is being allocated");
+ }
+ s.IsGhost = callee.IsGhost;
+ if (specContextOnly && !callee.IsGhost) {
+ Error(s, "only ghost methods can be called from this context");
+ }
+ } else {
+ Error(s, "member {0} in type {1} does not refer to a method", s.MethodName, nptype);
+ }
+
+ // resolve left-hand sides
+ foreach (var lhs in s.Lhs) {
+ Contract.Assume(lhs.Type != null); // a sanity check that LHSs have already been resolved
+ }
+ // resolve arguments
+ if (!s.IsGhost && s.Receiver.WasResolved()) {
+ CheckIsNonGhost(s.Receiver);
+ }
+ int j = 0;
+ foreach (Expression e in s.Args) {
+ bool allowGhost = s.IsGhost || callee == null || callee.Ins.Count <= j || callee.Ins[j].IsGhost;
+ ResolveExpression(e, true);
+ if (!allowGhost) {
+ CheckIsNonGhost(e);
+ }
+ j++;
+ }
+
+ if (callee == null) {
+ // error has been reported above
+ } else if (callee.Ins.Count != s.Args.Count) {
+ Error(s, "wrong number of method arguments (got {0}, expected {1})", s.Args.Count, callee.Ins.Count);
+ } else if (callee.Outs.Count != s.Lhs.Count) {
+ if (isInitCall) {
+ Error(s, "a method called as an initialization method must not have any result arguments");
+ } else {
+ Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, callee.Outs.Count);
+ }
+ } else {
+ Contract.Assert(nptype != null); // follows from postcondition of ResolveMember above
+ if (isInitCall) {
+ if (callee.IsStatic) {
+ Error(s.Tok, "a method called as an initialization method must not be 'static'");
+ }
+ } else if (!callee.IsStatic) {
+ if (!scope.AllowInstance && s.Receiver is ThisExpr) {
+ // The call really needs an instance, but that instance is given as 'this', which is not
+ // available in this context. For more details, see comment in the resolution of a
+ // FunctionCallExpr.
+ Error(s.Receiver, "'this' is not allowed in a 'static' context");
+ } else if (s.Receiver is StaticReceiverExpr) {
+ Error(s.Receiver, "call to instance method requires an instance");
+ }
+ }
+#if !NO_WORK_TO_BE_DONE
+ UserDefinedType ctype = (UserDefinedType)nptype; // TODO: get rid of this statement, make this code handle any non-proxy type
+#endif
+ // build the type substitution map
+ s.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
+ for (int i = 0; i < ctype.TypeArgs.Count; i++) {
+ s.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
+ }
+ foreach (TypeParameter p in callee.TypeArgs) {
+ s.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));
+ }
+ // type check the arguments
+ for (int i = 0; i < callee.Ins.Count; i++) {
+ Type st = SubstType(callee.Ins[i].Type, s.TypeArgumentSubstitutions);
+ if (!UnifyTypes(cce.NonNull(s.Args[i].Type), st)) {
+ Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
+ }
+ }
+ for (int i = 0; i < callee.Outs.Count; i++) {
+ Type st = SubstType(callee.Outs[i].Type, s.TypeArgumentSubstitutions);
+ var lhs = s.Lhs[i];
+ if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {
+ Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);
+ } else {
+ var resolvedLhs = lhs.Resolved;
+ if (!specContextOnly && (s.IsGhost || callee.Outs[i].IsGhost)) {
+ // LHS must denote a ghost
+ if (resolvedLhs is IdentifierExpr) {
+ var ll = (IdentifierExpr)resolvedLhs;
+ if (!ll.Var.IsGhost) {
+ if (ll is AutoGhostIdentifierExpr && ll.Var is VarDecl) {
+ // the variable was actually declared in this statement, so auto-declare it as ghost
+ ((VarDecl)ll.Var).MakeGhost();
+ } else {
+ Error(s, "actual out-parameter {0} is required to be a ghost variable", i);
+ }
+ }
+ } else if (resolvedLhs is FieldSelectExpr) {
+ var ll = (FieldSelectExpr)resolvedLhs;
+ if (!ll.Field.IsGhost) {
+ Error(s, "actual out-parameter {0} is required to be a ghost field", i);
+ }
+ } else {
+ // this is an array update, and arrays are always non-ghost
+ Error(s, "actual out-parameter {0} is required to be a ghost variable", i);
+ }
+ }
+ // LHS must denote a mutable field.
+ if (resolvedLhs is IdentifierExpr) {
+ var ll = (IdentifierExpr)resolvedLhs;
+ if (!ll.Var.IsMutable) {
+ Error(resolvedLhs, "LHS of assignment must denote a mutable variable");
+ }
+ } else if (resolvedLhs is FieldSelectExpr) {
+ var ll = (FieldSelectExpr)resolvedLhs;
+ if (!ll.Field.IsUserMutable) {
+ Error(resolvedLhs, "LHS of assignment must denote a mutable field");
+ }
+ }
+ }
+ }
+
+ // Resolution termination check
+ ModuleDefinition callerModule = codeContext.EnclosingModule;
+ ModuleDefinition calleeModule = ((ICodeContext)callee).EnclosingModule;
+ if (callerModule == calleeModule) {
+ // intra-module call; this is allowed; add edge in module's call graph
+ var caller = codeContext is Method ? (Method)codeContext : ((IteratorDecl)codeContext).Member_MoveNext;
+ callerModule.CallGraph.AddEdge(caller, callee);
+ } else {
+ //Contract.Assert(dependencies.Reaches(callerModule, calleeModule));
+ //
+ }
+ }
+ }
+
+ void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, ICodeContext codeContext) {
+ Contract.Requires(blockStmt != null);
+ Contract.Requires(codeContext != null);
+
+ foreach (Statement ss in blockStmt.Body) {
+ labeledStatements.PushMarker();
+ // push labels
+ for (var l = ss.Labels; l != null; l = l.Next) {
+ var lnode = l.Data;
+ Contract.Assert(lnode.Name != null); // LabelNode's with .Label==null are added only during resolution of the break statements with 'stmt' as their target, which hasn't happened yet
+ var prev = labeledStatements.Find(lnode.Name);
+ if (prev == ss) {
+ Error(lnode.Tok, "duplicate label");
+ } else if (prev != null) {
+ Error(lnode.Tok, "label shadows an enclosing label");
+ } else {
+ bool b = labeledStatements.Push(lnode.Name, ss);
+ Contract.Assert(b); // since we just checked for duplicates, we expect the Push to succeed
+ if (l == ss.Labels) { // add it only once
+ inSpecOnlyContext.Add(ss, specContextOnly);
+ }
+ }
+ }
+ ResolveStatement(ss, specContextOnly, codeContext);
+ labeledStatements.PopMarker();
+ }
+ }
+
+ /// <summary>
+ /// This method performs some additional checks on the body "stmt" of a parallel statement of kind "kind".
+ /// </summary>
+ public void CheckParallelBodyRestrictions(Statement stmt, ParallelStmt.ParBodyKind kind) {
+ Contract.Requires(stmt != null);
+ if (stmt is PredicateStmt) {
+ // cool
+ } else if (stmt is PrintStmt) {
+ Error(stmt, "print statement is not allowed inside a parallel statement");
+ } else if (stmt is BreakStmt) {
+ // this case is checked already in the first pass through the parallel body, by doing so from an empty set of labeled statements and resetting the loop-stack
+ } else if (stmt is ReturnStmt) {
+ Error(stmt, "return statement is not allowed inside a parallel statement");
+ } else if (stmt is YieldStmt) {
+ Error(stmt, "yield statement is not allowed inside a parallel statement");
+ } else if (stmt is AssignSuchThatStmt) {
+ var s = (AssignSuchThatStmt)stmt;
+ foreach (var lhs in s.Lhss) {
+ CheckParallelBodyLhs(s.Tok, lhs.Resolved, kind);
+ }
+ } else if (stmt is ConcreteSyntaxStatement) {
+ var s = (ConcreteSyntaxStatement)stmt;
+ foreach (var ss in s.ResolvedStatements) {
+ CheckParallelBodyRestrictions(ss, kind);
+ }
+ } else if (stmt is AssignStmt) {
+ var s = (AssignStmt)stmt;
+ CheckParallelBodyLhs(s.Tok, s.Lhs.Resolved, kind);
+ var rhs = s.Rhs; // ExprRhs and HavocRhs are fine, but TypeRhs is not
+ if (rhs is TypeRhs) {
+ if (kind == ParallelStmt.ParBodyKind.Assign) {
+ Error(rhs.Tok, "new allocation not supported in parallel statements");
+ } else {
+ var t = (TypeRhs)rhs;
+ if (t.InitCall != null) {
+ CheckParallelBodyRestrictions(t.InitCall, kind);
+ }
+ }
+ } else if (rhs is ExprRhs) {
+ var r = ((ExprRhs)rhs).Expr.Resolved;
+ if (kind == ParallelStmt.ParBodyKind.Assign && r is UnaryExpr && ((UnaryExpr)r).Op == UnaryExpr.Opcode.SetChoose) {
+ Error(r, "set choose operator not supported inside the enclosing parallel statement");
+ }
+ }
+ } else if (stmt is VarDecl) {
+ // cool
+ } else if (stmt is CallStmt) {
+ var s = (CallStmt)stmt;
+ foreach (var lhs in s.Lhs) {
+ var idExpr = lhs as IdentifierExpr;
+ if (idExpr != null) {
+ if (scope.ContainsDecl(idExpr.Var)) {
+ Error(stmt, "body of parallel statement is attempting to update a variable declared outside the parallel statement");
+ }
+ } else {
+ Error(stmt, "the body of the enclosing parallel statement is not allowed to update heap locations");
+ }
+ }
+ if (!s.Method.IsGhost) {
+ // The reason for this restriction is that the compiler is going to omit the parallel statement altogether--it has
+ // no effect. However, print effects are not documented, so to make sure that the compiler does not omit a call to
+ // a method that prints something, all calls to non-ghost methods are disallowed. (Note, if this restriction
+ // is somehow lifted in the future, then it is still necessary to enforce s.Method.Mod.Expressions.Count != 0 for
+ // calls to non-ghost methods.)
+ Error(s, "the body of the enclosing parallel statement is not allowed to call non-ghost methods");
+ }
+
+ } else if (stmt is BlockStmt) {
+ var s = (BlockStmt)stmt;
+ scope.PushMarker();
+ foreach (var ss in s.Body) {
+ CheckParallelBodyRestrictions(ss, kind);
+ }
+ scope.PopMarker();
+
+ } else if (stmt is IfStmt) {
+ var s = (IfStmt)stmt;
+ CheckParallelBodyRestrictions(s.Thn, kind);
+ if (s.Els != null) {
+ CheckParallelBodyRestrictions(s.Els, kind);
+ }
+
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ foreach (var alt in s.Alternatives) {
+ foreach (var ss in alt.Body) {
+ CheckParallelBodyRestrictions(ss, kind);
+ }
+ }
+
+ } else if (stmt is WhileStmt) {
+ WhileStmt s = (WhileStmt)stmt;
+ CheckParallelBodyRestrictions(s.Body, kind);
+
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ foreach (var alt in s.Alternatives) {
+ foreach (var ss in alt.Body) {
+ CheckParallelBodyRestrictions(ss, kind);
+ }
+ }
+
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+ switch (s.Kind) {
+ case ParallelStmt.ParBodyKind.Assign:
+ Error(stmt, "a parallel statement with heap updates is not allowed inside the body of another parallel statement");
+ break;
+ case ParallelStmt.ParBodyKind.Call:
+ case ParallelStmt.ParBodyKind.Proof:
+ // these are fine, since they don't update any non-local state
+ break;
+ default:
+ Contract.Assert(false); // unexpected kind
+ break;
+ }
+
+ } else if (stmt is CalcStmt) {
+ // cool
+ // NadiaTodo: ...I assume because it's always ghost
+
+ } else if (stmt is MatchStmt) {
+ var s = (MatchStmt)stmt;
+ foreach (var kase in s.Cases) {
+ foreach (var ss in kase.Body) {
+ CheckParallelBodyRestrictions(ss, kind);
+ }
+ }
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException();
+ }
+ }
+
+ void CheckParallelBodyLhs(IToken tok, Expression lhs, ParallelStmt.ParBodyKind kind) {
+ var idExpr = lhs as IdentifierExpr;
+ if (idExpr != null) {
+ if (scope.ContainsDecl(idExpr.Var)) {
+ Error(tok, "body of parallel statement is attempting to update a variable declared outside the parallel statement");
+ }
+ } else if (kind != ParallelStmt.ParBodyKind.Assign) {
+ Error(tok, "the body of the enclosing parallel statement is not allowed to update heap locations");
+ }
+ }
+
+ Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, ICodeContext codeContext) {
+ Contract.Requires(rr != null);
+ Contract.Requires(stmt != null);
+ Contract.Requires(codeContext != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ if (rr.Type == null) {
+ ResolveType(stmt.Tok, rr.EType, null, true);
+ if (rr.ArrayDimensions == null) {
+ if (!rr.EType.IsRefType) {
+ Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);
+ } else {
+ bool callsConstructor = false;
+ if (rr.InitCall != null) {
+ ResolveCallStmt(rr.InitCall, specContextOnly, codeContext, rr.EType);
+ if (rr.InitCall.Method is Constructor) {
+ callsConstructor = true;
+ }
+ }
+ if (!callsConstructor && rr.EType is UserDefinedType) {
+ var udt = (UserDefinedType)rr.EType;
+ var cl = (ClassDecl)udt.ResolvedClass; // cast is guaranteed by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test
+ if (cl.HasConstructor) {
+ Error(stmt, "when allocating an object of type '{0}', one of its constructor methods must be called", cl.Name);
+ }
+ }
+ }
+ rr.Type = rr.EType;
+ } else {
+ int i = 0;
+ if (rr.EType.IsSubrangeType) {
+ Error(stmt, "sorry, cannot instantiate 'array' type with a subrange type");
+ }
+ foreach (Expression dim in rr.ArrayDimensions) {
+ Contract.Assert(dim != null);
+ ResolveExpression(dim, true);
+ if (!UnifyTypes(dim.Type, Type.Int)) {
+ Error(stmt, "new must use an integer expression for the array size (got {0} for index {1})", dim.Type, i);
+ }
+ i++;
+ }
+ rr.Type = builtIns.ArrayType(rr.ArrayDimensions.Count, rr.EType);
+ }
+ }
+ return rr.Type;
+ }
+
+ MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName, out NonProxyType nptype) {
+ Contract.Requires(tok != null);
+ Contract.Requires(receiverType != null);
+ Contract.Requires(memberName != null);
+ Contract.Ensures(Contract.Result<MemberDecl>() == null || Contract.ValueAtReturn(out nptype) != null);
+
+ nptype = null; // prepare for the worst
+ receiverType = receiverType.Normalize();
+ if (receiverType is TypeProxy) {
+ Error(tok, "type of the receiver is not fully determined at this program point", receiverType);
+ return null;
+ }
+ Contract.Assert(receiverType is NonProxyType); // there are only two kinds of types: proxies and non-proxies
+
+ UserDefinedType ctype = UserDefinedType.DenotesClass(receiverType);
+ if (ctype != null) {
+ var cd = (ClassDecl)ctype.ResolvedClass; // correctness of cast follows from postcondition of DenotesClass
+ Contract.Assert(ctype.TypeArgs.Count == cd.TypeArgs.Count); // follows from the fact that ctype was resolved
+ MemberDecl member;
+ if (!classMembers[cd].TryGetValue(memberName, out member)) {
+ Error(tok, "member {0} does not exist in {2} {1}", memberName, ctype.Name, cd is IteratorDecl ? "iterator" : "class");
+ return null;
+ } else {
+ nptype = ctype;
+ return member;
+ }
+ }
+
+ DatatypeDecl dtd = receiverType.AsDatatype;
+ if (dtd != null) {
+ MemberDecl member;
+ if (!datatypeMembers[dtd].TryGetValue(memberName, out member)) {
+ Error(tok, "member {0} does not exist in datatype {1}", memberName, dtd.Name);
+ return null;
+ } else {
+ nptype = (UserDefinedType)receiverType;
+ return member;
+ }
+ }
+
+ Error(tok, "type {0} does not have a member {1}", receiverType, memberName);
+ return null;
+ }
+
+ public static Type SubstType(Type type, Dictionary<TypeParameter/*!*/, Type/*!*/>/*!*/ subst) {
+ Contract.Requires(type != null);
+ Contract.Requires(cce.NonNullDictionaryAndValues(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ if (type is BasicType) {
+ return type;
+ } else if (type is MapType) {
+ MapType t = (MapType)type;
+ return new MapType(SubstType(t.Domain, subst), SubstType(t.Range, subst));
+ } else if (type is CollectionType) {
+ CollectionType t = (CollectionType)type;
+ Type arg = SubstType(t.Arg, subst);
+ if (arg == t.Arg) {
+ return type;
+ } else if (type is SetType) {
+ return new SetType(arg);
+ } else if (type is MultiSetType) {
+ return new MultiSetType(arg);
+ } else if (type is SeqType) {
+ return new SeqType(arg);
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected collection type
+ }
+ } else if (type is UserDefinedType) {
+ UserDefinedType t = (UserDefinedType)type;
+ if (t.ResolvedParam != null) {
+ Contract.Assert(t.TypeArgs.Count == 0);
+ Type s;
+ if (subst.TryGetValue(t.ResolvedParam, out s)) {
+ return cce.NonNull(s);
+ } else {
+ return type;
+ }
+ } else if (t.ResolvedClass != null) {
+ List<Type> newArgs = null; // allocate it lazily
+ for (int i = 0; i < t.TypeArgs.Count; i++) {
+ Type p = t.TypeArgs[i];
+ Type s = SubstType(p, subst);
+ if (s != p && newArgs == null) {
+ // lazily construct newArgs
+ newArgs = new List<Type>();
+ for (int j = 0; j < i; j++) {
+ newArgs.Add(t.TypeArgs[j]);
+ }
+ }
+ if (newArgs != null) {
+ newArgs.Add(s);
+ }
+ }
+ if (newArgs == null) {
+ // there were no substitutions
+ return type;
+ } else {
+ return new UserDefinedType(t.tok, t.Name, t.ResolvedClass, newArgs);
+ }
+ } else {
+ // there's neither a resolved param nor a resolved class, which means the UserDefinedType wasn't
+ // properly resolved; just return it
+ return type;
+ }
+ } else if (type is TypeProxy) {
+ TypeProxy t = (TypeProxy)type;
+ if (t.T == null) {
+ return type;
+ } else {
+ // bypass the proxy
+ return SubstType(t.T, subst);
+ }
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
+ }
+ }
+
+ public static UserDefinedType GetThisType(IToken tok, ClassDecl cl) {
+ Contract.Requires(tok != null);
+ Contract.Requires(cl != null);
+ Contract.Ensures(Contract.Result<UserDefinedType>() != null);
+
+ List<Type> args = new List<Type>();
+ foreach (TypeParameter tp in cl.TypeArgs) {
+ args.Add(new UserDefinedType(tok, tp.Name, tp));
+ }
+ return new UserDefinedType(tok, cl.Name, cl, args);
+ }
+
+ /// <summary>
+ /// Requires "member" to be declared in a class.
+ /// </summary>
+ public static UserDefinedType GetReceiverType(IToken tok, MemberDecl member) {
+ Contract.Requires(tok != null);
+ Contract.Requires(member != null);
+ Contract.Ensures(Contract.Result<UserDefinedType>() != null);
+
+ return GetThisType(tok, (ClassDecl)member.EnclosingClass);
+ }
+
+ /// <summary>
+ /// "twoState" implies that "old" and "fresh" expressions are allowed.
+ /// </summary>
+ void ResolveExpression(Expression expr, bool twoState) {
+ ResolveExpression(expr, twoState, null);
+ }
+
+ /// <summary>
+ /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression;
+ /// if null, no "match" expression will be allowed.
+ /// </summary>
+ void ResolveExpression(Expression expr, bool twoState, List<IVariable> matchVarContext) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(expr.Type != null);
+ if (expr.Type != null) {
+ // expression has already been resovled
+ return;
+ }
+
+ // The following cases will resolve the subexpressions and will attempt to assign a type of expr. However, if errors occur
+ // and it cannot be determined what the type of expr is, then it is fine to leave expr.Type as null. In that case, the end
+ // of this method will assign proxy type to the expression, which reduces the number of error messages that are produced
+ // while type checking the rest of the program.
+
+ if (expr is ParensExpression) {
+ var e = (ParensExpression)expr;
+ ResolveExpression(e.E, twoState, matchVarContext); // allow "match" expressions inside e.E if the parenthetic expression had been allowed to be a "match" expression
+ e.ResolvedExpression = e.E;
+ e.Type = e.E.Type;
+
+ } else if (expr is ChainingExpression) {
+ var e = (ChainingExpression)expr;
+ ResolveExpression(e.E, twoState);
+ e.ResolvedExpression = e.E;
+ e.Type = e.E.Type;
+
+ } else if (expr is IdentifierSequence) {
+ var e = (IdentifierSequence)expr;
+ ResolveIdentifierSequence(e, twoState, false);
+
+ } else if (expr is LiteralExpr) {
+ LiteralExpr e = (LiteralExpr)expr;
+ if (e.Value == null) {
+ e.Type = new ObjectTypeProxy();
+ } else if (e.Value is BigInteger) {
+ e.Type = Type.Int;
+ } else if (e.Value is bool) {
+ e.Type = Type.Bool;
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal type
+ }
+
+ } else if (expr is ThisExpr) {
+ if (!scope.AllowInstance) {
+ Error(expr, "'this' is not allowed in a 'static' context");
+ }
+ if (currentClass != null) {
+ expr.Type = GetThisType(expr.tok, currentClass); // do this regardless of scope.AllowInstance, for better error reporting
+ }
+
+ } else if (expr is IdentifierExpr) {
+ IdentifierExpr e = (IdentifierExpr)expr;
+ e.Var = scope.Find(e.Name);
+ if (e.Var == null) {
+ Error(expr, "Identifier does not denote a local variable, parameter, or bound variable: {0}", e.Name);
+ } else {
+ expr.Type = e.Var.Type;
+ }
+
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ TopLevelDecl d;
+ if (!moduleInfo.TopLevels.TryGetValue(dtv.DatatypeName, out d)) {
+ Error(expr.tok, "Undeclared datatype: {0}", dtv.DatatypeName);
+ } else if (d is AmbiguousTopLevelDecl) {
+ Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", dtv.DatatypeName, ((AmbiguousTopLevelDecl)d).ModuleNames());
+ } else if (!(d is DatatypeDecl)) {
+ Error(expr.tok, "Expected datatype: {0}", dtv.DatatypeName);
+ } else {
+ ResolveDatatypeValue(twoState, dtv, (DatatypeDecl)d);
+ }
+
+ } else if (expr is DisplayExpression) {
+ DisplayExpression e = (DisplayExpression)expr;
+ Type elementType = new InferredTypeProxy();
+ foreach (Expression ee in e.Elements) {
+ ResolveExpression(ee, twoState);
+ Contract.Assert(ee.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(elementType, ee.Type)) {
+ Error(ee, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", ee.Type, elementType);
+ }
+ }
+ if (expr is SetDisplayExpr) {
+ expr.Type = new SetType(elementType);
+ } else if (expr is MultiSetDisplayExpr) {
+ expr.Type = new MultiSetType(elementType);
+ } else {
+ expr.Type = new SeqType(elementType);
+ }
+ } else if (expr is MapDisplayExpr) {
+ MapDisplayExpr e = (MapDisplayExpr)expr;
+ Type domainType = new InferredTypeProxy();
+ Type rangeType = new InferredTypeProxy();
+ foreach (ExpressionPair p in e.Elements) {
+ ResolveExpression(p.A, twoState);
+ Contract.Assert(p.A.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(domainType, p.A.Type)) {
+ Error(p.A, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.A.Type, domainType);
+ }
+ ResolveExpression(p.B, twoState);
+ Contract.Assert(p.B.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(rangeType, p.B.Type)) {
+ Error(p.B, "All elements of display must be of the same type (got {0}, but type of previous elements is {1})", p.B.Type, rangeType);
+ }
+ }
+ expr.Type = new MapType(domainType, rangeType);
+ } else if (expr is ExprDotName) {
+ var e = (ExprDotName)expr;
+ // The following call to ResolveExpression is just preliminary. If it succeeds, it is redone below on the resolved expression. Thus,
+ // it's okay to be more lenient here and use coLevel (instead of trying to use CoLevel_Dec(coLevel), which is needed when .Name denotes a
+ // destructor for a co-datatype).
+ ResolveExpression(e.Obj, twoState);
+ Contract.Assert(e.Obj.Type != null); // follows from postcondition of ResolveExpression
+ Expression resolved = ResolvePredicateOrField(expr.tok, e.Obj, e.SuffixName);
+ if (resolved == null) {
+ // error has already been reported by ResolvePredicateOrField
+ } else {
+ // the following will cause e.Obj to be resolved again, but that's still correct
+ e.ResolvedExpression = resolved;
+ ResolveExpression(e.ResolvedExpression, twoState);
+ e.Type = e.ResolvedExpression.Type;
+ }
+
+ } else if (expr is FieldSelectExpr) {
+ var e = (FieldSelectExpr)expr;
+ ResolveExpression(e.Obj, twoState);
+ Contract.Assert(e.Obj.Type != null); // follows from postcondition of ResolveExpression
+ NonProxyType nptype;
+ MemberDecl member = ResolveMember(expr.tok, e.Obj.Type, e.FieldName, out nptype);
+#if !NO_WORK_TO_BE_DONE
+ UserDefinedType ctype = (UserDefinedType)nptype;
+#endif
+ if (member == null) {
+ // error has already been reported by ResolveMember
+ } else if (!(member is Field)) {
+ Error(expr, "member {0} in type {1} does not refer to a field", e.FieldName, cce.NonNull(ctype).Name);
+ } else {
+ Contract.Assert(ctype != null && ctype.ResolvedClass != null); // follows from postcondition of ResolveMember
+ e.Field = (Field)member;
+ if (e.Obj is StaticReceiverExpr) {
+ Error(expr, "a field must be selected via an object, not just a class name");
+ }
+ // build the type substitution map
+ Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
+ for (int i = 0; i < ctype.TypeArgs.Count; i++) {
+ subst.Add(ctype.ResolvedClass.TypeArgs[i], ctype.TypeArgs[i]);
+ }
+ e.Type = SubstType(e.Field.Type, subst);
+ }
+
+ } else if (expr is SeqSelectExpr) {
+ SeqSelectExpr e = (SeqSelectExpr)expr;
+ ResolveSeqSelectExpr(e, twoState, true);
+
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr e = (MultiSelectExpr)expr;
+
+ ResolveExpression(e.Array, twoState);
+ Contract.Assert(e.Array.Type != null); // follows from postcondition of ResolveExpression
+ Type elementType = new InferredTypeProxy();
+ if (!UnifyTypes(e.Array.Type, builtIns.ArrayType(e.Indices.Count, elementType))) {
+ Error(e.Array, "array selection requires an array{0} (got {1})", e.Indices.Count, e.Array.Type);
+ }
+ int i = 0;
+ foreach (Expression idx in e.Indices) {
+ Contract.Assert(idx != null);
+ ResolveExpression(idx, twoState);
+ Contract.Assert(idx.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(idx.Type, Type.Int)) {
+ Error(idx, "array selection requires integer indices (got {0} for index {1})", idx.Type, i);
+ }
+ i++;
+ }
+ e.Type = elementType;
+
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr e = (SeqUpdateExpr)expr;
+ ResolveExpression(e.Seq, twoState);
+ Contract.Assert(e.Seq.Type != null); // follows from postcondition of ResolveExpression
+ Type elementType = new InferredTypeProxy();
+ Type domainType = new InferredTypeProxy();
+ Type rangeType = new InferredTypeProxy();
+ if (UnifyTypes(e.Seq.Type, new SeqType(elementType))) {
+ ResolveExpression(e.Index, twoState);
+ Contract.Assert(e.Index.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Index.Type, Type.Int)) {
+ Error(e.Index, "sequence update requires integer index (got {0})", e.Index.Type);
+ }
+ ResolveExpression(e.Value, twoState);
+ Contract.Assert(e.Value.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Value.Type, elementType)) {
+ Error(e.Value, "sequence update requires the value to have the element type of the sequence (got {0})", e.Value.Type);
+ }
+ expr.Type = e.Seq.Type;
+ } else if (UnifyTypes(e.Seq.Type, new MapType(domainType, rangeType))) {
+ ResolveExpression(e.Index, twoState);
+ if (!UnifyTypes(e.Index.Type, domainType)) {
+ Error(e.Index, "map update requires domain element to be of type {0} (got {1})", domainType, e.Index.Type);
+ }
+ ResolveExpression(e.Value, twoState);
+ if (!UnifyTypes(e.Value.Type, rangeType)) {
+ Error(e.Value, "map update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type);
+ }
+ expr.Type = e.Seq.Type;
+ } else {
+ Error(expr, "update requires a sequence or map (got {0})", e.Seq.Type);
+ }
+
+
+ } else if (expr is FunctionCallExpr) {
+ FunctionCallExpr e = (FunctionCallExpr)expr;
+ ResolveFunctionCallExpr(e, twoState, false);
+
+ } else if (expr is OldExpr) {
+ OldExpr e = (OldExpr)expr;
+ if (!twoState) {
+ Error(expr, "old expressions are not allowed in this context");
+ }
+ ResolveExpression(e.E, twoState, null);
+ expr.Type = e.E.Type;
+
+ } else if (expr is MultiSetFormingExpr) {
+ MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
+ ResolveExpression(e.E, twoState);
+ if (!UnifyTypes(e.E.Type, new SetType(new InferredTypeProxy())) && !UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) {
+ Error(e.tok, "can only form a multiset from a seq or set.");
+ }
+ expr.Type = new MultiSetType(((CollectionType)e.E.Type).Arg);
+ } else if (expr is FreshExpr) {
+ FreshExpr e = (FreshExpr)expr;
+ if (!twoState) {
+ Error(expr, "fresh expressions are not allowed in this context");
+ }
+ ResolveExpression(e.E, twoState);
+ // the type of e.E must be either an object or a collection of objects
+ Type t = e.E.Type;
+ Contract.Assert(t != null); // follows from postcondition of ResolveExpression
+ if (t is CollectionType) {
+ t = ((CollectionType)t).Arg;
+ }
+ if (t is ObjectType) {
+ // fine
+ } else if (UserDefinedType.DenotesClass(t) != null) {
+ // fine
+ } else if (t.IsDatatype) {
+ // fine, treat this as the datatype itself.
+ } else {
+ Error(expr, "the argument of a fresh expression must denote an object or a collection of objects (instead got {0})", e.E.Type);
+ }
+ expr.Type = Type.Bool;
+
+ } else if (expr is UnaryExpr) {
+ UnaryExpr e = (UnaryExpr)expr;
+ ResolveExpression(e.E, twoState);
+ Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
+ switch (e.Op) {
+ case UnaryExpr.Opcode.Not:
+ if (!UnifyTypes(e.E.Type, Type.Bool)) {
+ Error(expr, "logical negation expects a boolean argument (instead got {0})", e.E.Type);
+ }
+ expr.Type = Type.Bool;
+ break;
+ case UnaryExpr.Opcode.SetChoose:
+ var elType = new InferredTypeProxy();
+ if (!UnifyTypes(e.E.Type, new SetType(elType))) {
+ Error(expr, "choose operator expects a set argument (instead got {0})", e.E.Type);
+ }
+ expr.Type = elType;
+ break;
+ case UnaryExpr.Opcode.SeqLength:
+ if (!UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) {
+ Error(expr, "length operator expects a sequence argument (instead got {0})", e.E.Type);
+ }
+ expr.Type = Type.Int;
+ break;
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary operator
+ }
+
+ } else if (expr is BinaryExpr) {
+ BinaryExpr e = (BinaryExpr)expr;
+ ResolveExpression(e.E0, twoState);
+ Contract.Assert(e.E0.Type != null); // follows from postcondition of ResolveExpression
+ ResolveExpression(e.E1, twoState);
+ Contract.Assert(e.E1.Type != null); // follows from postcondition of ResolveExpression
+ switch (e.Op) {
+ case BinaryExpr.Opcode.Iff:
+ case BinaryExpr.Opcode.Imp:
+ case BinaryExpr.Opcode.And:
+ case BinaryExpr.Opcode.Or:
+ if (!UnifyTypes(e.E0.Type, Type.Bool)) {
+ Error(expr, "first argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ }
+ if (!UnifyTypes(e.E1.Type, Type.Bool)) {
+ Error(expr, "second argument to {0} must be of type bool (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
+ }
+ expr.Type = Type.Bool;
+ break;
+
+ case BinaryExpr.Opcode.Eq:
+ case BinaryExpr.Opcode.Neq:
+ if (!ComparableTypes(e.E0.Type, e.E1.Type)) {
+ if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
+ Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
+ }
+ }
+ expr.Type = Type.Bool;
+ break;
+
+ case BinaryExpr.Opcode.Disjoint:
+ // TODO: the error messages are backwards from what (ideally) they should be. this is necessary because UnifyTypes can't backtrack.
+ if (!UnifyTypes(e.E0.Type, e.E1.Type)) {
+ Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);
+ }
+ if (!UnifyTypes(e.E0.Type, new SetType(new InferredTypeProxy())) &&
+ !UnifyTypes(e.E0.Type, new MultiSetType(new InferredTypeProxy())) &&
+ !UnifyTypes(e.E0.Type, new MapType(new InferredTypeProxy(), new InferredTypeProxy()))) {
+ Error(expr, "arguments must be of a [multi]set or map type (got {0})", e.E0.Type);
+ }
+ expr.Type = Type.Bool;
+ break;
+
+ case BinaryExpr.Opcode.Lt:
+ case BinaryExpr.Opcode.Le:
+ case BinaryExpr.Opcode.Add: {
+ if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsIndDatatype) {
+ if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {
+ Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
+ }
+ expr.Type = Type.Bool;
+ } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsIndDatatype) {
+ if (!UnifyTypes(e.E0.Type, new DatatypeProxy())) {
+ Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
+ }
+ expr.Type = Type.Bool;
+ } else {
+ bool err = false;
+ if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true))) {
+ Error(expr, "arguments to {0} must be int or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ err = true;
+ }
+ if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
+ Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
+ err = true;
+ }
+ if (e.Op != BinaryExpr.Opcode.Add) {
+ expr.Type = Type.Bool;
+ } else if (!err) {
+ expr.Type = e.E0.Type;
+ }
+ }
+ }
+ break;
+
+ case BinaryExpr.Opcode.Sub:
+ case BinaryExpr.Opcode.Mul:
+ case BinaryExpr.Opcode.Gt:
+ case BinaryExpr.Opcode.Ge: {
+ if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsIndDatatype) {
+ if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {
+ Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
+ }
+ expr.Type = Type.Bool;
+ } else {
+ bool err = false;
+ if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false))) {
+ Error(expr, "arguments to {0} must be int or a set (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ err = true;
+ }
+ if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
+ Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
+ err = true;
+ }
+ if (e.Op == BinaryExpr.Opcode.Gt || e.Op == BinaryExpr.Opcode.Ge) {
+ expr.Type = Type.Bool;
+ } else if (!err) {
+ expr.Type = e.E0.Type;
+ }
+ }
+ }
+ break;
+
+ case BinaryExpr.Opcode.In:
+ case BinaryExpr.Opcode.NotIn:
+ if (!UnifyTypes(e.E1.Type, new CollectionTypeProxy(e.E0.Type))) {
+ Error(expr, "second argument to \"{0}\" must be a set or sequence with elements of type {1}, or a map with domain {1} (instead got {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
+ }
+ expr.Type = Type.Bool;
+ break;
+
+ case BinaryExpr.Opcode.Div:
+ case BinaryExpr.Opcode.Mod:
+ if (!UnifyTypes(e.E0.Type, Type.Int)) {
+ Error(expr, "first argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ }
+ if (!UnifyTypes(e.E1.Type, Type.Int)) {
+ Error(expr, "second argument to {0} must be of type int (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E1.Type);
+ }
+ expr.Type = Type.Int;
+ break;
+
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected operator
+ }
+ e.ResolvedOp = ResolveOp(e.Op, e.E1.Type);
+
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ foreach (var rhs in e.RHSs) {
+ ResolveExpression(rhs, twoState);
+ }
+ scope.PushMarker();
+ if (e.Vars.Count != e.RHSs.Count) {
+ Error(expr, "let expression must have same number of bound variables (found {0}) as RHSs (found {1})", e.Vars.Count, e.RHSs.Count);
+ }
+ int i = 0;
+ foreach (var v in e.Vars) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate let-variable name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type, null, true);
+ if (i < e.RHSs.Count && !UnifyTypes(v.Type, e.RHSs[i].Type)) {
+ Error(e.RHSs[i].tok, "type of RHS ({0}) does not match type of bound variable ({1})", e.RHSs[i].Type, v.Type);
+ }
+ i++;
+ }
+ ResolveExpression(e.Body, twoState);
+ scope.PopMarker();
+ expr.Type = e.Body.Type;
+
+ } else if (expr is NamedExpr) {
+ var e = (NamedExpr)expr;
+ ResolveExpression(e.Body, twoState);
+ if (e.Contract != null) ResolveExpression(e.Contract, twoState);
+ e.Type = e.Body.Type;
+ } else if (expr is QuantifierExpr) {
+ QuantifierExpr e = (QuantifierExpr)expr;
+ int prevErrorCount = ErrorCount;
+ scope.PushMarker();
+ foreach (BoundVar v in e.BoundVars) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate bound-variable name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type, null, true);
+ }
+ if (e.Range != null) {
+ ResolveExpression(e.Range, twoState);
+ Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Range.Type, Type.Bool)) {
+ Error(expr, "range of quantifier must be of type bool (instead got {0})", e.Range.Type);
+ }
+ }
+ ResolveExpression(e.Term, twoState);
+ Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Term.Type, Type.Bool)) {
+ Error(expr, "body of quantifier must be of type bool (instead got {0})", e.Term.Type);
+ }
+ // Since the body is more likely to infer the types of the bound variables, resolve it
+ // first (above) and only then resolve the attributes (below).
+ ResolveAttributes(e.Attributes, twoState);
+ scope.PopMarker();
+ expr.Type = Type.Bool;
+
+ if (prevErrorCount == ErrorCount) {
+ var missingBounds = new List<BoundVar>();
+ e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, false, missingBounds);
+ if (missingBounds.Count != 0) {
+ // Report errors here about quantifications that depend on the allocation state.
+ var mb = missingBounds;
+ if (currentFunction != null) {
+ mb = new List<BoundVar>(); // (who cares if we allocate another array; this happens only in the case of a resolution error anyhow)
+ foreach (var bv in missingBounds) {
+ if (bv.Type.IsRefType) {
+ Error(expr, "a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{0}'", bv.Name);
+ } else {
+ mb.Add(bv);
+ }
+ }
+ }
+ if (mb.Count != 0) {
+ e.MissingBounds = mb;
+ }
+ }
+ }
+
+ } else if (expr is SetComprehension) {
+ var e = (SetComprehension)expr;
+ int prevErrorCount = ErrorCount;
+ scope.PushMarker();
+ foreach (BoundVar v in e.BoundVars) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate bound-variable name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type, null, true);
+ }
+ ResolveExpression(e.Range, twoState);
+ Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Range.Type, Type.Bool)) {
+ Error(expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
+ }
+ ResolveExpression(e.Term, twoState);
+ Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression
+
+ ResolveAttributes(e.Attributes, twoState);
+ scope.PopMarker();
+ expr.Type = new SetType(e.Term.Type);
+
+ if (prevErrorCount == ErrorCount) {
+ var missingBounds = new List<BoundVar>();
+ e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);
+ if (missingBounds.Count != 0) {
+ e.MissingBounds = missingBounds;
+ foreach (var bv in e.MissingBounds) {
+ Error(expr, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ }
+ }
+ }
+
+ } else if (expr is MapComprehension) {
+ var e = (MapComprehension)expr;
+ int prevErrorCount = ErrorCount;
+ scope.PushMarker();
+ if (e.BoundVars.Count != 1) {
+ Error(e.tok, "a map comprehension must have exactly one bound variable.");
+ }
+ foreach (BoundVar v in e.BoundVars) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate bound-variable name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type, null, true);
+ }
+ ResolveExpression(e.Range, twoState);
+ Contract.Assert(e.Range.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Range.Type, Type.Bool)) {
+ Error(expr, "range of comprehension must be of type bool (instead got {0})", e.Range.Type);
+ }
+ ResolveExpression(e.Term, twoState);
+ Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression
+
+ ResolveAttributes(e.Attributes, twoState);
+ scope.PopMarker();
+ expr.Type = new MapType(e.BoundVars[0].Type, e.Term.Type);
+
+ if (prevErrorCount == ErrorCount) {
+ var missingBounds = new List<BoundVar>();
+ e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);
+ if (missingBounds.Count != 0) {
+ e.MissingBounds = missingBounds;
+ foreach (var bv in e.MissingBounds) {
+ Error(expr, "a map comprehension must produce a finite domain, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ }
+ }
+ }
+
+ } else if (expr is WildcardExpr) {
+ expr.Type = new SetType(new ObjectType());
+
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ ResolveExpression(e.Guard, twoState);
+ Contract.Assert(e.Guard.Type != null); // follows from postcondition of ResolveExpression
+ ResolveExpression(e.Body, twoState);
+ Contract.Assert(e.Body.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Guard.Type, Type.Bool)) {
+ Error(expr, "guard condition in {0} expression must be a boolean (instead got {1})", e.Kind, e.Guard.Type);
+ }
+ expr.Type = e.Body.Type;
+
+ } else if (expr is ITEExpr) {
+ ITEExpr e = (ITEExpr)expr;
+ ResolveExpression(e.Test, twoState);
+ Contract.Assert(e.Test.Type != null); // follows from postcondition of ResolveExpression
+ ResolveExpression(e.Thn, twoState);
+ Contract.Assert(e.Thn.Type != null); // follows from postcondition of ResolveExpression
+ ResolveExpression(e.Els, twoState);
+ Contract.Assert(e.Els.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.Test.Type, Type.Bool)) {
+ Error(expr, "guard condition in if-then-else expression must be a boolean (instead got {0})", e.Test.Type);
+ }
+ if (UnifyTypes(e.Thn.Type, e.Els.Type)) {
+ expr.Type = e.Thn.Type;
+ } else {
+ Error(expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type);
+ }
+
+ } else if (expr is MatchExpr) {
+ MatchExpr me = (MatchExpr)expr;
+ Contract.Assert(!twoState); // currently, match expressions are allowed only at the outermost level of function bodies
+ if (matchVarContext == null) {
+ Error(me, "'match' expressions are not supported in this context");
+ matchVarContext = new List<IVariable>();
+ }
+ ResolveExpression(me.Source, twoState);
+ Contract.Assert(me.Source.Type != null); // follows from postcondition of ResolveExpression
+ UserDefinedType sourceType = null;
+ DatatypeDecl dtd = null;
+ Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
+ if (me.Source.Type.IsDatatype) {
+ sourceType = (UserDefinedType)me.Source.Type;
+ dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);
+ }
+ Dictionary<string, DatatypeCtor> ctors;
+ IVariable goodMatchVariable = null;
+ if (dtd == null) {
+ Error(me.Source, "the type of the match source expression must be a datatype (instead found {0})", me.Source.Type);
+ ctors = null;
+ } else {
+ Contract.Assert(sourceType != null); // dtd and sourceType are set together above
+ ctors = datatypeCtors[dtd];
+ Contract.Assert(ctors != null); // dtd should have been inserted into datatypeCtors during a previous resolution stage
+
+ IdentifierExpr ie = me.Source.Resolved as IdentifierExpr;
+ if (ie == null || !(ie.Var is Formal || ie.Var is BoundVar)) {
+ Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function or an enclosing match expression");
+ } else if (!matchVarContext.Contains(ie.Var)) {
+ Error(me.Source.tok, "match source expression '{0}' has already been used as a match source expression in this context", ie.Var.Name);
+ } else {
+ goodMatchVariable = ie.Var;
+ }
+
+ // build the type-parameter substitution map for this use of the datatype
+ for (int i = 0; i < dtd.TypeArgs.Count; i++) {
+ subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);
+ }
+ }
+
+ Dictionary<string, object> memberNamesUsed = new Dictionary<string, object>(); // this is really a set
+ expr.Type = new InferredTypeProxy();
+ foreach (MatchCaseExpr mc in me.Cases) {
+ DatatypeCtor ctor = null;
+ if (ctors != null) {
+ Contract.Assert(dtd != null);
+ if (!ctors.TryGetValue(mc.Id, out ctor)) {
+ Error(mc.tok, "member {0} does not exist in datatype {1}", mc.Id, dtd.Name);
+ } else {
+ Contract.Assert(ctor != null); // follows from postcondition of TryGetValue
+ mc.Ctor = ctor;
+ if (ctor.Formals.Count != mc.Arguments.Count) {
+ Error(mc.tok, "member {0} has wrong number of formals (found {1}, expected {2})", mc.Id, mc.Arguments.Count, ctor.Formals.Count);
+ }
+ if (memberNamesUsed.ContainsKey(mc.Id)) {
+ Error(mc.tok, "member {0} appears in more than one case", mc.Id);
+ } else {
+ memberNamesUsed.Add(mc.Id, null); // add mc.Id to the set of names used
+ }
+ }
+ }
+ scope.PushMarker();
+ int i = 0;
+ foreach (BoundVar v in mc.Arguments) {
+ if (!scope.Push(v.Name, v)) {
+ Error(v, "Duplicate parameter name: {0}", v.Name);
+ }
+ ResolveType(v.tok, v.Type, null, true);
+ if (ctor != null && i < ctor.Formals.Count) {
+ Formal formal = ctor.Formals[i];
+ Type st = SubstType(formal.Type, subst);
+ if (!UnifyTypes(v.Type, st)) {
+ Error(expr, "the declared type of the formal ({0}) does not agree with the corresponding type in the constructor's signature ({1})", v.Type, st);
+ }
+ v.IsGhost = formal.IsGhost;
+ }
+ i++;
+ }
+ List<IVariable> innerMatchVarContext = new List<IVariable>(matchVarContext);
+ if (goodMatchVariable != null) {
+ innerMatchVarContext.Remove(goodMatchVariable); // this variable is no longer available for matching
+ }
+ innerMatchVarContext.AddRange(mc.Arguments);
+ ResolveExpression(mc.Body, twoState, innerMatchVarContext);
+ Contract.Assert(mc.Body.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(expr.Type, mc.Body.Type)) {
+ Error(mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);
+ }
+ scope.PopMarker();
+ }
+ if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) {
+ // We could complain about the syntactic omission of constructors:
+ // Error(expr, "match expression does not cover all constructors");
+ // but instead we let the verifier do a semantic check.
+ // So, for now, record the missing constructors:
+ foreach (var ctr in dtd.Ctors) {
+ if (!memberNamesUsed.ContainsKey(ctr.Name)) {
+ me.MissingCases.Add(ctr);
+ }
+ }
+ Contract.Assert(memberNamesUsed.Count + me.MissingCases.Count == dtd.Ctors.Count);
+ }
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
+ }
+
+ if (expr.Type == null) {
+ // some resolution error occurred
+ expr.Type = Type.Flexible;
+ }
+ }
+
+ private void ResolveDatatypeValue(bool twoState, DatatypeValue dtv, DatatypeDecl dt) {
+ // this resolution is a little special, in that the syntax shows only the base name, not its instantiation (which is inferred)
+ List<Type> gt = new List<Type>(dt.TypeArgs.Count);
+ Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
+ for (int i = 0; i < dt.TypeArgs.Count; i++) {
+ Type t = new InferredTypeProxy();
+ gt.Add(t);
+ dtv.InferredTypeArgs.Add(t);
+ subst.Add(dt.TypeArgs[i], t);
+ }
+ // Construct a resolved type directly, as we know the declaration is dt.
+ dtv.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, dt, gt);
+
+ DatatypeCtor ctor;
+ if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {
+ Error(dtv.tok, "undeclared constructor {0} in datatype {1}", dtv.MemberName, dtv.DatatypeName);
+ } else {
+ Contract.Assert(ctor != null); // follows from postcondition of TryGetValue
+ dtv.Ctor = ctor;
+ if (ctor.Formals.Count != dtv.Arguments.Count) {
+ Error(dtv.tok, "wrong number of arguments to datatype constructor {0} (found {1}, expected {2})", dtv.DatatypeName, dtv.Arguments.Count, ctor.Formals.Count);
+ }
+ }
+ int j = 0;
+ foreach (Expression arg in dtv.Arguments) {
+ Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;
+ ResolveExpression(arg, twoState, null);
+ Contract.Assert(arg.Type != null); // follows from postcondition of ResolveExpression
+ if (formal != null) {
+ Type st = SubstType(formal.Type, subst);
+ if (!UnifyTypes(arg.Type, st)) {
+ Error(arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);
+ }
+ }
+ j++;
+ }
+ }
+
+ private bool ComparableTypes(Type A, Type B) {
+ if (A.IsArrayType && B.IsArrayType) {
+ Type a = UserDefinedType.ArrayElementType(A);
+ Type b = UserDefinedType.ArrayElementType(B);
+ return CouldPossiblyBeSameType(a, b);
+ } else
+ if (A is UserDefinedType && B is UserDefinedType) {
+ UserDefinedType a = (UserDefinedType)A;
+ UserDefinedType b = (UserDefinedType)B;
+ if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass.Name == b.ResolvedClass.Name) {
+ if (a.TypeArgs.Count != b.TypeArgs.Count) {
+ return false; // this probably doesn't happen if the classes are the same.
+ }
+ for (int i = 0; i < a.TypeArgs.Count; i++) {
+ if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))
+ return false;
+ }
+ // all parameters could be the same
+ return true;
+ }
+ // either we don't know what class it is yet, or the classes mismatch
+ return false;
+ }
+ return false;
+ }
+ private bool CouldPossiblyBeSameType(Type A, Type B) {
+ if (A.IsTypeParameter || B.IsTypeParameter) {
+ return true;
+ }
+ if (A.IsArrayType && B.IsArrayType) {
+ Type a = UserDefinedType.ArrayElementType(A);
+ Type b = UserDefinedType.ArrayElementType(B);
+ return CouldPossiblyBeSameType(a, b);
+ }
+ if (A is UserDefinedType && B is UserDefinedType) {
+ UserDefinedType a = (UserDefinedType)A;
+ UserDefinedType b = (UserDefinedType)B;
+ if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass == b.ResolvedClass) {
+ if (a.TypeArgs.Count != b.TypeArgs.Count) {
+ return false; // this probably doesn't happen if the classes are the same.
+ }
+ for (int i = 0; i < a.TypeArgs.Count; i++) {
+ if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))
+ return false;
+ }
+ // all parameters could be the same
+ return true;
+ }
+ // either we don't know what class it is yet, or the classes mismatch
+ return false;
+ }
+ return false;
+ }
+
+ /// <summary>
+ /// Generate an error for every non-ghost feature used in "expr".
+ /// Requires "expr" to have been successfully resolved.
+ /// </summary>
+ void CheckIsNonGhost(Expression expr) {
+ Contract.Requires(expr != null);
+ Contract.Requires(expr.WasResolved()); // this check approximates the requirement that "expr" be resolved
+
+ if (expr is IdentifierExpr) {
+ var e = (IdentifierExpr)expr;
+ if (e.Var != null && e.Var.IsGhost) {
+ Error(expr, "ghost variables are allowed only in specification contexts");
+ return;
+ }
+
+ } else if (expr is FieldSelectExpr) {
+ var e = (FieldSelectExpr)expr;
+ if (e.Field != null && e.Field.IsGhost) {
+ Error(expr, "ghost fields are allowed only in specification contexts");
+ return;
+ }
+
+ } else if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ if (e.Function != null) {
+ if (e.Function.IsGhost) {
+ Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')");
+ return;
+ }
+ // function is okay, so check all NON-ghost arguments
+ CheckIsNonGhost(e.Receiver);
+ for (int i = 0; i < e.Function.Formals.Count; i++) {
+ if (!e.Function.Formals[i].IsGhost) {
+ CheckIsNonGhost(e.Args[i]);
+ }
+ }
+ }
+ return;
+
+ } else if (expr is DatatypeValue) {
+ var e = (DatatypeValue)expr;
+ // check all NON-ghost arguments
+ // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals|
+ for (int i = 0; i < e.Arguments.Count; i++) {
+ if (!e.Ctor.Formals[i].IsGhost) {
+ CheckIsNonGhost(e.Arguments[i]);
+ }
+ }
+ return;
+
+ } else if (expr is OldExpr) {
+ Error(expr, "old expressions are allowed only in specification and ghost contexts");
+ return;
+
+ } else if (expr is FreshExpr) {
+ Error(expr, "fresh expressions are allowed only in specification and ghost contexts");
+ return;
+
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ // ignore the guard
+ CheckIsNonGhost(e.Body);
+ return;
+
+ } else if (expr is BinaryExpr) {
+ var e = (BinaryExpr)expr;
+ switch (e.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.RankGt:
+ case BinaryExpr.ResolvedOpcode.RankLt:
+ Error(expr, "rank comparisons are allowed only in specification and ghost contexts");
+ return;
+ default:
+ break;
+ }
+
+ } else if (expr is QuantifierExpr) {
+ var e = (QuantifierExpr)expr;
+ if (e.MissingBounds != null) {
+ foreach (var bv in e.MissingBounds) {
+ Error(expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+ }
+ return;
+ }
+ } else if (expr is NamedExpr) {
+ if (!moduleInfo.IsGhost)
+ CheckIsNonGhost(((NamedExpr)expr).Body);
+ return;
+ }
+
+ foreach (var ee in expr.SubExpressions) {
+ CheckIsNonGhost(ee);
+ }
+ }
+
+ /// <summary>
+ /// If "!allowMethodCall" or if what is being called does not refer to a method, resolves "e" and returns "null".
+ /// Otherwise (that is, if "allowMethodCall" and what is being called refers to a method), resolves the receiver
+ /// of "e" but NOT the arguments, and returns a CallRhs corresponding to the call.
+ /// </summary>
+ CallRhs ResolveFunctionCallExpr(FunctionCallExpr e, bool twoState, bool allowMethodCall) {
+ ResolveReceiver(e.Receiver, twoState);
+ Contract.Assert(e.Receiver.Type != null); // follows from postcondition of ResolveExpression
+ NonProxyType nptype;
+ MemberDecl member = ResolveMember(e.tok, e.Receiver.Type, e.Name, out nptype);
+#if !NO_WORK_TO_BE_DONE
+ UserDefinedType ctype = (UserDefinedType)nptype;
+#endif
+ if (member == null) {
+ // error has already been reported by ResolveMember
+ } else if (member is Method) {
+ if (allowMethodCall) {
+ // it's a method
+ return new CallRhs(e.tok, e.Receiver, e.Name, e.Args);
+ } else {
+ Error(e, "member {0} in type {1} refers to a method, but only functions can be used in this context", e.Name, cce.NonNull(ctype).Name);
+ }
+ } else if (!(member is Function)) {
+ Error(e, "member {0} in type {1} does not refer to a function", e.Name, cce.NonNull(ctype).Name);
+ } else {
+ Function function = (Function)member;
+ e.Function = function;
+ if (function is CoPredicate) {
+ ((CoPredicate)function).Uses.Add(e);
+ }
+ if (e.Receiver is StaticReceiverExpr && !function.IsStatic) {
+ Error(e, "an instance function must be selected via an object, not just a class name");
+ }
+ if (function.Formals.Count != e.Args.Count) {
+ Error(e, "wrong number of function arguments (got {0}, expected {1})", e.Args.Count, function.Formals.Count);
+ } else {
+ Contract.Assert(ctype != null); // follows from postcondition of ResolveMember
+ if (!function.IsStatic) {
+ if (!scope.AllowInstance && e.Receiver is ThisExpr) {
+ // The call really needs an instance, but that instance is given as 'this', which is not
+ // available in this context. In most cases, occurrences of 'this' inside e.Receiver would
+ // have been caught in the recursive call to resolve e.Receiver, but not the specific case
+ // of e.Receiver being 'this' (explicitly or implicitly), for that case needs to be allowed
+ // in the event that a static function calls another static function (and note that we need the
+ // type of the receiver in order to find the method, so we could not have made this check
+ // earlier).
+ Error(e.Receiver, "'this' is not allowed in a 'static' context");
+ } else if (e.Receiver is StaticReceiverExpr) {
+ Error(e.Receiver, "call to instance function requires an instance");
+ }
+ }
+ // build the type substitution map
+ e.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
+ for (int i = 0; i < ctype.TypeArgs.Count; i++) {
+ e.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
+ }
+ foreach (TypeParameter p in function.TypeArgs) {
+ e.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));
+ }
+ // type check the arguments
+ for (int i = 0; i < function.Formals.Count; i++) {
+ Expression farg = e.Args[i];
+ ResolveExpression(farg, twoState);
+ Contract.Assert(farg.Type != null); // follows from postcondition of ResolveExpression
+ Type s = SubstType(function.Formals[i].Type, e.TypeArgumentSubstitutions);
+ if (!UnifyTypes(farg.Type, s)) {
+ Error(e, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
+ }
+ }
+ e.Type = SubstType(function.ResultType, e.TypeArgumentSubstitutions);
+ }
+
+ // Resolution termination check
+ if (currentFunction != null && currentFunction.EnclosingClass != null && function.EnclosingClass != null) {
+ ModuleDefinition callerModule = currentFunction.EnclosingClass.Module;
+ ModuleDefinition calleeModule = function.EnclosingClass.Module;
+ if (callerModule == calleeModule) {
+ // intra-module call; this is allowed; add edge in module's call graph
+ callerModule.CallGraph.AddEdge(currentFunction, function);
+ if (currentFunction == function) {
+ currentFunction.IsRecursive = true; // self recursion (mutual recursion is determined elsewhere)
+ }
+ } else {
+ //Contract.Assert(dependencies.Reaches(callerModule, calleeModule));
+ }
+ }
+ }
+ return null;
+ }
+
+ /// <summary>
+ /// If "!allowMethodCall", or if "e" does not designate a method call, resolves "e" and returns "null".
+ /// Otherwise, resolves all sub-parts of "e" and returns a (resolved) CallRhs expression representing the call.
+ /// </summary>
+ CallRhs ResolveIdentifierSequence(IdentifierSequence e, bool twoState, bool allowMethodCall) {
+ // Look up "id" as follows:
+ // - local variable, parameter, or bound variable (if this clashes with something of interest, one can always rename the local variable locally)
+ // - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type)
+ // (if two imported types have the same name, an error message is produced here)
+ // - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)
+ // - field, function or method name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")
+ // - iterator
+ // - static function or method in the enclosing module, or its imports.
+
+ Expression r = null; // resolved version of e
+ CallRhs call = null;
+
+ TopLevelDecl decl;
+ Tuple<DatatypeCtor, bool> pair;
+ Dictionary<string, MemberDecl> members;
+ MemberDecl member;
+ var id = e.Tokens[0];
+ if (scope.Find(id.val) != null) {
+ // ----- root is a local variable, parameter, or bound variable
+ r = new IdentifierExpr(id, id.val);
+ ResolveExpression(r, twoState);
+ r = ResolveSuffix(r, e, 1, twoState, allowMethodCall, out call);
+
+ } else if (moduleInfo.TopLevels.TryGetValue(id.val, out decl)) {
+ if (decl is AmbiguousTopLevelDecl) {
+ Error(id, "The name {0} ambiguously refers to a type in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());
+ } else if (e.Tokens.Count == 1 && e.Arguments == null) {
+ Error(id, "name of type ('{0}') is used as a variable", id.val);
+ } else if (e.Tokens.Count == 1 && e.Arguments != null) {
+ Error(id, "name of type ('{0}') is used as a function", id.val);
+ // resolve the arguments nonetheless
+ foreach (var arg in e.Arguments) {
+ ResolveExpression(arg, twoState);
+ }
+ } else if (decl is ClassDecl) {
+ // ----- root is a class
+ var cd = (ClassDecl)decl;
+ r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, twoState, allowMethodCall, out call);
+
+ } else if (decl is ModuleDecl) {
+ // ----- root is a submodule
+ if (!(1 < e.Tokens.Count)) {
+ Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name);
+ }
+ call = ResolveIdentifierSequenceModuleScope(e, 1, ((ModuleDecl)decl).Signature, twoState, allowMethodCall);
+ } else {
+ // ----- root is a datatype
+ var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl
+ var args = (e.Tokens.Count == 2 ? e.Arguments : null) ?? new List<Expression>();
+ r = new DatatypeValue(id, id.val, e.Tokens[1].val, args);
+ ResolveExpression(r, twoState);
+ if (e.Tokens.Count != 2) {
+ r = ResolveSuffix(r, e, 2, twoState, allowMethodCall, out call);
+ }
+ }
+
+ } else if (moduleInfo.Ctors.TryGetValue(id.val, out pair)) {
+ // ----- root is a datatype constructor
+ if (pair.Item2) {
+ // there is more than one constructor with this name
+ Error(id, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", id.val, pair.Item1.EnclosingDatatype.Name);
+ } else {
+ var args = (e.Tokens.Count == 1 ? e.Arguments : null) ?? new List<Expression>();
+ r = new DatatypeValue(id, pair.Item1.EnclosingDatatype.Name, id.val, args);
+ ResolveExpression(r, twoState);
+ if (e.Tokens.Count != 1) {
+ r = ResolveSuffix(r, e, 1, twoState, allowMethodCall, out call);
+ }
+ }
+
+ } else if ((currentClass != null && classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member))
+ || moduleInfo.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.
+ {
+ // ----- field, function, or method
+ if (member is AmbiguousMemberDecl) {
+ Contract.Assert(member.IsStatic); // currently, static members of _default are the only thing which can be ambiguous.
+ Error(id, "The name {0} ambiguously refers to a static member in one of the modules {1}", id.val, ((AmbiguousMemberDecl)member).ModuleNames());
+ } else {
+ Expression receiver;
+ if (member.IsStatic) {
+ receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);
+ } else {
+ if (!scope.AllowInstance) {
+ Error(id, "'this' is not allowed in a 'static' context");
+ // nevertheless, set "receiver" to a value so we can continue resolution
+ }
+ receiver = new ImplicitThisExpr(id);
+ receiver.Type = GetThisType(id, (ClassDecl)member.EnclosingClass); // resolve here
+ }
+ r = ResolveSuffix(receiver, e, 0, twoState, allowMethodCall, out call);
+ }
+
+ } else {
+ Error(id, "unresolved identifier: {0}", id.val);
+ // resolve arguments, if any
+ if (e.Arguments != null) {
+ foreach (var arg in e.Arguments) {
+ ResolveExpression(arg, twoState);
+ }
+ }
+ }
+
+ if (r != null) {
+ e.ResolvedExpression = r;
+ e.Type = r.Type;
+ }
+ return call;
+ }
+
+ CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature sig, bool twoState, bool allowMethodCall) {
+ // Look up "id" as follows:
+ // - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type)
+ // (if two imported types have the same name, an error message is produced here)
+ // - static function or method of sig.
+ // This is used to look up names that appear after a dot in a sequence identifier. For example, in X.M.*, M should be looked up in X, but
+ // should not consult the local scope. This distingushes this from the above, in that local scope, imported modules, etc. are ignored.
+ Contract.Requires(p < e.Tokens.Count);
+ Expression r = null; // resolved version of e
+ CallRhs call = null;
+
+ TopLevelDecl decl;
+ MemberDecl member;
+ Tuple<DatatypeCtor, bool> pair;
+ var id = e.Tokens[p];
+ sig = GetSignature(sig);
+ if (sig.TopLevels.TryGetValue(id.val, out decl)) {
+ if (decl is AmbiguousTopLevelDecl) {
+ Error(id, "The name {0} ambiguously refers to a something in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());
+ } else if (decl is ClassDecl) {
+ // ----- root is a class
+ var cd = (ClassDecl)decl;
+ r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, p + 1, twoState, allowMethodCall, out call);
+
+ } else if (decl is ModuleDecl) {
+ // ----- root is a submodule
+ if (!(p + 1 < e.Tokens.Count)) {
+ Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name);
+ }
+ call = ResolveIdentifierSequenceModuleScope(e, p + 1, ((ModuleDecl)decl).Signature, twoState, allowMethodCall);
+ } else {
+ // ----- root is a datatype
+ var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl
+ var args = (e.Tokens.Count == p + 2 ? e.Arguments : null) ?? new List<Expression>();
+ r = new DatatypeValue(id, id.val, e.Tokens[p + 1].val, args);
+ ResolveDatatypeValue(twoState, (DatatypeValue)r, dt);
+ if (e.Tokens.Count != p + 2) {
+ r = ResolveSuffix(r, e, p + 2, twoState, allowMethodCall, out call);
+ }
+ }
+ } else if (sig.Ctors.TryGetValue(id.val, out pair)) {
+ // ----- root is a datatype constructor
+ if (pair.Item2) {
+ // there is more than one constructor with this name
+ Error(id, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", id.val, pair.Item1.EnclosingDatatype.Name);
+ } else {
+ var dt = pair.Item1.EnclosingDatatype;
+ var args = (e.Tokens.Count == p + 1 ? e.Arguments : null) ?? new List<Expression>();
+ r = new DatatypeValue(id, dt.Name, id.val, args);
+ ResolveDatatypeValue(twoState, (DatatypeValue)r, dt);
+ if (e.Tokens.Count != p + 1) {
+ r = ResolveSuffix(r, e, p + 1, twoState, allowMethodCall, out call);
+ }
+ }
+ } else if (sig.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.
+ {
+ // ----- function, or method
+ Expression receiver;
+ Contract.Assert(member.IsStatic);
+ receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);
+ r = ResolveSuffix(receiver, e, p, twoState, allowMethodCall, out call);
+
+ } else {
+ Error(id, "unresolved identifier: {0}", id.val);
+ // resolve arguments, if any
+ if (e.Arguments != null) {
+ foreach (var arg in e.Arguments) {
+ ResolveExpression(arg, twoState);
+ }
+ }
+ }
+
+ if (r != null) {
+ e.ResolvedExpression = r;
+ e.Type = r.Type;
+ }
+ return call;
+ }
+
+ private ModuleSignature GetSignature(ModuleSignature sig) {
+ if (useCompileSignatures) {
+ while (sig.CompileSignature != null)
+ sig = sig.CompileSignature;
+ }
+ return sig;
+ }
+ /// <summary>
+ /// Given resolved expression "r" and unresolved expressions e.Tokens[p..] and e.Arguments.
+ /// Returns a resolved version of the expression:
+ /// r . e.Tokens[p] . e.Tokens[p+1] ... . e.Tokens[e.Tokens.Count-1] ( e.Arguments )
+ /// Except, if "allowMethodCall" is "true" and the would-be-returned value designates a method
+ /// call, instead returns null and returns "call" as a non-null value.
+ /// </summary>
+ Expression ResolveSuffix(Expression r, IdentifierSequence e, int p, bool twoState, bool allowMethodCall, out CallRhs call) {
+ Contract.Requires(r != null);
+ Contract.Requires(e != null);
+ Contract.Requires(0 <= p && p <= e.Tokens.Count);
+ Contract.Ensures((Contract.Result<Expression>() != null && Contract.ValueAtReturn(out call) == null) ||
+ (allowMethodCall && Contract.Result<Expression>() == null && Contract.ValueAtReturn(out call) != null));
+
+ call = null;
+ int nonCallArguments = e.Arguments == null ? e.Tokens.Count : e.Tokens.Count - 1;
+ for (; p < nonCallArguments; p++) {
+ var resolved = ResolvePredicateOrField(e.Tokens[p], r, e.Tokens[p].val);
+ if (resolved != null) {
+ r = resolved;
+ ResolveExpression(r, twoState, null);
+ }
+ }
+
+ if (p < e.Tokens.Count) {
+ Contract.Assert(e.Arguments != null);
+
+
+ bool itIsAMethod = false;
+ if (allowMethodCall) {
+ var udt = r.Type.Normalize() as UserDefinedType;
+ if (udt != null && udt.ResolvedClass != null) {
+ Dictionary<string, MemberDecl> members;
+ if (udt.ResolvedClass is ClassDecl) {
+ classMembers.TryGetValue((ClassDecl)udt.ResolvedClass, out members);
+ } else {
+ members = null;
+ }
+ MemberDecl member;
+ if (members != null && members.TryGetValue(e.Tokens[p].val, out member) && member is Method) {
+ itIsAMethod = true;
+ }
+ }
+ }
+ if (itIsAMethod) {
+ // method
+ call = new CallRhs(e.Tokens[p], r, e.Tokens[p].val, e.Arguments);
+ r = null;
+ } else {
+ r = new FunctionCallExpr(e.Tokens[p], e.Tokens[p].val, r, e.OpenParen, e.Arguments);
+ ResolveExpression(r, twoState, null);
+ }
+ } else if (e.Arguments != null) {
+ Contract.Assert(p == e.Tokens.Count);
+ Error(e.OpenParen, "non-function expression is called with parameters");
+ // resolve the arguments nonetheless
+ foreach (var arg in e.Arguments) {
+ ResolveExpression(arg, twoState);
+ }
+ }
+ return r;
+ }
+
+ /// <summary>
+ /// Resolves "obj . suffixName" to either a parameter-less predicate invocation or a field selection.
+ /// Expects "obj" already to have been resolved.
+ /// On success, returns the result of the resolution--as an un-resolved expression.
+ /// On failure, returns null (in which case an error has been reported to the user).
+ /// </summary>
+ Expression/*?*/ ResolvePredicateOrField(IToken tok, Expression obj, string suffixName) {
+ Contract.Requires(tok != null);
+ Contract.Requires(obj != null);
+ Contract.Requires(obj.Type != null); // obj is expected already to have been resolved
+ Contract.Requires(suffixName != null);
+
+ NonProxyType nptype;
+ MemberDecl member = ResolveMember(tok, obj.Type, suffixName, out nptype);
+ if (member == null) {
+ // error has already been reported by ResolveMember
+ return null;
+ } else if (member is Predicate && ((Predicate)member).Formals.Count == 0) {
+ // parameter-less predicates are allowed to be used without parentheses
+ return new FunctionCallExpr(tok, suffixName, obj, null, new List<Expression>());
+ } else {
+ // assume it's a field and let the resolution of the FieldSelectExpr check any further problems
+ return new FieldSelectExpr(tok, obj, suffixName);
+ }
+ }
+
+ /// <summary>
+ /// Tries to find a bounded pool for each of the bound variables "bvars" of "expr". If this process
+ /// fails, then "null" is returned and the bound variables for which the process fails are added to "missingBounds".
+ /// If "returnAllBounds" is false, then:
+ /// -- at most one BoundedPool per variable is returned
+ /// -- every IntBoundedPool returned has both a lower and an upper bound
+ /// -- no SuperSetBoundedPool is returned
+ /// If "returnAllBounds" is true, then:
+ /// -- a variable may give rise to several BoundedPool's
+ /// -- IntBoundedPool bounds may have just one component
+ /// -- a non-null return value means that some bound were found for each variable (but, for example, perhaps one
+ /// variable only has lower bounds, no upper bounds)
+ /// Requires "expr" to be successfully resolved.
+ /// </summary>
+ public static List<ComprehensionExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, bool returnAllBounds, List<BoundVar> missingBounds) {
+ Contract.Requires(tok != null);
+ Contract.Requires(bvars != null);
+ Contract.Requires(missingBounds != null);
+ Contract.Requires(expr != null);
+ Contract.Requires(expr.Type != null); // a sanity check (but not a complete proof) that "expr" has been resolved
+ Contract.Ensures(
+ (returnAllBounds && Contract.OldValue(missingBounds.Count) <= missingBounds.Count) ||
+ (!returnAllBounds &&
+ Contract.Result<List<ComprehensionExpr.BoundedPool>>() != null &&
+ Contract.Result<List<ComprehensionExpr.BoundedPool>>().Count == bvars.Count &&
+ Contract.OldValue(missingBounds.Count) == missingBounds.Count) ||
+ (!returnAllBounds &&
+ Contract.Result<List<ComprehensionExpr.BoundedPool>>() == null &&
+ Contract.OldValue(missingBounds.Count) < missingBounds.Count));
+
+ var bounds = new List<ComprehensionExpr.BoundedPool>();
+ bool foundError = false;
+ for (int j = 0; j < bvars.Count; j++) {
+ var bv = bvars[j];
+ if (bv.Type is BoolType) {
+ // easy
+ bounds.Add(new ComprehensionExpr.BoolBoundedPool());
+ } else if (bv.Type.IsIndDatatype && (bv.Type.AsIndDatatype).HasFinitePossibleValues) {
+ bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));
+ } else {
+ // Go through the conjuncts of the range expression to look for bounds.
+ Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;
+ Expression upperBound = null;
+ bool foundBoundsForBv = false;
+ if (returnAllBounds && lowerBound != null) {
+ bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));
+ lowerBound = null;
+ foundBoundsForBv = true;
+ }
+ foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {
+ var c = conjunct as BinaryExpr;
+ if (c == null) {
+ goto CHECK_NEXT_CONJUNCT;
+ }
+ var e0 = c.E0;
+ var e1 = c.E1;
+ int whereIsBv = SanitizeForBoundDiscovery(bvars, j, c.ResolvedOp, ref e0, ref e1);
+ if (whereIsBv < 0) {
+ goto CHECK_NEXT_CONJUNCT;
+ }
+ switch (c.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.InSet:
+ if (whereIsBv == 0) {
+ bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.Subset:
+ if (returnAllBounds && whereIsBv == 1) {
+ bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(e0));
+ foundBoundsForBv = true;
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.InMultiSet:
+ if (whereIsBv == 0) {
+ bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.InSeq:
+ if (whereIsBv == 0) {
+ bounds.Add(new ComprehensionExpr.SeqBoundedPool(e1));
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.InMap:
+ if (whereIsBv == 0) {
+ bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.EqCommon:
+ if (bv.Type is IntType) {
+ var otherOperand = whereIsBv == 0 ? e1 : e0;
+ bounds.Add(new ComprehensionExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
+ } else if (returnAllBounds && bv.Type is SetType) {
+ var otherOperand = whereIsBv == 0 ? e1 : e0;
+ bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(otherOperand));
+ foundBoundsForBv = true;
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.Gt:
+ case BinaryExpr.ResolvedOpcode.Ge:
+ Contract.Assert(false); throw new cce.UnreachableException(); // promised by postconditions of NormalizedConjunct
+ case BinaryExpr.ResolvedOpcode.Lt:
+ if (whereIsBv == 0 && upperBound == null) {
+ upperBound = e1; // bv < E
+ } else if (whereIsBv == 1 && lowerBound == null) {
+ lowerBound = Plus(e0, 1); // E < bv
+ }
+ break;
+ case BinaryExpr.ResolvedOpcode.Le:
+ if (whereIsBv == 0 && upperBound == null) {
+ upperBound = Plus(e1, 1); // bv <= E
+ } else if (whereIsBv == 1 && lowerBound == null) {
+ lowerBound = e0; // E <= bv
+ }
+ break;
+ default:
+ break;
+ }
+ if ((lowerBound != null && upperBound != null) ||
+ (returnAllBounds && (lowerBound != null || upperBound != null))) {
+ // we have found two halves (or, in the case of returnAllBounds, we have found some bound)
+ bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));
+ lowerBound = null;
+ upperBound = null;
+ foundBoundsForBv = true;
+ if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;
+ }
+ CHECK_NEXT_CONJUNCT: ;
+ }
+ if (!foundBoundsForBv) {
+ // we have checked every conjunct in the range expression and still have not discovered good bounds
+ missingBounds.Add(bv); // record failing bound variable
+ foundError = true;
+ }
+ }
+ CHECK_NEXT_BOUND_VARIABLE: ; // should goto here only if the bound for the current variable has been discovered (otherwise, return with null from this method)
+ }
+ return foundError ? null : bounds;
+ }
+
+ /// <summary>
+ /// If the return value is negative, the resulting "e0" and "e1" should not be used.
+ /// Otherwise, the following is true on return:
+ /// The new "e0 op e1" is equivalent to the old "e0 op e1".
+ /// One of "e0" and "e1" is the identifier "boundVars[bvi]"; the return value is either 0 or 1, and indicates which.
+ /// The other of "e0" and "e1" is an expression whose free variables are not among "boundVars[bvi..]".
+ /// Ensures that the resulting "e0" and "e1" are not ConcreteSyntaxExpression's.
+ /// </summary>
+ static int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Requires(boundVars != null);
+ Contract.Requires(0 <= bvi && bvi < boundVars.Count);
+ Contract.Ensures(Contract.Result<int>() < 2);
+ Contract.Ensures(!(Contract.ValueAtReturn(out e0) is ConcreteSyntaxExpression));
+ Contract.Ensures(!(Contract.ValueAtReturn(out e1) is ConcreteSyntaxExpression));
+
+ var bv = boundVars[bvi];
+ e0 = e0.Resolved;
+ e1 = e1.Resolved;
+
+ // make an initial assessment of where bv is; to continue, we need bv to appear in exactly one operand
+ var fv0 = FreeVariables(e0);
+ var fv1 = FreeVariables(e1);
+ Expression thisSide;
+ Expression thatSide;
+ int whereIsBv;
+ if (fv0.Contains(bv)) {
+ if (fv1.Contains(bv)) {
+ return -1;
+ }
+ whereIsBv = 0;
+ thisSide = e0; thatSide = e1;
+ } else if (fv1.Contains(bv)) {
+ whereIsBv = 1;
+ thisSide = e1; thatSide = e0;
+ } else {
+ return -1;
+ }
+
+ // Next, clean up the side where bv is by adjusting both sides of the expression
+ switch (op) {
+ case BinaryExpr.ResolvedOpcode.EqCommon:
+ case BinaryExpr.ResolvedOpcode.NeqCommon:
+ case BinaryExpr.ResolvedOpcode.Gt:
+ case BinaryExpr.ResolvedOpcode.Ge:
+ case BinaryExpr.ResolvedOpcode.Le:
+ case BinaryExpr.ResolvedOpcode.Lt:
+ // Repeatedly move additive or subtractive terms from thisSide to thatSide
+ while (true) {
+ var bin = thisSide as BinaryExpr;
+ if (bin == null) {
+ break; // done simplifying
+
+ } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add) {
+ // Change "A+B op C" into either "A op C-B" or "B op C-A", depending on where we find bv among A and B.
+ if (!FreeVariables(bin.E1).Contains(bv)) {
+ thisSide = bin.E0.Resolved;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E1);
+ } else {
+ thisSide = bin.E1.Resolved;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, thatSide, bin.E0);
+ }
+ ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
+ thatSide.Type = bin.Type;
+
+ } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub) {
+ // Change "A-B op C" in a similar way.
+ if (!FreeVariables(bin.E1).Contains(bv)) {
+ // change to "A op C+B"
+ thisSide = bin.E0.Resolved;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Add, thatSide, bin.E1);
+ ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Add;
+ } else {
+ // In principle, change to "-B op C-A" and then to "B dualOp A-C". But since we don't want
+ // to change "op", we instead end with "A-C op B" and switch the mapping of thisSide/thatSide
+ // to e0/e1 (by inverting "whereIsBv").
+ thisSide = bin.E1.Resolved;
+ thatSide = new BinaryExpr(bin.tok, BinaryExpr.Opcode.Sub, bin.E0, thatSide);
+ ((BinaryExpr)thatSide).ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
+ whereIsBv = 1 - whereIsBv;
+ }
+ thatSide.Type = bin.Type;
+
+ } else {
+ break; // done simplifying
+ }
+ }
+ break;
+
+ default:
+ break;
+ }
+
+ // Now, see if the interesting side is simply bv itself
+ if (thisSide is IdentifierExpr && ((IdentifierExpr)thisSide).Var == bv) {
+ // we're cool
+ } else {
+ // no, the situation is more complicated than we care to understand
+ return -1;
+ }
+
+ // Finally, check that the other side does not contain "bv" or any of the bound variables
+ // listed after "bv" in the quantifier.
+ var fv = FreeVariables(thatSide);
+ for (int i = bvi; i < boundVars.Count; i++) {
+ if (fv.Contains(boundVars[i])) {
+ return -1;
+ }
+ }
+
+ // As we return, also return the adjusted sides
+ if (whereIsBv == 0) {
+ e0 = thisSide; e1 = thatSide;
+ } else {
+ e0 = thatSide; e1 = thisSide;
+ }
+ return whereIsBv;
+ }
+
+ /// <summary>
+ /// Returns all conjuncts of "expr" in "polarity" positions. That is, if "polarity" is "true", then
+ /// returns the conjuncts of "expr" in positive positions; else, returns the conjuncts of "expr" in
+ /// negative positions. The method considers a canonical-like form of the expression that pushes
+ /// negations inwards far enough that one can determine what the result is going to be (so, almost
+ /// a negation normal form).
+ /// As a convenience, arithmetic inequalities are rewritten so that the negation of an arithmetic
+ /// inequality is never returned and the comparisons > and >= are never returned; the negation of
+ /// a common equality or disequality is rewritten analogously.
+ /// Requires "expr" to be successfully resolved.
+ /// Ensures that what is returned is not a ConcreteSyntaxExpression.
+ /// </summary>
+ static IEnumerable<Expression> NormalizedConjuncts(Expression expr, bool polarity) {
+ // We consider 5 cases. To describe them, define P(e)=Conjuncts(e,true) and N(e)=Conjuncts(e,false).
+ // * X ==> Y is treated as a shorthand for !X || Y, and so is described by the remaining cases
+ // * X && Y P(_) = P(X),P(Y) and N(_) = !(X && Y)
+ // * X || Y P(_) = (X || Y) and N(_) = N(X),N(Y)
+ // * !X P(_) = N(X) and N(_) = P(X)
+ // * else P(_) = else and N(_) = !else
+ // So for ==>, we have:
+ // * X ==> Y P(_) = P(!X || Y) = (!X || Y) = (X ==> Y)
+ // N(_) = N(!X || Y) = N(!X),N(Y) = P(X),N(Y)
+ expr = expr.Resolved;
+
+ // Binary expressions
+ var b = expr as BinaryExpr;
+ if (b != null) {
+ bool breakDownFurther = false;
+ bool p0 = polarity;
+ if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
+ breakDownFurther = polarity;
+ } else if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {
+ breakDownFurther = !polarity;
+ } else if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
+ breakDownFurther = !polarity;
+ p0 = !p0;
+ }
+ if (breakDownFurther) {
+ foreach (var c in NormalizedConjuncts(b.E0, p0)) {
+ yield return c;
+ }
+ foreach (var c in NormalizedConjuncts(b.E1, polarity)) {
+ yield return c;
+ }
+ yield break;
+ }
+ }
+
+ // Unary expression
+ var u = expr as UnaryExpr;
+ if (u != null && u.Op == UnaryExpr.Opcode.Not) {
+ foreach (var c in NormalizedConjuncts(u.E, !polarity)) {
+ yield return c;
+ }
+ yield break;
+ }
+
+ // no other case applied, so return the expression or its negation, but first clean it up a little
+ b = expr as BinaryExpr;
+ if (b != null) {
+ BinaryExpr.Opcode newOp;
+ BinaryExpr.ResolvedOpcode newROp;
+ bool swapOperands;
+ switch (b.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.Gt: // A > B yield polarity ? (B < A) : (A <= B);
+ newOp = polarity ? BinaryExpr.Opcode.Lt : BinaryExpr.Opcode.Le;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.Lt : BinaryExpr.ResolvedOpcode.Le;
+ swapOperands = polarity;
+ break;
+ case BinaryExpr.ResolvedOpcode.Ge: // A >= B yield polarity ? (B <= A) : (A < B);
+ newOp = polarity ? BinaryExpr.Opcode.Le : BinaryExpr.Opcode.Lt;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.Le : BinaryExpr.ResolvedOpcode.Lt;
+ swapOperands = polarity;
+ break;
+ case BinaryExpr.ResolvedOpcode.Le: // A <= B yield polarity ? (A <= B) : (B < A);
+ newOp = polarity ? BinaryExpr.Opcode.Le : BinaryExpr.Opcode.Lt;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.Le : BinaryExpr.ResolvedOpcode.Lt;
+ swapOperands = !polarity;
+ break;
+ case BinaryExpr.ResolvedOpcode.Lt: // A < B yield polarity ? (A < B) : (B <= A);
+ newOp = polarity ? BinaryExpr.Opcode.Lt : BinaryExpr.Opcode.Le;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.Lt : BinaryExpr.ResolvedOpcode.Le;
+ swapOperands = !polarity;
+ break;
+ case BinaryExpr.ResolvedOpcode.EqCommon: // A == B yield polarity ? (A == B) : (A != B);
+ newOp = polarity ? BinaryExpr.Opcode.Eq : BinaryExpr.Opcode.Neq;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.EqCommon : BinaryExpr.ResolvedOpcode.NeqCommon;
+ swapOperands = false;
+ break;
+ case BinaryExpr.ResolvedOpcode.NeqCommon: // A != B yield polarity ? (A != B) : (A == B);
+ newOp = polarity ? BinaryExpr.Opcode.Neq : BinaryExpr.Opcode.Eq;
+ newROp = polarity ? BinaryExpr.ResolvedOpcode.NeqCommon : BinaryExpr.ResolvedOpcode.EqCommon;
+ swapOperands = false;
+ break;
+ default:
+ goto JUST_RETURN_IT;
+ }
+ if (newROp != b.ResolvedOp || swapOperands) {
+ b = new BinaryExpr(b.tok, newOp, swapOperands ? b.E1 : b.E0, swapOperands ? b.E0 : b.E1);
+ b.ResolvedOp = newROp;
+ b.Type = Type.Bool;
+ yield return b;
+ yield break;
+ }
+ }
+ JUST_RETURN_IT: ;
+ if (polarity) {
+ yield return expr;
+ } else {
+ expr = new UnaryExpr(expr.tok, UnaryExpr.Opcode.Not, expr);
+ expr.Type = Type.Bool;
+ yield return expr;
+ }
+ }
+
+ public static Expression Plus(Expression e, int n) {
+ Contract.Requires(0 <= n);
+
+ var nn = new LiteralExpr(e.tok, n);
+ nn.Type = Type.Int;
+ var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Add, e, nn);
+ p.ResolvedOp = BinaryExpr.ResolvedOpcode.Add;
+ p.Type = Type.Int;
+ return p;
+ }
+
+ public static Expression Minus(Expression e, int n) {
+ Contract.Requires(0 <= n);
+
+ var nn = new LiteralExpr(e.tok, n);
+ nn.Type = Type.Int;
+ var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Sub, e, nn);
+ p.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
+ p.Type = Type.Int;
+ return p;
+ }
+
+ /// <summary>
+ /// Returns the set of free variables in "expr".
+ /// Requires "expr" to be successfully resolved.
+ /// Ensures that the set returned has no aliases.
+ /// </summary>
+ static ISet<IVariable> FreeVariables(Expression expr) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(expr.Type != null);
+
+ if (expr is IdentifierExpr) {
+ var e = (IdentifierExpr)expr;
+ return new HashSet<IVariable>() { e.Var };
+
+ } else if (expr is QuantifierExpr) {
+ var e = (QuantifierExpr)expr;
+ var s = FreeVariables(e.LogicalBody());
+ foreach (var bv in e.BoundVars) {
+ s.Remove(bv);
+ }
+ return s;
+
+ } else if (expr is MatchExpr) {
+ var e = (MatchExpr)expr;
+ var s = FreeVariables(e.Source);
+ foreach (MatchCaseExpr mc in e.Cases) {
+ var t = FreeVariables(mc.Body);
+ foreach (var bv in mc.Arguments) {
+ t.Remove(bv);
+ }
+ s.UnionWith(t);
+ }
+ return s;
+
+ } else {
+ ISet<IVariable> s = null;
+ foreach (var e in expr.SubExpressions) {
+ var t = FreeVariables(e);
+ if (s == null) {
+ s = t;
+ } else {
+ s.UnionWith(t);
+ }
+ }
+ return s == null ? new HashSet<IVariable>() : s;
+ }
+ }
+
+ void ResolveReceiver(Expression expr, bool twoState) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(expr.Type != null);
+
+ if (expr is ThisExpr && !expr.WasResolved()) {
+ // Allow 'this' here, regardless of scope.AllowInstance. The caller is responsible for
+ // making sure 'this' does not really get used when it's not available.
+ Contract.Assume(currentClass != null); // this is really a precondition, in this case
+ expr.Type = GetThisType(expr.tok, currentClass);
+ } else {
+ ResolveExpression(expr, twoState);
+ }
+ }
+
+ void ResolveSeqSelectExpr(SeqSelectExpr e, bool twoState, bool allowNonUnitArraySelection) {
+ Contract.Requires(e != null);
+ if (e.Type != null) {
+ // already resolved
+ return;
+ }
+
+ bool seqErr = false;
+ ResolveExpression(e.Seq, twoState);
+ Contract.Assert(e.Seq.Type != null); // follows from postcondition of ResolveExpression
+ Type elementType = new InferredTypeProxy();
+ Type domainType = new InferredTypeProxy();
+
+ IndexableTypeProxy expectedType = new IndexableTypeProxy(elementType, domainType);
+ if (!UnifyTypes(e.Seq.Type, expectedType)) {
+ Error(e, "sequence/array/map selection requires a sequence, array or map (got {0})", e.Seq.Type);
+ seqErr = true;
+ }
+ if (!e.SelectOne) // require sequence or array
+ {
+ if (!allowNonUnitArraySelection) {
+ // require seq
+ if (!UnifyTypes(expectedType, new SeqType(new InferredTypeProxy()))) {
+ Error(e, "selection requires a sequence (got {0})", e.Seq.Type);
+ }
+ } else {
+ if (UnifyTypes(expectedType, new MapType(new InferredTypeProxy(), new InferredTypeProxy()))) {
+ Error(e, "cannot multiselect a map (got {0} as map type)", e.Seq.Type);
+ }
+ }
+ }
+ if (e.E0 != null) {
+ ResolveExpression(e.E0, twoState);
+ Contract.Assert(e.E0.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.E0.Type, domainType)) {
+ Error(e.E0, "sequence/array/map selection requires {1} indices (got {0})", e.E0.Type, domainType);
+ }
+ }
+ if (e.E1 != null) {
+ ResolveExpression(e.E1, twoState);
+ Contract.Assert(e.E1.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.E1.Type, domainType)) {
+ Error(e.E1, "sequence/array/map selection requires {1} indices (got {0})", e.E1.Type, domainType);
+ }
+ }
+ if (!seqErr) {
+ if (e.SelectOne) {
+ e.Type = elementType;
+ } else {
+ e.Type = new SeqType(elementType);
+ }
+ }
+ }
+
+ /// <summary>
+ /// Note: this method is allowed to be called even if "type" does not make sense for "op", as might be the case if
+ /// resolution of the binary expression failed. If so, an arbitrary resolved opcode is returned.
+ /// </summary>
+ BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, Type operandType) {
+ Contract.Requires(operandType != null);
+ switch (op) {
+ case BinaryExpr.Opcode.Iff: return BinaryExpr.ResolvedOpcode.Iff;
+ case BinaryExpr.Opcode.Imp: return BinaryExpr.ResolvedOpcode.Imp;
+ case BinaryExpr.Opcode.And: return BinaryExpr.ResolvedOpcode.And;
+ case BinaryExpr.Opcode.Or: return BinaryExpr.ResolvedOpcode.Or;
+ case BinaryExpr.Opcode.Eq:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.SetEq;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetEq;
+ } else if (operandType is SeqType) {
+ return BinaryExpr.ResolvedOpcode.SeqEq;
+ } else if (operandType is MapType) {
+ return BinaryExpr.ResolvedOpcode.MapEq;
+ } else {
+ return BinaryExpr.ResolvedOpcode.EqCommon;
+ }
+ case BinaryExpr.Opcode.Neq:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.SetNeq;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetNeq;
+ } else if (operandType is SeqType) {
+ return BinaryExpr.ResolvedOpcode.SeqNeq;
+ } else if (operandType is MapType) {
+ return BinaryExpr.ResolvedOpcode.MapNeq;
+ } else {
+ return BinaryExpr.ResolvedOpcode.NeqCommon;
+ }
+ case BinaryExpr.Opcode.Disjoint:
+ if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetDisjoint;
+ } else if (operandType is MapType) {
+ return BinaryExpr.ResolvedOpcode.MapDisjoint;
+ } else {
+ return BinaryExpr.ResolvedOpcode.Disjoint;
+ }
+ case BinaryExpr.Opcode.Lt:
+ if (operandType.IsIndDatatype || operandType is DatatypeProxy) {
+ return BinaryExpr.ResolvedOpcode.RankLt;
+ } else if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.ProperSubset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.ProperMultiSubset;
+ } else if (operandType is SeqType) {
+ return BinaryExpr.ResolvedOpcode.ProperPrefix;
+ } else {
+ return BinaryExpr.ResolvedOpcode.Lt;
+ }
+ case BinaryExpr.Opcode.Le:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.Subset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSubset;
+ } else if (operandType is SeqType) {
+ return BinaryExpr.ResolvedOpcode.Prefix;
+ } else {
+ return BinaryExpr.ResolvedOpcode.Le;
+ }
+ case BinaryExpr.Opcode.Add:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.Union;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetUnion;
+ } else if (operandType is MapType) {
+ return BinaryExpr.ResolvedOpcode.MapUnion;
+ } else if (operandType is SeqType) {
+ return BinaryExpr.ResolvedOpcode.Concat;
+ } else {
+ return BinaryExpr.ResolvedOpcode.Add;
+ }
+ case BinaryExpr.Opcode.Sub:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.SetDifference;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetDifference;
+ } else {
+ return BinaryExpr.ResolvedOpcode.Sub;
+ }
+ case BinaryExpr.Opcode.Mul:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.Intersection;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSetIntersection;
+ } else {
+ return BinaryExpr.ResolvedOpcode.Mul;
+ }
+ case BinaryExpr.Opcode.Gt:
+ if (operandType.IsDatatype) {
+ return BinaryExpr.ResolvedOpcode.RankGt;
+ } else if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.ProperSuperset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.ProperMultiSuperset;
+ } else {
+ return BinaryExpr.ResolvedOpcode.Gt;
+ }
+ case BinaryExpr.Opcode.Ge:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.Superset;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.MultiSuperset;
+ } else {
+ return BinaryExpr.ResolvedOpcode.Ge;
+ }
+ case BinaryExpr.Opcode.In:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.InSet;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.InMultiSet;
+ } else if (operandType is MapType) {
+ return BinaryExpr.ResolvedOpcode.InMap;
+ } else {
+ return BinaryExpr.ResolvedOpcode.InSeq;
+ }
+ case BinaryExpr.Opcode.NotIn:
+ if (operandType is SetType) {
+ return BinaryExpr.ResolvedOpcode.NotInSet;
+ } else if (operandType is MultiSetType) {
+ return BinaryExpr.ResolvedOpcode.NotInMultiSet;
+ } else if (operandType is MapType) {
+ return BinaryExpr.ResolvedOpcode.NotInMap;
+ } else {
+ return BinaryExpr.ResolvedOpcode.NotInSeq;
+ }
+ case BinaryExpr.Opcode.Div: return BinaryExpr.ResolvedOpcode.Div;
+ case BinaryExpr.Opcode.Mod: return BinaryExpr.ResolvedOpcode.Mod;
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected operator
+ }
+ }
+
+ /// <summary>
+ /// Returns whether or not 'expr' has any subexpression that uses some feature (like a ghost or quantifier)
+ /// that is allowed only in specification contexts.
+ /// Requires 'expr' to be a successfully resolved expression.
+ /// </summary>
+ bool UsesSpecFeatures(Expression expr) {
+ Contract.Requires(expr != null);
+ Contract.Requires(expr.WasResolved()); // this check approximates the requirement that "expr" be resolved
+
+ if (expr is LiteralExpr) {
+ return false;
+ } else if (expr is ThisExpr) {
+ return false;
+ } else if (expr is IdentifierExpr) {
+ IdentifierExpr e = (IdentifierExpr)expr;
+ return cce.NonNull(e.Var).IsGhost;
+ } else if (expr is DatatypeValue) {
+ DatatypeValue dtv = (DatatypeValue)expr;
+ return dtv.Arguments.Exists(arg => UsesSpecFeatures(arg));
+ } else if (expr is DisplayExpression) {
+ DisplayExpression e = (DisplayExpression)expr;
+ return e.Elements.Exists(ee => UsesSpecFeatures(ee));
+ } else if (expr is MapDisplayExpr) {
+ MapDisplayExpr e = (MapDisplayExpr)expr;
+ return e.Elements.Exists(p => UsesSpecFeatures(p.A) || UsesSpecFeatures(p.B));
+ } else if (expr is FieldSelectExpr) {
+ FieldSelectExpr e = (FieldSelectExpr)expr;
+ return cce.NonNull(e.Field).IsGhost || UsesSpecFeatures(e.Obj);
+ } else if (expr is SeqSelectExpr) {
+ SeqSelectExpr e = (SeqSelectExpr)expr;
+ return UsesSpecFeatures(e.Seq) ||
+ (e.E0 != null && UsesSpecFeatures(e.E0)) ||
+ (e.E1 != null && UsesSpecFeatures(e.E1));
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr e = (MultiSelectExpr)expr;
+ return UsesSpecFeatures(e.Array) || e.Indices.Exists(ee => UsesSpecFeatures(ee));
+ } else if (expr is SeqUpdateExpr) {
+ SeqUpdateExpr e = (SeqUpdateExpr)expr;
+ return UsesSpecFeatures(e.Seq) ||
+ (e.Index != null && UsesSpecFeatures(e.Index)) ||
+ (e.Value != null && UsesSpecFeatures(e.Value));
+ } else if (expr is FunctionCallExpr) {
+ FunctionCallExpr e = (FunctionCallExpr)expr;
+ if (cce.NonNull(e.Function).IsGhost) {
+ return true;
+ }
+ return e.Args.Exists(arg => UsesSpecFeatures(arg));
+ } else if (expr is OldExpr) {
+ OldExpr e = (OldExpr)expr;
+ return UsesSpecFeatures(e.E);
+ } else if (expr is FreshExpr) {
+ return true;
+ } else if (expr is UnaryExpr) {
+ UnaryExpr e = (UnaryExpr)expr;
+ return UsesSpecFeatures(e.E);
+ } else if (expr is BinaryExpr) {
+ BinaryExpr e = (BinaryExpr)expr;
+ if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.RankLt || e.ResolvedOp == BinaryExpr.ResolvedOpcode.RankGt) {
+ return true;
+ }
+ return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1);
+ } else if (expr is NamedExpr) {
+ return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body);
+ } else if (expr is ComprehensionExpr) {
+ if (expr is QuantifierExpr && ((QuantifierExpr)expr).Bounds == null) {
+ return true; // the quantifier cannot be compiled if the resolver found no bounds
+ }
+ return Contract.Exists(expr.SubExpressions, se => UsesSpecFeatures(se));
+ } else if (expr is SetComprehension) {
+ var e = (SetComprehension)expr;
+ return (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
+ } else if (expr is MapComprehension) {
+ var e = (MapComprehension)expr;
+ return (UsesSpecFeatures(e.Range)) || (UsesSpecFeatures(e.Term));
+ } else if (expr is WildcardExpr) {
+ return false;
+ } else if (expr is PredicateExpr) {
+ var e = (PredicateExpr)expr;
+ return UsesSpecFeatures(e.Body);
+ } else if (expr is ITEExpr) {
+ ITEExpr e = (ITEExpr)expr;
+ return UsesSpecFeatures(e.Test) || UsesSpecFeatures(e.Thn) || UsesSpecFeatures(e.Els);
+ } else if (expr is MatchExpr) {
+ MatchExpr me = (MatchExpr)expr;
+ if (UsesSpecFeatures(me.Source)) {
+ return true;
+ }
+ return me.Cases.Exists(mc => UsesSpecFeatures(mc.Body));
+ } else if (expr is ConcreteSyntaxExpression) {
+ var e = (ConcreteSyntaxExpression)expr;
+ return e.ResolvedExpression != null && UsesSpecFeatures(e.ResolvedExpression);
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
+ }
+ }
+ }
+
+ class CoCallResolution
+ {
+ readonly ModuleDefinition currentModule;
+ readonly Function currentFunction;
+ readonly bool dealsWithCodatatypes;
+
+ public CoCallResolution(Function currentFunction, bool dealsWithCodatatypes) {
+ Contract.Requires(currentFunction != null);
+ this.currentModule = currentFunction.EnclosingClass.Module;
+ this.currentFunction = currentFunction;
+ this.dealsWithCodatatypes = dealsWithCodatatypes;
+ }
+
+ /// <summary>
+ /// Determines which calls in "expr" can be considered to be co-calls, which co-constructor
+ /// invocations host such co-calls, and which destructor operations are not allowed.
+ /// Assumes "expr" to have been successfully resolved.
+ /// </summary>
+ public void CheckCoCalls(Expression expr) {
+ Contract.Requires(expr != null);
+ var candidates = CheckCoCalls(expr, true, null);
+ ProcessCoCallInfo(candidates);
+ }
+
+ struct CoCallInfo
+ {
+ public int GuardCount;
+ public FunctionCallExpr CandidateCall;
+ public DatatypeValue EnclosingCoConstructor;
+ public CoCallInfo(int guardCount, FunctionCallExpr candidateCall, DatatypeValue enclosingCoConstructor) {
+ Contract.Requires(0 <= guardCount);
+ Contract.Requires(candidateCall != null);
+
+ GuardCount = guardCount;
+ CandidateCall = candidateCall;
+ EnclosingCoConstructor = enclosingCoConstructor;
+ }
+
+ public void AdjustGuardCount(int p) {
+ GuardCount += p;
+ }
+ }
+
+ /// <summary>
+ /// Recursively goes through the entire "expr". Every call within the same recursive cluster is a potential
+ /// co-call. All such calls will get their .CoCall field filled in, indicating whether or not the call
+ /// is a co-call. If the situation deals with co-datatypes, then one of the NoBecause... values is chosen (rather
+ /// than just No), so that any error message that may later be produced when trying to prove termination of the
+ /// recursive call can include a note pointing out that the call was not selected to be a co-call.
+ /// "allowCallsWithinRecursiveCluster" is passed in as "false" if the enclosing context has no easy way of
+ /// controlling the uses of "expr" (for example, if the enclosing context passes "expr" to a function or binds
+ /// "expr" to a variable).
+ /// </summary>
+ List<CoCallInfo> CheckCoCalls(Expression expr, bool allowCallsWithinRecursiveCluster, DatatypeValue coContext) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(allowCallsWithinRecursiveCluster || Contract.Result<List<CoCallInfo>>().Count == 0);
+
+ var candidates = new List<CoCallInfo>();
+ expr = expr.Resolved;
+ if (expr is DatatypeValue) {
+ var e = (DatatypeValue)expr;
+ if (e.Ctor.EnclosingDatatype is CoDatatypeDecl) {
+ foreach (var arg in e.Arguments) {
+ foreach (var c in CheckCoCalls(arg, allowCallsWithinRecursiveCluster, e)) {
+ c.AdjustGuardCount(1);
+ candidates.Add(c);
+ }
+ }
+ return candidates;
+ }
+ } else if (expr is FieldSelectExpr) {
+ var e = (FieldSelectExpr)expr;
+ if (e.Field.EnclosingClass is CoDatatypeDecl) {
+ foreach (var c in CheckCoCalls(e.Obj, allowCallsWithinRecursiveCluster, null)) {
+ if (c.GuardCount <= 1) {
+ // This call was not guarded (c.GuardedCount == 0) or the guard for this candidate co-call is
+ // being removed (c.GuardedCount == 1), so this call is not allowed as a co-call.
+ // (So, don't include "res" among "results".)
+ c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
+ } else {
+ c.AdjustGuardCount(-1);
+ candidates.Add(c);
+ }
+ }
+ return candidates;
+ }
+ } else if (expr is MatchExpr) {
+ var e = (MatchExpr)expr;
+ var r = CheckCoCalls(e.Source, false, null);
+ Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls
+ foreach (var kase in e.Cases) {
+ r = CheckCoCalls(kase.Body, allowCallsWithinRecursiveCluster, null);
+ candidates.AddRange(r);
+ }
+ return candidates;
+ } else if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ // First, consider the arguments of the call, making sure that they do not include calls within the recursive cluster.
+ // (Note, if functions could have a "destruction level" declaration that promised to only destruct its arguments by
+ // so much, then some recursive calls within the cluster could be allowed.)
+ foreach (var arg in e.Args) {
+ var r = CheckCoCalls(arg, false, null);
+ Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls
+ }
+ // Second, investigate the possibility that this call itself may be a candidate co-call
+ if (currentModule.CallGraph.GetSCCRepresentative(currentFunction) == currentModule.CallGraph.GetSCCRepresentative(e.Function)) {
+ // This call goes to another function in the same recursive cluster
+ if (e.Function.Reads.Count != 0) {
+ // this call is disqualified from being a co-call, because of side effects
+ if (!dealsWithCodatatypes) {
+ e.CoCall = FunctionCallExpr.CoCallResolution.No;
+ } else if (coContext != null) {
+ e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects;
+ } else {
+ e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
+ }
+ } else if (!allowCallsWithinRecursiveCluster) {
+ if (!dealsWithCodatatypes) {
+ e.CoCall = FunctionCallExpr.CoCallResolution.No;
+ } else {
+ e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsAreNotAllowedInThisContext;
+ }
+ } else {
+ // e.CoCall is not filled in here, but will be filled in when the list of candidates are processed
+ candidates.Add(new CoCallInfo(0, e, coContext));
+ }
+ }
+ return candidates;
+ } else if (expr is OldExpr) {
+ var e = (OldExpr)expr;
+ // here, "coContext" is passed along (the use of "old" says this must be ghost code, so the compiler does not need to handle this case)
+ return CheckCoCalls(e.E, allowCallsWithinRecursiveCluster, coContext);
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ foreach (var rhs in e.RHSs) {
+ var r = CheckCoCalls(rhs, false, null);
+ Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls
+ }
+ return CheckCoCalls(e.Body, allowCallsWithinRecursiveCluster, null);
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ foreach (var ee in e.SubExpressions) {
+ var r = CheckCoCalls(ee, false, null);
+ Contract.Assert(r.Count == 0); // follows from postcondition of CheckCoCalls
+ }
+ return candidates;
+ }
+
+ // Default handling:
+ foreach (var ee in expr.SubExpressions) {
+ var r = CheckCoCalls(ee, allowCallsWithinRecursiveCluster, null);
+ candidates.AddRange(r);
+ }
+ if (expr.Type is BasicType) {
+ // nothing can escape this expression, so process the results now
+ ProcessCoCallInfo(candidates);
+ candidates.Clear();
+ }
+ return candidates;
+ }
+
+ /// <summary>
+ /// This method is to be called when it has been determined that all candidate
+ /// co-calls in "info" are indeed allowed as co-calls.
+ /// </summary>
+ void ProcessCoCallInfo(List<CoCallInfo> coCandidates) {
+ foreach (var c in coCandidates) {
+ if (c.GuardCount != 0) {
+ c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.Yes;
+ c.EnclosingCoConstructor.IsCoCall = true;
+ } else if (dealsWithCodatatypes) {
+ c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded;
+ } else {
+ c.CandidateCall.CoCall = FunctionCallExpr.CoCallResolution.No;
+ }
+ }
+ }
+ }
+
+ class Scope<Thing> where Thing : class
+ {
+ [Rep]
+ readonly List<string> names = new List<string>(); // a null means a marker
+ [Rep]
+ readonly List<Thing> things = new List<Thing>();
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(names != null);
+ Contract.Invariant(things != null);
+ Contract.Invariant(names.Count == things.Count);
+ Contract.Invariant(-1 <= scopeSizeWhereInstancesWereDisallowed && scopeSizeWhereInstancesWereDisallowed <= names.Count);
+ }
+
+ int scopeSizeWhereInstancesWereDisallowed = -1;
+
+ public bool AllowInstance {
+ get { return scopeSizeWhereInstancesWereDisallowed == -1; }
+ set {
+ Contract.Requires(AllowInstance && !value); // only allowed to change from true to false (that's all that's currently needed in Dafny); Pop is what can make the change in the other direction
+ scopeSizeWhereInstancesWereDisallowed = names.Count;
+ }
+ }
+
+ public void PushMarker() {
+ names.Add(null);
+ things.Add(null);
+ }
+
+ public void PopMarker() {
+ int n = names.Count;
+ while (true) {
+ n--;
+ if (names[n] == null) {
+ break;
+ }
+ }
+ names.RemoveRange(n, names.Count - n);
+ things.RemoveRange(n, things.Count - n);
+ if (names.Count < scopeSizeWhereInstancesWereDisallowed) {
+ scopeSizeWhereInstancesWereDisallowed = -1;
+ }
+ }
+
+ // Pushes name-->thing association and returns "true", if name has not already been pushed since the last marker.
+ // If name already has been pushed since the last marker, does nothing and returns "false".
+ public bool Push(string name, Thing thing) {
+ Contract.Requires(name != null);
+ Contract.Requires(thing != null);
+ if (Find(name, true) != null) {
+ return false;
+ } else {
+ names.Add(name);
+ things.Add(thing);
+ return true;
+ }
+ }
+
+ Thing Find(string name, bool topScopeOnly) {
+ Contract.Requires(name != null);
+ for (int n = names.Count; 0 <= --n; ) {
+ if (names[n] == null) {
+ if (topScopeOnly) {
+ return null; // no present
+ }
+ } else if (names[n] == name) {
+ Thing t = things[n];
+ Contract.Assert(t != null);
+ return t;
+ }
+ }
+ return null; // not present
+ }
+
+ public Thing Find(string name) {
+ Contract.Requires(name != null);
+ return Find(name, false);
+ }
+
+ public bool ContainsDecl(Thing t) {
+ return things.Exists(thing => thing == t);
+ }
+ }
+}
|