Skip to content

De-randomize assertion ordering in plain report #5206

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
Dec 17, 2019
Merged

De-randomize assertion ordering in plain report #5206

merged 1 commit into from
Dec 17, 2019

Conversation

xbauch
Copy link
Contributor

@xbauch xbauch commented Dec 13, 2019

specifically order also based on function-name and only compare line number if they differ.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

chrisr-diffblue
chrisr-diffblue reviewed Dec 13, 2019
View reviewed changes
hannes-steffenhagen-diffblue
hannes-steffenhagen-diffblue reviewed Dec 13, 2019
View reviewed changes
Copy link
Contributor

Choose a reason for hiding this comment

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

LGTM, but I imagine some tests will have to be updated?

src/goto-checker/report_util.cpp
return id2string(p1.get_function()) < id2string(p2.get_function());
else if(
!p1.get_line().empty() && !p2.get_line().empty() &&
p1.get_line() != p2.get_line())
return std::stoul(id2string(p1.get_line())) <
std::stoul(id2string(p2.get_line()));
else
Copy link
Contributor

Choose a reason for hiding this comment

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

I think it’d probably be better to sort ids numerically (by the number at the end) rather than lexicographically here

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Done.

chrisr-diffblue
chrisr-diffblue approved these changes Dec 13, 2019
View reviewed changes
Copy link
Contributor

@chrisr-diffblue chrisr-diffblue left a comment

Choose a reason for hiding this comment

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

Looks OK to me, pending un-drafting and passing CI, of course :-)

@codecov-io
Copy link

codecov-io commented Dec 13, 2019 •
edited
Loading

Codecov Report

Merging #5206 into develop will increase coverage by <.01%.
The diff coverage is 93.75%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5206      +/-   ##
===========================================
+ Coverage    67.37%   67.37%   +<.01%     
===========================================
  Files         1157     1157              
  Lines        95072    95087      +15     
===========================================
+ Hits         64054    64068      +14     
- Misses       31018    31019       +1
Flag Coverage Δ
#cproversmt2 42.65% <93.75%> (+0.01%) ⬆️
#regression 63.89% <93.75%> (ø) ⬆️
#unit 31.92% <0%> (-0.01%) ⬇️
Impacted Files Coverage Δ
src/goto-checker/report_util.cpp 41.47% <93.75%> (+3.2%) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update bcde700...ed498df. Read the comment docs.

martin-cs
martin-cs approved these changes Dec 13, 2019
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

Seems reasonable and removing this unnecessary platform non-determinism seems good. I am a little concerned about what this might break in test suites but I guess we will see.

allredj
allredj reviewed Dec 13, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: 26f6282).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/140982791

@xbauch xbauch marked this pull request as ready for review December 13, 2019 16:45
@xbauch xbauch force-pushed the feature/fix-report-order branch 2 times, most recently from 796d726 to 6c3ae51 Compare December 17, 2019 15:26
@petr-bauch
De-randomize assertion ordering in plain report
ed498df 
specifically order also based on function-name and only compare line number if
they differ. Moreover, we extend the id comparison to be alphabetical for the
assertion name and numerical for the number part.
@xbauch xbauch force-pushed the feature/fix-report-order branch from 6c3ae51 to ed498df Compare December 17, 2019 17:07
@martin-cs martin-cs merged commit 0e51ef3 into diffblue:develop Dec 17, 2019
allredj
allredj reviewed Dec 17, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: ed498df).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/141450413

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue left review comments

@martin-cs martin-cs martin-cs approved these changes

@chrisr-diffblue chrisr-diffblue chrisr-diffblue approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@smowton smowton Awaiting requested review from smowton

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
7 participants
@xbauch @codecov-io @martin-cs @allredj @chrisr-diffblue @hannes-steffenhagen-diffblue @petr-bauch