Mergen/docs/semantic_reports/vm_countdown_loop_report.md

vm_countdown_loop - original vs lifted equivalence

• Verdict: PASS
• Cases: 8/8 equivalent
• Source: testcases/rewrite_smoke/vm_countdown_loop.c
• Lifted IR: rewrite-regression-work/ir_outputs/vm_countdown_loop.ll
• Symbol: vm_countdown_loop_target
• Native driver: rewrite-regression-work/eq/vm_countdown_loop_eq.exe
• Lifted signature: define i64 @main(i64 %RAX, i64 %RCX, i64 %RDX, i64 %RBX, i64 %RSP, i64 %RBP, i64 %RSI, i64 %RDI, i64 %R8, i64 %R9, i64 %R10, i64 %R11, i64 %R12, i64 %R13, i64 %R14, i64 %R15, ptr nocapture readnone %EIP, ptr nocapture readnone %memory, i128 %XMM0, i128 %XMM1, i128 %XMM2, i128 %XMM3, i128 %XMM4, i128 %XMM5, i128 %XMM6, i128 %XMM7, i128 %XMM8, i128 %XMM9, i128 %XMM10, i128 %XMM11, i128 %XMM12, i128 %XMM13, i128 %XMM14, i128 %XMM15) local_unnamed_addr #0

Equivalence (native vs lifted)

Each row runs the same inputs through (a) the original program compiled to a real Win64 binary that calls vm_countdown_loop_target directly, and (b) the lifted+optimized LLVM IR executed via lli. A case is equivalent only if both observations agree and also match the manifest's expected value.

#	Inputs	Manifest	Native	Lifted	Equivalent	Label
1	RCX=0	0	0	0	yes	count=0: empty sum
2	RCX=1	1	1	1	yes	count=1: T(1)
3	RCX=2	3	3	3	yes	count=2: T(2)
4	RCX=5	15	15	15	yes	count=5: T(5)
5	RCX=10	55	55	55	yes	count=10: T(10)
6	RCX=15	120	120	120	yes	count=15: T(15)
7	RCX=16	0	0	0	yes	count=0 again (mask drops bit 4)
8	RCX=255	120	120	120	yes	count=15 again after mask

Source

/* PC-state VM with a reverse-induction counted loop.
 * Lift target: vm_countdown_loop_target.
 * Goal: exercise loop detection for a loop whose induction variable *decreases*
 * and whose bound is a symbolic countdown rather than a rising compare.
 * Computes the triangular number sum(1..n) where n = x & 0xF, but builds it
 * by counting down from n to 1 instead of up.
 */
#include <stdio.h>

enum CdVmPc {
    CD_INIT       = 0,
    CD_LOAD_COUNT = 1,
    CD_INIT_SUM   = 2,
    CD_CHECK      = 3,
    CD_BODY_ADD   = 4,
    CD_BODY_DEC   = 5,
    CD_HALT       = 6,
};

__declspec(noinline)
int vm_countdown_loop_target(int x) {
    int count = 0;
    int sum   = 0;
    int pc    = CD_INIT;

    while (1) {
        if (pc == CD_INIT) {
            pc = CD_LOAD_COUNT;
        } else if (pc == CD_LOAD_COUNT) {
            count = x & 0xF;
            pc = CD_INIT_SUM;
        } else if (pc == CD_INIT_SUM) {
            sum = 0;
            pc = CD_CHECK;
        } else if (pc == CD_CHECK) {
            pc = (count > 0) ? CD_BODY_ADD : CD_HALT;
        } else if (pc == CD_BODY_ADD) {
            sum = sum + count;
            pc = CD_BODY_DEC;
        } else if (pc == CD_BODY_DEC) {
            count = count - 1;
            pc = CD_CHECK;
        } else if (pc == CD_HALT) {
            return sum;
        } else {
            return -1;
        }
    }
}

int main(void) {
    printf("vm_countdown_loop(10)=%d vm_countdown_loop(15)=%d\n",
           vm_countdown_loop_target(10), vm_countdown_loop_target(15));
    return 0;
}