From f821ca9634084b4315d0c58a0ff41355fff064c3 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 12 Nov 2020 16:38:36 -0800 Subject: [PATCH] [sledge] Base implementation of localization on atoms instead of vars Summary: The computation of provable reachability through the heap currently uses a set of variables whose values are either determined by the desired roots or by the heap constraints. This requires globals to be treated as variables. In preparation for distinguishing globals from variables, this diff changes the reachability computation to use a set of atomic terms instead of variables. Reviewed By: jvillard Differential Revision: D24886573 fbshipit-source-id: c0e6763b6 --- sledge/src/domain_sh.ml | 47 ++++++++++++++++++----------------------- sledge/src/fol/exp.ml | 2 ++ sledge/src/fol/exp.mli | 2 ++ sledge/src/fol/trm.ml | 7 ++++++ sledge/src/fol/trm.mli | 6 +++++- 5 files changed, 37 insertions(+), 27 deletions(-) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 60fed440c..d3618f0fe 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -73,39 +73,30 @@ let exec_intrinsic ~skip_throw r i es q = (List.map ~f:X.term es) |> Option.map ~f:(Option.map ~f:simplify) -let term_eq_class_has_only_vars_in fvs ctx term = - [%Trace.call fun {pf} -> - pf "@[ fvs: @[%a@] @,ctx: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs - Context.pp ctx Term.pp term] - ; - let term_has_only_vars_in fvs term = - Var.Set.subset (Term.fv term) ~of_:fvs - in - let term_eq_class = Context.class_of ctx term in - List.exists ~f:(term_has_only_vars_in fvs) term_eq_class - |> - [%Trace.retn fun {pf} -> pf "%b"] +let value_determined_by ctx us a = + List.exists (Context.class_of ctx a) ~f:(fun b -> + Term.Set.subset (Term.Set.of_iter (Term.atoms b)) ~of_:us ) -let garbage_collect (q : t) ~wrt = +let garbage_collect (q : Sh.t) ~wrt = [%Trace.call fun {pf} -> pf "%a" pp q] ; (* only support DNF for now *) assert (List.is_empty q.djns) ; let rec all_reachable_vars previous current (q : t) = - if Var.Set.equal previous current then current + if Term.Set.equal previous current then current else let new_set = List.fold q.heap current ~f:(fun seg current -> - if term_eq_class_has_only_vars_in current q.ctx seg.loc then + if value_determined_by q.ctx current seg.loc then List.fold (Context.class_of q.ctx seg.seq) current - ~f:(fun e c -> Var.Set.union c (Term.fv e)) + ~f:(fun e c -> + Term.Set.union c (Term.Set.of_iter (Term.atoms e)) ) else current ) in all_reachable_vars current new_set q in - let r_vars = all_reachable_vars Var.Set.empty wrt q in - Sh.filter_heap q ~f:(fun seg -> - term_eq_class_has_only_vars_in r_vars q.ctx seg.loc ) + let r_vars = all_reachable_vars Term.Set.empty wrt q in + Sh.filter_heap q ~f:(fun seg -> value_determined_by q.ctx r_vars seg.loc) |> [%Trace.retn fun {pf} -> pf "%a" pp] @@ -120,10 +111,14 @@ let localize_entry globals actuals formals freturn locals shadow 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 = X.regs (Llair.Reg.Set.add_option freturn locals) in - let function_summary_pre = - garbage_collect entry - ~wrt:(Var.Set.union formals_set (X.globals globals)) + let wrt = + Term.Set.of_iter + (Iter.append + (Iter.map ~f:(Term.var << X.global) + (Llair.Global.Set.to_iter globals)) + (Iter.map ~f:Term.var (List.to_iter formals))) in + let function_summary_pre = garbage_collect entry ~wrt 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 @@ -332,19 +327,19 @@ let%test_module _ = let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= main} let%expect_test _ = - pp (garbage_collect seg_main ~wrt:(Var.Set.of_list [])) ; + pp (garbage_collect seg_main ~wrt:(Term.Set.of_list [])) ; [%expect {| emp |}] let%expect_test _ = pp (garbage_collect (Sh.star seg_a seg_main) - ~wrt:(Var.Set.of_list [a_])) ; + ~wrt:(Term.Set.of_list [a])) ; [%expect {| %a_2 -[ %b_4, %n_3 )-> ⟨%n_3,%end_5⟩ |}] let%expect_test _ = pp (garbage_collect (Sh.star seg_a seg_main) - ~wrt:(Var.Set.of_list [main_])) ; + ~wrt:(Term.Set.of_list [main])) ; [%expect {| %main_1 -[ %b_4, %n_3 )-> ⟨%n_3,%a_2⟩ @@ -354,7 +349,7 @@ let%test_module _ = pp (garbage_collect (Sh.star seg_cycle seg_main) - ~wrt:(Var.Set.of_list [a_])) ; + ~wrt:(Term.Set.of_list [a])) ; [%expect {| %main_1 -[ %b_4, %n_3 )-> ⟨%n_3,%a_2⟩ diff --git a/sledge/src/fol/exp.ml b/sledge/src/fol/exp.ml index 81f857f11..df24f3434 100644 --- a/sledge/src/fol/exp.ml +++ b/sledge/src/fol/exp.ml @@ -196,6 +196,7 @@ module Term = struct end include T + module Set = Set.Make (T) module Map = Map.Make (T) let ppx = ppx @@ -269,6 +270,7 @@ module Term = struct match e with `Fml f -> iter_f f | #cnd as c -> iter_c c let vars = iter ~f:Trm.vars + let atoms = iter ~f:(fun e -> Iter.map ~f:(fun a -> `Trm a) (Trm.atoms e)) (** Transform *) diff --git a/sledge/src/fol/exp.mli b/sledge/src/fol/exp.mli index a394a949f..4bfba9e70 100644 --- a/sledge/src/fol/exp.mli +++ b/sledge/src/fol/exp.mli @@ -13,6 +13,7 @@ module rec Term : sig val ppx : Var.strength -> t pp val pp : t pp + module Set : Set.S with type elt := t module Map : Map.S with type key := t (** Construct *) @@ -78,6 +79,7 @@ module rec Term : sig (** Traverse *) val vars : t -> Var.t iter + val atoms : t -> t iter (** Transform *) diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index 29f17f921..d00459e33 100644 --- a/sledge/src/fol/trm.ml +++ b/sledge/src/fol/trm.ml @@ -437,6 +437,13 @@ let trms = function Iter.(cons x (cons y (cons z empty))) | Concat xs | Apply (_, xs) -> Iter.of_array xs +let is_atomic = function + | Var _ | Z _ | Q _ | Concat [||] | Apply (_, [||]) -> true + | Arith _ | Splat _ | Sized _ | Extract _ | Concat _ | Apply _ -> false + +let rec atoms e = + if is_atomic e then Iter.return e else Iter.flat_map ~f:atoms (trms e) + (** Query *) let fv e = Var.Set.of_iter (vars e) diff --git a/sledge/src/fol/trm.mli b/sledge/src/fol/trm.mli index 14a0dbe9b..d2d05d002 100644 --- a/sledge/src/fol/trm.mli +++ b/sledge/src/fol/trm.mli @@ -89,8 +89,9 @@ val map : t -> f:(t -> t) -> t val seq_size_exn : t -> t val seq_size : t -> t option -val fv : t -> Var.Set.t +val is_atomic : t -> bool val height : t -> int +val fv : t -> Var.Set.t (** Traverse *) @@ -99,3 +100,6 @@ val trms : t -> t iter val vars : t -> Var.t iter (** The variables that occur in a term. *) + +val atoms : t -> t iter +(** The atomic reflexive-transitive subterms of a term. *)