Skip to content

Assume relation between two symbols #5362

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

Merged
merged 2 commits into from
Jun 5, 2020
Merged

Conversation

thk123
Copy link
Contributor

@thk123 thk123 commented May 28, 2020

Pulled out of #5361 as appears to be an unrelated bug fix. Not sure what bug it is fixing yet - will try and add a test!

  • 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).
  • [na] 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.

@thk123 thk123 mentioned this pull request May 28, 2020
6 tasks
@thk123
Copy link
Contributor Author

thk123 commented May 28, 2020

This doesn't fix #179. but a different issue on a private fork - adding a test now

@codecov
Copy link

codecov bot commented May 28, 2020

Codecov Report

Merging #5362 into develop will increase coverage by 36.35%.
The diff coverage is 70.00%.

Impacted file tree graph

@@             Coverage Diff              @@
##           develop    #5362       +/-   ##
============================================
+ Coverage    31.81%   68.17%   +36.35%     
============================================
  Files          919     1170      +251     
  Lines        80404    96559    +16155     
============================================
+ Hits         25584    65832    +40248     
+ Misses       54820    30727    -24093     
Flag Coverage Δ
#cproversmt2 42.47% <ø> (?)
#regression 65.37% <70.00%> (?)
#unit 31.81% <ø> (-0.01%) ⬇️
Impacted Files Coverage Δ
src/util/interval_template.h 89.39% <62.50%> (+5.18%) ⬆️
src/analyses/interval_domain.cpp 57.94% <100.00%> (ø)
src/pointer-analysis/value_set_analysis.h 20.00% <0.00%> (-13.34%) ⬇️
src/analyses/cfg_dominators.h 88.88% <0.00%> (-11.12%) ⬇️
src/analyses/natural_loops.h 92.30% <0.00%> (-7.70%) ⬇️
src/util/symbol.h 94.59% <0.00%> (-5.41%) ⬇️
src/goto-programs/goto_model.h 66.66% <0.00%> (-4.77%) ⬇️
src/analyses/static_analysis.h 54.16% <0.00%> (-2.36%) ⬇️
src/util/union_find.h 85.71% <0.00%> (-0.50%) ⬇️
src/analyses/ai.h 57.79% <0.00%> (-0.10%) ⬇️
... and 897 more

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 b27b828...d05b9c6. Read the comment docs.

@thk123 thk123 changed the title Assume relation between two int vars (issue #179) Assume relation between two symbols May 28, 2020
@thk123 thk123 force-pushed the assume-relation branch 2 times, most recently from 5d97f74 to f3e5eb9 Compare May 28, 2020 10:59
@thk123 thk123 marked this pull request as ready for review May 28, 2020 13:17
\[main\.assertion\.1\] line 8 assertion 0: UNKNOWN
\[main\.assertion\.2\] line 13 assertion 0: UNKNOWN
--
Test comparision between two symbols does not mark the
Copy link
Contributor

Choose a reason for hiding this comment

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

This is a do-not-match line, not a comment


bool is_less_than_eq(const interval_templatet &i)
{
if(i.lower_set && upper_set && upper <= i.lower)
Copy link
Contributor

Choose a reason for hiding this comment

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

if(x) return true; else return false; --> return x


bool is_less_than_eq(const interval_templatet &i)
{
if(i.lower_set && upper_set && upper <= i.lower)
Copy link
Contributor

Choose a reason for hiding this comment

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

Cross-check since there are no comments to this effect in interval_template.h: these intervals are inclusive at both ends?


void make_less_than_eq(interval_templatet &i)
{
if(upper_set && i.upper_set)
Copy link
Contributor

Choose a reason for hiding this comment

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

If my own upper bound is not set but i's is, shouldn't it now become set, and the same for i's lower bound inheriting mine?

void make_less_than(interval_templatet &i)
{
make_less_than_eq(i);
if(singleton() && i.singleton() && lower == i.lower)
Copy link
Contributor

Choose a reason for hiding this comment

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

Shouldn't this do more, too? For example, if i has max 5 and this is now always less than it, this should have max value 4, and similarly i's lower bound should be max(i.lower, lower + 1)?

Choose a reason for hiding this comment

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

@smowton It can do a lot more, but the nice thing about AI is that as long as we don’t add impossible behaviour we don’t necessarily have to do everything as precise as possible from the start (we should make it as precise as reasonable obviously, and there’s a lot of things that still could be done here).

@thk123
Copy link
Contributor Author

thk123 commented May 28, 2020

@smowton all your comments seem correct, but are a question of precision. I'm reluctant to apply since:

  • this is a valid over-approximation
  • this isn't my code
  • it should be deprecated by the new intervals in VSD

Will fix the test desc problem

@hannes-steffenhagen-diffblue
Copy link
Contributor

IIRC this wasn’t a bug fix, this was there to implement some amount of narrowing for intervals.

@thk123
Copy link
Contributor Author

thk123 commented May 29, 2020

@hannes-steffenhagen-diffblue I believe it is a bug - previously that assert in there would be marked as success (unreachable) which is not true!

@thk123 thk123 force-pushed the assume-relation branch from f3e5eb9 to 10dcdc1 Compare May 29, 2020 09:38
@thk123 thk123 merged commit 830c302 into diffblue:develop Jun 5, 2020
@thk123 thk123 deleted the assume-relation branch June 5, 2020 12:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants