diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-04 08:01:15 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-04 08:01:15 +0200 |
| commit | 10963816f7f909e58afb0b12cc77c84f7f9c8b94 (patch) | |
| tree | b4a23165cf7b2eb92300f0da7b41f0e446a2b911 /mppa_k1c/lib | |
| parent | 36d9f605478abac2f2fa15ecace6722863263bf3 (diff) | |
| download | compcert-kvx-10963816f7f909e58afb0b12cc77c84f7f9c8b94.tar.gz compcert-kvx-10963816f7f909e58afb0b12cc77c84f7f9c8b94.zip | |
big proofs for so / lo
Diffstat (limited to 'mppa_k1c/lib')
| -rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 9303b780..e8835a82 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -957,6 +957,15 @@ Proof. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. inv H1. Simpl. + - (* PLoadORRO *) + unfold parexec_load_o_offset in H1. + destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. + destruct (orb _ _) in H1; try discriminate. + destruct (Mem.loadv _ _ _) in H1; try discriminate. + destruct (Mem.loadv _ _ _) in H1; try discriminate. + destruct (Mem.loadv _ _ _) in H1; try discriminate. + destruct (Mem.loadv _ _ _) in H1; try discriminate. + inv H1. Simpl. - (* PStoreQRRO *) unfold parexec_store_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. @@ -964,6 +973,15 @@ Proof. destruct (Mem.storev _ _ _) in H1; try discriminate. destruct (Mem.storev _ _ _) in H1; try discriminate. inv H1. Simpl. reflexivity. + - (* PStoreORRO *) + unfold parexec_store_o_offset in H1. + destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. + unfold eval_offset in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + destruct (Mem.storev _ _ _) in H1; try discriminate. + inv H1. Simpl. reflexivity. - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. |