diff options
Diffstat (limited to 'backend/RTL.v')
| -rw-r--r-- | backend/RTL.v | 36 |
1 files changed, 25 insertions, 11 deletions
diff --git a/backend/RTL.v b/backend/RTL.v index 9599a24a..29a49311 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -43,11 +43,12 @@ Inductive instruction: Type := (** [Iop op args dest succ] performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest], and branches to [succ]. *) - | Iload: memory_chunk -> addressing -> list reg -> reg -> node -> instruction - (** [Iload chunk addr args dest succ] loads a [chunk] quantity from + | Iload: trapping_mode -> memory_chunk -> addressing -> list reg -> reg -> node -> instruction + (** [Iload trap chunk addr args dest succ] loads a [chunk] quantity from the address determined by the addressing mode [addr] and the values of the [args] registers, stores the quantity just read - into [dest], and branches to [succ]. *) + into [dest], and branches to [succ]. + If trap=NOTRAP, then failures lead to a default value written to [dest]. *) | Istore: memory_chunk -> addressing -> list reg -> reg -> node -> instruction (** [Istore chunk addr args src succ] stores the value of register [src] in the [chunk] quantity at the @@ -212,12 +213,25 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp pc rs m) E0 (State s f sp pc' (rs#res <- v) m) | exec_Iload: - forall s f sp pc rs m chunk addr args dst pc' a v, - (fn_code f)!pc = Some(Iload chunk addr args dst pc') -> + forall s f sp pc rs m trap chunk addr args dst pc' a v, + (fn_code f)!pc = Some(Iload trap chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> step (State s f sp pc rs m) E0 (State s f sp pc' (rs#dst <- v) m) + | exec_Iload_notrap1: + forall s f sp pc rs m chunk addr args dst pc', + (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) + | 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) | 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') -> @@ -299,8 +313,8 @@ Proof. Qed. Lemma exec_Iload': - forall s f sp pc rs m chunk addr args dst pc' rs' a v, - (fn_code f)!pc = Some(Iload chunk addr args dst pc') -> + forall s f sp pc rs m trap chunk addr args dst pc' rs' a v, + (fn_code f)!pc = Some(Iload trap chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> rs' = (rs#dst <- v) -> @@ -384,7 +398,7 @@ Definition successors_instr (i: instruction) : list node := match i with | Inop s => s :: nil | Iop op args res s => s :: nil - | Iload chunk addr args dst s => s :: nil + | Iload trap chunk addr args dst s => s :: nil | Istore chunk addr args src s => s :: nil | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil @@ -403,7 +417,7 @@ Definition instr_uses (i: instruction) : list reg := match i with | Inop s => nil | Iop op args res s => args - | Iload chunk addr args dst s => args + | Iload trap chunk addr args dst s => args | Istore chunk addr args src s => src :: args | Icall sig (inl r) args res s => r :: args | Icall sig (inr id) args res s => args @@ -422,7 +436,7 @@ Definition instr_defs (i: instruction) : option reg := match i with | Inop s => None | Iop op args res s => Some res - | Iload chunk addr args dst s => Some dst + | Iload trap chunk addr args dst s => Some dst | Istore chunk addr args src s => None | Icall sig ros args res s => Some res | Itailcall sig ros args => None @@ -462,7 +476,7 @@ Definition max_reg_instr (m: positive) (pc: node) (i: instruction) := match i with | Inop s => m | Iop op args res s => fold_left Pos.max args (Pos.max res m) - | Iload chunk addr args dst s => fold_left Pos.max args (Pos.max dst m) + | Iload trap chunk addr args dst s => fold_left Pos.max args (Pos.max dst m) | Istore chunk addr args src s => fold_left Pos.max args (Pos.max src m) | Icall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m)) | Icall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m) |