[sledge] Move handling of realpath to the frontend and cli

Summary:
The use of realpath on paths obtained from debug info and the current
working directory is application-usage-specific behavior that does not
belong in the backend library. This diff moves these uses to the
frontend and cli, respectively. Also, the use of realpath in the
frontend is memoized along the same lines as the other frontend
translation functions.

This was also the last use of `core` in the `sledge` library, so the
dependency is moved to `sledge_cli` and `sledge_report`.

Reviewed By: ngorogiannis

Differential Revision: D24989070

fbshipit-source-id: c21b275f5

sledge/cli/frontend.ml

@@ -73,25 +73,34 @@ end)
 let scope_tbl : (int ref * int String.Tbl.t) ScopeTbl.t =
   ScopeTbl.create ~size:32_768 ()
 
+let realpath_tbl = String.Tbl.create ()
+
+let get_debug_loc_directory llv =
+  let+ dir = Llvm.get_debug_loc_directory llv in
+  if String.is_empty dir then dir
+  else
+    String.Tbl.find_or_add realpath_tbl dir ~default:(fun () ->
+        try Core.Filename.realpath dir with Unix.Unix_error _ -> dir )
+
 open struct
   open struct
     let loc_of_global g =
       Loc.mk
-        ?dir:(Llvm.get_debug_loc_directory g)
+        ?dir:(get_debug_loc_directory g)
         ?file:(Llvm.get_debug_loc_filename g)
         ~line:(Llvm.get_debug_loc_line g)
         ?col:None
 
     let loc_of_function f =
       Loc.mk
-        ?dir:(Llvm.get_debug_loc_directory f)
+        ?dir:(get_debug_loc_directory f)
         ?file:(Llvm.get_debug_loc_filename f)
         ~line:(Llvm.get_debug_loc_line f)
         ?col:None
 
     let loc_of_instr i =
       Loc.mk
-        ?dir:(Llvm.get_debug_loc_directory i)
+        ?dir:(get_debug_loc_directory i)
         ?file:(Llvm.get_debug_loc_filename i)
         ~line:(Llvm.get_debug_loc_line i)
         ~col:(Llvm.get_debug_loc_column i)
@@ -1553,6 +1562,7 @@ let check_datalayout llcontext lldatalayout =
    Llvm.dispose_context. *)
 let cleanup llmodule llcontext =
   SymTbl.clear sym_tbl ;
+  String.Tbl.clear realpath_tbl ;
   ScopeTbl.clear scope_tbl ;
   LltypeTbl.clear anon_struct_name ;
   LltypeTbl.clear memo_type ;

sledge/cli/sledge_cli.ml

@@ -47,6 +47,7 @@ let command ~summary ?readme param =
     Trace.init ~colors ?margin ~config () ;
     Option.iter ~f:(Report.init ~append:append_report) report
   in
+  Llair.Loc.root := Some (Core.Filename.realpath (Sys.getcwd ())) ;
   let flush main () = Fun.protect main ~finally:Trace.flush in
   let report main () =
     try main () |> Report.status

sledge/dune

@@ -75,7 +75,7 @@
   (name sledge_report)
   (public_name sledge-report)
   (package sledge)
-  (libraries sledge)
+  (libraries sledge core)
   (flags
    (:standard -open NS -open Sledge))
   (preprocess
@@ -119,8 +119,8 @@
   (name sledge_cli)
   (public_name sledge)
   (package sledge)
-  (libraries apron apron.boxMPQ ctypes ctypes.foreign dune-build-info llvm
-    llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo
+  (libraries apron apron.boxMPQ core ctypes ctypes.foreign dune-build-info
+    llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo
     llvm.linker shexp.process yojson trace nonstdlib sledge model
     smtlib-utils)
   (flags

sledge/nonstdlib/NS.ml

@@ -50,9 +50,3 @@ module String = String
 module Sys = Sys
 module Timer = Timer
 module Z = Z_ext
-
-module Filename = struct
-  include Filename
-
-  let realpath = Core.Filename.realpath
-end

sledge/nonstdlib/NS.mli

@@ -172,12 +172,6 @@ module Out_channel = Stdio.Out_channel
 module Sys = Sys
 module Timer = Timer
 
-module Filename : sig
-  include module type of Filename
-
-  val realpath : string -> string
-end
-
 (** Invariants *)
 module Invariant : sig
   exception Violation of exn * Lexing.position * Sexp.t

sledge/nonstdlib/dune

@@ -6,8 +6,7 @@
 (library
  (name NS)
  (public_name nonstdlib)
- (libraries containers containers-data core core_kernel.fheap iter zarith
-   trace)
+ (libraries containers containers-data core_kernel.fheap iter zarith trace)
  (flags (:standard))
  (preprocess
   (pps ppx_sledge ppx_trace))

sledge/src/llair/loc.ml

@@ -13,25 +13,20 @@ 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 try Filename.realpath dir with Unix.Unix_error _ -> dir
-  in
   {dir; file; line; col}
 
-let root = ref (Filename.realpath (Sys.getcwd ()))
+let root = ref None
 
 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.map_or ~f:Fpath.to_string
-        (Fpath.relativize ~root:(Fpath.v !root) (Fpath.v dir))
-        ~default:dir
+  ( if not (String.is_empty dir) then
+    let dir_file = Fpath.append (Fpath.v dir) (Fpath.v file) in
+    let relative =
+      let* root = !root in
+      let+ relative = Fpath.relativize ~root:(Fpath.v root) dir_file in
+      relative
     in
-    Format.pp_print_string fs dir ;
-    Format.pp_print_string fs Filename.dir_sep ) ;
-  Format.pp_print_string fs file ;
+    Fpath.pp fs (Option.value relative ~default:dir_file) ) ;
   if not (String.is_empty file) then Format.pp_print_char fs ':' ;
   if line > 0 then (
     Format.pp_print_int fs line ;

sledge/src/llair/loc.mli

@@ -14,5 +14,5 @@ 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 *)
+val root : string option ref
+(** Pathnames are printed relative to [root] if set. *)