From 588d489a35e22976605b6d0350cc6855ea46c47c Mon Sep 17 00:00:00 2001
From: Ben Pfaff <bpfaff@vmware.com>
Date: Mon, 18 Jul 2022 18:03:18 -0700
Subject: [PATCH] Document and add a test for bit-shift operator behavior.

This documents the current requirement that the right-hand operand of
<< and >> have type bit<32>.  I tend to consider that a bug (see
https://github.com/vmware/differential-datalog/issues/1158), so I
hope that it will be relaxed in the future (and the documentation
updated).

Signed-off-by: Ben Pfaff <bpfaff@vmware.com>
---
 doc/language_reference/language_reference.md |  7 +++++
 test/datalog_tests/bit_shift.dl              |  7 +++++
 test/datalog_tests/bit_shift.dump.expected   | 33 ++++++++++++++++++++
 3 files changed, 47 insertions(+)
 create mode 100644 test/datalog_tests/bit_shift.dl
 create mode 100644 test/datalog_tests/bit_shift.dump.expected

diff --git a/doc/language_reference/language_reference.md b/doc/language_reference/language_reference.md
index d929c1071..b72c5e2f3 100644
--- a/doc/language_reference/language_reference.md
+++ b/doc/language_reference/language_reference.md
@@ -315,6 +315,13 @@ expr ::= term
        | expr "?"                                       (*try*)
 ```
 
+In shift expressions `lhs "<<" rhs` and `lhs ">>" rhs`, `lhs` may have
+any integer type.  The value of `rhs`, which must have type `bit<32>`,
+is taken modulo the bit-width of `lhs` rounded up to a power of 2, so
+that, for example, shifting a value of type `bit<10>` left or right by
+10 to 15 bits, inclusive, always yields a value of 0, and shifting by
+16 bits has no effect.
+
 The following table lists operators order by decreasing priority.
 
 |**priority** | **operators**                     |
diff --git a/test/datalog_tests/bit_shift.dl b/test/datalog_tests/bit_shift.dl
new file mode 100644
index 000000000..0638da025
--- /dev/null
+++ b/test/datalog_tests/bit_shift.dl
@@ -0,0 +1,7 @@
+relation X(x: bit<10>, y: bit<10>)
+output relation Y(x: bit<10>, y: bit<10>, z: bit<10>)
+Y(x, y, x << (y as u32)) :- X(x, y).
+
+X(x, y) :-
+    var x = FlatMap([0, 1, 2, 3]),
+    var y = FlatMap([0, 1, 9, 10, 11, 15, 16, 17]).
diff --git a/test/datalog_tests/bit_shift.dump.expected b/test/datalog_tests/bit_shift.dump.expected
new file mode 100644
index 000000000..5903b06fa
--- /dev/null
+++ b/test/datalog_tests/bit_shift.dump.expected
@@ -0,0 +1,33 @@
+Y:
+Y{.x = 0, .y = 0, .z = 0}: +1
+Y{.x = 0, .y = 1, .z = 0}: +1
+Y{.x = 0, .y = 9, .z = 0}: +1
+Y{.x = 0, .y = 10, .z = 0}: +1
+Y{.x = 0, .y = 11, .z = 0}: +1
+Y{.x = 0, .y = 15, .z = 0}: +1
+Y{.x = 0, .y = 16, .z = 0}: +1
+Y{.x = 0, .y = 17, .z = 0}: +1
+Y{.x = 1, .y = 0, .z = 1}: +1
+Y{.x = 1, .y = 1, .z = 2}: +1
+Y{.x = 1, .y = 9, .z = 512}: +1
+Y{.x = 1, .y = 10, .z = 0}: +1
+Y{.x = 1, .y = 11, .z = 0}: +1
+Y{.x = 1, .y = 15, .z = 0}: +1
+Y{.x = 1, .y = 16, .z = 1}: +1
+Y{.x = 1, .y = 17, .z = 2}: +1
+Y{.x = 2, .y = 0, .z = 2}: +1
+Y{.x = 2, .y = 1, .z = 4}: +1
+Y{.x = 2, .y = 9, .z = 0}: +1
+Y{.x = 2, .y = 10, .z = 0}: +1
+Y{.x = 2, .y = 11, .z = 0}: +1
+Y{.x = 2, .y = 15, .z = 0}: +1
+Y{.x = 2, .y = 16, .z = 2}: +1
+Y{.x = 2, .y = 17, .z = 4}: +1
+Y{.x = 3, .y = 0, .z = 3}: +1
+Y{.x = 3, .y = 1, .z = 6}: +1
+Y{.x = 3, .y = 9, .z = 512}: +1
+Y{.x = 3, .y = 10, .z = 0}: +1
+Y{.x = 3, .y = 11, .z = 0}: +1
+Y{.x = 3, .y = 15, .z = 0}: +1
+Y{.x = 3, .y = 16, .z = 3}: +1
+Y{.x = 3, .y = 17, .z = 6}: +1