diff options
Diffstat (limited to 'backend/RTL.v')
| -rw-r--r-- | backend/RTL.v | 30 |
1 files changed, 14 insertions, 16 deletions
diff --git a/backend/RTL.v b/backend/RTL.v index fe350adf..b43fd377 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -181,6 +181,18 @@ Inductive state : Type := (m: mem), (**r memory state *) state. +Inductive has_loaded {F V: Type} (genv: Genv.t F V) sp rs m chunk addr args v: trapping_mode -> Prop := + | has_loaded_normal a trap + (EVAL: eval_addressing genv sp addr rs##args = Some a) + (LOAD: Mem.loadv chunk m a = Some v) + : has_loaded genv sp rs m chunk addr args v trap + | has_loaded_default + (LOAD: forall a, eval_addressing genv sp addr rs##args = Some a -> Mem.loadv chunk m a = None) + (DEFAULT: v = Vundef) + : has_loaded genv sp rs m chunk addr args v NOTRAP + . +Local Hint Constructors has_loaded: core. + Section RELSEM. Variable ge: genv. @@ -214,25 +226,11 @@ 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 trap chunk addr args dst pc' a v, + forall s f sp pc rs m trap chunk addr args dst pc' 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 -> + has_loaded ge sp rs m chunk addr args v trap -> 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 <- 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 <- 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') -> |