diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 09:35:58 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 09:35:58 +0200 |
commit | 66b506779c4889a18fb7a147f3649005cc40fe7e (patch) | |
tree | 7fa1332b855741e6c1a34843ec4c7dc9ebfcf325 /backend | |
parent | 8532805d67991f25242557124eed009960f6bc61 (diff) | |
parent | d10bc429a5c08a25471e3f65e328f5cee12e4542 (diff) | |
download | compcert-kvx-66b506779c4889a18fb7a147f3649005cc40fe7e.tar.gz compcert-kvx-66b506779c4889a18fb7a147f3649005cc40fe7e.zip |
Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licm
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CSE2.v | 6 | ||||
-rw-r--r-- | backend/CSE2proof.v | 5 | ||||
-rw-r--r-- | backend/CSE3.v | 2 | ||||
-rw-r--r-- | backend/CSE3analysis.v | 4 | ||||
-rw-r--r-- | backend/CSE3analysisproof.v | 8 | ||||
-rw-r--r-- | backend/CSE3proof.v | 5 |
6 files changed, 18 insertions, 12 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index 8e2307b0..00b1821e 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -276,10 +276,10 @@ Definition apply_external_call ef (rel : RELATION.t) : RELATION.t := | Some bf => rel | None => kill_mem rel end - | EF_malloc (* FIXME *) + | EF_malloc (* would need lessdef *) | EF_external _ _ | EF_vstore _ - | EF_free (* FIXME *) + | EF_free (* would need lessdef? *) | EF_memcpy _ _ (* FIXME *) | EF_inline_asm _ _ _ => kill_mem rel | _ => rel @@ -363,7 +363,7 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) | Some src => Iop Omove (src::nil) dst s end | Istore chunk addr args src s => - Istore chunk addr (subst_args fmap pc args) src s + Istore chunk addr (subst_args fmap pc args) (subst_arg fmap pc src) s | Icall sig ros args dst s => Icall sig ros (subst_args fmap pc args) dst s | Itailcall sig ros args => diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 9e0ad909..f9c7b400 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1527,7 +1527,10 @@ Proof. assert (eval_addressing tge sp addr rs ## args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Istore; eauto. - rewrite (subst_args_ok' sp m); assumption. + - rewrite (subst_args_ok' sp m) by assumption. + eassumption. + - rewrite (subst_arg_ok' sp m) by assumption. + eassumption. } constructor; auto. diff --git a/backend/CSE3.v b/backend/CSE3.v index 352cc895..2203ad14 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -57,7 +57,7 @@ Definition transf_instr (fmap : PMap.t RB.t) | Some src => Iop Omove (src::nil) dst s end | Istore chunk addr args src s => - Istore chunk addr (subst_args fmap pc args) src s + Istore chunk addr (subst_args fmap pc args) (subst_arg fmap pc src) s | Icall sig ros args dst s => Icall sig ros (subst_args fmap pc args) dst s | Itailcall sig ros args => diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index bc5d3244..d3d1c043 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -323,7 +323,7 @@ Section OPERATIONS. (chunk : memory_chunk) (addr: addressing) (args : list reg) (src : reg) (ty: typ) (rel : RELATION.t) : RELATION.t := - store1 chunk addr (forward_move_l rel args) src ty rel. + store1 chunk addr (forward_move_l rel args) (forward_move rel src) ty rel. Definition kill_builtin_res res rel := match res with @@ -354,7 +354,7 @@ Section OPERATIONS. | Icond _ _ _ _ _ | Ijumptable _ _ => Some rel | Istore chunk addr args src _ => - Some (store chunk addr args src (tenv src) rel) + Some (store chunk addr args src (tenv (forward_move rel src)) rel) | Iop op args dst _ => Some (oper dst (SOp op) args rel) | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel) | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel)) diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index f4ec7a10..e1e9f6cc 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -848,14 +848,14 @@ Section SOUNDNESS. Qed. Hint Resolve store1_sound : cse3. - + Theorem store_sound: forall no chunk addr args a src rel tenv rs m m', sem_rel rel rs m -> wt_regset tenv rs -> eval_addressing genv sp addr (rs ## args) = Some a -> Mem.storev chunk m a (rs#src) = Some m' -> - sem_rel (store (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'. + sem_rel (store (ctx:=ctx) no chunk addr args src (tenv (forward_move (ctx:=ctx) rel src)) rel) rs m'. Proof. unfold store. intros until m'. @@ -863,8 +863,8 @@ Section SOUNDNESS. rewrite <- forward_move_l_sound with (rel:=rel) (m:=m) in ADDR by trivial. rewrite <- forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. apply store1_sound with (a := a) (m := m); trivial. - rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. - assumption. + (* rewrite forward_move_sound with (rel:=rel) (m:=m) in STORE by trivial. + assumption. *) Qed. Hint Resolve store_sound : cse3. diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 53872e62..ccbfd198 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -689,10 +689,13 @@ Proof. - (* Istore *) exists (State ts tf sp pc' rs m'). split. - + eapply exec_Istore with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption. + + eapply exec_Istore with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)) + (src := (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc src)) ; try eassumption. * TR_AT. reflexivity. * rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. rewrite eval_addressing_preserved with (ge1 := ge) by exact symbols_preserved. + eassumption. + * rewrite subst_arg_ok with (sp:=sp) (m:=m) by trivial. assumption. + econstructor; eauto. IND_STEP. |