diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 11:37:59 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 11:37:59 +0100 |
commit | a3be6358778bb02b03b62486a60b9fd9ef1f1c04 (patch) | |
tree | a88730ada5a8c405c8e322a13486caeb07cbd8d9 /backend | |
parent | ee3bc59771eb50a8e39dc1db21e5439ce992e630 (diff) | |
download | compcert-kvx-a3be6358778bb02b03b62486a60b9fd9ef1f1c04.tar.gz compcert-kvx-a3be6358778bb02b03b62486a60b9fd9ef1f1c04.zip |
more lemmas
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CSE3analysis.v | 15 | ||||
-rw-r--r-- | backend/CSE3analysisproof.v | 38 |
2 files changed, 45 insertions, 8 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 2d559413..a85cd493 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -286,12 +286,15 @@ Section OPERATIONS. (src : reg) (ty: typ) (rel : RELATION.t) : RELATION.t := let rel' := store2 chunk addr args src rel in - match eq_find {| eq_lhs := src; - eq_op := SLoad chunk addr; - eq_args:= args |} with - | Some id => PSet.add id rel' - | None => rel' - end. + if loadv_storev_compatible_type chunk ty + then + match eq_find {| eq_lhs := src; + eq_op := SLoad chunk addr; + eq_args:= args |} with + | Some id => PSet.add id rel' + | None => rel' + end + else rel'. End PER_NODE. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 7ef44c22..f5dd7bf9 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -7,6 +7,7 @@ Require Import Globalenvs Values. Require Import Linking Values Memory Globalenvs Events Smallstep. Require Import Registers Op RTL. Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet. +Require Import RTLtyping. Require Import Lia. Theorem loadv_storev_really_same: @@ -644,10 +645,10 @@ Section SOUNDNESS. Hint Resolve oper_sound : cse3. Theorem store2_sound: - forall chunk addr args a src rel rs m m' v, + forall chunk addr args a src rel rs m m', sem_rel rel rs m -> eval_addressing genv sp addr (rs ## args) = Some a -> - Mem.storev chunk m a v = Some m' -> + Mem.storev chunk m a (rs # src) = Some m' -> sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m'. Proof. unfold store2. @@ -656,4 +657,37 @@ Section SOUNDNESS. Qed. Hint Resolve store2_sound : cse3. + + Theorem store1_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 (store1 (ctx:=ctx) no chunk addr args src (tenv src) rel) rs m'. + Proof. + unfold store1. + intros until m'. + intros REL WT ADDR STORE. + assert (sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m') as REL' by eauto with cse3. + destruct loadv_storev_compatible_type eqn:COMPATIBLE. + 2: auto; fail. + destruct eq_find as [eq_id | ] eqn:FIND. + 2: auto; fail. + intros i eq CONTAINS CATALOG. + destruct (peq i eq_id). + { subst i. + rewrite eq_find_sound with (no:=no) (eq0:={| eq_lhs := src; eq_op := SLoad chunk addr; eq_args := args |}) in CATALOG; trivial. + inv CATALOG. + unfold sem_eq. + simpl. + rewrite ADDR. + rewrite loadv_storev_really_same with (m1:=m) (v:=rs#src) (ty:=(tenv src)); trivial. + } + unfold sem_rel in REL'. + rewrite PSet.gaddo in CONTAINS by congruence. + eauto. + Qed. + + Hint Resolve store2_sound : cse3. End SOUNDNESS. |