search

mgehre / llvm-project

The home of the clang-based implementation of lifetime safety warnings.
39 stars 4 forks source link

Auto-generate function annotations based on their definitions #17

Open mgehre opened 6 years ago

mgehre commented 6 years ago

To convert my codebase towards this checker, I would like to automatically generate the annotations of a function (on its definition and all declarations) that match the actual psets used in the definition.

Note: This might have an ordering problem because one might annotate all callees before their callers, which is harder with loops in the function call graph.

Xazax-hun commented 5 years ago

There are many alternatives how to do this.

One way is to start the broadest possible psets for all the inputs and each time we would see an error (e.g. a null dereference) we remove the corresponding pset from the input and redo the analysis. Repeat until no erros are found.

Propose to the user an annotation that contains the PSet for all the inputs (after pruning the elements that would cause a warning). The PSets for the outputs will be the union of their pset on all exit points.

This would basically assume that the code is correct and it would try to compute kind of the "weakest lifetime precondition", i.e. the most broad psets that cannot cause problems.

The broader the input psets are the easier for callers to satisfy it. I am not sure if this would be a good strategy for the output psets though. But we will see :)