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

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

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