Skip to content

Top thread ID sets inside partitioned arrays #386

@sim642

Description

@sim642

SV-COMP prerun reveals that we now get lots of crashes in ConcurrencySafety:

Fatal error: exception SetDomain.Unsupported("elements on `Top")

This happens when thread IDs sets are used inside partitioned arrays, for example:

./regtest.sh 28 02 --set ana.activated[+] thread --enable exp.partition-arrays.enabled

It happens because the array is initialized to contain unknown integer abstractions, but setting it to a singlethread thread ID set causes a join inside partitioned arrays, which results in a top ValueDomain variant, not a thread ID set.

There is a workaround for thread ID sets overwriting integers for initializing globals and it also gets invoked recursively for updating the array element, but partitioned arrays do some joining nevertheless.

A possible hack to work around this is to implement join of Int and Thread in ValueDomain to yield a Thread (and ignore the Int). Previously we wanted to avoid this since those things can be problematic (#185), but it seems inevitable now, unless someone has a better idea.

Metadata

Metadata

Assignees

Labels

bugsv-compSV-COMP (analyses, results), witnesses

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions