diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-07 17:36:31 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-07 17:36:31 +0100 |
commit | 747b4e21c1d31a0d8a1d273ab159f9fd87822a1e (patch) | |
tree | 87892061f8da2212f8612977f1bb902bc11b1519 /mppa_k1c | |
parent | a90988739214a8d9ffcaffea3f0bbc3367c01915 (diff) | |
download | compcert-kvx-747b4e21c1d31a0d8a1d273ab159f9fd87822a1e.tar.gz compcert-kvx-747b4e21c1d31a0d8a1d273ab159f9fd87822a1e.zip |
MBop proved
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 32 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof0.v | 8 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 192 |
3 files changed, 128 insertions, 104 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index d6074848..e049ac58 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -1298,7 +1298,8 @@ Proof. all: rewrite <- C; try discriminate; unfold nextblock; Simpl. }
intros. discriminate.
+ (* MBjumptable *)
- destruct TODO.
+ destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
+ inv TBC. inv TIC.
+ (* MBreturn *)
destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
inv TBC. inv TIC. inv H0.
@@ -1506,7 +1507,34 @@ Proof. simpl; intros. rewrite U; auto with asmgen.
apply preg_of_not_FP; auto.
- (* MBop *)
- destruct TODO.
+ simpl in EQ0. rewrite Hheader in DXP.
+
+ assert (eval_operation tge sp op (map ms args) m' = Some v).
+ rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
+ exploit eval_operation_lessdef.
+ eapply preg_vals; eauto.
+ 2: eexact H0.
+ all: eauto.
+ intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A.
+ exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].
+
+ eapply exec_straight_body in P.
+ 2: eapply code_to_basics_id; eauto.
+ destruct P as (l & ll & TBC & CTB & EXECB).
+ exists rs2, m1, ll.
+ eexists. eexists. split. instantiate (1 := x). eauto.
+ repeat (split; auto).
+ eapply basics_to_code_app; eauto.
+ remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
+(* assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
+ rewrite <- Hheadereq. *) subst.
+ eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.
+ apply agree_set_undef_mreg with rs1; auto.
+ apply Val.lessdef_trans with v'; auto.
+ simpl; intros. destruct (andb_prop _ _ H1); clear H1.
+ rewrite R; auto. apply preg_of_not_FP; auto.
+Local Transparent destroyed_by_op.
+ destruct op; simpl; auto; congruence.
- (* MBload *)
destruct TODO.
- (* MBstore *)
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index 6a71a746..0c5055d3 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -287,7 +287,7 @@ Proof. Qed. *) -(* Lemma agree_set_undef_mreg: +Lemma agree_set_undef_mreg: forall ms sp rs r v rl rs', agree ms sp rs -> Val.lessdef v (rs'#(preg_of r)) -> @@ -300,7 +300,6 @@ Proof. congruence. auto. intros. rewrite Pregmap.gso; auto. Qed. - *) Lemma agree_change_sp: forall ms sp rs sp', @@ -865,8 +864,6 @@ Lemma exec_straight_two: forall i1 i2 c rs1 m1 rs2 m2 rs3 m3, exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 -> exec_basic_instr ge i2 rs2 m2 = Next rs3 m3 -> - rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one -> - rs3#PC = Val.offset_ptr rs2#PC Ptrofs.one -> exec_straight (i1 ::g i2 ::g c) rs1 m1 c rs3 m3. Proof. intros. apply exec_straight_step with rs2 m2; auto. @@ -878,9 +875,6 @@ Lemma exec_straight_three: exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 -> exec_basic_instr ge i2 rs2 m2 = Next rs3 m3 -> exec_basic_instr ge i3 rs3 m3 = Next rs4 m4 -> - rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one -> - rs3#PC = Val.offset_ptr rs2#PC Ptrofs.one -> - rs4#PC = Val.offset_ptr rs3#PC Ptrofs.one -> exec_straight (i1 ::g i2 ::g i3 ::g c) rs1 m1 c rs4 m4. Proof. intros. apply exec_straight_step with rs2 m2; auto. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 4269a153..3858571f 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -220,20 +220,23 @@ Proof. intros; Simpl. Qed. *) +*) + +Definition yolo := 4. Lemma opimm64_correct: forall (op: arith_name_rrr) (opi: arith_name_rri64) (sem: val -> val -> val) m, (forall d s1 s2 rs, - exec_instr ge fn (op d s1 s2) rs m = Next (nextinstr (rs#d <- (sem rs###s1 rs###s2))) m) -> + exec_basic_instr ge (op d s1 s2) rs m = Next ((rs#d <- (sem rs#s1 rs#s2))) m) -> (forall d s n rs, - exec_instr ge fn (opi d s n) rs m = Next (nextinstr (rs#d <- (sem rs###s (Vlong n)))) m) -> + exec_basic_instr ge (opi d s n) rs m = Next ((rs#d <- (sem rs#s (Vlong n)))) m) -> forall rd r1 n k rs, r1 <> GPR31 -> exists rs', - exec_straight ge fn (opimm64 op opi rd r1 n k) rs m k rs' m - /\ rs'#rd = sem rs##r1 (Vlong n) + exec_straight ge (opimm64 op opi rd r1 n ::g k) rs m k rs' m + /\ rs'#rd = sem rs#r1 (Vlong n) /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. unfold opimm64. generalize (make_immed64_sound n); intros E. @@ -261,7 +264,7 @@ Lemma addptrofs_correct: forall rd r1 n k rs m, r1 <> GPR31 -> exists rs', - exec_straight ge fn (addptrofs rd r1 n k) rs m k rs' m + exec_straight ge (addptrofs rd r1 n ::g k) rs m k rs' m /\ Val.lessdef (Val.offset_ptr rs#r1 n) rs'#rd /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. @@ -274,9 +277,11 @@ Proof. - unfold addimm64. exploit (opimm64_correct Paddl Paddil Val.addl); eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. split; auto. - rewrite B. unfold getw. destruct (rs r1); simpl; auto. + rewrite B. destruct (rs r1); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto. Qed. + +(* (* Lemma addptrofs_correct_2: forall rd r1 n k (rs: regset) m b ofs, @@ -781,94 +786,93 @@ Qed. intros; Simpl. *) -(* (** Translation of condition operators *) Lemma transl_cond_int32s_correct: forall cmp rd r1 r2 k rs m, exists rs', - exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m - /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd + exec_straight ge (basics_to_code (transl_cond_int32s cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.cmp cmp rs#r1 rs#r2) rs'#rd /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. Qed. Lemma transl_cond_int32u_correct: forall cmp rd r1 r2 k rs m, exists rs', - exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m - /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2 + exec_straight ge (basics_to_code (transl_cond_int32u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs#r1 rs#r2 /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. Qed. Lemma transl_cond_int64s_correct: forall cmp rd r1 r2 k rs m, exists rs', - exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd + exec_straight ge (basics_to_code (transl_cond_int64s cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 rs#r2)) rs'#rd /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. Qed. Lemma transl_cond_int64u_correct: forall cmp rd r1 r2 k rs m, exists rs', - exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m - /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2) + exec_straight ge (basics_to_code (transl_cond_int64u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 rs#r2) /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. Qed. @@ -876,22 +880,22 @@ Lemma transl_condimm_int32s_correct: forall cmp rd r1 n k rs m, r1 <> GPR31 -> exists rs', - exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m + exec_straight ge (basics_to_code (transl_condimm_int32s cmp rd r1 n k)) rs m (basics_to_code k) rs' m /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. Qed. @@ -899,22 +903,22 @@ Lemma transl_condimm_int32u_correct: forall cmp rd r1 n k rs m, r1 <> GPR31 -> exists rs', - exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m + exec_straight ge (basics_to_code (transl_condimm_int32u cmp rd r1 n k)) rs m (basics_to_code k) rs' m /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. Qed. @@ -922,22 +926,22 @@ Lemma transl_condimm_int64s_correct: forall cmp rd r1 n k rs m, r1 <> GPR31 -> exists rs', - exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m + exec_straight ge (basics_to_code (transl_condimm_int64s cmp rd r1 n k)) rs m (basics_to_code k) rs' m /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. Qed. @@ -945,22 +949,22 @@ Lemma transl_condimm_int64u_correct: forall cmp rd r1 n k rs m, r1 <> GPR31 -> exists rs', - exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m + exec_straight ge (basics_to_code (transl_condimm_int64u cmp rd r1 n k)) rs m (basics_to_code k) rs' m /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. Qed. @@ -968,7 +972,7 @@ Lemma transl_cond_op_correct: forall cond rd args k c rs m, transl_cond_op cond rd args k = OK c -> exists rs', - exec_straight ge fn c rs m k rs' m + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd /\ forall r, r <> PC -> r <> rd -> r <> GPR31 -> rs'#r = rs#r. Proof. @@ -977,31 +981,32 @@ Proof. intros until m; intros TR. destruct cond; simpl in TR; ArgsInv. + (* cmp *) - exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. + exploit transl_cond_int32s_correct; eauto. simpl. intros (rs' & A & B & C). exists rs'; eauto. + (* cmpu *) - exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C). + exploit transl_cond_int32u_correct; eauto. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite B; auto. + (* cmpimm *) apply transl_condimm_int32s_correct; eauto with asmgen. + (* cmpuimm *) apply transl_condimm_int32u_correct; eauto with asmgen. + (* cmpl *) - exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C). + exploit transl_cond_int64s_correct; eauto. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite MKTOT; eauto. + (* cmplu *) - exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C). + exploit transl_cond_int64u_correct; eauto. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto. + (* cmplimm *) - exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. + exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite MKTOT; eauto. + (* cmpluimm *) - exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. + exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite MKTOT; eauto. Qed. (* +(* + (* cmpf *) destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. fold (Val.cmpf c0 (rs x) (rs x0)). @@ -1059,6 +1064,7 @@ Qed. apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto. split; intros; Simpl. *) +*) (** Some arithmetic properties. *) @@ -1075,18 +1081,18 @@ Qed. Lemma cast32signed_correct: forall (d s: ireg) (k: code) (rs: regset) (m: mem), exists rs': regset, - exec_straight ge fn (cast32signed d s k) rs m k rs' m + exec_straight ge (cast32signed d s ::g k) rs m k rs' m /\ Val.lessdef (Val.longofint (rs s)) (rs' d) /\ (forall r: preg, r <> PC -> r <> d -> rs' r = rs r). Proof. intros. unfold cast32signed. destruct (ireg_eq d s). - econstructor; split. - + apply exec_straight_one. simpl. eauto with asmgen. Simpl. + + apply exec_straight_one. simpl. eauto with asmgen. + split. * rewrite e. Simpl. * intros. destruct r; Simpl. - econstructor; split. - + apply exec_straight_one. simpl. eauto with asmgen. Simpl. + + apply exec_straight_one. simpl. eauto with asmgen. + split. * Simpl. * intros. destruct r; Simpl. @@ -1103,15 +1109,15 @@ end. Ltac TranslOpSimpl := econstructor; split; - [ apply exec_straight_one; [simpl; eauto | reflexivity] - | split; [ apply Val.lessdef_same; Simpl; fail | intros; Simpl; fail ] ]. + [ apply exec_straight_one; reflexivity + | split; [ apply Val.lessdef_same; simpl; Simpl; fail | intros; simpl; Simpl; fail ] ]. Lemma transl_op_correct: forall op args res k (rs: regset) m v c, transl_op op args res k = OK c -> eval_operation ge (rs#SP) op (map rs (map preg_of args)) m = Some v -> exists rs', - exec_straight ge fn c rs m k rs' m + exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m /\ Val.lessdef v rs'#(preg_of res) /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. Proof. @@ -1123,8 +1129,8 @@ Opaque Int.eq. destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. - (* Oaddrsymbol *) destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)). -+ set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))). - exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. ++ set (rs1 := (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))). + exploit (addptrofs_correct x x ofs (basics_to_code k) rs1 m); eauto with asmgen. intros (rs2 & A & B & C). exists rs2; split. apply exec_straight_step with rs1 m; auto. @@ -1139,22 +1145,22 @@ Opaque Int.eq. exists rs'; split; eauto. auto with asmgen. - (* Ocast8signed *) econstructor; split. - eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. - split; intros; Simpl. - assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. unfold getw. + eapply exec_straight_two. simpl;eauto. simpl;eauto. + split; intros; simpl; Simpl. + assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. - (* Ocast16signed *) econstructor; split. - eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. + eapply exec_straight_two. simpl;eauto. simpl;eauto. split; intros; Simpl. - assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. unfold getw. + assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. - (* Oshrximm *) clear H. exploit Val.shrx_shr_2; eauto. intros E; subst v; clear EV. destruct (Int.eq n Int.zero). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. ++ econstructor; split. apply exec_straight_one. simpl; eauto. split; intros; Simpl. + change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). econstructor; split. @@ -1162,7 +1168,7 @@ Opaque Int.eq. eapply exec_straight_step. simpl; reflexivity. auto. eapply exec_straight_step. simpl; reflexivity. auto. apply exec_straight_one. simpl; reflexivity. auto. - split; intros; unfold getw; Simpl. + split; intros; Simpl. - (* Ocast32signed *) exploit cast32signed_correct; eauto. intros (rs' & A & B & C). exists rs'; split; eauto. split. apply B. @@ -1170,8 +1176,8 @@ Opaque Int.eq. apply C; auto. - (* longofintu *) econstructor; split. - eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto. - split; intros; Simpl. unfold getl; unfold Pregmap.set; Simpl. destruct (PregEq.eq x0 x0). + eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. + split; intros; Simpl. (* unfold Pregmap.set; Simpl. *) destruct (PregEq.eq x0 x0). + destruct (rs x0); auto. simpl. assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto. rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal. @@ -1257,11 +1263,7 @@ Opaque Int.eq. *) Qed. - (** Memory accesses *) -*) - -Definition no := 0. Lemma indexed_memory_access_correct: forall mk_instr base ofs k rs m, |