Enforcing concreteness of pointers with types

[langston-barrett]

Concreteness of pointers is an important invariant, and there are at least a few places in Crucible that expect at least concrete allocation numbers, e.g.

crucible/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

Line 646 in 46dd13e

Nothing -> return (Left (text "Cannot resolve a symbolic pointer to a function handle:" <$$> ppPtr ptr))

(For another example, see discussion on #376). We should consider using types to enforce/expose/document this invariant. Pointers are represented by an allocation number and an offset, so there's a 2x2 matrix of concrete vs symbolic data.

There are two places in crucible-llvm that I can think of right now that could use this information fruitfully:

• The function doMalloc always returns concrete pointers.
• In MemImpl, the memImplGlobalMap should only contain concrete pointers, so doResolveGlobal could return concrete pointers.

There are two ways I can think of to reflect this information at the type level:

Newtypes

We could have up to three newtypes: ConcretePointer, ConcreteAllocationNumber, and ConcreteOffset. I think the above code snippet justifies ConcreteAllocationNumber, I'm not sure if the other two are worth it.

I would expect at least the following API:

• a smart constructor concretePointer :: LLVMPtr -> Maybe ConcretePointer
• a getter extractAllocationNumber :: ConcretePointer -> Int

With possibly some additional functions, like clones of doPtrAddOffset that retain the concreteness of the allocation number. This could end up with a reasonable amount of boilerplate if we pursue the full 2x2 matrix.

Type indices

We could also use two type-level indices to LLVMPtr, both with kinds isomorphic to Bool. This would probably enforce the strongest invariants, but this is a very commonly used datatype and the complexity tradeoff might not be worth it, especially since almost everything that uses pointers is polymorphic in their concreteness.