Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[compiler-v2] Perform check of uninitialized locals in code spec blocks #15943

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

rahxephon89
Copy link
Contributor

@rahxephon89 rahxephon89 commented Feb 13, 2025

Description

This PR adds checking of uninitialized locals in the spec block.

close #15928

How Has This Been Tested?

  1. existing tests;
  2. a new test case.

Key Areas to Review

Whether the fix covers all cases for spec blocks.

Type of Change

  • New feature
  • Bug fix
  • Breaking change
  • Performance improvement
  • Refactoring
  • Dependency update
  • Documentation update
  • Tests

Which Components or Systems Does This Change Impact?

  • Validator Node
  • Full Node (API, Indexer, etc.)
  • Move/Aptos Virtual Machine
  • Aptos Framework
  • Aptos CLI/SDK
  • Developer Infrastructure
  • Move Compiler
  • Other (specify)

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

Copy link

trunk-io bot commented Feb 13, 2025

⏱️ 10m total CI duration on this PR
Job Cumulative Duration Recent Runs
check-dynamic-deps 4m 🟩🟩
rust-cargo-deny 4m 🟩🟩
general-lints 55s 🟩🟩
semgrep/ci 44s 🟩🟩
file_change_determinator 22s 🟩🟩
permission-check 6s 🟩🟩
permission-check 4s 🟩🟩

settingsfeedbackdocs ⋅ learn more about trunk.io

@rahxephon89 rahxephon89 changed the title [compiler-v2] Perform unintialization of locals in the spec block [compiler-v2] Perform check of uninitialized locals in the spec block Feb 13, 2025
@rahxephon89 rahxephon89 changed the title [compiler-v2] Perform check of uninitialized locals in the spec block [compiler-v2] Perform check of uninitialized locals in code spec blocks Feb 13, 2025
@rahxephon89 rahxephon89 marked this pull request as ready for review February 13, 2025 06:16
@rahxephon89 rahxephon89 requested review from vineethk and wrwg February 13, 2025 06:16
});
};
if let Bytecode::SpecBlock(_, spec) = bc {
for cond in &spec.conditions {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is conditions the only field of spec that needs to be checked? How about update_map?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, update_map is not yet filled in this phase AFAIK. The test case with update z = y; is used to show it.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we can just say that in a comment here, so that it is explicit to the reader.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

[Bug][compiler-v2][prover] Compiler panic when translating an assertion with an uninitialized variable
2 participants