source: Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml @ 740

Last change on this file since 740 was 740, checked in by ayache, 10 years ago

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 6.3 KB
Line 
1
2let n_spaces n = String.make n ' '
3
4
5let print_global n (x, size) =
6  Printf.sprintf "%s\"%s\" [%d]" (n_spaces n) x size
7
8let print_globals n globs =
9  Printf.sprintf "%sglobals:\n%s"
10    (n_spaces n)
11    (List.fold_left (fun s g -> s ^ (print_global (n+2) g) ^ "\n") "" globs)
12
13
14let print_reg = Register.print
15
16let rec print_args args =
17  Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args)
18
19let print_result r = print_reg r
20
21let print_params r =
22  Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_reg r)
23
24let print_locals r =
25  Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_reg r)
26
27
28let print_cmp = function
29  | AST.Cmp_eq -> "eq"
30  | AST.Cmp_ne -> "ne"
31  | AST.Cmp_gt -> "gt"
32  | AST.Cmp_ge -> "ge"
33  | AST.Cmp_lt -> "lt"
34  | AST.Cmp_le -> "le"
35
36let print_cst = function
37  | AST.Cst_int i -> Printf.sprintf "imm_int %d" i
38  | AST.Cst_float f -> Printf.sprintf "imm_float %f" f
39  | AST.Cst_addrsymbol id -> Printf.sprintf "imm_addr \"%s\"" id
40  | AST.Cst_stackoffset off -> Printf.sprintf "imm_addr %d(STACK)" off
41
42let print_op1 = function
43  | AST.Op_cast8unsigned -> "cast8u"
44  | AST.Op_cast8signed -> "cast8"
45  | AST.Op_cast16unsigned -> "cast16u"
46  | AST.Op_cast16signed -> "cast16"
47  | AST.Op_negint -> "negint"
48  | AST.Op_notbool -> "notbool"
49  | AST.Op_notint -> "notint"
50  | AST.Op_negf -> "negf"
51  | AST.Op_absf -> "absf"
52  | AST.Op_singleoffloat -> "singleoffloat"
53  | AST.Op_intoffloat -> "intoffloat"
54  | AST.Op_intuoffloat -> "intuoffloat"
55  | AST.Op_floatofint -> "floatofint"
56  | AST.Op_floatofintu -> "floatofintu"
57  | AST.Op_id -> "id"
58  | AST.Op_ptrofint -> "ptrofint"
59  | AST.Op_intofptr -> "intofptr"
60
61let print_op2 = function
62  | AST.Op_add -> "add"
63  | AST.Op_sub -> "sub"
64  | AST.Op_mul -> "mul"
65  | AST.Op_div -> "div"
66  | AST.Op_divu -> "divu"
67  | AST.Op_mod -> "mod"
68  | AST.Op_modu -> "modu"
69  | AST.Op_and -> "and"
70  | AST.Op_or -> "or"
71  | AST.Op_xor -> "xor"
72  | AST.Op_shl -> "shl"
73  | AST.Op_shr -> "shr"
74  | AST.Op_shru -> "shru"
75  | AST.Op_addf -> "addf"
76  | AST.Op_subf -> "subf"
77  | AST.Op_mulf -> "mulf"
78  | AST.Op_divf -> "divf"
79  | AST.Op_cmp cmp -> print_cmp cmp
80  | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u"
81  | AST.Op_cmpf cmp -> (print_cmp cmp) ^ "f"
82  | AST.Op_addp -> "addp"
83  | AST.Op_subp -> "subp"
84  | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p"
85
86
87let print_addressing = function
88  | RTLabs.Aindexed off -> Printf.sprintf "%d" off
89  | RTLabs.Aindexed2 -> "add"
90  | RTLabs.Aglobal (id, off) -> Printf.sprintf "%d(\"%s\")" off id
91  | RTLabs.Abased (id, off) -> Printf.sprintf "add, %d(\"%s\")" off id
92  | RTLabs.Ainstack off -> Printf.sprintf "%d(STACK)" off
93
94
95let rec print_table = function
96  | [] -> ""
97  | [lbl] -> lbl
98  | lbl :: tbl -> lbl ^ ", " ^ (print_table tbl)
99
100
101let print_statement = function
102  | RTLabs.St_skip lbl -> "--> " ^ lbl
103  | RTLabs.St_cost (cost_lbl, lbl) ->
104      Printf.sprintf "emit %s --> %s" cost_lbl lbl
105  | RTLabs.St_cst (destr, cst, lbl) ->
106      Printf.sprintf "imm %s, %s --> %s"
107        (print_reg destr)
108        (print_cst cst)
109        lbl
110  | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
111      Printf.sprintf "%s %s, %s --> %s"
112        (print_op1 op1)
113        (print_reg destr)
114        (print_reg srcr)
115        lbl
116  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
117      Printf.sprintf "%s %s, %s, %s --> %s"
118        (print_op2 op2)
119        (print_reg destr)
120        (print_reg srcr1)
121        (print_reg srcr2)
122        lbl
123  | RTLabs.St_load (q, mode, args, destr, lbl) ->
124      Printf.sprintf "load %s, %s, %s, %s --> %s"
125        (Memory.string_of_quantity q)
126        (print_addressing mode)
127        (print_args args)
128        (print_reg destr)
129        lbl
130  | RTLabs.St_store (q, mode, args, srcr, lbl) ->
131      Printf.sprintf "store %s, %s, %s, %s --> %s"
132        (Memory.string_of_quantity q)
133        (print_addressing mode)
134        (print_args args)
135        (print_reg srcr)
136        lbl
137  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
138      Printf.sprintf "call \"%s\", %s, %s: %s --> %s"
139        f
140        (print_params args)
141        (print_reg res)
142        (Primitive.print_sig sg)
143        lbl
144  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
145      Printf.sprintf "call_ptr %s, %s, %s: %s --> %s"
146        (print_reg f)
147        (print_params args)
148        (print_reg res)
149        (Primitive.print_sig sg)
150        lbl
151  | RTLabs.St_tailcall_id (f, args, sg) ->
152      Printf.sprintf "tailcall \"%s\", %s: %s"
153        f
154        (print_params args)
155        (Primitive.print_sig sg)
156  | RTLabs.St_tailcall_ptr (f, args, sg) ->
157      Printf.sprintf "tailcall_ptr \"%s\", %s: %s"
158        (print_reg f)
159        (print_params args)
160        (Primitive.print_sig sg)
161  | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
162      Printf.sprintf "%s --> %s, %s"
163        (print_cst cst)
164        lbl_true
165        lbl_false
166  | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
167      Printf.sprintf "%s %s --> %s, %s"
168        (print_op1 op1)
169        (print_reg srcr)
170        lbl_true
171        lbl_false
172  | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
173      Printf.sprintf "%s %s, %s --> %s, %s"
174        (print_op2 op2)
175        (print_reg srcr1)
176        (print_reg srcr2)
177        lbl_true
178        lbl_false
179  | RTLabs.St_jumptable (r, tbl) ->
180      Printf.sprintf "j_tbl %s --> %s"
181        (print_reg r)
182        (print_table tbl)
183  | RTLabs.St_return r -> Printf.sprintf "return %s" (print_reg r)
184
185
186let print_graph n c =
187  let f lbl stmt s =
188    Printf.sprintf "%s%s: %s\n%s"
189      (n_spaces n)
190      lbl
191      (print_statement stmt)
192      s in
193  Label.Map.fold f c ""
194
195
196let print_internal_decl n f def =
197
198  Printf.sprintf
199    "%s\"%s\"%s: %s\n%slocals: %s\n%spointers: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
200    (n_spaces n)
201    f
202    (print_params def.RTLabs.f_params)
203    (Primitive.print_sig def.RTLabs.f_sig)
204    (n_spaces (n+2))
205    (print_locals def.RTLabs.f_locals)
206    (n_spaces (n+2))
207    (print_locals def.RTLabs.f_ptrs)
208    (n_spaces (n+2))
209    (print_result def.RTLabs.f_result)
210    (n_spaces (n+2))
211    def.RTLabs.f_stacksize
212    (n_spaces (n+2))
213    def.RTLabs.f_entry
214    (n_spaces (n+2))
215    def.RTLabs.f_exit
216    (print_graph (n+2) def.RTLabs.f_graph)
217
218
219let print_external_decl n f def =
220  Printf.sprintf "%sextern \"%s\": %s\n"
221    (n_spaces n)
222    f
223    (Primitive.print_sig def.AST.ef_sig)
224
225
226let print_fun_decl n (f, def) = match def with
227  | RTLabs.F_int def -> print_internal_decl n f def
228  | RTLabs.F_ext def -> print_external_decl n f def
229
230let print_fun_decls n functs =
231  List.fold_left (fun s f -> s ^ (print_fun_decl n f) ^ "\n\n") ""
232    functs
233
234
235let print_program p =
236  Printf.sprintf "program:\n\n\n%s\n\n%s"
237    (print_globals 2 p.RTLabs.vars)
238    (print_fun_decls 2 p.RTLabs.functs)
Note: See TracBrowser for help on using the repository browser.