SVA/LTL property instrumentation

.github/workflows/pull-request-checks.yaml

@@ -160,6 +160,39 @@ jobs:
       - name: HWMCC08 benchmarks
         run: PATH=$PATH:$PWD/ebmc benchmarking/hwmcc08.sh
 
+  # This job takes approximately 1 minute
+  ebmc-spot:
+    runs-on: ubuntu-24.04
+    needs: check-ubuntu-24_04-make-clang
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          # spot
+          wget -q -O - https://www.lrde.epita.fr/repo/debian.gpg | sudo apt-key add -
+          sudo sh -c 'echo "deb http://www.lrde.epita.fr/repo/debian/ stable/" >> /etc/apt/sources.list'
+          sudo apt-get update
+          sudo apt-get install spot
+      - name: Confirm ltl2tgba is available and log the version installed
+        run: ltl2tgba --version
+      - name: Get the ebmc binary
+        uses: actions/download-artifact@v4
+        with:
+          name: ebmc-binary
+          path: ebmc
+      - name: Try the ebmc binary
+        run: chmod a+x ./ebmc/ebmc ; ./ebmc/ebmc --version
+      - name: put the ebmc binary in place
+        run: cp ebmc/ebmc src/ebmc/
+      - name: run the ebmc-spot tests
+        run: make -C regression/ebmc-spot
+
   # This job takes approximately 1 minute
   examples:
     runs-on: ubuntu-24.04

CHANGELOG

@@ -1,6 +1,7 @@
 # EBMC 5.7
 
 * Verilog: `elsif preprocessor directive
+* LTL/SVA to Buechi with --buechi
 
 # EBMC 5.6
 

regression/ebmc-spot/Makefile

@@ -0,0 +1,9 @@
+default: test
+
+TEST_PL = ../../lib/cbmc/regression/test.pl
+
+test:
+	@$(TEST_PL) -e -p -c ../../../src/ebmc/ebmc
+
+test-z3:
+	@$(TEST_PL) -e -p -c "../../../src/ebmc/ebmc --z3" -X broken-smt-backend

regression/ebmc-spot/ltl-buechi/FGp1.desc

@@ -0,0 +1,9 @@
+CORE
+FGp1.smv
+--buechi --bdd
+^\[.*\] F G p: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/FGp1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC F G p

regression/ebmc-spot/ltl-buechi/Fp1.desc

@@ -0,0 +1,9 @@
+CORE
+Fp1.smv
+--buechi --bdd
+^\[.*\] F p: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/Fp1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC F p

regression/ebmc-spot/ltl-buechi/GFp1.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+GFp1.smv
+--buechi --bdd
+^\[.*\] G F p: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+BDD engine gives wrong answer.

regression/ebmc-spot/ltl-buechi/GFp1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := !p;
+
+-- should pass
+LTLSPEC G F p

regression/ebmc-spot/ltl-buechi/Gp1.desc

@@ -0,0 +1,9 @@
+CORE
+Gp1.smv
+--buechi --bdd
+^\[.*\] G p: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/Gp1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC G p

regression/ebmc-spot/ltl-buechi/Gp2.desc

@@ -0,0 +1,9 @@
+CORE
+Gp2.smv
+--buechi
+^\[.*\] G p: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/Gp2.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+-- should fail
+LTLSPEC G p

regression/ebmc-spot/ltl-buechi/R1.smv

@@ -0,0 +1,19 @@
+MODULE main
+
+VAR x : 0..10;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x>=3 : 3;
+      TRUE: x+1;
+    esac;
+
+LTLSPEC NAME p1 := x >= 1 R x = 1 -- should pass
+LTLSPEC NAME p2 := FALSE R x != 4 -- should pass
+LTLSPEC NAME p3 := x = 2 R x = 1 -- should fail
+LTLSPEC NAME p4 := (x >= 1 R x = 1) & (FALSE R x != 4) -- should pass
+LTLSPEC NAME p5 := (x = 2 R x = 1) & (x >= 1 R x = 1) -- should fail
+LTLSPEC NAME p6 := (x = 2 R x = 1) | (x >= 1 R x = 1) -- should pass

regression/ebmc-spot/ltl-buechi/R1p1.desc

@@ -0,0 +1,9 @@
+CORE
+R1.smv
+--bdd --property p1 --buechi
+^\[p1\] x >= 1 V x = 1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/R1p2.desc

@@ -0,0 +1,9 @@
+CORE
+R1.smv
+--bdd --property p2 --buechi
+^\[p2\] FALSE V x != 4: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/R1p3.desc

@@ -0,0 +1,9 @@
+CORE
+R1.smv
+--bdd --property p3 --buechi
+^\[p3\] x = 2 V x = 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/R1p4.desc

@@ -0,0 +1,9 @@
+CORE
+R1.smv
+--bdd --property p4 --buechi
+^\[p4\] x >= 1 V x = 1 & FALSE V x != 4: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/R1p5.desc

@@ -0,0 +1,9 @@
+CORE
+R1.smv
+--bdd --property p5 --buechi
+^\[p5\] x = 2 V x = 1 & x >= 1 V x = 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/R1p6.desc

@@ -0,0 +1,9 @@
+CORE
+R1.smv
+--bdd --property p6 --buechi
+^\[p6\] x = 2 V x = 1 \| x >= 1 V x = 1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/Xp1.desc

@@ -0,0 +1,9 @@
+CORE
+Xp1.smv
+--buechi --bdd
+^\[.*\] X p: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/Xp1.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+-- should pass
+LTLSPEC X p

regression/ebmc-spot/ltl-buechi/and1.desc

@@ -0,0 +1,9 @@
+CORE
+and1.smv
+--buechi --bdd
+^\[.*\] X p & X q: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/and1.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := FALSE;
+       next(q) := TRUE;
+
+-- should pass
+LTLSPEC X p & X q
+

regression/ebmc-spot/ltl-buechi/and2.desc

@@ -0,0 +1,9 @@
+CORE
+and2.smv
+--buechi --bdd
+^\[.*\] X \(p & q\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/and2.smv

@@ -0,0 +1,15 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := FALSE;
+       next(p) := TRUE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := FALSE;
+       next(q) := TRUE;
+
+-- should pass
+LTLSPEC X (p & q)
+

regression/ebmc-spot/ltl-buechi/iff1.desc

@@ -0,0 +1,9 @@
+CORE
+iff1.smv
+--buechi --bdd
+^\[.*\] X p <-> X q: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/iff1.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p <-> X q

regression/ebmc-spot/ltl-buechi/iff2.desc

@@ -0,0 +1,9 @@
+CORE
+iff2.smv
+--buechi --bdd
+^\[.*\] X \(p <-> q\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/iff2.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X (p <-> q)

regression/ebmc-spot/ltl-buechi/implies1.desc

@@ -0,0 +1,9 @@
+CORE
+implies1.smv
+--buechi --bdd
+^\[.*\] X p -> X q: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc-spot/ltl-buechi/implies1.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR p : boolean;
+
+ASSIGN init(p) := TRUE;
+       next(p) := FALSE;
+
+VAR q : boolean;
+
+ASSIGN init(q) := TRUE;
+       next(q) := FALSE;
+
+-- should pass
+LTLSPEC X p -> X q

regression/ebmc-spot/ltl-buechi/implies2.desc

@@ -0,0 +1,9 @@
+CORE
+implies2.smv
+--buechi --bdd
+^\[.*\] X \(p -> q\): PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--