fix for Risc-V

4 files changed, 34 insertions, 8 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index a704ed74..ecaca7b3 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -770,9 +770,13 @@ Definition transl_memory_access
       Error(msg "Asmgen.transl_memory_access")
   end.
 
-Definition transl_load (chunk: memory_chunk) (addr: addressing)
+Definition transl_load (trap : trapping_mode)
+           (chunk: memory_chunk) (addr: addressing)
            (args: list mreg) (dst: mreg) (k: code) :=
-  match chunk with
+  match trap with
+  | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm")
+  | TRAP =>
+    match chunk with
   | Mint8signed =>
       do r <- ireg_of dst;
       transl_memory_access (Plb r)  addr args k
@@ -799,6 +803,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
       transl_memory_access (Pfld r) addr args k
   | _ =>
       Error (msg "Asmgen.transl_load")
+    end
   end.
 
 Definition transl_store (chunk: memory_chunk) (addr: addressing)
@@ -848,8 +853,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
                 else loadind_ptr SP f.(fn_link_ofs) X30 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/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 5ec57886..e2fafb16 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -359,7 +359,7 @@ Proof.
 - destruct ep. eapply loadind_label; eauto.
   eapply tail_nolabel_trans. apply loadind_ptr_label. eapply loadind_label; eauto. 
 - eapply transl_op_label; eauto.
-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
+- destruct t; (try discriminate); destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
 - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
 - destruct s0; monadInv H; TailNoLabel.
 - destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]).
@@ -725,6 +725,12 @@ Local Transparent destroyed_by_op.
   intros; auto with asmgen.
   simpl; congruence.
 
+- (* Mload notrap *) (* isn't there a nicer way? *)
+  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 (eval_addressing tge sp addr (map rs args) = Some a).
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 98d5bd33..175e484f 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -1318,8 +1318,8 @@ Proof.
 Qed.
 
 Lemma transl_load_correct:
-  forall chunk addr args dst k c (rs: regset) m a v,
-  transl_load chunk addr args dst k = OK c ->
+  forall trap chunk addr args dst k c (rs: regset) m a v,
+  transl_load trap chunk addr args dst k = OK c ->
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
   exists rs',
@@ -1327,7 +1327,8 @@ Lemma transl_load_correct:
   /\ rs'#(preg_of dst) = v
   /\ forall r, r <> PC -> r <> X31 -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros until v; intros TR EV LOAD. 
+  intros until v; intros TR EV LOAD.
+  destruct trap; try (simpl in *; discriminate).
   assert (A: exists mk_instr,
       transl_memory_access mk_instr addr args k = OK c
    /\ forall base ofs rs,
diff --git a/riscV/Op.v b/riscV/Op.v
index 73d3f543..97bc301a 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -1343,6 +1343,20 @@ 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 ->