diff options
| -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. |