Support ==,!=,<,<=,>,>= over vectors #5940

tautschnig · 2021-03-15T22:09:02Z

These need to be rewritten to point-wise applications and return -1
(true) or 0 (false) per element.

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

kroening · 2021-03-16T07:04:57Z

What happens when the vector subtype is unsigned?

tautschnig · 2021-03-16T09:48:17Z

What happens when the vector subtype is unsigned?

GCC's documentation says "constant of the appropriate type where all bits are set" (https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html), so this should work (as we use two's complement).

src/util/std_expr.h

kroening · 2021-03-16T12:37:04Z

What happens when the vector subtype is unsigned?

GCC's documentation says "constant of the appropriate type where all bits are set" (https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html), so this should work (as we use two's complement).

Does that operation exist for vectors of type float?

tautschnig · 2021-03-16T13:30:12Z

What happens when the vector subtype is unsigned?

GCC's documentation says "constant of the appropriate type where all bits are set" (https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html), so this should work (as we use two's complement).

Does that operation exist for vectors of type float?

The docs say: "Comparison operands can be vector expressions of integer-type or real-type."

kroening · 2021-03-16T14:03:10Z

Does that operation exist for vectors of type float?

The docs say: "Comparison operands can be vector expressions of integer-type or real-type."

Won't the from_integer(-1, subtype) then fail?

kroening · 2021-03-16T14:08:14Z

The docs say: "Comparison operands can be vector expressions of integer-type or real-type."

Won't the from_integer(-1, subtype) then fail?

from_integer(-1, subtype) actually works for float. However, you then do get the floating-point representation of -1, which is not the same as "constant of the appropriate type where all bits are set" -- that would be NaN.

kroening · 2021-03-16T14:10:55Z

from_integer(-1, subtype) actually works for float. However, you then do get the floating-point representation of -1, which is not the same as "constant of the appropriate type where all bits are set" -- that would be NaN.

A quick test confirms that clang generates NaN, not -1.

tautschnig · 2021-03-16T14:31:09Z

from_integer(-1, subtype) actually works for float. However, you then do get the floating-point representation of -1, which is not the same as "constant of the appropriate type where all bits are set" -- that would be NaN.

A quick test confirms that clang generates NaN, not -1.

Ah, just noting that subtype (which is the type of the result, not that of the operands) wouldn't be float here, it would still be signed_int. Though that's only what the C front-end generates, I acknowledge that I omitted any checking in here.

kroening · 2021-03-16T15:04:53Z

Ah, I overlooked "The result of the comparison is a vector of the same width and number of elements as the comparison operands with a signed integral element type".

Right now, the result type is an array type, but should be a vector type.

kroening · 2021-03-16T15:07:40Z

Ah, sorry, wrong again -- the frontend does produce a vector type, of signed integers, but it does fail to meet the requirement "same width".

Newly created expressions did not have a source location, which may, however, be useful in debugging.

As specified in GCC's documentation, the result type is a vector of signed integers of the same width as the operand subtypes. As the semantics are different from relational expressions over scalars, introduce a different expression id: each operation is now prefixed with vector-.

These need to be rewritten to point-wise applications and return -1 (true) or 0 (false) per element. Fixes: diffblue#5930

codecov · 2021-03-16T19:48:12Z

Codecov Report

Merging #5940 (316ae8b) into develop (111b51e) will increase coverage by 0.01%.
The diff coverage is 91.93%.

@@             Coverage Diff             @@
##           develop    #5940      +/-   ##
===========================================
+ Coverage    73.55%   73.56%   +0.01%     
===========================================
  Files         1431     1431              
  Lines       155248   155291      +43     
===========================================
+ Hits        114189   114243      +54     
+ Misses       41059    41048      -11

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_base.h	`100.00% <ø> (ø)`
src/goto-programs/remove_vector.cpp	`96.85% <90.47%> (-2.29%)`	⬇️
src/ansi-c/c_typecheck_expr.cpp	`75.04% <92.85%> (+0.09%)`	⬆️
src/ansi-c/parser.y	`77.77% <100.00%> (-0.07%)`	⬇️
src/ansi-c/scanner.l	`61.63% <100.00%> (+0.03%)`	⬆️
...olvers/strings/string_constraint_instantiation.cpp	`91.15% <0.00%> (-3.54%)`	⬇️
src/goto-programs/builtin_functions.cpp	`54.72% <0.00%> (+0.14%)`	⬆️
src/solvers/smt2/smt2_conv.cpp	`59.02% <0.00%> (+0.15%)`	⬆️
src/solvers/floatbv/float_bv.cpp	`73.85% <0.00%> (+0.73%)`	⬆️
... and 2 more

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 b7859de...316ae8b. Read the comment docs.

kroening · 2021-03-16T20:12:55Z

src/ansi-c/c_typecheck_expr.cpp

+  if(expr.id() == ID_notequal)
+    expr.id(ID_vector_notequal);
+  else
+    expr.id("vector-" + id2string(expr.id()));
 }


This will be vector-=, vector-<= etc?

tautschnig added the bugfix label Mar 15, 2021

tautschnig requested review from kroening, peterschrammel and smowton as code owners March 15, 2021 22:09

tautschnig mentioned this pull request Mar 15, 2021

Feature request: Support for SIMD comparison operators #5930

Closed

tautschnig force-pushed the fix-5930 branch 3 times, most recently from 4c24ace to b691fad Compare March 16, 2021 10:12

tautschnig self-assigned this Mar 16, 2021

tautschnig commented Mar 16, 2021

View reviewed changes

src/util/std_expr.h Outdated Show resolved Hide resolved

remove_vector: maintain source location

5acadac

Newly created expressions did not have a source location, which may, however, be useful in debugging.

tautschnig force-pushed the fix-5930 branch from b691fad to eace402 Compare March 16, 2021 18:12

tautschnig requested a review from chrisr-diffblue as a code owner March 16, 2021 18:12

tautschnig force-pushed the fix-5930 branch from eace402 to cacbad9 Compare March 16, 2021 18:16

tautschnig force-pushed the fix-5930 branch from cacbad9 to 9f9f465 Compare March 16, 2021 18:17

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

tautschnig force-pushed the fix-5930 branch from 9f9f465 to 316ae8b Compare March 16, 2021 18:25

tautschnig assigned kroening and unassigned tautschnig Mar 16, 2021

kroening reviewed Mar 16, 2021

View reviewed changes

kroening approved these changes Mar 16, 2021

View reviewed changes

kroening merged commit 5e145e4 into diffblue:develop Mar 16, 2021

tautschnig deleted the fix-5930 branch March 16, 2021 21:02

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Support ==,!=,<,<=,>,>= over vectors #5940

Support ==,!=,<,<=,>,>= over vectors #5940

Uh oh!

tautschnig commented Mar 15, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

tautschnig commented Mar 16, 2021

Uh oh!

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

tautschnig commented Mar 16, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

tautschnig commented Mar 16, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

codecov bot commented Mar 16, 2021

Uh oh!

kroening Mar 16, 2021

Uh oh!

Uh oh!

Support ==,!=,<,<=,>,>= over vectors #5940

Support ==,!=,<,<=,>,>= over vectors #5940

Uh oh!

Conversation

tautschnig commented Mar 15, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

tautschnig commented Mar 16, 2021

Uh oh!

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

tautschnig commented Mar 16, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

tautschnig commented Mar 16, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

kroening commented Mar 16, 2021

Uh oh!

codecov bot commented Mar 16, 2021

Codecov Report

Uh oh!

kroening Mar 16, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!