1 2open HolKernel boolLib bossLib Parse; 3open decompilerLib prog_x86Lib; 4 5val decompile_x86 = decompile x86_tools 6 7open pred_setTheory arithmeticTheory pairTheory listTheory wordsTheory; 8open addressTheory set_sepTheory progTheory prog_x86Theory; 9open wordsLib x86_encodeLib helperLib; 10 11open jit_inputTheory jit_opsTheory; 12 13open compilerLib; 14open export_codeLib; 15 16infix \\ 17val op \\ = op THEN; 18 19 20val _ = new_theory "jit_codegen"; 21 22 23(* compiler setup code *) 24 25(* val _ = set_x86_exec_flag false; *) 26 27(* make function "f" have exec permissions *) 28val _ = add_executable_data_name "f" 29 30(* assign meanings to r1, r2, r3, r4 etc *) 31val _ = codegen_x86Lib.set_x86_regs 32 [(1,"eax"),(6,"ebx"),(5,"ecx"),(2,"edx"),(3,"edi"),(4,"esi"),(7,"ebp")] 33 34val dec_byte = let 35 val (th1,th2) = decompile_x86 "dec_byte" 36 [QUOTE (x86_encodeLib.x86_encode "DEC BYTE [eax]" ^ "/f")] 37 in SIMP_RULE std_ss [th2,LET_DEF] th1 end 38 39val _ = codegenLib.add_compiled [dec_byte]; 40 41 42(* 43 44r1 = pointer to generated code 45r2 = pointer to byte code instr 46r3 = pointer to start of byte code 47r4 = pointer to start of generated code 48r5 = temp 49r6 = temp 50r7 = pointer to initial stack 51 52*) 53 54 55val (th1,x86_istop_def,x86_istop_pre_def) = compile "x86" `` 56 (x86_isub (r1:word32,df:word32 set,f:word32->word8) = 57 let f = (r1 =+ 0x2Bw) f in 58 let f = (r1 + 1w =+ 0x07w) f in 59 let r1 = r1 + 2w in 60 (r1,df,f)) /\ 61 (x86_iswap (r1:word32,df:word32 set,f:word32->word8) = 62 let f = (r1 =+ 0x87w) f in 63 let f = (r1 + 1w =+ 0x07w) f in 64 let r1 = r1 + 2w in 65 (r1,df,f)) /\ 66 (x86_ipop (r1:word32,df:word32 set,f:word32->word8) = 67 let f = (r1 =+ 0x8Bw) f in 68 let f = (r1 + 1w =+ 0x07w) f in 69 let f = (r1 + 2w =+ 0x83w) f in 70 let f = (r1 + 3w =+ 0xC7w) f in 71 let f = (r1 + 4w =+ 0x04w) f in 72 let r1 = r1 + 5w in 73 (r1,df,f)) /\ 74 (x86_ipush (r1:word32,r6:word32,df:word32 set,f:word32->word8) = 75 let f = (r1 =+ 0x83w) f in 76 let f = (r1 + 1w =+ 0xEFw) f in 77 let f = (r1 + 2w =+ 0x04w) f in 78 let f = (r1 + 3w =+ 0x89w) f in 79 let f = (r1 + 4w =+ 0x07w) f in 80 let f = (r1 + 5w =+ 0xB8w) f in 81 let f = (r1 + 6w =+ w2w r6) f in 82 let f = (r1 + 7w =+ 0x00w) f in 83 let f = (r1 + 8w =+ 0x00w) f in 84 let f = (r1 + 9w =+ 0x00w) f in 85 let r1 = r1 + 10w in 86 (r1,df,f)) /\ 87 (x86_istop (r1:word32,df:word32 set,f:word32->word8) = 88 let f = (r1 =+ 0xFFw) f in 89 let f = (r1 + 1w =+ 0xE2w) f in 90 let r1 = r1 + 2w in 91 (r1,df,f)) /\ 92 (x86_ijump (r1:word32,df:word32 set,f:word32->word8) = 93 let f = (r1 =+ 0xE9w) f in 94 let r5 = 5w:word32 in 95 (r1,r5,df,f)) /\ 96 (x86_ijeq (r1:word32,df:word32 set,f:word32->word8) = 97 let f = (r1 + 3w =+ 0x84w) f in 98 let r5 = 8w:word32 in 99 (r1,r5,df,f)) /\ 100 (x86_ijlt (r1:word32,df:word32 set,f:word32->word8) = 101 let f = (r1 + 3w =+ 0x82w) f in 102 let r5 = 8w:word32 in 103 (r1,r5,df,f))`` 104 105fun ord_eval tm = let 106 val tms = find_terml (can (match_term ``n2w (ORD c):'a word``)) tm 107 in (snd o dest_eq o concl o REWRITE_CONV (map EVAL tms)) tm end 108 109val (th1,x86_codegen_jump_op_def,x86_codegen_jump_op_pre_def) = (compile "x86" o ord_eval) `` 110 x86_codegen_jump_op (r1:word32,r5:word32,df,f) = 111 if r5 = n2w (ORD #"j") then 112 let (r1,r5,df,f) = x86_ijump (r1,df,f) in (r1,r5,df,f) 113 else 114 let f = (r1 =+ 0x3Bw) f in 115 let f = (r1 + 1w =+ 0x07w) f in 116 let f = (r1 + 2w =+ 0x0Fw) f in 117 if r5 = n2w (ORD #"=") then 118 let (r1,r5,df,f) = x86_ijeq (r1,df,f) in (r1,r5,df,f) 119 else 120 let (r1,r5,df,f) = x86_ijlt (r1,df,f) in (r1,r5,df,f)``; 121 122(* r6 - pointer to bytecode, r5 - address in generated code *) 123val (th1,x86_addr_def,x86_addr_pre_def) = (compile "x86" o ord_eval) `` 124 x86_addr (r1:word32,r5:word32,r6:word32,df:word32 set,f:word32->word8,dg:word32 set,g:word32->word8) = 125 if f r1 = 0w then (r1,r5,df,f,dg,g) else 126 let f = (r1 =+ f r1 - 1w) f in 127 if (g r6 = n2w (ORD #"-")) \/ (g r6 = n2w (ORD #"s")) \/ (g r6 = n2w (ORD #".")) 128 then let r6 = r6 + 1w in let r5 = r5 + 2w in x86_addr (r1,r5,r6,df,f,dg,g) else 129 if g r6 = n2w (ORD #"p") then let r6 = r6 + 1w in let r5 = r5 + 5w in x86_addr (r1,r5,r6,df,f,dg,g) else 130 if g r6 = n2w (ORD #"c") then let r6 = r6 + 2w in let r5 = r5 + 10w in x86_addr (r1,r5,r6,df,f,dg,g) else 131 if g r6 = n2w (ORD #"j") then let r6 = r6 + 2w in let r5 = r5 + 5w in x86_addr (r1,r5,r6,df,f,dg,g) else 132 if (g r6 = n2w (ORD #"=")) \/ (g r6 = n2w (ORD #"<")) then let r6 = r6 + 2w in let r5 = r5 + 8w in x86_addr (r1,r5,r6,df,f,dg,g) else 133 (r1,r5,df,f,dg,g)``; 134 135val (th1,x86_codegen_jumps_def,x86_codegen_jumps_pre_def) = compile "x86" `` 136 x86_codegen_jumps (r1,r2,r3,r4,r5,df,f,dg,g) = 137 let (r1,r5,df,f) = x86_codegen_jump_op (r1,r5,df,f) in 138 let r1 = r1 + r5 in 139 let r5 = r4 in 140 let r6 = (w2w (g r2)):word32 in 141 let r1 = r1 - 1w in 142 let r6 = r6 - 48w in 143 let f = (r1 =+ w2w r6) f in 144 let r6 = r3 in 145 let (r1,r5,df,f,dg,g) = x86_addr (r1,r5,r6,df,f,dg,g) in 146 (* store offset *) 147 let r1 = r1 + 1w in 148 let r5 = r5 - r1 in 149 let f = (r1 - 4w =+ w2w r5) f in 150 let r5 = r5 >>> 8 in 151 let f = (r1 - 3w =+ w2w r5) f in 152 let r5 = r5 >>> 8 in 153 let f = (r1 - 2w =+ w2w r5) f in 154 let r5 = r5 >>> 8 in 155 let f = (r1 - 1w =+ w2w r5) f in 156 (r1,r2,r3,r4,df,f,dg,g)`` 157 158val (th1,x86_codegen_loop_def,x86_codegen_loop_pre_def) = (compile "x86" o ord_eval) `` 159 x86_codegen_loop (r1,r2,r3,r4,df,f,dg,g) = 160 let r5 = (w2w (g r2)):word32 in 161 let r2 = r2 + 1w in 162 if r5 = 0w then 163 (r4,df,f,dg,g) 164 else if r5 = n2w (ORD #"-") then 165 let (r1,df,f) = x86_isub (r1,df,f) in 166 x86_codegen_loop (r1,r2,r3,r4,df,f,dg,g) 167 else if r5 = n2w (ORD #"s") then 168 let (r1,df,f) = x86_iswap (r1,df,f) in 169 x86_codegen_loop (r1,r2,r3,r4,df,f,dg,g) 170 else if r5 = n2w (ORD #"p") then 171 let (r1,df,f) = x86_ipop (r1,df,f) in 172 x86_codegen_loop (r1,r2,r3,r4,df,f,dg,g) 173 else if r5 = n2w (ORD #"c") then 174 let r6 = (w2w (g r2)):word32 in 175 let r2 = r2 + 1w in 176 let r6 = r6 - 48w in 177 let (r1,df,f) = x86_ipush (r1,r6,df,f) in 178 x86_codegen_loop (r1,r2,r3,r4,df,f,dg,g) 179 else if r5 = n2w (ORD #".") then 180 let (r1,df,f) = x86_istop (r1,df,f) in 181 x86_codegen_loop (r1,r2,r3,r4,df,f,dg,g) 182 else (* must be a jump of some kind *) 183 let (r1,r2,r3,r4,df,f,dg,g) = x86_codegen_jumps (r1,r2,r3,r4,r5,df,f,dg,g) in 184 let r2 = r2 + 1w in 185 x86_codegen_loop (r1,r2,r3,r4,df,f,dg,g)`` 186 187val (x86_codegen_th,x86_codegen_def,x86_codegen_pre_def) = compile "x86" `` 188 x86_codegen (r1,r2,df,f,dg,g) = 189 let r3 = r2 in 190 let r4 = r1 in 191 let (r4,df,f,dg,g) = x86_codegen_loop (r1,r2,r3,r4,df,f,dg,g) in 192 (r4,df,f,dg,g)``; 193 194val SEP_BYTES_IN_MEM_def = Define ` 195 (SEP_BYTES_IN_MEM a [] = emp) /\ 196 (SEP_BYTES_IN_MEM a (x::xs) = one (a,x) * SEP_BYTES_IN_MEM (a+1w) xs)`; 197 198val SEP_CODE_IN_MEM_LOOP_def = Define ` 199 (SEP_CODE_IN_MEM_LOOP a [] (a1,ns1) = emp) /\ 200 (SEP_CODE_IN_MEM_LOOP a (n::ns) (a1,ns1) = 201 let branch j = ADDR ns1 a1 j - a in 202 let xs = X86_ENCODE branch n in 203 SEP_BYTES_IN_MEM a xs * SEP_CODE_IN_MEM_LOOP (a + n2w (LENGTH xs)) ns (a1,ns1))`; 204 205val SEP_CODE_IN_MEM_def = Define ` 206 SEP_CODE_IN_MEM a ns = SEP_CODE_IN_MEM_LOOP a ns (a,ns)`; 207 208val CODE_LENGTH_def = Define ` 209 (CODE_LENGTH [] = 0) /\ 210 (CODE_LENGTH (n::ns) = LENGTH (X86_ENCODE (\x.0w) n) + CODE_LENGTH ns)`; 211 212val one_list_def = Define ` 213 (one_list a [] b = cond (b = a)) /\ 214 (one_list a (x::xs) b = one (a,x) * one_list (a + 1w) xs b)`; 215 216val one_space_def = Define ` 217 (one_space a 0 b = cond (b = a)) /\ 218 (one_space a (SUC n) b = SEP_EXISTS y. one (a,y) * one_space (a + 1w) n b)`; 219 220val one_string_def = Define ` 221 one_string a (s:string) b = one_list a (MAP (n2w o ORD) s) b`; 222 223val one_string_0_def = Define ` 224 one_string_0 a (s:string) b = one_string a (s ++ [CHR 0]) b`; 225 226val one_string_STRCAT = store_thm("one_string_STRCAT", 227 ``!s t a c. 228 one_string a (s ++ t) c = 229 one_string a s (a + n2w (LENGTH s)) * 230 one_string (a + n2w (LENGTH s)) t c``, 231 Induct 232 \\ FULL_SIMP_TAC std_ss [one_string_def,WORD_ADD_0,SEP_CLAUSES, 233 ADD,MAP,LENGTH,one_list_def,APPEND] 234 \\ SIMP_TAC std_ss [ADD1,GSYM word_add_n2w] 235 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,STAR_ASSOC]); 236 237val one_string_0_STRCAT = store_thm("one_string_0_STRCAT", 238 ``!s t a c. 239 one_string_0 a (s ++ t) c = 240 one_string a s (a + n2w (LENGTH s)) * 241 one_string_0 (a + n2w (LENGTH s)) t c``, 242 SIMP_TAC std_ss [one_string_0_def,GSYM APPEND_ASSOC] 243 \\ REWRITE_TAC [one_string_STRCAT]); 244 245val one_space_ADD = store_thm("one_space_ADD", 246 ``!m n a c. 247 one_space a (m + n) c = 248 one_space a m (a + n2w m) * 249 one_space (a + n2w m) n c``, 250 Induct 251 \\ ASM_SIMP_TAC std_ss [one_space_def,WORD_ADD_0,SEP_CLAUSES,ADD] 252 \\ SIMP_TAC std_ss [ADD1,GSYM word_add_n2w] 253 \\ SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,STAR_ASSOC]); 254 255val LENGTH_X86_ENCODE = prove( 256 ``!n b. LENGTH (X86_ENCODE b n) = LENGTH (X86_ENCODE (\x.0w) n)``, 257 Cases THEN SIMP_TAC std_ss [LENGTH,X86_ENCODE_def,X86_IMMEDIATE_def,APPEND]); 258 259fun TRY_TAC t goal = t goal handle e => ALL_TAC goal; 260 261val x86_addr_thm = prove( 262 ``!y ns r x b2 f df r1 r5 r6. 263 (r * one_string_0 r6 (iENCODE ns) b1) (fun2set (g,dg)) /\ 264 (x * one (r1,n2w y)) (fun2set (f,df)) /\ y < 256 ==> 265 ?fi z. x86_addr_pre (r1,r5,r6,df,f,dg,g) /\ 266 (x86_addr (r1,r5,r6,df,f,dg,g) = (r1,ADDR ns r5 y,df,fi,dg,g)) /\ 267 (x * one (r1,z)) (fun2set (fi,df))``, 268 SIMP_TAC std_ss [] \\ Induct THEN1 269 (ONCE_REWRITE_TAC [x86_addr_def,x86_addr_pre_def] 270 \\ REPEAT STRIP_TAC \\ Cases_on `ns` 271 \\ `(f r1 = 0w) /\ (r1 IN df)` by SEP_READ_TAC 272 \\ ASM_SIMP_TAC std_ss [ADDR_def,LET_DEF] \\ METIS_TAC []) 273 \\ REPEAT STRIP_TAC 274 \\ ONCE_REWRITE_TAC [x86_addr_def,x86_addr_pre_def] 275 \\ `(f r1 = n2w (SUC y)) /\ r1 IN df` by SEP_READ_TAC 276 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,DECIDE ``~(SUC n = 0)``] 277 \\ SIMP_TAC std_ss [WORD_ADD_SUB,ADD1,GSYM word_add_n2w] 278 \\ Q.ABBREV_TAC `f2 = (r1 =+ n2w y) f` 279 \\ `(x * one (r1,n2w y)) (fun2set (f2,df))` by 280 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC) 281 \\ Cases_on `ns` THEN1 282 (FULL_SIMP_TAC (std_ss++sep_cond_ss) [ADDR_def,GSYM ADD1,iENCODE_def, 283 one_string_0_def,APPEND,one_string_def,MAP,one_list_def,cond_STAR, 284 stringTheory.ORD_CHR_RWT] 285 \\ `r6 IN dg /\ (g r6 = 0w)` by SEP_READ_TAC 286 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,LET_DEF] 287 \\ METIS_TAC []) 288 \\ FULL_SIMP_TAC std_ss [LENGTH,iENCODE_def,one_string_0_STRCAT,LET_DEF] 289 \\ `y < 256` by DECIDE_TAC 290 \\ REWRITE_TAC [GSYM ADD1,ADDR_def,TL,HD] 291 \\ Cases_on `h` 292 \\ FULL_SIMP_TAC std_ss [iENCODE1_def,LENGTH,one_string_def,MAP,APPEND, 293 STAR_ASSOC,one_list_def,SEP_CLAUSES,stringTheory.ORD_CHR_RWT, 294 iIMM_def,word_arith_lemma1] 295 \\ `r6 IN dg` by SEP_READ_TAC 296 \\ TRY_TAC (`g r6 = 0x2Dw` by SEP_READ_TAC) 297 \\ TRY_TAC (`g r6 = 0x20w` by SEP_READ_TAC) 298 \\ TRY_TAC (`g r6 = 0x73w` by SEP_READ_TAC) 299 \\ TRY_TAC (`g r6 = 0x70w` by SEP_READ_TAC) 300 \\ TRY_TAC (`g r6 = 0x2Ew` by SEP_READ_TAC) 301 \\ TRY_TAC (`g r6 = 0x63w` by SEP_READ_TAC) 302 \\ TRY_TAC (`g r6 = 0x6Aw` by SEP_READ_TAC) 303 \\ TRY_TAC (`g r6 = 0x3Dw` by SEP_READ_TAC) 304 \\ TRY_TAC (`g r6 = 0x3Cw` by SEP_READ_TAC) 305 \\ ASM_SIMP_TAC std_ss [xENC_LENGTH_def,X86_ENCODE_def,LENGTH,X86_IMMEDIATE_def,APPEND] 306 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [n2w_11] 307 \\ ASSUME_TAC (Q.SPEC `c` (SIMP_RULE (std_ss++SIZES_ss) [] (INST_TYPE [``:'a``|->``:7``] w2n_lt))) 308 \\ `48 + w2n c < 256` by DECIDE_TAC 309 \\ FULL_SIMP_TAC std_ss [stringTheory.ORD_CHR_RWT] 310 THEN1 311 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 312 \\ Q.EXISTS_TAC `r * one (r6,0x2Dw)` 313 \\ ASM_SIMP_TAC std_ss []) 314 THEN1 315 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 316 \\ Q.EXISTS_TAC `r * one (r6,0x73w)` 317 \\ ASM_SIMP_TAC std_ss []) 318 THEN1 319 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 320 \\ Q.EXISTS_TAC `r * one (r6,0x2Ew)` 321 \\ ASM_SIMP_TAC std_ss []) 322 THEN1 323 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 324 \\ Q.EXISTS_TAC `r * one (r6,0x70w)` 325 \\ ASM_SIMP_TAC std_ss []) 326 THEN1 327 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 328 \\ Q.EXISTS_TAC `r * one (r6,0x63w) * one (r6 + 0x1w,n2w (48 + w2n c))` 329 \\ ASM_SIMP_TAC std_ss []) 330 THEN1 331 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 332 \\ Q.EXISTS_TAC `r * one (r6,0x6Aw) * one (r6 + 0x1w,n2w (48 + w2n c))` 333 \\ ASM_SIMP_TAC std_ss []) 334 THEN1 335 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 336 \\ Q.EXISTS_TAC `r * one (r6,0x3Dw) * one (r6 + 0x1w,n2w (48 + w2n c))` 337 \\ ASM_SIMP_TAC std_ss []) 338 THEN1 339 (Q.PAT_ASSUM `!ns.bbb` MATCH_MP_TAC 340 \\ Q.EXISTS_TAC `r * one (r6,0x3Cw) * one (r6 + 0x1w,n2w (48 + w2n c))` 341 \\ ASM_SIMP_TAC std_ss [])); 342 343val w2w_w2w_n2w_lemma = prove( 344 ``!c:word7. w2w (w2w ((n2w (48 + w2n c)):word8) - 0x30w:word32) = 345 (n2w (w2n c)):word8``, 346 Cases_word 347 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w] 348 \\ `48 + n < 256` by DECIDE_TAC 349 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 350 \\ ONCE_REWRITE_TAC [ADD_COMM] 351 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_SUB] 352 \\ `n < 2**32` by (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 353 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w]); 354 355val x86_codegen_loop_lemma = prove( 356 ``!ns r x a r2 df f dg g b1 b2 y a1 r3 r4. 357 (y * one_string_0 r3 (iENCODE ns1) b1) (fun2set (g,dg)) /\ 358 (x * one_string_0 r2 (iENCODE ns) b1) (fun2set (g,dg)) /\ 359 (r * one_space a (CODE_LENGTH ns) b2) (fun2set (f,df)) ==> 360 ?fi. 361 x86_codegen_loop_pre (a,r2,r3,r4,df,f,dg,g) /\ 362 (x86_codegen_loop (a,r2,r3,r4,df,f,dg,g) = (r4,df,fi,dg,g)) /\ 363 (r * SEP_CODE_IN_MEM_LOOP a ns (r4,ns1)) (fun2set (fi,df))``, 364 Induct THEN1 365 (SIMP_TAC std_ss [SEP_CODE_IN_MEM_LOOP_def,CODE_LENGTH_def,iENCODE_def, 366 one_string_0_def,APPEND,one_space_def,one_string_def,one_list_def,MAP] 367 \\ SIMP_TAC std_ss [EVAL ``ORD (CHR 0)``,cond_STAR] 368 \\ REPEAT STRIP_TAC 369 \\ `(g r2 = 0w) /\ r2 IN dg` by SEP_READ_TAC 370 \\ ONCE_REWRITE_TAC [x86_codegen_loop_pre_def,x86_codegen_loop_def] 371 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,SEP_CLAUSES]) 372 \\ SIMP_TAC std_ss [iENCODE_def,CODE_LENGTH_def,one_string_0_STRCAT] 373 \\ SIMP_TAC std_ss [SEP_CODE_IN_MEM_LOOP_def,LET_DEF,one_space_ADD,STAR_ASSOC] 374 \\ SIMP_TAC std_ss [LENGTH_X86_ENCODE] 375 \\ REPEAT STRIP_TAC 376 \\ Q.ABBREV_TAC `r2j = r2 + n2w (STRLEN (iENCODE1 h))` 377 \\ Cases_on `h` 378 \\ FULL_SIMP_TAC bool_ss [SEP_BYTES_IN_MEM_def,X86_ENCODE_def,STAR_ASSOC, 379 SEP_CLAUSES,iENCODE1_def,one_string_def,MAP,one_list_def,cond_STAR, 380 LENGTH,APPEND,X86_IMMEDIATE_def,one_space_def] 381 \\ FULL_SIMP_TAC std_ss [stringTheory.ORD_CHR_RWT,word_arith_lemma1, 382 SEP_CLAUSES,SEP_EXISTS] 383 \\ Q.PAT_ASSUM `pp (fun2set (g,dg))` MP_TAC 384 \\ REWRITE_TAC [GSYM STAR_ASSOC] 385 \\ ONCE_REWRITE_TAC [STAR_COMM] 386 \\ SIMP_TAC std_ss [GSYM STAR_ASSOC] 387 \\ STRIP_TAC \\ IMP_RES_TAC read_fun2set 388 \\ Q.PAT_ASSUM `pp (fun2set (g,dg))` MP_TAC 389 \\ REWRITE_TAC [STAR_ASSOC] 390 \\ ONCE_REWRITE_TAC [STAR_COMM] 391 \\ REWRITE_TAC [STAR_ASSOC] 392 \\ REPEAT STRIP_TAC 393 \\ ONCE_REWRITE_TAC [x86_codegen_loop_def,x86_codegen_loop_pre_def] 394 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [LET_DEF,w2w_def,w2n_n2w,n2w_11, 395 x86_istop_def,x86_istop_pre_def] 396 \\ TRY_TAC (`a IN df` by SEP_READ_TAC) 397 \\ TRY_TAC (`a+1w IN df` by SEP_READ_TAC) 398 \\ TRY_TAC (`a+2w IN df` by SEP_READ_TAC) 399 \\ TRY_TAC (`a+3w IN df` by SEP_READ_TAC) 400 \\ TRY_TAC (`a+4w IN df` by SEP_READ_TAC) 401 \\ TRY_TAC (`a+5w IN df` by SEP_READ_TAC) 402 \\ TRY_TAC (`a+6w IN df` by SEP_READ_TAC) 403 \\ TRY_TAC (`a+7w IN df` by SEP_READ_TAC) 404 \\ TRY_TAC (`a+8w IN df` by SEP_READ_TAC) 405 \\ TRY_TAC (`a+9w IN df` by SEP_READ_TAC) 406 \\ ASM_SIMP_TAC std_ss [] 407 THEN1 408 (Q.PAT_ASSUM `!xx. bb` MATCH_MP_TAC 409 \\ Q.EXISTS_TAC `x * one (r2,0x2Dw)` 410 \\ Q.EXISTS_TAC `b1` \\ Q.EXISTS_TAC `b2` 411 \\ Q.EXISTS_TAC `y` 412 \\ ASM_SIMP_TAC std_ss [] 413 \\ SEP_WRITE_TAC) 414 THEN1 415 (Q.PAT_ASSUM `!xx. bb` MATCH_MP_TAC 416 \\ Q.EXISTS_TAC `x * one (r2,0x73w)` 417 \\ Q.EXISTS_TAC `b1` \\ Q.EXISTS_TAC `b2` 418 \\ Q.EXISTS_TAC `y` 419 \\ ASM_SIMP_TAC std_ss [] 420 \\ SEP_WRITE_TAC) 421 THEN1 422 (Q.PAT_ASSUM `!xx. bb` MATCH_MP_TAC 423 \\ Q.EXISTS_TAC `x * one (r2,0x2Ew)` 424 \\ Q.EXISTS_TAC `b1` \\ Q.EXISTS_TAC `b2` 425 \\ Q.EXISTS_TAC `y` 426 \\ ASM_SIMP_TAC std_ss [] 427 \\ SEP_WRITE_TAC) 428 THEN1 429 (Q.PAT_ASSUM `!xx. bb` MATCH_MP_TAC 430 \\ Q.EXISTS_TAC `x * one (r2,0x70w)` 431 \\ Q.EXISTS_TAC `b1` \\ Q.EXISTS_TAC `b2` 432 \\ Q.EXISTS_TAC `y` 433 \\ ASM_SIMP_TAC std_ss [] 434 \\ SEP_WRITE_TAC) 435 THEN1 436 (FULL_SIMP_TAC (std_ss++sep_cond_ss) [iIMM_def,stringTheory.ORD_CHR_RWT,MAP, 437 one_list_def,STAR_ASSOC] 438 \\ `r2 + 0x1w IN dg` by SEP_READ_TAC 439 \\ `g (r2 + 1w) = n2w (ORD (CHR (48 + w2n c)))` by SEP_READ_TAC 440 \\ ASSUME_TAC (Q.SPEC `c` (SIMP_RULE (std_ss++SIZES_ss) [] (INST_TYPE [``:'a``|->``:7``] w2n_lt))) 441 \\ `48 + w2n c < 256` by DECIDE_TAC 442 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,w2w_w2w_n2w_lemma,GSYM w2w_def,stringTheory.ORD_CHR_RWT] 443 \\ Q.PAT_ASSUM `!xx. bb` MATCH_MP_TAC 444 \\ Q.EXISTS_TAC `x * one (r2,0x63w) * one (r2 + 0x1w,n2w (48 + w2n c))` 445 \\ Q.EXISTS_TAC `b1` \\ Q.EXISTS_TAC `b2` 446 \\ Q.EXISTS_TAC `y` 447 \\ ASM_SIMP_TAC std_ss [] 448 \\ FULL_SIMP_TAC std_ss [cond_STAR] 449 \\ Q.PAT_ASSUM `r2j = r2 + 2w` ASSUME_TAC 450 \\ FULL_SIMP_TAC std_ss [] 451 \\ SEP_WRITE_TAC) 452 \\ SIMP_TAC (std_ss++SIZES_ss) [x86_codegen_jumps_def, 453 x86_codegen_jumps_pre_def,LET_DEF,x86_codegen_jump_op_pre_def, 454 x86_codegen_jump_op_def,n2w_11,x86_istop_def,x86_istop_pre_def] 455 \\ SIMP_TAC std_ss [word_arith_lemma1,word_arith_lemma2] 456 \\ SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma4,w2w_eq_n2w] 457 \\ Q.UNABBREV_TAC `r2j` 458 \\ FULL_SIMP_TAC std_ss [iIMM_def,MAP,one_list_def,LENGTH, 459 word_arith_lemma1,SEP_CLAUSES,EVAL ``ORD #"0"``] 460 \\ ASSUME_TAC (Q.SPEC `c` (SIMP_RULE (std_ss++SIZES_ss) [] (INST_TYPE [``:'a``|->``:7``] w2n_lt))) 461 \\ `48 + w2n c < 256` by DECIDE_TAC 462 \\ FULL_SIMP_TAC std_ss [stringTheory.ORD_CHR_RWT] 463 THEN1 464 (`(g (r2 + 0x1w) = n2w (48 + w2n c)) /\ r2 + 0x1w IN dg` by SEP_READ_TAC 465 \\ ASM_SIMP_TAC std_ss [w2w_w2w_n2w_lemma] 466 \\ Q.ABBREV_TAC `f2 = (a + 0x4w =+ n2w (w2n c)) ((a =+ 0xE9w) f)` 467 \\ `w2n c < 256` by DECIDE_TAC 468 \\ `(r * one (a,0xE9w) * one (a + 0x1w,y'') * one (a + 0x2w,y''') * 469 one (a + 0x3w,y'''') * one_space (a + 0x5w) (CODE_LENGTH ns) b2 * 470 one (a + 0x4w,n2w (w2n (c:word7)))) (fun2set (f2,df))` by 471 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC) 472 \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o Q.SPECL [`w2n (c:word7)`,`ns1`,`y`, 473 `r * one (a,0xE9w) * one (a + 0x1w,y'') * 474 one (a + 0x2w,y''') * one (a + 0x3w,y'''') * 475 one_space (a + 0x5w) (CODE_LENGTH ns) b2`, 476 `b2`,`f2`,`df`,`a+4w`,`r4`,`r3`]) x86_addr_thm 477 \\ ASM_SIMP_TAC std_ss [GSYM w2w_def,word_arith_lemma1] 478 \\ SIMP_TAC std_ss [WORD_SUB_PLUS] 479 \\ Q.ABBREV_TAC `imm = ADDR ns1 r4 (w2n c) - a - 0x5w` 480 \\ SIMP_TAC std_ss [LSR_ADD,WORD_ADD_0,word_arith_lemma3,word_arith_lemma4] 481 \\ ASM_SIMP_TAC std_ss [] 482 \\ Q.PAT_ASSUM `!xx.bb` MATCH_MP_TAC 483 \\ Q.EXISTS_TAC `x * one (r2,0x6Aw) * one (r2 + 0x1w,n2w (48 + w2n (c:word7)))` 484 \\ Q.EXISTS_TAC `b1` \\ Q.EXISTS_TAC `b2` \\ Q.EXISTS_TAC `y` 485 \\ ASM_SIMP_TAC std_ss [] \\ SEP_WRITE_TAC) 486 THEN1 487 (`(g (r2 + 0x1w) = n2w (48 + w2n c)) /\ r2 + 0x1w IN dg` by SEP_READ_TAC 488 \\ ASM_SIMP_TAC std_ss [w2w_w2w_n2w_lemma] 489 \\ Q.PAT_ABBREV_TAC `f2 = (a + 0x7w =+ (n2w (w2n (c:word7))):word8) ff` 490 \\ `w2n c < 256` by DECIDE_TAC 491 \\ `(r * one (a,0x3Bw) * one (a + 0x1w,7w) * one (a + 0x2w,0xFw) * 492 one (a + 0x3w,0x84w) * one (a + 0x4w,y''''') * 493 one (a + 0x5w,y'''''') * one (a + 0x6w,y''''''') * 494 one_space (a + 0x8w) (CODE_LENGTH ns) b2 * 495 one (a + 0x7w,n2w (w2n (c:word7)))) (fun2set (f2,df))` by 496 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC) 497 \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o Q.SPECL [`w2n (c:word7)`,`ns1`,`y`, 498 `r * one (a,0x3Bw) * one (a + 0x1w,0x7w) * one (a + 0x2w,0xFw) * 499 one (a + 0x3w,0x84w) * one (a + 0x4w,y''''') * 500 one (a + 0x5w,y'''''') * one (a + 0x6w,y''''''') * 501 one_space (a + 0x8w) (CODE_LENGTH ns) b2`, 502 `b2`,`f2`,`df`,`a+7w`,`r4`,`r3`]) x86_addr_thm 503 \\ ASM_SIMP_TAC std_ss [GSYM w2w_def,word_arith_lemma1] 504 \\ SIMP_TAC std_ss [WORD_SUB_PLUS] 505 \\ Q.ABBREV_TAC `imm = ADDR ns1 r4 (w2n c) - a - 0x8w` 506 \\ SIMP_TAC std_ss [LSR_ADD,WORD_ADD_0,word_arith_lemma3,word_arith_lemma4] 507 \\ ASM_SIMP_TAC std_ss [] 508 \\ Q.PAT_ASSUM `!xx.bb` MATCH_MP_TAC 509 \\ Q.EXISTS_TAC `x * one (r2,0x3Dw) * one (r2 + 0x1w,n2w (48 + w2n (c:word7)))` 510 \\ Q.EXISTS_TAC `b1` \\ Q.EXISTS_TAC `b2` \\ Q.EXISTS_TAC `y` 511 \\ ASM_SIMP_TAC std_ss [] 512 \\ SEP_WRITE_TAC) 513 THEN1 514 (`(g (r2 + 0x1w) = n2w (48 + w2n c)) /\ r2 + 0x1w IN dg` by SEP_READ_TAC 515 \\ ASM_SIMP_TAC std_ss [w2w_w2w_n2w_lemma] 516 \\ Q.PAT_ABBREV_TAC `f2 = (a + 0x7w =+ (n2w (w2n (c:word7))):word8) ff` 517 \\ `w2n c < 256` by DECIDE_TAC 518 \\ `(r * one (a,0x3Bw) * one (a + 0x1w,7w) * one (a + 0x2w,0xFw) * 519 one (a + 0x3w,0x82w) * one (a + 0x4w,y''''') * 520 one (a + 0x5w,y'''''') * one (a + 0x6w,y''''''') * 521 one_space (a + 0x8w) (CODE_LENGTH ns) b2 * 522 one (a + 0x7w,n2w (w2n (c:word7)))) (fun2set (f2,df))` by 523 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC) 524 \\ (STRIP_ASSUME_TAC o UNDISCH_ALL o RW [GSYM AND_IMP_INTRO] o Q.SPECL [`w2n (c:word7)`,`ns1`,`y`, 525 `r * one (a,0x3Bw) * one (a + 0x1w,0x7w) * one (a + 0x2w,0xFw) * 526 one (a + 0x3w,0x82w) * one (a + 0x4w,y''''') * 527 one (a + 0x5w,y'''''') * one (a + 0x6w,y''''''') * 528 one_space (a + 0x8w) (CODE_LENGTH ns) b2`, 529 `b2`,`f2`,`df`,`a+7w`,`r4`,`r3`]) x86_addr_thm 530 \\ ASM_SIMP_TAC std_ss [GSYM w2w_def,word_arith_lemma1] 531 \\ SIMP_TAC std_ss [WORD_SUB_PLUS] 532 \\ Q.ABBREV_TAC `imm = ADDR ns1 r4 (w2n c) - a - 0x8w` 533 \\ SIMP_TAC std_ss [LSR_ADD,WORD_ADD_0,word_arith_lemma3,word_arith_lemma4] 534 \\ ASM_SIMP_TAC std_ss [] 535 \\ Q.PAT_ASSUM `!xx.bb` MATCH_MP_TAC 536 \\ Q.EXISTS_TAC `x * one (r2,0x3Cw) * one (r2 + 0x1w,n2w (48 + w2n (c:word7)))` 537 \\ Q.EXISTS_TAC `b1` \\ Q.EXISTS_TAC `b2` \\ Q.EXISTS_TAC `y` 538 \\ ASM_SIMP_TAC std_ss [] 539 \\ SEP_WRITE_TAC)); 540 541val x86_codegen_thm = save_thm("x86_codegen_thm",let 542 val th = SPEC_ALL x86_codegen_loop_lemma 543 val th = Q.INST [`y`|->`x`,`r4`|->`a`,`ns1`|->`ns`,`r3`|->`r2`] th 544 val th = RW [GSYM CONJ_ASSOC,GSYM SEP_CODE_IN_MEM_def] (RW [CONJ_ASSOC] th) 545 val cc = SIMP_CONV std_ss [LET_DEF] THENC DEPTH_CONV FORCE_PBETA_CONV 546 THENC SIMP_CONV std_ss [LET_DEF] 547 val def1 = CONV_RULE cc x86_codegen_def 548 val pre1 = CONV_RULE cc x86_codegen_pre_def 549 val th = RW [GSYM def1,GSYM pre1] (Q.INST [`a`|->`r1`] th) 550 in th end); 551 552val SEP_CODE_IN_MEM_LOOP_thm = prove( 553 ``!ns a ns1 a2 x. 554 (x * SEP_CODE_IN_MEM_LOOP a ns (a1,ns1)) (fun2set (f,df)) ==> 555 !p n. 556 (iFETCH p ns = SOME n) ==> 557 (let branch = \j. ADDR ns1 a1 j - ADDR ns a p in 558 BYTES_IN_MEM (ADDR ns a p) df f (X86_ENCODE branch n))``, 559 Induct THEN1 SIMP_TAC std_ss [iFETCH_def] 560 \\ SIMP_TAC std_ss [iFETCH_def,LET_DEF] 561 \\ REPEAT STRIP_TAC \\ REVERSE (Cases_on `p`) 562 \\ FULL_SIMP_TAC std_ss [] 563 THEN1 564 (FULL_SIMP_TAC std_ss [ADDR_def,SEP_CODE_IN_MEM_LOOP_def,LET_DEF, 565 STAR_ASSOC,DECIDE ``~(SUC n = 0)``] \\ RES_TAC 566 \\ FULL_SIMP_TAC std_ss [LENGTH_X86_ENCODE,GSYM xENC_LENGTH_def]) 567 \\ Q.PAT_ASSUM `!xx.bb` (K ALL_TAC) 568 \\ Cases_on `n` 569 \\ FULL_SIMP_TAC std_ss [SEP_BYTES_IN_MEM_def,ADDR_def,STAR_ASSOC, 570 SEP_CODE_IN_MEM_LOOP_def,LET_DEF,SEP_BYTES_IN_MEM_def,X86_ENCODE_def, 571 BYTES_IN_MEM_def,SEP_CLAUSES,X86_IMMEDIATE_def,APPEND] 572 \\ SEP_READ_TAC); 573 574val SEP_CODE_IN_MEM_IMP = store_thm("SEP_CODE_IN_MEM_IMP", 575 ``!x a ns f df xs l p ns. 576 (x * SEP_CODE_IN_MEM a ns) (fun2set (f,df)) ==> 577 CODE_IN_MEM (xs,l,p,ns) a df f``, 578 SIMP_TAC std_ss [SEP_CODE_IN_MEM_def] \\ REPEAT STRIP_TAC 579 \\ IMP_RES_TAC SEP_CODE_IN_MEM_LOOP_thm 580 \\ FULL_SIMP_TAC std_ss [CODE_IN_MEM_def,LET_DEF]); 581 582fun subst_SPEC_PC th tm = let 583 val p = find_term (can (match_term ``aPC p``)) (cdr (concl th)) handle e => 584 find_term (can (match_term ``pPC p``)) (cdr (concl th)) handle e => 585 find_term (can (match_term ``xPC p``)) (cdr (concl th)) 586 val p = cdr p 587 val tm = subst [mk_var("p",``:word32``) |-> p] tm 588 in tm end; 589 590val _ = write_code_to_file "codegen.s" x86_codegen_th 591 592val x86_codegen_better = save_thm("x86_codegen_better",let 593 val th = Q.INST [`eax`|->`r1`,`edx`|->`r2`] x86_codegen_th 594 val tm = (fst o dest_imp o concl) x86_codegen_thm 595 val th = SPEC_BOOL_FRAME_RULE th tm 596 val (th,goal) = SPEC_WEAKEN_RULE th (subst_SPEC_PC th `` 597 xCODE_IN_MEM df ns * xBYTE_MEMORY dg g * ~xR EAX * ~xR EBX * 598 ~xR ECX * ~xR EDI * ~xR EDX * xPC p * ~xS``) 599 val lemma = prove(goal, 600 SIMP_TAC std_ss [SEP_IMP_MOVE_COND] \\ REPEAT STRIP_TAC 601 \\ IMP_RES_TAC x86_codegen_thm 602 \\ NTAC 2 (POP_ASSUM (K ALL_TAC)) 603 \\ ASM_SIMP_TAC std_ss [LET_DEF,xCODE_IN_MEM_def,SEP_CLAUSES] 604 \\ IMP_RES_TAC SEP_CODE_IN_MEM_IMP 605 \\ SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_def,SEP_EXISTS] 606 \\ REPEAT STRIP_TAC 607 \\ Q.EXISTS_TAC `fi` 608 \\ Q.EXISTS_TAC `r1` 609 \\ FULL_SIMP_TAC (std_ss++star_ss) [cond_STAR] 610 \\ FULL_SIMP_TAC std_ss [CODE_IN_MEM_def]) 611 val th = MP th lemma 612 val th = RW [SPEC_MOVE_COND,AND_IMP_INTRO] th 613 val tm2 = (fst o dest_imp o concl) th 614 val goal = mk_imp(tm,tm2) 615 val lemma = prove(goal, 616 SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 617 \\ IMP_RES_TAC x86_codegen_thm); 618 val th = DISCH_ALL (MP th (UNDISCH lemma)) 619 val th = RW [GSYM SPEC_MOVE_COND] th 620 in th end); 621 622 623val _ = export_theory(); 624