Lab 2025 again

.github/workflows/ci.yml

@@ -14,7 +14,7 @@ on:
 
 env:
   NODE_VERSION: 18
-  LOCAL_DOCKER_IMG: gillian-src:local
+  LOCAL_DOCKER_IMG: gillian-build:local
   DOCKER_IMG_PRE: ghcr.io/gillianplatform/
 
 jobs:
@@ -59,15 +59,11 @@ jobs:
         run: |
           mkdir _dist
           opam exec -- dune install --relocatable --prefix ./_dist
-          cd _dist
-          zip -r ../gillian-${{ runner.os }}.zip ./*
-          cd ..
-          rm -rf ./_dist
       - name: Sending artifact
         uses: actions/upload-artifact@v4
         with:
-          name: gillian-${{ runner.os }}.zip
-          path: gillian-${{ runner.os }}.zip
+          name: gillian-${{ runner.os }}
+          path: _dist
       - name: Building API docs
         run: make docs
         if: runner.os == 'Linux'
@@ -93,12 +89,13 @@ jobs:
         name: Download artifact
         uses: actions/download-artifact@v4
         with:
-          name: gillian-${{ runner.os }}.zip
+          name: gillian-${{ runner.os }}
+          path: _dist
       - &INSTALL_ARTIFACT
-        name: Extract and install Gillian
+        name: Install Gillian
         run: |
-          sudo unzip gillian-${{ runner.os }}.zip -d /usr/local > /dev/null
-          rm gillian-${{ runner.os }}.zip
+          sudo rsync -a --chmod=a+rx _dist/ /usr/local
+          rm -rf _dist
       - uses: actions/checkout@v4
       - name: init env
         run: "Gillian-C/scripts/setup_environment.sh"
@@ -235,15 +232,15 @@ jobs:
           file: docker/Dockerfile.build
           context: .
           tags: ${{ env.LOCAL_DOCKER_IMG }}
-          outputs: type=docker, dest=${{ runner.temp }}/docker.tar
+          outputs: type=docker, dest=${{ runner.temp }}/gillian-build-docker.tar
       - name: Upload docker image
         uses: actions/upload-artifact@v4
         with:
-          name: gillian-src-docker
-          path: ${{ runner.temp }}/docker.tar
+          name: gillian-build-docker
+          path: ${{ runner.temp }}/gillian-build-docker.tar
       - name: Load image
         run: |
-          docker load --input ${{ runner.temp }}/docker.tar
+          docker load --input ${{ runner.temp }}/gillian-build-docker.tar
           docker image ls -a
       - name: Dune test
         run: docker run --rm ${{ env.LOCAL_DOCKER_IMG }} opam exec -- dune test
@@ -255,10 +252,9 @@ jobs:
           docker cp deps:/home/opam/.opam/5.3 ./.docker_opam_cache
           docker rm deps
 
-  docker-push:
+  docker-dist:
     runs-on: ubuntu-latest
     needs: docker-build
-    if: ${{ contains(fromJSON('["push", "workflow_dispatch", "release"]'), github.event_name) }}
     strategy:
       matrix:
         include:
@@ -274,16 +270,24 @@ jobs:
     env:
       DOCKER_TAG_RAW: ${{ github.event.inputs.docker-tag || (github.ref_name == 'master' && 'nightly' || github.ref_name) }}
     steps:
+      - name: Free up disk space
+        run: |
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL
+          sudo docker image prune --all --force
+          sudo docker builder prune -a
+      - name: Checkout
+        uses: actions/checkout@v4
       - name: Download base image
         uses: actions/download-artifact@v4
         with:
-          name: gillian-src-docker
+          name: gillian-build-docker
           path: ${{ runner.temp }}
       - name: Load image
         run: |
-          docker load --input ${{ runner.temp }}/docker.tar
+          docker load --input ${{ runner.temp }}/gillian-build-docker.tar
           docker image ls -a
       - name: Login to GitHub Container Registry
+        if: ${{ contains(fromJSON('["push", "workflow_dispatch", "release"]'), github.event_name) }}
         uses: docker/login-action@v3
         with:
           registry: ghcr.io
@@ -295,11 +299,18 @@ jobs:
         uses: docker/build-push-action@v6
         with:
           file: docker/Dockerfile.dist
-          tags: ${{ env.DOCKER_IMG_PRE }}${{ env.image }}:${{ env.DOCKER_TAG }}
+          tags: ${{ env.DOCKER_IMG_PRE }}${{ matrix.image }}:${{ env.DOCKER_TAG }}
           build-args: |
-            packages=${{ env.packages }}
-            no_cbmc=${{ env.no_cbmc }}
-          push: true
+            packages=${{ matrix.packages }}
+            no_cbmc=${{ matrix.no_cbmc }}
+          push: ${{ contains(fromJSON('["push", "workflow_dispatch", "release"]'), github.event_name) }}
+      - name: Export docker image
+        run: docker save ${{ env.DOCKER_IMG_PRE }}${{ matrix.image }}:${{ env.DOCKER_TAG }} > ${{ runner.temp }}/${{ matrix.image }}-docker.tar
+      - name: Upload docker image
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.image }}-docker
+          path: ${{ runner.temp }}/${{ matrix.image }}-docker.tar
 
   deploy-docs:
     if: github.ref_name == github.event.repository.default_branch

GillianCore/debugging/log/debugger_log.ml

@@ -1,4 +1,5 @@
 module L = Logging
+module Gillian_result = Utils.Gillian_result
 
 let file_name = "./gillian-debugger.log"
 let rpc_ref : Debug_rpc.t option ref = ref None
@@ -103,6 +104,7 @@ let setup rpc =
 
 let dump_dbg : (unit -> Yojson.Safe.t) option ref = ref None
 let set_debug_state_dumper f = dump_dbg := Some f
+let reraise exc = Printexc.(raise_with_backtrace exc (get_raw_backtrace ()))
 
 let try' ~name f x =
   let err_json backtrace =
@@ -129,23 +131,35 @@ let try' ~name f x =
       let err_json = err_json backtrace in
       let json = err_json @ json in
       log_async (fun m -> m ~json "[Error] %s" e);%lwt
-      raise (Failure e)
+      reraise (Failure e)
   | (Failure e | Invalid_argument e) as err ->
       let backtrace = Printexc.get_backtrace () in
       let err_json = err_json backtrace in
       log_async (fun m -> m ~json:err_json "[Error] %s" e);%lwt
-      raise err
+      reraise err
   | Not_found ->
       let backtrace = Printexc.get_backtrace () in
       let err_json = err_json backtrace in
       log_async (fun m -> m ~json:err_json "[Error] Not found");%lwt
-      raise Not_found
+      reraise Not_found
   | Effect.Unhandled _ as e ->
+      let backtrace = Printexc.get_backtrace () in
+      let err_json = err_json backtrace in
+      let s = Printexc.to_string e in
+      log_async (fun m -> m ~json:err_json "[Error] Unhandled effect\n%s" s);%lwt
+      reraise e
+  | Gillian_result.Exc.Gillian_error g as e ->
+      let backtrace = Printexc.get_backtrace () in
+      let err_json = err_json backtrace in
+      log_async (fun m ->
+          m ~json:err_json "[Error] %a" Gillian_result.Error.pp g);%lwt
+      reraise e
+  | e ->
       let backtrace = Printexc.get_backtrace () in
       let err_json = err_json backtrace in
       let s = Printexc.to_string e in
       log_async (fun m -> m ~json:err_json "[Error] Unhandled exception\n%s" s);%lwt
-      raise e
+      reraise e
 
 let set_rpc_command_handler rpc ?name ?(catchall = true) module_ f =
   let f x = if catchall then try' ~name f x else f x in

GillianCore/engine/Abstraction/PState.ml

@@ -267,18 +267,23 @@ module Make (State : SState.S) :
       (x : string option)
       (args : vt list)
       (astate : t) : (t * Flag.t, SMatcher.err_t) Res_list.t =
+    let open Res_list.Syntax in
+    let open Syntaxes.List in
     L.verbose (fun m ->
         m "INSIDE RUN spec of %s (%d more) with the following MP:@\n%a@\n" name
           (List.length more_specs) MP.pp mp);
     let old_store = get_store astate in
-    let new_store =
-      try SStore.init (List.combine params args)
+    let** new_store =
+      try SStore.init (List.combine params args) |> Res_list.return
       with Invalid_argument _ ->
-        Fmt.failwith
-          "Running spec of %s which takes %i parameters with the following %i \
-           arguments : %a"
-          name (List.length params) (List.length args) (Fmt.Dump.list Expr.pp)
-          args
+        let msg =
+          Fmt.str
+            "Running spec of %s which takes %i parameters with the following \
+             %i arguments : %a"
+            name (List.length params) (List.length args) (Fmt.Dump.list Expr.pp)
+            args
+        in
+        Res_list.error_with (StateErr.EOther msg)
     in
 
     let astate' = set_store astate new_store in
@@ -295,8 +300,6 @@ module Make (State : SState.S) :
         m "About to use the spec of %s with the following MP:@\n%a@\n" name
           MP.pp mp);
 
-    let open Res_list.Syntax in
-    let open Syntaxes.List in
     let res = SMatcher.match_ astate' subst mp (FunctionCall name) in
     if List.exists Result.is_error res then
       L.normal (fun m ->

docker/Dockerfile.dist

@@ -1,6 +1,6 @@
 # syntax=docker/dockerfile:1
 
-FROM gillian-src:local AS dist
+FROM gillian-build:local AS dist
 ARG packages=
 RUN opam exec -- dune install $packages --relocatable --prefix ./_dist
 RUN sudo mv _dist /
@@ -9,16 +9,18 @@ FROM ubuntu:noble AS install
 ADD https://github.com/diffblue/cbmc/releases/download/cbmc-5.14.3/cbmc-5.14.3-Linux.deb cbmc.deb
 ARG no_cbmc=
 RUN apt update \
-    && apt install -y z3 libsqlite3-0 $([ $no_cbmc ] || echo './cbmc.deb') \
+    && apt install -y rsync z3 libsqlite3-0 $([ $no_cbmc ] || echo './cbmc.deb') \
     && apt clean \
     && rm -rf /var/lib/apt/lists* \
     && rm cbmc.deb
-COPY --from=dist /_dist/bin/* /usr/bin/
-COPY --from=dist /_dist/lib/* /usr/lib/
-COPY --from=dist /_dist/share/* /usr/share/
+COPY --from=dist /_dist /_dist
+RUN rsync -a --chmod=a+rx /_dist/ /usr/local \
+    && rm -rf /_dist \
+    && apt remove -y rsync \
+    && apt clean -y
 
 FROM scratch
-LABEL maintainer "Nat Karmios"
+LABEL maintainer="Nat Karmios"
 COPY --from=install / /
 CMD [ "bash" ]
 

githooks/pre-commit

@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 
-set -euo pipefail
+set -eo pipefail
 code=0
 dune_checks=1
 

wisl/lib/state_ex/wislLifter.ml

@@ -1266,6 +1266,9 @@ struct
       | Lit l -> Fmt.pf ft "%a" pp_lit l
       | UnOp (LstLen, e) -> Fmt.pf ft "len(%a)" pp_o e
       | BinOp (e1, LstNth, e2) -> Fmt.pf ft "%a[%a]" pp e1 pp_o e2
+      | BinOp (Lit (Int x), IPlus, e2) ->
+          if Z.sign x = -1 then Fmt.pf ft "%a - %a" pp e2 Z.pp_print (Z.neg x)
+          else Fmt.pf ft "%a + %a" pp e2 Z.pp_print x
       | BinOp (e1, op, e2) when outermost ->
           Fmt.pf ft "%a %a %a" pp e1 pp_binop op pp e2
       | BinOp (e1, op, e2) -> Fmt.pf ft "(%a %a %a)" pp e1 pp_binop op pp e2