 Timestamp:
 Jun 10, 2011, 6:36:55 PM (10 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r922 r938 202 202 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with 203 203 [ DATA16 w ⇒ λ_. 204 let 〈b1,b2〉 ≝ split ? 8 8 w in 204 let b1_b2 ≝ split ? 8 8 w in 205 let b1 ≝ \fst b1_b2 in 206 let b2 ≝ \fst b1_b2 in 205 207 [ ([[true;false;false;true;false;false;false;false]]); b1; b2] 206 208  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] … … 352 354 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 353 355 [ ADDR11 w ⇒ λ_. 354 let 〈v1,v2〉 ≝ split ? 3 8 w in 356 let v1_v2 ≝ split ? 3 8 w in 357 let v1 ≝ \fst v1_v2 in 358 let v2 ≝ \snd v1_v2 in 355 359 [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] 356 360  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) … … 358 362 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 359 363 [ ADDR11 w ⇒ λ_. 360 let 〈v1,v2〉 ≝ split ? 3 8 w in 364 let v1_v2 ≝ split ? 3 8 w in 365 let v1 ≝ \fst v1_v2 in 366 let v2 ≝ \snd v1_v2 in 361 367 [ (v1 @@ [[false; false; false; false; true]]) ; v2 ] 362 368  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) … … 366 372 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 367 373 [ ADDR16 w ⇒ λ_. 368 let 〈b1,b2〉 ≝ split ? 8 8 w in 374 let b1_b2 ≝ split ? 8 8 w in 375 let b1 ≝ \fst b1_b2 in 376 let b2 ≝ \snd b1_b2 in 369 377 [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ] 370 378  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) … … 372 380 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 373 381 [ ADDR16 w ⇒ λ_. 374 let 〈b1,b2〉 ≝ split ? 8 8 w in 382 let b1_b2 ≝ split ? 8 8 w in 383 let b1 ≝ \fst b1_b2 in 384 let b2 ≝ \snd b1_b2 in 375 385 [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ] 376 386  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 
src/ASM/AssemblyProof.ma
r937 r938 1761 1761  Comment comment ⇒ 〈0, 0〉 1762 1762  Cost cost ⇒ 〈0, 0〉 1763  Jmp jmp ⇒ 〈 0, 2〉1764  Call call ⇒ 〈 0, 2〉1765  Mov dptr tgt ⇒ 〈 0, 2〉1763  Jmp jmp ⇒ 〈2, 2〉 1764  Call call ⇒ 〈2, 2〉 1765  Mov dptr tgt ⇒ 〈2, 2〉 1766 1766 ]. 1767 1767 cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *) … … 1984 1984 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 1985 1985 #H2 >(eq_bv_to_eq … H2) >EQ % 1986 4: (* Jmp *) 1986 4: (* Jmp *) #label 1987 whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta; 1988 [3: (* long *) #H1 #H2 #EQ %[@1] 1989 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 1990 change in ⊢ (? → ??%?) with (execute_1_0 ??) 1991 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 1992 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 1993 >H2b >(eq_instruction_to_eq … H2a) 1994 generalize in match EQ; EQ; 1995 (*whd in ⊢ (???% → ??%?);*) 1996 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) 1997 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX % 1998  (* short *) 1999  (* medium *) 2000 ] *) 1987 2001 5: (* Call *) 1988 2002 6: (* Mov *)
Note: See TracChangeset
for help on using the changeset viewer.