Executable mode bits in release files not set

[ifndefJOSH]

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

• prusti-rustc
• prusti-server
• prusti-server-driver
• cargo-prusti
• viper_tools/z3/bin
• viper_tools/boogie/Binaries/Boogie

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

• I'm not sure why this would be happening because it looks like your deploy file isn't stripping the mode bits (only zip option is recursive -r)
• I don't know if the same thing is happening with your MacOS or Windows deployments

[fpoli]

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]

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]

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

prusti-dev/.github/workflows/deploy.yml

Line 117 in f94b7fa

zip -r prusti.zip *

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

prusti-dev/.github/workflows/deploy.yml

Lines 107 to 108 in f94b7fa

	- name: Download all Prusti artifacts
	uses: actions/download-artifact@v2

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

[fpoli]

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

prusti-dev/.github/workflows/deploy.yml

Lines 107 to 108 in f94b7fa

	- name: Download all Prusti artifacts
	uses: actions/download-artifact@v2

Indeed, that seems to be the reason: actions/download-artifact#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.)