From 95744f7774f57df5719761d7b1085dc809fcd14e Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Fri, 1 Nov 2024 15:13:27 +1000 Subject: [PATCH] booltobv1 and copyprop heuristic --- src/main/scala/boogie/BExpr.scala | 8 +++ src/main/scala/ir/Expr.scala | 28 +++++---- src/main/scala/ir/eval/ExprEval.scala | 23 +++---- src/main/scala/ir/eval/SimplifyExpr.scala | 31 +++++----- .../invariant/BlocksUniqueToProcedure.scala | 20 +++++++ src/main/scala/ir/transforms/Simp.scala | 60 ++++++++++++++----- src/main/scala/translating/IRExpToSMT2.scala | 24 +++++--- src/main/scala/translating/IRToBoogie.scala | 8 ++- src/main/scala/util/RunUtils.scala | 43 +++++++++---- 9 files changed, 171 insertions(+), 74 deletions(-) diff --git a/src/main/scala/boogie/BExpr.scala b/src/main/scala/boogie/BExpr.scala index 3d3d00e52..cd01c39b9 100644 --- a/src/main/scala/boogie/BExpr.scala +++ b/src/main/scala/boogie/BExpr.scala @@ -270,6 +270,7 @@ case class BFunctionCall(name: String, args: List[BExpr], outType: BType, uninte case class UnaryBExpr(op: UnOp, arg: BExpr) extends BExpr { override def getType: BType = (op, arg.getType) match { + case (BoolToBV1, BoolBType) => BitVecBType(1) case (_: BoolUnOp, BoolBType) => BoolBType case (_: BVUnOp, bv: BitVecBType) => bv case (_: IntUnOp, IntBType) => IntBType @@ -282,6 +283,7 @@ case class UnaryBExpr(op: UnOp, arg: BExpr) extends BExpr { } override def toString: String = op match { + case BoolToBV1 => s"$op($arg)" case uOp: BoolUnOp => s"($uOp$arg)" case uOp: BVUnOp => s"bv$uOp$inSize($arg)" case uOp: IntUnOp => s"($uOp$arg)" @@ -289,6 +291,7 @@ case class UnaryBExpr(op: UnOp, arg: BExpr) extends BExpr { override def functionOps: Set[FunctionOp] = { val thisFn = op match { + case b @ BoolToBV1 => Set(BoolToBV1Op(arg)) case b: BVUnOp => Set(BVFunctionOp(s"bv$b$inSize", s"bv$b", List(BParam(arg.getType)), BParam(getType))) case _ => Set() @@ -680,6 +683,11 @@ case class BInBounds(base: BExpr, len: BExpr, endian: Endian, i: BExpr) extends override def loads: Set[BExpr] = base.loads ++ len.loads ++ i.loads } + +case class BoolToBV1Op(arg: BExpr) extends FunctionOp { + val fnName: String = "bool2bv1" +} + case class BMemoryLoad(memory: BMapVar, index: BExpr, endian: Endian, bits: Int) extends BExpr { override def toString: String = s"$fnName($memory, $index)" diff --git a/src/main/scala/ir/Expr.scala b/src/main/scala/ir/Expr.scala index b572a52eb..8fd9f2fa6 100644 --- a/src/main/scala/ir/Expr.scala +++ b/src/main/scala/ir/Expr.scala @@ -25,7 +25,6 @@ sealed trait Expr { lazy val variablesCached = variables } - def size(e: Expr) = { e.getType match { case BitVecType(s) => Some(s) @@ -67,9 +66,10 @@ case class IntLiteral(value: BigInt) extends Literal { override def toString: String = value.toString } -/** - * @param end : high bit exclusive - * @param start : low bit inclusive +/** @param end + * : high bit exclusive + * @param start + * : low bit inclusive * @param body */ case class Extract(end: Int, start: Int, body: Expr) extends Expr { @@ -130,6 +130,7 @@ case class UnaryExpr(op: UnOp, arg: Expr) extends Expr { override def variables: Set[Variable] = arg.variables override def loads: Set[MemoryLoad] = arg.loads override def getType: IRType = (op, arg.getType) match { + case (BoolToBV1, BoolType) => BitVecType(1) case (_: BoolUnOp, BoolType) => BoolType case (_: BVUnOp, bv: BitVecType) => bv case (_: IntUnOp, IntType) => IntType @@ -157,6 +158,7 @@ sealed trait BoolUnOp(op: String) extends UnOp { } case object BoolNOT extends BoolUnOp("!") +case object BoolToBV1 extends BoolUnOp("bool2bv1") sealed trait IntUnOp(op: String) extends UnOp { override def toString: String = op @@ -165,7 +167,6 @@ sealed trait IntUnOp(op: String) extends UnOp { case object IntNEG extends IntUnOp("-") - sealed trait BVUnOp(op: String) extends UnOp { override def toString: String = op } @@ -212,7 +213,9 @@ case class BinaryExpr(op: BinOp, arg1: Expr, arg2: Expr) extends Expr { case IntEQ | IntNEQ | IntLT | IntLE | IntGT | IntGE => BoolType } case _ => - throw new Exception("type mismatch, operator " + op.getClass.getSimpleName + s" type doesn't match args: (" + arg1 + ", " + arg2 + ")") + throw new Exception( + "type mismatch, operator " + op.getClass.getSimpleName + s" type doesn't match args: (" + arg1 + ", " + arg2 + ")" + ) } private def inSize = arg1.getType match { @@ -237,7 +240,7 @@ case class BinaryExpr(op: BinOp, arg1: Expr, arg2: Expr) extends Expr { } trait BinOp { - def opName : String + def opName: String } sealed trait BoolBinOp(op: String) extends BinOp { @@ -386,7 +389,7 @@ case class Register(override val name: String, size: Int) extends Variable with } // Variable with scope local to the procedure, typically a temporary variable created in the lifting process -case class LocalVar(varName: String, override val irType: IRType, val index : Int = 0) extends Variable { +case class LocalVar(varName: String, override val irType: IRType, val index: Int = 0) extends Variable { override val name = varName + (if (index > 0) then s"_$index" else "") override def toGamma: BVar = BVariable(s"Gamma_$name", BoolBType, Scope.Local) override def toBoogie: BVar = BVariable(s"$name", irType.toBoogie, Scope.Local) @@ -396,11 +399,10 @@ case class LocalVar(varName: String, override val irType: IRType, val index : In object LocalVar { - def unapply(l: LocalVar) : Option[(String, IRType)] = Some((s"${l.name}_${l.index}", l.irType)) + def unapply(l: LocalVar): Option[(String, IRType)] = Some((s"${l.name}_${l.index}", l.irType)) } - // A memory section sealed trait Memory extends Global { val name: String @@ -416,11 +418,13 @@ sealed trait Memory extends Global { } // A stack section of memory, which is local to a thread -case class StackMemory(override val name: String, override val addressSize: Int, override val valueSize: Int) extends Memory { +case class StackMemory(override val name: String, override val addressSize: Int, override val valueSize: Int) + extends Memory { override def acceptVisit(visitor: Visitor): Memory = visitor.visitStackMemory(this) } // A non-stack region of memory, which is shared between threads -case class SharedMemory(override val name: String, override val addressSize: Int, override val valueSize: Int) extends Memory { +case class SharedMemory(override val name: String, override val addressSize: Int, override val valueSize: Int) + extends Memory { override def acceptVisit(visitor: Visitor): Memory = visitor.visitSharedMemory(this) } diff --git a/src/main/scala/ir/eval/ExprEval.scala b/src/main/scala/ir/eval/ExprEval.scala index 22ee56370..18a154e99 100644 --- a/src/main/scala/ir/eval/ExprEval.scala +++ b/src/main/scala/ir/eval/ExprEval.scala @@ -89,6 +89,8 @@ def evalUnOp(op: UnOp, body: Literal): Expr = { case (i: IntLiteral, IntNEG) => IntLiteral(-i.value) case (FalseLiteral, BoolNOT) => TrueLiteral case (TrueLiteral, BoolNOT) => FalseLiteral + case (TrueLiteral, BoolToBV1) => BitVecLiteral(1, 0) + case (FalseLiteral, BoolToBV1) => BitVecLiteral(0, 1) case (_, _) => throw Exception(s"Unreachable ${(body, op)}") } } @@ -154,15 +156,15 @@ def fastPartialEvalExpr(exp: Expr): Expr = { exp match { case f: UninterpretedFunction => f case unOp: UnaryExpr => { - unOp.arg match { - case l: Literal => evalUnOp(unOp.op, l) - case o => UnaryExpr(unOp.op, o) - } + unOp.arg match { + case l: Literal => evalUnOp(unOp.op, l) + case o => UnaryExpr(unOp.op, o) } + } case binOp: BinaryExpr => - val lhs = binOp.arg1 - val rhs = binOp.arg2 - binOp.getType match { + val lhs = binOp.arg1 + val rhs = binOp.arg2 + binOp.getType match { case m: MapType => binOp case b: BitVecType => { (binOp.op, lhs, rhs) match { @@ -217,14 +219,13 @@ def fastPartialEvalExpr(exp: Expr): Expr = { case o => r.copy(body = o) } case variable: Variable => variable - case ml: MemoryLoad => + case ml: MemoryLoad => val addr = ml.index - ml.copy(index= addr) - case b: Literal => b + ml.copy(index = addr) + case b: Literal => b } } - def statePartialEvalExpr[S](l: Loader[S, InterpreterError])(exp: Expr): State[S, Expr, InterpreterError] = { val eval = statePartialEvalExpr(l) val ns = exp match { diff --git a/src/main/scala/ir/eval/SimplifyExpr.scala b/src/main/scala/ir/eval/SimplifyExpr.scala index ec42a540d..2a94aa399 100644 --- a/src/main/scala/ir/eval/SimplifyExpr.scala +++ b/src/main/scala/ir/eval/SimplifyExpr.scala @@ -118,7 +118,7 @@ def simplifyExpr(e: Expr): (Expr, Boolean) = { def bool2bv1(e: Expr) = { e.getType match { case BitVecType(1) => e - case BoolType => UninterpretedFunction("bool2bv1", Seq(e), BitVecType(1)) + case BoolType => UnaryExpr(BoolToBV1, e) case _ => ??? } @@ -221,28 +221,27 @@ def simplifyExpr(e: Expr): (Expr, Boolean) = { /* push bool2bv upwards */ case BinaryExpr( bop, - UninterpretedFunction("bool2bv1", Seq(l), _), - UninterpretedFunction("bool2bv1", Seq(r), _) + UnaryExpr(BoolToBV1, l), + UnaryExpr(BoolToBV1, r), ) if bvLogOpToBoolOp.contains(bop) => { bool2bv1(BinaryExpr(bvLogOpToBoolOp(bop), (l), (r))) } case BinaryExpr( bop, - UninterpretedFunction("bool2bv1", Seq(l), _), - UninterpretedFunction("bool2bv1", Seq(r), _) + UnaryExpr(BoolToBV1, l), + UnaryExpr(BoolToBV1, r), ) if bvLogOpToBoolOp.contains(bop) => { bool2bv1(BinaryExpr(bvLogOpToBoolOp(bop), (l), (r))) } - case UnaryExpr(BVNOT, UninterpretedFunction("bool2bv1", Seq(arg), BitVecType(1))) => + case UnaryExpr(BVNOT, UnaryExpr(BoolToBV1, arg)) => bool2bv1(UnaryExpr(BoolNOT, arg)) /* remove bool2bv in boolean context */ - case BinaryExpr(BVEQ, UninterpretedFunction("bool2bv1", Seq(body), _), BitVecLiteral(1, 1)) => (body) - case BinaryExpr(BVEQ, UninterpretedFunction("bool2bv1", Seq(l), _), UninterpretedFunction("bool2bv1", Seq(r), _)) => - BinaryExpr(BoolEQ, (l), (r)) - case UninterpretedFunction("bool2bv1", Seq(FalseLiteral), _) => BitVecLiteral(0, 1) - case UninterpretedFunction("bool2bv1", Seq(TrueLiteral), _) => BitVecLiteral(1, 1) + case BinaryExpr(BVEQ, UnaryExpr(BoolToBV1, body), BitVecLiteral(1, 1)) => body + case BinaryExpr(BVEQ, UnaryExpr(BoolToBV1, l), UnaryExpr(BoolToBV1, r)) => BinaryExpr(BoolEQ, (l), (r)) + case UnaryExpr(BoolToBV1, FalseLiteral) => BitVecLiteral(0, 1) + case UnaryExpr(BoolToBV1, TrueLiteral) => BitVecLiteral(1, 1) case BinaryExpr(BoolAND, x, TrueLiteral) => x case BinaryExpr(BoolAND, x, FalseLiteral) => FalseLiteral @@ -288,7 +287,7 @@ def simplifyExpr(e: Expr): (Expr, Boolean) = { ) // high precision op ) ) - if (o1 == o2) && o1 == BVADD && (lhs) == (orig) + if sz > 1 && (o1 == o2) && o1 == BVADD && (lhs) == (orig) && AlgebraicSimplifications(SignExtend(exts, x1)) == x2 && AlgebraicSimplifications(SignExtend(exts, y1)) == y2 => { BinaryExpr(BVSGE, x1, UnaryExpr(BVNEG, y1)) @@ -333,7 +332,7 @@ def simplifyExpr(e: Expr): (Expr, Boolean) = { ) ) ) - if (o1 == o2) && o2 == o4 && o1 == BVADD && (lhs) == (orig) + if sz > 1 && (o1 == o2) && o2 == o4 && o1 == BVADD && (lhs) == (orig) && AlgebraicSimplifications(x2) == AlgebraicSimplifications(SignExtend(exts, x1)) && AlgebraicSimplifications(y2) == AlgebraicSimplifications(SignExtend(exts, y1)) && AlgebraicSimplifications(z2) == AlgebraicSimplifications(SignExtend(exts, z1)) => { @@ -346,7 +345,7 @@ def simplifyExpr(e: Expr): (Expr, Boolean) = { ZeroExtend(exts, orig @ BinaryExpr(o1, x1, y1)), compar @ BinaryExpr(o2, x2, y2) ) - if (o1 == o2) && o1 == BVADD + if size(x1).get > 1 && (o1 == o2) && o1 == BVADD && AlgebraicSimplifications(x2) == AlgebraicSimplifications(ZeroExtend(exts, x1)) && AlgebraicSimplifications(y2) == AlgebraicSimplifications(ZeroExtend(exts, y1)) => { // C not Set @@ -358,7 +357,7 @@ def simplifyExpr(e: Expr): (Expr, Boolean) = { ZeroExtend(exts, orig @ BinaryExpr(o1, BinaryExpr(o3, x1, y1), z1)), BinaryExpr(o2, compar @ BinaryExpr(o4, x2, y2), z2) // high precision op ) - if (o1 == o2) && o2 == o4 && o1 == BVADD + if size(x1).get > 1 && (o1 == o2) && o2 == o4 && o1 == BVADD && (x2) == (ZeroExtend(exts, x1)) && (y2) == (ZeroExtend(exts, y1)) && (z2) == (ZeroExtend(exts, z1)) => { @@ -371,7 +370,7 @@ def simplifyExpr(e: Expr): (Expr, Boolean) = { ZeroExtend(exts, orig @ BinaryExpr(o1, x1, UnaryExpr(BVNEG, y1))), BinaryExpr(o2, compar @ BinaryExpr(o4, ZeroExtend(ext1, x2), ZeroExtend(ext2, UnaryExpr(BVNOT, y2))), BitVecLiteral(1, _)) // high precision op ) - if (o1 == o2) && o2 == o4 && o1 == BVADD + if size(x1).get > 1 && (o1 == o2) && o2 == o4 && o1 == BVADD && exts == ext1 && exts == ext2 && x1 == x2 && y1 == y2 => { // C not Set diff --git a/src/main/scala/ir/invariant/BlocksUniqueToProcedure.scala b/src/main/scala/ir/invariant/BlocksUniqueToProcedure.scala index a90f7633a..e53ae4d30 100644 --- a/src/main/scala/ir/invariant/BlocksUniqueToProcedure.scala +++ b/src/main/scala/ir/invariant/BlocksUniqueToProcedure.scala @@ -37,6 +37,26 @@ private class BVis extends CILVisitor { } } + +def blockUniqueLabels(p: Program) : Boolean = { + p.procedures.forall(blockUniqueLabels) +} + +def blockUniqueLabels(p: Procedure) : Boolean = { + val blockNames = mutable.Set[String]() + var passed = true + + for (block <- p.blocks) { + if (blockNames.contains(block.label)) { + passed = false + Logger.error("Duplicate block name: " + block.label) + } + blockNames.add(block.label) + } + passed +} + + def blocksUniqueToEachProcedure(p: Program) : Boolean = { val v = BVis() visit_prog(v, p) diff --git a/src/main/scala/ir/transforms/Simp.scala b/src/main/scala/ir/transforms/Simp.scala index 77974081b..af95457fc 100644 --- a/src/main/scala/ir/transforms/Simp.scala +++ b/src/main/scala/ir/transforms/Simp.scala @@ -269,7 +269,7 @@ def removeSlices(p: Procedure): Unit = { } enum HighZeroBits: - case Bits(n: Int) // most significant bit that is accessed (and all below) + case Bits(n: Int, var unifromAccesses: Boolean = true) // most significant bit that is accessed (and all below) case False // property is false case Bot // don't know anything @@ -306,18 +306,18 @@ def removeSlices(p: Procedure): Unit = { return (); } if (((!result.contains(v)) || result.get(v).contains(HighZeroBits.Bot))) { - result(v) = HighZeroBits.Bits(highestBit) + result(v) = HighZeroBits.Bits(highestBit, true) } else { result(v) match { - case HighZeroBits.Bits(n) if highestBit == size(v).get => { + case HighZeroBits.Bits(n, _) if highestBit == size(v).get => { // access full expr result(v) = HighZeroBits.False } - case HighZeroBits.Bits(n) if highestBit > n => { + case HighZeroBits.Bits(n, _) if highestBit > n => { // relax constraint to bits accessed - result(v) = HighZeroBits.Bits(highestBit) + result(v) = HighZeroBits.Bits(highestBit, false) } - case HighZeroBits.Bits(n) if n >= highestBit => { + case HighZeroBits.Bits(n, _) if n >= highestBit => { // access satisfied by upper constraint } case _ => () @@ -327,7 +327,12 @@ def removeSlices(p: Procedure): Unit = { override def vstmt(s: Statement) = { s match { + case Assign(l: LocalVar, r: LocalVar, _) => { + /** direct copy ; use union-find result to process access **/ + SkipChildren() + } case d: DirectCall => { + /** we always need to pass whole variable across calls since we analyse intraprocedurally */ d.outParams.map(_._2).collect { case l: LocalVar => { result(l) = HighZeroBits.False @@ -366,10 +371,18 @@ def removeSlices(p: Procedure): Unit = { } } - val toSmallen = CheckUsesHaveExtend()(p).collect { case (v, HighZeroBits.Bits(x)) => + val onlyKeepWhereAllAccessesSliceSameBits = true + val toSmallen = CheckUsesHaveExtend()(p).collect { case (v, HighZeroBits.Bits(x, onlyKeepWhereAllAccessesSliceSameBits)) => v -> x }.toMap + /** + * This transform moves bvextracts from the uses to the definition, if all uses have an extract of some size. + * Ideally this removes the extract in some cases. To bemore strict the + * val onlyKeepWhereAllAccessesSliceSameBits = true + * flag only applies this transform when all accesses have extactly the same slice, effectively removing the slice at access. + */ + class ReplaceAlwaysSlicedVars(varHighZeroBits: Map[LocalVar, Int]) extends CILVisitor { var formals = Set[LocalVar]() @@ -914,15 +927,15 @@ object CCP { def DSACopyProp(p: Procedure): Map[Variable, Expr] = { - case class PropState(val e: Expr, val deps: Set[Variable], var clobbered: Boolean, var useCount: Int) + case class PropState(val e: Expr, val deps: mutable.Set[Variable], var clobbered: Boolean, var useCount: Int, var isFlagDep: Boolean) val state = mutable.HashMap[Variable, PropState]() - var poisoned = false + var poisoned = false // we have an indirect call def clobberFull(c: mutable.HashMap[Variable, PropState], l: Variable): Unit = { if (c.contains(l)) { c(l).clobbered = true } else { - c(l) = PropState(FalseLiteral, Set(), true, 0) + c(l) = PropState(FalseLiteral, mutable.Set(), true, 0, false) } } @@ -933,6 +946,8 @@ def DSACopyProp(p: Procedure): Map[Variable, Expr] = { } } + val flagNames = Set("ZF", "VF", "CF", "NF", "R31") + def transfer(c: mutable.HashMap[Variable, PropState], s: Statement): Unit = { // val callClobbers = ((0 to 7) ++ (19 to 30)).map("R" + _).map(c => Register(c, 64)) s match { @@ -945,17 +960,29 @@ def DSACopyProp(p: Procedure): Map[Variable, Expr] = { val rhsDeps = evaled.variables.toSet val existing = c.get(l) + val isFlag = l match { + case l: LocalVar => flagNames.contains(l.varName) + case l => flagNames.contains(l.name) + } + + c.get(l).foreach(v => v.isFlagDep = v.isFlagDep || isFlag) + for (l <- rhsDeps) { + c.get(l).foreach(v => v.isFlagDep = v.isFlagDep || isFlag) + } + existing match { case None => { - c(l) = PropState(evaled, rhsDeps, false, 0) + c(l) = PropState(evaled, mutable.Set.from(rhsDeps), false, 0, isFlag) } case Some(ps) if ps.clobbered => { () } case Some(ps) if ps.e != evaled => { + ps.deps.addAll(rhsDeps) clobberFull(c, l) } case _ => { + // clobberFull(c, l) // ps.e == evaled and have prop } } @@ -975,6 +1002,8 @@ def DSACopyProp(p: Procedure): Map[Variable, Expr] = { } } case x: IndirectCall => { + // not really correct + poisoned = true for ((i, v) <- c) { v.clobbered = true } @@ -987,7 +1016,7 @@ def DSACopyProp(p: Procedure): Map[Variable, Expr] = { val worklist = mutable.PriorityQueue[Block]()(Ordering.by(_.rpoOrder)) worklist.addAll(p.blocks) - while (worklist.nonEmpty) { + while (worklist.nonEmpty && !poisoned) { val b: Block = worklist.dequeue for (l <- b.statements) { @@ -995,8 +1024,8 @@ def DSACopyProp(p: Procedure): Map[Variable, Expr] = { } } - val res = state.collect { - case (v, c) if !c.clobbered => v -> c.e + val res = if poisoned then Map() else state.collect { + case (v, c) if !c.clobbered && (c.useCount == 1 || c.isFlagDep || c.e.isInstanceOf[Variable] || c.e.isInstanceOf[Literal]) => v -> c.e }.toMap res } @@ -1151,7 +1180,8 @@ class Simplify( Logger.warn(s"Some skipped substitution at $bl due to resulting expr size > ${threshold} threshold") } } - ChangeTo(result) + // ChangeDoChildrenPost(result, x => x) + ChangeDoChildrenPost(result, x => x) } override def vblock(b: Block) = { diff --git a/src/main/scala/translating/IRExpToSMT2.scala b/src/main/scala/translating/IRExpToSMT2.scala index fd71a3440..30edde03c 100644 --- a/src/main/scala/translating/IRExpToSMT2.scala +++ b/src/main/scala/translating/IRExpToSMT2.scala @@ -94,6 +94,7 @@ object BasilIRToSMT2 extends BasilIRExpWithVis[Sexp] { case BVNOT => "bvnot" case BVNEG => "bvneg" case IntNEG => "-" + case BoolToBV1 => "bool2bv1" } } @@ -159,16 +160,21 @@ object BasilIRToSMT2 extends BasilIRExpWithVis[Sexp] { } } + + def booltoBVDef : Sexp[Expr] = { + list( + sym("define-fun"), + sym("bool2bv1"), + list(list(sym("arg"), basilTypeToSMTType(BoolType))), + basilTypeToSMTType(BitVecType(1)), + list(sym("ite"), sym("arg"), bv2smt(BitVecLiteral(1, 1)), bv2smt(BitVecLiteral(0, 1))) + ) + } + def interpretFun(x: UninterpretedFunction): Option[Sexp[Expr]] = { x.name match { case "bool2bv1" => { - Some(list( - sym("define-fun"), - sym(x.name), - list(list(sym("arg"), basilTypeToSMTType(BoolType))), - basilTypeToSMTType(x.returnType), - list(sym("ite"), sym("arg"), bv2smt(BitVecLiteral(1, 1)), bv2smt(BitVecLiteral(0, 1))) - )) + Some(booltoBVDef) } case "bvsaddo" => None case _ => { @@ -193,6 +199,10 @@ object BasilIRToSMT2 extends BasilIRExpWithVis[Sexp] { decled = decled ++ decl.toSet DoChildren() // get variables out of args } + case UnaryExpr(BoolToBV1, _) => { + decled = decled + booltoBVDef + DoChildren() + } case v: Variable => { val decl = list(sym("declare-const"), sym(fixVname(v.name)), basilTypeToSMTType(v.getType)) decled = decled + decl diff --git a/src/main/scala/translating/IRToBoogie.scala b/src/main/scala/translating/IRToBoogie.scala index acdd70243..b32ec0ffb 100644 --- a/src/main/scala/translating/IRToBoogie.scala +++ b/src/main/scala/translating/IRToBoogie.scala @@ -63,7 +63,7 @@ class IRToBoogie(var program: Program, var spec: Specification, var thread: Opti translatedProcedures } val defaultGlobals = List(BVarDecl(mem, List(externAttr)), BVarDecl(Gamma_mem, List(externAttr))) - val globalVars = procedures.flatMap(p => p.globals ++ p.freeRequires.flatMap(_.globals) ++ p.freeEnsures.flatMap(_.globals) ++ p.ensures.flatMap(_.globals) ++ p.requires.flatMap(_.globals)) + val globalVars = procedures.flatMap(p => p.globals) val globalDecls = (globalVars.map(b => BVarDecl(b, List(externAttr))) ++ defaultGlobals).distinct.sorted.toList val globalConsts: List[BConstAxiomPair] = @@ -217,6 +217,12 @@ class IRToBoogie(var program: Program, var spec: Specification, var thread: Opti def functionOpToDefinition(f: FunctionOp): BFunction = { f match { + case b @ BoolToBV1Op(arg) => { + val invar = BParam("arg", BoolBType) + val outvar = BParam(BitVecBType(1)) + val body = IfThenElse(invar, BitVecBLiteral(1,1), BitVecBLiteral(0, 1)) + BFunction(b.fnName, List(invar), outvar, Some(body), List(externAttr)) + } case b: BVFunctionOp => BFunction(b.name, b.in, b.out, None, List(externAttr, b.attribute)) case m: MemoryLoadOp => val memVar = BMapVar("memory", MapBType(BitVecBType(m.addressSize), BitVecBType(m.valueSize)), Scope.Parameter) diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala index 9a9c00694..cf3d1ff3d 100644 --- a/src/main/scala/util/RunUtils.scala +++ b/src/main/scala/util/RunUtils.scala @@ -531,45 +531,64 @@ object RunUtils { // writeToFile(dotBlockGraph(ctx.program, ctx.program.filter(_.isInstanceOf[Block]).map(b => b -> b.toString).toMap), s"blockgraph-before-simp.dot") Logger.info("[!] Running Simplify") val timer = PerformanceTimer("Simplify") + val write = false transforms.applyRPO(ctx.program) + + transforms.removeEmptyBlocks(ctx.program) + transforms.coalesceBlocks(ctx.program) + transforms.removeEmptyBlocks(ctx.program) + if write then writeToFile(dotBlockGraph(ctx.program, ctx.program.filter(_.isInstanceOf[Block]).map(b => b -> b.toString).toMap), s"blockgraph-before-dsa.dot") + Logger.info(s"RPO ${timer.checkPoint("RPO")} ms ") Logger.info("[!] Simplify :: DynamicSingleAssignment") - - // writeToFile(serialiseIL(ctx.program), s"il-before-dsa.il") + if write then writeToFile(serialiseIL(ctx.program), s"il-before-dsa.il") // transforms.DynamicSingleAssignment.applyTransform(ctx.program, liveVars) transforms.OnePassDSA().applyTransform(ctx.program) Logger.info(s"DSA ${timer.checkPoint("DSA ")} ms ") - // writeToFile(dotBlockGraph(ctx.program, ctx.program.filter(_.isInstanceOf[Block]).map(b => b -> b.toString).toMap), s"blockgraph-after-dsa.dot") + if write then writeToFile(dotBlockGraph(ctx.program, ctx.program.filter(_.isInstanceOf[Block]).map(b => b -> b.toString).toMap), s"blockgraph-after-dsa.dot") if (ir.eval.SimplifyValidation.validate) { - Logger.info("Live vars difftest") - val tipLiveVars : Map[CFGPosition, Set[Variable]] = analysis.IntraLiveVarsAnalysis(ctx.program).analyze() - assert(ctx.program.procedures.forall(transforms.difftestLiveVars(_, tipLiveVars))) + // Logger.info("Live vars difftest") + // val tipLiveVars : Map[CFGPosition, Set[Variable]] = analysis.IntraLiveVarsAnalysis(ctx.program).analyze() + //assert(ctx.program.procedures.forall(transforms.difftestLiveVars(_, tipLiveVars))) Logger.info("DSA Check") val x = ctx.program.procedures.forall(transforms.rdDSAProperty) assert(x) + Logger.info("DSA Check passed") } - Logger.info("DSA Check passed") assert(invariant.singleCallBlockEnd(ctx.program)) assert(invariant.cfgCorrect(ctx.program)) assert(invariant.blocksUniqueToEachProcedure(ctx.program)) - // writeToFile(serialiseIL(ctx.program), s"il-before-copyprop.il") + if write then writeToFile(serialiseIL(ctx.program), s"il-before-copyprop.il") // brute force run the analysis twice because it cleans up more stuff transforms.doCopyPropTransform(ctx.program) transforms.doCopyPropTransform(ctx.program) - transforms.doCopyPropTransform(ctx.program) + assert(invariant.blockUniqueLabels(ctx.program)) Logger.info(s"CopyProp ${timer.checkPoint("CopyProp")} ms ") - // writeToFile(serialiseIL(ctx.program), s"il-after-copyprop.il") + if write then writeToFile(serialiseIL(ctx.program), s"il-after-copyprop.il") + + + if (ir.eval.SimplifyValidation.validate) { + Logger.info("DSA Check (after transform)") + val x = ctx.program.procedures.forall(transforms.rdDSAProperty) + assert(x) + Logger.info("passed") + } // run this after cond recovery because sign bit calculations often need high bits // which go away in high level conss - // writeToFile(serialiseIL(ctx.program), s"il-after-slices.il") + if write then writeToFile(serialiseIL(ctx.program), s"il-after-slices.il") + + if write then writeToFile(dotBlockGraph(ctx.program, ctx.program.filter(_.isInstanceOf[Block]).map(b => b -> b.toString).toMap), s"blockgraph-after-simp.dot") + + // re-apply dsa + // transforms.OnePassDSA().applyTransform(ctx.program) + if write then writeToFile(dotBlockGraph(ctx.program, ctx.program.filter(_.isInstanceOf[Block]).map(b => b -> b.toString).toMap), s"blockgraph-after-second-dsa.dot") - // writeToFile(dotBlockGraph(ctx.program, ctx.program.filter(_.isInstanceOf[Block]).map(b => b -> b.toString).toMap), s"blockgraph-after-simp.dot") if (ir.eval.SimplifyValidation.validate) { Logger.info("[!] Simplify :: Writing simplification validation")