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.

Sign up for GitHub

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

Jump to bottom

Concrete playback fails when temp folder is on a different mount point #2705

Closed
yvizel opened this issue Aug 23, 2023 · 4 comments · Fixed by #2804
Closed

Concrete playback fails when temp folder is on a different mount point #2705

yvizel opened this issue Aug 23, 2023 · 4 comments · Fixed by #2804
Assignees
@tautschnig @jaisnan
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@yvizel
Copy link

yvizel commented Aug 23, 2023

Hi,

I built Kani on Ubuntu 22.04 and I am getting the following output when running the regression.

regression_output.txt

What can it be?
@yvizel yvizel added the [C] Bug This is a bug. Something isn't working. label Aug 23, 2023
@tautschnig
Copy link
Member

Would you mind doing export RUST_BACKTRACE=1 and re-run those tests? All errors are of the form

thread '<unnamed>' panicked at kani-driver/src/util.rs:64:18:
called `Result::unwrap()` on an `Err` value: Error renaming file /tmp/kani_tmp_2761667929_concrete_playback.tmp

Caused by:
    Invalid cross-device link (os error 18)

but it would be helpful to know where we are invoking rename from.

@yvizel
Copy link
Author

yvizel commented Aug 23, 2023

Attached is the new log.
regression.txt

@celinval
Copy link
Contributor

celinval commented Aug 23, 2023 •
edited
Loading

This could be a bug in Kani. Is your /tmp folder mounted in a different partition as your home folder?

We currently invoke std::fs::rename() to override the new file, but the documentation of this function clearly states that "This will not work if the new name is on a different mount point."

@yvizel
Copy link
Author

yvizel commented Sep 5, 2023

@celinval - yes. The home folder is nfs while tmp is local to the machine.

@celinval celinval changed the title Regression failure on Ubuntu 22.04 Concrete playback fails when temp folder is on a different mount point Sep 5, 2023
@tautschnig tautschnig self-assigned this Oct 3, 2023
tautschnig added a commit to tautschnig/kani that referenced this issue Oct 4, 2023
@tautschnig
Create concrete playback temp files in source directory
4cccf8a 
Concrete playback seeks to generate unit tests in the original source
file. An intermediate temporary file is used to reduce the risk of
corrupting original source files. Once the temporary file has been
completely written to, it is to be atomically moved to replace the
source file. This can only be done on the same file system.

We now create the temporary file in the same source directory as the
original source file to ensure we are on the same file system. The
implementation uses NamedTempFile from the tempfile crate, which renders
our own tempfile implementation redundant.

Tested on Ubuntu 20.04 with /tmp on a different partition (where our
regression tests would previously fail).

Resolves: model-checking#2705
@tautschnig tautschnig mentioned this issue Oct 4, 2023
Merged
tautschnig added a commit that referenced this issue Oct 4, 2023
@tautschnig
Create concrete playback temp files in source directory (#2804)
fb08f3e 
Concrete playback seeks to generate unit tests in the original source
file. An intermediate temporary file is used to reduce the risk of
corrupting original source files. Once the temporary file has been
completely written to, it is to be atomically moved to replace the
source file. This can only be done on the same file system.

We now create the temporary file in the same source directory as the
original source file to ensure we are on the same file system. The
implementation uses NamedTempFile from the tempfile crate, which renders
our own tempfile implementation redundant.

Tested on Ubuntu 20.04 with /tmp on a different partition (where our
regression tests would previously fail).

Resolves: #2705
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@tautschnig tautschnig

@jaisnan jaisnan

Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Create concrete playback temp files in source directory tautschnig/kani
4 participants
@tautschnig @yvizel @celinval @jaisnan