[sledge] Eliminate SSA

Summary:
While SSA can be useful for code transformation purposes, it offers
little for semantic static analyses. Essentially, such analyses
explore the dynamic semantics of code, and the *static* single
assignment property does not buy much. For example, once an execution
visits a loop body that assigns a variable, there are multiple
assignments that the analysis must deal with. This leads to the need
to treat blocks as if they assign all their local variables, renaming
to avoid name clashes a la Floyd's assignment axiom. That is fine, but
it makes it much more involved to implement a version that is
economical with respect to renaming only when necessary. Additionally
the scoping constraints of SSA are cumbersome and significantly
complicate interprocedural analysis (where there is a long history of
incorrect proof rules for procedures, and SSA pushes the
interprocedural analysis away from being able to use known-good
ones). So this diff changes Llair from a functional SSA form to a
traditional imperative language.

Reviewed By: jvillard

Differential Revision: D16905898

fbshipit-source-id: 0fd835220

sledge/src/control.ml

@@ -18,14 +18,7 @@ module Stack : sig
   val empty : t
 
   val push_call :
-       Llair.block
-    -> retreating:bool
-    -> bound:int
-    -> return:Llair.jump
-    -> Domain.from_call
-    -> ?throw:Llair.jump
-    -> t
-    -> t option
+    Llair.func Llair.call -> bound:int -> Domain.from_call -> t -> t option
 
   val pop_return : t -> (Domain.from_call * Llair.jump * t) option
 
@@ -37,8 +30,7 @@ module Stack : sig
 end = struct
   type t =
     | Return of
-        { retreating: bool
-              (** return from a call not known to be nonrecursive *)
+        { recursive: bool  (** return from a possibly-recursive call *)
         ; dst: Llair.Jump.t
         ; params: Var.t list
         ; locals: Var.Set.t
@@ -59,8 +51,8 @@ end = struct
     if x == y then 0
     else
       match (x, y) with
-      | Return {retreating= true; stk= x}, y
-       |x, Return {retreating= true; stk= y} ->
+      | Return {recursive= true; stk= x}, y
+       |x, Return {recursive= true; stk= y} ->
           compare_as_inlined_location x y
       | Return {dst= j; stk= x}, Return {dst= k; stk= y} -> (
         match Llair.Jump.compare j k with
@@ -77,10 +69,10 @@ end = struct
       | Empty, Empty -> 0
 
   let rec print_abbrev fs = function
-    | Return {retreating= false; stk= s} ->
+    | Return {recursive= false; stk= s} ->
         print_abbrev fs s ;
         Format.pp_print_char fs 'R'
-    | Return {retreating= true; stk= s} ->
+    | Return {recursive= true; stk= s} ->
         print_abbrev fs s ;
         Format.pp_print_string fs "R↑"
     | Throw (_, s) ->
@@ -97,16 +89,16 @@ end = struct
 
   let empty = Empty |> check invariant
 
-  let push_return ~retreating dst params locals from_call stk =
-    Return {retreating; dst; params; locals; from_call; stk}
+  let push_return Llair.{callee= {params; locals}; return; recursive}
+      from_call stk =
+    Return {recursive; dst= return; params; locals; 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 (entry : Llair.block) ~retreating ~bound ~return from_call
-      ?throw stk =
+  let push_call (Llair.{return; throw} as call) ~bound from_call stk =
     [%Trace.call fun {pf} -> pf "%a" print_abbrev stk]
     ;
     let rec count_f_in_stack acc f = function
@@ -118,11 +110,7 @@ end = struct
     in
     let n = count_f_in_stack 0 return stk in
     ( if n > bound then None
-    else
-      Some
-        (push_throw throw
-           (push_return ~retreating return entry.params entry.parent.locals
-              from_call stk)) )
+    else Some (push_throw throw (push_return call from_call stk)) )
     |>
     [%Trace.retn fun {pf} _ ->
       pf "%d of %a on stack" n Llair.Jump.pp return]
@@ -246,55 +234,52 @@ end = struct
     | None -> [%Trace.info "queue empty"] ; ()
 end
 
-let exec_goto stk state block ({dst; retreating} : Llair.jump) =
+let exec_jump stk state block Llair.{dst; retreating} =
   Work.add ~prev:block ~retreating stk state dst
 
-let exec_jump ?temps stk state block ({dst; args} as jmp : Llair.jump) =
-  let state = Domain.jump args dst.params ?temps state in
-  exec_goto stk state block jmp
-
 let summary_table = Hashtbl.create (module Var)
 
-let exec_call opts stk state block ({dst; args; retreating} : Llair.jump)
-    (return : Llair.jump) throw globals =
+let exec_call opts stk state block call globals =
+  let Llair.{callee; args; areturn; return; recursive} = call in
+  let Llair.{name; params; freturn; locals; entry} = callee in
   [%Trace.call fun {pf} ->
-    pf "%a from %a" Var.pp dst.parent.name.var Var.pp
-      return.dst.parent.name.var]
+    pf "%a from %a" Var.pp name.var Var.pp return.dst.parent.name.var]
   ;
   let dnf_states =
     if opts.function_summaries then Domain.dnf state else [state]
   in
-  let locals = dst.parent.locals in
-  let domain_call = Domain.call args dst.params locals globals in
+  let domain_call =
+    Domain.call args areturn params (Set.add_option freturn locals) globals
+  in
   List.fold ~init:Work.skip dnf_states ~f:(fun acc state ->
+      match
+        if not opts.function_summaries then None
+        else
           let maybe_summary_post =
-        if opts.function_summaries then
             let state = fst (domain_call ~summaries:false state) in
-          Hashtbl.find summary_table dst.parent.name.var
+            Hashtbl.find summary_table name.var
             >>= List.find_map ~f:(Domain.apply_summary state)
-        else None
           in
           [%Trace.info
             "Maybe summary post: %a"
               (Option.pp "%a" Domain.pp)
               maybe_summary_post] ;
-      match maybe_summary_post with
+          maybe_summary_post
+      with
       | None ->
           let state, from_call =
             domain_call ~summaries:opts.function_summaries state
           in
           Work.seq acc
-            ( match
-                Stack.push_call ~bound:opts.bound dst ~retreating ~return
-                  from_call ?throw stk
-              with
-            | Some stk -> Work.add stk ~prev:block ~retreating state dst
+            ( match Stack.push_call call ~bound:opts.bound from_call stk with
+            | Some stk ->
+                Work.add stk ~prev:block ~retreating:recursive state entry
             | None -> Work.skip )
-      | Some post -> Work.seq acc (exec_goto stk post block return) )
+      | Some post -> Work.seq acc (exec_jump stk post block return) )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
-let pp_st _ =
+let pp_st () =
   [%Trace.printf
     "@[<v>%t@]" (fun fs ->
         Hashtbl.iteri summary_table ~f:(fun ~key ~data ->
@@ -303,88 +288,72 @@ let pp_st _ =
               data ) )]
 
 let exec_return ~opts stk pre_state (block : Llair.block) exp globals =
-  [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
+  let Llair.{name; params; freturn; locals} = block.parent in
+  [%Trace.call fun {pf} -> pf "from %a" Var.pp name.var]
   ;
   ( match Stack.pop_return stk with
   | Some (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
+            Domain.exec_move pre_state freturn return_val
         | None, None -> pre_state
         | _ -> violates Llair.Func.invariant block.parent
       in
-      let exit_state =
+      let post_state = Domain.post locals from_call exit_state in
+      let post_state =
         if opts.function_summaries then (
           let globals =
             Var.Set.of_vector
               (Vector.map globals ~f:(fun (g : Global.t) -> g.var))
           in
-          let function_summary, exit_state =
-            Domain.create_summary ~locals:block.parent.locals exit_state
-              ~formals:
-                (Set.union
-                   (Var.Set.of_list block.parent.entry.params)
-                   globals)
+          let function_summary, post_state =
+            Domain.create_summary ~locals post_state
+              ~formals:(Set.union (Var.Set.of_list params) globals)
           in
-          Hashtbl.add_multi summary_table ~key:block.parent.name.var
+          Hashtbl.add_multi summary_table ~key:name.var
             ~data:function_summary ;
           pp_st () ;
-          exit_state )
-        else exit_state
+          post_state )
+        else post_state
       in
-      let post_state =
-        Domain.post block.parent.locals 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 )
+      let retn_state = Domain.retn params freturn from_call post_state in
+      exec_jump stk retn_state block retn_site
   | None -> Work.skip )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
 let exec_throw stk pre_state (block : Llair.block) exc =
-  [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
+  let func = block.parent in
+  [%Trace.call fun {pf} -> pf "from %a" Var.pp func.name.var]
   ;
   let unwind params scope from_call state =
-    Domain.retn params from_call (Domain.post scope from_call state)
+    Domain.retn params (Some func.fthrow) from_call
+      (Domain.post scope from_call state)
   in
   ( match Stack.pop_throw stk ~unwind ~init:pre_state with
   | Some (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 block.parent.locals from_call exit_state
-      in
+      let fthrow = func.fthrow in
+      let exit_state = Domain.exec_move unwind_state fthrow exc in
+      let post_state = Domain.post func.locals from_call exit_state in
       let retn_state =
-        Domain.retn block.parent.entry.params from_call post_state
+        Domain.retn func.params func.freturn 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)
+      exec_jump stk retn_state block retn_site
   | None -> Work.skip )
   |>
   [%Trace.retn fun {pf} _ -> pf ""]
 
 let exec_skip_func :
-    Stack.t -> Domain.t -> Llair.block -> Llair.jump -> Work.x =
- fun stk state block ({dst; args} as return) ->
+       Stack.t
+    -> Domain.t
+    -> Llair.block
+    -> Var.t option
+    -> Llair.jump
+    -> Work.x =
+ fun stk state block areturn return ->
   Report.unknown_call block.term ;
-  let return =
-    if List.is_empty dst.params then return
-    else
-      let args =
-        List.fold_right dst.params ~init:args ~f:(fun param args ->
-            Exp.nondet (Var.name param) :: args )
-      in
-      {return with args}
-  in
+  let state = Option.fold ~f:Domain.exec_kill ~init:state areturn in
   exec_jump stk state block return
 
 let exec_term :
@@ -417,32 +386,30 @@ let exec_term :
           with
           | Some state -> exec_jump stk state block jump |> Work.seq x
           | None -> x )
-  | Call {call= {dst; args; retreating}; return; throw} -> (
+  | Call ({callee; args; areturn; return} as call) -> (
     match
       let lookup name =
         Option.to_list (Llair.Func.find pgm.functions name)
       in
-      Domain.resolve_callee lookup dst state
+      Domain.resolve_callee lookup callee state
     with
-    | [] -> exec_skip_func stk state block return
+    | [] -> exec_skip_func stk state block areturn return
     | callees ->
         List.fold callees ~init:Work.skip ~f:(fun x callee ->
             ( match
                 Domain.exec_intrinsic ~skip_throw:opts.skip_throw state
-                  (List.hd return.dst.params)
-                  callee.name.var args
+                  areturn callee.name.var args
               with
             | Some (Error ()) ->
                 Report.invalid_access_term (Domain.project state) block.term ;
                 Work.skip
             | Some (Ok state) when Domain.is_false state -> Work.skip
-            | Some (Ok state) -> exec_goto stk state block return
+            | Some (Ok state) -> exec_jump stk state block return
             | None when Llair.Func.is_undefined callee ->
-                exec_skip_func stk state block return
+                exec_skip_func stk state block areturn return
             | None ->
-                exec_call opts stk state block
-                  {dst= callee.entry; args; retreating}
-                  return throw pgm.globals )
+                exec_call opts stk state block {call with callee}
+                  pgm.globals )
             |> Work.seq x ) )
   | Return {exp} -> exec_return ~opts stk state block exp pgm.globals
   | Throw {exc} ->
@@ -471,13 +438,13 @@ let harness : exec_opts -> Llair.t -> (int -> Work.t) option =
   List.find_map entry_points ~f:(fun name ->
       Llair.Func.find pgm.functions (Var.program name) )
   |> function
-  | Some {locals; entry= {params= []} as block} ->
+  | Some {locals; params= []; entry} ->
       Some
         (Work.init
            (fst
-              (Domain.call ~summaries:opts.function_summaries [] [] locals
-                 pgm.globals (Domain.init pgm.globals)))
-           block)
+              (Domain.call ~summaries:opts.function_summaries [] None []
+                 locals pgm.globals (Domain.init pgm.globals)))
+           entry)
   | _ -> None
 
 let exec_pgm : exec_opts -> Llair.t -> unit =

