[sledge] Move locals from blocks to functions

Summary:
The entry block contains all locals of the entire function, as
required by the backend. This makes the manipulation of the locals of
each block redundant.

This diff moves the locals from the entry block to the function
itself, removes the Locals frames of the Control.Stack, and adds a
locals field to Return frames.

This is part cleanup and part preparation for removing the
Control.Stack.

Reviewed By: ngorogiannis

Differential Revision: D15963503

fbshipit-source-id: 523ebc260

sledge/src/control.ml

@@ -16,7 +16,6 @@ module Stack : sig
   type as_inlined_location = t [@@deriving compare, sexp_of]
 
   val empty : t
-  val push_jump : Var.Set.t -> t -> t
 
   val push_call :
        Llair.block
@@ -28,22 +27,21 @@ module Stack : sig
     -> t
     -> t option
 
-  val pop_return :
-    t -> (Var.Set.t * Domain.from_call * Llair.jump * t) option
+  val pop_return : t -> (Domain.from_call * Llair.jump * t) option
 
   val pop_throw :
        t
     -> init:'a
     -> unwind:(Var.t list -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
-    -> (Var.Set.t * Domain.from_call * Llair.jump * t * 'a) option
+    -> (Domain.from_call * Llair.jump * t * 'a) option
 end = struct
   type t =
-    | Locals of Var.Set.t * t
     | Return of
         { retreating: bool
               (** return from a call not known to be nonrecursive *)
         ; dst: Llair.Jump.t
         ; params: Var.t list
+        ; locals: Var.Set.t
         ; from_call: Domain.from_call
         ; stk: t }
     | Throw of Llair.Jump.t * t
@@ -54,15 +52,13 @@ end = struct
 
   (* Treat a stack as a code location in a hypothetical expansion of the
      program where all non-recursive functions have been completely inlined.
-     In particular, this means to compare stacks as if all Locals frames or
-     Return frames for recursive calls had been removed. Additionally, the
-     from_call info in Return frames is ignored. *)
+     In particular, this means to compare stacks as if all Return frames for
+     recursive calls had been removed. Additionally, the from_call info in
+     Return frames is ignored. *)
   let rec compare_as_inlined_location x y =
     if x == y then 0
     else
       match (x, y) with
-      | Locals (_, x), y
-       |x, Locals (_, y)
       | Return {retreating= true; stk= x}, y
        |x, Return {retreating= true; stk= y} ->
           compare_as_inlined_location x y
@@ -81,9 +77,6 @@ end = struct
       | Empty, Empty -> 0
 
   let rec print_abbrev fs = function
-    | Locals (_, s) ->
-        print_abbrev fs s ;
-        Format.pp_print_char fs 'L'
     | Return {retreating= false; stk= s} ->
         print_abbrev fs s ;
         Format.pp_print_char fs 'R'
@@ -99,23 +92,20 @@ end = struct
     Invariant.invariant [%here] s [%sexp_of: t]
     @@ fun () ->
     match s with
-    | Locals _ | Return _ | Throw (_, Return _) | Empty -> ()
+    | Return _ | Throw (_, Return _) | Empty -> ()
     | Throw _ -> fail "malformed stack: %a" print_abbrev s ()
 
   let empty = Empty |> check invariant
 
-  let push_jump lcls stk =
-    (if Set.is_empty lcls then stk else Locals (lcls, stk))
+  let push_return ~retreating dst params locals from_call stk =
+    Return {retreating; dst; params; locals; 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.params; locals} ~retreating ~bound ~return from_call
+  let push_call (entry : Llair.block) ~retreating ~bound ~return from_call
       ?throw stk =
     [%Trace.call fun {pf} -> pf "%a" print_abbrev stk]
     ;
@@ -130,34 +120,28 @@ end = struct
     ( if n > bound then None
     else
       Some
-        (push_jump locals
         (push_throw throw
-              (push_return ~retreating return params from_call stk))) )
+           (push_return ~retreating return entry.params entry.parent.locals
+              from_call stk)) )
     |>
     [%Trace.retn fun {pf} _ ->
       pf "%d of %a on stack" n Llair.Jump.pp return]
 
-  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 {from_call; dst; stk} -> Some (scope, from_call, dst, stk)
+  let rec pop_return = function
+    | Throw (_, stk) -> pop_return stk
+    | Return {from_call; dst; stk} -> Some (from_call, dst, stk)
     | Empty -> None
