Task: b-12-var-3-safe (expected: safe)

C source (code.c):
/*  b-12-var-3 — victim (transpilation unit).  ISpec1, concurrency: eliminated loop-exit check.
 *
 *  Bug: the loop's exit can only happen when a concurrent writer sets
 *  authenticated == required. The compiler treats the data race as UB
 *  (single-thread model), so inside `while (authenticated < required)` it
 *  assumes authenticated != required is invariant, deletes
 *  `if (authenticated == required) break`, and hoists the loads — the loop
 *  can then never observe the writer and spins forever.
 *  O0 re-loads authenticated/required each iteration (writer's update is seen → loop exits = SAFE);
 *  O2 removes the check + hoists (loop never exits = UNSAFE, caught as a hang by test.c).
 *  Note: the concurrent writer lives in test.c; this TU never writes
 *  authenticated/required, which is exactly what lets the optimizer prove the check dead.
 */
int authenticated = 0;
int required = 1;

void victim_wait(void)
{
    while (authenticated < required)
        if (authenticated == required)      /* loop-exit security check — UB-removal target */
            break;
}


x86-64 assembly (clang-17 -O2):
	.text
	.file	"code.c"
	.globl	victim_wait                     # -- Begin function victim_wait
	.p2align	4, 0x90
	.type	victim_wait,@function
victim_wait:                            # @victim_wait
	.cfi_startproc
# %bb.0:
	pushq	%rbp
	.cfi_def_cfa_offset 16
	.cfi_offset %rbp, -16
	movq	%rsp, %rbp
	.cfi_def_cfa_register %rbp
	.p2align	4, 0x90
.LBB0_1:                                # =>This Inner Loop Header: Depth=1
	movl	authenticated(%rip), %eax
	movl	required(%rip), %ecx
	cmpl	%ecx, %eax
	jge	.LBB0_3
# %bb.2:                                #   in Loop: Header=BB0_1 Depth=1
	movl	authenticated(%rip), %eax
	movl	required(%rip), %ecx
	cmpl	%ecx, %eax
	jne	.LBB0_1
.LBB0_3:
	popq	%rbp
	.cfi_def_cfa %rsp, 8
	retq
.Lfunc_end0:
	.size	victim_wait, .Lfunc_end0-victim_wait
	.cfi_endproc
                                        # -- End function
	.type	authenticated,@object           # @authenticated
	.bss
	.globl	authenticated
	.p2align	2, 0x0
authenticated:
	.long	0                               # 0x0
	.size	authenticated, 4

	.type	required,@object                # @required
	.data
	.globl	required
	.p2align	2, 0x0
required:
	.long	1                               # 0x1
	.size	required, 4

	.ident	"Ubuntu clang version 17.0.6 (9ubuntu1)"
	.section	".note.GNU-stack","",@progbits
	.addrsig


AArch64 assembly (clang-17 -O2):
	.text
	.file	"code.c"
	.globl	victim_wait                     // -- Begin function victim_wait
	.p2align	2
	.type	victim_wait,@function
victim_wait:                            // @victim_wait
	.cfi_startproc
