diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 08:17:40 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-03 08:17:40 +0100 |
| commit | 1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68 (patch) | |
| tree | 210ffc156c83f04fb0c61a40b4f9037d7ba8a7e1 /backend/RTLtyping.v | |
| parent | 222c9047d61961db9c6b19fed5ca49829223fd33 (diff) | |
| parent | 12be46d59a2483a10d77fa8ee67f7e0ca1bd702f (diff) | |
| download | compcert-kvx-1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68.tar.gz compcert-kvx-1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68.zip | |
Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
Diffstat (limited to 'backend/RTLtyping.v')
| -rw-r--r-- | backend/RTLtyping.v | 26 |
1 files changed, 20 insertions, 6 deletions
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 5b8646ea..857f2211 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -104,11 +104,11 @@ Inductive wt_instr : instruction -> Prop := valid_successor s -> wt_instr (Iop op args res s) | wt_Iload: - forall chunk addr args dst s, + forall trap chunk addr args dst s, map env args = type_of_addressing addr -> env dst = type_of_chunk chunk -> valid_successor s -> - wt_instr (Iload chunk addr args dst s) + wt_instr (Iload trap chunk addr args dst s) | wt_Istore: forall chunk addr args src s, map env args = type_of_addressing addr -> @@ -283,7 +283,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := else (let (targs, tres) := type_of_operation op in do e1 <- S.set_list e args targs; S.set e1 res tres) - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => do x <- check_successor s; do e1 <- S.set_list e args (type_of_addressing addr); S.set e1 dst (type_of_chunk chunk) @@ -844,14 +844,24 @@ Proof. Qed. Lemma wt_exec_Iload: - forall env f chunk addr args dst s m a v rs, - wt_instr f env (Iload chunk addr args dst s) -> + forall env f trap chunk addr args dst s m a v rs, + wt_instr f env (Iload trap chunk addr args dst s) -> Mem.loadv chunk m a = Some v -> wt_regset env rs -> wt_regset env (rs#dst <- v). Proof. intros. destruct a; simpl in H0; try discriminate. inv H. - eapply wt_regset_assign; eauto. rewrite H8; eapply Mem.load_type; eauto. + eapply wt_regset_assign; eauto. rewrite H9; eapply Mem.load_type; eauto. +Qed. + +Lemma wt_exec_Iload_notrap: + forall env f chunk addr args dst s rs, + wt_instr f env (Iload NOTRAP chunk addr args dst s) -> + wt_regset env rs -> + wt_regset env (rs#dst <- (default_notrap_load_value chunk)). +Proof. + intros. + eapply wt_regset_assign; eauto. simpl. trivial. Qed. Lemma wt_exec_Ibuiltin: @@ -933,6 +943,10 @@ Proof. econstructor; eauto. eapply wt_exec_Iop; eauto. (* Iload *) econstructor; eauto. eapply wt_exec_Iload; eauto. + (* Iload notrap1*) + econstructor; eauto. eapply wt_exec_Iload_notrap; eauto. + (* Iload notrap2*) + econstructor; eauto. eapply wt_exec_Iload_notrap; eauto. (* Istore *) econstructor; eauto. (* Icall *) |