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, 320 insertions, 0 deletions

diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs
new file mode 100644
index 00000000..7b236481
--- /dev/null
+++ b/Source/AbsInt/NativeLattice.cs
@@ -0,0 +1,320 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+

+using System;

+using System.Collections.Generic;

+using System.Text;

+using System.Diagnostics.Contracts;

+using Microsoft.Boogie;

+using IMutableSet = Microsoft.Boogie.Set;

+using ISet = Microsoft.Boogie.Set;

+using HashSet = Microsoft.Boogie.Set;

+using ArraySet = Microsoft.Boogie.Set;

+

+namespace Microsoft.Boogie.AbstractInterpretation

+{

+  /// <summary>

+  ///  Specifies the operations (e.g., join) on a mathematical lattice that depend

+  ///  only on the elements of the lattice.

+  /// </summary>

+  public abstract class NativeLattice

+  {

+    /// <summary>

+    ///  An element of the lattice.  This class should be derived from in any

+    ///  implementation of MathematicalLattice.

+    /// </summary>

+    public abstract class Element

+    {

+      public abstract Expr ToExpr();

+    }

+

+    public abstract Element Top { get; }

+    public abstract Element Bottom { get; }

+

+    public abstract bool IsTop(Element element);

+    public abstract bool IsBottom(Element element);

+

+    /// <summary>

+    /// Is 'a' better (or equal) information than 'b'?  That is, is 'a' below 'b' in the lattice?

+    /// </summary>

+    public abstract bool Below(Element a, Element b);

+

+    public abstract Element Meet(Element a, Element b);

+    public abstract Element Join(Element a, Element b);

+    public abstract Element Widen(Element a, Element b);

+

+    public abstract Element Constrain(Element element, Expr expr);

+    public abstract Element Update(Element element, AssignCmd cmd);  // requiers 'cmd' to be a simple (possibly parallel) assignment command

+    public abstract Element Eliminate(Element element, Variable v);

+

+    public virtual void Validate() {

+      Contract.Assert(IsTop(Top));

+      Contract.Assert(IsBottom(Bottom));

+      Contract.Assert(!IsBottom(Top));

+      Contract.Assert(!IsTop(Bottom));

+

+      Contract.Assert(Below(Top, Top));

+      Contract.Assert(Below(Bottom, Top));

+      Contract.Assert(Below(Bottom, Bottom));

+

+      Contract.Assert(IsTop(Join(Top, Top)));

+      Contract.Assert(IsBottom(Join(Bottom, Bottom)));

+    }

+  }

+

+  public class NativeAbstractInterpretation

+  {

+    public static void RunAbstractInterpretation(Program program) {

+      Contract.Requires(program != null);

+

+      if (!CommandLineOptions.Clo.UseAbstractInterpretation) {

+        return;

+      }

+      Helpers.ExtraTraceInformation("Starting abstract interpretation");

+

+      DateTime start = new DateTime();  // to please compiler's definite assignment rules

+      if (CommandLineOptions.Clo.Trace) {

+        Console.WriteLine();

+        Console.WriteLine("Running abstract interpretation...");

+        start = DateTime.Now;

+      }

+

+      WidenPoints.Compute(program);

+

+      NativeLattice lattice = null;

+      if (CommandLineOptions.Clo.Ai.J_Trivial) {

+        lattice = new TrivialDomain();

+      } else if (CommandLineOptions.Clo.Ai.J_Intervals) {

+        lattice = new NativeIntervallDomain();

+      }

+

+      if (lattice != null) {

+        Dictionary<Procedure, Implementation[]> procedureImplementations = AbstractionEngine.ComputeProcImplMap(program);

+        ComputeProgramInvariants(program, procedureImplementations, lattice);

+        if (CommandLineOptions.Clo.Ai.DebugStatistics) {

+          Console.Error.WriteLine(lattice);

+        }

+      }

+

+      if (CommandLineOptions.Clo.Trace) {

+        DateTime end = DateTime.Now;

+        TimeSpan elapsed = end - start;

+        Console.WriteLine("  [{0} s]", elapsed.TotalSeconds);

+        Console.Out.Flush();

+      }

+    }

+

+    /// <summary>

+    /// Compute and apply the invariants for the program using the underlying abstract domain (using native Boogie

+    /// expressions, not the abstracted AI.Expr's).

+    /// </summary>

+    public static void ComputeProgramInvariants(Program program, Dictionary<Procedure, Implementation[]> procedureImplementations, NativeLattice lattice) {

+      Contract.Requires(program != null);

+      Contract.Requires(procedureImplementations != null);

+      Contract.Requires(lattice != null);

+

+      // Gather all the axioms to create the initial lattice element

+      // Differently stated, it is the \alpha from axioms (i.e. first order formulae) to the underlyng abstract domain

+      var initialElement = lattice.Top;

+      Contract.Assert(initialElement != null);

+      foreach (var decl in program.TopLevelDeclarations) {

+        var ax = decl as Axiom;

+        if (ax != null) {

+          initialElement = lattice.Constrain(initialElement, ax.Expr);

+        }

+      }

+

+      // analyze each procedure

+      foreach (var decl in program.TopLevelDeclarations) {

+        var proc = decl as Procedure;

+        if (proc != null && procedureImplementations.ContainsKey(proc)) {

+          // analyze each implementation of the procedure

+          foreach (var impl in procedureImplementations[proc]) {

+            // add the precondition to the axioms

+            Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());

+            var start = initialElement;

+            foreach (Requires pre in proc.Requires) {

+              Expr e = Substituter.Apply(formalProcImplSubst, pre.Condition);

+              start = lattice.Constrain(start, e);

+            }

+            Analyze(impl, lattice, start);

+          }

+        }

+      }

+    }

+

+    public static void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.Element start) {

+      // We need to keep track of some information for each(some) block(s).  To do that efficiently,

+      // we number the implementation's blocks sequentially, and then we can use arrays to store

+      // the additional information.

+      var pre = new NativeLattice.Element[impl.Blocks.Count];  // set to null if we never compute a join/widen at this block

+      var post = CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere ? new NativeLattice.Element[impl.Blocks.Count] : null;

+      var iterations = new int[impl.Blocks.Count];

+      var bottom = lattice.Bottom;

+      int n = 0;

+      foreach (var block in impl.Blocks) {

+        block.aiId = n;

+        // Note:  The forward analysis below will store lattice elements in pre[n] if pre[n] is non-null.

+        // Thus, the assignment "pre[n] = bottom;" below must be done under the following condition:

+        //    n == 0 || block.widenBlock

+        // One possible strategy would be to do it only under that condition.  Alternatively,

+        // one could do the assignment under the following condition:

+        //    n == 0 || block.widenBlock || block.Predecessors.Length != 1

+        // (which would require first setting the Predecessors field).  In any case, if

+        //    CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere

+        // then all pre[n] should be set.

+        pre[n] = bottom;

+        n++;

+      }

+      Contract.Assert(n == impl.Blocks.Count);

+

+      var workItems = new Queue<Tuple<Block, NativeLattice.Element>>();

+      workItems.Enqueue(new Tuple<Block, NativeLattice.Element>(impl.Blocks[0], start));

+      //ComputeBlockInvariantsNative(impl, );

+      // compute a fixpoint here

+      while (workItems.Count > 0) {

+        var workItem = workItems.Dequeue();

+        var b = workItem.Item1;

+        var id = b.aiId;

+        var e = workItem.Item2;

+        if (pre[id] == null) {

+          // no pre information stored here, so just go ahead through the block

+        } else if (lattice.Below(e, pre[id])) {

+          // no change

+          continue;

+        } else if (b.widenBlock && CommandLineOptions.Clo.StepsBeforeWidening <= iterations[id]) {

+          e = lattice.Widen(pre[id], e);

+          pre[id] = e;

+          iterations[id]++;

+        } else {

+          e = lattice.Join(pre[id], e);

+          pre[id] = e;

+          iterations[id]++;

+        }

+

+        // propagate'e' through b.Cmds

+        foreach (Cmd cmd in b.Cmds) {

+          e = Step(lattice, cmd, e);

+        }

+

+        if (post != null && pre[id] != null) {

+          post[id] = e;

+        }

+

+        var g = b.TransferCmd as GotoCmd;

+        if (g != null) {  // if g==null, it's a pity we didn't pay attention to that earlier, because then we could have skipped analyzing the code in this block

+          foreach (Block succ in g.labelTargets) {

+            workItems.Enqueue(new Tuple<Block, NativeLattice.Element>(succ, e));

+          }

+        }

+      }

+

+      Instrument(impl, pre, post);

+    }

