Disable zip feature in Bytecode mode

As Basile noticed, the Javascript code in `My_zip` is dead too. I
removed it and clean a bit the module.

I also produces an appropriate `run error` if we try to use the feature
in Javascript because `camlzip` does not work properly in bytecode.

Currently, the error cannot be trigger because we do not use yet the
Dolmen version of `Solving_loop` in the javascript worker. This will
change in my next PR.

src/bin/common/solving_loop.ml

@@ -32,6 +32,9 @@ module DO = D_state_option
 module Sy = Symbols
 module O = Options
 
+let src = Logs.Src.create ~doc:"Solving_loop" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 type solver_ctx = {
   ctx    : Commands.sat_tdecl list;
   local  : Commands.sat_tdecl list;
@@ -1048,6 +1051,9 @@ let main () =
   in
 
   let filename = O.get_file () in
-  match O.get_frontend () with
-  | "dolmen" -> d_fe filename
-  | frontend -> ae_fe filename frontend
+  try
+    match O.get_frontend () with
+    | "dolmen" -> d_fe filename
+    | frontend -> ae_fe filename frontend
+  with Errors.Error e ->
+    Log.err (fun k -> k "%a" Errors.report e)

src/lib/structures/errors.ml

@@ -82,6 +82,7 @@ type run_error =
   | Unsupported_feature of string
   | Dynlink_error of string
   | Stack_underflow
+  | Invalid_zip of string
 
 type mode_error =
   | Invalid_set_option of string
@@ -122,6 +123,9 @@ let invalid_set_option mode opt_key =
 let forbidden_command mode cmd_name =
   error (Mode_error (mode, Forbidden_command cmd_name))
 
+let unsupported_feature msg =
+  Format.kasprintf (fun s -> run_error (Unsupported_feature s)) msg
+
 let report_typing_error fmt = function
   | BitvExtract(i,j) ->
     fprintf fmt "bitvector extraction malformed (%d>%d)" i j
@@ -250,6 +254,8 @@ let report_run_error fmt = function
     fprintf fmt "[Dynlink] %s" s
   | Stack_underflow ->
     fprintf fmt "The stack of the assertion levels is empty"
+  | Invalid_zip filename ->
+    Fmt.pf fmt "The zipped file '%s' should contain exactly one file." filename
 
 let report_mode_error fmt = function
   | Invalid_set_option s ->

src/lib/structures/errors.mli

@@ -89,6 +89,7 @@ type run_error =
   | Unsupported_feature of string
   | Dynlink_error of string
   | Stack_underflow
+  | Invalid_zip of string
 
 (** Errors raised when performing actions forbidden in some modes. *)
 type mode_error =
@@ -145,6 +146,8 @@ val invalid_set_option : Util.mode -> string -> 'a
     being used in a mode where it should not be available. *)
 val forbidden_command : Util.mode -> string -> 'a
 
+val unsupported_feature : ('a, Format.formatter, unit, 'b) format4 -> 'a
+
 (** {2 Printing } *)
 
 (** Print a message on the formatter corresponding to the error *)

src/lib/util/my_zip.ml

@@ -25,54 +25,31 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** A wrapper of the Zip module of CamlZip: we use Zip except when we want to
-    generate the.js file for try-Alt-Ergo. *)
+[@@@ocaml.warning "-32-33"]
+(** A wrapper of the Zip module of CamlZip *)
 
-module ZipWrapper = struct
-  include Zip
-  let filename e = e.Zip.filename
-  let is_directory e = e.Zip.is_directory
-end
+let src = Logs.Src.create ~doc:"My_zip" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
 
-include ZipWrapper
+open Zip
 
-let extract_zip_file f =
-  let cin = open_in f in
-  try
-    match entries cin with
-    | [e] when not @@ is_directory e ->
-      if Options.get_verbose () then
-        Printer.print_dbg
-          ~module_name:"My_zip" ~function_name:"extract_zip_file"
-          "I'll read the content of '%s' in the given zip"
-          (filename e);
-      let content = read_entry cin e in
-      close_in cin;
-      content
-    | _ ->
-      close_in cin;
-      raise (Arg.Bad
-               (Format.sprintf "%s '%s' %s@?"
-                  "The zipped file" f
-                  "should contain exactly one file."))
-  with e ->
-    close_in cin;
-    raise e
-
-(* !! This commented code is used when compiling to javascript !!
-   module DummyZip = struct
-   type entry = unit
-   type in_file = unit
+let filename e = e.Zip.filename
+let is_directory e = e.Zip.is_directory
 
-   let s = "Zip module not available for your setting or has been disabled !"
-
-   let open_in  _  =  failwith s
-   let close_in _ = failwith s
-   let entries  _  =  failwith s
-   let read_entry  _ _  =  failwith s
-   let filename  _  =  failwith s
-   let is_directory  _  =  failwith s
-   end
+let extract_zip_file f =
+  if Stdlib.(Sys.backend_type = Bytecode) then
+    Errors.unsupported_feature "Zip format in javascript mode";
 
-   include DummyZip
-*)
+  let cin = open_in f in
+  Fun.protect ~finally:(fun () -> close_in cin) @@ fun () ->
+  match entries cin with
+  | [e] when not @@ is_directory e ->
+    if Options.get_verbose () then
+      Log.debug
+        (fun k -> k "Extract the content of '%s' in the given zip"
+            (filename e));
+    read_entry cin e
+  | _ ->
+    Errors.run_error (Invalid_zip f)
+
+include Zip

src/lib/util/my_zip.mli

@@ -25,8 +25,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** A wrapper of the Zip module of CamlZip: we use Zip except when we want to
-    generate the.js file for try-Alt-Ergo **)
+(** A wrapper of the Zip module of CamlZip. **)
 
 type in_file
 type entry