This repository was archived by the owner on Jun 17, 2022. It is now read-only.
Repository navigation
This repository was archived by the owner on Jun 17, 2022. It is now read-only.
Pointers to locals can escape, allowing UB #138
Description
The following compiles:
using <stdio.h>::{printf};
fn addr_of_local() int*
model safe(return)
{
int x = 12;
return &x;
}
fn deref(int *x) int
model *x == return
{
return *x;
}
export fn main() -> int {
int *ptr = addr_of_local();
int a = *ptr;
printf("a is %d\n", a);
int b = deref(ptr);
static_assert(a == b);
printf("%d == %d guaranteed by ZZ's static analysis\n", a, b);
return 0;
}Here is an example output on my machine:
a is 12
12 == 2147450884 guaranteed by ZZ's static analysis
I love the concept behind ZZ, so I'm sad to have found such a gaping hole.
Activity
aep commentedon Oct 13, 2020
yes, there's no lifetime checking at all. see also #13 for a lower hanging fruit in that direction.
Implementing that depends on a whole lot of infrastructure that ins't there yet, specifically i need to separate SSA form from the symbolic prover so we can add more static analysis tools.
Oh there are much worse bugs than this :-P