trailofbits/binary_type_inference

Examine implications of not considering the original type when using callsite types for concrete refinement

Closed this issue · 1 comments

In dca9410 I removed intersecting/unioning callsite types with the original representation. This decision was made because the sketch union of out parameters would result in a loss of information.

Ie. a type like:

sub_id.in <= sub_id.out
sub_id:callsite_0.out.field_at_0 <= int
sub_id:callsite_1.out.field_at_4 <= float

Would discard the structure because the identity function has no language intersection with the original type. We should more carefully examine the implications of this decision.

Ah ok one plausible issue is we have overlapping types that get refined by binding parameters and we treat those parameters in isolation then we will lose information from other refinements. Bumping this to med/bug since im observing this in a test