[sledge] Revise llvm to llair translation to avoid code duplication

Summary:
In some cases inlining pure expressions into their use sites causes
code blowup. This diff changes the frontend to inline expressions only
if there is a single use, and otherwise adds a move instruction.

Reviewed By: ngorogiannis

Differential Revision: D17071770

fbshipit-source-id: d866a0622

sledge/src/llair/frontend.ml

@@ -297,11 +297,21 @@ let xlate_name_opt : Llvm.llvalue -> Var.t option =
   | Void -> None
   | _ -> Some (xlate_name instr)
 
-let memo_value : (Llvm.llvalue, Exp.t) Hashtbl.t = Hashtbl.Poly.create ()
+let memo_value : (bool * Llvm.llvalue, Exp.t) Hashtbl.t =
+  Hashtbl.Poly.create ()
 
 let memo_global : (Llvm.llvalue, Global.t) Hashtbl.t =
   Hashtbl.Poly.create ()
 
+let should_inline : Llvm.llvalue -> bool =
+ fun llv ->
+  match Llvm.use_begin llv with
+  | Some use -> (
+    match Llvm.use_succ use with
+    | Some _ -> false (* do not inline if >= 2 uses *)
+    | None -> true )
+  | None -> true
+
 module Llvalue = struct
   type t = Llvm.llvalue
 
@@ -339,7 +349,7 @@ let rec xlate_intrinsic_exp : string -> (x -> Llvm.llvalue -> Exp.t) option
           xlate_llvm_eh_typeid_for x src arg )
   | _ -> None
 
-and xlate_value : x -> Llvm.llvalue -> Exp.t =
+and xlate_value ?(inline = false) : x -> Llvm.llvalue -> Exp.t =
  fun x llv ->
   let xlate_value_ llv =
     match Llvm.classify_value llv with
@@ -347,8 +357,8 @@ and xlate_value : x -> Llvm.llvalue -> Exp.t =
         let func = Llvm.operand llv (Llvm.num_arg_operands llv) in
         let fname = Llvm.value_name func in
         match xlate_intrinsic_exp fname with
-        | Some intrinsic -> intrinsic x llv
+        | Some intrinsic when inline || should_inline llv -> intrinsic x llv
-        | None -> Exp.var (xlate_name llv) )
+        | _ -> Exp.var (xlate_name llv) )
     | Instruction (Invoke | Alloca | Load | PHI | LandingPad | VAArg)
      |Argument ->
         Exp.var (xlate_name llv)
@@ -396,8 +406,9 @@ and xlate_value : x -> Llvm.llvalue -> Exp.t =
           | Add | FAdd | Sub | FSub | Mul | FMul | UDiv | SDiv | FDiv | URem
           | SRem | FRem | Shl | LShr | AShr | And | Or | Xor | ICmp | FCmp
           | Select | GetElementPtr | ExtractElement | InsertElement
-          | ExtractValue | InsertValue | ShuffleVector ) as opcode ) ->
+          | ShuffleVector | ExtractValue | InsertValue ) as opcode ) ->
-        xlate_opcode x llv opcode
+        if inline || should_inline llv then xlate_opcode x llv opcode
+        else Exp.var (xlate_name llv)
     | ConstantExpr -> xlate_opcode x llv (Llvm.constexpr_opcode llv)
     | GlobalIFunc -> todo "ifuncs: %a" pp_llvalue llv ()
     | Instruction (CatchPad | CleanupPad | CatchSwitch) ->
@@ -409,7 +420,7 @@ and xlate_value : x -> Llvm.llvalue -> Exp.t =
      |NullValue | BasicBlock | InlineAsm | MDNode | MDString ->
         fail "xlate_value: %a" pp_llvalue llv ()
   in
-  Hashtbl.find_or_add memo_value llv ~default:(fun () ->
+  Hashtbl.find_or_add memo_value (inline, llv) ~default:(fun () ->
       [%Trace.call fun {pf} -> pf "%a" pp_llvalue llv]
       ;
       xlate_value_ llv
@@ -780,6 +791,14 @@ let xlate_instr :
   in
   let name = find_name instr in
   let loc = find_loc instr in
+  let inline_or_move xlate =
+    if should_inline instr then nop ()
+    else
+      let reg = xlate_name instr in
+      let exp = xlate instr in
+      let reg_exps = Vector.of_array [|(reg, exp)|] in
+      emit_inst (Llair.Inst.move ~reg_exps ~loc)
+  in
   let opcode = Llvm.instr_opcode instr in
   match opcode with
   | Load ->
@@ -837,8 +856,10 @@ let xlate_instr :
         emit_inst (Llair.Inst.nondet ~reg ~msg:fname ~loc)
       in
       (* intrinsics *)
+      match xlate_intrinsic_exp fname with
+      | Some intrinsic -> inline_or_move (intrinsic x)
+      | None -> (
         match String.split fname ~on:'.' with
-      | _ when Option.is_some (xlate_intrinsic_exp fname) -> nop ()
         | ["__llair_throw"] ->
             let exc = xlate_value x (Llvm.operand instr 0) in
             emit_term ~prefix:(pop loc) (Llair.Term.throw ~exc ~loc)
@@ -892,7 +913,8 @@ let xlate_instr :
         (* unimplemented *)
         | ["llvm"; ("stacksave" | "stackrestore")] ->
             skip "dynamic stack deallocation"
-      | "llvm" :: "coro" :: _ -> todo "coroutines:@ %a" pp_llvalue instr ()
+        | "llvm" :: "coro" :: _ ->
+            todo "coroutines:@ %a" pp_llvalue instr ()
         | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ ->
             todo "statepoints:@ %a" pp_llvalue instr ()
         | ["llvm"; ("va_start" | "va_copy" | "va_end")] ->
@@ -915,11 +937,12 @@ let xlate_instr :
                     ( match Hash_set.strict_add ignored_callees fname with
                     | Ok () when not (Llvm.is_declaration llfunc) ->
                         warn
-                        "ignoring variable arguments to variadic function: \
+                          "ignoring variable arguments to variadic \
-                         %a"
+                           function: %a"
                           Exp.pp func ()
                     | _ -> () ) ;
-                  Array.length (Llvm.param_types (Llvm.element_type lltyp))
+                    Array.length
+                      (Llvm.param_types (Llvm.element_type lltyp))
                 in
                 List.rev_init num_args ~f:(fun i ->
                     xlate_value x (Llvm.operand instr i) )
@@ -931,7 +954,7 @@ let xlate_instr :
             in
             continue (fun (insts, term) ->
                 let cmnd = Vector.of_list insts in
-              ([], call, [Llair.Block.mk ~lbl ~cmnd ~term]) ) )
+                ([], call, [Llair.Block.mk ~lbl ~cmnd ~term]) ) ) )
   | Invoke -> (
       let llfunc = Llvm.operand instr (Llvm.num_operands instr - 3) in
       let lltyp = Llvm.type_of llfunc in
@@ -1162,7 +1185,7 @@ let xlate_instr :
    |Shl | LShr | AShr | And | Or | Xor | ICmp | FCmp | Select
    |GetElementPtr | ExtractElement | InsertElement | ShuffleVector
    |ExtractValue | InsertValue ->
-      nop ()
+      inline_or_move (xlate_value ~inline:true x)
   | VAArg ->
       let reg = xlate_name_opt instr in
       warn "variadic function argument: %a" Loc.pp loc () ;