This PR refactors the C front-end. The centerpiece of the changes made is the new intermediate representation between FrontC and Core Theory.
This intermediate representation is called "PatchC", since its semantics and structure (as well as the set of features) are intended for writing patches instead of full C programs.
The abstract syntax explicitly separates values from effects; all expressions are pure. Moreover, all expressions are explicitly typed, and indeed type checking is now performed. There may be some oddities with the semantics of C when it comes to rounding out the edges of the typing discipline currently in use, but for the moment we seem to be in good shape.
To that end, the Core_c pass in the compiler is greatly simplified, and the code is very straightforward.
Since the FrontC to PatchC pass involves elaboration, it might introduce assignments to temporary variables that hold intermediate results, which may result in larger code if the register allocator and instruction scheduler pick a suboptimal solution. Therefore, it seemed useful to introduce this optimization layer into VIBES, basically for free.
This PR refactors the C front-end. The centerpiece of the changes made is the new intermediate representation between FrontC and Core Theory.
This intermediate representation is called "PatchC", since its semantics and structure (as well as the set of features) are intended for writing patches instead of full C programs.
The abstract syntax explicitly separates values from effects; all expressions are pure. Moreover, all expressions are explicitly typed, and indeed type checking is now performed. There may be some oddities with the semantics of C when it comes to rounding out the edges of the typing discipline currently in use, but for the moment we seem to be in good shape.
To that end, the
Core_c
pass in the compiler is greatly simplified, and the code is very straightforward.I also copied the code from BAP's BIR optimization plugin: https://github.com/BinaryAnalysisPlatform/bap/tree/master/plugins/optimization
Since the FrontC to PatchC pass involves elaboration, it might introduce assignments to temporary variables that hold intermediate results, which may result in larger code if the register allocator and instruction scheduler pick a suboptimal solution. Therefore, it seemed useful to introduce this optimization layer into VIBES, basically for free.
Also, addresses https://github.com/draperlaboratory/VIBES/issues/164 and https://github.com/draperlaboratory/VIBES/issues/163