summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/Asm.v10
-rw-r--r--arm/Asmgen.v9
-rw-r--r--arm/Asmgenproof.v80
-rw-r--r--arm/Op.v3
4 files changed, 41 insertions, 61 deletions
diff --git a/arm/Asm.v b/arm/Asm.v
index e689c20..13c2e57 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -146,7 +146,7 @@ Inductive instruction : Type :=
(* Pseudo-instructions *)
| Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *)
- | Pfreeframe: int -> instruction (**r deallocate stack frame and restore previous frame *)
+ | Pfreeframe: Z -> Z -> int -> instruction (**r deallocate stack frame and restore previous frame *)
| Plabel: label -> instruction (**r define a code label *)
| Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *)
| Pbtbl: ireg -> list label -> instruction. (**r N-way branch through a jump table *)
@@ -503,12 +503,16 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
| None => Error
| Some m2 => OK (nextinstr (rs#IR13 <- sp)) m2
end
- | Pfreeframe pos =>
+ | Pfreeframe lo hi pos =>
match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with
| None => Error
| Some v =>
match rs#IR13 with
- | Vptr stk ofs => OK (nextinstr (rs#IR13 <- v)) (Mem.free m stk)
+ | Vptr stk ofs =>
+ match Mem.free m stk lo hi with
+ | None => Error
+ | Some m' => OK (nextinstr (rs#IR13 <- v)) m'
+ end
| _ => Error
end
end
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 069a08a..2a3b3f3 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -473,10 +473,12 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
Pblsymb symb :: k
| Mtailcall sig (inl r) =>
loadind_int IR13 f.(fn_retaddr_ofs) IR14
- (Pfreeframe f.(fn_link_ofs) :: Pbreg (ireg_of r) :: k)
+ (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
+ :: Pbreg (ireg_of r) :: k)
| Mtailcall sig (inr symb) =>
loadind_int IR13 f.(fn_retaddr_ofs) IR14
- (Pfreeframe f.(fn_link_ofs) :: Pbsymb symb :: k)
+ (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
+ :: Pbsymb symb :: k)
| Mlabel lbl =>
Plabel lbl :: k
| Mgoto lbl =>
@@ -488,7 +490,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
Pbtbl IR14 tbl :: k
| Mreturn =>
loadind_int IR13 f.(fn_retaddr_ofs) IR14
- (Pfreeframe f.(fn_link_ofs) :: Pbreg IR14 :: k)
+ (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
+ :: Pbreg IR14 :: k)
end.
Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 0260feb..eec0c65 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -55,7 +55,7 @@ Lemma functions_translated:
Genv.find_funct_ptr ge b = Some f ->
exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = Errors.OK tf.
Proof
- (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF).
+ (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
Lemma functions_transl:
forall f b,
@@ -741,7 +741,7 @@ Lemma exec_Mload_prop:
(dst : mreg) (c : list Mach.instruction) (ms : mreg -> val)
(m : mem) (a v : val),
eval_addressing ge sp addr ms ## args = Some a ->
- loadv chunk m a = Some v ->
+ Mem.loadv chunk m a = Some v ->
exec_instr_prop (Machconcr.State s fb sp (Mload chunk addr args dst :: c) ms m)
E0 (Machconcr.State s fb sp c (Regmap.set dst v ms) m).
Proof.
@@ -756,13 +756,14 @@ Proof.
eauto; intros; reflexivity.
Qed.
+Lemma storev_8_signed_unsigned: forall m a v, Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_8. Qed. Lemma storev_16_signed_unsigned: forall m a v, Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_16. Qed.
Lemma exec_Mstore_prop:
forall (s : list stackframe) (fb : block) (sp : val)
(chunk : memory_chunk) (addr : addressing) (args : list mreg)
(src : mreg) (c : list Mach.instruction) (ms : mreg -> val)
(m m' : mem) (a : val),
eval_addressing ge sp addr ms ## args = Some a ->
- storev chunk m a (ms src) = Some m' ->
+ Mem.storev chunk m a (ms src) = Some m' ->
exec_instr_prop (Machconcr.State s fb sp (Mstore chunk addr args src :: c) ms m) E0
(Machconcr.State s fb sp c ms m').
Proof.
@@ -775,8 +776,9 @@ Proof.
destruct chunk; simpl; simpl in H6;
try (rewrite storev_8_signed_unsigned in H0);
try (rewrite storev_16_signed_unsigned in H0);
+ simpl;
(eapply transl_store_int_correct || eapply transl_store_float_correct);
- eauto; intros; reflexivity.
+ eauto; intros; simpl; auto.
Qed.
Lemma exec_Mcall_prop:
@@ -826,18 +828,7 @@ Proof.
rewrite RA_EQ. econstructor; eauto.
Qed.
-Lemma exec_Mtailcall_prop:
- forall (s : list stackframe) (fb stk : block) (soff : int)
- (sig : signature) (ros : mreg + ident) (c : list Mach.instruction)
- (ms : Mach.regset) (m : mem) (f: function) (f' : block),
- find_function_ptr ge ros ms = Some f' ->
- Genv.find_funct_ptr ge fb = Some (Internal f) ->
- load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
- load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
- exec_instr_prop
- (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0
- (Callstate s f' ms (free m stk)).
-Proof.
+Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (sig : signature) (ros : mreg + ident) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m', find_function_ptr ge ros ms = Some f' -> Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 (Callstate s f' ms m'). Proof.
intros; red; intros; inv MS.
assert (f0 = f) by congruence. subst f0.
generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
@@ -846,24 +837,25 @@ Proof.
match ros with inl r => Pbreg (ireg_of r) | inr symb => Pbsymb symb end).
assert (TR: transl_code f (Mtailcall sig ros :: c) =
loadind_int IR13 (fn_retaddr_ofs f) IR14
- (Pfreeframe (fn_link_ofs f) :: call_instr :: transl_code f c)).
+ (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)).
unfold call_instr; destruct ros; auto.
destruct (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14
rs m (parent_ra s)
- (Pfreeframe f.(fn_link_ofs) :: call_instr :: transl_code f c))
+ (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c))
as [rs1 [EXEC1 [RES1 OTH1]]].
rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))).
assert (EXEC2: exec_straight tge (transl_function f)
(transl_code f (Mtailcall sig ros :: c)) rs m
- (call_instr :: transl_code f c) rs2 (free m stk)).
+ (call_instr :: transl_code f c) rs2 m').
rewrite TR. eapply exec_straight_trans. eexact EXEC1.
apply exec_straight_one. simpl.
rewrite OTH1; auto with ppcgen.
rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
- unfold load_stack in H1. simpl in H1. simpl. rewrite H1. auto. auto.
+ unfold load_stack in H1. simpl in H1. simpl. rewrite H1.
+ rewrite H3. auto. auto.
set (rs3 := rs2#PC <- (Vptr f' Int.zero)).
- left. exists (State rs3 (free m stk)); split.
+ left. exists (State rs3 m'); split.
(* Execution *)
eapply plus_right'. eapply exec_straight_exec; eauto.
inv AT. exploit exec_straight_steps_2; eauto.
@@ -878,7 +870,7 @@ Proof.
rewrite Pregmap.gso. rewrite OTH1; auto with ppcgen.
rewrite <- (ireg_val ms (Vptr stk soff) rs); auto.
destruct (ms m0); try discriminate.
- generalize H. predSpec Int.eq Int.eq_spec i Int.zero; intros; inv H9.
+ generalize H. predSpec Int.eq Int.eq_spec i Int.zero; intros; inv H10.
auto.
decEq. auto with ppcgen. decEq. auto with ppcgen. decEq. auto with ppcgen.
replace (symbol_offset tge i Int.zero) with (Vptr f' Int.zero). auto.
@@ -1036,34 +1028,26 @@ Opaque Zmod. Opaque Zdiv.
unfold rs1. apply agree_nextinstr. apply agree_set_other; auto with ppcgen.
Qed.
-Lemma exec_Mreturn_prop:
- forall (s : list stackframe) (fb stk : block) (soff : int)
- (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: function),
- Genv.find_funct_ptr ge fb = Some (Internal f) ->
- load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) ->
- load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) ->
- exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0
- (Returnstate s ms (free m stk)).
-Proof.
+Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m', Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 (Returnstate s ms m'). Proof.
intros; red; intros; inv MS.
assert (f0 = f) by congruence. subst f0.
exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14
rs m (parent_ra s)
- (Pfreeframe f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)).
+ (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)).
rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
intros [rs1 [EXEC1 [RES1 OTH1]]].
set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))).
assert (EXEC2: exec_straight tge (transl_function f)
(loadind_int IR13 (fn_retaddr_ofs f) IR14
- (Pfreeframe (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c))
- rs m (Pbreg IR14 :: transl_code f c) rs2 (free m stk)).
+ (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c))
+ rs m (Pbreg IR14 :: transl_code f c) rs2 m').
eapply exec_straight_trans. eexact EXEC1.
apply exec_straight_one. simpl. rewrite OTH1; try congruence.
rewrite <- (sp_val ms (Vptr stk soff) rs); auto.
- unfold load_stack in H0. simpl in H0; simpl; rewrite H0. reflexivity.
+ unfold load_stack in H0. simpl in H0; simpl; rewrite H0. rewrite H2. reflexivity.
reflexivity.
set (rs3 := rs2#PC <- (parent_ra s)).
- left; exists (State rs3 (free m stk)); split.
+ left; exists (State rs3 m'); split.
(* execution *)
eapply plus_right'. eapply exec_straight_exec; eauto.
inv AT. exploit exec_straight_steps_2; eauto.
@@ -1093,7 +1077,7 @@ Lemma exec_function_internal_prop:
forall (s : list stackframe) (fb : block) (ms : Mach.regset)
(m : mem) (f : function) (m1 m2 m3 : mem) (stk : block),
Genv.find_funct_ptr ge fb = Some (Internal f) ->
- alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) ->
+ Mem.alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) ->
let sp := Vptr stk (Int.repr (- fn_framesize f)) in
store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 ->
store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 ->
@@ -1102,7 +1086,7 @@ Lemma exec_function_internal_prop:
Proof.
intros; red; intros; inv MS.
assert (WTF: wt_function f).
- generalize (Genv.find_funct_ptr_prop wt_fundef wt_prog H); intro TY.
+ generalize (Genv.find_funct_ptr_prop wt_fundef _ _ wt_prog H); intro TY.
inversion TY; auto.
exploit functions_transl; eauto. intro TFIND.
generalize (functions_transl_no_overflow _ _ H); intro NOOV.
@@ -1146,24 +1130,14 @@ Proof.
econstructor; eauto with coqlib.
Qed.
-Lemma exec_function_external_prop:
- forall (s : list stackframe) (fb : block) (ms : Mach.regset)
- (m : mem) (t0 : trace) (ms' : RegEq.t -> val)
- (ef : external_function) (args : list val) (res : val),
- Genv.find_funct_ptr ge fb = Some (External ef) ->
- event_match ef args t0 res ->
- Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
- ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms ->
- exec_instr_prop (Machconcr.Callstate s fb ms m)
- t0 (Machconcr.Returnstate s ms' m).
-Proof.
+Lemma exec_function_external_prop: forall (s : list stackframe) (fb : block) (ms : Mach.regset) (m : mem) (t0 : trace) (ms' : RegEq.t -> val) (ef : external_function) (args : list val) (res : val) (m': mem), Genv.find_funct_ptr ge fb = Some (External ef) -> external_call ef args m t0 res m' -> Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms -> exec_instr_prop (Machconcr.Callstate s fb ms m) t0 (Machconcr.Returnstate s ms' m'). Proof.
intros; red; intros; inv MS.
exploit functions_translated; eauto.
intros [tf [A B]]. simpl in B. inv B.
left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs IR14))
- m); split.
+ m'); split.
apply plus_one. eapply exec_step_external; eauto.
- eapply extcall_arguments_match; eauto.
+ eauto. eapply extcall_arguments_match; eauto.
econstructor; eauto.
unfold loc_external_result. auto with ppcgen.
Qed.
@@ -1209,14 +1183,14 @@ Proof.
intros. inversion H. unfold ge0 in *.
econstructor; split.
econstructor.
+ eapply Genv.init_mem_transf_partial; eauto.
replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero)
with (Vptr fb Int.zero).
- rewrite (Genv.init_mem_transf_partial _ _ TRANSF).
econstructor; eauto. constructor.
split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen.
unfold symbol_offset.
rewrite (transform_partial_program_main _ _ TRANSF).
- rewrite symbols_preserved. unfold ge; rewrite H0. auto.
+ rewrite symbols_preserved. unfold ge; rewrite H1. auto.
Qed.
Lemma transf_final_states:
diff --git a/arm/Op.v b/arm/Op.v
index 51ce002..7a25511 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -572,8 +572,7 @@ Proof.
destruct v; destruct chunk; exact I.
intros until v. unfold Mem.loadv.
destruct addr; intros; try discriminate.
- generalize (Mem.load_inv _ _ _ _ _ H0).
- intros [X Y]. subst v. apply H.
+ eapply Mem.load_type; eauto.
Qed.
End SOUNDNESS.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 12:21:57 +0000