diff options
| -rw-r--r-- | backend/CSE3analysis.v | 27 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 34 |
2 files changed, 61 insertions, 0 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 18aa33b1..2d559413 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -4,6 +4,16 @@ Require Import Memory Registers Op RTL Maps CSE2deps. Require Import HashedSet. Require List. +Definition loadv_storev_compatible_type + (chunk : memory_chunk) (ty : typ) : bool := + match chunk, ty with + | Mint32, Tint + | Mint64, Tlong + | Mfloat32, Tsingle + | Mfloat64, Tfloat => true + | _, _ => false + end. + Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. Definition t := PSet.t. Definition eq (x : t) (y : t) := x = y. @@ -266,6 +276,23 @@ Section OPERATIONS. | None => oper1 dst op args rel end. + Definition store2 + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (src : reg) + (rel : RELATION.t) : RELATION.t := kill_mem rel. + + Definition store1 + (chunk : memory_chunk) (addr: addressing) (args : list reg) + (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. + End PER_NODE. Definition apply_instr no instr (rel : RELATION.t) : RB.t := diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index f805d2b8..7ef44c22 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -9,6 +9,26 @@ Require Import Registers Op RTL. Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet. Require Import Lia. +Theorem loadv_storev_really_same: + forall chunk: memory_chunk, + forall m1: mem, + forall addr v: val, + forall m2: mem, + forall ty : typ, + forall TYPE: Val.has_type v ty, + forall STORE: Mem.storev chunk m1 addr v = Some m2, + forall COMPATIBLE: loadv_storev_compatible_type chunk ty = true, + Mem.loadv chunk m2 addr = Some v. +Proof. + intros. + rewrite Mem.loadv_storev_same with (m1:=m1) (v:=v) by assumption. + f_equal. + destruct chunk; destruct ty; try discriminate. + all: destruct v; trivial; try contradiction. + all: unfold Val.load_result, Val.has_type in *. + all: destruct Archi.ptr64; trivial; discriminate. +Qed. + Lemma subst_args_notin : forall (rs : regset) dst v args, ~ In dst args -> @@ -622,4 +642,18 @@ Section SOUNDNESS. Qed. Hint Resolve oper_sound : cse3. + + Theorem store2_sound: + forall chunk addr args a src rel rs m m' v, + sem_rel rel rs m -> + eval_addressing genv sp addr (rs ## args) = Some a -> + Mem.storev chunk m a v = Some m' -> + sem_rel (store2 (ctx:=ctx) chunk addr args src rel) rs m'. + Proof. + unfold store2. + intros. + apply kill_mem_sound with (m:=m); auto. + Qed. + + Hint Resolve store2_sound : cse3. End SOUNDNESS. |