From 8539759095f95f2fbb680efc7633d868099114c8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 29 Dec 2012 16:55:38 +0000 Subject: Merge of the clightgen branch: - Alternate semantics for Clight where function parameters are temporaries, not variables - New pass SimplLocals that turns non-addressed local variables into temporaries - Simplified Csharpminor, Cshmgen and Cminorgen accordingly - SimplExpr starts its temporaries above variable names, therefoe Cminorgen no longer needs to encode variable names and temps names. - Simplified Cminor parser & printer, as well as Errors, accordingly. - New tool clightgen to produce Clight AST in Coq-parsable .v files. - Removed side condition "return type is void" on rules skip_seq in the semantics of CompCert C, Clight, C#minor, Cminor. - Adapted RTLgenproof accordingly (now uses a memory extension). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/SimplLocals.v | 234 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 234 insertions(+) create mode 100644 cfrontend/SimplLocals.v (limited to 'cfrontend/SimplLocals.v') diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v new file mode 100644 index 00000000..2a472f7f --- /dev/null +++ b/cfrontend/SimplLocals.v @@ -0,0 +1,234 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pulling local scalar variables whose address is not taken + into temporary variables. *) + +Require Import FSets. +Require FSetAVL. +Require Import Coqlib. +Require Import Ordered. +Require Import Errors. +Require Import AST. +Require Import Ctypes. +Require Import Cop. +Require Import Clight. + +Open Scope error_monad_scope. +Open Scope string_scope. + +Module VSet := FSetAVL.Make(OrderedPositive). + +(** The set of local variables that can be lifted to temporaries, + because they are scalar and their address is not taken. *) + +Definition compilenv := VSet.t. + +Definition is_liftable_var (cenv: compilenv) (a: expr) : option ident := + match a with + | Evar id ty => if VSet.mem id cenv then Some id else None + | _ => None + end. + +(** Rewriting of expressions and statements. *) + +Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr := + match a with + | Econst_int _ _ => a + | Econst_float _ _ => a + | Evar id ty => if VSet.mem id cenv then Etempvar id ty else Evar id ty + | Etempvar id ty => Etempvar id ty + | Ederef a1 ty => Ederef (simpl_expr cenv a1) ty + | Eaddrof a1 ty => Eaddrof (simpl_expr cenv a1) ty + | Eunop op a1 ty => Eunop op (simpl_expr cenv a1) ty + | Ebinop op a1 a2 ty => Ebinop op (simpl_expr cenv a1) (simpl_expr cenv a2) ty + | Ecast a1 ty => Ecast (simpl_expr cenv a1) ty + | Efield a1 fld ty => Efield (simpl_expr cenv a1) fld ty + end. + +Definition simpl_exprlist (cenv: compilenv) (al: list expr) : list expr := + List.map (simpl_expr cenv) al. + +Definition check_temp (cenv: compilenv) (id: ident) : res unit := + if VSet.mem id cenv + then Error (MSG "bad temporary " :: CTX id :: nil) + else OK tt. + +Definition check_opttemp (cenv: compilenv) (optid: option ident) : res unit := + match optid with + | Some id => check_temp cenv id + | None => OK tt + end. + +Fixpoint simpl_stmt (cenv: compilenv) (s: statement) : res statement := + match s with + | Sskip => OK Sskip + | Sassign a1 a2 => + match is_liftable_var cenv a1 with + | Some id => + OK (Sset id (Ecast (simpl_expr cenv a2) (typeof a1))) + | None => + OK (Sassign (simpl_expr cenv a1) (simpl_expr cenv a2)) + end + | Sset id a => + do x <- check_temp cenv id; + OK (Sset id (simpl_expr cenv a)) + | Scall optid a al => + do x <- check_opttemp cenv optid; + OK (Scall optid (simpl_expr cenv a) (simpl_exprlist cenv al)) + | Sbuiltin optid ef tyargs al => + do x <- check_opttemp cenv optid; + OK (Sbuiltin optid ef tyargs (simpl_exprlist cenv al)) + | Ssequence s1 s2 => + do s1' <- simpl_stmt cenv s1; + do s2' <- simpl_stmt cenv s2; + OK (Ssequence s1' s2') + | Sifthenelse a s1 s2 => + do s1' <- simpl_stmt cenv s1; + do s2' <- simpl_stmt cenv s2; + OK (Sifthenelse (simpl_expr cenv a) s1' s2') + | Sloop s1 s2 => + do s1' <- simpl_stmt cenv s1; + do s2' <- simpl_stmt cenv s2; + OK (Sloop s1' s2') + | Sbreak => OK Sbreak + | Scontinue => OK Scontinue + | Sreturn opta => OK (Sreturn (option_map (simpl_expr cenv) opta)) + | Sswitch a ls => + do ls' <- simpl_lblstmt cenv ls; + OK (Sswitch (simpl_expr cenv a) ls') + | Slabel lbl s => + do s' <- simpl_stmt cenv s; + OK (Slabel lbl s') + | Sgoto lbl => OK (Sgoto lbl) + end + +with simpl_lblstmt (cenv: compilenv) (ls: labeled_statements) : res labeled_statements := + match ls with + | LSdefault s => + do s' <- simpl_stmt cenv s; + OK (LSdefault s') + | LScase n s ls1 => + do s' <- simpl_stmt cenv s; + do ls1' <- simpl_lblstmt cenv ls1; + OK (LScase n s' ls1') + end. + +(** Function parameters that are not lifted to temporaries must be + stored in the corresponding local variable at function entry. *) + +Fixpoint store_params (cenv: compilenv) (params: list (ident * type)) + (s: statement): statement := + match params with + | nil => s + | (id, ty) :: params' => + if VSet.mem id cenv + then store_params cenv params' s + else Ssequence (Sassign (Evar id ty) (Etempvar id ty)) + (store_params cenv params' s) + end. + +(** Compute the set of variables whose address is taken *) + +Fixpoint addr_taken_expr (a: expr): VSet.t := + match a with + | Econst_int _ _ => VSet.empty + | Econst_float _ _ => VSet.empty + | Evar id ty => VSet.empty + | Etempvar id ty => VSet.empty + | Ederef a1 ty => addr_taken_expr a1 + | Eaddrof (Evar id ty1) ty => VSet.singleton id + | Eaddrof a1 ty => addr_taken_expr a1 + | Eunop op a1 ty => addr_taken_expr a1 + | Ebinop op a1 a2 ty => VSet.union (addr_taken_expr a1) (addr_taken_expr a2) + | Ecast a1 ty => addr_taken_expr a1 + | Efield a1 fld ty => addr_taken_expr a1 + end. + +Fixpoint addr_taken_exprlist (l: list expr) : VSet.t := + match l with + | nil => VSet.empty + | a :: l' => VSet.union (addr_taken_expr a) (addr_taken_exprlist l') + end. + +Fixpoint addr_taken_stmt (s: statement) : VSet.t := + match s with + | Sskip => VSet.empty + | Sassign a b => VSet.union (addr_taken_expr a) (addr_taken_expr b) + | Sset id a => addr_taken_expr a + | Scall optid a bl => VSet.union (addr_taken_expr a) (addr_taken_exprlist bl) + | Sbuiltin optid ef tyargs bl => addr_taken_exprlist bl + | Ssequence s1 s2 => VSet.union (addr_taken_stmt s1) (addr_taken_stmt s2) + | Sifthenelse a s1 s2 => + VSet.union (addr_taken_expr a) (VSet.union (addr_taken_stmt s1) (addr_taken_stmt s2)) + | Sloop s1 s2 => VSet.union (addr_taken_stmt s1) (addr_taken_stmt s2) + | Sbreak => VSet.empty + | Scontinue => VSet.empty + | Sreturn None => VSet.empty + | Sreturn (Some a) => addr_taken_expr a + | Sswitch a ls => VSet.union (addr_taken_expr a) (addr_taken_lblstmt ls) + | Slabel lbl s => addr_taken_stmt s + | Sgoto lbl => VSet.empty + end + +with addr_taken_lblstmt (ls: labeled_statements) : VSet.t := + match ls with + | LSdefault s => addr_taken_stmt s + | LScase n s ls' => VSet.union (addr_taken_stmt s) (addr_taken_lblstmt ls') + end. + +(** The compilation environment for a function is the set of local variables + that are scalars and whose addresses are not taken. *) + +Definition add_local_variable (atk: VSet.t) (id_ty: ident * type) + (cenv: compilenv) : compilenv := + let (id, ty) := id_ty in + match access_mode ty with + | By_value chunk => if VSet.mem id atk then cenv else VSet.add id cenv + | _ => cenv + end. + +Definition cenv_for (f: function) : compilenv := + let atk := addr_taken_stmt f.(fn_body) in + List.fold_right (add_local_variable atk) VSet.empty (f.(fn_params) ++ f.(fn_vars)). + +(** Transform a function *) + +Definition remove_lifted (cenv: compilenv) (vars: list (ident * type)) := + List.filter (fun id_ty => negb (VSet.mem (fst id_ty) cenv)) vars. + +Definition add_lifted (cenv: compilenv) (vars1 vars2: list (ident * type)) := + List.filter (fun id_ty => VSet.mem (fst id_ty) cenv) vars1 ++ vars2. + +Definition transf_function (f: function) : res function := + let cenv := cenv_for f in + do x <- assertion (list_disjoint_dec ident_eq (var_names f.(fn_params)) + (var_names f.(fn_temps))); + do body' <- simpl_stmt cenv f.(fn_body); + OK {| fn_return := f.(fn_return); + fn_params := f.(fn_params); + fn_vars := remove_lifted cenv (f.(fn_params) ++ f.(fn_vars)); + fn_temps := add_lifted cenv f.(fn_vars) f.(fn_temps); + fn_body := store_params cenv f.(fn_params) body' |}. + +(** Whole-program transformation *) + +Definition transf_fundef (fd: fundef) : res fundef := + match fd with + | Internal f => do tf <- transf_function f; OK (Internal tf) + | External ef targs tres => OK (External ef targs tres) + end. + +Definition transf_program (p: program) : res program := + AST.transform_partial_program transf_fundef p. + + -- cgit