Skip to content

Feature request: Support for SIMD comparison operators #5930

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
adpaco-aws opened this issue Mar 15, 2021 · 1 comment · Fixed by #5940
Closed

Feature request: Support for SIMD comparison operators #5930

adpaco-aws opened this issue Mar 15, 2021 · 1 comment · Fixed by #5940
Labels
pending merge

Comments

@adpaco-aws
Copy link
Contributor

adpaco-aws commented Mar 15, 2021 •
edited
Loading

Support for SIMD arithmetic operators (e.g., addition or logical operators) exists in CBMC but this is not the case for comparison operators ==, !=, <, >, <= and >=. According to GCC online docs vectors are compared element by element producing a 0 when the comparison is false and -1 otherwise.

I am not able to provide an example since #5903 does not allow to compile, but this is the warning I am getting from CBMC when I run it on code that we generate:

warning: ignoring =
  * type: array
      * #source_location: nil
      * size: constant
          * type: signedbv
              * width: 64
              * #c_type: signed_long_int
          * value: 2
      0: signedbv
          * width: 64
          * #c_type: signed_long_int
  0: array
      * type: array
          * #source_location: nil
          * size: constant
              * type: signedbv
                  * width: 64
                  * #c_type: signed_long_int
              * value: 2
          0: signedbv
              * width: 64
              * #c_type: signed_long_int
      0: constant
          * type: signedbv
              * width: 64
              * #c_type: signed_long_int
          * value: 0
      1: constant
          * type: signedbv
              * width: 64
              * #c_type: signed_long_int
          * value: 0
  1: array
      * type: array
          * #source_location: nil
          * size: constant
              * type: signedbv
                  * width: 64
                  * #c_type: signed_long_int
              * value: 2
          0: signedbv
              * width: 64
              * #c_type: signed_long_int
      0: constant
          * type: signedbv
              * width: 64
              * #c_type: signed_long_int
          * value: 0
      1: constant
          * type: signedbv
              * width: 64
              * #c_type: signed_long_int
          * value: 0
@adpaco-aws adpaco-aws changed the title Support for SIMD comparison operators Feature request: Support for SIMD comparison operators Mar 15, 2021
tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 15, 2021
@tautschnig
Support ==,!=,<,<=,>,>= over vectors
79d0ed7 
These need to be rewritten to point-wise applications and return -1
(true) or 0 (false) per element.

Fixes: diffblue#5930
@tautschnig tautschnig mentioned this issue Mar 15, 2021
Merged
3 tasks
@tautschnig
Copy link
Collaborator

Thank you for raising this, will be fixed once #5940 is merged.

tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 16, 2021
@tautschnig
Support ==,!=,<,<=,>,>= over vectors
733b82a 
These need to be rewritten to point-wise applications and return -1
(true) or 0 (false) per element.

Fixes: diffblue#5930
tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 16, 2021
@tautschnig
Support ==,!=,<,<=,>,>= over vectors
4c24ace 
These need to be rewritten to point-wise applications and return -1
(true) or 0 (false) per element.

Fixes: diffblue#5930
tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 16, 2021
@tautschnig
Support ==,!=,<,<=,>,>= over vectors
b691fad 
These need to be rewritten to point-wise applications and return -1
(true) or 0 (false) per element.

Fixes: diffblue#5930
tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 16, 2021
@tautschnig
Support ==,!=,<,<=,>,>= over vectors
eace402 
These need to be rewritten to point-wise applications and return -1
(true) or 0 (false) per element.

Fixes: diffblue#5930
tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 16, 2021
@tautschnig
Support ==,!=,<,<=,>,>= over vectors
cacbad9 
These need to be rewritten to point-wise applications and return -1
(true) or 0 (false) per element.

Fixes: diffblue#5930
tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 16, 2021
@tautschnig
Support ==,!=,<,<=,>,>= over vectors
9f9f465 
These need to be rewritten to point-wise applications and return -1
(true) or 0 (false) per element.

Fixes: diffblue#5930
tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 16, 2021
@tautschnig
Support ==,!=,<,<=,>,>= over vectors
316ae8b 
These need to be rewritten to point-wise applications and return -1
(true) or 0 (false) per element.

Fixes: diffblue#5930
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pending merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Support ==,!=,<,<=,>,>= over vectors tautschnig/cbmc
2 participants
@tautschnig @adpaco-aws