You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
For some benchmarks, the register type seemingly is {map_fd, number}, possibly due to a join operation over control flow. However, later it can be seen (in PREVAIL) that the type is resolved to map_fd and number on different successor branches without explicit conversion. Since the type domain is unable to track multiple regions/provenance, it is not possible to keep track of both {map_fd, number}. This might be needed in future, but for now it is okay to be less precise.
The text was updated successfully, but these errors were encountered:
As an example, consider benchmark prototype-kernel/xdp_ddos01_blacklist_kern for section xdp_prog. Basic blocks 106:107 and 106:108 both have pre-invariant that r2 is {map_fd, number}. However, 106:107 has post-invariant as r2.type=map_fd, while for 106:108, r2.type=number without explicit conversions.
For some benchmarks, the register type seemingly is
{map_fd, number}
, possibly due to a join operation over control flow. However, later it can be seen (in PREVAIL) that the type is resolved tomap_fd
andnumber
on different successor branches without explicit conversion. Since the type domain is unable to track multiple regions/provenance, it is not possible to keep track of both{map_fd, number}
. This might be needed in future, but for now it is okay to be less precise.The text was updated successfully, but these errors were encountered: