From fcf5b5c840f93d8c8b09ba299ab3962f43f080d3 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 20 Apr 2020 21:43:32 +0200 Subject: new semantics for some trapping operations --- mppa_k1c/Asmblockgenproof1.v | 2 -- mppa_k1c/Asmvliw.v | 20 ++++++++++---------- mppa_k1c/Op.v | 10 +--------- mppa_k1c/SelectLongproof.v | 33 +++++---------------------------- mppa_k1c/SelectOpproof.v | 40 ++++++++++------------------------------ 5 files changed, 26 insertions(+), 79 deletions(-) (limited to 'mppa_k1c') 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. -- cgit