Boogie: Renaming VCExpr sources in preparation for port commit

1 files changed, 198 insertions, 0 deletions

diff --git a/Source/VCExpr/BigLiteralAbstracter.cs b/Source/VCExpr/BigLiteralAbstracter.cs
new file mode 100644
index 00000000..fac34a8d
--- /dev/null
+++ b/Source/VCExpr/BigLiteralAbstracter.cs
@@ -0,0 +1,198 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+using System;

+using System.Text;

+using System.IO;

+using System.Collections;

+using System.Collections.Generic;

+using Microsoft.Contracts;

+using Microsoft.Basetypes;

+

+// Code for replacing large integer literals in VCExpr with

+// constants. This is necessary for Simplify, which cannot deal with

+// literals larger than 32 bits

+

+namespace Microsoft.Boogie.VCExprAST

+{

+

+  public class BigLiteralAbstracter : MutatingVCExprVisitor<bool>, ICloneable {

+

+    public BigLiteralAbstracter(VCExpressionGenerator! gen) {

+      base(gen);

+      DummyVar = gen.Variable("x", Type.Int);

+      IncAxioms = new List<VCExpr!> ();

+      Literals = new List<KeyValuePair<BigNum, VCExprVar!>> ();

+    }

+

+    private BigLiteralAbstracter(BigLiteralAbstracter! abstracter) {

+      base(abstracter.Gen);

+      DummyVar = abstracter.DummyVar;

+      IncAxioms = new List<VCExpr!> (abstracter.IncAxioms);

+      Literals = new List<KeyValuePair<BigNum, VCExprVar!>> (abstracter.Literals);

+    }

+

+    public Object! Clone() {

+      return new BigLiteralAbstracter(this);

+    }

+

+    private static readonly BigNum ConstantDistance = BigNum.FromLong(100000);

+    private static readonly BigNum NegConstantDistance = BigNum.FromLong(-100000);

+    // distance twice plus one

+    private static readonly BigNum ConstantDistanceTPO = BigNum.FromLong(200001);

+    private static readonly BigNum ConstantDistancePO = BigNum.FromLong(100001);

+

+    public VCExpr! Abstract(VCExpr! expr) {

+      return Mutate(expr, true);

+    }

+

+    ////////////////////////////////////////////////////////////////////////////

+

+    // list in which axioms are incrementally collected

+    private readonly List<VCExpr!>! IncAxioms;

+

+    private void AddAxiom(VCExpr! axiom) {

+      IncAxioms.Add(axiom);

+    }

+

+    // Return all axioms that were added since the last time NewAxioms

+    // was called

+    public VCExpr! GetNewAxioms() {

+      VCExpr! res = Gen.NAry(VCExpressionGenerator.AndOp, IncAxioms);

+      IncAxioms.Clear();

+      return res;

+    }

+

+    ////////////////////////////////////////////////////////////////////////////

+

+    // All named integer literals known to the visitor, in ascending

+    // order. Such literals are always positive, and the distance

+    // between two literals is always more than ConstantDistance.

+    private readonly List<KeyValuePair<BigNum, VCExprVar!>>! Literals;

+    

+    private class EntryComparerC : IComparer<KeyValuePair<BigNum, VCExprVar!>> {

+      public int Compare(KeyValuePair<BigNum, VCExprVar!> a,

+                         KeyValuePair<BigNum, VCExprVar!> b) {

+        return a.Key.CompareTo(b.Key);

+      }

+    }

+

+    private static readonly EntryComparerC EntryComparer = new EntryComparerC ();

+

+    // variable used when searching for entries in the literal list

+    private readonly VCExprVar! DummyVar;

+

+    ////////////////////////////////////////////////////////////////////////////

+    

+    // Construct an expression to represent the given (large) integer

+    // literal. Constants are defined and axiomatised if necessary

+    private VCExpr! Represent(BigNum lit)

+      requires NegConstantDistance > lit || lit > ConstantDistance; {

+

+      if (lit.IsNegative)

+        return Gen.Function(VCExpressionGenerator.SubOp,

+                            Gen.Integer(BigNum.ZERO), RepresentPos(lit.Neg));

+      else

+        return RepresentPos(lit);

+    }

+

+    private VCExpr! RepresentPos(BigNum lit)

+      requires lit > ConstantDistance; {

+      

+      int index = GetIndexFor(lit);

+      if (index >= 0)

+        // precise match

+        return Literals[index].Value;

+      

+      // check whether a constant is defined that is at most

+      // ConstantDistance away from lit

+      index = ~index;

+      VCExpr res = null;

+      BigNum resDistance = ConstantDistancePO;

+

+      if (index > 0) {

+        BigNum dist = lit - Literals[index - 1].Key;

+        if (dist < resDistance) {

+          resDistance = dist;

+          res = Gen.Function(VCExpressionGenerator.AddOp,

+                             Literals[index - 1].Value, Gen.Integer(dist));

+        }

+      }

+

+      if (index < Literals.Count) {

+        BigNum dist = Literals[index].Key - lit;

+        if (dist < resDistance) {

+          resDistance = dist;

+          res = Gen.Function(VCExpressionGenerator.SubOp,

+                             Literals[index].Value, Gen.Integer(dist));

+        }

+      }

+

+      if (res != null)

+        return res;

+

+      // otherwise, define a new constant to represent this literal

+      return AddConstantFor(lit);

+    }

+

+    private VCExpr! AddConstantFor(BigNum lit)

+      requires lit > ConstantDistance; {

+      

+      VCExprVar! res = Gen.Variable("int#" + lit, Type.Int);

+      int index = GetIndexFor(lit);

+      assert index < 0;

+      index = ~index;

+

+      Literals.Insert(index, new KeyValuePair<BigNum, VCExprVar!>(lit, res));

+      

+      // relate the new constant to the predecessor and successor

+      if (index > 0)

+        DefineRelationship(Literals[index - 1].Value, Literals[index - 1].Key,

+                           res, lit);

+      else

+        DefineRelationship(Gen.Integer(BigNum.ZERO), BigNum.ZERO, res, lit);

+        

+      if (index < Literals.Count - 1)

+        DefineRelationship(res, lit,

+                           Literals[index + 1].Value, Literals[index + 1].Key);

+

+      return res;

+    }

+    

+    private void DefineRelationship(VCExpr! aExpr, BigNum aValue,

+                                    VCExpr! bExpr, BigNum bValue)

+      requires aValue < bValue; {

+

+      BigNum dist = bValue - aValue;

+      VCExpr! distExpr = Gen.Function(VCExpressionGenerator.SubOp, bExpr, aExpr);

+      if (dist <= ConstantDistanceTPO)

+        // constants that are sufficiently close to each other are put

+        // into a precise relationship

+        AddAxiom(Gen.Eq(distExpr, Gen.Integer(dist)));

+      else

+        AddAxiom(Gen.Function(VCExpressionGenerator.GtOp,

+                              distExpr, Gen.Integer(ConstantDistanceTPO)));

+    }

+

+    private int GetIndexFor(BigNum lit) {

+      return Literals.BinarySearch(new KeyValuePair<BigNum, VCExprVar!>

+                                                   (lit, DummyVar),

+                                   EntryComparer);

+    }

+

+    ////////////////////////////////////////////////////////////////////////////

+

+    public override VCExpr! Visit(VCExprLiteral! node, bool arg) {

+      VCExprIntLit intLit = node as VCExprIntLit;

+      if (intLit != null) {

+        if (NegConstantDistance > intLit.Val || intLit.Val > ConstantDistance)

+          return Represent(intLit.Val);

+      }

+      return node;

+    }

+

+  }

+

+}
\ No newline at end of file