symbolic: Improve the semantics of pointer comparisons

[langston-barrett]

Consider doPtrLt:

macaw/symbolic/src/Data/Macaw/Symbolic/MemOps.hs

Lines 858 to 870 in 6457541

	doPtrLt :: PtrOp sym w (RegValue sym BoolType)
	doPtrLt = ptrOp $ \bak mem w xPtr xBits yPtr yBits x y ->
	do let sym = backendGetSym bak
	both_bits <- andPred sym xBits yBits
	both_ptrs <- andPred sym xPtr yPtr
	sameRegion <- natEq sym (ptrBase x) (ptrBase y)
	okP1 <- isValidPtr sym mem w x
	okP2 <- isValidPtr sym mem w y
	ok <- andPred sym sameRegion =<< orPred sym both_bits
	=<< andPred sym both_ptrs =<< andPred sym okP1 okP2
	undef <- mkUndefinedBool sym "ptr_lt"
	res <- bvUlt sym (asBits x) (asBits y)
	itePred sym ok res undef

First of all, there's some redundancy here: andPred sym okP1 okP2 is strictly stronger than both_ptrs, which it is anded with.

More concerningly, this function invents a fresh predicate (via mkUndefinedBool) that encodes the result of the comparison in the case that they aren't pointers to the same allocation. This means that multiple calls to doPtrLt with the same pointers return uncorrelated fresh predicates, so that the following pseudo-code program could report an assertion failure, even though the assertion should be unreachable:

void f(void *p, void *q) {
    if (p < q) {
        if (q < p) {
            assert(false);
        }
    }
}

(I haven't tested this, but it should be easy to develop such a test case when we have a CLI #390). doPtrLeq suffers from the same problem.

It's not clear if there's really a great solution here. In the ideal world, Macaw would explore all and only the feasible executions of a program, but for these operations it appears that there's a trade-off:

• If we just assert (as a safety condition) that pointer comparisons only happen between pointers to the same allocation (or between raw bitvectors), we'll probably miss out on being able to simulate real code that appears in the wild.
• However, the current code is permissive enough that it explores infeasible executions.

Perhaps it's worth exposing more knobs with which to tune Macaw's behavior, as appropriate for downstream clients? For clients doing verification, this more permissive behavior might be fine: if you can prove the verification conditions for all the feasible executions plus some infeasible ones, you've still proved them for the feasible ones. However, for bug-hunting, we might might care less about missing some feasible paths, prefering fewer false positives (reports of possible bugs that cannot occur in real executions).

[RyanGlScott]

I agree that this behavior is not desirable in many applications, and it would be nice to offer easy-to-use alternatives. We've exposed a similar knob on the crucible-llvm side for configuring the behavior of how "undefined" memory from an uninitialized memory load should work (see here).