Changeset 1572 for Deliverables


Ignore:
Timestamp:
Nov 28, 2011, 3:13:14 PM (8 years ago)
Author:
tranquil
Message:
  • corrected previous bug
  • finished propagating immediates
Location:
Deliverables/D2.2/8051/src
Files:
21 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/ERTL/ERTL.mli

    r1568 r1572  
    9191  (* Push a value from a register to the IRAM. Parameter are the source
    9292     register, and the label of the next statement. *)
    93   | St_push of Register.t * Label.t
     93  | St_push of argument * Label.t
    9494
    9595  (* Assign the most significant bits of the address of a symbol to a
     
    115115     operation, the destination register, the source registers, and the label of
    116116     the next statement. *)
    117   | St_opaccsA of I8051.opaccs * Register.t * Register.t * Register.t * Label.t
     117  | St_opaccsA of I8051.opaccs * Register.t * argument * argument * Label.t
    118118
    119119  (* Apply a binary operation that will later be translated in an operation on
     
    121121     operation, the destination register, the source registers, and the label of
    122122     the next statement. *)
    123   | St_opaccsB of I8051.opaccs * Register.t * Register.t * Register.t * Label.t
     123  | St_opaccsB of I8051.opaccs * Register.t * argument * argument * Label.t
    124124
    125125  (* Apply an unary operation. Parameters are the operation, the destination
     
    129129  (* Apply a binary operation. Parameters are the operation, the destination
    130130     register, the source registers, and the label of the next statement. *)
    131   | St_op2 of I8051.op2 * Register.t * Register.t * argument * Label.t
     131  | St_op2 of I8051.op2 * Register.t * argument * argument * Label.t
    132132
    133133  (* Set the carry flag to zero. Parameter is the label of the next
     
    141141     address registers (low bytes first), and the label of the next
    142142     statement. *)
    143   | St_load of Register.t * Register.t * Register.t * Label.t
     143  | St_load of Register.t * argument * argument * Label.t
    144144
    145145  (* Store to external memory. Parameters are the address registers (low bytes
    146146     first), the source register, and the label of the next statement. *)
    147   | St_store of Register.t * Register.t * Register.t * Label.t
     147  | St_store of argument * argument * argument * Label.t
    148148
    149149  (* Call to a function given its name. Parameters are the name of the function,
     
    173173
    174174  (* Transfer control to the address stored in the return address registers. *)
    175   | St_return of registers
     175  | St_return of argument list
    176176
    177177type graph = statement Label.Map.t
  • Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml

    r1568 r1572  
    207207  st
    208208
    209 let make_addr st r1 r2 = List.map (fun r -> get_reg (Psd r) st) [r1 ; r2]
     209let make_addr st r1 r2 = List.map (fun r -> get_arg r st) [r1 ; r2]
    210210
    211211
     
    318318
    319319    | ERTL.St_push (srcr, lbl) ->
    320       let v = get_reg (Psd srcr) st in
     320      let v = get_arg srcr st in
    321321      let st = push st v in
    322322      next_pc st lbl
     
    343343      let (v, _) =
    344344        Eval.opaccs opaccs
    345           (get_reg (Psd srcr1) st)
    346           (get_reg (Psd srcr2) st) in
     345          (get_arg srcr1 st)
     346          (get_arg srcr2 st) in
    347347      let st = add_reg (Psd destr) v st in
    348348      next_pc st lbl
     
    351351      let (_, v) =
    352352        Eval.opaccs opaccs
    353           (get_reg (Psd srcr1) st)
    354           (get_reg (Psd srcr2) st) in
     353          (get_arg srcr1 st)
     354          (get_arg srcr2 st) in
    355355      let st = add_reg (Psd destr) v st in
    356356      next_pc st lbl
     
    364364      let (v, carry) =
    365365        Eval.op2 st.carry op2
    366           (get_reg (Psd srcr1) st)
     366          (get_arg srcr1 st)
    367367          (get_arg srcr2 st) in
    368368      let st = change_carry st carry in
     
    386386    | ERTL.St_store (addr1, addr2, srcr, lbl) ->
    387387      let addr = make_addr st addr1 addr2 in
    388       let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
     388      let mem = Mem.store st.mem chunk addr (get_arg srcr st) in
    389389      let st = change_mem st mem in
    390390      next_pc st lbl
     
    394394
    395395    | ERTL.St_call_ptr (f1, f2, _, lbl) ->
    396       interpret_call lbls_offs st (make_addr st f1 f2) lbl
     396      interpret_call lbls_offs st (make_addr st (RTL.Reg f1) (RTL.Reg f2)) lbl
    397397
    398398    | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
     
    436436
    437437let compute_result st ret_regs =
    438   let vs = List.map (fun r -> get_reg (Psd r) st) ret_regs in
     438  let vs = List.map (fun r -> get_arg r st) ret_regs in
    439439  let f res v = res && (Val.is_int v) in
    440440  let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in
  • Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml

    r1568 r1572  
    2323    first (MiscPottier.string_of_list sep f rl) last
    2424
     25let print_arg = function
     26  | RTL.Imm i -> string_of_int i
     27  | RTL.Reg r -> Register.print r
     28
    2529let print_ptr rl = print_reg_list "[" "]" " ; " Register.print rl
    2630
    2731let print_args rl = print_reg_list "(" ")" ", " Register.print rl
    2832
    29 let print_return rl = print_reg_list "[" "]" " ; " Register.print rl
     33let print_return rl = print_reg_list "[" "]" " ; " print_arg rl
    3034
    3135let print_params rl = print_reg_list "(" ")" ", " Register.print rl
     
    3640
    3741let print_result rl = print_reg_list "[" "]" " ; " Register.print rl
    38 
    39 let print_arg = function
    40   | RTL.Imm i -> string_of_int i
    41   | RTL.Reg r -> Register.print r
    4242
    4343let print_statement = function
     
    7070    Printf.sprintf "pop %s --> %s" (Register.print r) lbl
    7171  | ERTL.St_push (r, lbl) ->
    72     Printf.sprintf "push %s --> %s" (Register.print r) lbl
     72    Printf.sprintf "push %s --> %s" (print_arg r) lbl
    7373  | ERTL.St_addrH (dstr, id, lbl) ->
    7474    Printf.sprintf "addrH %s, %s --> %s" (Register.print dstr) id lbl
     
    8484      (I8051.print_opaccs opaccs)
    8585      (Register.print dstr)
    86       (Register.print srcr1)
    87       (Register.print srcr2)
     86      (print_arg srcr1)
     87      (print_arg srcr2)
    8888      lbl
    8989  | ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, lbl) ->
     
    9191      (I8051.print_opaccs opaccs)
    9292      (Register.print dstr)
    93       (Register.print srcr1)
    94       (Register.print srcr2)
     93      (print_arg srcr1)
     94      (print_arg srcr2)
    9595      lbl
    9696  | ERTL.St_op1 (op1, dstr, srcr, lbl) ->
     
    104104      (I8051.print_op2 op2)
    105105      (Register.print dstr)
    106       (Register.print srcr1)
     106      (print_arg srcr1)
    107107      (print_arg srcr2)
    108108      lbl
     
    114114    Printf.sprintf "load %s, (%s, %s) --> %s"
    115115      (Register.print dstr)
    116       (Register.print addr1)
    117       (Register.print addr2)
     116      (print_arg addr1)
     117      (print_arg addr2)
    118118      lbl
    119119  | ERTL.St_store (addr1, addr2, srcr, lbl) ->
    120120    Printf.sprintf "store (%s, %s), %s --> %s"
    121       (Register.print addr1)
    122       (Register.print addr2)
    123       (Register.print srcr)
     121      (print_arg addr1)
     122      (print_arg addr2)
     123      (print_arg srcr)
    124124      lbl
    125125  | ERTL.St_call_id (f, nb_args, lbl) ->
     
    148148
    149149
    150 let print_graph n c =
     150let print_graph n c entry =
    151151  let f lbl stmt s =
    152152    Printf.sprintf "%s%s: %s\n%s"
     
    155155      (print_statement stmt)
    156156      s in
    157   Label.Map.fold f c ""
     157  ERTLUtilities.dfs_fold f c entry ""
     158  (* Label.Map.fold f c "" *)
    158159
    159160
     
    173174    (n_spaces (n+2))
    174175    def.ERTL.f_exit
    175     (print_graph (n+2) def.ERTL.f_graph)
     176    (print_graph (n+2) def.ERTL.f_graph def.ERTL.f_entry)
    176177
    177178
  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

    r1568 r1572  
    3333  open I8051
    3434
     35
     36  type argument =
     37    | AColor of I8051.register
     38    | ASpill of AST.immediate
     39    | AImm of AST.immediate
     40
     41  let lookup_as_arg r = match lookup r with
     42    | Spill k -> ASpill k
     43    | Color r -> AColor r
     44
     45  let lookup_arg = function
     46    | RTL.Imm k -> AImm k
     47    | RTL.Reg r -> lookup_as_arg r
     48
    3549  let adjust off = locals - (off + I8051.int_size)
    3650
    37   let get_stack r off l =
    38     let off = adjust off in
    39     let l = generate (LTL.St_from_acc (r, l)) in
    40     let l = generate (LTL.St_load l) in
    41     let l = generate (LTL.St_from_acc (I8051.dph, l)) in
    42     let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
    43     let l = generate (LTL.St_int (I8051.a, 0, l)) in
    44     let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
    45     let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
    46     LTL.St_int (I8051.a, off, l)
    47 
    48   let set_stack_preamble off l =
     51  (* side-effects : dpl, dph, a *)
     52  let move_sp_to_dptr off l =
    4953    let off = adjust off in
    5054    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
     
    5559    LTL.St_int (I8051.a, off, l)
    5660
    57   let set_stack off r l =
     61
     62  (* side-effects : dpl, dph, a *)
     63  let get_stack r off l =
     64    let l =
     65      if I8051.eq_reg r I8051.a then l else generate (LTL.St_from_acc (r, l)) in
     66    let l = generate (LTL.St_load l) in
     67    move_sp_to_dptr off l
     68
     69  (* side-effects : dpl, dph, a *)
     70  let set_stack_not_a off r l =
    5871    let l = generate (LTL.St_store l) in
    5972    let l = generate (LTL.St_to_acc (r, l)) in
    60     set_stack_preamble off l
    61 
     73    move_sp_to_dptr off l
     74
     75  (* side-effects : dpl, dph, sst *)
     76  let set_stack_a off l =
     77    let l = generate (LTL.St_store l) in
     78    let l = generate (set_stack_not_a off I8051.sst l) in
     79    LTL.St_from_acc (I8051.st0, l)
     80
     81  (* side-effects : dpl, dph, st0 if r = a, a if r != a *)
     82  let set_stack off r =
     83    if I8051.eq_reg r I8051.a then set_stack_a off else
     84      set_stack_not_a off r
     85
     86  (* side-effects : dpl, dph, a *)
    6287  let set_stack_int off k l =
    6388    let l = generate (LTL.St_store l) in
    6489    let l = generate (LTL.St_int (I8051.a, k, l)) in
    65     set_stack_preamble off l
    66 
    67   (* let write (r : Register.t) (l : Label.t) : (I8051.register * Label.t) = *)
    68   (*   match lookup r with *)
    69 
    70   (*     | Color hwr -> *)
    71   (*       (\* Pseudo-register [r] has been mapped to hardware register *)
    72   (*          [hwr]. Just write into [hwr] and branch to [l]. *\) *)
    73   (*       (hwr, l) *)
    74 
    75   (*     | Spill off -> *)
    76   (*       (\* Pseudo-register [r] has been mapped to offset [off] in the local zone *)
    77   (*          of the stack. Then, write into [sst] (never allocated) and transfer *)
    78   (*          control to an instruction that copies [sst] in the designated *)
    79   (*          location of the stack before branching to [l]. *\) *)
    80   (*       (I8051.sst, generate (set_stack off I8051.sst l)) *)
    81 
    82 
    83   (* let read (r : Register.t) (stmt : I8051.register -> LTL.statement) = *)
    84   (*   match lookup r with *)
    85   (*     | Color hwr -> *)
    86   (*       (\* Pseudo-register [r] has been mapped to hardware register [hwr]. Just *)
    87   (*          generate statement [stmt] with a reference to register [hwr]. *\) *)
    88   (*       generate (stmt hwr) *)
    89 
    90   (*     | Spill off -> *)
    91   (*       (\* Pseudo-register [r] has been mapped to offset [off] in the local zone *)
    92   (*          of the stack. Issue a statement that copies the designated area in *)
    93   (*          the stack into the temporary unallocatable hardware register [sst], *)
    94   (*          then generate statement [stmt] with a reference to register *)
    95   (*          [sst]. *\) *)
    96   (*       let temphwr = I8051.sst in *)
    97   (*       let l = generate (stmt temphwr) in *)
    98   (*       generate (get_stack temphwr off l) *)
    99 
    100 
    101   let move (dest : decision) (src : decision) l =
    102     match dest, src with
    103 
    104       (* Both pseudo-registers are translated to hardware registers. Issue move
    105          statements, or no statement at all if both pseudo-registers reside in
    106          the same hardware register. *)
    107       | Color desthwr, Color sourcehwr when I8051.eq_reg desthwr sourcehwr ->
    108         LTL.St_skip l
    109       | Color desthwr, Color sourcehwr when I8051.eq_reg desthwr I8051.a ->
    110         LTL.St_to_acc (sourcehwr, l)
    111       | Color desthwr, Color sourcehwr when I8051.eq_reg sourcehwr I8051.a ->
    112         LTL.St_from_acc (desthwr, l)
    113       | Color desthwr, Color sourcehwr ->
    114         let l = generate (LTL.St_from_acc (desthwr, l)) in
    115         LTL.St_to_acc (sourcehwr, l)
    116 
    117       (* One pseudo-register is translated to a hardware register, while the
    118          other is spilled. Issue a single stack access instruction. *)
    119       | Color desthwr, Spill off -> get_stack desthwr off l
    120       | Spill off, Color sourcehwr -> set_stack off sourcehwr l
    121 
    122       (* Both pseudo-registers are spilled. Combine the previous two cases. Of
    123          course, if the two pseudo-registers have been spilled into the same
    124          stack slot, there is nothing to do. *)
    125       | Spill off1, Spill off2 when off1 = off2 ->
    126         LTL.St_skip l
    127       | Spill off1, Spill off2 ->
    128         let temphwr = I8051.sst in
    129         let l = generate (set_stack off1 temphwr l) in
    130         get_stack temphwr off2 l
    131 
     90    move_sp_to_dptr off l
     91
     92
     93  (* side-effects : (dpl, dph, a) if dest spilled *)
    13294  let move_int (dest : decision) (k : int) l =
    13395    match dest with
     
    13597      | Spill off -> set_stack_int off k l
    13698
    137   let op2 op (dest : decision) (src1 : decision) (src2 : decision) l =
    138     let l = generate (move dest (Color I8051.a) l) in
     99  (* side-effects : none if dest = src, a if both colored,
     100                    (dpl, dph, a) if src spilled or src imm and dest spilled,
     101                    (dpl, dph, a, sst) if dest spilled *)
     102  let move (dest : decision) (src : argument) l =
     103    match dest, src with
     104      | _, AImm k -> move_int dest k l
     105      (* Both pseudo-registers are translated to hardware registers. Issue move
     106         statements, or no statement at all if both pseudo-registers reside in
     107         the same hardware register. *)
     108      | Color desthwr, AColor sourcehwr
     109        when I8051.eq_reg desthwr sourcehwr ->
     110        LTL.St_skip l
     111      | Color desthwr, AColor sourcehwr
     112        when I8051.eq_reg desthwr I8051.a ->
     113        LTL.St_to_acc (sourcehwr, l)
     114      | Color desthwr, AColor sourcehwr
     115        when I8051.eq_reg sourcehwr I8051.a ->
     116        LTL.St_from_acc (desthwr, l)
     117      | Color desthwr, AColor sourcehwr ->
     118        let l = generate (LTL.St_from_acc (desthwr, l)) in
     119        LTL.St_to_acc (sourcehwr, l)
     120
     121      (* One pseudo-register is translated to a hardware register, while the
     122         other is spilled. Issue a single stack access instruction. *)
     123      | Color desthwr, ASpill off -> get_stack desthwr off l
     124      | Spill off, AColor sourcehwr -> set_stack off sourcehwr l
     125
     126      (* Both pseudo-registers are spilled. Combine the previous two cases. Of
     127         course, if the two pseudo-registers have been spilled into the same
     128         stack slot, there is nothing to do. *)
     129      | Spill off1, ASpill off2 when off1 = off2 ->
     130        LTL.St_skip l
     131      | Spill off1, ASpill off2 ->
     132        let l = generate (set_stack_a off1 l) in
     133        get_stack I8051.a off2 l
     134
     135  (* side-effects (dpl, dph) if either spilled, (dpl, dph, b) if both *)
     136  let op2 op (dest : decision) (src1 : argument) (src2 : argument) l =
     137    let l = generate (move dest (AColor I8051.a) l) in
    139138    match op, src1, src2 with
    140       | _, _, Color src2hwr ->
     139      | _, _, AImm k ->
     140        let l = generate (LTL.St_op2 (op, LTL.Imm k, l)) in
     141        move (Color I8051.a) src1 l
     142        (* if op is commutative, we can do as above if first is hwr *)
     143      | (Add | Addc | And | Or | Xor), AImm k, _ ->
     144        let l = generate (LTL.St_op2 (op, LTL.Imm k, l)) in
     145        move (Color I8051.a) src2 l
     146      | _, _, AColor src2hwr ->
    141147        let l = generate (LTL.St_op2 (op, LTL.Reg src2hwr, l)) in
    142148        move (Color I8051.a) src1 l
    143         (* if op is commutative, we can do as above if first is hwr *)
    144       | (Add | Addc | And | Or | Xor), Color src1hwr, _ ->
     149      | (Add | Addc | And | Or | Xor), AColor src1hwr, _ ->
    145150        let l = generate (LTL.St_op2 (op, LTL.Reg src1hwr, l)) in
    146151        move (Color I8051.a) src2 l
    147         (* otherwise we have to use b *)
    148       | _ ->
     152      | _, _, _ ->
    149153        let l = generate (LTL.St_op2 (op, LTL.Reg I8051.b, l)) in
    150154        let l = generate (move (Color I8051.a) src1 l) in
    151155        move (Color I8051.b) src2 l
    152156
    153   let move_to_dptr (addr1 : decision) (addr2 : decision) l =
     157  (* side-effects : a, b if both spilled *)
     158  let move_to_dptr (addr1 : argument) (addr2 : argument) l =
    154159    match addr1, addr2 with
    155       | Color _, _ ->
     160      | ASpill _, ASpill _  ->
     161        let l = generate (move (Color I8051.dph) (AColor I8051.b) l) in
     162        let l = generate (move (Color I8051.dpl) addr1 l) in
     163        move (Color I8051.b) addr2 l
     164      | (AColor _ | AImm _) , _ ->
    156165        (* the following does not change dph, as addr1 is hwr *)
    157166        let l = generate (move (Color I8051.dpl) addr1 l) in
    158167        move (Color I8051.dph) addr2 l
    159       | _, Color _ ->
    160         (* the following does not change dph, as addr1 is hwr *)
     168      | _, (AColor _ | AImm _) ->
     169        (* the following does not change dpl, as addr2 is hwr *)
    161170        let l = generate (move (Color I8051.dph) addr2 l) in
    162171        move (Color I8051.dpl) addr1 l
    163       | _ ->
    164         let l = generate (move (Color I8051.dph) (Color I8051.b) l) in
    165         let l = generate (move (Color I8051.dpl) addr1 l) in
    166         move (Color I8051.b) addr2 l
    167 
    168   let store addr1 addr2 srcr l =
     172
     173  (* side-effects :  dpl, dph, b if both addr spilled,
     174                     st0 if srcr = a or srcr spilled, a if srcrs != a *)
     175  let store (addr1 : argument) (addr2 : argument) (srcr : argument) l =
    169176    let l = generate (LTL.St_store l) in
    170177    match srcr with
    171       | Color _ ->
    172         let l = generate (move (Color I8051.a) srcr l) in
     178      | AColor r when I8051.eq_reg r a ->
     179        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
     180        let l = generate (move_to_dptr addr1 addr2 l) in
     181        LTL.St_from_acc (I8051.st0, l)
     182      | AColor r ->
     183        let l = generate (LTL.St_to_acc (r, l)) in
    173184        move_to_dptr addr1 addr2 l
    174       | _ ->
     185      | AImm k ->
     186        let l = generate (LTL.St_int (I8051.a, k, l)) in
     187        move_to_dptr addr1 addr2 l
     188      | ASpill _ ->
    175189        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
    176190        let l = generate (move_to_dptr addr1 addr2 l) in
     
    227241
    228242      | ERTL.St_get_hdw (destr, sourcehwr, l) ->
    229         move (lookup destr) (Color sourcehwr) l
    230 
    231       | ERTL.St_set_hdw (desthwr, RTL.Reg sourcer, l) ->
    232         move (Color desthwr) (lookup sourcer) l
    233 
    234       | ERTL.St_set_hdw (desthwr, RTL.Imm k, l) ->
    235         move_int (Color desthwr) k l
     243        move (lookup destr) (AColor sourcehwr) l
     244
     245      | ERTL.St_set_hdw (desthwr, sourcer, l) ->
     246        move (Color desthwr) (lookup_arg sourcer) l
    236247
    237248      | ERTL.St_hdw_to_hdw (r1, r2, l) ->
    238         move (Color r1) (Color r2) l
     249        move (Color r1) (AColor r2) l
    239250
    240251      | ERTL.St_newframe l ->
     
    248259
    249260      | ERTL.St_pop (r, l) ->
    250         let l = generate (move (lookup r) (Color I8051.a) l) in
     261        let l = generate (move (lookup r) (AColor I8051.a) l) in
    251262        LTL.St_pop l
    252263
    253264      | ERTL.St_push (r, l) ->
    254265        let l = generate (LTL.St_push l) in
    255         move (Color I8051.a) (lookup r) l
     266        move (Color I8051.a) (lookup_arg r) l
    256267
    257268      | ERTL.St_addrH (r, x, l) ->
    258         let l = generate (move (lookup r) (Color I8051.dph) l) in
     269        let l = generate (move (lookup r) (AColor I8051.dph) l) in
    259270        LTL.St_addr (x, l)
    260271
    261272      | ERTL.St_addrL (r, x, l) ->
    262         let l = generate (move (lookup r) (Color I8051.dpl) l) in
     273        let l = generate (move (lookup r) (AColor I8051.dpl) l) in
    263274        LTL.St_addr (x, l)
    264275
    265       | ERTL.St_move (r, RTL.Imm i, l) ->
    266         move_int (lookup r) i l
    267 
    268       | ERTL.St_move (r1, RTL.Reg r2, l) ->
    269         move (lookup r1) (lookup r2) l
     276      | ERTL.St_move (r, a, l) ->
     277        move (lookup r) (lookup_arg a) l
    270278
    271279      | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
    272         let l = generate (move (lookup destr) (Color I8051.a) l) in
     280        let l = generate (move (lookup destr) (AColor I8051.a) l) in
    273281        let l = generate (LTL.St_opaccs (opaccs, l)) in
    274         let l = generate (move (Color I8051.a) (lookup srcr1) l) in
    275         move (Color I8051.b) (lookup srcr2) l
     282        let l = generate (move (Color I8051.a) (lookup_arg srcr1) l) in
     283        move (Color I8051.b) (lookup_arg srcr2) l
    276284
    277285      | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
    278         let l = generate (move (lookup destr) (Color I8051.b) l) in
     286        let l = generate (move (lookup destr) (AColor I8051.b) l) in
    279287        let l = generate (LTL.St_opaccs (opaccs, l)) in
    280         let l = generate (move (Color I8051.a) (lookup srcr1) l) in
    281         move (Color I8051.b) (lookup srcr2) l
     288        let l = generate (move (Color I8051.a) (lookup_arg srcr1) l) in
     289        move (Color I8051.b) (lookup_arg srcr2) l
    282290
    283291      | ERTL.St_op1 (op1, destr, srcr, l) ->
    284         let l = generate (move (lookup destr) (Color I8051.a) l) in
     292        let l = generate (move (lookup destr) (AColor I8051.a) l) in
    285293        let l = generate (LTL.St_op1 (op1, l)) in
    286         move (Color I8051.a) (lookup srcr) l
    287 
    288       | ERTL.St_op2 (op, destr, srcr1, RTL.Reg srcr2, l) ->
    289         op2 op (lookup destr) (lookup srcr1) (lookup srcr2) l
    290 
    291       | ERTL.St_op2 (op2, destr, srcr1, RTL.Imm k, l) ->
    292         let l = generate (move (lookup destr) (Color I8051.a) l) in
    293         let l = generate (LTL.St_op2 (op2, LTL.Imm k, l)) in
    294         move (Color I8051.a) (lookup srcr1) l
     294        move (Color I8051.a) (lookup_as_arg srcr) l
     295
     296      | ERTL.St_op2 (op, destr, arg1, arg2, l) ->
     297        op2 op (lookup destr) (lookup_arg arg1) (lookup_arg arg2) l
    295298
    296299      | ERTL.St_clear_carry l ->
     
    300303        LTL.St_set_carry l
    301304
    302       (* act differently on hardware registers? if at least one of
    303          the address bytes is hdw use of st0 can be avoided. And in
    304          case of non-hdw, the read could actually target a register
    305          directly *)
    306305      | ERTL.St_load (destr, addr1, addr2, l) ->
    307         let l = generate (move (lookup destr) (Color I8051.a) l) in
     306        let l = generate (move (lookup destr) (AColor I8051.a) l) in
    308307        let l = generate (LTL.St_load l) in
    309         move_to_dptr (lookup addr1) (lookup addr2) l
     308        move_to_dptr (lookup_arg addr1) (lookup_arg addr2) l
    310309
    311310      | ERTL.St_store (addr1, addr2, srcr, l) ->
    312         store (lookup addr1) (lookup addr2) (lookup srcr) l
     311        store (lookup_arg addr1) (lookup_arg addr2) (lookup_arg srcr) l
    313312
    314313      | ERTL.St_call_id (f, _, l) ->
     
    317316      | ERTL.St_call_ptr (f1, f2, _, l) ->
    318317        let l = generate (LTL.St_call_ptr l) in
    319         move_to_dptr (lookup f1) (lookup f2) l
     318        move_to_dptr (lookup_as_arg f1) (lookup_as_arg f2) l
    320319
    321320      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
    322321        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
    323         move (Color I8051.a) (lookup srcr) l
     322        move (Color I8051.a) (lookup_as_arg srcr) l
    324323
    325324      | ERTL.St_return _ ->
  • Deliverables/D2.2/8051/src/ERTL/liveness.ml

    r1568 r1572  
    143143let ret_regs = set_of_list I8051.rets
    144144
     145let add_arg : RTL.argument -> L.property -> L.property = function
     146  | RTL.Reg r -> L.join (L.psingleton r)
     147  | RTL.Imm _ -> fun x -> x
     148
    145149let used (stmt : statement) : L.t =
    146150  match stmt with
     
    156160  (* | St_int _ *)
    157161  | St_clear_carry _
    158   | St_set_carry _
    159   | St_set_hdw (_, RTL.Imm _, _)
    160   | St_move (_, RTL.Imm _, _) ->
     162  | St_set_carry _ ->
    161163    L.bottom
    162164  | St_call_id (_, nparams, _) ->
     
    171173  | St_hdw_to_hdw (_, r, _) ->
    172174    L.hsingleton r
    173   | St_op2 (I8051.Addc, _, r1, RTL.Reg r2, _) ->
    174     L.join (L.join (L.psingleton r1) (L.psingleton r2))
    175       (L.hsingleton I8051.carry)
    176   | St_op2 (I8051.Addc, _, r1, RTL.Imm _, _) ->
    177     L.join (L.psingleton r1) (L.hsingleton I8051.carry)
    178   | St_set_hdw (_, RTL.Reg r, _)
    179   | St_push (r, _)
    180   | St_move (_, RTL.Reg r, _)
    181175  | St_op1 (_, _, r, _)
    182   | St_op2 (_, _, r, RTL.Imm _, _)
    183176  | St_cond (r, _, _) ->
    184177    L.psingleton r
    185   | St_opaccsA (_, _, r1, r2, _)
    186   | St_opaccsB (_, _, r1, r2, _)
    187   | St_op2 (_, _, r1, RTL.Reg r2, _)
    188   | St_load (_, r1, r2, _) ->
    189     L.join (L.psingleton r1) (L.psingleton r2)
    190   | St_store (r1, r2, r3, _) ->
    191     L.join (L.join (L.psingleton r1) (L.psingleton r2)) (L.psingleton r3)
     178  | St_set_hdw (_, a, _)
     179  | St_push (a, _)
     180  | St_move (_, a, _) ->
     181    add_arg a L.bottom
     182  | St_op2 ((I8051.Addc | I8051.Sub), _, a1, a2, _) ->
     183    add_arg a1 (add_arg a2 (L.hsingleton I8051.carry))
     184  | St_opaccsA (_, _, a1, a2, _)
     185  | St_opaccsB (_, _, a1, a2, _)
     186  | St_op2 (_, _, a1, a2, _)
     187  | St_load (_, a1, a2, _) ->
     188    add_arg a1 (add_arg a2 L.bottom)
     189  | St_store (a1, a2, a3, _) ->
     190    add_arg a1 (add_arg a2 (add_arg a3 L.bottom))
    192191  | St_newframe _
    193192  | St_delframe _ ->
  • Deliverables/D2.2/8051/src/ERTL/uses.ml

    r1568 r1572  
    1515let count r uses = Register.Map.add r (lookup uses r + 1) uses
    1616
     17let count_arg = function
     18  | RTL.Reg r -> count r
     19  | RTL.Imm _ -> fun x -> x
     20
    1721let examine_statement _ stmt uses =
    1822  match stmt with
     
    2327  | St_ind_inc _
    2428  | St_hdw_to_hdw _
    25   | St_set_hdw (_, RTL.Imm _, _)
    2629  | St_newframe _
    2730  | St_delframe _
     
    3235    uses
    3336  | St_get_hdw (r, _, _)
    34   | St_set_hdw (_, RTL.Reg r, _)
    3537  | St_framesize (r, _)
    3638  | St_pop (r, _)
    37   | St_push (r, _)
    38   | St_move (r, RTL.Imm _, _)
    3939  | St_addrH (r, _, _)
    4040  | St_addrL (r, _, _)
    4141  | St_cond (r, _, _) ->
    4242    count r uses
    43   | St_move (r1, RTL.Reg r2, _)
    44   | St_op1 (_, r1, r2, _)
    45   | St_op2 (_, r1, r2, RTL.Imm _, _)
    46   | St_call_ptr (r1, r2, _, _) ->
     43  | St_set_hdw (_, a, _)
     44  | St_push (a, _) ->
     45    count_arg a uses
     46  | St_move (r1, a2, _) ->
     47    count r1 (count_arg a2 uses)
     48  | St_call_ptr (r1, r2, _, _)
     49  | St_op1 (_, r1, r2, _) ->
    4750    count r1 (count r2 uses)
    48   | St_opaccsA (_, r1, r2, r3, _)
    49   | St_opaccsB (_, r1, r2, r3, _)
    50   | St_op2 (_, r1, r2, RTL.Reg r3, _)
    51   | St_load (r1, r2, r3, _)
    52   | St_store (r1, r2, r3, _) ->
    53     count r1 (count r2 (count r3 uses))
     51  | St_opaccsA (_, r, a1, a2, _)
     52  | St_opaccsB (_, r, a1, a2, _)
     53  | St_load (r, a1, a2, _)
     54  | St_op2 (_, r, a1, a2, _) ->
     55    count r (count_arg a1 (count_arg a1 uses))
     56  | St_store (a1, a2, a3, _) ->
     57    count_arg a1 (count_arg a2 (count_arg a3 uses))
    5458
    5559let examine_internal int_fun =
  • Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

    r1568 r1572  
    8282  fst (List.fold_left f (Labels_Offsets.empty, Val.Offset.zero) p.LTL.functs)
    8383
    84 let fun_def_of_ptr mem ptr = match Mem.find_fun_def mem ptr with
     84let fun_def_of_ptr mem ptr =
     85  match Mem.find_fun_def mem ptr with
    8586  | LTL.F_int def -> def
    8687  | _ -> error "Trying to fetch the definition of an external function."
  • Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml

    r1568 r1572  
    7171
    7272
    73 let print_graph n c =
     73let print_graph n c entry =
    7474  let f lbl stmt s =
    7575    Printf.sprintf "%s%s: %s\n%s"
     
    7878      (print_statement stmt)
    7979      s in
    80   Label.Map.fold f c ""
     80  LTLUtilities.dfs_fold f c entry ""
     81  (* Label.Map.fold f c "" *)
    8182
    8283
     
    9394    (n_spaces (n+2))
    9495    def.LTL.f_exit
    95     (print_graph (n+2) def.LTL.f_graph)
     96    (print_graph (n+2) def.LTL.f_graph def.LTL.f_entry)
    9697
    9798
  • Deliverables/D2.2/8051/src/RTL/RTL.mli

    r1568 r1572  
    5050     statement. *)
    5151  | St_opaccs of I8051.opaccs * Register.t * Register.t *
    52                                 Register.t * Register.t * Label.t
     52                                argument * argument * Label.t
    5353
    5454  (* Apply an unary operation. Parameters are the operation, the destination
     
    5858  (* Apply a binary operation. Parameters are the operation, the destination
    5959     register, the source arguments, and the label of the next statement. *)
    60   | St_op2 of I8051.op2 * Register.t * Register.t * argument * Label.t
     60  | St_op2 of I8051.op2 * Register.t * argument * argument * Label.t
    6161
    6262  (* Set the carry flag to zero. Parameter is the label of the next
     
    7070     address registers (low bytes first), and the label of the next
    7171     statement. *)
    72   | St_load of Register.t * Register.t * Register.t * Label.t
     72  | St_load of Register.t * argument * argument * Label.t
    7373
    7474  (* Store to external memory. Parameters are the address registers (low bytes
    7575     first), the source register, and the label of the next statement. *)
    76   | St_store of Register.t * Register.t * Register.t * Label.t
     76  | St_store of argument * argument * argument * Label.t
    7777
    7878  (* Call to a function given its name. Parameters are the name of the function,
    7979     the arguments of the function, the destination registers, and the label of
    8080     the next statement. *)
    81   | St_call_id of AST.ident * Register.t list * registers * Label.t
     81  | St_call_id of AST.ident * argument list * registers * Label.t
    8282
    8383  (* Call to a function given its address. Parameters are the registers holding
     
    8585     function, the destination registers, and the label of the next
    8686     statement. *)
    87   | St_call_ptr of Register.t * Register.t * Register.t list * registers *
     87  | St_call_ptr of Register.t * Register.t * argument list * registers *
    8888      Label.t
    8989
    9090  (* Tail call to a function given its name. Parameters are the name of the
    9191     function, and the arguments of the function. *)
    92   | St_tailcall_id of AST.ident * Register.t list
     92  | St_tailcall_id of AST.ident * argument list
    9393
    9494  (* Tail call to a function given its address. Parameters are the registers
    9595     holding the address of the function (low bytes first), and the arguments of
    9696     the function. *)
    97   | St_tailcall_ptr of Register.t * Register.t * Register.t list
     97  | St_tailcall_ptr of Register.t * Register.t * argument list
    9898
    9999  (* Branch. Parameters are the register holding the value for the branching,
     
    103103
    104104  (* Return the value of some registers (low bytes first). *)
    105   | St_return of registers
     105  | St_return of argument list
    106106
    107107
  • Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

    r1568 r1572  
    9494  | RTL.Imm i -> Val.of_int i
    9595
    96 let get_arg_values lenv args = List.map (get_local_value lenv) args
     96let get_arg_values lenv args = List.map (get_local_arg_value lenv) args
    9797
    9898let get_local_addr lenv f1 f2 =
    99   List.map (get_local_value lenv) [f1 ; f2]
     99  List.map (get_local_arg_value lenv) [f1 ; f2]
    100100
    101101
     
    174174        let (v1, v2) =
    175175          Eval.opaccs opaccs
    176             (get_local_value lenv srcr1)
    177             (get_local_value lenv srcr2) in
     176            (get_local_arg_value lenv srcr1)
     177            (get_local_arg_value lenv srcr2) in
    178178        assign_state sfrs graph lbl sp lenv carry mem inds trace
    179179          [destr1 ; destr2] [v1 ; v2]
     
    186186        let (v, carry) =
    187187          Eval.op2 carry op2
    188             (get_local_value lenv srcr1)
     188            (get_local_arg_value lenv srcr1)
    189189            (get_local_arg_value lenv srcr2) in
    190190        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
     
    203203      | RTL.St_store (addr1, addr2, srcr, lbl) ->
    204204        let addr = get_local_addr lenv addr1 addr2 in
    205         let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
     205        let mem = Mem.store mem chunk addr (get_local_arg_value lenv srcr) in
    206206        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    207207
     
    216216
    217217      | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
    218         let addr = get_local_addr lenv f1 f2 in
     218        let addr = get_local_addr lenv (RTL.Reg f1) (RTL.Reg f2) in
    219219        let f_def = Mem.find_fun_def mem addr in
    220220        let args = get_arg_values lenv args in
     
    230230
    231231      | RTL.St_tailcall_ptr (f1, f2, args) ->
    232         let addr = get_local_addr lenv f1 f2 in
     232        let addr = get_local_addr lenv (RTL.Reg f1) (RTL.Reg f2) in
    233233        let f_def = Mem.find_fun_def mem addr in
    234234        let args = get_arg_values lenv args in
     
    241241
    242242      | RTL.St_return rl ->
    243         let vl = List.map (get_local_value lenv) rl in
     243        let vl = List.map (get_local_arg_value lenv) rl in
    244244        let mem = Mem.free mem sp in
    245245        ReturnState (sfrs, vl, mem, inds, trace)
  • Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml

    r1568 r1572  
    3131let print_ptr rl = print_reg_list "[" "]" " ; " print_reg rl
    3232
    33 let print_args rl = print_reg_list "(" ")" ", " print_reg rl
     33let print_args rl = print_reg_list "(" ")" ", " print_arg rl
    3434
    35 let print_return rl = print_reg_list "[" "]" " ; " print_reg rl
     35let print_returned rl = print_reg_list "[" "]" " ; " print_reg rl
     36
     37let print_return rl = print_reg_list "[" "]" " ; " print_arg rl
    3638
    3739let print_params rl = print_reg_list "(" ")" ", " Register.print rl
     
    6971      (print_reg dstr1)
    7072      (print_reg dstr2)
    71       (print_reg srcr1)
    72       (print_reg srcr2)
     73      (print_arg srcr1)
     74      (print_arg srcr2)
    7375      lbl
    7476  | RTL.St_op1 (op1, dstr, srcr, lbl) ->
     
    7981      (I8051.print_op2 op2)
    8082      (print_reg dstr)
    81       (print_reg srcr1)
     83      (print_arg srcr1)
    8284      (print_arg srcr2)
    8385      lbl
     
    8991    Printf.sprintf "load %s, (%s, %s) --> %s"
    9092      (print_reg dstr)
    91       (print_reg addr1)
    92       (print_reg addr2)
     93      (print_arg addr1)
     94      (print_arg addr2)
    9395      lbl
    9496  | RTL.St_store (addr1, addr2, srcr, lbl) ->
    9597    Printf.sprintf "store (%s, %s), %s --> %s"
    96       (print_reg addr1)
    97       (print_reg addr2)
    98       (print_reg srcr)
     98      (print_arg addr1)
     99      (print_arg addr2)
     100      (print_arg srcr)
    99101      lbl
    100102  | RTL.St_call_id (f, args, dstrs, lbl) ->
     
    102104      f
    103105      (print_args args)
    104       (print_return dstrs)
     106      (print_returned dstrs)
    105107      lbl
    106108  | RTL.St_call_ptr (f1, f2, args, dstrs, lbl) ->
     
    109111      (print_reg f2)
    110112      (print_args args)
    111       (print_return dstrs)
     113      (print_returned dstrs)
    112114      lbl
    113115  | RTL.St_tailcall_id (f, args) ->
  • Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

    r1568 r1572  
    100100
    101101let restore_hdws l =
    102   let f (destr, srcr) start_lbl =
    103     adds_graph [ERTL.St_set_hdw (destr, RTL.Reg srcr, start_lbl)] start_lbl in
    104   List.map f (List.map (fun (x, y) -> (y, x)) l)
     102  let f (srcr, destr) start_lbl =
     103    adds_graph [ERTL.St_set_hdw (destr, srcr, start_lbl)] start_lbl in
     104  List.map f l
    105105
    106106let get_params_hdw params =
     
    117117  adds_graph
    118118    [ERTL.St_framesize (addr1, start_lbl) ;
    119      ERTL.St_op2 (I8051.Sub, addr1, addr1, RTL.Imm (off+I8051.int_size),
     119     ERTL.St_op2 (I8051.Sub, addr1, RTL.Reg addr1, RTL.Imm (off+I8051.int_size),
    120120                  start_lbl) ;
    121121     ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
    122      ERTL.St_op2 (I8051.Add, addr1, addr1, RTL.Reg tmpr, start_lbl) ;
     122     ERTL.St_op2 (I8051.Add, addr1, RTL.Reg addr1, RTL.Reg tmpr, start_lbl) ;
    123123     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
    124      ERTL.St_op2 (I8051.Addc, addr2, tmpr, RTL.Imm 0, start_lbl) ;
    125      ERTL.St_load (destr, addr1, addr2, start_lbl)]
     124     ERTL.St_op2 (I8051.Addc, addr2, RTL.Reg tmpr, RTL.Imm 0, start_lbl) ;
     125     ERTL.St_load (destr, RTL.Reg addr1, RTL.Reg addr2, start_lbl)]
    126126    start_lbl dest_lbl def
    127127
     
    203203       (* restore the return address *)
    204204       [adds_graph [ERTL.St_comment ("Restore return address", start_lbl) ;
    205                     ERTL.St_push (srah, start_lbl) ;
    206                     ERTL.St_push (sral, start_lbl)]] @
     205                    ERTL.St_push (RTL.Reg srah, start_lbl) ;
     206                    ERTL.St_push (RTL.Reg sral, start_lbl)]] @
    207207       (* delete frame *)
    208208       [adds_graph [ERTL.St_comment ("Delete frame", start_lbl) ;
     
    225225let add_pro_and_epilogue params ret_regs def =
    226226  (* Allocate registers to hold the return address. *)
    227   let (def, sra) = fresh_regs def 2 in
    228   let sral = List.nth sra 0 in
    229   let srah = List.nth sra 1 in
     227  let (def, sral) = fresh_reg def in
     228  let (def, srah) = fresh_reg def in
    230229  (* Allocate registers to save callee-saved registers. *)
    231230  let (def, sregs) = allocate_regs I8051.callee_saved def in
    232231  (* Add a prologue and a epilogue. *)
    233232  let def = add_prologue params sral srah sregs def in
     233  let sregs = List.map (fun (r, r') -> (RTL.Reg r, r')) sregs in
    234234  let def = add_epilogue ret_regs sral srah sregs def in
    235235  def
     
    238238let set_params_hdw params =
    239239  if List.length params = 0 then
    240     [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
     240    []
    241241  else
    242242    let l = MiscPottier.combine params I8051.parameters in
     
    250250    [ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
    251251     ERTL.St_clear_carry start_lbl ;
    252      ERTL.St_op2 (I8051.Sub, addr1, tmpr, RTL.Imm (off+I8051.int_size),
     252     ERTL.St_op2 (I8051.Sub, addr1, RTL.Reg tmpr, RTL.Imm (off+I8051.int_size),
    253253                  start_lbl) ;
    254254     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
    255      ERTL.St_op2 (I8051.Sub, addr2, tmpr, RTL.Imm 0, start_lbl) ;
    256      ERTL.St_store (addr1, addr2, srcr, start_lbl)]
     255     ERTL.St_op2 (I8051.Sub, addr2, RTL.Reg tmpr, RTL.Imm 0, start_lbl) ;
     256     ERTL.St_store (RTL.Reg addr1, RTL.Reg addr2, srcr, start_lbl)]
    257257    start_lbl dest_lbl def
    258258
  • Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli

    r1568 r1572  
    6161     register, the signature of the function and the label of the next
    6262     statement. *)
    63   | St_call_id of AST.ident * Register.t list * Register.t option *
     63  | St_call_id of AST.ident * argument list * Register.t option *
    6464                  AST.signature * Label.t
    6565
     
    7171     differenciate the two to allow translation to a formalism with no
    7272     function pointer. *)
    73   | St_call_ptr of Register.t * Register.t list * Register.t option *
     73  | St_call_ptr of Register.t * argument list * Register.t option *
    7474                   AST.signature * Label.t
    7575
     
    7777     function, the arguments of the function, the signature of the function and
    7878     the label of the next statement. *)
    79   | St_tailcall_id of AST.ident * Register.t list * AST.signature
     79  | St_tailcall_id of AST.ident * argument list * AST.signature
    8080
    8181  (* Tail call to a function given its address. Parameters are a register
     
    8383     signature of the function and the label of the next statement. Same remark
    8484     as for the [St_call_ptr]. *)
    85   | St_tailcall_ptr of Register.t * Register.t list * AST.signature
     85  | St_tailcall_ptr of Register.t * argument list * AST.signature
    8686
    8787  (* Branch. Parameters are the register holding the value to branch on, the
     
    9696
    9797  (* Return statement. *)
    98   | St_return of Register.t option
     98  | St_return of argument option
    9999
    100100
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

    r1542 r1572  
    8888
    8989let get_value = get_local_env fst
    90 let get_args lenv args = List.map (get_value lenv) args
    9190
    9291let get_type = get_local_env snd
     
    108107let concrete_stacksize = Eval.concrete_stacksize
    109108
     109
     110let eval_arg lenv mem sp = function
     111  | RTLabs.Reg r -> get_value lenv r
     112  | RTLabs.Imm (c, t) -> Eval.cst mem sp t c
     113
     114let get_type_arg lenv = function
     115  | RTLabs.Reg r -> get_type lenv r
     116  | RTLabs.Imm (_, typ) -> typ
     117
     118let get_args lenv mem sp  args = List.map (eval_arg lenv mem sp) args
    110119
    111120(* Assign a value to some destinations registers. *)
     
    130139
    131140let new_ind = CostLabel.new_const_ind
    132 
    133 let eval_arg lenv mem sp = function
    134   | RTLabs.Reg r -> get_value lenv r
    135   | RTLabs.Imm (c, t) -> Eval.cst mem sp t c
    136 
    137 let get_type_arg lenv = function
    138   | RTLabs.Reg r -> get_type lenv r
    139   | RTLabs.Imm (_, typ) -> typ
    140141
    141142(* Interpret statements. *)
     
    205206      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
    206207        let f_def = find_function mem f in
    207         let args = get_args lenv args in
     208        let args = get_args lenv mem sp args in
    208209        (* Save the stack frame. *)
    209210        let sf =
     
    215216        let addr = get_value lenv r in
    216217        let f_def = Mem.find_fun_def mem (address_of_value addr) in
    217         let args = get_args lenv args in
     218        let args = get_args lenv mem sp args in
    218219        (* Save the stack frame. *)
    219220        let sf =
     
    224225      | RTLabs.St_tailcall_id (f, args, sg) ->
    225226        let f_def = find_function mem f in
    226         let args = get_args lenv args in
     227        let args = get_args lenv mem sp args in
    227228        (* No need to save the stack frame. But free the stack. *)
    228229        let mem = Mem.free mem sp in
     
    232233        let addr = get_value lenv r in
    233234        let f_def = Mem.find_fun_def mem (address_of_value addr) in
    234         let args = get_args lenv args in
     235        let args = get_args lenv mem sp args in
    235236        (* No need to save the stack frame. But free the stack. *)
    236237        let mem = Mem.free mem sp in
     
    279280
    280281      | RTLabs.St_return (Some r) ->
    281         let v = get_value lenv r in
     282        let v = eval_arg lenv mem sp r in
    282283        let mem = Mem.free mem sp in
    283284        ReturnState (sfrs, v, mem, inds, trace)
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

    r1568 r1572  
    3030  (Primitive.print_type t) ^ " " ^ (Register.print r)
    3131
    32 let rec print_args args =
    33   Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args)
    34 
    3532let print_result = function
    3633  | None -> "_"
     
    7572  | AST.Cst_offset off -> Printf.sprintf "imm_offset { %s }" (print_offset off)
    7673  | AST.Cst_sizeof t -> "imm_sizeof (" ^ (print_size t) ^ ")"
     74
     75let print_arg = function
     76  | RTLabs.Reg r -> print_reg r
     77  | RTLabs.Imm (c, t) ->
     78    Printf.sprintf "(%s)%s" (Primitive.print_type t) (print_cst c)
     79
     80let rec print_args args =
     81  Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_arg args)
    7782
    7883let string_of_signedness = function
     
    9499  | AST.Op_intofptr -> "intofptr")
    95100        (print_reg r)
    96 
    97 let print_arg = function
    98   | RTLabs.Reg r -> print_reg r
    99   | RTLabs.Imm (c, t) ->
    100     Printf.sprintf "(%s)%s" (Primitive.print_type t) (print_cst c)
    101101
    102102let print_op2 op r s = Printf.sprintf "%s %s %s"
     
    246246        (print_table tbl)
    247247  | RTLabs.St_return None -> Printf.sprintf "return"
    248   | RTLabs.St_return (Some r) -> Printf.sprintf "return %s" (print_reg r)
     248  | RTLabs.St_return (Some r) -> Printf.sprintf "return %s" (print_arg r)
    249249
    250250
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r1568 r1572  
    6666let mem_local_env = Register.Map.mem
    6767let add_local_env = Register.Map.add
    68 let find_local_env = Register.Map.find
     68
     69let rec int_to_args (size : int) = function
     70
     71  | AST.Cst_int i ->
     72    let module M = IntValue.Make (struct let size = size end) in
     73    let chunks = M.break (M.of_int i) size in
     74    List.map (fun x -> RTL.Imm (M.to_int x)) chunks
     75
     76  | AST.Cst_float _ -> error_float ()
     77
     78  | AST.Cst_offset off ->
     79    let i = concrete_offset off in
     80    int_to_args size (AST.Cst_int i)
     81
     82  | AST.Cst_sizeof size' ->
     83    let i = concrete_size size' in
     84    int_to_args size (AST.Cst_int i)
     85
     86  | _ -> assert false (* should not be called on non-int arguments *)
     87
     88let find_local_env_reg = Register.Map.find
     89
     90let find_local_env a env = match a with
     91  | RTLabs.Reg r -> List.map (fun r -> RTL.Reg r) (Register.Map.find r env)
     92  | RTLabs.Imm (k, t) -> int_to_args (size_of_sig_type t) k
    6993
    7094let initialize_local_env runiverse registers result =
     
    76100  List.fold_left f Register.Map.empty registers
    77101
    78 let map_list_local_env lenv regs =
    79   let f res r = res @ (find_local_env r lenv) in
     102let map_list_local_env_reg lenv regs =
     103  let f res r = res @ (find_local_env_reg r lenv) in
    80104  List.fold_left f [] regs
    81105
     
    84108  | _ -> assert false (* do not use on these arguments *)
    85109
    86 let find_and_addr r lenv = make_addr (find_local_env r lenv)
     110let find_and_addr r lenv = make_addr (find_local_env_reg r lenv)
    87111
    88112let rtl_args regs_list lenv =
     
    144168
    145169
    146 (*
    147 
    148 let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    149   match op2, destrs, srcrs1, srcrs2 with
    150 
    151     | AST.Op_mul (1, _), [destr], [srcr1], [srcr2] ->
    152       adds_graph
    153         [RTL.St_opaccs (I8051.Mul, destr, srcr1, srcr2, start_lbl)]
    154         start_lbl dest_lbl def
    155 
    156     | AST.Op_shr _, _, _, _ ->
    157       error_shift ()
    158 
    159     | AST.Op_cmp (AST.Cmp_lt, (1, AST.Unsigned)), [destr], [srcr1], [srcr2] ->
    160       let (def, tmpr) = fresh_reg def in
    161       adds_graph
    162         [RTL.St_clear_carry start_lbl ;
    163          RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ;
    164          RTL.St_int (destr, 0, start_lbl) ;
    165          RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)]
    166         start_lbl dest_lbl def
    167 
    168     | AST.Op_cmp (cmp, ((size, AST.Signed) as int_type)), _, _, _ ->
    169       let (def, tmprs1) = fresh_regs def (List.length srcrs1) in
    170       let (def, tmprs2) = fresh_regs def (List.length srcrs2) in
    171       add_translates
    172         [translate_cst (AST.Cst_int 128) tmprs1 ;
    173          translate_cst (AST.Cst_int 128) tmprs2 ;
    174          translate_op2 (AST.Op_add int_type) tmprs1 srcrs1 tmprs1 ;
    175          translate_op2 (AST.Op_add int_type) tmprs2 srcrs2 tmprs2 ;
    176          translate_op2 (AST.Op_cmp (cmp, (size, AST.Unsigned)))
    177            destrs tmprs1 tmprs2]
    178         start_lbl dest_lbl def
    179 
    180     | AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] ->
    181       let (def, tmpr1) = fresh_reg def in
    182       let (def, tmpr2) = fresh_reg def in
    183       add_translates
    184         [translate_op2 (AST.Op_cmp (AST.Cmp_lt, uint))
    185             [tmpr1] [srcr12] [srcr22] ;
    186          translate_op2 (AST.Op_cmp (AST.Cmp_eq, uint))
    187             [tmpr2] [srcr12] [srcr22] ;
    188          translate_op2 (AST.Op_cmp (AST.Cmp_lt, uint))
    189             [destr] [srcr11] [srcr21] ;
    190          translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
    191          translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
    192         start_lbl dest_lbl def
    193 
    194     | _ -> error_int ()
    195 *)
    196 
    197 let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with
    198 
    199   | AST.Cst_int _ when destrs = [] ->
    200     add_graph start_lbl (RTL.St_skip dest_lbl) def
    201 
    202   | AST.Cst_int i ->
    203     let size = List.length destrs in
    204     let module M = IntValue.Make (struct let size = size end) in
    205     let is = List.map M.to_int (M.break (M.of_int i) size) in
    206     let f r i = RTL.St_move (r, RTL.Imm i, dest_lbl) in
    207     let l = List.map2 f destrs is in
    208     adds_graph l start_lbl dest_lbl def
    209 
    210   | AST.Cst_float _ -> error_float ()
    211 
    212   | AST.Cst_addrsymbol id ->
    213     let (r1, r2) = make_addr destrs in
    214     add_graph start_lbl (RTL.St_addr (r1, r2, id, dest_lbl)) def
    215 
    216   | AST.Cst_stack ->
    217     let (r1, r2) = make_addr destrs in
    218     add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def
    219 
    220   | AST.Cst_offset off ->
    221     let i = concrete_offset off in
    222     translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
    223 
    224   | AST.Cst_sizeof size ->
    225     let i = concrete_size size in
    226     translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
    227 
    228 
    229170let rec translate_move destrs srcrs start_lbl =
    230171  let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
    231   let f_common destr srcr = RTL.St_move (destr, RTL.Reg srcr, start_lbl) in
     172  let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
    232173  let translates1 = adds_graph (List.map2 f_common common1 common2) in
    233174  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
    234175  add_translates [translates1 ; translates2] start_lbl
    235176
    236 let rec translate_imm destrs vals start_lbl =
    237   let ((common1, rest1), (common2, _)) = MiscPottier.reduce destrs vals in
    238   let f_common destr srcr = RTL.St_move (destr, RTL.Imm srcr, start_lbl) in
    239   let translates1 = adds_graph (List.map2 f_common common1 common2) in
    240   let translates2 = translate_cst (AST.Cst_int 0) rest1 in
    241   add_translates [translates1 ; translates2] start_lbl
     177(* translate non-int constants *)
     178and translate_cst cst destrs start_lbl = match destrs, cst with
     179
     180  | [], _ -> adds_graph [] start_lbl
     181
     182  | _, AST.Cst_float _ -> error_float ()
     183
     184  | _, AST.Cst_addrsymbol id ->
     185    let (r1, r2) = make_addr destrs in
     186    adds_graph [RTL.St_addr (r1, r2, id, start_lbl)] start_lbl
     187
     188  | _, AST.Cst_stack ->
     189    let (r1, r2) = make_addr destrs in
     190    adds_graph [RTL.St_stackaddr (r1, r2, start_lbl)] start_lbl
     191
     192  | _ ->
     193    let srcrs = int_to_args (List.length destrs) cst in
     194    translate_move destrs srcrs start_lbl
    242195
    243196
     
    260213     RTL.St_op1 (I8051.Inc, tmpr, tmpr, start_lbl) ;
    261214     RTL.St_op1 (I8051.Cmpl, tmpr, tmpr, start_lbl) ] in
    262   let srcrs = MiscPottier.make tmpr (List.length destrs) in
     215  let srcrs = MiscPottier.make (RTL.Reg tmpr) (List.length destrs) in
    263216  add_translates [adds_graph insts ; translate_move destrs srcrs]
    264217    start_lbl dest_lbl def
     
    273226      let sign_reg = MiscPottier.last srcrs in
    274227      let insts_sign = match src_sign with
    275         | AST.Unsigned -> translate_cast_unsigned rest1
    276         | AST.Signed -> translate_cast_signed rest1 sign_reg in
     228        | AST.Unsigned -> translate_cast_unsigned rest1
     229        | AST.Signed -> translate_cast_signed rest1 sign_reg in
    277230      add_translates [insts_common ; insts_sign]
    278231
    279232
    280233let translate_negint destrs srcrs start_lbl dest_lbl def =
    281   assert (List.length destrs = List.length srcrs && List.length destrs > 0) ;
    282   let f_cmpl destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
     234  let f_cmpl destr = function
     235    | RTL.Reg r -> RTL.St_op1 (I8051.Cmpl, destr, r, start_lbl)
     236    | RTL.Imm k -> RTL.St_move (destr, RTL.Imm (lnot k), start_lbl) in
    283237  let insts_cmpl = List.map2 f_cmpl destrs srcrs in
    284   let first, rest = List.hd destrs, List.tl destrs in
    285   let inst_init =
    286     RTL.St_op2 (I8051.Add, first, first, RTL.Imm 0, start_lbl) in
    287   let f_add destr =
    288     RTL.St_op2 (I8051.Addc, destr, destr, RTL.Imm 0, start_lbl) in
    289   let insts_add = List.map f_add rest in
    290   adds_graph (insts_cmpl @ inst_init :: insts_add)
    291     start_lbl dest_lbl def
     238  match destrs with
     239    | destr :: destrs ->
     240      let inst_init =
     241        RTL.St_op2 (I8051.Add, destr, RTL.Reg destr, RTL.Imm 1, start_lbl) in
     242      let f_add destr =
     243        RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Imm 0, start_lbl) in
     244      let insts_add = List.map f_add destrs in
     245      adds_graph (insts_cmpl @ inst_init :: insts_add)
     246        start_lbl dest_lbl def
     247    | [] ->
     248      adds_graph [] start_lbl dest_lbl def
    292249
    293250
     
    297254    | destr :: destrs, srcr :: srcrs ->
    298255      let (def, tmpr) = fresh_reg def in
    299       let init_destr = RTL.St_move (destr, RTL.Reg srcr, start_lbl) in
     256      let init_destr = RTL.St_move (destr, srcr, start_lbl) in
    300257      let f r =
    301         RTL.St_op2 (I8051.Or, destr, destr, RTL.Reg r, start_lbl) in
     258        RTL.St_op2 (I8051.Or, destr, RTL.Reg destr, r, start_lbl) in
    302259      let big_or = List.map f srcrs in
    303260      let finalize_destr =
    304261        [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
    305262         RTL.St_clear_carry start_lbl ;
    306          RTL.St_op2 (I8051.Sub, tmpr, tmpr, RTL.Reg destr, start_lbl) ;
     263         RTL.St_op2 (I8051.Sub, tmpr, RTL.Reg tmpr, RTL.Reg destr, start_lbl) ;
    307264         (* carry bit is set iff destr is non-zero iff destrs was non-zero *)
    308265         RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
    309          RTL.St_op2 (I8051.Addc, destr, tmpr, RTL.Reg tmpr, start_lbl) ;
     266         RTL.St_op2 (I8051.Addc, destr, RTL.Reg tmpr, RTL.Reg tmpr, start_lbl) ;
    310267         (* destr = carry bit = bigor of old destrs *)
    311          RTL.St_op2 (I8051.Xor, destr, destr, RTL.Imm 1, start_lbl)] in
     268         RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr, RTL.Imm 1, start_lbl)] in
    312269      let epilogue = translate_cst (AST.Cst_int 0) destrs in
    313270      add_translates [adds_graph (init_destr :: big_or @ finalize_destr) ;
     
    331288
    332289  | AST.Op_notint ->
    333     let f destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
     290    let f destr = function
     291      | RTL.Reg srcr ->  RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl)
     292      | RTL.Imm k -> RTL.St_move (destr, RTL.Imm (lnot k), start_lbl) in
    334293    let l = List.map2 f destrs srcrs in
    335294    adds_graph l start_lbl dest_lbl def
     
    354313    | I8051.Add -> assert false (* should not call with add, not correct *)
    355314    | _ -> [] in
    356   let inst_init = RTL.St_move (tmpr, RTL.Imm 0, start_lbl) :: carry_init in
    357315  let f_add destr srcr1 srcr2 =
    358     RTL.St_op2 (op, destr, srcr1, RTL.Reg srcr2, start_lbl) in
     316    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
    359317  let insts_add =
    360318    MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
    361319  let f_add_cted destr srcr =
    362     RTL.St_op2 (op, destr, srcr, RTL.Reg tmpr, start_lbl) in
     320    RTL.St_op2 (op, destr, srcr, RTL.Imm 0, start_lbl) in
    363321  let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
    364322  let f_rest destr =
    365     RTL.St_op2 (op, destr, tmpr, RTL.Reg tmpr, start_lbl) in
     323    match op with
     324      | I8051.Addc | I8051.Sub ->
     325        (* propagate carry bit *)
     326        RTL.St_op2 (op, destr, RTL.Imm 0, RTL.Imm 0, start_lbl)
     327      | _ ->
     328        RTL.St_move (destr, RTL.Imm 0, start_lbl) in
    366329  let insts_rest = List.map f_rest destrs_rest in
    367   adds_graph (inst_init @ insts_add @ insts_add_cted @ insts_rest)
     330  adds_graph (carry_init @ insts_add @ insts_add_cted @ insts_rest)
    368331    start_lbl dest_lbl def
    369332
     
    373336    | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl
    374337    | [destr], [] ->
    375       adds_graph [RTL.St_op2 (I8051.Addc, destr, destr, RTL.Imm 0, start_lbl)]
     338      adds_graph
     339        [RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Imm 0, start_lbl)]
    376340        start_lbl
    377341    | destr1 :: destr2 :: destrs, [] ->
    378342      add_translates
    379343        [adds_graph
    380             [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
    381              RTL.St_op2 (I8051.Addc, destr1, destr1, RTL.Imm 0, start_lbl) ;
    382              RTL.St_op2 (I8051.Addc, destr2, tmpr, RTL.Imm 0, start_lbl)] ;
     344            [RTL.St_op2 (I8051.Addc, destr1,
     345                         RTL.Reg destr1, RTL.Imm 0, start_lbl) ;
     346             RTL.St_op2 (I8051.Addc, destr2, RTL.Imm 0, RTL.Imm 0, start_lbl)] ;
    383347         translate_cst (AST.Cst_int 0) destrs]
    384348        start_lbl
     
    386350      adds_graph
    387351        [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
    388          RTL.St_op2 (I8051.Addc, destr, destr, RTL.Reg tmpr, start_lbl)]
    389         start_lbl
     352         RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Reg tmpr, start_lbl)]
     353        start_lbl
    390354    | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
    391355      add_translates
    392         [adds_graph
    393             [RTL.St_opaccs
    394                 (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
    395              RTL.St_op2 (I8051.Addc, destr1, destr1, RTL.Reg tmpr, start_lbl)] ;
    396          translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
    397         start_lbl
     356        [adds_graph
     357            [RTL.St_opaccs
     358                (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
     359             RTL.St_op2 (I8051.Addc, destr1, RTL.Reg destr1,
     360                         RTL.Reg tmpr, start_lbl)] ;
     361         translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
     362        start_lbl
    398363
    399364let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates
     
    404369      | [] -> []
    405370      | tmp_destr2 :: tmp_destrs2 ->
    406         [adds_graph [RTL.St_clear_carry dummy_lbl ;
    407                      RTL.St_move (tmp_destr2, RTL.Imm 0, dummy_lbl)] ;
    408          translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
    409          translate_cst (AST.Cst_int 0) tmp_destrs1 ;
    410          translate_op I8051.Addc destrs destrs tmp_destrs])
     371        [adds_graph [RTL.St_clear_carry dummy_lbl ;
     372                     RTL.St_move (tmp_destr2, RTL.Imm 0, dummy_lbl)] ;
     373         translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
     374         translate_cst (AST.Cst_int 0) tmp_destrs1 ;
     375         let reg_destrs = List.map (fun r -> RTL.Reg r) destrs in
     376         let tmp_destrs = List.map (fun r -> RTL.Reg r) tmp_destrs in
     377         translate_op I8051.Addc destrs reg_destrs tmp_destrs])
    411378
    412379let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     
    415382  let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
    416383  let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
    417   let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in
     384  (* let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in *)
     385  let reg r = RTL.Reg r in
    418386  let insts_init =
    419387    [translate_move fresh_srcrs1 srcrs1 ;
    420      translate_move fresh_srcrs2 srcrs2 ;
     388     (* translate_move fresh_srcrs2 srcrs2 ; *)
    421389     translate_cst (AST.Cst_int 0) destrs] in
     390  let fresh_srcrs1 = List.map reg fresh_srcrs1 in
    422391  let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
    423392  let insts_mul = MiscPottier.foldi f [] srcrs2 in
     
    448417        | c1hd :: c1tl, c2hd :: c2tl ->
    449418          let init =
    450             RTL.St_op2 (I8051.Xor, destr, c1hd, RTL.Reg c2hd, start_lbl) in
     419            RTL.St_op2 (I8051.Xor, destr, c1hd, c2hd, start_lbl) in
    451420          let f_common tmp_srcr1 tmp_srcr2 =
    452             [RTL.St_op2 (I8051.Xor, tmpr, tmp_srcr1,
    453                          RTL.Reg tmp_srcr2, start_lbl) ;
    454              RTL.St_op2 (I8051.Or, destr, destr, RTL.Reg tmpr, start_lbl)] in
     421            [RTL.St_op2 (I8051.Xor, tmpr, tmp_srcr1, tmp_srcr2, start_lbl) ;
     422             RTL.St_op2 (I8051.Or, destr, RTL.Reg destr,
     423                        RTL.Reg tmpr, start_lbl)] in
    455424          let insts_common = List.flatten (List.map2 f_common c1tl c2tl) in
    456425          init :: insts_common
     
    460429        | _ -> assert false in
    461430      let f_rest tmp_srcr =
    462         RTL.St_op2 (I8051.Xor, destr, destr, RTL.Reg tmp_srcr, start_lbl) in
     431        RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr,
     432                    tmp_srcr, start_lbl) in
    463433      let insts_rest = List.map f_rest rest in
    464434      let insts = firsts @ insts_rest in
     
    472442    | [] -> adds_graph [] start_lbl
    473443    | destr :: _ ->
    474       adds_graph [RTL.St_op1 (I8051.Cmpl, destr, destr, start_lbl)] start_lbl
    475 
    476 
    477 
    478 (* let translate_eq_reg tmp_zero tmpr destr dummy_lbl *)
    479 (*     (srcr1, srcr2) = *)
    480 (*   [RTL.St_op2 (I8051.Xor, tmpr, srcr1, srcr2, dummy_lbl) ; *)
    481 (*    (\* now tmpr = 0 iff srcr1 = srcr2 *\) *)
    482 (*    RTL.St_clear_carry dummy_lbl ; *)
    483 (*    RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmpr, dummy_lbl) ; *)
    484 (*    (\* now carry bit = (old tmpr is not zero) = (srcr1 != srcr2) *\) *)
    485 (*    RTL.St_op2 (I8051.Addc, tmpr, tmp_zero, tmp_zero, dummy_lbl) ; *)
    486 (*    (\* now tmpr = old carry bit = (srcr1 != srcr2) *\) *)
    487 (*    RTL.St_op1 (I8051.Cpl, tmpr, tmpr, dummy_lbl)] *)
    488 
    489 (* let translate_eq_list tmp_zero tmpr destr leq dummy_lbl = match leq with *)
    490 (*   | leqhd :: leqtl -> *)
    491 (*     let init = translate_eq_reg tmp_zero destr dummy_lbl leqhd in *)
    492 (*     let f p = translate_eq_reg tmp_zero tmpr destr dummy_lbl p @ *)
    493 (*       [RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)] in *)
    494 (*     init @ List.flatten (List.map f leqtl) *)
    495 (*   | _ -> [RTL.St_move (destr, RTL.Imm 1, dummy_lbl)] *)
    496 
    497 (* let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq *)
    498 (*     srcr1 srcr2 = *)
    499 (*   (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @ *)
    500 (*   [RTL.St_clear_carry dummy_lbl ; *)
    501 (*    RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ; *)
    502 (*    RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ; *)
    503 (*    RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ; *)
    504 (*    RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)] *)
    505 
    506 (* let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl *)
    507 (*     srcrs1 srcrs2 = *)
    508 (*   let f (insts, leq) srcr1 srcr2 = *)
    509 (*     let added_insts = *)
    510 (*       translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq *)
    511 (*      srcr1 srcr2 in *)
    512 (*     (insts @ added_insts, leq @ [(srcr1, srcr2)]) in *)
    513 (*   fst (List.fold_left2 f ([], []) srcrs1 srcrs2) *)
    514 
    515 (* let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def = *)
    516 (*   match destrs with *)
    517 (*     | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def *)
    518 (*     | _ -> *)
    519 (*       let (def, tmp_destrs) = fresh_regs def (List.length destrs) in *)
    520 (*       let tmp_destr = List.hd tmp_destrs in *)
    521 (*       let (def, tmp_zero) = fresh_reg def in *)
    522 (*       let (def, tmp_one) = fresh_reg def in *)
    523 (*       let (def, tmpr1) = fresh_reg def in *)
    524 (*       let (def, tmpr2) = fresh_reg def in *)
    525 (*       let (def, tmpr3) = fresh_reg def in *)
    526 (*       let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in *)
    527 (*       let srcrs1 = List.rev srcrs1 in *)
    528 (*       let srcrs2 = List.rev srcrs2 in *)
    529 (*       let insts_init = *)
    530 (*      [translate_cst (AST.Cst_int 0) tmp_destrs ; *)
    531 (*       translate_cst (AST.Cst_int 0) added ; *)
    532 (*       adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ; *)
    533 (*                   RTL.St_int (tmp_one, 1, start_lbl)]] in *)
    534 (*       let insts_main = *)
    535 (*      translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl *)
    536 (*        srcrs1 srcrs2 in *)
    537 (*       let insts_main = [adds_graph insts_main] in *)
    538 (*       let insts_exit = [translate_move destrs tmp_destrs] in *)
    539 (*       add_translates (insts_init @ insts_main @ insts_exit ) *)
    540 (*      start_lbl dest_lbl def *)
     444      adds_graph [RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr,
     445                              RTL.Imm 1, start_lbl)] start_lbl
    541446
    542447let rec pad_with p l1 l2 = match l1, l2 with
     
    552457    | [] -> adds_graph [] start_lbl dest_lbl def
    553458    | destr :: destrs ->
    554       let (def, tmpr_zero) = fresh_reg def in
    555       let (srcrs1, srcrs2) = pad_with tmpr_zero srcrs1 srcrs2 in
    556       let init =
    557         [RTL.St_move (tmpr_zero, RTL.Imm 0, start_lbl) ;
    558          RTL.St_clear_carry start_lbl] in
     459      (* not sure that it is the correct thing to do, what about signed?
     460         can really srcrs1 and srcrs2 be of different length? Are not all
     461         correct types enforced? *)
     462      let (srcrs1, srcrs2) = pad_with (RTL.Imm 0) srcrs1 srcrs2 in
     463      let init = RTL.St_clear_carry start_lbl in
    559464      let f srcr1 srcr2 =
    560         RTL.St_op2 (I8051.Sub, destr, srcr1, RTL.Reg srcr2, start_lbl) in
     465        RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) in
    561466      (* not interested in result, just the carry bit
    562467         the following is safe even if destrs = srcrsi *)
    563468      let iter_sub = List.map2 f srcrs1 srcrs2 in
    564469      let extract_carry =
    565         [RTL.St_op2 (I8051.Addc, destr, tmpr_zero,
    566                      RTL.Reg tmpr_zero, start_lbl)] in
     470        [RTL.St_op2 (I8051.Addc, destr, RTL.Imm 0,
     471                     RTL.Imm 0, start_lbl)] in
    567472      let epilogue = translate_cst (AST.Cst_int 0) destrs in
    568       add_translates [adds_graph (init @ iter_sub @ extract_carry);
     473      add_translates [adds_graph (init :: iter_sub @ extract_carry);
    569474                      epilogue] start_lbl dest_lbl def
    570475
    571476let rec add_128_to_last
    572     (tmp_128 : Register.t)
    573477    (last_subst : Register.t)
    574     (rs : Register.t list)
     478    (rs : RTL.argument list)
    575479    (dummy_lbl : Label.t) = match rs with
    576480  | [] -> ([], adds_graph [])
    577481  | [last] ->
    578482    let insts =
    579       [RTL.St_move (last_subst, RTL.Reg last, dummy_lbl) ;
    580        RTL.St_op2 (I8051.Add, last_subst, last_subst,
    581                    RTL.Reg tmp_128, dummy_lbl)] in
    582     ([last_subst], adds_graph insts)
     483      [RTL.St_move (last_subst, last, dummy_lbl) ;
     484       RTL.St_op2 (I8051.Add, last_subst, RTL.Reg last_subst,
     485                   RTL.Imm 128, dummy_lbl)] in
     486    ([RTL.Reg last_subst], adds_graph insts)
    583487  | hd :: tail ->
    584     let (tail', trans) = add_128_to_last tmp_128 last_subst tail dummy_lbl in
     488    let (tail', trans) = add_128_to_last last_subst tail dummy_lbl in
    585489    (hd :: tail', trans)
    586490
    587 (* what happens if srcrs1 and srcrs2 have different length? seems to me
     491(* Paolo: what happens if srcrs1 and srcrs2 have different length? seems to me
    588492   128 is added at the wrong place then *)
    589493let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    590494  let (def, tmp_last_srcr1) = fresh_reg def in
    591495  let (def, tmp_last_srcr2) = fresh_reg def in
    592   let (def, tmp_128) = fresh_reg def in
    593496  (* I save just the last registers *)
    594497  let (srcrs1, add_128_to_srcrs1) =
    595     add_128_to_last tmp_128 tmp_last_srcr1 srcrs1 start_lbl in
     498    add_128_to_last tmp_last_srcr1 srcrs1 start_lbl in
    596499  let (srcrs2, add_128_to_srcrs2) =
    597     add_128_to_last tmp_128 tmp_last_srcr2 srcrs2 start_lbl in
     500    add_128_to_last tmp_last_srcr2 srcrs2 start_lbl in
    598501  add_translates
    599     [adds_graph [RTL.St_move (tmp_128, RTL.Imm 128, start_lbl)] ;
    600      add_128_to_srcrs1;
     502    [add_128_to_srcrs1;
    601503     add_128_to_srcrs2;
    602504     translate_ltu destrs srcrs1 srcrs2]
     
    690592      let tmp_lbl = fresh_label def in
    691593      let init = RTL.St_move (tmpr, RTL.Reg srcr, start_lbl) in
    692       let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, RTL.Reg srcr, start_lbl) in
     594      let f srcr = RTL.St_op2 (I8051.Or, tmpr, RTL.Reg tmpr,
     595                               RTL.Reg srcr, start_lbl) in
    693596      let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
    694597      add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
     
    696599
    697600let translate_load addr destrs start_lbl dest_lbl def =
    698   let (def, save_addr) = fresh_regs def (List.length addr) in
    699   let (def, tmp_addr) = fresh_regs def (List.length addr) in
     601  let (def, tmp_addr) = fresh_regs def 2 in
    700602  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
     603  let save_addr a (saves, def, rs) = match a with
     604    | RTL.Reg r when List.exists (Register.equal r) destrs ->
     605      let (def, tmp) = fresh_reg def in
     606      (RTL.St_move (tmp, RTL.Reg r, start_lbl) :: saves, def, RTL.Reg tmp :: rs)
     607    | _ as a -> (saves, def, a :: rs) in
     608  let (saves, def, addr) = List.fold_right save_addr addr ([], def, []) in
    701609  let (def, tmpr) = fresh_reg def in
    702   let insts_save_addr = translate_move save_addr addr in
    703610  let f (translates, off) r =
    704611    let translates =
    705612      translates @
    706         [adds_graph [RTL.St_move (tmpr, RTL.Imm off, start_lbl)] ;
    707          translate_op2 AST.Op_addp tmp_addr save_addr [tmpr] ;
    708          adds_graph [RTL.St_load (r, tmp_addr1, tmp_addr2, dest_lbl)]] in
     613        [translate_op2 AST.Op_addp tmp_addr addr [RTL.Imm off] ;
     614         adds_graph [RTL.St_load (r, RTL.Reg tmp_addr1,
     615                                  RTL.Reg tmp_addr2, dest_lbl)]] in
    709616    (translates, off + Driver.TargetArch.int_size) in
    710617  let (translates, _) = List.fold_left f ([], 0) destrs in
    711   add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
     618  add_translates translates start_lbl dest_lbl def
    712619
    713620
     
    719626    let translates =
    720627      translates @
    721         [adds_graph [RTL.St_move (tmpr, RTL.Imm off, start_lbl)] ;
    722          translate_op2 AST.Op_addp tmp_addr addr [tmpr] ;
    723          adds_graph [RTL.St_store (tmp_addr1, tmp_addr2, srcr, dest_lbl)]] in
     628        [translate_op2 AST.Op_addp tmp_addr addr [RTL.Imm off] ;
     629         adds_graph [RTL.St_store (RTL.Reg tmp_addr1,
     630                                   RTL.Reg tmp_addr2, srcr, dest_lbl)]] in
    724631    (translates, off + Driver.TargetArch.int_size) in
    725632  let (translates, _) = List.fold_left f ([], 0) srcrs in
     
    742649
    743650  | RTLabs.St_cst (destr, cst, lbl') ->
    744     translate_cst cst (find_local_env destr lenv) lbl lbl' def
     651    translate_cst cst (find_local_env_reg destr lenv) lbl lbl' def
    745652
    746653  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
    747     translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
     654    translate_op1 op1
     655      (find_local_env_reg destr lenv)
     656      (List.map (fun r -> RTL.Reg r) (find_local_env_reg srcr lenv))
    748657      lbl lbl' def
    749658
    750   | RTLabs.St_op2 (op2, destr, RTLabs.Reg srcr1, RTLabs.Reg srcr2, lbl') ->
    751     translate_op2 op2 (find_local_env destr lenv)
     659  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
     660    translate_op2 op2 (find_local_env_reg destr lenv)
    752661      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
    753662
    754   | RTLabs.St_load (_, RTLabs.Reg addr, destr, lbl') ->
    755     translate_load (find_local_env addr lenv) (find_local_env destr lenv)
     663  | RTLabs.St_load (_, addr, destr, lbl') ->
     664    translate_load (find_local_env addr lenv) (find_local_env_reg destr lenv)
    756665      lbl lbl' def
    757666
    758   | RTLabs.St_store (_, RTLabs.Reg addr, RTLabs.Reg srcr, lbl') ->
     667  | RTLabs.St_store (_, addr, srcr, lbl') ->
    759668    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
    760669      lbl lbl' def
     
    765674  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
    766675    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
    767                                    find_local_env retr lenv, lbl')) def
     676                                   find_local_env_reg retr lenv, lbl')) def
    768677
    769678  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
     
    775684    add_graph lbl
    776685      (RTL.St_call_ptr
    777          (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
     686         (f1, f2, rtl_args args lenv, find_local_env_reg retr lenv, lbl')) def
    778687
    779688  | RTLabs.St_tailcall_id (f, args, _) ->
     
    785694
    786695  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
    787     translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
     696    translate_cond (find_local_env_reg r lenv) lbl lbl_true lbl_false def
    788697
    789698  | RTLabs.St_jumptable _ ->
     
    796705    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
    797706
    798   | _ -> assert false (*not possible because of previous removal of immediates*)
    799 
    800 let remove_immediates def =
    801   let load_arg a lbl g rs = match a with
    802     | RTLabs.Reg r -> (lbl, g, rs, r)
    803     | RTLabs.Imm (c, t) ->
    804       let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in
    805       let new_r = Register.fresh def.RTLabs.f_runiverse in
    806       let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in
    807       (new_l, g, (new_r, t) :: rs, new_r) in
    808   let f lbl stmt (g, rs) =
    809     match stmt with
    810       | RTLabs.St_op2(op, r, a1, a2, l) ->
    811         let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
    812         let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
    813         let s = RTLabs.St_op2 (op, r, RTLabs.Reg r1, RTLabs.Reg r2, l) in
    814         let g = Label.Map.add lbl' s g in
    815         (g, rs)
    816       | RTLabs.St_store(q, a1, a2, l) ->
    817         let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
    818         let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
    819         let s = RTLabs.St_store (q, RTLabs.Reg r1, RTLabs.Reg r2, l) in
    820         let g = Label.Map.add lbl' s g in
    821         (g, rs)
    822       | RTLabs.St_load (q, a, r, l) ->
    823         let (lbl', g, rs, r1) = load_arg a lbl g rs in
    824         let s = RTLabs.St_load (q, RTLabs.Reg r1, r, l) in
    825         let g = Label.Map.add lbl' s g in
    826         (g, rs)
    827       | _ -> (g, rs) in
    828   let g = def.RTLabs.f_graph in
    829   let (g, rs) = Label.Map.fold f g (g, []) in
    830   let locals = List.rev_append rs def.RTLabs.f_locals in
    831   { def with RTLabs.f_graph = g; RTLabs.f_locals = locals }
     707(* let remove_non_int_immediates def = *)
     708(*   let load_arg a lbl g rs = match a with *)
     709(*     | RTLabs.Reg r -> (lbl, g, rs, r) *)
     710(*     | RTLabs.Imm ((AST.Cst_stack _ | AST.Cst_addrsymbol _) as c, t) -> *)
     711(*       let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in *)
     712(*       let new_r = Register.fresh def.RTLabs.f_runiverse in *)
     713(*       let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in *)
     714(*       (new_l, g, (new_r, t) :: rs, new_r) in  *)
     715(*   let f lbl stmt (g, rs) = *)
     716(*     match stmt with *)
     717(*       | RTLabs.St_op2(op, r, a1, a2, l) -> *)
     718(*      let (lbl', g, rs, r1) = load_arg a1 lbl g rs in *)
     719(*         let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in *)
     720(*         let s = RTLabs.St_op2 (op, r, RTLabs.Reg r1, RTLabs.Reg r2, l) in *)
     721(*      let g = Label.Map.add lbl' s g in *)
     722(*      (g, rs) *)
     723(*       | RTLabs.St_store(q, a1, a2, l) -> *)
     724(*         let (lbl', g, rs, r1) = load_arg a1 lbl g rs in *)
     725(*         let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in *)
     726(*         let s = RTLabs.St_store (q, RTLabs.Reg r1, RTLabs.Reg r2, l) in *)
     727(*         let g = Label.Map.add lbl' s g in *)
     728(*         (g, rs) *)
     729(*       | RTLabs.St_load (q, a, r, l) -> *)
     730(*         let (lbl', g, rs, r1) = load_arg a lbl g rs in *)
     731(*         let s = RTLabs.St_load (q, RTLabs.Reg r1, r, l) in *)
     732(*         let g = Label.Map.add lbl' s g in *)
     733(*         (g, rs) *)
     734(*       | _ -> (g, rs) in *)
     735(*   let g = def.RTLabs.f_graph in *)
     736(*   let (g, rs) = Label.Map.fold f g (g, []) in *)
     737(*   let locals = List.rev_append rs def.RTLabs.f_locals in *)
     738(*   { def with RTLabs.f_graph = g; RTLabs.f_locals = locals } *)
    832739 
    833740let translate_internal def =
    834   let def = remove_immediates def in
    835741  let runiverse = def.RTLabs.f_runiverse in
    836742  let lenv =
     
    838744      (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
    839745  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
    840   let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in
    841   let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in
     746  let params = map_list_local_env_reg lenv (List.map fst def.RTLabs.f_params) in
     747  let locals = map_list_local_env_reg lenv (List.map fst def.RTLabs.f_locals) in
    842748  let locals = set_of_list locals in
    843749  let result = match def.RTLabs.f_result with
    844750    | None -> []
    845     | Some (r, _) -> find_local_env r lenv in
     751    | Some (r, _) -> find_local_env_reg r lenv in
    846752  let res =
    847753    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsUtilities.ml

    r1569 r1572  
    99  match stmt with
    1010  | St_return _
    11         | St_tailcall_id _
    12         | St_tailcall_ptr _ ->
    13           []
     11  | St_tailcall_id _
     12  | St_tailcall_ptr _ ->
     13    []
    1414  | St_skip l
    1515  | St_cost (_, l)
     
    3131  match stmt with
    3232  | St_return _
    33         | St_tailcall_id _
    34         | St_tailcall_ptr _ -> 0
     33  | St_tailcall_id _
     34  | St_tailcall_ptr _ -> 0
    3535  | St_skip _
    3636  | St_cost _
     
    8383let fill_labels stmt lbls = match stmt, lbls with
    8484  | St_return _, _
    85         | St_tailcall_id _, _
    86         | St_tailcall_ptr _, _ -> stmt
     85  | St_tailcall_id _, _
     86  | St_tailcall_ptr _, _ -> stmt
    8787  | St_skip _, lbl :: _ -> St_skip lbl
    8888  | St_cost (cost_lbl, _), lbl :: _ -> St_cost (cost_lbl, lbl)
     
    9595  | St_store (q, r, s, _), lbl :: _ -> St_store (q, r, s, lbl)
    9696  | St_call_ptr (r, args, ret, sg, _), lbl :: _ ->
    97                 St_call_ptr (r, args, ret, sg, lbl)
     97    St_call_ptr (r, args, ret, sg, lbl)
    9898  | St_call_id (i, args, ret, sg, _), lbl :: _ ->
    9999    St_call_id (i, args, ret, sg, lbl)
    100100  | St_cond (r, _, _), lbl1 :: lbl2 :: _ -> St_cond (r, lbl1, lbl2)
    101101  | St_jumptable (r, _), lbls -> St_jumptable (r, lbls)
    102         | _ -> invalid_arg "fill_labels: not enough successors to fill"
     102  | _ -> invalid_arg "fill_labels: not enough successors to fill"
    103103
    104104(** [insert_in_between u g src tgt s] inserts [s] between [src] and [tgt].
     
    109109let insert_in_between
    110110    (fresh : unit -> node)
    111                 (g : graph)
    112                 (src : node)
    113                 (tgt : node)
    114                 (s : statement)
    115                 : Label.t * graph =
    116                 let new_lbl = fresh () in
    117                 let src_stmt = Label.Map.find src g in
    118                 let succs = statement_successors src_stmt in
    119                 let repl lbl = if lbl = tgt then new_lbl else lbl in
    120                 let new_succs = List.map repl succs in
    121                 let new_src_stmt = fill_labels src_stmt new_succs in
    122                 (new_lbl, Label.Map.add new_lbl s (Label.Map.add src new_src_stmt g))
     111    (g : graph)
     112    (src : node)
     113    (tgt : node)
     114    (s : statement)
     115    : Label.t * graph =
     116  let new_lbl = fresh () in
     117  let src_stmt = Label.Map.find src g in
     118  let succs = statement_successors src_stmt in
     119  let repl lbl = if lbl = tgt then new_lbl else lbl in
     120  let new_succs = List.map repl succs in
     121  let new_src_stmt = fill_labels src_stmt new_succs in
     122  (new_lbl, Label.Map.add new_lbl s (Label.Map.add src new_src_stmt g))
    123123
    124124let dfs_fold
    125125    (f : node -> statement -> 'a -> 'a)
    126                 (g : graph)
    127                 (entry : node)
    128                 (init : 'a)
    129                 : 'a =
    130         assert (Label.Map.mem entry g);
    131         let rec process done_set = function
    132                 | [] -> init
    133                 | next :: worklist when Label.Set.mem next done_set ->
    134                         process done_set worklist
    135                 | next :: worklist ->
    136                         let stmt = Label.Map.find next g in
    137                         let succs = statement_successors stmt in
    138                         f next stmt (process (Label.Set.add next done_set) (succs @ worklist)) in
    139         process Label.Set.empty [entry]
    140        
     126    (g : graph)
     127    (entry : node)
     128    (init : 'a)
     129    : 'a =
     130  assert (Label.Map.mem entry g);
     131  let rec process done_set = function
     132    | [] -> init
     133    | next :: worklist when Label.Set.mem next done_set ->
     134      process done_set worklist
     135    | next :: worklist ->
     136      let stmt = Label.Map.find next g in
     137      let succs = statement_successors stmt in
     138      f next stmt (process (Label.Set.add next done_set) (succs @ worklist)) in
     139  process Label.Set.empty [entry]
     140   
    141141let dead_code_elim
    142142    (g     : graph)
    143143    (entry : node)
    144144    : graph =
    145                 let add lbl _ = Label.Set.add lbl in
    146                 let reachable = dfs_fold add g entry Label.Set.empty in
    147     let is_reachable x _ = Label.Set.mem x reachable in
    148     Label.Map.filter is_reachable g
     145  let add lbl _ = Label.Set.add lbl in
     146  let reachable = dfs_fold add g entry Label.Set.empty in
     147  let is_reachable x _ = Label.Set.mem x reachable in
     148  Label.Map.filter is_reachable g
    149149
    150150let dfs_iter
     
    153153    (entry : node)
    154154    : unit =
    155     assert (Label.Map.mem entry g);
    156     let rec process done_set = function
    157         | [] -> ();
    158         | next :: worklist when Label.Set.mem next done_set ->
    159             process done_set worklist
    160         | next :: worklist ->
    161             let stmt = Label.Map.find next g in
    162             let succs = statement_successors stmt in
    163             f next stmt;
    164                                                 process (Label.Set.add next done_set) (succs @ worklist) in
    165     process Label.Set.empty [entry]
    166    
     155  assert (Label.Map.mem entry g);
     156  let rec process done_set = function
     157    | [] -> ();
     158    | next :: worklist when Label.Set.mem next done_set ->
     159      process done_set worklist
     160    | next :: worklist ->
     161      let stmt = Label.Map.find next g in
     162      let succs = statement_successors stmt in
     163      f next stmt;
     164      process (Label.Set.add next done_set) (succs @ worklist) in
     165  process Label.Set.empty [entry]
     166
    167167let computes_type_map
    168168    (f_def : internal_function)
    169                 : AST.sig_type Register.Map.t =
    170         let types = Register.Map.empty in
    171         let add map (r, typ)  = Register.Map.add r typ map in
    172         let types = List.fold_left add types f_def.f_params in
    173         let types = List.fold_left add types f_def.f_locals in
    174         match f_def.f_result with
     169    : AST.sig_type Register.Map.t =
     170  let types = Register.Map.empty in
     171  let add map (r, typ)  = Register.Map.add r typ map in
     172  let types = List.fold_left add types f_def.f_params in
     173  let types = List.fold_left add types f_def.f_locals in
     174  match f_def.f_result with
    175175    | None -> types
    176176    | Some x -> add types x
     
    179179let modified_at_stmt stmt =
    180180  match stmt with
    181         | St_op1 (_, r, _, _)
    182         | St_op2 (_, r, _, _, _)
    183         | St_cst (r, _, _)
    184         | St_load (_, _, r, _)
    185         | St_call_id (_, _, Some r, _, _)
    186         | St_call_ptr (_, _, Some r, _, _) -> Some r
    187         | _ -> None
     181    | St_op1 (_, r, _, _)
     182    | St_op2 (_, r, _, _, _)
     183    | St_cst (r, _, _)
     184    | St_load (_, _, r, _)
     185    | St_call_id (_, _, Some r, _, _)
     186    | St_call_ptr (_, _, Some r, _, _) -> Some r
     187    | _ -> None
    188188
    189189let modified_at (g : graph) (n : Label.t) : Register.t option =
    190     modified_at_stmt (Label.Map.find n g)
     190  modified_at_stmt (Label.Map.find n g)
    191191
  • Deliverables/D2.2/8051/src/RTLabs/constPropagation.ml

    r1569 r1572  
    1717
    1818module L  = struct
    19        
    20         (* bottom will be when the map is undefined, so we do not need it explicitly*)
    21         type t =
    22                 | T
    23                 | V of Mem.Value.t
    24                 | S (* stack: could add offset *)
    25                 | A of AST.ident (* address symbol *)
     19
     20  (* bottom will be when the map is undefined, so we do not need it explicitly*)
     21  type t =
     22    | T
     23    | V of Mem.Value.t
     24    | S (* stack: could add offset *)
     25    | A of AST.ident (* address symbol *)
    2626
    2727  type property =
     
    2929
    3030  let bottom : property =
    31                 Register.FlexMap.empty
     31    Register.FlexMap.empty
    3232
    3333  let join_t x y = match x, y with
    34                 | V v1, V v2 when Mem.Value.equal v1 v2 -> V v1
    35                 | S, S -> S
    36                 | A i, A j when i = j -> A i
    37                 | _ -> T
     34    | V v1, V v2 when Mem.Value.equal v1 v2 -> V v1
     35    | S, S -> S
     36    | A i, A j when i = j -> A i
     37    | _ -> T
    3838
    3939  let join : property -> property -> property =
    40                 let choose i b1 b2 = match b1, b2 with
    41                         | Some v, Some v' -> Some (join_t v v')
    42                         | Some v, None | None, Some v -> Some v
    43                         | _ -> None in
    44                 Register.FlexMap.merge choose
    45 
    46         let bind = Register.FlexMap.add
    47        
    48         let find = Register.FlexMap.find
    49        
    50         let rem = Register.FlexMap.remove
    51                
    52         let mem = Register.FlexMap.mem
    53        
    54         let is_cst i p =
    55                 try
    56                         match find i p with
    57                                 | T -> false
    58                                 | _ -> true
    59                 with
    60                         | Not_found -> false
     40    let choose i b1 b2 = match b1, b2 with
     41      | Some v, Some v' -> Some (join_t v v')
     42      | Some v, None | None, Some v -> Some v
     43      | _ -> None in
     44    Register.FlexMap.merge choose
     45
     46  let bind = Register.FlexMap.add
     47
     48  let find = Register.FlexMap.find
     49
     50  let rem = Register.FlexMap.remove
     51
     52  let mem = Register.FlexMap.mem
     53
     54  let is_cst i p =
     55    try
     56      match find i p with
     57        | T -> false
     58        | _ -> true
     59    with
     60      | Not_found -> false
    6161
    6262  let find_cst i p =
    6363    match find i p with
    64             | T -> raise Not_found
    65             | v -> v
    66 
    67                
     64      | T -> raise Not_found
     65      | v -> v
    6866
    6967  let is_top i p =
    7068    try
    71         match find i p with
    72             | T -> true
    73                                                 | _ -> false
     69      match find i p with
     70        | T -> true
     71        | _ -> false
    7472    with
    75         | Not_found -> false
    76        
    77         let is_zero i p =
    78                 try
     73      | Not_found -> false
     74
     75  let is_zero i p =
     76    try
    7977      match find i p with
    80                                 | V v -> Mem.Value.is_false v
     78        | V v -> Mem.Value.is_false v
    8179        | _ -> false
    82       with
    83                                 | Not_found -> false
    84        
     80    with
     81      | Not_found -> false
     82
    8583  let equal : property -> property -> bool =
    86                 Register.FlexMap.equal (fun x y -> match x, y with
    87                         | T, T | S, S -> true
    88                         | V v1, V v2 -> Mem.Value.equal v1 v2
    89                         | A i, A j -> i = j
    90                         | _ -> false)
     84    Register.FlexMap.equal (fun x y -> match x, y with
     85      | T, T | S, S -> true
     86      | V v1, V v2 -> Mem.Value.equal v1 v2
     87      | A i, A j -> i = j
     88      | _ -> false)
    9189
    9290  let is_maximal _ = false
    93        
    94         let print = function
     91
     92  let print = function
    9593    | T -> "T"
    9694    | V v -> Mem.Value.to_string v
     
    103101
    104102module Eval = CminorInterpret.Eval_op (Mem)
    105   (* evaluation happens in RTLabs memory model ... *)
     103(* evaluation happens in RTLabs memory model ... *)
    106104
    107105module MemTarget = Memory.Make (Driver.TargetArch)
    108   (* ... but for sizeof and offsets, which rely on the target memory model *)
     106(* ... but for sizeof and offsets, which rely on the target memory model *)
    109107
    110108open AST
     
    123121  | Cst_offset off -> L.V (Mem.Value.of_int (MemTarget.concrete_offset off))
    124122  | Cst_sizeof t' ->
    125           L.V (cast_to_std t (Mem.Value.of_int (MemTarget.concrete_size t')))
    126         | Cst_stack -> L.S
    127         | Cst_addrsymbol i -> L.A i
    128         | _ -> assert false (* won't call in these cases *)
    129 
    130 let do_the_op1 type_of i j op x = match op, x with
    131         | _, L.V v -> L.V (Eval.op1 (type_of i) (type_of j) op v)
    132         | Op_id, _ -> x
     123    L.V (cast_to_std t (Mem.Value.of_int (MemTarget.concrete_size t')))
     124  | Cst_stack -> L.S
     125  | Cst_addrsymbol i -> L.A i
     126  | _ -> assert false (* won't call in these cases *)
     127
     128let arg_type type_of = function
     129  | Reg r -> type_of r
     130  | Imm (_, t) -> t
     131
     132let find_arg a prop = match a with
     133  | Reg r -> L.find r prop
     134  | Imm (k, t) -> cst t k
     135
     136let do_the_op1
     137    (op : op1)
     138    (type_of : Register.t -> sig_type)
     139    (prop : F.property)
     140    (i : Register.t)
     141    (j : Register.t)
     142    : L.t =
     143  let x = L.find j prop in
     144  match op, x with
     145  | _, L.V v -> L.V (Eval.op1 (type_of i) (type_of j) op v)
     146  | Op_id, _ -> x
    133147  | _ -> L.T
    134148
    135 let do_the_op2 type_of i j k op x y = match x, y, op with
    136         (* consider a constant division by 0 as not constant *)
    137         | L.V _, L.V v2, (Op_div | Op_divu | Op_mod | Op_modu)
    138           when Mem.Value.is_false v2 -> L.T
    139         | L.V v1, L.V v2, _ ->
    140                 L.V (Eval.op2 (type_of i) (type_of j) (type_of k) op v1 v2)
    141         (* ops with stack and address symbols are not considered constant, unless *)
    142         (* clearly so *)
    143         | x, L.V v, (Op_addp | Op_subp) when Mem.Value.is_false v -> x
    144         | _ -> L.T
     149let do_the_op2
     150    (op : op2)
     151    (type_of : Register.t -> sig_type)
     152    (prop : F.property)
     153    (i : Register.t)
     154    (a : argument)
     155    (b : argument)
     156    : L.t =
     157  let x = find_arg a prop in
     158  let y = find_arg b prop in
     159  match x, y, op with
     160  (* consider a constant division by 0 as not constant *)
     161  | L.V _, L.V v2, (Op_div | Op_divu | Op_mod | Op_modu)
     162    when Mem.Value.is_false v2 -> L.T
     163  | L.V v1, L.V v2, _ ->
     164    L.V (Eval.op2
     165           (type_of i)
     166           (arg_type type_of a)
     167           (arg_type type_of b) op v1 v2)
     168  (* ops with stack and address symbols are not considered constant, unless *)
     169  (* clearly so *)
     170  | x, L.V v, (Op_addp | Op_subp) when Mem.Value.is_false v -> x
     171  | _ -> L.T
     172
     173let is_zero_arg a prop = match a with
     174  | Reg r -> L.is_zero r prop
     175  | Imm (Cst_int i, _) -> i = 0
     176  | _ -> false
    145177
    146178(* this is used to mark some results of a bin op as constant even if its *)
    147179(* operands are not both constant *)
    148 let mark_const_op op i j k prop =
    149         match L.is_zero j prop, L.is_zero k prop, op with
    150                 | true, _, (Op_mul | Op_div | Op_divu | Op_mod | Op_modu | Op_and |
    151                             Op_shl | Op_shr | Op_shru | Op_cmpu Cmp_gt)
    152           | _, true, (Op_mul | Op_and | Op_cmpu Cmp_lt) ->
    153                   L.bind i (L.V Mem.Value.zero) prop
     180let mark_const_op op i a b prop =
     181  match is_zero_arg a prop, is_zero_arg b prop, op with
     182    | true, _, (Op_mul | Op_div | Op_divu | Op_mod | Op_modu | Op_and |
     183        Op_shl | Op_shr | Op_shru | Op_cmpu Cmp_gt)
     184    | _, true, (Op_mul | Op_and | Op_cmpu Cmp_lt) ->
     185      L.bind i (L.V Mem.Value.zero) prop
    154186    | true, _, Op_cmpu Cmp_le
    155                 | _, true, Op_cmpu Cmp_ge -> L.bind i (L.V (Mem.Value.of_bool true)) prop
    156                 | _, _, (Op_cmp Cmp_eq | Op_cmpu Cmp_eq | Op_cmpp Cmp_eq)
    157                   when Register.equal j k -> L.bind i (L.V (Mem.Value.of_bool true)) prop
     187    | _, true, Op_cmpu Cmp_ge -> L.bind i (L.V (Mem.Value.of_bool true)) prop
     188    | _, _, (Op_cmp Cmp_eq | Op_cmpu Cmp_eq | Op_cmpp Cmp_eq) ->
     189      (match a, b with
     190        | Reg j, Reg k when Register.equal j k ->
     191          L.bind i (L.V (Mem.Value.of_bool true)) prop
     192        | _ -> L.rem i prop)
    158193    | _, _, (Op_cmp Cmp_ne | Op_cmp Cmp_gt | Op_cmp Cmp_lt |
    159                          Op_cmpu Cmp_ne | Op_cmpu Cmp_gt | Op_cmpu Cmp_lt |
    160                                                  Op_cmpp Cmp_ne | Op_cmpp Cmp_gt | Op_cmpp Cmp_lt)
    161       when Register.equal j k -> L.bind i (L.V (Mem.Value.of_bool false)) prop
    162                 | _ -> L.rem i prop
     194             Op_cmpu Cmp_ne | Op_cmpu Cmp_gt | Op_cmpu Cmp_lt |
     195             Op_cmpp Cmp_ne | Op_cmpp Cmp_gt | Op_cmpp Cmp_lt |
     196             Op_xor) ->
     197      (match a, b with
     198        | Reg j, Reg k when Register.equal j k ->
     199          L.bind i (L.V (Mem.Value.of_bool false)) prop
     200        | _ -> L.rem i prop)
     201    | _ -> L.rem i prop
     202
     203let is_cst_arg prop = function
     204  | Reg r -> L.mem r prop
     205  | Imm _ -> true
    163206
    164207let semantics
    165208    (types : sig_type Register.Map.t)
    166209    (graph : statement Label.Map.t)
    167                 (pred_table : Label.Set.t Label.Map.t)
    168                 (lbl : Label.t)
    169                 (valu : F.valuation)
    170                 : F.property =
    171         let pred_prop = (* the situation at the entry of the statement (in [valu]) *)
    172                 let f pred prop =
    173                         L.join (valu pred) prop in
    174                 Label.Set.fold f (Label.Map.find lbl pred_table) L.bottom in
    175         let type_of r = Register.Map.find r types in
    176         match Label.Map.find lbl graph with
     210    (pred_table : Label.Set.t Label.Map.t)
     211    (lbl : Label.t)
     212    (valu : F.valuation)
     213    : F.property =
     214  let pred_prop = (* the situation at the entry of the statement (in [valu]) *)
     215    let f pred prop =
     216      L.join (valu pred) prop in
     217    Label.Set.fold f (Label.Map.find lbl pred_table) L.bottom in
     218  let type_of r = Register.Map.find r types in
     219  match Label.Map.find lbl graph with
    177220    | St_cst (_, Cst_float _, _) -> error_float ()
    178                 | St_cst (i, k, _) -> L.bind i (cst (type_of i) k) pred_prop
     221    | St_cst (i, k, _) -> L.bind i (cst (type_of i) k) pred_prop
    179222    | St_op1 (op, i, j, _) ->
    180223      (try
    181                                 L.bind i (do_the_op1 type_of i j op (L.find j pred_prop)) pred_prop
    182                         with
    183                                 | Not_found -> L.rem i pred_prop)
    184 
    185     | St_op2 (op,i,Reg j,Reg k,_) when L.mem j pred_prop && L.mem k pred_prop ->
    186                         let j_val = L.find j pred_prop in
    187                         let k_val = L.find k pred_prop in
    188       L.bind i (do_the_op2 type_of i j k op j_val k_val) pred_prop
    189                 | St_op2 (op, i, Reg j, Reg k, _) ->
    190                         mark_const_op op i j k pred_prop
    191                 | St_load (_, _, i, _)
    192                 | St_call_id (_, _, Some i, _, _)
    193                 | St_call_ptr (_, _, Some i, _, _) -> L.rem i pred_prop
     224         L.bind i (do_the_op1 op type_of pred_prop i j) pred_prop
     225       with
     226         | Not_found -> L.rem i pred_prop)
     227    | St_op2 (op, i, a, b, _)
     228      when is_cst_arg pred_prop a && is_cst_arg pred_prop b ->
     229      L.bind i (do_the_op2 op type_of pred_prop i a b) pred_prop
     230    | St_op2 (op, i, a, b, _) ->
     231      mark_const_op op i a b pred_prop
     232    | St_load (_, _, i, _)
     233    | St_call_id (_, _, Some i, _, _)
     234    | St_call_ptr (_, _, Some i, _, _) -> L.rem i pred_prop
    194235    | _ -> pred_prop
    195236
    196237let analyze
    197238    (f_def : internal_function)
    198                 : F.valuation =
    199         (* extract types of registers from the definition *)
     239    : F.valuation =
     240  (* extract types of registers from the definition *)
    200241  let types = RTLabsUtilities.computes_type_map f_def in
    201                
    202         let graph = f_def.f_graph in
    203        
    204         let pred_table = RTLabsUtilities.compute_predecessors graph in
    205        
    206         F.lfp (semantics types graph pred_table)
    207                
     242
     243  let graph = f_def.f_graph in
     244
     245  let pred_table = RTLabsUtilities.compute_predecessors graph in
     246
     247  F.lfp (semantics types graph pred_table)
     248
    208249(* now that the info for constants can be gathered, let's put that to use *)
    209250
    210251(* this will be used to turn values back into constants. Notice: *)
    211 (* 1) if we have mapped a register to a value, it must be an integer *)
    212 (* 2) we are turning abstract offsets and sizes into integers *)
    213 (* 3) this shares the problem with AST constants of representability *)
     252(* 1) we are turning abstract offsets and sizes into integers *)
     253(* 2) this shares the problem with AST constants of representability *)
    214254(*    with ocaml 31 bits integers *)
    215255let cst_of_value = function
    216         | L.V v -> Cst_int (Mem.Value.to_int v)
    217         | L.S -> Cst_stack
    218         | L.A i -> Cst_addrsymbol i
    219         | _ -> invalid_arg "cst_of_value"
     256  | L.V v -> Cst_int (Mem.Value.to_int v)
     257  | L.S -> Cst_stack
     258  | L.A a -> Cst_addrsymbol a
     259  | _ -> invalid_arg "cst_of_value"
     260
     261let arg_from_reg prop types r =
     262  try
     263    Imm (cst_of_value (L.find_cst r prop), Register.Map.find r types)
     264  with
     265    | Not_found -> Reg r
     266
     267let arg_from_arg prop types = function
     268  | Reg i -> arg_from_reg prop types i
     269  | _ as a -> a
     270
     271let copy i a l = match a with
     272  | Reg j -> St_op1 (Op_id, i, j, l)
     273  | _ -> assert false (* should already have been substituted *)
     274
     275let negate i a l = match a with
     276  | Reg j -> St_op1 (Op_negint, i, j, l)
     277  | _ -> assert false (* should already have been substituted *)
    220278
    221279let simpl_imm_op2 op i j k types prop l =
    222         let f r =
    223                 try
    224                         Some (L.find_cst r prop)
    225                 with
    226                         | Not_found -> None in
    227         let one = Mem.Value.of_int 1 in
    228         let type_of r = Register.Map.find r types in
    229         match f j, f k, op with
    230   | Some (L.V v), _, (Op_add | Op_or | Op_xor ) when Mem.Value.is_false v ->
    231     St_op1(Op_id, i, k, l)
    232   | Some (L.V v), _, Op_mul when Mem.Value.equal v one ->
    233     St_op1(Op_id, i, k, l)
    234   | _, Some (L.V v), (Op_add | Op_sub | Op_addp | Op_subp | Op_or | Op_xor)
    235           when Mem.Value.is_false v ->
    236     St_op1(Op_id, i, j, l)
    237   | _, Some (L.V v), Op_mul when Mem.Value.equal v one ->
    238     St_op1(Op_id, i, j, l)
    239   | Some (L.V v), _, Op_sub when Mem.Value.is_false v ->
    240                 St_op1(Op_negint, i, k, l)
    241   | Some v, Some u, _ ->
    242                 let a1 = Imm (cst_of_value v, type_of j) in
    243                 let a2 = Imm (cst_of_value u, type_of k) in
    244                 St_op2(op, i, a1, a2, l)
    245   | Some v, _, _ -> St_op2(op, i, Imm (cst_of_value v, type_of j), Reg k, l)
    246   | _, Some v, _ -> St_op2(op, i, Reg j, Imm (cst_of_value v, type_of k), l)
    247         | _ -> St_op2(op, i, Reg j, Reg k, l)
    248 
    249 let simpl_imm_load q i j types prop l =
    250         try
    251                 let v = L.find_cst i prop in
    252                 St_load(q, Imm (cst_of_value v, Register.Map.find i types), j, l)
    253         with
    254                 | Not_found -> St_load (q, Reg i, j, l)
    255 
    256 let simpl_imm_store q i j types prop l =
    257         let f r =
    258                 try
    259                     Some (L.find_cst r prop)
    260                 with
    261                     | Not_found -> None in
    262         let type_of r = Register.Map.find r types in
    263         match f i, f j with
    264                 | Some v, Some u ->
    265             let a1 = Imm (cst_of_value v, type_of i) in
    266             let a2 = Imm (cst_of_value u, type_of j) in
    267             St_store(q, a1, a2, l)
    268                 | Some v, _ ->
    269                         St_store(q, Imm (cst_of_value v, type_of i), Reg j, l)
    270     | _, Some u ->
    271       St_store(q, Reg i, Imm (cst_of_value u, type_of j), l)
    272                 | _ -> St_store(q, Reg i, Reg j, l)
     280  let f = function
     281    | Imm _ -> None
     282    | Reg r ->
     283      try
     284        Some (L.find_cst r prop)
     285      with
     286        | Not_found -> None in
     287  let one = Mem.Value.of_int 1 in
     288  match f j, f k, op with
     289    | Some (L.V v), _, (Op_add | Op_addp | Op_or | Op_xor )
     290      when Mem.Value.is_false v ->
     291      copy i k l
     292    | Some (L.V v), _, Op_mul when Mem.Value.equal v one ->
     293      copy i j l
     294    | _, Some (L.V v), (Op_add | Op_sub | Op_addp | Op_subp | Op_or | Op_xor)
     295      when Mem.Value.is_false v ->
     296      copy i j l
     297    | _, Some (L.V v), (Op_mul | Op_div)  when Mem.Value.equal v one ->
     298      copy i j l
     299    | Some (L.V v), _, Op_sub when Mem.Value.is_false v ->
     300      negate i j l
     301    | _ ->
     302      St_op2(op, i, arg_from_arg prop types j, arg_from_arg prop types k, l)
    273303
    274304(* we transform statements according to the valuation found out by analyze *)
     
    276306let transform_statement
    277307    (valu : F.valuation)
    278                 (types: sig_type Register.Map.t)
     308    (types: sig_type Register.Map.t)
    279309    (p    : Label.t)
    280                 : statement -> statement = function
    281   | St_cst (i, (Cst_offset _ | Cst_sizeof _), next) ->
    282                 (* we are sure valu has a binding for i, we change the abstract quantities*)
    283                 (* into actual integers *)
    284                 St_cst (i, cst_of_value (L.find_cst i (valu p)), next)
    285         | (St_op1 (_,i,_,next) | St_op2(_,i,_,_,next)) when L.is_cst i (valu p) ->
    286                 St_cst (i, cst_of_value (L.find_cst i (valu p)), next)
    287         | St_op2 (op, i, Reg j, Reg k, l) ->
    288                 simpl_imm_op2 op i j k types (valu p) l
    289   | St_load (q, Reg i, j, l) ->
    290                 simpl_imm_load q i j types (valu p) l
    291         | St_store (q, Reg i, Reg j, l) ->
    292                 simpl_imm_store q i j types (valu p) l
    293   | St_op2 _ | St_load _ | St_store _ ->
    294           assert false (* there should not be any imm argument *)
    295         | St_cond (i, if_true, if_false) as s when L.is_cst i (valu p) ->
    296                 let s = match L.find_cst i (valu p) with
    297                         | L.V v when Mem.Value.is_false v -> St_skip if_false
    298                         | L.V _ | L.A _ -> St_skip if_true
    299                         | _ -> s in s
    300         | stmt -> stmt
    301 
    302 let dom (map : 'a Label.Map.t) : Label.Set.t =
    303         let add key _ = Label.Set.add key in
    304         Label.Map.fold add map Label.Set.empty
     310    : statement -> statement = function
     311      | St_cst (i, (Cst_offset _ | Cst_sizeof _), next) ->
     312        (* we are sure valu has a binding for i, we change the abstract
     313           quantities into actual integers *)
     314        St_cst (i, cst_of_value (L.find_cst i (valu p)), next)
     315      | (St_op1 (_,i,_,next) | St_op2(_,i,_,_,next)) when L.is_cst i (valu p) ->
     316        St_cst (i, cst_of_value (L.find_cst i (valu p)), next)
     317      | St_op2 (op, i, a, b, l) ->
     318        simpl_imm_op2 op i a b types (valu p) l
     319      | St_load (q, a, j, l) ->
     320        St_load(q, arg_from_arg (valu p) types a, j, l)
     321      | St_store (q, a, b, l) ->
     322        St_store (q, arg_from_arg (valu p) types a,
     323                     arg_from_arg (valu p) types b, l)
     324      | St_cond (i, if_true, if_false) as s when L.is_cst i (valu p) ->
     325        let s = match L.find_cst i (valu p) with
     326          | L.V v when Mem.Value.is_false v -> St_skip if_false
     327          | L.V _ | L.A _ -> St_skip if_true
     328          | _ -> s in s
     329      | St_return (Some a) ->
     330        St_return (Some (arg_from_arg (valu p) types a))
     331      | St_call_id (f, args, ret, sg, l) ->
     332        St_call_id (f, List.map (arg_from_arg (valu p) types) args, ret, sg, l)
     333      | St_call_ptr (f, args, ret, sg, l) ->
     334        St_call_ptr (f, List.map (arg_from_arg (valu p) types) args, ret, sg, l)
     335      | St_tailcall_id (f, args, sg) ->
     336        St_tailcall_id (f, List.map (arg_from_arg (valu p) types) args, sg)
     337      | St_tailcall_ptr (f, args, sg) ->
     338        St_tailcall_ptr (f, List.map (arg_from_arg (valu p) types) args, sg)
     339      | stmt -> stmt
    305340
    306341let transform_int_function
    307342    (f_def  : internal_function)
    308                 : internal_function =
    309         let valu = analyze f_def in
    310         (* we transform the graph according to the analysis *)
    311         let types = RTLabsUtilities.computes_type_map f_def in
    312         let graph = Label.Map.mapi (transform_statement valu types) f_def.f_graph in
    313         (* and we eliminate resulting dead code *)
    314         let graph = RTLabsUtilities.dead_code_elim graph f_def.f_entry in
    315         {f_def with f_graph = graph}
     343    : internal_function =
     344  let valu = analyze f_def in
     345        (* we transform the graph according to the analysis *)
     346  let types = RTLabsUtilities.computes_type_map f_def in
     347  let graph = Label.Map.mapi (transform_statement valu types) f_def.f_graph in
     348        (* and we eliminate resulting dead code *)
     349  let graph = RTLabsUtilities.dead_code_elim graph f_def.f_entry in
     350  {f_def with f_graph = graph}
    316351
    317352let transform_function = function
    318         | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
    319         | f -> f
     353  | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
     354  | f -> f
    320355
    321356let trans = Languages.RTLabs, function
    322         | Languages.AstRTLabs p ->
    323                 Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
    324         | _ -> assert false
    325 
    326          
     357  | Languages.AstRTLabs p ->
     358    Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
     359  | _ -> assert false
     360
     361
  • Deliverables/D2.2/8051/src/RTLabs/copyPropagation.ml

    r1569 r1572  
    1818
    1919module L  = struct
    20        
     20
    2121  type property =
    2222      Register.t Register.FlexMap.t
    2323
    2424  let bottom : property =
    25                 Register.FlexMap.empty
    26                
    27         let meet =
    28                 let choose r ro1 ro2 = match ro1, ro2 with
    29                         | Some r1, Some r2 when r1 = r2 -> Some r1
    30                         | _ -> None in
    31                 Register.FlexMap.merge choose
     25    Register.FlexMap.empty
     26
     27  let meet =
     28    let choose r ro1 ro2 = match ro1, ro2 with
     29      | Some r1, Some r2 when r1 = r2 -> Some r1
     30      | _ -> None in
     31    Register.FlexMap.merge choose
    3232
    3333  let big_meet f = function
    34                 | [] -> bottom
    35                 | x :: xs ->
    36                         let f' s y = meet s (f y) in
    37                         List.fold_left f' (f x) xs
    38        
     34    | [] -> bottom
     35    | x :: xs ->
     36      let f' s y = meet s (f y) in
     37      List.fold_left f' (f x) xs
     38
    3939  let equal : property -> property -> bool =
    40                 Register.FlexMap.equal Register.equal
     40    Register.FlexMap.equal Register.equal
    4141
    4242  let is_maximal _ = false
    43        
     43
    4444end
    4545
    4646let ( --* ) m = function
    47         | None -> m
    48         | Some r ->
    49                 let filter s t = not (Register.equal s r || Register.equal t r) in
    50                 Register.FlexMap.filter filter m
     47  | None -> m
     48  | Some r ->
     49    let filter s t = not (Register.equal s r || Register.equal t r) in
     50    Register.FlexMap.filter filter m
    5151
    5252module F = Fix.Make (Label.ImpMap) (L)
     
    5454let semantics
    5555    (graph : statement Label.Map.t)
    56                 (pred_table : Label.t list Label.Map.t)
    57                 (lbl : Label.t)
    58                 (valu : F.valuation)
    59                 : F.property =
     56    (pred_table : Label.t list Label.Map.t)
     57    (lbl : Label.t)
     58    (valu : F.valuation)
     59    : F.property =
    6060  let copies_out l =
    61                 let copies_out = valu l in
    62                 match Label.Map.find l graph with
    63                         | St_op1 (Op_id, r, s, _) ->
    64                                 let copy_of x =
    65                                         (try
    66                                                 Register.FlexMap.find x copies_out
    67                                         with
    68                                                 | Not_found -> x) in
    69                                 if Register.equal (copy_of r) (copy_of s) then copies_out else
    70                                 Register.FlexMap.add r s (copies_out --* (Some r))
    71                         | stmt -> copies_out --* RTLabsUtilities.modified_at_stmt stmt in
    72         L.big_meet copies_out (Label.Map.find lbl pred_table)
     61    let copies_out = valu l in
     62    match Label.Map.find l graph with
     63      | St_op1 (Op_id, r, s, _) ->
     64        let copy_of x =
     65          (try
     66             Register.FlexMap.find x copies_out
     67           with
     68             | Not_found -> x) in
     69        if Register.equal (copy_of r) (copy_of s) then copies_out else
     70          Register.FlexMap.add r s (copies_out --* (Some r))
     71      | stmt -> copies_out --* RTLabsUtilities.modified_at_stmt stmt in
     72  L.big_meet copies_out (Label.Map.find lbl pred_table)
    7373
    7474let analyze
    7575    (f_def : internal_function)
    76                 : F.valuation =
    77                
    78         let graph = f_def.f_graph in
    79        
    80         let pred_table = RTLabsUtilities.compute_predecessor_lists graph in
    81        
    82         F.lfp (semantics graph pred_table)
     76    : F.valuation =
     77
     78  let graph = f_def.f_graph in
     79
     80  let pred_table = RTLabsUtilities.compute_predecessor_lists graph in
     81
     82  F.lfp (semantics graph pred_table)
    8383
    8484(* we transform statements according to the valuation found out by analyze *)
     
    8686    (valu : F.valuation)
    8787    (p    : Label.t)
    88                 : statement -> statement =
    89         let copy_of x =
    90                 try
    91                         Register.FlexMap.find x (valu p)
    92                 with
    93                         | Not_found -> x in
    94         let copy_of_arg = function
    95                 | Reg x -> Reg (copy_of x)
    96                 | Imm _ as a -> a in
    97         function
    98                 | St_op1 (o,i,j,next) -> St_op1(o,i,copy_of j,next)
    99                 | St_op2 (o,i,j,k,next) -> St_op2(o,i,copy_of_arg j, copy_of_arg k,next)
    100           | St_load (q, a, j, l) -> St_load (q, copy_of_arg a, j, l)
    101                 | St_store (q, a1, a2, l) -> St_store(q, copy_of_arg a1, copy_of_arg a2, l)
    102                 | St_cond (i, if_true, if_false) -> St_cond (copy_of i, if_true, if_false)
    103                 | St_call_id (f, args, ret, sign, l) ->
    104                         St_call_id (f, List.map copy_of args, ret, sign, l)
    105                 | St_call_ptr (f, args, ret, sign, l) ->
    106             St_call_ptr (f, List.map copy_of args, ret, sign, l)
    107                 | stmt -> stmt
     88    : statement -> statement =
     89  let copy_of x =
     90    try
     91      Register.FlexMap.find x (valu p)
     92    with
     93      | Not_found -> x in
     94  let copy_of_arg = function
     95    | Reg x -> Reg (copy_of x)
     96    | Imm _ as a -> a in
     97  function
     98    | St_op1 (o,i,j,next) -> St_op1(o,i,copy_of j,next)
     99    | St_op2 (o,i,j,k,next) -> St_op2(o,i,copy_of_arg j, copy_of_arg k,next)
     100    | St_load (q, a, j, l) -> St_load (q, copy_of_arg a, j, l)
     101    | St_store (q, a1, a2, l) -> St_store(q, copy_of_arg a1, copy_of_arg a2, l)
     102    | St_cond (i, if_true, if_false) -> St_cond (copy_of i, if_true, if_false)
     103    | St_call_id (f, args, ret, sign, l) ->
     104      St_call_id (f, List.map copy_of_arg args, ret, sign, l)
     105    | St_call_ptr (f, args, ret, sign, l) ->
     106      St_call_ptr (f, List.map copy_of_arg args, ret, sign, l)
     107    | St_return (Some a) -> St_return (Some (copy_of_arg a))
     108    | stmt -> stmt
    108109
    109110let transform_int_function
    110111    (f_def  : internal_function)
    111                 : internal_function =
    112         let valu = analyze f_def in
    113         (* we transform the graph according to the analysis *)
    114         let graph = Label.Map.mapi (transform_statement valu) f_def.f_graph in
    115         {f_def with f_graph = graph}
     112    : internal_function =
     113  let valu = analyze f_def in
     114        (* we transform the graph according to the analysis *)
     115  let graph = Label.Map.mapi (transform_statement valu) f_def.f_graph in
     116  {f_def with f_graph = graph}
    116117
    117118let transform_function = function
    118         | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
    119         | f -> f
     119  | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
     120  | f -> f
    120121
    121122let trans = Languages.RTLabs, function
    122         | Languages.AstRTLabs p ->
    123                 Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
    124         | _ -> assert false
    125 
    126          
     123  | Languages.AstRTLabs p ->
     124    Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
     125  | _ -> assert false
  • Deliverables/D2.2/8051/src/RTLabs/redundancyElimination.ml

    r1569 r1572  
    33    This is a reformulation of material found in Muchnick, Advanced compiler
    44    design and implementation.
    5                 Along the way we also perform a first rough liveness analysis. *)
    6                
     5    Along the way we also perform a first rough liveness analysis. *)
     6
    77
    88open RTLabs
     
    2424(* an example where this transformation really applies. *)
    2525
    26 let count_predecessors 
     26let count_predecessors
    2727    (g : graph)
    2828    : int Label.Map.t =
    2929  let f lbl s m =
    3030    let succs = RTLabsUtilities.statement_successors s in
    31       let f' m succ =
     31    let f' m succ =
    3232      try
    3333        Label.Map.add succ (1 + Label.Map.find succ m) m
    3434      with
    3535        | Not_found -> Label.Map.add succ 1 m in
    36       let m = List.fold_left f' m succs in
    37       if Label.Map.mem lbl m then m else Label.Map.add lbl 0 m in
     36    let m = List.fold_left f' m succs in
     37    if Label.Map.mem lbl m then m else Label.Map.add lbl 0 m in
    3838  Label.Map.fold f g Label.Map.empty
    3939
     
    4747  let add_if_2_preds l1 s l2 =
    4848    if Label.Map.find l2 pred_count < 2 then s else
    49     LabelPairSet.add (l1, l2) s in
     49      LabelPairSet.add (l1, l2) s in
    5050  let f l stmt s = match stmt with
    5151    | St_cond(_, l1, l2) ->
    52       add_if_2_preds l (add_if_2_preds l s l1) l2 
     52      add_if_2_preds l (add_if_2_preds l s l1) l2
    5353    | St_jumptable (_, ls) when List.length ls > 1 ->
    5454      List.fold_left (add_if_2_preds l) s ls
    5555    | _ -> s in
    5656  Label.Map.fold f g LabelPairSet.empty
    57      
     57
    5858(* note to self: there is a degenrate case that is not eliminated by the *)
    5959(* following, namely (top to bottom) *)
     
    7676    (f_def : internal_function)
    7777    : internal_function =
    78         let g = f_def.f_graph in
    79         let fresh () = Label.Gen.fresh f_def.f_luniverse in
     78  let g = f_def.f_graph in
     79  let fresh () = Label.Gen.fresh f_def.f_luniverse in
    8080  let critical_edges = find_critical_edges g in
    8181  let rem (src, tgt) g =
    8282    snd (RTLabsUtilities.insert_in_between fresh g src tgt (St_skip tgt)) in
    8383  { f_def with f_graph = LabelPairSet.fold rem critical_edges g }
    84          
     84
    8585(* Expressions, expression sets, and operations thereof *)
    8686
    8787(* Load and store ops are not taken into account, maybe later *)
    8888type expr =
    89 (*      | Cst of cst (* do we need to consider constants? maybe only big ones? *)*)
     89  (*        | Cst of cst (* do we need to consider constants? maybe only big ones? *)*)
    9090  | UnOp of op1 * Register.t
    9191  | BinOp of op2 * argument * argument
    9292
    9393let expr_of_stmt (s : statement) : expr option = match s with
    94 (*      | St_cst (_, c, _) -> Some (Cst c)*)
    95         | St_op1 (op, _, s, _) when op <> Op_id -> Some (UnOp (op, s))
    96         | St_op2 (op, _, s, t, _) -> Some (BinOp (op, s, t))
    97         | _ -> None
     94        (*        | St_cst (_, c, _) -> Some (Cst c)*)
     95  | St_op1 (op, _, s, _) when op <> Op_id -> Some (UnOp (op, s))
     96  | St_op2 (op, _, s, t, _) -> Some (BinOp (op, s, t))
     97  | _ -> None
    9898
    9999let expr_of (g : graph) (n : Label.t) : expr option =
    100         expr_of_stmt (Label.Map.find n g)
     100  expr_of_stmt (Label.Map.find n g)
    101101
    102102(* the register modified by a node *)
     
    111111let vars_of_stmt = function
    112112  | St_op2 (_, _, Reg s, Reg t, _) ->
    113                 Register.Set.add s (Register.Set.singleton t)
     113    Register.Set.add s (Register.Set.singleton t)
    114114  | St_load (_, Reg s, _, _)
    115115  | St_op1 (_, _, s, _)
    116         | St_op2 (_, _, Reg s, _, _)
    117         | St_op2 (_, _, _, Reg s, _) -> Register.Set.singleton s
    118         | _ -> Register.Set.empty
     116  | St_op2 (_, _, Reg s, _, _)
     117  | St_op2 (_, _, _, Reg s, _) -> Register.Set.singleton s
     118  | _ -> Register.Set.empty
    119119
    120120let vars_of (g : graph) (n : Label.t) : Register.Set.t =
    121         vars_of_stmt (Label.Map.find n g)
    122        
     121  vars_of_stmt (Label.Map.find n g)
     122
    123123(* used in possibly non side-effect-free statements *)
    124 let used_at_stmt = function
    125         | St_call_id (_, rs, _, _, _)
    126         | St_call_ptr (_, rs, _, _, _)
    127         | St_tailcall_id (_, rs, _)
    128         | St_tailcall_ptr (_, rs, _) ->
    129             let f s r = Register.Set.add r s in
    130             List.fold_left f Register.Set.empty rs
    131   | St_store (_, Reg s, Reg t, _) ->
    132                 Register.Set.add s (Register.Set.singleton t)
    133         | St_return (Some r)
    134         | St_cond (r, _, _)
    135         | St_store (_, Reg r, _, _)
    136         | St_store (_, _, Reg r, _)  -> Register.Set.singleton r
    137         | _ -> Register.Set.empty
     124let used_at_stmt stmt =
     125  let add_arg s = function
     126    | Reg r -> Register.Set.add r s
     127    | Imm _ -> s in
     128  match stmt with
     129    | St_call_id (_, rs, _, _, _)
     130    | St_call_ptr (_, rs, _, _, _)
     131    | St_tailcall_id (_, rs, _)
     132    | St_tailcall_ptr (_, rs, _) ->
     133      List.fold_left add_arg Register.Set.empty rs
     134    | St_store (_, a, b, _) ->
     135      add_arg (add_arg Register.Set.empty a) b
     136    | St_return (Some (Reg r))
     137    | St_cond (r, _, _) -> Register.Set.singleton r
     138    | _ -> Register.Set.empty
    138139
    139140let used_at g n = used_at_stmt (Label.Map.find n g)
    140141
    141142module ExprOrdered = struct
    142         type t = expr
    143         let compare = compare
     143  type t = expr
     144  let compare = compare
    144145end
    145146
     
    164165
    165166let big_inter (f : Label.t -> ExprSet.t) (ls : Label.t list) : ExprSet.t =
    166         (* generalized intersection, but in case of empty list it is empty *)
    167         match ls with
    168                 | [] -> ExprSet.empty
     167        (* generalized intersection, but in case of empty list it is empty *)
     168  match ls with
     169    | [] -> ExprSet.empty
    169170    (* these two cases are singled out for speed, as they will be common *)
    170171    | [l] -> f l
     
    176177let big_union (f : Label.t -> Register.Set.t) (ls : Label.t list)
    177178    : Register.Set.t =
    178     (* generalized union *)
     179  (* generalized union *)
    179180  let union s l' = Register.Set.union s (f l') in
    180     List.fold_left union Register.Set.empty ls
     181  List.fold_left union Register.Set.empty ls
    181182
    182183let filter_unchanged (r : Register.t option) (s : expr_set) : expr_set =
    183         match r with
    184                 | None -> s
    185                 | Some r ->
    186                         let filter = function
    187                                 | UnOp (_, s) when r = s -> false
    188                                 | BinOp (_, s, t) when s = Reg r || t = Reg r -> false
    189                                 | _ -> true in
    190                         ExprSet.filter filter s
    191                        
     184  match r with
     185    | None -> s
     186    | Some r ->
     187      let filter = function
     188        | UnOp (_, s) when r = s -> false
     189        | BinOp (_, s, t) when s = Reg r || t = Reg r -> false
     190        | _ -> true in
     191      ExprSet.filter filter s
     192
    192193module Lpair = struct
    193        
    194         (* A property is a pair of sets of expressions. *)
    195         type property = expr_set * expr_set
    196        
    197         let bottom = (ExprSet.empty, ExprSet.empty)
    198        
     194
     195        (* A property is a pair of sets of expressions. *)
     196  type property = expr_set * expr_set
     197
     198  let bottom = (ExprSet.empty, ExprSet.empty)
     199
    199200  let equal (ant1, nea1) (ant2, nea2) =
    200                 ExprSet.equal ant1 ant2 && ExprSet.equal nea1 nea2
     201    ExprSet.equal ant1 ant2 && ExprSet.equal nea1 nea2
    201202
    202203  let is_maximal _ = false
    203        
     204
    204205end
    205206
    206207module Lsing = struct
    207    
     208
    208209  (* A property is a set of expressions. *)
    209210  type property = expr_set
    210    
     211
    211212  let bottom = ExprSet.empty
    212    
     213
    213214  let equal = ExprSet.equal
    214215
    215216  let is_maximal _ = false
    216    
     217
    217218end
    218219
    219220module Lexprid = struct
    220    
     221
    221222  (* A property is a set of expressions and a set of registers. *)
    222223  type property = expr_set * Register.Set.t
    223    
     224
    224225  let bottom = (ExprSet.empty, Register.Set.empty)
    225    
     226
    226227  let equal (a, b) (c, d) = ExprSet.equal a c && Register.Set.equal b d
    227228
    228229  let is_maximal _ = false
    229    
     230
    230231end
    231232
     
    239240
    240241let print_expr = function
    241 (*    | Cst c ->
    242       (RTLabsPrinter.print_cst c)*)
    243     | UnOp (op, r) ->
    244       (RTLabsPrinter.print_op1 op r)
    245     | BinOp (op, r, s) ->
    246       (RTLabsPrinter.print_op2 op r s)
    247                        
     242    (*    | Cst c ->
     243          (RTLabsPrinter.print_cst c)*)
     244  | UnOp (op, r) ->
     245    (RTLabsPrinter.print_op1 op r)
     246  | BinOp (op, r, s) ->
     247    (RTLabsPrinter.print_op2 op r s)
     248
    248249let print_prop_pair (p : Fpair.property) = let (ant, nea) = p in
    249   let f e = Printf.printf "%s, " (print_expr e) in
    250         Printf.printf "{ ";
    251         ExprSet.iter f ant;
    252   Printf.printf "}; { ";
    253   ExprSet.iter f nea;
    254   Printf.printf "}\n"
     250                                           let f e = Printf.printf "%s, " (print_expr e) in
     251                                           Printf.printf "{ ";
     252                                           ExprSet.iter f ant;
     253                                           Printf.printf "}; { ";
     254                                           ExprSet.iter f nea;
     255                                           Printf.printf "}\n"
    255256
    256257let print_valu_pair (valu : Fpair.valuation) (g : graph) (entry : Label.t) =
    257     let f lbl _ =
    258         Printf.printf "%s: " lbl;
    259         print_prop_pair (valu lbl) in
    260      RTLabsUtilities.dfs_iter f g entry
    261 
    262 let print_prop_sing (p : Fsing.property) = 
     258  let f lbl _ =
     259    Printf.printf "%s: " lbl;
     260    print_prop_pair (valu lbl) in
     261  RTLabsUtilities.dfs_iter f g entry
     262
     263let print_prop_sing (p : Fsing.property) =
    263264  let f e = Printf.printf "%s, " (print_expr e) in
    264265  Printf.printf "{ ";
     
    267268
    268269let print_valu_sing (valu : Fsing.valuation) (g : graph) (entry : Label.t) =
    269     let f lbl _ =
    270         Printf.printf "%s: " lbl;
    271         print_prop_sing (valu lbl) in
    272      RTLabsUtilities.dfs_iter f g entry
    273    
    274    
     270  let f lbl _ =
     271    Printf.printf "%s: " lbl;
     272    print_prop_sing (valu lbl) in
     273  RTLabsUtilities.dfs_iter f g entry
     274
     275
    275276(* ----- PHASE 1 : Anticipatability and erliestness ------ *)
    276277(* An expression e is anticipatable at point p if every path from p contains  *)
     
    280281(* preceding p giving the same value. *)
    281282(* We will compute anticipatable expressions and *non*-earliest ones for every*)
    282 (* point with a single invocation to a fixpoint calculation. *) 
     283(* point with a single invocation to a fixpoint calculation. *)
    283284
    284285
    285286let semantics_ant_nea
    286287    (g : graph)
    287                 (pred_table : Label.t list Label.Map.t)
     288    (pred_table : Label.t list Label.Map.t)
    288289    (lbl : Label.t)
    289290    (valu : Fpair.valuation)
    290291    : Fpair.property =
    291         let succs = RTLabsUtilities.statement_successors (Label.Map.find lbl g) in
    292         let preds = Label.Map.find lbl pred_table in
    293        
    294   (* anticipatable expressions at entry *)
    295         (* take anticipatable expressions of successors... *)
    296         let ant l = fst (valu l) in
    297         let nea l = snd (valu l) in
    298         let ant_in = big_inter ant succs in
    299         (* ... filter out those that contain the register being changed ...*)
    300         let ant_in = filter_unchanged (modified_at g lbl) ant_in in
    301         (* ... and add the expression being calculated ... *)
    302         let ant_in = ant_in ++* expr_of g lbl in
    303        
    304         (* non-earliest expressions at entry *)
    305         (* take non-earliest or anticipatable expressions of predecessors, *)
    306         (* filtered so that just unchanged expressions leak *)
    307         let ant_or_nea l =
    308                 filter_unchanged (modified_at g l) (ant l ++ nea l) in
    309         let nea_in = big_inter ant_or_nea preds in
    310                        
    311         (ant_in, nea_in)
    312        
     292  let succs = RTLabsUtilities.statement_successors (Label.Map.find lbl g) in
     293  let preds = Label.Map.find lbl pred_table in
     294
     295        (* anticipatable expressions at entry *)
     296        (* take anticipatable expressions of successors... *)
     297  let ant l = fst (valu l) in
     298  let nea l = snd (valu l) in
     299  let ant_in = big_inter ant succs in
     300        (* ... filter out those that contain the register being changed ...*)
     301  let ant_in = filter_unchanged (modified_at g lbl) ant_in in
     302        (* ... and add the expression being calculated ... *)
     303  let ant_in = ant_in ++* expr_of g lbl in
     304
     305        (* non-earliest expressions at entry *)
     306        (* take non-earliest or anticipatable expressions of predecessors, *)
     307        (* filtered so that just unchanged expressions leak *)
     308  let ant_or_nea l =
     309    filter_unchanged (modified_at g l) (ant l ++ nea l) in
     310  let nea_in = big_inter ant_or_nea preds in
     311
     312  (ant_in, nea_in)
     313
    313314let compute_anticipatable_and_non_earliest
    314315    (f_def : internal_function)
    315316    (pred_table : Label.t list Label.Map.t)
    316317    : Fpair.valuation =
    317    
    318     Fpair.lfp (semantics_ant_nea f_def.f_graph pred_table)
    319    
     318
     319  Fpair.lfp (semantics_ant_nea f_def.f_graph pred_table)
     320
    320321(* ------------ PHASE 2 : delayedness and lateness ----------- *)
    321322(* An expression e is delayable at position p there is a point p' preceding it*)
     
    331332    (valu : Fsing.valuation)
    332333    : Fsing.property =
    333     let preds = Label.Map.find lbl pred_table in
    334    
    335     (* delayed expressions at entry *)
    336     (* take delayed expressions of predecessors which are not the expressions *)
    337                 (* of such predecessors... *)
    338                 let rem_pred lbl' = valu lbl' --* expr_of g lbl' in
    339     let delay_in = big_inter rem_pred preds in
    340                 (* ... and add in anticipatable and earliest expressions *)
    341                 let (ant, nea) = ant_nea lbl in
    342     delay_in ++ (ant -- nea)
    343    
     334  let preds = Label.Map.find lbl pred_table in
     335
     336                (* delayed expressions at entry *)
     337                (* take delayed expressions of predecessors which are not the expressions *)
     338                (* of such predecessors... *)
     339  let rem_pred lbl' = valu lbl' --* expr_of g lbl' in
     340  let delay_in = big_inter rem_pred preds in
     341                (* ... and add in anticipatable and earliest expressions *)
     342  let (ant, nea) = ant_nea lbl in
     343  delay_in ++ (ant -- nea)
     344
    344345let compute_delayed
    345346    (f_def : internal_function)
    346                 (pred_table : Label.t list Label.Map.t)
    347                 (ant_nea : Fpair.valuation)
     347    (pred_table : Label.t list Label.Map.t)
     348    (ant_nea : Fpair.valuation)
    348349    : Fsing.valuation =
    349    
    350     Fsing.lfp (semantics_delay f_def.f_graph pred_table ant_nea)
     350
     351  Fsing.lfp (semantics_delay f_def.f_graph pred_table ant_nea)
    351352
    352353(* An expression is latest at p if it cannot be delayed further *)
    353354let late (g : graph) (delay : Fsing.valuation)
    354   : Fsing.valuation = fun lbl ->
    355         let stmt = Label.Map.find lbl g in
    356         let succs = RTLabsUtilities.statement_successors stmt in
    357        
    358         let eo = match expr_of g lbl with
    359                 | Some e when ExprSet.mem e (delay lbl) -> Some e
    360                 | _ -> None in
    361 
    362   (delay lbl -- big_inter delay succs) ++* eo   
    363        
     355    : Fsing.valuation = fun lbl ->
     356      let stmt = Label.Map.find lbl g in
     357      let succs = RTLabsUtilities.statement_successors stmt in
     358
     359      let eo = match expr_of g lbl with
     360        | Some e when ExprSet.mem e (delay lbl) -> Some e
     361        | _ -> None in
     362
     363      (delay lbl -- big_inter delay succs) ++* eo
     364
    364365
    365366(* --------------- PHASE 3 : isolatedness, optimality and redudancy --------*)
     
    372373let semantics_isolated_used
    373374    (g : graph)
    374                 (late : Fsing.valuation)
     375    (late : Fsing.valuation)
    375376    (lbl : Label.t)
    376377    (valu : Fexprid.valuation)
    377                 : Fexprid.property =
    378        
    379         let stmt = Label.Map.find lbl g in
    380         let succs = RTLabsUtilities.statement_successors stmt in
    381         let f l = late l ++ (fst (valu l) --* expr_of g l) in
    382         let isol = big_inter f succs in
    383        
    384         let f l =
    385                 let used_out = snd (valu l) in
    386                 let used_out = match modified_at g l with
    387                 | Some r when Register.Set.mem r used_out ->
    388                         Register.Set.union (Register.Set.remove r used_out) (vars_of g l)
    389                 | _ -> used_out in
    390                 Register.Set.union used_out (used_at g l) in
    391         let used = big_union f succs in
    392        
    393         (isol, used)
    394        
     378    : Fexprid.property =
     379
     380  let stmt = Label.Map.find lbl g in
     381  let succs = RTLabsUtilities.statement_successors stmt in
     382  let f l = late l ++ (fst (valu l) --* expr_of g l) in
     383  let isol = big_inter f succs in
     384
     385  let f l =
     386    let used_out = snd (valu l) in
     387    let used_out = match modified_at g l with
     388      | Some r when Register.Set.mem r used_out ->
     389        Register.Set.union (Register.Set.remove r used_out) (vars_of g l)
     390      | _ -> used_out in
     391    Register.Set.union used_out (used_at g l) in
     392  let used = big_union f succs in
     393
     394  (isol, used)
     395
    395396let compute_isolated_used
    396397    (f_def : internal_function)
     
    398399    : Fexprid.valuation =
    399400
    400     let graph = f_def.f_graph in
    401                
    402     Fexprid.lfp (semantics_isolated_used graph (late graph delayed))
     401  let graph = f_def.f_graph in
     402
     403  Fexprid.lfp (semantics_isolated_used graph (late graph delayed))
    403404
    404405(* expressions that are optimally placed at point p, without being isolated *)
    405406let optimal (late : Fsing.valuation) (isol : Fsing.valuation)
    406407    : Fsing.valuation = fun lbl ->
    407         late lbl -- isol lbl
     408      late lbl -- isol lbl
    408409
    409410(* mark instructions that are redundant and can be removed *)
    410411let redundant g late isol lbl =
    411         match expr_of g lbl with
    412                 | Some e when ExprSet.mem e (isol lbl) ->
    413                         false
    414                 | Some _ -> true
    415                 | _ -> false
     412  match expr_of g lbl with
     413    | Some e when ExprSet.mem e (isol lbl) ->
     414      false
     415    | Some _ -> true
     416    | _ -> false
    416417
    417418(* mark instructions that modify an unused register *)
    418419let unused g used lbl =
    419     match modified_at g lbl with
    420         | Some r when Register.Set.mem r (used lbl) ->
    421             false
    422         | Some r -> true
    423                                 | _ -> false
     420  match modified_at g lbl with
     421    | Some r when Register.Set.mem r (used lbl) ->
     422      false
     423    | Some r -> true
     424    | _ -> false
    424425
    425426(*------ PHASE 4 : place expressions, remove reduntant ones -------------*)
    426427
    427428let remove_redundant def is_redundant is_unused =
    428         let g = def.f_graph in
    429         let types = RTLabsUtilities.computes_type_map def in
    430         let f lbl stmt (g', s) =
    431                 if is_unused lbl then
     429  let g = def.f_graph in
     430  let types = RTLabsUtilities.computes_type_map def in
     431  let f lbl stmt (g', s) =
     432    if is_unused lbl then
    432433      let succ = List.hd (RTLabsUtilities.statement_successors stmt) in
    433                         (Label.Map.add lbl (St_skip succ) g', s) else
    434                 if is_redundant lbl then
    435                         match modified_at_stmt stmt, expr_of_stmt stmt with
    436                                 | Some r, Some e ->
    437                                         let succ = List.hd (RTLabsUtilities.statement_successors stmt) in
    438                             let (s, (tmp, _)) =
    439                                                 try
    440                                                         (s, ExprMap.find e s)
    441                                                 with
    442                                                         | Not_found ->
    443                                                                 let tmp =       Register.fresh def.f_runiverse in
    444                                                                 let typ = Register.Map.find r types in
    445                                                                 let s = ExprMap.add e (tmp, typ) s in
    446                                                                 (s, (tmp, typ)) in
    447                                         let new_stmt = St_op1 (Op_id, r, tmp, succ) in
    448           (Label.Map.add lbl new_stmt g', s)
    449         | _ -> assert false
    450                 else (g', s) in
    451         let (g, s) = Label.Map.fold f g (g, ExprMap.empty) in
    452         ({ def with f_graph = g }, s)
     434      (Label.Map.add lbl (St_skip succ) g', s) else
     435      if is_redundant lbl then
     436        match modified_at_stmt stmt, expr_of_stmt stmt with
     437          | Some r, Some e ->
     438            let succ = List.hd (RTLabsUtilities.statement_successors stmt) in
     439            let (s, (tmp, _)) =
     440              try
     441                (s, ExprMap.find e s)
     442              with
     443                | Not_found ->
     444                  let tmp =        Register.fresh def.f_runiverse in
     445                  let typ = Register.Map.find r types in
     446                  let s = ExprMap.add e (tmp, typ) s in
     447                  (s, (tmp, typ)) in
     448            let new_stmt = St_op1 (Op_id, r, tmp, succ) in
     449            (Label.Map.add lbl new_stmt g', s)
     450          | _ -> assert false
     451      else (g', s) in
     452  let (g, s) = Label.Map.fold f g (g, ExprMap.empty) in
     453  ({ def with f_graph = g }, s)
    453454
    454455let stmt_of_expr
    455456    (r : Register.t)
    456                 (e : expr)
    457                 (l : Label.t)
    458                 : statement =
    459         match e with
    460 (*              | Cst c -> St_cst (r, c, l)*)
    461                 | UnOp (op, s) -> St_op1 (op, r, s, l)
    462                 | BinOp (op, s, t) -> St_op2 (op, r, s, t, l)
     457    (e : expr)
     458    (l : Label.t)
     459    : statement =
     460  match e with
     461                (*                | Cst c -> St_cst (r, c, l)*)
     462    | UnOp (op, s) -> St_op1 (op, r, s, l)
     463    | BinOp (op, s, t) -> St_op2 (op, r, s, t, l)
    463464
    464465let insert_after exprs redundants g freshl lbl next =
    465466  let f e (next', g') =
    466     try 
     467    try
    467468      let (tmp, _) = ExprMap.find e redundants in
    468469      let opt_calc = stmt_of_expr tmp e next' in
    469470      RTLabsUtilities.insert_in_between freshl g' lbl next' opt_calc
    470                 with
    471                         | Not_found -> (next', g') in
     471    with
     472      | Not_found -> (next', g') in
    472473  snd (ExprSet.fold f exprs (next, g))
    473        
     474
    474475let insert_before exprs redundants g freshl lbl stmt =
    475         let f e (stmt', g') =
    476     try 
     476  let f e (stmt', g') =
     477    try
    477478      let (tmp, _) = ExprMap.find e redundants in
    478                         let n_lbl = freshl () in
     479      let n_lbl = freshl () in
    479480      let opt_calc = stmt_of_expr tmp e n_lbl in
    480                         let g' = Label.Map.add n_lbl stmt' g' in
    481                         let g' = Label.Map.add lbl opt_calc g' in
    482                         (opt_calc, g')
    483      with
    484                         | Not_found -> (stmt', g') in
     481      let g' = Label.Map.add n_lbl stmt' g' in
     482      let g' = Label.Map.add lbl opt_calc g' in
     483      (opt_calc, g')
     484    with
     485      | Not_found -> (stmt', g') in
    485486  snd (ExprSet.fold f exprs (stmt, g))
    486                
     487
    487488let store_optimal_computation (def, redundants) optimal =
    488         (* first add the temporaries' declarations *)
    489         let f _ (r, typ) vars = (r, typ) :: vars in
    490         let f_locals = ExprMap.fold f redundants def.f_locals in
    491        
    492         (* now the actual replacement *)
    493         let g = def.f_graph in
     489        (* first add the temporaries' declarations *)
     490  let f _ (r, typ) vars = (r, typ) :: vars in
     491  let f_locals = ExprMap.fold f redundants def.f_locals in
     492
     493        (* now the actual replacement *)
     494  let g = def.f_graph in
    494495  let freshl () = Label.Gen.fresh def.f_luniverse in
    495         let f lbl stmt g' =
    496                 match stmt with
    497                         (* in case of cost emittance the optimal calculations are inserted *)
    498                         (* after, to preserve preciness *)
    499 (*                      | St_cost (_, next) ->
    500                                 insert_after (optimal lbl) redundants g' freshl lbl next *)
    501                         | _ ->
    502                                 insert_before (optimal lbl) redundants g' freshl lbl stmt in
    503         { def with f_locals = f_locals; f_graph = Label.Map.fold f g g }
    504 
    505                
    506 (* piecing it all together *)           
    507 let transform_internal f_def = 
     496  let f lbl stmt g' =
     497    match stmt with
     498      (* in case of cost emittance the optimal calculations are inserted *)
     499      (* after, to preserve preciness *)
     500      | St_cost (_, next) ->
     501         insert_after (optimal lbl) redundants g' freshl lbl next
     502      | _ ->
     503        insert_before (optimal lbl) redundants g' freshl lbl stmt in
     504  { def with f_locals = f_locals; f_graph = Label.Map.fold f g g }
     505
     506
     507(* piecing it all together *)
     508let transform_internal f_def =
    508509  let pred_table = RTLabsUtilities.compute_predecessor_lists f_def.f_graph in
    509510  let ant_nea = compute_anticipatable_and_non_earliest f_def pred_table in
    510   (*Printf.printf "Ant + Nearl:\n";
    511   print_valu_pair ant_nea f_def.f_graph f_def.f_entry;*)
    512511  let delay = compute_delayed f_def pred_table ant_nea in
    513   (*Printf.printf "Delayed:\n";
    514   print_valu_sing delay f_def.f_graph f_def.f_entry;*)
    515512  let late = late f_def.f_graph delay in
    516   (*Printf.printf "Late:\n";
    517   print_valu_sing late f_def.f_graph f_def.f_entry;*)
    518513  let isol_used = compute_isolated_used f_def delay in
    519         let isol = fun lbl -> fst (isol_used lbl) in
     514  let isol = fun lbl -> fst (isol_used lbl) in
    520515  let used = fun lbl -> snd (isol_used lbl) in
    521   (*Printf.printf "isolated:\n";
    522   print_valu_sing isol f_def.f_graph f_def.f_entry;*)
    523         let opt = optimal late isol in
    524         let redn = redundant f_def.f_graph late isol in
    525         let unusd = unused f_def.f_graph used in
    526   (*Printf.printf "optimal:\n";
    527   print_valu_sing opt f_def.f_graph f_def.f_entry;
    528   Printf.printf "redundant:\n";
    529     let f lbl _ =
    530       Printf.printf "%s : %s\n" lbl (if redn lbl then "yes" else "no") in
    531     RTLabsUtilities.dfs_iter f f_def.f_graph f_def.f_entry;*)
    532         let f lbl _ s = Register.Set.union (used lbl) s in
    533         let regs_used =
    534                 RTLabsUtilities.dfs_fold f f_def.f_graph f_def.f_entry Register.Set.empty in
    535         let filter (r, _) = Register.Set.mem r regs_used in
    536         let f_def = { f_def with f_locals = List.filter filter f_def.f_locals } in
    537         store_optimal_computation (remove_redundant f_def redn unusd) opt
    538        
    539        
     516  let opt = optimal late isol in
     517  let redn = redundant f_def.f_graph late isol in
     518  let unusd = unused f_def.f_graph used in
     519  let f lbl _ s = Register.Set.union (used lbl) s in
     520  let regs_used =
     521    RTLabsUtilities.dfs_fold f f_def.f_graph f_def.f_entry Register.Set.empty in
     522  let filter (r, _) = Register.Set.mem r regs_used in
     523  let f_def = { f_def with f_locals = List.filter filter f_def.f_locals } in
     524  store_optimal_computation (remove_redundant f_def redn unusd) opt
     525
     526
    540527let transform_funct = function
    541         | (f, F_int f_def) -> (f, F_int (transform_internal f_def))
    542         | f -> f
     528  | (f, F_int f_def) -> (f, F_int (transform_internal f_def))
     529  | f -> f
    543530
    544531let trans = Languages.RTLabs, function
    545         | Languages.AstRTLabs p ->
    546                 Languages.AstRTLabs { p with functs = List.map transform_funct p.functs }
    547         | _ -> assert false (* wrong language *)
     532  | Languages.AstRTLabs p ->
     533    Languages.AstRTLabs { p with functs = List.map transform_funct p.functs }
     534  | _ -> assert false (* wrong language *)
  • Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml

    r1542 r1572  
    297297      let oretr = find_olocal lenv oret in
    298298      let old_entry = rtlabs_fun.RTLabs.f_entry in
    299       let stmt = RTLabs.St_call_id (f, regs, oretr, sg, old_entry) in
     299      let regs' = List.map (fun reg -> RTLabs.Reg reg) regs in
     300      let stmt = RTLabs.St_call_id (f, regs', oretr, sg, old_entry) in
    300301      let rtlabs_fun = generate rtlabs_fun stmt in
    301302      translate_exprs rtlabs_fun lenv regs args
     
    306307      let oretr = find_olocal lenv oret in
    307308      let old_entry = rtlabs_fun.RTLabs.f_entry in
    308       let stmt = RTLabs.St_call_ptr (fr, regs, oretr, sg, old_entry) in
     309      let regs' = List.map (fun reg -> RTLabs.Reg reg) regs in
     310      let stmt = RTLabs.St_call_ptr (fr, regs', oretr, sg, old_entry) in
    309311      let rtlabs_fun = generate rtlabs_fun stmt in
    310312      translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args)
     
    313315                          args, sg) ->
    314316      let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
    315       let stmt = RTLabs.St_tailcall_id (f, regs, sg) in
     317      let regs' = List.map (fun reg -> RTLabs.Reg reg) regs in
     318      let stmt = RTLabs.St_tailcall_id (f, regs', sg) in
    316319      let rtlabs_fun = generate rtlabs_fun stmt in
    317320      translate_exprs rtlabs_fun lenv regs args
     
    320323      let (rtlabs_fun, fr) = choose_destination rtlabs_fun lenv f in
    321324      let (rtlabs_fun, regs) = choose_destinations rtlabs_fun lenv args in
    322       let stmt = RTLabs.St_tailcall_ptr (fr, regs, sg) in
     325      let regs' = List.map (fun reg -> RTLabs.Reg reg) regs in
     326      let stmt = RTLabs.St_tailcall_ptr (fr, regs', sg) in
    323327      let rtlabs_fun = generate rtlabs_fun stmt in
    324328      translate_exprs rtlabs_fun lenv (fr :: regs) (f :: args)
     
    445449  let return = match result with
    446450    | None -> None
    447     | Some (retr, _) -> Some retr in
     451    | Some (retr, _) -> Some (RTLabs.Reg retr) in
    448452  let graph = Label.Map.add exit (RTLabs.St_return return) Label.Map.empty in
    449453
Note: See TracChangeset for help on using the changeset viewer.