summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-12-05 23:07:06 -0800
committerGravatar Rustan Leino <leino@microsoft.com>2011-12-05 23:07:06 -0800
commit95bb8b3b4454fdc1a14fd67b22a5ac6183135cfd (patch)
tree014162d0766bdec9922ea6d314ac05bc2d9a065e
parent9e18c32b3fda7b377f095e8ee865424c51af1e73 (diff)
Boogie: Added new abstract interpretation harness, which uses native Boogie Expr's, not the more abstract AIExpr's.
Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred}
Diffstat
-rw-r--r--Source/AbsInt/AbsInt.csproj4
-rw-r--r--Source/AbsInt/AbstractInterpretation.cs10
-rw-r--r--Source/AbsInt/IntervalDomain.cs861
-rw-r--r--Source/AbsInt/NativeLattice.cs320
-rw-r--r--Source/AbsInt/TrivialDomain.cs79
-rw-r--r--Source/Basetypes/BigNum.cs6
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs30
-rw-r--r--Source/Core/Absy.cs12
-rw-r--r--Source/Core/AbsyCmd.cs1
-rw-r--r--Source/Core/AbsyExpr.cs4
-rw-r--r--Source/Core/CommandLineOptions.cs22
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs62
-rw-r--r--Test/aitest0/Answer38
-rw-r--r--Test/aitest0/Intervals.bpl19
-rw-r--r--Test/aitest0/runtest.bat1
-rw-r--r--Test/aitest1/Answer140
-rw-r--r--Test/dafny0/Answer28
17 files changed, 1486 insertions, 151 deletions
diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index 454fc081..93d304d7 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -147,12 +147,16 @@
<RequiredTargetFramework>3.5</RequiredTargetFramework>
</Reference>
<Reference Include="System.Data" />
+ <Reference Include="System.Numerics" />
<Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
<Compile Include="AbstractInterpretation.cs" />
<Compile Include="ExprFactories.cs" />
+ <Compile Include="IntervalDomain.cs" />
<Compile Include="LoopInvariantsOnDemand.cs" />
+ <Compile Include="TrivialDomain.cs" />
+ <Compile Include="NativeLattice.cs" />
<Compile Include="Traverse.cs" />
<Compile Include="..\version.cs" />
</ItemGroup>
diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs
index a5847594..ef9814c6 100644
--- a/Source/AbsInt/AbstractInterpretation.cs
+++ b/Source/AbsInt/AbstractInterpretation.cs
@@ -70,7 +70,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
this.callReturnWorkItems = new Queue();
}
- private Dictionary<Procedure, Implementation[]> ComputeProcImplMap(Program program) {
+ public static Dictionary<Procedure, Implementation[]> ComputeProcImplMap(Program program) {
Contract.Requires(program != null);
// Since implementations call procedures (impl. signatures)
// rather than directly calling other implementations, we first
@@ -541,20 +541,18 @@ namespace Microsoft.Boogie.AbstractInterpretation {
}
/// <summary>
- /// Flat an expresion in the form P AND Q ... AND R into a list [P, Q, ..., R]
+ /// Flatten an expresion in the form P AND Q ... AND R into a list [P, Q, ..., R]
/// </summary>
private List<Expr/*!>!*/> flatConjunction(Expr embeddedExpr) {
Contract.Requires(embeddedExpr != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expr>>()));
-
- List<Expr/*!>!*/> retValue = new List<Expr/*!*/>();//No asserts necessarry. It is the return value, and thus will be subject to the postcondition
+ var retValue = new List<Expr/*!*/>();
NAryExpr e = embeddedExpr as NAryExpr;
if (e != null && e.Fun.FunctionName.CompareTo("&&") == 0) { // if it is a conjunction
foreach (Expr arg in e.Args) {
Contract.Assert(arg != null);
- List<Expr/*!*/>/*!*/ newConjuncts = flatConjunction(arg);
- Contract.Assert(cce.NonNullElements(newConjuncts));
+ var newConjuncts = flatConjunction(arg);
retValue.AddRange(newConjuncts);
}
} else {
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
new file mode 100644
index 00000000..cf84e4bd
--- /dev/null
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -0,0 +1,861 @@
+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 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
+ 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;
+ }
+
+ /// <summary>
+ /// This constructor leaves Next as null, allowing the caller to fill in Next to finish off the construction.
+ /// </summary>
+ 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;
+ }
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ 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;
+ }
+
+ /// <summary>
+ /// 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).
+ /// </summary>
+ 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);
+ }
+ }
+
+ /// <summary>
+ /// 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).
+ /// </summary>
+ 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<Tuple<Node, Node>> Merge(Node a, Node b) {
+ while (true) {
+ if (a == null && b == null) {
+ yield break;
+ } else if (a == null || b == null) {
+ yield return new Tuple<Node, Node>(a, b);
+ if (a != null) { a = a.Next; } else { b = b.Next; }
+ } else if (a.V == b.V) {
+ yield return new Tuple<Node, Node>(a, b);
+ a = a.Next; b = b.Next;
+ } else if (StrictlyBefore(a.V, b.V)) {
+ yield return new Tuple<Node, Node>(a, null);
+ a = a.Next;
+ } else {
+ yield return new Tuple<Node, Node>(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 {
+ 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, Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Lo))));
+ } else {
+ // produce a (possibly empty) conjunction of inequalities
+ if (Lo != null) {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLe(Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Lo)), ide));
+ }
+ if (Hi != null) {
+ var ide = new IdentifierExpr(Token.NoToken, V);
+ e = Expr.And(e, BplLt(ide, Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Hi))));
+ }
+ }
+ return e;
+ }
+ }
+ }
+
+ 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, then we're overconstrained
+ if (lo != null && hi != null && hi <= lo) {
+ return bottom;
+ }
+ n = new Node(x.V, lo, hi);
+ }
+ if (head == null) {
+ head = n;
+ } else {
+ prev.Next = n;
+ }
+ prev = n;
+ }
+ return new E(head);
+ }
+ }
+
+ public override Element Join(Element a, Element b) {
+ if (a is E_Bottom) {
+ return b;
+ } else if (b is E_Bottom) {
+ return a;
+ } else {
+ var aa = (E)a;
+ var bb = (E)b;
+ // for each variable, take the weaker of the constraints
+ Node head = null;
+ Node prev = null;
+ foreach (var t in Node.Merge(aa.N, bb.N)) {
+ if (t.Item1 != null && t.Item2 != null) {
+ var lo = Node.Min(t.Item1.Lo, t.Item2.Lo, false);
+ var hi = Node.Max(t.Item1.Hi, t.Item2.Hi, false);
+ if (lo != null || hi != null) {
+ var n = new Node(t.Item1.V, lo, hi);
+ if (head == null) {
+ head = n;
+ } else {
+ prev.Next = n;
+ }
+ prev = n;
+ }
+ }
+ }
+ return new E(head);
+ }
+ }
+
+ public override Element Widen(Element a, Element b) {
+ if (a is E_Bottom) {
+ return b; // since this is done just once, we maintain the ascending chains property
+ } else if (b is E_Bottom) {
+ return a;
+ } else {
+ var aa = (E)a;
+ var bb = (E)b;
+ // return a subset of the constraints of aa, namely those that are implied by bb
+ Node head = null;
+ Node prev = null;
+ foreach (var t in Node.Merge(aa.N, bb.N)) {
+ var x = t.Item1;
+ var y = t.Item2;
+ 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.Hi == null || (y.Hi != null && y.Hi <= x.Hi)) {
+ // okay, we keep the upper bound
+ hi = x.Hi;
+ }
+ if (lo != null || hi != null) {
+ var n = new Node(x.V, lo, hi);
+ if (head == null) {
+ head = n;
+ } else {
+ prev.Next = n;
+ }
+ prev = n;
+ }
+ }
+ }
+ return new E(head);
+ }
+ }
+
+ 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);
+ }
+ }
+
+ /// <summary>
+ /// Returns an Element that corresponds to the constraints implied by "expr" in the
+ /// state "state".
+ /// Return "null" to indicate no constraints.
+ /// </summary>
+ E_Common Constraint(Expr expr, Node state) {
+ Variable v;
+ if (IsVariable(expr, out v)) {
+ var n = new Node(v, new BigInteger(1), 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, new BigInteger(1));
+ 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 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)Meet(c, new E(n));
+ }
+ }
+ return c;
+ }
+ case BinaryOperator.Opcode.Neq: {
+ E 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)Meet(c, cc);
+ }
+ }
+ return c;
+ }
+ case BinaryOperator.Opcode.Le: {
+ E 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)Meet(c, new E(n));
+ }
+ }
+ return c;
+ }
+ case BinaryOperator.Opcode.Lt: {
+ E 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 + 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, hi - 1);
+ c = c == null ? new E(n) : (E)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 (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 : StandardVisitor
+ {
+ public BigInteger? Lo;
+ public BigInteger? Hi;
+
+ readonly BigInteger one = new BigInteger(1);
+
+ Node N;
+ public PEVisitor(Node n) {
+ N = n;
+ }
+
+ // Override visitors for all expressions that can return a boolean or integer result
+
+ public override Expr VisitExpr(Expr node) {
+ Lo = Hi = null;
+ return base.VisitExpr(node);
+ }
+ public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ if (node.Val is BigNum) {
+ var n = ((BigNum)node.Val).ToBigInteger;
+ Lo = n;
+ Hi = n + 1;
+ } 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.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.Length == 1);
+ 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.Length == 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;
+ 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 && hi0 <= lo1) {
+ Lo = null; Hi = one;
+ } else if (lo0 != null && hi1 != null && hi1 <= lo0) {
+ Lo = null; Hi = one;
+ } else if (lo0 != null && hi0 != null && lo1 != null && hi1 != null &&
+ lo0 + 1 == hi0 && lo0 == lo1 && lo1 + 1 == hi1) {
+ Lo = one; Hi = null;
+ }
+ if (op.Op == BinaryOperator.Opcode.Neq) {
+ var tmp = Lo; Lo = Hi; Hi = tmp;
+ }
+ 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;
+ }
+ 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;
+ }
+ break;
+ case BinaryOperator.Opcode.Add:
+ if (lo0 != null && lo1 != null) {
+ Lo = lo0 + lo1;
+ }
+ if (hi0 != null && hi1 != null) {
+ Hi = hi0 + hi1 - 1;
+ }
+ break;
+ case BinaryOperator.Opcode.Sub:
+ if (lo0 != null && hi1 != null) {
+ Lo = 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 : (hi0 - 1) * (hi1 - 1) + 1;
+ } else if ((BigInteger)lo0 < 0 && (BigInteger)lo1 < 0) {
+ Lo = null; // approximation
+ Hi = 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);
+ Hi = lo0 - 1;
+ }
+ 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);
+ Hi = lo1;
+ }
+ break;
+ default:
+ break;
+ }
+ } else if (node.Fun is IfThenElse) {
+ var op = (IfThenElse)node.Fun;
+ Contract.Assert(node.Args.Length == 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);
+ }
+ }
+ 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 BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {
+ // don't recurse on subexpression
+ return node;
+ }
+ public override BvExtractExpr 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;
+ }
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ 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;
+ }
+ }
+
+ /// <summary>
+ /// Return a resolved/type-checked expression that represents a EQUALS b.
+ /// Requires a and b to be resolved and type checked already.
+ /// </summary>
+ public static Expr BplEq(Expr a, Expr b) {
+ var e = Expr.Eq(a, b);
+ e.Type = Type.Bool;
+ return e;
+ }
+
+ /// <summary>
+ /// Return a resolved/type-checked expression that represents a LESS-EQUAL b.
+ /// Requires a and b to be resolved and type checked already.
+ /// </summary>
+ public static Expr BplLe(Expr a, Expr b) {
+ var e = Expr.Le(a, b);
+ e.Type = Type.Bool;
+ return e;
+ }
+ /// <summary>
+ /// Return a resolved/type-checked expression that represents a LESS b.
+ /// Requires a and b to be resolved and type checked already.
+ /// </summary>
+ public static Expr BplLt(Expr a, Expr b) {
+ var e = Expr.Lt(a, b);
+ e.Type = Type.Bool;
+ return e;
+ }
+ }
+
+}
diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs
new file mode 100644
index 00000000..7b236481
--- /dev/null
+++ b/Source/AbsInt/NativeLattice.cs
@@ -0,0 +1,320 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.Text;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+using IMutableSet = Microsoft.Boogie.Set;
+using ISet = Microsoft.Boogie.Set;
+using HashSet = Microsoft.Boogie.Set;
+using ArraySet = Microsoft.Boogie.Set;
+
+namespace Microsoft.Boogie.AbstractInterpretation
+{
+ /// <summary>
+ /// Specifies the operations (e.g., join) on a mathematical lattice that depend
+ /// only on the elements of the lattice.
+ /// </summary>
+ public abstract class NativeLattice
+ {
+ /// <summary>
+ /// An element of the lattice. This class should be derived from in any
+ /// implementation of MathematicalLattice.
+ /// </summary>
+ public abstract class Element
+ {
+ public abstract Expr ToExpr();
+ }
+
+ public abstract Element Top { get; }
+ public abstract Element Bottom { get; }
+
+ public abstract bool IsTop(Element element);
+ public abstract bool IsBottom(Element element);
+
+ /// <summary>
+ /// Is 'a' better (or equal) information than 'b'? That is, is 'a' below 'b' in the lattice?
+ /// </summary>
+ public abstract bool Below(Element a, Element b);
+
+ public abstract Element Meet(Element a, Element b);
+ public abstract Element Join(Element a, Element b);
+ public abstract Element Widen(Element a, Element b);
+
+ public abstract Element Constrain(Element element, Expr expr);
+ 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);
+
+ public virtual void Validate() {
+ Contract.Assert(IsTop(Top));
+ Contract.Assert(IsBottom(Bottom));
+ Contract.Assert(!IsBottom(Top));
+ Contract.Assert(!IsTop(Bottom));
+
+ Contract.Assert(Below(Top, Top));
+ Contract.Assert(Below(Bottom, Top));
+ Contract.Assert(Below(Bottom, Bottom));
+
+ Contract.Assert(IsTop(Join(Top, Top)));
+ Contract.Assert(IsBottom(Join(Bottom, Bottom)));
+ }
+ }
+
+ public class NativeAbstractInterpretation
+ {
+ public static void RunAbstractInterpretation(Program program) {
+ Contract.Requires(program != null);
+
+ if (!CommandLineOptions.Clo.UseAbstractInterpretation) {
+ return;
+ }
+ Helpers.ExtraTraceInformation("Starting abstract interpretation");
+
+ DateTime start = new DateTime(); // to please compiler's definite assignment rules
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine();
+ Console.WriteLine("Running abstract interpretation...");
+ start = DateTime.Now;
+ }
+
+ WidenPoints.Compute(program);
+
+ NativeLattice lattice = null;
+ if (CommandLineOptions.Clo.Ai.J_Trivial) {
+ lattice = new TrivialDomain();
+ } else if (CommandLineOptions.Clo.Ai.J_Intervals) {
+ lattice = new NativeIntervallDomain();
+ }
+
+ if (lattice != null) {
+ Dictionary<Procedure, Implementation[]> procedureImplementations = AbstractionEngine.ComputeProcImplMap(program);
+ ComputeProgramInvariants(program, procedureImplementations, lattice);
+ if (CommandLineOptions.Clo.Ai.DebugStatistics) {
+ Console.Error.WriteLine(lattice);
+ }
+ }
+
+ if (CommandLineOptions.Clo.Trace) {
+ DateTime end = DateTime.Now;
+ TimeSpan elapsed = end - start;
+ Console.WriteLine(" [{0} s]", elapsed.TotalSeconds);
+ Console.Out.Flush();
+ }
+ }
+
+ /// <summary>
+ /// Compute and apply the invariants for the program using the underlying abstract domain (using native Boogie
+ /// expressions, not the abstracted AI.Expr's).
+ /// </summary>
+ public static void ComputeProgramInvariants(Program program, Dictionary<Procedure, Implementation[]> procedureImplementations, NativeLattice lattice) {
+ Contract.Requires(program != null);
+ Contract.Requires(procedureImplementations != null);
+ Contract.Requires(lattice != null);
+
+ // Gather all the axioms to create the initial lattice element
+ // Differently stated, it is the \alpha from axioms (i.e. first order formulae) to the underlyng abstract domain
+ var initialElement = lattice.Top;
+ Contract.Assert(initialElement != null);
+ foreach (var decl in program.TopLevelDeclarations) {
+ var ax = decl as Axiom;
+ if (ax != null) {
+ initialElement = lattice.Constrain(initialElement, ax.Expr);
+ }
+ }
+
+ // analyze each procedure
+ foreach (var decl in program.TopLevelDeclarations) {
+ var proc = decl as Procedure;
+ if (proc != null && procedureImplementations.ContainsKey(proc)) {
+ // analyze each implementation of the procedure
+ foreach (var impl in procedureImplementations[proc]) {
+ // add the precondition to the axioms
+ Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
+ var start = initialElement;
+ foreach (Requires pre in proc.Requires) {
+ Expr e = Substituter.Apply(formalProcImplSubst, pre.Condition);
+ start = lattice.Constrain(start, e);
+ }
+ Analyze(impl, lattice, start);
+ }
+ }
+ }
+ }
+
+ public static void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.Element start) {
+ // We need to keep track of some information for each(some) block(s). To do that efficiently,
+ // we number the implementation's blocks sequentially, and then we can use arrays to store
+ // the additional information.
+ var pre = new NativeLattice.Element[impl.Blocks.Count]; // set to null if we never compute a join/widen at this block
+ var post = CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere ? new NativeLattice.Element[impl.Blocks.Count] : null;
+ var iterations = new int[impl.Blocks.Count];
+ var bottom = lattice.Bottom;
+ int n = 0;
+ foreach (var block in impl.Blocks) {
+ block.aiId = n;
+ // Note: The forward analysis below will store lattice elements in pre[n] if pre[n] is non-null.
+ // Thus, the assignment "pre[n] = bottom;" below must be done under the following condition:
+ // n == 0 || block.widenBlock
+ // One possible strategy would be to do it only under that condition. Alternatively,
+ // one could do the assignment under the following condition:
+ // n == 0 || block.widenBlock || block.Predecessors.Length != 1
+ // (which would require first setting the Predecessors field). In any case, if
+ // CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere
+ // then all pre[n] should be set.
+ pre[n] = bottom;
+ n++;
+ }
+ Contract.Assert(n == impl.Blocks.Count);
+
+ var workItems = new Queue<Tuple<Block, NativeLattice.Element>>();
+ workItems.Enqueue(new Tuple<Block, NativeLattice.Element>(impl.Blocks[0], start));
+ //ComputeBlockInvariantsNative(impl, );
+ // compute a fixpoint here
+ while (workItems.Count > 0) {
+ var workItem = workItems.Dequeue();
+ var b = workItem.Item1;
+ var id = b.aiId;
+ var e = workItem.Item2;
+ if (pre[id] == null) {
+ // no pre information stored here, so just go ahead through the block
+ } else if (lattice.Below(e, pre[id])) {
+ // no change
+ continue;
+ } else if (b.widenBlock && CommandLineOptions.Clo.StepsBeforeWidening <= iterations[id]) {
+ e = lattice.Widen(pre[id], e);
+ pre[id] = e;
+ iterations[id]++;
+ } else {
+ e = lattice.Join(pre[id], e);
+ pre[id] = e;
+ iterations[id]++;
+ }
+
+ // propagate'e' through b.Cmds
+ foreach (Cmd cmd in b.Cmds) {
+ e = Step(lattice, cmd, e);
+ }
+
+ if (post != null && pre[id] != null) {
+ post[id] = e;
+ }
+
+ var g = b.TransferCmd as GotoCmd;
+ if (g != null) { // if g==null, it's a pity we didn't pay attention to that earlier, because then we could have skipped analyzing the code in this block
+ foreach (Block succ in g.labelTargets) {
+ workItems.Enqueue(new Tuple<Block, NativeLattice.Element>(succ, e));
+ }
+ }
+ }
+
+ Instrument(impl, pre, post);
+ }
+
+ static void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.Element[] post) {
+ Contract.Requires(impl != null);
+ Contract.Requires(pre != null);
+
+ foreach (var b in impl.Blocks) {
+ var element = pre[b.aiId];
+ if (element != null && (b.widenBlock || CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere)) {
+ CmdSeq newCommands = new CmdSeq();
+ Expr inv = element.ToExpr();
+ PredicateCmd cmd;
+ var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
+ if (CommandLineOptions.Clo.InstrumentWithAsserts) {
+ cmd = new AssertCmd(Token.NoToken, inv, kv);
+ } else {
+ cmd = new AssumeCmd(Token.NoToken, inv, kv);
+ }
+ newCommands.Add(cmd);
+ newCommands.AddRange(b.Cmds);
+ if (post != null && post[b.aiId] != null) {
+ inv = post[b.aiId].ToExpr();
+ kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
+ if (CommandLineOptions.Clo.InstrumentWithAsserts) {
+ cmd = new AssertCmd(Token.NoToken, inv, kv);
+ } else {
+ cmd = new AssumeCmd(Token.NoToken, inv, kv);
+ }
+ newCommands.Add(cmd);
+ }
+ b.Cmds = newCommands; // destructively replace the commands of the block
+ }
+ }
+ }
+
+ /// <summary>
+ /// The abstract transition relation.
+ /// 'cmd' is allowed to be a StateCmd.
+ /// </summary>
+ static NativeLattice.Element Step(NativeLattice lattice, Cmd cmd, NativeLattice.Element elmt) {
+ Contract.Requires(lattice != null);
+ Contract.Requires(cmd != null);
+ Contract.Requires(elmt != null);
+ Contract.Ensures(Contract.Result<NativeLattice.Element>() != null);
+
+ if (cmd is AssignCmd) { // parallel assignment
+ var c = (AssignCmd)cmd;
+ elmt = lattice.Update(elmt, c.AsSimpleAssignCmd);
+ } else if (cmd is HavocCmd) {
+ var c = (HavocCmd)cmd;
+ foreach (IdentifierExpr id in c.Vars) {
+ Contract.Assert(id != null);
+ elmt = lattice.Eliminate(elmt, id.Decl);
+ }
+ } else if (cmd is PredicateCmd) {
+ var c = (PredicateCmd)cmd;
+ var conjuncts = new List<Expr>();
+ foreach (var ee in Conjuncts(c.Expr)) {
+ Contract.Assert(ee != null);
+ elmt = lattice.Constrain(elmt, ee);
+ }
+ } else if (cmd is StateCmd) {
+ var c = (StateCmd)cmd;
+ // Iterate the abstract transition on all the commands in the desugaring of the call
+ foreach (Cmd callDesug in c.Cmds) {
+ Contract.Assert(callDesug != null);
+ elmt = Step(lattice, callDesug, elmt);
+ }
+ // Project out the local variables of the StateCmd
+ foreach (Variable local in c.Locals) {
+ Contract.Assert(local != null);
+ elmt = lattice.Eliminate(elmt, local);
+ }
+ } else if (cmd is SugaredCmd) {
+ var c = (SugaredCmd)cmd;
+ elmt = Step(lattice, c.Desugaring, elmt);
+ } else if (cmd is CommentCmd) {
+ // skip
+ } else {
+ Contract.Assert(false); // unknown command
+ }
+ return elmt;
+ }
+
+ /// <summary>
+ /// Yields the conjuncts of 'expr'.
+ /// </summary>
+ public static IEnumerable<Expr> Conjuncts(Expr expr) {
+ Contract.Requires(expr != null);
+
+ var e = expr as NAryExpr;
+ if (e != null && e.Fun.FunctionName == "&&") { // if it is a conjunction
+ foreach (Expr ee in e.Args) {
+ Contract.Assert(ee != null);
+ foreach (var c in Conjuncts(ee)) {
+ yield return c;
+ }
+ }
+ } else {
+ yield return expr;
+ }
+ }
+
+ }
+}
diff --git a/Source/AbsInt/TrivialDomain.cs b/Source/AbsInt/TrivialDomain.cs
new file mode 100644
index 00000000..f9298e11
--- /dev/null
+++ b/Source/AbsInt/TrivialDomain.cs
@@ -0,0 +1,79 @@
+using System;
+using System.Numerics;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie.AbstractInterpretation
+{
+ class TrivialDomain : NativeLattice
+ {
+ class E : NativeLattice.Element
+ {
+ public readonly bool IsTop;
+ public E(bool isTop) {
+ IsTop = isTop;
+ }
+
+ public override Expr ToExpr() {
+ return Expr.Literal(IsTop);
+ }
+ }
+
+ private E top = new E(true);
+ private E bottom = new E(false);
+
+ public override Element Top { get { return top; } }
+ public override Element Bottom { get { return bottom; } }
+
+ public override bool IsTop(Element element) {
+ var e = (E)element;
+ return e.IsTop;
+ }
+ public override bool IsBottom(Element element) {
+ var e = (E)element;
+ return !e.IsTop;
+ }
+
+ public override bool Below(Element a, Element b) {
+ return IsBottom(a) || IsTop(b);
+ }
+
+ public override Element Meet(Element a, Element b) {
+ if (IsBottom(b)) {
+ return b;
+ } else {
+ return a;
+ }
+ }
+
+ public override Element Join(Element a, Element b) {
+ if (IsTop(b)) {
+ return b;
+ } else {
+ return a;
+ }
+ }
+
+ public override Element Widen(Element a, Element b) {
+ return Join(a, b); // it's a finite domain, after all
+ }
+
+ public override Element Constrain(Element element, Expr expr) {
+ var e = (E)element;
+ var lit = expr as LiteralExpr;
+ if (lit != null && lit.isBool && !(bool)lit.Val) {
+ return bottom;
+ } else {
+ return e;
+ }
+ }
+
+ public override Element Update(Element element, AssignCmd cmd) {
+ return element;
+ }
+
+ public override Element Eliminate(Element element, Variable v) {
+ return element;
+ }
+ }
+}
diff --git a/Source/Basetypes/BigNum.cs b/Source/Basetypes/BigNum.cs
index 73840482..ff676bc6 100644
--- a/Source/Basetypes/BigNum.cs
+++ b/Source/Basetypes/BigNum.cs
@@ -75,6 +75,12 @@ namespace Microsoft.Basetypes {
}
}
+ public BIM ToBigInteger {
+ get {
+ return val;
+ }
+ }
+
// Convert to int; assert that no overflows occur
public int ToIntSafe {
get {
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index ed61b709..aa132c5d 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -163,8 +163,7 @@ namespace Microsoft.Boogie {
return;
}
- oc = EliminateDeadVariablesAndInline(program);
- //BoogiePL.Errors.count = 0;
+ EliminateDeadVariablesAndInline(program);
int errorCount, verified, inconclusives, timeOuts, outOfMemories;
oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
@@ -363,7 +362,7 @@ namespace Microsoft.Boogie {
return PipelineOutcome.ResolvedAndTypeChecked;
}
- static PipelineOutcome EliminateDeadVariablesAndInline(Program program) {
+ static void EliminateDeadVariablesAndInline(Program program) {
Contract.Requires(program != null);
// Eliminate dead variables
Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
@@ -379,33 +378,31 @@ namespace Microsoft.Boogie {
}
// Inline
- // In Spec#, there was no run-time test. The type was just List<Declaration!>
- List<Declaration> TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);
-
+ var TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);
if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {
bool inline = false;
- foreach (Declaration d in TopLevelDeclarations) {
+ foreach (var d in TopLevelDeclarations) {
if (d.FindExprAttribute("inline") != null) {
inline = true;
}
}
if (inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) {
- foreach (Declaration d in TopLevelDeclarations) {
- Implementation impl = d as Implementation;
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
if (impl != null) {
impl.OriginalBlocks = impl.Blocks;
impl.OriginalLocVars = impl.LocVars;
}
}
- foreach (Declaration d in TopLevelDeclarations) {
- Implementation impl = d as Implementation;
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
if (impl != null && !impl.SkipVerification) {
Inliner.ProcessImplementation(program, impl);
}
}
- foreach (Declaration d in TopLevelDeclarations) {
- Implementation impl = d as Implementation;
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
if (impl != null) {
impl.OriginalBlocks = null;
impl.OriginalLocVars = null;
@@ -413,7 +410,6 @@ namespace Microsoft.Boogie {
}
}
}
- return PipelineOutcome.Done;
}
/// <summary>
@@ -434,7 +430,11 @@ namespace Microsoft.Boogie {
// ---------- Infer invariants --------------------------------------------------------
// Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
- Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
+ if (CommandLineOptions.Clo.Ai.J_Intervals || CommandLineOptions.Clo.Ai.J_Trivial) {
+ Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+ } else {
+ Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
+ }
if (CommandLineOptions.Clo.ContractInfer) {
Houdini.Houdini houdini = new Houdini.Houdini(program, true);
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 0aaf3c46..402905a3 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2745,13 +2745,15 @@ namespace Microsoft.Boogie {
CmdSeq newCommands = new CmdSeq();
if (instrumentEntry) {
Expr inv = (Expr)b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/
- PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
+ var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
+ PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv, kv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv, kv);
newCommands.Add(cmd);
}
newCommands.AddRange(b.Cmds);
if (instrumentExit) {
Expr inv = (Expr)b.Lattice.ToPredicate(b.PostInvariant);
- PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
+ var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
+ PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv, kv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv, kv);
newCommands.Add(cmd);
}
b.Cmds = newCommands;
@@ -3537,12 +3539,6 @@ namespace Microsoft.Boogie {
d.Emit(stream, 0);
}
}
- public void InstrumentWithInvariants() {
- foreach (Declaration/*!*/ d in this) {
- Contract.Assert(d != null);
- d.InstrumentWithInvariants();
- }
- }
}
#endregion
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 676ffd5a..06eb3ae5 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -800,6 +800,7 @@ namespace Microsoft.Boogie {
}; // used by WidenPoints.Compute
public VisitState TraversingStatus;
+ public int aiId; // block ID used by the abstract interpreter, which may change these numbers with each AI run
public bool widenBlock;
public int iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 9a0fe64e..fe5f0621 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -438,6 +438,7 @@ namespace Microsoft.Boogie {
: base(tok) {
Contract.Requires(tok != null);
Val = b;
+ Type = Type.Bool;
}
/// <summary>
/// Creates a literal expression for the integer value "v".
@@ -448,6 +449,7 @@ namespace Microsoft.Boogie {
: base(tok) {
Contract.Requires(tok != null);
Val = v;
+ Type = Type.Int;
}
/// <summary>
@@ -456,7 +458,9 @@ namespace Microsoft.Boogie {
public LiteralExpr(IToken/*!*/ tok, BigNum v, int b)
: base(tok) {
Contract.Requires(tok != null);
+ Contract.Requires(0 <= b);
Val = new BvConst(v, b);
+ Type = Type.GetBvType(b);
}
[Pure]
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 2f02f0e5..9413cf30 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -604,6 +604,8 @@ namespace Microsoft.Boogie {
public bool DynamicType = false;
public bool Nullness = false;
public bool Polyhedra = false;
+ public bool J_Trivial = false;
+ public bool J_Intervals = false;
public bool DebugStatistics = false;
public bool AnySet {
@@ -612,7 +614,9 @@ namespace Microsoft.Boogie {
|| Constant
|| DynamicType
|| Nullness
- || Polyhedra;
+ || Polyhedra
+ || J_Trivial
+ || J_Intervals;
}
}
}
@@ -645,6 +649,14 @@ namespace Microsoft.Boogie {
Ai.Polyhedra = true;
UseAbstractInterpretation = true;
break;
+ case 't':
+ Ai.J_Trivial = true;
+ UseAbstractInterpretation = true;
+ break;
+ case 'j':
+ Ai.J_Intervals = true;
+ UseAbstractInterpretation = true;
+ break;
case 's':
Ai.DebugStatistics = true;
UseAbstractInterpretation = true;
@@ -1458,6 +1470,11 @@ namespace Microsoft.Boogie {
d = dynamic type
n = nullness
p = polyhedra for linear inequalities
+ t = trivial bottom/top lattice (cannot be combined with
+ other domains)
+ j = stronger intervals (cannot be combined with other
+ domains)
+ or the following (which denote options, not domains):
s = debug statistics
0..9 = number of iterations before applying a widen (default=0)
/noinfer turn off the default inference, and overrides the /infer
@@ -1473,7 +1490,8 @@ namespace Microsoft.Boogie {
h - instrument inferred invariants only at beginning of
loop headers (default)
e - instrument inferred invariants at beginning and end
- of every block
+ of every block (this mode is intended for use in
+ debugging of abstract domains)
/printInstrumented
print Boogie program after it has been instrumented with
invariants
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 80e24356..648fd84f 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -378,11 +378,11 @@ namespace Microsoft.Dafny
/// </summary>
static PipelineOutcome BoogiePipelineWithRerun (Bpl.Program/*!*/ program, string/*!*/ bplFileName,
out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)
- {Contract.Requires(program != null);
- Contract.Requires(bplFileName != null);
+ {
+ Contract.Requires(program != null);
+ Contract.Requires(bplFileName != null);
Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
-
errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
PipelineOutcome oc = ResolveAndTypecheck(program, bplFileName);
switch (oc) {
@@ -407,6 +407,7 @@ namespace Microsoft.Dafny
return oc;
case PipelineOutcome.ResolvedAndTypeChecked:
+ EliminateDeadVariablesAndInline(program);
return InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
default:
@@ -414,6 +415,55 @@ namespace Microsoft.Dafny
}
}
+ static void EliminateDeadVariablesAndInline(Bpl.Program program) {
+ Contract.Requires(program != null);
+ // Eliminate dead variables
+ Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+
+ // Collect mod sets
+ if (CommandLineOptions.Clo.DoModSetAnalysis) {
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
+ }
+
+ // Coalesce blocks
+ if (CommandLineOptions.Clo.CoalesceBlocks) {
+ Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+ }
+
+ // Inline
+ var TopLevelDeclarations = program.TopLevelDeclarations;
+
+ if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {
+ bool inline = false;
+ foreach (var d in TopLevelDeclarations) {
+ if (d.FindExprAttribute("inline") != null) {
+ inline = true;
+ }
+ }
+ if (inline && CommandLineOptions.Clo.LazyInlining == 0 && CommandLineOptions.Clo.StratifiedInlining == 0) {
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ }
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
+ if (impl != null && !impl.SkipVerification) {
+ Inliner.ProcessImplementation(program, impl);
+ }
+ }
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+ }
+ }
+ }
+ }
enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }
enum ExitValue { VERIFIED = 0, PREPROCESSING_ERROR, DAFNY_ERROR, NOT_VERIFIED }
@@ -477,7 +527,11 @@ namespace Microsoft.Dafny
// ---------- Infer invariants --------------------------------------------------------
// Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
- Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
+ if (CommandLineOptions.Clo.Ai.J_Intervals || CommandLineOptions.Clo.Ai.J_Trivial) {
+ Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+ } else {
+ Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
+ }
if (CommandLineOptions.Clo.LoopUnrollCount != -1) {
program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index 58750460..e517aa18 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -18,34 +18,34 @@ implementation Join(b: bool)
var z: int;
start:
- assume true;
+ assume {:inferred} true;
GlobalFlag := true;
x := 3;
y := 4;
z := x + y;
- assume x == 3 && y == 4 && z == 7;
+ assume {:inferred} x == 3 && y == 4 && z == 7;
goto Then, Else;
Then:
- assume x == 3 && y == 4 && z == 7;
+ assume {:inferred} x == 3 && y == 4 && z == 7;
assume b <==> true;
x := x + 1;
- assume x == 4 && y == 4 && z == 7;
+ assume {:inferred} x == 4 && y == 4 && z == 7;
goto join;
Else:
- assume x == 3 && y == 4 && z == 7;
+ assume {:inferred} x == 3 && y == 4 && z == 7;
assume b <==> false;
y := 4;
- assume x == 3 && y == 4 && z == 7;
+ assume {:inferred} x == 3 && y == 4 && z == 7;
goto join;
join:
- assume y == 4 && z == 7;
+ assume {:inferred} y == 4 && z == 7;
assert y == 4;
assert z == 7;
assert GlobalFlag <==> true;
- assume y == 4 && z == 7;
+ assume {:inferred} y == 4 && z == 7;
return;
}
@@ -61,27 +61,27 @@ implementation Loop()
var i: int;
start:
- assume true;
+ assume {:inferred} true;
c := 0;
i := 0;
- assume c == 0 && i == 0;
+ assume {:inferred} c == 0 && i == 0;
goto test;
test: // cut point
- assume c == 0;
- assume c == 0;
+ assume {:inferred} c == 0;
+ assume {:inferred} c == 0;
goto Then, Else;
Then:
- assume c == 0;
+ assume {:inferred} c == 0;
assume i < 10;
i := i + 1;
- assume c == 0;
+ assume {:inferred} c == 0;
goto test;
Else:
- assume c == 0;
- assume c == 0;
+ assume {:inferred} c == 0;
+ assume {:inferred} c == 0;
return;
}
@@ -96,16 +96,18 @@ implementation Evaluate()
var i: int;
start:
- assume true;
+ assume {:inferred} true;
i := 5;
i := 3 * i + 1;
i := 3 * (i + 1);
i := 1 + 3 * i;
i := (i + 1) * 3;
- assume i == 465;
+ assume {:inferred} i == 465;
return;
}
Boogie program verifier finished with 0 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
new file mode 100644
index 00000000..49d27b1c
--- /dev/null
+++ b/Test/aitest0/Intervals.bpl
@@ -0,0 +1,19 @@
+const N: int;
+axiom 0 <= N;
+
+procedure P(K: int)
+ requires 0 <= K;
+{
+ var b: bool, x, k: int;
+
+ if (!b) {
+ b := !b;
+ }
+ x := if b then 13 else 10;
+ k := K;
+ while (k != 0) {
+ x := x + k;
+ k := k - 1;
+ }
+ assert 13 <= x;
+}
diff --git a/Test/aitest0/runtest.bat b/Test/aitest0/runtest.bat
index a4c12d8d..1cb7a60c 100644
--- a/Test/aitest0/runtest.bat
+++ b/Test/aitest0/runtest.bat
@@ -4,3 +4,4 @@ setlocal
set BGEXE=..\..\Binaries\Boogie.exe
%BGEXE% %* -infer:c -instrumentInfer:e -printInstrumented -noVerify constants.bpl
+%BGEXE% %* -infer:j Intervals.bpl
diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index ca9ff22a..718e7171 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -8,27 +8,27 @@ implementation SimpleLoop()
var i: int;
start:
- assume true;
+ assume {:inferred} true;
i := 0;
- assume i == 0;
+ assume {:inferred} i == 0;
goto test;
test: // cut point
- assume 0 <= i;
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
+ assume {:inferred} 0 <= i;
goto Then, Else;
Then:
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
assume i < 10;
i := i + 1;
- assume i <= 10 && 1 <= i;
+ assume {:inferred} i <= 10 && 1 <= i;
goto test;
Else:
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
assume !(i < 10);
- assume 10 <= i;
+ assume {:inferred} 10 <= i;
return;
}
@@ -43,27 +43,27 @@ implementation VariableBoundLoop(n: int)
var i: int;
start:
- assume true;
+ assume {:inferred} true;
i := 0;
- assume i == 0;
+ assume {:inferred} i == 0;
goto test;
test: // cut point
- assume 0 <= i;
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
+ assume {:inferred} 0 <= i;
goto Then, Else;
Then:
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
assume i < n;
i := i + 1;
- assume i <= n && 1 <= i;
+ assume {:inferred} i <= n && 1 <= i;
goto test;
Else:
- assume 0 <= i;
+ assume {:inferred} 0 <= i;
assume !(i < n);
- assume n <= i && 0 <= i;
+ assume {:inferred} n <= i && 0 <= i;
return;
}
@@ -78,12 +78,12 @@ implementation Foo()
var i: int;
start:
- assume true;
+ assume {:inferred} true;
i := 3 * i + 1;
i := 3 * (i + 1);
i := 1 + 3 * i;
i := (i + 1) * 3;
- assume true;
+ assume {:inferred} true;
return;
}
@@ -98,13 +98,13 @@ implementation FooToo()
var i: int;
start:
- assume true;
+ assume {:inferred} true;
i := 5;
i := 3 * i + 1;
i := 3 * (i + 1);
i := 1 + 3 * i;
i := (i + 1) * 3;
- assume 1 / 3 * i == 155;
+ assume {:inferred} 1 / 3 * i == 155;
return;
}
@@ -119,13 +119,13 @@ implementation FooTooStepByStep()
var i: int;
L0:
- assume true;
+ assume {:inferred} true;
i := 5;
i := 3 * i + 1;
i := 3 * (i + 1);
i := 1 + 3 * i;
i := (i + 1) * 3;
- assume 1 / 3 * i == 155;
+ assume {:inferred} 1 / 3 * i == 155;
return;
}
@@ -145,8 +145,8 @@ implementation p()
{
start:
- assume true;
- assume true;
+ assume {:inferred} true;
+ assume {:inferred} true;
return;
}
@@ -166,9 +166,9 @@ implementation p()
{
start:
- assume true;
+ assume {:inferred} true;
assume x * x == y;
- assume true;
+ assume {:inferred} true;
return;
}
@@ -188,9 +188,9 @@ implementation p()
{
start:
- assume true;
- assume x == 8;
+ assume {:inferred} true;
assume x == 8;
+ assume {:inferred} x == 8;
return;
}
@@ -210,9 +210,9 @@ implementation p()
{
start:
- assume true;
+ assume {:inferred} true;
assume x < y;
- assume x + 1 <= y;
+ assume {:inferred} x + 1 <= y;
return;
}
@@ -233,20 +233,20 @@ implementation p()
{
A:
- assume true;
+ assume {:inferred} true;
assume x < y;
- assume x + 1 <= y;
+ assume {:inferred} x + 1 <= y;
goto B, C;
B:
- assume x + 1 <= y;
+ assume {:inferred} x + 1 <= y;
x := x * x;
- assume true;
+ assume {:inferred} true;
return;
C:
- assume x + 1 <= y;
- assume x + 1 <= y;
+ assume {:inferred} x + 1 <= y;
+ assume {:inferred} x + 1 <= y;
return;
}
@@ -267,32 +267,32 @@ implementation p()
{
A:
- assume true;
+ assume {:inferred} true;
assume 0 - 1 <= x;
- assume -1 <= x;
+ assume {:inferred} -1 <= x;
goto B, E;
B:
- assume -1 <= x;
+ assume {:inferred} -1 <= x;
assume x < y;
- assume x + 1 <= y && -1 <= x;
+ assume {:inferred} x + 1 <= y && -1 <= x;
goto C, E;
C:
- assume x + 1 <= y && -1 <= x;
+ assume {:inferred} x + 1 <= y && -1 <= x;
x := x * x;
- assume 0 <= y;
+ assume {:inferred} 0 <= y;
goto D, E;
D:
- assume 0 <= y;
+ assume {:inferred} 0 <= y;
x := y;
- assume x == y && 0 <= y;
+ assume {:inferred} x == y && 0 <= y;
return;
E:
- assume true;
- assume true;
+ assume {:inferred} true;
+ assume {:inferred} true;
return;
}
@@ -315,26 +315,26 @@ implementation p()
{
A:
- assume true;
+ assume {:inferred} true;
x := 8;
- assume x == 8;
+ assume {:inferred} x == 8;
goto B, C;
B:
- assume x == 8;
+ assume {:inferred} x == 8;
x := 9;
- assume x == 9;
+ assume {:inferred} x == 9;
goto D;
C:
- assume x == 8;
+ assume {:inferred} x == 8;
x := 10;
- assume x == 10;
+ assume {:inferred} x == 10;
goto D;
D:
- assume 9 <= x && x <= 10;
- assume 9 <= x && x <= 10;
+ assume {:inferred} 9 <= x && x <= 10;
+ assume {:inferred} 9 <= x && x <= 10;
return;
}
@@ -356,25 +356,25 @@ implementation p()
{
A:
- assume true;
- assume true;
+ assume {:inferred} true;
+ assume {:inferred} true;
goto B, C;
B:
- assume true;
- assume x <= 0;
+ assume {:inferred} true;
assume x <= 0;
+ assume {:inferred} x <= 0;
goto D;
C:
- assume true;
- assume y <= 0;
+ assume {:inferred} true;
assume y <= 0;
+ assume {:inferred} y <= 0;
goto D;
D:
- assume true;
- assume true;
+ assume {:inferred} true;
+ assume {:inferred} true;
return;
}
@@ -393,7 +393,7 @@ implementation foo()
var n: int;
A:
- assume true;
+ assume {:inferred} true;
n := 0;
j := 0;
i := j + 1;
@@ -402,7 +402,7 @@ implementation foo()
i := i + 1;
i := i + 1;
j := j + 1;
- assume i == j + 4 && j == 1 && n == 0;
+ assume {:inferred} i == j + 4 && j == 1 && n == 0;
return;
}
@@ -421,24 +421,24 @@ implementation foo()
var n: int;
entry:
- assume true;
+ assume {:inferred} true;
assume n >= 4;
i := 0;
j := i + 1;
- assume j == i + 1 && i == 0 && 4 <= n;
+ assume {:inferred} j == i + 1 && i == 0 && 4 <= n;
goto exit, loop0;
loop0: // cut point
- assume 4 <= n && 0 <= i && j == i + 1;
+ assume {:inferred} 4 <= n && 0 <= i && j == i + 1;
assume j <= n;
i := i + 1;
j := j + 1;
- assume j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;
+ assume {:inferred} j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;
goto loop0, exit;
exit:
- assume j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
- assume j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
+ assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
+ assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
return;
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 15cec24f..aab1990d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -307,7 +307,6 @@ Execution trace:
(0,0): anon0
Definedness.dfy(105,15): Error: possible division by zero
Execution trace:
- (0,0): anon0
Definedness.dfy(105,5): anon8_LoopHead
(0,0): anon8_LoopBody
Definedness.dfy(105,5): anon9_Else
@@ -799,13 +798,11 @@ Execution trace:
ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon71_Then
ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
@@ -821,20 +818,17 @@ Execution trace:
ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon71_Then
ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
ControlStructures.dfy(210,9): anon73_Else
(0,0): anon20
ControlStructures.dfy(210,9): anon74_Else
- (0,0): anon22
(0,0): anon75_Then
(0,0): after_4
ControlStructures.dfy(221,7): anon77_LoopHead
@@ -842,7 +836,6 @@ Execution trace:
ControlStructures.dfy(221,7): anon78_Else
(0,0): anon33
ControlStructures.dfy(221,7): anon79_Else
- (0,0): anon35
(0,0): anon81_Then
(0,0): anon38
(0,0): after_9
@@ -856,13 +849,11 @@ Execution trace:
ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon68_Then
(0,0): after_5
(0,0): anon87_Then
@@ -876,20 +867,17 @@ Execution trace:
ControlStructures.dfy(194,3): anon63_Else
(0,0): anon3
ControlStructures.dfy(194,3): anon64_Else
- (0,0): anon5
ControlStructures.dfy(198,5): anon65_LoopHead
(0,0): anon65_LoopBody
ControlStructures.dfy(198,5): anon66_Else
(0,0): anon8
ControlStructures.dfy(198,5): anon67_Else
- (0,0): anon10
(0,0): anon71_Then
ControlStructures.dfy(210,9): anon72_LoopHead
(0,0): anon72_LoopBody
ControlStructures.dfy(210,9): anon73_Else
(0,0): anon20
ControlStructures.dfy(210,9): anon74_Else
- (0,0): anon22
(0,0): anon75_Then
(0,0): after_4
ControlStructures.dfy(221,7): anon77_LoopHead
@@ -897,7 +885,6 @@ Execution trace:
ControlStructures.dfy(221,7): anon78_Else
(0,0): anon33
ControlStructures.dfy(221,7): anon79_Else
- (0,0): anon35
(0,0): anon82_Then
(0,0): anon85_Then
(0,0): after_8
@@ -915,7 +902,6 @@ Execution trace:
Termination.dfy(105,3): anon8_Else
(0,0): anon3
Termination.dfy(105,3): anon9_Else
- (0,0): anon5
Termination.dfy(113,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
@@ -925,7 +911,6 @@ Execution trace:
(0,0): anon11_Then
(0,0): anon5
Termination.dfy(113,3): anon12_Else
- (0,0): anon7
Termination.dfy(122,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
@@ -935,7 +920,6 @@ Execution trace:
(0,0): anon11_Then
(0,0): anon5
Termination.dfy(122,3): anon12_Else
- (0,0): anon7
Termination.dfy(123,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
(0,0): anon0
@@ -945,7 +929,6 @@ Execution trace:
(0,0): anon11_Then
(0,0): anon5
Termination.dfy(122,3): anon12_Else
- (0,0): anon7
Termination.dfy(251,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon6_Else
@@ -959,7 +942,6 @@ Execution trace:
Termination.dfy(291,3): anon11_Else
Termination.dfy(291,3): anon12_Else
(0,0): anon13_Else
- (0,0): anon8
Dafny program verifier finished with 45 verified, 6 errors
@@ -1131,7 +1113,6 @@ Execution trace:
TypeParameters.dfy(153,3): anon22_Else
(0,0): anon13
TypeParameters.dfy(153,3): anon24_Else
- (0,0): anon15
Dafny program verifier finished with 35 verified, 5 errors
@@ -1224,7 +1205,6 @@ Execution trace:
LoopModifies.dfy(14,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(14,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1233,7 +1213,6 @@ Execution trace:
LoopModifies.dfy(42,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(42,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1242,7 +1221,6 @@ Execution trace:
LoopModifies.dfy(57,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(57,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause
Execution trace:
(0,0): anon0
@@ -1254,7 +1232,6 @@ Execution trace:
LoopModifies.dfy(90,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(90,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(146,11): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1263,13 +1240,11 @@ Execution trace:
LoopModifies.dfy(134,4): anon18_Else
(0,0): anon5
LoopModifies.dfy(134,4): anon20_Else
- (0,0): anon7
LoopModifies.dfy(139,7): anon21_LoopHead
(0,0): anon21_LoopBody
LoopModifies.dfy(139,7): anon22_Else
(0,0): anon12
LoopModifies.dfy(139,7): anon24_Else
- (0,0): anon14
LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1278,7 +1253,6 @@ Execution trace:
LoopModifies.dfy(193,4): anon10_Else
(0,0): anon5
LoopModifies.dfy(193,4): anon12_Else
- (0,0): anon7
LoopModifies.dfy(285,13): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -1287,13 +1261,11 @@ Execution trace:
LoopModifies.dfy(273,4): anon18_Else
(0,0): anon5
LoopModifies.dfy(273,4): anon20_Else
- (0,0): anon7
LoopModifies.dfy(281,7): anon21_LoopHead
(0,0): anon21_LoopBody
LoopModifies.dfy(281,7): anon22_Else
(0,0): anon12
LoopModifies.dfy(281,7): anon24_Else
- (0,0): anon14
Dafny program verifier finished with 23 verified, 9 errors
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 22:07:30 +0000