+

+    static void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.Element[] post) {

+      Contract.Requires(impl != null);

+      Contract.Requires(pre != null);

+

+      foreach (var b in impl.Blocks) {

+        var element = pre[b.aiId];

+        if (element != null && (b.widenBlock || CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere)) {

+          CmdSeq newCommands = new CmdSeq();

+          Expr inv = element.ToExpr();

+          PredicateCmd cmd;

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

+          if (CommandLineOptions.Clo.InstrumentWithAsserts) {

+            cmd = new AssertCmd(Token.NoToken, inv, kv);

+          } else {

+            cmd = new AssumeCmd(Token.NoToken, inv, kv);

+          }

+          newCommands.Add(cmd);

+          newCommands.AddRange(b.Cmds);

+          if (post != null && post[b.aiId] != null) {

+            inv = post[b.aiId].ToExpr();

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

+            if (CommandLineOptions.Clo.InstrumentWithAsserts) {

+              cmd = new AssertCmd(Token.NoToken, inv, kv);

+            } else {

+              cmd = new AssumeCmd(Token.NoToken, inv, kv);

+            }

+            newCommands.Add(cmd);

+          }

+          b.Cmds = newCommands;  // destructively replace the commands of the block

+        }

+      }

+    }

+

+    /// <summary>

