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.

mbeddr supports embedded software development based on an extensible
version 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.

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:

In mbeddr-C you would write something like:

Variability in mbeddr

 

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 to be held in Genova on the 5th of March.

Download the guide with 68 resources on Creating Programming Languages

68resources

Receive the guide to your inbox to read it on all your devices when you have time

Powered by ConvertKit

Do You Need a Domain Specific Language (DSL)?

We can design and implement languages tailored to support your processes. We build also all the necessary infrastructure: editors, code generators, compilers, simulators. Our goal is to deliver complete solutions.

We can use different technologies like Jetbrains MPS, Xtext, and ANTLR for custom solutions.

1 reply

Trackbacks & Pingbacks

  1. […] Our colleague Federico Tomassetti has spent the last few months working on a facility that can import existing textual C sources into mbeddr. The challenge, of course, is to handle the preprocessor correctly. Federico has done various studies of how the preprocessor is used (see, for example, this paper). Based on these studies he has made significant progress with a preprocessor-aware importer. Today, Federico has recorded a screencast that shows the approach and the current status. The video is embedded below. For details you might also want to take a look at a related blog post. […]

Comments are closed.