diff --git a/.gitignore b/.gitignore index b75ea5e72a..3e24787b60 100644 --- a/.gitignore +++ b/.gitignore @@ -21,6 +21,8 @@ /ccomp.prof /clightgen /clightgen.byte +/csyntaxgen +/csyntaxgen.byte /tools/ndfun /tools/modorder /Makefile.config @@ -75,6 +77,7 @@ .DS_Store # Test generated data /test/clightgen/*.v +/test/csyntaxgen/*.v # Coq caches .lia.cache .nia.cache diff --git a/Makefile b/Makefile index a0f9fde6f1..d8a4629be8 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 exportclight exportcsyntax cparser COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcert.$(d)) @@ -179,6 +179,9 @@ endif ifeq ($(CLIGHTGEN),true) $(MAKE) clightgen endif +ifeq ($(CSYNTAXGEN),true) + $(MAKE) csyntaxgen +endif ifeq ($(INSTALL_COQDEV),true) $(MAKE) compcert.config endif @@ -208,6 +211,11 @@ clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.m clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE $(MAKE) -f Makefile.extr clightgen.byte +csyntaxgen: .depend.extr compcert.ini exportcsyntax/Csyntaxdefs.vo driver/Version.ml FORCE + $(MAKE) -f Makefile.extr csyntaxgen +csyntaxgen.byte: .depend.extr compcert.ini exportcsyntax/Csyntaxdefs.vo driver/Version.ml FORCE + $(MAKE) -f Makefile.extr csyntaxgen.byte + runtime: $(MAKE) -C runtime @@ -310,6 +318,9 @@ install: ifeq ($(CLIGHTGEN),true) install -m 0755 ./clightgen $(DESTDIR)$(BINDIR) endif +ifeq ($(CSYNTAXGEN),true) + install -m 0755 ./csyntaxgen $(DESTDIR)$(BINDIR) +endif ifeq ($(INSTALL_COQDEV),true) install -d $(DESTDIR)$(COQDEVDIR) for d in $(DIRS); do \ diff --git a/Makefile.extr b/Makefile.extr index a894982066..9e45277375 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 + exportclight exportcsyntax debug INCLUDES=$(patsubst %,-I %, $(DIRS)) @@ -89,7 +89,7 @@ LEXERS=cparser/Lexer.mll lib/Tokenize.mll \ LIBS=str.cmxa unix.cmxa $(MENHIR_LIBS) LIBS_BYTE=$(patsubst %.cmxa,%.cma,$(patsubst %.cmx,%.cmo,$(LIBS))) -EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte +EXECUTABLES=ccomp ccomp.byte cchecklink cchecklink.byte clightgen clightgen.byte csyntaxgen csyntaxgen.byte GENERATED=$(PARSERS:.mly=.mli) $(PARSERS:.mly=.ml) $(LEXERS:.mll=.ml) cparser/pre_parser_messages.ml # Beginning of part that assumes .depend.extr already exists @@ -128,6 +128,22 @@ clightgen.byte: $(CLIGHTGEN_OBJS:.cmx=.cmo) @echo "Linking $@" @$(OCAMLC) -o $@ $(LIBS_BYTE) $+ +CSYNTAXGEN_OBJS:=$(shell $(MODORDER) exportcsyntax/Csyntaxgen.cmx) + +ifeq ($(OCAML_NATIVE_COMP),true) +csyntaxgen: $(CSYNTAXGEN_OBJS) + @echo "Linking $@" + @$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+ +else +csyntaxgen: csyntaxgen.byte + @echo "Copying to $@" + @$(COPY) $+ $@ +endif + +csyntaxgen.byte: $(CSYNTAXGEN_OBJS:.cmx=.cmo) + @echo "Linking $@" + @$(OCAMLC) -o $@ $(LIBS_BYTE) $+ + include .depend.extr endif diff --git a/configure b/configure index b342b143af..c393370293 100755 --- a/configure +++ b/configure @@ -26,6 +26,7 @@ target='' has_runtime_lib=true has_standard_headers=true clightgen=false +csyntaxgen=false install_coqdev=false ignore_coq_version=false library_Flocq=local @@ -95,7 +96,8 @@ Options: -no-runtime-lib Do not compile nor install the runtime support library -no-standard-headers Do not install nor use the standard .h headers -clightgen Also compile and install the clightgen tool - -install-coqdev Also install the Coq development (implied by -clightgen) + -csyntaxgen Also compile and install the csyntaxgen tool + -install-coqdev Also install the Coq development (implied by -clightgen and -csyntaxgen) -ignore-coq-version Accept to use experimental or unsupported versions of Coq ' @@ -130,6 +132,9 @@ while : ; do -clightgen) clightgen=true install_coqdev=true;; + -csyntaxgen) + csyntaxgen=true + install_coqdev=true;; -ignore-coq-version|--ignore-coq-version) ignore_coq_version=true;; -install-coqdev|--install-coqdev|-install-coq-dev|--install-coq-dev) @@ -639,6 +644,7 @@ CASM_OPTIONS=$casm_options CASMRUNTIME=$casmruntime CC=$cc $cc_options CLIGHTGEN=$clightgen +CSYNTAXGEN=$csyntaxgen CLINKER=$clinker CLINKER_OPTIONS=$clinker_options CPREPRO=$cprepro @@ -750,6 +756,9 @@ ASM_SUPPORTS_CFI=false # Turn on/off compilation of clightgen CLIGHTGEN=false +# Turn on/off compilation of csyntaxgen +CSYNTAXGEN=false + # Whether the other tools support responsefiles in GNU syntax or Diab syntax RESPONSEFILE=gnu # diab @@ -771,6 +780,7 @@ S cfrontend S driver S debug S exportclight +S exportcsyntax S cparser S extraction @@ -782,6 +792,7 @@ B cfrontend B driver B debug B exportclight +B exportcsyntax B cparser B extraction EOF diff --git a/exportcsyntax/Csyntaxdefs.v b/exportcsyntax/Csyntaxdefs.v new file mode 100644 index 0000000000..fe829b075f --- /dev/null +++ b/exportcsyntax/Csyntaxdefs.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 files generated by csyntaxgen *) + +From Coq Require Import Ascii String List ZArith. +From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Csyntax. + +(** ** 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) : Csyntax.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 CsyntaxNotations. + +(** 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) : csyntax_scope. + +End CsyntaxNotations. diff --git a/exportcsyntax/Csyntaxgen.ml b/exportcsyntax/Csyntaxgen.ml new file mode 100644 index 0000000000..84a4149a46 --- /dev/null +++ b/exportcsyntax/Csyntaxgen.ml @@ -0,0 +1,177 @@ +(* *********************************************************************) +(* *) +(* 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 = "Csyntax generator" + +(* csyntaxgen-specific options *) + +(* Export CompCert C AST *) + +let compile_c_ast sourcename csyntax ofile = + (* Print Csyntax in Coq syntax *) + let oc = open_out ofile in + ExportCsyntax.print_program (Format.formatter_of_out_channel oc) + csyntax sourcename; + close_out oc + +(* Export CompCert C AST parsed from C source *) + +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"; + 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: csyntaxgen [options] +Recognized source files: + .c C source file + .i or .p C source file that should not be preprocessed +Processing options: + -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 + -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 "-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 "-dall", Self (fun _ -> + option_dprepro := true; + option_dparse := true; + option_dcmedium := 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/exportcsyntax/ExportCsyntax.ml b/exportcsyntax/ExportCsyntax.ml new file mode 100644 index 0000000000..be92317985 --- /dev/null +++ b/exportcsyntax/ExportCsyntax.ml @@ -0,0 +1,497 @@ +(* *********************************************************************) +(* *) +(* 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 Values +open Cop +open Csyntax + +(* 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 s = + let s' = Bytes.create (String.length s) in + for i = 0 to String.length s - 1 do + Bytes.set s' i + (match String.get s i with + | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' as c -> c + | ' ' | '$' -> '_' + | _ -> raise Not_an_identifier) + done; + Bytes.to_string s' + +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 -> + 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 -> + ()); + fprintf p "@ " + +(* 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 + +(* 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 + +(* Values *) + +let val_ p = function + | Vundef -> fprintf p "Vundef" + | Vint i -> fprintf p "(Vint %a)" coqint i + | Vlong l -> fprintf p "(Vlong %a)" coqint64 l + | Vfloat f -> fprintf p "(Vfloat %a)" coqfloat f + | Vsingle s -> fprintf p "(Vsingle %a)" coqsingle s + | Vptr(b, o) -> fprintf p "(Vptr %a %a)" positive b coqptrofs o + +(* 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 name_incr_or_decr = function + | Incr -> "Incr" + | Decr -> "Decr" + +let rec expr p = function + | Eval(v, t) -> + fprintf p "(Eval %a %a)" val_ v typ t + | Evar(id, t) -> + fprintf p "(Evar %a %a)" ident id typ t + | Efield(a1, f, t) -> + fprintf p "@[(Efield@ %a@ %a@ %a)@]" expr a1 ident f typ t + | Evalof(l, t) -> + fprintf p "@[(Evalof@ %a@ %a)@]" expr l typ t + | Ederef(a1, t) -> + fprintf p "@[(Ederef@ %a@ %a)@]" expr a1 typ t + | Eaddrof(a1, t) -> + fprintf p "@[(Eaddrof@ %a@ %a)@]" expr a1 typ t + | Eunop(op, a1, t) -> + fprintf p "@[(Eunop %s@ %a@ %a)@]" + (name_unop op) 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 + | Eseqand(a1, a2, t) -> + fprintf p "@[(Eseqand@ %a@ %a@ %a)@]" expr a1 expr a2 typ t + | Eseqor(a1, a2, t) -> + fprintf p "@[(Eseqor@ %a@ %a@ %a)@]" expr a1 expr a2 typ t + | Econdition(a1, a2, a3, t) -> + fprintf p "@[(Econdition@ %a@ %a@ %a@ %a)@]" expr a1 expr a2 expr a3 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 + | Eassign(l, r, t) -> + fprintf p "@[(Eassign@ %a@ %a@ %a)@]" expr l expr r typ t + | Eassignop(op, l, r, t', t) -> + fprintf p "@[(Eassignop@ %s@ %a@ %a@ %a %a)@]" (name_binop op) expr l expr r typ t' typ t + | Epostincr(id, l, t) -> + fprintf p "@[(Epostincr@ %s@ %a@ %a)@]" (name_incr_or_decr id) expr l typ t + | Ecomma(a1, a2, t) -> + fprintf p "@[(Ecomma@ %a@ %a@ %a)@]" expr a1 expr a2 typ t + | Ecall(r1, rargs, t) -> + fprintf p "@[(Ecall@ %a@ %a@ %a)@]" expr r1 exprlist rargs typ t + | Ebuiltin(ef, tyargs, rargs, t) -> + fprintf p "@[(Ebuiltin@ %a@ %a@ %a@ %a)@]" external_function ef typlist tyargs exprlist rargs typ t + | Eloc(b, o, t) -> + fprintf p "@[(Eloc@ %a@ %a@ %a)@]" positive b coqptrofs o typ t + | Eparen(r, t', t) -> + fprintf p "@[(Eparen@ %a@ %a@ %a)@]" expr r typ t' typ t +and exprlist p = function + | Enil -> + fprintf p "Enil" + | Econs(r1, rl) -> + fprintf p "@[(Econs@ %a@ %a)@]" expr r1 exprlist rl + +(* Statements *) + +let rec statement p = function + | Sskip -> + fprintf p "Sskip" + | Sdo(e) -> + fprintf p "@[(Sdo %a)@]" expr e + | Ssequence(s1, s2) -> + fprintf p "@[(Ssequence@ %a@ %a)@]" statement s1 statement s2 + | Sifthenelse(e, s1, s2) -> + fprintf p "@[(Sifthenelse %a@ %a@ %a)@]" expr e statement s1 statement s2 + | Swhile(e, s) -> + fprintf p "@[(Swhile@ %a@ %a)@]" expr e statement s + | Sdowhile(e, s) -> + fprintf p "@[(Sdowhile@ %a@ %a)@]" expr e statement s + | Sfor(s1, e, s2, s3) -> + fprintf p "@[(Sfor@ %a@ %a@ %a@ %a)@]" statement s1 expr e statement s2 statement s3 + | Sbreak -> + fprintf p "Sbreak" + | Scontinue -> + fprintf p "Scontinue" + | Sreturn e -> + fprintf p "@[(Sreturn %a)@]" (print_option expr) e + | Sswitch(e, cases) -> + fprintf p "@[(Sswitch %a@ %a)@]" expr e labeled_statements cases + | Slabel(lbl, s1) -> + fprintf p "@[(Slabel %a@ %a)@]" ident lbl statement s1 + | Sgoto lbl -> + fprintf p "(Sgoto %a)" ident lbl + +and labeled_statements p = function + | LSnil -> + (fprintf p "LSnil") + | LScons(lbl, s, ls) -> + fprintf p "@[(LScons %a@ %a@ %a)@]" + (print_option coqZ) lbl statement s labeled_statements 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_body :=@ "; + statement 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_composite_definition p (Composite(id, su, m, a)) = + fprintf p "@[Composite %a %s@ %a@ %a@]" + ident id + (match su with Struct -> "Struct" | Union -> "Union") + (print_list (print_pair ident typ)) m + attribute a + +(* The prologue *) + +let prologue = "\ +From Coq Require Import String List ZArith.\n\ +From compcert Require Import Coqlib Integers Floats Values AST Ctypes Cop Csyntax Csyntaxdefs.\n\ +Import Csyntaxdefs.CsyntaxNotations.\n\ +Local Open Scope Z_scope.\n\ +Local Open Scope string_scope.\n\ +Local Open Scope csyntax_scope.\n" + +(* Information about this run of csyntaxgen *) + +let print_csyntaxgen_info p sourcefile = + 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 "@]@ End Info.@ @ " + +(* All together *) + +let print_program p prog sourcefile = + fprintf p "@["; + fprintf p "%s" prologue; + print_csyntaxgen_info p sourcefile; + 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 : Csyntax.program := @ "; + fprintf p " mkprogram composites global_definitions public_idents %a Logic.I.@ @ " + ident prog.Ctypes.prog_main; + fprintf p "@]@." diff --git a/exportcsyntax/README.md b/exportcsyntax/README.md new file mode 100644 index 0000000000..b2d91ef8ea --- /dev/null +++ b/exportcsyntax/README.md @@ -0,0 +1,33 @@ +# The clightgen tool + + +## Overview +"csyntaxgen" is an experimental tool that transforms C source files +into CompCert C abstract syntax, pretty-printed in Coq format in .v files. +These generated .v files can be loaded in a Coq session for +verification, typically. + + +## How to build + +Change to the top-level CompCert directory and issue +``` + make csyntaxgen +``` + +## Usage +``` + csyntaxgen [options] +``` +For each source file `src.c`, its CompCert C 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/Makefile b/test/Makefile index fa1fef3083..c9676bd26d 100644 --- a/test/Makefile +++ b/test/Makefile @@ -4,6 +4,9 @@ DIRS=c compression raytracer spass regression abi ifeq ($(CLIGHTGEN),true) DIRS+=clightgen endif +ifeq ($(CSYNTAXGEN),true) +DIRS+=csyntaxgen +endif all: set -e; for i in $(DIRS); do $(MAKE) CCOMPOPTS='$(CCOMPOPTS)' -C $$i all; done diff --git a/test/csyntaxgen/Makefile b/test/csyntaxgen/Makefile new file mode 100644 index 0000000000..f3631d90b9 --- /dev/null +++ b/test/csyntaxgen/Makefile @@ -0,0 +1,54 @@ +include ../../Makefile.config + +ifeq ($(wildcard ../../$(ARCH)_$(BITSIZE)),) +ARCHDIRS=$(ARCH) +else +ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) +endif +RECDIRS := lib common $(ARCHDIRS) cfrontend exportcsyntax +COQINCLUDES := $(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) +ifeq ($(LIBRARY_FLOCQ),local) +COQINCLUDES += -R ../../flocq Flocq +endif + + +CSYNTAXGEN=../../csyntaxgen +COQC=coqc + +# Regression tests in the current directory +SRC=$(wildcard *.c) +# From ../c +SRC+=aes.c almabench.c binarytrees.c bisect.c chomp.c fannkuch.c fft.c \ + fftsp.c fftw.c fib.c integr.c knucleotide.c lists.c mandelbrot.c \ + nbody.c nsievebits.c nsieve.c perlin.c qsort.c sha1.c sha3.c \ + siphash24.c spectral.c vmach.c +# From ../raytracer +SRC+=arrays.c eval.c gmllexer.c gmlparser.c intersect.c light.c main.c \ + matrix.c memory.c object.c render.c simplify.c surface.c vector.c + +CFLAGS=-DSYSTEM_$(SYSTEM) + +aes.vo almabench.vo binarytrees.vo bisect.vo chomp.vo: CFLAGS += -short-idents + +fft.vo fftsp.vo fftw.vo fib.vo integr.vo knucleotide.vo: CFLAGS += -short-idents + +all: $(SRC:.c=.vo) + +test: + +%.v: %.c + $(CSYNTAXGEN) $(CFLAGS) -o $@ $< + +%.v: ../c/%.c + $(CSYNTAXGEN) $(CFLAGS) -o $@ $< + +%.v: ../raytracer/%.c + $(CSYNTAXGEN) -I../raytracer -fall $(CFLAGS) -o $@ $< + +%.vo: %.v + $(COQC) $(COQINCLUDES) -noglob $< + +.SECONDARY: $(SRC:.c=.v) + +clean: + rm -f *.v *.vo* .*.aux diff --git a/test/csyntaxgen/annotations.c b/test/csyntaxgen/annotations.c new file mode 100644 index 0000000000..993fa7d02e --- /dev/null +++ b/test/csyntaxgen/annotations.c @@ -0,0 +1,8 @@ +int f(int x, long y) +{ +#if !defined(SYSTEM_macos) && !defined(SYSTEM_cygwin) + __builtin_ais_annot("x is %e1, y is %e2", x, y); +#endif + __builtin_annot("x is %1, y is %2", x, y); + return __builtin_annot_intval("x was here: %1", x); +} diff --git a/test/csyntaxgen/empty.c b/test/csyntaxgen/empty.c new file mode 100644 index 0000000000..8f8871a781 --- /dev/null +++ b/test/csyntaxgen/empty.c @@ -0,0 +1 @@ +/* The empty source file */ diff --git a/test/csyntaxgen/issue196.c b/test/csyntaxgen/issue196.c new file mode 100644 index 0000000000..1821fd6d43 --- /dev/null +++ b/test/csyntaxgen/issue196.c @@ -0,0 +1,927 @@ +#include +#include +#include + + +typedef int ASN1_BOOLEAN; +typedef int ASN1_NULL; +typedef struct ASN1_ITEM_st ASN1_ITEM; +typedef struct asn1_object_st ASN1_OBJECT; +typedef struct asn1_pctx_st ASN1_PCTX; +typedef struct asn1_string_st ASN1_BIT_STRING; +typedef struct asn1_string_st ASN1_BMPSTRING; +typedef struct asn1_string_st ASN1_ENUMERATED; +typedef struct asn1_string_st ASN1_GENERALIZEDTIME; +typedef struct asn1_string_st ASN1_GENERALSTRING; +typedef struct asn1_string_st ASN1_IA5STRING; +typedef struct asn1_string_st ASN1_INTEGER; +typedef struct asn1_string_st ASN1_OCTET_STRING; +typedef struct asn1_string_st ASN1_PRINTABLESTRING; +typedef struct asn1_string_st ASN1_STRING; +typedef struct asn1_string_st ASN1_T61STRING; +typedef struct asn1_string_st ASN1_TIME; +typedef struct asn1_string_st ASN1_UNIVERSALSTRING; +typedef struct asn1_string_st ASN1_UTCTIME; +typedef struct asn1_string_st ASN1_UTF8STRING; +typedef struct asn1_string_st ASN1_VISIBLESTRING; + +typedef struct AUTHORITY_KEYID_st AUTHORITY_KEYID; +typedef struct DIST_POINT_st DIST_POINT; +typedef struct ISSUING_DIST_POINT_st ISSUING_DIST_POINT; +typedef struct NAME_CONSTRAINTS_st NAME_CONSTRAINTS; +typedef struct X509_POLICY_CACHE_st X509_POLICY_CACHE; +typedef struct X509_POLICY_LEVEL_st X509_POLICY_LEVEL; +typedef struct X509_POLICY_NODE_st X509_POLICY_NODE; +typedef struct X509_POLICY_TREE_st X509_POLICY_TREE; +typedef struct X509_algor_st X509_ALGOR; +typedef struct X509_crl_st X509_CRL; +typedef struct X509_pubkey_st X509_PUBKEY; +typedef struct bignum_ctx BN_CTX; +typedef struct bignum_st BIGNUM; +typedef struct bio_method_st BIO_METHOD; +typedef struct bio_st BIO; +typedef struct bn_gencb_st BN_GENCB; +typedef struct bn_mont_ctx_st BN_MONT_CTX; +typedef struct buf_mem_st BUF_MEM; +typedef struct cbb_st CBB; +typedef struct cbs_st CBS; +typedef struct conf_st CONF; +typedef struct dh_method DH_METHOD; +typedef struct dh_st DH; +typedef struct dsa_method DSA_METHOD; +typedef struct dsa_st DSA; +typedef struct ec_key_st EC_KEY; +typedef struct ecdsa_method_st ECDSA_METHOD; +typedef struct ecdsa_sig_st ECDSA_SIG; +typedef struct engine_st ENGINE; +typedef struct env_md_ctx_st EVP_MD_CTX; +typedef struct env_md_st EVP_MD; +typedef struct evp_aead_st EVP_AEAD; +typedef struct evp_cipher_ctx_st EVP_CIPHER_CTX; +typedef struct evp_cipher_st EVP_CIPHER; +typedef struct evp_pkey_asn1_method_st EVP_PKEY_ASN1_METHOD; +typedef struct evp_pkey_ctx_st EVP_PKEY_CTX; +typedef struct evp_pkey_method_st EVP_PKEY_METHOD; +typedef struct evp_pkey_st EVP_PKEY; +typedef struct hmac_ctx_st HMAC_CTX; +typedef struct md4_state_st MD4_CTX; +typedef struct md5_state_st MD5_CTX; +typedef struct pkcs8_priv_key_info_st PKCS8_PRIV_KEY_INFO; +typedef struct pkcs12_st PKCS12; +typedef struct rand_meth_st RAND_METHOD; +typedef struct rc4_key_st RC4_KEY; +typedef struct rsa_meth_st RSA_METHOD; +typedef struct rsa_st RSA; +typedef struct sha256_state_st SHA256_CTX; +typedef struct sha512_state_st SHA512_CTX; +typedef struct sha_state_st SHA_CTX; +typedef struct ssl_ctx_st SSL_CTX; +typedef struct ssl_st SSL; +typedef struct st_ERR_FNS ERR_FNS; +typedef struct v3_ext_ctx X509V3_CTX; +typedef struct x509_crl_method_st X509_CRL_METHOD; +typedef struct x509_revoked_st X509_REVOKED; +typedef struct x509_st X509; +typedef struct x509_store_ctx_st X509_STORE_CTX; +typedef struct x509_store_st X509_STORE; +typedef void *OPENSSL_BLOCK; + const EVP_MD *EVP_md4(void); + const EVP_MD *EVP_md5(void); + const EVP_MD *EVP_sha1(void); + const EVP_MD *EVP_sha224(void); + const EVP_MD *EVP_sha256(void); + const EVP_MD *EVP_sha384(void); + const EVP_MD *EVP_sha512(void); + + + + const EVP_MD *EVP_md5_sha1(void); + + + + const EVP_MD *EVP_get_digestbynid(int nid); + + + + const EVP_MD *EVP_get_digestbyobj(const ASN1_OBJECT *obj); + void EVP_MD_CTX_init(EVP_MD_CTX *ctx); + + + + EVP_MD_CTX *EVP_MD_CTX_create(void); + + + + int EVP_MD_CTX_cleanup(EVP_MD_CTX *ctx); + + + void EVP_MD_CTX_destroy(EVP_MD_CTX *ctx); + + + + int EVP_MD_CTX_copy_ex(EVP_MD_CTX *out, const EVP_MD_CTX *in); + + + + + + + + int EVP_DigestInit_ex(EVP_MD_CTX *ctx, const EVP_MD *type, + ENGINE *engine); + + + + int EVP_DigestInit(EVP_MD_CTX *ctx, const EVP_MD *type); + + + + int EVP_DigestUpdate(EVP_MD_CTX *ctx, const void *data, + size_t len); + int EVP_DigestFinal_ex(EVP_MD_CTX *ctx, uint8_t *md_out, + unsigned int *out_size); + + + + int EVP_DigestFinal(EVP_MD_CTX *ctx, uint8_t *md_out, + unsigned int *out_size); + + + + + + + int EVP_Digest(const void *data, size_t len, uint8_t *md_out, + unsigned int *md_out_size, const EVP_MD *type, + ENGINE *impl); + int EVP_MD_type(const EVP_MD *md); + + + const char *EVP_MD_name(const EVP_MD *md); + + + + uint32_t EVP_MD_flags(const EVP_MD *md); + + + size_t EVP_MD_size(const EVP_MD *md); + + + size_t EVP_MD_block_size(const EVP_MD *md); + int EVP_MD_CTX_copy(EVP_MD_CTX *out, const EVP_MD_CTX *in); + + + + int EVP_add_digest(const EVP_MD *digest); + + + + + + + const EVP_MD *EVP_MD_CTX_md(const EVP_MD_CTX *ctx); + + + + unsigned EVP_MD_CTX_size(const EVP_MD_CTX *ctx); + + + + unsigned EVP_MD_CTX_block_size(const EVP_MD_CTX *ctx); + + + + + int EVP_MD_CTX_type(const EVP_MD_CTX *ctx); + + + void EVP_MD_CTX_set_flags(EVP_MD_CTX *ctx, uint32_t flags); + + + + void EVP_MD_CTX_clear_flags(EVP_MD_CTX *ctx, uint32_t flags); + + + + uint32_t EVP_MD_CTX_test_flags(const EVP_MD_CTX *ctx, + uint32_t flags); + + +struct evp_md_pctx_ops; + +struct env_md_ctx_st { + + const EVP_MD *digest; + + uint32_t flags; + + + void *md_data; + + + + int (*update)(EVP_MD_CTX *ctx, const void *data, size_t count); + + + + EVP_PKEY_CTX *pctx; + + + + const struct evp_md_pctx_ops *pctx_ops; +} ; + + int MD4_Init(MD4_CTX *md4); + + + int MD4_Update(MD4_CTX *md4, const void *data, size_t len); + + + + + int MD4_Final(uint8_t *md, MD4_CTX *md4); + + + + void MD4_Transform(MD4_CTX *md4, const uint8_t *block); + +struct md4_state_st { + uint32_t A, B, C, D; + uint32_t Nl, Nh; + uint32_t data[16]; + unsigned int num; +}; + int MD5_Init(MD5_CTX *md5); + + + int MD5_Update(MD5_CTX *md5, const void *data, size_t len); + + + + + int MD5_Final(uint8_t *md, MD5_CTX *md5); + + + + uint8_t *MD5(const uint8_t *data, size_t len, uint8_t *out); + + + + void MD5_Transform(MD5_CTX *md5, const uint8_t *block); + +struct md5_state_st { + uint32_t A, B, C, D; + uint32_t Nl, Nh; + uint32_t data[16]; + unsigned int num; +}; +struct cbs_st { + const uint8_t *data; + size_t len; +}; + + + + void CBS_init(CBS *cbs, const uint8_t *data, size_t len); + + + + int CBS_skip(CBS *cbs, size_t len); + + + const uint8_t *CBS_data(const CBS *cbs); + + + size_t CBS_len(const CBS *cbs); + + + + + + + int CBS_stow(const CBS *cbs, uint8_t **out_ptr, size_t *out_len); + int CBS_strdup(const CBS *cbs, char **out_ptr); + + + + int CBS_contains_zero_byte(const CBS *cbs); + + + + + int CBS_mem_equal(const CBS *cbs, const uint8_t *data, + size_t len); + + + + int CBS_get_u8(CBS *cbs, uint8_t *out); + + + + int CBS_get_u16(CBS *cbs, uint16_t *out); + + + + int CBS_get_u24(CBS *cbs, uint32_t *out); + + + + int CBS_get_u32(CBS *cbs, uint32_t *out); + + + + int CBS_get_bytes(CBS *cbs, CBS *out, size_t len); + + + + + int CBS_get_u8_length_prefixed(CBS *cbs, CBS *out); + + + + + int CBS_get_u16_length_prefixed(CBS *cbs, CBS *out); + + + + + int CBS_get_u24_length_prefixed(CBS *cbs, CBS *out); + int CBS_get_asn1(CBS *cbs, CBS *out, unsigned tag_value); + + + + int CBS_get_asn1_element(CBS *cbs, CBS *out, unsigned tag_value); + + + + + + + int CBS_peek_asn1_tag(const CBS *cbs, unsigned tag_value); + int CBS_get_any_asn1_element(CBS *cbs, CBS *out, + unsigned *out_tag, + size_t *out_header_len); + + + + + + int CBS_get_asn1_uint64(CBS *cbs, uint64_t *out); + + + + + + + int CBS_get_optional_asn1(CBS *cbs, CBS *out, int *out_present, + unsigned tag); + + + + + + + + int CBS_get_optional_asn1_octet_string(CBS *cbs, CBS *out, + int *out_present, + unsigned tag); + + + + + + + int CBS_get_optional_asn1_uint64(CBS *cbs, uint64_t *out, + unsigned tag, + uint64_t default_value); + + + + + + + int CBS_get_optional_asn1_bool(CBS *cbs, int *out, unsigned tag, + int default_value); +struct cbb_buffer_st { + uint8_t *buf; + size_t len; + size_t cap; + char can_resize; + +}; + +struct cbb_st { + struct cbb_buffer_st *base; + + + size_t offset; + + struct cbb_st *child; + + + uint8_t pending_len_len; + char pending_is_asn1; + + + char is_top_level; +}; + + + + + int CBB_init(CBB *cbb, size_t initial_capacity); + + + + + int CBB_init_fixed(CBB *cbb, uint8_t *buf, size_t len); + + + + + void CBB_cleanup(CBB *cbb); + int CBB_finish(CBB *cbb, uint8_t **out_data, size_t *out_len); + + + + + int CBB_flush(CBB *cbb); + + + + + int CBB_add_u8_length_prefixed(CBB *cbb, CBB *out_contents); + + + + + int CBB_add_u16_length_prefixed(CBB *cbb, CBB *out_contents); + + + + + int CBB_add_u24_length_prefixed(CBB *cbb, CBB *out_contents); + + + + + + + int CBB_add_asn1(CBB *cbb, CBB *out_contents, uint8_t tag); + + + + int CBB_add_bytes(CBB *cbb, const uint8_t *data, size_t len); + + + + + + int CBB_add_space(CBB *cbb, uint8_t **out_data, size_t len); + + + + int CBB_add_u8(CBB *cbb, uint8_t value); + + + + int CBB_add_u16(CBB *cbb, uint16_t value); + + + + int CBB_add_u24(CBB *cbb, uint32_t value); + + + + + int CBB_add_asn1_uint64(CBB *cbb, uint64_t value); + ASN1_OBJECT *OBJ_dup(const ASN1_OBJECT *obj); + + + + int OBJ_cmp(const ASN1_OBJECT *a, const ASN1_OBJECT *b); + + + + + + + int OBJ_obj2nid(const ASN1_OBJECT *obj); + + + + int OBJ_cbs2nid(const CBS *cbs); + + + + int OBJ_sn2nid(const char *short_name); + + + + int OBJ_ln2nid(const char *long_name); + + + + + int OBJ_txt2nid(const char *s); + + + + + + + const ASN1_OBJECT *OBJ_nid2obj(int nid); + + + const char *OBJ_nid2sn(int nid); + + + const char *OBJ_nid2ln(int nid); + + + + int OBJ_nid2cbb(CBB *out, int nid); + ASN1_OBJECT *OBJ_txt2obj(const char *s, int dont_search_names); + int OBJ_obj2txt(char *out, int out_len, const ASN1_OBJECT *obj, + int dont_return_name); + + + + + + + int OBJ_create(const char *oid, const char *short_name, + const char *long_name); + int OBJ_find_sigid_algs(int sign_nid, int *out_digest_nid, + int *out_pkey_nid); + + + + + + + int OBJ_find_sigid_by_algs(int *out_sign_nid, int digest_nid, + int pkey_nid); + int SHA1_Init(SHA_CTX *sha); + + + int SHA1_Update(SHA_CTX *sha, const void *data, size_t len); + + + + + int SHA1_Final(uint8_t *md, SHA_CTX *sha); + + + + + uint8_t *SHA1(const uint8_t *data, size_t len, uint8_t *out); + + + + void SHA1_Transform(SHA_CTX *sha, const uint8_t *block); + +struct sha_state_st { + uint32_t h0, h1, h2, h3, h4; + uint32_t Nl, Nh; + uint32_t data[16]; + unsigned int num; +}; + int SHA224_Init(SHA256_CTX *sha); + + + int SHA224_Update(SHA256_CTX *sha, const void *data, size_t len); + + + + int SHA224_Final(uint8_t *md, SHA256_CTX *sha); + + + + + uint8_t *SHA224(const uint8_t *data, size_t len, uint8_t *out); + int SHA256_Init(SHA256_CTX *sha); + + + int SHA256_Update(SHA256_CTX *sha, const void *data, size_t len); + + + + int SHA256_Final(uint8_t *md, SHA256_CTX *sha); + + + + + uint8_t *SHA256(const uint8_t *data, size_t len, uint8_t *out); + + + + void SHA256_Transform(SHA256_CTX *sha, const uint8_t *data); + +struct sha256_state_st { + uint32_t h[8]; + uint32_t Nl, Nh; + uint32_t data[16]; + unsigned int num, md_len; +}; + int SHA384_Init(SHA512_CTX *sha); + + + int SHA384_Update(SHA512_CTX *sha, const void *data, size_t len); + + + + int SHA384_Final(uint8_t *md, SHA512_CTX *sha); + + + + + uint8_t *SHA384(const uint8_t *data, size_t len, uint8_t *out); + + + + void SHA384_Transform(SHA512_CTX *sha, const uint8_t *data); + int SHA512_Init(SHA512_CTX *sha); + + + int SHA512_Update(SHA512_CTX *sha, const void *data, size_t len); + + + + int SHA512_Final(uint8_t *md, SHA512_CTX *sha); + + + + + uint8_t *SHA512(const uint8_t *data, size_t len, uint8_t *out); + + + + void SHA512_Transform(SHA512_CTX *sha, const uint8_t *data); + +struct sha512_state_st { + uint64_t h[8]; + uint64_t Nl, Nh; + union { + uint64_t d[16]; + uint8_t p[128]; + } u; + unsigned int num, md_len; +}; + +struct env_md_st { + + + int type; + + + unsigned md_size; + + + uint32_t flags; + + + + int (*init)(EVP_MD_CTX *ctx); + + + int (*update)(EVP_MD_CTX *ctx, const void *data, size_t count); + + + int (*final)(EVP_MD_CTX *ctx, uint8_t *out); + + + unsigned block_size; + + + unsigned ctx_size; +}; + + + + +struct evp_md_pctx_ops { + + + void (*free) (EVP_PKEY_CTX *pctx); + + + + EVP_PKEY_CTX* (*dup) (EVP_PKEY_CTX *pctx); + + + + int (*begin_digest) (EVP_MD_CTX *ctx); +}; + + +static int md4_init(EVP_MD_CTX *ctx) { return MD4_Init(ctx->md_data); } + +static int md4_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return MD4_Update(ctx->md_data, data, count); +} + +static int md4_final(EVP_MD_CTX *ctx, unsigned char *out) { + return MD4_Final(out, ctx->md_data); +} + +static const EVP_MD md4_md = { + 257, 16, 0 , md4_init, + md4_update, md4_final, 64 , sizeof(MD4_CTX), +}; + +const EVP_MD *EVP_md4(void) { return &md4_md; } + + +static int md5_init(EVP_MD_CTX *ctx) { return MD5_Init(ctx->md_data); } + +static int md5_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return MD5_Update(ctx->md_data, data, count); +} + +static int md5_final(EVP_MD_CTX *ctx, unsigned char *out) { + return MD5_Final(out, ctx->md_data); +} + +static const EVP_MD md5_md = { + 4, 16, 0 , md5_init, + md5_update, md5_final, 64 , sizeof(MD5_CTX), +}; + +const EVP_MD *EVP_md5(void) { return &md5_md; } + + +static int sha1_init(EVP_MD_CTX *ctx) { return SHA1_Init(ctx->md_data); } + +static int sha1_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return SHA1_Update(ctx->md_data, data, count); +} + +static int sha1_final(EVP_MD_CTX *ctx, unsigned char *md) { + return SHA1_Final(md, ctx->md_data); +} + +static const EVP_MD sha1_md = { + 64, 20, 0 , sha1_init, + sha1_update, sha1_final, 64 , sizeof(SHA_CTX), +}; + +const EVP_MD *EVP_sha1(void) { return &sha1_md; } + + +static int sha224_init(EVP_MD_CTX *ctx) { return SHA224_Init(ctx->md_data); } + +static int sha224_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return SHA224_Update(ctx->md_data, data, count); +} + +static int sha224_final(EVP_MD_CTX *ctx, unsigned char *md) { + return SHA224_Final(md, ctx->md_data); +} + +static const EVP_MD sha224_md = { + 675, 28, 0 , + sha224_init, sha224_update, sha224_final, + 64 , sizeof(SHA256_CTX), +}; + +const EVP_MD *EVP_sha224(void) { return &sha224_md; } + + +static int sha256_init(EVP_MD_CTX *ctx) { return SHA256_Init(ctx->md_data); } + +static int sha256_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return SHA256_Update(ctx->md_data, data, count); +} + +static int sha256_final(EVP_MD_CTX *ctx, unsigned char *md) { + return SHA256_Final(md, ctx->md_data); +} + +static const EVP_MD sha256_md = { + 672, 32, 0 , + sha256_init, sha256_update, sha256_final, + 64 , sizeof(SHA256_CTX), +}; + +const EVP_MD *EVP_sha256(void) { return &sha256_md; } + + +static int sha384_init(EVP_MD_CTX *ctx) { return SHA384_Init(ctx->md_data); } + +static int sha384_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return SHA384_Update(ctx->md_data, data, count); +} + +static int sha384_final(EVP_MD_CTX *ctx, unsigned char *md) { + return SHA384_Final(md, ctx->md_data); +} + +static const EVP_MD sha384_md = { + 673, 48, 0 , + sha384_init, sha384_update, sha384_final, + 128 , sizeof(SHA512_CTX), +}; + +const EVP_MD *EVP_sha384(void) { return &sha384_md; } + + +static int sha512_init(EVP_MD_CTX *ctx) { return SHA512_Init(ctx->md_data); } + +static int sha512_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return SHA512_Update(ctx->md_data, data, count); +} + +static int sha512_final(EVP_MD_CTX *ctx, unsigned char *md) { + return SHA512_Final(md, ctx->md_data); +} + +static const EVP_MD sha512_md = { + 674, 64, 0 , + sha512_init, sha512_update, sha512_final, + 128 , sizeof(SHA512_CTX), +}; + +const EVP_MD *EVP_sha512(void) { return &sha512_md; } + + +typedef struct { + MD5_CTX md5; + SHA_CTX sha1; +} MD5_SHA1_CTX; + +static int md5_sha1_init(EVP_MD_CTX *md_ctx) { + MD5_SHA1_CTX *ctx = md_ctx->md_data; + return MD5_Init(&ctx->md5) && SHA1_Init(&ctx->sha1); +} + +static int md5_sha1_update(EVP_MD_CTX *md_ctx, const void *data, size_t count) { + MD5_SHA1_CTX *ctx = md_ctx->md_data; + return MD5_Update(&ctx->md5, data, count) && SHA1_Update(&ctx->sha1, data, count); +} + +static int md5_sha1_final(EVP_MD_CTX *md_ctx, unsigned char *out) { + MD5_SHA1_CTX *ctx = md_ctx->md_data; + if (!MD5_Final(out, &ctx->md5) || + !SHA1_Final(out + 16, &ctx->sha1)) { + return 0; + } + return 1; +} + +static const EVP_MD md5_sha1_md = { + 114, + 16 + 20, + 0 , + md5_sha1_init, + md5_sha1_update, + md5_sha1_final, + 64 , + sizeof(MD5_SHA1_CTX), +}; + +const EVP_MD *EVP_md5_sha1(void) { return &md5_sha1_md; } + + +struct nid_to_digest { + int nid; + const EVP_MD* (*md_func)(void); +}; + +static const struct nid_to_digest nid_to_digest_mapping[] = { + { 4, EVP_md5 }, + { 64, EVP_sha1 }, + { 675, EVP_sha224 }, + { 672, EVP_sha256 }, + { 673, EVP_sha384 }, + { 674, EVP_sha512 }, + { 114, EVP_md5_sha1 }, + { 66, EVP_sha1 }, + { 113, EVP_sha1 }, + { 416, EVP_sha1 }, + { 8, EVP_md5 }, + { 65, EVP_sha1 }, + { 671, EVP_sha224 }, + { 668, EVP_sha256 }, + { 669, EVP_sha384 }, + { 670, EVP_sha512 }, +}; + +const EVP_MD* EVP_get_digestbynid(int nid) { + unsigned i; + + for (i = 0; i < sizeof(nid_to_digest_mapping) / sizeof(struct nid_to_digest); + i++) { + if (nid_to_digest_mapping[i].nid == nid) { + return nid_to_digest_mapping[i].md_func(); + } + } + + return + ((void *)0) + ; +} + +const EVP_MD* EVP_get_digestbyobj(const ASN1_OBJECT *obj) { + return EVP_get_digestbynid(OBJ_obj2nid(obj)); +} diff --git a/test/csyntaxgen/issue216.c b/test/csyntaxgen/issue216.c new file mode 100644 index 0000000000..796b69b408 --- /dev/null +++ b/test/csyntaxgen/issue216.c @@ -0,0 +1,5 @@ +#include + +struct list {unsigned head; struct list *tail;}; +struct list three[] = { {1, three+1}, {2, three+2}, {3, NULL} }; +int f(int x) { return x;} diff --git a/test/csyntaxgen/issue319.c b/test/csyntaxgen/issue319.c new file mode 100644 index 0000000000..be9f3f7e61 --- /dev/null +++ b/test/csyntaxgen/issue319.c @@ -0,0 +1,12 @@ +/* Dollar signs in identifiers */ + +int c$d = 42; + +int a$b(int x$$) { + return c$d + x$$; +} + +int main(int argc, const char *argv[]) +{ + return a$b(6); +}