Poor Pointer Analysis Inside of Store Prevents us From Associating a Field of the Abstract Object to a Store

[2over12]

In mooosl at address 0010160f a store occurs of the value returned by key_hash to the calloced pointer at field offset 32. The constraints are setup such that we know that instr_001015a9_0_RBP.load.σ64@-16 is a subtype of the GLOBAL.store.@0_size64

Basically we know that stack location holds a pointer that is equivalent in type to the global linked list. We also know that

weak_integer ⊑ instr_00101609_0_RDX
instr_00101609_0_RDX ⊑ instr_0010160f_0_$U3100.store.σ64@0
instr_0010160b_1_$Uc000.+32 ⊑ instr_0010160f_0_$U3100
instr_001015a9_0_RBP.load.σ64@-16 ⊑ instr_0010160b_1_$Uc000

Which if we look as a human says that the pointer at .σ64@-16 has a field at offset 32 that can have a weak_integer stored to it. But constant integers proof rules in retypd dont work that way. The only proof rule we have for +32 is a covariant field rule so if we had a ⊑ b and a.+32 exists somewhere and b.+32 exists somewhere then we can prove a.+32 ⊑ b.+32, which is incredibly useful but doesn't help us prove this property. Any proof rule that accounts for these fields is going to be highly complex and I doubt it could be automated so lets consider a different approach where we lean on our abstract interpreter:

(uint8_t **)calloc(1,0x30) ought to create us an abstract object in the interpreter of size 0x30. Lets call the identifier beta

We ought to be able to generate the constraints return_from_calloc ⊑ beta therefore instr_001015a9_0_RBP.load.σ64@-16 ⊑ beta

Then in the store we ought to be able to conclude from abstract interpretation that the store is going to imply: iinstr_0010160f_0_$U3100.store.σ64@0 ⊑ beta@32sigma64 allowing us to prove the property that the field is a weak_int

I suspect this isn't happening currently because we aren't creating a reasonable abstract object from a 1 elem calloc

[2over12]

There is an appropriate abstract object (instr_001015ba_2@RAX), but this object isn't letting us bind up the pointer for some reason

[2over12]

The issue here is pretty subtle. The trouble is we recognize and associate constraints to the abstract identifier instr_001015ba_2@RAX the trouble is there is no constraint binding the pointer to the abstract object.

The pointer stored into the linked list is the pointer represented by the dtv: instr_001015a9_0_RBP.load.σ64@-16 but there is no relationship between the abstract object pointed to by the pointer in instr_001015a9_0_RBP.load.σ64@-16. The two layers of indirection cause the proof to fail. Since none of the accesses can relate the abstract object back tot the original pointer itself we never see some constraint like instr_001015a9_0_RBP.load.σ64@-16 <= instr_001015ba_2@RAX