source: Deliverables/D2.2/8051/src/LIN/LINToASM.ml @ 1462

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

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 5.3 KB
Line 
1
2(** This module translates a [LIN] program into a [ASM] program. *)
3
4
5let error_prefix = "LIN to ASM"
6let error s = Error.global_error error_prefix s
7
8
9(* Fetch the labels found in a LIN program. *)
10
11let statement_labels = function
12  | LIN.St_goto lbl
13  | LIN.St_label lbl
14  | LIN.St_cost lbl
15  | LIN.St_condacc lbl -> Label.Set.singleton lbl
16  | _ -> Label.Set.empty
17
18let funct_labels (_, fun_def) = match fun_def with
19  | LIN.F_int stmts ->
20    let f labels stmt = Label.Set.union labels (statement_labels stmt) in
21    List.fold_left f Label.Set.empty stmts
22  | _ -> Label.Set.empty
23
24let prog_labels p =
25  let f labels funct = Label.Set.union labels (funct_labels funct) in
26  List.fold_left f Label.Set.empty p.LIN.functs
27
28
29let size_of_vect_size = function
30  | `Four -> 4
31  | `Seven -> 7
32  | `Eight -> 8
33  | `Eleven -> 11
34  | `Sixteen -> 16
35
36let vect_of_int i size =
37  let i' =
38    if i < 0 then (MiscPottier.pow 2 (size_of_vect_size size)) + i else i in
39  BitVectors.vect_of_int i' size
40
41let byte_of_int i = vect_of_int i `Eight
42let data_of_int i = `DATA (byte_of_int i)
43let data16_of_int i = `DATA16 (vect_of_int i `Sixteen)
44let acc_addr = I8051.reg_addr I8051.a
45
46
47let call_ptr_instrs f1 f2 =
48  [LIN.St_to_acc f1 ;
49   LIN.St_push ;
50   LIN.St_to_acc f2 ;
51   LIN.St_push ;
52   LIN.St_return]
53
54let rec translate_statement glbls_addr set_ra_label = function
55  | LIN.St_goto lbl -> [`Jmp lbl]
56  | LIN.St_label lbl -> [`Label lbl]
57  | LIN.St_comment _ -> []
58  | LIN.St_cost lbl -> [`Cost lbl ; `NOP (* TODO: hack! Need to make the difference between cost labels and regular labels. *)]
59  | LIN.St_int (r, i) ->
60    [`MOV (`U3 (I8051.reg_addr r, data_of_int i))]
61  | LIN.St_pop ->
62    [`POP acc_addr]
63  | LIN.St_push ->
64    [`PUSH acc_addr]
65  | LIN.St_addr x when List.mem_assoc x glbls_addr ->
66    [`MOV (`U4 (`DPTR, data16_of_int (List.assoc x glbls_addr)))]
67  | LIN.St_addr x (* TODO *) ->
68    error ("unknown global " ^ x ^ ".")
69  | LIN.St_from_acc r ->
70    [`MOV (`U3 (I8051.reg_addr r, `A))]
71  | LIN.St_to_acc r ->
72    [`MOV (`U1 (`A, I8051.reg_addr r))]
73  | LIN.St_opaccs I8051.Mul ->
74    [`MUL (`A, `B)]
75  | LIN.St_opaccs I8051.DivuModu ->
76    [`DIV (`A, `B)]
77  | LIN.St_op1 I8051.Cmpl ->
78    [`CPL `A]
79  | LIN.St_op1 I8051.Inc ->
80    [`INC `A]
81  | LIN.St_op2 (I8051.Add, r) ->
82    [`ADD (`A, I8051.reg_addr r)]
83  | LIN.St_op2 (I8051.Addc, r) ->
84    [`ADDC (`A, I8051.reg_addr r)]
85  | LIN.St_op2 (I8051.Sub, r) ->
86    [`SUBB (`A, I8051.reg_addr r)]
87  | LIN.St_op2 (I8051.And, r) ->
88    [`ANL (`U1 (`A, I8051.reg_addr r))]
89  | LIN.St_op2 (I8051.Or, r) ->
90    [`ORL (`U1 (`A, I8051.reg_addr r))]
91  | LIN.St_op2 (I8051.Xor, r) ->
92    [`XRL (`U1 (`A, I8051.reg_addr r))]
93  | LIN.St_clear_carry ->
94    [`CLR `C]
95  | LIN.St_set_carry ->
96    [`SETB `C]
97  | LIN.St_load ->
98    [`MOVX (`U1 (`A, `EXT_IND_DPTR))]
99  | LIN.St_store ->
100    [`MOVX (`U2 (`EXT_IND_DPTR, `A))]
101  | LIN.St_call_id f ->
102    [`Call f]
103  | LIN.St_call_ptr (f1, f2) ->
104    translate_code glbls_addr set_ra_label
105      (LIN.St_call_id set_ra_label :: (call_ptr_instrs f1 f2))
106  | LIN.St_condacc lbl ->
107    [`WithLabel (`JNZ (`Label lbl))]
108  | LIN.St_return ->
109    [`RET]
110
111and translate_code glbls_addr set_ra_label code =
112  List.flatten (List.map (translate_statement glbls_addr set_ra_label) code)
113
114
115let translate_fun_def glbls_addr set_ra_label (id, def) =
116  let code = match def with
117  | LIN.F_int code -> translate_code glbls_addr set_ra_label code
118  | LIN.F_ext ext -> [`NOP] in
119  (`Label id) :: code
120
121(*
122let translate_fun_def glbls_addr (id, def) = match def with
123  | LIN.F_int code -> (`Label id) :: (translate_code glbls_addr code)
124  | LIN.F_ext ext ->
125    error ("potential call to unsupported external " ^ ext.AST.ef_tag ^ ".")
126*)
127
128let fun_set_ra set_ra_label =
129  let size = 0 (* TODO *) in
130  [LIN.St_label set_ra_label ;
131   LIN.St_pop ;
132   LIN.St_from_acc I8051.st1 ;
133   LIN.St_pop ;
134   LIN.St_from_acc I8051.st0 ;
135   LIN.St_int (I8051.a, size) ;
136   LIN.St_op2 (I8051.Add, I8051.st0) ;
137   LIN.St_push ;
138   LIN.St_op2 (I8051.Addc, I8051.st1) ;
139   LIN.St_push ;
140   LIN.St_to_acc I8051.st0 ;
141   LIN.St_push ;
142   LIN.St_to_acc I8051.st1 ;
143   LIN.St_push ;
144   LIN.St_return]
145
146let translate_functs glbls_addr exit_label set_ra_label main functs =
147  let preamble = match main with
148    | None -> []
149    | Some main ->
150      [`MOV (`U3 (`DIRECT (byte_of_int I8051.isp_addr),
151                  data_of_int I8051.isp_init)) ;
152       `Call main ;
153       `Label exit_label ; `Jmp exit_label] in
154(*
155  let fun_set_ra =
156    translate_code glbls_addr set_ra_label (fun_set_ra set_ra_label) in
157*)
158  preamble @ (* fun_set_ra @ *)
159  (List.flatten (List.map (translate_fun_def glbls_addr set_ra_label) functs))
160
161
162let globals_addr l =
163  let f (res, offset) (x, size) = ((x, offset) :: res, offset + size) in
164  fst (List.fold_left f ([], 0) l)
165
166
167(* Translating programs.
168
169   Global variables are associated an offset from the base of the external
170   memory. *)
171
172let translate p =
173  let prog_lbls = prog_labels p in
174  let exit_label = Label.Gen.fresh_prefix prog_lbls "_exit" in
175  let set_ra_label = Label.Gen.fresh_prefix prog_lbls "_set_ra" in
176  let glbls_addr = globals_addr p.LIN.vars in
177  let p =
178    { ASM.ppreamble = p.LIN.vars ;
179      ASM.pexit_label = exit_label ;
180      ASM.pcode =
181        translate_functs glbls_addr exit_label set_ra_label
182          p.LIN.main p.LIN.functs ;
183      ASM.phas_main = p.LIN.main <> None } in
184  ASMInterpret.assembly p
Note: See TracBrowser for help on using the repository browser.