How do I write an "is power of 2" predicate in ACSL?

user_2505159 0
Viewed 153

My attempt to write an ACSL predicate to see if an integer is a power of 2 goes like this:

/*@
  predicate positive_power_of_2 (integer i) =
    i > 0 &&
    (i == 1 || ((i & 1) == 0 && positive_power_of_2 (i >> 1)));
 */

However when I added some assert lines into a random function, some Timeout (ie. fail). I don't understand why?

//@ assert positive_power_of_2 (1);  // Timeout
//@ assert positive_power_of_2 (2);  // Valid
//@ assert positive_power_of_2 (4);  // Valid
//@ assert !positive_power_of_2 (7); // Timeout
acsl frama-c
1 Answers

As a side note, for such purely logic properties, you can use lemmas instead of assert, as in //@ lemma pow2_1: positive_power_of_2(1);. Since a lemma is a global annotation, it spares you from writing a function just for the sake of holding an assert.

Now back to the issue itself. Mixing bitwise operations with arithmetic ones (the less-than comparison) tends to confuse automated theorem provers. You did not specify which one(s) you use, but if you only used one, you might want to try installing others (nowadays, a mix of alt-ergo, z3 and cvc4 tends to provide good results). That said, a small interactive help to WP's internal simplifier QED is also sufficient: by using the GUI (see section 2.4 of WP manual), you can conclude by just unfolding the definition of positive_power_of_2 in each of the goals (as far as I know, there's no command-line option to do the equivalent).

Basically, once you are in the WP Proofs panel of the GUI, you have to double click in the Script column of the row corresponding to the proof obligation you want to work on, which will let you enter the interactive proof mode, as in the screenshot below:

WP interactive proof mode in Frama-C GUI

Now, the point is that the list of available tactics (on the right) is contextual: only the ones that are relevant for the term you have selected in the proof obligation (on the left) are shown. Some tactics are always relevant, such as Cut, which let you prove an auxiliary statement that can be used as an hypothesis in the rest of the proof, but unfolding a definition only makes sense if there's a definition to unfold in your selection. Hence you have to click on P_positive_power_of_2 to let the tactic appear. Afterwards, just click on the corresponding triangle to let WP unfold the definition and attempt to complete the proof afterwards.

user_16336650
Related