diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-27 17:28:10 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-27 17:28:10 +0100 |
commit | 63942e04b0fcb84d54f066122c31ca4c3aa99ad4 (patch) | |
tree | ccdced72b87622e25e113352557c1703077ac3bf /aarch64 | |
parent | 2e1912abc2d1f20f50d98c862c5ce9a961a3f3bf (diff) | |
parent | b8647d11c1af9bfe19fd8be33f8e88f92de77888 (diff) | |
download | compcert-kvx-63942e04b0fcb84d54f066122c31ca4c3aa99ad4.tar.gz compcert-kvx-63942e04b0fcb84d54f066122c31ca4c3aa99ad4.zip |
Merge remote-tracking branch 'origin/kvx-work' into aarch64-postpass
Diffstat (limited to 'aarch64')
-rw-r--r-- | aarch64/CSE2deps.v | 5 | ||||
-rw-r--r-- | aarch64/CSE2depsproof.v | 75 | ||||
-rw-r--r-- | aarch64/Op.v | 14 |
3 files changed, 90 insertions, 4 deletions
diff --git a/aarch64/CSE2deps.v b/aarch64/CSE2deps.v index a23e41a8..d5c7ee0f 100644 --- a/aarch64/CSE2deps.v +++ b/aarch64/CSE2deps.v @@ -28,5 +28,8 @@ Definition may_overlap chunk addr args chunk' addr' args' := (base :: nil), (base' :: nil) => if peq base base' then negb (can_swap_accesses_ofs (Int64.unsigned ofs') chunk' (Int64.unsigned ofs) chunk) - else true | _, _, _, _ => true + else true + | (Ainstack ofs), (Ainstack ofs'), _, _ => + negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk) + | _, _, _, _ => true end. diff --git a/aarch64/CSE2depsproof.v b/aarch64/CSE2depsproof.v index dbd46142..653c88f4 100644 --- a/aarch64/CSE2depsproof.v +++ b/aarch64/CSE2depsproof.v @@ -104,9 +104,71 @@ Section MEMORY_WRITE. Qed. End INDEXED_AWAY. End MEMORY_WRITE. -End SOUNDNESS. +Section STACK_WRITE. + Variable m m2 : mem. + Variable chunkw chunkr : memory_chunk. + + Variable addrw addrr valw : val. + Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2. + + Section INDEXED_AWAY. + Variable ofsw ofsr : ptrofs. + Hypothesis ADDRW : eval_addressing genv sp + (Ainstack ofsw) nil = Some addrw. + Hypothesis ADDRR : eval_addressing genv sp + (Ainstack ofsr) nil = Some addrr. + + Lemma stack_load_store_away1 : + forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk, + forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk, + forall SWAPPABLE : Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr + \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw, + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intros. + + pose proof (max_size_chunk chunkr) as size_chunkr_bounded. + pose proof (max_size_chunk chunkw) as size_chunkw_bounded. + unfold largest_size_chunk in *. + + rewrite ptrofs_modulus in *. + simpl in *. + inv ADDRR. + inv ADDRW. + + destruct sp; try discriminate. + eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b). + exact STORE. + right. + + all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR]; + rewrite OFSR). + all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW]; + rewrite OFSW). + + all: try rewrite ptrofs_modulus in *. + + all: intuition lia. + Qed. + + Theorem stack_load_store_away : + can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true -> + Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr. + Proof. + intro SWAP. + unfold can_swap_accesses_ofs in SWAP. + repeat rewrite andb_true_iff in SWAP. + repeat rewrite orb_true_iff in SWAP. + repeat rewrite Z.leb_le in SWAP. + apply stack_load_store_away1. + all: tauto. + Qed. + End INDEXED_AWAY. +End STACK_WRITE. +End SOUNDNESS. + Section SOUNDNESS. Variable F V : Type. Variable genv: Genv.t F V. @@ -124,7 +186,7 @@ Proof. intros until rs. intros ADDR ADDR' OVERLAP STORE. destruct addr; destruct addr'; try discriminate. - { (* Aindexed / Aindexed *) + - (* Aindexed / Aindexed *) destruct args as [ | base [ | ]]. 1,3: discriminate. destruct args' as [ | base' [ | ]]. 1,3: discriminate. simpl in OVERLAP. @@ -134,7 +196,14 @@ Proof. 2: discriminate. simpl in *. eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. - } +- (* Ainstack / Ainstack *) + destruct args. 2: discriminate. + destruct args'. 2: discriminate. + cbn in OVERLAP. + destruct (can_swap_accesses_ofs (Ptrofs.unsigned ofs0) chunk' (Ptrofs.unsigned ofs) chunk) eqn:SWAP. + 2: discriminate. + cbn in *. + eapply stack_load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption. Qed. End SOUNDNESS. diff --git a/aarch64/Op.v b/aarch64/Op.v index afc25aa6..f720e545 100644 --- a/aarch64/Op.v +++ b/aarch64/Op.v @@ -1209,6 +1209,20 @@ Proof. rewrite (cond_depends_on_memory_correct cond args m1 m2 H). auto. Qed. +Lemma op_valid_pointer_eq: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. +Proof. + intros until m2. destruct op eqn:OP; simpl; try congruence. + - intros MEM; destruct cond; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + - intro MEM; destruct cond; simpl; try congruence; + repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +Qed. + (** Global variables mentioned in an operation or addressing mode *) Definition globals_addressing (addr: addressing) : list ident := |