[sledge] Include all function locals in entry block
[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

facebook/infer,jvillard/infer,facebook/infer,jvillard/infer,facebook/infer,facebook/infer,jvillard/infer,jvillard/infer,facebook/infer,jvillard/infer,jvillard/infer,jvillard/infer,facebook/infer,facebook/infer