Libvsync

[leventeBajczi]

• Can parse non-variable references if they are referencing a literal-offset (currently only 0) dereference
• Can parse GNU C builtins
• Can parse ambiguous expressions such as (len) & a ( -- is it a cast? is it a bitwise AND? i hate C)
• Can interpret GNU C builtins for atomic accesses

[leventeBajczi]

@csanadtelbisz, if we were able to change the StartLabel/JoinLabel handles to expressions (i'm okay with constraining them to LHS expressions, i.e., RefExpr and DerefExpr), we could now parse libvsync tasks.

[csanadtelbisz]

@csanadtelbisz, if we were able to change the StartLabel/JoinLabel handles to expressions (i'm okay with constraining them to LHS expressions, i.e., RefExpr and DerefExpr), we could now parse libvsync tasks.

I do not see any obstacle: we would only need to add an extra case for creating a memoryassignment when necessary. I am expecting some changes in both the LTS-based analysis (XcfaState), OC checker event graph mapping and the monolithic conversion, but none of them should be too challenging. Shall I do it or are you working on it?

[leventeBajczi]

Please do it if you have the time, I won't really be able to work on this.
I'll happily do the atomic builtin mappings if you'd like me to, though!

[github-actions]

❗ Please modify build.gradle.kts to contain a later version than 6.27.14. Current version is 6.27.14.

[github-actions]

❗ Please run ./gradlew spotlessApply on your branch to fix formatting.

[github-actions]

Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all):

Rundefinition	COMPLEX	EMERGENT	HORN
SV-COMP25_no-data-race	✅ (1 / 0 / 27) HTML/CSV	✅ (1 / 0 / 27) HTML/CSV	✅ (1 / 0 / 27) HTML/CSV
SV-COMP25_no-overflow	✅ (10 / 0 / 228) HTML/CSV	❓ (0 / 0 / 220) HTML/CSV	❓ (0 / 0 / 234) HTML/CSV
SV-COMP25_termination	❓ (0 / 0 / 201) HTML/CSV	❓ (0 / 0 / 201) HTML/CSV	❓ (0 / 0 / 203) HTML/CSV
SV-COMP25_unreach-call	✅ (1 / 0 / 64) HTML/CSV	❓ (0 / 0 / 62) HTML/CSV	❓ (0 / 0 / 65) HTML/CSV
SV-COMP25_valid-memcleanup	❓ (0 / 0 / 66) HTML/CSV	❓ (0 / 0 / 66) HTML/CSV	❓ (0 / 0 / 66) HTML/CSV
SV-COMP25_valid-memsafety	❓ (0 / 0 / 266) HTML/CSV	❓ (0 / 0 / 144) HTML/CSV	❓ (0 / 0 / 256) HTML/CSV

[leventeBajczi]

SV-COMP26_no-data-race.C.no-data-race.Concurrency.xml.bz2.diff.html
SV-COMP26_no-data-race.C.no-data-race.Concurrency.xml.bz2.table.html
SV-COMP26_no-overflow.xml.bz2.diff.html
SV-COMP26_no-overflow.xml.bz2.table.html
SV-COMP26_termination.xml.bz2.diff.html
SV-COMP26_termination.xml.bz2.table.html
SV-COMP26_unreach-call.xml.bz2.diff.html
SV-COMP26_unreach-call.xml.bz2.table.html

I realized I had some finished tests for this branch; it shows we have significant work to do still.