From 47fae389c800034e002c9f8a398e9adc79a14b81 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 May 2021 18:07:02 +0200 Subject: Native support for bit fields (#400) This big PR adds support for bit fields in structs and unions to the verified part of CompCert, namely the CompCert C and Clight languages. The compilation of bit field accesses to normal integer accesses + shifts and masks is done and proved correct as part of the Cshmgen pass. The layout of bit fields in memory is done by the functions in module Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic soundness properties of the layout are shown, such as "two different bit fields do not overlap" or "a bit field and a regular field do not overlap". All this replaces the previous emulation of bit fields by source-to-source rewriting in the unverified front-end of CompCert (module cparse/Bitfield.ml). This emulation was prone to errors (see nonstandard layout instead. The core idea for the PR is that expressions in l-value position denote not just a block, a byte offset and a type, but also a bitfield designator saying whether all the bits of the type are accessed (designator Full) or only some of its bits (designator Bits). Designators of the Bits kind appear when the l-value is a bit field access; the bit width and bit offset in Bits are computed by the functions in Ctypes that implement the layout algorithm. Consequently, both in the semantics of CompCert C and Clight and in the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a type and a bitfield designator are used in a number of places where a single type was used before. The introduction of bit fields has a big impact on static initialization (module cfrontend/Initializers.v), which had to be rewritten in large part, along with its soundness proof (cfrontend/Initializersproof.v). Both static initialization and run-time manipulation of bit fields are tested in test/abi using differential testing against GCC and randomly-generated structs. This work exposed subtle interactions between bit fields and the volatile modifier. Currently, the volatile modifier is ignored when accessing a bit field (and a warning is printed at compile-time), just like it is ignored when accessing a struct or union as a r-value. Currently, the natural alignment of bit fields and their storage units cannot be modified with the aligned attribute. _Alignas on bit fields is rejected as per C11, and the packed modifier cannot be applied to a struct containing bit fields. --- exportclight/ExportClight.ml | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) (limited to 'exportclight') diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 474a1bd8..ced07427 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -161,6 +161,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 = @@ -444,11 +460,24 @@ let print_ident_globdef p = function (* Composite definitions *) +let print_member p = function + | Member_plain (id, ty) -> + fprintf p "@[Member_plain@ %a@ %a@]" + ident id typ ty + | Member_bitfield (id, sz, sg, a, width, pad) -> + fprintf p "@[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 "@[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 *) -- cgit From 8eaff6bf3933f2213ae85584009e05123c40fa65 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Sep 2021 10:47:14 +0200 Subject: clightgen: handle empty names given to padding bit fields In the Clight AST, padding bit fields (such as `int : 6;`) in composite declarations are given an ident that corresponds to the empty string. Previously, clightgen would give name `_` to this ident, but this is not valid Coq. This commit gives name `empty_ident` to the empty ident. This name does not start with an underscore, so it cannot conflict with the names for regular idents, which all start with `_`. --- exportclight/ExportClight.ml | 31 +++++++++++++++---------------- 1 file changed, 15 insertions(+), 16 deletions(-) (limited to 'exportclight') diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index ced07427..742b3a5c 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -90,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 @@ -125,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 -> ()); @@ -415,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; @@ -436,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; @@ -451,12 +450,12 @@ 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 "@[(%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)) + fprintf p "(%a, Gvar v%s)" ident id (sanitize (extern_atom id)) (* Composite definitions *) -- cgit 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/ --- exportclight/Clightdefs.v | 304 ---------------------- exportclight/Clightgen.ml | 201 --------------- exportclight/Clightnorm.ml | 178 ------------- exportclight/ExportClight.ml | 584 ------------------------------------------- exportclight/README.md | 33 --- 5 files changed, 1300 deletions(-) delete mode 100644 exportclight/Clightdefs.v delete mode 100644 exportclight/Clightgen.ml delete mode 100644 exportclight/Clightnorm.ml delete mode 100644 exportclight/ExportClight.ml delete mode 100644 exportclight/README.md (limited to 'exportclight') diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v deleted file mode 100644 index 708be1cb..00000000 --- a/exportclight/Clightdefs.v +++ /dev/null @@ -1,304 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(** All imports and definitions used by .v Clight files generated by clightgen *) - -From Coq Require Import Ascii String List ZArith. -From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight. - -(** ** Short names for types *) - -Definition tvoid := Tvoid. -Definition tschar := Tint I8 Signed noattr. -Definition tuchar := Tint I8 Unsigned noattr. -Definition tshort := Tint I16 Signed noattr. -Definition tushort := Tint I16 Unsigned noattr. -Definition tint := Tint I32 Signed noattr. -Definition tuint := Tint I32 Unsigned noattr. -Definition tbool := Tint IBool Unsigned noattr. -Definition tlong := Tlong Signed noattr. -Definition tulong := Tlong Unsigned noattr. -Definition tfloat := Tfloat F32 noattr. -Definition tdouble := Tfloat F64 noattr. -Definition tptr (t: type) := Tpointer t noattr. -Definition tarray (t: type) (sz: Z) := Tarray t sz noattr. - -Definition volatile_attr := {| attr_volatile := true; attr_alignas := None |}. - -Definition tattr (a: attr) (ty: type) := - match ty with - | Tvoid => Tvoid - | Tint sz si _ => Tint sz si a - | Tlong si _ => Tlong si a - | Tfloat sz _ => Tfloat sz a - | Tpointer elt _ => Tpointer elt a - | Tarray elt sz _ => Tarray elt sz a - | Tfunction args res cc => Tfunction args res cc - | Tstruct id _ => Tstruct id a - | Tunion id _ => Tunion id a - end. - -Definition tvolatile (ty: type) := tattr volatile_attr ty. - -Definition talignas (n: N) (ty: type) := - tattr {| attr_volatile := false; attr_alignas := Some n |} ty. - -Definition tvolatile_alignas (n: N) (ty: type) := - tattr {| attr_volatile := true; attr_alignas := Some n |} ty. - -(** ** Constructor for programs and compilation units *) - -Definition wf_composites (types: list composite_definition) : Prop := - match build_composite_env types with OK _ => True | Error _ => False end. - -Definition build_composite_env' (types: list composite_definition) - (WF: wf_composites types) - : { ce | build_composite_env types = OK ce }. -Proof. - revert WF. unfold wf_composites. case (build_composite_env types); intros. -- exists c; reflexivity. -- contradiction. -Defined. - -Definition mkprogram (types: list composite_definition) - (defs: list (ident * globdef fundef type)) - (public: list ident) - (main: ident) - (WF: wf_composites types) : Clight.program := - let (ce, EQ) := build_composite_env' types WF in - {| prog_defs := defs; - prog_public := public; - prog_main := main; - prog_types := types; - prog_comp_env := ce; - prog_comp_env_eq := EQ |}. - -(** ** Encoding character strings as positive numbers *) - -(** The following encoding of character strings as positive numbers - must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *) - -Definition append_bit_pos (b: bool) (p: positive) : positive := - if b then xI p else xO p. - -Definition append_char_pos_default (c: ascii) (p: positive) : positive := - let '(Ascii b7 b6 b5 b4 b3 b2 b1 b0) := c in - xI (xI (xI (xI (xI (xI - (append_bit_pos b0 (append_bit_pos b1 - (append_bit_pos b2 (append_bit_pos b3 - (append_bit_pos b4 (append_bit_pos b5 - (append_bit_pos b6 (append_bit_pos b7 p))))))))))))). - -Definition append_char_pos (c: ascii) (p: positive) : positive := - match c with - | "0"%char => xO (xO (xO (xO (xO (xO p))))) - | "1"%char => xI (xO (xO (xO (xO (xO p))))) - | "2"%char => xO (xI (xO (xO (xO (xO p))))) - | "3"%char => xI (xI (xO (xO (xO (xO p))))) - | "4"%char => xO (xO (xI (xO (xO (xO p))))) - | "5"%char => xI (xO (xI (xO (xO (xO p))))) - | "6"%char => xO (xI (xI (xO (xO (xO p))))) - | "7"%char => xI (xI (xI (xO (xO (xO p))))) - | "8"%char => xO (xO (xO (xI (xO (xO p))))) - | "9"%char => xI (xO (xO (xI (xO (xO p))))) - | "a"%char => xO (xI (xO (xI (xO (xO p))))) - | "b"%char => xI (xI (xO (xI (xO (xO p))))) - | "c"%char => xO (xO (xI (xI (xO (xO p))))) - | "d"%char => xI (xO (xI (xI (xO (xO p))))) - | "e"%char => xO (xI (xI (xI (xO (xO p))))) - | "f"%char => xI (xI (xI (xI (xO (xO p))))) - | "g"%char => xO (xO (xO (xO (xI (xO p))))) - | "h"%char => xI (xO (xO (xO (xI (xO p))))) - | "i"%char => xO (xI (xO (xO (xI (xO p))))) - | "j"%char => xI (xI (xO (xO (xI (xO p))))) - | "k"%char => xO (xO (xI (xO (xI (xO p))))) - | "l"%char => xI (xO (xI (xO (xI (xO p))))) - | "m"%char => xO (xI (xI (xO (xI (xO p))))) - | "n"%char => xI (xI (xI (xO (xI (xO p))))) - | "o"%char => xO (xO (xO (xI (xI (xO p))))) - | "p"%char => xI (xO (xO (xI (xI (xO p))))) - | "q"%char => xO (xI (xO (xI (xI (xO p))))) - | "r"%char => xI (xI (xO (xI (xI (xO p))))) - | "s"%char => xO (xO (xI (xI (xI (xO p))))) - | "t"%char => xI (xO (xI (xI (xI (xO p))))) - | "u"%char => xO (xI (xI (xI (xI (xO p))))) - | "v"%char => xI (xI (xI (xI (xI (xO p))))) - | "w"%char => xO (xO (xO (xO (xO (xI p))))) - | "x"%char => xI (xO (xO (xO (xO (xI p))))) - | "y"%char => xO (xI (xO (xO (xO (xI p))))) - | "z"%char => xI (xI (xO (xO (xO (xI p))))) - | "A"%char => xO (xO (xI (xO (xO (xI p))))) - | "B"%char => xI (xO (xI (xO (xO (xI p))))) - | "C"%char => xO (xI (xI (xO (xO (xI p))))) - | "D"%char => xI (xI (xI (xO (xO (xI p))))) - | "E"%char => xO (xO (xO (xI (xO (xI p))))) - | "F"%char => xI (xO (xO (xI (xO (xI p))))) - | "G"%char => xO (xI (xO (xI (xO (xI p))))) - | "H"%char => xI (xI (xO (xI (xO (xI p))))) - | "I"%char => xO (xO (xI (xI (xO (xI p))))) - | "J"%char => xI (xO (xI (xI (xO (xI p))))) - | "K"%char => xO (xI (xI (xI (xO (xI p))))) - | "L"%char => xI (xI (xI (xI (xO (xI p))))) - | "M"%char => xO (xO (xO (xO (xI (xI p))))) - | "N"%char => xI (xO (xO (xO (xI (xI p))))) - | "O"%char => xO (xI (xO (xO (xI (xI p))))) - | "P"%char => xI (xI (xO (xO (xI (xI p))))) - | "Q"%char => xO (xO (xI (xO (xI (xI p))))) - | "R"%char => xI (xO (xI (xO (xI (xI p))))) - | "S"%char => xO (xI (xI (xO (xI (xI p))))) - | "T"%char => xI (xI (xI (xO (xI (xI p))))) - | "U"%char => xO (xO (xO (xI (xI (xI p))))) - | "V"%char => xI (xO (xO (xI (xI (xI p))))) - | "W"%char => xO (xI (xO (xI (xI (xI p))))) - | "X"%char => xI (xI (xO (xI (xI (xI p))))) - | "Y"%char => xO (xO (xI (xI (xI (xI p))))) - | "Z"%char => xI (xO (xI (xI (xI (xI p))))) - | "_"%char => xO (xI (xI (xI (xI (xI p))))) - | _ => append_char_pos_default c p - end. - -Fixpoint ident_of_string (s: string) : ident := - match s with - | EmptyString => xH - | String c s => append_char_pos c (ident_of_string s) - end. - -(** The inverse conversion, from encoded strings to strings *) - -Section DECODE_BITS. - -Variable rec: positive -> string. - -Fixpoint decode_n_bits (n: nat) (l: list bool) (p: positive) : string := - match n with - | O => - match l with - | b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: _ => - String (Ascii b7 b6 b5 b4 b3 b2 b1 b0) (rec p) - | _ => EmptyString - end - | S n => - match p with - | xO q => decode_n_bits n (false :: l) q - | xI q => decode_n_bits n (true :: l) q - | xH => EmptyString - end - end. - -Definition decode_8_bits := Eval compute in (decode_n_bits 8%nat nil). - -End DECODE_BITS. - -Fixpoint string_of_ident (p: positive) : string := - match p with - | xO (xO (xO (xO (xO (xO p))))) => String "0"%char (string_of_ident p) - | xI (xO (xO (xO (xO (xO p))))) => String "1"%char (string_of_ident p) - | xO (xI (xO (xO (xO (xO p))))) => String "2"%char (string_of_ident p) - | xI (xI (xO (xO (xO (xO p))))) => String "3"%char (string_of_ident p) - | xO (xO (xI (xO (xO (xO p))))) => String "4"%char (string_of_ident p) - | xI (xO (xI (xO (xO (xO p))))) => String "5"%char (string_of_ident p) - | xO (xI (xI (xO (xO (xO p))))) => String "6"%char (string_of_ident p) - | xI (xI (xI (xO (xO (xO p))))) => String "7"%char (string_of_ident p) - | xO (xO (xO (xI (xO (xO p))))) => String "8"%char (string_of_ident p) - | xI (xO (xO (xI (xO (xO p))))) => String "9"%char (string_of_ident p) - | xO (xI (xO (xI (xO (xO p))))) => String "a"%char (string_of_ident p) - | xI (xI (xO (xI (xO (xO p))))) => String "b"%char (string_of_ident p) - | xO (xO (xI (xI (xO (xO p))))) => String "c"%char (string_of_ident p) - | xI (xO (xI (xI (xO (xO p))))) => String "d"%char (string_of_ident p) - | xO (xI (xI (xI (xO (xO p))))) => String "e"%char (string_of_ident p) - | xI (xI (xI (xI (xO (xO p))))) => String "f"%char (string_of_ident p) - | xO (xO (xO (xO (xI (xO p))))) => String "g"%char (string_of_ident p) - | xI (xO (xO (xO (xI (xO p))))) => String "h"%char (string_of_ident p) - | xO (xI (xO (xO (xI (xO p))))) => String "i"%char (string_of_ident p) - | xI (xI (xO (xO (xI (xO p))))) => String "j"%char (string_of_ident p) - | xO (xO (xI (xO (xI (xO p))))) => String "k"%char (string_of_ident p) - | xI (xO (xI (xO (xI (xO p))))) => String "l"%char (string_of_ident p) - | xO (xI (xI (xO (xI (xO p))))) => String "m"%char (string_of_ident p) - | xI (xI (xI (xO (xI (xO p))))) => String "n"%char (string_of_ident p) - | xO (xO (xO (xI (xI (xO p))))) => String "o"%char (string_of_ident p) - | xI (xO (xO (xI (xI (xO p))))) => String "p"%char (string_of_ident p) - | xO (xI (xO (xI (xI (xO p))))) => String "q"%char (string_of_ident p) - | xI (xI (xO (xI (xI (xO p))))) => String "r"%char (string_of_ident p) - | xO (xO (xI (xI (xI (xO p))))) => String "s"%char (string_of_ident p) - | xI (xO (xI (xI (xI (xO p))))) => String "t"%char (string_of_ident p) - | xO (xI (xI (xI (xI (xO p))))) => String "u"%char (string_of_ident p) - | xI (xI (xI (xI (xI (xO p))))) => String "v"%char (string_of_ident p) - | xO (xO (xO (xO (xO (xI p))))) => String "w"%char (string_of_ident p) - | xI (xO (xO (xO (xO (xI p))))) => String "x"%char (string_of_ident p) - | xO (xI (xO (xO (xO (xI p))))) => String "y"%char (string_of_ident p) - | xI (xI (xO (xO (xO (xI p))))) => String "z"%char (string_of_ident p) - | xO (xO (xI (xO (xO (xI p))))) => String "A"%char (string_of_ident p) - | xI (xO (xI (xO (xO (xI p))))) => String "B"%char (string_of_ident p) - | xO (xI (xI (xO (xO (xI p))))) => String "C"%char (string_of_ident p) - | xI (xI (xI (xO (xO (xI p))))) => String "D"%char (string_of_ident p) - | xO (xO (xO (xI (xO (xI p))))) => String "E"%char (string_of_ident p) - | xI (xO (xO (xI (xO (xI p))))) => String "F"%char (string_of_ident p) - | xO (xI (xO (xI (xO (xI p))))) => String "G"%char (string_of_ident p) - | xI (xI (xO (xI (xO (xI p))))) => String "H"%char (string_of_ident p) - | xO (xO (xI (xI (xO (xI p))))) => String "I"%char (string_of_ident p) - | xI (xO (xI (xI (xO (xI p))))) => String "J"%char (string_of_ident p) - | xO (xI (xI (xI (xO (xI p))))) => String "K"%char (string_of_ident p) - | xI (xI (xI (xI (xO (xI p))))) => String "L"%char (string_of_ident p) - | xO (xO (xO (xO (xI (xI p))))) => String "M"%char (string_of_ident p) - | xI (xO (xO (xO (xI (xI p))))) => String "N"%char (string_of_ident p) - | xO (xI (xO (xO (xI (xI p))))) => String "O"%char (string_of_ident p) - | xI (xI (xO (xO (xI (xI p))))) => String "P"%char (string_of_ident p) - | xO (xO (xI (xO (xI (xI p))))) => String "Q"%char (string_of_ident p) - | xI (xO (xI (xO (xI (xI p))))) => String "R"%char (string_of_ident p) - | xO (xI (xI (xO (xI (xI p))))) => String "S"%char (string_of_ident p) - | xI (xI (xI (xO (xI (xI p))))) => String "T"%char (string_of_ident p) - | xO (xO (xO (xI (xI (xI p))))) => String "U"%char (string_of_ident p) - | xI (xO (xO (xI (xI (xI p))))) => String "V"%char (string_of_ident p) - | xO (xI (xO (xI (xI (xI p))))) => String "W"%char (string_of_ident p) - | xI (xI (xO (xI (xI (xI p))))) => String "X"%char (string_of_ident p) - | xO (xO (xI (xI (xI (xI p))))) => String "Y"%char (string_of_ident p) - | xI (xO (xI (xI (xI (xI p))))) => String "Z"%char (string_of_ident p) - | xO (xI (xI (xI (xI (xI p))))) => String "_"%char (string_of_ident p) - | xI (xI (xI (xI (xI (xI p))))) => decode_8_bits string_of_ident p - | _ => EmptyString - end. - -Lemma string_of_ident_of_string: - forall s, string_of_ident (ident_of_string s) = s. -Proof. - induction s as [ | c s]; simpl. -- auto. -- rewrite <- IHs at 2. destruct c as [[] [] [] [] [] [] [] []]; reflexivity. -Qed. - -Corollary ident_of_string_injective: - forall s1 s2, ident_of_string s1 = ident_of_string s2 -> s1 = s2. -Proof. - intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2). - congruence. -Qed. - -(** ** Notations *) - -Module ClightNotations. - -(** A convenient notation [$ "ident"] to force evaluation of - [ident_of_string "ident"] *) - -Ltac ident_of_string s := - let x := constr:(ident_of_string s) in - let y := eval compute in x in - exact y. - -Notation "$ s" := (ltac:(ident_of_string s)) - (at level 1, only parsing) : clight_scope. - -End ClightNotations. diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml deleted file mode 100644 index 44c76cc6..00000000 --- a/exportclight/Clightgen.ml +++ /dev/null @@ -1,201 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -open Printf -open Commandline -open Clflags -open CommonOptions -open Driveraux -open Frontend -open Diagnostics - -let tool_name = "Clight generator" - -(* clightgen-specific options *) - -let option_normalize = ref false - -(* From CompCert C AST to Clight *) - -let compile_c_ast sourcename csyntax ofile = - let loc = file_loc sourcename in - let clight = - match SimplExpr.transl_program csyntax with - | Errors.OK p -> - begin match SimplLocals.transf_program p with - | Errors.OK p' -> - if !option_normalize - then Clightnorm.norm_program p' - else p' - | Errors.Error msg -> - fatal_error loc "%a" print_error msg - end - | Errors.Error msg -> - fatal_error loc "%a" print_error msg in - (* Dump Clight in C syntax if requested *) - PrintClight.print_if_2 clight; - (* Print Clight in Coq syntax *) - let oc = open_out ofile in - ExportClight.print_program (Format.formatter_of_out_channel oc) - clight sourcename !option_normalize; - close_out oc - -(* From C source to Clight *) - -let compile_c_file sourcename ifile ofile = - let set_dest dst opt ext = - dst := if !opt then Some (output_filename sourcename ".c" ext) - else None in - set_dest Cprint.destination option_dparse ".parsed.c"; - set_dest PrintCsyntax.destination option_dcmedium ".compcert.c"; - set_dest PrintClight.destination option_dclight ".light.c"; - compile_c_ast sourcename (parse_c_file sourcename ifile) ofile - -let output_filename sourcename suff = - let prefixname = Filename.chop_suffix sourcename suff in - output_filename_default (prefixname ^ ".v") - -(* Processing of a .c file *) - -let process_c_file sourcename = - ensure_inputfile_exists sourcename; - let ofile = output_filename sourcename ".c" in - if !option_E then begin - preprocess sourcename "-" - end else begin - let preproname = if !option_dprepro then - Driveraux.output_filename sourcename ".c" ".i" - else - Driveraux.tmp_file ".i" in - preprocess sourcename preproname; - compile_c_file sourcename preproname ofile - end - -(* Processing of a .i file *) - -let process_i_file sourcename = - ensure_inputfile_exists sourcename; - let ofile = output_filename sourcename ".i" in - compile_c_file sourcename sourcename ofile - -let usage_string = - version_string tool_name ^ -{|Usage: clightgen [options] -Recognized source files: - .c C source file - .i or .p C source file that should not be preprocessed -Processing options: - -normalize Normalize the generated Clight code w.r.t. loads in expressions - -canonical-idents Use canonical numbers to represent identifiers (default) - -short-idents Use small, non-canonical numbers to represent identifiers - -E Preprocess only, send result to standard output - -o Generate output in -|} ^ -prepro_help ^ -language_support_help ^ -{|Tracing options: - -dprepro Save C file after preprocessing in .i - -dparse Save C file after parsing and elaboration in .parsed.c - -dc Save generated Compcert C in .compcert.c - -dclight Save generated Clight in .light.c - -dall Save all generated intermediate files in . -|} ^ - general_help ^ - warning_help - - -let print_usage_and_exit () = - printf "%s" usage_string; exit 0 - -let set_all opts () = List.iter (fun r -> r := true) opts -let unset_all opts () = List.iter (fun r -> r := false) opts - -let actions : ((string -> unit) * string) list ref = ref [] -let push_action fn arg = - actions := (fn, arg) :: !actions - -let perform_actions () = - let rec perform = function - | [] -> () - | (fn,arg) :: rem -> fn arg; perform rem - in perform (List.rev !actions) - -let num_input_files = ref 0 - -let cmdline_actions = - [ -(* Getting help *) - Exact "-help", Unit print_usage_and_exit; - Exact "--help", Unit print_usage_and_exit;] - (* Getting version info *) - @ version_options tool_name @ -(* Processing options *) - [ Exact "-E", Set option_E; - Exact "-normalize", Set option_normalize; - Exact "-canonical-idents", Set Camlcoq.use_canonical_atoms; - Exact "-short-idents", Unset Camlcoq.use_canonical_atoms; - Exact "-o", String(fun s -> option_o := Some s); - Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in - option_o := Some s);] -(* Preprocessing options *) - @ prepro_actions @ -(* Tracing options *) - [ Exact "-dprepro", Set option_dprepro; - Exact "-dparse", Set option_dparse; - Exact "-dc", Set option_dcmedium; - Exact "-dclight", Set option_dclight; - Exact "-dall", Self (fun _ -> - option_dprepro := true; - option_dparse := true; - option_dcmedium := true; - option_dclight := true;); - ] - @ general_options -(* Diagnostic options *) - @ warning_options - @ language_support_options @ -(* Catch options that are not handled *) - [Prefix "-", Self (fun s -> - fatal_error no_loc "Unknown option `%s'" s); -(* File arguments *) - Suffix ".c", Self (fun s -> - incr num_input_files; push_action process_c_file s); - Suffix ".i", Self (fun s -> - incr num_input_files; push_action process_i_file s); - Suffix ".p", Self (fun s -> - incr num_input_files; push_action process_i_file s); - ] - -let _ = -try - Gc.set { (Gc.get()) with - Gc.minor_heap_size = 524288; (* 512k *) - Gc.major_heap_increment = 4194304 (* 4M *) - }; - Printexc.record_backtrace true; - Camlcoq.use_canonical_atoms := true; - Frontend.init (); - parse_cmdline cmdline_actions; - if !option_o <> None && !num_input_files >= 2 then - fatal_error no_loc "Ambiguous '-o' option (multiple source files)"; - if !num_input_files = 0 then - fatal_error no_loc "no input file"; - perform_actions () -with - | Sys_error msg - | CmdError msg -> error no_loc "%s" msg; exit 2 - | Abort -> exit 2 - | e -> crash e diff --git a/exportclight/Clightnorm.ml b/exportclight/Clightnorm.ml deleted file mode 100644 index 88d44c08..00000000 --- a/exportclight/Clightnorm.ml +++ /dev/null @@ -1,178 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(** Clight-to-Clight rewriting to name memory loads *) - -(* The effect of this rewriting is to ensure that Clight expressions - whose evaluation involves a memory load (i.e. a lvalue-to-rvalue - conversion with By_value access mode) are always bound to a temporary - and never occur deep inside another expression. For example, - - tmp = *(x + 0) + *(x + 1) - - in the original Clight is rewritten to - - tmp1 = *(x + 0) - tmp2 = *(x + 1) - tmp = tmp1 + tmp2 -*) - -open Camlcoq -open Ctypes -open Clight - -let gen_next : AST.ident ref = ref P.one -let gen_trail : (AST.ident * coq_type) list ref = ref [] - -let gensym ty = - let id = !gen_next in - gen_next := P.succ id; - gen_trail := (id, ty) :: !gen_trail; - id - -let is_lvalue = function - | Evar _ | Ederef _ | Efield _ -> true - | _ -> false - -let accesses_memory e = - is_lvalue e && - match access_mode (typeof e) with By_value _ -> true | _ -> false - -(** Normalization of an expression. Return a normalized expression - and a list of statements to be executed before evaluating the expression. *) - -let rec norm_expr e = - let (sl, e') = norm_expr_1 e in - if accesses_memory e then begin - let ty = typeof e in - let id = gensym ty in - (sl @ [Sset(id, e')], Etempvar(id, ty)) - end else - (sl, e') - -and norm_expr_1 e = - match e with - | Econst_int _ | Econst_float _ | Econst_single _ | Econst_long _ -> ([], e) - | Evar _ | Etempvar _ -> ([], e) - | Ederef(e1, t) -> - let (sl, e1') = norm_expr e1 in (sl, Ederef(e1', t)) - | Eaddrof(e1, t) -> - let (sl, e1') = norm_expr_lvalue e1 in (sl, Eaddrof(e1', t)) - | Eunop(op, e1, t) -> - let (sl, e1') = norm_expr e1 in (sl, Eunop(op, e1', t)) - | Ebinop(op, e1, e2, t) -> - let (sl1, e1') = norm_expr e1 in - let (sl2, e2') = norm_expr e2 in - (sl1 @ sl2, Ebinop(op, e1', e2', t)) - | Ecast(e1, t) -> - let (sl, e1') = norm_expr e1 in (sl, Ecast(e1', t)) - | Efield(e1, id, t) -> - let (sl, e1') = norm_expr e1 in (sl, Efield(e1', id, t)) - | Esizeof _ | Ealignof _ -> ([], e) - -(** An expression in l-value position has no memory dereference at top level, - by definition of l-values. Hence, use the [norm_expr_1] variant.. *) -and norm_expr_lvalue e = norm_expr_1 e - -(** In a [Sset id e] statement, the [e] expression can contain a memory - dereference at top level. Hence, use the [norm_expr_1] variant. *) -let norm_expr_set_top = norm_expr_1 - -let rec norm_expr_list el = - match el with - | [] -> ([], []) - | e1 :: el -> - let (sl1, e1') = norm_expr e1 in - let (sl2, el') = norm_expr_list el in - (sl1 @ sl2, e1' :: el') - -let rec add_sequence sl s = - match sl with - | [] -> s - | s1 :: sl -> Ssequence(s1, add_sequence sl s) - -let rec norm_stmt s = - match s with - | Sskip -> s - | Sassign(e1, e2) -> - let (sl1, e1') = norm_expr_lvalue e1 in - let (sl2, e2') = norm_expr e2 in - add_sequence (sl1 @ sl2) (Sassign(e1', e2')) - | Sset(id, e) -> - let (sl, e') = norm_expr_set_top e in - add_sequence sl (Sset(id, e')) - | Scall(optid, e, el) -> - let (sl1, e') = norm_expr e in - let (sl2, el') = norm_expr_list el in - add_sequence (sl1 @ sl2) (Scall(optid, e', el')) - | Sbuiltin(optid, ef, tyl, el) -> - let (sl, el') = norm_expr_list el in - add_sequence sl (Sbuiltin(optid, ef, tyl, el')) - | Ssequence(s1, s2) -> - Ssequence(norm_stmt s1, norm_stmt s2) - | Sifthenelse(e, s1, s2) -> - let (sl, e') = norm_expr e in - add_sequence sl (Sifthenelse(e', norm_stmt s1, norm_stmt s2)) - | Sloop(s1, s2) -> - Sloop(norm_stmt s1, norm_stmt s2) - | Sbreak | Scontinue | Sreturn None -> s - | Sreturn (Some e) -> - let (sl, e') = norm_expr e in - add_sequence sl (Sreturn(Some e')) - | Sswitch(e, ls) -> - let (sl, e') = norm_expr e in - add_sequence sl (Sswitch(e', norm_lbl_stmt ls)) - | Slabel(lbl, s1) -> - Slabel(lbl, norm_stmt s1) - | Sgoto lbl -> s - -and norm_lbl_stmt ls = - match ls with - | LSnil -> LSnil - | LScons(n, s, ls) -> LScons(n, norm_stmt s, norm_lbl_stmt ls) - -(* In "canonical atoms" mode, temporaries are between 2^7 and 2^12 - 1. - Below 2^7 are single-letter identifiers and above 2^12 are all - other identifiers. *) - -let first_temp = P.of_int 128 -let last_temp = P.of_int 4095 - -let next_var curr (v, _) = - if P.lt v curr - || !use_canonical_atoms && (P.lt v first_temp || P.gt v last_temp) - then curr - else P.succ v - -let next_var_list vars start = List.fold_left next_var start vars - -let norm_function f = - gen_next := next_var_list f.fn_params - (next_var_list f.fn_vars - (next_var_list f.fn_temps - (Camlcoq.first_unused_ident ()))); - gen_trail := []; - let s' = norm_stmt f.fn_body in - let new_temps = !gen_trail in - { f with fn_body = s'; fn_temps = f.fn_temps @ new_temps } - -let norm_fundef = function - | Internal f -> Internal (norm_function f) - | External _ as fd -> fd - -let norm_program p = - let p1 = AST.transform_program norm_fundef (program_of_program p) in - { p with prog_defs = p1.AST.prog_defs } diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml deleted file mode 100644 index 742b3a5c..00000000 --- a/exportclight/ExportClight.ml +++ /dev/null @@ -1,584 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 - -(* Options, lists, pairs *) - -let print_option fn p = function - | None -> fprintf p "None" - | Some x -> fprintf p "(Some %a)" fn x - -let print_pair fn1 fn2 p (x1, x2) = - fprintf p "@[(%a,@ %a)@]" fn1 x1 fn2 x2 - -let print_list fn p l = - match l with - | [] -> - fprintf p "nil" - | hd :: tl -> - fprintf p "@[("; - let rec plist = function - | [] -> fprintf p "nil" - | hd :: tl -> fprintf p "%a ::@ " fn hd; plist tl - in plist l; - fprintf p ")@]" - -(* Numbers *) - -let coqint p n = - let n = camlint_of_coqint n in - if n >= 0l - then fprintf p "(Int.repr %ld)" n - else fprintf p "(Int.repr (%ld))" n - -let coqptrofs p n = - let s = Z.to_string n in - if Z.ge n Z.zero - then fprintf p "(Ptrofs.repr %s)" s - else fprintf p "(Ptrofs.repr (%s))" s - -let coqint64 p n = - let n = camlint64_of_coqint n in - if n >= 0L - then fprintf p "(Int64.repr %Ld)" n - else fprintf p "(Int64.repr (%Ld))" n - -let coqfloat p n = - fprintf p "(Float.of_bits %a)" coqint64 (Floats.Float.to_bits n) - -let coqsingle p n = - fprintf p "(Float32.of_bits %a)" coqint (Floats.Float32.to_bits n) - -let positive p n = - fprintf p "%s%%positive" (Z.to_string (Z.Zpos n)) - -let coqN p n = - fprintf p "%s%%N" (Z.to_string (Z.of_N n)) - -let coqZ p n = - if Z.ge n Z.zero - then fprintf p "%s" (Z.to_string n) - else fprintf p "(%s)" (Z.to_string n) - -(* Coq strings *) - -let coqstring p s = - fprintf p "\"%s\"" (camlstring_of_coqstring s) - -(* Identifiers *) - -exception Not_an_identifier - -let sanitize_char = function - | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' as c -> c - | ' ' | '$' -> '_' - | _ -> raise Not_an_identifier - -let sanitize 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) - with Not_found | Not_an_identifier -> - try - let s = Hashtbl.find temp_names id in - fprintf p "%s" s - with Not_found -> - positive p id - -let iter_hashtbl_sorted (h: ('a, string) Hashtbl.t) (f: 'a * string -> unit) = - List.iter f - (List.fast_sort (fun (k1, d1) (k2, d2) -> String.compare d1 d2) - (Hashtbl.fold (fun k d accu -> (k, d) :: accu) h [])) - -let define_idents p = - iter_hashtbl_sorted - string_of_atom - (fun (id, name) -> - try - if !use_canonical_atoms && id = pos_of_string name then - fprintf p "Definition %s : ident := $\"%s\".@ " - (sanitize name) name - else - fprintf p "Definition %s : ident := %a.@ " - (sanitize name) positive id - with Not_an_identifier -> - ()); - iter_hashtbl_sorted - temp_names - (fun (id, name) -> - fprintf p "Definition %s : ident := %a.@ " - name positive id); - fprintf p "@ " - -let name_temporary t = - if not (Hashtbl.mem string_of_atom t) && not (Hashtbl.mem temp_names t) - then begin - let t0 = first_unused_ident () in - let d = Z.succ (Z.sub (Z.Zpos t) (Z.Zpos t0)) in - Hashtbl.add temp_names t ("_t'" ^ Z.to_string d) - end - -let name_opt_temporary = function - | None -> () - | Some id -> name_temporary id - -(* Raw attributes *) - -let attribute p a = - if a = noattr then - fprintf p "noattr" - else - fprintf p "{| attr_volatile := %B; attr_alignas := %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 = - match attr_of_type t with - | { attr_volatile = false; attr_alignas = None} -> - rtyp p t - | { attr_volatile = true; attr_alignas = None} -> - fprintf p "(tvolatile %a)" rtyp t - | { attr_volatile = false; attr_alignas = Some n} -> - fprintf p "(talignas %a %a)" coqN n rtyp t - | { attr_volatile = true; attr_alignas = Some n} -> - fprintf p "(tvolatile_alignas %a %a)" coqN n rtyp t - -and rtyp p = function - | Tvoid -> fprintf p "tvoid" - | Ctypes.Tint(sz, sg, _) -> - fprintf p "%s" ( - match sz, sg with - | I8, Signed -> "tschar" - | I8, Unsigned -> "tuchar" - | I16, Signed -> "tshort" - | I16, Unsigned -> "tushort" - | I32, Signed -> "tint" - | I32, Unsigned -> "tuint" - | IBool, _ -> "tbool") - | Ctypes.Tlong(sg, _) -> - fprintf p "%s" ( - match sg with - | Signed -> "tlong" - | Unsigned -> "tulong") - | Ctypes.Tfloat(sz, _) -> - fprintf p "%s" ( - match sz with - | F32 -> "tfloat" - | F64 -> "tdouble") - | Tpointer(t, _) -> - fprintf p "(tptr %a)" typ t - | Tarray(t, sz, _) -> - fprintf p "(tarray %a %ld)" typ t (Z.to_int32 sz) - | Tfunction(targs, tres, cc) -> - fprintf p "@[(Tfunction@ %a@ %a@ %a)@]" - typlist targs typ tres callconv cc - | Tstruct(id, _) -> - fprintf p "(Tstruct %a noattr)" ident id - | Tunion(id, _) -> - fprintf p "(Tunion %a noattr)" ident id - -and typlist p = function - | Tnil -> - fprintf p "Tnil" - | Tcons(t, tl) -> - fprintf p "@[(Tcons@ %a@ %a)@]" typ t typlist tl - -and callconv p cc = - if cc = cc_default - then fprintf p "cc_default" - 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 *) - -let asttype p t = - fprintf p "%s" - (match t with - | AST.Tint -> "AST.Tint" - | AST.Tfloat -> "AST.Tfloat" - | AST.Tlong -> "AST.Tlong" - | AST.Tsingle -> "AST.Tsingle" - | AST.Tany32 -> "AST.Tany32" - | AST.Tany64 -> "AST.Tany64") - -let astrettype p = function - | AST.Tret t -> asttype p t - | AST.Tvoid -> fprintf p "AST.Tvoid" - | AST.Tint8signed -> fprintf p "AST.Tint8signed" - | AST.Tint8unsigned -> fprintf p "AST.Tint8unsigned" - | AST.Tint16signed -> fprintf p "AST.Tint16signed" - | AST.Tint16unsigned -> fprintf p "AST.Tint16unsigned" - -let name_of_chunk = function - | Mint8signed -> "Mint8signed" - | Mint8unsigned -> "Mint8unsigned" - | Mint16signed -> "Mint16signed" - | Mint16unsigned -> "Mint16unsigned" - | Mint32 -> "Mint32" - | Mint64 -> "Mint64" - | Mfloat32 -> "Mfloat32" - | Mfloat64 -> "Mfloat64" - | Many32 -> "Many32" - | Many64 -> "Many64" - -let signatur p sg = - fprintf p "@[(mksignature@ %a@ %a@ %a)@]" - (print_list asttype) sg.sig_args - astrettype sg.sig_res - callconv sg.sig_cc - -let external_function p = function - | EF_external(name, sg) -> - fprintf p "@[(EF_external %a@ %a)@]" coqstring name signatur sg - | EF_builtin(name, sg) -> - fprintf p "@[(EF_builtin %a@ %a)@]" coqstring name signatur sg - | EF_runtime(name, sg) -> - fprintf p "@[(EF_runtime %a@ %a)@]" coqstring name signatur sg - | EF_vload chunk -> - fprintf p "(EF_vload %s)" (name_of_chunk chunk) - | EF_vstore chunk -> - fprintf p "(EF_vstore %s)" (name_of_chunk chunk) - | EF_malloc -> fprintf p "EF_malloc" - | EF_free -> fprintf p "EF_free" - | EF_memcpy(sz, al) -> - fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al) - | EF_annot(kind, text, targs) -> - fprintf p "(EF_annot %a %a %a)" - positive kind coqstring text (print_list asttype) targs - | EF_annot_val(kind, text, targ) -> - fprintf p "(EF_annot_val %a %a %a)" - positive kind coqstring text asttype targ - | EF_debug(kind, text, targs) -> - fprintf p "(EF_debug %a %a %a)" - positive kind positive text (print_list asttype) targs - | EF_inline_asm(text, sg, clob) -> - fprintf p "@[(EF_inline_asm %a@ %a@ %a)@]" - coqstring text - signatur sg - (print_list coqstring) clob - -(* 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 - -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 init_data p = function - | Init_int8 n -> fprintf p "Init_int8 %a" coqint n - | Init_int16 n -> fprintf p "Init_int16 %a" coqint n - | Init_int32 n -> fprintf p "Init_int32 %a" coqint n - | Init_int64 n -> fprintf p "Init_int64 %a" coqint64 n - | Init_float32 n -> fprintf p "Init_float32 %a" coqsingle n - | Init_float64 n -> fprintf p "Init_float64 %a" coqfloat n - | Init_space n -> fprintf p "Init_space %a" coqZ n - | 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 " 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; - fprintf p " gvar_volatile := %B@ " v.gvar_volatile; - 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 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)) - -(* Composite definitions *) - -let print_member p = function - | Member_plain (id, ty) -> - fprintf p "@[Member_plain@ %a@ %a@]" - ident id typ ty - | Member_bitfield (id, sz, sg, a, width, pad) -> - fprintf p "@[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 "@[Composite %a %s@ %a@ %a@]" - ident id - (match su with Struct -> "Struct" | Union -> "Union") - (print_list print_member) m - attribute a - -(* 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 - -(* Information about this run of clightgen *) - -let print_clightgen_info p sourcefile normalized = - fprintf p "@[Module Info."; - fprintf p "@ Definition version := %S." Version.version; - fprintf p "@ Definition build_number := %S." Version.buildnr; - fprintf p "@ Definition build_tag := %S." Version.tag; - fprintf p "@ Definition build_branch := %S." Version.branch; - fprintf p "@ Definition arch := %S." Configuration.arch; - fprintf p "@ Definition model := %S." Configuration.model; - fprintf p "@ Definition abi := %S." Configuration.abi; - fprintf p "@ Definition bitsize := %d." (if Archi.ptr64 then 64 else 32); - fprintf p "@ Definition big_endian := %B." Archi.big_endian; - fprintf p "@ Definition source_file := %S." sourcefile; - fprintf p "@ Definition normalized := %B." normalized; - fprintf p "@]@ End Info.@ @ " - -(* 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 p sourcefile normalized; - 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 "@]@." diff --git a/exportclight/README.md b/exportclight/README.md deleted file mode 100644 index 85e0790b..00000000 --- a/exportclight/README.md +++ /dev/null @@ -1,33 +0,0 @@ -# The clightgen tool - - -## Overview -"clightgen" is an experimental tool that transforms C source files -into Clight abstract syntax, pretty-printed in Coq format in .v files. -These generated .v files can be loaded in a Coq session for -interactive verification, typically. - - -## How to build - -Change to the top-level CompCert directory and issue -``` - make clightgen -``` - -## Usage -``` - clightgen [options] -``` -For each source file `src.c`, its Clight abstract syntax is generated -in `src.v`. - -The options recognized are a subset of those of the CompCert compiler ccomp -(see [user's manual](http://compcert.inria.fr/man/manual003.html) for full documentation): -``` - -I search for include files - -D define preprocessor macro - -U undefine preprocessor macro - -Wp, pass options to C preprocessor - -f activate emulation of the given C feature -``` -- cgit