From 08b39b2025951a9655939c1377f6e53b346c6821 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 7 May 2021 19:58:02 +0200 Subject: Some advance in proof and NOTRAP loads fix --- scheduling/BTL.v | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index fb67d150..c8dfa0af 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -400,9 +400,9 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i | mib_op isfst pc pc' op lr r: cfg!pc = Some (Iop op lr r pc') -> match_iblock dupmap cfg isfst pc (Bop op lr r) (Some pc') - | mib_load isfst pc pc' tm m a lr r: - cfg!pc = Some (Iload tm m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bload tm m a lr r) (Some pc') + | mib_load isfst pc pc' m a lr r: + cfg!pc = Some (Iload TRAP m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r) (Some pc') | mib_store isfst pc pc' m a lr r: cfg!pc = Some (Istore m a lr r pc') -> match_iblock dupmap cfg isfst pc (Bstore m a lr r) (Some pc') @@ -581,7 +581,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | Bload tm m a lr r => match cfg!pc with | Some (Iload tm' m' a' lr' r' pc') => - if (trapping_mode_eq tm tm') then + if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then if (chunk_eq m m') then if (eq_addressing a a') then if (list_eq_dec Pos.eq_dec lr lr') then @@ -591,7 +591,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "verify_block: different lr in Bload") else Error (msg "verify_block: different addressing in Bload") else Error (msg "verify_block: different mchunk in Bload") - else Error (msg "verify_block: different trapping_mode in Bload") + else Error (msg "verify_block: NOTRAP trapping_mode unsupported in Bload") | _ => Error (msg "verify_block: incorrect cfg Bload") end | Bstore m a lr r => @@ -691,7 +691,8 @@ Proof. constructor; assumption. - (* Bload *) destruct i; try discriminate. - destruct (trapping_mode_eq _ _); try discriminate. + do 2 (destruct (trapping_mode_eq _ _); try discriminate). + simpl in H. destruct (chunk_eq _ _); try discriminate. destruct (eq_addressing _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. -- cgit