Null pointer comparison of out-of-bounds pointers is unsound

Problem: Currently, Caesium allows arbitrary out of bounds pointer construction and pointers always compare in-equal to NULL. This is unsound since one can create an out of bounds pointer with address 0 and it would still compare in-equal to NULL.

Proposed solution:

• For each block, keep track of the bounds of the allocation. I.e. make st_used_blocks a gmap from Z to (Z, Z).
• Add heap_loc_in_bounds : loc -> nat -> state -> Prop which means that the range l...l+n is included in the range of the allocation
• Add a heap_loc_in_bounds l 0 st precondition to comparison with NULL
• (Optional) Make heap_loc_in_bounds a precondition of offset operations
• Add a loc_in_bounds : loc -> nat -> iProp ghost state that corresponds to heap_loc_in_bounds, should be persistent
• From l |->{q} v you should get loc_in_bounds l (length v)
• Add a axiom to type that ty_own implies loc_in_bounds l 0

Open problems:

• What about an allocation that ends at the maximal address and where the 1-past-the-end pointer overflows to NULL? Can we just not support this?

Handled in a later step, not here:

• Making allocations return pointers in a finite address range
• Making allocation able to fail

added bug caesium soundness typesystem labels

changed the description

changed the description

closed with commit dc744bb2

made the issue visible to everyone

marked the checklist item For each block, keep track of the bounds of the allocation. I.e. make st_used_blocks a gmap from Z to (Z, Z). as completed

marked the checklist item Add heap_loc_in_bounds : loc -> nat -> state -> Prop which means that the range l...l+n is included in the range of the allocation as completed

marked the checklist item Add a heap_loc_in_bounds l 0 st precondition to comparison with NULL as completed

marked the checklist item (Optional) Make heap_loc_in_bounds a precondition of offset operations as completed

marked the checklist item Add a loc_in_bounds : loc -> nat -> iProp ghost state that corresponds to heap_loc_in_bounds, should be persistent as completed

marked the checklist item From l |->{q} v you should get loc_in_bounds l (length v) as completed

marked the checklist item Add a axiom to type that ty_own implies loc_in_bounds l 0 as completed

marked the checklist item (Optional) Make heap_loc_in_bounds a precondition of offset operations as incomplete

marked the checklist item Add a axiom to type that ty_own implies loc_in_bounds l 0 as incomplete