diff options
Diffstat (limited to 'cparser/Unblock.ml')
| -rw-r--r-- | cparser/Unblock.ml | 201 |
1 files changed, 175 insertions, 26 deletions
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 34d8cf8..ba8e379 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -22,31 +22,24 @@ open C open Cutil open Cerrors -(* Convert an initializer to a list of assignments. - Prepend those assignments to the given statement. *) +(* Convert an initializer to a list of assignment expressions. *) -let sdoseq loc e s = - sseq loc {sdesc = Sdo e; sloc = loc} s - -let rec local_initializer loc env path init k = +let rec local_initializer env path init k = match init with | Init_single e -> - sdoseq loc - { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp } - k + { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp } :: k | Init_array il -> let (ty_elt, sz) = match unroll env path.etyp with | TArray(ty_elt, Some sz, _) -> (ty_elt, sz) - | _ -> fatal_error "%aWrong type for array initializer" - formatloc loc in + | _ -> fatal_error "Wrong type for array initializer" in let rec array_init pos il = if pos >= sz then k else begin let (i1, il') = match il with | [] -> (default_init env ty_elt, []) | i1 :: il' -> (i1, il') in - local_initializer loc env + local_initializer env { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, [])); etyp = ty_elt } i1 @@ -55,18 +48,37 @@ let rec local_initializer loc env path init k = array_init 0L il | Init_struct(id, fil) -> let field_init (fld, i) k = - local_initializer loc env + local_initializer env { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ } i k in List.fold_right field_init fil k | Init_union(id, fld, i) -> - local_initializer loc env + local_initializer env { edesc = EUnop(Odot fld.fld_name, path); etyp = fld.fld_typ } i k -(* Record new variables to be locally defined *) +(* Prepend assignments to the given statement. *) + +let add_inits_stmt loc inits s = + List.fold_right + (fun e s -> sseq loc {sdesc = Sdo e; sloc = loc} s) + inits s + +(* Prepend assignments to the given expression. *) +(* Associate to the left so that it prints more nicely *) + +let add_inits_expr inits e = + match inits with + | [] -> e + | i1 :: il -> + let comma a b = + { edesc = EBinop(Ocomma, a, b, b.etyp); etyp = b.etyp } in + comma (List.fold_left comma i1 il) e + +(* Record new variables to be locally or globally defined *) let local_variables = ref ([]: decl list) +let global_variables = ref ([]: decl list) (* Note: "const int x = y - 1;" is legal, but we turn it into "const int x; x = y - 1;", which is not. Therefore, remove @@ -75,7 +87,97 @@ let local_variables = ref ([]: decl list) let remove_const env ty = remove_attributes_type env [AConst] ty -(* Process a variable declaration. +(* Process a compound literal "(ty) { init }". + At top-level, within an initializer for a global variable, + it gives rise to a static global definition of a fresh variable, + initialized with "init". The compound variable is replaced + by the fresh variable. + Within a function, it gives rise to a local variable + and an explicit initialization at the nearest sequence point. *) + +let process_compound_literal islocal env ty init = + let id = Env.fresh_ident "__compound" in + if islocal then begin + let ty' = remove_const env ty in + let e = {edesc = EVar id; etyp = ty'} in + local_variables := + (Storage_default, id, ty', None) :: !local_variables; + (local_initializer env e init [], e) + end else begin + global_variables := + (Storage_static, id, ty, Some init) :: !global_variables; + ([], {edesc = EVar id; etyp = ty}) + end + +(* Elimination of compound literals within an expression. + Compound literals are turned into fresh variables, recorded in + [local_variables] or [global_variables] depending on [islocal]. + For local variables, initializing assignments are added before + the expression and after sequence points in the expression. + Use only if [e] is a r-value. *) + +let rec expand_expr islocal env e = + let inits = ref [] in (* accumulator for initializing assignments *) + let rec expand e = + match e.edesc with + | EConst _ | ESizeof _ | EAlignof _ | EVar _ -> e + | EUnop(op, e1) -> + {edesc = EUnop(op, expand e1); etyp = e.etyp} + | EBinop(op, e1, e2, ty) -> + let e1' = expand e1 in + let e2' = + match op with + | Ocomma | Ologand | Ologor -> expand_expr islocal env e2 + (* Make sure the initializers of [e2] are performed in + sequential order, i.e. just before [e2] but after [e1]. *) + | _ -> expand e2 in + {edesc = EBinop(op, e1', e2', ty); etyp = e.etyp} + | EConditional(e1, e2, e3) -> + (* Same remark as above: initializers of [e2] and [e3] must + be performed after the conditional is resolved. *) + {edesc = EConditional(expand e1, + expand_expr islocal env e2, + expand_expr islocal env e3); + etyp = e.etyp} + | ECast(ty, e1) -> + {edesc = ECast(ty, expand e1); etyp = e.etyp} + | ECompound(ty, ie) -> + let ie' = expand_init islocal env ie in + let (l, e') = process_compound_literal islocal env ty ie' in + inits := l @ !inits; + e' + | ECall(e1, el) -> + {edesc = ECall(expand e1, List.map expand el); etyp = e.etyp} + in + let e' = expand e in add_inits_expr !inits e' + +(* Elimination of compound literals within an initializer. *) + +and expand_init islocal env i = + let rec expand i = + match i with + (* The following "flattening" is not C99. GCC documents it; whether + it implements it is unclear, Clang implements it. At any rate, + it makes it possible to use compound literals in static initializers, + something that is not possible in C99 because compound literals + are not constant expressions. + Note that flattening is done for structs and unions but not for + arrays, because a compound literal of array type in r-value position + decays to a pointer to its first element. *) + | Init_single {edesc = ECompound(_, ((Init_struct _ | Init_union _) as i))} -> + expand i + | Init_single e -> + Init_single (expand_expr islocal env e) + | Init_array il -> + Init_array (List.map expand il) + | Init_struct(id, flds) -> + Init_struct(id, List.map (fun (f, i) -> (f, expand i)) flds) + | Init_union(id, fld, i) -> + Init_union(id, fld, expand i) + in + expand i + +(* Process a block-scoped variable declaration. The variable is entered in [local_variables]. The initializer, if any, is converted into assignments and prepended to [k]. *) @@ -86,32 +188,41 @@ let process_decl loc env (sto, id, ty, optinit) k = match optinit with | None -> k | Some init -> - local_initializer loc env { edesc = EVar id; etyp = ty' } init k + let init' = expand_init true env init in + let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in + add_inits_stmt loc l k (* Simplification of blocks within a statement *) let rec unblock_stmt env s = match s.sdesc with | Sskip -> s - | Sdo e -> s + | Sdo e -> + {s with sdesc = Sdo(expand_expr true env e)} | Sseq(s1, s2) -> {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)} | Sif(e, s1, s2) -> - {s with sdesc = Sif(e, unblock_stmt env s1, unblock_stmt env s2)} + {s with sdesc = Sif(expand_expr true env e, + unblock_stmt env s1, unblock_stmt env s2)} | Swhile(e, s1) -> - {s with sdesc = Swhile(e, unblock_stmt env s1)} + {s with sdesc = Swhile(expand_expr true env e, unblock_stmt env s1)} | Sdowhile(s1, e) -> - {s with sdesc = Sdowhile(unblock_stmt env s1, e)} + {s with sdesc = Sdowhile(unblock_stmt env s1, expand_expr true env e)} | Sfor(s1, e, s2, s3) -> - {s with sdesc = Sfor(unblock_stmt env s1, e, unblock_stmt env s2, unblock_stmt env s3)} + {s with sdesc = Sfor(unblock_stmt env s1, + expand_expr true env e, + unblock_stmt env s2, + unblock_stmt env s3)} | Sbreak -> s | Scontinue -> s | Sswitch(e, s1) -> - {s with sdesc = Sswitch(e, unblock_stmt env s1)} + {s with sdesc = Sswitch(expand_expr true env e, unblock_stmt env s1)} | Slabeled(lbl, s1) -> {s with sdesc = Slabeled(lbl, unblock_stmt env s1)} | Sgoto lbl -> s - | Sreturn opte -> s + | Sreturn None -> s + | Sreturn (Some e) -> + {s with sdesc = Sreturn(Some (expand_expr true env e))} | Sblock sl -> unblock_block env sl | Sdecl d -> assert false | Sasm _ -> s @@ -123,7 +234,7 @@ and unblock_block env = function | s :: sl -> sseq s.sloc (unblock_stmt env s) (unblock_block env sl) -(* Simplification of blocks within a function *) +(* Simplification of blocks and compound literals within a function *) let unblock_fundef env f = local_variables := []; @@ -132,7 +243,45 @@ let unblock_fundef env f = local_variables := []; { f with fd_locals = f.fd_locals @ decls; fd_body = body } +(* Simplification of compound literals within a top-level declaration *) + +let unblock_decl loc env ((sto, id, ty, optinit) as d) = + match optinit with + | None -> [d] + | Some init -> + global_variables := []; + let init' = expand_init false env init in + let decls = !global_variables in + global_variables := []; + decls @ [(sto, id, ty, Some init')] + +(* Unblocking and simplification for whole files. + The environment is used for typedefs only, so we do not maintain + other declarations. *) + +let rec unblock_glob env accu = function + | [] -> List.rev accu + | g :: gl -> + match g.gdesc with + | Gdecl((sto, id, ty, init) as d) -> + let dl = unblock_decl g.gloc env d in + unblock_glob env + (List.rev_append + (List.map (fun d' -> {g with gdesc = Gdecl d'}) dl) + accu) + gl + | Gfundef f -> + let f' = unblock_fundef env f in + unblock_glob env ({g with gdesc = Gfundef f'} :: accu) gl + | Gtypedef(id, ty) -> + unblock_glob (Env.add_typedef env id ty) (g :: accu) gl + | Gcompositedecl _ + | Gcompositedef _ + | Genumdef _ + | Gpragma _ -> + unblock_glob env (g :: accu) gl + (* Entry point *) let program p = - Transform.program ~fundef:unblock_fundef p + unblock_glob (Builtins.environment()) [] p |