[Prover] Fix bug in loop unrolling #15136

rahxephon89 · 2024-10-31T05:26:41Z

Description

Currently, loop analysis collects bytecode for unrolling loops and returns a vector of basic blocks, which will be directly flatten later. This implementation will lead to incorrect boogie code if a block in the vector falls through to its successor in the original CFG but the next element in the vector is actually not its successor. The bug leads to verification failure shown in #15044 when CFG simplification is turned on. This PR fixes the issue by inserting the explicit jump instruction.

Close #15044

How Has This Been Tested?

existing tests pass;
a new test;

Key Areas to Review

The code change will only influence bounded verification with unroll pragma. Need to make sure this change will not affect other part of the prover.

Type of Change

Which Components or Systems Does This Change Impact?

Checklist

I have read and followed the CONTRIBUTING doc
I have performed a self-review of my own code
I have commented my code, particularly in hard-to-understand areas
I identified and added all stakeholders and component owners affected by this change as reviewers
I tested both happy and unhappy path of the functionality
I have made corresponding changes to the documentation

trunk-io · 2024-10-31T05:26:45Z

⏱️ 1h 52m total CI duration on this PR

Slowest 15 Jobs	Cumulative Duration	Recent Runs
execution-performance / single-node-performance	23m	🟩
rust-move-tests	10m	🟩
rust-move-tests	9m	🟩
rust-move-tests	9m	🟩
rust-move-tests	9m	🟩
rust-cargo-deny	9m	🟩 🟩 🟩 🟩 🟩
rust-move-tests	9m	🟩
check-dynamic-deps	5m	🟩 🟩 🟩 🟩 🟩 (+1 more)
rust-doc-tests	5m	🟩
execution-performance / test-target-determinator	4m	🟩
test-target-determinator	4m	🟩
check	4m	🟩
permission-check	3m	🟩 🟩 🟩 🟩 🟩 (+1 more)
general-lints	2m	🟩 🟩 🟩 🟩 🟩
semgrep/ci	2m	🟩 🟩 🟩 🟩 🟩 (+1 more)

🚨 1 job on the last run was significantly faster/slower than expected

Job	Duration	vs 7d avg	Delta
permission-check	3m	2s

_{settings ⋅ feedback ⋅ docs ⋅ learn more about trunk.io}

rahxephon89 · 2024-10-31T05:39:43Z

third_party/move/move-prover/tests/sources/functional/aborts_if.v2_exp

@@ -102,7 +102,7 @@ error: abort not covered by any of the `aborts_if` clauses
    ┌─ tests/sources/functional/aborts_if.move:139:5
    │
 137 │           if (x == 2 || x == 3) abort 1;
-    │                         ------ abort happened here with code 0x1


This is due to cfg simplification

Do we have an issue to track the expression attribution being so wrong in V2 here? V1 shows the abort at the abort expression.

will file one once it is landed

rahxephon89 · 2024-10-31T05:39:58Z

third_party/move/move-prover/tests/sources/functional/bv_aborts.v2_exp

   =     at tests/sources/functional/bv_aborts.move:16: assert_with_spec (spec)

 error: abort not covered by any of the `aborts_if` clauses
   ┌─ tests/sources/functional/bv_aborts.move:14:5
   │
-12 │           assert!(x > 815);


This is due to cfg simplification

rahxephon89 · 2024-10-31T17:19:57Z

[Prover] Fix bug in loop unrolling #15136 👈
main

This stack of pull requests is managed by Graphite. Learn more about stacking.

Join @rahxephon89 and the rest of your teammates on Graphite

rahxephon89 · 2024-10-31T18:33:38Z

third_party/move/move-model/bytecode/ast-generator-tests/tests/conditionals.exp

