From 453818ff089f14d4ccf887184ba54b0cb568ffe5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 23 Feb 2022 15:31:31 +0100
Subject: Improve pretty-printing of environments by filtering and grouping
 values which don't need to be printed

---
 src/Print.ml       | 68 +++++++++++++++++++++++++++++++++++++++++++++++++++---
 src/ValuesUtils.ml |  2 ++
 src/main.ml        |  2 +-
 3 files changed, 68 insertions(+), 4 deletions(-)

diff --git a/src/Print.ml b/src/Print.ml
index a868963a..27a932be 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -2,6 +2,7 @@ open Identifiers
 module T = Types
 module TU = TypesUtils
 module V = Values
+module VU = ValuesUtils
 module E = Expressions
 module A = CfimAst
 module C = Contexts
@@ -498,10 +499,56 @@ module Contexts = struct
     | Abs abs -> PV.abs_to_string fmt indent indent_incr abs
     | Frame -> failwith "Can't print a Frame element"
 
-  let env_to_string (fmt : PV.value_formatter) (env : C.env) : string =
+  let opt_env_elem_to_string (fmt : PV.value_formatter) (indent : string)
+      (indent_incr : string) (ev : C.env_elem option) : string =
+    match ev with
+    | None -> indent ^ "..."
+    | Some ev -> env_elem_to_string fmt indent indent_incr ev
+
+  (** Filters "dummy" bindings from an environment, to gain space and clarity/
+      See [env_to_string]. *)
+  let filter_env (env : C.env) : C.env_elem option list =
+    (* We filter:
+     * - non-dummy bindings which point to ⊥
+     * - dummy bindings which don't contain loans nor borrows
+     * Note that the first case can sometimes be confusing: we may try to improve
+     * it...
+     *)
+    let filter_elem (ev : C.env_elem) : C.env_elem option =
+      match ev with
+      | Var (Some _, tv) ->
+          (* Not a dummy binding: check if the value is ⊥ *)
+          if VU.is_bottom tv.value then None else Some ev
+      | Var (None, tv) ->
+          (* Dummy binding: check if the value contains borrows or loans *)
+          if VU.borrows_in_value tv || VU.loans_in_value tv then Some ev
+          else None
+      | _ -> Some ev
+    in
+    let env = List.map filter_elem env in
+    (* We collapse groups of filtered values - so that we can print one
+     * single "..." for a whole group of filtered values *)
+    let rec group_filtered (env : C.env_elem option list) :
+        C.env_elem option list =
+      match env with
+      | [] -> []
+      | None :: None :: env -> group_filtered (None :: env)
+      | x :: env -> x :: group_filtered env
+    in
+    group_filtered env
+
+  (** Environments can have a lot of dummy or uninitialized values: [filter]
+      allows to filter them when printing, replacing groups of such bindings with
+      "..." to gain space and clarity.
+   *)
+  let env_to_string (filter : bool) (fmt : PV.value_formatter) (env : C.env) :
+      string =
+    let env =
+      if filter then filter_env env else List.map (fun ev -> Some ev) env
+    in
     "{\n"
     ^ String.concat "\n"
-        (List.map (fun ev -> env_elem_to_string fmt "  " "  " ev) env)
+        (List.map (fun ev -> opt_env_elem_to_string fmt "  " "  " ev) env)
     ^ "\n}"
 
   type ctx_formatter = PV.value_formatter
@@ -595,7 +642,22 @@ module Contexts = struct
     let frames =
       List.mapi
         (fun i f ->
-          "\n# Frame " ^ string_of_int i ^ ":\n" ^ env_to_string fmt f ^ "\n")
+          let num_bindings = ref 0 in
+          let num_dummies = ref 0 in
+          let num_abs = ref 0 in
+          List.iter
+            (fun ev ->
+              match ev with
+              | C.Var (None, _) -> num_dummies := !num_abs + 1
+              | C.Var (Some _, _) -> num_bindings := !num_bindings + 1
+              | C.Abs _ -> num_abs := !num_abs + 1
+              | _ -> raise (Failure "Unreachable"))
+            f;
+          "\n# Frame " ^ string_of_int i ^ ":" ^ "\n- locals: "
+          ^ string_of_int !num_bindings
+          ^ "\n- dummy bindings: " ^ string_of_int !num_dummies
+          ^ "\n- abstractions: " ^ string_of_int !num_abs ^ "\n"
+          ^ env_to_string true fmt f ^ "\n")
         frames
     in
     "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index 623703ee..9aeb15f4 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -20,6 +20,8 @@ let mk_box_value (v : typed_value) : typed_value =
   let box_v = Adt { variant_id = None; field_values = [ v ] } in
   mk_typed_value box_ty box_v
 
+let is_bottom (v : value) : bool = match v with Bottom -> true | _ -> false
+
 let is_symbolic (v : value) : bool =
   match v with Symbolic _ -> true | _ -> false
 
diff --git a/src/main.ml b/src/main.ml
index ac490cbb..4a111a25 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -117,7 +117,7 @@ let () =
 
   (* Set up the logging - for now we use default values - TODO: use the
    * command-line arguments *)
-  Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
+  Easy_logging.Handlers.set_level main_logger_handler EL.Info;
   main_log#set_level EL.Info;
   cfim_of_json_logger#set_level EL.Info;
   pre_passes_log#set_level EL.Info;
-- 
cgit v1.2.3