From 0f919eb26c68d3882e612a1b3a9df45bee6d3624 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 13 Feb 2019 18:53:17 +0100 Subject: Upgrade embedded version of Flocq to 3.1. Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully). --- Makefile | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 0247b688..5a9701aa 100644 --- a/Makefile +++ b/Makefile @@ -22,8 +22,8 @@ ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) endif DIRS=lib common $(ARCHDIRS) backend cfrontend driver \ - flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight \ - cparser cparser/MenhirLib + flocq/Core flocq/Prop flocq/Calc flocq/IEEE754 \ + exportclight cparser cparser/MenhirLib RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight cparser @@ -43,15 +43,12 @@ GPATH=$(DIRS) # Flocq FLOCQ=\ - Fcore_Raux.v Fcore_Zaux.v Fcore_defs.v Fcore_digits.v \ - Fcore_float_prop.v Fcore_FIX.v Fcore_FLT.v Fcore_FLX.v \ - Fcore_FTZ.v Fcore_generic_fmt.v Fcore_rnd.v Fcore_rnd_ne.v \ - Fcore_ulp.v Fcore.v \ - Fcalc_bracket.v Fcalc_digits.v Fcalc_div.v Fcalc_ops.v \ - Fcalc_round.v Fcalc_sqrt.v \ - Fprop_div_sqrt_error.v Fprop_mult_error.v Fprop_plus_error.v \ - Fprop_relative.v Fprop_Sterbenz.v \ - Fappli_rnd_odd.v Fappli_double_round.v Fappli_IEEE.v Fappli_IEEE_bits.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 \ + Div_sqrt_error.v Mult_error.v Plus_error.v \ + Relative.v Sterbenz.v Round_odd.v Double_rounding.v \ + Binary.v Bits.v # General-purpose libraries (in lib/) -- cgit From 08fd5faf30c18e17caa610076e67cf002a01d8b4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 24 Apr 2019 14:02:32 +0200 Subject: Move Z definitions out of Integers and into Zbits The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 5a9701aa..7b1d3a76 100644 --- a/Makefile +++ b/Makefile @@ -53,7 +53,7 @@ FLOCQ=\ # General-purpose libraries (in lib/) VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ - Iteration.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \ + Iteration.v Zbits.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \ Parmov.v UnionFind.v Wfsimpl.v \ Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v -- cgit From 8df51b9866ccda99980e9f4de7ec2f2a0cd416e6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 26 Apr 2019 14:17:38 +0200 Subject: Rename Fappli_IEEE_extra.v into IEEE754_extra.v To match the new module names from version 3 of Flocq. Plus, it's shorter. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 7b1d3a76..dc98e7a0 100644 --- a/Makefile +++ b/Makefile @@ -53,7 +53,7 @@ FLOCQ=\ # General-purpose libraries (in lib/) VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \ - Iteration.v Zbits.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \ + Iteration.v Zbits.v Integers.v Archi.v IEEE754_extra.v Floats.v \ Parmov.v UnionFind.v Wfsimpl.v \ Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v -- cgit From 5b7fc96afb149ad916a9bf5015fe1eb2e0baaa7c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 17 May 2019 17:30:03 +0200 Subject: Prepend $(DESTDIR) to the installation target (#169) Following the gnu Makefile Conventions the variable $(DESTDIR) should be prepended to all installation commands. This allows staged installs. --- Makefile | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index dc98e7a0..8ab6b5b0 100644 --- a/Makefile +++ b/Makefile @@ -235,24 +235,24 @@ depend1: $(FILES) exportclight/Clightdefs.v @$(COQDEP) $^ > .depend install: - install -d $(BINDIR) - install -m 0755 ./ccomp $(BINDIR) - install -d $(SHAREDIR) - install -m 0644 ./compcert.ini $(SHAREDIR) - install -d $(MANDIR)/man1 - install -m 0644 ./doc/ccomp.1 $(MANDIR)/man1 + install -d $(DESTDIR)$(BINDIR) + install -m 0755 ./ccomp $(DESTDIR)$(BINDIR) + install -d $(DESTDIR)$(SHAREDIR) + install -m 0644 ./compcert.ini $(DESTDIR)$(SHAREDIR) + install -d $(DESTDIR)$(MANDIR)/man1 + install -m 0644 ./doc/ccomp.1 $(DESTDIR)$(MANDIR)/man1 $(MAKE) -C runtime install ifeq ($(CLIGHTGEN),true) - install -m 0755 ./clightgen $(BINDIR) + install -m 0755 ./clightgen $(DESTDIR)$(BINDIR) endif ifeq ($(INSTALL_COQDEV),true) - install -d $(COQDEVDIR) + install -d $(DESTDIR)$(COQDEVDIR) for d in $(DIRS); do \ - install -d $(COQDEVDIR)/$$d && \ - install -m 0644 $$d/*.vo $(COQDEVDIR)/$$d/; \ + install -d $(DESTDIR)$(COQDEVDIR)/$$d && \ + install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \ done - install -m 0644 ./VERSION $(COQDEVDIR) - @(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(COQDEVDIR)/README + install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR) + @(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README endif -- cgit From be028b543f48577f762ffb26e79e2a482b4ff15d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 31 May 2019 19:09:25 +0200 Subject: Type inference and type checking for Cminor This module is similar to RTLtyping: it performs type inference and type checking, but on the Cminor intermediate representation rather than the RTL IR. For each function, it returns a mapping from variables to types. Its first use will be if-conversion optimization. --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 8ab6b5b0..369fd4cd 100644 --- a/Makefile +++ b/Makefile @@ -67,7 +67,7 @@ COMMON=Errors.v AST.v Linking.v \ # Back-end modules (in backend/, $(ARCH)/) BACKEND=\ - Cminor.v Op.v CminorSel.v \ + Cminor.v Cminortyping.v Op.v CminorSel.v \ SelectOp.v SelectDiv.v SplitLong.v SelectLong.v Selection.v \ SelectOpproof.v SelectDivproof.v SplitLongproof.v \ SelectLongproof.v Selectionproof.v \ -- cgit