diff --git a/TCB/forbid_chdir.jsonnet b/TCB/forbid_chdir.jsonnet index fcaa59c2710a..b630fb224740 100644 --- a/TCB/forbid_chdir.jsonnet +++ b/TCB/forbid_chdir.jsonnet @@ -6,7 +6,7 @@ local common = import 'common.libsonnet'; id: 'forbid-chdir', match: { any: [ 'Unix.chdir','UUnix.chdir', - 'Sys.chdir', 'USys.chdir', + 'Sys.chdir', 'USys.chdir', ] }, languages: ['ocaml'], paths: common.exclude, diff --git a/TCB/forbid_exit.jsonnet b/TCB/forbid_exit.jsonnet index 8a1157017d70..e0d965c6f25f 100644 --- a/TCB/forbid_exit.jsonnet +++ b/TCB/forbid_exit.jsonnet @@ -5,11 +5,11 @@ local common = import 'common.libsonnet'; { id: 'forbid-exit', match: { any: [ - 'exit $N', + 'exit $N', 'Stdlib.exit', 'UStdlib.exit', - 'Unix._exit', - 'UUnix._exit' + 'Unix._exit', + 'UUnix._exit' ] }, languages: ['ocaml'], paths: common.exclude, diff --git a/TCB/forbid_misc.jsonnet b/TCB/forbid_misc.jsonnet index d2d169c5cde5..d7d36f70511b 100644 --- a/TCB/forbid_misc.jsonnet +++ b/TCB/forbid_misc.jsonnet @@ -5,7 +5,7 @@ local common = import 'common.libsonnet'; { id: 'forbid-random', match: { any: [ - 'Random.$F', + 'Random.$F', ] }, languages: ['ocaml'], paths: common.exclude, @@ -17,7 +17,7 @@ local common = import 'common.libsonnet'; { id: 'forbid-obj-magic', match: { any: [ - 'Obj.magic', + 'Obj.magic', ] }, languages: ['ocaml'], paths: { diff --git a/libs/commons/Common.ml b/libs/commons/Common.ml index c06315f1da4a..24ffcc78acf2 100644 --- a/libs/commons/Common.ml +++ b/libs/commons/Common.ml @@ -105,61 +105,7 @@ let ( != ) : hidden_by_your_nanny = () (*****************************************************************************) (* Comparison *) (*****************************************************************************) - -type order = Less | Equal | Greater - -(* We use this to be able to factorize our code for binary search, by - instantiating our code against different kinds of containers and - element types. - In particular, this is an improvement over functorization, because the - type of Bigarray.Array1.t is actually triply-polymorphic. By making the - container type itself unspecified, we are able to abstract over even - multiply-polymorphic containers. -*) -type ('elt, 'container) binary_searchable = { - length : 'container -> int; - get : 'container -> int -> 'elt; -} - -let create_binary_search (searchable : ('elt, 'container) binary_searchable) = - let binary_search ~f arr = - let arr_lo = 0 in - let arr_hi = searchable.length arr in - - let rec aux lo hi = - if Int.equal lo hi then Error lo - else - let mid = (lo + hi) / 2 in - match f mid (searchable.get arr mid) with - | Equal -> Ok (mid, searchable.get arr mid) - | Less -> aux lo mid - | Greater -> aux (mid + 1) hi - in - aux arr_lo arr_hi - in - binary_search - -let arr_searchable = { length = Array.length; get = Array.get } - -let bigarr1_searchable = - { length = Bigarray.Array1.dim; get = Bigarray.Array1.get } - -let binary_search_arr ~f x = create_binary_search arr_searchable ~f x -let binary_search_bigarr1 ~f x = create_binary_search bigarr1_searchable ~f x - -let to_comparison f x y = - let res = f x y in - if res < 0 then Less else if res > 0 then Greater else Equal - -let cmp target _i x = to_comparison Int.compare target x -let%test _ = binary_search_arr ~f:(cmp 1) [| 1; 2; 4; 5 |] =*= Ok (0, 1) -let%test _ = binary_search_arr ~f:(cmp 2) [| 1; 2; 4; 5 |] =*= Ok (1, 2) -let%test _ = binary_search_arr ~f:(cmp 5) [| 1; 2; 4; 5 |] =*= Ok (3, 5) - -(* out of bounds or not in the array returns the position it should be inserted at *) -let%test _ = binary_search_arr ~f:(cmp 6) [| 1; 2; 4; 5 |] =*= Error 4 -let%test _ = binary_search_arr ~f:(cmp 3) [| 1; 2; 4; 5 |] =*= Error 2 -let%test _ = binary_search_arr ~f:(cmp 0) [| 1; 2; 4; 5 |] =*= Error 0 +(* now in Ord.ml *) (*****************************************************************************) (* Debugging/logging *) diff --git a/libs/commons/Common.mli b/libs/commons/Common.mli index 76f246c43b34..f42f6c090ee9 100644 --- a/libs/commons/Common.mli +++ b/libs/commons/Common.mli @@ -62,25 +62,7 @@ val ( != ) : hidden_by_your_nanny (*****************************************************************************) (* Comparison *) (*****************************************************************************) - -type order = Less | Equal | Greater - -val binary_search_arr : - f:(int -> 'a -> order) -> 'a array -> (int * 'a, int) result -(** [binary_search_arr f A] returns Ok (idx, x) if the element x can be found - at idx x, according to comparison function f. - Otherwise, it returns Error idx, where idx is the index that the element - must be inserted at, if it were to be in the array. - For instance, when searching for 2 in [|0, 3|], we get Error 1. - Inserting at the beginning is Error 0, and at the end is Error 2. - *) - -val binary_search_bigarr1 : - f:(int -> 'a -> order) -> - ('a, 'b, 'c) Bigarray.Array1.t -> - (int * 'a, int) result - -val to_comparison : ('a -> 'a -> int) -> 'a -> 'a -> order +(* now in Ord.ml *) (*****************************************************************************) (* Composition/Control *) diff --git a/libs/commons/Ord.ml b/libs/commons/Ord.ml new file mode 100644 index 000000000000..362a1a21044f --- /dev/null +++ b/libs/commons/Ord.ml @@ -0,0 +1,54 @@ +type t = Less | Equal | Greater + +(* We use this to be able to factorize our code for binary search, by + instantiating our code against different kinds of containers and + element types. + In particular, this is an improvement over functorization, because the + type of Bigarray.Array1.t is actually triply-polymorphic. By making the + container type itself unspecified, we are able to abstract over even + multiply-polymorphic containers. +*) +type ('elt, 'container) binary_searchable = { + length : 'container -> int; + get : 'container -> int -> 'elt; +} + +let create_binary_search (searchable : ('elt, 'container) binary_searchable) = + let binary_search ~f arr = + let arr_lo = 0 in + let arr_hi = searchable.length arr in + + let rec aux lo hi = + if Int.equal lo hi then Error lo + else + let mid = (lo + hi) / 2 in + match f mid (searchable.get arr mid) with + | Equal -> Ok (mid, searchable.get arr mid) + | Less -> aux lo mid + | Greater -> aux (mid + 1) hi + in + aux arr_lo arr_hi + in + binary_search + +let arr_searchable = { length = Array.length; get = Array.get } + +let bigarr1_searchable = + { length = Bigarray.Array1.dim; get = Bigarray.Array1.get } + +let binary_search_arr ~f x = create_binary_search arr_searchable ~f x +let binary_search_bigarr1 ~f x = create_binary_search bigarr1_searchable ~f x + +let to_comparison f x y = + let res = f x y in + if res < 0 then Less else if res > 0 then Greater else Equal + +let cmp target _i x = to_comparison Int.compare target x +let%test _ = binary_search_arr ~f:(cmp 1) [| 1; 2; 4; 5 |] = Ok (0, 1) +let%test _ = binary_search_arr ~f:(cmp 2) [| 1; 2; 4; 5 |] = Ok (1, 2) +let%test _ = binary_search_arr ~f:(cmp 5) [| 1; 2; 4; 5 |] = Ok (3, 5) + +(* out of bounds or not in the array returns the position it should be inserted at *) +let%test _ = binary_search_arr ~f:(cmp 6) [| 1; 2; 4; 5 |] = Error 4 +let%test _ = binary_search_arr ~f:(cmp 3) [| 1; 2; 4; 5 |] = Error 2 +let%test _ = binary_search_arr ~f:(cmp 0) [| 1; 2; 4; 5 |] = Error 0 diff --git a/libs/commons/Ord.mli b/libs/commons/Ord.mli new file mode 100644 index 000000000000..26396e0b05af --- /dev/null +++ b/libs/commons/Ord.mli @@ -0,0 +1,15 @@ +type t = Less | Equal | Greater + +val binary_search_arr : f:(int -> 'a -> t) -> 'a array -> (int * 'a, int) result +(** [binary_search_arr f A] returns Ok (idx, x) if the element x can be found + at idx x, according to comparison function f. + Otherwise, it returns Error idx, where idx is the index that the element + must be inserted at, if it were to be in the array. + For instance, when searching for 2 in [|0, 3|], we get Error 1. + Inserting at the beginning is Error 0, and at the end is Error 2. + *) + +val binary_search_bigarr1 : + f:(int -> 'a -> t) -> ('a, 'b, 'c) Bigarray.Array1.t -> (int * 'a, int) result + +val to_comparison : ('a -> 'a -> int) -> 'a -> 'a -> t diff --git a/libs/commons2/common2.ml b/libs/commons2/common2.ml index 16c373ebb55a..72113105898b 100644 --- a/libs/commons2/common2.ml +++ b/libs/commons2/common2.ml @@ -1768,20 +1768,6 @@ let normalize_path (file : string) : string = let xs' = aux [] xs in (if is_rel then "" else "/") ^ join "/" xs' -(* -let relative_to_absolute s = - if Filename.is_relative s - then - begin - let old = USys.getcwd () in - Sys.chdir s; - let current = USys.getcwd () in - Sys.chdir old; - s - end - else s -*) - let relative_to_absolute s = if s = "." then USys.getcwd () else if Filename.is_relative s then USys.getcwd () ^ "/" ^ s diff --git a/libs/lib_parsing/Pos.ml b/libs/lib_parsing/Pos.ml index 0e9d1a556230..bffa76856c3c 100644 --- a/libs/lib_parsing/Pos.ml +++ b/libs/lib_parsing/Pos.ml @@ -139,13 +139,13 @@ let converters_of_arrays line_arr col_arr : bytepos_linecol_converters = let i = max 0 (min i (len - 1)) in (line_arr.{i}, col_arr.{i})); linecol_to_bytepos_fun = - (let cmp = Common.to_comparison Int.compare in + (let cmp = Ord.to_comparison Int.compare in (* This is the line/col we're trying to find the pos of. *) fun (line, col) -> let res = line_arr - |> Common.binary_search_bigarr1 ~f:(fun bytepos line' -> + |> Ord.binary_search_bigarr1 ~f:(fun bytepos line' -> let col' = col_arr.{bytepos} in (* We want the relationship of the varying line' with respect to the line we are trying to search for. @@ -153,9 +153,9 @@ let converters_of_arrays line_arr col_arr : bytepos_linecol_converters = should want to say Greater, because we want to go greater. *) match cmp line line' with - | Equal -> cmp col col' - | Less -> Less - | Greater -> Greater) + | Ord.Equal -> cmp col col' + | Ord.Less -> Ord.Less + | Ord.Greater -> Ord.Greater) in match res with | Error _idx -> raise Not_found