 Timestamp:
 Jun 8, 2011, 6:15:26 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r846 r907 424 424  long_jump: jump_length. 425 425 426 axiom jump_expansion_policy: 427 ∀program: pseudo_assembly_program. 428 ∀pc: Word. 429 jump_length. 430 426 definition jump_expansion_policy ≝ BitVectorTrie jump_length 16. 427 428 definition find_right_call: Word → Word → nat × (option jump_length) ≝ 429 (* medium call: 11 bits, only in "current segment" *) 430 (* can this be done more efficiently with bit vector arithmetic? *) 431 λpc.λaddress. 432 let 〈p1, p2〉 ≝ split ? 5 11 address in 433 let 〈a1, a2〉 ≝ split ? 5 11 pc in 434 if eq_bv ? p1 a1 then (* we're in the same segment *) 435 〈2, Some ? medium_jump〉 436 else 437 〈3, Some ? long_jump〉. 438 439 definition distance ≝ 440 λx.λy.if gtb x y then x  y else y  x. 441 442 definition find_right_jump: Word → Word → nat × (option jump_length) ≝ 443 (* short jump: 8 bits signed *) 444 (* medium jump: 11 bits, forward only *) 445 λpc.λaddress. 446 let pn ≝ nat_of_bitvector ? pc in 447 let pa ≝ nat_of_bitvector ? address in 448 if ltb (distance pn pa) 512 then 449 〈2, Some ? short_jump〉 450 else 451 find_right_call pc address. 452 453 definition find_right_relative_jump: Word → (BitVectorTrie Word 16) → 454 Identifier → nat × (option jump_length) ≝ 455 λpc.λlabels.λjmp. 456 match lookup_opt ? ? jmp labels with 457 [ None ⇒ 〈2, Some ? short_jump〉 458  Some a ⇒ find_right_jump pc a ]. 459 460 definition jep_relative: Word → (BitVectorTrie Word 16) → preinstruction Identifier → ? ≝ 461 λpc.λlabels.λi. 462 match i with 463 [ JC jmp ⇒ find_right_relative_jump pc labels jmp 464  JNC jmp ⇒ find_right_relative_jump pc labels jmp 465  JB baddr jmp ⇒ find_right_relative_jump pc labels jmp 466  JZ jmp ⇒ find_right_relative_jump pc labels jmp 467  JNZ jmp ⇒ find_right_relative_jump pc labels jmp 468  JBC baddr jmp ⇒ find_right_relative_jump pc labels jmp 469  JNB baddr jmp ⇒ find_right_relative_jump pc labels jmp 470  CJNE addr jmp ⇒ find_right_relative_jump pc labels jmp 471  DJNZ addr jmp ⇒ find_right_relative_jump pc labels jmp 472  _ ⇒ 〈length ? (assembly_preinstruction ? (λx.zero ?) i), None …〉 ]. 473 474 definition jump_expansion_policy_internal: pseudo_assembly_program → 475 (BitVectorTrie Word 16) → jump_expansion_policy → 476 ((BitVectorTrie Word 16) × jump_expansion_policy × bool)≝ 477 λprogram.λlabels.λpolicy. 478 let 〈pc, new_labels, new_policy, changed〉 ≝ 479 foldl ? ? (λacc.λi:labelled_instruction. 480 let 〈label, instr〉 ≝ i in 481 let 〈pc,labels,policy,c0〉 ≝ acc in 482 let 〈c1,new_labels〉 ≝ match label with 483 [ None ⇒ 〈c0,labels〉 484  Some l ⇒ 485 match update ? ? pc l labels with 486 [ None ⇒ 〈c0,labels〉 487  Some x ⇒ 〈true, x〉 ] ] in 488 let 〈pc_delta, jmp_len〉 ≝ match instr with 489 [ Call c ⇒ 490 match lookup_opt ? ? c new_labels with 491 [ None ⇒ 〈2, Some ? medium_jump〉 492  Some c_addr ⇒ find_right_call pc c_addr ] 493  Jmp j ⇒ 494 match lookup_opt ? ? j new_labels with 495 [ None ⇒ 〈2, Some ? short_jump〉 496  Some j_addr ⇒ find_right_jump pc j_addr ] 497  Instruction i ⇒ jep_relative pc new_labels i 498  Mov _ _ ⇒ (* XXX is this correct? *) 〈2, None …〉 499  Cost _ ⇒ 〈0, None …〉 500  Comment _ ⇒ 〈0, None …〉 ] in 501 let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 502 match jmp_len with 503 [ None ⇒ 〈new_pc, new_labels, policy, c1〉 504  Some j ⇒ 505 match update ? ? pc j policy with 506 [ None ⇒ 〈new_pc, new_labels, policy, c1〉 507  Some x ⇒ 〈new_pc, new_labels, x, true〉 ] ] 508 ) 〈zero ?, labels, policy, false〉 (\snd program) in 509 〈labels, policy, changed〉. 510 511 (* let 〈new_labels, new_policy, ch〉 = 512 jump_expansion_policy_internal program old_labels old_policy in 513 if changed then recurse else stop *) 514 431 515 definition expand_relative_jump_internal: 432 516 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) → … … 563 647 λlookup_datalabels. 564 648 λi. 565 let expansion ≝ jump_expansion_policy p rogram pc in649 let expansion ≝ jump_expansion_policy policy_zero program pc in 566 650 match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with 567 651 [ None ⇒ None ? 
src/ASM/Util.ma
r900 r907 189 189 interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z). 190 190 191 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)" 192 with precedence 90 for @{ 'quadruple $a $b $c $d}. 193 interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)). 194 195 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)" 196 with precedence 10 197 for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }. 198 191 199 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)" 192 200 with precedence 10
Note: See TracChangeset
for help on using the changeset viewer.