+    /// The abstract transition relation.

+    /// 'cmd' is allowed to be a StateCmd.

+    /// </summary>

+    static NativeLattice.Element Step(NativeLattice lattice, Cmd cmd, NativeLattice.Element elmt) {

+      Contract.Requires(lattice != null);

+      Contract.Requires(cmd != null);

+      Contract.Requires(elmt != null);

+      Contract.Ensures(Contract.Result<NativeLattice.Element>() != null);

+

+      if (cmd is AssignCmd) { // parallel assignment

+        var c = (AssignCmd)cmd;

+        elmt = lattice.Update(elmt, c.AsSimpleAssignCmd);

+      } else if (cmd is HavocCmd) {

+        var c = (HavocCmd)cmd;

+        foreach (IdentifierExpr id in c.Vars) {

+          Contract.Assert(id != null);

+          elmt = lattice.Eliminate(elmt, id.Decl);

+        }

+      } else if (cmd is PredicateCmd) {

+        var c = (PredicateCmd)cmd;

+        var conjuncts = new List<Expr>();

+        foreach (var ee in Conjuncts(c.Expr)) {

+          Contract.Assert(ee != null);

+          elmt = lattice.Constrain(elmt, ee);

+        }

+      } else if (cmd is StateCmd) {

+        var c = (StateCmd)cmd;

+        // Iterate the abstract transition on all the commands in the desugaring of the call

+        foreach (Cmd callDesug in c.Cmds) {

+          Contract.Assert(callDesug != null);

+          elmt = Step(lattice, callDesug, elmt);

+        }

+        // Project out the local variables of the StateCmd

+        foreach (Variable local in c.Locals) {

+          Contract.Assert(local != null);

+          elmt = lattice.Eliminate(elmt, local);

+        }

+      } else if (cmd is SugaredCmd) {

+        var c = (SugaredCmd)cmd;

+        elmt = Step(lattice, c.Desugaring, elmt);

+      } else if (cmd is CommentCmd) {

+        // skip

+      } else {

+        Contract.Assert(false);  // unknown command

+      }

+      return elmt;

+    }

+

+    /// <summary>

+    /// Yields the conjuncts of 'expr'.

+    /// </summary>

+    public static IEnumerable<Expr> Conjuncts(Expr expr) {

+      Contract.Requires(expr != null);

+

+      var e = expr as NAryExpr;

+      if (e != null && e.Fun.FunctionName == "&&") {    // if it is a conjunction

+        foreach (Expr ee in e.Args) {

+          Contract.Assert(ee != null);

+          foreach (var c in Conjuncts(ee)) {

+            yield return c;

+          }

+        }

+      } else {

+        yield return expr;

+      }

+    }

+

+  }

+}