VSD: Simplifying abstract_objectt::write, collapsing inheritance hierarchy #5755

jezhiggins · 2021-01-16T16:33:13Z

This PR simplifies the write member function implementation in abstract_objectt subclasses. It collapses the inheritance hierarchy for classes modelling aggregate values (arrays, structs, unions), eliminating duplication.

Several classes were named to better reflect their purpose - eg union_abstract_objectt became two_value_union_abstract_objectt, and some new classes introduced to in place of a previously existing base class, eg two_value_array_abstract_objectt in place of the eliminated array_abtract_objectt.

This allowed further work to combine interval_array_abstract_objectt and constant_array_abstract_objectt together. The combined implementation has been renamed full_array_abstract_objectt, and the implementation refactored for reading comprehension.

This PR is behaviour preserving. No need functionality is introduced.

codecov · 2021-01-17T18:05:16Z

Codecov Report

Merging #5755 (d9f7b72) into develop (f2fafac) will increase coverage by 0.02%.
The diff coverage is 88.20%.

@@             Coverage Diff             @@
##           develop    #5755      +/-   ##
===========================================
+ Coverage    69.64%   69.67%   +0.02%     
===========================================
  Files         1248     1242       -6     
  Lines       100911   100875      -36     
===========================================
- Hits         70284    70282       -2     
+ Misses       30627    30593      -34

Flag	Coverage Δ
cproversmt2	`43.36% <ø> (ø)`
regression	`66.63% <83.77%> (+<0.01%)`	⬆️
unit	`32.30% <57.52%> (+0.11%)`	⬆️

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

Impacted Files	Coverage Δ
...alyses/variable-sensitivity/abstract_environment.h	`100.00% <ø> (ø)`
...rc/analyses/variable-sensitivity/abstract_object.h	`88.46% <ø> (-2.97%)`	⬇️
...s/variable-sensitivity/pointer_abstract_object.cpp	`85.71% <ø> (ø)`
...-sensitivity/value_set_pointer_abstract_object.cpp	`60.00% <ø> (+26.66%)`	⬆️
...le-sensitivity/value_set_pointer_abstract_object.h	`0.00% <ø> (ø)`
...variable-sensitivity/variable_sensitivity_domain.h	`100.00% <ø> (ø)`
...-sensitivity/variable_sensitivity_object_factory.h	`100.00% <ø> (ø)`
...es/variable-sensitivity/write_location_context.cpp	`96.82% <ø> (ø)`
.../analyses/variable-sensitivity/write_stack_entry.h	`100.00% <ø> (ø)`
...riable-sensitivity/full_struct_abstract_object.cpp	`81.90% <63.63%> (+2.46%)`	⬆️
... and 30 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 f2fafac...d9f7b72. Read the comment docs.

martin-cs

I don't see any immediate show stoppers but this is quite a substantial refactor and it would be good to work through the code-base with you before we merge this PR.

martin-cs · 2021-01-18T15:25:41Z

src/analyses/variable-sensitivity/abstract_enviroment.cpp

  else if(
    simplified_id == ID_array || simplified_id == ID_struct ||
-    simplified_id == ID_constant)
+    simplified_id == ID_constant || simplified_id == ID_address_of)


It is true that it is handled the same but it is for quite different reasons. This is not necessarily a problem, but it is something to be aware of.

martin-cs · 2021-01-18T15:37:14Z

src/analyses/variable-sensitivity/abstract_aggregate_object.h

+
+class member_exprt;
+
+template<class aggregate_typet, class aggregate_traitst>


This is probably a bit more template-y than we normally write but under the circumstances I can see this reduces an amount of duplication.

It's compile type polymorphism rather than run-time. We don't need, actually don't want, run-time polymorphism here.

martin-cs · 2021-01-18T15:56:18Z

src/analyses/variable-sensitivity/interval_array_abstract_object.cpp

-      merging_write);
-  }
-  else if(
+  if(
    !index_interval.is_top() && !index_interval.is_bottom() &&
    index_interval.get_lower().id() != ID_min &&
    index_interval.get_upper().id() != ID_max)


Although not touched by this PR, this case really should result in the interval being top.

martin-cs · 2021-01-18T15:57:30Z

src/analyses/variable-sensitivity/abstract_value_object.h

+  }
+};
+
+#endif


