[sledge] Rework function return value passing

Summary:
The current handling of the formal return variable scope is not
correct. Since it is passed as an actual argument to the return
continuation, it is manipulated as if it was a local variable of the
caller. However, its scope is not ended with the caller's locals,
leading to clashes.

This diff reworks the passing of return values to avoid this problem,
mainly by introducing a notion of temporary variables during parameter
passing. This essentially has the effect of taking a function spec

{ P } f(x) { λv. Q }

and generating a "temporary" variable v, applying the post λv. Q to it
to obtain the pre-state for the call to the return continuation
k(v). Being a temporary variable just means that it goes out of scope
just after parameter passing. This amounts to a long-winded way of
applying the post-state to the formal parameter of the return
continuation without violating scopes or SSA.

This diff also separates the manipulation of the symbolic states as they
proceed from:

1. the pre-state before the return instruction;

2. the exit-state after the return instruction (including the binding
   of the returned value to the return formal variable);

3. the post-state, where the locals are existentially quantified; and

4. the return-state, which is expressed in terms of actual args
   instead of formal parameters.

Also in support of summarization, formal return and throw parameters
are no longer tracked on the analyzer's stack.

Note that these changes involve changing the locals of blocks and
functions to no longer include the formal parameters.

Reviewed By: kren1

Differential Revision: D15912148

fbshipit-source-id: e41dd6e42

sledge/src/control.ml

@@ -29,16 +29,13 @@ module Stack : sig
     -> t option
 
   val pop_return :
