Mutation isn't checked properly

[gmorenz]

This is almost certainly a known issue, but just in case it isn't, and even if it is to document it. Mutation isn't handled properly, for example

fn a_lie(usize mut i) -> usize
model return == i {
    i += 1;
    return i;
}

export fn main() -> int {
    u8 mut arr[2] = {0, 1};
    printf("%d\n", arr[a_lie(1)]);
}

Expected output: Compiler error

Actual output: Stack buffer overflow

[aep]

thanks for the report. I actually forgot this case.

i = i + 1 should work fine, but the unary operators are broken.

[aep]

i just checked the SMT output and this is actually much worse

the model is scoped after return, so like this:

fn a_lie(usize mut i[0]) -> usize
model return == i {
    i[1] = i[0] + 1;
    return = i[1];
    static_assert(return == i[1]);
}

that's why it passes. but obviously it needs to be scoped so that "i" refers to the input temporal i[0] i believe this should be fixable by using zero as temporal here https://github.com/aep/zz/blob/master/src/symbolic.rs#L617

[gmorenz]

Hmm, so in this case I think I see why 0 should work (though I don't claim to fully understand the code yet).

Won't it have problems for trying to model the output value of mutable pointers though? For example this would no longer work

fn zero_ptr(usize mut * p)
model *p == 0 {
    *p = 0;
}

export fn main() -> int { 
    u8 mut arr[2] = {0, 1};  
    usize mut i = 3;
    zero_ptr(&i);
    printf("%d\n", arr[i]);
}

For mutable pointers, at least, it seems like we need a way of specifying whether we are talking about the final value or the initial value when we make models.

[gmorenz]

PS. I just tried that change... and it has no effect on either of the above examples. I'm not sure why.

[gmorenz]

Ah, I understand why the above doesn't work now. It's setting the version of the boolean return == i, but not the version of i. There is only one version of that boolean, so self.memory[casym].temporal is 0. Rather we want to change the version of i that is used in making that expression.

I'm currently trying to understand where that happens, I hope you don't mind me posting comments here as I work through this.

[aep]

we need a way of specifying whether we are talking about the final value or the initial value

no, the model is always the final value. it applies to the caller of the function. so the case with *p should pass because i is zero after calling zero_ptr(&i);

I hope you don't mind me posting comments here as I work through this.

very happy to go through it together :)

It's setting the version of the boolean return == i, but not the version of i

ah yes of course. ok in that case the correct fix might actually be to just reset all argument names manually. so check_function_model needs to

• let freeze = self.memory.clone();
• go through every argument name in args: &Vec,
  • self.memory[arg].temporal = 0;
• do the check
• self.memory = unfreeze

alternatively i wonder if this works better:

• alloc() the argument names and return before push() to body
• pop before check_function_model so everything is out of scope except args and return
• for every argument name
  • self.memory[arg].temporal = 0;
• do the check

every function is checked with its own ssa instance, so messing with the global scope like this is fine and might better reflect the intent of post-function modeling