martin-cs · 2021-01-18T15:58:03Z

src/analyses/variable-sensitivity/abstract_value_object.h

+
+#include <analyses/variable-sensitivity/abstract_object.h>
+
+class abstract_value_tag { };


I'm not sure I follow why this is needed...

I'd initially expected abstract_value_objectt to be a template in a similar way to abstract_aggregate_objectt. Didn't turn out that way, although may yet with the next bit of work. Happy to remove this now if you'd prefer.

martin-cs · 2021-01-18T16:01:43Z

src/analyses/variable-sensitivity/interval_abstract_value.cpp

+  if (is_top() || is_bottom() || interval.is_top() || interval.is_bottom())
+    return std::make_shared<empty_index_ranget>();
+  if (interval.get_lower().id() == ID_min || interval.get_upper().id() == ID_max)
+    return std::make_shared<empty_index_ranget>();


I get that if the interval is bottom you should get an empty range but I'm not sure I get why this is the case for top or if the interval is open at one end.

It doesn't make sense to me either, but this is the existing behaviour.

martin-cs · 2021-01-18T16:04:15Z

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

@@ -40,14 +40,18 @@ SCENARIO(
    }
  }

-  GIVEN("a top constant's range is empty")
+  GIVEN("a top constant's range is has a single nil expression")


If it tis top then it should be everything so this is definitely an improvement but I'm not quite sure what the nil is supposed to describe.

The index_range is only used to during array access, and this supports the existing behaviour. Returning a nil expression here takes us down to https://github.com/jezhiggins/cbmc/blob/b618d2e3703434aa0cfb4d1c991c867b1dea9955/src/analyses/variable-sensitivity/full_array_abstract_object.cpp#L298
It is a special case, but it's isolated here rather than having to be explicitly handed in potentially several places elsewhere. As we look to expand other value representations, the more we can keep within those representations, the better.

martin-cs · 2021-01-18T16:11:22Z

src/analyses/variable-sensitivity/abstract_object.h

@@ -443,18 +443,6 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
  /// abstraction anyway
  bool should_use_base_meet(const abstract_object_pointert &other) const;

-  template <class keyt>


Good tidy up.

martin-cs · 2021-01-18T16:15:30Z

src/analyses/variable-sensitivity/full_array_abstract_object.cpp

@@ -272,113 +270,137 @@ abstract_object_pointert full_array_abstract_objectt::write_element(
      environment, ns, stack, expr, value, merging_write);
  }

+  if(!stack.empty())


It's not entirely clear to me why this is needed. Can't you just delegate the write to the relevant abstract_object and then update the relevant entry with whatever it returns?

No, because once we get to the end of the stack we need to worry about whether it's a merging write or not. Higher up the stack, we don't need to do that.

We have a similar decision point in full_struct_abstract_objectt, and I assume we'll have one in our union representation when we fill that out. When we get there, it's entirely possible we'll be able to collapse the implementations.

martin-cs · 2021-01-18T16:18:03Z

src/analyses/variable-sensitivity/full_array_abstract_object.cpp

