introduce index_type and element_type for arrays and vectors #6552

kroening · 2021-12-27T22:26:02Z

This commit introduces convenience methods for retrieving the type of the
elements and of the indices for array and vector types. This avoids using a
global, architecture-dependent function to generate the index type.

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

codecov · 2021-12-28T11:56:08Z

Codecov Report

Merging #6552 (5ba2935) into develop (e4c5999) will decrease coverage by 0.00%.
The diff coverage is 56.75%.

@@             Coverage Diff             @@
##           develop    #6552      +/-   ##
===========================================
- Coverage    75.98%   75.98%   -0.01%     
===========================================
  Files         1578     1578              
  Lines       181058   181070      +12     
===========================================
+ Hits        137579   137585       +6     
- Misses       43479    43485       +6

Impacted Files	Coverage Δ
src/goto-cc/gcc_cmdline.cpp	`74.80% <ø> (ø)`
src/goto-instrument/goto_program2code.cpp	`68.32% <0.00%> (ø)`
src/util/std_expr.h	`92.04% <ø> (ø)`
src/solvers/flattening/boolbv_get.cpp	`82.03% <23.07%> (-0.72%)`	⬇️
src/util/std_types.cpp	`85.71% <50.00%> (-1.65%)`	⬇️
src/util/std_types.h	`95.01% <50.00%> (-0.57%)`	⬇️
src/goto-symex/field_sensitivity.cpp	`90.96% <100.00%> (ø)`
src/goto-symex/symex_builtin_functions.cpp	`93.35% <100.00%> (ø)`
src/util/pointer_offset_size.cpp	`92.18% <100.00%> (+0.02%)`	⬆️

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 9b72a5c...5ba2935. Read the comment docs.

tautschnig

Shouldn't we rather strive towards a situation where an array index can be of an arbitrary numeric type?

src/goto-instrument/goto_program2code.cpp

src/solvers/flattening/boolbv_get.cpp

tautschnig · 2021-12-29T05:09:02Z

src/util/std_types.h

+  /// The type of the elements of the array.
+  const typet &element_type() const
+  {
+    return subtype();


Should we actually hide subtype() for array_typet and vector_typet?

Yes, that will improve readability.

tautschnig · 2021-12-29T05:11:40Z

src/util/std_types.h

@@ -768,6 +768,15 @@ class array_typet:public type_with_subtypet
    add(ID_size, std::move(_size));
  }

+  /// The type of the index expressions into any instance of this type.
+  typet index_type() const;


I am concerned that this may be confusing: we could end up in a situation where array.index().type() != array.index_type()!

I'd like to enforce that, going forward, using a precondition.

kroening · 2021-12-29T10:33:03Z

Shouldn't we rather strive towards a situation where an array index can be of an arbitrary numeric type?

I did consider it, but I don't think it's a good idea.

It would be problematic to use the SMT-LIB array theory, which is basically a map type.
Expressions that one would expect to be identical are not. Say a[1] and a[1l] would be different.

tautschnig · 2021-12-31T06:13:08Z

Shouldn't we rather strive towards a situation where an array index can be of an arbitrary numeric type?

I did consider it, but I don't think it's a good idea.
1. It would be problematic to use the SMT-LIB array theory, which is basically a map type.

2. Expressions that one would expect to be identical are not. Say a[1] and a[1l] would be different.

Will it always be possible to have the same index type, even when linking together objects from different source languages, for example C and Java?

kroening · 2021-12-31T11:03:32Z

Will it always be possible to have the same index type, even when linking together objects from different source languages, for example C and Java?

The plan is to make the index type part of the array type; you can then mix as you see fit.

src/goto-symex/field_sensitivity.cpp

src/goto-symex/symex_builtin_functions.cpp

tautschnig

My concerns/comments that I've left unresolved remain in place, but approving nonetheless.

kroening · 2021-12-31T20:51:36Z

My concerns/comments that I've left unresolved remain in place, but approving nonetheless.

Both of these won't be easy -- look at the branch typet_subtype

This commit introduces convenience methods for retrieving the type of the elements and of the indices for array and vector types. This avoids using a global, architecture-dependent function to generate the index type.

kroening force-pushed the index_type branch from b455f3e to 31946bc Compare December 27, 2021 22:31

kroening marked this pull request as ready for review December 27, 2021 22:43

kroening requested review from chrisr-diffblue, martin-cs, peterschrammel, romainbrenguier and tautschnig as code owners December 27, 2021 22:43

kroening force-pushed the index_type branch from 31946bc to b219969 Compare December 28, 2021 10:35

tautschnig reviewed Dec 29, 2021

View reviewed changes

kroening force-pushed the index_type branch 2 times, most recently from bd9f103 to de7ed5b Compare December 29, 2021 17:18

tautschnig reviewed Dec 31, 2021

View reviewed changes

src/goto-symex/field_sensitivity.cpp Show resolved Hide resolved

src/goto-symex/symex_builtin_functions.cpp Show resolved Hide resolved

kroening force-pushed the index_type branch from de7ed5b to acb0a35 Compare December 31, 2021 16:47

tautschnig approved these changes Dec 31, 2021

View reviewed changes

tautschnig assigned kroening, peterschrammel and martin-cs Dec 31, 2021

introduce index_type and element_type for arrays and vectors

5ba2935

This commit introduces convenience methods for retrieving the type of the elements and of the indices for array and vector types. This avoids using a global, architecture-dependent function to generate the index type.

kroening force-pushed the index_type branch from acb0a35 to 5ba2935 Compare December 31, 2021 20:53

peterschrammel approved these changes Jan 12, 2022

View reviewed changes

kroening merged commit 90bcd52 into develop Jan 12, 2022

kroening deleted the index_type branch January 12, 2022 15:42

TGWDB mentioned this pull request May 31, 2023

[RFC] Version 6 #7743

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

introduce index_type and element_type for arrays and vectors #6552

introduce index_type and element_type for arrays and vectors #6552

kroening commented Dec 27, 2021

codecov bot commented Dec 28, 2021 •

edited

Loading

tautschnig left a comment

tautschnig Dec 29, 2021

kroening Dec 29, 2021

tautschnig Dec 29, 2021

kroening Dec 29, 2021

kroening commented Dec 29, 2021

tautschnig commented Dec 31, 2021

kroening commented Dec 31, 2021

tautschnig left a comment

kroening commented Dec 31, 2021

introduce index_type and element_type for arrays and vectors #6552

introduce index_type and element_type for arrays and vectors #6552

Conversation

kroening commented Dec 27, 2021

codecov bot commented Dec 28, 2021 • edited Loading

Codecov Report

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Dec 29, 2021

Choose a reason for hiding this comment

kroening Dec 29, 2021

Choose a reason for hiding this comment

tautschnig Dec 29, 2021

Choose a reason for hiding this comment

kroening Dec 29, 2021

Choose a reason for hiding this comment

kroening commented Dec 29, 2021

tautschnig commented Dec 31, 2021

kroening commented Dec 31, 2021

tautschnig left a comment

Choose a reason for hiding this comment

kroening commented Dec 31, 2021

codecov bot commented Dec 28, 2021 •

edited

Loading