ltcmelo / psychec, Hacker News

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 interfaceillustrates the essential functionality of PsycheC.

Requirements

• Cmake
• C 14 compiler
• Haskell Stack
• Python 3

cmake CMakeLists.txt make

Running the Tests

./ psychecgen -t ./CompileTests.sh cd solver && stack test

(Cnippet) **************

The simplest way to use PsycheC is through theCnippetcompiler adapter. Let us see an example. *******

Consider the filenode.cBelow.

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

If you were to compilenode.cwith GCC / Clang, you would issue a command similar to this one:

gcc -c node. c

As a result, an object filenode.owould have been produced. However, this will not happen, since a declaration forTis not available. Instead, you will get an “undeclared identifier” error.

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

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

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

typedefstructTYPE_1__ {     intvalue;     structTYPE_1 __ * next; } * T;

Generic Programming

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

PsycheC provides an alternative tovoid *and# macrosfor writing generic code in C. This is how you would implement a generic linked-list’sprependfunction.

_ GenericvoidPrepend(_ 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 neithernode_tnorvalue_t. The definition ofprependapplies “for all” kinds of nodes and values. This way, you can focus on thealgorithms(the essence of generic programming).

Let us create 2 lists, one ofintand another ofpoint_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_tp;     P.x=p.y=42;     Prepend(& plst, p); }

Now, PsycheC infers that there “exists” a (node) type whose value is anint, together with an specialization ofprependfor such arguments. A different (node) type forpoint_t“exists” too, with its corresponding specialization ofprepend.

Check the examples directory forthis snippet.

Publications

PsycheC is an ongoing research project. It has been presented at:

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

Below is a list of papers whose developed tooling rely on PsycheC:

• Generation of in-bounds inputs for arrays in memory-unsafe languages ​​; Proceedings of the (IEEE / ACM International Symposium on) CGO(Code Generation and Optimization), February 2019, Pages 136 – 148.

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

This is an online article about PsycheC:

• Programming in C with Type Inference