[sledge][NFC] Rename params to formals

Summary: For consistency

Reviewed By: ngorogiannis

Differential Revision: D17801926

fbshipit-source-id: 012b13561

sledge/src/control.ml

@@ -38,7 +38,7 @@ module Make (Dom : Domain_sig.Dom) = struct
       | Return of
           { recursive: bool  (** return from a possibly-recursive call *)
           ; dst: Llair.Jump.t
-          ; params: Reg.t list
+          ; formals: Reg.t list
           ; locals: Reg.Set.t
           ; from_call: Dom.from_call
           ; stk: t }
@@ -95,9 +95,9 @@ module Make (Dom : Domain_sig.Dom) = struct
 
     let empty = Empty |> check invariant
 
-    let push_return Llair.{callee= {params; locals}; return; recursive}
+    let push_return Llair.{callee= {formals; locals}; return; recursive}
         from_call stk =
-      Return {recursive; dst= return; params; locals; from_call; stk}
+      Return {recursive; dst= return; formals; locals; from_call; stk}
       |> check invariant
 
     let push_throw jmp stk =
@@ -128,8 +128,8 @@ module Make (Dom : Domain_sig.Dom) = struct
 
     let pop_throw stk ~init ~unwind =
       let rec pop_throw_ state = function
-        | Return {params; locals; from_call; stk} ->
-            pop_throw_ (unwind params locals from_call state) stk
+        | Return {formals; locals; from_call; stk} ->
+            pop_throw_ (unwind formals locals from_call state) stk
         | Throw (dst, Return {from_call; stk}) ->
             Some (from_call, dst, stk, state)
         | Empty -> None
@@ -272,7 +272,7 @@ module Make (Dom : Domain_sig.Dom) = struct
 
   let exec_call opts stk state block call globals =
     let Llair.{callee; args= actuals; areturn; return; recursive} = call in
-    let Llair.{name; params= formals; freturn; locals; entry} = callee in
+    let Llair.{name; formals; freturn; locals; entry} = callee in
     [%Trace.call fun {pf} ->
       pf "%a from %a with state %a" Reg.pp name.reg Reg.pp
         return.dst.parent.name.reg Dom.pp state]
@@ -325,7 +325,7 @@ module Make (Dom : Domain_sig.Dom) = struct
                 data ) )]
 
   let exec_return ~opts stk pre_state (block : Llair.block) exp =
-    let Llair.{name; params; freturn; locals} = block.parent in
+    let Llair.{name; formals; freturn; locals} = block.parent in
     [%Trace.call fun {pf} ->
       pf "from %a with pre_state %a" Reg.pp name.reg Dom.pp pre_state]
     ;
@@ -334,7 +334,7 @@ module Make (Dom : Domain_sig.Dom) = struct
         let globals = used_globals opts name.reg in
         let function_summary, post_state =
           Dom.create_summary ~locals post_state
-            ~formals:(Set.union (Reg.Set.of_list params) globals)
+            ~formals:(Set.union (Reg.Set.of_list formals) globals)
         in
         Hashtbl.add_multi summary_table ~key:name.reg ~data:function_summary ;
         pp_st () ;
