Refactor code related to bitvector type min/max values #4352

antlechner · 2019-03-08T13:11:58Z

This PR includes no functional changes, only refactoring.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
n/a 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).
n/a My commit message includes data points confirming performance improvements (if claimed).
n/a My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

We should only store these arithmetic calculations in one place in the codebase.

martin-cs

Seems reasonable and code reduction patches are always a good thing!

tautschnig · 2019-03-08T14:51:00Z

src/util/std_types.h

+  mp_integer largest() const;
+  constant_exprt smallest_expr() const;
+  constant_exprt zero_expr() const;
+  constant_exprt largest_expr() const;


This is brilliant refactoring, thank you! Yet can you please hide these in pointer_typet? A pointer_typet happens to be a bitvector_typet, but really they must not be used (not even zero_expr) on a pointer_typet.

Ah, I overlooked that there are actually quite a few classes that inherit from bitvector_typet. Besides the three that were already mentioned, there are bv_typet, fixedbv_typet, floatbv_typet, c_bit_field_typet and c_bool_typet. However these functions will hit an UNREACHABLE if the type id is anything other than ID_unsignedbv or ID_signedbv. Would it make sense to introduce a new class that inherits from bitvector_typet and that both signedbv_typet and unsignedbv_typet inherit from? Any suggestions for what such a class should be called?

smallest()/largest() only make sense for the integer ones -- so that could be integer_bitvector_typet. smallest_expr, zero_expr, largest_expr() also work on fixedbv and floatbv; these could be a numeric_bitvector_typet.

That makes sense, thank you! I only created the integer_bitvector_typet class as all five methods were previously only defined for the signedbv/unsignedbv types, and I added some documentation and a comment mentioning that the methods returning an exprt would make sense for fixedbv/floatbv as well in case we need them there in the future.

tautschnig · 2019-03-08T14:52:17Z

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -458,7 +446,7 @@ void initialize_nondet_string_fields(
  code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length)));

  // assume (length_expr <= max_input_length)
-  if(max_nondet_string_length <= max_value(length_expr.type()))
+  if(max_nondet_string_length <= bv_spect(length_expr.type()).max_value())


How about to_bitvector_type(length_expr.type()).largest()?

Good point, why does the class bv_spect even (publicly) exist if this functionality is already made available by the typet?
I changed it to your suggestion for now. Depending on what you think about my previous question I might change to_bitvector_type to something more specific.
I also found another place where bv_spect was used to get the max value, and replaced this with bitvector_type::largest as well.

Following @kroening 's comment above, this is now to_integer_bitvector_type(...) (and similarly for your other comment).

tautschnig · 2019-03-08T14:53:09Z

src/ansi-c/ansi_c_entry_point.cpp

-        }
-        else
-          UNREACHABLE;
+        const mp_integer max = bv_spect(envp_size_symbol.type).max_value();


As above to_bitvector_type(envp_size_symbol.type).largest()?

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 23c17f1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103691044

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: c8f8458).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103716955

Since unsignedbv_typet and signedbv_typet now have some common functionality, it makes sense to give them a common parent to store these methods in.

These methods are now all identical and can be inherited from integer_bitvector_typet.

The method can be used in several places that previously duplicated its logic.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: f313fdf).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103736558

De-duplicate logic for bitvector max/min values

13a058c

We should only store these arithmetic calculations in one place in the codebase.

antlechner requested review from danpoe and romainbrenguier March 8, 2019 13:11

antlechner requested review from cesaro, cristina-david, kroening, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners March 8, 2019 13:11

antlechner force-pushed the antonia/bv-min-max-refactor branch from 68ef509 to 23c17f1 Compare March 8, 2019 13:14

martin-cs approved these changes Mar 8, 2019

View reviewed changes

tautschnig approved these changes Mar 8, 2019

View reviewed changes

tautschnig assigned antlechner, smowton, thk123 and peterschrammel Mar 8, 2019

tautschnig added the cleanup label Mar 8, 2019

smowton approved these changes Mar 8, 2019

View reviewed changes

allredj reviewed Mar 8, 2019

View reviewed changes

antlechner force-pushed the antonia/bv-min-max-refactor branch from 23c17f1 to c8f8458 Compare March 8, 2019 16:56

antlechner assigned tautschnig Mar 8, 2019

allredj reviewed Mar 8, 2019

View reviewed changes

antlechner added 4 commits March 8, 2019 18:47

Create common parent of (un)signedbv_typet classes

df6cb81

Since unsignedbv_typet and signedbv_typet now have some common functionality, it makes sense to give them a common parent to store these methods in.

Move methods from (un)signedbv typet to parent class

01376d5

These methods are now all identical and can be inherited from integer_bitvector_typet.

Make use of bitvector_typet::largest

cbb1dee

The method can be used in several places that previously duplicated its logic.

Add documentation to smallest/largest/zero methods

f313fdf

antlechner force-pushed the antonia/bv-min-max-refactor branch from c8f8458 to f313fdf Compare March 8, 2019 19:14

allredj reviewed Mar 8, 2019

View reviewed changes

tautschnig merged commit 5973f10 into diffblue:develop Mar 11, 2019

antlechner deleted the antonia/bv-min-max-refactor branch March 11, 2019 10:19

tautschnig mentioned this pull request Apr 16, 2021

Use bv_spect/bv_arithmetict #1933

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Refactor code related to bitvector type min/max values #4352

Refactor code related to bitvector type min/max values #4352

Uh oh!

antlechner commented Mar 8, 2019

Uh oh!

martin-cs left a comment

Uh oh!

tautschnig Mar 8, 2019

Uh oh!

antlechner Mar 8, 2019

Uh oh!

kroening Mar 8, 2019

Uh oh!

antlechner Mar 8, 2019

Uh oh!

tautschnig Mar 8, 2019

Uh oh!

antlechner Mar 8, 2019

Uh oh!

antlechner Mar 8, 2019

Uh oh!

tautschnig Mar 8, 2019

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

allredj left a comment

Uh oh!

Uh oh!

Refactor code related to bitvector type min/max values #4352

Refactor code related to bitvector type min/max values #4352

Uh oh!

Conversation

antlechner commented Mar 8, 2019

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!