Merge pull request #324 from csanadtelbisz/oc-optimizer-fix

Xcfa oc checker optimization fix

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.8.3"
+    version = "6.8.4"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java

@@ -743,6 +743,10 @@ public Expr<?> visitGccPrettyFunc(CParser.GccPrettyFuncContext ctx) {
     @Override
     public Expr<?> visitPrimaryExpressionId(CParser.PrimaryExpressionIdContext ctx) {
         final var variable = getVar(ctx.Identifier().getText());
+        if (atomicVars.contains(variable)) {
+            preStatements.add(new CCall("__VERIFIER_atomic_begin", List.of(), parseContext));
+            postStatements.add(new CCall("__VERIFIER_atomic_end", List.of(), parseContext));
+        }
         return variable.getRef();
     }
 
@@ -983,7 +987,7 @@ public Function<Expr<?>, Expr<?>> visitPostfixExpressionIncrement(
                 cexpr = new CExpr(expr, parseContext);
                 // no need to truncate here, as left and right side types are the same
                 CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext);
-                postStatements.add(cAssignment);
+                postStatements.add(0, cAssignment);
                 functionVisitor.recordMetadata(ctx, cAssignment);
                 functionVisitor.recordMetadata(ctx, cexpr);
                 return primary;
@@ -1004,7 +1008,7 @@ public Function<Expr<?>, Expr<?>> visitPostfixExpressionDecrement(
                 cexpr = new CExpr(expr, parseContext);
                 // no need to truncate here, as left and right side types are the same
                 CAssignment cAssignment = new CAssignment(primary, cexpr, "=", parseContext);
-                postStatements.add(cAssignment);
+                postStatements.add(0, cAssignment);
                 functionVisitor.recordMetadata(ctx, cAssignment);
                 functionVisitor.recordMetadata(ctx, cexpr);
                 return expr;

subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt

@@ -768,7 +768,9 @@ class FrontendXcfaBuilder(
       xcfaEdge = XcfaEdge(elseEnd, endLoc, metadata = getMetadata(statement))
       builder.addEdge(xcfaEdge)
     } else {
-      xcfaEdge = XcfaEdge(elseBranch, endLoc, metadata = getMetadata(statement))
+      val elseAfterGuard =
+        buildPostStatement(guard, ParamPack(builder, elseBranch, breakLoc, continueLoc, returnLoc))
+      xcfaEdge = XcfaEdge(elseAfterGuard, endLoc, metadata = getMetadata(statement))
       builder.addEdge(xcfaEdge)
     }
     xcfaEdge = XcfaEdge(mainEnd, endLoc, metadata = getMetadata(statement))

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt

@@ -25,6 +25,7 @@ import hu.bme.mit.theta.analysis.algorithm.oc.OcChecker
 import hu.bme.mit.theta.analysis.algorithm.oc.Relation
 import hu.bme.mit.theta.analysis.algorithm.oc.RelationType
 import hu.bme.mit.theta.analysis.unit.UnitPrec
+import hu.bme.mit.theta.common.exception.NotSolvableException
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.core.decl.ConstDecl
 import hu.bme.mit.theta.core.decl.Decls
@@ -50,21 +51,25 @@ import hu.bme.mit.theta.solver.SolverStatus
 import hu.bme.mit.theta.xcfa.*
 import hu.bme.mit.theta.xcfa.analysis.XcfaPrec
 import hu.bme.mit.theta.xcfa.model.*
+import hu.bme.mit.theta.xcfa.passes.*
 import kotlin.time.measureTime
 
 private val Expr<*>.vars
   get() = ExprUtils.getVars(this)
 
 class XcfaOcChecker(
-  private val xcfa: XCFA,
+  xcfa: XCFA,
   decisionProcedure: OcDecisionProcedureType,
   private val logger: Logger,
   conflictInput: String?,
   private val outputConflictClauses: Boolean,
   nonPermissiveValidation: Boolean,
   private val autoConflictConfig: AutoConflictFinderConfig,
+  private val acceptUnreliableSafe: Boolean = false,
 ) : SafetyChecker<EmptyProof, Cex, XcfaPrec<UnitPrec>> {
 
+  private val xcfa = xcfa.optimizeFurther(OcExtraPasses())
+
   private var indexing = VarIndexingFactory.indexing(0)
   private val localVars = mutableMapOf<VarDecl<*>, MutableMap<Int, VarDecl<*>>>()
   private val memoryDecl = Decls.Var("__oc_checker_memory_declaration__", Int())
@@ -147,7 +152,16 @@ class XcfaOcChecker(
           else -> SafetyResult.unknown()
         }
       }
-      .also { logger.writeln(Logger.Level.MAINSTEP, "OC checker result: $it") }
+      .also {
+        logger.writeln(Logger.Level.MAINSTEP, "OC checker result: $it")
+        if (xcfa.unsafeUnrollUsed && !acceptUnreliableSafe) {
+          logger.writeln(
+            Logger.Level.MAINSTEP,
+            "Incomplete loop unroll used: safe result is unreliable.",
+          )
+          throw NotSolvableException()
+        }
+      }
 
   private inner class ThreadProcessor(private val thread: Thread) {
 

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToOcChecker.kt

@@ -42,6 +42,7 @@ fun getOcChecker(
       ocConfig.outputConflictClauses,
       ocConfig.nonPermissiveValidation,
       ocConfig.autoConflict,
+      config.outputConfig.acceptUnreliableSafe,
     )
   return SafetyChecker { ocChecker.check() }
 }

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/portfolio/complex25.kt

@@ -46,7 +46,6 @@ import hu.bme.mit.theta.xcfa.cli.params.Refinement.SEQ_ITP
 import hu.bme.mit.theta.xcfa.cli.params.Search.*
 import hu.bme.mit.theta.xcfa.cli.runConfig
 import hu.bme.mit.theta.xcfa.model.XCFA
-import hu.bme.mit.theta.xcfa.model.optimizeFurther
 import hu.bme.mit.theta.xcfa.passes.*
 import java.nio.file.Paths
 
@@ -124,20 +123,9 @@ fun complexPortfolio25(
       debugConfig = portfolioConfig.debugConfig,
     )
 
-  val forceUnrolledXcfa =
-    xcfa.optimizeFurther(
-      listOf(
-        AssumeFalseRemovalPass(),
-        MutexToVarPass(),
-        AtomicReadsOneWritePass(),
-        LoopUnrollPass(2),
-      )
-    )
-
   val ocConfig = { inProcess: Boolean ->
     XcfaConfig(
-      inputConfig =
-        baseConfig.inputConfig.copy(xcfaWCtx = Triple(forceUnrolledXcfa, mcm, parseContext)),
+      inputConfig = baseConfig.inputConfig.copy(xcfaWCtx = Triple(xcfa, mcm, parseContext)),
       frontendConfig = baseConfig.frontendConfig,
       backendConfig =
         BackendConfig(

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/gson/XcfaAdapter.kt

@@ -98,7 +98,7 @@ class XcfaAdapter(val gsonSupplier: () -> Gson) : TypeAdapter<XCFA>() {
     lateinit var vars: Set<XcfaGlobalVar>
     lateinit var xcfaProcedures: Map<String, XcfaProcedure>
     lateinit var initProcedures: List<Pair<XcfaProcedure, List<Expr<*>>>>
-    var unsafeUnrollUsed: Boolean = false
+    var unsafeUnrollUsed = false
 
     val varsType = object : TypeToken<Set<XcfaGlobalVar>>() {}.type
 

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt

@@ -34,7 +34,6 @@ constructor(
   private val procedures: MutableSet<XcfaProcedureBuilder> = LinkedHashSet(),
   private val initProcedures: MutableList<Pair<XcfaProcedureBuilder, List<Expr<*>>>> = ArrayList(),
   val metaData: MutableMap<String, Any> = LinkedHashMap(),
-  var unsafeUnrollUsed: Boolean = false,
 ) {
 
   fun getVars(): Set<XcfaGlobalVar> = vars
@@ -49,7 +48,6 @@ constructor(
       globalVars = vars,
       procedureBuilders = procedures,
       initProcedureBuilders = initProcedures,
-      unsafeUnrollUsed = unsafeUnrollUsed,
     )
   }
 
@@ -80,6 +78,7 @@ constructor(
   private val locs: MutableSet<XcfaLocation> = LinkedHashSet(),
   private val edges: MutableSet<XcfaEdge> = LinkedHashSet(),
   val metaData: MutableMap<String, Any> = LinkedHashMap(),
+  unsafeUnrollUsed: Boolean = false,
 ) {
 
   lateinit var initLoc: XcfaLocation
@@ -91,6 +90,9 @@ constructor(
   var errorLoc: Optional<XcfaLocation> = Optional.empty()
     private set
 
+  var unsafeUnrollUsed: Boolean = unsafeUnrollUsed
+    private set
+
   lateinit var parent: XcfaBuilder
   private lateinit var built: XcfaProcedure
   private lateinit var optimized: XcfaProcedureBuilder
@@ -322,6 +324,6 @@ constructor(
   }
 
   fun setUnsafeUnroll() {
-    parent.unsafeUnrollUsed = true
+    unsafeUnrollUsed = true
   }
 }

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XCFA.kt

@@ -26,12 +26,12 @@ class XCFA(
   val globalVars: Set<XcfaGlobalVar>, // global variables
   val procedureBuilders: Set<XcfaProcedureBuilder> = emptySet(),
   val initProcedureBuilders: List<Pair<XcfaProcedureBuilder, List<Expr<*>>>> = emptyList(),
-  val unsafeUnrollUsed: Boolean = false,
+  var unsafeUnrollUsed: Boolean = false,
 ) {
 
-  val pointsToGraph by this.lazyPointsToGraph
+  private var cachedHash: Int? = null
 
-  var cachedHash: Int? = null
+  val pointsToGraph by this.lazyPointsToGraph
 
   var procedures: Set<XcfaProcedure> // procedure definitions
     private set
@@ -51,6 +51,8 @@ class XCFA(
 
     procedures = procedureBuilders.map { it.build(this) }.toSet()
     initProcedures = initProcedureBuilders.map { Pair(it.first.build(this), it.second) }
+    unsafeUnrollUsed =
+      (procedureBuilders + initProcedureBuilders.map { it.first }).any { it.unsafeUnrollUsed }
   }
 
   /** Recreate an existing XCFA by substituting the procedures and initProcedures fields. */

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaFurtherOptimizer.kt

@@ -15,22 +15,20 @@
  */
 package hu.bme.mit.theta.xcfa.model
 
-import hu.bme.mit.theta.xcfa.passes.ProcedurePass
 import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager
 
-fun XCFA.optimizeFurther(passes: List<ProcedurePass>): XCFA {
-  if (passes.isEmpty()) return this
-  val passManager = ProcedurePassManager(passes)
-  val copy: XcfaProcedureBuilder.() -> XcfaProcedureBuilder = {
-    val newLocs = getLocs().associateWith { it.copy() }
+fun XCFA.optimizeFurther(passManager: ProcedurePassManager): XCFA {
+  if (passManager.passes.isEmpty()) return this
+  val deepCopy: XcfaProcedure.() -> XcfaProcedureBuilder = {
+    val newLocs = locs.associateWith { it.copy() }
     XcfaProcedureBuilder(
         name = name,
         manager = passManager,
-        params = getParams().toMutableList(),
-        vars = getVars().toMutableSet(),
-        locs = getLocs().map { newLocs[it]!! }.toMutableSet(),
+        params = params.toMutableList(),
+        vars = vars.toMutableSet(),
+        locs = locs.map { newLocs[it]!! }.toMutableSet(),
         edges =
-          getEdges()
+          edges
             .map {
               val source = newLocs[it.source]!!
               val target = newLocs[it.target]!!
@@ -40,10 +38,11 @@ fun XCFA.optimizeFurther(passes: List<ProcedurePass>): XCFA {
               edge
             }
             .toMutableSet(),
-        metaData = metaData.toMutableMap(),
+        metaData = mutableMapOf(),
+        unsafeUnrollUsed = unsafeUnrollUsed,
       )
-      .also {
-        it.copyMetaLocs(
+      .also { proc ->
+        proc.copyMetaLocs(
           newLocs[initLoc]!!,
           finalLoc.map { newLocs[it] },
           errorLoc.map { newLocs[it] },
@@ -52,9 +51,9 @@ fun XCFA.optimizeFurther(passes: List<ProcedurePass>): XCFA {
   }
 
   val builder = XcfaBuilder(name, globalVars.toMutableSet())
-  procedureBuilders.forEach { builder.addProcedure(it.copy()) }
-  initProcedureBuilders.forEach { (proc, params) ->
-    val initProc = builder.getProcedures().find { it.name == proc.name } ?: proc.copy()
+  procedures.forEach { builder.addProcedure(it.deepCopy()) }
+  initProcedures.forEach { (proc, params) ->
+    val initProc = builder.getProcedures().find { it.name == proc.name } ?: proc.deepCopy()
     builder.addEntryPoint(initProc, params)
   }
   return builder.build()

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt

@@ -18,9 +18,9 @@ package hu.bme.mit.theta.xcfa.passes
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.frontend.ParseContext
 
-open class ProcedurePassManager(vararg passes: List<ProcedurePass>) {
+open class ProcedurePassManager(val passes: List<List<ProcedurePass>>) {
 
-  val passes: List<List<ProcedurePass>> = passes.toList()
+  constructor(vararg passes: List<ProcedurePass>) : this(passes.toList())
 }
 
 class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningLogger: Logger) :
@@ -52,7 +52,7 @@ class CPasses(checkOverflow: Boolean, parseContext: ParseContext, uniqueWarningL
       // trying to inline procedures
       InlineProceduresPass(parseContext),
       EmptyEdgeRemovalPass(),
-      RemoveDeadEnds(),
+      RemoveDeadEnds(parseContext),
       EliminateSelfLoops(),
     ),
     listOf(StaticCoiPass()),
@@ -87,7 +87,7 @@ class ChcPasses(parseContext: ParseContext, uniqueWarningLogger: Logger) :
     listOf(
       // trying to inline procedures
       InlineProceduresPass(parseContext),
-      RemoveDeadEnds(),
+      RemoveDeadEnds(parseContext),
       EliminateSelfLoops(),
       // handling remaining function calls
       LbePass(parseContext),
@@ -99,3 +99,13 @@ class ChcPasses(parseContext: ParseContext, uniqueWarningLogger: Logger) :
   )
 
 class LitmusPasses : ProcedurePassManager()
+
+class OcExtraPasses :
+  ProcedurePassManager(
+    listOf(
+      AssumeFalseRemovalPass(),
+      MutexToVarPass(),
+      AtomicReadsOneWritePass(),
+      LoopUnrollPass(2), // force loop unroll for BMC
+    )
+  )