The Psyche project is going through a major overhaul in a private branch which will (hopefully) be merged soon.
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: