From 074f668c0015e158765592d421b527ea8e642d07 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 2 Dec 2020 13:46:53 -0800
Subject: [PATCH] [sledge] Add Intrinsic instruction

Summary:
Currently intrinsics are treated as functions, with Call instructions
to possibly-undefined functions with known names. This diff adds an
Intrinsic instruction form to express these more directly and:

- avoid the overhead of intrinsics needing to end blocks

- avoid the overhead of the function call machiery

- avoid the complexity of doing the string name lookup to find their
  specs, repeatedly

This diff only adds the backend support, the added Intrinsic
instructions are not yet generated by the frontend.

Reviewed By: jvillard

Differential Revision: D25146155

fbshipit-source-id: f24024183
---
 sledge/cli/domain_itv.ml       |  2 ++
 sledge/dune                    |  4 ++--
 sledge/src/domain_sh.ml        |  8 +++++++-
 sledge/src/llair/intrinsics.ml | 10 +++++++++
 sledge/src/llair/llair.ml      | 37 +++++++++++++++++++++++++++++++---
 sledge/src/llair/llair.mli     | 19 +++++++++++++++++
 6 files changed, 74 insertions(+), 6 deletions(-)
 create mode 100644 sledge/src/llair/intrinsics.ml

diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml
index 332723172..cff530416 100644
--- a/sledge/cli/domain_itv.ml
+++ b/sledge/cli/domain_itv.ml
@@ -197,6 +197,8 @@ let exec_inst i q =
    |Alloc _ | Memset _ | Memcpy _ | Memmov _ | Free _ ->
       Some q
   | Abort _ -> None
+  | 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 =
diff --git a/sledge/dune b/sledge/dune
index 709c3b5c1..5dcd7472d 100644
--- a/sledge/dune
+++ b/sledge/dune
@@ -29,8 +29,8 @@
 (library
  (name ppx_sledge)
  (kind ppx_rewriter)
- (libraries ppx_compare ppx_expect ppx_hash ppx_here ppx_inline_test ppx_let
-   ppx_sexp_conv ppx_sexp_value)
+ (libraries ppx_compare ppx_enumerate ppx_expect ppx_hash ppx_here
+   ppx_inline_test ppx_let ppx_sexp_conv ppx_sexp_value ppx_variants_conv)
  (preprocess no_preprocessing))
 
 (subdir
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index c687772a4..864a56737 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -70,7 +70,13 @@ let exec_inst inst pre =
       Exec.alloc pre ~reg:(X.reg reg) ~num:(X.term num) ~len
   | Free {ptr; _} -> Exec.free pre ~ptr:(X.term ptr)
   | Nondet {reg; _} -> Some (Exec.nondet pre (Option.map ~f:X.reg reg))
-  | Abort _ -> Exec.abort 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 ~skip_throw:true pre areturn intrinsic actuals
+      |> Option.get_lazy (fail "exec_inst: %a" Llair.Inst.pp inst) )
   |> Option.map ~f:simplify
 
 let exec_intrinsic ~skip_throw r i es q =