sledge/src/import/import.ml

@@ -264,6 +264,7 @@ module Set = struct
   let equal_m__t (module Elt : Compare_m) = equal
   let pp pp_elt fs x = List.pp ",@ " pp_elt fs (to_list x)
   let disjoint x y = is_empty (inter x y)
+  let add_option yo x = Option.fold ~f:add ~init:x yo
   let add_list ys x = List.fold ~f:add ~init:x ys
   let diff_inter_diff x y = (diff x y, inter x y, diff y x)
   let inter_diff x y = (inter x y, diff y x)

sledge/src/import/import.mli

@@ -212,6 +212,7 @@ module Set : sig
 
   val pp : 'e pp -> ('e, 'c) t pp
   val disjoint : ('e, 'c) t -> ('e, 'c) t -> bool
+  val add_option : 'e option -> ('e, 'c) t -> ('e, 'c) t
   val add_list : 'e list -> ('e, 'c) t -> ('e, 'c) t
 
   val diff_inter_diff :

sledge/src/llair/exp.ml

@@ -520,6 +520,7 @@ module Var = struct
     let pp_full ?is_x vs = Set.pp (pp_full ?is_x) vs
     let pp = pp_full ?is_x:None
     let empty = Set.empty (module T)
+    let of_option = Option.fold ~f:Set.add ~init:empty
     let of_list = Set.of_list (module T)
     let of_vector = Set.of_vector (module T)
   end

sledge/src/llair/exp.mli

@@ -99,6 +99,7 @@ module Var : sig
     val pp_full : ?is_x:(exp -> bool) -> t pp
     val pp : t pp
     val empty : t
+    val of_option : var option -> t
     val of_list : var list -> t
     val of_vector : var vector -> t
   end

sledge/src/llair/frontend.ml

@@ -675,150 +675,49 @@ let landingpad_typs : x -> Llvm.llvalue -> Typ.t * Typ.t * Llvm.lltype =
   let cxa_exception = Llvm.struct_type llcontext [|tip; dtor|] in
   (i32, xlate_type x tip, cxa_exception)
 
-(** construct the argument of a landingpad block, mainly fix the encoding
-    scheme for landingpad instruction name to block arg name *)
-let landingpad_arg : Llvm.llvalue -> Var.t =
- fun instr -> Var.program (find_name instr ^ ".exc")
-
-(** [rev_map_phis ~f blk] returns [(retn_arg, rev_args, pos)] by rev_mapping
-    over the prefix of [PHI] instructions at the beginning of [blk].
-    [retn_arg], if any, is [f] applied to the [PHI] instruction which takes
-    the return value of every [Invoke] predecessor of [blk]. [rev_args] is
-    the result of applying [f] to each of the other [PHI] instructions.
-    [pos] is the instruction iterator position before the first non-[PHI]
-    instruction of [blk]. *)
-let rev_map_phis :
-       f:(Llvm.llvalue -> 'a)
+(** Translate a control transfer from instruction [instr] to block [dst] to
+    a jump, if necessary by extending [blocks] with a trampoline containing
+    the PHIs of [dst] translated to a move. *)
+let xlate_jump :
+       x
+    -> ?reg_exps:(Var.var * Exp.t) list
+    -> Llvm.llvalue
     -> Llvm.llbasicblock
-    -> 'a option * 'a list * _ Llvm.llpos =
- fun ~f blk ->
-  let rec block_args_ found_invoke_pred retn_arg rev_args pos =
-    match (pos : _ Llvm.llpos) with
-    | Before instr -> (
-      match Llvm.instr_opcode instr with
-      | PHI ->
-          (* [has_invoke_pred] holds if some value selected by this PHI is
-             the return value of an [invoke] instr. [is_retn_arg] holds if
-             for each predecessor terminated by an invoke instr, this PHI
-             instr takes the value of the invoke's return value. *)
-          let has_invoke_pred, is_retn_arg =
-            List.fold (Llvm.incoming instr) ~init:(false, true)
-              ~f:(fun (has_invoke_pred, is_retn_arg) (arg, pred) ->
-                match Llvm.block_terminator pred with
-                | Some instr -> (
-                  match Llvm.instr_opcode instr with
-                  | Invoke when Poly.equal arg instr -> (true, is_retn_arg)
-                  | Invoke -> (has_invoke_pred, false)
-                  | _ -> (has_invoke_pred, is_retn_arg) )
-                | None -> fail "rev_map_phis: %a" pp_llblock blk () )
-          in
-          if found_invoke_pred && has_invoke_pred then
-            (* Supporting multiple PHI instructions that take the return
-               values of invoke instructions will require adding trampolines
-               for the invoke instructions to return to, that each reorder
-               arguments and invoke the translation of this block. *)
-            todo "multiple PHI instructions taking invoke return values: %a"
-              pp_llblock blk () ;
-          let retn_arg, rev_args =
-            if has_invoke_pred && is_retn_arg then (Some (f instr), rev_args)
-            else (None, f instr :: rev_args)
-          in
-          block_args_ has_invoke_pred retn_arg rev_args
-            (Llvm.instr_succ instr)
-      | LandingPad when Option.is_some retn_arg ->
-          (* Supporting returning and throwing to the same block, with
-             different arguments, will require adding trampolines. *)
-          todo
-            "return and throw to the same block with different arguments: %a"
-            pp_llblock blk ()
-      | _ -> (retn_arg, rev_args, pos) )
-    | At_end blk -> fail "rev_map_phis: %a" pp_llblock blk ()
-  in
-  block_args_ false None [] (Llvm.instr_begin blk)
-
-(** [trampoline_args jump_instr dest_block] is the actual arguments to which
-    the translation of [dest_block] should be partially-applied, to yield a
-    trampoline accepting the return parameter of the block and then jumping
-    with all the args. *)
-let trampoline_args : x -> Llvm.llvalue -> Llvm.llbasicblock -> Exp.t list =
- fun x jmp dst ->
-  let src = Llvm.instr_parent jmp in
-  rev_map_phis dst ~f:(fun instr ->
-      List.find_map_exn (Llvm.incoming instr) ~f:(fun (arg, pred) ->
-          if Poly.equal pred src then Some (xlate_value x arg) else None )
-  )
-  |> snd3
-
-(** [unique_pred blk] is the unique predecessor of [blk], or [None] if there
-    are 0 or >1 predecessors. *)
-let unique_pred : Llvm.llbasicblock -> Llvm.llvalue option =
- fun blk ->
-  match Llvm.use_begin (Llvm.value_of_block blk) with
-  | Some use -> (
-    match Llvm.use_succ use with
-    | None -> Some (Llvm.user use)
-    | Some _ -> None )
-  | None -> None
-
-(** [return_formal_is_used instr] holds if the return value of [instr] is
-    used anywhere. *)
-let return_formal_is_used : Llvm.llvalue -> bool =
- fun instr -> Option.is_some (Llvm.use_begin instr)
-
-(** [need_return_trampoline instr blk] holds when the return formal of
-    [instr] is used, but the returned to block [blk] does not take it as an
-    argument (e.g. if it has multiple predecessors and no PHI node). *)
-let need_return_trampoline : Llvm.llvalue -> Llvm.llbasicblock -> bool =
- fun instr blk ->
-  Option.is_none (fst3 (rev_map_phis blk ~f:Fn.id))
-  && Option.is_none (unique_pred blk)
-  && return_formal_is_used instr
-
-(** [unique_used_invoke_pred blk] is the unique predecessor of [blk], if it
-    is an [Invoke] instruction, whose return value is used. *)
-let unique_used_invoke_pred : Llvm.llbasicblock -> 'a option =
- fun blk ->
-  let is_invoke i = Poly.equal (Llvm.instr_opcode i) Invoke in
-  match unique_pred blk with
-  | Some instr when is_invoke instr && return_formal_is_used instr ->
-      Some instr
-  | _ -> None
-
-(** formal parameters accepted by a block *)
-let block_formals : Llvm.llbasicblock -> Var.t list * _ Llvm.llpos =
- fun blk ->
-  let retn_arg, rev_args, pos = rev_map_phis blk ~f:xlate_name in
+    -> Loc.t
+    -> Llair.block list
+    -> Llair.jump * Llair.block list =
+ fun x ?(reg_exps = []) instr dst loc blocks ->
+  let src = Llvm.instr_parent instr in
+  let rec xlate_jump_ reg_exps (pos : _ Llvm.llpos) =
     match pos with
-  | Before instr ->
-      let instr_arg =
-        match Llvm.instr_opcode instr with
-        | LandingPad ->
-            assert (Option.is_none retn_arg (* ensured by rev_map_phis *)) ;
-            Some (landingpad_arg instr)
-        | _ ->
-            Option.first_some retn_arg
-              (Option.map (unique_used_invoke_pred blk) ~f:xlate_name)
+    | Before dst_instr -> (
+      match Llvm.instr_opcode dst_instr with
+      | PHI ->
+          let reg_exp =
+            List.find_map_exn (Llvm.incoming dst_instr)
+              ~f:(fun (arg, pred) ->
+                if Poly.equal pred src then
+                  Some (xlate_name dst_instr, xlate_value x arg)
+                else None )
+          in
+          xlate_jump_ (reg_exp :: reg_exps) (Llvm.instr_succ dst_instr)
+      | _ -> reg_exps )
+    | At_end blk -> fail "xlate_jump: %a" pp_llblock blk ()
+  in
+  let jmp = Llair.Jump.mk (label_of_block dst) in
+  match xlate_jump_ reg_exps (Llvm.instr_begin dst) with
+  | [] -> (jmp, blocks)
+  | reg_exps ->
+      let mov =
+        Llair.Inst.move ~reg_exps:(Vector.of_list_rev reg_exps) ~loc
+      in
+      let lbl = find_name instr ^ ".jmp" in
+      let blk =
+        Llair.Block.mk ~lbl
+          ~cmnd:(Vector.of_array [|mov|])
+          ~term:(Llair.Term.goto ~dst:jmp ~loc)
       in
-      (Option.cons instr_arg rev_args, pos)
-  | At_end blk -> fail "block_formals: %a" pp_llblock blk ()
-
-(** actual arguments passed by a jump to a block *)
-let jump_args : x -> Llvm.llvalue -> Llvm.llbasicblock -> Exp.t list =
- fun x jmp dst ->
-  let src = Llvm.instr_parent jmp in
-  let retn_arg, rev_args, _ =
-    rev_map_phis dst ~f:(fun phi ->
-        Option.value_exn
-          (List.find_map (Llvm.incoming phi) ~f:(fun (arg, pred) ->
-               if Poly.equal pred src then Some (xlate_value x arg)
-               else None )) )
-  in
-  let retn_arg =
-    Option.first_some retn_arg
-      (Option.map (unique_used_invoke_pred dst) ~f:(fun invoke ->
-           Exp.var (xlate_name invoke) ))
-  in
-  Option.cons retn_arg rev_args
+      (Llair.Jump.mk lbl, blk :: blocks)
 
 (** An LLVM instruction is translated to a sequence of LLAIR instructions
     and a terminator, plus some additional blocks to which it may refer
@@ -1025,24 +924,21 @@ let xlate_instr :
               List.rev_init num_args ~f:(fun i ->
                   xlate_value x (Llvm.operand instr i) )
             in
-            let return = Llair.Jump.mk lbl [] in
-            Llair.Term.call ~func ~typ ~args ~loc ~return ~throw:None
-              ~ignore_result:false
+            let areturn = xlate_name_opt instr in
+            let return = Llair.Jump.mk lbl in
+            Llair.Term.call ~func ~typ ~args ~areturn ~return ~throw:None
+              ~ignore_result:false ~loc
           in
-          let params = Option.to_list (xlate_name_opt instr) in
           continue (fun (insts, term) ->
               let cmnd = Vector.of_list insts in
-              ([], call, [Llair.Block.mk ~lbl ~params ~cmnd ~term]) ) )
+              ([], call, [Llair.Block.mk ~lbl ~cmnd ~term]) ) )
   | Invoke -> (
-      let reg = xlate_name_opt instr in
       let llfunc = Llvm.operand instr (Llvm.num_operands instr - 3) in
       let lltyp = Llvm.type_of llfunc in
       assert (Poly.(Llvm.classify_type lltyp = Pointer)) ;
       let fname = Llvm.value_name llfunc in
       let return_blk = Llvm.get_normal_dest instr in
-      let return_dst = label_of_block return_blk in
       let unwind_blk = Llvm.get_unwind_dest instr in
-      let unwind_dst = label_of_block unwind_blk in
       let num_args =
         if not (Llvm.is_var_arg (Llvm.element_type lltyp)) then
           Llvm.num_arg_operands instr
@@ -1058,15 +954,15 @@ let xlate_instr :
         List.rev_init num_args ~f:(fun i ->
             xlate_value x (Llvm.operand instr i) )
       in
+      let areturn = xlate_name_opt instr in
       (* intrinsics *)
       match String.split fname ~on:'.' with
       | _ when Option.is_some (xlate_intrinsic_exp fname) ->
-          let arg = Option.to_list (Option.map ~f:Exp.var reg) in
-          let dst = Llair.Jump.mk return_dst arg in
-          emit_term (Llair.Term.goto ~dst ~loc)
+          let dst, blocks = xlate_jump x instr return_blk loc [] in
+          emit_term (Llair.Term.goto ~dst ~loc) ~blocks
       | ["__llair_throw"] ->
-          let dst = Llair.Jump.mk unwind_dst args in
-          emit_term (Llair.Term.goto ~dst ~loc)
+          let dst, blocks = xlate_jump x instr unwind_blk loc [] in
+          emit_term (Llair.Term.goto ~dst ~loc) ~blocks
       | ["abort"] ->
           emit_term ~prefix:[Llair.Inst.abort ~loc] Llair.Term.unreachable
       | ["_Znwm" (* operator new(size_t num) *)]
@@ -1077,11 +973,11 @@ let xlate_instr :
           let num = xlate_value x (Llvm.operand instr 0) in
           let llt = Llvm.type_of instr in
           let len = Exp.integer (Z.of_int (size_of x llt)) Typ.siz in
-          let args = jump_args x instr return_blk in
-          let dst = Llair.Jump.mk return_dst args in
+          let dst, blocks = xlate_jump x instr return_blk loc [] in
           emit_term
             ~prefix:[Llair.Inst.alloc ~reg ~num ~len ~loc]
             (Llair.Term.goto ~dst ~loc)
+            ~blocks
       (* unimplemented *)
       | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ ->
           todo "statepoints:@ %a" pp_llvalue instr ()
@@ -1089,37 +985,18 @@ let xlate_instr :
       | _ ->
           let func = xlate_func_name x llfunc in
           let typ = xlate_type x (Llvm.type_of llfunc) in
+          let return, blocks = xlate_jump x instr return_blk loc [] in
+          let throw, blocks = xlate_jump x instr unwind_blk loc blocks in
+          let throw = Some throw in
           let ignore_result =
             match typ with
             | Pointer {elt= Function {return= Some _}} ->
-                not (return_formal_is_used instr)
+                Option.is_none (Llvm.use_begin instr)
             | _ -> false
           in
-          let return, blocks =
-            let args = trampoline_args x instr return_blk in
-            if not (need_return_trampoline instr return_blk) then
-              (Llair.Jump.mk return_dst args, [])
-            else
-              let lbl = name ^ ".ret" in
-              let block =
-                let params = [xlate_name instr] in
-                let cmnd = Vector.empty in
-                let term =
-                  let dst = Llair.Jump.mk return_dst args in
-                  Llair.Term.goto ~dst ~loc
-                in
-                Llair.Block.mk ~lbl ~params ~cmnd ~term
-              in
-              (Llair.Jump.mk lbl [], [block])
-          in
-          let throw =
-            let dst = unwind_dst in
-            let args = trampoline_args x instr unwind_blk in
-            Some (Llair.Jump.mk dst args)
-          in
           emit_term
-            (Llair.Term.call ~func ~typ ~args ~loc ~return ~throw
-               ~ignore_result)
+            (Llair.Term.call ~func ~typ ~args ~areturn ~return ~throw
+               ~ignore_result ~loc)
             ~blocks )
   | Ret ->
       let exp =
@@ -1130,61 +1007,53 @@ let xlate_instr :
   | Br -> (
     match Option.value_exn (Llvm.get_branch instr) with
     | `Unconditional blk ->
-        let args = jump_args x instr blk in
-        let dst = Llair.Jump.mk (label_of_block blk) args in
-        emit_term (Llair.Term.goto ~dst ~loc)
+        let dst, blocks = xlate_jump x instr blk loc [] in
+        emit_term (Llair.Term.goto ~dst ~loc) ~blocks
     | `Conditional (cnd, thn, els) ->
         let key = xlate_value x cnd in
-        let thn_lbl = label_of_block thn in
-        let thn_args = jump_args x instr thn in
-        let thn = Llair.Jump.mk thn_lbl thn_args in
-        let els_lbl = label_of_block els in
-        let els_args = jump_args x instr els in
-        let els = Llair.Jump.mk els_lbl els_args in
-        emit_term (Llair.Term.branch ~key ~nzero:thn ~zero:els ~loc) )
+        let thn, blocks = xlate_jump x instr thn loc [] in
+        let els, blocks = xlate_jump x instr els loc blocks in
+        emit_term (Llair.Term.branch ~key ~nzero:thn ~zero:els ~loc) ~blocks
+    )
   | Switch ->
       let key = xlate_value x (Llvm.operand instr 0) in
-      let cases =
+      let cases, blocks =
         let num_cases = (Llvm.num_operands instr / 2) - 1 in
-        let rec xlate_cases i =
+        let rec xlate_cases i blocks =
           if i <= num_cases then
             let idx = Llvm.operand instr (2 * i) in
             let blk =
               Llvm.block_of_value (Llvm.operand instr ((2 * i) + 1))
             in
             let num = xlate_value x idx in
-            let dst = label_of_block blk in
-            let args = jump_args x instr blk in
-            let rest = xlate_cases (i + 1) in
-            (num, Llair.Jump.mk dst args) :: rest
-          else []
+            let jmp, blocks = xlate_jump x instr blk loc blocks in
+            let rest, blocks = xlate_cases (i + 1) blocks in
+            ((num, jmp) :: rest, blocks)
+          else ([], blocks)
         in
-        xlate_cases 1
+        xlate_cases 1 []
       in
       let tbl = Vector.of_list cases in
       let blk = Llvm.block_of_value (Llvm.operand instr 1) in
