From 92b48e2aa6d24d1ad487c1d2a3644a57966c765e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 3 May 2019 09:25:48 +0200 Subject: rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/Asmblock.v | 4 ++-- mppa_k1c/Asmblockdeps.v | 9 ++++---- mppa_k1c/Asmblockgen.v | 4 ++-- mppa_k1c/Asmblockgenproof1.v | 28 +++++++++++------------ mppa_k1c/Asmexpand.ml | 44 ++++++++++++++++++------------------ mppa_k1c/Asmvliw.v | 14 ++---------- mppa_k1c/PostpassSchedulingOracle.ml | 5 ++-- mppa_k1c/PostpassSchedulingproof.v | 38 ++++++++----------------------- mppa_k1c/TargetPrinter.ml | 4 +--- mppa_k1c/lib/Asmblockgenproof0.v | 4 ++-- 10 files changed, 61 insertions(+), 93 deletions(-) diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 1988813f..9abc1ca1 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -264,13 +264,13 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := parexec (** Auxiliaries for memory accesses *) -Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := parexec_load_offset ge chunk rs rs m m d a ofs. +Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := parexec_load_offset chunk rs rs m m d a ofs. Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_reg chunk rs rs m m d a ro. Definition exec_load_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_regxs chunk rs rs m m d a ro. -Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset ge chunk rs rs m m s a ofs. +Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset chunk rs rs m m s a ofs. Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_reg chunk rs rs m m s a ro. diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 1ee5002c..7cfcbff1 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -135,7 +135,7 @@ Definition arith_eval (ao: arith_op) (l: list value) := Definition exec_load_deps_offset (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) := let (ge, fn) := Ge in - match (eval_offset ge ofs) with + match (eval_offset ofs) with | OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with | None => None | Some vl => Some (Val vl) @@ -165,7 +165,7 @@ Definition load_eval (lo: load_op) (l: list value) := Definition exec_store_deps_offset (chunk: memory_chunk) (m: mem) (vs va: val) (ofs: offset) := let (ge, fn) := Ge in - match (eval_offset ge ofs) with + match (eval_offset ofs) with | OK ptr => match Mem.storev chunk m (Val.offset_ptr va ptr) vs with | None => None | Some m' => Some (Memstate m') @@ -841,7 +841,8 @@ Proof. (* Load Offset *) + destruct i; simpl load_chunk. all: unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0; - destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; + unfold eval_offset; + simpl; auto; destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. @@ -865,7 +866,7 @@ Proof. (* Store Offset *) + destruct i; simpl store_chunk. all: unfold parexec_store_offset; simpl; unfold exec_store_deps_offset; erewrite GENV, H, H0; rewrite (H0 ra); - destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; + unfold eval_offset; simpl; auto; destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index ca7094da..dc55715a 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -803,7 +803,7 @@ Definition indexed_memory_access (base: ireg) (ofs: ptrofs) := match make_immed64 (Ptrofs.to_int64 ofs) with | Imm64_single imm => - mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) + mk_instr base (Ptrofs.of_int64 imm) end. Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := @@ -868,7 +868,7 @@ Definition transl_memory_access do rs <- ireg_of a1; OK (indexed_memory_access mk_instr rs ofs ::i k) | Aglobal id ofs, nil => - OK (Ploadsymbol id ofs RTMP ::i (mk_instr RTMP (Ofsimm Ptrofs.zero) ::i k)) + OK (Ploadsymbol id ofs RTMP ::i (mk_instr RTMP Ptrofs.zero ::i k)) | Ainstack ofs, nil => OK (indexed_memory_access mk_instr SP ofs ::i k) | _, _ => diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index b265f221..c3ee28f1 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1872,7 +1872,7 @@ Lemma indexed_memory_access_correct: exists base' ofs' rs' ptr', exec_straight_opt (indexed_memory_access mk_instr base ofs ::g k) rs m (mk_instr base' ofs' ::g k) rs' m - /\ eval_offset ge ofs' = OK ptr' + /\ eval_offset ofs' = OK ptr' /\ Val.offset_ptr rs'#base' ptr' = Val.offset_ptr rs#base ofs /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. Proof. @@ -1917,7 +1917,7 @@ Qed. Lemma indexed_load_access_correct: forall chunk (mk_instr: ireg -> offset -> basic) rd m, (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs) -> forall (base: ireg) ofs k (rs: regset) v, Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v -> base <> RTMP -> @@ -1938,7 +1938,7 @@ Qed. Lemma indexed_store_access_correct: forall chunk (mk_instr: ireg -> offset -> basic) r1 m, (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk rs m r1 base ofs) -> forall (base: ireg) ofs k (rs: regset) m', Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' -> base <> RTMP -> r1 <> RTMP -> @@ -1974,7 +1974,7 @@ Proof. /\ c = indexed_memory_access mk_instr base ofs :: k /\ forall base' ofs' rs', exec_basic_instr ge (mk_instr base' ofs') rs' m = - exec_load_offset ge (chunk_of_type ty) rs' m rd base' ofs'). + exec_load_offset (chunk_of_type ty) rs' m rd base' ofs'). { unfold loadind in TR. destruct ty, (preg_of dst); inv TR; econstructor; esplit; eauto. } destruct A as (mk_instr & rd & rdEq & B & C). subst c. rewrite rdEq. @@ -1996,7 +1996,7 @@ Proof. /\ c = indexed_memory_access mk_instr base ofs :: k /\ forall base' ofs' rs', exec_basic_instr ge (mk_instr base' ofs') rs' m = - exec_store_offset ge (chunk_of_type ty) rs' m rr base' ofs'). + exec_store_offset (chunk_of_type ty) rs' m rr base' ofs'). { unfold storeind in TR. destruct ty, (preg_of src); inv TR; econstructor; esplit; eauto. } destruct A as (mk_instr & rr & rsEq & B & C). subst c. eapply indexed_store_access_correct; eauto with asmgen. @@ -2066,7 +2066,7 @@ Lemma transl_memory_access_correct: eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> exists base ofs rs' ptr, exec_straight_opt (basics_to_code c) rs m (mk_instr base ofs ::g (basics_to_code k)) rs' m - /\ eval_offset ge ofs = OK ptr + /\ eval_offset ofs = OK ptr /\ Val.offset_ptr rs'#base ptr = v /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. Proof. @@ -2183,7 +2183,7 @@ Qed. Lemma transl_load_access_correct: forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v', (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs) -> transl_memory_access mk_instr addr args k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> Mem.loadv chunk m v = Some v' -> @@ -2211,7 +2211,7 @@ Lemma transl_load_memory_access_ok: preg_of dst = IR rd /\ transl_memory_access mk_instr addr args k = OK c /\ forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs. + exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs. Proof. intros until m. intros ADDR TR ? ?. unfold transl_load in TR. destruct addr; try contradiction. @@ -2347,7 +2347,7 @@ Qed. Lemma transl_store_access_correct: forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m', (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) -> + exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk rs m r1 base ofs) -> transl_memory_access mk_instr addr args k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> Mem.storev chunk m v rs#r1 = Some m' -> @@ -2368,16 +2368,16 @@ Qed. Remark exec_store_offset_8_sign rs m x base ofs: - exec_store_offset ge Mint8unsigned rs m x base ofs = exec_store_offset ge Mint8signed rs m x base ofs. + exec_store_offset Mint8unsigned rs m x base ofs = exec_store_offset Mint8signed rs m x base ofs. Proof. - unfold exec_store_offset. unfold parexec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev. + unfold exec_store_offset. unfold parexec_store_offset. unfold eval_offset; auto. unfold Mem.storev. destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_8. reflexivity. Qed. Remark exec_store_offset_16_sign rs m x base ofs: - exec_store_offset ge Mint16unsigned rs m x base ofs = exec_store_offset ge Mint16signed rs m x base ofs. + exec_store_offset Mint16unsigned rs m x base ofs = exec_store_offset Mint16signed rs m x base ofs. Proof. - unfold exec_store_offset. unfold parexec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev. + unfold exec_store_offset. unfold parexec_store_offset. unfold eval_offset; auto. unfold Mem.storev. destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_16. reflexivity. Qed. @@ -2391,7 +2391,7 @@ Lemma transl_store_memory_access_ok: preg_of src = IR rr /\ transl_memory_access mk_instr addr args k = OK c /\ (forall base ofs rs, - exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk' rs m rr base ofs) + exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk' rs m rr base ofs) /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src). Proof. intros until m'. intros ? TR ? ?. diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index ba771bcb..c49cfbd5 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -154,10 +154,10 @@ let expand_builtin_memcpy_big sz al src dst = let lbl = new_label() in emit (Ploopdo (tmpbuf, lbl)); emit Psemi; - emit (Plb (tmpbuf, srcptr, AOff (Asmvliw.Ofsimm Z.zero))); + emit (Plb (tmpbuf, srcptr, AOff Z.zero)); emit (Paddil (srcptr, srcptr, Z.one)); emit Psemi; - emit (Psb (tmpbuf, dstptr, AOff (Asmvliw.Ofsimm Z.zero))); + emit (Psb (tmpbuf, dstptr, AOff Z.zero)); emit (Paddil (dstptr, dstptr, Z.one)); emit Psemi; emit (Plabel lbl);; @@ -173,30 +173,30 @@ let expand_builtin_memcpy sz al args = let expand_builtin_vload_common chunk base ofs res = match chunk, res with | Mint8unsigned, BR(Asmvliw.IR res) -> - emit (Plbu (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plbu (res, base, AOff ofs)) | Mint8signed, BR(Asmvliw.IR res) -> - emit (Plb (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plb (res, base, AOff ofs)) | Mint16unsigned, BR(Asmvliw.IR res) -> - emit (Plhu (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plhu (res, base, AOff ofs)) | Mint16signed, BR(Asmvliw.IR res) -> - emit (Plh (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plh (res, base, AOff ofs)) | Mint32, BR(Asmvliw.IR res) -> - emit (Plw (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plw (res, base, AOff ofs)) | Mint64, BR(Asmvliw.IR res) -> - emit (Pld (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Pld (res, base, AOff ofs)) | Mint64, BR_splitlong(BR(Asmvliw.IR res1), BR(Asmvliw.IR res2)) -> let ofs' = Ptrofs.add ofs _4 in if base <> res2 then begin - emit (Plw (res2, base, AOff (Asmvliw.Ofsimm ofs))); - emit (Plw (res1, base, AOff (Asmvliw.Ofsimm ofs'))) + emit (Plw (res2, base, AOff ofs)); + emit (Plw (res1, base, AOff ofs')) end else begin - emit (Plw (res1, base, AOff (Asmvliw.Ofsimm ofs'))); - emit (Plw (res2, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Plw (res1, base, AOff ofs')); + emit (Plw (res2, base, AOff ofs)) end | Mfloat32, BR(Asmvliw.IR res) -> - emit (Pfls (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Pfls (res, base, AOff ofs)) | Mfloat64, BR(Asmvliw.IR res) -> - emit (Pfld (res, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Pfld (res, base, AOff ofs)) | _ -> assert false @@ -215,21 +215,21 @@ let expand_builtin_vload chunk args res = let expand_builtin_vstore_common chunk base ofs src = match chunk, src with | (Mint8signed | Mint8unsigned), BA(Asmvliw.IR src) -> - emit (Psb (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Psb (src, base, AOff ofs)) | (Mint16signed | Mint16unsigned), BA(Asmvliw.IR src) -> - emit (Psh (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Psh (src, base, AOff ofs)) | Mint32, BA(Asmvliw.IR src) -> - emit (Psw (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Psw (src, base, AOff ofs)) | Mint64, BA(Asmvliw.IR src) -> - emit (Psd (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Psd (src, base, AOff ofs)) | Mint64, BA_splitlong(BA(Asmvliw.IR src1), BA(Asmvliw.IR src2)) -> let ofs' = Ptrofs.add ofs _4 in - emit (Psw (src2, base, AOff (Asmvliw.Ofsimm ofs))); - emit (Psw (src1, base, AOff (Asmvliw.Ofsimm ofs'))) + emit (Psw (src2, base, AOff ofs)); + emit (Psw (src1, base, AOff ofs')) | Mfloat32, BA(Asmvliw.IR src) -> - emit (Pfss (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Pfss (src, base, AOff ofs)) | Mfloat64, BA(Asmvliw.IR src) -> - emit (Pfsd (src, base, AOff (Asmvliw.Ofsimm ofs))) + emit (Pfsd (src, base, AOff ofs)) | _ -> assert false diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index e460727c..c25d4235 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -152,9 +152,7 @@ Inductive ftest: Type := (** Offsets for load and store instructions. An offset is either an immediate integer or the low part of a symbol. *) -Inductive offset : Type := - | Ofsimm (ofs: ptrofs) - | Ofslow (id: ident) (ofs: ptrofs). +Definition offset : Type := ptrofs. (** We model a subset of the K1c instruction set. In particular, we do not support floats yet. @@ -1093,15 +1091,7 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset := | PArithARRI64 n d s i => rsw#d <- (arith_eval_arri64 n rsr#d rsr#s i) end. -Definition eval_offset (ofs: offset) : res ptrofs := - match ofs with - | Ofsimm n => OK n - | Ofslow id delta => - match (Genv.symbol_address ge id delta) with - | Vptr b ofs => OK ofs - | _ => Error (msg "Asmblock.eval_offset") - end - end. +Definition eval_offset (ofs: offset) : res ptrofs := OK ofs. (** * load/store *) diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index abc3dcb6..033cf943 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -544,9 +544,8 @@ exception InvalidEncoding let rec_to_usage r = let encoding = match r.imm with None -> None | Some (I32 i) | Some (I64 i) -> Some (encode_imm @@ Z.to_int64 i) - | Some (Off (Ofsimm ptr)) -> Some (encode_imm @@ camlint64_of_ptrofs ptr) - | Some (Off (Ofslow (_, _))) -> Some E27U27L10 (* FIXME *) - (* I do not know yet in which context Ofslow can be used by CompCert *) + | Some (Off ptr) -> Some (encode_imm @@ camlint64_of_ptrofs ptr) + and real_inst = ab_inst_to_real r.inst in match real_inst with | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 43c8acb8..47248e3e 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -96,11 +96,11 @@ Proof. Qed. Lemma exec_load_offset_pc_var: - forall ge t rs m rd ra ofs rs' m' v, - exec_load_offset ge t rs m rd ra ofs = Next rs' m' -> - exec_load_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. + forall t rs m rd ra ofs rs' m' v, + exec_load_offset t rs m rd ra ofs = Next rs' m' -> + exec_load_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. - intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. + intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - discriminate. @@ -129,12 +129,12 @@ Proof. Qed. Lemma exec_store_offset_pc_var: - forall ge t rs m rd ra ofs rs' m' v, - exec_store_offset ge t rs m rd ra ofs = Next rs' m' -> - exec_store_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. + forall t rs m rd ra ofs rs' m' v, + exec_store_offset t rs m rd ra ofs = Next rs' m' -> + exec_store_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate. - destruct (eval_offset ge ofs); try discriminate. + destruct (eval_offset ofs); try discriminate. destruct (Mem.storev _ _ _). - inv H. apply next_eq; auto. - discriminate. @@ -600,32 +600,12 @@ Proof. unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto. Qed. -Lemma eval_offset_preserved: - forall ofs, eval_offset ge ofs = eval_offset tge ofs. -Proof. - intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto. -Qed. - -Lemma transf_exec_load_offset: - forall t rs m rd ra ofs, exec_load_offset ge t rs m rd ra ofs = exec_load_offset tge t rs m rd ra ofs. -Proof. - intros. unfold exec_load_offset. unfold parexec_load_offset. rewrite eval_offset_preserved. reflexivity. -Qed. - -Lemma transf_exec_store_offset: - forall t rs m rs0 ra ofs, exec_store_offset ge t rs m rs0 ra ofs = exec_store_offset tge t rs m rs0 ra ofs. -Proof. - intros. unfold exec_store_offset. unfold parexec_store_offset. rewrite eval_offset_preserved. reflexivity. -Qed. - Lemma transf_exec_basic_instr: forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m. Proof. intros. pose symbol_address_preserved. unfold exec_basic_instr. unfold parexec_basic_instr. exploreInst; simpl; auto; try congruence. - - unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. - - apply transf_exec_load_offset. - - apply transf_exec_store_offset. + unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. Qed. Lemma transf_exec_body: diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 62b02f58..156b16d0 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -160,9 +160,7 @@ module Target (*: TARGET*) = *) (* Offset part of a load or store *) - let offset oc = let open Asmvliw in function - | Ofsimm n -> ptrofs oc n - | Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs) + let offset oc n = ptrofs oc n let addressing oc = function | AOff ofs -> offset oc ofs diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 0a83a903..130f0b12 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -944,10 +944,10 @@ Lemma exec_basic_instr_pc: Proof. intros. destruct b; try destruct i; try destruct i. all: try (inv H; Simpl). - 1-10: try (unfold parexec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + 1-10: try (unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). 1-10: try (unfold parexec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). 1-10: try (unfold parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - 1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). + 1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). 1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. 1-10: try (unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. -- cgit