From 92d9f59f6cdf5b7789d5040ac78cc2f4763d9918 Mon Sep 17 00:00:00 2001 From: Alexander Arthur Date: Wed, 16 Jul 2025 10:39:03 +1000 Subject: [PATCH 1/7] Skeleton of generic reduced product --- src/main/scala/analysis/Domains.scala | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/src/main/scala/analysis/Domains.scala b/src/main/scala/analysis/Domains.scala index eb98e0cc86..dccfc4745a 100644 --- a/src/main/scala/analysis/Domains.scala +++ b/src/main/scala/analysis/Domains.scala @@ -9,9 +9,12 @@ trait MustAnalysis /** A domain that performs two analyses in parallel. */ -class ProductDomain[L1, L2](d1: AbstractDomain[L1], d2: AbstractDomain[L2]) extends AbstractDomain[(L1, L2)] { +trait ProductDomain[L1, L2] extends AbstractDomain[(L1, L2)] { def join(a: (L1, L2), b: (L1, L2), pos: Block): (L1, L2) = (d1.join(a._1, b._1, pos), d2.join(a._2, b._2, pos)) + def d1: AbstractDomain[L1] + def d2: AbstractDomain[L2] + override def widen(a: (L1, L2), b: (L1, L2), pos: Block): (L1, L2) = (d1.widen(a._1, b._1, pos), d2.widen(a._2, b._2, pos)) override def narrow(a: (L1, L2), b: (L1, L2)): (L1, L2) = (d1.narrow(a._1, b._1), d2.narrow(a._2, b._2)) @@ -25,11 +28,26 @@ class ProductDomain[L1, L2](d1: AbstractDomain[L1], d2: AbstractDomain[L2]) exte def bot: (L1, L2) = (d1.bot, d2.bot) } +/** A domain that is the reduced product of two other domains. + * */ +trait ReducedProductDomain[L1, L2] extends ProductDomain[L1, L2] { + def reduce(a: L1, b: L2): (L1, L2) +} + +class TNumIntervalReducedProduct extends ReducedProductDomain[Map[Variable, TNum], LatticeMap[Variable, Interval]] { + override val d1 : AbstractDomain[Map[Variable, TNum]] = TNumDomain() + override val d2: AbstractDomain[LatticeMap[Variable, Interval]] = UnsignedIntervalDomain() + + + override def reduce(a: Map[Variable, TNum], b: LatticeMap[Variable, Interval]): (Map[Variable, TNum], LatticeMap[Variable, Interval]) = ??? +} + /** * Encodes the conjunction of two domain predicates. */ -class PredProductDomain[L1, L2](d1: PredicateEncodingDomain[L1], d2: PredicateEncodingDomain[L2]) - extends ProductDomain[L1, L2](d1, d2) +class PredProductDomain[L1, L2](override val d1: PredicateEncodingDomain[L1], + override val d2: PredicateEncodingDomain[L2]) + extends ProductDomain[L1, L2] with PredicateEncodingDomain[(L1, L2)] { def toPred(x: (L1, L2)): Predicate = Predicate.and(d1.toPred(x._1), d2.toPred(x._2)) From 42da6b6765399e86e010241d3efc8c7835972854 Mon Sep 17 00:00:00 2001 From: Alexander Arthur Date: Thu, 24 Jul 2025 14:08:11 +1000 Subject: [PATCH 2/7] Implementation of reduced product between intervals and tnums --- src/main/scala/analysis/Domains.scala | 85 +++++++++++++++++++++++-- src/main/scala/analysis/KnownBits.scala | 4 ++ 2 files changed, 83 insertions(+), 6 deletions(-) diff --git a/src/main/scala/analysis/Domains.scala b/src/main/scala/analysis/Domains.scala index dccfc4745a..e98effcee5 100644 --- a/src/main/scala/analysis/Domains.scala +++ b/src/main/scala/analysis/Domains.scala @@ -1,5 +1,6 @@ package analysis +import analysis.Interval.ConcreteInterval import ir.* import ir.transforms.AbstractDomain import util.assertion.* @@ -31,15 +32,87 @@ trait ProductDomain[L1, L2] extends AbstractDomain[(L1, L2)] { /** A domain that is the reduced product of two other domains. * */ trait ReducedProductDomain[L1, L2] extends ProductDomain[L1, L2] { - def reduce(a: L1, b: L2): (L1, L2) + def reduce(a: (L1, L2)): (L1, L2) + override def transfer(a: (L1, L2), b: Command): (L1, L2) = { + val things = (d1.transfer(a._1, b), d2.transfer(a._2, b)) + reduce(a) + } } -class TNumIntervalReducedProduct extends ReducedProductDomain[Map[Variable, TNum], LatticeMap[Variable, Interval]] { - override val d1 : AbstractDomain[Map[Variable, TNum]] = TNumDomain() - override val d2: AbstractDomain[LatticeMap[Variable, Interval]] = UnsignedIntervalDomain() - +private implicit val intervalTerm: Interval = Interval.Bottom +// private implicit val tnumTerm: TNum = TNum.top(3506) // + +class TNumIntervalReducedProduct extends ReducedProductDomain[LatticeMap[Variable, Interval], + Map[Variable, TNum]] { + override def d1: AbstractDomain[LatticeMap[Variable, Interval]] = UnsignedIntervalDomain() + override def d2 : AbstractDomain[Map[Variable, TNum]] = TNumDomain() + + override def reduce(a: (LatticeMap[Variable, Interval], Map[Variable, TNum])): (LatticeMap[Variable, Interval], Map[Variable, TNum]) = { + def reduceSingle(int: Interval, x: TNum): Option[(Interval, TNum)] = { + def refineLowerBound(a: BigInt, x: TNum): BigInt = { + var newBound = x.maxUnsignedValue().value + for i <- x.width to 0 by -1 + do + newBound = newBound & (~(1 << i)) // Unset the ith bit + if newBound < a then + newBound = newBound | (1 << i) // Re-set the ith bit + newBound + } + def refineUpperBound(a: BigInt, x: TNum): BigInt = { + var newBound = x.minUnsignedValue().value + for i <- x.width to 0 by -1 + do + newBound = newBound | (1 << i) // Set the ith bit + if newBound > a then + newBound = newBound & (~(1 << i)) // Unset the ith bit + newBound + } + def refineTnum(a: BigInt, b: BigInt, x: TNum): Option[TNum] = { + var mask = ~(a ^ b) + var value = x.value.value + var tnumMask = x.mask.value + for i <- x.width to 0 by -1 do + if (mask & (1 << i)) != 0 then + mask = 0 // Because break doesn't exist because actually this for loop is + // a method call! or something + if !(((value & (1 << i)) > 0) || ((value & (1 << i)) == (a & (1 << i)))) then + return None + value = value | (a & (1 << i)) + tnumMask = tnumMask & (~(1 << i)) + + Some(TNum(BitVecLiteral(value, x.width), BitVecLiteral(tnumMask, x.width))) + } + + int match { + case int@ConcreteInterval(lo, hi, width) => + var interval: ConcreteInterval = int + var tnum: Option[TNum] = Some(x) + while + val oldInt = interval + val oldx = tnum + + interval = Interval.ConcreteInterval(refineLowerBound(interval.lower, tnum.get), + refineUpperBound(interval.upper, tnum.get), interval.width) + tnum = refineTnum(interval.lower, interval.upper, tnum.get) + + oldInt == interval && oldx == tnum && tnum.nonEmpty + do () + + tnum match { + case Some(thing) => Some((interval, thing)) + case None => None + } + case Interval.Top => Some((Interval.Top, x)) + case Interval.Bottom => Some((Interval.Bottom, x)) + } + } - override def reduce(a: Map[Variable, TNum], b: LatticeMap[Variable, Interval]): (Map[Variable, TNum], LatticeMap[Variable, Interval]) = ??? + for ((vara, interval) <- a._1.toMap) { + val x: TNum = a._2(vara) + val updated = reduceSingle(interval, x) + } + a + } } /** diff --git a/src/main/scala/analysis/KnownBits.scala b/src/main/scala/analysis/KnownBits.scala index dad7cbce73..3fa131d321 100644 --- a/src/main/scala/analysis/KnownBits.scala +++ b/src/main/scala/analysis/KnownBits.scala @@ -78,6 +78,10 @@ case class TNum(value: BitVecLiteral, mask: BitVecLiteral) { TNum(n, 0.bv(n.size)) } + def maxUnsignedValue(): BitVecLiteral = value | mask + + def minUnsignedValue(): BitVecLiteral = value & (~mask) + override def toString() = { val padwidth = width / 4 + (if width % 4 != 0 then 1 else 0) def padded(number: BigInt) = { From 34d0ccb2ce40e03b85ef9934e211de0b689d1a54 Mon Sep 17 00:00:00 2001 From: Alexander Arthur Date: Fri, 25 Jul 2025 14:36:44 +1000 Subject: [PATCH 3/7] Overly simplistic tests of tnum-interval reduction logic --- .../TNumIntervalReducedProductTest.scala | 42 +++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 src/test/scala/TNumIntervalReducedProductTest.scala diff --git a/src/test/scala/TNumIntervalReducedProductTest.scala b/src/test/scala/TNumIntervalReducedProductTest.scala new file mode 100644 index 0000000000..6923f3c377 --- /dev/null +++ b/src/test/scala/TNumIntervalReducedProductTest.scala @@ -0,0 +1,42 @@ +import analysis.Interval.ConcreteInterval +import analysis.{TNum, TNumIntervalReducedProduct} +import ir.BitVecLiteral +import org.scalatest.funsuite.AnyFunSuiteLike + +class TNumIntervalReducedProductTest extends AnyFunSuiteLike { + + val domain = TNumIntervalReducedProduct() + val interval = ConcreteInterval(6, 10, 4) + val tnum = TNum(BitVecLiteral(0,4), BitVecLiteral(9, 4)) + + test("Refine lower bound - simple example") { + val expected = 8 + assert(expected == domain.refineLowerBound(6, tnum)) + } + + test("Refine lower bound - 0") { + val expected = 0 + assert(expected == domain.refineLowerBound(0, tnum)) + } + + test("Refine upper bound - simple example") { + val expected = 9 + assert(expected == domain.refineUpperBound(10, tnum)) + } + + test("Refine upper bound - 0") { + val expected = 0 + assert(expected == domain.refineUpperBound(0, tnum)) + } + + test("Refine tnum - simple example") { + val expected = TNum(BitVecLiteral(8, 4), BitVecLiteral(1, 4)) + assert(expected == domain.refineTnum(8, 9, tnum)) + } + + test("Refine tnum - 0") { + val expected = TNum(BitVecLiteral(0, 4), BitVecLiteral(0, 4)) + assert(expected == domain.refineTnum(0, 0, tnum)) + } + +} From fe696b85ddadcc2d4aa1f11c5abd1fa2c6da4e52 Mon Sep 17 00:00:00 2001 From: Alexander Arthur Date: Fri, 25 Jul 2025 14:37:58 +1000 Subject: [PATCH 4/7] Fix logic errors + reformat --- src/main/scala/analysis/Domains.scala | 171 +++++++++++++++----------- 1 file changed, 97 insertions(+), 74 deletions(-) diff --git a/src/main/scala/analysis/Domains.scala b/src/main/scala/analysis/Domains.scala index e98effcee5..303d51144d 100644 --- a/src/main/scala/analysis/Domains.scala +++ b/src/main/scala/analysis/Domains.scala @@ -29,98 +29,121 @@ trait ProductDomain[L1, L2] extends AbstractDomain[(L1, L2)] { def bot: (L1, L2) = (d1.bot, d2.bot) } -/** A domain that is the reduced product of two other domains. - * */ -trait ReducedProductDomain[L1, L2] extends ProductDomain[L1, L2] { - def reduce(a: (L1, L2)): (L1, L2) - override def transfer(a: (L1, L2), b: Command): (L1, L2) = { - val things = (d1.transfer(a._1, b), d2.transfer(a._2, b)) - reduce(a) +/** + * A domain that is the reduced product of two other domains. + */ +trait ReducedProductDomain[L1, L2] extends ProductDomain[L1, L2] { + def reduce(a: (L1, L2), c: Command): (L1, L2) + override def transfer(a: (L1, L2), c: Command): (L1, L2) = { + val things = (d1.transfer(a._1, c), d2.transfer(a._2, c)) + // PERFORMANCE: This reduces every variable every transfer. Needless to say that this is + // quite inefficient. + reduce(things, c) } } private implicit val intervalTerm: Interval = Interval.Bottom -// private implicit val tnumTerm: TNum = TNum.top(3506) // -class TNumIntervalReducedProduct extends ReducedProductDomain[LatticeMap[Variable, Interval], - Map[Variable, TNum]] { +/** + * The reduced product between the interval and tnum domains. + */ +class TNumIntervalReducedProduct extends ReducedProductDomain[LatticeMap[Variable, Interval], Map[Variable, TNum]] { override def d1: AbstractDomain[LatticeMap[Variable, Interval]] = UnsignedIntervalDomain() - override def d2 : AbstractDomain[Map[Variable, TNum]] = TNumDomain() - - override def reduce(a: (LatticeMap[Variable, Interval], Map[Variable, TNum])): (LatticeMap[Variable, Interval], Map[Variable, TNum]) = { - def reduceSingle(int: Interval, x: TNum): Option[(Interval, TNum)] = { - def refineLowerBound(a: BigInt, x: TNum): BigInt = { - var newBound = x.maxUnsignedValue().value - for i <- x.width to 0 by -1 - do - newBound = newBound & (~(1 << i)) // Unset the ith bit - if newBound < a then - newBound = newBound | (1 << i) // Re-set the ith bit - newBound - } - def refineUpperBound(a: BigInt, x: TNum): BigInt = { - var newBound = x.minUnsignedValue().value - for i <- x.width to 0 by -1 - do - newBound = newBound | (1 << i) // Set the ith bit - if newBound > a then - newBound = newBound & (~(1 << i)) // Unset the ith bit - newBound - } - def refineTnum(a: BigInt, b: BigInt, x: TNum): Option[TNum] = { - var mask = ~(a ^ b) - var value = x.value.value - var tnumMask = x.mask.value - for i <- x.width to 0 by -1 do - if (mask & (1 << i)) != 0 then - mask = 0 // Because break doesn't exist because actually this for loop is - // a method call! or something - if !(((value & (1 << i)) > 0) || ((value & (1 << i)) == (a & (1 << i)))) then - return None - value = value | (a & (1 << i)) - tnumMask = tnumMask & (~(1 << i)) - - Some(TNum(BitVecLiteral(value, x.width), BitVecLiteral(tnumMask, x.width))) - } + override def d2: AbstractDomain[Map[Variable, TNum]] = TNumDomain() + + override def reduce( + unreduced: (LatticeMap[Variable, Interval], Map[Variable, TNum]), + c: Command + ): (LatticeMap[Variable, Interval], Map[Variable, TNum]) = { + def reduceSingle(int: Interval, x: TNum): (Interval, TNum) = { + int match { - case int@ConcreteInterval(lo, hi, width) => - var interval: ConcreteInterval = int - var tnum: Option[TNum] = Some(x) - while - val oldInt = interval - val oldx = tnum - - interval = Interval.ConcreteInterval(refineLowerBound(interval.lower, tnum.get), - refineUpperBound(interval.upper, tnum.get), interval.width) - tnum = refineTnum(interval.lower, interval.upper, tnum.get) - - oldInt == interval && oldx == tnum && tnum.nonEmpty - do () - - tnum match { - case Some(thing) => Some((interval, thing)) - case None => None - } - case Interval.Top => Some((Interval.Top, x)) - case Interval.Bottom => Some((Interval.Bottom, x)) + case int: ConcreteInterval => + val interval = + Interval.ConcreteInterval(refineLowerBound(int.lower, x), refineUpperBound(int.upper, x), int.width) + val tnum = refineTnum(int.lower, int.upper, x) + (interval, tnum) + case Interval.Top => (Interval.Top, x) + case Interval.Bottom => (Interval.Bottom, x) } } - for ((vara, interval) <- a._1.toMap) { - val x: TNum = a._2(vara) - val updated = reduceSingle(interval, x) + c match { + case c: LocalAssign => + val result = reduceSingle(unreduced._1(c.lhs), unreduced._2(c.lhs)) + (unreduced._1 + (c.lhs -> result._1), unreduced._2 + (c.lhs -> result._2)) + case c: MemoryAssign => + val result = reduceSingle(unreduced._1(c.lhs), unreduced._2(c.lhs)) + (unreduced._1 + (c.lhs -> result._1), unreduced._2 + (c.lhs -> result._2)) + case c: SimulAssign => + val (ints, tnums) = c.assignments + .map((v, e) => v) + .map(v => (v, reduceSingle(unreduced._1(v), unreduced._2(v)))) + .map((v, t) => ((v, t._1), (v, t._2))) + .unzip + (unreduced._1 ++ ints.toMap, unreduced._2 ++ tnums) + case c: Return => + val (ints, tnums) = c.outParams + .map((v, e) => v) + .map(v => (v, reduceSingle(unreduced._1(v), unreduced._2(v)))) + .map((v, t) => ((v, t._1), (v, t._2))) + .unzip + (unreduced._1 ++ ints.toMap, unreduced._2 ++ tnums) + case _ => unreduced } - a + } + + /* These three methods (refine*()) are only exposed publicly so they can be tested, since they + * contain most of the logic for this domain. You probably shouldn't use them. + */ + def refineLowerBound(a: BigInt, x: TNum): BigInt = { + var newBound = x.maxUnsignedValue().value + for i <- x.width to 0 by -1 + do + if 0 != (x.mask.value & (1 << i)) then + newBound = newBound & (~(1 << i)) // Unset the ith bit + if newBound < a then newBound = newBound | (1 << i) // Re-set the ith bit + newBound + } + + def refineUpperBound(a: BigInt, x: TNum): BigInt = { + var newBound = x.minUnsignedValue().value + for i <- x.width to 0 by -1 + do + if 0 != (x.mask.value & (1 << i)) then + newBound = newBound | (1 << i) // Set the ith bit + if newBound > a then newBound = newBound & (~(1 << i)) // Unset the ith bit + newBound + } + + def refineTnum(a: BigInt, b: BigInt, x: TNum): TNum = { + val mask = ~(a ^ b) + var lb = a // An extra copy to obliterate instead of breaking from the loop + var stupidVariable = 1 + var value = x.value.value + var tnumMask = x.mask.value + for i <- x.width - 1 to 0 by -1 do + if (mask & (1 << i)) == 0 then + lb = 0 + stupidVariable = 0 // Because break doesn't exist because actually this for loop is a + // method call! or something. Just do nothing for the rest of the loop instead. + /* if !(((value & (1 << i)) > 0) || ((value & (1 << i)) == (a & (1 << i)))) then + * TODO: go to bottom here because interval and tnum don't overlap */ + value = value | (lb & (1 << i)) + tnumMask = tnumMask & (~(stupidVariable << i)) + + TNum(BitVecLiteral(value, x.width), BitVecLiteral(tnumMask, x.width)) } } /** * Encodes the conjunction of two domain predicates. */ -class PredProductDomain[L1, L2](override val d1: PredicateEncodingDomain[L1], - override val d2: PredicateEncodingDomain[L2]) - extends ProductDomain[L1, L2] +class PredProductDomain[L1, L2]( + override val d1: PredicateEncodingDomain[L1], + override val d2: PredicateEncodingDomain[L2] +) extends ProductDomain[L1, L2] with PredicateEncodingDomain[(L1, L2)] { def toPred(x: (L1, L2)): Predicate = Predicate.and(d1.toPred(x._1), d2.toPred(x._2)) From f2c6dcc46ac708f8c7e202923b204ebdb7983e0f Mon Sep 17 00:00:00 2001 From: Alexander Arthur Date: Fri, 25 Jul 2025 15:11:51 +1000 Subject: [PATCH 5/7] Make CI happy --- src/main/scala/analysis/Domains.scala | 17 ++++++++--------- .../scala/TNumIntervalReducedProductTest.scala | 3 ++- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/main/scala/analysis/Domains.scala b/src/main/scala/analysis/Domains.scala index 303d51144d..1fadd505cd 100644 --- a/src/main/scala/analysis/Domains.scala +++ b/src/main/scala/analysis/Domains.scala @@ -57,7 +57,6 @@ class TNumIntervalReducedProduct extends ReducedProductDomain[LatticeMap[Variabl ): (LatticeMap[Variable, Interval], Map[Variable, TNum]) = { def reduceSingle(int: Interval, x: TNum): (Interval, TNum) = { - int match { case int: ConcreteInterval => val interval = @@ -100,20 +99,20 @@ class TNumIntervalReducedProduct extends ReducedProductDomain[LatticeMap[Variabl def refineLowerBound(a: BigInt, x: TNum): BigInt = { var newBound = x.maxUnsignedValue().value for i <- x.width to 0 by -1 - do - if 0 != (x.mask.value & (1 << i)) then - newBound = newBound & (~(1 << i)) // Unset the ith bit - if newBound < a then newBound = newBound | (1 << i) // Re-set the ith bit + do + if 0 != (x.mask.value & (1 << i)) then + newBound = newBound & (~(1 << i)) // Unset the ith bit + if newBound < a then newBound = newBound | (1 << i) // Re-set the ith bit newBound } def refineUpperBound(a: BigInt, x: TNum): BigInt = { var newBound = x.minUnsignedValue().value for i <- x.width to 0 by -1 - do - if 0 != (x.mask.value & (1 << i)) then - newBound = newBound | (1 << i) // Set the ith bit - if newBound > a then newBound = newBound & (~(1 << i)) // Unset the ith bit + do + if 0 != (x.mask.value & (1 << i)) then + newBound = newBound | (1 << i) // Set the ith bit + if newBound > a then newBound = newBound & (~(1 << i)) // Unset the ith bit newBound } diff --git a/src/test/scala/TNumIntervalReducedProductTest.scala b/src/test/scala/TNumIntervalReducedProductTest.scala index 6923f3c377..06b0e85ecd 100644 --- a/src/test/scala/TNumIntervalReducedProductTest.scala +++ b/src/test/scala/TNumIntervalReducedProductTest.scala @@ -3,11 +3,12 @@ import analysis.{TNum, TNumIntervalReducedProduct} import ir.BitVecLiteral import org.scalatest.funsuite.AnyFunSuiteLike +@test_util.tags.UnitTest class TNumIntervalReducedProductTest extends AnyFunSuiteLike { val domain = TNumIntervalReducedProduct() val interval = ConcreteInterval(6, 10, 4) - val tnum = TNum(BitVecLiteral(0,4), BitVecLiteral(9, 4)) + val tnum = TNum(BitVecLiteral(0, 4), BitVecLiteral(9, 4)) test("Refine lower bound - simple example") { val expected = 8 From 721ba358d9924db3aa4268c3f9a304a36aaaa02c Mon Sep 17 00:00:00 2001 From: Alexander Arthur Date: Fri, 25 Jul 2025 16:49:13 +1000 Subject: [PATCH 6/7] Test case with real procedure! --- .../TNumIntervalReducedProductTest.scala | 120 +++++++++++++++++- 1 file changed, 119 insertions(+), 1 deletion(-) diff --git a/src/test/scala/TNumIntervalReducedProductTest.scala b/src/test/scala/TNumIntervalReducedProductTest.scala index 06b0e85ecd..f9244c7c2f 100644 --- a/src/test/scala/TNumIntervalReducedProductTest.scala +++ b/src/test/scala/TNumIntervalReducedProductTest.scala @@ -1,6 +1,9 @@ import analysis.Interval.ConcreteInterval import analysis.{TNum, TNumIntervalReducedProduct} -import ir.BitVecLiteral +import ir.dsl.* +import ir.* +import ir.transforms.{worklistSolver, reversePostOrder} + import org.scalatest.funsuite.AnyFunSuiteLike @test_util.tags.UnitTest @@ -10,6 +13,113 @@ class TNumIntervalReducedProductTest extends AnyFunSuiteLike { val interval = ConcreteInterval(6, 10, 4) val tnum = TNum(BitVecLiteral(0, 4), BitVecLiteral(9, 4)) + val kbitsProg = prog( + proc( + "knownBitsExample_4196164", + Seq("R0_in" -> BitVecType(64), "R1_in" -> BitVecType(64)), + Seq("R0_out" -> BitVecType(64), "R2_out" -> BitVecType(64), "R3_out" -> BitVecType(64)), + block( + "lknownBitsExample", + LocalAssign( + LocalVar("R2", BitVecType(64), 2), + BinaryExpr( + BVOR, + BinaryExpr(BVAND, LocalVar("R0_in", BitVecType(64), 0), BitVecLiteral(BigInt("18374966859414961920"), 64)), + BitVecLiteral(BigInt("18446744069414584320"), 64) + ), + Some("%0000023e") + ), + LocalAssign( + LocalVar("R0", BitVecType(64), 3), + BinaryExpr( + BVOR, + BinaryExpr(BVAND, LocalVar("R0_in", BitVecType(64), 0), BitVecLiteral(BigInt("18374966859414961920"), 64)), + BitVecLiteral(BigInt("71777218305454335"), 64) + ), + Some("%00000257") + ), + goto("lknownBitsExample_phi_lknownBitsExample_goto_l00000271", "lknownBitsExample_goto_l0000026d") + ), + block( + "l00000274", + LocalAssign( + LocalVar("R0", BitVecType(64), 6), + ZeroExtend( + 4, + BinaryExpr( + BVSHL, + ZeroExtend(8, Extract(60, 8, LocalVar("R2", BitVecType(64), 9))), + BitVecLiteral(BigInt("8"), 60) + ) + ), + Some("%0000027e") + ), + LocalAssign( + LocalVar("R0", BitVecType(64), 7), + BinaryExpr(BVOR, LocalVar("R0", BitVecType(64), 6), BitVecLiteral(BigInt("15"), 64)), + Some("%00000284") + ), + goto("l00000274_phi_l00000274_goto_l00000299", "l00000274_goto_l0000029d") + ), + block( + "l000002a0", + Assert(TrueLiteral, Some("is returning to caller-set R30"), None), + goto("knownBitsExample_4196164_basil_return") + ), + block( + "lknownBitsExample_goto_l0000026d", + Assume(BinaryExpr(EQ, LocalVar("R1_in", BitVecType(64), 0), BitVecLiteral(BigInt("0"), 64)), None, None, true), + LocalAssign(LocalVar("R2", BitVecType(64), 9), LocalVar("R0", BitVecType(64), 3), Some("phiback")), + goto("l00000274") + ), + block( + "l00000274_goto_l0000029d", + Assume( + BinaryExpr(EQ, Extract(16, 0, LocalVar("R2", BitVecType(64), 9)), BitVecLiteral(BigInt("0"), 16)), + None, + None, + true + ), + LocalAssign(LocalVar("R0", BitVecType(64), 14), LocalVar("R2", BitVecType(64), 9), Some("phiback")), + goto("l000002a0") + ), + block( + "knownBitsExample_4196164_basil_return", + ret( + "R0_out" -> LocalVar("R0", BitVecType(64), 14), + "R2_out" -> LocalVar("R2", BitVecType(64), 9), + "R3_out" -> BitVecLiteral(BigInt("71777218305454335"), 64) + ) + ), + block( + "lknownBitsExample_phi_lknownBitsExample_goto_l00000271", + Assume( + UnaryExpr(BoolNOT, BinaryExpr(EQ, LocalVar("R1_in", BitVecType(64), 0), BitVecLiteral(BigInt("0"), 64))), + None, + None, + true + ), + LocalAssign(LocalVar("R2", BitVecType(64), 9), LocalVar("R2", BitVecType(64), 2), Some("phiback")), + goto("l00000274") + ), + block( + "l00000274_phi_l00000274_goto_l00000299", + Assume( + UnaryExpr( + BoolNOT, + BinaryExpr(EQ, Extract(16, 0, LocalVar("R2", BitVecType(64), 9)), BitVecLiteral(BigInt("0"), 16)) + ), + None, + None, + true + ), + LocalAssign(LocalVar("R0", BitVecType(64), 14), LocalVar("R0", BitVecType(64), 7), Some("phiback")), + goto("l000002a0") + ) + ) + ) + val littleProc = kbitsProg.nameToProcedure("knownBitsExample_4196164") + test("Refine lower bound - simple example") { val expected = 8 assert(expected == domain.refineLowerBound(6, tnum)) @@ -40,4 +150,12 @@ class TNumIntervalReducedProductTest extends AnyFunSuiteLike { assert(expected == domain.refineTnum(0, 0, tnum)) } + test("Run on some code!") { + val domain = TNumIntervalReducedProduct() + val solver = worklistSolver(domain) + reversePostOrder(littleProc) + print(solver.solveProc(littleProc, backwards = false)) + assert(true) + } + } From 44f6d833950f7de5491a2c355930b6abee2acb95 Mon Sep 17 00:00:00 2001 From: Alexander Arthur Date: Fri, 25 Jul 2025 16:59:55 +1000 Subject: [PATCH 7/7] Make scalafmt happy (again) --- src/test/scala/TNumIntervalReducedProductTest.scala | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/test/scala/TNumIntervalReducedProductTest.scala b/src/test/scala/TNumIntervalReducedProductTest.scala index f9244c7c2f..c59c37ec82 100644 --- a/src/test/scala/TNumIntervalReducedProductTest.scala +++ b/src/test/scala/TNumIntervalReducedProductTest.scala @@ -1,9 +1,8 @@ import analysis.Interval.ConcreteInterval import analysis.{TNum, TNumIntervalReducedProduct} -import ir.dsl.* import ir.* -import ir.transforms.{worklistSolver, reversePostOrder} - +import ir.dsl.* +import ir.transforms.{reversePostOrder, worklistSolver} import org.scalatest.funsuite.AnyFunSuiteLike @test_util.tags.UnitTest