trailofbits / binary_type_inference

GNU General Public License v3.0
12 stars 0 forks source link

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

Closed 2over12 closed 2 years ago

2over12 commented 2 years ago

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?

2over12 commented 2 years ago

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.

2over12 commented 2 years ago

Addressed in 517dd34806f2c7624b2d698c2f8c6cd3a6c324e5