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

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

merge of indexed labels branch

File size: 3.8 KB
RevLine 
[486]1(* This module provides a translation of LTL programs to LIN programs. *)
2
3(* Adapted from Pottier's PP compiler *)
4
5(* ------------------------------------------------------------------------- *)
6
7(* [translate_statement] translates an [LTL] statement into a [LIN]
8   statement. *)
9
10let translate_statement = function
11
12  (* Because [Branch.compress] has been called before, no [St_skip]
13     statement can be reached. *)
14
15  | LTL.St_skip lbl ->
16    LIN.St_goto lbl
17
18  (* Sequential statements. *)
19
20  | LTL.St_comment (s, _) ->
21    LIN.St_comment s
22  | LTL.St_cost (lbl, _) ->
23    LIN.St_cost lbl
[1542]24  | LTL.St_ind_0 (i, _) ->
25    LIN.St_ind_0 i
26  | LTL.St_ind_inc (i, _) ->
27    LIN.St_ind_inc i
[486]28  | LTL.St_int (r, i, _) ->
29    LIN.St_int (r, i)
30  | LTL.St_addr (x, _) ->
31    LIN.St_addr x
32  | LTL.St_pop _ ->
33    LIN.St_pop
34  | LTL.St_push _ ->
35    LIN.St_push
36  | LTL.St_clear_carry _ ->
37    LIN.St_clear_carry
[818]38  | LTL.St_set_carry _ ->
39    LIN.St_set_carry
[486]40  | LTL.St_from_acc (r, _) ->
41    LIN.St_from_acc (r)
42  | LTL.St_to_acc (r, _) ->
43    LIN.St_to_acc r
44  | LTL.St_opaccs (opaccs, _) ->
45    LIN.St_opaccs opaccs
46  | LTL.St_op1 (op1, _) ->
47    LIN.St_op1 op1
48  | LTL.St_op2 (op2, r, _) ->
49    LIN.St_op2 (op2, r)
50  | LTL.St_load _ ->
51    LIN.St_load
52  | LTL.St_store _ ->
53    LIN.St_store
54  | LTL.St_call_id (f, _) ->
55    LIN.St_call_id f
[1488]56  | LTL.St_call_ptr _ ->
57    LIN.St_call_ptr
[486]58
59  (* Conditional branch statement. In [LIN], control implicitly
60     falls through to the second successor, so only the first
61     successor is explicitly mentioned in the statement. *)
62
63  | LTL.St_condacc (lbl_true, _) ->
64    LIN.St_condacc lbl_true
65
66  (* Statement without a successor. *)
67
68  | LTL.St_return ->
69    LIN.St_return
70
71(* ------------------------------------------------------------------------- *)
72
73(* [translate entry graph] turns an [LTL] control flow graph into
74   a [LIN] sequence of statements. *)
75
76let translate_graph entry graph =
77
78  (* Keep track of the labels that have been visited (initially none), of the
79     labels that must exist within the [LIN] code (initially only the graph's
80     entry point) and of the list of [LIN] statements that are being
81     generated (initially empty). Statements are held in the list in reverse
82     order, for efficiency. The list is reversed once generation is over. *)
83
84  let visited, required, statements =
85    ref Label.Set.empty, ref (Label.Set.singleton entry), ref []
86  in
87
88  (* Instantiate the functor. *)
89
90  let module V = LTLToLINI.Visit (struct
91    let fetch label =
92      Label.Map.find label graph
93    let translate_statement =
94      translate_statement
95    let generate statement =
96      statements := statement :: !statements
97    let require label =
98      required := Label.Set.add label !required
99    let mark label =
100      visited := Label.Set.add label !visited
101    let marked label =
102      Label.Set.mem label !visited
103  end) in
104
105  (* Traverse the control flow graph. *)
106
107  V.visit entry;
108
109  (* Now, get rid of the labels that do not need to exist. Also,
110     reverse the list to re-establish the correct order. *)
111
112  List.filter (function
113    | LIN.St_label l ->
114        Label.Set.mem l !required
115    | _ ->
116        true
117  ) (List.rev !statements)
118
119(* ------------------------------------------------------------------------- *)
120
121(* Extend the translation to procedures and programs. *)
122
123let translate_internal int_fun =
124  (* Compress the graph to eliminate gotos (St_skip) statements. *)
125  let entry, graph = Branch.compress int_fun.LTL.f_entry int_fun.LTL.f_graph in
126  translate_graph entry graph
127
128let translate_funct (name, def) =
129  let def' = match def with
130    | LTL.F_int def -> LIN.F_int (translate_internal def)
131    | LTL.F_ext def -> LIN.F_ext def in
132  (name, def')
133
134let translate (p : LTL.program) : LIN.program =
135  { LIN.vars = p.LTL.vars;
136    LIN.functs = List.map translate_funct p.LTL.functs ;
137    LIN.main = p.LTL.main }
Note: See TracBrowser for help on using the repository browser.