Changeset 1349 for Deliverables/D2.2


Ignore:
Timestamp:
Oct 10, 2011, 11:32:44 PM (9 years ago)
Author:
tranquil
Message:
  • work on LIN completed
  • small implementation of extensible arrays
Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
2 added
11 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASM.mli

    r1291 r1349  
    103103 [ instruction
    104104 | `Cost of CostLabel.t
     105 | `Index of int
     106 | `Inc of int
    105107 | `Label of string
    106108 | `Jmp of string
    … …  
    122124type program =
    123125    { code        : BitVectors.byte list ;
     126      inds        : int BitVectors.WordMap.t ; (* loop index resets *)
     127      incs        : int BitVectors.WordMap.t ; (* loop index increments *)
    124128      cost_labels : CostLabel.t BitVectors.WordMap.t ;
    125129      exit_addr   : BitVectors.word ;

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMInterpret.ml

    r1291 r1349  
    131131
    132132  exit_addr   : BitVectors.word;
     133       
     134        ind_0s      : int BitVectors.WordMap.t;
     135  ind_incs    : int BitVectors.WordMap.t;
    133136  cost_labels : CostLabel.t BitVectors.WordMap.t
    134137}
    … …  
    284287
    285288  exit_addr = BitVectors.zero `Sixteen;
     289  ind_0s = BitVectors.WordMap.empty;
     290  ind_incs = BitVectors.WordMap.empty;
    286291  cost_labels = BitVectors.WordMap.empty
    287292}
    … …  
    950955   ) (StringTools.Map.empty,0) p.ASM.ppreamble
    951956 in
    952  let pc,exit_addr,labels,costs =
     957 let pc,exit_addr,labels,inds,incs,costs =
    953958  List.fold_left
    954    (fun (pc,exit_addr,labels,costs) i ->
     959   (fun (pc,exit_addr,labels,inds,incs,costs) i ->
    955960     match i with
    956         `Label s when s = p.ASM.pexit_label -> pc, pc, StringTools.Map.add s pc labels, costs
    957       | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, costs
    958       | `Cost s -> pc, exit_addr, labels, BitVectors.WordMap.add pc s costs
    959       | `Mov (_,_) -> (snd (half_add pc (vect_of_int 1 `Sixteen))), exit_addr, labels, costs
     961        `Label s when s = p.ASM.pexit_label -> pc, pc, StringTools.Map.add s pc labels, inds, incs, costs
     962      | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, inds, incs, costs
     963      | `Cost s -> pc, exit_addr, labels, inds, incs, BitVectors.WordMap.add pc s costs
     964                        | `Index i -> pc, exit_addr, labels, BitVectors.WordMap.add pc i inds, incs, costs
     965      | `Inc i -> pc, exit_addr, labels, inds, BitVectors.WordMap.add pc i incs, costs
     966      | `Mov (_,_) -> (snd (half_add pc (vect_of_int 1 `Sixteen))), exit_addr, labels, inds, incs, costs
    960967      | `Jmp _
    961       | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, costs
     968      | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs
    962969      (*CSC: very stupid: always expand to worst opcode *)
    963970      | `WithLabel i ->
    … …  
    967974        assert (fake_jump = i');
    968975        let pc' = snd (half_add pc' (vect_of_int 5 `Sixteen)) in
    969           (snd (half_add pc pc'), exit_addr, labels, costs)
     976          (snd (half_add pc pc'), exit_addr, labels, inds, incs, costs)
    970977      | #instruction as i ->
    971978        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
    972979         assert (i = i');
    973          (snd (half_add pc pc'),exit_addr,labels, costs)
     980         (snd (half_add pc pc'),exit_addr,labels, inds, incs, costs)
    974981   )
    975982    (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen,
    976      StringTools.Map.empty, BitVectors.WordMap.empty) p.ASM.pcode
     983     StringTools.Map.empty, BitVectors.WordMap.empty, BitVectors.WordMap.empty,
     984                 BitVectors.WordMap.empty) p.ASM.pcode
    977985 in
    978986 let code =
    … …  
    980988     (function
    981989        `Label _
    982       | `Cost _ -> []
     990      | `Cost _
     991                        | `Index _
     992                        | `Inc _ -> []
    983993      | `WithLabel i ->
    984994         (* We need to expand a conditional jump to a label to a machine language
    … …  
    10451055            assembly1 (`LCALL (`ADDR16 pc_offset ))
    10461056      | #instruction as i -> assembly1 i) p.ASM.pcode) in
    1047  { ASM.code = code ; ASM.cost_labels = costs ;
     1057 { ASM.code = code ; ASM.inds = inds; ASM.incs = incs; ASM.cost_labels = costs ;
    10481058   ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main }
    10491059;;
    … …  
    19731983  { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels }
    19741984
    1975 let observe_trace trace_ref st =
    1976   let cost_label =
    1977     if BitVectors.WordMap.mem st.pc st.cost_labels then
    1978       [BitVectors.WordMap.find st.pc st.cost_labels]
    1979     else [] in
    1980   trace_ref := cost_label @ !trace_ref ;
     1985type cost_trace = {
     1986        mutable ct_labels : CostLabel.t list;
     1987        mutable ct_inds   : CostLabel.const_indexing list;
     1988}
     1989
     1990(* TODO: indexes *)
     1991let observe_trace trace st =
     1992        let update_ct_labels =
     1993          try
     1994                        let cost_label = BitVectors.WordMap.find st.pc st.cost_labels in
     1995            trace.ct_labels <- cost_label :: trace.ct_labels
     1996          with Not_found -> () in
     1997        update_ct_labels;
    19811998  if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st
    19821999
    … …  
    19962013  if p.ASM.has_main then
    19972014    let st = load_program p in
    1998     let trace = ref [] in
     2015    let trace = {ct_labels = []; ct_inds = []} in
    19992016    let callback = observe_trace trace in
    20002017    let st = execute callback st in
    … …  
    20022019    if debug then
    20032020      Printf.printf "Result = %s\n%!" (IntValue.Int32.to_string res) ;
    2004     (res, List.rev !trace)
     2021    (res, List.rev trace.ct_labels)
    20052022  else (IntValue.Int32.zero, [])

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMInterpret.mli

    r1291 r1349  
    9898
    9999      exit_addr   : BitVectors.word;
     100
     101      ind_0s      : int BitVectors.WordMap.t;
     102      ind_incs    : int BitVectors.WordMap.t;
    100103      cost_labels : CostLabel.t BitVectors.WordMap.t
    101104    }

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/Pretty.ml

    r1291 r1349  
    4545                (* ugly-printing *)
    4646  | `Cost l -> CostLabel.string_of_cost_label l ^ ":"
     47        | `Index i -> "index " ^ string_of_int i ^ ":"
     48  | `Inc i -> "increment " ^ string_of_int i ^ ":"
    4749  | `Jmp j -> "ljmp  " ^ j
    4850  | `Call j -> "lcall " ^ j

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LIN.mli

    r818 r1349  
    1818  (* Emit a cost label. *)
    1919  | St_cost of CostLabel.t
     20
     21  (* Reset to 0 a loop index *)
     22  | St_ind_0 of CostLabel.index
     23
     24  (* Increment a loop index *)
     25  | St_ind_inc of CostLabel.index
    2026
    2127  (* Assign an integer constant to a register. Parameters are the destination

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINInterpret.ml

    r818 r1349  
    2121
    2222type hdw_reg_env = Val.t I8051.RegisterMap.t
     23
     24
     25type indexing = CostLabel.const_indexing
    2326
    2427(* Execution states. *)
    … …  
    3134      renv   : hdw_reg_env ;
    3235      mem    : memory ;
     36                        inds   : indexing list ;
    3337      trace  : CostLabel.t list }
    3438
    … …  
    4549let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    4650
     51let forget_ind st = match st.inds with
     52    | _ :: tail -> {st with inds = tail}
     53    | _ -> assert false (* indexing list must be non-empty *)
     54let curr_ind st = match st.inds with
     55    | ind :: _ -> ind
     56    | _ -> assert false (* indexing list must be non-empty *)
     57let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds }
     58
     59let max_depth =
     60    let f_stmt j = function
     61        | LIN.St_ind_0 i | LIN.St_ind_inc i -> max (i + 1) j
     62        | _ -> j in
     63    List.fold_left f_stmt 0
     64
    4765let empty_state =
    4866  { pc     = Val.null ;
    … …  
    5270    renv   = I8051.RegisterMap.empty ;
    5371    mem    = Mem.empty ;
     72                inds   = [] ;
    5473    trace  = [] }
    5574
    … …  
    7190  else error msg
    7291
    73 let init_fun_call st ptr =
     92let init_fun_call st ptr def =
     93        let st = allocate_ind st (max_depth def) in
    7494  change_pc st (Val.change_address_offset ptr Val.Offset.zero)
    7595
    … …  
    171191    | LIN.F_int def ->
    172192      let st = save_ra st in
    173       init_fun_call st ptr
     193      init_fun_call st ptr def
    174194    | LIN.F_ext def ->
    175195      let st = next_pc st in
    … …  
    177197
    178198let interpret_return st =
     199        let st = forget_ind st in
    179200  let (st, pc) = return_pc st in
    180201  change_pc st pc
    … …  
    196217
    197218    | LIN.St_cost cost_lbl ->
     219                        let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in
    198220      let st = add_trace st cost_lbl in
    199221      next_pc st
     222                       
     223                | LIN.St_ind_0 i ->
     224                        CostLabel.enter_loop (Some i) (curr_ind st);
     225                        next_pc st
     226
     227    | LIN.St_ind_inc i ->
     228            CostLabel.continue_loop (Some i) (curr_ind st);
     229            next_pc st
    200230
    201231    | LIN.St_int (r, i) ->
    … …  
    348378  match Mem.find_fun_def st.mem ptr with
    349379    | LIN.F_int def ->
    350       init_fun_call st ptr
     380      init_fun_call st ptr def
    351381    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
    352382

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINPrinter.ml

    r1291 r1349  
    2828    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    2929                Printf.sprintf "emit %s" cost_lbl
     30  | LIN.St_ind_0 i ->
     31    Printf.sprintf "index %d" i
     32  | LIN.St_ind_inc i ->
     33    Printf.sprintf "increment %d" i
    3034  | LIN.St_int (dstr, i) ->
    3135    Printf.sprintf "imm %s, %d" (print_reg dstr) i

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINToASM.ml

    r1291 r1349  
    5151  | LIN.St_comment _ -> []
    5252  | LIN.St_cost lbl -> [`Cost lbl ; `NOP (* TODO: hack! Need to make the difference between cost labels and regular labels. *)]
     53  | LIN.St_ind_0 i -> [`Index i ; `NOP (* TODO: hack! *)]
     54  | LIN.St_ind_inc i -> [`Inc i ; `NOP (* TODO: hack! *)]
    5355  | LIN.St_int (r, i) ->
    5456    [`MOV (`U3 (I8051.reg_addr r, data_of_int i))]

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLToLIN.ml

    r818 r1349  
    2222  | LTL.St_cost (lbl, _) ->
    2323    LIN.St_cost lbl
     24        | LTL.St_ind_0 (i, _) ->
     25                LIN.St_ind_0 i
     26        | LTL.St_ind_inc (i, _) ->
     27                LIN.St_ind_inc i
    2428  | LTL.St_int (r, i, _) ->
    2529    LIN.St_int (r, i)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLToLINI.ml

    r818 r1349  
    117117        | LTL.St_comment (_, l)
    118118        | LTL.St_cost (_, l)
     119        | LTL.St_ind_0 (_, l)
     120        | LTL.St_ind_inc (_, l)
    119121        | LTL.St_int (_, _, l)
    120122        | LTL.St_pop l

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml

    r1328 r1349  
    153153(* A loop address like [2, 0, 1] means the corresponding label is in the *)
    154154(* third loop inside the first loop inside the second loop of the body. The *)
    155 (* type is *)
    156 (* int list -> int -> map -> Clight.statement -> int * map *)
    157 (* where map = int list Label.Map.t *)
    158 let rec assign_loop_addrs_s current offset m = function
     155let rec assign_loop_addrs_s
     156    (current : int list)
     157                (offset  : int)
     158                (m       : int list Label.Map.t)
     159                : Clight.statement -> int*int list Label.Map.t = function
    159160        (* I am supposing you cannot jump to the update statement of for loops... *)
    160161        | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
    … …  
    182183
    183184(* traversal of code which for every statement [s] returns the set of loop*)
    184 (* addresses which are multi-entry due to a goto in [s]. The type is *)
    185 (* map -> int list -> int -> statement -> int*set *)
    186 (* where maps is as above, set = InListSet.t *)
    187 let rec find_multi_entry_loops_s m current offset = function
     185(* addresses which are multi-entry due to a goto in [s]. *)
     186let rec find_multi_entry_loops_s
     187    (m       : int list Label.Map.t)
     188                (current : int list)
     189                (offset  : int)
     190                : Clight.statement -> int*IntListSet.t = function
    188191        (* I am supposing you cannot jump to the update statement of for loops... *)
    189192        | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
Note: See TracChangeset for help on using the changeset viewer.