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]. *) |
---|
6 | |
---|
7 | let f_ctype ctype _ = ctype |
---|
8 | |
---|
9 | let f_expr = ClightFold.expr_fill_subs |
---|
10 | |
---|
11 | let f_expr_descr e sub_ctypes_res sub_exprs_res = |
---|
12 | match e, sub_exprs_res with |
---|
13 | | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _), |
---|
14 | Clight.Expr |
---|
15 | (Clight.Eunop |
---|
16 | (unop, |
---|
17 | Clight.Expr |
---|
18 | (Clight.Ecast |
---|
19 | (Clight.Tint (Clight.I32, _), |
---|
20 | (Clight.Expr (_, Clight.Tint (Clight.I8, signedness2)) as e)), |
---|
21 | _)), |
---|
22 | _) :: _ when signedness1 = signedness2 -> |
---|
23 | Clight.Eunop (unop, e) |
---|
24 | | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _), |
---|
25 | Clight.Expr |
---|
26 | (Clight.Ebinop |
---|
27 | (binop, |
---|
28 | Clight.Expr |
---|
29 | (Clight.Ecast |
---|
30 | (Clight.Tint (Clight.I32, _), |
---|
31 | (Clight.Expr (_, |
---|
32 | Clight.Tint (Clight.I8, signedness2)) as e1)), |
---|
33 | _), |
---|
34 | Clight.Expr |
---|
35 | (Clight.Ecast |
---|
36 | (Clight.Tint (Clight.I32, _), |
---|
37 | (Clight.Expr (_, |
---|
38 | Clight.Tint (Clight.I8, signedness3)) as e2)), |
---|
39 | _)), |
---|
40 | _) :: _ when signedness1 = signedness2 && signedness2 = signedness3 -> |
---|
41 | Clight.Ebinop (binop, e1, e2) |
---|
42 | | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _), |
---|
43 | Clight.Expr |
---|
44 | (Clight.Ebinop |
---|
45 | (binop, |
---|
46 | Clight.Expr |
---|
47 | (Clight.Ecast |
---|
48 | (Clight.Tint (Clight.I32, _), |
---|
49 | (Clight.Expr (_, |
---|
50 | Clight.Tint (Clight.I8, signedness2)) as e1)), |
---|
51 | _), |
---|
52 | Clight.Expr (Clight.Econst_int i, _)), |
---|
53 | _) :: _ when signedness1 = signedness2 -> |
---|
54 | Clight.Ebinop (binop, e1, |
---|
55 | Clight.Expr (Clight.Econst_int i, |
---|
56 | Clight.Tint (Clight.I8, signedness1))) |
---|
57 | | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _), |
---|
58 | Clight.Expr |
---|
59 | (Clight.Ebinop |
---|
60 | (binop, |
---|
61 | Clight.Expr (Clight.Econst_int i, _), |
---|
62 | Clight.Expr |
---|
63 | (Clight.Ecast |
---|
64 | (Clight.Tint (Clight.I32, _), |
---|
65 | (Clight.Expr (_, |
---|
66 | Clight.Tint (Clight.I8, signedness2)) as e1)), |
---|
67 | _)), |
---|
68 | _) :: _ when signedness1 = signedness2 -> |
---|
69 | Clight.Ebinop (binop, |
---|
70 | Clight.Expr (Clight.Econst_int i, |
---|
71 | Clight.Tint (Clight.I8, signedness1)), |
---|
72 | e1) |
---|
73 | | _ -> ClightFold.expr_descr_fill_subs e sub_ctypes_res sub_exprs_res |
---|
74 | |
---|
75 | let f_statement = ClightFold.statement_fill_subs |
---|
76 | |
---|
77 | let simplify_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_statement |
---|
78 | |
---|
79 | let simplify_funct (id, fundef) = |
---|
80 | let fundef' = match fundef with |
---|
81 | | Clight.Internal cfun -> |
---|
82 | Clight.Internal |
---|
83 | { cfun with Clight.fn_body = simplify_stmt cfun.Clight.fn_body } |
---|
84 | | _ -> fundef in |
---|
85 | (id, fundef') |
---|
86 | |
---|
87 | let simplify p = |
---|
88 | { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct } |
---|