Lab Session 6 - Implementing a Static Type Checker for a fragment of C

The goal of this lab is to implement the static typing for a small fragment of C, called mini-C.
The syntax and typing rules are given in the accompanying PDF description.

Provided Code

The abstract syntax tree, lexer, parser, main file and tests are already implemented: mini-c.tar.gz

It is important to read and understand the abstract syntax of mini-C, that is files Ptree.mli (parsed trees) and Ttree.mli (typed trees).

A Makefile is also provided, which calls dune. The executable is minic.exe. It expects a file with extension .c on the command line, possibly with options --debug, --parse-only, and --type-only.

If a lexical or syntax error is detected, it is reported and the program exits with code 1.

If the parsing is successful and option --parse-only is on the command line, then the program exits with code 0.

Lab Assignment

Implement the type checking in file typing.ml, as a function program that takes a Ptree.file as input and returns a Ttree.file.

The file typing.ml provides the skeleton of the typechecking with explanations and comments and contains 12 implementation tasks.

If a type error is detected, it is signaled using exception Error defined in typing.ml, with a suitable message string. This exception is caught in main.ml and displayed as

     error: ... your message here ...

and the program exits with code 1.

Indications

It is strongly advised to proceed step by step, with systematic testing. As a first goal, consider a C program as simple as

int main() { return 0; }

This means you only have to consider integer literals in expressions and return statements.

In the provided tarball, the command make compiles minic.exe and then runs it on file test.c (also provided). So you simply have to modify test.c as you make progress.

Tests

Some tests are provided in the /tests folder in the tar.gz file and where

C files organized in various categories:

  syntax/bad/    rejected at parsing
  syntax/good/   accepted at parsing
  typing/bad/    rejected at type checking
  typing/good/   accepted at type checking

run make typing-tests to run your compiler on these files. You should get the following:

> make typing-tests
dune build minic.exe
cd  ./tests ; \
	./test -2 ../minic.exe
Test de ../minic.exe

11 states, 374 transitions, table size 1562 bytes
1401 additional bytes used for bindings

Part 2: Type-checking
bad .................................
good ......
Typing  : 39/39 : 100%

back to the main page