Unexpected timeout using __CPROVER_overflow_mult

[nchong-at-aws]

CBMC version: 5.48.0
Operating system: Ubuntu 20.04.3
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: VERIFICATION SUCCESSFUL
What happened instead: Timeout

The following test approximates the output of the Kani verifier (https://github.com/model-checking/rmc) which uses __CPROVER_overflow_mult to detect unsigned integer wraparound. This test results in a timeout with CBMC.

Switching the implementation to using a wider integer to detect the wraparound (using -DUSE_LARGER_WIDTH) results in the test being fast to verify with CBMC.

#include <stdint.h>
#include <stdlib.h>
#include <stdbool.h>
#include <assert.h>

struct rectangle {
    uint64_t width;
    uint64_t height;
};

bool can_hold(struct rectangle self, struct rectangle other) {
    return self.width > other.width && self.height > other.height;
}

bool stretch(struct rectangle self, uint64_t factor, struct rectangle *result) {
#ifdef USE_LARGER_WIDTH
    __uint128_t w = (__uint128_t) self.width * (__uint128_t) factor;
    if (0xffffffffffffffff < w) {
	return false;
    }
    __uint128_t h = (__uint128_t) self.height * (__uint128_t) factor;
    if (0xffffffffffffffff < h) {
	return false;
    }
#else // simulate kani output
    if (__CPROVER_overflow_mult(self.width, factor)) {
        return false;
    }
    if (__CPROVER_overflow_mult(self.height, factor)) {
        return false;
    }
    uint64_t w = self.width * factor;
    uint64_t h = self.height * factor;
#endif
    result->width = w;
    result->height = h;
    return true;
}

uint64_t nondet_uint64_t();

int main() {
    struct rectangle original = { nondet_uint64_t(), nondet_uint64_t() };
    uint64_t factor = nondet_uint64_t();
    __CPROVER_assume(0 != original.width);
    __CPROVER_assume(0 != original.height);
    __CPROVER_assume(1 < factor);
    struct rectangle result = { nondet_uint64_t(), nondet_uint64_t() };
    if (stretch(original, factor, &result)) {
        assert(can_hold(result, original));
    }
    return 0;
}

[tautschnig]

There is the inherent hardness of multiplication. What, as far as I can see, causes the surprising behaviour here is that __CPROVER_overflow_mult will also do the multiplication (but only returns whether there was an overflow or not). Consequently, the code when not using USE_LARGER_WIDTH will cause four multipliers to be encoded, while USE_LARGER_WIDTH entails only two of them.

In my opinion, we should seek to introduce something along the lines of

struct result_with_overflow
{
  T result;
  __CPROVER_bool overflow;
} __attribute__((packed));
result_with_overflow __CPROVER_mult_with_overflow(T, T);

so that you could write code

struct result_with_overflow r = __CPROVER_mult_with_overflow(a, b);
if(!r.overflow) ... use r.result ...

[tautschnig]

I'm afraid it only dawned on me today that we actually have support for what I said two days ago already in place. The following modified version of your code works, and works with about the same performance as -DUSE_LARGER_WIDTH:

#include <stdint.h>
#include <stdlib.h>
#include <stdbool.h>
#include <assert.h>

struct rectangle {
    uint64_t width;
    uint64_t height;
};

bool can_hold(struct rectangle self, struct rectangle other) {
    return self.width > other.width && self.height > other.height;
}

bool stretch(struct rectangle self, uint64_t factor, struct rectangle *result) {
#ifdef USE_LARGER_WIDTH
    __uint128_t w = (__uint128_t) self.width * (__uint128_t) factor;
    if (0xffffffffffffffff < w) {
	return false;
    }
    __uint128_t h = (__uint128_t) self.height * (__uint128_t) factor;
    if (0xffffffffffffffff < h) {
	return false;
    }
    result->width = w;
    result->height = h;
#else // simulate kani output
    // if (__CPROVER_overflow_mult(self.width, factor)) {
    if (__builtin_mul_overflow(self.width, factor, &result->width)) {
        return false;
    }
    // if (__CPROVER_overflow_mult(self.height, factor)) {
    if (__builtin_mul_overflow(self.height, factor, &result->height)) {
        return false;
    }
    // uint64_t w = self.width * factor;
    // uint64_t h = self.height * factor;
#endif
    return true;
}

uint64_t nondet_uint64_t();

int main() {
    struct rectangle original = { nondet_uint64_t(), nondet_uint64_t() };
    uint64_t factor = nondet_uint64_t();
    __CPROVER_assume(0 != original.width);
    __CPROVER_assume(0 != original.height);
    __CPROVER_assume(1 < factor);
    struct rectangle result = { nondet_uint64_t(), nondet_uint64_t() };
    if (stretch(original, factor, &result)) {
        assert(can_hold(result, original));
    }
    return 0;
}

This uses the GCC built-in __builtin_mul_overflow, and in Kani you could directly access this using a side_effect_expr_overflowt, which you'd construct as an irep with the following structure:

• id: ID_side_effect
• ID_type: bool_typet (a type with ID_bool)
• ID_statement: "overflow-mult"
• two bitvector-typed operands (whatever is to be multiplied)
• one pointer-typed operand (where the result is to be stored)

Let me know whether that works for you!

[nchong-at-aws]

Awesome! Thanks Michael, I will try this out and get back to you.

[tautschnig]

Noting that it really takes #6616 to make sure __builtin_mul_overflow can be use safely.

[tautschnig]

The problems of __builtin_mul_overflow that #6616 could have fixed have now been addressed more cleanly in #6903, which introduces the struct expression suggested in my earlier post in here. Resolving this issue, but Kani will still need to pick this up.