What is RefacCert ?

RefacCert is a project to explore the idea of a "proven correct" refactoring tool. It is designed for C source code and is based on CompCert C : http://compcert.inria.fr .

Contract

Our main focus is to ensure that if the operation succeeds, the resulting program will have the same behavior as the original program. It the operation fails, the program is left unchanged.

Supported operations :

• Renaming global variables.
  • And swapping two global variable names.
• Removing unused local variables.
  • And adding a local variable.
• Renaming labels.

Status

This is a proof of concept. It has the limitations given below.

Publications

• The research report is available at https://hal.archives-ouvertes.fr/hal-01248121 : A Correct Refactoring Operation to Rename Global Variables in C Programs (2015)
• An article was presented at the 4th International Workshop on Verification and Program Transformation (available in Electronic Proceedings in Theoretical Computer Science / apr. 2016). Renaming Global Variables in C Mechanically Proved Correct
• Another research report : Memory bijections: reasoning about exact memory transformations induced by refactorings in CompCert C : https://hal.archives-ouvertes.fr/hal-02078356/ (2019)

Limitations

• Our proofs of correctness cannot take the preprocessor into account.
• Our prototype cannot preserve comments, layout and preprocessing directives.
• Some parts of the tool (the driver) are written directly in OCaml and cannot be taken into account by proofs of correctness.

Development

Developped by Julien Cohen, Lina laboratory (Ascola team http://www.emn.fr/z-info/ascola/doku.php), University of Nantes (Polytech Nantes). The operation that removes an unused local variable is developped by Igor Zhirkov.

What's new ?

Version 0.9

• Improvement of the renaming of labels : you have to specify the function where the renaming takes place. The labels in other functions are not impacted.

Version 0.8

• New refactoring operation : rename labels. This operation is proved correct, but it is not complete : it rejects some cases where the renaming would be legal (see the tests).

• Upgraded to CompCert 3.4.

Version 0.7 (based on CompCert 2.7.1)

• New refactoring operation : add/remove a local variable, by Igor Zhirkov.
• Proof of correctness for renaming global variables is better structured.
  • Correspondences between semantic constructions in programs (contexts, continuations, states...) are now represented by relations and not by functions anymore. Proofs are easier, in particular for context transformation, which needed a painful encoding before, and for continuation transformation, which was too memory and time consuming.
  • More iterators are used to ditinguish properties coming from renaming and those coming from tree traversals.

Version 0.6 (based on Compcert 2.6)

• BUGFIX : problematic situations with block variables are now rejected.

Version 0.4 (based on Compcert 2.4)

• Added an operation 'swap' to swap two global variable names. This operation relies on the base operation that renames global variables.
• A sufficient precondition for Swap is proved.

Version 0.3

• The transformation is proved invertible. This simplifies some results for bisimulation (in particular backward simulation comes for free from forward simulation).

Version 0.2

• Preservation of behaviors (type @program_behavior@, relation @program_behaves@).
• Example of static composition.

Version 0.1 (based on Compcert 2.3pl2)

• Renaming of global variables.
• Preservation of transitions with a correspondence on traces is proved.