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