Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

IR Changes #188

Merged
merged 12 commits into from
Jun 11, 2024
Merged

IR Changes #188

Show file tree
Hide file tree
Changes from 11 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
b5ae130
merge MemoryStore into MemoryAssign, make BProcedure and BProcedure h…
Feb 23, 2024
2354dbe
make Memory not an Expr as it can only make sense as part of loads an…
Feb 23, 2024
4da2ea4
comment invariants
Feb 23, 2024
143b330
make state register flags IR registers
Feb 23, 2024
fbbc930
updated expected & updatedexpected task for BAP
Feb 23, 2024
199a745
Merge branch 'main' into ir-cleanup
Jun 5, 2024
d5dc2f2
fix merge
Jun 6, 2024
e89a976
Merge branch 'main' into ir-cleanup
Jun 6, 2024
523b0d4
fix merge
Jun 6, 2024
d8e528b
update expected
Jun 6, 2024
fa071bb
Merge branch 'main' into ir-cleanup
Jun 6, 2024
78a0bf6
Merge branch 'main' into ir-cleanup
Jun 11, 2024
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
6 changes: 3 additions & 3 deletions build.sbt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,9 +39,9 @@ libraryDependencies ++= Seq(
)
libraryDependencies += "io.spray" %% "spray-json" % "1.3.6"

lazy val updateExpected = taskKey[Unit]("updates .expected for test cases")
lazy val updateExpectedBAP = taskKey[Unit]("updates .expected for BAP test cases")

