n0w0rk / goblint-cil

C Intermediate Language

C Intermediate Language (CIL)

CIL is a front-end for the C programming language that facilitates program analysis and transformation. CIL will parse and typecheck a program, and compile it into a simplified subset of C.

goblint-cil is a fork of CIL that supports C99, C11 as well as most of the extensions of the GNU C. It makes many changes to the original CIL in an effort to modernize it and keep up with the latest versions of the C language. Here is an incomplete list of some of the ways goblint-cil improves upon CIL:

• Support for C99 and C11.
• Compatibility with modern OCaml versions.
• Use Zarith instead of Num and use that for integer constants.
• Improved locations with columns and spans.
• Removal of unmaintained extensions and MSVC support.
• Use dune instead of make and ocamlbuild.
• Many bug fixes.

Quickstart

Install the latest release of goblint-cil with opam:

opam install goblint-cil

Read the excellent CIL tutorial by Zachary Anderson, much of which still applies to goblint-cil. The repository referenced in that document has now moved here.

ATTENTION: Don't install the cil package. This is the unmaintained original version of CIL.

Installation from Source

Prerequisites:

• opam
• GCC
• Perl

First create a local opam switch and install all dependencies:

opam switch create .

Then, you can use dune to build goblint-cil. Run the following commands to build and test goblint-cil:

dune build
dune runtest    # runs the regression test suite

To run a single test go to the build directory (e.g. _build/default/test) and run e.g.:

dune exec -- make test/array1

You can also install goblint-cil into the opam switch:

dune build @install
dune install

Usage

You can use cilly (installed in the opam switch) as a drop-in replacement for gcc to compile and link your programs.

You can also use goblint-cil as a library to write your own programs. For instance in the OCaml toplevel using Findlib:

$ ocaml
OCaml version 4.14.0

# #use "topfind";;
[...]
# #require "goblint-cil";;
[...]
# GoblintCil.cilVersion;;
- : string = "2.0.2"

License

goblint-cil is licensed under the BSD license. See LICENSE.

goblint-cil's Issues

Add support for parsing labels

Changes needed in cabs.ml and cabs.mly

And parse labels in cparser.mly

New type for asm instruction ->

tmpls: asm_inst list
asm_ins = record {label: type str list opt, operands: str list}

Check if additional registers are clobbered

cabs2cil.ml

Registers may be clobbered but nut declared in the clobber list.
Check if this happens.

Exception list of instructions whose last register is not written to
Exception list of registers that implicitly write to registers.

check if there are more efficient approaches.

https://www.felixcloutier.com/x86/

One command to rule them all

inside goblint-cil/src:
dune exec -- ./main.exe test_asm.c --verbose --live_debug --printCilAsIs --out cil.out && cat cil.out

Assembly Context Statements

Each Assembly statement is translated into an instruction. Those instructions need to reference the context of the assembly block. To prevent multiple visits to the same context, context should be implemented as dummy statement without controlflow wich can be referenced by each assembly instruction.
This has to be a reference so it can be mutable.
Fields also may have to be mutable. (location, the rest probably not)