Remove zlib dependency (#799)

Remove support for directly reading gzip compressed ELF files. This means we can remove the dependency on zlib which simplifies compilation. (Note this dependency affects the *users* of Sail, not the Sail compiler itself.)

.github/workflows/build.yml

@@ -28,7 +28,7 @@ jobs:
     - name: System dependencies (macOS)
       if: startsWith(matrix.os, 'macOS')
       run: |
-        brew install --force --overwrite gpatch gmp z3 pkg-config lzlib zlib opam
+        brew install --force --overwrite gpatch gmp z3 pkg-config opam
 
     - name: Restore cached opam
       id: cache-opam-restore

.github/workflows/release.yml

@@ -34,7 +34,6 @@ jobs:
         dnf install --assumeyes \
           gmp-devel \
           pkg-config \
-          zlib-devel \
           openssl \
           curl \
           git \

Dockerfile.nightly

@@ -1,7 +1,7 @@
 FROM ubuntu
 
 # Install apt deps
-RUN apt-get update && apt-get install -y --no-install-recommends ca-certificates build-essential libgmp-dev z3 libz3-dev opam rsync pkg-config m4 zlib1g-dev
+RUN apt-get update && apt-get install -y --no-install-recommends ca-certificates build-essential libgmp-dev z3 libz3-dev opam rsync pkg-config m4
 
 # Configure opam
 RUN opam init -y --no-setup --compiler=5.2.0 --shell=sh --disable-sandboxing

Dockerfile.release

@@ -8,7 +8,6 @@ RUN apt-get update && \
     libgmp-dev \
     z3 \
     pkg-config \
-    zlib1g-dev \
     sudo && \
     apt-get clean && \
     rm -rf /var/lib/apt/lists/*

INSTALL.md

@@ -19,7 +19,7 @@ eval $(opam config env)
 ```
 Install system dependencies, on Ubuntu (if using WSL see the note below):
 ```
-sudo apt-get install build-essential libgmp-dev z3 pkg-config zlib1g-dev
+sudo apt-get install build-essential libgmp-dev z3 pkg-config
 ```
 or [MacOS homebrew](https://brew.sh/):
 ```

doc/Dockerfile

@@ -1,6 +1,6 @@
 FROM debian
 
-RUN apt-get update && apt-get install -y --no-install-recommends build-essential git ruby ruby-rubygems opam z3 rsync libgmp-dev pkg-config zlib1g-dev texlive-latex-base texlive-pictures poppler-utils
+RUN apt-get update && apt-get install -y --no-install-recommends build-essential git ruby ruby-rubygems opam z3 rsync libgmp-dev pkg-config texlive-latex-base texlive-pictures poppler-utils
 
 RUN gem install asciidoctor asciidoctor-pdf asciidoctor-bibtex asciidoctor-sail rouge
 

doc/asciidoc/usage.adoc

@@ -68,10 +68,10 @@ this needs to be compiled and linked with the C files in the
 `$SAIL_DIR/lib` directory:
 [source,sh]
 ----
-gcc out.c $SAIL_DIR/lib/*.c -lgmp -lz -I $SAIL_DIR/lib/ -o out
+gcc out.c $SAIL_DIR/lib/*.c -lgmp -I $SAIL_DIR/lib/ -o out
 ----
 The C output requires the https://gmplib.org/[GMP library] for arbitrary precision
-arithmetic, as well as https://zlib.net/[zlib] for working with compressed ELF binaries.
+arithmetic.
 
 There are several Sail options that affect the C output:
 

doc/manual.html

@@ -3112,12 +3112,12 @@ <h3 id="_c_compilation">C compilation</h3>
 </div>
 <div class="listingblock">
 <div class="content">
-<pre class="rouge highlight"><code data-lang="sh">gcc out.c <span class="nv">$SAIL_DIR</span>/lib/<span class="k">*</span>.c <span class="nt">-lgmp</span> <span class="nt">-lz</span> <span class="nt">-I</span> <span class="nv">$SAIL_DIR</span>/lib/ <span class="nt">-o</span> out</code></pre>
+<pre class="rouge highlight"><code data-lang="sh">gcc out.c <span class="nv">$SAIL_DIR</span>/lib/<span class="k">*</span>.c <span class="nt">-lgmp</span> <span class="nt">-I</span> <span class="nv">$SAIL_DIR</span>/lib/ <span class="nt">-o</span> out</code></pre>
 </div>
 </div>
 <div class="paragraph">
 <p>The C output requires the <a href="https://gmplib.org/">GMP library</a> for arbitrary precision
-arithmetic, as well as <a href="https://zlib.net/">zlib</a> for working with compressed ELF binaries.</p>
+arithmetic.</p>
 </div>
 <div class="paragraph">
 <p>There are several Sail options that affect the C output:</p>
@@ -4958,7 +4958,7 @@ <h4 id="_automatic_wildcard_insertion">Automatic wildcard insertion</h4>
 <pre class="rouge highlight"><code>Warning: Required literal ../examples/cannot_wildcard.sail:17.14-17:
 17 |        (Some(0b1), _)         =&gt; print_endline("3"),
    |              ^-^
-   | 
+   |
 Sail cannot simplify the above pattern match:
 This bitvector pattern literal must be kept, as it is required for Sail to show that the surrounding pattern match is complete.
 When translated into prover targets (e.g. Lem, Coq) without native bitvector patterns, they may be unable to verify that the match covers all possible cases.</code></pre>
@@ -5957,7 +5957,7 @@ <h3 id="_modules">Modules</h3>
 6 |    let x = alfa();
   |            ^--^
   | Not in scope
-  | 
+  |
   | Try requiring module A to bring the following into scope for module B:
   | ../examples/amod.sail:6.4-8:
   | 6 |val alfa : unit -&gt; int
@@ -6681,4 +6681,4 @@ <h2 id="_references">References</h2>
 </div>
 </div>
 </body>
-</html>
+</html>

doc/old/usage.tex

@@ -123,10 +123,10 @@ \subsection{C compilation}
 this needs to be compiled and linked with the C files in the
 \verb+sail/lib+ directory:
 \begin{verbatim}
-gcc out.c $SAIL_DIR/lib/*.c -lgmp -lz -I $SAIL_DIR/lib/ -o out
+gcc out.c $SAIL_DIR/lib/*.c -lgmp -I $SAIL_DIR/lib/ -o out
 \end{verbatim}
 The C output requires the GMP library for arbitrary precision
-arithmetic, as well as zlib for working with compressed ELF binaries.
+arithmetic.
 
 There are several Sail options that affect the C output:
 \begin{itemize}

dune-project

@@ -57,7 +57,6 @@ http://www.cl.cam.ac.uk/~pes20/sail/.
     (lem (>= "2018-12-14"))
     (linksem (>= "0.3"))
     conf-gmp
-    conf-zlib
     (yojson (>= 1.6.0))
     (pprint (>= 20220103))))
 

lib/elf.c

@@ -53,9 +53,6 @@
 #include "rts.h"
 #include "sail.h"
 
-// Use the zlib library to uncompress ELF.gz files
-#include <zlib.h>
-
 #ifdef __cplusplus
 extern "C" {
 #endif
@@ -434,17 +431,18 @@ void load_elf(char *filename, bool *is32bit_p, uint64_t *entry) {
     int   size   = 0;
     int   chunk  = (1<<24); // increments output buffer this much
     int   read   = 0;
-    gzFile in = gzopen(filename, "rb");
+    FILE* in = fopen(filename, "rb");
     if (in == NULL) { goto fail; }
-    while (!gzeof(in)) {
+    while (!feof(in)) {
         size = read + chunk;
         buffer = (char*)realloc(buffer, size);
         if (buffer == NULL) { goto fail; }
 
-        int s = gzread(in, buffer+read, size - read);
+        int s = fread(buffer+read, 1, size - read, in);
         if (s < 0) { goto fail; }
         read += s;
     }
+    fclose(in);
     loadELFHdr(buffer, read, is32bit_p, entry);
     free(buffer);
     return;
@@ -587,17 +585,18 @@ int lookup_sym(const char *filename, const char *symname, uint64_t *value) {
     int   chunk  = (1<<24); // increments output buffer this much
     int   read   = 0;
     int   ret    = 0;
-    gzFile in = gzopen(filename, "rb");
+    FILE* in = fopen(filename, "rb");
     if (in == NULL) { goto fail; }
-    while (!gzeof(in)) {
+    while (!feof(in)) {
         size = read + chunk;
         buffer = (char*)realloc(buffer, size);
         if (buffer == NULL) { goto fail; }
 
-        int s = gzread(in, buffer+read, size - read);
+        int s = fread(buffer+read, 1, size - read, in);
         if (s < 0) { goto fail; }
         read += s;
     }
+    fclose(in);
     ret = lookupSymbol(buffer, read, symname, value);
     free(buffer);
     return ret;

libsail.opam

@@ -38,7 +38,6 @@ depends: [
   "lem" {>= "2018-12-14"}
   "linksem" {>= "0.3"}
   "conf-gmp"
-  "conf-zlib"
   "yojson" {>= "1.6.0"}
   "pprint" {>= "20220103"}
   "odoc" {with-doc}

test/builtins/run_tests.py

@@ -29,7 +29,7 @@ def test_c_builtins(name, sail_opts):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('{} -no_warn -c {} {} 1> {}.c'.format(sail, sail_opts, filename, basename))
-                step('gcc {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(basename, sail_dir, sail_dir, basename))
+                step('gcc {}.c {}/lib/*.c -lgmp -I {}/lib -o {}'.format(basename, sail_dir, sail_dir, basename))
                 step('./{}'.format(basename))
                 step('rm {}.c'.format(basename))
                 step('rm {}'.format(basename))
@@ -171,4 +171,3 @@ def test_isla_builtins(name):
 output = open('tests.xml', 'w')
 output.write(xml)
 output.close()
-

test/c/run_tests.py

@@ -42,7 +42,7 @@ def test_c(name, c_opts, sail_opts, valgrind, compiler='cc'):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('{} -no_warn -c {} {} 1> {}.c'.format(sail, sail_opts, filename, basename))
-                step('{} {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}.bin'.format(compiler, c_opts, basename, sail_dir, sail_dir, basename))
+                step('{} {} {}.c {}/lib/*.c -lgmp -I {}/lib -o {}.bin'.format(compiler, c_opts, basename, sail_dir, sail_dir, basename))
                 step('./{}.bin > {}.result 2> {}.err_result'.format(basename, basename, basename), expected_status = 1 if basename.startswith('fail') else 0)
                 step('diff {}.result {}.expect'.format(basename, basename))
                 if os.path.exists('{}.err_expect'.format(basename)):
@@ -65,7 +65,7 @@ def test_c2(name, c_opts, sail_opts, valgrind):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('{} -no_warn -c2 {} {} -o {}'.format(sail, sail_opts, filename, basename))
-                step('gcc {} {}.c {}_emu.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}'.format(c_opts, basename, basename, sail_dir, sail_dir, basename))
+                step('gcc {} {}.c {}_emu.c {}/lib/*.c -lgmp -I {}/lib -o {}'.format(c_opts, basename, basename, sail_dir, sail_dir, basename))
                 step('./{} > {}.result 2>&1'.format(basename, basename), expected_status = 1 if basename.startswith('fail') else 0)
                 step('diff {}.result {}.expect'.format(basename, basename))
                 if valgrind:

test/float/run_tests.py

@@ -31,7 +31,7 @@ def test_float(name, sail_opts, compiler, c_opts):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('{} -no_warn -c {} {} 1> {}.c'.format(sail, sail_opts, filename, basename))
-                step('{} {} {}.c {}/lib/*.c -lgmp -lz -I {}/lib -o {}.bin'.format(compiler, c_opts, basename, sail_dir, sail_dir, basename))
+                step('{} {} {}.c {}/lib/*.c -lgmp -I {}/lib -o {}.bin'.format(compiler, c_opts, basename, sail_dir, sail_dir, basename))
                 step('./{}.bin > {}.result 2> {}.err_result'.format(basename, basename, basename), expected_status = 1 if basename.startswith('fail') else 0)
 
                 step('diff {}.err_result no_error && rm {}.err_result'.format(basename, basename))

test/sailcov/run_tests.py

@@ -39,7 +39,7 @@ def test_sailcov():
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('{} -no_warn -no_memo_z3 -c -c_include sail_coverage.h -c_coverage {}.branches {} -o {}'.format(sail, basename, filename, basename))
-                step('cc {}.c {}/lib/*.c {}/lib/coverage/libsail_coverage.a -lgmp -lz -lpthread -ldl -I {}/lib -o {}.bin'.format(basename, sail_dir, sail_dir, sail_dir, basename))
+                step('cc {}.c {}/lib/*.c {}/lib/coverage/libsail_coverage.a -lgmp -lpthread -ldl -I {}/lib -o {}.bin'.format(basename, sail_dir, sail_dir, sail_dir, basename))
                 step('./{}.bin -c {}.taken'.format(basename, basename))
                 step('{} --werror --all {}.branches --taken {}.taken {}'.format(sailcov, basename, basename, filename))
                 step('diff {}.html {}.expect'.format(basename, basename))