From 586e3a86c0daddedaaf1ebb2e80cdc91c4351f5a Mon Sep 17 00:00:00 2001 From: septract Date: Wed, 12 Feb 2025 15:47:02 -0800 Subject: [PATCH] Add timeouts from cerberus issues #856 and #844 --- .../broken/error-timeout/case_timeout.c | 22 ++++++ .../broken/error-timeout/mult_timeout.c | 10 +++ .../error-timeout/overflow_timeout_3var.c | 69 ++++++++++++++++++ .../error-timeout/overflow_timeout_4var.c | 71 +++++++++++++++++++ 4 files changed, 172 insertions(+) create mode 100644 src/example-archive/simple-examples/broken/error-timeout/case_timeout.c create mode 100644 src/example-archive/simple-examples/broken/error-timeout/mult_timeout.c create mode 100644 src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c create mode 100644 src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c diff --git a/src/example-archive/simple-examples/broken/error-timeout/case_timeout.c b/src/example-archive/simple-examples/broken/error-timeout/case_timeout.c new file mode 100644 index 00000000..4238f9a2 --- /dev/null +++ b/src/example-archive/simple-examples/broken/error-timeout/case_timeout.c @@ -0,0 +1,22 @@ +// Filed by @lwli11, see https://github.com/rems-project/cerberus/issues/856 + +#include + +int case_timeout(int a, int b){ + if (a==0 || b==0){ + return 0; + } + else if (a > 0 && b>0 && INT_MAX / b > a){ + return a*b; + } + else if (a>0 && b <0 && b > INT_MIN/a){ + return a*b; + } + else if (a<0 && b>0 && a > INT_MIN / b){ + return a*b; + } + else if (a<0 && b<0 && b > INT_MAX / a){ + return a*b; + } + return 0; +} \ No newline at end of file diff --git a/src/example-archive/simple-examples/broken/error-timeout/mult_timeout.c b/src/example-archive/simple-examples/broken/error-timeout/mult_timeout.c new file mode 100644 index 00000000..cf3185c3 --- /dev/null +++ b/src/example-archive/simple-examples/broken/error-timeout/mult_timeout.c @@ -0,0 +1,10 @@ +// Filed by @lwli11, see https://github.com/rems-project/cerberus/issues/856 + +#include + +int mult_timeout(int a, int b){ + if (a > 0 && b>0 && INT_MAX / b > a){ + return a*b; + } + return 0; +} diff --git a/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c new file mode 100644 index 00000000..481a5a85 --- /dev/null +++ b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_3var.c @@ -0,0 +1,69 @@ +// Filed by @lwli11, see https://github.com/rems-project/cerberus/issues/844 + +#include + +extern int pow(int a, int b); +/*@ + spec pow(i32 a, i32 b); + requires true; + ensures true; +@*/ + +typedef struct { + uint16_t x; + uint16_t y; + uint16_t z; + uint16_t a; + uint16_t b; +} example_t; +int overflow_timeout_3var(example_t* p1,example_t* p2) +/*@ + requires take x = Owned(p1); + take y = Owned(p2); + ensures take x2 = Owned(p1); + take y2 = Owned(p2); +@*/ +{ + int distance = 0; + + if (!((int)p2->x > 0 && (int)p1->x< INT_MIN + (int)p2->x) && !((int)p2->x <0 && (int)p1->x > INT_MAX + (int)p2->x)){ + distance += pow((int)p1->x - (int)p2->x, 2); + } + + if (!((int)p2->y > 0 && (int)p1->y < INT_MIN + (int)p2->y) && !((int)p2->y <0 && (int)p1->y > INT_MAX + (int)p2->y)){ + + int tmp = pow((int)p1->y - (int)p2->y, 2); + if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) { + distance +=tmp; + } + } + + if (!((int)p2->z > 0 && (int)p1->z < INT_MIN + (int)p2->z) && !((int)p2->z <0 && (int)p1->z > INT_MAX + (int)p2->z)){ + int tmp = pow((int)p1->z - (int)p2->z, 2); + + if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) { + distance +=tmp; + } + + } +/* // 4var version - takes longer + if (!((int)p2->a > 0 && (int)p1->a < INT_MIN + (int)p2->a) && !((int)p2->a <0 && (int)p1->a > INT_MAX + (int)p2->a)){ + int tmp = pow((int)p1->a - (int)p2->a, 2); + + if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) { + distance +=tmp; + } + } + // 5var version - doesn't terminate + if (!((int)p2->b > 0 && (int)p1->b < INT_MIN + (int)p2->b) && !((int)p2->b <0 && (int)p1->b > INT_MAX + (int)p2->b)){ + int tmp = pow((int)p1->b - (int)p2->b, 2); + + if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) { + distance +=tmp; + } + } + +*/ + return distance; + +} diff --git a/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c new file mode 100644 index 00000000..44ee9a84 --- /dev/null +++ b/src/example-archive/simple-examples/broken/error-timeout/overflow_timeout_4var.c @@ -0,0 +1,71 @@ +// Filed by @lwli11, see https://github.com/rems-project/cerberus/issues/844 + +#include + +extern int pow(int a, int b); +/*@ + spec pow(i32 a, i32 b); + requires true; + ensures true; +@*/ + +typedef struct { + uint16_t x; + uint16_t y; + uint16_t z; + uint16_t a; + uint16_t b; +} example_t; +int overflow_timeout_4var(example_t* p1,example_t* p2) +/*@ + requires take x = Owned(p1); + take y = Owned(p2); + ensures take x2 = Owned(p1); + take y2 = Owned(p2); +@*/ +{ + int distance = 0; + + if (!((int)p2->x > 0 && (int)p1->x< INT_MIN + (int)p2->x) && !((int)p2->x <0 && (int)p1->x > INT_MAX + (int)p2->x)){ + distance += pow((int)p1->x - (int)p2->x, 2); + } + + if (!((int)p2->y > 0 && (int)p1->y < INT_MIN + (int)p2->y) && !((int)p2->y <0 && (int)p1->y > INT_MAX + (int)p2->y)){ + + int tmp = pow((int)p1->y - (int)p2->y, 2); + if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) { + distance +=tmp; + } + } + + if (!((int)p2->z > 0 && (int)p1->z < INT_MIN + (int)p2->z) && !((int)p2->z <0 && (int)p1->z > INT_MAX + (int)p2->z)){ + int tmp = pow((int)p1->z - (int)p2->z, 2); + + if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) { + distance +=tmp; + } + + } + + // 4var version - takes longer + if (!((int)p2->a > 0 && (int)p1->a < INT_MIN + (int)p2->a) && !((int)p2->a <0 && (int)p1->a > INT_MAX + (int)p2->a)){ + int tmp = pow((int)p1->a - (int)p2->a, 2); + + if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) { + distance +=tmp; + } + } + +/* // 5var version - doesn't terminate + if (!((int)p2->b > 0 && (int)p1->b < INT_MIN + (int)p2->b) && !((int)p2->b <0 && (int)p1->b > INT_MAX + (int)p2->b)){ + int tmp = pow((int)p1->b - (int)p2->b, 2); + + if (!(tmp > 0 && (distance > (INT_MAX - tmp) )) && !(tmp < 0 && (distance < (INT_MIN - tmp) ) )) { + distance +=tmp; + } + } + +*/ + return distance; + +}