*p and p[0] are treated differently

[ksqsf]

using <stdio.h>::{printf, scanf};

fn foo(int *p) -> int {
  // return p[0]; // not ok
  return *p; // ok
}

export fn main() -> int {
    int mut y = 123;
    foo(&y);
    return 0;
}

[aep]

thanks for the report!

that's an unfortunate side effect of the len vs safe theory.

because safe(p) is implicit, the prover knows *p is fine,
but len(p) is undefined, so p + anything is unprovable

a quick fix would be

 assert( = (safe(x) (> len(x) 0) )

but this slows down the prover dramatically

i'd prefer to not fix this until deref is correctly implemented. it actually needs to check len() as well because you might cast to a different pointer size and then deref.

that again isn't implemented yet because i haven't found a good way yet to get target pointer sizes. the current prover VM just assumes 64bit.

[jacereda]

that again isn't implemented yet because i haven't found a good way yet to get target pointer sizes. the current prover VM just assumes 64bit.

Does __SIZEOF_POINTER__ preprocessor symbol suffice?

[aep]

yes, but the prepro is unavailable to zz.

One leasson learned from rust is that zz will never make assumptions about your target build system, so it cannot possibly know how to call your c compiler with the correct flags for your target.

the options are pretty much

1. just assume 64bit because the edges cases where 32bit has bugs that 64bit doesnt aren't worth it
2. add some sort of --architecture build flags
3. test 64 and 32bit (nope because thats insanely slow)

[jacereda]

Well, you can shell-out to the target compiler (would need to be configured) with -dM -E flags to extract things like type sizes and endianness.

I guess 2 could also be a good option.

[aep]

actually, this is fixed, isnt it?