From 0aebb07757cffb1279f6064d7608618339d00311 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2020 16:38:42 -0800
Subject: [PATCH] [sledge] Identify intrinsics using strings instead of
 variables

Reviewed By: jvillard

Differential Revision: D24886574

fbshipit-source-id: 70059713f
---
 sledge/src/domain_sh.ml |  4 ++--
 sledge/src/exec.ml      | 13 +++++++------
 sledge/src/exec.mli     |  2 +-
 3 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index d3618f0fe..452fa2f70 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -69,8 +69,8 @@ let exec_inst inst pre =
   |> Option.map ~f:simplify
 
 let exec_intrinsic ~skip_throw r i es q =
-  Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r) (X.func i)
-    (List.map ~f:X.term es)
+  Exec.intrinsic ~skip_throw q (Option.map ~f:X.reg r)
+    (Llair.Function.name i) (List.map ~f:X.term es)
   |> Option.map ~f:(Option.map ~f:simplify)
 
 let value_determined_by ctx us a =
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 80a08e462..9301bf3df 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -735,11 +735,12 @@ let nondet pre = function Some reg -> kill pre reg | None -> pre
 let abort _ = None
 
 let intrinsic ~skip_throw :
-    Sh.t -> Var.t option -> Var.t -> Term.t list -> Sh.t option option =
+    Sh.t -> Var.t option -> string -> Term.t list -> Sh.t option option =
  fun pre areturn intrinsic actuals ->
   let name =
-    let n = Var.name intrinsic in
-    match String.index n '.' with None -> n | Some i -> String.take i n
+    match String.index intrinsic '.' with
+    | None -> intrinsic
+    | Some i -> String.take i intrinsic
   in
   let skip pre = Some (Some pre) in
   ( match (areturn, name, actuals) with
@@ -820,7 +821,7 @@ let intrinsic ~skip_throw :
   | None -> ()
   | Some _ ->
       [%Trace.info
-        "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]"
+        "@[<2>exec intrinsic@ @[%a%s(@[%a@])@] from@ @[{ %a@ }@]@]"
           (Option.pp "%a := " Var.pp)
-          areturn Var.pp intrinsic (List.pp ",@ " Term.pp)
-          (List.rev actuals) Sh.pp pre]
+          areturn intrinsic (List.pp ",@ " Term.pp) (List.rev actuals) Sh.pp
+          pre]
diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli
index ff16c9ea5..578ad571b 100644
--- a/sledge/src/exec.mli
+++ b/sledge/src/exec.mli
@@ -26,6 +26,6 @@ val intrinsic :
      skip_throw:bool
   -> Sh.t
   -> Var.t option
-  -> Var.t
+  -> string
   -> Term.t list
   -> Sh.t option option