diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-07 19:58:02 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-07 19:58:02 +0200 |
| commit | 08b39b2025951a9655939c1377f6e53b346c6821 (patch) | |
| tree | f6a64ddf1f59404a58405ffdee06d476b7b28fb5 /scheduling/BTL.v | |
| parent | 89aececb825a04dbc1982ec9e61331ef3272c228 (diff) | |
| download | compcert-kvx-08b39b2025951a9655939c1377f6e53b346c6821.tar.gz compcert-kvx-08b39b2025951a9655939c1377f6e53b346c6821.zip | |
Some advance in proof and NOTRAP loads fix
Diffstat (limited to 'scheduling/BTL.v')
| -rw-r--r-- | scheduling/BTL.v | 13 |
1 files changed, 7 insertions, 6 deletions
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. |