Track multiplicities for mustLocks #1073
Conversation
| else | ||
| (add v (current - 1) x, current-1 = 0) | ||
| end | ||
| module D = struct include Lattice.Prod(Lockset)(Multiplicity) |
There was a problem hiding this comment.
Just a quick thought: instead of keeping the lockset both as Lockset and as the key set of Multiplicity, couldn't we just have some multiset that behaves as both?
There was a problem hiding this comment.
Yes, and I thought about it for a while. The idea why I decided against it for now is that it will only be a small minority of mutexes that are recursive, so I want to avoid additional overhead in as many places as possible.
Also, keeping the representation that is needed by other analysis (lockset without multiplicities) around might be advantageous over having to construct it all the time.
There was a problem hiding this comment.
Also, keeping the representation that is needed by other analysis (lockset without multiplicities) around might be advantageous over having to construct it all the time.
Queries.MustLockset reconstructs it all the time anyway since the query returns a different type, but this can be for the time being.
| else | ||
| (add v (current - 1) x, current-1 = 0) | ||
| end | ||
| module D = struct include Lattice.Prod(Lockset)(Multiplicity) |
There was a problem hiding this comment.
Also, keeping the representation that is needed by other analysis (lockset without multiplicities) around might be advantageous over having to construct it all the time.
Queries.MustLockset reconstructs it all the time anyway since the query returns a different type, but this can be for the time being.
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
CHANGES: * Add `setjmp`/`longjmp` analysis (goblint/analyzer#887, goblint/analyzer#970, goblint/analyzer#1015, goblint/analyzer#1019). * Refactor race analysis to lazy distribution (goblint/analyzer#1084, goblint/analyzer#1089, goblint/analyzer#1136, goblint/analyzer#1016). * Add thread-unsafe library function call analysis (goblint/analyzer#723, goblint/analyzer#1082). * Add mutex type analysis and mutex API analysis (goblint/analyzer#800, goblint/analyzer#839, goblint/analyzer#1073). * Add interval set domain and string literals domain (goblint/analyzer#901, goblint/analyzer#966, goblint/analyzer#994, goblint/analyzer#1048). * Add affine equalities analysis (goblint/analyzer#592). * Add use-after-free analysis (goblint/analyzer#1050, goblint/analyzer#1114). * Add dead code elimination transformation (goblint/analyzer#850, goblint/analyzer#979). * Add taint analysis for partial contexts (goblint/analyzer#553, goblint/analyzer#952). * Add YAML witness validation via unassume (goblint/analyzer#796, goblint/analyzer#977, goblint/analyzer#1044, goblint/analyzer#1045, goblint/analyzer#1124). * Add incremental analysis rename detection (goblint/analyzer#774, goblint/analyzer#777). * Fix address sets unsoundness (goblint/analyzer#822, goblint/analyzer#967, goblint/analyzer#564, goblint/analyzer#1032, goblint/analyzer#998, goblint/analyzer#1031). * Fix thread escape analysis unsoundness (goblint/analyzer#939, goblint/analyzer#984, goblint/analyzer#1074, goblint/analyzer#1078). * Fix many incremental analysis issues (goblint/analyzer#627, goblint/analyzer#836, goblint/analyzer#835, goblint/analyzer#841, goblint/analyzer#932, goblint/analyzer#678, goblint/analyzer#942, goblint/analyzer#949, goblint/analyzer#950, goblint/analyzer#957, goblint/analyzer#955, goblint/analyzer#954, goblint/analyzer#960, goblint/analyzer#959, goblint/analyzer#1004, goblint/analyzer#558, goblint/analyzer#1010, goblint/analyzer#1091). * Fix server mode for abstract debugging (goblint/analyzer#983, goblint/analyzer#990, goblint/analyzer#997, goblint/analyzer#1000, goblint/analyzer#1001, goblint/analyzer#1013, goblint/analyzer#1018, goblint/analyzer#1017, goblint/analyzer#1026, goblint/analyzer#1027). * Add documentation for configuration JSON schema and OCaml API (goblint/analyzer#999, goblint/analyzer#1054, goblint/analyzer#1055, goblint/analyzer#1053). * Add many library function specifications (goblint/analyzer#962, goblint/analyzer#996, goblint/analyzer#1028, goblint/analyzer#1079, goblint/analyzer#1121, goblint/analyzer#1135, goblint/analyzer#1138). * Add OCaml 5.0 support (goblint/analyzer#1003, goblint/analyzer#945, goblint/analyzer#1162).
Closes #800.