From 6f84787b191d78f4b8d3a10b58ad31d6688a3bd7 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 10 Oct 2019 06:16:47 -0700 Subject: [PATCH] [sledge] Change exec_inst to return an option instead of a result Summary: The `(t, unit) result` type is no more informative than `t option` and less convenient. Reviewed By: bennostein Differential Revision: D17665244 fbshipit-source-id: fa969d8b7 --- sledge/src/control.ml | 9 ++++----- sledge/src/domain/domain_sig.ml | 4 ++-- sledge/src/domain/relation.ml | 15 ++++++--------- sledge/src/domain/unit.ml | 4 ++-- sledge/src/domain/used_globals.ml | 6 +++--- sledge/src/symbheap/exec.ml | 27 ++++++++++----------------- sledge/src/symbheap/exec.mli | 31 +++++++++---------------------- sledge/src/symbheap/sh_domain.ml | 4 ++-- 8 files changed, 38 insertions(+), 62 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 9d3513a34..143f4c692 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -443,13 +443,13 @@ module Make (Dom : Domain_sig.Dom) = struct Dom.exec_intrinsic ~skip_throw:opts.skip_throw state areturn callee.name.reg args with - | Some (Error ()) -> + | Some None -> Report.invalid_access_term (Dom.report_fmt_thunk state) block.term ; Work.skip - | Some (Ok state) when Dom.is_false state -> Work.skip - | Some (Ok state) -> exec_jump stk state block return + | Some (Some state) when Dom.is_false state -> Work.skip + | Some (Some state) -> exec_jump stk state block return | None when Llair.Func.is_undefined callee -> exec_skip_func stk state block areturn return | None -> @@ -465,8 +465,7 @@ module Make (Dom : Domain_sig.Dom) = struct let exec_inst : Dom.t -> Llair.inst -> (Dom.t, Dom.t * Llair.inst) result = fun state inst -> - Dom.exec_inst state inst - |> Result.map_error ~f:(fun () -> (state, inst)) + Dom.exec_inst state inst |> Result.of_option ~error:(state, inst) let exec_block : exec_opts -> Llair.t -> Stack.t -> Dom.t -> Llair.block -> Work.x = diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml index 186522ab1..4482e4510 100644 --- a/sledge/src/domain/domain_sig.ml +++ b/sledge/src/domain/domain_sig.ml @@ -17,7 +17,7 @@ module type Dom = sig val exec_assume : t -> Exp.t -> t option val exec_kill : t -> Reg.t -> t val exec_move : t -> (Reg.t * Exp.t) vector -> t - val exec_inst : t -> Llair.inst -> (t, unit) result + val exec_inst : t -> Llair.inst -> t option val exec_intrinsic : skip_throw:bool @@ -25,7 +25,7 @@ module type Dom = sig -> Reg.t option -> Reg.t -> Exp.t list - -> (t, unit) result option + -> t option option type from_call [@@deriving sexp_of] diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml index 57a15b1d5..143623f82 100644 --- a/sledge/src/domain/relation.ml +++ b/sledge/src/domain/relation.ml @@ -51,19 +51,16 @@ module Make (State_domain : State_domain_sig) = struct (entry, State_domain.exec_move current reg_exps) let exec_inst (entry, current) inst = - match State_domain.exec_inst current inst with - | Ok current -> Ok (entry, current) - | Error e -> Error e + State_domain.exec_inst current inst >>| fun current -> (entry, current) let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals = - match - State_domain.exec_intrinsic ~skip_throw current areturn intrinsic - actuals - with + State_domain.exec_intrinsic ~skip_throw current areturn intrinsic + actuals + |> function + | Some (Some current) -> Some (Some (entry, current)) + | Some None -> Some None | None -> None - | Some (Ok current) -> Some (Ok (entry, current)) - | Some (Error e) -> Some (Error e) type from_call = {state_from_call: State_domain.from_call; caller_entry: State_domain.t} diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml index e4a45a6c6..94e614930 100644 --- a/sledge/src/domain/unit.ml +++ b/sledge/src/domain/unit.ml @@ -17,8 +17,8 @@ let is_false _ = false let exec_assume () _ = Some () let exec_kill () _ = () let exec_move () _ = () -let exec_inst () _ = Ok () -let exec_intrinsic ~skip_throw:_ _ _ _ _ : (t, unit) result option = None +let exec_inst () _ = Some () +let exec_intrinsic ~skip_throw:_ _ _ _ _ : t option option = None type from_call = unit [@@deriving compare, equal, sexp] diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml index 3b6c4d997..8fa7c0aa8 100644 --- a/sledge/src/domain/used_globals.ml +++ b/sledge/src/domain/used_globals.ml @@ -38,12 +38,12 @@ let exec_move st reg_exps = let exec_inst st inst = [%Trace.call fun {pf} -> pf "pre:{%a} %a" pp st Llair.Inst.pp inst] ; - Ok + Some (Llair.Inst.fold_exps inst ~init:st ~f:(fun acc e -> used_globals ~init:acc e )) |> [%Trace.retn fun {pf} -> - Result.iter ~f:(fun uses -> pf "post:{%a}" pp uses)] + Option.iter ~f:(fun uses -> pf "post:{%a}" pp uses)] let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals = let name = Reg.name intrinsic in @@ -57,7 +57,7 @@ let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals = ~f:(String.equal name) then List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a) - |> fun res -> Some (Ok res) + |> fun res -> Some (Some res) else None type from_call = t [@@deriving sexp_of] diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index ee7656956..3cc70f6a1 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -669,25 +669,22 @@ let exec_spec pre {xs; foot; sub; ms; post} = ; let foot = Sh.extend_us xs foot in let zs, pre = Sh.bind_exists pre ~wrt:xs in - ( match Solver.infer_frame pre xs foot with - | Some frame -> - Ok - (Sh.exists (Set.union zs xs) - (Sh.star post (Sh.exists ms (Sh.rename sub frame)))) - | None -> Error () ) + ( Solver.infer_frame pre xs foot + >>| fun frame -> + Sh.exists (Set.union zs xs) + (Sh.star post (Sh.exists ms (Sh.rename sub frame))) ) |> - [%Trace.retn fun {pf} r -> pf "%a" (Result.pp "%a" Sh.pp) r] + [%Trace.retn fun {pf} r -> pf "%a" (Option.pp "%a" Sh.pp) r] (* execute a multiple-spec command, where the disjunction of the specs preconditions are known to be tautologous *) let rec exec_specs pre = function | ({xs; foot; _} as spec) :: specs -> - let open Result.Monad_infix 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 - | [] -> Ok (Sh.false_ pre.us) + | [] -> Some (Sh.false_ pre.us) (* * Exposed interface @@ -701,7 +698,7 @@ let kill pre reg = Sh.exists (Set.add Var.Set.empty reg) pre let move pre reg_exps = exec_spec pre (move_spec pre.us reg_exps) - |> function Ok post -> post | _ -> assert false + |> function Some post -> post | _ -> fail "Exec.move failed" let load pre ~reg ~ptr ~len = exec_spec pre (load_spec pre.us reg ptr len) let store pre ~ptr ~exp ~len = exec_spec pre (store_spec pre.us ptr exp len) @@ -718,14 +715,10 @@ let memmov pre ~dst ~src ~len = let alloc pre ~reg ~num ~len = exec_spec pre (alloc_spec pre.us reg num len) let free pre ~ptr = exec_spec pre (free_spec pre.us ptr) let nondet pre = function Some reg -> kill pre reg | None -> pre -let abort _ = Error () +let abort _ = None let intrinsic ~skip_throw : - Sh.t - -> Var.t option - -> Var.t - -> Term.t list - -> (Sh.t, unit) result option = + Sh.t -> Var.t option -> Var.t -> Term.t list -> Sh.t option option = fun pre areturn intrinsic actuals -> [%Trace.info "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]" @@ -737,7 +730,7 @@ let intrinsic ~skip_throw : let n = Var.name intrinsic in match String.index n '.' with None -> n | Some i -> String.prefix n i in - let skip pre = Some (Ok pre) in + let skip pre = Some (Some pre) in match (areturn, name, actuals) with (* * cstdlib - memory management diff --git a/sledge/src/symbheap/exec.mli b/sledge/src/symbheap/exec.mli index d108ac679..03dea716c 100644 --- a/sledge/src/symbheap/exec.mli +++ b/sledge/src/symbheap/exec.mli @@ -10,28 +10,15 @@ val assume : Sh.t -> Term.t -> Sh.t option val kill : Sh.t -> Var.t -> Sh.t val move : Sh.t -> (Var.t * Term.t) vector -> Sh.t - -val load : - Sh.t -> reg:Var.var -> ptr:Term.t -> len:Term.t -> (Sh.t, unit) result - -val store : - Sh.t -> ptr:Term.t -> exp:Term.t -> len:Term.t -> (Sh.t, unit) result - -val memset : - Sh.t -> dst:Term.t -> byt:Term.t -> len:Term.t -> (Sh.t, unit) result - -val memcpy : - Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> (Sh.t, unit) result - -val memmov : - Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> (Sh.t, unit) result - -val alloc : - Sh.t -> reg:Var.var -> num:Term.t -> len:Term.t -> (Sh.t, unit) result - -val free : Sh.t -> ptr:Term.t -> (Sh.t, unit) result +val load : Sh.t -> reg:Var.var -> ptr:Term.t -> len:Term.t -> Sh.t option +val store : Sh.t -> ptr:Term.t -> exp:Term.t -> len:Term.t -> Sh.t option +val memset : Sh.t -> dst:Term.t -> byt:Term.t -> len:Term.t -> Sh.t option +val memcpy : Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> Sh.t option +val memmov : Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> Sh.t option +val alloc : Sh.t -> reg:Var.var -> num:Term.t -> len:Term.t -> Sh.t option +val free : Sh.t -> ptr:Term.t -> Sh.t option val nondet : Sh.t -> Var.var sexp_option -> Sh.t -val abort : Sh.t -> (Sh.t, unit) result +val abort : Sh.t -> Sh.t option val intrinsic : skip_throw:bool @@ -39,4 +26,4 @@ val intrinsic : -> Var.t option -> Var.t -> Term.t list - -> (Sh.t, unit) result option + -> Sh.t option option diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml index 4c3c9e0e5..56aeb4a6e 100644 --- a/sledge/src/symbheap/sh_domain.ml +++ b/sledge/src/symbheap/sh_domain.ml @@ -40,7 +40,7 @@ let exec_inst pre inst = assert (Set.disjoint (Sh.fv pre) (Reg.Set.vars (Llair.Inst.locals inst))) ; match inst with | Move {reg_exps; _} -> - Ok + Some (Exec.move pre (Vector.map reg_exps ~f:(fun (r, e) -> (Reg.var r, Exp.term e)))) | Load {reg; ptr; len; _} -> @@ -62,7 +62,7 @@ let exec_inst pre inst = Exec.alloc pre ~reg:(Reg.var reg) ~num:(Exp.term num) ~len:(Exp.term len) | Free {ptr; _} -> Exec.free pre ~ptr:(Exp.term ptr) - | Nondet {reg; _} -> Ok (Exec.nondet pre (Option.map ~f:Reg.var reg)) + | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:Reg.var reg)) | Abort _ -> Exec.abort pre let exec_intrinsic ~skip_throw q r i es =