Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Apr 7, 2022

This adds Errormsg.transformLocation, which Goblint can override to supply a function for transforming the location directives. It allows us to massage paths relative to other directories from compilation databases to make them relative to the analyzed project as a whole.
Also it allows ignoring the location directives which could be used to analyze already preprocessed files, which have location directives to some old absolute paths that no longer make sense.

@sim642
Copy link
Member Author

sim642 commented Apr 7, 2022

This would actually allow us to revert #73, because using this transformation hook Goblint could also remember what it transformed on its own. Do we want to revert that or just keep it?

@michael-schwarz
Copy link
Member

Do we want to revert that or just keep it?

I'd be in favor of reverting and using this instead. No point in keeping different ways to do the same thing around!

@michael-schwarz
Copy link
Member

I think we should investigate the failures on OS X. Especially since for #90 the OS X CI is now also happy.

@sim642
Copy link
Member Author

sim642 commented Apr 8, 2022

I added a step to the CI workflow to upload the cil.log from failed runs, so it's possible to see that from MacOS as well.
Apparently all the tests fail with

Error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"dlopen(/Users/runner/work/cil/cil/_opam/lib/batteries/batteries.cmxs, 10): image not found\")")

I guess that's related to having removed the batteries dependency from the CIL library itself, but I'm very confused why it would be needed on MacOS, but not Linux. Also batteries itself does get installed into the opam switch nevertheless, so it's weird that it wouldn't be found there. It's not something in dune's _build.

@sim642
Copy link
Member Author

sim642 commented Apr 8, 2022

I'm just reverting that and hoping it works again. I think it's somehow related to all this dynamic feature library loading, which somehow also depends on what dependencies the CIL library itself has:

cil/src/feature.ml

Lines 98 to 101 in e559ead

let preds = [ if D.is_native then "native" else "byte"; "plugin" ] in
let cil_deps = F.package_deep_ancestors preds ["goblint-cil"] in
let deps = F.package_deep_ancestors preds [pkg] in
let deps = List.filter (fun x -> not (List.mem x cil_deps)) deps in

I'm still not sure why it would be any different between Linux vs MacOS, but whatever for now.

@sim642 sim642 requested a review from michael-schwarz April 8, 2022 10:24
@sim642 sim642 merged commit faff341 into develop Apr 11, 2022
@sim642 sim642 deleted the transform-location branch May 30, 2022 07:12
@sim642 sim642 added this to the 2.0.0 milestone Aug 12, 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.

3 participants