aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/Mach.v19
-rw-r--r--backend/Stacking.v4
-rw-r--r--mppa_k1c/Asmblockgen.v19
-rw-r--r--mppa_k1c/Asmblockgenproof1.v34
-rw-r--r--mppa_k1c/lib/Machblock.v17
-rw-r--r--mppa_k1c/lib/Machblockgen.v2
-rw-r--r--mppa_k1c/lib/Machblockgenproof.v4
7 files changed, 75 insertions, 24 deletions
diff --git a/backend/Mach.v b/backend/Mach.v
index 9fdee9eb..1c6fdb18 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -56,7 +56,7 @@ Inductive instruction: Type :=
| Msetstack: mreg -> ptrofs -> typ -> instruction
| Mgetparam: ptrofs -> typ -> mreg -> instruction
| Mop: operation -> list mreg -> mreg -> instruction
- | Mload: memory_chunk -> addressing -> list mreg -> mreg -> instruction
+ | Mload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> instruction
| Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction
| Mcall: signature -> mreg + ident -> instruction
| Mtailcall: signature -> mreg + ident -> instruction
@@ -321,11 +321,24 @@ Inductive step: state -> trace -> state -> Prop :=
step (State s f sp (Mop op args res :: c) rs m)
E0 (State s f sp c rs' m)
| exec_Mload:
- forall s f sp chunk addr args dst c rs m a v rs',
+ forall s f sp trap chunk addr args dst c rs m a v rs',
eval_addressing ge sp addr rs##args = Some a ->
Mem.loadv chunk m a = Some v ->
rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) ->
- step (State s f sp (Mload chunk addr args dst :: c) rs m)
+ step (State s f sp (Mload trap chunk addr args dst :: c) rs m)
+ E0 (State s f sp c rs' m)
+ | exec_Mload_notrap1:
+ forall s f sp chunk addr args dst c rs m rs',
+ eval_addressing ge sp addr rs##args = None ->
+ rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+ step (State s f sp (Mload NOTRAP chunk addr args dst :: c) rs m)
+ E0 (State s f sp c rs' m)
+ | exec_Mload_notrap2:
+ forall s f sp chunk addr args dst c rs m a rs',
+ eval_addressing ge sp addr rs##args = Some a ->
+ Mem.loadv chunk m a = None ->
+ rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+ step (State s f sp (Mload NOTRAP chunk addr args dst :: c) rs m)
E0 (State s f sp c rs' m)
| exec_Mstore:
forall s f sp chunk addr args src c rs m m' a rs',
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 7b382d05..0e3f2832 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -133,8 +133,8 @@ Definition transl_instr
end
| Lop op args res =>
Mop (transl_op fe op) args res :: k
- | Lload chunk addr args dst =>
- Mload chunk (transl_addr fe addr) args dst :: k
+ | Lload trap chunk addr args dst =>
+ Mload trap chunk (transl_addr fe addr) args dst :: k
| Lstore chunk addr args src =>
Mstore chunk (transl_addr fe addr) args src :: k
| Lcall sig ros =>
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index ade84e7b..cd9b3202 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -1008,12 +1008,17 @@ Definition transl_load_rrrXS (chunk: memory_chunk) (scale : Z)
do r <- ireg_of dst;
transl_memory_access2XS chunk (PLoadRRRXS (chunk2load chunk) r) scale args k.
-Definition transl_load (chunk: memory_chunk) (addr: addressing)
+Definition transl_load (trap : trapping_mode)
+ (chunk: memory_chunk) (addr: addressing)
(args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
- match addr with
- | Aindexed2XS scale => transl_load_rrrXS chunk scale args dst k
- | Aindexed2 => transl_load_rrr chunk addr args dst k
- | _ => transl_load_rro chunk addr args dst k
+ match trap with
+ | NOTRAP => Error(msg "Asmblockgen.transl_load NOTRAP TODO")
+ | TRAP =>
+ match addr with
+ | Aindexed2XS scale => transl_load_rrrXS chunk scale args dst k
+ | Aindexed2 => transl_load_rrr chunk addr args dst k
+ | _ => transl_load_rro chunk addr args dst k
+ end
end.
Definition chunk2store (chunk: memory_chunk) :=
@@ -1073,8 +1078,8 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c)
| MBop op args res =>
transl_op op args res k
- | MBload chunk addr args dst =>
- transl_load chunk addr args dst k
+ | MBload trap chunk addr args dst =>
+ transl_load trap chunk addr args dst k
| MBstore chunk addr args src =>
transl_store chunk addr args src k
end.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index e1e2b0b0..ce01041d 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1947,9 +1947,9 @@ Proof.
Qed.
Lemma transl_load_memory_access_ok:
- forall addr chunk args dst k c rs a v m,
+ forall addr trap chunk args dst k c rs a v m,
(match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) ->
- transl_load chunk addr args dst k = OK c ->
+ transl_load trap chunk addr args dst k = OK c ->
eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
Mem.loadv chunk m a = Some v ->
exists mk_instr rd,
@@ -1958,6 +1958,8 @@ Lemma transl_load_memory_access_ok:
/\ forall base ofs rs,
exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs.
Proof.
+ destruct trap.
+ { (* TRAP *)
intros until m. intros ADDR TR ? ?.
unfold transl_load in TR. destruct addr; try contradiction.
- monadInv TR. destruct chunk; ArgsInv; econstructor; (esplit; eauto).
@@ -1967,12 +1969,15 @@ Proof.
- monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split;
[ instantiate (1 := (PLoadRRO _ x)); simpl; reflexivity
| eauto ].
+ }
+ intros until m. intros ADDR TR ? ?.
+ monadInv TR.
Qed.
Lemma transl_load_memory_access2_ok:
- forall addr chunk args dst k c rs a v m,
+ forall addr trap chunk args dst k c rs a v m,
addr = Aindexed2 ->
- transl_load chunk addr args dst k = OK c ->
+ transl_load trap chunk addr args dst k = OK c ->
eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
Mem.loadv chunk m a = Some v ->
exists mk_instr mr0 mro rd ro,
@@ -1983,17 +1988,24 @@ Lemma transl_load_memory_access2_ok:
/\ forall base rs,
exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg chunk rs m rd base ro.
Proof.
+ destruct trap.
+ { (* TRAP *)
intros until m. intros ? TR ? ?.
unfold transl_load in TR. subst. monadInv TR. destruct chunk. all:
unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
[ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity
| rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRR _ x)); simpl; reflexivity
| eauto].
+ }
+ { (* NOTRAP *)
+ intros until m. intros ? TR ? ?.
+ unfold transl_load in TR. subst. monadInv TR.
+ }
Qed.
Lemma transl_load_memory_access2XS_ok:
- forall scale chunk args dst k c rs a v m,
- transl_load chunk (Aindexed2XS scale) args dst k = OK c ->
+ forall scale trap chunk args dst k c rs a v m,
+ transl_load trap chunk (Aindexed2XS scale) args dst k = OK c ->
eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a ->
Mem.loadv chunk m a = Some v ->
exists mk_instr mr0 mro rd ro,
@@ -2004,17 +2016,23 @@ Lemma transl_load_memory_access2XS_ok:
/\ forall base rs,
exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs chunk rs m rd base ro.
Proof.
+ destruct trap.
+ { (* TRAP *)
intros until m. intros TR ? ?.
unfold transl_load in TR. subst. monadInv TR. destruct chunk. all:
unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
[ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity
| rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRRXS _ x)); simpl; rewrite Heqb; eauto
| eauto].
+ }
+ { (* NOTRAP *)
+ intros until m. intros TR ? ?.
+ unfold transl_load in TR. subst. monadInv TR. }
Qed.
Lemma transl_load_correct:
- forall chunk addr args dst k c (rs: regset) m a v,
- transl_load chunk addr args dst k = OK c ->
+ forall trap chunk addr args dst k c (rs: regset) m a v,
+ transl_load trap chunk addr args dst k = OK c ->
eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
Mem.loadv chunk m a = Some v ->
exists rs',
diff --git a/mppa_k1c/lib/Machblock.v b/mppa_k1c/lib/Machblock.v
index 2759c49d..5a7f1782 100644
--- a/mppa_k1c/lib/Machblock.v
+++ b/mppa_k1c/lib/Machblock.v
@@ -20,7 +20,7 @@ Inductive basic_inst: Type :=
| MBsetstack: mreg -> ptrofs -> typ -> basic_inst
| MBgetparam: ptrofs -> typ -> mreg -> basic_inst
| MBop: operation -> list mreg -> mreg -> basic_inst
- | MBload: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst
+ | MBload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> basic_inst
| MBstore: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst
.
@@ -207,11 +207,22 @@ Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m:
rs' = ((undef_regs (destroyed_by_op op) rs)#res <- v) ->
basic_step s fb sp rs m (MBop op args res) rs' m
| exec_MBload:
- forall addr args a v rs' chunk dst,
+ forall addr args a v rs' trap chunk dst,
eval_addressing ge sp addr rs##args = Some a ->
Mem.loadv chunk m a = Some v ->
rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) ->
- basic_step s fb sp rs m (MBload chunk addr args dst) rs' m
+ basic_step s fb sp rs m (MBload trap chunk addr args dst) rs' m
+ | exec_MBload_notrap1:
+ forall addr args rs' chunk dst,
+ eval_addressing ge sp addr rs##args = None ->
+ rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+ basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m
+ | exec_MBload_notrap2:
+ forall addr args a rs' chunk dst,
+ eval_addressing ge sp addr rs##args = Some a ->
+ Mem.loadv chunk m a = None ->
+ rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) ->
+ basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m
| exec_MBstore:
forall chunk addr args src m' a rs',
eval_addressing ge sp addr rs##args = Some a ->
diff --git a/mppa_k1c/lib/Machblockgen.v b/mppa_k1c/lib/Machblockgen.v
index db48934e..a65b218f 100644
--- a/mppa_k1c/lib/Machblockgen.v
+++ b/mppa_k1c/lib/Machblockgen.v
@@ -33,7 +33,7 @@ Definition trans_inst (i:Mach.instruction) : Machblock_inst :=
| Msetstack src ofs ty => MB_basic (MBsetstack src ofs ty)
| Mgetparam ofs ty dst => MB_basic (MBgetparam ofs ty dst)
| Mop op args res => MB_basic (MBop op args res)
- | Mload chunk addr args dst => MB_basic (MBload chunk addr args dst)
+ | Mload trap chunk addr args dst=> MB_basic (MBload trap chunk addr args dst)
| Mstore chunk addr args src => MB_basic (MBstore chunk addr args src)
| Mlabel l => MB_label l
end.
diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v
index 9186e54a..77db094d 100644
--- a/mppa_k1c/lib/Machblockgenproof.v
+++ b/mppa_k1c/lib/Machblockgenproof.v
@@ -483,6 +483,10 @@ Proof.
unfold Genv.symbol_address; rewrite symbols_preserved; auto.
- eapply exec_MBload; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+ - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
+ unfold Genv.symbol_address; rewrite symbols_preserved; auto.
+ - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
+ unfold Genv.symbol_address; rewrite symbols_preserved; auto.
- eapply exec_MBstore; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto;
unfold Genv.symbol_address; rewrite symbols_preserved; auto.
Qed.
generated by cgit (git 2.34.1) at 2024-06-03 00:17:59 +0000