diff options
Diffstat (limited to 'Source/VCExpr/BigLiteralAbstracter.cs')
-rw-r--r-- | Source/VCExpr/BigLiteralAbstracter.cs | 462 |
1 files changed, 231 insertions, 231 deletions
diff --git a/Source/VCExpr/BigLiteralAbstracter.cs b/Source/VCExpr/BigLiteralAbstracter.cs index 879ab6d6..39064fb7 100644 --- a/Source/VCExpr/BigLiteralAbstracter.cs +++ b/Source/VCExpr/BigLiteralAbstracter.cs @@ -1,232 +1,232 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Text;
-using System.IO;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.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) {
- Contract.Requires(gen != null);
- DummyVar = gen.Variable("x", Type.Int);
- IncAxioms = new List<VCExpr>();
- Literals = new List<KeyValuePair<BigNum, VCExprVar>>();
- }
-
- private BigLiteralAbstracter(BigLiteralAbstracter abstracter)
- : base(abstracter.Gen) {
- Contract.Requires(abstracter != null);
- DummyVar = abstracter.DummyVar;
- IncAxioms = new List<VCExpr>(abstracter.IncAxioms);
- Literals = new List<KeyValuePair<BigNum, VCExprVar>>(abstracter.Literals);
- }
-
- public Object Clone() {
- Contract.Ensures(Contract.Result<Object>() != null);
-
- 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) {
- Contract.Requires(expr != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- return Mutate(expr, true);
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- // list in which axioms are incrementally collected
- private readonly List<VCExpr/*!*/>/*!*/ IncAxioms;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(cce.NonNullElements(IncAxioms));
- }
-
- private void AddAxiom(VCExpr/*!*/ axiom) {
- Contract.Requires(axiom != null);
- IncAxioms.Add(axiom);
- }
-
- // Return all axioms that were added since the last time NewAxioms
- // was called
- public VCExpr GetNewAxioms() {
- Contract.Ensures(Contract.Result<VCExpr>() != null);
- 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;
-
- [ContractInvariantMethod]
- void ObjectInvariat() {
- Contract.Invariant(Literals != null);
- Contract.Invariant(Contract.ForAll(Literals, i => i.Value != null));
- }
-
-
- private class EntryComparerC : IComparer<KeyValuePair<BigNum, VCExprVar/*!*/>> {
- public int Compare(KeyValuePair<BigNum, VCExprVar/*!*/> a,
- KeyValuePair<BigNum, VCExprVar/*!*/> b) {
- //Contract.Requires(a.Value!=null);
- //Contract.Requires(b.Value!=null);
- 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;
- [ContractInvariantMethod]
- void ObjectInvarint() {
- Contract.Invariant(DummyVar != null);
- }
-
-
- ////////////////////////////////////////////////////////////////////////////
-
- // Construct an expression to represent the given (large) integer
- // literal. Constants are defined and axiomatised if necessary
- private VCExpr Represent(BigNum lit) {
- Contract.Requires((NegConstantDistance > lit || lit > ConstantDistance));
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- if (lit.IsNegative)
- return Gen.Function(VCExpressionGenerator.SubIOp,
- Gen.Integer(BigNum.ZERO), RepresentPos(lit.Neg));
- else
- return RepresentPos(lit);
- }
-
- private VCExpr RepresentPos(BigNum lit) {
- Contract.Requires((lit > ConstantDistance));
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- 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.AddIOp,
- 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.SubIOp,
- 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) {
- Contract.Requires((lit > ConstantDistance));
- Contract.Ensures(Contract.Result<VCExpr>() != null);
-
- VCExprVar res = Gen.Variable("int#" + lit, Type.Int);
- int index = GetIndexFor(lit);
- Contract.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) {
- Contract.Requires(aValue < bValue);
- Contract.Requires(aExpr != null);
- Contract.Requires(bExpr != null);
-
- BigNum dist = bValue - aValue;
- VCExpr distExpr = Gen.Function(VCExpressionGenerator.SubIOp, 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) {
- Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
- VCExprIntLit intLit = node as VCExprIntLit;
- if (intLit != null) {
- if (NegConstantDistance > intLit.Val || intLit.Val > ConstantDistance)
- return Represent(intLit.Val);
- }
- return node;
- }
-
- }
-
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Text; +using System.IO; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics.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) { + Contract.Requires(gen != null); + DummyVar = gen.Variable("x", Type.Int); + IncAxioms = new List<VCExpr>(); + Literals = new List<KeyValuePair<BigNum, VCExprVar>>(); + } + + private BigLiteralAbstracter(BigLiteralAbstracter abstracter) + : base(abstracter.Gen) { + Contract.Requires(abstracter != null); + DummyVar = abstracter.DummyVar; + IncAxioms = new List<VCExpr>(abstracter.IncAxioms); + Literals = new List<KeyValuePair<BigNum, VCExprVar>>(abstracter.Literals); + } + + public Object Clone() { + Contract.Ensures(Contract.Result<Object>() != null); + + 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) { + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result<VCExpr>() != null); + + return Mutate(expr, true); + } + + //////////////////////////////////////////////////////////////////////////// + + // list in which axioms are incrementally collected + private readonly List<VCExpr/*!*/>/*!*/ IncAxioms; + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(IncAxioms)); + } + + private void AddAxiom(VCExpr/*!*/ axiom) { + Contract.Requires(axiom != null); + IncAxioms.Add(axiom); + } + + // Return all axioms that were added since the last time NewAxioms + // was called + public VCExpr GetNewAxioms() { + Contract.Ensures(Contract.Result<VCExpr>() != null); + 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; + + [ContractInvariantMethod] + void ObjectInvariat() { + Contract.Invariant(Literals != null); + Contract.Invariant(Contract.ForAll(Literals, i => i.Value != null)); + } + + + private class EntryComparerC : IComparer<KeyValuePair<BigNum, VCExprVar/*!*/>> { + public int Compare(KeyValuePair<BigNum, VCExprVar/*!*/> a, + KeyValuePair<BigNum, VCExprVar/*!*/> b) { + //Contract.Requires(a.Value!=null); + //Contract.Requires(b.Value!=null); + 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; + [ContractInvariantMethod] + void ObjectInvarint() { + Contract.Invariant(DummyVar != null); + } + + + //////////////////////////////////////////////////////////////////////////// + + // Construct an expression to represent the given (large) integer + // literal. Constants are defined and axiomatised if necessary + private VCExpr Represent(BigNum lit) { + Contract.Requires((NegConstantDistance > lit || lit > ConstantDistance)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + + if (lit.IsNegative) + return Gen.Function(VCExpressionGenerator.SubIOp, + Gen.Integer(BigNum.ZERO), RepresentPos(lit.Neg)); + else + return RepresentPos(lit); + } + + private VCExpr RepresentPos(BigNum lit) { + Contract.Requires((lit > ConstantDistance)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + + 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.AddIOp, + 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.SubIOp, + 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) { + Contract.Requires((lit > ConstantDistance)); + Contract.Ensures(Contract.Result<VCExpr>() != null); + + VCExprVar res = Gen.Variable("int#" + lit, Type.Int); + int index = GetIndexFor(lit); + Contract.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) { + Contract.Requires(aValue < bValue); + Contract.Requires(aExpr != null); + Contract.Requires(bExpr != null); + + BigNum dist = bValue - aValue; + VCExpr distExpr = Gen.Function(VCExpressionGenerator.SubIOp, 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) { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result<VCExpr>() != null); + 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 |