# One function at each tier. A lowering change moves exactly one of these; read the new output and
# judge it before blessing it.

NAME=fnv1a32 low IL
FILE=tests/coverage/pinned/hashes_gcc_x64_O2
CMDS=s 0x401330; pdil
EXPECT=<<EOF
Entry: 0x401330
Blocks: 5

Block 0x401330 (9 bytes, 10 ops)
    0: CF = COPY 0x0:1
    1: OF = COPY 0x0:1
    2: uniq:0x0[8] = RSI & RSI
    3: SF = uniq:0x0[8] s< 0x0:8
    4: ZF = uniq:0x0[8] == 0x0:8
    5: uniq:0x8[8] = uniq:0x0[8] & 0xff:8
    6: uniq:0x10[1] = POPCOUNT(uniq:0x8[8])
    7: uniq:0x11[1] = uniq:0x10[1] & 0x1:1
    8: PF = uniq:0x11[1] == 0x0:1
    9: CBRANCH ram:0x401360[8] if ZF
  -> 0x401360 (Direct)
  -> 0x401339 (Fallthrough)

Block 0x401339 (15 bytes, 14 ops)
    0: CF = CARRY(RSI, RDI)
    1: OF = SCARRY(RSI, RDI)
    2: uniq:0x0[8] = RSI & 0xf:8
    3: uniq:0x8[8] = RDI & 0xf:8
    4: uniq:0x10[8] = uniq:0x0[8] + uniq:0x8[8]
    5: AF = 0xf:8 < uniq:0x10[8]
    6: RSI = RSI + RDI
    7: SF = RSI s< 0x0:8
    8: ZF = RSI == 0x0:8
    9: uniq:0x18[8] = RSI & 0xff:8
   10: uniq:0x20[1] = POPCOUNT(uniq:0x18[8])
   11: uniq:0x21[1] = uniq:0x20[1] & 0x1:1
   12: PF = uniq:0x21[1] == 0x0:1
   13: RAX = COPY 0x811c9dc5:8
  -> 0x401348 (Fallthrough)

Block 0x401348 (20 bytes, 50 ops)
    0: uniq:0x0[1] = LOAD [ram]RDI
    1: EDX = ZEXT(uniq:0x0[1])
    2: RDX = ZEXT(EDX)
    3: CF = CARRY(RDI, 0x1:8)
    4: OF = SCARRY(RDI, 0x1:8)
    5: uniq:0x0[8] = RDI & 0xf:8
    6: uniq:0x8[8] = 0x1:8 & 0xf:8
    7: uniq:0x10[8] = uniq:0x0[8] + uniq:0x8[8]
    8: AF = 0xf:8 < uniq:0x10[8]
    9: RDI = RDI + 0x1:8
   10: SF = RDI s< 0x0:8
   11: ZF = RDI == 0x0:8
   12: uniq:0x18[8] = RDI & 0xff:8
   13: uniq:0x20[1] = POPCOUNT(uniq:0x18[8])
   14: uniq:0x21[1] = uniq:0x20[1] & 0x1:1
   15: PF = uniq:0x21[1] == 0x0:1
   16: CF = COPY 0x0:1
   17: OF = COPY 0x0:1
   18: EAX = EAX ^ EDX
   19: RAX = ZEXT(EAX)
   20: SF = EAX s< 0x0:4
   21: ZF = EAX == 0x0:4
   22: uniq:0x0[4] = EAX & 0xff:4
   23: uniq:0x4[1] = POPCOUNT(uniq:0x0[4])
   24: uniq:0x5[1] = uniq:0x4[1] & 0x1:1
   25: PF = uniq:0x5[1] == 0x0:1
   26: uniq:0x0[8] = SEXT(EAX)
   27: uniq:0x8[8] = SEXT(0x1000193:4)
   28: uniq:0x10[8] = uniq:0x0[8] * uniq:0x8[8]
   29: EAX = SUBPIECE(uniq:0x10[8], 0)
   30: uniq:0x18[4] = SUBPIECE(uniq:0x10[8], 4)
   31: uniq:0x1c[8] = SEXT(EAX)
   32: CF = uniq:0x1c[8] != uniq:0x10[8]
   33: OF = COPY CF
   34: RAX = ZEXT(EAX)
   35: uniq:0x0[8] = COPY RSI
   36: CF = uniq:0x0[8] < RDI
   37: OF = SBORROW(uniq:0x0[8], RDI)
   38: uniq:0x8[8] = uniq:0x0[8] & 0xf:8
   39: uniq:0x10[8] = RDI & 0xf:8
   40: AF = uniq:0x8[8] < uniq:0x10[8]
   41: uniq:0x18[8] = uniq:0x0[8] - RDI
   42: SF = uniq:0x18[8] s< 0x0:8
   43: ZF = uniq:0x18[8] == 0x0:8
   44: uniq:0x20[8] = uniq:0x18[8] & 0xff:8
   45: uniq:0x28[1] = POPCOUNT(uniq:0x20[8])
   46: uniq:0x29[1] = uniq:0x28[1] & 0x1:1
   47: PF = uniq:0x29[1] == 0x0:1
   48: uniq:0x0[1] = !ZF
   49: CBRANCH ram:0x401348[8] if uniq:0x0[1]
  -> 0x401348 (Direct)
  -> 0x40135c (Fallthrough)

