Clean up handling of builtin operators

[JonasAlaif]

Summary (Claude generated)

Reworks how the encoder models pointer metadata for references, raw pointers,
and dynamically-sized types, reorganizes the builtin encoders into their own
module, and fixes integer as casts and zero-sized types. Net result: several
previously-failing slice/DST tests now verify, integer-cast overflow behaviour is
modelled correctly, and unsupported constructs report clean errors instead of
panicking. No test regressions vs rewrite-2023.

What's changed

1. Reorganize builtin encoders & model pointer metadata for references

• Splits the monolithic mir_builtin.rs into a builtin/ module (bin_op,
  un_op, cast, metadata, use_cast, use_metadata).
• References and raw pointers now carry pointer metadata (a slice's length, a
  dyn vtable) alongside the address and value in their snapshot. The metadata
  type is derived from the referent as <T as Pointee>::Metadata rather than
  being a separate generic. New ty/kinds/raw.rs models raw pointers (reference-shaped
  but pointee-opaque).
• Threads this metadata through the pure / impure / const encoders and the place
  walkers, including propagation to a DST's unsized tail field.
• Adds support for unsizing coercions to dyn Trait and through mutable references.
• Removes the Len builtins and reports unsupported rvalues as proper
  verification errors instead of panicking or emitting unsound placeholders.

2. Model integer IntToInt casts without a precondition

• as casts between integers never panic, so they are encoded without a
  precondition; out-of-range values wrap into the target type's range via a new
  vir::VirCtxt::get_wrapped_val helper (shared by casts and wrapping arithmetic).
• Drops the cast cases that previously (incorrectly) tripped overflow checking and
  adds a casts/wrapping.rs test.

3. Encode zero-sized types via a dedicated TyZstEnc

• Moves the is_zst flag off the args-agnostic base type (where it caused
  duplicate Viper definitions for the same type used in different generic
  contexts) onto the args-aware decomposition, emitting the canonical s_T_zst
  value on demand from a new ty/zst.rs encoder.

4. Encode FakeForPtrMetadata raw pointers in pure code

• &raw const (fake) (*p) (which carries a pointee's pointer metadata so a later
  PtrMetadata can read it back) is now handled in the pure rvalue encoder,
  so reading slice.len() or indexing a slice inside a specification works.

Test impact

• Fixes several previously-failing slice/DST tests (pure-array-unsize-to-slice,
  issue-721-*, issue-812-*, Dijkstras_algorithm-simpl) and adds new coverage
  (casts/{wrapping,sign_mix,signed,unsigned}, simple-specs/modulo_div_symbolic).
• No known regressions vs rewrite-2023.
• Each commit builds and passes ./x.py fmt-all && ./x.py clippy.

Known limitations / follow-ups

• Some slice operations are still unsupported and report a clean error rather than
  verifying: Rvalue::Len on a slice place, and certain slice indexing in impure
  contexts (slices/slice-len, slice-snap, type_param_slice).
• Cast kinds other than IntToInt / Unsize (e.g. ptr-to-ptr, int-to-float) are
  still todo!().
• Recursive &mut-returning functions with magic wands (e.g. magic-wands/from_nth)
  do not verify: the recursive call is approximated rather than encoded via its own
  contract. The call_labels crash on that path is fixed, but full support needs
  proper recursive method-call encoding (a Viper error without a source position
  currently aborts back-translation in prusti-server).

[JonasAlaif]

@Aurel300 though I did use claude for the second half of this PR (time-wise, I got the AI to logically clean up the commits), I tried to go through all the changes and approve them myself. So should be final and relatively clean for review.

[Aurel300]

Various comments, a lot are cosmetic, the overall code restructuring looks mostly fine.

though I did use claude for the second half of this PR

I strongly wish you would not. Reviewing LLM-assisted code in general expects more of the reviewer than code that was written by yourself (or the review is not done properly). I don't want to trade student project slop for AI slop.

[Aurel300]

Doctests fixed (9)

core_any_doctest_336.rs (was: fail, now: success)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
use std::any::Any;

fn is_string(s: &(dyn Any + Send)) {
    if s.is::<String>() {
        println!("It's a string!");
    } else {
        println!("Not a string...");
    }
}

is_string(&0);
is_string(&"cookie monster".to_string());
}

core_any_doctest_360.rs (was: fail, now: success)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
use std::any::Any;

fn print_if_string(s: &(dyn Any + Send)) {
    if let Some(string) = s.downcast_ref::<String>() {
        println!("It's a string({}): '{}'", string.len(), string);
    } else {
        println!("Not a string...");
    }
}

print_if_string(&0);
print_if_string(&"cookie monster".to_string());
}

core_any_doctest_470.rs (was: fail, now: success)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
use std::any::Any;

fn is_string(s: &(dyn Any + Send + Sync)) {
    if s.is::<String>() {
        println!("It's a string!");
    } else {
        println!("Not a string...");
    }
}

is_string(&0);
is_string(&"cookie monster".to_string());
}

core_any_doctest_494.rs (was: fail, now: success)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
use std::any::Any;

fn print_if_string(s: &(dyn Any + Send + Sync)) {
    if let Some(string) = s.downcast_ref::<String>() {
        println!("It's a string({}): '{}'", string.len(), string);
    } else {
        println!("Not a string...");
    }
}

print_if_string(&0);
print_if_string(&"cookie monster".to_string());
}

core_slice_mod_doctest_2006.rs (was: timeout, now: success)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let v = ['a', 'b', 'c'];

unsafe {
   let (left, right) = v.split_at_unchecked(0);
   assert_eq!(left, []);
   assert_eq!(right, ['a', 'b', 'c']);
}

unsafe {
    let (left, right) = v.split_at_unchecked(2);
    assert_eq!(left, ['a', 'b']);
    assert_eq!(right, ['c']);
}

unsafe {
    let (left, right) = v.split_at_unchecked(3);
    assert_eq!(left, ['a', 'b', 'c']);
    assert_eq!(right, []);
}
}

core_slice_mod_doctest_4499.rs (was: fail, now: success)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let mut slice: &mut [_] = &mut ['a', 'b', 'c', 'd'];
let mut first_three = slice.split_off_mut(..3).unwrap();

assert_eq!(slice, &mut ['d']);
assert_eq!(first_three, &mut ['a', 'b', 'c']);
}

core_slice_mod_doctest_4509.rs (was: fail, now: success)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let mut slice: &mut [_] = &mut ['a', 'b', 'c', 'd'];
let mut tail = slice.split_off_mut(2..).unwrap();

assert_eq!(slice, &mut ['a', 'b']);
assert_eq!(tail, &mut ['c', 'd']);
}

core_slice_mod_doctest_4519.rs (was: fail, now: success)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let mut slice: &mut [_] = &mut ['a', 'b', 'c', 'd'];

assert_eq!(None, slice.split_off_mut(5..));
assert_eq!(None, slice.split_off_mut(..5));
assert_eq!(None, slice.split_off_mut(..=4));
let expected: &mut [_] = &mut ['a', 'b', 'c', 'd'];
assert_eq!(Some(expected), slice.split_off_mut(..4));
}

core_slice_mod_doctest_4806.rs (was: fail, now: success)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
#![feature(substr_range)]


fn main() {
let arr: &[[u32; 2]] = &[[0, 1], [2, 3]];
let flat_arr: &[u32] = arr.as_flattened();

let ok_elm: &[u32; 2] = flat_arr[0..2].try_into().unwrap();
let weird_elm: &[u32; 2] = flat_arr[1..3].try_into().unwrap();

assert_eq!(ok_elm, &[0, 1]);
assert_eq!(weird_elm, &[1, 2]);

assert_eq!(arr.element_offset(ok_elm), Some(0)); // Points to element 0
assert_eq!(arr.element_offset(weird_elm), None);
}

Doctests regressed (29)

alloc_boxed_convert_doctest_237.rs (was: success, now: timeout)

#![allow(unused_variables)]
fn main() {
// create a Box<str> which will be used to create a Box<[u8]>
let boxed: Box<str> = Box::from("hello");
let boxed_str: Box<[u8]> = Box::from(boxed);

// create a &[u8] which will be used to create a Box<[u8]>
let slice: &[u8] = &[104, 101, 108, 108, 111];
let boxed_slice = Box::from(slice);

assert_eq!(boxed_slice, boxed_str);
}

