//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Linq;
using System.Numerics;
using System.Diagnostics.Contracts;
using Microsoft.Boogie;
namespace Microsoft.Dafny
{
public class ResolutionErrorReporter
{
public int ErrorCount = 0;
///
/// This method is virtual, because it is overridden in the VSX plug-in for Dafny.
///
public virtual void Error(IToken tok, string msg, params object[] args) {
Contract.Requires(tok != null);
Contract.Requires(msg != null);
ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Red;
Console.WriteLine("{0}({1},{2}): Error: {3}",
tok.filename, tok.line, tok.col - 1,
string.Format(msg, args));
Console.ForegroundColor = col;
ErrorCount++;
}
public void Error(Declaration d, string msg, params object[] args) {
Contract.Requires(d != null);
Contract.Requires(msg != null);
Error(d.tok, msg, args);
}
public void Error(Statement s, string msg, params object[] args) {
Contract.Requires(s != null);
Contract.Requires(msg != null);
Error(s.Tok, msg, args);
}
public void Error(NonglobalVariable v, string msg, params object[] args) {
Contract.Requires(v != null);
Contract.Requires(msg != null);
Error(v.tok, msg, args);
}
public void Error(Expression e, string msg, params object[] args) {
Contract.Requires(e != null);
Contract.Requires(msg != null);
Error(e.tok, msg, args);
}
public void Warning(IToken tok, string msg, params object[] args) {
Contract.Requires(tok != null);
Contract.Requires(msg != null);
ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Yellow;
Console.WriteLine("{0}({1},{2}): Warning: {3}",
tok.filename, tok.line, tok.col - 1,
string.Format(msg, args));
Console.ForegroundColor = col;
}
}
public class Resolver : ResolutionErrorReporter
{
readonly BuiltIns builtIns;
//Dictionary/*!*/ classes; // can map to AmbiguousTopLevelDecl
//Dictionary importedNames; // the imported modules, as a map.
ModuleSignature moduleInfo = null;
class AmbiguousTopLevelDecl : TopLevelDecl // only used with "classes"
{
readonly TopLevelDecl A;
readonly TopLevelDecl B;
public AmbiguousTopLevelDecl(ModuleDefinition m, TopLevelDecl a, TopLevelDecl b)
: base(a.tok, a.Name + "/" + b.Name, m, new List(), null) {
A = a;
B = b;
}
public string ModuleNames() {
string nm;
if (A is AmbiguousTopLevelDecl) {
nm = ((AmbiguousTopLevelDecl)A).ModuleNames();
} else {
nm = A.Module.Name;
}
if (B is AmbiguousTopLevelDecl) {
nm += ", " + ((AmbiguousTopLevelDecl)B).ModuleNames();
} else {
nm += ", " + B.Module.Name;
}
return nm;
}
}
class AmbiguousMemberDecl : MemberDecl // only used with "classes"
{
readonly MemberDecl A;
readonly MemberDecl B;
public AmbiguousMemberDecl(ModuleDefinition m, MemberDecl a, MemberDecl b)
: base(a.tok, a.Name + "/" + b.Name, a.IsStatic, a.IsGhost, null) {
A = a;
B = b;
}
public string ModuleNames() {
string nm;
if (A is AmbiguousMemberDecl) {
nm = ((AmbiguousMemberDecl)A).ModuleNames();
} else {
nm = A.EnclosingClass.Module.Name;
}
if (B is AmbiguousMemberDecl) {
nm += ", " + ((AmbiguousMemberDecl)B).ModuleNames();
} else {
nm += ", " + B.EnclosingClass.Module.Name;
}
return nm;
}
}
//Dictionary> allDatatypeCtors;
readonly Dictionary/*!*/>/*!*/ classMembers = new Dictionary/*!*/>();
readonly Dictionary/*!*/>/*!*/ datatypeMembers = new Dictionary/*!*/>();
readonly Dictionary/*!*/>/*!*/ datatypeCtors = new Dictionary/*!*/>();
readonly Graph/*!*/ dependencies = new Graph();
private ModuleSignature systemNameInfo = null;
private bool useCompileSignatures = false;
public Resolver(Program prog) {
Contract.Requires(prog != null);
builtIns = prog.BuiltIns;
}
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(builtIns != null);
Contract.Invariant(cce.NonNullElements(dependencies));
Contract.Invariant(cce.NonNullDictionaryAndValues(classMembers) && Contract.ForAll(classMembers.Values, v => cce.NonNullDictionaryAndValues(v)));
Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v)));
}
public void ResolveProgram(Program prog) {
Contract.Requires(prog != null);
var bindings = new ModuleBindings(null);
var b = BindModuleNames(prog.DefaultModuleDef, bindings);
bindings.BindName("_module", prog.DefaultModule, b);
if (ErrorCount > 0) { return; } // if there were errors, then the implict ModuleBindings data structure invariant
// is violated, so Processing dependencies will not succeed.
ProcessDependencies(prog.DefaultModule, b, dependencies);
// check for cycles in the import graph
List cycle = dependencies.TryFindCycle();
if (cycle != null) {
var cy = Util.Comma(" -> ", cycle, m => m.Name);
Error(cycle[0], "module definition contains a cycle (note: parent modules implicitly depend on submodules): {0}", cy);
}
if (ErrorCount > 0) { return; } // give up on trying to resolve anything else
// fill in module heights
List sortedDecls = dependencies.TopologicallySortedComponents();
int h = 0;
foreach (ModuleDecl m in sortedDecls) {
m.Height = h;
if (m is LiteralModuleDecl) {
var mdef = ((LiteralModuleDecl)m).ModuleDef;
mdef.Height = h;
prog.Modules.Add(mdef);
}
h++;
}
var refinementTransformer = new RefinementTransformer(this, prog);
IRewriter rewriter = new AutoContractsRewriter();
systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);
foreach (var decl in sortedDecls) {
if (decl is LiteralModuleDecl) {
// The declaration is a literal module, so it has members and such that we need
// to resolve. First we do refinement transformation. Then we construct the signature
// of the module. This is the public, externally visible signature. Then we add in
// everything that the system defines, as well as any "import" (i.e. "opened" modules)
// directives (currently not supported, but this is where we would do it.) This signature,
// which is only used while resolving the members of the module is stored in the (basically)
// global variable moduleInfo. Then the signatures of the module members are resolved, followed
// by the bodies.
var literalDecl = (LiteralModuleDecl)decl;
var m = literalDecl.ModuleDef;
var errorCount = ErrorCount;
ModuleSignature refinedSig = null;
if (m.RefinementBaseRoot != null) {
if (ResolvePath(m.RefinementBaseRoot, m.RefinementBaseName, out refinedSig)) {
if (refinedSig.ModuleDef != null) {
m.RefinementBase = refinedSig.ModuleDef;
refinementTransformer.PreResolve(m);
} else {
Error(m.RefinementBaseName[0], "module ({0}) named as refinement base is not a literal module or simple reference to a literal module", Util.Comma(".", m.RefinementBaseName, x => x.val));
}
} else {
Error(m.RefinementBaseName[0], "module ({0}) named as refinement base does not exist", Util.Comma(".", m.RefinementBaseName, x => x.val));
}
}
if (errorCount == ErrorCount) {
rewriter.PreResolve(m);
}
literalDecl.Signature = RegisterTopLevelDecls(m, true);
literalDecl.Signature.Refines = refinedSig;
var sig = literalDecl.Signature;
// set up environment
var preResolveErrorCount = ErrorCount;
ResolveModuleDefinition(m, sig);
if (ErrorCount == preResolveErrorCount) {
refinementTransformer.PostResolve(m);
// give rewriter a chance to do processing
rewriter.PostResolve(m);
}
if (ErrorCount == errorCount && !m.IsAbstract) {
// compilation should only proceed if everything is good, including the signature (which preResolveErrorCount does not include);
Contract.Assert(!useCompileSignatures);
useCompileSignatures = true; // set Resolver-global flag to indicate that Signatures should be followed to their CompiledSignature
var nw = new Cloner().CloneModuleDefinition(m, m.CompileName + "_Compile");
var compileSig = RegisterTopLevelDecls(nw, true);
compileSig.Refines = refinedSig;
sig.CompileSignature = compileSig;
ResolveModuleDefinition(nw, compileSig);
prog.CompileModules.Add(nw);
useCompileSignatures = false; // reset the flag
}
} else if (decl is AliasModuleDecl) {
var alias = (AliasModuleDecl)decl;
// resolve the path
ModuleSignature p;
if (ResolvePath(alias.Root, alias.Path, out p)) {
alias.Signature = p;
} else {
alias.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature
}
} else if (decl is ModuleFacadeDecl) {
var abs = (ModuleFacadeDecl)decl;
ModuleSignature p;
if (ResolvePath(abs.Root, abs.Path, out p)) {
abs.Signature = MakeAbstractSignature(p, abs.FullCompileName, abs.Height, prog.Modules);
abs.OriginalSignature = p;
ModuleSignature compileSig;
if (abs.CompilePath != null) {
if (ResolvePath(abs.CompileRoot, abs.CompilePath, out compileSig)) {
if (refinementTransformer.CheckIsRefinement(compileSig, p)) {
abs.Signature.CompileSignature = compileSig;
} else {
Error(abs.CompilePath[0],
"module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of " + Util.Comma(".", abs.Path, x => x.val));
}
abs.Signature.IsGhost = compileSig.IsGhost;
// always keep the ghost information, to supress a spurious error message when the compile module isn't actually a refinement
}
}
} else {
abs.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature
}
} else { Contract.Assert(false); }
Contract.Assert(decl.Signature != null);
}
// compute IsRecursive bit for mutually recursive functions
foreach (ModuleDefinition m in prog.Modules) {
foreach (var fn in ModuleDefinition.AllFunctions(m.TopLevelDecls)) {
if (!fn.IsRecursive) { // note, self-recursion has already been determined
int n = m.CallGraph.GetSCCSize(fn);
if (2 <= n) {
// the function is mutually recursive (note, the SCC does not determine self recursion)
fn.IsRecursive = true;
}
}
if (fn.IsRecursive && fn is CoPredicate) {
// this means the corresponding prefix predicate is also recursive
var prefixPred = ((CoPredicate)fn).PrefixPredicate;
if (prefixPred != null) {
prefixPred.IsRecursive = true;
}
}
}
}
}
private void ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) {
moduleInfo = MergeSignature(sig, systemNameInfo);
// resolve
var datatypeDependencies = new Graph();
var codatatypeDependencies = new Graph();
int prevErrorCount = ErrorCount;
ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);
if (ErrorCount == prevErrorCount) {
ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);
}
}
public class ModuleBindings
{
private ModuleBindings parent;
private Dictionary modules;
private Dictionary bindings;
public ModuleBindings(ModuleBindings p) {
parent = p;
modules = new Dictionary();
bindings = new Dictionary();
}
public bool BindName(string name, ModuleDecl subModule, ModuleBindings b) {
if (modules.ContainsKey(name)) {
return false;
} else {
modules.Add(name, subModule);
bindings.Add(name, b);
return true;
}
}
public bool TryLookup(IToken name, out ModuleDecl m) {
Contract.Requires(name != null);
if (modules.TryGetValue(name.val, out m)) {
return true;
} else if (parent != null) {
return parent.TryLookup(name, out m);
} else return false;
}
public bool TryLookupIgnore(IToken name, out ModuleDecl m, ModuleDecl ignore) {
Contract.Requires(name != null);
if (modules.TryGetValue(name.val, out m) && m != ignore) {
return true;
} else if (parent != null) {
return parent.TryLookup(name, out m);
} else return false;
}
public IEnumerable ModuleList {
get { return modules.Values; }
}
public ModuleBindings SubBindings(string name) {
ModuleBindings v = null;
bindings.TryGetValue(name, out v);
return v;
}
}
private ModuleBindings BindModuleNames(ModuleDefinition moduleDecl, ModuleBindings parentBindings) {
var bindings = new ModuleBindings(parentBindings);
foreach (var tld in moduleDecl.TopLevelDecls) {
if (tld is LiteralModuleDecl) {
var subdecl = (LiteralModuleDecl)tld;
var subBindings = BindModuleNames(subdecl.ModuleDef, bindings);
if (!bindings.BindName(subdecl.Name, subdecl, subBindings)) {
Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name);
}
} else if (tld is ModuleFacadeDecl) {
var subdecl = (ModuleFacadeDecl)tld;
if (!bindings.BindName(subdecl.Name, subdecl, null)) {
Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name);
}
} else if (tld is AliasModuleDecl) {
var subdecl = (AliasModuleDecl)tld;
if (!bindings.BindName(subdecl.Name, subdecl, null)) {
Error(subdecl.tok, "Duplicate module name: {0}", subdecl.Name);
}
}
}
return bindings;
}
private void ProcessDependenciesDefinition(ModuleDecl decl, ModuleDefinition m, ModuleBindings bindings, Graph dependencies) {
if (m.RefinementBaseName != null) {
ModuleDecl other;
if (!bindings.TryLookup(m.RefinementBaseName[0], out other)) {
Error(m.RefinementBaseName[0], "module {0} named as refinement base does not exist", m.RefinementBaseName[0].val);
} else if (other is LiteralModuleDecl && ((LiteralModuleDecl)other).ModuleDef == m) {
Error(m.RefinementBaseName[0], "module cannot refine itself: {0}", m.RefinementBaseName[0].val);
} else {
Contract.Assert(other != null); // follows from postcondition of TryGetValue
dependencies.AddEdge(decl, other);
m.RefinementBaseRoot = other;
}
}
foreach (var toplevel in m.TopLevelDecls) {
if (toplevel is ModuleDecl) {
var d = (ModuleDecl)toplevel;
dependencies.AddEdge(decl, d);
var subbindings = bindings.SubBindings(d.Name);
ProcessDependencies(d, subbindings ?? bindings, dependencies);
}
}
}
private void ProcessDependencies(ModuleDecl moduleDecl, ModuleBindings bindings, Graph dependencies) {
dependencies.AddVertex(moduleDecl);
if (moduleDecl is LiteralModuleDecl) {
ProcessDependenciesDefinition(moduleDecl, ((LiteralModuleDecl)moduleDecl).ModuleDef, bindings, dependencies);
} else if (moduleDecl is AliasModuleDecl) {
var alias = moduleDecl as AliasModuleDecl;
ModuleDecl root;
if (!bindings.TryLookupIgnore(alias.Path[0], out root, alias))
Error(alias.tok, ModuleNotFoundErrorMessage(0, alias.Path));
else {
dependencies.AddEdge(moduleDecl, root);
alias.Root = root;
}
} else if (moduleDecl is ModuleFacadeDecl) {
var abs = moduleDecl as ModuleFacadeDecl;
ModuleDecl root;
if (!bindings.TryLookup(abs.Path[0], out root))
Error(abs.tok, ModuleNotFoundErrorMessage(0, abs.Path));
else {
dependencies.AddEdge(moduleDecl, root);
abs.Root = root;
}
if (abs.CompilePath != null) {
if (!bindings.TryLookup(abs.CompilePath[0], out root))
Error(abs.tok, ModuleNotFoundErrorMessage(0, abs.CompilePath));
else {
dependencies.AddEdge(moduleDecl, root);
abs.CompileRoot = root;
}
}
}
}
private string ModuleNotFoundErrorMessage(int i, List path) {
Contract.Requires(path != null);
Contract.Requires(0 <= i && i < path.Count);
return "module " + path[i].val + " does not exist" +
(1 < path.Count ? " (position " + i.ToString() + " in path " + Util.Comma(".", path, x => x.val) + ")" : "");
}
public static ModuleSignature MergeSignature(ModuleSignature m, ModuleSignature system) {
var info = new ModuleSignature();
// add the system-declared information, among which we know there are no duplicates
foreach (var kv in system.TopLevels) {
info.TopLevels.Add(kv.Key, kv.Value);
}
foreach (var kv in system.Ctors) {
info.Ctors.Add(kv.Key, kv.Value);
}
// add for the module itself
foreach (var kv in m.TopLevels) {
info.TopLevels[kv.Key] = kv.Value;
}
foreach (var kv in m.Ctors) {
info.Ctors[kv.Key] = kv.Value;
}
foreach (var kv in m.StaticMembers) {
info.StaticMembers[kv.Key] = kv.Value;
}
info.IsGhost = m.IsGhost;
return info;
}
ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImports) {
Contract.Requires(moduleDef != null);
var sig = new ModuleSignature();
sig.ModuleDef = moduleDef;
sig.IsGhost = moduleDef.IsAbstract;
List declarations = moduleDef.TopLevelDecls;
if (useImports) {
// First go through and add anything from the opened imports
foreach (var im in declarations) {
if (im is ModuleDecl && ((ModuleDecl)im).Opened) {
var s = GetSignature(((ModuleDecl)im).Signature);
// classes:
foreach (var kv in s.TopLevels) {
TopLevelDecl d;
if (sig.TopLevels.TryGetValue(kv.Key, out d)) {
sig.TopLevels[kv.Key] = new AmbiguousTopLevelDecl(moduleDef, d, kv.Value);
} else {
sig.TopLevels.Add(kv.Key, kv.Value);
}
}
// constructors:
foreach (var kv in s.Ctors) {
Tuple pair;
if (sig.Ctors.TryGetValue(kv.Key, out pair)) {
// mark it as a duplicate
sig.Ctors[kv.Key] = new Tuple(pair.Item1, true);
} else {
// add new
sig.Ctors.Add(kv.Key, kv.Value);
}
}
// static members:
foreach (var kv in s.StaticMembers) {
MemberDecl md;
if (sig.StaticMembers.TryGetValue(kv.Key, out md)) {
sig.StaticMembers[kv.Key] = new AmbiguousMemberDecl(moduleDef, md, kv.Value);
} else {
// add new
sig.StaticMembers.Add(kv.Key, kv.Value);
}
}
}
}
}
// This is solely used to detect duplicates amongst the various e
Dictionary toplevels = new Dictionary();
// Now add the things present
foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
// register the class/datatype/module name
if (toplevels.ContainsKey(d.Name)) {
Error(d, "Duplicate name of top-level declaration: {0}", d.Name);
} else {
toplevels[d.Name] = d;
sig.TopLevels[d.Name] = d;
}
if (d is ModuleDecl) {
// nothing to do
} else if (d is ArbitraryTypeDecl) {
// nothing more to register
} else if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
// register the names of the implicit members
var members = new Dictionary();
classMembers.Add(iter, members);
// First, register the iterator's in- and out-parameters as readonly fields
foreach (var p in iter.Ins) {
if (members.ContainsKey(p.Name)) {
Error(p, "Name of in-parameter is used by another member of the iterator: {0}", p.Name);
} else {
var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, false, false, p.Type, null);
field.EnclosingClass = iter; // resolve here
members.Add(p.Name, field);
iter.Members.Add(field);
}
}
foreach (var p in iter.Outs) {
if (members.ContainsKey(p.Name)) {
Error(p, "Name of yield-parameter is used by another member of the iterator: {0}", p.Name);
} else {
var field = new SpecialField(p.tok, p.Name, p.CompileName, "", "", p.IsGhost, true, true, p.Type, null);
field.EnclosingClass = iter; // resolve here
iter.OutsFields.Add(field);
members.Add(p.Name, field);
iter.Members.Add(field);
}
}
foreach (var p in iter.Outs) {
var nm = p.Name + "s";
if (members.ContainsKey(nm)) {
Error(p.tok, "Name of implicit yield-history variable '{0}' is already used by another member of the iterator", p.Name);
} else {
var tp = new SeqType(p.Type.IsSubrangeType ? new IntType() : p.Type);
var field = new SpecialField(p.tok, nm, nm, "", "", true, true, false, tp, null);
field.EnclosingClass = iter; // resolve here
iter.OutsHistoryFields.Add(field); // for now, just record this field (until all parameters have been added as members)
}
}
// now that already-used 'ys' names have been checked for, add these yield-history variables
iter.OutsHistoryFields.ForEach(f => {
members.Add(f.Name, f);
iter.Members.Add(f);
});
// add the additional special variables as fields
iter.Member_Reads = new SpecialField(iter.tok, "_reads", "_reads", "", "", true, false, false, new SetType(new ObjectType()), null);
iter.Member_Modifies = new SpecialField(iter.tok, "_modifies", "_modifies", "", "", true, false, false, new SetType(new ObjectType()), null);
iter.Member_New = new SpecialField(iter.tok, "_new", "_new", "", "", true, true, true, new SetType(new ObjectType()), null);
foreach (var field in new List() { iter.Member_Reads, iter.Member_Modifies, iter.Member_New }) {
field.EnclosingClass = iter; // resolve here
members.Add(field.Name, field);
iter.Members.Add(field);
}
// finally, add special variables to hold the components of the (explicit or implicit) decreases clause
bool inferredDecreases;
var decr = Translator.MethodDecreasesWithDefault(iter, out inferredDecreases);
if (inferredDecreases) {
iter.InferredDecreases = true;
Contract.Assert(iter.Decreases.Expressions.Count == 0);
iter.Decreases.Expressions.AddRange(decr);
}
// create the fields; unfortunately, we don't know their types yet, so we'll just insert type proxies for now
var i = 0;
foreach (var p in iter.Decreases.Expressions) {
var nm = "_decreases" + i;
var field = new SpecialField(p.tok, nm, nm, "", "", true, false, false, new InferredTypeProxy(), null);
field.EnclosingClass = iter; // resolve here
iter.DecreasesFields.Add(field);
members.Add(field.Name, field);
iter.Members.Add(field);
i++;
}
// Note, the typeArgs parameter to the following Method/Predicate constructors is passed in as the empty list. What that is
// saying is that the Method/Predicate does not take any type parameters over and beyond what the enclosing type (namely, the
// iterator type) does.
// --- here comes the constructor
var init = new Constructor(iter.tok, "_ctor", new List(), iter.Ins,
new List(),
new Specification(new List(), null),
new List(),
new Specification(new List(), null),
null, null, false);
// --- here comes predicate Valid()
var valid = new Predicate(iter.tok, "Valid", false, true, new List(), iter.tok,
new List(),
new List(),
new List(),
new List(),
new Specification(new List(), null),
null, Predicate.BodyOriginKind.OriginalOrInherited, null, false);
// --- here comes method MoveNext
var moveNext = new Method(iter.tok, "MoveNext", false, false, new List(),
new List(), new List() { new Formal(iter.tok, "more", Type.Bool, false, false) },
new List(),
new Specification(new List(), null),
new List(),
new Specification(new List(), null),
null, null, false);
// add these implicit members to the class
init.EnclosingClass = iter;
valid.EnclosingClass = iter;
moveNext.EnclosingClass = iter;
iter.HasConstructor = true;
iter.Member_Init = init;
iter.Member_Valid = valid;
iter.Member_MoveNext = moveNext;
MemberDecl member;
if (members.TryGetValue(init.Name, out member)) {
Error(member.tok, "member name '{0}' is already predefined for this iterator", init.Name);
} else {
members.Add(init.Name, init);
iter.Members.Add(init);
}
// If the name of the iterator is "Valid" or "MoveNext", one of the following will produce an error message. That
// error message may not be as clear as it could be, but the situation also seems unlikely to ever occur in practice.
if (members.TryGetValue("Valid", out member)) {
Error(member.tok, "member name 'Valid' is already predefined for iterators");
} else {
members.Add(valid.Name, valid);
iter.Members.Add(valid);
}
if (members.TryGetValue("MoveNext", out member)) {
Error(member.tok, "member name 'MoveNext' is already predefined for iterators");
} else {
members.Add(moveNext.Name, moveNext);
iter.Members.Add(moveNext);
}
} else if (d is ClassDecl) {
ClassDecl cl = (ClassDecl)d;
// register the names of the class members
var members = new Dictionary();
classMembers.Add(cl, members);
bool hasConstructor = false;
foreach (MemberDecl m in cl.Members) {
if (!members.ContainsKey(m.Name)) {
members.Add(m.Name, m);
if (m is CoPredicate || m is CoMethod) {
var extraName = m.Name + "#";
MemberDecl extraMember;
var cloner = new Cloner();
var formals = new List();
var k = new ImplicitFormal(m.tok, "_k", new NatType(), true, false);
formals.Add(k);
if (m is CoPredicate) {
var cop = (CoPredicate)m;
formals.AddRange(cop.Formals.ConvertAll(cloner.CloneFormal));
// create prefix predicate
cop.PrefixPredicate = new PrefixPredicate(cop.tok, extraName, cop.IsStatic,
cop.TypeArgs.ConvertAll(cloner.CloneTypeParam), cop.OpenParen, k, formals,
cop.Req.ConvertAll(cloner.CloneExpr), cop.Reads.ConvertAll(cloner.CloneFrameExpr), cop.Ens.ConvertAll(cloner.CloneExpr),
new Specification(new List() { new IdentifierExpr(cop.tok, k.Name) }, null),
cop.Body, null, cop);
extraMember = cop.PrefixPredicate;
// In the call graph, add an edge from P# to P, since this will have the desired effect of detecting unwanted cycles.
moduleDef.CallGraph.AddEdge(cop.PrefixPredicate, cop);
} else {
var com = (CoMethod)m;
// _k has already been added to 'formals', so append the original formals
formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal));
// prepend _k to the given decreases clause
var decr = new List();
decr.Add(new IdentifierExpr(com.tok, k.Name));
decr.AddRange(com.Decreases.Expressions.ConvertAll(cloner.CloneExpr));
// Create prefix method. Note that the body is not cloned, but simply shared.
com.PrefixMethod = new PrefixMethod(com.tok, extraName, com.IsStatic,
com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal),
com.Req.ConvertAll(cloner.CloneMayBeFreeExpr), cloner.CloneSpecFrameExpr(com.Mod),
new List(), // Note, the postconditions are filled in after the comethod's postconditions have been resolved
new Specification(decr, null),
null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the comethod is known
cloner.CloneAttributes(com.Attributes), com);
extraMember = com.PrefixMethod;
// In the call graph, add an edge from M# to M, since this will have the desired effect of detecting unwanted cycles.
moduleDef.CallGraph.AddEdge(com.PrefixMethod, com);
}
members.Add(extraName, extraMember);
}
} else if (m is Constructor && !((Constructor)m).HasName) {
Error(m, "More than one default constructor");
} else {
Error(m, "Duplicate member name: {0}", m.Name);
}
if (m is Constructor) {
hasConstructor = true;
}
}
cl.HasConstructor = hasConstructor;
if (cl.IsDefaultClass) {
foreach (MemberDecl m in cl.Members) {
if (m.IsStatic && (m is Function || m is Method)) {
sig.StaticMembers[m.Name] = m;
}
}
}
} else {
DatatypeDecl dt = (DatatypeDecl)d;
// register the names of the constructors
var ctors = new Dictionary();
datatypeCtors.Add(dt, ctors);
// ... and of the other members
var members = new Dictionary();
datatypeMembers.Add(dt, members);
foreach (DatatypeCtor ctor in dt.Ctors) {
if (ctor.Name.EndsWith("?")) {
Error(ctor, "a datatype constructor name is not allowed to end with '?'");
} else if (ctors.ContainsKey(ctor.Name)) {
Error(ctor, "Duplicate datatype constructor name: {0}", ctor.Name);
} else {
ctors.Add(ctor.Name, ctor);
// create and add the query "method" (field, really)
string queryName = ctor.Name + "?";
var query = new SpecialField(ctor.tok, queryName, "is_" + ctor.CompileName, "", "", false, false, false, Type.Bool, null);
query.EnclosingClass = dt; // resolve here
members.Add(queryName, query);
ctor.QueryField = query;
// also register the constructor name globally
Tuple pair;
if (sig.Ctors.TryGetValue(ctor.Name, out pair)) {
// mark it as a duplicate
sig.Ctors[ctor.Name] = new Tuple(pair.Item1, true);
} else {
// add new
sig.Ctors.Add(ctor.Name, new Tuple(ctor, false));
}
}
}
// add deconstructors now (that is, after the query methods have been added)
foreach (DatatypeCtor ctor in dt.Ctors) {
foreach (var formal in ctor.Formals) {
bool nameError = false;
if (formal.HasName && members.ContainsKey(formal.Name)) {
Error(ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);
nameError = true;
}
var dtor = new DatatypeDestructor(formal.tok, ctor, formal, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);
dtor.EnclosingClass = dt; // resolve here
if (!nameError && formal.HasName) {
members.Add(formal.Name, dtor);
}
ctor.Destructors.Add(dtor);
}
}
}
}
return sig;
}
private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, List mods) {
var mod = new ModuleDefinition(Token.NoToken, Name + ".Abs", true, true, null, null, false);
mod.Height = Height;
foreach (var kv in p.TopLevels) {
mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name));
}
var sig = RegisterTopLevelDecls(mod, false);
sig.Refines = p.Refines;
sig.CompileSignature = p;
sig.IsGhost = p.IsGhost;
mods.Add(mod);
ResolveModuleDefinition(mod, sig);
return sig;
}
TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m, List mods, string Name) {
Contract.Requires(d != null);
Contract.Requires(m != null);
if (d is ArbitraryTypeDecl) {
var dd = (ArbitraryTypeDecl)d;
return new ArbitraryTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, null);
} else if (d is IndDatatypeDecl) {
var dd = (IndDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var ctors = dd.Ctors.ConvertAll(CloneCtor);
var dt = new IndDatatypeDecl(dd.tok, dd.Name, m, tps, ctors, null);
return dt;
} else if (d is CoDatatypeDecl) {
var dd = (CoDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var ctors = dd.Ctors.ConvertAll(CloneCtor);
var dt = new CoDatatypeDecl(dd.tok, dd.Name, m, tps, ctors, null);
return dt;
} else if (d is ClassDecl) {
var dd = (ClassDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var mm = dd.Members.ConvertAll(CloneMember);
if (dd is DefaultClassDecl) {
return new DefaultClassDecl(m, mm);
} else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl) {
return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);
} else if (d is AliasModuleDecl) {
var a = (AliasModuleDecl)d;
var alias = new AliasModuleDecl(a.Path, a.tok, m, a.Opened);
alias.ModuleReference = a.ModuleReference;
alias.Signature = a.Signature;
return alias;
} else if (d is ModuleFacadeDecl) {
var abs = (ModuleFacadeDecl)d;
var sig = MakeAbstractSignature(abs.OriginalSignature, Name + "." + abs.Name, abs.Height, mods);
var a = new ModuleFacadeDecl(abs.Path, abs.tok, m, abs.CompilePath, abs.Opened);
a.Signature = sig;
a.OriginalSignature = abs.OriginalSignature;
return a;
} else {
Contract.Assert(false); // unexpected declaration
return null; // to please compiler
}
} else {
Contract.Assert(false); // unexpected declaration
return null; // to please compiler
}
}
MemberDecl CloneMember(MemberDecl member) {
if (member is Field) {
Contract.Assert(!(member is SpecialField)); // we don't expect a SpecialField to be cloned (or do we?)
var f = (Field)member;
return new Field(f.tok, f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), null);
} else if (member is Function) {
var f = (Function)member;
return CloneFunction(f.tok, f, f.IsGhost);
} else {
var m = (Method)member;
return CloneMethod(m);
}
}
TypeParameter CloneTypeParam(TypeParameter tp) {
return new TypeParameter(tp.tok, tp.Name);
}
DatatypeCtor CloneCtor(DatatypeCtor ct) {
return new DatatypeCtor(ct.tok, ct.Name, ct.Formals.ConvertAll(CloneFormal), null);
}
Formal CloneFormal(Formal formal) {
return new Formal(formal.tok, formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);
}
Type CloneType(Type t) {
if (t is BasicType) {
return t;
} else if (t is SetType) {
var tt = (SetType)t;
return new SetType(CloneType(tt.Arg));
} else if (t is SeqType) {
var tt = (SeqType)t;
return new SeqType(CloneType(tt.Arg));
} else if (t is MultiSetType) {
var tt = (MultiSetType)t;
return new MultiSetType(CloneType(tt.Arg));
} else if (t is MapType) {
var tt = (MapType)t;
return new MapType(CloneType(tt.Domain), CloneType(tt.Range));
} else if (t is UserDefinedType) {
var tt = (UserDefinedType)t;
return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => x));
} else if (t is InferredTypeProxy) {
return new InferredTypeProxy();
} else {
Contract.Assert(false); // unexpected type (e.g., no other type proxies are expected at this time)
return null; // to please compiler
}
}
Function CloneFunction(IToken tok, Function f, bool isGhost) {
var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
var formals = f.Formals.ConvertAll(CloneFormal);
var req = f.Req.ConvertAll(CloneExpr);
var reads = f.Reads.ConvertAll(CloneFrameExpr);
var decreases = CloneSpecExpr(f.Decreases);
var ens = f.Ens.ConvertAll(CloneExpr);
Expression body = CloneExpr(f.Body);
if (f is Predicate) {
return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,
req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, null, false);
} else if (f is CoPredicate) {
return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,
req, reads, ens, body, null, false);
} else {
return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),
req, reads, ens, decreases, body, null, false);
}
}
Method CloneMethod(Method m) {
Contract.Requires(m != null);
var tps = m.TypeArgs.ConvertAll(CloneTypeParam);
var ins = m.Ins.ConvertAll(CloneFormal);
var req = m.Req.ConvertAll(CloneMayBeFreeExpr);
var mod = CloneSpecFrameExpr(m.Mod);
var decreases = CloneSpecExpr(m.Decreases);
var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr);
if (m is Constructor) {
return new Constructor(m.tok, m.Name, tps, ins,
req, mod, ens, decreases, null, null, false);
} else if (m is CoMethod) {
return new CoMethod(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, null, null, false);
} else {
return new Method(m.tok, m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, null, null, false);
}
}
Specification CloneSpecExpr(Specification spec) {
var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr);
return new Specification(ee, null);
}
Specification CloneSpecFrameExpr(Specification frame) {
var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr);
return new Specification(ee, null);
}
FrameExpression CloneFrameExpr(FrameExpression frame) {
return new FrameExpression(frame.tok, CloneExpr(frame.E), frame.FieldName);
}
MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {
return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);
}
BoundVar CloneBoundVar(BoundVar bv) {
return new BoundVar(bv.tok, bv.Name, CloneType(bv.Type));
}
// ToDo: Remove this and use cloner
Expression CloneExpr(Expression expr) {
if (expr == null) {
return null;
} else if (expr is LiteralExpr) {
var e = (LiteralExpr)expr;
if (e.Value == null) {
return new LiteralExpr(e.tok);
} else if (e.Value is bool) {
return new LiteralExpr(e.tok, (bool)e.Value);
} else {
return new LiteralExpr(e.tok, (BigInteger)e.Value);
}
} else if (expr is ThisExpr) {
if (expr is ImplicitThisExpr) {
return new ImplicitThisExpr(expr.tok);
} else {
return new ThisExpr(expr.tok);
}
} else if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
return new IdentifierExpr(e.tok, e.Name);
} else if (expr is DatatypeValue) {
var e = (DatatypeValue)expr;
return new DatatypeValue(e.tok, e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr));
} else if (expr is DisplayExpression) {
DisplayExpression e = (DisplayExpression)expr;
if (expr is SetDisplayExpr) {
return new SetDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr));
} else if (expr is MultiSetDisplayExpr) {
return new MultiSetDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr));
} else {
Contract.Assert(expr is SeqDisplayExpr);
return new SeqDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr));
}
} else if (expr is MapDisplayExpr) {
MapDisplayExpr e = (MapDisplayExpr)expr;
List pp = new List();
foreach (ExpressionPair p in e.Elements) {
pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B)));
}
return new MapDisplayExpr(expr.tok, pp);
} else if (expr is ExprDotName) {
var e = (ExprDotName)expr;
return new ExprDotName(e.tok, CloneExpr(e.Obj), e.SuffixName);
} else if (expr is FieldSelectExpr) {
var e = (FieldSelectExpr)expr;
return new FieldSelectExpr(e.tok, CloneExpr(e.Obj), e.FieldName);
} else if (expr is SeqSelectExpr) {
var e = (SeqSelectExpr)expr;
return new SeqSelectExpr(e.tok, e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1));
} else if (expr is MultiSelectExpr) {
var e = (MultiSelectExpr)expr;
return new MultiSelectExpr(e.tok, CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr));
} else if (expr is SeqUpdateExpr) {
var e = (SeqUpdateExpr)expr;
return new SeqUpdateExpr(e.tok, CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value));
} else if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
return new FunctionCallExpr(e.tok, e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : (e.OpenParen), e.Args.ConvertAll(CloneExpr));
} else if (expr is OldExpr) {
var e = (OldExpr)expr;
return new OldExpr(e.tok, CloneExpr(e.E));
} else if (expr is MultiSetFormingExpr) {
var e = (MultiSetFormingExpr)expr;
return new MultiSetFormingExpr(e.tok, CloneExpr(e.E));
} else if (expr is FreshExpr) {
var e = (FreshExpr)expr;
return new FreshExpr(e.tok, CloneExpr(e.E));
} else if (expr is UnaryExpr) {
var e = (UnaryExpr)expr;
return new UnaryExpr(e.tok, e.Op, CloneExpr(e.E));
} else if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
return new BinaryExpr(e.tok, e.Op, CloneExpr(e.E0), CloneExpr(e.E1));
} else if (expr is TernaryExpr) {
var e = (TernaryExpr)expr;
return new TernaryExpr(e.tok, e.Op, CloneExpr(e.E0), CloneExpr(e.E1), CloneExpr(e.E2));
} else if (expr is ChainingExpression) {
var e = (ChainingExpression)expr;
return CloneExpr(e.E); // just clone the desugaring, since it's already available
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
return new LetExpr(e.tok, e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body), e.Exact);
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
var tk = e.tok;
var bvs = e.BoundVars.ConvertAll(CloneBoundVar);
var range = CloneExpr(e.Range);
var term = CloneExpr(e.Term);
if (e is ForallExpr) {
return new ForallExpr(tk, bvs, range, term, null);
} else if (e is ExistsExpr) {
return new ExistsExpr(tk, bvs, range, term, null);
} else if (e is MapComprehension) {
return new MapComprehension(tk, bvs, range, term);
} else {
Contract.Assert(e is SetComprehension);
return new SetComprehension(tk, bvs, range, term);
}
} else if (expr is WildcardExpr) {
return new WildcardExpr(expr.tok);
} else if (expr is PredicateExpr) {
var e = (PredicateExpr)expr;
if (e is AssertExpr) {
return new AssertExpr(e.tok, CloneExpr(e.Guard), CloneExpr(e.Body));
} else {
Contract.Assert(e is AssumeExpr);
return new AssumeExpr(e.tok, CloneExpr(e.Guard), CloneExpr(e.Body));
}
} else if (expr is CalcExpr) {
var e = (CalcExpr)expr;
return new CalcExpr(e.tok, (CalcStmt)((new Cloner()).CloneStmt(e.Guard)), CloneExpr(e.Body), (AssumeExpr)CloneExpr(e.AsAssumeExpr));
} else if (expr is ITEExpr) {
var e = (ITEExpr)expr;
return new ITEExpr(e.tok, CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els));
} else if (expr is ParensExpression) {
var e = (ParensExpression)expr;
return CloneExpr(e.E); // skip the parentheses in the clone
} else if (expr is IdentifierSequence) {
var e = (IdentifierSequence)expr;
var aa = e.Arguments == null ? null : e.Arguments.ConvertAll(CloneExpr);
return new IdentifierSequence(e.Tokens.ConvertAll(tk => (tk)), e.OpenParen == null ? null : (e.OpenParen), aa);
} else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
return new MatchExpr(e.tok, CloneExpr(e.Source),
e.Cases.ConvertAll(c => new MatchCaseExpr(c.tok, c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))));
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
}
private bool ResolvePath(ModuleDecl root, List Path, out ModuleSignature p) {
p = root.Signature;
int i = 1;
while (i < Path.Count) {
ModuleSignature pp;
if (p.FindSubmodule(Path[i].val, out pp)) {
p = pp;
i++;
} else {
Error(Path[i], ModuleNotFoundErrorMessage(i, Path));
break;
}
}
return i == Path.Count;
}
public void ResolveTopLevelDecls_Signatures(ModuleDefinition def, List/*!*/ declarations, Graph/*!*/ datatypeDependencies, Graph/*!*/ codatatypeDependencies) {
Contract.Requires(declarations != null);
Contract.Requires(datatypeDependencies != null);
Contract.Requires(codatatypeDependencies != null);
foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
allTypeParameters.PushMarker();
ResolveTypeParameters(d.TypeArgs, true, d);
if (d is ArbitraryTypeDecl) {
// nothing to do
} else if (d is IteratorDecl) {
ResolveIteratorSignature((IteratorDecl)d);
} else if (d is ClassDecl) {
ResolveClassMemberTypes((ClassDecl)d);
} else if (d is ModuleDecl) {
var decl = (ModuleDecl)d;
if (!def.IsAbstract) {
if (decl.Signature.IsGhost)
{
if (!(def.IsDefaultModule)) // _module is allowed to contain abstract modules, but not be abstract itself. Note this presents a challenge to
// trusted verification, as toplevels can't be trusted if they invoke abstract module members.
Error(d.tok, "an abstract module can only be imported into other abstract modules, not a concrete one.");
} else {
// physical modules are allowed everywhere
}
} else {
// everything is allowed in an abstract module
}
} else {
ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies, codatatypeDependencies);
}
allTypeParameters.PopMarker();
}
}
public void ResolveTopLevelDecls_Meat(List/*!*/ declarations, Graph/*!*/ datatypeDependencies, Graph/*!*/ codatatypeDependencies) {
Contract.Requires(declarations != null);
Contract.Requires(cce.NonNullElements(datatypeDependencies));
Contract.Requires(cce.NonNullElements(codatatypeDependencies));
int prevErrorCount = ErrorCount;
// Resolve the meat of classes, and the type parameters of all top-level type declarations
foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
allTypeParameters.PushMarker();
ResolveTypeParameters(d.TypeArgs, false, d);
if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
ResolveIterator(iter);
ResolveClassMemberBodies(iter); // resolve the automatically generated members
} else if (d is ClassDecl) {
var cl = (ClassDecl)d;
ResolveAttributes(cl.Attributes, false, new NoContext(cl.Module));
ResolveClassMemberBodies(cl);
}
allTypeParameters.PopMarker();
}
if (ErrorCount == prevErrorCount) {
// fill in the postconditions and bodies of prefix methods
foreach (var com in ModuleDefinition.AllCoMethods(declarations)) {
var prefixMethod = com.PrefixMethod;
if (prefixMethod == null) {
continue; // something went wrong during registration of the prefix method (probably a duplicated comethod name)
}
Contract.Assume(prefixMethod.Ens.Count == 0 && prefixMethod.Body == null); // there are not supposed have have been filled in before
// compute the postconditions of the prefix method
var k = prefixMethod.Ins[0];
foreach (var p in com.Ens) {
var coConclusions = new HashSet();
CheckCoMethodConclusions(p.E, true, coConclusions);
var subst = new CoMethodPostconditionSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name));
var post = subst.CloneExpr(p.E);
prefixMethod.Ens.Add(new MaybeFreeExpression(post, p.IsFree));
}
// Compute the statement body of the prefix method
if (com.Body != null) {
var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1));
var subst = new CoMethodBodyCloner(com, kMinusOne);
var mainBody = subst.CloneBlockStmt(com.Body);
var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name));
var condBody = new IfStmt(com.BodyStartTok, kPositive, mainBody, null);
prefixMethod.Body = new BlockStmt(com.tok, new List() { condBody });
}
// The prefix method now has all its components, so it's finally time we resolve it
currentClass = (ClassDecl)prefixMethod.EnclosingClass;
allTypeParameters.PushMarker();
ResolveTypeParameters(currentClass.TypeArgs, false, currentClass);
ResolveTypeParameters(prefixMethod.TypeArgs, false, prefixMethod);
ResolveMethod(prefixMethod);
allTypeParameters.PopMarker();
currentClass = null;
}
foreach (TopLevelDecl d in declarations) {
if (d is ClassDecl) {
foreach (var member in ((ClassDecl)d).Members) {
if (member is Method) {
var m = (Method)member;
m.Req.Iter(mfe => CheckTypeInference(mfe.E));
m.Ens.Iter(mfe => CheckTypeInference(mfe.E));
m.Mod.Expressions.Iter(fe => CheckTypeInference(fe.E));
m.Decreases.Expressions.Iter(CheckTypeInference);
if (m.Body != null) {
CheckTypeInference(m.Body);
bool tail = true;
bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail);
if (hasTailRecursionPreference && !tail) {
// the user specifically requested no tail recursion, so do nothing else
} else if (hasTailRecursionPreference && tail && m.IsGhost) {
Error(m.tok, "tail recursion can be specified only for methods that will be compiled, not for ghost methods");
} else {
var module = m.EnclosingClass.Module;
var sccSize = module.CallGraph.GetSCCSize(m);
if (hasTailRecursionPreference && 2 <= sccSize) {
Error(m.tok, "sorry, tail-call optimizations are not supported for mutually recursive methods");
} else if (hasTailRecursionPreference || sccSize == 1) {
CallStmt tailCall = null;
var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
if (status != TailRecursionStatus.NotTailRecursive) {
m.IsTailRecursive = true;
}
}
}
}
if (!m.IsTailRecursive && m.Body != null && Contract.Exists(m.Decreases.Expressions, e => e is WildcardExpr)) {
Error(m.Decreases.Expressions[0].tok, "'decreases *' is allowed only on tail-recursive methods");
}
} else if (member is Function) {
var f = (Function)member;
f.Req.Iter(CheckTypeInference);
f.Ens.Iter(CheckTypeInference);
f.Reads.Iter(fe => CheckTypeInference(fe.E));
f.Decreases.Expressions.Iter(CheckTypeInference);
if (f.Body != null) {
CheckTypeInference(f.Body);
bool tail = true;
if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) {
Error(f.tok, "sorry, tail-call functions are not supported");
}
}
}
}
}
}
}
// Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support
foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {
if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {
// do the following check once per SCC, so call it on each SCC representative
SccStratosphereCheck(dtd, datatypeDependencies);
DetermineEqualitySupport(dtd, datatypeDependencies);
}
}
// Set the SccRepr field of codatatypes
foreach (var repr in codatatypeDependencies.TopologicallySortedComponents()) {
foreach (var codt in codatatypeDependencies.GetSCC(repr)) {
codt.SscRepr = repr;
}
}
if (ErrorCount == prevErrorCount) { // because CheckCoCalls requires the given expression to have been successfully resolved
// Perform the guardedness check on co-datatypes
foreach (var fn in ModuleDefinition.AllFunctions(declarations)) {
var module = fn.EnclosingClass.Module;
if (fn.Body != null && module.CallGraph.GetSCCRepresentative(fn) == fn) {
bool dealsWithCodatatypes = false;
foreach (var m in module.CallGraph.GetSCC(fn)) {
var f = (Function)m;
if (f.ResultType.InvolvesCoDatatype) {
dealsWithCodatatypes = true;
break;
}
}
foreach (var m in module.CallGraph.GetSCC(fn)) {
var f = (Function)m;
var checker = new CoCallResolution(f, dealsWithCodatatypes);
checker.CheckCoCalls(f.Body);
}
}
}
// Inferred required equality support for datatypes and for Function and Method signatures
// First, do datatypes until a fixpoint is reached
bool inferredSomething;
do {
inferredSomething = false;
foreach (var d in declarations) {
if (d is DatatypeDecl) {
var dt = (DatatypeDecl)d;
foreach (var tp in dt.TypeArgs) {
if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
// here's our chance to infer the need for equality support
foreach (var ctor in dt.Ctors) {
foreach (var arg in ctor.Formals) {
if (InferRequiredEqualitySupport(tp, arg.Type)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
inferredSomething = true;
goto DONE_DT; // break out of the doubly-nested loop
}
}
}
DONE_DT: ;
}
}
}
}
} while (inferredSomething);
// Now do it for Function and Method signatures
foreach (var d in declarations) {
if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
foreach (var tp in iter.TypeArgs) {
if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
// here's our chance to infer the need for equality support
foreach (var p in iter.Ins) {
if (InferRequiredEqualitySupport(tp, p.Type)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
goto DONE;
}
}
foreach (var p in iter.Outs) {
if (InferRequiredEqualitySupport(tp, p.Type)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
goto DONE;
}
}
DONE: ;
}
}
} else if (d is ClassDecl) {
var cl = (ClassDecl)d;
foreach (var member in cl.Members) {
if (!member.IsGhost) {
if (member is Function) {
var f = (Function)member;
foreach (var tp in f.TypeArgs) {
if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
// here's our chance to infer the need for equality support
if (InferRequiredEqualitySupport(tp, f.ResultType)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
} else {
foreach (var p in f.Formals) {
if (InferRequiredEqualitySupport(tp, p.Type)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
break;
}
}
}
}
}
} else if (member is Method) {
var m = (Method)member;
foreach (var tp in m.TypeArgs) {
if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
// here's our chance to infer the need for equality support
foreach (var p in m.Ins) {
if (InferRequiredEqualitySupport(tp, p.Type)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
goto DONE;
}
}
foreach (var p in m.Outs) {
if (InferRequiredEqualitySupport(tp, p.Type)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
goto DONE;
}
}
DONE: ;
}
}
}
}
}
}
}
// Check that all == and != operators in non-ghost contexts are applied to equality-supporting types.
// Note that this check can only be done after determining which expressions are ghosts.
foreach (var d in declarations) {
if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
foreach (var p in iter.Ins) {
if (!p.IsGhost) {
CheckEqualityTypes_Type(p.tok, p.Type);
}
}
foreach (var p in iter.Outs) {
if (!p.IsGhost) {
CheckEqualityTypes_Type(p.tok, p.Type);
}
}
if (iter.Body != null) {
CheckEqualityTypes_Stmt(iter.Body);
}
} else if (d is ClassDecl) {
var cl = (ClassDecl)d;
foreach (var member in cl.Members) {
if (!member.IsGhost) {
if (member is Field) {
var f = (Field)member;
CheckEqualityTypes_Type(f.tok, f.Type);
} else if (member is Function) {
var f = (Function)member;
foreach (var p in f.Formals) {
if (!p.IsGhost) {
CheckEqualityTypes_Type(p.tok, p.Type);
}
}
CheckEqualityTypes_Type(f.tok, f.ResultType);
if (f.Body != null) {
CheckEqualityTypes(f.Body);
}
} else if (member is Method) {
var m = (Method)member;
foreach (var p in m.Ins) {
if (!p.IsGhost) {
CheckEqualityTypes_Type(p.tok, p.Type);
}
}
foreach (var p in m.Outs) {
if (!p.IsGhost) {
CheckEqualityTypes_Type(p.tok, p.Type);
}
}
if (m.Body != null) {
CheckEqualityTypes_Stmt(m.Body);
}
}
}
}
} else if (d is DatatypeDecl) {
var dt = (DatatypeDecl)d;
foreach (var ctor in dt.Ctors) {
foreach (var p in ctor.Formals) {
if (!p.IsGhost) {
CheckEqualityTypes_Type(p.tok, p.Type);
}
}
}
}
}
// Check that copredicates are not recursive with non-copredicate functions, and
// check that comethods are not recursive with non-comethod methods.
foreach (var d in declarations) {
if (d is ClassDecl) {
foreach (var member in ((ClassDecl)d).Members) {
if (member is CoPredicate) {
var fn = (CoPredicate)member;
// Check here for the presence of any 'ensures' clauses, which are not allowed (because we're not sure
// of their soundness)
if (fn.Ens.Count != 0) {
Error(fn.Ens[0].tok, "a copredicate is not allowed to declare any ensures clause");
}
// Also check for 'reads' clauses
if (fn.Reads.Count != 0) {
Error(fn.Reads[0].tok, "a copredicate is not allowed to declare any reads clause"); // (why?)
}
if (fn.Body != null) {
CoPredicateChecks(fn.Body, fn, CallingPosition.Positive);
}
} else if (member is CoMethod) {
var m = (CoMethod)member;
if (m.Body != null) {
CoMethodChecks(m.Body, m);
}
}
}
}
}
}
}
enum TailRecursionStatus
{
NotTailRecursive, // contains code that makes the enclosing method body not tail recursive (in way that is supported)
CanBeFollowedByAnything, // the code just analyzed does not do any recursive calls
TailCallSpent, // the method body is tail recursive, provided that all code that follows it in the method body is ghost
}
///
/// Checks if "stmts" can be considered tail recursive, and (provided "reportsError" is true) reports an error if not.
/// Note, the current implementation is rather conservative in its analysis; upon need, the
/// algorithm could be improved.
/// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method.
///
/// The incoming value of "tailCall" is not used, but it's nevertheless a 'ref' parameter to allow the
/// body to return the incoming value or to omit assignments to it.
/// If the return value is CanBeFollowedByAnything, "tailCall" is unchanged.
/// If the return value is TailCallSpent, "tailCall" shows one of the calls where the tail call was spent. (Note,
/// there could be several if the statements have branches.)
/// If the return value is NoTailRecursive, "tailCall" could be anything. In this case, an error
/// message has been reported (provided "reportsErrors" is true).
///
TailRecursionStatus CheckTailRecursive(List stmts, Method enclosingMethod, ref CallStmt tailCall, bool reportErrors) {
Contract.Requires(stmts != null);
var status = TailRecursionStatus.CanBeFollowedByAnything;
foreach (var s in stmts) {
if (!s.IsGhost) {
if (s is ReturnStmt && ((ReturnStmt)s).hiddenUpdate == null) {
return status;
}
if (status == TailRecursionStatus.TailCallSpent) {
// a tail call cannot be followed by non-ghost code
if (reportErrors) {
Error(tailCall.Tok, "this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code");
}
return TailRecursionStatus.NotTailRecursive;
}
status = CheckTailRecursive(s, enclosingMethod, ref tailCall, reportErrors);
if (status == TailRecursionStatus.NotTailRecursive) {
return status;
}
}
}
return status;
}
///
/// See CheckTailRecursive(List Statement, ...), including its description of "tailCall".
/// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method.
///
TailRecursionStatus CheckTailRecursive(Statement stmt, Method enclosingMethod, ref CallStmt tailCall, bool reportErrors) {
Contract.Requires(stmt != null && !stmt.IsGhost);
if (stmt is PrintStmt) {
} else if (stmt is BreakStmt) {
} else if (stmt is ReturnStmt) {
var s = (ReturnStmt)stmt;
if (s.hiddenUpdate != null) {
return CheckTailRecursive(s.hiddenUpdate, enclosingMethod, ref tailCall, reportErrors);
}
} else if (stmt is AssignStmt) {
} else if (stmt is VarDecl) {
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
if (s.Method == enclosingMethod) {
// It's a recursive call. It can be considered a tail call only if the LHS of the call are the
// formal out-parameters of the method
for (int i = 0; i < s.Lhs.Count; i++) {
var formal = enclosingMethod.Outs[i];
if (!formal.IsGhost) {
var lhs = s.Lhs[i] as IdentifierExpr;
if (lhs != null && lhs.Var == formal) {
// all is good
} else {
if (reportErrors) {
Error(s.Tok, "the recursive call to '{0}' is not tail recursive because the actual out-parameter {1} is not the formal out-parameter '{2}'", s.Method.Name, i, formal.Name);
}
return TailRecursionStatus.NotTailRecursive;
}
}
}
tailCall = s;
return TailRecursionStatus.TailCallSpent;
}
} else if (stmt is BlockStmt) {
var s = (BlockStmt)stmt;
return CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);
} else if (stmt is IfStmt) {
var s = (IfStmt)stmt;
var stThen = CheckTailRecursive(s.Thn, enclosingMethod, ref tailCall, reportErrors);
if (stThen == TailRecursionStatus.NotTailRecursive) {
return stThen;
}
var stElse = s.Els == null ? TailRecursionStatus.CanBeFollowedByAnything : CheckTailRecursive(s.Els, enclosingMethod, ref tailCall, reportErrors);
if (stElse == TailRecursionStatus.NotTailRecursive) {
return stElse;
} else if (stThen == TailRecursionStatus.TailCallSpent || stElse == TailRecursionStatus.TailCallSpent) {
return TailRecursionStatus.TailCallSpent;
}
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
var status = TailRecursionStatus.CanBeFollowedByAnything;
foreach (var alt in s.Alternatives) {
var st = CheckTailRecursive(alt.Body, enclosingMethod, ref tailCall, reportErrors);
if (st == TailRecursionStatus.NotTailRecursive) {
return st;
} else if (st == TailRecursionStatus.TailCallSpent) {
status = st;
}
}
return status;
} else if (stmt is WhileStmt) {
var s = (WhileStmt)stmt;
var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);
if (status != TailRecursionStatus.CanBeFollowedByAnything) {
if (status == TailRecursionStatus.NotTailRecursive) {
// an error has already been reported
} else if (reportErrors) {
Error(tailCall.Tok, "a recursive call inside a loop is not recognized as being a tail call");
}
return TailRecursionStatus.NotTailRecursive;
}
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
foreach (var alt in s.Alternatives) {
var status = CheckTailRecursive(alt.Body, enclosingMethod, ref tailCall, reportErrors);
if (status != TailRecursionStatus.CanBeFollowedByAnything) {
if (status == TailRecursionStatus.NotTailRecursive) {
// an error has already been reported
} else if (reportErrors) {
Error(tailCall.Tok, "a recursive call inside a loop is not recognized as being a tail call");
}
return TailRecursionStatus.NotTailRecursive;
}
}
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);
if (status != TailRecursionStatus.CanBeFollowedByAnything) {
if (status == TailRecursionStatus.NotTailRecursive) {
// an error has already been reported
} else if (reportErrors) {
Error(tailCall.Tok, "a recursive call inside a forall statement is not a tail call");
}
return TailRecursionStatus.NotTailRecursive;
}
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
var status = TailRecursionStatus.CanBeFollowedByAnything;
foreach (var kase in s.Cases) {
var st = CheckTailRecursive(kase.Body, enclosingMethod, ref tailCall, reportErrors);
if (st == TailRecursionStatus.NotTailRecursive) {
return st;
} else if (st == TailRecursionStatus.TailCallSpent) {
status = st;
}
}
return status;
} else if (stmt is AssignSuchThatStmt) {
} else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
return CheckTailRecursive(s.ResolvedStatements, enclosingMethod, ref tailCall, reportErrors);
} else {
Contract.Assert(false); // unexpected statement type
}
return TailRecursionStatus.CanBeFollowedByAnything;
}
enum CallingPosition { Positive, Negative, Neither }
static CallingPosition Invert(CallingPosition cp) {
switch (cp) {
case CallingPosition.Positive: return CallingPosition.Negative;
case CallingPosition.Negative: return CallingPosition.Positive;
default: return CallingPosition.Neither;
}
}
void CoPredicateChecks(Expression expr, CoPredicate context, CallingPosition cp) {
Contract.Requires(expr != null);
Contract.Requires(context != null);
if (expr is ConcreteSyntaxExpression) {
var e = (ConcreteSyntaxExpression)expr;
CoPredicateChecks(e.Resolved, context, cp);
return;
} else if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
var moduleCaller = context.EnclosingClass.Module;
var moduleCallee = e.Function.EnclosingClass.Module;
if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) {
// we're looking at a recursive call
if (!(e.Function is CoPredicate)) {
Error(e, "a recursive call from a copredicate can go only to other copredicates");
} else if (cp != CallingPosition.Positive) {
var msg = "a recursive copredicate call can only be done in positive positions";
if (cp == CallingPosition.Neither) {
// this may be inside a
msg += " and cannot sit inside an existential quantifier";
} else {
// the co-call is not inside an existential quantifier, so don't bother mentioning the part of existentials in the error message
}
Error(e, msg);
} else {
e.CoCall = FunctionCallExpr.CoCallResolution.Yes;
}
}
// fall through to do the subexpressions
} else if (expr is UnaryExpr) {
var e = (UnaryExpr)expr;
if (e.Op == UnaryExpr.Opcode.Not) {
CoPredicateChecks(e.E, context, Invert(cp));
return;
}
} else if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
switch (e.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.And:
case BinaryExpr.ResolvedOpcode.Or:
CoPredicateChecks(e.E0, context, cp);
CoPredicateChecks(e.E1, context, cp);
return;
case BinaryExpr.ResolvedOpcode.Imp:
CoPredicateChecks(e.E0, context, Invert(cp));
CoPredicateChecks(e.E1, context, cp);
return;
default:
break;
}
} else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
CoPredicateChecks(e.Source, context, CallingPosition.Neither);
e.Cases.Iter(kase => CoPredicateChecks(kase.Body, context, cp));
return;
} else if (expr is ITEExpr) {
var e = (ITEExpr)expr;
CoPredicateChecks(e.Test, context, CallingPosition.Neither);
CoPredicateChecks(e.Thn, context, cp);
CoPredicateChecks(e.Els, context, cp);
return;
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
foreach (var rhs in e.RHSs) {
CoPredicateChecks(rhs, context, CallingPosition.Neither);
}
// note, a let-such-that expression introduces an existential that may depend on the _k in a copredicate, so we disallow recursive copredicate calls in the body of the let-such-that
CoPredicateChecks(e.Body, context, e.Exact ? cp : CallingPosition.Neither);
return;
} else if (expr is QuantifierExpr) {
var e = (QuantifierExpr)expr;
if ((cp == CallingPosition.Positive && e is ExistsExpr) || (cp == CallingPosition.Negative && e is ForallExpr)) {
// Don't allow any co-recursive calls under an existential, because that can be unsound.
// (Actually, I think we could be more liberal here--we could allow this if the range is finite.)
cp = CallingPosition.Neither;
}
if (e.Range != null) {
CoPredicateChecks(e.Range, context, e is ExistsExpr ? Invert(cp) : cp);
}
CoPredicateChecks(e.Term, context, cp);
return;
}
expr.SubExpressions.Iter(ee => CoPredicateChecks(ee, context, CallingPosition.Neither));
}
void CoMethodChecks(Statement stmt, CoMethod context) {
Contract.Requires(stmt != null);
Contract.Requires(context != null);
if (stmt is CallStmt) {
var s = (CallStmt)stmt;
if (s.Method is CoMethod || s.Method is PrefixMethod) {
// all is cool
} else {
// the call goes from a comethod context to a non-comethod callee
var moduleCaller = context.EnclosingClass.Module;
var moduleCallee = s.Method.EnclosingClass.Module;
if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) {
// we're looking at a recursive call (to a non-comethod)
Error(s, "a recursive call from a comethod can go only to other comethods and prefix methods");
}
}
} else {
stmt.SubStatements.Iter(ss => CoMethodChecks(ss, context));
}
}
void CheckEqualityTypes_Stmt(Statement stmt) {
Contract.Requires(stmt != null);
if (stmt.IsGhost) {
return;
} else if (stmt is PrintStmt) {
var s = (PrintStmt)stmt;
foreach (var arg in s.Args) {
if (arg.E != null) {
CheckEqualityTypes(arg.E);
}
}
} else if (stmt is BreakStmt) {
} else if (stmt is ProduceStmt) {
var s = (ProduceStmt)stmt;
if (s.rhss != null) {
s.rhss.Iter(CheckEqualityTypes_Rhs);
}
} else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
CheckEqualityTypes(s.Lhs);
CheckEqualityTypes_Rhs(s.Rhs);
} else if (stmt is VarDecl) {
var s = (VarDecl)stmt;
s.SubStatements.Iter(CheckEqualityTypes_Stmt);
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
CheckEqualityTypes(s.Receiver);
s.Args.Iter(CheckEqualityTypes);
s.Lhs.Iter(CheckEqualityTypes);
Contract.Assert(s.Method.TypeArgs.Count <= s.TypeArgumentSubstitutions.Count);
var i = 0;
foreach (var formalTypeArg in s.Method.TypeArgs) {
var actualTypeArg = s.TypeArgumentSubstitutions[formalTypeArg];
if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {
Error(s.Tok, "type parameter {0} ({1}) passed to method {2} must support equality (got {3}){4}", i, formalTypeArg.Name, s.Method.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));
}
i++;
}
} else if (stmt is BlockStmt) {
var s = (BlockStmt)stmt;
s.Body.Iter(CheckEqualityTypes_Stmt);
} else if (stmt is IfStmt) {
var s = (IfStmt)stmt;
if (s.Guard != null) {
CheckEqualityTypes(s.Guard);
}
s.SubStatements.Iter(CheckEqualityTypes_Stmt);
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
foreach (var alt in s.Alternatives) {
CheckEqualityTypes(alt.Guard);
alt.Body.Iter(CheckEqualityTypes_Stmt);
}
} else if (stmt is WhileStmt) {
var s = (WhileStmt)stmt;
if (s.Guard != null) {
CheckEqualityTypes(s.Guard);
}
CheckEqualityTypes_Stmt(s.Body);
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
foreach (var alt in s.Alternatives) {
CheckEqualityTypes(alt.Guard);
alt.Body.Iter(CheckEqualityTypes_Stmt);
}
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
CheckEqualityTypes(s.Range);
CheckEqualityTypes_Stmt(s.Body);
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
CheckEqualityTypes(s.Source);
foreach (MatchCaseStmt mc in s.Cases) {
mc.Body.Iter(CheckEqualityTypes_Stmt);
}
} else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
s.ResolvedStatements.Iter(CheckEqualityTypes_Stmt);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
}
void CheckEqualityTypes_Rhs(AssignmentRhs rhs) {
Contract.Requires(rhs != null);
rhs.SubExpressions.Iter(CheckEqualityTypes);
rhs.SubStatements.Iter(CheckEqualityTypes_Stmt);
}
void CheckEqualityTypes(Expression expr) {
Contract.Requires(expr != null);
if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
var t0 = e.E0.Type.Normalize();
var t1 = e.E1.Type.Normalize();
switch (e.Op) {
case BinaryExpr.Opcode.Eq:
case BinaryExpr.Opcode.Neq:
// First, check a special case: a datatype value (like Nil) that takes no parameters
var e0 = e.E0.Resolved as DatatypeValue;
var e1 = e.E1.Resolved as DatatypeValue;
if (e0 != null && e0.Arguments.Count == 0) {
// that's cool
} else if (e1 != null && e1.Arguments.Count == 0) {
// oh yeah!
} else if (!t0.SupportsEquality) {
Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
} else if (!t1.SupportsEquality) {
Error(e.E1, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));
}
break;
default:
switch (e.ResolvedOp) {
// Note, all operations on sets, multisets, and maps are guaranteed to work because of restrictions placed on how
// these types are instantiated. (Except: This guarantee does not apply to equality on maps, because the Range type
// of maps is not restricted, only the Domain type. However, the equality operator is checked above.)
case BinaryExpr.ResolvedOpcode.InSeq:
case BinaryExpr.ResolvedOpcode.NotInSeq:
case BinaryExpr.ResolvedOpcode.Prefix:
case BinaryExpr.ResolvedOpcode.ProperPrefix:
if (!t1.SupportsEquality) {
Error(e.E1, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));
} else if (!t0.SupportsEquality) {
if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet || e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSeq) {
Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
} else {
Error(e.E0, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
}
}
break;
default:
break;
}
break;
}
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
foreach (var bv in e.BoundVars) {
CheckEqualityTypes_Type(bv.tok, bv.Type);
}
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
foreach (var bv in e.Vars) {
CheckEqualityTypes_Type(bv.tok, bv.Type);
}
} else if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
Contract.Assert(e.Function.TypeArgs.Count <= e.TypeArgumentSubstitutions.Count);
var i = 0;
foreach (var formalTypeArg in e.Function.TypeArgs) {
var actualTypeArg = e.TypeArgumentSubstitutions[formalTypeArg];
if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {
Error(e.tok, "type parameter {0} ({1}) passed to function {2} must support equality (got {3}){4}", i, formalTypeArg.Name, e.Function.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));
}
i++;
}
}
foreach (var ee in expr.SubExpressions) {
CheckEqualityTypes(ee);
}
}
void CheckEqualityTypes_Type(IToken tok, Type type) {
Contract.Requires(tok != null);
Contract.Requires(type != null);
type = type.Normalize();
if (type is BasicType) {
// fine
} else if (type is SetType) {
var argType = ((SetType)type).Arg;
if (!argType.SupportsEquality) {
Error(tok, "set argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));
}
CheckEqualityTypes_Type(tok, argType);
} else if (type is MultiSetType) {
var argType = ((MultiSetType)type).Arg;
if (!argType.SupportsEquality) {
Error(tok, "multiset argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));
}
CheckEqualityTypes_Type(tok, argType);
} else if (type is MapType) {
var mt = (MapType)type;
if (!mt.Domain.SupportsEquality) {
Error(tok, "map domain type must support equality (got {0}){1}", mt.Domain, TypeEqualityErrorMessageHint(mt.Domain));
}
CheckEqualityTypes_Type(tok, mt.Domain);
CheckEqualityTypes_Type(tok, mt.Range);
} else if (type is SeqType) {
Type argType = ((SeqType)type).Arg;
CheckEqualityTypes_Type(tok, argType);
} else if (type is UserDefinedType) {
var udt = (UserDefinedType)type;
if (udt.ResolvedClass != null) {
Contract.Assert(udt.ResolvedClass.TypeArgs.Count == udt.TypeArgs.Count);
var i = 0;
foreach (var argType in udt.TypeArgs) {
var formalTypeArg = udt.ResolvedClass.TypeArgs[i];
if (formalTypeArg.MustSupportEquality && !argType.SupportsEquality) {
Error(tok, "type parameter {0} ({1}) passed to type {2} must support equality (got {3}){4}", i, formalTypeArg.Name, udt.ResolvedClass.Name, argType, TypeEqualityErrorMessageHint(argType));
}
CheckEqualityTypes_Type(tok, argType);
i++;
}
} else {
Contract.Assert(udt.TypeArgs.Count == 0); // TypeParameters have no type arguments
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
void CheckTypeIsDetermined(IToken tok, Type t, string what) {
Contract.Requires(tok != null);
Contract.Requires(t != null);
Contract.Requires(what != null);
t = t.Normalize();
if (t is TypeProxy && !(t is InferredTypeProxy || t is ParamTypeProxy || t is ObjectTypeProxy)) {
Error(tok, "the type of this {0} is underspecified, but it cannot be an arbitrary type.", what);
}
}
void CheckTypeInference(Expression e) {
if (e == null) return;
e.SubExpressions.Iter(CheckTypeInference);
var ce = e as ComprehensionExpr;
if (ce != null) {
foreach (var bv in ce.BoundVars) {
if (bv.Type.Normalize() is TypeProxy) {
Error(bv.tok, "type of bound variable '{0}' could not determined; please specify the type explicitly", bv.Name);
}
}
}
CheckTypeIsDetermined(e.tok, e.Type, "expression");
}
void CheckTypeInference(Statement stmt) {
Contract.Requires(stmt != null);
if (stmt is PrintStmt) {
var s = (PrintStmt)stmt;
s.Args.Iter(arg => CheckTypeInference(arg.E));
} else if (stmt is BreakStmt) {
} else if (stmt is ProduceStmt) {
var s = (ProduceStmt)stmt;
if (s.rhss != null) {
s.rhss.Iter(rhs => rhs.SubExpressions.Iter(e => CheckTypeInference(e)));
}
} else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
CheckTypeInference(s.Lhs);
s.Rhs.SubExpressions.Iter(e => { CheckTypeInference(e); });
} else if (stmt is VarDecl) {
var s = (VarDecl)stmt;
s.SubStatements.Iter(CheckTypeInference);
CheckTypeIsDetermined(s.Tok, s.Type, "local variable");
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
CheckTypeInference(s.Receiver);
s.Args.Iter(e => CheckTypeInference(e));
s.Lhs.Iter(e => CheckTypeInference(e));
} else if (stmt is BlockStmt) {
var s = (BlockStmt)stmt;
s.Body.Iter(CheckTypeInference);
} else if (stmt is IfStmt) {
var s = (IfStmt)stmt;
if (s.Guard != null) {
CheckTypeInference(s.Guard);
}
s.SubStatements.Iter(CheckTypeInference);
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
foreach (var alt in s.Alternatives) {
CheckTypeInference(alt.Guard);
alt.Body.Iter(CheckTypeInference);
}
} else if (stmt is WhileStmt) {
var s = (WhileStmt)stmt;
if (s.Guard != null) {
CheckTypeInference(s.Guard);
}
CheckTypeInference(s.Body);
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
foreach (var alt in s.Alternatives) {
CheckTypeInference(alt.Guard);
alt.Body.Iter(CheckTypeInference);
}
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
CheckTypeInference(s.Range);
CheckTypeInference(s.Body);
s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));
} else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
s.SubExpressions.Iter(e => CheckTypeInference(e));
s.SubStatements.Iter(CheckTypeInference);
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
CheckTypeInference(s.Source);
foreach (MatchCaseStmt mc in s.Cases) {
mc.Body.Iter(CheckTypeInference);
}
} else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
s.ResolvedStatements.Iter(CheckTypeInference);
} else if (stmt is PredicateStmt) {
CheckTypeInference(((PredicateStmt)stmt).Expr);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
}
string TypeEqualityErrorMessageHint(Type argType) {
Contract.Requires(argType != null);
var tp = argType.AsTypeParameter;
if (tp != null) {
return string.Format(" (perhaps try declaring type parameter '{0}' on line {1} as '{0}(==)', which says it can only be instantiated with a type that supports equality)", tp.Name, tp.tok.line);
}
return "";
}
bool InferRequiredEqualitySupport(TypeParameter tp, Type type) {
Contract.Requires(tp != null);
Contract.Requires(type != null);
type = type.Normalize();
if (type is BasicType) {
} else if (type is SetType) {
var st = (SetType)type;
return st.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, st.Arg);
} else if (type is MultiSetType) {
var ms = (MultiSetType)type;
return ms.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, ms.Arg);
} else if (type is MapType) {
var mt = (MapType)type;
return mt.Domain.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, mt.Domain) || InferRequiredEqualitySupport(tp, mt.Range);
} else if (type is SeqType) {
var sq = (SeqType)type;
return InferRequiredEqualitySupport(tp, sq.Arg);
} else if (type is UserDefinedType) {
var udt = (UserDefinedType)type;
if (udt.ResolvedClass != null) {
var i = 0;
foreach (var argType in udt.TypeArgs) {
var formalTypeArg = udt.ResolvedClass.TypeArgs[i];
if ((formalTypeArg.MustSupportEquality && argType.AsTypeParameter == tp) || InferRequiredEqualitySupport(tp, argType)) {
return true;
}
i++;
}
} else {
Contract.Assert(udt.TypeArgs.Count == 0); // TypeParameters have no type arguments
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
return false;
}
ClassDecl currentClass;
Function currentFunction;
readonly Scope/*!*/ allTypeParameters = new Scope();
readonly Scope/*!*/ scope = new Scope();
Scope/*!*/ labeledStatements = new Scope();
List loopStack = new List(); // the enclosing loops (from which it is possible to break out)
readonly Dictionary inSpecOnlyContext = new Dictionary(); // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
///
/// Assumes type parameters have already been pushed
///
void ResolveClassMemberTypes(ClassDecl/*!*/ cl) {
Contract.Requires(cl != null);
Contract.Requires(currentClass == null);
Contract.Ensures(currentClass == null);
currentClass = cl;
foreach (MemberDecl member in cl.Members) {
member.EnclosingClass = cl;
if (member is Field) {
ResolveType(member.tok, ((Field)member).Type, ResolveTypeOption.DontInfer, null);
} else if (member is Function) {
var f = (Function)member;
var ec = ErrorCount;
allTypeParameters.PushMarker();
ResolveTypeParameters(f.TypeArgs, true, f);
ResolveFunctionSignature(f);
allTypeParameters.PopMarker();
if (f is CoPredicate && ec == ErrorCount) {
var ff = ((CoPredicate)f).PrefixPredicate;
ff.EnclosingClass = cl;
allTypeParameters.PushMarker();
ResolveTypeParameters(ff.TypeArgs, true, ff);
ResolveFunctionSignature(ff);
allTypeParameters.PopMarker();
}
} else if (member is Method) {
var m = (Method)member;
var ec = ErrorCount;
allTypeParameters.PushMarker();
ResolveTypeParameters(m.TypeArgs, true, m);
ResolveMethodSignature(m);
allTypeParameters.PopMarker();
var com = m as CoMethod;
if (com != null && com.PrefixMethod != null && ec == ErrorCount) {
var mm = com.PrefixMethod;
// resolve signature of the prefix method
mm.EnclosingClass = cl;
allTypeParameters.PushMarker();
ResolveTypeParameters(mm.TypeArgs, true, mm);
ResolveMethodSignature(mm);
allTypeParameters.PopMarker();
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type
}
}
currentClass = null;
}
///
/// Assumes type parameters have already been pushed, and that all types in class members have been resolved
///
void ResolveClassMemberBodies(ClassDecl cl) {
Contract.Requires(cl != null);
Contract.Requires(currentClass == null);
Contract.Ensures(currentClass == null);
currentClass = cl;
foreach (MemberDecl member in cl.Members) {
if (member is Field) {
ResolveAttributes(member.Attributes, false, new NoContext(currentClass.Module));
// nothing more to do
} else if (member is Function) {
var f = (Function)member;
var ec = ErrorCount;
allTypeParameters.PushMarker();
ResolveTypeParameters(f.TypeArgs, false, f);
ResolveFunction(f);
allTypeParameters.PopMarker();
if (f is CoPredicate && ec == ErrorCount) {
var ff = ((CoPredicate)f).PrefixPredicate;
allTypeParameters.PushMarker();
ResolveTypeParameters(ff.TypeArgs, false, ff);
ResolveFunction(ff);
allTypeParameters.PopMarker();
}
} else if (member is Method) {
var m = (Method)member;
var ec = ErrorCount;
allTypeParameters.PushMarker();
ResolveTypeParameters(m.TypeArgs, false, m);
ResolveMethod(m);
allTypeParameters.PopMarker();
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type
}
}
currentClass = null;
}
///
/// Assumes type parameters have already been pushed
///
void ResolveCtorTypes(DatatypeDecl/*!*/ dt, Graph/*!*/ dependencies, Graph/*!*/ coDependencies) {
Contract.Requires(dt != null);
Contract.Requires(dependencies != null);
Contract.Requires(coDependencies != null);
foreach (DatatypeCtor ctor in dt.Ctors) {
ctor.EnclosingDatatype = dt;
allTypeParameters.PushMarker();
ResolveCtorSignature(ctor, dt.TypeArgs);
allTypeParameters.PopMarker();
if (dt is IndDatatypeDecl) {
// The dependencies of interest among inductive datatypes are all (inductive data)types mentioned in the parameter types
var idt = (IndDatatypeDecl)dt;
dependencies.AddVertex(idt);
foreach (Formal p in ctor.Formals) {
AddDatatypeDependencyEdge(idt, p.Type, dependencies);
}
} else {
// The dependencies of interest among codatatypes are just the top-level types of parameters.
var codt = (CoDatatypeDecl)dt;
coDependencies.AddVertex(codt);
foreach (var p in ctor.Formals) {
var co = p.Type.AsCoDatatype;
if (co != null && codt.Module == co.Module) {
coDependencies.AddEdge(codt, co);
}
}
}
}
}
void AddDatatypeDependencyEdge(IndDatatypeDecl/*!*/ dt, Type/*!*/ tp, Graph/*!*/ dependencies) {
Contract.Requires(dt != null);
Contract.Requires(tp != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
var dependee = tp.AsIndDatatype;
if (dependee != null && dt.Module == dependee.Module) {
dependencies.AddEdge(dt, dependee);
foreach (var ta in ((UserDefinedType)tp).TypeArgs) {
AddDatatypeDependencyEdge(dt, ta, dependencies);
}
}
}
///
/// Check that the SCC of 'startingPoint' can be carved up into stratospheres in such a way that each
/// datatype has some value that can be constructed from datatypes in lower stratospheres only.
/// The algorithm used here is quadratic in the number of datatypes in the SCC. Since that number is
/// deemed to be rather small, this seems okay.
///
/// As a side effect of this checking, the DefaultCtor field is filled in (for every inductive datatype
/// that passes the check). It may be that several constructors could be used as the default, but
/// only the first one encountered as recorded. This particular choice is slightly more than an
/// implementation detail, because it affects how certain cycles among inductive datatypes (having
/// to do with the types used to instantiate type parameters of datatypes) are used.
///
/// The role of the SCC here is simply to speed up this method. It would still be correct if the
/// equivalence classes in the given SCC were unions of actual SCC's. In particular, this method
/// would still work if "dependencies" consisted of one large SCC containing all the inductive
/// datatypes in the module.
///
void SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph/*!*/ dependencies) {
Contract.Requires(startingPoint != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
var scc = dependencies.GetSCC(startingPoint);
int totalCleared = 0;
while (true) {
int clearedThisRound = 0;
foreach (var dt in scc) {
if (dt.DefaultCtor != null) {
// previously cleared
} else if (ComputeDefaultCtor(dt)) {
Contract.Assert(dt.DefaultCtor != null); // should have been set by the successful call to StratosphereCheck)
clearedThisRound++;
totalCleared++;
}
}
if (totalCleared == scc.Count) {
// all is good
return;
} else if (clearedThisRound != 0) {
// some progress was made, so let's keep going
} else {
// whatever is in scc-cleared now failed to pass the test
foreach (var dt in scc) {
if (dt.DefaultCtor == null) {
Error(dt, "because of cyclic dependencies among constructor argument types, no instances of datatype '{0}' can be constructed", dt.Name);
}
}
return;
}
}
}
///
/// Check that the datatype has some constructor all whose argument types can be constructed.
/// Returns 'true' and sets dt.DefaultCtor if that is the case.
///
bool ComputeDefaultCtor(IndDatatypeDecl dt) {
Contract.Requires(dt != null);
Contract.Requires(dt.DefaultCtor == null); // the intention is that this method be called only when DefaultCtor hasn't already been set
Contract.Ensures(!Contract.Result() || dt.DefaultCtor != null);
// Stated differently, check that there is some constuctor where no argument type goes to the same stratum.
foreach (DatatypeCtor ctor in dt.Ctors) {
var typeParametersUsed = new List();
foreach (Formal p in ctor.Formals) {
if (!CheckCanBeConstructed(p.Type, typeParametersUsed)) {
// the argument type (has a component which) is not yet known to be constructable
goto NEXT_OUTER_ITERATION;
}
}
// this constructor satisfies the requirements, so the datatype is allowed
dt.DefaultCtor = ctor;
dt.TypeParametersUsedInConstructionByDefaultCtor = new bool[dt.TypeArgs.Count];
for (int i = 0; i < dt.TypeArgs.Count; i++) {
dt.TypeParametersUsedInConstructionByDefaultCtor[i] = typeParametersUsed.Contains(dt.TypeArgs[i]);
}
return true;
NEXT_OUTER_ITERATION: { }
}
// no constructor satisfied the requirements, so this is an illegal datatype declaration
return false;
}
bool CheckCanBeConstructed(Type tp, List typeParametersUsed) {
var dependee = tp.AsIndDatatype;
if (dependee == null) {
// the type is not an inductive datatype, which means it is always possible to construct it
if (tp.IsTypeParameter) {
typeParametersUsed.Add(((UserDefinedType)tp).ResolvedParam);
}
return true;
} else if (dependee.DefaultCtor == null) {
// the type is an inductive datatype that we don't yet know how to construct
return false;
}
// also check the type arguments of the inductive datatype
Contract.Assert(((UserDefinedType)tp).TypeArgs.Count == dependee.TypeParametersUsedInConstructionByDefaultCtor.Length);
var i = 0;
foreach (var ta in ((UserDefinedType)tp).TypeArgs) { // note, "tp" is known to be a UserDefinedType, because that follows from tp being an inductive datatype
if (dependee.TypeParametersUsedInConstructionByDefaultCtor[i] && !CheckCanBeConstructed(ta, typeParametersUsed)) {
return false;
}
i++;
}
return true;
}
void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph/*!*/ dependencies) {
Contract.Requires(startingPoint != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
var scc = dependencies.GetSCC(startingPoint);
// First, the simple case: If any parameter of any inductive datatype in the SCC is of a codatatype type, then
// the whole SCC is incapable of providing the equality operation.
foreach (var dt in scc) {
Contract.Assume(dt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed);
foreach (var ctor in dt.Ctors) {
foreach (var arg in ctor.Formals) {
var anotherIndDt = arg.Type.AsIndDatatype;
if ((anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || arg.Type.IsCoDatatype) {
// arg.Type is known never to support equality
// So, go around the entire SCC and record what we learnt
foreach (var ddtt in scc) {
ddtt.EqualitySupport = IndDatatypeDecl.ES.Never;
}
return; // we are done
}
}
}
}
// Now for the more involved case: we need to determine which type parameters determine equality support for each datatype in the SCC
// We start by seeing where each datatype's type parameters are used in a place known to determine equality support.
bool thingsChanged = false;
foreach (var dt in scc) {
if (dt.TypeArgs.Count == 0) {
// if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors
continue;
}
foreach (var ctor in dt.Ctors) {
foreach (var arg in ctor.Formals) {
var typeArg = arg.Type.AsTypeParameter;
if (typeArg != null) {
typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
thingsChanged = true;
} else {
var otherDt = arg.Type.AsIndDatatype;
if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) { // datatype is in a different SCC
var otherUdt = (UserDefinedType)arg.Type.Normalize();
var i = 0;
foreach (var otherTp in otherDt.TypeArgs) {
if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
var tp = otherUdt.TypeArgs[i].AsTypeParameter;
if (tp != null) {
tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
thingsChanged = true;
}
}
}
}
}
}
}
}
// Then we propagate this information up through the SCC
while (thingsChanged) {
thingsChanged = false;
foreach (var dt in scc) {
if (dt.TypeArgs.Count == 0) {
// if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors
continue;
}
foreach (var ctor in dt.Ctors) {
foreach (var arg in ctor.Formals) {
var otherDt = arg.Type.AsIndDatatype;
if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed) { // otherDt lives in the same SCC
var otherUdt = (UserDefinedType)arg.Type.Normalize();
var i = 0;
foreach (var otherTp in otherDt.TypeArgs) {
if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
var tp = otherUdt.TypeArgs[i].AsTypeParameter;
if (tp != null && !tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
thingsChanged = true;
}
}
i++;
}
}
}
}
}
}
// Now that we have computed the .NecessaryForEqualitySupportOfSurroundingInductiveDatatype values, mark the datatypes as ones
// where equality support should be checked by looking at the type arguments.
foreach (var dt in scc) {
dt.EqualitySupport = IndDatatypeDecl.ES.ConsultTypeArguments;
}
}
void ResolveAttributes(Attributes attrs, bool twoState, ICodeContext codeContext) {
// order does not matter much for resolution, so resolve them in reverse order
for (; attrs != null; attrs = attrs.Prev) {
if (attrs.Args != null) {
ResolveAttributeArgs(attrs.Args, twoState, codeContext, true);
}
}
}
void ResolveAttributeArgs(List/*!*/ args, bool twoState, ICodeContext codeContext, bool allowGhosts) {
Contract.Requires(args != null);
foreach (Attributes.Argument aa in args) {
Contract.Assert(aa != null);
if (aa.E != null) {
ResolveExpression(aa.E, twoState, codeContext);
if (!allowGhosts) {
CheckIsNonGhost(aa.E);
}
}
}
}
void ResolveTypeParameters(List/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {
Contract.Requires(tparams != null);
Contract.Requires(parent != null);
// push non-duplicated type parameter names
int index = 0;
foreach (TypeParameter tp in tparams) {
Contract.Assert(tp != null);
if (emitErrors) {
// we're seeing this TypeParameter for the first time
tp.Parent = parent;
tp.PositionalIndex = index;
}
if (!allTypeParameters.Push(tp.Name, tp) && emitErrors) {
Error(tp, "Duplicate type-parameter name: {0}", tp.Name);
}
}
}
///
/// Assumes type parameters have already been pushed
///
void ResolveFunctionSignature(Function f) {
Contract.Requires(f != null);
scope.PushMarker();
if (f.SignatureIsOmitted) {
Error(f, "function signature can be omitted only in refining functions");
}
var option = f.TypeArgs.Count == 0 ? ResolveTypeOption.AllowPrefixExtend : ResolveTypeOption.AllowPrefix;
foreach (Formal p in f.Formals) {
if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
ResolveType(p.tok, p.Type, option, f.TypeArgs);
}
ResolveType(f.tok, f.ResultType, option, f.TypeArgs);
scope.PopMarker();
}
///
/// Assumes type parameters have already been pushed
///
void ResolveFunction(Function f) {
Contract.Requires(f != null);
Contract.Requires(currentFunction == null);
Contract.Ensures(currentFunction == null);
scope.PushMarker();
currentFunction = f;
if (f.IsStatic) {
scope.AllowInstance = false;
}
foreach (Formal p in f.Formals) {
scope.Push(p.Name, p);
}
ResolveAttributes(f.Attributes, false, new NoContext(currentClass.Module));
foreach (Expression r in f.Req) {
ResolveExpression(r, false, new NoContext(currentFunction.EnclosingClass.Module));
Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(r.Type, Type.Bool)) {
Error(r, "Precondition must be a boolean (got {0})", r.Type);
}
}
foreach (FrameExpression fr in f.Reads) {
ResolveFrameExpression(fr, "reads");
}
foreach (Expression r in f.Ens) {
ResolveExpression(r, false, new NoContext(currentClass.Module)); // since this is a function, the postcondition is still a one-state predicate
Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(r.Type, Type.Bool)) {
Error(r, "Postcondition must be a boolean (got {0})", r.Type);
}
}
foreach (Expression r in f.Decreases.Expressions) {
ResolveExpression(r, false, new NoContext(currentClass.Module));
// any type is fine
}
if (f.Body != null) {
var prevErrorCount = ErrorCount;
List matchVarContext = new List(f.Formals);
ResolveExpression(f.Body, false, new NoContext(currentClass.Module), matchVarContext);
if (!f.IsGhost) {
CheckIsNonGhost(f.Body);
}
Contract.Assert(f.Body.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(f.Body.Type, f.ResultType)) {
Error(f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
}
}
currentFunction = null;
scope.PopMarker();
}
void ResolveFrameExpression(FrameExpression fe, string kind) {
Contract.Requires(fe != null);
Contract.Requires(kind != null);
ResolveExpression(fe.E, false, new NoContext(moduleInfo.ModuleDef));
Type t = fe.E.Type;
Contract.Assert(t != null); // follows from postcondition of ResolveExpression
if (t is CollectionType) {
t = ((CollectionType)t).Arg;
}
if (t is ObjectType) {
// fine, as long as there's no field name
if (fe.FieldName != null) {
Error(fe.E, "type '{0}' does not contain a field named '{1}'", t, fe.FieldName);
}
} else if (UserDefinedType.DenotesClass(t) != null) {
// fine type
if (fe.FieldName != null) {
NonProxyType nptype;
MemberDecl member = ResolveMember(fe.E.tok, t, fe.FieldName, out nptype);
UserDefinedType ctype = (UserDefinedType)nptype; // correctness of cast follows from the DenotesClass test above
if (member == null) {
// error has already been reported by ResolveMember
} else if (!(member is Field)) {
Error(fe.E, "member {0} in type {1} does not refer to a field", fe.FieldName, cce.NonNull(ctype).Name);
} else {
Contract.Assert(ctype != null && ctype.ResolvedClass != null); // follows from postcondition of ResolveMember
fe.Field = (Field)member;
}
}
} else {
Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type);
}
}
///
/// Assumes type parameters have already been pushed
///
void ResolveMethodSignature(Method m) {
Contract.Requires(m != null);
scope.PushMarker();
if (m.SignatureIsOmitted) {
Error(m, "method signature can be omitted only in refining methods");
}
var option = m.TypeArgs.Count == 0 ? ResolveTypeOption.AllowPrefixExtend : ResolveTypeOption.AllowPrefix;
// resolve in-parameters
foreach (Formal p in m.Ins) {
if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
ResolveType(p.tok, p.Type, option, m.TypeArgs);
}
// resolve out-parameters
foreach (Formal p in m.Outs) {
if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
ResolveType(p.tok, p.Type, option, m.TypeArgs);
}
scope.PopMarker();
}
///
/// Assumes type parameters have already been pushed
///
void ResolveMethod(Method m) {
Contract.Requires(m != null);
// Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported
scope.PushMarker();
if (m.IsStatic) {
scope.AllowInstance = false;
}
foreach (Formal p in m.Ins) {
scope.Push(p.Name, p);
}
// Start resolving specification...
foreach (MaybeFreeExpression e in m.Req) {
ResolveExpression(e.E, false, m);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E.Type, Type.Bool)) {
Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);
}
}
foreach (FrameExpression fe in m.Mod.Expressions) {
ResolveFrameExpression(fe, "modifies");
if (m is CoMethod) {
Error(fe.tok, "comethods are not allowed to have modifies clauses");
}
}
foreach (Expression e in m.Decreases.Expressions) {
ResolveExpression(e, false, m);
// any type is fine
if (m.IsGhost && e is WildcardExpr) {
Error(e, "'decreases *' is not allowed on ghost methods");
}
}
// Add out-parameters to a new scope that will also include the outermost-level locals of the body
// Don't care about any duplication errors among the out-parameters, since they have already been reported
scope.PushMarker();
foreach (Formal p in m.Outs) {
scope.Push(p.Name, p);
}
// ... continue resolving specification
foreach (MaybeFreeExpression e in m.Ens) {
ResolveExpression(e.E, true, m);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E.Type, Type.Bool)) {
Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
}
}
// Resolve body
if (m.Body != null) {
var com = m as CoMethod;
if (com != null && com.PrefixMethod != null) {
// The body may mentioned the implicitly declared parameter _k. Throw it into the
// scope before resolving the body.
var k = com.PrefixMethod.Ins[0];
scope.Push(k.Name, k); // we expect no name conflict for _k
}
var codeContext = m;
ResolveBlockStatement(m.Body, m.IsGhost, codeContext);
}
// attributes are allowed to mention both in- and out-parameters (including the implicit _k, for comethods)
ResolveAttributes(m.Attributes, false, m);
scope.PopMarker(); // for the out-parameters and outermost-level locals
scope.PopMarker(); // for the in-parameters
}
void ResolveCtorSignature(DatatypeCtor ctor, List dtTypeArguments) {
Contract.Requires(ctor != null);
Contract.Requires(dtTypeArguments != null);
foreach (Formal p in ctor.Formals) {
ResolveType(p.tok, p.Type, ResolveTypeOption.AllowExact, dtTypeArguments);
}
}
///
/// Assumes type parameters have already been pushed
///
void ResolveIteratorSignature(IteratorDecl iter) {
Contract.Requires(iter != null);
scope.PushMarker();
if (iter.SignatureIsOmitted) {
Error(iter, "iterator signature can be omitted only in refining methods");
}
var option = iter.TypeArgs.Count == 0 ? ResolveTypeOption.AllowPrefixExtend : ResolveTypeOption.AllowPrefix;
// resolve the types of the parameters
foreach (var p in iter.Ins.Concat(iter.Outs)) {
ResolveType(p.tok, p.Type, option, iter.TypeArgs);
}
// resolve the types of the added fields (in case some of these types would cause the addition of default type arguments)
foreach (var p in iter.OutsHistoryFields) {
ResolveType(p.tok, p.Type, option, iter.TypeArgs);
}
scope.PopMarker();
}
///
/// Assumes type parameters have already been pushed
///
void ResolveIterator(IteratorDecl iter) {
Contract.Requires(iter != null);
Contract.Requires(currentClass == null);
Contract.Ensures(currentClass == null);
var initialErrorCount = ErrorCount;
// Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported
scope.PushMarker();
scope.AllowInstance = false; // disallow 'this' from use, which means that the special fields and methods added are not accessible in the syntactically given spec
iter.Ins.ForEach(p => scope.Push(p.Name, p));
// Start resolving specification...
// we start with the decreases clause, because the _decreases fields were only given type proxies before; we'll know
// the types only after resolving the decreases clause (and it may be that some of resolution has already seen uses of
// these fields; so, with no further ado, here we go
Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);
for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {
var e = iter.Decreases.Expressions[i];
ResolveExpression(e, false, iter);
// any type is fine, but associate this type with the corresponding _decreases field
var d = iter.DecreasesFields[i];
if (!UnifyTypes(d.Type, e.Type)) {
// bummer, there was a use--and a bad use--of the field before, so this won't be the best of error messages
Error(e, "type of field {0} is {1}, but has been constrained elsewhere to be of type {2}", d.Name, e.Type, d.Type);
}
}
foreach (FrameExpression fe in iter.Reads.Expressions) {
ResolveFrameExpression(fe, "reads");
}
foreach (FrameExpression fe in iter.Modifies.Expressions) {
ResolveFrameExpression(fe, "modifies");
}
foreach (MaybeFreeExpression e in iter.Requires) {
ResolveExpression(e.E, false, iter);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E.Type, Type.Bool)) {
Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);
}
}
scope.PopMarker(); // for the in-parameters
// We resolve the rest of the specification in an instance context. So mentions of the in- or yield-parameters
// get resolved as field dereferences (with an implicit "this")
scope.PushMarker();
currentClass = iter;
Contract.Assert(scope.AllowInstance);
foreach (MaybeFreeExpression e in iter.YieldRequires) {
ResolveExpression(e.E, false, iter);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E.Type, Type.Bool)) {
Error(e.E, "Yield precondition must be a boolean (got {0})", e.E.Type);
}
}
foreach (MaybeFreeExpression e in iter.YieldEnsures) {
ResolveExpression(e.E, true, iter);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E.Type, Type.Bool)) {
Error(e.E, "Yield postcondition must be a boolean (got {0})", e.E.Type);
}
}
foreach (MaybeFreeExpression e in iter.Ensures) {
ResolveExpression(e.E, true, iter);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E.Type, Type.Bool)) {
Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
}
}
ResolveAttributes(iter.Attributes, false, iter);
var postSpecErrorCount = ErrorCount;
// Resolve body
if (iter.Body != null) {
ResolveBlockStatement(iter.Body, false, iter);
}
currentClass = null;
scope.PopMarker(); // pop off the AllowInstance setting
if (postSpecErrorCount == initialErrorCount) {
CreateIteratorMethodSpecs(iter);
}
}
///
/// Assumes the specification of the iterator itself has been successfully resolved.
///
void CreateIteratorMethodSpecs(IteratorDecl iter) {
Contract.Requires(iter != null);
// ---------- here comes the constructor ----------
// same requires clause as the iterator itself
iter.Member_Init.Req.AddRange(iter.Requires);
// modifies this;
iter.Member_Init.Mod.Expressions.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null));
var ens = iter.Member_Init.Ens;
foreach (var p in iter.Ins) {
// ensures this.x == x;
ens.Add(new MaybeFreeExpression(new BinaryExpr(p.tok, BinaryExpr.Opcode.Eq,
new FieldSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new IdentifierExpr(p.tok, p.Name))));
}
foreach (var p in iter.OutsHistoryFields) {
// ensures this.ys == [];
ens.Add(new MaybeFreeExpression(new BinaryExpr(p.tok, BinaryExpr.Opcode.Eq,
new FieldSelectExpr(p.tok, new ThisExpr(p.tok), p.Name), new SeqDisplayExpr(p.tok, new List()))));
}
// ensures this.Valid();
ens.Add(new MaybeFreeExpression(new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List())));
// ensures this._reads == old(ReadsClause);
var modSetSingletons = new List();
Expression frameSet = new SetDisplayExpr(iter.tok, modSetSingletons);
foreach (var fr in iter.Reads.Expressions) {
if (fr.FieldName != null) {
Error(fr.tok, "sorry, a reads clause for an iterator is not allowed to designate specific fields");
} else if (fr.E.Type.IsRefType) {
modSetSingletons.Add(fr.E);
} else {
frameSet = new BinaryExpr(fr.tok, BinaryExpr.Opcode.Add, frameSet, fr.E);
}
}
ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_reads"),
new OldExpr(iter.tok, frameSet))));
// ensures this._modifies == old(ModifiesClause);
modSetSingletons = new List();
frameSet = new SetDisplayExpr(iter.tok, modSetSingletons);
foreach (var fr in iter.Modifies.Expressions) {
if (fr.FieldName != null) {
Error(fr.tok, "sorry, a modifies clause for an iterator is not allowed to designate specific fields");
} else if (fr.E.Type.IsRefType) {
modSetSingletons.Add(fr.E);
} else {
frameSet = new BinaryExpr(fr.tok, BinaryExpr.Opcode.Add, frameSet, fr.E);
}
}
ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"),
new OldExpr(iter.tok, frameSet))));
// ensures this._new == {};
ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),
new SetDisplayExpr(iter.tok, new List()))));
// ensures this._decreases0 == old(DecreasesClause[0]) && ...;
Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);
for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {
var p = iter.Decreases.Expressions[i];
ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), iter.DecreasesFields[i].Name),
new OldExpr(iter.tok, p))));
}
// ---------- here comes predicate Valid() ----------
var reads = iter.Member_Valid.Reads;
reads.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null)); // reads this;
reads.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_reads"), null)); // reads this._reads;
reads.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null)); // reads this._new;
// ---------- here comes method MoveNext() ----------
// requires this.Valid();
var req = iter.Member_MoveNext.Req;
req.Add(new MaybeFreeExpression(new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List())));
// requires YieldRequires;
req.AddRange(iter.YieldRequires);
// modifies this, this._modifies, this._new;
var mod = iter.Member_MoveNext.Mod.Expressions;
mod.Add(new FrameExpression(iter.tok, new ThisExpr(iter.tok), null));
mod.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"), null));
mod.Add(new FrameExpression(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"), null));
// ensures fresh(_new - old(_new));
ens = iter.Member_MoveNext.Ens;
ens.Add(new MaybeFreeExpression(new FreshExpr(iter.tok,
new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub,
new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),
new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"))))));
// ensures more ==> this.Valid();
ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp,
new IdentifierExpr(iter.tok, "more"),
new FunctionCallExpr(iter.tok, "Valid", new ThisExpr(iter.tok), iter.tok, new List()))));
// ensures this.ys == if more then old(this.ys) + [this.y] else old(this.ys);
Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count);
for (int i = 0; i < iter.OutsFields.Count; i++) {
var y = iter.OutsFields[i];
var ys = iter.OutsHistoryFields[i];
var ite = new ITEExpr(iter.tok, new IdentifierExpr(iter.tok, "more"),
new BinaryExpr(iter.tok, BinaryExpr.Opcode.Add,
new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)),
new SeqDisplayExpr(iter.tok, new List() { new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), y.Name) })),
new OldExpr(iter.tok, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)));
var eq = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new FieldSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name), ite);
ens.Add(new MaybeFreeExpression(eq));
}
// ensures more ==> YieldEnsures;
foreach (var ye in iter.YieldEnsures) {
ens.Add(new MaybeFreeExpression(
new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp, new IdentifierExpr(iter.tok, "more"), ye.E),
ye.IsFree));
}
// ensures !more ==> Ensures;
foreach (var e in iter.Ensures) {
ens.Add(new MaybeFreeExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Imp,
new UnaryExpr(iter.tok, UnaryExpr.Opcode.Not, new IdentifierExpr(iter.tok, "more")),
e.E),
e.IsFree));
}
// decreases this._decreases0, this._decreases1, ...;
Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count);
for (int i = 0; i < iter.Decreases.Expressions.Count; i++) {
var p = iter.Decreases.Expressions[i];
iter.Member_MoveNext.Decreases.Expressions.Add(new FieldSelectExpr(p.tok, new ThisExpr(p.tok), iter.DecreasesFields[i].Name));
}
iter.Member_MoveNext.Decreases.Attributes = iter.Decreases.Attributes;
}
///
/// If ResolveType/ResolveTypeLenient encounters a (datatype or class) type "C" with no supplied arguments, then
/// the ResolveTypeOption says what to do. The last three options take a List as a parameter, which (would have
/// been supplied as an argument if C# had datatypes instead of just enums, but since C# doesn't) is supplied
/// as another parameter (called 'defaultTypeArguments') to ResolveType/ResolveTypeLenient.
///
public enum ResolveTypeOption
{
///
/// never infer type arguments
///
DontInfer,
///
/// create a new InferredTypeProxy type for each needed argument
///
InferTypeProxies,
///
/// if exactly defaultTypeArguments.Count type arguments are needed, use defaultTypeArguments
///
AllowExact,
///
/// if at most defaultTypeArguments.Count type arguments are needed, use a prefix of defaultTypeArguments
///
AllowPrefix,
///
/// same as AllowPrefix, but if more than defaultTypeArguments.Count type arguments are needed, first
/// extend defaultTypeArguments to a sufficient length
///
AllowPrefixExtend,
}
///
/// See ResolveTypeOption for a description of the option/defaultTypeArguments parameters.
///
public void ResolveType(IToken tok, Type type, ResolveTypeOption option, List defaultTypeArguments) {
Contract.Requires((option == ResolveTypeOption.DontInfer || option == ResolveTypeOption.InferTypeProxies) == (defaultTypeArguments == null));
var r = ResolveTypeLenient(tok, type, option, defaultTypeArguments, false);
Contract.Assert(r == null);
}
public class ResolveTypeReturn
{
public readonly Type ReplacementType;
public readonly string LastName;
public readonly IToken LastToken;
public ResolveTypeReturn(Type replacementType, string lastName, IToken lastToken) {
Contract.Requires(replacementType != null);
Contract.Requires(lastName != null);
Contract.Requires(lastToken != null);
ReplacementType = replacementType;
LastName = lastName;
LastToken = lastToken;
}
}
///
/// See ResolveTypeOption for a description of the option/defaultTypeArguments parameters.
/// One more thing: if "allowShortenedPath" is true, then if the resolution would have produced
/// an error message that could have been avoided if "type" denoted an identifier sequence one
/// shorter, then return an unresolved replacement type where the identifier sequence is one
/// shorter. (In all other cases, the method returns null.)
///
public ResolveTypeReturn ResolveTypeLenient(IToken tok, Type type, ResolveTypeOption option, List defaultTypeArguments, bool allowShortenedPath) {
Contract.Requires(tok != null);
Contract.Requires(type != null);
Contract.Requires((option == ResolveTypeOption.DontInfer || option == ResolveTypeOption.InferTypeProxies) == (defaultTypeArguments == null));
if (type is BasicType) {
// nothing to resolve
} else if (type is MapType) {
MapType mt = (MapType)type;
ResolveType(tok, mt.Domain, option, defaultTypeArguments);
ResolveType(tok, mt.Range, option, defaultTypeArguments);
if (mt.Domain.IsSubrangeType || mt.Range.IsSubrangeType) {
Error(tok, "sorry, cannot instantiate collection type with a subrange type");
}
} else if (type is CollectionType) {
var t = (CollectionType)type;
var argType = t.Arg;
ResolveType(tok, argType, option, defaultTypeArguments);
if (argType.IsSubrangeType) {
Error(tok, "sorry, cannot instantiate collection type with a subrange type");
}
} else if (type is UserDefinedType) {
UserDefinedType t = (UserDefinedType)type;
foreach (Type tt in t.TypeArgs) {
ResolveType(t.tok, tt, option, defaultTypeArguments);
if (tt.IsSubrangeType) {
Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");
}
}
TypeParameter tp = t.Path.Count == 0 ? allTypeParameters.Find(t.Name) : null;
if (tp != null) {
if (t.TypeArgs.Count == 0) {
t.ResolvedParam = tp;
} else {
Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);
}
} else if (t.ResolvedClass == null) { // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')
TopLevelDecl d = null;
int j;
var sig = moduleInfo;
for (j = 0; j < t.Path.Count; j++) {
ModuleSignature submodule;
if (sig.FindSubmodule(t.Path[j].val, out submodule)) {
sig = GetSignature(submodule);
} else {
// maybe the last component of t.Path is actually the type name
if (allowShortenedPath && t.TypeArgs.Count == 0 && j == t.Path.Count - 1 && sig.TopLevels.TryGetValue(t.Path[j].val, out d)) {
// move the last component of t.Path to t.tok/t.name, tell the caller about this, and continue
var reducedPath = new List();
for (int i = 0; i < j; i++) {
reducedPath.Add(t.Path[i]);
}
return new ResolveTypeReturn(new UserDefinedType(t.Path[j], t.Path[j].val, t.TypeArgs, reducedPath), t.Name, t.tok);
} else {
Error(t.Path[j], ModuleNotFoundErrorMessage(j, t.Path));
}
break;
}
}
if (j == t.Path.Count) {
if (!sig.TopLevels.TryGetValue(t.Name, out d)) {
if (j == 0)
Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)", t.Name);
else
Error(t.tok, "Undeclared type {0} in module {1}", t.Name, t.Path[t.Path.Count - 1].val);
}
} else {
// error has already been reported
}
if (d == null) {
// error has been reported above
} else if (d is AmbiguousTopLevelDecl) {
Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());
} else if (d is ArbitraryTypeDecl) {
t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType; // resolve like a type parameter
} else {
// d is a class or datatype, and it may have type parameters
t.ResolvedClass = d;
if (option == ResolveTypeOption.DontInfer) {
// don't add anything
} else if (d.TypeArgs.Count != t.TypeArgs.Count && t.TypeArgs.Count == 0) {
if (option == ResolveTypeOption.InferTypeProxies) {
// add type arguments that will be inferred
for (int i = 0; i < d.TypeArgs.Count; i++) {
t.TypeArgs.Add(new InferredTypeProxy());
}
} else if (option == ResolveTypeOption.AllowExact && defaultTypeArguments.Count != d.TypeArgs.Count) {
// the number of default arguments is not exactly what we need, so don't add anything
} else if (option == ResolveTypeOption.AllowPrefix && defaultTypeArguments.Count < d.TypeArgs.Count) {
// there aren't enough default arguments, so don't do anything
} else {
// we'll add arguments
if (option == ResolveTypeOption.AllowPrefixExtend) {
// extend defaultTypeArguments, if needed
for (int i = defaultTypeArguments.Count; i < d.TypeArgs.Count; i++) {
defaultTypeArguments.Add(new TypeParameter(t.tok, "_T" + i));
}
}
Contract.Assert(d.TypeArgs.Count <= defaultTypeArguments.Count);
// automatically supply a prefix of the arguments from defaultTypeArguments
for (int i = 0; i < d.TypeArgs.Count; i++) {
var typeArg = new UserDefinedType(t.tok, defaultTypeArguments[i].Name, new List(), null);
typeArg.ResolvedParam = defaultTypeArguments[i]; // resolve "typeArg" here
t.TypeArgs.Add(typeArg);
}
}
}
// defaults and auto have been applied; check if we now have the right number of arguments
if (d.TypeArgs.Count != t.TypeArgs.Count) {
Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);
}
}
}
} else if (type is TypeProxy) {
TypeProxy t = (TypeProxy)type;
if (t.T != null) {
ResolveType(tok, t.T, option, defaultTypeArguments);
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
return null;
}
public bool UnifyTypes(Type a, Type b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
while (a is TypeProxy) {
TypeProxy proxy = (TypeProxy)a;
if (proxy.T == null) {
// merge a and b; to avoid cycles, first get to the bottom of b
while (b is TypeProxy && ((TypeProxy)b).T != null) {
b = ((TypeProxy)b).T;
}
return AssignProxy(proxy, b);
} else {
a = proxy.T;
}
}
while (b is TypeProxy) {
TypeProxy proxy = (TypeProxy)b;
if (proxy.T == null) {
// merge a and b (we have already got to the bottom of a)
return AssignProxy(proxy, a);
} else {
b = proxy.T;
}
}
#if !NO_CHEAP_OBJECT_WORKAROUND
if (a is ObjectType || b is ObjectType) { // TODO: remove this temporary hack
var other = a is ObjectType ? b : a;
if (other is BoolType || other is IntType || other is SetType || other is SeqType || other.IsDatatype) {
return false;
}
// allow anything else with object; this is BOGUS
return true;
}
#endif
// Now, a and b are non-proxies and stand for the same things as the original a and b, respectively.
if (a is BoolType) {
return b is BoolType;
} else if (a is IntType) {
return b is IntType;
} else if (a is ObjectType) {
return b is ObjectType;
} else if (a is SetType) {
return b is SetType && UnifyTypes(((SetType)a).Arg, ((SetType)b).Arg);
} else if (a is MultiSetType) {
return b is MultiSetType && UnifyTypes(((MultiSetType)a).Arg, ((MultiSetType)b).Arg);
} else if (a is MapType) {
return b is MapType && UnifyTypes(((MapType)a).Domain, ((MapType)b).Domain) && UnifyTypes(((MapType)a).Range, ((MapType)b).Range);
} else if (a is SeqType) {
return b is SeqType && UnifyTypes(((SeqType)a).Arg, ((SeqType)b).Arg);
} else if (a is UserDefinedType) {
if (!(b is UserDefinedType)) {
return false;
}
UserDefinedType aa = (UserDefinedType)a;
UserDefinedType bb = (UserDefinedType)b;
if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) {
// these are both resolved class/datatype types
Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count);
bool successSoFar = true;
for (int i = 0; i < aa.TypeArgs.Count; i++) {
if (!UnifyTypes(aa.TypeArgs[i], bb.TypeArgs[i])) {
successSoFar = false;
}
}
return successSoFar;
} else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {
// these are both resolved type parameters
Contract.Assert(aa.TypeArgs.Count == 0 && bb.TypeArgs.Count == 0);
return true;
} else {
// something is wrong; either aa or bb wasn't properly resolved, or they don't unify
return false;
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
bool AssignProxy(TypeProxy proxy, Type t) {
Contract.Requires(proxy != null);
Contract.Requires(t != null);
Contract.Requires(proxy.T == null);
Contract.Requires(!(t is TypeProxy) || ((TypeProxy)t).T == null);
//modifies proxy.T, ((TypeProxy)t).T; // might also change t.T if t is a proxy
Contract.Ensures(Contract.Result() == (proxy == t || proxy.T != null || (t is TypeProxy && ((TypeProxy)t).T != null)));
if (proxy == t) {
// they are already in the same equivalence class
return true;
} else if (proxy is UnrestrictedTypeProxy) {
// it's fine to redirect proxy to t (done below)
} else if (t is UnrestrictedTypeProxy) {
// merge proxy and t by redirecting t to proxy, rather than the other way around
((TypeProxy)t).T = proxy;
return true;
} else if (t is RestrictedTypeProxy) {
// Both proxy and t are restricted type proxies. To simplify unification, order proxy and t
// according to their types.
RestrictedTypeProxy r0 = (RestrictedTypeProxy)proxy;
RestrictedTypeProxy r1 = (RestrictedTypeProxy)t;
if (r0.OrderID <= r1.OrderID) {
return AssignRestrictedProxies(r0, r1);
} else {
return AssignRestrictedProxies(r1, r0);
}
// In the remaining cases, proxy is a restricted proxy and t is a non-proxy
} else if (proxy is DatatypeProxy) {
var dtp = (DatatypeProxy)proxy;
if (!dtp.Co && t.IsIndDatatype) {
// all is fine, proxy can be redirected to t
} else if (dtp.Co && t.IsCoDatatype) {
// all is fine, proxy can be redirected to t
} else {
return false;
}
} else if (proxy is ObjectTypeProxy) {
if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {
// all is fine, proxy can be redirected to t
} else {
return false;
}
} else if (proxy is CollectionTypeProxy) {
CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy;
if (t is CollectionType) {
if (!UnifyTypes(collProxy.Arg, ((CollectionType)t).Arg)) {
return false;
}
} else {
return false;
}
} else if (proxy is OperationTypeProxy) {
OperationTypeProxy opProxy = (OperationTypeProxy)proxy;
if (t is IntType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) {
// this is the expected case
} else {
return false;
}
} else if (proxy is IndexableTypeProxy) {
IndexableTypeProxy iProxy = (IndexableTypeProxy)proxy;
if (t is SeqType) {
if (!UnifyTypes(iProxy.Arg, ((SeqType)t).Arg)) {
return false;
}
if (!UnifyTypes(iProxy.Domain, Type.Int)) {
return false;
}
} else if (t.IsArrayType && (t.AsArrayType).Dims == 1) {
Type elType = UserDefinedType.ArrayElementType(t);
if (!UnifyTypes(iProxy.Arg, elType)) {
return false;
}
if (!UnifyTypes(iProxy.Domain, Type.Int)) {
return false;
}
} else if (t is MapType) {
if (!UnifyTypes(iProxy.Arg, ((MapType)t).Range)) {
return false;
}
if (!UnifyTypes(iProxy.Domain, ((MapType)t).Domain)) {
return false;
}
} else {
return false;
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected proxy type
}
// do the merge, but never infer a subrange type
if (t is NatType) {
proxy.T = Type.Int;
} else {
proxy.T = t;
}
return true;
}
bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
Contract.Requires(a != b);
Contract.Requires(a.T == null && b.T == null);
Contract.Requires(a.OrderID <= b.OrderID);
//modifies a.T, b.T;
Contract.Ensures(!Contract.Result() || a.T != null || b.T != null);
if (a is DatatypeProxy) {
if (b is DatatypeProxy && ((DatatypeProxy)a).Co == ((DatatypeProxy)b).Co) {
// all is fine
a.T = b;
return true;
} else {
return false;
}
} else if (a is ObjectTypeProxy) {
if (b is ObjectTypeProxy) {
// all is fine
a.T = b;
return true;
} else if (b is IndexableTypeProxy) {
// the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type
a.T = builtIns.ArrayType(1, ((IndexableTypeProxy)b).Arg);
b.T = a.T;
return true;
} else {
return false;
}
} else if (a is CollectionTypeProxy) {
if (b is CollectionTypeProxy) {
a.T = b;
return UnifyTypes(((CollectionTypeProxy)a).Arg, ((CollectionTypeProxy)b).Arg);
} else if (b is OperationTypeProxy) {
if (((OperationTypeProxy)b).AllowSeq) {
b.T = a; // a is a stronger constraint than b
} else {
// a says set,seq and b says int,set; the intersection is set
a.T = new SetType(((CollectionTypeProxy)a).Arg);
b.T = a.T;
}
return true;
} else if (b is IndexableTypeProxy) {
CollectionTypeProxy pa = (CollectionTypeProxy)a;
IndexableTypeProxy pb = (IndexableTypeProxy)b;
// a and b could be a map or a sequence
return true;
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
}
} else if (a is OperationTypeProxy) {
OperationTypeProxy pa = (OperationTypeProxy)a;
if (b is OperationTypeProxy) {
if (!pa.AllowSeq || ((OperationTypeProxy)b).AllowSeq) {
b.T = a;
} else {
a.T = b; // b has the stronger requirement
}
return true;
} else {
IndexableTypeProxy pb = (IndexableTypeProxy)b; // cast justification: lse we have unexpected restricted-proxy type
if (pa.AllowSeq) {
// strengthen a and b to a sequence type
b.T = new SeqType(pb.Arg);
a.T = b.T;
return true;
} else {
return false;
}
}
} else if (a is IndexableTypeProxy) {
Contract.Assert(b is IndexableTypeProxy); // else we have unexpected restricted-proxy type
a.T = b;
return UnifyTypes(((IndexableTypeProxy)a).Arg, ((IndexableTypeProxy)b).Arg);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
}
}
///
/// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it
/// at run time. That means it must not have any side effects on non-ghost variables, for example.
///
public void ResolveStatement(Statement stmt, bool specContextOnly, ICodeContext codeContext) {
Contract.Requires(stmt != null);
Contract.Requires(codeContext != null);
if (stmt is PredicateStmt) {
PredicateStmt s = (PredicateStmt)stmt;
ResolveAttributes(s.Attributes, false, codeContext);
s.IsGhost = true;
ResolveExpression(s.Expr, true, codeContext);
Contract.Assert(s.Expr.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);
}
} else if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
ResolveAttributeArgs(s.Args, false, codeContext, false);
if (specContextOnly) {
Error(stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
} else if (stmt is BreakStmt) {
var s = (BreakStmt)stmt;
if (s.TargetLabel != null) {
Statement target = labeledStatements.Find(s.TargetLabel);
if (target == null) {
Error(s, "break label is undefined or not in scope: {0}", s.TargetLabel);
} else {
s.TargetStmt = target;
bool targetIsLoop = target is WhileStmt || target is AlternativeLoopStmt;
if (specContextOnly && !s.TargetStmt.IsGhost && !inSpecOnlyContext[s.TargetStmt]) {
Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure"));
}
}
} else {
if (loopStack.Count < s.BreakCount) {
Error(s, "trying to break out of more loop levels than there are enclosing loops");
} else {
Statement target = loopStack[loopStack.Count - s.BreakCount];
if (target.Labels == null) {
// make sure there is a label, because the compiler and translator will want to see a unique ID
target.Labels = new LList