From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/VCExpr/BigLiteralAbstracter.cs | 462 +++++++++++++++++----------------- 1 file changed, 231 insertions(+), 231 deletions(-) (limited to 'Source/VCExpr/BigLiteralAbstracter.cs') 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, ICloneable { - - public BigLiteralAbstracter(VCExpressionGenerator gen) - : base(gen) { - Contract.Requires(gen != null); - DummyVar = gen.Variable("x", Type.Int); - IncAxioms = new List(); - Literals = new List>(); - } - - private BigLiteralAbstracter(BigLiteralAbstracter abstracter) - : base(abstracter.Gen) { - Contract.Requires(abstracter != null); - DummyVar = abstracter.DummyVar; - IncAxioms = new List(abstracter.IncAxioms); - Literals = new List>(abstracter.Literals); - } - - public Object Clone() { - Contract.Ensures(Contract.Result() != 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() != null); - - return Mutate(expr, true); - } - - //////////////////////////////////////////////////////////////////////////// - - // list in which axioms are incrementally collected - private readonly List/*!*/ 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() != 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>/*!*/ Literals; - - [ContractInvariantMethod] - void ObjectInvariat() { - Contract.Invariant(Literals != null); - Contract.Invariant(Contract.ForAll(Literals, i => i.Value != null)); - } - - - private class EntryComparerC : IComparer> { - public int Compare(KeyValuePair a, - KeyValuePair 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() != 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() != 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() != null); - - VCExprVar res = Gen.Variable("int#" + lit, Type.Int); - int index = GetIndexFor(lit); - Contract.Assert(index < 0); - index = ~index; - - Literals.Insert(index, new KeyValuePair(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 - (lit, DummyVar), - EntryComparer); - } - - //////////////////////////////////////////////////////////////////////////// - - public override VCExpr Visit(VCExprLiteral node, bool arg) { - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != 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, ICloneable { + + public BigLiteralAbstracter(VCExpressionGenerator gen) + : base(gen) { + Contract.Requires(gen != null); + DummyVar = gen.Variable("x", Type.Int); + IncAxioms = new List(); + Literals = new List>(); + } + + private BigLiteralAbstracter(BigLiteralAbstracter abstracter) + : base(abstracter.Gen) { + Contract.Requires(abstracter != null); + DummyVar = abstracter.DummyVar; + IncAxioms = new List(abstracter.IncAxioms); + Literals = new List>(abstracter.Literals); + } + + public Object Clone() { + Contract.Ensures(Contract.Result() != 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() != null); + + return Mutate(expr, true); + } + + //////////////////////////////////////////////////////////////////////////// + + // list in which axioms are incrementally collected + private readonly List/*!*/ 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() != 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>/*!*/ Literals; + + [ContractInvariantMethod] + void ObjectInvariat() { + Contract.Invariant(Literals != null); + Contract.Invariant(Contract.ForAll(Literals, i => i.Value != null)); + } + + + private class EntryComparerC : IComparer> { + public int Compare(KeyValuePair a, + KeyValuePair 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() != 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() != 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() != null); + + VCExprVar res = Gen.Variable("int#" + lit, Type.Int); + int index = GetIndexFor(lit); + Contract.Assert(index < 0); + index = ~index; + + Literals.Insert(index, new KeyValuePair(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 + (lit, DummyVar), + EntryComparer); + } + + //////////////////////////////////////////////////////////////////////////// + + public override VCExpr Visit(VCExprLiteral node, bool arg) { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != 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 -- cgit v1.2.3