1open HolKernel Parse boolLib bossLib; 2 3open core_decompilerLib 4open arm_core_decompLib 5 6val () = new_theory "arm_decomp_demo"; 7 8(* the first PID exmaple *) 9 10val (PID_C_cert,PID_C_def) = arm_decompLib.l3_arm_decompile "PID_C" ` 11 (* ------ PID example ------- *) 12 ed907a00 (* vldr s14, [r0] *) 13 edd16a00 (* vldr s13, [r1] *) 14 ee676a26 (* vmul.f32 s13, s14, s13 *) 15 e3001000 (* movw r1, #0 *) 16 e3401000 (* movt r1, #0 *) 17 edd15a00 (* vldr s11, [r1] *) 18 ed936a00 (* vldr s12, [r3] *) 19 ed925a00 (* vldr s10, [r2] *) 20 edd17a01 (* vldr s15, [r1, #4] *) 21 e59d3000 (* ldr r3, [sp] *) 22 ed817a00 (* vstr s14, [r1] *) 23 ee775a65 (* vsub.f32 s11, s14, s11 *) 24 ee477a05 (* vmla.f32 s15, s14, s10 *) 25 ee456a86 (* vmla.f32 s13, s11, s12 *) 26 edc17a01 (* vstr s15, [r1, #4] *) 27 ee767aa7 (* vadd.f32 s15, s13, s15 *) 28 edc37a00 (* vstr s15, [r3] *)`; 29 30val _ = save_thm("PID_C_cert",PID_C_cert); 31 32val (PID_ADA_cert,PID_ADA_def) = arm_decompLib.l3_arm_decompile "PID_ADA" ` 33 e3003000 (* movw r3, #0 *) 34 e3403000 (* movt r3, #0 *) 35 ed937a00 (* vldr s14, [r3] *) 36 edd37a03 (* vldr s15, [r3, #12] *) 37 ee676a27 (* vmul.f32 s13, s14, s15 *) 38 edd35a01 (* vldr s11, [r3, #4] *) 39 edd37a05 (* vldr s15, [r3, #20] *) 40 ed936a02 (* vldr s12, [r3, #8] *) 41 ed935a04 (* vldr s10, [r3, #16] *) 42 ed837a01 (* vstr s14, [r3, #4] *) 43 ee775a65 (* vsub.f32 s11, s14, s11 *) 44 ee477a05 (* vmla.f32 s15, s14, s10 *) 45 ee456a86 (* vmla.f32 s13, s11, s12 *) 46 edc37a05 (* vstr s15, [r3, #20] *) 47 ee767aa7 (* vadd.f32 s15, s13, s15 *) 48 edc37a06 (* vstr s15, [r3, #24] *)` 49 50val _ = save_thm("PID_ADA_cert",PID_ADA_cert); 51 52(* an attempt at proving them equivalent *) 53 54open wordsTheory; 55open wordsLib; 56val _ = (guessing_word_lengths := true); 57 58val word_read_def = Define ` 59 word_read (m:word32 -> word8) a = 60 (m (a + 3w) @@ m (a + 2w) @@ m (a + 1w) @@ m (a))`; 61 62val word_write_def = Define ` 63 word_write (m:word32 -> word8) (a:word32) (w:word32) = 64 (a + 3w =+ (31 >< 24) w) 65 ((a + 2w =+ (23 >< 16) w) 66 ((a + 1w =+ (15 >< 8) w) 67 ((a =+ (7 >< 0) w) m)))`; 68 69val put_upper_def = Define ` 70 ((put_upper (w:word32) (d:word64)):word64) = 71 bit_field_insert 63 32 w d`; 72 73val put_lower_def = Define ` 74 ((put_lower (w:word32) (d:word64)):word64) = 75 bit_field_insert 31 0 w d`; 76 77val get_upper_def = Define ` 78 ((get_upper (d:word64)):word32) = (63 >< 32) d`; 79 80val get_lower_def = Define ` 81 ((get_lower (d:word64)):word32) = (31 >< 0) d`; 82 83val word_write_lower = prove( 84 ``((a + 3w =+ (31 >< 24) d7) 85 ((a + 2w =+ (23 >< 16) d7) 86 ((a + 1w =+ (15 >< 8) d7) 87 ((a =+ (7 >< 0) d7) m)))) = 88 (word_write m a (get_lower d7))``, 89 SIMP_TAC std_ss [word_write_def,get_lower_def] 90 THEN REPEAT (MATCH_MP_TAC 91 (METIS_PROVE [] ``(x1 = x2) /\ (m1 = m2) ==> ((a =+ x1) m1 = (a =+ x2) m2)``) 92 THEN REPEAT STRIP_TAC THEN SIMP_TAC std_ss [] THEN1 blastLib.BBLAST_TAC)); 93 94val word_write_upper = prove( 95 ``((a + 3w =+ (63 >< 56) d7) 96 ((a + 2w =+ (55 >< 48) d7) 97 ((a + 1w =+ (47 >< 40) d7) 98 ((a =+ (39 >< 32) d7) m)))) = 99 (word_write m a (get_upper d7))``, 100 SIMP_TAC std_ss [word_write_def,get_upper_def] 101 THEN REPEAT (MATCH_MP_TAC 102 (METIS_PROVE [] ``(x1 = x2) /\ (m1 = m2) ==> ((a =+ x1) m1 = (a =+ x2) m2)``) 103 THEN REPEAT STRIP_TAC THEN SIMP_TAC std_ss [] THEN1 blastLib.BBLAST_TAC)); 104 105val put_get_simp = prove( 106 ``(put_upper w (put_upper w1 d) = put_upper w d) /\ 107 (get_upper (put_upper w d) = w) /\ 108 (get_upper (put_lower w1 d) = get_upper d) /\ 109 (put_lower w (put_lower w1 d) = put_lower w d) /\ 110 (get_lower (put_lower w d) = w) /\ 111 (get_lower (put_upper w1 d) = get_lower d) /\ 112 (put_upper w1 (put_lower w2 d) = put_lower w2 (put_upper w1 d))``, 113 SIMP_TAC std_ss [put_lower_def,get_lower_def,put_upper_def,get_upper_def] 114 THEN blastLib.BBLAST_TAC); 115 116val lemma = EVAL ``bit_field_insert 31 16 (0w:word16) (0w:word32) : word32`` 117 118val PID_ADA_lemma = 119 PID_ADA_def |> CONJUNCT1 |> SIMP_RULE std_ss [GSYM word_read_def, 120 GSYM put_upper_def,GSYM put_lower_def,word_write_lower,word_write_upper, 121 GSYM get_lower_def,GSYM get_upper_def,Once LET_DEF,lemma] 122 |> SIMP_RULE std_ss [LET_DEF,put_get_simp,word_add_n2w] 123 124val PID_C_lemma = 125 PID_C_def |> CONJUNCT1 |> SIMP_RULE std_ss [GSYM word_read_def, 126 GSYM put_upper_def,GSYM put_lower_def,word_write_lower,word_write_upper, 127 GSYM get_lower_def,GSYM get_upper_def,Once LET_DEF,lemma] 128 |> SIMP_RULE std_ss [LET_DEF,put_get_simp,word_add_n2w,lemma] 129 130val PID_ADA_EQUIV_PID_C = store_thm("PID_ADA_EQUIV_PID_C", 131 ``(word_read m2 r0 = word_read m1 0w) /\ 132 (word_read m2 0w = word_read m1 4w) /\ 133 (word_read m2 r3 = word_read m1 8w) /\ 134 (word_read m2 r2 = word_read m1 16w) ==> 135 let (r3_a,d5_a,d6_a,d7_a,dm_a,m_a,rmode_a) = 136 PID_ADA (d5,d6,d7,dm,m1,rmode) in 137 let (r0_c,r1_c,r2_c,r3_c,r13_c,d5_c,d6_c,d7_c,dm_c,m_c,rmode_c) = 138 PID_C (r0,r1,r2,r3,r13,d5,d6,d7,dm,m2,rmode) in 139 (d7_a,rmode_a) = (d7_c,rmode_c)``, 140 SIMP_TAC std_ss [PID_ADA_lemma,PID_C_lemma,LET_DEF]); 141 142(* the second PID example *) 143 144val (PID_C2_cert, PID_C2_def) = core_decompilerLib.core_decompile "PID_C2" ` 145 (* ----------------------------------- *) 146 e59f322c 00012f94 (* ldr r3, [pc, #556] ; 824c *) 147 e59f222c 00012f80 (* ldr r2, [pc, #556] ; 8250 *) 148 edd37a00 (* vldr s15, [r3] *) 149 ed927a00 (* vldr s14, [r2] *) 150 e59f3224 00012e84 (* ldr r3, [pc, #548] ; 8254 *) 151 e59f2224 00012f98 (* ldr r2, [pc, #548] ; 8258 *) 152 edd25a00 (* vldr s11, [r2] *) 153 e1d320f8 (* ldrsh r2, [r3, #8] *) 154 e3520000 (* cmp r2, #0 *) 155 e52d4004 (* push {r4} ; (str *) 156 edd36a00 (* vldr s13, [r3] *) 157 ed936a01 (* vldr s12, [r3, #4] *) 158 edc37a00 (* vstr s15, [r3] *) 159 ee277a87 (* vmul.f32 s14, s15, s14 *) 160 e1d320fa (* ldrsh r2, [r3, #10] *) 161 0a000061 (* beq 81e0 <main+0x1c8> *) 162 e3520000 (* cmp r2, #0 *) 163 0a00000b (* beq 8090 <main+0x78> *) 164 e59f11f4 00012f86 (* ldr r1, [pc, #500] ; 825c *) 165 e59f01f4 00012f8c (* ldr r0, [pc, #500] ; 8260 *) 166 e3a02000 (* mov r2, #0 *) 167 e1c120b0 (* strh r2, [r1] *) 168 e1c020b0 (* strh r2, [r0] *) 169 e1c320ba (* strh r2, [r3, #10] *) 170 e1d320fc (* ldrsh r2, [r3, #12] *) 171 e3520000 (* cmp r2, #0 *) 172 03a02001 (* moveq r2, #1 *) 173 01c320bc (* strheq r2, [r3, #12] *) 174 01c120b0 (* strheq r2, [r1] *) 175 ea00005a (* b 81fc <main+0x1e4> *) 176 eeb65a00 (* vmov.f32 s10, #96 ; 0x60 *) 177 eef47ac5 (* vcmpe.f32 s15, s10 *) 178 eef1fa10 (* vmrs APSR_nzcv, fpscr *) 179 e1d300fc (* ldrsh r0, [r3, #12] *) 180 83a01000 (* movhi r1, #0 *) 181 93a01001 (* movls r1, #1 *) 182 e3500000 (* cmp r0, #0 *) 183 0a000018 (* beq 8114 <main+0xfc> *) 184 e59f01a4 00012f86 (* ldr r0, [pc, #420] ; 825c *) 185 e1d040f0 (* ldrsh r4, [r0] *) 186 e3540008 (* cmp r4, #8 *) 187 e1d0c0b0 (* ldrh ip, [r0] *) 188 d3a02001 (* movle r2, #1 *) 189 d1c320bc (* strhle r2, [r3, #12] *) 190 d08c3002 (* addle r3, ip, r2 *) 191 d1c030b0 (* strhle r3, [r0] *) 192 da000049 (* ble 81fc <main+0x1e4> *) 193 e3510000 (* cmp r1, #0 *) 194 0a000007 (* beq 80fc <main+0xe4> *) 195 e1c020b0 (* strh r2, [r0] *) 196 e1c320bc (* strh r2, [r3, #12] *) 197 e1d320fe (* ldrsh r2, [r3, #14] *) 198 e3520000 (* cmp r2, #0 *) 199 03a02001 (* moveq r2, #1 *) 200 01c320be (* strheq r2, [r3, #14] *) 201 01c020b0 (* strheq r2, [r0] *) 202 ea00003f (* b 81fc <main+0x1e4> *) 203 e3a02001 (* mov r2, #1 *) 204 e1c310bc (* strh r1, [r3, #12] *) 205 e1c320ba (* strh r2, [r3, #10] *) 206 e59f3154 00012f84 (* ldr r3, [pc, #340] ; 8264 *) 207 e1c310b0 (* strh r1, [r3] *) 208 ea000039 (* b 81fc <main+0x1e4> *) 209 e1d320fe (* ldrsh r2, [r3, #14] *) 210 e3520000 (* cmp r2, #0 *) 211 0a00001a (* beq 818c <main+0x174> *) 212 e59f2134 00012f86 (* ldr r2, [pc, #308] ; 825c *) 213 e1d240f0 (* ldrsh r4, [r2] *) 214 e3540008 (* cmp r4, #8 *) 215 e1d2c0b0 (* ldrh ip, [r2] *) 216 d3a01001 (* movle r1, #1 *) 217 d1c310be (* strhle r1, [r3, #14] *) 218 d08c3001 (* addle r3, ip, r1 *) 219 d1c230b0 (* strhle r3, [r2] *) 220 da00002d (* ble 81fc <main+0x1e4> *) 221 e3510000 (* cmp r1, #0 *) 222 1a000009 (* bne 8174 <main+0x15c> *) 223 e1d321f0 (* ldrsh r2, [r3, #16] *) 224 e3520000 (* cmp r2, #0 *) 225 e1c310be (* strh r1, [r3, #14] *) 226 1a000027 (* bne 81fc <main+0x1e4> *) 227 e3a02001 (* mov r2, #1 *) 228 e1c321b0 (* strh r2, [r3, #16] *) 229 e59f30f4 00012f8c (* ldr r3, [pc, #244] ; 8260 *) 230 e1d320b0 (* ldrh r2, [r3] *) 231 e2822001 (* add r2, r2, #1 *) 232 ea000020 (* b 81f8 <main+0x1e0> *) 233 e3a02001 (* mov r2, #1 *) 234 e1c300be (* strh r0, [r3, #14] *) 235 e1c320ba (* strh r2, [r3, #10] *) 236 e59f30dc 00012f84 (* ldr r3, [pc, #220] ; 8264 *) 237 e1c300b0 (* strh r0, [r3] *) 238 ea00001b (* b 81fc <main+0x1e4> *) 239 e1d311f0 (* ldrsh r1, [r3, #16] *) 240 e3510000 (* cmp r1, #0 *) 241 0a00000b (* beq 81c8 <main+0x1b0> *) 242 e59f10c0 00012f8c (* ldr r1, [pc, #192] ; 8260 *) 243 e1d110f0 (* ldrsh r1, [r1] *) 244 e3510ffa (* cmp r1, #1000 ; 0x3e8 *) 245 e1c321b0 (* strh r2, [r3, #16] *) 246 b3a02001 (* movlt r2, #1 *) 247 b1c320bc (* strhlt r2, [r3, #12] *) 248 b59f30a4 00012f86 (* ldrlt r3, [pc, #164] ; 825c *) 249 ba00000f (* blt 81f8 <main+0x1e0> *) 250 e1d321f2 (* ldrsh r2, [r3, #18] *) 251 e3520000 (* cmp r2, #0 *) 252 1a00000d (* bne 81fc <main+0x1e4> *) 253 ea000002 (* b 81d4 <main+0x1bc> *) 254 e1d321f2 (* ldrsh r2, [r3, #18] *) 255 e3520000 (* cmp r2, #0 *) 256 0a000009 (* beq 81fc <main+0x1e4> *) 257 e3a02001 (* mov r2, #1 *) 258 e1c321b2 (* strh r2, [r3, #18] *) 259 ea000004 (* b 81f4 <main+0x1dc> *) 260 e3a01001 (* mov r1, #1 *) 261 e3520000 (* cmp r2, #0 *) 262 e1c310b8 (* strh r1, [r3, #8] *) 263 1a000002 (* bne 81fc <main+0x1e4> *) 264 e1c310ba (* strh r1, [r3, #10] *) 265 e59f3068 00012f84 (* ldr r3, [pc, #104] ; 8264 *) 266 e1c320b0 (* strh r2, [r3] *) 267 ee377a06 (* vadd.f32 s14, s14, s12 *) 268 e59f305c 00012f84 (* ldr r3, [pc, #92] ; 8264 *) 269 e59f205c 00012f7c (* ldr r2, [pc, #92] ; 8268 *) 270 e1d330b0 (* ldrh r3, [r3] *) 271 e1c230b0 (* strh r3, [r2] *) 272 e59f203c 00012e84 (* ldr r2, [pc, #60] ; 8254 *) 273 ed827a01 (* vstr s14, [r2, #4] *) 274 e59f204c 00012f90 (* ldr r2, [pc, #76] ; 826c *) 275 e3530000 (* cmp r3, #0 *) 276 0e776ae6 (* vsubeq.f32 s13, s15, s13 *) 277 ed926a00 (* vldr s12, [r2] *) 278 0e677aa5 (* vmuleq.f32 s15, s15, s11 *) 279 0e467a26 (* vmlaeq.f32 s15, s12, s13 *) 280 1ddf7a04 42c7cccd (* vldrne s15, [pc, #16] ; 8248 *) 281 0e777a87 (* vaddeq.f32 s15, s15, s14 *) 282 e59f3030 00012f88 (* ldr r3, [pc, #48] ; 8270 *) 283 edc37a00 (* vstr s15, [r3] *) 284 e8bd0010 (* pop {r4} *)`; 285 286val _ = save_thm("PID_C2_def",PID_C2_def); 287val _ = save_thm("PID_C2_cert",PID_C2_cert); 288 289val () = export_theory() 290