From f160ac8a628c06c5e4366846cc80992dc73ce565 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 4 Sep 2020 13:38:10 -0700
Subject: [PATCH] [sledge] Improve: Print locations with relative pathnames

Reviewed By: ngorogiannis

Differential Revision: D23459523

fbshipit-source-id: 26f99f7c3
---
 sledge/dune                |  2 +-
 sledge/sledge.opam         |  1 +
 sledge/src/llair/global.ml |  5 ++---
 sledge/src/llair/loc.ml    | 17 +++++++++++++----
 sledge/src/llair/loc.mli   |  3 +++
 5 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/sledge/dune b/sledge/dune
index ea1e10e0f..f7a2ffa5c 100644
--- a/sledge/dune
+++ b/sledge/dune
@@ -38,7 +38,7 @@
  (library
   (name llair)
   (public_name sledge.llair)
-  (libraries nonstdlib)
+  (libraries nonstdlib fpath)
   (flags
    (:standard -open NS))
   (preprocess
diff --git a/sledge/sledge.opam b/sledge/sledge.opam
index 77fece1be..fb6ad21d0 100644
--- a/sledge/sledge.opam
+++ b/sledge/sledge.opam
@@ -18,6 +18,7 @@ depends: [
   "ctypes-foreign"
   "dune" {build & >= "2.7"}
   "dune-build-info" {build}
+  "fpath"
   "iter"
   "llvm" {= "8.0.0"}
   "ppx_compare"
diff --git a/sledge/src/llair/global.ml b/sledge/src/llair/global.ml
index c80f6625b..ca98b674e 100644
--- a/sledge/src/llair/global.ml
+++ b/sledge/src/llair/global.ml
@@ -19,10 +19,9 @@ let pp fs {reg} =
   pf "@%s%a" name Reg.pp_demangled reg
 
 let pp_defn fs {reg; init; loc} =
-  Format.fprintf fs "@[<2>%a %a%a%a@]" Typ.pp (Reg.typ reg) Reg.pp reg
-    Loc.pp loc
+  Format.fprintf fs "@[<2>%a %a%a %a@]" Typ.pp (Reg.typ reg) Reg.pp reg
     (Option.pp "@ = @[%a@]" Exp.pp)
-    (Option.map ~f:fst init)
+    (Option.map ~f:fst init) Loc.pp loc
 
 let invariant g =
   let@ () = Invariant.invariant [%here] g [%sexp_of: t] in
diff --git a/sledge/src/llair/loc.ml b/sledge/src/llair/loc.ml
index d69fb2f65..3245b4a39 100644
--- a/sledge/src/llair/loc.ml
+++ b/sledge/src/llair/loc.ml
@@ -13,12 +13,21 @@ type t = {dir: string; file: string; line: int; col: int}
 let none = {dir= ""; file= ""; line= 0; col= 0}
 
 let mk ?(dir = none.dir) ?(file = none.file) ?(col = none.col) ~line =
+  let dir = if String.is_empty dir then dir else Filename.realpath dir in
   {dir; file; line; col}
 
-let pp fs {dir; file; line; col} =
-  Format.pp_print_string fs dir ;
-  if not (String.is_empty dir) then
-    Format.pp_print_string fs Filename.dir_sep ;
+let root = ref (Filename.realpath (Sys.getcwd ()))
+
+let pp fs ({dir; file; line; col} as loc) =
+  if not (equal loc none) then Format.pp_print_string fs "; " ;
+  if not (String.is_empty dir) then (
+    let dir =
+      Option.value_map ~f:Fpath.to_string
+        (Fpath.relativize ~root:(Fpath.v !root) (Fpath.v dir))
+        ~default:dir
+    in
+    Format.pp_print_string fs dir ;
+    Format.pp_print_string fs Filename.dir_sep ) ;
   Format.pp_print_string fs file ;
   if not (String.is_empty file) then Format.pp_print_char fs ':' ;
   if line > 0 then (
diff --git a/sledge/src/llair/loc.mli b/sledge/src/llair/loc.mli
index 9132bf5b0..9fd4ba54a 100644
--- a/sledge/src/llair/loc.mli
+++ b/sledge/src/llair/loc.mli
@@ -13,3 +13,6 @@ type t = {dir: string; file: string; line: int; col: int}
 val pp : t pp
 val none : t
 val mk : ?dir:string -> ?file:string -> ?col:int -> line:int -> t
+
+val root : string ref
+(** pathnames are printed relative to [root], defaults to working directory *)