Added comment on assumptions and dereferences

ftsrg · Nov 13, 2024 · 82efcc2 · 82efcc2
1 parent 3165862
commit 82efcc2
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 6 deletions.
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
@@ -243,7 +243,7 @@ private fun backend(
         exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) {
             checker.check()
           }
-          .let { result ->
+          .let ResultMapper@{ result ->
             when {
               result.isSafe && xcfa.unsafeUnrollUsed -> {
                 // cannot report safe if force unroll was used
@@ -263,18 +263,27 @@ private fun backend(
                       trace
                         ?.states
                         ?.asReversed()
-                        ?.getOrNull(1)
+                        ?.firstOrNull {
+                          it.processes.values.any { it.locs.any { it.name.contains("__THETA_") } }
+                        }
                         ?.processes
                         ?.values
-                        ?.firstOrNull()
+                        ?.firstOrNull { it.locs.any { it.name.contains("__THETA_") } }
                         ?.locs
-                        ?.firstOrNull()
+                        ?.firstOrNull { it.name.contains("__THETA_") }
                         ?.name
                         ?.let {
                           when (it) {
                             "__THETA_bad_free" -> "valid-free"
                             "__THETA_bad_deref" -> "valid-deref"
-                            "__THETA_lost" -> "valid-memtrack"
+                            "__THETA_lost" ->
+                              if (config.inputConfig.property == ErrorDetection.MEMCLEANUP)
+                                "valid-memcleanup"
+                              else
+                                "valid-memtrack"
+                                  .also { // this is not an exact check.
+                                    return@ResultMapper SafetyResult.unknown<EmptyProof, EmptyCex>()
+                                  }
                             else ->
                               throw RuntimeException(
                                 "Something went wrong; could not determine subproperty! Named location: $it"

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt
@@ -149,7 +149,9 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass {
       ) {
         builder.removeEdge(edge)
         edges.forEach {
-          if (deref((it.label as SequenceLabel).labels[0])) {
+          if (
+            deref((it.label as SequenceLabel).labels[0])
+          ) { // if dereference is in a short-circuiting path, add prior assumptions as well.
             val derefAssume =
               Assume(
                 Or(