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 --- kvx/Asmblockdeps.v | 10 +++++----- kvx/Asmblockgenproof1.v | 8 ++++---- kvx/Asmblockprops.v | 4 ++-- kvx/Asmvliw.v | 11 +++++------ 4 files changed, 16 insertions(+), 17 deletions(-) (limited to 'kvx') 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. -- cgit