diff options
-rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 161 | ||||
-rw-r--r-- | Source/Basetypes/BigDec.cs | 34 | ||||
-rw-r--r-- | Source/Concurrency/MoverCheck.cs | 14 | ||||
-rw-r--r-- | Test/aitest9/TestIntervals.bpl | 30 | ||||
-rw-r--r-- | Test/aitest9/answer | 12 |
5 files changed, 173 insertions, 78 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 640a50fc..6cce0aac 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -34,7 +34,8 @@ namespace Microsoft.Boogie.AbstractInterpretation 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 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;
@@ -153,7 +154,7 @@ namespace Microsoft.Boogie.AbstractInterpretation if (!V.IsMutable && CommandLineOptions.Clo.InstrumentInfer != CommandLineOptions.InstrumentationPlaces.Everywhere) {
// omit invariants about readonly variables
return Expr.True;
- } else if (V.TypedIdent.Type.IsBool) {
+ } else if (V.TypedIdent.Type.IsBool) {
if (Lo == null && Hi == null) {
return Expr.True;
} else {
@@ -161,7 +162,7 @@ namespace Microsoft.Boogie.AbstractInterpretation var ide = new IdentifierExpr(Token.NoToken, V);
return Hi == null ? ide : Expr.Not(ide);
}
- } else {
+ } else if (V.TypedIdent.Type.IsInt) {
Expr e = Expr.True;
if (Lo != null && Hi != null && Lo + 1 == Hi) {
// produce an equality
@@ -179,6 +180,25 @@ namespace Microsoft.Boogie.AbstractInterpretation }
}
return e;
+ } else {
+ Contract.Assert(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;
}
}
}
@@ -292,8 +312,8 @@ namespace Microsoft.Boogie.AbstractInterpretation } 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) {
+ // if hi<=lo (or hi<lo for reals), then we're overconstrained
+ if (lo != null && hi != null && (x.V.TypedIdent.Type.IsReal ? hi < lo : hi <= lo)) {
return bottom;
}
n = new Node(x.V, lo, hi);
@@ -457,7 +477,7 @@ namespace Microsoft.Boogie.AbstractInterpretation E_Common Constraint(Expr expr, Node state) {
Variable v;
if (IsVariable(expr, out v)) {
- var n = new Node(v, new BigInteger(1), null);
+ var n = new Node(v, BigInteger.One, null);
return new E(n);
} else if (expr is LiteralExpr) {
var e = (LiteralExpr)expr;
@@ -467,7 +487,7 @@ namespace Microsoft.Boogie.AbstractInterpretation 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));
+ var n = new Node(v, null, BigInteger.One);
return new E(n);
}
}
@@ -534,7 +554,7 @@ namespace Microsoft.Boogie.AbstractInterpretation BigInteger? lo, hi;
PartiallyEvaluate(arg0, state, out lo, out hi);
if (lo != null) {
- var n = new Node(v, lo + 1, null);
+ var n = new Node(v, v.TypedIdent.Type.IsReal ? lo : lo + 1, null);
c = new E(n);
}
}
@@ -542,7 +562,7 @@ namespace Microsoft.Boogie.AbstractInterpretation BigInteger? lo, hi;
PartiallyEvaluate(arg1, state, out lo, out hi);
if (hi != null) {
- var n = new Node(v, null, hi - 1);
+ 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));
}
}
@@ -567,7 +587,7 @@ namespace Microsoft.Boogie.AbstractInterpretation 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) {
+ 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.
@@ -626,14 +646,14 @@ namespace Microsoft.Boogie.AbstractInterpretation public BigInteger? Lo;
public BigInteger? Hi;
- readonly BigInteger one = new BigInteger(1);
+ readonly BigInteger one = BigInteger.One;
Node N;
public PEVisitor(Node n) {
N = n;
}
- // Override visitors for all expressions that can return a boolean or integer result
+ // Override visitors for all expressions that can return a boolean, integer, or real result
public override Expr VisitExpr(Expr node) {
Lo = Hi = null;
@@ -645,9 +665,10 @@ namespace Microsoft.Boogie.AbstractInterpretation Lo = n;
Hi = n + 1;
} else if (node.Val is BigDec) {
- var n = ((BigDec)node.Val).Floor(-BigInteger.Pow(10, 12), BigInteger.Pow(10, 12));
- Lo = n;
- Hi = n + 1;
+ BigInteger floor, ceiling;
+ ((BigDec)node.Val).FloorCeiling(out floor, out ceiling);
+ Lo = floor;
+ Hi = ceiling;
} else if (node.Val is bool) {
if ((bool)node.Val) {
// true
@@ -676,10 +697,10 @@ namespace Microsoft.Boogie.AbstractInterpretation VisitExpr(node.Args[0]);
lo = Lo; hi = Hi;
if (hi != null) {
- Lo = 1 - hi;
+ Lo = node.Type.IsReal ? -hi : 1 - hi;
}
if (lo != null) {
- Hi = 1 - lo;
+ Hi = node.Type.IsReal ? -lo : 1 - lo;
}
}
else if (op.Op == UnaryOperator.Opcode.Not) {
@@ -700,6 +721,7 @@ namespace Microsoft.Boogie.AbstractInterpretation 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) {
@@ -750,12 +772,16 @@ namespace Microsoft.Boogie.AbstractInterpretation // 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) {
+ if (hi0 != null && lo1 != null && (isReal ? hi0 < lo1 : hi0 <= lo1)) {
+ // no overlap
Lo = null; Hi = one;
- } else if (lo0 != null && hi1 != null && hi1 <= lo0) {
+ } 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 + 1 == hi0 && lo0 == lo1 && lo1 + 1 == hi1) {
+ 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) {
@@ -763,42 +789,68 @@ namespace Microsoft.Boogie.AbstractInterpretation }
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;
+ 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:
- 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;
+ 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 = hi0 + hi1 - 1;
+ Hi = isReal ? hi0 + hi1 : hi0 + hi1 - 1;
}
break;
case BinaryOperator.Opcode.Sub:
if (lo0 != null && hi1 != null) {
- Lo = lo0 - hi1 + 1;
+ Lo = isReal ? lo0 - hi1 : lo0 - hi1 + 1;
}
if (hi0 != null && lo1 != null) {
Hi = hi0 - lo1;
@@ -809,38 +861,38 @@ namespace Microsoft.Boogie.AbstractInterpretation 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;
+ 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 = lo0 * lo1 + 1;
+ 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 = new BigInteger(0);
+ 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 = new BigInteger(0);
+ 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 = new BigInteger(0);
- Hi = hi1;
+ 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 = new BigInteger(0);
+ Lo = 1 <= (BigInteger)lo1 ? BigInteger.One : BigInteger.Zero;
Hi = hi1;
}
break;
@@ -1052,6 +1104,7 @@ namespace Microsoft.Boogie.AbstractInterpretation 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:
@@ -1083,22 +1136,22 @@ namespace Microsoft.Boogie.AbstractInterpretation k = AsIntLiteral(arg1);
if (k != null) {
var i = (BigInteger)k;
- ups.Add(i + 1);
- ups.Add(i + 2);
+ 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 );
downs.Add(i + 1);
}
k = AsIntLiteral(arg1);
if (k != null) {
var i = (BigInteger)k;
- ups.Add(i);
- ups.Add(i + 1);
+ ups.Add(i - 1 + offset);
+ ups.Add(i + offset);
}
break;
case BinaryOperator.Opcode.Ge:
diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs index beb9ec54..feabb425 100644 --- a/Source/Basetypes/BigDec.cs +++ b/Source/Basetypes/BigDec.cs @@ -136,31 +136,25 @@ namespace Microsoft.Basetypes { ////////////////////////////////////////////////////////////////////////////
// Conversion operations
- [Pure]
- public BIM Floor(BIM? minimum, BIM? maximum) {
+ public void FloorCeiling(out BIM floor, out BIM ceiling) {
BIM n = this.mantissa;
-
- if (this.exponent >= 0) {
- int e = this.exponent;
- while (e > 0 && (minimum == null || minimum <= n) && (maximum == null || n <= maximum)) {
+ int e = this.exponent;
+ if (n.IsZero) {
+ floor = ceiling = n;
+ } else if (0 <= e) {
+ // it's an integer
+ for (; 0 < e; e--) {
n = n * ten;
- e = e - 1;
}
- }
- else {
- int e = -this.exponent;
- while (e > 0 && !n.IsZero) {
- n = n / ten;
- e = e - 1;
+ floor = ceiling = n;
+ } else {
+ // it's a non-zero integer, so the ceiling is one more than the fllor
+ for (; e < 0 && !n.IsZero; e++) {
+ n = n / ten; // since we're dividing by a positive number, this will round down
}
+ floor = n;
+ ceiling = n + 1;
}
-
- if (minimum != null && n < minimum)
- return (BIM)minimum;
- else if (maximum != null && maximum < n)
- return (BIM)maximum;
- else
- return n;
}
[Pure]
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index cde18ba4..7583d250 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -350,6 +350,10 @@ namespace Microsoft.Boogie }
returnExpr = Expr.Or(returnExpr, expr);
}
+ ResolutionContext rc = new ResolutionContext(null);
+ rc.StateMode = ResolutionContext.State.Two;
+ returnExpr.Resolve(rc);
+ returnExpr.Typecheck(new TypecheckingContext(null));
return returnExpr;
}
@@ -360,6 +364,10 @@ namespace Microsoft.Boogie {
transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition(path));
}
+ ResolutionContext rc = new ResolutionContext(null);
+ rc.StateMode = ResolutionContext.State.Two;
+ transitionRelation.Resolve(rc);
+ transitionRelation.Typecheck(new TypecheckingContext(null));
return transitionRelation;
}
@@ -584,8 +592,10 @@ namespace Microsoft.Boogie foreach (AssertCmd assertCmd in first.thatGate)
{
requiresExpr = Expr.And(assertCmd.Expr, requiresExpr);
+ requiresExpr.Type = Type.Bool;
}
Expr failureExpr = Expr.Not(requiresExpr);
+ failureExpr.Type = Type.Bool;
List<Requires> requires = DisjointnessRequires(program, first, second);
requires.Add(new Requires(false, failureExpr));
foreach (AssertCmd assertCmd in second.thisGate)
@@ -616,15 +626,13 @@ namespace Microsoft.Boogie List<Variable> inputs = new List<Variable>();
inputs.AddRange(second.thisInParams);
- Expr failureExpr = Expr.True;
List<Requires> requires = DisjointnessRequires(program, null, second);
- requires.Add(new Requires(false, failureExpr));
foreach (AssertCmd assertCmd in second.thisGate)
{
requires.Add(new Requires(false, assertCmd.Expr));
}
- Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(failureExpr);
+ Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(Expr.True);
List<Ensures> ensures = new List<Ensures>();
Ensures ensureCheck = new Ensures(false, ensuresExpr);
ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name);
diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl index bee73a57..622a0b36 100644 --- a/Test/aitest9/TestIntervals.bpl +++ b/Test/aitest9/TestIntervals.bpl @@ -38,3 +38,33 @@ procedure Q(myField: Field [ref][teflon]bool, r: ref, t: teflon) {
Heap[myField][r][t] := true;
}
+
+// -----
+
+procedure Neq()
+{
+ var n: int;
+ assume 2 <= n && n <= 10;
+ assume 2 != n;
+ assume n != 10;
+ while (*) {
+ n := n;
+ }
+ assert 3 <= n;
+ assert n < 10;
+}
+
+procedure NeqX()
+{
+ var n: real;
+ assume 2.0 <= n && n <= 10.0;
+ assume 2.0 != n;
+ assume n != 10.0;
+ // The following statement will cause Boogie to know about n only
+ // what the abstract interpreter has inferred so far.
+ while (*) { n := n; }
+
+ assert 2.0 <= n && n <= 10.0; // yes
+ assert 2.0 < n; // error, the abstract domain is not precise enough to figure this out
+ assert n < 10.0; // error, ditto
+}
diff --git a/Test/aitest9/answer b/Test/aitest9/answer index d68508af..88af771c 100644 --- a/Test/aitest9/answer +++ b/Test/aitest9/answer @@ -17,5 +17,15 @@ Execution trace: TestIntervals.bpl(13,14): anon11_Then
TestIntervals.bpl(14,14): anon12_Then
TestIntervals.bpl(17,5): anon8
+TestIntervals.bpl(68,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ TestIntervals.bpl(60,3): anon0
+ TestIntervals.bpl(65,3): anon3_LoopHead
+ TestIntervals.bpl(65,3): anon3_LoopDone
+TestIntervals.bpl(69,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ TestIntervals.bpl(60,3): anon0
+ TestIntervals.bpl(65,3): anon3_LoopHead
+ TestIntervals.bpl(65,3): anon3_LoopDone
-Boogie program verifier finished with 1 verified, 1 error
+Boogie program verifier finished with 2 verified, 3 errors
|