[sledge] Move generation of formal return and throw parameters to frontend

Summary:
The generation of names for the function formal return and throw
parameters is not central to LLAIR, but a detail of the frontend,
since they are generated only because LLVM does not already have such
names.

Reviewed By: ngorogiannis

Differential Revision: D17665240

fbshipit-source-id: 684cbae92

sledge/src/llair/frontend.ml

@@ -1242,6 +1242,13 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
       (fun rev_args param -> xlate_name param :: rev_args)
       [] llf
   in
+  let freturn =
+    match name.typ with
+    | Pointer {elt= Function {return= Some _; _}} ->
+        Some (Var.program "freturn")
+    | _ -> None
+  in
+  let fthrow = Var.program "fthrow" in
   ( match Llvm.block_begin llf with
   | Before entry_blk ->
       let pop = pop_stack_frame_of_function llf entry_blk in
@@ -1263,10 +1270,10 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
         in
         trav_blocks (List.rev entry_blocks) entry_blk
       in
-      Llair.Func.mk ~name ~params ~entry ~cfg
+      Llair.Func.mk ~name ~params ~freturn ~fthrow ~entry ~cfg
   | At_end _ ->
       report_undefined llf name ;
-      Llair.Func.mk_undefined ~name ~params )
+      Llair.Func.mk_undefined ~name ~params ~freturn ~fthrow )
   |>
   [%Trace.retn fun {pf} -> pf "@\n%a" Llair.Func.pp]
 

sledge/src/llair/llair.ml

@@ -443,7 +443,7 @@ module Func = struct
 
   let find functions name = Map.find functions name
 
-  let mk ~(name : Global.t) ~params ~entry ~cfg =
+  let mk ~(name : Global.t) ~params ~freturn ~fthrow ~entry ~cfg =
     let locals =
       let locals_cmnd locals cmnd =
         Vector.fold_right ~f:Inst.union_locals cmnd ~init:locals
@@ -454,15 +454,6 @@ module Func = struct
       let init = locals_block Var.Set.empty entry in
       Vector.fold ~f:locals_block cfg ~init
     in
-    let wrt = Set.add_list params locals in
-    let freturn, wrt =
-      match name.typ with
-      | Pointer {elt= Function {return= Some _; _}} ->
-          let freturn, wrt = Var.fresh "freturn" ~wrt in
-          (Some freturn, wrt)
-      | _ -> (None, wrt)
-    in
-    let fthrow, _ = Var.fresh "fthrow" ~wrt in
     let func = {name; params; freturn; fthrow; locals; entry; cfg} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
@@ -484,12 +475,12 @@ module Func = struct
     Vector.iter cfg ~f:resolve_parent_and_jumps ;
     func |> check invariant
 
-  let mk_undefined ~name ~params =
+  let mk_undefined ~name ~params ~freturn ~fthrow =
     let entry =
       Block.mk ~lbl:"" ~cmnd:Vector.empty ~term:Term.unreachable
     in
     let cfg = Vector.empty in
-    mk ~name ~entry ~params ~cfg
+    mk ~name ~entry ~params ~freturn ~fthrow ~cfg
 end
 
 (** Derived meta-data *)

sledge/src/llair/llair.mli

@@ -185,11 +185,18 @@ module Func : sig
   val mk :
        name:Global.t
     -> params:Var.t list
+    -> freturn:Var.t option
+    -> fthrow:Var.t
     -> entry:block
     -> cfg:block vector
     -> func
 
-  val mk_undefined : name:Global.t -> params:Var.t list -> t
+  val mk_undefined :
+       name:Global.t
+    -> params:Var.t list
+    -> freturn:Var.t option
+    -> fthrow:Var.t
+    -> t
 
   val find : functions -> string -> func option
   (** Look up a function of the given name in the given functions. *)