New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add and fix library functions for Concrat benchmarks #1174

Merged

sim642 merged 11 commits into master from libfuns-concrat

Sep 27, 2023

Member

sim642 commented Sep 18, 2023

Changes

Fix incorrect and unsound return_on_success value for some pthread locking functions. This caused most of uthash benchmark being dead.
Convert remaining old library function classify to new specifications. In particular, some benchmark needed precise accesses for pthread_join to not deeply invalidate everything via the second argument.
Remove now-unnecessary bridge code for old library function classify.
Add missing library functions for nnn benchmark. Apparently Add missing library functions for Concrat benchmarks #996 didn't add everything.

sim642 added 5 commits

September 18, 2023 15:51


          Add missing library functions for nnn

c9c3980


          Fix return_on_success for some pthread locking functions

ffc5c6d


          Make pthread_join invalidate precise

2d91b05


          Convert remaining old library function classify

f27a6e7


          Remove old library function classify

4e83af9

sim642 added cleanup bug unsound precision benchmarking labels

sim642 added this to the v2.3.0 milestone

michael-schwarz self-requested a review

September 18, 2023 15:27

sim642 mentioned this pull request

MayPointTo is not subset of ReachableFrom #1175

Open


          Add some missing library functions for shairport

a4772d6

sim642 mentioned this pull request

Fix NULL and unknown pointer handling in MayPointTo and ReachableFrom for race analysis #1176

Merged

Member

michael-schwarz commented Sep 19, 2023

Fix incorrect and unsound return_on_success value for some pthread locking functions. This caused most of uthash benchmark being dead.

Might be worth adding tests for this.

michael-schwarz reviewed

View reviewed changes

src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved

michael-schwarz reviewed

View reviewed changes

src/analyses/libraryFunctions.ml Show resolved Hide resolved

michael-schwarz reviewed

View reviewed changes

src/analyses/libraryFunctions.ml Outdated Show resolved Hide resolved

michael-schwarz reviewed

View reviewed changes

src/analyses/libraryFunctions.ml Show resolved Hide resolved

michael-schwarz reviewed

View reviewed changes

src/analyses/libraryFunctions.ml Show resolved Hide resolved

sim642 added 3 commits

September 20, 2023 10:05


          Move memccpy to c_descs_list for C23

f7851e8


          Use unknown_exp for usb_alloc_urb size

d1d8d66


          Add test for atexit soundness

71035d2

sim642 mentioned this pull request

Autotuner doesn't account for all spawning functions #1181

Closed

michael-schwarz linked an issue

that may be closed by this pull request

Convert all library functions to new specifications #1029

Closed

michael-schwarz approved these changes

View reviewed changes

Member

michael-schwarz left a comment

LGTM! Two things I would still want:

A test for the unsoundness due to the wrong return values of pthread functions you mentioned
An option sem.atexit.ignore to get the behavior w.r.t. these that is the current default on master.

sim642 added 2 commits

September 25, 2023 11:00


          Add test for pthread locking function return values

1947aae


          Add atexit test with spawn disabled

4bc0303

sim642 merged commit 631888e into master

11 of 16 checks passed

sim642 deleted the libfuns-concrat branch

September 27, 2023 10:35

sim642 mentioned this pull request

Add missing library functions for large Concrat benchmarks #1212

Merged

sim642 mentioned this pull request

[new release] goblint (2.3.0) ocaml/opam-repository#24844

Merged

sim642 added a commit to sim642/opam-repository that referenced this pull request


          [new release] goblint (2.3.0)

34ad5a7

CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

* Add termination analysis for loops (goblint/analyzer#1093).
* Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197).
* Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246).
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262).
* Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248).
* Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191).
* Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269).
* Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).

nberth pushed a commit to nberth/opam-repository that referenced this pull request


          [new release] goblint (2.3.0)

8f8e773

CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

* Add termination analysis for loops (goblint/analyzer#1093).
* Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197).
* Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246).
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262).
* Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248).
* Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191).
* Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269).
* Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).

sim642 added a commit to sim642/opam-repository that referenced this pull request


          [new release] goblint (2.4.0)

38186e2

CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).

sim642 mentioned this pull request

[new release] goblint (2.4.0) ocaml/opam-repository#26327

Merged

avsm pushed a commit to avsm/opam-repository that referenced this pull request


          [new release] goblint (2.4.0)

2afe816

CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).

sim642 mentioned this pull request

Fix sem.unknown_function.spawn handling in base #1603

Merged

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

benchmarking bug cleanup precision unsound