source: Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml @ 1488

Last change on this file since 1488 was 1488, checked in by ayache, 8 years ago

Function pointers in D2.2/8051. Bugged for now.

File size: 4.9 KB
Line 
1(* Adapted from Pottier's PP compiler *)
2
3open MIPSOps
4
5(* ------------------------------------------------------------------------- *)
6
7(* The functor [Visit] implements the core of the translation of
8   [LTL] to [LIN]. *)
9
10module 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
43end) = 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
171end
172
Note: See TracBrowser for help on using the repository browser.