diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-04-10 12:05:55 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-04-10 12:05:55 +0200 |
| commit | 7505104944ce67229ac522665bc83c6cab5d113d (patch) | |
| tree | 2cde0e43c20c7452418bc7ea028fb30d3bc718c9 /backend/Lineartyping.v | |
| parent | d760be4554fa65f8fcfa9232f3d9ff7f9183f452 (diff) | |
| parent | 6e7c693e6cfe683b7a44c4f2a3420678fcdcc36f (diff) | |
| download | compcert-kvx-7505104944ce67229ac522665bc83c6cab5d113d.tar.gz compcert-kvx-7505104944ce67229ac522665bc83c6cab5d113d.zip | |
[BROKEN] Merge branch 'mppa-work' into mppa-RTLpathSE
Diffstat (limited to 'backend/Lineartyping.v')
| -rw-r--r-- | backend/Lineartyping.v | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 18594be8..22658fb7 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -76,7 +76,7 @@ Definition wt_instr (i: instruction) : bool := let (targs, tres) := type_of_operation op in subtype tres (mreg_type res) end - | Lload chunk addr args dst => + | Lload trap chunk addr args dst => subtype (type_of_chunk chunk) (mreg_type dst) | Ltailcall sg ros => zeq (size_arguments sg) 0 @@ -326,13 +326,28 @@ Local Opaque mreg_type. eapply Val.has_subtype; eauto. change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. red; intros; subst op. simpl in ISMOVE. - destruct args; try discriminate. destruct args; discriminate. + destruct args; try discriminate. destruct args; discriminate. + (* no longer needed apply wt_undef_regs; auto. *) - (* load *) simpl in *; InvBooleans. econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto. apply wt_undef_regs; auto. +- (* load notrap1 *) + simpl in *; InvBooleans. + econstructor; eauto. + apply wt_setreg. eapply Val.has_subtype; eauto. + unfold default_notrap_load_value. + constructor. + apply wt_undef_regs; auto. +- (* load notrap2 *) + simpl in *; InvBooleans. + econstructor; eauto. + apply wt_setreg. eapply Val.has_subtype; eauto. + unfold default_notrap_load_value. + constructor. + apply wt_undef_regs; auto. - (* store *) simpl in *; InvBooleans. econstructor. eauto. eauto. eauto. |