aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/CSE2proof.v4
-rw-r--r--backend/CSE3analysisproof.v2
-rw-r--r--backend/CSEdomain.v4
-rw-r--r--backend/CSEproof.v5
-rw-r--r--backend/Deadcodeproof.v2
-rw-r--r--backend/LTL.v4
-rw-r--r--backend/Linear.v4
-rw-r--r--backend/Lineartyping.v2
-rw-r--r--backend/Mach.v4
-rw-r--r--backend/RTL.v4
-rw-r--r--backend/RTLtyping.v2
-rw-r--r--backend/Tailcallproof.v4
-rw-r--r--backend/ValueAnalysis.v2
-rw-r--r--common/Memory.v2
-rw-r--r--kvx/Asmblockdeps.v10
-rw-r--r--kvx/Asmblockgenproof1.v8
-rw-r--r--kvx/Asmblockprops.v4
-rw-r--r--kvx/Asmvliw.v11
-rw-r--r--scheduling/RTLpath.v2
-rw-r--r--scheduling/RTLpathSE_theory.v4
-rw-r--r--scheduling/postpass_lib/Machblock.v4
21 files changed, 39 insertions, 49 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 49dbd409..252240c9 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -1399,7 +1399,7 @@ Proof.
2: discriminate.
econstructor; split.
{
- eapply exec_Iop with (v := (default_notrap_load_value chunk)); eauto.
+ eapply exec_Iop with (v := Vundef); eauto.
simpl.
rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
{
@@ -1472,7 +1472,7 @@ Proof.
2: discriminate.
econstructor; split.
{
- eapply exec_Iop with (v := (default_notrap_load_value chunk)); eauto.
+ eapply exec_Iop with (v := Vundef); eauto.
simpl.
rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
{
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index d53cf604..382c9f4c 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -502,7 +502,7 @@ Section SOUNDNESS.
end
with
| Some dat => v' = dat
- | None => v' = default_notrap_load_value chunk
+ | None => v' = Vundef
end
end.
diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v
index f78e1d25..9641d012 100644
--- a/backend/CSEdomain.v
+++ b/backend/CSEdomain.v
@@ -113,12 +113,12 @@ Inductive rhs_eval_to (valu: valuation) (ge: genv) (sp: val) (m: mem):
(* | load_notrap1_eval_to: forall chunk addr vl,
eval_addressing ge sp addr (map valu vl) = None ->
rhs_eval_to valu ge sp m (Load NOTRAP chunk addr vl)
- (default_notrap_load_value chunk)
+ Vundef
| load_notrap2_eval_to: forall chunk addr vl a,
eval_addressing ge sp addr (map valu vl) = Some a ->
Mem.loadv chunk m a = None ->
rhs_eval_to valu ge sp m (Load NOTRAP chunk addr vl)
- (default_notrap_load_value chunk) *).
+ Vundef *).
Inductive equation_holds (valu: valuation) (ge: genv) (sp: val) (m: mem):
equation -> Prop :=
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index cf51f5a2..556b44b3 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -402,7 +402,7 @@ Lemma add_load_holds_none1:
forall valu1 ge sp rs m n addr (args: list reg) chunk dst,
numbering_holds valu1 ge sp rs m n ->
eval_addressing ge sp addr rs##args = None ->
- exists valu2, numbering_holds valu2 ge sp (rs#dst <- (default_notrap_load_value chunk)) m (add_load n dst chunk addr args).
+ exists valu2, numbering_holds valu2 ge sp (rs#dst <- Vundef) m (add_load n dst chunk addr args).
Proof.
unfold add_load; intros.
destruct (valnum_regs n args) as [n1 vl] eqn:VN.
@@ -418,7 +418,7 @@ Lemma add_load_holds_none2:
numbering_holds valu1 ge sp rs m n ->
eval_addressing ge sp addr rs##args = Some a ->
Mem.loadv chunk m a = None ->
- exists valu2, numbering_holds valu2 ge sp (rs#dst <- (default_notrap_load_value chunk)) m (add_load n dst NOTRAP chunk addr args).
+ exists valu2, numbering_holds valu2 ge sp (rs#dst <- Vundef) m (add_load n dst NOTRAP chunk addr args).
Proof.
unfold add_load; intros.
destruct (valnum_regs n args) as [n1 vl] eqn:VN.
@@ -1210,7 +1210,6 @@ Proof.
exists valu1.
apply set_unknown_holds.
assumption.
- unfold default_notrap_load_value.
apply set_reg_lessdef; eauto.
}
{
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index b51d6cce..be20af0b 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -845,7 +845,6 @@ Ltac UseTransfer :=
eapply match_succ_states; eauto. simpl; auto.
apply eagree_update; auto.
rewrite is_int_zero_sound by auto.
- unfold default_notrap_load_value.
constructor.
+ (* preserved *)
exploit eval_addressing_lessdef_none. eapply add_needs_all_lessdef; eauto. eassumption.
@@ -878,7 +877,6 @@ Ltac UseTransfer :=
eapply match_succ_states; eauto. simpl; auto.
apply eagree_update; auto.
rewrite is_int_zero_sound by auto.
- unfold default_notrap_load_value.
constructor.
+ (* preserved *)
exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto.
diff --git a/backend/LTL.v b/backend/LTL.v
index 3edd60a2..a382ef0e 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -217,14 +217,14 @@ Inductive step: state -> trace -> state -> Prop :=
E0 (Block s f sp bb rs' m)
| exec_Lload_notrap1: forall s f sp chunk addr args dst bb rs m rs',
eval_addressing ge sp addr (reglist rs args) = None ->
- rs' = Locmap.set (R dst) (default_notrap_load_value chunk)
+ rs' = Locmap.set (R dst) Vundef
(undef_regs (destroyed_by_load chunk addr) rs) ->
step (Block s f sp (Lload NOTRAP chunk addr args dst :: bb) rs m)
E0 (Block s f sp bb rs' m)
| exec_Lload_notrap2: forall s f sp chunk addr args dst bb rs m a rs',
eval_addressing ge sp addr (reglist rs args) = Some a ->
Mem.loadv chunk m a = None ->
- rs' = Locmap.set (R dst) (default_notrap_load_value chunk)
+ rs' = Locmap.set (R dst) Vundef
(undef_regs (destroyed_by_load chunk addr) rs) ->
step (Block s f sp (Lload NOTRAP chunk addr args dst :: bb) rs m)
E0 (Block s f sp bb rs' m)
diff --git a/backend/Linear.v b/backend/Linear.v
index 1443f795..cb11f7dc 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -170,7 +170,7 @@ Inductive step: state -> trace -> state -> Prop :=
forall s f sp chunk addr args dst b rs m rs',
eval_addressing ge sp addr (reglist rs args) = None ->
rs' = Locmap.set (R dst)
- (default_notrap_load_value chunk)
+ Vundef
(undef_regs (destroyed_by_load chunk addr) rs) ->
step (State s f sp (Lload NOTRAP chunk addr args dst :: b) rs m)
E0 (State s f sp b rs' m)
@@ -179,7 +179,7 @@ Inductive step: state -> trace -> state -> Prop :=
eval_addressing ge sp addr (reglist rs args) = Some a ->
Mem.loadv chunk m a = None ->
rs' = Locmap.set (R dst)
- (default_notrap_load_value chunk)
+ Vundef
(undef_regs (destroyed_by_load chunk addr) rs) ->
step (State s f sp (Lload NOTRAP chunk addr args dst :: b) rs m)
E0 (State s f sp b rs' m)
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 22658fb7..cf903aad 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -338,14 +338,12 @@ Local Opaque mreg_type.
simpl in *; InvBooleans.
econstructor; eauto.
apply wt_setreg. eapply Val.has_subtype; eauto.
- unfold default_notrap_load_value.
constructor.
apply wt_undef_regs; auto.
- (* load notrap2 *)
simpl in *; InvBooleans.
econstructor; eauto.
apply wt_setreg. eapply Val.has_subtype; eauto.
- unfold default_notrap_load_value.
constructor.
apply wt_undef_regs; auto.
- (* store *)
diff --git a/backend/Mach.v b/backend/Mach.v
index 1c6fdb18..2cfd738d 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -330,14 +330,14 @@ Inductive step: state -> trace -> state -> Prop :=
| 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)) ->
+ rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- Vundef) ->
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)) ->
+ rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- Vundef) ->
step (State s f sp (Mload NOTRAP chunk addr args dst :: c) rs m)
E0 (State s f sp c rs' m)
| exec_Mstore:
diff --git a/backend/RTL.v b/backend/RTL.v
index 31b5cf99..fe350adf 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -225,14 +225,14 @@ Inductive step: state -> trace -> state -> Prop :=
(fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') ->
eval_addressing ge sp addr rs##args = None ->
step (State s f sp pc rs m)
- E0 (State s f sp pc' (rs#dst <- (default_notrap_load_value chunk)) m)
+ E0 (State s f sp pc' (rs#dst <- Vundef) m)
| exec_Iload_notrap2:
forall s f sp pc rs m chunk addr args dst pc' a,
(fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') ->
eval_addressing ge sp addr rs##args = Some a ->
Mem.loadv chunk m a = None->
step (State s f sp pc rs m)
- E0 (State s f sp pc' (rs#dst <- (default_notrap_load_value chunk)) m)
+ E0 (State s f sp pc' (rs#dst <- Vundef) m)
| exec_Istore:
forall s f sp pc rs m chunk addr args src pc' a m',
(fn_code f)!pc = Some(Istore chunk addr args src pc') ->
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 15ed6d8a..6048f895 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -858,7 +858,7 @@ Lemma wt_exec_Iload_notrap:
forall env f chunk addr args dst s rs,
wt_instr f env (Iload NOTRAP chunk addr args dst s) ->
wt_regset env rs ->
- wt_regset env (rs#dst <- (default_notrap_load_value chunk)).
+ wt_regset env (rs#dst <- Vundef).
Proof.
intros.
eapply wt_regset_assign; eauto. simpl. trivial.
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 80a68327..39fc10fb 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -440,7 +440,7 @@ Proof.
TransfInstr.
assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
left.
- exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- (default_notrap_load_value chunk)) m'); split.
+ exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split.
eapply exec_Iload_notrap1.
eassumption.
eapply eval_addressing_lessdef_none. eassumption.
@@ -465,7 +465,7 @@ Proof.
exact symbols_preserved.
assumption.
econstructor; eauto. apply set_reg_lessdef; auto.
- + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- (default_notrap_load_value chunk)) m'); split.
+ + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split.
eapply exec_Iload_notrap2. eassumption.
erewrite eval_addressing_preserved.
eassumption.
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 561e94c9..e20edff7 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1287,13 +1287,11 @@ Proof.
eapply sound_succ_state; eauto. simpl; auto.
unfold transfer; rewrite H. eauto.
apply ematch_update; auto.
- unfold default_notrap_load_value.
constructor.
- (* load notrap2 *)
eapply sound_succ_state; eauto. simpl; auto.
unfold transfer; rewrite H. eauto.
apply ematch_update; auto.
- unfold default_notrap_load_value.
constructor.
- (* store *)
exploit eval_static_addressing_sound; eauto with va. intros VMADDR.
diff --git a/common/Memory.v b/common/Memory.v
index bf8ca083..ff17efb0 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -41,8 +41,6 @@ Require Export Memdata.
Require Export Memtype.
Require Import Lia.
-Definition default_notrap_load_value (chunk : memory_chunk) := Vundef.
-
(* To avoid useless definitions of inductors in extracted code. *)
Local Unset Elimination Schemes.
diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v
index b6d18c3e..a9786e0a 100644
--- a/kvx/Asmblockdeps.v
+++ b/kvx/Asmblockdeps.v
@@ -164,17 +164,17 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
| _, _ => None
end.
-Definition exec_incorrect_load trap chunk :=
+Definition exec_incorrect_load trap :=
match trap with
| TRAP => None
- | NOTRAP => Some (Val (concrete_default_notrap_load_value chunk))
+ | NOTRAP => Some (Val Vundef)
end.
Definition exec_load_deps_offset (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) :=
let (ge, fn) := Ge in
match (eval_offset ofs) with
| OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with
- | None => exec_incorrect_load trap chunk
+ | None => exec_incorrect_load trap
| Some vl => Some (Val vl)
end
| _ => None
@@ -182,13 +182,13 @@ Definition exec_load_deps_offset (trap: trapping_mode) (chunk: memory_chunk) (m:
Definition exec_load_deps_reg (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v vo: val) :=
match Mem.loadv chunk m (Val.addl v vo) with
- | None => exec_incorrect_load trap chunk
+ | None => exec_incorrect_load trap
| Some vl => Some (Val vl)
end.
Definition exec_load_deps_regxs (trap: trapping_mode) (chunk: memory_chunk) (m: mem) (v vo: val) :=
match Mem.loadv chunk m (Val.addl v (Val.shll vo (scale_of_chunk chunk))) with
- | None => exec_incorrect_load trap chunk
+ | None => exec_incorrect_load trap
| Some vl => Some (Val vl)
end.
diff --git a/kvx/Asmblockgenproof1.v b/kvx/Asmblockgenproof1.v
index a65bd5bc..259c4f9c 100644
--- a/kvx/Asmblockgenproof1.v
+++ b/kvx/Asmblockgenproof1.v
@@ -1914,7 +1914,7 @@ Lemma transl_load_access2_correct_notrap2:
Mem.loadv chunk m v = None ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
- /\ rs'#rd = concrete_default_notrap_load_value chunk
+ /\ rs'#rd = Vundef
/\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
Proof.
intros until ro; intros ARGS IREGE INSTR TR EV LOAD.
@@ -1963,7 +1963,7 @@ Lemma transl_load_access2XS_correct_notrap2:
Mem.loadv chunk m v = None ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
- /\ rs'#rd = concrete_default_notrap_load_value chunk
+ /\ rs'#rd = Vundef
/\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
Proof.
intros until ro; intros ARGS IREGE INSTR TR EV LOAD.
@@ -2008,7 +2008,7 @@ Lemma transl_load_access_correct_notrap2:
Mem.loadv chunk m v = None ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
- /\ rs'#rd = concrete_default_notrap_load_value chunk
+ /\ rs'#rd = Vundef
/\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
Proof.
intros until v; intros INSTR TR EV LOAD.
@@ -2185,7 +2185,7 @@ Lemma transl_load_correct_notrap2:
Mem.loadv chunk m a = None ->
exists rs',
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
- /\ rs'#(preg_of dst) = (concrete_default_notrap_load_value chunk)
+ /\ rs'#(preg_of dst) = Vundef
/\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
intros until a; intros TR EV LOAD. destruct addr.
diff --git a/kvx/Asmblockprops.v b/kvx/Asmblockprops.v
index c3929be5..a732d29b 100644
--- a/kvx/Asmblockprops.v
+++ b/kvx/Asmblockprops.v
@@ -96,9 +96,9 @@ Theorem exec_basic_instr_pc:
Proof.
intros. destruct b; try destruct i; try destruct i.
all: try (inv H; Simpl).
- 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
+ 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; inv H1; Simpl; fail.
- 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
+ 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; inv H1; Simpl; fail.
{ (* PLoadQRRO *)
unfold parexec_load_q_offset in H1.
diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v
index 304e45a8..45b230e6 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -313,7 +313,6 @@ Inductive cf_instruction : Type :=
.
(** *** Loads *)
-Definition concrete_default_notrap_load_value (chunk : memory_chunk) := Vundef.
(* What follows was the original spec, but is subtly incorrect.
Our definition of the assembly-level memory model is already an abstraction of the real world.
@@ -1174,16 +1173,16 @@ Definition eval_offset (ofs: offset) : res ptrofs := OK ofs.
(** *** load/store instructions *)
-Definition parexec_incorrect_load trap chunk d rsw mw :=
+Definition parexec_incorrect_load trap d rsw mw :=
match trap with
| TRAP => Stuck
- | NOTRAP => Next (rsw#d <- (concrete_default_notrap_load_value chunk)) mw
+ | NOTRAP => Next (rsw#d <- Vundef) mw
end.
Definition parexec_load_offset (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) :=
match (eval_offset ofs) with
| OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with
- | None => parexec_incorrect_load trap chunk d rsw mw
+ | None => parexec_incorrect_load trap d rsw mw
| Some v => Next (rsw#d <- v) mw
end
| _ => Stuck
@@ -1230,13 +1229,13 @@ Definition parexec_load_o_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_o) (a
Definition parexec_load_reg (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
match Mem.loadv chunk mr (Val.addl (rsr a) (rsr ro)) with
- | None => parexec_incorrect_load trap chunk d rsw mw
+ | None => parexec_incorrect_load trap d rsw mw
| Some v => Next (rsw#d <- v) mw
end.
Definition parexec_load_regxs (trap: trapping_mode) (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with
- | None => parexec_incorrect_load trap chunk d rsw mw
+ | None => parexec_incorrect_load trap d rsw mw
| Some v => Next (rsw#d <- v) mw
end.
diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v
index a4fce97e..b29a7759 100644
--- a/scheduling/RTLpath.v
+++ b/scheduling/RTLpath.v
@@ -156,7 +156,7 @@ Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem)
SOME v <- Mem.loadv chunk m a IN
Some (mk_istate true pc' (rs#dst <- v) m)
| Iload NOTRAP chunk addr args dst pc' =>
- let default_state := mk_istate true pc' rs#dst <- (default_notrap_load_value chunk) m in
+ let default_state := mk_istate true pc' rs#dst <- Vundef m in
match (eval_addressing ge sp addr rs##args) with
| None => Some default_state
| Some a => match (Mem.loadv chunk m a) with
diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v
index aa8db342..2a791feb 100644
--- a/scheduling/RTLpathSE_theory.v
+++ b/scheduling/RTLpathSE_theory.v
@@ -87,11 +87,11 @@ Fixpoint seval_sval (ge: RTL.genv) (sp:val) (sv: sval) (rs0: regset) (m0: mem):
| NOTRAP =>
SOME args <- seval_list_sval ge sp lsv rs0 m0 IN
match (eval_addressing ge sp addr args) with
- | None => Some (default_notrap_load_value chunk)
+ | None => Some Vundef
| Some a =>
SOME m <- seval_smem ge sp sm rs0 m0 IN
match (Mem.loadv chunk m a) with
- | None => Some (default_notrap_load_value chunk)
+ | None => Some Vundef
| Some val => Some val
end
end
diff --git a/scheduling/postpass_lib/Machblock.v b/scheduling/postpass_lib/Machblock.v
index c8eadbd7..b588cca8 100644
--- a/scheduling/postpass_lib/Machblock.v
+++ b/scheduling/postpass_lib/Machblock.v
@@ -237,13 +237,13 @@ Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (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)) ->
+ rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- Vundef) ->
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)) ->
+ rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- Vundef) ->
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',
generated by cgit (git 2.34.1) at 2024-05-19 07:15:53 +0000