[sledge] Add Exec.intrinsic for intrinsic instructions

Reviewed By: jvillard

Differential Revision: D25146167

fbshipit-source-id: 60c4e8476

sledge/src/domain_sh.ml

@@ -73,10 +73,8 @@ let exec_inst inst pre =
   | Abort _ -> Exec.abort pre
   | Intrinsic {reg; name; args; _} ->
       let areturn = Option.map ~f:X.reg reg in
-      let intrinsic = Llair.Intrinsic.to_string name in
       let actuals = IArray.map ~f:X.term args in
-      Exec.intrinsic_func ~skip_throw:true pre areturn intrinsic actuals
-      |> Option.get_lazy (fail "exec_inst: %a" Llair.Inst.pp inst) )
+      Exec.intrinsic ~skip_throw:true pre areturn name actuals )
   |> Option.map ~f:simplify
 
 let exec_intrinsic ~skip_throw r i es q =

sledge/src/exec.ml

@@ -737,6 +737,15 @@ let free pre ~ptr = exec_spec pre (free_spec ptr)
 let nondet pre = function Some reg -> kill pre reg | None -> pre
 let abort _ = None
 
+let intrinsic ~skip_throw:_ :
+       Sh.t
+    -> Var.t option
+    -> Llair.Intrinsic.t
+    -> Term.t iarray
+    -> Sh.t option =
+ fun pre _areturn intrinsic _actuals ->
+  match intrinsic with `nop -> Some pre
+
 let intrinsic_func ~skip_throw :
     Sh.t -> Var.t option -> string -> Term.t iarray -> Sh.t option option =
  fun pre areturn intrinsic actuals ->

sledge/src/exec.mli

@@ -22,6 +22,14 @@ val free : Sh.t -> ptr:Term.t -> Sh.t option
 val nondet : Sh.t -> Var.t option -> Sh.t
 val abort : Sh.t -> Sh.t option
 
+val intrinsic :
+     skip_throw:bool
+  -> Sh.t
+  -> Var.t option
+  -> Llair.Intrinsic.t
+  -> Term.t iarray
+  -> Sh.t option
+
 val intrinsic_func :
      skip_throw:bool
   -> Sh.t