Changeset 2032 for src/ASM/Assembly.ma
 Timestamp:
 Jun 8, 2012, 4:32:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2028 r2032 212 212 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with 213 213 [ DATA16 w ⇒ λ_. 214 let b1_b2 ≝ split ? 8 8 w in214 let b1_b2 ≝ vsplit ? 8 8 w in 215 215 let b1 ≝ \fst b1_b2 in 216 216 let b2 ≝ \snd b1_b2 in … … 364 364 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 365 365 [ ADDR11 w ⇒ λ_. 366 let v1_v2 ≝ split ? 3 8 w in366 let v1_v2 ≝ vsplit ? 3 8 w in 367 367 let v1 ≝ \fst v1_v2 in 368 368 let v2 ≝ \snd v1_v2 in … … 372 372 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 373 373 [ ADDR11 w ⇒ λ_. 374 let v1_v2 ≝ split ? 3 8 w in374 let v1_v2 ≝ vsplit ? 3 8 w in 375 375 let v1 ≝ \fst v1_v2 in 376 376 let v2 ≝ \snd v1_v2 in … … 382 382 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 383 383 [ ADDR16 w ⇒ λ_. 384 let b1_b2 ≝ split ? 8 8 w in384 let b1_b2 ≝ vsplit ? 8 8 w in 385 385 let b1 ≝ \fst b1_b2 in 386 386 let b2 ≝ \snd b1_b2 in … … 390 390 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 391 391 [ ADDR16 w ⇒ λ_. 392 let b1_b2 ≝ split ? 8 8 w in392 let b1_b2 ≝ vsplit ? 8 8 w in 393 393 let b1 ≝ \fst b1_b2 in 394 394 let b2 ≝ \snd b1_b2 in … … 431 431 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 432 432 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in 433 let 〈upper, lower〉 ≝ split ? 8 8 result in433 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 434 434 if eq_bv ? upper (zero 8) then 435 435 let address ≝ RELATIVE lower in … … 535 535  Comment comment ⇒ [ ] 536 536  Call call ⇒ 537 let 〈addr_5, resta〉 ≝ split ? 5 11 (sigma (lookup_labels call)) in537 let 〈addr_5, resta〉 ≝ vsplit ? 5 11 (sigma (lookup_labels call)) in 538 538 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 539 539 let do_a_long ≝ policy ppc in 540 let 〈pc_5, restp〉 ≝ split ? 5 11 pc_plus_jmp_length in540 let 〈pc_5, restp〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in 541 541 if eq_bv ? addr_5 pc_5 ∧ ¬ do_a_long then 542 542 let address ≝ ADDR11 resta in … … 554 554 let lookup_address ≝ sigma (lookup_labels jmp) in 555 555 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_address false in 556 let 〈upper, lower〉 ≝ split ? 8 8 result in556 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 557 557 if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then 558 558 let address ≝ RELATIVE lower in 559 559 [ SJMP address ] 560 560 else 561 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (sigma (lookup_labels jmp)) in562 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc_plus_jmp_length in561 let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (sigma (lookup_labels jmp)) in 562 let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in 563 563 if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then 564 564 let address ≝ ADDR11 rest_addr in … … 866 866 867 867 (*CSC: FALSE!!!*) 868 axiom fetch_pseudo_instruction_ split:868 axiom fetch_pseudo_instruction_vsplit: 869 869 ∀instr_list,ppc. 870 870 ∃pre,suff,lbl. … … 936 936 cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %] 937 937 #res #K 938 cases (fetch_pseudo_instruction_ split (\snd program) ppc) #pre * #suff * #lbl #EQ1938 cases (fetch_pseudo_instruction_vsplit (\snd program) ppc) #pre * #suff * #lbl #EQ1 939 939 generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?; 940 940 cases daemon (* CSC: XXXXXXXX Ero qui
Note: See TracChangeset
for help on using the changeset viewer.