diff --git a/src/main/scala/analysis/Analysis.scala b/src/main/scala/analysis/Analysis.scala index 2cd8f3c15..5dadbf4b4 100644 --- a/src/main/scala/analysis/Analysis.scala +++ b/src/main/scala/analysis/Analysis.scala @@ -364,7 +364,7 @@ trait MemoryRegionAnalysisMisc: */ s ++ Set((n, result)) case localAssign: LocalAssign => - var m = s + val m = s unwrapExpr(localAssign.rhs).foreach { case memoryLoad: MemoryLoad => val result = eval(memoryLoad.index, s, n) @@ -417,9 +417,8 @@ abstract class LiftedMemoryRegionAnalysis[P <: ProgramCfg]( val globals: Map[BigInt, String], val globalOffsets: Map[BigInt, BigInt], val subroutines: Map[BigInt, String], - val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]] - - , stateAfterNode: Boolean) + val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]], + stateAfterNode: Boolean) extends FlowSensitiveAnalysis(stateAfterNode) with MapLatticeSolver[CfgNode] with MemoryRegionAnalysisMisc { @@ -471,13 +470,13 @@ trait LiftedMemoryRegionAnalysisMisc extends MemoryRegionAnalysisMisc { * Intraprocedural value analysis that uses [[tip.solvers.WorklistFixpointSolverWithReachability]], * with all function entries as start nodes. */ -abstract class IntraprocValueAnalysisWorklistSolverWithReachability[L]( - cfg: ProgramCfg, - globals: Map[BigInt, String], - globalOffsets: Map[BigInt, BigInt], - subroutines: Map[BigInt, String], - constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]] - ) +abstract class IntraprocMemoryRegionAnalysisWorklistSolverWithReachability[L]( + cfg: ProgramCfg, + globals: Map[BigInt, String], + globalOffsets: Map[BigInt, BigInt], + subroutines: Map[BigInt, String], + constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]] + ) extends LiftedMemoryRegionAnalysis( cfg, globals, @@ -497,7 +496,7 @@ object MemoryRegionAnalysis: globalOffsets: Map[BigInt, BigInt], subroutines: Map[BigInt, String], constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]] - ) extends IntraprocValueAnalysisWorklistSolverWithReachability( + ) extends IntraprocMemoryRegionAnalysisWorklistSolverWithReachability( cfg, globals, globalOffsets, diff --git a/src/main/scala/analysis/UtilMethods.scala b/src/main/scala/analysis/UtilMethods.scala index 3b76466c0..7ac6283d8 100644 --- a/src/main/scala/analysis/UtilMethods.scala +++ b/src/main/scala/analysis/UtilMethods.scala @@ -25,6 +25,7 @@ def evaluateExpression(exp: Expr, n: CfgNode, constantPropResult: Map[Variable, case BVSUB => BitVectorEval.smt_bvsub(l, r) case BVASHR => BitVectorEval.smt_bvashr(l, r) case BVCOMP => BitVectorEval.smt_bvcomp(l, r) + case BVCONCAT => BitVectorEval.smt_concat(l, r) case _ => throw new RuntimeException("Binary operation support not implemented: " + binOp.op) } case _ => exp diff --git a/src/main/scala/analysis/VSA.scala b/src/main/scala/analysis/VSA.scala index 14b7919a4..2c0bb5430 100644 --- a/src/main/scala/analysis/VSA.scala +++ b/src/main/scala/analysis/VSA.scala @@ -27,7 +27,7 @@ case class LiteralValue(expr: BitVecLiteral) extends Value { type VSALatticeElem = MapLattice[Variable | MemoryRegion, PowersetLattice[Value]] -trait MemoryRegionValueSetAnalysis: +trait ValueSetAnalysisMisc: val cfg: ProgramCfg val globals: Map[BigInt, String] @@ -43,7 +43,7 @@ trait MemoryRegionValueSetAnalysis: /** The lattice of abstract states. */ - val lattice: MapLattice[CfgNode, VSALatticeElem] = MapLattice(powersetLattice) + val stateLattice: MapLattice[CfgNode, VSALatticeElem] = MapLattice(powersetLattice) val domain: Set[CfgNode] = cfg.nodes.toSet @@ -100,7 +100,7 @@ trait MemoryRegionValueSetAnalysis: /** Default implementation of eval. */ - def eval(cmd: Command, s: lattice.sublattice.Element, n: CfgNode): lattice.sublattice.Element = { + def eval(cmd: Command, s: stateLattice.Element, n: CfgNode): stateLattice.Element = { Logger.debug(s"eval: $cmd") Logger.debug(s"state: $s") Logger.debug(s"node: $n") @@ -114,17 +114,17 @@ trait MemoryRegionValueSetAnalysis: // this is an exception to the rule and only applies to data regions evaluateExpression(memoryLoad.index, n, constantProp(n)) match case bitVecLiteral: BitVecLiteral => - val m = s + (r -> Set(getValueType(bitVecLiteral))) - m + (localAssign.lhs -> m(r)) + s//TODO: val m = s + Set((n, Map(r -> Set(getValueType(bitVecLiteral))))) + //m + (n, localAssign.lhs -> m(r)) case _ => - s + (localAssign.lhs -> s(r)) + s//TODO: s + (localAssign.lhs -> s(r)) case None => Logger.warn("could not find region for " + localAssign) s case e: Expr => { val evaled = evaluateExpression(e, n, constantProp(n)) evaled match - case bv: BitVecLiteral => s + (localAssign.lhs -> Set(getValueType(bv))) + case bv: BitVecLiteral => s//TODO: s + (localAssign.lhs -> Set(getValueType(bv))) case _ => Logger.warn("could not evaluate expression" + e) s @@ -137,9 +137,9 @@ trait MemoryRegionValueSetAnalysis: case Some(r: MemoryRegion) => evaluateExpression(memAssign.rhs.value, n, constantProp(n)) match case bitVecLiteral: BitVecLiteral => - return s + (r -> Set(getValueType(bitVecLiteral))) + return s//TODO: return s + (r -> Set(getValueType(bitVecLiteral))) case variable: Variable => // constant prop returned BOT OR TOP. Merge regions because RHS could be a memory loaded address - return s + (r -> s(variable)) + return s//TODO: return s + (r -> s(variable)) case _ => Logger.warn("Too Complex or Wrapped i.e. Extract(Variable)") // do nothing s @@ -154,7 +154,7 @@ trait MemoryRegionValueSetAnalysis: /** Transfer function for state lattice elements. */ - def localTransfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element = + def localTransfer(n: CfgNode, s: stateLattice.Element): stateLattice.Element = n match { case entry: CfgFunctionEntryNode => mmm.pushContext(entry.data.name) @@ -167,25 +167,85 @@ trait MemoryRegionValueSetAnalysis: case _ => s // ignore other kinds of nodes } -/** Base class for memory region analysis (non-lifted) lattice. - */ -abstract class ValueSetAnalysis( - val cfg: ProgramCfg, +///** Base class for memory region analysis (non-lifted) lattice. +// */ +//abstract class ValueSetAnalysis( +// val cfg: ProgramCfg, +// val globals: Map[BigInt, String], +// val externalFunctions: Map[BigInt, String], +// val globalOffsets: Map[BigInt, BigInt], +// val subroutines: Map[BigInt, String], +// val mmm: MemoryModelMap, +// val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]] +//) extends FlowSensitiveAnalysis(true) +// with MemoryRegionValueSetAnalysis { +// +// /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.) +// */ +// def transfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element = localTransfer(n, s) +// +//} + +/** + * Base class for value analysis with lifted lattice, where the extra bottom element represents "unreachable". + */ +abstract class LiftedValueSetAnalysis[P <: ProgramCfg] ( + val cfg: P, val globals: Map[BigInt, String], val externalFunctions: Map[BigInt, String], val globalOffsets: Map[BigInt, BigInt], val subroutines: Map[BigInt, String], val mmm: MemoryModelMap, - val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]] -) extends FlowSensitiveAnalysis(true) - with MemoryRegionValueSetAnalysis { + val constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]], + stateAfterNode: Boolean) + extends FlowSensitiveAnalysis(stateAfterNode) + with MapLatticeSolver[CfgNode] + with ValueSetAnalysisMisc { - /** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.) - */ - def transfer(n: CfgNode, s: lattice.sublattice.Element): lattice.sublattice.Element = localTransfer(n, s) + /** + * Lifted state lattice, with new bottom element representing "unreachable". + */ + val liftedstatelattice: LiftLattice[stateLattice.type] = new LiftLattice(stateLattice) + + /** + * The analysis lattice. + */ + val lattice: MapLattice[CfgNode, liftedstatelattice.type] = new MapLattice(liftedstatelattice) + + override val domain: Set[CfgNode] = cfg.nodes.toSet + + /** + * The worklist is initialized with all function entry nodes. + */ + val first: Set[CfgNode] = cfg.funEntries.toSet[CfgNode] + + /** + * Overrides `funsub` from [[tip.solvers.MapLatticeSolver]], treating function entry nodes as reachable. + */ + override def funsub(n: CfgNode, x: lattice.Element, intra: Boolean): liftedstatelattice.Element = { + import liftedstatelattice._ + n match { + // function entry nodes are always reachable (if intra-procedural analysis) + case _: CfgFunctionEntryNode => lift(stateLattice.bottom) + // all other nodes are processed with join+transfer + case _ => super.funsub(n, x, intra = true) + } + } +} + +/** + * Functionality for basic analyses with lifted state lattice. + */ +trait LiftedValueSetAnalysisMisc extends ValueSetAnalysisMisc { + /** + * Transfer function for state lattice elements. + * (Same as `localTransfer` for basic analyses with lifted state lattice.) + */ + def transferUnlifted(n: CfgNode, s: stateLattice.Element): stateLattice.Element = localTransfer(n, s) } + abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem]( cfg: ProgramCfg, globals: Map[BigInt, String], @@ -195,8 +255,16 @@ abstract class IntraprocValueSetAnalysisWorklistSolver[L <: VSALatticeElem]( mmm: MemoryModelMap, constantProp: Map[CfgNode, Map[Variable, ConstantPropagationLattice.Element]], val powersetLattice: L -) extends ValueSetAnalysis(cfg, globals, externalFunctions, globalOffsets, subroutines, mmm, constantProp) - with SimpleWorklistFixpointSolver[CfgNode] +) extends LiftedValueSetAnalysis( + cfg, + globals, + externalFunctions, + globalOffsets, subroutines, + mmm, + constantProp, + true) + with LiftedValueSetAnalysisMisc + with WorklistFixpointSolverWithReachability[CfgNode] with ForwardDependencies object ValueSetAnalysis: diff --git a/src/main/scala/util/RunUtils.scala b/src/main/scala/util/RunUtils.scala index 9e9e7a283..abecc1cbb 100644 --- a/src/main/scala/util/RunUtils.scala +++ b/src/main/scala/util/RunUtils.scala @@ -173,7 +173,10 @@ object RunUtils { Logger.info("[!] Running VSA") val vsaSolver = ValueSetAnalysis.WorklistSolver(cfg, globalAddresses, externalAddresses, globalOffsets, subroutines, mmm, constPropResult) - val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.analyze(false) + // TODO: replace ? with the right type + val vsaResult: Map[CfgNode, Map[Variable | MemoryRegion, Set[Value]]] = vsaSolver.unliftedAnalyze(true).asInstanceOf[Map[CfgNode, ?]]].map { + case (k, v) => k -> v.values.flatten.toSet + } Output.output( OtherOutput(OutputKindE.cfg), cfg.toDot(Output.labeler(vsaResult, vsaSolver.stateAfterNode), Output.dotIder),