From 1aa34c6a6ac81617b679553c0bd831653705f048 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 9 Jun 2022 14:55:34 +0100 Subject: [PATCH 1/4] Add a regression test covering casting pointers form integer values. --- .../pointers-conversions/pointer_from_int.c | 13 +++++++++++++ .../pointers-conversions/pointer_from_int.desc | 16 ++++++++++++++++ 2 files changed, 29 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers-conversions/pointer_from_int.c create mode 100644 regression/cbmc-incr-smt2/pointers-conversions/pointer_from_int.desc diff --git a/regression/cbmc-incr-smt2/pointers-conversions/pointer_from_int.c b/regression/cbmc-incr-smt2/pointers-conversions/pointer_from_int.c new file mode 100644 index 00000000000..6879ef74e34 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-conversions/pointer_from_int.c @@ -0,0 +1,13 @@ +int main() +{ + int *p = (int *)4; + __CPROVER_allocated_memory(4, sizeof(int)); + + __CPROVER_assert(p == 4, "p == 4: expected success"); + __CPROVER_assert(p != 0, "p != 0: expected success"); + + p = (int *)0x1020304; + __CPROVER_assert(p == 0x1020304, "p == 0x1020304: expected success"); + __CPROVER_assert(p != 0, "p != 0: expected success"); + __CPROVER_assert(p == 0, "p != 0: expected failure"); +} diff --git a/regression/cbmc-incr-smt2/pointers-conversions/pointer_from_int.desc b/regression/cbmc-incr-smt2/pointers-conversions/pointer_from_int.desc new file mode 100644 index 00000000000..b5a51cc0000 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-conversions/pointer_from_int.desc @@ -0,0 +1,16 @@ +CORE +pointer_from_int.c +--trace +\[main\.assertion\.1\] line \d+ p == 4: expected success: SUCCESS +\[main\.assertion\.2\] line \d+ p != 0: expected success: SUCCESS +\[main\.assertion\.3\] line \d+ p == 0x1020304: expected success: SUCCESS +\[main\.assertion\.4\] line \d+ p != 0: expected success: SUCCESS +\[main\.assertion\.5\] line \d+ p != 0: expected failure: FAILURE +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test is covering basic conversion of pointer values to integers. +It contains two such conversions, one of an integer in decimal form, +and one of an integer in a hexadecimal form. From c47678d9bf09ae1abdf7011041df1619ecbbf449 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 10 Jun 2022 16:00:04 +0100 Subject: [PATCH 2/4] Add an integer value round trip (int -> void* -> int) test --- .../pointers-conversions/pointer_round_trip.c | 13 +++++++++++++ .../pointers-conversions/pointer_round_trip.desc | 11 +++++++++++ 2 files changed, 24 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers-conversions/pointer_round_trip.c create mode 100644 regression/cbmc-incr-smt2/pointers-conversions/pointer_round_trip.desc diff --git a/regression/cbmc-incr-smt2/pointers-conversions/pointer_round_trip.c b/regression/cbmc-incr-smt2/pointers-conversions/pointer_round_trip.c new file mode 100644 index 00000000000..c731f33de77 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-conversions/pointer_round_trip.c @@ -0,0 +1,13 @@ +int f(int x) +{ + void *p = (void *)x; + int r = (int)p; + return r; +} + +int main() +{ + int a = f(5); + __CPROVER_assert(a == 5, "a == 5: expected success"); + __CPROVER_assert(a != 5, "a != 5: expected failure"); +} diff --git a/regression/cbmc-incr-smt2/pointers-conversions/pointer_round_trip.desc b/regression/cbmc-incr-smt2/pointers-conversions/pointer_round_trip.desc new file mode 100644 index 00000000000..0cfeb602d6c --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-conversions/pointer_round_trip.desc @@ -0,0 +1,11 @@ +CORE +pointer_round_trip.c +--trace +\[main\.assertion\.1\] line \d+ a == 5: expected success: SUCCESS +\[main\.assertion\.2\] line \d+ a != 5: expected failure: FAILURE +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test is testing an integer value round trip (int -> pointer -> int) test. From f80319718acc60fbd65522da6814b08b73e15ffe Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 10 Jun 2022 16:20:28 +0100 Subject: [PATCH 3/4] Add a test based on the conversion of casting of pointer values --- .../pointers-conversions/pointer_to_int.c | 19 +++++++++++++++++++ .../pointers-conversions/pointer_to_int.desc | 16 ++++++++++++++++ 2 files changed, 35 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.c create mode 100644 regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc diff --git a/regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.c b/regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.c new file mode 100644 index 00000000000..35eb5b4e25a --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.c @@ -0,0 +1,19 @@ +int cmp(const void *p1, const void *p2) +{ + int x = *(int *)p1; + int y = *(int *)p2; + + return (x < y) ? -1 : ((x == y) ? 0 : 1); +} + +int main() +{ + int a = 5; + int b = 6; + int c = 7; + + __CPROVER_assert(cmp(&a, &b) == -1, "expected result == -1: success"); + __CPROVER_assert(cmp(&c, &b) == 1, "expected result == 1: success"); + __CPROVER_assert(cmp(&c, &c) == 0, "expected result == 0: success"); + __CPROVER_assert(cmp(&c, &c) == 1, "expected result == 1: failure"); +} diff --git a/regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc b/regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc new file mode 100644 index 00000000000..f9cfae9d67e --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc @@ -0,0 +1,16 @@ +CORE +pointer_to_int.c +--trace +\[main\.assertion\.1\] line \d+ expected result == -1: success: SUCCESS +\[main\.assertion\.2\] line \d+ expected result == 1: success: SUCCESS +\[main\.assertion\.3\] line \d+ expected result == 0: success: SUCCESS +\[main\.assertion\.4\] line \d+ expected result == 1: failure: FAILURE +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test is covering basic conversion of casting of different pointer values, +which are then dereferenced and used in the function. We are asserting against +the result of the function, which cannot be right, unless the conversions +work as they should. From 126cfff220f31e0ae513d3f13b098681ff64714e Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 13 Jun 2022 11:39:27 +0100 Subject: [PATCH 4/4] Add two tests (marked `KNOWNBUG` for now) as documentation for lack of support for byte operations on pointers. In particular the tests regard `byte_extract_little_endian` and `byte_update_little_endian` expressions. --- .../pointers-conversions/byte_extract_issue.c | 12 ++++++++++++ .../pointers-conversions/byte_extract_issue.desc | 10 ++++++++++ .../pointers-conversions/byte_update_issue.c | 12 ++++++++++++ .../pointers-conversions/byte_update_issue.desc | 10 ++++++++++ 4 files changed, 44 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.c create mode 100644 regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.desc create mode 100644 regression/cbmc-incr-smt2/pointers-conversions/byte_update_issue.c create mode 100644 regression/cbmc-incr-smt2/pointers-conversions/byte_update_issue.desc diff --git a/regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.c b/regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.c new file mode 100644 index 00000000000..1abb1cb267c --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.c @@ -0,0 +1,12 @@ +#include +#include + +int main() +{ + uint32_t input; + uint32_t original = input; + uint8_t *ptr = (uint8_t *)(&input); + assert(*ptr == 0); // falsifiable + *ptr = ~(*ptr); + assert(input != original); // valid +} diff --git a/regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.desc b/regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.desc new file mode 100644 index 00000000000..7811c4ad4e0 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-conversions/byte_extract_issue.desc @@ -0,0 +1,10 @@ +KNOWNBUG +byte_extract_issue.c +--trace +^EXIT=10$ +^SIGNAL=0$ +-- +Reached unimplemented Generation of SMT formula for byte extract expression: byte_extract_little_endian +-- +This test is here to document our lack of support for byte_extract_little_endian +in the pointers support for the new SMT backend. diff --git a/regression/cbmc-incr-smt2/pointers-conversions/byte_update_issue.c b/regression/cbmc-incr-smt2/pointers-conversions/byte_update_issue.c new file mode 100644 index 00000000000..27c3a4fbddc --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-conversions/byte_update_issue.c @@ -0,0 +1,12 @@ +#include +#include + +int main() +{ + uint32_t x = 0; + uint8_t *ptr = (uint8_t *)(&x); + int offset; + __CPROVER_assume(offset >= 0 && offset < 4); + *(ptr + offset) = 1; + assert(x != 256); +} diff --git a/regression/cbmc-incr-smt2/pointers-conversions/byte_update_issue.desc b/regression/cbmc-incr-smt2/pointers-conversions/byte_update_issue.desc new file mode 100644 index 00000000000..3a71b581fd4 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-conversions/byte_update_issue.desc @@ -0,0 +1,10 @@ +KNOWNBUG +byte_update_issue.c +--trace +^EXIT=10$ +^SIGNAL=0$ +-- +Reached unimplemented Generation of SMT formula for byte extract expression: byte_update_little_endian +-- +This test is here to document our lack of support for byte_update_little_endian +in the pointers support for the new SMT backend.