From 995de071ed1b0d429e51d66c6f9e001b4179d94e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 15 Oct 2019 11:30:49 -0700 Subject: [PATCH] [sledge] Revise Sh_domain handling of function call and return Summary: Fix a bug where the actual return variable was not scoped correctly in cases where its name clashed with a local or formal of the callee. Also comment and simplify to attempt to make more understandable. Reviewed By: bennostein Differential Revision: D17801944 fbshipit-source-id: 286739241 --- sledge/src/llair/term.ml | 3 + sledge/src/symbheap/sh.ml | 5 +- sledge/src/symbheap/sh_domain.ml | 117 ++++++++++++++++++------------- 3 files changed, 77 insertions(+), 48 deletions(-) diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index 415903f76..9dcbad980 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -472,6 +472,9 @@ module Var = struct else ( assert (not (Set.equal vs' vs)) ; Set.add vs' data ) ) + |> check (fun vs' -> + assert (Set.disjoint (domain sub) vs') ; + assert (Set.is_subset (range sub) ~of_:vs') ) end end diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 092f861ff..6a1d21c06 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -276,7 +276,10 @@ let exists xs q = assert ( Set.is_subset xs ~of_:q.us || fail "Sh.exists xs - q.us: %a" Var.Set.pp (Set.diff xs q.us) () ) ; - {q with us= Set.diff q.us xs; xs= Set.union q.xs xs} |> check invariant + ( if Set.is_empty xs then q + else + {q with us= Set.diff q.us xs; xs= Set.union q.xs xs} |> check invariant + ) |> [%Trace.retn fun {pf} -> pf "%a" pp] diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml index b5196c800..44eeb4410 100644 --- a/sledge/src/symbheap/sh_domain.ml +++ b/sledge/src/symbheap/sh_domain.ml @@ -106,6 +106,34 @@ let garbage_collect (q : t) ~wrt = |> [%Trace.retn fun {pf} -> pf "%a" pp] +let and_eqs sub formals actuals q = + let and_eq q formal actual = + let actual' = Term.rename sub actual in + Sh.and_ (Term.eq (Term.var formal) actual') q + in + List.fold2_exn ~f:and_eq formals actuals ~init:q + +let localize_entry globals actuals formals freturn locals subst pre entry = + (* Add the formals here to do garbage collection and then get rid of them *) + let formals_set = Var.Set.of_list formals in + let freturn_locals = Reg.Set.vars (Set.add_option freturn locals) in + let function_summary_pre = + garbage_collect entry + ~wrt:(Set.union formals_set (Reg.Set.vars globals)) + in + [%Trace.info "function summary pre %a" pp function_summary_pre] ; + let foot = Sh.exists formals_set function_summary_pre in + let xs, foot = Sh.bind_exists ~wrt:pre.Sh.us foot in + let frame = + Option.value_exn + (Solver.infer_frame pre xs foot) + ~message:"Solver couldn't infer frame of a garbage-collected pre" + in + let q'' = + Sh.extend_us freturn_locals (and_eqs subst formals actuals foot) + in + (q'', frame) + type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t} [@@deriving compare, equal, sexp] @@ -123,52 +151,35 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q = let actuals = List.map ~f:Exp.term actuals in let areturn = Option.map ~f:Reg.var areturn in let formals = List.map ~f:Reg.var formals in - let locals = Reg.Set.vars (Set.add_option freturn locals) in - let q', freshen_locals = - Sh.freshen q ~wrt:(Set.add_list formals locals) - in - let and_eq q formal actual = - let actual' = Term.rename freshen_locals actual in - Sh.and_ (Term.eq (Term.var formal) actual') q - in - let and_eqs formals actuals q = - List.fold2_exn ~f:and_eq formals actuals ~init:q - in - let q'' = and_eqs formals actuals q' in - ( if not summaries then - let q'' = Sh.extend_us locals q'' in - (q'', {areturn; subst= freshen_locals; frame= Sh.emp}) + let freturn_locals = Reg.Set.vars (Set.add_option freturn locals) in + let modifs = Var.Set.of_option areturn in + (* quantify modifs, their current value will be overwritten and so does + not need to be saved in the freshening renaming *) + let q = Sh.exists modifs q in + (* save current values of shadowed formals and locals with a renaming *) + let q', subst = Sh.freshen q ~wrt:(Set.add_list formals freturn_locals) in + assert (Set.disjoint modifs (Var.Subst.domain subst)) ; + (* pass arguments by conjoining equations between formals and actuals *) + let entry = and_eqs subst formals actuals q' in + (* note: locals and formals are in scope *) + assert (Set.is_subset (Set.add_list formals freturn_locals) ~of_:entry.us) ; + ( if not summaries then (entry, {areturn; subst; frame= Sh.emp}) else - (* Add the formals here to do garbage collection and then get rid of - them *) - let formals_set = Var.Set.of_list formals in - let function_summary_pre = - garbage_collect q'' - ~wrt:(Set.union formals_set (Reg.Set.vars globals)) + let q'', frame = + localize_entry globals actuals formals freturn locals subst q' entry in - [%Trace.info "function summary pre %a" pp function_summary_pre] ; - let foot = Sh.exists formals_set function_summary_pre in - let pre = q' in - let xs, foot = Sh.bind_exists ~wrt:pre.us foot in - let frame = - Option.value_exn - (Solver.infer_frame pre xs foot) - ~message:"Solver couldn't infer frame of a garbage-collected pre" - in - let q'' = Sh.extend_us locals (and_eqs formals actuals foot) in - (q'', {areturn; subst= freshen_locals; frame}) ) + (q'', {areturn; subst; frame}) ) |> - [%Trace.retn fun {pf} (q', {subst; frame}) -> - pf "@[subst: %a@ frame: %a@ q': %a@]" Var.Subst.pp subst pp frame pp - q'] + [%Trace.retn fun {pf} (entry, {subst; frame}) -> + pf "@[subst: %a@ frame: %a@ entry: %a@]" Var.Subst.pp subst pp frame + pp entry] (** Leave scope of locals: existentially quantify locals. *) let post locals _ q = [%Trace.call fun {pf} -> pf "@[locals: {@[%a@]}@ q: %a@]" Reg.Set.pp locals Sh.pp q] ; - let locals = Reg.Set.vars locals in - Sh.exists locals q + Sh.exists (Reg.Set.vars locals) q |> [%Trace.retn fun {pf} -> pf "%a" Sh.pp] @@ -177,21 +188,33 @@ let post locals _ q = restore the shadowed variables. *) let retn formals freturn {areturn; subst; frame} q = [%Trace.call fun {pf} -> - pf "@[formals: {@[%a@]}@ subst: %a@ q: %a@ frame: %a@]" - (List.pp ", " Reg.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp - q pp frame] + pf "@[formals: {@[%a@]}%a%a@ subst: %a@ q: %a@ frame: %a@]" + (List.pp ", " Reg.pp) formals + (Option.pp "@ freturn: %a" Reg.pp) + freturn + (Option.pp "@ areturn: %a" Var.pp) + areturn Var.Subst.pp (Var.Subst.invert subst) pp q pp frame] ; let formals = List.map ~f:Reg.var formals in let freturn = Option.map ~f:Reg.var freturn in - let q = - match (areturn, freturn) with - | Some areturn, Some freturn -> - Exec.move q (Vector.of_ (areturn, Term.var freturn)) - | Some areturn, None -> Exec.kill q areturn - | _ -> q + let inv_subst = Var.Subst.invert subst in + let q, inv_subst = + match areturn with + | Some areturn -> ( + (* reenter scope of areturn just before exiting scope of formals *) + let q = Sh.extend_us (Var.Set.of_ areturn) q in + (* pass return value *) + match freturn with + | Some freturn -> + (Exec.move q (Vector.of_ (areturn, Term.var freturn)), inv_subst) + | None -> (Exec.kill q areturn, inv_subst) ) + | None -> (q, inv_subst) in + (* exit scope of formals *) let q = Sh.exists (Set.add_list formals (Var.Set.of_option freturn)) q in - let q = Sh.rename (Var.Subst.invert subst) q in + (* reinstate shadowed values of locals *) + let q = Sh.rename inv_subst q in + (* reconjoin frame *) Sh.star frame q |> [%Trace.retn fun {pf} -> pf "%a" pp]