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

5 files changed, 97 insertions, 28 deletions

diff --git a/.depend b/.depend
index df0d874..8e69f1b 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 c63dc66..f07154c 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 0c19673..abd28ac 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 e7a7aa0..edb6d6b 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 0dc7997..8dc5b6f 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: