Skip to content

remove_vector: lower vector-to-scalar casts to byte extracts - #9235

Open
traffaillac wants to merge 3 commits into
diffblue:developfrom
traffaillac:fix-vector-to-scalar-cast
Open

traffaillac wants to merge 3 commits into
diffblue:developfrom
traffaillac:fix-vector-to-scalar-cast

Conversation

@traffaillac

Copy link
Copy Markdown

Hi,

Thanks for this amazing project! I am beginning to use it to validate a video codec making heavy use of GCC vector extensions (https://github.com/tvlabs/edge264).

The code to reproduce this bug and the fix were generated by Claude Opus 5.5 (as with my other PR), as I am not familiar with this codebase. I insctructed it to follow the points below, and to be concise with comments (yeah it does not seem so...). Please tell me if they need manual refining in any direction.

Cheers,
Thibault Raffaillac

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

As in GCC and Clang, the C front-end accepts casts from a vector to a
scalar of the same size, e.g., (uint64_t)v with v a vector of 8 bytes,
which reinterpret the bits of the vector. remove_vector turned the
operand into an array but kept the typecast, and the back-ends cannot
convert an array to a bit-vector with a typecast. They printed "warning:
ignoring typecast" and left the result unconstrained, so assertions
about it failed spuriously.

Lower such casts to a byte extract at offset 0, which reinterprets the
array with the configured endianness.

The new regression test gcc_vector_to_scalar_cast compares the result of
such a cast with a memcpy of the same vector. Without this change it
reports "warning: ignoring typecast" and the assertion fails.
The test uses __attribute__((vector_size(...))), which other compilers
such as Visual Studio do not support. Guard it with #ifdef __GNUC__, as
the existing gcc_vector1 and gcc_vector3 tests do, so that the test
trivially succeeds on such platforms instead of failing to parse. The
gcc-only tag is no longer needed.
Besides unsigned elements, vectors can have signed, floating-point and
fixed-point elements (_Bool and enum elements are rejected by
typecheck_vector_type). Check that casts of such vectors to a scalar of
the same size also reinterpret their bits. Without the fix in
remove_vector, all four assertions fail with "warning: ignoring
typecast".

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant