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/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}"); + } +}