Frama-C does not recognize valid memory access from bitwise-ANDed index

Question

I am right-shifting an unsigned integer then &ing it with 0b111, so the resulting value must be in the range [0, 7].

When I use that value as an index into an array of length 8, Frama-C is not able to verify the associated rte: mem_access assertion.

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

/*@
  requires \valid_read(bitRuleBuf + (0 .. 7));
  assigns \nothing;
  ensures \forall uint8_t c; (0 <= c < 8) ==> (
    ((\result >> c) & 0b1) <==> bitRuleBuf[(state >> c) & 0b111]
  );
*/
uint8_t GetNewOctet(
    const uint16_t state,
    const bool bitRuleBuf[const static 8])
{
    uint8_t result = 0;

    /*
      loop invariant 0 <= b <= 8;
      loop invariant \forall uint8_t c; (0 <= c < b) ==> (
        ((result >> c) & 0b1) <==> bitRuleBuf[(state >> c) & 0b111]
      );
      loop assigns b, result;
      loop variant 8 - b;
    */
    for (uint8_t b = 0; b < 8; b += 1) {
        result |= ((uint8_t)bitRuleBuf[(state >> b) & 0b111]) << b;

        // Still seeing an issue if break apart the steps:
        /*
        const uint16_t shifted  = state >> b;
        const uint16_t anded    = shifted & 0b111;

        // "assert rte: mem_access" is not successful here.
        const uint8_t  value    = bitRuleBuf[anded];
        const uint8_t  shifted2 = value << b;

        result |= shifted2;
        */
    }

    return result;
}

/*@
  assigns \nothing;
*/
int main(void) {
    // Empty cells with both neighbors empty become alive.
    // All other cells become empty.
    const bool bitRuleBuf[] = {
        1, // 0b000
        0, // 0b001
        0, // 0b010
        0, // 0b011
        0, // 0b100
        0, // 0b101
        0, // 0b110
        0  // 0b111
    };

    const uint8_t newOctet = GetNewOctet(0b0010000100, bitRuleBuf);

    //assert(newOctet == 0b00011000); // Can be uncommented to verify.

    //@ assert newOctet == 0b00011000;

    return 0;
}

The failed assertion happens for line 27: result |= ((uint8_t)bitRuleBuf[(state >> b) & 0b111]) << b;.

Changing the & 0b111 to % 8 does not resolve the issue. I have tried many variations of the code and ACSL involved, but have not been successful. I'm guessing integer promotion might be involved in the issue.

How can the code/ACSL be modified so that verification is successful?

$ frama-c --version
24.0 (Chromium)

I am running frama-c and frama-c-gui with arguments -wp and -wp-rte.

For background of the included block of code, the least significant 10 bits of the state argument are the state of 10 cells of 1-dimensional cellular automata. The function returns the next state of the middle 8 cells of those 10.

Edit: Alt-Ergo 2.4.1 is used:

$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
1 prover(s) added
Save config to /home/user/.why3.conf

Answer 1

First, a small note: if you're using WP, it is also important to state which solvers you have configured: each of them has strengths and weaknesses, so that it might be easier to complete a proof with the appropriate solver. In particular, my answer is based on the use of Z3 (4.8.14), known as z3-ce by why3 config detect (note that you have to run this command each time you change the set of solvers you use).

EDIT As mentioned in comments below, the Mod-Mask tactic is not available in Frama-C 24.0, but only in the development version (https://git.frama-c.com/pub/frama-c). As far as I can tell, for a Frama-C 24.0 solution, you need to resort to a Coq script as mentioned at the end of this answer.

Z3 alone is not sufficient to complete the proof, but you can use a WP tactic (see section 2.2 of the WP manual about the interactive proof editor in Frama-C's GUI). Namely, if you select land(7, to_sint32(x)) in the proof editor, the tactics panel will show you a Mod-Mask tactic, which converts bitmasks to modulo operations and vice-versa (see image below). If you apply it, Z3 will complete the two resulting proof obligations, completing the proof of the assertion.

After that, you can save the script in order to be able to replay it later: use e.g. -wp-prover script,z3-ce,alt-ergo to let WP take advantage of existing scripts in addition to automated solvers. The scripts are searched for (and saved to) the script subdirectory of the WP session directory, which defaults to ./.frama-c/wp and can be set with -wp-session.

Another possibility is to use a Coq script to complete the proof. This supposes you have Coq, CoqIDE and the Why3 Coq libraries installed (they are available as opam packages coq, coqide and why3-coq respectively). Once this is done and you have configured Why3 to use Coq (why3 config detect should tell you that it has found Coq), you can use it through the GUI of Frama-C to complete proofs that the built-in interactive prover can't take care of.

For that, you may need to configure Frama-C to display a Coq column in the WP Goals panel: click on the Provers button in this panel, and make sure that Coq is ON, as shown below:

Once this is done, you can double-click in the cell of this column that corresponds to the proof obligation you want to discharge with Coq. This will open a CoqIDE session where you have to complete the proof script at then end of the opened file. Once this is done, save the file and quit CoqIDE. The Coq script will then be saved as part of the WP session, and can be played again if coq is among the arguments given to -wp-prover. For what it's worth, the following script seems to do the trick (Coq 8.13.2, Why3 1.4.1, and of course Frama-C 24.0):

intros alloc mem_int b buf state0 state1 x a1 hpos hval hbmax hbmax1 htyp hlink huint1 huint2 huint3 hvalid htyp1 htyp2 hdef.
assert (0<=land 7 (to_sint32 x) <= 7)%Z.
apply uint_land_range; auto with zarith.
unfold valid_rd.
unfold valid_rd in hvalid.
unfold a1.
unfold shift; simpl.
unfold shift in hvalid; simpl in hvalid.
assert (to_sint32 (land 7 (to_sint32 x)) = land 7 (to_sint32 x))%Z.
- apply id_sint32; unfold is_sint32; auto with zarith.
- intros _; repeat split; auto with zarith.