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