Skip to content

Commit

Permalink
MemoryLoad as Statement (#269)
Browse files Browse the repository at this point in the history 
* make MemoryLoad a type of Statement, some general cleanup

* consolidate constant propagation variations

* fix renamed parser

* fix deprecated override (this is still inelegant but it will have to do)

* add labels to MemoryLoad

* make DSA behaviour consistent with previous

* fix issues

---------

Co-authored-by: l-kent <[email protected]>
  • Loading branch information
@l-kent
l-kent and l-kent authored Nov 13, 2024
1 parent 7849e72 commit 4586ce2
Show file tree
Hide file tree
Showing 47 changed files with 1,268 additions and 1,305 deletions.
2 changes: 1 addition & 1 deletion src/main/antlr4/Semantics.g4 → src/main/antlr4/ASLp.g4
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
grammar Semantics;
grammar ASLp;

// See aslp/libASL/asl.ott for reference grammar Bap-ali-plugin/asli_lifer.ml may also be useful for
// visitors
Expand Down
38 changes: 22 additions & 16 deletions src/main/scala/analysis/ANR.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import scala.collection.immutable

/**
* Calculates the set of variables that are not read after being written up to that point in the program.
* Useful for detecting dead stores, constants and if what variables are passed as parameters in a function call.
* Useful for detecting dead stores, constants and which variables are passed as parameters in a function call.
*/
trait ANRAnalysis(program: Program) {

Expand All @@ -26,35 +26,41 @@ trait ANRAnalysis(program: Program) {
/** Default implementation of eval.
*/
def eval(cmd: Command, s: Set[Variable]): Set[Variable] = {
var m = s
cmd match {
case assume: Assume =>
m.diff(assume.body.variables)
s.diff(assume.body.variables)
case assert: Assert =>
m.diff(assert.body.variables)
case memoryAssign: MemoryAssign =>
m.diff(memoryAssign.index.variables)
s.diff(assert.body.variables)
case memoryStore: MemoryStore =>
s.diff(memoryStore.index.variables)
case indirectCall: IndirectCall =>
m - indirectCall.target
case assign: Assign =>
m = m.diff(assign.rhs.variables)
if ignoreRegions.contains(assign.lhs) then m else m + assign.lhs
s - indirectCall.target
case assign: LocalAssign =>
val m = s.diff(assign.rhs.variables)
if (ignoreRegions.contains(assign.lhs)) {
m
} else {
m + assign.lhs
}
case memoryLoad: MemoryLoad =>
val m = s.diff(memoryLoad.index.variables)
if (ignoreRegions.contains(memoryLoad.lhs)) {
m
} else {
m + memoryLoad.lhs
}
case _ =>
m
s
}
}

/** Transfer function for state lattice elements.
*/
def localTransfer(n: CFGPosition, s: Set[Variable]): Set[Variable] = n match {
def transfer(n: CFGPosition, s: Set[Variable]): Set[Variable] = n match {
case cmd: Command =>
eval(cmd, s)
case _ => s // ignore other kinds of nodes
}

/** Transfer function for state lattice elements.
*/
def transfer(n: CFGPosition, s: Set[Variable]): Set[Variable] = localTransfer(n, s)
}

class ANRAnalysisSolver(program: Program) extends ANRAnalysis(program)
Expand Down
183 changes: 1 addition & 182 deletions src/main/scala/analysis/Analysis.scala
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,5 @@
package analysis

import ir.*
import analysis.solvers.*

import scala.collection.mutable.{ArrayBuffer, HashMap, ListBuffer}
import java.io.{File, PrintWriter}
import scala.collection.mutable
import scala.collection.immutable
import util.Logger

/** Trait for program analyses.
*
* @tparam R
Expand All @@ -18,176 +9,4 @@ trait Analysis[+R]:

/** Performs the analysis and returns the result.
*/
def analyze(): R

/** Base class for value analysis with simple (non-lifted) lattice.
*/
trait ConstantPropagation(val program: Program) {
/** The lattice of abstract states.
*/

val valuelattice: ConstantPropagationLattice = ConstantPropagationLattice()

val statelattice: MapLattice[Variable, FlatElement[BitVecLiteral], ConstantPropagationLattice] = MapLattice(valuelattice)

/** Default implementation of eval.
*/
def eval(exp: Expr, env: Map[Variable, FlatElement[BitVecLiteral]]): FlatElement[BitVecLiteral] = {
import valuelattice._
exp match {
case id: Variable => env(id)
case n: BitVecLiteral => bv(n)
case ze: ZeroExtend => zero_extend(ze.extension, eval(ze.body, env))
case se: SignExtend => sign_extend(se.extension, eval(se.body, env))
case e: Extract => extract(e.end, e.start, eval(e.body, env))
case bin: BinaryExpr =>
val left = eval(bin.arg1, env)
val right = eval(bin.arg2, env)
bin.op match {
case BVADD => bvadd(left, right)
case BVSUB => bvsub(left, right)
case BVMUL => bvmul(left, right)
case BVUDIV => bvudiv(left, right)
case BVSDIV => bvsdiv(left, right)
case BVSREM => bvsrem(left, right)
case BVUREM => bvurem(left, right)
case BVSMOD => bvsmod(left, right)
case BVAND => bvand(left, right)
case BVOR => bvor(left, right)
case BVXOR => bvxor(left, right)
case BVNAND => bvnand(left, right)
case BVNOR => bvnor(left, right)
case BVXNOR => bvxnor(left, right)
case BVSHL => bvshl(left, right)
case BVLSHR => bvlshr(left, right)
case BVASHR => bvashr(left, right)
case BVCOMP => bvcomp(left, right)
case BVCONCAT => concat(left, right)
}
case un: UnaryExpr =>
val arg = eval(un.arg, env)
un.op match {
case BVNOT => bvnot(arg)
case BVNEG => bvneg(arg)
}
case _ => valuelattice.top
}
}


/** Transfer function for state lattice elements.
*/
def localTransfer(n: CFGPosition, s: Map[Variable, FlatElement[BitVecLiteral]]): Map[Variable, FlatElement[BitVecLiteral]] = {
n match {
// assignments
case la: Assign =>
s + (la.lhs -> eval(la.rhs, s))
// all others: like no-ops
case _ => s
}
}

/** The analysis lattice.
*/
val lattice: MapLattice[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]], MapLattice[Variable, FlatElement[BitVecLiteral], ConstantPropagationLattice]] = MapLattice(statelattice)

val domain: Set[CFGPosition] = Set.empty ++ program

/** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
*/
def transfer(n: CFGPosition, s: Map[Variable, FlatElement[BitVecLiteral]]): Map[Variable, FlatElement[BitVecLiteral]] = localTransfer(n, s)
}

class ConstantPropagationSolver(program: Program) extends ConstantPropagation(program)
with SimplePushDownWorklistFixpointSolver[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]], MapLattice[Variable, FlatElement[BitVecLiteral], ConstantPropagationLattice]]
with IRInterproceduralForwardDependencies
with Analysis[Map[CFGPosition, Map[Variable, FlatElement[BitVecLiteral]]]]


