diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-23 09:33:59 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-01-23 09:33:59 +0100 |
commit | d594c5da5e11fb10775c2b772961b8a2383887c7 (patch) | |
tree | 750ed5d4a0829519a258f3c12f7d518e53504487 /cfrontend/PrintClight.ml | |
parent | 1e97bb4f6297b6fa7949684e522a592aab754d99 (diff) | |
parent | 2dd864217cc864d44e828a4d14dd45668e4ab095 (diff) | |
download | compcert-d594c5da5e11fb10775c2b772961b8a2383887c7.tar.gz compcert-d594c5da5e11fb10775c2b772961b8a2383887c7.zip |
Merge branch 'named-structs'
- Switch CompCert C / Clight AST of composite types (structs and unions)
from a structural representation to a nominal representation,
closer to concrete syntax.
- This avoids algorithmic inefficiencies due to the structural representation.
- Closes PR#4.
- Smallstep: make small-step semantics more polymorphic in the type of the
global environment.
- Globalenvs: introduce Senv.t (symbol environments) as a restricted view
on Genv.t (full global environments).
- Events, Smallstep: use Senv instead of Genv to talk about global names.
Diffstat (limited to 'cfrontend/PrintClight.ml')
-rw-r--r-- | cfrontend/PrintClight.ml | 71 |
1 files changed, 8 insertions, 63 deletions
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index c5a6e6e1..ebd06c54 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -45,6 +45,8 @@ let rec precedence = function | Econst_float _ -> (16, NA) | Econst_single _ -> (16, NA) | Econst_long _ -> (16, NA) + | Esizeof _ -> (15, RtoL) + | Ealignof _ -> (15, RtoL) | Eunop _ -> (15, RtoL) | Eaddrof _ -> (15, RtoL) | Ecast _ -> (14, RtoL) @@ -100,6 +102,10 @@ let rec expr p (prec, e) = expr (prec1, a1) (name_binop op) expr (prec2, a2) | Ecast(a1, ty) -> fprintf p "(%s) %a" (name_type ty) expr (prec', a1) + | Esizeof(ty, _) -> + fprintf p "sizeof(%s)" (name_type ty) + | Ealignof(ty, _) -> + fprintf p "__alignof__(%s)" (name_type ty) end; if prec' < prec then fprintf p ")@]" else fprintf p "@]" @@ -265,71 +271,10 @@ let print_globdef p (id, gd) = | Gfun f -> print_fundef p id f | Gvar v -> print_globvar p id v (* from PrintCsyntax *) -(* Collect struct and union types *) - -let rec collect_expr e = - collect_type (typeof e); - match e with - | Econst_int _ -> () - | Econst_float _ -> () - | Econst_single _ -> () - | Econst_long _ -> () - | Evar _ -> () - | Etempvar _ -> () - | Ederef(r, _) -> collect_expr r - | Efield(l, _, _) -> collect_expr l - | Eaddrof(l, _) -> collect_expr l - | Eunop(_, r, _) -> collect_expr r - | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2 - | Ecast(r, _) -> collect_expr r - -let rec collect_exprlist = function - | [] -> () - | r1 :: rl -> collect_expr r1; collect_exprlist rl - -let rec collect_stmt = function - | Sskip -> () - | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 - | Sset(id, e2) -> collect_expr e2 - | Scall(optid, e1, el) -> collect_expr e1; collect_exprlist el - | Sbuiltin(optid, ef, tyargs, el) -> collect_exprlist el - | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 - | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 - | Sloop(s1, s2) -> collect_stmt s1; collect_stmt s2 - | Sbreak -> () - | Scontinue -> () - | Sswitch(e, cases) -> collect_expr e; collect_cases cases - | Sreturn None -> () - | Sreturn (Some e) -> collect_expr e - | Slabel(lbl, s) -> collect_stmt s - | Sgoto lbl -> () - -and collect_cases = function - | LSnil -> () - | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem - -let collect_function f = - collect_type f.fn_return; - List.iter (fun (id, ty) -> collect_type ty) f.fn_params; - List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; - List.iter (fun (id, ty) -> collect_type ty) f.fn_temps; - collect_stmt f.fn_body - -let collect_globdef (id, gd) = - match gd with - | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res - | Gfun(Internal f) -> collect_function f - | Gvar v -> collect_type v.gvar_info - -let collect_program p = - List.iter collect_globdef p.prog_defs - let print_program p prog = - struct_unions := StructUnion.empty; - collect_program prog; fprintf p "@[<v 0>"; - StructUnion.iter (declare_struct_or_union p) !struct_unions; - StructUnion.iter (print_struct_or_union p) !struct_unions; + List.iter (declare_composite p) prog.prog_types; + List.iter (define_composite p) prog.prog_types; List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." |