updateExpected := {
updateExpectedBAP := {
val correctPath = baseDirectory.value / "src" / "test" / "correct"
val incorrectPath = baseDirectory.value / "src" / "test" / "incorrect"

Expand All @@ -52,7 +52,7 @@ updateExpected := {
val variations = (e * "*") filter { _.isDirectory }
for (v <- variations.get()) {
val name = e.getName
val outPath = v / (name + ".bpl")
val outPath = v / (name + "_bap.bpl")
val expectedPath = v / (name + ".expected")
val resultPath = v / (name + "_result.txt")
if (resultPath.exists()) {
Expand Down
14 changes: 7 additions & 7 deletions src/main/scala/analysis/ANR.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,9 @@ trait ANRAnalysis(cfg: ProgramCfg) {

val first: Set[CfgNode] = Set(cfg.startNode)

private val stackPointer = Register("R31", BitVecType(64))
private val linkRegister = Register("R30", BitVecType(64))
private val framePointer = Register("R29", BitVecType(64))
private val stackPointer = Register("R31", 64)
private val linkRegister = Register("R30", 64)
private val framePointer = Register("R29", 64)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think this change is worth it, it might cause problems if we want to change back to integers e.g. if we are interested in something like the SMACK int selection with cegar paper. Trying to make register an alias for global bitvector variable using inheritance is a bit too tricky imo. It seems cleaner to me to only have regular variables where scope is a parameter/field rather than a trait mixin. We could approach variables being shared similarly, but I do think it makes sense to have shared and unshared be type-incompatible. E.g.

enum VariableKind(name, type, scope, shared):
    case Memory(n,keytype,valtype) extends Variable(n,MapType(keytype,valtype), Global, Shared)
    case Variable(n,t, scope) extends Variable(n,t, scope, Unshared)
    case Register(n, sz) extends Variable(n, BitVecType(sz), Global, Unsharedl)

(as implemented as a trait/case class heirachy this just means moving name,type,scope,shared to the parent trait's constructor?)

Copy link
Contributor Author

@l-kent l-kent Jun 11, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR doesn't make any changes to the scope. If you want to propose changes to how the scope works, you can do that separately. What you're suggesting would make the type system weaker though. What this PR does change is make it so Memory is not an Expr, and so (correctly) is no longer allowed to appear arbitrarily inside other Exprs.

I did consider the implications for supporting an integer representation (as in SMACK) but that would require wider changes anyway, as everything else already assumes everything is bitvectors - the Memory case class already does for instance.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah I agree, if we want to lift registers to variables then we can lift registers to variables.


private val ignoreRegions: Set[Expr] = Set(linkRegister, framePointer, stackPointer)

Expand All @@ -35,12 +35,12 @@ trait ANRAnalysis(cfg: ProgramCfg) {
case assert: Assert =>
m.diff(assert.body.variables)
case memoryAssign: MemoryAssign =>
m.diff(memoryAssign.lhs.variables ++ memoryAssign.rhs.variables)
m.diff(memoryAssign.index.variables)
case indirectCall: IndirectCall =>
m - indirectCall.target
case localAssign: LocalAssign =>
m = m.diff(localAssign.rhs.variables)
if ignoreRegions.contains(localAssign.lhs) then m else m + localAssign.lhs
case assign: Assign =>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am still in favour of having a separate load instruction so that assign is clearly pure computation, but its not essential.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As we've discussed before. this means creating a new temporary variable for nearly every load, adding a lot of bloat to the IR without actually improving anything.

m = m.diff(assign.rhs.variables)
if ignoreRegions.contains(assign.lhs) then m else m + assign.lhs
case _ =>
m
}
Expand Down
10 changes: 5 additions & 5 deletions src/main/scala/analysis/Analysis.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ trait ConstantPropagation(val cfg: ProgramCfg) {
case r: CfgCommandNode =>
r.data match
// assignments
case la: LocalAssign =>
case la: Assign =>
s + (la.lhs -> eval(la.rhs, s))
// all others: like no-ops
case _ => s
Expand Down Expand Up @@ -162,14 +162,14 @@ trait ConstantPropagationWithSSA(val cfg: ProgramCfg) {
case r: CfgCommandNode =>
r.data match {
// assignments
case la: LocalAssign =>
case a: Assign =>
val lhsWrappers = s.collect {
case (k, v) if RegisterVariableWrapper(k.variable) == RegisterWrapperEqualSets(la.lhs) => (k, v)
case (k, v) if RegisterVariableWrapper(k.variable) == RegisterWrapperEqualSets(a.lhs) => (k, v)
}
if (lhsWrappers.nonEmpty) {
s ++ lhsWrappers.map((k, v) => (k, v.union(eval(la.rhs, s))))
s ++ lhsWrappers.map((k, v) => (k, v.union(eval(a.rhs, s))))
} else {
s + (RegisterWrapperEqualSets(la.lhs) -> eval(la.rhs, s))
s + (RegisterWrapperEqualSets(a.lhs) -> eval(a.rhs, s))
}
// all others: like no-ops
case _ => s
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/analysis/BasicIRConstProp.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,9 +54,9 @@ trait ILValueAnalysisMisc:
*/
def localTransfer(n: CFGPosition, s: Map[Variable, FlatElement[BitVecLiteral]]): Map[Variable, FlatElement[BitVecLiteral]] =
n match
case la: LocalAssign =>
case la: Assign =>
s + (la.lhs -> eval(la.rhs, s))
case c: Call => s ++ callerPreservedRegisters.filter(reg => s.keys.exists(_.name == reg)).map(n => Register(n, BitVecType(64)) -> statelattice.sublattice.top).toMap
case c: Call => s ++ callerPreservedRegisters.filter(reg => s.keys.exists(_.name == reg)).map(n => Register(n, 64) -> statelattice.sublattice.top).toMap
case _ => s


Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/analysis/Cfg.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -593,7 +593,7 @@ class ProgramCfgFactory:

// R30 is the link register - this stores the address to return to.
// For now just add a node expressing that we are to return to the previous context.
if (iCall.target == Register("R30", BitVecType(64))) {
if (iCall.target == Register("R30", 64)) {
val returnNode = CfgProcedureReturnNode()
cfg.addEdge(jmpNode, returnNode)
cfg.addEdge(returnNode, funcExitNode)
Expand Down
8 changes: 4 additions & 4 deletions src/main/scala/analysis/InterLiveVarsAnalysis.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package analysis

import analysis.solvers.BackwardIDESolver
import ir.{Assert, Assume, GoTo, CFGPosition, Command, DirectCall, IndirectCall, LocalAssign, MemoryAssign, Procedure, Program, Variable, toShortString}
import ir.{Assert, Assume, GoTo, CFGPosition, Command, DirectCall, IndirectCall, Assign, MemoryAssign, Procedure, Program, Variable, toShortString}

/**
* Micro-transfer-functions for LiveVar analysis
Expand Down Expand Up @@ -35,7 +35,7 @@ trait LiveVarsAnalysisFunctions extends BackwardIDEAnalysis[Variable, TwoElement

def edgesOther(n: CFGPosition)(d: DL): Map[DL, EdgeFunction[TwoElement]] = {
n match
case LocalAssign(variable, expr, _) => // (s - variable) ++ expr.variables
case Assign(variable, expr, _) => // (s - variable) ++ expr.variables
d match
case Left(value) =>
if value == variable then
Expand All @@ -47,11 +47,11 @@ trait LiveVarsAnalysisFunctions extends BackwardIDEAnalysis[Variable, TwoElement
(mp, expVar) => mp + (Left(expVar) -> ConstEdge(TwoElementTop))
}

case MemoryAssign(_, store, _) => // s ++ store.index.variables ++ store.value.variables
case MemoryAssign(_, index, value, _, _, _) => // s ++ store.index.variables ++ store.value.variables
d match
case Left(value) => Map(d -> IdEdge())
case Right(_) =>
(store.index.variables ++ store.value.variables).foldLeft(Map[DL, EdgeFunction[TwoElement]](d -> IdEdge())) {
(index.variables ++ value.variables).foldLeft(Map[DL, EdgeFunction[TwoElement]](d -> IdEdge())) {
(mp, storVar) => mp + (Left(storVar) -> ConstEdge(TwoElementTop))
}

Expand Down
36 changes: 18 additions & 18 deletions src/main/scala/analysis/InterprocSteensgaardAnalysis.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,11 +46,11 @@ class InterprocSteensgaardAnalysis(

val solver: UnionFindSolver[StTerm] = UnionFindSolver()

private val stackPointer = Register("R31", BitVecType(64))
private val linkRegister = Register("R30", BitVecType(64))
private val framePointer = Register("R29", BitVecType(64))
private val stackPointer = Register("R31", 64)
private val linkRegister = Register("R30", 64)
private val framePointer = Register("R29", 64)
private val ignoreRegions: Set[Expr] = Set(linkRegister, framePointer)
private val mallocVariable = Register("R0", BitVecType(64))
private val mallocVariable = Register("R0", 64)

var mallocCount: Int = 0
var stackCount: Int = 0
Expand Down Expand Up @@ -239,19 +239,19 @@ class InterprocSteensgaardAnalysis(
unify(IdentifierVariable(RegisterVariableWrapper(mallocVariable)), PointerRef(AllocVariable(alloc)))
}

case localAssign: LocalAssign =>
localAssign.rhs match {
case assign:Assign =>
assign.rhs match {
case binOp: BinaryExpr =>
// X1 = &X2: [[X1]] = ↑[[X2]]
exprToRegion(binOp, cmd).foreach(
x => unify(IdentifierVariable(RegisterVariableWrapper(localAssign.lhs)), PointerRef(AllocVariable(x)))
x => unify(IdentifierVariable(RegisterVariableWrapper(assign.lhs)), PointerRef(AllocVariable(x)))
)
// TODO: should lookout for global base + offset case as well
case _ =>
unwrapExpr(localAssign.rhs).foreach {
unwrapExpr(assign.rhs).foreach {
case memoryLoad: MemoryLoad =>
// X1 = *X2: [[X2]] = ↑a ^ [[X1]] = a where a is a fresh term variable
val X1 = localAssign.lhs
val X1 = assign.lhs
val X2_star = exprToRegion(memoryLoad.index, cmd)
val alpha = FreshVariable()
X2_star.foreach(
Expand All @@ -263,35 +263,35 @@ class InterprocSteensgaardAnalysis(
Logger.debug("Index: " + memoryLoad.index)
Logger.debug("X2_star: " + X2_star)
Logger.debug("X1: " + X1)
Logger.debug("LocalAssign: " + localAssign)
Logger.debug("LocalAssign: " + assign)

// TODO: This might not be correct for globals
// X1 = &X: [[X1]] = ↑[[X2]] (but for globals)
val $X2 = exprToRegion(memoryLoad.index, cmd)
$X2.foreach(
x => unify(IdentifierVariable(RegisterVariableWrapper(localAssign.lhs)), PointerRef(AllocVariable(x)))
x => unify(IdentifierVariable(RegisterVariableWrapper(assign.lhs)), PointerRef(AllocVariable(x)))
)
case variable: Variable =>
// X1 = X2: [[X1]] = [[X2]]
val X1 = localAssign.lhs
val X1 = assign.lhs
val X2 = variable
unify(IdentifierVariable(RegisterVariableWrapper(X1)), IdentifierVariable(RegisterVariableWrapper(X2)))
case _ => // do nothing
}
}
case memoryAssign: MemoryAssign =>
// *X1 = X2: [[X1]] = ↑a ^ [[X2]] = a where a is a fresh term variable
val X1_star = exprToRegion(memoryAssign.rhs.index, cmd)
val X2 = evaluateExpressionWithSSA(memoryAssign.rhs.value, constantProp(n))
val X1_star = exprToRegion(memoryAssign.index, cmd)
val X2 = evaluateExpressionWithSSA(memoryAssign.value, constantProp(n))
var possibleRegions = Set[MemoryRegion]()
if (X2.isEmpty) {
Logger.debug("Maybe a region: " + exprToRegion(memoryAssign.rhs.value, cmd))
possibleRegions = exprToRegion(memoryAssign.rhs.value, cmd)
Logger.debug("Maybe a region: " + exprToRegion(memoryAssign.value, cmd))
possibleRegions = exprToRegion(memoryAssign.value, cmd)
}
Logger.debug("X2 is: " + X2)
Logger.debug("Evaluated: " + memoryAssign.rhs.value)
Logger.debug("Evaluated: " + memoryAssign.value)
Logger.debug("Region " + X1_star)
Logger.debug("Index " + memoryAssign.rhs.index)
Logger.debug("Index " + memoryAssign.index)
val alpha = FreshVariable()
X1_star.foreach(x =>
unify(ExpressionVariable(x), PointerRef(alpha))
Expand Down
8 changes: 4 additions & 4 deletions src/main/scala/analysis/IntraLiveVarsAnalysis.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
package analysis

import analysis.solvers.SimpleWorklistFixpointSolver
import ir.{Assert, Assume, Block, CFGPosition, Call, DirectCall, GoTo, IndirectCall, Jump, LocalAssign, MemoryAssign, NOP, Procedure, Program, Statement, Variable}
import ir.{Assert, Assume, Block, CFGPosition, Call, DirectCall, GoTo, IndirectCall, Jump, Assign, MemoryAssign, NOP, Procedure, Program, Statement, Variable}

abstract class LivenessAnalysis(program: Program) extends Analysis[Any]:
val lattice: MapLattice[CFGPosition, Set[Variable], PowersetLattice[Variable]] = new MapLattice(new PowersetLattice())
val lattice: MapLattice[CFGPosition, Set[Variable], PowersetLattice[Variable]] = MapLattice(PowersetLattice())
val domain: Set[CFGPosition] = Set.empty ++ program

def transfer(n: CFGPosition, s: Set[Variable]): Set[Variable] = {
n match {
case p: Procedure => s
case b: Block => s
case LocalAssign(variable, expr, _) => (s - variable) ++ expr.variables
case MemoryAssign(_, store, _) => s ++ store.index.variables ++ store.value.variables
case Assign(variable, expr, _) => (s - variable) ++ expr.variables
case MemoryAssign(_, index, value, _, _, _) => s ++ index.variables ++ value.variables
case Assume(expr, _, _, _) => s ++ expr.variables
case Assert(expr, _, _) => s ++ expr.variables
case IndirectCall(variable, _, _) => s + variable
Expand Down
28 changes: 14 additions & 14 deletions src/main/scala/analysis/MemoryRegionAnalysis.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,14 +53,14 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
Logger.debug("Stack detection")
Logger.debug(spList)
stmt match {
case localAssign: LocalAssign =>
if (spList.contains(localAssign.rhs)) {
case assign: Assign =>
if (spList.contains(assign.rhs)) {
// add lhs to spList
spList.addOne(localAssign.lhs)
spList.addOne(assign.lhs)
} else {
// remove lhs from spList
if spList.contains(localAssign.lhs) && localAssign.lhs != stackPointer then // TODO: This is a hack: it should check for stack ptr using the wrapper
spList.remove(spList.indexOf(localAssign.lhs))
if spList.contains(assign.lhs) && assign.lhs != stackPointer then // TODO: This is a hack: it should check for stack ptr using the wrapper
spList.remove(spList.indexOf(assign.lhs))
}
// TODO: should handle the store case (last case)
case _ =>
Expand All @@ -80,10 +80,10 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,

val first: Set[CfgNode] = cfg.funEntries.toSet

private val stackPointer = Register("R31", BitVecType(64))
private val linkRegister = Register("R30", BitVecType(64))
private val framePointer = Register("R29", BitVecType(64))
private val mallocVariable = Register("R0", BitVecType(64))
private val stackPointer = Register("R31", 64)
private val linkRegister = Register("R30", 64)
private val framePointer = Register("R29", 64)
private val mallocVariable = Register("R0", 64)
private val spList = ListBuffer[Expr](stackPointer)
private val ignoreRegions: Set[Expr] = Set(linkRegister, framePointer)
// TODO: this could be used instead of regionAccesses in other analyses to reduce the Expr to region conversion
Expand Down Expand Up @@ -202,16 +202,16 @@ trait MemoryRegionAnalysis(val cfg: ProgramCfg,
s
}
case memAssign: MemoryAssign =>
if (ignoreRegions.contains(memAssign.rhs.value)) {
if (ignoreRegions.contains(memAssign.value)) {
s
} else {
val result = eval(memAssign.rhs.index, s, cmd)
val result = eval(memAssign.index, s, cmd)
regionLattice.lub(s, result)
}
case localAssign: LocalAssign =>
stackDetection(localAssign)
case assign: Assign =>
stackDetection(assign)
var m = s
unwrapExpr(localAssign.rhs).foreach {
unwrapExpr(assign.rhs).foreach {
case memoryLoad: MemoryLoad =>
val result = eval(memoryLoad.index, s, cmd)
m = regionLattice.lub(m, result)
Expand Down
6 changes: 3 additions & 3 deletions src/main/scala/analysis/ParamAnalysis.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,9 @@ class ParamAnalysis(val program: Program) extends Analysis[Any] {
case _ => s
}

private val stackPointer = Register("R31", BitVecType(64))
private val linkRegister = Register("R30", BitVecType(64))
private val framePointer = Register("R29", BitVecType(64))
private val stackPointer = Register("R31", 64)
private val linkRegister = Register("R30", 64)
private val framePointer = Register("R29", 64)

private val ignoreRegisters: Set[Variable] = Set(linkRegister, framePointer, stackPointer)

Expand Down
14 changes: 7 additions & 7 deletions src/main/scala/analysis/RNA.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,9 @@ trait RNAAnalysis(cfg: ProgramCfg) {

val first: Set[CfgNode] = Set(cfg.startNode)

private val stackPointer = Register("R31", BitVecType(64))
private val linkRegister = Register("R30", BitVecType(64))
private val framePointer = Register("R29", BitVecType(64))
private val stackPointer = Register("R31", 64)
private val linkRegister = Register("R30", 64)
private val framePointer = Register("R29", 64)

private val ignoreRegions: Set[Expr] = Set(linkRegister, framePointer, stackPointer)

Expand All @@ -36,13 +36,13 @@ trait RNAAnalysis(cfg: ProgramCfg) {
case assert: Assert =>
m.union(assert.body.variables.filter(!ignoreRegions.contains(_)))
case memoryAssign: MemoryAssign =>
m.union((memoryAssign.lhs.variables ++ memoryAssign.rhs.variables).filter(!ignoreRegions.contains(_)))
m.union(memoryAssign.index.variables.filter(!ignoreRegions.contains(_)))
case indirectCall: IndirectCall =>
if (ignoreRegions.contains(indirectCall.target)) return m
m + indirectCall.target
case localAssign: LocalAssign =>
m = m - localAssign.lhs
m.union(localAssign.rhs.variables.filter(!ignoreRegions.contains(_)))
case assign: Assign =>
m = m - assign.lhs
m.union(assign.rhs.variables.filter(!ignoreRegions.contains(_)))
case _ =>
m
}
Expand Down
8 changes: 4 additions & 4 deletions src/main/scala/analysis/RegToMemAnalysis.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,13 +28,13 @@ trait RegionAccessesAnalysis(cfg: ProgramCfg, constantProp: Map[CfgNode, Map[Var
*/
def eval(cmd: Command, constants: Map[Variable, FlatElement[BitVecLiteral]], s: Map[RegisterVariableWrapper, FlatElement[Expr]]): Map[RegisterVariableWrapper, FlatElement[Expr]] = {
cmd match {
case localAssign: LocalAssign =>
localAssign.rhs match {
case assign: Assign =>
assign.rhs match {
case memoryLoad: MemoryLoad =>
s + (RegisterVariableWrapper(localAssign.lhs) -> FlatEl(memoryLoad))
s + (RegisterVariableWrapper(assign.lhs) -> FlatEl(memoryLoad))
case binaryExpr: BinaryExpr =>
if (evaluateExpression(binaryExpr.arg1, constants).isEmpty) { // approximates Base + Offset
s + (RegisterVariableWrapper(localAssign.lhs) -> FlatEl(binaryExpr))
s + (RegisterVariableWrapper(assign.lhs) -> FlatEl(binaryExpr))
} else {
s
}
Expand Down
16 changes: 8 additions & 8 deletions src/main/scala/analysis/SSAForm.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,18 +52,18 @@ class SSAForm(program: Program) {
for (stmt <- currentBlock.statements) {
Logger.debug(stmt)
stmt match {
case localAssign: LocalAssign =>
transformVariables(localAssign.rhs.variables, currentBlock, proc)
val maxVal = varMaxTracker.getOrElseUpdate(localAssign.lhs.name, 0)
blockBasedMappings((currentBlock, localAssign.lhs.name)) = mutable.Set(maxVal)
case assign: Assign =>
transformVariables(assign.rhs.variables, currentBlock, proc)
val maxVal = varMaxTracker.getOrElseUpdate(assign.lhs.name, 0)
blockBasedMappings((currentBlock, assign.lhs.name)) = mutable.Set(maxVal)

localAssign.lhs.ssa_id.clear()
localAssign.lhs.ssa_id.addAll(blockBasedMappings((currentBlock, localAssign.lhs.name)))
assign.lhs.ssa_id.clear()
assign.lhs.ssa_id.addAll(blockBasedMappings((currentBlock, assign.lhs.name)))

varMaxTracker(localAssign.lhs.name) = blockBasedMappings((currentBlock, localAssign.lhs.name)).max + 1
varMaxTracker(assign.lhs.name) = blockBasedMappings((currentBlock, assign.lhs.name)).max + 1

case memoryAssign: MemoryAssign =>
transformVariables(memoryAssign.rhs.variables, currentBlock, proc)
transformVariables(memoryAssign.index.variables, currentBlock, proc)

case assume: Assume =>
transformVariables(assume.body.variables, currentBlock, proc)
Expand Down
Empty file added src/main/scala/analysis/SteensgaardAnalysis.scala
View file
Open in desktop
Empty file.
Loading