Skip to content

Commit

Permalink
First working version of function Summaries
Browse files Browse the repository at this point in the history
  • Loading branch information
morbitzer committed Dec 10, 2024
1 parent 1948ca3 commit c521a21
Show file tree
Hide file tree
Showing 2 changed files with 51 additions and 3 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,7 @@ class PointsToPass(ctx: TranslationContext) : EOGStarterPass(ctx, orderDependenc
// doubleState.

// First, collect all writes to all parameters
var changedParams = mutableMapOf<Node, MutableSet<Pair<Node, Boolean>>>()
val changedParams = mutableMapOf<Node, MutableSet<Pair<Node, Boolean>>>()
currentNode.invokes.forEach { fd ->
val tmp = ctx.config.functionSummaries.getLastWrites(fd)
for ((k, v) in tmp) {
Expand Down Expand Up @@ -281,7 +281,26 @@ class PointsToPass(ctx: TranslationContext) : EOGStarterPass(ctx, orderDependenc
} else {
sources.add(currentNode.arguments[value.argumentIndex])
}
// else -> null
is ParameterMemoryValue -> {
// In case the FunctionSummary says that we have to use the
// dereferenced value here, we look up the argument, dereference it,
// and then add it to the sources
if (value.name.localName == "derefvalue") {
val p =
currentNode.invokes
.flatMap { it.parameters }
.filter { it.name == value.name.parent }
p.forEach {
val arg = currentNode.arguments[it.argumentIndex]
sources.addAll(
doubleState.getValues(arg).flatMap {
doubleState.getValues(it)
}
)
}
}
}
else -> sources.add(value)
}
}
if (destinations != null && sources.isNotEmpty()) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1112,6 +1112,20 @@ class PointsToPassTest {
.firstOrNull()
assertNotNull(iRefLine234)

val iRefLine237 =
tu.allChildren<Reference> {
it.location?.region?.startLine == 237 && it.name.localName == "i"
}
.firstOrNull()
assertNotNull(iRefLine237)

val iRefLine240 =
tu.allChildren<Reference> {
it.location?.region?.startLine == 240 && it.name.localName == "i"
}
.firstOrNull()
assertNotNull(iRefLine240)

// Dereferences
val pDerefLine231 =
tu.allChildren<PointerDereference> {
Expand All @@ -1134,6 +1148,13 @@ class PointsToPassTest {
.firstOrNull()
assertNotNull(pDerefLine237)

val pDerefLine240 =
tu.allChildren<PointerDereference> {
it.location?.region?.startLine == 240 && it.name.localName == "p"
}
.firstOrNull()
assertNotNull(pDerefLine240)

// BinaryOperators
val binOpLine207 =
tu.allChildren<BinaryOperator> { it.location?.region?.startLine == 207 }.firstOrNull()
Expand Down Expand Up @@ -1162,8 +1183,16 @@ class PointsToPassTest {

// Line 237
assertEquals(1, pDerefLine237.memoryAddress.size)
assertEquals(jDecl.memoryAddress, pDerefLine237.memoryAddress.firstOrNull())
assertEquals(iDecl.memoryAddress, pDerefLine237.memoryAddress.firstOrNull())
assertEquals(1, pDerefLine237.prevDFG.size)
assertEquals(jDecl.prevDFG.firstOrNull(), pDerefLine237.prevDFG.firstOrNull())

// Line 240
assertEquals(1, pDerefLine240.memoryAddress.size)
assertEquals(iDecl.memoryAddress, pDerefLine240.memoryAddress.firstOrNull())
assertEquals(1, pDerefLine240.prevDFG.size)
assertEquals(binOpLine212, pDerefLine240.prevDFG.firstOrNull())
assertEquals(1, iRefLine240.prevDFG.size)
assertEquals(binOpLine212, iRefLine240.prevDFG.firstOrNull())
}
}

0 comments on commit c521a21

Please sign in to comment.