Rename/repurpose cf_instruction_simulated for exec_cfi_simulation

exec_cfi_simulation's rephrasing is inspired by the needs of
exec_exit_simulation_plus.

1 files changed, 150 insertions, 179 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 4b18e712..1412a3a4 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -287,185 +287,6 @@ Proof.
   - reflexivity.
 Qed.
 
-Lemma cf_instruction_simulated:
-  forall size_b f tf rs1 m1 rs1' m1' cfi,
-  (* there are no emnpty basic blocks *)
-  size_b >= 1 ->
-  exec_exit ge f (Ptrofs.repr size_b) rs1 m1 (Some (PCtlFlow cfi)) E0 rs1' m1' ->
-  forall rs2 m2, match_internal (size_b - 1) (State rs1 m1) (State rs2 m2) ->
-  exists rs2' m2', Asm.exec_instr tge tf (cf_instruction_to_instruction cfi)
-                                  rs2 m2 = Next rs2' m2'
-                   /\ match_states (State rs1' m1') (State rs2' m2').
-Proof.
-  intros size_b f tf rs1 m1 rs1' m1' cfi SIZE_B_GE_1 STEP rs2 m2 MI.
-  destruct cfi; inv STEP; simpl in H0.
-  - (* Pb *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0;
-      unfold incrPC, Asm.goto_label, goto_label;
-      inv MI; rewrite <- AGPC.
-      (* TODO: show that Asm.label_pos and label_pos behave the same *
-       *       show that both Val.offset_ptr calculation return Vptr _ _ *)
-      admit.
-    + constructor.
-  - (* Pbc *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      (* TODO see Pb *)
-      admit.
-    + constructor.
-  - (* Pbl *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      rewrite symbol_addresses_preserved.
-      unfold incrPC.
-      assert ( Val.offset_ptr (rs2 PC) Ptrofs.one
-             = Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)
-             ) as EQPC. {
-        inv MI. rewrite <- AGPC.
-        rewrite Val.offset_ptr_assoc.
-        unfold Ptrofs.one.
-        rewrite Ptrofs.add_unsigned.
-        rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr.
-        rewrite Z.sub_add; reflexivity.
-        * split; try omega. apply one_le_max_unsigned.
-        * split; try omega.
-          (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit.
-      } rewrite EQPC.
-      rewrite Pregmap.gss.
-      assert (  (rs2 # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
-                     # PC <-  (Genv.symbol_address ge id Ptrofs.zero)
-             = ((rs1 # PC  <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
-                     # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
-                     # PC  <- (Genv.symbol_address ge id Ptrofs.zero)
-             ) as EQRS. {
-        unfold Pregmap.set.
-        apply functional_extensionality.
-        intros x. destruct (PregEq.eq x X30) as [X | X].
-        - rewrite X. reflexivity.
-        - destruct (PregEq.eq x PC) as [X' | X']; auto.
-        inv MI. rewrite AG; auto.
-      } rewrite EQRS. inv MI. reflexivity.
-    + constructor.
-  - (* Pbs *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      rewrite symbol_addresses_preserved.
-      unfold incrPC.
-      assert ( (rs2 # PC <- (Genv.symbol_address ge id Ptrofs.zero))
-             = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
-                    # PC <- (Genv.symbol_address ge id Ptrofs.zero)
-             ) as EQRS. {
-        unfold Pregmap.set; apply functional_extensionality. intros x.
-        destruct (PregEq.eq x PC) as [X | X]; auto.
-        inv MI; rewrite AG; auto.
-      } rewrite EQRS; inv MI; auto.
-    + constructor.
-  - (* Pblr *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold incrPC. rewrite Pregmap.gss. rewrite Pregmap.gso; try discriminate.
-      assert ( (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one)) # PC <- (rs2 r)
-             = ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
-                     # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
-                     # PC <- (rs1 r)
-             ) as EQRS. {
-        unfold Pregmap.set. apply functional_extensionality.
-        intros x; destruct (PregEq.eq x PC) as [X | X].
-        - inv MI; rewrite AG; auto. discriminate.
-        - destruct (PregEq.eq x X30) as [X' | X'].
-          + inv MI. rewrite <- AGPC.
-            rewrite Val.offset_ptr_assoc. unfold Ptrofs.one.
-            rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr.
-            rewrite Z.sub_add; reflexivity.
-            * split; try omega. apply one_le_max_unsigned.
-            * split; try omega.
-              (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit.
-          + inv MI; rewrite AG; auto.
-      } rewrite EQRS. inv MI; auto.
-    + constructor.
-  - (* Pbr *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold incrPC. rewrite Pregmap.gso; try discriminate.
-      assert (  rs2 # PC <- (rs2 r)
-             = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
-                    # PC <- (rs1 r)
-             ) as EQRS. {
-        unfold Pregmap.set; apply functional_extensionality.
-        intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate.
-        - inv MI; rewrite AG; try discriminate. reflexivity.
-        - inv MI; rewrite AG; auto.
-      } rewrite EQRS; inv MI; auto.
-    + constructor.
-  - (* Pret *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold incrPC. rewrite Pregmap.gso; try discriminate.
-      assert (  rs2 # PC <- (rs2 r)
-             = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) # PC <- (rs1 r)
-             ) as EQRS. {
-        unfold Pregmap.set; apply functional_extensionality.
-        intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate.
-        - inv MI; rewrite AG; try discriminate. reflexivity.
-        - inv MI; rewrite AG; auto.
-      } rewrite EQRS; inv MI; auto.
-    + constructor.
-  - (* Pcbnz *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold eval_neg_branch. destruct sz.
-      * simpl. inv MI. rewrite <- AG; try discriminate.
-        replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs1 r). 2: {
-          symmetry. rewrite incrPC_agree_but_pc; try discriminate; auto.
-        }
-        assert (Asm.nextinstr rs2 = (incrPC (Ptrofs.repr size_b) rs1)) as EQTrue. {
-          unfold incrPC, Asm.nextinstr, Ptrofs.one. rewrite <- AGPC.
-          rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned.
-          rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr.
-          - rewrite Z.sub_add; unfold Pregmap.set; apply functional_extensionality.
-            intros x; destruct (PregEq.eq x PC) as [ X | X ]; auto. rewrite AG; trivial.
-          - split; try omega. apply one_le_max_unsigned.
-          - split; try omega.
-            (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit.
-        } rewrite EQTrue. fold Stuck.
-          (* TODO show that Asm.goto_label and goto_label behave the same *) admit.
-      * (* TODO see/merge above case *) admit.
-    + constructor.
-  - (* Pcbz *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold eval_branch. (* TODO, will be very similar to Pcbnz *) admit.
-    + constructor.
-  - (* Pcbz *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      unfold eval_branch.
-      replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs2 r). 2: {
-          symmetry; rewrite incrPC_agree_but_pc; try discriminate; auto;
-          inv MI; rewrite AG; try discriminate; auto.
-      } (* TODO, cf. Pcbnz *) admit.
-    + constructor.
-  - (* Ptbz *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      (* TODO, cf. Pcbz *) admit.
-    + constructor.
-  - (* Pbtbl *)
-    simpl; eexists; eexists; split.
-    + rewrite <- H0.
-      assert (  rs2 # X16 <- Vundef r1
-             = (incrPC (Ptrofs.repr size_b) rs1) # X16 <- Vundef r1
-             ) as EQUNDEFX16. {
-        unfold incrPC, Pregmap.set.
-        destruct (PregEq.eq r1 X16) as [X16 | X16]; auto.
-        destruct (PregEq.eq r1 PC) as [PC' | PC']; try discriminate.
-        inv MI; rewrite AG; auto.
-      } rewrite <- EQUNDEFX16.
-      (* TODO Asm.goto_label and goto_label *) admit.
-    + constructor.
-Admitted.
-
 Lemma bblock_non_empty bb: body bb <> nil \/ exit bb <> None.
 Proof.
   destruct bb. simpl.
@@ -769,6 +590,156 @@ Proof.
   exploit list_nth_z_range; eauto. omega.
 Qed.
 
+Lemma exec_cfi_simulation:
+  forall bb f tf rs1 m1 rs1' m1' rs2 m2 cfi
+  (SIZE: size bb <= Ptrofs.max_unsigned)
+  (* Warning: Asmblock's PC is assumed to be already pointing on the next instruction ! *)
+  (CFI: exec_cfi ge f cfi (incrPC (Ptrofs.repr (size bb)) rs1) m1 = Next rs1' m1')
+  (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)),
+  exists rs2' m2', Asm.exec_instr tge tf (cf_instruction_to_instruction cfi)
+                                  rs2 m2 = Next rs2' m2'
+                   /\ match_states (State rs1' m1') (State rs2' m2').
+Proof.
+  intros.
+  destruct cfi; inv CFI; simpl.
+  - (* Pb *) admit.
+  - (* Pbc *) admit.
+  - (* Pbl *)
+    eexists; eexists; split.
+    + eauto.
+    + assert ( ((incrPC (Ptrofs.repr (size bb)) rs1) # X30 <- (incrPC (Ptrofs.repr (size bb)) rs1 PC))
+                                                     # PC <-  (Genv.symbol_address ge id Ptrofs.zero)
+             = (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one))
+                             # PC <- (Genv.symbol_address tge id Ptrofs.zero)
+             ) as EQRS. {
+        unfold incrPC. unfold Pregmap.set. simpl. apply functional_extensionality.
+        intros x. destruct (PregEq.eq x PC).
+        * rewrite symbol_addresses_preserved. reflexivity.
+        * destruct (PregEq.eq x X30).
+          -- inv MATCHI. rewrite <- AGPC. rewrite Val.offset_ptr_assoc.
+             unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr).
+             ++ replace (size bb - 1 + 1) with (size bb) by omega. reflexivity.
+             ++ split; try omega. apply one_le_max_unsigned.
+             ++ generalize (bblock_size_pos bb); omega.
+          -- inv MATCHI; rewrite AG; try assumption; reflexivity.
+      } rewrite EQRS; inv MATCHI; reflexivity.
+  - (* Pbs *)
+    eexists; eexists; split.
+    + eauto.
+    + assert ( (incrPC (Ptrofs.repr (size bb)) rs1) # PC <-
+                             (Genv.symbol_address ge id Ptrofs.zero)
+             = rs2 # PC <- (Genv.symbol_address tge id Ptrofs.zero)
+             ) as EQRS. {
+        unfold incrPC, Pregmap.set. rewrite symbol_addresses_preserved. inv MATCHI.
+        apply functional_extensionality. intros x. destruct (PregEq.eq x PC); auto.
+      } rewrite EQRS; inv MATCHI; reflexivity.
+(*
+  - (* Pblr *)
+    simpl; eexists; eexists; split.
+    + rewrite <- H0.
+      unfold incrPC. rewrite Pregmap.gss. rewrite Pregmap.gso; try discriminate.
+      assert ( (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one)) # PC <- (rs2 r)
+             = ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
+                     # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
+                     # PC <- (rs1 r)
+             ) as EQRS. {
+        unfold Pregmap.set. apply functional_extensionality.
+        intros x; destruct (PregEq.eq x PC) as [X | X].
+        - inv MI; rewrite AG; auto. discriminate.
+        - destruct (PregEq.eq x X30) as [X' | X'].
+          + inv MI. rewrite <- AGPC.
+            rewrite Val.offset_ptr_assoc. unfold Ptrofs.one.
+            rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr.
+            rewrite Z.sub_add; reflexivity.
+            * split; try omega. apply one_le_max_unsigned.
+            * split; try omega.
+              (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit.
+          + inv MI; rewrite AG; auto.
+      } rewrite EQRS. inv MI; auto.
+    + constructor.
+  - (* Pbr *)
+    simpl; eexists; eexists; split.
+    + rewrite <- H0.
+      unfold incrPC. rewrite Pregmap.gso; try discriminate.
+      assert (  rs2 # PC <- (rs2 r)
+             = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
+                    # PC <- (rs1 r)
+             ) as EQRS. {
+        unfold Pregmap.set; apply functional_extensionality.
+        intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate.
+        - inv MI; rewrite AG; try discriminate. reflexivity.
+        - inv MI; rewrite AG; auto.
+      } rewrite EQRS; inv MI; auto.
+    + constructor.
+  - (* Pret *)
+    simpl; eexists; eexists; split.
+    + rewrite <- H0.
+      unfold incrPC. rewrite Pregmap.gso; try discriminate.
+      assert (  rs2 # PC <- (rs2 r)
+             = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) # PC <- (rs1 r)
+             ) as EQRS. {
+        unfold Pregmap.set; apply functional_extensionality.
+        intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate.
+        - inv MI; rewrite AG; try discriminate. reflexivity.
+        - inv MI; rewrite AG; auto.
+      } rewrite EQRS; inv MI; auto.
+    + constructor.
+  - (* Pcbnz *)
+    simpl; eexists; eexists; split.
+    + rewrite <- H0.
+      unfold eval_neg_branch. destruct sz.
+      * simpl. inv MI. rewrite <- AG; try discriminate.
+        replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs1 r). 2: {
+          symmetry. rewrite incrPC_agree_but_pc; try discriminate; auto.
+        }
+        assert (Asm.nextinstr rs2 = (incrPC (Ptrofs.repr size_b) rs1)) as EQTrue. {
+          unfold incrPC, Asm.nextinstr, Ptrofs.one. rewrite <- AGPC.
+          rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned.
+          rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr.
+          - rewrite Z.sub_add; unfold Pregmap.set; apply functional_extensionality.
+            intros x; destruct (PregEq.eq x PC) as [ X | X ]; auto. rewrite AG; trivial.
+          - split; try omega. apply one_le_max_unsigned.
+          - split; try omega.
+            (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit.
+        } rewrite EQTrue. fold Stuck.
+          (* TODO show that Asm.goto_label and goto_label behave the same *) admit.
+      * (* TODO see/merge above case *) admit.
+    + constructor.
+  - (* Pcbz *)
+    simpl; eexists; eexists; split.
+    + rewrite <- H0.
+      unfold eval_branch. (* TODO, will be very similar to Pcbnz *) admit.
+    + constructor.
+  - (* Pcbz *)
+    simpl; eexists; eexists; split.
+    + rewrite <- H0.
+      unfold eval_branch.
+      replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs2 r). 2: {
+          symmetry; rewrite incrPC_agree_but_pc; try discriminate; auto;
+          inv MI; rewrite AG; try discriminate; auto.
+      } (* TODO, cf. Pcbnz *) admit.
+    + constructor.
+  - (* Ptbz *)
+    simpl; eexists; eexists; split.
+    + rewrite <- H0.
+      (* TODO, cf. Pcbz *) admit.
+    + constructor.
+  - (* Pbtbl *)
+    simpl; eexists; eexists; split.
+    + rewrite <- H0.
+      assert (  rs2 # X16 <- Vundef r1
+             = (incrPC (Ptrofs.repr size_b) rs1) # X16 <- Vundef r1
+             ) as EQUNDEFX16. {
+        unfold incrPC, Pregmap.set.
+        destruct (PregEq.eq r1 X16) as [X16 | X16]; auto.
+        destruct (PregEq.eq r1 PC) as [PC' | PC']; try discriminate.
+        inv MI; rewrite AG; auto.
+      } rewrite <- EQUNDEFX16.
+      (* TODO Asm.goto_label and goto_label *) admit.
+    + constructor.
+*)
+Admitted.
+
 Lemma last_instruction_cannot_be_label bb:
   list_nth_z (header bb) (size bb - 1) = None.
 Proof.