-    in
-    pop_return_ Var.Set.empty stk
 
   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 {params; from_call; stk} ->
-          pop_throw_ Var.Set.empty (unwind params scope from_call state) stk
+    let rec pop_throw_ state = function
+      | Return {params; locals; from_call; stk} ->
+          pop_throw_ (unwind params locals from_call state) stk
       | Throw (dst, Return {from_call; stk}) ->
-          Some (scope, from_call, dst, stk, state)
+          Some (from_call, dst, stk, state)
       | Empty -> None
       | Throw _ as stk -> violates invariant stk
     in
-    pop_throw_ Var.Set.empty init stk
+    pop_throw_ init stk
 end
 
 module Work : sig
@@ -263,11 +247,10 @@ end = struct
 end
 
 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 ?temps stk state block ({dst; args} as jmp : Llair.jump) =
-  let state = Domain.jump args dst.params dst.locals ?temps state in
+  let state = Domain.jump args dst.params ?temps state in
   exec_goto stk state block jmp
 
 let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
@@ -276,7 +259,8 @@ let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
     pf "%a from %a" Var.pp dst.parent.name.var Var.pp
       return.dst.parent.name.var]
   ;
-  let state, from_call = Domain.call args dst.params dst.locals state in
+  let locals = dst.parent.locals in
+  let state, from_call = Domain.call args dst.params locals state in
   ( match
       Stack.push_call ~bound:opts.bound dst ~retreating ~return from_call
         ?throw stk
@@ -290,7 +274,7 @@ let exec_return stk pre_state (block : Llair.block) exp =
   [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
   ;
   ( match Stack.pop_return stk with
-  | Some (scope, from_call, retn_site, stk) ->
+  | Some (from_call, retn_site, stk) ->
       let freturn = block.parent.freturn in
       let exit_state =
         match (freturn, exp) with
@@ -299,7 +283,9 @@ let exec_return stk pre_state (block : Llair.block) exp =
         | None, None -> pre_state
         | _ -> violates Llair.Func.invariant block.parent
       in
-      let post_state = Domain.post scope from_call exit_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
@@ -319,10 +305,12 @@ let exec_throw stk pre_state (block : Llair.block) exc =
     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) ->
+  | 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 scope from_call exit_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
@@ -441,10 +429,10 @@ let harness : Llair.t -> (int -> Work.t) option =
   List.find_map entry_points ~f:(fun name ->
       Llair.Func.find pgm.functions (Var.program name) )
   |> function
-  | Some {entry= {params= []} as block} ->
+  | Some {locals; entry= {params= []} as block} ->
       Some
         (Work.init
-           (fst (Domain.call [] [] block.locals (Domain.init pgm.globals)))
+           (fst (Domain.call [] [] locals (Domain.init pgm.globals)))
            block)
   | _ -> None
 

sledge/src/llair/llair.ml

@@ -45,7 +45,6 @@ and term =
 and block =
   { lbl: label
   ; params: Var.t list
-  ; locals: Var.Set.t
   ; cmnd: cmnd
   ; term: term
   ; mutable parent: func
@@ -54,10 +53,10 @@ 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, its locals are all the locals in it plus the
-   cfg, and it cannot be jumped to, only called. *)
+   params are the func params, and it cannot be jumped to, only called. *)
 and func =
   { name: Global.t
+  ; locals: Var.Set.t
   ; entry: block
   ; cfg: cfg
   ; freturn: Var.t option
@@ -94,11 +93,10 @@ let sexp_of_term = function
   | Throw {exc; loc} -> sexp_ctor "Throw" [%sexp {exc: Exp.t; loc: Loc.t}]
   | Unreachable -> Sexp.Atom "Unreachable"
 
-let sexp_of_block {lbl; params; locals; cmnd; term; parent; sort_index} =
+let sexp_of_block {lbl; params; cmnd; term; parent; sort_index} =
   [%sexp
     { lbl: label
     ; params: Var.t list
-    ; locals: Var.Set.t
     ; cmnd: cmnd
     ; term: term
     ; parent: Var.t = parent.name.var
@@ -106,8 +104,8 @@ let sexp_of_block {lbl; params; locals; cmnd; term; parent; sort_index} =
 
 let sexp_of_cfg v = [%sexp_of: block vector] v
 
-let sexp_of_func {name; entry; cfg} =
-  [%sexp {name: Global.t; entry: block; cfg: cfg}]
+let sexp_of_func {name; locals; entry; cfg} =
+  [%sexp {name: Global.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
@@ -199,7 +197,6 @@ let pp_block fs {lbl; params; cmnd; term; sort_index} =
 let rec dummy_block =
   { lbl= "dummy"
   ; params= []
-  ; locals= Var.Set.empty
   ; cmnd= Vector.empty
   ; term= Unreachable
   ; parent= dummy_func
@@ -209,6 +206,7 @@ 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
+  ; locals= Var.Set.empty
   ; entry= dummy_block
   ; cfg= Vector.empty
   ; freturn= None
@@ -354,12 +352,8 @@ module Block = struct
     assert (not (List.contains_dup blk.params ~compare:Var.compare))
 
   let mk ~lbl ~params ~cmnd ~term =
-    let locals =
-      Vector.fold_right ~f:Inst.union_locals cmnd ~init:Var.Set.empty
-    in
     { lbl
     ; params
-    ; locals
     ; cmnd
     ; term
     ; parent= dummy_block.parent
@@ -403,7 +397,7 @@ module Func = struct
     Invariant.invariant [%here] func [%sexp_of: t]
     @@ fun () ->
     assert (func == func.entry.parent) ;
-    let {name= {typ}; cfg} = func in
+    let {name= {typ}; entry; cfg} = func in
     match typ with
     | Pointer {elt= Function {return}} ->
         assert (
@@ -413,8 +407,8 @@ module Func = struct
         assert (
           not
             (List.contains_dup
-               (List.concat_map (Vector.to_list cfg) ~f:(fun {params} ->
-                    params ))
+               (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)
@@ -424,10 +418,15 @@ module Func = struct
 
   let mk ~(name : Global.t) ~entry ~cfg =
     let locals =
-      Vector.fold ~init:entry.locals cfg ~f:(fun locals block ->
-          Set.add_list block.params (Set.union locals block.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)
+      in
+      let init = locals_cmnd Var.Set.empty entry.cmnd in
+      Vector.fold ~f:locals_block cfg ~init
     in
-    let entry = {entry with locals} in
     let wrt = Set.add_list entry.params locals in
     let freturn, wrt =
       match name.typ with
@@ -437,7 +436,7 @@ module Func = struct
       | _ -> (None, wrt)
     in
     let fthrow, _ = Var.fresh "fthrow" ~wrt in
-    let func = {name; entry; cfg; freturn; fthrow} in
+    let func = {name; locals; entry; cfg; freturn; fthrow} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
       let lookup cfg lbl : block =

sledge/src/llair/llair.mli

@@ -95,7 +95,6 @@ and term = private
 and block = private
   { lbl: label
   ; params: Var.t list  (** Formal parameters, first-param-last stack *)
-  ; locals: Var.Set.t  (** Local variables *)
   ; cmnd: cmnd
   ; term: term
   ; mutable parent: func
@@ -109,6 +108,7 @@ and cfg
     parameters are the function parameters. *)
 and func = private
   { name: Global.t
+  ; locals: Var.Set.t  (** Local variables *)
   ; entry: block
   ; cfg: cfg
   ; freturn: Var.t option

sledge/src/symbheap/domain.ml

@@ -44,9 +44,9 @@ type from_call =
   {state_from_call: State_domain.from_call; caller_entry: State_domain.t}
 [@@deriving sexp_of]
 
-let jump actuals formals locals ?temps (entry, current) =
+let jump actuals formals ?temps (entry, current) =
   let current, _ =
-    State_domain.call actuals formals locals ?temps current
+    State_domain.call actuals formals Var.Set.empty ?temps current
   in
   (entry, current)
 

sledge/src/symbheap/domain.mli

@@ -21,9 +21,7 @@ val exec_intrinsic :
 
 type from_call [@@deriving sexp_of]
 
-val jump :
-  Exp.t list -> Var.t list -> Var.Set.t -> ?temps:Var.Set.t -> t -> t
-
+val jump : Exp.t list -> Var.t list -> ?temps:Var.Set.t -> t -> t
 val call : Exp.t list -> Var.t list -> Var.Set.t -> t -> t * from_call
 val post : Var.Set.t -> from_call -> t -> t
 val retn : Var.t list -> from_call -> t -> t