Merge pull request #787 from goblint/cram

Use Cram for tests

.github/workflows/locked.yml

@@ -58,6 +58,9 @@ jobs:
       - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
+      - name: Test regression cram
+        run: opam exec -- dune runtest tests/regression
+
       - name: Test unit
         run: opam exec -- dune runtest unittest
 
@@ -101,7 +104,7 @@ jobs:
         run: ./make.sh nat
 
       - name: Test extraction
-        run: cd tests/extraction && ./test.sh
+        run: opam exec -- dune runtest tests/extraction
 
 
   gobview:

.github/workflows/unlocked.yml

@@ -83,6 +83,9 @@ jobs:
         if: ${{ matrix.apron }}
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
+      - name: Test regression cram
+        run: opam exec -- dune runtest tests/regression
+
       - name: Test unit
         run: opam exec -- dune runtest unittest
 
@@ -159,6 +162,9 @@ jobs:
         # if: ${{ matrix.apron }}
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
+      - name: Test regression cram
+        run: opam exec -- dune runtest tests/regression
+
       - name: Test unit
         run: opam exec -- dune runtest unittest
 

dune-project

@@ -1,6 +1,7 @@
 (lang dune 2.9)
 ; need 2.9 for dune-site to work with opam install: https://github.com/ocaml/dune/issues/4212, https://github.com/ocaml/dune/pull/4645, https://github.com/ocaml/dune/pull/4774
 (using dune_site 0.1)
+(cram enable)
 (name goblint)
 ; build failed with: Files src/.maingoblint.eobjs/native/mutex.cmx and _opam/lib/ocaml/threads/threads.cmxa both define a module named Mutex
 ; maybe related: https://github.com/ocaml/dune/issues/1727, https://github.com/ocaml/dune/issues/597

tests/extraction/00-sanity.t

@@ -0,0 +1,16 @@
+Copy Promela model here.
+
+  $ cp -r ../../spin ./spin
+
+Run Goblint extraction.
+
+  $ goblint --set ana.activated[+] extract-pthread 00-sanity.c > /dev/null 2>&1
+
+Run spin.
+
+  $ (spin -a pml-result/pthread.pml && cc -o pan pan.c && ./pan -a) > out.txt 2>&1
+
+Non-starving, should not have trail.
+
+  $ grep pthread.pml.trail out.txt
+  [1]

tests/extraction/01-base.t

@@ -0,0 +1,16 @@
+Copy Promela model here.
+
+  $ cp -r ../../spin ./spin
+
+Run Goblint extraction.
+
+  $ goblint --set ana.activated[+] extract-pthread 01-base.c > /dev/null 2>&1
+
+Run spin.
+
+  $ (spin -a pml-result/pthread.pml && cc -o pan pan.c && ./pan -a) > out.txt 2>&1
+
+Starving, should have trail.
+
+  $ grep pthread.pml.trail out.txt
+  pan: wrote pthread.pml.trail

tests/extraction/02-starve.t

@@ -0,0 +1,16 @@
+Copy Promela model here.
+
+  $ cp -r ../../spin ./spin
+
+Run Goblint extraction.
+
+  $ goblint --set ana.activated[+] extract-pthread 02-starve.c > /dev/null 2>&1
+
+Run spin.
+
+  $ (spin -a pml-result/pthread.pml && cc -o pan pan.c && ./pan -a) > out.txt 2>&1
+
+Starving, should have trail.
+
+  $ grep pthread.pml.trail out.txt
+  pan: wrote pthread.pml.trail

tests/extraction/dune

@@ -0,0 +1,3 @@
+(cram
+ (enabled_if %{bin-available:spin})
+ (deps %{bin:goblint} (package goblint) (glob_files *.c) (source_tree ../../spin))) ; need entire package for includes/

tests/extraction/dune-project

@@ -0,0 +1,3 @@
+(lang dune 3.0)
+; need 3.0 for bin-available, but cannot use 3.0 for entire project because https://github.com/johnwhitington/ppx_blob/issues/23
+; TODO: remove when ppx_blob fixed

tests/regression/00-sanity/01-assert.t

@@ -0,0 +1,9 @@
+  $ goblint 01-assert.c
+  [Success][Assert] Assertion "success" will succeed (01-assert.c:10:3-10:28)
+  [Warning][Assert] Assertion "unknown == 4" is unknown. (01-assert.c:11:3-11:33)
+  [Error][Assert] Assertion "fail" will fail. (01-assert.c:12:3-12:25)
+  Live lines: 7
+  [Warning][Deadcode] Function 'main' has dead code:
+    on lines 13..14 (01-assert.c:13-14)
+  Found dead code on 2 lines!
+  Total lines (logical LoC): 9

tests/regression/00-sanity/dune

@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))

tests/regression/04-mutex/01-simple_rc.t

@@ -0,0 +1,17 @@
+  $ goblint 01-simple_rc.c
+  Live lines: 12
+  No lines with dead code found by solver.
+  Total lines (logical LoC): 12
+  [Warning][Race] Memory location myglobal@01-simple_rc.c:4:5-4:13 (race with conf. 110):
+    write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40]},
+              lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (01-simple_rc.c:10:3-10:22)
+    write with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110) (01-simple_rc.c:19:3-19:22)
+    read with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110) (01-simple_rc.c:10:3-10:22)
+    read with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110) (01-simple_rc.c:19:3-19:22)
+
+  Summary for all memory locations:
+  	safe:            0
+  	vulnerable:      0
+  	unsafe:          1
+  	-------------------
+  	total:           1

tests/regression/04-mutex/dune

@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))

tests/regression/dune

@@ -0,0 +1,3 @@
+(cram
+ (applies_to :whole_subtree)
+ (deps %{bin:goblint} (package goblint))) ; need entire package for includes/