From 399b5405336a52a6ac6eeda0b059e06b3f3a69b9 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 9 Jul 2025 14:23:10 +1000 Subject: [PATCH 1/5] use generated exprs to test expression evaluation against smt solver --- src/test/scala/BitVectorSMTTest.scala | 23 +++- src/test/scala/ExprGen.scala | 100 ++++++++++++++++++ src/test/scala/TestKnownBitsInterpreter.scala | 97 +---------------- 3 files changed, 124 insertions(+), 96 deletions(-) create mode 100644 src/test/scala/ExprGen.scala diff --git a/src/test/scala/BitVectorSMTTest.scala b/src/test/scala/BitVectorSMTTest.scala index 40a2754e9..645b8ce6e 100644 --- a/src/test/scala/BitVectorSMTTest.scala +++ b/src/test/scala/BitVectorSMTTest.scala @@ -1,12 +1,18 @@ import ir.* +import org.scalacheck.{Arbitrary, Gen} import org.scalatest.* import org.scalatest.funsuite.* +import test_util.{CaptureOutput, ExprGen} import translating.BasilIRToSMT2 import translating.PrettyPrinter.* +import util.Logger import util.z3.* @test_util.tags.UnitTest -class BitVectorEvalTest extends AnyFunSuite { +class BitVectorEvalTest + extends AnyFunSuite + with org.scalatestplus.scalacheck.ScalaCheckPropertyChecks + with CaptureOutput { def genSMT(size: Int) = { val max = BitVecType(size).maxValue.toInt @@ -67,5 +73,20 @@ class BitVectorEvalTest extends AnyFunSuite { } } + implicit lazy val arbExpr: Arbitrary[Expr] = Arbitrary(for { + sz <- Gen.oneOf(List(30, 31, 32, 33, 60, 63, 64, 65, 66, 70, 90, 128, 126)) + e <- ExprGen.genExpr(Some(sz)) + } yield (e)) + + test("interp exprs smt") { + forAll(minSuccessful(30)) { (exp: Expr) => + val test = BinaryExpr(NEQ, exp, ir.eval.evaluateExpr(exp).get) + val q = BasilIRToSMT2.exprUnsat(test, None, false) + Logger.info("assert: " + test) + util.z3.checkSATSMT2(q, Some(30000)) == SatResult.UNSAT + } + } + genSMT(2) + } diff --git a/src/test/scala/ExprGen.scala b/src/test/scala/ExprGen.scala new file mode 100644 index 000000000..4697f97bd --- /dev/null +++ b/src/test/scala/ExprGen.scala @@ -0,0 +1,100 @@ +package test_util +import ir.* +import org.scalacheck.Gen + +object ExprGen { + + def arbBinOp = + Gen.oneOf( + BVAND, + BVOR, + BVADD, + BVMUL, + BVSHL, + BVLSHR, + BVNAND, + BVNOR, + BVXOR, + BVXNOR, + BVSUB, + BVASHR, // broken + BVUREM, // broken + BVSREM, // broken + BVSMOD, // broken + BVUDIV, // broken + BVSDIV // broken + ) + + def arbBinComp = Gen.oneOf(BVULE, BVUGT, BVULT, BVUGE, BVSLT, BVSLE, BVSGT, BVSGE, EQ, NEQ, BVCOMP) + + def genValue(givenSize: Option[Int] = None) = for { + genSize <- Gen.chooseNum(1, 70) + size = givenSize.getOrElse(genSize) + maxVal = BitVecType(size).maxValue + value <- Gen.chooseNum(BigInt(0), maxVal) + } yield (BitVecLiteral(value, size)) + + def genUnExp(size: Option[Int] = None) = for { + v <- genValue(size) + op <- Gen.oneOf(BVNOT, BVNEG) + } yield (UnaryExpr(op, v)) + + def genExt(givenSize: Option[Int] = None) = + if givenSize.exists(_ < 1) then { + genValue(givenSize) + } else + for { + genSize <- Gen.chooseNum(1, 70) + size = givenSize.getOrElse(genSize) + amount <- Gen.chooseNum(0, size - 1) + sizeLeft = size - amount + v <- if (sizeLeft > 1) then genExpr(Some(sizeLeft)) else genValue(Some(sizeLeft)) + vv <- genExpr(Some(amount)) + op <- Gen.oneOf(ZeroExtend(amount, v), SignExtend(amount, v), BinaryExpr(BVCONCAT, v, vv)) + } yield (op) + + def genBinComp() = for { + op <- arbBinComp + genSize <- Gen.chooseNum(1, 70) + l <- genExpr(Some(genSize)) + r <- genExpr(Some(genSize)) + } yield (BinaryExpr(op, l, r)) + + def genBinExp(givenSize: Option[Int] = None): Gen[Expr] = { + def genBV(min: BigInt, max: BigInt, size: Int) = for { + v <- Gen.chooseNum(min, max) + } yield BitVecLiteral(v, size) + for { + genSize <- Gen.chooseNum(1, 70) + size = givenSize.getOrElse(genSize) + op <- Gen.oneOf(arbBinOp, arbBinComp) + maxVal = (BigInt(2).pow(size) - 1) + smallMax = maxVal.min(255) + rhs <- op match { + case BVSDIV => genBV(BigInt(1), maxVal, size) + case BVUDIV => genBV(BigInt(1), maxVal, size) + case BVSREM => genBV(BigInt(1), maxVal, size) + case BVSMOD => genBV(BigInt(1), maxVal, size) + case BVSHL => genBV(BigInt(0), smallMax, size) + case BVLSHR => genBV(BigInt(0), smallMax, size) + case BVASHR => genBV(BigInt(0), smallMax, size) + case _ => genExpr(Some(size)) + } + lhs <- genExpr(Some(size)) + expr = BinaryExpr(op, lhs, rhs) + nexpr <- expr.getType match { + case BoolType if size != 1 => + Gen.oneOf(ZeroExtend(size - 1, UnaryExpr(BoolToBV1, expr)), SignExtend(size - 1, UnaryExpr(BoolToBV1, expr))) + case BoolType => Gen.const(UnaryExpr(BoolToBV1, expr)) + case BitVecType(bvsz) if size > bvsz => Gen.oneOf(ZeroExtend(size - bvsz, expr), SignExtend(size - bvsz, expr)) + case BitVecType(sz) if size == sz => Gen.const(expr) + case x => throw Exception(s"TYPE $x DOES NOT MATCH EXPECTED $size $expr") + } + // rhs <- Gen.chooseNum(BigInt(minBound), (BigInt(2).pow(sizeRhs) - 1)) + } yield nexpr + } + + def genExpr(size: Option[Int] = None): Gen[Expr] = + if (size.exists(_ <= 1)) then genValue(size) else Gen.oneOf(genBinExp(size), genUnExp(size), genValue(size)) + +} diff --git a/src/test/scala/TestKnownBitsInterpreter.scala b/src/test/scala/TestKnownBitsInterpreter.scala index 16d072d42..92d7fe5d0 100644 --- a/src/test/scala/TestKnownBitsInterpreter.scala +++ b/src/test/scala/TestKnownBitsInterpreter.scala @@ -6,7 +6,7 @@ import org.scalacheck.{Arbitrary, Gen} import org.scalatest.* import org.scalatest.funsuite.* import org.scalatestplus.scalacheck.* -import test_util.TestValueDomainWithInterpreter +import test_util.{ExprGen, TestValueDomainWithInterpreter} import translating.PrettyPrinter.* @test_util.tags.UnitTest @@ -166,102 +166,9 @@ class TestKnownBitsInterpreter testInterpret(BigInt("ffffffffffffffff", 16), BigInt("ffffffffffffffff", 16)) } - def arbBinOp = - Gen.oneOf( - BVAND, - BVOR, - BVADD, - BVMUL, - BVSHL, - BVLSHR, - BVNAND, - BVNOR, - BVXOR, - BVXNOR, - BVSUB, - BVASHR, // broken - BVUREM, // broken - BVSREM, // broken - BVSMOD, // broken - BVUDIV, // broken - BVSDIV // broken - ) - - def arbBinComp = Gen.oneOf(BVULE, BVUGT, BVULT, BVUGE, BVSLT, BVSLE, BVSGT, BVSGE, EQ, NEQ, BVCOMP) - - def genValue(givenSize: Option[Int] = None) = for { - genSize <- Gen.chooseNum(1, 70) - size = givenSize.getOrElse(genSize) - maxVal = BitVecType(size).maxValue - value <- Gen.chooseNum(BigInt(0), maxVal) - } yield (BitVecLiteral(value, size)) - - def genUnExp(size: Option[Int] = None) = for { - v <- genValue(size) - op <- Gen.oneOf(BVNOT, BVNEG) - } yield (UnaryExpr(op, v)) - - def genExt(givenSize: Option[Int] = None) = - if givenSize.exists(_ < 1) then { - genValue(givenSize) - } else - for { - genSize <- Gen.chooseNum(1, 70) - size = givenSize.getOrElse(genSize) - amount <- Gen.chooseNum(0, size - 1) - sizeLeft = size - amount - v <- if (sizeLeft > 1) then genExpr(Some(sizeLeft)) else genValue(Some(sizeLeft)) - vv <- genExpr(Some(amount)) - op <- Gen.oneOf(ZeroExtend(amount, v), SignExtend(amount, v), BinaryExpr(BVCONCAT, v, vv)) - } yield (op) - - def genBinComp() = for { - op <- arbBinComp - genSize <- Gen.chooseNum(1, 70) - l <- genExpr(Some(genSize)) - r <- genExpr(Some(genSize)) - } yield (BinaryExpr(op, l, r)) - - def genBinExp(givenSize: Option[Int] = None): Gen[Expr] = { - def genBV(min: BigInt, max: BigInt, size: Int) = for { - v <- Gen.chooseNum(min, max) - } yield BitVecLiteral(v, size) - for { - genSize <- Gen.chooseNum(1, 70) - size = givenSize.getOrElse(genSize) - op <- Gen.oneOf(arbBinOp, arbBinComp) - maxVal = (BigInt(2).pow(size) - 1) - smallMax = maxVal.min(255) - rhs <- op match { - case BVSDIV => genBV(BigInt(1), maxVal, size) - case BVUDIV => genBV(BigInt(1), maxVal, size) - case BVSREM => genBV(BigInt(1), maxVal, size) - case BVSMOD => genBV(BigInt(1), maxVal, size) - case BVSHL => genBV(BigInt(0), smallMax, size) - case BVLSHR => genBV(BigInt(0), smallMax, size) - case BVASHR => genBV(BigInt(0), smallMax, size) - case _ => genExpr(Some(size)) - } - lhs <- genExpr(Some(size)) - expr = BinaryExpr(op, lhs, rhs) - nexpr <- expr.getType match { - case BoolType if size != 1 => - Gen.oneOf(ZeroExtend(size - 1, UnaryExpr(BoolToBV1, expr)), SignExtend(size - 1, UnaryExpr(BoolToBV1, expr))) - case BoolType => Gen.const(UnaryExpr(BoolToBV1, expr)) - case BitVecType(bvsz) if size > bvsz => Gen.oneOf(ZeroExtend(size - bvsz, expr), SignExtend(size - bvsz, expr)) - case BitVecType(sz) if size == sz => Gen.const(expr) - case x => throw Exception(s"TYPE $x DOES NOT MATCH EXPECTED $size $expr") - } - // rhs <- Gen.chooseNum(BigInt(minBound), (BigInt(2).pow(sizeRhs) - 1)) - } yield nexpr - } - - def genExpr(size: Option[Int] = None): Gen[Expr] = - if (size.exists(_ <= 1)) then genValue(size) else Gen.oneOf(genBinExp(size), genUnExp(size), genValue(size)) - implicit lazy val arbExpr: Arbitrary[Expr] = Arbitrary(for { sz <- Gen.chooseNum(0, 70) - e <- genExpr(Some(sz)) + e <- ExprGen.genExpr(Some(sz)) } yield (e)) def evaluateAbstract(e: Expr): TNum = TNumDomain().evaluateExprToTNum(Map(), e) From bdb1f16d93ae7afbfdb0228f15ed1b0eb19e42f5 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 9 Jul 2025 14:44:28 +1000 Subject: [PATCH 2/5] dont gen literal as root expr --- src/main/scala/util/z3/z3process.scala | 12 +++++++++-- src/test/scala/BitVectorSMTTest.scala | 5 +++-- src/test/scala/ExprGen.scala | 20 +++++++++++-------- src/test/scala/TestKnownBitsInterpreter.scala | 2 +- 4 files changed, 26 insertions(+), 13 deletions(-) diff --git a/src/main/scala/util/z3/z3process.scala b/src/main/scala/util/z3/z3process.scala index b4b9786d4..30e7461a8 100644 --- a/src/main/scala/util/z3/z3process.scala +++ b/src/main/scala/util/z3/z3process.scala @@ -8,9 +8,17 @@ enum SatResult { case Unknown(s: String, errors: List[String]) } -def checkSATSMT2(smt: String, softTimeoutMillis: Option[Int] = None): SatResult = { +def checkSATSMT2(smt: String, softTimeoutMillis: Option[Int] = None, timeoutSec: Option[Int] = None): SatResult = { + val t = timeoutSec match { + case Some(n) => Seq(s"-T:$n") + case _ => Seq() + } + val softT = softTimeoutMillis match { + case Some(n) => Seq(s"-t:$n") + case None => Seq() + } val cmd = - Seq("z3", "-smt2", "-in") ++ (if softTimeoutMillis.isDefined then Seq(s"-t:${softTimeoutMillis.get}") else Seq()) + Seq("z3", "-smt2", "-in") ++ t ++ softT val output = (cmd #< ByteArrayInputStream(smt.getBytes("UTF-8"))).!! val errors = output.split("\n").filter(_.trim.startsWith("(error")).toList val outputStripped = output.stripLineEnd diff --git a/src/test/scala/BitVectorSMTTest.scala b/src/test/scala/BitVectorSMTTest.scala index 645b8ce6e..85c78ce27 100644 --- a/src/test/scala/BitVectorSMTTest.scala +++ b/src/test/scala/BitVectorSMTTest.scala @@ -75,7 +75,7 @@ class BitVectorEvalTest implicit lazy val arbExpr: Arbitrary[Expr] = Arbitrary(for { sz <- Gen.oneOf(List(30, 31, 32, 33, 60, 63, 64, 65, 66, 70, 90, 128, 126)) - e <- ExprGen.genExpr(Some(sz)) + e <- ExprGen.genNonLiteralExpr(Some(sz)) } yield (e)) test("interp exprs smt") { @@ -83,7 +83,8 @@ class BitVectorEvalTest val test = BinaryExpr(NEQ, exp, ir.eval.evaluateExpr(exp).get) val q = BasilIRToSMT2.exprUnsat(test, None, false) Logger.info("assert: " + test) - util.z3.checkSATSMT2(q, Some(30000)) == SatResult.UNSAT + assert(util.z3.checkSATSMT2(q, None, Some(5)) == SatResult.UNSAT) + false } } diff --git a/src/test/scala/ExprGen.scala b/src/test/scala/ExprGen.scala index 4697f97bd..f45fdf7cd 100644 --- a/src/test/scala/ExprGen.scala +++ b/src/test/scala/ExprGen.scala @@ -53,14 +53,14 @@ object ExprGen { op <- Gen.oneOf(ZeroExtend(amount, v), SignExtend(amount, v), BinaryExpr(BVCONCAT, v, vv)) } yield (op) - def genBinComp() = for { + def genBinComp(depthLimit: Int) = for { op <- arbBinComp genSize <- Gen.chooseNum(1, 70) - l <- genExpr(Some(genSize)) - r <- genExpr(Some(genSize)) + l <- genExpr(Some(genSize), depthLimit) + r <- genExpr(Some(genSize), depthLimit) } yield (BinaryExpr(op, l, r)) - def genBinExp(givenSize: Option[Int] = None): Gen[Expr] = { + def genBinExp(givenSize: Option[Int] = None, depthLimit: Int): Gen[Expr] = { def genBV(min: BigInt, max: BigInt, size: Int) = for { v <- Gen.chooseNum(min, max) } yield BitVecLiteral(v, size) @@ -78,9 +78,9 @@ object ExprGen { case BVSHL => genBV(BigInt(0), smallMax, size) case BVLSHR => genBV(BigInt(0), smallMax, size) case BVASHR => genBV(BigInt(0), smallMax, size) - case _ => genExpr(Some(size)) + case _ => genExpr(Some(size), depthLimit) } - lhs <- genExpr(Some(size)) + lhs <- genExpr(Some(size), depthLimit) expr = BinaryExpr(op, lhs, rhs) nexpr <- expr.getType match { case BoolType if size != 1 => @@ -94,7 +94,11 @@ object ExprGen { } yield nexpr } - def genExpr(size: Option[Int] = None): Gen[Expr] = - if (size.exists(_ <= 1)) then genValue(size) else Gen.oneOf(genBinExp(size), genUnExp(size), genValue(size)) + def genExpr(size: Option[Int] = None, depthLimit: Int = 10): Gen[Expr] = + if (size.exists(_ <= 1) || depthLimit <= 0) then genValue(size) else Gen.oneOf(genBinExp(size, depthLimit - 1), genUnExp(size), genValue(size)) + + def genNonLiteralExpr(size: Option[Int] = None, depthLimit : Int = 3): Gen[Expr] = + if (size.exists(_ <= 1)) then genValue(size) else Gen.oneOf(genBinExp(size, depthLimit), genUnExp(size)) + } diff --git a/src/test/scala/TestKnownBitsInterpreter.scala b/src/test/scala/TestKnownBitsInterpreter.scala index 92d7fe5d0..1b6cde81d 100644 --- a/src/test/scala/TestKnownBitsInterpreter.scala +++ b/src/test/scala/TestKnownBitsInterpreter.scala @@ -168,7 +168,7 @@ class TestKnownBitsInterpreter implicit lazy val arbExpr: Arbitrary[Expr] = Arbitrary(for { sz <- Gen.chooseNum(0, 70) - e <- ExprGen.genExpr(Some(sz)) + e <- ExprGen.genNonLiteralExpr(Some(sz)) } yield (e)) def evaluateAbstract(e: Expr): TNum = TNumDomain().evaluateExprToTNum(Map(), e) From a31fd986b9cccae274deae094cf3fd193f9092c1 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 9 Jul 2025 14:48:05 +1000 Subject: [PATCH 3/5] fmt --- src/test/scala/BitVectorSMTTest.scala | 1 - src/test/scala/ExprGen.scala | 6 +++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/test/scala/BitVectorSMTTest.scala b/src/test/scala/BitVectorSMTTest.scala index 85c78ce27..f6337ec9d 100644 --- a/src/test/scala/BitVectorSMTTest.scala +++ b/src/test/scala/BitVectorSMTTest.scala @@ -84,7 +84,6 @@ class BitVectorEvalTest val q = BasilIRToSMT2.exprUnsat(test, None, false) Logger.info("assert: " + test) assert(util.z3.checkSATSMT2(q, None, Some(5)) == SatResult.UNSAT) - false } } diff --git a/src/test/scala/ExprGen.scala b/src/test/scala/ExprGen.scala index f45fdf7cd..cf07273d2 100644 --- a/src/test/scala/ExprGen.scala +++ b/src/test/scala/ExprGen.scala @@ -95,10 +95,10 @@ object ExprGen { } def genExpr(size: Option[Int] = None, depthLimit: Int = 10): Gen[Expr] = - if (size.exists(_ <= 1) || depthLimit <= 0) then genValue(size) else Gen.oneOf(genBinExp(size, depthLimit - 1), genUnExp(size), genValue(size)) + if (size.exists(_ <= 1) || depthLimit <= 0) then genValue(size) + else Gen.oneOf(genBinExp(size, depthLimit - 1), genUnExp(size), genValue(size)) - def genNonLiteralExpr(size: Option[Int] = None, depthLimit : Int = 3): Gen[Expr] = + def genNonLiteralExpr(size: Option[Int] = None, depthLimit: Int = 3): Gen[Expr] = if (size.exists(_ <= 1)) then genValue(size) else Gen.oneOf(genBinExp(size, depthLimit), genUnExp(size)) - } From f6024d5e1aea52b75cfb2e704e17226708186433 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 9 Jul 2025 15:01:02 +1000 Subject: [PATCH 4/5] require bitvector value is positive in constructor --- src/main/scala/ir/Expr.scala | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/scala/ir/Expr.scala b/src/main/scala/ir/Expr.scala index 2aa360440..612efe168 100644 --- a/src/main/scala/ir/Expr.scala +++ b/src/main/scala/ir/Expr.scala @@ -80,6 +80,7 @@ case object FalseLiteral extends BoolLit { case class BitVecLiteral(value: BigInt, size: Int) extends Literal with CachedHashCode { require(size >= 0) + require(value >= 0, "bitvector [[value]] must be positive, negatives are represented by twos-complement interpretation of [[value]]") require(value <= getType.maxValue, s"bad value: $value for width $size") override def toBoogie: BitVecBLiteral = BitVecBLiteral(value, size) override def getType: BitVecType = BitVecType(size) From 501aedd36088d4491958f5a525ad4673ee5a9a49 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Wed, 9 Jul 2025 15:37:26 +1000 Subject: [PATCH 5/5] fix lifter bv use --- src/main/scala/ir/Expr.scala | 14 +++++++++++++- .../translating/offlineLifter/OfflineLifter.scala | 2 +- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/main/scala/ir/Expr.scala b/src/main/scala/ir/Expr.scala index 612efe168..fd9b92751 100644 --- a/src/main/scala/ir/Expr.scala +++ b/src/main/scala/ir/Expr.scala @@ -78,9 +78,21 @@ case object FalseLiteral extends BoolLit { override def value = false } +object BitVecLiteral { + def apply(i: Int) = { + eval.BitVectorEval.signedInt2BV(32, BigInt(i)) + } + def apply(i: Long) = { + eval.BitVectorEval.signedInt2BV(64, BigInt(i)) + } +} + case class BitVecLiteral(value: BigInt, size: Int) extends Literal with CachedHashCode { require(size >= 0) - require(value >= 0, "bitvector [[value]] must be positive, negatives are represented by twos-complement interpretation of [[value]]") + require( + value >= 0, + "bitvector [[value]] must be positive, negatives are represented by twos-complement interpretation of [[value]]" + ) require(value <= getType.maxValue, s"bad value: $value for width $size") override def toBoogie: BitVecBLiteral = BitVecBLiteral(value, size) override def getType: BitVecType = BitVecType(size) diff --git a/src/main/scala/translating/offlineLifter/OfflineLifter.scala b/src/main/scala/translating/offlineLifter/OfflineLifter.scala index 96964dbbb..e8441e4c6 100644 --- a/src/main/scala/translating/offlineLifter/OfflineLifter.scala +++ b/src/main/scala/translating/offlineLifter/OfflineLifter.scala @@ -126,7 +126,7 @@ object Lifter { try { val lift = StmtListLifter() lift.builder.pcValue = sp - f_A64_decoder[Expr, Int, BitVecLiteral](lift, BitVecLiteral(BigInt(op), 32), BitVecLiteral(sp, 64)) + f_A64_decoder[Expr, Int, BitVecLiteral](lift, BitVecLiteral(op), BitVecLiteral(sp, 64)) lift.extract.toSeq } catch { case e => {