diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.c b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.c new file mode 100644 index 00000000000..fdbacacb495 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.c @@ -0,0 +1,14 @@ +#include +#include + +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"); +} diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc new file mode 100644 index 00000000000..4e2f90d69b1 --- /dev/null +++ b/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. diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.c b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.c new file mode 100644 index 00000000000..2f086e2b56a --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.c @@ -0,0 +1,16 @@ +#include + +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; +} diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc new file mode 100644 index 00000000000..6149a33f6d1 --- /dev/null +++ b/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. diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.c b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.c new file mode 100644 index 00000000000..93a7b631a84 --- /dev/null +++ b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.c @@ -0,0 +1,34 @@ +#include + +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"); +} diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc new file mode 100644 index 00000000000..70a07e129fa --- /dev/null +++ b/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. diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.c b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.c new file mode 100644 index 00000000000..8d2fc040566 --- /dev/null +++ b/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"); +} diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc new file mode 100644 index 00000000000..db0157d613b --- /dev/null +++ b/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. diff --git a/src/util/piped_process.cpp b/src/util/piped_process.cpp index f11d63f3a5c..664ea6d1ebb 100644 --- a/src/util/piped_process.cpp +++ b/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(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.");