src/LTL/LTLToLINI.ml

   1 (* Adapted from Pottier's PP compiler *)
   2
   3 open MIPSOps
   4
   5 (* ------------------------------------------------------------------------- *)
   6
   7 (* The functor [Visit] implements the core of the translation of
   8    [LTL] to [LIN]. *)
   9
  10 module Visit (S : sig
  11
  12   (* [fetch l] is the statement found at label [l] in the source
  13      program. *)
  14
  15   val fetch: Label.t -> LTL.statement
  16
  17   (* [translate_statement stmt] translates the [LTL] statement [stmt] to
  18      a [LIN] statement. [LTL] statements that have one explicit
  19      successor are turned into [LIN] statements with an implicit
  20      successor. [LTL] statements that have two explicit successors
  21      are turned into [LIN] statements where the first successor is
  22      explicit and the second successor is implicit. *)
  23
  24   val translate_statement: LTL.statement -> LIN.statement
  25
  26   (* [generate stmt] generates statement [stmt]. Statements are
  27      generated sequentially. *)
  28
  29   val generate: LIN.statement -> unit
  30
  31   (* [require l] records the fact that the label [l] should explicitly
  32      exist in the [LIN] program. It must be used whenever a [LIN]
  33      branch statement is issued. *)
  34
  35   val require: Label.t -> unit
  36
  37   (* [mark l] marks the label [l]. [marked l] tells whether [l] is
  38      marked. *)
  39
  40   val mark: Label.t -> unit
  41   val marked: Label.t -> bool
  42
  43 end) = struct
  44
  45   open S
  46
  47   let rec visit l =
  48
  49     if marked l then begin
  50
  51       (* Label [l] has been visited before. This implies that an [St_label l]
  52          statement has been issued already. We must now generate an
  53          [St_goto] statement that transfers control to this place. Because
  54          [l] is the target of a branch statement, we require it to exist
  55          in the [LIN] code. *)
  56
  57       require l;
  58       generate (LIN.St_goto l)
  59
  60     end
  61     else begin
  62
  63       (* Label [l] has never been visited before. First, record that it
  64          now has been visited, so as to avoid looping. *)
  65
  66       mark l;
  67
  68       (* Then, generate an [St_label l] statement. This statement
  69          will be useless if [l] turns out not to be the target of a
  70          branch: this is taken care of later. *)
  71
  72       generate (LIN.St_label l);
  73
  74       (* Fetch the statement found at label [l] in the source program. *)
  75
  76       let statement = fetch l in
  77
  78       (* As an optional optimization, check if this is a conditional branch
  79          whose implicit successor has been visited before and whose explicit
  80          successor has not. In that case, if we did nothing special, we would
  81          produce a conditional branch immediately followed with an
  82          unconditional one, like this:
  83
  84                 bgtz  $t1, find24
  85                 j     find42
  86                 find24:
  87                 ...
  88
  89          This can be avoided simply by reversing the condition:
  90
  91                 blez  $t1, find42
  92                 ...
  93
  94          *)
  95
  96       (* But in fact, there is only a unique conditional branch statement in
  97          LTL for the 8051, so this is optimization is not used. *)
  98
  99       (* Translate the statement. *)
 100
 101       generate (translate_statement statement);
 102
 103       (* Note that [translate_statement] never produces an [St_goto]
 104          statement. As a result, the code above never generates an [St_label]
 105          statement immediately followed with an [St_goto] statement. This
 106          proves that we never generate a (conditional or unconditional) branch
 107          towards an [St_goto] statement. *)
 108
 109       (* There now remains to visit the statement's successors. *)
 110
 111       match statement with
 112
 113         (* Sequential statements. There is only one successor, with implicit
 114            fallthrough. *)
 115
 116         | LTL.St_skip l
 117         | LTL.St_comment (_, l)
 118         | LTL.St_cost (_, l)
 119         | LTL.St_int (_, _, l)
 120         | LTL.St_pop l
 121         | LTL.St_push l
 122         | LTL.St_addr (_, l)
 123         | LTL.St_from_acc (_, l)
 124         | LTL.St_to_acc (_, l)
 125         | LTL.St_opaccs (_, l)
 126         | LTL.St_op1 (_, l)
 127         | LTL.St_op2 (_, _, l)
 128         | LTL.St_clear_carry l
 129         | LTL.St_set_carry l
 130         | LTL.St_load l
 131         | LTL.St_store l
 132         | LTL.St_call_id (_, l)
 133         | LTL.St_call_ptr l ->
 134
 135           visit l
 136
 137         (* Conditional branch statement. The label that is reached by
 138            falling through in [LIN] is [l2], which means that it must be
 139            translated first, so that its statements are contiguous with the
 140            [LIN] branch statement. The label [l1], on the other hand,
 141            becomes the target of a jump, so it is required to exist in the
 142            [LIN] code.
 143
 144            Code for [l1] is generated, if necessary, after we are done dealing
 145            with [l2]. If [l1] has already been visited at this point, no code
 146            needs be produced, so the second call to visit is made only if [l1]
 147            has not been visited yet. *)
 148
 149         | LTL.St_condacc (l1, l2) ->
 150
 151           visit l2;
 152           require l1;
 153           if not (marked l1) then
 154             visit l1
 155
 156         (* Statement without a successor. *)
 157
 158         (* We would prefer to duplicate, rather than share, these
 159            statements. Indeed, it is inefficient to generate a jump towards
 160            one of these statements. Unfortunately, it is not easy to achieve
 161            this, for two reasons. First, frame deletion is in the way. Second,
 162            and worse, we must not generate duplicate labels. Maybe I will find
 163            a fix in the future. *)
 164
 165         | LTL.St_return ->
 166
 167           ()
 168
 169     end
 170
 171 end
 172