PsycheC is a compiler frontend infrastructure for the C language that is enabled with an ML/Haskell-style (unification-based) type inference engine. This online interface illustrates the essential functionality of PsycheC.

Applications:

• Enabling static analysis on partial programs.
• Supporting semantic tools despite of #include failures.
• Compiling a code snippet (e.g., retrieved from a bug tracker).
• Generating test-input data for a function, individually.
• Prototyping of an algorithm without a type specification.

Be creative!

To build PsycheC:

• Cmake
• C++14 compiler
• Haskell Stack

To use PsycheC (download here):

• Python 3

cmake CMakeLists.txt  
make

export PATH=$PATH:/path/to/psychec

The simplest way to use PsycheC is through the Cnippet compiler adaptor.

Let us see an example.

Consider the file node.c below.

// node.c
void f()
{
    T v = 0;
    v->value = 42;
    v->next = v;
}

If you were to compile node.c with GCC/Clang, you would issue a command similar to this one:

gcc -c node.c

As a result, an object file node.o would have been produced. However, this will not happen, since a declaration for T is not available. Instead, you will get an "undeclared identifier" error.

Now, if you invoke Cnippet, the compilation succeeds (flag -f is for non-commercial use).

./cnip.sh -f gcc -c node.c

That is because, under the hood, PsycheC will infer the necessary missing definitions.

typedef struct TYPE_1__
{
    int value;
    struct TYPE_1__* next;
}* T;

This is a work-in-progress, feedback is welcome through this form.

PsycheC provides an alternative to void* and #macros for writing generic code in C. This is how you would implement a generic linked-list's prepend function.

_Template void prepend(_Forall(node_t)** head,
                      _Forall(value_t) value)
{
    node_t* n = malloc(sizeof(node_t));
    n->value = value;
    n->next = *head;
    *head = n;
}

It is not necessary to define neither node_t nor value_t. The definition of prepend applies "for all" kinds of nodes and values. This way, you can focus on the algorithms (the essence of generic programming).

Let us create 2 lists, one of int and another of point_t, and insert an new head to them.

int main()
{
    _Exists(node_t)* ilst = 0;
    prepend(&ilst, 42);

    _Exists(node_t)* plst = 0;
    struct point_t p;
    p.x = p.y = 42;
    prepend(&plst, p);
}

Now, PsycheC infers that there "exists" a (node) type whose value is an int, together with an specialization of prepend for such arguments. A different (node) type for point_t "exists" too, with its corresponding specialization of prepend.

Check the examples directory for this snippet.

./psychecgen -t
./test_infer_and_compile.sh
cd solver && stack test && cd -
cd formalism && ./test_muC.sh

PsycheC is an ongoing research project.

• Type Inference for C: Applications to the Static Analysis of Incomplete Programs
  ACM Transactions on Programming Languages and Systems — TOPLAS, Volume 42, Issue 3, Artible No. 15, December 2020.

• Inference of static semantics for incomplete C programs
  Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL, January 2018, Article No. 29.

• AnghaBench: a Suite with One Million Compilable C Benchmarks for Code-Size Reduction
  Proceedings of the IEEE/ACM International Symposium on Code Generation and Optimization — CGO, 2021.

• Generation of in-bounds inputs for arrays in memory-unsafe languages
  Proceedings of the IEEE/ACM International Symposium on Code Generation and Optimization — CGO, February 2019, p. 136-148.

• Automatic annotation of tasks in structured code
  Proceedings of the International Conference on Parallel Architectures and Compilation Techniques — PACT, November 2018, Article No. 31.

• Synthesis of Benchmarks for the C Programming Language by Mining Software Repositories
  Proceedings of the Simpósio Brasileiro de Linguagens de Programacao — SBLP, September 2019.

An small article about PsycheC:

• Programming in C with Type Inference