Proof generation for CFG optimizations (Block coalescing and pruning of unreachable blocks) #63
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Boogie Proof Generation CI | |
| on: | |
| push: | |
| branches: [ master, staging, trying ] | |
| pull_request: | |
| branches: [ master ] | |
| workflow_dispatch: | |
| env: | |
| Z3_VERSION: 4.8.8 | |
| jobs: | |
| build: | |
| strategy: | |
| matrix: | |
| os: [ ubuntu-latest ] | |
| fail-fast: false | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v3 | |
| with: | |
| submodules: 'true' | |
| - name: Setup dotnet | |
| uses: actions/setup-dotnet@v1 | |
| with: | |
| dotnet-version: '6.0.x' | |
| - name: Setup Python | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.10.6' | |
| - name: Get Z3 | |
| run: | | |
| wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-16.04.zip | |
| unzip z3-*.zip | |
| echo $(find $PWD/z3* -name bin -type d)>> $GITHUB_PATH | |
| - name: Compile Boogie proof generation | |
| run: | | |
| dotnet build -c Release Source/Boogie.sln | |
| - name: Generate external benchmark proofs | |
| run: | | |
| BOOGIE_EXE=$(find $PWD -type f -name "BoogieDriver") | |
| python3 etc/scripts/generate_proofs.py --inputdir ProofGenerationBenchmarks/external_benchmarks/modified --outputdir table_benchmarks_proofs --boogieproofExe $BOOGIE_EXE | |
| - name: Get Isabelle | |
| run: | | |
| wget --quiet https://isabelle.in.tum.de/dist/Isabelle2022_linux.tar.gz | |
| tar -xf Isabelle2022_linux.tar.gz | |
| rm Isabelle2022_linux.tar.gz | |
| mv Isabelle2022 isabelle_dir | |
| isabelle_dir/bin/isabelle version | |
| echo isabelle_dir/bin >> $GITHUB_PATH | |
| # add Boogie language session to ROOTS and create heap image (option -b) | |
| # for the session so that it does not have to rechecked every time | |
| - name: Set up Isabelle Boogie language session | |
| run: | | |
| echo "$PWD/foundational_boogie/BoogieLang" >> isabelle_dir/ROOTS | |
| isabelle_dir/bin/isabelle build -b -j4 -d $PWD/foundational_boogie/BoogieLang Boogie_Lang | |
| - name: Check external benchmark proofs | |
| run: | | |
| python3 etc/scripts/check_proofs.py --inputdir table_benchmarks_proofs --reps 1 | |
| - name: Generate CFG optimization benchmarks | |
| run: | | |
| BOOGIE_EXE=$(find $PWD -type f -name "BoogieDriver") | |
| python3 etc/scripts/generate_proofs.py --inputdir ProofGenerationBenchmarks/cfg_optimizations_tests --outputdir cfg_optimizations_proofs --boogieproofExe $BOOGIE_EXE | |
| #- name: Check CFG optimization proofs | |
| # run: | | |
| # python3 etc/scripts/check_proofs.py --inputdir cfg_optimizations_proofs --reps 1 | |
| - name: Generate Boogie benchmark proofs | |
| run: | | |
| BOOGIE_EXE=$(find $PWD -type f -name "BoogieDriver") | |
| python3 etc/scripts/generate_proofs.py --inputdir ProofGenerationBenchmarks/boogie_testsuite_benchmarks --outputdir boogie_benchmarks_proofs --boogieproofExe $BOOGIE_EXE | |
| - name: Check Boogie benchmark proofs | |
| run: | | |
| python3 etc/scripts/check_proofs.py --inputdir boogie_benchmarks_proofs --reps 1 |