Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions src/main/scala/analysis/EdgeFunctionLattice.scala
Original file line number Diff line number Diff line change
Expand Up @@ -78,9 +78,35 @@ class EdgeFunctionLattice[T, L <: Lattice[T]](val valuelattice: L) extends Latti
case IdEdge() => this
case ConstEdge(d) => JoinEdge(valuelattice.lub(c, d))
case JoinEdge(d) => JoinEdge(valuelattice.lub(c, d))
case _ => e.joinWith(this)
}

override def toString = s"JoinEdge($c)"
}

/** Edge that has `\l . lub (glb(l, a), b)` as a lambda expression. */
case class MeetThenJoinEdge(a: T, b: T) extends EdgeFunction[T] {
def apply(x: T): T = valuelattice.lub(valuelattice.glb(a, x), b)

def composeWith(e: EdgeFunction[T]): EdgeFunction[T] =
e match {
case IdEdge() => this
case ConstEdge(c) => ConstEdge(valuelattice.lub(b, valuelattice.glb(a, c)))
case JoinEdge(_) => ??? // The JoinEdge case for composition is ignored
case MeetThenJoinEdge(c, d) => MeetThenJoinEdge(valuelattice.lub(b, d),
valuelattice.lub(b, valuelattice.glb(a, valuelattice.lub(c, d))))
case _ => ???
}

def joinWith(e: EdgeFunction[T]): EdgeFunction[T] =
e match {
case IdEdge() => MeetThenJoinEdge(valuelattice.top, b)
case ConstEdge(c) => MeetThenJoinEdge(a, valuelattice.lub(b, c))
case JoinEdge(d) => ???
case MeetThenJoinEdge(c, d) => MeetThenJoinEdge(valuelattice.lub(a, c), valuelattice.lub(b, d))
case _ => e.joinWith(this)
}

override def toString = s"MeetThenJoinEdge($a, $b)"
}
}
22 changes: 22 additions & 0 deletions src/main/scala/analysis/Lattice.scala
Original file line number Diff line number Diff line change
Expand Up @@ -821,3 +821,25 @@ class ConstantPropagationLatticeWithSSA extends PowersetLattice[BitVecLiteral] {

def concat(a: Set[BitVecLiteral], b: Set[BitVecLiteral]): Set[BitVecLiteral] = apply(BitVectorEval.smt_concat, a, b)
}

class StronglyLiveBitsLattice extends MapLattice[Int, TwoElement, TwoElementLattice](TwoElementLattice()) {

override def top: Map[Int, TwoElement] = Map().withDefaultValue(sublattice.top)
def shift(value: Int, originalMap: Map[Int, TwoElement]): Map[Int, TwoElement] = originalMap.map({
case (x, d) =>
x + value -> d
}).withDefaultValue(sublattice.bottom)

def shiftMap(values: Set[Int], originalMap: Map[Int, TwoElement]): Map[Int, TwoElement] = {
values.foldLeft(Map(): Map[Int, TwoElement]){
(x, y) => x ++ originalMap.map({
case (m, n) =>
m + y -> n
})
}.withDefaultValue(sublattice.bottom)
}

def cartesianAdd(as: Set[Int], bs: Set[Int]): Set[Int] =
for {a <- as; b <- bs} yield a + b

}
176 changes: 176 additions & 0 deletions src/main/scala/analysis/StronglyLiveBitsAnalysis.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,176 @@
package analysis

import analysis.solvers.BackwardIDESolver
import ir.*

class StronglyLiveBitsEdgeFunctionLattice(valuelattice: StronglyLiveBitsLattice)
extends EdgeFunctionLattice[Map[Int, TwoElement], StronglyLiveBitsLattice](valuelattice) {
case class ShiftThenJoinEdge(values: Set[Int], constant: Map[Int, TwoElement])
extends EdgeFunction[Map[Int, TwoElement]] {
def apply(x: Map[Int, TwoElement]): Map[Int, TwoElement] =
valuelattice.lub(valuelattice.shiftMap(values, x), constant)

/** Composes this function with the given one. The resulting function first applies `e` then this function.
*/
def composeWith(e: EdgeFunction[Map[Int, TwoElement]]): EdgeFunction[Map[Int, TwoElement]] =
e match {
case IdEdge() => this
case ConstEdge(c) => ConstEdge(this.apply(c))
case ShiftThenJoinEdge(b, d) => ShiftThenJoinEdge(valuelattice.cartesianAdd(values, b),
valuelattice.lub(valuelattice.shiftMap(values, d), constant))
case _ => ??? // Other edges will not be used
}

/** Finds the least upper bound of this function and the given one.
*/
def joinWith(e: EdgeFunction[Map[Int, TwoElement]]): EdgeFunction[Map[Int, TwoElement]] =
e match {
case IdEdge() => ShiftThenJoinEdge(values + 0, constant)
case ConstEdge(c) => ShiftThenJoinEdge(values, valuelattice.lub(constant, c))
case ShiftThenJoinEdge(b, d) => ShiftThenJoinEdge(values ++ b, valuelattice.lub(constant, d))
case _ => ??? // Unimplemented as other edges will not be used
}

override def toString(): String = s"ShiftThenJoinEdge($values, $constant)"
}
}

