From c9449cce778b2594f1a8ae74cb97fb89ae69ceeb Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 28 Nov 2019 12:41:52 -0800 Subject: [PATCH] [sledge] Some simplifications using let+ Reviewed By: jvillard Differential Revision: D18738850 fbshipit-source-id: dc3477fe7 --- sledge/src/control.ml | 4 +-- sledge/src/domain/itv.ml | 21 ++++++++-------- sledge/src/domain/relation.ml | 42 +++++++++++++++---------------- sledge/src/symbheap/exec.ml | 47 +++++++++++++++++------------------ sledge/src/symbheap/solver.ml | 47 ++++++++++++++++++----------------- 5 files changed, 79 insertions(+), 82 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 5273fce5c..af1e06546 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -271,8 +271,8 @@ module Make (Dom : Domain_sig.Dom) = struct else let maybe_summary_post = let state = fst (domain_call ~summaries:false state) in - Hashtbl.find summary_table name.reg - >>= List.find_map ~f:(Dom.apply_summary state) + let* summary = Hashtbl.find summary_table name.reg in + List.find_map ~f:(Dom.apply_summary state) summary in [%Trace.info "Maybe summary post: %a" (Option.pp "%a" Dom.pp) diff --git a/sledge/src/domain/itv.ml b/sledge/src/domain/itv.ml index 739eb5dde..1e8e4d718 100644 --- a/sledge/src/domain/itv.ml +++ b/sledge/src/domain/itv.ml @@ -8,7 +8,6 @@ (** Interval abstract domain *) open Apron -open Option.Let_syntax let equal_apron_typ = (* Apron.Texpr1.typ is a sum of nullary constructors *) @@ -77,7 +76,7 @@ let rec pow base typ = function let rec texpr_of_nary_term subtms typ q op = assert (Qset.length subtms >= 2) ; let term_to_texpr (tm, coeff) = - let%bind base = apron_texpr_of_llair_term tm q typ in + let* base = apron_texpr_of_llair_term tm q typ in match op with | Texpr1.Add -> Some @@ -91,8 +90,8 @@ let rec texpr_of_nary_term subtms typ q op = match Qset.to_list subtms with | hd :: tl -> List.fold tl ~init:(term_to_texpr hd) ~f:(fun acc curr -> - let%bind c = term_to_texpr curr in - let%map a = acc in + let* c = term_to_texpr curr in + let+ a = acc in Texpr1.Binop (op, c, a, typ, Texpr0.Rnd) ) | _ -> assert false @@ -115,21 +114,21 @@ and apron_texpr_of_llair_term tm q typ = let subtm = apron_texpr_of_llair_term t q src in if equal_apron_typ src dst then subtm else - let%bind t = subtm in - Some (Texpr1.Unop (Texpr1.Cast, t, dst, Texpr0.Rnd)) ) + let+ t = subtm in + Texpr1.Unop (Texpr1.Cast, t, dst, Texpr0.Rnd) ) (* extraction to unsigned 1-bit int is llvm encoding of C boolean; restrict to [0,1] *) | Ap1 (Unsigned {bits= 1}, _t) -> Some (Texpr1.Cst (Coeff.i_of_int 0 1)) (* "t xor true" and "true xor t" are negation *) | Ap2 (Xor, t, Integer {data}) when Z.is_true data -> - let%map t = apron_texpr_of_llair_term t q typ in + let+ t = apron_texpr_of_llair_term t q typ in Texpr1.Unop (Texpr1.Neg, t, typ, Texpr0.Rnd) | Ap2 (Xor, Integer {data}, t) when Z.is_true data -> - let%map t = apron_texpr_of_llair_term t q typ in + let+ t = apron_texpr_of_llair_term t q typ in Texpr1.Unop (Texpr1.Neg, t, typ, Texpr0.Rnd) (* query apron for abstract evaluation of binary operations*) | Ap2 (op, t1, t2) -> - let%bind f = + let* f = match op with | Rem -> Some (mk_arith_binop typ Texpr0.Mod) | Div -> Some (mk_arith_binop typ Texpr0.Div) @@ -139,8 +138,8 @@ and apron_texpr_of_llair_term tm q typ = | Le -> Some (Fn.flip (mk_bool_binop typ q Tcons0.SUPEQ)) | _ -> None in - let%bind te1 = apron_texpr_of_llair_term t1 q typ in - let%map te2 = apron_texpr_of_llair_term t2 q typ in + let* te1 = apron_texpr_of_llair_term t1 q typ in + let+ te2 = apron_texpr_of_llair_term t2 q typ in f te1 te2 | x -> [%Trace.info diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml index 662230e9d..a73aa0177 100644 --- a/sledge/src/domain/relation.ml +++ b/sledge/src/domain/relation.ml @@ -32,17 +32,16 @@ module Make (State_domain : State_domain_sig) = struct let init globals = embed (State_domain.init globals) let join (entry_a, current_a) (entry_b, current_b) = - if State_domain.equal entry_b entry_a then - State_domain.join current_a current_b - >>= fun curr -> Some (entry_a, curr) + if State_domain.equal entry_a entry_b then + let+ next = State_domain.join current_a current_b in + (entry_a, next) else None let is_false (_, curr) = State_domain.is_false curr let exec_assume (entry, current) cnd = - match State_domain.exec_assume current cnd with - | Some current -> Some (entry, current) - | None -> None + let+ next = State_domain.exec_assume current cnd in + (entry, next) let exec_kill (entry, current) reg = (entry, State_domain.exec_kill current reg) @@ -51,16 +50,17 @@ module Make (State_domain : State_domain_sig) = struct (entry, State_domain.exec_move current reg_exps) let exec_inst (entry, current) inst = - State_domain.exec_inst current inst >>| fun current -> (entry, current) + let+ next = State_domain.exec_inst current inst in + (entry, next) let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals = - State_domain.exec_intrinsic ~skip_throw current areturn intrinsic - actuals - |> function - | Some (Some current) -> Some (Some (entry, current)) - | Some None -> Some None - | None -> None + let+ next_opt = + State_domain.exec_intrinsic ~skip_throw current areturn intrinsic + actuals + in + let+ next = next_opt in + (entry, next) type from_call = {state_from_call: State_domain.from_call; caller_entry: State_domain.t} @@ -105,22 +105,20 @@ module Make (State_domain : State_domain_sig) = struct List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current) let resolve_callee f e (entry, current) = - let callees, current = State_domain.resolve_callee f e current in - (callees, (entry, current)) + let callees, next = State_domain.resolve_callee f e current in + (callees, (entry, next)) type summary = State_domain.summary let pp_summary = State_domain.pp_summary let create_summary ~locals ~formals (entry, current) = - let fs, current = + let fs, next = State_domain.create_summary ~locals ~formals ~entry ~current in - (fs, (entry, current)) + (fs, (entry, next)) - let apply_summary rel summ = - let entry, current = rel in - Option.map - ~f:(fun c -> (entry, c)) - (State_domain.apply_summary current summ) + let apply_summary (entry, current) summ = + let+ next = State_domain.apply_summary current summ in + (entry, next) end diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index e619e7430..c3f9e529b 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -635,31 +635,30 @@ let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) = (* execute a command with given spec from pre *) let exec_spec pre0 {xs; foot; sub; ms; post} = - [%Trace.call fun {pf} -> - pf "@[%a@]@ @[<2>%a@,@[{%a %a}@;<1 -1>%a--@ {%a }@]@]" Sh.pp pre0 - (Sh.pp_us ~pre:"@<2>∀ ") - xs Sh.pp foot - (fun fs sub -> - if not (Var.Subst.is_empty sub) then - Format.fprintf fs "∧ %a" Var.Subst.pp sub ) - sub - (fun fs ms -> - if not (Set.is_empty ms) then - Format.fprintf fs "%a := " Var.Set.pp ms ) - ms Sh.pp post ; - assert ( - let vs = Set.diff (Set.diff foot.us xs) pre0.us in - Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ; - assert ( - let vs = Set.diff (Set.diff post.us xs) pre0.us in - Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )] + ([%Trace.call fun {pf} -> + pf "@[%a@]@ @[<2>%a@,@[{%a %a}@;<1 -1>%a--@ {%a }@]@]" Sh.pp pre0 + (Sh.pp_us ~pre:"@<2>∀ ") + xs Sh.pp foot + (fun fs sub -> + if not (Var.Subst.is_empty sub) then + Format.fprintf fs "∧ %a" Var.Subst.pp sub ) + sub + (fun fs ms -> + if not (Set.is_empty ms) then + Format.fprintf fs "%a := " Var.Set.pp ms ) + ms Sh.pp post ; + assert ( + let vs = Set.diff (Set.diff foot.us xs) pre0.us in + Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ; + assert ( + let vs = Set.diff (Set.diff post.us xs) pre0.us in + Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )] ; let foot = Sh.extend_us xs foot in let zs, pre = Sh.bind_exists pre0 ~wrt:xs in - ( Solver.infer_frame pre xs foot - >>| fun frame -> + let+ frame = Solver.infer_frame pre xs foot in Sh.exists (Set.union zs xs) - (Sh.star post (Sh.exists ms (Sh.rename sub frame))) ) + (Sh.star post (Sh.exists ms (Sh.rename sub frame)))) |> [%Trace.retn fun {pf} r -> pf "%a" (Option.pp "%a" Sh.pp) r ; @@ -671,9 +670,9 @@ let rec exec_specs pre = function | ({xs; foot; _} as spec) :: specs -> let foot = Sh.extend_us xs foot in let pre_pure = Sh.star (Sh.exists xs (Sh.pure_approx foot)) pre in - exec_spec pre_pure spec - >>= fun post -> - exec_specs pre specs >>| fun posts -> Sh.or_ post posts + let* post = exec_spec pre_pure spec in + let+ posts = exec_specs pre specs in + Sh.or_ post posts | [] -> Some (Sh.false_ pre.us) let exec_specs pre specs = diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index 71d789c1c..1d26c295f 100644 --- a/sledge/src/symbheap/solver.ml +++ b/sledge/src/symbheap/solver.ml @@ -85,9 +85,11 @@ let excise_term ({us; min; xs} as goal) pure term = let excise_pure ({sub} as goal) = [%Trace.info "@[<2>excise_pure@ %a@]" pp goal] ; - List.fold_option sub.pure ~init:(goal, []) ~f:(fun (goal, pure) term -> - excise_term goal pure term ) - >>| fun (goal, pure) -> {goal with sub= Sh.with_pure pure sub} + let+ goal, pure = + List.fold_option sub.pure ~init:(goal, []) ~f:(fun (goal, pure) term -> + excise_term goal pure term ) + in + {goal with sub= Sh.with_pure pure sub} (* [k; o) * ⊢ [l; n) @@ -496,8 +498,7 @@ let excise_seg ({sub} as goal) msg ssg = (Sh.pp_seg_norm sub.cong) ssg] ; let {Sh.loc= k; bas= b; len= m; siz= o} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in - Equality.difference sub.cong k l - >>= fun k_l -> + let* k_l = Equality.difference sub.cong k l in if (not (Equality.entails_eq sub.cong b b')) || not (Equality.entails_eq sub.cong m m') @@ -511,13 +512,11 @@ let excise_seg ({sub} as goal) msg ssg = | -1 -> ( let ko = Term.add k o in let ln = Term.add l n in - Equality.difference sub.cong ko ln - >>= fun ko_ln -> + let* ko_ln = Equality.difference sub.cong ko ln in match[@warning "-p"] Z.sign ko_ln with (* k+o-(l+n) < 0 so k+o < l+n *) | -1 -> ( - Equality.difference sub.cong l ko - >>= fun l_ko -> + let* l_ko = Equality.difference sub.cong l ko in match[@warning "-p"] Z.sign l_ko with (* l-(k+o) < 0 [k; o) * so l < k+o ⊢ [l; n) *) @@ -551,8 +550,7 @@ let excise_seg ({sub} as goal) msg ssg = | 1 -> ( let ko = Term.add k o in let ln = Term.add l n in - Equality.difference sub.cong ko ln - >>= fun ko_ln -> + let* ko_ln = Equality.difference sub.cong ko ln in match[@warning "-p"] Z.sign ko_ln with (* k+o-(l+n) < 0 [k; o) * so k+o < l+n ⊢ [l; n) *) @@ -562,8 +560,7 @@ let excise_seg ({sub} as goal) msg ssg = | 0 -> Some (excise_seg_min_suffix goal msg ssg k_l) (* k+o-(l+n) > 0 so k+o > l+n *) | 1 -> ( - Equality.difference sub.cong k ln - >>= fun k_ln -> + let* k_ln = Equality.difference sub.cong k ln in match[@warning "-p"] Z.sign k_ln with (* k-(l+n) < 0 [k; o) * so k < l+n ⊢ [l; n) *) @@ -601,16 +598,20 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option = let ys, min = Sh.bind_exists minuend ~wrt:xs in let us = min.us in let com = Sh.emp in - List.find_map dnf_subtrahend ~f:(fun sub -> - [%Trace.info "@[<2>subtrahend@ %a@]" Sh.pp sub] ; - let sub = Sh.extend_us us sub in - let ws, sub = Sh.bind_exists sub ~wrt:xs in - let xs = Set.union xs ws in - let sub = Sh.and_cong min.cong sub in - let zs = Var.Set.empty in - excise {us; com; min; xs; sub; zs; pgs= true} - >>| fun remainder -> Sh.exists (Set.union ys ws) remainder ) - >>| fun remainder -> Sh.or_ remainders remainder ) + let+ remainder = + List.find_map dnf_subtrahend ~f:(fun sub -> + [%Trace.info "@[<2>subtrahend@ %a@]" Sh.pp sub] ; + let sub = Sh.extend_us us sub in + let ws, sub = Sh.bind_exists sub ~wrt:xs in + let xs = Set.union xs ws in + let sub = Sh.and_cong min.cong sub in + let zs = Var.Set.empty in + let+ remainder = + excise {us; com; min; xs; sub; zs; pgs= true} + in + Sh.exists (Set.union ys ws) remainder ) + in + Sh.or_ remainders remainder ) let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option = fun minuend xs subtrahend ->