First go at showing that translated cfi behave the same

Import Axioms in order to use functional extensionality

1 files changed, 191 insertions, 0 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 10586f0e..29c746ba 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -20,6 +20,7 @@ Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock.
 Require Machblockgenproof Asmblockgenproof.
 Require Import Asmgen.
+Require Import Axioms.
 
 
 Module Asmblock_PRESERVATION.
@@ -206,6 +207,196 @@ Proof.
       * rewrite <- functions_bound_max_pos; eauto; omega.
 Qed.
 
+Lemma incrPC_agree_but_pc:
+  forall rs r ofs,
+  r <> PC ->
+  (incrPC ofs rs)#r = rs#r.
+Proof.
+  intros rs r ofs NOTPC.
+  unfold incrPC; unfold Pregmap.set; destruct (PregEq.eq r PC).
+  - contradiction.
+  - 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. (* XXX auto-generated names *)
+  destruct cfi.
+  - (* Pb *)
+    simpl; eexists; eexists; split.
+    + inv H0. simpl in H3. rewrite <- H3.
+      unfold incrPC, Asm.goto_label, goto_label.
+      inv H1. 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.
+    + inv H0. simpl in H3. rewrite <- H3.
+      admit.
+    + constructor.
+  - (* Pbl *)
+    simpl; eexists; eexists; split.
+    + inv H0. simpl in H3. rewrite <- H3.
+      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 H1. 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 H1. rewrite AG; auto.
+      } rewrite EQRS. inv H1. reflexivity.
+    + constructor.
+  - (* Pbs *)
+    simpl; eexists; eexists; split.
+    + inv H0. simpl in H3. rewrite <- H3.
+      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 H1; rewrite AG; auto.
+      } rewrite EQRS; inv H1; auto.
+    + constructor.
+  - (* Pblr *)
+    simpl; eexists; eexists; split.
+    + inv H0. simpl in H3. rewrite <- H3.
+      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 H1; rewrite AG; auto. discriminate.
+        - destruct (PregEq.eq x X30) as [X' | X'].
+          + inv H1. 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 H1; rewrite AG; auto.
+      } rewrite EQRS. inv H1; auto.
+    + constructor.
+  - (* Pbr *)
+    simpl; eexists; eexists; split.
+    + inv H0. simpl in H3. rewrite <- H3.
+      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 H1; rewrite AG; try discriminate. reflexivity.
+        - inv H1; rewrite AG; auto.
+      } rewrite EQRS; inv H1; auto.
+    + constructor.
+  - (* Pret *)
+    simpl; eexists; eexists; split.
+    + inv H0. simpl in H3.
+      rewrite <- H3. 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 H1; rewrite AG; try discriminate. reflexivity.
+        - inv H1; rewrite AG; auto.
+      } rewrite EQRS; inv H1; auto.
+    + constructor.
+  - (* Pcbnz *)
+    simpl; eexists; eexists; split.
+    + inv H0. simpl in H3. rewrite <- H3.
+      unfold eval_neg_branch. destruct sz.
+      * simpl. inv H1. 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.
+    + inv H0. simpl in H3. rewrite <- H3.
+      unfold eval_branch. (* TODO, will be very similar to Pcbnz *) admit.
+    + constructor.
+  - (* Pcbz *)
+    simpl; eexists; eexists; split.
+    + inv H0. simpl in H3. rewrite <- H3.
+      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 H1; rewrite AG; try discriminate; auto.
+      } (* TODO, cf. Pcbnz *) admit.
+    + constructor.
+  - (* Ptbz *)
+    simpl; eexists; eexists; split.
+    + inv H0. simpl in H3. rewrite <- H3.
+      (* TODO, cf. Pcbz *) admit.
+    + constructor.
+  - (* Pbtbl *)
+    simpl; eexists; eexists; split.
+    + inv H0. simpl in H3. rewrite <- H3.
+      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 H1; rewrite AG; auto.
+      } rewrite <- EQUNDEFX16.
+      (* TODO Asm.goto_label and goto_label *) admit.
+    + constructor.
+Admitted.
+
 Lemma step_simulation s1 t s1':
   Asmblock.step lk ge s1 t s1' ->
   forall s2, match_states s1 s2 ->