From 02015cafba394b4e18c6231204c5838724b31297 Mon Sep 17 00:00:00 2001
From: chaomaer <1506174913@qq.com>
Date: Mon, 25 Mar 2019 17:47:17 +0800
Subject: Update the comment of the free operation (#277)

The comment says "writable" but it should be "freeable".
---
 common/Memtype.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'common')

diff --git a/common/Memtype.v b/common/Memtype.v
index ae4fa5fd..03dc1499 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -104,7 +104,7 @@ Parameter alloc: forall (m: mem) (lo hi: Z), mem * block.
 
 (** [free m b lo hi] frees (deallocates) the range of offsets from [lo]
   included to [hi] excluded in block [b].  Returns the updated memory
-  state, or [None] if the freed addresses are not writable. *)
+  state, or [None] if the freed addresses are not freeable. *)
 Parameter free: forall (m: mem) (b: block) (lo hi: Z), option mem.
 
 (** [load chunk m b ofs] reads a memory quantity [chunk] from
-- 
cgit 


From b66ddea9b0304d390b56afadda80fa4d2f2184d6 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Tue, 23 Apr 2019 14:12:04 +0200
Subject: Replace nat_of_Z with Z.to_nat

Use Z.to_nat theorems from the standard Coq library in preference to
our theorems in lib/Coqlib.v.

Simplify lib/Coqlib.v accordingly.
---
 common/Events.v  |  2 +-
 common/Memdata.v |  2 +-
 common/Memory.v  | 34 +++++++++++++++++-----------------
 common/Memtype.v |  2 +-
 4 files changed, 20 insertions(+), 20 deletions(-)

(limited to 'common')

diff --git a/common/Events.v b/common/Events.v
index b2335b96..26dd505f 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1208,7 +1208,7 @@ Proof.
   assert (RPDST: Mem.range_perm m1 bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sz) Cur Nonempty).
     replace sz with (Z.of_nat (length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
-    rewrite LEN. apply nat_of_Z_eq. omega.
+    rewrite LEN. apply Z2Nat.id. omega.
   assert (PSRC: Mem.perm m1 bsrc (Ptrofs.unsigned osrc) Cur Nonempty).
     apply RPSRC. omega.
   assert (PDST: Mem.perm m1 bdst (Ptrofs.unsigned odst) Cur Nonempty).
diff --git a/common/Memdata.v b/common/Memdata.v
index a9ed48b4..307a02db 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -50,7 +50,7 @@ Proof.
 Qed.
 
 Definition size_chunk_nat (chunk: memory_chunk) : nat :=
-  nat_of_Z(size_chunk chunk).
+  Z.to_nat(size_chunk chunk).
 
 Lemma size_chunk_conv:
   forall chunk, size_chunk chunk = Z.of_nat (size_chunk_nat chunk).
diff --git a/common/Memory.v b/common/Memory.v
index 2cf1c3ab..fed6c1d7 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -460,7 +460,7 @@ Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
 
 Definition loadbytes (m: mem) (b: block) (ofs n: Z): option (list memval) :=
   if range_perm_dec m b ofs (ofs + n) Cur Readable
-  then Some (getN (nat_of_Z n) ofs (m.(mem_contents)#b))
+  then Some (getN (Z.to_nat n) ofs (m.(mem_contents)#b))
   else None.
 
 (** Memory stores. *)
@@ -780,7 +780,7 @@ Qed.
 Theorem loadbytes_length:
   forall m b ofs n bytes,
   loadbytes m b ofs n = Some bytes ->
-  length bytes = nat_of_Z n.
+  length bytes = Z.to_nat n.
 Proof.
   unfold loadbytes; intros.
   destruct (range_perm_dec m b ofs (ofs + n) Cur Readable); try congruence.
@@ -791,7 +791,7 @@ Theorem loadbytes_empty:
   forall m b ofs n,
   n <= 0 -> loadbytes m b ofs n = Some nil.
 Proof.
-  intros. unfold loadbytes. rewrite pred_dec_true. rewrite nat_of_Z_neg; auto.
+  intros. unfold loadbytes. rewrite pred_dec_true. rewrite Z_to_nat_neg; auto.
   red; intros. omegaContradiction.
 Qed.
 
@@ -816,8 +816,8 @@ Proof.
   unfold loadbytes; intros.
   destruct (range_perm_dec m b ofs (ofs + n1) Cur Readable); try congruence.
   destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Cur Readable); try congruence.
-  rewrite pred_dec_true. rewrite nat_of_Z_plus; auto.
-  rewrite getN_concat. rewrite nat_of_Z_eq; auto.
+  rewrite pred_dec_true. rewrite Z2Nat.inj_add by omega.
+  rewrite getN_concat. rewrite Z2Nat.id by omega.
   congruence.
   red; intros.
   assert (ofs0 < ofs + n1 \/ ofs0 >= ofs + n1) by omega.
@@ -836,8 +836,8 @@ Proof.
   unfold loadbytes; intros.
   destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Cur Readable);
   try congruence.
-  rewrite nat_of_Z_plus in H; auto. rewrite getN_concat in H.
-  rewrite nat_of_Z_eq in H; auto.
+  rewrite Z2Nat.inj_add in H by omega. rewrite getN_concat in H.
+  rewrite Z2Nat.id in H by omega.
   repeat rewrite pred_dec_true.
   econstructor; econstructor.
   split. reflexivity. split. reflexivity. congruence.
@@ -1106,7 +1106,7 @@ Proof.
   assert (valid_access m2 chunk b ofs Readable) by eauto with mem.
   unfold loadbytes. rewrite pred_dec_true. rewrite store_mem_contents; simpl.
   rewrite PMap.gss.
-  replace (nat_of_Z (size_chunk chunk)) with (length (encode_val chunk v)).
+  replace (Z.to_nat (size_chunk chunk)) with (length (encode_val chunk v)).
   rewrite getN_setN_same. auto.
   rewrite encode_val_length. auto.
   apply H.
@@ -1127,10 +1127,10 @@ Proof.
   rewrite PMap.gsspec. destruct (peq b' b). subst b'.
   destruct H. congruence.
   destruct (zle n 0) as [z | n0].
-  rewrite (nat_of_Z_neg _ z). auto.
+  rewrite (Z_to_nat_neg _ z). auto.
   destruct H. omegaContradiction.
   apply getN_setN_outside. rewrite encode_val_length. rewrite <- size_chunk_conv.
-  rewrite nat_of_Z_eq. auto. omega.
+  rewrite Z2Nat.id. auto. omega.
   auto.
   red; intros. eauto with mem.
   rewrite pred_dec_false. auto.
@@ -1523,7 +1523,7 @@ Proof.
   destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable);
   try discriminate.
   rewrite pred_dec_true.
-  decEq. inv STORE2; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat.
+  decEq. inv STORE2; simpl. rewrite PMap.gss. rewrite Nat2Z.id.
   apply getN_setN_same.
   red; eauto with mem.
 Qed.
@@ -1539,7 +1539,7 @@ Proof.
   rewrite pred_dec_true.
   rewrite storebytes_mem_contents. decEq.
   rewrite PMap.gsspec. destruct (peq b' b). subst b'.
-  apply getN_setN_disjoint. rewrite nat_of_Z_eq; auto. intuition congruence.
+  apply getN_setN_disjoint. rewrite Z2Nat.id by omega. intuition congruence.
   auto.
   red; auto with mem.
   apply pred_dec_false.
@@ -1867,7 +1867,7 @@ Proof.
   unfold loadbytes; intros. destruct (range_perm_dec m2 b ofs (ofs + n) Cur Readable); inv H.
   revert H0.
   injection ALLOC; intros A B. rewrite <- A; rewrite <- B; simpl. rewrite PMap.gss.
-  generalize (nat_of_Z n) ofs. induction n0; simpl; intros.
+  generalize (Z.to_nat n) ofs. induction n0; simpl; intros.
   contradiction.
   rewrite ZMap.gi in H0. destruct H0; eauto.
 Qed.
@@ -2342,13 +2342,13 @@ Lemma loadbytes_inj:
 Proof.
   intros. unfold loadbytes in *.
   destruct (range_perm_dec m1 b1 ofs (ofs + len) Cur Readable); inv H0.
-  exists (getN (nat_of_Z len) (ofs + delta) (m2.(mem_contents)#b2)).
+  exists (getN (Z.to_nat len) (ofs + delta) (m2.(mem_contents)#b2)).
   split. apply pred_dec_true.
   replace (ofs + delta + len) with ((ofs + len) + delta) by omega.
   eapply range_perm_inj; eauto with mem.
   apply getN_inj; auto.
-  destruct (zle 0 len). rewrite nat_of_Z_eq; auto. omega.
-  rewrite nat_of_Z_neg. simpl. red; intros; omegaContradiction. omega.
+  destruct (zle 0 len). rewrite Z2Nat.id by omega. auto.
+  rewrite Z_to_nat_neg by omega. simpl. red; intros; omegaContradiction.
 Qed.
 
 (** Preservation of stores. *)
@@ -4340,7 +4340,7 @@ Proof.
 + unfold loadbytes. destruct H.
   destruct (range_perm_dec m b ofs (ofs + n) Cur Readable).
   rewrite pred_dec_true. f_equal.
-  apply getN_exten. intros. rewrite nat_of_Z_eq in H by omega.
+  apply getN_exten. intros. rewrite Z2Nat.id in H by omega.
   apply unchanged_on_contents0; auto.
   red; intros. apply unchanged_on_perm0; auto.
   rewrite pred_dec_false. auto.
diff --git a/common/Memtype.v b/common/Memtype.v
index 03dc1499..53775d8b 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -358,7 +358,7 @@ Axiom load_loadbytes:
 Axiom loadbytes_length:
   forall m b ofs n bytes,
   loadbytes m b ofs n = Some bytes ->
-  length bytes = nat_of_Z n.
+  length bytes = Z.to_nat n.
 
 Axiom loadbytes_empty:
   forall m b ofs n,
-- 
cgit 


From 51c497b2e5a2b09788f2cf05f414634b037f52bf Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Tue, 23 Apr 2019 15:00:41 +0200
Subject: lib/Coqlib.v: remove defns about multiplication, division, modulus

Instead, use definitions and lemmas from the Coq standard library
(ZArith, Znumtheory).
---
 common/Memdata.v    |  4 ++--
 common/Memory.v     | 10 +++++-----
 common/Separation.v |  2 +-
 common/Switch.v     |  6 +++---
 4 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'common')

diff --git a/common/Memdata.v b/common/Memdata.v
index 307a02db..c53f0e5d 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -258,14 +258,14 @@ Lemma decode_encode_int_4:
   forall x, Int.repr (decode_int (encode_int 4 (Int.unsigned x))) = x.
 Proof.
   intros. rewrite decode_encode_int. transitivity (Int.repr (Int.unsigned x)).
-  decEq. apply Zmod_small. apply Int.unsigned_range. apply Int.repr_unsigned.
+  decEq. apply Z.mod_small. apply Int.unsigned_range. apply Int.repr_unsigned.
 Qed.
 
 Lemma decode_encode_int_8:
   forall x, Int64.repr (decode_int (encode_int 8 (Int64.unsigned x))) = x.
 Proof.
   intros. rewrite decode_encode_int. transitivity (Int64.repr (Int64.unsigned x)).
-  decEq. apply Zmod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned.
+  decEq. apply Z.mod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned.
 Qed.
 
 (** A length-[n] encoding depends only on the low [8*n] bits of the integer. *)
diff --git a/common/Memory.v b/common/Memory.v
index fed6c1d7..b68a5049 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -284,7 +284,7 @@ Lemma valid_access_dec:
 Proof.
   intros.
   destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur p).
-  destruct (Zdivide_dec (align_chunk chunk) ofs (align_chunk_pos chunk)).
+  destruct (Zdivide_dec (align_chunk chunk) ofs).
   left; constructor; auto.
   right; red; intro V; inv V; contradiction.
   right; red; intro V; inv V; contradiction.
@@ -887,11 +887,11 @@ Proof.
   intros (bytes1 & bytes2 & LB1 & LB2 & APP).
   change 4 with (size_chunk Mint32) in LB1.
   exploit loadbytes_load. eexact LB1.
-  simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
+  simpl. apply Z.divide_trans with 8; auto. exists 2; auto.
   intros L1.
   change 4 with (size_chunk Mint32) in LB2.
   exploit loadbytes_load. eexact LB2.
-  simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
+  simpl. apply Z.divide_add_r. apply Z.divide_trans with 8; auto. exists 2; auto. exists 1; auto.
   intros L2.
   exists (decode_val Mint32 (if Archi.big_endian then bytes1 else bytes2));
   exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)).
@@ -1644,9 +1644,9 @@ Proof.
   rewrite encode_val_length in SB2. simpl in SB2.
   exists m1; split.
   apply storebytes_store. exact SB1.
-  simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
+  simpl. apply Z.divide_trans with 8; auto. exists 2; auto.
   apply storebytes_store. exact SB2.
-  simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
+  simpl. apply Z.divide_add_r. apply Z.divide_trans with 8; auto. exists 2; auto. exists 1; auto.
 Qed.
 
 Theorem storev_int64_split:
diff --git a/common/Separation.v b/common/Separation.v
index a9642d72..1493b535 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -702,7 +702,7 @@ Proof.
 - intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). omega.
 - intros. apply Mem.perm_implies with Freeable; auto with mem.
   eapply Mem.perm_alloc_2; eauto. xomega.
-- red; intros. apply Zdivides_trans with 8; auto.
+- red; intros. apply Z.divide_trans with 8; auto.
   exists (8 / align_chunk chunk). destruct chunk; reflexivity.
 - intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto.
 - intros (j' & INJ' & J1 & J2 & J3).
diff --git a/common/Switch.v b/common/Switch.v
index 0ef91d60..5a6d4c63 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -288,10 +288,10 @@ Lemma validate_jumptable_correct:
 Proof.
   intros.
   rewrite (validate_jumptable_correct_rec cases tbl ofs); auto.
-- f_equal. f_equal. rewrite Zmod_small. omega.
+- f_equal. f_equal. rewrite Z.mod_small. omega.
   destruct (zle ofs v). omega.
   assert (M: ((v - ofs) + 1 * modulus) mod modulus = (v - ofs) + modulus).
-  { rewrite Zmod_small. omega. omega. }
+  { rewrite Z.mod_small. omega. omega. }
   rewrite Z_mod_plus in M by auto. rewrite M in H0. omega.
 - generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega.
 Qed.
@@ -331,7 +331,7 @@ Proof.
   rewrite (split_between_prop v _ _ _ _ _ _ EQ).
   assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; omega).
   destruct (zlt ((v - ofs) mod modulus) sz).
-  rewrite Zmod_small by omega. eapply validate_jumptable_correct; eauto.
+  rewrite Z.mod_small by omega. eapply validate_jumptable_correct; eauto.
   eapply IHt; eauto.
 Qed.
 
-- 
cgit 


From 08fd5faf30c18e17caa610076e67cf002a01d8b4 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
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.
---
 common/Memdata.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'common')

diff --git a/common/Memdata.v b/common/Memdata.v
index c53f0e5d..7144d72c 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -17,6 +17,7 @@
 (** In-memory representation of values. *)
 
 Require Import Coqlib.
+Require Import Zbits.
 Require Archi.
 Require Import AST.
 Require Import Integers.
@@ -272,7 +273,7 @@ Qed.
 
 Lemma bytes_of_int_mod:
   forall n x y,
-  Int.eqmod (two_p (Z.of_nat n * 8)) x y ->
+  eqmod (two_p (Z.of_nat n * 8)) x y ->
   bytes_of_int n x = bytes_of_int n y.
 Proof.
   induction n.
@@ -284,7 +285,7 @@ Proof.
   intro EQM.
   simpl; decEq.
   apply Byte.eqm_samerepr. red.
-  eapply Int.eqmod_divides; eauto. apply Z.divide_factor_r.
+  eapply eqmod_divides; eauto. apply Z.divide_factor_r.
   apply IHn.
   destruct EQM as [k EQ]. exists k. rewrite EQ.
   rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega.
@@ -292,7 +293,7 @@ Qed.
 
 Lemma encode_int_8_mod:
   forall x y,
-  Int.eqmod (two_p 8) x y ->
+  eqmod (two_p 8) x y ->
   encode_int 1%nat x = encode_int 1%nat y.
 Proof.
   intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto.
@@ -300,7 +301,7 @@ Qed.
 
 Lemma encode_int_16_mod:
   forall x y,
-  Int.eqmod (two_p 16) x y ->
+  eqmod (two_p 16) x y ->
   encode_int 2%nat x = encode_int 2%nat y.
 Proof.
   intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto.
-- 
cgit 


From 3830a91a4711c4570394e02e93e4e08db88eac6f Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 12 Apr 2019 17:35:18 +0200
Subject: Support a "select" operation between two values

`Val.select ob v1 v2 ty` is a conditional operation that chooses between
the values `v1` and `v2` depending on the comparison `ob : option bool`.
If `ob` is `None`, `Vundef` is returned.
If the selected value does not match type `ty`, `Vundef` is returned.

This operation will be used to model a "select" (or "conditional move")
operation at the CminorSel/RTL/LTL/Mach level.
---
 common/Values.v | 126 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 126 insertions(+)

(limited to 'common')

diff --git a/common/Values.v b/common/Values.v
index a20dd567..a51a390f 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -132,6 +132,23 @@ Proof.
   simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto.
 Qed.
 
+Definition has_type_dec (v: val) (t: typ) : { has_type v t } + { ~ has_type v t }.
+Proof.
+  unfold has_type; destruct v.
+- auto.
+- destruct t; auto.
+- destruct t; auto.
+- destruct t; auto.
+- destruct t; auto.
+- destruct t. 
+  apply bool_dec.
+  auto.
+  apply bool_dec.
+  auto.
+  apply bool_dec.
+  auto.
+Defined.
+
 (** Truth values.  Non-zero integers are treated as [True].
   The integer 0 (also used to represent the null pointer) is [False].
   Other values are neither true nor false. *)
@@ -898,6 +915,55 @@ Definition offset_ptr (v: val) (delta: ptrofs) : val :=
   | _ => Vundef
   end.
 
+(** Normalize a value to the given type, turning it into Vundef if it does not
+    match the type. *)
+
+Definition normalize (v: val) (ty: typ) : val :=
+  match v, ty with
+  | Vundef, _ => Vundef
+  | Vint _, Tint => v
+  | Vlong _, Tlong => v
+  | Vfloat _, Tfloat => v
+  | Vsingle _, Tsingle => v
+  | Vptr _ _, (Tint | Tany32) => if Archi.ptr64 then Vundef else v
+  | Vptr _ _, Tlong => if Archi.ptr64 then v else Vundef
+  | (Vint _ | Vsingle _), Tany32 => v
+  | _, Tany64 => v
+  | _, _ => Vundef
+  end.
+
+Lemma normalize_type:
+  forall v ty, has_type (normalize v ty) ty.
+Proof.
+  intros; destruct v; simpl.
+- auto.
+- destruct ty; exact I.
+- destruct ty; exact I.
+- destruct ty; exact I.
+- destruct ty; exact I.
+- unfold has_type; destruct ty, Archi.ptr64; auto.
+Qed.
+
+Lemma normalize_idem:
+  forall v ty, has_type v ty -> normalize v ty = v.
+Proof.
+  unfold has_type, normalize; intros. destruct v.
+- auto.
+- destruct ty; intuition auto.
+- destruct ty; intuition auto.
+- destruct ty; intuition auto.
+- destruct ty; intuition auto.
+- destruct ty, Archi.ptr64; intuition congruence.
+Qed.
+
+(** Select between two values based on the result of a comparison. *)
+
+Definition select (cmp: option bool) (v1 v2: val) (ty: typ) :=
+  match cmp with
+  | Some b => normalize (if b then v1 else v2) ty
+  | None => Vundef
+  end.
+
 (** [load_result] reflects the effect of storing a value with a given
   memory chunk, then reading it back with the same chunk.  Depending
   on the chunk and the type of the value, some normalization occurs.
@@ -2044,6 +2110,36 @@ Proof.
   intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc.
 Qed.
 
+Lemma lessdef_normalize:
+  forall v ty, lessdef (normalize v ty) v.
+Proof.
+  intros. destruct v; simpl.
+  - auto.
+  - destruct ty; auto.
+  - destruct ty; auto.
+  - destruct ty; auto.
+  - destruct ty; auto.
+  - destruct ty, Archi.ptr64; auto.
+Qed.
+
+Lemma normalize_lessdef:
+  forall v v' ty, lessdef v v' -> lessdef (normalize v ty) (normalize v' ty).
+Proof.
+  intros. inv H; auto.
+Qed.
+
+Lemma select_lessdef:
+  forall ob ob' v1 v1' v2 v2' ty,
+  ob = None \/ ob = ob' ->
+  lessdef v1 v1' -> lessdef v2 v2' ->
+  lessdef (select ob v1 v2 ty) (select ob' v1' v2' ty).
+Proof.
+  intros; unfold select. destruct H.
+- subst ob; auto.
+- subst ob'; destruct ob as [b|]; auto.
+  apply normalize_lessdef. destruct b; auto.
+Qed.
+
 (** * Values and memory injections *)
 
 (** A memory injection [f] is a function from addresses to either [None]
@@ -2328,6 +2424,36 @@ Proof.
   intros. unfold Val.hiword; inv H; auto.
 Qed.
 
+Lemma normalize_inject:
+  forall v v' ty, inject f v v' -> inject f (normalize v ty) (normalize v' ty).
+Proof.
+  intros. inv H.
+- destruct ty; constructor.
+- destruct ty; constructor.
+- destruct ty; constructor.
+- destruct ty; constructor.
+- simpl. destruct ty.
++ destruct Archi.ptr64; econstructor; eauto.
++ auto.
++ destruct Archi.ptr64; econstructor; eauto.
++ auto.
++ destruct Archi.ptr64; econstructor; eauto.
++ econstructor; eauto.
+- constructor.
+Qed.
+
+Lemma select_inject:
+  forall ob ob' v1 v1' v2 v2' ty,
+  ob = None \/ ob = ob' ->
+  inject f v1 v1' -> inject f v2 v2' ->
+  inject f (select ob v1 v2 ty) (select ob' v1' v2' ty).
+Proof.
+  intros; unfold select. destruct H.
+- subst ob; auto.
+- subst ob'; destruct ob as [b|]; auto.
+  apply normalize_inject. destruct b; auto.
+Qed.
+
 End VAL_INJ_OPS.
 
 End Val.
-- 
cgit 


From 8b0724fdb1af4f89a603f7bde4b5b625c870e111 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 31 May 2019 11:55:57 +0200
Subject: Fix misspellings in messages, man pages, and comments

This is a manual, partial merge of Github pull request #296 by @Fourchaux.
flocq/, cparser/MenhirLib/ and parts of test/ have not been changed
because these are local copies and the fixes should be performed upstream.
---
 common/AST.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'common')

diff --git a/common/AST.v b/common/AST.v
index 145f4919..a91138c9 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -432,12 +432,12 @@ Inductive external_function : Type :=
      (** A function from the run-time library.  Behaves like an
          external, but must not be redefined. *)
   | EF_vload (chunk: memory_chunk)
-     (** A volatile read operation.  If the adress given as first argument
+     (** A volatile read operation.  If the address given as first argument
          points within a volatile global variable, generate an
          event and return the value found in this event.  Otherwise,
          produce no event and behave like a regular memory load. *)
   | EF_vstore (chunk: memory_chunk)
-     (** A volatile store operation.   If the adress given as first argument
+     (** A volatile store operation.   If the address given as first argument
          points within a volatile global variable, generate an event.
          Otherwise, produce no event and behave like a regular memory store. *)
   | EF_malloc
-- 
cgit 


From e10870c3da5b28a76c0c0d283c1a0beb09cd7950 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Fri, 31 May 2019 19:07:47 +0200
Subject: Additional simulation diagrams for determinate source languages

If the source language is determinate, it can take several steps
(not just one) before the "match_state" invariant is reinstated.
---
 common/Smallstep.v | 173 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 173 insertions(+)

(limited to 'common')

diff --git a/common/Smallstep.v b/common/Smallstep.v
index c269013b..27ad0a2d 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -872,6 +872,14 @@ Proof.
   intros. eapply sd_determ; eauto.
 Qed.
 
+Lemma sd_determ_3:
+  forall s t s1 s2,
+  Step L s t s1 -> Step L s E0 s2 -> t = E0 /\ s1 = s2.
+Proof.
+  intros. exploit (sd_determ DET). eexact H. eexact H0.
+  intros [A B]. inv A. auto.
+Qed.
+
 Lemma star_determinacy:
   forall s t s', Star L s t s' ->
   forall s'', Star L s t s'' -> Star L s' E0 s'' \/ Star L s'' E0 s'.
@@ -895,6 +903,171 @@ Qed.
 
 End DETERMINACY.
 
+(** Extra simulation diagrams for determinate languages. *)
+
+Section FORWARD_SIMU_DETERM.
+
+Variable L1: semantics.
+Variable L2: semantics.
+
+Hypothesis L1det: determinate L1.
+
+Variable index: Type.
+Variable order: index -> index -> Prop.
+Hypothesis wf_order: well_founded order.
+
+Variable match_states: index -> state L1 -> state L2 -> Prop.
+
+Hypothesis match_initial_states:
+  forall s1, initial_state L1 s1 ->
+  exists i s2, initial_state L2 s2 /\ match_states i s1 s2.
+
+Hypothesis match_final_states:
+  forall i s1 s2 r,
+  match_states i s1 s2 ->
+  final_state L1 s1 r ->
+  final_state L2 s2 r.
+
+Hypothesis simulation:
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall i s2, match_states i s1 s2 ->
+  exists s1'' i' s2',
+      Star L1 s1' E0 s1''
+   /\ (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ order i' i))
+   /\ match_states i' s1'' s2'.
+
+Hypothesis public_preserved:
+  forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id.
+
+Inductive match_states_later: index * nat -> state L1 -> state L2 -> Prop :=
+| msl_now: forall i s1 s2,
+    match_states i s1 s2 -> match_states_later (i, O) s1 s2
+| msl_later: forall i n s1 s1' s2,
+    Step L1 s1 E0 s1' -> match_states_later (i, n) s1' s2 -> match_states_later (i, S n) s1 s2.
+
+Lemma star_match_states_later:
+  forall s1 s1', Star L1 s1 E0 s1' ->
+  forall i s2, match_states i s1' s2 ->
+  exists n, match_states_later (i, n) s1 s2.
+Proof.
+  intros s10 s10' STAR0. pattern s10, s10'; eapply star_E0_ind; eauto.
+  - intros s1 i s2 M. exists O; constructor; auto.
+  - intros s1 s1' s1'' STEP IH i s2 M.
+    destruct (IH i s2 M) as (n & MS).
+    exists (S n); econstructor; eauto.
+Qed.
+
+Lemma forward_simulation_determ: forward_simulation L1 L2.
+Proof.
+  apply Forward_simulation with (order0 := lex_ord order lt) (match_states0 := match_states_later);
+  constructor.
+- apply wf_lex_ord. apply wf_order. apply lt_wf.
+- intros. exploit match_initial_states; eauto. intros (i & s2 & A & B).
+  exists (i, O), s2; auto using msl_now.
+- intros. inv H.
+  + eapply match_final_states; eauto.
+  + eelim (sd_final_nostep L1det); eauto.
+- intros s1 t s1' A; destruct 1.
+  + exploit simulation; eauto. intros (s1'' & i' & s2' & B & C & D).
+    exploit star_match_states_later; eauto. intros (n & E).
+    exists (i', n), s2'; split; auto.
+    destruct C as [P | [P Q]]; auto using lex_ord_left.
+  + exploit sd_determ_3. eauto. eexact A. eauto. intros [P Q]; subst t s1'0.
+    exists (i, n), s2; split; auto.
+    right; split. apply star_refl. apply lex_ord_right. omega.
+- exact public_preserved.
+Qed.
+
+End FORWARD_SIMU_DETERM.
+
+(** A few useful special cases. *)
+
+Section FORWARD_SIMU_DETERM_DIAGRAMS.
+
+Variable L1: semantics.
+Variable L2: semantics.
+
+Hypothesis L1det: determinate L1.
+
+Variable match_states: state L1 -> state L2 -> Prop.
+
+Hypothesis public_preserved:
+  forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id.
+
+Hypothesis match_initial_states:
+  forall s1, initial_state L1 s1 ->
+  exists s2, initial_state L2 s2 /\ match_states s1 s2.
+
+Hypothesis match_final_states:
+  forall s1 s2 r,
+  match_states s1 s2 ->
+  final_state L1 s1 r ->
+  final_state L2 s2 r.
+
+Section SIMU_DETERM_STAR.
+
+Variable measure: state L1 -> nat.
+
+Hypothesis simulation:
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  exists s1'' s2',
+      Star L1 s1' E0 s1''
+   /\ (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ measure s1'' < measure s1))%nat
+   /\ match_states s1'' s2'.
+
+Lemma forward_simulation_determ_star: forward_simulation L1 L2.
+Proof.
+  apply forward_simulation_determ with
+    (match_states := fun i s1 s2 => i = s1 /\ match_states s1 s2)
+    (order := ltof _ measure).
+- assumption.
+- apply well_founded_ltof.
+- intros. exploit match_initial_states; eauto. intros (s2 & A & B). 
+  exists s1, s2; auto.
+- intros. destruct H. eapply match_final_states; eauto.
+- intros. destruct H0; subst i. 
+  exploit simulation; eauto. intros (s1'' & s2' & A & B & C).
+  exists s1'', s1'', s2'. auto.
+- assumption.
+Qed.
+
+End SIMU_DETERM_STAR.
+
+Section SIMU_DETERM_PLUS.
+
+Hypothesis simulation:
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  exists s1'' s2', Star L1 s1' E0 s1'' /\ Plus L2 s2 t s2' /\ match_states s1'' s2'.
+
+Lemma forward_simulation_determ_plus: forward_simulation L1 L2.
+Proof.
+  apply forward_simulation_determ_star with (measure := fun _ => O).
+  intros. exploit simulation; eauto. intros (s1'' & s2' & A & B & C).
+  exists s1'', s2'; auto.
+Qed.
+
+End SIMU_DETERM_PLUS.
+
+Section SIMU_DETERM_ONE.
+
+Hypothesis simulation:
+  forall s1 t s1', Step L1 s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  exists s1'' s2', Star L1 s1' E0 s1'' /\ Step L2 s2 t s2' /\ match_states s1'' s2'.
+
+Lemma forward_simulation_determ_one: forward_simulation L1 L2.
+Proof.
+  apply forward_simulation_determ_plus.
+  intros. exploit simulation; eauto. intros (s1'' & s2' & A & B & C).
+  exists s1'', s2'; auto using plus_one.
+Qed.
+
+End SIMU_DETERM_ONE.
+
+End FORWARD_SIMU_DETERM_DIAGRAMS.
+
 (** * Backward simulations between two transition semantics. *)
 
 Definition safe (L: semantics) (s: state L) : Prop :=
-- 
cgit