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.

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

Abstract Value Analysis #1759

Open
wants to merge 61 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 60 commits
Commits
Show all changes
61 commits
Select commit Hold shift + click to select a range
3e76a77
create initial Size evaluator for modifiable lists
CodingDepot Jul 24, 2024
7d9db53
move all collection dependant logic into collection class
CodingDepot Jul 29, 2024
3abfa1c
add support for static arrays
CodingDepot Jul 31, 2024
cb55e93
implement narrowing and widening operations
CodingDepot Jul 31, 2024
f43919d
add narrowing and widening to loop analysis
CodingDepot Aug 5, 2024
901f9c2
handle branches in analysis
CodingDepot Aug 5, 2024
4f0e95a
improve loops by preprocessing, better narrowing and valid starting r…
CodingDepot Aug 8, 2024
34412ba
improve subtraction by handling 0 as lowest possible value
CodingDepot Aug 8, 2024
372572c
mark branching nodes as nodes with an effect
CodingDepot Aug 8, 2024
0e3bc5b
correctly identify nodes of deeper branch layers in a loop
CodingDepot Aug 8, 2024
a002201
add documentation
CodingDepot Aug 12, 2024
3648081
temporarily repurpose cpg-neo4j for debugging
CodingDepot Aug 12, 2024
899f919
rework lattice intervals to support negative values
CodingDepot Aug 19, 2024
ecc8035
rename target package to circumvent gitignore
CodingDepot Aug 19, 2024
c6122c6
implement comparable for the LatticeInterval
CodingDepot Aug 19, 2024
fb884f5
implement the IntervalState
CodingDepot Aug 21, 2024
c6d3abb
update the evaluator name in tests
CodingDepot Aug 26, 2024
d231c6d
implement equals check for intervals
CodingDepot Aug 26, 2024
54210d9
add method stub for condition evaluation
CodingDepot Aug 26, 2024
ed21aa8
Merge branch 'main' into rh/abstract-value-analysis
KuechA Oct 3, 2024
344ea58
Spotless
KuechA Oct 3, 2024
52cb857
Squashed commit of the following:
CodingDepot Oct 16, 2024
7028045
fix LatticeInterval.push to join with the previous value as it is alr…
CodingDepot Oct 21, 2024
10f2fc2
Fix Declaration to only effect matching integers
CodingDepot Oct 21, 2024
39db0ba
correctly propagate widening only within loops
CodingDepot Oct 21, 2024
d74c427
added second evaluate call with more defined arguments
CodingDepot Oct 23, 2024
6e988bb
support functions with side effects by creating a function-local eval…
CodingDepot Oct 23, 2024
479f5a4
Merge branch 'main' into rh/abstract-value-analysis
CodingDepot Oct 23, 2024
e0dbe1c
moved side effect analysis to list instead of integer...
CodingDepot Oct 23, 2024
f202ffe
add new 'assignMinus' expression and add the name as code when creati…
CodingDepot Oct 28, 2024
223cc64
cleanup
CodingDepot Oct 28, 2024
bd129b1
add tests for the new Evaluator
CodingDepot Oct 28, 2024
f4c432f
first implementation for other integer operations
CodingDepot Oct 28, 2024
02efd13
add prefix versions of the inc and dec operator
CodingDepot Oct 28, 2024
969260b
Add test case for all implemented Integer operations
CodingDepot Oct 28, 2024
1bcff47
add auto-generated hashcode function
CodingDepot Oct 28, 2024
974ec6a
cleanup and documentation
CodingDepot Oct 28, 2024
68e3b27
remove old code
CodingDepot Oct 28, 2024
e48b709
import cleanup
CodingDepot Oct 28, 2024
04d3260
Merge branch 'main' into rh/abstract-value-analysis
CodingDepot Oct 28, 2024
44e8079
automatically switch interval bounds if the lower bound is greater th…
CodingDepot Oct 30, 2024
eac9e89
remove min and max comparisons after multiplication as the constructo…
CodingDepot Oct 30, 2024
6a3965b
convert Bounded from data class to real class to remove constructor v…
CodingDepot Oct 30, 2024
448363c
fix division to estimate x / ∞ = 0
CodingDepot Oct 30, 2024
7bde4ca
simplify division cases
CodingDepot Oct 30, 2024
5bb2316
Fix invalid division cases
CodingDepot Oct 30, 2024
14c7197
make modulo calculation more concise
CodingDepot Oct 30, 2024
0a29a53
beautify toString representation
CodingDepot Oct 30, 2024
d9cb986
add first LatticeInterval tests
CodingDepot Oct 30, 2024
b61a970
fix meet of intervals when they do not overlap
CodingDepot Oct 30, 2024
70e6853
add equals operator for the Interval wrapper
CodingDepot Nov 4, 2024
dbdb0f7
add tests for meet, widen, narrow and the wrapper
CodingDepot Nov 4, 2024
ce029f5
fix meet test method
CodingDepot Nov 4, 2024
dfc5b29
change default of plusAssign and minusAssign to lose all information
CodingDepot Nov 4, 2024
613457c
add tests for the Integer Value
CodingDepot Nov 4, 2024
ee316eb
check name of array declaration
CodingDepot Nov 4, 2024
435a673
move code block for function side effects further up
CodingDepot Nov 4, 2024
103de89
add tests for array and mutable list
CodingDepot Nov 4, 2024
aa1a467
remove unfinished code block in MutableList
CodingDepot Nov 4, 2024
ebfafd6
made spotless
CodingDepot Nov 4, 2024
6557a39
changed the name of the Value classes to prevent confusion with built…
CodingDepot Nov 18, 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
Original file line number Diff line number Diff line change
@@ -0,0 +1,249 @@
/*
* Copyright (c) 2024, Fraunhofer AISEC. All rights reserved.
*
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
*
* http://www.apache.org/licenses/LICENSE-2.0
*
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
* See the License for the specific language governing permissions and
* limitations under the License.
*
* $$$$$$\ $$$$$$$\ $$$$$$\
* $$ __$$\ $$ __$$\ $$ __$$\
* $$ / \__|$$ | $$ |$$ / \__|
* $$ | $$$$$$$ |$$ |$$$$\
* $$ | $$ ____/ $$ |\_$$ |
* $$ | $$\ $$ | $$ | $$ |
* \$$$$$ |$$ | \$$$$$ |
* \______/ \__| \______/
*
*/
package de.fraunhofer.aisec.cpg.analysis.abstracteval

