diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2021-08-11 15:21:57 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-06 14:33:45 +0200 |
| commit | 7e8e3efdd69cee4412817f2e29f9ef687bec019b (patch) | |
| tree | e758a33cc8066b230aea40625a28e71458b4f566 /powerpc/Asmgenproof1.v | |
| parent | a320361a90efaa48275153f2e19ccfb443b32688 (diff) | |
| download | compcert-kvx-7e8e3efdd69cee4412817f2e29f9ef687bec019b.tar.gz compcert-kvx-7e8e3efdd69cee4412817f2e29f9ef687bec019b.zip | |
Share code for memory access for PowerPC
Instead of duplicating the memory access code in `Asmexpand.ml` we move
the code for each of the different addressings in `Asmgen.v` into
separate functions that then can be reused in `Asmexpand.ml`.
Diffstat (limited to 'powerpc/Asmgenproof1.v')
| -rw-r--r-- | powerpc/Asmgenproof1.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 7268b407..6ae520ef 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1564,6 +1564,7 @@ Proof. intros until m'; intros TR ADDR TEMP MK1 MK2. unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in ADDR; inv ADDR. - (* Aindexed *) + unfold aindexed. destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero); [destruct (Int.eq (high_s i) Int.zero) |]. + (* Aindexed 4 aligned short *) apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. @@ -1590,6 +1591,7 @@ Proof. - (* Aindexed2 *) apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. - (* Aglobal *) + unfold aglobal in *. destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR. + (* Aglobal from small data 4 aligned *) case (unaligned || symbol_ofs_word_aligned i i0). @@ -1643,7 +1645,8 @@ Proof. apply exec_straight_step with rs2 m; auto. simpl. unfold rs2. rewrite gpr_or_zero_not_zero; auto. f_equal. f_equal. f_equal. unfold rs1; Simpl. apply low_high_half_zero. eexact EX'. auto. - -(* Abased *) + - (* Abased *) + unfold abased in *. destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]. + (* Abased from small data *) set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))). @@ -1700,6 +1703,7 @@ Proof. unfold rs2; Simpl. apply low_high_half_zero. eexact EX'. auto. - (* Ainstack *) + unfold ainstack in *. set (ofs := Ptrofs.to_int i) in *. assert (L: Val.lessdef (Val.offset_ptr (rs GPR1) i) (Val.add (rs GPR1) (Vint ofs))). { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. } |