Variable sensitivity domain #5472

martin-cs · 2020-08-24T21:34:40Z

This PR merges in several years of work on a new domain for the abstract interpreter. It should solve a number of the long-standing problems with soundness and precision. The key feature of the domain is that the abstraction used for each type can be selected at run-time, allowing a wide range of scalability / precision trade-offs and easy specialisation without having to re-write all of the array, field, pointer sensitivity, etc.

This is the work of a lot of people, notably @thk123 @chrisr-diffblue @hannes-steffenhagen-diffblue @danpoe @NlightNFotis and others. I have tried to preserve authorship where-ever possible.
I don't think it is reasonable to try to review this in the normal way, nor do I think it is viable to split it up further. Whether it gets merged or not has to be a policy question really. Over the years this has been going on I have asked @peterschrammel and @tautschnig about this as an approach and they seemed supportive because...
The PR should have very little impact on existing functionality, it is enabled with an option in goto-analyzer. It has also been deployed in at least two industrial applications.
There is still work to be done in tidying up the code but I think it can be and would be best done as PRs to it after merging. I will try to do some during the discussion / review.
This includes Changes to sharing-map needed to merge VSD #5202 and String container stats from the VSD branch #5204 which were previous attempts at splitting this out a bit.
I don't know who is currently looking after
https://github.com/diffblue/cbmc/tree/variable-sensitivity-domain
and
https://github.com/diffblue/cbmc/tree/variable-sensitivity-with-get-function-pointers
( @chrisr-diffblue ? @danpoe ? @hannes-steffenhagen-diffblue ? )
but this PR includes the majority of the content of these. I have a branch of the remainder and am happy to work with people to rebase that on top of this PR.

Let me know what you think!

martin-cs · 2020-08-24T23:40:16Z

The unit tests currently don't compile (oops!). I note that "AWS CodeBuild us-east-1 (cbmc-windows-cmake)" passes; is it supposed to skip / ignore the unit tests?

peterschrammel · 2020-08-25T16:53:40Z

Happy to review if you make the monster pass CI first.

peterschrammel · 2020-08-25T16:54:36Z

is it supposed to skip / ignore the unit tests?

It probably isn't. @hannes-steffenhagen-diffblue ?

martin-cs · 2020-08-25T17:47:06Z

@peterschrammel Thank you, I think it is just the unit tests which are outstanding. All the regression tests and linting, formatting, etc. all pass. I will update the usage of exprt in the unit tests and ping you.

hannes-steffenhagen-diffblue · 2020-08-25T19:02:13Z

@martin-cs @peterschrammel The cmake windows build is currently not running any tests actually. This is a long outstanding bug which is one of the things we're hoping to "fix" with our "move CI to github actions" work.

martin-cs · 2020-08-25T19:41:20Z

@hannes-steffenhagen-diffblue cool, as long as this isn't news to you!

martin-cs · 2020-08-25T20:27:53Z

@hannes-steffenhagen-diffblue you probably already know this but it looks like "AWS CodeBuild us-east-1 (cbmc-clang-3-8)" doesn't run any tests either.

codecov · 2020-08-26T00:41:12Z

Codecov Report

Merging #5472 (22f775c) into develop (27f2a8a) will increase coverage by 0.28%.
The diff coverage is 79.03%.

@@             Coverage Diff             @@
##           develop    #5472      +/-   ##
===========================================
+ Coverage    68.53%   68.82%   +0.28%     
===========================================
  Files         1187     1241      +54     
  Lines        98263   100447    +2184     
===========================================
+ Hits         67347    69128    +1781     
- Misses       30916    31319     +403

Flag	Coverage Δ
cproversmt2	`43.05% <ø> (-0.05%)`	⬇️
regression	`65.75% <73.55%> (+0.04%)`	⬆️
unit	`32.23% <34.46%> (-0.04%)`	⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/analyses/ai_storage.h	`70.17% <ø> (+1.75%)`	⬆️
.../variable-sensitivity/abstract_object_statistics.h	`0.00% <0.00%> (ø)`
...ses/variable-sensitivity/union_abstract_object.cpp	`0.00% <0.00%> (ø)`
...lyses/variable-sensitivity/union_abstract_object.h	`0.00% <0.00%> (ø)`
...able-sensitivity/value_set_array_abstract_object.h	`0.00% <0.00%> (ø)`
...le-sensitivity/value_set_pointer_abstract_object.h	`0.00% <0.00%> (ø)`
...-sensitivity/value_set_pointer_abstract_object.cpp	`23.07% <23.07%> (ø)`
...le-sensitivity/value_set_array_abstract_object.cpp	`27.27% <27.27%> (ø)`
...c/analyses/variable-sensitivity/abstract_value.cpp	`33.33% <33.33%> (ø)`
src/analyses/variable-sensitivity/abstract_value.h	`33.33% <33.33%> (ø)`
... and 102 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 27f2a8a...22f775c. Read the comment docs.