/** Base class for value analysis with simple (non-lifted) lattice.
*/
trait ConstantPropagationWithSSA(val program: Program, val reachingDefs: Map[CFGPosition, (Map[Variable, Set[Assign]], Map[Variable, Set[Assign]])]) {
/** The lattice of abstract states.
*/

val valuelattice: ConstantPropagationLatticeWithSSA = ConstantPropagationLatticeWithSSA()

val statelattice: MapLattice[RegisterWrapperEqualSets, Set[BitVecLiteral], ConstantPropagationLatticeWithSSA] = MapLattice(valuelattice)

/** Default implementation of eval.
*/
def eval(exp: Expr, env: Map[RegisterWrapperEqualSets, Set[BitVecLiteral]], n: CFGPosition): Set[BitVecLiteral] = {
import valuelattice._
exp match {
case id: Variable => env(RegisterWrapperEqualSets(id, getUse(id, n, reachingDefs)))
case n: BitVecLiteral => bv(n)
case ze: ZeroExtend => zero_extend(ze.extension, eval(ze.body, env, n))
case se: SignExtend => sign_extend(se.extension, eval(se.body, env, n))
case e: Extract => extract(e.end, e.start, eval(e.body, env, n))
case bin: BinaryExpr =>
val left = eval(bin.arg1, env, n)
val right = eval(bin.arg2, env, n)
bin.op match {
case BVADD => bvadd(left, right)
case BVSUB => bvsub(left, right)
case BVMUL => bvmul(left, right)
case BVUDIV => bvudiv(left, right)
case BVSDIV => bvsdiv(left, right)
case BVSREM => bvsrem(left, right)
case BVUREM => bvurem(left, right)
case BVSMOD => bvsmod(left, right)
case BVAND => bvand(left, right)
case BVOR => bvor(left, right)
case BVXOR => bvxor(left, right)
case BVNAND => bvnand(left, right)
case BVNOR => bvnor(left, right)
case BVXNOR => bvxnor(left, right)
case BVSHL => bvshl(left, right)
case BVLSHR => bvlshr(left, right)
case BVASHR => bvashr(left, right)
case BVCOMP => bvcomp(left, right)
case BVCONCAT => concat(left, right)
}

case un: UnaryExpr =>
val arg = eval(un.arg, env, n)
un.op match {
case BVNOT => bvnot(arg)
case BVNEG => bvneg(arg)
}

case _ => Set.empty
}
}

/** Transfer function for state lattice elements.
*/
def localTransfer(n: CFGPosition, s: Map[RegisterWrapperEqualSets, Set[BitVecLiteral]]): Map[RegisterWrapperEqualSets, Set[BitVecLiteral]] =
n match {
case a: Assign =>
val lhsWrappers = s.collect {
case (k, v) if RegisterVariableWrapper(k.variable, k.assigns) == RegisterVariableWrapper(a.lhs, getDefinition(a.lhs, a, reachingDefs)) => (k, v)
}
if (lhsWrappers.nonEmpty) {
s ++ lhsWrappers.map((k, v) => (k, v.union(eval(a.rhs, s, a))))
} else {
s + (RegisterWrapperEqualSets(a.lhs, getDefinition(a.lhs, a, reachingDefs)) -> eval(a.rhs, s, n))
}
case _ => s
}

/** The analysis lattice.
*/
val lattice: MapLattice[CFGPosition, Map[RegisterWrapperEqualSets, Set[BitVecLiteral]], MapLattice[RegisterWrapperEqualSets, Set[BitVecLiteral], ConstantPropagationLatticeWithSSA]] = MapLattice(statelattice)

val domain: Set[CFGPosition] = Set.empty ++ program

/** Transfer function for state lattice elements. (Same as `localTransfer` for simple value analysis.)
*/
def transfer(n: CFGPosition, s: Map[RegisterWrapperEqualSets, Set[BitVecLiteral]]): Map[RegisterWrapperEqualSets, Set[BitVecLiteral]] = localTransfer(n, s)
}

class ConstantPropagationSolverWithSSA(program: Program, reachingDefs: Map[CFGPosition, (Map[Variable, Set[Assign]], Map[Variable, Set[Assign]])]) extends ConstantPropagationWithSSA(program, reachingDefs)
with SimplePushDownWorklistFixpointSolver[CFGPosition, Map[RegisterWrapperEqualSets, Set[BitVecLiteral]], MapLattice[RegisterWrapperEqualSets, Set[BitVecLiteral], ConstantPropagationLatticeWithSSA]]
with IRInterproceduralForwardDependencies
with Analysis[Map[CFGPosition, Map[RegisterWrapperEqualSets, Set[BitVecLiteral]]]]
def analyze(): R
75 changes: 0 additions & 75 deletions src/main/scala/analysis/BasicIRConstProp.scala
View file

This file was deleted.

Loading

0 comments on commit 4586ce2

Please sign in to comment.