# Atomic read-modify-writes (tests/gold/atomics.c, clang 18 -O2 -g): each renders as the helper
# wrapping its C11 builtin at the ordering the machine states. AArch64's LSE forms take their
# acquire and release marks (ldadd relaxed, ldseta acquire, ldclrl release, ldaddal, swpal and
# casal acq_rel); x86's LOCK is seq_cst whatever the source asked, and its lock cmpxchg retry
# loops carry the value a failed exchange read back to the next pass.

NAME=aarch64 lse fetch operations
FILE=tests/fixtures/atomics_clang_aarch64_O2g
CMDS=<<EOF
pdd @ sym.counter_next
pdd @ sym.total_add
pdd @ sym.flags_set
pdd @ sym.flags_clear
pdd @ sym.slot_swap
pdd @ sym.reference_release
EOF
EXPECT=<<EOF
uint32_t counter_next(uint32_t* counter)
{
    uint32_t tmp_40062c_0_1;

    /* r2dec proof: no individual construct is marked; 7 source obligations: 7 rendered, 0 elided, 0 refused; 2 statements rendered */
    {
        tmp_40062c_0_1 = r2sleigh_atomic_fetch_add_u32_relaxed((void*)(uint64_t)counter, (uint32_t)1U);
        return (uint32_t)tmp_40062c_0_1;
    }
}

void total_add(uint64_t* total, uint64_t amount)
{
    /* r2dec proof: no individual construct is marked; 5 source obligations: 5 rendered, 0 elided, 0 refused; 2 statements rendered */
    {
        r2sleigh_atomic_fetch_add_u64_relaxed((void*)(uint64_t)total, (uint64_t)amount);
        return;
    }
}

uint32_t flags_set(uint32_t* flags, uint32_t bits)
{
    uint32_t tmp_400644_0_1;

    /* r2dec proof: no individual construct is marked; 7 source obligations: 7 rendered, 0 elided, 0 refused; 2 statements rendered */
    {
        tmp_400644_0_1 = r2sleigh_atomic_fetch_or_u32_acquire((void*)(uint64_t)flags, (uint32_t)bits);
        return (uint32_t)tmp_400644_0_1;
    }
}

uint32_t flags_clear(uint32_t* flags, uint32_t bits)
{
    uint32_t tmp_40064c_4_1;

    /* r2dec proof: no individual construct is marked; 8 source obligations: 8 rendered, 0 elided, 0 refused; 2 statements rendered */
    {
        tmp_40064c_4_1 = r2sleigh_atomic_fetch_and_u32_release((void*)(uint64_t)flags, (uint32_t)~(uint32_t)bits);
        return (uint32_t)tmp_40064c_4_1;
    }
}

uint8_t slot_swap(uint8_t* slot, uint8_t value)
{
    uint8_t tmp_40065c_5_1;

    /* r2dec proof: no individual construct is marked; 7 source obligations: 7 rendered, 0 elided, 0 refused; 2 statements rendered */
    {
        tmp_40065c_5_1 = r2sleigh_atomic_exchange_u8_acq_rel((void*)(uint64_t)slot, (uint8_t)value);
        return (uint8_t)tmp_40065c_5_1;
    }
}

int32_t reference_release(int32_t* count)
{
    uint32_t tmp_40068c_0_1;

    /* r2dec proof: no individual construct is marked; 9 source obligations: 9 rendered, 0 elided, 0 refused; 2 statements rendered */
    {
        tmp_40068c_0_1 = r2sleigh_atomic_fetch_add_u32_acq_rel((void*)(uint64_t)count, (uint32_t)0xffffffffU);
        return (int32_t)(uint8_t)((uint32_t)tmp_40068c_0_1 == (uint32_t)1U);
    }
}

EOF
RUN

NAME=aarch64 cas
FILE=tests/fixtures/atomics_clang_aarch64_O2g
CMDS=<<EOF
pdd @ sym.lock_try
pdd @ sym.cell_exchange
EOF
EXPECT=<<EOF
int32_t lock_try(int32_t* lock)
{
    uint32_t tmp_40066c_8_1;

    /* r2dec proof: no individual construct is marked; 9 source obligations: 9 rendered, 0 elided, 0 refused; 2 statements rendered */
    {
        tmp_40066c_8_1 = r2sleigh_atomic_compare_exchange_u32_acquire((void*)(uint64_t)lock, (uint32_t)0U, (uint32_t)1U);
        return (int32_t)(uint8_t)((uint32_t)tmp_40066c_8_1 == (uint32_t)0U);
    }
}

