diff options
Diffstat (limited to 'exportclight/Clightnorm.ml')
| -rw-r--r-- | exportclight/Clightnorm.ml | 178 |
1 files changed, 0 insertions, 178 deletions
diff --git a/exportclight/Clightnorm.ml b/exportclight/Clightnorm.ml deleted file mode 100644 index 88d44c08..00000000 --- a/exportclight/Clightnorm.ml +++ /dev/null @@ -1,178 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 } |