Home » forums » LtU Forum

An Executable Formal Semantics of C with Applications

An Executable Formal Semantics of C with Applications
Chucky Ellison & Grigore Rosu, POPL '12

This paper describes an executable formal semantics of C. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes 99.2% of 776 test programs. It is the most complete and thoroughly tested formal definition of C to date. The semantics yields an interpreter, debugger, state space search tool, and model checker “for free”. The semantics is shown capable of automatically finding program errors, both statically and at runtime. It is also used to enumerate nondeterministic behavior.

This is the most ambitious use of rewriting logic that I've yet seen. On its face it seems like a quite elegant and general-purpose formulation; this specific C semantics is open sourced, even.

For more background I recommend the main page on the K framework.

Anyone else investigating this system and style of semantics definition?

By RobJellinghaus at 2012-07-24 00:54 | LtU Forum | previous forum topic | next forum topic | other blogs | 7038 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

(Suitable for front page?)

(Suitable for front page?)

By RobJellinghaus at Tue, 2012-07-24 00:54 | login or register to post comments

This K framework is pretty

This K framework is pretty impressive and really promising already, IMO. There is even an online interface to play with (I can't wait to give it a try). Don't miss to check out the nice Project Ideas page, too. Rewriting logic-based systems probably have a good fraction of their potential left to explore, esp. as one manages to raise their applicability abstraction level orderly enough.

By Cyril at Tue, 2012-07-24 03:05 | login or register to post comments

Program dependencies on installation.

This looks like a great idea, so I'm trying to install it under Cygwin on Windows 7. It's not easy. It requires Perl, many Perl packages, OCaml, Maude (requires Bison, Flex, BuDDy, Tecla, GNU MP), and K.

All the necessary Perl packages are available through the Cygwin installer. OCaml must be installed and built from source, and seems to work OK.

"Maude", however, has build problems. "Maude" hasn't been updated since 2010, and is now slightly out of sync with some of its dependencies. Maude's site has some old versions of packages they suggest using, but that doesn't help. I'm building Gnu MP under Cygwin, which fails because the version of Gnu MP suggested for Maude isn't compatible with current GCC compilers due to an incorrect regparm declaration deep inside the bignum package:

(aorsmul.c:43:1: error: conflicting types for '__gmpz_aorsmul', no longer accpted by GCC).

The current version of Gnu MP will build, but must be built with
./configure --enable-cxx, because the Gnu MP bignum package doesn't build the C++ libraries by default.

It's also necessary to install "libsigsegv" from Cygwin setup before building Maude.

Then, building Maude, we hit:

interact.cc: In static member function `static void UserLevelRewritingContext::setHandlers(bool)':
interact.cc:84:24: error: `SIGSTKSZ' was not declared in this scope

This is a known problem on Cygwin, where SIGSTKSZ is not defined. This broke the Boost libraries at one point, but they fixed that.

There's a version of Maude for Windows under Cygwin, but may require its own private copy of Cygwin, and apparently Java and Eclipse as well. That project warns about running other Cygwin programs while Maude is running, apparently due to DLL conflicts. I may try this later and see what it breaks.

More later.

By John Nagle at Sun, 2012-07-29 18:24 | login or register to post comments

Anyone else investigating

Anyone else investigating this system and style of semantics definition?

Executable logic compilers and compiler generators are a close fit since both deal with language and their meaning. So if you're looking for systems, ASF/SDF is one, Stratego is one, Rascall seems to be one. DMS software reengineering another one. So yeah, lots of systems available.

Systems like this vary in usability, so K being able to translate C is the recognition of having passed a milestone (other systems like DMS already passed.)

By marco at Mon, 2012-07-30 16:51 | login or register to post comments

Really tough to install

I got stuck trying to get Maude to work. The K people blame Maude, the Maude people aren't doing much with it any more.

Anybody else able to install and run this?

By John Nagle at Sun, 2012-08-05 03:30 | login or register to post comments

Re: Really tough to install

Thanks for your update on this. That's rather sad to read, IMO.

Still haven't got a chance to give it a try on my end, yet. But I might do so eventually. Is Maude the only blocker ?

By Cyril at Sun, 2012-08-05 08:07 | login or register to post comments

Is Maude the only blocker?

I think Maude is the main problem. Maude seems to be no longer actively maintained. The old versions have incompatibilities with current software. The problems are minor and fixable, but require getting into the internals of Maude, which I'd like to avoid doing.

By John Nagle at Fri, 2012-08-10 17:20 | login or register to post comments

Alternative approach

If you want it to run it under windows (presumably so that you can try it on code that you under your windows install) then another approach would be to stick linux in a VirtualBox VM. Ubuntu works quite nicely in there allow it is quite a fat install. Once you put the client additions into the VM then you can mount your windows drive as a psuedo-network mount and have a POSIX interface with access to your windows files. This might give you more joy than the cygwin approach.

By Andrew Moss at Sun, 2012-08-05 12:15 | login or register to post comments