trait StronglyLiveBitsAnalysisFunctions
extends BackwardIDEAnalysis[Variable, Map[Int, TwoElement], StronglyLiveBitsLattice] {
override val valuelattice: StronglyLiveBitsLattice = StronglyLiveBitsLattice()

override val edgelattice: StronglyLiveBitsEdgeFunctionLattice =
StronglyLiveBitsEdgeFunctionLattice(valuelattice)

val subBot = valuelattice.sublattice.bottom
val subTop = valuelattice.sublattice.top

import edgelattice.{IdEdge, ConstEdge, ShiftThenJoinEdge}

def edgesCallToAfterCall(call: Command, aftercall: DirectCall)(d: DL): Map[DL, EdgeFunction[Map[Int, TwoElement]]] = ???

def edgesCallToEntry(call: Command, entry: Return)(d: DL): Map[DL, EdgeFunction[Map[Int, TwoElement]]] = ???

def edgesExitToAfterCall(exit: Procedure, aftercall: DirectCall)(d: DL): Map[DL, EdgeFunction[Map[Int, TwoElement]]] =
Map(d -> IdEdge())

def mapToTop(body: Expr): Map[Variable, EdgeFunction[Map[Int, TwoElement]]] = {
body.variables.foldLeft(Map(): Map[Variable, EdgeFunction[Map[Int, TwoElement]]])
((x, y) => x + (y -> ConstEdge(valuelattice.top))) // TODO: Make this more precise
}

// Helps with assignment operation
def assignHelper(expr: Expr): Map[Variable, EdgeFunction[Map[Int, TwoElement]]] = {
expr match {
case literal: Literal => Map()
case Extract(end, start, body) => body match {
case literal: Literal => Map()
case variable: Variable => Map(variable -> ShiftThenJoinEdge(Set(start), Map().withDefaultValue(subBot)))
case expr: Expr =>
assignHelper(expr).map({
case (x, edgeFunc) => x -> edgeFunc.composeWith(ShiftThenJoinEdge(Set(start), Map().withDefaultValue(subBot)))
})
}
case Repeat(repeats, body) => mapToTop(body)
case ZeroExtend(extension, body) => assignHelper(body)
case SignExtend(extension, body) => ???
case UnaryExpr(op, arg) => arg match {
case variable: Variable => Map(variable->IdEdge())
case literal: Literal => Map()
case expr: Expr => assignHelper(expr)
}
case BinaryExpr(op, arg1, arg2) => expr.getType match {
case BitVecType(size) => op match {
case op: BVBinOp => op match {
case op: BVCmpOp => ???
case BVAND => (arg1, arg2) match {
case (var1: Variable, var2: Variable) => Map(var1 -> IdEdge(), var2 -> IdEdge())
case (var1: Variable, var2: Literal) => Map(var1 -> IdEdge()) // TODO: More precise?
case (var1: Literal, var2: Variable) => Map(var2 -> IdEdge())
case (var1: Literal, var2: Literal) => Map()
case _ => mapToTop(arg1) ++ mapToTop(arg2)
}
case BVOR => ???
case BVADD => ???
case BVSHL => ???
case BVLSHR => ???
case BVCONCAT => ???
case BVMUL => ???
case BVUDIV => ???
case BVUREM => ???
case BVNAND => ???
case BVNOR => ???
case BVXOR => ???
case BVXNOR => ???
case BVCOMP => ???
case BVSUB => ???
case BVSDIV => ???
case BVSREM => ???
case BVSMOD => ???
case BVASHR => ???
}
case _ => Map()
}
case _ => Map()
}
case variable: Variable => Map(variable -> IdEdge())
case _ => mapToTop(expr)
}
}

def edgesOther(n: CFGPosition)(d: DL): Map[DL, EdgeFunction[Map[Int, TwoElement]]] =
n match {
case LocalAssign(variable, expr, _) =>
d match {
case Left(value) => value.getType match {
case BitVecType(_) => assignHelper(expr).foldLeft(Map[DL, EdgeFunction[Map[Int, TwoElement]]]())
((x, y) => x + (y match {
case (a, b) => Left(a) -> b
}))
case _ => Map() // Non-BitVector type does not have live bits
}
case Right(value) => Map().withDefaultValue(edgelattice.bottom)
}
case MemoryAssign(variable, expr, _) =>
d match {
case Left(value) => value.getType match {
case BitVecType(_) => assignHelper(expr).foldLeft(Map[DL, EdgeFunction[Map[Int, TwoElement]]]())
((x, y) => x + (y match {
case (a, b) => Left(a) -> b
}))
case _ => Map() // Non-BitVector type does not have live bits
}
case Right(value) => Map().withDefaultValue(edgelattice.bottom)
}
case MemoryLoad(variable, _, index, _, _, _) =>
d match {
case Left(value) => value.getType match {
case BitVecType(_) => assignHelper(index).foldLeft(Map[DL, EdgeFunction[Map[Int, TwoElement]]]())
((x, y) => x + (y match {
case (a, b) => Left(a) -> b
}))
case _ => Map() // Non-BitVector type does not have live bits
}
case Right(value) => Map().withDefaultValue(edgelattice.bottom)
}
case MemoryStore(_, index, value, _, _, _) => ???
case Assert(expr, _, _) => ???
case Assume(expr, _, _, _) => ???
case Return(_, varExpr) => varExpr.foldLeft(Map[DL, EdgeFunction[Map[Int, TwoElement]]]())
((x, y) => y match {
case (_, retExpr) => x ++ mapToTop(retExpr).foldLeft(Map[DL, EdgeFunction[Map[Int, TwoElement]]]())(
(a, b) => b match {
case (var1, eFunc) => a + (Left[Variable, Nothing](var1) -> eFunc)
}
)
}
// TODO: Make this more precise

)
case _ => Map(d -> IdEdge()).withDefaultValue(edgelattice.bottom)
}
}

