new semantics for some trapping operations

5 files changed, 26 insertions, 79 deletions

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 00df01e3..9c836037 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1535,7 +1535,6 @@ Opaque Int.eq.
   + apply exec_straight_one. simpl. eauto.
   + repeat split.
     * rewrite Pregmap.gss.
-      subst v.
       destruct (rs x0); simpl; trivial.
       unfold Val.maketotal.
       destruct (Int.ltu _ _); simpl; trivial.
@@ -1546,7 +1545,6 @@ Opaque Int.eq.
   + apply exec_straight_one. simpl. eauto.
   + repeat split.
     * rewrite Pregmap.gss.
-      subst v.
       destruct (rs x0); simpl; trivial.
       unfold Val.maketotal.
       destruct (Int.ltu _ _); simpl; trivial.
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 946007c1..819120a0 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -988,16 +988,16 @@ Definition arith_eval_rr n v :=
   | Pfinvw => ExtValues.invfs v
   | Pfnarrowdw => Val.singleoffloat v
   | Pfwidenlwd => Val.floatofsingle v
-  | Pfloatwrnsz => match Val.singleofint v with Some f => f | _ => Vundef end
-  | Pfloatuwrnsz => match Val.singleofintu v with Some f => f | _ => Vundef end
-  | Pfloatudrnsz => match Val.floatoflongu v with Some f => f | _ => Vundef end
-  | Pfloatdrnsz => match Val.floatoflong v with Some f => f | _ => Vundef end
-  | Pfixedwrzz => match Val.intofsingle v with Some i => i | _ => Vundef end
-  | Pfixeduwrzz => match Val.intuofsingle v with Some i => i | _ => Vundef end
-  | Pfixeddrzz => match Val.longoffloat v with Some i => i | _ => Vundef end
-  | Pfixedudrzz => match Val.longuoffloat v with Some i => i | _ => Vundef end
-  | Pfixeddrzz_i32 => match Val.intoffloat v with Some i => i | _ => Vundef end
-  | Pfixedudrzz_i32 => match Val.intuoffloat v with Some i => i | _ => Vundef end
+  | Pfloatwrnsz => Val.maketotal (Val.singleofint v)
+  | Pfloatuwrnsz => Val.maketotal (Val.singleofintu v)
+  | Pfloatudrnsz => Val.maketotal (Val.floatoflongu v)
+  | Pfloatdrnsz => Val.maketotal (Val.floatoflong v)
+  | Pfixedwrzz => Val.maketotal (Val.intofsingle v)
+  | Pfixeduwrzz => Val.maketotal (Val.intuofsingle v)
+  | Pfixeddrzz => Val.maketotal (Val.longoffloat v)
+  | Pfixedudrzz => Val.maketotal (Val.longuoffloat v)
+  | Pfixeddrzz_i32 => Val.maketotal (Val.intoffloat v)
+  | Pfixedudrzz_i32 => Val.maketotal (Val.intuoffloat v)
   end.
 
 Definition arith_eval_ri32 n i :=
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 57c49ef2..4e874ca8 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -1033,15 +1033,7 @@ Qed.
 Definition is_trapping_op (op : operation) :=
   match op with
   | Odiv | Odivl | Odivu | Odivlu
-  | Omod | Omodl | Omodu | Omodlu
-  | Oshrximm _ | Oshrxlimm _
-  | Ointoffloat | Ointuoffloat
-  | Ointofsingle | Ointuofsingle
-  | Olongoffloat | Olonguoffloat
-  | Olongofsingle | Olonguofsingle
-  | Osingleofint | Osingleofintu
-  | Osingleoflong | Osingleoflongu
-  | Ofloatoflong | Ofloatoflongu => true
+  | Omod | Omodl | Omodu | Omodlu => true
   | _ => false
   end.
 
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index ada02585..5e4f3ed6 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -838,34 +838,7 @@ Proof.
 + predSpec Int.eq Int.eq_spec n Int.zero.
 - subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto.
   change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto.
