Changeset 1589 for Deliverables/D2.2/8051
- Timestamp:
- Dec 6, 2011, 5:04:13 PM (9 years ago)
- Location:
- Deliverables/D2.2/8051/src
- Files:
-
- 23 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/src/ASM/I8051.ml
r1568 r1589 162 162 | 130 -> "DPL" 163 163 | 131 -> "DPH" 164 | -1 -> "carry bit" 164 165 | _ -> assert false (* impossible *) 165 166 -
Deliverables/D2.2/8051/src/ERTL/ERTL.mli
r1572 r1589 173 173 174 174 (* Transfer control to the address stored in the return address registers. *) 175 | St_return of argument list175 | St_return 176 176 177 177 type graph = statement Label.Map.t -
Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml
r1572 r1589 436 436 437 437 let compute_result st ret_regs = 438 let vs = List.map (fun r -> get_ arg rst) ret_regs in438 let vs = List.map (fun r -> get_reg (Hdw r) st) ret_regs in 439 439 let f res v = res && (Val.is_int v) in 440 440 let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in … … 452 452 if debug then print_state lbls_offs st ; 453 453 match fetch_stmt lbls_offs st with 454 | ERTL.St_return ret_regswhen Val.eq_address (get_ra st) st.exit ->455 print_and_return_result (compute_result st ret_regs, List.rev st.trace)454 | ERTL.St_return when Val.eq_address (get_ra st) st.exit -> 455 print_and_return_result (compute_result st I8051.rets, List.rev st.trace) 456 456 | stmt -> 457 457 let st' = interpret_stmt lbls_offs st stmt in -
Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml
r1580 r1589 144 144 Printf.sprintf "branch %s <> 0 --> %s, %s" 145 145 (Register.print srcr) lbl_true lbl_false 146 | ERTL.St_return ret_regs->147 Printf.sprintf "return %s" (print_return ret_regs)146 | ERTL.St_return -> 147 Printf.sprintf "return" 148 148 149 149 -
Deliverables/D2.2/8051/src/ERTL/ERTLToLTL.ml
r1585 r1589 104 104 match Liveness.eliminable (G.liveafter label) stmt with 105 105 | Some successor -> 106 Printf.printf "dead %s!\n%!" (ERTLPrinter.print_statement stmt);107 106 LTL.St_skip successor 108 107 | None -> -
Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml
r1572 r1589 52 52 let move_sp_to_dptr off l = 53 53 let off = adjust off in 54 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 55 let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in 56 let l = generate (LTL.St_int (I8051.a, 0, l)) in 57 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 58 let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in 59 LTL.St_int (I8051.a, off, l) 54 if off = 0 then 55 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 56 let l = generate (LTL.St_to_acc (I8051.sph, l)) in 57 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 58 LTL.St_to_acc (I8051.spl, l) 59 else 60 let l = generate (LTL.St_from_acc (I8051.dph, l)) in 61 let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in 62 let l = generate (LTL.St_int (I8051.a, 0, l)) in 63 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 64 let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in 65 LTL.St_int (I8051.a, off, l) 60 66 61 67 … … 73 79 move_sp_to_dptr off l 74 80 75 (* side-effects : dpl, dph, s st*)81 (* side-effects : dpl, dph, st0 *) 76 82 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 83 let l = generate (set_stack_not_a off I8051.st0 l) in 79 84 LTL.St_from_acc (I8051.st0, l) 80 85 … … 99 104 (* side-effects : none if dest = src, a if both colored, 100 105 (dpl, dph, a) if src spilled or src imm and dest spilled, 101 (dpl, dph, a, s st) if dest spilled *)106 (dpl, dph, a, st0) if dest spilled *) 102 107 let move (dest : decision) (src : argument) l = 103 108 match dest, src with -
Deliverables/D2.2/8051/src/ERTL/liveness.ml
r1585 r1589 5 5 (* In the following, a ``variable'' means a pseudo-register or an 6 6 allocatable hardware register. *) 7 8 (* These functions allow turning an [ERTL] control flow graph into an9 explicit graph, that is, making successor edges explicit. This is10 useful in itself and facilitates the computation of predecessor11 edges. *)12 13 let statement_successors (stmt : statement) =14 match stmt with15 | St_return _ ->16 Label.Set.empty17 | St_skip l18 | St_comment (_, l)19 | St_cost (_, l)20 | St_ind_0 (_, l)21 | St_ind_inc (_, l)22 | St_set_hdw (_, _, l)23 | St_get_hdw (_, _, l)24 | St_hdw_to_hdw (_, _, l)25 | St_newframe l26 | St_delframe l27 | St_framesize (_, l)28 | St_push (_, l)29 | St_pop (_, l)30 | St_addrH (_, _, l)31 | St_addrL (_, _, l)32 (* | St_int (_, _, l) *)33 | St_move (_, _, l)34 | St_opaccsA (_, _, _, _, l)35 | St_opaccsB (_, _, _, _, l)36 | St_op1 (_, _, _, l)37 | St_op2 (_, _, _, _, l)38 | St_clear_carry l39 | St_set_carry l40 | St_load (_, _, _, l)41 | St_store (_, _, _, l)42 | St_call_id (_, _, l)43 | St_call_ptr (_, _, _, l) ->44 Label.Set.singleton l45 | St_cond (_, l1, l2) ->46 Label.Set.add l1 (Label.Set.singleton l2)47 7 48 8 (* The analysis uses the lattice of sets of variables. The lattice's … … 99 59 | St_store _ 100 60 | St_cond _ 101 | St_return _->61 | St_return -> 102 62 L.bottom 103 63 | St_clear_carry _ … … 191 151 | St_delframe _ -> 192 152 L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph) 193 | St_return _->153 | St_return -> 194 154 Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs 195 155 … … 207 167 208 168 let eliminable ((pliveafter, hliveafter) : L.t) (stmt : statement) = 209 let res =210 169 match stmt with 211 170 | St_skip _ … … 224 183 | St_call_ptr _ 225 184 | St_cond _ 226 | St_return _->185 | St_return -> 227 186 None 228 187 | St_get_hdw (r, _, l) … … 241 200 | St_set_hdw (r, _, l) 242 201 | St_hdw_to_hdw (r, _, l) -> 243 if I8051.RegisterSet.mem r hliveafter then None else Some l in 244 Printf.printf "%s %sfound eliminable\n" 245 (ERTLPrinter.print_statement stmt) 246 (match res with 247 | Some _ -> "" 248 | _ -> "not "); res 202 if I8051.RegisterSet.mem r hliveafter then None else Some l 249 203 250 204 (* This is the abstract semantics of instructions. It defines the … … 312 266 let liveafter label (liveafter : valuation) : L.t = 313 267 let stmt : statement = Label.Map.find label int_fun.f_graph in 314 L abel.Set.fold(fun successor accu ->268 List.fold_right (fun successor accu -> 315 269 L.join (livebefore successor liveafter) accu 316 ) ( statement_successors stmt) L.bottom270 ) (ERTLGraph.successors stmt) L.bottom 317 271 in 318 272 … … 320 274 321 275 F.lfp liveafter 276 277 (* let print_prop ((reg_s, hdw_s) : L.property) : string = *) 278 (* let fp pr s = Printf.sprintf "%s%s, " s *) 279 (* (Register.print pr) in *) 280 (* let fh hr s = Printf.sprintf "%s%s, " s *) 281 (* (I8051.print_register hr) in *) 282 (* Printf.sprintf "{ %s%s}\n" *) 283 (* (Register.Set.fold fp reg_s "") *) 284 (* (I8051.RegisterSet.fold fh hdw_s "") *) 285 286 (* let print (def : internal_function) (valu : valuation) : string = *) 287 (* let f lbl stmt s = match stmt with *) 288 (* | St_skip _ -> s *) 289 (* | _ -> Printf.sprintf "%s%s : %s\n" s lbl *) 290 (* (print_prop (valu lbl)) in *) 291 (* Label.Map.fold f def.f_graph "" *) -
Deliverables/D2.2/8051/src/ERTL/liveness.mli
r486 r1589 49 49 50 50 val eliminable: L.t -> statement -> Label.t option 51 -
Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml
r1585 r1589 47 47 let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds) 48 48 let new_ind st = { st with inds = CostLabel.new_const_ind st.inds } 49 let forget_ind st = Printf.printf "forgetting\n"; 50 { st with inds = CostLabel.forget_const_ind st.inds } 49 let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds } 51 50 let enter_loop st = CostLabel.enter_loop st.inds 52 51 let continue_loop st = CostLabel.continue_loop st.inds … … 102 101 Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs) 103 102 104 let init_fun_call namelbls_offs st ptr def =103 let init_fun_call lbls_offs st ptr def = 105 104 let pc = entry_pc lbls_offs ptr def in 106 105 let st = new_ind st in 107 Printf.printf "calling %s\n" name;108 106 change_pc st pc 109 107 … … 149 147 150 148 let label_of_pointer lbls_offs ptr = 151 (*152 Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;153 *)154 149 let off = Val.offset_of_address ptr in 155 150 Labels_Offsets.find2 off lbls_offs … … 211 206 change_pc st next_pc 212 207 213 let interpret_call namelbls_offs st ptr ra =208 let interpret_call lbls_offs st ptr ra = 214 209 match Mem.find_fun_def st.mem ptr with 215 210 | LTL.F_int def -> 216 211 let st = save_ra lbls_offs st ra in 217 init_fun_call namelbls_offs st ptr def212 init_fun_call lbls_offs st ptr def 218 213 | LTL.F_ext def -> 219 214 let next_pc = … … 222 217 223 218 let interpret_return lbls_offs st = 224 Printf.printf "returning\n";225 219 let st = forget_ind st in 226 220 let (st, pc) = return_pc st in … … 328 322 329 323 | LTL.St_call_id (f, lbl) -> 330 interpret_call flbls_offs st (Mem.find_global st.mem f) lbl324 interpret_call lbls_offs st (Mem.find_global st.mem f) lbl 331 325 332 326 | LTL.St_call_ptr lbl -> 333 interpret_call (Val.string_of_address (dptr st))lbls_offs st (dptr st) lbl327 interpret_call lbls_offs st (dptr st) lbl 334 328 335 329 | LTL.St_condacc (lbl_true, lbl_false) -> … … 362 356 (res, cost_labels) in 363 357 if debug then print_state lbls_offs st ; 364 Printf.printf "%s\n" (Val.string_of_address st.pc);365 358 match fetch_stmt lbls_offs st with 366 359 | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit -> … … 411 404 match Mem.find_fun_def st.mem ptr with 412 405 | LTL.F_int def -> 413 init_fun_call mainlbls_offs st ptr def406 init_fun_call lbls_offs st ptr def 414 407 | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.") 415 408 -
Deliverables/D2.2/8051/src/RTL/RTL.mli
r1572 r1589 102 102 | St_cond of Register.t * Label.t * Label.t 103 103 104 (* Return the value of some registers (low bytes first). *)105 | St_return of argument list104 (* Return control. *) 105 | St_return 106 106 107 107 -
Deliverables/D2.2/8051/src/RTL/RTLConstPropagation.ml
r1585 r1589 415 415 | St_opaccs (op, i, j, a, b, l) -> 416 416 (simpl_imm_opaccs op i j a b (valu p) l, None) 417 | St_set_carry l when L.find_cst_carry_in (valu p) = Some 1 -> ([], None) 418 | St_clear_carry l when L.find_cst_carry_in (valu p) = Some 0 -> ([], None) 417 419 | St_load (i, a, b, l) -> 418 420 ([St_load(i, arg_from_arg (valu p) a, arg_from_arg (valu p) b, l)], None) … … 426 428 | Some _ -> ([], Some [if_true]) 427 429 | None -> ([s], Some [if_true ; if_false])) 428 | St_return rets ->429 let rets' = List.map (arg_from_arg (valu p)) rets in430 ([St_return rets'], None)431 430 | St_call_id (f, args, rets, l) -> 432 431 let args' = List.map (arg_from_arg (valu p)) args in -
Deliverables/D2.2/8051/src/RTL/RTLGraph.ml
r1580 r1589 62 62 | St_tailcall_id (f, args), [] -> St_tailcall_id (f, args) 63 63 | St_tailcall_ptr (f1, f2, args), [] -> St_tailcall_ptr (f1, f2, args) 64 | St_return regs, [] -> St_return regs64 | St_return, [] -> St_return 65 65 | _ -> invalid_arg "fill_succs: statement and successors do not match" -
Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml
r1572 r1589 19 19 being executed. *) 20 20 21 type local_env = Val.t Register.Map.t 21 type local_env = { 22 le_vals : Val.t Register.Map.t ; 23 le_rets : Register.t list 24 } 22 25 23 26 (* Call frames. The execution state has a call stack, each element of the stack … … 27 30 28 31 type stack_frame = 29 { re t_regs: Register.t list ;32 { result : Register.t list ; 30 33 graph : RTL.graph ; 31 34 pc : Label.t ; … … 55 58 (if Val.eq v Val.undef then "" 56 59 else (Register.print x) ^ " = " ^ (Val.to_string v) ^ " ") in 57 Register.Map.fold f lenv ""60 Register.Map.fold f lenv.le_vals "" 58 61 59 62 let string_of_args args = … … 87 90 88 91 let get_local_value (lenv : local_env) (r : Register.t) : Val.t = 89 if Register.Map.mem r lenv then Register.Map.find r lenv 90 else error ("Unknown local register \"" ^ (Register.print r) ^ "\".") 92 try 93 Register.Map.find r lenv.le_vals 94 with 95 | Not_found -> 96 error ("Unknown local register \"" ^ (Register.print r) ^ "\".") 97 91 98 92 99 let get_local_arg_value (lenv : local_env) : RTL.argument -> Val.t = function … … 108 115 109 116 let assign_state sfrs graph lbl sp lenv carry mem inds trace destrs vs = 110 let lenv = adds destrs vs lenvin117 let lenv = { lenv with le_vals = adds destrs vs lenv.le_vals } in 111 118 State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace) 112 119 … … 210 217 let args = get_arg_values lenv args in 211 218 let sf = 212 { re t_regs= ret_regs ; graph = graph ; pc = lbl ;219 { result = ret_regs ; graph = graph ; pc = lbl ; 213 220 sp = sp ; lenv = lenv ; carry = carry } 214 221 in … … 219 226 let f_def = Mem.find_fun_def mem addr in 220 227 let args = get_arg_values lenv args in 221 let sf = { re t_regs= ret_regs ; graph = graph ; pc = lbl ;228 let sf = { result = ret_regs ; graph = graph ; pc = lbl ; 222 229 sp = sp ; lenv = lenv ; carry = carry } in 223 230 CallState (sf :: sfrs, f_def, args, mem, inds, trace) … … 240 247 branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v 241 248 242 | RTL.St_return rl->243 let vl = List.map (get_local_ arg_value lenv) rlin249 | RTL.St_return -> 250 let vl = List.map (get_local_value lenv) lenv.le_rets in 244 251 let mem = Mem.free mem sp in 245 252 ReturnState (sfrs, vl, mem, inds, trace) … … 255 262 (locals : Register.Set.t) 256 263 (params : Register.t list) 264 (rets : Register.t list) 257 265 (args : Val.t list) : 258 266 local_env = 259 let f r lenv = Register.Map.add r Val.undef lenvin260 let lenv = Register.Set.fold f locals Register.Map.empty in261 let f lenv r v = Register.Map.add r v lenvin262 List.fold_left2 f lenv params args267 let f r lenv_vals = Register.Map.add r Val.undef lenv_vals in 268 let lenv_vals = Register.Set.fold f locals Register.Map.empty in 269 let f lenv_vals r v = Register.Map.add r v lenv_vals in 270 { le_vals = List.fold_left2 f lenv_vals params args ; le_rets = rets } 263 271 264 272 let state_after_call … … 274 282 let inds = new_ind inds in 275 283 let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in 284 let lenv = 285 init_locals def.RTL.f_locals def.RTL.f_params def.RTL.f_result args in 276 286 State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp, 277 init_locals def.RTL.f_locals def.RTL.f_params args,287 lenv, 278 288 Val.undef, mem', inds, trace) 279 289 | RTL.F_ext def -> … … 289 299 (trace : CostLabel.t list) : 290 300 state = 291 let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in 292 let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in 301 let f i lenv_vals r = Register.Map.add r (List.nth ret_vals i) lenv_vals in 302 let lenv = 303 {sf.lenv with 304 le_vals = MiscPottier.foldi f sf.lenv.le_vals sf.result } in 293 305 let inds = forget_ind inds in 294 306 State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace) -
Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml
r1580 r1589 125 125 Printf.sprintf "branch %s <> 0 --> %s, %s" 126 126 (print_reg srcr) lbl_true lbl_false 127 | RTL.St_return regs->128 Printf.sprintf "return %s" (print_return regs)127 | RTL.St_return -> 128 Printf.sprintf "return" 129 129 130 130 … … 143 143 144 144 Printf.sprintf 145 "%s\"%s\"%s\n%slocals: %s\n%s result: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"145 "%s\"%s\"%s\n%slocals: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s" 146 146 (n_spaces n) 147 147 f … … 149 149 (n_spaces (n+2)) 150 150 (print_locals def.RTL.f_locals) 151 ( n_spaces (n+2))152 ( print_result def.RTL.f_result)151 (* (n_spaces (n+2)) *) 152 (* (print_result def.RTL.f_result) *) 153 153 (n_spaces (n+2)) 154 154 def.RTL.f_stacksize -
Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml
r1584 r1589 350 350 add_graph lbl (ERTL.St_cond (srcr, lbl_true, lbl_false)) def 351 351 352 | RTL.St_return ret_regs->353 add_graph lbl (ERTL.St_return ret_regs) def352 | RTL.St_return -> 353 add_graph lbl (ERTL.St_return) def 354 354 355 355 | RTL.St_tailcall_id _ | RTL.St_tailcall_ptr _ -> -
Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli
r1572 r1589 96 96 97 97 (* Return statement. *) 98 | St_return of argument option98 | St_return 99 99 100 100 -
Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml
r1572 r1589 19 19 function being executed. *) 20 20 21 type local_env = (Val.t * AST.sig_type) Register.Map.t 21 type local_env = { 22 le_vals : (Val.t * AST.sig_type) Register.Map.t ; 23 le_ret : Register.t option 24 } 22 25 23 26 (* Call frames. The execution state has a call stack, each element of the stack … … 27 30 28 31 type stack_frame = 29 { re t_reg: Register.t option ;32 { result : Register.t option ; 30 33 graph : RTLabs.graph ; 31 34 sp : Val.address ; … … 53 56 (if Val.eq v Val.undef then "" 54 57 else (Register.print x) ^ " = " ^ (Val.to_string v) ^ " ") in 55 Register.Map.fold f lenv ""58 Register.Map.fold f lenv.le_vals "" 56 59 57 60 let string_of_args args = … … 84 87 85 88 let get_local_env f lenv r = 86 if Register.Map.mem r lenv then f (Register.Map.find r lenv) 87 else error ("Unknown local register \"" ^ (Register.print r) ^ "\".") 89 let a = try Register.Map.find r lenv.le_vals with 90 | Not_found -> 91 error ("Unknown local register \"" ^ (Register.print r) ^ "\".") in 92 f a 88 93 89 94 let get_value = get_local_env fst … … 92 97 93 98 let update_local r v lenv = 94 let f (_, t) = Register.Map.add r (v, t) lenv in95 get_local_env f lenv r99 let f (_, t) = Register.Map.add r (v, t) lenv.le_vals in 100 { lenv with le_vals = get_local_env f lenv r } 96 101 97 102 let update_locals rs vs lenv = … … 209 214 (* Save the stack frame. *) 210 215 let sf = 211 { re t_reg= destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }216 { result = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } 212 217 in 213 218 CallState (sf :: sfrs, f_def, args, mem, inds, trace) … … 219 224 (* Save the stack frame. *) 220 225 let sf = 221 { re t_reg= destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }226 { result = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } 222 227 in 223 228 CallState (sf :: sfrs, f_def, args, mem, inds, trace) … … 275 280 *) 276 281 277 | RTLabs.St_return None->282 | RTLabs.St_return -> 278 283 let mem = Mem.free mem sp in 279 ReturnState (sfrs, Val.undef, mem, inds, trace) 280 281 | RTLabs.St_return (Some r) -> 282 let v = eval_arg lenv mem sp r in 283 let mem = Mem.free mem sp in 284 ReturnState (sfrs, v, mem, inds, trace) 285 284 let res = match lenv.le_ret with 285 | None -> Val.undef 286 | Some r -> get_value lenv r in 287 ReturnState (sfrs, res, mem, inds, trace) 286 288 287 289 module InterpretExternal = Primitive.Interpret (Mem) … … 297 299 (locals : (Register.t * AST.sig_type) list) 298 300 (params : (Register.t * AST.sig_type) list) 301 (ret : (Register.t * AST.sig_type) option) 299 302 (args : Val.t list) : 300 303 local_env = 301 304 let f_param lenv (r, t) v = Register.Map.add r (v, t) lenv in 302 305 let f_local lenv (r, t) = Register.Map.add r (Val.undef, t) lenv in 303 let lenv = List.fold_left2 f_param Register.Map.empty params args in 304 List.fold_left f_local lenv locals 306 let lenv_vals = List.fold_left2 f_param Register.Map.empty params args in 307 let ret = Option.map fst ret in 308 { le_vals = List.fold_left f_local lenv_vals locals; le_ret = ret } 305 309 306 310 let state_after_call … … 316 320 let (mem', sp) = 317 321 Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in 318 let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in 322 let lenv = init_locals 323 def.RTLabs.f_locals 324 def.RTLabs.f_params 325 def.RTLabs.f_result 326 args in 327 let graph = def.RTLabs.f_graph in 319 328 (* allocate new constant indexing *) 320 let graph = def.RTLabs.f_graph in321 329 let inds = new_ind inds in 322 330 State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace) … … 334 342 (trace : CostLabel.t list) : 335 343 state = 336 let lenv = match sf.re t_regwith344 let lenv = match sf.result with 337 345 | None -> sf.lenv 338 346 | Some ret_reg -> update_local ret_reg ret_val sf.lenv in 339 (* erase current indexing and revert to previous one *) 340 let inds = forget_ind inds in 341 State (sfrs, sf.graph, sf.sp, sf.pc, lenv, 342 mem, inds, trace) 347 (* erase current indexing and revert to previous one *) 348 let inds = forget_ind inds in 349 State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, inds, trace) 343 350 344 351 -
Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml
r1580 r1589 245 245 (print_reg r) 246 246 (print_table tbl) 247 | RTLabs.St_return None -> Printf.sprintf "return" 248 | RTLabs.St_return (Some r) -> Printf.sprintf "return %s" (print_arg r) 247 | RTLabs.St_return -> Printf.sprintf "return" 249 248 250 249 -
Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml
r1585 r1589 11 11 let error_shift () = error "Shift operations not supported." 12 12 13 let dummy = Label.dummy 13 14 14 15 let add_graph lbl stmt def = … … 174 175 translate_cst (AST.Cst_int 0) destrs start_lbl dest_lbl def 175 176 176 let translate_cast_signed destrs srcr start_lbl dest_lbl def = 177 let (def, tmpr) = fresh_reg def in 178 let insts = 177 let sign_mask destr srcr = 179 178 (* this sets tmpr to 0xFF if s is neg, 0x00 o.w. Done like that: 180 179 byte in tmpr if srcr is: neg | pos … … 185 184 186 185 *) 187 [RTL.St_op2 (I8051.Or, tmpr, srcr, RTL.Imm 127, start_lbl) ; 188 RTL.St_op1 (I8051.Rl, tmpr, tmpr, start_lbl) ; 189 RTL.St_op1 (I8051.Inc, tmpr, tmpr, start_lbl) ; 190 RTL.St_op1 (I8051.Cmpl, tmpr, tmpr, start_lbl) ] in 186 [RTL.St_op2 (I8051.Or, destr, srcr, RTL.Imm 127, dummy) ; 187 RTL.St_op1 (I8051.Rl, destr, destr, dummy) ; 188 RTL.St_op1 (I8051.Inc, destr, destr, dummy) ; 189 RTL.St_op1 (I8051.Cmpl, destr, destr, dummy) ] 190 191 192 let translate_cast_signed destrs srcr start_lbl dest_lbl def = 193 let (def, tmpr) = fresh_reg def in 191 194 let srcrs = MiscPottier.make (RTL.Reg tmpr) (List.length destrs) in 192 add_translates [adds_graph insts; translate_move destrs srcrs]195 add_translates [adds_graph (sign_mask tmpr srcr); translate_move destrs srcrs] 193 196 start_lbl dest_lbl def 194 197 … … 477 480 478 481 | AST.Op_add | AST.Op_addp -> 479 translate_op I8051.Add cdestrs srcrs1 srcrs2 start_lbl dest_lbl def482 translate_op I8051.Add destrs srcrs1 srcrs2 start_lbl dest_lbl def 480 483 481 484 | AST.Op_sub | AST.Op_subp | AST.Op_subpp -> … … 666 669 error "Jump tables not supported yet." 667 670 668 | RTLabs.St_return None -> 669 add_graph lbl (RTL.St_return []) def 670 671 | RTLabs.St_return (Some r) -> 672 add_graph lbl (RTL.St_return (find_local_env r lenv)) def 671 | RTLabs.St_return -> 672 add_graph lbl RTL.St_return def 673 674 open BList.Notation 673 675 674 676 open BList.Notation … … 708 710 load_args args (fun args -> 709 711 RTLabs.St_tailcall_ptr (f, args, s) ^:: bnil) 710 | RTLabs.St_return (Some a) ->711 load_arg a (fun a ->712 RTLabs.St_return (Some a) ^:: bnil)713 712 | stmt -> stmt ^:: bnil in 714 713 let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in -
Deliverables/D2.2/8051/src/RTLabs/constPropagation.ml
r1580 r1589 332 332 | L.V _ | L.A _ -> ([], Some [if_true]) 333 333 | _ -> ([s], Some [if_true ; if_false])) 334 | St_return (Some a) ->335 ([St_return (Some (arg_from_arg (valu p) types a))], None)336 334 | St_call_id (f, args, ret, sg, l) -> 337 335 ([St_call_id (f, args_from_args (valu p) types args, ret, sg, l)], None) -
Deliverables/D2.2/8051/src/RTLabs/copyPropagation.ml
r1580 r1589 107 107 | St_call_ptr (f, args, ret, sign, l) -> 108 108 St_call_ptr (f, List.map copy_of_arg args, ret, sign, l) 109 | St_return (Some a) -> St_return (Some (copy_of_arg a))110 109 | stmt -> stmt 111 110 -
Deliverables/D2.2/8051/src/RTLabs/redundancyElimination.ml
r1580 r1589 118 118 119 119 (* used in possibly non side-effect-free statements *) 120 let used_at_stmt stmt =120 let used_at_stmt ret stmt = 121 121 let add_arg s = function 122 122 | Reg r -> Register.Set.add r s … … 130 130 | St_store (_, a, b, _) -> 131 131 add_arg (add_arg Register.Set.empty a) b 132 | St_return (Some (Reg r))133 132 | St_cond (r, _, _) -> Register.Set.singleton r 133 | St_return -> 134 begin match ret with 135 | Some (r, _) -> Register.Set.singleton r 136 | None -> Register.Set.empty 137 end 134 138 | _ -> Register.Set.empty 135 139 136 let used_at g n = used_at_stmt (Label.Map.find n g)140 let used_at ret g n = used_at_stmt ret (Label.Map.find n g) 137 141 138 142 module ExprOrdered = struct … … 378 382 (g : graph) 379 383 (type_of : Register.t -> AST.sig_type) 384 (ret : (Register.t * AST.sig_type) option) 380 385 (late : Fsing.valuation) 381 386 (lbl : Label.t) … … 394 399 Register.Set.union (Register.Set.remove r used_out) (vars_of g l) 395 400 | _ -> used_out in 396 Register.Set.union used_out (used_at g l) in401 Register.Set.union used_out (used_at ret g l) in 397 402 let used = big_union f succs in 398 403 … … 406 411 407 412 let graph = f_def.f_graph in 413 let ret = f_def.f_result in 408 414 409 415 Fexprid.lfp 410 (semantics_isolated_used graph type_of (late graph type_of delayed))416 (semantics_isolated_used graph type_of ret (late graph type_of delayed)) 411 417 412 418 (* expressions that are optimally placed at point p, without being isolated *) -
Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml
r1572 r1589 445 445 let exit = Label.Gen.fresh luniverse in 446 446 447 (* The control flow graph: for now, it is only a return instruction at the 448 end. *) 449 let return = match result with 450 | None -> None 451 | Some (retr, _) -> Some (RTLabs.Reg retr) in 452 let graph = Label.Map.add exit (RTLabs.St_return return) Label.Map.empty in 447 let graph = Label.Map.add exit RTLabs.St_return Label.Map.empty in 453 448 454 449 let rtlabs_fun =
Note: See TracChangeset
for help on using the changeset viewer.