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
In the presence of buffer-overflows our alias analysis is unsound and there can be different same-address accesses that are not considered aliasing and thus will not appear in the loc relation of an eager encoding.
However, the CAAT solver established the loc relation in an execution by comparing the address values directly thus ignoring the (unsound) alias analysis.
This results in cases where the CAAT solver and the eager encoding return different verdicts.
What do we do about this?
The alias analysis is intentionally unsound in overflow cases, so we cannot blame this issue on the analysis.
I guess the most reasonable fix is to let CAAT inherit this unsoundness by querying the alias analysis between same-address accesses?
Alternatively we live with this discrepancy as it only appears on benchmarks where we are unsound anyways.
The text was updated successfully, but these errors were encountered:
In the presence of buffer-overflows our alias analysis is unsound and there can be different same-address accesses that are not considered aliasing and thus will not appear in the
loc
relation of an eager encoding.However, the CAAT solver established the
loc
relation in an execution by comparing the address values directly thus ignoring the (unsound) alias analysis.This results in cases where the CAAT solver and the eager encoding return different verdicts.
What do we do about this?
The alias analysis is intentionally unsound in overflow cases, so we cannot blame this issue on the analysis.
I guess the most reasonable fix is to let CAAT inherit this unsoundness by querying the alias analysis between same-address accesses?
Alternatively we live with this discrepancy as it only appears on benchmarks where we are unsound anyways.
The text was updated successfully, but these errors were encountered: