The C to mbeddr-C importer: a first look

Currently I am in Munich, working at Fortiss, an institute of the Technische Universität München. I am here to work on mbeddr, which is a super-cool project.

What it means in practice?

We are using a Jetbrains MPS to build an extensible variant of C. Using mbeddr the user could write plain C code and use, when it is needed, some extra features.

One example? State machines. Instead of manually encoding them using a bunch of switch the user could use specific constructs. Some advantages:

• it is less error prone,
• it is faster,
• the editor understand what you are doing and catch your errors,
• you can verify that some properties holds (e.g., are all the states reachable?)

In other words mbeddr permits to work to higher levels of abstractions.

How C and mbeddr-C differs

Mbeddr supports almost all the features of C. It does not support error-prone features like the preprocessor. For most of the usages of the preprocessor mbeddr offers higher-level constructs. Consider for example variability. In C you would see this code:

void foo(){
  init();
#if SOME_FEATURE_IS_ENABLED && VERSION>3
  // do great things!
#elif SOME_FEATURE_IS_ENABLED
  // do less great things
#else
  // do almost nothing
#endif
  printResults();
}

In mbeddr-C you would write something like:

in practice you have the possibility to decorate statements and functions with their presence condition. This is cool for many reasons, first of all the possibility for mbeddr to verify that your code is valid under every possible configuration.

What is my contribution?

I am building the importer which converts plain C to mbeddr-C. It interprets how the preprocessor is used in C code and translate it to higher level concepts.

In this video I show the current state of the importer.

If you want some more details about the importer you can read this very preliminary paper, accepted for the Reverse Engineering workshop archived copyto be held in Genova on the 5th of March.

mbeddr supports embedded software development based on an extensibleversion of C language and IDE. Existing extensions include interfaces with pre- and postconditions, components, state machines and physical units, as well as support for requirements tracing and product line variability. Based on these abstractions, mbeddr also supports formal verification based on model checking and SMT solving.