SVA/LTL property instrumentation

This adds --buechi, which triggers an instrumentation pass that turns LTL
and select SVA properties into a Buechi automaton.  The automaton is then
added to the model, and the property is replaced by the Buechi acceptance
condition.

The translation is done via ltl2tgba.

This enables checking arbitrary LTL properties via the BDD engine.

Author: kroening

.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
 

lib/cbmc

@@ -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/Makefile

@@ -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.desc

@@ -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/FGp1.smv

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

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

@@ -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/Fp1.smv

@@ -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.desc

@@ -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/GFp1.smv

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

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

@@ -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/Gp1.smv

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

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

@@ -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/Gp2.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/R1.smv

@@ -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/R1p1.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/R1p2.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/R1p3.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/R1p4.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/R1p5.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/R1p6.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.desc

@@ -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/Xp1.smv

@@ -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.desc

@@ -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/and1.smv

@@ -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.desc

@@ -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/and2.smv

@@ -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.desc

@@ -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/iff1.smv

@@ -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.desc

@@ -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/iff2.smv

@@ -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.desc

@@ -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/implies1.smv

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