From e7e1020e36fa8b3c3e2c42a464df0d59723484d5 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 2 Dec 2020 13:49:29 -0800 Subject: [PATCH] [sledge] Fix scope on return in case actual return clashes with formals Summary: It can happen that the actual return variable, which is the name of the variable in the caller's scope that receives the returned value, clashes with the formals of the callee. The scope of the return formula was wrong in this case, as the actual return was outscoped via existential quantification with the rest of the formals after the return values was passed. Reviewed By: jvillard Differential Revision: D25196727 fbshipit-source-id: 94cf25418 --- sledge/src/domain_sh.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 4a59975a2..73cd7ae5d 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -215,8 +215,13 @@ let retn formals freturn {areturn; unshadow; frame} q = | None -> Exec.kill q areturn ) | None -> q in - (* exit scope of formals *) - let q = Sh.exists (Var.Set.union formals (Var.Set.of_option freturn)) q in + (* exit scope of formals, except for areturn, which move/kill handled *) + let outscoped = + Var.Set.diff + (Var.Set.union formals (Var.Set.of_option freturn)) + (Var.Set.of_option areturn) + in + let q = Sh.exists outscoped q in (* reinstate shadowed values of locals *) let q = Sh.rename unshadow q in (* reconjoin frame *)