correctcomputation / checkedc-clang

This is the primary development repository for 3C, a tool for automatically converting legacy C code to the Checked C extension of C, which aims to enforce spatial memory safety. This repository is a fork of Checked C's.
14 stars 5 forks source link

Better choice of pointer-type constraint solution for `-infer-types-for-undefs` #697

Open mattmccutchen-cci opened 3 years ago

mattmccutchen-cci commented 3 years ago

IIUC, -infer-types-for-undefs currently uses the same pointer-type constraint solving algorithm for undefined functions as 3C normally uses for all functions: first the "greatest" solution (closest to _Ptr) for parameters, then the "least" solution (closest to _Nt_array_ptr) for returns (modulo some special cases?), then the greatest solution for everything else (this part isn't relevant to undefined functions). This algorithm is based on the idea that we want to give each function the most "useful" type that is consistent with its body in order to support valid calls that we haven't seen yet. But if we don't have the function body and we simply skip generating any constraints for the function body, this algorithm won't give good results: it will tend to make all parameters _Ptr and all returns _Nt_array_ptr. Thus, there was a proposal to give each undefined function the type that makes the fewest assumptions about its implementation that is consistent with all current call sites: essentially the opposite of what 3C does for defined functions. This would be implemented by using the least solution for parameters and the greatest solution for returns (maybe with some special cases I'm not familiar with).