alloc_boxed_doctest_637.rs (was: success, now: fail)

#![allow(unused_variables)]
fn main() {
let mut values = Box::<[u32]>::new_uninit_slice(3);
// Deferred initialization:
values[0].write(1);
values[1].write(2);
values[2].write(3);
let values = unsafe {values.assume_init() };

assert_eq!(*values, [1, 2, 3])
}

alloc_boxed_doctest_662.rs (was: success, now: fail)

#![allow(unused_variables)]
#![feature(new_zeroed_alloc)]


fn main() {
let values = Box::<[u32]>::new_zeroed_slice(3);
let values = unsafe { values.assume_init() };

assert_eq!(*values, [0, 0, 0])
}

alloc_boxed_doctest_772.rs (was: success, now: fail)

#![allow(unused_variables)]
#![feature(allocator_api)]


fn main() {
use std::alloc::System;

let mut values = Box::<[u32], _>::new_uninit_slice_in(3, System);
// Deferred initialization:
values[0].write(1);
values[1].write(2);
values[2].write(3);
let values = unsafe { values.assume_init() };

assert_eq!(*values, [1, 2, 3])
}

alloc_boxed_doctest_802.rs (was: success, now: fail)

#![allow(unused_variables)]
#![feature(allocator_api)]


fn main() {
use std::alloc::System;

let values = Box::<[u32], _>::new_zeroed_slice_in(3, System);
let values = unsafe { values.assume_init() };

assert_eq!(*values, [0, 0, 0])
}

alloc_boxed_doctest_980.rs (was: success, now: fail)

#![allow(unused_variables)]
fn main() {
let mut values = Box::<[u32]>::new_uninit_slice(3);
// Deferred initialization:
values[0].write(1);
values[1].write(2);
values[2].write(3);
let values = unsafe { values.assume_init() };

assert_eq!(*values, [1, 2, 3])
}

alloc_collections_btree_map_doctest_1092.rs (was: success, now: fail)

#![allow(unused_variables)]
fn main() {
use std::collections::BTreeMap;

let mut map = BTreeMap::new();
map.insert(1, "a");
assert_eq!(map.remove(&1), Some("a"));
assert_eq!(map.remove(&1), None);
}

alloc_collections_btree_map_doctest_702.rs (was: success, now: fail)

#![allow(unused_variables)]
fn main() {
use std::collections::BTreeMap;

let mut map = BTreeMap::new();
map.insert(1, "a");
assert_eq!(map.get(&1), Some(&"a"));
assert_eq!(map.get(&2), None);
}

alloc_fmt_doctest_177.rs (was: success, now: fail)

#![allow(unused_variables)]
fn main() {
println!("Hello {:^15}!", format!("{:?}", Some("hi")));
}

alloc_string_doctest_3119.rs (was: success, now: fail)

#![allow(unused_variables)]
fn main() {
use std::borrow::Cow;
assert_eq!(Cow::from("eggplant"), Cow::Borrowed("eggplant"));
}

alloc_string_doctest_3163.rs (was: success, now: fail)

#![allow(unused_variables)]
fn main() {
use std::borrow::Cow;
let s = "eggplant".to_string();
assert_eq!(Cow::from(&s), Cow::Borrowed("eggplant"));
}

core_cell_doctest_1285.rs (was: success, now: timeout)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
use std::cell::RefCell;

let c = RefCell::new(5);
let five = c.take();

assert_eq!(five, 5);
assert_eq!(c.into_inner(), 0);
}

core_convert_mod_doctest_678.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let big_number = 1_000_000_000_000i64;
// Silently truncates `big_number`, requires detecting
// and handling the truncation after the fact.
let smaller_number = big_number as i32;
assert_eq!(smaller_number, -727379968);

// Returns an error because `big_number` is too big to
// fit in an `i32`.
let try_smaller_number = i32::try_from(big_number);
assert!(try_smaller_number.is_err());

