Allow parallel update_suite run with -m/-i/-w

.github/workflows/unlocked.yml

@@ -193,13 +193,13 @@ jobs:
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
       - name: Test marshal regression
-        run: ruby scripts/update_suite.rb -m
+        run: ruby scripts/update_suite.rb -m -s
 
       - name: Test incremental regression
-        run: ruby scripts/update_suite.rb -i
+        run: ruby scripts/update_suite.rb -i -s
 
       - name: Test incremental regression with cfg comparison
-        run: ruby scripts/update_suite.rb -c
+        run: ruby scripts/update_suite.rb -c -s
 
   gobview:
     strategy:

scripts/update_suite.rb

@@ -73,9 +73,6 @@ def clearline
 incremental = (ARGV.last == "-i" && ARGV.pop) || cfg
 report = ARGV.last == "-r" && ARGV.pop
 only = ARGV[0] unless ARGV[0].nil?
-if marshal || witness || incremental then
-  sequential = true
-end
 if marshal && incremental then
   fail "Marshal (-m) and Incremental (-i) tests can not be activated at the same time!"
 end
@@ -505,8 +502,9 @@ def create_test_set(lines)
 
   def run
     filename = File.basename(@path)
-    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --enable incremental.save --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}"
-    cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --enable dbg.timing.enabled --enable incremental.load --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}"
+    incrdir = "incremental_data-#{@id.sub('/','-')}"
+    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --enable incremental.save --set incremental.save-dir #{incrdir} --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}"
+    cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --enable dbg.timing.enabled --enable incremental.load --set incremental.load-dir #{incrdir} --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}"
     starttime = Time.now
     run_testset(@testset_incr, cmd, starttime)
     # apply patch
@@ -515,7 +513,7 @@ def run
     run_testset(@testset_incr, cmd_incr, starttime)
     # revert patch
     `patch -p3 -b -R <#{@patch_path}`
-    FileUtils.rm_rf('incremental_data')
+    FileUtils.rm_rf(incrdir)
   end
 
   def report
@@ -549,12 +547,13 @@ def create_test_set(lines)
   end
   def run ()
     filename = File.basename(@path)
-    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --set save_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}"
-    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --conf run/config.json --set save_run '' --set load_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}"
+    rundir = "run-#{@id.sub('/','-')}"
+    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --set save_run #{rundir} --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}"
+    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --conf #{rundir}/config.json --set save_run '' --set load_run #{rundir} --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd1, starttime)
     run_testset(@testset, cmd2, starttime)
-    FileUtils.rm_rf('run')
+    FileUtils.rm_rf(rundir)
     end
 end
 
@@ -565,13 +564,14 @@ def create_test_set(lines)
   end
   def run ()
     filename = File.basename(@path)
-    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile}0 --enable warn.debug --set dbg.timing.enabled true --enable witness.yaml.enabled --set goblint-dir .goblint-#{@id.sub('/','-')}-witness1 2>#{@testset.statsfile}0"
-    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set ana.activated[+] unassume --enable warn.debug --set dbg.timing.enabled true --set witness.yaml.unassume witness.yml --set goblint-dir .goblint-#{@id.sub('/','-')}-witness2 2>#{@testset.statsfile}"
+    witness = "witness-#{@id.sub('/','-')}.yml"
+    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile}0 --enable warn.debug --set dbg.timing.enabled true --enable witness.yaml.enabled --set witness.yaml.path #{witness} --set goblint-dir .goblint-#{@id.sub('/','-')}-witness1 2>#{@testset.statsfile}0"
+    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set ana.activated[+] unassume --enable warn.debug --set dbg.timing.enabled true --set witness.yaml.unassume #{witness} --set goblint-dir .goblint-#{@id.sub('/','-')}-witness2 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd1, starttime)
     starttime = Time.now
     run_testset(@testset, cmd2, starttime)
-    FileUtils.rm_f('witness.yml')
+    FileUtils.rm_f(witness)
     end
 end
 

tests/regression/01-cpa/48-inf-recursion.c

@@ -1,4 +1,4 @@
-// SKIP
+// SKIP NOTIMEOUT
 
 // Can be used to try timeouts.
 // With defaults this will create |int| contexts and lead to a stack overflow in

tests/regression/02-base/05-result_thread_creation.c

@@ -1,4 +1,4 @@
-// SKIP This is not testing anything right now...
+// SKIP NOCHECK This is not testing anything right now...
 #include<stdlib.h>
 #include<pthread.h>