Changeset 3034


Ignore:
Timestamp:
Mar 29, 2013, 2:39:40 PM (4 years ago)
Author:
sacerdot
Message:

Bug fixed: COST instructions are now assembled as NOP to prevent the following
situation:

COST k

l: ...

...
JMP l

where the jump used to emit the label. The patch is a bit rough: we could avoid
the COST if nobody is jumping/calling the instruction just after it. But we
do not know how to decide it. Thus we should associate label emission to pairs
of PC (from-to). This patch is simpler, but it leaves a few NOPs in the
generated code.

Files:
4 edited

Legend:

Unmodified
Added
Removed
  • extracted/assembly.ml

    r2999 r3034  
    26522652  expand_relative_jump lookup_labels sigma policy ppc instr
    26532653| ASM.Comment comment -> List.Nil
    2654 | ASM.Cost cost -> List.Nil
     2654| ASM.Cost cost -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil)
    26552655| ASM.Jmp jmp ->
    26562656  let pc_plus_jmp_length =
     
    27902790let assembly p sigma policy =
    27912791  (let { Types.fst = labels_to_ppc; Types.snd = ppc_to_costs } =
    2792      Fetch.create_label_cost_map p.ASM.code
     2792     Fetch.create_label_cost_map (ASM.code p)
    27932793   in
    27942794  (fun _ ->
    2795   let preamble = p.ASM.preamble in
    2796   let instr_list = p.ASM.code in
     2795  let preamble = ASM.preamble p in
     2796  let instr_list = ASM.code p in
    27972797  let datalabels = Status.construct_datalabels preamble in
    27982798  let lookup_labels = fun x ->
     
    28512851      symboltable) (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    28522852    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    2853     (Nat.S Nat.O))))))))))))))))) p.ASM.renamed_symbols); ASM.final_pc =
    2854   (sigma (lookup_labels p.ASM.final_label)) })) __)) __
     2853    (Nat.S Nat.O))))))))))))))))) (ASM.renamed_symbols p)); ASM.final_pc =
     2854  (sigma (lookup_labels (ASM.final_label p))) })) __)) __
    28552855
    28562856(** val ticks_of_instruction : ASM.instruction -> Nat.nat **)
     
    31593159   | ASM.JMP x -> assert false (* absurd case *))
    31603160| ASM.Comment comment -> { Types.fst = Nat.O; Types.snd = Nat.O }
    3161 | ASM.Cost cost -> { Types.fst = Nat.O; Types.snd = Nat.O }
     3161| ASM.Cost cost ->
     3162  let ticks = ticks_of_instruction (ASM.RealInstruction ASM.NOP) in
     3163  { Types.fst = ticks; Types.snd = ticks }
    31623164| ASM.Jmp jmp ->
    31633165  let pc_plus_jmp_length =
     
    32203222let ticks_of program sigma policy ppc =
    32213223  let { Types.fst = labels; Types.snd = costs } =
    3222     Fetch.create_label_cost_map program.ASM.code
     3224    Fetch.create_label_cost_map (ASM.code program)
    32233225  in
    32243226  let addr_of = fun id ->
     
    32293231  in
    32303232  let { Types.fst = fetched; Types.snd = new_ppc } =
    3231     ASM.fetch_pseudo_instruction program.ASM.code ppc
     3233    ASM.fetch_pseudo_instruction (ASM.code program) ppc
    32323234  in
    32333235  ticks_of0 program addr_of sigma policy ppc fetched
  • extracted/policyFront.ml

    r2773 r3034  
    197197| ASM.Instruction instr -> expand_relative_jump_unsafe jmp_len instr
    198198| ASM.Comment comment -> List.Nil
    199 | ASM.Cost cost -> List.Nil
     199| ASM.Cost cost -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil)
    200200| ASM.Jmp jmp ->
    201201  (match jmp_len with
  • src/ASM/Assembly.ma

    r2999 r3034  
    525525  λi.
    526526  match i with
    527   [ Cost cost ⇒ [ ]
     527  [ Cost cost ⇒ [ NOP … ]
    528528  | Comment comment ⇒ [ ]
    529529  | Call call ⇒
     
    12231223      ]
    12241224    | Comment comment ⇒ 〈0, 0〉
    1225     | Cost cost ⇒ 〈0, 0〉
     1225    | Cost cost ⇒
     1226       let ticks ≝ ticks_of_instruction (NOP ?) in
     1227         〈ticks, ticks〉
    12261228    | Jnz _ _ _ ⇒ ? (*CSC: To be implemented*)
    12271229    | MovSuccessor _ _ _ ⇒ ? (*CSC: To be implemented *)
  • src/ASM/PolicyFront.ma

    r2713 r3034  
    137137  λi.
    138138  match i with
    139   [ Cost cost ⇒ [ ]
     139  [ Cost cost ⇒ [ NOP … ]
    140140  | Comment comment ⇒ [ ]
    141141  | Call call ⇒
Note: See TracChangeset for help on using the changeset viewer.