Suboptimal placement of comment

[msprotz]

Consider the following function (from mlkem):

pub(crate) fn barrett_reduce_element(value: FieldElement) -> FieldElement {
    // hax_debug_assert!(
    //     i32::from(value) > -BARRETT_R && i32::from(value) < BARRETT_R,
    //     "value is {value}"
    // );

    let t = (i32::from(value) * BARRETT_MULTIPLIER) + (BARRETT_R >> 1);
    ...

If I dump what I receive from Charon, the comment is attached to the intermediary (unnamed) value that MIR introduces for i32::from(value) (which internally is just value), or more specifically:

// pseudo-MIR
fn barrett_...(...) {
... lots of variable declarations
i32 t; // this is the user-provided name
... lots of variable declarations
i32 tmp; // internal MIR name
... lots more variable declarations
<<comment attached to the assignment below>>
tmp := value;

I would expect the comment to be attached either to i) the declaration i32 t; or ii) the assignment into t that comes further down (not modeled in the snippet above).

Right now, Eurydice tracks the location of the comment all the way down to C, re-inlines the temporary computations, and produces something unsightly:

  int32_t
  t =
    (int32_t)/*
    hax_debug_assert!(
    i32::from(value) > -BARRETT_R && i32::from(value) < BARRETT_R,
    "value is {value}"
    );
    */
      value

notice how the comment is attached to the inner value, per the original LLBC received from Charon. Thank you!

[msprotz]

initially spotted by @franziskuskiefer

[Nadrieril]

Right now I assign each comment to the first MIR statement that has a matching span. Maybe I should choose the last one instead? I expect that being more precise than that will be hard because I can't inspect the original syntax.

[Nadrieril]

Nevermind I can do better

[sonmarcho]

Another suboptimal placement issue which I believe is linked to the CFG reconstruction:

fn test(
    a : u32,
    b : u32,
) {
    debug_assert!(a < 12);
    // COMMENT 1
    let x = a + b;
    // COMMENT 2
    let y = x * 2;
    // COMMENT 3
}

leads to the following LLBC:

fn test(@1: u32, @2: u32)
{
    ... // variable declarations

    ... // a sequence of storage_live
    <all the comments grouped together>
    ... // the rest of the function body
}

Note that the comments are placed properly if we remove the debug_assert.