Francesco Bertolaccini

Z3 all the things

13

Converts Rellic to operate on Z3 expressions for as long as possible, only materializing to Clang AST before expression simplification. ~~Also keeps conditions in CNF without exponential blowup with a...

Invalid stores like `store i8 undef, i8* null` are ignored at the code lifting level ( https://github.com/lifting-bits/rellic/blob/master/lib/AST/IRToASTVisitor.cpp#L735-L738 ) , but they should be removed by a preprocessing pass.

Using substitution maps for provenance tracking loses info

2

Master branch uses a `substitutions` map in each pass to keep track of how AST nodes are substituted, but this not fine-grained enough. As an example, let's say we have...

Refine types based on debug metadata

5

Solves #190

Recover type information

8

Currently, some type information (e.g. `const`, `volatile`) regarding variables is lost. For example, this source code ```c struct foo { int x; }; typedef struct foo foo_t; int main(void) {...

Merge local variables and parameter declarations when possible

5

Rellic generates temporary local variables to store parameter values, instead of directly using the parameters themselves: ```c int foo(int a, int b, int c) { a = a * 2;...

Improve `while` lifting

7

Currently, a loop such as this while(cond) { body } rest is lifted like this: while(cond) { body } if(!cond) { rest } It would be nice to get rid...

Maintain `goto`s when present in the original C code

3

Currently, Rellic always avoids generating `goto`s, favoring `if`s and `while`s. This is not always favorable, e.g. ```c extern int doA(void); extern void undoA(); extern int doB(void); extern void undoB(); extern...