diff --git a/sledge/src/llair/intrinsics.ml b/sledge/src/llair/intrinsics.ml
new file mode 100644
index 000000000..1775a891f
--- /dev/null
+++ b/sledge/src/llair/intrinsics.ml
@@ -0,0 +1,10 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Intrinsic instruction opcodes *)
+
+type t = [`nop] [@@deriving compare, equal, hash, sexp, enumerate, variants]
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index f549a1506..56b360b04 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -17,6 +17,24 @@ module Function = Function
 module Global = Global
 module GlobalDefn = GlobalDefn
 
+module Intrinsic = struct
+  include Intrinsics
+  module Intrinsic_to_String = Bijection.Make (Intrinsics) (String)
+
+  let t_to_name =
+    Iter.of_list all
+    |> Iter.map ~f:(fun i -> (i, Variants.to_name i))
+    |> Intrinsic_to_String.of_iter
+
+  let to_string i = Intrinsic_to_String.find_left i t_to_name
+
+  let of_name s =
+    try Some (Intrinsic_to_String.find_right s t_to_name)
+    with Not_found -> None
+
+  let pp ppf i = Format.pp_print_string ppf (to_string i)
+end
+
 type inst =
   | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t}
   | Load of {reg: Reg.t; ptr: Exp.t; len: Exp.t; loc: Loc.t}
@@ -28,6 +46,8 @@ type inst =
   | Free of {ptr: Exp.t; loc: Loc.t}
   | Nondet of {reg: Reg.t option; msg: string; loc: Loc.t}
   | Abort of {loc: Loc.t}
+  | Intrinsic of
+      {reg: Reg.t option; name: Intrinsic.t; args: Exp.t iarray; loc: Loc.t}
 [@@deriving compare, equal, hash, sexp]
 
 type cmnd = inst iarray [@@deriving compare, equal, hash, sexp]
@@ -258,6 +278,10 @@ let pp_inst fs inst =
         (Option.pp "%a := " Reg.pp)
         reg msg Loc.pp loc
   | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc
+  | Intrinsic {reg; name; args; loc} ->
+      pf "@[<2>%aintrinsic %a(%a);@]\t%a"
+        (Option.pp "%a := " Reg.pp)
+        reg Intrinsic.pp name (IArray.pp ",@ " Exp.pp) args Loc.pp loc
 
 let pp_actuals pp_actual fs actuals =
   Format.fprintf fs "@ (@[%a@])" (IArray.pp ",@ " pp_actual) actuals
@@ -352,6 +376,7 @@ module Inst = struct
   let free ~ptr ~loc = Free {ptr; loc}
   let nondet ~reg ~msg ~loc = Nondet {reg; msg; loc}
   let abort ~loc = Abort {loc}
+  let intrinsic ~reg ~name ~args ~loc = Intrinsic {reg; name; args; loc}
 
   let loc = function
     | Move {loc; _}
@@ -363,18 +388,23 @@ module Inst = struct
      |Alloc {loc; _}
      |Free {loc; _}
      |Nondet {loc; _}
-     |Abort {loc; _} ->
+     |Abort {loc; _}
+     |Intrinsic {loc; _} ->
         loc
 
   let union_locals inst vs =
     match inst with
     | Move {reg_exps; _} ->
         IArray.fold ~f:(fun (reg, _) vs -> Reg.Set.add reg vs) reg_exps vs
-    | Load {reg; _} | Alloc {reg; _} | Nondet {reg= Some reg; _} ->
+    | Load {reg; _}
+     |Alloc {reg; _}
+     |Nondet {reg= Some reg; _}
+     |Intrinsic {reg= Some reg; _} ->
         Reg.Set.add reg vs
     | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _
      |Nondet {reg= None; _}
-     |Abort _ ->
+     |Abort _
+     |Intrinsic {reg= None; _} ->
         vs
 
   let locals inst = union_locals inst Reg.Set.empty
@@ -392,6 +422,7 @@ module Inst = struct
     | Free {ptr; loc= _} -> f ptr s
     | Nondet {reg= _; msg= _; loc= _} -> s
     | Abort {loc= _} -> s
+    | Intrinsic {reg= _; name= _; args; loc= _} -> IArray.fold ~f args s
 end
 
 (** Jumps *)
diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli
index 7b54458b1..78886a877 100644
--- a/sledge/src/llair/llair.mli
+++ b/sledge/src/llair/llair.mli
@@ -16,6 +16,14 @@ module Function = Function
 module Global = Global
 module GlobalDefn = GlobalDefn
 
+module Intrinsic : sig
+  include module type of Intrinsics
+
+  val to_string : t -> string
+  val of_name : string -> t option
+  val pp : t pp
+end
+
 (** Instructions for memory manipulation or other non-control effects. *)
 type inst = private
   | Move of {reg_exps: (Reg.t * Exp.t) iarray; loc: Loc.t}
@@ -42,6 +50,9 @@ type inst = private
       (** Bind [reg] to an arbitrary value, representing non-deterministic
           approximation of behavior described by [msg]. *)
   | Abort of {loc: Loc.t}  (** Trigger abnormal program termination *)
+  | Intrinsic of
+      {reg: Reg.t option; name: Intrinsic.t; args: Exp.t iarray; loc: Loc.t}
+      (** Bind [reg] to the value of applying intrinsic [name] to [args]. *)
 
 (** A (straight-line) command is a sequence of instructions. *)
 type cmnd = inst iarray
@@ -122,6 +133,14 @@ module Inst : sig
   val free : ptr:Exp.t -> loc:Loc.t -> inst
   val nondet : reg:Reg.t option -> msg:string -> loc:Loc.t -> inst
   val abort : loc:Loc.t -> inst
+
+  val intrinsic :
+       reg:Reg.t option
+    -> name:Intrinsic.t
+    -> args:Exp.t iarray
+    -> loc:Loc.t
+    -> t
+
   val loc : inst -> Loc.t
   val locals : inst -> Reg.Set.t
   val fold_exps : inst -> 's -> f:(Exp.t -> 's -> 's) -> 's