// Returns `Ok(3)`.
let try_successful_smaller_number = i32::try_from(3);
assert!(try_successful_smaller_number.is_ok());
}

core_fmt_mod_doctest_694.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
assert_eq!(format_args!("hello").as_str(), Some("hello"));
assert_eq!(format_args!("").as_str(), Some(""));
assert_eq!(format_args!("{:?}", std::env::current_dir()).as_str(), None);
}

core_marker_doctest_1216.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
#![feature(arbitrary_self_types, derive_coerce_pointee)]

fn main() {
use std::marker::CoercePointee;
use std::ops::Deref;

#[derive(CoercePointee)]
#[repr(transparent)]
struct MySmartPointer<T: ?Sized>(Box<T>);

impl<T: ?Sized> Deref for MySmartPointer<T> {
    type Target = T;
    fn deref(&self) -> &T {
        &self.0
    }
}

// You can always define this trait. (as long as you have #![feature(arbitrary_self_types)])
trait MyTrait {
    fn func(self: MySmartPointer<Self>);
}

// But using `dyn MyTrait` requires #[derive(CoercePointee)].
fn call_func(value: MySmartPointer<dyn MyTrait>) {
    value.func();
}
}

core_mem_mod_doctest_1116.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
use std::mem;

enum Foo { A(&'static str), B(i32), C(i32) }

assert_eq!(mem::discriminant(&Foo::A("bar")), mem::discriminant(&Foo::A("baz")));
assert_eq!(mem::discriminant(&Foo::B(1)), mem::discriminant(&Foo::B(2)));
assert_ne!(mem::discriminant(&Foo::B(3)), mem::discriminant(&Foo::C(3)));
}

core_ops_control_flow_doctest_144.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
use std::ops::ControlFlow;

assert!(ControlFlow::<&str, i32>::Break("Stop right there!").is_break());
assert!(!ControlFlow::<&str, i32>::Continue(3).is_break());
}

core_ops_control_flow_doctest_160.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
use std::ops::ControlFlow;

assert!(!ControlFlow::<&str, i32>::Break("Stop right there!").is_continue());
assert!(ControlFlow::<&str, i32>::Continue(3).is_continue());
}

core_ops_control_flow_doctest_177.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
use std::ops::ControlFlow;

assert_eq!(ControlFlow::<&str, i32>::Break("Stop right there!").break_value(), Some("Stop right there!"));
assert_eq!(ControlFlow::<&str, i32>::Continue(3).break_value(), None);
}

core_option_doctest_1320.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let x = Some("foo");
assert_eq!(x.ok_or(0), Ok("foo"));

let x: Option<&str> = None;
assert_eq!(x.ok_or(0), Err(0));
}

core_option_doctest_1470.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let x = Some(2);
let y: Option<&str> = None;
assert_eq!(x.and(y), None);

let x: Option<u32> = None;
let y = Some("foo");
assert_eq!(x.and(y), None);

let x = Some(2);
let y = Some("foo");
assert_eq!(x.and(y), Some("foo"));

let x: Option<u32> = None;
let y: Option<&str> = None;
assert_eq!(x.and(y), None);
}

core_option_doctest_2012.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let x = Some((1, "hi"));
let y = None::<(u8, u32)>;

assert_eq!(x.unzip(), (Some(1), Some("hi")));
assert_eq!(y.unzip(), (None, None));
}

core_result_doctest_1414.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let x: Result<u32, &str> = Ok(2);
let y: Result<&str, &str> = Err("late error");
assert_eq!(x.and(y), Err("late error"));

let x: Result<u32, &str> = Err("early error");
let y: Result<&str, &str> = Ok("foo");
assert_eq!(x.and(y), Err("early error"));

let x: Result<u32, &str> = Err("not a 2");
let y: Result<&str, &str> = Err("late error");
assert_eq!(x.and(y), Err("not a 2"));

let x: Result<u32, &str> = Ok(2);
let y: Result<&str, &str> = Ok("different result type");
assert_eq!(x.and(y), Ok("different result type"));
}

core_result_doctest_1500.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let x: Result<u32, &str> = Ok(2);
let y: Result<u32, &str> = Err("late error");
assert_eq!(x.or(y), Ok(2));

