//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Numerics;
using System.Diagnostics.Contracts;
using Microsoft.Boogie;
namespace Microsoft.Dafny {
public class ResolutionErrorReporter
{
public int ErrorCount = 0;
///
/// This method is virtual, because it is overridden in the VSX plug-in for Dafny.
///
public virtual void Error(IToken tok, string msg, params object[] args) {
Contract.Requires(tok != null);
Contract.Requires(msg != null);
ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Red;
Console.WriteLine("{0}({1},{2}): Error: {3}",
tok.filename, tok.line, tok.col - 1,
string.Format(msg, args));
Console.ForegroundColor = col;
ErrorCount++;
}
public void Error(Declaration d, string msg, params object[] args) {
Contract.Requires(d != null);
Contract.Requires(msg != null);
Error(d.tok, msg, args);
}
public void Error(Statement s, string msg, params object[] args) {
Contract.Requires(s != null);
Contract.Requires(msg != null);
Error(s.Tok, msg, args);
}
public void Error(NonglobalVariable v, string msg, params object[] args) {
Contract.Requires(v != null);
Contract.Requires(msg != null);
Error(v.tok, msg, args);
}
public void Error(Expression e, string msg, params object[] args) {
Contract.Requires(e != null);
Contract.Requires(msg != null);
Error(e.tok, msg, args);
}
public void Warning(IToken tok, string msg, params object[] args) {
Contract.Requires(tok != null);
Contract.Requires(msg != null);
ConsoleColor col = Console.ForegroundColor;
Console.ForegroundColor = ConsoleColor.Yellow;
Console.WriteLine("{0}({1},{2}): Warning: {3}",
tok.filename, tok.line, tok.col - 1,
string.Format(msg, args));
Console.ForegroundColor = col;
}
}
public class Resolver : ResolutionErrorReporter {
readonly BuiltIns builtIns;
Dictionary/*!*/ classes; // can map to AmbiguousTopLevelDecl
class AmbiguousTopLevelDecl : TopLevelDecl // only used with "classes"
{
readonly TopLevelDecl A;
readonly TopLevelDecl B;
public AmbiguousTopLevelDecl(ModuleDecl m, TopLevelDecl a, TopLevelDecl b)
: base(a.tok, a.Name + "/" + b.Name, m, new List(), null) {
A = a;
B = b;
}
public string ModuleNames() {
string nm;
if (A is AmbiguousTopLevelDecl) {
nm = ((AmbiguousTopLevelDecl)A).ModuleNames();
} else {
nm = A.Module.Name;
}
if (B is AmbiguousTopLevelDecl) {
nm += ", " + ((AmbiguousTopLevelDecl)B).ModuleNames();
} else {
nm += ", " + B.Module.Name;
}
return nm;
}
}
Dictionary> allDatatypeCtors;
readonly Dictionary/*!*/>/*!*/ classMembers = new Dictionary/*!*/>();
readonly Dictionary/*!*/>/*!*/ datatypeMembers = new Dictionary/*!*/>();
readonly Dictionary/*!*/>/*!*/ datatypeCtors = new Dictionary/*!*/>();
readonly Graph/*!*/ importGraph = new Graph();
public Resolver(Program prog) {
Contract.Requires(prog != null);
builtIns = prog.BuiltIns;
}
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(builtIns != null);
Contract.Invariant(cce.NonNullElements(importGraph));
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);
// register modules
var modules = new Dictionary();
foreach (var m in prog.Modules) {
if (modules.ContainsKey(m.Name)) {
Error(m, "Duplicate module name: {0}", m.Name);
} else {
modules.Add(m.Name, m);
}
}
// resolve refines and imports
foreach (var m in prog.Modules) {
importGraph.AddVertex(m);
if (m.RefinementBaseName != null) {
ModuleDecl other;
if (!modules.TryGetValue(m.RefinementBaseName, out other)) {
Error(m, "module {0} named as refinement base does not exist", m.RefinementBaseName);
} else if (other == m) {
Error(m, "module cannot refine itself: {0}", m.RefinementBaseName);
} else {
Contract.Assert(other != null); // follows from postcondition of TryGetValue
importGraph.AddEdge(m, other);
m.RefinementBase = other;
}
}
foreach (string imp in m.ImportNames) {
ModuleDecl other;
if (!modules.TryGetValue(imp, out other)) {
Error(m, "module {0} named among imports does not exist", imp);
} else if (other == m) {
Error(m, "module must not import itself: {0}", imp);
} else {
Contract.Assert(other != null); // follows from postcondition of TryGetValue
importGraph.AddEdge(m, other);
m.Imports.Add(other);
}
}
}
// check for cycles in the import graph
List cycle = importGraph.TryFindCycle();
if (cycle != null) {
string cy = "";
string sep = "";
foreach (ModuleDecl m in cycle) {
cy = m.Name + sep + cy;
sep = " -> ";
}
Error(cycle[0], "import graph contains a cycle: {0}", cy);
return; // give up on trying to resolve anything else
}
// fill in module heights
List mm = importGraph.TopologicallySortedComponents();
Contract.Assert(mm.Count == prog.Modules.Count); // follows from the fact that there are no cycles
int h = 0;
foreach (ModuleDecl m in mm) {
m.Height = h;
h++;
}
// register top-level declarations
var rewriters = new List();
// The following line could be generalized to allow rewriter plug-ins; to support such, just add command-line
// switches and .Add to "rewriters" here.
rewriters.Add(new AutoContractsRewriter());
rewriters.Add(new RefinementTransformer(this));
var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls);
var moduleNameInfo = new ModuleNameInformation[h];
foreach (var m in mm) {
rewriters.Iter(r => r.PreResolve(m));
moduleNameInfo[m.Height] = RegisterTopLevelDecls(m.TopLevelDecls);
// set up environment
ModuleNameInformation info = ModuleNameInformation.Merge(m, systemNameInfo, moduleNameInfo);
classes = info.Classes;
allDatatypeCtors = info.Ctors;
// resolve
var datatypeDependencies = new Graph();
int prevErrorCount = ErrorCount;
ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);
if (prevErrorCount == ErrorCount) {
ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
}
// tear down
classes = null;
allDatatypeCtors = null;
// give rewriters a chance to do processing
rewriters.Iter(r => r.PostResolve(m));
}
// compute IsRecursive bit for mutually recursive functions
foreach (ModuleDecl m in mm) {
foreach (TopLevelDecl decl in m.TopLevelDecls) {
ClassDecl cl = decl as ClassDecl;
if (cl != null) {
foreach (MemberDecl member in cl.Members) {
Function fn = member as Function;
if (fn != null && !fn.IsRecursive) { // note, self-recursion has already been determined
int n = m.CallGraph.GetSCCSize(fn);
if (2 <= n) {
// the function is mutually recursive (note, the SCC does not determine self recursion)
fn.IsRecursive = true;
}
}
}
}
}
}
}
class ModuleNameInformation
{
public readonly Dictionary Classes = new Dictionary();
public readonly Dictionary> Ctors = new Dictionary>();
public static ModuleNameInformation Merge(ModuleDecl m, ModuleNameInformation system, ModuleNameInformation[] modules) {
var info = new ModuleNameInformation();
// add the system-declared information, among which we know there are no duplicates
foreach (var kv in system.Classes) {
info.Classes.Add(kv.Key, kv.Value);
}
foreach (var kv in system.Ctors) {
info.Ctors.Add(kv.Key, kv.Value);
}
// for each imported module, add its information, noting any duplicates
foreach (var im in m.Imports) {
Contract.Assume(0 <= im.Height && im.Height < m.Height);
var import = modules[im.Height];
// classes:
foreach (var kv in import.Classes) {
TopLevelDecl d;
if (info.Classes.TryGetValue(kv.Key, out d)) {
info.Classes[kv.Key] = new AmbiguousTopLevelDecl(m, d, kv.Value);
} else {
info.Classes.Add(kv.Key, kv.Value);
}
}
// constructors:
foreach (var kv in import.Ctors) {
Tuple pair;
if (info.Ctors.TryGetValue(kv.Key, out pair)) {
// mark it as a duplicate
info.Ctors[kv.Key] = new Tuple(pair.Item1, true);
} else {
// add new
info.Ctors.Add(kv.Key, kv.Value);
}
}
}
// finally, for the module itself, let its information override whatever is imported
foreach (var kv in modules[m.Height].Classes) {
info.Classes[kv.Key] = kv.Value;
}
foreach (var kv in modules[m.Height].Ctors) {
info.Ctors[kv.Key] = kv.Value;
}
return info;
}
}
ModuleNameInformation RegisterTopLevelDecls(List declarations) {
Contract.Requires(declarations != null);
var info = new ModuleNameInformation();
foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
// register the class/datatype name
if (info.Classes.ContainsKey(d.Name)) {
Error(d, "Duplicate name of top-level declaration: {0}", d.Name);
} else {
info.Classes.Add(d.Name, d);
}
if (d is ArbitraryTypeDecl) {
// nothing more to register
} else if (d is ClassDecl) {
ClassDecl cl = (ClassDecl)d;
// register the names of the class members
Dictionary members = new Dictionary();
classMembers.Add(cl, members);
bool hasConstructor = false;
foreach (MemberDecl m in cl.Members) {
if (members.ContainsKey(m.Name)) {
Error(m, "Duplicate member name: {0}", m.Name);
} else {
members.Add(m.Name, m);
}
if (m is Constructor) {
hasConstructor = true;
}
}
cl.HasConstructor = hasConstructor;
} else {
DatatypeDecl dt = (DatatypeDecl)d;
// register the names of the constructors
Dictionary ctors = new Dictionary();
datatypeCtors.Add(dt, ctors);
// ... and of the other members
Dictionary 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, Type.Bool, null);
query.EnclosingClass = dt; // resolve here
members.Add(queryName, query);
ctor.QueryField = query;
// also register the constructor name globally
Tuple pair;
if (info.Ctors.TryGetValue(ctor.Name, out pair)) {
// mark it as a duplicate
info.Ctors[ctor.Name] = new Tuple(pair.Item1, true);
} else {
// add new
info.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) {
SpecialField dtor = null;
if (formal.HasName) {
if (members.ContainsKey(formal.Name)) {
Error(ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);
} else {
dtor = new DatatypeDestructor(formal.tok, ctor, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);
dtor.EnclosingClass = dt; // resolve here
members.Add(formal.Name, dtor);
}
}
ctor.Destructors.Add(dtor);
}
}
}
}
return info;
}
public void ResolveTopLevelDecls_Signatures(List/*!*/ declarations, Graph/*!*/ datatypeDependencies) {
Contract.Requires(declarations != null);
Contract.Requires(datatypeDependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(datatypeDependencies));
foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
allTypeParameters.PushMarker();
ResolveTypeParameters(d.TypeArgs, true, d);
if (d is ArbitraryTypeDecl) {
// nothing to do
} else if (d is ClassDecl) {
ResolveClassMemberTypes((ClassDecl)d);
} else {
ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies);
}
allTypeParameters.PopMarker();
}
}
public void ResolveTopLevelDecls_Meat(List/*!*/ declarations, Graph/*!*/ datatypeDependencies) {
Contract.Requires(declarations != null);
Contract.Requires(cce.NonNullElements(datatypeDependencies));
int prevErrorCount = ErrorCount;
// Resolve the meat of classes, and the type parameters of all top-level type declarations
foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
allTypeParameters.PushMarker();
ResolveTypeParameters(d.TypeArgs, false, d);
if (d is ClassDecl) {
ResolveClassMemberBodies((ClassDecl)d);
}
allTypeParameters.PopMarker();
}
// Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support
foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {
if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {
// do the following check once per SCC, so call it on each SCC representative
SccStratosphereCheck(dtd, datatypeDependencies);
DetermineEqualitySupport(dtd, datatypeDependencies);
}
}
if (ErrorCount == prevErrorCount) { // because CheckCoCalls requires the given expression to have been successfully resolved
// Perform the guardedness check on co-datatypes
foreach (var decl in declarations) {
var cl = decl as ClassDecl;
if (cl != null) {
foreach (var member in cl.Members) {
var fn = member as Function;
if (fn != null && fn.Body != null && cl.Module.CallGraph.GetSCCRepresentative(fn) == fn) {
bool dealsWithCodatatypes = false;
foreach (var m in cl.Module.CallGraph.GetSCC(fn)) {
var f = (Function)m;
if (f.ResultType.InvolvesCoDatatype) {
dealsWithCodatatypes = true;
break;
}
}
foreach (var m in cl.Module.CallGraph.GetSCC(fn)) {
var f = (Function)m;
var checker = new CoCallResolution(f, dealsWithCodatatypes);
checker.CheckCoCalls(f.Body);
}
}
}
}
}
// Inferred required equality support for datatypes and for Function and Method signatures
// First, do datatypes until a fixpoint is reached
bool inferredSomething;
do {
inferredSomething = false;
foreach (var d in declarations) {
if (d is DatatypeDecl) {
var dt = (DatatypeDecl)d;
foreach (var tp in dt.TypeArgs) {
if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
// here's our chance to infer the need for equality support
foreach (var ctor in dt.Ctors) {
foreach (var arg in ctor.Formals) {
if (InferRequiredEqualitySupport(tp, arg.Type)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
inferredSomething = true;
goto DONE_DT; // break out of the doubly-nested loop
}
}
}
DONE_DT: ;
}
}
}
}
} while (inferredSomething);
// Now do it for Function and Method signatures
foreach (var d in declarations) {
if (d is ClassDecl) {
var cl = (ClassDecl)d;
foreach (var member in cl.Members) {
if (!member.IsGhost) {
if (member is Function) {
var f = (Function)member;
foreach (var tp in f.TypeArgs) {
if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
// here's our chance to infer the need for equality support
if (InferRequiredEqualitySupport(tp, f.ResultType)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
} else {
foreach (var p in f.Formals) {
if (InferRequiredEqualitySupport(tp, p.Type)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
break;
}
}
}
}
}
} else if (member is Method) {
var m = (Method)member;
foreach (var tp in m.TypeArgs) {
if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
// here's our chance to infer the need for equality support
foreach (var p in m.Ins) {
if (InferRequiredEqualitySupport(tp, p.Type)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
goto DONE;
}
}
foreach (var p in m.Outs) {
if (InferRequiredEqualitySupport(tp, p.Type)) {
tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
goto DONE;
}
}
DONE: ;
}
}
}
}
}
}
}
// Check that all == and != operators in non-ghost contexts are applied to equality-supporting types.
// Note that this check can only be done after determining which expressions are ghosts.
foreach (var d in declarations) {
if (d is 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);
}
}
}
}
}
}
}
void CheckEqualityTypes_Stmt(Statement stmt) {
Contract.Requires(stmt != null);
if (stmt.IsGhost) {
return;
} else if (stmt is PrintStmt) {
var s = (PrintStmt)stmt;
foreach (var arg in s.Args) {
if (arg.E != null) {
CheckEqualityTypes(arg.E);
}
}
} else if (stmt is BreakStmt) {
} else if (stmt is ReturnStmt) {
var s = (ReturnStmt)stmt;
if (s.rhss != null) {
s.rhss.Iter(CheckEqualityTypes_Rhs);
}
} else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
CheckEqualityTypes(s.Lhs);
CheckEqualityTypes_Rhs(s.Rhs);
} else if (stmt is VarDecl) {
var s = (VarDecl)stmt;
s.SubStatements.Iter(CheckEqualityTypes_Stmt);
} else if (stmt is CallStmt) {
var s = (CallStmt)stmt;
CheckEqualityTypes(s.Receiver);
s.Args.Iter(CheckEqualityTypes);
s.Lhs.Iter(CheckEqualityTypes);
Contract.Assert(s.Method.TypeArgs.Count <= s.TypeArgumentSubstitutions.Count);
var i = 0;
foreach (var formalTypeArg in s.Method.TypeArgs) {
var actualTypeArg = s.TypeArgumentSubstitutions[formalTypeArg];
if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {
Error(s.Tok, "type parameter {0} ({1}) passed to method {2} must support equality (got {3}){4}", i, formalTypeArg.Name, s.Method.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));
}
i++;
}
} else if (stmt is BlockStmt) {
var s = (BlockStmt)stmt;
s.Body.Iter(CheckEqualityTypes_Stmt);
} else if (stmt is IfStmt) {
var s = (IfStmt)stmt;
if (s.Guard != null) {
CheckEqualityTypes(s.Guard);
}
s.SubStatements.Iter(CheckEqualityTypes_Stmt);
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
foreach (var alt in s.Alternatives) {
CheckEqualityTypes(alt.Guard);
alt.Body.Iter(CheckEqualityTypes_Stmt);
}
} else if (stmt is WhileStmt) {
var s = (WhileStmt)stmt;
if (s.Guard != null) {
CheckEqualityTypes(s.Guard);
}
CheckEqualityTypes_Stmt(s.Body);
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
foreach (var alt in s.Alternatives) {
CheckEqualityTypes(alt.Guard);
alt.Body.Iter(CheckEqualityTypes_Stmt);
}
} else if (stmt is ParallelStmt) {
var s = (ParallelStmt)stmt;
CheckEqualityTypes(s.Range);
CheckEqualityTypes_Stmt(s.Body);
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
CheckEqualityTypes(s.Source);
foreach (MatchCaseStmt mc in s.Cases) {
mc.Body.Iter(CheckEqualityTypes_Stmt);
}
} else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
s.ResolvedStatements.Iter(CheckEqualityTypes_Stmt);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
}
void CheckEqualityTypes_Rhs(AssignmentRhs rhs) {
Contract.Requires(rhs != null);
rhs.SubExpressions.Iter(CheckEqualityTypes);
rhs.SubStatements.Iter(CheckEqualityTypes_Stmt);
}
void CheckEqualityTypes(Expression expr) {
Contract.Requires(expr != null);
if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
var t0 = e.E0.Type.Normalize();
var t1 = e.E1.Type.Normalize();
switch (e.Op) {
case BinaryExpr.Opcode.Eq:
case BinaryExpr.Opcode.Neq:
if (!t0.SupportsEquality) {
Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
} else if (!t1.SupportsEquality) {
Error(e.E1, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));
}
break;
default:
switch (e.ResolvedOp) {
// Note, all operations on sets, multisets, and maps are guaranteed to work because of restrictions placed on how
// these types are instantiated. (Except: This guarantee does not apply to equality on maps, because the Range type
// of maps is not restricted, only the Domain type. However, the equality operator is checked above.)
case BinaryExpr.ResolvedOpcode.InSeq:
case BinaryExpr.ResolvedOpcode.NotInSeq:
case BinaryExpr.ResolvedOpcode.Prefix:
case BinaryExpr.ResolvedOpcode.ProperPrefix:
if (!t1.SupportsEquality) {
Error(e.E1, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));
} else if (!t0.SupportsEquality) {
if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet || e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSeq) {
Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
} else {
Error(e.E0, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
}
}
break;
default:
break;
}
break;
}
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
foreach (var bv in e.BoundVars) {
CheckEqualityTypes_Type(bv.tok, bv.Type);
}
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
foreach (var bv in e.Vars) {
CheckEqualityTypes_Type(bv.tok, bv.Type);
}
} else if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
Contract.Assert(e.Function.TypeArgs.Count <= e.TypeArgumentSubstitutions.Count);
var i = 0;
foreach (var formalTypeArg in e.Function.TypeArgs) {
var actualTypeArg = e.TypeArgumentSubstitutions[formalTypeArg];
if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {
Error(e.tok, "type parameter {0} ({1}) passed to function {2} must support equality (got {3}){4}", i, formalTypeArg.Name, e.Function.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));
}
i++;
}
}
foreach (var ee in expr.SubExpressions) {
CheckEqualityTypes(ee);
}
}
void CheckEqualityTypes_Type(IToken tok, Type type) {
Contract.Requires(tok != null);
Contract.Requires(type != null);
type = type.Normalize();
if (type is BasicType) {
// fine
} else if (type is SetType) {
var argType = ((SetType)type).Arg;
if (!argType.SupportsEquality) {
Error(tok, "set argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));
}
CheckEqualityTypes_Type(tok, argType);
} else if (type is MultiSetType) {
var argType = ((MultiSetType)type).Arg;
if (!argType.SupportsEquality) {
Error(tok, "multiset argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));
}
CheckEqualityTypes_Type(tok, argType);
} else if (type is MapType) {
var mt = (MapType)type;
if (!mt.Domain.SupportsEquality) {
Error(tok, "map domain type must support equality (got {0}){1}", mt.Domain, TypeEqualityErrorMessageHint(mt.Domain));
}
CheckEqualityTypes_Type(tok, mt.Domain);
CheckEqualityTypes_Type(tok, mt.Range);
} else if (type is SeqType) {
Type argType = ((SeqType)type).Arg;
CheckEqualityTypes_Type(tok, argType);
} else if (type is UserDefinedType) {
var udt = (UserDefinedType)type;
if (udt.ResolvedClass != null) {
Contract.Assert(udt.ResolvedClass.TypeArgs.Count == udt.TypeArgs.Count);
var i = 0;
foreach (var argType in udt.TypeArgs) {
var formalTypeArg = udt.ResolvedClass.TypeArgs[i];
if (formalTypeArg.MustSupportEquality && !argType.SupportsEquality) {
Error(tok, "type parameter {0} ({1}) passed to type {2} must support equality (got {3}){4}", i, formalTypeArg.Name, udt.ResolvedClass.Name, argType, TypeEqualityErrorMessageHint(argType));
}
CheckEqualityTypes_Type(tok, argType);
i++;
}
} else {
Contract.Assert(udt.TypeArgs.Count == 0); // TypeParameters have no type arguments
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
string TypeEqualityErrorMessageHint(Type argType) {
Contract.Requires(argType != null);
var tp = argType.AsTypeParameter;
if (tp != null) {
return string.Format(" (perhaps try declaring type parameter '{0}' on line {1} as '{0}(==)', which says it can only be instantiated with a type that supports equality)", tp.Name, tp.tok.line);
}
return "";
}
bool InferRequiredEqualitySupport(TypeParameter tp, Type type) {
Contract.Requires(tp != null);
Contract.Requires(type != null);
type = type.Normalize();
if (type is BasicType) {
} else if (type is SetType) {
var st = (SetType)type;
return st.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, st.Arg);
} else if (type is MultiSetType) {
var ms = (MultiSetType)type;
return ms.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, ms.Arg);
} else if (type is MapType) {
var mt = (MapType)type;
return mt.Domain.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, mt.Domain) || InferRequiredEqualitySupport(tp, mt.Range);
} else if (type is SeqType) {
var sq = (SeqType)type;
return InferRequiredEqualitySupport(tp, sq.Arg);
} else if (type is UserDefinedType) {
var udt = (UserDefinedType)type;
if (udt.ResolvedClass != null) {
var i = 0;
foreach (var argType in udt.TypeArgs) {
var formalTypeArg = udt.ResolvedClass.TypeArgs[i];
if ((formalTypeArg.MustSupportEquality && argType.AsTypeParameter == tp) || InferRequiredEqualitySupport(tp, argType)) {
return true;
}
i++;
}
} else {
Contract.Assert(udt.TypeArgs.Count == 0); // TypeParameters have no type arguments
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
return false;
}
ClassDecl currentClass;
Function currentFunction;
readonly Scope/*!*/ allTypeParameters = new Scope();
readonly Scope/*!*/ scope = new Scope();
Scope/*!*/ labeledStatements = new Scope();
List loopStack = new List(); // the enclosing loops (from which it is possible to break out)
readonly Dictionary inSpecOnlyContext = new Dictionary(); // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
///
/// Assumes type parameters have already been pushed
///
void ResolveClassMemberTypes(ClassDecl/*!*/ cl)
{
Contract.Requires(cl != null);
Contract.Requires(currentClass == null);
Contract.Ensures(currentClass == null);
currentClass = cl;
foreach (MemberDecl member in cl.Members) {
member.EnclosingClass = cl;
if (member is Field) {
ResolveType(member.tok, ((Field)member).Type, null, false);
} else if (member is Function) {
Function f = (Function)member;
allTypeParameters.PushMarker();
ResolveTypeParameters(f.TypeArgs, true, f);
ResolveFunctionSignature(f);
allTypeParameters.PopMarker();
} else if (member is Method) {
Method m = (Method)member;
allTypeParameters.PushMarker();
ResolveTypeParameters(m.TypeArgs, true, m);
ResolveMethodSignature(m);
allTypeParameters.PopMarker();
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type
}
}
currentClass = null;
}
///
/// 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);
ResolveAttributes(cl.Attributes, false);
currentClass = cl;
foreach (MemberDecl member in cl.Members) {
if (member is Field) {
ResolveAttributes(member.Attributes, false);
// nothing more to do
} else if (member is Function) {
Function f = (Function)member;
allTypeParameters.PushMarker();
ResolveTypeParameters(f.TypeArgs, false, f);
ResolveFunction(f);
allTypeParameters.PopMarker();
} else if (member is Method) {
Method m = (Method)member;
allTypeParameters.PushMarker();
ResolveTypeParameters(m.TypeArgs, false, m);
ResolveMethod(m);
allTypeParameters.PopMarker();
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type
}
}
currentClass = null;
}
///
/// Assumes type parameters have already been pushed
///
void ResolveCtorTypes(DatatypeDecl/*!*/ dt, Graph/*!*/ dependencies)
{
Contract.Requires(dt != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
foreach (DatatypeCtor ctor in dt.Ctors) {
ctor.EnclosingDatatype = dt;
allTypeParameters.PushMarker();
ResolveCtorSignature(ctor, dt.TypeArgs);
allTypeParameters.PopMarker();
if (dt is IndDatatypeDecl) {
var idt = (IndDatatypeDecl)dt;
dependencies.AddVertex(idt);
foreach (Formal p in ctor.Formals) {
AddDatatypeDependencyEdge(idt, p.Type, dependencies);
}
}
}
}
void AddDatatypeDependencyEdge(IndDatatypeDecl/*!*/ dt, Type/*!*/ tp, Graph/*!*/ dependencies) {
Contract.Requires(dt != null);
Contract.Requires(tp != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
var dependee = tp.AsIndDatatype;
if (dependee != null && dt.Module == dependee.Module) {
dependencies.AddEdge((IndDatatypeDecl)dt, dependee);
foreach (var ta in ((UserDefinedType)tp).TypeArgs) {
AddDatatypeDependencyEdge(dt, ta, dependencies);
}
}
}
///
/// Check that the SCC of 'startingPoint' can be carved up into stratospheres in such a way that each
/// datatype has some value that can be constructed from datatypes in lower stratospheres only.
/// The algorithm used here is quadratic in the number of datatypes in the SCC. Since that number is
/// deemed to be rather small, this seems okay.
///
/// As a side effect of this checking, the DefaultCtor field is filled in (for every inductive datatype
/// that passes the check). It may be that several constructors could be used as the default, but
/// only the first one encountered as recorded. This particular choice is slightly more than an
/// implementation detail, because it affects how certain cycles among inductive datatypes (having
/// to do with the types used to instantiate type parameters of datatypes) are used.
///
/// The role of the SCC here is simply to speed up this method. It would still be correct if the
/// equivalence classes in the given SCC were unions of actual SCC's. In particular, this method
/// would still work if "dependencies" consisted of one large SCC containing all the inductive
/// datatypes in the module.
///
void SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph/*!*/ dependencies)
{
Contract.Requires(startingPoint != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
var scc = dependencies.GetSCC(startingPoint);
int totalCleared = 0;
while (true) {
int clearedThisRound = 0;
foreach (var dt in scc) {
if (dt.DefaultCtor != null) {
// previously cleared
} else if (ComputeDefaultCtor(dt)) {
Contract.Assert(dt.DefaultCtor != null); // should have been set by the successful call to StratosphereCheck)
clearedThisRound++;
totalCleared++;
}
}
if (totalCleared == scc.Count) {
// all is good
return;
} else if (clearedThisRound != 0) {
// some progress was made, so let's keep going
} else {
// whatever is in scc-cleared now failed to pass the test
foreach (var dt in scc) {
if (dt.DefaultCtor == null) {
Error(dt, "because of cyclic dependencies among constructor argument types, no instances of datatype '{0}' can be constructed", dt.Name);
}
}
return;
}
}
}
///
/// Check that the datatype has some constructor all whose argument types can be constructed.
/// Returns 'true' and sets dt.DefaultCtor if that is the case.
///
bool ComputeDefaultCtor(IndDatatypeDecl dt) {
Contract.Requires(dt != null);
Contract.Requires(dt.DefaultCtor == null); // the intention is that this method be called only when DefaultCtor hasn't already been set
Contract.Ensures(!Contract.Result() || dt.DefaultCtor != null);
// Stated differently, check that there is some constuctor where no argument type goes to the same stratum.
foreach (DatatypeCtor ctor in dt.Ctors) {
var typeParametersUsed = new List();
foreach (Formal p in ctor.Formals) {
if (!CheckCanBeConstructed(p.Type, typeParametersUsed)) {
// the argument type (has a component which) is not yet known to be constructable
goto NEXT_OUTER_ITERATION;
}
}
// this constructor satisfies the requirements, so the datatype is allowed
dt.DefaultCtor = ctor;
dt.TypeParametersUsedInConstructionByDefaultCtor = new bool[dt.TypeArgs.Count];
for (int i = 0; i < dt.TypeArgs.Count; i++) {
dt.TypeParametersUsedInConstructionByDefaultCtor[i] = typeParametersUsed.Contains(dt.TypeArgs[i]);
}
return true;
NEXT_OUTER_ITERATION: {}
}
// no constructor satisfied the requirements, so this is an illegal datatype declaration
return false;
}
bool CheckCanBeConstructed(Type tp, List typeParametersUsed) {
var dependee = tp.AsIndDatatype;
if (dependee == null) {
// the type is not an inductive datatype, which means it is always possible to construct it
if (tp.IsTypeParameter) {
typeParametersUsed.Add(((UserDefinedType)tp).ResolvedParam);
}
return true;
} else if (dependee.DefaultCtor == null) {
// the type is an inductive datatype that we don't yet know how to construct
return false;
}
// also check the type arguments of the inductive datatype
Contract.Assert(((UserDefinedType)tp).TypeArgs.Count == dependee.TypeParametersUsedInConstructionByDefaultCtor.Length);
var i = 0;
foreach (var ta in ((UserDefinedType)tp).TypeArgs) { // note, "tp" is known to be a UserDefinedType, because that follows from tp being an inductive datatype
if (dependee.TypeParametersUsedInConstructionByDefaultCtor[i] && !CheckCanBeConstructed(ta, typeParametersUsed)) {
return false;
}
i++;
}
return true;
}
void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph/*!*/ dependencies) {
Contract.Requires(startingPoint != null);
Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
#if SOON
var scc = dependencies.GetSCC(startingPoint);
// First, the simple case: If any parameter of any inductive datatype in the SCC is of a codatatype type, then
// the whole SCC is incapable of providing the equality operation.
foreach (var dt in scc) {
Contract.Assume(dt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed);
foreach (var ctor in dt.Ctors) {
foreach (var arg in ctor.Formals) {
var anotherIndDt = arg.Type.AsIndDatatype;
if ((anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || arg.Type.IsCoDatatype) {
// arg.Type is known never to support equality
// So, go around the entire SCC and record what we learnt
foreach (var ddtt in scc) {
ddtt.EqualitySupport = IndDatatypeDecl.ES.Never;
}
return; // we are done
}
}
}
}
// Now for the more involved case: we need to determine which type parameters determine equality support for each datatype in the SCC
// We start by seeing where each datatype's type parameters are used in a place known to determine equality support.
bool thingsChanged = false;
foreach (var dt in scc) {
if (dt.TypeArgs.Count == 0) {
// if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors
continue;
}
foreach (var ctor in dt.Ctors) {
foreach (var arg in ctor.Formals) {
var typeArg = arg.Type.AsTypeParameter;
if (typeArg != null) {
typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
thingsChanged = true;
} else {
var otherDt = arg.Type.AsIndDatatype;
if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) { // datatype is in a different SCC
var otherUdt = (UserDefinedType)arg.Type.Normalize();
var i = 0;
foreach (var otherTp in otherDt.TypeArgs) {
if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
var tp = otherUdt.TypeArgs[i].AsTypeParameter;
if (tp != null) {
tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
thingsChanged = true;
}
}
}
}
}
}
}
}
// Then we propagate this information up through the SCC
while (thingsChanged) {
thingsChanged = false;
foreach (var dt in scc) {
if (dt.TypeArgs.Count == 0) {
// if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors
continue;
}
foreach (var ctor in dt.Ctors) {
foreach (var arg in ctor.Formals) {
var otherDt = arg.Type.AsIndDatatype;
if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed) { // otherDt lives in the same SCC
var otherUdt = (UserDefinedType)arg.Type.Normalize();
var i = 0;
foreach (var otherTp in otherDt.TypeArgs) {
if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
var tp = otherUdt.TypeArgs[i].AsTypeParameter;
if (tp != null) {
tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = 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;
}
#endif
}
void ResolveAttributes(Attributes attrs, bool twoState) {
// order does not matter much for resolution, so resolve them in reverse order
for (; attrs != null; attrs = attrs.Prev) {
if (attrs.Args != null)
{
ResolveAttributeArgs(attrs.Args, twoState, true);
}
}
}
void ResolveAttributeArgs(List/*!*/ args, bool twoState, bool allowGhosts) {
Contract.Requires(args != null);
foreach (Attributes.Argument aa in args) {
Contract.Assert(aa != null);
if (aa.E != null) {
ResolveExpression(aa.E, twoState);
if (!allowGhosts) {
CheckIsNonGhost(aa.E);
}
}
}
}
void ResolveTypeParameters(List/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {
Contract.Requires(tparams != null);
Contract.Requires(parent != null);
// push non-duplicated type parameter names
foreach (TypeParameter tp in tparams) {
Contract.Assert(tp != null);
if (emitErrors) {
// we're seeing this TypeParameter for the first time
tp.Parent = parent;
}
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 defaultTypeArguments = f.TypeArgs.Count == 0 ? f.TypeArgs : null;
foreach (Formal p in f.Formals) {
if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
ResolveType(p.tok, p.Type, defaultTypeArguments, true);
}
ResolveType(f.tok, f.ResultType, defaultTypeArguments, true);
scope.PopMarker();
}
///
/// Assumes type parameters have already been pushed
///
void ResolveFunction(Function f){
Contract.Requires(f != null);
Contract.Requires(currentFunction == null);
Contract.Ensures(currentFunction == null);
scope.PushMarker();
currentFunction = f;
if (f.IsStatic) {
scope.AllowInstance = false;
}
foreach (Formal p in f.Formals) {
scope.Push(p.Name, p);
}
ResolveAttributes(f.Attributes, false);
foreach (Expression r in f.Req) {
ResolveExpression(r, false);
Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(r.Type, Type.Bool)) {
Error(r, "Precondition must be a boolean (got {0})", r.Type);
}
}
foreach (FrameExpression fr in f.Reads) {
ResolveFrameExpression(fr, "reads");
}
foreach (Expression r in f.Ens) {
ResolveExpression(r, false); // since this is a function, the postcondition is still a one-state predicate
Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(r.Type, Type.Bool)) {
Error(r, "Postcondition must be a boolean (got {0})", r.Type);
}
}
foreach (Expression r in f.Decreases.Expressions)
{
ResolveExpression(r, false);
// any type is fine
}
if (f.Body != null) {
var prevErrorCount = ErrorCount;
List matchVarContext = new List(f.Formals);
ResolveExpression(f.Body, false, matchVarContext);
if (!f.IsGhost) {
CheckIsNonGhost(f.Body);
}
Contract.Assert(f.Body.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(f.Body.Type, f.ResultType)) {
Error(f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
}
}
currentFunction = null;
scope.PopMarker();
}
void ResolveFrameExpression(FrameExpression fe, string kind) {
Contract.Requires(fe != null);
Contract.Requires(kind != null);
ResolveExpression(fe.E, false);
Type t = fe.E.Type;
Contract.Assert(t != null); // follows from postcondition of ResolveExpression
if (t is CollectionType) {
t = ((CollectionType)t).Arg;
}
if (t is ObjectType) {
// fine, as long as there's no field name
if (fe.FieldName != null) {
Error(fe.E, "type '{0}' does not contain a field named '{1}'", t, fe.FieldName);
}
} else if (UserDefinedType.DenotesClass(t) != null) {
// fine type
if (fe.FieldName != null) {
NonProxyType nptype;
MemberDecl member = ResolveMember(fe.E.tok, t, fe.FieldName, out nptype);
UserDefinedType ctype = (UserDefinedType)nptype; // correctness of cast follows from the DenotesClass test above
if (member == null) {
// error has already been reported by ResolveMember
} else if (!(member is Field)) {
Error(fe.E, "member {0} in type {1} does not refer to a field", fe.FieldName, cce.NonNull(ctype).Name);
} else {
Contract.Assert(ctype != null && ctype.ResolvedClass != null); // follows from postcondition of ResolveMember
fe.Field = (Field)member;
}
}
} else {
Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type);
}
}
///
/// 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 defaultTypeArguments = m.TypeArgs.Count == 0 ? m.TypeArgs : null;
// resolve in-parameters
foreach (Formal p in m.Ins) {
if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
ResolveType(p.tok, p.Type, defaultTypeArguments, true);
}
// resolve out-parameters
foreach (Formal p in m.Outs) {
if (!scope.Push(p.Name, p)) {
Error(p, "Duplicate parameter name: {0}", p.Name);
}
ResolveType(p.tok, p.Type, defaultTypeArguments, true);
}
scope.PopMarker();
}
///
/// Assumes type parameters have already been pushed
///
void ResolveMethod(Method m) {
Contract.Requires(m != null);
// Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported
scope.PushMarker();
if (m.IsStatic) {
scope.AllowInstance = false;
}
foreach (Formal p in m.Ins) {
scope.Push(p.Name, p);
}
// Start resolving specification...
foreach (MaybeFreeExpression e in m.Req) {
ResolveExpression(e.E, false);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E.Type, Type.Bool)) {
Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);
}
}
foreach (FrameExpression fe in m.Mod.Expressions) {
ResolveFrameExpression(fe, "modifies");
}
foreach (Expression e in m.Decreases.Expressions)
{
ResolveExpression(e, false);
// any type is fine
}
// Add out-parameters to a new scope that will also include the outermost-level locals of the body
// Don't care about any duplication errors among the out-parameters, since they have already been reported
scope.PushMarker();
foreach (Formal p in m.Outs) {
scope.Push(p.Name, p);
}
// attributes are allowed to mention both in- and out-parameters
ResolveAttributes(m.Attributes, false);
// ... continue resolving specification
foreach (MaybeFreeExpression e in m.Ens) {
ResolveExpression(e.E, true);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E.Type, Type.Bool)) {
Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
}
}
// Resolve body
if (m.Body != null) {
ResolveBlockStatement(m.Body, m.IsGhost, m);
}
scope.PopMarker(); // for the out-parameters and outermost-level locals
scope.PopMarker(); // for the in-parameters
}
void ResolveCtorSignature(DatatypeCtor ctor, List dtTypeArguments) {
Contract.Requires(ctor != null);
Contract.Requires(dtTypeArguments != null);
foreach (Formal p in ctor.Formals) {
ResolveType(p.tok, p.Type, dtTypeArguments, false);
}
}
///
/// If ResolveType encounters a type "T" that takes type arguments but wasn't given any, then:
/// * If "defaultTypeArguments" is non-null and "defaultTypeArgument.Count" equals the number
/// of type arguments that "T" expects, then use these default type arguments as "T"'s arguments.
/// * If "allowAutoTypeArguments" is true, then infer "T"'s arguments.
/// * If "defaultTypeArguments" is non-null AND "allowAutoTypeArguments" is true, then enough
/// type parameters will be added to "defaultTypeArguments" to have at least as many type
/// parameters as "T" expects, and then a prefix of the "defaultTypeArguments" will be supplied
/// as arguments to "T".
///
public void ResolveType(IToken tok, Type type, List defaultTypeArguments, bool allowAutoTypeArguments) {
Contract.Requires(tok != null);
Contract.Requires(type != null);
if (type is BasicType) {
// nothing to resolve
} else if (type is MapType) {
MapType mt = (MapType)type;
ResolveType(tok, mt.Domain, defaultTypeArguments, allowAutoTypeArguments);
ResolveType(tok, mt.Range, defaultTypeArguments, allowAutoTypeArguments);
if (mt.Domain.IsSubrangeType || mt.Range.IsSubrangeType) {
Error(tok, "sorry, cannot instantiate collection type with a subrange type");
}
} else if (type is CollectionType) {
var t = (CollectionType)type;
var argType = t.Arg;
ResolveType(tok, argType, defaultTypeArguments, allowAutoTypeArguments);
if (argType.IsSubrangeType) {
Error(tok, "sorry, cannot instantiate collection type with a subrange type");
}
} else if (type is UserDefinedType) {
UserDefinedType t = (UserDefinedType)type;
foreach (Type tt in t.TypeArgs) {
ResolveType(t.tok, tt, defaultTypeArguments, allowAutoTypeArguments);
if (tt.IsSubrangeType) {
Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");
}
}
TypeParameter tp = t.ModuleName == null ? allTypeParameters.Find(t.Name) : null;
if (tp != null) {
if (t.TypeArgs.Count == 0) {
t.ResolvedParam = tp;
} else {
Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);
}
} else if (t.ResolvedClass == null) { // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')
TopLevelDecl d = null;
if (t.ModuleName != null) {
foreach (var imp in currentClass.Module.Imports) {
if (imp.Name == t.ModuleName.val) {
// now search among the types declared in module "imp"
foreach (var tld in imp.TopLevelDecls) { // this search is slow, but oh well
if (tld.Name == t.Name) {
// found the class
d = tld;
goto DONE_WITH_QUALIFIED_NAME;
}
}
Error(t.tok, "Undeclared class name {0} in module {1}", t.Name, t.ModuleName.val);
goto DONE_WITH_QUALIFIED_NAME;
}
}
Error(t.ModuleName, "Undeclared module name: {0} (did you forget a module import?)", t.ModuleName.val);
DONE_WITH_QUALIFIED_NAME: ;
} else if (!classes.TryGetValue(t.Name, out d)) {
Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget a module import?)", t.Name);
}
if (d == null) {
// error has been reported above
} else if (d is AmbiguousTopLevelDecl) {
Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());
} else if (d is ArbitraryTypeDecl) {
t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType; // resolve like a type parameter
} else {
// d is a class or datatype, and it may have type parameters
t.ResolvedClass = d;
if (d.TypeArgs.Count != t.TypeArgs.Count && t.TypeArgs.Count == 0) {
if (allowAutoTypeArguments && defaultTypeArguments == null) {
// add type arguments that will be inferred
for (int i = 0; i < d.TypeArgs.Count; i++) {
t.TypeArgs.Add(new InferredTypeProxy());
}
} else if (defaultTypeArguments != null) {
// add specific type arguments, drawn from defaultTypeArguments (which may have to be extended)
if (allowAutoTypeArguments) {
// add to defaultTypeArguments the necessary number of arguments
for (int i = defaultTypeArguments.Count; i < d.TypeArgs.Count; i++) {
defaultTypeArguments.Add(new TypeParameter(t.tok, "_T" + i));
}
}
if (allowAutoTypeArguments || d.TypeArgs.Count == defaultTypeArguments.Count) {
Contract.Assert(d.TypeArgs.Count <= defaultTypeArguments.Count);
// automatically supply a prefix of the arguments from defaultTypeArguments
for (int i = 0; i < d.TypeArgs.Count; i++) {
var typeArg = new UserDefinedType(t.tok, defaultTypeArguments[i].Name, new List(), null);
typeArg.ResolvedParam = defaultTypeArguments[i]; // resolve "typeArg" here
t.TypeArgs.Add(typeArg);
}
}
}
}
// defaults and auto have been applied; check if we now have the right number of arguments
if (d.TypeArgs.Count != t.TypeArgs.Count) {
Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);
}
}
}
} else if (type is TypeProxy) {
TypeProxy t = (TypeProxy)type;
if (t.T != null) {
ResolveType(tok, t.T, defaultTypeArguments, allowAutoTypeArguments);
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
public bool UnifyTypes(Type a, Type b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
while (a is TypeProxy) {
TypeProxy proxy = (TypeProxy)a;
if (proxy.T == null) {
// merge a and b; to avoid cycles, first get to the bottom of b
while (b is TypeProxy && ((TypeProxy)b).T != null) {
b = ((TypeProxy)b).T;
}
return AssignProxy(proxy, b);
} else {
a = proxy.T;
}
}
while (b is TypeProxy) {
TypeProxy proxy = (TypeProxy)b;
if (proxy.T == null) {
// merge a and b (we have already got to the bottom of a)
return AssignProxy(proxy, a);
} else {
b = proxy.T;
}
}
#if !NO_CHEAP_OBJECT_WORKAROUND
if (a is ObjectType || b is ObjectType) { // TODO: remove this temporary hack
var other = a is ObjectType ? b : a;
if (other is BoolType || other is IntType || other is SetType || other is SeqType || other.IsDatatype) {
return false;
}
// allow anything else with object; this is BOGUS
return true;
}
#endif
// Now, a and b are non-proxies and stand for the same things as the original a and b, respectively.
if (a is BoolType) {
return b is BoolType;
} else if (a is IntType) {
return b is IntType;
} else if (a is ObjectType) {
return b is ObjectType;
} else if (a is SetType) {
return b is SetType && UnifyTypes(((SetType)a).Arg, ((SetType)b).Arg);
} else if (a is MultiSetType) {
return b is MultiSetType && UnifyTypes(((MultiSetType)a).Arg, ((MultiSetType)b).Arg);
}else if (a is MapType) {
return b is MapType && UnifyTypes(((MapType)a).Domain, ((MapType)b).Domain) && UnifyTypes(((MapType)a).Range, ((MapType)b).Range);
} else if (a is SeqType) {
return b is SeqType && UnifyTypes(((SeqType)a).Arg, ((SeqType)b).Arg);
} else if (a is UserDefinedType) {
if (!(b is UserDefinedType)) {
return false;
}
UserDefinedType aa = (UserDefinedType)a;
UserDefinedType bb = (UserDefinedType)b;
if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) {
// these are both resolved class/datatype types
Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count);
bool successSoFar = true;
for (int i = 0; i < aa.TypeArgs.Count; i++) {
if (!UnifyTypes(aa.TypeArgs[i], bb.TypeArgs[i])) {
successSoFar = false;
}
}
return successSoFar;
} else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {
// these are both resolved type parameters
Contract.Assert(aa.TypeArgs.Count == 0 && bb.TypeArgs.Count == 0);
return true;
} else {
// something is wrong; either aa or bb wasn't properly resolved, or they don't unify
return false;
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
}
}
bool AssignProxy(TypeProxy proxy, Type t){
Contract.Requires(proxy != null);
Contract.Requires(t != null);
Contract.Requires(proxy.T == null);
Contract.Requires(!(t is TypeProxy) || ((TypeProxy)t).T == null);
//modifies proxy.T, ((TypeProxy)t).T; // might also change t.T if t is a proxy
Contract.Ensures(Contract.Result() == (proxy == t || proxy.T != null || (t is TypeProxy && ((TypeProxy)t).T != null)));
if (proxy == t) {
// they are already in the same equivalence class
return true;
} else if (proxy is UnrestrictedTypeProxy) {
// it's fine to redirect proxy to t (done below)
} else if (t is UnrestrictedTypeProxy) {
// merge proxy and t by redirecting t to proxy, rather than the other way around
((TypeProxy)t).T = proxy;
return true;
} else if (t is RestrictedTypeProxy) {
// Both proxy and t are restricted type proxies. To simplify unification, order proxy and t
// according to their types.
RestrictedTypeProxy r0 = (RestrictedTypeProxy)proxy;
RestrictedTypeProxy r1 = (RestrictedTypeProxy)t;
if (r0.OrderID <= r1.OrderID) {
return AssignRestrictedProxies(r0, r1);
} else {
return AssignRestrictedProxies(r1, r0);
}
// In the remaining cases, proxy is a restricted proxy and t is a non-proxy
} else if (proxy is DatatypeProxy) {
if (t.IsIndDatatype) {
// all is fine, proxy can be redirected to t
} else {
return false;
}
} else if (proxy is ObjectTypeProxy) {
if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {
// all is fine, proxy can be redirected to t
} else {
return false;
}
} else if (proxy is CollectionTypeProxy) {
CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy;
if (t is CollectionType) {
if (!UnifyTypes(collProxy.Arg, ((CollectionType)t).Arg)) {
return false;
}
} else {
return false;
}
} else if (proxy is OperationTypeProxy) {
OperationTypeProxy opProxy = (OperationTypeProxy)proxy;
if (t is IntType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) {
// this is the expected case
} else {
return false;
}
} else if (proxy is IndexableTypeProxy) {
IndexableTypeProxy iProxy = (IndexableTypeProxy)proxy;
if (t is SeqType) {
if (!UnifyTypes(iProxy.Arg, ((SeqType)t).Arg)) {
return false;
}
if (!UnifyTypes(iProxy.Domain, Type.Int)) {
return false;
}
} else if (t.IsArrayType && (t.AsArrayType).Dims == 1) {
Type elType = UserDefinedType.ArrayElementType(t);
if (!UnifyTypes(iProxy.Arg, elType)) {
return false;
}
if (!UnifyTypes(iProxy.Domain, Type.Int)) {
return false;
}
} else if (t is MapType) {
if (!UnifyTypes(iProxy.Arg, ((MapType)t).Range)) {
return false;
}
if (!UnifyTypes(iProxy.Domain, ((MapType)t).Domain)) {
return false;
}
} else {
return false;
}
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected proxy type
}
// do the merge, but never infer a subrange type
if (t is NatType) {
proxy.T = Type.Int;
} else {
proxy.T = t;
}
return true;
}
bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b)
{ Contract.Requires(a != null);
Contract.Requires(b != null);
Contract.Requires(a != b);
Contract.Requires(a.T == null && b.T == null);
Contract.Requires(a.OrderID <= b.OrderID);
//modifies a.T, b.T;
Contract.Ensures(Contract.Result() || a.T != null || b.T != null);
if (a is DatatypeProxy) {
if (b is DatatypeProxy) {
// all is fine
a.T = b;
return true;
} else {
return false;
}
} else if (a is ObjectTypeProxy) {
if (b is ObjectTypeProxy) {
// all is fine
a.T = b;
return true;
} else if (b is IndexableTypeProxy) {
// the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type
a.T = builtIns.ArrayType(1, ((IndexableTypeProxy)b).Arg);
b.T = a.T;
return true;
} else {
return false;
}
} else if (a is CollectionTypeProxy) {
if (b is CollectionTypeProxy) {
a.T = b;
return UnifyTypes(((CollectionTypeProxy)a).Arg, ((CollectionTypeProxy)b).Arg);
} else if (b is OperationTypeProxy) {
if (((OperationTypeProxy)b).AllowSeq) {
b.T = a; // a is a stronger constraint than b
} else {
// a says set,seq and b says int,set; the intersection is set
a.T = new SetType(((CollectionTypeProxy)a).Arg);
b.T = a.T;
}
return true;
} else if (b is IndexableTypeProxy) {
CollectionTypeProxy pa = (CollectionTypeProxy)a;
IndexableTypeProxy pb = (IndexableTypeProxy)b;
// a and b could be a map or a sequence
return true;
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
}
} else if (a is OperationTypeProxy) {
OperationTypeProxy pa = (OperationTypeProxy)a;
if (b is OperationTypeProxy) {
if (!pa.AllowSeq || ((OperationTypeProxy)b).AllowSeq) {
b.T = a;
} else {
a.T = b; // b has the stronger requirement
}
return true;
} else {
IndexableTypeProxy pb = (IndexableTypeProxy)b; // cast justification: lse we have unexpected restricted-proxy type
if (pa.AllowSeq) {
// strengthen a and b to a sequence type
b.T = new SeqType(pb.Arg);
a.T = b.T;
return true;
} else {
return false;
}
}
} else if (a is IndexableTypeProxy) {
Contract.Assert(b is IndexableTypeProxy); // else we have unexpected restricted-proxy type
a.T = b;
return UnifyTypes(((IndexableTypeProxy)a).Arg, ((IndexableTypeProxy)b).Arg);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
}
}
///
/// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it
/// at run time. That means it must not have any side effects on non-ghost variables, for example.
///
public void ResolveStatement(Statement stmt, bool specContextOnly, Method method) {
Contract.Requires(stmt != null);
Contract.Requires(method != null);
if (stmt is PredicateStmt) {
PredicateStmt s = (PredicateStmt)stmt;
ResolveAttributes(s.Attributes, false);
s.IsGhost = true;
ResolveExpression(s.Expr, true);
Contract.Assert(s.Expr.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(s.Expr.Type, Type.Bool)) {
Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);
}
} else if (stmt is PrintStmt) {
PrintStmt s = (PrintStmt)stmt;
ResolveAttributeArgs(s.Args, false, false);
if (specContextOnly) {
Error(stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
} else if (stmt is BreakStmt) {
var s = (BreakStmt)stmt;
if (s.TargetLabel != null) {
Statement target = labeledStatements.Find(s.TargetLabel);
if (target == null) {
Error(s, "break label is undefined or not in scope: {0}", s.TargetLabel);
} else {
s.TargetStmt = target;
bool targetIsLoop = target is WhileStmt || target is AlternativeLoopStmt;
if (specContextOnly && !s.TargetStmt.IsGhost && !inSpecOnlyContext[s.TargetStmt]) {
Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure"));
}
}
} else {
if (loopStack.Count < s.BreakCount) {
Error(s, "trying to break out of more loop levels than there are enclosing loops");
} else {
Statement target = loopStack[loopStack.Count - s.BreakCount];
if (target.Labels == null) {
// make sure there is a label, because the compiler and translator will want to see a unique ID
target.Labels = new LList