diff options
37 files changed, 1881 insertions, 1418 deletions
diff --git a/Chalice/src/main/scala/PrettyPrinter.scala b/Chalice/src/main/scala/PrettyPrinter.scala index 18557b99..a54173df 100644 --- a/Chalice/src/main/scala/PrettyPrinter.scala +++ b/Chalice/src/main/scala/PrettyPrinter.scala @@ -285,7 +285,7 @@ object PrintProgram { case IntPermTimes(n, p) => BinExpr(n, p, "*", 0x60, false, false, contextBindingPower, fragileContext)
case Epsilons(e) => print("rd("); Expr(e); print(")");
case Access(e, p) => print("acc("); Expr(e); print(", "); Expr(p); print(")")
- case AccessAll(obj, p) => print("acc("); Expr(obj); print(", "); print(".*"); Expr(p); print(")")
+ case AccessAll(obj, p) => print("acc("); Expr(obj); print(".*"); print(", "); Expr(p); print(")")
case AccessSeq(s, f, p) => print("acc("); Expr(s); print(", "); print("[*].");
f match { case None => print("*"); case Some(x) => print(x)}
Expr(p); print(")")
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index ae26d8db..746504b3 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -594,6 +594,15 @@ namespace Microsoft.Boogie { program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
}
+ if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining > 0) {
+ BlockPredicator.Predicate(program, false, false);
+ if (CommandLineOptions.Clo.PrintInstrumented) {
+ using (TokenTextWriter writer = new TokenTextWriter(Console.Out)) {
+ program.Emit(writer);
+ }
+ }
+ }
+
Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;
if (CommandLineOptions.Clo.ExtractLoops)
{
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 7d55e177..e7633014 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -574,6 +574,8 @@ namespace Microsoft.Boogie { public string CoverageReporterPath = null;
public Process coverageReporter = null; // used internally for debugging
+ public bool DoPredication = false;
+
public enum TypeEncoding {
None,
Predicates,
@@ -1230,7 +1232,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
- ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)
+ ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||
+ ps.CheckBooleanFlag("predicate", ref DoPredication)
) {
// one of the boolean flags matched
return true;
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 66756b0c..4b9e0c27 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -290,10 +290,13 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.> ArbitraryTypeDecl<ModuleDecl/*!*/ module, out ArbitraryTypeDecl at>
= (. IToken/*!*/ id;
Attributes attrs = null;
+ var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
.)
"type"
{ Attribute<ref attrs> }
- Ident<out id> (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .)
+ Ident<out id>
+ [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
+ ] (. at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); .)
SYNC ";"
.
GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>
@@ -356,10 +359,16 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t /*------------------------------------------------------------------------*/
GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
= (. Contract.Requires(cce.NonNullElements(typeArgs));
- IToken/*!*/ id; .)
+ IToken/*!*/ id;
+ TypeParameter.EqualitySupportValue eqSupport;
+ .)
"<"
- Ident<out id> (. typeArgs.Add(new TypeParameter(id, id.val)); .)
- { "," Ident<out id> (. typeArgs.Add(new TypeParameter(id, id.val)); .)
+ Ident<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
+ [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
+ ] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
+ { "," Ident<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
+ [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
+ ] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
}
">"
.
@@ -1027,11 +1036,11 @@ CaseStatement<out MatchCaseStmt/*!*/ c> /*------------------------------------------------------------------------*/
AssertStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
- Expression/*!*/ e = null; Attributes attrs = null;
+ Expression e = null; Attributes attrs = null;
.)
- "assert" (. x = t; s = null;.)
+ "assert" (. x = t; .)
{ IF(IsAttribute()) Attribute<ref attrs> }
- ( Expression<out e>
+ ( Expression<out e>
| "..."
)
";"
@@ -1043,9 +1052,21 @@ AssertStmt<out Statement/*!*/ s> .)
.
AssumeStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
+ Expression e = null; Attributes attrs = null;
+ .)
"assume" (. x = t; .)
- Expression<out e> ";" (. s = new AssumeStmt(x, e); .)
+ { IF(IsAttribute()) Attribute<ref attrs> }
+ ( Expression<out e>
+ | "..."
+ )
+ (. if (e == null) {
+ s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
+ } else {
+ s = new AssumeStmt(x, e, attrs);
+ }
+ .)
+ ";"
.
PrintStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 5e6ad5c3..bf985ddc 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -269,8 +269,18 @@ namespace Microsoft.Dafny { }
public bool IsTypeParameter {
get {
+ return AsTypeParameter != null;
+ }
+ }
+ public TypeParameter AsTypeParameter {
+ get {
UserDefinedType ct = this as UserDefinedType;
- return ct != null && ct.ResolvedParam != null;
+ return ct == null ? null : ct.ResolvedParam;
+ }
+ }
+ public virtual bool SupportsEquality {
+ get {
+ return true;
}
}
}
@@ -318,16 +328,20 @@ namespace Microsoft.Dafny { public abstract class CollectionType : NonProxyType
{
- public readonly Type Arg;
+ public readonly Type Arg; // denotes the Domain type for a Map
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Arg != null);
}
-
public CollectionType(Type arg) {
Contract.Requires(arg != null);
this.Arg = arg;
}
+ public override bool SupportsEquality {
+ get {
+ return Arg.SupportsEquality;
+ }
+ }
}
public class SetType : CollectionType {
@@ -369,12 +383,14 @@ namespace Microsoft.Dafny { }
public class MapType : CollectionType
{
- public Type Domain, Range;
+ public Type Range;
public MapType(Type domain, Type range) : base(domain) {
Contract.Requires(domain != null && range != null);
- Domain = domain;
Range = range;
}
+ public Type Domain {
+ get { return Arg; }
+ }
[Pure]
public override string ToString() {
Contract.Ensures(Contract.Result<string>() != null);
@@ -515,6 +531,35 @@ namespace Microsoft.Dafny { }
return s;
}
+
+ public override bool SupportsEquality {
+ get {
+ if (ResolvedClass is ClassDecl) {
+ return true;
+ } else if (ResolvedClass is CoDatatypeDecl) {
+ return false;
+ } else if (ResolvedClass is IndDatatypeDecl) {
+ var dt = (IndDatatypeDecl)ResolvedClass;
+ Contract.Assume(dt.EqualitySupport != IndDatatypeDecl.ES.NotYetComputed);
+ if (dt.EqualitySupport == IndDatatypeDecl.ES.Never) {
+ return false;
+ }
+ Contract.Assert(dt.TypeArgs.Count == TypeArgs.Count);
+ var i = 0;
+ foreach (var tp in dt.TypeArgs) {
+ if (tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && !TypeArgs[i].SupportsEquality) {
+ return false;
+ }
+ i++;
+ }
+ return true;
+ } else if (ResolvedParam != null) {
+ return ResolvedParam.MustSupportEquality;
+ }
+ Contract.Assume(false); // the SupportsEquality getter requires the Type to have been successfully resolved
+ return true;
+ }
+ }
}
public abstract class TypeProxy : Type {
@@ -529,6 +574,15 @@ namespace Microsoft.Dafny { Contract.Assume(T == null || cce.IsPeerConsistent(T));
return T == null ? "?" : T.ToString();
}
+ public override bool SupportsEquality {
+ get {
+ if (T != null) {
+ return T.SupportsEquality;
+ } else {
+ return base.SupportsEquality;
+ }
+ }
+ }
}
public abstract class UnrestrictedTypeProxy : TypeProxy {
@@ -589,17 +643,6 @@ namespace Microsoft.Dafny { }
/// <summary>
- /// This proxy stands for object or any class/array type or a set/sequence of object or a class/array type.
- /// </summary>
- public class ObjectsTypeProxy : RestrictedTypeProxy {
- public override int OrderID {
- get {
- return 2;
- }
- }
- }
-
- /// <summary>
/// This proxy stands for:
/// set(Arg) or seq(Arg) or map(Arg, Range)
/// </summary>
@@ -616,7 +659,7 @@ namespace Microsoft.Dafny { }
public override int OrderID {
get {
- return 3;
+ return 2;
}
}
}
@@ -635,7 +678,7 @@ namespace Microsoft.Dafny { }
public override int OrderID {
get {
- return 4;
+ return 3;
}
}
}
@@ -658,7 +701,7 @@ namespace Microsoft.Dafny { }
public override int OrderID {
get {
- return 5;
+ return 4;
}
}
}
@@ -723,10 +766,19 @@ namespace Microsoft.Dafny { parent = value;
}
}
- public TypeParameter(IToken tok, string name)
+ public enum EqualitySupportValue { Required, InferredRequired, Unspecified }
+ public EqualitySupportValue EqualitySupport; // the resolver may change this value from Unspecified to InferredRequired (for some signatures that may immediately imply that equality support is required)
+ public bool MustSupportEquality {
+ get { return EqualitySupport != EqualitySupportValue.Unspecified; }
+ }
+
+ public bool NecessaryForEqualitySupportOfSurroundingInductiveDatatype = false; // computed during resolution; relevant only when Parent denotes an IndDatatypeDecl
+
+ public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified)
: base(tok, name, null) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
+ EqualitySupport = equalitySupport;
}
}
@@ -888,7 +940,10 @@ namespace Microsoft.Dafny { public class IndDatatypeDecl : DatatypeDecl
{
public DatatypeCtor DefaultCtor; // set during resolution
- public bool[] TypeParametersUsedInConstructionByDefaultCtor; // set during resolution; has same length as
+ public bool[] TypeParametersUsedInConstructionByDefaultCtor; // set during resolution; has same length as the number of type arguments
+
+ public enum ES { NotYetComputed, Never, ConsultTypeArguments }
+ public ES EqualitySupport = ES.NotYetComputed;
public IndDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List<TypeParameter/*!*/>/*!*/ typeArgs,
[Captured] List<DatatypeCtor/*!*/>/*!*/ ctors, Attributes attributes)
@@ -953,13 +1008,15 @@ namespace Microsoft.Dafny { public abstract class MemberDecl : Declaration {
public readonly bool IsStatic;
+ public readonly bool IsGhost;
public TopLevelDecl EnclosingClass; // filled in during resolution
- public MemberDecl(IToken tok, string name, bool isStatic, Attributes attributes)
+ public MemberDecl(IToken tok, string name, bool isStatic, bool isGhost, Attributes attributes)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
IsStatic = isStatic;
+ IsGhost = isGhost;
}
/// <summary>
/// Returns className+"."+memberName. Available only after resolution.
@@ -983,7 +1040,6 @@ namespace Microsoft.Dafny { }
public class Field : MemberDecl {
- public readonly bool IsGhost;
public readonly bool IsMutable;
public readonly Type Type;
[ContractInvariantMethod]
@@ -999,11 +1055,10 @@ namespace Microsoft.Dafny { }
public Field(IToken tok, string name, bool isGhost, bool isMutable, Type type, Attributes attributes)
- : base(tok, name, false, attributes) {
+ : base(tok, name, false, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
- IsGhost = isGhost;
IsMutable = isMutable;
Type = type;
}
@@ -1043,17 +1098,23 @@ namespace Microsoft.Dafny { public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType
{
public readonly TypeParameter TheType;
+ public TypeParameter.EqualitySupportValue EqualitySupport {
+ get { return TheType.EqualitySupport; }
+ }
+ public bool MustSupportEquality {
+ get { return TheType.MustSupportEquality; }
+ }
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(TheType != null && Name == TheType.Name);
}
- public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, Attributes attributes)
+ public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, TypeParameter.EqualitySupportValue equalitySupport, Attributes attributes)
: base(tok, name, module, new List<TypeParameter>(), attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(module != null);
- TheType = new TypeParameter(tok, name);
+ TheType = new TypeParameter(tok, name, equalitySupport);
}
}
@@ -1153,7 +1214,7 @@ namespace Microsoft.Dafny { return name + nm.Substring(i);
}
} else {
- string nxt = nm.Substring(i, j);
+ string nxt = nm.Substring(i, j - i);
name = name == null ? nxt : name + nxt;
switch (nm[j]) {
case '\'': name += "_k"; break;
@@ -1274,7 +1335,6 @@ namespace Microsoft.Dafny { }
public class Function : MemberDecl, TypeParameter.ParentType {
- public readonly bool IsGhost; // functions are "ghost" by default; a non-ghost function is called a "function method"
public bool IsRecursive; // filled in during resolution
public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;
public readonly IToken OpenParen; // can be null (for predicates), if there are no formals
@@ -1297,11 +1357,14 @@ namespace Microsoft.Dafny { Contract.Invariant(Decreases != null);
}
+ /// <summary>
+ /// Note, functions are "ghost" by default; a non-ghost function is called a "function method".
+ /// </summary>
public Function(IToken tok, string name, bool isStatic, bool isGhost,
List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals, Type resultType,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
Expression body, Attributes attributes, bool signatureOmitted)
- : base(tok, name, isStatic, attributes) {
+ : base(tok, name, isStatic, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -1312,7 +1375,6 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(reads));
Contract.Requires(cce.NonNullElements(ens));
Contract.Requires(decreases != null);
- this.IsGhost = isGhost;
this.TypeArgs = typeArgs;
this.OpenParen = openParen;
this.Formals = formals;
@@ -1341,7 +1403,6 @@ namespace Microsoft.Dafny { public class Method : MemberDecl, TypeParameter.ParentType
{
- public readonly bool IsGhost;
public readonly bool SignatureIsOmitted;
public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;
public readonly List<Formal/*!*/>/*!*/ Ins;
@@ -1372,7 +1433,7 @@ namespace Microsoft.Dafny { [Captured] Specification<Expression>/*!*/ decreases,
[Captured] BlockStmt body,
Attributes attributes, bool signatureOmitted)
- : base(tok, name, isStatic, attributes) {
+ : base(tok, name, isStatic, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
@@ -1382,7 +1443,6 @@ namespace Microsoft.Dafny { Contract.Requires(mod != null);
Contract.Requires(cce.NonNullElements(ens));
Contract.Requires(decreases != null);
- this.IsGhost = isGhost;
this.TypeArgs = typeArgs;
this.Ins = ins;
this.Outs = outs;
@@ -1507,60 +1567,40 @@ namespace Microsoft.Dafny { public abstract class PredicateStmt : Statement
{
- [Peer]
public readonly Expression Expr;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Expr != null);
}
- [Captured]
public PredicateStmt(IToken tok, Expression expr, Attributes attrs)
: base(tok, attrs) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
- Contract.Ensures(cce.Owner.Same(this, expr));
- cce.Owner.AssignSame(this, expr);
this.Expr = expr;
}
- [Captured]
public PredicateStmt(IToken tok, Expression expr)
: this(tok, expr, null) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
- Contract.Ensures(cce.Owner.Same(this, expr));
- cce.Owner.AssignSame(this, expr);
this.Expr = expr;
}
}
public class AssertStmt : PredicateStmt {
- [Captured]
public AssertStmt(IToken/*!*/ tok, Expression/*!*/ expr, Attributes attrs)
: base(tok, expr, attrs) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
- Contract.Ensures(cce.Owner.Same(this, expr));
- }
-
- [Captured]
- public AssertStmt(IToken/*!*/ tok, Expression/*!*/ expr)
- : this(tok, expr, null) {
- Contract.Requires(tok != null);
- Contract.Requires(expr != null);
- Contract.Ensures(cce.Owner.Same(this, expr));
}
}
public class AssumeStmt : PredicateStmt {
- [Captured]
- public AssumeStmt(IToken/*!*/ tok, Expression/*!*/ expr)
- : base(tok, expr) {
+ public AssumeStmt(IToken/*!*/ tok, Expression/*!*/ expr, Attributes attrs)
+ : base(tok, expr, attrs) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
- Contract.Ensures(cce.Owner.Same(this, expr));
-
}
}
@@ -1640,6 +1680,18 @@ namespace Microsoft.Dafny { Attributes = attrs;
}
public abstract bool CanAffectPreviouslyKnownExpressions { get; }
+ /// <summary>
+ /// Returns the non-null subexpressions of the AssignmentRhs.
+ /// </summary>
+ public virtual IEnumerable<Expression> SubExpressions {
+ get { yield break; }
+ }
+ /// <summary>
+ /// Returns the non-null sub-statements of the AssignmentRhs.
+ /// </summary>
+ public virtual IEnumerable<Statement> SubStatements{
+ get { yield break; }
+ }
}
public class ExprRhs : AssignmentRhs
@@ -1657,6 +1709,11 @@ namespace Microsoft.Dafny { Expr = expr;
}
public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Expr;
+ }
+ }
}
public class TypeRhs : AssignmentRhs
@@ -1705,6 +1762,23 @@ namespace Microsoft.Dafny { return false;
}
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ if (ArrayDimensions != null) {
+ foreach (var e in ArrayDimensions) {
+ yield return e;
+ }
+ }
+ }
+ }
+ public override IEnumerable<Statement> SubStatements {
+ get {
+ if (InitCall != null) {
+ yield return InitCall;
+ }
+ }
+ }
}
public class CallRhs : AssignmentRhs
@@ -1744,6 +1818,14 @@ namespace Microsoft.Dafny { return false;
}
}
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Receiver;
+ foreach (var e in Args) {
+ yield return e;
+ }
+ }
+ }
}
public class HavocRhs : AssignmentRhs {
@@ -1980,6 +2062,7 @@ namespace Microsoft.Dafny { public Expression/*!*/ Receiver;
public readonly string/*!*/ MethodName;
public readonly List<Expression/*!*/>/*!*/ Args;
+ public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions; // create, initialized, and used by resolution (could be deleted once all of resolution is done)
public Method Method; // filled in by resolution
public CallStmt(IToken tok, List<Expression/*!*/>/*!*/ lhs, Expression/*!*/ receiver,
@@ -2018,13 +2101,13 @@ namespace Microsoft.Dafny { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Thn != null);
- Contract.Invariant(Els == null || Els is BlockStmt || Els is IfStmt);
+ Contract.Invariant(Els == null || Els is BlockStmt || Els is IfStmt || Els is SkeletonStatement);
}
public IfStmt(IToken tok, Expression guard, BlockStmt thn, Statement els)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(thn != null);
- Contract.Requires(els == null || els is BlockStmt || els is IfStmt);
+ Contract.Requires(els == null || els is BlockStmt || els is IfStmt || els is SkeletonStatement);
this.Guard = guard;
this.Thn = thn;
this.Els = els;
@@ -2317,6 +2400,8 @@ namespace Microsoft.Dafny { /// S == null
/// * assert ...
/// ConditionOmitted == true
+ /// * assume ...
+ /// ConditionOmitted == true
/// * if ... { Stmt }
/// if ... { Stmt } else ElseStmt
/// ConditionOmitted == true
@@ -2785,6 +2870,7 @@ namespace Microsoft.Dafny { public readonly Expression/*!*/ Receiver;
public readonly IToken OpenParen; // can be null if Args.Count == 0
public readonly List<Expression/*!*/>/*!*/ Args;
+ public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions; // create, initialized, and used by resolution (could be deleted once all of resolution is done)
public enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects, NoBecauseRecursiveCallsAreNotAllowedInThisContext, NoBecauseIsNotGuarded }
public CoCallResolution CoCall = CoCallResolution.No; // indicates whether or not the call is a co-recursive call; filled in by resolution
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 26b98833..a4e51924 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -315,7 +315,7 @@ bool IsAttribute() { Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 22) {
+ if (la.kind == 25) {
GenericParameters(typeArgs);
}
Expect(6);
@@ -351,7 +351,7 @@ bool IsAttribute() { Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 22) {
+ if (la.kind == 25) {
GenericParameters(typeArgs);
}
Expect(16);
@@ -376,13 +376,20 @@ bool IsAttribute() { void ArbitraryTypeDecl(ModuleDecl/*!*/ module, out ArbitraryTypeDecl at) {
IToken/*!*/ id;
Attributes attrs = null;
+ var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
Expect(21);
while (la.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- at = new ArbitraryTypeDecl(id, id.val, module, attrs);
+ if (la.kind == 22) {
+ Get();
+ Expect(23);
+ Expect(24);
+ eqSupport = TypeParameter.EqualitySupportValue.Required;
+ }
+ at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(113); Get();}
Expect(18);
}
@@ -405,10 +412,10 @@ bool IsAttribute() { }
if (la.kind == 19) {
FieldDecl(mmod, mm);
- } else if (la.kind == 44 || la.kind == 45) {
+ } else if (la.kind == 45 || la.kind == 46) {
FunctionDecl(mmod, out f);
mm.Add(f);
- } else if (la.kind == 24 || la.kind == 25) {
+ } else if (la.kind == 27 || la.kind == 28) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
} else SynErr(114);
@@ -416,16 +423,32 @@ bool IsAttribute() { void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
Contract.Requires(cce.NonNullElements(typeArgs));
- IToken/*!*/ id;
- Expect(22);
+ IToken/*!*/ id;
+ TypeParameter.EqualitySupportValue eqSupport;
+
+ Expect(25);
Ident(out id);
- typeArgs.Add(new TypeParameter(id, id.val));
+ eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
+ if (la.kind == 22) {
+ Get();
+ Expect(23);
+ Expect(24);
+ eqSupport = TypeParameter.EqualitySupportValue.Required;
+ }
+ typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
while (la.kind == 20) {
Get();
Ident(out id);
- typeArgs.Add(new TypeParameter(id, id.val));
+ eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
+ if (la.kind == 22) {
+ Get();
+ Expect(23);
+ Expect(24);
+ eqSupport = TypeParameter.EqualitySupportValue.Required;
+ }
+ typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
}
- Expect(23);
+ Expect(26);
}
void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {
@@ -470,9 +493,9 @@ bool IsAttribute() { IToken bodyEnd = Token.NoToken;
bool signatureOmitted = false;
- if (la.kind == 44) {
+ if (la.kind == 45) {
Get();
- if (la.kind == 24) {
+ if (la.kind == 27) {
Get();
isFunctionMethod = true;
}
@@ -482,22 +505,22 @@ bool IsAttribute() { Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 22 || la.kind == 33) {
- if (la.kind == 22) {
+ if (la.kind == 22 || la.kind == 25) {
+ if (la.kind == 25) {
GenericParameters(typeArgs);
}
Formals(true, isFunctionMethod, formals, out openParen);
Expect(5);
Type(out returnType);
- } else if (la.kind == 27) {
+ } else if (la.kind == 30) {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
} else SynErr(117);
- } else if (la.kind == 45) {
+ } else if (la.kind == 46) {
Get();
isPredicate = true;
- if (la.kind == 24) {
+ if (la.kind == 27) {
Get();
isFunctionMethod = true;
}
@@ -508,17 +531,17 @@ bool IsAttribute() { }
Ident(out id);
if (StartOf(4)) {
- if (la.kind == 22) {
+ if (la.kind == 25) {
GenericParameters(typeArgs);
}
- if (la.kind == 33) {
+ if (la.kind == 22) {
Formals(true, isFunctionMethod, formals, out openParen);
if (la.kind == 5) {
Get();
SemErr(t, "predicates do not have an explicitly declared return type; it is always bool");
}
}
- } else if (la.kind == 27) {
+ } else if (la.kind == 30) {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
@@ -562,10 +585,10 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(120); Get();}
- if (la.kind == 24) {
+ while (!(la.kind == 0 || la.kind == 27 || la.kind == 28)) {SynErr(120); Get();}
+ if (la.kind == 27) {
Get();
- } else if (la.kind == 25) {
+ } else if (la.kind == 28) {
Get();
if (allowConstructor) {
isConstructor = true;
@@ -587,17 +610,17 @@ bool IsAttribute() { Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 22 || la.kind == 33) {
- if (la.kind == 22) {
+ if (la.kind == 22 || la.kind == 25) {
+ if (la.kind == 25) {
GenericParameters(typeArgs);
}
Formals(true, !mmod.IsGhost, ins, out openParen);
- if (la.kind == 26) {
+ if (la.kind == 29) {
Get();
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs, out openParen);
}
- } else if (la.kind == 27) {
+ } else if (la.kind == 30) {
Get();
signatureOmitted = true; openParen = Token.NoToken;
} else SynErr(122);
@@ -629,7 +652,7 @@ bool IsAttribute() { Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 33) {
+ if (la.kind == 22) {
FormalsOptionalIds(formals);
}
ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
@@ -637,7 +660,7 @@ bool IsAttribute() { void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
- Expect(33);
+ Expect(22);
if (StartOf(7)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
@@ -647,7 +670,7 @@ bool IsAttribute() { formals.Add(new Formal(id, name, ty, true, isGhost));
}
}
- Expect(34);
+ Expect(24);
}
void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
@@ -731,22 +754,22 @@ bool IsAttribute() { List<Type/*!*/>/*!*/ gt;
switch (la.kind) {
- case 35: {
+ case 36: {
Get();
tok = t;
break;
}
- case 36: {
+ case 37: {
Get();
tok = t; ty = new NatType();
break;
}
- case 37: {
+ case 38: {
Get();
tok = t; ty = new IntType();
break;
}
- case 38: {
+ case 39: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -757,7 +780,7 @@ bool IsAttribute() { break;
}
- case 39: {
+ case 40: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -768,7 +791,7 @@ bool IsAttribute() { break;
}
- case 40: {
+ case 41: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -779,7 +802,7 @@ bool IsAttribute() { break;
}
- case 41: {
+ case 42: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -790,7 +813,7 @@ bool IsAttribute() { break;
}
- case 1: case 3: case 42: {
+ case 1: case 3: case 43: {
ReferenceType(out tok, out ty);
break;
}
@@ -800,7 +823,7 @@ bool IsAttribute() { void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
- Expect(33);
+ Expect(22);
openParen = t;
if (la.kind == 1 || la.kind == 8) {
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
@@ -811,7 +834,7 @@ bool IsAttribute() { formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
}
}
- Expect(34);
+ Expect(24);
}
void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
@@ -820,7 +843,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null;
while (!(StartOf(8))) {SynErr(124); Get();}
- if (la.kind == 28) {
+ if (la.kind == 31) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -836,18 +859,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
while (!(la.kind == 0 || la.kind == 18)) {SynErr(125); Get();}
Expect(18);
- } else if (la.kind == 29 || la.kind == 30 || la.kind == 31) {
- if (la.kind == 29) {
+ } else if (la.kind == 32 || la.kind == 33 || la.kind == 34) {
+ if (la.kind == 32) {
Get();
isFree = true;
}
- if (la.kind == 30) {
+ if (la.kind == 33) {
Get();
Expression(out e);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();}
Expect(18);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
@@ -857,7 +880,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(18);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
} else SynErr(128);
- } else if (la.kind == 32) {
+ } else if (la.kind == 35) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
@@ -885,7 +908,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void FrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
Expression(out e);
- if (la.kind == 48) {
+ if (la.kind == 49) {
Get();
Ident(out id);
fieldName = id.val;
@@ -920,7 +943,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {
Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
- Expect(22);
+ Expect(25);
Type(out ty);
gt.Add(ty);
while (la.kind == 20) {
@@ -928,7 +951,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Type(out ty);
gt.Add(ty);
}
- Expect(23);
+ Expect(26);
}
void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
@@ -937,7 +960,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken moduleName = null;
List<Type/*!*/>/*!*/ gt;
- if (la.kind == 42) {
+ if (la.kind == 43) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 3) {
@@ -956,12 +979,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 1) {
Ident(out tok);
gt = new List<Type/*!*/>();
- if (la.kind == 43) {
+ if (la.kind == 44) {
moduleName = tok;
Get();
Ident(out tok);
}
- if (la.kind == 22) {
+ if (la.kind == 25) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, moduleName);
@@ -971,14 +994,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
- if (la.kind == 30) {
- while (!(la.kind == 0 || la.kind == 30)) {SynErr(132); Get();}
+ if (la.kind == 33) {
+ while (!(la.kind == 0 || la.kind == 33)) {SynErr(132); Get();}
Get();
Expression(out e);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(133); Get();}
Expect(18);
reqs.Add(e);
- } else if (la.kind == 46) {
+ } else if (la.kind == 47) {
Get();
if (StartOf(11)) {
PossiblyWildFrameExpression(out fe);
@@ -991,13 +1014,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
while (!(la.kind == 0 || la.kind == 18)) {SynErr(134); Get();}
Expect(18);
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
Expression(out e);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(135); Get();}
Expect(18);
ens.Add(e);
- } else if (la.kind == 32) {
+ } else if (la.kind == 35) {
Get();
DecreasesList(decreases, false);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(136); Get();}
@@ -1016,7 +1039,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 47) {
+ if (la.kind == 48) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(9)) {
@@ -1027,7 +1050,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 47) {
+ if (la.kind == 48) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(9)) {
@@ -1056,19 +1079,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s = bs;
break;
}
- case 66: {
+ case 67: {
AssertStmt(out s);
break;
}
- case 54: {
+ case 55: {
AssumeStmt(out s);
break;
}
- case 67: {
+ case 68: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
+ case 1: case 2: case 17: case 22: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
UpdateStmt(out s);
break;
}
@@ -1076,23 +1099,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo VarDeclStatement(out s);
break;
}
- case 59: {
+ case 60: {
IfStmt(out s);
break;
}
- case 63: {
+ case 64: {
WhileStmt(out s);
break;
}
- case 65: {
+ case 66: {
MatchStmt(out s);
break;
}
- case 68: {
+ case 69: {
ParallelStmt(out s);
break;
}
- case 49: {
+ case 50: {
Get();
x = t;
Ident(out id);
@@ -1101,14 +1124,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
break;
}
- case 50: {
+ case 51: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
Ident(out id);
label = id.val;
- } else if (la.kind == 18 || la.kind == 50) {
- while (la.kind == 50) {
+ } else if (la.kind == 18 || la.kind == 51) {
+ while (la.kind == 51) {
Get();
breakCount++;
}
@@ -1118,11 +1141,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
}
- case 51: {
+ case 52: {
ReturnStmt(out s);
break;
}
- case 27: {
+ case 30: {
Get();
s = new SkeletonStatement(t);
Expect(18);
@@ -1134,16 +1157,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void AssertStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
- Expression/*!*/ e = null; Attributes attrs = null;
+ Expression e = null; Attributes attrs = null;
- Expect(66);
- x = t; s = null;
+ Expect(67);
+ x = t;
while (IsAttribute()) {
Attribute(ref attrs);
}
if (StartOf(9)) {
Expression(out e);
- } else if (la.kind == 27) {
+ } else if (la.kind == 30) {
Get();
} else SynErr(144);
Expect(18);
@@ -1156,19 +1179,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void AssumeStmt(out Statement/*!*/ s) {
- Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(54);
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
+ Expression e = null; Attributes attrs = null;
+
+ Expect(55);
x = t;
- Expression(out e);
+ while (IsAttribute()) {
+ Attribute(ref attrs);
+ }
+ if (StartOf(9)) {
+ Expression(out e);
+ } else if (la.kind == 30) {
+ Get();
+ } else SynErr(145);
+ if (e == null) {
+ s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
+ } else {
+ s = new AssumeStmt(x, e, attrs);
+ }
+
Expect(18);
- s = new AssumeStmt(x, e);
}
void PrintStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Expect(67);
+ Expect(68);
x = t;
AttributeArg(out arg);
args.Add(arg);
@@ -1199,14 +1236,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(18);
rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 20 || la.kind == 52 || la.kind == 53) {
+ } else if (la.kind == 20 || la.kind == 53 || la.kind == 54) {
lhss.Add(e); lhs0 = e;
while (la.kind == 20) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 52) {
+ if (la.kind == 53) {
Get();
x = t;
Rhs(out r, lhs0);
@@ -1216,20 +1253,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0);
rhss.Add(r);
}
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
Get();
x = t;
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
suchThatAssume = t;
}
Expression(out suchThat);
- } else SynErr(145);
+ } else SynErr(146);
Expect(18);
} else if (la.kind == 5) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(146);
+ } else SynErr(147);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
@@ -1260,8 +1297,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 52 || la.kind == 53) {
- if (la.kind == 52) {
+ if (la.kind == 53 || la.kind == 54) {
+ if (la.kind == 53) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1277,7 +1314,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else {
Get();
assignTok = t;
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
suchThatAssume = t;
}
@@ -1316,25 +1353,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(59);
+ Expect(60);
x = t;
- if (la.kind == 27 || la.kind == 33) {
- if (la.kind == 33) {
+ if (la.kind == 22 || la.kind == 30) {
+ if (la.kind == 22) {
Guard(out guard);
} else {
Get();
guardOmitted = true;
}
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 60) {
+ if (la.kind == 61) {
Get();
- if (la.kind == 59) {
+ if (la.kind == 60) {
IfStmt(out s);
els = s;
} else if (la.kind == 6) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs;
- } else SynErr(147);
+ } else SynErr(148);
}
if (guardOmitted) {
ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
@@ -1345,7 +1382,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 6) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(148);
+ } else SynErr(149);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1361,10 +1398,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(63);
+ Expect(64);
x = t;
- if (la.kind == 27 || la.kind == 33) {
- if (la.kind == 33) {
+ if (la.kind == 22 || la.kind == 30) {
+ if (la.kind == 22) {
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
} else {
@@ -1374,10 +1411,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
if (la.kind == 6) {
BlockStmt(out body, out bodyStart, out bodyEnd);
- } else if (la.kind == 27) {
+ } else if (la.kind == 30) {
Get();
bodyOmitted = true;
- } else SynErr(149);
+ } else SynErr(150);
if (guardOmitted || bodyOmitted) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -1395,18 +1432,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives);
- } else SynErr(150);
+ } else SynErr(151);
}
void MatchStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
- Expect(65);
+ Expect(66);
x = t;
Expression(out e);
Expect(6);
- while (la.kind == 61) {
+ while (la.kind == 62) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1426,9 +1463,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ block;
IToken bodyStart, bodyEnd;
- Expect(68);
+ Expect(69);
x = t;
- Expect(33);
+ Expect(22);
if (la.kind == 1) {
List<BoundVar/*!*/> bvarsX; Attributes attrsX; Expression rangeX;
QuantifierDomain(out bvarsX, out attrsX, out rangeX);
@@ -1438,14 +1475,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
- Expect(34);
- while (la.kind == 29 || la.kind == 31) {
+ Expect(24);
+ while (la.kind == 32 || la.kind == 34) {
isFree = false;
- if (la.kind == 29) {
+ if (la.kind == 32) {
Get();
isFree = true;
}
- Expect(31);
+ Expect(34);
Expression(out e);
Expect(18);
ens.Add(new MaybeFreeExpression(e, isFree));
@@ -1459,7 +1496,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<AssignmentRhs> rhss = null;
AssignmentRhs r;
- Expect(51);
+ Expect(52);
returnTok = t;
if (StartOf(14)) {
Rhs(out r, null);
@@ -1483,27 +1520,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = null; // to please compiler
Attributes attrs = null;
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 33 || la.kind == 43 || la.kind == 56) {
- if (la.kind == 56) {
+ if (la.kind == 22 || la.kind == 44 || la.kind == 57) {
+ if (la.kind == 57) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(57);
+ Expect(58);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
Ident(out x);
- Expect(33);
+ Expect(22);
args = new List<Expression/*!*/>();
if (StartOf(9)) {
Expressions(args);
}
- Expect(34);
+ Expect(24);
initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
} else {
Get();
@@ -1521,7 +1558,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(9)) {
Expressions(args);
}
- Expect(34);
+ Expect(24);
if (x != null) {
initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
}
@@ -1534,18 +1571,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = new TypeRhs(newToken, ty, initCall);
}
- } else if (la.kind == 58) {
+ } else if (la.kind == 59) {
Get();
x = t;
Expression(out e);
r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e));
- } else if (la.kind == 47) {
+ } else if (la.kind == 48) {
Get();
r = new HavocRhs(t);
} else if (StartOf(9)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(151);
+ } else SynErr(152);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -1557,16 +1594,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 43 || la.kind == 56) {
+ while (la.kind == 44 || la.kind == 57) {
Suffix(ref e);
}
} else if (StartOf(15)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 43 || la.kind == 56) {
+ while (la.kind == 44 || la.kind == 57) {
Suffix(ref e);
}
- } else SynErr(152);
+ } else SynErr(153);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1582,15 +1619,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
- Expect(33);
- if (la.kind == 47) {
+ Expect(22);
+ if (la.kind == 48) {
Get();
e = null;
} else if (StartOf(9)) {
Expression(out ee);
e = ee;
- } else SynErr(153);
- Expect(34);
+ } else SynErr(154);
+ Expect(24);
}
void AlternativeBlock(out List<GuardedAlternative> alternatives) {
@@ -1600,11 +1637,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Statement> body;
Expect(6);
- while (la.kind == 61) {
+ while (la.kind == 62) {
Get();
x = t;
Expression(out e);
- Expect(62);
+ Expect(63);
body = new List<Statement>();
while (StartOf(10)) {
Stmt(body);
@@ -1622,22 +1659,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod = null;
while (StartOf(16)) {
- if (la.kind == 29 || la.kind == 64) {
+ if (la.kind == 32 || la.kind == 65) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(155); Get();}
Expect(18);
invariants.Add(invariant);
- } else if (la.kind == 32) {
- while (!(la.kind == 0 || la.kind == 32)) {SynErr(155); Get();}
+ } else if (la.kind == 35) {
+ while (!(la.kind == 0 || la.kind == 35)) {SynErr(156); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(156); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(157); Get();}
Expect(18);
} else {
- while (!(la.kind == 0 || la.kind == 28)) {SynErr(157); Get();}
+ while (!(la.kind == 0 || la.kind == 31)) {SynErr(158); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1652,7 +1689,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 18)) {SynErr(158); Get();}
+ while (!(la.kind == 0 || la.kind == 18)) {SynErr(159); Get();}
Expect(18);
}
}
@@ -1660,12 +1697,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Invariant(out MaybeFreeExpression/*!*/ invariant) {
bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 29 || la.kind == 64)) {SynErr(159); Get();}
- if (la.kind == 29) {
+ while (!(la.kind == 0 || la.kind == 32 || la.kind == 65)) {SynErr(160); Get();}
+ if (la.kind == 32) {
Get();
isFree = true;
}
- Expect(64);
+ Expect(65);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -1680,10 +1717,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(61);
+ Expect(62);
x = t;
Ident(out id);
- if (la.kind == 33) {
+ if (la.kind == 22) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
@@ -1692,9 +1729,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
arguments.Add(bv);
}
- Expect(34);
+ Expect(24);
}
- Expect(62);
+ Expect(63);
while (StartOf(10)) {
Stmt(body);
}
@@ -1709,7 +1746,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(9)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(160);
+ } else SynErr(161);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1737,7 +1774,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 69 || la.kind == 70) {
+ while (la.kind == 70 || la.kind == 71) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1748,7 +1785,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 71 || la.kind == 72) {
+ if (la.kind == 72 || la.kind == 73) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1757,23 +1794,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void EquivOp() {
- if (la.kind == 69) {
+ if (la.kind == 70) {
Get();
- } else if (la.kind == 70) {
+ } else if (la.kind == 71) {
Get();
- } else SynErr(161);
+ } else SynErr(162);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(17)) {
- if (la.kind == 73 || la.kind == 74) {
+ if (la.kind == 74 || la.kind == 75) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 73 || la.kind == 74) {
+ while (la.kind == 74 || la.kind == 75) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1784,7 +1821,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 75 || la.kind == 76) {
+ while (la.kind == 76 || la.kind == 77) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1795,11 +1832,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void ImpliesOp() {
- if (la.kind == 71) {
+ if (la.kind == 72) {
Get();
- } else if (la.kind == 72) {
+ } else if (la.kind == 73) {
Get();
- } else SynErr(162);
+ } else SynErr(163);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1893,19 +1930,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void AndOp() {
- if (la.kind == 73) {
+ if (la.kind == 74) {
Get();
- } else if (la.kind == 74) {
+ } else if (la.kind == 75) {
Get();
- } else SynErr(163);
+ } else SynErr(164);
}
void OrOp() {
- if (la.kind == 75) {
+ if (la.kind == 76) {
Get();
- } else if (la.kind == 76) {
+ } else if (la.kind == 77) {
Get();
- } else SynErr(164);
+ } else SynErr(165);
}
void Term(out Expression/*!*/ e0) {
@@ -1924,17 +1961,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken y;
switch (la.kind) {
- case 77: {
+ case 23: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
}
- case 22: {
+ case 25: {
Get();
x = t; op = BinaryExpr.Opcode.Lt;
break;
}
- case 23: {
+ case 26: {
Get();
x = t; op = BinaryExpr.Opcode.Gt;
break;
@@ -1997,14 +2034,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(165); break;
+ default: SynErr(166); break;
}
}
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 47 || la.kind == 89 || la.kind == 90) {
+ while (la.kind == 48 || la.kind == 89 || la.kind == 90) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2019,7 +2056,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 88) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(166);
+ } else SynErr(167);
}
void UnaryExpression(out Expression/*!*/ e) {
@@ -2039,43 +2076,43 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 19: case 38: case 54: case 59: case 65: case 66: case 101: case 102: case 103: case 104: {
+ case 19: case 39: case 55: case 60: case 66: case 67: case 101: case 102: case 103: case 104: {
EndlessExpression(out e);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 43 || la.kind == 56) {
+ while (la.kind == 44 || la.kind == 57) {
Suffix(ref e);
}
break;
}
- case 6: case 56: {
+ case 6: case 57: {
DisplayExpr(out e);
break;
}
- case 39: {
+ case 40: {
MultiSetExpr(out e);
break;
}
- case 41: {
+ case 42: {
MapExpr(out e);
break;
}
- case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
+ case 2: case 17: case 22: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
ConstAtomExpression(out e);
- while (la.kind == 43 || la.kind == 56) {
+ while (la.kind == 44 || la.kind == 57) {
Suffix(ref e);
}
break;
}
- default: SynErr(167); break;
+ default: SynErr(168); break;
}
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 47) {
+ if (la.kind == 48) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
} else if (la.kind == 89) {
@@ -2084,7 +2121,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 90) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(168);
+ } else SynErr(169);
}
void NegOp() {
@@ -2092,7 +2129,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 91) {
Get();
- } else SynErr(169);
+ } else SynErr(170);
}
void EndlessExpression(out Expression e) {
@@ -2103,18 +2140,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<BoundVar> letVars; List<Expression> letRHSs;
switch (la.kind) {
- case 59: {
+ case 60: {
Get();
x = t;
Expression(out e);
Expect(99);
Expression(out e0);
- Expect(60);
+ Expect(61);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
break;
}
- case 65: {
+ case 66: {
MatchExpression(out e);
break;
}
@@ -2122,11 +2159,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo QuantifierGuts(out e);
break;
}
- case 38: {
+ case 39: {
ComprehensionExpr(out e);
break;
}
- case 66: {
+ case 67: {
Get();
x = t;
Expression(out e0);
@@ -2135,7 +2172,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new AssertExpr(x, e0, e1);
break;
}
- case 54: {
+ case 55: {
Get();
x = t;
Expression(out e0);
@@ -2156,7 +2193,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out d);
letVars.Add(d);
}
- Expect(52);
+ Expect(53);
Expression(out e);
letRHSs.Add(e);
while (la.kind == 20) {
@@ -2169,7 +2206,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LetExpr(x, letVars, letRHSs, e);
break;
}
- default: SynErr(170); break;
+ default: SynErr(171); break;
}
}
@@ -2180,18 +2217,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out id);
idents.Add(id);
- while (la.kind == 43) {
+ while (la.kind == 44) {
Get();
Ident(out id);
idents.Add(id);
}
- if (la.kind == 33) {
+ if (la.kind == 22) {
Get();
openParen = t; args = new List<Expression>();
if (StartOf(9)) {
Expressions(args);
}
- Expect(34);
+ Expect(24);
}
e = new IdentifierSequence(idents, openParen, args);
}
@@ -2202,20 +2239,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
Ident(out id);
- if (la.kind == 33) {
+ if (la.kind == 22) {
Get();
IToken openParen = t; args = new List<Expression/*!*/>(); func = true;
if (StartOf(9)) {
Expressions(args);
}
- Expect(34);
+ Expect(24);
e = new FunctionCallExpr(id, id.val, e, openParen, args);
}
if (!func) { e = new ExprDotName(id, e, id.val); }
- } else if (la.kind == 56) {
+ } else if (la.kind == 57) {
Get();
x = t;
if (StartOf(9)) {
@@ -2228,11 +2265,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 52) {
+ } else if (la.kind == 53) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 20 || la.kind == 57) {
+ } else if (la.kind == 20 || la.kind == 58) {
while (la.kind == 20) {
Get();
Expression(out ee);
@@ -2243,7 +2280,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(171);
+ } else SynErr(172);
} else if (la.kind == 100) {
Get();
anyDots = true;
@@ -2251,7 +2288,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee);
e1 = ee;
}
- } else SynErr(172);
+ } else SynErr(173);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2274,8 +2311,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- Expect(57);
- } else SynErr(173);
+ Expect(58);
+ } else SynErr(174);
}
void DisplayExpr(out Expression e) {
@@ -2291,15 +2328,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new SetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 56) {
+ } else if (la.kind == 57) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(9)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(57);
- } else SynErr(174);
+ Expect(58);
+ } else SynErr(175);
}
void MultiSetExpr(out Expression e) {
@@ -2307,7 +2344,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(39);
+ Expect(40);
x = t;
if (la.kind == 6) {
Get();
@@ -2317,15 +2354,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new MultiSetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 33) {
+ } else if (la.kind == 22) {
Get();
x = t; elements = new List<Expression/*!*/>();
Expression(out e);
e = new MultiSetFormingExpr(x, e);
- Expect(34);
+ Expect(24);
} else if (StartOf(19)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(175);
+ } else SynErr(176);
}
void MapExpr(out Expression e) {
@@ -2334,16 +2371,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<ExpressionPair/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(41);
+ Expect(42);
x = t;
- if (la.kind == 56) {
+ if (la.kind == 57) {
Get();
elements = new List<ExpressionPair/*!*/>();
if (StartOf(9)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(x, elements);
- Expect(57);
+ Expect(58);
} else if (la.kind == 1) {
BoundVar/*!*/ bv;
List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
@@ -2359,7 +2396,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new MapComprehension(x, bvars, range, body);
} else if (StartOf(19)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(176);
+ } else SynErr(177);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2396,27 +2433,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo case 96: {
Get();
x = t;
- Expect(33);
+ Expect(22);
Expression(out e);
- Expect(34);
+ Expect(24);
e = new FreshExpr(x, e);
break;
}
case 97: {
Get();
x = t;
- Expect(33);
+ Expect(22);
Expression(out e);
- Expect(34);
+ Expect(24);
e = new AllocatedExpr(x, e);
break;
}
case 98: {
Get();
x = t;
- Expect(33);
+ Expect(22);
Expression(out e);
- Expect(34);
+ Expect(24);
e = new OldExpr(x, e);
break;
}
@@ -2428,15 +2465,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(17);
break;
}
- case 33: {
+ case 22: {
Get();
x = t;
Expression(out e);
e = new ParensExpression(x, e);
- Expect(34);
+ Expect(24);
break;
}
- default: SynErr(177); break;
+ default: SynErr(178); break;
}
}
@@ -2455,13 +2492,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d);
- Expect(52);
+ Expect(53);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
while (la.kind == 20) {
Get();
Expression(out d);
- Expect(52);
+ Expect(53);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
}
@@ -2472,17 +2509,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 106) {
Get();
- } else SynErr(178);
+ } else SynErr(179);
}
void MatchExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(65);
+ Expect(66);
x = t;
Expression(out e);
- while (la.kind == 61) {
+ while (la.kind == 62) {
CaseExpression(out c);
cases.Add(c);
}
@@ -2503,7 +2540,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 103 || la.kind == 104) {
Exists();
x = t;
- } else SynErr(179);
+ } else SynErr(180);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
@@ -2523,7 +2560,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ range;
Expression body = null;
- Expect(38);
+ Expect(39);
x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -2549,10 +2586,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(61);
+ Expect(62);
x = t;
Ident(out id);
- if (la.kind == 33) {
+ if (la.kind == 22) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
@@ -2561,9 +2598,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
arguments.Add(bv);
}
- Expect(34);
+ Expect(24);
}
- Expect(62);
+ Expect(63);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
@@ -2573,7 +2610,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 102) {
Get();
- } else SynErr(180);
+ } else SynErr(181);
}
void Exists() {
@@ -2581,7 +2618,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 104) {
Get();
- } else SynErr(181);
+ } else SynErr(182);
}
void AttributeBody(ref Attributes attrs) {
@@ -2617,27 +2654,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, T,T,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
- {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
- {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
- {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
- {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
+ {T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, x,T,x,T, T,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
+ {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
};
} // end Parser
@@ -2684,62 +2721,62 @@ public class Errors { case 19: s = "\"var\" expected"; break;
case 20: s = "\",\" expected"; break;
case 21: s = "\"type\" expected"; break;
- case 22: s = "\"<\" expected"; break;
- case 23: s = "\">\" expected"; break;
- case 24: s = "\"method\" expected"; break;
- case 25: s = "\"constructor\" expected"; break;
- case 26: s = "\"returns\" expected"; break;
- case 27: s = "\"...\" expected"; break;
- case 28: s = "\"modifies\" expected"; break;
- case 29: s = "\"free\" expected"; break;
- case 30: s = "\"requires\" expected"; break;
- case 31: s = "\"ensures\" expected"; break;
- case 32: s = "\"decreases\" expected"; break;
- case 33: s = "\"(\" expected"; break;
- case 34: s = "\")\" expected"; break;
- case 35: s = "\"bool\" expected"; break;
- case 36: s = "\"nat\" expected"; break;
- case 37: s = "\"int\" expected"; break;
- case 38: s = "\"set\" expected"; break;
- case 39: s = "\"multiset\" expected"; break;
- case 40: s = "\"seq\" expected"; break;
- case 41: s = "\"map\" expected"; break;
- case 42: s = "\"object\" expected"; break;
- case 43: s = "\".\" expected"; break;
- case 44: s = "\"function\" expected"; break;
- case 45: s = "\"predicate\" expected"; break;
- case 46: s = "\"reads\" expected"; break;
- case 47: s = "\"*\" expected"; break;
- case 48: s = "\"`\" expected"; break;
- case 49: s = "\"label\" expected"; break;
- case 50: s = "\"break\" expected"; break;
- case 51: s = "\"return\" expected"; break;
- case 52: s = "\":=\" expected"; break;
- case 53: s = "\":|\" expected"; break;
- case 54: s = "\"assume\" expected"; break;
- case 55: s = "\"new\" expected"; break;
- case 56: s = "\"[\" expected"; break;
- case 57: s = "\"]\" expected"; break;
- case 58: s = "\"choose\" expected"; break;
- case 59: s = "\"if\" expected"; break;
- case 60: s = "\"else\" expected"; break;
- case 61: s = "\"case\" expected"; break;
- case 62: s = "\"=>\" expected"; break;
- case 63: s = "\"while\" expected"; break;
- case 64: s = "\"invariant\" expected"; break;
- case 65: s = "\"match\" expected"; break;
- case 66: s = "\"assert\" expected"; break;
- case 67: s = "\"print\" expected"; break;
- case 68: s = "\"parallel\" expected"; break;
- case 69: s = "\"<==>\" expected"; break;
- case 70: s = "\"\\u21d4\" expected"; break;
- case 71: s = "\"==>\" expected"; break;
- case 72: s = "\"\\u21d2\" expected"; break;
- case 73: s = "\"&&\" expected"; break;
- case 74: s = "\"\\u2227\" expected"; break;
- case 75: s = "\"||\" expected"; break;
- case 76: s = "\"\\u2228\" expected"; break;
- case 77: s = "\"==\" expected"; break;
+ case 22: s = "\"(\" expected"; break;
+ case 23: s = "\"==\" expected"; break;
+ case 24: s = "\")\" expected"; break;
+ case 25: s = "\"<\" expected"; break;
+ case 26: s = "\">\" expected"; break;
+ case 27: s = "\"method\" expected"; break;
+ case 28: s = "\"constructor\" expected"; break;
+ case 29: s = "\"returns\" expected"; break;
+ case 30: s = "\"...\" expected"; break;
+ case 31: s = "\"modifies\" expected"; break;
+ case 32: s = "\"free\" expected"; break;
+ case 33: s = "\"requires\" expected"; break;
+ case 34: s = "\"ensures\" expected"; break;
+ case 35: s = "\"decreases\" expected"; break;
+ case 36: s = "\"bool\" expected"; break;
+ case 37: s = "\"nat\" expected"; break;
+ case 38: s = "\"int\" expected"; break;
+ case 39: s = "\"set\" expected"; break;
+ case 40: s = "\"multiset\" expected"; break;
+ case 41: s = "\"seq\" expected"; break;
+ case 42: s = "\"map\" expected"; break;
+ case 43: s = "\"object\" expected"; break;
+ case 44: s = "\".\" expected"; break;
+ case 45: s = "\"function\" expected"; break;
+ case 46: s = "\"predicate\" expected"; break;
+ case 47: s = "\"reads\" expected"; break;
+ case 48: s = "\"*\" expected"; break;
+ case 49: s = "\"`\" expected"; break;
+ case 50: s = "\"label\" expected"; break;
+ case 51: s = "\"break\" expected"; break;
+ case 52: s = "\"return\" expected"; break;
+ case 53: s = "\":=\" expected"; break;
+ case 54: s = "\":|\" expected"; break;
+ case 55: s = "\"assume\" expected"; break;
+ case 56: s = "\"new\" expected"; break;
+ case 57: s = "\"[\" expected"; break;
+ case 58: s = "\"]\" expected"; break;
+ case 59: s = "\"choose\" expected"; break;
+ case 60: s = "\"if\" expected"; break;
+ case 61: s = "\"else\" expected"; break;
+ case 62: s = "\"case\" expected"; break;
+ case 63: s = "\"=>\" expected"; break;
+ case 64: s = "\"while\" expected"; break;
+ case 65: s = "\"invariant\" expected"; break;
+ case 66: s = "\"match\" expected"; break;
+ case 67: s = "\"assert\" expected"; break;
+ case 68: s = "\"print\" expected"; break;
+ case 69: s = "\"parallel\" expected"; break;
+ case 70: s = "\"<==>\" expected"; break;
+ case 71: s = "\"\\u21d4\" expected"; break;
+ case 72: s = "\"==>\" expected"; break;
+ case 73: s = "\"\\u21d2\" expected"; break;
+ case 74: s = "\"&&\" expected"; break;
+ case 75: s = "\"\\u2227\" expected"; break;
+ case 76: s = "\"||\" expected"; break;
+ case 77: s = "\"\\u2228\" expected"; break;
case 78: s = "\"<=\" expected"; break;
case 79: s = "\">=\" expected"; break;
case 80: s = "\"!=\" expected"; break;
@@ -2807,43 +2844,44 @@ public class Errors { case 142: s = "this symbol not expected in OneStmt"; break;
case 143: s = "invalid OneStmt"; break;
case 144: s = "invalid AssertStmt"; break;
- case 145: s = "invalid UpdateStmt"; break;
+ case 145: s = "invalid AssumeStmt"; break;
case 146: s = "invalid UpdateStmt"; break;
- case 147: s = "invalid IfStmt"; break;
+ case 147: s = "invalid UpdateStmt"; break;
case 148: s = "invalid IfStmt"; break;
- case 149: s = "invalid WhileStmt"; break;
+ case 149: s = "invalid IfStmt"; break;
case 150: s = "invalid WhileStmt"; break;
- case 151: s = "invalid Rhs"; break;
- case 152: s = "invalid Lhs"; break;
- case 153: s = "invalid Guard"; break;
- case 154: s = "this symbol not expected in LoopSpec"; break;
+ case 151: s = "invalid WhileStmt"; break;
+ case 152: s = "invalid Rhs"; break;
+ case 153: s = "invalid Lhs"; break;
+ case 154: s = "invalid Guard"; break;
case 155: s = "this symbol not expected in LoopSpec"; break;
case 156: s = "this symbol not expected in LoopSpec"; break;
case 157: s = "this symbol not expected in LoopSpec"; break;
case 158: s = "this symbol not expected in LoopSpec"; break;
- case 159: s = "this symbol not expected in Invariant"; break;
- case 160: s = "invalid AttributeArg"; break;
- case 161: s = "invalid EquivOp"; break;
- case 162: s = "invalid ImpliesOp"; break;
- case 163: s = "invalid AndOp"; break;
- case 164: s = "invalid OrOp"; break;
- case 165: s = "invalid RelOp"; break;
- case 166: s = "invalid AddOp"; break;
- case 167: s = "invalid UnaryExpression"; break;
- case 168: s = "invalid MulOp"; break;
- case 169: s = "invalid NegOp"; break;
- case 170: s = "invalid EndlessExpression"; break;
- case 171: s = "invalid Suffix"; break;
+ case 159: s = "this symbol not expected in LoopSpec"; break;
+ case 160: s = "this symbol not expected in Invariant"; break;
+ case 161: s = "invalid AttributeArg"; break;
+ case 162: s = "invalid EquivOp"; break;
+ case 163: s = "invalid ImpliesOp"; break;
+ case 164: s = "invalid AndOp"; break;
+ case 165: s = "invalid OrOp"; break;
+ case 166: s = "invalid RelOp"; break;
+ case 167: s = "invalid AddOp"; break;
+ case 168: s = "invalid UnaryExpression"; break;
+ case 169: s = "invalid MulOp"; break;
+ case 170: s = "invalid NegOp"; break;
+ case 171: s = "invalid EndlessExpression"; break;
case 172: s = "invalid Suffix"; break;
case 173: s = "invalid Suffix"; break;
- case 174: s = "invalid DisplayExpr"; break;
- case 175: s = "invalid MultiSetExpr"; break;
- case 176: s = "invalid MapExpr"; break;
- case 177: s = "invalid ConstAtomExpression"; break;
- case 178: s = "invalid QSep"; break;
- case 179: s = "invalid QuantifierGuts"; break;
- case 180: s = "invalid Forall"; break;
- case 181: s = "invalid Exists"; break;
+ case 174: s = "invalid Suffix"; break;
+ case 175: s = "invalid DisplayExpr"; break;
+ case 176: s = "invalid MultiSetExpr"; break;
+ case 177: s = "invalid MapExpr"; break;
+ case 178: s = "invalid ConstAtomExpression"; break;
+ case 179: s = "invalid QSep"; break;
+ case 180: s = "invalid QuantifierGuts"; break;
+ case 181: s = "invalid Forall"; break;
+ case 182: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index fb46ba4b..3654c672 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -71,6 +71,9 @@ namespace Microsoft.Dafny { if (i++ != 0) { wr.WriteLine(); }
Indent(indent);
PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());
+ if (at.EqualitySupport == TypeParameter.EqualitySupportValue.Required) {
+ wr.Write("(==)");
+ }
wr.WriteLine(";");
} else if (d is DatatypeDecl) {
if (i++ != 0) { wr.WriteLine(); }
@@ -149,6 +152,9 @@ namespace Microsoft.Dafny { foreach (TypeParameter tp in typeArgs) {
Contract.Assert(tp != null);
wr.Write("{0}{1}", sep, tp.Name);
+ if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Required) {
+ wr.Write("(==)");
+ }
sep = ", ";
}
wr.Write(">");
@@ -427,24 +433,14 @@ namespace Microsoft.Dafny { }
}
- if (stmt is AssertStmt) {
- Expression expr = ((AssertStmt)stmt).Expr;
-
- wr.Write("assert");
-
- if (stmt.HasAttributes())
- {
+ if (stmt is PredicateStmt) {
+ Expression expr = ((PredicateStmt)stmt).Expr;
+ wr.Write(stmt is AssertStmt ? "assert" : "assume");
+ if (stmt.HasAttributes()) {
PrintAttributes(stmt.Attributes);
}
-
wr.Write(" ");
PrintExpression(expr);
-
- wr.Write(";");
-
- } else if (stmt is AssumeStmt) {
- wr.Write("assume ");
- PrintExpression(((AssumeStmt)stmt).Expr);
wr.Write(";");
} else if (stmt is PrintStmt) {
@@ -629,6 +625,9 @@ namespace Microsoft.Dafny { } else if (s.S is AssertStmt) {
Contract.Assert(s.ConditionOmitted);
wr.Write("assert ...;");
+ } else if (s.S is AssumeStmt) {
+ Contract.Assert(s.ConditionOmitted);
+ wr.Write("assume ...;");
} else if (s.S is IfStmt) {
PrintIfStatement(indent, (IfStmt)s.S, s.ConditionOmitted);
} else if (s.S is WhileStmt) {
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 56006a7f..bbc12d6a 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -50,7 +50,7 @@ namespace Microsoft.Dafny { }
}
- public class RefinementTransformer
+ public class RefinementTransformer : IRewriter
{
ResolutionErrorReporter reporter;
public RefinementTransformer(ResolutionErrorReporter reporter) {
@@ -59,12 +59,17 @@ namespace Microsoft.Dafny { }
private ModuleDecl moduleUnderConstruction; // non-null for the duration of Construct calls
+ private Queue<Action> postTasks = new Queue<Action>(); // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction
- public void Construct(ModuleDecl m) {
- Contract.Requires(m != null);
- Contract.Requires(m.RefinementBase != null);
+ public void PreResolve(ModuleDecl m) {
+ if (m.RefinementBase == null) {
+ // This Rewriter doesn't do anything
+ return;
+ }
- Contract.Assert(moduleUnderConstruction == null);
+ if (moduleUnderConstruction != null) {
+ postTasks.Clear();
+ }
moduleUnderConstruction = m;
var prev = m.RefinementBase;
@@ -99,7 +104,35 @@ namespace Microsoft.Dafny { } else {
var nw = m.TopLevelDecls[index];
if (d is ArbitraryTypeDecl) {
- // this is allowed to be refined by any type declaration, so just keep the new one
+ bool dDemandsEqualitySupport = ((ArbitraryTypeDecl)d).MustSupportEquality;
+ if (nw is ArbitraryTypeDecl) {
+ if (dDemandsEqualitySupport != ((ArbitraryTypeDecl)nw).MustSupportEquality) {
+ reporter.Error(nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);
+ }
+ } else if (dDemandsEqualitySupport) {
+ if (nw is ClassDecl) {
+ // fine, as long as "nw" does not take any type parameters
+ if (nw.TypeArgs.Count != 0) {
+ reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a class that takes type parameters", nw.Name);
+ }
+ } else if (nw is CoDatatypeDecl) {
+ reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");
+ } else {
+ Contract.Assert(nw is IndDatatypeDecl);
+ if (nw.TypeArgs.Count != 0) {
+ reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a datatype that takes type parameters", nw.Name);
+ } else {
+ // Here, we need to figure out if the new type supports equality. But we won't know about that until resolution has
+ // taken place, so we defer it until the PostResolve phase.
+ var udt = new UserDefinedType(nw.tok, nw.Name, nw, new List<Type>());
+ postTasks.Enqueue(delegate() {
+ if (!udt.SupportsEquality) {
+ reporter.Error(udt.tok, "datatype '{0}' is used to refine an arbitrary type with equality support, but '{0}' does not support equality", udt.Name);
+ }
+ });
+ }
+ }
+ }
} else if (nw is ArbitraryTypeDecl) {
reporter.Error(nw, "an arbitrary type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);
} else if (nw is DatatypeDecl) {
@@ -115,7 +148,18 @@ namespace Microsoft.Dafny { }
}
- Contract.Assert(moduleUnderConstruction == m);
+ Contract.Assert(moduleUnderConstruction == m); // this should be as it was set earlier in this method
+ }
+
+ public void PostResolve(ModuleDecl m) {
+ if (m == moduleUnderConstruction) {
+ while (this.postTasks.Count != 0) {
+ var a = postTasks.Dequeue();
+ a();
+ }
+ } else {
+ postTasks.Clear();
+ }
moduleUnderConstruction = null;
}
@@ -135,7 +179,7 @@ namespace Microsoft.Dafny { if (d is ArbitraryTypeDecl) {
var dd = (ArbitraryTypeDecl)d;
- return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, null);
+ return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, null);
} else if (d is IndDatatypeDecl) {
var dd = (IndDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
@@ -165,7 +209,7 @@ namespace Microsoft.Dafny { }
TypeParameter CloneTypeParam(TypeParameter tp) {
- return new TypeParameter(Tok(tp.tok), tp.Name);
+ return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport);
}
MemberDecl CloneMember(MemberDecl member) {
@@ -429,11 +473,11 @@ namespace Microsoft.Dafny { Statement r;
if (stmt is AssertStmt) {
var s = (AssertStmt)stmt;
- r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr));
+ r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr), null);
} else if (stmt is AssumeStmt) {
var s = (AssumeStmt)stmt;
- r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr));
+ r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr), null);
} else if (stmt is PrintStmt) {
var s = (PrintStmt)stmt;
@@ -598,6 +642,8 @@ namespace Microsoft.Dafny { // -------------------------------------------------- Merging ---------------------------------------------------------------
ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {
+ CheckAgreement_TypeParameters(nw.tok, prev.TypeArgs, nw.TypeArgs, nw.Name, "class");
+
// Create a simple name-to-member dictionary. Ignore any duplicates at this time.
var declaredNames = new Dictionary<string, int>();
for (int i = 0; i < nw.Members.Count; i++) {
@@ -731,6 +777,27 @@ namespace Microsoft.Dafny { var n = nw[i];
if (o.Name != n.Name) {
reporter.Error(n.tok, "type parameters are not allowed to be renamed from the names given in the {0} in the module being refined (expected '{1}', found '{2}')", thing, o.Name, n.Name);
+ } else {
+ // This explains what we want to do and why:
+ // switch (o.EqualitySupport) {
+ // case TypeParameter.EqualitySupportValue.Required:
+ // // here, we will insist that the new type-parameter also explicitly requires equality support (because we don't want
+ // // to wait for the inference to run on the new module)
+ // good = n.EqualitySupport == TypeParameter.EqualitySupportValue.Required;
+ // break;
+ // case TypeParameter.EqualitySupportValue.InferredRequired:
+ // // here, we can allow anything, because even with an Unspecified value, the inference will come up with InferredRequired, like before
+ // good = true;
+ // break;
+ // case TypeParameter.EqualitySupportValue.Unspecified:
+ // // inference didn't come up with anything on the previous module, so the only value we'll allow here is Unspecified as well
+ // good = n.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified;
+ // break;
+ // }
+ // Here's how we actually compute it:
+ if (o.EqualitySupport != TypeParameter.EqualitySupportValue.InferredRequired && o.EqualitySupport != n.EqualitySupport) {
+ reporter.Error(n.tok, "type parameter '{0}' is not allowed to change the requirement of supporting equality", n.Name);
+ }
}
}
}
@@ -794,6 +861,8 @@ namespace Microsoft.Dafny { * assert ...; assert E; assert E;
* assert E; assert E;
*
+ * assume ...; assume E; assume E;
+ *
* var x := E; var x; var x := E;
* var x := E; var x := *; var x := E;
* var x := E1; var x :| E0; var x := E1; assert E0;
@@ -855,6 +924,19 @@ namespace Microsoft.Dafny { i++; j++;
}
+ } else if (S is AssumeStmt) {
+ var skel = (AssumeStmt)S;
+ Contract.Assert(((SkeletonStatement)cur).ConditionOmitted);
+ var oldAssume = oldS as AssumeStmt;
+ if (oldAssume == null) {
+ reporter.Error(cur.Tok, "assume template does not match inherited statement");
+ i++;
+ } else {
+ var e = CloneExpr(oldAssume.Expr);
+ body.Add(new AssumeStmt(skel.Tok, e, null));
+ i++; j++;
+ }
+
} else if (S is IfStmt) {
var skel = (IfStmt)S;
Contract.Assert(((SkeletonStatement)cur).ConditionOmitted);
@@ -928,7 +1010,7 @@ namespace Microsoft.Dafny { body.Add(cNew);
i++; j++;
if (addedAssert != null) {
- body.Add(new AssertStmt(addedAssert.tok, addedAssert));
+ body.Add(new AssertStmt(addedAssert.tok, addedAssert, null));
}
} else {
MergeAddStatement(cur, body);
@@ -1006,6 +1088,8 @@ namespace Microsoft.Dafny { var S = ((SkeletonStatement)nxt).S;
if (S is AssertStmt) {
return other is PredicateStmt;
+ } else if (S is AssumeStmt) {
+ return other is AssumeStmt;
} else if (S is IfStmt) {
return other is IfStmt;
} else if (S is WhileStmt) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f0990aa0..3d99f732 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -170,15 +170,17 @@ namespace Microsoft.Dafny { }
// register top-level declarations
- Rewriter rewriter = new AutoContractsRewriter();
+ var rewriters = new List<IRewriter>();
+ // 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) {
- rewriter.PreResolve(m);
- if (m.RefinementBase != null) {
- var transformer = new RefinementTransformer(this);
- transformer.Construct(m);
- }
+ rewriters.Iter(r => r.PreResolve(m));
+
moduleNameInfo[m.Height] = RegisterTopLevelDecls(m.TopLevelDecls);
// set up environment
@@ -187,13 +189,16 @@ namespace Microsoft.Dafny { allDatatypeCtors = info.Ctors;
// resolve
var datatypeDependencies = new Graph<IndDatatypeDecl>();
+ int prevErrorCount = ErrorCount;
ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);
- ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
+ if (prevErrorCount == ErrorCount) {
+ ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
+ }
// tear down
classes = null;
allDatatypeCtors = null;
- // give rewriter a chance to do processing
- rewriter.PostResolve(m);
+ // give rewriters a chance to do processing
+ rewriters.Iter(r => r.PostResolve(m));
}
// compute IsRecursive bit for mutually recursive functions
@@ -394,15 +399,16 @@ namespace Microsoft.Dafny { allTypeParameters.PopMarker();
}
- // Perform the stratosphere check on inductive datatypes
+ // 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);
}
}
- // Perform the guardedness check on co-datatypes
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) {
@@ -426,7 +432,396 @@ namespace Microsoft.Dafny { }
}
}
+ // 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:
+ // First, check a special case: a datatype value (like Nil) that takes no parameters
+ var e0 = e.E0.Resolved as DatatypeValue;
+ var e1 = e.E1.Resolved as DatatypeValue;
+ if (e0 != null && e0.Arguments.Count == 0) {
+ // that's cool
+ } else if (e1 != null && e1.Arguments.Count == 0) {
+ // oh yeah!
+ } else if (!t0.SupportsEquality) {
+ Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
+ } else if (!t1.SupportsEquality) {
+ Error(e.E1, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));
+ }
+ break;
+ default:
+ switch (e.ResolvedOp) {
+ // Note, all operations on sets, multisets, and maps are guaranteed to work because of restrictions placed on how
+ // these types are instantiated. (Except: This guarantee does not apply to equality on maps, because the Range type
+ // of maps is not restricted, only the Domain type. However, the equality operator is checked above.)
+ case BinaryExpr.ResolvedOpcode.InSeq:
+ case BinaryExpr.ResolvedOpcode.NotInSeq:
+ case BinaryExpr.ResolvedOpcode.Prefix:
+ case BinaryExpr.ResolvedOpcode.ProperPrefix:
+ if (!t1.SupportsEquality) {
+ Error(e.E1, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));
+ } else if (!t0.SupportsEquality) {
+ if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet || e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSeq) {
+ Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
+ } else {
+ Error(e.E0, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
+ }
+ }
+ break;
+ default:
+ break;
+ }
+ break;
+ }
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ foreach (var bv in e.BoundVars) {
+ CheckEqualityTypes_Type(bv.tok, bv.Type);
+ }
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ foreach (var bv in e.Vars) {
+ CheckEqualityTypes_Type(bv.tok, bv.Type);
+ }
+ } else if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ Contract.Assert(e.Function.TypeArgs.Count <= e.TypeArgumentSubstitutions.Count);
+ var i = 0;
+ foreach (var formalTypeArg in e.Function.TypeArgs) {
+ var actualTypeArg = e.TypeArgumentSubstitutions[formalTypeArg];
+ if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {
+ Error(e.tok, "type parameter {0} ({1}) passed to function {2} must support equality (got {3}){4}", i, formalTypeArg.Name, e.Function.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));
+ }
+ i++;
+ }
+ }
+
+ foreach (var ee in expr.SubExpressions) {
+ CheckEqualityTypes(ee);
+ }
+ }
+
+ void CheckEqualityTypes_Type(IToken tok, Type type) {
+ Contract.Requires(tok != null);
+ Contract.Requires(type != null);
+ type = type.Normalize();
+ if (type is BasicType) {
+ // fine
+ } else if (type is SetType) {
+ var argType = ((SetType)type).Arg;
+ if (!argType.SupportsEquality) {
+ Error(tok, "set argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));
+ }
+ CheckEqualityTypes_Type(tok, argType);
+
+ } else if (type is MultiSetType) {
+ var argType = ((MultiSetType)type).Arg;
+ if (!argType.SupportsEquality) {
+ Error(tok, "multiset argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));
+ }
+ CheckEqualityTypes_Type(tok, argType);
+
+ } else if (type is MapType) {
+ var mt = (MapType)type;
+ if (!mt.Domain.SupportsEquality) {
+ Error(tok, "map domain type must support equality (got {0}){1}", mt.Domain, TypeEqualityErrorMessageHint(mt.Domain));
+ }
+ CheckEqualityTypes_Type(tok, mt.Domain);
+ CheckEqualityTypes_Type(tok, mt.Range);
+
+ } else if (type is SeqType) {
+ Type argType = ((SeqType)type).Arg;
+ CheckEqualityTypes_Type(tok, argType);
+
+ } else if (type is UserDefinedType) {
+ var udt = (UserDefinedType)type;
+ if (udt.ResolvedClass != null) {
+ Contract.Assert(udt.ResolvedClass.TypeArgs.Count == udt.TypeArgs.Count);
+ var i = 0;
+ foreach (var argType in udt.TypeArgs) {
+ var formalTypeArg = udt.ResolvedClass.TypeArgs[i];
+ if (formalTypeArg.MustSupportEquality && !argType.SupportsEquality) {
+ Error(tok, "type parameter {0} ({1}) passed to type {2} must support equality (got {3}){4}", i, formalTypeArg.Name, udt.ResolvedClass.Name, argType, TypeEqualityErrorMessageHint(argType));
+ }
+ CheckEqualityTypes_Type(tok, argType);
+ i++;
+ }
+ } else {
+ Contract.Assert(udt.TypeArgs.Count == 0); // TypeParameters have no type arguments
+ }
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
+ }
+ }
+
+ 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;
@@ -655,6 +1050,99 @@ namespace Microsoft.Dafny { return true;
}
+ void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies) {
+ Contract.Requires(startingPoint != null);
+ Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));
+
+ var scc = dependencies.GetSCC(startingPoint);
+ // First, the simple case: If any parameter of any inductive datatype in the SCC is of a codatatype type, then
+ // the whole SCC is incapable of providing the equality operation.
+ foreach (var dt in scc) {
+ Contract.Assume(dt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed);
+ foreach (var ctor in dt.Ctors) {
+ foreach (var arg in ctor.Formals) {
+ var anotherIndDt = arg.Type.AsIndDatatype;
+ if ((anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || arg.Type.IsCoDatatype) {
+ // arg.Type is known never to support equality
+ // So, go around the entire SCC and record what we learnt
+ foreach (var ddtt in scc) {
+ ddtt.EqualitySupport = IndDatatypeDecl.ES.Never;
+ }
+ return; // we are done
+ }
+ }
+ }
+ }
+
+ // Now for the more involved case: we need to determine which type parameters determine equality support for each datatype in the SCC
+ // We start by seeing where each datatype's type parameters are used in a place known to determine equality support.
+ bool thingsChanged = false;
+ foreach (var dt in scc) {
+ if (dt.TypeArgs.Count == 0) {
+ // if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors
+ continue;
+ }
+ foreach (var ctor in dt.Ctors) {
+ foreach (var arg in ctor.Formals) {
+ var typeArg = arg.Type.AsTypeParameter;
+ if (typeArg != null) {
+ typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
+ thingsChanged = true;
+ } else {
+ var otherDt = arg.Type.AsIndDatatype;
+ if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) { // datatype is in a different SCC
+ var otherUdt = (UserDefinedType)arg.Type.Normalize();
+ var i = 0;
+ foreach (var otherTp in otherDt.TypeArgs) {
+ if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
+ var tp = otherUdt.TypeArgs[i].AsTypeParameter;
+ if (tp != null) {
+ tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
+ thingsChanged = true;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ // Then we propagate this information up through the SCC
+ while (thingsChanged) {
+ thingsChanged = false;
+ foreach (var dt in scc) {
+ if (dt.TypeArgs.Count == 0) {
+ // if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors
+ continue;
+ }
+ foreach (var ctor in dt.Ctors) {
+ foreach (var arg in ctor.Formals) {
+ var otherDt = arg.Type.AsIndDatatype;
+ if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed) { // otherDt lives in the same SCC
+ var otherUdt = (UserDefinedType)arg.Type.Normalize();
+ var i = 0;
+ foreach (var otherTp in otherDt.TypeArgs) {
+ if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
+ var tp = otherUdt.TypeArgs[i].AsTypeParameter;
+ if (tp != null && !tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {
+ tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;
+ thingsChanged = true;
+ }
+ }
+ i++;
+ }
+ }
+ }
+ }
+ }
+ }
+ // Now that we have computed the .NecessaryForEqualitySupportOfSurroundingInductiveDatatype values, mark the datatypes as ones
+ // where equality support should be checked by looking at the type arguments.
+ foreach (var dt in scc) {
+ dt.EqualitySupport = IndDatatypeDecl.ES.ConsultTypeArguments;
+ }
+ }
+
void ResolveAttributes(Attributes attrs, bool twoState) {
// order does not matter much for resolution, so resolve them in reverse order
for (; attrs != null; attrs = attrs.Prev) {
@@ -1133,7 +1621,7 @@ namespace Microsoft.Dafny { // In the remaining cases, proxy is a restricted proxy and t is a non-proxy
} else if (proxy is DatatypeProxy) {
- if (t.IsDatatype) {
+ if (t.IsIndDatatype) {
// all is fine, proxy can be redirected to t
} else {
return false;
@@ -1146,14 +1634,6 @@ namespace Microsoft.Dafny { return false;
}
- } else if (proxy is ObjectsTypeProxy) {
- if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {
- // all is good
- } else if (t is CollectionType) {
- proxy.T = new CollectionTypeProxy(new ObjectTypeProxy());
- return UnifyTypes(proxy.T, t);
- }
-
} else if (proxy is CollectionTypeProxy) {
CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy;
if (t is CollectionType) {
@@ -1235,10 +1715,6 @@ namespace Microsoft.Dafny { // all is fine
a.T = b;
return true;
- } else if (b is ObjectsTypeProxy) {
- // unify a and b by redirecting b to a, since a gives the stronger requirement
- b.T = a;
- 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);
@@ -1248,37 +1724,6 @@ namespace Microsoft.Dafny { return false;
}
- } else if (a is ObjectsTypeProxy) {
- if (b is ObjectsTypeProxy) {
- // fine
- a.T = b;
- return true;
- } else if (b is CollectionTypeProxy) {
- // fine provided b's collection-element-type can be unified with object or a class type
- a.T = b;
- return UnifyTypes(((CollectionTypeProxy)b).Arg, new ObjectTypeProxy());
- } else if (b is OperationTypeProxy) {
- // fine; restrict a to sets of object/class, and restrict b to set/seq of object/class
- if (((OperationTypeProxy)b).AllowSeq) {
- a.T = new CollectionTypeProxy(new ObjectTypeProxy());
- b.T = a.T;
- } else {
- a.T = new SetType(new ObjectTypeProxy());
- b.T = a.T;
- }
- return true;
- } else if (b is IndexableTypeProxy) {
- IndexableTypeProxy pb = (IndexableTypeProxy)b;
- // the intersection of ObjectsTypeProxy and IndexableTypeProxy is
- // EITHER a sequence of ObjectTypeProxy OR an array of anything OR map of ObjectTypeProxy in either domain or range.
- // TODO: here, only the first of the three cases is supported
- b.T = new SeqType(pb.Arg);
- a.T = b.T;
- return UnifyTypes(pb.Arg, new ObjectTypeProxy());
- } else {
- Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
- }
-
} else if (a is CollectionTypeProxy) {
if (b is CollectionTypeProxy) {
a.T = b;
@@ -2122,22 +2567,22 @@ namespace Microsoft.Dafny { UserDefinedType ctype = (UserDefinedType)nptype; // TODO: get rid of this statement, make this code handle any non-proxy type
#endif
// build the type substitution map
- Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
+ s.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
for (int i = 0; i < ctype.TypeArgs.Count; i++) {
- subst.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
+ s.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
}
foreach (TypeParameter p in callee.TypeArgs) {
- subst.Add(p, new ParamTypeProxy(p));
+ s.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));
}
// type check the arguments
for (int i = 0; i < callee.Ins.Count; i++) {
- Type st = SubstType(callee.Ins[i].Type, subst);
+ Type st = SubstType(callee.Ins[i].Type, s.TypeArgumentSubstitutions);
if (!UnifyTypes(cce.NonNull(s.Args[i].Type), st)) {
Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
}
}
for (int i = 0; i < callee.Outs.Count; i++) {
- Type st = SubstType(callee.Outs[i].Type, subst);
+ Type st = SubstType(callee.Outs[i].Type, s.TypeArgumentSubstitutions);
var lhs = s.Lhs[i];
if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {
Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);
@@ -2925,12 +3370,12 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Le:
case BinaryExpr.Opcode.Add:
{
- if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsDatatype) {
+ if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsIndDatatype) {
if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
expr.Type = Type.Bool;
- } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsDatatype) {
+ } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsIndDatatype) {
if (!UnifyTypes(e.E0.Type, new DatatypeProxy())) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
}
@@ -2959,7 +3404,7 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Gt:
case BinaryExpr.Opcode.Ge:
{
- if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsDatatype) {
+ if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsIndDatatype) {
if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
@@ -3467,24 +3912,24 @@ namespace Microsoft.Dafny { }
}
// build the type substitution map
- Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
+ e.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
for (int i = 0; i < ctype.TypeArgs.Count; i++) {
- subst.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
+ e.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
}
foreach (TypeParameter p in function.TypeArgs) {
- subst.Add(p, new ParamTypeProxy(p));
+ e.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));
}
// type check the arguments
for (int i = 0; i < function.Formals.Count; i++) {
Expression farg = e.Args[i];
ResolveExpression(farg, twoState);
Contract.Assert(farg.Type != null); // follows from postcondition of ResolveExpression
- Type s = SubstType(function.Formals[i].Type, subst);
+ Type s = SubstType(function.Formals[i].Type, e.TypeArgumentSubstitutions);
if (!UnifyTypes(farg.Type, s)) {
Error(e, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
}
}
- e.Type = SubstType(function.ResultType, subst);
+ e.Type = SubstType(function.ResultType, e.TypeArgumentSubstitutions);
}
// Resolution termination check
@@ -4112,6 +4557,7 @@ namespace Microsoft.Dafny { Contract.Assert(e.Seq.Type != null); // follows from postcondition of ResolveExpression
Type elementType = new InferredTypeProxy();
Type domainType = new InferredTypeProxy();
+
IndexableTypeProxy expectedType = new IndexableTypeProxy(elementType, domainType);
if (!UnifyTypes(e.Seq.Type, expectedType)) {
Error(e, "sequence/array/map selection requires a sequence, array or map (got {0})", e.Seq.Type);
@@ -4197,7 +4643,7 @@ namespace Microsoft.Dafny { return BinaryExpr.ResolvedOpcode.Disjoint;
}
case BinaryExpr.Opcode.Lt:
- if (operandType.IsDatatype || operandType is DatatypeProxy) {
+ if (operandType.IsIndDatatype || operandType is DatatypeProxy) {
return BinaryExpr.ResolvedOpcode.RankLt;
} else if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.ProperSubset;
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 26ec496e..e04c5e9b 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -4,11 +4,22 @@ using System.Diagnostics.Contracts; namespace Microsoft.Dafny
{
- public interface Rewriter
+ [ContractClass(typeof(IRewriterContracts))]
+ public interface IRewriter
{
void PreResolve(ModuleDecl m);
void PostResolve(ModuleDecl m);
}
+ [ContractClassFor(typeof(IRewriter))]
+ abstract class IRewriterContracts : IRewriter
+ {
+ public void PreResolve(ModuleDecl m) {
+ Contract.Requires(m != null);
+ }
+ public void PostResolve(ModuleDecl m) {
+ Contract.Requires(m != null);
+ }
+ }
/// <summary>
/// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate
@@ -48,7 +59,7 @@ namespace Microsoft.Dafny /// if (A != null) { Repr := Repr + {A}; }
/// if (F != null) { Repr := Repr + {F} + F.Repr; }
/// </summary>
- public class AutoContractsRewriter : Rewriter
+ public class AutoContractsRewriter : IRewriter
{
public void PreResolve(ModuleDecl m) {
foreach (var d in m.TopLevelDecls) {
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index d35fc22f..7cb302fa 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -265,11 +265,11 @@ public class Scanner { start[124] = 58;
start[59] = 19;
start[44] = 20;
+ start[40] = 21;
+ start[41] = 22;
start[60] = 59;
start[62] = 60;
start[46] = 61;
- start[40] = 22;
- start[41] = 23;
start[42] = 24;
start[96] = 25;
start[91] = 28;
@@ -498,40 +498,40 @@ public class Scanner { case "codatatype": t.kind = 15; break;
case "var": t.kind = 19; break;
case "type": t.kind = 21; break;
- case "method": t.kind = 24; break;
- case "constructor": t.kind = 25; break;
- case "returns": t.kind = 26; break;
- case "modifies": t.kind = 28; break;
- case "free": t.kind = 29; break;
- case "requires": t.kind = 30; break;
- case "ensures": t.kind = 31; break;
- case "decreases": t.kind = 32; break;
- case "bool": t.kind = 35; break;
- case "nat": t.kind = 36; break;
- case "int": t.kind = 37; break;
- case "set": t.kind = 38; break;
- case "multiset": t.kind = 39; break;
- case "seq": t.kind = 40; break;
- case "map": t.kind = 41; break;
- case "object": t.kind = 42; break;
- case "function": t.kind = 44; break;
- case "predicate": t.kind = 45; break;
- case "reads": t.kind = 46; break;
- case "label": t.kind = 49; break;
- case "break": t.kind = 50; break;
- case "return": t.kind = 51; break;
- case "assume": t.kind = 54; break;
- case "new": t.kind = 55; break;
- case "choose": t.kind = 58; break;
- case "if": t.kind = 59; break;
- case "else": t.kind = 60; break;
- case "case": t.kind = 61; break;
- case "while": t.kind = 63; break;
- case "invariant": t.kind = 64; break;
- case "match": t.kind = 65; break;
- case "assert": t.kind = 66; break;
- case "print": t.kind = 67; break;
- case "parallel": t.kind = 68; break;
+ case "method": t.kind = 27; break;
+ case "constructor": t.kind = 28; break;
+ case "returns": t.kind = 29; break;
+ case "modifies": t.kind = 31; break;
+ case "free": t.kind = 32; break;
+ case "requires": t.kind = 33; break;
+ case "ensures": t.kind = 34; break;
+ case "decreases": t.kind = 35; break;
+ case "bool": t.kind = 36; break;
+ case "nat": t.kind = 37; break;
+ case "int": t.kind = 38; break;
+ case "set": t.kind = 39; break;
+ case "multiset": t.kind = 40; break;
+ case "seq": t.kind = 41; break;
+ case "map": t.kind = 42; break;
+ case "object": t.kind = 43; break;
+ case "function": t.kind = 45; break;
+ case "predicate": t.kind = 46; break;
+ case "reads": t.kind = 47; break;
+ case "label": t.kind = 50; break;
+ case "break": t.kind = 51; break;
+ case "return": t.kind = 52; break;
+ case "assume": t.kind = 55; break;
+ case "new": t.kind = 56; break;
+ case "choose": t.kind = 59; break;
+ case "if": t.kind = 60; break;
+ case "else": t.kind = 61; break;
+ case "case": t.kind = 62; break;
+ case "while": t.kind = 64; break;
+ case "invariant": t.kind = 65; break;
+ case "match": t.kind = 66; break;
+ case "assert": t.kind = 67; break;
+ case "print": t.kind = 68; break;
+ case "parallel": t.kind = 69; break;
case "in": t.kind = 82; break;
case "false": t.kind = 92; break;
case "true": t.kind = 93; break;
@@ -652,47 +652,47 @@ public class Scanner { case 20:
{t.kind = 20; break;}
case 21:
- {t.kind = 27; break;}
+ {t.kind = 22; break;}
case 22:
- {t.kind = 33; break;}
+ {t.kind = 24; break;}
case 23:
- {t.kind = 34; break;}
+ {t.kind = 30; break;}
case 24:
- {t.kind = 47; break;}
- case 25:
{t.kind = 48; break;}
+ case 25:
+ {t.kind = 49; break;}
case 26:
- {t.kind = 52; break;}
- case 27:
{t.kind = 53; break;}
+ case 27:
+ {t.kind = 54; break;}
case 28:
- {t.kind = 56; break;}
- case 29:
{t.kind = 57; break;}
+ case 29:
+ {t.kind = 58; break;}
case 30:
- {t.kind = 62; break;}
+ {t.kind = 63; break;}
case 31:
if (ch == '>') {AddCh(); goto case 32;}
else {goto case 0;}
case 32:
- {t.kind = 69; break;}
- case 33:
{t.kind = 70; break;}
- case 34:
+ case 33:
{t.kind = 71; break;}
- case 35:
+ case 34:
{t.kind = 72; break;}
+ case 35:
+ {t.kind = 73; break;}
case 36:
if (ch == '&') {AddCh(); goto case 37;}
else {goto case 0;}
case 37:
- {t.kind = 73; break;}
- case 38:
{t.kind = 74; break;}
- case 39:
+ case 38:
{t.kind = 75; break;}
- case 40:
+ case 39:
{t.kind = 76; break;}
+ case 40:
+ {t.kind = 77; break;}
case 41:
{t.kind = 79; break;}
case 42:
@@ -731,41 +731,41 @@ public class Scanner { else {t.kind = 5; break;}
case 57:
recEnd = pos; recKind = 16;
- if (ch == '>') {AddCh(); goto case 30;}
- else if (ch == '=') {AddCh(); goto case 63;}
+ if (ch == '=') {AddCh(); goto case 63;}
+ else if (ch == '>') {AddCh(); goto case 30;}
else {t.kind = 16; break;}
case 58:
recEnd = pos; recKind = 17;
if (ch == '|') {AddCh(); goto case 39;}
else {t.kind = 17; break;}
case 59:
- recEnd = pos; recKind = 22;
+ recEnd = pos; recKind = 25;
if (ch == '=') {AddCh(); goto case 64;}
- else {t.kind = 22; break;}
+ else {t.kind = 25; break;}
case 60:
- recEnd = pos; recKind = 23;
+ recEnd = pos; recKind = 26;
if (ch == '=') {AddCh(); goto case 41;}
- else {t.kind = 23; break;}
+ else {t.kind = 26; break;}
case 61:
- recEnd = pos; recKind = 43;
+ recEnd = pos; recKind = 44;
if (ch == '.') {AddCh(); goto case 65;}
- else {t.kind = 43; break;}
+ else {t.kind = 44; break;}
case 62:
recEnd = pos; recKind = 83;
if (ch == '=') {AddCh(); goto case 42;}
else if (ch == '!') {AddCh(); goto case 43;}
else {t.kind = 83; break;}
case 63:
- recEnd = pos; recKind = 77;
+ recEnd = pos; recKind = 23;
if (ch == '>') {AddCh(); goto case 34;}
- else {t.kind = 77; break;}
+ else {t.kind = 23; break;}
case 64:
recEnd = pos; recKind = 78;
if (ch == '=') {AddCh(); goto case 31;}
else {t.kind = 78; break;}
case 65:
recEnd = pos; recKind = 100;
- if (ch == '.') {AddCh(); goto case 21;}
+ if (ch == '.') {AddCh(); goto case 23;}
else {t.kind = 100; break;}
}
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index cb880767..ddc51368 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -259,10 +259,10 @@ namespace GPUVerify private Expr MakeCTimesLocalIdRangeExpression(Variable v, Expr constant, string ReadOrWrite, int Thread)
{
- Expr CTimesLocalId = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr,
+ Expr CTimesLocalId = verifier.MakeBVMul(constant.Clone() as Expr,
new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread)));
- Expr CTimesLocalIdPlusC = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr,
+ Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr);
Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread));
@@ -293,10 +293,10 @@ namespace GPUVerify private Expr MakeCTimesGloalIdRangeExpr(Variable v, Expr constant, string ReadOrWrite, int Thread)
{
- Expr CTimesGlobalId = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr,
+ Expr CTimesGlobalId = verifier.MakeBVMul(constant.Clone() as Expr,
GlobalIdExpr("X", Thread));
- Expr CTimesGlobalIdPlusC = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL", constant.Clone() as Expr,
+ Expr CTimesGlobalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
GlobalIdExpr("X", Thread)), constant.Clone() as Expr);
Expr CTimesGlobalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesGlobalId, OffsetXExpr(v, ReadOrWrite, Thread));
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 40e27310..e3d94fcc 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -61,8 +61,6 @@ namespace GPUVerify public IRaceInstrumenter RaceInstrumenter;
public UniformityAnalyser uniformityAnalyser;
- public MayBeThreadConfigurationVariableAnalyser mayBeTidAnalyser;
- public MayBeGidAnalyser mayBeGidAnalyser;
public MayBeLocalIdPlusConstantAnalyser mayBeTidPlusConstantAnalyser;
public MayBeGlobalIdPlusConstantAnalyser mayBeGidPlusConstantAnalyser;
public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;
@@ -361,7 +359,7 @@ namespace GPUVerify DoUniformityAnalysis();
- DoMayBeTidAnalysis();
+ DoVariableDefinitionAnalysis();
DoMayBeIdPlusConstantAnalysis();
@@ -369,8 +367,6 @@ namespace GPUVerify DoArrayControlFlowAnalysis();
- DoVariableDefinitionAnalysis();
-
if (CommandLineOptions.ShowStages)
{
emitProgram(outputFilename + "_preprocessed");
@@ -483,15 +479,6 @@ namespace GPUVerify mayBePowerOfTwoAnalyser.Analyse();
}
- private void DoMayBeTidAnalysis()
- {
- mayBeTidAnalyser = new MayBeThreadConfigurationVariableAnalyser(this);
- mayBeTidAnalyser.Analyse();
-
- mayBeGidAnalyser = new MayBeGidAnalyser(this);
- mayBeGidAnalyser.Analyse();
- }
-
private void DoMayBeIdPlusConstantAnalysis()
{
mayBeTidPlusConstantAnalyser = new MayBeLocalIdPlusConstantAnalyser(this);
@@ -1040,15 +1027,29 @@ namespace GPUVerify return _GROUP_SIZE_Z != null;
}
- internal static string StripThreadIdentifier(string p)
+ internal static string StripThreadIdentifier(string p, out int id)
{
- if (p.Contains("$"))
+ if (p.EndsWith("$1"))
+ {
+ id = 1;
+ return p.Substring(0, p.Length - 2);
+ }
+ if (p.EndsWith("$2"))
{
- return p.Substring(0, p.LastIndexOf("$"));
+ id = 2;
+ return p.Substring(0, p.Length - 2);
}
+
+ id = 0;
return p;
}
+ internal static string StripThreadIdentifier(string p)
+ {
+ int id;
+ return StripThreadIdentifier(p, out id);
+ }
+
private void AddStartAndEndBarriers()
{
CallCmd FirstBarrier = new CallCmd(KernelImplementation.tok, BarrierProcedure.Name, new ExprSeq(), new IdentifierExprSeq());
@@ -1299,7 +1300,9 @@ namespace GPUVerify private Expr MakeBVFunctionCall(string functionName, string smtName, Microsoft.Boogie.Type resultType, params Expr[] args)
{
Function f = GetOrCreateBVFunction(functionName, smtName, resultType, args.Select(a => a.Type).ToArray());
- return new NAryExpr(Token.NoToken, new FunctionCall(f), new ExprSeq(args));
+ var e = new NAryExpr(Token.NoToken, new FunctionCall(f), new ExprSeq(args));
+ e.Type = resultType;
+ return e;
}
private Expr MakeBitVectorBinaryBoolean(string suffix, string smtName, Expr lhs, Expr rhs)
@@ -1316,6 +1319,12 @@ namespace GPUVerify internal Expr MakeBVSgt(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBoolean("SGT", "bvsgt", lhs, rhs); }
internal Expr MakeBVSge(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBoolean("SGE", "bvsge", lhs, rhs); }
+ internal Expr MakeBVAnd(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("AND", "bvand", lhs, rhs); }
+ internal Expr MakeBVAdd(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("ADD", "bvadd", lhs, rhs); }
+ internal Expr MakeBVSub(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("SUB", "bvsub", lhs, rhs); }
+ internal Expr MakeBVMul(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("MUL", "bvmul", lhs, rhs); }
+ internal Expr MakeBVURem(Expr lhs, Expr rhs) { return MakeBitVectorBinaryBitVector("UREM", "bvurem", lhs, rhs); }
+
internal static Expr MakeBitVectorBinaryBoolean(string functionName, Expr lhs, Expr rhs)
{
return new NAryExpr(lhs.tok, new FunctionCall(new Function(lhs.tok, functionName, new VariableSeq(new Variable[] {
@@ -1332,6 +1341,42 @@ namespace GPUVerify }), new LocalVariable(lhs.tok, new TypedIdent(lhs.tok, "result", Microsoft.Boogie.Type.GetBvType(32))))), new ExprSeq(new Expr[] { lhs, rhs }));
}
+ private static bool IsBVFunctionCall(Expr e, string smtName, out ExprSeq args)
+ {
+ args = null;
+ var ne = e as NAryExpr;
+ if (ne == null)
+ return false;
+
+ var fc = ne.Fun as FunctionCall;
+ if (fc == null)
+ return false;
+
+ string bvBuiltin = QKeyValue.FindStringAttribute(fc.Func.Attributes, "bvbuiltin");
+ if (bvBuiltin == smtName)
+ {
+ args = ne.Args;
+ return true;
+ }
+
+ return false;
+ }
+
+ private static bool IsBVFunctionCall(Expr e, string smtName, out Expr lhs, out Expr rhs)
+ {
+ ExprSeq es;
+ if (IsBVFunctionCall(e, smtName, out es))
+ {
+ lhs = es[0]; rhs = es[1];
+ return true;
+ }
+ lhs = null; rhs = null;
+ return false;
+ }
+
+ internal static bool IsBVAdd(Expr e, out Expr lhs, out Expr rhs) { return IsBVFunctionCall(e, "bvadd", out lhs, out rhs); }
+ internal static bool IsBVMul(Expr e, out Expr lhs, out Expr rhs) { return IsBVFunctionCall(e, "bvmul", out lhs, out rhs); }
+
internal Constant GetGroupSize(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
@@ -2291,14 +2336,9 @@ namespace GPUVerify return !arrayControlFlowAnalyser.MayAffectControlFlow(v.Name);
}
- internal static Expr StripThreadIdentifiers(Expr e)
- {
- return new ThreadIdentifierStripper().VisitExpr(e.Clone() as Expr);
- }
-
internal Expr GlobalIdExpr(string dimension)
{
- return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",
+ return MakeBVAdd(MakeBVMul(
new IdentifierExpr(Token.NoToken, GetGroupId(dimension)), new IdentifierExpr(Token.NoToken, GetGroupSize(dimension))),
new IdentifierExpr(Token.NoToken, MakeThreadId(Token.NoToken, dimension)));
}
@@ -2310,14 +2350,112 @@ namespace GPUVerify else
return new StructuredRegion(Impl);
}
- }
- class ThreadIdentifierStripper : StandardVisitor
- {
- public override Variable VisitVariable(Variable node)
+
+ public static bool IsGivenConstant(Expr e, Constant c)
+ {
+ if (!(e is IdentifierExpr))
+ return false;
+
+ var varName = ((IdentifierExpr)e).Decl.Name;
+ return (StripThreadIdentifier(varName) == StripThreadIdentifier(c.Name));
+ }
+
+ public bool SubstIsGivenConstant(Implementation impl, Expr e, Constant c)
+ {
+ if (!(e is IdentifierExpr))
+ return false;
+ e = varDefAnalyses[impl].SubstDefinitions(e, impl.Name);
+ return IsGivenConstant(e, c);
+ }
+
+ public Constant GetLocalIdConst(int dim)
+ {
+ switch (dim)
+ {
+ case 0: return _X;
+ case 1: return _Y;
+ case 2: return _Z;
+ default: Debug.Assert(false);
+ return null;
+ }
+ }
+
+ public Constant GetGroupIdConst(int dim)
+ {
+ switch (dim)
+ {
+ case 0: return _GROUP_X;
+ case 1: return _GROUP_Y;
+ case 2: return _GROUP_Z;
+ default: Debug.Assert(false);
+ return null;
+ }
+ }
+
+ public Constant GetGroupSizeConst(int dim)
+ {
+ switch (dim)
+ {
+ case 0: return _GROUP_SIZE_X;
+ case 1: return _GROUP_SIZE_Y;
+ case 2: return _GROUP_SIZE_Z;
+ default: Debug.Assert(false);
+ return null;
+ }
+ }
+
+ public bool IsLocalId(Expr e, int dim, Implementation impl)
+ {
+ return SubstIsGivenConstant(impl, e, GetLocalIdConst(dim));
+ }
+
+ public bool IsGlobalId(Expr e, int dim, Implementation impl)
+ {
+ e = varDefAnalyses[impl].SubstDefinitions(e, impl.Name);
+
+ if (e is NAryExpr && (e as NAryExpr).Fun.FunctionName.Equals("BV32_ADD"))
+ {
+ NAryExpr nary = e as NAryExpr;
+ Constant localId = GetLocalIdConst(dim);
+
+ if (IsGivenConstant(nary.Args[1], localId))
+ {
+ return IsGroupIdTimesGroupSize(nary.Args[0], dim);
+ }
+
+ if (IsGivenConstant(nary.Args[0], localId))
+ {
+ return IsGroupIdTimesGroupSize(nary.Args[1], dim);
+ }
+ }
+
+ return false;
+ }
+
+ private bool IsGroupIdTimesGroupSize(Expr expr, int dim)
+ {
+ if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))
+ {
+ NAryExpr innerNary = expr as NAryExpr;
+
+ if (IsGroupIdAndSize(dim, innerNary.Args[0], innerNary.Args[1]))
+ {
+ return true;
+ }
+
+ if (IsGroupIdAndSize(dim, innerNary.Args[1], innerNary.Args[0]))
+ {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ private bool IsGroupIdAndSize(int dim, Expr maybeGroupId, Expr maybeGroupSize)
{
- node.Name = GPUVerifier.StripThreadIdentifier(node.Name);
- return base.VisitVariable(node);
+ return IsGivenConstant(maybeGroupId, GetGroupIdConst(dim)) &&
+ IsGivenConstant(maybeGroupSize, GetGroupSizeConst(dim));
}
}
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index eba91cd2..6762e634 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -113,13 +113,11 @@ <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />
<Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />
<Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />
- <Compile Include="MayBeGidAnalyser.cs" />
<Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />
<Compile Include="KernelDualiser.cs" />
<Compile Include="LiveVariableAnalyser.cs" />
<Compile Include="LoopInvariantGenerator.cs" />
<Compile Include="MayBePowerOfTwoAnalyser.cs" />
- <Compile Include="MayBeThreadConfigurationVariableAnalyser.cs" />
<Compile Include="MayBeIdPlusConstantAnalyser.cs" />
<Compile Include="StructuredProgramVisitor.cs" />
<Compile Include="CrossThreadInvariantProcessor.cs" />
diff --git a/Source/GPUVerify/MayBeGidAnalyser.cs b/Source/GPUVerify/MayBeGidAnalyser.cs deleted file mode 100644 index f7d8c973..00000000 --- a/Source/GPUVerify/MayBeGidAnalyser.cs +++ /dev/null @@ -1,320 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics;
-using Microsoft.Boogie;
-
-namespace GPUVerify
-{
- class MayBeGidAnalyser : MayBeAnalyser
- {
- private static string[] dimensions = { "x", "y", "z" };
-
- private GPUVerifier verifier;
-
- private bool ProcedureChanged;
-
- private Dictionary<string, Dictionary<string, Dictionary<string, bool>>> mayBeInfo;
-
- public MayBeGidAnalyser(GPUVerifier verifier)
- {
- this.verifier = verifier;
-
- mayBeInfo = new Dictionary<string,Dictionary<string,Dictionary<string,bool>>>();
- foreach (string s in dimensions)
- {
- mayBeInfo[s] = new Dictionary<string, Dictionary<string, bool>>();
- }
-
- }
-
- internal void Analyse()
- {
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if(D is Implementation)
- {
- Implementation Impl = D as Implementation;
-
- foreach (string s in dimensions)
- {
- mayBeInfo[s][Impl.Name] = new Dictionary<string, bool>();
- }
-
- foreach (Variable v in Impl.LocVars)
- {
- foreach (string s in dimensions)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.InParams)
- {
- foreach (string s in dimensions)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.OutParams)
- {
- foreach (string s in dimensions)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- ProcedureChanged = true;
- }
- }
-
- while (ProcedureChanged)
- {
- ProcedureChanged = false;
-
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if (D is Implementation)
- {
- Implementation Impl = D as Implementation;
- Analyse(Impl);
- }
- }
- }
-
- if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)
- {
- dump();
- }
- }
-
- private void Analyse(Implementation Impl)
- {
- Analyse(Impl, verifier.RootRegion(Impl));
- }
-
- private void Analyse(Implementation impl, IRegion region)
- {
- foreach (Cmd c in region.Cmds())
- {
- if (c is AssignCmd)
- {
- foreach (string s in dimensions)
- {
- TransferAssign(impl, c as AssignCmd, s);
- }
- }
- else if (c is CallCmd)
- {
- foreach (string s in dimensions)
- {
- TransferCall(impl, c as CallCmd, s);
- }
- }
- else if (c is HavocCmd)
- {
- foreach (string s in dimensions)
- {
- TransferHavoc(impl, c as HavocCmd, s);
- }
- }
- }
- }
-
- private void TransferHavoc(Implementation impl, HavocCmd havoc, string component)
- {
- Debug.Assert(havoc.Vars.Length == 1);
- if (MayBe(component, impl.Name, havoc.Vars[0].Decl.Name))
- {
- SetNot(component, impl.Name, havoc.Vars[0].Decl.Name);
- }
- }
-
- private void TransferCall(Implementation impl, CallCmd callCmd, string component)
- {
- if (callCmd.callee != verifier.BarrierProcedure.Name)
- {
-
- Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
- for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
- {
- if (MayBe(component, callCmd.callee, CalleeImplementation.InParams[i].Name)
- && !MayBe(component, impl.Name, callCmd.Ins[i]))
- {
- SetNot(component, callCmd.callee, CalleeImplementation.InParams[i].Name);
- }
- }
-
- for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
- {
- if (MayBe(component, impl.Name, callCmd.Outs[i].Name)
- && !MayBe(component, callCmd.callee, CalleeImplementation.OutParams[i].Name))
- {
- SetNot(component, impl.Name, callCmd.Outs[i].Name);
- }
- }
-
- }
- }
-
- private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)
- {
- for (int i = 0; i != assignCmd.Lhss.Count; ++i)
- {
- if (assignCmd.Lhss[i] is SimpleAssignLhs)
- {
- SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[i];
-
- if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
- && !MayBe(component, impl.Name, rhs))
- {
- SetNot(component, impl.Name, lhs.AssignedVariable.Name);
- }
- }
- }
- }
-
- private void SetNot(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = false;
- ProcedureChanged = true;
- }
-
- private void SetMayBe(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = true;
- }
-
- override internal bool MayBe(string component, string proc, string v)
- {
- if (!mayBeInfo[component].ContainsKey(proc))
- {
- return false;
- }
-
- if (!mayBeInfo[component][proc].ContainsKey(v))
- {
- return false;
- }
-
- return mayBeInfo[component][proc][v];
- }
-
- override internal bool MayBe(string component, string proc, Expr e)
- {
- if (e is IdentifierExpr)
- {
- return MayBe(component, proc, (e as IdentifierExpr).Decl.Name);
- }
-
- if (e is NAryExpr && (e as NAryExpr).Fun.FunctionName.Equals("BV32_ADD"))
- {
- NAryExpr nary = e as NAryExpr;
-
- string localIdString = null;
-
- if (component.Equals("x"))
- {
- localIdString = GPUVerifier.LOCAL_ID_X_STRING;
- }
- else if (component.Equals("y"))
- {
- localIdString = GPUVerifier.LOCAL_ID_Y_STRING;
- }
- else if (component.Equals("z"))
- {
- localIdString = GPUVerifier.LOCAL_ID_Z_STRING;
- }
- else
- {
- Debug.Assert(false);
- }
-
- if(verifier.mayBeTidAnalyser.MayBe(localIdString, proc, nary.Args[1]))
- {
- return IsGroupIdTimesGroupSize(component, proc, nary.Args[0]);
- }
-
- if (verifier.mayBeTidAnalyser.MayBe(localIdString, proc, nary.Args[0]))
- {
- return IsGroupIdTimesGroupSize(component, proc, nary.Args[1]);
- }
- }
-
- return false;
- }
-
- private bool IsGroupIdTimesGroupSize(string component, string proc, Expr expr)
- {
- if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))
- {
- NAryExpr innerNary = expr as NAryExpr;
-
- if (IsGroupIdAndSize(component, proc, innerNary.Args[0], innerNary.Args[1]))
- {
- return true;
- }
-
- if (IsGroupIdAndSize(component, proc, innerNary.Args[1], innerNary.Args[0]))
- {
- return true;
- }
- }
- return false;
- }
-
- private bool IsGroupIdAndSize(string component, string proc, Expr maybeGroupId, Expr maybeGroupSize)
- {
- string groupIdString = null;
- string groupSizeString = null;
- if (component.Equals("x"))
- {
- groupIdString = GPUVerifier.GROUP_ID_X_STRING;
- groupSizeString = GPUVerifier.GROUP_SIZE_X_STRING;
- }
- else if (component.Equals("y"))
- {
- groupIdString = GPUVerifier.GROUP_ID_Y_STRING;
- groupSizeString = GPUVerifier.GROUP_SIZE_Y_STRING;
- }
- else if (component.Equals("z"))
- {
- groupIdString = GPUVerifier.GROUP_ID_Z_STRING;
- groupSizeString = GPUVerifier.GROUP_SIZE_Z_STRING;
- }
- else
- {
- Debug.Assert(false);
- }
-
- return verifier.mayBeTidAnalyser.MayBe(groupIdString, proc, maybeGroupId) &&
- verifier.mayBeTidAnalyser.MayBe(groupSizeString, proc, maybeGroupSize);
- }
-
- private void dump()
- {
- foreach (string s in dimensions)
- {
- Console.WriteLine("*** global_id_" + s + " ***");
-
- foreach (string p in mayBeInfo[s].Keys)
- {
- Console.WriteLine(" Procedure " + p);
-
- foreach (string v in mayBeInfo[s][p].Keys)
- {
- if (mayBeInfo[s][p][v])
- {
- Console.WriteLine(" " + v + ": may be global_id_" + s);
- }
- }
- }
- }
-
- }
-
- }
-}
diff --git a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs index a57f35ee..3ee8edc8 100644 --- a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs +++ b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs @@ -11,8 +11,6 @@ namespace GPUVerify {
protected GPUVerifier verifier;
- protected MayBeAnalyser mayBeAnalyser;
-
// Given a p.v, says whether p.v may be assigned to a tid variable at some point
protected Dictionary<string, Dictionary<string, bool>> mayBeAssignedId;
@@ -104,7 +102,7 @@ namespace GPUVerify Variable rhsV = (assign.Rhss[i] as IdentifierExpr).Decl;
- if (mayBeAnalyser.MayBe(ComponentString(), impl.Name, rhsV.Name))
+ if (IsId(assign.Rhss[i], impl))
{
mayBeAssignedId[impl.Name][lhsV.Name] = true;
}
@@ -128,6 +126,7 @@ namespace GPUVerify }
}
+
private string ConvertToString(Expr constantIncrement)
{
if (constantIncrement is IdentifierExpr)
@@ -217,7 +216,7 @@ namespace GPUVerify internal abstract string idKind();
- protected abstract string ComponentString();
+ protected abstract bool IsId(Expr expr, Implementation impl);
internal Expr GetIncrement(string p, string v)
{
@@ -260,7 +259,11 @@ namespace GPUVerify internal MayBeLocalIdPlusConstantAnalyser(GPUVerifier verifier) : base(verifier)
{
- mayBeAnalyser = verifier.mayBeTidAnalyser;
+ }
+
+ protected override bool IsId(Expr expr, Implementation impl)
+ {
+ return verifier.IsLocalId(expr, 0, impl);
}
override internal Expr MakeIdExpr()
@@ -272,11 +275,6 @@ namespace GPUVerify {
return "local id";
}
-
- protected override string ComponentString()
- {
- return GPUVerifier.LOCAL_ID_X_STRING;
- }
}
class MayBeGlobalIdPlusConstantAnalyser : MayBeIdPlusConstantAnalyser
@@ -284,7 +282,11 @@ namespace GPUVerify internal MayBeGlobalIdPlusConstantAnalyser(GPUVerifier verifier)
: base(verifier)
{
- mayBeAnalyser = verifier.mayBeGidAnalyser;
+ }
+
+ protected override bool IsId(Expr expr, Implementation impl)
+ {
+ return verifier.IsGlobalId(expr, 0, impl);
}
internal override string idKind()
@@ -296,12 +298,6 @@ namespace GPUVerify {
return verifier.GlobalIdExpr("X");
}
-
- protected override string ComponentString()
- {
- return "x";
- }
-
}
diff --git a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs deleted file mode 100644 index d445d422..00000000 --- a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs +++ /dev/null @@ -1,273 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics;
-using Microsoft.Boogie;
-
-namespace GPUVerify
-{
- abstract class MayBeAnalyser
- {
- abstract internal bool MayBe(string component, string proc, string v);
- abstract internal bool MayBe(string component, string proc, Expr e);
- }
-
- class MayBeThreadConfigurationVariableAnalyser : MayBeAnalyser
- {
- private static string[] SpecialNames = {
- GPUVerifier.LOCAL_ID_X_STRING,
- GPUVerifier.LOCAL_ID_Y_STRING,
- GPUVerifier.LOCAL_ID_Z_STRING,
- GPUVerifier.GROUP_ID_X_STRING,
- GPUVerifier.GROUP_ID_Y_STRING,
- GPUVerifier.GROUP_ID_Z_STRING,
- GPUVerifier.NUM_GROUPS_X_STRING,
- GPUVerifier.NUM_GROUPS_Y_STRING,
- GPUVerifier.NUM_GROUPS_Z_STRING,
- GPUVerifier.GROUP_SIZE_X_STRING,
- GPUVerifier.GROUP_SIZE_Y_STRING,
- GPUVerifier.GROUP_SIZE_Z_STRING
- };
-
- private GPUVerifier verifier;
-
- private bool ProcedureChanged;
-
- private Dictionary<string, Dictionary<string, Dictionary<string, bool>>> mayBeInfo;
-
- public MayBeThreadConfigurationVariableAnalyser(GPUVerifier verifier)
- {
- this.verifier = verifier;
-
- mayBeInfo = new Dictionary<string,Dictionary<string,Dictionary<string,bool>>>();
- foreach (string s in SpecialNames)
- {
- mayBeInfo[s] = new Dictionary<string, Dictionary<string, bool>>();
- }
-
- }
-
- internal void Analyse()
- {
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if(D is Implementation)
- {
- Implementation Impl = D as Implementation;
-
- foreach (string s in SpecialNames)
- {
- mayBeInfo[s][Impl.Name] = new Dictionary<string, bool>();
- }
-
- SetMayBe(GPUVerifier.LOCAL_ID_X_STRING, Impl.Name, GPUVerifier._X.Name);
- SetMayBe(GPUVerifier.LOCAL_ID_Y_STRING, Impl.Name, GPUVerifier._Y.Name);
- SetMayBe(GPUVerifier.LOCAL_ID_Z_STRING, Impl.Name, GPUVerifier._Z.Name);
-
- SetMayBe(GPUVerifier.GROUP_ID_X_STRING, Impl.Name, GPUVerifier._GROUP_X.Name);
- SetMayBe(GPUVerifier.GROUP_ID_Y_STRING, Impl.Name, GPUVerifier._GROUP_Y.Name);
- SetMayBe(GPUVerifier.GROUP_ID_Z_STRING, Impl.Name, GPUVerifier._GROUP_Z.Name);
-
- SetMayBe(GPUVerifier.GROUP_SIZE_X_STRING, Impl.Name, GPUVerifier._GROUP_SIZE_X.Name);
- SetMayBe(GPUVerifier.GROUP_SIZE_Y_STRING, Impl.Name, GPUVerifier._GROUP_SIZE_Y.Name);
- SetMayBe(GPUVerifier.GROUP_SIZE_Z_STRING, Impl.Name, GPUVerifier._GROUP_SIZE_Z.Name);
-
- SetMayBe(GPUVerifier.NUM_GROUPS_X_STRING, Impl.Name, GPUVerifier._NUM_GROUPS_X.Name);
- SetMayBe(GPUVerifier.NUM_GROUPS_Y_STRING, Impl.Name, GPUVerifier._NUM_GROUPS_Y.Name);
- SetMayBe(GPUVerifier.NUM_GROUPS_Z_STRING, Impl.Name, GPUVerifier._NUM_GROUPS_Z.Name);
-
- foreach (Variable v in Impl.LocVars)
- {
- foreach (string s in SpecialNames)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.InParams)
- {
- foreach (string s in SpecialNames)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- foreach (Variable v in Impl.OutParams)
- {
- foreach (string s in SpecialNames)
- {
- SetMayBe(s, Impl.Name, v.Name);
- }
- }
-
- ProcedureChanged = true;
- }
- }
-
- while (ProcedureChanged)
- {
- ProcedureChanged = false;
-
- foreach (Declaration D in verifier.Program.TopLevelDeclarations)
- {
- if (D is Implementation)
- {
- Implementation Impl = D as Implementation;
- Analyse(Impl);
- }
- }
- }
-
- if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)
- {
- dump();
- }
- }
-
- private void Analyse(Implementation Impl)
- {
- Analyse(Impl, verifier.RootRegion(Impl));
- }
-
- private void Analyse(Implementation impl, IRegion region)
- {
- foreach (Cmd c in region.Cmds())
- {
- if (c is AssignCmd)
- {
- foreach (string s in SpecialNames)
- {
- TransferAssign(impl, c as AssignCmd, s);
- }
- }
- else if (c is CallCmd)
- {
- foreach (string s in SpecialNames)
- {
- TransferCall(impl, c as CallCmd, s);
- }
- }
- else if (c is HavocCmd)
- {
- foreach (string s in SpecialNames)
- {
- TransferHavoc(impl, c as HavocCmd, s);
- }
- }
- }
- }
-
- private void TransferHavoc(Implementation impl, HavocCmd havoc, string component)
- {
- Debug.Assert(havoc.Vars.Length == 1);
- if (MayBe(component, impl.Name, havoc.Vars[0].Decl.Name))
- {
- SetNot(component, impl.Name, havoc.Vars[0].Decl.Name);
- }
- }
-
- private void TransferCall(Implementation impl, CallCmd callCmd, string component)
- {
- if (callCmd.callee != verifier.BarrierProcedure.Name)
- {
-
- Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);
- for (int i = 0; i < CalleeImplementation.InParams.Length; i++)
- {
- if (MayBe(component, callCmd.callee, CalleeImplementation.InParams[i].Name)
- && !MayBe(component, impl.Name, callCmd.Ins[i]))
- {
- SetNot(component, callCmd.callee, CalleeImplementation.InParams[i].Name);
- }
- }
-
- for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)
- {
- if (MayBe(component, impl.Name, callCmd.Outs[i].Name)
- && !MayBe(component, callCmd.callee, CalleeImplementation.OutParams[i].Name))
- {
- SetNot(component, impl.Name, callCmd.Outs[i].Name);
- }
- }
-
- }
- }
-
- private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)
- {
- for (int i = 0; i != assignCmd.Lhss.Count; ++i)
- {
- if (assignCmd.Lhss[i] is SimpleAssignLhs)
- {
- SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;
- Expr rhs = assignCmd.Rhss[i];
-
- if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)
- && !MayBe(component, impl.Name, rhs))
- {
- SetNot(component, impl.Name, lhs.AssignedVariable.Name);
- }
- }
- }
- }
-
- private void SetNot(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = false;
- ProcedureChanged = true;
- }
-
- private void SetMayBe(string component, string proc, string v)
- {
- mayBeInfo[component][proc][v] = true;
- }
-
- override internal bool MayBe(string component, string proc, string v)
- {
- if (!mayBeInfo[component].ContainsKey(proc))
- {
- return false;
- }
-
- if (!mayBeInfo[component][proc].ContainsKey(v))
- {
- return false;
- }
-
- return mayBeInfo[component][proc][v];
- }
-
- override internal bool MayBe(string component, string proc, Expr e)
- {
- if (e is IdentifierExpr)
- {
- return MayBe(component, proc, (e as IdentifierExpr).Decl.Name);
- }
- return false;
- }
-
- private void dump()
- {
- foreach (string s in SpecialNames)
- {
- Console.WriteLine("*** " + s + " ***");
-
- foreach (string p in mayBeInfo[s].Keys)
- {
- Console.WriteLine(" Procedure " + p);
-
- foreach (string v in mayBeInfo[s][p].Keys)
- {
- if (mayBeInfo[s][p][v])
- {
- Console.WriteLine(" " + v + ": may be " + s);
- }
- }
- }
- }
-
- }
-
- }
-}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 13a4585b..5a75fa21 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -131,121 +131,145 @@ namespace GPUVerify }
}
- private bool TryGenerateCandidateForDirectStridedAccess(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)
+ private class StrideConstraint {}
+ private class EqStrideConstraint : StrideConstraint {
+ public EqStrideConstraint(Expr eq) { this.eq = eq; }
+ public Expr eq;
+ }
+ private class ModStrideConstraint : StrideConstraint {
+ public ModStrideConstraint(Expr mod, Expr modEq) { this.mod = mod; this.modEq = modEq; }
+ public Expr mod, modEq;
+ }
+
+ private StrideConstraint BuildBottomStrideConstraint(Expr e)
{
- if (!(e is NAryExpr))
- {
- return false;
- }
+ int width = e.Type.BvBits;
+ return new ModStrideConstraint(new LiteralExpr(Token.NoToken, BigNum.FromInt(1), width),
+ new LiteralExpr(Token.NoToken, BigNum.FromInt(0), width));
+ }
- NAryExpr nary = e as NAryExpr;
+ private bool IsBottomStrideConstraint(StrideConstraint sc)
+ {
+ var msc = sc as ModStrideConstraint;
+ if (msc == null)
+ return false;
- if (!nary.Fun.FunctionName.Equals("BV32_ADD"))
- {
+ var le = msc.mod as LiteralExpr;
+ if (le == null)
return false;
- }
- {
- Expr constant = IsIdPlusConstantMultiple(nary.Args[0], nary.Args[1], true, impl);
- if (constant != null)
- {
- Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));
- Expr modPow2Expr = ExprModPow2EqualsId(offsetExpr, constant, new IdentifierExpr(Token.NoToken,
- verifier.MakeThreadId(Token.NoToken, "X")));
+ var bvc = le.Val as BvConst;
+ if (bvc == null)
+ return false;
- Expr candidateInvariantExpr = Expr.Imp(
- new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),
- modPow2Expr);
+ return bvc.Value.InInt32 && bvc.Value.ToInt == 1;
+ }
- AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride local");
- return true;
- }
+ private StrideConstraint BuildAddStrideConstraint(Expr e, StrideConstraint lhsc, StrideConstraint rhsc)
+ {
+ if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint)
+ {
+ return new EqStrideConstraint(e);
}
- {
- Expr constant = IsIdPlusConstantMultiple(nary.Args[0], nary.Args[1], false, impl);
- if (constant != null)
- {
- Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));
- Expr modPow2Expr = ExprModPow2EqualsId(offsetExpr, constant, verifier.GlobalIdExpr("X"));
+ if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)
+ return BuildAddStrideConstraint(e, rhsc, lhsc);
- Expr candidateInvariantExpr = Expr.Imp(
- new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),
- modPow2Expr);
+ if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint)
+ {
+ var lhsmc = (ModStrideConstraint)lhsc;
+ var rhsec = (EqStrideConstraint)rhsc;
- AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride global");
- return true;
- }
+ return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsec.eq));
}
- return false;
+ if (lhsc is ModStrideConstraint && rhsc is ModStrideConstraint)
+ {
+ var lhsmc = (ModStrideConstraint)lhsc;
+ var rhsmc = (ModStrideConstraint)rhsc;
- }
+ if (lhsmc.mod == rhsmc.mod)
+ return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsmc.modEq));
+ }
- private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag)
- {
- Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);
- verifier.AddCandidateInvariant(region, candidate, tag);
+ return BuildBottomStrideConstraint(e);
}
- private Expr IsIdPlusConstantMultiple(Expr arg1, Expr arg2, bool local, Implementation impl)
+ private StrideConstraint BuildMulStrideConstraint(Expr e, StrideConstraint lhsc, StrideConstraint rhsc)
{
+ if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint)
{
- Expr constant = IsConstantMultiple(arg2);
- if (constant != null && IsId(arg1, local, impl))
- {
- return constant;
- }
+ return new EqStrideConstraint(e);
}
+ if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)
+ return BuildMulStrideConstraint(e, rhsc, lhsc);
+
+ if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint)
{
- Expr constant = IsConstantMultiple(arg1);
- if (constant != null && IsId(arg2, local, impl))
- {
- return constant;
- }
- }
+ var lhsmc = (ModStrideConstraint)lhsc;
+ var rhsec = (EqStrideConstraint)rhsc;
- return null;
+ return new ModStrideConstraint(verifier.MakeBVMul(lhsmc.mod, rhsec.eq),
+ verifier.MakeBVMul(lhsmc.modEq, rhsec.eq));
+ }
+ return BuildBottomStrideConstraint(e);
}
- private Expr IsConstantMultiple(Expr e)
+ private StrideConstraint BuildStrideConstraint(Implementation impl, Expr e)
{
- if (!(e is NAryExpr))
- {
- return null;
- }
+ if (e is LiteralExpr || (e is IdentifierExpr && ((IdentifierExpr)e).Decl is Constant))
+ return new EqStrideConstraint(e);
- NAryExpr nary = e as NAryExpr;
+ Expr lhs, rhs;
- if (!(nary.Fun.FunctionName.Equals("BV32_MUL")))
+ if (GPUVerifier.IsBVAdd(e, out lhs, out rhs))
{
- return null;
+ var lhsc = BuildStrideConstraint(impl, lhs);
+ var rhsc = BuildStrideConstraint(impl, rhs);
+ return BuildAddStrideConstraint(e, lhsc, rhsc);
}
- if (IsConstant(nary.Args[0]))
+ if (GPUVerifier.IsBVMul(e, out lhs, out rhs))
{
- return nary.Args[0];
+ var lhsc = BuildStrideConstraint(impl, lhs);
+ var rhsc = BuildStrideConstraint(impl, rhs);
+ return BuildMulStrideConstraint(e, lhsc, rhsc);
}
- if (IsConstant(nary.Args[1]))
- {
- return nary.Args[1];
- }
-
- return null;
-
+ return BuildBottomStrideConstraint(e);
}
- private bool IsId(Expr mayBeId, bool local, Implementation impl)
+ private bool TryGenerateCandidateForDirectStridedAccess(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)
{
- if (local)
+ bool isConstant;
+ e = verifier.varDefAnalyses[impl].SubstDefinitions(e, impl.Name, out isConstant);
+ if (isConstant)
+ return false;
+
+ var sc = BuildStrideConstraint(impl, e);
+ var msc = sc as ModStrideConstraint;
+ if (msc != null && !IsBottomStrideConstraint(msc))
{
- return verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, mayBeId);
+ Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));
+ Expr modEqExpr = Expr.Eq(verifier.MakeBVURem(offsetExpr, msc.mod), verifier.MakeBVURem(msc.modEq, msc.mod));
+
+ Expr candidateInvariantExpr = Expr.Imp(
+ new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),
+ modEqExpr);
+
+ AddAccessRelatedCandidateInvariant(region, accessKind, candidateInvariantExpr, impl.Name, "direct stride");
+ return true;
}
- return verifier.mayBeGidAnalyser.MayBe("x", impl.Name, mayBeId);
+ return false;
+ }
+
+ private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag)
+ {
+ Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);
+ verifier.AddCandidateInvariant(region, candidate, tag);
}
private bool TryGenerateCandidateForReducedStrengthStrideVariable(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)
@@ -379,14 +403,14 @@ namespace GPUVerify {
if (DoesNotReferTo(nary.Args[0], v))
{
- return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_SUB",
+ return verifier.MakeBVSub(
InverseOfLinearFunctionOfVariable(nary.Args[1], v, offsetExpr),
nary.Args[0]);
}
else
{
Debug.Assert(DoesNotReferTo(nary.Args[1], v));
- return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_SUB",
+ return verifier.MakeBVSub(
InverseOfLinearFunctionOfVariable(nary.Args[0], v, offsetExpr),
nary.Args[1]);
}
@@ -400,11 +424,10 @@ namespace GPUVerify private Expr ExprModPow2EqualsId(Expr expr, Expr powerOfTwoExpr, Expr threadIdExpr)
{
- Expr Pow2Minus1 = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_SUB", powerOfTwoExpr,
+ Expr Pow2Minus1 = verifier.MakeBVSub(powerOfTwoExpr,
new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 32));
- Expr Pow2Minus1BitAndExpr =
- GPUVerifier.MakeBitVectorBinaryBitVector("BV32_AND", Pow2Minus1, expr);
+ Expr Pow2Minus1BitAndExpr = verifier.MakeBVAnd(Pow2Minus1, expr);
return Expr.Eq(Pow2Minus1BitAndExpr, threadIdExpr);
@@ -453,7 +476,7 @@ namespace GPUVerify private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType)
{
var offsets = GetOffsetsAccessed(region, v, accessType)
- .Select(ofs => verifier.varDefAnalyses[impl].SubstDualisedDefinitions(ofs, 1, impl.Name))
+ .Select(ofs => verifier.varDefAnalyses[impl].SubstDefinitions(ofs, impl.Name))
.ToList();
if (offsets.Count != 0 && !offsets.Contains(null))
@@ -520,8 +543,8 @@ namespace GPUVerify }
return
- (SameConstant(nary.Args[0], constant) && verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, nary.Args[1])) ||
- (SameConstant(nary.Args[1], constant) && verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, nary.Args[0]));
+ (SameConstant(nary.Args[0], constant) && verifier.IsLocalId(nary.Args[1], 0, impl)) ||
+ (SameConstant(nary.Args[1], constant) && verifier.IsLocalId(nary.Args[0], 0, impl));
}
@@ -558,8 +581,8 @@ namespace GPUVerify }
return
- (SameConstant(nary.Args[0], constant) && verifier.mayBeGidAnalyser.MayBe("x", impl.Name, nary.Args[1])) ||
- (SameConstant(nary.Args[1], constant) && verifier.mayBeGidAnalyser.MayBe("x", impl.Name, nary.Args[0]));
+ (SameConstant(nary.Args[0], constant) && verifier.IsGlobalId(nary.Args[1], 0, impl)) ||
+ (SameConstant(nary.Args[1], constant) && verifier.IsGlobalId(nary.Args[0], 0, impl));
}
diff --git a/Source/GPUVerify/VariableDefinitionAnalysis.cs b/Source/GPUVerify/VariableDefinitionAnalysis.cs index f55e51e8..5dac47d6 100644 --- a/Source/GPUVerify/VariableDefinitionAnalysis.cs +++ b/Source/GPUVerify/VariableDefinitionAnalysis.cs @@ -5,12 +5,14 @@ using System.Linq; namespace GPUVerify {
+using VarDef = Tuple<Expr, bool>;
+
class VariableDefinitionAnalysis {
GPUVerifier verifier;
Implementation impl;
- Dictionary<Variable, Expr> defMap = new Dictionary<Variable, Expr>();
- Dictionary<string, Expr> namedDefMap = new Dictionary<string, Expr>();
+ Dictionary<Variable, VarDef> defMap = new Dictionary<Variable, VarDef>();
+ Dictionary<string, VarDef> namedDefMap = new Dictionary<string, VarDef>();
bool changed;
VariableDefinitionAnalysis(GPUVerifier v, Implementation i) {
@@ -19,12 +21,9 @@ class VariableDefinitionAnalysis { }
private class IsConstantVisitor : StandardVisitor {
- private VariableDefinitionAnalysis analysis;
public bool isConstant = true;
- public IsConstantVisitor(VariableDefinitionAnalysis a) {
- analysis = a;
- }
+ public IsConstantVisitor() {}
public override Expr VisitNAryExpr(NAryExpr expr) {
if (expr.Fun is MapSelect) {
@@ -33,26 +32,48 @@ class VariableDefinitionAnalysis { } else
return base.VisitNAryExpr(expr);
}
+ };
+
+ private class IsDerivedFromConstantsVisitor : StandardVisitor {
+ private VariableDefinitionAnalysis analysis;
+ public bool isDerivedFromConstants = true;
+
+ public IsDerivedFromConstantsVisitor(VariableDefinitionAnalysis a) {
+ analysis = a;
+ }
public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
if (expr.Decl is Constant)
return expr;
- if (!analysis.defMap.ContainsKey(expr.Decl) || analysis.defMap[expr.Decl] == null)
- isConstant = false;
+ if (!analysis.defMap.ContainsKey(expr.Decl) || !analysis.defMap[expr.Decl].Item2)
+ isDerivedFromConstants = false;
return expr;
}
};
bool IsConstant(Expr e) {
- var v = new IsConstantVisitor(this);
+ var v = new IsConstantVisitor();
v.Visit(e);
return v.isConstant;
}
- void UpdateDefMap(Variable v, Expr def) {
- if (!defMap.ContainsKey(v) || defMap[v] != def) {
+ bool IsDerivedFromConstants(Expr e) {
+ var v = new IsDerivedFromConstantsVisitor(this);
+ v.Visit(e);
+ return v.isDerivedFromConstants;
+ }
+
+ void UpdateDefMap(Variable v, Expr def, bool isConstant) {
+ if (!defMap.ContainsKey(v)) {
changed = true;
- defMap[v] = def;
+ defMap[v] = new VarDef(def, isConstant);
+ return;
+ }
+
+ var d = defMap[v];
+ if (d.Item1 != def || d.Item2 != isConstant) {
+ changed = true;
+ defMap[v] = new VarDef(def, isConstant);
}
}
@@ -60,10 +81,10 @@ class VariableDefinitionAnalysis { if (lhs is SimpleAssignLhs) {
var sLhs = (SimpleAssignLhs)lhs;
var theVar = sLhs.DeepAssignedVariable;
- if ((defMap.ContainsKey(theVar) && defMap[theVar] != rhs) || !IsConstant(rhs)) {
- UpdateDefMap(theVar, null);
+ if ((defMap.ContainsKey(theVar) && defMap[theVar].Item1 != rhs) || !IsConstant(rhs)) {
+ UpdateDefMap(theVar, null, false);
} else {
- UpdateDefMap(theVar, rhs);
+ UpdateDefMap(theVar, rhs, IsDerivedFromConstants(rhs));
}
}
}
@@ -78,11 +99,16 @@ class VariableDefinitionAnalysis { AddAssignment(a.Item1, a.Item2);
}
}
+ if (c is HavocCmd) {
+ var hCmd = (HavocCmd)c;
+ foreach (Variable v in hCmd.Vars)
+ UpdateDefMap(v, null, false);
+ }
}
} while (changed);
}
- private class BuildNamedDefVisitor : StandardVisitor {
+ private class BuildNamedDefVisitor : Duplicator {
private VariableDefinitionAnalysis analysis;
public BuildNamedDefVisitor(VariableDefinitionAnalysis a) {
@@ -92,56 +118,79 @@ class VariableDefinitionAnalysis { public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
if (expr.Decl is Constant)
return expr;
- return analysis.BuildNamedDefFor(expr.Decl);
+ return analysis.BuildNamedDefFor(expr.Decl, expr);
}
}
- Expr BuildNamedDefFor(Variable v) {
- Expr def;
+ Expr BuildNamedDefFor(Variable v, Expr e = null) {
+ VarDef def;
if (namedDefMap.TryGetValue(v.Name, out def))
- return def;
- def = (Expr)new BuildNamedDefVisitor(this).Visit(defMap[v].Clone());
- namedDefMap[v.Name] = def;
- return def;
+ return def.Item1;
+
+ def = defMap[v];
+ Expr defExpr;
+ if (def.Item1 == null)
+ defExpr = e;
+ else
+ defExpr = (Expr)new BuildNamedDefVisitor(this).Visit(def.Item1.Clone());
+ namedDefMap[v.Name] = new VarDef(defExpr, def.Item2);
+
+ return defExpr;
}
void BuildNamedDefMap() {
foreach (var v in defMap.Keys)
- if (defMap[v] != null)
+ if (defMap[v].Item1 != null)
BuildNamedDefFor(v);
}
- private class SubstDualisedDefVisitor : StandardVisitor {
+ private class SubstDefVisitor : Duplicator {
private VariableDefinitionAnalysis analysis;
- private VariableDualiser dualiser;
+ private string procName;
public bool isSubstitutable = true;
+ public bool isConstant = true;
- public SubstDualisedDefVisitor(VariableDefinitionAnalysis a, int id, string procName) {
+ public SubstDefVisitor(VariableDefinitionAnalysis a, string p) {
analysis = a;
- dualiser = new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName);
+ procName = p;
}
public override Expr VisitIdentifierExpr(IdentifierExpr expr) {
if (expr.Decl is Constant)
- return dualiser.VisitIdentifierExpr(expr);
- var varName = GPUVerifier.StripThreadIdentifier(expr.Decl.Name);
- Expr def;
+ return expr;
+ int id;
+ var varName = GPUVerifier.StripThreadIdentifier(expr.Decl.Name, out id);
+ VarDef def;
if (!analysis.namedDefMap.TryGetValue(varName, out def)) {
isSubstitutable = false;
return null;
}
- return (Expr)dualiser.Visit(def.Clone());
+ if (!def.Item2)
+ isConstant = false;
+ if (id == 0)
+ return def.Item1;
+ else
+ return (Expr)new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName).Visit(def.Item1.Clone());
}
}
- public Expr SubstDualisedDefinitions(Expr e, int id, string procName) {
- var v = new SubstDualisedDefVisitor(this, id, procName);
+ public Expr SubstDefinitions(Expr e, string procName, out bool isConstant) {
+ var v = new SubstDefVisitor(this, procName);
Expr result = (Expr)v.Visit(e.Clone());
+ isConstant = v.isConstant;
if (!v.isSubstitutable)
return null;
return result;
}
+ public Expr SubstDefinitions(Expr e, string procName) {
+ bool isConstant;
+ var result = SubstDefinitions(e, procName, out isConstant);
+ if (!isConstant)
+ return null;
+ return result;
+ }
+
public static VariableDefinitionAnalysis Analyse(GPUVerifier verifier, Implementation impl) {
var a = new VariableDefinitionAnalysis(verifier, impl);
a.Analyse();
diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs index 987574be..dcdb087f 100644 --- a/Source/VCGeneration/BlockPredicator.cs +++ b/Source/VCGeneration/BlockPredicator.cs @@ -77,10 +77,14 @@ public class BlockPredicator { // the first statement in the block. var assign = cmdSeq.Last(); cmdSeq.Truncate(cmdSeq.Length-1); - cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(pExpr, aCmd.Expr))); + aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr); + cmdSeq.Add(aCmd); + // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr))); cmdSeq.Add(assign); } else { - cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr))); + aCmd.Expr = Expr.Imp(p, aCmd.Expr); + cmdSeq.Add(aCmd); + // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr))); } } else if (cmd is AssumeCmd) { var aCmd = (AssumeCmd)cmd; @@ -114,15 +118,20 @@ public class BlockPredicator { var cCmd = (CallCmd)cmd; cCmd.Ins.Insert(0, p); cmdSeq.Add(cCmd); - } else if (cmd is StateCmd) { - var sCmd = (StateCmd)cmd; - var newCmdSeq = new CmdSeq(); - foreach (Cmd c in sCmd.Cmds) - PredicateCmd(newCmdSeq, c); - sCmd.Cmds = newCmdSeq; - cmdSeq.Add(sCmd); - } else { - Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString()); + } + else if (cmd is CommentCmd) { + // skip
+ }
+ else if (cmd is StateCmd) {
+ var sCmd = (StateCmd)cmd;
+ var newCmdSeq = new CmdSeq();
+ foreach (Cmd c in sCmd.Cmds)
+ PredicateCmd(newCmdSeq, c);
+ sCmd.Cmds = newCmdSeq;
+ cmdSeq.Add(sCmd);
+ }
+ else {
+ Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
} } @@ -298,13 +307,23 @@ public class BlockPredicator { dwf.InParams = new VariableSeq( (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>())) .ToArray()); - } - var impl = decl as Implementation; - if (impl != null) - new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation(); + }
+ try {
+ var impl = decl as Implementation;
+ if (impl != null)
+ new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();
+ }
+ catch (Program.IrreducibleLoopException) { } } } + public static void Predicate(Program p, Implementation impl) {
+ try {
+ new BlockPredicator(p, impl, false, false).PredicateImplementation();
+ }
+ catch (Program.IrreducibleLoopException) { } + } + } } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 373b685a..1c3fa979 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1968,6 +1968,26 @@ namespace VC { #endregion
}
+ public void DesugarCalls(Implementation impl) {
+ foreach (Block block in impl.Blocks) {
+ CmdSeq newCmds = new CmdSeq();
+ foreach (Cmd cmd in block.Cmds) {
+ SugaredCmd sugaredCmd = cmd as SugaredCmd;
+ if (sugaredCmd != null) {
+ StateCmd stateCmd = sugaredCmd.Desugaring as StateCmd;
+ foreach (Variable v in stateCmd.Locals) {
+ impl.LocVars.Add(v);
+ }
+ newCmds.AddRange(stateCmd.Cmds);
+ }
+ else {
+ newCmds.Add(cmd);
+ }
+ }
+ block.Cmds = newCmds;
+ }
+ }
+
public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)
{
Contract.Requires(impl != null);
@@ -2035,7 +2055,13 @@ namespace VC { EmitImpl(impl, true);
}
#endregion
-
+
+ if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining == 0) {
+ DesugarCalls(impl);
+ BlockPredicator.Predicate(program, impl);
+ impl.ComputePredecessorsForBlocks();
+ }
+
if (CommandLineOptions.Clo.LiveVariableAnalysis > 0) {
Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);
}
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index b70ff4d0..76e1ffa7 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -14,7 +14,7 @@ // that the specification can use mathematical sequences while the
// implementation uses a linked list.
-class Map<Key,Value> {
+class Map<Key(==),Value> {
ghost var Keys: seq<Key>;
ghost var Values: seq<Value>;
ghost var Repr: set<object>;
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index 383bccfd..2149df25 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -250,7 +250,7 @@ class WriterStream { -class Map<Key,Value> {
+class Map<Key(==),Value> {
var keys: seq<Key>;
var values: seq<Value>;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 5f80df86..7510363a 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -58,7 +58,6 @@ class C { Dafny program verifier finished with 0 verified, 0 errors
-------------------- TypeTests.dfy --------------------
-TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type
TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
@@ -88,11 +87,12 @@ TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)
TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)
-TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(91,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(116,4): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(117,7): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(93,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(117,4): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(118,7): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
36 resolution/type errors detected in TypeTests.dfy
@@ -719,33 +719,32 @@ Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of th Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)
-Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)
-Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
-Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
-Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
-Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
-Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
-Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
-Modules0.dfy(250,15): Error: unresolved identifier: X
-Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X
-Modules0.dfy(294,16): Error: member R does not exist in class B
-Modules0.dfy(294,6): Error: expected method call, found expression
-Modules0.dfy(317,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)
-Modules0.dfy(321,13): Error: arguments must have the same type (got Q_Imp.Node and Node)
-Modules0.dfy(322,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)
-Modules0.dfy(323,11): Error: Undeclared module name: Wazzup (did you forget a module import?)
-Modules0.dfy(324,17): Error: Undeclared class name Edon in module Q_Imp
-Modules0.dfy(326,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
-Modules0.dfy(327,30): Error: member Create does not exist in class Klassy
-Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts
-Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts
-Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts
-Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts
-Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context
-Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context
-37 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(52,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
+Modules0.dfy(52,12): Error: new can be applied only to reference types (got T)
+Modules0.dfy(57,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
+Modules0.dfy(73,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
+Modules0.dfy(74,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(84,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(108,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
+Modules0.dfy(247,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
+Modules0.dfy(256,13): Error: unresolved identifier: X
+Modules0.dfy(257,15): Error: member DoesNotExist does not exist in class X
+Modules0.dfy(299,16): Error: member R does not exist in class B
+Modules0.dfy(299,6): Error: expected method call, found expression
+Modules0.dfy(322,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)
+Modules0.dfy(326,13): Error: arguments must have the same type (got Q_Imp.Node and Node)
+Modules0.dfy(327,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)
+Modules0.dfy(328,11): Error: Undeclared module name: Wazzup (did you forget a module import?)
+Modules0.dfy(329,17): Error: Undeclared class name Edon in module Q_Imp
+Modules0.dfy(331,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
+Modules0.dfy(332,30): Error: member Create does not exist in class Klassy
+Modules0.dfy(143,11): Error: ghost variables are allowed only in specification contexts
+Modules0.dfy(157,11): Error: old expressions are allowed only in specification and ghost contexts
+Modules0.dfy(158,11): Error: fresh expressions are allowed only in specification and ghost contexts
+Modules0.dfy(159,11): Error: allocated expressions are allowed only in specification and ghost contexts
+Modules0.dfy(175,10): Error: match source expression 'tree' has already been used as a match source expression in this context
+Modules0.dfy(214,12): Error: match source expression 'l' has already been used as a match source expression in this context
+36 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
Modules1.dfy(74,16): Error: assertion violation
@@ -1328,6 +1327,17 @@ Dafny program verifier finished with 12 verified, 3 errors Dafny program verifier finished with 12 verified, 0 errors
+-------------------- EqualityTypes.dfy --------------------
+EqualityTypes.dfy(31,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
+EqualityTypes.dfy(32,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
+EqualityTypes.dfy(37,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes type parameters
+EqualityTypes.dfy(38,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes type parameters
+EqualityTypes.dfy(42,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality
+EqualityTypes.dfy(43,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
+EqualityTypes.dfy(63,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
+EqualityTypes.dfy(82,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)
+8 resolution/type errors detected in EqualityTypes.dfy
+
-------------------- SplitExpr.dfy --------------------
Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy new file mode 100644 index 00000000..251b2e2f --- /dev/null +++ b/Test/dafny0/EqualityTypes.dfy @@ -0,0 +1,89 @@ +module A {
+ datatype Explicit<T(==)> = Nil | Cons(set<T>, Explicit<T>);
+ datatype Inferred<T> = Nil | Cons(set<T>, Inferred<T>);
+
+ class C {
+ method M<T>(x: Explicit<T>)
+ method N<T>(x: Inferred<T>)
+ }
+}
+
+module B refines A {
+ class C {
+ method M<T>(x: Explicit<T>)
+ method N<T(==)>(x: Inferred<T>)
+ }
+}
+
+// ----------------------------
+
+module C {
+ type X(==);
+ type Y(==);
+}
+
+module D refines C {
+ class X { }
+ datatype Y = Red | Green | Blue;
+}
+
+module E refines C {
+ codatatype X = Next(int, X); // error: X requires equality and codatatypes don't got it
+ datatype Y = Nil | Something(Z) | More(Y, Y); // error: Y does not support equality
+ codatatype Z = Red | Green(X) | Blue;
+}
+
+module F refines C {
+ datatype X<T> = Nil | Cons(T, X<T>); // error: not allowed to add a type parameter to type X
+ class Y<T> { } // error: not allowed to add a type parameter to type Y
+}
+
+module G refines C {
+ datatype X = Nil | Next(Z, X); // error: X does not support equality
+ datatype Y = Nil | Something(Z) | More(Y, Y); // error: Y does not support equality
+ codatatype Z = Red | Green | Blue;
+}
+
+// ----------------------------
+
+module H {
+ datatype Dt<T> = Nil | Cons(T, Dt);
+
+ datatype BulkyList<T> = Nothing | Wrapper(T, BulkyListAux);
+ datatype BulkyListAux<T> = Kons(set<T>, BulkyListAuxAux);
+ datatype BulkyListAuxAux<T> = GoBack(BulkyList);
+
+ codatatype Stream<T> = Next(head: T, tail: Stream<T>);
+
+ method M<T(==)>(x: T)
+ { }
+ function method F<T>(x: BulkyList<T>, y: BulkyList<T>): int
+ { if x == y then 5 else 7 } // this equality is allowed
+ function method G<T>(x: Dt<T>, y: Dt<T>): int
+ { if x == y then 5 else 7 } // error: the equality is not allowed, because Dt<T> may not support equality
+ function method G'<T(==)>(x: Dt<T>, y: Dt<T>): int
+ { if x == y then 5 else 7 } // fine
+
+ method Caller0(b: BulkyList, y: int) {
+ match (b) {
+ case Nothing =>
+ case Wrapper(t, bla) =>
+ var u;
+ if (y < 100) { u := t; }
+ // The following call is allowed, because it will be inferred that
+ // 'u' is of a type that supports equality
+ M(u);
+ }
+ }
+ method Caller1(d: Dt) {
+ match (d) {
+ case Nil =>
+ case Cons(t, rest) =>
+ M(t); // error: t may be of a type that does not support equality
+ }
+ }
+ method Caller2(co: Stream) {
+ var d := Cons(co, Nil);
+ Caller1(d); // case in point for the error in Caller1
+ }
+}
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index cc66c3c1..80ac7eef 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -45,9 +45,12 @@ module A imports N, M { // Note, this has the effect of importing two different { x }
method M(x: T) // error: use of the ambiguous name T
returns (y: T) // error: use of the ambiguous name T
- { var g := new T; } // error: use of the ambiguous name T
}
}
+module A' imports N, M {
+ method M()
+ { var g := new T; } // error: use of the ambiguous name T
+}
module B0 imports A {
class BadUse {
@@ -241,15 +244,17 @@ module BTr imports ATr { module CTr imports BTr {
class Z {
var b: Y; // fine
- var a: X; // error: imports don't reach name name X explicitly
- method P() {
- var y := new Y;
- var x := y.N(); // this is allowed and will correctly infer the type of x to
- // be X, but X could not have been mentioned explicitly
- var q := x.M();
- var r := X.Q(); // error: X is not in scope
- var s := x.DoesNotExist(); // error: method not declared in class X
- }
+ var a: X; // error: imports don't reach name X explicitly
+ }
+}
+module CTs imports BTr {
+ method P() {
+ var y := new Y;
+ var x := y.N(); // this is allowed and will correctly infer the type of x to
+ // be X, but X could not have been mentioned explicitly
+ var q := x.M();
+ var r := X.Q(); // error: X is not in scope
+ var s := x.DoesNotExist(); // error: method not declared in class X
}
}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index e8b618d7..40df1135 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -294,7 +294,7 @@ method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int) assert x != y;
}
-method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)
+method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int)
requires 0 <= N && N <= |a|;
requires exists k | 0 <= k && k < N :: a[k] == y;
ensures forall k | 0 <= k && k < N :: a[k] == y; // error
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 1482dc24..bf3702ae 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -92,8 +92,8 @@ class Termination { ensures a == List.Cons(val, b);
{
match a {
- case Cons(v, r) => val := v; b := r;
- }
+ case Cons(v, r) => val := v; b := r;
+ }
}
}
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index d6804661..cb9b5660 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -1,11 +1,11 @@ -class C<U> {
+class C<U(==)> {
method M<T>(x: T, u: U) returns (y: T)
ensures x == y && u == u;
{
y := x;
}
- function method F<X>(x: X, u: U): bool
+ function method F<X(==)>(x: X, u: U): bool
{
x == x && u == u
}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 8434f06c..2dea7a52 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -86,7 +86,8 @@ method ArrayRangeAssignments(a: array<C>, c: C) // --------------------- tests of restrictions on subranges (nat)
-method K(s: set<nat>) { // error: not allowed to instantiate 'set' with 'nat'
+method K() {
+ var s: set<nat>; // error: not allowed to instantiate 'set' with 'nat'
var d: MutuallyRecursiveDataType<nat>; // error: not allowed to instantiate with 'nat'
var a := new nat[100]; // error: not allowed the type array<nat>
var b := new nat[100,200]; // error: not allowed the type array2<nat>
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index ac7c8aed..d352cf44 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -17,7 +17,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
TypeParameters.dfy Datatypes.dfy Coinductive.dfy Corecursion.dfy
- TypeAntecedents.dfy NoTypeArgs.dfy SplitExpr.dfy
+ TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy
LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index 21b895aa..4c761671 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -10,7 +10,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool }
method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
- requires (exists c :: IsCelebrity(c, people));
+ requires exists c :: IsCelebrity(c, people);
ensures r == c;
{
var cc; assume cc == c; // this line essentially converts ghost c to non-ghost cc
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index c8419890..c78d5e81 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -1,6 +1,6 @@ // ultra filter
-class UltraFilter<G> {
+class UltraFilter<G(==)> {
static function IsFilter(f: set<set<G>>, S: set<G>): bool
{
(forall A, B :: A in f && A <= B ==> B in f) &&
diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy index a7512486..af67ee92 100644 --- a/Test/dafny2/MajorityVote.dfy +++ b/Test/dafny2/MajorityVote.dfy @@ -31,6 +31,10 @@ // choice, if there is such a choice, and then passes in that choice as the ghost parameter K
// to the main algorithm. Neat, huh?
+// Language comment:
+// The "(==)" that sits after some type parameters in this program says that the actual
+// type argument must support equality.
+
// Advanced remark:
// There is a subtle situation in the verification of DetermineElection. Suppose the type
// parameter Candidate denotes some type whose instances depend on which object are
@@ -47,7 +51,7 @@ // to the Count function. Alternatively, one could have added the antecedent "c in a" or
// "old(allocated(c))" to the "forall c" quantification in the postcondition of DetermineElection.
-function method Count<T>(a: seq<T>, s: int, t: int, x: T): int
+function method Count<T(==)>(a: seq<T>, s: int, t: int, x: T): int
requires 0 <= s <= t <= |a|;
ensures Count(a, s, t, x) == 0 || x in a;
{
@@ -57,7 +61,7 @@ function method Count<T>(a: seq<T>, s: int, t: int, x: T): int // Here is the first version of the algorithm, the one that assumes there is a majority choice.
-method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)
+method FindWinner<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)
requires 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes
ensures k == K; // find K
{
@@ -93,7 +97,7 @@ method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: // Here is the second version of the program, the one that also computes whether or not
// there is a majority choice.
-method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)
+method DetermineElection<Candidate(==)>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)
ensures hasWinner ==> 2 * Count(a, 0, |a|, cand) > |a|;
ensures !hasWinner ==> forall c :: 2 * Count(a, 0, |a|, c) <= |a|;
{
@@ -107,7 +111,7 @@ method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, // antecedent "hasWinner ==>" and the two checks for no-more-votes that may result in a "return"
// statement.
-method SearchForWinner<Candidate>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)
+method SearchForWinner<Candidate(==)>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)
requires hasWinner ==> 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes
ensures hasWinner ==> k == K; // find K
{
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy index 5153b053..4373136b 100644 --- a/Test/vstte2012/BreadthFirstSearch.dfy +++ b/Test/vstte2012/BreadthFirstSearch.dfy @@ -1,4 +1,4 @@ -class BreadthFirstSearch<Vertex>
+class BreadthFirstSearch<Vertex(==)>
{
// The following function is left uninterpreted (for the purpose of the
// verification problem, it can be thought of as a parameter to the class)
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 051d60f4..af789102 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -42,6 +42,7 @@ % the following isn't actually Dafny, but it gives the option to produce nicer latex
{<<}{$\langle$}1
{>>}{$\rangle$}1
+ {(==)}{${}^{(=)}$}2
{...}{$\ldots$}1
{\\alpha}{$\alpha$}1
{\\beta}{$\beta$}1
diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log index 93cdd92c..2f3d4b16 100644 --- a/_admin/Boogie/aste/summary.log +++ b/_admin/Boogie/aste/summary.log @@ -1,15 +1,15 @@ -# Aste started: 2012-06-08 07:00:06
+# Aste started: 2012-06-23 07:00:02
# Host id: Boogiebox
# Configuration: boogie.cfg
# Task: aste.tasks.boogie.FullBuild
-# [2012-06-08 07:02:11] SpecSharp revision: b46b99e00a7e
-# [2012-06-08 07:02:11] SscBoogie revision: b46b99e00a7e
-# [2012-06-08 07:03:22] Boogie revision: 4c147e39859e
-[2012-06-08 07:05:15] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build
+# [2012-06-23 07:01:14] SpecSharp revision: 4c8cfe160e05
+# [2012-06-23 07:01:14] SscBoogie revision: 4c8cfe160e05
+# [2012-06-23 07:02:30] Boogie revision: de93d0fe3e85
+[2012-06-23 07:04:21] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com SpecSharp.sln /Project "Checkin Tests" /Build
1>corflags : warning CF011: The specified file is strong name signed. Using /Force will invalidate the signature of this image and will require the assembly to be resigned.
warning CF011: The specified file is strong name signed. Using /Force will invalidate the signature of this image and will require the assembly to be resigned.
-[2012-06-08 07:06:42] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
+[2012-06-23 07:05:51] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()
@@ -41,5 +41,5 @@ warning CS0162: Unreachable code detected
warning CC1032: Method 'Microsoft.Boogie.Houdini.InlineRequiresVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)' overrides 'Microsoft.Boogie.StandardVisitor.VisitCmdSeq(Microsoft.Boogie.CmdSeq)', thus cannot add Requires.
warning CC1032: Method 'Microsoft.Boogie.Houdini.FreeRequiresVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)' overrides 'Microsoft.Boogie.StandardVisitor.VisitAssertRequiresCmd(Microsoft.Boogie.AssertRequiresCmd)', thus cannot add Requires.
-[2012-06-08 08:03:55] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
-# [2012-06-08 08:04:37] Released nightly of Boogie
+[2012-06-23 08:09:55] 0 out of 33 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
+# [2012-06-23 08:10:37] Released nightly of Boogie
|