Macaw symbolic seems to produce doubled memory safety assertions

[robdockins]

When doing verification using macaw symbolic via SAW, I'm getting what appear to be redundant proof obligations on memory reads and writes. The resulting proof obligations always seem to be paired up, like the following:

[16:52:52.607] Goal aesni_gcm_decrypt (goal number 0): safety assertion
at 0x76031e in aesni_gcm_decrypt
[doReadMem] Reading through an invalid pointer: (5, 0x50:[64])


[16:52:52.651] WARNING: admitting goal aesni_gcm_decrypt
[16:52:52.658] Goal aesni_gcm_decrypt (goal number 1): safety assertion
at 0x76031e in aesni_gcm_decrypt
Error during memory load

This appears to be caused by these (And similar lines elsewhere)

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

Lines 1019 to 1022 in 2791b10

	res <- Mem.assertSafe bak =<< Mem.loadRaw sym mem ptr ty alignment
	case memValToCrucible memRep res of
	Left err -> fail $ "[doReadMem] " ++ err
	Right crucVal -> return crucVal

The assertSafe will generate one obligation, and the fail also appears to bubble out and generate a separate proof obligation.

Are these actually asserting separate things that are necessary for soundness? If so, can we combine them somehow into a single obligation? If not, what's the best way to remove one of them?

[robdockins]

On further investigation, I think the additional assertion is actually coming from here:

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

Lines 1008 to 1012 in 2791b10

	-- Check pointer is valid.
	-- Note. I think we should check that pointer has at least "bytes" bytes available?
	ok <- isValidPtr sym mem ptrWidth ptr
	check bak ok "doReadMem" $
	"Reading through an invalid pointer: " ++ show (Mem.ppPtr ptr)

@travitch, as far as I can tell, this check is just redundant (as are related ones in doWriteMem, etc.) is there some aspect of this that I am missing?

[travitch]

@robdockins Is it redundant because loadRaw and similar functions ultimately do their own checks?

I'm not that familiar with the reasoning for why these functions are structured the way they are. I suspect you are right. If I had to guess, maybe these were copied and pasted from crucible-llvm before a refactoring that cleaned things up?

If loadRaw and friends already do this check, I have no objections to removing it. My only concern would be if some downstream tools are counting the number of assertions and relying on that somehow. I have one that I'm happy to fix. Perhaps @andreistefanescu or @chameco know if any of the x86 SAW proofs might be disrupted?

[robdockins]

Indeed, my hypothesis (which I or someone should validate) is that the isValidPtr check boils down in the end to an isAllocated check, which is already performed by loadRaw and storeRaw and is therefore purely redundant.

SAW can indeed use the numbering of goals to select what to do; I don't know offhand how common that is in our finished proofs, but it is something to look out for.

[travitch]

I'm happy to fix this after getting an idea from the SAW team on expected breakage.

I did just chase down isValidPtr. It boils down to Generic.isValidPointer, which calls isAllocated, so I believe you are correct.

[robdockins]

I think the easiest way is to make a SAW PR and see what breaks. I can do that, if you don't think there's some subtle reason to have the checks in there separately.

[travitch]

At this point I'm pretty confident that there is no subtle reason - lets give it a shot. Thanks for starting on the PR

[RyanGlScott]

This was fixed in #310.