diff --git a/.github/workflows/continuous_integration.yml b/.github/workflows/continuous_integration.yml index ed0a8748..968161e3 100644 --- a/.github/workflows/continuous_integration.yml +++ b/.github/workflows/continuous_integration.yml @@ -1,24 +1,124 @@ name: Continuous integration -on: [push, pull_request] +on: [push, pull_request, workflow_dispatch] jobs: - test: + format: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 - - run: cargo test --all + - uses: actions/checkout@v4 + - run: cargo fmt --all -- --check - format: + clippy: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 - - run: cargo fmt --all -- --check + - uses: actions/checkout@v4 + - run: cargo clippy --all -- -D warnings - clippy: + test: + # will wait for new cache on push to main branch, otherwise will run straight away with existing cache + needs: generate_log + strategy: + matrix: + z3version: ['4.8.7', '4.12.2'] + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + - id: configure-z3-id + run: echo "z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')" >> $GITHUB_OUTPUT + - uses: actions/cache/restore@v3 + with: + path: logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2 + key: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-${{ github.sha }} + - id: extract-cache + run: tar -xf "logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2" + - run: cargo test --all + + generate_log: + # only run this job on push to main branch + if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch' + strategy: + matrix: + z3version: ['4.8.7', '4.12.2'] + + # for versions of Z3 at least 4.9.0 we need v1.3 of the GitHub action, for older versions of Z3, 1.2.2 runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 - - run: cargo clippy --all -- -D warnings \ No newline at end of file + - uses: actions/checkout@v3 # this copies the whole repository + with: + fetch-depth: 0 # needed, see GitHub Action "Changed Files" + + - name: Install Z3 for older version + uses: pavpanchekha/setup-z3@1.2.2 # see GitHub Action "Install Z3" + if: ${{ matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9' }} + with: + version: ${{ matrix.z3version }} + + - name: Install Z3 for newer version + uses: pavpanchekha/setup-z3@v1.3 # see GitHub Action "Install Z3" + if: ${{ !(matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9') }} + with: + version: ${{ matrix.z3version }} + + - name: Configure Z3 version environment variable + id: configure-z3-id + run: + echo "z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')" >> $GITHUB_OUTPUT + + - name: Cache log files + id: cache-log + uses: actions/cache@v3 + with: + path: logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2 + key: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-${{ github.sha }} + restore-keys: | + logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}- + + - name: Run Z3 solver on changed smt2 files and compress + id: run_z3_and_upload + env: + CACHE_FILE: logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2 + run: | + # Create the 'logs' directory + mkdir logs + test -f "${CACHE_FILE}" && tar -xf "${CACHE_FILE}" || echo "No cache" + + # Loop through all files and check that log exists + for file in smt-problems/**/*.smt2; do + test -f "$file" || break + # Get the file hash + file_hash=$(shasum -a 256 "$file" | cut -d' ' -f1) + # Get the filename without extension + base_name=$(basename "${file%.*}") + # Log file name + log_file_name="logs/${base_name}_fHash_${file_hash}.log" + test -f "${log_file_name}" && continue + + rm -f "logs/${base_name}_fHash_*.log" + echo "Processing $file to $log_file_name" + # Run Z3 solver for the file and save the log in the 'logs' directory, TODO: `proof=true`? + z3 trace=true proof=true trace-file-name=${log_file_name} ./$file > /dev/null || echo "!!! Error processing $file" + done + + # Compress the 'logs' directory using bzip2 + echo "Compressing to ${CACHE_FILE}" + tar -cjf "${CACHE_FILE}" logs/ + + # TODO: not enough permission for this. + # - name: Delete old cache + # run: | + # echo "Fetching list of cache key" + # cacheKeys=$(gh cache list -R $REPO | cut -f 1) + + # ## Setting this to not fail the workflow while deleting cache keys. + # set +e + # for cacheKey in $cacheKeys; do + # echo "Deleting $cacheKey" + # gh cache delete $cacheKey -R $REPO + # done + # env: + # GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + # REPO: ${{ github.repository }} diff --git a/.github/workflows/z3_trace_log_gen.yml b/.github/workflows/z3_trace_log_gen.yml deleted file mode 100644 index a153fc44..00000000 --- a/.github/workflows/z3_trace_log_gen.yml +++ /dev/null @@ -1,94 +0,0 @@ -name: Z3 Trace Log Generator - -on: - push: - branches: [ "main" ] - - # job can also be triggered manually on GitHub - workflow_dispatch: - -jobs: - generate_log: - strategy: - matrix: - z3version: ['4.12.2'] - - # for versions of Z3 at least 4.9.0 we need v1.3 of the GitHub action, for older versions of Z3, 1.2.2 - runs-on: ubuntu-latest - - steps: - - uses: actions/checkout@v3 # this copies the whole repository - with: - fetch-depth: 0 # needed, see GitHub Action "Changed Files" - - - name: Install Z3 for older version - uses: pavpanchekha/setup-z3@1.2.2 # see GitHub Action "Install Z3" - if: ${{ matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9' }} - with: - version: ${{ matrix.z3version }} - - - name: Install Z3 for newer version - uses: pavpanchekha/setup-z3@v1.3 # see GitHub Action "Install Z3" - if: ${{ !(matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9') }} - with: - version: ${{ matrix.z3version }} - - - name: Configure Z3 version environment variable - id: configure-z3-id - run: - echo "z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')" >> $GITHUB_OUTPUT - - - name: Cache log files - id: cache-log - uses: actions/cache@v3 - with: - path: logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2 - key: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-${{ github.sha }} - restore-keys: | - logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}- - - - name: Run Z3 solver on changed smt2 files and compress - id: run_z3_and_upload - env: - CACHE_FILE: logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2 - run: | - # Create the 'logs' directory - mkdir logs - test -f "${CACHE_FILE}" && tar -xf "${CACHE_FILE}" || echo "No cache" - - # Loop through all files and check that log exists - for file in smt-problems/**/*.smt2; do - test -f "$file" || break - # Get the file hash - file_hash=$(shasum -a 256 "$file" | cut -d' ' -f1) - # Get the filename without extension - base_name=$(basename "${file%.*}") - # Log file name - log_file_name="logs/${base_name}_fHash_${file_hash}.log" - test -f "${log_file_name}" && continue - - rm -f "logs/${base_name}_fHash_*.log" - echo "Processing $file to $log_file_name" - # Run Z3 solver for the file and save the log in the 'logs' directory, TODO: `proof=true`? - z3 trace=true proof=true trace-file-name=${log_file_name} ./$file > /dev/null || echo "!!! Error processing $file" - done - - # Compress the 'logs' directory using bzip2 - echo "Compressing to ${CACHE_FILE}" - tar -cjf "${CACHE_FILE}" logs/ - - # TODO: not enough permission for this. - # - name: Delete old cache - # run: | - # echo "Fetching list of cache key" - # cacheKeys=$(gh cache list -L 100 | cut -f 1) - - # ## Setting this to not fail the workflow while deleting cache keys. - # set +e - # for cacheKey in $cacheKeys; do - # echo "Deleting $cacheKey" - # gh cache delete $cacheKey -R $REPO - # done - # env: - # GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} - # REPO: ${{ github.repository }} diff --git a/smt-log-parser/src/lib.rs b/smt-log-parser/src/lib.rs index 74b211a5..359fd3b7 100644 --- a/smt-log-parser/src/lib.rs +++ b/smt-log-parser/src/lib.rs @@ -6,3 +6,6 @@ pub mod parsers; /// Pretty printing for items. pub mod display_with; + +pub use parsers::LogParser; +pub use parsers::z3::z3parser::Z3Parser; diff --git a/smt-log-parser/src/parsers/z3/mod.rs b/smt-log-parser/src/parsers/z3/mod.rs index 9df3ef54..b7e5bc51 100644 --- a/smt-log-parser/src/parsers/z3/mod.rs +++ b/smt-log-parser/src/parsers/z3/mod.rs @@ -17,7 +17,7 @@ impl LogParser for T { first_byte == b'[' } - fn process_line(&mut self, line: &str, _line_no: usize) -> bool { + fn process_line(&mut self, line: &str, line_no: usize) -> bool { // Much faster than `split_whitespace` or `split(' ')` since it works on // [u8] instead of [char] and so doesn't need to convert to UTF-8. let mut split = line.split_ascii_whitespace(); @@ -52,7 +52,11 @@ impl LogParser for T { "[conflict]" => self.conflict(split), _ => None, }; - parse.unwrap_or_else(|| eprintln!("Error parsing line: {line:?}")); + parse.unwrap_or_else(|| if std::env::var("SLP_TEST_MODE").is_ok() { + panic!("Error parsing line {line_no}: {line:?}"); + } else { + eprintln!("Error parsing line {line_no}: {line:?}") + }); true } diff --git a/smt-log-parser/tests/parse_logs.rs b/smt-log-parser/tests/parse_logs.rs new file mode 100644 index 00000000..02128784 --- /dev/null +++ b/smt-log-parser/tests/parse_logs.rs @@ -0,0 +1,19 @@ +use std::time::Duration; + +use smt_log_parser::{LogParser, Z3Parser}; + +#[test] +fn parse_all_logs() { + std::env::set_var("SLP_TEST_MODE", "true"); + + let all_logs = std::fs::read_dir("../logs").unwrap(); + for log in all_logs { + let filename = log.unwrap().path(); + println!("Parsing {}", filename.display()); + let (metadata, parser) = Z3Parser::from_file(filename).unwrap(); + // Gives 10 millis per MB (or 10 secs per GB) + let to = Duration::from_millis(500 + (metadata.len() / 100_000)); + let (timeout, _result) = parser.process_all_timeout(to); + assert!(timeout.is_none()); + } +}