From 9b2269b9193bd9cf3a1fb94fbc5b7b3376b22218 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 21 Nov 2024 06:52:57 +0100 Subject: [PATCH 1/7] frontend(cli): output source maps if any When the engine is producing a source map, the CLI now add inline source data to it and save it as a `.map` file. --- cli/subcommands/src/cargo_hax.rs | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index d77a0b50f..ee353799c 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -332,6 +332,27 @@ fn run_engine( std::fs::write(&path, file.contents).unwrap(); wrote = true; } + if let Some(mut sourcemap) = file.sourcemap.clone() { + sourcemap.sourcesContent = sourcemap + .sources + .iter() + .map(PathBuf::from) + .map(|path| { + if path.is_absolute() { + path + } else { + manifest_dir.join(path).to_path_buf() + } + }) + .map(|path| fs::read_to_string(path).ok()) + .collect(); + let f = std::fs::File::create(path.with_file_name(format!( + "{}.map", + path.file_name().unwrap().to_string_lossy() + ))) + .unwrap(); + serde_json::to_writer(std::io::BufWriter::new(f), &sourcemap).unwrap() + } HaxMessage::ProducedFile { path, wrote }.report(message_format, None) } } From 07851ee8795e4acd52a3eae267d777f1942236b1 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 21 Nov 2024 06:54:47 +0100 Subject: [PATCH 2/7] feat(engine/sourcemaps): derive more yojson --- engine/utils/sourcemaps/location.ml | 2 +- engine/utils/sourcemaps/mappings/dual.ml | 2 +- engine/utils/sourcemaps/mappings/mappings.ml | 5 +++-- engine/utils/sourcemaps/mappings/mappings.mli | 8 ++++++-- engine/utils/sourcemaps/mappings/types.ml | 6 ++++-- 5 files changed, 15 insertions(+), 8 deletions(-) diff --git a/engine/utils/sourcemaps/location.ml b/engine/utils/sourcemaps/location.ml index cf2bda904..1086dce76 100644 --- a/engine/utils/sourcemaps/location.ml +++ b/engine/utils/sourcemaps/location.ml @@ -1,6 +1,6 @@ open Prelude -type t = { line : int; col : int } [@@deriving eq] +type t = { line : int; col : int } [@@deriving eq, yojson] let show { line; col } = "(" ^ Int.to_string line ^ ":" ^ Int.to_string col ^ ")" diff --git a/engine/utils/sourcemaps/mappings/dual.ml b/engine/utils/sourcemaps/mappings/dual.ml index 09548fd9f..5161e133f 100644 --- a/engine/utils/sourcemaps/mappings/dual.ml +++ b/engine/utils/sourcemaps/mappings/dual.ml @@ -1,4 +1,4 @@ -type 'a t = { gen : 'a; src : 'a } [@@deriving show, eq] +type 'a t = { gen : 'a; src : 'a } [@@deriving show, eq, yojson] let transpose ~(default : 'a t) ({ gen; src } : 'a option t) : 'a t option = match (gen, src) with diff --git a/engine/utils/sourcemaps/mappings/mappings.ml b/engine/utils/sourcemaps/mappings/mappings.ml index 67fb40347..1ce0612f3 100644 --- a/engine/utils/sourcemaps/mappings/mappings.ml +++ b/engine/utils/sourcemaps/mappings/mappings.ml @@ -2,10 +2,11 @@ open Prelude include Types type range = { start : Location.t; end_ : Location.t option } -[@@deriving show, eq] +[@@deriving show, eq, yojson] module Chunk = struct - type t = { gen : range; src : range; meta : meta } [@@deriving show, eq] + type t = { gen : range; src : range; meta : meta } + [@@deriving show, eq, yojson] let compare (x : t) (y : t) = Location.compare x.gen.start y.gen.start diff --git a/engine/utils/sourcemaps/mappings/mappings.mli b/engine/utils/sourcemaps/mappings/mappings.mli index 7bc0e9d55..44f72a818 100644 --- a/engine/utils/sourcemaps/mappings/mappings.mli +++ b/engine/utils/sourcemaps/mappings/mappings.mli @@ -1,8 +1,12 @@ -type meta = { file_offset : int; name : int option } [@@deriving show, eq] +type meta = { file_offset : int; name : int option } +[@@deriving show, eq, yojson] + type range = { start : Location.t; end_ : Location.t option } +[@@deriving show, eq, yojson] module Chunk : sig - type t = { gen : range; src : range; meta : meta } [@@deriving show, eq] + type t = { gen : range; src : range; meta : meta } + [@@deriving show, eq, yojson] val compare : t -> t -> int end diff --git a/engine/utils/sourcemaps/mappings/types.ml b/engine/utils/sourcemaps/mappings/types.ml index be2cd146e..f670fc023 100644 --- a/engine/utils/sourcemaps/mappings/types.ml +++ b/engine/utils/sourcemaps/mappings/types.ml @@ -1,4 +1,6 @@ open Prelude -type meta = { file_offset : int; name : int option } [@@deriving show, eq] -type point = Location.t Dual.t * meta option [@@deriving show, eq] +type meta = { file_offset : int; name : int option } +[@@deriving show, eq, yojson] + +type point = Location.t Dual.t * meta option [@@deriving show, eq, yojson] From 5586b78b645f1fc20dc947578d138ade52f6cfe8 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 21 Nov 2024 06:55:15 +0100 Subject: [PATCH 3/7] feat(engine/genprinter): helpers around annotated strings --- engine/lib/generic_printer/generic_printer.ml | 25 ++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml index c82312e44..811051c0e 100644 --- a/engine/lib/generic_printer/generic_printer.ml +++ b/engine/lib/generic_printer/generic_printer.ml @@ -74,6 +74,29 @@ module AnnotatedString = struct let to_spanned_strings ((s, annots) : t) : (Ast.span * string) list = Annotation.split_with_string s annots + (** Lifts a string to an annotated list *) + let pure (s : string) : t = (s, []) + + (** Concatenate two annotated strings *) + let concat (x : t) (y : t) : t = + let (xs, xl), (ys, yl) = (x, y) in + let last_x = + let lines = String.split ~on:'\n' xs in + let last_line = List.last lines |> Option.value ~default:"" in + let col, line = (String.length last_line, List.length lines) in + Annotation.{ col; line } + in + let yl = + let f ({ line; col } : Annotation.loc) : Annotation.loc = + { + line = line + last_x.line; + col = (match col with 0 -> col + last_x.col | _ -> col); + } + in + List.map ~f:(f *** Fn.id) yl + in + (xs ^ ys, xl @ yl) + let to_sourcemap : t -> Types.source_map = snd >> List.filter_map ~f:Annotation.to_mapping >> Sourcemaps.Source_maps.mk >> fun ({ @@ -90,7 +113,7 @@ module AnnotatedString = struct { mappings; sourceRoot; sources; sourcesContent; names; version; file } end -(** Helper class that brings imperative span *) +(** Helper class that brings imperative span *) class span_helper : object method span_data : Annotation.t list (** Get the span annotation accumulated while printing *) From 01aad4aab4ab4430f02feb40bb241419971b88e2 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 21 Nov 2024 06:55:47 +0100 Subject: [PATCH 4/7] fix(engine/source maps): file offsets are relative --- engine/utils/sourcemaps/mappings/instruction.ml | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/engine/utils/sourcemaps/mappings/instruction.ml b/engine/utils/sourcemaps/mappings/instruction.ml index 922e1593a..5f36760a9 100644 --- a/engine/utils/sourcemaps/mappings/instruction.ml +++ b/engine/utils/sourcemaps/mappings/instruction.ml @@ -75,23 +75,32 @@ let to_points ?(init = Dual.default Location.default) : t list -> point list = >> snd >> List.rev let from_points : point list -> t list = - List.folding_map ~init:(Dual.default Location.default) - ~f:(fun { src; gen } (x, m) -> + List.folding_map + ~init:(Dual.default Location.default, None) + ~f:(fun ({ src; gen }, m0) (x, m) -> let d = Location.(Dual.{ Dual.src = x.src - src; Dual.gen = x.gen - gen }) in let shift_gen_col = (if Int.(d.gen.line = 0) then d else x).gen.col in + let relative_m = + Option.map m ~f:(fun m -> + match m0 with + | Some m0 -> + { file_offset = m.file_offset - m0.file_offset; name = None } + | None -> m) + in let output = (if Int.(d.gen.line = 0) then [] else [ ShiftGenLinesResetGenCols { lines = d.gen.line } ]) @ - match m with + match relative_m with | Some meta -> [ Full { shift_gen_col; shift_src = d.src; meta } ] | None when Int.(shift_gen_col = 0) -> [] + | _ when Int.(shift_gen_col = 0) -> [] | _ -> [ ShiftGenCols shift_gen_col ] in let x = match m with Some _ -> x | None -> { x with src } in - (x, output)) + ((x, Option.first_some m m0), output)) >> List.concat let%test _ = From 412fdf09ae1b1dd4b0659def1de59a18029b73aa Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 21 Nov 2024 06:56:14 +0100 Subject: [PATCH 5/7] feat(engine/coq): output source maps --- engine/backends/coq/coq/coq_backend.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 7258e44ea..cbf6c6166 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -767,13 +767,16 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list = ~f:(map_first_letter String.uppercase) (fst ns :: snd ns)) in - let contents, _annotations = my_printer#entrypoint_modul items in - Types. - { - path = mod_name ^ ".v"; - contents = hardcoded_coq_headers ^ "\n" ^ contents; - sourcemap = None; - }) + let sourcemap, contents = + let annotated = my_printer#entrypoint_modul items in + let open Generic_printer.AnnotatedString in + let header = pure hardcoded_coq_headers in + let annotated = concat header annotated in + (to_sourcemap annotated, to_string annotated) + in + let sourcemap = Some sourcemap in + let path = mod_name ^ ".v" in + Types.{ path; contents; sourcemap }) open Phase_utils From 33131af62a10e4cda1a145561562aeb7b2209ad8 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 21 Nov 2024 07:22:50 +0100 Subject: [PATCH 6/7] fix(sourcemaps): misc --- cli/subcommands/src/cargo_hax.rs | 2 +- engine/utils/sourcemaps/mappings/instruction.ml | 4 +--- engine/utils/sourcemaps/source_maps.ml | 1 - 3 files changed, 2 insertions(+), 5 deletions(-) diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index ee353799c..2d2f91749 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -341,7 +341,7 @@ fn run_engine( if path.is_absolute() { path } else { - manifest_dir.join(path).to_path_buf() + working_dir.join(path).to_path_buf() } }) .map(|path| fs::read_to_string(path).ok()) diff --git a/engine/utils/sourcemaps/mappings/instruction.ml b/engine/utils/sourcemaps/mappings/instruction.ml index 5f36760a9..767f846c8 100644 --- a/engine/utils/sourcemaps/mappings/instruction.ml +++ b/engine/utils/sourcemaps/mappings/instruction.ml @@ -8,9 +8,7 @@ type t = [@@deriving show { with_path = false }, eq] let encode_one : t -> string * [ `Sep | `NeedsSep ] = function - | ShiftGenLinesResetGenCols { lines } -> - Stdlib.prerr_endline ("lines:::" ^ Int.to_string lines); - (String.make lines ';', `Sep) + | ShiftGenLinesResetGenCols { lines } -> (String.make lines ';', `Sep) | ShiftGenCols n -> (Vql.encode_base64 [ n ], `NeedsSep) | Full { shift_gen_col; shift_src; meta = { file_offset; name } } -> ( Vql.encode_base64 diff --git a/engine/utils/sourcemaps/source_maps.ml b/engine/utils/sourcemaps/source_maps.ml index 6da383baa..96bd09b24 100644 --- a/engine/utils/sourcemaps/source_maps.ml +++ b/engine/utils/sourcemaps/source_maps.ml @@ -45,7 +45,6 @@ let mk ?(file = "") ?(sourceRoot = "") ?(sourcesContent = fun _ -> None) Chunk.{ gen; src; meta } in let mappings = List.map mappings ~f |> List.sort ~compare:Chunk.compare in - Stdlib.prerr_endline @@ [%show: Chunk.t list] mappings; let mappings = Mappings.encode mappings in let sourcesContent = List.map ~f:sourcesContent sources in { mappings; sourceRoot; sourcesContent; sources; names; version = 3; file } From d74e33ae7605f418eee308e0bf0d2f07dc0312fd Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 21 Nov 2024 14:58:31 +0100 Subject: [PATCH 7/7] fix(enigne/coq): missing newline --- engine/backends/coq/coq/coq_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index cbf6c6166..0e03029fc 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -770,7 +770,7 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list = let sourcemap, contents = let annotated = my_printer#entrypoint_modul items in let open Generic_printer.AnnotatedString in - let header = pure hardcoded_coq_headers in + let header = pure (hardcoded_coq_headers ^ "\n") in let annotated = concat header annotated in (to_sourcemap annotated, to_string annotated) in