From d3d0c4b36e45a905e6ed9369552b593a8d6ddc87 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 14 Oct 2019 07:23:56 -0700 Subject: [PATCH] [sledge][NFC] Rename params to formals Summary: For consistency Reviewed By: ngorogiannis Differential Revision: D17801926 fbshipit-source-id: 012b13561 --- sledge/src/control.ml | 26 +++++++++++++------------- sledge/src/llair/frontend.ml | 6 +++--- sledge/src/llair/llair.ml | 22 +++++++++++----------- sledge/src/llair/llair.mli | 6 +++--- 4 files changed, 30 insertions(+), 30 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 254ecb777..99f9e64fb 100644 --- a/sledge/src/control.ml +++ b/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 diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 176eac2f6..ef6c60258 100644 --- a/sledge/src/llair/frontend.ml +++ b/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] diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index 4d186dfdb..a95e1bd49 100644 --- a/sledge/src/llair/llair.ml +++ b/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 *) diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index 430cbe8e5..176422a5a 100644 --- a/sledge/src/llair/llair.mli +++ b/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