Changeset 685 for Deliverables/D2.2


Ignore:
Timestamp:
Mar 16, 2011, 2:36:28 PM (9 years ago)
Author:
ayache
Message:

Bug fix in LINToASM (wrong conditional translation) in 8051 branch.

Location:
Deliverables/D2.2/8051
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051/myocamlbuild_config.ml

    r664 r685  
    1 let parser_lib = "/home/dpm/Projects/Cerco/Deliverables/D2.2/8051/lib"
     1let parser_lib = "/home/ayache/Downloads/Bol/Deliverables/D2.2/8051/lib"

  • Deliverables/D2.2/8051/src/LIN/LINToASM.ml

    r631 r685  
    7777    [`Call f]
    7878  | LIN.St_condacc lbl ->
    79     assert false (* particular case treated in translate_code *)
     79    [`WithLabel (`JNZ (`Label lbl))]
    8080  | LIN.St_return ->
    8181    [`RET]
    8282
    83 (** [remove_following_cost_label lbl code] first finds the label instruction of
    84     [lbl]. It supposes that [lbl] is the destination of a conditional
    85     statement. Thus, it is followed by a cost instruction. The result is then
    86     this cost label and the code without this particular cost instruction. *)
    87 
    88 let rec remove_following_cost_label lbl = function
    89   | [] -> (None, []) (* no labelling *)
    90   | LIN.St_label lbl' :: LIN.St_cost cost_lbl :: code when lbl' = lbl ->
    91     (Some cost_lbl, LIN.St_label lbl' :: code)
    92   | stmt :: code ->
    93     let (cost_lbl, code') = remove_following_cost_label lbl code in
    94     (cost_lbl, stmt :: code')
    95 
    96 let translate_code tmp_universe glbls_addr =
    97   let rec aux = function
    98     | [] -> []
    99     | LIN.St_condacc lbl :: code ->
    100       (* The conditional statement requires a special treatment. See the .mli
    101          for details. We have to pay a special attention to the cost labels, so
    102          as to not introduce an imprecision. *)
    103       let (cost_lbl, code') = remove_following_cost_label lbl code in
    104       (match cost_lbl with
    105         | None -> aux code'
    106         | Some cost_lbl ->
    107           let tmp_lbl = Label.Gen.fresh tmp_universe in
    108           [`WithLabel (`JZ (`Label tmp_lbl)) ;
    109            `Cost cost_lbl ; `NOP (* TODO: hack! Need to make the difference between cost labels and regular labels. *) ; `Jmp lbl ;
    110            `Label tmp_lbl] @
    111             (aux code'))
    112     | stmt :: code -> (translate_statement glbls_addr stmt) @ (aux code) in
    113   aux
     83let translate_code glbls_addr code =
     84  List.flatten (List.map (translate_statement glbls_addr) code)
    11485
    11586
    116 let translate_fun_def tmp_universe glbls_addr (id, def) = match def with
    117   | LIN.F_int code ->
    118     (`Label id) :: (translate_code tmp_universe glbls_addr code)
     87let translate_fun_def glbls_addr (id, def) = match def with
     88  | LIN.F_int code -> (`Label id) :: (translate_code glbls_addr code)
    11989  | _ -> []
    12090
    121 let translate_functs tmp_universe glbls_addr exit_label main functs =
     91let translate_functs glbls_addr exit_label main functs =
    12292  let preamble = match main with
    12393    | None -> []
    12494    | Some main -> [`Call main ; `Label exit_label ; `Jmp exit_label] in
    12595  preamble @
    126     (List.flatten (List.map (translate_fun_def tmp_universe glbls_addr) functs))
     96    (List.flatten (List.map (translate_fun_def glbls_addr) functs))
    12797
    12898
    … …  
    134104(* Translating programs.
    135105
    136    A fresh universe is create, in order to create an exit label and fresh labels
    137    for the expansion of conditional instructions (see the .mli).
    138 
    139106   Global variables are associated an offset from the base of the external
    140107   memory. *)
    … …  
    143110  let prog_lbls = prog_labels p in
    144111  let exit_label = Label.Gen.fresh_prefix prog_lbls "_exit" in
    145   let fresh_tmp =
    146     Label.Gen.fresh_prefix (Label.Set.add exit_label prog_lbls) "_tmp_lbl" in
    147   let tmp_universe = Label.Gen.new_universe fresh_tmp in
    148112  let glbls_addr = globals_addr p.LIN.vars in
    149113  let p =
    … …  
    151115      ASM.pexit_label = exit_label ;
    152116      ASM.pcode =
    153         translate_functs tmp_universe glbls_addr exit_label p.LIN.main
    154           p.LIN.functs ;
     117        translate_functs glbls_addr exit_label p.LIN.main p.LIN.functs ;
    155118      ASM.phas_main = p.LIN.main <> None } in
    156119  ASMInterpret.assembly p

  • Deliverables/D2.2/8051/src/LIN/LINToASM.mli

    r486 r685  
    1212    In 8051, a program is supposed to run forever. A preamble that contains
    1313    two instructions is added: the first calls the main, and the second
    14     infinitely jumps to itself once the main has returned.
    15 
    16     Since conditional jumps are very restricted in 8051 (only 8 bits relative),
    17     these instructions are expanded as follows in order to jump further away. A
    18     jump instruction is added after the condition. Its destination is the
    19     destination of the condition. The condition is replaced by its opposite, the
    20     destination being the instruction following the previously added jump
    21     instruction. The translation looks like this:
    22 
    23     JNZ lbl   ->   JZ lbl'
    24     ...            j  lbl
    25     lbl:           lbl':
    26                    ...
    27                    lbl:
    28 
    29     But in fact, this introduces an imprecision in the cost prediction. Indeed,
    30     after labelling the source code, a condition instruction looks like this
    31     (and beside is the same transformation):
    32 
    33     JNZ lbl     ->   JZ lbl'
    34     emit cost1       j  lbl
    35     ...              lbl':
    36     lbl:             emit cost1
    37     emit cost2       ...
    38                      lbl:
    39                      emit cost2
    40 
    41     As we can see, if the condition JZ holds, then the flow directly goes to
    42     lbl' and reaches [emit cost1] without having executed a single costly
    43     instruction (labelling is not an instruction). On the other hand, if the
    44     condition JZ does not hold, the flow reaches a [j lbl] which has a non nul
    45     cost, then goes to lbl and finally reaches [emit cost2]. Depending on the
    46     condition JZ, the cost of the paths to the next cost label is not the
    47     same. To cope with this problem, the emission of cost2 is moved before the
    48     jump to lbl, as depicted below.
    49 
    50     JNZ lbl     ->   JZ lbl'
    51     emit cost1       emit cost2
    52     ...              j  lbl
    53     lbl:             lbl':
    54     emit cost2       emit cost1
    55                      ...
    56                      lbl:
    57 *)
     14    infinitely jumps to itself once the main has returned. *)
    5815
    5916val translate : LIN.program -> ASM.program
Note: See TracChangeset for help on using the changeset viewer.