From 2b226da49ea711bfe8139a0fae7c44cb432e2f61 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 5 Feb 2019 13:27:26 +0100 Subject: Removing the low_half axiom --- mppa_k1c/Asmblock.v | 46 +++++++++++++++++--------------------- mppa_k1c/Asmblockgenproof1.v | 34 +++++++++++++++------------- mppa_k1c/PostpassSchedulingproof.v | 11 +++------ mppa_k1c/lib/Asmblockgenproof0.v | 8 +++---- 4 files changed, 46 insertions(+), 53 deletions(-) diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 300ab0fc..1600b867 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -934,42 +934,38 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset) (m: mem) : regset (** * load/store *) -(** The two functions below axiomatize how the linker processes - symbolic references [symbol + offset)] and splits their - actual values into a 20-bit high part [%hi(symbol + offset)] and - a 12-bit low part [%lo(symbol + offset)]. *) - -Parameter low_half: genv -> ident -> ptrofs -> ptrofs. -Parameter high_half: genv -> ident -> ptrofs -> val. - -(** The fundamental property of these operations is that, when applied - to the address of a symbol, their results can be recombined by - addition, rebuilding the original address. *) - -Axiom low_high_half: - forall id ofs, - Val.offset_ptr (high_half ge id ofs) (low_half ge id ofs) = Genv.symbol_address ge id ofs. - (** Auxiliaries for memory accesses *) -Definition eval_offset (ofs: offset) : ptrofs := +Definition eval_offset (ofs: offset) : res ptrofs := match ofs with - | Ofsimm n => n - | Ofslow id delta => low_half ge id delta + | 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 exec_load (chunk: memory_chunk) (rs: regset) (m: mem) (d: ireg) (a: ireg) (ofs: offset) := - match Mem.loadv chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) with - | None => Stuck - | Some v => Next (rs#d <- v) m + match (eval_offset ofs) with + | OK ptr => + match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with + | None => Stuck + | Some v => Next (rs#d <- v) m + end + | _ => Stuck end. Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem) (s: ireg) (a: ireg) (ofs: offset) := - match Mem.storev chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) (rs s) with - | None => Stuck - | Some m' => Next rs m' + match (eval_offset ofs) with + | OK ptr => + match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with + | None => Stuck + | Some m' => Next rs m' + end + | _ => Stuck end. (** * basic instructions *) diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index bf3be247..81e02e4e 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1268,10 +1268,11 @@ Qed. Lemma indexed_memory_access_correct: forall mk_instr base ofs k rs m, base <> RTMP -> - exists base' ofs' rs', + 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 - /\ Val.offset_ptr rs'#base' (eval_offset ge ofs') = Val.offset_ptr rs#base ofs + /\ eval_offset ge 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. unfold indexed_memory_access; intros. @@ -1279,7 +1280,7 @@ Proof. assert (Archi.ptr64 = true) as SF; auto. - generalize (make_immed64_sound (Ptrofs.to_int64 ofs)); intros EQ. destruct (make_immed64 (Ptrofs.to_int64 ofs)). -+ econstructor; econstructor; econstructor; split. ++ econstructor; econstructor; econstructor; econstructor; split. apply exec_straight_opt_refl. split; auto. simpl. subst imm. rewrite Ptrofs.of_int64_to_int64 by auto. auto. (* @@ -1326,10 +1327,10 @@ Lemma indexed_load_access_correct: Proof. intros until m; intros EXEC; intros until v; intros LOAD NOT31. exploit indexed_memory_access_correct; eauto. - intros (base' & ofs' & rs' & A & B & C). + intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC. - unfold exec_load. rewrite B, LOAD. eauto. Simpl. + unfold exec_load. rewrite PtrEq. rewrite B, LOAD. eauto. Simpl. split; intros; Simpl. auto. Qed. @@ -1346,10 +1347,10 @@ Lemma indexed_store_access_correct: Proof. intros until m; intros EXEC; intros until m'; intros STORE NOT31 NOT31'. exploit indexed_memory_access_correct. instantiate (1 := base). eauto. - intros (base' & ofs' & rs' & A & B & C). + intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC. - unfold exec_store. rewrite B, C, STORE. + unfold exec_store. rewrite PtrEq. rewrite B, C, STORE. eauto. discriminate. { intro. inv H. contradiction. } @@ -1463,9 +1464,10 @@ Lemma transl_memory_access_correct: forall mk_instr addr args k c (rs: regset) m v, transl_memory_access mk_instr addr args k = OK c -> eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v -> - exists base ofs rs', + 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 - /\ Val.offset_ptr rs'#base (eval_offset ge ofs) = v + /\ eval_offset ge ofs = OK ptr + /\ Val.offset_ptr rs'#base ptr = v /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. Proof. intros until v; intros TR EV. @@ -1473,14 +1475,14 @@ Proof. - (* indexed *) inv EV. apply indexed_memory_access_correct; eauto with asmgen. - (* global *) - simpl in EV. inv EV. inv TR. econstructor; econstructor; econstructor; split. + simpl in EV. inv EV. inv TR. econstructor; econstructor; econstructor; econstructor; split. constructor. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. unfold eval_offset. + split; split; intros; Simpl. assert (Val.lessdef (Val.offset_ptr (Genv.symbol_address ge i i0) Ptrofs.zero) (Genv.symbol_address ge i i0)). { apply Val.offset_ptr_zero. } remember (Genv.symbol_address ge i i0) as symbol. destruct symbol; auto. - + contradict Heqsymbol; unfold Genv.symbol_address; + + contradict Heqsymbol; unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); discriminate. + contradict Heqsymbol; unfold Genv.symbol_address; destruct (Genv.find_symbol ge i); discriminate. @@ -1507,10 +1509,10 @@ Lemma transl_load_access_correct: Proof. intros until v'; intros INSTR TR EV LOAD. exploit transl_memory_access_correct; eauto. - intros (base & ofs & rs' & A & B & C). + intros (base & ofs & rs' & ptr & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. - rewrite INSTR. unfold exec_load. rewrite B, LOAD. reflexivity. Simpl. + rewrite INSTR. unfold exec_load. rewrite PtrEq, B, LOAD. reflexivity. Simpl. split; intros; Simpl. auto. Qed. @@ -1528,10 +1530,10 @@ Lemma transl_store_access_correct: Proof. intros until m'; intros INSTR TR EV STORE NOT31. exploit transl_memory_access_correct; eauto. - intros (base & ofs & rs' & A & B & C). + intros (base & ofs & rs' & ptr & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. - rewrite INSTR. unfold exec_store. rewrite B. rewrite C; try discriminate. rewrite STORE. auto. + rewrite INSTR. unfold exec_store. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto. intro. inv H. contradiction. auto. Qed. diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index d16362a8..c6b037fd 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -127,10 +127,6 @@ Axiom verified_schedule_header: header bb = header tbb /\ Forall (fun b => header b = nil) lbb. -(* This needs to be axiomatized since we have no information on low_half (axiomatized parameter, see Asmblock.v) *) -Axiom low_half_preservation: - forall id ofs ge tge, Genv.symbol_address ge id ofs = Genv.symbol_address tge id ofs -> low_half ge id ofs = low_half tge id ofs. - Remark builtin_body_nil: forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil. Proof. @@ -242,7 +238,7 @@ Lemma exec_load_pc_var: exec_load ge t rs m rd ra ofs = Next rs' m' -> exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. - intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. + intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. destruct (Mem.loadv _ _ _). - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - discriminate. @@ -253,7 +249,7 @@ Lemma exec_store_pc_var: exec_store ge t rs m rd ra ofs = Next rs' m' -> exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. Proof. - intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. + intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate. destruct (Mem.storev _ _ _). - inv H. apply next_eq; auto. - discriminate. @@ -718,8 +714,7 @@ Qed. Lemma eval_offset_preserved: forall ofs, eval_offset ge ofs = eval_offset tge ofs. Proof. - intros. unfold eval_offset. destruct ofs; auto. erewrite low_half_preservation; eauto. - apply symbol_address_preserved. + intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto. Qed. Lemma transf_exec_load: diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 443e8757..8c299f88 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -937,11 +937,11 @@ Lemma exec_basic_instr_pc: Proof. intros. destruct b; try destruct i; try destruct i. all: try (inv H; Simpl). - all: try (unfold exec_load in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). - all: try (unfold exec_store in H1; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). + all: try (unfold exec_load in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). + all: try (unfold exec_store in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - destruct (rs1 _); try discriminate. - destruct (Mem.free _ _ _ _). inv H0. Simpl. discriminate. + destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. + destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. destruct rs; try discriminate. inv H1. Simpl. destruct rd; try discriminate. inv H1; Simpl. auto. -- cgit