martin-cs · 2020-08-26T01:01:10Z

@peterschrammel All of CI now passes, any kind of review would be most appreciated.

peterschrammel

A shallow review of 20KLOC to scan for red flags. The PR is in pretty good state code quality-wise - ie acceptable to be merged. The main concern are outdated documentation formats that need to be fixed so that the doxygen documentation is produced correctly. Also, some copyright headers don't follow the guidelines and must be fixed before merge.

peterschrammel · 2020-08-26T17:18:04Z

regression/goto-analyzer-simplify/simplify-lhs-pointer-array-dereference/main.c

+
+  // TODO: Currently writing to an offset pointer sets the domain to top
+  // so recreate the variables to reign the domain back in
+  // This will be addressed by diffblue/cbmc-toyota#118


⛏️ I don't think this reference is publically accessible.

peterschrammel · 2020-08-26T17:22:17Z

src/analyses/variable-sensitivity/abstract_enviroment.cpp

+
+ Purpose: Evaluate the value of an expression relative to the current domain
+
+\*******************************************************************/


❗ Outdated comment headers. This needs replacing - if not in this PR than immediately as a follow-up.

I have reformatted all of them.

peterschrammel · 2020-08-26T17:23:52Z

src/analyses/variable-sensitivity/abstract_enviroment.cpp