@@ -351,7 +351,7 @@ module Make (Dom : Domain_sig.Dom) = struct
     ( match Stack.pop_return stk with
     | Some (from_call, retn_site, stk) ->
         let post_state = summarize (Dom.post locals from_call exit_state) in
-        let retn_state = Dom.retn params freturn from_call post_state in
+        let retn_state = Dom.retn formals freturn from_call post_state in
         exec_jump stk retn_state block retn_site
     | None ->
         (* Create and store a function summary for main *)
@@ -369,8 +369,8 @@ module Make (Dom : Domain_sig.Dom) = struct
     let func = block.parent in
     [%Trace.call fun {pf} -> pf "from %a" Reg.pp func.name.reg]
     ;
-    let unwind params scope from_call state =
-      Dom.retn params (Some func.fthrow) from_call
+    let unwind formals scope from_call state =
+      Dom.retn formals (Some func.fthrow) from_call
         (Dom.post scope from_call state)
     in
     ( match Stack.pop_throw stk ~unwind ~init:pre_state with
@@ -381,7 +381,7 @@ module Make (Dom : Domain_sig.Dom) = struct
         in
         let post_state = Dom.post func.locals from_call exit_state in
         let retn_state =
-          Dom.retn func.params func.freturn from_call post_state
+          Dom.retn func.formals func.freturn from_call post_state
         in
         exec_jump stk retn_state block retn_site
     | None -> Work.skip )
@@ -482,7 +482,7 @@ module Make (Dom : Domain_sig.Dom) = struct
     let entry_points = Config.find_list "entry-points" in
     List.find_map ~f:(Llair.Func.find pgm.functions) entry_points
     |> function
-    | Some {name= {reg}; locals; params= []; entry} ->
+    | Some {name= {reg}; locals; formals= []; entry} ->
         Some
           (Work.init
              (fst

sledge/src/llair/frontend.ml

@@ -1293,7 +1293,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
   [%Trace.call fun {pf} -> pf "%a" pp_llvalue llf]
   ;
   let name = xlate_global x llf in
-  let params =
+  let formals =
     Llvm.fold_left_params
       (fun rev_args param -> xlate_name x param :: rev_args)
       [] llf
@@ -1327,10 +1327,10 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
         in
         trav_blocks (List.rev entry_blocks) entry_blk
       in
-      Llair.Func.mk ~name ~params ~freturn ~fthrow ~entry ~cfg
+      Llair.Func.mk ~name ~formals ~freturn ~fthrow ~entry ~cfg
   | At_end _ ->
       report_undefined llf name ;
-      Llair.Func.mk_undefined ~name ~params ~freturn ~fthrow )
+      Llair.Func.mk_undefined ~name ~formals ~freturn ~fthrow )
   |>
   [%Trace.retn fun {pf} -> pf "@\n%a" Llair.Func.pp]
 

sledge/src/llair/llair.ml

@@ -57,7 +57,7 @@ and cfg = block vector
 (* [entry] is not part of [cfg] since it cannot be jumped to, only called. *)
 and func =
   { name: Global.t
-  ; params: Reg.t list
+  ; formals: Reg.t list
   ; freturn: Reg.t option
   ; fthrow: Reg.t
   ; locals: Reg.Set.t
@@ -107,10 +107,10 @@ let sexp_of_block {lbl; cmnd; term; parent; sort_index} =
 
 let sexp_of_cfg v = [%sexp_of: block vector] v
 
-let sexp_of_func {name; params; freturn; fthrow; locals; entry; cfg} =
+let sexp_of_func {name; formals; freturn; fthrow; locals; entry; cfg} =
   [%sexp
     { name: Global.t
-    ; params: Reg.t list
+    ; formals: Reg.t list
     ; freturn: Reg.t option
     ; fthrow: Reg.t
     ; locals: Reg.Set.t
@@ -161,7 +161,7 @@ let pp_inst fs inst =
 let pp_args pp_arg fs args =
   Format.fprintf fs "@ (@[%a@])" (List.pp ",@ " pp_arg) (List.rev args)
 
-let pp_param fs reg = Reg.pp fs reg
+let pp_formal fs reg = Reg.pp fs reg
 
 let pp_jump fs {dst; retreating} =
   Format.fprintf fs "@[<2>%s%%%s@]"
@@ -221,7 +221,7 @@ let rec dummy_block =
 and dummy_func =
   let dummy_reg = Reg.program ~global:() Typ.ptr "dummy" in
   { name= Global.mk dummy_reg Typ.ptr Loc.none
-  ; params= []
+  ; formals= []
   ; freturn= None
   ; fthrow= dummy_reg
   ; locals= Reg.Set.empty
@@ -395,7 +395,7 @@ module Func = struct
 
   let pp fs
       ( { name
-        ; params
+        ; formals
         ; freturn
         ; fthrow= _
         ; locals= _
@@ -408,7 +408,7 @@ module Func = struct
       | Pointer {elt= Function {return; _}} -> return
       | _ -> None )
       (Option.pp " %a := " Reg.pp)
-      freturn Global.pp name (pp_args pp_param) params
+      freturn Global.pp name (pp_args pp_formal) formals
       (fun fs ->
         if is_undefined func then Format.fprintf fs " #%i@]" sort_index
         else
@@ -442,7 +442,7 @@ module Func = struct
 
   let find functions name = Map.find functions name
 
-  let mk ~(name : Global.t) ~params ~freturn ~fthrow ~entry ~cfg =
+  let mk ~(name : Global.t) ~formals ~freturn ~fthrow ~entry ~cfg =
     let locals =
       let locals_cmnd locals cmnd =
         Vector.fold_right ~f:Inst.union_locals cmnd ~init:locals
@@ -453,7 +453,7 @@ module Func = struct
       let init = locals_block Reg.Set.empty entry in
       Vector.fold ~f:locals_block cfg ~init
     in
-    let func = {name; params; freturn; fthrow; locals; entry; cfg} in
+    let func = {name; formals; freturn; fthrow; locals; entry; cfg} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
       let lookup cfg lbl : block =
@@ -474,12 +474,12 @@ module Func = struct
     Vector.iter cfg ~f:resolve_parent_and_jumps ;
     func |> check invariant
 
-  let mk_undefined ~name ~params ~freturn ~fthrow =
+  let mk_undefined ~name ~formals ~freturn ~fthrow =
     let entry =
       Block.mk ~lbl:"" ~cmnd:Vector.empty ~term:Term.unreachable
     in
     let cfg = Vector.empty in
-    mk ~name ~entry ~params ~freturn ~fthrow ~cfg
+    mk ~name ~entry ~formals ~freturn ~fthrow ~cfg
 end
 
 (** Derived meta-data *)

sledge/src/llair/llair.mli

@@ -89,7 +89,7 @@ and cfg
     parameters are the function parameters. *)
 and func = private
   { name: Global.t
-  ; params: Reg.t list  (** Formal parameters, first-param-last stack *)
+  ; formals: Reg.t list  (** Formal parameters, first-param-last stack *)
   ; freturn: Reg.t option
   ; fthrow: Reg.t
   ; locals: Reg.Set.t  (** Local registers *)
@@ -184,7 +184,7 @@ module Func : sig
 
   val mk :
        name:Global.t
-    -> params:Reg.t list
+    -> formals:Reg.t list
     -> freturn:Reg.t option
     -> fthrow:Reg.t
     -> entry:block
@@ -193,7 +193,7 @@ module Func : sig
 
   val mk_undefined :
        name:Global.t
-    -> params:Reg.t list
+    -> formals:Reg.t list
     -> freturn:Reg.t option
     -> fthrow:Reg.t
     -> t