summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/AbsInt/IntervalDomain.cs8
-rw-r--r--Source/Core/Absy.cs44
-rw-r--r--Source/Core/CommandLineOptions.cs8
-rw-r--r--Test/aitest0/Answer42
-rw-r--r--Test/aitest0/Intervals.bpl225
5 files changed, 315 insertions, 12 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index be62eb58..c024a62a 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -857,6 +857,14 @@ namespace Microsoft.Boogie.AbstractInterpretation
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;
}
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c20798b2..39343e6f 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -979,21 +979,43 @@ namespace Microsoft.Boogie {
}
}
- // Look for {:name true} or {:name false} in list of attributes. Return result in 'result'
- // (which is not touched if there is no attribute specified).
- //
- // Returns false is there was an error processing the flag, true otherwise.
+ /// <summary>
+ /// If the declaration has an attribute {:name} or {:name true}, then set "result" to "true" and return "true".
+ /// If the declaration has an attribute {:name false}, then set "result" to "false" and return "true".
+ /// Otherwise, return "false" and leave "result" unchanged (which gives the caller an easy way to indicate
+ /// a default value if the attribute is not mentioned).
+ /// If there is more than one attribute called :name, then the last attribute rules.
+ /// </summary>
public bool CheckBooleanAttribute(string name, ref bool result) {
Contract.Requires(name != null);
- Expr expr = FindExprAttribute(name);
- if (expr != null) {
- if (expr is LiteralExpr && ((LiteralExpr)expr).isBool) {
- result = ((LiteralExpr)expr).asBool;
- } else {
- return false;
+ var kv = FindAttribute(name);
+ if (kv != null) {
+ if (kv.Params.Count == 0) {
+ result = true;
+ return true;
+ } else if (kv.Params.Count == 1) {
+ var lit = kv.Params[0] as LiteralExpr;
+ if (lit != null && lit.isBool) {
+ result = lit.asBool;
+ return true;
+ }
}
}
- return true;
+ return false;
+ }
+
+ /// <summary>
+ /// Find and return the last occurrence of an attribute with the name "name", if any. If none, return null.
+ /// </summary>
+ public QKeyValue FindAttribute(string name) {
+ Contract.Requires(name != null);
+ QKeyValue res = null;
+ for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
+ if (kv.Key == name) {
+ res = kv;
+ }
+ }
+ return res;
}
// Look for {:name expr} in list of attributes.
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index fdd4d9e3..f23eaf3b 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1506,6 +1506,14 @@ namespace Microsoft.Boogie {
trigger annotations. Internally it works by adding {:nopats ...}
annotations to quantifiers.
+ {:identity}
+ {:identity true}
+ If the function has 1 argument and the use of it has type X->X for
+ some X, then the abstract interpreter will treat the function as an
+ identity function. Note, the abstract interpreter trusts the
+ attribute--it does not try to verify that the function really is an
+ identity function.
+
---- On variables ----------------------------------------------------------
{:existential true}
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index dabe9710..961b3c33 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -124,5 +124,45 @@ Execution trace:
Intervals.bpl(87,5): anon0
Intervals.bpl(88,3): loop_head
Intervals.bpl(91,3): after_loop
+Intervals.bpl(138,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(133,5): anon0
+ Intervals.bpl(134,3): anon3_LoopHead
+ Intervals.bpl(134,3): anon3_LoopDone
+Intervals.bpl(149,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(144,5): anon0
+ Intervals.bpl(145,3): anon3_LoopHead
+ Intervals.bpl(145,3): anon3_LoopDone
+Intervals.bpl(200,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(190,8): anon0
+ Intervals.bpl(191,3): anon4_LoopHead
+ Intervals.bpl(191,3): anon4_LoopDone
+Intervals.bpl(238,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(233,5): anon0
+ Intervals.bpl(234,3): anon3_LoopHead
+ Intervals.bpl(234,3): anon3_LoopDone
+Intervals.bpl(250,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(244,8): anon0
+ Intervals.bpl(245,3): anon3_LoopHead
+ Intervals.bpl(245,3): anon3_LoopDone
+Intervals.bpl(261,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(256,5): anon0
+ Intervals.bpl(257,3): anon3_LoopHead
+ Intervals.bpl(257,3): anon3_LoopDone
+Intervals.bpl(283,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(278,5): anon0
+ Intervals.bpl(279,3): anon3_LoopHead
+ Intervals.bpl(279,3): anon3_LoopDone
+Intervals.bpl(305,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Intervals.bpl(300,5): anon0
+ Intervals.bpl(301,3): anon3_LoopHead
+ Intervals.bpl(301,3): anon3_LoopDone
-Boogie program verifier finished with 5 verified, 3 errors
+Boogie program verifier finished with 15 verified, 11 errors
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index 4520a032..6a588bbe 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -91,3 +91,228 @@ procedure UnaryNegation1() returns (x: int) // this was once buggy
after_loop:
assert x == 1; // error
}
+
+// --------------------------- test {:identity} annotation --------------------
+
+function {:identity} MyId(x: int): int;
+function MyStealthyId(x: int): int; // this one messes up the abstract interpretation
+function {:identity false} {:identity}/*the last attribute rules*/ MyPolyId<T>(x: T): T;
+function {:identity /*this is a lie*/} MyBogusId(x: int): int { -x }
+function {:identity /*ignored, since the function takes more than one argument*/} MultipleArgs(x: int, y: int): int;
+function {:identity /*ignored, since the return type is not equal to the argument type*/} BoolToInt(b: bool): int;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId0<T>(x: T): int;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId1<T>(x: int): T;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId2<T,U>(x: T): U;
+
+
+procedure Id0(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + 1;
+ }
+ assert 0 <= i;
+}
+
+procedure Id1(n: int)
+{
+ var i: int;
+ i := MyId(0);
+ while (i < n)
+ {
+ i := i + MyId(1);
+ }
+ assert 0 <= i;
+}
+
+procedure Id2(n: int)
+{
+ var i: int;
+ i := MyStealthyId(0);
+ while (i < n)
+ {
+ i := i + 1;
+ }
+ assert 0 <= i; // error: abstract interpreter does not figure this one out
+}
+
+procedure Id3(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + MyStealthyId(1);
+ }
+ assert 0 <= i; // error: abstract interpreter does not figure this one out
+}
+
+procedure Id4(n: int)
+{
+ var i: int;
+ i := MyPolyId(0);
+ while (i < n)
+ {
+ i := i + MyPolyId(1);
+ }
+ assert 0 <= i;
+}
+
+procedure Id5(n: int)
+{
+ var i: int;
+ var b: bool;
+ i, b := 0, false;
+ while (i < n)
+ {
+ i, b := i + 1, false;
+ }
+ assert !b;
+}
+
+procedure Id6(n: int)
+{
+ var i: int;
+ var b: bool;
+ i, b := 0, MyPolyId(false);
+ while (i < n)
+ {
+ i, b := i + 1, false;
+ }
+ assert !b;
+}
+
+procedure Id7(n: int)
+{
+ var i, k, y, z: int;
+ i, k := 0, 0;
+ while (i < n)
+ {
+ i := i + 1;
+ y, z := MyBogusId(5), -5;
+ k := k + z;
+ if (*) {
+ assert y == z; // fine
+ }
+ }
+ assert 0 <= k; // error: this does not hold -- k may very well be negative
+}
+
+procedure Id8(n: int)
+{
+ var i, k: int;
+ i, k := 0, 0;
+ while (i < n)
+ {
+ i := i + 1;
+ k := k + MyBogusId(5);
+ }
+ assert 0 <= k; // since we lied about MyBogusId being an {:identity} function, the abstract interpreter gives us this bogus invariant
+}
+
+procedure Id9(n: int)
+ requires 0 < n;
+{
+ var i, k: int;
+ i, k := 0, 0;
+ while (i < n)
+ invariant i <= n && -k == 5*i;
+ {
+ i := i + 1;
+ k := k + MyBogusId(5);
+ }
+ assert -k == 5*n;
+ assert false; // this just shows the effect of MyBogusId even more; there is no complaint about this assert
+}
+
+procedure Id10(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + MultipleArgs(19, 23);
+ }
+ assert 0 <= i; // error: no information is known about i
+}
+
+procedure Id11(n: int)
+{
+ var i, k: int;
+ i, k := 0, 0;
+ while (i < n)
+ {
+ i := i + 1;
+ k := k + BoolToInt(false); // this should not be treated as an identity function, since it goes from one type to another
+ }
+ assert 0 <= k; // error: no information is known about k
+}
+
+procedure Id12(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId0(false);
+ }
+ assert 0 <= i; // error: no information is known about i
+}
+
+procedure Id13(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId0(1);
+ }
+ assert 0 <= i;
+}
+
+procedure Id14(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId0(-1);
+ }
+ assert 0 <= i; // error: this does not hold
+}
+
+procedure Id15(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId1(1);
+ }
+ assert 0 <= i; // fine: SometimesId1 claims to be an identity and the use of it is int->int
+}
+
+procedure Id16(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId2(false);
+ }
+ assert 0 <= i; // error: no information is known about i
+}
+
+procedure Id17(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId2(1);
+ }
+ assert 0 <= i; // fine: SometimesId2 claims to be an identity and the use of it is int->int
+}
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-18 01:52:45 +0000