Changes to intervals needed to merge VSD #5203

martin-cs · 2019-12-08T20:57:14Z

Similar to #5202 this is a series of commits pulled out of the variable-sensitivity-domain branch. As some of the patches have been squashed and cherry-picked multiple times I am not 100% sure of who wrote what but I think the full set of authors is correct. Again, squashing and editing of the commit messages are probably needed but let's look at the code first.

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.

(INT) Interval values

Also fix wrong placing of parentheses in output

As it stands in conflicted with the method from exprt

So they don't conflict with the exprt methods

Also, mark them as explicit where appropriate and add some documentation

…tions

Also replace some asserts with INVARIANT, PRECONDITION or UNREACHABLE

Also left some comments for things that need to be cleaned up in the future

Also, refactor minus and correct a typo in the comments

And also add tests for it.

and add tests for them and eval.

…val_exprt

Previously the typecast operator for interval_exprt simply set the type on the bounds; This yielded incorrect results for widening or narrowing casts. This delegates the typecast handling to simplify_expr instead.

hannes-steffenhagen-diffblue · 2020-01-31T11:36:19Z

unit/util/interval/add.cpp

@@ -0,0 +1,95 @@
+/*******************************************************************\
+ Module: Unit tests for variable/sensitivity/abstract_object::merge
+ Author: DiffBlue Limited


So it turns out it’s spelled Diffblue actually, oops.

hannes-steffenhagen-diffblue · 2020-01-31T13:46:41Z

Worth pointing out that this has... limitations w.r.t. to floating point numbers.

martin-cs · 2020-02-06T13:57:03Z

@hannes-steffenhagen-diffblue Thanks for the note about floating-point. Yes, there are still things to do on this code but I would like to get VSD merged and then improve.

thk123

There are a number of ways the intervals code could be improved to help maintainability, but in the interest of getting something merged I suggest focusing on two priorities and address the other points in due course:

ensure that testing covers 100% of the file - there is so much code here it seems like there will be a few typos that a complete set of unit tests will surely catch.
minimize and tidy the public API as this will be hard to do after the fact (as code gets added, removing it later will be harder).

I will rebase this now so that we can see the codecov report, and add a commit eliminating parts of the interface that probably aren't required.

thk123 · 2020-05-21T14:51:04Z

src/analyses/interval_domain.cpp

-      rhs_i=lhs_i;
-      if(rhs_i.is_bottom())
-        make_bottom();
+      if(id == ID_lt && !lhs_i.is_less_than(rhs_i))


❓ I'd expect to see an equivalent for ID_gt and ID_ge?

thk123 · 2020-05-21T14:54:18Z

src/util/interval.h

+  {
+  }
+
+  explicit min_exprt(const exprt &_expr) : exprt(ID_min, _expr.type())


❓ What is the reason for this constructor?

thk123 · 2020-05-21T14:55:55Z

src/util/interval.h

+    PRECONDITION(is_well_formed());
+  }
+
+  constant_interval_exprt(const constant_interval_exprt &x)


❓ Why the manual copy constructor? Seems like the default would work

thk123 · 2020-05-21T14:58:36Z

src/util/interval.h

+
+  bool is_well_formed() const
+  {
+    bool b = true;


⛏️ b-> well_formed;
💡 I'd probably just ditch the overall local variable and introduce a few locals:

const bool valid_type = is_numeric() || type.id() == ID_bool ... ... retur valid_type && matching_type && valid_bounds

thk123 · 2020-05-21T14:59:46Z

src/util/interval.h

+    return b;
+  }
+
+  bool is_valid_bound(const exprt &expr) const


⛏️ This can be static if expr.type() is used

unit/util/interval/multiply.cpp

thk123 · 2020-05-21T16:14:38Z

unit/util/interval/shift.cpp

+    WHEN("Something")
+    {
+      THEN("Something else")
+      {
+        REQUIRE(
+          constant_interval_exprt(CEV(4), CEV(8))
+            .left_shift(constant_interval_exprt(CEV(1))) ==
+          constant_interval_exprt(CEV(8), CEV(16)));
+      }
+    }


Looks incomplete and maybe tested elsewhere?

thk123 · 2020-05-21T16:16:50Z

src/util/interval_template.h

@@ -143,6 +143,47 @@ template<class T> class interval_templatet
    }
  }

+  void make_bottom()


❓ I need to see why these changes are introduced - they seem unrelated to the rest of the PR>

thk123 · 2020-05-21T16:17:19Z

src/util/interval.h

+/// or min_exprt for the lower bound
+/// or max_exprt for the upper bound
+/// Also, lower bound should always be <= upper bound
+class constant_interval_exprt : public binary_exprt


⛏️ from an "is-a" relation, I don't think an interval really is a binary expr? Not sure...

thk123 · 2020-05-21T16:27:03Z

src/util/interval.cpp

+  if(equal(get_upper(), o.get_upper()) && equal(get_upper(), o.get_upper()))
+  {
+    return tvt(true);
+  }


This seems wrong. For one, it appears to be if(A && A) and if the intention is whether upper == o.upper && lower ==o.lower, this is wrong. I think this should always be unknown unless the intersection is empty, then false, or one element, then true

TBH the semantics of this are confusing, do you expect [a, b] == [a, b] to be true or unknown The docs appear to suggest unknown, this behaviour appears to suggest true. I think depending on context you will want one or the other, so probably much safer to not guess and implement two clearly different methods: range_equal which returns true or false if the ranges are exactly the same, and value_equal which returns a tvt - but this can be left for now and fixed in the follow up PR

thk123 · 2020-05-22T15:49:24Z

However, given that the VSD is based on this interface - I think it actually makes more sense to merge this, and then tidy up the interface along with changes required to the VSD in subsequent PR. Instead i will dimiss comments to this effect - and will focus on the testing component

thk123 · 2020-06-04T09:28:56Z

#5361, a rebased version of this, has been merged. #5362 still needs to be merged (a small fix from this PR), but I'm going to close this PR in any case.

thk123 · 2020-06-05T12:48:11Z

Just noting here #5362 has now also been merged.

Daniel Neville and others added 30 commits December 8, 2019 20:49

(INT) Interval operations

b70513a

(INT) Interval values

(INT) Fix broken interval unit tests

a003056

(INT) Remove unnecessary construction of dstring

5942219

Also fix wrong placing of parentheses in output

(INT) Rename interval is_constant to is_single_value_interval

b7a7123

As it stands in conflicted with the method from exprt

(INT) Rename is_true and is_false in interval expressions

848b976

So they don't conflict with the exprt methods

(INT) Make eval take an identifier instead of an exprt

ff3dd1f

(INT) Make constructors take constant references instead of values

fe65713

Also, mark them as explicit where appropriate and add some documentation

(INT) Apply clang-format

bff9516

(INT) Remove unnecessary constant specifier from value returning func…

0ed412f

…tions

(INT) Use irep_idt in place of exprt when exprt isn't needed

6abdda2

Also replace some asserts with INVARIANT, PRECONDITION or UNREACHABLE

(INT) Cleanup to_string and operator<< for intervals

38193e1

Also left some comments for things that need to be cleaned up in the future

(INT) Give handle constants a better name

8f31842

(INT) Remove swap function in intervals

9e2e1a9

Also, refactor minus and correct a typo in the comments

(INT) Add additional unit tests for intervals

fa720e9

(INT) Various code style fixes in intervals code

dfbe6c8

(INT) Fix eval handling of ID_not case in intervals

c46f13c

And also add tests for it.

(INT) Fix bitwise operators for intervals

1458656

and add tests for them and eval.

(INT) Make eval in constant_interval_exprt const

6940fe2

(INT) Removed unimplemented function from util/interval.h

9972d79

(INT) accept false of ID_bool as valid zero value

7235a30

(INT) Add ID_bool type preconditions to logical interval operations

6497477

(INT) use tvt_to_interval instead of tv_to_interval in constant_inter…

d8c1e02

…val_exprt

(INT) Handle typecasts in constant_interval_exprt

19dbd4c

(INT) Typecast from ID_bool to integer types

3ac8c90

(INT) Addressing review comments

90ffba1

(INT) Add well-formedness checks for constant_interval_exprt

47424c0

(INT) Extend interval multiplication for extremes

bdc2b08

(INT) Add support for bit field and enums intervals.cpp

c42cac7

(INT) Fix broken interval unit tests

6cd795f

(INT) Fix bug with interval typecasts

efe4328

Previously the typecast operator for interval_exprt simply set the type on the bounds; This yielded incorrect results for widening or narrowing casts. This delegates the typecast handling to simplify_expr instead.

Petr Bauch and others added 3 commits December 8, 2019 20:49

(INT) Assume relation between two int vars (issue diffblue#179)

8d8ed40

(INT) Fixup for nil_typet being removed

1867091

(INT) Fixups post-rebase

4f76dbf

martin-cs requested review from chrisr-diffblue, danpoe, kroening, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners December 8, 2019 20:57

martin-cs mentioned this pull request Dec 9, 2019

String container stats from the VSD branch #5204

Closed

7 tasks

martin added 2 commits December 9, 2019 22:22

clang-format changes to the interval code and unit tests

d62ce16

Fixes for the linter.

d92a7db

hannes-steffenhagen-diffblue reviewed Jan 31, 2020

View reviewed changes

thk123 reviewed May 21, 2020

View reviewed changes

thk123 mentioned this pull request May 21, 2020

VSD Intervals #5354

Closed

7 tasks

thk123 mentioned this pull request May 27, 2020

Intervals with tests #5361

Merged

6 tasks

thk123 closed this Jun 4, 2020

Changes to intervals needed to merge VSD #5203

Changes to intervals needed to merge VSD #5203

Uh oh!

Conversation

martin-cs commented Dec 8, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue commented Jan 31, 2020

Uh oh!

martin-cs commented Feb 6, 2020

Uh oh!

thk123 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!

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!

thk123 commented May 22, 2020

Uh oh!

thk123 commented Jun 4, 2020

Uh oh!

thk123 commented Jun 5, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

thk123 commented Jun 5, 2020 •

edited

Loading