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

Generate unit test line by line (for --inplace) #2213

Merged
merged 22 commits into from
Mar 2, 2023

Conversation

jaisnan
Copy link
Contributor

@jaisnan jaisnan commented Feb 16, 2023

Description of changes:

This PR adds -

  1. Generating the unit tests (concrete playback tests) line by line using a sync buffered reader/writer.
  2. Util functions and related unit tests.
  3. Minor refactoring

The reason to generate the unit tests line by line is -

  1. to avoid storing the entire unit test, no matter how large in a string variable before dumping it.
  2. To make sure users still have access to the generated unit tests in case generation fails midway.

Resolved issues:

Closes the changes proposed by #1625

Call-outs:

  1. Uses the tempfile crate to take care of the file handling. The documentation says that the tempfile is deleted automatically whenever it goes out of scope.
  2. Changes the definition of the UnitTest struct.
  3. There are no regression tests for the changes made.

Testing:

  • How is this change tested? unit tests but not

  • Is this a refactor change? yes

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@jaisnan jaisnan requested a review from a team as a code owner February 16, 2023 02:36
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Thanks

kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
@jaisnan jaisnan requested a review from celinval February 21, 2023 18:36
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

It's looking good. I was wondering if we should modify the TempFile slightly. So, we don't want to delete the file if it doesn't exist anymore. We should also consider bringing the BufWriter to be inside this structure since we want to explicitly call flush() before dropping it and before removing the file.

kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Awesome, thanks again. Not for this PR, but we should eventually change this code to write all the unit tests in the file at once.

kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
kani-driver/src/concrete_playback.rs Outdated Show resolved Hide resolved
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Thanks @jaisnan. Just tiny comments

kani-driver/src/util.rs Show resolved Hide resolved
kani-driver/src/util.rs Show resolved Hide resolved
kani-driver/src/util.rs Show resolved Hide resolved
@jaisnan jaisnan merged commit 4b504b2 into model-checking:main Mar 2, 2023
@jaisnan jaisnan assigned jaisnan and unassigned karkhaz Mar 6, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
No open projects
Status: Done
Development

Successfully merging this pull request may close these issues.

3 participants