-- TrivialExists.
-(*
-  intros. unfold shrxlimm. destruct Archi.splitlong eqn:SL.
-+ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32.
-+ destruct x; simpl in H0; try discriminate. 
-  destruct (Int.ltu n (Int.repr 63)) eqn:LTU; inv H0.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  - subst n. exists (Vlong i); split; auto. rewrite Int64.shrx'_zero. auto.
-  - assert (NZ: Int.unsigned n <> 0).
-    { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
-    assert (LT: 0 <= Int.unsigned n < 63) by (apply Int.ltu_inv in LTU; assumption).
-    assert (LTU2: Int.ltu (Int.sub Int64.iwordsize' n) Int64.iwordsize' = true).
-    { unfold Int.ltu; apply zlt_true.
-      unfold Int.sub. change (Int.unsigned Int64.iwordsize') with 64. 
-      rewrite Int.unsigned_repr. omega. 
-      assert (64 < Int.max_unsigned) by reflexivity. omega. }
-    assert (X: eval_expr ge sp e m le
-               (Eop (Oshrlimm (Int.repr (Int64.zwordsize - 1))) (a ::: Enil))
-               (Vlong (Int64.shr' i (Int.repr (Int64.zwordsize - 1))))).
-    { EvalOp. }
-    assert (Y: eval_expr ge sp e m le (shrxlimm_inner a n)
-               (Vlong (Int64.shru' (Int64.shr' i (Int.repr (Int64.zwordsize - 1))) (Int.sub Int64.iwordsize' n)))).
-    { EvalOp. simpl. rewrite LTU2. auto. }
-    TrivialExists. 
-    constructor. EvalOp. simpl; eauto. constructor. 
-    simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int64.shrx'_shr_2 by auto. reflexivity. 
-    change (Int.unsigned Int64.iwordsize') with 64; omega.
-*)
+- TrivialExists. simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_cmplu:
@@ -915,6 +888,7 @@ Proof.
   unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_longoffloat; eauto.
   TrivialExists.
+  simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat.
@@ -922,6 +896,7 @@ Proof.
   unfold longuoffloat; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_longuoffloat; eauto.
   TrivialExists.
+  simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong.
@@ -929,6 +904,7 @@ Proof.
   unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_floatoflong; eauto.
   TrivialExists.
+  simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu.
@@ -936,6 +912,7 @@ Proof.
   unfold floatoflongu; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_floatoflongu; eauto.
   TrivialExists.
+  simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index d3eb1dde..23d2d5b7 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -990,34 +990,8 @@ Proof.
   replace (Int.shrx i Int.zero) with i. auto.
   unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
   change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
-  econstructor; split. EvalOp. auto.
-(*
-  intros. destruct x; simpl in H0; try discriminate. 
-  destruct (Int.ltu n (Int.repr 31)) eqn:LTU; inv H0.
-  unfold shrximm.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  - subst n. exists (Vint i); split; auto.
-    unfold Int.shrx, Int.divs. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto.
-  - assert (NZ: Int.unsigned n <> 0).
-    { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
-    assert (LT: 0 <= Int.unsigned n < 31) by (apply Int.ltu_inv in LTU; assumption).
-    assert (LTU2: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true).
-    { unfold Int.ltu; apply zlt_true.
-      unfold Int.sub. change (Int.unsigned Int.iwordsize) with 32. 
-      rewrite Int.unsigned_repr. omega. 
-      assert (32 < Int.max_unsigned) by reflexivity. omega. }
-    assert (X: eval_expr ge sp e m le
-               (Eop (Oshrimm (Int.repr (Int.zwordsize - 1))) (a ::: Enil))
-               (Vint (Int.shr i (Int.repr (Int.zwordsize - 1))))).
-    { EvalOp. }
-    assert (Y: eval_expr ge sp e m le (shrximm_inner a n)
-               (Vint (Int.shru (Int.shr i (Int.repr (Int.zwordsize - 1))) (Int.sub Int.iwordsize n)))).
-    { EvalOp. simpl. rewrite LTU2. auto. }
-    TrivialExists. 
-    constructor. EvalOp. simpl; eauto. constructor. 
-    simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int.shrx_shr_2 by auto. reflexivity. 
-    change (Int.unsigned Int.iwordsize) with 32; omega.
-*)
+  econstructor; split. EvalOp.
+  simpl. rewrite H0. simpl. reflexivity. auto.
 Qed.
 
 Theorem eval_shl: binary_constructor_sound shl Val.shl.
@@ -1228,6 +1202,7 @@ Theorem eval_intoffloat:
   exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold intoffloat. TrivialExists.
+  simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_intuoffloat:
@@ -1237,6 +1212,7 @@ Theorem eval_intuoffloat:
   exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold intuoffloat. TrivialExists.
+  simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_floatofintu:
@@ -1256,7 +1232,7 @@ Proof.
     constructor. econstructor. constructor. eassumption. constructor.
     simpl. f_equal. constructor.
     simpl.
-    destruct x; simpl; trivial.
+    destruct x; simpl; trivial; try discriminate.
     f_equal.
     inv H0.
     f_equal.
@@ -1280,7 +1256,7 @@ Proof.
     constructor. econstructor. constructor. eassumption. constructor.
     simpl. f_equal. constructor.
     simpl.
-    destruct x; simpl; trivial.
+    destruct x; simpl; trivial; try discriminate.
     f_equal.
     inv H0.
     f_equal.
@@ -1295,6 +1271,7 @@ Theorem eval_intofsingle:
   exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold intofsingle. TrivialExists.
+  simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_singleofint:
@@ -1304,6 +1281,7 @@ Theorem eval_singleofint:
   exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold singleofint; TrivialExists.
+  simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_intuofsingle:
@@ -1313,6 +1291,7 @@ Theorem eval_intuofsingle:
   exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold intuofsingle. TrivialExists.
+  simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_singleofintu:
@@ -1322,6 +1301,7 @@ Theorem eval_singleofintu:
   exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold intuofsingle. TrivialExists.
+  simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.