Data Structure Analysis #222

sadrabt · 2024-07-01T02:17:40Z

Adapted version of DSA for BASIL

includes symbolic access analysis and a reaching definitions analysis that works slightly differently from the one already implemented. (registers changed by a procedure call are defined by the call instruction)

l-kent · 2024-07-01T03:36:01Z

I'm a bit confused by the commit history here - some of Yousif's commits that are not ready to merge in yet have been included, but then later reverted? Is there a neater way to do things than that?

src/main/scala/translating/ReadELFLoader.scala

src/main/scala/analysis/SymbolicAccessAnalysis.scala

src/main/scala/analysis/solvers/IDESolver.scala

src/main/scala/util/RunUtils.scala

src/test/scala/RegionBuilderTests.scala

src/main/scala/analysis/InterprocSteensgaardAnalysis.scala

src/main/scala/analysis/Local.scala

l-kent · 2024-07-07T23:10:33Z

It'll take some time to get across all the details of this, so detailed comments would really help to make it easier to understand.

One thing that makes the code more difficult to follow at the moment is the widespread use of tuples - is it possible that replacing those with case classes would make sense?

src/main/scala/analysis/SymbolicAccessAnalysis.scala

src/main/scala/analysis/Local.scala

src/main/scala/analysis/BitVectorEval.scala

src/main/scala/analysis/DSAUtility.scala

l-kent · 2024-08-05T05:52:05Z

src/test/scala/LocalTest.scala

+import specification.Specification
+import util.{BASILConfig, BoogieGeneratorConfig, ILLoadingConfig, IRContext, RunUtils, StaticAnalysisConfig}
+
+class LocalTest extends AnyFunSuite, TestUtil {


Rather than 'LocalTest' wouldn't the name DSATest be clearer for this file & class?

l-kent · 2024-08-05T05:54:49Z

src/test/scala/LocalTest.scala

+  ignore("local jumptable2_clang main") {
+    val results = RunUtils.loadAndTranslate(
+      BASILConfig(
+        loading = ILLoadingConfig(
+          inputFile = "examples/jumptable2/jumptable2_clang.adt",
+          relfFile = "examples/jumptable2/jumptable2_clang.relf",
+          specFile = None,
+          dumpIL = None,
+        ),
+        staticAnalysis = Some(StaticAnalysisConfig()),
+        boogieTranslation = BoogieGeneratorConfig(),
+        outputPrefix = "boogie_out",
+      )
+    )
+    val program = results.ir.program
+    val dsg = results.analysis.get.locals.get(program.mainProcedure)
+//    assert(dsg.pointTo.size == 7)
+//    assert(dsg.stackMapping.isEmpty)
+//    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69680, 69684))._1.cells(0))._1.node.get.collapsed)
+  }
+
+
+
+
+  ignore("interproc unsafe pointer arithmetic") {
+    // test interproc unification with points-to that have internal offsets into cells
+  }


Are these needed for anything? Should they be removed?

l-kent · 2024-08-05T05:59:03Z

src/test/scala/LocalTest.scala

+    assert(dsg.pointTo.size == 9)
+    assert(dsg.stackMapping.isEmpty)
+    println(dsg.globalMapping(AddressRange(69648, 69652))._1.cells(0))
+    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69648, 69652))._1.cells(0))._1.node.get.collapsed)
+
+    // initial global mappings
+    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69600, 69608))._1.cells(0))._1.equals(dsg.globalMapping(AddressRange(2136, 2136 + 124))._1.cells(0)))
+    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69656, 69656 + 24))._1.cells(0))._1.equals(dsg.globalMapping(AddressRange(1948, 1948 + 36))._1.cells(0)))
+    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69624, 69632))._1.cells(0))._1.equals(dsg.globalMapping(AddressRange(69656, 69656 + 24))._1.cells(0)))
+    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69608, 69616))._1.cells(0))._1.equals(dsg.globalMapping(AddressRange(2056, 2056 + 76))._1.cells(0)))
+    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69608, 69616))._1.cells(0))._1.equals(dsg.globalMapping(AddressRange(2056, 2056 + 76))._1.cells(0)))
+    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69656, 69656 + 24))._1.cells(8))._1.equals(dsg.globalMapping(AddressRange(1984, 1984 + 36))._1.cells(0)))
+    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69560, 69568))._1.cells(0))._1.equals(dsg.globalMapping(AddressRange(2264, 2268))._1.cells(0)))
+    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69656, 69656 + 24))._1.cells(16))._1.equals(dsg.globalMapping(AddressRange(2020, 2020 + 36))._1.cells(0)))
+    assert(dsg.pointTo(dsg.globalMapping(AddressRange(69584, 69584 + 8))._1.cells(0))._1.equals(dsg.globalMapping(AddressRange(69648, 69648 + 4))._1.cells(0)))


It's a bit hard to follow exactly what any of these tests are actually testing - comments for each assertion would be extremely useful and it would help if the tuple accesses could be replaced with the name of the fields. Accessing case classes as if they are tuples is a very obscure feature of Scala and makes the code very difficult to follow.

l-kent · 2024-08-05T06:12:26Z

src/main/scala/analysis/DSAUtility.scala

+  // determine if an address is a global and return the corresponding global if it is.
+  def isGlobal(address: BigInt): Option[(AddressRange, Field)] =
+    var global: Option[(AddressRange, Field)]  = None


This is another case that would benefit from using a case class instead of a tuple

src/main/scala/util/RunUtils.scala

l-kent · 2024-08-06T04:05:15Z

src/main/scala/util/RunUtils.scala

+      IRconstPropResult = analysisResult.last.IRconstPropResult,
+      memoryRegionResult = analysisResult.last.memoryRegionResult,
+      vsaResult = analysisResult.last.vsaResult,
+      interLiveVarsResults = analysisResult.last.interLiveVarsResults,


I don't think this analysis is ever actually run so you may want to re-enable it where it makes sense to

sadrabt requested a review from l-kent July 1, 2024 03:17