From b14580d88bf1878f9a28d82e49b261b636d733f0 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 24 Jun 2019 05:21:50 -0700 Subject: [PATCH] [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 | 84 +++++++++++++++------------------- sledge/src/llair/llair.ml | 37 ++++++++------- sledge/src/llair/llair.mli | 2 +- sledge/src/symbheap/domain.ml | 4 +- sledge/src/symbheap/domain.mli | 4 +- 5 files changed, 58 insertions(+), 73 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index fed120797..cd95bb325 100644 --- a/sledge/src/control.ml +++ b/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,16 +52,14 @@ 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 + | Return {retreating= true; stk= x}, y |x, Return {retreating= true; stk= y} -> compare_as_inlined_location x y | Return {dst= j; stk= x}, Return {dst= k; stk= 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_throw throw + (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) - | Empty -> None - in - pop_return_ Var.Set.empty stk + let rec pop_return = function + | Throw (_, stk) -> pop_return stk + | Return {from_call; dst; stk} -> Some (from_call, dst, stk) + | Empty -> None 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 diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index 87cb49021..62bddc49f 100644 --- a/sledge/src/llair/llair.ml +++ b/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 = diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index 5dfa78fda..b19cf7fef 100644 --- a/sledge/src/llair/llair.mli +++ b/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 diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml index 39fbbdeeb..20b1b10f2 100644 --- a/sledge/src/symbheap/domain.ml +++ b/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) diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli index f9b4cca65..bc4cf0e99 100644 --- a/sledge/src/symbheap/domain.mli +++ b/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