From 7a614ea53948423b0266eefd98ea5714559c3cfc Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 28 Jun 2012 11:23:52 +0000 Subject: Changelog: updated driver/Interp.ml: clean up dead code lib/Integers.v: add shifted_or_is_add lib/Floats.v: add from_words_eq .depend: updated git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- .depend | 8 ++++---- Changelog | 38 ++++++++++++++++++++++++++++++++++++++ driver/Interp.ml | 25 +------------------------ lib/Floats.v | 14 ++++++++++++++ lib/Integers.v | 40 ++++++++++++++++++++++++++++++++++++++++ 5 files changed, 97 insertions(+), 28 deletions(-) diff --git a/.depend b/.depend index df0d8746..8e69f1b3 100644 --- a/.depend +++ b/.depend @@ -7,7 +7,7 @@ lib/Lattice.vo lib/Lattice.glob: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo lib/Ordered.glob: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Iteration.vo lib/Iteration.glob: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo lib/Wfsimpl.vo lib/Integers.vo lib/Integers.glob: lib/Integers.v lib/Axioms.vo lib/Coqlib.vo -lib/Floats.vo lib/Floats.glob: lib/Floats.v lib/Axioms.vo lib/Coqlib.vo lib/Integers.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo flocq/Core/Fcore.vo +lib/Floats.vo lib/Floats.glob: lib/Floats.v lib/Axioms.vo lib/Coqlib.vo lib/Integers.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo flocq/Core/Fcore.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Prop/Fprop_Sterbenz.vo lib/Parmov.vo lib/Parmov.glob: lib/Parmov.v lib/Axioms.vo lib/Coqlib.vo lib/UnionFind.vo lib/UnionFind.glob: lib/UnionFind.v lib/Coqlib.vo lib/Wfsimpl.vo lib/Wfsimpl.glob: lib/Wfsimpl.v lib/Axioms.vo @@ -95,9 +95,9 @@ backend/Stackingtyping.vo backend/Stackingtyping.glob: backend/Stackingtyping.v backend/Machsem.vo backend/Machsem.glob: backend/Machsem.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asm.vo $(ARCH)/Asm.glob: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo -$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo -$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo -$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo +$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo +$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo +$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo diff --git a/Changelog b/Changelog index c63dc66c..f07154c4 100644 --- a/Changelog +++ b/Changelog @@ -1,4 +1,12 @@ +Release 1.11 +======================== + +Improvements in confidence: +- Floating-point numbers and arithmetic operations, previously axiomatized, + are now implemented and proved correct in Coq, using the Flocq library + of S. Boldo and G. Melquiond. +Language semantics: - In accordance with ISO C standards, the signed division min_int / -1 and the signed remainder min_int % -1 (where min_int is the smallest representable signed integer) now have undefined semantics and are @@ -7,6 +15,36 @@ but this behavior requires unnatural code to be generated on IA32 and PowerPC.) +Performance improvements: +- Function inlining is now implemented. The functions that are inlined + are those declared "inline" in the C source, provided they are not + recursive. +- Constant propagation is now able to propagate the initial values of + "const" global variables. +- Added option -ffloat-const-prop to control the propagation of + floating-point constants; see user's manual for documentation. +- Common subexpression elimination can now eliminate memory loads + following a memory store at the same location. +- ARM: make use of the "fcmpzd" and "fmdrr" instructions. + +New tool: +- The "cchecklink" tool performs a posteriori validation of the + assembling and linking phases. It is available for PowerPC-EABI + only. It takes as inputs an ELF-PowerPC executable as produced + by the linker, as well as .sdump files (abstract assembly) as + produced by "ccomp -sdump", and checks that the executable contains + properly-assembled and linked code and data corresponding to those + produced by CompCert. + +Other changes: +- Elimination of "static" functions and global variables that are unused. +- The memory model was enriched with "max" permissions in addition to + "current" permissions, to better reason over "const" blocks and + already-deallocated blocks. +- More efficient implementation of the memory model, resulting + in faster interpretation of source files by "ccomp -interp". + + Release 1.10, 2012-03-13 ======================== diff --git a/driver/Interp.ml b/driver/Interp.ml index 0c19673d..abd28acb 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -147,32 +147,9 @@ let mem_of_state = function (* Comparing memory states *) -let compare_mem m1 m2 = +let compare_mem m1 m2 = (* should permissions be taken into account? *) Pervasives.compare (m1.Mem.nextblock, m1.Mem.mem_contents) (m2.Mem.nextblock, m1.Mem.mem_contents) -(* FIXME: should permissions be taken into account? *) - -(* -let rec compare_Z_range lo hi f = - if coq_Zcompare lo hi = Lt then begin - let c = f lo in if c <> 0 then c else compare_Z_range (coq_Zsucc lo) hi f - end else 0 - -let compare_mem m1 m2 = - if m1 == m2 then 0 else - let c = compare m1.Mem.nextblock m2.Mem.nextblock in if c <> 0 then c else - compare_Z_range Z0 m1.Mem.nextblock (fun b -> - - let ((lo, hi) as bnds) = m1.Mem.bounds b in - let c = compare bnds (m2.Mem.bounds b) in if c <> 0 then c else - let contents1 = m1.Mem.mem_contents b and contents2 = m2.Mem.mem_contents b in - if contents1 == contents2 then 0 else - let c = compare_Z_range lo hi (fun ofs -> - compare (contents1 ofs) (contents2 ofs)) in if c <> 0 then c else - let access1 = m1.Mem.mem_access b and access2 = m2.Mem.mem_access b in - if access1 == access2 then 0 else - compare_Z_range lo hi (fun ofs -> compare (access1 ofs) (access2 ofs))) -*) (* Comparing continuations *) diff --git a/lib/Floats.v b/lib/Floats.v index e7a7aa0a..edb6d6bd 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -189,6 +189,20 @@ Definition from_words (hi lo: int) : float := (Int64.or (Int64.shl (Int64.repr (Int.unsigned hi)) (Int64.repr 32)) (Int64.repr (Int.unsigned lo))). +Lemma from_words_eq: + forall lo hi, + from_words hi lo = + double_of_bits (Int64.repr (Int.unsigned hi * two_p 32 + Int.unsigned lo)). +Proof. + intros. unfold from_words. decEq. + rewrite Int64.shifted_or_is_add. + apply Int64.eqm_samerepr. auto with ints. + change (Z_of_nat Int64.wordsize) with 64. omega. + generalize (Int.unsigned_range lo). intros [A B]. + rewrite Int64.unsigned_repr. assumption. + assert (Int.modulus < Int64.max_unsigned). compute; auto. omega. +Qed. + (** Below are the only properties of floating-point arithmetic that we rely on in the compiler proof. *) diff --git a/lib/Integers.v b/lib/Integers.v index 0dc79979..8dc5b6f5 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -1224,6 +1224,24 @@ Proof. rewrite inj_S in H. omega. rewrite inj_S in H. omega. Qed. +Lemma bits_of_Z_greater: + forall n x i, + 0 <= x < two_p i -> bits_of_Z n x i = false. +Proof. + induction n; intros. + auto. + destruct (zlt i 0). apply bits_of_Z_below. auto. + simpl. + destruct (Z_bin_decomp x) as [b x1]_eqn. + destruct (zeq i 0). + subst i. simpl in H. assert (x = 0) by omega. subst x. simpl in Heqp. congruence. + apply IHn. + rewrite <- (Z_shift_add_bin_decomp x) in H. rewrite Heqp in H. simpl in H. + replace i with (Zsucc (i-1)) in H by omega. rewrite two_p_S in H. + unfold Z_shift_add in H. destruct b; omega. + omega. +Qed. + Lemma bits_of_Z_of_bits_gen': forall n f i j, bits_of_Z n (Z_of_bits n f j) i = @@ -2283,6 +2301,28 @@ Proof. auto. Qed. +Theorem shifted_or_is_add: + forall x y n, + 0 <= n < Z_of_nat wordsize -> + unsigned y < two_p n -> + or (shl x (repr n)) y = repr(unsigned x * two_p n + unsigned y). +Proof. + intros. rewrite <- add_is_or. + rewrite shl_mul_two_p. rewrite unsigned_repr. + unfold add. apply eqm_samerepr. unfold mul. auto with ints. + generalize wordsize_max_unsigned; omega. + unfold and, shl, bitwise_binop. unfold zero. decEq. apply Z_of_bits_false. intros. + rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits_gen. + rewrite unsigned_repr. apply andb_false_iff. + destruct (zlt j n). + left. apply bits_of_Z_below. omega. + right. apply bits_of_Z_greater. + split. generalize (unsigned_range y); omega. + assert (two_p n <= two_p j). apply two_p_monotone. omega. omega. + generalize wordsize_max_unsigned; omega. + omega. +Qed. + (** Unsigned right shifts and unsigned divisions by powers of 2. *) Lemma Z_of_bits_shift_right: -- cgit