Skip to content
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.

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

Port all remaining library functions #1447

Merged
merged 13 commits into from
May 23, 2024
Merged

Port all remaining library functions #1447

merged 13 commits into from
May 23, 2024

Conversation

karoliineh
Copy link
Member

@karoliineh karoliineh commented May 7, 2024

  • Must be thoroughly checked by someone before merging, because the last bit was quite difficult and can likely contain mistakes
  • Revealed some bug: test 02/34 builtin_va_list fails and has to be looked into, something to do with the autotuner:
Fatal error: exception LibraryDsl.Pattern.Expected("Library function is called with more arguments than expected.")
Raised at LibraryDsl.Pattern.fail in file "src/util/library/libraryDsl.ml", line 14, characters 15-33
Called from Goblint_lib__AutoTune.hasFunction.relevant_static.(fun) in file "src/autoTune.ml", line 158, characters 41-60
Called from Stdlib__Map.Make.exists in file "map.ml", line 329, characters 29-34
Called from Goblint_lib__AutoTune.hasFunction in file "src/autoTune.ml", line 175, characters 2-77
Called from Goblint_lib__AutoTune.activateLongjmpAnalysesWhenRequired in file "src/autoTune.ml", line 210, characters 5-26
Called from Dune__exe__Goblint.main in file "src/goblint.ml", line 59, characters 6-53
Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 560, characters 59-63
Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 566, characters 20-61
Called from Std_exit in file "std_exit.ml", line 18, characters 8-20
See result/index.xml

The latter was caused by the fact that cil has special cases for handling va_arg and va_start functions. Thus, I fixed their argument definitions according to what is written in CIL and left comments.

@karoliineh karoliineh added the cleanup Refactoring, clean-up label May 7, 2024
@karoliineh karoliineh linked an issue May 7, 2024 that may be closed by this pull request
@sim642 sim642 self-requested a review May 8, 2024 10:56
src/util/library/libraryFunctions.ml Outdated Show resolved Hide resolved
src/util/library/libraryFunctions.ml Outdated Show resolved Hide resolved
src/util/library/libraryFunctions.ml Outdated Show resolved Hide resolved
src/util/library/libraryFunctions.ml Outdated Show resolved Hide resolved
src/util/library/libraryFunctions.ml Outdated Show resolved Hide resolved
src/util/library/libraryFunctions.ml Outdated Show resolved Hide resolved
src/util/library/libraryFunctions.ml Outdated Show resolved Hide resolved
src/util/library/libraryFunctions.ml Outdated Show resolved Hide resolved
src/util/library/libraryFunctions.ml Outdated Show resolved Hide resolved
src/util/library/libraryFunctions.ml Show resolved Hide resolved
karoliineh and others added 8 commits May 15, 2024 12:03
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh karoliineh requested a review from sim642 May 21, 2024 09:51
@sim642 sim642 added this to the v2.4.0 milestone May 21, 2024
@sim642 sim642 merged commit ac1225a into master May 23, 2024
21 checks passed
@sim642 sim642 deleted the libfuns-final branch May 23, 2024 07:08
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 2, 2024
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).
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
cleanup Refactoring, clean-up
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Convert all library functions to new specifications
2 participants