Heap repair

High-level

Summary:

a new automated program repair technique using Separation Logic. Doesn’t need test-cases. Ensure general pointer safety properties: resource leaks, memory leaks, and null dereferences.

Evaluation:

Correctly fixing 55 bugs, including 11 previously undiscovered bugs, in 11 projects (in Java and C, e.g. apktool, dablooms, lex, swoole etc.)

Takeaways:

I don’t feel like there is much to be learned.

Practical Value

What you can learn from this to make your research better?

I don’t see how this work is interesting. Not comparing with any baseline seems not good either. I think I am just going to bash this work.

Details and Problems From the presenters’ point of view, what questions might audience ask?

How much time information is used?

What is the definition of a “fix”? Example?

FootPatch currently requires a simple manual fix specification, generally per bug type

How does this spec look like?

FP and FN?

We do not explicitly compare our technique to prior repair techniques.

We argue that our focus on explicitly codifying semantic effects offers additional protection against patch overfitting.

What is semantic effects?

Comparison with CheckerFramework?

Soundness?

The relationship between proof search and program repair.

https://github.com/squaresLab/footpatch/blob/master/infer/src/footpatch/footpatch_spec.ml