From 891377ce1962cdb31357d6580d6546ec22df2b4f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 10:22:27 +0000 Subject: Switching to the new C parser/elaborator/simplifier git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cparser/SimplExpr.ml | 564 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 564 insertions(+) create mode 100644 cparser/SimplExpr.ml (limited to 'cparser/SimplExpr.ml') diff --git a/cparser/SimplExpr.ml b/cparser/SimplExpr.ml new file mode 100644 index 00000000..484e2d87 --- /dev/null +++ b/cparser/SimplExpr.ml @@ -0,0 +1,564 @@ +(* *********************************************************************) +(* *) +(* 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 General Public License as published by *) +(* the Free Software Foundation, either version 2 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. *) +(* *) +(* *********************************************************************) + +(* Pulling side-effects out of expressions *) + +(* Assumes: nothing + Produces: simplified code *) + +open C +open Cutil +open Transform + +(* Grammar of simplified expressions: + e ::= EConst cst + | ESizeof ty + | EVar id + | EUnop pure-unop e + | EBinop pure-binop e e + | EConditional e e e + | ECast ty e + + Grammar of statements produced to reflect side-effects in expressions: + s ::= Sskip + | Sdo (EBinop Oassign e e) + | Sdo (EBinop Oassign e (ECall e e* )) + | Sdo (Ecall e el) + | Sseq s s + | Sif e s s +*) + +let rec is_simpl_expr e = + match e.edesc with + | EConst cst -> true + | ESizeof ty -> true + | EVar id -> true + | EUnop((Ominus|Oplus|Olognot|Onot|Oderef|Oaddrof), e1) -> + is_simpl_expr e1 + | EBinop((Oadd|Osub|Omul|Odiv|Omod|Oand|Oor|Oxor|Oshl|Oshr| + Oeq|One|Olt|Ogt|Ole|Oge|Oindex|Ologand|Ologor), e1, e2, _) -> + is_simpl_expr e1 && is_simpl_expr e2 + | EConditional(e1, e2, e3) -> + is_simpl_expr e1 && is_simpl_expr e2 && is_simpl_expr e3 + | ECast(ty, e1) -> + is_simpl_expr e1 + | _ -> + false + +(* "Destination" of a simplified expression *) + +type exp_destination = + | RHS (* evaluate as a r-value *) + | LHS (* evaluate as a l-value *) + | Drop (* drop its value, we only need the side-effects *) + | Set of exp (* assign it to the given simplified l.h.s. *) + +let voidconst = { nullconst with etyp = TVoid [] } + +(* Reads from volatile lvalues are also considered as side-effects if + [volatilize] is true. *) + +let volatilize = ref false + +(* [simpl_expr loc env e act] returns a pair [s, e'] of + a statement that performs the side-effects present in [e] and + a simplified, side-effect-free expression [e']. + If [act] is [RHS], [e'] evaluates to the same value as [e]. + If [act] is [LHS], [e'] evaluates to the same location as [e]. + If [act] is [Drop], [e'] is not meaningful and must be ignored. + If [act] is [Set lhs], [s] also performs an assignment + equivalent to [lhs = e]. [e'] is not meaningful. *) + +let simpl_expr loc env e act = + + (* Temporaries should not be [const] because we assign into them, + and need not be [volatile] because no one else is writing into them. + As for [restrict] it doesn't make sense anyway. *) + + let new_temp ty = + Transform.new_temp (erase_attributes_type env ty) in + + let sseq s1 s2 = Cutil.sseq loc s1 s2 in + + let sassign e1 e2 = + { sdesc = Sdo {edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp}; + sloc = loc } in + + let sif e s1 s2 = + { sdesc = Sif(e, s1, s2); sloc = loc } in + + let is_volatile_read e = + !volatilize + && List.mem AVolatile (attributes_of_type env e.etyp) + && is_lvalue env e in + + let lhs_to_rhs e = + if is_volatile_read e + then (let t = new_temp e.etyp in (sassign t e, t)) + else (sskip, e) in + + let finish act s e = + match act with + | RHS -> + if is_volatile_read e + then (let t = new_temp e.etyp in (sseq s (sassign t e), t)) + else (s, e) + | LHS -> + (s, e) + | Drop -> + if is_volatile_read e + then (let t = new_temp e.etyp in (sseq s (sassign t e), voidconst)) + else (s, voidconst) + | Set lhs -> + if is_volatile_read e + then (let t = new_temp e.etyp in + (sseq s (sseq (sassign t e) (sassign lhs t)), voidconst)) + else (sseq s (sassign lhs e), voidconst) in + + let rec simpl e act = + match e.edesc with + + | EConst cst -> + finish act sskip e + + | ESizeof ty -> + finish act sskip e + + | EVar id -> + finish act sskip e + + | EUnop(op, e1) -> + + begin match op with + + | Ominus | Oplus | Olognot | Onot | Oderef | Oarrow _ -> + let (s1, e1') = simpl e1 RHS in + finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp} + + | Oaddrof -> + let (s1, e1') = simpl e1 LHS in + finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp} + + | Odot _ -> + let (s1, e1') = simpl e1 (if act = LHS then LHS else RHS) in + finish act s1 {edesc = EUnop(op, e1'); etyp = e.etyp} + + | Opreincr | Opredecr -> + let (s1, e1') = simpl e1 LHS in + let (s2, e2') = lhs_to_rhs e1' in + let op' = match op with Opreincr -> Oadd | _ -> Osub in + let ty = unary_conversion env e.etyp in + let e3 = + {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in + begin match act with + | Drop -> + (sseq s1 (sseq s2 (sassign e1' e3)), voidconst) + | _ -> + let tmp = new_temp e.etyp in + finish act (sseq s1 (sseq s2 (sseq (sassign tmp e3) + (sassign e1' tmp)))) + tmp + end + + | Opostincr | Opostdecr -> + let (s1, e1') = simpl e1 LHS in + let op' = match op with Opostincr -> Oadd | _ -> Osub in + let ty = unary_conversion env e.etyp in + begin match act with + | Drop -> + let (s2, e2') = lhs_to_rhs e1' in + let e3 = + {edesc = EBinop(op', e2', intconst 1L IInt, ty); etyp = ty} in + (sseq s1 (sseq s2 (sassign e1' e3)), voidconst) + | _ -> + let tmp = new_temp e.etyp in + let e3 = + {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in + finish act (sseq s1 (sseq (sassign tmp e1') (sassign e1' e3))) + tmp + end + + end + + | EBinop(op, e1, e2, ty) -> + + begin match op with + + | Oadd | Osub | Omul | Odiv | Omod | Oand | Oor | Oxor + | Oshl | Oshr | Oeq | One | Olt | Ogt | Ole | Oge | Oindex -> + let (s1, e1') = simpl e1 RHS in + let (s2, e2') = simpl e2 RHS in + finish act (sseq s1 s2) + {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp} + + | Oassign -> + if act = Drop && is_simpl_expr e1 then + simpl e2 (Set e1) + else begin + match act with + | Drop -> + let (s1, e1') = simpl e1 LHS in + let (s2, e2') = simpl e2 RHS in + (sseq s1 (sseq s2 (sassign e1' e2')), voidconst) + | _ -> + let tmp = new_temp e.etyp in + let (s1, e1') = simpl e1 LHS in + let (s2, e2') = simpl e2 (Set tmp) in + finish act (sseq s1 (sseq s2 (sassign e1' tmp))) + tmp + end + + | Oadd_assign | Osub_assign | Omul_assign | Odiv_assign + | Omod_assign | Oand_assign | Oor_assign | Oxor_assign + | Oshl_assign | Oshr_assign -> + let (s1, e1') = simpl e1 LHS in + let (s11, e11') = lhs_to_rhs e1' in + let (s2, e2') = simpl e2 RHS in + let op' = + match op with + | Oadd_assign -> Oadd | Osub_assign -> Osub + | Omul_assign -> Omul | Odiv_assign -> Odiv + | Omod_assign -> Omod | Oand_assign -> Oand + | Oor_assign -> Oor | Oxor_assign -> Oxor + | Oshl_assign -> Oshl | Oshr_assign -> Oshr + | _ -> assert false in + let e3 = + { edesc = EBinop(op', e11', e2', ty); etyp = ty } in + begin match act with + | Drop -> + (sseq s1 (sseq s11 (sseq s2 (sassign e1' e3))), voidconst) + | _ -> + let tmp = new_temp e.etyp in + finish act (sseq s1 (sseq s11 (sseq s2 + (sseq (sassign tmp e3) (sassign e1' tmp))))) + tmp + end + + | Ocomma -> + let (s1, _) = simpl e1 Drop in + let (s2, e2') = simpl e2 act in + (sseq s1 s2, e2') + + | Ologand -> + let (s1, e1') = simpl e1 RHS in + if is_simpl_expr e2 then begin + finish act s1 + {edesc = EBinop(Ologand, e1', e2, ty); etyp = e.etyp} + end else begin + match act with + | Drop -> + let (s2, _) = simpl e2 Drop in + (sseq s1 (sif e1' s2 sskip), voidconst) + | RHS | LHS -> (* LHS should not happen *) + let (s2, e2') = simpl e2 RHS in + let tmp = new_temp e.etyp in + (sseq s1 (sif e1' + (sseq s2 (sif e2' + (sassign tmp (intconst 1L IInt)) + (sassign tmp (intconst 0L IInt)))) + (sassign tmp (intconst 0L IInt))), + tmp) + | Set lv -> + let (s2, _) = simpl e2 (Set lv) in + (sseq s1 (sif e1' s2 (sassign lv (intconst 0L IInt))), + voidconst) + end + + | Ologor -> + let (s1, e1') = simpl e1 RHS in + if is_simpl_expr e2 then begin + finish act s1 + {edesc = EBinop(Ologor, e1', e2, ty); etyp = e.etyp} + end else begin + match act with + | Drop -> + let (s2, _) = simpl e2 Drop in + (sseq s1 (sif e1' sskip s2), voidconst) + | RHS | LHS -> (* LHS should not happen *) + let (s2, e2') = simpl e2 RHS in + let tmp = new_temp e.etyp in + (sseq s1 (sif e1' + (sassign tmp (intconst 1L IInt)) + (sseq s2 (sif e2' + (sassign tmp (intconst 1L IInt)) + (sassign tmp (intconst 0L IInt))))), + tmp) + | Set lv -> + let (s2, _) = simpl e2 (Set lv) in + (sseq s1 (sif e1' (sassign lv (intconst 1L IInt)) s2), + voidconst) + end + + end + + | EConditional(e1, e2, e3) -> + let (s1, e1') = simpl e1 RHS in + if is_simpl_expr e2 && is_simpl_expr e3 then begin + finish act s1 {edesc = EConditional(e1', e2, e3); etyp = e.etyp} + end else begin + match act with + | Drop -> + let (s2, _) = simpl e2 Drop in + let (s3, _) = simpl e3 Drop in + (sseq s1 (sif e1' s2 s3), voidconst) + | RHS | LHS -> (* LHS should not happen *) + let tmp = new_temp e.etyp in + let (s2, _) = simpl e2 (Set tmp) in + let (s3, _) = simpl e3 (Set tmp) in + (sseq s1 (sif e1' s2 s3), tmp) + | Set lv -> + let (s2, _) = simpl e2 (Set lv) in + let (s3, _) = simpl e3 (Set lv) in + (sseq s1 (sif e1' s2 s3), voidconst) + end + + | ECast(ty, e1) -> + if is_void_type env ty then begin + if act <> Drop then + Errors.warning "%acast to 'void' in a context expecting a value\n" + formatloc loc; + simpl e1 act + end else begin + let (s1, e1') = simpl e1 RHS in + finish act s1 {edesc = ECast(ty, e1'); etyp = e.etyp} + end + + | ECall(e1, el) -> + let (s1, e1') = simpl e1 RHS in + let (s2, el') = simpl_list el in + let e2 = { edesc = ECall(e1', el'); etyp = e.etyp } in + begin match act with + | Drop -> + (sseq s1 (sseq s2 {sdesc = Sdo e2; sloc=loc}), voidconst) + | Set({edesc = EVar _} as lhs) -> + (* CompCert wants the destination of a call to be a variable, + not a more complex lhs. In the latter case, we + fall through the catch-all case below *) + (sseq s1 (sseq s2 (sassign lhs e2)), voidconst) + | _ -> + let tmp = new_temp e.etyp in + finish act (sseq s1 (sseq s2 (sassign tmp e2))) tmp + end + + and simpl_list = function + | [] -> (sskip, []) + | e1 :: el -> + let (s1, e1') = simpl e1 RHS in + let (s2, el') = simpl_list el in + (sseq s1 s2, e1' :: el') + + in simpl e act + +(* Simplification of an initializer *) + +let simpl_initializer loc env i = + + let rec simpl_init = function + | Init_single e -> + let (s, e') = simpl_expr loc env e RHS in + (s, Init_single e) + | Init_array il -> + let rec simpl = function + | [] -> (sskip, []) + | i1 :: il -> + let (s1, i1') = simpl_init i1 in + let (s2, il') = simpl il in + (sseq loc s1 s2, i1' :: il') in + let (s, il') = simpl il in + (s, Init_array il') + | Init_struct(id, il) -> + let rec simpl = function + | [] -> (sskip, []) + | (f1, i1) :: il -> + let (s1, i1') = simpl_init i1 in + let (s2, il') = simpl il in + (sseq loc s1 s2, (f1, i1') :: il') in + let (s, il') = simpl il in + (s, Init_struct(id, il')) + | Init_union(id, f, i) -> + let (s, i') = simpl_init i in + (s, Init_union(id, f, i')) + + in simpl_init i + +(* Construct a simplified statement equivalent to [if (e) s1; else s2;]. + Optimizes the case where e contains [&&] or [||] or [?]. + [s1] or [s2] can be duplicated, so use only for small [s1] and [s2] + that do not define any labels. *) + +let rec simpl_if loc env e s1 s2 = + match e.edesc with + | EUnop(Olognot, e1) -> + simpl_if loc env e1 s2 s1 + | EBinop(Ologand, e1, e2, _) -> + simpl_if loc env e1 + (simpl_if loc env e2 s1 s2) + s2 + | EBinop(Ologor, e1, e2, _) -> + simpl_if loc env e1 + s1 + (simpl_if loc env e2 s1 s2) + | EConditional(e1, e2, e3) -> + simpl_if loc env e1 + (simpl_if loc env e2 s1 s2) + (simpl_if loc env e3 s1 s2) + | _ -> + let (s, e') = simpl_expr loc env e RHS in + sseq loc s {sdesc = Sif(e', s1, s2); sloc = loc} + +(* Trivial statements for which [simpl_if] is applicable *) + +let trivial_stmt s = + match s.sdesc with + | Sskip | Scontinue | Sbreak | Sgoto _ -> true + | _ -> false + +(* Construct a simplified statement equivalent to [if (!e) exit; ]. *) + +let break_if_false loc env e = + simpl_if loc env e + {sdesc = Sskip; sloc = loc} + {sdesc = Sbreak; sloc = loc} + +(* Simplification of a statement *) + +let simpl_statement env s = + + let rec simpl_stmt s = + match s.sdesc with + + | Sskip -> + s + + | Sdo e -> + let (s', _) = simpl_expr s.sloc env e Drop in + s' + + | Sseq(s1, s2) -> + {sdesc = Sseq(simpl_stmt s1, simpl_stmt s2); sloc = s.sloc} + + | Sif(e, s1, s2) -> + if trivial_stmt s1 && trivial_stmt s2 then + simpl_if s.sloc env e (simpl_stmt s1) (simpl_stmt s2) + else begin + let (s', e') = simpl_expr s.sloc env e RHS in + sseq s.sloc s' + {sdesc = Sif(e', simpl_stmt s1, simpl_stmt s2); + sloc = s.sloc} + end + + | Swhile(e, s1) -> + if is_simpl_expr e then + {sdesc = Swhile(e, simpl_stmt s1); sloc = s.sloc} + else + {sdesc = + Swhile(intconst 1L IInt, + sseq s.sloc (break_if_false s.sloc env e) + (simpl_stmt s1)); + sloc = s.sloc} + + | Sdowhile(s1, e) -> + if is_simpl_expr e then + {sdesc = Sdowhile(simpl_stmt s1, e); sloc = s.sloc} + else begin + let tmp = new_temp (TInt(IInt, [])) in + let (s', _) = simpl_expr s.sloc env e (Set tmp) in + let s_init = + {sdesc = Sdo {edesc = EBinop(Oassign, tmp, intconst 1L IInt, tmp.etyp); + etyp = tmp.etyp}; + sloc = s.sloc} in + {sdesc = Sfor(s_init, tmp, s', simpl_stmt s1); sloc = s.sloc} + end +(*** Alternate translation that unfortunately puts a "break" in the + "next" part of a "for", something that is not supported + by Clight semantics, and has unknown behavior in gcc. + {sdesc = + Sfor(sskip, + intconst 1L IInt, + break_if_false s.sloc env e, + simpl_stmt s1); + sloc = s.sloc} +***) + + | Sfor(s1, e, s2, s3) -> + if is_simpl_expr e then + {sdesc = Sfor(simpl_stmt s1, + e, + simpl_stmt s2, + simpl_stmt s3); + sloc = s.sloc} + else + let (s', e') = simpl_expr s.sloc env e RHS in + {sdesc = Sfor(sseq s.sloc (simpl_stmt s1) s', + e', + sseq s.sloc (simpl_stmt s2) s', + simpl_stmt s3); + sloc = s.sloc} + + | Sbreak -> + s + | Scontinue -> + s + + | Sswitch(e, s1) -> + let (s', e') = simpl_expr s.sloc env e RHS in + sseq s.sloc s' {sdesc = Sswitch(e', simpl_stmt s1); sloc = s.sloc} + + | Slabeled(lbl, s1) -> + {sdesc = Slabeled(lbl, simpl_stmt s1); sloc = s.sloc} + + | Sgoto lbl -> + s + + | Sreturn None -> + s + + | Sreturn (Some e) -> + let (s', e') = simpl_expr s.sloc env e RHS in + sseq s.sloc s' {sdesc = Sreturn(Some e'); sloc = s.sloc} + + | Sblock sl -> + {sdesc = Sblock(simpl_block sl); sloc = s.sloc} + + | Sdecl d -> assert false + + and simpl_block = function + | [] -> [] + | ({sdesc = Sdecl(sto, id, ty, None)} as s) :: sl -> + s :: simpl_block sl + | ({sdesc = Sdecl(sto, id, ty, Some i)} as s) :: sl -> + let (s', i') = simpl_initializer s.sloc env i in + let sl' = + {sdesc = Sdecl(sto, id, ty, Some i'); sloc = s.sloc} + :: simpl_block sl in + if s'.sdesc = Sskip then sl' else s' :: sl' + | s :: sl -> + simpl_stmt s :: simpl_block sl + + in simpl_stmt s + +(* Simplification of a function definition *) + +let simpl_fundef env f = + reset_temps(); + let body' = simpl_statement env f.fd_body in + let temps = get_temps() in + { f with fd_locals = f.fd_locals @ temps; fd_body = body' } + +(* Entry point *) + +let program ?(volatile = false) p = + volatilize := volatile; + Transform.program ~fundef:simpl_fundef p -- cgit