Block 0x40135c (1 bytes, 3 ops)
    0: RIP = LOAD [ram]RSP
    1: RSP = RSP + 0x8:8
    2: RETURN RIP

Block 0x401360 (6 bytes, 4 ops)
    0: RAX = COPY 0x811c9dc5:8
    1: RIP = LOAD [ram]RSP
    2: RSP = RSP + 0x8:8
    3: RETURN RIP

EOF
RUN

NAME=fnv1a32 C
FILE=tests/coverage/pinned/hashes_gcc_x64_O2
CMDS=s 0x401330; pdd
EXPECT=<<EOF
uint64_t fnv1a32(uint64_t arg0, uint64_t arg1)
{
    uint64_t rsi_1;
    uint64_t rax_2;
    uint64_t rdi_1;
    uint8_t tmp_401348_0_1;
    uint64_t rdi_2;
    uint64_t rax_4;

    /* r2dec proof: no individual construct is marked; 40 source obligations: 32 rendered, 8 elided, 0 refused; 12 statements rendered */
    {
        if ((uint8_t)((uint64_t)arg1 == (uint64_t)0U)) {
            return (uint64_t)0x811c9dc5U;
        } else {
            rsi_1 = (uint64_t)((uint64_t)arg1 + (uint64_t)arg0);
            rax_2 = (uint64_t)0x811c9dc5U;
            rdi_1 = arg0;
            do {
                tmp_401348_0_1 = r2sleigh_load_u8((void*)rdi_1);
                rdi_2 = (uint64_t)((uint64_t)rdi_1 + (uint64_t)1U);
                rax_4 = (uint64_t)(uint32_t)((uint64_t)((uint64_t)(int32_t)((uint32_t)(uint8_t)tmp_401348_0_1 ^ (uint32_t)((uint64_t)rax_2 >> 0U)) * (uint64_t)0x1000193U) >> 0U);
                rax_2 = rax_4;
                rdi_1 = rdi_2;
            } while ((uint8_t)((uint64_t)rsi_1 != (uint64_t)rdi_2));
            {
                return (uint64_t)rax_4;
            }
        }
    }
}

EOF
RUN

# A dispatch's arms are blocks of the low tier, as `afb` lists them.
NAME=switch low IL blocks
FILE=tests/coverage/pinned/hashes_gcc_x64_O2
CMDS=s 0x4018b0; pdil~Block
EXPECT=<<EOF
Blocks: 12
Block 0x4018b0 (81 bytes, 120 ops)
Block 0x401901 (7 bytes, 0 ops)
Block 0x401908 (114 bytes, 500 ops)
Block 0x40197a (13 bytes, 14 ops)
Block 0x401990 (12 bytes, 54 ops)
Block 0x40199c (12 bytes, 54 ops)
Block 0x4019a8 (12 bytes, 54 ops)
Block 0x4019b4 (12 bytes, 54 ops)
Block 0x4019c0 (12 bytes, 54 ops)
Block 0x4019cc (12 bytes, 54 ops)
Block 0x4019d8 (7 bytes, 12 ops)
Block 0x4019df (305 bytes, 1342 ops)
EOF
RUN
