llvm: Fix validity predicate for memory reads with symbolic block numbers

[langston-barrett]

Previously, this case returned the concretely-true predicate. This is incorrect, as isAllocatedGeneric takes an argument inAlloc, which is supposed to be applied to the AllocInfo of the allocation with the matching block number, as it is in the other branch.

Mea culpa, looks like I introduced this bug long ago.

[langston-barrett]

I tried to create a regression test, but I'm having trouble triggering this case. Here's what I tried:

(defun @main () Unit
  (start start:
    (let szbv (fresh (Bitvector 64)))
    (let sz (ptr 64 0 szbv))

    (let mg (resolve-global "memset"))
    (let mh (load-handle (Ptr 64) ((Ptr 64) (Ptr 32) (Ptr 64)) mg))

    (let asz (bv 64 1))
    (let p (alloca none asz))
    (let pblk (ptr-block 64 p))
    (let qblk (fresh Nat))
    (assume! (equal? qblk pblk) "equal block numbers")
    (let q (ptr 64 qblk (bv 64 0)))

    (let c (ptr 32 0 (bv 32 0)))
    (let _ (funcall mh q c sz))

    (return ())))

But it looks like this wasn't good enough to both (1) avoid the Just case of asNat but (2) still hit the Just case of asConstantPred.

[langston-barrett]

For what it's worth, I do have a test-case for a downstream project that this fixes.

[RyanGlScott]

If it makes you feel better, some of the uc-crux-llvm test cases are sensitive to this change (as seen in the crux-llvm CI failures), so there's that. I'll leave it to your judgment to audit these test failures to figure out which changes are benign and which are evidence of deeper issues.

[langston-barrett]

It looks to me like what's happening is that UC-Crux previously found certain errors in each of these test cases that were adequately handled by its heuristics. Fixing this predicate introduces a new kind of error, and the heuristics aren't sophisticated enough to deal with this one. UC-Crux then gives up, saying it's not sure how to avoid these errors with a new precondition (leaving them "unclassified").

This is unfortunate, but UC-Crux already can't abduce preconditions for a wide variety of programs, so I don't consider this a blocker.

[RyanGlScott]

I do wonder if this will cause other proof goals to shift in downstream projects (e.g., SAW). That being said, this code is clearly more correct than it was before, so I'm in support of landing it.