diff --git a/sledge/src/domain/itv.ml b/sledge/src/domain/itv.ml index 1e8e4d718..a4cfe10d7 100644 --- a/sledge/src/domain/itv.ml +++ b/sledge/src/domain/itv.ml @@ -171,8 +171,9 @@ let assign reg exp q = ; let lval = apron_var_of_reg reg in ( match - apron_typ_of_llair_typ (Reg.typ reg) - >>= apron_texpr_of_llair_term (Exp.term exp) q + Option.bind + ~f:(apron_texpr_of_llair_term (Exp.term exp) q) + (apron_typ_of_llair_typ (Reg.typ reg)) with | Some e -> let env = Abstract1.env q in @@ -195,8 +196,9 @@ let assign reg exp q = (** block if [e] is known to be false; skip otherwise *) let exec_assume q e = match - apron_typ_of_llair_typ (Exp.typ e) - >>= apron_texpr_of_llair_term (Exp.term e) q + Option.bind + ~f:(apron_texpr_of_llair_term (Exp.term e) q) + (apron_typ_of_llair_typ (Exp.typ e)) with | Some e -> let cond = @@ -247,7 +249,7 @@ let exec_intrinsic ~skip_throw:_ pre aret i _ = ; "mallctlbymib"; "malloc_stats_print"; "strlen" ; "__cxa_allocate_exception"; "_ZN5folly13usingJEMallocEv" ] ~f:(String.equal name) - then aret >>| (exec_kill pre >> Option.some) + then Option.map ~f:(Option.some << exec_kill pre) aret else None type from_call = {areturn: Reg.t option; caller_q: t} [@@deriving sexp_of] diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml index 8562841bb..f72ebdb84 100644 --- a/sledge/src/import/import.ml +++ b/sledge/src/import/import.ml @@ -40,6 +40,7 @@ let trd3 (_, _, z) = z (** Function combinators *) let ( >> ) f g x = g (f x) +let ( << ) f g x = f (g x) let ( $ ) f g x = f x ; g x let ( $> ) x f = f x ; x let ( <$ ) f x = f x ; x diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli index 9a483dce5..adaff7758 100644 --- a/sledge/src/import/import.mli +++ b/sledge/src/import/import.mli @@ -47,17 +47,21 @@ val ( >> ) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c (** Composition of functions: [(f >> g) x] is exactly equivalent to [g (f (x))]. Left associative. *) +val ( << ) : ('b -> 'c) -> ('a -> 'b) -> 'a -> 'c +(** Reverse composition of functions: [(g << f) x] is exactly equivalent to + [g (f (x))]. Left associative. *) + val ( $ ) : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b (** Sequential composition of functions: [(f $ g) x] is exactly equivalent to [(f x) ; (g x)]. Left associative. *) val ( $> ) : 'a -> ('a -> unit) -> 'a -(** Apply and ignore function: [x $> f] is exactly equivalent to [f x ; x]. - Left associative. *) +(** Reverse apply and ignore function: [x $> f] is exactly equivalent to [f + x ; x]. Left associative. *) val ( <$ ) : ('a -> unit) -> 'a -> 'a -(** Reverse apply and ignore function: [f <$ x] is exactly equivalent to [f - x ; x]. Left associative. *) +(** Apply and ignore function: [f <$ x] is exactly equivalent to [f x ; x]. + Left associative. *) (** Pretty-printing *) diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index d3bd8b162..0845b1184 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -642,9 +642,10 @@ and xlate_opcode : x -> Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = (ptr_idx x ~ptr ~idx ~llelt, llelt) | Struct -> let fld = - Option.bind ~f:Int64.to_int - (Llvm.int64_of_const (Llvm.operand llv i)) - |> function + match + Option.bind ~f:Int64.to_int + (Llvm.int64_of_const (Llvm.operand llv i)) + with | Some n -> n | None -> fail "xlate_opcode: %i %a" i pp_llvalue llv () in diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index b053a91e9..e42cf6930 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -547,7 +547,8 @@ let set_derived_metadata functions = | Iswitch {tbl; _} -> Vector.iter tbl ~f:jump | Call ({callee; return; throw; _} as call) -> ( match - Reg.of_exp callee >>| Reg.name >>= Func.find functions + Option.bind ~f:(Func.find functions) + (Option.map ~f:Reg.name (Reg.of_exp callee)) with | Some func -> if Set.mem ancestors func.entry then call.recursive <- true diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml index 473b8c75d..ccf33d65b 100644 --- a/sledge/src/symbheap/sh_domain.ml +++ b/sledge/src/symbheap/sh_domain.ml @@ -283,8 +283,7 @@ let apply_summary q ({xs; foot; post} as fs) = if Set.is_empty xs_in_fv_q then Solver.infer_frame q xs foot else None in [%Trace.info "frame %a" (Option.pp "%a" pp) frame] ; - Option.map ~f:(Sh.star post) frame - |> Option.map ~f:(Sh.extend_us add_back) + Option.map ~f:(Sh.extend_us add_back) (Option.map ~f:(Sh.star post) frame) |> [%Trace.retn fun {pf} r -> match r with None -> pf "None" | Some q -> pf "@,%a" pp q]