From 10963816f7f909e58afb0b12cc77c84f7f9c8b94 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 4 May 2019 08:01:15 +0200 Subject: big proofs for so / lo --- mppa_k1c/lib/Asmblockgenproof0.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'mppa_k1c/lib/Asmblockgenproof0.v') 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. -- cgit