diff options
Diffstat (limited to 'export/Clightnorm.ml')
| -rw-r--r-- | export/Clightnorm.ml | 178 |
1 files changed, 178 insertions, 0 deletions
diff --git a/export/Clightnorm.ml b/export/Clightnorm.ml new file mode 100644 index 00000000..88d44c08 --- /dev/null +++ b/export/Clightnorm.ml @@ -0,0 +1,178 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Clight-to-Clight rewriting to name memory loads *) + +(* The effect of this rewriting is to ensure that Clight expressions + whose evaluation involves a memory load (i.e. a lvalue-to-rvalue + conversion with By_value access mode) are always bound to a temporary + and never occur deep inside another expression. For example, + + tmp = *(x + 0) + *(x + 1) + + in the original Clight is rewritten to + + tmp1 = *(x + 0) + tmp2 = *(x + 1) + tmp = tmp1 + tmp2 +*) + +open Camlcoq +open Ctypes +open Clight + +let gen_next : AST.ident ref = ref P.one +let gen_trail : (AST.ident * coq_type) list ref = ref [] + +let gensym ty = + let id = !gen_next in + gen_next := P.succ id; + gen_trail := (id, ty) :: !gen_trail; + id + +let is_lvalue = function + | Evar _ | Ederef _ | Efield _ -> true + | _ -> false + +let accesses_memory e = + is_lvalue e && + match access_mode (typeof e) with By_value _ -> true | _ -> false + +(** Normalization of an expression. Return a normalized expression + and a list of statements to be executed before evaluating the expression. *) + +let rec norm_expr e = + let (sl, e') = norm_expr_1 e in + if accesses_memory e then begin + let ty = typeof e in + let id = gensym ty in + (sl @ [Sset(id, e')], Etempvar(id, ty)) + end else + (sl, e') + +and norm_expr_1 e = + match e with + | Econst_int _ | Econst_float _ | Econst_single _ | Econst_long _ -> ([], e) + | Evar _ | Etempvar _ -> ([], e) + | Ederef(e1, t) -> + let (sl, e1') = norm_expr e1 in (sl, Ederef(e1', t)) + | Eaddrof(e1, t) -> + let (sl, e1') = norm_expr_lvalue e1 in (sl, Eaddrof(e1', t)) + | Eunop(op, e1, t) -> + let (sl, e1') = norm_expr e1 in (sl, Eunop(op, e1', t)) + | Ebinop(op, e1, e2, t) -> + let (sl1, e1') = norm_expr e1 in + let (sl2, e2') = norm_expr e2 in + (sl1 @ sl2, Ebinop(op, e1', e2', t)) + | Ecast(e1, t) -> + let (sl, e1') = norm_expr e1 in (sl, Ecast(e1', t)) + | Efield(e1, id, t) -> + let (sl, e1') = norm_expr e1 in (sl, Efield(e1', id, t)) + | Esizeof _ | Ealignof _ -> ([], e) + +(** An expression in l-value position has no memory dereference at top level, + by definition of l-values. Hence, use the [norm_expr_1] variant.. *) +and norm_expr_lvalue e = norm_expr_1 e + +(** In a [Sset id e] statement, the [e] expression can contain a memory + dereference at top level. Hence, use the [norm_expr_1] variant. *) +let norm_expr_set_top = norm_expr_1 + +let rec norm_expr_list el = + match el with + | [] -> ([], []) + | e1 :: el -> + let (sl1, e1') = norm_expr e1 in + let (sl2, el') = norm_expr_list el in + (sl1 @ sl2, e1' :: el') + +let rec add_sequence sl s = + match sl with + | [] -> s + | s1 :: sl -> Ssequence(s1, add_sequence sl s) + +let rec norm_stmt s = + match s with + | Sskip -> s + | Sassign(e1, e2) -> + let (sl1, e1') = norm_expr_lvalue e1 in + let (sl2, e2') = norm_expr e2 in + add_sequence (sl1 @ sl2) (Sassign(e1', e2')) + | Sset(id, e) -> + let (sl, e') = norm_expr_set_top e in + add_sequence sl (Sset(id, e')) + | Scall(optid, e, el) -> + let (sl1, e') = norm_expr e in + let (sl2, el') = norm_expr_list el in + add_sequence (sl1 @ sl2) (Scall(optid, e', el')) + | Sbuiltin(optid, ef, tyl, el) -> + let (sl, el') = norm_expr_list el in + add_sequence sl (Sbuiltin(optid, ef, tyl, el')) + | Ssequence(s1, s2) -> + Ssequence(norm_stmt s1, norm_stmt s2) + | Sifthenelse(e, s1, s2) -> + let (sl, e') = norm_expr e in + add_sequence sl (Sifthenelse(e', norm_stmt s1, norm_stmt s2)) + | Sloop(s1, s2) -> + Sloop(norm_stmt s1, norm_stmt s2) + | Sbreak | Scontinue | Sreturn None -> s + | Sreturn (Some e) -> + let (sl, e') = norm_expr e in + add_sequence sl (Sreturn(Some e')) + | Sswitch(e, ls) -> + let (sl, e') = norm_expr e in + add_sequence sl (Sswitch(e', norm_lbl_stmt ls)) + | Slabel(lbl, s1) -> + Slabel(lbl, norm_stmt s1) + | Sgoto lbl -> s + +and norm_lbl_stmt ls = + match ls with + | LSnil -> LSnil + | LScons(n, s, ls) -> LScons(n, norm_stmt s, norm_lbl_stmt ls) + +(* In "canonical atoms" mode, temporaries are between 2^7 and 2^12 - 1. + Below 2^7 are single-letter identifiers and above 2^12 are all + other identifiers. *) + +let first_temp = P.of_int 128 +let last_temp = P.of_int 4095 + +let next_var curr (v, _) = + if P.lt v curr + || !use_canonical_atoms && (P.lt v first_temp || P.gt v last_temp) + then curr + else P.succ v + +let next_var_list vars start = List.fold_left next_var start vars + +let norm_function f = + gen_next := next_var_list f.fn_params + (next_var_list f.fn_vars + (next_var_list f.fn_temps + (Camlcoq.first_unused_ident ()))); + gen_trail := []; + let s' = norm_stmt f.fn_body in + let new_temps = !gen_trail in + { f with fn_body = s'; fn_temps = f.fn_temps @ new_temps } + +let norm_fundef = function + | Internal f -> Internal (norm_function f) + | External _ as fd -> fd + +let norm_program p = + let p1 = AST.transform_program norm_fundef (program_of_program p) in + { p with prog_defs = p1.AST.prog_defs } |