diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-08 11:30:46 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-08 11:30:46 +0100 |
commit | f88eb3311e606c1d8de616c3c231f95144ff4825 (patch) | |
tree | 6d601e032bd5dd9189bfb01acf6e946228280607 /mppa_k1c/Asmblockdeps.v | |
parent | 405f173c02e73a929ce9e9debb3f2bfa704702c7 (diff) | |
parent | 8e68be1345bef8e2f8ee428c51d4290e4464ebd6 (diff) | |
download | compcert-kvx-f88eb3311e606c1d8de616c3c231f95144ff4825.tar.gz compcert-kvx-f88eb3311e606c1d8de616c3c231f95144ff4825.zip |
Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patch
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index ec5c3cf5..b7e7b87c 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -292,7 +292,7 @@ Definition iandb (ib1 ib2: ?? bool): ?? bool := Definition arith_op_eq (o1 o2: arith_op): ?? bool := match o1, o2 with - | OArithR n1, OArithR n2 => phys_eq n1 n2 + | OArithR n1, OArithR n2 => struct_eq n1 n2 | OArithRR n1, OArithRR n2 => phys_eq n1 n2 | OArithRI32 n1 i1, OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | OArithRI64 n1 i1, OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) @@ -359,16 +359,17 @@ Proof. - rewrite Z.eqb_eq in * |-. congruence. Qed. -(* + Definition op_eq (o1 o2: op): ?? bool := match o1, o2 with | Arith i1, Arith i2 => arith_op_eq i1 i2 | Load i1, Load i2 => load_op_eq i1 i2 | Store i1, Store i2 => store_op_eq i1 i2 | Control i1, Control i2 => control_op_eq i1 i2 - | Allocframe sz1 pos1, Allocframe sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2) - | Freeframe sz1 pos1, Freeframe sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2) - | Freeframe2 sz1 pos1, Freeframe2 sz2 pos2 => iandb (phys_eq sz1 sz2) (phys_eq pos1 pos2) + | Allocframe sz1 pos1, Allocframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) + | Allocframe2 sz1 pos1, Allocframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) + | Freeframe sz1 pos1, Freeframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) + | Freeframe2 sz1 pos1, Freeframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | Constant c1, Constant c2 => phys_eq c1 c2 | Fail, Fail => RET true | _, _ => RET false @@ -383,22 +384,25 @@ Proof. - simpl in Hexta. exploit load_op_eq_correct. eassumption. eauto. congruence. - simpl in Hexta. exploit store_op_eq_correct. eassumption. eauto. congruence. - simpl in Hexta. exploit control_op_eq_correct. eassumption. eauto. congruence. - - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. - - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. - - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. + - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence. + - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence. + - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence. + - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence. - congruence. Qed. -*) + (* QUICK FIX WITH struct_eq *) -Definition op_eq (o1 o2: op): ?? bool := struct_eq o1 o2. +(* Definition op_eq (o1 o2: op): ?? bool := struct_eq o1 o2. + Theorem op_eq_correct o1 o2: WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2. Proof. wlp_simplify. Qed. + *) End IMPPARAM. |