Executable mode bits in release files not set

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

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.

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

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.

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.)

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