[sledge][NFC] Label args of Domain.call

Summary: Just for legibility.

Reviewed By: ngorogiannis

Differential Revision: D17801937

fbshipit-source-id: ee1bd95d2

sledge/src/control.ml

@@ -271,8 +271,8 @@ module Make (Dom : Domain_sig.Dom) = struct
   let summary_table = Hashtbl.create (module Reg)
 
   let exec_call opts stk state block call globals =
-    let Llair.{callee; args; areturn; return; recursive} = call in
+    let Llair.{callee; args= actuals; areturn; return; recursive} = call in
-    let Llair.{name; params; freturn; locals; entry} = callee in
+    let Llair.{name; params= 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]
@@ -281,7 +281,7 @@ module Make (Dom : Domain_sig.Dom) = struct
       if opts.function_summaries then Dom.dnf state else [state]
     in
     let domain_call =
-      Dom.call ~globals args areturn params
+      Dom.call ~globals ~actuals ~areturn ~formals
         ~locals:(Set.add_option freturn locals)
     in
     List.fold ~init:Work.skip dnf_states ~f:(fun acc state ->
@@ -487,8 +487,8 @@ module Make (Dom : Domain_sig.Dom) = struct
           (Work.init
              (fst
                 (Dom.call ~summaries:opts.function_summaries
-                   ~globals:(used_globals opts reg) [] None [] ~locals
+                   ~globals:(used_globals opts reg) ~actuals:[]
-                   (Dom.init pgm.globals)))
+                   ~areturn:None ~formals:[] ~locals (Dom.init pgm.globals)))
              entry)
     | _ -> None
 

sledge/src/domain/domain_sig.ml

@@ -32,9 +32,9 @@ module type Dom = sig
   val call :
        summaries:bool
     -> globals:Reg.Set.t
-    -> Exp.t list
+    -> actuals:Exp.t list
-    -> Reg.t option
+    -> areturn:Reg.t option
-    -> Reg.t list
+    -> formals:Reg.t list
     -> locals:Reg.Set.t
     -> t
     -> t * from_call

sledge/src/domain/relation.ml

@@ -68,7 +68,7 @@ module Make (State_domain : State_domain_sig) = struct
 
   let recursion_beyond_bound = State_domain.recursion_beyond_bound
 
-  let call ~summaries ~globals actuals areturn formals ~locals
+  let call ~summaries ~globals ~actuals ~areturn ~formals ~locals
       (entry, current) =
     [%Trace.call fun {pf} ->
       pf
@@ -79,8 +79,8 @@ module Make (State_domain : State_domain_sig) = struct
         State_domain.pp current]
     ;
     let caller_current, state_from_call =
-      State_domain.call ~summaries ~globals actuals areturn formals ~locals
+      State_domain.call ~summaries ~globals ~actuals ~areturn ~formals
-        current
+        ~locals current
     in
     ( (caller_current, caller_current)
     , {state_from_call; caller_entry= entry} )

sledge/src/domain/unit.ml

@@ -22,7 +22,10 @@ let exec_intrinsic ~skip_throw:_ _ _ _ _ : t option option = None
 
 type from_call = unit [@@deriving compare, equal, sexp]
 
-let call ~summaries:_ ~globals:_ _ _ _ ~locals:_ _ = ((), ())
+let call ~summaries:_ ~globals:_ ~actuals:_ ~areturn:_ ~formals:_ ~locals:_
+    _ =
+  ((), ())
+
 let recursion_beyond_bound = `skip
 let post _ _ () = ()
 let retn _ _ _ _ = ()

sledge/src/domain/used_globals.ml

@@ -63,7 +63,8 @@ let exec_intrinsic ~skip_throw:_ st _ intrinsic actuals =
 type from_call = t [@@deriving sexp_of]
 
 (* Set abstract state to bottom (i.e. empty set) at function entry *)
-let call ~summaries:_ ~globals:_ actuals _ _ ~locals:_ st =
+let call ~summaries:_ ~globals:_ ~actuals ~areturn:_ ~formals:_ ~locals:_ st
+    =
   (empty, List.fold actuals ~init:st ~f:(fun s a -> used_globals ~init:s a))
 
 let resolve_callee lookup ptr st =

sledge/src/symbheap/sh_domain.ml

@@ -113,7 +113,7 @@ type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t}
 (** Express formula in terms of formals instead of actuals, and enter scope
     of locals: rename formals to fresh vars in formula and actuals, add
     equations between each formal and actual, and quantify fresh vars. *)
-let call ~summaries ~globals actuals areturn formals ~locals q =
+let call ~summaries ~globals ~actuals ~areturn ~formals ~locals q =
   [%Trace.call fun {pf} ->
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ \