1 | |
---|
2 | (** [simplify p] removes unnecessary casts in the Clight program [p]. |
---|
3 | |
---|
4 | Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char] |
---|
5 | will be transformed into [x + y]. Primitive operations are thus supposed to |
---|
6 | be polymorphic, but working only on homogene types. *) |
---|
7 | |
---|
8 | let f_ctype ctype _ = ctype |
---|
9 | |
---|
10 | (* |
---|
11 | let f_expr = ClightFold.expr_fill_subs |
---|
12 | |
---|
13 | let f_expr_descr e sub_ctypes_res sub_exprs_res = |
---|
14 | match e, sub_exprs_res with |
---|
15 | | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _), |
---|
16 | Clight.Expr |
---|
17 | (Clight.Eunop |
---|
18 | (unop, |
---|
19 | Clight.Expr |
---|
20 | (Clight.Ecast |
---|
21 | (Clight.Tint (Clight.I32, _), |
---|
22 | (Clight.Expr (_, Clight.Tint (Clight.I8, signedness2)) as e)), |
---|
23 | _)), |
---|
24 | _) :: _ when signedness1 = signedness2 -> |
---|
25 | Clight.Eunop (unop, e) |
---|
26 | | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _), |
---|
27 | Clight.Expr |
---|
28 | (Clight.Ebinop |
---|
29 | (binop, |
---|
30 | Clight.Expr |
---|
31 | (Clight.Ecast |
---|
32 | (Clight.Tint (Clight.I32, _), |
---|
33 | (Clight.Expr (_, |
---|
34 | Clight.Tint (Clight.I8, signedness2)) as e1)), |
---|
35 | _), |
---|
36 | Clight.Expr |
---|
37 | (Clight.Ecast |
---|
38 | (Clight.Tint (Clight.I32, _), |
---|
39 | (Clight.Expr (_, |
---|
40 | Clight.Tint (Clight.I8, signedness3)) as e2)), |
---|
41 | _)), |
---|
42 | _) :: _ when signedness1 = signedness2 && signedness2 = signedness3 -> |
---|
43 | Clight.Ebinop (binop, e1, e2) |
---|
44 | | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _), |
---|
45 | Clight.Expr |
---|
46 | (Clight.Ebinop |
---|
47 | (binop, |
---|
48 | Clight.Expr |
---|
49 | (Clight.Ecast |
---|
50 | (Clight.Tint (Clight.I32, _), |
---|
51 | (Clight.Expr (_, |
---|
52 | Clight.Tint (Clight.I8, signedness2)) as e1)), |
---|
53 | _), |
---|
54 | Clight.Expr (Clight.Econst_int i, _)), |
---|
55 | _) :: _ when signedness1 = signedness2 -> |
---|
56 | Clight.Ebinop (binop, e1, |
---|
57 | Clight.Expr (Clight.Econst_int i, |
---|
58 | Clight.Tint (Clight.I8, signedness1))) |
---|
59 | | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _), |
---|
60 | Clight.Expr |
---|
61 | (Clight.Ebinop |
---|
62 | (binop, |
---|
63 | Clight.Expr (Clight.Econst_int i, _), |
---|
64 | Clight.Expr |
---|
65 | (Clight.Ecast |
---|
66 | (Clight.Tint (Clight.I32, _), |
---|
67 | (Clight.Expr (_, |
---|
68 | Clight.Tint (Clight.I8, signedness2)) as e1)), |
---|
69 | _)),sub_ctypes_res sub_exprs_res |
---|
70 | _) :: _ when signedness1 = signedness2 -> |
---|
71 | Clight.Ebinop (binop, |
---|
72 | Clight.Expr (Clight.Econst_int i, |
---|
73 | Clight.Tint (Clight.I8, signedness1)), |
---|
74 | e1) |
---|
75 | | _ -> ClightFold.expr_descr_fill_subs e sub_ctypes_res sub_exprs_res |
---|
76 | *) |
---|
77 | |
---|
78 | let simplify_exp ctype_opt e = e (* TODO *) |
---|
79 | |
---|
80 | let f_expr e _ _ = e |
---|
81 | |
---|
82 | let f_expr_descr e _ _ = e |
---|
83 | |
---|
84 | let f_statement stmt _ sub_stmts_res = |
---|
85 | let sub_exprs = match stmt with |
---|
86 | | _ -> assert false in |
---|
87 | ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res |
---|
88 | |
---|
89 | let simplify_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_statement |
---|
90 | |
---|
91 | let simplify_funct (id, fundef) = |
---|
92 | let fundef' = match fundef with |
---|
93 | | Clight.Internal cfun -> |
---|
94 | Clight.Internal |
---|
95 | { cfun with Clight.fn_body = simplify_stmt cfun.Clight.fn_body } |
---|
96 | | _ -> fundef in |
---|
97 | (id, fundef') |
---|
98 | |
---|
99 | let simplify p = p |
---|
100 | (* (* TODO: below *) |
---|
101 | { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct } |
---|
102 | *) |
---|