+ what kind of array abstraction it is).  So, as we find the variable
+ ('a' in this case) we build a stack of which part of it is accessed.
+
+ As abstractions may split the assignment into multiple write (for


⛏️

Suggested change

As abstractions may split the assignment into multiple write (for

As abstractions may split the assignment into multiple writes (for

Fixed. Thanks.

peterschrammel · 2020-08-26T17:25:33Z

src/analyses/variable-sensitivity/abstract_enviroment.cpp

+    // to be none of that.
+    if(s.id() != ID_symbol)
+    {
+      throw "invalid l-value";


❓ What is an i-value?

? Is this a font issue? The source says l-value as in https://en.wikipedia.org/wiki/Value_(computer_science)#lrvalue

peterschrammel · 2020-08-26T17:27:07Z

src/analyses/variable-sensitivity/abstract_enviroment.cpp

+
+  /* TODO : full implementation here
+   * Note that this is *very* syntax dependent so some normalisation would help
+   * 1. split up conjucts, handle each part separately


Suggested change

* 1. split up conjucts, handle each part separately

* 1. split up conjuncts, handle each part separately

peterschrammel · 2020-08-26T18:13:48Z

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -129,7 +130,17 @@ class optionst;
  "(intervals)" \
  "(non-null)" \
  "(constants)" \
-  "(dependence-graph)"
+  "(dependence-graph)" \


💡 dependency-graph seems to be more common.

Yes but this is what the class in question is called and it has been a command-line option for some time. I'm happy to change it but I don't think it should be part of this PR.

peterschrammel · 2020-08-26T18:17:24Z

unit/analyses/variable-sensitivity/abstract_object/merge.cpp

+
+ Module: Unit tests for variable/sensitivity/abstract_object::merge
+
+ Author: DiffBlue Limited. All rights reserved.


❗

Suggested change

Author: DiffBlue Limited. All rights reserved.

Author: Diffblue Limited.

peterschrammel · 2020-08-26T18:18:42Z

unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp

+
+ Module: Unit tests for constant_abstract_valuet::merge
+
+ Author: DiffBlue Limited. All rights reserved.


peterschrammel · 2020-08-26T18:19:22Z

unit/analyses/variable-sensitivity/constant_array_abstract_object/merge.cpp

+
+ Module: Unit tests for constant_array_abstract_object::merge
+
+ Author: DiffBlue Limited. All rights reserved.


❗ (and all other files)

peterschrammel · 2020-08-26T18:20:06Z

unit/analyses/variable-sensitivity/eval.cpp

@@ -0,0 +1,100 @@
+// Copyright 2016-2020 Diffblue Limited. All Rights Reserved.


martin-cs · 2020-09-08T12:17:49Z

@peterschrammel I need to move various doxygen comments into the headers but otherwise I should be done with the requested changes. Let me know if there are more.

@chrisr-diffblue, @danpoe, @hannes-steffenhagen-diffblue : you know this code, any chance of a review?

martin-cs · 2020-09-09T11:46:49Z

@peterschrammel I have moved the doxygen comments to the headers. Modulo fixing any issues doxygen has, I think I'm done.

martin-cs · 2020-09-14T14:29:16Z

@peterschrammel Are the changes OK?

@danpoe @hannes-steffenhagen-diffblue @smowton you are owners for this area, please can you say something about this. I don't think an in-depth review is appropriate but some kind of comment would help.

@owen-mc-diffblue If I understand correctly, you were an owner under a different name that hasn't been updated in CODEOWNERS. Please can you comment?

peterschrammel · 2020-09-14T14:35:56Z

@martin-cs, lgtm modulo the doxygen issues: https://travis-ci.org/github/diffblue/cbmc/jobs/725557168

martin-cs · 2020-09-14T14:39:40Z

Thanks @peterschrammel I will work through the doxygen issues once I have it set up on my machine.

martin-cs · 2020-09-22T13:45:16Z

The doxygen issues should be finished. I think it's just waiting on a stalled CI job.

This requires a few legacy contortions similar to the ones done in dependency graph.

These are due to new global variables being added to __CPROVER_initialise

The N_CATCH_TESTS check in the Makefile found this!

In a previous commit I fixed a bug where the default state of a constructed abstract_environment was top rather than bottom. Correcting this meant this unit test fails as the environment will only return objects which are bottom. Also improve the tagging of the test.

Thankfully the names of the variables and the description of the tests makes it clear that this was a typo. Documentation FTW!

A recent PR has removed a couple of the in-built global variables that are used for modelling the C standard library. This has a knock on effect for the line numbers in the tests of dependency graphs.

This was inefficient but now causes build failures on OS X as it uses -Werror -Wrange-loop-analysis

NlightNFotis · 2020-11-11T12:00:25Z

This PR looks to be in a good state, and it's mergeable. Is there anything outstanding on it? If not, I can merge it now.

martin-cs · 2020-11-11T15:20:41Z

@NlightNFotis Thanks. There are still quite a few refactorings, fixes, improvements, etc. that we will be making but TBH I would rather merge this and have these as separate PRs so they are easier to review. The code in this PR works, has been deployed, has a higher test coverage than the rest of the project -- let's get it merged. Plus it would be good to acknowledge everyone's hard work on this.

While we are on the subject, do you / @hannes-steffenhagen-diffblue / @chrisr-diffblue / @peterschrammel want / need any of the rest of the code from this branch? I have a branch with it in, partially ready to be converted into PRs and I'm happy to work with people to do that but it is not a high priority if it is just me.

peterschrammel · 2020-11-11T16:27:51Z

@martin-cs, it's favourable to get any (valuable) code that is lying around in branches in various forks into the shape of PRs eventually. It's shame when a lot of work has been done and then it rots and dies... and someone else starts reimplementing something similar...

martin-cs · 2020-11-11T16:31:03Z

@peterschrammel agreed it is a question of priorities and time. I could make them into draft PRs but they are unlikely to make mergable without someone else getting involved.

NlightNFotis · 2020-11-11T23:20:03Z

@martin-cs I think there is value for the draft PRs to be made - if we can find some time we can shape them up to be more mergeable.

Obviously, I cannot give guarantees for when that is, as it depends on a lot of things, but if the PRs are there, they are much more likely to be picked up by someone.

thk123 · 2020-11-12T10:05:39Z

😮 Never thought I'd see the day - can't let it go without commenting! 🎉 🎉 🎉

Hope you're all well

smowton · 2020-11-12T10:22:12Z

Signs of the end times:
[x] POTUS refusing to leave the white house
[x] The variable-sensitivity domain has been merged
[ ] Rains of branston pickle

chrisr-diffblue · 2020-11-12T10:50:23Z

This really should have been merged on 1st April....

hannes-steffenhagen-diffblue · 2020-11-12T10:50:50Z

Hello @thk123 and @smowton, nice to hear from you! I hope you're all well too!

martin-cs · 2020-11-12T10:53:03Z

@chrisr-diffblue ... I should have thought of that ... sigh

peterschrammel · 2020-11-12T12:09:39Z

11/11 11:11 is the beginning of carnival...

martin-cs requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners August 24, 2020 21:34

martin-cs force-pushed the refactor/VSD-with-history-2 branch from 9a99b5b to df1b79c Compare August 25, 2020 19:40

martin-cs force-pushed the refactor/VSD-with-history-2 branch from ed13b18 to f6dacb0 Compare August 25, 2020 22:43

peterschrammel reviewed Aug 26, 2020

View reviewed changes

martin-cs force-pushed the refactor/VSD-with-history-2 branch from 8595305 to f0e5f58 Compare September 8, 2020 12:14

martin-cs force-pushed the refactor/VSD-with-history-2 branch from f0e5f58 to 3f7ed08 Compare September 8, 2020 12:22

peterschrammel approved these changes Sep 14, 2020

View reviewed changes

martin-cs force-pushed the refactor/VSD-with-history-2 branch from 6bd0bb2 to 17c9d8f Compare September 25, 2020 11:21

martin added 15 commits November 10, 2020 21:35

Use three-way merge in the VSD dependency graph

74bc496

This requires a few legacy contortions similar to the ones done in dependency graph.

Update the VSD dependency graph tests for line number changes

57e7d01

These are due to new global variables being added to __CPROVER_initialise

Update unit tests for the improved, type safe(r) exprts

516567f

Tweak the VSDG to fix a clang specific warning about get_state

3322378

One of the new unit tests was omitted from the source list

69d5367

The N_CATCH_TESTS check in the Makefile found this!

Correct a typo in the creation of an interval

593eec7

Thankfully the names of the variables and the description of the tests makes it clear that this was a typo. Documentation FTW!

Remove reference to non-public issue tracker

8917763

Convert comments to the new(er) doxygen format

4608220

Reformat so that comments pass linting

3a1c7ca

Apply Peter Schrammel's review comments

0d80676

Move doxygen comments from .cpp to .h files

12b273e

Fix issues and warnings raised by doxygen

7a72940

Update regression tests to cope with changes to initialisation

41606b0

A recent PR has removed a couple of the in-built global variables that are used for modelling the C standard library. This has a knock on effect for the line numbers in the tests of dependency graphs.

s/const auto/const auto &/ in loops

22f775c

This was inefficient but now causes build failures on OS X as it uses -Werror -Wrange-loop-analysis

martin-cs force-pushed the refactor/VSD-with-history-2 branch from edbdc4f to 22f775c Compare November 10, 2020 21:36

NlightNFotis merged commit ac9c634 into diffblue:develop Nov 11, 2020

This was referenced Feb 11, 2021

[depends: #472] Variable Sensitivity Domain #708

Closed

Vsd value set implementation #5793

Merged


		Purpose: Evaluate the value of an expression relative to the current domain

		\*******************************************************************/

	As abstractions may split the assignment into multiple write (for
	As abstractions may split the assignment into multiple writes (for

	* 1. split up conjucts, handle each part separately
	* 1. split up conjuncts, handle each part separately


		Module: Unit tests for variable/sensitivity/abstract_object::merge

		Author: DiffBlue Limited. All rights reserved.

	Author: DiffBlue Limited. All rights reserved.
	Author: Diffblue Limited.


		Module: Unit tests for constant_abstract_valuet::merge

		Author: DiffBlue Limited. All rights reserved.


		Module: Unit tests for constant_array_abstract_object::merge

		Author: DiffBlue Limited. All rights reserved.

		@@ -0,0 +1,100 @@
		// Copyright 2016-2020 Diffblue Limited. All Rights Reserved.

Variable sensitivity domain #5472

Variable sensitivity domain #5472

Conversation

martin-cs commented Aug 24, 2020

martin-cs commented Aug 24, 2020

peterschrammel commented Aug 25, 2020

peterschrammel commented Aug 25, 2020

martin-cs commented Aug 25, 2020

hannes-steffenhagen-diffblue commented Aug 25, 2020

martin-cs commented Aug 25, 2020

martin-cs commented Aug 25, 2020

codecov bot commented Aug 26, 2020 • edited Loading

Codecov Report

martin-cs commented Aug 26, 2020

peterschrammel left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs commented Sep 8, 2020

martin-cs commented Sep 9, 2020

martin-cs commented Sep 14, 2020

peterschrammel commented Sep 14, 2020

martin-cs commented Sep 14, 2020

martin-cs commented Sep 22, 2020

NlightNFotis commented Nov 11, 2020

martin-cs commented Nov 11, 2020

peterschrammel commented Nov 11, 2020

martin-cs commented Nov 11, 2020

NlightNFotis commented Nov 11, 2020

thk123 commented Nov 12, 2020

smowton commented Nov 12, 2020

chrisr-diffblue commented Nov 12, 2020

hannes-steffenhagen-diffblue commented Nov 12, 2020

martin-cs commented Nov 12, 2020

peterschrammel commented Nov 12, 2020

codecov bot commented Aug 26, 2020 •

edited

Loading

peterschrammel left a comment •

edited

Loading