[inferbo] Reset LatestPrune at the assignment of return variable

Summary:
This diff changes a LatestPrune to use a return variable instead of another local variable, when the function returns a conditional value.  This is a preparation to propagate LatestPrune inter-procedurally in the following diffs.

context: If a function returns a conditional value, e.g. `return x == y`, the LatestPrune value includes a temporary local variable introduced by the SIL translation.  This diff is to avoid propagating the temporary local variables to its caller.

Reviewed By: mbouaziz

Differential Revision: D14321534

fbshipit-source-id: d157bfdd0
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 86861498a5
commit bf096b4d4d

@ -1080,6 +1080,18 @@ module LatestPrune = struct
else V (x, PrunePairs.forget locs ptrue, PrunePairs.forget locs pfalse)
| Top ->
Top
let replace ~from ~to_ x =
match x with
| TrueBranch (x, p) when Pvar.equal x from ->
TrueBranch (to_, p)
| FalseBranch (x, p) when Pvar.equal x from ->
FalseBranch (to_, p)
| V (x, ptrue, pfalse) when Pvar.equal x from ->
V (to_, ptrue, pfalse)
| _ ->
x
end
module Reachability = struct
@ -1352,6 +1364,12 @@ module MemReach = struct
if IntLit.isone i then {m with latest_prune= LatestPrune.TrueBranch (x, p)}
else if IntLit.iszero i then {m with latest_prune= LatestPrune.FalseBranch (x, p)}
else {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune}
| Lvar return, _, _ when Pvar.is_return return -> (
match Alias.find_ret m.alias with
| Some (Simple (Var (ProgramVar pvar))) ->
{m with latest_prune= LatestPrune.replace ~from:pvar ~to_:return m.latest_prune}
| _ ->
m )
| _, _, _ ->
{m with latest_prune= LatestPrune.forget updated_locs m.latest_prune}

Loading…
Cancel
Save