From 9ccd7aee63b23bebe59229bb388cfefb26d186ab Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Mon, 9 Jan 2023 18:29:40 -0500 Subject: [PATCH 1/6] Added kani integration. --- .../continuous-integration-workflow.yaml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/.github/workflows/continuous-integration-workflow.yaml b/.github/workflows/continuous-integration-workflow.yaml index f4287198e..330d03b91 100644 --- a/.github/workflows/continuous-integration-workflow.yaml +++ b/.github/workflows/continuous-integration-workflow.yaml @@ -96,6 +96,21 @@ jobs: command: test args: --no-default-features + kani: + runs-on: ubuntu-latest + steps: + - name: checkout + uses: actions/checkout@v3 + with: + submodules: recursive + - name: Verify with Kani + uses: model-checking/kani-github-action@02764e1 + with: + working-directory: prost + args: --tests -p prost-types --default-unwind 3 \ + --harness "tests::check_timestamp_roundtrip_via_system_time" + enable-propproof: true + no-std: runs-on: ubuntu-latest steps: From 89e6c6442cf7e3ce58ffd0a22b9c01e979c3e742 Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Mon, 9 Jan 2023 18:46:01 -0500 Subject: [PATCH 2/6] Fix yaml problem. --- .github/workflows/continuous-integration-workflow.yaml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/continuous-integration-workflow.yaml b/.github/workflows/continuous-integration-workflow.yaml index 330d03b91..b90c4813b 100644 --- a/.github/workflows/continuous-integration-workflow.yaml +++ b/.github/workflows/continuous-integration-workflow.yaml @@ -107,8 +107,9 @@ jobs: uses: model-checking/kani-github-action@02764e1 with: working-directory: prost - args: --tests -p prost-types --default-unwind 3 \ - --harness "tests::check_timestamp_roundtrip_via_system_time" + args: | + --tests -p prost-types --default-unwind 3 \ + --harness "tests::check_timestamp_roundtrip_via_system_time" enable-propproof: true no-std: From 2874b990900e7903b07db1b59bfa1233f3891998 Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Mon, 9 Jan 2023 18:46:46 -0500 Subject: [PATCH 3/6] yaml hash problem --- .github/workflows/continuous-integration-workflow.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/continuous-integration-workflow.yaml b/.github/workflows/continuous-integration-workflow.yaml index b90c4813b..1b97f23c1 100644 --- a/.github/workflows/continuous-integration-workflow.yaml +++ b/.github/workflows/continuous-integration-workflow.yaml @@ -104,7 +104,7 @@ jobs: with: submodules: recursive - name: Verify with Kani - uses: model-checking/kani-github-action@02764e1 + uses: model-checking/kani-github-action@02764e122079011adaf31e7d0630a8841d277507 with: working-directory: prost args: | From 1f898d66891d6e15c1afa675c5ae08ab4c032509 Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Mon, 9 Jan 2023 18:50:28 -0500 Subject: [PATCH 4/6] No need to cd? --- .github/workflows/continuous-integration-workflow.yaml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/continuous-integration-workflow.yaml b/.github/workflows/continuous-integration-workflow.yaml index 1b97f23c1..78cd6182b 100644 --- a/.github/workflows/continuous-integration-workflow.yaml +++ b/.github/workflows/continuous-integration-workflow.yaml @@ -106,7 +106,6 @@ jobs: - name: Verify with Kani uses: model-checking/kani-github-action@02764e122079011adaf31e7d0630a8841d277507 with: - working-directory: prost args: | --tests -p prost-types --default-unwind 3 \ --harness "tests::check_timestamp_roundtrip_via_system_time" From ada582872ed1aa9ce6cdf6336616f0c6b50cad90 Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Wed, 11 Jan 2023 15:41:58 -0500 Subject: [PATCH 5/6] Use new release, not the hash --- .github/workflows/continuous-integration-workflow.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/continuous-integration-workflow.yaml b/.github/workflows/continuous-integration-workflow.yaml index 78cd6182b..df05fe7a2 100644 --- a/.github/workflows/continuous-integration-workflow.yaml +++ b/.github/workflows/continuous-integration-workflow.yaml @@ -104,7 +104,7 @@ jobs: with: submodules: recursive - name: Verify with Kani - uses: model-checking/kani-github-action@02764e122079011adaf31e7d0630a8841d277507 + uses: model-checking/kani-github-action@v0.19 with: args: | --tests -p prost-types --default-unwind 3 \ From 1d567753ab694068bcb521ef6934a5d5e643bbf8 Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Fri, 13 Jan 2023 01:16:21 -0500 Subject: [PATCH 6/6] Added comment describing the unwind value. --- .github/workflows/continuous-integration-workflow.yaml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.github/workflows/continuous-integration-workflow.yaml b/.github/workflows/continuous-integration-workflow.yaml index df05fe7a2..233c5c859 100644 --- a/.github/workflows/continuous-integration-workflow.yaml +++ b/.github/workflows/continuous-integration-workflow.yaml @@ -106,10 +106,16 @@ jobs: - name: Verify with Kani uses: model-checking/kani-github-action@v0.19 with: + enable-propproof: true args: | --tests -p prost-types --default-unwind 3 \ --harness "tests::check_timestamp_roundtrip_via_system_time" - enable-propproof: true + # --default-unwind N roughly corresponds to how much effort + # Kani will spend trying to prove correctness of the + # program. Higher the number, more programs can be proven + # correct. However, Kani will require more time and memory. If + # Kani fails with "Failed Checks: unwinding assertion," this + # number may need to be raised for Kani to succeed. no-std: runs-on: ubuntu-latest