class StronglyLiveBitsAnalysis(program: Program) extends
BackwardIDESolver[Variable, Map[Int, TwoElement], StronglyLiveBitsLattice](program),
StronglyLiveBitsAnalysisFunctions
67 changes: 67 additions & 0 deletions src/test/scala/StronglyLiveBitAnalysisTests.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
import analysis.{StronglyLiveBitsEdgeFunctionLattice, StronglyLiveBitsLattice, StronglyLiveBitsAnalysis,
TwoElement, TwoElementBottom, TwoElementTop}
import ir.BitVecType
import org.scalatest.funsuite.AnyFunSuite
import test_util.{BASILTest, CaptureOutput}
import ir.{dsl, *}
import ir.dsl.*

class StronglyLiveBitAnalysisTests extends AnyFunSuite, CaptureOutput, BASILTest{

val lattice = StronglyLiveBitsLattice()
val bot: TwoElement = TwoElementBottom
val top: TwoElement = TwoElementTop

val edgeFuncLat = StronglyLiveBitsEdgeFunctionLattice(lattice)

// Lattice Tests
test("Shifting Empty map - should return Empty map") {
val result = lattice.shiftMap(Set(1), Map().withDefaultValue(bot))
assert(result == Map().withDefaultValue(bot))
}

test("Shifting a Map with 1 element to the left by one - should return shifted map") {
val result = lattice.shiftMap(Set(1), Map(1->top).withDefaultValue(bot))
assert(result == Map(2->top).withDefaultValue(bot))
}

test("Shifting a Map with a set of two elements - should return a set of two elements") {
val result = lattice.shiftMap(Set(1, 2), Map(1->top).withDefaultValue(bot))
assert(result == Map(2->top, 3->top).withDefaultValue(bot))
}

// End lattice tests
// Start EdgeFunction Tests

test("The composition of an empty constant edge with empty constant edge - should return an empty constant edge") {
val result = edgeFuncLat.ConstEdge(Map().withDefaultValue(bot)).composeWith(
edgeFuncLat.ConstEdge(Map().withDefaultValue(bot)))
assert(result == edgeFuncLat.ConstEdge(Map().withDefaultValue(bot)))
}

// Actual tests


def basicIntraCase(): Unit = {
val program = prog(
proc("main",
block(
"main",
LocalAssign(LocalVar("R1", BitVecType(64), 0), BitVecLiteral(BigInt("7"), 32)),
LocalAssign(LocalVar("R0", BitVecType(64), 2), ZeroExtend(32, Extract(32, 0, LocalVar("R1", BitVecType(64), 0)))),
goto("main_return")
),
block(
"main_return",
ret("R0_out" -> LocalVar("R0", BitVecType(64), 2))
))
)
val liveBitsAnalysisResults = StronglyLiveBitsAnalysis(program).analyze()
println(liveBitsAnalysisResults(program.mainProcedure))

assert(liveBitsAnalysisResults(program.mainProcedure) == Map(R0 -> Map()))
}
test("Basic Intra Live Bits"){
basicIntraCase()
}
}
Loading