Intervals with tests by thk123 · Pull Request #5361 · diffblue/cbmc

thk123 · 2020-05-27T17:47:19Z

A note to reviewers, this PR, though large, is entirely an isolated addition util/interval. There are lots of ways this code could be improved (I've listed some in #5203) since VSD is based on top of this, I propose merging as is, and then applying fixes after - so I'd encourage not going through this with a fine tooth comb to find the ways it is wrong!

This is a rebase of #5203 that addresses I believe the most pressing issues:

ensures all tests are run on Make and CMake builds
fixes the errors in operator== that stops the tests actually checking things properly
fixes error in to string
adds a lot of tests for the missing coverage (still some gaps)
highlight some areas where the behavior is wrong
fixes bug in eval(ID_minus)
Some gaps in the tests remain:

logical_or / logical_and / logical_xor
I believe these functions should be removed, and there just be a single method to get the range as a tvt, and then have these functions implemented on tvt. As such, I didn't write the tests.

code in the generate_* and append_* functions
The semantics of these aren't clear to me, and shouldn't be part of the public interface. Probably the code that is uncovered will be hard to cover if the interface is tidier

trivial type getters and constructors
There are loads of these, and they mostly need to be deleted. To avoid breaking, I recommend waiting until VSD is merged before deleting. However, not worth testing in the meantime.

wrappers
interval.cpp implements all of the calling conventions. This wants tidying up, but in the meantime I've not bothered to test every possible calling syntax.

typecast
This is worth testing, but I don't understand what it's doing and it seems fishy. However, it is used in VSD so I'll leave for now, so it can be tested / removed after VSD is merged.

TBH in the brief time I've spent with this, there are a bunch of bugs and inconsistencies here, if there wasn't a mountain of work built on top of it, I'd recommend breaking this into something smaller than works (e.g. remove the untested or broken functionality). However, this isn't really an option, so I suggest we merge like this, merge VSD and perhaps immediately remove the interval portion of the VSD, along with this, and reintroduce it gradually (allowing at least the bulk of VSD to be merged).

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.

codecov · 2020-05-27T18:22:11Z

Codecov Report

Merging #5361 into develop will increase coverage by 0.00%.
The diff coverage is 68.36%.

@@            Coverage Diff            @@
##           develop    #5361    +/-   ##
=========================================
  Coverage    68.14%   68.14%            
=========================================
  Files         1171     1173     +2     
  Lines        96641    97333   +692     
=========================================
+ Hits         65858    66331   +473     
- Misses       30783    31002   +219

Flag	Coverage Δ
#cproversmt2	`42.47% <ø> (ø)`
#regression	`65.36% <ø> (-0.01%)`	⬇️
#unit	`32.18% <68.36%> (+0.36%)`	⬆️

Impacted Files	Coverage Δ
src/util/interval.cpp	`66.92% <66.92%> (ø)`
src/util/interval.h	`100.00% <100.00%> (ø)`
src/solvers/strings/string_builtin_function.h	`74.39% <0.00%> (-2.44%)`	⬇️
src/util/threeval.h	`85.71% <0.00%> (-1.79%)`	⬇️
src/pointer-analysis/value_set_fi.h	`97.56% <0.00%> (+2.43%)`	⬆️

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...1d92ca0. Read the comment docs.

thk123 · 2020-05-28T08:57:28Z

I've added test for binary eval (And found a bug in the process 😑), will add one for to_string since it also originally contained a bug and then this PR I believe is ready

thk123 · 2020-05-28T09:20:50Z

Added to_string tests and squashed clang format changes into the original commit that introduces them

thk123 · 2020-05-28T09:37:45Z

Removed the changes to interval_template, one into separate PR: #5362, the other changes essentially cancelled themselves out, so I just removed them both.

thk123 · 2020-05-28T13:10:20Z

CI failure is lint - will fix, but ready for review

smowton

Some things to check, but as you say happy to get this in then fix it up subsequently. I didn't look at the big "fix crap after rebase" commit or the huge 2000-line "add intervals" one due to lack of time.

smowton · 2020-05-28T14:16:50Z

unit/util/interval/to_string.cpp

@@ -0,0 +1,52 @@
+/*******************************************************************\
+ Module: Unit tests for variable/sensitivity/abstract_object::merge


Wrong header

smowton · 2020-05-28T14:21:00Z

unit/util/interval/eval.cpp

+    REQUIRE(five.eval(ID_minus, eight) == interval_of(-3));
+    REQUIRE(five.eval(ID_mult, eight) == interval_of(40));
+    REQUIRE(five.eval(ID_div, eight) == interval_of(0));
+    REQUIRE(five.eval(ID_mod, eight) == interval_from_to(0, 5));


Checking this oddity is known

It is but i've added a comment to highlight it.

smowton · 2020-05-28T14:22:46Z

unit/util/interval/eval.cpp

  }
 }
+
+TEST_CASE("binary eval switch", "[core][analyses][interval]")


Comment that this only considers singletons?

I guess - the reason for only considering singletons is each of the opertions is tested seperatly with both singleton and ranges, this test is really to check eval dispatches to the correct function

smowton · 2020-05-28T14:25:54Z

unit/util/interval/comparisons.cpp

+    // REQUIRE(two_to_four.equal(six_to_eight).is_unknown());
+    REQUIRE_FALSE(two_to_four.equal(five_to_ten).is_true());
+
+    REQUIRE_FALSE(two_to_four.not_equal(six_to_eight).is_unknown());


Why does the not-unknown one use six_to_eight but the others use five_to_ten?

Yeah this seems like a confusing mess - I've broken it into 3 sections - same interval, overlapping interval, disjoint interval and used consistent intervals for equal and not equal.

smowton · 2020-05-28T14:26:54Z

unit/util/interval/modulo.cpp

+    REQUIRE(V(a_mod_b.get_upper()) == 5);
+
+    const auto b_mod_a = b.modulo(a);
+    // TODO: precision with single element modulo


Perhaps add commented-out the results you would expect when fixed. Got a ticket for this?

No - it isn't wrong and we have no intention to fix it any time soon - a ticket will just sit not getting done. I would only raise it once someone actually wanted this to be more precise. Perhaps TODO is wrong, perhaps should just say note modulo is very imprecise.

smowton · 2020-05-28T14:40:37Z

unit/util/interval/eval.cpp

+      auto upper_value = numeric_cast<mp_integer>(
+        five_to_eight.eval(ID_unary_minus).get_upper());
+      REQUIRE(upper_value.has_value());
+      REQUIRE(upper_value.value() == -8);


Known bug that -((5, 8)) == (-8, -8)?

Typo that gets fixed in later commit

smowton · 2020-05-28T14:40:47Z

unit/util/interval/eval.cpp

+    THEN("When we apply unary subtraction to it, it should be negated")
+    {
+      auto negated_val = numeric_cast<mp_integer>(
+        five_to_eight.eval(ID_unary_minus).get_lower());


Compare equality against expected interval?

smowton · 2020-05-28T14:44:04Z

src/util/interval.cpp

-  lower.type() = type;
+  if(this->type().id() == ID_bool && is_int(type))
+  {
+    unsigned lower_num = !has_no_lower_bound() && get_lower().is_true();


has-no-lower-bound but get-lower returns something?

Well it has a not before the has_no_lower_bound -This function is one of the functions I don't really get, but would want to tidy up only after the code that is already using it is merged so I can change both at the same time if necessary

smowton · 2020-05-28T14:53:56Z

unit/util/interval/subtract.cpp

+  WHEN("Subtracting two constant intervals")
+  {
+    auto lhs =
+      constant_interval_exprt(constant_exprt("1010", unsignedbv_typet(32)));


Use from_integer and perhaps binary numeric literals if you want to emphasise the bitpattern you intend. I think these might be broken too because constant_exprt expects hex representation?

This thankfully ends up going away

smowton · 2020-05-28T14:55:45Z

src/util/interval.cpp


 constant_interval_exprt
-constant_interval_exprt::minus(const constant_interval_exprt &o) const
+constant_interval_exprt::minus(const constant_interval_exprt &other) const


Split commit "Remove swap function in intervals Also, refactor minus and correct a typo in the comments" to do one thing at a time

Go on then - since it's your last day 😛

(INT) Interval values

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

Currently checks are equivalent intervals, but before wasn't even checking that

ireps now use hex encoding, updated to modern version to get string of number

These aren't currently supported and cause a crash when executed

Currently this returns top rather than the actual range

Move some shift tests from the bitwise set of tests

Was wrongly using the unary negation operator, rather than subtracting one interval from the other.

thk123 force-pushed the fix-vsd-intervals branch 2 times, most recently from 963d5b5 to b9e275b Compare May 28, 2020 09:21

thk123 mentioned this pull request May 28, 2020

Assume relation between two symbols #5362

Merged

6 tasks

thk123 force-pushed the fix-vsd-intervals branch from b9e275b to cf6e08e Compare May 28, 2020 09:37

thk123 force-pushed the fix-vsd-intervals branch from cf6e08e to c128252 Compare May 28, 2020 11:04

thk123 marked this pull request as ready for review May 28, 2020 13:10

thk123 requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners May 28, 2020 13:10

thk123 force-pushed the fix-vsd-intervals branch from c128252 to 5f0aeab Compare May 28, 2020 13:14

smowton approved these changes May 28, 2020

View reviewed changes

Daniel Neville and others added 12 commits May 29, 2020 10:35

(INT) Interval operations

9689a66

(INT) Interval values

(INT) Fix broken interval unit tests

eefe162

(INT) Rename interval is_constant to is_single_value_interval

4e2d044

As it stands in conflicted with the method from exprt

(INT) Rename is_true and is_false in interval expressions

3473ad1

So they don't conflict with the exprt methods

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

ab44ab1

(INT) Make constructors take constant references instead of values

1ba8004

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

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

007c84d

…tions

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

b9e0d5a

Also replace some asserts with INVARIANT, PRECONDITION or UNREACHABLE

(INT) Cleanup to_string and operator<< for intervals

8c48d15

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

(INT) Give handle constants a better name

bb0c583

(INT) Remove swap function in intervals

f7bb442

Refactor minus and correct a typo in the comments

412bbad

Thomas Kiley added 24 commits May 29, 2020 10:37

Add tests for divide

1cd26b4

Add missing test coverage for unary operations

50fae45

Add missing coverage for multiply

b9d3dcf

Fix equality

bd34f7d

Currently checks are equivalent intervals, but before wasn't even checking that

Fix printing code

813c5b5

ireps now use hex encoding, updated to modern version to get string of number

Fix typo in unary plus tests for min and max

2c43d53

Disable unary minus tests on ranges

b62d567

These aren't currently supported and cause a crash when executed

Adapt test for bitwise not on a range

481f181

Currently this returns top rather than the actual range

Tidy up shift test

c1f60ad

Add remaining shift tests

763b906

Move some shift tests from the bitwise set of tests

Add missing tests for increment

a0cff82

Add missing bitwise tests for actual intervals

3722357

Add missing comparator tests

cc83805

Add tests for definitely_true/false for numeric intervals

d838704

Add missing tests for modulo

1faf516

Add tests for equality and inequality

7c16a14

Fix error in binary eval for subtraction

2d067f2

Was wrongly using the unary negation operator, rather than subtracting one interval from the other.

Add test case for eval on binary operations

39edeea

Add tests for the to_string operation

a84494c

fixup binary eval unit test commit

7f61939

Tidy the test for unary minus

42e2d5a

Make the equality comparison test easier to follow

536fc46

Add a comment explaining that modulo is imprecise

296fe68

Do a full check on the multiply test

1d92ca0

thk123 force-pushed the fix-vsd-intervals branch 2 times, most recently from 4e39366 to 1d92ca0 Compare May 29, 2020 10:58

danpoe approved these changes Jun 2, 2020

View reviewed changes

thk123 merged commit 7edbf52 into diffblue:develop Jun 4, 2020

thk123 deleted the fix-vsd-intervals branch June 4, 2020 09:28

thk123 mentioned this pull request Jun 4, 2020

Changes to intervals needed to merge VSD #5203

Closed

7 tasks

		@@ -0,0 +1,52 @@
		/*******************************************************************\
		Module: Unit tests for variable/sensitivity/abstract_object::merge

Conversation

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

Uh oh!

Uh oh!

codecov bot commented May 27, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

thk123 commented May 28, 2020

Uh oh!

thk123 commented May 28, 2020

Uh oh!

thk123 commented May 28, 2020

Uh oh!

thk123 commented May 28, 2020

Uh oh!

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

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

thk123 commented May 27, 2020 •

edited

Loading

codecov bot commented May 27, 2020 •

edited

Loading