-       t
-    -> init:'a
-    -> f:(Var.t option -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
-    -> (Llair.jump * 'a * t) option
+    t -> (Var.Set.t * Domain.from_call * Llair.jump * t) option
 
   val pop_throw :
        t
     -> init:'a
-    -> f:(Var.t option -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
-    -> (Llair.jump * 'a * t) option
+    -> unwind:(Var.t list -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
+    -> (Var.Set.t * Domain.from_call * Llair.jump * t * 'a) option
 end = struct
   type t =
     | Locals of Var.Set.t * t
@@ -46,8 +43,7 @@ end = struct
         { retreating: bool
               (** return from a call not known to be nonrecursive *)
         ; dst: Llair.Jump.t
-        ; freturn: Var.t option
-        ; fthrow: Var.t
+        ; params: Var.t list
         ; from_call: Domain.from_call
         ; stk: t }
     | Throw of Llair.Jump.t * t
@@ -112,16 +108,15 @@ end = struct
     (if Set.is_empty lcls then stk else Locals (lcls, stk))
     |> check invariant
 
-  let push_return ~retreating dst freturn fthrow from_call stk =
-    Return {retreating; dst; freturn; fthrow; from_call; stk}
-    |> check invariant
+  let push_return ~retreating dst params from_call stk =
+    Return {retreating; dst; params; from_call; stk} |> check invariant
 
   let push_throw jmp stk =
     (match jmp with None -> stk | Some jmp -> Throw (jmp, stk))
     |> check invariant
 
-  let push_call {Llair.locals; parent= {freturn; fthrow}} ~retreating ~bound
-      ~return from_call ?throw stk =
+  let push_call {Llair.params; locals} ~retreating ~bound ~return from_call
+      ?throw stk =
     [%Trace.call fun {pf} -> pf "%a" print_abbrev stk]
     ;
     let rec count_f_in_stack acc f = function
@@ -137,36 +132,28 @@ end = struct
       Some
         (push_jump locals
            (push_throw throw
-              (push_return ~retreating return freturn fthrow from_call stk)))
-    )
+              (push_return ~retreating return params from_call stk))) )
     |>
     [%Trace.retn fun {pf} _ ->
       pf "%d of %a on stack" n Llair.Jump.pp return]
 
-  let pop_return stk ~init ~f =
+  let pop_return stk =
     let rec pop_return_ scope = function
       | Locals (locals, stk) -> pop_return_ (Set.union locals scope) stk
       | Throw (_, stk) -> pop_return_ scope stk
-      | Return {dst; freturn; from_call; stk} ->
-          let dst =
-            match freturn with
-            | Some freturn -> {dst with args= Exp.var freturn :: dst.args}
-            | None -> dst
-          in
-          Some (dst, f freturn scope from_call init, stk)
+      | Return {from_call; dst; stk} -> Some (scope, from_call, dst, stk)
       | Empty -> None
     in
     pop_return_ Var.Set.empty stk
 
-  let pop_throw stk ~init ~f =
+  let pop_throw stk ~init ~unwind =
     let rec pop_throw_ scope state = function
       | Locals (locals, stk) ->
           pop_throw_ (Set.union locals scope) state stk
-      | Return {freturn; from_call; stk} ->
-          pop_throw_ Var.Set.empty (f freturn scope from_call state) stk
-      | Throw (dst, Return {fthrow; from_call; stk}) ->
-          let dst = {dst with args= Exp.var fthrow :: dst.args} in
-          Some (dst, f (Some fthrow) scope from_call state, stk)
+      | Return {params; from_call; stk} ->
+          pop_throw_ Var.Set.empty (unwind params scope from_call state) stk
+      | Throw (dst, Return {from_call; stk}) ->
+          Some (scope, from_call, dst, stk, state)
       | Empty -> None
       | Throw _ as stk -> violates invariant stk
     in
@@ -279,8 +266,8 @@ let exec_goto stk state block ({dst; retreating} : Llair.jump) =
   let stk = Stack.push_jump dst.locals stk in
   Work.add ~prev:block ~retreating stk state dst
 
-let exec_jump stk state block ({dst; args} as jmp : Llair.jump) =
-  let state = Domain.jump args dst.params dst.locals state in
+let exec_jump ?temps stk state block ({dst; args} as jmp : Llair.jump) =
+  let state = Domain.jump args dst.params dst.locals ?temps state in
   exec_goto stk state block jmp
 
 let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
@@ -299,20 +286,52 @@ let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
-let exec_pop pop stk state (block : Llair.block) exp =
+let exec_return stk pre_state (block : Llair.block) exp =
   [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
   ;
-  ( match pop stk ~init:state ~f:(Domain.retn exp) with
-  | Some ((jmp : Llair.jump), state, stk) -> exec_jump stk state block jmp
+  ( match Stack.pop_return stk with
+  | Some (scope, from_call, retn_site, stk) ->
+      let freturn = block.parent.freturn in
+      let exit_state =
+        match (freturn, exp) with
+        | Some freturn, Some return_val ->
+            Domain.exec_return pre_state freturn return_val
+        | None, None -> pre_state
+        | _ -> violates Llair.Func.invariant block.parent
+      in
+      let post_state = Domain.post scope from_call exit_state in
+      let retn_state =
+        Domain.retn block.parent.entry.params from_call post_state
+      in
+      exec_jump stk retn_state block
+        ~temps:(Option.fold ~f:Set.add freturn ~init:Var.Set.empty)
+        ( match freturn with
+        | Some freturn -> Llair.Jump.push_arg (Exp.var freturn) retn_site
+        | None -> retn_site )
   | None -> Work.skip )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
-let exec_return stk state block exp =
-  exec_pop Stack.pop_return stk state block exp
-
-let exec_throw stk state block exc =
-  exec_pop Stack.pop_throw stk state block (Some exc)
+let exec_throw stk pre_state (block : Llair.block) exc =
+  [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
+  ;
+  let unwind params scope from_call state =
+    Domain.retn params from_call (Domain.post scope from_call state)
+  in
+  ( match Stack.pop_throw stk ~unwind ~init:pre_state with
+  | Some (scope, from_call, retn_site, stk, unwind_state) ->
+      let fthrow = block.parent.fthrow in
+      let exit_state = Domain.exec_return unwind_state fthrow exc in
+      let post_state = Domain.post scope from_call exit_state in
+      let retn_state =
+        Domain.retn block.parent.entry.params from_call post_state
+      in
+      exec_jump stk retn_state block
+        ~temps:(Set.add Var.Set.empty fthrow)
+        (Llair.Jump.push_arg (Exp.var fthrow) retn_site)
+  | None -> Work.skip )
+  |>
+  [%Trace.retn fun {pf} _ -> pf ""]
 
 let exec_skip_func :
     Stack.t -> Domain.t -> Llair.block -> Llair.jump -> Work.x =
@@ -342,12 +361,12 @@ let exec_term :
   | Switch {key; tbl; els} ->
       Vector.fold tbl
         ~f:(fun x (case, jump) ->
-          match Domain.assume state (Exp.eq key case) with
+          match Domain.exec_assume state (Exp.eq key case) with
           | Some state -> exec_jump stk state block jump |> Work.seq x
           | None -> x )
         ~init:
           ( match
-              Domain.assume state
+              Domain.exec_assume state
                 (Vector.fold tbl ~init:(Exp.bool true)
                    ~f:(fun b (case, _) -> Exp.and_ (Exp.dq key case) b))
             with
@@ -356,7 +375,7 @@ let exec_term :
   | Iswitch {ptr; tbl} ->
       Vector.fold tbl ~init:Work.skip ~f:(fun x (jump : Llair.jump) ->
           match
-            Domain.assume state
+            Domain.exec_assume state
               (Exp.eq ptr
                  (Exp.label
                     ~parent:(Var.name jump.dst.parent.name.var)

sledge/src/llair/llair.ml

@@ -276,6 +276,8 @@ module Jump = struct
   let mk lbl args =
     {dst= {dummy_block with lbl}; args; retreating= false}
     |> check invariant
+
+  let push_arg arg jmp = {jmp with args= arg :: jmp.args}
 end
 
 (** Basic-Block Terminators *)
@@ -285,7 +287,7 @@ module Term = struct
 
   let pp = pp_term
 
-  let invariant term =
+  let invariant ?parent term =
     Invariant.invariant [%here] term [%sexp_of: t]
     @@ fun () ->
     match term with
@@ -301,7 +303,12 @@ module Term = struct
             ~accept_return:(Option.is_some retn_typ && not ignore_result) ;
           Option.iter throw ~f:(Jump.invariant ~accept_return:true)
       | _ -> assert false )
-    | Return _ | Throw _ | Unreachable -> assert true
+    | Return {exp} -> (
+      match parent with
+      | Some parent ->
+          assert (Bool.(Option.is_some exp = Option.is_some parent.freturn))
+      | None -> assert true )
+    | Throw _ | Unreachable -> assert true
 
   let goto ~dst ~loc =
     Switch {key= Exp.bool false; tbl= Vector.empty; els= dst; loc}
@@ -318,14 +325,8 @@ module Term = struct
   let iswitch ~ptr ~tbl ~loc = Iswitch {ptr; tbl; loc} |> check invariant
 
   let call ~func ~typ ~args ~return ~throw ~ignore_result ~loc =
-    Call
-      { call= {dst= func; args; retreating= false}
-      ; typ
-      ; return
-      ; throw
-      ; ignore_result
-      ; loc }
-    |> check invariant
+    let call = {dst= func; args; retreating= false} in
+    Call {call; typ; return; throw; ignore_result; loc} |> check invariant
 
   let return ~exp ~loc = Return {exp; loc} |> check invariant
   let throw ~exc ~loc = Throw {exc; loc} |> check invariant
@@ -354,11 +355,7 @@ module Block = struct
 
   let mk ~lbl ~params ~cmnd ~term =
     let locals =
-      let locals_cmnd cmnd vs =
-        Vector.fold_right cmnd ~init:vs ~f:Inst.union_locals
-      in
-      let locals_params params vs = List.fold params ~init:vs ~f:Set.add in
-      locals_params params (locals_cmnd cmnd Var.Set.empty)
+      Vector.fold_right ~f:Inst.union_locals cmnd ~init:Var.Set.empty
     in
     { lbl
     ; params
@@ -408,7 +405,7 @@ module Func = struct
     assert (func == func.entry.parent) ;
     let {name= {typ}; cfg} = func in
     match typ with
-    | Pointer _ ->
+    | Pointer {elt= Function {return}} ->
         assert (
           not
             (Vector.contains_dup cfg ~compare:(fun b1 b2 ->
@@ -419,7 +416,8 @@ module Func = struct
                (List.concat_map (Vector.to_list cfg) ~f:(fun {params} ->
                     params ))
                ~compare:Var.compare) ) ;
-        iter_term func ~f:(fun term -> Term.invariant term)
+        assert (Bool.(Option.is_some return = Option.is_some func.freturn)) ;
+        iter_term func ~f:(fun term -> Term.invariant ~parent:func term)
     | _ -> assert false
 
   let find functions name = Map.find functions name
@@ -427,21 +425,18 @@ module Func = struct
   let mk ~(name : Global.t) ~entry ~cfg =
     let locals =
       Vector.fold ~init:entry.locals cfg ~f:(fun locals block ->
-          Set.union locals block.locals )
+          Set.add_list block.params (Set.union locals block.locals) )
     in
-    let freturn, locals =
+    let entry = {entry with locals} in
+    let wrt = Set.add_list entry.params locals in
+    let freturn, wrt =
       match name.typ with
       | Pointer {elt= Function {return= Some _}} ->
-          let freturn, locals =
-            Var.fresh "freturn" ~wrt:(Set.add_list entry.params locals)
-          in
-          (Some freturn, locals)
-      | _ -> (None, locals)
-    in
-    let fthrow, locals =
-      Var.fresh "fthrow" ~wrt:(Set.add_list entry.params locals)
+          let freturn, wrt = Var.fresh "freturn" ~wrt in
+          (Some freturn, wrt)
+      | _ -> (None, wrt)
     in
-    let entry = {entry with locals} in
+    let fthrow, _ = Var.fresh "fthrow" ~wrt in
     let func = {name; entry; cfg; freturn; fthrow} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;

sledge/src/llair/llair.mli

@@ -95,7 +95,7 @@ and term = private
 and block = private
   { lbl: label
   ; params: Var.t list  (** Formal parameters, first-param-last stack *)
-  ; locals: Var.Set.t  (** Local variables, including [params]. *)
+  ; locals: Var.Set.t  (** Local variables *)
   ; cmnd: cmnd
   ; term: term
   ; mutable parent: func
@@ -148,6 +148,7 @@ module Jump : sig
 
   val pp : jump pp
   val mk : string -> Exp.t list -> jump
+  val push_arg : Exp.t -> jump -> jump
 end
 
 module Term : sig

sledge/src/symbheap/domain.ml

@@ -21,8 +21,8 @@ let join (entry_a, current_a) (entry_b, current_b) =
   assert (State_domain.equal entry_b entry_a) ;
   (entry_a, State_domain.join current_a current_b)
 
-let assume (entry, current) q =
-  match State_domain.assume current q with
+let exec_assume (entry, current) cnd =
+  match State_domain.exec_assume current cnd with
   | Some current -> Some (entry, current)
   | None -> None
 
@@ -31,6 +31,9 @@ let exec_inst (entry, current) inst =
   | Ok current -> Ok (entry, current)
   | Error e -> Error e
 
+let exec_return (entry, current) formal actual =
+  (entry, State_domain.exec_return current formal actual)
+
 let exec_intrinsic (entry, current) result intrinsic actuals =
   match State_domain.exec_intrinsic current result intrinsic actuals with
   | None -> None
@@ -41,8 +44,10 @@ type from_call =
   {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
 [@@deriving sexp_of]
 
-let jump actuals formals locals (entry, current) =
-  let current, _ = State_domain.call actuals formals locals current in
+let jump actuals formals locals ?temps (entry, current) =
+  let current, _ =
+    State_domain.call actuals formals locals ?temps current
+  in
   (entry, current)
 
 let call actuals formals locals (_, current) =
@@ -55,11 +60,17 @@ let call actuals formals locals (_, current) =
   |>
   [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln]
 
-let retn actual formal locals {caller_entry; state_from_call} (_, current) =
+let post locals {caller_entry} (_, current) =
+  [%Trace.call fun {pf} -> pf ""]
+  ;
+  (caller_entry, State_domain.post locals current)
+  |>
+  [%Trace.retn fun {pf} -> pf "@,%a" pp]
+
+let retn formals {caller_entry; state_from_call} (_, current) =
   [%Trace.call fun {pf} -> pf ""]
   ;
-  ( caller_entry
-  , State_domain.retn actual formal locals state_from_call current )
+  (caller_entry, State_domain.retn formals state_from_call current)
   |>
   [%Trace.retn fun {pf} -> pf "@,%a" pp]
 

sledge/src/symbheap/domain.mli

@@ -12,17 +12,21 @@ type t
 val pp : t pp
 val init : Global.t vector -> t
 val join : t -> t -> t
-val assume : t -> Exp.t -> t option
+val exec_assume : t -> Exp.t -> t option
 val exec_inst : t -> Llair.inst -> (t, unit) result
+val exec_return : t -> Var.t -> Exp.t -> t
 
 val exec_intrinsic :
   t -> Var.t option -> Var.t -> Exp.t list -> (t, unit) result option
 
 type from_call [@@deriving sexp_of]
 
-val jump : Exp.t list -> Var.t list -> Var.Set.t -> t -> t
+val jump :
+  Exp.t list -> Var.t list -> Var.Set.t -> ?temps:Var.Set.t -> t -> t
+
 val call : Exp.t list -> Var.t list -> Var.Set.t -> t -> t * from_call
-val retn : Exp.t option -> Var.t option -> Var.Set.t -> from_call -> t -> t
+val post : Var.Set.t -> from_call -> t -> t
+val retn : Var.t list -> from_call -> t -> t
 
 val resolve_callee :
   (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list

sledge/src/symbheap/exec.ml

@@ -33,7 +33,9 @@ let zero = Exp.integer Z.zero Typ.siz
  * Instruction small axioms
  *)
 
-let assume cnd pre =
+let return pre formal exp = Sh.and_ (Exp.eq (Exp.var formal) exp) pre
+
+let assume pre cnd =
   let post = Sh.and_ cnd pre in
   if Sh.is_false post then None else Some post
 

sledge/src/symbheap/exec.mli

@@ -7,7 +7,8 @@
 
 (** Symbolic Execution *)
 
-val assume : Exp.t -> Sh.t -> Sh.t option
+val assume : Sh.t -> Exp.t -> Sh.t option
+val return : Sh.t -> Var.t -> Exp.t -> Sh.t
 val inst : Sh.t -> Llair.inst -> (Sh.t, unit) result
 
 val intrinsic :

sledge/src/symbheap/state_domain.ml

@@ -13,10 +13,6 @@ let pp_full fs s = [%Trace.fprintf fs "%a" Sh.pp s]
 let pp fs s = [%Trace.fprintf fs "%a" Sh.pp (Sh.simplify s)]
 let pp fs s = pp_full fs s ; pp fs s
 
-(* I think it would be nice if `-t State_domain.pp` enabled the simplified
-   printing, with `-t State_domain.pp_full` for the more verbose one. So how
-   about this renaming? *)
-
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function
     | {Global.var; init= Some (arr, siz)} ->
@@ -26,7 +22,8 @@ let init globals =
     | _ -> q )
 
 let join = Sh.or_
-let assume q b = Exec.assume b q
+let exec_assume = Exec.assume
+let exec_return = Exec.return
 let exec_inst = Exec.inst
 let exec_intrinsic = Exec.intrinsic
 
@@ -34,15 +31,17 @@ type from_call = Var.Subst.t [@@deriving compare, equal, sexp]
 
 (** 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 the fresh vars. *)
-let call actuals formals locals q =
+    equations between each formal and actual, and quantify the temps and
+    fresh vars. *)
+let call actuals formals locals ?temps q =
   [%Trace.call fun {pf} ->
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]"
       (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
       (List.rev formals) Var.Set.pp locals Sh.pp q]
   ;
-  let q', freshen_locals = Sh.freshen q ~wrt:locals in
+  let wrt = Set.add_list formals locals in
+  let q', freshen_locals = Sh.freshen q ~wrt in
   let and_eq q formal actual =
     let actual' = Exp.rename actual freshen_locals in
     Sh.and_ (Exp.eq (Exp.var formal) actual') q
@@ -50,33 +49,36 @@ let call actuals formals locals q =
   let and_eqs formals actuals q =
     List.fold2_exn ~f:and_eq formals actuals ~init:q
   in
-  (Sh.extend_us locals (and_eqs formals actuals q'), freshen_locals)
+  ( Sh.extend_us locals
+      (Option.fold ~f:(Fn.flip Sh.exists) temps
+         ~init:(and_eqs formals actuals q'))
+  , freshen_locals )
   |>
   [%Trace.retn fun {pf} (q', s) ->
     pf "@[<hv>subst: %a@ q': %a@]" Var.Subst.pp s Sh.pp q']
 
-(** Leave scope of locals and express in terms of actuals instead of
-    formals: existentially quantify locals and formals, and apply inverse of
-    fresh variables for formals renaming to restore the shadowed variables. *)
-let retn actual formal locals freshen_locals q =
+(** Leave scope of locals: existentially quantify locals. *)
+let post locals q =
   [%Trace.call fun {pf} ->
-    pf "@[<hv>%a%alocals: {@[%a@]}@ subst: %a@ q: %a@]"
-      (Option.pp "%a to " Exp.pp)
-      actual (Option.pp "%a@ " Var.pp) formal Var.Set.pp locals Var.Subst.pp
+    pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Var.Set.pp locals Sh.pp q]
+  ;
+  Sh.exists locals q
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
+
+(** Express in terms of actuals instead of formals: existentially quantify
+    formals, and apply inverse of fresh variables for formals renaming to
+    restore the shadowed variables. *)
+let retn formals freshen_locals q =
+  [%Trace.call fun {pf} ->
+    pf "@[<hv>formals: {@[%a@]}@ subst: %a@ q: %a@]" (List.pp ", " Var.pp)
+      formals Var.Subst.pp
       (Var.Subst.invert freshen_locals)
       Sh.pp q]
   ;
-  let q' =
-    match (actual, formal) with
-    | Some actl, Some frml -> Sh.and_ (Exp.eq (Exp.var frml) actl) q
-    | None, None -> q
-    | _ ->
-        fail "mismatched actual and formal return: %a to %a"
-          (Option.pp "%a" Exp.pp) actual (Option.pp "%a" Var.pp) formal ()
-  in
   Sh.rename
     (Var.Subst.invert freshen_locals)
-    (Sh.exists (Option.fold ~f:Set.remove ~init:locals formal) q')
+    (Sh.exists (Var.Set.of_list formals) q)
   |>
   [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
 

sledge/src/symbheap/state_domain.mli

@@ -12,16 +12,25 @@ type t [@@deriving equal, sexp_of]
 val pp : t pp
 val init : Global.t vector -> t
 val join : t -> t -> t
-val assume : t -> Exp.t -> t option
+val exec_assume : t -> Exp.t -> t option
 val exec_inst : t -> Llair.inst -> (t, unit) result
+val exec_return : t -> Var.t -> Exp.t -> t
 
 val exec_intrinsic :
   t -> Var.t option -> Var.t -> Exp.t list -> (t, unit) result option
 
 type from_call [@@deriving compare, equal, sexp]
 
-val call : Exp.t list -> Var.t list -> Var.Set.t -> t -> t * from_call
-val retn : Exp.t option -> Var.t option -> Var.Set.t -> from_call -> t -> t
+val call :
+     Exp.t list
+  -> Var.t list
+  -> Var.Set.t
+  -> ?temps:Var.Set.t
+  -> t
+  -> t * from_call
+
+val post : Var.Set.t -> t -> t
+val retn : Var.t list -> from_call -> t -> t
 
 val resolve_callee :
   (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list