Skip to content

Commit

Permalink
add three different state modes
Browse files Browse the repository at this point in the history
  • Loading branch information
CodingDepot committed Oct 14, 2024
1 parent e0e1a28 commit ccd839e
Show file tree
Hide file tree
Showing 4 changed files with 31 additions and 20 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ class AbstractEvaluator {
val initialRange = getInitialRange(initializer, targetType)

// evaluate effect of each operation on the list until we reach "node"
val startState = IntervalState(null)
val startState = IntervalState(IntervalState.Mode.OVERWRITE)
startState.push(initializer, IntervalLattice(initialRange))
val finalState = iterateEOG(initializer, startState, ::handleNode)
// TODO: null-safety
Expand Down Expand Up @@ -153,7 +153,7 @@ class AbstractEvaluator {
node: Node,
state: State<Node, LatticeInterval>,
worklist: Worklist<Node, Node, LatticeInterval>
): IntervalState {
): State<Node, LatticeInterval> {
// TODO: create a new micro-evaluation of the value! To do this:
// 1) Determine the EOG that ends the loop
// 2) Create a new State with the current value as initial value
Expand All @@ -164,12 +164,11 @@ class AbstractEvaluator {

val afterLoop = node.nextEOG[1]

// TODO: check condition
// TODO: make sure we only include loop head once

// TODO: apply widening until the current node does not change and stop then
// Create new state using widening and iterate over it
val operatingState = IntervalState(IntervalState.Mode.WIDEN)
operatingState.push(node, state[node])
node.nextEOG.forEach { operatingState.push(it, IntervalLattice(LatticeInterval.BOTTOM)) }
// We set the barrier before iterating to prevent the iteration from leaving the loop
pathBarrier = afterLoop
Expand Down Expand Up @@ -201,7 +200,7 @@ class AbstractEvaluator {

// -- we can return the now overwritten state --

return state as IntervalState
return state
}

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,7 @@ sealed class LatticeInterval : Comparable<LatticeInterval> {
class IntervalLattice(override val elements: LatticeInterval) :
LatticeElement<LatticeInterval>(elements) {
override fun compareTo(other: LatticeElement<LatticeInterval>): Int {
return this.compareTo(other)
return elements.compareTo(other.elements)
}

// Returns true whenever other is fully within this
Expand Down Expand Up @@ -292,14 +292,16 @@ class IntervalLattice(override val elements: LatticeInterval) :
}
}

class IntervalState(private var mode: Mode) : State<Node, LatticeInterval>() {
class IntervalState(private var mode: Mode?) : State<Node, LatticeInterval>() {
var function: (IntervalLattice, IntervalLattice) -> IntervalLattice

/**
* An enum that holds the current mode of operation as this State may be used to apply either
* widening or narrowing
*/
// TODO: should this control the whole state?
enum class Mode {
OVERWRITE,
WIDEN,
NARROW
}
Expand All @@ -308,7 +310,8 @@ class IntervalState(private var mode: Mode) : State<Node, LatticeInterval>() {
function =
when (mode) {
Mode.WIDEN -> IntervalLattice::widen
else -> IntervalLattice::narrow
Mode.NARROW -> IntervalLattice::narrow
else -> { a, _ -> a }
}
}

Expand All @@ -332,14 +335,19 @@ class IntervalState(private var mode: Mode) : State<Node, LatticeInterval>() {
return update
}

/**
* This method checks whether an interval needs to be updated depending on the mode of the
* state. If the state does not operate in a mode it will always return true.
*/
private fun intervalNeedsUpdate(
current: IntervalLattice?,
newLattice: IntervalLattice,
mode: Mode
mode: Mode?
): Boolean {
return when (mode) {
Mode.WIDEN -> current == null || !current.contains(newLattice)
else -> current == null || !newLattice.contains(current)
Mode.NARROW -> current == null || !newLattice.contains(current)
else -> true
}
}

Expand All @@ -360,10 +368,7 @@ class IntervalState(private var mode: Mode) : State<Node, LatticeInterval>() {
newLatticeElement as IntervalLattice
// here we use our "intervalNeedsUpdate" function to determine if we have to do something
if (current != null && intervalNeedsUpdate(current, newLatticeElement, mode)) {
when (mode) {
Mode.WIDEN -> this[newNode] = current.widen(newLatticeElement)
else -> this[newNode] = current.narrow(newLatticeElement)
}
function(current, newLatticeElement)
} else if (current != null) {
return false
} else {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -60,13 +60,21 @@ class Integer : Value {
}
} else if (node is AssignExpression) {
if (node.lhs.any { it.code == name }) {
// TODO: we need to evaluate the right hand side!
return when (node.operatorCode) {
"=" -> {
TODO()
}
"+=" -> {
val openUpper = LatticeInterval.Bounded(0, LatticeInterval.Bound.INFINITE)
current + openUpper to true
}
"-=" -> {
val zeroInterval = LatticeInterval.Bounded(0, 0)
val zeroInterval =
LatticeInterval.Bounded(
LatticeInterval.Bound.NEGATIVE_INFINITE,
LatticeInterval.Bound.NEGATIVE_INFINITE
)
current.join(zeroInterval) to true
}
"*=" -> {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ package de.fraunhofer.aisec.cpg_vis_neo4j

import com.fasterxml.jackson.databind.ObjectMapper
import de.fraunhofer.aisec.cpg.*
import de.fraunhofer.aisec.cpg.analysis.collectioneval.CollectionSizeEvaluator
import de.fraunhofer.aisec.cpg.analysis.abstracteval.AbstractEvaluator
import de.fraunhofer.aisec.cpg.frontends.CompilationDatabase.Companion.fromFile
import de.fraunhofer.aisec.cpg.graph.nodes
import de.fraunhofer.aisec.cpg.graph.statements.expressions.Reference
Expand Down Expand Up @@ -622,13 +622,12 @@ class Application : Callable<Int> {
val targetNodes = nodes.filter { it.name.localName == "a" }
val focusNode =
targetNodes.first {
it.location?.region?.startLine == 53 &&
it.location?.region?.startLine == 87 &&
it is Reference &&
it.type.name.toString() ==
"java.util.LinkedList<java.lang.Integer>" // "int[]" //
// "java.util.LinkedList<java.lang.Integer>"
"int" // "java.util.LinkedList<java.lang.Integer>" // "int[]"
}
val size = CollectionSizeEvaluator().evaluate(focusNode)
val size = AbstractEvaluator().evaluate(focusNode)
println(size)
return EXIT_SUCCESS

Expand Down

0 comments on commit ccd839e

Please sign in to comment.