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}

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