Sleep-Reduced Thread-Modular Proofs and related CHC refactoring

.gitignore

@@ -50,6 +50,7 @@ trunk/examples/concurrent/bpl/VMCAI2021/generated/*.yml
 trunk/examples/concurrent/bpl/weaver-benchmarks/generated/**/*.bpl
 trunk/examples/concurrent/bpl/weaver-benchmarks/generated/**/*.yml
 trunk/examples/concurrent/bpl/weaver-benchmarks/weaver
+trunk/examples/concurrent/bpl/parameterized/*/CHC*.smt2
 trunk/examples/witness-generation-validation/regression/*.graphml
 trunk/examples/witness-generation-validation/regression/*.yaml
 trunk/examples/witness-generation-validation/regression/*.yml

releaseScripts/default/benchexec/sleep-threadmodular.xml

@@ -0,0 +1,246 @@
+<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
+<benchmark tool="ultimateautomizer" memlimit="22GB" timelimit="7200" hardtimelimit="7220" cpuCores="2">
+  <resultfiles>${taskdef_path}/CHC_*.smt2</resultfiles>
+
+  <option name="--force-no-wrapper" />
+
+  <rundefinition name="SleepExplicit.Eldarica">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--chcsolver.chc.solver.backend">ELDARICA</option>
+  </rundefinition>
+
+  <rundefinition name="SleepExplicit.Z3">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--chcsolver.chc.solver.backend">Z3</option>
+  </rundefinition>
+
+  <rundefinition name="SleepExplicit.Golem">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--chcsolver.chc.solver.backend">GOLEM</option>
+  </rundefinition>
+
+  <?ignore
+  <rundefinition name="SleepExplicit.TreeAutomizer">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--chcsolver.chc.solver.backend">TREEAUTOMIZER</option>
+    <option name="--rcfgbuilder.smt.solver">Internal_SMTInterpol</option>
+  </rundefinition>
+  ?>
+
+  <rundefinition name="SleepExplicit.NondetSleep.Eldarica">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--icfgtochc.use.nondeterministic.sleep.update.encoding">true</option>
+    <option name="--chcsolver.chc.solver.backend">ELDARICA</option>
+  </rundefinition>
+
+  <rundefinition name="SleepExplicit.NondetSleep.Z3">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--icfgtochc.use.nondeterministic.sleep.update.encoding">true</option>
+    <option name="--chcsolver.chc.solver.backend">Z3</option>
+  </rundefinition>
+
+  <rundefinition name="SleepExplicit.NondetSleep.Golem">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--icfgtochc.use.nondeterministic.sleep.update.encoding">true</option>
+    <option name="--chcsolver.chc.solver.backend">GOLEM</option>
+  </rundefinition>
+
+  <rundefinition name="SleepExplicit.NondetSleep.NecSufComm.Eldarica">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--icfgtochc.use.nondeterministic.sleep.update.encoding">true</option>
+    <option name="--icfgtochc.conditional.independence">NECESSARY_AND_SUFFICIENT</option>
+    <option name="--chcsolver.chc.solver.backend">ELDARICA</option>
+  </rundefinition>
+
+  <rundefinition name="SleepExplicit.NondetSleep.NecSufComm.Z3">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--icfgtochc.use.nondeterministic.sleep.update.encoding">true</option>
+    <option name="--icfgtochc.conditional.independence">NECESSARY_AND_SUFFICIENT</option>
+    <option name="--chcsolver.chc.solver.backend">Z3</option>
+  </rundefinition>
+
+  <rundefinition name="SleepExplicit.NondetSleep.NecSufComm.Golem">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--icfgtochc.use.nondeterministic.sleep.update.encoding">true</option>
+    <option name="--icfgtochc.conditional.independence">NECESSARY_AND_SUFFICIENT</option>
+    <option name="--chcsolver.chc.solver.backend">GOLEM</option>
+  </rundefinition>
+
+  <rundefinition name="SleepExplicit.NecSufComm.Eldarica">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--icfgtochc.conditional.independence">NECESSARY_AND_SUFFICIENT</option>
+    <option name="--chcsolver.chc.solver.backend">ELDARICA</option>
+  </rundefinition>
+
+  <rundefinition name="SleepExplicit.NecSufComm.Z3">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--icfgtochc.conditional.independence">NECESSARY_AND_SUFFICIENT</option>
+    <option name="--chcsolver.chc.solver.backend">Z3</option>
+  </rundefinition>
+
+  <rundefinition name="SleepExplicit.NecSufComm.Golem">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">true</option>
+    <option name="--icfgtochc.conditional.independence">NECESSARY_AND_SUFFICIENT</option>
+    <option name="--chcsolver.chc.solver.backend">GOLEM</option>
+  </rundefinition>
+
+  <rundefinition name="SleepSymbolic.Eldarica">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">false</option>
+    <option name="--chcsolver.chc.solver.backend">ELDARICA</option>
+  </rundefinition>
+
+  <rundefinition name="SleepSymbolic.Z3">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">false</option>
+    <option name="--chcsolver.chc.solver.backend">Z3</option>
+  </rundefinition>
+
+  <rundefinition name="SleepSymbolic.Golem">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">false</option>
+    <option name="--chcsolver.chc.solver.backend">GOLEM</option>
+  </rundefinition>
+
+  <?ignore
+  <rundefinition name="SleepSymbolic.TreeAutomizer">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">false</option>
+    <option name="--chcsolver.chc.solver.backend">TREEAUTOMIZER</option>
+    <option name="--rcfgbuilder.smt.solver">Internal_SMTInterpol</option>
+  </rundefinition>
+  ?>
+
+  <rundefinition name="SleepSymbolic-Symmetry.Eldarica">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">false</option>
+    <option name="--icfgtochc.use.symmetry.clauses">true</option>
+    <option name="--chcsolver.chc.solver.backend">ELDARICA</option>
+  </rundefinition>
+
+  <rundefinition name="SleepSymbolic-Symmetry.Z3">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">false</option>
+    <option name="--icfgtochc.use.symmetry.clauses">true</option>
+    <option name="--chcsolver.chc.solver.backend">Z3</option>
+  </rundefinition>
+
+  <rundefinition name="SleepSymbolic-Symmetry.Golem">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">false</option>
+    <option name="--icfgtochc.use.symmetry.clauses">true</option>
+    <option name="--chcsolver.chc.solver.backend">GOLEM</option>
+  </rundefinition>
+
+  <?ignore
+  <rundefinition name="SleepSymbolic-Symmetry.TreeAutomizer">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">true</option>
+    <option name="--icfgtochc.break.symmetry.of.preference.order">false</option>
+    <option name="--icfgtochc.use.symmetry.clauses">true</option>
+    <option name="--chcsolver.chc.solver.backend">TREEAUTOMIZER</option>
+    <option name="--rcfgbuilder.smt.solver">Internal_SMTInterpol</option>
+  </rundefinition>
+  ?>
+
+  <rundefinition name="NoSleep.Eldarica">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">false</option>
+    <option name="--chcsolver.chc.solver.backend">ELDARICA</option>
+  </rundefinition>
+
+  <rundefinition name="NoSleep.Z3">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">false</option>
+    <option name="--chcsolver.chc.solver.backend">Z3</option>
+  </rundefinition>
+
+  <rundefinition name="NoSleep.Golem">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">false</option>
+    <option name="--chcsolver.chc.solver.backend">GOLEM</option>
+  </rundefinition>
+
+  <?ignore
+  <rundefinition name="NoSleep.TreeAutomizer">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">false</option>
+    <option name="--chcsolver.chc.solver.backend">TREEAUTOMIZER</option>
+    <option name="--rcfgbuilder.smt.solver">Internal_SMTInterpol</option>
+  </rundefinition>
+  ?>
+
+  <rundefinition name="NoSleep-Symmetry.Eldarica">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">false</option>
+    <option name="--icfgtochc.use.symmetry.clauses">true</option>
+    <option name="--chcsolver.chc.solver.backend">ELDARICA</option>
+  </rundefinition>
+
+  <rundefinition name="NoSleep-Symmetry.Z3">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">false</option>
+    <option name="--icfgtochc.use.symmetry.clauses">true</option>
+    <option name="--chcsolver.chc.solver.backend">Z3</option>
+  </rundefinition>
+
+  <rundefinition name="NoSleep-Symmetry.Golem">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml</option>
+    <option name="--icfgtochc.enable.sleep.set.reduction">false</option>
+    <option name="--icfgtochc.use.symmetry.clauses">true</option>
+    <option name="--chcsolver.chc.solver.backend">GOLEM</option>
+  </rundefinition>
+
+  <?ignore
+  <rundefinition name="UniHorn">
+    <option name="-tc">../../../trunk/examples/concurrent/bpl/parameterized/ThreadModularUniHorn.xml</option>
+  </rundefinition>
+  ?>
+
+  <tasks name="threadmodular-examples">
+    <include>../../../trunk/examples/concurrent/bpl/parameterized/*/*.yml</include>
+    <propertyfile>../../../trunk/examples/svcomp/properties/unreach-call.prp</propertyfile>
+
+    <option name="-s">${taskdef_path}/${taskdef_name}-settings.epf</option>
+  </tasks>
+
+  <tasks name="threadmodular-unsolved">
+    <includesfile>../../../trunk/examples/concurrent/bpl/parameterized/unsolved.set</includesfile>
+    <propertyfile>../../../trunk/examples/svcomp/properties/unreach-call.prp</propertyfile>
+
+    <option name="-s">${taskdef_path}/${taskdef_name}-settings.epf</option>
+  </tasks>
+</benchmark>

