diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-07-05 09:41:33 -0700 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-07-05 09:41:33 -0700 |
| commit | 88dab600dda872d76be801e3d0011b2174ce01aa (patch) | |
| tree | 37785e0f9e8735b4fb522ff2a8cdbd94a13f5fc7 | |
| parent | 7361ff10cf634b447dc7fa69527d3bb3e6f01dd8 (diff) | |
| parent | d786b753f39294f4e2d5f57d16c69bb450abc799 (diff) | |
Merge
71 files changed, 475 insertions, 194 deletions
@@ -8,6 +8,7 @@ syntax: regexp ^Binaries/BytecodeTranslator$
^BCT/Binaries/.*$
^Chalice/bin/
+^Chalice/tests/(examples|permission-model|refinements)/.*\.bpl
Test/([^/]*)/Output
Test/([^/]*)/([^/]*)\.sx
Test/(dafny0|dafny1|VSI-Benchmarks|vacid0|VSComp2010)/(out\.cs|.*\.dll|.*\.pdb|.*\.exe)
@@ -18,3 +19,4 @@ BCT/TestResults/ BCT/testimpactdata.sdf
backup.diff
BCT/Samples/CodeCounter/console/ClassDiagram1.cd
+Chalice/makestamp
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 4b49125c..51b2a525 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -925,7 +925,7 @@ namespace BytecodeTranslator { }
return v;
}
- Dictionary<ITryCatchFinallyStatement, int> tryCatchFinallyIdentifiers;
+ public Dictionary<ITryCatchFinallyStatement, int> tryCatchFinallyIdentifiers;
public string FindOrCreateCatchLabel(ITryCatchFinallyStatement stmt) {
int id;
if (!tryCatchFinallyIdentifiers.TryGetValue(stmt, out id)) {
@@ -950,6 +950,14 @@ namespace BytecodeTranslator { }
return "continuation" + id;
}
+ public string FindOrCreateDispatchContinuationLabel(ITryCatchFinallyStatement stmt) {
+ int id;
+ if (!tryCatchFinallyIdentifiers.TryGetValue(stmt, out id)) {
+ id = tryCatchFinallyIdentifiers.Count;
+ tryCatchFinallyIdentifiers[stmt] = id;
+ }
+ return "DispatchContinuation" + id;
+ }
MostNestedTryStatementTraverser mostNestedTryStatementTraverser;
public ITryCatchFinallyStatement MostNestedTryStatement(IName label) {
return mostNestedTryStatementTraverser.MostNestedTryStatement(label);
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index b0821dcd..0dc7c5ab 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -95,16 +95,18 @@ namespace BytecodeTranslator }
public void GenerateDispatchContinuation() {
- // Iterate over all labels in sink.cciLabels and generate dispatch based on sink.LabelVariable
- this.StmtBuilder.AddLabelCmd("DispatchContinuation");
- Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(true), TranslationHelper.BuildStmtList(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false))), null, null);
- Bpl.IdentifierExpr labelExpr = Bpl.Expr.Ident(this.sink.LabelVariable);
- foreach (IName name in sink.cciLabels.Keys) {
- Bpl.GotoCmd gotoCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(name.Value));
- Bpl.Expr targetExpr = Bpl.Expr.Literal(sink.cciLabels[name]);
- elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr), TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);
+ foreach (ITryCatchFinallyStatement stmt in sink.tryCatchFinallyIdentifiers.Keys) {
+ // Iterate over all labels in sink.cciLabels and generate dispatch based on sink.LabelVariable
+ this.StmtBuilder.AddLabelCmd(sink.FindOrCreateDispatchContinuationLabel(stmt));
+ Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(true), TranslationHelper.BuildStmtList(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false))), null, null);
+ Bpl.IdentifierExpr labelExpr = Bpl.Expr.Ident(this.sink.LabelVariable);
+ foreach (IName name in sink.cciLabels.Keys) {
+ Bpl.GotoCmd gotoCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(name.Value));
+ Bpl.Expr targetExpr = Bpl.Expr.Literal(sink.cciLabels[name]);
+ elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr), TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);
+ }
+ this.StmtBuilder.Add(elseIfCmd);
}
- this.StmtBuilder.Add(elseIfCmd);
}
#endregion
@@ -227,7 +229,6 @@ namespace BytecodeTranslator /// <param name="expressionStatement"></param>
/// <remarks> TODO: might be wrong for the general case</remarks>
public override void Visit(IExpressionStatement expressionStatement) {
-
ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);
etrav.Visit(expressionStatement.Expression);
}
@@ -238,7 +239,12 @@ namespace BytecodeTranslator /// <remarks>(mschaef) Not Implemented</remarks>
/// <param name="breakStatement"></param>
public override void Visit(IBreakStatement breakStatement) {
- StmtBuilder.Add(new Bpl.BreakCmd(breakStatement.Token(), "I dont know"));
+ throw new TranslationException("Break statements are not handled");
+ //StmtBuilder.Add(new Bpl.BreakCmd(breakStatement.Token(), "I dont know"));
+ }
+
+ public override void Visit(IContinueStatement continueStatement) {
+ throw new TranslationException("Continue statements are not handled");
}
/// <summary>
@@ -357,10 +363,16 @@ namespace BytecodeTranslator #region Looping Statements
public override void Visit(IWhileDoStatement whileDoStatement) {
- throw new NotImplementedException("While Statements are not implemented");
+ throw new TranslationException("WhileDo statements are not handled");
}
+ public override void Visit(IForEachStatement forEachStatement) {
+ throw new TranslationException("ForEach statements are not handled");
+ }
+ public override void Visit(IForStatement forStatement) {
+ throw new TranslationException("For statements are not handled");
+ }
#endregion
@@ -451,7 +463,7 @@ namespace BytecodeTranslator StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Ident(savedFinallyStackCounterVariable)));
nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);
}
- Bpl.GotoCmd dispatchCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq("DispatchContinuation"));
+ Bpl.GotoCmd dispatchCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateDispatchContinuationLabel(tryCatchFinallyStatement)));
Bpl.GotoCmd continuationCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement)));
Bpl.IfCmd ifCmd = new Bpl.IfCmd(
Bpl.Token.NoToken,
diff --git a/Chalice/src/Chalice.scala b/Chalice/src/Chalice.scala index 1b53a187..973d6b94 100644 --- a/Chalice/src/Chalice.scala +++ b/Chalice/src/Chalice.scala @@ -47,7 +47,7 @@ object Chalice { var boogieArgs = " ";
var gen = false;
var showFullStackTrace = false
-
+
// closures should be idempotent
val options = Map(
"-print" -> {() => printProgram = true},
@@ -87,7 +87,13 @@ object Chalice { else percentageSupport = in
} catch { case _ => CommandLineError("-percentageSupport takes integer argument", help); }
}
- else if (a.startsWith("-") || a.startsWith("/")) boogieArgs += (a + " ") // other arguments starting with "-" or "/" are sent to Boogie.exe
+ else if (a.startsWith("-") || a.startsWith("/"))
+ boogieArgs += ('"' + a + '"' + " ")
+ // other arguments starting with "-" or "/" are sent to Boogie.exe
+ /* [MHS] Quote whole argument to not confuse Boogie with arguments that
+ * contain spaces, e.g. if Chalice is invoked as
+ * chalice -z3exe:"C:\Program Files\z3\z3.exe" program.chalice
+ */
else inputs += a
}
diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala index 5e9943a0..b1aaeea9 100644 --- a/Chalice/src/Translator.scala +++ b/Chalice/src/Translator.scala @@ -969,7 +969,7 @@ class Translator { // havoc formal outs
(for (v <- formalOuts) yield Havoc(v)) :::
// havoc lockchanges
- LockHavoc(for (e <- LockChanges(c.m.Spec) map (p => SubstVars(p, formalThis, c.m.Ins, formalIns))) yield etran.Tr(e), postEtran) :::
+ LockHavoc(for (e <- LockChanges(c.m.Spec) map (p => SubstVars(p, formalThis, c.m.Ins ++ c.m.Outs, formalIns ++ formalOuts))) yield etran.Tr(e), postEtran) :::
// inhale postconditions (using the state before the call as the "old" state)
postEtran.Inhale(Postconditions(c.m.Spec) map
(p => SubstVars(p, formalThis, c.m.Ins ++ c.m.Outs, formalIns ++ formalOuts)) , "postcondition", false, methodCallK) :::
diff --git a/Chalice/test.bat b/Chalice/test.bat deleted file mode 100644 index 4bf5db07..00000000 --- a/Chalice/test.bat +++ /dev/null @@ -1,46 +0,0 @@ -@echo off
-echo start > Output
-
-set CHALICE=call scala -cp bin chalice.Chalice -nologo
-
-
-REM to do: AssociationList
-REM to do: GhostConst
-REM to do: Leaks -checkLeaks
-
-for %%f in (cell counter dining-philosophers ForkJoin HandOverHand
- iterator iterator2 producer-consumer
- prog0 prog1 prog2 prog3 prog4 ImplicitLocals
- RockBand swap OwickiGries ProdConsChannel LoopLockChange
- PetersonsAlgorithm quantifiers) do (
- echo Testing %%f.chalice ...
- echo ------ Running regression test %%f.chalice >> Output
- %CHALICE% %* examples\%%f.chalice >> Output 2>&1
-)
-
-echo Testing cell-defaults.chalice ...
-echo ------ Running regression test cell-defaults.chalice >> Output
-%CHALICE% %* -defaults -autoFold -autoMagic examples\cell-defaults.chalice >> Output 2>&1
-
-echo Testing RockBand-automagic.chalice ...
-echo ------ Running regression test RockBand-automagic.chalice >> Output
-%CHALICE% %* -defaults -autoMagic -checkLeaks -autoFold examples\RockBand-automagic.chalice >> Output 2>&1
-
-
-fc examples\Answer Output > nul
-if not errorlevel 1 goto passTest
-goto failTest
-
-:passTest
-echo Succeeded
-goto end
-
-:failTest
-echo Failed
-goto end
-
-:errorEnd
-exit /b 1
-
-:end
-exit /b 0
diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt index 719af1af..618d878a 100644 --- a/Chalice/tests/examples/AssociationList.output.txt +++ b/Chalice/tests/examples/AssociationList.output.txt @@ -1,4 +1,4 @@ -Verification of AssociationList.chalice
+Verification of AssociationList.chalice using parameters=""
19.3: The postcondition at 21.13 might not hold. Insufficient fraction at 21.13 for mu.
64.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
diff --git a/Chalice/tests/examples/BackgroundComputation.chalice b/Chalice/tests/examples/BackgroundComputation.chalice new file mode 100644 index 00000000..e8168183 --- /dev/null +++ b/Chalice/tests/examples/BackgroundComputation.chalice @@ -0,0 +1,38 @@ +class C {
+ var x: int;
+
+ method main()
+ requires acc(x);
+ ensures acc(x);
+ {
+ // start long-running processing
+ fork tk := processing();
+
+ /* do some computation itself */
+
+ // finish
+ call finish(tk);
+ }
+
+ method finish(tk: token<C.processing>)
+ requires acc(x,100-rd(tk));
+ requires acc(tk.joinable) && tk.joinable && tk != null;
+ requires eval(tk.fork this.processing(), true);
+ ensures acc(x);
+ {
+ var res: int;
+ join res := tk;
+
+ // final write to x (requires full permission)
+ this.x := res - 1;
+ }
+
+ method processing() returns (res: int)
+ requires rd(x);
+ ensures rd(x);
+ {
+ res := 1;
+ /* do some computation */
+ }
+
+}
diff --git a/Chalice/tests/examples/BackgroundComputation.output.txt b/Chalice/tests/examples/BackgroundComputation.output.txt new file mode 100644 index 00000000..c139677a --- /dev/null +++ b/Chalice/tests/examples/BackgroundComputation.output.txt @@ -0,0 +1,4 @@ +Verification of BackgroundComputation.chalice using parameters=""
+
+
+Boogie program verifier finished with 7 verified, 0 errors
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt index 46633611..4099f78a 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt @@ -1,4 +1,4 @@ -Verification of CopyLessMessagePassing-with-ack.chalice
+Verification of CopyLessMessagePassing-with-ack.chalice using parameters=""
Boogie program verifier finished with 11 verified, 0 errors
diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt index e8c42507..6ba69de5 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt @@ -1,4 +1,4 @@ -Verification of CopyLessMessagePassing-with-ack2.chalice
+Verification of CopyLessMessagePassing-with-ack2.chalice using parameters=""
Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Chalice/tests/examples/CopyLessMessagePassing.output.txt b/Chalice/tests/examples/CopyLessMessagePassing.output.txt index d6fd8be3..859c9998 100644 --- a/Chalice/tests/examples/CopyLessMessagePassing.output.txt +++ b/Chalice/tests/examples/CopyLessMessagePassing.output.txt @@ -1,4 +1,4 @@ -Verification of CopyLessMessagePassing.chalice
+Verification of CopyLessMessagePassing.chalice using parameters=""
Boogie program verifier finished with 11 verified, 0 errors
diff --git a/Chalice/tests/examples/FictionallyDisjointCells.chalice b/Chalice/tests/examples/FictionallyDisjointCells.chalice new file mode 100644 index 00000000..d26dedbb --- /dev/null +++ b/Chalice/tests/examples/FictionallyDisjointCells.chalice @@ -0,0 +1,75 @@ +class Cell
+{
+ var inner: InnerCell;
+
+ predicate inv
+ {
+ acc(inner) && inner!=null && rd(inner.value,1) && rd*(inner.mu) && rd*(this.mu)
+ }
+
+ method CellConstructor()
+ requires acc(inner) && acc(this.mu)
+ ensures inv && get()==0;
+ {
+ inner := new InnerCell;
+ call inner.InnerCellConstructor(0)
+ share inner;
+ fold inv;
+ }
+
+ method CellConstructor2(other: Cell)
+ requires acc(inner) && acc(this.mu)
+ requires other != null && other.inv;
+ requires unfolding other.inv in waitlevel << other.inner.mu
+ ensures inv && other.inv && get()==other.get();
+ {
+ unfold other.inv;
+ inner := other.inner;
+ acquire inner;
+ inner.refCount := inner.refCount+1;
+ release inner;
+ fold other.inv;
+ fold inv;
+ }
+
+ function get():int
+ requires inv;
+ { unfolding inv in inner.value }
+
+ method set(x:int)
+ requires inv;
+ requires unfolding inv in waitlevel << inner.mu
+ ensures inv && get()==x;
+ {
+ var old_in: InnerCell;
+ unfold inv;
+ old_in := inner;
+ acquire old_in;
+ if (inner.refCount==1) { inner.value:=x; }
+ else
+ {
+ inner.refCount := inner.refCount-1;
+ inner := new InnerCell;
+ call inner.InnerCellConstructor(x)
+ share inner;
+ }
+ release old_in;
+ fold inv;
+ }
+}
+
+class InnerCell
+{
+ var value: int;
+ var refCount: int;
+
+ invariant acc(refCount) && refCount > 0 && acc(value,100-rd(refCount));
+
+ method InnerCellConstructor(val: int)
+ requires acc(refCount) && acc(value)
+ ensures acc(refCount) && acc(value) && refCount==1 && value == val;
+ {
+ refCount := 1;
+ value := val
+ }
+}
diff --git a/Chalice/tests/examples/FictionallyDisjointCells.output.txt b/Chalice/tests/examples/FictionallyDisjointCells.output.txt new file mode 100644 index 00000000..1dc7a7b1 --- /dev/null +++ b/Chalice/tests/examples/FictionallyDisjointCells.output.txt @@ -0,0 +1,4 @@ +Verification of FictionallyDisjointCells.chalice using parameters=""
+
+
+Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Chalice/tests/examples/ForkJoin.output.txt b/Chalice/tests/examples/ForkJoin.output.txt index 06d44bec..ed2abbda 100644 --- a/Chalice/tests/examples/ForkJoin.output.txt +++ b/Chalice/tests/examples/ForkJoin.output.txt @@ -1,4 +1,4 @@ -Verification of ForkJoin.chalice
+Verification of ForkJoin.chalice using parameters=""
Boogie program verifier finished with 18 verified, 0 errors
diff --git a/Chalice/tests/examples/HandOverHand.output.txt b/Chalice/tests/examples/HandOverHand.output.txt index a57fe677..de7ab98c 100644 --- a/Chalice/tests/examples/HandOverHand.output.txt +++ b/Chalice/tests/examples/HandOverHand.output.txt @@ -1,4 +1,4 @@ -Verification of HandOverHand.chalice
+Verification of HandOverHand.chalice using parameters=""
Boogie program verifier finished with 10 verified, 0 errors
diff --git a/Chalice/tests/examples/ImplicitLocals.output.txt b/Chalice/tests/examples/ImplicitLocals.output.txt index c3f518ed..4d7b08b1 100644 --- a/Chalice/tests/examples/ImplicitLocals.output.txt +++ b/Chalice/tests/examples/ImplicitLocals.output.txt @@ -1,4 +1,4 @@ -Verification of ImplicitLocals.chalice
+Verification of ImplicitLocals.chalice using parameters=""
Boogie program verifier finished with 8 verified, 0 errors
diff --git a/Chalice/tests/examples/LoopLockChange.output.txt b/Chalice/tests/examples/LoopLockChange.output.txt index c6c69a24..7a03627f 100644 --- a/Chalice/tests/examples/LoopLockChange.output.txt +++ b/Chalice/tests/examples/LoopLockChange.output.txt @@ -1,4 +1,4 @@ -Verification of LoopLockChange.chalice
+Verification of LoopLockChange.chalice using parameters=""
10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
35.5: The loop might lock/unlock more than the lockchange clause allows.
diff --git a/Chalice/tests/examples/OwickiGries.output.txt b/Chalice/tests/examples/OwickiGries.output.txt index ff585ab1..a56e7442 100644 --- a/Chalice/tests/examples/OwickiGries.output.txt +++ b/Chalice/tests/examples/OwickiGries.output.txt @@ -1,4 +1,4 @@ -Verification of OwickiGries.chalice
+Verification of OwickiGries.chalice using parameters=""
Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Chalice/tests/examples/PetersonsAlgorithm.output.txt b/Chalice/tests/examples/PetersonsAlgorithm.output.txt index bf470e3a..5bc49aaa 100644 --- a/Chalice/tests/examples/PetersonsAlgorithm.output.txt +++ b/Chalice/tests/examples/PetersonsAlgorithm.output.txt @@ -1,4 +1,4 @@ -Verification of PetersonsAlgorithm.chalice
+Verification of PetersonsAlgorithm.chalice using parameters=""
Boogie program verifier finished with 7 verified, 0 errors
diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt index 1cfe7dfb..de5e8467 100644 --- a/Chalice/tests/examples/ProdConsChannel.output.txt +++ b/Chalice/tests/examples/ProdConsChannel.output.txt @@ -1,4 +1,4 @@ -Verification of ProdConsChannel.chalice
+Verification of ProdConsChannel.chalice using parameters=""
47.3: Method body is not allowed to leave any debt.
61.3: Method body is not allowed to leave any debt.
diff --git a/Chalice/tests/examples/RockBand-automagic.chalice b/Chalice/tests/examples/RockBand-automagic.chalice index d231ae5a..8a64b691 100644 --- a/Chalice/tests/examples/RockBand-automagic.chalice +++ b/Chalice/tests/examples/RockBand-automagic.chalice @@ -1,3 +1,4 @@ +// chalice-parameter=-checkLeaks -defaults -autoFold -autoMagic
// verify this program with -checkLeaks -defaults -autoFold -autoMagic
class Client {
diff --git a/Chalice/tests/examples/RockBand-automagic.output.txt b/Chalice/tests/examples/RockBand-automagic.output.txt index d494e16a..9ce4b436 100644 --- a/Chalice/tests/examples/RockBand-automagic.output.txt +++ b/Chalice/tests/examples/RockBand-automagic.output.txt @@ -1,11 +1,8 @@ -Verification of RockBand-automagic.chalice
+Verification of RockBand-automagic.chalice using parameters="-checkLeaks -defaults -autoFold -autoMagic"
- 19.27: Location might not be readable.
- 27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
- 41.10: Location might not be readable.
- 50.5: Location might not be writable
- 58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.
- 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.
- 96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.
+ 20.27: Location might not be readable.
+ 28.3: Method RockBand.Init might leak references.
+ 42.10: Location might not be readable.
+ 51.5: Location might not be writable
-Boogie program verifier finished with 28 verified, 7 errors
+Boogie program verifier finished with 31 verified, 4 errors
diff --git a/Chalice/tests/examples/RockBand.chalice b/Chalice/tests/examples/RockBand.chalice index 49b99a68..379b4113 100644 --- a/Chalice/tests/examples/RockBand.chalice +++ b/Chalice/tests/examples/RockBand.chalice @@ -1,3 +1,4 @@ +// chalice-parameter=-checkLeaks -defaults -autoFold
// verify this program with -checkLeaks -defaults -autoFold
class Client {
diff --git a/Chalice/tests/examples/RockBand.output.txt b/Chalice/tests/examples/RockBand.output.txt index 3fb1b1c6..a52b021b 100644 --- a/Chalice/tests/examples/RockBand.output.txt +++ b/Chalice/tests/examples/RockBand.output.txt @@ -1,10 +1,4 @@ -Verification of RockBand.chalice
+Verification of RockBand.chalice using parameters="-checkLeaks -defaults -autoFold"
- 27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
- 41.10: Location might not be readable.
- 50.5: Location might not be writable
- 58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.
- 77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.
- 96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.
-Boogie program verifier finished with 29 verified, 6 errors
+Boogie program verifier finished with 35 verified, 0 errors
diff --git a/Chalice/tests/examples/Sieve.output.txt b/Chalice/tests/examples/Sieve.output.txt index b8b74b59..93271d87 100644 --- a/Chalice/tests/examples/Sieve.output.txt +++ b/Chalice/tests/examples/Sieve.output.txt @@ -1,4 +1,4 @@ -Verification of Sieve.chalice
+Verification of Sieve.chalice using parameters=""
Boogie program verifier finished with 11 verified, 0 errors
diff --git a/Chalice/tests/examples/TreeOfWorker.chalice b/Chalice/tests/examples/TreeOfWorker.chalice new file mode 100644 index 00000000..6483f884 --- /dev/null +++ b/Chalice/tests/examples/TreeOfWorker.chalice @@ -0,0 +1,29 @@ +class Node {
+ var l: Node
+ var r: Node
+
+ method work(data: Data)
+ requires rd(data.f)
+ requires valid
+ ensures rd(data.f)
+ ensures valid
+ {
+ var tkl: token<Node.work>
+ var tkr: token<Node.work>
+
+ unfold valid
+ if (l != null) { fork tkl := l.work(data) }
+ if (r != null) { fork tkr := r.work(data) }
+ /* .. perform work on this node (using the global data: data.f) */
+ if (l != null) { join tkl }
+ if (r != null) { join tkr }
+ fold valid
+ }
+
+ predicate valid {
+ acc(l) && acc(r) &&
+ (l != null ==> l.valid) &&
+ (r != null ==> r.valid)
+ }
+}
+class Data { var f: int; }
diff --git a/Chalice/tests/examples/TreeOfWorker.output.txt b/Chalice/tests/examples/TreeOfWorker.output.txt new file mode 100644 index 00000000..4dc67e3c --- /dev/null +++ b/Chalice/tests/examples/TreeOfWorker.output.txt @@ -0,0 +1,4 @@ +Verification of TreeOfWorker.chalice using parameters=""
+
+
+Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Chalice/tests/examples/UnboundedThreads.chalice b/Chalice/tests/examples/UnboundedThreads.chalice new file mode 100644 index 00000000..c52bb10a --- /dev/null +++ b/Chalice/tests/examples/UnboundedThreads.chalice @@ -0,0 +1,59 @@ +class C {
+
+ var f: int;
+
+ method main(n: int)
+ requires n > 0 && acc(this.f)
+ ensures acc(this.f)
+ {
+ // fork all threads, and join them afterwards
+ call work(n);
+
+ this.f := 100; // we want a full permission in the end
+ }
+
+ method work(n: int)
+ requires rd(this.f,n)
+ ensures rd(this.f,n)
+ {
+ var tks:seq<token<C.m>> := nil<token<C.m>>;
+
+ // first loop; fork all threads
+ var i := 0;
+ while (i < n)
+ invariant i <= n && |tks| == i;
+ invariant i < n ==> rd(this.f,n-i);
+ invariant acc(tks[*].joinable);
+ invariant forall k in [0..|tks|] :: tks[k] != null && tks[k].joinable;
+ invariant forall k in [0..|tks|] :: eval(tks[k].fork this.m(), true);
+ invariant forall k,j in [0..|tks|] :: k < j ==> tks[k] != tks[j];
+ {
+ fork tk := m();
+ tks := tks ++ [tk];
+ i := i+1;
+ }
+
+ // second loop; join all threads
+ i := n;
+ while (i > 0)
+ invariant i >= 0 && |tks| == i;
+ invariant i < n ==> rd(this.f,n-i); // BUG: the eval construct inside the quantification does not give us the information needed to proof this invariant, see http://boogie.codeplex.com/workitem/10187
+ invariant acc(tks[*].joinable);
+ invariant forall k in [0..|tks|] :: tks[k] != null && tks[k].joinable;
+ invariant forall k in [0..|tks|] :: eval(tks[k].fork this.m(), true);
+ invariant forall k,j in [0..|tks|] :: k < j ==> tks[k] != tks[j];
+ {
+ var tk: token<C.m>;
+ tk := tks[i-1];
+ join tk;
+ i := i-1;
+ tks := tks[0..i];
+ }
+ }
+
+ method m()
+ requires rd(this.f,1);
+ ensures rd(this.f,1);
+ { /* do some computation */ }
+
+}
diff --git a/Chalice/tests/examples/UnboundedThreads.output.txt b/Chalice/tests/examples/UnboundedThreads.output.txt new file mode 100644 index 00000000..efd70a6d --- /dev/null +++ b/Chalice/tests/examples/UnboundedThreads.output.txt @@ -0,0 +1,5 @@ +Verification of UnboundedThreads.chalice using parameters=""
+
+ 40.17: The loop invariant at 40.17 might not be preserved by the loop. Insufficient epsilons at 40.27 for C.f.
+
+Boogie program verifier finished with 6 verified, 1 error
diff --git a/Chalice/tests/examples/cell-defaults.chalice b/Chalice/tests/examples/cell-defaults.chalice index 4781db97..eb826f89 100644 --- a/Chalice/tests/examples/cell-defaults.chalice +++ b/Chalice/tests/examples/cell-defaults.chalice @@ -1,3 +1,4 @@ +// chalice-parameter=-defaults -autoFold -autoMagic
// verify this program with -defaults -autoFold -autoMagic
class Cell module Library {
diff --git a/Chalice/tests/examples/cell-defaults.output.txt b/Chalice/tests/examples/cell-defaults.output.txt index ee7ae4e5..0f7a3b80 100644 --- a/Chalice/tests/examples/cell-defaults.output.txt +++ b/Chalice/tests/examples/cell-defaults.output.txt @@ -1,17 +1,7 @@ -Verification of cell-defaults.chalice
+Verification of cell-defaults.chalice using parameters="-defaults -autoFold -autoMagic"
- 6.3: The postcondition at 8.13 might not hold. Insufficient fraction at 8.13 for Cell.valid.
- 17.5: Location might not be writable
- 24.5: Location might not be writable
- 31.5: The field x of the target of the free statement might not be writable.
- 38.5: Location might not be readable.
- 52.3: The postcondition at 55.13 might not hold. Insufficient fraction at 55.13 for Interval.valid.
- 71.10: Location might not be readable.
- 80.10: Location might not be readable.
- 89.10: Location might not be readable.
- 96.5: Location might not be readable.
- 102.5: Location might not be readable.
- 107.5: Location might not be readable.
- 131.5: Assertion might not hold. Insufficient fraction at 131.12 for Cell.valid.
+ 97.5: The heap of the callee might not be strictly smaller than the heap of the caller.
+ 103.5: The heap of the callee might not be strictly smaller than the heap of the caller.
+ 132.5: Assertion might not hold. Insufficient fraction at 132.12 for Cell.valid.
-Boogie program verifier finished with 19 verified, 13 errors
+Boogie program verifier finished with 29 verified, 3 errors
diff --git a/Chalice/tests/examples/cell.output.txt b/Chalice/tests/examples/cell.output.txt index 3ca21dd2..2c6c617d 100644 --- a/Chalice/tests/examples/cell.output.txt +++ b/Chalice/tests/examples/cell.output.txt @@ -1,4 +1,4 @@ -Verification of cell.chalice
+Verification of cell.chalice using parameters=""
142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.
diff --git a/Chalice/tests/examples/counter.output.txt b/Chalice/tests/examples/counter.output.txt index 6fdd2d7c..961b1413 100644 --- a/Chalice/tests/examples/counter.output.txt +++ b/Chalice/tests/examples/counter.output.txt @@ -1,4 +1,4 @@ -Verification of counter.chalice
+Verification of counter.chalice using parameters=""
69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.
80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.
diff --git a/Chalice/tests/examples/dining-philosophers.output.txt b/Chalice/tests/examples/dining-philosophers.output.txt index 2bf72597..651bd638 100644 --- a/Chalice/tests/examples/dining-philosophers.output.txt +++ b/Chalice/tests/examples/dining-philosophers.output.txt @@ -1,4 +1,4 @@ -Verification of dining-philosophers.chalice
+Verification of dining-philosophers.chalice using parameters=""
Boogie program verifier finished with 12 verified, 0 errors
diff --git a/Chalice/tests/examples/iterator.output.txt b/Chalice/tests/examples/iterator.output.txt index a03f7c0c..de361b94 100644 --- a/Chalice/tests/examples/iterator.output.txt +++ b/Chalice/tests/examples/iterator.output.txt @@ -1,4 +1,4 @@ -Verification of iterator.chalice
+Verification of iterator.chalice using parameters=""
Boogie program verifier finished with 22 verified, 0 errors
diff --git a/Chalice/tests/examples/iterator2.output.txt b/Chalice/tests/examples/iterator2.output.txt index 512a2e26..af837e6f 100644 --- a/Chalice/tests/examples/iterator2.output.txt +++ b/Chalice/tests/examples/iterator2.output.txt @@ -1,4 +1,4 @@ -Verification of iterator2.chalice
+Verification of iterator2.chalice using parameters=""
Boogie program verifier finished with 21 verified, 0 errors
diff --git a/Chalice/tests/examples/linkedlist.output.txt b/Chalice/tests/examples/linkedlist.output.txt index b164664d..65f03446 100644 --- a/Chalice/tests/examples/linkedlist.output.txt +++ b/Chalice/tests/examples/linkedlist.output.txt @@ -1,4 +1,4 @@ -Verification of linkedlist.chalice
+Verification of linkedlist.chalice using parameters=""
49.39: Precondition at 47.14 might not hold. The expression at 47.31 might not evaluate to true.
diff --git a/Chalice/tests/examples/producer-consumer.output.txt b/Chalice/tests/examples/producer-consumer.output.txt index ebf7c738..b21044bb 100644 --- a/Chalice/tests/examples/producer-consumer.output.txt +++ b/Chalice/tests/examples/producer-consumer.output.txt @@ -1,4 +1,4 @@ -Verification of producer-consumer.chalice
+Verification of producer-consumer.chalice using parameters=""
Boogie program verifier finished with 36 verified, 0 errors
diff --git a/Chalice/tests/examples/prog0.output.txt b/Chalice/tests/examples/prog0.output.txt index 7949fa88..5b329874 100644 --- a/Chalice/tests/examples/prog0.output.txt +++ b/Chalice/tests/examples/prog0.output.txt @@ -1,4 +1,4 @@ -Verification of prog0.chalice
+Verification of prog0.chalice using parameters=""
The program did not typecheck.
3.17: undeclared member a in class C
diff --git a/Chalice/tests/examples/prog1.output.txt b/Chalice/tests/examples/prog1.output.txt index eb552ac2..61938bf7 100644 --- a/Chalice/tests/examples/prog1.output.txt +++ b/Chalice/tests/examples/prog1.output.txt @@ -1,4 +1,4 @@ -Verification of prog1.chalice
+Verification of prog1.chalice using parameters=""
9.10: Location might not be readable.
25.5: Location might not be writable
diff --git a/Chalice/tests/examples/prog2.output.txt b/Chalice/tests/examples/prog2.output.txt index 1581039d..b3ea3e93 100644 --- a/Chalice/tests/examples/prog2.output.txt +++ b/Chalice/tests/examples/prog2.output.txt @@ -1,4 +1,4 @@ -Verification of prog2.chalice
+Verification of prog2.chalice using parameters=""
24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.
31.13: Location might not be readable.
diff --git a/Chalice/tests/examples/prog3.output.txt b/Chalice/tests/examples/prog3.output.txt index 7537f222..82eeab18 100644 --- a/Chalice/tests/examples/prog3.output.txt +++ b/Chalice/tests/examples/prog3.output.txt @@ -1,4 +1,4 @@ -Verification of prog3.chalice
+Verification of prog3.chalice using parameters=""
76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true.
76.3: Method might lock/unlock more than allowed.
diff --git a/Chalice/tests/examples/prog4.output.txt b/Chalice/tests/examples/prog4.output.txt index 950c2277..62197afb 100644 --- a/Chalice/tests/examples/prog4.output.txt +++ b/Chalice/tests/examples/prog4.output.txt @@ -1,4 +1,4 @@ -Verification of prog4.chalice
+Verification of prog4.chalice using parameters=""
5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.
17.7: The target of the release statement might not be locked by the current thread.
diff --git a/Chalice/tests/examples/quantifiers.output.txt b/Chalice/tests/examples/quantifiers.output.txt index 20b0af7b..efae2ed6 100644 --- a/Chalice/tests/examples/quantifiers.output.txt +++ b/Chalice/tests/examples/quantifiers.output.txt @@ -1,4 +1,4 @@ -Verification of quantifiers.chalice
+Verification of quantifiers.chalice using parameters=""
57.29: The heap of the callee might not be strictly smaller than the heap of the caller.
diff --git a/Chalice/tests/examples/swap.output.txt b/Chalice/tests/examples/swap.output.txt index 29df3021..70bac3a2 100644 --- a/Chalice/tests/examples/swap.output.txt +++ b/Chalice/tests/examples/swap.output.txt @@ -1,4 +1,4 @@ -Verification of swap.chalice
+Verification of swap.chalice using parameters=""
Boogie program verifier finished with 5 verified, 0 errors
diff --git a/Chalice/tests/permission-model/basic.output.txt b/Chalice/tests/permission-model/basic.output.txt index 510ae7f5..9d92923a 100644 --- a/Chalice/tests/permission-model/basic.output.txt +++ b/Chalice/tests/permission-model/basic.output.txt @@ -1,4 +1,4 @@ -Verification of basic.chalice
+Verification of basic.chalice using parameters=""
28.3: The postcondition at 30.13 might not hold. Insufficient fraction at 30.13 for Cell.x.
48.3: The postcondition at 50.13 might not hold. Insufficient fraction at 50.13 for Cell.x.
diff --git a/Chalice/tests/permission-model/channels.output.txt b/Chalice/tests/permission-model/channels.output.txt index 11543925..a79b5fb1 100644 --- a/Chalice/tests/permission-model/channels.output.txt +++ b/Chalice/tests/permission-model/channels.output.txt @@ -1,4 +1,4 @@ -Verification of channels.chalice
+Verification of channels.chalice using parameters=""
8.5: The where clause at 44.24 might not hold. Insufficient fraction at 44.24 for C.f.
18.3: The postcondition at 20.13 might not hold. Insufficient fraction at 20.13 for C.f.
diff --git a/Chalice/tests/permission-model/locks.output.txt b/Chalice/tests/permission-model/locks.output.txt index c1167c3b..98cd0d4e 100644 --- a/Chalice/tests/permission-model/locks.output.txt +++ b/Chalice/tests/permission-model/locks.output.txt @@ -1,4 +1,4 @@ -Verification of locks.chalice
+Verification of locks.chalice using parameters=""
21.5: Assertion might not hold. Insufficient fraction at 21.12 for Cell.x.
24.5: Assertion might not hold. Insufficient fraction at 24.12 for Cell.x.
diff --git a/Chalice/tests/permission-model/peculiar.output.txt b/Chalice/tests/permission-model/peculiar.output.txt index fd3c0a76..6754cf7f 100644 --- a/Chalice/tests/permission-model/peculiar.output.txt +++ b/Chalice/tests/permission-model/peculiar.output.txt @@ -1,4 +1,4 @@ -Verification of peculiar.chalice
+Verification of peculiar.chalice using parameters=""
35.5: Assertion might not hold. Insufficient fraction at 35.12 for Cell.x.
diff --git a/Chalice/tests/permission-model/permarith_parser.output.txt b/Chalice/tests/permission-model/permarith_parser.output.txt index f124b714..bc6598a1 100644 --- a/Chalice/tests/permission-model/permarith_parser.output.txt +++ b/Chalice/tests/permission-model/permarith_parser.output.txt @@ -1,4 +1,4 @@ -Verification of permarith_parser.chalice
+Verification of permarith_parser.chalice using parameters=""
The program did not typecheck.
6.14: fraction in permission must be of type integer
diff --git a/Chalice/tests/permission-model/permission_arithmetic.output.txt b/Chalice/tests/permission-model/permission_arithmetic.output.txt index f735cf85..afbd9be7 100644 --- a/Chalice/tests/permission-model/permission_arithmetic.output.txt +++ b/Chalice/tests/permission-model/permission_arithmetic.output.txt @@ -1,4 +1,4 @@ -Verification of permission_arithmetic.chalice
+Verification of permission_arithmetic.chalice using parameters=""
24.5: Assertion might not hold. The permission at 24.18 might not be positive.
40.5: The precondition at 33.14 might not hold. The permission at 33.20 might not be positive.
diff --git a/Chalice/tests/permission-model/predicate_error1.output.txt b/Chalice/tests/permission-model/predicate_error1.output.txt index d7964c29..a5e27bac 100644 --- a/Chalice/tests/permission-model/predicate_error1.output.txt +++ b/Chalice/tests/permission-model/predicate_error1.output.txt @@ -1,3 +1,3 @@ -Verification of predicate_error1.chalice
+Verification of predicate_error1.chalice using parameters=""
Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error2.output.txt b/Chalice/tests/permission-model/predicate_error2.output.txt index cc580b7b..fb660013 100644 --- a/Chalice/tests/permission-model/predicate_error2.output.txt +++ b/Chalice/tests/permission-model/predicate_error2.output.txt @@ -1,3 +1,3 @@ -Verification of predicate_error2.chalice
+Verification of predicate_error2.chalice using parameters=""
Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error3.output.txt b/Chalice/tests/permission-model/predicate_error3.output.txt index 3e325f1b..9f5b503c 100644 --- a/Chalice/tests/permission-model/predicate_error3.output.txt +++ b/Chalice/tests/permission-model/predicate_error3.output.txt @@ -1,3 +1,3 @@ -Verification of predicate_error3.chalice
+Verification of predicate_error3.chalice using parameters=""
Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicate_error4.output.txt b/Chalice/tests/permission-model/predicate_error4.output.txt index 8cd03821..16da656f 100644 --- a/Chalice/tests/permission-model/predicate_error4.output.txt +++ b/Chalice/tests/permission-model/predicate_error4.output.txt @@ -1,3 +1,3 @@ -Verification of predicate_error4.chalice
+Verification of predicate_error4.chalice using parameters=""
Error: Not supported: 17.5: Scaling epsilon permissions with non-full permissions is not possible.
diff --git a/Chalice/tests/permission-model/predicates.output.txt b/Chalice/tests/permission-model/predicates.output.txt index be87e044..30c08a1a 100644 --- a/Chalice/tests/permission-model/predicates.output.txt +++ b/Chalice/tests/permission-model/predicates.output.txt @@ -1,4 +1,4 @@ -Verification of predicates.chalice
+Verification of predicates.chalice using parameters=""
37.5: Fold might fail because the definition of Cell.write1 does not hold. Insufficient fraction at 6.22 for Cell.x.
55.5: Fold might fail because the definition of Cell.read1 does not hold. Insufficient fraction at 8.21 for Cell.x.
diff --git a/Chalice/tests/permission-model/scaling.output.txt b/Chalice/tests/permission-model/scaling.output.txt index 1ff1d596..863e79d8 100644 --- a/Chalice/tests/permission-model/scaling.output.txt +++ b/Chalice/tests/permission-model/scaling.output.txt @@ -1,4 +1,4 @@ -Verification of scaling.chalice
+Verification of scaling.chalice using parameters=""
33.5: Assertion might not hold. Insufficient fraction at 33.12 for Cell.x.
36.3: The postcondition at 38.13 might not hold. Insufficient fraction at 38.13 for Cell.read1.
diff --git a/Chalice/tests/permission-model/sequences.output.txt b/Chalice/tests/permission-model/sequences.output.txt index 16dd9137..c7099103 100644 --- a/Chalice/tests/permission-model/sequences.output.txt +++ b/Chalice/tests/permission-model/sequences.output.txt @@ -1,4 +1,4 @@ -Verification of sequences.chalice
+Verification of sequences.chalice using parameters=""
36.3: The postcondition at 41.13 might not hold. Insufficient permission at 41.13 for A.f
60.3: The postcondition at 65.13 might not hold. Insufficient permission at 65.13 for A.f
diff --git a/Chalice/tests/readme.txt b/Chalice/tests/readme.txt index 0e09fb57..be0b6f91 100644 --- a/Chalice/tests/readme.txt +++ b/Chalice/tests/readme.txt @@ -31,9 +31,9 @@ Commands (sorted by relevance): current directory.
- getboogieoutput.bat: File used internally by generete_reference.bat.
+To provide additional parameters to Chalice when verifying the tests (e.g., to
+test the autoMagic feature, see tests/examples/RockBand-automagic.chalice), one
+can start the Chalice source file with the line
+ "// chalice-parameter=<list of space-separated parameters>"
-Note: There is also an alternative way to execute the tests in example, namely
-to use the script test.bat. The scripts in test-scripts allow more fine-grained
-testing, but they do not allow to use special parameters for certain tests
-(e.g. -autoMagic).
-For the refinement tests, there is a bash script test.sh, similar to test.bat.
+Note: For the refinement tests, there is a bash script test.sh.
diff --git a/Chalice/tests/test-scripts/generate_reference.bat b/Chalice/tests/test-scripts/generate_reference.bat index a2e9c443..0c480e5c 100644 --- a/Chalice/tests/test-scripts/generate_reference.bat +++ b/Chalice/tests/test-scripts/generate_reference.bat @@ -1,5 +1,4 @@ @echo off
-
set getboogieoutput="%~dp0\getboogieoutput.bat"
echo Generating reference for %1.chalice ...
diff --git a/Chalice/tests/test-scripts/generate_reference_all.bat b/Chalice/tests/test-scripts/generate_reference_all.bat index 83b04700..1e9e7cfb 100644 --- a/Chalice/tests/test-scripts/generate_reference_all.bat +++ b/Chalice/tests/test-scripts/generate_reference_all.bat @@ -1,10 +1,9 @@ @echo off
-set getboogieoutput="%~dp0\getboogieoutput.bat"
+set generatereference="%~dp0\generate_reference.bat"
for /F %%f in ('dir *.chalice /b') do (
- echo Generating reference for %%~nf.chalice ...
- call %getboogieoutput% %%~nf %1 %2 %3 %4 %5 %6 %7
+ call %generatereference% %%~nf %1 %2 %3 %4 %5 %6 %7
)
exit /b 0
diff --git a/Chalice/tests/test-scripts/getboogieoutput.bat b/Chalice/tests/test-scripts/getboogieoutput.bat index eb7d99a4..40590120 100644 --- a/Chalice/tests/test-scripts/getboogieoutput.bat +++ b/Chalice/tests/test-scripts/getboogieoutput.bat @@ -1,13 +1,33 @@ @echo off
-
set chalice="%~dp0\..\..\chalice.bat"
+set getparams="%~dp0\getparams.bat"
set output="%1.output.txt"
-echo Verification of %1.chalice > %output%
+:: get parameters
+set chaliceparameters=
+setlocal EnableDelayedExpansion
+set done=0
+set key=a
+FOR /F "usebackq tokens=1,2 delims==" %%i in (%1.chalice) do (
+
+ if !done!==0 (
+ set key=%%i
+ set param=%%j
+ )
+
+ set done=1
+)
+set str=// chalice-parameter
+if "!key!"=="!str!" (
+ set chaliceparameters=!param!
+)
+
+echo Verification of %1.chalice using parameters="%chaliceparameters%" > %output%
echo.>> %output%
-call %chalice% "%1.chalice" %2 %3 %4 %5 >> %output% 2>&1
+call %chalice% "%1.chalice" %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1
set o=%~dp1%out.bpl
if exist "%o%" copy "%o%" "%1.bpl">nul
if exist "%o%" del "%~dp1%out.bpl"
+goto :eof
diff --git a/Chalice/tests/test-scripts/reg_test.bat b/Chalice/tests/test-scripts/reg_test.bat index d31773da..0e5e4dbf 100644 --- a/Chalice/tests/test-scripts/reg_test.bat +++ b/Chalice/tests/test-scripts/reg_test.bat @@ -1,15 +1,34 @@ @echo off
-
+setlocal
set chalice="%~dp0\..\..\chalice.bat"
set diff="%~dp0\diff.bat"
if not exist "%1.chalice" goto errorNotFound
if not exist "%1.output.txt" goto errorNoRef
+:: get parameters
+set chaliceparameters=
+setlocal EnableDelayedExpansion
+set done=0
+set key=a
+FOR /F "usebackq tokens=1,2 delims==" %%i in (%1.chalice) do (
+
+ if !done!==0 (
+ set key=%%i
+ set param=%%j
+ )
+
+ set done=1
+)
+set str=// chalice-parameter
+if "!key!"=="!str!" (
+ set chaliceparameters=!param!
+)
+
set output=output.txt
-echo Verification of %1.chalice > %output%
+echo Verification of %1.chalice using parameters="%chaliceparameters%" > %output%
echo.>> %output%
-call %chalice% "%1.chalice" %2 %3 %4 %5 %6 %7 >> %output% 2>&1
+call %chalice% "%1.chalice" %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1
fc "%1.output.txt" output.txt > nul
if not errorlevel 1 goto passTest
@@ -27,11 +46,13 @@ goto errorEnd :errorEnd
if exist out.bpl del out.bpl
if exist output.txt del output.txt
+endlocal
exit /b 1
:end
if exist out.bpl del out.bpl
if exist output.txt del output.txt
+endlocal
exit /b 0
:errorNotFound
diff --git a/Chalice/tests/test-scripts/test.bat b/Chalice/tests/test-scripts/test.bat index 321fdcef..ca66d3b6 100644 --- a/Chalice/tests/test-scripts/test.bat +++ b/Chalice/tests/test-scripts/test.bat @@ -1,13 +1,33 @@ @echo off
set chalice="%~dp0\..\..\chalice.bat"
+set getparams="%~dp0\getparams.bat"
if not exist "%1.chalice" goto errorNotFound
+:: get parameters
+set chaliceparameters=
+setlocal EnableDelayedExpansion
+set done=0
+set key=a
+FOR /F "usebackq tokens=1,2 delims==" %%i in (%1.chalice) do (
+
+ if !done!==0 (
+ set key=%%i
+ set param=%%j
+ )
+
+ set done=1
+)
+set str=// chalice-parameter
+if "!key!"=="!str!" (
+ set chaliceparameters=!param!
+)
+
set output=output.txt
-echo Verification of %1.chalice > %output%
+echo Verification of %1.chalice using parameters="%chaliceparameters%" > %output%
echo.>> %output%
-call %chalice% "%1.chalice" %2 %3 %4 %5 %6 %7 >> %output% 2>&1
+call %chalice% "%1.chalice" %chaliceparameters% %2 %3 %4 %5 %6 %7 >> %output% 2>&1
type %output%
exit /B 0
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index af0926fe..95078433 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -19,6 +19,8 @@ </FileUpgradeFlags>
<OldToolsVersion>3.5</OldToolsVersion>
<UpgradeBackupLocation />
+ <IsWebBootstrapper>false</IsWebBootstrapper>
+ <TargetFrameworkProfile />
<PublishUrl>publish\</PublishUrl>
<Install>true</Install>
<InstallFrom>Disk</InstallFrom>
@@ -31,17 +33,15 @@ <MapFileExtensions>true</MapFileExtensions>
<ApplicationRevision>0</ApplicationRevision>
<ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
<UseApplicationTrust>false</UseApplicationTrust>
<BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile />
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
<OutputPath>..\..\Binaries\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DefineConstants>TRACE;DEBUG</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 22264c8f..4a9c531b 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -136,6 +136,7 @@ namespace Microsoft.Boogie { public bool NoTypecheck = false;
public bool OverlookBoogieTypeErrors = false;
public bool Verify = true;
+ public bool DisallowSoundnessCheating = false;
public bool TraceVerify = false;
public int /*(0:3)*/ ErrorTrace = 1;
public bool IntraproceduralInfer = true;
@@ -143,6 +144,7 @@ namespace Microsoft.Boogie { public bool UseUncheckedContracts = false;
public bool SimplifyLogFileAppend = false;
public bool SoundnessSmokeTest = false;
+ public string Z3ExecutablePath = null;
private bool noConsistencyChecks = false;
public bool NoConsistencyChecks {
@@ -720,6 +722,15 @@ namespace Microsoft.Boogie { break;
}
+ case "-noCheating":
+ case "/noCheating": {
+ int cheat = 0; // 0 is default, allows cheating
+ if (ps.GetNumericArgument(ref cheat, 2)) {
+ DisallowSoundnessCheating = cheat == 1;
+ }
+ break;
+ }
+
case "-contracts":
case "/contracts":
case "-c":
@@ -1378,6 +1389,13 @@ namespace Microsoft.Boogie { }
break;
+ case "-z3exe":
+ case "/z3exe":
+ if (ps.ConfirmArgumentCount(1)) {
+ Z3ExecutablePath = args[ps.i];
+ }
+ break;
+
default:
Contract.Assume(true);
bool option = false;
@@ -2101,6 +2119,8 @@ namespace Microsoft.Boogie { program, compile Dafny program to C# program out.cs
2 - always attempt to compile Dafny program to C# program
out.cs, regardless of verification outcome
+ /noCheating:<n> : 0 (default) - allow assume statements and free invariants
+ 1 - treat all assumptions as asserts, and drop free.
---- Boogie options --------------------------------------------------------
@@ -2323,6 +2343,7 @@ namespace Microsoft.Boogie { /z3types : generate multi-sorted VC that make use of Z3 types
/z3lets:<n> : 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,
3 - (default) any
+ /z3exe:<path> : path to Z3 executable
");
}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index e16470c3..d1c77122 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2517,19 +2517,20 @@ namespace Microsoft.Dafny { if (!wellformednessProc) {
string comment = "user-defined preconditions";
foreach (MaybeFreeExpression p in m.Req) {
- if (p.IsFree) {
+ if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {
req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
foreach (var s in TrSplitExpr(p.E, etran, out splitHappened)) {
req.Add(Requires(s.E.tok, s.IsFree, s.E, null, null));
+ // the free here is not linked to the free on the original expression (this is free things generated in the splitting.)
}
}
comment = null;
}
comment = "user-defined postconditions";
if (!skipEnsures) foreach (MaybeFreeExpression p in m.Ens) {
- if (p.IsFree) {
+ if (p.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {
ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment));
} else {
bool splitHappened; // we actually don't care
@@ -3001,27 +3002,31 @@ namespace Microsoft.Dafny { Contract.Requires(locals != null);
Contract.Requires(etran != null);
Contract.Requires(currentMethod != null && predef != null);
- if (stmt is AssertStmt) {
- AddComment(builder, stmt, "assert statement");
- AssertStmt s = (AssertStmt)stmt;
- TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
- bool splitHappened;
- var ss = TrSplitExpr(s.Expr, etran, out splitHappened);
- if (!splitHappened) {
- builder.Add(Assert(s.Expr.tok, etran.TrExpr(s.Expr), "assertion violation"));
- } else {
- foreach (var split in ss) {
- if (!split.IsFree) {
- builder.Add(AssertNS(split.E.tok, split.E, "assertion violation"));
+ if (stmt is PredicateStmt) {
+ if (stmt is AssertStmt || CommandLineOptions.Clo.DisallowSoundnessCheating) {
+ AddComment(builder, stmt, "assert statement");
+ PredicateStmt s = (PredicateStmt)stmt;
+ TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
+ bool splitHappened;
+ var ss = TrSplitExpr(s.Expr, etran, out splitHappened);
+ if (!splitHappened) {
+ builder.Add(Assert(s.Expr.tok, etran.TrExpr(s.Expr), "assertion violation"));
+ }
+ else {
+ foreach (var split in ss) {
+ if (!split.IsFree) {
+ builder.Add(AssertNS(split.E.tok, split.E, "assertion violation"));
+ }
}
+ builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
}
+ }
+ else if (stmt is AssumeStmt) {
+ AddComment(builder, stmt, "assume statement");
+ AssumeStmt s = (AssumeStmt)stmt;
+ TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
}
- } else if (stmt is AssumeStmt) {
- AddComment(builder, stmt, "assume statement");
- AssumeStmt s = (AssumeStmt)stmt;
- TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);
- builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));
} else if (stmt is PrintStmt) {
AddComment(builder, stmt, "print statement");
PrintStmt s = (PrintStmt)stmt;
@@ -3030,7 +3035,7 @@ namespace Microsoft.Dafny { TrStmt_CheckWellformed(arg.E, builder, locals, etran, false);
}
}
-
+
} else if (stmt is BreakStmt) {
AddComment(builder, stmt, "break statement");
var s = (BreakStmt)stmt;
@@ -3100,11 +3105,11 @@ namespace Microsoft.Dafny { Bpl.Expr wh = GetWhereClause(stmt.Tok, new Bpl.IdentifierExpr(stmt.Tok, s.UniqueName, varType), s.Type, etran);
Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, s.UniqueName, varType, wh));
locals.Add(var);
-
+
} else if (stmt is CallStmt) {
AddComment(builder, stmt, "call statement");
TrCallStmt((CallStmt)stmt, builder, locals, etran, null);
-
+
} else if (stmt is BlockStmt) {
foreach (Statement ss in ((BlockStmt)stmt).Body) {
TrStmt(ss, builder, locals, etran);
@@ -3201,7 +3206,7 @@ namespace Microsoft.Dafny { oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, boxO)));
}
oInS = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS);
-
+
// range
Bpl.Expr qr = new Bpl.ForallExpr(s.Range.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(s.Range, etran)));
builder.Add(AssertNS(s.Range.tok, qr, "range expression must be well defined"));
@@ -3209,7 +3214,7 @@ namespace Microsoft.Dafny { // sequence of asserts and assumes and uses
foreach (PredicateStmt ps in s.BodyPrefix) {
- if (ps is AssertStmt) {
+ if (ps is AssertStmt || CommandLineOptions.Clo.DisallowSoundnessCheating) {
Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(ps.Expr, etran)));
builder.Add(AssertNS(ps.Expr.tok, q, "assert condition must be well defined")); // totality check
bool splitHappened;
@@ -3249,7 +3254,7 @@ namespace Microsoft.Dafny { Bpl.Expr qqq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), bbb);
builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined")); // totality check
}
-
+
// Here comes: assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);
Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));
Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
@@ -3407,7 +3412,7 @@ namespace Microsoft.Dafny { invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));
invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));
- if (loopInv.IsFree) {
+ if (loopInv.IsFree && !CommandLineOptions.Clo.DisallowSoundnessCheating) {
invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));
} else {
bool splitHappened;
diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index 95d8950a..497911ab 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -239,6 +239,10 @@ namespace Microsoft.Boogie.Simplify { Contract.Requires(proverExe != null);
Contract.Ensures(_proverPath != null);
+ if (CommandLineOptions.Clo.Z3ExecutablePath != null) {
+ _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;
+ }
+
if (_proverPath == null) {
// Initialize '_proverPath'
_proverPath = Path.Combine(CodebaseString(), proverExe);
diff --git a/Source/version.cs b/Source/version.cs index 2804c330..fd211b1c 100644 --- a/Source/version.cs +++ b/Source/version.cs @@ -1,8 +1,12 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
+// ==++==
+//
+//
+//
+// ==--==
+// Warning: Automatically generated file. DO NOT EDIT
+// Generated at Dienstag, 5. Juli 2011 11:26:45
+
using System.Reflection;
-[assembly: AssemblyVersion("2.0.0.0")]
-[assembly: AssemblyFileVersion("2.0.0.0")]
+[assembly: AssemblyVersion("2.2.30705.1126")]
+[assembly: AssemblyFileVersion("2.2.30705.1126")]
+
diff --git a/Source/version.ssc b/Source/version.ssc index 2804c330..fd211b1c 100644 --- a/Source/version.ssc +++ b/Source/version.ssc @@ -1,8 +1,12 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
+// ==++==
+//
+//
+//
+// ==--==
+// Warning: Automatically generated file. DO NOT EDIT
+// Generated at Dienstag, 5. Juli 2011 11:26:45
+
using System.Reflection;
-[assembly: AssemblyVersion("2.0.0.0")]
-[assembly: AssemblyFileVersion("2.0.0.0")]
+[assembly: AssemblyVersion("2.2.30705.1126")]
+[assembly: AssemblyFileVersion("2.2.30705.1126")]
+
|