From 409b21ec649b16d5b802ab8354a0a30bb211eefb Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 20 Oct 2020 11:42:02 -0700 Subject: [PATCH] [sledge] Switch from Base.Option to Containers.Option Reviewed By: ngorogiannis Differential Revision: D24306079 fbshipit-source-id: e42b45cfa --- sledge/cli/domain_itv.ml | 2 +- sledge/cli/frontend.ml | 8 ++++---- sledge/cli/sledge_buck.ml | 2 +- sledge/cli/version.ml | 2 +- sledge/nonstdlib/NS.ml | 2 +- sledge/nonstdlib/NS.mli | 2 +- sledge/nonstdlib/hashTable.ml | 2 +- sledge/nonstdlib/list.ml | 4 ++-- sledge/nonstdlib/map.ml | 6 +++--- sledge/nonstdlib/option.ml | 25 ++++++++++--------------- sledge/nonstdlib/option.mli | 22 ++++++++++------------ sledge/nonstdlib/set.ml | 5 ++--- sledge/src/domain_sh.ml | 2 +- sledge/src/exec.ml | 2 +- sledge/src/llair/loc.ml | 2 +- sledge/src/ses/equality.ml | 6 +++--- 16 files changed, 43 insertions(+), 51 deletions(-) diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml index d01b0844d..caef8639b 100644 --- a/sledge/cli/domain_itv.ml +++ b/sledge/cli/domain_itv.ml @@ -223,7 +223,7 @@ let exec_intrinsic ~skip_throw:_ pre aret i _ = ; "__cxa_allocate_exception" ; "_ZN5folly13usingJEMallocEv" ] ~f:(String.equal name) - then Option.map ~f:(Option.some << exec_kill pre) aret + then Option.map ~f:(Option.return << exec_kill pre) aret else None type from_call = {areturn: Llair.Reg.t option; caller_q: t} diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml index c674d3956..89c53bd8e 100644 --- a/sledge/cli/frontend.ml +++ b/sledge/cli/frontend.ml @@ -43,7 +43,7 @@ exception Invalid_llvm of string let invalid_llvm : string -> 'a = fun msg -> let first_line = - Option.value_map ~default:msg + Option.map_or ~default:msg ~f:(fun i -> String.take i msg) (String.index msg '\n') in @@ -554,7 +554,7 @@ and xlate_opcode stk : |FPExt | PtrToInt | IntToPtr | BitCast | AddrSpaceCast -> convert opcode | ICmp -> ( - match Option.value_exn (Llvm.icmp_predicate llv) with + match Option.get_exn (Llvm.icmp_predicate llv) with | Eq -> binary Exp.eq | Ne -> binary Exp.dq | Sgt -> binary Exp.gt @@ -1187,7 +1187,7 @@ let xlate_instr : in emit_term ~prefix:(pop loc @ pre) (Term.return ~exp ~loc) | Br -> ( - match Option.value_exn (Llvm.get_branch instr) with + match Option.get_exn (Llvm.get_branch instr) with | `Unconditional blk -> let prefix, dst, blocks = xlate_jump x instr blk loc [] in emit_term ~prefix (Term.goto ~dst ~loc) ~blocks @@ -1567,7 +1567,7 @@ let translate ~models ~fuzzer ~internalize : string list -> Llair.program = let link_model_file name = Llvm_linker.link_in link_ctx (Llvm_irreader.parse_ir llcontext - (Llvm.MemoryBuffer.of_string (Option.value_exn (Model.read name)))) + (Llvm.MemoryBuffer.of_string (Option.get_exn (Model.read name)))) in if models then link_model_file "/cxxabi.bc" ; if fuzzer then link_model_file "/lib_fuzzer_main.bc" ; diff --git a/sledge/cli/sledge_buck.ml b/sledge/cli/sledge_buck.ml index e4808b2e3..cdfc60295 100644 --- a/sledge/cli/sledge_buck.ml +++ b/sledge/cli/sledge_buck.ml @@ -150,7 +150,7 @@ let llvm_link_opt ~fuzzer ~bitcode_output modules = let open Process in eval ~context ( ( if fuzzer then - echo ~n:() (Option.value_exn (Model.read "/lib_fuzzer_main.bc")) + echo ~n:() (Option.get_exn (Model.read "/lib_fuzzer_main.bc")) else return () ) |- run (Lazy.force llvm_bin ^ "llvm-link") ("-o=-" :: modules) |- run diff --git a/sledge/cli/version.ml b/sledge/cli/version.ml index 3782af8ad..242c9d679 100644 --- a/sledge/cli/version.ml +++ b/sledge/cli/version.ml @@ -17,7 +17,7 @@ let debug = module Build_info = Build_info.V1 let version_to_string v = - Option.value_map ~f:Build_info.Version.to_string v ~default:"dev" + Option.map_or ~f:Build_info.Version.to_string v ~default:"dev" let version = Format.sprintf "%s%s" diff --git a/sledge/nonstdlib/NS.ml b/sledge/nonstdlib/NS.ml index 88c647667..ffaba1610 100644 --- a/sledge/nonstdlib/NS.ml +++ b/sledge/nonstdlib/NS.ml @@ -20,7 +20,7 @@ module Map = Map module Monad = Monad module Multiset = Multiset module Option = Option -include Option.Import +include Option.Infix module Q = Q_ext module Set = Set module Sign = Sign diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli index e91369c53..1591ce195 100644 --- a/sledge/nonstdlib/NS.mli +++ b/sledge/nonstdlib/NS.mli @@ -130,7 +130,7 @@ include module type of Iter.Import type ('a, 'b) continue_or_stop = Continue of 'a | Stop of 'b module Option = Option -include module type of Option.Import +include module type of Option.Infix module Either : sig type ('a, 'b) t = Left of 'a | Right of 'b diff --git a/sledge/nonstdlib/hashTable.ml b/sledge/nonstdlib/hashTable.ml index 1a1d68202..2f838b702 100644 --- a/sledge/nonstdlib/hashTable.ml +++ b/sledge/nonstdlib/hashTable.ml @@ -34,7 +34,7 @@ module Make (Key : HashedType) = struct | Some v -> found := Some v ; Some v ) ; - Option.value_exn !found + Option.get_exn !found let iteri tbl ~f = iter (fun key data -> f ~key ~data) tbl diff --git a/sledge/nonstdlib/list.ml b/sledge/nonstdlib/list.ml index 7f7fcdad1..d6a147c21 100644 --- a/sledge/nonstdlib/list.ml +++ b/sledge/nonstdlib/list.ml @@ -13,12 +13,12 @@ exception Not_found_s = Base.Sexp.Not_found_s let rec pp ?pre ?suf sep pp_elt fs = function | [] -> () | x :: xs -> - Option.iter pre ~f:(Format.fprintf fs) ; + Option.iter ~f:(Format.fprintf fs) pre ; pp_elt fs x ; ( match xs with | [] -> () | xs -> Format.fprintf fs "%( %)%a" sep (pp sep pp_elt) xs ) ; - Option.iter suf ~f:(Format.fprintf fs) + Option.iter ~f:(Format.fprintf fs) suf let findi x xs = let rec findi_ i xs = diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml index 990754569..c85ba7963 100644 --- a/sledge/nonstdlib/map.ml +++ b/sledge/nonstdlib/map.ml @@ -105,7 +105,7 @@ end) : S with type key = Key.t = struct let length = M.cardinal let choose_key = root_key let choose = root_binding - let choose_exn m = CCOpt.get_exn (choose m) + let choose_exn m = Option.get_exn (choose m) let min_binding = M.min_binding_opt let mem m k = M.mem k m let find_exn m k = M.find k m @@ -141,10 +141,10 @@ end) : S with type key = Key.t = struct in Option.map ~f:(fun v -> (v, m)) !found - let pop m = choose m |> CCOpt.map (fun (k, v) -> (k, v, remove m k)) + let pop m = choose m |> Option.map ~f:(fun (k, v) -> (k, v, remove m k)) let pop_min_binding m = - min_binding m |> CCOpt.map (fun (k, v) -> (k, v, remove m k)) + min_binding m |> Option.map ~f:(fun (k, v) -> (k, v, remove m k)) let change m key ~f = M.update key f m let update m k ~f = M.update k (fun v -> Some (f v)) m diff --git a/sledge/nonstdlib/option.ml b/sledge/nonstdlib/option.ml index 1fa93acc5..a319c519d 100644 --- a/sledge/nonstdlib/option.ml +++ b/sledge/nonstdlib/option.ml @@ -6,23 +6,18 @@ *) open! NS0 -include Base.Option +include Containers.Option + +type 'a t = 'a option [@@deriving compare, equal, hash, sexp] let pp fmt pp_elt fs = function | Some x -> Format.fprintf fs fmt pp_elt x | None -> () -let or_else ~f = function None -> f () | o -> o -let cons xo xs = match xo with Some x -> x :: xs | None -> xs - -module Monad_syntax = struct - let ( let+ ) x f = map ~f x - let ( and+ ) x y = both x y - let ( let* ) x f = bind ~f x - let ( and* ) x y = both x y -end - -module Import = struct - include Monad_infix - include Monad_syntax -end +let map xo ~f = map f xo +let map_or xo ~default ~f = map_or ~default f xo +let bind xo ~f = bind xo f +let iter xo ~f = iter f xo +let exists xo ~f = exists f xo +let for_all xo ~f = for_all f xo +let fold xo ~init ~f = fold f init xo diff --git a/sledge/nonstdlib/option.mli b/sledge/nonstdlib/option.mli index caf9d8c8c..92cb6838c 100644 --- a/sledge/nonstdlib/option.mli +++ b/sledge/nonstdlib/option.mli @@ -6,17 +6,15 @@ *) open! NS0 -include module type of Base.Option +include module type of Containers.Option -val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> 'a option pp -(** Pretty-print an option. *) - -val or_else : f:(unit -> 'a option) -> 'a option -> 'a option -(** [or_else ~f] is [f ()] on [None] and otherwise identity *) +type 'a t = 'a option [@@deriving compare, equal, hash, sexp] -val cons : 'a t -> 'a list -> 'a list - -module Import : sig - include Monad_syntax with type 'a t := 'a option - include module type of Monad_infix -end +val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> 'a option pp +val map : 'a t -> f:('a -> 'b) -> 'b t +val map_or : 'a t -> default:'b -> f:('a -> 'b) -> 'b +val bind : 'a t -> f:('a -> 'b t) -> 'b t +val iter : 'a t -> f:('a -> unit) -> unit +val exists : 'a t -> f:('a -> bool) -> bool +val for_all : 'a t -> f:('a -> bool) -> bool +val fold : 'a t -> init:'s -> f:('s -> 'a -> 's) -> 's diff --git a/sledge/nonstdlib/set.ml b/sledge/nonstdlib/set.ml index 9261637b8..7c9d94550 100644 --- a/sledge/nonstdlib/set.ml +++ b/sledge/nonstdlib/set.ml @@ -6,7 +6,6 @@ *) open! NS0 -module Option = CCOpt include Set_intf module Make (Elt : sig @@ -29,10 +28,10 @@ end) : S with type elt = Elt.t = struct let empty = S.empty let of_ = S.singleton - let of_option xo = Option.map_or S.singleton xo ~default:empty + let of_option xo = Option.map_or ~f:S.singleton xo ~default:empty let of_list = S.of_list let add s x = S.add x s - let add_option xo s = Option.fold add s xo + let add_option xo s = Option.fold ~f:add ~init:s xo let add_list xs s = S.add_list s xs let diff = S.diff let inter = S.inter diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 9c2f8db99..234438462 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -126,7 +126,7 @@ let localize_entry globals actuals formals freturn locals shadow pre entry = let foot = Sh.exists formals_set function_summary_pre in let xs, foot = Sh.bind_exists ~wrt:pre.Sh.us foot in let frame = - try Option.value_exn (Solver.infer_frame pre xs foot) + try Option.get_exn (Solver.infer_frame pre xs foot) with _ -> fail "Solver couldn't infer frame of a garbage-collected pre" () in diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index a5e47b368..d96ae5e70 100644 --- a/sledge/src/exec.ml +++ b/sledge/src/exec.ml @@ -630,7 +630,7 @@ let strlen_spec reg ptr = * Symbolic Execution *) -open Option.Import +open Option.Infix let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) = let gain_us = Var.Set.diff q1.us q0.us in diff --git a/sledge/src/llair/loc.ml b/sledge/src/llair/loc.ml index 3245b4a39..35647bec1 100644 --- a/sledge/src/llair/loc.ml +++ b/sledge/src/llair/loc.ml @@ -22,7 +22,7 @@ let pp fs ({dir; file; line; col} as loc) = if not (equal loc none) then Format.pp_print_string fs "; " ; if not (String.is_empty dir) then ( let dir = - Option.value_map ~f:Fpath.to_string + Option.map_or ~f:Fpath.to_string (Fpath.relativize ~root:(Fpath.v !root) (Fpath.v dir)) ~default:dir in diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml index f12eb5edf..73226ac3b 100644 --- a/sledge/src/ses/equality.ml +++ b/sledge/src/ses/equality.ml @@ -320,7 +320,7 @@ and solve_ ?f d e s = let solve ?f ~us ~xs d e = [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp d Term.pp e] ; - (solve_ ?f d e (us, xs, Subst.empty) >>| fun (_, xs, s) -> (xs, s)) + (solve_ ?f d e (us, xs, Subst.empty) >|= fun (_, xs, s) -> (xs, s)) |> [%Trace.retn fun {pf} -> function @@ -443,8 +443,8 @@ let invariant r = let true_ = let rep = Subst.empty in - let rep = Option.value_exn (Subst.extend Term.true_ rep) in - let rep = Option.value_exn (Subst.extend Term.false_ rep) in + let rep = Option.get_exn (Subst.extend Term.true_ rep) in + let rep = Option.get_exn (Subst.extend Term.false_ rep) in {xs= Var.Set.empty; sat= true; rep} |> check invariant let false_ = {true_ with sat= false}