import de.fraunhofer.aisec.cpg.analysis.abstracteval.value.Array
import de.fraunhofer.aisec.cpg.analysis.abstracteval.value.Integer
import de.fraunhofer.aisec.cpg.analysis.abstracteval.value.Value
import de.fraunhofer.aisec.cpg.graph.Node
import de.fraunhofer.aisec.cpg.graph.statements.DoStatement
import de.fraunhofer.aisec.cpg.graph.statements.ForEachStatement
import de.fraunhofer.aisec.cpg.graph.statements.ForStatement
import de.fraunhofer.aisec.cpg.graph.statements.WhileStatement
import de.fraunhofer.aisec.cpg.graph.statements.expressions.*
import de.fraunhofer.aisec.cpg.helpers.*
import kotlin.reflect.KClass
import kotlin.reflect.full.createInstance
import org.apache.commons.lang3.NotImplementedException

/**
* An evaluator performing abstract evaluation for a singular [Value]. It takes a target [Node] and
* walks back to its Declaration. From there it uses the [Worklist] to traverse the EOG graph until
* it reaches the node. All statements encountered may influence the result as implemented in the
* respective [Value] class. The result is a [LatticeInterval] defining both a lower and upper bound
* for the final value.
*/
class AbstractEvaluator {
// The node for which we want to get the value
private lateinit var targetNode: Node
// The name of the value we are analyzing
private lateinit var targetName: String
// The type of the value we are analyzing
private lateinit var targetType: KClass<out Value>

/**
* Takes a node (e.g. Reference) and tries to evaluate its value at this point in the program.
*/
fun evaluate(node: Node): LatticeInterval {
return evaluate(
node.name.localName,
getInitializerOf(node)!!,
node,
getType(node),
IntervalLattice(LatticeInterval.BOTTOM)
)
}

/**
* Takes a manual configuration and tries to evaluate the value of the node at the end.
*
* @param name The name of the target node
* @param start The beginning of the analysis, usually the start of the target's life
* @param end The place at which we want to know the target's value
* @param type The Type of the target
* @param interval The starting value of the analysis, optional
*/
fun evaluate(
name: String,
start: Node,
end: Node,
type: KClass<out Value>,
interval: IntervalLattice? = null

Check warning on line 84 in cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt

View check run for this annotation

Codecov / codecov/patch

cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt#L84

Added line #L84 was not covered by tests
): LatticeInterval {
targetNode = end
targetName = name
targetType = type

// evaluate effect of each operation on the list until we reach "node"
val startState = IntervalState()
startState.push(start, interval)
val finalState = iterateEOG(start, startState, ::handleNode, targetNode)
return finalState?.get(targetNode)?.elements ?: LatticeInterval.BOTTOM
}

/**
* This function changes the state depending on the current node. This is the handler used in
* _iterateEOG_ to correctly handle complex statements.
*
* @param currentNode The current node
* @param state The state for the current node
* @param worklist The whole worklist to manually handle complex scenarios
* @return The updated state after handling the current node
*/
private fun handleNode(
currentNode: Node,
state: State<Node, LatticeInterval>,
worklist: Worklist<Node, Node, LatticeInterval>
): State<Node, LatticeInterval> {
// Check if the current node is already DONE
// (prevents infinite loop and unnecessary double-checking)
if (worklist.isDone(currentNode)) {
// Mark following nodes as DONE if they only have this as previousEOG or all are DONE
// In other cases, converging branches may still change the node
currentNode.nextEOG.forEach { next ->
if (

Check warning on line 117 in cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt

View check run for this annotation

Codecov / codecov/patch

cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt#L116-L117

Added lines #L116 - L117 were not covered by tests
next.prevEOG.singleOrNull() == currentNode ||
next.prevEOG.all { worklist.isDone(it) }
) {
worklist.evaluationStateMap[next] = Worklist.EvaluationState.DONE

Check warning on line 121 in cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt

View check run for this annotation

Codecov / codecov/patch

cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt#L121

Added line #L121 was not covered by tests
}
}
return state

Check warning on line 124 in cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt

View check run for this annotation

Codecov / codecov/patch

cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt#L123-L124

Added lines #L123 - L124 were not covered by tests
}

// Calculate the effect of the currentNode
val previousInterval = state[currentNode]?.elements
val newInterval = state.calculateEffect(currentNode)
val newState = state.duplicate()

// Check if it is marked as in need of widening
if (worklist.needsWidening(currentNode)) {
// Widen the interval
val widenedInterval = previousInterval!!.widen(newInterval)
// Check if the widening caused a change
if (widenedInterval != previousInterval) {
// YES: mark next nodes as needs widening, add them to worklist
// Overwrite current interval, mark this node as needs narrowing
newState[currentNode] = IntervalLattice(widenedInterval)
currentNode.nextEOG.forEach {
if (!isLoopEnd(it)) {
worklist.evaluationStateMap[it] = Worklist.EvaluationState.WIDENING
}
}
worklist.evaluationStateMap[currentNode] = Worklist.EvaluationState.NARROWING
} else {
// NO: mark the current node as DONE
// We never mark loop heads as DONE as they prevent loop entering otherwise
if (!isLoopHead(currentNode)) {
worklist.evaluationStateMap[currentNode] = Worklist.EvaluationState.DONE
}
}
}

// Otherwise, check if it is marked as in need of narrowing
else if (worklist.needsNarrowing(currentNode)) {
// Narrow the interval
val narrowedInterval = previousInterval!!.narrow(newInterval)

Check warning on line 159 in cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt

View check run for this annotation

Codecov / codecov/patch

cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt#L159

Added line #L159 was not covered by tests
// Check if the narrowing caused a change
if (narrowedInterval != previousInterval) {
// YES: overwrite and keep this node marked
// Mark next nodes as need narrowing and add to worklist
newState[currentNode] = IntervalLattice(narrowedInterval)
currentNode.nextEOG.forEach {
worklist.evaluationStateMap[it] = Worklist.EvaluationState.NARROWING
}

Check warning on line 167 in cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt

View check run for this annotation

Codecov / codecov/patch

cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt#L164-L167

Added lines #L164 - L167 were not covered by tests
} else {
// NO: mark the node as DONE
// We never mark loop heads as DONE as they prevent loop entering otherwise
if (!isLoopHead(currentNode)) {
worklist.evaluationStateMap[currentNode] = Worklist.EvaluationState.DONE

Check warning on line 172 in cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt

View check run for this annotation

Codecov / codecov/patch

cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt#L172

Added line #L172 was not covered by tests
}
}
}

// Otherwise, if it was seen for the first time directly apply the effect.
// If it is within a loop mark it as "NEEDS WIDENING".
// We cannot use the "already_seen" field as it is set before this handler is called
else {
newState[currentNode] = IntervalLattice(newInterval)
// We mark the node as needs widening if it is either a loop head or any previous node
// is marked, but not if the current node ends a loop
if (

Check warning on line 184 in cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt

View check run for this annotation

Codecov / codecov/patch

cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt#L184

Added line #L184 was not covered by tests
isLoopHead(currentNode) ||
(currentNode.prevEOG.any { worklist.needsWidening(it) } &&
!isLoopEnd(currentNode))
) {
worklist.evaluationStateMap[currentNode] = Worklist.EvaluationState.WIDENING
}
}

// Finally, we propagate the current Interval to all successor nodes which are empty.
// If the next EOG already has a value we need to join them.
// This is implemented in IntervalState.push.
// Only do this if we have not yet reached the goal node
if (currentNode != targetNode) {
currentNode.nextEOG.forEach { newState.push(it, newState[currentNode]) }
}

return newState
}

private fun getInitializerOf(node: Node): Node? {
return Value.getInitializer(node)
}

private fun State<Node, LatticeInterval>.calculateEffect(node: Node): LatticeInterval {
return targetType.createInstance().applyEffect(this[node]!!.elements, node, targetName)
}

/**
* Tries to determine the type of the target Node by parsing the type name.
*
* @param node The target node
* @return A [Value] class that models the effects on the node type
*/
private fun getType(node: Node): KClass<out Value> {
if (node !is Reference) {
throw NotImplementedException()

Check warning on line 220 in cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt

View check run for this annotation

Codecov / codecov/patch

cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt#L220

Added line #L220 was not covered by tests
}
val name = node.type.name.toString()
return when {
name.endsWith("[]") -> Array::class
name == "int" -> Integer::class
else -> throw NotImplementedException()

Check warning on line 226 in cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt

View check run for this annotation

Codecov / codecov/patch

cpg-analysis/src/main/kotlin/de/fraunhofer/aisec/cpg/analysis/abstracteval/AbstractEvaluator.kt#L226

Added line #L226 was not covered by tests
}
}

/** This method checks for known loop heads such as For, While or Do. */
private fun isLoopHead(node: Node): Boolean {
return when (node) {
is ForStatement,
is WhileStatement,
is ForEachStatement,
is DoStatement -> true
else -> false
}
}

/**
* This method checks if the current node marks the end of a loop. It assumes that nextEOG[1] of
* the loop head always points to the loop end.
*/
private fun isLoopEnd(node: Node): Boolean {
val head = node.prevEOG.firstOrNull { isLoopHead(it) } ?: return false
return head.nextEOG[1] == node
}
}
Loading
Loading