Skip to content

Memory Transform Bug #592 #595

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

Closed
JTrenerry wants to merge 5 commits into from
Closed

Memory Transform Bug #592 #595

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
9bc478c
Makes a fix of #592, this is still wrong as I cannot convert from Exp…
JTrenerry Jan 27, 2026
5dbd78a
partial commit
JTrenerry Jan 28, 2026
e283229
Pretty much fixed #592, the index is incorrect as it is not the dynam…
JTrenerry Jan 28, 2026
bf0e67b
automated scalafmt
github-actions[bot] Jan 28, 2026
55ce8c1
Move name down to in local areas so global doesn't get confused
JTrenerry Jan 28, 2026
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
134 changes: 126 additions & 8 deletions src/main/scala/ir/transforms/MemoryTransform.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ import scala.collection.mutable
class MemoryTransform(dsa: Map[Procedure, IntervalGraph], globals: Map[IntervalNode, IntervalNode]) extends CILVisitor {
val counter: Counter = Counter()
val memVals = mutable.Map[IntervalCell, String]()
val stackVars: mutable.Map[String, IRType] = mutable.Map.empty
val revEdges: Map[Procedure, Map[IntervalCell, Set[IntervalCell]]] = Map.empty

def isGlobal(flag: DSFlag): Boolean = {
Expand Down Expand Up @@ -45,9 +46,41 @@ class MemoryTransform(dsa: Map[Procedure, IntervalGraph], globals: Map[IntervalN
then ChangeTo(List(LocalAssign(load.lhs, Register(scalarName(index), load.size), load.label)))
else if isLocal(flag) && !index.node.isCollapsed && !flag.escapes && index.node.bases.contains(Stack(proc))
then
ChangeTo(
List(LocalAssign(load.lhs, LocalVar(scalarName(index, Some(proc)), load.lhs.getType), load.label))
)
val name = scalarName(index, Some(proc))
val typeSize = load.lhs.getType match
case BoolType => 1
case IntType => 32
case BitVecType(size) => size
case CustomSort(_) | MapType(_, _) => -1 // TODO: no clue what these types mean in terms of IR
val stackType = stackVars.get(name)
val (loadSize, stype) = stackType match
case t @ Some(BoolType) => (1, t)
case t @ Some(IntType) => (32, t)
case t @ Some(BitVecType(size)) => (size, t)
case t @ Some(CustomSort(_)) => (-1, t)
case t @ Some(MapType(_, _)) => (-1, t)
case None => (-1, None) // Was not in map
stype match
case Some(t) if typeSize != loadSize => (
ChangeTo(
List(
LocalAssign(
load.lhs,
Extract(
load.size,
0,
BinaryExpr(BVSHL, LocalVar(scalarName(index, Some(proc)), t), load.index)
),
load.label
)
)
)
)
case _ => (
ChangeTo(
List(LocalAssign(load.lhs, LocalVar(scalarName(index, Some(proc)), load.lhs.getType), load.label))
)
)
else if !flag.escapes || isGlobal(flag) then
val memName =
if isGlobal(flag) then "Global"
Expand All @@ -74,15 +107,100 @@ class MemoryTransform(dsa: Map[Procedure, IntervalGraph], globals: Map[IntervalN
then ChangeTo(List(MemoryAssign(Register(scalarName(index), store.size), store.value, store.label)))
else if isLocal(flag) && !index.node.isCollapsed && !flag.escapes && index.node.bases.contains(Stack(proc))
then
ChangeTo(
List(
LocalAssign(LocalVar(scalarName(index, Some(proc)), store.value.getType), store.value, store.label)
val name = scalarName(index, Some(proc))
val stackType = stackVars.getOrElseUpdate(name, store.value.getType)
val lhs = LocalVar(name, stackType)
val totalSize = stackType match
case BoolType => 1
case IntType => 32
case BitVecType(size) => size
case CustomSort(_) => -1
case MapType(_, _) => -1
val totalSize2 = store.index.getType match
case BoolType => 1
case IntType => 32
case BitVecType(size) => size
case CustomSort(_) => -1
case MapType(_, _) => -1
if totalSize != store.size
then
/*
If the size of the value you are entering into the stack variable is not the same type
i.e. bitvector size mismatch you need to do the below steps

We seperate the variable into three sections, start, end and the value we are chucking in.
For example for the assignment

var a = b;
where,
a = 000100101010
b = 0101
and we want to put b 4 bits into b
i.e.
a= 0001(0101)1010

start-section = 0001
b / value = 0101
end-section = 1010

== to get start
shift lhs left total size - index = 12 - 4 = 8
000100101010
000000000001
shift right back
000100000000

== to get end
shift lhs right store size + index = 4 + 4 + 8
000100101010
101000000000
shift left back
000000001010

== to extend value
0101
zero extend total size - store.size = 12 - 4 = 8
000000000101
shift left index total size - index = 12 - 4 = 8
000001010000

xor those

000001010000
000000001010
000100000000

gives
000101011010
tada
*/
val bitvectorTotalSize = BitVecLiteral(totalSize, totalSize2)
val bitvectorStoreSize = BitVecLiteral(store.size, totalSize2)

val extendedStoreValue = BinaryExpr(BVSHL, ZeroExtend(totalSize - store.size, store.value), store.index)

val startShift = BinaryExpr(BVSUB, bitvectorTotalSize, store.index)
val endShift = BinaryExpr(BVADD, bitvectorStoreSize, store.index)

val startBV = BinaryExpr(BVSHL, BinaryExpr(BVLSHR, extendedStoreValue, startShift), startShift)
val endBV = BinaryExpr(BVLSHR, BinaryExpr(BVSHL, extendedStoreValue, endShift), endShift)

val resBV = BinaryExpr(BVXOR, startBV, BinaryExpr(BVXOR, extendedStoreValue, endBV))

ChangeTo(List(LocalAssign(lhs, resBV, store.label)))
else
ChangeTo(
List(
LocalAssign(LocalVar(name, store.value.getType), store.value, store.label)
)
)
)
else if !flag.escapes || isGlobal(flag) then
val memName =
if isGlobal(flag) then "Global"
else if isLocal(flag) then "Stack"
else if isLocal(flag) then
val name = scalarName(index, Some(proc))
val stackType = stackVars.getOrElseUpdate(name, store.value.getType)
"Stack"
else
memVals.getOrElseUpdate(
globals.getOrElse(index.node, index.node).get(index.interval),
Expand Down
Loading