Polymorphism

[N1ark]

Add support for some notion of polymorphic testing to Soteria Rust!

What's supported

We support symbolic tests that have generic arguments, e.g.:

fn with_vec<T>() {
    let my_vec: Vec<T> = Vec::with_capacity(10);
    if mem::size_of::<T>() == 0 {
        assert!(my_vec.capacity() == usize::MAX);
    } else {
        assert!(my_vec.capacity() == 10);
    }
}

In this case we generate a type T of unknown size and alignment. Currently I bound the size to the range [0; 1024[, to avoid detecting invalid layouts due to types having extremely large sizes, since that's not the point. I also limit the alignment to 1, to make generated layouts simpler, otherwise layout size expressions grow very (very) large from trying to calculate padding. If you have a clever solution let me know; this can also just be enabled through a flag maybe.

We support creating nondeterministic T variables, and reading/storing them, though that's about it.

let mut x: T = rusteria::nondet();
let mut y: T = x;
if std::mem::size_of::<T>() == 0 {
    let ptr = std::ptr::dangling::<T>();
    let my_t: T = unsafe { ptr.read() };
    std::mem::drop(my_t);
} else {
    let mut z: T = rusteria::nondet();
    x = z;
    z = y;
}

We also support symbolic tests that have const generic arguments, e.g.:

fn test_poly_const_generic2<const C: usize>() {
    match C {
        0 => {}
        1 => {}
        8 => {}
        15 => {}
        255 => {}
        _ => {}
    }
}

In this case we generate a nondet value of the constant's type. Note that the constant can be used in the body, but not in types, e.g. fn generic_array<const C: usize>() { let x = [0; C] } currently doesn't work, since we would need symbolic arrays.

What's not supported

This is a cool first step but is still quite limited; the following features are currently unsupported:

• Reasoning about trait bounds of generic arguments. If we encounter a method call for an unknown polymorphic type, an unimplemented warning is raised.
• Using constant generics in types (e.g. [u8; T])
• Splitting, merging, or reading the bytes of polymorphic values. They are blocks of size size_of::<T> and currently cannot be split or manipulated in any way.
• Running in polymorphic mode (with the --poly flag) with Obol. Obol is for monomorphic analysis only, and if you want to use polymorphic analysis you must have --frontend charon.

Implementation details

We keep track of the generic environment we're in by equipping Rustsymex with a substitution that is carried around. We also track a map of generic layouts in Rustsymex, since symbolic information cannot be stored globally with the rest of the layouts.
We keep track of const generics in State (due to some module dependency problems around Rust_val and Sptr). It keeps a mapping of constant ID to Rust_val, and generates a fresh nondet variable on the first access of each const. (Layouts works similarly, only computing generic layouts on the first access).

The one ugly thing I had to do is that whenever I had a Charon.Types.fun_decl_ref (e.g. State.declare_fn for fn pointers), I now have a new ADT Fun_kind.t = | Real of fun_decl_ref | Synthetic of synth_fn where for now synth_fn is only GenericDropInPlace. This is because in the function resolution step, there are cases where we want to emulate a trait method into a function that doesn't exist.

We do this for core::marker::Destruct::drop_in_place, i.e. the drop glue of a droppable type. If the trait clause associated to Destruct is for a generic type, the function Synthetic GenericDropInPlace is used, which is a no-op. This is an approximation but is needed to allow values of type T, since this function is called at the end of their scope.

Review details

There are a few PRs dedicated to cleaning up dependencies / moving functions around; in particular:

• cf5bd4f removed the layout.ml -> rust_val.ml dependency, by moving functions to encoder.ml
• 59bbb42 removes the rust_state_m.ml -> state_intf.ml dependency by redefining all thats needed
• 5384685 removes the layout_common.ml -> rust_val.ml dependency, by moving stuff to charon_util.ml
• 8fdd07a moves the definitions of Layout.t etc. to layout_common.ml, to allow for the layout type to be used in Rustsymex (for polymorphic layouts to be threaded through)

Feel free to review them but they are just code moves, as far as I'm aware