Changeset 1349 for Deliverables/D2.2
- Timestamp:
- Oct 10, 2011, 11:32:44 PM (9 years ago)
- 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 103 103 [ instruction 104 104 | `Cost of CostLabel.t 105 | `Index of int 106 | `Inc of int 105 107 | `Label of string 106 108 | `Jmp of string … … 122 124 type program = 123 125 { code : BitVectors.byte list ; 126 inds : int BitVectors.WordMap.t ; (* loop index resets *) 127 incs : int BitVectors.WordMap.t ; (* loop index increments *) 124 128 cost_labels : CostLabel.t BitVectors.WordMap.t ; 125 129 exit_addr : BitVectors.word ; -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMInterpret.ml
r1291 r1349 131 131 132 132 exit_addr : BitVectors.word; 133 134 ind_0s : int BitVectors.WordMap.t; 135 ind_incs : int BitVectors.WordMap.t; 133 136 cost_labels : CostLabel.t BitVectors.WordMap.t 134 137 } … … 284 287 285 288 exit_addr = BitVectors.zero `Sixteen; 289 ind_0s = BitVectors.WordMap.empty; 290 ind_incs = BitVectors.WordMap.empty; 286 291 cost_labels = BitVectors.WordMap.empty 287 292 } … … 950 955 ) (StringTools.Map.empty,0) p.ASM.ppreamble 951 956 in 952 let pc,exit_addr,labels, costs =957 let pc,exit_addr,labels,inds,incs,costs = 953 958 List.fold_left 954 (fun (pc,exit_addr,labels, costs) i ->959 (fun (pc,exit_addr,labels,inds,incs,costs) i -> 955 960 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 960 967 | `Jmp _ 961 | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, costs968 | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs 962 969 (*CSC: very stupid: always expand to worst opcode *) 963 970 | `WithLabel i -> … … 967 974 assert (fake_jump = i'); 968 975 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) 970 977 | #instruction as i -> 971 978 let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in 972 979 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) 974 981 ) 975 982 (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 977 985 in 978 986 let code = … … 980 988 (function 981 989 `Label _ 982 | `Cost _ -> [] 990 | `Cost _ 991 | `Index _ 992 | `Inc _ -> [] 983 993 | `WithLabel i -> 984 994 (* We need to expand a conditional jump to a label to a machine language … … 1045 1055 assembly1 (`LCALL (`ADDR16 pc_offset )) 1046 1056 | #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 ; 1048 1058 ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main } 1049 1059 ;; … … 1973 1983 { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels } 1974 1984 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 ; 1985 type cost_trace = { 1986 mutable ct_labels : CostLabel.t list; 1987 mutable ct_inds : CostLabel.const_indexing list; 1988 } 1989 1990 (* TODO: indexes *) 1991 let 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; 1981 1998 if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st 1982 1999 … … 1996 2013 if p.ASM.has_main then 1997 2014 let st = load_program p in 1998 let trace = ref []in2015 let trace = {ct_labels = []; ct_inds = []} in 1999 2016 let callback = observe_trace trace in 2000 2017 let st = execute callback st in … … 2002 2019 if debug then 2003 2020 Printf.printf "Result = %s\n%!" (IntValue.Int32.to_string res) ; 2004 (res, List.rev !trace)2021 (res, List.rev trace.ct_labels) 2005 2022 else (IntValue.Int32.zero, []) -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMInterpret.mli
r1291 r1349 98 98 99 99 exit_addr : BitVectors.word; 100 101 ind_0s : int BitVectors.WordMap.t; 102 ind_incs : int BitVectors.WordMap.t; 100 103 cost_labels : CostLabel.t BitVectors.WordMap.t 101 104 } -
Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/Pretty.ml
r1291 r1349 45 45 (* ugly-printing *) 46 46 | `Cost l -> CostLabel.string_of_cost_label l ^ ":" 47 | `Index i -> "index " ^ string_of_int i ^ ":" 48 | `Inc i -> "increment " ^ string_of_int i ^ ":" 47 49 | `Jmp j -> "ljmp " ^ j 48 50 | `Call j -> "lcall " ^ j -
Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LIN.mli
r818 r1349 18 18 (* Emit a cost label. *) 19 19 | 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 20 26 21 27 (* Assign an integer constant to a register. Parameters are the destination -
Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINInterpret.ml
r818 r1349 21 21 22 22 type hdw_reg_env = Val.t I8051.RegisterMap.t 23 24 25 type indexing = CostLabel.const_indexing 23 26 24 27 (* Execution states. *) … … 31 34 renv : hdw_reg_env ; 32 35 mem : memory ; 36 inds : indexing list ; 33 37 trace : CostLabel.t list } 34 38 … … 45 49 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace) 46 50 51 let forget_ind st = match st.inds with 52 | _ :: tail -> {st with inds = tail} 53 | _ -> assert false (* indexing list must be non-empty *) 54 let curr_ind st = match st.inds with 55 | ind :: _ -> ind 56 | _ -> assert false (* indexing list must be non-empty *) 57 let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds } 58 59 let 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 47 65 let empty_state = 48 66 { pc = Val.null ; … … 52 70 renv = I8051.RegisterMap.empty ; 53 71 mem = Mem.empty ; 72 inds = [] ; 54 73 trace = [] } 55 74 … … 71 90 else error msg 72 91 73 let init_fun_call st ptr = 92 let init_fun_call st ptr def = 93 let st = allocate_ind st (max_depth def) in 74 94 change_pc st (Val.change_address_offset ptr Val.Offset.zero) 75 95 … … 171 191 | LIN.F_int def -> 172 192 let st = save_ra st in 173 init_fun_call st ptr 193 init_fun_call st ptr def 174 194 | LIN.F_ext def -> 175 195 let st = next_pc st in … … 177 197 178 198 let interpret_return st = 199 let st = forget_ind st in 179 200 let (st, pc) = return_pc st in 180 201 change_pc st pc … … 196 217 197 218 | LIN.St_cost cost_lbl -> 219 let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in 198 220 let st = add_trace st cost_lbl in 199 221 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 200 230 201 231 | LIN.St_int (r, i) -> … … 348 378 match Mem.find_fun_def st.mem ptr with 349 379 | LIN.F_int def -> 350 init_fun_call st ptr 380 init_fun_call st ptr def 351 381 | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.") 352 382 -
Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINPrinter.ml
r1291 r1349 28 28 let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in 29 29 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 30 34 | LIN.St_int (dstr, i) -> 31 35 Printf.sprintf "imm %s, %d" (print_reg dstr) i -
Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINToASM.ml
r1291 r1349 51 51 | LIN.St_comment _ -> [] 52 52 | 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! *)] 53 55 | LIN.St_int (r, i) -> 54 56 [`MOV (`U3 (I8051.reg_addr r, data_of_int i))] -
Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLToLIN.ml
r818 r1349 22 22 | LTL.St_cost (lbl, _) -> 23 23 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 24 28 | LTL.St_int (r, i, _) -> 25 29 LIN.St_int (r, i) -
Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLToLINI.ml
r818 r1349 117 117 | LTL.St_comment (_, l) 118 118 | LTL.St_cost (_, l) 119 | LTL.St_ind_0 (_, l) 120 | LTL.St_ind_inc (_, l) 119 121 | LTL.St_int (_, _, l) 120 122 | LTL.St_pop l -
Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml
r1328 r1349 153 153 (* A loop address like [2, 0, 1] means the corresponding label is in the *) 154 154 (* 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 155 let 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 159 160 (* I am supposing you cannot jump to the update statement of for loops... *) 160 161 | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) -> … … 182 183 183 184 (* 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]. *) 186 let 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 188 191 (* I am supposing you cannot jump to the update statement of for loops... *) 189 192 | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
Note: See TracChangeset
for help on using the changeset viewer.