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/ --- LICENSE | 2 +- Makefile | 8 +- Makefile.extr | 4 +- configure | 4 +- export/Clightdefs.v | 304 ++++++++++++++++++++++ export/Clightgen.ml | 201 +++++++++++++++ export/Clightnorm.ml | 178 +++++++++++++ export/ExportBase.ml | 261 +++++++++++++++++++ export/ExportClight.ml | 251 +++++++++++++++++++ export/ExportCtypes.ml | 122 +++++++++ export/README.md | 33 +++ exportclight/Clightdefs.v | 304 ---------------------- exportclight/Clightgen.ml | 201 --------------- exportclight/Clightnorm.ml | 178 ------------- exportclight/ExportClight.ml | 584 ------------------------------------------- exportclight/README.md | 33 --- test/clightgen/Makefile | 2 +- 17 files changed, 1360 insertions(+), 1310 deletions(-) create mode 100644 export/Clightdefs.v create mode 100644 export/Clightgen.ml create mode 100644 export/Clightnorm.ml create mode 100644 export/ExportBase.ml create mode 100644 export/ExportClight.ml create mode 100644 export/ExportCtypes.ml create mode 100644 export/README.md 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 diff --git a/LICENSE b/LICENSE index 6a4c62c3..54b36ed7 100644 --- a/LICENSE +++ b/LICENSE @@ -44,7 +44,7 @@ Foundation GNU Lesser General Public License, either version 2.1 or all files in the cparser/ directory - all files in the exportclight/ directory + all files in the export/ directory the Archi.v, Builtins1.v, CBuiltins.ml, and extractionMachdep.v files in directories aarch64, arm, powerpc, riscV, x86, x86_32, x86_64 diff --git a/Makefile b/Makefile index a0f9fde6..c14f65c7 100644 --- a/Makefile +++ b/Makefile @@ -28,7 +28,7 @@ else ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) endif -DIRS := lib common $(ARCHDIRS) backend cfrontend driver exportclight cparser +DIRS := lib common $(ARCHDIRS) backend cfrontend driver export cparser COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(d)) @@ -203,9 +203,9 @@ ccomp: .depend.extr compcert.ini driver/Version.ml FORCE ccomp.byte: .depend.extr compcert.ini driver/Version.ml FORCE $(MAKE) -f Makefile.extr ccomp.byte -clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE +clightgen: .depend.extr compcert.ini export/Clightdefs.vo driver/Version.ml FORCE $(MAKE) -f Makefile.extr clightgen -clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE +clightgen.byte: .depend.extr compcert.ini export/Clightdefs.vo driver/Version.ml FORCE $(MAKE) -f Makefile.extr clightgen.byte runtime: @@ -295,7 +295,7 @@ cparser/Parser.v: cparser/Parser.vy depend: $(GENERATED) depend1 -depend1: $(FILES) exportclight/Clightdefs.v +depend1: $(FILES) export/Clightdefs.v @echo "Analyzing Coq dependencies" @$(COQDEP) $^ > .depend diff --git a/Makefile.extr b/Makefile.extr index fc631d78..e4b24ecd 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -45,7 +45,7 @@ cparser/pre_parser_messages.ml: DIRS=extraction \ lib common $(ARCH) backend cfrontend cparser driver \ - exportclight debug + export debug INCLUDES=$(patsubst %,-I %, $(DIRS)) @@ -112,7 +112,7 @@ ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" @$(OCAMLC) -o $@ $(LIBS_BYTE) $+ -CLIGHTGEN_OBJS:=$(shell $(MODORDER) exportclight/Clightgen.cmx) +CLIGHTGEN_OBJS:=$(shell $(MODORDER) export/Clightgen.cmx) ifeq ($(OCAML_NATIVE_COMP),true) clightgen: $(CLIGHTGEN_OBJS) diff --git a/configure b/configure index b342b143..10f60262 100755 --- a/configure +++ b/configure @@ -770,7 +770,7 @@ S backend S cfrontend S driver S debug -S exportclight +S export S cparser S extraction @@ -781,7 +781,7 @@ B backend B cfrontend B driver B debug -B exportclight +B export B cparser B extraction EOF diff --git a/export/Clightdefs.v b/export/Clightdefs.v new file mode 100644 index 00000000..708be1cb --- /dev/null +++ b/export/Clightdefs.v @@ -0,0 +1,304 @@ +(* *********************************************************************) +(* *) +(* 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/export/Clightgen.ml b/export/Clightgen.ml new file mode 100644 index 00000000..44c76cc6 --- /dev/null +++ b/export/Clightgen.ml @@ -0,0 +1,201 @@ +(* *********************************************************************) +(* *) +(* 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/export/Clightnorm.ml b/export/Clightnorm.ml new file mode 100644 index 00000000..88d44c08 --- /dev/null +++ b/export/Clightnorm.ml @@ -0,0 +1,178 @@ +(* *********************************************************************) +(* *) +(* 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/export/ExportBase.ml b/export/ExportBase.ml new file mode 100644 index 00000000..b7d0170d --- /dev/null +++ b/export/ExportBase.ml @@ -0,0 +1,261 @@ +(* *********************************************************************) +(* *) +(* 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 Format +open Camlcoq +open AST + +(* 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 + +(* 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 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 + +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 + +(* Variables *) + +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 print_info p (id, v) = + fprintf p "Definition v%s := {|@ " (sanitize (extern_atom id)); + fprintf p " gvar_info := %a;@ " print_info 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 "|}.@ @ " + +(* Information about this run of clightgen *) + +let print_clightgen_info ~sourcefile ?normalized p = + 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; + begin match normalized with + | None -> () + | Some b -> fprintf p "@ Definition normalized := %B." b + end; + fprintf p "@]@ End Info.@ @ " + 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 "@]@." diff --git a/export/ExportCtypes.ml b/export/ExportCtypes.ml new file mode 100644 index 00000000..428a1459 --- /dev/null +++ b/export/ExportCtypes.ml @@ -0,0 +1,122 @@ +(* *********************************************************************) +(* *) +(* 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 Format +open Camlcoq +open Ctypes +open ExportBase + +(* 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 + +(* 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 + diff --git a/export/README.md b/export/README.md new file mode 100644 index 00000000..85e0790b --- /dev/null +++ b/export/README.md @@ -0,0 +1,33 @@ +# 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 +``` 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 -``` diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile index f0e9d961..83ba0fd3 100644 --- a/test/clightgen/Makefile +++ b/test/clightgen/Makefile @@ -5,7 +5,7 @@ ARCHDIRS=$(ARCH) else ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) endif -RECDIRS := lib common $(ARCHDIRS) cfrontend exportclight +RECDIRS := lib common $(ARCHDIRS) cfrontend export COQINCLUDES := $(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) ifeq ($(LIBRARY_FLOCQ),local) COQINCLUDES += -R ../../flocq Flocq -- cgit