CHB: Trampoline path sensitivity #160
Description
Trampoline payload functions encode the action to be taken (e.g., fall-through, continue, return) in the return value of the function. Even though the trampoline function is inlined in the analysis, the return instruction forms a join point in that analysis, thus preventing the downstream analysis to take full advantage of the invariants generated in the different paths through the trampoline function. Precision can be improved by adding path sensitivity to the trampoline.
This approach was prototyped in March 2024 on the grididps challenge problem. The control flow graph attached
cfg_inlined_paths.pdf
demonstrates the effect of adding path sensitivity: the grey nodes denote dead code; the conditions imposed on each path lead to more precise invariants on the live code, thereby enabling the proof of stronger properties on the live code. The prototype implementation provided most of the infrastructure to create the paths, but did not include any facility for the user to specify (e.g., via userdata) where in the code to activate it, and the feature was never taken into production.
The current effort seeks to make this facility available in a more robust way. The work will include a redesign of the representation of location contexts, to facilitate the composition of multiple nested contexts, e.g., path sensitivity on top of function inlining, as is necessary for trampoline payload functions. The motivation for the redesign is that the current implementation is manageable for single-level contexts, but gets increasingly awkward for nested contexts, as the contexts are currently all directly encoded in the name of the location (as is visible in the cfg attached).
The current effort is primarily focused on the addition of path sensitivity to trampoline payloads. It will take elements from the patch description file to determine the paths split and join points. Based on experience with this feature in this setting, more generalization may be added later to make this facility available in a wider setting.