From 3dc0c5938ff45d2f21659ec58532850f61f32a80 Mon Sep 17 00:00:00 2001 From: Benno Stein Date: Thu, 12 Sep 2019 08:23:58 -0700 Subject: [PATCH] [sledge] Extract relational logic from Sh_domain, create "domain" module Summary: Generalize the lifting from State_domain (i.e. symbolic heaps) to Sh_domain (i.e. relations over symbolic heaps). Also, extract abstract-domain-related code into its own module/directory. Reviewed By: jberdine Differential Revision: D17319007 fbshipit-source-id: cefbd1393 --- sledge/.gitignore | 1 + sledge/src/{ => domain}/domain_sig.ml | 2 +- sledge/src/domain/dune.in | 20 +++ sledge/src/domain/relation.ml | 128 ++++++++++++++++++ sledge/src/domain/relation.mli | 22 +++ sledge/src/{unit_domain.ml => domain/unit.ml} | 2 +- .../src/{unit_domain.mli => domain/unit.mli} | 0 sledge/src/dune.in | 2 +- sledge/src/sledge.ml | 4 +- sledge/src/symbheap/dune.in | 2 +- sledge/src/symbheap/sh_domain.ml | 111 --------------- sledge/src/symbheap/sh_domain.mli | 57 -------- sledge/src/symbheap/state_domain.ml | 13 +- sledge/src/symbheap/state_domain.mli | 43 +----- 14 files changed, 187 insertions(+), 220 deletions(-) rename sledge/src/{ => domain}/domain_sig.ml (97%) create mode 100644 sledge/src/domain/dune.in create mode 100644 sledge/src/domain/relation.ml create mode 100644 sledge/src/domain/relation.mli rename sledge/src/{unit_domain.ml => domain/unit.ml} (95%) rename sledge/src/{unit_domain.mli => domain/unit.mli} (100%) delete mode 100644 sledge/src/symbheap/sh_domain.ml delete mode 100644 sledge/src/symbheap/sh_domain.mli diff --git a/sledge/.gitignore b/sledge/.gitignore index 933ad7ca6..20c95a932 100644 --- a/sledge/.gitignore +++ b/sledge/.gitignore @@ -8,6 +8,7 @@ /src/llair/dune /src/symbheap/dune /src/trace/dune +/src/domain/dune /src/version.ml /test/*/*.bc /test/*/*.bc.err diff --git a/sledge/src/domain_sig.ml b/sledge/src/domain/domain_sig.ml similarity index 97% rename from sledge/src/domain_sig.ml rename to sledge/src/domain/domain_sig.ml index b400994eb..d4ef69d50 100644 --- a/sledge/src/domain_sig.ml +++ b/sledge/src/domain/domain_sig.ml @@ -7,7 +7,7 @@ (** Abstract Domain *) module type Dom = sig - type t + type t [@@deriving equal, sexp_of] val pp : t pp val report_fmt_thunk : t -> Formatter.t -> unit diff --git a/sledge/src/domain/dune.in b/sledge/src/domain/dune.in new file mode 100644 index 000000000..55e110291 --- /dev/null +++ b/sledge/src/domain/dune.in @@ -0,0 +1,20 @@ +(* -*- tuareg -*- *) +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +let deps = ["import"; "llair_"] + +;; +Jbuild_plugin.V1.send +@@ Format.sprintf {| +(library + (name domain) + %s + (libraries %s)) +|} + (flags `lib deps) + (libraries deps) diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml new file mode 100644 index 000000000..99749cdff --- /dev/null +++ b/sledge/src/domain/relation.ml @@ -0,0 +1,128 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Relational abstract domain, elements of which are interpreted as Hoare + triples over a base state domain *) + +module type State_domain_sig = sig + include Domain_sig.Dom + + val create_summary : + locals:Var.Set.t + -> formals:Var.Set.t + -> entry:t + -> current:t + -> summary * t +end + +module Make (State_domain : State_domain_sig) = struct + type t = State_domain.t * State_domain.t [@@deriving sexp_of, equal] + + let embed b = (b, b) + + let pp fs (entry, curr) = + Format.fprintf fs "@[ entry: %a@;current:%a@]" State_domain.pp + entry State_domain.pp curr + + let report_fmt_thunk (_, curr) fs = State_domain.pp fs curr + let init globals = embed (State_domain.init globals) + + let join (entry_a, current_a) (entry_b, current_b) = + assert (State_domain.equal entry_b entry_a) ; + (entry_a, State_domain.join current_a current_b) + + let is_false (_, curr) = State_domain.is_false curr + + let exec_assume (entry, current) cnd = + match State_domain.exec_assume current cnd with + | Some current -> Some (entry, current) + | None -> None + + let exec_kill (entry, current) reg = + (entry, State_domain.exec_kill current reg) + + let exec_move (entry, current) formal actual = + (entry, State_domain.exec_move current formal actual) + + let exec_inst (entry, current) inst = + match State_domain.exec_inst current inst with + | Ok current -> Ok (entry, current) + | Error e -> Error e + + let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals + = + match + State_domain.exec_intrinsic ~skip_throw current areturn intrinsic + actuals + with + | None -> None + | Some (Ok current) -> Some (Ok (entry, current)) + | Some (Error e) -> Some (Error e) + + type from_call = + {state_from_call: State_domain.from_call; caller_entry: State_domain.t} + [@@deriving sexp_of] + + let call ~summaries actuals areturn formals locals globals_vec + (entry, current) = + let globals = + Var.Set.of_vector + (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var)) + in + ([%Trace.call fun {pf} -> + pf + "@[@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \ + globals: {@[%a@]}@ current: %a@]" + (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp) + (List.rev formals) Var.Set.pp locals Var.Set.pp globals + State_domain.pp current] + ; + let caller_current, state_from_call = + State_domain.call ~summaries actuals areturn formals locals + globals_vec current + in + ( (caller_current, caller_current) + , {state_from_call; caller_entry= entry} )) + |> + [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln] + + let post locals {state_from_call; caller_entry} (_, current) = + [%Trace.call fun {pf} -> pf "locals: %a" Var.Set.pp locals] + ; + (caller_entry, State_domain.post locals state_from_call current) + |> + [%Trace.retn fun {pf} -> pf "@,%a" pp] + + let retn formals freturn {caller_entry; state_from_call} (_, current) = + [%Trace.call fun {pf} -> pf "@,%a" State_domain.pp current] + ; + (caller_entry, State_domain.retn formals freturn state_from_call current) + |> + [%Trace.retn fun {pf} -> pf "@,%a" pp] + + let dnf (entry, current) = + List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current) + + let resolve_callee f e (_, current) = + State_domain.resolve_callee f e current + + type summary = State_domain.summary + + let pp_summary = State_domain.pp_summary + + let create_summary ~locals ~formals (entry, current) = + let fs, current = + State_domain.create_summary ~locals ~formals ~entry ~current + in + (fs, (entry, current)) + + let apply_summary rel summ = + let entry, current = rel in + Option.map + ~f:(fun c -> (entry, c)) + (State_domain.apply_summary current summ) +end diff --git a/sledge/src/domain/relation.mli b/sledge/src/domain/relation.mli new file mode 100644 index 000000000..0e28b3f15 --- /dev/null +++ b/sledge/src/domain/relation.mli @@ -0,0 +1,22 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +(** Relational abstract domain, elements of which are interpreted as Hoare + triples over a base domain *) + +module type State_domain_sig = sig + include Domain_sig.Dom + + val create_summary : + locals:Var.Set.t + -> formals:Var.Set.t + -> entry:t + -> current:t + -> summary * t +end + +module Make (State_domain : State_domain_sig) : Domain_sig.Dom diff --git a/sledge/src/unit_domain.ml b/sledge/src/domain/unit.ml similarity index 95% rename from sledge/src/unit_domain.ml rename to sledge/src/domain/unit.ml index d026ff7d3..8fa8eca83 100644 --- a/sledge/src/unit_domain.ml +++ b/sledge/src/domain/unit.ml @@ -7,7 +7,7 @@ (** "Unit" abstract domain *) -type t = unit +type t = unit [@@deriving equal, sexp_of] let pp fs () = Format.pp_print_string fs "()" let report_fmt_thunk () fs = pp fs () diff --git a/sledge/src/unit_domain.mli b/sledge/src/domain/unit.mli similarity index 100% rename from sledge/src/unit_domain.mli rename to sledge/src/domain/unit.mli diff --git a/sledge/src/dune.in b/sledge/src/dune.in index e9a08233c..a2a3ec62e 100644 --- a/sledge/src/dune.in +++ b/sledge/src/dune.in @@ -6,7 +6,7 @@ * LICENSE file in the root directory of this source tree. *) -let deps = ["import"; "llair_"; "symbheap"; "config"] +let deps = ["import"; "llair_"; "symbheap"; "config"; "domain"] ;; Jbuild_plugin.V1.send diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index 09a0200c1..849df1036 100644 --- a/sledge/src/sledge.ml +++ b/sledge/src/sledge.ml @@ -13,8 +13,8 @@ open Command.Let_syntax type 'a param = 'a Command.Param.t -module Sh_executor = Control.Make (Sh_domain) -module Unit_executor = Control.Make (Unit_domain) +module Sh_executor = Control.Make (Domain.Relation.Make (State_domain)) +module Unit_executor = Control.Make (Domain.Unit) (* reverse application in the Command.Param applicative *) let ( |*> ) : 'a param -> ('a -> 'b) param -> 'b param = diff --git a/sledge/src/symbheap/dune.in b/sledge/src/symbheap/dune.in index 68261513c..083e4c119 100644 --- a/sledge/src/symbheap/dune.in +++ b/sledge/src/symbheap/dune.in @@ -6,7 +6,7 @@ * LICENSE file in the root directory of this source tree. *) -let deps = ["import"; "llair_"] +let deps = ["import"; "llair_"; "domain"] ;; Jbuild_plugin.V1.send diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/src/symbheap/sh_domain.ml deleted file mode 100644 index 195868b8e..000000000 --- a/sledge/src/symbheap/sh_domain.ml +++ /dev/null @@ -1,111 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -(** Abstract domain *) - -type t = State_domain.t * State_domain.t - -let embed q = (q, q) - -let pp fs (entry, current) = - Format.fprintf fs "@[ entry: %a@;current: %a@]" State_domain.pp entry - State_domain.pp current - -let report_fmt_thunk (_, curr) fs = State_domain.pp fs curr -let init globals = embed (State_domain.init globals) - -let join (entry_a, current_a) (entry_b, current_b) = - assert (State_domain.equal entry_b entry_a) ; - (entry_a, State_domain.join current_a current_b) - -let is_false (_, curr) = State_domain.is_false curr - -let exec_assume (entry, current) cnd = - match State_domain.exec_assume current cnd with - | Some current -> Some (entry, current) - | None -> None - -let exec_kill (entry, current) reg = - (entry, State_domain.exec_kill current reg) - -let exec_move (entry, current) formal actual = - (entry, State_domain.exec_move current formal actual) - -let exec_inst (entry, current) inst = - match State_domain.exec_inst current inst with - | Ok current -> Ok (entry, current) - | Error e -> Error e - -let exec_intrinsic ~skip_throw (entry, current) areturn intrinsic actuals = - match - State_domain.exec_intrinsic ~skip_throw current areturn intrinsic - actuals - with - | None -> None - | Some (Ok current) -> Some (Ok (entry, current)) - | Some (Error e) -> Some (Error e) - -type from_call = - {state_from_call: State_domain.from_call; caller_entry: State_domain.t} -[@@deriving sexp_of] - -let call ~summaries actuals areturn formals locals globals_vec - (entry, current) = - let globals = - Var.Set.of_vector - (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var)) - in - ([%Trace.call fun {pf} -> - pf - "@[@[actuals: (@[%a@])@ formals: (@[%a@])@]@ locals: {@[%a@]}@ \ - globals: {@[%a@]}@ current: %a@]" - (List.pp ",@ " Exp.pp) (List.rev actuals) (List.pp ",@ " Var.pp) - (List.rev formals) Var.Set.pp locals Var.Set.pp globals - State_domain.pp current] - ; - let caller_current, state_from_call = - State_domain.call ~summaries actuals areturn formals locals globals - current - in - ((caller_current, caller_current), {state_from_call; caller_entry= entry})) - |> - [%Trace.retn fun {pf} (reln, _) -> pf "@,%a" pp reln] - -let post locals {caller_entry} (_, current) = - [%Trace.call fun {pf} -> pf "locals: %a" Var.Set.pp locals] - ; - (caller_entry, State_domain.post locals current) - |> - [%Trace.retn fun {pf} -> pf "@,%a" pp] - -let retn formals freturn {caller_entry; state_from_call} (_, current) = - [%Trace.call fun {pf} -> pf "@,%a" State_domain.pp current] - ; - (caller_entry, State_domain.retn formals freturn state_from_call current) - |> - [%Trace.retn fun {pf} -> pf "@,%a" pp] - -let dnf (entry, current) = - List.map ~f:(fun c -> (entry, c)) (State_domain.dnf current) - -let resolve_callee f e (_, current) = - State_domain.resolve_callee f e current - -type summary = State_domain.summary - -let pp_summary = State_domain.pp_summary - -let create_summary ~locals ~formals (entry, current) = - let fs, current = - State_domain.create_summary ~locals ~formals ~entry ~current - in - (fs, (entry, current)) - -let apply_summary (entry, current) fs = - Option.map - ~f:(fun c -> (entry, c)) - (State_domain.apply_summary fs current) diff --git a/sledge/src/symbheap/sh_domain.mli b/sledge/src/symbheap/sh_domain.mli deleted file mode 100644 index 37e86c096..000000000 --- a/sledge/src/symbheap/sh_domain.mli +++ /dev/null @@ -1,57 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -(** Abstract domain *) - -type t - -val pp : t pp -val report_fmt_thunk : t -> Formatter.t -> unit -val init : Global.t vector -> t -val join : t -> t -> t -val is_false : t -> bool -val exec_assume : t -> Exp.t -> t option -val exec_kill : t -> Var.t -> t -val exec_move : t -> Var.t -> Exp.t -> t -val exec_inst : t -> Llair.inst -> (t, unit) result - -val exec_intrinsic : - skip_throw:bool - -> t - -> Var.t option - -> Var.t - -> Exp.t list - -> (t, unit) result option - -type from_call [@@deriving sexp_of] -type summary - -val pp_summary : summary pp - -(* formals should include all the parameters of the summary. That is both - formals and globals.*) -val create_summary : - locals:Var.Set.t -> formals:Var.Set.t -> t -> summary * t - -val apply_summary : t -> summary -> t option - -val call : - summaries:bool - -> Exp.t list - -> Var.t option - -> Var.t list - -> Var.Set.t - -> Global.t vector - -> t - -> t * from_call - -val post : Var.Set.t -> from_call -> t -> t -val retn : Var.t list -> Var.t option -> from_call -> t -> t -val dnf : t -> t list - -val resolve_callee : - (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index 17349751c..b5d5e9b91 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/sledge/src/symbheap/state_domain.ml @@ -15,6 +15,7 @@ let pp_simp fs q = Sh.pp fs !q' let pp = pp_simp +let report_fmt_thunk = Fn.flip pp let init globals = Vector.fold globals ~init:Sh.emp ~f:(fun q -> function @@ -73,7 +74,7 @@ type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t} (** Express formula in terms of formals instead of actuals, and enter scope of locals: rename formals to fresh vars in formula and actuals, add equations between each formal and actual, and quantify fresh vars. *) -let call ~summaries actuals areturn formals locals globals q = +let call ~summaries actuals areturn formals locals globals_vec q = [%Trace.call fun {pf} -> pf "@[actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]" @@ -95,9 +96,13 @@ let call ~summaries actuals areturn formals locals globals q = let q'' = Sh.extend_us locals q'' in (q'', {areturn; subst= freshen_locals; frame= Sh.emp}) else - let formals_set = Var.Set.of_list formals in (* Add the formals here to do garbage collection and then get rid of them *) + let formals_set = Var.Set.of_list formals + and globals = + Var.Set.of_vector + (Vector.map globals_vec ~f:(fun (g : Global.t) -> g.var)) + in let function_summary_pre = garbage_collect q'' ~wrt:(Set.union formals_set globals) in @@ -118,7 +123,7 @@ let call ~summaries actuals areturn formals locals globals q = q'] (** Leave scope of locals: existentially quantify locals. *) -let post locals q = +let post locals _ q = [%Trace.call fun {pf} -> pf "@[locals: {@[%a@]}@ q: %a@]" Var.Set.pp locals Sh.pp q] ; @@ -186,7 +191,7 @@ let create_summary ~locals ~formals ~entry ~current:(post : Sh.t) = |> [%Trace.retn fun {pf} (fs, _) -> pf "@,%a" pp_summary fs] -let apply_summary ({xs; foot; post} as fs) q = +let apply_summary q ({xs; foot; post} as fs) = [%Trace.call fun {pf} -> pf "fs: %a@ q: %a" pp_summary fs pp q] ; let xs_in_q = Set.inter xs q.Sh.us in diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli index 82c3cd3a7..3f6e03004 100644 --- a/sledge/src/symbheap/state_domain.mli +++ b/sledge/src/symbheap/state_domain.mli @@ -7,41 +7,7 @@ (** Abstract domain *) -type t [@@deriving equal, sexp_of] - -val pp : t pp -val init : Global.t vector -> t -val join : t -> t -> t -val is_false : t -> bool -val exec_assume : t -> Exp.t -> t option -val exec_kill : t -> Var.t -> t -val exec_move : t -> Var.t -> Exp.t -> t -val exec_inst : t -> Llair.inst -> (t, unit) result - -val exec_intrinsic : - skip_throw:bool - -> t - -> Var.t option - -> Var.t - -> Exp.t list - -> (t, unit) result option - -type from_call [@@deriving compare, equal, sexp] - -val call : - summaries:bool - -> Exp.t list - -> Var.t option - -> Var.t list - -> Var.Set.t - -> Var.Set.t - -> t - -> t * from_call - -type summary = {xs: Var.Set.t; foot: t; post: t} - -val pp_summary : summary pp -val apply_summary : summary -> t -> t option +include Domain_sig.Dom (* formals should include all the parameters of the summary. That is both formals and globals.*) @@ -51,10 +17,3 @@ val create_summary : -> entry:t -> current:t -> summary * t - -val post : Var.Set.t -> t -> t -val retn : Var.t list -> Var.t option -> from_call -> t -> t -val dnf : t -> t list - -val resolve_callee : - (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list