Skip to content

Write tests for kmir run with basic computations and control flow #166

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

Closed
yanliu18 opened this issue Jun 29, 2023 · 0 comments · Fixed by #257
Closed

Write tests for kmir run with basic computations and control flow #166

yanliu18 opened this issue Jun 29, 2023 · 0 comments · Fixed by #257
Labels
kmir-tests Adding/updating tests in KMIR mir-semantics MIR semantics in K

Comments

@yanliu18
Copy link
Contributor

yanliu18 commented Jun 29, 2023

The purpose is to implement milestone 3, enable kmir on executing basic computations.
The tests should be written in Rust suface syntax (refer to the pattern described by @geo2a) and compile to MIR using rustc (nightly version) options such as

rustc prog.rs --emit=mir -Zmir-enable-passes=-ConstDebugInfo,-PromoteTemps -C debug-assertions=off

Using the two flags to avoid syntax we do not support right now and to turn off the debug mode (options to resemble the production code, refer to Discussion in #65 for more details.)

In particular, we should be able to test

  1. the operations defined in Rvalue, NullaryOp, UnaryOp, BinaryOp with CheckedBinaryOp as optional (This would require refining the implementation of AssertKind).
  2. the basic control flow structures sequential, conditions, switch with optional support for loops. Though there is no explicit support for the common control flow structures in MIR, it has Switch and -> commands to support the control flow. We might want to the surface syntax to test the coverage.
@yanliu18 yanliu18 added mir-semantics MIR semantics in K kmir-tests Adding/updating tests in KMIR labels Jun 29, 2023
@yanliu18 yanliu18 added this to the Milestone 3 - KMIR Semantics milestone Jun 29, 2023
@dkcumming dkcumming self-assigned this Jul 10, 2023
@yanliu18 yanliu18 linked a pull request Nov 28, 2023 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kmir-tests Adding/updating tests in KMIR mir-semantics MIR semantics in K
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants