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

Expose standalone expression parsing via Frontc #97

Merged
merged 2 commits into from
May 30, 2022

Conversation

sim642
Copy link
Member

@sim642 sim642 commented May 26, 2022

This is currently on top of #96, but could be rebased if necessary.

Since Formatcil is not intended for parsing standalone expressions from user input and is very fragile (#94, #95), then this is an attempt to provide a proper alternative. It exposes Frontc and Cabs2cil functions for parsing just an expression from a given string. This allows expressions to be parsed using the normal parsing pipeline with all the usual behavior (correct typing, implicit casts, etc).

This is a more reliable alternative to be used in goblint/analyzer#745.

This might still be buggy, because doPureExp, which is at the center of this, uses at least 30 global variables (I might have missed some). Here I just require env and genv to be given such that the expression can be converted to CIL in the correct function's context (with all the variables referring to a particular function's locals). As to rest of the globals, there's no way to reconstruct their content at a particular function as they were when the entire file was parsed, so this might still break in surprising ways, but it should already be better than Formatcil.

@sim642 sim642 added enhancement pr-dependency Depends or builds on another PR, which should be merged before labels May 26, 2022
This can be set from Goblint before convStandaloneExp.
@sim642 sim642 merged commit 91d5d2b into check-exp May 30, 2022
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label May 30, 2022
@sim642
Copy link
Member Author

sim642 commented May 30, 2022

Weird, merging #96, which this was on top of, didn't for some reason cause the base of this PR to change to develop automatically, so it still merged to the check-exp branch. I'll merge it to develop directly myself then.

sim642 added a commit that referenced this pull request May 30, 2022
Expose standalone expression parsing via Frontc
@sim642 sim642 deleted the frontc-standalone-exp branch May 30, 2022 07:12
@sim642
Copy link
Member Author

sim642 commented May 30, 2022

Oh, I know: this repository didn't have "Automatically delete head branches" enabled like the analyzer repository. I enabled it here as well and deleted all the branches corresponding to merged PRs to clean things up.

@sim642 sim642 added this to the 2.0.0 milestone Jul 17, 2022
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 12, 2022
CHANGES:

* Wrap library into `GoblintCil` module (goblint/cil#107).
* Remove all MSVC support (goblint/cil#52, goblint/cil#88).
* Port entire build process from configure/make to dune (goblint/cil#104).
* Add C11 `_Generic` support (goblint/cil#48).
* Add C11 `_Noreturn` support (goblint/cil#58).
* Add C11 `_Static_assert` support (goblint/cil#62).
* Add C11 `_Alignof` support (goblint/cil#66).
* Add C11 `_Alignas` support (goblint/cil#93, goblint/cil#108).
* Add partial C11 `_Atomic` support (goblint/cil#61).
* Add `_Float32`, `_Float64`, `_Float32x` and `_Float64x` type support (goblint/cil#8, goblint/cil#60).
* Add Universal Character Names, `char16_t` and `char32_t` type support (goblint/cil#80).
* Change locations to location spans and add additional expression locations (goblint/cil#51).
* Add synthetic marking for CIL-inserted statement locations (goblint/cil#98).
* Expose list of files from line control directives (goblint/cil#73).
* Add parsed location transformation hook (goblint/cil#89).
* Use Zarith for integer constants (goblint/cil#47, goblint/cil#53).
* Fix constant folding overflows (goblint/cil#59).
* Add option to disable constant branch removal (goblint/cil#103).
* Add standalone expression parsing and checking (goblint/cil#97, goblint/cil#96).
* Improve inline function merging (goblint/cil#72, goblint/cil#85, goblint/cil#84, goblint/cil#86).
* Fix some attribute parsing cases (goblint/cil#71, goblint/cil#75, goblint/cil#76, goblint/cil#77).
* Fix global NaN initializers (goblint/cil#78, goblint/cil#79).
* Fix `cilly` binary installation (goblint/cil#99, goblint/cil#100, goblint/cil#102).
* Remove batteries dependency to support OCaml 5 (goblint/cil#106).
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 12, 2022
CHANGES:

* Wrap library into `GoblintCil` module (goblint/cil#107).
* Remove all MSVC support (goblint/cil#52, goblint/cil#88).
* Port entire build process from configure/make to dune (goblint/cil#104).
* Add C11 `_Generic` support (goblint/cil#48).
* Add C11 `_Noreturn` support (goblint/cil#58).
* Add C11 `_Static_assert` support (goblint/cil#62).
* Add C11 `_Alignof` support (goblint/cil#66).
* Add C11 `_Alignas` support (goblint/cil#93, goblint/cil#108).
* Add partial C11 `_Atomic` support (goblint/cil#61).
* Add `_Float32`, `_Float64`, `_Float32x` and `_Float64x` type support (goblint/cil#8, goblint/cil#60).
* Add Universal Character Names, `char16_t` and `char32_t` type support (goblint/cil#80).
* Change locations to location spans and add additional expression locations (goblint/cil#51).
* Add synthetic marking for CIL-inserted statement locations (goblint/cil#98).
* Expose list of files from line control directives (goblint/cil#73).
* Add parsed location transformation hook (goblint/cil#89).
* Use Zarith for integer constants (goblint/cil#47, goblint/cil#53).
* Fix constant folding overflows (goblint/cil#59).
* Add option to disable constant branch removal (goblint/cil#103).
* Add standalone expression parsing and checking (goblint/cil#97, goblint/cil#96).
* Improve inline function merging (goblint/cil#72, goblint/cil#85, goblint/cil#84, goblint/cil#86).
* Fix some attribute parsing cases (goblint/cil#71, goblint/cil#75, goblint/cil#76, goblint/cil#77).
* Fix global NaN initializers (goblint/cil#78, goblint/cil#79).
* Fix `cilly` binary installation (goblint/cil#99, goblint/cil#100, goblint/cil#102).
* Remove batteries dependency to support OCaml 5 (goblint/cil#106).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants