-
Notifications
You must be signed in to change notification settings - Fork 20
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
Fix syntactic search #147
Fix syntactic search #147
Conversation
Goblint-CIL aims to support OCaml >= 4.05, so things such as |
8ac975c
to
f89a373
Compare
I am extremely skeptical that this indeed fixes that issue. We had identified that it was due to |
Ok, I am sure this is a stupid question, but here it comes: Why rely on something so brittle as line numbers here at all? |
I did some more investigation: |
CIL renames duplicate variable names in its so-called alpha-conversion. These renamings are stored in a hash table that maps variable names from the c source code to (possibly several) tuples of varinfo (which possibly has a different name) and location (where the varinfo with the new name was created). The function Here is an example:
Querying for variables of name I was wondering if one could avoid this check by searching for the varinfo, instead of just its name, but I think this would need some more extensive refactoring. |
Thanks for the clarification! I feel like I knew this at some point, but have forgotten it since then. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM!
@stilscher what is blocking this? |
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
CHANGES: * Add `asm inline` parsing (goblint/cil#151). * Ignore top level qualifiers in `__builtin_types_compatible_p` (goblint/cil#157). * Add attribute `goblint_cil_nested` to local variables in inner scopes (goblint/cil#155). * Expose `Cil.typeSigAddAttrs`. * Add option to suppress `long double` warnings (goblint/cil#136, goblint/cil#156). * Fix syntactic search (goblint/cil#147).
CHANGES: * Add `asm inline` parsing (goblint/cil#151). * Ignore top level qualifiers in `__builtin_types_compatible_p` (goblint/cil#157). * Add attribute `goblint_cil_nested` to local variables in inner scopes (goblint/cil#155). * Expose `Cil.typeSigAddAttrs`. * Add option to suppress `long double` warnings (goblint/cil#136, goblint/cil#156). * Fix syntactic search (goblint/cil#147).
Fixes #146.
The syntactic search looks up the corresponding (possibly differently named) varinfo and location in the environment and checks whether it is within the function currently in focus. The check whether the location is within the function only considers the starting line number. Also, as the end of the function the starting line number of the "next" function is taken. There can however be several different files, so the line number is not a sufficiently precise representation of the location. Also the start line number of the next function might be in a different file and therefore does not correspond with the actual end line number of the function (apart from this I am not sure if any reasonable ordering of the functions in the list can even be assumed).
In the example from the issue, this leads to function main reaching from line 4-5 (5 is the start line of function pthread_once), and so no variable use of
fail
is found within.Changes:
file
field of the location and use itsendLine
field directly whenever it is set.This also fixes the issue goblint/gobview#7 (comment).The expression of the semantic query is only evaluated on the results from the syntactic analysis, so if no variable uses are found in the syntactic search, the semantic search will also look broken. I could not find an example where the semantic analysis is still broken (apart from what is fixed in goblint/analyzer#1092 (comment)).Related PRs: goblint/analyzer#1092 (comment), goblint/gobview#25 (comment)