Changeset 914


Ignore:
Timestamp:
Jun 9, 2011, 11:10:16 AM (8 years ago)
Author:
boender
Message:
  • complete.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r913 r914  
    446446  let pn ≝ nat_of_bitvector ? pc in
    447447  let pa ≝ nat_of_bitvector ? address in
    448    if ltb (distance pn pa) 512 then
     448   if ltb (distance pn pa) 127 then
    449449    〈2, Some ? short_jump〉
    450450   else
     
    637637qed.
    638638
    639 (* let 〈new_labels, new_policy, ch〉 =
    640  jump_expansion_policy_internal program old_labels old_policy in
    641  if changed then recurse else stop *)
    642  
     639let rec jump_expansion_internal (n: nat) (program: pseudo_assembly_program)
     640 (old_labels: BitVectorTrie Word 16) (old_policy: BitVectorTrie jump_length 16)
     641 on n: jump_expansion_policy ≝
     642 match n with
     643 [ O ⇒ old_policy
     644 | S n' ⇒
     645   let 〈new_labels, new_policy, ch〉 ≝
     646    jump_expansion_policy_internal program old_labels old_policy in
     647    jump_expansion_internal n' program new_labels new_policy ].
     648         
     649definition jump_expansion ≝
     650 λpc.λprogram.
     651  let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in
     652  lookup ? ? pc policy long_jump.
     653 
    643654definition assembly_1_pseudoinstruction ≝
    644655  λprogram: pseudo_assembly_program.
     
    647658  λlookup_datalabels.
    648659  λi.
    649   let expansion ≝ long_jump (* XXX temporarily, s.t. it compiles *) in
     660  let expansion ≝ jump_expansion pc program in
    650661    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
    651662    [ None ⇒ None ?
Note: See TracChangeset for help on using the changeset viewer.