diff options
| -rw-r--r-- | backend/CSE2.v | 6 | ||||
| -rw-r--r-- | backend/CSE2proof.v | 5 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 20 | ||||
| -rw-r--r-- | mppa_k1c/ConstpropOpproof.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 118 | ||||
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 33 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 40 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 314 | ||||
| -rw-r--r-- | runtime/Makefile | 1 | ||||
| -rw-r--r-- | test/c/Results/mandelbrot-mppa_k1c | bin | 409 -> 209 bytes |
11 files changed, 393 insertions, 152 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index 8e2307b0..00b1821e 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -276,10 +276,10 @@ Definition apply_external_call ef (rel : RELATION.t) : RELATION.t := | Some bf => rel | None => kill_mem rel end - | EF_malloc (* FIXME *) + | EF_malloc (* would need lessdef *) | EF_external _ _ | EF_vstore _ - | EF_free (* FIXME *) + | EF_free (* would need lessdef? *) | EF_memcpy _ _ (* FIXME *) | EF_inline_asm _ _ _ => kill_mem rel | _ => rel @@ -363,7 +363,7 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) | Some src => Iop Omove (src::nil) dst s end | Istore chunk addr args src s => - Istore chunk addr (subst_args fmap pc args) src s + Istore chunk addr (subst_args fmap pc args) (subst_arg fmap pc src) s | Icall sig ros args dst s => Icall sig ros (subst_args fmap pc args) dst s | Itailcall sig ros args => diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 9e0ad909..f9c7b400 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1527,7 +1527,10 @@ Proof. assert (eval_addressing tge sp addr rs ## args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Istore; eauto. - rewrite (subst_args_ok' sp m); assumption. + - rewrite (subst_args_ok' sp m) by assumption. + eassumption. + - rewrite (subst_arg_ok' sp m) by assumption. + eassumption. } constructor; auto. 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/ConstpropOpproof.v b/mppa_k1c/ConstpropOpproof.v index ae11a220..4dd0441d 100644 --- a/mppa_k1c/ConstpropOpproof.v +++ b/mppa_k1c/ConstpropOpproof.v @@ -276,7 +276,8 @@ Proof. inv H; auto. destruct (Int.is_power2 n) eqn:?. destruct (Int.ltu i (Int.repr 31)) eqn:?. - exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. + exists v; split; auto. simpl. + erewrite Val.divs_pow2; eauto. reflexivity. congruence. exists v; auto. exists v; auto. Qed. @@ -449,7 +450,8 @@ Lemma make_divlimm_correct: Proof. intros; unfold make_divlimm. destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?. - rewrite H0 in H. econstructor; split. simpl; eauto. eapply Val.divls_pow2; eauto. auto. + rewrite H0 in H. econstructor; split. simpl; eauto. + erewrite Val.divls_pow2; eauto. auto. exists v; auto. exists v; auto. Qed. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 92061d04..4e874ca8 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -374,7 +374,7 @@ Definition eval_operation | Ororimm n, v1 :: nil => Some (Val.ror v1 (Vint n)) | Oshru, v1 :: v2 :: nil => Some (Val.shru v1 v2) | Oshruimm n, v1 :: nil => Some (Val.shru v1 (Vint n)) - | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) + | Oshrximm n, v1::nil => Some (Val.maketotal (Val.shrx v1 (Vint n))) | Omadd, v1::v2::v3::nil => Some (Val.add v1 (Val.mul v2 v3)) | (Omaddimm n), v1::v2::nil => Some (Val.add v1 (Val.mul v2 (Vint n))) | Omsub, v1::v2::v3::nil => Some (Val.sub v1 (Val.mul v2 v3)) @@ -424,7 +424,7 @@ Definition eval_operation | Oshrlimm n, v1::nil => Some (Val.shrl v1 (Vint n)) | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2) | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n)) - | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n) + | Oshrxlimm n, v1::nil => Some (Val.maketotal (Val.shrxl v1 (Vint n))) | Omaddl, v1::v2::v3::nil => Some (Val.addl v1 (Val.mull v2 v3)) | (Omaddlimm n), v1::v2::nil => Some (Val.addl v1 (Val.mull v2 (Vlong n))) | Omsubl, v1::v2::v3::nil => Some (Val.subl v1 (Val.mull v2 v3)) @@ -454,20 +454,20 @@ Definition eval_operation | Osingleoffloat, v1::nil => Some (Val.singleoffloat v1) | Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1) - | Ointoffloat, v1::nil => Val.intoffloat v1 - | Ointuoffloat, v1::nil => Val.intuoffloat v1 - | Ointofsingle, v1::nil => Val.intofsingle v1 - | Ointuofsingle, v1::nil => Val.intuofsingle v1 - | Osingleofint, v1::nil => Val.singleofint v1 - | Osingleofintu, v1::nil => Val.singleofintu v1 - | Olongoffloat, v1::nil => Val.longoffloat v1 - | Olonguoffloat, v1::nil => Val.longuoffloat v1 - | Ofloatoflong, v1::nil => Val.floatoflong v1 - | Ofloatoflongu, v1::nil => Val.floatoflongu v1 - | Olongofsingle, v1::nil => Val.longofsingle v1 - | Olonguofsingle, v1::nil => Val.longuofsingle v1 - | Osingleoflong, v1::nil => Val.singleoflong v1 - | Osingleoflongu, v1::nil => Val.singleoflongu v1 + | Ointoffloat, v1::nil => Some (Val.maketotal (Val.intoffloat v1)) + | Ointuoffloat, v1::nil => Some (Val.maketotal (Val.intuoffloat v1)) + | Ointofsingle, v1::nil => Some (Val.maketotal (Val.intofsingle v1)) + | Ointuofsingle, v1::nil => Some (Val.maketotal (Val.intuofsingle v1)) + | Osingleofint, v1::nil => Some (Val.maketotal (Val.singleofint v1)) + | Osingleofintu, v1::nil => Some (Val.maketotal (Val.singleofintu v1)) + | Olongoffloat, v1::nil => Some (Val.maketotal (Val.longoffloat v1)) + | Olonguoffloat, v1::nil => Some (Val.maketotal (Val.longuoffloat v1)) + | Ofloatoflong, v1::nil => Some (Val.maketotal (Val.floatoflong v1)) + | Ofloatoflongu, v1::nil => Some (Val.maketotal (Val.floatoflongu v1)) + | Olongofsingle, v1::nil => Some (Val.maketotal (Val.longofsingle v1)) + | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1)) + | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1)) + | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1)) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) | (Oextfz stop start), v0::nil => Some (extfz stop start v0) | (Oextfs stop start), v0::nil => Some (extfs stop start v0) @@ -840,7 +840,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)... (* shrx *) - - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 31)); inv H0... + - destruct v0; simpl... destruct (Int.ltu n (Int.repr 31)); simpl; trivial. (* shrimm *) - destruct v0; simpl... (* madd *) @@ -920,7 +920,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... (* shrxl *) - - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0... + - destruct v0; simpl... destruct (Int.ltu n (Int.repr 63)); simpl; trivial. (* maddl, maddlim *) - apply type_addl. - apply type_addl. @@ -962,26 +962,26 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0... - destruct v0... (* intoffloat, intuoffloat *) - - destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2... - - destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2... + - destruct v0; simpl... destruct (Float.to_int f); simpl; trivial. + - destruct v0; simpl... destruct (Float.to_intu f); simpl; trivial. (* intofsingle, intuofsingle *) - - destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); inv H2... - - destruct v0; simpl in H0; inv H0. destruct (Float32.to_intu f); inv H2... + - destruct v0; simpl... destruct (Float32.to_int f); simpl; trivial. + - destruct v0; simpl... destruct (Float32.to_intu f); simpl; trivial. (* singleofint, singleofintu *) - - destruct v0; simpl in H0; inv H0... - - destruct v0; simpl in H0; inv H0... + - destruct v0; simpl... + - destruct v0; simpl... (* longoffloat, longuoffloat *) - - destruct v0; simpl in H0; inv H0. destruct (Float.to_long f); inv H2... - - destruct v0; simpl in H0; inv H0. destruct (Float.to_longu f); inv H2... + - destruct v0; simpl... destruct (Float.to_long f); simpl; trivial. + - destruct v0; simpl... destruct (Float.to_longu f); simpl; trivial. (* floatoflong, floatoflongu *) - - destruct v0; simpl in H0; inv H0... - - destruct v0; simpl in H0; inv H0... + - destruct v0; simpl... + - destruct v0; simpl... (* longofsingle, longuofsingle *) - - destruct v0; simpl in H0; inv H0. destruct (Float32.to_long f); inv H2... - - destruct v0; simpl in H0; inv H0. destruct (Float32.to_longu f); inv H2... + - destruct v0; simpl... destruct (Float32.to_long f); simpl; trivial. + - destruct v0; simpl... destruct (Float32.to_longu f); simpl; trivial. (* singleoflong, singleoflongu *) - - destruct v0; simpl in H0; inv H0... - - destruct v0; simpl in H0; inv H0... + - destruct v0; simpl... + - destruct v0; simpl... (* cmp *) - destruct (eval_condition cond vl m)... destruct b... (* extfz *) @@ -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. @@ -1477,8 +1469,8 @@ Proof. - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. (* shrx *) - - inv H4; simpl in H1; try discriminate. simpl. - destruct (Int.ltu n (Int.repr 31)); inv H1. TrivialExists. + - inv H4; simpl; auto. + destruct (Int.ltu n (Int.repr 31)); inv H; simpl; auto. (* rorimm *) - inv H4; simpl; auto. (* madd, maddim *) @@ -1567,8 +1559,8 @@ Proof. - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. (* shrx *) - - inv H4; simpl in H1; try discriminate. simpl. - destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists. + - inv H4; simpl; auto. + destruct (Int.ltu n (Int.repr 63)); simpl; auto. (* maddl, maddlimm *) - apply Val.addl_inject; auto. @@ -1615,34 +1607,26 @@ Proof. - inv H4; simpl; auto. - inv H4; simpl; auto. (* intoffloat, intuoffloat *) - - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2. - exists (Vint i); auto. - - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2. - exists (Vint i); auto. + - inv H4; simpl; auto. destruct (Float.to_int f0); simpl; auto. + - inv H4; simpl; auto. destruct (Float.to_intu f0); simpl; auto. (* intofsingle, intuofsingle *) - - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2. - exists (Vint i); auto. - - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_intu f0); simpl in H2; inv H2. - exists (Vint i); auto. + - inv H4; simpl; auto. destruct (Float32.to_int f0); simpl; auto. + - inv H4; simpl; auto. destruct (Float32.to_intu f0); simpl; auto. (* singleofint, singleofintu *) - - inv H4; simpl in H1; inv H1. simpl. TrivialExists. - - inv H4; simpl in H1; inv H1. simpl. TrivialExists. + - inv H4; simpl; auto. + - inv H4; simpl; auto. (* longoffloat, longuoffloat *) - - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_long f0); simpl in H2; inv H2. - exists (Vlong i); auto. - - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_longu f0); simpl in H2; inv H2. - exists (Vlong i); auto. + - inv H4; simpl; auto. destruct (Float.to_long f0); simpl; auto. + - inv H4; simpl; auto. destruct (Float.to_longu f0); simpl; auto. (* floatoflong, floatoflongu *) - - inv H4; simpl in H1; inv H1. simpl. TrivialExists. - - inv H4; simpl in H1; inv H1. simpl. TrivialExists. + - inv H4; simpl; auto. + - inv H4; simpl; auto. (* longofsingle, longuofsingle *) - - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_long f0); simpl in H2; inv H2. - exists (Vlong i); auto. - - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_longu f0); simpl in H2; inv H2. - exists (Vlong i); auto. + - inv H4; simpl; auto. destruct (Float32.to_long f0); simpl; auto. + - inv H4; simpl; auto. destruct (Float32.to_longu f0); simpl; auto. (* singleoflong, singleoflongu *) - - inv H4; simpl in H1; inv H1. simpl. TrivialExists. - - inv H4; simpl in H1; inv H1. simpl. TrivialExists. + - inv H4; simpl; auto. + - inv H4; simpl; auto. (* cmp *) - subst v1. destruct (eval_condition cond vl1 m1) eqn:?. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. 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. diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 7d84447e..901908b5 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -14,6 +14,86 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op ExtValues ExtFloats RTL ValueDomain. +Definition intoffloat_total (x: aval) := + match x with + | F f => + match Float.to_int f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition intuoffloat_total (x: aval) := + match x with + | F f => + match Float.to_intu f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition intofsingle_total (x: aval) := + match x with + | FS f => + match Float32.to_int f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition intuofsingle_total (x: aval) := + match x with + | FS f => + match Float32.to_intu f with + | Some i => I i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longoffloat_total (x: aval) := + match x with + | F f => + match Float.to_long f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longuoffloat_total (x: aval) := + match x with + | F f => + match Float.to_longu f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longofsingle_total (x: aval) := + match x with + | FS f => + match Float32.to_long f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + +Definition longuofsingle_total (x: aval) := + match x with + | FS f => + match Float32.to_longu f with + | Some i => L i + | None => ntop + end + | _ => ntop1 x + end. + Definition minf := binop_float ExtFloat.min. Definition maxf := binop_float ExtFloat.max. Definition minfs := binop_single ExtFloat32.min. @@ -282,18 +362,18 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ofmsubfs, v1::v2::v3::nil => fmsubfs v1 v2 v3 | Osingleoffloat, v1::nil => singleoffloat v1 | Ofloatofsingle, v1::nil => floatofsingle v1 - | Ointoffloat, v1::nil => intoffloat v1 - | Ointuoffloat, v1::nil => intuoffloat v1 - | Ointofsingle, v1::nil => intofsingle v1 - | Ointuofsingle, v1::nil => intuofsingle v1 + | Ointoffloat, v1::nil => intoffloat_total v1 + | Ointuoffloat, v1::nil => intuoffloat_total v1 + | Ointofsingle, v1::nil => intofsingle_total v1 + | Ointuofsingle, v1::nil => intuofsingle_total v1 | Osingleofint, v1::nil => singleofint v1 | Osingleofintu, v1::nil => singleofintu v1 - | Olongoffloat, v1::nil => longoffloat v1 - | Olonguoffloat, v1::nil => longuoffloat v1 + | Olongoffloat, v1::nil => longoffloat_total v1 + | Olonguoffloat, v1::nil => longuoffloat_total v1 | Ofloatoflong, v1::nil => floatoflong v1 | Ofloatoflongu, v1::nil => floatoflongu v1 - | Olongofsingle, v1::nil => longofsingle v1 - | Olonguofsingle, v1::nil => longuofsingle v1 + | Olongofsingle, v1::nil => longofsingle_total v1 + | Olonguofsingle, v1::nil => longuofsingle_total v1 | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) @@ -317,6 +397,196 @@ Hypothesis GENV: genv_match bc ge. Variable sp: block. Hypothesis STACK: bc sp = BCstack. +Lemma intoffloat_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.intoffloat v)) (intoffloat_total x). +Proof. + unfold Val.intoffloat, intoffloat_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve intoffloat_total_sound : va. + +Lemma intuoffloat_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.intuoffloat v)) (intuoffloat_total x). +Proof. + unfold Val.intoffloat, intoffloat_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve intuoffloat_total_sound : va. + +Lemma intofsingle_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.intofsingle v)) (intofsingle_total x). +Proof. + unfold Val.intofsingle, intofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_int f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve intofsingle_total_sound : va. + +Lemma intuofsingle_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.intuofsingle v)) (intuofsingle_total x). +Proof. + unfold Val.intofsingle, intofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_intu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve intuofsingle_total_sound : va. + +Lemma singleofint_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.singleofint v)) (singleofint x). +Proof. + unfold Val.singleofint, singleofint; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve singleofint_total_sound : va. + +Lemma singleofintu_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.singleofintu v)) (singleofintu x). +Proof. + unfold Val.singleofintu, singleofintu; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve singleofintu_total_sound : va. + +Lemma longoffloat_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.longoffloat v)) (longoffloat_total x). +Proof. + unfold Val.longoffloat, longoffloat_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve longoffloat_total_sound : va. + +Lemma longuoffloat_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.longuoffloat v)) (longuoffloat_total x). +Proof. + unfold Val.longoffloat, longoffloat_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve longuoffloat_total_sound : va. + +Lemma longofsingle_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.longofsingle v)) (longofsingle_total x). +Proof. + unfold Val.longofsingle, longofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_long f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve longofsingle_total_sound : va. + +Lemma longuofsingle_total_sound: + forall v x + (MATCH : vmatch bc v x), + vmatch bc (Val.maketotal (Val.longuofsingle v)) (longuofsingle_total x). +Proof. + unfold Val.longofsingle, longofsingle_total. intros. + inv MATCH; simpl in *; try constructor. + all: destruct (Float32.to_longu f) as [i|] eqn:E; simpl; [auto with va | constructor]. + unfold ntop1, provenance. + destruct (va_strict tt); constructor. +Qed. + +Hint Resolve longuofsingle_total_sound : va. + +Lemma singleoflong_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.singleoflong v)) (singleoflong x). +Proof. + unfold Val.singleoflong, singleoflong; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve singleoflong_total_sound : va. + +Lemma singleoflongu_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.singleoflongu v)) (singleoflongu x). +Proof. + unfold Val.singleoflongu, singleoflongu; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve singleoflongu_total_sound : va. + +Lemma floatoflong_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.floatoflong v)) (floatoflong x). +Proof. + unfold Val.floatoflong, floatoflong; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve floatoflong_total_sound : va. + +Lemma floatoflongu_total_sound: + forall v x, vmatch bc v x -> + vmatch bc (Val.maketotal (Val.floatoflongu v)) (floatoflongu x). +Proof. + unfold Val.floatoflongu, floatoflongu; intros. + inv H; simpl. + all: auto with va. + all: unfold ntop1, provenance. + all: try constructor. +Qed. + +Hint Resolve floatoflongu_total_sound : va. + Lemma minf_sound: forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y). Proof. @@ -490,6 +760,26 @@ Proof. destruct addr; trivial; discriminate. Qed. +Lemma vmatch_vint_ntop1: + forall x y, vmatch bc (Vint x) (ntop1 y). +Proof. + intro. unfold ntop1, provenance. + destruct y; + destruct (va_strict tt); + constructor. +Qed. + +Lemma vmatch_vlong_ntop1: + forall x y, vmatch bc (Vlong x) (ntop1 y). +Proof. + intro. unfold ntop1, provenance. + destruct y; + destruct (va_strict tt); + constructor. +Qed. + +Hint Resolve vmatch_vint_ntop1 vmatch_vlong_ntop1: va. + Theorem eval_static_operation_sound: forall op vargs m vres aargs, eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres -> @@ -518,6 +808,10 @@ Proof. end) with (Val.sub (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))). + eauto with va. + destruct n; destruct shift; reflexivity. + - (* shrx *) + inv H1; simpl; try constructor. + all: destruct Int.ltu; [simpl | constructor; fail]. + all: auto with va. - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with | Vlong n2 => Vlong (Int64.add n n2) | Vptr b2 ofs2 => @@ -535,6 +829,10 @@ Proof. end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))). + eauto with va. + destruct a1; destruct shift; reflexivity. + - (* shrxl *) + inv H1; simpl; try constructor. + all: destruct Int.ltu; [simpl | constructor; fail]. + all: auto with va. - apply of_optbool_sound. eapply eval_static_condition_sound; eauto. (* extfz *) diff --git a/runtime/Makefile b/runtime/Makefile index 3b1cabc4..e3f008a9 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -26,7 +26,6 @@ else ifeq ($(ARCH),mppa_k1c) OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o vararg.o\ i64_dtos.o i64_dtou.o i64_utod.o i64_utof.o i64_stod.o i64_stof.o\ i64_shl.o i64_shr.o -# Missing: i64_utod.o i64_utof.o i64_stod.o i64_stof.o DOMAKE:=$(shell (cd mppa_k1c && make)) else ifeq ($(ARCH),aarch64) OBJS=vararg.o diff --git a/test/c/Results/mandelbrot-mppa_k1c b/test/c/Results/mandelbrot-mppa_k1c Binary files differindex f50961fe..55c5683a 100644 --- a/test/c/Results/mandelbrot-mppa_k1c +++ b/test/c/Results/mandelbrot-mppa_k1c |