Ignore:
Timestamp:
Dec 2, 2011, 3:13:04 PM (9 years ago)
Author:
tranquil
Message:
  • new form of translation written in graphUtilites (mainly as a test before implementation in Matita)
  • rewritten multiplication in RTLasbToRTL
Location:
Deliverables/D2.2/8051/src
Files:
11 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051/src/RTL/RTLConstPropagation.ml

    r1580 r1584  
    333333      (* in the above case if carry is set add unsets it, that's why we must
    334334         make sure it's unset *)
     335
    335336    | Some 255, _, Some 1, I8051.Addc
    336337    | Some 255, _, _, I8051.And ->
    … …  
    341342    | _, Some 255, _, I8051.And ->
    342343      St_move (i, a, l)
     344    | _, _, Some 0, I8051.Addc ->
     345      (* does not change time, but maybe helps getting better results
     346         with liveness analysis *)
     347      St_op2 (I8051.Add, i, arg_from_arg prop a, arg_from_arg prop b, l)
    343348    | _ ->
    344349      St_op2 (op, i, arg_from_arg prop a, arg_from_arg prop b, l)

  • Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

    r1572 r1584  
    1919
    2020let change_label lbl = function
    21   | ERTL.St_skip _ -> ERTL.St_skip lbl
    22   | ERTL.St_comment (s, _) -> ERTL.St_comment (s, lbl)
    23   | ERTL.St_cost (cost_lbl, _) -> ERTL.St_cost (cost_lbl, lbl)
    24   | ERTL.St_ind_0 (i, _) -> ERTL.St_ind_0 (i, lbl)
    25   | ERTL.St_ind_inc (i, _) -> ERTL.St_ind_inc (i, lbl)
    26   | ERTL.St_get_hdw (r1, r2, _) -> ERTL.St_get_hdw (r1, r2, lbl)
    27   | ERTL.St_set_hdw (r1, r2, _) -> ERTL.St_set_hdw (r1, r2, lbl)
    28   | ERTL.St_hdw_to_hdw (r1, r2, _) -> ERTL.St_hdw_to_hdw (r1, r2, lbl)
    29   | ERTL.St_newframe _ -> ERTL.St_newframe lbl
    30   | ERTL.St_delframe _ -> ERTL.St_delframe lbl
    31   | ERTL.St_framesize (r, _) -> ERTL.St_framesize (r, lbl)
    32   | ERTL.St_pop (r, _) -> ERTL.St_pop (r, lbl)
    33   | ERTL.St_push (r, _) -> ERTL.St_push (r, lbl)
    34   | ERTL.St_addrH (r, id, _) -> ERTL.St_addrH (r, id, lbl)
    35   | ERTL.St_addrL (r, id, _) -> ERTL.St_addrL (r, id, lbl)
    36   | ERTL.St_move (r1, a, _) -> ERTL.St_move (r1, a, lbl)
    37   | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, _) ->
    38     ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl)
    39   | ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, _) ->
    40     ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, lbl)
    41   | ERTL.St_op1 (op1, dstr, srcr, _) -> ERTL.St_op1 (op1, dstr, srcr, lbl)
    42   | ERTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
    43     ERTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
    44   | ERTL.St_clear_carry _ -> ERTL.St_clear_carry lbl
    45   | ERTL.St_set_carry _ -> ERTL.St_set_carry lbl
    46   | ERTL.St_load (dstrs, addr1, addr2, _) ->
    47     ERTL.St_load (dstrs, addr1, addr2, lbl)
    48   | ERTL.St_store (addr1, addr2, srcrs, _) ->
    49     ERTL.St_store (addr1, addr2, srcrs, lbl)
    50   | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl)
    51   | ERTL.St_call_ptr (f1, f2, nb_args, _) ->
    52     ERTL.St_call_ptr (f1, f2, nb_args, lbl)
    5321  | ERTL.St_cond _ as inst -> inst
    5422  | ERTL.St_return _ as inst -> inst
     23  | stmt -> ERTLGraph.fill_succs stmt [lbl]
    5524
    5625(* Add a list of instruction in a graph, from one label to another, by creating

  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r1580 r1584  
    115115
    116116let change_label lbl = function
    117   | RTL.St_skip _ -> RTL.St_skip lbl
    118   | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl)
    119   | RTL.St_ind_0 (i, _) -> RTL.St_ind_0 (i, lbl)
    120   | RTL.St_ind_inc (i, _) -> RTL.St_ind_inc (i, lbl)
    121   | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
    122   | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
    123   (* | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl) *)
    124   | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl)
    125   | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) ->
    126     RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl)
    127   | RTL.St_op1 (op1, dstr, srcr, _) -> RTL.St_op1 (op1, dstr, srcr, lbl)
    128   | RTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
    129     RTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
    130   | RTL.St_clear_carry _ -> RTL.St_clear_carry lbl
    131   | RTL.St_set_carry _ -> RTL.St_set_carry lbl
    132   | RTL.St_load (dstrs, addr1, addr2, _) ->
    133     RTL.St_load (dstrs, addr1, addr2, lbl)
    134   | RTL.St_store (addr1, addr2, srcrs, _) ->
    135     RTL.St_store (addr1, addr2, srcrs, lbl)
    136   | RTL.St_call_id (f, args, retrs, _) -> RTL.St_call_id (f, args, retrs, lbl)
    137   | RTL.St_call_ptr (f1, f2, args, retrs, _) ->
    138     RTL.St_call_ptr (f1, f2, args, retrs, lbl)
    139   | RTL.St_tailcall_id (f, args) -> RTL.St_tailcall_id (f, args)
    140   | RTL.St_tailcall_ptr (f1, f2, args) -> RTL.St_tailcall_ptr (f1, f2, args)
    141   | RTL.St_cond _ as inst -> inst
    142   | RTL.St_return regs -> RTL.St_return regs
     117  | (RTL.St_cond _ | RTL.St_return _) as inst -> inst
     118  | stmt -> RTLGraph.fill_succs stmt [lbl]
    143119
    144120(* Add a list of instruction in a graph, from one label to another, by creating
    … …  
    308284  let (def, tmpr) = fresh_reg def in
    309285  let carry_init = match op with
    310     | I8051.Addc | I8051.Sub ->
     286    | I8051.Sub | I8051.Addc ->
    311287      (* depend on carry bit *)
    312288      [RTL.St_clear_carry start_lbl]
    313     | I8051.Add -> assert false (* should not call with add, not correct *)
    314289    | _ -> [] in
    315   let f_add destr srcr1 srcr2 =
     290  let f_add op destr srcr1 srcr2 =
    316291    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
    317292  let insts_add =
    318     MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
     293    match op with
     294      | I8051.Add ->
     295        (* we perform a first add followed by Addc's *)
     296        let f destr srcr1 srcr2 (op, insts) =
     297          (I8051.Addc, f_add op destr srcr1 srcr2 :: insts) in
     298        snd (MiscPottier.fold3_right
     299          f destrs_common srcrs1_common srcrs2_common (I8051.Add, []))
     300      | _ ->
     301        (* we just do the same operation on all *)
     302        MiscPottier.map3 (f_add op) destrs_common srcrs1_common srcrs2_common in
    319303  let f_add_cted destr srcr =
    320304    RTL.St_op2 (op, destr, srcr, RTL.Imm 0, start_lbl) in
    … …  
    331315    start_lbl dest_lbl def
    332316
    333 
    334 let rec translate_mul1 dummy tmpr destrs srcrs1 srcr2 start_lbl =
    335   match destrs, srcrs1 with
    336     | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl
    337     | [destr], [] ->
    338       adds_graph
    339         [RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Imm 0, start_lbl)]
    340         start_lbl
    341     | destr1 :: destr2 :: destrs, [] ->
    342       add_translates
    343         [adds_graph
    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)] ;
    347          translate_cst (AST.Cst_int 0) destrs]
    348         start_lbl
    349     | [destr], srcr1 :: _ ->
    350       adds_graph
    351         [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
    352          RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Reg tmpr, start_lbl)]
    353         start_lbl
    354     | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
    355       add_translates
    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
    363 
    364 let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates
    365     srcr2i =
    366   let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
    367   translates @
    368     (match tmp_destrs2 with
    369       | [] -> []
    370       | tmp_destr2 :: tmp_destrs2 ->
    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])
    378 
    379317let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
    380   let (def, dummy) = fresh_reg def in
    381   let (def, tmpr) = fresh_reg def in
    382   let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
    383   let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
    384   (* let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in *)
    385   let reg r = RTL.Reg r in
    386   let insts_init =
    387     [translate_move fresh_srcrs1 srcrs1 ;
    388      (* translate_move fresh_srcrs2 srcrs2 ; *)
    389      translate_cst (AST.Cst_int 0) destrs] in
    390   let fresh_srcrs1 = List.map reg fresh_srcrs1 in
    391   let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
    392   let insts_mul = MiscPottier.foldi f [] srcrs2 in
    393   add_translates (insts_init @ insts_mul) start_lbl dest_lbl def
    394 
     318  (* we save those parts of srcrs that could be overwritten *)
     319  let save_srcrs a (def, srcrs, init) = match a with
     320    | RTL.Reg r when List.mem r destrs ->
     321      let (def, new_r) = fresh_reg def in
     322      (def, RTL.Reg new_r :: srcrs,
     323       adds_graph [RTL.St_move (new_r, a, start_lbl)] :: init)
     324    | _ -> (def, a :: srcrs, init) in
     325  let (def, fresh_srcrs1, init) =
     326    List.fold_right save_srcrs srcrs1 (def, [], []) in
     327  let (def, fresh_srcrs2, init) =
     328    List.fold_right save_srcrs srcrs2 (def, [], init) in
     329  let srcrs1_n = List.length srcrs1 in
     330  let srcrs2_n = List.length srcrs2 in
     331  let destrs_n = List.length destrs in
     332  (* the next must be an invariant *)
     333  assert (srcrs1_n = destrs_n && destrs_n = srcrs1_n);
     334  (* we pad destrs with a copy of itself that will be added to it at the end
     335     (when the multiplication overflows) and then three more. The routine
     336     should thus handle overflow nicely, but it must be checked *)
     337  let all_destrs = MiscPottier.fill destrs (2 * destrs_n + 3) in
     338  let init = translate_cst (AST.Cst_int 0) destrs :: init in
     339  (* the registries to hold the temporary results of 8-bit mutliplication *)
     340  let (def, a) = fresh_reg def in
     341  let (def, b) = fresh_reg def in
     342  (* when getting the result, this is what is used (padded to 3 bytes *)
     343  let mul_arg = [RTL.Reg a ; RTL.Reg b ; RTL.Imm 0] in
     344  let mul i j =
     345    let s1i, s2j = List.nth fresh_srcrs1 i, List.nth fresh_srcrs2 i in
     346    let k = i + j in
     347    let dloc = MiscPottier.sublist all_destrs k (k+3) in
     348    let dloc_arg = List.map (fun r -> RTL.Reg r) dloc in
     349    [ adds_graph [RTL.St_opaccs (I8051.Mul, a, b, s1i, s2j, start_lbl)] ;
     350      translate_op I8051.Add dloc dloc_arg mul_arg ] in
     351  let insts = List.flatten (List.flatten
     352    (MiscPottier.makei (fun i ->
     353      MiscPottier.makei (mul i) srcrs2_n) srcrs1_n)) in
     354  add_translates (init @ insts) start_lbl dest_lbl def
    395355
    396356let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def =
    … …  
    457417    | [] -> adds_graph [] start_lbl dest_lbl def
    458418    | destr :: destrs ->
    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? *)
    462419      let (srcrs1, srcrs2) = pad_with (RTL.Imm 0) srcrs1 srcrs2 in
    463420      let init = RTL.St_clear_carry start_lbl in
    … …  
    705662    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
    706663
     664open BList.Notation
     665
    707666let remove_non_int_immediates def =
    708   let load_arg a lbl g rs = match a with
     667  let load_arg a f = match a with
    709668    | RTLabs.Imm ((AST.Cst_stack _ | AST.Cst_addrsymbol _) as c, t) ->
    710       let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in
    711       let new_r = Register.fresh def.RTLabs.f_runiverse in
    712       let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in
    713       (new_l, g, (new_r, t) :: rs, RTLabs.Reg new_r)
    714     | _ -> (lbl, g, rs, a) in
    715   let load_args args lbl g rs =
    716     let f a (lbl', g', rs', args') =
    717       let (lbl'', g'', rs'', a') = load_arg a lbl' g' rs' in
    718       (lbl'', g'', rs'', a' :: args') in
    719     List.fold_right f args (lbl, g, rs, []) in
    720   let f lbl stmt (g, rs) =
    721     match stmt with
    722       | RTLabs.St_op2(op, r, a1, a2, l) ->
    723         let (lbl', g, rs, a1) = load_arg a1 lbl g rs in
    724         let (lbl', g, rs, a2) = load_arg a2 lbl' g rs in
    725         let s = RTLabs.St_op2 (op, r, a1, a2, l) in
    726         let g = Label.Map.add lbl' s g in
    727         (g, rs)
    728       | RTLabs.St_store(q, a1, a2, l) ->
    729         let (lbl', g, rs, a1) = load_arg a1 lbl g rs in
    730         let (lbl', g, rs, a2) = load_arg a2 lbl' g rs in
    731         let s = RTLabs.St_store (q, a1, a2, l) in
    732         let g = Label.Map.add lbl' s g in
    733         (g, rs)
    734       | RTLabs.St_load (q, a, r, l) ->
    735         let (lbl', g, rs, a) = load_arg a lbl g rs in
    736         let s = RTLabs.St_load (q, a, r, l) in
    737         let g = Label.Map.add lbl' s g in
    738         (g, rs)
    739       | RTLabs.St_call_id (f, args, ret, s, l) ->
    740         let (lbl', g, rs, args) = load_args args lbl g rs in
    741         let s = RTLabs.St_call_id (f, args, ret, s, l) in
    742         let g = Label.Map.add lbl' s g in
    743         (g, rs)
    744       | RTLabs.St_tailcall_id (f, args, s) ->
    745         let (lbl', g, rs, args) = load_args args lbl g rs in
    746         let s = RTLabs.St_tailcall_id (f, args, s) in
    747         let g = Label.Map.add lbl' s g in
    748         (g, rs)
    749       | RTLabs.St_call_ptr (f, args, ret, s, l) ->
    750         let (lbl', g, rs, args) = load_args args lbl g rs in
    751         let s = RTLabs.St_call_ptr (f, args, ret, s, l) in
    752         let g = Label.Map.add lbl' s g in
    753         (g, rs)
    754       | RTLabs.St_tailcall_ptr (f, args, s) ->
    755         let (lbl', g, rs, args) = load_args args lbl g rs in
    756         let s = RTLabs.St_tailcall_ptr (f, args, s) in
    757         let g = Label.Map.add lbl' s g in
    758         (g, rs)
    759       | RTLabs.St_return (Some a) ->
    760         let (lbl', g, rs, a) = load_arg a lbl g rs in
    761         let s = RTLabs.St_return (Some a) in
    762         let g = Label.Map.add lbl' s g in
    763         (g, rs)
    764       | _ -> (g, rs) in
     669      fresh_t t (fun tmp ->
     670      RTLabs.St_cst (tmp, c, Label.dummy) ^:: f (RTLabs.Reg tmp))
     671    | _ -> f a in
     672  let rec load_args args f = match args with
     673    | [] -> f []
     674    | a :: args ->
     675      load_arg a (fun a -> load_args args (fun l -> f (a :: l))) in
     676  let trans lbl = function
     677    | RTLabs.St_op2(op, r, a1, a2, l) ->
     678      load_arg a1 (fun a1 ->
     679        load_arg a2 (fun a2 ->
     680          RTLabs.St_op2 (op, r, a1, a2, l) ^:: bnil))
     681    | RTLabs.St_store(q, a1, a2, l) ->
     682      load_arg a1 (fun a1 ->
     683        load_arg a2 (fun a2 ->
     684          RTLabs.St_store (q, a1, a2, l) ^:: bnil))
     685    | RTLabs.St_load (q, a, r, l) ->
     686      load_arg a (fun a ->
     687        RTLabs.St_load (q, a, r, l) ^:: bnil)
     688    | RTLabs.St_call_id (f, args, ret, s, l) ->
     689      load_args args (fun args ->
     690        RTLabs.St_call_id (f, args, ret, s, l) ^:: bnil)
     691    | RTLabs.St_tailcall_id (f, args, s) ->
     692      load_args args (fun args ->
     693        RTLabs.St_tailcall_id (f, args, s) ^:: bnil)
     694    | RTLabs.St_call_ptr (f, args, ret, s, l) ->
     695      load_args args (fun args ->
     696        RTLabs.St_call_ptr (f, args, ret, s, l) ^:: bnil)
     697    | RTLabs.St_tailcall_ptr (f, args, s) ->
     698      load_args args (fun args ->
     699        RTLabs.St_tailcall_ptr (f, args, s) ^:: bnil)
     700    | RTLabs.St_return (Some a) ->
     701      load_arg a (fun a ->
     702        RTLabs.St_return (Some a) ^:: bnil)
     703    | stmt -> stmt ^:: bnil in
     704  let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in
    765705  let g = def.RTLabs.f_graph in
    766   let (g, rs) = Label.Map.fold f g (g, []) in
    767   let locals = List.rev_append rs def.RTLabs.f_locals in
    768   { def with RTLabs.f_graph = g; RTLabs.f_locals = locals }
     706  let fresh_reg def t =
     707    let r = Register.fresh def.RTLabs.f_runiverse in
     708    let locals = (r, t) :: def.RTLabs.f_locals in
     709    ({ def with RTLabs.f_locals = locals }, r) in
     710  let fresh_lbl () = Label.Gen.fresh def.RTLabs.f_luniverse in
     711  let (def, g) = T.translate' fresh_lbl fresh_reg trans def g in
     712  { def with RTLabs.f_graph = g }
    769713 
    770714let translate_internal def =

  • Deliverables/D2.2/8051/src/common/label.ml

    r1542 r1584  
    11
    22include StringTools
     3
     4let dummy = ""
    35
    46module ImpMap = struct

  • Deliverables/D2.2/8051/src/common/label.mli

    r1542 r1584  
    55include StringSig.S
    66
     7val dummy : t
     8
    79(** Imperative label maps for use with Fix *)
    810module ImpMap : (Fix.IMPERATIVE_MAPS with type key = t)

  • Deliverables/D2.2/8051/src/utilities/bList.ml

    r1580 r1584  
    11(** This module gives lists with internal binders. *)
    22
    3 type ('a, 'b) t =
    4   | BNil
    5   | BCons of 'a * ('a, 'b) t
    6   | BNew of ('b -> ('a, 'b) t)
    73
    8 let (^::) x l = BCons (x, l)
     4type ('a, 'b, 'c) t =
     5  | Nil
     6  | Cons of 'a * ('a, 'b, 'c) t
     7  | New of 'c * ('b -> ('a, 'b, 'c) t)
    98
    10 let rec (^@) l1 l2 = match l1 with
    11   | BNil -> l2
    12   | BCons (x, l1') -> BCons (x, l1' ^@ l2)
    13   | BNew f -> BNew (fun x -> f x ^@ l2)
     9type ('a, 'b) t2 = ('a, 'b, unit) t
    1410
    15 let (?^) f = BNew f
     11let rec append l1 l2 = match l1 with
     12  | Nil -> l2
     13  | Cons (x, l1') -> Cons (x, append l1' l2)
     14  | New (t, f) -> New (t, fun x -> append (f x) l2)
    1615
    17 let b_rev l =
     16let rev l =
    1817  let rec rev_acc acc = function
    19     | BNil -> acc
    20     | BCons (x, l) -> rev_acc (BCons (x, acc)) l
    21     | BNew f -> BNew (fun x -> rev_acc acc (f x)) in
    22   rev_acc BNil l
     18    | Nil -> acc
     19    | Cons (x, l) -> rev_acc (Cons (x, acc)) l
     20    | New (t, f) -> New (t, fun x -> rev_acc acc (f x)) in
     21  rev_acc Nil l
     22
     23let of_list l = List.fold_right (fun x l -> Cons (x, l)) l Nil
     24
     25let rec compile fresh u l = match l with
     26  | Nil -> (u, [])
     27  | Cons (a, l) ->
     28    let (u', l') = compile fresh u l in
     29    (u', a :: l')
     30  | New (t, f) ->
     31    let (u', r) = fresh u t in
     32    compile fresh u' (f r)
     33
     34let compile2 fresh =
     35  let fresh' u () = fresh u in
     36  compile fresh'
     37
     38let rec fold_left f f_new init = function
     39  | Nil -> init
     40  | Cons (a, l) -> fold_left f f_new (f init a) l
     41  | New (t, f_l) -> f_new t (fun x -> fold_left f f_new init (f_l x))
     42
     43let rec fold_right f f_new l init = match l with
     44  | Nil -> init
     45  | Cons (a, l) -> f a (fold_right f f_new l init)
     46  | New (t, f_l) -> f_new t (fun x -> fold_right f f_new (f_l x) init)
     47
     48let rec concat = function
     49  | [] -> Nil
     50  | l :: ls -> append l (concat ls)
     51
     52let rec fresh_ts ts f = match ts with
     53  | [] -> f []
     54  | t :: ts -> New (t, fun x -> (fresh_ts ts (fun l -> f (x :: l))))
     55
     56let rec fresh_n n f =
     57  if n <= 0 then f [] else
     58    New ((), fun x -> (fresh_n (n - 1) (fun l -> f (x :: l))))
     59
     60module Notation = struct
     61
     62  let (^::) x l = Cons (x, l)
     63  let (^@) = append
     64  let bnil = Nil
     65  let fresh f = New ((), f)
     66  let fresh_n = fresh_n
     67  let fresh_t t f = New (t, f)
     68  let fresh_ts = fresh_ts
     69
     70end

  • Deliverables/D2.2/8051/src/utilities/bList.mli

    r1580 r1584  
    11(** This module gives lists with internal binders. *)
    22
    3 type ('a, 'b) t =
    4   | BNil
    5   | BCons of 'a * ('a, 'b) t
    6   | BNew of ('b -> ('a, 'b) t)
     3type ('a, 'b, 'c) t =
     4  | Nil
     5  | Cons of 'a * ('a, 'b, 'c) t
     6  | New of 'c * ('b -> ('a, 'b, 'c) t)
    77
    8 val (^::) : 'a -> ('a, 'b) t -> ('a, 'b) t
     8type ('a, 'b) t2 = ('a, 'b, unit) t
    99
    10 val (^@) : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t
     10val rev : ('a, 'b, 'c) t -> ('a, 'b, 'c) t
    1111
    12 val (?^) : ('b -> ('a, 'b) t) -> ('a, 'b) t
     12val append : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
    1313
    14 val b_rev : ('a, 'b) t -> ('a, 'b) t
     14val of_list : 'a list -> ('a, 'b, 'c) t
     15
     16val compile : ('u -> 'c -> 'u * 'b) -> 'u -> ('a, 'b, 'c) t -> 'u * 'a list
     17val compile2 : ('u -> 'u * 'b) -> 'u -> ('a, 'b) t2 -> 'u * 'a list
     18
     19val fold_left : ('a -> 'b -> 'a) -> ('d -> ('c -> 'a) -> 'a) -> 'a ->
     20  ('b, 'c, 'd) t -> 'a
     21
     22val fold_right :
     23  ('a -> 'b -> 'b) -> ('d -> ('c -> 'b) -> 'b) -> ('a, 'c, 'd) t -> 'b -> 'b
     24
     25val concat : ('a, 'b, 'c) t list -> ('a, 'b, 'c) t
     26
     27val fresh_n : int -> ('b list -> ('a, 'b) t2) -> ('a, 'b) t2
     28
     29val fresh_ts : 'c list -> ('b list -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t
     30
     31module Notation : sig
     32  val (^::) : 'a -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
     33  val (^@) : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
     34  val bnil : ('a, 'b, 'c) t
     35  val fresh : ('b -> ('a, 'b) t2) -> ('a, 'b) t2
     36  val fresh_n : int -> ('b list -> ('a, 'b) t2) -> ('a, 'b) t2
     37  val fresh_t : 'c -> ('b -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t
     38  val fresh_ts : 'c list -> ('b list -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t
     39end

  • Deliverables/D2.2/8051/src/utilities/graphUtilities.ml

    r1580 r1584  
    8282    NodeMap.filter is_reachable g
    8383
     84  let rec put_rev freshl stmts src dests graph =
     85    match stmts, dests with
     86      | [], [next] -> (src, NodeMap.add src (skip next) graph)
     87      | [last], _ ->
     88        (src, NodeMap.add src (fill_succs last dests) graph)
     89      | last :: stmts, _ ->
     90        let new_l = freshl () in
     91        let graph = NodeMap.add new_l (fill_succs last dests) graph in
     92        (new_l, snd (put_rev freshl stmts src [new_l] graph))
     93      | _ ->
     94        invalid_arg "successors of statement and translation do not match"
     95
     96  let replace freshl lbl stmts succs g =
     97    let succs = match succs with
     98      | Some x -> x
     99      | None -> successors (NodeMap.find lbl g) in
     100
     101    snd (put_rev freshl (List.rev stmts) lbl succs g)
     102
     103  let replace'
     104      (freshl : unit -> node)
     105      (freshr : 'u -> 't -> 'u * 'r)
     106      (lbl : node)
     107      (stmts : (statement, 'r, 't) BList.t)
     108      (succs : node list option)
     109      (def : 'u)
     110      (g : t)
     111      : 'u * t =
     112    let succs = match succs with
     113      | Some x -> x
     114      | None -> successors (NodeMap.find lbl g) in
     115    let (def, l) = BList.compile freshr def stmts in
     116    (def, snd (put_rev freshl l lbl succs g))
     117
     118  let insert freshl lbl stmts g =
     119    let stmt = NodeMap.find lbl g in
     120    let succs = successors (NodeMap.find lbl g) in
     121    put_rev freshl (stmt :: List.rev stmts) lbl succs g
     122
     123  let insert' freshl freshr lbl stmts def g =
     124    let stmt = NodeMap.find lbl g in
     125    let succs = successors (NodeMap.find lbl g) in
     126    let (def, l) = BList.compile freshr def stmts in
     127    let (lbl, g) = put_rev freshl (stmt :: l) lbl succs g in
     128    (def, lbl, g)
     129
    84130end
    85131
    … …  
    155201
    156202  let translate_with_redirects' freshl freshr f def g =
    157 
    158     let rec put_rev stmts src dests def graph =
    159       match stmts, dests with
    160         | BNil, [next] -> (def, Trg.NodeMap.add src (Trg.skip next) graph)
    161         | BCons (last, BNil), _ ->
    162           (def, Trg.NodeMap.add src (Trg.fill_succs last dests) graph)
    163         | BCons (last, stmts), _ ->
    164           let new_l = freshl () in
    165           let graph = Trg.NodeMap.add new_l (Trg.fill_succs last dests) graph in
    166           put_rev stmts src [new_l] def graph
    167         | BNew f_stmts, _ ->
    168           let (def, new_r) = freshr def in
    169           let stmts = f_stmts new_r in
    170           put_rev stmts src dests def graph
    171         | _ ->
    172           invalid_arg "successors of statement and translation do not match" in
    173 
    174     let trans lbl stmt (def, graph) =
     203    let f' def lbl stmt =
    175204      let (stmts, redirects) = f lbl stmt in
    176       let succs = match redirects with
    177         | Some x -> x
    178         | None -> Src.successors stmt in
    179       put_rev (b_rev stmts) lbl succs def graph in
    180 
    181     Src.NodeMap.fold trans g (def, Trg.NodeMap.empty)
     205      let (def, stmts) = BList.compile freshr def stmts in
     206      (def, stmts, redirects) in
     207    translate_with_redirects freshl f' def g
    182208
    183209  let translate' freshl freshr f =
    184210    let f' lbl stmt = (f lbl stmt, None) in
    185211    translate_with_redirects' freshl freshr f'
     212
    186213
    187214

  • Deliverables/D2.2/8051/src/utilities/graphUtilities.mli

    r1580 r1584  
    6464  val dead_code_elim : G.t -> G.node -> G.t
    6565
     66  val replace : (unit -> G.node) ->
     67    G.node -> G.statement list -> G.node list option -> G.t -> G.t
     68
     69  val replace' : (unit -> G.node) -> ('u -> 't -> 'u * 'r) ->
     70    G.node -> (G.statement, 'r, 't) BList.t -> G.node list option ->
     71    'u -> G.t -> 'u * G.t
     72
     73  val insert : (unit -> G.node) ->
     74    G.node -> G.statement list -> G.t -> G.node * G.t
     75
     76  val insert' : (unit -> G.node) -> ('u -> 't -> 'u * 'r) ->
     77    G.node -> (G.statement, 'r, 't) BList.t ->
     78    'u -> G.t -> 'u * G.node * G.t
     79
     80
    6681end
    6782
    … …  
    123138      translation.
    124139      @see translate *)
    125   val translate' : (unit -> node) -> ('u -> 'u * 'reg) ->
    126     (node -> Src.statement -> (Trg.statement, 'reg) BList.t) ->
     140  val translate' : (unit -> node) -> ('u -> 't -> 'u * 'reg) ->
     141    (node -> Src.statement -> (Trg.statement, 'reg, 't) BList.t) ->
    127142    'u -> Src.t -> 'u * Trg.t
    128143
    … …  
    131146      @see translate'
    132147      @see translate_with_redirect *)
    133   val translate_with_redirects' : (unit -> node) -> ('u -> 'u * 'reg) ->
     148  val translate_with_redirects' : (unit -> node) -> ('u -> 't -> 'u * 'reg) ->
    134149    (node -> Src.statement ->
    135      (Trg.statement, 'reg) BList.t * node list option) ->
     150     (Trg.statement, 'reg, 't) BList.t * node list option) ->
    136151    'u -> Src.t -> 'u * Trg.t
    137152

  • Deliverables/D2.2/8051/src/utilities/miscPottier.ml

    r818 r1584  
    11
    2 let rec map3 f al bl cl =
     2let map3 f al bl cl =
    33  let f' ((a, b), c) = f a b c in
    44  List.map f' (List.combine (List.combine al bl) cl)
     5
     6let fold3_right f al bl cl =
     7  let f' ((a, b), c) d = f a b c d in
     8  List.fold_right f' (List.combine (List.combine al bl) cl)
    59
    610let rec max_list = function
    … …  
    2529
    2630let rec make a n =
    27   if n = 0 then []
     31  if n <= 0 then []
    2832  else a :: (make a (n-1))
     33
     34let makei f n =
     35  let rec app f k =
     36  if k >= n then []
     37  else f k :: (app f (k + 1)) in
     38  app f 0
    2939
    3040let index_of x =
    … …  
    159169  in
    160170  aux
     171
     172
     173let rec sublist l k h =
     174  if h < k || h < 0 || k < 0 then
     175    invalid_arg "sublist: invalid interval"
     176  else
     177  match k, h, l with
     178  | 0, 0, _ -> []
     179  | 0, _, x :: l -> x :: sublist l 0 (h-1)
     180  | _, _, x :: l -> sublist l (k-1) (h-1)
     181  | _ -> invalid_arg "sublist: invalid interval"
     182
     183let rec fill l n =
     184  let k = List.length l in
     185  if k = 0 then invalid_arg "fill: list empty" else
     186  if n < 0 then invalid_arg "fill: negative argument" else
     187  if n <= k then sublist l 0 n else
     188    l @ fill l (n - k)

  • Deliverables/D2.2/8051/src/utilities/miscPottier.mli

    r818 r1584  
    1010   size. *)
    1111val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
     12val fold3_right : ('a -> 'b -> 'c -> 'd -> 'd) ->
     13  'a list -> 'b list -> 'c list -> 'd -> 'd
    1214
    1315val max_list : 'a list -> 'a
    … …  
    1618
    1719val make: 'a -> int -> 'a list
     20
     21val makei : (int -> 'a) -> int -> 'a list
    1822
    1923val index_of : 'a -> 'a list -> int
    … …  
    8488
    8589val string_of_list: string -> ('a -> string) -> 'a list -> string
     90
     91(* [sublist h k l] gives the sublist of [l] starting from index [h] to
     92   [k] excluded. Can raise [Invalid_argument "sublist: invalid interval"]. *)
     93val sublist : 'a list -> int -> int -> 'a list
     94
     95(* [fill l n] makes a list of length [n] using elements from [l], possibly
     96   repeating it. Raises Invalid_argument if [n < 0] or [l = []]. *)
     97val fill : 'a list -> int -> 'a list
     98
Note: See TracChangeset for help on using the changeset viewer.