1 | |
---|
2 | (** This module provides folding functions over the constructors of the |
---|
3 | [Clight]'s AST. *) |
---|
4 | |
---|
5 | |
---|
6 | let ctype_subs = function |
---|
7 | | Clight.Tvoid | Clight.Tint _ | Clight.Tfloat _ | Clight.Tcomp_ptr _ -> [] |
---|
8 | | Clight.Tpointer ctype | Clight.Tarray (ctype, _) -> [ctype] |
---|
9 | | Clight.Tfunction (args, res) -> args @ [res] |
---|
10 | | Clight.Tstruct (_, fields) | Clight.Tunion (_, fields) -> |
---|
11 | List.map snd fields |
---|
12 | |
---|
13 | let ctype_fill_subs ctype sub_ctypes = match ctype, sub_ctypes with |
---|
14 | | Clight.Tvoid, _ | Clight.Tint _, _ | Clight.Tfloat _, _ |
---|
15 | | Clight.Tcomp_ptr _, _ -> ctype |
---|
16 | | Clight.Tpointer _, ctype :: _ -> Clight.Tpointer ctype |
---|
17 | | Clight.Tarray (_, size), ctype :: _ -> Clight.Tarray (ctype, size) |
---|
18 | | Clight.Tfunction _, _ -> |
---|
19 | let (args, res) = MiscPottier.split_last sub_ctypes in |
---|
20 | Clight.Tfunction (args, res) |
---|
21 | | Clight.Tstruct (name, fields), _ -> |
---|
22 | let fields = List.map2 (fun (x, _) ctype -> (x, ctype)) fields sub_ctypes in |
---|
23 | Clight.Tstruct (name, fields) |
---|
24 | | Clight.Tunion (name, fields), _ -> |
---|
25 | let fields = List.map2 (fun (x, _) ctype -> (x, ctype)) fields sub_ctypes in |
---|
26 | Clight.Tunion (name, fields) |
---|
27 | | _ -> assert false (* wrong arguments, do not use on these values *) |
---|
28 | |
---|
29 | let rec ctype f t = |
---|
30 | let sub_ctypes_res = List.map (ctype f) (ctype_subs t) in |
---|
31 | f t sub_ctypes_res |
---|
32 | |
---|
33 | |
---|
34 | let expr_subs = function |
---|
35 | | Clight.Expr (expr_descr, ctype) -> ([ctype], [expr_descr]) |
---|
36 | |
---|
37 | let expr_descr_subs = function |
---|
38 | | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _ -> ([], []) |
---|
39 | | Clight.Ederef e | Clight.Eaddrof e | Clight.Eunop (_, e) |
---|
40 | | Clight.Efield (e, _) -> ([], [e]) |
---|
41 | | Clight.Ebinop (_, e1, e2) | Clight.Eandbool (e1, e2) |
---|
42 | | Clight.Eorbool (e1, e2) -> ([], [e1 ; e2]) |
---|
43 | | Clight.Ecast (ctype, e) -> ([ctype], [e]) |
---|
44 | | Clight.Econdition (e1, e2, e3) -> ([], [e1 ; e2 ; e3]) |
---|
45 | | Clight.Esizeof ctype -> ([ctype], []) |
---|
46 | | Clight.Ecost (_, e) -> ([], [e]) |
---|
47 | | Clight.Ecall (_, e1, e2) -> ([], [e1 ; e2]) |
---|
48 | |
---|
49 | let expr_fill_subs e sub_ctypes sub_expr_descrs = |
---|
50 | match e, sub_ctypes, sub_expr_descrs with |
---|
51 | | Clight.Expr _, ctype :: _, expr_descr :: _ -> |
---|
52 | Clight.Expr (expr_descr, ctype) |
---|
53 | | _ -> assert false (* wrong arguments, do not use on these values *) |
---|
54 | |
---|
55 | let expr_descr_fill_subs e sub_ctypes sub_exprs = |
---|
56 | match e, sub_ctypes, sub_exprs with |
---|
57 | | Clight.Econst_int _, _, _ | Clight.Econst_float _, _, _ |
---|
58 | | Clight.Evar _, _, _ -> e |
---|
59 | | Clight.Ederef _, _, e :: _ -> Clight.Ederef e |
---|
60 | | Clight.Eaddrof _, _, e :: _ -> Clight.Eaddrof e |
---|
61 | | Clight.Eunop (unop, _), _, e :: _ -> Clight.Eunop (unop, e) |
---|
62 | | Clight.Ebinop (binop, _, _), _, e1 :: e2 :: _ -> |
---|
63 | Clight.Ebinop (binop, e1, e2) |
---|
64 | | Clight.Ecast _, ctype :: _, e :: _ -> Clight.Ecast (ctype, e) |
---|
65 | | Clight.Econdition _, _, e1 :: e2 :: e3 :: _ -> |
---|
66 | Clight.Econdition (e1, e2, e3) |
---|
67 | | Clight.Eandbool (_, _), _, e1 :: e2 :: _ -> |
---|
68 | Clight.Eandbool (e1, e2) |
---|
69 | | Clight.Eorbool (_, _), _, e1 :: e2 :: _ -> |
---|
70 | Clight.Eorbool (e1, e2) |
---|
71 | | Clight.Esizeof _, ctype :: _, _ -> Clight.Esizeof ctype |
---|
72 | | Clight.Efield (_, field_name), _, e :: _ -> Clight.Efield (e, field_name) |
---|
73 | | Clight.Ecost (lbl, _), _, e :: _ -> Clight.Ecost (lbl, e) |
---|
74 | | Clight.Ecall (id, _, _), _, e1 :: e2 :: _ -> Clight.Ecall (id, e1, e2) |
---|
75 | | _ -> assert false (* wrong arguments, do not use on these values *) |
---|
76 | |
---|
77 | let expr_fill_exprs (Clight.Expr (ed, t)) exprs = |
---|
78 | let (sub_ctypes, _) = expr_descr_subs ed in |
---|
79 | let ed = expr_descr_fill_subs ed sub_ctypes exprs in |
---|
80 | Clight.Expr (ed, t) |
---|
81 | |
---|
82 | let rec expr f_ctype f_expr f_expr_descr e = |
---|
83 | let (sub_ctypes, sub_expr_descrs) = expr_subs e in |
---|
84 | let sub_expr_descrs_res = |
---|
85 | List.map (expr_descr f_ctype f_expr f_expr_descr) sub_expr_descrs in |
---|
86 | let sub_ctypes_res = List.map (ctype f_ctype) sub_ctypes in |
---|
87 | f_expr e sub_ctypes_res sub_expr_descrs_res |
---|
88 | |
---|
89 | and expr_descr f_ctype f_expr f_expr_descr e = |
---|
90 | let (sub_ctypes, sub_exprs) = expr_descr_subs e in |
---|
91 | let sub_exprs_res = |
---|
92 | List.map (expr f_ctype f_expr f_expr_descr) sub_exprs in |
---|
93 | let sub_ctypes_res = List.map (ctype f_ctype) sub_ctypes in |
---|
94 | f_expr_descr e sub_ctypes_res sub_exprs_res |
---|
95 | |
---|
96 | |
---|
97 | let expr_subs2 e = |
---|
98 | let (_, expr_descrs) = expr_subs e in |
---|
99 | let l = List.map expr_descr_subs expr_descrs in |
---|
100 | List.flatten (List.map snd l) |
---|
101 | |
---|
102 | let rec expr2 f e = f e (List.map (expr2 f) (expr_subs2 e)) |
---|
103 | |
---|
104 | |
---|
105 | let rec labeled_statements_subs = function |
---|
106 | | Clight.LSdefault stmt -> [stmt] |
---|
107 | | Clight.LScase (_, stmt, lbl_stmts) -> |
---|
108 | stmt :: (labeled_statements_subs lbl_stmts) |
---|
109 | |
---|
110 | let statement_subs = function |
---|
111 | | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None |
---|
112 | | Clight.Sgoto _ -> ([], []) |
---|
113 | | Clight.Sassign (e1, e2) -> ([e1 ; e2], []) |
---|
114 | | Clight.Scall (None, e, args) -> (e :: args, []) |
---|
115 | | Clight.Scall (Some e1, e2, args) -> (e1 :: e2 :: args, []) |
---|
116 | | Clight.Ssequence (stmt1, stmt2) -> ([], [stmt1 ; stmt2]) |
---|
117 | | Clight.Sifthenelse (e, stmt1, stmt2) -> ([e], [stmt1 ; stmt2]) |
---|
118 | | Clight.Swhile (_, e, stmt) | Clight.Sdowhile (_, e, stmt) -> ([e], [stmt]) |
---|
119 | | Clight.Sfor (_, stmt1, e, stmt2, stmt3) -> ([e], [stmt1 ; stmt2 ; stmt3]) |
---|
120 | | Clight.Sreturn (Some e) -> ([e], []) |
---|
121 | | Clight.Sswitch (e, lbl_stmts) -> ([e], labeled_statements_subs lbl_stmts) |
---|
122 | | Clight.Slabel (_, stmt) | Clight.Scost (_, stmt) -> ([], [stmt]) |
---|
123 | |
---|
124 | let statement_sub_exprs stmt = fst (statement_subs stmt) |
---|
125 | |
---|
126 | let rec labeled_statements_fill_subs lbl_stmts sub_statements = |
---|
127 | match lbl_stmts, sub_statements with |
---|
128 | | Clight.LSdefault _, stmt :: _ -> Clight.LSdefault stmt |
---|
129 | | Clight.LScase (i, _, lbl_stmts), stmt :: sub_statements -> |
---|
130 | Clight.LScase (i, stmt, |
---|
131 | labeled_statements_fill_subs lbl_stmts sub_statements) |
---|
132 | | _ -> assert false (* wrong arguments, do not use on these values *) |
---|
133 | |
---|
134 | let statement_fill_subs statement sub_exprs sub_statements = |
---|
135 | match statement, sub_exprs, sub_statements with |
---|
136 | | Clight.Sskip, _, _ | Clight.Sbreak, _, _ | Clight.Scontinue, _, _ |
---|
137 | | Clight.Sreturn None, _, _ | Clight.Sgoto _, _, _ -> statement |
---|
138 | | Clight.Sassign _, e1 :: e2 :: _, _ -> Clight.Sassign (e1, e2) |
---|
139 | | Clight.Scall (None, _, _), e :: args, _ -> |
---|
140 | Clight.Scall (None, e, args) |
---|
141 | | Clight.Scall (Some _, _, _), e1 :: e2 :: args, _ -> |
---|
142 | Clight.Scall (Some e1, e2, args) |
---|
143 | | Clight.Ssequence _, _, stmt1 :: stmt2 :: _ -> |
---|
144 | Clight.Ssequence (stmt1, stmt2) |
---|
145 | | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ -> |
---|
146 | Clight.Sifthenelse (e, stmt1, stmt2) |
---|
147 | | Clight.Swhile (i, _, _), e :: _, stmt :: _ -> |
---|
148 | Clight.Swhile (i, e, stmt) |
---|
149 | | Clight.Sdowhile (i, _, _), e :: _, stmt :: _ -> |
---|
150 | Clight.Sdowhile (i, e, stmt) |
---|
151 | | Clight.Sfor (i, _, _, _, _), e :: _, stmt1 :: stmt2 :: stmt3 :: _ -> |
---|
152 | Clight.Sfor (i, stmt1, e, stmt2, stmt3) |
---|
153 | | Clight.Sreturn (Some _), e :: _, _ -> Clight.Sreturn (Some e) |
---|
154 | | Clight.Sswitch (_, lbl_stmts), e :: _, _ -> |
---|
155 | Clight.Sswitch (e, labeled_statements_fill_subs lbl_stmts sub_statements) |
---|
156 | | Clight.Slabel (lbl, _), _, stmt :: _ -> Clight.Slabel (lbl, stmt) |
---|
157 | | Clight.Scost (lbl, _), _, stmt :: _ -> Clight.Scost (lbl, stmt) |
---|
158 | | _ -> assert false (* wrong arguments, do not use on these values *) |
---|
159 | |
---|
160 | let rec statement f_ctype f_expr f_expr_descr f_statement stmt = |
---|
161 | let (sub_exprs, sub_stmts) = statement_subs stmt in |
---|
162 | let sub_exprs_res = List.map (expr f_ctype f_expr f_expr_descr) sub_exprs in |
---|
163 | let sub_stmts_res = |
---|
164 | List.map (statement f_ctype f_expr f_expr_descr f_statement) sub_stmts in |
---|
165 | f_statement stmt sub_exprs_res sub_stmts_res |
---|
166 | |
---|
167 | let rec statement2 f_expr f_statement stmt = |
---|
168 | let (sub_exprs, sub_stmts) = statement_subs stmt in |
---|
169 | let sub_exprs_res = List.map (expr2 f_expr) sub_exprs in |
---|
170 | let sub_stmts_res = List.map (statement2 f_expr f_statement) sub_stmts in |
---|
171 | f_statement stmt sub_exprs_res sub_stmts_res |
---|