releaseScripts/default/makeZip.sh

@@ -51,7 +51,7 @@ if [ "$2" == "linux" ]; then
   echo "Building .zip for linux..."
   ARCH="linux"
   ARCHPATH="products/CLI-E4/linux/gtk/x86_64"
-  ADDS+=("adds/z3" "adds/cvc4" "adds/mathsat" "adds/ltl2ba")
+  ADDS+=("adds/z3" "adds/cvc4" "adds/mathsat" "adds/ltl2ba" "adds/golem")
 elif [ "$2" == "win32" ]; then
   echo "Building .zip for win32..."
   ARCH="win32"

trunk/examples/concurrent/OwickiGries/PetriPrograms/separate-threads-interaction.og.yml

@@ -0,0 +1,17 @@
+#invalid
+# needs ghost variables to distinguish case where other thread has set g:=1 but not yet incremented its z_i
+omega:
+  "m.l0"  : true
+  "m.l1"  : (= g 0)
+  "t1.l0" : (and (= z1 1) (= g 0))
+  "t1.l1" : (and (= z1 2) (or (and (= g 0) (= z2 2)) (= g 1)))
+  "t1.l2" : (and (= z1 2) (= g 1) (= z2 2))
+  "t1.l3" : (and (= g 1)  (or (and (= z1 3) (= z2 2)) (and (= z1 2) (= z2 3))))
+  "t2.l0" : (and (= z2 1) (= g 0))
+  "t2.l1" : (and (= z2 2) (or (and (= g 0) (= z1 2)) (and (= g 1) (= z1 3))))
+  "t2.l2" : (and (= z2 2) (= g 1) (= z1 2))
+  "t2.l3" : (and (= g 1)  (or (and (= z1 2) (= z2 3)) (and (= z1 3) (= z2 2))))
+  "e"     : false
+ghost_variables:
+ghost_updates:
+

