From 49d6d54211286e38addbac73bab1168cf7795bba Mon Sep 17 00:00:00 2001 From: Calin Cruceru Date: Tue, 30 May 2017 19:12:15 +0300 Subject: [PATCH 1/2] Stop executing instructions in InstructionBlock when `Forward' is reached and use `mkNumeral' instead of `mkInt' in ConstantValue, to avoid overflows --- .../expression/concrete/ConstantValue.scala | 4 ++-- .../instructions/InstructionBlock.scala | 14 +++++++++----- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/main/scala/org/change/v2/analysis/expression/concrete/ConstantValue.scala b/src/main/scala/org/change/v2/analysis/expression/concrete/ConstantValue.scala index 0741712..6b48742 100755 --- a/src/main/scala/org/change/v2/analysis/expression/concrete/ConstantValue.scala +++ b/src/main/scala/org/change/v2/analysis/expression/concrete/ConstantValue.scala @@ -9,7 +9,7 @@ import z3.scala.{Z3Solver, Z3AST} * Created by radu on 3/24/15. */ case class ConstantValue(value: Long) extends Expression with FloatingExpression { - lazy val ast = Z3Util.z3Context.mkInt(value.asInstanceOf[Int], Z3Util.defaultSort) + lazy val ast = Z3Util.z3Context.mkNumeral(value.toString, Z3Util.defaultSort) override def toZ3(solver: Option[Z3Solver] = None): (Z3AST, Option[Z3Solver]) = (ast, solver) @@ -22,5 +22,5 @@ case class ConstantValue(value: Long) extends Expression with FloatingExpression */ override def instantiate(s: State): Either[Expression, String] = Left(this) - override def toString = s"Const($value)]" + override def toString = s"[Const($value)]" } diff --git a/src/main/scala/org/change/v2/analysis/processingmodels/instructions/InstructionBlock.scala b/src/main/scala/org/change/v2/analysis/processingmodels/instructions/InstructionBlock.scala index 1e5e086..7de6fd3 100755 --- a/src/main/scala/org/change/v2/analysis/processingmodels/instructions/InstructionBlock.scala +++ b/src/main/scala/org/change/v2/analysis/processingmodels/instructions/InstructionBlock.scala @@ -14,15 +14,19 @@ case class InstructionBlock(instructions: Iterable[Instruction]) extends Instruc * @param s * @return */ - override def apply(s: State, v: Boolean): (List[State], List[State]) = + override def apply(s: State, v: Boolean): (List[State], List[State]) = { + val initialHistory = s.history + instructions.foldLeft((List(s), Nil: List[State])) { (acc, i) => { - val (valid: List[State], failed: List[State]) = acc - val (nextValid, nextFailed) = valid.map(i(_, v)).unzip - val allValid = nextValid.foldLeft(Nil: List[State])(_ ++ _) - val allFailed = nextFailed.foldLeft(failed: List[State])(_ ++ _) + val (valid, failed) = acc + val (forwarded, notForwarded) = valid.partition(_.history != s.history) + val (nextValid, nextFailed) = notForwarded.map(i(_, v)).unzip + val allValid = nextValid.foldLeft(forwarded)(_ ++ _) + val allFailed = nextFailed.foldLeft(failed)(_ ++ _) (allValid, allFailed) } } + } } object InstructionBlock { From e7945875320c3ee5bb616c6117165d55b53ce8d6 Mon Sep 17 00:00:00 2001 From: Calin Cruceru Date: Tue, 30 May 2017 19:15:55 +0300 Subject: [PATCH 2/2] Use mkNumeral instead of mkInt in ConstantBitVector too --- .../v2/analysis/expression/concrete/ConstantValue.scala | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/main/scala/org/change/v2/analysis/expression/concrete/ConstantValue.scala b/src/main/scala/org/change/v2/analysis/expression/concrete/ConstantValue.scala index 6b48742..14ecd4d 100755 --- a/src/main/scala/org/change/v2/analysis/expression/concrete/ConstantValue.scala +++ b/src/main/scala/org/change/v2/analysis/expression/concrete/ConstantValue.scala @@ -24,3 +24,12 @@ case class ConstantValue(value: Long) extends Expression with FloatingExpression override def toString = s"[Const($value)]" } + +case class ConstantBitVector(value: Long) extends Expression with FloatingExpression { + lazy val ast = Z3Util.z3Context.mkNumeral(value.toString, Z3Util.bv32Sort) + + override def toZ3(solver: Option[Z3Solver] = None): (Z3AST, Option[Z3Solver]) = (ast, solver) + + override def instantiate(s: State): Either[Expression, String] = Left(this) + override def toString = s"[ConstBV($value)]" +}