[sledge] Include all function locals in entry block

Summary:
The backend has an implicit assumption that the entry block's locals
are all the function locals, not just those that happen to appear in
the entry block.

An alternative would be to collect the inverse renaming substitutions
produced by symbolic execution of jumps, which rename variables to
avoid clashes with the destination block's locals. These inverse
substitutions could be applied upon function return, in inverse
order. The complication with this approach is that it would be
necessary to distinguish between a destination local that clashes
because it has the same name as a local of some function higher in the
call stack versus a clash due to being a previous incarnation of the
same local due to a control-flow cycle. Accumulating unrenamings for
the latter case is expensive and pointless, as well as incongrous with
true interprocedural extensions.

So it seems preferable to exploit the asymmetry between the entry
block and others a bit more.

Reviewed By: jvillard

Differential Revision: D14354530

fbshipit-source-id: 815cdb224
master
Josh Berdine 6 years ago committed by Facebook Github Bot
parent d769718192
commit 2896ff15f1

@ -54,8 +54,9 @@ and block =
and cfg = block vector
(* [entry] is not part of [cfg] since it is special in two ways: its params
are the func params, and it cannot be jumped to, only called. *)
(* [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. *)
and func = {name: Global.t; entry: block; cfg: cfg}
let rec sexp_of_jump ({dst; args; retreating} as jmp) =
@ -415,8 +416,12 @@ module Func = struct
| Return _ | Throw _ | Unreachable -> ()
in
resolve_parent_and_jumps entry ;
Vector.iter cfg ~f:resolve_parent_and_jumps ;
func |> check invariant
let locals =
Vector.fold ~init:entry.locals cfg ~f:(fun locals block ->
resolve_parent_and_jumps block ;
Set.union locals block.locals )
in
{func with entry= {entry with locals}} |> check invariant
let mk_undefined ~name ~params =
let entry =

Loading…
Cancel
Save