Support hacker's delight

[eukaryo]

I tried the following code in flux-playfround, but flux did not proved the postcondition. Z3 SMT solver probably can solve the problem. I wish flux could handle algorithms that involve bit manipulation like this code.

#![allow(unused)]

#[flux::sig(fn(x0: u64) -> u64{x6: x6 <= 64})]
fn popcount(x0: u64) -> u64 {
    let x1 = (x0 & 0x5555_5555_5555_5555u64) + ((x0 >> 1) & 0x5555_5555_5555_5555u64);
    let x2 = (x1 & 0x3333_3333_3333_3333u64) + ((x1 >> 2) & 0x3333_3333_3333_3333u64);
    let x3 = (x2 & 0x0f0f_0f0f_0f0f_0f0fu64) + ((x2 >> 4) & 0x0f0f_0f0f_0f0f_0f0fu64);
    let x4 = (x3 & 0x00ff_00ff_00ff_00ffu64) + ((x3 >> 8) & 0x00ff_00ff_00ff_00ffu64);
    let x5 = (x4 & 0x0000_ffff_0000_ffffu64) + ((x4 >> 16) & 0x0000_ffff_0000_ffffu64);
    let x6 = (x5 & 0x0000_0000_ffff_ffffu64) + ((x5 >> 32) & 0x0000_0000_ffff_ffffu64);
    x6
}

[ranjitjhala]

Thanks for this interesting use-case; we're going to start tweaking interface with the SMT solver so this will be a handy testcase!

[nilehmann]

The reason we don't support this out of the box is that bit vectors are way too slow to make them the default encoding of integers.

We do have some support for bit vectors, but you need a wrapper type see https://github.com/flux-rs/flux/blob/main/tests/tests/lib/rbitvec.rs and https://github.com/flux-rs/flux/blob/main/tests/tests/pos/surface/bitvec01.rs. We haven't implemented all the operators on bit vector so the example in the op is not currently expressible, but I think we could easily add support to write the example as:

#[flux::sig(fn(x0: u64) -> u64{x6: x6 <= 64})]
fn popcount(x0: u64) -> u64 {
    let x0 = Bv64::from_u64(x0);
    let x1 = (x0 & 0x5555_5555_5555_5555u64) + ((x0 >> 1) & 0x5555_5555_5555_5555u64);
    let x2 = (x1 & 0x3333_3333_3333_3333u64) + ((x1 >> 2) & 0x3333_3333_3333_3333u64);
    let x3 = (x2 & 0x0f0f_0f0f_0f0f_0f0fu64) + ((x2 >> 4) & 0x0f0f_0f0f_0f0f_0f0fu64);
    let x4 = (x3 & 0x00ff_00ff_00ff_00ffu64) + ((x3 >> 8) & 0x00ff_00ff_00ff_00ffu64);
    let x5 = (x4 & 0x0000_ffff_0000_ffffu64) + ((x4 >> 16) & 0x0000_ffff_0000_ffffu64);
    let x6 = (x5 & 0x0000_0000_ffff_ffffu64) + ((x5 >> 32) & 0x0000_0000_ffff_ffffu64);
    x6.to_u64()
}

It'd be neat to support bitvectors directly on integers as an opt-in behavior, but I'm not sure what that would look like because we would need some way to change the encoding of integers locally.

[ranjitjhala]

@nilehmann -- The verus people have a thing called assert BLAH by (bit_vector) -- to specify this but I think that's too hard for us and also unclear that's what we want. I was thinking something like a "function-level" thing e.g.

#[flux::bit_blast(u64, Bv64)]
fn popcount(x0: u64) -> u64 {
  ...
}

would tell flux to tell encode all u64 as Bv64 when checking the constraints generated by popcount.

WDYT?

[nilehmann]

Yes, something like that could work. However, I did some testing, and the queries we are generating for the stuff we do support just hang fixpoint. It makes me think we are doing something wrong. Or are bit vectors really that slow?

[ranjitjhala]

Bit vectors are just that slow -- in these cases, the query is mostly going straight to Z3, not much happening in fixpoint. That said, it could be there are some special flags to pass to the SMT solver / Z3 that make it more effective with bitvectors. When stuff hangs, you can:

1. Just run fixpoint directly on the generated file,
2. That will, in the .liquid directory, generate itself another .smt2 file which is the actual query sent to Z3,
3. You can then just run z3 on the query itself to see if it freezes.

Usually they (z3/cvc/etc.) are very good about getting back if one has queries that choke their solvers...