From de994ac942cd6a017f2f277bd0be37a7e8cc0c98 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 12 Dec 2011 13:53:32 -0800 Subject: Dafny: implemented thresholds for the new interval domain (/infer:j) --- Source/AbsInt/IntervalDomain.cs | 229 ++++++++++++++++++++++++++++++++++++++-- Source/AbsInt/NativeLattice.cs | 10 ++ 2 files changed, 233 insertions(+), 6 deletions(-) (limited to 'Source/AbsInt') diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 1a2904a4..247a357d 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -182,6 +182,40 @@ namespace Microsoft.Boogie.AbstractInterpretation } } + 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(); @@ -310,13 +344,23 @@ namespace Microsoft.Boogie.AbstractInterpretation 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.Lo != null && y.Lo != null) { + if (x.Lo <= y.Lo) { + // okay, we keep the lower bound + lo = x.Lo; + } else { + // set "lo" to the threshold that is below (or equal) y.Lo + lo = RoundDown((BigInteger)y.Lo); + } } - if (x.Hi == null || (y.Hi != null && y.Hi <= x.Hi)) { - // okay, we keep the upper bound - hi = x.Hi; + if (x.Hi != null && y.Hi != null) { + if (y.Hi <= x.Hi) { + // okay, we keep the upper bound + hi = x.Hi; + } else { + // set "hi" to the threshold that is above (or equal) y.Hi + hi = RoundUp((BigInteger)y.Hi); + } } if (lo != null || hi != null) { var n = new Node(x.V, lo, hi); @@ -333,6 +377,56 @@ namespace Microsoft.Boogie.AbstractInterpretation } } + /// + /// 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; @@ -858,4 +952,127 @@ namespace Microsoft.Boogie.AbstractInterpretation } } + public class ThresholdFinder : StandardVisitor + { + 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.Length == 2); + var arg0 = node.Args[0]; + var arg1 = node.Args[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 + 1); + ups.Add(i + 2); + } + 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); + ups.Add(i + 1); + } + 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; + } + } + } diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs index 7abe52e2..d02e6f31 100644 --- a/Source/AbsInt/NativeLattice.cs +++ b/Source/AbsInt/NativeLattice.cs @@ -46,6 +46,13 @@ namespace Microsoft.Boogie.AbstractInterpretation 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); + /// + /// Specialize the lattice to implementation "impl", if non-null. + /// If "impl" is null, remove specialization. + /// + public virtual void Specialize(Implementation impl) { + } + public virtual void Validate() { Contract.Assert(IsTop(Top)); Contract.Assert(IsBottom(Bottom)); @@ -136,7 +143,10 @@ namespace Microsoft.Boogie.AbstractInterpretation Expr e = Substituter.Apply(formalProcImplSubst, pre.Condition); start = lattice.Constrain(start, e); } + + lattice.Specialize(impl); Analyze(impl, lattice, start); + lattice.Specialize(null); } } } -- cgit v1.2.3