Why are solvers timing out on a trivial bitmask function?

user_17813271 0
Viewed 56

Getting started with frama-c and decided to prove a trivial bitmask function worked as intended.

/*@ requires width > 0 && width <= 64 ;
    assigns \nothing ;
    ensures \result > 0 ;
    ensures \result == (1 << width) - 1 ;
*/
uint64_t gen_mask(uint64_t width) {
    if (width >= 64)
        return 0xffffffffffffffff;
    else
        return ((uint64_t)1 << width) - 1;
}

Unfortunately even the obvious statement that result > 0 times out with both alt-ego and z3 provers.

[wp] [Alt-Ergo 2.4.1] Goal typed_gen_mask_ensures : Timeout (Qed:2ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_gen_mask_ensures_2 : Timeout (Qed:2ms) (10s)

What's wrong with my specification? The provers only have to check 64 cases even if they brute-force it, so they shouldn't be timing out.

frama-c
1 Answers

By default, WP does not apply all strategies; this could lead to state space explosion in the general case, and it's not obvious which strategies to automatically enable in which cases.

In your example in particular, the Range strategy is the one which performs splitting of the 64 cases, and it can be enabled in the command line via option -wp-auto wp:range.

In the graphical interface, in the WP Goals tab, if you double-click the unproven goal, the rightmost panel will list some tactics to be applied via the "Play" buttons next to them. This can help find out about other tactics and strategies that you can enable in WP.

Frama-C GUI screenshot of the WP Goals' tactics panel

user_11736740
Related