From 58e1732e4f1ba0e955df9a7bff39ad5d3c8c9e0f Mon Sep 17 00:00:00 2001 From: Ryota Kobayashi Date: Sat, 8 Apr 2023 01:35:21 +0900 Subject: [PATCH 1/6] add log --- src/dune | 1 + src/flowInference.ml | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/src/dune b/src/dune index 5f0c7b54..12e50352 100644 --- a/src/dune +++ b/src/dune @@ -50,6 +50,7 @@ (name test) (preprocess (pps ppx_sexp_conv ppx_let with_monad ppx_custom_printf ppx_cast)) (libraries consort yaml) + (flags (-linkall)) (modules Test)) (executable diff --git a/src/flowInference.ml b/src/flowInference.ml index 6ca8a38a..d0f05cd0 100644 --- a/src/flowInference.ml +++ b/src/flowInference.ml @@ -322,9 +322,13 @@ let add_assert_cond assert_cond curr_relation = null flag of [v] happens to be represented as an extension (and thus "beneath") [v]; this requires an annoying special case when doing havoc queries, but *believe me*, it's far more annoying to use another strategy. *) + +let show_map m = OI.GenMap.fold (fun k d rest -> Printf.sprintf !"%{sexp:OI.magic_loc * P.path}" k ^ " -> " ^ string_of_float d ^ ", " ^ rest) m "" + let rec havoc_oracle ctxt ml p = Log.debug ~src:"FLOW-OWN" !"Looking for %{P} @ %{sexp:OI.magic_loc}" p ml; let from_path p_ = + Log.debug ~src:"DEBUG" !"Searching %{sexp:OI.magic_loc * P.path} in %s" (ml,p_) (show_map ctxt.o_hints.OI.gen); let o = OI.GenMap.find (ml,p_) ctxt.o_hints.OI.gen in o = 0.0 in From 364742ad8b0ee370f5ce7771c7b4a24d5e7e32a6 Mon Sep 17 00:00:00 2001 From: artoy Date: Sun, 9 Apr 2023 23:33:40 +0900 Subject: [PATCH 2/6] ignore bin --- src/regnant/.gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/src/regnant/.gitignore b/src/regnant/.gitignore index 5b3aa78e..31fe4301 100644 --- a/src/regnant/.gitignore +++ b/src/regnant/.gitignore @@ -6,3 +6,4 @@ build/ sootOutput/ tmp/ minepump +bin/ \ No newline at end of file From dbb1b89680bc42b7e741d1acc1a5c41207dee1a7 Mon Sep 17 00:00:00 2001 From: artoy Date: Sun, 9 Apr 2023 23:35:53 +0900 Subject: [PATCH 3/6] update gitignore --- src/.gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/src/.gitignore b/src/.gitignore index 4eeaaab6..94b5a0db 100644 --- a/src/.gitignore +++ b/src/.gitignore @@ -1,3 +1,4 @@ *.smt /recursive-tests/ /benchmarks/consort/**/*.class +/tmp/ \ No newline at end of file From f5c15f28b76382144019b079501c56ae8dedf366 Mon Sep 17 00:00:00 2001 From: Ryota Kobayashi Date: Mon, 10 Apr 2023 15:51:24 +0900 Subject: [PATCH 4/6] dump context.save_env --- src/ownershipInference.ml | 13 +++++++++---- src/std.ml | 10 +++++++++- 2 files changed, 18 insertions(+), 5 deletions(-) diff --git a/src/ownershipInference.ml b/src/ownershipInference.ml index 1dbfcab9..78096d84 100644 --- a/src/ownershipInference.ml +++ b/src/ownershipInference.ml @@ -18,6 +18,7 @@ module P = Paths type ownership = OVar of int (** A variable with id int *) | OConst of float (** a constant ownership with the given rational number *) +[@@deriving sexp] type ocon = | Live of ownership (** The ownership must be greater than 0 (only emitted in relaxed mode) *) @@ -35,8 +36,9 @@ type 'a otype_ = | Tuple of 'a otype_ list | TVar of int | Mu of int * 'a otype_ +[@@deriving sexp] -type otype = ownership otype_ +type otype = ownership otype_ [@@deriving sexp] (** For the most part, the ownership and refinement inference passes may be run independently. The only intersection is handling 0 ownership references; when a reference drops to 0 ownership, all refinements must go to top (although we use @@ -110,6 +112,10 @@ type 'a ownership_ops = { the function parameters, and b) the ownership returned back to the function. *) +(** Save the ownership types at each point in the program; only used for debugging *) +type save_env = otype StringMap.t IntMap.t +let sexp_of_save_env = IntMap.sexp_of_t ~v:(StringMap.sexp_of_t ~v:sexp_of_otype) + type context = { relaxed : bool; ovars: int list; @@ -124,9 +130,7 @@ type context = { gamma: otype StringMap.t; theta: (otype RefinementTypes._funtype) StringMap.t; op_record: ownership ownership_ops; - save_env: otype StringMap.t IntMap.t (** Save the ownership types at - each point in the program; - only used for debugging *) + save_env: save_env } type infr_options = bool @@ -838,6 +842,7 @@ let infer ~opts (simple_types,iso) (fn,prog) = in let ctxt = List.fold_left analyze_fn ctxt fn in let (ctxt,_) = process_expr ~output:None prog ctxt in + Log.debug ~src:"DEBUG" !"%{sexp:save_env}" ctxt.save_env; { Result.ocons = ctxt.ocons; Result.ovars = ctxt.ovars; diff --git a/src/std.ml b/src/std.ml index 04a0aa42..01de2669 100644 --- a/src/std.ml +++ b/src/std.ml @@ -18,7 +18,15 @@ module PrintSet(P: sig let to_string e = elements e |> List.map P.to_string |> String.concat ", " |> Printf.sprintf "{%s}" end -module IntMap = Map.Make(Int) +module IntMap = struct + open Sexplib.Std + include Map.Make(Int) + let sexp_of_t (type v_type) ~(v: v_type -> Sexplib.Sexp.t) t = + let sexp_of_v_type = v in + bindings t + |> [%sexp_of: (int * v_type) list] +end + module IntSet = PrintSet(Int) module StringSet = PrintSet(struct include String let to_string = Fun.id end) From abc3fef407bdada57b95beaf536693e933dfff57 Mon Sep 17 00:00:00 2001 From: Ryota Kobayashi Date: Mon, 10 Apr 2023 16:48:58 +0900 Subject: [PATCH 5/6] add log --- src/consort.ml | 3 +++ src/flowInference.ml | 2 +- src/ownershipInference.ml | 8 ++++++-- src/paths.mli | 1 + 4 files changed, 11 insertions(+), 3 deletions(-) diff --git a/src/consort.ml b/src/consort.ml index a0ada1b2..d87b7c02 100644 --- a/src/consort.ml +++ b/src/consort.ml @@ -1,3 +1,5 @@ +open Sexplib.Std + type reason = | Timeout | Unsafe @@ -193,6 +195,7 @@ let consort ~opts file = let simple_res = SimpleChecker.typecheck_prog simple_typing ast in let infer_res = OwnershipInference.infer ~opts simple_res ast in let ownership_res = OwnershipSolver.solve_ownership ~opts infer_res in + Log.debug ~src:"OWNERSHIP" !"Mapping from ownership variable to value: %{sexp:(int * float) list option}" ownership_res; match ownership_res with | None -> Unverified Aliasing | Some o_res -> diff --git a/src/flowInference.ml b/src/flowInference.ml index d0f05cd0..683c9025 100644 --- a/src/flowInference.ml +++ b/src/flowInference.ml @@ -328,7 +328,7 @@ let show_map m = OI.GenMap.fold (fun k d rest -> Printf.sprintf !"%{sexp:OI.magi let rec havoc_oracle ctxt ml p = Log.debug ~src:"FLOW-OWN" !"Looking for %{P} @ %{sexp:OI.magic_loc}" p ml; let from_path p_ = - Log.debug ~src:"DEBUG" !"Searching %{sexp:OI.magic_loc * P.path} in %s" (ml,p_) (show_map ctxt.o_hints.OI.gen); + Log.debug ~src:"FLOW-OWN" !"Searching %{sexp:OI.magic_loc * P.path} in %s" (ml,p_) (show_map ctxt.o_hints.OI.gen); let o = OI.GenMap.find (ml,p_) ctxt.o_hints.OI.gen in o = 0.0 in diff --git a/src/ownershipInference.ml b/src/ownershipInference.ml index 78096d84..9f303b8e 100644 --- a/src/ownershipInference.ml +++ b/src/ownershipInference.ml @@ -112,6 +112,9 @@ type 'a ownership_ops = { the function parameters, and b) the ownership returned back to the function. *) +type gamma = otype StringMap.t +let sexp_of_gamma = StringMap.sexp_of_t ~v:sexp_of_otype + (** Save the ownership types at each point in the program; only used for debugging *) type save_env = otype StringMap.t IntMap.t let sexp_of_save_env = IntMap.sexp_of_t ~v:(StringMap.sexp_of_t ~v:sexp_of_otype) @@ -127,7 +130,7 @@ type context = { v_counter: int; iso: SimpleChecker.SideAnalysis.results; ocons: ocon list; - gamma: otype StringMap.t; + gamma: gamma; theta: (otype RefinementTypes._funtype) StringMap.t; op_record: ownership ownership_ops; save_env: save_env @@ -842,7 +845,8 @@ let infer ~opts (simple_types,iso) (fn,prog) = in let ctxt = List.fold_left analyze_fn ctxt fn in let (ctxt,_) = process_expr ~output:None prog ctxt in - Log.debug ~src:"DEBUG" !"%{sexp:save_env}" ctxt.save_env; + Log.debug ~src:"OWNERSHIP" !"Gamma: %{sexp:gamma}" ctxt.gamma; + Log.debug ~src:"OWNERSHIP" !"Owenrship types at each point: %{sexp:save_env}" ctxt.save_env; { Result.ocons = ctxt.ocons; Result.ovars = ctxt.ovars; diff --git a/src/paths.mli b/src/paths.mli index 94bb5c77..f1bae8fa 100644 --- a/src/paths.mli +++ b/src/paths.mli @@ -28,6 +28,7 @@ type steps = [ private (to protect crucial invariants), but may still be pattern matched over. To make extension O(1), the steps are stored in _reverse_ order in the path representation; i.e., the last step is the head of the list, etc. *) type path = private root * steps list * suff [@@deriving sexp] +(* type path = root * steps list * suff [@@deriving sexp] *) type concr_ap = path [@@deriving sexp] (** Give a string representation of the path, suitable for use as a z3 identifier *) From 227feacd859190843b7725533df4d6256efbf9f0 Mon Sep 17 00:00:00 2001 From: artoy Date: Mon, 17 Apr 2023 15:53:09 +0900 Subject: [PATCH 6/6] add log --- src/flowInference.ml | 3 +++ src/paths.ml | 17 ++++++++++++++--- src/paths.mli | 2 ++ 3 files changed, 19 insertions(+), 3 deletions(-) diff --git a/src/flowInference.ml b/src/flowInference.ml index 683c9025..9794857a 100644 --- a/src/flowInference.ml +++ b/src/flowInference.ml @@ -332,6 +332,7 @@ let rec havoc_oracle ctxt ml p = let o = OI.GenMap.find (ml,p_) ctxt.o_hints.OI.gen in o = 0.0 in + Log.debug ~src:"FLOW-OWN" !"P.tail p is %s" (P.string_of_tail (P.tail p)); match P.tail p with | Some `Deref | Some `Ind @@ -2288,6 +2289,7 @@ let%lq get_iso_at e_id ctxt = labelled return statements) is described by the output argument. *) let rec process_expr ~output (((relation : relation),tyenv) as st) continuation ((e_id,_),e) = + Log.debug ~src:"DEBUG" !"processing %d: %{sexp:raw_exp}" e_id e; (* execute two branches, and then bring their results into sync. analyzes branch 1, b2 analyzes branch 2 *) let scoped_effect ~b1 ~b2 ctxt = (* some trickery here; we abuse the context to record information about the current @@ -2915,6 +2917,7 @@ let analyze_main start_rel main ctxt = let ctxt,_ = process_expr (start_rel,[]) ~output:None None main ctxt in ctxt +(* Take options "~opts", a result of simple type checking "(simple_theta,side_results)", ownership information "o_hints", and AST "(fns, main)" as arguments. *) let infer ~opts (simple_theta,side_results) o_hints (fns,main) = let lift_and_unfold = (fun p -> deep_type_normalization @@ simple_to_fltype p) in let simple_theta = StringMap.map (fun ft -> diff --git a/src/paths.ml b/src/paths.ml index b8be6f0f..f23ce380 100644 --- a/src/paths.ml +++ b/src/paths.ml @@ -143,11 +143,11 @@ let unsafe_get_root (v,_,_) = match v with | Var n -> n | _ -> failwith "Not rooted in var" -let parent (p,suff,fl) = - match suff,fl with +let parent (p,fl,suff) = + match fl,suff with | [],`None -> raise @@ Invalid_argument "at root" | _::t,`None -> (p,t,`None) - | _,_ -> (p,suff,`None) + | _,_ -> (p,fl,`None) let root_at ~child:(r,steps,suff) ~parent:(root,steps2,suff2) = let () = @@ -171,6 +171,17 @@ let tail (_,l,f) = | [],`None -> None | _,(#inh_tags as cr) -> Some cr +let string_of_tail = function + | Some e -> + (match e with + | `Null -> "Null" + | `Deref -> "Deref" + | `Proj i -> Printf.sprintf "Proj %d" i + | `Len -> "Len" + | `Elem -> "Elem" + | `Ind -> "Ind") + | None -> "None" + module PathOrd = struct type t = path let compare = compare diff --git a/src/paths.mli b/src/paths.mli index f1bae8fa..ade34f95 100644 --- a/src/paths.mli +++ b/src/paths.mli @@ -144,6 +144,8 @@ val compare : path -> path -> int *) val tail : path -> [`Null | `Deref | `Proj of int | `Len | `Elem | `Ind ] option +val string_of_tail: [`Null | `Deref | `Proj of int | `Len | `Elem | `Ind ] option -> string + (** A (printable) set of paths *) module PathSet : Std.PRINTSET with type elt = path