[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

@@ -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 (Some state) when Dom.is_false state -> Work.skip
-                | Some (Ok state) -> exec_jump stk state block return
+                | 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
+    Dom.exec_inst state inst |> Result.of_option ~error:(state, inst)
-    |> Result.map_error ~f:(fun () -> (state, inst))
 
   let exec_block :
       exec_opts -> Llair.t -> Stack.t -> Dom.t -> Llair.block -> Work.x =

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]
 

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
+    State_domain.exec_inst current inst >>| fun current -> (entry, current)
-    | Ok current -> Ok (entry, current)
-    | Error e -> Error e
 
   let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals
       =
-    match
+    State_domain.exec_intrinsic ~skip_throw current areturn intrinsic
-      State_domain.exec_intrinsic ~skip_throw current areturn intrinsic
+      actuals
-        actuals
+    |> function
-    with
+    | 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}

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_inst () _ = Some ()
-let exec_intrinsic ~skip_throw:_ _ _ _ _ : (t, unit) result option = None
+let exec_intrinsic ~skip_throw:_ _ _ _ _ : t option option = None
 
 type from_call = unit [@@deriving compare, equal, sexp]
 

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]

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
+  ( Solver.infer_frame pre xs foot
-  | Some frame ->
+  >>| fun frame ->
-      Ok
+  Sh.exists (Set.union zs xs)
-        (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))))
-  | None -> Error () )
   |>
-  [%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
+    Sh.t -> Var.t option -> Var.t -> Term.t list -> Sh.t option option =
-    -> Var.t option
-    -> Var.t
-    -> Term.t list
-    -> (Sh.t, unit) result 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

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 option
-val load :
+val store : Sh.t -> ptr:Term.t -> exp:Term.t -> len:Term.t -> Sh.t option
-  Sh.t -> reg:Var.var -> ptr:Term.t -> len:Term.t -> (Sh.t, unit) result
+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 store :
+val memmov : Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> Sh.t option
-  Sh.t -> ptr:Term.t -> exp:Term.t -> len:Term.t -> (Sh.t, unit) result
+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 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 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

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 =