From 330b266d2832c27433c593f25f49d09cda6de9a7 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 20 Jun 2019 13:32:29 -0700 Subject: [PATCH] [sledge] Rework function return value passing MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 103 ++++++++++++++++----------- sledge/src/llair/llair.ml | 51 ++++++------- sledge/src/llair/llair.mli | 3 +- sledge/src/symbheap/domain.ml | 25 +++++-- sledge/src/symbheap/domain.mli | 10 ++- sledge/src/symbheap/exec.ml | 4 +- sledge/src/symbheap/exec.mli | 3 +- sledge/src/symbheap/state_domain.ml | 52 +++++++------- sledge/src/symbheap/state_domain.mli | 15 +++- 9 files changed, 155 insertions(+), 111 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 6cccdce5a..fed120797 100644 --- a/sledge/src/control.ml +++ b/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) diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index 468d03c4b..87cb49021 100644 --- a/sledge/src/llair/llair.ml +++ b/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 ; diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index 08600bb3f..5dfa78fda 100644 --- a/sledge/src/llair/llair.mli +++ b/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 diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml index 7a33722d9..39fbbdeeb 100644 --- a/sledge/src/symbheap/domain.ml +++ b/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] diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli index 1d53cc355..f9b4cca65 100644 --- a/sledge/src/symbheap/domain.mli +++ b/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 diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index e2d8318f6..7ea7650ca 100644 --- a/sledge/src/symbheap/exec.ml +++ b/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 diff --git a/sledge/src/symbheap/exec.mli b/sledge/src/symbheap/exec.mli index 045094525..715777120 100644 --- a/sledge/src/symbheap/exec.mli +++ b/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 : diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index a58ff7c91..b609f8415 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/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 "@[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 "@[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 "@[%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 "@[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 "@[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] diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli index 61e850688..194e8b4a3 100644 --- a/sledge/src/symbheap/state_domain.mli +++ b/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