Adding buitin_args lemmas

There was an issue with the register PC in the eval_BA constructor for builtin : we were not able to prove that the concerned reg was different from PC.
This commit modify the definitions in Asmgen and Asmblock to support this, by replacing the parameter with a dreg instead of a preg.

1 files changed, 60 insertions, 19 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index b2671972..1d13fa7e 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1859,6 +1859,60 @@ Proof.
   exploit list_nth_z_range; eauto; omega.
 Qed.
 
+Lemma pc_ptr_exec_step: forall ofs bb b rs m _rs _m
+  (ATPC : rs PC = Vptr b ofs)
+  (MATCHI : match_internal (size bb - 1)
+            {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |}
+            {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}),
+  _rs PC = Vptr b (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))).
+Proof.
+  intros; inv MATCHI. rewrite <- AGPC; rewrite ATPC; unfold Val.offset_ptr; eauto.
+Qed.
+
+Lemma find_instr_ofs_somei: forall ofs bb f tc asmi rs m _rs _m
+  (BOUNDOFS : Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned)
+  (FIND_INSTR : Asm.find_instr (Ptrofs.unsigned ofs + (size bb - 1)) tc =
+                Some (asmi))
+  (MATCHI : match_internal (size bb - 1)
+            {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |}
+            {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}),
+  Asm.find_instr (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))))
+    (Asm.fn_code {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}) =
+  Some (asmi).
+Proof.
+  intros; simpl.
+  replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))))
+          with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption.
+  generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros.
+  unfold Ptrofs.add.
+  rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega.
+  rewrite Ptrofs.unsigned_repr; omega.
+Qed.
+
+Lemma eval_builtin_arg_match: forall rs _m _rs a1 b1
+  (AG : forall r : preg, r <> PC -> rs r = _rs r)
+  (EVAL : eval_builtin_arg tge (fun r : dreg => rs r) (rs SP) _m a1 b1),
+  eval_builtin_arg tge _rs (_rs SP) _m (map_builtin_arg DR a1) b1.
+Proof.
+  intros; induction EVAL; simpl in *; try rewrite AG; try rewrite AG in EVAL; try discriminate; try congruence; eauto with barg.
+  econstructor. rewrite <- AG; try discriminate; auto.
+Qed.
+
+Lemma eval_builtin_args_match: forall bb rs m _rs _m args vargs
+  (MATCHI : match_internal (size bb - 1)
+            {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |}
+            {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |})
+  (EVAL : eval_builtin_args tge (fun r : dreg => rs r) (rs SP) m args vargs),
+  eval_builtin_args tge _rs (_rs SP) _m (map (map_builtin_arg DR) args) vargs.
+Proof.
+  intros; inv MATCHI.
+  induction EVAL; subst.
+  - econstructor.
+  - econstructor.
+    + eapply eval_builtin_arg_match; eauto.
+    + eauto.
+Qed.
+
 Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
   (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
@@ -1899,18 +1953,11 @@ Proof.
       intros (tf & FINDtf' & TRANSf). inversion FINDtf'; subst; clear FINDtf'.
       exploit exec_cfi_simulation; eauto.
       (* extract exec_cfi_simulation's conclusion as separate hypotheses *)
-      (* TODO: ligne ci-dessous à remplacer avec un intro (rs2' & m2' & ...) *)
-      intro H3; destruct H3; destruct H3; destruct H3. rewrite H5.
-      inversion MATCHI.
+      intros (rs2' & m2' & EXECI & MATCHS); rewrite MATCHS.
       apply plus_one.
       eapply Asm.exec_step_internal; eauto.
-      - rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. eauto.
-      - simpl. replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))))
-                  with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption.
-        generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros.
-        unfold Ptrofs.add.
-        rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega.
-        rewrite Ptrofs.unsigned_repr; omega.
+      - eapply pc_ptr_exec_step; eauto.
+      - eapply find_instr_ofs_somei; eauto.
     * (* builtin *)
       destruct s2.
       rewrite H in EXIT.
@@ -1921,15 +1968,9 @@ Proof.
       eapply external_call_symbols_preserved in H10; try (apply senv_preserved).
       eapply eval_builtin_args_preserved in H6; try (apply symbols_preserved).
       eapply Asm.exec_step_builtin; eauto.
-      - inv MATCHI. rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. eauto.
-      - (* XXX copy-paste from case above *)
-        simpl. replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))))
-                  with (Ptrofs.unsigned ofs + (size bb - 1)); eauto.
-        generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros.
-        unfold Ptrofs.add.
-        rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega.
-        rewrite Ptrofs.unsigned_repr; omega.
-      - simpl. (* TODO something like eval_builtin_args_match *) admit.
+      - eapply pc_ptr_exec_step; eauto.
+      - eapply find_instr_ofs_somei; eauto.
+      - eapply eval_builtin_args_match; eauto.
       - inv MATCHI; eauto.
       - rewrite H11. (* TODO lemmas for set_res, undef_regs ... *) admit.
 Admitted.