[<<][compsci][>>][..]

Sun Mar 7 22:56:47 CET 2010

Writing compilers

The basic idea is that a compiler is a function, i.e. implemented by a
collection of rewrite rules, that relates one syntactic domain to
another.

In order to verify correctness of this ``arrow'' the language needs a
formal model - another arrow - to compare it with.

                comp
    language   ----->  machine code

       |                   |
       | definitional      | machine code
       | interpreter       | interpreter
       v                   v

   abstract domain (i.e. Haskell functions)

That's my idea.  How does [1] do it?  In each pass (14 passes and 8
intermediate languages) the semantics of the language is defined, and
the transformation is proven to preserve the semantics.

I am only interested in one pass: the reductions used in the PIC18
instruction selection.  It looks like I need a Hoare logic[2] for the
machine opcodes, i.e. some kind of typing rules for the state
transitions, and how they can be composed.

So, my question is: in the spirit of tagless interpreters, is it
possible to write down the Staapl PIC18 reduction rules such that:

  * PIC18 Instruction semantics can be encoded in the type as much as
    possible.  I.e. data dependencies.

  * Remaining semantics (i.e. add or sub) is encoded in behaviour, and
    can be verified by quickcheck.

Doing this in Scheme as an alternative to encoding it in Haskell/OCaml
type system is probably also possible, but I would need to make a
checker/inferencer.


[1] http://compcert.inria.fr/doc/index.html
[2] http://en.wikipedia.org/wiki/Hoare_logic

[Reply][About]

[<<][compsci][>>][..]