-      let dst = label_of_block blk in
-      let args = jump_args x instr blk in
-      let els = Llair.Jump.mk dst args in
-      emit_term (Llair.Term.switch ~key ~tbl ~els ~loc)
+      let els, blocks = xlate_jump x instr blk loc blocks in
+      emit_term (Llair.Term.switch ~key ~tbl ~els ~loc) ~blocks
   | IndirectBr ->
       let ptr = xlate_value x (Llvm.operand instr 0) in
       let num_dests = Llvm.num_operands instr - 1 in
-      let lldests =
-        let rec dests i =
+      let lldests, blocks =
+        let rec dests i blocks =
           if i <= num_dests then
             let v = Llvm.operand instr i in
             let blk = Llvm.block_of_value v in
-            let dst = label_of_block blk in
-            let args = jump_args x instr blk in
-            let rest = dests (i + 1) in
-            Llair.Jump.mk dst args :: rest
-          else []
+            let jmp, blocks = xlate_jump x instr blk loc blocks in
+            let rest, blocks = dests (i + 1) blocks in
+            (jmp :: rest, blocks)
+          else ([], blocks)
         in
-        dests 1
+        dests 1 []
       in
       let tbl = Vector.of_list lldests in
-      emit_term (Llair.Term.iswitch ~ptr ~tbl ~loc)
+      emit_term (Llair.Term.iswitch ~ptr ~tbl ~loc) ~blocks
   | LandingPad ->
       (* Translate the landingpad clauses to code to load the type_info from
          the thrown exception, and test the type_info against the clauses,
@@ -1192,7 +1061,7 @@ let xlate_instr :
          passing a value for the selector which the handler code tests to
          e.g. either cleanup or rethrow. *)
       let i32, tip, cxa_exception = landingpad_typs x instr in
-      let exc = Exp.var (landingpad_arg instr) in
+      let exc = Exp.var (Var.program (find_name instr ^ ".exc")) in
       let ti = Var.program (name ^ ".ti") in
       (* std::type_info* ti = ((__cxa_exception* )exc - 1)->exceptionType *)
       let load_ti =
@@ -1213,33 +1082,44 @@ let xlate_instr :
       let typeid = xlate_llvm_eh_typeid_for x tip ti in
       let lbl = name ^ ".unwind" in
       let param = xlate_name instr in
-      let params = [param] in
-      let jump_unwind sel =
-        let dst = lbl in
-        let args = [Exp.record [exc; sel]] in
-        Llair.Jump.mk dst args
+      let jump_unwind i sel rev_blocks =
+        let arg = Exp.record [exc; sel] in
+        let mov =
+          Llair.Inst.move ~reg_exps:(Vector.of_array [|(param, arg)|]) ~loc
+        in
+        let lbl = lbl ^ "." ^ Int.to_string i in
+        let blk =
+          Llair.Block.mk ~lbl
+            ~cmnd:(Vector.of_array [|mov|])
+            ~term:(Llair.Term.goto ~dst:(Llair.Jump.mk lbl) ~loc)
         in
-      let goto_unwind sel =
-        let dst = jump_unwind sel in
-        Llair.Term.goto ~dst ~loc
+        (Llair.Jump.mk lbl, blk :: rev_blocks)
+      in
+      let goto_unwind i sel blocks =
+        let dst, blocks = jump_unwind i sel blocks in
+        (Llair.Term.goto ~dst ~loc, blocks)
       in
       let term_unwind, rev_blocks =
         if Llvm.is_cleanup instr then
-          (goto_unwind (Exp.integer Z.zero i32), [])
+          goto_unwind 0 (Exp.integer Z.zero i32) []
         else
           let num_clauses = Llvm.num_operands instr in
           let lbl i = name ^ "." ^ Int.to_string i in
-          let jump i = Llair.Jump.mk (lbl i) [] in
+          let jump i = Llair.Jump.mk (lbl i) in
           let block i term =
-            Llair.Block.mk ~lbl:(lbl i) ~params:[] ~cmnd:Vector.empty ~term
+            Llair.Block.mk ~lbl:(lbl i) ~cmnd:Vector.empty ~term
           in
-          let match_filter =
-            jump_unwind (Exp.sub i32 (Exp.integer Z.zero i32) typeid)
+          let match_filter i rev_blocks =
+            jump_unwind i
+              (Exp.sub i32 (Exp.integer Z.zero i32) typeid)
+              rev_blocks
           in
-          let xlate_clause i =
+          let xlate_clause i rev_blocks =
             let clause = Llvm.operand instr i in
             let num_tis = Llvm.num_operands clause in
-            if num_tis = 0 then Llair.Term.goto ~dst:match_filter ~loc
+            if num_tis = 0 then
+              let dst, rev_blocks = match_filter i rev_blocks in
+              (Llair.Term.goto ~dst ~loc, rev_blocks)
             else
               match Llvm.classify_type (Llvm.type_of clause) with
               | Array (* filter *) -> (
@@ -1252,30 +1132,32 @@ let xlate_instr :
                       else Exp.dq tiI ti
                     in
                     let key = xlate_filter 0 in
-                    Llair.Term.branch ~loc ~key ~nzero:match_filter
-                      ~zero:(jump (i + 1))
+                    let nzero, rev_blocks = match_filter i rev_blocks in
+                    ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1))
+                    , rev_blocks )
                 | _ -> fail "xlate_instr: %a" pp_llvalue instr () )
               | _ (* catch *) ->
                   let clause = xlate_value x clause in
                   let key =
                     Exp.or_ (Exp.eq clause Exp.null) (Exp.eq clause ti)
                   in
-                  Llair.Term.branch ~loc ~key ~nzero:(jump_unwind typeid)
-                    ~zero:(jump (i + 1))
+                  let nzero, rev_blocks = jump_unwind i typeid rev_blocks in
+                  ( Llair.Term.branch ~loc ~key ~nzero ~zero:(jump (i + 1))
+                  , rev_blocks )
           in
           let rec rev_blocks i z =
             if i < num_clauses then
-              rev_blocks (i + 1) (block i (xlate_clause i) :: z)
+              let term, z = xlate_clause i z in
+              rev_blocks (i + 1) (block i term :: z)
             else block i Llair.Term.unreachable :: z
           in
-          (xlate_clause 0, rev_blocks 1 [])
+          xlate_clause 0 (rev_blocks 1 [])
       in
       continue (fun (insts, term) ->
           ( [load_ti]
           , term_unwind
           , List.rev_append rev_blocks
-              [ Llair.Block.mk ~lbl ~params ~cmnd:(Vector.of_list insts)
-                  ~term ] ) )
+              [Llair.Block.mk ~lbl ~cmnd:(Vector.of_list insts) ~term] ) )
   | Resume ->
       let rcd = xlate_value x (Llvm.operand instr 0) in
       let exc = Exp.select ~rcd ~idx:(Exp.integer Z.zero Typ.siz) in
@@ -1298,6 +1180,18 @@ let xlate_instr :
       fail "xlate_instr: %a" pp_llvalue instr ()
   | PHI | Invalid | Invalid2 | UserOp1 | UserOp2 -> assert false
 
+let skip_phis : Llvm.llbasicblock -> _ Llvm.llpos =
+ fun blk ->
+  let rec skip_phis_ (pos : _ Llvm.llpos) =
+    match pos with
+    | Before instr -> (
+      match Llvm.instr_opcode instr with
+      | PHI -> skip_phis_ (Llvm.instr_succ instr)
+      | _ -> pos )
+    | _ -> pos
+  in
+  skip_phis_ (Llvm.instr_begin blk)
+
 let rec xlate_instrs : pop_thunk -> x -> _ Llvm.llpos -> code =
  fun pop x -> function
   | Before instrI ->
@@ -1313,9 +1207,9 @@ let xlate_block : pop_thunk -> x -> Llvm.llbasicblock -> Llair.block list =
   [%Trace.call fun {pf} -> pf "%a" pp_llblock blk]
   ;
   let lbl = label_of_block blk in
-  let params, pos = block_formals blk in
+  let pos = skip_phis blk in
   let insts, term, blocks = xlate_instrs pop x pos in
-  Llair.Block.mk ~lbl ~params ~cmnd:(Vector.of_list insts) ~term :: blocks
+  Llair.Block.mk ~lbl ~cmnd:(Vector.of_list insts) ~term :: blocks
   |>
   [%Trace.retn fun {pf} blocks -> pf "%s" (List.hd_exn blocks).Llair.lbl]
 
@@ -1341,8 +1235,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
       in
       let entry =
         let {Llair.lbl; cmnd; term} = entry_block in
-        assert (List.is_empty entry_block.params) ;
-        Llair.Block.mk ~lbl ~params ~cmnd ~term
+        Llair.Block.mk ~lbl ~cmnd ~term
       in
       let cfg =
         let rec trav_blocks rev_cfg prev =
@@ -1355,7 +1248,7 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func =
         in
         trav_blocks (List.rev entry_blocks) entry_blk
       in
-      Llair.Func.mk ~name ~entry ~cfg
+      Llair.Func.mk ~name ~params ~entry ~cfg
   | At_end _ ->
       report_undefined llf name ;
       Llair.Func.mk_undefined ~name ~params )

sledge/src/llair/llair.ml

@@ -5,7 +5,9 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(** Translation units *)
+(** LLAIR (Low-Level Analysis Internal Representation) *)
+
+[@@@warning "+9"]
 
 type inst =
   | Move of {reg_exps: (Var.t * Exp.t) vector; loc: Loc.t}
@@ -23,29 +25,29 @@ type inst =
 type cmnd = inst vector [@@deriving sexp]
 type label = string [@@deriving sexp]
 
-type 'a control_transfer =
-  {mutable dst: 'a; args: Exp.t list; mutable retreating: bool}
-[@@deriving compare, equal, sexp_of]
-
-type jump = block control_transfer
+type jump = {mutable dst: block; mutable retreating: bool}
 
-and term =
-  | Switch of {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t}
-  | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t}
-  | Call of
-      { call: Exp.t control_transfer
+and 'a call =
+  { callee: 'a
   ; typ: Typ.t
+  ; args: Exp.t list
+  ; areturn: Var.t option
   ; return: jump
   ; throw: jump option
   ; ignore_result: bool
+  ; mutable recursive: bool
   ; loc: Loc.t }
+
+and term =
+  | Switch of {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t}
+  | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t}
+  | Call of Exp.t call
   | Return of {exp: Exp.t option; loc: Loc.t}
   | Throw of {exc: Exp.t; loc: Loc.t}
   | Unreachable
 
 and block =
   { lbl: label
-  ; params: Var.t list
   ; cmnd: cmnd
   ; term: term
   ; mutable parent: func
@@ -53,15 +55,15 @@ and block =
 
 and cfg = block vector
 
-(* [entry] is not part of [cfg] since it is special in several ways: its
-   params are the func params, and it cannot be jumped to, only called. *)
+(* [entry] is not part of [cfg] since it cannot be jumped to, only called. *)
 and func =
   { name: Global.t
+  ; params: Var.t list
+  ; freturn: Var.t option
+  ; fthrow: Var.t
   ; locals: Var.Set.t
   ; entry: block
-  ; cfg: cfg
-  ; freturn: Var.t option
-  ; fthrow: Var.t }
+  ; cfg: cfg }
 
 let sexp_cons (hd : Sexp.t) (tl : Sexp.t) =
   match tl with
