diff options
author | 2011-12-05 23:07:06 -0800 | |
---|---|---|
committer | 2011-12-05 23:07:06 -0800 | |
commit | 3a7eade26fe538317ceff5335f808aee4d80e438 (patch) | |
tree | ca9fe0e3b3060d680171f025754cba6e6b5ee6ee | |
parent | 38027f14460e51c0f65e4575d240b7906235ad9e (diff) |
Boogie: Added new abstract interpretation harness, which uses native Boogie Expr's, not the more abstract AIExpr's.
Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false.
Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals
Boogie: Mark all inferred conditions with attribute {:inferred}
-rw-r--r-- | DafnyDriver/DafnyDriver.cs | 62 | ||||
-rw-r--r-- | Test/dafny0/Answer | 28 |
2 files changed, 58 insertions, 32 deletions
diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs index 80e24356..648fd84f 100644 --- a/DafnyDriver/DafnyDriver.cs +++ b/DafnyDriver/DafnyDriver.cs @@ -378,11 +378,11 @@ namespace Microsoft.Dafny /// </summary>
static PipelineOutcome BoogiePipelineWithRerun (Bpl.Program/*!*/ program, string/*!*/ bplFileName,
out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)
- {Contract.Requires(program != null);
- Contract.Requires(bplFileName != null);
+ {
+ Contract.Requires(program != null);
+ Contract.Requires(bplFileName != null);
Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
-
errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
PipelineOutcome oc = ResolveAndTypecheck(program, bplFileName);
switch (oc) {
@@ -407,6 +407,7 @@ namespace Microsoft.Dafny return oc;
case PipelineOutcome.ResolvedAndTypeChecked:
+ EliminateDeadVariablesAndInline(program);
return InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
default:
@@ -414,6 +415,55 @@ namespace Microsoft.Dafny }
}
+ static void EliminateDeadVariablesAndInline(Bpl.Program program) {
+ Contract.Requires(program != null);
+ // Eliminate dead variables
+ Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+
+ // Collect mod sets
+ if (CommandLineOptions.Clo.DoModSetAnalysis) {
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
+ }
+
+ // Coalesce blocks
+ if (CommandLineOptions.Clo.CoalesceBlocks) {
+ Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+ }
+
+ // Inline
+ var TopLevelDeclarations = program.TopLevelDeclarations;
+
+ if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {
+ bool inline = false;
+ foreach (var d in TopLevelDeclarations) {
+ if (d.FindExprAttribute("inline") != null) {
+ inline = true;
+ }
+ }
+ if (inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) {
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ }
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
+ if (impl != null && !impl.SkipVerification) {
+ Inliner.ProcessImplementation(program, impl);
+ }
+ }
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+ }
+ }
+ }
+ }
enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }
enum ExitValue { VERIFIED = 0, PREPROCESSING_ERROR, DAFNY_ERROR, NOT_VERIFIED }
@@ -477,7 +527,11 @@ namespace Microsoft.Dafny // ---------- Infer invariants --------------------------------------------------------
// Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
- Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
+ if (CommandLineOptions.Clo.Ai.J_Intervals || CommandLineOptions.Clo.Ai.J_Trivial) {
+ Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+ } else {
+ Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
+ }
if (CommandLineOptions.Clo.LoopUnrollCount != -1) {
program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 15cec24f..aab1990d 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -307,7 +307,6 @@ Execution trace: (0,0): anon0
Definedness.dfy(105,15): Error: possible division by zero
Execution trace:
- (0,0): anon0
Definedness.dfy(105,5): anon8_LoopHead
(0,0): anon8_LoopBody
Definedness.dfy(105,5): anon9_Else
@@ -799,13 +798,11 @@ Execution trace: ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon71_Then
ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
@@ -821,20 +818,17 @@ Execution trace: ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon71_Then
ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
ControlStructures.dfy(210,9): anon73_Else
(0,0): anon20
ControlStructures.dfy(210,9): anon74_Else
- (0,0): anon22
(0,0): anon75_Then
(0,0): after_4
ControlStructures.dfy(221,7): anon77_LoopHead
@@ -842,7 +836,6 @@ Execution trace: ControlStructures.dfy(221,7): anon78_Else
(0,0): anon33
ControlStructures.dfy(221,7): anon79_Else
- (0,0): anon35
(0,0): anon81_Then
(0,0): anon38
(0,0): after_9
@@ -856,13 +849,11 @@ Execution trace: ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon68_Then
(0,0): after_5
(0,0): anon87_Then
@@ -876,20 +867,17 @@ Execution trace: ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon71_Then
ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
ControlStructures.dfy(210,9): anon73_Else
(0,0): anon20
ControlStructures.dfy(210,9): anon74_Else
- (0,0): anon22
(0,0): anon75_Then
(0,0): after_4
ControlStructures.dfy(221,7): anon77_LoopHead
@@ -897,7 +885,6 @@ Execution trace: ControlStructures.dfy(221,7): anon78_Else
(0,0): anon33
ControlStructures.dfy(221,7): anon79_Else
- (0,0): anon35
(0,0): anon82_Then
(0,0): anon85_Then
(0,0): after_8
@@ -915,7 +902,6 @@ Execution trace: Termination.dfy(105,3): anon8_Else
(0,0): anon3
Termination.dfy(105,3): anon9_Else
- (0,0): anon5
Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
@@ -925,7 +911,6 @@ Execution trace: (0,0): anon11_Then
(0,0): anon5
Termination.dfy(113,3): anon12_Else
- (0,0): anon7
Termination.dfy(122,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
@@ -935,7 +920,6 @@ Execution trace: (0,0): anon11_Then
(0,0): anon5
Termination.dfy(122,3): anon12_Else
- (0,0): anon7
Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
(0,0): anon0
@@ -945,7 +929,6 @@ Execution trace: (0,0): anon11_Then
(0,0): anon5
Termination.dfy(122,3): anon12_Else
- (0,0): anon7
Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon6_Else
@@ -959,7 +942,6 @@ Execution trace: Termination.dfy(291,3): anon11_Else
Termination.dfy(291,3): anon12_Else
(0,0): anon13_Else
- (0,0): anon8
Dafny program verifier finished with 45 verified, 6 errors
@@ -1131,7 +1113,6 @@ Execution trace: TypeParameters.dfy(153,3): anon22_Else
(0,0): anon13
TypeParameters.dfy(153,3): anon24_Else
- (0,0): anon15
Dafny program verifier finished with 35 verified, 5 errors
@@ -1224,7 +1205,6 @@ Execution trace: LoopModifies.dfy(14,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(14,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1233,7 +1213,6 @@ Execution trace: LoopModifies.dfy(42,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(42,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1242,7 +1221,6 @@ Execution trace: LoopModifies.dfy(57,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(57,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause
Execution trace:
(0,0): anon0
@@ -1254,7 +1232,6 @@ Execution trace: LoopModifies.dfy(90,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(90,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(146,11): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1263,13 +1240,11 @@ Execution trace: LoopModifies.dfy(134,4): anon18_Else
(0,0): anon5
LoopModifies.dfy(134,4): anon20_Else
- (0,0): anon7
LoopModifies.dfy(139,7): anon21_LoopHead
(0,0): anon21_LoopBody
LoopModifies.dfy(139,7): anon22_Else
(0,0): anon12
LoopModifies.dfy(139,7): anon24_Else
- (0,0): anon14
LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1278,7 +1253,6 @@ Execution trace: LoopModifies.dfy(193,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(193,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(285,13): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1287,13 +1261,11 @@ Execution trace: LoopModifies.dfy(273,4): anon18_Else
(0,0): anon5
LoopModifies.dfy(273,4): anon20_Else
- (0,0): anon7
LoopModifies.dfy(281,7): anon21_LoopHead
(0,0): anon21_LoopBody
LoopModifies.dfy(281,7): anon22_Else
(0,0): anon12
LoopModifies.dfy(281,7): anon24_Else
- (0,0): anon14
Dafny program verifier finished with 23 verified, 9 errors
|