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

Add location ranges to output #449

Merged
merged 13 commits into from
Nov 23, 2021
Merged

Add location ranges to output #449

merged 13 commits into from
Nov 23, 2021

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Nov 16, 2021

Closes #428.

This is based on goblint/cil#51.

TODO

@sim642
Copy link
Member Author

sim642 commented Nov 16, 2021

Currently for testing purposes I made CilType.Location.show fail if the end location is missing in order to easily find all constructs where it was still missing. I will undo that now, but it did reveal two interesting cases.

12/01 containment/analyse

Crashes with

Option warning: Without thread escape analysis, every local variable whose address is taken is considered escaped, i.e., global!
Unimplemented: joinLoc LLVM INTERNAL:1:1--1:-1 regression.h:5:1--1:-1

Apparently that old C++ -> C converter produced some crazy location info where a function beginning is in one filename and the end is in another. There's no sensible way to construct such location range.

So far I haven't seen any other case where such insanity happens, so maybe we can just ignore it and it'll be fixed after we remove the contain analysis from "lean" Goblint.

EDIT: I've now just skipped it, so this doesn't have to wait for "fat" Goblint release.

24/08 octagon/previously_problematic_f

Crashes with

[Warning][Integer > Overflow][CWE-190] Signed integer overflow ([Error][Unknown] About to crash! (Fatal error: exception Failure("no end at initfun:0:0")

The output is wacky because the exception happens when printing the location of the previous message, but in essence the non-apron octagon analysis uses IntDomain internally and in its computations performs operations which would be an overflow (despite the program itself not having one). And this doesn't happen during some transfer functions, but lattice operations like join, which is the reason for the weird initfun:0:0 location.

@sim642
Copy link
Member Author

sim642 commented Nov 18, 2021

I now adapted this to goblint/cil#51 (comment) as well. The just expression locations for ifs are now used for the Test edges in the CFG, instead of the location spanning the entire if. This way warnings about the expression are nice and local.

EDIT: Additionally had to add secondary location ranges to primitive instructions as well since they may be temporary statements inserted by CIL to perform calls and assignments that are part of a conditional expression originally. Those should also have the location on the expression itself, not the entire if.

@sim642 sim642 merged commit 74d7157 into master Nov 23, 2021
@sim642 sim642 deleted the loc-end branch November 23, 2021 13:15
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
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.

Location ranges for output
1 participant