uint64_t cell_exchange(uint64_t* cell, uint64_t expected, uint64_t desired)
{
    uint64_t tmp_40067c_10_1;

    /* r2dec proof: no individual construct is marked; 8 source obligations: 8 rendered, 0 elided, 0 refused; 2 statements rendered */
    {
        tmp_40067c_10_1 = r2sleigh_atomic_compare_exchange_u64_acq_rel((void*)(uint64_t)cell, (uint64_t)expected, (uint64_t)desired);
        return (uint64_t)tmp_40067c_10_1;
    }
}

EOF
RUN

NAME=x86-64 locked operations
FILE=tests/fixtures/atomics_clang_x86_64_O2g
CMDS=<<EOF
pdd @ sym.counter_next
pdd @ sym.total_add
pdd @ sym.flags_set
pdd @ sym.flags_clear
pdd @ sym.parity_toggle
pdd @ sym.slot_swap
pdd @ sym.lock_try
pdd @ sym.reference_release
EOF
EXPECT=<<EOF
uint32_t counter_next(uint32_t* counter)
{
    uint32_t tmp_401115_0_1;

    /* r2dec proof: no individual construct is marked; 10 source obligations: 7 rendered, 3 elided, 0 refused; 2 statements rendered */
    {
        tmp_401115_0_1 = r2sleigh_atomic_fetch_add_u32_seq_cst((void*)(uint64_t)counter, (uint32_t)1U);
        return (uint32_t)tmp_401115_0_1;
    }
}

void total_add(uint64_t* total, uint64_t amount)
{
    /* r2dec proof: no individual construct is marked; 8 source obligations: 5 rendered, 3 elided, 0 refused; 2 statements rendered */
    {
        r2sleigh_atomic_fetch_add_u64_seq_cst((void*)(uint64_t)total, (uint64_t)amount);
        return;
    }
}

uint32_t flags_set(uint32_t* flags, uint32_t bits)
{
    uint32_t tmp_401140_0_1;
    uint64_t rax_2;
    uint32_t tmp_lane_401154_1_0_1;
    uint32_t tmp_401154_4_1;
    uint8_t zf_2;
    uint64_t rax_4;

    /* r2dec proof: no individual construct is marked; 28 source obligations: 25 rendered, 3 elided, 0 refused; 9 statements rendered */
    {
        tmp_401140_0_1 = r2sleigh_load_u32((void*)(uint64_t)flags);
        rax_2 = (uint64_t)(uint32_t)tmp_401140_0_1;
        do {
            tmp_lane_401154_1_0_1 = (uint32_t)((uint64_t)rax_2 >> 0U);
            tmp_401154_4_1 = r2sleigh_atomic_compare_exchange_u32_seq_cst((void*)(uint64_t)flags, (uint32_t)tmp_lane_401154_1_0_1, (uint32_t)((uint32_t)((uint64_t)rax_2 >> 0U) | (uint32_t)bits));
            zf_2 = (uint8_t)((uint32_t)tmp_lane_401154_1_0_1 == (uint32_t)tmp_401154_4_1);
            rax_4 = zf_2 ? (uint64_t)((uint64_t)(uint32_t)((uint64_t)rax_2 >> 32U) << 32U | (uint64_t)(zf_2 ? (uint32_t)tmp_lane_401154_1_0_1 : (uint32_t)tmp_401154_4_1)) : (uint64_t)(uint32_t)tmp_401154_4_1;
            rax_2 = rax_4;
        } while ((uint8_t)((uint32_t)zf_2 ^ (uint32_t)(uint8_t)1U));
        {
            return (uint32_t)rax_4;
        }
    }
}

uint32_t flags_clear(uint32_t* flags, uint32_t bits)
{
    uint32_t tmp_lane_401160_0_1_1;
    uint32_t tmp_401162_0_1;
    uint64_t rax_2;
    uint32_t tmp_lane_401174_1_0_1;
    uint32_t tmp_401174_4_1;
    uint8_t zf_2;
    uint64_t rax_4;

    /* r2dec proof: no individual construct is marked; 29 source obligations: 26 rendered, 3 elided, 0 refused; 10 statements rendered */
    {
        tmp_lane_401160_0_1_1 = (uint32_t)~(uint32_t)bits;
        tmp_401162_0_1 = r2sleigh_load_u32((void*)(uint64_t)flags);
        rax_2 = (uint64_t)(uint32_t)tmp_401162_0_1;
        do {
            tmp_lane_401174_1_0_1 = (uint32_t)((uint64_t)rax_2 >> 0U);
            tmp_401174_4_1 = r2sleigh_atomic_compare_exchange_u32_seq_cst((void*)(uint64_t)flags, (uint32_t)tmp_lane_401174_1_0_1, (uint32_t)((uint32_t)((uint64_t)rax_2 >> 0U) & (uint32_t)tmp_lane_401160_0_1_1));
            zf_2 = (uint8_t)((uint32_t)tmp_lane_401174_1_0_1 == (uint32_t)tmp_401174_4_1);
            rax_4 = zf_2 ? (uint64_t)((uint64_t)(uint32_t)((uint64_t)rax_2 >> 32U) << 32U | (uint64_t)(zf_2 ? (uint32_t)tmp_lane_401174_1_0_1 : (uint32_t)tmp_401174_4_1)) : (uint64_t)(uint32_t)tmp_401174_4_1;
            rax_2 = rax_4;
        } while ((uint8_t)((uint32_t)zf_2 ^ (uint32_t)(uint8_t)1U));
        {
            return (uint32_t)rax_4;
        }
    }
}