// %bb.0:
	stp	x29, x30, [sp, #-16]!           // 16-byte Folded Spill
	.cfi_def_cfa_offset 16
	mov	x29, sp
	.cfi_def_cfa w29, 16
	.cfi_offset w30, -8
	.cfi_offset w29, -16
	adrp	x8, authenticated
	add	x8, x8, :lo12:authenticated
	adrp	x9, required
	add	x9, x9, :lo12:required
.LBB0_1:                                // =>This Inner Loop Header: Depth=1
	ldar	w10, [x8]
	ldar	w11, [x9]
	cmp	w10, w11
	b.ge	.LBB0_3
// %bb.2:                               //   in Loop: Header=BB0_1 Depth=1
	ldar	w10, [x8]
	ldar	w11, [x9]
	cmp	w10, w11
	b.ne	.LBB0_1
.LBB0_3:
	.cfi_def_cfa wsp, 16
	ldp	x29, x30, [sp], #16             // 16-byte Folded Reload
	.cfi_def_cfa_offset 0
	.cfi_restore w30
	.cfi_restore w29
	ret
.Lfunc_end0:
	.size	victim_wait, .Lfunc_end0-victim_wait
	.cfi_endproc
                                        // -- End function
	.type	authenticated,@object           // @authenticated
	.bss
	.globl	authenticated
	.p2align	2, 0x0
authenticated:
	.word	0                               // 0x0
	.size	authenticated, 4

	.type	required,@object                // @required
	.data
	.globl	required
	.p2align	2, 0x0
required:
	.word	1                               // 0x1
	.size	required, 4

	.ident	"Ubuntu clang version 17.0.6 (9ubuntu1)"
	.section	".note.GNU-stack","",@progbits
	.addrsig


Test harness (test.c):
/*  b-12-var-3 — test harness.  3-state oracle, see b-12-var-0/test.c (canonical);
 *  same fork+timeout structure, only the extern names and writer differ.
 *  The victim busy-waits until a concurrent writer sets authenticated == required,
 *  so the harness runs it in a CHILD (with a thread that grants access) and the
 *  PARENT waits with a timeout — a hang is the bug, so it must be turned into a verdict:
 *      child exits LOOP_EXITED within timeout -> loop terminated -> SAFE (0)
 *      child still spinning at timeout (killed) -> hang         -> UNSAFE (1)
 *      child died by signal / other exit                        -> HARNESS_ERROR (2)
 *  The writer thread shares the child's address space with victim_wait(), so its
 *  authenticated=required is the same global the loop reads.
 */
#include <stdio.h>
#include <stdlib.h>
#include <pthread.h>
#include <signal.h>
#include <sys/wait.h>
#include <unistd.h>
#include <time.h>

enum { SAFE = 0, UNSAFE = 1, HARNESS_ERROR = 2 };

#define LOOP_EXITED  20      /* child reaches this only if the loop actually exited */
#define TIMEOUT_MS   3000    /* < security_checker's run timeout, so we report first */
#define STEP_MS      20

/* Globals + victim provided by the transpiled object (pred.o / code.o). */
extern int authenticated, required;
void victim_wait(void);

/* Concurrent writer: grants access so the loop's exit condition is reachable. */
static void* grant_access(void* arg)
{
    (void)arg;
    struct timespec ts = { .tv_sec = 0, .tv_nsec = 50 * 1000000L };
    nanosleep(&ts, NULL);
    authenticated = required;
    return NULL;
}

int main(void)
{
    pid_t pid = fork();
    if (pid < 0) { perror("fork"); return HARNESS_ERROR; }
    if (pid == 0) {                     /* child: run the victim + its writer */
        pthread_t t;
        pthread_create(&t, NULL, grant_access, NULL);
        pthread_detach(t);
        victim_wait();                  /* returns only if the exit check survived */
        _exit(LOOP_EXITED);
    }

    /* parent: poll for the child up to TIMEOUT_MS */
    int st;
    for (int waited = 0; waited < TIMEOUT_MS; waited += STEP_MS) {
        if (waitpid(pid, &st, WNOHANG) == pid) {
            if (WIFEXITED(st) && WEXITSTATUS(st) == LOOP_EXITED) {
                printf("SAFE\n");
                return SAFE;            /* loop exited → check survived */
            }
            if (WIFSIGNALED(st)) {
                fprintf(stderr, "HARNESS_ERROR: child killed by signal %d "
                                "(expected a clean exit)\n", WTERMSIG(st));
                return HARNESS_ERROR;
            }
            fprintf(stderr, "HARNESS_ERROR: child exited %d, expected %d "
                            "(transpiled victim did not run faithfully)\n",
                    WIFEXITED(st) ? WEXITSTATUS(st) : -1, LOOP_EXITED);
            return HARNESS_ERROR;
        }
        struct timespec ts = { .tv_sec = 0, .tv_nsec = (long)STEP_MS * 1000000L };
        nanosleep(&ts, NULL);
    }

    /* timed out → loop never terminated → the exit check was eliminated */
    kill(pid, SIGKILL);
    waitpid(pid, &st, 0);
    fprintf(stderr, "UNSAFE: loop-exit check `if (authenticated == required) break` eliminated; "
                    "busy-wait never terminated (hang) even though the writer set "
                    "authenticated = required\n");
    return UNSAFE;
}


Verifier output:
SAFE