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

Last change on this file since 740 was 740, checked in by ayache, 9 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.