aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asmblock.v46
-rw-r--r--mppa_k1c/Asmblockgenproof1.v34
-rw-r--r--mppa_k1c/PostpassSchedulingproof.v11
-rw-r--r--mppa_k1c/lib/Asmblockgenproof0.v8
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.
generated by cgit (git 2.34.1) at 2024-07-04 02:20:37 +0000