Refactor element access of pointer arrays into a separate function #4525

antlechner · 2019-04-12T16:29:44Z

~~This PR is based on #4524. Please only review the last commit.~~

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.
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.

allredj

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

smowton

This is not JBMC-specific -- suggest move to util/

smowton · 2019-04-13T12:26:48Z

jbmc/src/java_bytecode/java_utils.cpp

@@ -191,6 +191,12 @@ dereference_exprt checked_dereference(const exprt &expr)
  return result;
 }

+dereference_exprt
+element_at_pointer_array_index(const exprt &pointer, const exprt &index)


Suggested name array_element_from_pointer

Changed the name to your suggestion.

owen-mc-diffblue · 2019-04-15T09:14:09Z

jbmc/src/java_bytecode/java_utils.cpp

+dereference_exprt
+element_at_pointer_array_index(const exprt &pointer, const exprt &index)
+{
+  return dereference_exprt{plus_exprt{pointer, index}};


💡 Would it be a good idea to have something like INVARIANT(can_cast_type<pointer_typet>(pointer.type())); at the beginning of this function?

Done (using PRECONDITION).

antlechner · 2019-04-15T10:31:02Z

This is rebased on develop now.
@smowton I moved it to a new file util/array_element_from_pointer.h and changed the documentation slightly. I don't actually know how we represent arrays for C / when we represent them as pointers to the first element, so let me know if anything should be added to the documentation as it is now.

tautschnig

I think this is fine for C as well. I'm wondering, however, whether util/pointer_offset_sum.h would also be an ok header to place this? No particularly strong feelings about it, though.

tautschnig · 2019-04-15T10:54:51Z

src/util/array_element_from_pointer.h

+array_element_from_pointer(const exprt &pointer, const exprt &index)
+{
+  PRECONDITION(can_cast_type<pointer_typet>(pointer.type()));
+  return dereference_exprt{plus_exprt{pointer, index}};


While at it, maybe also do PRECONDITION(index.type().id() == ID_signedbv || index.type().id() == ID_unsignedbv);? I think those are the only two reasonable options, although maybe we could also work with some other bitvector types.

I added the precondition. If we need other types in the future we can always add them later.

smowton · 2019-04-15T10:57:24Z

src/util/array_element_from_pointer.h

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: Util


This is usually a description of the file, not the directory

I had seen Module: Util in another file and just copied that. Most files in util seem to just leave this empty... Anyway, I changed this one to "Element access in a pointer array".

smowton · 2019-04-15T11:01:54Z

src/util/array_element_from_pointer.h

+/// given index of a pointer array:
+/// `*(pointer + index)`
+/// Arrays are sometimes (always in JBMC) represented as a pointer to their
+/// first element. This is because we cannot know the type of an array of


Suggest replace the second sentence with just , especially when their length is uncertain

I replaced a part of the second sentence with that. 🙂

allredj

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

This does not save many lines of code, but the way we access arrays using pointer arithmetic can be a bit confusing and it makes sense to abstract it away and keep the documentation of why we do things this way in one place.

antlechner · 2019-04-16T17:44:45Z

@tautschnig pointer_offset_sum.h contains only one function with the same name as the file, so I'll keep this one separate for now to avoid confusion.

allredj

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

antlechner added the do not merge label Apr 12, 2019

antlechner requested review from smowton, majakusber and thomasspriggs April 12, 2019 16:29

antlechner requested review from allredj, cesaro, chrisr-diffblue, cristina-david, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, NathanJPhillips, owen-mc-diffblue, peterschrammel, pkesseli, romainbrenguier, tautschnig and thk123 as code owners April 12, 2019 16:29

antlechner force-pushed the antonia/array-index-arithmetic branch from 3f3a702 to 4b7cf97 Compare April 12, 2019 17:17

allredj reviewed Apr 12, 2019

View reviewed changes

tautschnig changed the title ~~Refactor element access of pointer arrays into a separate function (review last commit only)~~ Refactor element access of pointer arrays into a separate function (review last commit only) [depends-on: #4524] Apr 13, 2019

tautschnig added dependent - do not merge and removed do not merge labels Apr 13, 2019

smowton reviewed Apr 13, 2019

View reviewed changes

owen-mc-diffblue approved these changes Apr 15, 2019

View reviewed changes

antlechner force-pushed the antonia/array-index-arithmetic branch from 4b7cf97 to 779f5df Compare April 15, 2019 10:28

antlechner removed the dependent - do not merge label Apr 15, 2019

tautschnig approved these changes Apr 15, 2019

View reviewed changes

smowton approved these changes Apr 15, 2019

View reviewed changes

allredj reviewed Apr 15, 2019

View reviewed changes

peterschrammel changed the title ~~Refactor element access of pointer arrays into a separate function (review last commit only) [depends-on: #4524]~~ Refactor element access of pointer arrays into a separate function Apr 15, 2019

peterschrammel assigned antlechner Apr 15, 2019

Refactor array access into a separate function

2088544

This does not save many lines of code, but the way we access arrays using pointer arithmetic can be a bit confusing and it makes sense to abstract it away and keep the documentation of why we do things this way in one place.

antlechner force-pushed the antonia/array-index-arithmetic branch from 779f5df to 2088544 Compare April 16, 2019 17:41

allredj reviewed Apr 16, 2019

View reviewed changes

tautschnig merged commit abbafd2 into diffblue:develop Apr 17, 2019

antlechner deleted the antonia/array-index-arithmetic branch April 17, 2019 09:08

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor element access of pointer arrays into a separate function #4525

Refactor element access of pointer arrays into a separate function #4525

antlechner commented Apr 12, 2019 •

edited by peterschrammel

Loading

allredj left a comment

smowton left a comment

smowton Apr 13, 2019

antlechner Apr 15, 2019

owen-mc-diffblue Apr 15, 2019

antlechner Apr 15, 2019

antlechner commented Apr 15, 2019

tautschnig left a comment

tautschnig Apr 15, 2019

antlechner Apr 16, 2019

smowton Apr 15, 2019

antlechner Apr 16, 2019

smowton Apr 15, 2019

antlechner Apr 16, 2019

allredj left a comment

antlechner commented Apr 16, 2019

allredj left a comment

		@@ -0,0 +1,32 @@
		/*******************************************************************\

		Module: Util

Refactor element access of pointer arrays into a separate function #4525

Refactor element access of pointer arrays into a separate function #4525

Conversation

antlechner commented Apr 12, 2019 • edited by peterschrammel Loading

allredj left a comment

Choose a reason for hiding this comment

smowton left a 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

antlechner commented Apr 15, 2019

tautschnig left a 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

allredj left a comment

Choose a reason for hiding this comment

antlechner commented Apr 16, 2019

allredj left a comment

Choose a reason for hiding this comment

antlechner commented Apr 12, 2019 •

edited by peterschrammel

Loading