trailofbits/binary_type_inference

Formal params and actual returns do not preserve the appropriate subtyping relation in the case of multiple definitions for the returned or passed value

Closed this issue · 2 comments

When accessing registers and possibly points to information for formal parameters the subtyping relationship goes in the wrong direction.

Ie. In assignment x=y
Where y is defined by a and b we get
a <= t
b <= t
t <= x

This works to get a passed up to x since both must be a subtype. (ie, a <= t <= x) We are using this same method for formals but it doesn’t work:

We have sub.in_0 <= t ie. Stating that the formal must be a subtype of its usages so say the defines are a and b we want to get sub.in_0 <= a and sub.in_0 <= b
So we want sub.in_0 <= t t <= a and t <= b but we use the same reg access method. So we get (sub.in_0 <= t and a <= t b <= t) the subtyping relationship causes a and b to not constraint in_0 at all.

This can probably happen for the memaccess stuff as well. Ie. imagine a parameter on the stack we get
stack_obj <= x.load.stack_loc

sub.in_0 <= x.load.stack_loc. Once again information on stack_obj does not constraint sub.in_0. Somewhat fortunately x.load.stack_loc will still constrain it in this case.

We should write testcases for both of these. Is it the case that what should actually happen is x.load.stack_loc <= stack_obj?

Ive decided that this is at least appropriate for registers. The point being each callsite register reaching the actual param can be upcasted to the param type. This means that the param type must be more specific therefore we should get param <= a
and param <= b which means we need t <= a, t <= b , param <= t.

Addressed in 517dd34