[sledge] Remove support for intrinsic functions

Summary: No longer needed.

Reviewed By: jvillard

Differential Revision: D25146153

fbshipit-source-id: d5d7a969d

sledge/cli/domain_itv.ml

@@ -200,18 +200,6 @@ let exec_inst i q =
   | Intrinsic {reg= Some reg; _} -> Some (exec_kill reg q)
   | Intrinsic {reg= None; _} -> Some q
 
-(** Treat any intrinsic function as havoc on the return register [aret] *)
-let exec_intrinsic ~skip_throw:_ aret i _ pre =
-  let name = Llair.Function.name i in
-  if
-    List.exists
-      ["__cxa_allocate_exception"; "_ZN5folly13usingJEMallocEv"]
-      ~f:(String.equal name)
-  then
-    let+ aret = aret in
-    Some (exec_kill aret pre)
-  else None
-
 type from_call = {areturn: Llair.Reg.t option; caller_q: t}
 [@@deriving sexp_of]
 

sledge/src/control.ml

@@ -425,7 +425,7 @@ module Make (Dom : Domain_intf.Dom) = struct
             with
             | Some state -> exec_jump stk state block jump |> Work.seq x
             | None -> x )
-    | Call ({callee; actuals; areturn; return} as call) -> (
+    | Call ({callee; areturn; return} as call) -> (
         let lookup name =
           Option.to_list (Llair.Func.find name pgm.functions)
         in
@@ -434,23 +434,12 @@ module Make (Dom : Domain_intf.Dom) = struct
         | [] -> exec_skip_func stk state block areturn return
         | callees ->
             List.fold callees Work.skip ~f:(fun callee x ->
-                ( match
+                ( if Llair.Func.is_undefined callee then
-                    Dom.exec_intrinsic ~skip_throw:opts.skip_throw areturn
+                  exec_skip_func stk state block areturn return
-                      callee.name actuals state
+                else
-                  with
+                  exec_call opts stk state block {call with callee}
-                | Some None ->
+                    (Domain_used_globals.by_function opts.globals
-                    Report.invalid_access_term
+                       callee.name) )
-                      (Dom.report_fmt_thunk state)
-                      block.term ;
-                    Work.skip
-                | 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 ->
-                    exec_call opts stk state block {call with callee}
-                      (Domain_used_globals.by_function opts.globals
-                         callee.name) )
                 |> Work.seq x ) )
     | Return {exp} -> exec_return ~opts stk state block exp
     | Throw {exc} ->

sledge/src/domain_intf.ml

@@ -20,14 +20,6 @@ module type Dom = sig
   val exec_move : (Llair.Reg.t * Llair.Exp.t) iarray -> t -> t
   val exec_inst : Llair.inst -> t -> t option
 
-  val exec_intrinsic :
-       skip_throw:bool
-    -> Llair.Reg.t option
-    -> Llair.Function.t
-    -> Llair.Exp.t iarray
-    -> t
-    -> t option option
-
   type from_call [@@deriving sexp_of]
 
   val call :

sledge/src/domain_relation.ml

@@ -55,15 +55,6 @@ module Make (State_domain : State_domain_sig) = struct
     let+ next = State_domain.exec_inst inst current in
     (entry, next)
 
-  let exec_intrinsic ~skip_throw areturn intrinsic actuals (entry, current)
-      =
-    let+ next_opt =
-      State_domain.exec_intrinsic ~skip_throw areturn intrinsic actuals
-        current
-    in
-    let+ next = next_opt in
-    (entry, next)
-
   type from_call =
     {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
   [@@deriving sexp_of]

sledge/src/domain_sh.ml

@@ -77,11 +77,6 @@ let exec_inst inst pre =
       Exec.intrinsic ~skip_throw:true pre areturn name actuals )
   |> Option.map ~f:simplify
 
-let exec_intrinsic ~skip_throw r i es q =
-  Exec.intrinsic_func ~skip_throw q (Option.map ~f:X.reg r)
-    (Llair.Function.name i) (IArray.map ~f:X.term es)
-  |> Option.map ~f:(Option.map ~f:simplify)
-
 let value_determined_by ctx us a =
   List.exists (Context.class_of ctx a) ~f:(fun b ->
       Term.Set.subset (Term.Set.of_iter (Term.atoms b)) ~of_:us )

sledge/src/domain_unit.ml

@@ -18,7 +18,6 @@ let exec_assume () _ = Some ()
 let exec_kill _ () = ()
 let exec_move _ () = ()
 let exec_inst _ () = Some ()
-let exec_intrinsic ~skip_throw:_ _ _ _ _ : t option option = None
 
 type from_call = unit [@@deriving compare, equal, sexp]
 

sledge/src/domain_used_globals.ml

@@ -45,15 +45,6 @@ let exec_inst inst st =
   [%Trace.retn fun {pf} ->
     Option.iter ~f:(fun uses -> pf "post:{%a}" pp uses)]
 
-let exec_intrinsic ~skip_throw:_ _ intrinsic actuals st =
-  let name = Llair.Function.name intrinsic in
-  if
-    List.exists
-      ["__cxa_allocate_exception"; "_ZN5folly13usingJEMallocEv"]
-      ~f:(String.equal name)
-  then IArray.fold ~f:used_globals actuals st |> fun res -> Some (Some res)
-  else None
-
 type from_call = t [@@deriving sexp]
 
 (* Set abstract state to bottom (i.e. empty set) at function entry *)

sledge/src/exec.ml

@@ -827,20 +827,3 @@ let intrinsic ~skip_throw :
         (Option.pp "%a := " Var.pp)
         areturn Llair.Intrinsic.pp intrinsic (IArray.pp "@ " Term.pp)
         actuals ()
-
-let intrinsic_func ~skip_throw:_ :
-    Sh.t -> Var.t option -> string -> Term.t iarray -> Sh.t option option =
- fun pre areturn intrinsic actuals ->
-  let name =
-    match String.index intrinsic '.' with
-    | None -> intrinsic
-    | Some i -> String.take i intrinsic
-  in
-  (match (areturn, name, IArray.to_array actuals) with _ -> None)
-  $> function
-  | None -> ()
-  | Some _ ->
-      [%Trace.info
-        "@[<2>exec intrinsic@ @[%a%s(@[%a@])@] from@ @[{ %a@ }@]@]"
-          (Option.pp "%a := " Var.pp)
-          areturn intrinsic (IArray.pp ",@ " Term.pp) actuals Sh.pp pre]

sledge/src/exec.mli

@@ -29,11 +29,3 @@ val intrinsic :
   -> Llair.Intrinsic.t
   -> Term.t iarray
   -> Sh.t option
-
-val intrinsic_func :
-     skip_throw:bool
-  -> Sh.t
-  -> Var.t option
-  -> string
-  -> Term.t iarray
-  -> Sh.t option option