зеркало из https://github.com/microsoft/mcBV.git
402 строки
16 KiB
Forth
402 строки
16 KiB
Forth
module Interval
|
|
|
|
open BitVector
|
|
open System.Numerics
|
|
open Microsoft.Z3
|
|
open Util
|
|
|
|
// Interval [lower,upper)
|
|
// CMW: I.e., lower is included, but upper is not.
|
|
// However, when constructing a new Interval, we always
|
|
// provide an _inclusive_ upper bound. From the outside,
|
|
// we don't care how Intervals are saved internally, but
|
|
// we always want to provide an inclusive upper bound,
|
|
// because it's easier to think inclusive.
|
|
type Interval private (l:BitVector, u:BitVector, fr:bool) =
|
|
do assert(l.Length = u.Length)
|
|
do assert(l.isConcreteValue)
|
|
do assert(u.isConcreteValue)
|
|
|
|
// CMW: The following are private; this is the internal state of
|
|
// the Interval object, they are never leaked outside of this class.
|
|
member private this.dimension = l.Length
|
|
member private this.lower = l
|
|
member private this.upper = u
|
|
|
|
static member Empty (dim:int) = Interval(BitVector.AllOne dim, BitVector.AllOne dim, false)
|
|
static member Full (dim:int) = Interval(BitVector.AllZero dim, BitVector.AllOne dim, true)
|
|
|
|
// This is the constructor for the user; upper is inclusive.
|
|
new(lower:BitVector, upper:BitVector) =
|
|
assert (upper.Length = lower.Length)
|
|
let dim = lower.Length
|
|
let upper_plus_one = (BitVector.bvAdd upper (BitVector.One upper.Length))
|
|
let l, u, f =
|
|
if BitVector.bvEQ lower upper_plus_one then
|
|
BitVector.AllZero dim, BitVector.AllOne dim, true // full
|
|
elif BitVector.bvULT upper lower then
|
|
upper, (BitVector.bvAdd lower (BitVector.One dim)), false // normalized
|
|
else
|
|
lower, upper_plus_one, false
|
|
Interval(l, u, f)
|
|
|
|
// This is the constructor for one-sided intervals, i.e., [bound, +oo] if
|
|
// is_lower = true and [-oo, bound] otherwise.
|
|
new(bound:BitVector, is_lower:bool) =
|
|
if is_lower then
|
|
Interval(bound, BitVector.AllOne bound.Length)
|
|
else
|
|
Interval(BitVector.AllZero bound.Length, bound)
|
|
|
|
// CMW: What is the definition of "full" and "range" here?
|
|
// Is "upperIsIncluded" a better description, or does it mean something else?
|
|
member private this.fullRange = fr
|
|
|
|
// CMW: The following three are functions to access the dimension, the lowest and
|
|
// the uppermost element of the interval. The user thinks in inclusive upper
|
|
// bounds and doesn't care what the internal representation is like.
|
|
// So, we need to translate from exclusive to inclusive in this.Upper.
|
|
member this.Dimension = this.dimension
|
|
|
|
member this.Lower = assert(not this.isEmpty)
|
|
this.lower
|
|
|
|
member this.Upper = if this.isFull then
|
|
BitVector.AllOne this.dimension
|
|
else
|
|
assert(not this.isEmpty)
|
|
BitVector.bvSub this.upper (BitVector.One this.dimension)
|
|
|
|
member this.isEmpty = (not this.fullRange && BitVector.bvEQ this.lower this.upper)
|
|
|
|
member this.isFull = (this.fullRange) // AZ: This or case causes problems on length one intervals. Singleton [0,0] is represented as [0,1] and not full, but it meets the conditions of the or case of the test.
|
|
//|| ((BitVector.isAllZero this.lower) && (BitVector.isAllOnes this.upper))
|
|
|
|
member this.containsZero = (BitVector.isAllZero this.lower)
|
|
|
|
// CMW: I haven't checked/tested any of the functions below after changing
|
|
// the interface of the Interval class.
|
|
|
|
member this.Complement() = //AZ: this might still be buggy
|
|
if this.isFull then
|
|
Interval.Empty(this.dimension)
|
|
elif this.isEmpty then
|
|
Interval.Full(this.dimension)
|
|
else
|
|
Interval(this.upper, BitVector.bvSub this.Lower (BitVector.One this.Dimension)) //AZ: Note the small upper!
|
|
|
|
|
|
override this.ToString() =
|
|
if this.isEmpty then
|
|
"]["
|
|
else
|
|
"[" + (this.Lower.ToString()) + ", " + (this.Upper.ToString()) + "]"
|
|
|
|
member this.estimateSearchSpace() = if this.isFull then this.Dimension
|
|
elif this.isEmpty then 0
|
|
else
|
|
let diff = BitVector.bvSub this.Upper this.Lower
|
|
diff.Length - diff.LeadingZeros
|
|
|
|
member this.AddConstantShift (b:BitVector) =
|
|
Interval(BitVector.bvAdd this.lower b, BitVector.bvAdd this.upper b,this.fullRange)
|
|
|
|
member this.SubstractConstantShift (b:BitVector) =
|
|
Interval(BitVector.bvSub this.lower b, BitVector.bvSub this.upper b,this.fullRange)
|
|
|
|
member this.isEqual (other:Interval) =
|
|
this.dimension = other.dimension &&
|
|
this.fullRange = other.fullRange &&
|
|
BitVector.bvEQ this.upper other.upper &&
|
|
BitVector.bvEQ this.lower this.lower
|
|
|
|
static member iULEQ (lhs:Interval) (rhs:Interval) =
|
|
// lhs <= rhs can only cut off one side of the interval
|
|
// rhs cuts off lhs.upper
|
|
// lhs cuts off rhs.lower
|
|
let nLhsBounds = if BitVector.bvUGT lhs.upper rhs.upper then
|
|
Interval(lhs.lower,rhs.upper,false)
|
|
else
|
|
lhs
|
|
let nRhsBounds = if BitVector.bvUGT lhs.lower rhs.lower then
|
|
Interval(lhs.lower,rhs.upper,false)
|
|
else
|
|
rhs
|
|
|
|
(nLhsBounds,nRhsBounds)
|
|
|
|
// static member iEQ (a:Interval) (b:Interval) =
|
|
// if BitVector.bvULEQ a.upper b.lower then Val.True
|
|
// elif BitVector.bvULEQ b.upper a.lower then Val.False
|
|
// else Val.U
|
|
//
|
|
// static member iULEQ (a:Interval) (b:Interval) =
|
|
// BitVector.bvEQ (a.getSingletonElement()) (b.getSingletonElement())
|
|
|
|
member this.Normalize () =
|
|
this.SubstractConstantShift this.lower
|
|
|
|
member this.isSupersetRotational (sub:Interval) =
|
|
if this.fullRange then
|
|
true
|
|
elif sub.fullRange then
|
|
false
|
|
elif sub.isEmpty then
|
|
true
|
|
else
|
|
//Normalize the intervals
|
|
let nThis = this.Normalize()
|
|
let nSub = sub.SubstractConstantShift this.lower
|
|
|
|
BitVector.bvULEQ nThis.lower nSub.lower &&
|
|
BitVector.bvULEQ nSub.lower nSub.upper &&
|
|
BitVector.bvULEQ nSub.upper this.upper
|
|
|
|
member this.isSuperset (sub:Interval) =
|
|
not this.isEmpty &&
|
|
BitVector.bvULEQ this.Lower sub.Lower &&
|
|
BitVector.bvULEQ sub.Upper this.Upper
|
|
|
|
|
|
member this.isSubset(sup:Interval) =
|
|
sup.isSuperset(this)
|
|
|
|
|
|
member this.isSingleton =
|
|
if this.isEmpty then //Necessarry check due to assertions in this.Lower and this.Upper
|
|
false
|
|
elif (BitVector.bvEQ this.Lower this.Upper) then
|
|
true
|
|
else
|
|
false
|
|
|
|
|
|
member this.Singleton =
|
|
if this.isSingleton then
|
|
this.lower
|
|
else
|
|
BitVector.Invalid
|
|
|
|
|
|
// CMW: The following functions are highly inefficient and only needed when
|
|
// rotational BVs are used.
|
|
// member this.Size() =
|
|
// if this.fullRange then
|
|
// BitVector.AllOne(this.dimension).toBigInt()
|
|
// else
|
|
// let norm = this.Normalize()
|
|
// let sz = (BitVector.bvSub norm.upper norm.lower)
|
|
// sz.toBigInt()
|
|
//
|
|
// member this.RotationalUnion (i:Interval) =
|
|
// let isFullRange = this.isSuperset (i.Complement())
|
|
//
|
|
// if isFullRange then
|
|
// Interval(this.lower,this.lower,isFullRange)
|
|
// else
|
|
// let (lMin,lMax) = if BitVector.bvULEQ this.lower i.lower then
|
|
// (this.lower,i.lower)
|
|
// else
|
|
// (i.lower, this.lower)
|
|
// let (uMin, uMax) = if BitVector.bvULEQ this.upper i.upper then
|
|
// (i.upper, this.upper)
|
|
// else
|
|
// (this.upper, i.upper)
|
|
//
|
|
// let lowerUpper = Interval(lMin,uMax,false)
|
|
// let upperLower = Interval(uMin,lMax,false)
|
|
//
|
|
// if lowerUpper.Size() < upperLower.Size() then
|
|
// lowerUpper
|
|
// else
|
|
// upperLower
|
|
|
|
member this.Union (other:Interval) =
|
|
let l = BitVector.Min this.Lower other.Lower
|
|
let u = BitVector.Max this.Upper other.Upper
|
|
let res = Interval(l,u)
|
|
assert (res.isSuperset this && res.isSuperset other)
|
|
res
|
|
|
|
member this.Intersection (other:Interval) =
|
|
if this.isEmpty then
|
|
this
|
|
elif other.isEmpty then
|
|
other
|
|
else
|
|
let l = BitVector.Max this.lower other.lower
|
|
let u = BitVector.Min this.Upper other.Upper
|
|
if BitVector.bvULEQ l u then
|
|
let res = Interval (l, u)
|
|
assert (res.isSubset this && res.isSubset other)
|
|
res
|
|
else
|
|
Interval.Empty(this.Dimension)
|
|
|
|
|
|
member this.Contains (value:BitVector) =
|
|
(BitVector.bvULEQ this.Lower value) &&
|
|
(BitVector.bvULEQ value this.Upper)
|
|
|
|
member this.RemoveValue (value:BitVector) =
|
|
if BitVector.bvEQ value this.Lower then
|
|
Interval (BitVector.bvAdd (this.Lower) (BitVector.One this.Dimension),this.Upper)
|
|
elif BitVector.bvEQ value this.Upper then
|
|
Interval (this.Upper, BitVector.bvSub (this.Upper) (BitVector.One this.Dimension))
|
|
else
|
|
this
|
|
|
|
static member Add (a:Interval) (b:Interval) =
|
|
assert (not a.isEmpty)
|
|
assert (not b.isEmpty)
|
|
assert (a.dimension = b.dimension)
|
|
|
|
if a.fullRange then a
|
|
elif b.fullRange then b
|
|
elif a.isSingleton && b.isSingleton then
|
|
let q = (BitVector.bvAdd a.lower b.lower)
|
|
Interval(q, q)
|
|
else
|
|
let n = a.dimension
|
|
let extra_bits = 1
|
|
let big_al = (BitVector.bvConcat (BitVector.AllZero extra_bits) a.Lower)
|
|
let big_au = (BitVector.bvConcat (BitVector.AllZero extra_bits) a.Upper)
|
|
let big_bl = (BitVector.bvConcat (BitVector.AllZero extra_bits) b.Lower)
|
|
let big_bu = (BitVector.bvConcat (BitVector.AllZero extra_bits) b.Upper)
|
|
let big_l = (BitVector.bvAdd big_al big_bl)
|
|
let big_u = (BitVector.bvAdd big_au big_bu)
|
|
let big_l_overflow = not (BitVector.isAllZero (BitVector.bvExtract ((n+extra_bits)-1) n big_l))
|
|
let big_u_overflow = not (BitVector.isAllZero (BitVector.bvExtract ((n+extra_bits)-1) n big_u))
|
|
if not big_l_overflow && not big_u_overflow then
|
|
let l = (BitVector.bvExtract (n-1) 0 big_l)
|
|
let u = (BitVector.bvExtract (n-1) 0 big_u)
|
|
Interval(l, u)
|
|
else
|
|
Interval.Full n
|
|
|
|
static member Sub (a:Interval) (b:Interval) =
|
|
assert (not a.isEmpty)
|
|
assert (not b.isEmpty)
|
|
assert (a.dimension = b.dimension)
|
|
|
|
if a.fullRange then a
|
|
elif b.fullRange then b
|
|
elif a.isSingleton && b.isSingleton then
|
|
let q = (BitVector.bvSub a.lower b.lower)
|
|
Interval(q, q)
|
|
else
|
|
let n = a.dimension
|
|
let extra_bits = 1
|
|
let big_al = (BitVector.bvConcat (BitVector.AllZero extra_bits) a.Lower)
|
|
let big_au = (BitVector.bvConcat (BitVector.AllZero extra_bits) a.Upper)
|
|
let big_bl = (BitVector.bvConcat (BitVector.AllZero extra_bits) b.Lower)
|
|
let big_bu = (BitVector.bvConcat (BitVector.AllZero extra_bits) b.Upper)
|
|
let big_l = (BitVector.bvSub big_al big_bu)
|
|
let big_u = (BitVector.bvSub big_au big_bl)
|
|
let big_l_overflow = not (BitVector.isAllZero (BitVector.bvExtract ((n+extra_bits)-1) n big_l))
|
|
let big_u_overflow = not (BitVector.isAllZero (BitVector.bvExtract ((n+extra_bits)-1) n big_u))
|
|
if not big_l_overflow && not big_u_overflow then
|
|
let l = (BitVector.bvExtract (n-1) 0 big_l)
|
|
let u = (BitVector.bvExtract (n-1) 0 big_u)
|
|
Interval(l, u)
|
|
else
|
|
Interval.Full n
|
|
|
|
static member Mul (a:Interval) (b:Interval) =
|
|
assert (not a.isEmpty)
|
|
assert (not b.isEmpty)
|
|
assert (a.dimension = b.dimension)
|
|
if a.fullRange then a
|
|
elif b.fullRange then b
|
|
elif a.isSingleton && b.isSingleton then
|
|
let q = (BitVector.bvMul a.lower b.lower)
|
|
Interval(q, q)
|
|
else
|
|
let n = a.dimension
|
|
let extra_bits = n
|
|
let big_al = (BitVector.bvConcat (BitVector.AllZero extra_bits) a.Lower)
|
|
let big_au = (BitVector.bvConcat (BitVector.AllZero extra_bits) a.Upper)
|
|
let big_bl = (BitVector.bvConcat (BitVector.AllZero extra_bits) b.Lower)
|
|
let big_bu = (BitVector.bvConcat (BitVector.AllZero extra_bits) b.Upper)
|
|
let big_l = (BitVector.bvMul big_al big_bl)
|
|
let big_u = (BitVector.bvMul big_au big_bu)
|
|
let big_l_overflow = not (BitVector.isAllZero (BitVector.bvExtract ((n+extra_bits)-1) n big_l))
|
|
let big_u_overflow = not (BitVector.isAllZero (BitVector.bvExtract ((n+extra_bits)-1) n big_u))
|
|
if not big_l_overflow && not big_u_overflow then
|
|
let l = (BitVector.bvExtract (n-1) 0 big_l)
|
|
let u = (BitVector.bvExtract (n-1) 0 big_u)
|
|
Interval(l, u)
|
|
else
|
|
Interval.Full n
|
|
|
|
static member UDiv (a:Interval) (b:Interval) =
|
|
assert (not a.isEmpty)
|
|
assert (not b.isEmpty)
|
|
assert (a.dimension = b.dimension)
|
|
if a.fullRange then a
|
|
elif b.fullRange then b
|
|
elif (BitVector.isAllZero b.Upper) ||
|
|
(BitVector.isAllZero b.Lower) then
|
|
Interval.Full a.Dimension
|
|
else
|
|
// l and u can only be smaller than a.Lower and a.Upper,
|
|
// so no overflow detection is necessary.
|
|
let l = (BitVector.bvUDiv a.Lower b.Upper)
|
|
let u = (BitVector.bvUDiv a.Upper b.Lower)
|
|
Interval(l, u)
|
|
|
|
static member SDiv (a:Interval) (b:Interval) =
|
|
assert (not a.isEmpty)
|
|
assert (not b.isEmpty)
|
|
assert (a.dimension = b.dimension)
|
|
if a.fullRange then a
|
|
elif b.fullRange then b
|
|
elif a.isSingleton && b.isSingleton then
|
|
let q = (BitVector.bvSDiv a.lower b.lower)
|
|
Interval(q, q)
|
|
elif (BitVector.isAllZero b.Lower) ||
|
|
(BitVector.isAllZero b.Upper) then
|
|
Interval.Full a.Dimension
|
|
else
|
|
// CMW: The values within the interval are not ordered correctly
|
|
// for signed division (e.g., Upper can be negative while Lower
|
|
// is positive). To get around that, we could just translate
|
|
// everything into an unsigned scale, run an unsigned divison,
|
|
// and then translate the results back. For now, we just give
|
|
// up and throw it away:
|
|
Interval.Full a.Dimension
|
|
|
|
static member Neg (a:Interval) =
|
|
if a.fullRange then
|
|
a
|
|
else
|
|
assert(false)
|
|
// CMW: This is not necessarily the kind of "negation" we want.
|
|
// It transforms [l, u] into [-u, -l], while often we will want [0, l] || [u, 1...1].
|
|
// The latter will of course usually have to be approximated to the full interval
|
|
// (or the exclusive-upper interval with negation, etc).
|
|
let l = BitVector.bvNegate (a.Upper)
|
|
let u = BitVector.bvAdd (BitVector.bvNegate a.lower) (BitVector.One a.dimension)
|
|
Interval (l, u, false)
|
|
|
|
static member Extract (u:int) (l:int) (b:Interval) =
|
|
let nL = BitVector.bvExtract u l (b.Lower)
|
|
let nU = BitVector.bvExtract u l (b.Upper)
|
|
Interval(nL, nU)
|
|
|
|
static member Concat (a:Interval) (b:Interval) =
|
|
let nL = BitVector.bvConcat a.Lower b.Lower
|
|
let nU = BitVector.bvConcat a.Upper b.Upper
|
|
Interval(nL, nU)
|
|
|
|
static member Equal (a:Interval) (b:Interval) =
|
|
assert(a.dimension = b.dimension)
|
|
BitVector.bvEQ a.lower b.lower && BitVector.bvEQ a.upper b.upper
|
|
|
|
static member RLEToInterval (b: BitVector) =
|
|
if not (b.isConcreteValue) then
|
|
let l = b.Minimum
|
|
let u = b.Maximum
|
|
Interval(l, u)
|
|
else
|
|
Interval(b, BitVector.bvAdd b (BitVector.One b.Length), false) |