diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-05 23:07:06 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-05 23:07:06 -0800 |
| commit | 95bb8b3b4454fdc1a14fd67b22a5ac6183135cfd (patch) | |
| tree | 014162d0766bdec9922ea6d314ac05bc2d9a065e /Source/AbsInt | |
| parent | 9e18c32b3fda7b377f095e8ee865424c51af1e73 (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 (limited to 'Source/AbsInt')
| -rw-r--r-- | Source/AbsInt/AbsInt.csproj | 4 | ||||
| -rw-r--r-- | Source/AbsInt/AbstractInterpretation.cs | 10 | ||||
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 861 | ||||
| -rw-r--r-- | Source/AbsInt/NativeLattice.cs | 320 | ||||
| -rw-r--r-- | Source/AbsInt/TrivialDomain.cs | 79 |
5 files changed, 1268 insertions, 6 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;
+ }
+ }
+}
|