@@ -70,8 +72,8 @@ let sexp_cons (hd : Sexp.t) (tl : Sexp.t) =
 
 let sexp_ctor label args = sexp_cons (Sexp.Atom label) args
 
-let sexp_of_jump {dst; args; retreating} =
-  [%sexp {dst: label = dst.lbl; args: Exp.t list; retreating: bool}]
+let sexp_of_jump {dst; retreating} =
+  [%sexp {dst: label = dst.lbl; retreating: bool}]
 
 let sexp_of_term = function
   | Switch {key; tbl; els; loc} ->
@@ -80,24 +82,35 @@ let sexp_of_term = function
           {key: Exp.t; tbl: (Exp.t * jump) vector; els: jump; loc: Loc.t}]
   | Iswitch {ptr; tbl; loc} ->
       sexp_ctor "Iswitch" [%sexp {ptr: Exp.t; tbl: jump vector; loc: Loc.t}]
-  | Call {call; typ; return; throw; ignore_result; loc} ->
+  | Call
+      { callee
+      ; typ
+      ; args
+      ; areturn
+      ; return
+      ; throw
+      ; ignore_result
+      ; recursive
+      ; loc } ->
       sexp_ctor "Call"
         [%sexp
-          { call: Exp.t control_transfer
+          { callee: Exp.t
           ; typ: Typ.t
+          ; args: Exp.t list
+          ; areturn: Var.t option
           ; return: jump
           ; throw: jump option
           ; ignore_result: bool
+          ; recursive: bool
           ; loc: Loc.t }]
   | Return {exp; loc} ->
       sexp_ctor "Return" [%sexp {exp: Exp.t option; loc: Loc.t}]
   | Throw {exc; loc} -> sexp_ctor "Throw" [%sexp {exc: Exp.t; loc: Loc.t}]
   | Unreachable -> Sexp.Atom "Unreachable"
 
-let sexp_of_block {lbl; params; cmnd; term; parent; sort_index} =
+let sexp_of_block {lbl; cmnd; term; parent; sort_index} =
   [%sexp
     { lbl: label
-    ; params: Var.t list
     ; cmnd: cmnd
     ; term: term
     ; parent: Var.t = parent.name.var
@@ -105,8 +118,15 @@ let sexp_of_block {lbl; params; cmnd; term; parent; sort_index} =
 
 let sexp_of_cfg v = [%sexp_of: block vector] v
 
-let sexp_of_func {name; locals; entry; cfg} =
-  [%sexp {name: Global.t; locals: Var.Set.t; entry: block; cfg: cfg}]
+let sexp_of_func {name; params; freturn; fthrow; locals; entry; cfg} =
+  [%sexp
+    { name: Global.t
+    ; params: Var.t list
+    ; freturn: Var.t option
+    ; fthrow: Var.t
+    ; locals: Var.Set.t
+    ; entry: block
+    ; cfg: cfg }]
 
 (* blocks in a [t] are uniquely identified by [sort_index] *)
 let compare_block x y = Int.compare x.sort_index y.sort_index
@@ -125,7 +145,7 @@ let pp_inst fs inst =
       pf "@[<2>@[%a@]@ := @[%a@];@]\t%a" (Vector.pp ",@ " Var.pp) regs
         (Vector.pp ",@ " Exp.pp) exps Loc.pp loc
   | Load {reg; ptr; len; loc} ->
-      pf "@[<2>load %a@ %a@ %a;@]\t%a" Exp.pp len Var.pp reg Exp.pp ptr
+      pf "@[<2>%a@ := load %a@ %a;@]\t%a" Var.pp reg Exp.pp len Exp.pp ptr
         Loc.pp loc
   | Store {ptr; exp; len; loc} ->
       pf "@[<2>store %a@ %a@ %a;@]\t%a" Exp.pp len Exp.pp ptr Exp.pp exp
@@ -140,12 +160,13 @@ let pp_inst fs inst =
       pf "@[<2>memmov %a %a %a;@]\t%a" Exp.pp len Exp.pp dst Exp.pp src
         Loc.pp loc
   | Alloc {reg; num; len; loc} ->
-      pf "@[<2>alloc %a@ [%a x %a];@]\t%a" Var.pp reg Exp.pp num Exp.pp len
-        Loc.pp loc
+      pf "@[<2>%a@ := alloc [%a x %a];@]\t%a" Var.pp reg Exp.pp num Exp.pp
+        len Loc.pp loc
   | Free {ptr; loc} -> pf "@[<2>free %a;@]\t%a" Exp.pp ptr Loc.pp loc
   | Nondet {reg; msg; loc} ->
-      pf "@[<2>nondet %a\"%s\";@]\t%a" (Option.pp "%a " Var.pp) reg msg
-        Loc.pp loc
+      pf "@[<2>%anondet \"%s\";@]\t%a"
+        (Option.pp "%a := " Var.pp)
+        reg msg Loc.pp loc
   | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc
 
 let pp_args pp_arg fs args =
@@ -153,10 +174,10 @@ let pp_args pp_arg fs args =
 
 let pp_param fs var = Var.pp fs var
 
-let pp_jump fs {dst= {lbl}; args; retreating} =
-  Format.fprintf fs "@[<2>%s%%%s%a@]"
+let pp_jump fs {dst; retreating} =
+  Format.fprintf fs "@[<2>%s%%%s@]"
     (if retreating then "↑" else "")
-    lbl (pp_args Exp.pp) args
+    dst.lbl
 
 let pp_term fs term =
   let pf pp = Format.fprintf fs pp in
@@ -175,13 +196,15 @@ let pp_term fs term =
           tbl pp_goto els Loc.pp loc )
   | Iswitch {ptr; tbl; loc} ->
       pf "@[<2>iswitch %a@ @[<hv>%a@]@]\t%a" Exp.pp ptr
-        (Vector.pp "@ " (fun fs ({dst= {lbl}; _} as jmp) ->
-             Format.fprintf fs "%s: %a" lbl pp_goto jmp ))
+        (Vector.pp "@ " (fun fs jmp ->
+             Format.fprintf fs "%s: %a" jmp.dst.lbl pp_goto jmp ))
         tbl Loc.pp loc
-  | Call {call= {dst; args; retreating}; return; throw; loc} ->
-      pf "@[<2>@[<7>call @[<2>%s%a%a@]@]@ @[returnto %a%a;@]@]\t%a"
-        (if retreating then "↑" else "")
-        Exp.pp dst (pp_args Exp.pp) args pp_jump return
+  | Call {callee; args; areturn; return; throw; recursive; loc; _} ->
+      pf "@[<2>@[<7>%acall @[<2>%s%a%a@]@]@ @[returnto %a%a;@]@]\t%a"
+        (Option.pp "%a := " Var.pp)
+        areturn
+        (if recursive then "↑" else "")
+        Exp.pp callee (pp_args Exp.pp) args pp_jump return
         (Option.pp "@ throwto %a" pp_jump)
         throw Loc.pp loc
   | Return {exp; loc} ->
@@ -191,9 +214,9 @@ let pp_term fs term =
 
 let pp_cmnd = Vector.pp "@ " pp_inst
 
-let pp_block fs {lbl; params; cmnd; term; sort_index} =
-  Format.fprintf fs "@[<v 2>@[<4>%s%a@]: #%i@ @[<v>%a%t%a@]@]" lbl
-    (pp_args pp_param) params sort_index pp_cmnd cmnd
+let pp_block fs {lbl; cmnd; term; parent= _; sort_index} =
+  Format.fprintf fs "@[<v 2>%s: #%i@ @[<v>%a%t%a@]@]" lbl sort_index pp_cmnd
+    cmnd
     (fun fs -> if Vector.is_empty cmnd then () else Format.fprintf fs "@ ")
     pp_term term
 
@@ -201,7 +224,6 @@ let pp_block fs {lbl; params; cmnd; term; sort_index} =
 
 let rec dummy_block =
   { lbl= "dummy"
-  ; params= []
   ; cmnd= Vector.empty
   ; term= Unreachable
   ; parent= dummy_func
@@ -211,11 +233,12 @@ and dummy_func =
   let dummy_var = Var.program "dummy" in
   let dummy_ptr_typ = Typ.pointer ~elt:(Typ.opaque ~name:"dummy") in
   { name= Global.mk dummy_var dummy_ptr_typ Loc.none
+  ; params= []
+  ; freturn= None
+  ; fthrow= dummy_var
   ; locals= Var.Set.empty
   ; entry= dummy_block
-  ; cfg= Vector.empty
-  ; freturn= None
-  ; fthrow= dummy_var }
+  ; cfg= Vector.empty }
 
 (** Instructions *)
 
@@ -235,25 +258,26 @@ module Inst = struct
   let abort ~loc = Abort {loc}
 
   let loc = function
-    | Move {loc}
-     |Load {loc}
-     |Store {loc}
-     |Memset {loc}
-     |Memcpy {loc}
-     |Memmov {loc}
-     |Alloc {loc}
-     |Free {loc}
-     |Nondet {loc}
-     |Abort {loc} ->
+    | Move {loc; _}
+     |Load {loc; _}
+     |Store {loc; _}
+     |Memset {loc; _}
+     |Memcpy {loc; _}
+     |Memmov {loc; _}
+     |Alloc {loc; _}
+     |Free {loc; _}
+     |Nondet {loc; _}
+     |Abort {loc; _} ->
         loc
 
   let union_locals inst vs =
     match inst with
-    | Move {reg_exps} ->
+    | Move {reg_exps; _} ->
         Vector.fold ~f:(fun vs (reg, _) -> Set.add vs reg) ~init:vs reg_exps
-    | Load {reg} | Alloc {reg} | Nondet {reg= Some reg} -> Set.add vs reg
+    | Load {reg; _} | Alloc {reg; _} | Nondet {reg= Some reg; _} ->
+        Set.add vs reg
     | Store _ | Memcpy _ | Memmov _ | Memset _ | Free _
-     |Nondet {reg= None}
+     |Nondet {reg= None; _}
      |Abort _ ->
         vs
 
@@ -265,26 +289,10 @@ end
 module Jump = struct
   type t = jump [@@deriving sexp_of]
 
-  let compare = compare_control_transfer compare_block
-  let equal = equal_control_transfer equal_block
+  let compare x y = compare_block x.dst y.dst
+  let equal x y = equal_block x.dst y.dst
   let pp = pp_jump
-
-  let invariant ?(accept_return = false) jmp =
-    Invariant.invariant [%here] (jmp, accept_return) [%sexp_of: t * bool]
-    @@ fun () ->
-    let {dst= {params; parent}; args} = jmp in
-    if parent == dummy_func then
-      (* jmp not yet backpatched by Func.mk *)
-      assert true
-    else
-      assert (
-        List.length params = List.length args + Bool.to_int accept_return )
-
-  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}
+  let mk lbl = {dst= {dummy_block with lbl}; retreating= false}
 end
 
 (** Basic-Block Terminators *)
@@ -298,19 +306,14 @@ module Term = struct
     Invariant.invariant [%here] term [%sexp_of: t]
     @@ fun () ->
     match term with
-    | Switch {tbl; els} ->
-        Vector.iter tbl ~f:(fun (_, jmp) -> Jump.invariant jmp) ;
-        Jump.invariant els
-    | Iswitch {tbl} -> Vector.iter tbl ~f:Jump.invariant
-    | Call {call= {args= actls}; typ; return; throw; ignore_result} -> (
+    | Switch _ | Iswitch _ -> assert true
+    | Call {typ; args= actls; areturn; _} -> (
       match typ with
-      | Pointer {elt= Function {args= frmls; return= retn_typ}} ->
+      | Pointer {elt= Function {args= frmls; return= retn_typ; _}} ->
           assert (Vector.length frmls = List.length actls) ;
-          Jump.invariant return
-            ~accept_return:(Option.is_some retn_typ && not ignore_result) ;
-          Option.iter throw ~f:(Jump.invariant ~accept_return:true)
+          assert (Option.is_some retn_typ || Option.is_none areturn)
       | _ -> assert false )
-    | Return {exp} -> (
+    | Return {exp; _} -> (
       match parent with
       | Some parent ->
           assert (Bool.(Option.is_some exp = Option.is_some parent.freturn))
@@ -331,19 +334,36 @@ module Term = struct
 
   let iswitch ~ptr ~tbl ~loc = Iswitch {ptr; tbl; loc} |> check invariant
 
-  let call ~func ~typ ~args ~return ~throw ~ignore_result ~loc =
-    let call = {dst= func; args; retreating= false} in
-    Call {call; typ; return; throw; ignore_result; loc} |> check invariant
+  let call ~func ~typ ~args ~areturn ~return ~throw ~ignore_result ~loc =
+    Call
+      { callee= func
+      ; typ
+      ; args
+      ; areturn
+      ; return
+      ; throw
+      ; ignore_result
+      ; recursive= false
+      ; loc }
+    |> check invariant
 
   let return ~exp ~loc = Return {exp; loc} |> check invariant
   let throw ~exc ~loc = Throw {exc; loc} |> check invariant
   let unreachable = Unreachable |> check invariant
 
   let loc = function
-    | Switch {loc} | Iswitch {loc} | Call {loc} | Return {loc} | Throw {loc}
-      ->
+    | Switch {loc; _}
+     |Iswitch {loc; _}
+     |Call {loc; _}
+     |Return {loc; _}
+     |Throw {loc; _} ->
         loc
     | Unreachable -> Loc.none
+
+  let union_locals term vs =
+    match term with
+    | Call {areturn; _} -> Set.add_option areturn vs
+    | _ -> vs
 end
 
 (** Basic-Blocks *)
@@ -355,19 +375,12 @@ module Block = struct
 
   let pp = pp_block
 
-  let invariant blk =
-    Invariant.invariant [%here] blk [%sexp_of: t]
-    @@ fun () ->
-    assert (not (List.contains_dup blk.params ~compare:Var.compare))
-
-  let mk ~lbl ~params ~cmnd ~term =
+  let mk ~lbl ~cmnd ~term =
     { lbl
-    ; params
     ; cmnd
     ; term
     ; parent= dummy_block.parent
     ; sort_index= dummy_block.sort_index }
-    |> check invariant
 end
 
 (** Functions *)
@@ -376,16 +389,25 @@ module Func = struct
   type t = func [@@deriving sexp_of]
 
   let is_undefined = function
-    | {entry= {cmnd; term= Unreachable}} -> Vector.is_empty cmnd
+    | {entry= {cmnd; term= Unreachable; _}; _} -> Vector.is_empty cmnd
     | _ -> false
 
-  let pp fs ({name; entry= {params; cmnd; term; sort_index}; cfg} as func) =
+  let pp fs
+      ( { name
+        ; params
+        ; freturn
+        ; fthrow= _
+        ; locals= _
+        ; entry= {cmnd; term; sort_index; _}
+        ; cfg } as func ) =
     let pp_if cnd str fs = if cnd then Format.fprintf fs str in
-    Format.fprintf fs "@[<v>@[<v>%a@[<2>%a%a@]%t@]" (Option.pp "%a " Typ.pp)
+    Format.fprintf fs "@[<v>@[<v>%a%a@[<2>%a%a@]%t@]"
+      (Option.pp "%a " Typ.pp)
       ( match name.typ with
-      | Pointer {elt= Function {return}} -> return
+      | Pointer {elt= Function {return; _}} -> return
       | _ -> None )
-      Global.pp name (pp_args pp_param) params
+      (Option.pp " %a := " Var.pp)
+      freturn Global.pp name (pp_args pp_param) params
       (fun fs ->
         if is_undefined func then Format.fprintf fs " #%i@]" sort_index
         else
@@ -395,57 +417,51 @@ module Func = struct
             (Vector.pp "@\n@\n  " Block.pp)
             cfg )
 
-  let fold_term {entry= {term}; cfg} ~init ~f =
-    Vector.fold cfg ~init:(f init term) ~f:(fun a {term} -> f a term)
+  let fold_term {entry; cfg; _} ~init ~f =
+    Vector.fold cfg ~init:(f init entry.term) ~f:(fun a blk -> f a blk.term)
 
-  let iter_term {entry= {term}; cfg} ~f =
-    f term ;
-    Vector.iter cfg ~f:(fun {term} -> f term)
+  let iter_term {entry; cfg; _} ~f =
+    f entry.term ;
+    Vector.iter cfg ~f:(fun blk -> f blk.term)
 
   let invariant func =
     Invariant.invariant [%here] func [%sexp_of: t]
     @@ fun () ->
     assert (func == func.entry.parent) ;
-    let {name= {typ}; entry; cfg} = func in
+    let {name= {typ; _}; cfg; _} = func in
     match typ with
-    | Pointer {elt= Function {return}} ->
+    | Pointer {elt= Function {return; _}} ->
         assert (
           not
             (Vector.contains_dup cfg ~compare:(fun b1 b2 ->
                  String.compare b1.lbl b2.lbl )) ) ;
-        assert (
-          not
-            (List.contains_dup
-               (List.concat_map (entry :: Vector.to_list cfg) ~f:(fun blk ->
-                    blk.params ))
-               ~compare:Var.compare) ) ;
         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
 
-  let mk ~(name : Global.t) ~entry ~cfg =
+  let mk ~(name : Global.t) ~params ~entry ~cfg =
     let locals =
       let locals_cmnd locals cmnd =
         Vector.fold_right ~f:Inst.union_locals cmnd ~init:locals
       in
       let locals_block locals block =
-        Set.add_list block.params (locals_cmnd locals block.cmnd)
+        locals_cmnd (Term.union_locals block.term locals) block.cmnd
       in
-      let init = locals_cmnd Var.Set.empty entry.cmnd in
+      let init = locals_block Var.Set.empty entry in
       Vector.fold ~f:locals_block cfg ~init
     in
-    let wrt = Set.add_list entry.params locals in
+    let wrt = Set.add_list params locals in
     let freturn, wrt =
       match name.typ with
-      | Pointer {elt= Function {return= Some _}} ->
+      | Pointer {elt= Function {return= Some _; _}} ->
           let freturn, wrt = Var.fresh "freturn" ~wrt in
           (Some freturn, wrt)
       | _ -> (None, wrt)
     in
     let fthrow, _ = Var.fresh "fthrow" ~wrt in
-    let func = {name; locals; entry; cfg; freturn; fthrow} in
+    let func = {name; params; freturn; fthrow; locals; entry; cfg} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
       let lookup cfg lbl : block =
@@ -453,11 +469,11 @@ module Func = struct
       in
       let set_dst jmp = jmp.dst <- lookup cfg jmp.dst.lbl in
       match block.term with
-      | Switch {tbl; els} ->
+      | Switch {tbl; els; _} ->
           Vector.iter tbl ~f:(fun (_, jmp) -> set_dst jmp) ;
           set_dst els
-      | Iswitch {tbl} -> Vector.iter tbl ~f:set_dst
-      | Call {return; throw} ->
+      | Iswitch {tbl; _} -> Vector.iter tbl ~f:set_dst
+      | Call {return; throw; _} ->
           set_dst return ;
           Option.iter throw ~f:set_dst
       | Return _ | Throw _ | Unreachable -> ()
@@ -468,10 +484,10 @@ module Func = struct
 
   let mk_undefined ~name ~params =
     let entry =
-      Block.mk ~lbl:"" ~params ~cmnd:Vector.empty ~term:Term.unreachable
+      Block.mk ~lbl:"" ~cmnd:Vector.empty ~term:Term.unreachable
     in
     let cfg = Vector.empty in
-    mk ~name ~entry ~cfg
+    mk ~name ~entry ~params ~cfg
 end
 
 (** Derived meta-data *)
@@ -509,8 +525,8 @@ let set_derived_metadata functions =
         FuncQ.enqueue_back_exn roots func.name.var func ) ;
     Map.iter functions ~f:(fun func ->
         Func.fold_term func ~init:() ~f:(fun () -> function
-          | Call {call= {dst}} -> (
-            match Var.of_exp dst with
+          | Call {callee; _} -> (
+            match Var.of_exp callee with
             | Some callee ->
                 FuncQ.remove roots callee |> (ignore : [> ] -> unit)
             | None -> () )
@@ -528,18 +544,18 @@ let set_derived_metadata functions =
           else visit ancestors func jmp.dst
         in
         ( match src.term with
-        | Switch {tbl; els} ->
+        | Switch {tbl; els; _} ->
             Vector.iter tbl ~f:(fun (_, jmp) -> jump jmp) ;
             jump els
-        | Iswitch {tbl} -> Vector.iter tbl ~f:jump
-        | Call {call= {dst} as call; return; throw} ->
-            ( match Var.of_exp dst >>= Func.find functions with
+        | Iswitch {tbl; _} -> Vector.iter tbl ~f:jump
+        | Call ({callee; return; throw; _} as call) ->
+            ( match Var.of_exp callee >>= Func.find functions with
             | Some func ->
-                if Set.mem ancestors func.entry then call.retreating <- true
+                if Set.mem ancestors func.entry then call.recursive <- true
                 else visit ancestors func func.entry
             | None ->
                 (* conservatively assume all virtual calls are recursive *)
-                call.retreating <- true ) ;
+                call.recursive <- true ) ;
             jump return ; Option.iter ~f:jump throw
         | Return _ | Throw _ | Unreachable -> () ) ;
         BlockQ.enqueue_back_exn tips_to_roots src ()
@@ -555,7 +571,7 @@ let set_derived_metadata functions =
         index := !index - 1 )
   in
   let sort_cfgs functions =
-    Map.iter functions ~f:(fun {cfg} ->
+    Map.iter functions ~f:(fun {cfg; _} ->
         Array.sort
           ~compare:(fun x y -> Int.compare x.sort_index y.sort_index)
           (Vector.to_array cfg) )

sledge/src/llair/llair.mli

@@ -5,28 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(** Translation units
-
-    LLAIR (Low-Level Analysis Internal Representation) is an IR tailored for
-    static analysis using a low-level model of memory. Compared to a
-    compiler IR such as LLVM, an analyzer does not need to perform register
-    allocation, instruction selection, code generation, etc. or even much
-    code transformation, so the constraints on the IR are very different.
-
-    LLAIR is a "Functional SSA" form where control transfers pass arguments
-    instead of using ϕ-nodes. An analyzer will need good support for
-    parameter passing anyhow, and ϕ-nodes make it hard to express program
-    properties as predicates on states, since some execution history is
-    needed to evaluate ϕ instructions. An alternative view is that the scope
-    of variables [reg] assigned in instructions such as [Load] is the
-    successor block as well as all blocks the instruction dominates in the
-    control-flow graph. This language is first-order, and a term structure
-    for the code constituting the scope of variables is not needed, so SSA
-    rather than full CPS suffices.
-
-    Additionally, the focus on memory analysis leads to a design where the
-    arithmetic and logic operations are not "instructions" but instead are
-    complex expressions (see [Exp]) that refer to registers (see [Var]). *)
+(** LLAIR (Low-Level Analysis Internal Representation) is an IR tailored for
+    static analysis using a low-level model of memory. *)
 
 (** Instructions for memory manipulation or other non-control effects. *)
 type inst = private
@@ -61,15 +41,21 @@ type cmnd = inst vector
 (** A label is a name of a block. *)
 type label = string
 
-(** A jump with arguments. *)
-type 'a control_transfer =
-  { mutable dst: 'a
-  ; args: Exp.t list  (** Stack of arguments, first-arg-last *)
-  ; mutable retreating: bool
-        (** Holds if [dst] is an ancestor in a depth-first traversal. *) }
+(** A jump to a block. *)
+type jump = {mutable dst: block; mutable retreating: bool}
 
-(** A jump with arguments to a block. *)
-type jump = block control_transfer
+(** A call to a function. *)
+and 'a call =
+  { callee: 'a
+  ; typ: Typ.t  (** Type of the callee. *)
+  ; args: Exp.t list  (** Stack of arguments, first-arg-last. *)
+  ; areturn: Var.t option  (** Register to receive return value. *)
+  ; return: jump  (** Return destination. *)
+  ; throw: jump option  (** Handler destination. *)
+  ; ignore_result: bool  (** Drop return value when invoking return. *)
+  ; mutable recursive: bool
+        (** Holds unless [callee] is definitely not recursive. *)
+  ; loc: Loc.t }
 
 (** Block terminators for function call/return or other control transfers. *)
 and term = private
@@ -78,14 +64,8 @@ and term = private
           [case] which is equal to [key], if any, otherwise invoke [els]. *)
   | Iswitch of {ptr: Exp.t; tbl: jump vector; loc: Loc.t}
       (** Invoke the [jump] in [tbl] whose [dst] is equal to [ptr]. *)
-  | Call of
-      { call: Exp.t control_transfer  (** A [global] for non-virtual call. *)
-      ; typ: Typ.t  (** Type of the callee. *)
-      ; return: jump  (** Return destination or trampoline. *)
-      ; throw: jump option  (** Handler destination or trampoline. *)
-      ; ignore_result: bool  (** Drop return value when invoking return. *)
-      ; loc: Loc.t }
-      (** Call function [call.dst] with arguments [call.args]. *)
+  | Call of Exp.t call
+      (** Call function with arguments. A [global] for non-virtual call. *)
   | Return of {exp: Exp.t option; loc: Loc.t}
       (** Invoke [return] of the dynamically most recent [Call]. *)
   | Throw of {exc: Exp.t; loc: Loc.t}
@@ -97,7 +77,6 @@ and term = private
 (** A block is a destination of a jump with arguments, contains code. *)
 and block = private
   { lbl: label
-  ; params: Var.t list  (** Formal parameters, first-param-last stack *)
   ; cmnd: cmnd
   ; term: term
   ; mutable parent: func
@@ -111,11 +90,12 @@ and cfg
     parameters are the function parameters. *)
 and func = private
   { name: Global.t
+  ; params: Var.t list  (** Formal parameters, first-param-last stack *)
+  ; freturn: Var.t option
+  ; fthrow: Var.t
   ; locals: Var.Set.t  (** Local variables *)
   ; entry: block
-  ; cfg: cfg
-  ; freturn: Var.t option
-  ; fthrow: Var.t }
+  ; cfg: cfg }
 
 type functions
 
@@ -151,8 +131,7 @@ module Jump : sig
   type t = jump [@@deriving compare, equal, sexp_of]
 
   val pp : jump pp
-  val mk : string -> Exp.t list -> jump
-  val push_arg : Exp.t -> jump -> jump
+  val mk : string -> jump
 end
 
 module Term : sig
@@ -175,6 +154,7 @@ module Term : sig
        func:Exp.t
     -> typ:Typ.t
     -> args:Exp.t list
+    -> areturn:Var.t option
     -> return:jump
     -> throw:jump option
     -> ignore_result:bool
@@ -193,10 +173,7 @@ module Block : sig
   include Comparator.S with type t := t
 
   val pp : t pp
-
-  include Invariant.S with type t := t
-
-  val mk : lbl:label -> params:Var.t list -> cmnd:cmnd -> term:term -> block
+  val mk : lbl:label -> cmnd:cmnd -> term:term -> block
 end
 
 module Func : sig
@@ -206,7 +183,13 @@ module Func : sig
 
   include Invariant.S with type t := t
 
-  val mk : name:Global.t -> entry:block -> cfg:block vector -> func
+  val mk :
+       name:Global.t
+    -> params:Var.t list
+    -> entry:block
+    -> cfg:block vector
+    -> func
+
   val mk_undefined : name:Global.t -> params:Var.t list -> t
 
   val find : functions -> Var.t -> func option

sledge/src/report.ml

@@ -15,10 +15,10 @@ let unknown_call call =
       call
       (fun fs (call : Llair.Term.t) ->
         match call with
-        | Call {call= {dst}} -> (
-          match Var.of_exp dst with
+        | Call {callee} -> (
+          match Var.of_exp callee with
           | Some var -> Var.pp_demangled fs var
-          | None -> Exp.pp fs dst )
+          | None -> Exp.pp fs callee )
         | _ -> () )
       call Llair.Term.pp call]
 

sledge/src/symbheap/domain.ml

@@ -29,17 +29,21 @@ let exec_assume (entry, current) cnd =
   | Some current -> Some (entry, current)
   | None -> None
 
+let exec_kill (entry, current) reg =
+  (entry, State_domain.exec_kill current reg)
+
+let exec_move (entry, current) formal actual =
+  (entry, State_domain.exec_move current formal actual)
+
 let exec_inst (entry, current) inst =
   match State_domain.exec_inst current inst with
   | 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 ~skip_throw (entry, current) result intrinsic actuals =
+let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals =
   match
-    State_domain.exec_intrinsic ~skip_throw current result intrinsic actuals
+    State_domain.exec_intrinsic ~skip_throw current areturn intrinsic
+      actuals
   with
   | None -> None
   | Some (Ok current) -> Some (Ok (entry, current))
@@ -49,11 +53,8 @@ type from_call =
   {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
 [@@deriving sexp_of]
 
-let jump actuals formals ?temps (entry, current) =
-  let current, _ = State_domain.jump actuals formals ?temps current in
-  (entry, current)
-
-let call ~summaries actuals formals locals globals_vec (entry, current) =
+let call ~summaries actuals areturn formals locals globals_vec
+    (entry, current) =
   let globals =
     Var.Set.of_vector
       (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var))
@@ -67,7 +68,8 @@ let call ~summaries actuals formals locals globals_vec (entry, current) =
        State_domain.pp current]
   ;
   let caller_current, state_from_call =
-    State_domain.call ~summaries actuals formals locals globals current
+    State_domain.call ~summaries actuals areturn formals locals globals
+      current
   in
   ((caller_current, caller_current), {state_from_call; caller_entry= entry}))
   |>
@@ -80,10 +82,10 @@ let post locals {caller_entry} (_, current) =
   |>
   [%Trace.retn fun {pf} -> pf "@,%a" pp]
 
-let retn formals {caller_entry; state_from_call} (_, current) =
+let retn formals freturn {caller_entry; state_from_call} (_, current) =
   [%Trace.call fun {pf} -> pf "@,%a" State_domain.pp current]
   ;
-  (caller_entry, State_domain.retn formals state_from_call current)
+  (caller_entry, State_domain.retn formals freturn state_from_call current)
   |>
   [%Trace.retn fun {pf} -> pf "@,%a" pp]
 

sledge/src/symbheap/domain.mli

@@ -15,8 +15,9 @@ val init : Global.t vector -> t
 val join : t -> t -> t
 val is_false : t -> bool
 val exec_assume : t -> Exp.t -> t option
+val exec_kill : t -> Var.t -> t
+val exec_move : t -> Var.t -> Exp.t -> t
 val exec_inst : t -> Llair.inst -> (t, unit) result
-val exec_return : t -> Var.t -> Exp.t -> t
 
 val exec_intrinsic :
      skip_throw:bool
@@ -37,11 +38,11 @@ val create_summary :
   -> State_domain.function_summary * t
 
 val apply_summary : t -> State_domain.function_summary -> t option
-val jump : Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t
 
 val call :
      summaries:bool
   -> Exp.t list
+  -> Var.t option
   -> Var.t list
   -> Var.Set.t
   -> Global.t vector
@@ -49,7 +50,7 @@ val call :
   -> t * from_call
 
 val post : Var.Set.t -> from_call -> t -> t
-val retn : Var.t list -> from_call -> t -> t
+val retn : Var.t list -> Var.t option -> from_call -> t -> t
 val dnf : t -> t list
 
 val resolve_callee :

sledge/src/symbheap/exec.ml

@@ -52,7 +52,6 @@ let assume pre cnd =
   if Sh.is_false post then None else Some post
 
 let kill pre reg = Sh.exists (Set.add Var.Set.empty reg) pre
-let return pre formal exp = Sh.and_ (Exp.eq (Exp.var formal) exp) pre
 
 (* { emp }
  *   rs := es
@@ -670,10 +669,10 @@ let exec_spec pre {xs; foot; sub; ms; post} =
           Format.fprintf fs "%a := " Var.Set.pp ms )
       ms Sh.pp post ;
     assert (
-      let vs = Set.diff (Set.diff foot.Sh.us xs) pre.Sh.us in
+      let vs = Set.diff (Set.diff foot.us xs) pre.us in
       Set.is_empty vs || Trace.fail "unbound foot: {%a}" Var.Set.pp vs ) ;
     assert (
-      let vs = Set.diff (Set.diff post.Sh.us xs) pre.Sh.us in
+      let vs = Set.diff (Set.diff post.us xs) pre.us in
       Set.is_empty vs || Trace.fail "unbound post: {%a}" Var.Set.pp vs )]
   ;
   let foot = Sh.extend_us xs foot in
