diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-12-04 17:41:14 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-12-04 17:41:14 +0100 |
commit | 60ff1e39bac5ab35c46698cbc1ed7a76fc936cab (patch) | |
tree | 87ff5f3b209e5659e967f862dab1517bb2b32baa /arm | |
parent | f2fb8540c94ceb9892510f83bd7d6734fe9d422f (diff) | |
parent | d2197102d6b81e225865cfac5f1d319d168e1e23 (diff) | |
download | compcert-kvx-60ff1e39bac5ab35c46698cbc1ed7a76fc936cab.tar.gz compcert-kvx-60ff1e39bac5ab35c46698cbc1ed7a76fc936cab.zip |
Merge branch 'kvx-work' into kvx-work-merge3.8
Conflicts:
Makefile
configure
Diffstat (limited to 'arm')
-rw-r--r-- | arm/CSE2deps.v | 5 | ||||
-rw-r--r-- | arm/CSE2depsproof.v | 74 | ||||
-rw-r--r-- | arm/Op.v | 14 | ||||
l--------- | arm/PrepassSchedulingOracle.ml | 1 |
4 files changed, 91 insertions, 3 deletions
diff --git a/arm/CSE2deps.v b/arm/CSE2deps.v index d48dabf3..4592f408 100644 --- a/arm/CSE2deps.v +++ b/arm/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 (Int.unsigned ofs') chunk' (Int.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/arm/CSE2depsproof.v b/arm/CSE2depsproof.v index 28ef41ca..7dd0914e 100644 --- a/arm/CSE2depsproof.v +++ b/arm/CSE2depsproof.v @@ -105,6 +105,68 @@ Section MEMORY_WRITE. Qed. End INDEXED_AWAY. End MEMORY_WRITE. + +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. @@ -125,7 +187,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. @@ -135,7 +197,15 @@ 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 i0) chunk' (Ptrofs.unsigned i) 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. @@ -751,6 +751,20 @@ Proof. 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 c; 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 c; 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_operation (op: operation) : list ident := diff --git a/arm/PrepassSchedulingOracle.ml b/arm/PrepassSchedulingOracle.ml new file mode 120000 index 00000000..9885fd52 --- /dev/null +++ b/arm/PrepassSchedulingOracle.ml @@ -0,0 +1 @@ +../x86/PrepassSchedulingOracle.ml
\ No newline at end of file |