picosat 965: deterministic Linux reproducer for the LLP64 pointer-rebase bug (long vs ptrdiff_t in enlarge)

driver.c

/* Mimic Resolver's usage: adjust(N) up front, build clauses, then grow the
   solver mid-population via inc_max_var (which is what set_trigger does). */
#include <stdio.h>
#include <stdlib.h>
#include "picosat.h"
int main(int argc, char **argv) {
    int N = argc > 1 ? atoi(argv[1]) : 11164;
    PicoSAT *ps = picosat_init();
    picosat_adjust(ps, N);
    for (int v = 1; v < N; v += 2) {          /* clauses over the adjusted range */
        picosat_add(ps, v); picosat_add(ps, -(v+1)); picosat_add(ps, 0);
    }
    /* grow a *populated* solver, repeatedly -- the Resolver pattern */
    for (int k = 0; k < 200; k++) {
        int t = picosat_inc_max_var(ps);
        picosat_add(ps, -t); picosat_add(ps, 1); picosat_add(ps, 0);
    }
    int r = picosat_sat(ps, -1);
    printf("solve result = %d (10=SAT 20=UNSAT)\n", r);
    picosat_reset(ps);
    printf("SURVIVED\n");
    return 0;
}

exp_trunc.diff

--- picosat-965/picosat.c	2016-01-13 07:19:13.000000000 +0000
+++ far_trunc/picosat.c	2026-08-17 14:00:51.962241732 +0000
@@ -959,6 +959,37 @@
   return 0;
 }
 
+
+/* ---- DIAGNOSTIC BUILD ONLY: far allocator ----------------------------------
+   Forces every (re)allocation to land 4GB past the previous one, so enlarge()'s
+   pointer rebase always sees a delta too large for a 32-bit long. This
+   reproduces the Windows x64 (LLP64) condition on Linux, where glibc's realloc
+   otherwise keeps blocks close together and the bug never fires. */
+#include <sys/mman.h>
+static char *far_next = (char *) 0x200000000000ULL;
+static size_t far_round (size_t n) { return (n + 0xFFF) & ~(size_t) 0xFFF; }
+static void *far_alloc (size_t bytes) {
+  size_t len = far_round (bytes);
+  void *q = mmap (far_next, len, PROT_READ | PROT_WRITE,
+                  MAP_PRIVATE | MAP_ANONYMOUS | MAP_NORESERVE, -1, 0);
+  if (q == MAP_FAILED) return 0;
+  far_next += 0x100000000ULL;
+  return q;
+}
+static void far_free (void *q, size_t bytes) {
+  if (q) munmap (q, far_round (bytes));
+}
+static void *far_realloc (void *q, size_t old_bytes, size_t new_bytes) {
+  void *r;
+  if (!new_bytes) { far_free (q, old_bytes); return 0; }
+  r = far_alloc (new_bytes);
+  if (!r) return 0;
+  if (q && old_bytes) memcpy (r, q, old_bytes < new_bytes ? old_bytes : new_bytes);
+  far_free (q, old_bytes);
+  return r;
+}
+/* -------------------------------------------------------------------------- */
+
 static void *
 new (PS * ps, size_t size)
 {
@@ -973,7 +1004,7 @@
   if (ps->enew)
     b = ps->enew (ps->emgr, bytes);
   else
-    b = malloc (bytes);
+    b = far_alloc (bytes);
 
   ABORTIF (!b, "out of memory in 'new'");
 #ifndef NDEBUG
@@ -1009,7 +1040,7 @@
   if (ps->edelete)
     ps->edelete (ps->emgr, b, bytes);
   else
-    free (b);
+    far_free (b, bytes);
 }
 
 static void *
@@ -1037,7 +1068,7 @@
   if (ps->eresize)
     b = ps->eresize (ps->emgr, b, old_bytes, new_bytes);
   else
-    b = realloc (b, new_bytes);
+    b = far_realloc (b, old_bytes, new_bytes);
 
   if (!new_size)
     {
@@ -2903,7 +2934,8 @@
 static void
 enlarge (PS * ps, unsigned new_size_vars)
 {
-  long rnks_delta, lits_delta;
+  int32_t rnks_delta, lits_delta;
+  ptrdiff_t real_lits_delta;
   Lit *old_lits = ps->lits;
   Rnk *old_rnks = ps->rnks;
 
@@ -2917,6 +2949,11 @@
   RESIZEN (ps->vars, ps->size_vars, new_size_vars);
   RESIZEN (ps->rnks, ps->size_vars, new_size_vars);
 
+  real_lits_delta = ps->lits - old_lits;
+  if (real_lits_delta != (ptrdiff_t)(int32_t) real_lits_delta)
+    fprintf (stderr, "PICOTRUNC max_var=%u real=%td as32=%d\n",
+             (unsigned) ps->max_var, real_lits_delta,
+             (int)(int32_t) real_lits_delta);
   if ((lits_delta = ps->lits - old_lits))
     {
       fix_trail_lits (ps, lits_delta);

REPRODUCER.md

Reproducing the picosat LLP64 pointer-rebase bug on Linux

enlarge() in picosat.c rebases every stored Lit*/Rnk* by the byte distance the arrays moved during realloc, holding that distance in a long. On LLP64 (Windows x64) long is 32 bits while pointers are 64, so a move of more than 2GB truncates and every rebased pointer is left wild.

The bug does not normally reproduce on Linux for two independent reasons, and you have to remove both to see it:

1. LP64 has a wide enough long. Simulate LLP64 by making only the delta variables int32_t, leaving pointers 64-bit. This is faithful: on LLP64 both the delta variable and the fix_* parameters are 32-bit, so truncating once at the assignment and sign-extending into the (64-bit) parameters gives the same arithmetic.
2. glibc's realloc keeps blocks close together, so the >2GB move never happens. Force it by routing picosat's three allocation primitives (new/delete/resize, all of which carry explicit sizes) through an mmap allocator that places each block 4GB past the previous one.

With both removed, the failure is deterministic: 6/6 crash with the truncating delta, 6/6 survive with ptrdiff_t. Same allocator, same workload, same compiler — the delta type is the only variable.

int32_t   delta: PICOTRUNC max_var=0     real=38654705664    as32=0
                 PICOTRUNC max_var=11164 real=24133421236224 as32=0
                 Segmentation fault (signal 11)

ptrdiff_t delta: same two truncations detected
                 solve result = 10 (SAT), SURVIVED

The max_var=0 truncation is harmless — it happens during picosat_adjust on an empty solver, where the fix-up loops have nothing to iterate. The fatal one is on a populated solver.

Usage

tar xzf picosat-965.tar.gz
cp -r picosat-965 far_trunc && (cd far_trunc && patch -p1 < ../exp_trunc.diff)
cp -r picosat-965 far_fixed && (cd far_fixed && patch -p1 < ../exp_trunc.diff \
    && sed -i 's/int32_t rnks_delta, lits_delta;/ptrdiff_t rnks_delta, lits_delta;/' picosat.c)
# build each as a shared lib, then:
gcc -O2 -Ipicosat-965 driver.c -o driver_trunc far_trunc/libpicosat.so -Wl,-rpath,far_trunc
gcc -O2 -Ipicosat-965 driver.c -o driver_fixed far_fixed/libpicosat.so -Wl,-rpath,far_fixed
./driver_trunc 11164   # segfaults
./driver_fixed 11164   # survives

NOTE: exp_trunc.diff is a diagnostic scaffold, not the proposed fix. The proposed fix is only long -> ptrdiff_t at the two delta declarations and the nine fix_* signatures.