diff options
28 files changed, 700 insertions, 617 deletions
@@ -8,3 +8,4 @@ e57f596b36edd27f66ff7400a6610034ce67d19d emicvccbld_build_2.1.30905.0 8b7a180291a5ecb7d1ffa0dbc3483cc4f7685064 emicvccbld_build_2.1.31020.0 f59d45429b672bb429d26e1aff6e9df1d9def6b5 emicvccbld_build_2.1.31022.0 f3b3df39e9877fb2b3fde172f300f995689e6402 emicvccbld_build_2.1.31028.0 +f5c14add09d2f57402c94574eeef490d900d58e8 emicvccbld_build_2.1.31109.0 diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 1fe21204..c954c019 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -326,6 +326,14 @@ axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref :: axiom (forall h: HeapType, i: int, v: BoxType, a: ref ::
{ Seq#FromArray(update(h, a, IndexField(i), v), a) }
0 <= i && i < array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) );
+/**** Someday:
+axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a) }
+ $IsGoodHeap(h) &&
+ a != null && read(h, a, alloc) && dtype(a) == class.array && TypeParams(a, 0) == class.bool
+ ==>
+ (forall i: int :: { Seq#Index(Seq#FromArray(h, a), i) }
+ 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> $IsCanonicalBoolBox(Seq#Index(Seq#FromArray(h, a), i))));
+****/
// Commutability of Take and Drop with Update.
axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
@@ -379,6 +387,7 @@ const unique class.bool: ClassName; const unique class.set: ClassName;
const unique class.seq: ClassName;
const unique class.multiset: ClassName;
+const unique class.array: ClassName;
function /*{:never_pattern true}*/ dtype(ref): ClassName;
function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a4d99bd0..2d3ddcca 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2674,6 +2674,11 @@ namespace Microsoft.Dafny { 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) {
+ if (!UnifyTypes(e.E0.Type, new DatatypeProxy())) {
+ Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
+ }
+ expr.Type = Type.Bool;
} else {
bool err = false;
if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true))) {
@@ -3768,7 +3773,7 @@ namespace Microsoft.Dafny { return BinaryExpr.ResolvedOpcode.Disjoint;
}
case BinaryExpr.Opcode.Lt:
- if (operandType.IsDatatype) {
+ if (operandType.IsDatatype || operandType is DatatypeProxy) {
return BinaryExpr.ResolvedOpcode.RankLt;
} else if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.ProperSubset;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 2cc15c5a..e455561a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -54,6 +54,7 @@ namespace Microsoft.Dafny { public readonly Bpl.Type DtCtorId;
public readonly Bpl.Expr Null;
private readonly Bpl.Constant allocField;
+ public readonly Bpl.Constant ClassDotArray;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(RefType != null);
@@ -71,6 +72,7 @@ namespace Microsoft.Dafny { Contract.Invariant(DtCtorId != null);
Contract.Invariant(Null != null);
Contract.Invariant(allocField != null);
+ Contract.Invariant(ClassDotArray != null);
}
@@ -116,7 +118,7 @@ namespace Microsoft.Dafny { Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,
- Bpl.Constant allocField) {
+ Bpl.Constant allocField, Bpl.Constant classDotArray) {
#region Non-null preconditions on parameters
Contract.Requires(refType != null);
Contract.Requires(boxType != null);
@@ -130,6 +132,7 @@ namespace Microsoft.Dafny { Contract.Requires(datatypeType != null);
Contract.Requires(dtCtorId != null);
Contract.Requires(allocField != null);
+ Contract.Requires(classDotArray != null);
#endregion
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
@@ -148,6 +151,7 @@ namespace Microsoft.Dafny { this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());
this.allocField = allocField;
this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);
+ this.ClassDotArray = classDotArray;
}
}
@@ -171,6 +175,7 @@ namespace Microsoft.Dafny { Bpl.TypeCtorDecl tickType = null;
Bpl.GlobalVariable heap = null;
Bpl.Constant allocField = null;
+ Bpl.Constant classDotArray = null;
foreach (var d in prog.TopLevelDeclarations) {
if (d is Bpl.TypeCtorDecl) {
Bpl.TypeCtorDecl dt = (Bpl.TypeCtorDecl)d;
@@ -203,6 +208,8 @@ namespace Microsoft.Dafny { Bpl.Constant c = (Bpl.Constant)d;
if (c.Name == "alloc") {
allocField = c;
+ } else if (c.Name == "class.array") {
+ classDotArray = c;
}
} else if (d is Bpl.GlobalVariable) {
Bpl.GlobalVariable v = (Bpl.GlobalVariable)d;
@@ -241,10 +248,12 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of $Heap");
} else if (allocField == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");
+ } else if (classDotArray == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of class.array");
} else {
return new PredefinedDecls(refType, boxType, tickType,
setTypeCtor, multiSetTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
- allocField);
+ allocField, classDotArray);
}
return null;
}
@@ -520,7 +529,11 @@ namespace Microsoft.Dafny { {
Contract.Requires(sink != null && predef != null);
Contract.Requires(c != null);
- sink.TopLevelDeclarations.Add(GetClass(c));
+ if (c.Name == "array") {
+ classes.Add(c, predef.ClassDotArray);
+ } else {
+ sink.TopLevelDeclarations.Add(GetClass(c));
+ }
foreach (MemberDecl member in c.Members) {
if (member is Field) {
@@ -1514,6 +1527,25 @@ namespace Microsoft.Dafny { // }
// Here go the postconditions (termination checks included, but no reads checks)
StmtListBuilder postCheckBuilder = new StmtListBuilder();
+ // Assume the type returned by the call itself respects its type (this matter if the type is "nat", for example)
+ {
+ var args = new Bpl.ExprSeq();
+ args.Add(etran.HeapExpr);
+ if (!f.IsStatic) {
+ args.Add(new Bpl.IdentifierExpr(f.tok, etran.This, predef.RefType));
+ }
+ foreach (var p in f.Formals) {
+ args.Add(new Bpl.IdentifierExpr(p.tok, p.UniqueName, TrType(p.Type)));
+ }
+ Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, FunctionName(f, 1), TrType(f.ResultType));
+ Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);
+
+ var wh = GetWhereClause(f.tok, funcAppl, f.ResultType, etran);
+ if (wh != null) {
+ postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, wh));
+ }
+ }
+ // Now for the ensures clauses
foreach (Expression p in f.Ens) {
CheckWellformed(p, new WFOptions(f, f, false), locals, postCheckBuilder, etran);
// assume the postcondition for the benefit of checking the remaining postconditions
@@ -3109,7 +3141,7 @@ namespace Microsoft.Dafny { } else if (type.IsRefType) {
// object and class types translate to ref
return predef.RefType;
- } else if (type.IsDatatype) {
+ } else if (type.IsDatatype || type is DatatypeProxy) {
return predef.DatatypeType;
} else if (type is SetType) {
return predef.SetType(Token.NoToken, predef.BoxType);
@@ -4513,13 +4545,14 @@ namespace Microsoft.Dafny { Bpl.Expr xSubT = Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, x, t), Bpl.Expr.Literal(0));
Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t);
+ Bpl.Expr isGoodMultiset = FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x);
Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran);
if (wh != null) {
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
- return Bpl.Expr.And(FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, Bpl.Type.Bool, x),
- new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh)));
+ var q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));
+ isGoodMultiset = Bpl.Expr.And(isGoodMultiset, q);
}
- return FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x);
+ return isGoodMultiset;
} else if (type is SeqType) {
SeqType st = (SeqType)type;
// (forall i: int :: { Seq#Index(x,i) }
diff --git a/Source/GPUVerify/AccessCollector.cs b/Source/GPUVerify/AccessCollector.cs index 43491460..42ca5cc8 100644 --- a/Source/GPUVerify/AccessCollector.cs +++ b/Source/GPUVerify/AccessCollector.cs @@ -8,13 +8,11 @@ namespace GPUVerify {
abstract class AccessCollector : StandardVisitor
{
- protected ICollection<Variable> GlobalVariables;
- protected ICollection<Variable> TileStaticVariables;
+ protected INonLocalState NonLocalState;
- public AccessCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public AccessCollector(INonLocalState NonLocalState)
{
- this.GlobalVariables = GlobalVariables;
- this.TileStaticVariables = TileStaticVariables;
+ this.NonLocalState = NonLocalState;
}
protected void MultiDimensionalMapError()
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs index 9e7ba32c..2f08477b 100644 --- a/Source/GPUVerify/CommandLineOptions.cs +++ b/Source/GPUVerify/CommandLineOptions.cs @@ -14,10 +14,7 @@ namespace GPUVerify public static List<string> inputFiles = new List<string>();
public static string outputFile = null;
- public static string formulaSkeletonsFile = null;
- public static string formulasFile = null;
- public static bool NewRaceDetectionMethod = false;
public static bool OnlyDivergence = false;
public static bool FullAbstraction;
public static bool Inference;
@@ -49,6 +46,12 @@ namespace GPUVerify switch (beforeColon)
{
+ case "-help":
+ case "/help":
+ case "-?":
+ case "/?":
+ return -1;
+
case "-print":
case "/print":
if (!hasColonArgument)
@@ -60,34 +63,6 @@ namespace GPUVerify outputFile = afterColon;
break;
- case "-generateFormulaSkeletons":
- case "/generateFormulaSkeletons":
- if (!hasColonArgument)
- {
- Console.WriteLine("Error: filename expected after " + beforeColon + " argument");
- Environment.Exit(1);
- }
- Debug.Assert(afterColon != null);
- formulaSkeletonsFile = afterColon;
- break;
-
- case "-formulas":
- case "/formulas":
- if (!hasColonArgument)
- {
- Console.WriteLine("Error: filename expected after " + beforeColon + " argument");
- Environment.Exit(1);
- }
- Debug.Assert(afterColon != null);
- formulasFile = afterColon;
- break;
-
- case "-newRaceDetectionMethod":
- case "/newRaceDetectionMethod":
- NewRaceDetectionMethod = true;
-
- break;
-
case "-onlyDivergence":
case "/onlyDivergence":
OnlyDivergence = true;
@@ -163,5 +138,35 @@ namespace GPUVerify return 0;
}
+ private static bool printedHelp = false;
+
+ public static void Usage()
+ {
+ // Ensure that we only print the help message once
+ if (printedHelp)
+ {
+ return;
+ }
+ printedHelp = true;
+
+ Console.WriteLine(@"GPUVerify: usage: GPUVerify [ option ... ] [ filename ... ]
+ where <option> is one of
+
+ /help : this message
+ /fullAbstraction : apply full state abstraction
+ /onlyDivergence : only check for divergence-freedom, not race-freedom
+ /symmetry : apply symmetry breaking
+ /eager : check races eagerly, rather than waiting for barrier
+ /inference:file : use automatic invariant inference. Optional file can include manually supplied candidates
+ /raceCheckingContract : try to infer race-freedom contracts for procedures
+ /setEncoding : check races using set encoding
+ /divided : check individual pairs of possibly racing statements separately
+ /dividedArray : check races on arrays one at a time
+ /dividedElement : ???
+
+");
+ }
+
+
}
}
diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs index 78ace202..74bdaa5e 100644 --- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs @@ -89,9 +89,10 @@ namespace GPUVerify verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);
}
- protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite)
+ protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog)
{
- IdentifierExprSeq newVars = new IdentifierExprSeq();
+ ModifiedAtLog = new IdentifierExprSeq();
+ ResetAtBarrier = new IdentifierExprSeq();
Variable AccessHasOccurred = new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));
@@ -100,7 +101,8 @@ namespace GPUVerify verifier.HalfDualisedVariableNames.Add(AccessHasOccurred.Name);
}
- newVars.Add(new IdentifierExpr(v.tok, AccessHasOccurred));
+ ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessHasOccurred));
+ ResetAtBarrier.Add(new IdentifierExpr(v.tok, AccessHasOccurred));
verifier.Program.TopLevelDeclarations.Add(AccessHasOccurred);
if (v.TypedIdent.Type is MapType)
@@ -116,7 +118,7 @@ namespace GPUVerify verifier.HalfDualisedVariableNames.Add(AccessOffsetX.Name);
}
- newVars.Add(new IdentifierExpr(v.tok, AccessOffsetX));
+ ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetX));
verifier.Program.TopLevelDeclarations.Add(AccessOffsetX);
if (mt.Result is MapType)
@@ -132,7 +134,7 @@ namespace GPUVerify verifier.HalfDualisedVariableNames.Add(AccessOffsetY.Name);
}
- newVars.Add(new IdentifierExpr(v.tok, AccessOffsetY));
+ ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetY));
verifier.Program.TopLevelDeclarations.Add(AccessOffsetY);
if (mt2.Result is MapType)
@@ -149,19 +151,15 @@ namespace GPUVerify verifier.HalfDualisedVariableNames.Add(AccessOffsetZ.Name);
}
- newVars.Add(new IdentifierExpr(v.tok, AccessOffsetZ));
+ ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetZ));
verifier.Program.TopLevelDeclarations.Add(AccessOffsetZ);
}
}
}
- foreach (IdentifierExpr e in newVars)
- {
- // TODO: add modiies to every procedure that calls BARRIER
- verifier.KernelProcedure.Modifies.Add(e);
- }
}
+
private static AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs)
{
List<AssignLhs> lhss = new List<AssignLhs>();
@@ -179,7 +177,6 @@ namespace GPUVerify List<AssignLhs> lhss = new List<AssignLhs>();
List<Expr> rhss = new List<Expr>();
- verifier.BarrierProcedure.Modifies.Add(AccessOccurred1);
lhss.Add(new SimpleAssignLhs(tok, AccessOccurred1));
rhss.Add(Expr.False);
@@ -187,7 +184,6 @@ namespace GPUVerify {
lhss.Add(new SimpleAssignLhs(tok, AccessOccurred2));
rhss.Add(Expr.False);
- verifier.BarrierProcedure.Modifies.Add(AccessOccurred2);
}
bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 1aac817c..25974225 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -19,18 +19,13 @@ namespace GPUVerify public Implementation KernelImplementation;
public Procedure BarrierProcedure;
- public ICollection<Variable> TileStaticVariables = new List<Variable>();
- public ICollection<Variable> GlobalVariables = new List<Variable>();
+ public INonLocalState NonLocalState = new NonLocalStateLists();
private HashSet<string> ReservedNames = new HashSet<string>();
internal HashSet<string> HalfDualisedProcedureNames = new HashSet<string>();
internal HashSet<string> HalfDualisedVariableNames = new HashSet<string>();
- private static int WhileLoopCounter;
- private static int IfCounter;
- private static HashSet<Microsoft.Boogie.Type> RequiredHavocVariables;
-
private int TempCounter = 0;
private int invariantGenerationCounter;
@@ -165,11 +160,11 @@ namespace GPUVerify {
if (QKeyValue.FindBoolAttribute(D.Attributes, "tile_static"))
{
- TileStaticVariables.Add(D as Variable);
+ NonLocalState.getTileStaticVariables().Add(D as Variable);
}
else
{
- GlobalVariables.Add(D as Variable);
+ NonLocalState.getGlobalVariables().Add(D as Variable);
}
}
}
@@ -296,16 +291,6 @@ namespace GPUVerify // TODO!
}
- internal ICollection<Variable> GetTileStaticVariables()
- {
- return TileStaticVariables;
- }
-
- internal ICollection<Variable> GetGlobalVariables()
- {
- return GlobalVariables;
- }
-
internal void preProcess()
{
RemoveElseIfs();
@@ -331,7 +316,7 @@ namespace GPUVerify AbstractSharedState();
- MakeKerenelPredicated();
+ MakeKernelPredicated();
MakeKernelDualised();
@@ -399,7 +384,7 @@ namespace GPUVerify private void AddEagerRaceChecking()
{
- foreach(Variable v in GlobalVariables)
+ foreach(Variable v in NonLocalState.getAllNonLocalVariables())
{
foreach (Declaration d in Program.TopLevelDeclarations)
{
@@ -425,32 +410,6 @@ namespace GPUVerify }
}
}
- foreach (Variable v in TileStaticVariables)
- {
- foreach (Declaration d in Program.TopLevelDeclarations)
- {
- if (!(d is Implementation))
- {
- continue;
- }
-
- Implementation impl = d as Implementation;
-
- if (impl.Name.Equals("_LOG_READ_" + v.Name) || impl.Name.Equals("_LOG_WRITE_" + v.Name))
- {
- BigBlock bb = new BigBlock(v.tok, "__CheckForRaces", new CmdSeq(), null, null);
- RaceInstrumenter.CheckForRaces(v.tok, bb, v);
- StmtList newStatements = new StmtList(new List<BigBlock>(), v.tok);
-
- foreach (BigBlock bb2 in impl.StructuredStmts.BigBlocks)
- {
- newStatements.BigBlocks.Add(bb2);
- }
- newStatements.BigBlocks.Add(bb);
- impl.StructuredStmts = newStatements;
- }
- }
- }
}
private void ComputeInvariant()
@@ -735,12 +694,7 @@ namespace GPUVerify if (!CommandLineOptions.FullAbstraction)
{
- foreach (Variable v in GlobalVariables)
- {
- AddEqualityCandidateInvariant(wc, LoopPredicate, v);
- }
-
- foreach (Variable v in TileStaticVariables)
+ foreach (Variable v in NonLocalState.getAllNonLocalVariables())
{
AddEqualityCandidateInvariant(wc, LoopPredicate, v);
}
@@ -855,21 +809,23 @@ namespace GPUVerify return true;
}
+
+
public Microsoft.Boogie.Type GetTypeOfIdX()
{
- Contract.Assert(_X != null);
+ Contract.Requires(_X != null);
return _X.TypedIdent.Type;
}
public Microsoft.Boogie.Type GetTypeOfIdY()
{
- Contract.Assert(_Y != null);
+ Contract.Requires(_Y != null);
return _Y.TypedIdent.Type;
}
public Microsoft.Boogie.Type GetTypeOfIdZ()
{
- Contract.Assert(_Z != null);
+ Contract.Requires(_Z != null);
return _Z.TypedIdent.Type;
}
@@ -1164,11 +1120,7 @@ namespace GPUVerify {
BigBlock havocSharedState = new BigBlock(tok, "__HavocSharedState", new CmdSeq(), null, null);
bigblocks.Add(havocSharedState);
- foreach (Variable v in GlobalVariables)
- {
- HavocAndAssumeEquality(tok, havocSharedState, v);
- }
- foreach (Variable v in TileStaticVariables)
+ foreach (Variable v in NonLocalState.getAllNonLocalVariables())
{
HavocAndAssumeEquality(tok, havocSharedState, v);
}
@@ -1219,35 +1171,18 @@ namespace GPUVerify IdentifierExpr v1 = new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable));
IdentifierExpr v2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable));
- bb.simpleCmds.Add(new HavocCmd(tok, new IdentifierExprSeq(new IdentifierExpr[] { v1, v2 })));
+ IdentifierExprSeq ModifiedVars = new IdentifierExprSeq(new IdentifierExpr[] { v1, v2 });
+ bb.simpleCmds.Add(new HavocCmd(tok, ModifiedVars));
bb.simpleCmds.Add(new AssumeCmd(tok, Expr.Eq(v1, v2)));
- BarrierProcedure.Modifies.Add(v1);
- BarrierProcedure.Modifies.Add(v2);
-
- foreach (Declaration d in Program.TopLevelDeclarations)
- {
- if (d is Implementation)
- {
- Implementation impl = d as Implementation;
- if (CallsBarrier(impl))
- {
- Procedure proc = impl.Proc;
- if (!ModifiesSetContains(proc.Modifies, v1))
- {
- Debug.Assert(!ModifiesSetContains(proc.Modifies, v2));
- proc.Modifies.Add(v1);
- proc.Modifies.Add(v2);
- }
- }
- }
- }
+ HashSet<string> MayCallBarrier = GetProceduresThatIndirectlyCallProcedure(BarrierProcedure.Name);
+ ExtendModifiesSetOfProcedures(ModifiedVars, MayCallBarrier);
}
- private bool ModifiesSetContains(IdentifierExprSeq seq, IdentifierExpr v)
+ internal static bool ModifiesSetContains(IdentifierExprSeq Modifies, IdentifierExpr v)
{
- foreach (IdentifierExpr ie in seq)
+ foreach (IdentifierExpr ie in Modifies)
{
if (ie.Name.Equals(v.Name))
{
@@ -1257,7 +1192,7 @@ namespace GPUVerify return false;
}
- private bool CallsBarrier(Implementation impl)
+/* private bool CallsBarrier(Implementation impl)
{
return CallsBarrier(impl.StructuredStmts);
}
@@ -1292,7 +1227,7 @@ namespace GPUVerify Debug.Assert(bb.ec == null);
return false;
}
- }
+ }*/
private void AbstractSharedState()
{
@@ -1305,7 +1240,7 @@ namespace GPUVerify foreach (Declaration d in Program.TopLevelDeclarations)
{
- if (d is Variable && GlobalVariables.Contains(d as Variable) || TileStaticVariables.Contains(d as Variable))
+ if (d is Variable && NonLocalState.Contains(d as Variable))
{
continue;
}
@@ -1334,7 +1269,7 @@ namespace GPUVerify foreach (IdentifierExpr e in proc.Modifies)
{
- if (!(GlobalVariables.Contains(e.Decl) || TileStaticVariables.Contains(e.Decl)))
+ if (!NonLocalState.Contains(e.Decl))
{
NewModifies.Add(e);
}
@@ -1350,10 +1285,8 @@ namespace GPUVerify foreach (Variable v in impl.LocVars)
{
- if (!TileStaticVariables.Contains(v))
- {
- NewLocVars.Add(v);
- }
+ Debug.Assert(!NonLocalState.getTileStaticVariables().Contains(v));
+ NewLocVars.Add(v);
}
impl.LocVars = NewLocVars;
@@ -1389,7 +1322,7 @@ namespace GPUVerify Debug.Assert(assign.Rhss.Count == 1);
AssignLhs lhs = assign.Lhss[0];
Expr rhs = assign.Rhss[0];
- ReadCollector rc = new ReadCollector(GlobalVariables, TileStaticVariables);
+ ReadCollector rc = new ReadCollector(NonLocalState);
rc.Visit(rhs);
if (rc.accesses.Count > 0)
{
@@ -1398,7 +1331,7 @@ namespace GPUVerify continue;
}
- WriteCollector wc = new WriteCollector(GlobalVariables, TileStaticVariables);
+ WriteCollector wc = new WriteCollector(NonLocalState);
wc.Visit(lhs);
if (wc.GetAccess() != null)
{
@@ -1642,7 +1575,7 @@ namespace GPUVerify {
Expr e = call.Ins[i];
- while (NonLocalAccessCollector.ContainsNonLocalAccess(e, GlobalVariables, TileStaticVariables))
+ while (NonLocalAccessCollector.ContainsNonLocalAccess(e, NonLocalState))
{
AssignCmd assignToTemp;
LocalVariable tempDecl;
@@ -1666,7 +1599,9 @@ namespace GPUVerify AssignLhs lhs = assign.Lhss.ElementAt(0);
Expr rhs = assign.Rhss.ElementAt(0);
- if (!NonLocalAccessCollector.ContainsNonLocalAccess(rhs, GlobalVariables, TileStaticVariables) || (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, GlobalVariables, TileStaticVariables) && NonLocalAccessCollector.IsNonLocalAccess(rhs, GlobalVariables, TileStaticVariables)))
+ if (!NonLocalAccessCollector.ContainsNonLocalAccess(rhs, NonLocalState) ||
+ (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, NonLocalState) &&
+ NonLocalAccessCollector.IsNonLocalAccess(rhs, NonLocalState)))
{
result.simpleCmds.Add(c);
}
@@ -1703,7 +1638,7 @@ namespace GPUVerify if (bb.ec is WhileCmd)
{
WhileCmd WhileCommand = bb.ec as WhileCmd;
- while (NonLocalAccessCollector.ContainsNonLocalAccess(WhileCommand.Guard, GlobalVariables, TileStaticVariables))
+ while (NonLocalAccessCollector.ContainsNonLocalAccess(WhileCommand.Guard, NonLocalState))
{
AssignCmd assignToTemp;
LocalVariable tempDecl;
@@ -1716,8 +1651,8 @@ namespace GPUVerify else if (bb.ec is IfCmd)
{
IfCmd IfCommand = bb.ec as IfCmd;
- Debug.Assert(IfCommand.elseIf == null); // We don't handle else if yet
- while (NonLocalAccessCollector.ContainsNonLocalAccess(IfCommand.Guard, GlobalVariables, TileStaticVariables))
+ Debug.Assert(IfCommand.elseIf == null); // "else if" must have been eliminated by this phase
+ while (NonLocalAccessCollector.ContainsNonLocalAccess(IfCommand.Guard, NonLocalState))
{
AssignCmd assignToTemp;
LocalVariable tempDecl;
@@ -1742,7 +1677,7 @@ namespace GPUVerify private Expr PullOutNonLocalAccessesIntoTemps(BigBlock result, Expr e, Implementation impl)
{
- while (NonLocalAccessCollector.ContainsNonLocalAccess(e, GlobalVariables, TileStaticVariables))
+ while (NonLocalAccessCollector.ContainsNonLocalAccess(e, NonLocalState))
{
AssignCmd assignToTemp;
LocalVariable tempDecl;
@@ -1755,7 +1690,7 @@ namespace GPUVerify private Expr ExtractLocalAccessToTemp(Expr rhs, out AssignCmd tempAssignment, out LocalVariable tempDeclaration)
{
- NonLocalAccessExtractor extractor = new NonLocalAccessExtractor(TempCounter, GlobalVariables, TileStaticVariables);
+ NonLocalAccessExtractor extractor = new NonLocalAccessExtractor(TempCounter, NonLocalState);
TempCounter++;
rhs = extractor.VisitExpr(rhs);
tempAssignment = extractor.Assignment;
@@ -1860,7 +1795,7 @@ namespace GPUVerify return result;
}
- private void MakeKerenelPredicated()
+ private void MakeKernelPredicated()
{
foreach (Declaration d in Program.TopLevelDeclarations)
{
@@ -1882,38 +1817,12 @@ namespace GPUVerify }
else if (d is Implementation)
{
- MakePredicated(d as Implementation, d != KernelImplementation);
- }
- }
+ new Predicator(d != KernelImplementation).transform(d as Implementation);
- }
-
- private void MakePredicated(Implementation impl, bool AddPredicateParameter)
- {
- Expr Predicate;
-
- if (AddPredicateParameter)
- {
- VariableSeq NewIns = new VariableSeq();
- Variable PredicateVariable = new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P", Microsoft.Boogie.Type.Bool));
- NewIns.Add(PredicateVariable);
- foreach (Variable v in impl.InParams)
- {
- NewIns.Add(v);
+ //MakePredicated(d as Implementation, d != KernelImplementation);
}
- impl.InParams = NewIns;
- Predicate = new IdentifierExpr(impl.tok, PredicateVariable);
- }
- else
- {
- Predicate = Expr.True;
}
- WhileLoopCounter = 0;
- IfCounter = 0;
- RequiredHavocVariables = new HashSet<Microsoft.Boogie.Type>();
- impl.StructuredStmts = MakePredicated(impl.StructuredStmts, Predicate, null);
- AddPredicateLocalVariables(impl);
}
private StmtList MakeDual(StmtList stmtList, bool HalfDualise)
@@ -2081,208 +1990,6 @@ namespace GPUVerify impl.LocVars = NewLocalVars;
}
- private void AddPredicateLocalVariables(Implementation impl)
- {
- for (int i = 0; i < IfCounter; i++)
- {
- impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P" + i, Microsoft.Boogie.Type.Bool)));
- }
- for (int i = 0; i < WhileLoopCounter; i++)
- {
- impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_LC" + i, Microsoft.Boogie.Type.Bool)));
- }
- foreach (Microsoft.Boogie.Type t in RequiredHavocVariables)
- {
- impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_HAVOC_" + t.ToString(), t)));
- }
-
- }
-
- private StmtList MakePredicated(StmtList sl, Expr predicate, IdentifierExpr EnclosingLoopPredicate)
- {
- StmtList result = new StmtList(new List<BigBlock>(), sl.EndCurly);
-
- foreach (BigBlock bodyBlock in sl.BigBlocks)
- {
- List<BigBlock> newBigBlocks = MakePredicated(bodyBlock, predicate, EnclosingLoopPredicate);
- foreach (BigBlock newBigBlock in newBigBlocks)
- {
- result.BigBlocks.Add(newBigBlock);
- }
- }
-
- return result;
-
- }
-
- private List<BigBlock> MakePredicated(BigBlock b, Expr IncomingPredicate, IdentifierExpr EnclosingLoopPredicate)
- {
- // Not sure what to do about the transfer command
-
- List<BigBlock> result = new List<BigBlock>();
-
- BigBlock firstBigBlock = new BigBlock(b.tok, b.LabelName, new CmdSeq(), null, b.tc);
- result.Add(firstBigBlock);
-
- foreach (Cmd c in b.simpleCmds)
- {
- if (c is CallCmd)
- {
-
- CallCmd Call = c as CallCmd;
-
- List<Expr> NewIns = new List<Expr>();
- NewIns.Add(IncomingPredicate);
-
- foreach (Expr e in Call.Ins)
- {
- NewIns.Add(e);
- }
-
- CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, NewIns, Call.Outs);
-
- firstBigBlock.simpleCmds.Add(NewCallCmd);
- }
- else if (IncomingPredicate.Equals(Expr.True))
- {
- firstBigBlock.simpleCmds.Add(c);
- }
- else if (c is AssignCmd)
- {
- AssignCmd assign = c as AssignCmd;
- Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
-
- ExprSeq iteArgs = new ExprSeq();
- iteArgs.Add(IncomingPredicate);
- iteArgs.Add(assign.Rhss.ElementAt(0));
- iteArgs.Add(assign.Lhss.ElementAt(0).AsExpr);
- NAryExpr ite = new NAryExpr(assign.tok, new IfThenElse(assign.tok), iteArgs);
-
- List<Expr> newRhs = new List<Expr>();
- newRhs.Add(ite);
-
- AssignCmd newAssign = new AssignCmd(assign.tok, assign.Lhss, newRhs);
-
- firstBigBlock.simpleCmds.Add(newAssign);
- }
- else if (c is HavocCmd)
- {
- HavocCmd havoc = c as HavocCmd;
- Debug.Assert(havoc.Vars.Length == 1);
-
- Microsoft.Boogie.Type type = havoc.Vars[0].Decl.TypedIdent.Type;
- Debug.Assert(type != null);
-
- RequiredHavocVariables.Add(type);
-
- IdentifierExpr HavocTempExpr = new IdentifierExpr(havoc.tok, new LocalVariable(havoc.tok, new TypedIdent(havoc.tok, "_HAVOC_" + type.ToString(), type)));
- firstBigBlock.simpleCmds.Add(new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
- HavocTempExpr
- })));
-
- List<AssignLhs> lhss = new List<AssignLhs>();
- lhss.Add(new SimpleAssignLhs(havoc.tok, havoc.Vars[0]));
-
- List<Expr> rhss = new List<Expr>();
- rhss.Add(new NAryExpr(havoc.tok, new IfThenElse(havoc.tok), new ExprSeq(new Expr[] { IncomingPredicate, HavocTempExpr, havoc.Vars[0] })));
-
- firstBigBlock.simpleCmds.Add(new AssignCmd(havoc.tok, lhss, rhss));
-
- }
- else
- {
- Debug.Assert(false);
- }
- }
-
- if (b.ec is WhileCmd)
- {
- string LoopPredicate = "_LC" + WhileLoopCounter;
- WhileLoopCounter++;
-
- IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, LoopPredicate, Microsoft.Boogie.Type.Bool)));
- Expr GuardExpr = (b.ec as WhileCmd).Guard;
-
- List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();
- WhilePredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));
-
- List<Expr> WhilePredicateRhss = new List<Expr>();
- WhilePredicateRhss.Add(IncomingPredicate.Equals(Expr.True) ? GuardExpr : Expr.And(IncomingPredicate, GuardExpr));
-
- firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, WhilePredicateRhss));
-
- WhileCmd NewWhile = new WhileCmd(b.ec.tok, PredicateExpr, (b.ec as WhileCmd).Invariants, MakePredicated((b.ec as WhileCmd).Body, PredicateExpr, PredicateExpr));
-
- List<Expr> UpdatePredicateRhss = new List<Expr>();
- UpdatePredicateRhss.Add(Expr.And(PredicateExpr, GuardExpr));
-
- CmdSeq updateCmd = new CmdSeq();
- updateCmd.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, UpdatePredicateRhss));
-
- NewWhile.Body.BigBlocks.Add(new BigBlock(b.ec.tok, "update_" + LoopPredicate, updateCmd, null, null));
-
- firstBigBlock.ec = NewWhile;
-
- }
- else if (b.ec is IfCmd)
- {
- IfCmd IfCommand = b.ec as IfCmd;
-
- string IfPredicate = "_P" + IfCounter;
- IfCounter++;
-
- IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, IfPredicate, Microsoft.Boogie.Type.Bool)));
- Expr GuardExpr = IfCommand.Guard;
-
- List<AssignLhs> IfPredicateLhss = new List<AssignLhs>();
- IfPredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));
-
- List<Expr> IfPredicateRhss = new List<Expr>();
- IfPredicateRhss.Add(GuardExpr);
-
- firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, IfPredicateLhss, IfPredicateRhss));
-
- Debug.Assert(IfCommand.elseIf == null); // We need to preprocess these away
-
- StmtList PredicatedThen = MakePredicated(IfCommand.thn, Expr.And(IncomingPredicate, PredicateExpr), EnclosingLoopPredicate);
-
- foreach (BigBlock bb in PredicatedThen.BigBlocks)
- {
- result.Add(bb);
- }
-
- if (IfCommand.elseBlock != null)
- {
- StmtList PredicatedElse = MakePredicated(IfCommand.elseBlock, Expr.And(IncomingPredicate, Expr.Not(PredicateExpr)), EnclosingLoopPredicate);
-
- foreach (BigBlock bb in PredicatedElse.BigBlocks)
- {
- result.Add(bb);
- }
- }
-
-
-
-
- }
- else if (b.ec is BreakCmd)
- {
-
-
- firstBigBlock.simpleCmds.Add(new AssignCmd(b.tok,
- new List<AssignLhs>(new AssignLhs[] { new SimpleAssignLhs(b.tok, EnclosingLoopPredicate) }),
- new List<Expr>(new Expr[] { new NAryExpr(b.tok, new IfThenElse(b.tok), new ExprSeq(new Expr[] { IncomingPredicate, Expr.False, EnclosingLoopPredicate })) })
- ));
- firstBigBlock.ec = null;
-
- }
- else
- {
- Debug.Assert(b.ec == null);
- }
-
- return result;
- }
private void CheckKernelParameters()
{
@@ -2454,5 +2161,87 @@ namespace GPUVerify return variable is Constant && (variable.Name.Equals(_X_name) || variable.Name.Equals(_Y_name) || variable.Name.Equals(_Z_name));
}
+ internal HashSet<string> GetProceduresThatIndirectlyCallProcedure(string Name)
+ {
+ HashSet<string> MayCallProc = new HashSet<string>();
+ MayCallProc.Add(Name);
+ bool changed = true;
+ while (changed)
+ {
+ changed = false;
+ foreach (Declaration d in Program.TopLevelDeclarations)
+ {
+ if (d is Implementation && !MayCallProc.Contains((d as Implementation).Name))
+ {
+ HashSet<string> CalledProcedures = GetCalledProcedures(d as Implementation);
+ foreach (string p in CalledProcedures)
+ {
+ if (MayCallProc.Contains(p))
+ {
+ changed = true;
+ MayCallProc.Add((d as Implementation).Name);
+ break;
+ }
+ }
+ }
+ }
+ }
+ return MayCallProc;
+ }
+
+ private HashSet<string> GetCalledProcedures(Implementation impl)
+ {
+ HashSet<string> result = new HashSet<string>();
+ return GetCalledProcedures(impl.StructuredStmts, result);
+ }
+
+ private HashSet<string> GetCalledProcedures(StmtList statements, HashSet<string> result)
+ {
+ foreach (BigBlock bb in statements.BigBlocks)
+ {
+ foreach (Cmd c in bb.simpleCmds)
+ {
+ if (c is CallCmd)
+ {
+ result.Add((c as CallCmd).callee);
+ }
+ }
+
+ if (bb.ec is WhileCmd)
+ {
+ result = GetCalledProcedures((bb.ec as WhileCmd).Body, result);
+ }
+ else if (bb.ec is IfCmd)
+ {
+ result = GetCalledProcedures((bb.ec as IfCmd).thn, result);
+ Debug.Assert((bb.ec as IfCmd).elseIf == null);
+ if ((bb.ec as IfCmd).elseBlock != null)
+ {
+ result = GetCalledProcedures((bb.ec as IfCmd).elseBlock, result);
+ }
+ }
+ }
+
+ return result;
+ }
+
+ internal void ExtendModifiesSetOfProcedures(IdentifierExprSeq ModifiedVariables, HashSet<string> Procedures)
+ {
+ foreach (Declaration d in Program.TopLevelDeclarations)
+ {
+ if (d is Procedure && Procedures.Contains((d as Procedure).Name))
+ {
+ Procedure P = d as Procedure;
+ foreach (IdentifierExpr e in ModifiedVariables)
+ {
+ if (!GPUVerifier.ModifiesSetContains(P.Modifies, e))
+ {
+ P.Modifies.Add(e);
+ }
+ }
+ }
+ }
+ }
+
}
}
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 3b4e3bc5..7023a2b3 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -2,7 +2,7 @@ <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <Platform Condition=" '$(Platform)' == '' ">x86</Platform>
<ProductVersion>8.0.30703</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>{E5D16606-06D0-434F-A9D7-7D079BC80229}</ProjectGuid>
@@ -15,8 +15,8 @@ <FileAlignment>512</FileAlignment>
<CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
</PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <PlatformTarget>AnyCPU</PlatformTarget>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">
+ <PlatformTarget>x86</PlatformTarget>
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
@@ -24,7 +24,7 @@ <DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
<CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
@@ -51,93 +51,15 @@ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
<CodeContractsAnalysisPrecisionLevel>0</CodeContractsAnalysisPrecisionLevel>
- <CodeContractsInferRequires>False</CodeContractsInferRequires>
- <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
- <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
- <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
- <CodeContractsDisjunctiveRequires>False</CodeContractsDisjunctiveRequires>
</PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <PlatformTarget>AnyCPU</PlatformTarget>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
+ <PlatformTarget>x86</PlatformTarget>
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
<OutputPath>bin\Release\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsInferRequires>False</CodeContractsInferRequires>
- <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
- <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
- <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
- <CodeContractsDisjunctiveRequires>False</CodeContractsDisjunctiveRequires>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\GPUVerify.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
@@ -155,12 +77,15 @@ <Compile Include="CommandLineOptions.cs" />
<Compile Include="ElementEncodingraceInstrumenter.cs" />
<Compile Include="GPUVerifier.cs" />
+ <Compile Include="INonLocalState.cs" />
<Compile Include="IRaceInstrumenter.cs" />
<Compile Include="Main.cs" />
<Compile Include="NoConflictingAccessOptimiser.cs" />
<Compile Include="NonLocalAccessCollector.cs" />
<Compile Include="NonLocalAccessExtractor.cs" />
+ <Compile Include="NonLocalStateLists.cs" />
<Compile Include="NullRaceInstrumenter.cs" />
+ <Compile Include="Predicator.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="RaceInstrumenterBase.cs" />
<Compile Include="ReadCollector.cs" />
diff --git a/Source/GPUVerify/INonLocalState.cs b/Source/GPUVerify/INonLocalState.cs new file mode 100644 index 00000000..0e03d685 --- /dev/null +++ b/Source/GPUVerify/INonLocalState.cs @@ -0,0 +1,21 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ interface INonLocalState
+ {
+
+ ICollection<Variable> getGlobalVariables();
+
+ ICollection<Variable> getTileStaticVariables();
+
+ ICollection<Variable> getAllNonLocalVariables();
+
+ bool Contains(Variable v);
+
+ }
+}
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs index 06fe70c6..9791d6cf 100644 --- a/Source/GPUVerify/Main.cs +++ b/Source/GPUVerify/Main.cs @@ -15,11 +15,16 @@ namespace GPUVerify {
class GPUVerify
{
- static bool ASYNCHRONOUS_METHOD = false;
public static void Main(string[] args)
{
- CommandLineOptions.Parse(args);
+ int showHelp = CommandLineOptions.Parse(args);
+
+ if (showHelp == -1)
+ {
+ CommandLineOptions.Usage();
+ System.Environment.Exit(0);
+ }
if (CommandLineOptions.inputFiles.Count < 1)
{
@@ -42,36 +47,6 @@ namespace GPUVerify }
}
- if (ASYNCHRONOUS_METHOD)
- {
-
- string[] preprocessArguments = new string[CommandLineOptions.inputFiles.Count + 4];
- preprocessArguments[0] = "/noVerify";
- preprocessArguments[1] = "/printUnstructured";
- preprocessArguments[2] = "/print:temp_unstructured.bpl";
- preprocessArguments[3] = Path.GetDirectoryName(Application.ExecutablePath) + "\\..\\..\\BoogieLibrary\\GPUVerifyLibrary.bpl";
- for (int i = 0; i < CommandLineOptions.inputFiles.Count; i++)
- {
- preprocessArguments[i + 4] = CommandLineOptions.inputFiles[i];
- }
-
- OnlyBoogie.Main(preprocessArguments);
-
- if ((CommandLineOptions.formulasFile == null && CommandLineOptions.formulaSkeletonsFile == null) || (CommandLineOptions.formulasFile != null && CommandLineOptions.formulaSkeletonsFile != null))
- {
- Console.WriteLine("Error, specify one of /formulas:... or /generateFormulaSkeletons:...");
- Environment.Exit(1);
- }
-
- CommandLineOptions.inputFiles = new List<string>();
- CommandLineOptions.inputFiles.Add("temp_unstructured.bpl");
- if (CommandLineOptions.formulasFile != null)
- {
- CommandLineOptions.inputFiles.Add(CommandLineOptions.formulasFile);
- }
-
- }
-
parseProcessOutput();
}
@@ -121,23 +96,23 @@ namespace GPUVerify ri.setVerifier(newGp);
- Variable newG = findClonedVar(v, newGp.GlobalVariables);
- Variable newT = findClonedVar(v, newGp.TileStaticVariables);
+ Variable newG = findClonedVar(v, newGp.NonLocalState.getGlobalVariables());
+ Variable newT = findClonedVar(v, newGp.NonLocalState.getTileStaticVariables());
Contract.Assert(newG == null || newT == null);
-
- ri.globalVarsToCheck.Clear();
- ri.tileStaticVarsToCheck.Clear();
+
+ ri.NonLocalStateToCheck.getGlobalVariables().Clear();
+ ri.NonLocalStateToCheck.getTileStaticVariables().Clear();
ri.onlyLog1 = a1;
ri.onlyLog2 = a2;
if (newG != null)
{
- ri.globalVarsToCheck.Add(newG);
+ ri.NonLocalStateToCheck.getGlobalVariables().Add(newG);
}
if (newT != null)
{
- ri.globalVarsToCheck.Add(newT);
+ ri.NonLocalStateToCheck.getTileStaticVariables().Add(newT);
}
newGp.doit();
@@ -159,11 +134,7 @@ namespace GPUVerify if (CommandLineOptions.DividedArray)
{
- List<Variable> nonLocalVars = new List<Variable>();
- nonLocalVars.AddRange(g.GlobalVariables);
- nonLocalVars.AddRange(g.TileStaticVariables);
-
- foreach (Variable v in nonLocalVars)
+ foreach (Variable v in g.NonLocalState.getAllNonLocalVariables())
{
if (CommandLineOptions.DividedAccesses)
{
diff --git a/Source/GPUVerify/NonLocalAccessCollector.cs b/Source/GPUVerify/NonLocalAccessCollector.cs index bbab9040..13d8f672 100644 --- a/Source/GPUVerify/NonLocalAccessCollector.cs +++ b/Source/GPUVerify/NonLocalAccessCollector.cs @@ -12,16 +12,14 @@ namespace GPUVerify {
public HashSet<Expr> Accesses = new HashSet<Expr>();
- private ICollection<Variable> GlobalVariables;
- private ICollection<Variable> TileStaticVariables;
+ private INonLocalState NonLocalState;
- public NonLocalAccessCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public NonLocalAccessCollector(INonLocalState NonLocalState)
{
- this.GlobalVariables = GlobalVariables;
- this.TileStaticVariables = TileStaticVariables;
+ this.NonLocalState = NonLocalState;
}
- public static bool IsNonLocalAccess(Expr n, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public static bool IsNonLocalAccess(Expr n, INonLocalState NonLocalState)
{
if (n is NAryExpr)
{
@@ -37,22 +35,22 @@ namespace GPUVerify Variable v = (temp as IdentifierExpr).Decl;
- return (GlobalVariables.Contains(v) || TileStaticVariables.Contains(v));
+ return (NonLocalState.Contains(v));
}
}
if (n is IdentifierExpr)
{
IdentifierExpr node = n as IdentifierExpr;
- return GlobalVariables.Contains(node.Decl) || TileStaticVariables.Contains(node.Decl);
+ return NonLocalState.Contains(node.Decl);
}
return false;
}
- public static bool ContainsNonLocalAccess(AssignLhs lhs, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public static bool ContainsNonLocalAccess(AssignLhs lhs, INonLocalState NonLocalState)
{
- NonLocalAccessCollector collector = new NonLocalAccessCollector(GlobalVariables, TileStaticVariables);
+ NonLocalAccessCollector collector = new NonLocalAccessCollector(NonLocalState);
if (lhs is SimpleAssignLhs)
{
collector.VisitSimpleAssignLhs(lhs as SimpleAssignLhs);
@@ -65,9 +63,9 @@ namespace GPUVerify return collector.Accesses.Count > 0;
}
- public static bool ContainsNonLocalAccess(Expr rhs, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public static bool ContainsNonLocalAccess(Expr rhs, INonLocalState NonLocalState)
{
- NonLocalAccessCollector collector = new NonLocalAccessCollector(GlobalVariables, TileStaticVariables);
+ NonLocalAccessCollector collector = new NonLocalAccessCollector(NonLocalState);
collector.VisitExpr(rhs);
return collector.Accesses.Count > 0;
}
@@ -75,7 +73,7 @@ namespace GPUVerify public override Expr VisitNAryExpr(NAryExpr node)
{
- if (IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))
+ if (IsNonLocalAccess(node, NonLocalState))
{
Accesses.Add(node);
return node;
@@ -85,7 +83,7 @@ namespace GPUVerify public override Expr VisitIdentifierExpr(IdentifierExpr node)
{
- if (IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))
+ if (IsNonLocalAccess(node, NonLocalState))
{
Accesses.Add(node);
return node;
diff --git a/Source/GPUVerify/NonLocalAccessExtractor.cs b/Source/GPUVerify/NonLocalAccessExtractor.cs index 506ec3c5..553be683 100644 --- a/Source/GPUVerify/NonLocalAccessExtractor.cs +++ b/Source/GPUVerify/NonLocalAccessExtractor.cs @@ -14,14 +14,12 @@ namespace GPUVerify public LocalVariable Declaration = null;
public bool done = false;
- private ICollection<Variable> GlobalVariables;
- private ICollection<Variable> TileStaticVariables;
+ private INonLocalState NonLocalState;
- public NonLocalAccessExtractor(int TempId, ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
+ public NonLocalAccessExtractor(int TempId, INonLocalState NonLocalState)
{
this.TempId = TempId;
- this.GlobalVariables = GlobalVariables;
- this.TileStaticVariables = TileStaticVariables;
+ this.NonLocalState = NonLocalState;
}
@@ -32,7 +30,7 @@ namespace GPUVerify return node;
}
- if (!NonLocalAccessCollector.IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))
+ if (!NonLocalAccessCollector.IsNonLocalAccess(node, NonLocalState))
{
return base.VisitNAryExpr(node);
}
@@ -42,7 +40,7 @@ namespace GPUVerify {
Debug.Assert((temp as NAryExpr).Args.Length == 2);
- if (NonLocalAccessCollector.ContainsNonLocalAccess((temp as NAryExpr).Args[1], GlobalVariables, TileStaticVariables))
+ if (NonLocalAccessCollector.ContainsNonLocalAccess((temp as NAryExpr).Args[1], NonLocalState))
{
return VisitExpr((temp as NAryExpr).Args[1]);
}
@@ -77,7 +75,7 @@ namespace GPUVerify return node;
}
- if (NonLocalAccessCollector.IsNonLocalAccess(node, GlobalVariables, TileStaticVariables))
+ if (NonLocalAccessCollector.IsNonLocalAccess(node, NonLocalState))
{
done = true;
Declaration = new LocalVariable(node.tok, new TypedIdent(node.tok, "_temp" + TempId, node.Decl.TypedIdent.Type));
diff --git a/Source/GPUVerify/NonLocalStateLists.cs b/Source/GPUVerify/NonLocalStateLists.cs new file mode 100644 index 00000000..a4b5e154 --- /dev/null +++ b/Source/GPUVerify/NonLocalStateLists.cs @@ -0,0 +1,45 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics;
+
+namespace GPUVerify
+{
+ class NonLocalStateLists : INonLocalState
+ {
+ private List<Variable> GlobalVariables;
+ private List<Variable> TileStaticVariables;
+
+ public NonLocalStateLists()
+ {
+ GlobalVariables = new List<Variable>();
+ TileStaticVariables = new List<Variable>();
+ }
+
+ public ICollection<Variable> getGlobalVariables()
+ {
+ return GlobalVariables;
+ }
+
+ public ICollection<Variable> getTileStaticVariables()
+ {
+ return TileStaticVariables;
+ }
+
+ public ICollection<Variable> getAllNonLocalVariables()
+ {
+ List<Variable> all = new List<Variable>();
+ all.AddRange(GlobalVariables);
+ all.AddRange(TileStaticVariables);
+ return all;
+ }
+
+ public bool Contains(Variable v)
+ {
+ return getAllNonLocalVariables().Contains(v);
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs new file mode 100644 index 00000000..cca89b52 --- /dev/null +++ b/Source/GPUVerify/Predicator.cs @@ -0,0 +1,256 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace GPUVerify
+{
+ class Predicator
+ {
+ private bool AddPredicateParameter;
+ private int WhileLoopCounter;
+ private int IfCounter;
+ private static HashSet<Microsoft.Boogie.Type> RequiredHavocVariables;
+
+ internal Predicator(bool AddPredicateParameter)
+ {
+ this.AddPredicateParameter = AddPredicateParameter;
+ WhileLoopCounter = 0;
+ IfCounter = 0;
+ RequiredHavocVariables = new HashSet<Microsoft.Boogie.Type>();
+ }
+
+ internal void transform(Implementation impl)
+ {
+ Expr Predicate;
+
+ if (AddPredicateParameter)
+ {
+ VariableSeq NewIns = new VariableSeq();
+ Variable PredicateVariable = new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P", Microsoft.Boogie.Type.Bool));
+ NewIns.Add(PredicateVariable);
+ foreach (Variable v in impl.InParams)
+ {
+ NewIns.Add(v);
+ }
+ impl.InParams = NewIns;
+ Predicate = new IdentifierExpr(impl.tok, PredicateVariable);
+ }
+ else
+ {
+ Predicate = Expr.True;
+ }
+
+ impl.StructuredStmts = MakePredicated(impl.StructuredStmts, Predicate, null);
+ AddPredicateLocalVariables(impl);
+ }
+
+
+ private StmtList MakePredicated(StmtList sl, Expr predicate, IdentifierExpr EnclosingLoopPredicate)
+ {
+ StmtList result = new StmtList(new List<BigBlock>(), sl.EndCurly);
+
+ foreach (BigBlock bodyBlock in sl.BigBlocks)
+ {
+ List<BigBlock> newBigBlocks = MakePredicated(bodyBlock, predicate, EnclosingLoopPredicate);
+ foreach (BigBlock newBigBlock in newBigBlocks)
+ {
+ result.BigBlocks.Add(newBigBlock);
+ }
+ }
+
+ return result;
+
+ }
+
+ private List<BigBlock> MakePredicated(BigBlock b, Expr IncomingPredicate, IdentifierExpr EnclosingLoopPredicate)
+ {
+ // Not sure what to do about the transfer command
+
+ List<BigBlock> result = new List<BigBlock>();
+
+ BigBlock firstBigBlock = new BigBlock(b.tok, b.LabelName, new CmdSeq(), null, b.tc);
+ result.Add(firstBigBlock);
+
+ foreach (Cmd c in b.simpleCmds)
+ {
+ if (c is CallCmd)
+ {
+
+ CallCmd Call = c as CallCmd;
+
+ List<Expr> NewIns = new List<Expr>();
+ NewIns.Add(IncomingPredicate);
+
+ foreach (Expr e in Call.Ins)
+ {
+ NewIns.Add(e);
+ }
+
+ CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, NewIns, Call.Outs);
+
+ firstBigBlock.simpleCmds.Add(NewCallCmd);
+ }
+ else if (IncomingPredicate.Equals(Expr.True))
+ {
+ firstBigBlock.simpleCmds.Add(c);
+ }
+ else if (c is AssignCmd)
+ {
+ AssignCmd assign = c as AssignCmd;
+ Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);
+
+ ExprSeq iteArgs = new ExprSeq();
+ iteArgs.Add(IncomingPredicate);
+ iteArgs.Add(assign.Rhss.ElementAt(0));
+ iteArgs.Add(assign.Lhss.ElementAt(0).AsExpr);
+ NAryExpr ite = new NAryExpr(assign.tok, new IfThenElse(assign.tok), iteArgs);
+
+ List<Expr> newRhs = new List<Expr>();
+ newRhs.Add(ite);
+
+ AssignCmd newAssign = new AssignCmd(assign.tok, assign.Lhss, newRhs);
+
+ firstBigBlock.simpleCmds.Add(newAssign);
+ }
+ else if (c is HavocCmd)
+ {
+ HavocCmd havoc = c as HavocCmd;
+ Debug.Assert(havoc.Vars.Length == 1);
+
+ Microsoft.Boogie.Type type = havoc.Vars[0].Decl.TypedIdent.Type;
+ Debug.Assert(type != null);
+
+ RequiredHavocVariables.Add(type);
+
+ IdentifierExpr HavocTempExpr = new IdentifierExpr(havoc.tok, new LocalVariable(havoc.tok, new TypedIdent(havoc.tok, "_HAVOC_" + type.ToString(), type)));
+ firstBigBlock.simpleCmds.Add(new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] {
+ HavocTempExpr
+ })));
+
+ List<AssignLhs> lhss = new List<AssignLhs>();
+ lhss.Add(new SimpleAssignLhs(havoc.tok, havoc.Vars[0]));
+
+ List<Expr> rhss = new List<Expr>();
+ rhss.Add(new NAryExpr(havoc.tok, new IfThenElse(havoc.tok), new ExprSeq(new Expr[] { IncomingPredicate, HavocTempExpr, havoc.Vars[0] })));
+
+ firstBigBlock.simpleCmds.Add(new AssignCmd(havoc.tok, lhss, rhss));
+
+ }
+ else
+ {
+ Debug.Assert(false);
+ }
+ }
+
+ if (b.ec is WhileCmd)
+ {
+ string LoopPredicate = "_LC" + WhileLoopCounter;
+ WhileLoopCounter++;
+
+ IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, LoopPredicate, Microsoft.Boogie.Type.Bool)));
+ Expr GuardExpr = (b.ec as WhileCmd).Guard;
+
+ List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();
+ WhilePredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));
+
+ List<Expr> WhilePredicateRhss = new List<Expr>();
+ WhilePredicateRhss.Add(IncomingPredicate.Equals(Expr.True) ? GuardExpr : Expr.And(IncomingPredicate, GuardExpr));
+
+ firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, WhilePredicateRhss));
+
+ WhileCmd NewWhile = new WhileCmd(b.ec.tok, PredicateExpr, (b.ec as WhileCmd).Invariants, MakePredicated((b.ec as WhileCmd).Body, PredicateExpr, PredicateExpr));
+
+ List<Expr> UpdatePredicateRhss = new List<Expr>();
+ UpdatePredicateRhss.Add(Expr.And(PredicateExpr, GuardExpr));
+
+ CmdSeq updateCmd = new CmdSeq();
+ updateCmd.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, UpdatePredicateRhss));
+
+ NewWhile.Body.BigBlocks.Add(new BigBlock(b.ec.tok, "update_" + LoopPredicate, updateCmd, null, null));
+
+ firstBigBlock.ec = NewWhile;
+
+ }
+ else if (b.ec is IfCmd)
+ {
+ IfCmd IfCommand = b.ec as IfCmd;
+
+ string IfPredicate = "_P" + IfCounter;
+ IfCounter++;
+
+ IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, IfPredicate, Microsoft.Boogie.Type.Bool)));
+ Expr GuardExpr = IfCommand.Guard;
+
+ List<AssignLhs> IfPredicateLhss = new List<AssignLhs>();
+ IfPredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));
+
+ List<Expr> IfPredicateRhss = new List<Expr>();
+ IfPredicateRhss.Add(GuardExpr);
+
+ firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, IfPredicateLhss, IfPredicateRhss));
+
+ Debug.Assert(IfCommand.elseIf == null); // We need to preprocess these away
+
+ StmtList PredicatedThen = MakePredicated(IfCommand.thn, Expr.And(IncomingPredicate, PredicateExpr), EnclosingLoopPredicate);
+
+ foreach (BigBlock bb in PredicatedThen.BigBlocks)
+ {
+ result.Add(bb);
+ }
+
+ if (IfCommand.elseBlock != null)
+ {
+ StmtList PredicatedElse = MakePredicated(IfCommand.elseBlock, Expr.And(IncomingPredicate, Expr.Not(PredicateExpr)), EnclosingLoopPredicate);
+
+ foreach (BigBlock bb in PredicatedElse.BigBlocks)
+ {
+ result.Add(bb);
+ }
+ }
+
+
+
+
+ }
+ else if (b.ec is BreakCmd)
+ {
+
+
+ firstBigBlock.simpleCmds.Add(new AssignCmd(b.tok,
+ new List<AssignLhs>(new AssignLhs[] { new SimpleAssignLhs(b.tok, EnclosingLoopPredicate) }),
+ new List<Expr>(new Expr[] { new NAryExpr(b.tok, new IfThenElse(b.tok), new ExprSeq(new Expr[] { IncomingPredicate, Expr.False, EnclosingLoopPredicate })) })
+ ));
+ firstBigBlock.ec = null;
+
+ }
+ else
+ {
+ Debug.Assert(b.ec == null);
+ }
+
+ return result;
+ }
+
+
+ private void AddPredicateLocalVariables(Implementation impl)
+ {
+ for (int i = 0; i < IfCounter; i++)
+ {
+ impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P" + i, Microsoft.Boogie.Type.Bool)));
+ }
+ for (int i = 0; i < WhileLoopCounter; i++)
+ {
+ impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_LC" + i, Microsoft.Boogie.Type.Bool)));
+ }
+ foreach (Microsoft.Boogie.Type t in RequiredHavocVariables)
+ {
+ impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_HAVOC_" + t.ToString(), t)));
+ }
+
+ }
+
+ }
+}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs index 90229af0..0f5f8278 100644 --- a/Source/GPUVerify/RaceInstrumenterBase.cs +++ b/Source/GPUVerify/RaceInstrumenterBase.cs @@ -12,8 +12,8 @@ namespace GPUVerify abstract class RaceInstrumenterBase : IRaceInstrumenter
{
protected GPUVerifier verifier;
- public ICollection<Variable> globalVarsToCheck;
- public ICollection<Variable> tileStaticVarsToCheck;
+
+ public INonLocalState NonLocalStateToCheck;
public int onlyLog1;
public int onlyLog2;
@@ -33,8 +33,15 @@ namespace GPUVerify public void setVerifier(GPUVerifier verifier)
{
this.verifier = verifier;
- globalVarsToCheck = new HashSet<Variable>(verifier.GlobalVariables);
- tileStaticVarsToCheck = new HashSet<Variable>(verifier.TileStaticVariables);
+ NonLocalStateToCheck = new NonLocalStateLists();
+ foreach(Variable v in verifier.NonLocalState.getGlobalVariables())
+ {
+ NonLocalStateToCheck.getGlobalVariables().Add(v);
+ }
+ foreach(Variable v in verifier.NonLocalState.getTileStaticVariables())
+ {
+ NonLocalStateToCheck.getTileStaticVariables().Add(v);
+ }
}
protected abstract void AddRequiresNoPendingAccess(Variable v);
@@ -80,13 +87,7 @@ namespace GPUVerify public void AddRaceCheckingCandidateInvariants(WhileCmd wc)
{
- foreach (Variable v in globalVarsToCheck)
- {
- AddNoReadOrWriteCandidateInvariants(wc, v);
- AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(wc, v);
- }
-
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
AddNoReadOrWriteCandidateInvariants(wc, v);
AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(wc, v);
@@ -134,12 +135,7 @@ namespace GPUVerify public void AddKernelPrecondition()
{
- foreach (Variable v in globalVarsToCheck)
- {
- AddRequiresNoPendingAccess(v);
- }
-
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
AddRequiresNoPendingAccess(v);
}
@@ -163,12 +159,7 @@ namespace GPUVerify if (failedToFindSecondAccess || !addedLogWrite)
return false;
- foreach (Variable v in globalVarsToCheck)
- {
- AddRaceCheckingDecsAndProcsForVar(v);
- }
-
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
AddRaceCheckingDecsAndProcsForVar(v);
}
@@ -179,12 +170,29 @@ namespace GPUVerify private void AddRaceCheckingDecsAndProcsForVar(Variable v)
{
- AddLogRaceDeclarations(v, "READ");
- AddLogRaceDeclarations(v, "WRITE");
+ IdentifierExprSeq ReadDeclsResetAtBarrier;
+ IdentifierExprSeq WriteDeclsResetAtBarrier;
+ IdentifierExprSeq ReadDeclsModifiedAtLogRead;
+ IdentifierExprSeq WriteDeclsModifiedAtLogWrite;
+
+ AddLogRaceDeclarations(v, "READ", out ReadDeclsResetAtBarrier, out ReadDeclsModifiedAtLogRead);
+ AddLogRaceDeclarations(v, "WRITE", out WriteDeclsResetAtBarrier, out WriteDeclsModifiedAtLogWrite);
AddLogAccessProcedure(v, "READ");
AddLogAccessProcedure(v, "WRITE");
- }
+ HashSet<string> MayCallBarrier = verifier.GetProceduresThatIndirectlyCallProcedure(verifier.BarrierProcedure.Name);
+
+ verifier.ExtendModifiesSetOfProcedures(ReadDeclsResetAtBarrier, MayCallBarrier);
+ verifier.ExtendModifiesSetOfProcedures(WriteDeclsResetAtBarrier, MayCallBarrier);
+
+ HashSet<string> MayCallLogRead = verifier.GetProceduresThatIndirectlyCallProcedure("_LOG_READ_" + v.Name);
+ HashSet<string> MayCallLogWrite = verifier.GetProceduresThatIndirectlyCallProcedure("_LOG_WRITE_" + v.Name);
+
+ verifier.ExtendModifiesSetOfProcedures(ReadDeclsModifiedAtLogRead, MayCallLogRead);
+ verifier.ExtendModifiesSetOfProcedures(WriteDeclsModifiedAtLogWrite, MayCallLogWrite);
+
+ }
+
private StmtList AddRaceCheckCalls(StmtList stmtList)
{
Contract.Requires(stmtList != null);
@@ -242,7 +250,7 @@ namespace GPUVerify AssignLhs lhs = assign.Lhss[0];
Expr rhs = assign.Rhss[0];
- ReadCollector rc = new ReadCollector(globalVarsToCheck, tileStaticVarsToCheck);
+ ReadCollector rc = new ReadCollector(NonLocalStateToCheck);
rc.Visit(rhs);
if (rc.accesses.Count > 0)
{
@@ -271,7 +279,7 @@ namespace GPUVerify }
}
- WriteCollector wc = new WriteCollector(globalVarsToCheck, tileStaticVarsToCheck);
+ WriteCollector wc = new WriteCollector(NonLocalStateToCheck);
wc.Visit(lhs);
if (wc.GetAccess() != null)
{
@@ -331,7 +339,7 @@ namespace GPUVerify }
- protected abstract void AddLogRaceDeclarations(Variable v, String ReadOrWrite);
+ protected abstract void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog);
protected abstract void AddLogAccessProcedure(Variable v, string ReadOrWrite);
@@ -341,21 +349,13 @@ namespace GPUVerify BigBlock checkForRaces = new BigBlock(tok, "__CheckForRaces", new CmdSeq(), null, null);
if (!CommandLineOptions.Eager)
{
- foreach (Variable v in globalVarsToCheck)
- {
- CheckForRaces(tok, checkForRaces, v);
- }
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
CheckForRaces(tok, checkForRaces, v);
}
}
- foreach (Variable v in globalVarsToCheck)
- {
- SetNoAccessOccurred(tok, checkForRaces, v);
- }
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
SetNoAccessOccurred(tok, checkForRaces, v);
}
@@ -431,13 +431,7 @@ namespace GPUVerify public void AddRaceCheckingCandidateRequires(Procedure Proc)
{
- foreach (Variable v in globalVarsToCheck)
- {
- AddNoReadOrWriteCandidateRequires(Proc, v);
- AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
- }
-
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
AddNoReadOrWriteCandidateRequires(Proc, v);
AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
@@ -446,13 +440,7 @@ namespace GPUVerify public void AddRaceCheckingCandidateEnsures(Procedure Proc)
{
- foreach (Variable v in globalVarsToCheck)
- {
- AddNoReadOrWriteCandidateEnsures(Proc, v);
- AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
- }
-
- foreach (Variable v in tileStaticVarsToCheck)
+ foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
{
AddNoReadOrWriteCandidateEnsures(Proc, v);
AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
diff --git a/Source/GPUVerify/ReadCollector.cs b/Source/GPUVerify/ReadCollector.cs index 281620c5..53d9234e 100644 --- a/Source/GPUVerify/ReadCollector.cs +++ b/Source/GPUVerify/ReadCollector.cs @@ -17,8 +17,8 @@ namespace GPUVerify public List<AccessRecord> accesses = new List<AccessRecord>();
- public ReadCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
- : base(GlobalVariables, TileStaticVariables)
+ public ReadCollector(INonLocalState NonLocalState)
+ : base(NonLocalState)
{
}
@@ -83,7 +83,7 @@ namespace GPUVerify this.VisitExpr(node.Args[1]);
- if (GlobalVariables.Contains(ReadVariable) || TileStaticVariables.Contains(ReadVariable))
+ if (NonLocalState.Contains(ReadVariable))
{
accesses.Add(new AccessRecord(ReadVariable, IndexZ, IndexY, IndexX));
}
@@ -100,7 +100,7 @@ namespace GPUVerify public override Variable VisitVariable(Variable node)
{
- if (!(GlobalVariables.Contains(node) || TileStaticVariables.Contains(node)))
+ if (!NonLocalState.Contains(node))
{
return node;
}
diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs index c4f42923..3b1f877e 100644 --- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs +++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs @@ -11,7 +11,7 @@ namespace GPUVerify class SetEncodingRaceInstrumenter : RaceInstrumenterBase
{
- protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite)
+ protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog)
{
Variable AccessSet = MakeAccessSetVariable(v, ReadOrWrite);
@@ -22,9 +22,9 @@ namespace GPUVerify verifier.Program.TopLevelDeclarations.Add(AccessSet);
- // TODO: add modiies to every procedure that calls BARRIER
+ ResetAtBarrier = new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, AccessSet) });
+ ModifiedAtLog = ResetAtBarrier;
- verifier.KernelProcedure.Modifies.Add(new IdentifierExpr(v.tok, AccessSet));
}
private static Variable MakeAccessSetVariable(Variable v, String ReadOrWrite)
@@ -192,13 +192,11 @@ namespace GPUVerify MakeAccessSetVariable(v, AccessType)));
IdentifierExprSeq VariablesToHavoc = new IdentifierExprSeq();
VariablesToHavoc.Add(AccessSet1);
- verifier.BarrierProcedure.Modifies.Add(AccessSet1);
if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))
{
IdentifierExpr AccessSet2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(
MakeAccessSetVariable(v, AccessType)));
VariablesToHavoc.Add(AccessSet2);
- verifier.BarrierProcedure.Modifies.Add(AccessSet2);
}
bb.simpleCmds.Add(new HavocCmd(tok, VariablesToHavoc));
diff --git a/Source/GPUVerify/WriteCollector.cs b/Source/GPUVerify/WriteCollector.cs index e8623e3b..d55c5d05 100644 --- a/Source/GPUVerify/WriteCollector.cs +++ b/Source/GPUVerify/WriteCollector.cs @@ -13,15 +13,15 @@ namespace GPUVerify private AccessRecord access = null;
- public WriteCollector(ICollection<Variable> GlobalVariables, ICollection<Variable> TileStaticVariables)
- : base(GlobalVariables, TileStaticVariables)
+ public WriteCollector(INonLocalState NonLocalState)
+ : base(NonLocalState)
{
}
public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)
{
Debug.Assert(NoWrittenVariable());
- if (GlobalVariables.Contains(node.DeepAssignedVariable) || TileStaticVariables.Contains(node.DeepAssignedVariable))
+ if (NonLocalState.Contains(node.DeepAssignedVariable))
{
access = new AccessRecord(node.DeepAssignedVariable, null, null, null);
}
@@ -37,7 +37,7 @@ namespace GPUVerify {
Debug.Assert(NoWrittenVariable());
- if (!(GlobalVariables.Contains(node.DeepAssignedVariable) || TileStaticVariables.Contains(node.DeepAssignedVariable)))
+ if (!NonLocalState.Contains(node.DeepAssignedVariable))
{
return node;
}
diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs index c1d7fcd3..afcb0fe6 100644 --- a/Source/ModelViewer/Namer.cs +++ b/Source/ModelViewer/Namer.cs @@ -159,7 +159,13 @@ namespace Microsoft.Boogie.ModelViewer Action<IEnumerable<IDisplayNode>> addList = (IEnumerable<IDisplayNode> nodes) =>
{
- var ch = nodes.ToDictionary(x => x.Name);
+ var ch = new Dictionary<string, IDisplayNode>();
+ foreach (var x in nodes) {
+ if (ch.ContainsKey(x.Name)) {
+ // throw new System.InvalidOperationException("duplicated model entry: " + x.Name);
+ }
+ ch[x.Name] = x;
+ }
foreach (var k in SortFields(nodes))
workList.Enqueue(ch[k]);
};
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs index ede520cb..10e4db10 100644 --- a/Source/ModelViewer/VccProvider.cs +++ b/Source/ModelViewer/VccProvider.cs @@ -307,6 +307,8 @@ namespace Microsoft.Boogie.ModelViewer.Vcc res = 1;
else if (name.EndsWith("#frame"))
res = 2;
+ else if (name.Contains("#limited#"))
+ res = 2;
else {
for (int i = 0; i < prefixes.Length; ++i)
foreach (var p in prefixes[i])
@@ -314,7 +316,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc res = i;
//goto stop;
}
- //stop: ;
+ //stop: ;
}
if (res == -1)
@@ -395,6 +397,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc return name.Substring(2);
}
+ if (name.StartsWith("OP#")) {
+ kind = "out-param";
+ return name.Substring(3);
+ }
+
if (name.StartsWith("SL#")) {
kind = "spec local";
return name.Substring(3);
@@ -500,7 +507,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc foreach (var app in elt.Names)
if (app.Func.Arity == 0 && app.Func.Name.StartsWith("^")) {
- var n = app.Func.Name.Substring(1);
+ var n = app.Func.Name.Substring(1);
switch (n) {
case "^i1": return "int8_t";
case "^u1": return "uint8_t";
@@ -511,8 +518,11 @@ namespace Microsoft.Boogie.ModelViewer.Vcc case "^i8": return "int64_t";
case "^u8": return "uint64_t";
case "^bool": return "bool";
- default: return n;
- }
+ default:
+ var pref = "_vcc_math_type_";
+ if (n.StartsWith(pref)) n = n.Substring(pref.Length);
+ return n;
+ }
}
return null;
@@ -676,12 +686,12 @@ namespace Microsoft.Boogie.ModelViewer.Vcc var fldName = tpl.Func.Name.Substring(3);
var idx = fldName.LastIndexOf('.');
if (idx > 0) {
- return fldName.Substring(0, idx);
+ return fldName.Substring(0, idx).Replace("_vcc_math_type_", ""); }
}
if (tpl.Args.Length == 1 && tpl.Args[0] == elt && (fname.StartsWith("DSZ#") || fname.StartsWith("RSZ#") || fname.StartsWith("DGH#"))) {
- return fname.Substring(4);
+ return fname.Substring(4).Replace("_vcc_math_type_", "");
}
return null;
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index bdbb8822..bae3aa50 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -133,8 +133,11 @@ Execution trace: (0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
+NatTypes.dfy(127,21): Error: value assigned to a nat must be non-negative
+Execution trace:
+ (0,0): anon3_Then
-Dafny program verifier finished with 12 verified, 8 errors
+Dafny program verifier finished with 15 verified, 9 errors
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 47bc22e1..0513591c 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -108,3 +108,30 @@ function Abs(x: int): nat {
if 0 <= x then x else -x
}
+
+// ----- Here are tests that the type of the result value of a function is known by the
+// ----- time the well-formedness of the function's specification is checked.
+
+function TakesANat(n: nat): bool
+{
+ n < 29
+}
+
+function Naturally(): nat
+ ensures TakesANat(Naturally()); // the wellformedness of this check requires
+{
+ 17
+}
+
+function Integrally_Bad(): int
+ ensures TakesANat(Integrally_Bad()); // error: well-formedness check fails
+{
+ 17
+}
+
+function Integrally_Good(): int
+ ensures 0 <= Integrally_Good();
+ ensures TakesANat(Integrally_Good()); // here, the needed information follows from the preceding ensures clause
+{
+ 17
+}
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index cf603751..7235303a 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -39,7 +39,7 @@ "assert" "assume" "break" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print"
"old" "forall" "exists" "new" "parallel" "in" "this" "fresh" "allocated"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
- `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "nat" "int" "object" "set" "seq")) . font-lock-type-face)
+ `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "nat" "int" "object" "set" "seq")) . font-lock-type-face)
)
"Minimal highlighting for Dafny mode")
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 6f9ec810..557beb32 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -12,7 +12,8 @@ namespace Demo #region 1. Terminals
NumberLiteral n = TerminalFactory.CreateCSharpNumber("number");
- IdentifierTerminal ident = new IdentifierTerminal("Identifier");
+ IdentifierTerminal ident = new IdentifierTerminal("Identifier", "'_?", "'_?");
+
StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");
this.MarkReservedWords( // NOTE: these keywords must also appear once more below
@@ -351,7 +352,6 @@ namespace Demo | "==>"
| "<==>"
| "#"
- | "?" // this is not an operator, but a possible character in identifiers
| n
| stringLiteral
;
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index f80acc26..e8e94e17 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -266,6 +266,7 @@ namespace DafnyLanguage case "method":
case "modifies":
case "module":
+ case "multiset":
case "nat":
case "new":
case "null":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 1bbab1b7..34ee3d1d 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -5,7 +5,7 @@ \usepackage{listings}
\lstdefinelanguage{dafny}{
- morekeywords={class,datatype,bool,nat,int,object,set,seq,array,array2,array3,%
+ morekeywords={class,datatype,bool,nat,int,object,set,multiset,seq,array,array2,array3,%
function,unlimited,
ghost,var,static,refines,replaces,by,
method,constructor,returns,module,imports,in,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index 2d0aeab3..b806fb0b 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -11,7 +11,7 @@ syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while parallel syntax keyword dafnyStatement havoc assume assert return new print break label syntax keyword dafnyKeyword var ghost returns null static this refines replaces by -syntax keyword dafnyType bool nat int seq set object array array2 array3 +syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant syntax keyword dafnyOperator forall exists old fresh allocated choose syntax keyword dafnyBoolean true false |