Regression tests for the SMT bitvector arithmetic operator conversion

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.c

@@ -0,0 +1,14 @@
+#include <limits.h>
+#include <stdlib.h>
+
+int main()
+{
+  int a = INT_MAX;
+  int b = INT_MIN;
+
+  __CPROVER_assert(
+    a + 1 == INT_MIN, "Wrap-around to INT_MIN when adding to INT_MAX");
+  __CPROVER_assert(
+    b - 1 == INT_MAX, "Wrap-around to INT_MAX when subtracting from INT_MIN");
+  __CPROVER_assert(a - b == -1, "INT_MAX minus INT_MIN equals -1");
+}

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc

@@ -0,0 +1,13 @@
+CORE
+overflow_behaviour.c
+--incremental-smt2-solver 'z3 --smt2 -in' --trace
+\[main\.assertion\.1\] line \d+ Wrap-around to INT_MIN when adding to INT_MAX: SUCCESS
+\[main\.assertion\.2\] line \d+ Wrap-around to INT_MAX when subtracting from INT_MIN: SUCCESS
+\[main\.assertion\.3\] line \d+ INT_MAX minus INT_MIN equals -1: SUCCESS
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test is designed to test wrap-around behaviour for boundary-values
+of the int domain.

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.c

@@ -0,0 +1,16 @@
+#include <stdbool.h>
+
+int main()
+{
+  int x;
+  __CPROVER_assume(x < 100);
+  __CPROVER_assume(x > -100);
+  bool quadratic_solved = (x + 8) * (x - 42) == 0;
+
+  if(x < 0)
+    __CPROVER_assert(!quadratic_solved, "No negative solution");
+  else
+    __CPROVER_assert(!quadratic_solved, "No positive solution");
+
+  return 0;
+}

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc

@@ -0,0 +1,15 @@
+CORE
+polynomial.c
+--incremental-smt2-solver 'z3 --smt2 -in' --trace
+\[main\.assertion\.1\] line \d+ No negative solution: FAILURE
+\[main\.assertion\.2\] line \d+ No positive solution: FAILURE
+x=-8\ \(11111111 11111111 11111111 11111000\)
+x=42\ \(00000000 00000000 00000000 00101010\)
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is an end-to-end test making sure that CBMC has encoded
+the problem and sent it to the SMT solver, and we manage to
+get the solutions to the polynomial back through the trace.

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.c

@@ -0,0 +1,34 @@
+#include <stdlib.h>
+
+int main()
+{
+  int a;
+  __CPROVER_assume(a < 100);
+  __CPROVER_assume(a > -100);
+  __CPROVER_assume(a != 0);
+
+  // Simple algebraic identities - expected to drive the SMT backend
+  __CPROVER_assert(a + a == a * 2, "a plus a always equals two times a");
+  __CPROVER_assert(a - a == 0, "a minus a always equals 0");
+  __CPROVER_assert(a + -a == 0, "a plus its additive inverse equals 0");
+  __CPROVER_assert(
+    a - -a == 2 * a, "a minus its additive inverse equals two times a");
+  __CPROVER_assert((a * a) / a == a, "a squared divided by a equals a");
+  __CPROVER_assert((2 * a) / a == 2, "two times a divided by a equals two");
+  __CPROVER_assert(a % a == 0, "a mod itself equals 0");
+
+  // Same round of tests, but for a type of different size
+  long long int b;
+  __CPROVER_assume(b < 100ll);
+  __CPROVER_assume(b > -100ll);
+  __CPROVER_assume(b != 0ll);
+
+  __CPROVER_assert(b + b == b * 2ll, "b plus b always equals two times b");
+  __CPROVER_assert(b - b == 0ll, "b minus b always equals 0");
+  __CPROVER_assert(b + -b == 0ll, "b plus its additive inverse equals 0");
+  __CPROVER_assert(
+    b - -b == 2ll * b, "b minus its additive inverse equals two times b");
+  __CPROVER_assert((b * b) / b == b, "b squared divided by b equals b");
+  __CPROVER_assert((2ll * b) / b == 2ll, "two times b divided by b equals two");
+  __CPROVER_assert(b % b == 0ll, "b mod itself equals 0");
+}

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc

@@ -0,0 +1,27 @@
+CORE
+simple_equation.c
+--incremental-smt2-solver 'z3 --smt2 -in' --trace
+\[main\.assertion\.1\] line \d+ a plus a always equals two times a: SUCCESS
+\[main\.assertion\.2\] line \d+ a minus a always equals 0: SUCCESS
+\[main\.assertion\.3\] line \d+ a plus its additive inverse equals 0: SUCCESS
+\[main\.assertion\.4\] line \d+ a minus its additive inverse equals two times a: SUCCESS
+\[main\.assertion\.5\] line \d+ a squared divided by a equals a: SUCCESS
+\[main\.assertion\.6\] line \d+ two times a divided by a equals two: SUCCESS
+\[main\.assertion\.7\] line \d+ a mod itself equals 0: SUCCESS
+\[main\.assertion\.8\] line \d+ b plus b always equals two times b: SUCCESS
+\[main\.assertion\.9\] line \d+ b minus b always equals 0: SUCCESS
+\[main\.assertion\.10\] line \d+ b plus its additive inverse equals 0: SUCCESS
+\[main\.assertion\.11\] line \d+ b minus its additive inverse equals two times b: SUCCESS
+\[main\.assertion\.12\] line \d+ b squared divided by b equals b: SUCCESS
+\[main\.assertion\.13\] line \d+ two times b divided by b equals two: SUCCESS
+\[main\.assertion\.14\] line \d+ b mod itself equals 0: SUCCESS
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This is a simple test that's trying to verify that some simple algebraic
+identities hold for all values insider an integral interval. This is expected
+to work as an end-to-end example driving the all of the conversion function
+for bitvector arithmetic in the new SMT backend, getting us to the point of
+a full verification run producing a result.

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.c

@@ -0,0 +1,21 @@
+int main()
+{
+  unsigned int a;
+  unsigned int b = 12;
+  __CPROVER_assume(a > 15);
+
+  // expected to fail by assigning a = 4294967284u in the trace
+  // and wrapping around to 0, which results in 0 > 27.
+  __CPROVER_assert(a + b > 27, "a plus b should be more than 27");
+  // expected to fail by assigning a = 2147483648u in the trace
+  // and evaluating to 2147483660 > 27, which is true.
+  __CPROVER_assert(!(a + b > 27), "a plus b should be more than 27");
+
+  // Same round of tests but for unsigned long long.
+  unsigned long long int c;
+  unsigned long long int d = 12llu;
+  __CPROVER_assume(c > 15llu);
+
+  __CPROVER_assert(c + d > 27, "c plus d should be more than 27");
+  __CPROVER_assert(!(c + d > 27), "c plus d should be more than 27");
+}

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc

@@ -0,0 +1,16 @@
+CORE
+unsigned_behaviour.c
+--incremental-smt2-solver 'z3 --smt2 -in' --trace
+\[main\.assertion\.1\] line \d+ a plus b should be more than 27: FAILURE
+\[main\.assertion\.2\] line \d+ a plus b should be more than 27: FAILURE
+\[main\.assertion\.3\] line \d+ c plus d should be more than 27: FAILURE
+\[main\.assertion\.4\] line \d+ c plus d should be more than 27: FAILURE
+a=\d+(u|ul)?
+c=\d+(u|ul)?
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test checks for the correct behaviour of unsigned integers around
+boundary values.

src/util/piped_process.cpp

@@ -348,12 +348,30 @@ piped_processt::send_responset piped_processt::send(const std::string &message)
 #ifdef _WIN32
   const auto message_size = narrow<DWORD>(message.size());
   DWORD bytes_written = 0;
-  if(!WriteFile(
-       child_std_IN_Wr, message.c_str(), message_size, &bytes_written, NULL))
+  const auto write_file = [&]() {
+    return WriteFile(
+      child_std_IN_Wr, message.c_str(), message_size, &bytes_written, NULL);
+  };
+  if(!write_file())
   {
     // Error handling with GetLastError ?
     return send_responset::FAILED;
   }
+  // `WriteFile` can return a success status but write 0 bytes if we write
+  // messages quickly enough. This problem has been observed when using a
+  // release build, but resolved when using a debug build or `--verbosity 10`.
+  // Presumably this happens if cbmc gets too far ahead of the sub process.
+  // Flushing the buffer and retrying should then succeed to write the message
+  // in this case.
+  if(bytes_written == 0)
+  {
+    FlushFileBuffers(child_std_IN_Wr);
+    if(!write_file())
+    {
+      // Error handling with GetLastError ?
+      return send_responset::FAILED;
+    }
+  }
   INVARIANT(
     message_size == bytes_written,
     "Number of bytes written to sub process must match message size.");