Merge pull request #321 from ftsrg/portfolio-update

Portfolio update
ftsrg · Nov 12, 2024 · 35fd050 · 35fd050
2 parents f042054 + baae8cd
commit 35fd050
Show file tree

Hide file tree

Showing 25 changed files with 1,735 additions and 82 deletions.
diff --git a/.github/actions/benchexec-test/theta.xml b/.github/actions/benchexec-test/theta.xml
@@ -1,6 +1,6 @@
 <?xml version="1.0"?>
 <!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-2.3.dtd">
-<benchmark tool="theta" timelimit="20 s" hardtimelimit="30 s">
+<benchmark tool="theta" timelimit="40 s" hardtimelimit="60 s">
 
   <resultfiles>**/witness.*</resultfiles>
 

diff --git a/.github/actions/create-release/action.yml b/.github/actions/create-release/action.yml
@@ -40,6 +40,14 @@ runs:
       with:
         name: Theta_SV-COMP
         path: upload/
+    - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v3.0.2
+      with:
+        name: EmergenTheta_SV-COMP
+        path: upload/
+    - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v3.0.2
+      with:
+        name: Thorn_SV-COMP
+        path: upload/
     - run: for i in $(find jar -name "*-all.jar"); do mv -v $i upload/$(basename ${i%-${{steps.value.outputs.version}}-all.jar}.jar); done
       shell: bash
     - name: Release

diff --git a/.github/workflows/linux-build-test-deploy.yml b/.github/workflows/linux-build-test-deploy.yml
@@ -129,7 +129,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-latest, ubuntu-22.04]
+        os: [ubuntu-latest]
     needs: build
     runs-on: ${{ matrix.os }}
     steps:

diff --git a/build.gradle.kts b/build.gradle.kts
@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.8.1"
+    version = "6.8.2"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/common/grammar/src/main/antlr/CommonTokens.g4 b/subprojects/common/grammar/src/main/antlr/CommonTokens.g4
@@ -101,9 +101,6 @@ MINUS
 	:	'-'
 	;
 
-MUL	:	'*'
-	;
-
 DIV	:	'div'
 	;
 
@@ -406,7 +403,10 @@ SIGN:	PLUS | MINUS
 DOT	:	'.'
 	;
 
-ID	:	(LETTER | UNDERSCORE) (LETTER | UNDERSCORE | '$' | DIGIT | COLON)*
+ID	:	(LETTER | UNDERSCORE) (LETTER | UNDERSCORE | '$' | '*' | DIGIT | COLON)*
+	;
+
+MUL	:	'*'
 	;
 
 UNDERSCORE

diff --git a/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt b/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt
@@ -65,6 +65,7 @@ class ExprTest {
     fun data(): Collection<Array<Any>> {
       val x = Var("x", Int())
       val p = Param("p", Int())
+      val casret = Var("thr1::casret*", Int())
 
       val bvLit1 = Bv(BooleanArray(4) { it % 2 == 0 })
       val bvLit2 = Bv(BooleanArray(4) { it % 2 == 1 })
@@ -286,6 +287,11 @@ class ExprTest {
           emptyMap<Symbol, Decl<*>>(),
         ),
         arrayOf(Dereference(Int(0), Int(1), Int()), "(deref 0 1 Int)", emptyMap<Symbol, Decl<*>>()),
+        arrayOf(
+          Dereference(casret.ref, Int(0), Int()),
+          "(deref thr1::casret* 0 Int)",
+          mapOf(Pair(NamedSymbol("thr1::casret*"), casret)),
+        ),
       )
     }
   }

diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/Utils.kt
@@ -34,7 +34,9 @@ fun <K, V> Map<K, V>.reverseMapping() = this.entries.associate { it.value to it.
 fun Valuation.changeVars(varLut: Map<out Decl<*>, VarDecl<*>>): Valuation {
   val builder = ImmutableValuation.builder()
   for (decl in this.decls) {
-    builder.put(decl.changeVars(varLut), this.eval(decl).get())
+    if (decl in varLut) {
+      builder.put(decl.changeVars(varLut), this.eval(decl).get())
+    }
   }
   return builder.build()
 }

diff --git a/...jects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/...jects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt
@@ -50,16 +50,13 @@ 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.AssumeFalseRemovalPass
-import hu.bme.mit.theta.xcfa.passes.AtomicReadsOneWritePass
-import hu.bme.mit.theta.xcfa.passes.MutexToVarPass
 import kotlin.time.measureTime
 
 private val Expr<*>.vars
   get() = ExprUtils.getVars(this)
 
 class XcfaOcChecker(
-  xcfa: XCFA,
+  private val xcfa: XCFA,
   decisionProcedure: OcDecisionProcedureType,
   private val logger: Logger,
   conflictInput: String?,
@@ -68,10 +65,6 @@ class XcfaOcChecker(
   private val autoConflictConfig: AutoConflictFinderConfig,
 ) : SafetyChecker<EmptyProof, Cex, XcfaPrec<UnitPrec>> {
 
-  private val xcfa: XCFA =
-    xcfa.optimizeFurther(
-      listOf(AssumeFalseRemovalPass(), MutexToVarPass(), AtomicReadsOneWritePass())
-    )
   private var indexing = VarIndexingFactory.indexing(0)
   private val localVars = mutableMapOf<VarDecl<*>, MutableMap<Int, VarDecl<*>>>()
   private val memoryDecl = Decls.Var("__oc_checker_memory_declaration__", Int())

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(
           }
           .let { result ->
             when {
-              result.isSafe && LoopUnrollPass.FORCE_UNROLL_USED -> {
+              result.isSafe && xcfa.unsafeUnrollUsed -> {
                 // cannot report safe if force unroll was used
                 logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n")
                 if (config.outputConfig.acceptUnreliableSafe)

diff --git a/...ts/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt b/...ts/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToCegarChecker.kt
@@ -40,6 +40,7 @@ import hu.bme.mit.theta.xcfa.analysis.*
 import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts
 import hu.bme.mit.theta.xcfa.cli.params.*
 import hu.bme.mit.theta.xcfa.cli.utils.getSolver
+import hu.bme.mit.theta.xcfa.dereferences
 import hu.bme.mit.theta.xcfa.model.XCFA
 
 fun getCegarChecker(
@@ -53,6 +54,12 @@ fun getCegarChecker(
   XcfaPrec<*>,
 > {
   val cegarConfig = config.backendConfig.specConfig as CegarConfig
+  if (
+    config.inputConfig.property == ErrorDetection.DATA_RACE &&
+      xcfa.procedures.any { it.edges.any { it.label.dereferences.isNotEmpty() } }
+  ) {
+    throw RuntimeException("DATA_RACE cannot be checked when pointers exist in the file.")
+  }
   val abstractionSolverFactory: SolverFactory =
     getSolver(
       cegarConfig.abstractorConfig.abstractionSolver,

diff --git a/...jects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt b/...jects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPortfolio.kt
@@ -59,16 +59,22 @@ fun getPortfolioChecker(
       "STABLE",
       "CEGAR",
       "COMPLEX",
+      "COMPLEX25" -> complexPortfolio25(xcfa, mcm, parseContext, config, logger, uniqueLogger)
+
       "COMPLEX24" -> complexPortfolio24(xcfa, mcm, parseContext, config, logger, uniqueLogger)
 
       "COMPLEX23" -> complexPortfolio23(xcfa, mcm, parseContext, config, logger, uniqueLogger)
 
       "EMERGENT",
-      "BOUNDED" -> boundedPortfolio(xcfa, mcm, parseContext, config, logger, uniqueLogger)
+      "BOUNDED",
+      "BOUNDED25" -> boundedPortfolio25(xcfa, mcm, parseContext, config, logger, uniqueLogger)
+
+      "BOUNDED24" -> boundedPortfolio24(xcfa, mcm, parseContext, config, logger, uniqueLogger)
 
       "TESTING",
       "CHC",
-      "HORN" -> hornPortfolio(xcfa, mcm, parseContext, config, logger, uniqueLogger)
+      "HORN",
+      "HORN25" -> hornPortfolio25(xcfa, mcm, parseContext, config, logger, uniqueLogger)
 
       else -> {
         if (File(portfolioName).exists()) {

diff --git a/...e/mit/theta/xcfa/cli/portfolio/bounded.kt → ...mit/theta/xcfa/cli/portfolio/bounded24.kt b/...e/mit/theta/xcfa/cli/portfolio/bounded.kt → ...mit/theta/xcfa/cli/portfolio/bounded24.kt
@@ -27,7 +27,7 @@ import hu.bme.mit.theta.xcfa.passes.LbePass
 import hu.bme.mit.theta.xcfa.passes.LoopUnrollPass
 import java.nio.file.Paths
 
-fun boundedPortfolio(
+fun boundedPortfolio24(
   xcfa: XCFA,
   mcm: MCM,
   parseContext: ParseContext,