let x: Result<u32, &str> = Err("early error");
let y: Result<u32, &str> = Ok(2);
assert_eq!(x.or(y), Ok(2));

let x: Result<u32, &str> = Err("not a 2");
let y: Result<u32, &str> = Err("late error");
assert_eq!(x.or(y), Err("late error"));

let x: Result<u32, &str> = Ok(2);
let y: Result<u32, &str> = Ok(100);
assert_eq!(x.or(y), Ok(2));
}

core_result_doctest_1817.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let x: Result<Result<&'static str, u32>, u32> = Ok(Ok("hello"));
assert_eq!(Ok("hello"), x.flatten());

let x: Result<Result<&'static str, u32>, u32> = Ok(Err(6));
assert_eq!(Err(6), x.flatten());

let x: Result<Result<&'static str, u32>, u32> = Err(6);
assert_eq!(Err(6), x.flatten());
}

core_result_doctest_718.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let x: Result<u32, &str> = Ok(2);
assert_eq!(x.err(), None);

let x: Result<u32, &str> = Err("Nothing here");
assert_eq!(x.err(), Some("Nothing here"));
}

core_slice_mod_doctest_1380.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
let slice = ['R', 'u', 's', 't'];
let (chunks, []) = slice.as_chunks::<2>() else {
    panic!("slice didn't have even length")
};
assert_eq!(chunks, &[['R', 'u'], ['s', 't']]);
}

core_str_mod_doctest_2407.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
assert_eq!("foo:bar".strip_prefix("foo:"), Some("bar"));
assert_eq!("foo:bar".strip_prefix("bar"), None);
assert_eq!("foofoo".strip_prefix("foo"), Some("foo"));
}

core_str_mod_doctest_2435.rs (was: success, now: fail)

#![allow(dead_code, deprecated, unused_variables, unused_mut)]
fn main() {
assert_eq!("bar:foo".strip_suffix(":foo"), Some("bar"));
assert_eq!("bar:foo".strip_suffix("bar"), None);
assert_eq!("foofoo".strip_suffix("foo"), Some("foo"));
}

[JonasAlaif]

I strongly wish you would not. Reviewing LLM-assisted code in general expects more of the reviewer than code that was written by yourself (or the review is not done properly). I don't want to trade student project slop for AI slop.

I don't agree with this. Yes, it's easy to produce AI slop, but it's also easy to produce human slop. As long as I "review" the code myself before asking for a PR review from you (which I already did with hand-written PRs), I do not think that the quality of the code will be any worse than if I had authored it fully myself (and correspondingly the review effort from you).

I would point to this PR as proof of that. Yes I forgot to go over the comments and so there were many issues there (I'll make sure not to miss that in the future), but if you look at reviewing the code changes themselves then I would not think that it was different to any other PR for you.

Ultimately I see this as a personal decision: do I want to trade faster code iteration at the cost of spending more time going over the LLM generated code myself. Currently, I'm trying it out to see if that's worth it for me, but I don't see this as affecting others. Yes ofc if I got lazy and skipped the self-review step then AI slop PRs would be a problem, but equally I could be lazy and hand-write quick/poor-quality code by hand, which also pushes a lot of the work onto a reviewer.

[JonasAlaif]

Regarding the Doctests regressions, it seems that those are due to fixing the unsoundness: I only clicked onto a few, but for all of those I don't see how we would've been able to prove their assertions beforehand.

[Aurel300]

@JonasAlaif There are a few unresolved conversations still, otherwise as far as I understand, these are follow-up tasks (for separate PRs):

• run rustc (or the runtime checking version of Prusti) on some tests which test that our encoding aligns with the compiler's semantics (Clean up handling of builtin operators #181 (comment))
• separate encoder for encoding expressions related to integer wrapping (Clean up handling of builtin operators #181 (comment))
• update rustc version (then remove encode_len_snap)
• fix extern specs, then see if the mode in MirLocalDefEnc is needed (Clean up handling of builtin operators #181 (comment))
• Add an error flag that ensures an error doesn't go unreported (Clean up handling of builtin operators #181 (comment))
• remove ZST encoder?