analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Try to fix lval lattice

Open sim642 opened this issue 1 year ago • 0 comments

This is an attempt to address https://github.com/goblint/analyzer/issues/101#issuecomment-1200996946 and https://github.com/goblint/analyzer/pull/809#discussion_r935693299 by adding more lval lattice tests for some possibly reasonable structure and getting them to pass.

I've opened this separate from #809 because with the growing complexity and nuance of the domain, I'm no longer sure what the intended behavior should be. Right now I have added a bunch of extra cases to treat a, a[0] and a.fst (first field) equivalently.

One can imagine increasingly complex lvals that this doesn't treat correctly. For example, a.snd (second field) and a[0].snd are the same memory location, but we don't currently treat them as equivalent, because the above equivalence is only ever applied at the end of the offset, not at every intermediate offset. I suspect the only way to deal with that would be to compute some edit distance between the offsets (i.e. where [0] and .fst can be inserted or removed to get from one to the other), but that would be insane. I guess this is why some people use automata to describe access paths...

sim642 avatar Aug 05 '22 11:08 sim642