Overwriting a composite object in an array causes a blowup in variables

[jsalzbergedu]

The following code:

const MAX_NUM_OBJECTS: usize = 1024;
const MAX_OBJECT_SIZE: usize = 64;
const STACK_DEPTH: usize = 6;


type PtrId = u32;

#[derive(Copy, Clone)]
enum Item {
    Even,
    Odd,
}

#[kani::proof]
fn main() {
    let mut local = 5;
    let local_ptr = &local as *const i32;
    let ptr_object = kani::mem::pointer_object(local_ptr);
    let ptr_offset = kani::mem::pointer_offset(local_ptr);
    let mut mem: [[Option<[Item; 10]>; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS] =
                 [[None; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS];
    let mut s = match mem[ptr_object][ptr_offset] {
        None => [Item::Even; 10],
        Some(v) => v
    };
    s[0] = Item::Odd;
    mem[ptr_object][ptr_offset] = Some(s);
}

Produces a SAT instance with millions of variables when run by Kani. Changing the pointer object to a constant reduces the size to roughly 100 variables:

const MAX_NUM_OBJECTS: usize = 1024;
const MAX_OBJECT_SIZE: usize = 64;
const STACK_DEPTH: usize = 6;


type PtrId = u32;

#[derive(Copy, Clone)]
enum Item {
    Even,
    Odd,
}

#[kani::proof]
fn main() {
    let mut local = 5;
    let local_ptr = &local as *const i32;
    let ptr_object = kani::mem::pointer_object(local_ptr);
    let ptr_offset = kani::mem::pointer_offset(local_ptr);
    let mut mem: [[Option<[Item; 10]>; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS] =
                 [[None; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS];
    let mut s = match mem[0][ptr_offset] {
        None => [Item::Even; 10],
        Some(v) => v
    };
    s[0] = Item::Odd;
    mem[0][ptr_offset] = Some(s);
}

and swapping out for a triple array also has a reasonable verification size

const MAX_NUM_OBJECTS: usize = 1024;
const MAX_OBJECT_SIZE: usize = 64;
const STACK_DEPTH: usize = 6;


type PtrId = u32;

#[derive(Copy, Clone)]
enum Item {
    Even,
    Odd,
}

#[kani::proof]
fn main() {
    let mut local = 5;
    let local_ptr = &local as *const i32;
    let ptr_object = kani::mem::pointer_object(local_ptr);
    let ptr_offset = kani::mem::pointer_offset(local_ptr);
    let mut mem: [[[Item; 10]; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS] =
                 [[[Item::Even; 10]; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS];
    mem[ptr_object][ptr_offset][0] = Item::Odd;
}

[tautschnig]

This is as expected, see below. Can you please elaborate what the expectation or problem is?

Explanation: Accessing an array at a non-constant index requires encoding conditional updates to all elements of the array in an eager propositional encoding. The theory of arrays gives rise to a decision procedure that does not require constraints for all possible indices, and we know that this is something that we ought to improve on the CBMC side. See diffblue/cbmc#1874 for what remains work-in-progress.

[jsalzbergedu]

@tautschnig understood. I was thinking that the memory would be updated in-place; generating the MIR showed however that the array is copied in. I was able to resolve the issue for my example by using a triple array with constant size elements, as shown in the last example. Can I close the issue?

[tautschnig]

I was able to resolve the issue for my example by using a triple array with constant size elements, as shown in the last example. Can I close the issue?

I'm still not sure what exactly the problem is/was. Was it that the performance was unacceptable?