Merge pull request #955 from hacspec/add-regular-comments

feat(frontend): collect regular comments
cryspen · Oct 7, 2024 · a6c36de · a6c36de
2 parents 71c232d + 9f0a5c6
commit a6c36de
Show file tree

Hide file tree

Showing 6 changed files with 63 additions and 0 deletions.
diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs
@@ -263,12 +263,21 @@ impl Callbacks for ExtractionCallbacks {
                 <Body>|| {
                     let (spans, def_ids, impl_infos, items) =
                         convert_thir(&self.clone().into(), self.macro_calls.clone(), tcx);
+                    let files: HashSet<PathBuf> = HashSet::from_iter(
+                        items
+                            .iter()
+                            .flat_map(|item| item.span.filename.to_path().map(|path| path.to_path_buf()))
+                    );
                     let haxmeta: HaxMeta<Body> = HaxMeta {
                         crate_name,
                         cg_metadata,
                         externs,
                         impl_infos,
                         items,
+                        comments: files.into_iter()
+                            .flat_map(|path|hax_frontend_exporter::comments::comments_of_file(path).ok())
+                            .flatten()
+                            .collect(),
                         def_ids,
                     };
                     haxmeta.write(&mut file);

diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs
@@ -453,6 +453,7 @@ fn run_command(options: &Options, haxmeta_files: Vec<EmitHaxMetaMessage>) -> boo
                                 def_ids: haxmeta.def_ids,
                                 impl_infos: haxmeta.impl_infos,
                                 items: haxmeta.items,
+                                comments: haxmeta.comments,
                             },
                         )
                     } else {

diff --git a/frontend/exporter/src/comments.rs b/frontend/exporter/src/comments.rs
@@ -0,0 +1,49 @@
+use crate::prelude::*;
+use rustc_lexer::TokenKind;
+use std::fs;
+
+/// Returns a list of (spanned) comments found in file `path`, or an
+/// error if the file at `path` could not be open.
+pub fn comments_of_file(path: PathBuf) -> std::io::Result<Vec<(Span, String)>> {
+    fn clean_comment(comment: &str) -> &str {
+        let comment = if let Some(comment) = comment.strip_prefix("/*") {
+            comment
+                .strip_suffix("*/")
+                .expect("A comment that starts with `/*` should always ends with `*/`")
+        } else {
+            comment
+                .strip_prefix("//")
+                .expect("A comment has to start with `//` or `/*`")
+        };
+        comment.strip_prefix("!").unwrap_or(comment)
+    }
+    let source = &fs::read_to_string(&path)?;
+
+    let mut comments = vec![];
+    let (mut pos, mut line, mut col) = (0, 0, 0);
+    for token in rustc_lexer::tokenize(source) {
+        let len = token.len as usize;
+        let sub = &source[pos..(pos + len)];
+        let lo = Loc { line, col };
+        line += sub.chars().filter(|c| matches!(c, '\n')).count();
+        pos += len;
+        if lo.line != line {
+            col = sub.chars().rev().take_while(|c| !matches!(c, '\n')).count();
+        } else {
+            col += len;
+        }
+
+        if let TokenKind::LineComment { .. } | TokenKind::BlockComment { .. } = token.kind {
+            if !sub.starts_with("///") && !sub.starts_with("/**") {
+                let span = Span {
+                    lo,
+                    hi: Loc { line, col },
+                    filename: FileName::Real(RealFileName::LocalPath(path.clone())),
+                    rust_span_data: None,
+                };
+                comments.push((span, clean_comment(sub).to_string()));
+            }
+        }
+    }
+    Ok(comments)
+}
diff --git a/frontend/exporter/src/lib.rs b/frontend/exporter/src/lib.rs
@@ -38,11 +38,13 @@ cfg_feature_rustc! {
     extern crate rustc_target;
     extern crate rustc_trait_selection;
     extern crate rustc_type_ir;
+    extern crate rustc_lexer;
 
     mod rustc_utils;
     pub mod state;
     mod utils;
     mod deterministic_hash;
+    pub mod comments;
 }
 
 mod body;

diff --git a/hax-types/src/driver_api.rs b/hax-types/src/driver_api.rs
@@ -27,6 +27,7 @@ pub struct HaxMeta<Body: hax_frontend_exporter::IsBody> {
         hax_frontend_exporter::ImplInfos,
     )>,
     pub def_ids: Vec<hax_frontend_exporter::DefId>,
+    pub comments: Vec<(hax_frontend_exporter::Span, String)>,
 }
 
 impl<Body: hax_frontend_exporter::IsBody> HaxMeta<Body>

diff --git a/hax-types/src/engine_api.rs b/hax-types/src/engine_api.rs
@@ -62,4 +62,5 @@ pub struct WithDefIds<Body: hax_frontend_exporter::IsBody> {
         hax_frontend_exporter::ImplInfos,
     )>,
     pub items: Vec<hax_frontend_exporter::Item<Body>>,
+    pub comments: Vec<(hax_frontend_exporter::Span, String)>,
 }