@@ -698,6 +697,10 @@ let rec exec_specs pre = function
       exec_specs pre specs >>| fun posts -> Sh.or_ post posts
   | [] -> Ok (Sh.false_ pre.us)
 
+let move pre reg exp =
+  exec_spec pre (move_spec pre.us (Vector.of_array [|(reg, exp)|]))
+  |> function Ok post -> post | _ -> assert false
+
 let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result =
  fun pre inst ->
   [%Trace.info
@@ -727,18 +730,18 @@ let intrinsic ~skip_throw :
     -> Var.t
     -> Exp.t list
     -> (Sh.t, unit) result option =
- fun pre result intrinsic actuals ->
+ fun pre areturn intrinsic actuals ->
   [%Trace.info
     "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]"
       (Option.pp "%a := " Var.pp)
-      result Var.pp intrinsic (List.pp ",@ " Exp.pp) (List.rev actuals)
+      areturn Var.pp intrinsic (List.pp ",@ " Exp.pp) (List.rev actuals)
       Sh.pp pre] ;
   let us = pre.us in
   let name =
     let n = Var.name intrinsic in
     match String.index n '.' with None -> n | Some i -> String.prefix n i
   in
-  match (result, name, actuals) with
+  match (areturn, name, actuals) with
   (*
    * cstdlib - memory management
    *)

sledge/src/symbheap/exec.mli

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

sledge/src/symbheap/solver.ml

@@ -61,7 +61,7 @@ let single_existential_occurrence xs exp =
   with Multiple_existential_occurrences -> Many
 
 let special_cases xs = function
-  | Exp.(App {op= App {op= Eq; arg= Var _}; arg= Var _}) as e ->
+  | Exp.App {op= App {op= Eq; arg= Var _}; arg= Var _} as e ->
       if Set.is_subset (Exp.fv e) ~of_:xs then Exp.bool true else e
   | e -> e
 

sledge/src/symbheap/state_domain.ml

@@ -27,7 +27,8 @@ let init globals =
 let join = Sh.or_
 let is_false = Sh.is_false
 let exec_assume = Exec.assume
-let exec_return = Exec.return
+let exec_kill = Exec.kill
+let exec_move = Exec.move
 let exec_inst = Exec.inst
 let exec_intrinsic = Exec.intrinsic
 let dnf = Sh.dnf
@@ -66,46 +67,22 @@ let garbage_collect (q : t) ~wrt =
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
-type from_call = {subst: Var.Subst.t; frame: Sh.t}
+type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.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 temps and
-    fresh vars. *)
-let jump actuals formals ?temps q =
-  [%Trace.call fun {pf} ->
-    pf "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ q: %a@]"
-      (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp)
-      (List.rev formals) Sh.pp q]
-  ;
-  let q', freshen_locals = Sh.freshen q ~wrt:(Var.Set.of_list formals) in
-  let and_eq q formal actual =
-    let actual' = Exp.rename freshen_locals actual in
-    Sh.and_ (Exp.eq (Exp.var formal) actual') q
-  in
-  let and_eqs formals actuals q =
-    List.fold2_exn ~f:and_eq formals actuals ~init:q
-  in
-  ( Option.fold ~f:(Fn.flip Sh.exists) temps
-      ~init:(and_eqs formals actuals q')
-  , {subst= freshen_locals; frame= Sh.emp} )
-  |>
-  [%Trace.retn fun {pf} (q', {subst}) ->
-    pf "@[<hv>subst: %a@ q': %a@]" Var.Subst.pp subst Sh.pp q']
-
 (** 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 actuals formals locals globals q =
+let call ~summaries actuals areturn formals locals globals 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 pp q]
   ;
-  let wrt = Set.add_list formals locals in
-  let q', freshen_locals = Sh.freshen q ~wrt in
+  let q', freshen_locals =
+    Sh.freshen q ~wrt:(Set.add_list formals locals)
+  in
   let and_eq q formal actual =
     let actual' = Exp.rename freshen_locals actual in
     Sh.and_ (Exp.eq (Exp.var formal) actual') q
@@ -116,7 +93,7 @@ let call ~summaries actuals formals locals globals q =
   let q'' = and_eqs formals actuals q' in
   ( if not summaries then
     let q'' = Sh.extend_us locals q'' in
-    (q'', {subst= freshen_locals; frame= Sh.emp})
+    (q'', {areturn; subst= freshen_locals; frame= Sh.emp})
   else
     let formals_set = Var.Set.of_list formals in
     (* Add the formals here to do garbage collection and then get rid of
@@ -134,7 +111,7 @@ let call ~summaries actuals formals locals globals q =
         ~message:"Solver couldn't infer frame of a garbage-collected pre"
     in
     let q'' = Sh.extend_us locals (and_eqs formals actuals foot) in
-    (q'', {subst= freshen_locals; frame}) )
+    (q'', {areturn; subst= freshen_locals; frame}) )
   |>
   [%Trace.retn fun {pf} (q', {subst; frame}) ->
     pf "@[<v>subst: %a@ frame: %a@ q': %a@]" Var.Subst.pp subst pp frame pp
@@ -152,13 +129,19 @@ let post locals q =
 (** 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 {subst; frame} q =
+let retn formals freturn {areturn; subst; frame} q =
   [%Trace.call fun {pf} ->
     pf "@[<v>formals: {@[%a@]}@ subst: %a@ q: %a@ frame: %a@]"
       (List.pp ", " Var.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp
       q pp frame]
   ;
-  let q = Sh.exists (Var.Set.of_list formals) q in
+  let q =
+    match (areturn, freturn) with
+    | Some areturn, Some freturn -> exec_move q areturn (Exp.var freturn)
+    | Some areturn, None -> exec_kill q areturn
+    | _ -> q
+  in
+  let q = Sh.exists (Set.add_list formals (Var.Set.of_option freturn)) q in
   let q = Sh.rename (Var.Subst.invert subst) q in
   Sh.star frame q
   |>
@@ -175,13 +158,12 @@ let pp_function_summary fs {xs; foot; post} =
   Format.fprintf fs "@[<v>xs: @[%a@]@ foot: %a@ post: %a @]" Var.Set.pp xs
     pp foot pp post
 
-let create_summary ~locals ~formals ~entry ~current =
+let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) =
   [%Trace.call fun {pf} ->
     pf "formals %a@ entry: %a@ current: %a" Var.Set.pp formals pp entry pp
-      current]
+      post]
   ;
   let foot = Sh.exists locals entry in
-  let post = Sh.exists locals current in
   let foot, subst = Sh.freshen ~wrt:(Set.union foot.us post.us) foot in
   let restore_formals q =
     Set.fold formals ~init:q ~f:(fun q var ->
@@ -199,7 +181,7 @@ let create_summary ~locals ~formals ~entry ~current =
   let xs_and_formals = Set.union xs formals in
   let foot = Sh.exists (Set.diff foot.us xs_and_formals) foot in
   let post = Sh.exists (Set.diff post.us xs_and_formals) post in
-  let current = Sh.extend_us xs current in
+  let current = Sh.extend_us xs post in
   ({xs; foot; post}, current)
   |>
   [%Trace.retn fun {pf} (fs, _) -> pf "@,%a" pp_function_summary fs]

sledge/src/symbheap/state_domain.mli

@@ -14,8 +14,9 @@ val init : Global.t vector -> t
 val join : t -> t -> t
 val is_false : t -> bool
 val exec_assume : t -> Exp.t -> t option
+val exec_kill : t -> Var.t -> t
+val exec_move : t -> Var.t -> Exp.t -> t
 val exec_inst : t -> Llair.inst -> (t, unit) result
-val exec_return : t -> Var.t -> Exp.t -> t
 
 val exec_intrinsic :
      skip_throw:bool
@@ -27,12 +28,10 @@ val exec_intrinsic :
 
 type from_call [@@deriving compare, equal, sexp]
 
-val jump :
-  Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t * from_call
-
 val call :
      summaries:bool
   -> Exp.t list
+  -> Var.t option
   -> Var.t list
   -> Var.Set.t
   -> Var.Set.t
@@ -54,7 +53,7 @@ val create_summary :
   -> function_summary * t
 
 val post : Var.Set.t -> t -> t
-val retn : Var.t list -> from_call -> t -> t
+val retn : Var.t list -> Var.t option -> from_call -> t -> t
 val dnf : t -> t list
 
 val resolve_callee :