Inferring contracts by abstract interpretation with application to pointer nullness analysis

This paper proposes a semantic static analysis for inferring nullable or non-null pointer annotations in low level programs. The analysis is formulated on a minimalistic imperative language and it is expressed as a least fixpoint computation over pointer annotations calling a sound type-checking algorithm. Therefore, this analysis may be used for more general annotations than pointer nullability. We prove two main properties for this approach: (1) when using a sound and precise type-checker (i.e., without false alarms), it will find an annotation that guarantees the absence of run-time errors due to pointer deference, if such an annotation exists, (2) when the type-checker is only sound, the errors singled out by the analysis are real errors. We report on the implementation of this method in Codex , a static analyzer for C and binary code. Codex already provides an abstract interpretation based type-checker for a rich dependent type systems. The evaluation of our implementation on a benchmark of challenging programs shows that the inference is better than manual annotations obtained by code inspection.