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}

4 files changed, 29 insertions, 10 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 0aaf3c46..402905a3 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2745,13 +2745,15 @@ namespace Microsoft.Boogie {
             CmdSeq newCommands = new CmdSeq();

             if (instrumentEntry) {

               Expr inv = (Expr)b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/

-              PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);

+              var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);

+              PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv, kv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv, kv);

               newCommands.Add(cmd);

             }

             newCommands.AddRange(b.Cmds);

             if (instrumentExit) {

               Expr inv = (Expr)b.Lattice.ToPredicate(b.PostInvariant);

-              PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);

+              var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);

+              PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv, kv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv, kv);

               newCommands.Add(cmd);

             }

             b.Cmds = newCommands;

@@ -3537,12 +3539,6 @@ namespace Microsoft.Boogie {
         d.Emit(stream, 0);

       }

     }

-    public void InstrumentWithInvariants() {

-      foreach (Declaration/*!*/ d in this) {

-        Contract.Assert(d != null);

-        d.InstrumentWithInvariants();

-      }

-    }

   }

   #endregion

 

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 676ffd5a..06eb3ae5 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -800,6 +800,7 @@ namespace Microsoft.Boogie {
     };     // used by WidenPoints.Compute

     public VisitState TraversingStatus;

 

+    public int aiId;  // block ID used by the abstract interpreter, which may change these numbers with each AI run

     public bool widenBlock;

     public int iterations;         // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not

 

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 9a0fe64e..fe5f0621 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -438,6 +438,7 @@ namespace Microsoft.Boogie {
       : base(tok) {

       Contract.Requires(tok != null);

       Val = b;

+      Type = Type.Bool;

     }

     /// <summary>

     /// Creates a literal expression for the integer value "v".

@@ -448,6 +449,7 @@ namespace Microsoft.Boogie {
       : base(tok) {

       Contract.Requires(tok != null);

       Val = v;

+      Type = Type.Int;

     }

 

     /// <summary>

@@ -456,7 +458,9 @@ namespace Microsoft.Boogie {
     public LiteralExpr(IToken/*!*/ tok, BigNum v, int b)

       : base(tok) {

       Contract.Requires(tok != null);

+      Contract.Requires(0 <= b);

       Val = new BvConst(v, b);

+      Type = Type.GetBvType(b);

     }

 

     [Pure]

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 2f02f0e5..9413cf30 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -604,6 +604,8 @@ namespace Microsoft.Boogie {
       public bool DynamicType = false;

       public bool Nullness = false;

       public bool Polyhedra = false;

+      public bool J_Trivial = false;

+      public bool J_Intervals = false;

       public bool DebugStatistics = false;

 

       public bool AnySet {

@@ -612,7 +614,9 @@ namespace Microsoft.Boogie {
               || Constant

               || DynamicType

               || Nullness

-              || Polyhedra;

+              || Polyhedra

+              || J_Trivial

+              || J_Intervals;

         }

       }

     }

@@ -645,6 +649,14 @@ namespace Microsoft.Boogie {
                   Ai.Polyhedra = true;

                   UseAbstractInterpretation = true;

                   break;

+                case 't':

+                  Ai.J_Trivial = true;

+                  UseAbstractInterpretation = true;

+                  break;

+                case 'j':

+                  Ai.J_Intervals = true;

+                  UseAbstractInterpretation = true;

+                  break;

                 case 's':

                   Ai.DebugStatistics = true;

                   UseAbstractInterpretation = true;

@@ -1458,6 +1470,11 @@ namespace Microsoft.Boogie {
                    d = dynamic type

                    n = nullness

                    p = polyhedra for linear inequalities

+                   t = trivial bottom/top lattice (cannot be combined with

+                       other domains)

+                   j = stronger intervals (cannot be combined with other

+                       domains)

+                or the following (which denote options, not domains):

                    s = debug statistics

                 0..9 = number of iterations before applying a widen (default=0)

   /noinfer      turn off the default inference, and overrides the /infer

@@ -1473,7 +1490,8 @@ namespace Microsoft.Boogie {
                 h - instrument inferred invariants only at beginning of

                     loop headers (default)

                 e - instrument inferred invariants at beginning and end

-                    of every block

+                    of every block (this mode is intended for use in

+                    debugging of abstract domains)

   /printInstrumented

                 print Boogie program after it has been instrumented with

                 invariants