Various tweaks for TACAS '25 artifact (#317)

* Tweak `make build`

* Remove debug-ui examples' launch.json

* Tweak debug-ui package.json

* Debug ext: tweak installed Gillian behaviour

* Add build stages to dockerfile

* Reorganise debug examples

* Tweak .gitignore

* Fix mutation bug in lifters

* Tweak path resolution in Gil_parsing

* Fix LAction bugs in GInterpreter

- Fix the first LAction success being indexed with 1
- Fix vanish when recovery gives `Ok []`

* Support include paths in Kanillian

* Add enums to Kanillian types

* Kanillian: handle `continue` statement

* Kanillian: handle +=, -=, etc.

* Kanillian: handle comma expression

* Kanillian: Fix enum casting

* Kanillian: Add some missing float operations

* Debug ext: Allow extra command-line args

* Optionally dump annots with GIL code

* Debug examples: Add collections-c, tweak others

* Make debug logging quieter

* Debug: parse and compile files via the lifter

* Kanillian: support float-to-int casting

* Kanillian: add internal calloc

* Kanillian: improve compilation logging

* pretty printing for all wisl commands

* Kanillian: fix assume_type for enum, improve compiler log

* Minor tweaks to Kani & WISL lifter behaviour

* Kani lifter: fix uneval'd funcs overriding nest for eval'd ones

* Kani lifter: Show errors encountered before canonical cmd

* WISL & Kani lifters: Address corner cases when erroring in nest

* Add fmt to makefile

* Fix collections-c debug example

* Tweak docker to not conflict with native deps

* Squash docker image

* Add CBMC to Docker image

* Reorganise examples

---------

Co-authored-by: Sacha Ayoun <sachaayoun@gmail.com>

.github/workflows/ci.yml

@@ -308,7 +308,7 @@ jobs:
         env:
             cache-name: cache-ocaml
         with:
-          path: _opam
+          path: .docker_opam_cache
           key: docker-${{ env.cache-name }}-ocaml-5.2.0-${{ hashFiles('**/*.opam') }}
           restore-keys: |
             docker-${{ env.cache-name }}-ocaml-5.2.0
@@ -318,14 +318,15 @@ jobs:
           context: .
           load: true
           tags: ${{ env.DOCKER_TEST_TAG }}
+          target: test
       - name: Dune test
         run: docker run --rm ${{ env.DOCKER_TEST_TAG }} opam exec -- dune test
       - name: Extract cache
         if: steps.restore-cache.outputs.cache-hit != 'true'
         run: |
-          rm -rf _opam
+          rm -rf .docker_opam_cache
           docker run --name deps ${{ env.DOCKER_TEST_TAG }} bash -c "opam clean"
-          docker cp deps:/home/opam/.opam/5.2 ./
+          docker cp deps:/home/opam/.opam/5.2 ./.docker_opam_cache
           docker rm deps
 
   deploy-docs:

.gitignore

@@ -75,6 +75,9 @@ gillian.esy.lock
 *.env
 **/.gillian
 gillian_smt_queries
+*.deps
+*.i
+*.symtab.json
 
 # Dependency graphs
 with-depgraph.esy.lock

Dockerfile

@@ -1,31 +1,37 @@
-FROM ocaml/opam:debian-ocaml-5.2
-
-LABEL maintaner "Sacha \"Giltho\" Ayoun"
+# syntax=docker.io/docker/dockerfile:1.7-labs
 
+FROM ocaml/opam:debian-ocaml-5.2 AS build
+LABEL maintainer "Nat Karmios"
 ARG DEBIAN_FRONTEND=noninteractive
-
 RUN sudo apt-get update
-
 RUN sudo apt-get install libgmp-dev pkg-config libsqlite3-dev python3 z3 -y
+WORKDIR /home/opam/app/Gillian
+COPY --exclude=./_opam --exclude=**/_build . .
+RUN [ ! -f .docker_opam_cache ] || mv .docker_opam_cache ~/.opam/5.2
+RUN opam update -y
+RUN opam install . --deps-only
+RUN opam exec -- dune build @all
+CMD [ "bash" ]
 
-RUN mkdir /home/opam/app
-
+FROM build AS test
 WORKDIR /home/opam/app
-
 RUN git clone https://github.com/GillianPlatform/javert-test262.git test262
-
 RUN git clone https://github.com/GillianPlatform/collections-c-for-gillian.git collections-c
-
 WORKDIR /home/opam/app/Gillian
+CMD [ "bash" ]
 
