From 3eee30e946ea68d317cd9e21cc3b661569a6b25e Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Tue, 5 Nov 2024 11:20:54 +0100
Subject: [PATCH 1/2] Fix spans in error reporting with unicode characters.

---
 hax-types/src/diagnostics/report.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/hax-types/src/diagnostics/report.rs b/hax-types/src/diagnostics/report.rs
index cf84959b6..a60c08f48 100644
--- a/hax-types/src/diagnostics/report.rs
+++ b/hax-types/src/diagnostics/report.rs
@@ -12,10 +12,10 @@ pub struct ReportCtx {
 
 /// Translates a line and column position into an absolute offset
 fn compute_offset(src: &str, mut line: usize, col: usize) -> usize {
-    let mut chars = src.chars().enumerate();
+    let mut chars = src.bytes().enumerate();
     while line > 1 {
         while let Some((_offset, ch)) = chars.next() {
-            if ch == '\n' {
+            if ch == b'\n' {
                 break;
             }
         }
@@ -28,7 +28,7 @@ fn compute_offset(src: &str, mut line: usize, col: usize) -> usize {
         .unwrap_or(0);
     let are_col_first_chars_blank = chars
         .take(col)
-        .all(|(_offset, ch)| matches!(ch, ' ' | '\t'));
+        .all(|(_offset, ch)| matches!(ch, b' ' | b'\t'));
     if are_col_first_chars_blank {
         offset
     } else {

From ccff2d9ba31e8fd5e4e94b8228b287d518d1059d Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Tue, 5 Nov 2024 13:23:30 +0100
Subject: [PATCH 2/2] Use miette for offset computation.

---
 Cargo.lock                          | 26 +++++++++++++++++++++++++-
 hax-types/Cargo.toml                |  1 +
 hax-types/src/diagnostics/report.rs | 26 +++-----------------------
 3 files changed, 29 insertions(+), 24 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index c46631bc2..5daeaf35d 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1,6 +1,6 @@
 # This file is automatically @generated by Cargo.
 # It is not intended for manual editing.
-version = 3
+version = 4
 
 [[package]]
 name = "aho-corasick"
@@ -604,6 +604,7 @@ dependencies = [
  "hax-frontend-exporter",
  "hax-frontend-exporter-options",
  "itertools",
+ "miette",
  "path-clean",
  "schemars",
  "serde",
@@ -851,6 +852,29 @@ version = "2.7.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3"
 
+[[package]]
+name = "miette"
+version = "7.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4edc8853320c2a0dab800fbda86253c8938f6ea88510dc92c5f1ed20e794afc1"
+dependencies = [
+ "cfg-if",
+ "miette-derive",
+ "thiserror",
+ "unicode-width",
+]
+
+[[package]]
+name = "miette-derive"
+version = "7.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dcf09caffaac8068c346b6df2a7fc27a177fd20b39421a39ce0a211bde679a6c"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.79",
+]
+
 [[package]]
 name = "mio"
 version = "0.8.11"
diff --git a/hax-types/Cargo.toml b/hax-types/Cargo.toml
index 52d2c981e..caeba72f6 100644
--- a/hax-types/Cargo.toml
+++ b/hax-types/Cargo.toml
@@ -24,6 +24,7 @@ hax-adt-into.workspace = true
 tracing.workspace = true
 serde-brief ={ version = "*", features = ["std", "alloc"]}
 zstd = "0.13.1"
+miette = "7.2.0"
 
 [features]
 rustc = ["hax-frontend-exporter/rustc"]
diff --git a/hax-types/src/diagnostics/report.rs b/hax-types/src/diagnostics/report.rs
index a60c08f48..e1cc96ef5 100644
--- a/hax-types/src/diagnostics/report.rs
+++ b/hax-types/src/diagnostics/report.rs
@@ -1,5 +1,6 @@
 use super::Diagnostics;
 use annotate_snippets::*;
+use miette::SourceOffset;
 use std::collections::HashMap;
 use std::path::{Path, PathBuf};
 use std::rc::Rc;
@@ -11,29 +12,8 @@ pub struct ReportCtx {
 }
 
 /// Translates a line and column position into an absolute offset
-fn compute_offset(src: &str, mut line: usize, col: usize) -> usize {
-    let mut chars = src.bytes().enumerate();
-    while line > 1 {
-        while let Some((_offset, ch)) = chars.next() {
-            if ch == b'\n' {
-                break;
-            }
-        }
-        line -= 1;
-    }
-    let offset = chars
-        .clone()
-        .next()
-        .map(|(offset, _ch)| offset)
-        .unwrap_or(0);
-    let are_col_first_chars_blank = chars
-        .take(col)
-        .all(|(_offset, ch)| matches!(ch, b' ' | b'\t'));
-    if are_col_first_chars_blank {
-        offset
-    } else {
-        offset + col
-    }
+fn compute_offset(src: &str, line: usize, col: usize) -> usize {
+    SourceOffset::from_location(src, line, col).offset() + 1
 }
 
 impl ReportCtx {