From 268ad015833889c705f4aa5f4b566ecad26cae78 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 27 May 2025 05:03:11 -0700 Subject: [PATCH 1/2] bump CBMC dependency --- lib/cbmc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/cbmc b/lib/cbmc index 3c915ebe3..50be009ae 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit 3c915ebe35448a20555c1ef55d51540b52c5c34a +Subproject commit 50be009aeec0a21713b20e980b39fa61470a40c0 From d682fe43333a31675bb40b65de7cf0a62dedc463 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 3 Nov 2024 07:17:12 -0500 Subject: [PATCH 2/2] 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. --- .github/workflows/pull-request-checks.yaml | 33 ++ CHANGELOG | 1 + lib/cbmc | 2 +- regression/ebmc-spot/Makefile | 9 + regression/ebmc-spot/ltl-buechi/FGp1.desc | 9 + regression/ebmc-spot/ltl-buechi/FGp1.smv | 9 + regression/ebmc-spot/ltl-buechi/Fp1.desc | 9 + regression/ebmc-spot/ltl-buechi/Fp1.smv | 9 + regression/ebmc-spot/ltl-buechi/GFp1.desc | 10 + regression/ebmc-spot/ltl-buechi/GFp1.smv | 9 + regression/ebmc-spot/ltl-buechi/Gp1.desc | 9 + regression/ebmc-spot/ltl-buechi/Gp1.smv | 9 + regression/ebmc-spot/ltl-buechi/Gp2.desc | 9 + regression/ebmc-spot/ltl-buechi/Gp2.smv | 9 + regression/ebmc-spot/ltl-buechi/R1.smv | 19 + regression/ebmc-spot/ltl-buechi/R1p1.desc | 9 + regression/ebmc-spot/ltl-buechi/R1p2.desc | 9 + regression/ebmc-spot/ltl-buechi/R1p3.desc | 9 + regression/ebmc-spot/ltl-buechi/R1p4.desc | 9 + regression/ebmc-spot/ltl-buechi/R1p5.desc | 9 + regression/ebmc-spot/ltl-buechi/R1p6.desc | 9 + regression/ebmc-spot/ltl-buechi/Xp1.desc | 9 + regression/ebmc-spot/ltl-buechi/Xp1.smv | 9 + regression/ebmc-spot/ltl-buechi/and1.desc | 9 + regression/ebmc-spot/ltl-buechi/and1.smv | 15 + regression/ebmc-spot/ltl-buechi/and2.desc | 9 + regression/ebmc-spot/ltl-buechi/and2.smv | 15 + regression/ebmc-spot/ltl-buechi/iff1.desc | 9 + regression/ebmc-spot/ltl-buechi/iff1.smv | 14 + regression/ebmc-spot/ltl-buechi/iff2.desc | 9 + regression/ebmc-spot/ltl-buechi/iff2.smv | 14 + regression/ebmc-spot/ltl-buechi/implies1.desc | 9 + regression/ebmc-spot/ltl-buechi/implies1.smv | 14 + regression/ebmc-spot/ltl-buechi/implies2.desc | 9 + regression/ebmc-spot/ltl-buechi/implies2.smv | 14 + regression/ebmc-spot/ltl-buechi/or1.desc | 9 + regression/ebmc-spot/ltl-buechi/or1.smv | 14 + regression/ebmc-spot/ltl-buechi/or2.desc | 9 + regression/ebmc-spot/ltl-buechi/or2.smv | 14 + .../ebmc-spot/sva-buechi/cycle_delay2.desc | 7 + .../sva-buechi/default_disable1.desc | 9 + .../ebmc-spot/sva-buechi/eventually4.desc | 8 + .../ebmc-spot/sva-buechi/immediate1.desc | 9 + regression/ebmc-spot/sva-buechi/initial2.desc | 10 + .../ebmc-spot/sva-buechi/restrict1.bdd.desc | 10 + .../ebmc-spot/sva-buechi/restrict1.bmc.desc | 10 + .../sva-buechi/s_eventually1.bdd.desc | 8 + .../ebmc-spot/sva-buechi/s_eventually3.desc | 8 + .../ebmc-spot/sva-buechi/sequence4.bdd.desc | 8 + .../ebmc-spot/sva-buechi/sequence4.bmc.desc | 8 + .../ebmc-spot/sva-buechi/sequence5.desc | 12 + .../ebmc-spot/sva-buechi/sequence6.desc | 10 + .../sva-buechi/sequence_implication1.desc | 12 + .../sva-buechi/sequence_implication2.desc | 8 + .../sva-buechi/sequence_intersect1.desc | 14 + .../sva-buechi/sequence_repetition6.desc | 8 + .../ebmc-spot/sva-buechi/static_final1.desc | 9 + regression/ebmc-spot/sva-buechi/sva_and1.desc | 11 + regression/ebmc-spot/sva-buechi/sva_iff1.desc | 11 + .../ebmc-spot/sva-buechi/sva_implies1.desc | 11 + regression/ebmc-spot/sva-buechi/sva_not1.desc | 9 + .../sva-buechi/system_verilog_assertion3.desc | 7 + src/ebmc/Makefile | 1 + src/ebmc/ebmc_parse_options.cpp | 6 + src/ebmc/ebmc_parse_options.h | 2 +- src/ebmc/instrument_buechi.cpp | 70 +++ src/ebmc/instrument_buechi.h | 25 + src/temporal-logic/Makefile | 3 + src/temporal-logic/hoa.cpp | 535 ++++++++++++++++++ src/temporal-logic/hoa.h | 66 +++ src/temporal-logic/ltl_sva_to_string.cpp | 409 +++++++++++++ src/temporal-logic/ltl_sva_to_string.h | 56 ++ src/temporal-logic/ltl_to_buechi.cpp | 181 ++++++ src/temporal-logic/ltl_to_buechi.h | 41 ++ src/temporal-logic/sva_sequence_match.cpp | 10 +- src/temporal-logic/temporal_logic.cpp | 8 + src/temporal-logic/temporal_logic.h | 10 +- src/trans-word-level/sequence.cpp | 11 +- src/verilog/sva_expr.h | 32 +- unit/Makefile | 1 + unit/temporal-logic/ltl_sva_to_string.cpp | 69 +++ 81 files changed, 2141 insertions(+), 25 deletions(-) create mode 100644 regression/ebmc-spot/Makefile create mode 100644 regression/ebmc-spot/ltl-buechi/FGp1.desc create mode 100644 regression/ebmc-spot/ltl-buechi/FGp1.smv create mode 100644 regression/ebmc-spot/ltl-buechi/Fp1.desc create mode 100644 regression/ebmc-spot/ltl-buechi/Fp1.smv create mode 100644 regression/ebmc-spot/ltl-buechi/GFp1.desc create mode 100644 regression/ebmc-spot/ltl-buechi/GFp1.smv create mode 100644 regression/ebmc-spot/ltl-buechi/Gp1.desc create mode 100644 regression/ebmc-spot/ltl-buechi/Gp1.smv create mode 100644 regression/ebmc-spot/ltl-buechi/Gp2.desc create mode 100644 regression/ebmc-spot/ltl-buechi/Gp2.smv create mode 100644 regression/ebmc-spot/ltl-buechi/R1.smv create mode 100644 regression/ebmc-spot/ltl-buechi/R1p1.desc create mode 100644 regression/ebmc-spot/ltl-buechi/R1p2.desc create mode 100644 regression/ebmc-spot/ltl-buechi/R1p3.desc create mode 100644 regression/ebmc-spot/ltl-buechi/R1p4.desc create mode 100644 regression/ebmc-spot/ltl-buechi/R1p5.desc create mode 100644 regression/ebmc-spot/ltl-buechi/R1p6.desc create mode 100644 regression/ebmc-spot/ltl-buechi/Xp1.desc create mode 100644 regression/ebmc-spot/ltl-buechi/Xp1.smv create mode 100644 regression/ebmc-spot/ltl-buechi/and1.desc create mode 100644 regression/ebmc-spot/ltl-buechi/and1.smv create mode 100644 regression/ebmc-spot/ltl-buechi/and2.desc create mode 100644 regression/ebmc-spot/ltl-buechi/and2.smv create mode 100644 regression/ebmc-spot/ltl-buechi/iff1.desc create mode 100644 regression/ebmc-spot/ltl-buechi/iff1.smv create mode 100644 regression/ebmc-spot/ltl-buechi/iff2.desc create mode 100644 regression/ebmc-spot/ltl-buechi/iff2.smv create mode 100644 regression/ebmc-spot/ltl-buechi/implies1.desc create mode 100644 regression/ebmc-spot/ltl-buechi/implies1.smv create mode 100644 regression/ebmc-spot/ltl-buechi/implies2.desc create mode 100644 regression/ebmc-spot/ltl-buechi/implies2.smv create mode 100644 regression/ebmc-spot/ltl-buechi/or1.desc create mode 100644 regression/ebmc-spot/ltl-buechi/or1.smv create mode 100644 regression/ebmc-spot/ltl-buechi/or2.desc create mode 100644 regression/ebmc-spot/ltl-buechi/or2.smv create mode 100644 regression/ebmc-spot/sva-buechi/cycle_delay2.desc create mode 100644 regression/ebmc-spot/sva-buechi/default_disable1.desc create mode 100644 regression/ebmc-spot/sva-buechi/eventually4.desc create mode 100644 regression/ebmc-spot/sva-buechi/immediate1.desc create mode 100644 regression/ebmc-spot/sva-buechi/initial2.desc create mode 100644 regression/ebmc-spot/sva-buechi/restrict1.bdd.desc create mode 100644 regression/ebmc-spot/sva-buechi/restrict1.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/s_eventually1.bdd.desc create mode 100644 regression/ebmc-spot/sva-buechi/s_eventually3.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence4.bdd.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence4.bmc.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence5.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence6.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_implication1.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_implication2.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_intersect1.desc create mode 100644 regression/ebmc-spot/sva-buechi/sequence_repetition6.desc create mode 100644 regression/ebmc-spot/sva-buechi/static_final1.desc create mode 100644 regression/ebmc-spot/sva-buechi/sva_and1.desc create mode 100644 regression/ebmc-spot/sva-buechi/sva_iff1.desc create mode 100644 regression/ebmc-spot/sva-buechi/sva_implies1.desc create mode 100644 regression/ebmc-spot/sva-buechi/sva_not1.desc create mode 100644 regression/ebmc-spot/sva-buechi/system_verilog_assertion3.desc create mode 100644 src/ebmc/instrument_buechi.cpp create mode 100644 src/ebmc/instrument_buechi.h create mode 100644 src/temporal-logic/hoa.cpp create mode 100644 src/temporal-logic/hoa.h create mode 100644 src/temporal-logic/ltl_sva_to_string.cpp create mode 100644 src/temporal-logic/ltl_sva_to_string.h create mode 100644 src/temporal-logic/ltl_to_buechi.cpp create mode 100644 src/temporal-logic/ltl_to_buechi.h create mode 100644 unit/temporal-logic/ltl_sva_to_string.cpp diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index d66cbf957..6839520f7 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.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 diff --git a/CHANGELOG b/CHANGELOG index 43e8b92d9..287d9252f 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,6 +1,7 @@ # EBMC 5.7 * Verilog: `elsif preprocessor directive +* LTL/SVA to Buechi with --buechi # EBMC 5.6 diff --git a/lib/cbmc b/lib/cbmc index 50be009ae..3c915ebe3 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit 50be009aeec0a21713b20e980b39fa61470a40c0 +Subproject commit 3c915ebe35448a20555c1ef55d51540b52c5c34a diff --git a/regression/ebmc-spot/Makefile b/regression/ebmc-spot/Makefile new file mode 100644 index 000000000..68b2eefbf --- /dev/null +++ b/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 diff --git a/regression/ebmc-spot/ltl-buechi/FGp1.desc b/regression/ebmc-spot/ltl-buechi/FGp1.desc new file mode 100644 index 000000000..f6f835869 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/FGp1.smv b/regression/ebmc-spot/ltl-buechi/FGp1.smv new file mode 100644 index 000000000..0dd410b72 --- /dev/null +++ b/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 diff --git a/regression/ebmc-spot/ltl-buechi/Fp1.desc b/regression/ebmc-spot/ltl-buechi/Fp1.desc new file mode 100644 index 000000000..26ba9ccee --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/Fp1.smv b/regression/ebmc-spot/ltl-buechi/Fp1.smv new file mode 100644 index 000000000..4c220d228 --- /dev/null +++ b/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 diff --git a/regression/ebmc-spot/ltl-buechi/GFp1.desc b/regression/ebmc-spot/ltl-buechi/GFp1.desc new file mode 100644 index 000000000..acc42e335 --- /dev/null +++ b/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. diff --git a/regression/ebmc-spot/ltl-buechi/GFp1.smv b/regression/ebmc-spot/ltl-buechi/GFp1.smv new file mode 100644 index 000000000..cd99bc0fd --- /dev/null +++ b/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 diff --git a/regression/ebmc-spot/ltl-buechi/Gp1.desc b/regression/ebmc-spot/ltl-buechi/Gp1.desc new file mode 100644 index 000000000..f5659eb44 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/Gp1.smv b/regression/ebmc-spot/ltl-buechi/Gp1.smv new file mode 100644 index 000000000..d0fcb3abd --- /dev/null +++ b/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 diff --git a/regression/ebmc-spot/ltl-buechi/Gp2.desc b/regression/ebmc-spot/ltl-buechi/Gp2.desc new file mode 100644 index 000000000..0e491248f --- /dev/null +++ b/regression/ebmc-spot/ltl-buechi/Gp2.desc @@ -0,0 +1,9 @@ +CORE +Gp2.smv +--buechi +^\[.*\] G p: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/ltl-buechi/Gp2.smv b/regression/ebmc-spot/ltl-buechi/Gp2.smv new file mode 100644 index 000000000..69e1ce125 --- /dev/null +++ b/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 diff --git a/regression/ebmc-spot/ltl-buechi/R1.smv b/regression/ebmc-spot/ltl-buechi/R1.smv new file mode 100644 index 000000000..8f941b239 --- /dev/null +++ b/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 diff --git a/regression/ebmc-spot/ltl-buechi/R1p1.desc b/regression/ebmc-spot/ltl-buechi/R1p1.desc new file mode 100644 index 000000000..98620fafa --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/R1p2.desc b/regression/ebmc-spot/ltl-buechi/R1p2.desc new file mode 100644 index 000000000..40a37f5cf --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/R1p3.desc b/regression/ebmc-spot/ltl-buechi/R1p3.desc new file mode 100644 index 000000000..276552362 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/R1p4.desc b/regression/ebmc-spot/ltl-buechi/R1p4.desc new file mode 100644 index 000000000..a6bfa6d91 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/R1p5.desc b/regression/ebmc-spot/ltl-buechi/R1p5.desc new file mode 100644 index 000000000..33d7539fc --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/R1p6.desc b/regression/ebmc-spot/ltl-buechi/R1p6.desc new file mode 100644 index 000000000..f75d4826f --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/Xp1.desc b/regression/ebmc-spot/ltl-buechi/Xp1.desc new file mode 100644 index 000000000..ef5d754a3 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/Xp1.smv b/regression/ebmc-spot/ltl-buechi/Xp1.smv new file mode 100644 index 000000000..424cf3f08 --- /dev/null +++ b/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 diff --git a/regression/ebmc-spot/ltl-buechi/and1.desc b/regression/ebmc-spot/ltl-buechi/and1.desc new file mode 100644 index 000000000..959774a5a --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/and1.smv b/regression/ebmc-spot/ltl-buechi/and1.smv new file mode 100644 index 000000000..fa313d5ec --- /dev/null +++ b/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 + diff --git a/regression/ebmc-spot/ltl-buechi/and2.desc b/regression/ebmc-spot/ltl-buechi/and2.desc new file mode 100644 index 000000000..398a49338 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/and2.smv b/regression/ebmc-spot/ltl-buechi/and2.smv new file mode 100644 index 000000000..3ad65c695 --- /dev/null +++ b/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) + diff --git a/regression/ebmc-spot/ltl-buechi/iff1.desc b/regression/ebmc-spot/ltl-buechi/iff1.desc new file mode 100644 index 000000000..747232a91 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/iff1.smv b/regression/ebmc-spot/ltl-buechi/iff1.smv new file mode 100644 index 000000000..6fc3d251a --- /dev/null +++ b/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 diff --git a/regression/ebmc-spot/ltl-buechi/iff2.desc b/regression/ebmc-spot/ltl-buechi/iff2.desc new file mode 100644 index 000000000..b5acbadc7 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/iff2.smv b/regression/ebmc-spot/ltl-buechi/iff2.smv new file mode 100644 index 000000000..6af005430 --- /dev/null +++ b/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) diff --git a/regression/ebmc-spot/ltl-buechi/implies1.desc b/regression/ebmc-spot/ltl-buechi/implies1.desc new file mode 100644 index 000000000..2b177c3ab --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/implies1.smv b/regression/ebmc-spot/ltl-buechi/implies1.smv new file mode 100644 index 000000000..4651e1345 --- /dev/null +++ b/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 diff --git a/regression/ebmc-spot/ltl-buechi/implies2.desc b/regression/ebmc-spot/ltl-buechi/implies2.desc new file mode 100644 index 000000000..bd8c14375 --- /dev/null +++ b/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 +-- diff --git a/regression/ebmc-spot/ltl-buechi/implies2.smv b/regression/ebmc-spot/ltl-buechi/implies2.smv new file mode 100644 index 000000000..345654ca8 --- /dev/null +++ b/regression/ebmc-spot/ltl-buechi/implies2.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) diff --git a/regression/ebmc-spot/ltl-buechi/or1.desc b/regression/ebmc-spot/ltl-buechi/or1.desc new file mode 100644 index 000000000..f6efd1247 --- /dev/null +++ b/regression/ebmc-spot/ltl-buechi/or1.desc @@ -0,0 +1,9 @@ +CORE +or1.smv +--buechi --bdd +^\[.*\] X p \| X q: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/ltl-buechi/or1.smv b/regression/ebmc-spot/ltl-buechi/or1.smv new file mode 100644 index 000000000..35a424fda --- /dev/null +++ b/regression/ebmc-spot/ltl-buechi/or1.smv @@ -0,0 +1,14 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := FALSE; + next(p) := TRUE; + +VAR q : boolean; + +ASSIGN init(q) := TRUE; + next(q) := FALSE; + +-- should pass +LTLSPEC X p | X q diff --git a/regression/ebmc-spot/ltl-buechi/or2.desc b/regression/ebmc-spot/ltl-buechi/or2.desc new file mode 100644 index 000000000..fbed26c19 --- /dev/null +++ b/regression/ebmc-spot/ltl-buechi/or2.desc @@ -0,0 +1,9 @@ +CORE +or2.smv +--buechi --bdd +^\[.*\] X \(p \| q\): PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/ltl-buechi/or2.smv b/regression/ebmc-spot/ltl-buechi/or2.smv new file mode 100644 index 000000000..b037a3c43 --- /dev/null +++ b/regression/ebmc-spot/ltl-buechi/or2.smv @@ -0,0 +1,14 @@ +MODULE main + +VAR p : boolean; + +ASSIGN init(p) := FALSE; + next(p) := TRUE; + +VAR q : boolean; + +ASSIGN init(q) := TRUE; + next(q) := FALSE; + +-- should pass +LTLSPEC X (p | q) diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay2.desc b/regression/ebmc-spot/sva-buechi/cycle_delay2.desc new file mode 100644 index 000000000..dfb0a4555 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/cycle_delay2.desc @@ -0,0 +1,7 @@ +CORE +../../verilog/SVA/cycle_delay2.sv +--buechi --bound 10 +^\[.*\] ##\[1:2\] main\.x == 2: PROVED up to bound 10$ +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/ebmc-spot/sva-buechi/default_disable1.desc b/regression/ebmc-spot/sva-buechi/default_disable1.desc new file mode 100644 index 000000000..725db4b64 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/default_disable1.desc @@ -0,0 +1,9 @@ +CORE +../../verilog/SVA/default_disable1.sv +--buechi +^file .* line 5: default disable iff is unsupported$ +^EXIT=2$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/eventually4.desc b/regression/ebmc-spot/sva-buechi/eventually4.desc new file mode 100644 index 000000000..2a7d451cf --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/eventually4.desc @@ -0,0 +1,8 @@ +CORE +../../verilog/SVA/eventually4.sv +--buechi --bound 2 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/immediate1.desc b/regression/ebmc-spot/sva-buechi/immediate1.desc new file mode 100644 index 000000000..363029799 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/immediate1.desc @@ -0,0 +1,9 @@ +CORE +../../verilog/SVA/immediate1.sv +--buechi --bound 20 +^\[main\.assert\.1\] always main\.x & 1: PROVED up to bound 20$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/initial2.desc b/regression/ebmc-spot/sva-buechi/initial2.desc new file mode 100644 index 000000000..019005220 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/initial2.desc @@ -0,0 +1,10 @@ +CORE +../../verilog/SVA/initial2.sv +--buechi --module main +^\[main\.assert\.1\] main\.counter == 1: PROVED up to bound \d+$ +^\[main\.assert\.2\] main\.counter == 2: PROVED up to bound \d+$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/restrict1.bdd.desc b/regression/ebmc-spot/sva-buechi/restrict1.bdd.desc new file mode 100644 index 000000000..40e125050 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/restrict1.bdd.desc @@ -0,0 +1,10 @@ +CORE +../../verilog/SVA/restrict1.sv +--buechi --bdd +^\[main\.p0\] always main\.x != 5: ASSUMED$ +^\[main\.p1\] always main\.x != 6: PROVED$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/restrict1.bmc.desc b/regression/ebmc-spot/sva-buechi/restrict1.bmc.desc new file mode 100644 index 000000000..c737b2d57 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/restrict1.bmc.desc @@ -0,0 +1,10 @@ +CORE +../../verilog/SVA/restrict1.sv +--buechi --module main --bound 10 +^\[main\.p0\] always main\.x != 5: ASSUMED$ +^\[main\.p1\] always main\.x != 6: PROVED up to bound 10$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/s_eventually1.bdd.desc b/regression/ebmc-spot/sva-buechi/s_eventually1.bdd.desc new file mode 100644 index 000000000..e2fdca98c --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/s_eventually1.bdd.desc @@ -0,0 +1,8 @@ +CORE +../../verilog/SVA/s_eventually1.sv +--buechi --bdd +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/s_eventually3.desc b/regression/ebmc-spot/sva-buechi/s_eventually3.desc new file mode 100644 index 000000000..aee552805 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/s_eventually3.desc @@ -0,0 +1,8 @@ +KNOWNBUG +../../verilog/SVA/s_eventually3.sv +--buechi --module main --bound 11 +^EXIT=10$ +^SIGNAL=0$ +^\[main\.p0\] always s_eventually main\.counter <= 5: REFUTED$ +-- +^warning: ignoring diff --git a/regression/ebmc-spot/sva-buechi/sequence4.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence4.bdd.desc new file mode 100644 index 000000000..717e5e682 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence4.bdd.desc @@ -0,0 +1,8 @@ +CORE +../../verilog/SVA/sequence4.sv +--buechi --bdd +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence4.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence4.bmc.desc new file mode 100644 index 000000000..620adef3e --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence4.bmc.desc @@ -0,0 +1,8 @@ +CORE +../../verilog/SVA/sequence4.sv +--buechi --bound 10 +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence5.desc b/regression/ebmc-spot/sva-buechi/sequence5.desc new file mode 100644 index 000000000..a331f43e8 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence5.desc @@ -0,0 +1,12 @@ +CORE +../../verilog/SVA/sequence5.sv +--buechi +^\[main\.p0\] 1: PROVED up to bound \d+$ +^\[main\.p1\] 0: REFUTED$ +^\[main\.p2\] 1'bx: REFUTED$ +^\[main\.p3\] 1'bz: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence6.desc b/regression/ebmc-spot/sva-buechi/sequence6.desc new file mode 100644 index 000000000..2a01726a9 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence6.desc @@ -0,0 +1,10 @@ +CORE +../../verilog/SVA/sequence6.sv +--buechi +^\[main\.p0\] \(1 ##1 1\) \|-> main\.x == 1: PROVED up to bound 5$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- + diff --git a/regression/ebmc-spot/sva-buechi/sequence_implication1.desc b/regression/ebmc-spot/sva-buechi/sequence_implication1.desc new file mode 100644 index 000000000..7621d7737 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_implication1.desc @@ -0,0 +1,12 @@ +CORE +../../verilog/SVA/sequence_implication1.sv +--buechi --bound 20 +^\[.*\] always \(\(main\.counter == 1 ##1 main\.counter == 2\) \|-> \(##1 main.counter == 0\)\): PROVED up to bound 20$ +^\[.*\] always \(\(main\.counter == 1 ##1 main\.counter == 2\) \|=> main\.counter == 0\): PROVED up to bound 20$ +^\[.*\] always \(0 \|-> 0\): PROVED up to bound 20$ +^\[.*\] \(1 or \(##1 1\)\) \|-> main\.counter == 0: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_implication2.desc b/regression/ebmc-spot/sva-buechi/sequence_implication2.desc new file mode 100644 index 000000000..450619797 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_implication2.desc @@ -0,0 +1,8 @@ +CORE +../../verilog/SVA/sequence_implication2.sv +--buechi --module main +^file .* line 4: sequence required, but got property$ +^EXIT=2$ +^SIGNAL=0$ +-- +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_intersect1.desc b/regression/ebmc-spot/sva-buechi/sequence_intersect1.desc new file mode 100644 index 000000000..9474b89d0 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_intersect1.desc @@ -0,0 +1,14 @@ +CORE +../../verilog/SVA/sequence_intersect1.sv +--buechi --bound 10 +^\[main\.p0\] main\.x == 0 intersect main\.x == 1: REFUTED$ +^\[main\.p1\] always main\.x >= 0: PROVED up to bound 10$ +^\[main\.p2\] always main\.x <= 5: PROVED up to bound 10$ +^\[main\.p3\] always main\.x <= 3: REFUTED$ +^\[main\.p4\] always \(main\.x >= 0 intersect main\.x <= 5\): PROVED up to bound 10$ +^\[main\.p5\] always \(main\.x >= 0 intersect main\.x <= 3\): REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition6.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition6.desc new file mode 100644 index 000000000..c33fee5a6 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sequence_repetition6.desc @@ -0,0 +1,8 @@ +CORE +../../verilog/SVA/sequence_repetition6.sv +--buechi +^file .* line 4: sequence required, but got property$ +^EXIT=2$ +^SIGNAL=0$ +-- +-- diff --git a/regression/ebmc-spot/sva-buechi/static_final1.desc b/regression/ebmc-spot/sva-buechi/static_final1.desc new file mode 100644 index 000000000..b3d1c6084 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/static_final1.desc @@ -0,0 +1,9 @@ +CORE +../../verilog/SVA/static_final1.sv +--buechi +^\[full_adder\.p0\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED up to bound \d+$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sva_and1.desc b/regression/ebmc-spot/sva-buechi/sva_and1.desc new file mode 100644 index 000000000..11606f320 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sva_and1.desc @@ -0,0 +1,11 @@ +CORE +../../verilog/SVA/sva_and1.sv +--buechi +^\[main\.p0\] always \(1 and 1\): PROVED up to bound \d+$ +^\[main\.p1\] always \(1 and 0\): REFUTED$ +^\[main\.p2\] always \(1 and 32'b0000000000000000000000000000000x\): REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sva_iff1.desc b/regression/ebmc-spot/sva-buechi/sva_iff1.desc new file mode 100644 index 000000000..b2a7ad54a --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sva_iff1.desc @@ -0,0 +1,11 @@ +CORE +../../verilog/SVA/sva_iff1.sv +--buechi +^\[main\.p0\] always \(1 iff 1\): PROVED up to bound \d+$ +^\[main\.p1\] always \(1 iff 0\): REFUTED$ +^\[main\.p2\] always \(1 iff 32'b0000000000000000000000000000000x\): REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sva_implies1.desc b/regression/ebmc-spot/sva-buechi/sva_implies1.desc new file mode 100644 index 000000000..518185134 --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sva_implies1.desc @@ -0,0 +1,11 @@ +CORE +../../verilog/SVA/sva_implies1.sv +--buechi +^\[main\.p0\] always \(1 implies 1\): PROVED up to bound \d+$ +^\[main\.p1\] always \(1 implies 0\): REFUTED$ +^\[main\.p2\] always \(1 implies 32'b0000000000000000000000000000000x\): REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/ebmc-spot/sva-buechi/sva_not1.desc b/regression/ebmc-spot/sva-buechi/sva_not1.desc new file mode 100644 index 000000000..5831727ec --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/sva_not1.desc @@ -0,0 +1,9 @@ +CORE +../../verilog/SVA/sva_not1.sv +--buechi +^\[main\.p0] always not 0: PROVED up to bound \d+$ +^\[main\.p1] always not 1: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/ebmc-spot/sva-buechi/system_verilog_assertion3.desc b/regression/ebmc-spot/sva-buechi/system_verilog_assertion3.desc new file mode 100644 index 000000000..08408689e --- /dev/null +++ b/regression/ebmc-spot/sva-buechi/system_verilog_assertion3.desc @@ -0,0 +1,7 @@ +CORE +../../verilog/SVA/system_verilog_assertion3.sv +--buechi --module main +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index 0c592f5a9..6497d7b0a 100644 --- a/src/ebmc/Makefile +++ b/src/ebmc/Makefile @@ -18,6 +18,7 @@ SRC = \ ebmc_solver_factory.cpp \ ebmc_version.cpp \ instrument_past.cpp \ + instrument_buechi.cpp \ k_induction.cpp \ liveness_to_safety.cpp \ live_signal.cpp \ diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 4d38808fd..3e243e5fc 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ebmc_base.h" #include "ebmc_error.h" #include "ebmc_version.h" +#include "instrument_buechi.h" #include "liveness_to_safety.h" #include "netlist.h" #include "neural_liveness.h" @@ -221,6 +222,10 @@ int ebmc_parse_optionst::doit() return 0; } + // LTL/SVA to Buechi? + if(cmdline.isset("buechi")) + instrument_buechi(transition_system, properties, ui_message_handler); + // possibly apply liveness-to-safety if(cmdline.isset("liveness-to-safety")) liveness_to_safety(transition_system, properties); @@ -386,6 +391,7 @@ void ebmc_parse_optionst::help() " {y--show-properties} \t list the properties in the model\n" " {y--property} {uid} \t check the property with given ID\n" " {y--liveness-to-safety} \t translate liveness properties to safety properties\n" + " {y--buechi} \t translate LTL/SVA properties to Buechi acceptance\n" "\n" "Methods:\n" " {y--k-induction} \t do k-induction with k=bound\n" diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index b9b678e63..6b346444f 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -49,7 +49,7 @@ class ebmc_parse_optionst:public parse_options_baset "(random-traces)(trace-steps):(random-seed):(traces):" "(random-trace)(random-waveform)" "(bmc-with-assumptions)" - "(liveness-to-safety)" + "(liveness-to-safety)(buechi)" "I:D:(preprocess)(systemverilog)(vl2smv-extensions)" "(warn-implicit-nets)", argc, diff --git a/src/ebmc/instrument_buechi.cpp b/src/ebmc/instrument_buechi.cpp new file mode 100644 index 000000000..ba95ebebc --- /dev/null +++ b/src/ebmc/instrument_buechi.cpp @@ -0,0 +1,70 @@ +/*******************************************************************\ + +Module: Buechi Automaton Instrumentation + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "instrument_buechi.h" + +#include +#include +#include + +void instrument_buechi( + transition_systemt &transition_system, + ebmc_propertiest &properties, + message_handlert &message_handler) +{ + for(auto &property : properties.properties) + { + if(!property.is_unknown()) + continue; + + // This is for LTL and some fragment of SVA only. + if( + !is_LTL(property.normalized_expr) && + !is_Buechi_SVA(property.normalized_expr)) + { + continue; + } + + messaget message(message_handler); + message.debug() << "Translating " << property.description << " to Buechi" + << messaget::eom; + + // make the automaton for the negation of the property + auto buechi = + ltl_to_buechi(not_exprt{property.normalized_expr}, message_handler); + + // make a fresh symbol for the state of the automaton + namespacet ns(transition_system.symbol_table); + auto property_symbol = ns.lookup(property.identifier); + + auxiliary_symbolt new_state_symbol{ + id2string(property_symbol.name) + "::buechi_state", + buechi.state_symbol.type(), + property_symbol.mode}; + new_state_symbol.is_state_var = true; + new_state_symbol.module = property_symbol.module; + + buechi.rename_state_symbol(new_state_symbol.symbol_expr()); + + // add the new symbol to the symbol table + transition_system.symbol_table.add(std::move(new_state_symbol)); + + // add the automaton to the transition system + transition_system.trans_expr.init() = + and_exprt{transition_system.trans_expr.init(), buechi.init}; + + transition_system.trans_expr.trans() = + and_exprt{transition_system.trans_expr.trans(), buechi.trans}; + + // Replace the normalized property expression. + // Note that we have negated the property, + // so this is the negation of the Buechi acceptance condition. + property.normalized_expr = + F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}}; + } +} diff --git a/src/ebmc/instrument_buechi.h b/src/ebmc/instrument_buechi.h new file mode 100644 index 000000000..af2005396 --- /dev/null +++ b/src/ebmc/instrument_buechi.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: Buechi Automaton Instrumentation + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +/// \file +/// Buechi Automaton Instrumentation + +#ifndef EBMC_BUECHI_AUTOMATON_INSTRUMENTATION_H +#define EBMC_BUECHI_AUTOMATON_INSTRUMENTATION_H + +#include + +#include "ebmc_properties.h" +#include "transition_system.h" + +void instrument_buechi( + transition_systemt &, + ebmc_propertiest &, + message_handlert &); + +#endif // EBMC_BUECHI_AUTOMATON_INSTRUMENTATION_H diff --git a/src/temporal-logic/Makefile b/src/temporal-logic/Makefile index 79f556a7a..e0bc4dc70 100644 --- a/src/temporal-logic/Makefile +++ b/src/temporal-logic/Makefile @@ -1,5 +1,8 @@ SRC = ctl.cpp \ + hoa.cpp \ ltl.cpp \ + ltl_to_buechi.cpp \ + ltl_sva_to_string.cpp \ nnf.cpp \ normalize_property.cpp \ sva_sequence_match.cpp \ diff --git a/src/temporal-logic/hoa.cpp b/src/temporal-logic/hoa.cpp new file mode 100644 index 000000000..3d432aa3f --- /dev/null +++ b/src/temporal-logic/hoa.cpp @@ -0,0 +1,535 @@ +/*******************************************************************\ + +Module: Hanoi Omega Automata (HOA) Format + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "hoa.h" + +#include + +#include + +#include +#include + +class hoa_tokenizert +{ +public: + explicit hoa_tokenizert(std::istream &_in) : in(_in) + { + } + + struct tokent + { + tokent() = default; + explicit tokent(char ch) : text(1, ch) + { + } + + std::string text, string; + bool is_string() const + { + return text.empty(); + } + bool is_state() const + { + return text == "State:"; + } + bool is_body() const + { + return text == "--BODY--"; + } + bool is_end() const + { + return text == "--END--"; + } + bool is_headername() const + { + // Headernames end on a colon, and are not quoted strings. + return !text.empty() && text.back() == ':'; + } + }; + + const tokent &peek() + { + if(!token_opt.has_value()) + token_opt = get_token(in); + return token_opt.value(); + } + + tokent consume() + { + if(token_opt.has_value()) + { + auto value = std::move(token_opt.value()); + token_opt = {}; + return value; + } + else + { + return get_token(in); + } + } + +protected: + std::istream ∈ + static tokent get_token(std::istream &); + std::optional token_opt; + static bool is_whitespace(char ch) + { + return ch == ' ' || ch == '\r' || ch == '\n' || ch == '\t'; + } +}; + +hoa_tokenizert::tokent hoa_tokenizert::get_token(std::istream &in) +{ + while(true) + { + char ch; + + if(!in.get(ch)) + throw ebmc_errort() << "EOF while reading HOA"; + + if(is_whitespace(ch)) + { + // ignore + } + else if(ch == '/') + { + if(in.peek() == '*') + { + // comment; these may be nested + in.get(ch); // eat * + std::size_t nesting = 1; + while(true) + { + if(!in.get(ch)) + throw ebmc_errort() << "EOF while reading HOA comment"; + if(ch == '*' && in.peek() == '/') + { + in.get(ch); // eat / + nesting--; + if(nesting == 0) + break; // done + } + else if(ch == '/' && in.peek() == '*') + { + in.get(ch); // eat * + nesting++; + } + } + } + else + { + // just a / + return tokent{ch}; + } + } + else if(ch == '"') + { + // quoted string + tokent token; + while(true) + { + if(!in.get(ch)) + throw ebmc_errort() << "EOF while reading HOA string"; + + if(ch == '"') + return token; + else + token.string += ch; + } + } + else if(isalnum(ch) || ch == '_' || ch == '@' || ch == '-') + { + // BOOLEAN, IDENTIFIER, ANAME, HEADERNAME, INT, --BODY--, --END-- + // Dots appear to be allowed in identifiers, in contrast to the definition. + tokent token; + token.text += ch; + auto cont = [](char ch) { + return isalnum(ch) || ch == '_' || ch == '-' || ch == ':' || ch == '.'; + }; + while(cont(in.peek())) + { + in.get(ch); + token.text += ch; + } + return token; + } + else + { + // single-character token, say {}()[] + return tokent{ch}; + } + } +} + +mp_integer hoat::max_state_number() const +{ + mp_integer max = 0; + + for(auto &state : body) + max = std::max(max, state.first.number); + + return max; +} + +class hoa_parsert +{ +public: + explicit hoa_parsert(hoa_tokenizert &_tokenizer) : tokenizer(_tokenizer) + { + } + + hoa_tokenizert &tokenizer; + + using headert = hoat::headert; + using bodyt = hoat::bodyt; + using edgest = hoat::edgest; + using edget = hoat::edget; + using labelt = hoat::labelt; + using state_namet = hoat::state_namet; + using acc_sigt = hoat::acc_sigt; + + headert parse_header(); + bodyt parse_body(); + state_namet parse_state_name(); + edgest parse_edges(); + edget parse_edge(); + labelt parse_label(); + labelt parse_label_expr() + { + return parse_label_expr_or(); + } + labelt parse_label_expr_or(); + labelt parse_label_expr_and(); + labelt parse_label_expr_primary(); + acc_sigt parse_acc_sig(); +}; + +hoat hoat::from_string(const std::string &src) +{ + std::istringstream in(src); + hoa_tokenizert tokenizer(in); + hoa_parsert parser(tokenizer); + + auto header = parser.parse_header(); + auto body = parser.parse_body(); + + return hoat{header, body}; +} + +hoat::headert hoa_parsert::parse_header() +{ + std::string headername; + std::list values; + headert header; + + while(!tokenizer.peek().is_body()) + { + auto token = tokenizer.consume(); + + if(token.is_headername()) + { + if(!headername.empty()) + { + header.emplace_back(headername, std::move(values)); + values.clear(); + } + + if(token.is_headername()) + headername = token.text; + } + else if(token.is_string()) + values.push_back(token.string); + else + values.push_back(token.text); + } + + if(!headername.empty()) + header.emplace_back(headername, std::move(values)); + + return header; +} + +hoat::bodyt hoa_parsert::parse_body() +{ + if(!tokenizer.consume().is_body()) + throw ebmc_errort() << "HOA-parser expected --BODY--"; + + bodyt body; + + while(!tokenizer.peek().is_end()) + { + auto state_name = parse_state_name(); + auto edges = parse_edges(); + body.emplace_back(std::move(state_name), std::move(edges)); + } + + return body; +} + +hoat::state_namet hoa_parsert::parse_state_name() +{ + if(!tokenizer.consume().is_state()) + throw ebmc_errort() << "HOA-parser expected State:"; + + state_namet state_name; + + // label? + if(tokenizer.peek().text == "[") + state_name.label = parse_label(); + + // INT + auto number = tokenizer.consume().text; + state_name.number = string2integer(number); + + // STRING? + if(tokenizer.peek().is_string()) + { + tokenizer.consume(); + } + + // acc-sig? + if(tokenizer.peek().text == "{") + state_name.acc_sig = parse_acc_sig(); + + return state_name; +} + +hoat::edgest hoa_parsert::parse_edges() +{ + edgest edges; + + while(!tokenizer.peek().is_end() && !tokenizer.peek().is_state()) + { + auto edge = parse_edge(); + edges.push_back(std::move(edge)); + } + + return edges; +} + +#include + +hoat::edget hoa_parsert::parse_edge() +{ + edget edge; + + // label? + if(tokenizer.peek().text == "[") + edge.label = parse_label(); + + // state-conj: INT | state-conj "&" INT + edge.dest_states.push_back(string2integer(tokenizer.consume().text)); + while(tokenizer.peek().text == "&") + { + tokenizer.consume(); + edge.dest_states.push_back(string2integer(tokenizer.consume().text)); + } + + // acc-sig? + if(tokenizer.peek().text == "{") + edge.acc_sig = parse_acc_sig(); + + return edge; +} + +hoat::acc_sigt hoa_parsert::parse_acc_sig() +{ + if(tokenizer.consume().text != "{") + throw ebmc_errort() << "HOA-parser expected {"; + + acc_sigt acc_sig; + + while(tokenizer.peek().text != "}") + { + auto token = tokenizer.consume(); + acc_sig.push_back(token.text); + } + + tokenizer.consume(); + + return acc_sig; +} + +hoat::labelt hoa_parsert::parse_label() +{ + if(tokenizer.consume().text != "[") + throw ebmc_errort() << "HOA-parser expected ["; + + auto label = parse_label_expr(); + + if(tokenizer.consume().text != "]") + throw ebmc_errort() << "HOA-parser expected ]"; + + return label; +} + +hoat::labelt hoa_parsert::parse_label_expr_or() +{ + // label-expr ::= label-expr "|" label-expr + auto irep = parse_label_expr_and(); + + while(tokenizer.peek().text == "|") + { + tokenizer.consume(); + auto rhs = parse_label_expr_and(); + irep = irept{"|", {}, {std::move(irep), std::move(rhs)}}; + } + + return irep; +} + +hoat::labelt hoa_parsert::parse_label_expr_and() +{ + // label-expr ::= label-expr "&" label-expr + auto irep = parse_label_expr_primary(); + + while(tokenizer.peek().text == "&") + { + tokenizer.consume(); + auto rhs = parse_label_expr_primary(); + irep = irept{"&", {}, {std::move(irep), std::move(rhs)}}; + } + + return irep; +} + +hoat::labelt hoa_parsert::parse_label_expr_primary() +{ + // label-expr ::= BOOLEAN | INT | ANAME | "!" label-expr + // | "(" label-expr ")" + auto token = tokenizer.consume(); + + if(token.text == "!") + { + auto op = parse_label_expr_primary(); + return irept{"!", {}, {std::move(op)}}; + } + else if(token.text == "(") + { + auto expr = parse_label_expr(); + if(tokenizer.consume().text != ")") + throw ebmc_errort() << "HOA-parser expected )"; + return expr; + } + else + return irept{token.text}; +} + +static void output(std::ostream &out, const hoat::acc_sigt &acc_sig) +{ + if(!acc_sig.empty()) + { + out << " {"; + bool first = true; + for(auto &acc_set : acc_sig) + { + if(first) + first = false; + else + out << ' '; + out << acc_set; + } + out << '}'; + } +} + +static void output(std::ostream &out, const hoat::labelt &label) +{ + if(label.id() == "|") + { + DATA_INVARIANT(label.get_sub().size() == 2, "| must have two operands"); + auto &lhs = label.get_sub()[0]; + auto &rhs = label.get_sub()[1]; + output(out, lhs); + out << label.id(); + output(out, rhs); + } + else if(label.id() == "&") + { + DATA_INVARIANT(label.get_sub().size() == 2, "& must have two operands"); + auto &lhs = label.get_sub()[0]; + auto &rhs = label.get_sub()[1]; + if(lhs.id() == "|") + out << '('; + output(out, lhs); + if(lhs.id() == "|") + out << ')'; + if(rhs.id() == "|") + out << '('; + out << label.id(); + output(out, rhs); + if(rhs.id() == "|") + out << ')'; + } + else if(label.id() == "!") + { + DATA_INVARIANT(label.get_sub().size() == 1, "! must have one operand"); + auto &op = label.get_sub()[0]; + if(op.id() == "|" || op.id() == "&") + out << '('; + out << label.id(); + if(op.id() == "|" || op.id() == "&") + out << ')'; + output(out, op); + } + else + { + out << label.id(); + } +} + +void hoat::output(std::ostream &out) const +{ + for(auto &header_item : header) + { + out << header_item.first; + for(auto &value : header_item.second) + out << ' ' << value; + out << '\n'; + } + + out << "--BODY--\n"; + + for(auto &state : body) + { + out << "State:"; + if(!state.first.label.id().empty()) + { + out << " ["; + ::output(out, state.first.label); + out << ']'; + } + out << ' ' << state.first.number; + ::output(out, state.first.acc_sig); + out << '\n'; + + for(auto &edge : state.second) + { + if(!edge.label.id().empty()) + { + out << '['; + ::output(out, edge.label); + out << "] "; + } + bool first = true; + for(auto &dest : edge.dest_states) + { + if(first) + first = false; + else + out << " & "; + out << dest; + } + ::output(out, edge.acc_sig); + out << '\n'; + } + } + + out << "--END--\n"; +} diff --git a/src/temporal-logic/hoa.h b/src/temporal-logic/hoa.h new file mode 100644 index 000000000..72f5e52c1 --- /dev/null +++ b/src/temporal-logic/hoa.h @@ -0,0 +1,66 @@ +/*******************************************************************\ + +Module: Hanoi Omega Automata (HOA) Format + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_TEMPORAL_LOGIC_HOA_H +#define CPROVER_TEMPORAL_LOGIC_HOA_H + +#include +#include + +#include +#include +#include + +// https://adl.github.io/hoaf/hoaf.pdf +class hoat +{ +public: + // header + using headert = std::list>>; + headert header; + + // body + using labelt = irept; + using acc_sigt = std::vector; + struct state_namet + { + mp_integer number; + labelt label; // in-state condition + acc_sigt acc_sig; + }; + struct edget + { + labelt label; // transition condition + std::vector dest_states; + acc_sigt acc_sig; // acceptance sets + }; + using edgest = std::list; + using bodyt = std::list>; + bodyt body; + + hoat(headert _header, bodyt _body) + : header(std::move(_header)), body(std::move(_body)) + { + } + + static hoat from_string(const std::string &); + void output(std::ostream &) const; + + friend std::ostream &operator<<(std::ostream &out, const hoat &hoa) + { + hoa.output(out); + return out; + } + + mp_integer max_state_number() const; + + // atomic propositions + std::map ap_map; +}; + +#endif // CPROVER_TEMPORAL_LOGIC_HOA_H diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp new file mode 100644 index 000000000..10729071d --- /dev/null +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -0,0 +1,409 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "ltl_sva_to_string.h" + +#include +#include + +#include +#include + +#include "ltl.h" +#include "temporal_expr.h" +#include "temporal_logic.h" + +// https://spot.lre.epita.fr/tl.pdf + +exprt ltl_sva_to_stringt::atom(const std::string &string) const +{ + // map back to number + auto number = safe_string2size_t(string); + + PRECONDITION(number < atoms.size()); + + return atoms[number]; +} + +ltl_sva_to_stringt::resultt +ltl_sva_to_stringt::suffix(std::string s, const exprt &expr, modet mode) +{ + auto op_rec = rec(to_unary_expr(expr).op(), mode); + + auto new_e = to_unary_expr(expr); + new_e.op() = op_rec.e; + + if(op_rec.p == precedencet::ATOM || op_rec.p == precedencet::SUFFIX) + return resultt{precedencet::SUFFIX, op_rec.s + s, new_e}; + else + return resultt{precedencet::SUFFIX, '(' + op_rec.s + ')' + s, new_e}; +} + +ltl_sva_to_stringt::resultt +ltl_sva_to_stringt::prefix(std::string s, const exprt &expr, modet mode) +{ + auto op_rec = rec(to_unary_expr(expr).op(), mode); + + auto new_e = to_unary_expr(expr); + new_e.op() = op_rec.e; + + if(op_rec.p == precedencet::ATOM || op_rec.p == precedencet::PREFIX) + return resultt{precedencet::PREFIX, s + op_rec.s, new_e}; + else + return resultt{precedencet::PREFIX, s + '(' + op_rec.s + ')', new_e}; +} + +ltl_sva_to_stringt::resultt +ltl_sva_to_stringt::infix(std::string s, const exprt &expr, modet mode) +{ + std::string result; + bool first = true; + exprt new_e = expr; // copy + + for(auto &op : new_e.operands()) + { + if(first) + first = false; + else + result += s; + + auto op_rec = rec(op, mode); + op = op_rec.e; + + if(op_rec.p == precedencet::ATOM) + result += op_rec.s; + else + result += '(' + op_rec.s + ')'; + } + + return resultt{precedencet::INFIX, result, new_e}; +} + +ltl_sva_to_stringt::resultt +ltl_sva_to_stringt::rec(const exprt &expr, modet mode) +{ + if(expr.id() == ID_and) + { + return infix("&", expr, mode); + } + else if(expr.id() == ID_or) + { + return infix("|", expr, mode); + } + else if(expr.id() == ID_xor) + { + return infix(" xor ", expr, mode); + } + else if(expr.id() == ID_implies) + { + return infix("->", expr, mode); + } + else if(expr.id() == ID_not) + { + return prefix("!", expr, mode); + } + else if(expr.is_true()) + { + // 1 is preferred, but G1 is parsed as an atom + return resultt{precedencet::ATOM, "true", expr}; + } + else if(expr.is_false()) + { + // 0 is preferred, but G0 is parsed as an atom + return resultt{precedencet::ATOM, "false", expr}; + } + else if(expr.id() == ID_F) + { + PRECONDITION(mode == PROPERTY); + return prefix("F", expr, mode); + } + else if(expr.id() == ID_G) + { + PRECONDITION(mode == PROPERTY); + return prefix("G", expr, mode); + } + else if(expr.id() == ID_X) + { + PRECONDITION(mode == PROPERTY); + return prefix("X", expr, mode); + } + else if(expr.id() == ID_U) + { + PRECONDITION(mode == PROPERTY); + return infix(" U ", expr, mode); + } + else if(expr.id() == ID_weak_U) + { + PRECONDITION(mode == PROPERTY); + return infix(" W ", expr, mode); + } + else if(expr.id() == ID_R) + { + PRECONDITION(mode == PROPERTY); + return infix(" R ", expr, mode); + } + else if(expr.id() == ID_strong_R) + { + PRECONDITION(mode == PROPERTY); + return infix(" M ", expr, mode); + } + else if(expr.id() == ID_sva_always) + { + PRECONDITION(mode == PROPERTY); + return prefix("G", expr, mode); + } + else if(expr.id() == ID_sva_ranged_always) + { + auto &always = to_sva_ranged_always_expr(expr); + auto new_expr = unary_exprt{ID_sva_ranged_always, always.op()}; + auto lower = numeric_cast_v(always.lower()); + if(!always.is_range()) + return prefix("F[" + integer2string(lower) + "]", new_expr, mode); + else if(always.is_unbounded()) + return prefix("F[" + integer2string(lower) + ":]", new_expr, mode); + else + { + auto upper = numeric_cast_v(to_constant_expr(always.upper())); + return prefix( + "F[" + integer2string(lower) + ":" + integer2string(upper) + "]", + new_expr, + mode); + } + } + else if(expr.id() == ID_sva_s_always) + { + throw ebmc_errort{} << "cannot convert " << expr.id() << " to Buechi"; + } + else if(expr.id() == ID_sva_s_eventually) + { + PRECONDITION(mode == PROPERTY); + return prefix("F", expr, mode); + } + else if(expr.id() == ID_sva_ranged_s_eventually) + { + PRECONDITION(mode == PROPERTY); + auto &s_eventually = to_sva_ranged_s_eventually_expr(expr); + auto new_expr = unary_exprt{ID_sva_ranged_s_eventually, s_eventually.op()}; + auto lower = numeric_cast_v(s_eventually.lower()); + if(!s_eventually.is_range()) + return prefix("F[" + integer2string(lower) + "]", new_expr, mode); + else if(s_eventually.is_unbounded()) + return prefix("F[" + integer2string(lower) + ":]", new_expr, mode); + else + { + auto upper = + numeric_cast_v(to_constant_expr(s_eventually.upper())); + return prefix( + "F[" + integer2string(lower) + ":" + integer2string(upper) + "]", + new_expr, + mode); + } + } + else if(expr.id() == ID_sva_s_nexttime) + { + PRECONDITION(mode == PROPERTY); + return prefix("X", expr, mode); + } + else if(expr.id() == ID_sva_nexttime) + { + PRECONDITION(mode == PROPERTY); + return prefix("X", expr, mode); + } + else if(expr.id() == ID_sva_overlapped_implication) + { + // maps to {f}|->g + PRECONDITION(mode == PROPERTY); + auto new_expr = to_sva_overlapped_implication_expr(expr); + new_expr.sequence() = sva_sequence_property_expr_baset{ + ID_sva_implicit_weak, new_expr.sequence()}; + return infix("|->", new_expr, mode); + } + else if(expr.id() == ID_sva_non_overlapped_implication) + { + // maps to {f}|=>g + PRECONDITION(mode == PROPERTY); + auto new_expr = to_sva_non_overlapped_implication_expr(expr); + new_expr.sequence() = sva_sequence_property_expr_baset{ + ID_sva_implicit_weak, new_expr.sequence()}; + return infix("|=>", new_expr, mode); + } + else if( + expr.id() == ID_sva_nonoverlapped_followed_by || + expr.id() == ID_sva_overlapped_followed_by) + { + PRECONDITION(mode == PROPERTY); + throw ebmc_errort{} << "cannot convert " << expr.id() << " to Buechi"; + } + else if(expr.id() == ID_sva_sequence_property) + { + // should have been turned into sva_implicit_weak or sva_implicit_strong + PRECONDITION(false); + } + else if(expr.id() == ID_sva_s_until) + { + PRECONDITION(mode == PROPERTY); + return infix(" U ", expr, mode); + } + else if(expr.id() == ID_sva_s_until_with) + { + // This is release with swapped operands + PRECONDITION(mode == PROPERTY); + auto &until_with = to_sva_s_until_with_expr(expr); + auto R = R_exprt{until_with.rhs(), until_with.lhs()}; // swapped + return rec(R, mode); + } + else if( + expr.id() == ID_sva_weak || expr.id() == ID_sva_strong || + expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong) + { + PRECONDITION(mode == PROPERTY); + // weak closure + auto &sequence = to_sva_sequence_property_expr_base(expr).sequence(); + auto op_rec = rec(sequence, SVA_SEQUENCE); + return resultt{precedencet::ATOM, '{' + op_rec.s + '}', expr}; + } + else if(expr.id() == ID_sva_or) + { + // can be sequence or property + PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE); + return infix("|", expr, mode); + } + else if(expr.id() == ID_sva_and) + { + // can be sequence or property + PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE); + // NLM intersection + return infix("&", expr, mode); + } + else if(expr.id() == ID_sva_sequence_intersect) + { + PRECONDITION(mode == SVA_SEQUENCE); + return infix("&&", expr, mode); + } + else if(expr.id() == ID_sva_boolean) + { + // can be sequence or property + PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE); + return rec(to_sva_boolean_expr(expr).op(), BOOLEAN); + } + else if(expr.id() == ID_sva_sequence_concatenation) + { + PRECONDITION(mode == SVA_SEQUENCE); + // SVA sequence concatenation is overlapping, whereas + // the ; operator is nonoverlapping. We special-case + // the following for better readability: + // f ##0 g --> f : g + // f ##1 g --> f ; g + // f ##n g --> f ; 1[*n-1] ; b + auto &concatenation = to_sva_sequence_concatenation_expr(expr); + if(concatenation.rhs().id() == ID_sva_cycle_delay) + { + auto &delay = to_sva_cycle_delay_expr(concatenation.rhs()); + + auto new_expr = concatenation; + new_expr.rhs() = delay.op(); + + if(delay.is_range()) + { + auto from = numeric_cast_v(delay.from()); + + if(from == 0) + { + // requires treatment of empty sequences on lhs + throw ebmc_errort{} + << "cannot convert 0.. ranged sequence concatenation to Buechi"; + } + else if(delay.is_unbounded()) + { + return infix( + " ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode); + } + else + { + auto to = numeric_cast_v(delay.to()); + PRECONDITION(to >= 0); + return infix( + " ; 1[*" + integer2string(from - 1) + ".." + + integer2string(to - 1) + "] ; ", + new_expr, + mode); + } + } + else + { + auto n = numeric_cast_v(delay.from()); + PRECONDITION(n >= 0); + if(n == 0) + return infix(" : ", new_expr, mode); + else if(n == 1) + return infix(" ; ", new_expr, mode); + else + { + return infix( + " ; 1[*" + integer2string(n - 1) + "] ; ", new_expr, mode); + } + } + } + else + return infix(":", expr, mode); + } + else if(expr.id() == ID_sva_cycle_delay) + { + PRECONDITION(mode == SVA_SEQUENCE); + auto &delay = to_sva_cycle_delay_expr(expr); + unary_exprt new_expr{expr.id(), delay.op()}; + + if(delay.is_range()) + { + auto from = numeric_cast_v(delay.from()); + + if(delay.is_unbounded()) + { + return prefix("1[*" + integer2string(from) + "..] ; ", new_expr, mode); + } + else + { + auto to = numeric_cast_v(delay.to()); + PRECONDITION(to >= 0); + return prefix( + "1[*" + integer2string(from) + ".." + integer2string(to) + "] ; ", + new_expr, + mode); + } + } + else // singleton + { + auto i = numeric_cast_v(delay.from()); + PRECONDITION(i >= 0); + return prefix("1[*" + integer2string(i) + "] ; ", new_expr, mode); + } + } + else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something + { + PRECONDITION(mode == SVA_SEQUENCE); + return suffix("[*]", expr, mode); + } + else if(expr.id() == ID_sva_cycle_delay_plus) // ##[+] something + { + PRECONDITION(mode == SVA_SEQUENCE); + return suffix("[+]", expr, mode); + } + else if(!is_temporal_operator(expr)) + { + auto number = atoms.number(expr); + + // a0, a1, a2, a3, a4, ... + std::string s = "a" + std::to_string(number); + + symbol_exprt new_e{s, expr.type()}; + + return resultt{precedencet::ATOM, s, new_e}; + } + else + throw ebmc_errort{} << "cannot convert " << expr.id() << " to Buechi"; +} diff --git a/src/temporal-logic/ltl_sva_to_string.h b/src/temporal-logic/ltl_sva_to_string.h new file mode 100644 index 000000000..37a74639f --- /dev/null +++ b/src/temporal-logic/ltl_sva_to_string.h @@ -0,0 +1,56 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_TEMPORAL_LOGIC_LTL_SVA_TO_STRING_H +#define CPROVER_TEMPORAL_LOGIC_LTL_SVA_TO_STRING_H + +#include +#include + +/// create formula strings for external LTL to Buechi tools +class ltl_sva_to_stringt +{ +public: + std::string operator()(const exprt &expr) + { + return rec(expr, PROPERTY).s; + } + + exprt atom(const std::string &) const; + +protected: + enum class precedencet + { + ATOM, + PREFIX, + SUFFIX, + INFIX + }; + + struct resultt + { + resultt(precedencet _p, std::string _s, exprt _e) + : p(_p), s(std::move(_s)), e(std::move(_e)) + { + } + precedencet p; + std::string s; + exprt e; + }; + + numberingt atoms; + + using modet = enum { PROPERTY, SVA_SEQUENCE, BOOLEAN }; + + resultt prefix(std::string s, const exprt &, modet); + resultt suffix(std::string s, const exprt &, modet); + resultt infix(std::string s, const exprt &, modet); + resultt rec(const exprt &, modet); +}; + +#endif diff --git a/src/temporal-logic/ltl_to_buechi.cpp b/src/temporal-logic/ltl_to_buechi.cpp new file mode 100644 index 000000000..d6e6ed33b --- /dev/null +++ b/src/temporal-logic/ltl_to_buechi.cpp @@ -0,0 +1,181 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "ltl_to_buechi.h" + +#include +#include +#include +#include +#include +#include +#include + +#include +#include + +#include "hoa.h" +#include "ltl_sva_to_string.h" + +#include + +void buechi_transt::rename_state_symbol(const symbol_exprt &new_state_symbol) +{ + next_symbol_exprt old_next_symbol{ + state_symbol.get_identifier(), state_symbol.type()}; + next_symbol_exprt new_next_symbol{ + new_state_symbol.get_identifier(), state_symbol.type()}; + + replace_mapt replace_map; + replace_map.insert({state_symbol, new_state_symbol}); + replace_map.insert({old_next_symbol, new_next_symbol}); + + replace_expr(replace_map, init); + replace_expr(replace_map, trans); + replace_expr(replace_map, liveness_signal); + + state_symbol = new_state_symbol; +} + +exprt hoa_label_to_expr( + const hoat::labelt &label, + const ltl_sva_to_stringt <l_sva_to_string) +{ + std::vector operands; + operands.reserve(label.get_sub().size()); + for(auto &sub : label.get_sub()) + operands.push_back(hoa_label_to_expr(sub, ltl_sva_to_string)); + + if(label.id() == "t") + { + return true_exprt{}; + } + else if(label.id() == "f") + { + return false_exprt{}; + } + else if(label.id() == "|") + { + PRECONDITION(operands.size() == 2); + return or_exprt{operands}; + } + else if(label.id() == "&") + { + PRECONDITION(operands.size() == 2); + return and_exprt{operands}; + } + else if(label.id() == "!") + { + PRECONDITION(operands.size() == 1); + return not_exprt{operands[0]}; + } + else + { + // atomic proposition, given as number + return ltl_sva_to_string.atom(label.id_string()); + } +} + +buechi_transt +ltl_to_buechi(const exprt &property, message_handlert &message_handler) +{ + // Turn the skeleton of the property into a string + ltl_sva_to_stringt ltl_sva_to_string; + auto string = ltl_sva_to_string(property); + + // Run Spot's ltl2tgba + std::ostringstream hoa_stream; + + messaget message(message_handler); + + message.debug() << "ltl2tgba property: " << string << messaget::eom; + + // State-based Buchi acceptance. Should compare with transition-based + // acceptance. + // Use --complete to be able to have multiple properties in one + // model. + auto run_result = run( + "ltl2tgba", + {"ltl2tgba", "--sba", "--complete", "--hoaf=1.1", string}, + "", + hoa_stream, + ""); + + if(run_result != 0) + throw ebmc_errort{} << "failed to run ltl2tgba"; + + auto hoa = hoat::from_string(hoa_stream.str()); + + message.debug() << hoa << messaget::eom; + + auto max_state_number = hoa.max_state_number(); + auto state_type = range_typet{0, max_state_number}; + const auto buechi_state = symbol_exprt{"buechi::state", state_type}; + const auto buechi_next_state = next_symbol_exprt{"buechi::state", state_type}; + + // construct the initial state constraint + std::vector init_disjuncts; + + for(auto &item : hoa.header) + if(item.first == "Start:") + { + if(item.second.size() != 1) + throw ebmc_errort() << "Start header must have one token"; + auto state_number = string2integer(item.second.front()); + init_disjuncts.push_back( + equal_exprt{buechi_state, from_integer(state_number, state_type)}); + } + + auto init = disjunction(init_disjuncts); + + message.debug() << "Buechi initial state: " << format(init) << messaget::eom; + + // construct the liveness signal + std::vector liveness_disjuncts; + + for(auto &state : hoa.body) + if(!state.first.acc_sig.empty()) + { + liveness_disjuncts.push_back(equal_exprt{ + buechi_state, from_integer(state.first.number, state_type)}); + } + + auto liveness_signal = disjunction(liveness_disjuncts); + + message.debug() << "Buechi liveness signal: " << format(liveness_signal) + << messaget::eom; + + // construct the transition relation + std::vector trans_disjuncts; + + for(auto &state : hoa.body) + { + auto pre = + equal_exprt{buechi_state, from_integer(state.first.number, state_type)}; + for(auto &edge : state.second) + { + if(edge.dest_states.size() != 1) + throw ebmc_errort() << "edge must have one destination state"; + auto cond = hoa_label_to_expr(edge.label, ltl_sva_to_string); + auto post = equal_exprt{ + buechi_next_state, from_integer(edge.dest_states.front(), state_type)}; + trans_disjuncts.push_back(and_exprt{pre, cond, post}); + } + } + + auto trans = disjunction(trans_disjuncts); + + message.debug() << "Buechi transition constraint: " << format(trans) + << messaget::eom; + + return { + buechi_state, + std::move(init), + std::move(trans), + std::move(liveness_signal)}; +} diff --git a/src/temporal-logic/ltl_to_buechi.h b/src/temporal-logic/ltl_to_buechi.h new file mode 100644 index 000000000..39e8b4a4e --- /dev/null +++ b/src/temporal-logic/ltl_to_buechi.h @@ -0,0 +1,41 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_EBMC_LTL_TO_BUECHI_H +#define CPROVER_EBMC_LTL_TO_BUECHI_H + +#include + +struct buechi_transt +{ + symbol_exprt state_symbol; + + exprt init; + exprt trans; + exprt liveness_signal; + + buechi_transt( + symbol_exprt __state_symbol, + exprt __init, + exprt __trans, + exprt __liveness_signal) + : state_symbol(std::move(__state_symbol)), + init(std::move(__init)), + trans(std::move(__trans)), + liveness_signal(std::move(__liveness_signal)) + { + } + + void rename_state_symbol(const symbol_exprt &new_state_symbol); +}; + +class message_handlert; + +buechi_transt ltl_to_buechi(const exprt &formula, message_handlert &); + +#endif diff --git a/src/temporal-logic/sva_sequence_match.cpp b/src/temporal-logic/sva_sequence_match.cpp index fd8bdf080..def3b107f 100644 --- a/src/temporal-logic/sva_sequence_match.cpp +++ b/src/temporal-logic/sva_sequence_match.cpp @@ -131,7 +131,7 @@ std::vector LTL_sequence_matches(const exprt &sequence) if(matches.empty()) return {}; - if(delay.to().is_nil()) + if(!delay.is_range()) { // delay as instructed auto delay_sequence = sva_sequence_matcht::true_match(from_int); @@ -141,13 +141,13 @@ std::vector LTL_sequence_matches(const exprt &sequence) return matches; } - else if(delay.to().id() == ID_infinity) + else if(delay.is_unbounded()) { return {}; // can't encode } - else if(delay.to().is_constant()) + else { - auto to_int = numeric_cast_v(to_constant_expr(delay.to())); + auto to_int = numeric_cast_v(delay.to()); std::vector new_matches; for(mp_integer i = from_int; i <= to_int; ++i) @@ -163,8 +163,6 @@ std::vector LTL_sequence_matches(const exprt &sequence) return new_matches; } - else - return {}; } else if(sequence.id() == ID_sva_and) { diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index 614c642d8..e61c53420 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -214,3 +214,11 @@ std::optional LTL_to_CTL(exprt expr) else return {}; } + +bool is_Buechi_SVA(const exprt &expr) +{ + auto unsupported_operator = [](const exprt &expr) + { return is_temporal_operator(expr) && !is_SVA_operator(expr); }; + + return !has_subexpr(expr, unsupported_operator); +} diff --git a/src/temporal-logic/temporal_logic.h b/src/temporal-logic/temporal_logic.h index fbe82eb76..280e00cbc 100644 --- a/src/temporal-logic/temporal_logic.h +++ b/src/temporal-logic/temporal_logic.h @@ -45,15 +45,15 @@ bool has_RTCTL_operator(const exprt &); /// Returns true iff the given expression is an LTL formula bool is_LTL(const exprt &); -/// Returns true iff the given expression is Gp -bool is_Gp(const exprt &); - /// Returns true iff the given expression is GFp bool is_GFp(const exprt &); /// Returns true iff the given expression is an LTL past formula bool is_LTL_past(const exprt &); +/// Returns true iff the given expression is of the form Gp +bool is_Gp(const exprt &); + /// Returns true iff the given expression has an LTL operator /// as its root bool is_LTL_operator(const exprt &); @@ -85,4 +85,8 @@ std::optional LTL_to_CTL(exprt); /// expression, or otherwise returns {}. std::optional SVA_to_LTL(exprt); +/// Returns true iff the given expression is an SVA expression that +/// we can convert into a Buechi automaton +bool is_Buechi_SVA(const exprt &); + #endif diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index 41464cfc7..c0ea89ca4 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -87,7 +87,7 @@ sequence_matchest instantiate_sequence( auto &sva_cycle_delay_expr = to_sva_cycle_delay_expr(expr); const auto from = numeric_cast_v(sva_cycle_delay_expr.from()); - if(sva_cycle_delay_expr.to().is_nil()) // ##1 something + if(!sva_cycle_delay_expr.is_range()) // ##1 something { const auto u = t + from; @@ -110,19 +110,16 @@ sequence_matchest instantiate_sequence( auto lower = t + from; mp_integer upper; - if(sva_cycle_delay_expr.to().id() == ID_infinity) + if(sva_cycle_delay_expr.is_unbounded()) { DATA_INVARIANT(no_timeframes != 0, "must have timeframe"); upper = no_timeframes; } - else if(sva_cycle_delay_expr.to().is_constant()) + else { - auto to = numeric_cast_v( - to_constant_expr(sva_cycle_delay_expr.to())); + auto to = numeric_cast_v(sva_cycle_delay_expr.to()); upper = t + to; } - else - throw ebmc_errort{} << "failed to convert sva_cycle_delay offsets"; sequence_matchest matches; diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 5d0b47685..0d8c0a22e 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -294,6 +294,16 @@ class sva_ranged_predicate_exprt : public ternary_exprt return static_cast(op0()); } + bool is_range() const + { + return op1().is_not_nil(); + } + + bool is_unbounded() const + { + return op1().id() == ID_infinity; + } + const exprt &upper() const { return op1(); @@ -1007,21 +1017,29 @@ class sva_cycle_delay_exprt : public ternary_exprt return static_cast(op0()); } - // may be nil (just the singleton 'from') or - // infinity (half-open interval starting at 'from') - const exprt &to() const + // May be just the singleton 'from' or + // a half-open interval starting at 'from'. + // Use is_range() and is_unbounded() to distinguish. + const constant_exprt &to() const { - return op1(); + PRECONDITION(is_range() && !is_unbounded()); + return static_cast(op1()); } - exprt &to() + constant_exprt &to() { - return op1(); + PRECONDITION(is_range() && !is_unbounded()); + return static_cast(op1()); + } + + bool is_range() const + { + return op1().is_not_nil(); } bool is_unbounded() const { - return to().id() == ID_infinity; + return op1().id() == ID_infinity; } const exprt &op() const diff --git a/unit/Makefile b/unit/Makefile index 3eb891767..8cfd79bcf 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -5,6 +5,7 @@ SRC = unit_tests.cpp # Test source files SRC += smvlang/expr2smv.cpp \ + temporal-logic/ltl_sva_to_string.cpp \ temporal-logic/nnf.cpp \ # Empty last line diff --git a/unit/temporal-logic/ltl_sva_to_string.cpp b/unit/temporal-logic/ltl_sva_to_string.cpp new file mode 100644 index 000000000..e3dea3de8 --- /dev/null +++ b/unit/temporal-logic/ltl_sva_to_string.cpp @@ -0,0 +1,69 @@ +/*******************************************************************\ + +Module: Property Instrumentation via Buechi Automata + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include +#include + +#include +#include +#include +#include + +SCENARIO("Generating a string from a formula") +{ + GIVEN("A boolean formula") + { + auto p = symbol_exprt{"p", bool_typet{}}; + auto q = symbol_exprt{"q", bool_typet{}}; + + REQUIRE(ltl_sva_to_stringt{}(true_exprt{}) == "true"); + REQUIRE(ltl_sva_to_stringt{}(p) == "a0"); + REQUIRE(ltl_sva_to_stringt{}(and_exprt{p, q}) == "a0&a1"); + } + + GIVEN("An LTL formula") + { + auto p = symbol_exprt{"p", bool_typet{}}; + auto q = symbol_exprt{"q", bool_typet{}}; + + REQUIRE(ltl_sva_to_stringt{}(not_exprt{G_exprt{p}}) == "!Ga0"); + REQUIRE(ltl_sva_to_stringt{}(X_exprt{F_exprt{p}}) == "XFa0"); + REQUIRE(ltl_sva_to_stringt{}(U_exprt{X_exprt{p}, q}) == "(Xa0) U a1"); + REQUIRE(ltl_sva_to_stringt{}(U_exprt{p, q}) == "a0 U a1"); + } + + GIVEN("An SVA formula") + { + auto sequence_type = verilog_sva_sequence_typet{}; + auto p = sva_boolean_exprt{symbol_exprt{"p", bool_typet{}}, sequence_type}; + auto q = sva_boolean_exprt{symbol_exprt{"q", bool_typet{}}, sequence_type}; + + auto sequence = [](const exprt &expr) { + return ltl_sva_to_stringt{}(sva_weak_exprt{ID_sva_weak, expr}); + }; + + REQUIRE( + sequence(sva_cycle_delay_exprt{from_integer(1, natural_typet{}), p}) == + "{1[*1] ; a0}"); + + REQUIRE( + sequence(sva_sequence_concatenation_exprt{ + p, sva_cycle_delay_exprt{from_integer(0, natural_typet{}), q}}) == + "{a0 : a1}"); + + REQUIRE( + sequence(sva_sequence_concatenation_exprt{ + p, sva_cycle_delay_exprt{from_integer(1, natural_typet{}), q}}) == + "{a0 ; a1}"); + + REQUIRE( + sequence(sva_sequence_concatenation_exprt{ + p, sva_cycle_delay_exprt{from_integer(10, natural_typet{}), q}}) == + "{a0 ; 1[*9] ; a1}"); + } +}