trunk/examples/concurrent/bpl/parameterized/ThreadModularVerifier.xml

@@ -0,0 +1,10 @@
+<rundefinition>
+  <name>Ultimate Toolchain</name>
+  <toolchain>
+    <plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
+    <plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+    <plugin id="de.uni_freiburg.informatik.ultimate.plugins.icfgtochc"/>
+    <plugin id="de.uni_freiburg.informatik.ultimate.chcprinter" />
+    <plugin id="de.uni_freiburg.informatik.ultimate.plugins.chcsolver"/>
+  </toolchain>
+</rundefinition>

trunk/examples/concurrent/bpl/parameterized/add-sub-k/add-sub-k.bpl

@@ -0,0 +1,15 @@
+//#Safe
+
+var x : int;
+
+procedure ULTIMATE.start()
+modifies x;
+free requires x == 0;
+free ensures x == 0;
+{
+  var k : int;
+
+  havoc k;
+  x := x + k;
+  x := x - k;
+}

trunk/examples/concurrent/bpl/parameterized/add-sub-k/add-sub-k.yml

@@ -0,0 +1,12 @@
+format_version: '2.0'
+
+input_files: 'add-sub-k.bpl'
+
+properties:
+  - property_file: ../../../../svcomp/properties/unreach-call.prp
+    expected_verdict: true
+
+options:
+  language: Boogie
+  # settings_file: add-sub-k.yml-settings.epf
+

