Improve unsize error handling

[rgwohlbold]

Currently, unsizing is only supported from arrays to slices, e.g. &[i32; 3] -> &[i32]. Even though #150 tries to improve this situation, it will not make unsizing fully supported. Therefore, it is a good first target to improve user-friendliness of error messages and show partial verification of a file.

This PR makes the following changes:

• Modify MirBuiltinEnc to return a proper error when trying to encode an unsize between unsupported types. This error has sufficient information to implement a proper describe_error method
• Record a Vec<Span> in ErrorEnqueue and ErrorEncode. Pass a Span to encode() and record this span for the error case.
• If require_{ref,dep}_spanned is used, the span is passed to encode(). Otherwise, the dummy span is used.
• Modify program.encoder_errors() to include a span next to the error message.

Test Cases

This yields to the following behavior for unsupported unsize operations:

use prusti_contracts::*;

#[ensures(result == 1)]
fn _boxed() -> i32 {
    let b = Box::new([1]);
    let b2: Box<[i32]> = b;
    b2[0]
}

#[ensures(result == 2)]
fn _boxed2() -> i32 {
    let b = Box::new(1);
    *b
}

Prusti version: 0.3.0, commit d20ecc48c 2026-03-17 14:14:14 UTC, built on 2026-03-20 16:18:29 UTC
Verification of 2 items...
error: [Prusti internal error] Prusti encountered an unexpected internal error
 --> richard_experiments/11b_box_unsizing.rs:6:26
  |
6 |     let b2: Box<[i32]> = b;
  |                          ^
  |
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: unsizing from `std::boxed::Box<[i32; 1]>` to `std::boxed::Box<[i32]>` is not yet supported in Prusti

error: [Prusti: verification error] postcondition might not hold
  --> richard_experiments/11b_box_unsizing.rs:10:11
   |
10 | #[ensures(result == 2)]
   |           ^^^^^^^^^^^

error: aborting due to 2 previous errors

use prusti_contracts::*;

trait MyTrait {}

struct S { x: i32 }

impl MyTrait for S {}

fn _consume(_v: &mut dyn MyTrait) {}

#[ensures(result == 42)]
fn _function() -> i32 {
    let mut s = S { x: 42 };
    consume(&mut s);
    s.x

}

#[ensures(result == 42)]
fn _function2() -> i32 {
    43
}

error: [Prusti internal error] Prusti encountered an unexpected internal error
  --> richard_experiments/44_unsizing.rs:14:13
   |
14 |     consume(&mut s);
   |             ^^^^^^
   |
   = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
   = note: unsizing from `S` to `(dyn MyTrait + '?5)` is not yet supported in Prusti

error: [Prusti: verification error] postcondition might not hold
  --> richard_experiments/44_unsizing.rs:19:11
   |
19 | #[ensures(result == 42)]
   |           ^^^^^^^^^^^^

error: aborting due to 2 previous errors; 3 warnings emitted

[Aurel300]

This seems a bit ad-hoc to do specifically for this one encoder dependency. Maybe deps for the impure encoder should be a wrapper that sets skip_body for any failure?

[rgwohlbold]

I implemented a wrapper, deps_or_skip, with an attribute skip_body which is checked in the visit_* methods.
I had to leave the method deps() as-is due to trait requirements. I replaces deps with deps_or_skip where applicable.

[Aurel300]

(If we do this then) should also be done in visit_terminator, and maybe visit_basic_block_data to just avoid the iteration.

[rgwohlbold]

Done

[Aurel300]

I guess overall I find it strange that we would add error tracking etc to ErrorEnqueue in this situation. Can the unsize encoding not get to an output ref at least, before bailing?

[rgwohlbold]

I guess overall I find it strange that we would add error tracking etc to ErrorEnqueue in this situation. Can the unsize encoding not get to an output ref at least, before bailing?

Unsize does always get to an output ref before bailing. My intention was to make this system generic such that it would also work with other encoders that maybe don't manage to produce an output ref. I'm happy to remove it, if you think it's unnecessary

[rgwohlbold]

Another point: an alternative to the skip_body solution could be to have the visit_* methods return a Result such that we propagate any errors that occur

[Aurel300]

Another point: an alternative to the skip_body solution could be to have the visit_* methods return a Result such that we propagate any errors that occur

Maybe this is nicer -- the reason we didn't do this is because these methods are methods of the mir::visit::Visitor trait. But we also don't use override most of the visit_* methods and the process of iterating a MIR body is simple (iterate over all basic blocks, and for each visit all statements and the terminator, if any). Also, the addition of body invariants will change the MIR impure encoder to walk basic blocks manually, anyway. So, if you want to do this still in this PR, feel free to change this: implement the methods directly instead of in impl Visitor, then also implement the iteration logic in visit_body and visit_basic_block_data.

[rgwohlbold]

Done, the code looks much better imo. It should also extend better to other encoders failing, by switching out unwrap()s for ? in the visitor