diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-13 16:02:15 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-13 16:02:15 +0200 |
commit | 94becaa726a06ab83a7e5e61f61cab89d5884d62 (patch) | |
tree | d627edf5c38ae46ff1dc4eccca0199f07caae9c0 /aarch64 | |
parent | 10ae0441711eba798e852ca580c5895cb49576d9 (diff) | |
download | compcert-kvx-94becaa726a06ab83a7e5e61f61cab89d5884d62.tar.gz compcert-kvx-94becaa726a06ab83a7e5e61f61cab89d5884d62.zip |
Simplifying Ltac and fixing a bug in AsmBlock semantics
The bug was a typo on the PArithPPP subl inst
Diffstat (limited to 'aarch64')
-rw-r--r-- | aarch64/Asmblock.v | 2 | ||||
-rw-r--r-- | aarch64/Asmgenproof.v | 40 |
2 files changed, 31 insertions, 11 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 8f859d55..950e28e9 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -1255,7 +1255,7 @@ Definition arith_eval_ppp i v1 v2 := | Pudiv W => Val.maketotal (Val.divu v1 v2) | Pudiv X => Val.maketotal (Val.divlu v1 v2) | Paddext x => Val.addl v1 (eval_extend v2 x) - | Psubext x => Val.subl v2 (eval_extend v2 x) + | Psubext x => Val.subl v1 (eval_extend v2 x) | Pfadd S => Val.addfs v1 v2 | Pfadd D => Val.addf v1 v2 | Pfdiv S => Val.divfs v1 v2 diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index a055bb42..718292f9 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1051,7 +1051,7 @@ Ltac reg_rwrt := Ltac destruct_reg_inv := repeat match goal with | [ H : match ?reg with _ => _ end = _ |- _ ] - => destruct reg; try congruence; try inv_ok_eq; try reg_rwrt + => simpl in *; destruct reg; try congruence; try inv_ok_eq; try reg_rwrt end. Ltac destruct_reg_size := @@ -1060,6 +1060,18 @@ Ltac destruct_reg_size := => destruct reg; try congruence end. +Ltac find_rwrt_ag := + match goal with + | [ AG: forall r, r <> ?PC -> _ r = _ r |- _ ] + => repeat rewrite <- AG; try congruence + end. + +Ltac inv_matchi := + match goal with + | [ MATCHI : match_internal _ _ _ |- _ ] + => inversion MATCHI; subst; find_rwrt_ag + end. + Lemma exec_basic_simulation: forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) @@ -1074,20 +1086,28 @@ Proof. destruct bi. - (* PArith *) simpl in *; destruct i. - + (* Padrp *) - destruct i; monadInv TRANSBI; - destruct rd as [[r|]|]; try congruence; inversion EQ; subst; + + (* PArithP *) + destruct i; + monadInv TRANSBI; + try (destruct_reg_inv); exploit next_inst_preserved; eauto; - intros; simpl in *; try destruct sz; eauto. - + (* Pmovz *) + try (destruct_reg_size). + + (* PArithPP *) + destruct i; + try (destruct sumbool_rec; try congruence); + try (monadInv TRANSBI); + try (destruct_reg_inv); + try (inv_matchi); + try (exploit next_inst_preserved; eauto); + try (destruct_reg_size). + + (* PArithPPP *) destruct i; - try ( destruct sumbool_rec; try congruence); - try (monadInv TRANSBI; simpl in *; destruct rd; try congruence; inversion EQ; subst); + try (monadInv TRANSBI); try (destruct_reg_inv); - try (inversion MATCHI; subst; rewrite <- AG; try congruence); + try (inv_matchi); try (exploit next_inst_preserved; eauto); try (destruct_reg_size). - + + + (* PArithRR0R *) all:admit. all:admit. |