trunk/examples/concurrent/bpl/parameterized/add-sub-k/add-sub-k.yml-settings.epf

@@ -0,0 +1,49 @@
+#Thu May 25 14:24:13 CEST 2023
+
+
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.icfgtochc=
+
+# Program model and specification
+/instance/de.uni_freiburg.informatik.ultimate.plugins.icfgtochc/Concurrency\ mode=PARAMETRIC
+/instance/de.uni_freiburg.informatik.ultimate.plugins.icfgtochc/Assume\ program\ has\ a\ precondition=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.icfgtochc/Specification\ mode=POSTCONDITION
+
+# Thread modularity level
+/instance/de.uni_freiburg.informatik.ultimate.plugins.icfgtochc/Thread-Modular\ Proof\ Level=2
+
+# Program-specific settings for sleep set reduction
+/instance/de.uni_freiburg.informatik.ultimate.plugins.icfgtochc/Conditional\ Independence=NONE
+/instance/de.uni_freiburg.informatik.ultimate.plugins.icfgtochc/Preference\ order\ used\ for\ reduction=SEQ_COMP
+
+@de.uni_freiburg.informatik.ultimate.plugins.icfgtochc=0.2.3
+file_export_version=3.0
+
+
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.chcsolver=
+/instance/de.uni_freiburg.informatik.ultimate.plugins.chcsolver/Produce\ CHC\ model\ if\ query\ is\ SAT=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.chcsolver/Produce\ UNSAT\ core\ if\ query\ is\ UNSAT=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.chcsolver/Produce\ derivation\ if\ query\ is\ UNSAT=false
+@de.uni_freiburg.informatik.ultimate.plugins.chcsolver=0.2.3
+file_export_version=3.0
+
+
+\!/instance/de.uni_freiburg.informatik.ultimate.chcprinter=
+/instance/de.uni_freiburg.informatik.ultimate.chcprinter/File\ name=CHC
+/instance/de.uni_freiburg.informatik.ultimate.chcprinter/Use\ automatic\ naming=true
+/instance/de.uni_freiburg.informatik.ultimate.chcprinter/Save\ file\ in\ source\ directory=true
+@de.uni_freiburg.informatik.ultimate.chcprinter=0.2.3
+file_export_version=3.0
+
+
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Add\ additional\ assume\ for\ each\ assert=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Size\ of\ a\ code\ block=OneNontrivialStatement
+@de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=0.2.3
+file_export_version=3.0
+
+
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Add\ additional\ assume\ for\ each\ assert=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Size\ of\ a\ code\ block=OneNontrivialStatement
+@de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=0.2.3
+file_export_version=3.0

trunk/examples/concurrent/bpl/parameterized/add-sub-k/regression/NoSleep.Level2.GOLEM.yml

@@ -0,0 +1,20 @@
+format_version: '2.0'
+
+input_files: '../add-sub-k.bpl'
+
+properties:
+  - property_file: ../../../../../svcomp/properties/unreach-call.prp
+    expected_verdict: unsat
+
+options:
+  language: Boogie
+
+  settings_file: ../add-sub-k.yml-settings.epf
+  timeout: 70 #seconds
+
+  de.uni_freiburg.informatik.ultimate.plugins.icfgtochc:
+    Enable sleep set reduction: false
+
+  de.uni_freiburg.informatik.ultimate.plugins.chcsolver:
+    CHC solver backend: GOLEM
+