-COPY . .
-
-RUN [ ! -f _opam ] || mv _opam ~/.opam/5.2
-
-RUN opam update -y
-
-RUN opam install . --deps-only
-
-RUN opam exec -- dune build @all
+FROM build AS install
+RUN opam install .
+WORKDIR /home/opam/app
+ADD https://github.com/diffblue/cbmc/releases/download/cbmc-5.14.3/cbmc-5.14.3-Linux.deb cbmc.deb
+RUN sudo dpkg -i cbmc.deb
+RUN opam clean -y
+RUN sudo rm -rf cbmc.deb Gillian ~/opam-repository ~/.opam/5.2/.opam-switch/sources/*
+CMD [ "bash" ]
 
+FROM scratch AS run
+LABEL maintainer "Nat Karmios"
+COPY --from=install / /
+USER opam
+WORKDIR /home/opam/app
 CMD [ "bash" ]

Gillian-JS/lib/Debugging/JSLifter.mli

@@ -9,3 +9,5 @@ module Make
      and type tl_ast = tl_ast
      and type cmd_report = V.SAInterpreter.Logging.ConfigReport.t
      and type annot = Gil_syntax.Annot.Basic.t
+     and type init_data = unit
+     and type pc_err = err

GillianCore/GIL_Syntax/Gil_syntax.mli

@@ -1079,15 +1079,17 @@ module Proc : sig
   val pp :
     show_labels:bool ->
     pp_label:'a Fmt.t ->
+    ?pp_annot:'b Fmt.t ->
     Format.formatter ->
     ('b, 'a) t ->
     unit
 
   (** Print labelled *)
-  val pp_labeled : Format.formatter -> ('a, string) t -> unit
+  val pp_labeled :
+    Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, string) t -> unit
 
   (** Print indexed *)
-  val pp_indexed : Format.formatter -> ('a, int) t -> unit
+  val pp_indexed : Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, int) t -> unit
 
   (** Returns the indexed procedure for a labeled procedures where the labels can be of any type.
     Equality of labels is decided by structural equality *)
@@ -1245,15 +1247,17 @@ module Prog : sig
   val pp :
     show_labels:bool ->
     pp_label:'b Fmt.t ->
+    ?pp_annot:'a Fmt.t ->
     Format.formatter ->
     ('a, 'b) t ->
     unit
 
   (** Print labelled *)
-  val pp_labeled : Format.formatter -> ('a, string) t -> unit
+  val pp_labeled :
+    Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, string) t -> unit
 
   (** Print indexed *)
-  val pp_indexed : Format.formatter -> ('a, int) t -> unit
+  val pp_indexed : Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, int) t -> unit
 end
 
 (** @canonical Gillian.Gil_syntax.Visitors *)

GillianCore/GIL_Syntax/Proc.ml

@@ -19,7 +19,12 @@ type ('annot, 'label) t = ('annot, 'label) TypeDef__.proc = {
 
 let get_params proc = proc.proc_params
 
-let pp ~(show_labels : bool) ~(pp_label : 'a Fmt.t) fmt labproc =
+let pp
+    ~(show_labels : bool)
+    ~(pp_label : 'a Fmt.t)
+    ?(pp_annot : 'b Fmt.t option)
+    fmt
+    labproc =
   let {
     proc_name = name;
     proc_source_path = path;
@@ -42,16 +47,28 @@ let pp ~(show_labels : bool) ~(pp_label : 'a Fmt.t) fmt labproc =
       Fmt.pf fmt " "
     done
   in
-  let pp_cmd_triple fmt (_, lab, cmd) =
+  let pp_annot =
+    match (pp_annot, !Config.dump_annots) with
+    | Some pp_annot, true ->
+        fun fmt annot ->
+          let annot_s =
+            Fmt.str "%a" pp_annot annot
+            |> Str.(global_replace (regexp_string "*)") "* )")
+          in
+          Fmt.pf fmt "    (* %s *)" annot_s
+    | _ -> fun fmt -> Fmt.nop fmt
+  in
+  let pp_cmd_triple fmt (annot, lab, cmd) =
     if show_labels then
       match lab with
       | None ->
-          Fmt.pf fmt "%a%a" pp_white (max_size_lab + 2) (Cmd.pp ~pp_label) cmd
+          Fmt.pf fmt "%a%a%a" pp_white (max_size_lab + 2) (Cmd.pp ~pp_label) cmd
+            pp_annot annot
       | Some l ->
-          Fmt.pf fmt "%a:%a%a" pp_label l pp_white
+          Fmt.pf fmt "%a:%a%a%a" pp_label l pp_white
             (max_size_lab - len_lab l + 1)
-            (Cmd.pp ~pp_label) cmd
-    else Fmt.pf fmt "%a" (Cmd.pp ~pp_label) cmd
+            (Cmd.pp ~pp_label) cmd pp_annot annot
+    else Fmt.pf fmt "%a%a" (Cmd.pp ~pp_label) cmd pp_annot annot
   in
   let pp_spec_opt fmt = function
     | None -> ()
@@ -72,8 +89,11 @@ let pp ~(show_labels : bool) ~(pp_label : 'a Fmt.t) fmt labproc =
     (Fmt.array ~sep:(Fmt.any ";@\n") pp_cmd_triple)
     body
 
-let pp_labeled fmt c = pp ~show_labels:true ~pp_label:Fmt.string fmt c
-let pp_indexed fmt c = pp ~show_labels:false ~pp_label:Fmt.int fmt c
+let pp_labeled fmt ?pp_annot c =
+  pp ~show_labels:true ~pp_label:Fmt.string ?pp_annot fmt c
+
+let pp_indexed fmt ?pp_annot c =
+  pp ~show_labels:false ~pp_label:Fmt.int ?pp_annot fmt c
 
 let indexed_of_labeled (lproc : ('annot, string) t) : ('annot, int) t =
   let no_of_cmds = Array.length lproc.proc_body in

GillianCore/GIL_Syntax/Prog.ml

@@ -157,7 +157,12 @@ let get_lemma_exn (prog : ('a, 'b) t) (name : string) : Lemma.t =
   | Some lemma -> lemma
   | None -> failwith (Printf.sprintf "could not find lemma %s" name)
 
-let pp ~(show_labels : bool) ~(pp_label : 'b Fmt.t) fmt (prog : ('a, 'b) t) =
+let pp
+    ~(show_labels : bool)
+    ~(pp_label : 'b Fmt.t)
+    ?(pp_annot : 'a Fmt.t option)
+    fmt
+    (prog : ('a, 'b) t) =
   let proc_names = Hashtbl.to_seq_keys prog.procs in
   let pp_list ppp = Fmt.list ~sep:(Fmt.any "@\n") ppp in
   let npp pp =
@@ -189,11 +194,14 @@ let pp ~(show_labels : bool) ~(pp_label : 'b Fmt.t) fmt (prog : ('a, 'b) t) =
     (get_ospecs prog)
     (pp_list (npp BiSpec.pp))
     (get_bispecs prog)
-    (pp_list (npp (Proc.pp ~show_labels ~pp_label)))
+    (pp_list (npp (Proc.pp ~show_labels ~pp_label ?pp_annot)))
     (get_procs ~proc_names:(List.of_seq proc_names) prog)
 
-let pp_labeled fmt x = pp ~show_labels:true ~pp_label:Fmt.string fmt x
-let pp_indexed fmt x = pp ~show_labels:false ~pp_label:Fmt.int fmt x
+let pp_labeled fmt ?pp_annot c =
+  pp ~show_labels:true ~pp_label:Fmt.string ?pp_annot fmt c
+
+let pp_indexed fmt ?pp_annot c =
+  pp ~show_labels:false ~pp_label:Fmt.int ?pp_annot fmt c
 
 (* let perform_syntax_checks (prog : t) : unit =
    if (!Config.perform_syntax_checks)

GillianCore/command_line/act_console.ml

@@ -55,12 +55,17 @@ struct
       in
       (labeled_prog, init_data, None)
 
+  let pp_annot fmt annot =
+    Fmt.pf fmt "%a"
+      (Yojson.Safe.pretty_print ?std:None)
+      (PC.Annot.to_yojson annot)
+
   let emit_specs e_prog prog file =
     let () = Prog.update_specs e_prog MP.(prog.prog) in
     let fname = Filename.chop_extension (Filename.basename file) in
     let dirname = Filename.dirname file in
     let out_path = Filename.concat dirname (fname ^ "_bi.gil") in
-    Io_utils.save_file_pp out_path Prog.pp_labeled e_prog
+    Io_utils.save_file_pp out_path (Prog.pp_labeled ~pp_annot) e_prog
 
   let make_callgraph (prog : ('a, 'b) Prog.t) =
     let fcalls =
@@ -97,7 +102,8 @@ struct
       parse_eprog file files already_compiled
     in
     let () =
-      burn_gil ~init_data:(ID.to_yojson init_data) ~pp_prog:Prog.pp_labeled
+      burn_gil ~init_data:(ID.to_yojson init_data)
+        ~pp_prog:(Prog.pp_labeled ~pp_annot)
         e_prog outfile_opt
     in
     let () =

GillianCore/command_line/c_interpreter_console.ml

@@ -70,7 +70,8 @@ struct
     let () = PC.initialize Concrete in
     let e_prog, init_data = parse_eprog files already_compiled in
     let () =
-      burn_gil ~init_data:(ID.to_yojson init_data) ~pp_prog:Prog.pp_labeled
+      burn_gil ~init_data:(ID.to_yojson init_data)
+        ~pp_prog:(Prog.pp_labeled ?pp_annot:None)
         e_prog outfile_opt
     in
     let prog =

GillianCore/command_line/command_line.ml

@@ -16,7 +16,9 @@ module Make
          and type memory_error = SMemory.err_t
          and type tl_ast = PC.tl_ast
          and type cmd_report = V.SAInterpreter.Logging.ConfigReport.t
-         and type annot = PC.Annot.t) =
+         and type annot = PC.Annot.t
+         and type init_data = ID.t
+         and type pc_err = PC.err) =
 struct
   module Gil_parsing = Gil_parsing.Make (PC.Annot)
   module CState = CState.Make (CMemory)

GillianCore/command_line/command_line.mli

@@ -19,7 +19,9 @@ module Make
          and type memory_error = SMemory.err_t
          and type tl_ast = PC.tl_ast
          and type cmd_report = V.SAInterpreter.Logging.ConfigReport.t
-         and type annot = PC.Annot.t) : sig
+         and type annot = PC.Annot.t
+         and type init_data = ID.t
+         and type pc_err = PC.err) : sig
   (** Parses command-line arguments and starts the requested Gillian execution *)
   val main : unit -> unit
 end

GillianCore/command_line/common_args.ml

@@ -137,6 +137,10 @@ module Make (PC : ParserAndCompiler.S) = struct
     let doc = "Dump every smt query sent to the solver" in
     Arg.(value & flag & info [ "dump-smt" ] ~doc)
 
+  let dump_annots =
+    let doc = "Dump annotations produced in compilation" in
+    Arg.(value & flag & info [ "dump-annots" ] ~doc)
+
   let use (term : (unit -> unit) Term.t) : unit Term.t =
     let apply_common
         logging_mode
@@ -146,7 +150,8 @@ module Make (PC : ParserAndCompiler.S) = struct
         tl_opts
         result_dir
         pbn
-        dump_smt =
+        dump_smt
+        dump_annots =
       Config.set_result_dir result_dir;
       Config.ci := ci;
       Logging.Mode.set_mode logging_mode;
@@ -157,12 +162,14 @@ module Make (PC : ParserAndCompiler.S) = struct
       Config.set_runtime_paths ?default_folders:PC.default_import_paths
         runtime_path;
       Config.pbn := pbn;
-      Config.dump_smt := dump_smt
+      Config.dump_smt := dump_smt;
+      Config.dump_annots := dump_annots
     in
     let common_term =
       Term.(
         const apply_common $ logging_mode $ reporters $ runtime_path $ ci
-        $ PC.TargetLangOptions.term $ result_directory $ pbn $ dump_smt)
+        $ PC.TargetLangOptions.term $ result_directory $ pbn $ dump_smt
+        $ dump_annots)
     in
     Term.(term $ common_term)
 end

GillianCore/command_line/compiler_console.ml

@@ -27,10 +27,17 @@ module Make
       ParserAndCompiler.get_progs_or_fail ~pp_err:PC.pp_err
         (PC.parse_and_compile_files files)
     in
+    let pp_annot fmt annot =
+      Fmt.pf fmt "%a"
+        (Yojson.Safe.pretty_print ?std:None)
+        (PC.Annot.to_yojson annot)
+    in
     List.iteri
       (fun i (path, prog) ->
         let init_data = if i = 0 then ID.to_yojson progs.init_data else `Null in
-        burn_gil ~init_data ~pp_prog:Prog.pp_labeled prog (Some path))
+        burn_gil ~init_data
+          ~pp_prog:(Prog.pp_labeled ~pp_annot)
+          prog (Some path))
       progs.gil_progs
 
   let compile files mode runtime_path ci tl_opts =

GillianCore/command_line/s_interpreter_console.ml

@@ -184,8 +184,14 @@ struct
       parse_eprog files already_compiled
     in
     let () =
-      burn_gil ~pp_prog:Prog.pp_labeled ~init_data:(ID.to_yojson init_data)
-        e_prog outfile_opt
+      let pp_annot fmt annot =
+        Fmt.pf fmt "%a"
+          (Yojson.Safe.pretty_print ?std:None)
+          (PC.Annot.to_yojson annot)
+      in
+      burn_gil
+        ~pp_prog:(Prog.pp_labeled ~pp_annot)
+        ~init_data:(ID.to_yojson init_data) e_prog outfile_opt
     in
     let () = L.normal (fun m -> m "*** Stage 2: Transforming the program.\n") in
     let prog =