From d32955030937937706b71a96dc6584800f0b8722 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 16 Sep 2021 11:03:40 +0200 Subject: Refactor clightgen Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/ --- export/ExportClight.ml | 251 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 251 insertions(+) create mode 100644 export/ExportClight.ml (limited to 'export/ExportClight.ml') diff --git a/export/ExportClight.ml b/export/ExportClight.ml new file mode 100644 index 00000000..421db5ed --- /dev/null +++ b/export/ExportClight.ml @@ -0,0 +1,251 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Export Clight as a Coq file *) + +open Format +open Camlcoq +open AST +open! Ctypes +open Cop +open Clight +open ExportBase +open ExportCtypes + +(* Expressions *) + +let name_unop = function + | Onotbool -> "Onotbool" + | Onotint -> "Onotint" + | Oneg -> "Oneg" + | Oabsfloat -> "Oabsfloat" + +let name_binop = function + | Oadd -> "Oadd" + | Osub -> "Osub" + | Omul -> "Omul" + | Odiv -> "Odiv" + | Omod -> "Omod" + | Oand -> "Oand" + | Oor -> "Oor" + | Oxor -> "Oxor" + | Oshl -> "Oshl" + | Oshr -> "Oshr" + | Oeq -> "Oeq" + | Cop.One -> "One" + | Olt -> "Olt" + | Ogt -> "Ogt" + | Ole -> "Ole" + | Oge -> "Oge" + +let rec expr p = function + | Evar(id, t) -> + fprintf p "(Evar %a %a)" ident id typ t + | Etempvar(id, t) -> + fprintf p "(Etempvar %a %a)" ident id typ t + | Ederef(a1, t) -> + fprintf p "@[(Ederef@ %a@ %a)@]" expr a1 typ t + | Efield(a1, f, t) -> + fprintf p "@[(Efield@ %a@ %a@ %a)@]" expr a1 ident f typ t + | Econst_int(n, t) -> + fprintf p "(Econst_int %a %a)" coqint n typ t + | Econst_float(n, t) -> + fprintf p "(Econst_float %a %a)" coqfloat n typ t + | Econst_long(n, t) -> + fprintf p "(Econst_long %a %a)" coqint64 n typ t + | Econst_single(n, t) -> + fprintf p "(Econst_single %a %a)" coqsingle n typ t + | Eunop(op, a1, t) -> + fprintf p "@[(Eunop %s@ %a@ %a)@]" + (name_unop op) expr a1 typ t + | Eaddrof(a1, t) -> + fprintf p "@[(Eaddrof@ %a@ %a)@]" expr a1 typ t + | Ebinop(op, a1, a2, t) -> + fprintf p "@[(Ebinop %s@ %a@ %a@ %a)@]" + (name_binop op) expr a1 expr a2 typ t + | Ecast(a1, t) -> + fprintf p "@[(Ecast@ %a@ %a)@]" expr a1 typ t + | Esizeof(t1, t) -> + fprintf p "(Esizeof %a %a)" typ t1 typ t + | Ealignof(t1, t) -> + fprintf p "(Ealignof %a %a)" typ t1 typ t + +(* Statements *) + +let rec stmt p = function + | Sskip -> + fprintf p "Sskip" + | Sassign(e1, e2) -> + fprintf p "@[(Sassign@ %a@ %a)@]" expr e1 expr e2 + | Sset(id, e2) -> + fprintf p "@[(Sset %a@ %a)@]" ident id expr e2 + | Scall(optid, e1, el) -> + fprintf p "@[(Scall %a@ %a@ %a)@]" + (print_option ident) optid expr e1 (print_list expr) el + | Sbuiltin(optid, ef, tyl, el) -> + fprintf p "@[(Sbuiltin %a@ %a@ %a@ %a)@]" + (print_option ident) optid + external_function ef + typlist tyl + (print_list expr) el + | Ssequence(Sskip, s2) -> + stmt p s2 + | Ssequence(s1, Sskip) -> + stmt p s1 + | Ssequence(s1, s2) -> + fprintf p "@[(Ssequence@ %a@ %a)@]" stmt s1 stmt s2 + | Sifthenelse(e, s1, s2) -> + fprintf p "@[(Sifthenelse %a@ %a@ %a)@]" expr e stmt s1 stmt s2 + | Sloop (Ssequence (Sifthenelse(e, Sskip, Sbreak), s), Sskip) -> + fprintf p "@[(Swhile@ %a@ %a)@]" expr e stmt s + | Sloop (Ssequence (Ssequence(Sskip, Sifthenelse(e, Sskip, Sbreak)), s), Sskip) -> + fprintf p "@[(Swhile@ %a@ %a)@]" expr e stmt s + | Sloop(s1, s2) -> + fprintf p "@[(Sloop@ %a@ %a)@]" stmt s1 stmt s2 + | Sbreak -> + fprintf p "Sbreak" + | Scontinue -> + fprintf p "Scontinue" + | Sswitch(e, cases) -> + fprintf p "@[(Sswitch %a@ %a)@]" expr e lblstmts cases + | Sreturn e -> + fprintf p "@[(Sreturn %a)@]" (print_option expr) e + | Slabel(lbl, s1) -> + fprintf p "@[(Slabel %a@ %a)@]" ident lbl stmt s1 + | Sgoto lbl -> + fprintf p "(Sgoto %a)" ident lbl + +and lblstmts p = function + | LSnil -> + (fprintf p "LSnil") + | LScons(lbl, s, ls) -> + fprintf p "@[(LScons %a@ %a@ %a)@]" + (print_option coqZ) lbl stmt s lblstmts ls + +(* Global definitions *) + +let print_function p (id, f) = + fprintf p "Definition f%s := {|@ " (sanitize (extern_atom id)); + fprintf p " fn_return := %a;@ " typ f.fn_return; + fprintf p " fn_callconv := %a;@ " callconv f.fn_callconv; + fprintf p " fn_params := %a;@ " (print_list (print_pair ident typ)) f.fn_params; + fprintf p " fn_vars := %a;@ " (print_list (print_pair ident typ)) f.fn_vars; + fprintf p " fn_temps := %a;@ " (print_list (print_pair ident typ)) f.fn_temps; + fprintf p " fn_body :=@ "; + stmt p f.fn_body; + fprintf p "@ |}.@ @ " + +let print_globdef p (id, gd) = + match gd with + | Gfun(Ctypes.Internal f) -> print_function p (id, f) + | Gfun(Ctypes.External _) -> () + | Gvar v -> print_variable typ p (id, v) + +let print_ident_globdef p = function + | (id, Gfun(Ctypes.Internal f)) -> + fprintf p "(%a, Gfun(Internal f%s))" ident id (sanitize (extern_atom id)) + | (id, Gfun(Ctypes.External(ef, targs, tres, cc))) -> + fprintf p "@[(%a,@ @[Gfun(External %a@ %a@ %a@ %a))@]@]" + ident id external_function ef typlist targs typ tres callconv cc + | (id, Gvar v) -> + fprintf p "(%a, Gvar v%s)" ident id (sanitize (extern_atom id)) + +(* The prologue *) + +let prologue = "\ +From Coq Require Import String List ZArith.\n\ +From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\ +Import Clightdefs.ClightNotations.\n\ +Local Open Scope Z_scope.\n\ +Local Open Scope string_scope.\n\ +Local Open Scope clight_scope.\n" + +(* Naming the compiler-generated temporaries occurring in the program *) + +let rec name_expr = function + | Evar(id, t) -> () + | Etempvar(id, t) -> name_temporary id + | Ederef(a1, t) -> name_expr a1 + | Efield(a1, f, t) -> name_expr a1 + | Econst_int(n, t) -> () + | Econst_float(n, t) -> () + | Econst_long(n, t) -> () + | Econst_single(n, t) -> () + | Eunop(op, a1, t) -> name_expr a1 + | Eaddrof(a1, t) -> name_expr a1 + | Ebinop(op, a1, a2, t) -> name_expr a1; name_expr a2 + | Ecast(a1, t) -> name_expr a1 + | Esizeof(t1, t) -> () + | Ealignof(t1, t) -> () + +let rec name_stmt = function + | Sskip -> () + | Sassign(e1, e2) -> name_expr e1; name_expr e2 + | Sset(id, e2) -> name_temporary id; name_expr e2 + | Scall(optid, e1, el) -> + name_opt_temporary optid; name_expr e1; List.iter name_expr el + | Sbuiltin(optid, ef, tyl, el) -> + name_opt_temporary optid; List.iter name_expr el + | Ssequence(s1, s2) -> name_stmt s1; name_stmt s2 + | Sifthenelse(e, s1, s2) -> name_expr e; name_stmt s1; name_stmt s2 + | Sloop(s1, s2) -> name_stmt s1; name_stmt s2 + | Sbreak -> () + | Scontinue -> () + | Sswitch(e, cases) -> name_expr e; name_lblstmts cases + | Sreturn (Some e) -> name_expr e + | Sreturn None -> () + | Slabel(lbl, s1) -> name_stmt s1 + | Sgoto lbl -> () + +and name_lblstmts = function + | LSnil -> () + | LScons(lbl, s, ls) -> name_stmt s; name_lblstmts ls + +let name_function f = + List.iter (fun (id, ty) -> name_temporary id) f.fn_temps; + name_stmt f.fn_body + +let name_globdef (id, g) = + match g with + | Gfun(Ctypes.Internal f) -> name_function f + | _ -> () + +let name_program p = + List.iter name_globdef p.Ctypes.prog_defs + +(* All together *) + +let print_program p prog sourcefile normalized = + Hashtbl.clear temp_names; + name_program prog; + fprintf p "@["; + fprintf p "%s" prologue; + print_clightgen_info ~sourcefile ~normalized p; + define_idents p; + List.iter (print_globdef p) prog.Ctypes.prog_defs; + fprintf p "Definition composites : list composite_definition :=@ "; + print_list print_composite_definition p prog.prog_types; + fprintf p ".@ @ "; + fprintf p "Definition global_definitions : list (ident * globdef fundef type) :=@ "; + print_list print_ident_globdef p prog.Ctypes.prog_defs; + fprintf p ".@ @ "; + fprintf p "Definition public_idents : list ident :=@ "; + print_list ident p prog.Ctypes.prog_public; + fprintf p ".@ @ "; + fprintf p "Definition prog : Clight.program := @ "; + fprintf p " mkprogram composites global_definitions public_idents %a Logic.I.@ @ " + ident prog.Ctypes.prog_main; + fprintf p "@]@." -- cgit