@@ -20,11 +20,11 @@ fun m::if_1($t0|c: bool): u8 {
  1: $t1 := $t2
  2: $t3 := move($t0)
  3: if ($t3) goto 4 else goto 8
-  4: label L1


change of exp files in this crate is due to cfg simplification.

rahxephon89 · 2024-10-31T18:33:46Z

third_party/move/tools/move-decompiler/tests/fixed_point32.exp

@@ -15,24 +15,23 @@ module 0x1::fixed_point32 {
        *&(&self).value >> 32u8
    }
    public fun create_from_rational(numerator: u64, denominator: u64): FixedPoint32 {
-        let _t5;


change of exp files in this crate is due to cfg simplification.

brmataptos

PR looks ok. Existing tests and error outputs look like they could be improved.

brmataptos · 2024-11-01T18:51:28Z

third_party/move/move-prover/tests/sources/functional/aborts_if.v2_exp

@@ -102,7 +102,7 @@ error: abort not covered by any of the `aborts_if` clauses
    ┌─ tests/sources/functional/aborts_if.move:139:5
    │
 137 │           if (x == 2 || x == 3) abort 1;
-    │                         ------ abort happened here with code 0x1


Do we have an issue to track the expression attribution being so wrong in V2 here? V1 shows the abort at the abort expression.

brmataptos · 2024-11-01T18:58:09Z

third_party/move/move-prover/tests/sources/functional/bv_aborts.v2_exp

+   │   ╰─────' abort happened here
+14 │ ╭       spec assert_with_spec  {
+15 │ │           // This will fail
+16 │ │           aborts_if x > 815 with std::error::internal(0) | (0xCA26CBD9BE << 24);


Should we have a test that includes a spec which passes? This is an oddly specific spec to be the only test of its kind.

fEst1ck

LGTM

rahxephon89 · 2024-11-04T19:54:36Z

third_party/move/move-model/bytecode/ast-generator-tests/tests/abort_example.exp

@@ -18,58 +18,50 @@ public fun m::f($t0|length: u64): u64 {
     var $t5: bool
     var $t6: u64
     var $t7: u64
-     var $t8: u64


change of exp files in this crate is due to cfg simplification.

wrwg · 2024-11-04T23:52:12Z

third_party/move/move-model/bytecode/src/fat_loop.rs

+            .collect();
+        let mut results = vec![];
+        for (i, (block_id, block)) in blocks.iter().enumerate() {
+            // if this block has one successor and the last bc of this block is not a branch


"If this is a fall-through block (block has one successor...)" we need to remove it by ...
The fatloop algorithm doesn't support fallthrough.

github-actions · 2024-11-05T01:24:40Z

✅ Forge suite `realistic_env_max_load` success on `b7acb475991b4161323e13eb191e13a0f82d8a39`

two traffics test: inner traffic : committed: 14468.94 txn/s, latency: 2747.06 ms, (p50: 2700 ms, p70: 2700, p90: 2900 ms, p99: 3300 ms), latency samples: 5501420
two traffics test : committed: 99.89 txn/s, latency: 1483.96 ms, (p50: 1400 ms, p70: 1400, p90: 1600 ms, p99: 6900 ms), latency samples: 1860
Latency breakdown for phase 0: ["MempoolToBlockCreation: max: 2.030, avg: 1.575", "ConsensusProposalToOrdered: max: 0.315, avg: 0.291", "ConsensusOrderedToCommit: max: 0.373, avg: 0.360", "ConsensusProposalToCommit: max: 0.662, avg: 0.652"]
Max non-epoch-change gap was: 0 rounds at version 0 (avg 0.00) [limit 4], 0.90s no progress at version 2962755 (avg 0.20s) [limit 15].
Max epoch-change gap was: 0 rounds at version 0 (avg 0.00) [limit 4], 8.62s no progress at version 2962753 (avg 8.62s) [limit 15].
Test Ok

github-actions · 2024-11-05T01:28:03Z

✅ Forge suite `framework_upgrade` success on `1086a5e00d773704731ab84fb4ed3538613b2250` ==> `b7acb475991b4161323e13eb191e13a0f82d8a39`

Compatibility test results for 1086a5e00d773704731ab84fb4ed3538613b2250 ==> b7acb475991b4161323e13eb191e13a0f82d8a39 (PR)
Upgrade the nodes to version: b7acb475991b4161323e13eb191e13a0f82d8a39
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1358.10 txn/s, submitted: 1360.97 txn/s, failed submission: 2.87 txn/s, expired: 2.87 txn/s, latency: 2165.22 ms, (p50: 2100 ms, p70: 2400, p90: 3000 ms, p99: 4500 ms), latency samples: 123220
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1440.52 txn/s, submitted: 1444.25 txn/s, failed submission: 3.74 txn/s, expired: 3.74 txn/s, latency: 2157.91 ms, (p50: 2100 ms, p70: 2100, p90: 3300 ms, p99: 4800 ms), latency samples: 131100
5. check swarm health
Compatibility test for 1086a5e00d773704731ab84fb4ed3538613b2250 ==> b7acb475991b4161323e13eb191e13a0f82d8a39 passed
Upgrade the remaining nodes to version: b7acb475991b4161323e13eb191e13a0f82d8a39
framework_upgrade::framework-upgrade::full-framework-upgrade : committed: 1217.12 txn/s, submitted: 1219.82 txn/s, failed submission: 2.70 txn/s, expired: 2.70 txn/s, latency: 2467.99 ms, (p50: 2100 ms, p70: 2700, p90: 3900 ms, p99: 6000 ms), latency samples: 108160
Test Ok

github-actions · 2024-11-05T01:28:44Z

✅ Forge suite `compat` success on `1086a5e00d773704731ab84fb4ed3538613b2250` ==> `b7acb475991b4161323e13eb191e13a0f82d8a39`

Compatibility test results for 1086a5e00d773704731ab84fb4ed3538613b2250 ==> b7acb475991b4161323e13eb191e13a0f82d8a39 (PR)
1. Check liveness of validators at old version: 1086a5e00d773704731ab84fb4ed3538613b2250
compatibility::simple-validator-upgrade::liveness-check : committed: 14149.61 txn/s, latency: 1966.89 ms, (p50: 1800 ms, p70: 1900, p90: 2400 ms, p99: 6300 ms), latency samples: 549420
2. Upgrading first Validator to new version: b7acb475991b4161323e13eb191e13a0f82d8a39
compatibility::simple-validator-upgrade::single-validator-upgrading : committed: 6845.30 txn/s, latency: 4176.82 ms, (p50: 4900 ms, p70: 5000, p90: 5100 ms, p99: 5200 ms), latency samples: 125080
compatibility::simple-validator-upgrade::single-validator-upgrade : committed: 6207.93 txn/s, latency: 5117.14 ms, (p50: 5200 ms, p70: 5200, p90: 7200 ms, p99: 7400 ms), latency samples: 232200
3. Upgrading rest of first batch to new version: b7acb475991b4161323e13eb191e13a0f82d8a39
compatibility::simple-validator-upgrade::half-validator-upgrading : committed: 6421.47 txn/s, latency: 4265.88 ms, (p50: 4900 ms, p70: 5200, p90: 5700 ms, p99: 5900 ms), latency samples: 115500
compatibility::simple-validator-upgrade::half-validator-upgrade : committed: 6502.52 txn/s, latency: 4955.84 ms, (p50: 5400 ms, p70: 5500, p90: 6700 ms, p99: 6900 ms), latency samples: 214820
4. upgrading second batch to new version: b7acb475991b4161323e13eb191e13a0f82d8a39
compatibility::simple-validator-upgrade::rest-validator-upgrading : committed: 10006.47 txn/s, latency: 2750.44 ms, (p50: 2900 ms, p70: 3400, p90: 3700 ms, p99: 3900 ms), latency samples: 179300
compatibility::simple-validator-upgrade::rest-validator-upgrade : committed: 9475.83 txn/s, latency: 3360.41 ms, (p50: 3200 ms, p70: 3600, p90: 5500 ms, p99: 6000 ms), latency samples: 307760
5. check swarm health
Compatibility test for 1086a5e00d773704731ab84fb4ed3538613b2250 ==> b7acb475991b4161323e13eb191e13a0f82d8a39 passed
Test Ok

rahxephon89 commented Oct 31, 2024

View reviewed changes

rahxephon89 changed the title ~~[WIP][Prover] Fix bug in loop unrolling~~ [Prover] Fix bug in loop unrolling Oct 31, 2024

rahxephon89 marked this pull request as ready for review October 31, 2024 19:18

rahxephon89 requested review from wrwg, vineethk, brmataptos and fEst1ck October 31, 2024 20:02

brmataptos approved these changes Nov 1, 2024

View reviewed changes

rahxephon89 force-pushed the teng/fix-15044 branch from 1dfc271 to 98b0aeb Compare November 3, 2024 22:54

fEst1ck approved these changes Nov 4, 2024

View reviewed changes

rahxephon89 commented Nov 4, 2024

View reviewed changes

wrwg approved these changes Nov 4, 2024

View reviewed changes

rahxephon89 added 4 commits November 4, 2024 16:40

fix bug in loop unrolling

4f44c62

ast generator tests

4e75351

decompiler tests

f05c09b

fix

b7acb47

rahxephon89 force-pushed the teng/fix-15044 branch from 98b0aeb to b7acb47 Compare November 5, 2024 00:57

rahxephon89 enabled auto-merge (squash) November 5, 2024 00:57

This comment has been minimized.

Sign in to view

rahxephon89 merged commit a45eafb into main Nov 5, 2024
82 of 92 checks passed

rahxephon89 deleted the teng/fix-15044 branch November 5, 2024 01:28

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Prover] Fix bug in loop unrolling #15136

[Prover] Fix bug in loop unrolling #15136

rahxephon89 commented Oct 31, 2024

trunk-io bot commented Oct 31, 2024 •

edited

Loading

rahxephon89 Oct 31, 2024

brmataptos Nov 1, 2024

rahxephon89 Nov 4, 2024

rahxephon89 Oct 31, 2024

rahxephon89 commented Oct 31, 2024

rahxephon89 Oct 31, 2024

rahxephon89 Oct 31, 2024

brmataptos left a comment

brmataptos Nov 1, 2024

brmataptos Nov 1, 2024

fEst1ck left a comment

rahxephon89 Nov 4, 2024

wrwg Nov 4, 2024

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

github-actions bot commented Nov 5, 2024

github-actions bot commented Nov 5, 2024

github-actions bot commented Nov 5, 2024

[Prover] Fix bug in loop unrolling #15136

[Prover] Fix bug in loop unrolling #15136

Conversation

rahxephon89 commented Oct 31, 2024

Description

How Has This Been Tested?

Key Areas to Review

Type of Change

Which Components or Systems Does This Change Impact?

Checklist

trunk-io bot commented Oct 31, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rahxephon89 commented Oct 31, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

brmataptos left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

fEst1ck left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

github-actions bot commented Nov 5, 2024

✅ Forge suite realistic_env_max_load success on b7acb475991b4161323e13eb191e13a0f82d8a39

github-actions bot commented Nov 5, 2024

✅ Forge suite framework_upgrade success on 1086a5e00d773704731ab84fb4ed3538613b2250 ==> b7acb475991b4161323e13eb191e13a0f82d8a39

github-actions bot commented Nov 5, 2024

✅ Forge suite compat success on 1086a5e00d773704731ab84fb4ed3538613b2250 ==> b7acb475991b4161323e13eb191e13a0f82d8a39

trunk-io bot commented Oct 31, 2024 •

edited

Loading

✅ Forge suite `realistic_env_max_load` success on `b7acb475991b4161323e13eb191e13a0f82d8a39`

✅ Forge suite `framework_upgrade` success on `1086a5e00d773704731ab84fb4ed3538613b2250` ==> `b7acb475991b4161323e13eb191e13a0f82d8a39`

✅ Forge suite `compat` success on `1086a5e00d773704731ab84fb4ed3538613b2250` ==> `b7acb475991b4161323e13eb191e13a0f82d8a39`