diff --git a/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/AbstractFlowAnalysis.kt b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/AbstractFlowAnalysis.kt
new file mode 100644
index 0000000000..c7cea444d2
--- /dev/null
+++ b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/AbstractFlowAnalysis.kt
@@ -0,0 +1,40 @@
+/*
+ * Copyright 2022 UnitTestBot contributors (utbot.org)
+ *
+ * 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 org.usvm.dataflow.jvm.flow
+
+import org.jacodb.api.jvm.cfg.JcBytecodeGraph
+
+abstract class AbstractFlowAnalysis(
+ override val graph: JcBytecodeGraph,
+) : FlowAnalysis {
+
+ override fun newEntryFlow(): T = newFlow()
+
+ protected open fun merge(successor: NODE, income1: T, income2: T, outcome: T) {
+ merge(income1, income2, outcome)
+ }
+
+ open fun ins(s: NODE): T? {
+ return ins[s]
+ }
+
+ protected fun mergeInto(successor: NODE, input: T, incoming: T) {
+ val tmp = newFlow()
+ merge(successor, input, incoming, tmp)
+ copy(tmp, input)
+ }
+}
diff --git a/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/BackwardFlowAnalysis.kt b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/BackwardFlowAnalysis.kt
new file mode 100644
index 0000000000..55ef48d7e3
--- /dev/null
+++ b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/BackwardFlowAnalysis.kt
@@ -0,0 +1,28 @@
+/*
+ * Copyright 2022 UnitTestBot contributors (utbot.org)
+ *
+ * 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 org.usvm.dataflow.jvm.flow
+
+import org.jacodb.api.jvm.cfg.JcBytecodeGraph
+
+abstract class BackwardFlowAnalysis(graph: JcBytecodeGraph) : FlowAnalysisImpl(graph) {
+
+ override val isForward: Boolean = false
+
+ override fun run() {
+ runAnalysis(FlowAnalysisDirection.BACKWARD, outs, ins)
+ }
+}
diff --git a/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/FlowAnalysis.kt b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/FlowAnalysis.kt
new file mode 100644
index 0000000000..6a796b4f48
--- /dev/null
+++ b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/FlowAnalysis.kt
@@ -0,0 +1,32 @@
+/*
+ * Copyright 2022 UnitTestBot contributors (utbot.org)
+ *
+ * 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 org.usvm.dataflow.jvm.flow
+
+import org.jacodb.api.jvm.cfg.JcBytecodeGraph
+
+interface FlowAnalysis {
+ val ins: MutableMap
+ val outs: MutableMap
+ val graph: JcBytecodeGraph
+ val isForward: Boolean
+
+ fun newFlow(): T
+ fun newEntryFlow(): T
+ fun merge(in1: T, in2: T, out: T)
+ fun copy(source: T?, dest: T)
+ fun run()
+}
diff --git a/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/FlowAnalysisImpl.kt b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/FlowAnalysisImpl.kt
new file mode 100644
index 0000000000..b2c8896b2d
--- /dev/null
+++ b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/FlowAnalysisImpl.kt
@@ -0,0 +1,412 @@
+/*
+ * Copyright 2022 UnitTestBot contributors (utbot.org)
+ *
+ * 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 org.usvm.dataflow.jvm.flow
+
+import org.jacodb.api.jvm.cfg.JcBytecodeGraph
+import org.jacodb.api.jvm.cfg.JcGotoInst
+import java.util.ArrayDeque
+import java.util.Arrays
+import java.util.Deque
+import java.util.PriorityQueue
+
+enum class Flow {
+ IN {
+ override fun getFlow(e: FlowEntry): T? {
+ return e.inFlow
+ }
+ },
+ OUT {
+ override fun getFlow(e: FlowEntry): T? {
+ return e.outFlow
+ }
+ };
+
+ abstract fun getFlow(e: FlowEntry): T?
+}
+
+/**
+ * Creates a new `Entry` graph based on a `JcGraph`. This includes pseudo topological order, local
+ * access for predecessors and successors, a graph entry-point, connected component marker.
+ */
+private fun JcBytecodeGraph.newScope(
+ direction: FlowAnalysisDirection,
+ entryFlow: T,
+ isForward: Boolean,
+): List> {
+ val size = toList().size
+ val s = ArrayDeque>(size)
+ val scope = ArrayList>(size)
+ val visited = HashMap>((size + 1) * 4 / 3)
+
+ // out of scope node
+ val instructions: List?
+ val actualEntries = direction.entries(this)
+ if (actualEntries.isNotEmpty()) {
+ // normal cases: there is at least
+ // one return statement for a backward analysis
+ // or one entry statement for a forward analysis
+ instructions = actualEntries
+ } else {
+ // cases without any entry statement
+ if (isForward) {
+ // case of a forward flow analysis on
+ // a method without any entry point
+ throw RuntimeException("No entry point for method in forward analysis")
+ } else {
+ // case of backward analysis on
+ // a method which potentially has
+ // an infinite loop and no return statement
+ instructions = ArrayList()
+ val head = entries.first()
+
+ // collect all 'goto' statements to catch the 'goto' from the infinite loop
+ val visitedInst = HashSet()
+ val list = arrayListOf(head)
+ var temp: NODE
+ while (list.isNotEmpty()) {
+ temp = list.removeAt(0)
+ visitedInst.add(temp)
+
+ // only add 'goto' statements
+ if (temp is JcGotoInst) {
+ instructions.add(temp)
+ }
+ for (next in successors(temp)) {
+ if (visitedInst.contains(next)) {
+ continue
+ }
+ list.add(next)
+ }
+ }
+
+ if (instructions.isEmpty()) {
+ throw RuntimeException("Backward analysis on an empty entry set.")
+ }
+ }
+ }
+ val root = RootEntry()
+ root.visitEntry(instructions, visited)
+ root.inFlow = entryFlow
+ root.outFlow = entryFlow
+
+ val sv: Array?> = arrayOfNulls(size)
+ val si = IntArray(size)
+ var index = 0
+ var i = 0
+ var entry: FlowEntry = root
+ while (true) {
+ if (i < entry.outs.size) {
+ val next = entry.outs[i++]
+
+ // an unvisited child node
+ if (next.number == Int.MIN_VALUE) {
+ next.number = s.size
+ s.add(next)
+ next.visitEntry(direction.outOf(this, next.data), visited)
+
+ // save old
+ si[index] = i
+ sv[index] = entry
+ index++
+ i = 0
+ entry = next
+ }
+ } else {
+ if (index == 0) {
+ assert(scope.size <= size)
+ scope.reverse()
+ return scope
+ }
+ scope.add(entry)
+ s.pop(entry)
+
+ // restore old
+ index--
+ entry = sv[index]!!
+ i = si[index]
+ }
+ }
+}
+
+private fun FlowEntry.visitEntry(
+ instructions: List,
+ visited: MutableMap>,
+): Array> {
+ val n = instructions.size
+ return Array(n) {
+ instructions[it].toEntry(this, visited)
+ }.also {
+ outs = it
+ }
+}
+
+private fun NODE.toEntry(
+ pred: FlowEntry,
+ visited: MutableMap>,
+): FlowEntry {
+ // either we reach a new node or a merge node, the latter one is rare
+ // so put and restore should be better that a lookup
+
+ val newEntry = LeafEntry(this, pred)
+ val oldEntry = visited.putIfAbsent(this, newEntry) ?: return newEntry
+
+ // no restore required
+
+ // adding self ref (real strongly connected with itself)
+ if (oldEntry === pred) {
+ oldEntry.isStronglyConnected = true
+ }
+
+ // merge nodes are rare, so this is ok
+ val length = oldEntry.ins.size
+ oldEntry.ins = Arrays.copyOf(oldEntry.ins, length + 1)
+ oldEntry.ins[length] = pred
+ return oldEntry
+}
+
+private fun Deque>.pop(entry: FlowEntry) {
+ var min = entry.number
+ for (e in entry.outs) {
+ assert(e.number > Int.MIN_VALUE)
+ min = min.coerceAtMost(e.number)
+ }
+
+ // not our SCC
+ if (min != entry.number) {
+ entry.number = min
+ return
+ }
+
+ // we only want real SCCs (size > 1)
+ var last = removeLast()
+ last.number = Int.MAX_VALUE
+ if (last === entry) {
+ return
+ }
+ last.isStronglyConnected = true
+ while (true) {
+ last = removeLast()
+ assert(last.number >= entry.number)
+ last.isStronglyConnected = true
+ last.number = Int.MAX_VALUE
+ if (last === entry) {
+ assert(last.ins.size >= 2)
+ return
+ }
+ }
+}
+
+enum class FlowAnalysisDirection {
+ BACKWARD {
+ override fun entries(g: JcBytecodeGraph): List {
+ return g.exits
+ }
+
+ override fun outOf(g: JcBytecodeGraph, s: NODE): List {
+ return g.predecessors(s).toList()
+ }
+ },
+ FORWARD {
+ override fun entries(g: JcBytecodeGraph): List {
+ return g.entries
+ }
+
+ override fun outOf(g: JcBytecodeGraph, s: NODE): List {
+ return g.successors(s).toList()
+ }
+ };
+
+ abstract fun entries(g: JcBytecodeGraph): List
+ abstract fun outOf(g: JcBytecodeGraph, s: NODE): List
+}
+
+abstract class FlowEntry(pred: FlowEntry?) {
+
+ abstract val data: NODE
+
+ var number = Int.MIN_VALUE
+ var isStronglyConnected = false
+ var ins: Array> = pred?.let { arrayOf(pred) } ?: emptyArray()
+ var outs: Array> = emptyArray()
+ var inFlow: T? = null
+ var outFlow: T? = null
+
+ override fun toString(): String {
+ return data.toString()
+ }
+
+}
+
+class RootEntry : FlowEntry(null) {
+ override val data: NODE get() = throw IllegalStateException()
+}
+
+class LeafEntry(override val data: NODE, pred: FlowEntry?) : FlowEntry(pred)
+
+abstract class FlowAnalysisImpl(graph: JcBytecodeGraph) : AbstractFlowAnalysis(graph) {
+
+ protected abstract fun flowThrough(instIn: T?, ins: NODE, instOut: T)
+
+ fun outs(s: NODE): T {
+ return outs[s] ?: newFlow()
+ }
+
+ override fun ins(s: NODE): T {
+ return ins[s] ?: newFlow()
+ }
+
+ private fun Iterable>.initFlow() {
+ // If a node has only a single in-flow, the in-flow is always equal
+ // to the out-flow if its predecessor, so we use the same object.
+ // this saves memory and requires less object creation and copy calls.
+
+ // Furthermore a node can be marked as `canSkip`, this allows us to use
+ // the same "flow-set" for out-flow and in-flow. T merge node with within
+ // a real scc cannot be omitted, as it could cause endless loops within
+ // the fixpoint-iteration!
+ for (node in this) {
+ var omit = true
+ val inFlow: T
+ val outFlow: T
+
+ if (node.ins.size > 1) {
+ inFlow = newFlow()
+
+ // no merge points in loops
+ omit = !node.isStronglyConnected
+ } else {
+ assert(node.ins.size == 1) { "Missing head" }
+ val flow = getFlow(node.ins.first(), node)
+ assert(flow != null) { "Topological order is broken" }
+ inFlow = flow!!
+ }
+ if (omit && node.data.canSkip) {
+ // We could recalculate the graph itself but that is more expensive than
+ // just falling through such nodes.
+ outFlow = inFlow
+ } else {
+ outFlow = newFlow()
+ }
+ node.inFlow = inFlow
+ node.outFlow = outFlow
+
+ ins[node.data] = inFlow
+ outs[node.data] = outFlow
+ }
+ }
+
+ /**
+ * If a flow node can be skipped return `true`, otherwise `false`. There is no guarantee a node will
+ * be omitted. `canSkip` node does not influence the result of an analysis.
+ *
+ * If you are unsure, don't overwrite this method
+ */
+ protected open val NODE.canSkip: Boolean
+ get() {
+ return false
+ }
+
+ protected open fun getFlow(from: NODE, mergeNode: NODE) = Flow.OUT
+
+ private fun getFlow(o: FlowEntry, e: FlowEntry): T? {
+ return if (o.inFlow === o.outFlow) {
+ o.outFlow
+ } else {
+ getFlow(o.data, e.data).getFlow(o)
+ }
+ }
+
+ private fun FlowEntry.meetFlows() {
+ assert(ins.isNotEmpty())
+ if (ins.size > 1) {
+ var copy = true
+ for (o in ins) {
+ val flow = getFlow(o, this)
+ val inFlow = inFlow
+ if (flow != null && inFlow != null) {
+ if (copy) {
+ copy = false
+ copy(flow, inFlow)
+ } else {
+ mergeInto(data, inFlow, flow)
+ }
+ }
+ }
+ }
+ }
+
+ open fun runAnalysis(
+ direction: FlowAnalysisDirection,
+ inFlow: Map,
+ outFlow: Map,
+ ): Int {
+ val scope = graph.newScope(direction, newEntryFlow(), isForward).also {
+ it.initFlow()
+ }
+ val queue = PriorityQueue> { o1, o2 -> o1.number.compareTo(o2.number) }
+ .also { it.addAll(scope) }
+
+ // Perform fixed point flow analysis
+ var numComputations = 0
+ while (true) {
+ val entry = queue.poll() ?: return numComputations
+ entry.meetFlows()
+
+ val hasChanged = flowThrough(entry)
+
+ // Update queue appropriately
+ if (hasChanged) {
+ queue.addAll(entry.outs.toList())
+ }
+ numComputations++
+ }
+ }
+
+ private fun flowThrough(entry: FlowEntry): Boolean {
+ if (entry.inFlow === entry.outFlow) {
+ assert(!entry.isStronglyConnected || entry.ins.size == 1)
+ return true
+ }
+ if (entry.isStronglyConnected) {
+ // A flow node that is influenced by at least one back-reference.
+ // It's essential to check if "flowThrough" changes the result.
+ // This requires the calculation of "equals", which itself
+ // can be really expensive - depending on the used flow-model.
+ // Depending on the "merge"+"flowThrough" costs, it can be cheaper
+ // to fall through. Only nodes with real back-references always
+ // need to be checked for changes
+ val out = newFlow()
+ flowThrough(entry.inFlow, entry.data, out)
+ if (out == entry.outFlow) {
+ return false
+ }
+ // copy back the result, as it has changed
+ entry.outFlow?.let {
+ copy(out, it)
+ }
+ return true
+ }
+
+ // no back-references, just calculate "flowThrough"
+ val outFlow = entry.outFlow
+ if (outFlow != null) {
+ flowThrough(entry.inFlow, entry.data, outFlow)
+ }
+ return true
+ }
+
+}
diff --git a/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/ForwardFlowAnalysis.kt b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/ForwardFlowAnalysis.kt
new file mode 100644
index 0000000000..248b943199
--- /dev/null
+++ b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/ForwardFlowAnalysis.kt
@@ -0,0 +1,28 @@
+/*
+ * Copyright 2022 UnitTestBot contributors (utbot.org)
+ *
+ * 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 org.usvm.dataflow.jvm.flow
+
+import org.jacodb.api.jvm.cfg.JcBytecodeGraph
+
+abstract class ForwardFlowAnalysis(graph: JcBytecodeGraph) : FlowAnalysisImpl(graph) {
+
+ override val isForward = true
+
+ override fun run() {
+ runAnalysis(FlowAnalysisDirection.FORWARD, ins, outs)
+ }
+}
diff --git a/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/NullAssumptionAnalysis.kt b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/NullAssumptionAnalysis.kt
new file mode 100644
index 0000000000..08305bf506
--- /dev/null
+++ b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/NullAssumptionAnalysis.kt
@@ -0,0 +1,229 @@
+/*
+ * Copyright 2022 UnitTestBot contributors (utbot.org)
+ *
+ * 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 org.usvm.dataflow.jvm.flow
+
+import org.jacodb.api.jvm.JcRefType
+import org.jacodb.api.jvm.cfg.JcArrayAccess
+import org.jacodb.api.jvm.cfg.JcAssignInst
+import org.jacodb.api.jvm.cfg.JcCallExpr
+import org.jacodb.api.jvm.cfg.JcCastExpr
+import org.jacodb.api.jvm.cfg.JcEnterMonitorInst
+import org.jacodb.api.jvm.cfg.JcFieldRef
+import org.jacodb.api.jvm.cfg.JcGraph
+import org.jacodb.api.jvm.cfg.JcInst
+import org.jacodb.api.jvm.cfg.JcInstanceCallExpr
+import org.jacodb.api.jvm.cfg.JcLocal
+import org.jacodb.api.jvm.cfg.JcValue
+import org.jacodb.api.jvm.ext.cfg.arrayRef
+import org.jacodb.api.jvm.ext.cfg.callExpr
+import org.jacodb.api.jvm.ext.cfg.fieldRef
+
+class NullAnalysisMap : HashMap {
+
+ constructor() : super()
+ constructor(m: Map) : super(m)
+
+ override fun get(key: JcValue): NullableState {
+ return super.get(key) ?: NullableState.UNKNOWN
+ }
+}
+
+enum class NullableState {
+ UNKNOWN,
+ NULL,
+ NON_NULL;
+}
+
+/**
+ * An inter-procedural nullness assumption analysis that computes for each location and each value in a method if the value
+ * (before or after that location) is treated as definitely null, definitely non-null or neither. This information could be
+ * useful in deciding whether to insert code that accesses a potentially null object.
+ *
+ * If the original program assumes a value is non-null, then adding a use of that value will not introduce any NEW nullness
+ * errors into the program. This code may be buggy, or just plain wrong. It has not been checked.
+ */
+open class NullAssumptionAnalysis(graph: JcGraph) : BackwardFlowAnalysis(graph) {
+
+ override val ins: MutableMap = hashMapOf()
+ override val outs: MutableMap = hashMapOf()
+
+ override fun flowThrough(
+ instIn: NullAnalysisMap?,
+ ins: JcInst,
+ instOut: NullAnalysisMap,
+ ) {
+ val out = instIn?.let { NullAnalysisMap(it) } ?: NullAnalysisMap()
+
+ // programmer assumes we have a non-null value
+ if (ins is JcEnterMonitorInst) {
+ out[ins.monitor] = NullableState.NON_NULL
+ }
+
+ // if we have an array ref, set the info for this ref to TOP,
+ // because we need to be conservative here
+ ins.arrayRef?.let {
+ onArrayAccess(it, out)
+ }
+ // same for field refs, but also set the receiver object to non-null, if there is one
+ ins.fieldRef?.let {
+ onFieldRef(it, out)
+ }
+ // same for invoke expr., also set the receiver object to non-null, if there is one
+ ins.callExpr?.let {
+ onCallExpr(it, out)
+ }
+
+ // allow sub-classes to define certain values as always-non-null
+ for (entry in out.entries) {
+ if (isAlwaysNonNull(entry.key)) {
+ entry.setValue(NullableState.NON_NULL)
+ }
+ }
+
+ // if we have a definition (assignment) statement to a ref-like type, handle it,
+ if (ins is JcAssignInst) {
+ // need to copy the current out set because we need to assign under this assumption;
+ // so this copy becomes the in-set to handleRefTypeAssignment
+ if (ins.lhv.type is JcRefType) {
+ onRefTypeAssignment(ins, NullAnalysisMap(out), out)
+ }
+ }
+
+ // save memory by only retaining information about locals
+ val outIter = out.keys.iterator()
+ while (outIter.hasNext()) {
+ val v = outIter.next()
+ if (!(v is JcLocal)) {
+ outIter.remove()
+ }
+ }
+
+ // now copy the computed info to out
+ copy(out, instOut)
+ }
+
+ protected open fun isAlwaysNonNull(v: JcValue): Boolean {
+ return false
+ }
+
+ private fun onArrayAccess(arrayRef: JcArrayAccess, out: NullAnalysisMap) {
+ // here we know that the array must point to an object, but the array value might be anything
+ out[arrayRef.array] = NullableState.NON_NULL
+ }
+
+ private fun onFieldRef(fieldRef: JcFieldRef, out: NullAnalysisMap) {
+ // here we know that the receiver must point to an object
+ val instance = fieldRef.instance
+ if (instance != null) {
+ out[instance] = NullableState.NON_NULL
+ }
+ }
+
+ private fun onCallExpr(invokeExpr: JcCallExpr, out: NullAnalysisMap) {
+ if (invokeExpr is JcInstanceCallExpr) {
+ // here we know that the receiver must point to an object
+ out[invokeExpr.instance] = NullableState.NON_NULL
+ }
+ }
+
+ private fun onRefTypeAssignment(assignStmt: JcAssignInst, rhsInfo: NullAnalysisMap, out: NullAnalysisMap) {
+ val right = when (val rhv = assignStmt.rhv) {
+ is JcCastExpr -> rhv.operand
+ is JcValue -> rhv
+ else -> null
+ }
+ if (right != null) {
+
+ // An assignment invalidates any assumptions of null/non-null for lhs
+ // We COULD be more accurate by assigning those assumptions to the rhs prior to this statement
+ rhsInfo[right] = NullableState.UNKNOWN
+
+ // assign from rhs to lhs
+ out[assignStmt.lhv] = rhsInfo[right]
+ }
+ }
+
+ override fun copy(source: NullAnalysisMap?, dest: NullAnalysisMap) {
+ dest.clear()
+ if (source != null) {
+ dest.putAll(source)
+ }
+ }
+
+ override fun newEntryFlow(): NullAnalysisMap {
+ return NullAnalysisMap()
+ }
+
+ override fun newFlow(): NullAnalysisMap {
+ return NullAnalysisMap()
+ }
+
+ override fun merge(in1: NullAnalysisMap, in2: NullAnalysisMap, out: NullAnalysisMap) {
+ val values = HashSet()
+ values.addAll(in1.keys)
+ values.addAll(in2.keys)
+ out.clear()
+ for (v in values) {
+ val leftAndRight = HashSet()
+ leftAndRight.add(in1[v])
+ leftAndRight.add(in2[v])
+ val result = if (leftAndRight.contains(NullableState.UNKNOWN)) {
+ // if on either side we know nothing... then together we know nothing for sure
+ NullableState.UNKNOWN
+ } else if (leftAndRight.contains(NullableState.NON_NULL)) {
+ if (leftAndRight.contains(NullableState.NULL)) {
+ // NULL and NON_NULL merges to BOTTOM
+ NullableState.UNKNOWN
+ } else {
+ // NON_NULL and NON_NULL stays NON_NULL
+ NullableState.NON_NULL
+ }
+ } else if (leftAndRight.contains(NullableState.NULL)) {
+ // NULL and NULL stays NULL
+ NullableState.NULL
+ } else {
+ // only BOTTOM remains
+ NullableState.UNKNOWN
+ }
+ out[v] = result
+ }
+ }
+
+ /**
+ * Returns `true` if the analysis could determine that `value` is always treated as null after and including the instruction inst.
+ *
+ * @param inst instruction of the respective body
+ * @param value a local or constant value of that body
+ * @return true if value is always null right before this statement
+ */
+ fun isAssumedNullBefore(inst: JcInst, value: JcValue): Boolean {
+ return ins(inst)[value] == NullableState.NULL
+ }
+
+ /**
+ * Returns `true` if the analysis could determine that value is always treated as non-null after and including the
+ * statement s.
+ *
+ * @param inst instruction of the respective body
+ * @param value a local or constant value of that body
+ * @return true if value is always non-null right before this statement
+ */
+ fun isAssumedNonNullBefore(inst: JcInst, value: JcValue): Boolean {
+ return ins(inst)[value] == NullableState.NON_NULL
+ }
+
+}
diff --git a/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/ReachingDefinitionsAnalysis.kt b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/ReachingDefinitionsAnalysis.kt
new file mode 100644
index 0000000000..55bf8f8a2b
--- /dev/null
+++ b/usvm-jvm-dataflow/src/main/kotlin/org/usvm/dataflow/jvm/flow/ReachingDefinitionsAnalysis.kt
@@ -0,0 +1,105 @@
+/*
+ * Copyright 2022 UnitTestBot contributors (utbot.org)
+ *
+ * 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 org.usvm.dataflow.jvm.flow
+
+import org.jacodb.api.jvm.cfg.JcAssignInst
+import org.jacodb.api.jvm.cfg.JcBasicBlock
+import org.jacodb.api.jvm.cfg.JcGraph
+import org.jacodb.api.jvm.cfg.JcInst
+import org.jacodb.api.jvm.cfg.JcInstRef
+import org.jacodb.api.jvm.cfg.JcValue
+import org.jacodb.impl.cfg.JcBlockGraphImpl
+import java.util.BitSet
+
+class ReachingDefinitionsAnalysis(private val blockGraph: JcBlockGraphImpl) {
+
+ private val jcGraph: JcGraph
+ get() = blockGraph.jcGraph
+
+ private val nDefinitions = jcGraph.instructions.size
+ private val ins = mutableMapOf()
+ private val outs = mutableMapOf()
+ private val assignmentsMap = mutableMapOf>()
+
+ init {
+ initAssignmentsMap()
+ val entry = blockGraph.entry
+ for (block in blockGraph) {
+ outs[block] = emptySet()
+ }
+
+ val queue = ArrayDeque().also { it += entry }
+ val notVisited = blockGraph.toMutableSet()
+ while (queue.isNotEmpty() || notVisited.isNotEmpty()) {
+ val current = when {
+ queue.isNotEmpty() -> queue.removeFirst()
+ else -> notVisited.random()
+ }
+ notVisited -= current
+
+ ins[current] = fullPredecessors(current).map { outs[it]!! }.fold(emptySet()) { acc, bitSet ->
+ acc.or(bitSet)
+ acc
+ }
+
+ val oldOut = outs[current]!!.clone() as BitSet
+ val newOut = gen(current)
+
+ if (oldOut != newOut) {
+ outs[current] = newOut
+ for (successor in fullSuccessors(current)) {
+ queue += successor
+ }
+ }
+ }
+ }
+
+ private fun initAssignmentsMap() {
+ for (inst in jcGraph) {
+ if (inst is JcAssignInst) {
+ assignmentsMap.getOrPut(inst.lhv, ::mutableSetOf) += jcGraph.ref(inst)
+ }
+ }
+ }
+
+ private fun emptySet(): BitSet = BitSet(nDefinitions)
+
+ private fun gen(block: JcBasicBlock): BitSet {
+ val inSet = ins[block]!!.clone() as BitSet
+ for (inst in blockGraph.instructions(block)) {
+ if (inst is JcAssignInst) {
+ for (kill in assignmentsMap.getOrDefault(inst.lhv, mutableSetOf())) {
+ inSet[kill] = false
+ }
+ inSet[jcGraph.ref(inst)] = true
+ }
+ }
+ return inSet
+ }
+
+ private fun fullPredecessors(block: JcBasicBlock) = blockGraph.predecessors(block) + blockGraph.throwers(block)
+ private fun fullSuccessors(block: JcBasicBlock) = blockGraph.successors(block) + blockGraph.catchers(block)
+
+ private operator fun BitSet.set(ref: JcInstRef, value: Boolean) {
+ this.set(ref.index, value)
+ }
+
+ fun outs(block: JcBasicBlock): List {
+ val defs = outs.getOrDefault(block, emptySet())
+ return (0 until nDefinitions).filter { defs[it] }.map { jcGraph.instructions[it] }
+ }
+}
diff --git a/usvm-jvm-dataflow/src/samples/java/NullAssumptionAnalysisExample.java b/usvm-jvm-dataflow/src/samples/java/NullAssumptionAnalysisExample.java
new file mode 100644
index 0000000000..abdcec3540
--- /dev/null
+++ b/usvm-jvm-dataflow/src/samples/java/NullAssumptionAnalysisExample.java
@@ -0,0 +1,29 @@
+/*
+ * Copyright 2022 UnitTestBot contributors (utbot.org)
+ *
+ * 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.
+ */
+
+public class NullAssumptionAnalysisExample {
+ public void test1(String a) {
+ System.out.println("Hello from test1");
+ System.out.println(a.length());
+ }
+
+ public void test2(Object a) {
+ System.out.println("Hello from test2");
+ System.out.println(a.hashCode());
+ String x = (String) a;
+ System.out.println(x.length());
+ }
+}
diff --git a/usvm-jvm-dataflow/src/test/kotlin/org/usvm/dataflow/jvm/impl/NullabilityAssumptionAnalysisTest.kt b/usvm-jvm-dataflow/src/test/kotlin/org/usvm/dataflow/jvm/impl/NullabilityAssumptionAnalysisTest.kt
new file mode 100644
index 0000000000..3d4bad0591
--- /dev/null
+++ b/usvm-jvm-dataflow/src/test/kotlin/org/usvm/dataflow/jvm/impl/NullabilityAssumptionAnalysisTest.kt
@@ -0,0 +1,69 @@
+/*
+ * Copyright 2022 UnitTestBot contributors (utbot.org)
+ *
+ * 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 org.usvm.dataflow.jvm.impl
+
+import NullAssumptionAnalysisExample
+import org.jacodb.api.jvm.JcClassOrInterface
+import org.jacodb.api.jvm.JcMethod
+import org.jacodb.api.jvm.cfg.JcAssignInst
+import org.jacodb.api.jvm.cfg.JcInstanceCallExpr
+import org.jacodb.api.jvm.cfg.JcLocal
+import org.jacodb.api.jvm.ext.findClass
+import org.junit.jupiter.api.Assertions.assertTrue
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.TestInstance
+import org.junit.jupiter.api.TestInstance.Lifecycle.PER_CLASS
+import org.usvm.dataflow.jvm.flow.NullAssumptionAnalysis
+
+@TestInstance(PER_CLASS)
+class NullabilityAssumptionAnalysisTest : BaseAnalysisTest() {
+
+ @Test
+ fun `null-assumption analysis should work`() {
+ val clazz = cp.findClass()
+ with(clazz.findMethod("test1").flowGraph()) {
+ val analysis = NullAssumptionAnalysis(this).also {
+ it.run()
+ }
+ val sout = (instructions[0] as JcAssignInst).lhv as JcLocal
+ val a = ((instructions[3] as JcAssignInst).rhv as JcInstanceCallExpr).instance
+
+ assertTrue(analysis.isAssumedNonNullBefore(instructions[2], a))
+ assertTrue(analysis.isAssumedNonNullBefore(instructions[0], sout))
+ }
+ }
+
+ @Test
+ fun `null-assumption analysis should work 2`() {
+ val clazz = cp.findClass()
+ with(clazz.findMethod("test2").flowGraph()) {
+ val analysis = NullAssumptionAnalysis(this).also {
+ it.run()
+ }
+ val sout = (instructions[0] as JcAssignInst).lhv as JcLocal
+ val a = ((instructions[3] as JcAssignInst).rhv as JcInstanceCallExpr).instance
+ val x = (instructions[5] as JcAssignInst).lhv as JcLocal
+
+ assertTrue(analysis.isAssumedNonNullBefore(instructions[2], a))
+ assertTrue(analysis.isAssumedNonNullBefore(instructions[0], sout))
+ analysis.isAssumedNonNullBefore(instructions[5], x)
+ }
+ }
+
+ private fun JcClassOrInterface.findMethod(name: String): JcMethod = declaredMethods.first { it.name == name }
+
+}