search

viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.52k stars 102 forks source link

Executable mode bits in release files not set #1497

Closed ifndefJOSH closed 4 months ago

ifndefJOSH commented 4 months ago

None of the executable files in the zip downloaded at releases have the executable mode bit set. This includes:

If a user manually marks prusti-rustc and cargo-prusti as executable via chmod, and then attempts to verify a simple program, they get an error.

Conversely, if prusti-rustc, prusti-server, prusti-server-driver, and cargo-prusti are marked as executable (but z3 and Boogie are not), they receive the following compiler panic. err_report.txt

Temporary Workaround: Obviously after running the following shell script in the Prusti directory, I was able to get Prusti to work.

chmod +x ./prusti-rustc
chmod +x ./prusti-server
chmod +x ./prusti-server-driver
chmod +x ./cargo-prusti
chmod +x ./viper_tools/z3/bin
chmod +x ./viper_tools/boogie/Binaries/Boogie

Platform information: Debian 12 6.1.55-1 (2023-09-29) x86_64 GNU/Linux (I downloaded the Ubuntu/Linux/ELF release)

Notes

fpoli commented 4 months ago

Thanks for raising this issue. The reason is that the zip format doesn't preserve file attributes. The proper fix is to release a tar.gz for Linux and macOS.

Note for future developers: remember that the zip release for Linux/macOS is used by our prusti-assistant extension, so don't remove the zip release yet. Converting prusti-assistant to unpack tar.gz requires adding a corresponding TarGzDownloader in our vs-verification-toolbox repo.

ifndefJOSH commented 4 months ago

The reason is that the zip format doesn't preserve file attributes.

I was under the impression that file mode bits were stored in the ZIP format's external attributes. Additionally, using the standard zip (v3.0) and unzip (v6.0) utilities on my Linux machine, I was able to verify that a test shell file which I marked as executable had its executable bit preserved upon compression and subsequent extraction from a ZIP file.

-rwxr-xr-x 1  38 Feb 27 08:59 hello_world.sh
-rwxr-xr-x 1  38 Feb 27 08:59 hello_world_unzipped.sh
-rw-r--r-- 1 216 Feb 27 09:00 test.zip
fpoli commented 4 months ago

Oh, nice! Thanks for pointing that out. So maybe the fault is in the version of zip that we use in GitHub's workflows?

https://github.com/viperproject/prusti-dev/blob/f94b7fa83282351255f3c278d2e96993cbd7d199/.github/workflows/deploy.yml#L117

Or maybe the permissions are lost when passing artifacts between the jobs of a GitHub workflow:

https://github.com/viperproject/prusti-dev/blob/f94b7fa83282351255f3c278d2e96993cbd7d199/.github/workflows/deploy.yml#L107-L108

It would be great if someone can experiment with GitHub runners to figure out what's needed to preserve those flags.

fpoli commented 4 months ago

Or maybe the permissions are lost when passing artifacts between the jobs of a GitHub workflow:

https://github.com/viperproject/prusti-dev/blob/f94b7fa83282351255f3c278d2e96993cbd7d199/.github/workflows/deploy.yml#L107-L108

Indeed, that seems to be the reason: https://github.com/actions/download-artifact/issues/14. A workaround would be to zip and unzip that artifact on our own, or to add the chmod +x after that download-artifact step.

(The upload-artifact action preserves the permissions correctly, in my tests.)