[DO NOT MERGE] V3.11

.gitattributes

@@ -1,3 +1,3 @@
 # Files that should be ignored by Github linguist
-test/* linguist-vendored
-doc/* linguist-documentation
+/test/** linguist-vendored
+/doc/** linguist-documentation

.gitignore

@@ -17,6 +17,7 @@ graph.png
 .*.aux
 *.cmti
 *.cmt
+.coq-native
 # Emacs saves
 *~
 # Executables and configuration
@@ -78,7 +79,8 @@ graph.png
 # MacOS metadata
 .DS_Store
 # Test generated data
-/test/clightgen/*.v
+/test/export/clight/*.v
+/test/export/csyntax/*.v
 # Coq caches
 .lia.cache
 .nia.cache

Changelog

@@ -1,3 +1,107 @@
+Release 3.11, 2022-06-27
+========================
+
+New features:
+- Support `_Generic` expressions from ISO C11.
+
+ISO C conformance:
+- Enumeration types are compatible only with `int` but not with
+  other integer types.
+- Fixed confusion between unprototyped function pointer types `T (*)()` and
+  prototyped, zero-argument function pointer types `T (*)(void)`
+  in type casts (#431).
+
+Usability:
+- Improved control-flow analysis of calls to "noreturn" functions,
+  resulting in more accurate warnings.
+- More detailed warning for unprototyped function definitions, now shows
+  the prototyped type that is given to the function.
+- Extended the warning above to definitions of the form `T f() { ... }`,
+  i.e. unprototyped but with no parameters.  (Before, the warning would
+  trigger only if parameters were declared.)
+- Check (and warn if requested) for arguments of struct/union types passed
+  to a variable-argument function.
+
+Bug fixes:
+- RISC-V: fixed an error in the modeling of float32 <-> float64 conversions
+  when the argument is a NaN (#428).
+- x86: changed the compilation of `__builtin_fmin` and `__builtin_fmax`
+  so that their NaN behavior is the one documented in the manual.
+- Improved reproducibility of register allocation.
+  (Before, compiling CompCert with two different OCaml versions could
+   have resulted in correct but different allocations.)
+- Hardened the configure script against Cygwin installations that produce
+  \r\n for end-of-lines (#434).
+- RISC-V: tail calls to far-away functions were causing link-time errors
+  (#436, #437).
+
+Coq development:
+- Updated the Flocq library to version 4.1.
+- Support for Coq 8.14.1, 8.15.0, 8.15.1, 8.15.2.
+- Minimal Coq version supported is now 8.12.0.
+
+
+Release 3.10, 2021-11-19
+========================
+
+Major improvement:
+- Bit fields in structs and unions are now handled in the
+  formally-verified part of CompCert. (Before, they were being
+  implemented through an unverified source-to-source translation.)
+  The CompCert C and Clight languages provide abstract syntax for
+  bit-field declarations and formal semantics for bit-field accesses.
+  The translation of bit-field accesses to bit manipulations is
+  performed in the Cshmgen pass and proved correct.
+
+Usability:
+- The layout of bit-fields in memory now follows the ELF ABI
+  algorithm, improving ABI compatibility for the CompCert target
+  platforms that use ELF.
+- Handle the `# 0` line directive generated by some C preprocessors (#398).
+- Un-define the `__SIZEOF_INT128__` macro that is predefined by some C
+  preprocessors (#419).
+- macOS assembler: use `##` instead of `#` to delimit comments (#399).
+
+ISO C conformance:
+- Stricter checking of multi-character constants `'abc'`.
+  Multi-wide-character constants `L'ab'` are now rejected,
+  like GCC and Clang do.
+- Ignore (but still warn about) unnamed plain members of structs
+  and unions (#411).
+- Ignore unnamed bit fields when initializing unions.
+
+Bug fixing:
+- x86 64 bits: overflow in offset of `leaq` instructions (#407).
+- AArch64, ARM, PowerPC, RISC-V: wrong expansion of `__builtin_memcpy_aligned`
+  in cases involving arguments that are stack addresses (#410, #412)
+- PowerPC 64 bits: wrong selection of 64-bit rotate-and-mask
+  instructions (`rldic`, `rldicl`, `rldicr`), resulting in assertion
+  failures later in the compiler.
+- RISC-V: update the Asm semantics to reflect the fact that
+  register X1 is destroyed by some builtins.
+
+Compiler internals:
+- The "PTree" data structure (binary tries) was reimplemented, using
+  a canonical representation that guarantees extensionality and
+  improves performance.
+- Add the ability to give formal semantics to numerical builtins
+  with small integer return types.
+- PowerPC: share code for memory accesses between Asmgen and Asmexpand
+- Declare `__compcert_i64*` helper runtime functions during the C2C
+  pass, so that they are not visible during source elaboration.
+
+The clightgen tool:
+- Add support for producing Csyntax abstract syntax instead of Clight
+  abstract syntax (option `-csyntax` to `clightgen`)
+  (contributed by Bart Jacobs; #404, #413).
+
+Coq development:
+- Added support for Coq 8.14 (#415).
+- Added support for OCaml 4.13.
+- Updated the Flocq library to version 3.4.2.
+- Replaced `Global Set Asymmetric Patterns` by more local settings (#408).
+
+
 Release 3.9, 2021-05-10
 =======================
 

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

Makefile

@@ -28,7 +28,7 @@ else
 ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
 endif
 
-DIRS := lib common $(ARCHDIRS) backend cfrontend driver exportclight cparser demo
+DIRS := lib common $(ARCHDIRS) backend cfrontend driver export cparser demo
 
 COQINCLUDES := $(foreach d, $(DIRS), -R $(d) compcertr.$(d))
 
@@ -53,11 +53,21 @@ endif
 # deprecated-ident-entry:
 #    warning introduced in 8.13
 #    suggested change (use `name` instead of `ident`) supported since 8.13
+# deprecated-hint-rewrite-without-locality:
+#    warning introduced in 8.14
+#    suggested change (add Global or Local or [#export] modifier)
+#    is not supported in 8.13 nor in 8.11, but was supported in 8.9 (go figure)
+# deprecated-instance-without-locality:
+#    warning introduced in 8.14
+#    triggered by Menhir-generated files, to be solved upstream in Menhir
 
 COQCOPTS ?= \
   -w -undeclared-scope \
   -w -unused-pattern-matching-variable \
-  -w -deprecated-ident-entry
+  -w -deprecated-ident-entry \
+  -w -deprecated-hint-rewrite-without-locality
+
+cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
 
 COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
 COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
@@ -74,13 +84,12 @@ GPATH=$(DIRS)
 
 ifeq ($(LIBRARY_FLOCQ),local)
 FLOCQ=\
-  SpecFloatCompat.v \
   Raux.v Zaux.v Defs.v Digits.v Float_prop.v FIX.v FLT.v FLX.v FTZ.v \
   Generic_fmt.v Round_pred.v Round_NE.v Ulp.v Core.v \
-  Bracket.v Div.v Operations.v Round.v Sqrt.v \
+  Bracket.v Div.v Operations.v Plus.v Round.v Sqrt.v \
   Div_sqrt_error.v Mult_error.v Plus_error.v \
   Relative.v Sterbenz.v Round_odd.v Double_rounding.v \
-  Binary.v Bits.v
+  BinarySingleNaN.v Binary.v Bits.v
 else
 FLOCQ=
 endif
@@ -159,10 +168,18 @@ endif
 
 DRIVER=Compopts.v Compiler.v Complements.v
 
+# Library for .v files generated by clightgen
+
+ifeq ($(CLIGHTGEN),true)
+EXPORTLIB=Ctypesdefs.v Clightdefs.v Csyntaxdefs.v
+else
+EXPORTLIB=
+endif
+
 # All source files
 
 FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \
-  $(MENHIRLIB) $(PARSER) exportclight/Clightdefs.v
+  $(MENHIRLIB) $(PARSER) $(EXPORTLIB)
 
 # Generated source files
 
@@ -214,9 +231,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 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 driver/Version.ml FORCE
 	$(MAKE) -f Makefile.extr clightgen.byte
 
 runtime:
@@ -311,7 +328,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
 

Makefile.extr

@@ -45,13 +45,13 @@ cparser/pre_parser_messages.ml:
 
 DIRS=extraction \
   lib common $(ARCH) backend cfrontend cparser driver \
-  exportclight debug
+  export debug
 
 INCLUDES=$(patsubst %,-I %, $(DIRS))
 
 # Control of warnings:
 
-WARNINGS=-w +a-4-9-27
+WARNINGS=-w +a-4-9-27-70
 extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
 extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
 cparser/pre_parser.cmx: WARNINGS += -w -41
@@ -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/ExportDriver.cmx)
 
 ifeq ($(OCAML_NATIVE_COMP),true)
 clightgen: $(CLIGHTGEN_OBJS)

MenhirLib/Alphabet.v

@@ -11,7 +11,7 @@
 (*                                                                          *)
 (****************************************************************************)
 
-From Coq Require Import Omega List Relations RelationClasses.
+From Coq Require Import ZArith List Relations RelationClasses.
 Import ListNotations.
 
 Local Obligation Tactic := intros.
@@ -37,7 +37,7 @@ Qed.
 Definition comparableLt {A:Type} (C: Comparable A) : relation A :=
   fun x y => compare x y = Lt.
 
-Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) :
+Global Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) :
   StrictOrder (comparableLt C).
 Proof.
 apply Build_StrictOrder.
@@ -53,7 +53,7 @@ apply compare_trans.
 Qed.
 
 (** nat is comparable. **)
-Program Instance natComparable : Comparable nat :=
+Global Program Instance natComparable : Comparable nat :=
   { compare := Nat.compare }.
 Next Obligation.
 symmetry.
@@ -79,7 +79,7 @@ apply (gt_trans _ _ _ H H0).
 Qed.
 
 (** A pair of comparable is comparable. **)
-Program Instance PairComparable {A:Type} (CA:Comparable A) {B:Type} (CB:Comparable B) :
+Global Program Instance PairComparable {A:Type} (CA:Comparable A) {B:Type} (CB:Comparable B) :
   Comparable (A*B) :=
   { compare := fun x y =>
       let (xa, xb) := x in let (ya, yb) := y in
@@ -134,10 +134,10 @@ destruct H.
 rewrite compare_refl; intuition.
 Qed.
 
-Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq.
+Global Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq.
 
 (** A pair of ComparableLeibnizEq is ComparableLeibnizEq **)
-Instance PairComparableLeibnizEq
+Global Instance PairComparableLeibnizEq
   {A:Type} {CA:Comparable A} (UA:ComparableLeibnizEq CA)
   {B:Type} {CB:Comparable B} (UB:ComparableLeibnizEq CB) :
     ComparableLeibnizEq (PairComparable CA CB).
@@ -174,7 +174,7 @@ Class Numbered (A:Type) := {
   inj_bound_spec : forall x, (inj x < Pos.succ inj_bound)%positive
 }.
 
-Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
+Global Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
   { AlphabetComparable := {| compare := fun x y => Pos.compare (inj x) (inj y) |};
     AlphabetFinite :=
       {| all_list := fst (Pos.iter
@@ -224,7 +224,7 @@ Import OrderedType.
 
 Module Type ComparableM.
   Parameter t : Type.
-  Declare Instance tComparable : Comparable t.
+  Global Declare Instance tComparable : Comparable t.
 End ComparableM.
 
 Module OrderedTypeAlt_from_ComparableM (C:ComparableM) <: OrderedTypeAlt.

MenhirLib/Automaton.v

@@ -23,10 +23,10 @@ Module Type AutInit.
 
   (** The set of non initial state is considered as an alphabet. **)
   Parameter noninitstate : Type.
-  Declare Instance NonInitStateAlph : Alphabet noninitstate.
+  Global Declare Instance NonInitStateAlph : Alphabet noninitstate.
 
   Parameter initstate : Type.
-  Declare Instance InitStateAlph : Alphabet initstate.
+  Global Declare Instance InitStateAlph : Alphabet initstate.
 
   (** When we are at this state, we know that this symbol is the top of the
      stack. **)
@@ -41,7 +41,7 @@ Module Types(Import Init:AutInit).
     | Init: initstate -> state
     | Ninit: noninitstate -> state.
 
-  Program Instance StateAlph : Alphabet state :=
+  Global Program Instance StateAlph : Alphabet state :=
     { AlphabetComparable := {| compare := fun x y =>
         match x, y return comparison with
           | Init _, Ninit _ => Lt

MenhirLib/Grammar.v

@@ -18,8 +18,8 @@ Require Import Alphabet.
 (** The terminal non-terminal alphabets of the grammar. **)
 Module Type Alphs.
   Parameters terminal nonterminal : Type.
-  Declare Instance TerminalAlph: Alphabet terminal.
-  Declare Instance NonTerminalAlph: Alphabet nonterminal.
+  Global Declare Instance TerminalAlph: Alphabet terminal.
+  Global Declare Instance NonTerminalAlph: Alphabet nonterminal.
 End Alphs.
 
 (** Definition of the alphabet of symbols, given the alphabet of terminals
@@ -30,7 +30,7 @@ Module Symbol(Import A:Alphs).
     | T: terminal -> symbol
     | NT: nonterminal -> symbol.
 
-  Program Instance SymbolAlph : Alphabet symbol :=
+  Global Program Instance SymbolAlph : Alphabet symbol :=
     { AlphabetComparable := {| compare := fun x y =>
         match x, y return comparison with
           | T _, NT _ => Gt
@@ -74,7 +74,7 @@ Module Type T.
 
   (** The type of productions identifiers **)
   Parameter production : Type.
-  Declare Instance ProductionAlph : Alphabet production.
+  Global Declare Instance ProductionAlph : Alphabet production.
 
   (** Accessors for productions: left hand side, right hand side,
      and semantic action. The semantic actions are given in the form