Annotations take forever to check - hang up in Z3

[vrindisbacher]

Hopefully this example helps narrow things down... I have two functions that do something fairly similar.

lmdia_w updates multiple general purpose register (which is refined by a map) with memory values (another map) at a given address. This address comes from a general purpose register.

ldmia_w_special does the exact same thing, except that it's address comes from a special purpose register.

ldmia_w checks in around 1 second, while ldmia_w_special hangs and hangs. I'm almost 100% sure that the hang up is in z3 because if I run FLUX_CHECK_DEF=ldmia_w_special cargo flux and use top I see fixpoint spin it's wheels for maybe a few seconds before z3 takes over and goes on and on.

The postcondition for ldmia_w is

ensures self: Armv7m { new_cpu: new_cpu == Armv7m {
    general_regs: gprs_post_ldmia_w(old_cpu, rd, rm1, rm2, rm3, rm4, rm5, rm6, rm7, rm8),
    ..old_cpu
}

where gprs_post_ldmia_w looks like:

    fn gprs_post_ldmia_w(
        cpu: Armv7m,
        rd: int,
        rm1: int,
        rm2: int,
        rm3: int,
        rm4: int,
        rm5: int,
        rm6: int,
        rm7: int,
        rm8: int
    ) -> Map<GPR, BV32> {
        map_set(
            map_set(
                map_set(
                    map_set(
                        map_set(
                            map_set(
                                map_set(
                                    map_set(
                                        cpu.general_regs,
                                        rm1,
                                        get_mem_addr(get_gpr(rd, cpu), cpu.mem)
                                    ),
                                    rm2,
                                    get_mem_addr(bv_add(get_gpr(rd, cpu), bv32(0x4)), cpu.mem)
                                ),
                                rm3,
                                get_mem_addr(bv_add(get_gpr(rd, cpu), bv32(0x8)), cpu.mem)
                            ),
                            rm4,
                            get_mem_addr(bv_add(get_gpr(rd, cpu), bv32(0xc)), cpu.mem)
                        ),
                        rm5,
                        get_mem_addr(bv_add(get_gpr(rd, cpu), bv32(0x10)), cpu.mem)
                    ),
                    rm6,
                    get_mem_addr(bv_add(get_gpr(rd, cpu), bv32(0x14)), cpu.mem)
                ),
                rm7,
                get_mem_addr(bv_add(get_gpr(rd, cpu), bv32(0x18)), cpu.mem)
            ),
            rm8,
            get_mem_addr(bv_add(get_gpr(rd, cpu), bv32(0x1c)), cpu.mem)
        )
    }

The spec for ldmia_w_special looks like:

ensures self: Armv7m { new_cpu: new_cpu == Armv7m {
        general_regs: gprs_post_ldmia_w_special(old_cpu, rd, rm1, rm2, rm3),
        ..old_cpu
    }
}

where gprs_post_ldmia_w_special looks like:

fn gprs_post_ldmia_w_special(
        cpu: Armv7m,
        rd: int,
        rm1: int,
        rm2: int,
        rm3: int,
    ) -> Map<GPR, BV32> {
        map_set(
            map_set(
                map_set(
                    cpu.general_regs,
                    rm1,
                    get_mem_addr(get_special_reg(rd, cpu), cpu.mem)
                ),
                rm2,
                get_mem_addr(bv_add(get_special_reg(rd, cpu), bv32(0x4)), cpu.mem)
            ),
            rm3,
            get_mem_addr(bv_add(get_special_reg(rd, cpu), bv32(0x8)), cpu.mem)
        )
    }

The only difference between these two is get_special_reg and get_gpr. Here is the definition for both:

fn get_gpr(reg: int, cpu: Armv7m) -> BV32 {
    map_get(cpu.general_regs, reg)
}  

fn get_control(control: Control) -> BV32 {
    if control.npriv && control.spsel {
        bv32(3)
    } else if control.npriv {
        // first bit is 1 - i.e. 01
        bv32(1)
    } else if control.spsel {
        // second bit is 1 - i.e. 10
        bv32(2)
    } else {
        bv32(0)
    }
}

fn get_sp(sp: SP, mode: int, control: Control) -> BV32 {
    if mode_is_handler(mode) || !control.spsel {
        sp.sp_main
    } else {
        sp.sp_process
    }
}

fn get_psp(sp: SP) -> BV32 {
    sp.sp_process
}

fn get_special_reg(reg: int, cpu: Armv7m) -> BV32 {
    if is_psp(reg) {
        get_psp(cpu.sp)
    } else if is_sp(reg) {
        get_sp(cpu.sp, cpu.mode, cpu.control)
    } else if is_lr(reg) {
        cpu.lr
    } else if is_pc(reg) {
        cpu.pc
    } else if is_control(reg) {
        get_control(cpu.control)
    } else if is_psr(reg) {
        cpu.psr
    } else {
        // ipsr
        bv_and(cpu.psr, bv32(0xff))
    }
}

I'm pretty convinced that the hang up is in get_special_reg. One thing I noticed looking at the constraints and spec etc. is that get_special_reg is unfolded multiple times in all the array updates. I'm not very knowledgeable in all things SMT solving but I'm wondering if this complex subexpression showing up many many times is slowing things down? Maybe the let (var expr) available in smtlib could help?

[vrindisbacher]

Diving a bit deeper, if I look at the spec for ldmia_w_special, the following expression (which is get_special_reg) is repeated 137 times in the simplified flux constraint.

(if rd.0 = 19 { old_cpu.1.1 } else { if rd.0 = 13 { if old_cpu.7.0 = 0 ∨ ¬old_cpu.2.1 { old_cpu.1.0 } else { old_cpu.1.1 } } else { if rd.0 = 14 { old_cpu.3 } else { if rd.0 = 15 { old_cpu.4 } else { if rd.0 = 16 { if old_cpu.2.0 ∧ old_cpu.2.1 { BV32 { bv_int_to_bv32(3) } } else { if old_cpu.2.0 { BV32 { bv_int_to_bv32(1) } } else { if old_cpu.2.1 { BV32 { bv_int_to_bv32(2) } } else { BV32 { bv_int_to_bv32(0) } } } } } else { if rd.0 = 17 { old_cpu.5 } else { BV32 { bv_and(old_cpu.5.0, bv_int_to_bv32(255)) } } } } } } }.0

And if I look at the SMT query, I see it 210 times.

(if (= reftgen$rd$2 19) (tuple2$1 (tuple8$1 reftgen$old_cpu$1)) (if (= reftgen$rd$2 13) (if (or (= (tuple8$7 reftgen$old_cpu$1) 0) (not (tuple2$1 (tuple8$2 reftgen$old_cpu$1)))) (tuple2$0 (tuple8$1 reftgen$old_cpu$1)) (tuple2$1 (tuple8$1 reftgen$old_cpu$1))) (if (= reftgen$rd$2 14) (tuple8$3 reftgen$old_cpu$1) (if (= reftgen$rd$2 15) (tuple8$4 reftgen$old_cpu$1) (if (= reftgen$rd$2 16) (if (and (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (tuple2$1 (tuple8$2 reftgen$old_cpu$1))) (int_to_bv32 3) (if (tuple2$0 (tuple8$2 reftgen$old_cpu$1)) (int_to_bv32 1) (if (tuple2$1 (tuple8$2 reftgen$old_cpu$1)) (int_to_bv32 2) (int_to_bv32 0)))) (if (= reftgen$rd$2 17) (tuple8$5 reftgen$old_cpu$1) (bvand (tuple8$5 reftgen$old_cpu$1) (int_to_bv32 255))))))))

I'm not sure if this is relevant - but it seems like it may be something to poke at?

[vrindisbacher]

I'm now thinking that this might not matter: Z3Prover/z3#6732

"within z3, there are no "let" term constructors. Let expressions are expanded. The reason why this works is that terms within z3 use shared pointers. So you can write let x = y + y let z = x + x in let u = z + z in u and the term named u has only 5 subterms.
If you write u out directly you have:
u := ((y + y) + (y + y)) + ((y + y) + (y + y))
But the subterm y + y will be represented by a pointer. The pointer is reused everywhere.
Similarly, the sub-term x + x is also a pointer. The pointer is reused twice, and within the pointer for x + x, the pointer into y + y is used twice."