uint16_t parity_toggle(uint16_t* word, uint16_t mask)
{
    uint64_t rsi_1;
    uint16_t tmp_401180_0_1;
    uint64_t rax_2;
    uint16_t tmp_lane_401194_1_0_1;
    uint16_t tmp_401194_2_1;
    uint8_t zf_2;
    uint16_t tmp_lane_401194_11_0_1;

    /* r2dec proof: no individual construct is marked; 30 source obligations: 27 rendered, 3 elided, 0 refused; 10 statements rendered */
    {
        rsi_1 = (uint64_t)(uint16_t)mask;
        tmp_401180_0_1 = r2sleigh_load_u16((void*)(uint64_t)word);
        rax_2 = (uint64_t)(uint16_t)tmp_401180_0_1;
        do {
            tmp_lane_401194_1_0_1 = (uint16_t)((uint64_t)rax_2 >> 0U);
            tmp_401194_2_1 = r2sleigh_atomic_compare_exchange_u16_seq_cst((void*)(uint64_t)word, (uint16_t)tmp_lane_401194_1_0_1, (uint16_t)((uint32_t)((uint32_t)((uint64_t)rax_2 >> 0U) ^ (uint32_t)((uint64_t)rsi_1 >> 0U)) >> 0U));
            zf_2 = (uint8_t)((uint16_t)tmp_lane_401194_1_0_1 == (uint16_t)tmp_401194_2_1);
            tmp_lane_401194_11_0_1 = zf_2 ? (uint16_t)tmp_lane_401194_1_0_1 : (uint16_t)tmp_401194_2_1;
            rax_2 = (uint64_t)(((uint64_t)rax_2 & (uint64_t)0xffffffffffff0000U) | ((uint64_t)tmp_lane_401194_11_0_1 & (uint64_t)0xffffU) << 0U);
        } while ((uint8_t)((uint32_t)zf_2 ^ (uint32_t)(uint8_t)1U));
        {
            return (uint16_t)tmp_lane_401194_11_0_1;
        }
    }
}

uint8_t slot_swap(uint8_t* slot, uint8_t value)
{
    uint8_t tmp_4011a2_1_1;

    /* r2dec proof: no individual construct is marked; 10 source obligations: 7 rendered, 3 elided, 0 refused; 2 statements rendered */
    {
        tmp_4011a2_1_1 = r2sleigh_atomic_exchange_u8_seq_cst((void*)(uint64_t)slot, (uint8_t)value);
        return (uint8_t)tmp_4011a2_1_1;
    }
}

int32_t lock_try(int32_t* lock)
{
    uint32_t tmp_4011b9_4_1;

    /* r2dec proof: no individual construct is marked; 15 source obligations: 12 rendered, 3 elided, 0 refused; 2 statements rendered */
    {
        tmp_4011b9_4_1 = r2sleigh_atomic_compare_exchange_u32_seq_cst((void*)(uint64_t)lock, (uint32_t)0U, (uint32_t)1U);
        return (int32_t)((uint64_t)(uint8_t)((uint32_t)((uint32_t)0U - (uint32_t)tmp_4011b9_4_1) == (uint32_t)0U) >> 0U);
    }
}

int32_t reference_release(int32_t* count)
{
    uint32_t tmp_4011e2_0_1;

    /* r2dec proof: no individual construct is marked; 14 source obligations: 11 rendered, 3 elided, 0 refused; 2 statements rendered */
    {
        tmp_4011e2_0_1 = r2sleigh_atomic_fetch_sub_u32_seq_cst((void*)(uint64_t)count, (uint32_t)1U);
        return (int32_t)(uint8_t)((uint32_t)tmp_4011e2_0_1 == (uint32_t)1U);
    }
}

EOF
RUN
