From 1ff54deac0036cd1dd1bdf5a8d91684e431483a7 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 18 Aug 2025 19:08:29 +0200 Subject: [PATCH 1/2] EcRegexp: PCRE -> PCRE2 --- src/dune | 4 ++-- src/ecRegexp.ml | 39 +++++++++++++++++++++------------------ 2 files changed, 23 insertions(+), 20 deletions(-) diff --git a/src/dune b/src/dune index 165e935b92..d3e8093146 100644 --- a/src/dune +++ b/src/dune @@ -15,7 +15,7 @@ (public_name easycrypt.ecLib) (foreign_stubs (language c) (names eunix)) (modules :standard \ ec) - (libraries batteries camlp-streams dune-build-info dune-site inifiles why3 yojson zarith) + (libraries batteries camlp-streams dune-build-info dune-site inifiles pcre2 why3 yojson zarith) ) (executable @@ -23,7 +23,7 @@ (name ec) (modules ec) (promote (until-clean)) - (libraries batteries camlp-streams dune-build-info dune-site inifiles why3 yojson zarith ecLib)) + (libraries batteries camlp-streams dune-build-info dune-site inifiles pcre2 why3 yojson zarith ecLib)) (ocamllex ecLexer) diff --git a/src/ecRegexp.ml b/src/ecRegexp.ml index f80473bfa8..e1230c3d5d 100644 --- a/src/ecRegexp.ml +++ b/src/ecRegexp.ml @@ -1,6 +1,9 @@ (* -------------------------------------------------------------------- *) open EcUtils +(* -------------------------------------------------------------------- *) +module PcreBck = Pcre2 + (* -------------------------------------------------------------------- *) type split = | Text of string @@ -33,12 +36,12 @@ end (* -------------------------------------------------------------------- *) module PcreCore : CORE = struct - type regexp = Pcre.regexp - type subst = Pcre.substitution - type match_ = Pcre.substrings + type regexp = PcreBck.regexp + type subst = PcreBck.substitution + type match_ = PcreBck.substrings type error = - | PCREError of Pcre.error + | PCREError of PcreBck.error | InvalidSubString of int | InvalidBackRef @@ -46,47 +49,47 @@ module PcreCore : CORE = struct let wrap (f : 'a -> 'b) (x : 'a) = try f x - with Pcre.Error err -> raise (Error (PCREError err)) + with PcreBck.Error err -> raise (Error (PCREError err)) - let quote (x : string) = (wrap Pcre.quote ) x - let regexp (x : string) = (wrap Pcre.regexp) x - let subst (x : string) = (wrap Pcre.subst ) x + let quote (x : string) = (wrap PcreBck.quote ) x + let regexp (x : string) = (wrap PcreBck.regexp) x + let subst (x : string) = (wrap PcreBck.subst ) x let exec ?(pos = 0) (rex : regexp) (x : string) = - try Some (wrap (Pcre.exec ~pos ~rex) x) + try Some (wrap (PcreBck.exec ~pos ~rex) x) with Not_found -> None let split ?(pos = 0) (rex : regexp) (x : string) = let convert = function - | Pcre.Text s -> Some (Text s) - | Pcre.Delim s -> Some (Delim s) + | PcreBck.Text s -> Some (Text s) + | PcreBck.Delim s -> Some (Delim s) | _ -> None - in List.pmap convert (wrap (Pcre.full_split ~pos ~rex) x) + in List.pmap convert (wrap (PcreBck.full_split ~pos ~rex) x) let sub (rex : regexp) (subst : subst) (x : string) = - try wrap (Pcre.replace ~rex ~itempl:subst) x + try wrap (PcreBck.replace ~rex ~itempl:subst) x with Failure _ -> raise (Error InvalidBackRef) let extract (rex : regexp) (x : string) = - try wrap (Pcre.extract_all_opt ~full_match:true ~rex) x + try wrap (PcreBck.extract_all_opt ~full_match:true ~rex) x with Not_found -> [||] module Match = struct let count (m : match_) : int = - (wrap Pcre.num_of_subs) m + (wrap PcreBck.num_of_subs) m let group (m : match_) (i : int) : string option = - try Some (wrap (Pcre.get_substring m) i) + try Some (wrap (PcreBck.get_substring m) i) with | Invalid_argument _ -> raise (Error (InvalidSubString i)) | Not_found -> None let groups (m : match_) : (string option) array = - wrap (Pcre.get_opt_substrings ~full_match:true) m + wrap (PcreBck.get_opt_substrings ~full_match:true) m let offset (m : match_) (i : int) : (int * int) option = - try Some (wrap (Pcre.get_substring_ofs m) i) + try Some (wrap (PcreBck.get_substring_ofs m) i) with | Invalid_argument _ -> raise (Error (InvalidSubString i)) | Not_found -> None From 8032ec0844e11e345afb7f40a7a5b27153a35ade Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 18 Aug 2025 19:23:11 +0200 Subject: [PATCH 2/2] port inifiles to PCRE2 & vendor it --- 3rdparty/inifiles-1.2/dune | 8 + 3rdparty/inifiles-1.2/inifiles.ml | 267 +++++++++++++++++++++++++++++ 3rdparty/inifiles-1.2/inifiles.mli | 101 +++++++++++ 3rdparty/inifiles-1.2/inilexer.mll | 35 ++++ 3rdparty/inifiles-1.2/parseini.mly | 39 +++++ dune | 2 +- dune-project | 3 +- easycrypt.opam | 3 +- 8 files changed, 453 insertions(+), 5 deletions(-) create mode 100644 3rdparty/inifiles-1.2/dune create mode 100644 3rdparty/inifiles-1.2/inifiles.ml create mode 100644 3rdparty/inifiles-1.2/inifiles.mli create mode 100644 3rdparty/inifiles-1.2/inilexer.mll create mode 100644 3rdparty/inifiles-1.2/parseini.mly diff --git a/3rdparty/inifiles-1.2/dune b/3rdparty/inifiles-1.2/dune new file mode 100644 index 0000000000..17a9e245f6 --- /dev/null +++ b/3rdparty/inifiles-1.2/dune @@ -0,0 +1,8 @@ +(library + (name inifiles) + (public_name easycrypt.inifiles) + (modules :standard) + (libraries pcre2 unix)) + +(ocamllex inilexer) +(ocamlyacc parseini) diff --git a/3rdparty/inifiles-1.2/inifiles.ml b/3rdparty/inifiles-1.2/inifiles.ml new file mode 100644 index 0000000000..7fd2d26495 --- /dev/null +++ b/3rdparty/inifiles-1.2/inifiles.ml @@ -0,0 +1,267 @@ +(* A small library to read and write .ini files + + Copyright (C) 2004 Eric Stokes, and The California State University + at Northridge + + This library is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License as published by the Free Software Foundation; either + version 2.1 of the License, or (at your option) any later version. + + This library is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with this library; if not, write to the Free Software + Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +*) + + +module Pcre = Pcre2 + +open Pcre +open Parseini +open Inilexer + +exception Invalid_section of string +exception Invalid_element of string +exception Missing_section of string +exception Missing_element of string +exception Ini_parse_error of (int * string) + +type attribute_specification = { + atr_name: string; + atr_required: bool; + atr_default: (string list) option; + atr_validator: Pcre.regexp option; +} + +type section_specification = { + sec_name: string; + sec_required: bool; + sec_attributes: attribute_specification list; +} + +type specification = section_specification list + +let comment = regexp "^#.*$" + +module Ordstr = +struct + type t = string + let compare (x:t) (y:t) = + String.compare (String.lowercase_ascii x) (String.lowercase_ascii y) +end + +module Strset = Set.Make(Ordstr) + +let setOfList list = + let rec dosetOfList list set = + match list with + a :: tail -> dosetOfList tail (Strset.add a set) + | [] -> set + in + dosetOfList list Strset.empty + +let rec filterfile ?(buf=Buffer.create 500) f fd = + try + let theline = input_line fd in + if f theline then begin + Buffer.add_string buf (theline ^ "\n"); + filterfile ~buf f fd + end + else + filterfile ~buf f fd + with End_of_file -> Buffer.contents buf + +let read_inifile file fd tbl = + let lxbuf = + Lexing.from_string + (filterfile + (fun line -> not (Pcre.pmatch ~rex:comment line)) + fd) + in + try + let parsed_file = inifile lexini lxbuf in + List.iter + (fun (section, values) -> + Hashtbl.add tbl section + (List.fold_left + (fun tbl (key, value) -> Hashtbl.add tbl key value;tbl) + (Hashtbl.create 10) + values)) + parsed_file + with Parsing.Parse_error | Failure _ -> + raise (Ini_parse_error (lxbuf.Lexing.lex_curr_p.Lexing.pos_lnum, file)) + +let write_inifile fd tbl = + Hashtbl.iter + (fun k v -> + output_string fd "[";output_string fd k;output_string fd "]\n"; + (Hashtbl.iter + (fun k v -> + output_string fd k;output_string fd " = ";output_string fd v; + output_string fd "\n") v); + output_string fd "\n") + tbl + +class inifile ?(spec=[]) file = +object (self) + val file = file + val data = Hashtbl.create 50 + + initializer + let inch = open_in file in + (try read_inifile file inch data + with exn -> close_in inch;raise exn); + close_in inch; + self#validate + + method private validate = + match spec with + [] -> () + | spec -> + List.iter + (fun {sec_name=name;sec_required=required; + sec_attributes=attrs} -> + try + let sec = + try Hashtbl.find data name + with Not_found -> raise (Missing_section name) + in + List.iter + (fun {atr_name=name;atr_required=req; + atr_default=def;atr_validator=validator} -> + try + let attr_val = + try Hashtbl.find sec name + with Not_found -> raise (Missing_element name) + in + (match validator with + Some rex -> + if not (Pcre.pmatch ~rex:rex attr_val) then + raise + (Invalid_element + (name ^ ": validation failed")) + | None -> ()) + with Missing_element elt -> + if req then raise (Missing_element elt) + else match def with + Some def -> List.iter (Hashtbl.add sec name) def + | None -> ()) + attrs + with Missing_section s -> + if required then raise (Missing_section s)) + spec + + method getval sec elt = + try Hashtbl.find + (try (Hashtbl.find data sec) + with Not_found -> raise (Invalid_section sec)) + elt + with Not_found -> raise (Invalid_element elt) + + method getaval sec elt = + try Hashtbl.find_all + (try (Hashtbl.find data sec) + with Not_found -> raise (Invalid_section sec)) + elt + with Not_found -> raise (Invalid_element elt) + + method setval sec elt v = + (Hashtbl.add + (try Hashtbl.find data sec + with Not_found -> + let h = Hashtbl.create 10 in + Hashtbl.add data sec h;h) + elt v); + try self#validate + with exn -> Hashtbl.remove data elt;raise exn + + method delval sec elt = + let valu = + try + Some + (Hashtbl.find + (try Hashtbl.find data sec + with Not_found -> raise (Invalid_section sec)) + elt) + with Not_found -> None + in + match valu with + Some v -> + ((Hashtbl.remove + (try Hashtbl.find data sec + with Not_found -> raise (Invalid_section sec)) + elt); + try self#validate + with exn -> + (Hashtbl.add + (try Hashtbl.find data sec + with Not_found -> raise (Invalid_section sec)) + elt v); + raise exn) + | None -> () + + + method sects = + (Hashtbl.fold + (fun k _v keys -> k :: keys) + data []) + + method iter func sec = + (Hashtbl.iter func + (try Hashtbl.find data sec + with Not_found -> raise (Invalid_section sec))) + + method attrs sec = + (Strset.elements + (setOfList + (Hashtbl.fold + (fun k _v attrs -> k :: attrs) + (try Hashtbl.find data sec + with Not_found -> raise (Invalid_section sec)) + []))) + + method save ?(file = file) () = + let outch = open_out file in + write_inifile outch data; + flush outch; +end + +let readdir path = + let dir = Unix.handle_unix_error Unix.opendir path in + let rec do_read dir = + try + let current = Unix.readdir dir in + current :: (do_read dir) + with End_of_file -> [] + in + let lst = do_read dir in + Unix.closedir dir; + lst + +let fold func path initial = + let check_file path = + match + (path, + (try (Unix.stat path).Unix.st_kind + with Unix.Unix_error (_,_,_) -> Unix.S_DIR)) + with + (_name, Unix.S_REG) when + (Pcre.pmatch ~rex:(Pcre.regexp "^.*\\.ini$") path) -> + true + | _ -> false + in + (List.fold_left + func + initial + (List.rev_map + (fun x -> new inifile x) + (List.filter + check_file + (List.rev_map + (fun p -> (path ^ "/" ^ p)) + (readdir path))))) diff --git a/3rdparty/inifiles-1.2/inifiles.mli b/3rdparty/inifiles-1.2/inifiles.mli new file mode 100644 index 0000000000..b186a4ce3b --- /dev/null +++ b/3rdparty/inifiles-1.2/inifiles.mli @@ -0,0 +1,101 @@ +(* A small library to read and write .ini files + + Copyright (C) 2004 Eric Stokes, and The California State University + at Northridge + + This library is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License as published by the Free Software Foundation; either + version 2.1 of the License, or (at your option) any later version. + + This library is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with this library; if not, write to the Free Software + Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +*) + + +(** This library reads ini format property files *) + +(** raised if you ask for a section which doesn't exist *) +exception Invalid_section of string + +(** raised if you ask for an element (attribute) which doesn't exist, + or the element fails to match the validation regex *) +exception Invalid_element of string + +(** raised if a required section is not specified in the config file *) +exception Missing_section of string + +(** raised if a required element is not specified in the config file *) +exception Missing_element of string + +(** raised if there is a parse error in the ini file it will contain the + line number and the name of the file in which the error happened *) +exception Ini_parse_error of (int * string) + +(** The type of an attribute/element specification *) +type attribute_specification = { + atr_name: string; + atr_required: bool; + atr_default: (string list) option; + atr_validator: Pcre2.regexp option; +} + +(** The type of a section specification *) +type section_specification = { + sec_name: string; + sec_required: bool; + sec_attributes: attribute_specification list; +} + +(** The type of a secification *) +type specification = section_specification list + +(** send the name of an ini file to the constructor the file must + exist, but can be empty *) +class inifile : ?spec:specification -> string -> +object + (** get a value from the config object raise Invalid_section, or + invalid_element on error. getval section element *) + method getval : string -> string -> string + + (** get a value from the config object. return a list of all the + objects bindings. If the key is listed on more than one line it + will get n bindings, where n is the number of lines it is + mentioned on. raise Invalid_section, or invalid_element on error. + getaval section element *) + method getaval : string -> string -> string list + + (** set a value in the config create a new section, and or element + if necessary. setval section element *) + method setval : string -> string -> string -> unit + + (** delete the topmost binding (the one returned by getval) from the + section sec. Possibly exposeing another binding. raise + Invalid_section on error. delval sec elt *) + method delval : string -> string -> unit + + (** save the changes you have made + optionally save to a different file *) + method save : ?file:string -> unit -> unit + + (** iterates across a section. passes all key valu pairs to f + exactly once.*) + method iter : (string -> string -> unit) -> string -> unit + + (** returns a list of all sections in the file *) + method sects : string list + + (** return all the attibutes of a section *) + method attrs : string -> string list +end + +(** Executes a fold left across a directory of ini files + (skips files which do not end with .ini). fold f path a + computes (f ... (f (f file1 a) file2) fileN) *) +val fold: ('a -> inifile -> 'a) -> string -> 'a -> 'a diff --git a/3rdparty/inifiles-1.2/inilexer.mll b/3rdparty/inifiles-1.2/inilexer.mll new file mode 100644 index 0000000000..0787905de8 --- /dev/null +++ b/3rdparty/inifiles-1.2/inilexer.mll @@ -0,0 +1,35 @@ +(* A small library to read and write .ini files + + Copyright (C) 2004 Eric Stokes, and The California State University + at Northridge + + This library is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License as published by the Free Software Foundation; either + version 2.1 of the License, or (at your option) any later version. + + This library is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with this library; if not, write to the Free Software + Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +*) + + +{ + open Parseini +} + +let newline = '\n' + +let whsp = ( [ ' ' '\t' ] | '\\' newline ) * +let id = ['-' '_' ':' '0' - '9' 'A' - 'Z' 'a' - 'z' ] + +let value = ( [ '\t' ' ' - '~' ] | '\\' newline | '\\' '#' ) + + +rule lexini = parse + whsp '[' whsp (id as id) whsp ']' {Section id} + | whsp (id as id) whsp '=' whsp (value as value) whsp {Value (id, value)} + | newline {Newline} + | eof {EOF} diff --git a/3rdparty/inifiles-1.2/parseini.mly b/3rdparty/inifiles-1.2/parseini.mly new file mode 100644 index 0000000000..da11a1025f --- /dev/null +++ b/3rdparty/inifiles-1.2/parseini.mly @@ -0,0 +1,39 @@ +/* A small library to read and write .ini files + + Copyright (C) 2004 Eric Stokes, and The California State University + at Northridge + + This library is free software; you can redistribute it and/or + modify it under the terms of the GNU Lesser General Public + License as published by the Free Software Foundation; either + version 2.1 of the License, or (at your option) any later version. + + This library is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU + Lesser General Public License for more details. + + You should have received a copy of the GNU Lesser General Public + License along with this library; if not, write to the Free Software + Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +*/ + + +%token Newline EOF +%token Section +%token Value +%type <(string * ((string * string) list)) list> inifile +%start inifile +%% + +values: + Value Newline values {$1 :: $3} +| Value Newline {[$1]} + +ini: + Section Newline values inifile {($1, $3) :: $4} +| Section Newline values {[($1, $3)]} + +inifile: + ini EOF {$1} +| Newline ini EOF {$2} diff --git a/dune b/dune index c588ae3ca4..7d254fcb7c 100644 --- a/dune +++ b/dune @@ -1,4 +1,4 @@ -(dirs src theories examples scripts) +(dirs 3rdparty src theories examples scripts) (install (section (site (easycrypt commands))) diff --git a/dune-project b/dune-project index ef32228ab9..298334722c 100644 --- a/dune-project +++ b/dune-project @@ -19,8 +19,7 @@ dune dune-build-info dune-site - (ocaml-inifiles (>= 1.2)) - (pcre (>= 7)) + (pcre2 (>= 8)) (why3 (and (>= 1.8.0) (< 1.9))) yojson (zarith (>= 1.10)) diff --git a/easycrypt.opam b/easycrypt.opam index 6a95a04800..47ea3eb083 100644 --- a/easycrypt.opam +++ b/easycrypt.opam @@ -7,8 +7,7 @@ depends: [ "dune" {>= "3.13"} "dune-build-info" "dune-site" - "ocaml-inifiles" {>= "1.2"} - "pcre" {>= "7"} + "pcre2" {>= "8"} "why3" {>= "1.8.0" & < "1.9"} "yojson" "zarith" {>= "1.10"}