From 1fddf1a5d0843e74fe6a1d590fb7a450e5d875a4 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 2 Dec 2020 13:47:49 -0800
Subject: [PATCH] [sledge] Add Exec.intrinsic for intrinsic instructions

Reviewed By: jvillard

Differential Revision: D25146167

fbshipit-source-id: 60c4e8476
---
 sledge/src/domain_sh.ml | 4 +---
 sledge/src/exec.ml      | 9 +++++++++
 sledge/src/exec.mli     | 8 ++++++++
 3 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 340795f80..7d14c16cb 100644
--- a/sledge/src/domain_sh.ml
+++ b/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 =
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 28e486af0..6ddf326cb 100644
--- a/sledge/src/exec.ml
+++ b/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 ->
diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli
index ec3e15dd9..64ba94eec 100644
--- a/sledge/src/exec.mli
+++ b/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