@@ -376,13 +376,10 @@ abstract_object_pointert full_array_abstract_objectt::write_leaf_element(
    }
    else
    {
-      auto const old_value = result->map.find(index_value);
+      auto old_value = result->map.find(index_value);
      if(old_value.has_value())


It may not change the value that is stored but breaking sharing is a serious concern. Please check that the sharing map does actually handle that case correctly.

martin-cs · 2021-01-22T16:31:46Z

I've had a discussion with @jezhiggins and I am in favour of merging this because:

It is at least an intermediate step towards sorting this code out.
It is code that I requested we merge "to be improved in tree".
It makes things simpler.
It is a pure refactoring. Jez has very intentionally preserved functionality, even when questionable.

martin-cs · 2021-01-25T16:42:14Z

@tautschnig @peterschrammel This is part of the refactor and tidy up of VSD. I don't expect you to look at that part of the commit, i think it is a net improvement and there is more to do. Please could you have a look at the changes in other parts of the tree, notably `util/' which are blocking the merge.

tautschnig

Some administrative comments only, I have browsed (but not properly reviewed) the code in analyses/ and focussed on the single change in src/util/ only.

tautschnig · 2021-01-26T20:44:33Z

src/analyses/variable-sensitivity/abstract_enviroment.cpp

 #include <util/pointer_expr.h>
+#include <language_util.h>


Seems surprising?

tautschnig · 2021-01-26T20:49:22Z

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -14,7 +14,7 @@
 #include <analyses/variable-sensitivity/two_value_struct_abstract_object.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 #include <util/pointer_expr.h>
-#include <language_util.h>
+#include <langapi/language_util.h>


Why is this file being included?

Good question - looking at now, I probably included for some debug/dev code which didn't need to be committed. I'll tidy this up.

tautschnig · 2021-01-26T20:52:10Z

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

@@ -0,0 +1,53 @@
+#include <analyses/variable-sensitivity/abstract_environment.h>


Quoting CODING_GUIDELINES.md: "Each source and header file must start with a comment block stating the author."

tautschnig · 2021-01-26T20:54:53Z

src/analyses/variable-sensitivity/abstract_value_object.cpp

@@ -0,0 +1,47 @@
+#include <analyses/variable-sensitivity/abstract_value_object.h>


See earlier comment: please make sure all files include a header stating the author.

tautschnig · 2021-01-26T20:56:49Z

src/analyses/variable-sensitivity/full_array_abstract_object.cpp

@@ -14,6 +14,12 @@

 #include "full_array_abstract_object.h"

+bool eval_index(


Should likely be static as only required within this file.

tautschnig · 2021-01-26T20:59:45Z

src/util/sharing_map.h

+  sorted_viewt get_sorted_view() const
+  {
+    sorted_viewt result;
+    get_view(result);
+    return result;
+  }


Would you mind adding documentation? It may be ok to put the three methods in a group, but there should be some sort of documentation.

tautschnig · 2021-01-26T21:02:08Z

src/analyses/variable-sensitivity/abstract_object.h

+  static abstract_object_pointert merge(
+    abstract_object_pointert op1,
+    abstract_object_pointert op2);


How about changing the interface to make merge return a pair?

I did try it, but it didn't really make the code any clearer. If structured bindings were available, I'd absolutely have gone for it.

… identical

Each case returns, so there's no fall-through to further processing. Removing the _else if_ in favour of plain _if_ is functionally identical but with less visual clutter.

…set_abstract_object

…ay abstract_object

…empty range

Reduced visibility, collapses common implementations, added factory methods.

Array representation is now independent of value representation. Renamed constant_array_abstract_object to full_array_abstract_object. Eliminated interval_array_abstract_object.

Not used in the code, and in any case now redundant as full_array_ works happily with value-sets.

…ad_component

…merge_maps

…ether op1 was modified

…f_element

if(value != abstract_object_pointert{old_value.value()}) I don't see that this test can ever fail, and even if it does the operation we're guarding against is benign

jezhiggins force-pushed the vsd-merge-and-eval branch 6 times, most recently from ec33346 to b27896b Compare January 17, 2021 17:30

jezhiggins force-pushed the vsd-merge-and-eval branch 2 times, most recently from 3c4977a to 5a328d4 Compare January 17, 2021 20:28

jezhiggins marked this pull request as ready for review January 17, 2021 22:04

jezhiggins requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners January 17, 2021 22:04

jezhiggins force-pushed the vsd-merge-and-eval branch from 5a328d4 to b618d2e Compare January 17, 2021 23:16

martin-cs approved these changes Jan 18, 2021

View reviewed changes

jezhiggins force-pushed the vsd-merge-and-eval branch from b618d2e to 82d5dfa Compare January 19, 2021 11:21

jezhiggins force-pushed the vsd-merge-and-eval branch 3 times, most recently from d134e80 to 6c5f28a Compare January 22, 2021 18:35

tautschnig approved these changes Jan 26, 2021

View reviewed changes

jezhiggins added 5 commits January 27, 2021 10:40

Fold ID_address_of into ID_array/ID_struct/ID_constant case. They are…

5b4f40f

… identical

Factored out abstract_environmentt::resolve_symbol

dbad4e5

abstract_environmentt::eval unpicked if ladder

ef31be2

Each case returns, so there's no fall-through to further processing. Removing the _else if_ in favour of plain _if_ is functionally identical but with less visual clutter.

Simplified abstract_environmentt::write - all cases were equivalent

6e35c3b

collapse equivalent cases in abstract_environmentt::assign

bb0b1fe

jezhiggins added 28 commits January 27, 2021 10:40

Introduce abstract_value_objectt as base for constant/interval/value_…

ff4aa07

…set_abstract_object

Starting work on index_range, first step along that path a single arr…

e7f7239

…ay abstract_object

input_range for interval_abstract_values

402809c

index_range needs namespacet passed in

0585702

Rework interval_array_...::write_component to using index_range

ab30d0c

Rework interval_array_...::read_component to use index_range

ce3eb0b

If the expression is not constant that's an inderminate range not an …

19b324e

…empty range

Remove interval_array_abstract_object::eval_index override

8e317ba

Implemented value_set_index_ranget

703c97f

Refactoring index_ranget and its subclasses

053df78

Reduced visibility, collapses common implementations, added factory methods.

Combine constant_array_ & interval_array_ implementations

fdd5712

full_array_abstract_object

5a5d4c1

Array representation is now independent of value representation. Renamed constant_array_abstract_object to full_array_abstract_object. Eliminated interval_array_abstract_object.

Removed value_set_array_abstract_objectt

aa9925f

Not used in the code, and in any case now redundant as full_array_ works happily with value-sets.

eval_index doesn't need to be a member function

a439481

Factor common index loop out of full_array_abstract_object::write_/re…

55b477d

…ad_component

get_top_entry instead big abstract_object_factory call

058ffd7

Use get_view()/get_sorted_view() instead of get_view(&view)

3168916

Hoist is_top check from read_element to read_component

886829c

Moved merged_sharing_maps into abstract_aggregate_object. Eliminated …

2a3f4cd

…merge_maps

use abstract_objectt::merge(op1, op2) when we're not interested in wh…

56370a7

…ether op1 was modified

Split full_array_::write_element into write_sub_element and write_lea…

27543d8

…f_element

Removed redundant if guard

33021a3

if(value != abstract_object_pointert{old_value.value()}) I don't see that this test can ever fail, and even if it does the operation we're guarding against is benign

Arrange write checks so everything if(not value) replace else insert

b04f5c8

clang-format fixes

1c18b88

Updated expected doxygen warnings

c5248bd

Fix doxygen warning

f332df8

Add header block

cc75d94

remove extraneous include

d9f7b72

jezhiggins force-pushed the vsd-merge-and-eval branch from 0b39442 to d9f7b72 Compare January 27, 2021 10:40

martin-cs merged commit a6a0729 into diffblue:develop Jan 28, 2021


		class member_exprt;

		template<class aggregate_typet, class aggregate_traitst>

+                }
+              };
+              #endif


		#include <analyses/variable-sensitivity/abstract_object.h>

		class abstract_value_tag { };

		@@ -0,0 +1,53 @@
		#include <analyses/variable-sensitivity/abstract_environment.h>

		@@ -0,0 +1,47 @@
		#include <analyses/variable-sensitivity/abstract_value_object.h>

		@@ -14,6 +14,12 @@

		#include "full_array_abstract_object.h"

		bool eval_index(

VSD: Simplifying abstract_objectt::write, collapsing inheritance hierarchy #5755

VSD: Simplifying abstract_objectt::write, collapsing inheritance hierarchy #5755

Uh oh!

Conversation

jezhiggins commented Jan 16, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Jan 17, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jezhiggins Jan 19, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Jan 22, 2021

Uh oh!

martin-cs commented Jan 25, 2021

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

jezhiggins commented Jan 16, 2021 •

edited

Loading

codecov bot commented Jan 17, 2021 •

edited

Loading

jezhiggins Jan 19, 2021 •

edited

Loading