Conversation
Co-authored-by: Jevgenijs Protopopovs <jevgenijs.protopopovs@ut.ee>
sim642
added
feature
pr-dependency
They should not be skipped over and no self-loop with Skip needs to be added.
|
Hmm, there's something fishy with the tests: they pass locally but fail in some of the CI. The CFG rendering might be sensitive to |
| | Asm a -> | ||
| let (changed, gotos') = List.fold_left_map (fun acc target -> | ||
| match newtarget !target with | ||
| | None -> (acc, target) (* TODO: need to copy target ref as well? *) | ||
| | Some nt -> (true, ref nt) | ||
| ) false a.gotos | ||
| in | ||
| if changed then ( | ||
| s.skind <- Asm {a with gotos = gotos'}; | ||
| DoChildren | ||
| ) | ||
| else | ||
| SkipChildren |
There was a problem hiding this comment.
I wondered about this too and that's why I left the TODO. It wasn't clear to me whether the sharing of refs might be intentional for something because the Goto case doesn't do the copy if it's not necessary. A bunch of this logic deals with physical equality in various ways so it can be quite fragile.
I then tried to just remove the ref wrapper from Goto in CIL itself to see if it's really necessary. There's at least one use case there for it: during Cabs2cil the Gotos initially refer to dummy statements which are filled in at the end of the function once all labels have been seen. Maybe that's the only reason for the ref and the mutability is never used again.
If that's the case, it'd be useful to have private mutability (which sadly doesn't exist): https://discuss.ocaml.org/t/mutable-fields-of-private-records/18213.
Another option might be to build some thin abstraction around the ref which can ensure that it's only assigned once within CIL and cannot be mutated later.
This is an alternative to #1326. It just adds
asm gotosupport, but nothing related to invalidation, etc.This is cherry-picked from https://github.com/sws-lab/race-harness-goblint/commit/733c9865e1912c7663207291cbf48dc26213a493, which is originally by @jprotopopov-ut.
TODO