more for passing notrap through x86

5 files changed, 56 insertions, 10 deletions

diff --git a/x86/Asmgen.v b/x86/Asmgen.v
index 73e3263e..99e9fc2b 100644
--- a/x86/Asmgen.v
+++ b/x86/Asmgen.v
@@ -636,9 +636,14 @@ Definition transl_op
 
 (** Translation of memory loads and stores *)
 
-Definition transl_load (chunk: memory_chunk)
+Definition transl_load
+           (trap : trapping_mode)
+           (chunk: memory_chunk)
                        (addr: addressing) (args: list mreg) (dest: mreg)
                        (k: code) : res code :=
+  match trap with
+  | NOTRAP => Error (msg "Asmgen.transl_load x86 does not support non trapping loads")
+  | TRAP =>
   do am <- transl_addressing addr args;
   match chunk with
   | Mint8unsigned =>
@@ -659,6 +664,7 @@ Definition transl_load (chunk: memory_chunk)
       do r <- freg_of dest; OK(Pmovsd_fm r am :: k)
   | _ =>
       Error (msg "Asmgen.transl_load")
+  end
   end.
 
 Definition transl_store (chunk: memory_chunk)
@@ -699,8 +705,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
          loadind RSP f.(fn_link_ofs) Tptr AX k1)
   | 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 reg) =>
diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v
index f1fd41e3..6886b2fd 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -235,11 +235,11 @@ Proof.
 Qed.
 
 Remark transl_load_label:
-  forall chunk addr args dest k c,
-  transl_load chunk addr args dest k = OK c ->
+  forall trap chunk addr args dest k c,
+  transl_load trap chunk addr args dest k = OK c ->
   tail_nolabel k c.
 Proof.
-  intros. monadInv H. destruct chunk; TailNoLabel.
+  intros. destruct trap; try discriminate. monadInv H. destruct chunk; TailNoLabel.
 Qed.
 
 Remark transl_store_label:
@@ -567,6 +567,12 @@ Opaque loadind.
   split. eapply agree_set_undef_mreg; eauto. congruence.
   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 rs##args = Some a).
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v
index fd88954e..7cff1047 100644
--- a/x86/Asmgenproof1.v
+++ b/x86/Asmgenproof1.v
@@ -1464,8 +1464,8 @@ Qed.
 (** Translation of memory loads. *)
 
 Lemma transl_load_correct:
-  forall chunk addr args dest k c (rs: regset) m a v,
-  transl_load chunk addr args dest k = OK c ->
+  forall trap chunk addr args dest k c (rs: regset) m a v,
+  transl_load trap chunk addr args dest k = OK c ->
   eval_addressing ge (rs#RSP) addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
   exists rs',
@@ -1473,7 +1473,9 @@ Lemma transl_load_correct:
   /\ rs'#(preg_of dest) = v
   /\ forall r, data_preg r = true -> r <> preg_of dest -> rs'#r = rs#r.
 Proof.
-  unfold transl_load; intros. monadInv H.
+  unfold transl_load; intros.
+  destruct trap; simpl; try discriminate.
+  monadInv H.
   exploit transl_addressing_mode_correct; eauto. intro EA.
   assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto.
   set (rs2 := nextinstr_nf (rs#(preg_of dest) <- v)).
diff --git a/x86/Op.v b/x86/Op.v
index a1000a51..a7176ce4 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -1505,6 +1505,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 ->
diff --git a/x86/ValueAOp.v b/x86/ValueAOp.v
index d0b8427a..e5584b6a 100644
--- a/x86/ValueAOp.v
+++ b/x86/ValueAOp.v
@@ -261,6 +261,25 @@ Proof.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
   apply select_sound; auto. eapply eval_static_condition_sound; eauto.
 Qed.
-
+(*
+Theorem eval_static_addressing_sound_none:
+  forall addr vargs aargs,
+  eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = None ->
+  list_forall2 (vmatch bc) vargs aargs ->
+  (eval_static_addressing addr aargs) = Vbot.
+Proof.
+  unfold eval_addressing, eval_static_addressing.
+  intros until aargs. intros Heval_none Hlist.
+  destruct (Archi.ptr64).
+  inv Hlist.
+  destruct addr; trivial; discriminate.
+  inv H0.
+  destruct addr; trivial; try discriminate. simpl in *.
+  inv H2.
+  destruct addr; trivial; discriminate.
+  inv H3;
+  destruct addr; trivial; discriminate.
+Qed.
+*)
 End SOUNDNESS.