Skip to content

Port all remaining library functions #1447

Merged
sim642 merged 13 commits intomasterfrom
libfuns-final
May 23, 2024
Merged

Port all remaining library functions #1447
sim642 merged 13 commits intomasterfrom
libfuns-final

Conversation

@karoliineh
Copy link
Copy Markdown
Member

@karoliineh karoliineh commented May 7, 2024 •
edited
Loading

  • 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
Convert all library functions to new specifications #1029
Closed
@sim642 sim642 self-requested a review May 8, 2024 10:56
sim642
sim642 reviewed May 15, 2024
View reviewed changes
karoliineh and others added 8 commits May 15, 2024 12:03
@karoliineh @sim642
w for lhs in __builtin_va_arg
f4504b6 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh
Move __builtin_ prefixed functions from c standard lib to GCC builtins
ab35510
@karoliineh @sim642
:: for VarArgs instead ;
6c93ce6 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Add w for n in getline and getdelim
ef726e9 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Apply suggested changes
3279111 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh @sim642
Apply suggestions from code review
96f2cf2 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@karoliineh
Make arguments of function pointer type spawn
bedfb35
@karoliineh
Merge branch 'libfuns-final' of github.com:goblint/analyzer into libf…
cbf00dd 
…uns-final
sim642
sim642 reviewed May 16, 2024
View reviewed changes
@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
@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
@sim642
[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 sim642 mentioned this pull request Aug 2, 2024
Merged
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
@sim642 @avsm
[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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sim642 sim642 sim642 approved these changes

Assignees

No one assigned

Labels

cleanup Refactoring, clean-up

Projects

None yet

Milestone

v2.4.0

Development

Successfully merging this pull request may close these issues.

Convert all library functions to new specifications

2 participants

@karoliineh @sim642