4 files changed, 64 insertions, 7 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index 1c0e41a1..c7332329 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -957,8 +957,12 @@ Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
 
 (** Translation of loads and stores *)
 
-Definition transl_load (chunk: memory_chunk) (addr: Op.addressing)
+Definition transl_load (trap: trapping_mode)
+                       (chunk: memory_chunk) (addr: Op.addressing)
                        (args: list mreg) (dst: mreg) (k: code) : res code :=
+  match trap with
+  | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on aarch64")
+  | TRAP =>
   match chunk with
   | Mint8unsigned =>
       do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrb W rd) k
@@ -980,6 +984,7 @@ Definition transl_load (chunk: memory_chunk) (addr: Op.addressing)
       do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw_a rd) k
   | Many64 =>
       do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx_a rd) k
+  end
   end.
 
 Definition transl_store (chunk: memory_chunk) (addr: Op.addressing)
@@ -1063,8 +1068,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
       OK (if r29_is_parent then c else loadptr XSP f.(fn_link_ofs) X29 c)
   | Mop op args res =>
       transl_op op args res k
-  | Mload chunk addr args dst =>
-      transl_load chunk addr args dst k
+  | Mload trap chunk addr args dst =>
+      transl_load trap chunk addr args dst k
   | Mstore chunk addr args src =>
       transl_store chunk addr args src k
   | Mcall sig (inl r) =>
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index eeff1956..c860b961 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -283,10 +283,10 @@ Proof.
 Qed.
 
 Remark transl_load_label:
-  forall chunk addr args dst k c,
-  transl_load chunk addr args dst k = OK c -> tail_nolabel k c.
+  forall trap chunk addr args dst k c,
+  transl_load trap chunk addr args dst k = OK c -> tail_nolabel k c.
 Proof.
-  unfold transl_load; intros; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto.
+  unfold transl_load; intros; destruct trap; try discriminate; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto.
 Qed.
 
 Remark transl_store_label:
@@ -709,6 +709,8 @@ Local Transparent destroyed_by_op.
   destruct op; try exact I; simpl; congruence.
 
 - (* Mload *)
+  destruct trap.
+  {
   assert (Op.eval_addressing tge sp addr (map rs args) = Some a).
   { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. }
   exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
@@ -719,6 +721,16 @@ Local Transparent destroyed_by_op.
   exists rs2; split. eauto.
   split. eapply agree_set_undef_mreg; eauto. congruence.
   simpl; congruence.
+  }
+  
+  (* Mload notrap1 *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
+- (* Mload notrap *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
+- (* Mload notrap *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
 
 - (* Mstore *)
   assert (Op.eval_addressing tge sp addr (map rs args) = Some a).
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index 663ee50b..245eeb62 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
@@ -1620,7 +1620,7 @@ Qed.
 
 Lemma transl_load_correct:
   forall chunk addr args dst k c (rs: regset) m vaddr v,
-  transl_load chunk addr args dst k = OK c ->
+  transl_load TRAP chunk addr args dst k = OK c ->
   Op.eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some vaddr ->
   Mem.loadv chunk m vaddr = Some v ->
   exists rs',
diff --git a/aarch64/Op.v b/aarch64/Op.v
index a7483d56..bf33ab0d 100644
--- a/aarch64/Op.v
+++ b/aarch64/Op.v
@@ -1576,6 +1576,21 @@ Proof.
 - apply Val.offset_ptr_inject; auto. 
 Qed.
 
+
+Lemma eval_addressing_inj_none:
+  forall addr sp1 vl1 sp2 vl2,
+  (forall id ofs,
+      In id (globals_addressing addr) ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
+  eval_addressing ge1 sp1 addr vl1 = None ->
+  eval_addressing ge2 sp2 addr vl2 = None.
+Proof.
+  intros until vl2. intros Hglobal Hinjsp Hinjvl.
+  destruct addr; simpl in *;
+  inv Hinjvl; trivial; try discriminate; inv H0; trivial; try discriminate; inv H2; trivial; try discriminate.
+Qed.
 End EVAL_COMPAT.
 
 (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *)
@@ -1682,6 +1697,18 @@ Proof.
   destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto.
 Qed.
 
+Lemma eval_addressing_lessdef_none:
+  forall sp addr vl1 vl2,
+  Val.lessdef_list vl1 vl2 ->
+  eval_addressing genv sp addr vl1 = None ->
+  eval_addressing genv sp addr vl2 = None.
+Proof.
+  intros. rewrite val_inject_list_lessdef in H.
+  eapply eval_addressing_inj_none with (sp1 := sp).
+  intros. rewrite <- val_inject_lessdef; auto.
+  rewrite <- val_inject_lessdef; auto.
+  eauto. auto.
+Qed.
 End EVAL_LESSDEF.
 
 (** Compatibility of the evaluation functions with memory injections. *)
@@ -1734,6 +1761,19 @@ Proof.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
 Qed.
 
+Lemma eval_addressing_inject_none:
+  forall addr vl1 vl2,
+  Val.inject_list f vl1 vl2 ->
+  eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = None ->
+  eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = None.
+Proof.
+  intros.
+  rewrite eval_shift_stack_addressing.
+  eapply eval_addressing_inj_none with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
+  intros. apply symbol_address_inject.
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
+Qed.
+
 Lemma eval_operation_inject:
   forall op vl1 vl2 v1 m1 m2,
   Val.inject_list f vl1 vl2 ->