From 9f5dbd7cdaadebe023d29109ae48cf796206ebac Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 31 Oct 2024 15:53:06 +0100 Subject: [PATCH] Remove My_zip module (#1264) * Use similar test for zip feature in native and SMT format We should use the same test as we only want to check that Alt-Ergo can unzip correctly the input file if its name has the form: name.format.zip. * Remove My_zip The module `My_Zip` contains only function which is called once in `Solving_loop`. This commit cleans the code and move it in `Solving_loop` directly. Technically, `Solving_loop` is a part of the binary, but as everyone knows, most of the code of this module will be push into the library after we design a good API. * Force deflate compression in zip tests Add a padding comment in both tests to ensure that zip won't choose the store method while compressing them. --- src/bin/common/solving_loop.ml | 11 ++++- src/lib/dune | 2 +- src/lib/util/my_zip.ml | 78 --------------------------------- src/lib/util/my_zip.mli | 48 -------------------- tests/misc/unzip.ae.expected | 2 +- tests/misc/unzip.ae.zip | Bin 203 -> 277 bytes tests/misc/unzip.smt2.zip | Bin 531 -> 299 bytes 7 files changed, 12 insertions(+), 129 deletions(-) delete mode 100644 src/lib/util/my_zip.ml delete mode 100644 src/lib/util/my_zip.mli diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 10db9c4751..a35411d7bd 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -305,6 +305,15 @@ let process_source ?selector_inst ~print_status src = end | `Stdin -> () in + let extract_zip_file f = + let cin = Zip.open_in f in + Fun.protect ~finally:(fun () -> Zip.close_in cin) @@ fun () -> + match Zip.entries cin with + | [e] when not @@ e.Zip.is_directory -> + Zip.read_entry cin e + | _ -> + fatal_error "the zip archive '%s' should contain exactly one file" f + in (* Prepare the input source for Dolmen from an input source for Alt-Ergo. *) let mk_files src = let lang = @@ -316,7 +325,7 @@ let process_source ?selector_inst ~print_status src = let src = match src with | `File path when Filename.check_suffix path ".zip" -> - let content = AltErgoLib.My_zip.extract_zip_file path in + let content = extract_zip_file path in `Raw (Filename.(chop_extension path |> basename), content) | `File _ | `Raw _ | `Stdin -> src in diff --git a/src/lib/dune b/src/lib/dune index 30cc3b00b6..67f3b0de3c 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -61,7 +61,7 @@ ; util Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue Options Timers Util Vec Version Steps Printer - My_zip My_list Theories Nest Compat + My_list Theories Nest Compat ) (js_of_ocaml diff --git a/src/lib/util/my_zip.ml b/src/lib/util/my_zip.ml deleted file mode 100644 index d3efd8fd1f..0000000000 --- a/src/lib/util/my_zip.ml +++ /dev/null @@ -1,78 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -(** A wrapper of the Zip module of CamlZip: we use Zip except when we want to - generate the.js file for try-Alt-Ergo. *) - -module ZipWrapper = struct - include Zip - let filename e = e.Zip.filename - let is_directory e = e.Zip.is_directory -end - -include ZipWrapper - -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 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 - - include DummyZip -*) diff --git a/src/lib/util/my_zip.mli b/src/lib/util/my_zip.mli deleted file mode 100644 index 65ff2a6b65..0000000000 --- a/src/lib/util/my_zip.mli +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) --- OCamlPro SAS *) -(* *) -(* This file is distributed under the terms of OCamlPro *) -(* Non-Commercial Purpose License, version 1. *) -(* *) -(* As an exception, Alt-Ergo Club members at the Gold level can *) -(* use this file under the terms of the Apache Software License *) -(* version 2.0. *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) -(* More details can be found in the directory licenses/ *) -(* *) -(**************************************************************************) - -(** A wrapper of the Zip module of CamlZip: we use Zip except when we want to - generate the.js file for try-Alt-Ergo **) - -type in_file -type entry - -val open_in : string -> in_file - -val close_in : in_file -> unit - -val entries : in_file -> entry list - -val read_entry : in_file -> entry -> string - -val filename : entry -> string - -val is_directory : entry -> bool - -val extract_zip_file : string -> string -(** [extract_zip_file filename] extract the unique file of the zip archive - [filename] and its content. *) diff --git a/tests/misc/unzip.ae.expected b/tests/misc/unzip.ae.expected index a6e005255c..6f99ff0f44 100644 --- a/tests/misc/unzip.ae.expected +++ b/tests/misc/unzip.ae.expected @@ -1,2 +1,2 @@ -unknown +unsat diff --git a/tests/misc/unzip.ae.zip b/tests/misc/unzip.ae.zip index 9c7c81c8ce1b1019ffd7b29e9269901f6783ca3a..45f4ca3031cb6187cfff2be3f1b7f165b817885d 100644 GIT binary patch literal 277 zcmWIWW@Zs#U|`^2cvc-BS$4EQAs@(F$pjLSVJOY3$}G@JObrd;WMJMfML8XWODnh; z7+GF0GcbUOx7~((hYSQ*eperzHbF^f3dct-yM&|S_dTcI=+bBUSoKDKN$Xm--PX$) z{V#S2C0#LHxbVZV4?Jb?MPMkYCCTuzn%I-Y@n5r~&Gf>;O-utGe5=J)__ RRyL42Mj-S9(i=e>1^^xyT8{t# literal 203 zcmWIWW@h1H0D;5;!?4|QH`RH8Y!DV{H*UCpiCf^uZh@PvANEH+e%Y#h<5h@$ zewt1}e`jDUM`rv*!ysi3#6LW?bHo m0D6dlff0z8fc%EyDOQN5&^#32&B_K+$q0l2K>8?%!vFwNs$PQt literal 531 zcmWIWW@Zs#U|`^2;4Ux>Th#7dmCeY&aEY0Lfs;Xop(MW~U#~c~#3(d`lY#l!>|@Cw zTw1}+z{v6fs0K`w21jQfRuHMXzuw}Dr=+AIx3|@-zD>&y&HEh{lVv@#+u1jAp?zK4 zq-D!i^0S>Ux4a+NWMa&j|4k_FYriMUf1f^|Og-rn^Wr`*7wwq99(VXv^4?cma~-y= zN-OyHboTe+mMd2_G>53q_?UJ*Yq5ps=7{VSnWkHMmmOoW4&z=Gu_<5rMvf;J$KhQ& zU7uZMn6DQc?xwx;#mR;94436x&J?;jOOx5dVE4l9iyvQ1V|Uxib79k`#Gst;6~A*A zEObo`UV43j_Cgj8wtLgXr#(LQ_Iyxfw)MHicRN1c^LA}55Y+i-xr8}Hm;JnmP0L@! z4L^E~<_DFi=CSm@e9~4+yCQ{&;kzSGrKw0eSKP6 zTX}K%!E^Jb7v3lm*>~V?mBUx@)%z!Z5Wd;>?K6LXHzSiAGp_iO0LCK&12Fm+mNbG` cNU_HXi9NKK3-D%T11V$#LVqB=4y2a>07}ExGynhq