diff options
Diffstat (limited to 'exportclight/ExportClight.ml')
| -rw-r--r-- | exportclight/ExportClight.ml | 79 |
1 files changed, 55 insertions, 24 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 4ff901eb..742b3a5c 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -6,10 +6,11 @@ (* *) (* 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. *) +(* 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. *) (* *) (* *********************************************************************) @@ -89,23 +90,22 @@ let coqstring p s = exception Not_an_identifier +let sanitize_char = function + | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' as c -> c + | ' ' | '$' -> '_' + | _ -> raise Not_an_identifier + let sanitize s = - let s' = Bytes.create (String.length s) in - for i = 0 to String.length s - 1 do - Bytes.set s' i - (match String.get s i with - | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' as c -> c - | ' ' | '$' -> '_' - | _ -> raise Not_an_identifier) - done; - Bytes.to_string s' + if s <> "" + then "_" ^ String.map sanitize_char s + else "empty_ident" let temp_names : (ident, string) Hashtbl.t = Hashtbl.create 17 let ident p id = try let s = Hashtbl.find string_of_atom id in - fprintf p "_%s" (sanitize s) + fprintf p "%s" (sanitize s) with Not_found | Not_an_identifier -> try let s = Hashtbl.find temp_names id in @@ -124,10 +124,10 @@ let define_idents p = (fun (id, name) -> try if !use_canonical_atoms && id = pos_of_string name then - fprintf p "Definition _%s : ident := $\"%s\".@ " + fprintf p "Definition %s : ident := $\"%s\".@ " (sanitize name) name else - fprintf p "Definition _%s : ident := %a.@ " + fprintf p "Definition %s : ident := %a.@ " (sanitize name) positive id with Not_an_identifier -> ()); @@ -160,6 +160,22 @@ let attribute p a = a.attr_volatile (print_option coqN) a.attr_alignas +(* Raw int size and signedness *) + +let intsize p sz = + fprintf p "%s" + (match sz with + | I8 -> "I8" + | I16 -> "I16" + | I32 -> "I32" + | IBool -> "IBool") + +let signedness p sg = + fprintf p "%s" + (match sg with + | Signed -> "Signed" + | Unsigned -> "Unsigned") + (* Types *) let rec typ p t = @@ -216,8 +232,8 @@ and typlist p = function and callconv p cc = if cc = cc_default then fprintf p "cc_default" - else fprintf p "{|cc_vararg:=%b; cc_unproto:=%b; cc_structret:=%b|}" - cc.cc_vararg cc.cc_unproto cc.cc_structret + else fprintf p "{|cc_vararg:=%a; cc_unproto:=%b; cc_structret:=%b|}" + (print_option coqZ) cc.cc_vararg cc.cc_unproto cc.cc_structret (* External functions *) @@ -398,7 +414,7 @@ and lblstmts p = function (print_option coqZ) lbl stmt s lblstmts ls let print_function p (id, f) = - fprintf p "Definition f_%s := {|@ " (sanitize (extern_atom id)); + 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; @@ -419,7 +435,7 @@ let init_data p = function | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqptrofs ofs let print_variable p (id, v) = - fprintf p "Definition v_%s := {|@ " (sanitize (extern_atom id)); + fprintf p "Definition v%s := {|@ " (sanitize (extern_atom id)); fprintf p " gvar_info := %a;@ " typ v.gvar_info; fprintf p " gvar_init := %a;@ " (print_list init_data) v.gvar_init; fprintf p " gvar_readonly := %B;@ " v.gvar_readonly; @@ -434,20 +450,33 @@ let print_globdef p (id, gd) = let print_ident_globdef p = function | (id, Gfun(Ctypes.Internal f)) -> - fprintf p "(%a, Gfun(Internal f_%s))" ident id (sanitize (extern_atom id)) + fprintf p "(%a, Gfun(Internal f%s))" ident id (sanitize (extern_atom id)) | (id, Gfun(Ctypes.External(ef, targs, tres, cc))) -> fprintf p "@[<hov 2>(%a,@ @[<hov 2>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)) + fprintf p "(%a, Gvar v%s)" ident id (sanitize (extern_atom id)) (* Composite definitions *) +let print_member p = function + | Member_plain (id, ty) -> + fprintf p "@[<hov 2>Member_plain@ %a@ %a@]" + ident id typ ty + | Member_bitfield (id, sz, sg, a, width, pad) -> + fprintf p "@[<hov 2>Member_bitfield@ %a@ %a@ %a@ %a@ %a@ %B@]" + ident id + intsize sz + signedness sg + attribute a + coqZ width + pad + let print_composite_definition p (Composite(id, su, m, a)) = fprintf p "@[<hv 2>Composite %a %s@ %a@ %a@]" ident id (match su with Struct -> "Struct" | Union -> "Union") - (print_list (print_pair ident typ)) m + (print_list print_member) m attribute a (* The prologue *) @@ -455,8 +484,10 @@ let print_composite_definition p (Composite(id, su, m, a)) = 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 string_scope.\n\ +Local Open Scope clight_scope.\n" (* Naming the compiler-generated temporaries occurring in the program *) |