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

Last change on this file was 1542, checked in by tranquil, 8 years ago

merge of indexed labels branch

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_ind_0 (_, l)
120        | LTL.St_ind_inc (_, l)
121        | LTL.St_int (_, _, l)
122        | LTL.St_pop l
123        | LTL.St_push l
124        | LTL.St_addr (_, l)
125        | LTL.St_from_acc (_, l)
126        | LTL.St_to_acc (_, l)
127        | LTL.St_opaccs (_, l)
128        | LTL.St_op1 (_, l)
129        | LTL.St_op2 (_, _, l)
130        | LTL.St_clear_carry l
131        | LTL.St_set_carry l
132        | LTL.St_load l
133        | LTL.St_store l
134        | LTL.St_call_id (_, l)
135        | LTL.St_call_ptr l ->
136
137          visit l
138
139        (* Conditional branch statement. The label that is reached by
140           falling through in [LIN] is [l2], which means that it must be
141           translated first, so that its statements are contiguous with the
142           [LIN] branch statement. The label [l1], on the other hand,
143           becomes the target of a jump, so it is required to exist in the
144           [LIN] code.
145
146           Code for [l1] is generated, if necessary, after we are done dealing
147           with [l2]. If [l1] has already been visited at this point, no code
148           needs be produced, so the second call to visit is made only if [l1]
149           has not been visited yet. *)
150
151        | LTL.St_condacc (l1, l2) ->
152
153          visit l2;
154          require l1;
155          if not (marked l1) then
156            visit l1
157
158        (* Statement without a successor. *)
159
160        (* We would prefer to duplicate, rather than share, these
161           statements. Indeed, it is inefficient to generate a jump towards
162           one of these statements. Unfortunately, it is not easy to achieve
163           this, for two reasons. First, frame deletion is in the way. Second,
164           and worse, we must not generate duplicate labels. Maybe I will find
165           a fix in the future. *)
166
167        | LTL.St_return ->
168
169          ()
170
171    end
172
173end
174
Note: See TracBrowser for help on using the repository browser.