From 95bb8b3b4454fdc1a14fd67b22a5ac6183135cfd Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 5 Dec 2011 23:07:06 -0800 Subject: 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} --- Source/AbsInt/AbsInt.csproj | 4 + Source/AbsInt/AbstractInterpretation.cs | 10 +- Source/AbsInt/IntervalDomain.cs | 861 ++++++++++++++++++++++++++++++++ Source/AbsInt/NativeLattice.cs | 320 ++++++++++++ Source/AbsInt/TrivialDomain.cs | 79 +++ 5 files changed, 1268 insertions(+), 6 deletions(-) create mode 100644 Source/AbsInt/IntervalDomain.cs create mode 100644 Source/AbsInt/NativeLattice.cs create mode 100644 Source/AbsInt/TrivialDomain.cs (limited to 'Source/AbsInt') diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj index 454fc081..93d304d7 100644 --- a/Source/AbsInt/AbsInt.csproj +++ b/Source/AbsInt/AbsInt.csproj @@ -147,12 +147,16 @@ 3.5 + + + + diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs index a5847594..ef9814c6 100644 --- a/Source/AbsInt/AbstractInterpretation.cs +++ b/Source/AbsInt/AbstractInterpretation.cs @@ -70,7 +70,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { this.callReturnWorkItems = new Queue(); } - private Dictionary ComputeProcImplMap(Program program) { + public static Dictionary ComputeProcImplMap(Program program) { Contract.Requires(program != null); // Since implementations call procedures (impl. signatures) // rather than directly calling other implementations, we first @@ -541,20 +541,18 @@ namespace Microsoft.Boogie.AbstractInterpretation { } /// - /// Flat an expresion in the form P AND Q ... AND R into a list [P, Q, ..., R] + /// Flatten an expresion in the form P AND Q ... AND R into a list [P, Q, ..., R] /// private List!*/> flatConjunction(Expr embeddedExpr) { Contract.Requires(embeddedExpr != null); Contract.Ensures(cce.NonNullElements(Contract.Result>())); - - List!*/> retValue = new List();//No asserts necessarry. It is the return value, and thus will be subject to the postcondition + var retValue = new List(); NAryExpr e = embeddedExpr as NAryExpr; if (e != null && e.Fun.FunctionName.CompareTo("&&") == 0) { // if it is a conjunction foreach (Expr arg in e.Args) { Contract.Assert(arg != null); - List/*!*/ newConjuncts = flatConjunction(arg); - Contract.Assert(cce.NonNullElements(newConjuncts)); + var newConjuncts = flatConjunction(arg); retValue.AddRange(newConjuncts); } } else { diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs new file mode 100644 index 00000000..cf84e4bd --- /dev/null +++ b/Source/AbsInt/IntervalDomain.cs @@ -0,0 +1,861 @@ +using System; +using System.Numerics; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Basetypes; + +namespace Microsoft.Boogie.AbstractInterpretation +{ + class NativeIntervallDomain : NativeLattice + { + abstract class E_Common : NativeLattice.Element { } + class E_Bottom : E_Common + { + public override Expr ToExpr() { + return Expr.False; + } + } + class E : E_Common + { + public readonly Node N; + public E() { } + public E(Node n) { + N = n; + } + + public override Expr ToExpr() { + Expr expr = Expr.True; + for (var n = N; n != null; n = n.Next) { + expr = BplAnd(expr, n.ToExpr()); + } + return expr; + } + } + public class Node + { + public readonly Variable V; // variable has type bool or int + // For an integer variable (Lo,Hi) indicates Lo <= V < Hi, where Lo==null means no lower bound and Hi==null means no upper bound + // For a boolean variable, (Lo,Hi) is one of: (null,null) for {false,true}, (null,1) for {false}, and (1,null) for {true}. + public readonly BigInteger? Lo; + public readonly BigInteger? Hi; + public Node Next; // always sorted according to StrictlyBefore; readonly after full initialization + public static bool StrictlyBefore(Variable a, Variable b) { + Contract.Assert(a.UniqueId != b.UniqueId || a == b); + return a.UniqueId < b.UniqueId; + } + + Node(Variable v, BigInteger? lo, BigInteger? hi, Node next) { + Contract.Requires(lo != null || hi != null); // don't accept empty constraints + Contract.Requires(next == null || StrictlyBefore(v, next.V)); + V = v; + Lo = lo; + Hi = hi; + Next = next; + } + + /// + /// This constructor leaves Next as null, allowing the caller to fill in Next to finish off the construction. + /// + public Node(Variable v, BigInteger? lo, BigInteger? hi) { + Contract.Requires(lo != null || hi != null); // don't accept empty constraints + V = v; + Lo = lo; + Hi = hi; + } + + /// + /// Returns a Node that has the constraints head.{V,Lo,Hi} plus + /// all the constraints entailed by Nodes reachable from tail. + /// Requires that "head" sorts no later than anything in "tail". + /// Create either returns "head" itself or returns a new Node. + /// + public static Node Create(Node head, Node tail) { + Contract.Requires(head != null); + Contract.Requires(tail == null || !StrictlyBefore(tail.V, head.V)); + Contract.Requires(head != tail); + + if (head.Next == tail) { + return head; + } else if (tail != null && head.V == tail.V) { + // incorporate both constraints into one Node + return new Node(head.V, Max(head.Lo, tail.Lo, true), Min(head.Lo, tail.Lo, true), tail.Next); + } else { + return new Node(head.V, head.Lo, head.Hi, tail); + } + } + + public static void GetBounds(Node n, Variable v, out BigInteger? lo, out BigInteger? hi) { + for (; n != null; n = n.Next) { + if (n.V == v) { + lo = n.Lo; + hi = n.Hi; + return; + } else if (StrictlyBefore(v, n.V)) { + break; + } + } + lo = null; + hi = null; + } + + /// + /// Return the minimum of "a" and "b". If treatNullAsUnit==true, then "null" is + /// interpreted as positive infinity (the unit element of min); otherwise, it is + /// treated as negative infinity (the zero element of min). + /// + public static BigInteger? Min(BigInteger? a, BigInteger? b, bool treatNullAsUnit) { + if (a == null) { + return treatNullAsUnit ? b : a; + } else if (b == null) { + return treatNullAsUnit ? a : b; + } else { + return BigInteger.Min((BigInteger)a, (BigInteger)b); + } + } + + /// + /// Return the maximum of "a" and "b". If treatNullAsUnit==true, then "null" is + /// interpreted as negative infinity (the unit element of max); otherwise, it is + /// treated as positive infinity (the zero element of max). + /// + public static BigInteger? Max(BigInteger? a, BigInteger? b, bool treatNullAsUnit) { + if (a == null) { + return treatNullAsUnit ? b : a; + } else if (b == null) { + return treatNullAsUnit ? a : b; + } else { + return BigInteger.Max((BigInteger)a, (BigInteger)b); + } + } + + public static IEnumerable> Merge(Node a, Node b) { + while (true) { + if (a == null && b == null) { + yield break; + } else if (a == null || b == null) { + yield return new Tuple(a, b); + if (a != null) { a = a.Next; } else { b = b.Next; } + } else if (a.V == b.V) { + yield return new Tuple(a, b); + a = a.Next; b = b.Next; + } else if (StrictlyBefore(a.V, b.V)) { + yield return new Tuple(a, null); + a = a.Next; + } else { + yield return new Tuple(null, b); + b = b.Next; + } + } + } + + public Expr ToExpr() { + if (!V.IsMutable && CommandLineOptions.Clo.InstrumentInfer != CommandLineOptions.InstrumentationPlaces.Everywhere) { + // omit invariants about readonly variables + return Expr.True; + } else if (V.TypedIdent.Type.IsBool) { + if (Lo == null && Hi == null) { + return Expr.True; + } else { + Contract.Assert((Lo == null && (BigInteger)Hi == 1) || (Hi == null && (BigInteger)Lo == 1)); + var ide = new IdentifierExpr(Token.NoToken, V); + return Hi == null ? ide : Expr.Not(ide); + } + } else { + Expr e = Expr.True; + if (Lo != null && Hi != null && Lo + 1 == Hi) { + // produce an equality + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplEq(ide, Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Lo)))); + } else { + // produce a (possibly empty) conjunction of inequalities + if (Lo != null) { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Lo)), ide)); + } + if (Hi != null) { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLt(ide, Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Hi)))); + } + } + return e; + } + } + } + + private E_Common top = new E(); + private E_Common bottom = new E_Bottom(); + + public override Element Top { get { return top; } } + public override Element Bottom { get { return bottom; } } + + public override bool IsTop(Element element) { + var e = element as E; + return e != null && e.N == null; + } + public override bool IsBottom(Element element) { + return element is E_Bottom; + } + + public override bool Below(Element a, Element b) { + if (a is E_Bottom) { + return true; + } else if (b is E_Bottom) { + return false; + } else { + var aa = (E)a; + var bb = (E)b; + // check if every constraint in 'bb' is implied by constraints in 'aa' + foreach (var t in Node.Merge(aa.N, bb.N)) { + var x = t.Item1; + var y = t.Item2; + if (x == null) { + // bb constrains a variable that aa does not + return false; + } else if (y == null) { + // aa constrains a variable that bb does not; that's fine + } else if (y.Lo != null && (x.Lo == null || x.Lo < y.Lo)) { + // bb has a Lo constraint, and either aa has no Lo constraint or it has a weaker Lo constraint + return false; + } else if (y.Hi != null && (x.Hi == null || y.Hi < x.Hi)) { + // bb has a Hi o constraint, and either aa has no Hi constraint or it has a weaker Hi constraint + return false; + } + } + return true; + } + } + + public override Element Meet(Element a, Element b) { + if (a is E_Bottom) { + return a; + } else if (b is E_Bottom) { + return b; + } else { + var aa = (E)a; + var bb = (E)b; + Node head = null; + Node prev = null; + foreach (var t in Node.Merge(aa.N, bb.N)) { + var x = t.Item1; + var y = t.Item2; + Node n; + if (x == null) { + n = new Node(y.V, y.Lo, y.Hi); + } else if (y == null) { + n = new Node(x.V, x.Lo, x.Hi); + } else { + var lo = Node.Max(x.Lo, y.Lo, true); + var hi = Node.Min(x.Hi, y.Hi, true); + // if hi<=lo, then we're overconstrained + if (lo != null && hi != null && hi <= lo) { + return bottom; + } + n = new Node(x.V, lo, hi); + } + if (head == null) { + head = n; + } else { + prev.Next = n; + } + prev = n; + } + return new E(head); + } + } + + public override Element Join(Element a, Element b) { + if (a is E_Bottom) { + return b; + } else if (b is E_Bottom) { + return a; + } else { + var aa = (E)a; + var bb = (E)b; + // for each variable, take the weaker of the constraints + Node head = null; + Node prev = null; + foreach (var t in Node.Merge(aa.N, bb.N)) { + if (t.Item1 != null && t.Item2 != null) { + var lo = Node.Min(t.Item1.Lo, t.Item2.Lo, false); + var hi = Node.Max(t.Item1.Hi, t.Item2.Hi, false); + if (lo != null || hi != null) { + var n = new Node(t.Item1.V, lo, hi); + if (head == null) { + head = n; + } else { + prev.Next = n; + } + prev = n; + } + } + } + return new E(head); + } + } + + public override Element Widen(Element a, Element b) { + if (a is E_Bottom) { + return b; // since this is done just once, we maintain the ascending chains property + } else if (b is E_Bottom) { + return a; + } else { + var aa = (E)a; + var bb = (E)b; + // return a subset of the constraints of aa, namely those that are implied by bb + Node head = null; + Node prev = null; + foreach (var t in Node.Merge(aa.N, bb.N)) { + var x = t.Item1; + var y = t.Item2; + if (x != null && y != null) { + BigInteger? lo, hi; + lo = hi = null; + if (x.Lo == null || (y.Lo != null && x.Lo <= y.Lo)) { + // okay, we keep the lower bound + lo = x.Lo; + } + if (x.Hi == null || (y.Hi != null && y.Hi <= x.Hi)) { + // okay, we keep the upper bound + hi = x.Hi; + } + if (lo != null || hi != null) { + var n = new Node(x.V, lo, hi); + if (head == null) { + head = n; + } else { + prev.Next = n; + } + prev = n; + } + } + } + return new E(head); + } + } + + public override Element Constrain(Element element, Expr expr) { + if (element is E_Bottom) { + return element; + } else { + var e = (E)element; + var c = Constraint(expr, e.N); + return c == null ? element : Meet(element, c); + } + } + + /// + /// Returns an Element that corresponds to the constraints implied by "expr" in the + /// state "state". + /// Return "null" to indicate no constraints. + /// + E_Common Constraint(Expr expr, Node state) { + Variable v; + if (IsVariable(expr, out v)) { + var n = new Node(v, new BigInteger(1), null); + return new E(n); + } else if (expr is LiteralExpr) { + var e = (LiteralExpr)expr; + return (bool)e.Val ? null : new E_Bottom(); + } else if (expr is NAryExpr) { + var e = (NAryExpr)expr; + if (e.Fun is UnaryOperator) { + if (((UnaryOperator)e.Fun).Op == UnaryOperator.Opcode.Not) { + if (IsVariable(e.Args[0], out v)) { + var n = new Node(v, null, new BigInteger(1)); + return new E(n); + } + } + } else if (e.Fun is BinaryOperator) { + var op = ((BinaryOperator)e.Fun).Op; + var arg0 = e.Args[0]; + var arg1 = e.Args[1]; + switch (op) { + case BinaryOperator.Opcode.Eq: + case BinaryOperator.Opcode.Iff: { + E c = null; + if (IsVariable(arg0, out v)) { + BigInteger? lo, hi; + if (PartiallyEvaluate(arg1, state, out lo, out hi)) { + var n = new Node(v, lo, hi); + c = new E(n); + } + } + if (IsVariable(arg1, out v)) { + BigInteger? lo, hi; + if (PartiallyEvaluate(arg1, state, out lo, out hi)) { + var n = new Node(v, lo, hi); + c = c == null ? new E(n) : (E)Meet(c, new E(n)); + } + } + return c; + } + case BinaryOperator.Opcode.Neq: { + E c = null; + if (IsVariable(arg0, out v)) { + c = ConstrainNeq(state, v, arg1); + } + if (IsVariable(arg1, out v)) { + var cc = ConstrainNeq(state, v, arg0); + if (cc != null) { + c = c == null ? cc : (E)Meet(c, cc); + } + } + return c; + } + case BinaryOperator.Opcode.Le: { + E c = null; + if (IsVariable(arg1, out v)) { + BigInteger? lo, hi; + PartiallyEvaluate(arg0, state, out lo, out hi); + if (lo != null) { + var n = new Node(v, lo, null); + c = new E(n); + } + } + if (IsVariable(arg0, out v)) { + BigInteger? lo, hi; + PartiallyEvaluate(arg1, state, out lo, out hi); + if (hi != null) { + var n = new Node(v, null, hi); + c = c == null ? new E(n) : (E)Meet(c, new E(n)); + } + } + return c; + } + case BinaryOperator.Opcode.Lt: { + E c = null; + if (IsVariable(arg1, out v)) { + BigInteger? lo, hi; + PartiallyEvaluate(arg0, state, out lo, out hi); + if (lo != null) { + var n = new Node(v, lo + 1, null); + c = new E(n); + } + } + if (IsVariable(arg0, out v)) { + BigInteger? lo, hi; + PartiallyEvaluate(arg1, state, out lo, out hi); + if (hi != null) { + var n = new Node(v, null, hi - 1); + c = c == null ? new E(n) : (E)Meet(c, new E(n)); + } + } + return c; + } + case BinaryOperator.Opcode.Ge: { + var tmp = arg0; arg0 = arg1; arg1 = tmp; + goto case BinaryOperator.Opcode.Le; + } + case BinaryOperator.Opcode.Gt: { + var tmp = arg0; arg0 = arg1; arg1 = tmp; + goto case BinaryOperator.Opcode.Lt; + } + default: + break; + } + } + } + return null; // approximation + } + + private E ConstrainNeq(Node state, Variable v, Expr arg) { + BigInteger? lo, hi; + if (PartiallyEvaluate(arg, state, out lo, out hi)) { + if (lo != null && hi != null && lo + 1 == hi) { + var exclude = lo; + // If the partially evaluated arg (whose value is "exclude") is an end-point of + // the interval known for "v", then produce a constraint that excludes that bound. + Node.GetBounds(state, v, out lo, out hi); + if (lo != null && lo == exclude) { + var n = new Node(v, lo + 1, null); + return new E(n); + } else if (hi != null && exclude + 1 == hi) { + var n = new Node(v, null, exclude); + return new E(n); + } + } + } + return null; + } + + bool IsVariable(Expr expr, out Variable v) { + var e = expr as IdentifierExpr; + if (e == null) { + v = null; + return false; + } else { + v = e.Decl; + return true; + } + } + + public override Element Update(Element element, AssignCmd cmd) { + if (element is E_Bottom) { + return element; + } + var e = (E)element; + var nn = e.N; + Contract.Assert(cmd.Lhss.Count == cmd.Rhss.Count); + for (int i = 0; i < cmd.Lhss.Count; i++) { + var lhs = cmd.Lhss[i]; + var rhs = cmd.Rhss[i]; + BigInteger? lo; + BigInteger? hi; + PartiallyEvaluate(rhs, e.N, out lo, out hi); + nn = UpdateOne(nn, lhs.DeepAssignedVariable, lo, hi); + } + return new E(nn); + } + + bool PartiallyEvaluate(Expr rhs, Node node, out BigInteger? lo, out BigInteger? hi) { + var pe = new PEVisitor(node); + pe.VisitExpr(rhs); + lo = pe.Lo; + hi = pe.Hi; + return lo != null || hi != null; + } + + class PEVisitor : StandardVisitor + { + public BigInteger? Lo; + public BigInteger? Hi; + + readonly BigInteger one = new BigInteger(1); + + Node N; + public PEVisitor(Node n) { + N = n; + } + + // Override visitors for all expressions that can return a boolean or integer result + + public override Expr VisitExpr(Expr node) { + Lo = Hi = null; + return base.VisitExpr(node); + } + public override LiteralExpr VisitLiteralExpr(LiteralExpr node) { + if (node.Val is BigNum) { + var n = ((BigNum)node.Val).ToBigInteger; + Lo = n; + Hi = n + 1; + } else if (node.Val is bool) { + if ((bool)node.Val) { + // true + Lo = one; + Hi = null; + } else { + // false + Lo = null; + Hi = one; + } + } + return node; + } + public override Expr VisitIdentifierExpr(IdentifierExpr node) { + if (node.Type.IsBool || node.Type.IsInt) { + Node.GetBounds(N, node.Decl, out Lo, out Hi); + } + return node; + } + public override Expr VisitNAryExpr(NAryExpr node) { + if (node.Fun is UnaryOperator) { + var op = (UnaryOperator)node.Fun; + Contract.Assert(node.Args.Length == 1); + if (op.Op == UnaryOperator.Opcode.Not) { + VisitExpr(node.Args[0]); + Contract.Assert((Lo == null && Hi == null) || + (Lo == null && (BigInteger)Hi == 1) || + (Hi == null && (BigInteger)Lo == 1)); + var tmp = Lo; + Lo = Hi; + Hi = tmp; + } + } else if (node.Fun is BinaryOperator) { + var op = (BinaryOperator)node.Fun; + Contract.Assert(node.Args.Length == 2); + BigInteger? lo0, hi0, lo1, hi1; + VisitExpr(node.Args[0]); + lo0 = Lo; hi0 = Hi; + VisitExpr(node.Args[1]); + lo1 = Lo; hi1 = Hi; + Lo = Hi = null; + switch (op.Op) { + case BinaryOperator.Opcode.And: + if (hi0 != null || hi1 != null) { + // one operand is definitely false, thus so is the result + Lo = null; Hi = one; + } else if (lo0 != null && lo1 != null) { + // both operands are definitely true, thus so is the result + Lo = one; Hi = null; + } + break; + case BinaryOperator.Opcode.Or: + if (lo0 != null || lo1 != null) { + // one operand is definitely true, thus so is the result + Lo = one; Hi = null; + } else if (hi0 != null && hi1 != null) { + // both operands are definitely false, thus so is the result + Lo = null; Hi = one; + } + break; + case BinaryOperator.Opcode.Imp: + if (hi0 != null || lo1 != null) { + // either arg0 false or arg1 is true, so the result is true + Lo = one; Hi = null; + } else if (lo0 != null && hi1 != null) { + // arg0 is true and arg1 is false, so the result is false + Lo = null; Hi = one; + } + break; + case BinaryOperator.Opcode.Iff: + if (lo0 != null && lo1 != null) { + Lo = one; Hi = null; + } else if (hi0 != null && hi1 != null) { + Lo = one; Hi = null; + } else if (lo0 != null && hi1 != null) { + Lo = null; Hi = one; + } else if (hi0 != null && lo1 != null) { + Lo = null; Hi = one; + } + if (op.Op == BinaryOperator.Opcode.Neq) { + var tmp = Lo; Lo = Hi; Hi = tmp; + } + break; + case BinaryOperator.Opcode.Eq: + case BinaryOperator.Opcode.Neq: + if (node.Args[0].Type.IsBool) { + goto case BinaryOperator.Opcode.Iff; + } + // For Eq: + // If the (lo0,hi0) and (lo1,hi1) ranges do not overlap, the answer is false. + // If both ranges are the same unit range, then the answer is true. + if (hi0 != null && lo1 != null && hi0 <= lo1) { + Lo = null; Hi = one; + } else if (lo0 != null && hi1 != null && hi1 <= lo0) { + Lo = null; Hi = one; + } else if (lo0 != null && hi0 != null && lo1 != null && hi1 != null && + lo0 + 1 == hi0 && lo0 == lo1 && lo1 + 1 == hi1) { + Lo = one; Hi = null; + } + if (op.Op == BinaryOperator.Opcode.Neq) { + var tmp = Lo; Lo = Hi; Hi = tmp; + } + break; + case BinaryOperator.Opcode.Le: + case BinaryOperator.Opcode.Gt: + // If hi0 - 1 <= lo1, then the answer is true. + // If hi1 <= lo0, then the answer is false. + if (hi0 != null && lo1 != null && hi0 - 1 <= lo1) { + Lo = one; Hi = null; + } else if (lo0 != null && hi1 != null && hi1 <= lo0) { + Lo = null; Hi = one; + } + if (op.Op == BinaryOperator.Opcode.Gt) { + var tmp = Lo; Lo = Hi; Hi = tmp; + } + break; + case BinaryOperator.Opcode.Lt: + case BinaryOperator.Opcode.Ge: + // If hi0 <= lo1, then the answer is true. + // If hi1 - 1 <= lo0, then the answer is false. + if (hi0 != null && lo1 != null && hi0 <= lo1) { + Lo = one; Hi = null; + } else if (lo0 != null && hi1 != null && hi1 - 1 <= lo0) { + Lo = null; Hi = one; + } + if (op.Op == BinaryOperator.Opcode.Ge) { + var tmp = Lo; Lo = Hi; Hi = tmp; + } + break; + case BinaryOperator.Opcode.Add: + if (lo0 != null && lo1 != null) { + Lo = lo0 + lo1; + } + if (hi0 != null && hi1 != null) { + Hi = hi0 + hi1 - 1; + } + break; + case BinaryOperator.Opcode.Sub: + if (lo0 != null && hi1 != null) { + Lo = lo0 - hi1 + 1; + } + if (hi0 != null && lo1 != null) { + Hi = hi0 - lo1; + } + break; + case BinaryOperator.Opcode.Mul: + // this uses an incomplete approximation that could be tightened up + if (lo0 != null && lo1 != null) { + if (0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { + Lo = lo0 * lo1; + Hi = hi0 == null || hi1 == null ? null : (hi0 - 1) * (hi1 - 1) + 1; + } else if ((BigInteger)lo0 < 0 && (BigInteger)lo1 < 0) { + Lo = null; // approximation + Hi = lo0 * lo1 + 1; + } + } + break; + case BinaryOperator.Opcode.Div: + // this uses an incomplete approximation that could be tightened up + if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { + Lo = new BigInteger(0); + Hi = lo0 - 1; + } + break; + case BinaryOperator.Opcode.Mod: + // this uses an incomplete approximation that could be tightened up + if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { + Lo = new BigInteger(0); + Hi = lo1; + } + break; + default: + break; + } + } else if (node.Fun is IfThenElse) { + var op = (IfThenElse)node.Fun; + Contract.Assert(node.Args.Length == 3); + BigInteger? guardLo, guardHi, lo0, hi0, lo1, hi1; + VisitExpr(node.Args[0]); + guardLo = Lo; guardHi = Hi; + VisitExpr(node.Args[1]); + lo0 = Lo; hi0 = Hi; + VisitExpr(node.Args[2]); + lo1 = Lo; hi1 = Hi; + Contract.Assert(guardLo == null || guardHi == null); // this is a consequence of the guard being boolean + if (guardLo != null) { + // guard is always true + Lo = lo0; Hi = hi0; + } else if (guardHi != null) { + // guard is always false + Lo = lo1; Hi = hi1; + } else { + // we don't know which branch will be taken, so join the information from the two branches + Lo = Node.Min(lo0, lo1, false); + Hi = Node.Max(hi0, hi1, false); + } + } + return node; + } + public override BinderExpr VisitBinderExpr(BinderExpr node) { + // don't recurse on subexpression + return node; + } + public override Expr VisitOldExpr(OldExpr node) { + // don't recurse on subexpression + return node; + } + public override Expr VisitCodeExpr(CodeExpr node) { + // don't recurse on subexpression + return node; + } + public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) { + // don't recurse on subexpression + return node; + } + public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) { + // don't recurse on subexpression + return node; + } + } + + public override Element Eliminate(Element element, Variable v) { + if (element is E_Bottom) { + return element; + } + var e = (E)element; + var nn = UpdateOne(e.N, v, null, null); + if (nn == e.N) { + return element; + } else { + return new E(nn); + } + } + + Node UpdateOne(Node nn, Variable v, BigInteger? lo, BigInteger? hi) { + var orig = nn; + Node head = null; + Node prev = null; + var foundV = false; + for (; nn != null && !Node.StrictlyBefore(v, nn.V); nn = nn.Next) { + if (nn.V == v) { + foundV = true; + nn = nn.Next; + break; // we found the place where the new node goes + } else { + var n = new Node(nn.V, nn.Lo, nn.Hi); // copy this Node + if (head == null) { + head = n; + } else { + prev.Next = n; + } + prev = n; + } + } + Node rest; + if (lo == null && hi == null) { + // eliminate all information about "v" + if (!foundV) { + return orig; + } + rest = nn; + } else { + rest = new Node(v, lo, hi); + rest.Next = nn; + } + if (head == null) { + head = rest; + } else { + prev.Next = rest; + } + return head; + } + + /// + /// Return a resolved/type-checked expression that represents the conjunction of a and b. + /// Requires a and b to be resolved and type checked already. + /// + public static Expr BplAnd(Expr a, Expr b) { + if (a == Expr.True) { + return b; + } else if (b == Expr.True) { + return a; + } else { + var nary = Expr.Binary(BinaryOperator.Opcode.And, a, b); + nary.Type = Type.Bool; + nary.TypeParameters = SimpleTypeParamInstantiation.EMPTY; + return nary; + } + } + + /// + /// Return a resolved/type-checked expression that represents a EQUALS b. + /// Requires a and b to be resolved and type checked already. + /// + public static Expr BplEq(Expr a, Expr b) { + var e = Expr.Eq(a, b); + e.Type = Type.Bool; + return e; + } + + /// + /// Return a resolved/type-checked expression that represents a LESS-EQUAL b. + /// Requires a and b to be resolved and type checked already. + /// + public static Expr BplLe(Expr a, Expr b) { + var e = Expr.Le(a, b); + e.Type = Type.Bool; + return e; + } + /// + /// Return a resolved/type-checked expression that represents a LESS b. + /// Requires a and b to be resolved and type checked already. + /// + public static Expr BplLt(Expr a, Expr b) { + var e = Expr.Lt(a, b); + e.Type = Type.Bool; + return e; + } + } + +} 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 +{ + /// + /// Specifies the operations (e.g., join) on a mathematical lattice that depend + /// only on the elements of the lattice. + /// + public abstract class NativeLattice + { + /// + /// An element of the lattice. This class should be derived from in any + /// implementation of MathematicalLattice. + /// + 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); + + /// + /// Is 'a' better (or equal) information than 'b'? That is, is 'a' below 'b' in the lattice? + /// + 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 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(); + } + } + + /// + /// Compute and apply the invariants for the program using the underlying abstract domain (using native Boogie + /// expressions, not the abstracted AI.Expr's). + /// + public static void ComputeProgramInvariants(Program program, Dictionary 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>(); + workItems.Enqueue(new Tuple(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(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(), 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(), 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 + } + } + } + + /// + /// The abstract transition relation. + /// 'cmd' is allowed to be a StateCmd. + /// + 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() != 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(); + 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; + } + + /// + /// Yields the conjuncts of 'expr'. + /// + public static IEnumerable 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; + } + } + + } +} diff --git a/Source/AbsInt/TrivialDomain.cs b/Source/AbsInt/TrivialDomain.cs new file mode 100644 index 00000000..f9298e11 --- /dev/null +++ b/Source/AbsInt/TrivialDomain.cs @@ -0,0 +1,79 @@ +using System; +using System.Numerics; +using System.Collections.Generic; +using System.Diagnostics.Contracts; + +namespace Microsoft.Boogie.AbstractInterpretation +{ + class TrivialDomain : NativeLattice + { + class E : NativeLattice.Element + { + public readonly bool IsTop; + public E(bool isTop) { + IsTop = isTop; + } + + public override Expr ToExpr() { + return Expr.Literal(IsTop); + } + } + + private E top = new E(true); + private E bottom = new E(false); + + public override Element Top { get { return top; } } + public override Element Bottom { get { return bottom; } } + + public override bool IsTop(Element element) { + var e = (E)element; + return e.IsTop; + } + public override bool IsBottom(Element element) { + var e = (E)element; + return !e.IsTop; + } + + public override bool Below(Element a, Element b) { + return IsBottom(a) || IsTop(b); + } + + public override Element Meet(Element a, Element b) { + if (IsBottom(b)) { + return b; + } else { + return a; + } + } + + public override Element Join(Element a, Element b) { + if (IsTop(b)) { + return b; + } else { + return a; + } + } + + public override Element Widen(Element a, Element b) { + return Join(a, b); // it's a finite domain, after all + } + + public override Element Constrain(Element element, Expr expr) { + var e = (E)element; + var lit = expr as LiteralExpr; + if (lit != null && lit.isBool && !(bool)lit.Val) { + return bottom; + } else { + return e; + } + } + + public override Element Update(Element element, AssignCmd cmd) { + return element; + } + + public override Element Eliminate(Element element, Variable v) { + return element; + } + } +} -- cgit v1.2.3