Changeset 1585 for Deliverables/D2.2
- Timestamp:
- Dec 2, 2011, 7:49:19 PM (9 years ago)
- Location:
- Deliverables/D2.2/8051/src
- Files:
-
- 2 added
- 11 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.mli
r486 r1585 2 2 (** This module provides a function to print [ERTL] programs. *) 3 3 4 val print_statement : ERTL.statement -> string 5 4 6 val print_program : ERTL.program -> string -
Deliverables/D2.2/8051/src/ERTL/ERTLToLTL.ml
r1272 r1585 104 104 match Liveness.eliminable (G.liveafter label) stmt with 105 105 | Some successor -> 106 LTL.St_skip successor 106 Printf.printf "dead %s!\n%!" (ERTLPrinter.print_statement stmt); 107 LTL.St_skip successor 107 108 | None -> 108 109 I.translate_statement stmt -
Deliverables/D2.2/8051/src/ERTL/liveness.ml
r1580 r1585 207 207 208 208 let eliminable ((pliveafter, hliveafter) : L.t) (stmt : statement) = 209 let res = 209 210 match stmt with 210 211 | St_skip _ … … 240 241 | St_set_hdw (r, _, l) 241 242 | St_hdw_to_hdw (r, _, l) -> 242 if I8051.RegisterSet.mem r hliveafter then None else Some 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 243 249 244 250 (* This is the abstract semantics of instructions. It defines the -
Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml
r1572 r1585 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 = { st with inds = CostLabel.forget_const_ind st.inds } 49 let forget_ind st = Printf.printf "forgetting\n"; 50 { st with inds = CostLabel.forget_const_ind st.inds } 50 51 let enter_loop st = CostLabel.enter_loop st.inds 51 52 let continue_loop st = CostLabel.continue_loop st.inds … … 101 102 Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs) 102 103 103 let init_fun_call lbls_offs st ptr def =104 let init_fun_call name lbls_offs st ptr def = 104 105 let pc = entry_pc lbls_offs ptr def in 105 106 let st = new_ind st in 107 Printf.printf "calling %s\n" name; 106 108 change_pc st pc 107 109 … … 209 211 change_pc st next_pc 210 212 211 let interpret_call lbls_offs st ptr ra =213 let interpret_call name lbls_offs st ptr ra = 212 214 match Mem.find_fun_def st.mem ptr with 213 215 | LTL.F_int def -> 214 216 let st = save_ra lbls_offs st ra in 215 init_fun_call lbls_offs st ptr def217 init_fun_call name lbls_offs st ptr def 216 218 | LTL.F_ext def -> 217 219 let next_pc = … … 220 222 221 223 let interpret_return lbls_offs st = 224 Printf.printf "returning\n"; 222 225 let st = forget_ind st in 223 226 let (st, pc) = return_pc st in … … 325 328 326 329 | LTL.St_call_id (f, lbl) -> 327 interpret_call lbls_offs st (Mem.find_global st.mem f) lbl330 interpret_call f lbls_offs st (Mem.find_global st.mem f) lbl 328 331 329 332 | LTL.St_call_ptr lbl -> 330 interpret_call lbls_offs st (dptr st) lbl333 interpret_call (Val.string_of_address (dptr st)) lbls_offs st (dptr st) lbl 331 334 332 335 | LTL.St_condacc (lbl_true, lbl_false) -> … … 359 362 (res, cost_labels) in 360 363 if debug then print_state lbls_offs st ; 364 Printf.printf "%s\n" (Val.string_of_address st.pc); 361 365 match fetch_stmt lbls_offs st with 362 366 | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit -> … … 407 411 match Mem.find_fun_def st.mem ptr with 408 412 | LTL.F_int def -> 409 init_fun_call lbls_offs st ptr def413 init_fun_call main lbls_offs st ptr def 410 414 | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.") 411 415 -
Deliverables/D2.2/8051/src/RTL/RTLConstPropagation.ml
r1584 r1585 38 38 val bind_2 39 39 : Register.t -> Register.t -> t option * t option -> property -> property 40 val find : Register.t -> property -> t option 40 val find_in : Register.t -> property -> t option 41 val find_out : Register.t -> property -> t option 41 42 val find_carry_in : property -> t option 42 43 val equal : property -> property -> bool 43 44 val is_maximal : property -> bool 44 val is_cst : Register.t -> property -> bool 45 val find_cst : Register.t -> property -> int 46 val find_cst_opt : Register.t -> property -> int option 45 val is_cst_in : Register.t -> property -> bool 46 val find_cst_in : Register.t -> property -> int 47 val find_cst_opt_in : Register.t -> property -> int option 48 val is_cst_out : Register.t -> property -> bool 49 val find_cst_out : Register.t -> property -> int 50 val find_cst_opt_out : Register.t -> property -> int option 47 51 val find_cst_carry_in : property -> int option 48 52 … … 56 60 57 61 type property = { 58 regs : t Register.FlexMap.t ; (* no need to have out and in *) 62 in_regs : t Register.FlexMap.t ; 63 out_regs : t Register.FlexMap.t ; 59 64 in_c : t option ; 60 65 out_c : t option … … 62 67 63 68 let bottom : property = 64 { regs = Register.FlexMap.empty; in_c = None; out_c = None } 69 { in_regs = Register.FlexMap.empty; 70 out_regs = Register.FlexMap.empty; 71 in_c = None; out_c = None } 65 72 66 73 let join_t x y = match x, y with … … 72 79 let choose _ = join_t in 73 80 let carry = join_t p.out_c q.out_c in 74 { regs = Register.FlexMap.merge choose p.regs q.regs; 81 let regs = Register.FlexMap.merge choose p.out_regs q.out_regs in 82 { 83 in_regs = regs; 84 out_regs = regs; 75 85 in_c = carry; 76 86 out_c = carry … … 79 89 let bind r t p = 80 90 let regs = match t with 81 | Some v -> Register.FlexMap.add r v p. regs82 | None -> Register.FlexMap.remove r p. regs in83 { p with regs = regs }91 | Some v -> Register.FlexMap.add r v p.out_regs 92 | None -> Register.FlexMap.remove r p.out_regs in 93 { p with out_regs = regs } 84 94 85 95 let bind_carry t p = { p with out_c = t } … … 94 104 bind s u (bind r v p) 95 105 96 let find r p = to_opt_2 Register.FlexMap.find r p.regs 106 let find_in r p = to_opt_2 Register.FlexMap.find r p.in_regs 107 let find_out r p = to_opt_2 Register.FlexMap.find r p.out_regs 97 108 let find_carry_in p = p.in_c 98 109 … … 112 123 equal_t_opt_as_bool p.in_c q.in_c && 113 124 equal_t_opt_as_bool p.out_c q.out_c && 114 Register.FlexMap.equal equal_t p.regs q.regs 125 Register.FlexMap.equal equal_t p.in_regs q.in_regs && 126 Register.FlexMap.equal equal_t p.out_regs q.out_regs 127 115 128 116 129 let is_maximal _ = false 117 130 118 let is_cst r p =131 let is_cst_in r p = 119 132 try 120 match Register.FlexMap.find r p. regs with133 match Register.FlexMap.find r p.in_regs with 121 134 | V _ -> true 122 135 | T -> false … … 124 137 | Not_found -> false 125 138 126 let find_cst r p = 127 match find r p with 139 let is_cst_out r p = 140 try 141 match Register.FlexMap.find r p.out_regs with 142 | V _ -> true 143 | T -> false 144 with 145 | Not_found -> false 146 147 let find_cst_in r p = 148 match find_in r p with 128 149 | Some (V v) -> Val.to_int v 129 150 | _ -> raise Not_found 130 151 131 let find_cst_opt r p = 132 try Some (find_cst r p) with 152 let find_cst_out r p = 153 match find_out r p with 154 | Some (V v) -> Val.to_int v 155 | _ -> raise Not_found 156 157 let find_cst_opt_in r p = 158 try Some (find_cst_in r p) with 159 | Not_found -> None 160 161 let find_cst_opt_out r p = 162 try Some (find_cst_in r p) with 133 163 | Not_found -> None 134 164 … … 150 180 let cst i = L.V (Val.of_int i) 151 181 152 let find_arg a prop = match a with153 | Reg r -> L.find r prop182 let find_arg_in a prop = match a with 183 | Reg r -> L.find_in r prop 154 184 | Imm k -> Some (cst k) 155 185 … … 159 189 (j : Register.t) 160 190 : L.t option = 161 let x = L.find j prop in191 let x = L.find_in j prop in 162 192 match x with 163 193 | Some (L.V v) -> Some (L.V (Eval.op1 op v)) … … 173 203 (b : argument) 174 204 : L.t option * L.t option = 175 let x = find_arg a prop in176 let y = find_arg b prop in205 let x = find_arg_in a prop in 206 let y = find_arg_in b prop in 177 207 let c = L.find_carry_in prop in 178 208 match x, y, c, op with … … 243 273 (b : argument) 244 274 : L.t option * L.t option = 245 let x = find_arg a prop in246 let y = find_arg b prop in275 let x = find_arg_in a prop in 276 let y = find_arg_in b prop in 247 277 match x, y, op with 248 278 | _, Some (L.V v2), I8051.DivuModu when Val.is_false v2 -> … … 285 315 match Label.Map.find lbl graph with 286 316 287 | St_move (r, a, _) -> L.bind r (find_arg a pred_prop) pred_prop317 | St_move (r, a, _) -> L.bind r (find_arg_in a pred_prop) pred_prop 288 318 | St_op1 (op, r, s, _) -> L.bind r (do_the_op1 op pred_prop s) pred_prop 289 319 | St_op2 (op, r, a, b, _) -> … … 317 347 (* now that the info for constants can be gathered, let's put that to use *) 318 348 319 let find_cst_arg prop = function349 let find_cst_arg_in prop = function 320 350 | Imm k -> Some k 321 | Reg r -> L.find_cst_opt r prop351 | Reg r -> L.find_cst_opt_in r prop 322 352 323 353 let arg_from_arg prop a = 324 match find_cst_arg prop a with354 match find_cst_arg_in prop a with 325 355 | Some k -> Imm k 326 356 | None -> a 327 357 358 let move i a prop = 359 match arg_from_arg prop a with 360 | Reg j when i = j -> [] 361 | Imm k when L.find_cst_opt_in i prop = Some k -> [] 362 | a' -> [St_move (i, a', Label.dummy)] 363 328 364 let simpl_imm_op2 op i a b prop l = 329 match find_cst_arg prop a, find_cst_argprop b,365 match find_cst_arg_in prop a, find_cst_arg_in prop b, 330 366 L.find_cst_carry_in prop, op with 331 367 | Some 0, _, _, (I8051.Or | I8051.Xor) … … 336 372 | Some 255, _, Some 1, I8051.Addc 337 373 | Some 255, _, _, I8051.And -> 338 St_move (i, b, l)374 move i b prop 339 375 | _, Some 0, _, (I8051.Or | I8051.Xor) 340 376 | _, Some 0, Some 0, (I8051.Addc | I8051.Sub | I8051.Add) 341 377 | _, Some 255, Some 1, I8051.Addc 342 378 | _, Some 255, _, I8051.And -> 343 St_move (i, a, l)379 move i a prop 344 380 | _, _, Some 0, I8051.Addc -> 345 381 (* does not change time, but maybe helps getting better results 346 382 with liveness analysis *) 347 St_op2 (I8051.Add, i, arg_from_arg prop a, arg_from_arg prop b, l)383 [St_op2 (I8051.Add, i, arg_from_arg prop a, arg_from_arg prop b, l)] 348 384 | _ -> 349 St_op2 (op, i, arg_from_arg prop a, arg_from_arg prop b, l)385 [St_op2 (op, i, arg_from_arg prop a, arg_from_arg prop b, l)] 350 386 351 387 let simpl_imm_opaccs op i j a b prop l = 352 match find_cst_arg prop a, find_cst_argprop b, op with388 match find_cst_arg_in prop a, find_cst_arg_in prop b, op with 353 389 | Some 1, _, I8051.Mul -> 354 [St_move (i, b, l) ; St_move (j, Imm 0, l)]390 move i b prop @ move j (Imm 0) prop 355 391 | _, Some 1, (I8051.Mul | I8051.DivuModu) -> 356 [St_move (i, a, l) ; St_move (j, Imm 0, l)]392 move i a prop @ move j (Imm 0) prop 357 393 | _ -> 358 394 [St_opaccs (op, i, j, arg_from_arg prop a, arg_from_arg prop b, l)] 395 359 396 360 397 (* we transform statements according to the valuation found out by analyze *) … … 369 406 (stmt : statement) : statement list * Label.t list option = 370 407 match stmt with 371 | (St_op1 (_,i,_,l) | St_op2(_,i,_,_,l) | St_move (i, _, l)) 372 when L.is_cst i (valu p) -> 373 ([St_move (i, Imm (L.find_cst i (valu p)), p)], None) 408 | St_move (i, a, l) -> 409 (move i a (valu p), None) 410 | (St_op1 (_,i,_,l) | St_op2(_,i,_,_,l)) 411 when L.is_cst_out i (valu p) -> 412 (move i (Imm (L.find_cst_out i (valu p))) (valu p), None) 374 413 | St_op2 (op, i, a, b, l) -> 375 ( [simpl_imm_op2 op i a b (valu p) l], None)414 (simpl_imm_op2 op i a b (valu p) l, None) 376 415 | St_opaccs (op, i, j, a, b, l) -> 377 416 (simpl_imm_opaccs op i j a b (valu p) l, None) … … 383 422 arg_from_arg (valu p) c, l)], None) 384 423 | St_cond (i, if_true, if_false) as s -> 385 (match L.find_cst_opt i (valu p) with424 (match L.find_cst_opt_in i (valu p) with 386 425 | Some 0 -> ([], Some [if_false]) 387 426 | Some _ -> ([], Some [if_true]) -
Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml
r1584 r1585 294 294 | I8051.Add -> 295 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, [])) 296 begin match destrs_common, srcrs1_common, srcrs2_common with 297 | destr :: destrs, srcr1 :: srcrs1, srcr2 :: srcrs2 -> 298 f_add op destr srcr1 srcr2 :: 299 MiscPottier.map3 (f_add I8051.Addc) destrs srcrs1 srcrs2 300 | [], [], [] -> [] 301 | _ -> assert false 302 end 300 303 | _ -> 301 304 (* we just do the same operation on all *) … … 332 335 (* the next must be an invariant *) 333 336 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 337 (* we pad destrs with itself until we have two times as much 338 registers. The routine should thus handle overflow nicely. *) 339 let all_destrs = MiscPottier.fill destrs (2 * destrs_n) in 338 340 let init = translate_cst (AST.Cst_int 0) destrs :: init in 339 341 (* the registries to hold the temporary results of 8-bit mutliplication *) 340 342 let (def, a) = fresh_reg def in 341 343 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 (* when getting the result, this is what is used (padded as necessary) *) 345 let mul_arg k = [RTL.Reg a ; RTL.Reg b] @ 346 MiscPottier.make (RTL.Imm 0) (2*destrs_n - k - 2) in 347 (* multiplication between the ith byte of srcrs1 and the jth byte of 348 srcrs2 *) 344 349 let mul i j = 345 let s1i, s2j = List.nth fresh_srcrs1 i, List.nth fresh_srcrs2 i in 350 let s1i, s2j = List.nth fresh_srcrs1 i, List.nth fresh_srcrs2 j in 351 (* the position in the result where the resulting bytes must be added *) 346 352 let k = i + j in 347 let dloc = MiscPottier.sublist all_destrs k ( k+3) in353 let dloc = MiscPottier.sublist all_destrs k (2*destrs_n) in 348 354 let dloc_arg = List.map (fun r -> RTL.Reg r) dloc in 355 (* we add until the end to propagate the carry bit. 356 At the beginning this will be useless, but we rely on 357 RTL's constant propagation and later dead register elimination 358 to amend that *) 349 359 [ adds_graph [RTL.St_opaccs (I8051.Mul, a, b, s1i, s2j, start_lbl)] ; 350 translate_op I8051.Add dloc dloc_arg mul_arg] in360 translate_op I8051.Add dloc dloc_arg (mul_arg k)] in 351 361 let insts = List.flatten (List.flatten 352 362 (MiscPottier.makei (fun i -> -
Deliverables/D2.2/8051/src/checker.ml
r1542 r1585 5 5 Misc.ListExt.assoc_diff occs_trace1 occs_trace2 6 6 in 7 let check_trace (_, (_, trace1)) (_, (_, trace2)) = 7 let check_trace (_, (res1, trace1)) (_, (res2, trace2)) = 8 IntValue.Int32.eq res1 res2 && 8 9 compare_trace trace1 trace2 = [] 9 10 in … … 28 29 let diff = compare_trace trace1 trace2 in 29 30 Error.global_error "during trace comparison" 30 (Printf.sprintf 31 "The traces of two intermediate programs differ:\n%s" 32 (print_trace lang1 lang2 diff)) 31 (Printf.sprintf "%s%s" 32 (if res1 != res2 then 33 Printf.sprintf 34 "The results of two intermediate programs differ:\n 35 in %s it was %d, in %s it was %d\n" 36 lang1 37 (IntValue.Int32.to_int res1) 38 lang2 39 (IntValue.Int32.to_int res2) else "") 40 (Printf.sprintf "The traces of the two intermediate programs:\n%s" 41 (print_trace lang1 lang2 diff))) -
Deliverables/D2.2/8051/src/common/costLabel.ml
r1542 r1585 42 42 let curr_ind = function 43 43 | hd :: _ -> hd 44 | _ -> invalid_arg " non-empty indexing stack"44 | _ -> invalid_arg "empty indexing stack" 45 45 46 46 let enter_loop inds = enter_loop_single (curr_ind inds) … … 56 56 let forget_const_ind = function 57 57 | _ :: inds -> inds 58 | _ -> invalid_arg " non-empty indexing stack"58 | _ -> invalid_arg "empty indexing stack" 59 59 60 60 let sexpr_of i l = -
Deliverables/D2.2/8051/src/common/costLabel.mli
r1542 r1585 31 31 32 32 (** This is equivalent to [List.hd], but raises 33 [Invalid_argument " non-empty indexing stack"] if argument is empty *)33 [Invalid_argument "empty indexing stack"] if argument is empty *) 34 34 val curr_const_ind : const_indexing list -> const_indexing 35 35 … … 46 46 (** [continue_loop inds n] is used to update the indexing stack [inds] when 47 47 one is continuing a loop indexed by [n]. 48 @raise [Invalid_argument " non-empty indexing stack"] if [inds] is empty.48 @raise [Invalid_argument "empty indexing stack"] if [inds] is empty. 49 49 @raise [Invalid_argument "uninitialized loop index"] if the head of 50 50 [inds] has no value for [index]. *) … … 61 61 62 62 (** [forget_const_ind inds] pops and discards the top constant indexing from the 63 stack [inds]. Raises [Invalid_argument " non-empty indexing stack"] if63 stack [inds]. Raises [Invalid_argument "empty indexing stack"] if 64 64 [inds] is empty. *) 65 65 val forget_const_ind : const_indexing list -> const_indexing list -
Deliverables/D2.2/8051/src/utilities/miscPottier.ml
r1584 r1585 4 4 List.map f' (List.combine (List.combine al bl) cl) 5 5 6 let 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) 6 let rec fold3_right f al bl cl d = match al, bl, cl with 7 | a :: al, b :: bl, c :: cl -> 8 f a b c (fold3_right f al bl cl d) 9 | [], [], [] -> d 10 | _ -> invalid_arg "fold3_right: list lengths do not match" 11 12 let rec fold3_left f a bl cl dl = match bl, cl, dl with 13 | b :: bl, c :: cl, d :: dl -> 14 fold3_left f (f a b c d) bl cl dl 15 | [], [], [] -> a 16 | _ -> invalid_arg "fold3_left: list lengths do not match" 9 17 10 18 let rec max_list = function -
Deliverables/D2.2/8051/src/utilities/miscPottier.mli
r1584 r1585 10 10 size. *) 11 11 val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list 12 val fold3_left : ('a -> 'b -> 'c -> 'd -> 'a) -> 13 'a -> 'b list -> 'c list -> 'd list -> 'a 12 14 val fold3_right : ('a -> 'b -> 'c -> 'd -> 'd) -> 13 15 'a list -> 'b list -> 'c list -> 'd -> 'd
Note: See TracChangeset
for help on using the changeset viewer.