Changeset 907


Ignore:
Timestamp:
Jun 8, 2011, 6:15:26 PM (9 years ago)
Author:
boender
Message:
  • added quadruples to Util
  • start of implementation of new jump expansion policy
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r846 r907  
    424424  | long_jump: jump_length.
    425425
    426 axiom jump_expansion_policy:
    427   ∀program: pseudo_assembly_program.
    428   ∀pc: Word.
    429    jump_length.
    430 
     426definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
     427
     428definition 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
     439definition distance ≝
     440 λx.λy.if gtb x y then x - y else y - x.
     441 
     442definition 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
     453definition 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 
     460definition 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 
     474definition 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 
    431515definition expand_relative_jump_internal:
    432516 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
     
    563647  λlookup_datalabels.
    564648  λi.
    565   let expansion ≝ jump_expansion_policy program pc in
     649  let expansion ≝ jump_expansion_policy policy_zero program pc in
    566650    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
    567651    [ None ⇒ None ?
  • src/ASM/Util.ma

    r900 r907  
    189189interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
    190190
     191notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
     192with precedence 90 for @{ 'quadruple $a $b $c $d}.
     193interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)).
     194
     195notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
     196 with precedence 10
     197for @{ 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
    191199notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
    192200 with precedence 10
Note: See TracChangeset for help on using the changeset viewer.