Regression tests for Bitwise Operators Conversion in new SMT backend

regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc

@@ -0,0 +1,11 @@
+CORE
+bitwise_ops.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+\[main\.assertion\.1\] line \d+ This is going to fail for bit-opposites: FAILURE
+\[main\.assertion\.2\] line \d+ This is going to hold for all values != 0: SUCCESS
+\[main\.assertion\.3\] line \d+ This is going to fail for the same value in A and B: FAILURE
+\[main\.assertion\.4\] line \d+ This will fail for the the same value in A and B: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise_ops.c

@@ -0,0 +1,24 @@
+int main()
+{
+  int a;
+  int b;
+
+  __CPROVER_assume(a != 0);
+
+  // This is going to be failing for values of `0000` and `1111` (as an example),
+  // as the bitwise-& of that will produce 0, failing this assertion.
+  __CPROVER_assert(a & b, "This is going to fail for bit-opposites");
+  // This will always be true, because bitwise-or allows a 1 at a bit
+  // that either A or B have set as one, and with an assumption of
+  // a != 0, there's always going to be at least 1 bit set, allowing
+  // the assertion below to evaluate to true.
+  __CPROVER_assert(a | b, "This is going to hold for all values != 0");
+  // This will fail for the same value, as an XOR of the bits will
+  // result in `0`, resulting in the assertion failure.
+  __CPROVER_assert(
+    a ^ b, "This is going to fail for the same value in A and B");
+  // This will fail for the exact same value of A and B, as
+  // NOT(A) will flip all the bits, resulting in the equality
+  // below to be false for the assertion.
+  __CPROVER_assert(~a == b, "This will fail for the the same value in A and B");
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.c

@@ -0,0 +1,10 @@
+int main()
+{
+  int starting_val = 1;
+  int shifting_places;
+  __CPROVER_assume(shifting_places > 0);
+  __CPROVER_assume(shifting_places < 32);
+  int result = starting_val << shifting_places;
+
+  __CPROVER_assert(result > 1, "Shifted result should be greater than one");
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc

@@ -0,0 +1,8 @@
+CORE
+shift_left.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+\[main\.assertion\.1\] line \d Shifted result should be greater than one: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--

regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.c

@@ -0,0 +1,40 @@
+#include <stdint.h>
+
+// In C, whether a right-shift is arithmetic or logical depends on the
+// original type being shifted. An unsigned value will be shifted to
+// the right in a logical manner (this assigns `0` to the leftmost bit).
+// If the type is signed, right shift will assign the sign bit to the
+// leftmost digit.
+
+int main()
+{
+  int first;
+  uint8_t second;
+
+  int place;
+  __CPROVER_assume(place >= 1);
+
+  int result_signed = first >> place;
+  uint8_t result_unsigned = second >> place;
+
+  // This assertion captures the intend of the expected behaviour of
+  // bit-shifting an unsigned int (logical shift)
+  __CPROVER_assert(
+    result_unsigned != 64,
+    "Right shifting a uint with leftmost bit set is a logical shift");
+  // The following assertions capture the expected behaviour of
+  // a right logical (in the case of a signed positive int) and
+  // arithmetic shift (in the case of a signed negative int).
+  if(first >= 0)
+  {
+    __CPROVER_assert(
+      result_signed >= 0,
+      "Right shifting a positive number has a lower bound of 0");
+  }
+  else
+  {
+    __CPROVER_assert(
+      result_signed <= -1,
+      "Right shifting a negative number has a lower bound value of -1");
+  }
+}

regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc

@@ -0,0 +1,12 @@
+CORE
+shift_right.c
+--incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --trace
+\[main\.assertion\.1\] line \d+ Right shifting a uint with leftmost bit set is a logical shift: FAILURE
+\[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: SUCCESS
+\[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: SUCCESS
+second=128
+result_unsigned=64
+^EXIT=10$
+^SIGNAL=0$
+--
+--