Merge pull request #797 from diffblue/instrument_property

SVA/LTL property instrumentation

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
 

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
+--