From 8fc7e5ef588d627781dcd309967a3bbcd797569e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 16 Nov 2020 12:53:14 -0800 Subject: [PATCH] [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 | 16 +++++++++++++--- sledge/cli/sledge_cli.ml | 1 + sledge/dune | 6 +++--- sledge/nonstdlib/NS.ml | 6 ------ sledge/nonstdlib/NS.mli | 6 ------ sledge/nonstdlib/dune | 3 +-- sledge/src/llair/loc.ml | 21 ++++++++------------- sledge/src/llair/loc.mli | 4 ++-- 8 files changed, 28 insertions(+), 35 deletions(-) diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml index 0ca07835a..e698e3e26 100644 --- a/sledge/cli/frontend.ml +++ b/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 ; diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index 36ef7a8ab..fb1271329 100644 --- a/sledge/cli/sledge_cli.ml +++ b/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 diff --git a/sledge/dune b/sledge/dune index b15e31f48..709c3b5c1 100644 --- a/sledge/dune +++ b/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 diff --git a/sledge/nonstdlib/NS.ml b/sledge/nonstdlib/NS.ml index 1ffc2501e..388fefae0 100644 --- a/sledge/nonstdlib/NS.ml +++ b/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 diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli index b365d23bc..6c6c062f6 100644 --- a/sledge/nonstdlib/NS.mli +++ b/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 diff --git a/sledge/nonstdlib/dune b/sledge/nonstdlib/dune index 9898b26fd..757e97581 100644 --- a/sledge/nonstdlib/dune +++ b/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)) diff --git a/sledge/src/llair/loc.ml b/sledge/src/llair/loc.ml index d642bc3b2..1f93299c2 100644 --- a/sledge/src/llair/loc.ml +++ b/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 ; diff --git a/sledge/src/llair/loc.mli b/sledge/src/llair/loc.mli index 9fd4ba54a..cdd84d9a0 100644 --- a/sledge/src/llair/loc.mli +++ b/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. *)