From 5798f56b8a8630e43dbed84a824811a5626a1503 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 18 Jun 2021 18:35:50 +0200 Subject: Replacing default notrap load value by Vundef everywhere --- backend/CSE2proof.v | 4 ++-- backend/CSE3analysisproof.v | 2 +- backend/CSEdomain.v | 4 ++-- backend/CSEproof.v | 5 ++--- backend/Deadcodeproof.v | 2 -- backend/LTL.v | 4 ++-- backend/Linear.v | 4 ++-- backend/Lineartyping.v | 2 -- backend/Mach.v | 4 ++-- backend/RTL.v | 4 ++-- backend/RTLtyping.v | 2 +- backend/Tailcallproof.v | 4 ++-- backend/ValueAnalysis.v | 2 -- common/Memory.v | 2 -- kvx/Asmblockdeps.v | 10 +++++----- kvx/Asmblockgenproof1.v | 8 ++++---- kvx/Asmblockprops.v | 4 ++-- kvx/Asmvliw.v | 11 +++++------ scheduling/RTLpath.v | 2 +- scheduling/RTLpathSE_theory.v | 4 ++-- scheduling/postpass_lib/Machblock.v | 4 ++-- 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', -- cgit