Failing to assume invariants on field when unfolding a struct

[Ralender]

Why is the following program considered not safe ?

struct A {
  val: u32,
}

impl A {
  fn f(&mut self) -> () {
    if self.val == 0 {
      return;
    }
    let a = self.val - 1;
  }
}

but the following is considered safe ?

fn f(val: u32) -> () {
  if val == 0 {
    return;
  }
  let a = val - 1;
}

[ranjitjhala]

Good catch! @nilehmann I thought it was due to the two occurrences of self.val being unconnected (and so the guard not "applying". However, this modification fails ... so I think maybe the u32 is non-negative is lost when we extract it from a field projection?

#![feature(register_tool)]
#![register_tool(flux)]

struct A {
  val: u32,
}

#[flux::sig(fn (bool[true]))]
fn assert(_b:bool) {}

impl A {
  fn f(&mut self) {
    let tmp = self.val;
    assert(tmp >= 0);    // THIS ASSERTION ALSO FAILS
    
    if tmp == 0 {
      return;
    }
    let a = tmp  - 1;
  }
}

[ranjitjhala]

Furthermore, adding this makes stuff work (if you have a single self.val read up at the top)

struct A {
    #[flux::field(u32{v:0 <= v})]
    val: u32,
}

[nilehmann]

Coming a bit late to the game but this definitively looks like a bug.

The issue seems to be that we are not correctly assuming the invariants on u32 (i.e., that values are non-negative) when we unfold the struct. Without knowing self.val >= 0 then self.val != 0 doesn't imply self.val - 1 >= 0.

We try to be smart about when to assume invariants on types to avoid unnecessarily polluting the constraint with extra facts, but in doing so we are failing to do it in some places.

[nilehmann]

#541 solves the problem of not correctly assuming the type invariants when creating the temporary. To solve the original problem we need to implement unfolding of mutable references.