Skip to content

MSVC gte_mask optimized SSE path is disabled (and the disabled code is buggy) #728

Description

@protz

File: krmllib/c/fstar_uint128_msvc.h:362

The && 0 permanently disables the SSE path. The disabled code uses _mm_cmpgt_epi32 which performs signed 32-bit comparison -- incorrect for unsigned 128-bit integers. If someone removes && 0, the bug returns.

// CURRENT:
#if HAS_OPTIMIZED && 0   // permanently disabled -- looks like a debug leftover

Test snippet: (demonstrates the signed comparison bug if the path were enabled)

#include <emmintrin.h>
#include <stdio.h>
int main(void) {
    // 0x80000001 > 0x7FFFFFFF as unsigned, but < as signed
    __m128i a = _mm_set_epi32(0, 0, 0, 0x80000001);
    __m128i b = _mm_set_epi32(0, 0, 0, 0x7FFFFFFF);
    __m128i gt = _mm_cmpgt_epi32(a, b);
    int mask = _mm_movemask_epi8(gt);
    printf("signed cmpgt mask: 0x%x (expect 0xF for unsigned gt, got 0x0)\n", mask);
    return 0;
}

Suggested fix: Add a comment explaining why it's disabled:

#if 0 /* Disabled: _mm_cmpgt_epi32 performs SIGNED comparison, which is
       * incorrect for unsigned 128-bit integers. The scalar fallback below
       * using FStar_UInt64_gte_mask is correct. */

This issue was found by Claude (Opus 4.6)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions