From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/AbsInt/IntervalDomain.cs | 2428 ++++++++++++++++++++------------------- 1 file changed, 1218 insertions(+), 1210 deletions(-) (limited to 'Source/AbsInt/IntervalDomain.cs') diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index d5a5efc9..0dd78cbb 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -1,1210 +1,1218 @@ -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 real 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 - [Pure] - 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 if (V.TypedIdent.Type.IsInt) { - 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, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type))); - } else { - // produce a (possibly empty) conjunction of inequalities - if (Lo != null) { - var ide = new IdentifierExpr(Token.NoToken, V); - e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide)); - } - if (Hi != null) { - var ide = new IdentifierExpr(Token.NoToken, V); - e = Expr.And(e, BplLt(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type))); - } - } - return e; - } else if (V.TypedIdent.Type.IsReal){ - Expr e = Expr.True; - if (Lo != null && Hi != null && Lo == Hi) { - // produce an equality - var ide = new IdentifierExpr(Token.NoToken, V); - e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type))); - } else { - // produce a (possibly empty) conjunction of inequalities - if (Lo != null) { - var ide = new IdentifierExpr(Token.NoToken, V); - e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide)); - } - if (Hi != null) { - var ide = new IdentifierExpr(Token.NoToken, V); - e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type))); - } - } - return e; - } else { - Contract.Assert(V.TypedIdent.Type.IsFloat); - Expr e = Expr.True; - if (Lo != null && Hi != null && Lo == Hi) - { - // produce an equality - var ide = new IdentifierExpr(Token.NoToken, V); - e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type))); - } - else - { - // produce a (possibly empty) conjunction of inequalities - if (Lo != null) - { - var ide = new IdentifierExpr(Token.NoToken, V); - e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide)); - } - if (Hi != null) - { - var ide = new IdentifierExpr(Token.NoToken, V); - e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type))); - } - } - return e; - } - } - } - - static Expr NumberToExpr(BigInteger n, Type ty) { - if (n == null) { - return null; - } else if (ty.IsReal) { - return Expr.Literal(Basetypes.BigDec.FromBigInt(n)); - } else if (ty.IsFloat) { - return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatMantissa)); - } else { - Contract.Assume(ty.IsInt); - return Expr.Literal(Basetypes.BigNum.FromBigInt(n)); - } - } - - List upThresholds; // invariant: thresholds are sorted - List downThresholds; // invariant: thresholds are sorted - - /// - /// Requires "thresholds" to be sorted. - /// - public NativeIntervallDomain() { - upThresholds = new List(); - downThresholds = new List(); - } - - public override void Specialize(Implementation impl) { - if (impl == null) { - // remove thresholds - upThresholds = new List(); - downThresholds = new List(); - } else { - var tf = new ThresholdFinder(impl); - tf.Find(out downThresholds, out upThresholds); -#if DEBUG_PRINT - Console.Write("DEBUG: for implementation '{0}', setting downs to [", impl.Name); - foreach (var i in downThresholds) { - Console.Write(" {0}", i); - } - Console.Write(" ] and ups to ["); - foreach (var i in upThresholds) { - Console.Write(" {0}", i); - } - Console.WriteLine(" ]"); -#endif - } - base.Specialize(impl); - } - - 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 (or hi - /// For a proof of correctness of this method, see Test/dafny2/Intervals.dfy. - /// A difference is that the this method returns: - /// let d = Dafny_RoundDown(k); - /// return d == -1 ? null : downThresholds[d]; - /// - BigInteger? RoundDown(BigInteger k) - { - if (downThresholds.Count == 0 || k < downThresholds[0]) { - return null; - } - var i = 0; - var j = downThresholds.Count - 1; - while (i < j) - { - var mid = i + (j - i + 1) / 2; - if (downThresholds[mid] <= k) { - i = mid; - } else { - j = mid - 1; - } - } - return downThresholds[i]; - } - - /// - /// For a proof of correctness of this method, see Test/dafny2/Intervals.dfy. - /// A difference is that the this method returns: - /// let d = Dafny_RoundUp(k); - /// return d == thresholds.Count ? null : upThresholds[d]; - /// - BigInteger? RoundUp(BigInteger k) - { - if (upThresholds.Count == 0 || upThresholds[upThresholds.Count - 1] < k) { - return null; - } - var i = 0; - var j = upThresholds.Count - 1; - while (i < j) - { - var mid = i + (j - i) / 2; - if (upThresholds[mid] < k) { - i = mid + 1; - } else { - j = mid; - } - } - return upThresholds[i]; - } - - 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, BigInteger.One, 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, BigInteger.One); - 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_Common 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_Common)Meet(c, new E(n)); - } - } - return c; - } - case BinaryOperator.Opcode.Neq: { - E_Common 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_Common)Meet(c, cc); - } - } - return c; - } - case BinaryOperator.Opcode.Le: { - E_Common 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_Common)Meet(c, new E(n)); - } - } - return c; - } - case BinaryOperator.Opcode.Lt: { - E_Common 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, v.TypedIdent.Type.IsReal ? lo : 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, v.TypedIdent.Type.IsReal ? hi : hi - 1); - c = c == null ? new E(n) : (E_Common)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 (!v.TypedIdent.Type.IsReal && 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 : ReadOnlyVisitor - { - public BigInteger? Lo; - public BigInteger? Hi; - - readonly BigInteger one = BigInteger.One; - - Node N; - public PEVisitor(Node n) { - N = n; - } - - // Override visitors for all expressions that can return a boolean, integer, or real result - - public override Expr VisitExpr(Expr node) { - Lo = Hi = null; - return base.VisitExpr(node); - } - public override Expr VisitLiteralExpr(LiteralExpr node) { - if (node.Val is BigNum) { - var n = ((BigNum)node.Val).ToBigInteger; - Lo = n; - Hi = n + 1; - } else if (node.Val is BigDec) { - BigInteger floor, ceiling; - ((BigDec)node.Val).FloorCeiling(out floor, out ceiling); - Lo = floor; - Hi = ceiling; - } else if (node.Val is BigFloat) { - BigNum floor, ceiling; - ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling); - Lo = floor.ToBigInteger; - Hi = ceiling.ToBigInteger; - } 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.Type.IsReal) { - 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.Count == 1); - if (op.Op == UnaryOperator.Opcode.Neg) { - BigInteger? lo, hi; - VisitExpr(node.Args[0]); - lo = Lo; hi = Hi; - if (hi != null) { - Lo = node.Type.IsReal ? -hi : 1 - hi; - } - if (lo != null) { - Hi = node.Type.IsReal ? -lo : 1 - lo; - } - } - else 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.Count == 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; - var isReal = node.Args[0].Type.IsReal; - 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 && (isReal ? hi0 < lo1 : hi0 <= lo1)) { - // no overlap - Lo = null; Hi = one; - } else if (lo0 != null && hi1 != null && (isReal ? hi1 < lo0 : hi1 <= lo0)) { - Lo = null; Hi = one; - // no overlaop - } else if (lo0 != null && hi0 != null && lo1 != null && hi1 != null && - lo0 == lo1 && hi0 == hi1 && // ranges are the same - (isReal ? lo0 == hi0 : lo0 + 1 == hi0)) { // unit range - // both ranges are the same unit range - Lo = one; Hi = null; - } - if (op.Op == BinaryOperator.Opcode.Neq) { - var tmp = Lo; Lo = Hi; Hi = tmp; - } - break; - case BinaryOperator.Opcode.Le: - if (isReal) { - // If hi0 <= lo1, then the answer is true. - // If hi1 < lo0, then the answer is false. - if (hi0 != null && lo1 != null && hi0 <= lo1) { - Lo = one; Hi = null; - } else if (hi1 != null && lo0 != null && hi1 < lo0) { - Lo = null; Hi = one; - } - } else { - // 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; - } - } - break; - case BinaryOperator.Opcode.Lt: - if (isReal) { - // If hi0 < lo1, then the answer is true. - // If hi1 <= lo0, then the answer is false. - if (hi0 != null && lo1 != null && hi0 < lo1) { - Lo = one; Hi = null; - } else if (hi1 != null && lo0 != null && hi1 <= lo0) { - Lo = null; Hi = one; - } - } else { - // 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; - } - } - break; - case BinaryOperator.Opcode.Gt: - // swap the operands and then continue as Lt - { - var tmp = lo0; lo0 = lo1; lo1 = tmp; - tmp = hi0; hi0 = hi1; hi1 = tmp; - } - goto case BinaryOperator.Opcode.Lt; - case BinaryOperator.Opcode.Ge: - // swap the operands and then continue as Le - { - var tmp = lo0; lo0 = lo1; lo1 = tmp; - tmp = hi0; hi0 = hi1; hi1 = tmp; - } - goto case BinaryOperator.Opcode.Le; - case BinaryOperator.Opcode.Add: - if (lo0 != null && lo1 != null) { - Lo = lo0 + lo1; - } - if (hi0 != null && hi1 != null) { - Hi = isReal ? hi0 + hi1 : hi0 + hi1 - 1; - } - break; - case BinaryOperator.Opcode.Sub: - if (lo0 != null && hi1 != null) { - Lo = isReal ? lo0 - hi1 : 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 : isReal ? hi0 * hi1 : (hi0 - 1) * (hi1 - 1) + 1; - } else if ((BigInteger)lo0 < 0 && (BigInteger)lo1 < 0) { - Lo = null; // approximation - Hi = isReal ? lo0 * lo1 : 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 = BigInteger.Zero; - Hi = hi0; - } - 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 = BigInteger.Zero; - Hi = hi1; - } - break; - case BinaryOperator.Opcode.RealDiv: - // this uses an incomplete approximation that could be tightened up - if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { - Lo = BigInteger.Zero; - Hi = 1 <= (BigInteger)lo1 ? hi0 : null; - } - break; - case BinaryOperator.Opcode.Pow: - // this uses an incomplete approximation that could be tightened up - if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { - Lo = 1 <= (BigInteger)lo1 ? BigInteger.One : BigInteger.Zero; - Hi = hi1; - } - break; - default: - break; - } - } else if (node.Fun is IfThenElse) { - var op = (IfThenElse)node.Fun; - Contract.Assert(node.Args.Count == 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); - } - } else if (node.Fun is FunctionCall) { - var call = (FunctionCall)node.Fun; - // See if this is an identity function, which we do by checking: that the function has - // exactly one argument and the function has been marked by the user with the attribute {:identity} - bool claimsToBeIdentity = false; - if (call.ArgumentCount == 1 && call.Func.CheckBooleanAttribute("identity", ref claimsToBeIdentity) && claimsToBeIdentity && node.Args[0].Type.Equals(node.Type)) { - VisitExpr(node.Args[0]); - } - } - 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 Expr VisitBvConcatExpr(BvConcatExpr node) { - // don't recurse on subexpression - return node; - } - public override Expr 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; - } - } - - public class ThresholdFinder : ReadOnlyVisitor - { - readonly Implementation Impl; - public ThresholdFinder(Implementation impl) { - Contract.Requires(impl != null); - Impl = impl; - } - HashSet downs = new HashSet(); - HashSet ups = new HashSet(); - public void Find(out List downThresholds, out List upThresholds) { - // always include -1, 0, 1 as down-thresholds - downs.Clear(); - downs.Add(-1); - downs.Add(0); - downs.Add(1); - // always include 0 and 1 as up-thresholds - ups.Clear(); - ups.Add(0); - ups.Add(1); - - foreach (Requires p in Impl.Proc.Requires) { - Visit(p.Condition); - } - foreach (Ensures p in Impl.Proc.Ensures) { - Visit(p.Condition); - } - foreach (var b in Impl.Blocks) { - foreach (Cmd c in b.Cmds) { - Visit(c); - } - } - - // convert the HashSets to sorted Lists and return - downThresholds = new List(); - foreach (var i in downs) { - downThresholds.Add(i); - } - downThresholds.Sort(); - upThresholds = new List(); - foreach (var i in ups) { - upThresholds.Add(i); - } - upThresholds.Sort(); - } - - public override Expr VisitNAryExpr(NAryExpr node) { - if (node.Fun is BinaryOperator) { - var op = (BinaryOperator)node.Fun; - Contract.Assert(node.Args.Count == 2); - var arg0 = node.Args[0]; - var arg1 = node.Args[1]; - var offset = arg0.Type.IsReal ? 0 : 1; - BigInteger? k; - switch (op.Op) { - case BinaryOperator.Opcode.Eq: - case BinaryOperator.Opcode.Neq: - k = AsIntLiteral(arg0); - if (k != null) { - var i = (BigInteger)k; - downs.Add(i - 1); - downs.Add(i); - ups.Add(i + 1); - ups.Add(i + 2); - } - k = AsIntLiteral(arg1); - if (k != null) { - var i = (BigInteger)k; - downs.Add(i - 1); - downs.Add(i); - ups.Add(i + 1); - ups.Add(i + 2); - } - break; - case BinaryOperator.Opcode.Le: - k = AsIntLiteral(arg0); - if (k != null) { - var i = (BigInteger)k; - downs.Add(i - 1); - downs.Add(i); - } - k = AsIntLiteral(arg1); - if (k != null) { - var i = (BigInteger)k; - ups.Add(i + offset); - ups.Add(i + 1 + offset); - } - break; - case BinaryOperator.Opcode.Lt: - k = AsIntLiteral(arg0); - if (k != null) { - var i = (BigInteger)k; - downs.Add(i ); - downs.Add(i + 1); - } - k = AsIntLiteral(arg1); - if (k != null) { - var i = (BigInteger)k; - ups.Add(i - 1 + offset); - ups.Add(i + offset); - } - break; - 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 base.VisitNAryExpr(node); - } - - BigInteger? AsIntLiteral(Expr e) { - var lit = e as LiteralExpr; - if (lit != null && lit.isBigNum) { - BigNum bn = lit.asBigNum; - return bn.ToBigInteger; - } - return null; - } - } - -} +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 real 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 + [Pure] + 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 if (V.TypedIdent.Type.IsInt) { + 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, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type))); + } else { + // produce a (possibly empty) conjunction of inequalities + if (Lo != null) { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide)); + } + if (Hi != null) { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLt(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type))); + } + } + return e; + } else if (V.TypedIdent.Type.IsReal){ + Expr e = Expr.True; + if (Lo != null && Hi != null && Lo == Hi) { + // produce an equality + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type))); + } else { + // produce a (possibly empty) conjunction of inequalities + if (Lo != null) { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide)); + } + if (Hi != null) { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type))); + } + } + return e; + } else { + Contract.Assert(V.TypedIdent.Type.IsFloat); + Expr e = Expr.True; + if (Lo != null && Hi != null && Lo == Hi) + { + // produce an equality + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type))); + } + else + { + // produce a (possibly empty) conjunction of inequalities + if (Lo != null) + { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide)); + } + if (Hi != null) + { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type))); + } + } + return e; + } + } + } + + static Expr NumberToExpr(BigInteger n, Type ty) { + if (n == null) { + return null; + } else if (ty.IsReal) { + return Expr.Literal(Basetypes.BigDec.FromBigInt(n)); + } else if (ty.IsFloat) { + return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatMantissa)); + } else { + Contract.Assume(ty.IsInt); + return Expr.Literal(Basetypes.BigNum.FromBigInt(n)); + } + } + + List upThresholds; // invariant: thresholds are sorted + List downThresholds; // invariant: thresholds are sorted + + /// + /// Requires "thresholds" to be sorted. + /// + public NativeIntervallDomain() { + upThresholds = new List(); + downThresholds = new List(); + } + + public override void Specialize(Implementation impl) { + if (impl == null) { + // remove thresholds + upThresholds = new List(); + downThresholds = new List(); + } else { + var tf = new ThresholdFinder(impl); + tf.Find(out downThresholds, out upThresholds); +#if DEBUG_PRINT + Console.Write("DEBUG: for implementation '{0}', setting downs to [", impl.Name); + foreach (var i in downThresholds) { + Console.Write(" {0}", i); + } + Console.Write(" ] and ups to ["); + foreach (var i in upThresholds) { + Console.Write(" {0}", i); + } + Console.WriteLine(" ]"); +#endif + } + base.Specialize(impl); + } + + 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 (or hi + /// For a proof of correctness of this method, see Test/dafny2/Intervals.dfy. + /// A difference is that the this method returns: + /// let d = Dafny_RoundDown(k); + /// return d == -1 ? null : downThresholds[d]; + /// + BigInteger? RoundDown(BigInteger k) + { + if (downThresholds.Count == 0 || k < downThresholds[0]) { + return null; + } + var i = 0; + var j = downThresholds.Count - 1; + while (i < j) + { + var mid = i + (j - i + 1) / 2; + if (downThresholds[mid] <= k) { + i = mid; + } else { + j = mid - 1; + } + } + return downThresholds[i]; + } + + /// + /// For a proof of correctness of this method, see Test/dafny2/Intervals.dfy. + /// A difference is that the this method returns: + /// let d = Dafny_RoundUp(k); + /// return d == thresholds.Count ? null : upThresholds[d]; + /// + BigInteger? RoundUp(BigInteger k) + { + if (upThresholds.Count == 0 || upThresholds[upThresholds.Count - 1] < k) { + return null; + } + var i = 0; + var j = upThresholds.Count - 1; + while (i < j) + { + var mid = i + (j - i) / 2; + if (upThresholds[mid] < k) { + i = mid + 1; + } else { + j = mid; + } + } + return upThresholds[i]; + } + + 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, BigInteger.One, 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, BigInteger.One); + 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_Common 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_Common)Meet(c, new E(n)); + } + } + return c; + } + case BinaryOperator.Opcode.Neq: { + E_Common 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_Common)Meet(c, cc); + } + } + return c; + } + case BinaryOperator.Opcode.Le: { + E_Common 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_Common)Meet(c, new E(n)); + } + } + return c; + } + case BinaryOperator.Opcode.Lt: { + E_Common 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, v.TypedIdent.Type.IsReal ? lo : 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, v.TypedIdent.Type.IsReal ? hi : hi - 1); + c = c == null ? new E(n) : (E_Common)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 (!v.TypedIdent.Type.IsReal && 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 : ReadOnlyVisitor + { + public BigInteger? Lo; + public BigInteger? Hi; + + readonly BigInteger one = BigInteger.One; + + Node N; + public PEVisitor(Node n) { + N = n; + } + + // Override visitors for all expressions that can return a boolean, integer, or real result + + public override Expr VisitExpr(Expr node) { + Lo = Hi = null; + return base.VisitExpr(node); + } + public override Expr VisitLiteralExpr(LiteralExpr node) { + if (node.Val is BigNum) { + var n = ((BigNum)node.Val).ToBigInteger; + Lo = n; + Hi = n + 1; + } else if (node.Val is BigDec) { + BigInteger floor, ceiling; + ((BigDec)node.Val).FloorCeiling(out floor, out ceiling); + Lo = floor; + Hi = ceiling; + } else if (node.Val is BigFloat) { + BigNum floor, ceiling; + ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling); + Lo = floor.ToBigInteger; + Hi = ceiling.ToBigInteger; + } 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.Type.IsReal) { + 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.Count == 1); + if (op.Op == UnaryOperator.Opcode.Neg) { + BigInteger? lo, hi; + VisitExpr(node.Args[0]); + lo = Lo; hi = Hi; + if (hi != null) { + Lo = node.Type.IsReal ? -hi : 1 - hi; + } else { + Lo = null; + } + if (lo != null) { + Hi = node.Type.IsReal ? -lo : 1 - lo; + } else { + Hi = null; + } + } + else 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.Count == 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; + var isReal = node.Args[0].Type.IsReal; + 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 && (isReal ? hi0 < lo1 : hi0 <= lo1)) { + // no overlap + Lo = null; Hi = one; + } else if (lo0 != null && hi1 != null && (isReal ? hi1 < lo0 : hi1 <= lo0)) { + Lo = null; Hi = one; + // no overlaop + } else if (lo0 != null && hi0 != null && lo1 != null && hi1 != null && + lo0 == lo1 && hi0 == hi1 && // ranges are the same + (isReal ? lo0 == hi0 : lo0 + 1 == hi0)) { // unit range + // both ranges are the same unit range + Lo = one; Hi = null; + } + if (op.Op == BinaryOperator.Opcode.Neq) { + var tmp = Lo; Lo = Hi; Hi = tmp; + } + break; + case BinaryOperator.Opcode.Le: + if (isReal) { + // If hi0 <= lo1, then the answer is true. + // If hi1 < lo0, then the answer is false. + if (hi0 != null && lo1 != null && hi0 <= lo1) { + Lo = one; Hi = null; + } else if (hi1 != null && lo0 != null && hi1 < lo0) { + Lo = null; Hi = one; + } + } else { + // 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; + } + } + break; + case BinaryOperator.Opcode.Lt: + if (isReal) { + // If hi0 < lo1, then the answer is true. + // If hi1 <= lo0, then the answer is false. + if (hi0 != null && lo1 != null && hi0 < lo1) { + Lo = one; Hi = null; + } else if (hi1 != null && lo0 != null && hi1 <= lo0) { + Lo = null; Hi = one; + } + } else { + // 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; + } + } + break; + case BinaryOperator.Opcode.Gt: + // swap the operands and then continue as Lt + { + var tmp = lo0; lo0 = lo1; lo1 = tmp; + tmp = hi0; hi0 = hi1; hi1 = tmp; + } + goto case BinaryOperator.Opcode.Lt; + case BinaryOperator.Opcode.Ge: + // swap the operands and then continue as Le + { + var tmp = lo0; lo0 = lo1; lo1 = tmp; + tmp = hi0; hi0 = hi1; hi1 = tmp; + } + goto case BinaryOperator.Opcode.Le; + case BinaryOperator.Opcode.Add: + if (lo0 != null && lo1 != null) { + Lo = lo0 + lo1; + } + if (hi0 != null && hi1 != null) { + Hi = isReal ? hi0 + hi1 : hi0 + hi1 - 1; + } + break; + case BinaryOperator.Opcode.Sub: + if (lo0 != null && hi1 != null) { + Lo = isReal ? lo0 - hi1 : 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 : isReal ? hi0 * hi1 : (hi0 - 1) * (hi1 - 1) + 1; + } else if ((BigInteger)lo0 < 0 && (BigInteger)lo1 < 0) { + Lo = null; // approximation + Hi = isReal ? lo0 * lo1 : 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 = BigInteger.Zero; + Hi = hi0; + } + 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 = BigInteger.Zero; + Hi = hi1; + if (lo0 < lo1 && hi0 != null && hi0 < lo1) { + Lo = lo0; + Hi = hi0; + } + } + break; + case BinaryOperator.Opcode.RealDiv: + // this uses an incomplete approximation that could be tightened up + if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { + Lo = BigInteger.Zero; + Hi = 1 <= (BigInteger)lo1 ? hi0 : null; + } + break; + case BinaryOperator.Opcode.Pow: + // this uses an incomplete approximation that could be tightened up + if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { + Lo = 1 <= (BigInteger)lo1 ? BigInteger.One : BigInteger.Zero; + Hi = hi1; + } + break; + default: + break; + } + } else if (node.Fun is IfThenElse) { + var op = (IfThenElse)node.Fun; + Contract.Assert(node.Args.Count == 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); + } + } else if (node.Fun is FunctionCall) { + var call = (FunctionCall)node.Fun; + // See if this is an identity function, which we do by checking: that the function has + // exactly one argument and the function has been marked by the user with the attribute {:identity} + bool claimsToBeIdentity = false; + if (call.ArgumentCount == 1 && call.Func.CheckBooleanAttribute("identity", ref claimsToBeIdentity) && claimsToBeIdentity && node.Args[0].Type.Equals(node.Type)) { + VisitExpr(node.Args[0]); + } + } + 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 Expr VisitBvConcatExpr(BvConcatExpr node) { + // don't recurse on subexpression + return node; + } + public override Expr 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; + } + } + + public class ThresholdFinder : ReadOnlyVisitor + { + readonly Implementation Impl; + public ThresholdFinder(Implementation impl) { + Contract.Requires(impl != null); + Impl = impl; + } + HashSet downs = new HashSet(); + HashSet ups = new HashSet(); + public void Find(out List downThresholds, out List upThresholds) { + // always include -1, 0, 1 as down-thresholds + downs.Clear(); + downs.Add(-1); + downs.Add(0); + downs.Add(1); + // always include 0 and 1 as up-thresholds + ups.Clear(); + ups.Add(0); + ups.Add(1); + + foreach (Requires p in Impl.Proc.Requires) { + Visit(p.Condition); + } + foreach (Ensures p in Impl.Proc.Ensures) { + Visit(p.Condition); + } + foreach (var b in Impl.Blocks) { + foreach (Cmd c in b.Cmds) { + Visit(c); + } + } + + // convert the HashSets to sorted Lists and return + downThresholds = new List(); + foreach (var i in downs) { + downThresholds.Add(i); + } + downThresholds.Sort(); + upThresholds = new List(); + foreach (var i in ups) { + upThresholds.Add(i); + } + upThresholds.Sort(); + } + + public override Expr VisitNAryExpr(NAryExpr node) { + if (node.Fun is BinaryOperator) { + var op = (BinaryOperator)node.Fun; + Contract.Assert(node.Args.Count == 2); + var arg0 = node.Args[0]; + var arg1 = node.Args[1]; + var offset = arg0.Type.IsReal ? 0 : 1; + BigInteger? k; + switch (op.Op) { + case BinaryOperator.Opcode.Eq: + case BinaryOperator.Opcode.Neq: + k = AsIntLiteral(arg0); + if (k != null) { + var i = (BigInteger)k; + downs.Add(i - 1); + downs.Add(i); + ups.Add(i + 1); + ups.Add(i + 2); + } + k = AsIntLiteral(arg1); + if (k != null) { + var i = (BigInteger)k; + downs.Add(i - 1); + downs.Add(i); + ups.Add(i + 1); + ups.Add(i + 2); + } + break; + case BinaryOperator.Opcode.Le: + k = AsIntLiteral(arg0); + if (k != null) { + var i = (BigInteger)k; + downs.Add(i - 1); + downs.Add(i); + } + k = AsIntLiteral(arg1); + if (k != null) { + var i = (BigInteger)k; + ups.Add(i + offset); + ups.Add(i + 1 + offset); + } + break; + case BinaryOperator.Opcode.Lt: + k = AsIntLiteral(arg0); + if (k != null) { + var i = (BigInteger)k; + downs.Add(i ); + downs.Add(i + 1); + } + k = AsIntLiteral(arg1); + if (k != null) { + var i = (BigInteger)k; + ups.Add(i - 1 + offset); + ups.Add(i + offset); + } + break; + 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 base.VisitNAryExpr(node); + } + + BigInteger? AsIntLiteral(Expr e) { + var lit = e as LiteralExpr; + if (lit != null && lit.isBigNum) { + BigNum bn = lit.asBigNum; + return bn.ToBigInteger; + } + return null; + } + } + +} -- cgit v1.2.3