Assembly checking with aliasing
Opened this issue · 0 comments
andres-erbsen commented
Currently, the assembly checker assumes all inputs and outputs are disjoint. But the functions we are checking are sometimes used with overlapping inputs and outputs, e.g. x = x^2
.
- arbitrary aliasing (
array u64 xs px /\ array u64 ys py
in separation logic), could be supported by resolving reads against either conjunct and keeping only the matching conjunct on writes - we could support equal-or-disjoint pointers by explicitly checking both cases. Or perhaps some encoding like
seps (map (fun i => u64 xs[i] (px+8*i) /\ u64 ys[i] (px+8*i)) (range(len xs))
could do it.