Fix external/picosat undefined behaviour.

[kevemueller]

Suggested fix was reported to Prof. Biere by email.

[arrowd]

I remember stumbling upon this when playing with UBSan, but I didn't get to fix it properly.
Thanks for that!

[kevemueller]

Hi Gleb,

please have a close look as well as I miss the depth of PicoSAT knowledge that you have. I interpreted this as a simple start/end pointer comparison with the edge case of both not initialized (i.e. NULL).

Cheers,
K

[arrowd]

IIRC, the UB was coming from doing a pointer arithmetic on a possible NULL pointer. So I'd rephrase the fix as

if (ps->thead != NULL && ps->trail != NULL)
  return  ps->thead == ps->trail + ps->max_var;
else
  return 0;

[kevemueller]

Yes, in in the case ps->thead and ps->trail were both null. The UB was NULL == (NULL + 8). Your true clause is captured in my second clause. Your false clause is weaker than my first clause, as ps->thead == ps->trail (both null) and ps->max_var (0) is a positive as well.

…

On 2 Dec 2024, at 16:25, Gleb Popov ***@***.***> wrote: IIRC, the UB was coming from doing a pointer arithmetic on a possible NULL pointer. So I'd rephrase the fix as if (ps->thead != NULL && ps->trail != NULL) return ps->thead == ps->trail + ps->max_var; else return 0; — Reply to this email directly, view it on GitHub <#2375 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ADYNFPF5YK4Y2LHA74LCFL32DR3WPAVCNFSM6AAAAABS3POXKWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKMJRHAZTOMRRGQ>. You are receiving this because you authored the thread.

[arrowd]

Right, but then just if (ps->trail != NULL) should suffice?

[kevemueller]

Correct! I have simplified the clause.
Thx!