Invalid widen after join with mhp and threadJoins domains (regression 10/15)

[arkocal]

We have this issue on the fwd_constsys_new branch with the solver bu on commit 50de522 , but believe it is on the Lattice and not the solver. We run:

./goblint --solver bu --set ana.activated[+] mhp --set ana.activated[+] threadJoins tests/regression/10-synch/15-join_other_nr.c -v

and get

Fatal error: exception Lattice.Invalid_widen(Map: [mutex:(lockset:{}, multiplicity:{})] = [threadJoins:Reversed (Set (Thread id)): {[main, t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41], Unknown thread id} not leq {[main, t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41, t2_fun@tests/regression/10-synch/15-join_other_nr.c:14:3-14:41], [main, t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41]}])

The solver widens with a joined value, as suggested by Lattice.widen documentation.

L.widen contribution.value (L.join contribution.value new_value)

contribution.value is:

  Temp {
    RETURN ->   0
  }
}, {}, {}, {})), threadid:((unknown node, [main], (created (once) * created (multiple times):({t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41}, {}), created (once) * created (multiple times):({t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41}, {})))), threadflag:(Multithreaded (main)), threadreturn:(true), escape:({}), mutexEvents:(()), access:(()), mutex:(({}, {})), race:(()), mhp:(()), assert:(()), pthreadMutexType:(()), threadJoins:(({[main, t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41], Unknown thread id}, true))], {})}

new value is:

HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{([expRelation:(()), mallocWrapper:((Unknown node, {})), base:(({
  Temp {
    RETURN ->   0
  }
}, {}, {}, {})), threadid:((unknown node, [main], (created (once) * created (multiple times):({t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41}, {}), created (once) * created (multiple times):({t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41}, {})))), threadflag:(Multithreaded (main)), threadreturn:(true), escape:({}), mutexEvents:(()), access:(()), mutex:(({}, {})), race:(()), mhp:(()), assert:(()), pthreadMutexType:(()), threadJoins:(({[main, t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41, t2_fun@tests/regression/10-synch/15-join_other_nr.c:14:3-14:41], [main, t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41]}, true))], {})}

joined value is:

HConsed lifted PathSensitive (ProjectiveSet (MCP.D * map)):PathSensitive (ProjectiveSet (MCP.D * map)):{([expRelation:(()), mallocWrapper:((Unknown node, {})), base:(({
  Temp {
    RETURN ->   0
  }
}, {}, {}, {})), threadid:((unknown node, [main], (created (once) * created (multiple times):({t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41}, {}), created (once) * created (multiple times):({t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41}, {})))), threadflag:(Multithreaded (main)), threadreturn:(true), escape:({}), mutexEvents:(()), access:(()), mutex:(({}, {})), race:(()), mhp:(()), assert:(()), pthreadMutexType:(()), threadJoins:(({[main, t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41, t2_fun@tests/regression/10-synch/15-join_other_nr.c:14:3-14:41], [main, t1_fun@tests/regression/10-synch/15-join_other_nr.c:22:3-22:41]}, true))], {})}