Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Jun 1, 2022

For a long while now, the i-lock star (denoting symbolic index-based locking) hasn't been nicely printed. For example, the warning for the website example shows def_exc:-19012009 as the index:

[Warning][Race] Memory location data[?]@tests/regression/05-lval_ls/18-website.c:4:5-4:13 (race with conf. 110):
  write with [symblock:{i-lock:mutexes[def_exc:-19012009]}, mhp:{tid=[main, t_fun@tests/regression/05-lval_ls/18-website.c:25:3-25:40]}, lock:{mutexes[def_exc:3]}, thread:[main, t_fun@tests/regression/05-lval_ls/18-website.c:25:3-25:40]] (conf. 110)  (exp: & data[i]) (tests/regression/05-lval_ls/18-website.c:9:3-9:12)

After this PR, this is fixed to display the indented and more user-friendly * in its place, as it was originally intended:

[Warning][Race] Memory location data[?]@tests/regression/05-lval_ls/18-website.c:4:5-4:13 (race with conf. 110):
  write with [symblock:{i-lock:mutexes[*]}, mhp:{tid=[main, t_fun@tests/regression/05-lval_ls/18-website.c:25:3-25:40]}, lock:{mutexes[def_exc:3]}, thread:[main, t_fun@tests/regression/05-lval_ls/18-website.c:25:3-25:40]] (conf. 110)  (exp: & data[i]) (tests/regression/05-lval_ls/18-website.c:9:3-9:12)

This removes the global inthack altogether and changes the Printable used for those i-lock accesses to use a custom implementation that explicitly only has unknown and star indices in offsets. During the expression transformation, star is no longer an integer constant with inthack value, but rather has a special varinfo, which only exists in expressions very locally in the symb_locks analysis.

@sim642 sim642 added cleanup Refactoring, clean-up usability type-safety Type-safety improvements labels Jun 1, 2022
@sim642 sim642 added this to the v2.0.0 milestone Jun 1, 2022
@michael-schwarz michael-schwarz self-requested a review June 1, 2022 08:56
@sim642
Copy link
Member Author

sim642 commented Jun 1, 2022

In particular, this would be quite good for the PRIDE presentation or website update if the same example is to be used for screenshots.

Copy link
Member

@jerhard jerhard left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As the documentation of the SymbLocks analysis is currently pretty sparse, it might also make sense to reference the paper in the code.

@sim642 sim642 merged commit 529a650 into master Jun 7, 2022
@sim642 sim642 deleted the remove-inthack branch June 7, 2022 07:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

cleanup Refactoring, clean-up type-safety Type-safety improvements usability

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants