diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-09 18:13:30 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-09 18:13:30 +0200 |
| commit | f06f87e76cee43d2a4d9b47bea758a2ed5c78bd8 (patch) | |
| tree | 0c1202b05c9f75406307a82c79b9caa3537ecadf /kvx | |
| parent | 810db12b9c2a79a85612a28691b5c3a376bfeee4 (diff) | |
| download | compcert-kvx-f06f87e76cee43d2a4d9b47bea758a2ed5c78bd8.tar.gz compcert-kvx-f06f87e76cee43d2a4d9b47bea758a2ed5c78bd8.zip | |
hconsing: red_PTree_set_correct
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl_junk.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index 80e8b08c..dce66a5f 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -824,6 +824,17 @@ Definition red_PTree_set (r: reg) (hsv: hsval) (hst: PTree.t hsval): PTree.t hsv | _ => PTree.set r hsv hst end. +Lemma red_PTree_set_correct (r r0:reg) hsv hst ge sp rs0 m0: + hsi_sreg_eval ge sp (red_PTree_set r hsv hst) r0 rs0 m0 = hsi_sreg_eval ge sp (PTree.set r hsv hst) r0 rs0 m0. +Proof. + destruct hsv; simpl; auto. + destruct (Pos.eq_dec r r1); auto. + subst; unfold hsi_sreg_eval. + destruct (Pos.eq_dec r0 r1); auto. + - subst; rewrite PTree.grs, PTree.gss; simpl; auto. + - rewrite PTree.gro, PTree.gso; simpl; auto. +Qed. + Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local := DO ok_lhsv <~ (if may_trap rsv lr |