diff options
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 229 | ||||
| -rw-r--r-- | Source/AbsInt/NativeLattice.cs | 10 | ||||
| -rw-r--r-- | Test/aitest0/Answer | 14 | ||||
| -rw-r--r-- | Test/aitest0/Intervals.bpl | 56 | ||||
| -rw-r--r-- | Test/dafny2/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny2/Intervals.dfy | 63 | ||||
| -rw-r--r-- | Test/dafny2/runtest.bat | 1 |
7 files changed, 369 insertions, 8 deletions
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<BigInteger> upThresholds; // invariant: thresholds are sorted
+ List<BigInteger> downThresholds; // invariant: thresholds are sorted
+
+ /// <summary>
+ /// Requires "thresholds" to be sorted.
+ /// </summary>
+ public NativeIntervallDomain() {
+ upThresholds = new List<BigInteger>();
+ downThresholds = new List<BigInteger>();
+ }
+
+ public override void Specialize(Implementation impl) {
+ if (impl == null) {
+ // remove thresholds
+ upThresholds = new List<BigInteger>();
+ downThresholds = new List<BigInteger>();
+ } 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 }
}
+ /// <summary>
+ /// 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];
+ /// </summary>
+ 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];
+ }
+
+ /// <summary>
+ /// 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];
+ /// </summary>
+ 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<BigInteger> downs = new HashSet<BigInteger>();
+ HashSet<BigInteger> ups = new HashSet<BigInteger>();
+ public void Find(out List<BigInteger> downThresholds, out List<BigInteger> 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<BigInteger>();
+ foreach (var i in downs) {
+ downThresholds.Add(i);
+ }
+ downThresholds.Sort();
+ upThresholds = new List<BigInteger>();
+ 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);
+ /// <summary>
+ /// Specialize the lattice to implementation "impl", if non-null.
+ /// If "impl" is null, remove specialization.
+ /// </summary>
+ 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);
}
}
}
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer index e517aa18..73a9509c 100644 --- a/Test/aitest0/Answer +++ b/Test/aitest0/Answer @@ -109,5 +109,15 @@ implementation Evaluate() Boogie program verifier finished with 0 verified, 0 errors
-
-Boogie program verifier finished with 1 verified, 0 errors
+Intervals.bpl(62,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(57,5): anon0
+ Intervals.bpl(58,3): anon3_LoopHead
+ Intervals.bpl(58,3): anon3_LoopDone
+Intervals.bpl(73,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(68,5): anon0
+ Intervals.bpl(69,3): anon3_LoopHead
+ Intervals.bpl(69,3): anon3_LoopDone
+
+Boogie program verifier finished with 4 verified, 2 errors
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl index 49d27b1c..7ed2c3d2 100644 --- a/Test/aitest0/Intervals.bpl +++ b/Test/aitest0/Intervals.bpl @@ -17,3 +17,59 @@ procedure P(K: int) }
assert 13 <= x;
}
+
+procedure Thresholds0()
+{
+ var i: int;
+ i := 0;
+ while (i < 200)
+ {
+ i := i + 1;
+ }
+ assert i == 200;
+}
+
+procedure Thresholds1()
+{
+ var i: int;
+ i := 0;
+ while (i <= 199)
+ {
+ i := i + 1;
+ }
+ assert i == 200;
+}
+
+procedure Thresholds2()
+{
+ var i: int;
+ i := 100;
+ while (0 < i)
+ {
+ i := i - 1;
+ }
+ assert i == 0;
+}
+
+procedure Thresholds3()
+{
+ var i: int;
+ i := 0;
+ while (i < 200)
+ {
+ i := i + 1;
+ }
+ assert i == 199; // error
+}
+
+procedure Thresholds4()
+{
+ var i: int;
+ i := 0;
+ while (i + 3 < 203)
+ {
+ i := i + 1;
+ }
+ assert i * 2 == 400; // error: this would hold in an execution, but /infer:j is too weak to infer invariant i<=200
+}
+
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index 9cb94f69..ea481dae 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -26,3 +26,7 @@ Dafny program verifier finished with 4 verified, 0 errors -------------------- COST-verif-comp-2011-4-FloydCycleDetect.dfy --------------------
Dafny program verifier finished with 23 verified, 0 errors
+
+-------------------- Intervals.dfy --------------------
+
+Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/dafny2/Intervals.dfy b/Test/dafny2/Intervals.dfy new file mode 100644 index 00000000..f04f6411 --- /dev/null +++ b/Test/dafny2/Intervals.dfy @@ -0,0 +1,63 @@ +// The RoundDown and RoundUp methods in this file are the ones in the Boogie
+// implementation Source/AbsInt/IntervalDomain.cs.
+
+var thresholds: array<int>;
+
+function Valid(): bool
+ reads this, thresholds;
+{
+ thresholds != null &&
+ forall m,n :: 0 <= m < n < thresholds.Length ==> thresholds[m] <= thresholds[n]
+}
+
+method RoundDown(k: int) returns (r: int)
+ requires Valid();
+ ensures -1 <= r < thresholds.Length;
+ ensures forall m :: r < m < thresholds.Length ==> k < thresholds[m];
+ ensures 0 <= r ==> thresholds[r] <= k;
+{
+ if (thresholds.Length == 0 || k < thresholds[0]) {
+ return -1;
+ }
+ var i, j := 0, thresholds.Length - 1;
+ while (i < j)
+ invariant 0 <= i <= j < thresholds.Length;
+ invariant thresholds[i] <= k;
+ invariant forall m :: j < m < thresholds.Length ==> k < thresholds[m];
+ {
+ var mid := i + (j - i + 1) / 2;
+ assert i < mid <= j;
+ if (thresholds[mid] <= k) {
+ i := mid;
+ } else {
+ j := mid - 1;
+ }
+ }
+ return i;
+}
+
+method RoundUp(k: int) returns (r: int)
+ requires Valid();
+ ensures 0 <= r <= thresholds.Length;
+ ensures forall m :: 0 <= m < r ==> thresholds[m] < k;
+ ensures r < thresholds.Length ==> k <= thresholds[r];
+{
+ if (thresholds.Length == 0 || thresholds[thresholds.Length-1] < k) {
+ return thresholds.Length;
+ }
+ var i, j := 0, thresholds.Length - 1;
+ while (i < j)
+ invariant 0 <= i <= j < thresholds.Length;
+ invariant k <= thresholds[j];
+ invariant forall m :: 0 <= m < i ==> thresholds[m] < k;
+ {
+ var mid := i + (j - i) / 2;
+ assert i <= mid < j;
+ if (thresholds[mid] < k) {
+ i := mid + 1;
+ } else {
+ j := mid;
+ }
+ }
+ return i;
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index d7c0dc79..79ee0f89 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -14,6 +14,7 @@ for %%f in ( COST-verif-comp-2011-2-MaxTree-datatype.dfy
COST-verif-comp-2011-3-TwoDuplicates.dfy
COST-verif-comp-2011-4-FloydCycleDetect.dfy
+ Intervals.dfy
) do (
echo.
echo -------------------- %%f --------------------
|