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. *)