Sun Mar 14 19:21:09 CET 2010

Verifying the ad-hoc PIC18 code generator

      PROBLEM: verify the correctness an ad-hoc collection of
               reduction rules (pattern matching).

The solution I see is the use of an explicit representation of target
machine semantics.  I.e. run the generated code in a simulator and
hook it up to a test system that tries to provide full coverage.

My main point of confusion is not explicitly recognizing all these
language levels involved.  Each level's data is next level's function;
between every level lies an interpreter.

      FUNCTION               DATA
 rep  Scheme functions       Scheme syntax objects
  1)  Forth prefix parsers   concatenative syntax
  2)  Macro functions        machine assembly code (-> binary machine code)
  3)  Machine state TX       machine state

Level 1) can largely be ignored: it is a trivial preprocessing step to
relate traditional Forth to the functional macro model.

Level 2) is where the beef is.  This part contains a lot of
information (transformation rules) as it encodes semantics of the
machine in an indirect way, i.e. preserving an approximation of the
semantics of machine code.

Level 3) is given: the concrete semantics of the target machine can be
used to build a simulator in Scheme.

The point is verification of the error-prone creative hackery step 2)
by making an interpretation arrow from concatenative syntax (the data
of 1) to an abstract (function) domain that can somehow be related to
the translation that the compiler makes from data in 1) to the
function domain of level 3).

The trick is then to find a collection of input code that produces
programs that fire the optimization rules in different ways.

         COMPILER (w/o prefix parser)

                        asm stx
         conc stx  =====>  | macro     machine
                           | code       state
                           V              |
                        asm stx   =====>  | machine state tx


                      vm state
         conc stx  ===>  | vm state tx
                      vm state

A diagram that relates the interpretation (=>) and function (->)
relations.  Interpretation maps syntax (data) to semantics (function).