Use TrieDomain to distribute accesses to contained fields

[karoliineh]

Builds on #1084.

Instead of distributing an access-to-a-struct to all of the fields in that struct, the implementation distributes to those fields only that had direct access(es) themselves. Meaning that if there is access to a struct only, there will be one warning for that struct instead of a separate warning for each of the struct fields. And if there was access to a field of a struct, a race between the access to that struct's field and the access to the whole struct is not lost.

For that, the accesses are collected in a trie structure representing a struct. In the trie node, there is a set of accesses to that offset and a map of that offset's children with the child offset as a key and a sub-trie as a value. Later, the accesses of each node's ancestors are also checked for races with the node accesses, doing the distribution.

Also fixes soundness issue described in #978.
Previously Access.add_distribute_inner was based on the type. Since alloc variables have void type, contained fields for a blob could not be iterated and distributed to. Since this delays the inner distribution and flips the direction, the issue is automatically avoided: an access to (alloc).foo will be checked against an access to just (alloc) simply due to the trie structure.

[michael-schwarz]

Where is the PR-dependency here? Does it make sense to review this as of now?

[sim642]

Where is the PR-dependency here? Does it make sense to review this as of now?

The dependency was #1084, which is now merged, so this can be reviewed.

[michael-schwarz]

Apart from the comment of deriving eq for type, LGTM!

[michael-schwarz]

Thanks for the clarification!

…

On Tue, Jul 11, 2023, 4:46 PM Simmo Saan ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In src/domains/access.ml <#1089 (comment)>: > @@ -80,11 +80,34 @@ let reset () = type acc_typ = [ `Type of CilType.Typ.t | `Struct of CilType.Compinfo.t * Offset.Unit.t ] [@@deriving eq, ord, hash] (** Old access type inferred from an expression. *) +module MemoRoot = +struct + include Printable.StdLeaf + type t = [`Var of CilType.Varinfo.t | `Type of CilType.Typ.t] [@@deriving eq, ord, hash] CilType.Typ exists precisely to take care of it. The recursion in Cil.typ structural comparison comes from compinfos and CilType.Compinfo has an implementation that only compares cids. — Reply to this email directly, view it on GitHub <#1089 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ADJME3O6SJMICP5S55ZZSZDXPVRN5ANCNFSM6AAAAAAZIBJUJA> . You are receiving this because you commented.Message ID: ***@***.***>