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}

1 files changed, 15 insertions, 15 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index ed61b709..aa132c5d 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -163,8 +163,7 @@ namespace Microsoft.Boogie {
           return;

         }

 

-        oc = EliminateDeadVariablesAndInline(program);

-        //BoogiePL.Errors.count = 0;

+        EliminateDeadVariablesAndInline(program);

 

         int errorCount, verified, inconclusives, timeOuts, outOfMemories;

         oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

@@ -363,7 +362,7 @@ namespace Microsoft.Boogie {
       return PipelineOutcome.ResolvedAndTypeChecked;

     }

 

-    static PipelineOutcome EliminateDeadVariablesAndInline(Program program) {

+    static void EliminateDeadVariablesAndInline(Program program) {

       Contract.Requires(program != null);

       // Eliminate dead variables

       Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);

@@ -379,33 +378,31 @@ namespace Microsoft.Boogie {
       }

 

       // Inline

-      // In Spec#, there was no run-time test. The type was just List<Declaration!>

-      List<Declaration> TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);

-      

+      var TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);

       

       if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {

         bool inline = false;

-        foreach (Declaration d in TopLevelDeclarations) {

+        foreach (var d in TopLevelDeclarations) {

           if (d.FindExprAttribute("inline") != null) {

             inline = true;

           }

         }

         if (inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) {

-          foreach (Declaration d in TopLevelDeclarations) {

-            Implementation impl = d as Implementation;

+          foreach (var d in TopLevelDeclarations) {

+            var impl = d as Implementation;

             if (impl != null) {

               impl.OriginalBlocks = impl.Blocks;

               impl.OriginalLocVars = impl.LocVars;

             }

           }

-          foreach (Declaration d in TopLevelDeclarations) {

-            Implementation impl = d as Implementation;

+          foreach (var d in TopLevelDeclarations) {

+            var impl = d as Implementation;

             if (impl != null && !impl.SkipVerification) {

               Inliner.ProcessImplementation(program, impl);

             }

           }

-          foreach (Declaration d in TopLevelDeclarations) {

-            Implementation impl = d as Implementation;

+          foreach (var d in TopLevelDeclarations) {

+            var impl = d as Implementation;

             if (impl != null) {

               impl.OriginalBlocks = null;

               impl.OriginalLocVars = null;

@@ -413,7 +410,6 @@ namespace Microsoft.Boogie {
           }

         }

       }

-      return PipelineOutcome.Done;

     }

 

     /// <summary>

@@ -434,7 +430,11 @@ namespace Microsoft.Boogie {
       // ---------- 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.ContractInfer) {

         Houdini.Houdini houdini = new Houdini.Houdini(program, true);