Changeset 818 for Deliverables/D2.2/8051
- Timestamp:
- May 19, 2011, 4:03:04 PM (10 years ago)
- Location:
- Deliverables/D2.2/8051
- Files:
-
- 2 added
- 78 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/README
r619 r818 34 34 -------------- 35 35 36 - ocaml (>= 3.1 1)36 - ocaml (>= 3.13) 37 37 - menhir (>= 20090505) 38 38 - CIL (included in the distribution) -
Deliverables/D2.2/8051/myocamlbuild_config.ml
r742 r818 1 let parser_lib = "/home/ dpm/Projects/Cerco/Deliverables/D2.2/8051/lib"1 let parser_lib = "/home/ayache/Downloads/Bol/Deliverables/D2.2/8051/lib" -
Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml
r743 r818 1935 1935 let status = serial_port_output status out_cont in 1936 1936 let status = interrupts status in 1937 let status = { status with previous_p1_val = get_bit status.p3 4; 1938 previous_p3_val = get_bit status.p3 5 } in 1939 status 1937 { status with previous_p1_val = get_bit status.p3 4; 1938 previous_p3_val = get_bit status.p3 5 } 1940 1939 ;; 1941 1940 … … 1969 1968 ;; 1970 1969 1970 1971 1971 let load_program p = 1972 1972 let st = load p.ASM.code initialize in … … 1982 1982 1983 1983 let result st = 1984 let i = BitVectors.int_of_vect st.dpl in 1985 IntValue.Int8.of_int i 1986 1987 let interpret print_result p = 1988 if print_result then Printf.printf "8051: %!" ; 1984 let dpl = st.dpl in 1985 let dpr = st.dph in 1986 let addr i = BitVectors.vect_of_int i `Seven in 1987 let get_ireg i = Physical.Byte7Map.find (addr i) st.low_internal_ram in 1988 let r00 = get_ireg 0 in 1989 let r01 = get_ireg 1 in 1990 let is = [dpl ; dpr ; r00 ; r01] in 1991 let f i = IntValue.Int32.of_int (BitVectors.int_of_vect i) in 1992 IntValue.Int32.merge (List.map f is) 1993 1994 let interpret debug p = 1995 Printf.printf "*** 8051 interpret ***\n%!" ; 1989 1996 if p.ASM.has_main then 1990 1997 let st = load_program p in … … 1993 2000 let st = execute callback st in 1994 2001 let res = result st in 1995 if print_resultthen1996 Printf.printf " %s\n%!" (IntValue.Int8.to_string res) ;2002 if debug then 2003 Printf.printf "Result = %s\n%!" (IntValue.Int32.to_string res) ; 1997 2004 (res, List.rev !trace) 1998 else (IntValue.Int 8.zero, [])2005 else (IntValue.Int32.zero, []) -
Deliverables/D2.2/8051/src/ASM/I8051.ml
r740 r818 6 6 type opaccs = 7 7 | Mul 8 | Divu 9 | Modu 8 | DivuModu 10 9 11 10 type op1 = … … 23 22 let print_opaccs = function 24 23 | Mul -> "mul" 25 | Divu -> "divu" 26 | Modu -> "modu" 24 | DivuModu -> "divu" 27 25 28 26 let print_op1 = function … … 41 39 module Eval (Val : Value.S) = struct 42 40 43 let opaccs = function 44 | Mul -> Val.mul 45 | Divu -> Val.divu 46 | Modu -> Val.modulou 41 let eval_int_mul size i1 i2 = 42 let module Int = IntValue.Make (struct let size = 2 * size end) in 43 match Int.break (Int.mul i1 i2) 2 with 44 | res1 :: res2 :: _ -> (Val.of_int_repr res1, Val.of_int_repr res2) 45 | _ -> assert false (* should be impossible *) 46 47 let eval_mul v1 v2 = 48 if Val.is_int v1 && Val.is_int v2 then 49 eval_int_mul Val.int_size (Val.to_int_repr v1) (Val.to_int_repr v2) 50 else (Val.undef, Val.undef) 51 52 let opaccs op v1 v2 = match op with 53 | Mul -> eval_mul v1 v2 54 | DivuModu -> (Val.divu v1 v2, Val.modulou v1 v2) 47 55 48 56 let op1 = function … … 152 160 | _ -> assert false (* impossible *) 153 161 154 let sst = r03 155 let st0 = r04 156 let st1 = r05 162 let sst = r10 163 let st0 = r02 164 let st1 = r03 165 let st2 = r04 166 let st3 = r05 167 let sts = [st0 ; st1 ; st2 ; st3] 157 168 let spl = r06 158 169 let sph = r07 170 let rets = [dpl ; dph ; r00 ; r01] 171 172 let isp_addr = 129 173 let isp_init = 47 159 174 160 175 let set_of_list rl = List.fold_right RegisterSet.add rl RegisterSet.empty … … 169 184 170 185 let forbidden = 171 set_of_list [(* a ; b ; dpl ; dph ; *) spl ; sph ; st0 ; st1 ; sst] 186 set_of_list 187 [a ; b ; dpl ; dph ; spl ; sph ; st0 ; st1 ; st2 ; st3 ; sst] 172 188 173 189 let parameters = -
Deliverables/D2.2/8051/src/ASM/I8051.mli
r740 r818 4 4 type opaccs = 5 5 | Mul 6 | Divu 7 | Modu 6 | DivuModu 8 7 9 8 type op1 = … … 24 23 25 24 module Eval (Val : Value.S) : sig 26 val opaccs : opaccs -> Val.t -> Val.t -> Val.t 25 val opaccs : opaccs -> Val.t -> Val.t -> 26 (Val.t (* first result (ACC) *) * 27 Val.t (* second result (BACC) *)) 27 28 val op1 : op1 -> Val.t -> Val.t 28 29 val op2 : Val.t (* carry *) -> op2 -> Val.t -> Val.t -> … … 47 48 val st0 : register 48 49 val st1 : register 50 val st2 : register 51 val st3 : register 52 val sts : register list 53 val rets : register list 49 54 val sst : register 50 55 val carry : register (* only used for the liveness analysis *) 56 57 val isp_addr : int 58 val isp_init : int 51 59 52 60 val registers : RegisterSet.t -
Deliverables/D2.2/8051/src/ASM/Pretty.ml
r645 r818 100 100 let f (s, pc) _ = 101 101 let (inst, new_pc, cost) = ASMInterpret.fetch mem pc in 102 (Printf.sprintf "%s% 6 s%- 18s ;; %d %s\n"102 (Printf.sprintf "%s% 6X: %- 18s ;; %d %s\n" 103 103 s 104 ( (string_of_int (BitVectors.int_of_vect pc)) ^ ":")104 (BitVectors.int_of_vect pc) 105 105 (pp_instruction inst) 106 106 cost -
Deliverables/D2.2/8051/src/ERTL/ERTL.mli
r740 r818 104 104 105 105 (* Apply a binary operation that will later be translated in an operation on 106 the accumulators. Parameters are the operation, the destination register, 107 the source registers, and the label of the next statement. *) 108 | St_opaccs of I8051.opaccs * Register.t * Register.t * Register.t * Label.t 106 the accumulators, keeping only the result in ACC. Parameters are the 107 operation, the destination register, the source registers, and the label of 108 the next statement. *) 109 | St_opaccsA of I8051.opaccs * Register.t * Register.t * Register.t * Label.t 110 111 (* Apply a binary operation that will later be translated in an operation on 112 the accumulators, keeping only the result in BACC. Parameters are the 113 operation, the destination register, the source registers, and the label of 114 the next statement. *) 115 | St_opaccsB of I8051.opaccs * Register.t * Register.t * Register.t * Label.t 109 116 110 117 (* Apply an unary operation. Parameters are the operation, the destination … … 119 126 statement. *) 120 127 | St_clear_carry of Label.t 128 129 (* Set the carry flag to 1. Parameter is the label of the next statement. *) 130 | St_set_carry of Label.t 121 131 122 132 (* Load from external memory. Parameters are the destination register, the … … 152 162 the label to go to when the value is not 0, and the label to go to when the 153 163 value is 0. *) 154 | St_cond accof Register.t * Label.t * Label.t164 | St_cond of Register.t * Label.t * Label.t 155 165 156 166 (* Transfer control to the address stored in the return address registers. *) -
Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml
r740 r818 197 197 198 198 let interpret_external mem f args = match InterpretExternal.t mem f args with 199 | (mem', InterpretExternal.V v ) -> (mem', [v])199 | (mem', InterpretExternal.V vs) -> (mem', vs) 200 200 | (mem', InterpretExternal.A addr) -> (mem', addr) 201 201 202 let fetch_external_args st = 203 (* TODO: this is bad when parameters are the empty list. *) 204 [get_reg (Hdw (List.hd I8051.parameters)) st] 205 206 let set_result st = function 207 | [] -> assert false (* should be impossible: at least one value returned *) 208 | [v] -> add_reg (Hdw I8051.dpl) v st 209 | v1 :: v2 :: _ -> 210 let st = add_reg (Hdw I8051.dpl) v1 st in 211 add_reg (Hdw I8051.dph) v2 st 202 let fetch_external_args f st = 203 let size = Mem.size_of_quantity (Primitive.args_byte_size f) in 204 let params = MiscPottier.prefix size I8051.parameters in 205 List.map (fun r -> get_reg (Hdw r) st) params 206 207 let set_result st vs = 208 let f st (r, v) = add_reg (Hdw r) v st in 209 List.fold_left f st (MiscPottier.combine I8051.rets vs) 212 210 213 211 let interpret_external_call st f next_pc = 214 let args = fetch_external_args st in212 let args = fetch_external_args f st in 215 213 let (mem, vs) = interpret_external st.mem f args in 216 214 let st = change_mem st mem in … … 316 314 next_pc st lbl 317 315 318 | ERTL.St_opaccs (opaccs, destr, srcr1, srcr2, lbl) -> 319 let v = 316 | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, lbl) -> 317 let (v, _) = 318 Eval.opaccs opaccs 319 (get_reg (Psd srcr1) st) 320 (get_reg (Psd srcr2) st) in 321 let st = add_reg (Psd destr) v st in 322 next_pc st lbl 323 324 | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, lbl) -> 325 let (_, v) = 320 326 Eval.opaccs opaccs 321 327 (get_reg (Psd srcr1) st) … … 342 348 next_pc st lbl 343 349 350 | ERTL.St_set_carry lbl -> 351 let st = change_carry st (Val.of_int 1) in 352 next_pc st lbl 353 344 354 | ERTL.St_load (destr, addr1, addr2, lbl) -> 345 355 let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in … … 357 367 interpret_call lbls_offs st f lbl 358 368 359 | ERTL.St_cond acc(srcr, lbl_true, lbl_false) ->369 | ERTL.St_cond (srcr, lbl_true, lbl_false) -> 360 370 let v = get_reg (Psd srcr) st in 361 371 let lbl = … … 390 400 Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ; 391 401 Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ; 402 Printf.printf "Carry: %s%!" (Val.to_string st.carry) ; 392 403 print_lenv st.lenv ; 393 404 print_renv st.renv ; … … 396 407 397 408 let compute_result st ret_regs = 398 try 399 let v = get_reg (Psd (List.hd ret_regs)) st in 400 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 401 else IntValue.Int8.zero 402 with Not_found -> IntValue.Int8.zero 409 let vs = List.map (fun r -> get_reg (Psd r) st) ret_regs in 410 let f res v = res && (Val.is_int v) in 411 let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in 412 if is_int vs then 413 let chunks = 414 List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in 415 IntValue.Int32.merge chunks 416 else IntValue.Int32.zero 403 417 404 418 let rec iter_small_step debug lbls_offs st = 419 let print_and_return_result (res, cost_labels) = 420 if debug then Printf.printf "Result = %s\n%!" 421 (IntValue.Int32.to_string res) ; 422 (res, cost_labels) in 405 423 if debug then print_state lbls_offs st ; 406 424 match fetch_stmt lbls_offs st with 407 425 | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit -> 408 (compute_result st ret_regs, List.rev st.trace)426 print_and_return_result (compute_result st ret_regs, List.rev st.trace) 409 427 | stmt -> 410 428 let st' = interpret_stmt lbls_offs st stmt in … … 414 432 let add_global_vars = 415 433 List.fold_left 416 (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])434 (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None) 417 435 418 436 let add_fun_defs = … … 472 490 473 491 let interpret debug p = 474 if debug then Printf.printf "*** ERTL ***\n\n%!" ;492 Printf.printf "*** ERTL interpret ***\n%!" ; 475 493 match p.ERTL.main with 476 | None -> (IntValue.Int 8.zero, [])494 | None -> (IntValue.Int32.zero, []) 477 495 | Some main -> 478 496 let lbls_offs = labels_offsets p in -
Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml
r486 r818 72 72 Printf.sprintf "move %s, %s --> %s" 73 73 (Register.print dstr) (Register.print srcr) lbl 74 | ERTL.St_opaccs (opaccs, dstr, srcr1, srcr2, lbl) -> 75 Printf.sprintf "%s %s, %s, %s --> %s" 74 | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl) -> 75 Printf.sprintf "%sA %s, %s, %s --> %s" 76 (I8051.print_opaccs opaccs) 77 (Register.print dstr) 78 (Register.print srcr1) 79 (Register.print srcr2) 80 lbl 81 | ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, lbl) -> 82 Printf.sprintf "%sB %s, %s, %s --> %s" 76 83 (I8051.print_opaccs opaccs) 77 84 (Register.print dstr) … … 94 101 | ERTL.St_clear_carry lbl -> 95 102 Printf.sprintf "clear CARRY --> %s" lbl 103 | ERTL.St_set_carry lbl -> 104 Printf.sprintf "set CARRY --> %s" lbl 96 105 | ERTL.St_load (dstr, addr1, addr2, lbl) -> 97 106 Printf.sprintf "load %s, (%s, %s) --> %s" … … 127 136 (print_args args) 128 137 *) 129 | ERTL.St_cond acc(srcr, lbl_true, lbl_false) ->138 | ERTL.St_cond (srcr, lbl_true, lbl_false) -> 130 139 Printf.sprintf "branch %s <> 0 --> %s, %s" 131 140 (Register.print srcr) lbl_true lbl_false -
Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml
r740 r818 214 214 move (lookup r1) (lookup r2) l 215 215 216 | ERTL.St_opaccs (I8051.Modu, destr, srcr1, srcr2, l) -> 217 let (hdw, l) = write destr l in 218 let l = generate (LTL.St_from_acc (hdw, l)) in 219 let l = generate (LTL.St_to_acc (I8051.b, l)) in 220 let l = generate (LTL.St_opaccs (I8051.Divu, l)) in 221 let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in 222 let l = generate (LTL.St_from_acc (I8051.b, l)) in 223 let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in 224 LTL.St_skip l 225 226 | ERTL.St_opaccs (opaccs, destr, srcr1, srcr2, l) -> 216 | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) -> 227 217 let (hdw, l) = write destr l in 228 218 let l = generate (LTL.St_from_acc (hdw, l)) in … … 233 223 LTL.St_skip l 234 224 225 | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) -> 226 let (hdw, l) = write destr l in 227 let l = generate (LTL.St_from_acc (hdw, l)) in 228 let l = generate (LTL.St_to_acc (I8051.b, l)) in 229 let l = generate (LTL.St_opaccs (opaccs, l)) in 230 let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in 231 let l = generate (LTL.St_from_acc (I8051.b, l)) in 232 let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in 233 LTL.St_skip l 234 235 235 | ERTL.St_op1 (op1, destr, srcr, l) -> 236 236 let (hdw, l) = write destr l in … … 251 251 | ERTL.St_clear_carry l -> 252 252 LTL.St_clear_carry l 253 254 | ERTL.St_set_carry l -> 255 LTL.St_set_carry l 253 256 254 257 | ERTL.St_load (destr, addr1, addr2, l) -> … … 280 283 LTL.St_call_id (f, l) 281 284 282 | ERTL.St_cond acc(srcr, lbl_true, lbl_false) ->285 | ERTL.St_cond (srcr, lbl_true, lbl_false) -> 283 286 let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in 284 287 let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in -
Deliverables/D2.2/8051/src/ERTL/liveness.ml
r486 r818 30 30 | St_int (_, _, l) 31 31 | St_move (_, _, l) 32 | St_opaccs (_, _, _, _, l) 32 | St_opaccsA (_, _, _, _, l) 33 | St_opaccsB (_, _, _, _, l) 33 34 | St_op1 (_, _, _, l) 34 35 | St_op2 (_, _, _, _, l) 35 36 | St_clear_carry l 37 | St_set_carry l 36 38 | St_load (_, _, _, l) 37 39 | St_store (_, _, _, l) 38 40 | St_call_id (_, _, l) -> 39 41 Label.Set.singleton l 40 | St_cond acc(_, l1, l2) ->42 | St_cond (_, l1, l2) -> 41 43 Label.Set.add l1 (Label.Set.singleton l2) 42 44 … … 115 117 | St_cost _ 116 118 | St_push _ 117 | St_clear_carry _118 119 | St_store _ 119 | St_cond acc_120 | St_cond _ 120 121 | St_return _ -> 121 122 L.bottom 123 | St_clear_carry _ 124 | St_set_carry _ -> 125 Register.Set.empty, I8051.RegisterSet.singleton I8051.carry 122 126 | St_op2 (I8051.Add, r, _, _, _) 123 127 | St_op2 (I8051.Addc, r, _, _, _) 124 128 | St_op2 (I8051.Sub, r, _, _, _) -> 125 129 L.join (L.hsingleton I8051.carry) (L.psingleton r) 126 | St_op1 (I8051.Inc, r, _, _) -> 127 L.join (L.hsingleton I8051.carry) (L.psingleton r) 130 | St_op1 (I8051.Inc, r, _, _) 128 131 | St_get_hdw (r, _, _) 129 132 | St_framesize (r, _) … … 133 136 | St_addrL (r, _, _) 134 137 | St_move (r, _, _) 135 | St_opaccs (_, r, _, _, _) 138 | St_opaccsA (_, r, _, _, _) 139 | St_opaccsB (_, r, _, _, _) 136 140 | St_op1 (_, r, _, _) 137 141 | St_op2 (_, r, _, _, _) … … 153 157 (* This is the set of variables used at (read by) a statement. *) 154 158 155 let dptr = 156 I8051.RegisterSet.add I8051.dph (I8051.RegisterSet.singleton I8051.dpl) 159 let set_of_list = 160 let f set r = I8051.RegisterSet.add r set in 161 List.fold_left f I8051.RegisterSet.empty 162 163 let ret_regs = set_of_list I8051.rets 157 164 158 165 let used (stmt : statement) : L.t = … … 166 173 | St_addrL _ 167 174 | St_int _ 168 | St_clear_carry _ -> 175 | St_clear_carry _ 176 | St_set_carry _ -> 169 177 L.bottom 170 178 | St_call_id (_, nparams, _) -> … … 179 187 | St_move (_, r, _) 180 188 | St_op1 (_, _, r, _) 181 | St_cond acc(r, _, _) ->189 | St_cond (r, _, _) -> 182 190 L.psingleton r 183 191 | St_op2 (I8051.Addc, _, r1, r2, _) -> 184 192 L.join (L.join (L.psingleton r1) (L.psingleton r2)) 185 193 (L.hsingleton I8051.carry) 186 | St_opaccs (_, _, r1, r2, _) 194 | St_opaccsA (_, _, r1, r2, _) 195 | St_opaccsB (_, _, r1, r2, _) 187 196 | St_op2 (_, _, r1, r2, _) 188 197 | St_load (_, r1, r2, _) -> … … 194 203 L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph) 195 204 | St_return _ -> 196 Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved dptr205 Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs 197 206 198 207 (* A statement is considered pure if it has no side effect, that is, if … … 218 227 | St_push _ 219 228 | St_clear_carry _ 229 | St_set_carry _ 220 230 | St_store _ 221 231 | St_call_id _ 222 | St_cond acc_232 | St_cond _ 223 233 | St_return _ -> 224 234 None … … 229 239 | St_addrL (r, _, l) 230 240 | St_move (r, _, l) 231 | St_opaccs (_, r, _, _, l) 241 | St_opaccsA (_, r, _, _, l) 242 | St_opaccsB (_, r, _, _, l) 232 243 | St_op1 (_, r, _, l) 233 244 | St_op2 (_, r, _, _, l) -
Deliverables/D2.2/8051/src/ERTL/uses.ml
r486 r818 24 24 | St_delframe _ 25 25 | St_clear_carry _ 26 | St_set_carry _ 26 27 | St_call_id _ 27 28 | St_return _ -> … … 35 36 | St_addrH (r, _, _) 36 37 | St_addrL (r, _, _) 37 | St_cond acc(r, _, _) ->38 | St_cond (r, _, _) -> 38 39 count r uses 39 40 | St_move (r1, r2, _) 40 41 | St_op1 (_, r1, r2, _) -> 41 42 count r1 (count r2 uses) 42 | St_opaccs (_, r1, r2, r3, _) 43 | St_opaccsA (_, r1, r2, r3, _) 44 | St_opaccsB (_, r1, r2, r3, _) 43 45 | St_op2 (_, r1, r2, r3, _) 44 46 | St_load (r1, r2, r3, _) -
Deliverables/D2.2/8051/src/LIN/LIN.mli
r486 r818 54 54 | St_clear_carry 55 55 56 (* Set the carry flag to 1. *) 57 | St_set_carry 58 56 59 (* Load from external memory (address in DPTR) to the accumulator. *) 57 60 | St_load -
Deliverables/D2.2/8051/src/LIN/LINInterpret.ml
r740 r818 148 148 149 149 let interpret_external mem f args = match InterpretExternal.t mem f args with 150 | (mem', InterpretExternal.V v ) -> (mem', [v])150 | (mem', InterpretExternal.V vs) -> (mem', vs) 151 151 | (mem', InterpretExternal.A addr) -> (mem', addr) 152 152 153 let fetch_external_args st = 154 (* TODO: this is bad when parameters are the empty list. *) 155 [get_reg (List.hd I8051.parameters) st] 156 157 let set_result st = function 158 | [] -> assert false (* should be impossible: at least one value returned *) 159 | [v] -> add_reg I8051.dpl v st 160 | v1 :: v2 :: _ -> 161 let st = add_reg I8051.dpl v1 st in 162 add_reg I8051.dph v2 st 153 let fetch_external_args f st = 154 let size = Mem.size_of_quantity (Primitive.args_byte_size f) in 155 let params = MiscPottier.prefix size I8051.parameters in 156 List.map (fun r -> get_reg r st) params 157 158 let set_result st vs = 159 let f st (r, v) = add_reg r v st in 160 List.fold_left f st (MiscPottier.combine I8051.rets vs) 163 161 164 162 let interpret_external_call st f = 165 let args = fetch_external_args st in163 let args = fetch_external_args f st in 166 164 let (mem, vs) = interpret_external st.mem f args in 167 165 let st = change_mem st mem in … … 230 228 231 229 | LIN.St_opaccs opaccs -> 232 let v=230 let (a, b) = 233 231 Eval.opaccs opaccs 234 232 (get_reg I8051.a st) 235 233 (get_reg I8051.b st) in 236 let st = add_reg I8051.a v st in 234 let st = add_reg I8051.a a st in 235 let st = add_reg I8051.b b st in 237 236 next_pc st 238 237 … … 255 254 next_pc st 256 255 256 | LIN.St_set_carry -> 257 let st = change_carry st (Val.of_int 1) in 258 next_pc st 259 257 260 | LIN.St_load -> 258 261 let addr = dptr st in … … 282 285 283 286 let compute_result st = 284 let v = get_reg I8051.dpl st in 285 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 286 else IntValue.Int8.zero 287 let vs = List.map (fun r -> get_reg r st) I8051.rets in 288 let f res v = res && (Val.is_int v) in 289 let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in 290 if is_int vs then 291 let chunks = 292 List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in 293 IntValue.Int32.merge chunks 294 else IntValue.Int32.zero 287 295 288 296 let rec iter_small_step debug st = 297 let print_and_return_result (res, cost_labels) = 298 if debug then Printf.printf "Result = %s\n%!" 299 (IntValue.Int32.to_string res) ; 300 (res, cost_labels) in 289 301 if debug then print_state st ; 290 302 match fetch_stmt st with 291 303 | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit -> 292 (compute_result st, List.rev st.trace)304 print_and_return_result (compute_result st, List.rev st.trace) 293 305 | stmt -> 294 306 let st' = interpret_stmt st stmt in … … 298 310 let add_global_vars = 299 311 List.fold_left 300 (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])312 (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None) 301 313 302 314 let add_fun_defs = … … 354 366 355 367 let interpret debug p = 356 if debug then Printf.printf "*** LIN ***\n\n%!" ;368 Printf.printf "*** LIN interpret ***\n%!" ; 357 369 match p.LIN.main with 358 | None -> (IntValue.Int 8.zero, [])370 | None -> (IntValue.Int32.zero, []) 359 371 | Some main -> 360 372 let st = empty_state in -
Deliverables/D2.2/8051/src/LIN/LINPrinter.ml
r486 r818 48 48 (I8051.print_op2 op2) print_a (print_reg srcr) 49 49 | LIN.St_clear_carry -> "clear CARRY" 50 | LIN.St_set_carry -> "set CARRY" 50 51 | LIN.St_load -> 51 52 Printf.sprintf "movex %s, @DPTR" print_a -
Deliverables/D2.2/8051/src/LIN/LINPrinter.mli
r486 r818 2 2 (** This module provides a function to print [LIN] programs. *) 3 3 4 val print_statement : LIN.statement -> string 5 4 6 val print_program: LIN.program -> string -
Deliverables/D2.2/8051/src/LIN/LINToASM.ml
r741 r818 1 1 2 2 (** This module translates a [LIN] program into a [ASM] program. *) 3 4 5 let error_prefix = "LIN to ASM" 6 let error s = Error.global_error error_prefix s 3 7 4 8 … … 52 56 | LIN.St_push -> 53 57 [`PUSH acc_addr] 58 | LIN.St_addr x when List.mem_assoc x glbls_addr -> 59 [`MOV (`U4 (`DPTR, data16_of_int (List.assoc x glbls_addr)))] 54 60 | LIN.St_addr x -> 55 [`MOV (`U4 (`DPTR, data16_of_int (List.assoc x glbls_addr)))]61 error ("unknown global " ^ x ^ ".") 56 62 | LIN.St_from_acc r -> 57 63 [`MOV (`U3 (I8051.reg_addr r, `A))] … … 60 66 | LIN.St_opaccs I8051.Mul -> 61 67 [`MUL (`A, `B)] 62 | LIN.St_opaccs I8051.Divu ->68 | LIN.St_opaccs I8051.DivuModu -> 63 69 [`DIV (`A, `B)] 64 | LIN.St_opaccs I8051.Modu ->65 assert false (* Should have been translated before. *)66 70 | LIN.St_op1 I8051.Cmpl -> 67 71 [`CPL `A] … … 82 86 | LIN.St_clear_carry -> 83 87 [`CLR `C] 88 | LIN.St_set_carry -> 89 [`SETB `C] 84 90 | LIN.St_load -> 85 91 [`MOVX (`U1 (`A, `EXT_IND_DPTR))] … … 99 105 let translate_fun_def glbls_addr (id, def) = match def with 100 106 | LIN.F_int code -> (`Label id) :: (translate_code glbls_addr code) 101 | _ -> [] 107 | LIN.F_ext ext -> 108 error ("potential call to unsupported external " ^ ext.AST.ef_tag ^ ".") 102 109 103 110 let translate_functs glbls_addr exit_label main functs = 104 111 let preamble = match main with 105 112 | None -> [] 106 | Some main -> [`Call main ; `Label exit_label ; `Jmp exit_label] in 113 | Some main -> 114 [`MOV (`U3 (`DIRECT (byte_of_int I8051.isp_addr), 115 data_of_int I8051.isp_init)) ; 116 `Call main ; 117 `Label exit_label ; `Jmp exit_label] in 107 118 preamble @ 108 119 (List.flatten (List.map (translate_fun_def glbls_addr) functs)) 109 120 110 121 -
Deliverables/D2.2/8051/src/LTL/LTL.mli
r486 r818 60 60 | St_clear_carry of Label.t 61 61 62 (* Set the carry flag to 1. Parameter is the label of the next statement. *) 63 | St_set_carry of Label.t 64 62 65 (* Load from external memory (address in DPTR) to the accumulator. Parameter 63 66 is the label of the next statement. *) -
Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml
r740 r818 177 177 178 178 let interpret_external mem f args = match InterpretExternal.t mem f args with 179 | (mem', InterpretExternal.V v ) -> (mem', [v])179 | (mem', InterpretExternal.V vs) -> (mem', vs) 180 180 | (mem', InterpretExternal.A addr) -> (mem', addr) 181 181 182 let fetch_external_args st = 183 (* TODO: this is bad when parameters are the empty list. *) 184 [get_reg (List.hd I8051.parameters) st] 185 186 let set_result st = function 187 | [] -> assert false (* should be impossible: at least one value returned *) 188 | [v] -> add_reg I8051.dpl v st 189 | v1 :: v2 :: _ -> 190 let st = add_reg I8051.dpl v1 st in 191 add_reg I8051.dph v2 st 182 let fetch_external_args f st = 183 let size = Mem.size_of_quantity (Primitive.args_byte_size f) in 184 let params = MiscPottier.prefix size I8051.parameters in 185 List.map (fun r -> get_reg r st) params 186 187 let set_result st vs = 188 let f st (r, v) = add_reg r v st in 189 List.fold_left f st (MiscPottier.combine I8051.rets vs) 192 190 193 191 let interpret_external_call st f next_pc = 194 let args = fetch_external_args st in192 let args = fetch_external_args f st in 195 193 let (mem, vs) = interpret_external st.mem f args in 196 194 let st = change_mem st mem in … … 262 260 263 261 | LTL.St_opaccs (opaccs, lbl) -> 264 let v=262 let (a, b) = 265 263 Eval.opaccs opaccs 266 264 (get_reg I8051.a st) 267 265 (get_reg I8051.b st) in 268 let st = add_reg I8051.a v st in 266 let st = add_reg I8051.a a st in 267 let st = add_reg I8051.b b st in 269 268 next_pc st lbl 270 269 … … 287 286 next_pc st lbl 288 287 288 | LTL.St_set_carry lbl -> 289 let st = change_carry st (Val.of_int 1) in 290 next_pc st lbl 291 289 292 | LTL.St_load lbl -> 290 293 let addr = dptr st in … … 316 319 317 320 let compute_result st = 318 let v = get_reg I8051.dpl st in 319 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 320 else IntValue.Int8.zero 321 let vs = List.map (fun r -> get_reg r st) I8051.rets in 322 let f res v = res && (Val.is_int v) in 323 let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in 324 if is_int vs then 325 let chunks = 326 List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in 327 IntValue.Int32.merge chunks 328 else IntValue.Int32.zero 321 329 322 330 let rec iter_small_step debug lbls_offs st = 331 let print_and_return_result (res, cost_labels) = 332 if debug then Printf.printf "Result = %s\n%!" 333 (IntValue.Int32.to_string res) ; 334 (res, cost_labels) in 323 335 if debug then print_state lbls_offs st ; 324 336 match fetch_stmt lbls_offs st with 325 337 | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit -> 326 (compute_result st, List.rev st.trace)338 print_and_return_result (compute_result st, List.rev st.trace) 327 339 | stmt -> 328 340 let st' = interpret_stmt lbls_offs st stmt in … … 332 344 let add_global_vars = 333 345 List.fold_left 334 (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])346 (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None) 335 347 336 348 let add_fun_defs = … … 390 402 391 403 let interpret debug p = 392 if debug then Printf.printf "*** LTL ***\n\n%!" ;404 Printf.printf "*** LTL interpret ***\n%!" ; 393 405 match p.LTL.main with 394 406 | None -> (IntValue.Int8.zero, []) -
Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml
r486 r818 48 48 | LTL.St_clear_carry lbl -> 49 49 Printf.sprintf "clear CARRY --> %s" lbl 50 | LTL.St_set_carry lbl -> 51 Printf.sprintf "set CARRY --> %s" lbl 50 52 | LTL.St_load lbl -> 51 53 Printf.sprintf "movex %s, @DPTR --> %s" print_a lbl -
Deliverables/D2.2/8051/src/LTL/LTLToLIN.ml
r486 r818 32 32 | LTL.St_clear_carry _ -> 33 33 LIN.St_clear_carry 34 | LTL.St_set_carry _ -> 35 LIN.St_set_carry 34 36 | LTL.St_from_acc (r, _) -> 35 37 LIN.St_from_acc (r) -
Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml
r486 r818 127 127 | LTL.St_op2 (_, _, l) 128 128 | LTL.St_clear_carry l 129 | LTL.St_set_carry l 129 130 | LTL.St_load l 130 131 | LTL.St_store l -
Deliverables/D2.2/8051/src/LTL/branch.ml
r486 r818 62 62 | LTL.St_clear_carry l -> 63 63 LTL.St_clear_carry (rep l) 64 | LTL.St_set_carry l -> 65 LTL.St_set_carry (rep l) 64 66 | LTL.St_from_acc (r, l) -> 65 67 LTL.St_from_acc (r, rep l) -
Deliverables/D2.2/8051/src/RTL/RTL.mli
r740 r818 35 35 36 36 (* Apply a binary operation that will later be translated in an operation on 37 the accumulators. Parameters are the operation, the destination register, 38 the source registers, and the label of the next statement. *) 39 | St_opaccs of I8051.opaccs * Register.t * Register.t * Register.t * Label.t 37 the accumulators. Parameters are the operation, the destination registers 38 (ACC first, BACC second), the source registers, and the label of the next 39 statement. *) 40 | St_opaccs of I8051.opaccs * Register.t * Register.t * 41 Register.t * Register.t * Label.t 40 42 41 43 (* Apply an unary operation. Parameters are the operation, the destination … … 50 52 statement. *) 51 53 | St_clear_carry of Label.t 54 55 (* Set the carry flag to 1. Parameter is the label of the next statement. *) 56 | St_set_carry of Label.t 52 57 53 58 (* Load from external memory. Parameters are the destination register, the … … 84 89 the label to go to when the value is not 0, and the label to go to when the 85 90 value is 0. *) 86 | St_cond accof Register.t * Label.t * Label.t91 | St_cond of Register.t * Label.t * Label.t 87 92 88 (* Return the value of some registers. Their may be no register in case of 89 procedures, one register when returning an integer, or two registers when 90 returning an address (low bytes first). *) 93 (* Return the value of some registers (low bytes first). *) 91 94 | St_return of registers 92 95 … … 97 100 { f_luniverse : Label.Gen.universe ; 98 101 f_runiverse : Register.universe ; 99 f_sig : AST.signature ;100 102 f_result : Register.t list (* low byte first *) ; 101 103 f_params : Register.t list ; -
Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml
r740 r818 144 144 [get_local_value lenv srcr] 145 145 146 | RTL.St_opaccs (opaccs, destr , srcr1, srcr2, lbl) ->147 let v=146 | RTL.St_opaccs (opaccs, destr1, destr2, srcr1, srcr2, lbl) -> 147 let (v1, v2) = 148 148 Eval.opaccs opaccs 149 149 (get_local_value lenv srcr1) 150 150 (get_local_value lenv srcr2) in 151 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v] 151 assign_state sfrs graph lbl sp lenv carry mem trace 152 [destr1 ; destr2] [v1 ; v2] 152 153 153 154 | RTL.St_op1 (op1, destr, srcr, lbl) -> … … 164 165 | RTL.St_clear_carry lbl -> 165 166 State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace) 167 168 | RTL.St_set_carry lbl -> 169 State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, trace) 166 170 167 171 | RTL.St_load (destr, addr1, addr2, lbl) -> … … 205 209 CallState (sfrs, f_def, args, mem, trace) 206 210 207 | RTL.St_cond acc(srcr, lbl_true, lbl_false) ->211 | RTL.St_cond (srcr, lbl_true, lbl_false) -> 208 212 let v = get_local_value lenv srcr in 209 213 branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v … … 218 222 219 223 let interpret_external mem f args = match InterpretExternal.t mem f args with 220 | (mem', InterpretExternal.V v ) -> (mem', [v])224 | (mem', InterpretExternal.V vs) -> (mem', vs) 221 225 | (mem', InterpretExternal.A addr) -> (mem', addr) 222 226 … … 273 277 274 278 let compute_result vs = 275 try 276 let v = List.hd vs in 277 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 278 else IntValue.Int8.zero 279 with Not_found -> IntValue.Int8.zero 279 let f res v = res && (Val.is_int v) in 280 let is_int vs = (List.length vs > 0) && (List.fold_left f true vs) in 281 if is_int vs then 282 let chunks = 283 List.map (fun v -> IntValue.Int32.cast (Val.to_int_repr v)) vs in 284 IntValue.Int32.merge chunks 285 else IntValue.Int32.zero 280 286 281 287 let rec iter_small_step debug st = 288 let print_and_return_result (res, cost_labels) = 289 if debug then Printf.printf "Result = %s\n%!" 290 (IntValue.Int32.to_string res) ; 291 (res, cost_labels) in 282 292 if debug then print_state st ; 283 293 match small_step st with 284 | ReturnState ([], vs, mem, trace) -> (compute_result vs, List.rev trace) 294 | ReturnState ([], vs, mem, trace) -> 295 print_and_return_result (compute_result vs, List.rev trace) 285 296 | st' -> iter_small_step debug st' 286 297 … … 288 299 let add_global_vars = 289 300 List.fold_left 290 (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size])301 (fun mem (id, size) -> Mem.add_var mem id (AST.SQ (AST.QInt size)) None) 291 302 292 303 let add_fun_defs = … … 304 315 305 316 let interpret debug p = 306 if debug then Printf.printf "*** RTL ***\n\n%!" ;317 Printf.printf "*** RTL interpret ***\n%!" ; 307 318 match p.RTL.main with 308 | None -> (IntValue.Int 8.zero, [])319 | None -> (IntValue.Int32.zero, []) 309 320 | Some main -> 310 321 let mem = init_mem p in -
Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml
r486 r818 55 55 Printf.sprintf "move %s, %s --> %s" 56 56 (print_reg dstr) (print_reg srcr) lbl 57 | RTL.St_opaccs (opaccs, dstr , srcr1, srcr2, lbl) ->58 Printf.sprintf "%s %s,%s, %s --> %s"57 | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl) -> 58 Printf.sprintf "%s (%s, %s) %s, %s --> %s" 59 59 (I8051.print_opaccs opaccs) 60 (print_reg dstr) 60 (print_reg dstr1) 61 (print_reg dstr2) 61 62 (print_reg srcr1) 62 63 (print_reg srcr2) … … 74 75 | RTL.St_clear_carry lbl -> 75 76 Printf.sprintf "clear CARRY --> %s" lbl 77 | RTL.St_set_carry lbl -> 78 Printf.sprintf "set CARRY --> %s" lbl 76 79 | RTL.St_load (dstr, addr1, addr2, lbl) -> 77 80 Printf.sprintf "load %s, (%s, %s) --> %s" … … 108 111 (print_reg f2) 109 112 (print_args args) 110 | RTL.St_cond acc(srcr, lbl_true, lbl_false) ->113 | RTL.St_cond (srcr, lbl_true, lbl_false) -> 111 114 Printf.sprintf "branch %s <> 0 --> %s, %s" 112 115 (print_reg srcr) lbl_true lbl_false … … 128 131 129 132 Printf.sprintf 130 "%s\"%s\"%s : %s\n%slocals: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"133 "%s\"%s\"%s\n%slocals: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s" 131 134 (n_spaces n) 132 135 f 133 136 (print_params def.RTL.f_params) 134 (Primitive.print_sig def.RTL.f_sig)135 137 (n_spaces (n+2)) 136 138 (print_locals def.RTL.f_locals) -
Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml
r740 r818 34 34 | ERTL.St_int (r, i, _) -> ERTL.St_int (r, i, lbl) 35 35 | ERTL.St_move (r1, r2, _) -> ERTL.St_move (r1, r2, lbl) 36 | ERTL.St_opaccs (opaccs, dstr, srcr1, srcr2, _) -> 37 ERTL.St_opaccs (opaccs, dstr, srcr1, srcr2, lbl) 36 | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, _) -> 37 ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl) 38 | ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, _) -> 39 ERTL.St_opaccsB (opaccs, dstr, srcr1, srcr2, lbl) 38 40 | ERTL.St_op1 (op1, dstr, srcr, _) -> ERTL.St_op1 (op1, dstr, srcr, lbl) 39 41 | ERTL.St_op2 (op2, dstr, srcr1, srcr2, _) -> 40 42 ERTL.St_op2 (op2, dstr, srcr1, srcr2, lbl) 41 43 | ERTL.St_clear_carry _ -> ERTL.St_clear_carry lbl 44 | ERTL.St_set_carry _ -> ERTL.St_set_carry lbl 42 45 | ERTL.St_load (dstrs, addr1, addr2, _) -> 43 46 ERTL.St_load (dstrs, addr1, addr2, lbl) … … 45 48 ERTL.St_store (addr1, addr2, srcrs, lbl) 46 49 | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl) 47 | ERTL.St_cond acc_ as inst -> inst50 | ERTL.St_cond _ as inst -> inst 48 51 | ERTL.St_return _ as inst -> inst 49 52 … … 52 55 53 56 let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with 54 | [] -> def57 | [] -> add_graph start_lbl (ERTL.St_skip dest_lbl) def 55 58 | [stmt] -> 56 59 add_graph start_lbl (change_label dest_lbl stmt) def … … 66 69 let rec add_translates translate_list start_lbl dest_lbl def = 67 70 match translate_list with 68 | [] -> def71 | [] -> add_graph start_lbl (ERTL.St_skip dest_lbl) def 69 72 | [trans] -> trans start_lbl dest_lbl def 70 73 | trans :: translate_list -> … … 168 171 before jumping out of the function. *) 169 172 170 let save_return ret_regs = match ret_regs with 171 | [] -> [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl] 172 | [r] -> 173 [fun start_lbl dest_lbl def -> 174 let (def, r_tmp) = fresh_reg def in 175 adds_graph [ERTL.St_int (r_tmp, 0, start_lbl) ; 176 ERTL.St_set_hdw (I8051.st0, r, start_lbl) ; 177 ERTL.St_set_hdw (I8051.st1, r_tmp, start_lbl)] 178 start_lbl dest_lbl def] 179 | r1 :: r2 :: _ -> 180 [(fun start_lbl -> 181 adds_graph [ERTL.St_set_hdw (I8051.st0, r1, start_lbl) ; 182 ERTL.St_set_hdw (I8051.st1, r2, start_lbl)] start_lbl)] 173 let save_return ret_regs start_lbl dest_lbl def = 174 let (def, tmpr) = fresh_reg def in 175 let ((common1, rest1), (common2, _)) = 176 MiscPottier.reduce I8051.sts ret_regs in 177 let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in 178 let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in 179 let saves = List.map2 f_save common1 common2 in 180 let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in 181 let defaults = List.map f_default rest1 in 182 adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def 183 184 let assign_result start_lbl = 185 let ((common1, _), (common2, _)) = MiscPottier.reduce I8051.rets I8051.sts in 186 let f ret st = ERTL.St_hdw_to_hdw (ret, st, start_lbl) in 187 let insts = List.map2 f common1 common2 in 188 adds_graph insts start_lbl 183 189 184 190 let add_epilogue ret_regs sral srah sregs def = … … 190 196 ([adds_graph [ERTL.St_comment ("Epilogue", start_lbl)]] @ 191 197 (* save return value *) 192 (save_return ret_regs)@198 [save_return ret_regs] @ 193 199 (* restore callee-saved registers *) 194 200 [adds_graph [ERTL.St_comment ("Restore callee-saved registers", … … 204 210 (* assign the result to actual return registers *) 205 211 [adds_graph [ERTL.St_comment ("Set result", start_lbl)]] @ 206 [adds_graph [ERTL.St_hdw_to_hdw (I8051.dpl, I8051.st0, start_lbl) ; 207 ERTL.St_hdw_to_hdw (I8051.dph, I8051.st1, start_lbl) ; 208 ERTL.St_comment ("End Epilogue", start_lbl)]]) 212 [assign_result] @ 213 [adds_graph [ERTL.St_comment ("End Epilogue", start_lbl)]]) 209 214 start_lbl tmp_lbl def in 210 215 let def = add_graph tmp_lbl last_stmt def in … … 243 248 let (def, tmpr) = fresh_reg def in 244 249 adds_graph 245 [ERTL.St_int (addr 2, off+I8051.int_size, start_lbl) ;250 [ERTL.St_int (addr1, off+I8051.int_size, start_lbl) ; 246 251 ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ; 247 252 ERTL.St_clear_carry start_lbl ; … … 275 280 pseudo-register. *) 276 281 277 let fetch_result ret_regs start_lbl = match ret_regs with 278 | [] -> adds_graph [ERTL.St_skip start_lbl] start_lbl 279 | [r] -> 280 adds_graph 281 [ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ; 282 ERTL.St_get_hdw (r, I8051.st0, start_lbl)] 283 start_lbl 284 | r1 :: r2 :: _ -> 285 adds_graph 286 [ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ; 287 ERTL.St_hdw_to_hdw (I8051.st1, I8051.dph, start_lbl) ; 288 ERTL.St_get_hdw (r1, I8051.st0, start_lbl) ; 289 ERTL.St_get_hdw (r2, I8051.st1, start_lbl)] 290 start_lbl 282 let fetch_result ret_regs start_lbl = 283 let ((common1, _), (common2, _)) = MiscPottier.reduce I8051.sts I8051.rets in 284 let f_save st ret = ERTL.St_hdw_to_hdw (st, ret, start_lbl) in 285 let saves = List.map2 f_save common1 common2 in 286 let ((common1, _), (common2, _)) = MiscPottier.reduce ret_regs I8051.sts in 287 let f_restore r st = ERTL.St_get_hdw (r, st, start_lbl) in 288 let restores = List.map2 f_restore common1 common2 in 289 adds_graph (saves @ restores) start_lbl 291 290 292 291 (* When calling a function, we need to set its parameters in specific locations: … … 299 298 ([adds_graph [ERTL.St_comment ("Starting a call", start_lbl)] ; 300 299 adds_graph [ERTL.St_comment ("Setting up parameters", start_lbl)]] @ 301 set_params args @ 302 [adds_graph [ERTL.St_call_id (f, nb_args, start_lbl)] ; 303 adds_graph [ERTL.St_comment ("Fetching result", start_lbl)] ; 304 fetch_result ret_regs]) 300 set_params args @ 301 [adds_graph [ERTL.St_call_id (f, nb_args, start_lbl)] ; 302 adds_graph [ERTL.St_comment ("Fetching result", start_lbl)] ; 303 fetch_result ret_regs ; 304 adds_graph [ERTL.St_comment ("End of call sequence", start_lbl)]]) 305 305 start_lbl dest_lbl def 306 306 … … 334 334 add_graph lbl (ERTL.St_move (r1, r2, lbl')) def 335 335 336 | RTL.St_opaccs (op, destr, srcr1, srcr2, lbl') -> 337 add_graph lbl (ERTL.St_opaccs (op, destr, srcr1, srcr2, lbl')) def 336 | RTL.St_opaccs (op, destr1, destr2, srcr1, srcr2, lbl') -> 337 adds_graph [ERTL.St_opaccsA (op, destr1, srcr1, srcr2, lbl) ; 338 ERTL.St_opaccsB (op, destr2, srcr1, srcr2, lbl) ;] 339 lbl lbl' def 338 340 339 341 | RTL.St_op1 (op1, destr, srcr, lbl') -> … … 345 347 | RTL.St_clear_carry lbl' -> 346 348 add_graph lbl (ERTL.St_clear_carry lbl') def 349 350 | RTL.St_set_carry lbl' -> 351 add_graph lbl (ERTL.St_set_carry lbl') def 347 352 348 353 | RTL.St_load (destr, addr1, addr2, lbl') -> … … 366 371 *) 367 372 368 | RTL.St_cond acc(srcr, lbl_true, lbl_false) ->369 add_graph lbl (ERTL.St_cond acc(srcr, lbl_true, lbl_false)) def373 | RTL.St_cond (srcr, lbl_true, lbl_false) -> 374 add_graph lbl (ERTL.St_cond (srcr, lbl_true, lbl_false)) def 370 375 371 376 | RTL.St_return ret_regs -> … … 427 432 | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl) 428 433 | ERTL.St_addrL (_, _, lbl) | ERTL.St_int (_, _, lbl) 429 | ERTL.St_move (_, _, lbl) | ERTL.St_opaccs (_, _, _, _, lbl) 434 | ERTL.St_move (_, _, lbl) | ERTL.St_opaccsA (_, _, _, _, lbl) 435 | ERTL.St_opaccsB (_, _, _, _, lbl) 430 436 | ERTL.St_op1 (_, _, _, lbl) | ERTL.St_op2 (_, _, _, _, lbl) 431 | ERTL.St_clear_carry lbl | ERTL.St_load (_, _, _, lbl) 437 | ERTL.St_clear_carry lbl | ERTL.St_set_carry lbl 438 | ERTL.St_load (_, _, _, lbl) 432 439 | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl) 433 440 | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl) 434 441 -> 435 442 aux lbl 436 | ERTL.St_cond acc_ | ERTL.St_return _ ->443 | ERTL.St_cond _ | ERTL.St_return _ -> 437 444 (* No cost label found (no labelling performed). Indeed, the first cost 438 445 label must after some linear instructions. *) -
Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli
r740 r818 9 9 RTLabs is the last language of the frontend. It is intended to 10 10 ease retargetting. *) 11 12 13 (* The following type represents the possible addresses to load from or store to14 memory. *)15 16 type addressing =17 18 (* Address is r1 + offset *)19 | Aindexed of AST.immediate20 21 (* Address is r1 + r2 *)22 | Aindexed223 24 (* Address is symbol + offset *)25 | Aglobal of AST.ident * AST.immediate26 27 (* Address is symbol + offset + r1 *)28 | Abased of AST.ident * AST.immediate29 30 (* Address is stack_pointer + offset *)31 | Ainstack of AST.immediate32 11 33 12 … … 58 37 59 38 (* Memory load. Parameters are the size in bytes of what to load, the 60 addressing mode and its arguments, the destination register and the label39 register containing the address, the destination register and the label 61 40 of the next statement. *) 62 | St_load of Memory.quantity * addressing * Register.t list * Register.t * 63 Label.t 41 | St_load of AST.quantity * Register.t * Register.t * Label.t 64 42 65 43 (* Memory store. Parameters are the size in bytes of what to store, the 66 addressing mode and its arguments, the source register and the label of the44 register containing the address, the source register and the label of the 67 45 next statement. *) 68 | St_store of Memory.quantity * addressing * Register.t list * Register.t * 69 Label.t 46 | St_store of AST.quantity * Register.t * Register.t * Label.t 70 47 71 48 (* Call to a function given its name. Parameters are the name of the … … 73 50 register, the signature of the function and the label of the next 74 51 statement. *) 75 | St_call_id of AST.ident * Register.t list * Register.t *52 | St_call_id of AST.ident * Register.t list * Register.t option * 76 53 AST.signature * Label.t 77 54 … … 83 60 differenciate the two to allow translation to a formalism with no 84 61 function pointer. *) 85 | St_call_ptr of Register.t * Register.t list * Register.t *62 | St_call_ptr of Register.t * Register.t list * Register.t option * 86 63 AST.signature * Label.t 87 64 … … 97 74 | St_tailcall_ptr of Register.t * Register.t list * AST.signature 98 75 99 (* Constant branch. Parameters are the constant, the label to go to when the 100 constant evaluates to true (not 0), and the label to go to when the 101 constant evaluates to false (0). *) 102 | St_condcst of AST.cst * Label.t * Label.t 103 104 (* Unary branch. Parameters are the operation, its argument, the 105 label to go to when the operation on the argument evaluates to 106 true (not 0), and the label to go to when the operation on the 107 argument evaluates to false (0). *) 108 | St_cond1 of AST.op1 * Register.t * Label.t * Label.t 109 110 (* Binary branch. Parameters are the operation, its arguments, the 111 label to go to when the operation on the arguments evaluates to 112 true (not 0), and the label to go to when the operation on the 113 arguments evaluates to false (0). *) 114 | St_cond2 of AST.op2 * Register.t * Register.t * Label.t * Label.t 76 (* Branch. Parameters are the register holding the value to branch on, the 77 label to go to when the value evaluates to true (not 0), and the label 78 to go to when the value evaluates to false (0). *) 79 | St_cond of Register.t * Label.t * Label.t 115 80 116 81 (* Jump statement. Parameters are a register and a list of … … 120 85 121 86 (* Return statement. *) 122 | St_return of Register.t 87 | St_return of Register.t option 123 88 124 89 … … 128 93 { f_luniverse : Label.Gen.universe ; 129 94 f_runiverse : Register.universe ; 130 f_sig : AST.signature ; 131 f_result : Register.t ; 132 f_params : Register.t list ; 133 f_locals : Register.t list ; 134 f_ptrs : Register.t list ; 135 f_stacksize : int ; 95 f_result : (Register.t * AST.sig_type) option ; 96 f_params : (Register.t * AST.sig_type) list ; 97 f_locals : (Register.t * AST.sig_type) list ; 98 f_stacksize : AST.abstract_size ; 136 99 f_graph : graph ; 137 100 f_entry : Label.t ; … … 146 109 147 110 type program = 148 { vars : (AST.ident * int (* size *)) list ;111 { vars : (AST.ident * AST.abstract_size) list ; 149 112 functs : (AST.ident * function_def) list ; 150 113 main : AST.ident option } -
Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml
r740 r818 16 16 17 17 18 (* Local environments. They associate a value to the registers of the function19 being executed. *)20 21 type local_env = Val.tRegister.Map.t22 23 (* Call frames. The execution state has a call stack, each element of 24 the stack being composed of the return registers to store the result25 of the callee, the graph, the stack pointer, the node and the local26 environment to resume the execution of the caller. *)18 (* Local environments. They associate a value and a type to the registers of the 19 function being executed. *) 20 21 type local_env = (Val.t * AST.sig_type) Register.Map.t 22 23 (* Call frames. The execution state has a call stack, each element of the stack 24 being composed of the return registers to store the result of the callee, the 25 graph, the stack pointer, the node, the local environment and the typing 26 environments to resume the execution of the caller. *) 27 27 28 28 type stack_frame = 29 { ret_reg : Register.t ;29 { ret_reg : Register.t option ; 30 30 graph : RTLabs.graph ; 31 31 sp : Val.address ; … … 47 47 48 48 let string_of_local_env lenv = 49 let f x vs =49 let f x (v, _) s = 50 50 s ^ 51 51 (if Val.eq v Val.undef then "" … … 78 78 Mem.find_fun_def mem addr 79 79 80 let get_local_ value (lenv : local_env) (r : Register.t) : Val.t=81 if Register.Map.mem r lenv then Register.Map.find r lenv80 let get_local_env f lenv r = 81 if Register.Map.mem r lenv then f (Register.Map.find r lenv) 82 82 else error ("Unknown local register \"" ^ (Register.print r) ^ "\".") 83 let get_arg_values lenv args = List.map (get_local_value lenv) args 84 85 let adds rs vs lenv = 86 let f lenv r v = Register.Map.add r v lenv in 83 84 let get_value = get_local_env fst 85 let get_args lenv args = List.map (get_value lenv) args 86 87 let get_type = get_local_env snd 88 89 let update_local r v lenv = 90 let f (_, t) = Register.Map.add r (v, t) lenv in 91 get_local_env f lenv r 92 93 let update_locals rs vs lenv = 94 let f lenv r v = update_local r v lenv in 87 95 List.fold_left2 f lenv rs vs 88 96 … … 91 99 92 100 93 let eval_addressing 94 (mem : memory) 95 (sp : Val.address) 96 (mode : RTLabs.addressing) 97 (args : Val.t list) : 98 Val.address = match mode, args with 99 100 | RTLabs.Aindexed off, v :: _ -> 101 address_of_value (Val.add v (Val.of_int off)) 102 103 | RTLabs.Aindexed2, v1 :: v2 :: _ -> 104 address_of_value (Val.add v1 v2) 105 106 | RTLabs.Aglobal (id, off), _ -> 107 Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off) 108 109 | RTLabs.Abased (id, off), v :: _ -> 110 let addr = 111 Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off) in 112 address_of_value (Val.add (value_of_address addr) v) 113 114 | RTLabs.Ainstack off, _ -> 115 Val.add_address sp (Val.Offset.of_int off) 116 117 | _, _ -> error "Bad addressing mode." 118 119 120 let eval_cst mem sp = function 121 | AST.Cst_int i -> Val.of_int i 122 | AST.Cst_float f -> error_float () 123 | AST.Cst_addrsymbol id -> value_of_address (Mem.find_global mem id) 124 | AST.Cst_stackoffset shift -> 125 value_of_address (Val.add_address sp (Val.Offset.of_int shift)) 126 127 let eval_op1 = function 128 | AST.Op_cast8unsigned -> Val.cast8unsigned 129 | AST.Op_cast8signed -> Val.cast8signed 130 | AST.Op_cast16unsigned -> Val.cast16unsigned 131 | AST.Op_cast16signed -> Val.cast16signed 132 | AST.Op_negint -> Val.negint 133 | AST.Op_notbool -> Val.notbool 134 | AST.Op_notint -> Val.notint 135 | AST.Op_negf 136 | AST.Op_absf 137 | AST.Op_singleoffloat 138 | AST.Op_intoffloat 139 | AST.Op_intuoffloat 140 | AST.Op_floatofint 141 | AST.Op_floatofintu -> error_float () 142 | AST.Op_id -> (fun (v : Val.t) -> v) 143 | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO or not? *) 144 145 let rec eval_op2 = function 146 | AST.Op_add | AST.Op_addp -> Val.add 147 | AST.Op_sub | AST.Op_subp -> Val.sub 148 | AST.Op_mul -> Val.mul 149 | AST.Op_div -> Val.div 150 | AST.Op_divu -> Val.divu 151 | AST.Op_mod -> Val.modulo 152 | AST.Op_modu -> Val.modulou 153 | AST.Op_and -> Val.and_op 154 | AST.Op_or -> Val.or_op 155 | AST.Op_xor -> Val.xor 156 | AST.Op_shl -> Val.shl 157 | AST.Op_shr -> Val.shr 158 | AST.Op_shru -> Val.shru 159 | AST.Op_cmp AST.Cmp_eq -> Val.cmp_eq 160 | AST.Op_cmp AST.Cmp_ne -> Val.cmp_ne 161 | AST.Op_cmp AST.Cmp_lt -> Val.cmp_lt 162 | AST.Op_cmp AST.Cmp_le -> Val.cmp_le 163 | AST.Op_cmp AST.Cmp_gt -> Val.cmp_gt 164 | AST.Op_cmp AST.Cmp_ge -> Val.cmp_ge 165 | AST.Op_cmpu AST.Cmp_eq -> Val.cmp_eq_u 166 | AST.Op_cmpu AST.Cmp_ne -> Val.cmp_ne_u 167 | AST.Op_cmpu AST.Cmp_lt -> Val.cmp_lt_u 168 | AST.Op_cmpu AST.Cmp_le -> Val.cmp_le_u 169 | AST.Op_cmpu AST.Cmp_gt -> Val.cmp_gt_u 170 | AST.Op_cmpu AST.Cmp_ge -> Val.cmp_ge_u 171 | AST.Op_cmpp cmp -> eval_op2 (AST.Op_cmp cmp) 172 | AST.Op_addf 173 | AST.Op_subf 174 | AST.Op_mulf 175 | AST.Op_divf 176 | AST.Op_cmpf _ -> error_float () 101 module Eval = CminorInterpret.Eval_op (Mem) 102 103 let concrete_stacksize = Eval.concrete_stacksize 104 177 105 178 106 (* Assign a value to some destinations registers. *) 179 107 180 108 let assign_state sfrs graph sp lbl lenv mem trace destr v = 181 let lenv = Register.Map.adddestr v lenv in109 let lenv = update_local destr v lenv in 182 110 State (sfrs, graph, sp, lbl, lenv, mem, trace) 183 111 … … 205 133 state = match stmt with 206 134 207 | RTLabs.St_skip lbl -> State (sfrs, graph, sp, lbl, lenv, mem, trace) 135 | RTLabs.St_skip lbl -> 136 State (sfrs, graph, sp, lbl, lenv, mem, trace) 208 137 209 138 | RTLabs.St_cost (cost_lbl, lbl) -> … … 211 140 212 141 | RTLabs.St_cst (destr, cst, lbl) -> 213 let v = eval_cst mem spcst in142 let v = Eval.cst mem sp (get_type lenv destr) cst in 214 143 assign_state sfrs graph sp lbl lenv mem trace destr v 215 144 216 145 | RTLabs.St_op1 (op1, destr, srcr, lbl) -> 217 let v = eval_op1 op1 (get_local_value lenv srcr) in 146 let v = 147 Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1 148 (get_value lenv srcr) in 218 149 assign_state sfrs graph sp lbl lenv mem trace destr v 219 150 220 151 | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) -> 221 152 let v = 222 eval_op2 op2 223 (get_local_value lenv srcr1) 224 (get_local_value lenv srcr2) in 153 Eval.op2 154 (get_type lenv destr) (get_type lenv srcr1) (get_type lenv srcr2) 155 op2 156 (get_value lenv srcr1) 157 (get_value lenv srcr2) in 225 158 assign_state sfrs graph sp lbl lenv mem trace destr v 226 159 227 | RTLabs.St_load (q, mode, args, destr, lbl) ->228 let addr = eval_addressing mem sp mode (get_arg_values lenv args) in160 | RTLabs.St_load (q, addr, destr, lbl) -> 161 let addr = address_of_value (get_value lenv addr) in 229 162 let v = Mem.loadq mem q addr in 230 163 assign_state sfrs graph sp lbl lenv mem trace destr v 231 164 232 | RTLabs.St_store (q, mode, args, srcr, lbl) ->233 let addr = eval_addressing mem sp mode (get_arg_values lenv args) in234 let v = get_ local_value lenv srcr in165 | RTLabs.St_store (q, addr, srcr, lbl) -> 166 let addr = address_of_value (get_value lenv addr) in 167 let v = get_value lenv srcr in 235 168 let mem = Mem.storeq mem q addr v in 236 169 State (sfrs, graph, sp, lbl, lenv, mem, trace) … … 238 171 | RTLabs.St_call_id (f, args, destr, sg, lbl) -> 239 172 let f_def = find_function mem f in 240 let args = get_arg _values lenv args in173 let args = get_args lenv args in 241 174 (* Save the stack frame. *) 242 175 let sf = … … 246 179 247 180 | RTLabs.St_call_ptr (r, args, destr, sg, lbl) -> 248 let addr = get_ local_value lenv r in181 let addr = get_value lenv r in 249 182 let f_def = Mem.find_fun_def mem (address_of_value addr) in 250 let args = get_arg _values lenv args in183 let args = get_args lenv args in 251 184 (* Save the stack frame. *) 252 185 let sf = … … 257 190 | RTLabs.St_tailcall_id (f, args, sg) -> 258 191 let f_def = find_function mem f in 259 let args = get_arg _values lenv args in192 let args = get_args lenv args in 260 193 (* No need to save the stack frame. But free the stack. *) 261 194 let mem = Mem.free mem sp in … … 263 196 264 197 | RTLabs.St_tailcall_ptr (r, args, sg) -> 265 let addr = get_ local_value lenv r in198 let addr = get_value lenv r in 266 199 let f_def = Mem.find_fun_def mem (address_of_value addr) in 267 let args = get_arg _values lenv args in200 let args = get_args lenv args in 268 201 (* No need to save the stack frame. But free the stack. *) 269 202 let mem = Mem.free mem sp in 270 203 CallState (sfrs, f_def, args, mem, trace) 271 204 272 | RTLabs.St_cond cst (cst, lbl_true, lbl_false) ->273 let v = eval_cst mem sp cstin205 | RTLabs.St_cond (srcr, lbl_true, lbl_false) -> 206 let v = get_value lenv srcr in 274 207 branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v 275 208 209 (* 210 | RTLabs.St_condcst (cst, t, lbl_true, lbl_false) -> 211 let v = Eval.cst mem sp t cst in 212 branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v 213 276 214 | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) -> 277 let v = eval_op1 op1 (get_local_value lenv srcr) in 215 let v = 216 Eval.op1 (get_type lenv srcr) (get_type lenv srcr) 217 op1 (get_value lenv srcr) in 278 218 branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v 279 219 280 220 | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) -> 281 221 let v = 282 eval_op2 op2283 (get_ local_value lenv srcr1)284 (get_ local_value lenv srcr2) in222 Eval.op2 op2 223 (get_value lenv srcr1) 224 (get_value lenv srcr2) in 285 225 branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v 226 *) 286 227 287 228 | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *) 288 229 (* 289 let i = match get_ local_value lenv r with230 let i = match get_value lenv r with 290 231 | Val.Val_int i -> i 291 232 | Val.Val_ptr _ -> error "Illegal cast from pointer to integer." … … 299 240 *) 300 241 301 | RTLabs.St_return r -> 302 let v = get_local_value lenv r in 242 | RTLabs.St_return None -> 243 let mem = Mem.free mem sp in 244 ReturnState (sfrs, Val.undef, mem, trace) 245 246 | RTLabs.St_return (Some r) -> 247 let v = get_value lenv r in 303 248 let mem = Mem.free mem sp in 304 249 ReturnState (sfrs, v, mem, trace) … … 308 253 309 254 let interpret_external mem f args = match InterpretExternal.t mem f args with 310 | (mem', InterpretExternal.V v) -> (mem', v) 255 | (mem', InterpretExternal.V vs) -> 256 let v = if List.length vs = 0 then Val.undef else List.hd vs in 257 (mem', v) 311 258 | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) 312 259 260 313 261 let init_locals 314 (locals : Register.tlist)315 (params : Register.tlist)316 (args : Val.t list) :262 (locals : (Register.t * AST.sig_type) list) 263 (params : (Register.t * AST.sig_type) list) 264 (args : Val.t list) : 317 265 local_env = 318 let f lenv r = Register.Map.add r Val.undeflenv in319 let lenv = List.fold_left f Register.Map.empty localsin320 let f lenv r v = Register.Map.add r v lenvin321 List.fold_left 2 f lenv params args266 let f_param lenv (r, t) v = Register.Map.add r (v, t) lenv in 267 let f_local lenv (r, t) = Register.Map.add r (Val.undef, t) lenv in 268 let lenv = List.fold_left2 f_param Register.Map.empty params args in 269 List.fold_left f_local lenv locals 322 270 323 271 let state_after_call … … 330 278 match f_def with 331 279 | RTLabs.F_int def -> 332 let (mem', sp) = Mem.alloc mem def.RTLabs.f_stacksize in 333 State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry, 334 init_locals def.RTLabs.f_locals def.RTLabs.f_params args, 335 mem', trace) 280 let (mem', sp) = 281 Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in 282 let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in 283 State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry, lenv, mem', 284 trace) 336 285 | RTLabs.F_ext def -> 337 286 let (mem', v) = interpret_external mem def.AST.ef_tag args in … … 346 295 (trace : CostLabel.t list) : 347 296 state = 348 let lenv = Register.Map.add sf.ret_reg ret_val sf.lenv in 297 let lenv = match sf.ret_reg with 298 | None -> sf.lenv 299 | Some ret_reg -> update_local ret_reg ret_val sf.lenv in 349 300 State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace) 350 301 … … 363 314 364 315 let compute_result v = 365 if Val.is_int v then IntValue.Int 8.cast (Val.to_int_repr v)366 else IntValue.Int 8.zero316 if Val.is_int v then IntValue.Int32.cast (Val.to_int_repr v) 317 else IntValue.Int32.zero 367 318 368 319 let rec iter_small_step debug st = 320 let print_and_return_result (res, cost_labels) = 321 if debug then Printf.printf "Result = %s\n%!" 322 (IntValue.Int32.to_string res) ; 323 (res, cost_labels) in 369 324 if debug then print_state st ; 370 325 match small_step st with 371 | ReturnState ([], v, mem, trace) -> (compute_result v, List.rev trace) 326 | ReturnState ([], v, mem, trace) -> 327 print_and_return_result (compute_result v, List.rev trace) 372 328 | st' -> iter_small_step debug st' 373 329 374 330 375 331 let add_global_vars = 376 List.fold_left 377 (fun mem (id, size) -> Mem.add_var mem id [AST.Data_reserve size]) 332 List.fold_left (fun mem (id, size) -> Mem.add_var mem id size None) 378 333 379 334 let add_fun_defs = … … 381 336 382 337 383 (* The memory is initialized by load the code into it, and by reserving space338 (* The memory is initialized by loading the code into it, and by reserving space 384 339 for the global variables. *) 385 340 … … 391 346 392 347 let interpret debug p = 393 if debug then Printf.printf "*** RTLabs ***\n\n%!" ;348 Printf.printf "*** RTLabs interpret ***\n%!" ; 394 349 match p.RTLabs.main with 395 | None -> (IntValue.Int 8.zero, [])350 | None -> (IntValue.Int32.zero, []) 396 351 | Some main -> 397 352 let mem = init_mem p in -
Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml
r740 r818 3 3 4 4 5 let rec print_size = function 6 | AST.SQ q -> Memory.string_of_quantity q 7 | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}" 8 | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}" 9 | AST.SArray (i, se) -> 10 (print_size se) ^ "[" ^ (string_of_int i) ^ "]" 11 and print_size_list l = 12 MiscPottier.string_of_list ", " print_size l 13 5 14 let print_global n (x, size) = 6 Printf.sprintf "%s\"%s\" [%d]" (n_spaces n) x size15 Printf.sprintf "%s\"%s\" { %s }" (n_spaces n) x (print_size size) 7 16 8 17 let print_globals n globs = … … 14 23 let print_reg = Register.print 15 24 25 let print_oreg = function 26 | None -> "_" 27 | Some r -> print_reg r 28 29 let print_decl (r, t) = 30 (Primitive.print_type t) ^ " " ^ (Register.print r) 31 16 32 let rec print_args args = 17 33 Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args) 18 34 19 let print_result r = print_reg r 35 let print_result = function 36 | None -> "_" 37 | Some (r, t) -> (Primitive.print_type t) ^ " " ^ (Register.print r) 20 38 21 39 let print_params r = 22 Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_ regr)40 Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_decl r) 23 41 24 42 let print_locals r = 25 Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_ regr)43 Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_decl r) 26 44 27 45 … … 34 52 | AST.Cmp_le -> "le" 35 53 54 let rec print_size = function 55 | AST.SQ q -> Memory.string_of_quantity q 56 | AST.SProd l -> "struct {" ^ (print_size_list l) ^ "}" 57 | AST.SSum l -> "union {" ^ (print_size_list l) ^ "}" 58 | AST.SArray (i, se) -> 59 (print_size se) ^ "[" ^ (string_of_int i) ^ "]" 60 and print_size_list l = 61 MiscPottier.string_of_list ", " print_size l 62 63 let print_stacksize = print_size 64 65 let print_offset (size, depth) = 66 (print_size size) ^ ", " ^ (string_of_int depth) 67 68 let print_sizeof = print_size 69 36 70 let print_cst = function 37 71 | AST.Cst_int i -> Printf.sprintf "imm_int %d" i 38 72 | AST.Cst_float f -> Printf.sprintf "imm_float %f" f 39 73 | AST.Cst_addrsymbol id -> Printf.sprintf "imm_addr \"%s\"" id 40 | AST.Cst_stackoffset off -> Printf.sprintf "imm_addr %d(STACK)" off 74 | AST.Cst_stack -> "imm_addr STACK" 75 | AST.Cst_offset off -> Printf.sprintf "imm_offset { %s }" (print_offset off) 76 | AST.Cst_sizeof t -> "imm_sizeof (" ^ (print_size t) ^ ")" 77 78 let string_of_signedness = function 79 | AST.Signed -> "s" 80 | AST.Unsigned -> "u" 81 82 let string_of_int_type (size, sign) = 83 Printf.sprintf "%d%s" size (string_of_signedness sign) 41 84 42 85 let print_op1 = function 43 | AST.Op_cast8unsigned -> "cast8u" 44 | AST.Op_cast8signed -> "cast8" 45 | AST.Op_cast16unsigned -> "cast16u" 46 | AST.Op_cast16signed -> "cast16" 86 | AST.Op_cast (int_type, dest_size) -> 87 Printf.sprintf "int%sto%d" (string_of_int_type int_type) dest_size 47 88 | AST.Op_negint -> "negint" 48 89 | AST.Op_notbool -> "notbool" 49 90 | AST.Op_notint -> "notint" 50 | AST.Op_negf -> "negf"51 | AST.Op_absf -> "absf"52 | AST.Op_singleoffloat -> "singleoffloat"53 | AST.Op_intoffloat -> "intoffloat"54 | AST.Op_intuoffloat -> "intuoffloat"55 | AST.Op_floatofint -> "floatofint"56 | AST.Op_floatofintu -> "floatofintu"57 91 | AST.Op_id -> "id" 58 92 | AST.Op_ptrofint -> "ptrofint" … … 64 98 | AST.Op_mul -> "mul" 65 99 | AST.Op_div -> "div" 66 | AST.Op_divu -> " divu"100 | AST.Op_divu -> "/u" 67 101 | AST.Op_mod -> "mod" 68 102 | AST.Op_modu -> "modu" … … 73 107 | AST.Op_shr -> "shr" 74 108 | AST.Op_shru -> "shru" 75 | AST.Op_addf -> "addf"76 | AST.Op_subf -> "subf"77 | AST.Op_mulf -> "mulf"78 | AST.Op_divf -> "divf"79 109 | AST.Op_cmp cmp -> print_cmp cmp 80 | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u"81 | AST.Op_cmpf cmp -> (print_cmp cmp) ^ "f"82 110 | AST.Op_addp -> "addp" 83 111 | AST.Op_subp -> "subp" 112 | AST.Op_subpp -> "subpp" 84 113 | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p" 85 86 114 | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u" 115 116 117 (* 87 118 let print_addressing = function 88 | RTLabs.Aindexed off -> Printf.sprintf " %d" off119 | RTLabs.Aindexed off -> Printf.sprintf "{ %s }" (print_offset off) 89 120 | RTLabs.Aindexed2 -> "add" 90 | RTLabs.Aglobal (id, off) -> Printf.sprintf "%d(\"%s\")" off id 91 | RTLabs.Abased (id, off) -> Printf.sprintf "add, %d(\"%s\")" off id 92 | RTLabs.Ainstack off -> Printf.sprintf "%d(STACK)" off 121 | RTLabs.Aglobal (id, off) -> 122 Printf.sprintf "{ %s }(\"%s\")" (print_offset off) id 123 | RTLabs.Abased (id, off) -> 124 Printf.sprintf "add, { %s }(\"%s\")" (print_offset off) id 125 | RTLabs.Ainstack off -> Printf.sprintf "{ %s }(STACK)" (print_offset off) 126 *) 93 127 94 128 … … 121 155 (print_reg srcr2) 122 156 lbl 123 | RTLabs.St_load (q, mode, args, destr, lbl) ->124 Printf.sprintf "load %s, %s, %s , %s--> %s"157 | RTLabs.St_load (q, addr, destr, lbl) -> 158 Printf.sprintf "load %s, %s, %s --> %s" 125 159 (Memory.string_of_quantity q) 126 (print_addressing mode) 127 (print_args args) 128 (print_reg destr) 129 lbl 130 | RTLabs.St_store (q, mode, args, srcr, lbl) -> 131 Printf.sprintf "store %s, %s, %s, %s --> %s" 160 (print_reg addr) 161 (print_reg destr) 162 lbl 163 | RTLabs.St_store (q, addr, srcr, lbl) -> 164 Printf.sprintf "store %s, %s, %s --> %s" 132 165 (Memory.string_of_quantity q) 133 (print_addressing mode) 134 (print_args args) 166 (print_reg addr) 135 167 (print_reg srcr) 136 168 lbl … … 138 170 Printf.sprintf "call \"%s\", %s, %s: %s --> %s" 139 171 f 140 (print_ params args)141 (print_ reg res)172 (print_args args) 173 (print_oreg res) 142 174 (Primitive.print_sig sg) 143 175 lbl … … 145 177 Printf.sprintf "call_ptr %s, %s, %s: %s --> %s" 146 178 (print_reg f) 147 (print_ params args)148 (print_ reg res)179 (print_args args) 180 (print_oreg res) 149 181 (Primitive.print_sig sg) 150 182 lbl … … 152 184 Printf.sprintf "tailcall \"%s\", %s: %s" 153 185 f 154 (print_ params args)186 (print_args args) 155 187 (Primitive.print_sig sg) 156 188 | RTLabs.St_tailcall_ptr (f, args, sg) -> 157 189 Printf.sprintf "tailcall_ptr \"%s\", %s: %s" 158 190 (print_reg f) 159 (print_params args) 160 (Primitive.print_sig sg) 161 | RTLabs.St_condcst (cst, lbl_true, lbl_false) -> 162 Printf.sprintf "%s --> %s, %s" 191 (print_args args) 192 (Primitive.print_sig sg) 193 | RTLabs.St_cond (r, lbl_true, lbl_false) -> 194 Printf.sprintf "%s? --> %s, %s" 195 (print_reg r) 196 lbl_true 197 lbl_false 198 (* 199 | RTLabs.St_condcst (cst, t, lbl_true, lbl_false) -> 200 Printf.sprintf "(%s) %s --> %s, %s" 201 (Primitive.print_type t) 163 202 (print_cst cst) 164 203 lbl_true … … 177 216 lbl_true 178 217 lbl_false 218 *) 179 219 | RTLabs.St_jumptable (r, tbl) -> 180 220 Printf.sprintf "j_tbl %s --> %s" 181 221 (print_reg r) 182 222 (print_table tbl) 183 | RTLabs.St_return r -> Printf.sprintf "return %s" (print_reg r) 223 | RTLabs.St_return None -> Printf.sprintf "return" 224 | RTLabs.St_return (Some r) -> Printf.sprintf "return %s" (print_reg r) 184 225 185 226 … … 197 238 198 239 Printf.sprintf 199 "%s\"%s\"%s : %s\n%slocals: %s\n%spointers: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"240 "%s\"%s\"%s\n%slocals: %s\n%sresult: %s\n%sstacksize: %s\n%sentry: %s\n%sexit: %s\n\n%s" 200 241 (n_spaces n) 201 242 f 202 243 (print_params def.RTLabs.f_params) 203 (Primitive.print_sig def.RTLabs.f_sig)204 244 (n_spaces (n+2)) 205 245 (print_locals def.RTLabs.f_locals) 206 246 (n_spaces (n+2)) 207 (print_locals def.RTLabs.f_ptrs)208 (n_spaces (n+2))209 247 (print_result def.RTLabs.f_result) 210 248 (n_spaces (n+2)) 211 def.RTLabs.f_stacksize249 (print_stacksize def.RTLabs.f_stacksize) 212 250 (n_spaces (n+2)) 213 251 def.RTLabs.f_entry -
Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml
r740 r818 10 10 let error_float () = error "float not supported." 11 11 let error_shift () = error "Shift operations not supported." 12 12 13 13 14 let add_graph lbl stmt def = … … 30 31 let addr_regs regs = match regs with 31 32 | r1 :: r2 :: _ -> (r1, r2) 32 | _ -> error "Function pointer is not an address." 33 34 35 (* Local environments associate one (in case of an integer) or two (in case of a 36 pointer) RTL pseudo-registers to one RTLabs pseudo-register. *) 37 38 type reg_type = 39 | Int of Register.t 40 | Ptr of Register.t * Register.t 41 42 type local_env = reg_type Register.Map.t 43 44 let initialize_local_env runiverse ptrs registers = 45 let f lenv r = 46 let rt = 47 if List.mem r ptrs then Ptr (r, Register.fresh runiverse) 48 else Int r in 49 Register.Map.add r rt lenv in 33 | _ -> error "registers are not an address." 34 35 let rec register_freshes runiverse n = 36 if n <= 0 then [] 37 else (Register.fresh runiverse) :: (register_freshes runiverse (n-1)) 38 39 let choose_rest rest1 rest2 = match rest1, rest2 with 40 | [], _ -> rest2 41 | _, [] -> rest1 42 | _ -> assert false (* do not use on these arguments *) 43 44 let complete_regs def srcrs1 srcrs2 = 45 let nb_added = (List.length srcrs1) - (List.length srcrs2) in 46 let (def, added_regs) = fresh_regs def nb_added in 47 if nb_added > 0 then (srcrs1, srcrs2 @ added_regs, added_regs) 48 else (srcrs1 @ added_regs, srcrs2, added_regs) 49 50 51 let size_of_sig_type = function 52 | AST.Sig_int (i, _) -> i / Driver.TargetArch.int_size 53 | AST.Sig_float _ -> error_float () 54 | AST.Sig_offset -> Driver.TargetArch.int_size 55 | AST.Sig_ptr -> Driver.TargetArch.ptr_size 56 57 let concrete_size = Driver.RTLMemory.concrete_size 58 59 let concrete_offset = Driver.RTLMemory.concrete_offset 60 61 62 (* Local environments *) 63 64 type local_env = Register.t list Register.Map.t 65 66 let mem_local_env = Register.Map.mem 67 let add_local_env = Register.Map.add 68 let find_local_env = Register.Map.find 69 70 let initialize_local_env runiverse registers result = 71 let registers = 72 registers @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in 73 let f lenv (r, t) = 74 let rs = register_freshes runiverse (size_of_sig_type t) in 75 add_local_env r rs lenv in 50 76 List.fold_left f Register.Map.empty registers 51 77 52 let filter_and_to_list_local_env lenv registers = 53 let f l r = 54 l @ (match Register.Map.find r lenv with 55 | Int r -> [r] 56 | Ptr (r1, r2) -> [r1 ; r2]) in 57 List.fold_left f [] registers 58 59 let list_of_reg_type = function 60 | Int r -> [r] 61 | Ptr (r1, r2) -> [r1 ; r2] 62 63 let find_and_list r lenv = list_of_reg_type (Register.Map.find r lenv) 64 65 let find_and_list_args args lenv = 66 List.map (fun r -> find_and_list r lenv) args 67 68 let find_and_addr r lenv = match find_and_list r lenv with 78 let map_list_local_env lenv regs = 79 let f res r = res @ (find_local_env r lenv) in 80 List.fold_left f [] regs 81 82 let make_addr = function 69 83 | r1 :: r2 :: _ -> (r1, r2) 70 84 | _ -> assert false (* do not use on these arguments *) 71 85 72 let rtl_args regs_list lenv = List.flatten (find_and_list_args regs_list lenv) 73 86 let find_and_addr r lenv = make_addr (find_local_env r lenv) 87 88 let rtl_args regs_list lenv = 89 List.flatten (List.map (fun r -> find_local_env r lenv) regs_list) 74 90 75 91 … … 81 97 | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl) 82 98 | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl) 83 | RTL.St_opaccs (opaccs, dstr , srcr1, srcr2, _) ->84 RTL.St_opaccs (opaccs, dstr , srcr1, srcr2, lbl)99 | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) -> 100 RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl) 85 101 | RTL.St_op1 (op1, dstr, srcr, _) -> RTL.St_op1 (op1, dstr, srcr, lbl) 86 102 | RTL.St_op2 (op2, dstr, srcr1, srcr2, _) -> 87 103 RTL.St_op2 (op2, dstr, srcr1, srcr2, lbl) 88 104 | RTL.St_clear_carry _ -> RTL.St_clear_carry lbl 105 | RTL.St_set_carry _ -> RTL.St_set_carry lbl 89 106 | RTL.St_load (dstrs, addr1, addr2, _) -> 90 107 RTL.St_load (dstrs, addr1, addr2, lbl) … … 96 113 | RTL.St_tailcall_id (f, args) -> RTL.St_tailcall_id (f, args) 97 114 | RTL.St_tailcall_ptr (f1, f2, args) -> RTL.St_tailcall_ptr (f1, f2, args) 98 | RTL.St_cond acc_ as inst -> inst115 | RTL.St_cond _ as inst -> inst 99 116 | RTL.St_return regs -> RTL.St_return regs 100 117 … … 103 120 104 121 let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with 105 | [] -> def122 | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def 106 123 | [stmt] -> 107 124 add_graph start_lbl (change_label dest_lbl stmt) def … … 117 134 let rec add_translates translate_list start_lbl dest_lbl def = 118 135 match translate_list with 119 | [] -> def136 | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def 120 137 | [trans] -> trans start_lbl dest_lbl def 121 138 | trans :: translate_list -> … … 125 142 126 143 127 let rec translate_move destrs srcrs start_lbl dest_lbl def = 128 match destrs, srcrs with 129 | [], [] -> def 130 | [destr], [srcr] -> 131 add_graph start_lbl (RTL.St_move (destr, srcr, dest_lbl)) def 132 | destr :: destrs, srcr :: srcrs -> 133 let tmp_lbl = fresh_label def in 134 let def = 135 add_graph start_lbl (RTL.St_move (destr, srcr, tmp_lbl)) def in 136 translate_move destrs srcrs tmp_lbl dest_lbl def 137 | _ -> assert false (* wrong number of arguments *) 138 139 140 let translate_cst cst destrs start_lbl dest_lbl def = match cst, destrs with 141 142 | AST.Cst_int i, [r] -> 143 add_graph start_lbl (RTL.St_int (r, i, dest_lbl)) def 144 145 | AST.Cst_addrsymbol id, [r1 ; r2] -> 146 add_graph start_lbl (RTL.St_addr (r1, r2, id, dest_lbl)) def 147 148 | AST.Cst_stackoffset off, [r1 ; r2] -> 149 let (def, tmpr) = fresh_reg def in 150 adds_graph 151 [RTL.St_stackaddr (r1, r2, start_lbl) ; 152 RTL.St_int (tmpr, off, start_lbl) ; 153 RTL.St_op2 (I8051.Add, r1, r1, tmpr, start_lbl) ; 154 RTL.St_int (tmpr, 0, start_lbl) ; 155 RTL.St_op2 (I8051.Addc, r2, r2, tmpr, start_lbl)] 156 start_lbl dest_lbl def 157 158 | AST.Cst_float _, _ -> 159 error_float () 160 161 | _, _ -> assert false (* wrong number of arguments *) 162 163 164 let translate_op1 op1 destrs srcrs start_lbl dest_lbl def = 165 match op1, destrs, srcrs with 166 167 | AST.Op_cast8unsigned, _, _ | AST.Op_cast8signed, _, _ 168 | AST.Op_cast16unsigned, _, _ | AST.Op_cast16signed, _, _ -> 169 translate_move destrs srcrs start_lbl dest_lbl def 170 171 | AST.Op_negint, [destr], [srcr] -> 172 adds_graph 173 [RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) ; 174 RTL.St_op1 (I8051.Inc, destr, destr, start_lbl)] 175 start_lbl dest_lbl def 176 177 | AST.Op_notint, [destr], [srcr] -> 178 adds_graph 179 [RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl)] 180 start_lbl dest_lbl def 181 182 | AST.Op_id, _, _ -> 183 translate_move destrs srcrs start_lbl dest_lbl def 184 185 | AST.Op_ptrofint, [destr1 ; destr2], [srcr] -> 186 adds_graph 187 [RTL.St_move (destr1, srcr, dest_lbl) ; 188 RTL.St_int (destr2, 0, start_lbl)] 189 start_lbl dest_lbl def 190 191 | AST.Op_intofptr, [destr], [srcr ; _] -> 192 add_graph start_lbl (RTL.St_move (destr, srcr, dest_lbl)) def 193 194 | AST.Op_notbool, [destr], [srcr] -> 195 let (def, tmpr) = fresh_reg def in 196 adds_graph 197 [RTL.St_int (tmpr, 0, start_lbl) ; 198 RTL.St_clear_carry start_lbl ; 199 RTL.St_op2 (I8051.Sub, destr, tmpr, srcr, start_lbl) ; 200 RTL.St_int (destr, 0, dest_lbl) ; 201 RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl) ; 202 RTL.St_int (tmpr, 1, dest_lbl) ; 203 RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)] 204 start_lbl dest_lbl def 205 206 | AST.Op_negf, _, _ | AST.Op_absf, _, _ | AST.Op_singleoffloat, _, _ 207 | AST.Op_intoffloat, _, _ | AST.Op_intuoffloat, _, _ 208 | AST.Op_floatofint, _, _ | AST.Op_floatofintu, _, _ -> 209 error_float () 210 211 | _ -> assert false (* wrong number of arguments *) 212 144 (* 213 145 214 146 let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def = 215 147 match op2, destrs, srcrs1, srcrs2 with 216 148 217 | AST.Op_add, [destr], [srcr1], [srcr2] -> 218 adds_graph 219 [RTL.St_op2 (I8051.Add, destr, srcr1, srcr2, start_lbl)] 220 start_lbl dest_lbl def 221 222 | AST.Op_sub, [destr], [srcr1], [srcr2] -> 223 adds_graph 224 [RTL.St_clear_carry start_lbl ; 225 RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl)] 226 start_lbl dest_lbl def 227 228 | AST.Op_mul, [destr], [srcr1], [srcr2] -> 149 | AST.Op_mul (1, _), [destr], [srcr1], [srcr2] -> 229 150 adds_graph 230 151 [RTL.St_opaccs (I8051.Mul, destr, srcr1, srcr2, start_lbl)] 231 152 start_lbl dest_lbl def 232 153 233 | AST.Op_div, _, _, _ -> 234 error "Signed division not supported." 235 236 | AST.Op_divu, [destr], [srcr1], [srcr2] -> 237 adds_graph 238 [RTL.St_opaccs (I8051.Divu, destr, srcr1, srcr2, start_lbl)] 239 start_lbl dest_lbl def 240 241 | AST.Op_modu, [destr], [srcr1], [srcr2] -> 242 adds_graph 243 [RTL.St_opaccs (I8051.Modu, destr, srcr1, srcr2, start_lbl)] 244 start_lbl dest_lbl def 245 246 | AST.Op_mod, _, _, _ -> 247 error "Signed modulo not supported." 248 249 | AST.Op_and, [destr], [srcr1], [srcr2] -> 250 adds_graph 251 [RTL.St_op2 (I8051.And, destr, srcr1, srcr2, start_lbl)] 252 start_lbl dest_lbl def 253 254 | AST.Op_or, [destr], [srcr1], [srcr2] -> 255 adds_graph 256 [RTL.St_op2 (I8051.Or, destr, srcr1, srcr2, start_lbl)] 257 start_lbl dest_lbl def 258 259 | AST.Op_xor, [destr], [srcr1], [srcr2] -> 260 adds_graph 261 [RTL.St_op2 (I8051.Xor, destr, srcr1, srcr2, start_lbl)] 262 start_lbl dest_lbl def 263 264 | AST.Op_shru, _, _, _ | AST.Op_shr, _, _, _ | AST.Op_shl, _, _, _ -> 154 | AST.Op_shr _, _, _, _ -> 265 155 error_shift () 266 156 267 | AST.Op_addf, _, _, _ | AST.Op_subf, _, _, _ | AST.Op_mulf, _, _, _ 268 | AST.Op_divf, _, _, _ | AST.Op_cmpf _, _, _, _ -> 269 error_float () 270 271 | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] 272 | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] -> 273 let (def, tmpr1) = fresh_reg def in 274 let (def, tmpr2) = fresh_reg def in 275 adds_graph 276 [RTL.St_op2 (I8051.Add, tmpr1, srcr11, srcr2, start_lbl) ; 277 RTL.St_int (tmpr2, 0, start_lbl) ; 278 RTL.St_op2 (I8051.Addc, destr2, tmpr2, srcr12, start_lbl) ; 279 RTL.St_move (destr1, tmpr1, start_lbl)] 280 start_lbl dest_lbl def 281 282 | AST.Op_subp, [destr], [srcr1 ; _], [srcr2 ; _] -> 283 let (def, tmpr1) = fresh_reg def in 284 let (def, tmpr2) = fresh_reg def in 285 adds_graph 286 [RTL.St_op1 (I8051.Cmpl, tmpr1, srcr2, start_lbl) ; 287 RTL.St_int (tmpr2, 1, start_lbl) ; 288 RTL.St_op2 (I8051.Add, tmpr1, tmpr1, tmpr2, start_lbl) ; 289 RTL.St_op2 (I8051.Add, destr, srcr1, tmpr1, start_lbl)] 290 start_lbl dest_lbl def 291 292 | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] -> 293 adds_graph 294 [RTL.St_clear_carry start_lbl ; 295 RTL.St_op2 (I8051.Sub, destr1, srcr11, srcr2, start_lbl) ; 296 RTL.St_int (destr2, 0, start_lbl) ; 297 RTL.St_op2 (I8051.Sub, destr2, srcr12, destr2, start_lbl)] 298 start_lbl dest_lbl def 299 300 | AST.Op_cmp AST.Cmp_eq, _, _, _ 301 | AST.Op_cmpu AST.Cmp_eq, _, _, _ -> 302 add_translates 303 [translate_op2 AST.Op_sub destrs srcrs1 srcrs2 ; 304 translate_op1 AST.Op_notbool destrs destrs] 305 start_lbl dest_lbl def 306 307 | AST.Op_cmp AST.Cmp_ne, _, _, _ 308 | AST.Op_cmpu AST.Cmp_ne, _, _, _ -> 309 translate_op2 AST.Op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 310 311 | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] -> 157 | AST.Op_cmp (AST.Cmp_lt, (1, AST.Unsigned)), [destr], [srcr1], [srcr2] -> 312 158 let (def, tmpr) = fresh_reg def in 313 159 adds_graph … … 318 164 start_lbl dest_lbl def 319 165 320 | AST.Op_cmpu AST.Cmp_gt, _, _, _ -> 321 translate_op2 (AST.Op_cmpu AST.Cmp_lt) 322 destrs srcrs2 srcrs1 start_lbl dest_lbl def 323 324 | AST.Op_cmpu AST.Cmp_le, _, _, _ -> 325 add_translates 326 [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ; 327 translate_op1 AST.Op_notbool destrs destrs] 328 start_lbl dest_lbl def 329 330 | AST.Op_cmpu AST.Cmp_ge, _, _, _ -> 331 add_translates 332 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ; 333 translate_op1 AST.Op_notbool destrs destrs] 334 start_lbl dest_lbl def 335 336 | AST.Op_cmp cmp, _, _, _ -> 166 | AST.Op_cmp (cmp, ((size, AST.Signed) as int_type)), _, _, _ -> 337 167 let (def, tmprs1) = fresh_regs def (List.length srcrs1) in 338 168 let (def, tmprs2) = fresh_regs def (List.length srcrs2) in … … 340 170 [translate_cst (AST.Cst_int 128) tmprs1 ; 341 171 translate_cst (AST.Cst_int 128) tmprs2 ; 342 translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ; 343 translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ; 344 translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2] 345 start_lbl dest_lbl def 346 347 | AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] -> 348 let (def, tmpr) = fresh_reg def in 349 add_translates 350 [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ; 351 translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ; 352 translate_op2 AST.Op_or [destr] [destr] [tmpr] ; 353 adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ; 354 translate_op2 AST.Op_xor [destr] [destr] [tmpr]] 172 translate_op2 (AST.Op_add int_type) tmprs1 srcrs1 tmprs1 ; 173 translate_op2 (AST.Op_add int_type) tmprs2 srcrs2 tmprs2 ; 174 translate_op2 (AST.Op_cmp (cmp, (size, AST.Unsigned))) 175 destrs tmprs1 tmprs2] 355 176 start_lbl dest_lbl def 356 177 … … 359 180 let (def, tmpr2) = fresh_reg def in 360 181 add_translates 361 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ; 362 translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ; 363 translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ; 182 [translate_op2 (AST.Op_cmp (AST.Cmp_lt, uint)) 183 [tmpr1] [srcr12] [srcr22] ; 184 translate_op2 (AST.Op_cmp (AST.Cmp_eq, uint)) 185 [tmpr2] [srcr12] [srcr22] ; 186 translate_op2 (AST.Op_cmp (AST.Cmp_lt, uint)) 187 [destr] [srcr11] [srcr21] ; 364 188 translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ; 365 189 translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]] 366 190 start_lbl dest_lbl def 367 191 368 | AST.Op_cmpp AST.Cmp_gt, _, _, _ -> 192 | _ -> error_int () 193 *) 194 195 let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with 196 197 | AST.Cst_int _ when destrs = [] -> 198 add_graph start_lbl (RTL.St_skip dest_lbl) def 199 200 | AST.Cst_int i -> 201 let size = List.length destrs in 202 let module M = IntValue.Make (struct let size = size end) in 203 let is = List.map M.to_int (M.break (M.of_int i) size) in 204 let f r i = RTL.St_int (r, i, dest_lbl) in 205 let l = List.map2 f destrs is in 206 adds_graph l start_lbl dest_lbl def 207 208 | AST.Cst_float _ -> error_float () 209 210 | AST.Cst_addrsymbol id -> 211 let (r1, r2) = make_addr destrs in 212 add_graph start_lbl (RTL.St_addr (r1, r2, id, dest_lbl)) def 213 214 | AST.Cst_stack -> 215 let (r1, r2) = make_addr destrs in 216 add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def 217 218 | AST.Cst_offset off -> 219 let i = concrete_offset off in 220 translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def 221 222 | AST.Cst_sizeof size -> 223 let i = concrete_size size in 224 translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def 225 226 227 let rec translate_move destrs srcrs start_lbl = 228 let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in 229 let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in 230 let translates1 = adds_graph (List.map2 f_common common1 common2) in 231 let translates2 = translate_cst (AST.Cst_int 0) rest1 in 232 add_translates [translates1 ; translates2] start_lbl 233 234 235 let translate_cast_unsigned destrs start_lbl dest_lbl def = 236 let (def, tmp_zero) = fresh_reg def in 237 let zeros = MiscPottier.make tmp_zero (List.length destrs) in 238 add_translates 239 [adds_graph [RTL.St_int (tmp_zero, 0, start_lbl)] ; 240 translate_move destrs zeros] 241 start_lbl dest_lbl def 242 243 let translate_cast_signed destrs srcr start_lbl dest_lbl def = 244 let (def, tmp_128) = fresh_reg def in 245 let (def, tmp_255) = fresh_reg def in 246 let (def, tmpr) = fresh_reg def in 247 let (def, dummy) = fresh_reg def in 248 let insts = 249 [RTL.St_int (tmp_128, 128, start_lbl) ; 250 RTL.St_op2 (I8051.And, tmpr, tmp_128, srcr, start_lbl) ; 251 RTL.St_opaccs (I8051.DivuModu, tmpr, dummy, tmpr, tmp_128, start_lbl) ; 252 RTL.St_int (tmp_255, 255, start_lbl) ; 253 RTL.St_opaccs (I8051.Mul, tmpr, dummy, tmpr, tmp_255, start_lbl)] in 254 let srcrs = MiscPottier.make tmpr (List.length destrs) in 255 add_translates [adds_graph insts ; translate_move destrs srcrs] 256 start_lbl dest_lbl def 257 258 let translate_cast src_size src_sign dest_size destrs srcrs = 259 if List.length srcrs = 0 then adds_graph [] 260 else 261 if dest_size < src_size then translate_move destrs srcrs 262 else 263 let ((common1, rest1), (common2, _)) = MiscPottier.reduce destrs srcrs in 264 let insts_common = translate_move common1 common2 in 265 let sign_reg = MiscPottier.last srcrs in 266 let insts_sign = match src_sign with 267 | AST.Unsigned -> translate_cast_unsigned rest1 268 | AST.Signed -> translate_cast_signed rest1 sign_reg in 269 add_translates [insts_common ; insts_sign] 270 271 272 let translate_negint destrs srcrs start_lbl dest_lbl def = 273 assert (List.length destrs = List.length srcrs) ; 274 let (def, tmpr) = fresh_reg def in 275 let f_cmpl destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in 276 let insts_cmpl = List.map2 f_cmpl destrs srcrs in 277 let insts_init = 278 [RTL.St_set_carry start_lbl ; 279 RTL.St_int (tmpr, 0, start_lbl)] in 280 let f_add destr = RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl) in 281 let insts_add = List.map f_add destrs in 282 adds_graph (insts_cmpl @ insts_init @ insts_add) 283 start_lbl dest_lbl def 284 285 286 let translate_notbool destrs srcrs start_lbl dest_lbl def = match destrs with 287 | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def 288 | destr :: destrs -> 289 let (def, tmpr) = fresh_reg def in 290 let (def, tmp_srcrs) = fresh_regs def (List.length srcrs) in 291 let save_srcrs = translate_move tmp_srcrs srcrs in 292 let init_destr = RTL.St_int (destr, 1, start_lbl) in 293 let f tmp_srcr = 294 [RTL.St_clear_carry start_lbl ; 295 RTL.St_int (tmpr, 0, start_lbl) ; 296 RTL.St_op2 (I8051.Sub, tmpr, tmpr, tmp_srcr, start_lbl) ; 297 RTL.St_int (tmpr, 0, start_lbl) ; 298 RTL.St_op2 (I8051.Addc, tmpr, tmpr, tmpr, start_lbl) ; 299 RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)] in 300 let insts = init_destr :: (List.flatten (List.map f tmp_srcrs)) in 301 let epilogue = translate_cst (AST.Cst_int 0) destrs in 302 add_translates [save_srcrs ; adds_graph insts ; epilogue] 303 start_lbl dest_lbl def 304 305 306 let translate_op1 op1 destrs srcrs start_lbl dest_lbl def = match op1 with 307 308 | AST.Op_cast ((src_size, src_sign), dest_size) -> 309 translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl 310 def 311 312 | AST.Op_negint -> 313 translate_negint destrs srcrs start_lbl dest_lbl def 314 315 | AST.Op_notbool -> 316 translate_notbool destrs srcrs start_lbl dest_lbl def 317 318 | AST.Op_notint -> 319 let f destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in 320 let l = List.map2 f destrs srcrs in 321 adds_graph l start_lbl dest_lbl def 322 323 | AST.Op_ptrofint | AST.Op_intofptr | AST.Op_id -> 324 translate_move destrs srcrs start_lbl dest_lbl def 325 326 327 let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def = 328 let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) = 329 MiscPottier.reduce srcrs1 srcrs2 in 330 let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in 331 let ((destrs_common, destrs_rest), _) = 332 MiscPottier.reduce destrs srcrs1_common in 333 let ((destrs_cted, destrs_rest), (srcrs_cted, _)) = 334 MiscPottier.reduce destrs_rest srcrs_rest in 335 let (def, tmpr) = fresh_reg def in 336 let insts_init = 337 [RTL.St_clear_carry start_lbl ; 338 RTL.St_int (tmpr, 0, start_lbl)] in 339 let f_add destr srcr1 srcr2 = 340 RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in 341 let insts_add = 342 MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in 343 let f_add_cted destr srcr = 344 RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in 345 let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in 346 let f_rest destr = 347 RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in 348 let insts_rest = List.map f_rest destrs_rest in 349 adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) 350 start_lbl dest_lbl def 351 352 353 let rec translate_mul1 dummy tmpr destrs srcrs1 srcr2 start_lbl = 354 match destrs, srcrs1 with 355 | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl 356 | [destr], [] -> 357 adds_graph [RTL.St_int (tmpr, 0, start_lbl) ; 358 RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)] 359 start_lbl 360 | destr1 :: destr2 :: destrs, [] -> 361 add_translates 362 [adds_graph [RTL.St_int (tmpr, 0, start_lbl) ; 363 RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl) ; 364 RTL.St_op2 (I8051.Addc, destr2, tmpr, tmpr, start_lbl)] ; 365 translate_cst (AST.Cst_int 0) destrs] 366 start_lbl 367 | [destr], srcr1 :: _ -> 368 adds_graph 369 [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ; 370 RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)] 371 start_lbl 372 | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 -> 373 add_translates 374 [adds_graph 375 [RTL.St_opaccs 376 (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ; 377 RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl)] ; 378 translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2] 379 start_lbl 380 381 let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates 382 srcr2i = 383 let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in 384 translates @ 385 (match tmp_destrs2 with 386 | [] -> [] 387 | tmp_destr2 :: tmp_destrs2 -> 388 [adds_graph [RTL.St_clear_carry dummy_lbl ; 389 RTL.St_int (tmp_destr2, 0, dummy_lbl)] ; 390 translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ; 391 translate_cst (AST.Cst_int 0) tmp_destrs1 ; 392 adds_graph [RTL.St_clear_carry dummy_lbl] ; 393 translate_op I8051.Addc destrs destrs tmp_destrs]) 394 395 let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def = 396 let (def, dummy) = fresh_reg def in 397 let (def, tmpr) = fresh_reg def in 398 let (def, tmp_destrs) = fresh_regs def (List.length destrs) in 399 let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in 400 let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in 401 let insts_init = 402 [translate_move fresh_srcrs1 srcrs1 ; 403 translate_move fresh_srcrs2 srcrs2 ; 404 translate_cst (AST.Cst_int 0) destrs] in 405 let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in 406 let insts_mul = MiscPottier.foldi f [] srcrs2 in 407 add_translates (insts_init @ insts_mul) start_lbl dest_lbl def 408 409 410 let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def = 411 match destrs with 412 | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def 413 | destr :: destrs -> 414 let (def, dummy) = fresh_reg def in 415 let (destr1, destr2) = if order then (destr, dummy) else (dummy, destr) in 416 let inst_div = 417 adds_graph [RTL.St_opaccs (I8051.DivuModu, destr1, destr2, 418 srcr1, srcr2, start_lbl)] in 419 let insts_rest = translate_cst (AST.Cst_int 0) destrs in 420 add_translates [inst_div ; insts_rest] start_lbl dest_lbl def 421 422 423 let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def = 424 match destrs with 425 | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def 426 | destr :: destrs -> 427 let (def, tmpr) = fresh_reg def in 428 let (def, tmp_zero) = fresh_reg def in 429 let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in 430 let save_srcrs1 = translate_move tmp_srcrs1 srcrs1 in 431 let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in 432 let save_srcrs2 = translate_move tmp_srcrs2 srcrs2 in 433 let ((common1, rest1), (common2, rest2)) = 434 MiscPottier.reduce tmp_srcrs1 tmp_srcrs2 in 435 let rest = choose_rest rest1 rest2 in 436 let inits = 437 [RTL.St_int (destr, 0, start_lbl) ; 438 RTL.St_int (tmp_zero, 0, start_lbl)] in 439 let f_common tmp_srcr1 tmp_srcr2 = 440 [RTL.St_clear_carry start_lbl ; 441 RTL.St_op2 (I8051.Sub, tmpr, tmp_srcr1, tmp_srcr2, start_lbl) ; 442 RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in 443 let insts_common = List.flatten (List.map2 f_common common1 common2) in 444 let f_rest tmp_srcr = 445 [RTL.St_clear_carry start_lbl ; 446 RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmp_srcr, start_lbl) ; 447 RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in 448 let insts_rest = List.flatten (List.map f_rest rest) in 449 let insts = inits @ insts_common @ insts_rest in 450 let epilogue = translate_cst (AST.Cst_int 0) destrs in 451 add_translates [save_srcrs1 ; save_srcrs2 ; adds_graph insts ; epilogue] 452 start_lbl dest_lbl def 453 454 455 let translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl 456 (srcr1, srcr2) = 457 [RTL.St_clear_carry dummy_lbl ; 458 RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ; 459 RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ; 460 RTL.St_op2 (I8051.Sub, tmpr2, srcr2, srcr1, dummy_lbl) ; 461 RTL.St_op2 (I8051.Addc, tmpr2, tmp_zero, tmp_zero, dummy_lbl) ; 462 RTL.St_op2 (I8051.Or, tmpr1, tmpr1, tmpr2, dummy_lbl) ; 463 RTL.St_op2 (I8051.Xor, tmpr1, tmpr1, tmp_one, dummy_lbl) ; 464 RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)] 465 466 let translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 destr leq dummy_lbl = 467 let f = translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in 468 (RTL.St_int (destr, 1, dummy_lbl)) :: (List.flatten (List.map f leq)) 469 470 let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq 471 srcr1 srcr2 = 472 (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @ 473 [RTL.St_clear_carry dummy_lbl ; 474 RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ; 475 RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ; 476 RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ; 477 RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)] 478 479 let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl 480 srcrs1 srcrs2 = 481 let f (insts, leq) srcr1 srcr2 = 482 let added_insts = 483 translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq 484 srcr1 srcr2 in 485 (insts @ added_insts, leq @ [(srcr1, srcr2)]) in 486 fst (List.fold_left2 f ([], []) srcrs1 srcrs2) 487 488 let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def = 489 match destrs with 490 | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def 491 | _ -> 492 let (def, tmp_destrs) = fresh_regs def (List.length destrs) in 493 let tmp_destr = List.hd tmp_destrs in 494 let (def, tmp_zero) = fresh_reg def in 495 let (def, tmp_one) = fresh_reg def in 496 let (def, tmpr1) = fresh_reg def in 497 let (def, tmpr2) = fresh_reg def in 498 let (def, tmpr3) = fresh_reg def in 499 let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in 500 let srcrs1 = List.rev srcrs1 in 501 let srcrs2 = List.rev srcrs2 in 502 let insts_init = 503 [translate_cst (AST.Cst_int 0) tmp_destrs ; 504 translate_cst (AST.Cst_int 0) added ; 505 adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ; 506 RTL.St_int (tmp_one, 1, start_lbl)]] in 507 let insts_main = 508 translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl 509 srcrs1 srcrs2 in 510 let insts_main = [adds_graph insts_main] in 511 let insts_exit = [translate_move destrs tmp_destrs] in 512 add_translates (insts_init @ insts_main @ insts_exit ) 513 start_lbl dest_lbl def 514 515 516 let add_128_to_last tmp_128 rs start_lbl = match rs with 517 | [] -> adds_graph [] start_lbl 518 | _ -> 519 let r = MiscPottier.last rs in 520 adds_graph [RTL.St_op2 (I8051.Add, r, r, tmp_128, start_lbl)] start_lbl 521 522 let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def = 523 let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in 524 let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in 525 let (def, tmp_128) = fresh_reg def in 526 add_translates 527 [translate_move tmp_srcrs1 srcrs1 ; 528 translate_move tmp_srcrs2 srcrs2 ; 529 adds_graph [RTL.St_int (tmp_128, 128, start_lbl)] ; 530 add_128_to_last tmp_128 tmp_srcrs1 ; 531 add_128_to_last tmp_128 tmp_srcrs2 ; 532 translate_lt destrs tmp_srcrs1 tmp_srcrs2] 533 start_lbl dest_lbl def 534 535 536 let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def = 537 match op2 with 538 539 | AST.Op_add | AST.Op_addp -> 540 translate_op I8051.Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def 541 542 | AST.Op_sub | AST.Op_subp | AST.Op_subpp -> 543 translate_op I8051.Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 544 545 | AST.Op_mul -> 546 translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def 547 548 | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 -> 549 translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2) 550 start_lbl dest_lbl def 551 552 | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 -> 553 translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2) 554 start_lbl dest_lbl def 555 556 | AST.Op_and -> 557 translate_op I8051.And destrs srcrs1 srcrs2 start_lbl dest_lbl def 558 559 | AST.Op_or -> 560 translate_op I8051.Or destrs srcrs1 srcrs2 start_lbl dest_lbl def 561 562 | AST.Op_xor -> 563 translate_op I8051.Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def 564 565 | AST.Op_cmp AST.Cmp_eq 566 | AST.Op_cmpu AST.Cmp_eq 567 | AST.Op_cmpp AST.Cmp_eq -> 568 add_translates 569 [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ; 570 translate_op1 AST.Op_notbool destrs destrs] 571 start_lbl dest_lbl def 572 573 | AST.Op_cmp AST.Cmp_ne 574 | AST.Op_cmpu AST.Cmp_ne 575 | AST.Op_cmpp AST.Cmp_ne -> 576 translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def 577 578 | AST.Op_cmp AST.Cmp_lt -> 579 translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def 580 581 | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt -> 582 translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def 583 584 | AST.Op_cmp AST.Cmp_le -> 585 add_translates 586 [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ; 587 translate_op1 AST.Op_notbool destrs destrs] 588 start_lbl dest_lbl def 589 590 | AST.Op_cmpu AST.Cmp_le -> 591 add_translates 592 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ; 593 translate_op1 AST.Op_notbool destrs destrs] 594 start_lbl dest_lbl def 595 596 | AST.Op_cmpp AST.Cmp_le -> 597 add_translates 598 [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ; 599 translate_op1 AST.Op_notbool destrs destrs] 600 start_lbl dest_lbl def 601 602 | AST.Op_cmp AST.Cmp_gt -> 603 translate_op2 (AST.Op_cmp AST.Cmp_lt) 604 destrs srcrs2 srcrs1 start_lbl dest_lbl def 605 606 | AST.Op_cmpu AST.Cmp_gt -> 607 translate_op2 (AST.Op_cmpu AST.Cmp_lt) 608 destrs srcrs2 srcrs1 start_lbl dest_lbl def 609 610 | AST.Op_cmpp AST.Cmp_gt -> 369 611 translate_op2 (AST.Op_cmpp AST.Cmp_lt) 370 612 destrs srcrs2 srcrs1 start_lbl dest_lbl def 371 613 372 | AST.Op_cmp p AST.Cmp_le, _, _, _->373 add_translates 374 [translate_op2 (AST.Op_cmp p AST.Cmp_gt) destrs srcrs1 srcrs2 ;614 | AST.Op_cmp AST.Cmp_ge -> 615 add_translates 616 [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ; 375 617 translate_op1 AST.Op_notbool destrs destrs] 376 618 start_lbl dest_lbl def 377 619 378 | AST.Op_cmpp AST.Cmp_ge, _, _, _ -> 620 | AST.Op_cmpu AST.Cmp_ge -> 621 add_translates 622 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ; 623 translate_op1 AST.Op_notbool destrs destrs] 624 start_lbl dest_lbl def 625 626 | AST.Op_cmpp AST.Cmp_ge -> 379 627 add_translates 380 628 [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ; … … 382 630 start_lbl dest_lbl def 383 631 384 | _ -> assert false (* wrong number of arguments *) 385 386 387 let translate_condptr r1 r2 start_lbl lbl_true lbl_false def = 632 | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl 633 | AST.Op_shr | AST.Op_shru -> 634 (* Unsupported, should have been replaced by a runtime function. *) 635 assert false 636 637 638 let translate_cond srcrs start_lbl lbl_true lbl_false def = 388 639 let (def, tmpr) = fresh_reg def in 389 adds_graph 390 [RTL.St_op2 (I8051.Or, tmpr, r1, r2, start_lbl) ; 391 RTL.St_condacc (tmpr, lbl_true, lbl_false)] 392 start_lbl start_lbl def 393 394 395 let translate_condcst cst start_lbl lbl_true lbl_false def = match cst with 396 397 | AST.Cst_int i -> 398 let (def, tmpr) = fresh_reg def in 399 adds_graph 400 [RTL.St_int (tmpr, i, start_lbl) ; 401 RTL.St_condacc (tmpr, lbl_true, lbl_false)] 402 start_lbl start_lbl def 403 404 | AST.Cst_addrsymbol x -> 405 let (def, r1) = fresh_reg def in 406 let (def, r2) = fresh_reg def in 407 let lbl = fresh_label def in 408 let def = add_graph start_lbl (RTL.St_addr (r1, r2, x, lbl)) def in 409 translate_condptr r1 r2 lbl lbl_true lbl_false def 410 411 | AST.Cst_stackoffset off -> 412 let (def, r1) = fresh_reg def in 413 let (def, r2) = fresh_reg def in 414 let tmp_lbl = fresh_label def in 415 let def = 416 translate_cst (AST.Cst_stackoffset off) [r1 ; r2] start_lbl tmp_lbl def in 417 translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def 418 419 | AST.Cst_float _ -> 420 error_float () 421 422 423 let size_of_op1_ret = function 424 | AST.Op_cast8unsigned 425 | AST.Op_cast8signed 426 | AST.Op_cast16unsigned 427 | AST.Op_cast16signed 428 | AST.Op_negint 429 | AST.Op_notbool 430 | AST.Op_notint 431 | AST.Op_intofptr -> 1 432 | AST.Op_ptrofint -> 2 433 | AST.Op_id -> raise (Invalid_argument "RTLabsToRTL.size_of_op1_ret") 434 | AST.Op_negf 435 | AST.Op_absf 436 | AST.Op_singleoffloat 437 | AST.Op_intoffloat 438 | AST.Op_intuoffloat 439 | AST.Op_floatofint 440 | AST.Op_floatofintu -> error_float () 441 442 let rec translate_cond1 op1 srcrs start_lbl lbl_true lbl_false def = 443 match op1, srcrs with 444 445 | AST.Op_id, [srcr] -> 446 adds_graph 447 [RTL.St_condacc (srcr, lbl_true, lbl_false)] 448 start_lbl start_lbl def 449 450 | AST.Op_id, [srcr1 ; srcr2] -> 451 translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def 452 453 | AST.Op_id, _ -> assert false (* wrong number of arguments *) 454 455 | _, srcrs -> 456 let (def, destrs) = fresh_regs def (size_of_op1_ret op1) in 457 let lbl = fresh_label def in 458 let def = translate_op1 op1 destrs srcrs start_lbl lbl def in 459 translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def 460 461 462 let size_of_op2_ret n = function 463 | AST.Op_add 464 | AST.Op_sub 465 | AST.Op_mul 466 | AST.Op_div 467 | AST.Op_divu 468 | AST.Op_mod 469 | AST.Op_modu 470 | AST.Op_and 471 | AST.Op_or 472 | AST.Op_xor 473 | AST.Op_shl 474 | AST.Op_shr 475 | AST.Op_shru 476 | AST.Op_cmp _ 477 | AST.Op_cmpu _ 478 | AST.Op_cmpp _ -> 1 479 | AST.Op_addp -> 2 480 | AST.Op_subp -> 481 if n = 4 (* sub between two pointers, result is an integer *) then 1 482 else (* sub between a pointer and an integer, result is a pointer *) 2 483 | AST.Op_addf 484 | AST.Op_subf 485 | AST.Op_mulf 486 | AST.Op_divf 487 | AST.Op_cmpf _ -> error_float () 488 489 let translate_cond2 op2 srcrs1 srcrs2 start_lbl lbl_true lbl_false def = 490 match op2, srcrs1, srcrs2 with 491 492 | AST.Op_cmp AST.Cmp_eq, [srcr1], [srcr2] -> 493 let (def, tmpr) = fresh_reg def in 494 adds_graph 495 [RTL.St_clear_carry start_lbl ; 496 RTL.St_op2 (I8051.Sub, tmpr, srcr1, srcr2, start_lbl) ; 497 RTL.St_condacc (tmpr, lbl_false, lbl_true)] 498 start_lbl start_lbl def 499 500 | _, _, _ -> 501 let n = (List.length srcrs1) + (List.length srcrs2) in 502 let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in 503 let lbl = fresh_label def in 504 let def = translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def in 505 translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def 506 507 508 let rec addressing_pointer mode args destr1 destr2 start_lbl dest_lbl def = 509 let destrs = [destr1 ; destr2] in 510 match mode, args with 511 512 | RTLabs.Aindexed off, [[srcr1 ; srcr2]] -> 513 let (def, tmpr) = fresh_reg def in 514 add_translates 640 let tmp_lbl = fresh_label def in 641 let init = RTL.St_int (tmpr, 0, start_lbl) in 642 let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, srcr, start_lbl) in 643 let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in 644 add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def 645 646 647 let translate_load addr destrs start_lbl dest_lbl def = 648 let (def, save_addr) = fresh_regs def (List.length addr) in 649 let (def, tmp_addr) = fresh_regs def (List.length addr) in 650 let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in 651 let (def, tmpr) = fresh_reg def in 652 let insts_save_addr = translate_move save_addr addr in 653 let f (translates, off) r = 654 let translates = 655 translates @ 515 656 [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ; 516 translate_op2 AST.Op_addp destrs [srcr1 ; srcr2] [tmpr]] 517 start_lbl dest_lbl def 518 519 | RTLabs.Aindexed2, [[srcr11 ; srcr12] ; [srcr2]] 520 | RTLabs.Aindexed2, [[srcr2] ; [srcr11 ; srcr12]] -> 521 translate_op2 AST.Op_addp destrs [srcr11 ; srcr12] [srcr2] 522 start_lbl dest_lbl def 523 524 | RTLabs.Aglobal (x, off), _ -> 525 let (def, tmpr) = fresh_reg def in 526 add_translates 527 [adds_graph [RTL.St_int (tmpr, off, start_lbl) ; 528 RTL.St_addr (destr1, destr2, x, start_lbl)] ; 529 translate_op2 AST.Op_addp destrs destrs [tmpr]] 530 start_lbl dest_lbl def 531 532 | RTLabs.Abased (x, off), [srcrs] -> 533 let (def, tmpr1) = fresh_reg def in 534 let (def, tmpr2) = fresh_reg def in 535 add_translates 536 [addressing_pointer (RTLabs.Aglobal (x, off)) [] tmpr1 tmpr2 ; 537 translate_op2 AST.Op_addp destrs [tmpr1 ; tmpr2] srcrs] 538 start_lbl dest_lbl def 539 540 | RTLabs.Ainstack off, _ -> 541 let (def, tmpr) = fresh_reg def in 542 add_translates 543 [adds_graph [RTL.St_int (tmpr, off, start_lbl) ; 544 RTL.St_stackaddr (destr1, destr2, start_lbl)] ; 545 translate_op2 AST.Op_addp destrs destrs [tmpr]] 546 start_lbl dest_lbl def 547 548 | _ -> assert false (* wrong number of arguments *) 549 550 551 let translate_load q mode args destrs start_lbl dest_lbl def = 552 match q, destrs with 553 554 | Memory.QInt 1, [destr] -> 555 let (def, addr1) = fresh_reg def in 556 let (def, addr2) = fresh_reg def in 557 add_translates 558 [addressing_pointer mode args addr1 addr2 ; 559 adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]] 560 start_lbl dest_lbl def 561 562 | Memory.QPtr, [destr1 ; destr2] -> 563 let (def, addr1) = fresh_reg def in 564 let (def, addr2) = fresh_reg def in 565 let addr = [addr1 ; addr2] in 566 let (def, tmpr) = fresh_reg def in 567 add_translates 568 [addressing_pointer mode args addr1 addr2 ; 569 adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ; 570 RTL.St_int (tmpr, 1, start_lbl)] ; 571 translate_op2 AST.Op_addp addr addr [tmpr] ; 572 adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl)]] 573 start_lbl dest_lbl def 574 575 | _ -> error "Size error in load." 576 577 578 let translate_store q mode args srcrs start_lbl dest_lbl def = 579 match q, srcrs with 580 581 | Memory.QInt 1, [srcr] -> 582 let (def, addr1) = fresh_reg def in 583 let (def, addr2) = fresh_reg def in 584 add_translates 585 [addressing_pointer mode args addr1 addr2 ; 586 adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]] 587 start_lbl dest_lbl def 588 589 | Memory.QPtr, [srcr1 ; srcr2] -> 590 let (def, addr1) = fresh_reg def in 591 let (def, addr2) = fresh_reg def in 592 let addr = [addr1 ; addr2] in 593 let (def, tmpr) = fresh_reg def in 594 add_translates 595 [addressing_pointer mode args addr1 addr2 ; 596 adds_graph [RTL.St_store (addr1, addr2, srcr1, start_lbl) ; 597 RTL.St_int (tmpr, 1, start_lbl)] ; 598 translate_op2 AST.Op_addp addr addr [tmpr] ; 599 adds_graph [RTL.St_store (addr1, addr2, srcr2, dest_lbl)]] 600 start_lbl dest_lbl def 601 602 | _ -> error "Size error in store." 657 translate_op2 AST.Op_addp tmp_addr save_addr [tmpr] ; 658 adds_graph [RTL.St_load (r, tmp_addr1, tmp_addr2, dest_lbl)]] in 659 (translates, off + Driver.TargetArch.int_size) in 660 let (translates, _) = List.fold_left f ([], 0) destrs in 661 add_translates (insts_save_addr :: translates) start_lbl dest_lbl def 662 663 664 let translate_store addr srcrs start_lbl dest_lbl def = 665 let (def, tmp_addr) = fresh_regs def (List.length addr) in 666 let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in 667 let (def, tmpr) = fresh_reg def in 668 let f (translates, off) srcr = 669 let translates = 670 translates @ 671 [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ; 672 translate_op2 AST.Op_addp tmp_addr addr [tmpr] ; 673 adds_graph [RTL.St_store (tmp_addr1, tmp_addr2, srcr, dest_lbl)]] in 674 (translates, off + Driver.TargetArch.int_size) in 675 let (translates, _) = List.fold_left f ([], 0) srcrs in 676 add_translates translates start_lbl dest_lbl def 603 677 604 678 … … 612 686 613 687 | RTLabs.St_cst (destr, cst, lbl') -> 614 translate_cst cst (find_ and_listdestr lenv) lbl lbl' def688 translate_cst cst (find_local_env destr lenv) lbl lbl' def 615 689 616 690 | RTLabs.St_op1 (op1, destr, srcr, lbl') -> 617 translate_op1 op1 (find_ and_list destr lenv) (find_and_listsrcr lenv)691 translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) 618 692 lbl lbl' def 619 693 620 694 | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') -> 621 translate_op2 op2 (find_and_list destr lenv) 622 (find_and_list srcr1 lenv) (find_and_list srcr2 lenv) lbl lbl' def 623 624 | RTLabs.St_load (q, mode, args, destr, lbl') -> 625 translate_load q mode (find_and_list_args args lenv) 626 (find_and_list destr lenv) lbl lbl' def 627 628 | RTLabs.St_store (q, mode, args, srcr, lbl') -> 629 translate_store q mode (find_and_list_args args lenv) 630 (find_and_list srcr lenv) lbl lbl' def 631 632 | RTLabs.St_call_id (f, args, retr, _, lbl') -> 695 translate_op2 op2 (find_local_env destr lenv) 696 (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def 697 698 | RTLabs.St_load (_, addr, destr, lbl') -> 699 translate_load (find_local_env addr lenv) (find_local_env destr lenv) 700 lbl lbl' def 701 702 | RTLabs.St_store (_, addr, srcr, lbl') -> 703 translate_store (find_local_env addr lenv) (find_local_env srcr lenv) 704 lbl lbl' def 705 706 | RTLabs.St_call_id (f, args, None, _, lbl') -> 707 add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def 708 709 | RTLabs.St_call_id (f, args, Some retr, _, lbl') -> 633 710 add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, 634 find_and_list retr lenv, lbl')) def 635 636 | RTLabs.St_call_ptr (f, args, retr, _, lbl') -> 711 find_local_env retr lenv, lbl')) def 712 713 | RTLabs.St_call_ptr (f, args, None, _, lbl') -> 714 let (f1, f2) = find_and_addr f lenv in 715 add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def 716 717 | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') -> 637 718 let (f1, f2) = find_and_addr f lenv in 638 719 add_graph lbl 639 720 (RTL.St_call_ptr 640 (f1, f2, rtl_args args lenv, find_ and_listretr lenv, lbl')) def721 (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def 641 722 642 723 | RTLabs.St_tailcall_id (f, args, _) -> … … 647 728 add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def 648 729 649 | RTLabs.St_condcst (cst, lbl_true, lbl_false) -> 650 translate_condcst cst lbl lbl_true lbl_false def 651 652 | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) -> 653 translate_cond1 op1 (find_and_list srcr lenv) 654 lbl lbl_true lbl_false def 655 656 | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) -> 657 translate_cond2 op2 (find_and_list srcr1 lenv) 658 (find_and_list srcr2 lenv) lbl lbl_true lbl_false def 730 | RTLabs.St_cond (r, lbl_true, lbl_false) -> 731 translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def 659 732 660 733 | RTLabs.St_jumptable _ -> 661 734 error "Jump tables not supported yet." 662 735 663 | RTLabs.St_return r -> 664 add_graph lbl (RTL.St_return (find_and_list r lenv)) def 736 | RTLabs.St_return None -> 737 add_graph lbl (RTL.St_return []) def 738 739 | RTLabs.St_return (Some r) -> 740 add_graph lbl (RTL.St_return (find_local_env r lenv)) def 665 741 666 742 … … 668 744 let runiverse = def.RTLabs.f_runiverse in 669 745 let lenv = 670 initialize_local_env runiverse def.RTLabs.f_ptrs 671 (def.RTLabs.f_params @ def.RTLabs.f_locals) in 672 let result = find_and_list def.RTLabs.f_result lenv in 746 initialize_local_env runiverse 747 (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in 673 748 let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in 674 let params = filter_and_to_list_local_env lenv def.RTLabs.f_paramsin675 let locals = filter_and_to_list_local_env lenv def.RTLabs.f_localsin749 let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in 750 let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in 676 751 let locals = set_of_list locals in 752 let result = match def.RTLabs.f_result with 753 | None -> [] 754 | Some (r, _) -> find_local_env r lenv in 677 755 let res = 678 756 { RTL.f_luniverse = def.RTLabs.f_luniverse ; 679 757 RTL.f_runiverse = runiverse ; 680 RTL.f_sig = def.RTLabs.f_sig ;681 758 RTL.f_result = result ; 682 759 RTL.f_params = params ; 683 760 RTL.f_locals = locals ; 684 RTL.f_stacksize = def.RTLabs.f_stacksize ;761 RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ; 685 762 RTL.f_graph = Label.Map.empty ; 686 763 RTL.f_entry = def.RTLabs.f_entry ; … … 695 772 696 773 let translate p = 697 let f (id, fun_def) = (id, translate_fun_def fun_def) in 698 { RTL.vars = p.RTLabs.vars ; 699 RTL.functs = List.map f p.RTLabs.functs ; 774 let f_global (id, size) = (id, concrete_size size) in 775 let f_funct (id, fun_def) = (id, translate_fun_def fun_def) in 776 { RTL.vars = List.map f_global p.RTLabs.vars ; 777 RTL.functs = List.map f_funct p.RTLabs.functs ; 700 778 RTL.main = p.RTLabs.main } -
Deliverables/D2.2/8051/src/acc.ml
r740 r818 8 8 1. Parse. 9 9 10 2. Labelize.10 2. Add runtime functions. 11 11 12 3. Compile to the target language. 12 3. Labelize. 13 14 4. Compile to the target language. 13 15 (And keep track of annotations if required). 14 16 15 4. Annotate the input program with collected costs.17 5. Annotate the input program with collected costs. 16 18 17 5. Save the annotated input program.19 6. Save the annotated input program. 18 20 19 21 Optionnally, we can interpret the intermediate programs … … 25 27 let tgt_language = Options.get_target_language () in 26 28 let input_ast = Languages.parse src_language filename in 29 let input_ast = Languages.add_runtime input_ast in 27 30 let input_ast = Languages.labelize input_ast in 28 31 let (exact_output, output_filename) = match Options.get_output_files () with … … 53 56 if Options.interpretation_requested () || Options.is_debug_enabled () then 54 57 begin 55 let asts = input_ast :: target_asts in 56 let label_traces = List.map (Languages.interpret false) asts in 58 let asts = target_asts in 59 let debug = Options.is_debug_enabled () in 60 let label_traces = List.map (Languages.interpret debug) asts in 57 61 Printf.eprintf "Checking execution traces...%!"; 58 62 Checker.same_traces (List.combine asts label_traces); -
Deliverables/D2.2/8051/src/clight/clight.mli
r486 r818 8 8 (** ** Types *) 9 9 10 (** Clight types are similar to those of C. They include numeric types,11 pointers, arrays, function types, and composite types (struct and12 union). Numeric types (integers and floats) fully specify the13 bit size of the type. An integer type is a pair of a signed/unsigned14 flag and a bit size: 8, 16 or 32 bits. *)15 16 type signedness = Signed | Unsigned17 18 10 type intsize = I8 | I16 | I32 19 20 (** Float types come in two sizes: 32 bits (single precision)21 and 64-bit (double precision). *)22 11 23 12 type floatsize = F32 | F64 … … 114 103 | Econst_int of int (**r integer literal *) 115 104 | Econst_float of float (**r float literal *) 116 | Evar of ident (**r variable *)105 | Evar of ident (**r variable *) 117 106 | Ederef of expr (**r pointer dereference (unary [*]) *) 118 107 | Eaddrof of expr (**r address-of operator ([&]) *) … … 124 113 | Eorbool of expr*expr (**r sequential or ([||]) *) 125 114 | Esizeof of ctype (**r size of a type *) 126 | Efield of expr*ident (**r access to a member of a struct or union *)115 | Efield of expr*ident (**r access to a member of a struct or union *) 127 116 128 117 (** The following constructors are used by the annotation process only. *) … … 147 136 | Ssequence of statement*statement (**r sequence *) 148 137 | Sifthenelse of expr*statement*statement (**r conditional *) 149 | Swhile of expr*statement (**r [while] loop *)150 | Sdowhile of expr*statement (**r [do] loop *)138 | Swhile of expr*statement (**r [while] loop *) 139 | Sdowhile of expr*statement (**r [do] loop *) 151 140 | Sfor of statement*expr*statement*statement (**r [for] loop *) 152 141 | Sbreak (**r [break] statement *) … … 158 147 | Scost of CostLabel.t * statement 159 148 160 and labeled_statements =(**r cases of a [switch] *)149 and labeled_statements = (**r cases of a [switch] *) 161 150 | LSdefault of statement 162 151 | LScase of int*statement*labeled_statements -
Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml
r740 r818 12 12 13 13 14 let rec seq = function 15 | [] -> Clight.Sskip 16 | [stmt] -> stmt 17 | stmt :: l -> Clight.Ssequence (stmt, seq l) 18 19 20 let call tmp f_id args_and_type res_type = 14 let error_prefix = "Clight32 to Clight8" 15 let error s = Error.global_error error_prefix s 16 17 18 let cint32s = Clight.Tint (Clight.I32, AST.Signed) 19 let cint32u = Clight.Tint (Clight.I32, AST.Unsigned) 20 let cint8s = Clight.Tint (Clight.I8, AST.Signed) 21 let cint8u = Clight.Tint (Clight.I8, AST.Unsigned) 22 23 24 (* Change the main so that it returns a 8 bits integer. Indeed, 32 bits integers 25 will be replaced by structures, and returning a structure from the main is 26 not Clight compliant. *) 27 28 let main_ret_type = function 29 | Clight.Tint (_, AST.Signed) -> cint8s 30 | Clight.Tint (_, AST.Unsigned) -> cint8u 31 | _ -> error "The main should return an integer which is not the case." 32 33 let f_ctype ctype _ = ctype 34 let f_expr e _ _ = e 35 let f_expr_descr ed _ _ = ed 36 37 let f_stmt ret_type stmt sub_exprs_res sub_stmts_res = 38 match stmt, sub_exprs_res with 39 | Clight.Sreturn (Some _), e :: _ -> 40 let e' = Clight.Expr (Clight.Ecast (ret_type, e), ret_type) in 41 Clight.Sreturn (Some e') 42 | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res 43 44 let body_returns ret_type = 45 ClightFold.statement f_ctype f_expr f_expr_descr (f_stmt ret_type) 46 47 let fundef_returns_char = function 48 | Clight.Internal cfun -> 49 let ret_type = main_ret_type cfun.Clight.fn_return in 50 let body = body_returns ret_type cfun.Clight.fn_body in 51 Clight.Internal {cfun with Clight.fn_return = ret_type ; 52 Clight.fn_body = body } 53 | Clight.External _ as fundef -> fundef 54 55 let main_returns_char p = match p.Clight.prog_main with 56 | None -> p 57 | Some main -> 58 let main_def = List.assoc main p.Clight.prog_funct in 59 let main_def = fundef_returns_char main_def in 60 let prog_funct = 61 MiscPottier.update_list_assoc main main_def p.Clight.prog_funct in 62 { p with Clight.prog_funct = prog_funct } 63 64 65 (* Replacement *) 66 67 let seq = 68 List.fold_left 69 (fun stmt1 stmt2 -> Clight.Ssequence (stmt1, stmt2)) 70 Clight.Sskip 71 72 let is_complex = function 73 | Clight.Tstruct _ | Clight.Tunion _ -> true 74 | _ -> false 75 76 let is_subst_complex type_substitutions res_type = 77 if List.mem_assoc res_type type_substitutions then 78 is_complex (List.assoc res_type type_substitutions) 79 else false 80 81 let addrof_with_type e ctype = 82 let ctype = Clight.Tpointer ctype in 83 (Clight.Expr (Clight.Eaddrof e, ctype), ctype) 84 85 let address_if_subst_complex type_substitutions = 86 let f l (e, ctype) = 87 let arg_and_type = 88 if is_subst_complex type_substitutions ctype then addrof_with_type e ctype 89 else (e, ctype) in 90 l @ [arg_and_type] in 91 List.fold_left f [] 92 93 let make_call_struct tmpe res_type f_var args args_types = 94 let (res_e, res_type) = addrof_with_type tmpe res_type in 95 let f_type = Clight.Tfunction (res_type :: args_types, Clight.Tvoid) in 96 let f = Clight.Expr (f_var, f_type) in 97 Clight.Scall (None, f, res_e :: args) 98 99 let make_call_wo_struct tmpe res_type f_var args args_types = 100 let f_type = Clight.Tfunction (args_types, res_type) in 101 let f = Clight.Expr (f_var, f_type) in 102 Clight.Scall (Some tmpe, f, args) 103 104 let make_call type_substitutions tmp f_id args_with_types res_type = 21 105 let tmpe = Clight.Expr (Clight.Evar tmp, res_type) in 22 let (args, args_type) = List.split args_and_type in 106 let args_with_types = 107 address_if_subst_complex type_substitutions args_with_types in 108 let (args, args_types) = List.split args_with_types in 23 109 let f_var = Clight.Evar f_id in 24 let f_type = Clight.Tfunction (args_type, res_type) in 25 let f = Clight.Expr (f_var, f_type) in 26 (tmpe, Clight.Scall (Some tmpe, f, args)) 27 28 let replace_primitives_expression fresh unop_assoc binop_assoc = 29 30 let rec aux e = 31 let Clight.Expr (ed, t) = e in 110 let call = 111 if is_subst_complex type_substitutions res_type then make_call_struct 112 else make_call_wo_struct in 113 (tmpe, call tmpe res_type f_var args args_types) 114 115 let call fresh replaced type_substitutions replacement_assoc 116 args added_stmt added_tmps ret_type = 117 let tmp = fresh () in 118 let replacement_fun_name = List.assoc replaced replacement_assoc in 119 let (tmpe, call) = 120 make_call type_substitutions tmp replacement_fun_name args ret_type in 121 let stmt = seq (added_stmt @ [call]) in 122 (tmpe, stmt, added_tmps @ [(tmp, ret_type)]) 123 124 let replace_ident replacement_assoc x t = 125 let new_name = match t with 126 | Clight.Tfunction _ 127 when List.mem_assoc (Runtime.Fun x) replacement_assoc -> 128 let replacement_fun_name = List.assoc (Runtime.Fun x) replacement_assoc in 129 replacement_fun_name 130 | _ -> x in 131 (Clight.Expr (Clight.Evar new_name, t), Clight.Sskip, []) 132 133 let replace_expression fresh type_substitutions replacement_assoc e = 134 135 let rec aux (Clight.Expr (ed, t) as e) = 32 136 let expr ed = Clight.Expr (ed, t) in 33 137 match ed with 34 138 35 | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _ 36 | Clight.Esizeof _ -> 139 | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Esizeof _ -> 37 140 (e, Clight.Sskip, []) 38 141 39 | Clight.Ederef e -> 40 let (e', stmt, tmps) = aux e in 142 | Clight.Evar x -> replace_ident replacement_assoc x t 143 144 | Clight.Ederef e' -> 145 let (e', stmt, tmps) = aux e' in 41 146 (expr (Clight.Ederef e'), stmt, tmps) 42 147 43 | Clight.Eaddrof e ->44 let (e', stmt, tmps) = aux e in148 | Clight.Eaddrof e' -> 149 let (e', stmt, tmps) = aux e' in 45 150 (expr (Clight.Eaddrof e'), stmt, tmps) 46 151 47 | Clight.Eunop (unop, Clight.Expr (ed', t')) 48 when List.mem_assoc (unop, t') unop_assoc -> 49 let (e', stmt, tmps) = aux (Clight.Expr (ed', t')) in 50 let tmp = fresh () in 51 let (tmpe, call) = 52 call tmp (List.assoc (unop, t') unop_assoc) [(e', t')] t in 53 let stmt = seq [stmt ; call] in 54 (tmpe, stmt, tmps @ [(tmp, t)]) 55 56 | Clight.Ebinop (binop, Clight.Expr (ed1, t1), Clight.Expr (ed2, t2)) 57 when List.mem_assoc (binop, t1, t2) binop_assoc -> 58 let (e1, stmt1, tmps1) = aux (Clight.Expr (ed1, t1)) in 59 let (e2, stmt2, tmps2) = aux (Clight.Expr (ed2, t2)) in 60 let tmp = fresh () in 61 let (tmpe, call) = 62 call tmp (List.assoc (binop, t1, t2) binop_assoc) 63 [(e1, t1) ; (e2, t2)] t in 64 let stmt = seq [stmt1 ; stmt2 ; call] in 65 (tmpe, stmt, tmps1 @ tmps2 @ [(tmp, t)]) 66 67 | _ -> (e, Clight.Sskip, []) (* TODO *) 152 | Clight.Eunop (unop, (Clight.Expr (ed', t') as e')) 153 when List.mem_assoc (Runtime.Unary (unop, t')) replacement_assoc -> 154 let (e', stmt, tmps) = aux e' in 155 call fresh (Runtime.Unary (unop, t')) 156 type_substitutions replacement_assoc [(e', t')] 157 [stmt] tmps t 158 159 | Clight.Eunop (unop, e') -> 160 let (e', stmt, tmps) = aux e' in 161 (expr (Clight.Eunop (unop, e')), stmt, tmps) 162 163 | Clight.Ebinop (binop, 164 (Clight.Expr (ed1, t1) as e1), 165 (Clight.Expr (ed2, t2) as e2)) 166 when 167 List.mem_assoc (Runtime.Binary (binop, t1, t2)) replacement_assoc -> 168 let (e1, stmt1, tmps1) = aux e1 in 169 let (e2, stmt2, tmps2) = aux e2 in 170 call fresh (Runtime.Binary (binop, t1, t2)) 171 type_substitutions replacement_assoc 172 [(e1, t1) ; (e2, t2)] [stmt1 ; stmt2] (tmps1 @ tmps2) t 173 174 | Clight.Ebinop (binop, e1, e2) -> 175 let (e1, stmt1, tmps1) = aux e1 in 176 let (e2, stmt2, tmps2) = aux e2 in 177 let stmt = seq [stmt1 ; stmt2] in 178 (expr (Clight.Ebinop (binop, e1, e2)), stmt, tmps1 @ tmps2) 179 180 | Clight.Ecast (t, (Clight.Expr (_, t') as e')) 181 when List.mem_assoc (Runtime.Cast (t, t')) replacement_assoc -> 182 let (e', stmt, tmps) = aux e' in 183 call fresh (Runtime.Cast (t, t')) 184 type_substitutions replacement_assoc [(e', t')] [stmt] 185 tmps t 186 187 | Clight.Ecast (t', e') -> 188 let (e', stmt, tmps) = aux e' in 189 (expr (Clight.Ecast (t', e')), stmt, tmps) 190 191 | Clight.Econdition (e1, e2, e3) -> 192 let (e1, stmt1, tmps1) = aux e1 in 193 let (e2, stmt2, tmps2) = aux e2 in 194 let (e3, stmt3, tmps3) = aux e3 in 195 let stmt = seq [stmt1 ; stmt2 ; stmt3] in 196 (expr (Clight.Econdition (e1, e2, e3)), stmt, tmps1 @ tmps2 @ tmps3) 197 198 | Clight.Eandbool (e1, e2) -> 199 let (e1, stmt1, tmps1) = aux e1 in 200 let (e2, stmt2, tmps2) = aux e2 in 201 let stmt = seq [stmt1 ; stmt2] in 202 (expr (Clight.Eandbool (e1, e2)), stmt, tmps1 @ tmps2) 203 204 | Clight.Eorbool (e1, e2) -> 205 let (e1, stmt1, tmps1) = aux e1 in 206 let (e2, stmt2, tmps2) = aux e2 in 207 let stmt = seq [stmt1 ; stmt2] in 208 (expr (Clight.Eorbool (e1, e2)), stmt, tmps1 @ tmps2) 209 210 | Clight.Efield (e', field) -> 211 let (e', stmt, tmps) = aux e' in 212 (expr (Clight.Efield (e', field)), stmt, tmps) 213 214 | Clight.Ecost (lbl, e') -> 215 let (e', stmt, tmps) = aux e' in 216 (expr (Clight.Ecost (lbl, e')), stmt, tmps) 217 218 | Clight.Ecall (id, e1, e2) -> 219 let (e1, stmt1, tmps1) = aux e1 in 220 let (e2, stmt2, tmps2) = aux e2 in 221 let stmt = seq [stmt1 ; stmt2] in 222 (expr (Clight.Ecall (id, e1, e2)), stmt, tmps1 @ tmps2) 68 223 69 224 in 70 aux 71 72 73 let replace_ primitives_expression_list fresh unop_assoc binop_assoc =225 aux e 226 227 228 let replace_expression_list fresh type_substitutions replacement_assoc = 74 229 let f (l, stmt, tmps) e = 75 230 let (e', stmt', tmps') = 76 replace_ primitives_expression fresh unop_assoc binop_assoc e in77 (l @ [e ], seq [stmt ; stmt'], tmps @ tmps') in231 replace_expression fresh type_substitutions replacement_assoc e in 232 (l @ [e'], seq [stmt ; stmt'], tmps @ tmps') in 78 233 List.fold_left f ([], Clight.Sskip, []) 79 234 80 235 81 let replace_ primitives_statement fresh unop_assoc binop_assoc =236 let replace_statement fresh type_substitutions replacement_assoc = 82 237 let aux_exp = 83 replace_ primitives_expression fresh unop_assoc binop_assoc in238 replace_expression fresh type_substitutions replacement_assoc in 84 239 let aux_exp_list = 85 replace_ primitives_expression_list fresh unop_assoc binop_assoc in240 replace_expression_list fresh type_substitutions replacement_assoc in 86 241 87 242 let rec aux = function … … 89 244 | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sgoto _ 90 245 | Clight.Sreturn None 91 246 as stmt -> (stmt, []) 92 247 93 248 | Clight.Slabel (lbl, stmt) -> … … 116 271 let (args', stmt3, tmps3) = aux_exp_list args in 117 272 let stmt = seq [stmt1 ; stmt2 ; stmt3 ; 118 273 Clight.Scall (Some e', f', args')] in 119 274 (stmt, tmps1 @ tmps2 @ tmps3) 120 275 … … 144 299 let (stmt3', tmps3) = aux stmt3 in 145 300 let stmt = seq [stmt1' ; stmte ; 146 Clight.Swhile (e', seq [stmt 2' ; stmt3' ; stmte])] in301 Clight.Swhile (e', seq [stmt3' ; stmt2' ; stmte])] in 147 302 (stmt, tmpse @ tmps1 @ tmps2 @ tmps3) 148 303 … … 180 335 181 336 182 let replace_primitives_internal fresh unop_assoc binop_assoc def = 337 let f_ctype type_substitutions ctype sub_ctypes_res = match ctype with 338 | _ when List.mem_assoc ctype type_substitutions -> 339 List.assoc ctype type_substitutions 340 | _ -> ClightFold.ctype_fill_subs ctype sub_ctypes_res 341 342 let replace_ctype type_substitutions = 343 ClightFold.ctype (f_ctype type_substitutions) 344 345 let f_expr = ClightFold.expr_fill_subs 346 347 let f_expr_descr = ClightFold.expr_descr_fill_subs 348 349 let f_stmt = ClightFold.statement_fill_subs 350 351 let statement_replace_ctype type_substitutions = 352 ClightFold.statement (f_ctype type_substitutions) f_expr f_expr_descr f_stmt 353 354 355 let replace_internal fresh type_substitutions replacement_assoc def = 183 356 let (new_body, tmps) = 184 replace_ primitives_statement fresh unop_assoc binop_assoc357 replace_statement fresh type_substitutions replacement_assoc 185 358 def.Clight.fn_body in 186 { def with Clight.fn_vars = def.Clight.fn_vars @ tmps ; 187 Clight.fn_body = new_body } 188 189 let replace_primitives_funct fresh unop_assoc binop_assoc (id, fundef) = 359 let new_body = statement_replace_ctype type_substitutions new_body in 360 let f (x, t) = (x, replace_ctype type_substitutions t) in 361 let params = List.map f def.Clight.fn_params in 362 let vars = List.map f (def.Clight.fn_vars @ tmps) in 363 { Clight.fn_return = replace_ctype type_substitutions def.Clight.fn_return ; 364 Clight.fn_params = params ; 365 Clight.fn_vars = vars ; 366 Clight.fn_body = new_body } 367 368 let replace_funct fresh type_substitutions replacement_assoc (id, fundef) = 190 369 let fundef' = match fundef with 191 370 | Clight.Internal def -> 192 371 Clight.Internal 193 (replace_ primitives_internal fresh unop_assoc binop_assoc def)372 (replace_internal fresh type_substitutions replacement_assoc def) 194 373 | _ -> fundef in 195 374 (id, fundef') 196 375 197 let replace _primitives fresh unop_assoc binop_assoc p =376 let replace fresh type_substitutions replacement_assoc p = 198 377 let prog_funct = 199 List.map (replace_ primitives_funct fresh unop_assoc binop_assoc)378 List.map (replace_funct fresh type_substitutions replacement_assoc) 200 379 p.Clight.prog_funct in 201 380 { p with Clight.prog_funct = prog_funct } 202 381 203 382 383 (* The constant replacement replaces each 32 bits and 16 bits integer constant 384 by a global variable of the same value. They will be replaced by the 385 appropriate structural value by the global replacement that comes 386 afterwards. *) 387 388 module CstMap = 389 Map.Make 390 (struct 391 type t = (int * Clight.intsize * Clight.ctype) 392 let compare = Pervasives.compare 393 end) 394 395 let f_subs fresh replace subs map = 396 let f (l, map) x = 397 let (x, map) = replace fresh map x in 398 (l @ [x], map) in 399 List.fold_left f ([], map) subs 400 401 let rec replace_constant_expr fresh map (Clight.Expr (ed, t) as e) = 402 match ed, t with 403 | Clight.Econst_int i, Clight.Tint (Clight.I8, _) -> 404 (e, map) 405 | Clight.Econst_int i, Clight.Tint (size, _) 406 when CstMap.mem (i, size, t) map -> 407 let id = CstMap.find (i, size, t) map in 408 (Clight.Expr (Clight.Evar id, t), map) 409 | Clight.Econst_int i, Clight.Tint (size, _) -> 410 let id = fresh () in 411 let map = CstMap.add (i, size, t) id map in 412 let id = CstMap.find (i, size, t) map in 413 (Clight.Expr (Clight.Evar id, t), map) 414 | _ -> 415 let (sub_ctypes, sub_exprs) = ClightFold.expr_descr_subs ed in 416 let (sub_exprs, map) = f_subs fresh replace_constant_expr sub_exprs map in 417 let ed = ClightFold.expr_descr_fill_subs ed sub_ctypes sub_exprs in 418 (Clight.Expr (ed, t), map) 419 420 let rec replace_constant_stmt fresh map stmt = 421 let (sub_exprs, sub_stmts) = ClightFold.statement_subs stmt in 422 let (sub_exprs, map) = 423 f_subs fresh replace_constant_expr sub_exprs map in 424 let (sub_stmts, map) = 425 f_subs fresh replace_constant_stmt sub_stmts map in 426 (ClightFold.statement_fill_subs stmt sub_exprs sub_stmts, map) 427 428 let replace_constant_fundef fresh (functs, map) (id, fundef) = 429 match fundef with 430 | Clight.Internal cfun -> 431 let (body, map) = replace_constant_stmt fresh map cfun.Clight.fn_body in 432 let fundef = Clight.Internal { cfun with Clight.fn_body = body } in 433 (functs @ [(id, fundef)], map) 434 | Clight.External _ -> (functs @ [(id, fundef)], map) 435 436 let init_datas i size = 437 [match size with 438 | Clight.I8 -> Clight.Init_int8 i 439 | Clight.I16 -> Clight.Init_int16 i 440 | Clight.I32 -> Clight.Init_int32 i] 441 442 let globals_of_map map = 443 let f (i, size, t) id l = l @ [((id, init_datas i size), t)] in 444 CstMap.fold f map [] 445 446 let replace_constant p = 447 let tmp_universe = ClightAnnotator.fresh_universe "_cst" p in 448 let fresh () = StringTools.Gen.fresh tmp_universe in 449 let (functs, map) = 450 List.fold_left (replace_constant_fundef fresh) 451 ([], CstMap.empty) p.Clight.prog_funct in 452 let csts = globals_of_map map in 453 { p with 454 Clight.prog_funct = functs ; Clight.prog_vars = p.Clight.prog_vars @ csts } 455 456 457 (* Globals replacement *) 458 459 let expand_int size i = 460 let i = Big_int.big_int_of_int i in 461 let i = 462 if Big_int.ge_big_int i Big_int.zero_big_int then i 463 else Big_int.add_big_int i (Big_int.power_int_positive_int 2 size) in 464 let bound = Big_int.power_int_positive_int 2 8 in 465 let rec aux n i = 466 if n >= size then [] 467 else 468 let (next, chunk) = Big_int.quomod_big_int i bound in 469 chunk :: (aux (n+1) next) in 470 List.map (fun i -> Clight.Init_int8 (Big_int.int_of_big_int i)) (aux 0 i) 471 472 let expand_init_data = function 473 | Clight.Init_int16 i -> expand_int 2 i 474 | Clight.Init_int32 i -> expand_int 4 i 475 | init_data -> [init_data] 476 477 let expand_init_datas init_datas = 478 List.flatten (List.map expand_init_data init_datas) 479 480 let replace_global type_substitutions ((id, init_datas), t) = 481 let init_datas = expand_init_datas init_datas in 482 ((id, init_datas), replace_ctype type_substitutions t) 483 484 let replace_globals type_substitutions p = 485 let vars = List.map (replace_global type_substitutions) p.Clight.prog_vars in 486 { p with Clight.prog_vars = vars } 487 488 489 (* Unsupported operations by the 8051. *) 490 491 (* 8 bits signed division *) 492 493 let divs_fun s _ = 494 "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^ 495 " unsigned char x1 = (unsigned char) x;\n" ^ 496 " unsigned char y1 = (unsigned char) y;\n" ^ 497 " signed char sign = 1;\n" ^ 498 " if (x < 0) { x1 = (unsigned char) (-x); sign = -sign; }\n" ^ 499 " if (y < 0) { y1 = (unsigned char) (-y); sign = -sign; }\n" ^ 500 " return (sign * ((signed char) (x1/y1)));\n" ^ 501 "}\n\n" 502 503 let divs = 504 (Runtime.Binary (Clight.Odiv, cint8s, cint8s), "_divs", [], divs_fun, []) 505 506 507 (* 8 bits signed modulo *) 508 509 let mods_fun s _ = 510 "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^ 511 " return (x - (x/y) * y);\n" ^ 512 "}\n\n" 513 514 let mods = 515 (Runtime.Binary (Clight.Omod, cint8s, cint8s), "_mods", [], mods_fun, 516 [Runtime.Binary (Clight.Odiv, cint8s, cint8s)]) 517 518 519 (* Shifts *) 520 521 let sh_fun signedness op s _ = 522 signedness ^ " char " ^ s ^ " (" ^ signedness ^ " char x, " ^ 523 signedness ^ " char y) {\n" ^ 524 " " ^ signedness ^ " char res = x, i;\n" ^ 525 " for (i = 0 ; i < y ; i++) res = res " ^ op ^ " 2;\n" ^ 526 " return res;\n" ^ 527 "}\n\n" 528 529 (* 8 bits shifts left *) 530 531 let shls_fun = sh_fun "signed" "*" 532 533 let shls = 534 (Runtime.Binary (Clight.Oshl, cint8s, cint8s), "_shls", [], shls_fun, []) 535 536 let shlu_fun s _ = 537 "unsigned char " ^ s ^ " (unsigned char x, unsigned char y) {\n" ^ 538 " return ((unsigned char) ((signed char) x << (signed char) y));\n" ^ 539 "}\n\n" 540 541 let shlu = 542 (Runtime.Binary (Clight.Oshl, cint8u, cint8u), "_shlu", [], shlu_fun, 543 [Runtime.Binary (Clight.Oshl, cint8s, cint8s)]) 544 545 (* 8 bits shifts right *) 546 547 let shrs_fun s _ = 548 "signed char " ^ s ^ " (signed char x, signed char y) {\n" ^ 549 " signed char res = x, i;\n" ^ 550 " for (i = 0 ; i < y ; i++) {\n" ^ 551 " res = ((unsigned char) res) / 2;\n" ^ 552 " res = res + ((signed char) 128);\n" ^ 553 " }\n" ^ 554 " return res;\n" ^ 555 "}\n\n" 556 557 let shrs = 558 (Runtime.Binary (Clight.Oshr, cint8s, cint8s), "_shrs", [], shrs_fun, []) 559 560 let shru_fun = sh_fun "unsigned" "/" 561 562 let shru = 563 (Runtime.Binary (Clight.Oshr, cint8u, cint8u), "_shru", [], shru_fun, []) 564 565 566 (* int32 *) 567 568 let struct_int32 name fields = match fields with 569 | lolo :: lohi :: hilo :: hihi :: _ -> 570 Clight.Tstruct 571 (name, 572 [(lolo, cint8u) ; (lohi, cint8u) ; (hilo, cint8u) ; (hihi, cint8u)]) 573 | _ -> error ("bad field names when defining type " ^ name ^ ".") 574 575 let struct_int32_name = "struct _int32_" 576 577 let new_int32 int32 = 578 let lolo = "lolo" in 579 let lohi = "lohi" in 580 let hilo = "hilo" in 581 let hihi = "hihi" in 582 (int32, struct_int32_name, [lolo ; lohi ; hilo ; hihi], struct_int32) 583 584 let int32s = new_int32 (Clight.Tint (Clight.I32, AST.Signed)) 585 let int32u = new_int32 (Clight.Tint (Clight.I32, AST.Unsigned)) 586 587 (* 32 bits operations *) 588 589 (* 32 bits equality *) 590 591 let eq_int32s_fun s l = 592 let (int32, lolo, lohi, hilo, hihi) = match l with 593 | (int32, lolo :: lohi :: hilo :: hihi :: _) :: _ -> 594 (int32, lolo, lohi, hilo, hihi) 595 | _ -> error ("new type definition not coherent in function " ^ s ^ ".") in 596 int32 ^ " " ^ s ^ " (" ^ int32 ^ " x, " ^ int32 ^ " y) {\n" ^ 597 " " ^ int32 ^ " res;\n" ^ 598 " res." ^ lolo ^ " = 1;\n" ^ 599 " if (x." ^ lolo ^ " != y." ^ lolo ^ ") res." ^ lolo ^ " = 0;\n" ^ 600 " if (x." ^ lohi ^ " != y." ^ lohi ^ ") res." ^ lolo ^ " = 0;\n" ^ 601 " if (x." ^ hilo ^ " != y." ^ hilo ^ ") res." ^ lolo ^ " = 0;\n" ^ 602 " if (x." ^ hihi ^ " != y." ^ hihi ^ ") res." ^ lolo ^ " = 0;\n" ^ 603 " res." ^ lohi ^ " = 0;\n" ^ 604 " res." ^ hilo ^ " = 0;\n" ^ 605 " res." ^ hihi ^ " = 0;\n" ^ 606 " return (res);\n" ^ 607 "}\n\n" 608 609 let eq32s = 610 (Runtime.Binary (Clight.Oeq, cint32s, cint32s), "eq_int32s", 611 [struct_int32_name], eq_int32s_fun, []) 612 613 (* 32 bits casts *) 614 615 let int32s_to_int8s_fun s l = 616 let (int32, lolo, lohi, hilo, hihi) = match l with 617 | (int32, lolo :: lohi :: hilo :: hihi :: _) :: _ -> 618 (int32, lolo, lohi, hilo, hihi) 619 | _ -> error ("new type definition not coherent in function " ^ s ^ ".") in 620 "signed char " ^ s ^ " (" ^ int32 ^ " x) {\n" ^ 621 " return ((signed char) x." ^ lolo ^ ");\n" ^ 622 "}\n\n" 623 624 let int32s_to_int8s = 625 (Runtime.Cast (cint8s, cint32s), "int32s_to_int8s", [struct_int32_name], 626 int32s_to_int8s_fun, []) 627 628 629 (* int16 *) 630 631 let struct_int16 name fields = match fields with 632 | lo :: hi :: _ -> 633 Clight.Tstruct (name, [(lo, cint8u) ; (hi, cint8u)]) 634 | _ -> error ("bad field names when defining type " ^ name ^ ".") 635 636 let struct_int16_name = "struct _int16_" 637 638 let new_int16 int16 = 639 let lo = "lo" in 640 let hi = "hi" in 641 (int16, struct_int16_name, [lo ; hi], struct_int16) 642 643 let int16s = new_int16 (Clight.Tint (Clight.I16, AST.Signed)) 644 let int16u = new_int16 (Clight.Tint (Clight.I16, AST.Unsigned)) 645 646 647 (* int32 and int16 *) 648 649 let int32_and_int16_types = [int32s ; int32u ; int16s ; int16u] 650 let int32_and_int16_replacements = [eq32s ; int32s_to_int8s] 651 652 653 let unsupported = [divs ; mods ; shls ; shlu ; shrs ; shru] 654 655 656 let save_and_parse p = 657 let tmp_file = Filename.temp_file "clight32toclight8" ".c" in 658 try 659 let oc = open_out tmp_file in 660 output_string oc (ClightPrinter.print_program p) ; 661 close_out oc ; 662 let res = ClightParser.process tmp_file in 663 Misc.SysExt.safe_remove tmp_file ; 664 res 665 with Sys_error _ -> failwith "Error reparsing Clight8 transformation." 666 667 let add_replacements p new_types replacements = 668 let p = ClightCasts.simplify p in 669 let (p, type_substitutions, replacement_assoc) = 670 Runtime.add p new_types replacements in 671 let p = ClightCasts.simplify p in 672 let tmp_universe = ClightAnnotator.fresh_universe "_tmp" p in 673 let fresh () = StringTools.Gen.fresh tmp_universe in 674 let p = replace fresh type_substitutions replacement_assoc p in 675 let p = replace_globals type_substitutions p in 676 (* Printf.printf "%s\n%!" (ClightPrinter.print_program p) ; *) 677 let p = save_and_parse p in 678 ClightCasts.simplify p 679 204 680 let translate p = 205 (* TODO: restore below *) 206 (* 207 let (p, unop_assoc, binop_assoc) = Runtime.add p in 208 let p = ClightCasts.simplify p in 209 let labs = ClightAnnotator.all_labels p in 210 let tmp_prefix = StringTools.Gen.fresh_prefix labs "_tmp" in 211 let tmp_universe = StringTools.Gen.new_universe tmp_prefix in 212 let fresh () = StringTools.Gen.fresh tmp_universe in 213 let p = replace_primitives fresh unop_assoc binop_assoc p in 214 (* TODO: do the translation *) 215 p 216 *) 217 ClightCasts.simplify p 681 let p = main_returns_char p in 682 let p = replace_constant p in 683 let p = 684 add_replacements p int32_and_int16_types int32_and_int16_replacements in 685 add_replacements p [] unsupported -
Deliverables/D2.2/8051/src/clight/clightAnnotator.ml
r645 r818 19 19 20 20 let triple_union 21 ( var_names1, cost_labels1, user_labels1)22 ( var_names2, cost_labels2, user_labels2) =23 (StringTools.Set.union var_names1 var_names2,21 (names1, cost_labels1, user_labels1) 22 (names2, cost_labels2, user_labels2) = 23 (StringTools.Set.union names1 names2, 24 24 CostLabel.Set.union cost_labels1 cost_labels2, 25 25 Label.Set.union user_labels1 user_labels2) … … 27 27 let empty_triple = (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty) 28 28 29 let name_singleton id = 30 (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) 31 32 let cost_label_singleton cost_lbl = 33 (StringTools.Set.empty, CostLabel.Set.singleton cost_lbl, Label.Set.empty) 34 35 let label_singleton lbl = 36 (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl) 37 29 38 let list_union l = List.fold_left triple_union empty_triple l 30 39 31 let rec exp_idents e = 32 let Clight.Expr (e, _) = e in 33 match e with 34 | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Esizeof _ -> 35 empty_triple 36 | Clight.Evar x -> 37 (StringTools.Set.singleton x, CostLabel.Set.empty, Label.Set.empty) 38 | Clight.Ederef e | Clight.Eaddrof e | Clight.Eunop (_, e) 39 | Clight.Ecast (_, e) -> exp_idents e 40 | Clight.Efield (e, x) -> 41 let (var_names, cost_labels, user_labels) = exp_idents e in 42 (StringTools.Set.add x var_names, cost_labels, user_labels) 43 | Clight.Ebinop (_, e1, e2) | Clight.Eandbool (e1, e2) 44 | Clight.Eorbool (e1, e2) -> list_union [exp_idents e1 ; exp_idents e2] 45 | Clight.Econdition (e1, e2, e3) -> 46 list_union [exp_idents e1 ; exp_idents e2 ; exp_idents e3] 47 | Clight.Ecost (lbl, e) -> 48 let (var_names, cost_labels, user_labels) = exp_idents e in 49 (var_names, CostLabel.Set.add lbl cost_labels, user_labels) 50 | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen *) 51 52 let exp_idents_opt = function 53 | None -> empty_triple 54 | Some e -> exp_idents e 55 56 let exp_idents_list l = list_union (List.map exp_idents l) 57 58 let rec body_idents = function 59 | Clight.Sskip | Clight.Sbreak | Clight.Scontinue -> empty_triple 60 | Clight.Sassign (e1, e2) -> list_union [exp_idents e1 ; exp_idents e2] 61 | Clight.Scall (eopt, f, args) -> 62 list_union [exp_idents_opt eopt ; exp_idents f ; exp_idents_list args] 63 | Clight.Ssequence (s1, s2) -> list_union [body_idents s1 ; body_idents s2] 64 | Clight.Sifthenelse (e, s1, s2) -> 65 list_union [exp_idents e ; body_idents s1 ; body_idents s2] 66 | Clight.Swhile (e, s) | Clight.Sdowhile (e, s) -> 67 list_union [exp_idents e ; body_idents s] 68 | Clight.Sfor (s1, e, s2, s3) -> 69 list_union [body_idents s1 ; exp_idents e ; 70 body_idents s2 ; body_idents s3] 71 | Clight.Sreturn eopt -> exp_idents_opt eopt 72 | Clight.Sswitch (e, ls) -> list_union [exp_idents e ; ls_idents ls] 73 | Clight.Slabel (lbl, stmt) -> 74 let (var_names, cost_labels, user_labels) = body_idents stmt in 75 (var_names, cost_labels, Label.Set.add lbl user_labels) 76 | Clight.Sgoto lbl -> 77 (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.singleton lbl) 78 | Clight.Scost (lbl, stmt) -> 79 let (var_names, cost_labels, user_labels) = body_idents stmt in 80 (var_names, CostLabel.Set.add lbl cost_labels, user_labels) 81 and ls_idents = function 82 | Clight.LSdefault stmt -> body_idents stmt 83 | Clight.LScase (_, stmt, ls) -> list_union [body_idents stmt ; ls_idents ls] 40 let f_ctype ctype sub_ctypes_res = 41 let res = match ctype with 42 | Clight.Tstruct (id, fields) | Clight.Tunion (id, fields) -> 43 (string_set_of_list (id :: (List.map fst fields)), 44 CostLabel.Set.empty, Label.Set.empty) 45 | Clight.Tcomp_ptr id -> name_singleton id 46 | _ -> empty_triple in 47 list_union (res :: sub_ctypes_res) 48 49 let f_expr _ sub_ctypes_res sub_expr_descrs_res = 50 list_union (sub_ctypes_res @ sub_expr_descrs_res) 51 52 let f_expr_descr ed sub_ctypes_res sub_exprs_res = 53 let res = match ed with 54 | Clight.Evar id | Clight.Efield (_, id) | Clight.Ecall (id, _, _) -> 55 name_singleton id 56 | Clight.Ecost (cost_lbl, _) -> cost_label_singleton cost_lbl 57 | _ -> empty_triple in 58 list_union (res :: (sub_ctypes_res @ sub_exprs_res)) 59 60 let f_stmt stmt sub_exprs_res sub_stmts_res = 61 let stmt_res = match stmt with 62 | Clight.Slabel (lbl, _) | Clight.Sgoto lbl -> label_singleton lbl 63 | Clight.Scost (cost_lbl, _) -> cost_label_singleton cost_lbl 64 | _ -> empty_triple in 65 list_union (stmt_res :: (sub_exprs_res @ sub_stmts_res)) 66 67 let body_idents = ClightFold.statement f_ctype f_expr f_expr_descr f_stmt 84 68 85 69 let prog_idents p = … … 89 73 string_set_of_list 90 74 (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in 91 let ( var_names, cost_labels, user_labels) =75 let (names, cost_labels, user_labels) = 92 76 body_idents def.Clight.fn_body in 93 (StringTools.Set.union vars var_names, cost_labels, user_labels)77 (StringTools.Set.union vars names, cost_labels, user_labels) 94 78 | Clight.External (id, _, _) -> 95 79 (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in 96 80 let fun_idents (id, f_def) = 97 let ( var_names, cost_labels, user_labels) = def_idents f_def in98 (StringTools.Set.add id var_names, cost_labels, user_labels) in81 let (names, cost_labels, user_labels) = def_idents f_def in 82 (StringTools.Set.add id names, cost_labels, user_labels) in 99 83 let f idents def = triple_union idents (fun_idents def) in 100 84 List.fold_left f empty_triple p.Clight.prog_funct 101 85 102 let var_names p =103 let ( var_names, _, _) = prog_idents p in var_names86 let names p = 87 let (names, _, _) = prog_idents p in names 104 88 let cost_labels p = 105 89 let (_, cost_labels, _) = prog_idents p in cost_labels … … 114 98 Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all 115 99 100 let all_idents p = 101 let (names, cost_labels, user_labels) = prog_idents p in 102 let to_string_set fold set = 103 fold (fun lbl idents -> StringTools.Set.add lbl idents) set 104 StringTools.Set.empty in 105 let cost_labels = to_string_set CostLabel.Set.fold cost_labels in 106 let user_labels = to_string_set Label.Set.fold user_labels in 107 StringTools.Set.union names (StringTools.Set.union cost_labels user_labels) 108 109 let fresh_ident base p = 110 StringTools.Gen.fresh_prefix (all_idents p) base 111 112 let fresh_universe base p = 113 let universe = fresh_ident base p in 114 StringTools.Gen.new_universe universe 115 116 let make_fresh base p = 117 let universe = fresh_universe base p in 118 (fun () -> StringTools.Gen.fresh universe) 119 116 120 117 121 (* Instrumentation *) 118 122 119 let int_typ = Clight.Tint (Clight.I32, Clight.Signed)123 let int_typ = Clight.Tint (Clight.I32, AST.Signed) 120 124 121 125 let const_int i = Clight.Expr (Clight.Econst_int i, int_typ) … … 311 315 312 316 (* Create a fresh 'cost' variable. *) 313 let var_names = var_names p in314 let cost_id = StringTools.Gen.fresh_prefix var_names cost_id_prefix in317 let names = names p in 318 let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in 315 319 let cost_decl = cost_decl cost_id in 316 320 317 321 (* Define an increment function for the cost variable. *) 318 322 let cost_incr = 319 StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id var_names)323 StringTools.Gen.fresh_prefix (StringTools.Set.add cost_id names) 320 324 cost_incr_prefix in 321 325 let cost_incr_def = cost_incr_def cost_id cost_incr in -
Deliverables/D2.2/8051/src/clight/clightAnnotator.mli
r640 r818 14 14 val user_labels : Clight.program -> Label.Set.t 15 15 val all_labels : Clight.program -> StringTools.Set.t 16 val all_idents : Clight.program -> StringTools.Set.t 17 18 val fresh_ident : string (* base *) -> Clight.program -> string 19 20 val fresh_universe : 21 string (* prefix *) -> Clight.program -> StringTools.Gen.universe 22 23 val make_fresh : 24 string (* prefix *) -> Clight.program -> (unit -> string) -
Deliverables/D2.2/8051/src/clight/clightCasts.ml
r740 r818 6 6 be polymorphic, but working only on homogene types. *) 7 7 8 9 let error_prefix = "Clight casts simplification" 10 let error = Error.global_error error_prefix 11 let error_float () = error "float not supported." 12 13 14 (* Int sizes *) 15 16 let int_of_intsize = function 17 | Clight.I8 -> 8 18 | Clight.I16 -> 16 19 | Clight.I32 -> 32 20 21 let intsize_of_int = function 22 | i when i <= 8 -> Clight.I8 23 | i when i <= 16 -> Clight.I16 24 | _ -> Clight.I32 25 26 let cmp_intsize cmp size1 size2 = 27 cmp (int_of_intsize size1) (int_of_intsize size2) 28 29 let max_intsize size1 size2 = 30 if (int_of_intsize size1) < (int_of_intsize size2) then size2 else size1 31 32 let intsize_union size1 size2 = 33 intsize_of_int ((int_of_intsize size1) + (int_of_intsize size2)) 34 35 let pow2 = MiscPottier.pow 2 36 37 let belongs_to_int_type size sign i = match size, sign with 38 | Clight.I8, AST.Unsigned -> 0 <= i && i <= (pow2 8) - 1 39 | Clight.I8, AST.Signed -> -(pow2 7) <= i && i <= (pow2 7) - 1 40 | Clight.I16, AST.Unsigned -> 0 <= i && i <= (pow2 16) - 1 41 | Clight.I16, AST.Signed -> -(pow2 15) <= i && i <= (pow2 15) - 1 42 | Clight.I32, AST.Unsigned -> 0 <= i 43 | Clight.I32, AST.Signed -> 44 let pow2_30 = pow2 30 in 45 (-(pow2_30 + pow2_30)) <= i && 46 i <= ((pow2_30 - 1) + pow2_30) (* = 2^31 - 1 *) 47 48 let smallest_int_type i = 49 let (size, sign) = match i with 50 | _ when belongs_to_int_type Clight.I8 AST.Signed i -> 51 (Clight.I8, AST.Signed) 52 | _ when belongs_to_int_type Clight.I8 AST.Unsigned i -> 53 (Clight.I8, AST.Unsigned) 54 | _ when belongs_to_int_type Clight.I16 AST.Signed i -> 55 (Clight.I16, AST.Signed) 56 | _ when belongs_to_int_type Clight.I16 AST.Unsigned i -> 57 (Clight.I16, AST.Unsigned) 58 | _ when belongs_to_int_type Clight.I32 AST.Unsigned i -> 59 (Clight.I32, AST.Unsigned) 60 | _ -> 61 (Clight.I32, AST.Signed) in 62 Clight.Tint (size, sign) 63 64 65 let type_of_expr (Clight.Expr (_, t)) = t 66 67 let int_type_union t1 t2 = 68 let (size, sign) = match t1, t2 with 69 | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2) 70 when sign1 = sign2 -> (max_intsize size1 size2, sign1) 71 | Clight.Tint (size1, sign1), Clight.Tint (size2, sign2) -> 72 (intsize_union size1 size2, AST.Signed) 73 | _ -> assert false (* only use on int types *) 74 in 75 Clight.Tint (size, sign) 76 77 let cast_if_needed t (Clight.Expr (ed, t') as e) = match t, ed with 78 | _ when t = t' -> e 79 | Clight.Tint (size, sign), Clight.Econst_int i 80 when belongs_to_int_type size sign i -> 81 Clight.Expr (Clight.Econst_int i, t) 82 | _ -> Clight.Expr (Clight.Ecast (t, e), t) 83 84 let rec simplify_binop t binop 85 (Clight.Expr (ed1, t1) as e1) 86 (Clight.Expr (ed2, t2) as e2) = 87 let e1' = simplify_expr e1 in 88 let e2' = simplify_expr e2 in 89 let make_int i t = Clight.Expr (Clight.Econst_int i, t) in 90 91 let (e1', e2', t') = match t1, t2, ed1, ed2 with 92 93 | Clight.Tint _, Clight.Tint _, 94 Clight.Econst_int i1, Clight.Econst_int i2 -> 95 let t1' = smallest_int_type i1 in 96 let t2' = smallest_int_type i2 in 97 let t' = int_type_union t1' t2' in 98 (make_int i1 t', make_int i2 t', t') 99 100 | Clight.Tint _, Clight.Tint _, _, Clight.Econst_int i2 -> 101 let t' = type_of_expr e1' in 102 let e2' = make_int i2 t' in 103 (e1', e2', t') 104 105 | Clight.Tint _, Clight.Tint _, Clight.Econst_int i1, _ -> 106 let t' = type_of_expr e2' in 107 let e1' = make_int i1 t' in 108 (e1', e2', t') 109 110 | Clight.Tint _, Clight.Tint _, _, _ -> 111 let t' = int_type_union (type_of_expr e1') (type_of_expr e2') in 112 (cast_if_needed t' e1', cast_if_needed t' e2', t') 113 114 | _ -> (e1', e2', t) 115 116 in 117 118 Clight.Expr (Clight.Ebinop (binop, e1', e2'), t') 119 120 and simplify_bool_op f_bool t e1 e2 = 121 let (e1', e2', t') = simplify_and_same_type t e1 e2 in 122 Clight.Expr (f_bool e1' e2', t') 123 124 and simplify_and_same_type t e1 e2 = 125 let e1' = simplify_expr e1 in 126 let e2' = simplify_expr e2 in 127 if type_of_expr e1' = type_of_expr e2' then (e1', e2', type_of_expr e1') 128 else (cast_if_needed t e1', cast_if_needed t e2', t) 129 130 and simplify_expr (Clight.Expr (ed, t) as e) = match ed with 131 132 | Clight.Econst_int i -> 133 let t' = smallest_int_type i in 134 Clight.Expr (ed, t') 135 136 | Clight.Evar _ -> e 137 138 | Clight.Esizeof _ -> Clight.Expr (ed, Clight.Tint (Clight.I8, AST.Unsigned)) 139 140 | Clight.Econst_float _ -> error_float () 141 142 | Clight.Ederef e -> 143 let e' = simplify_expr e in 144 Clight.Expr (Clight.Ederef e', t) 145 146 | Clight.Eaddrof e -> 147 let e' = simplify_expr e in 148 Clight.Expr (Clight.Eaddrof e', t) 149 150 | Clight.Eunop (unop, e) -> 151 let e' = simplify_expr e in 152 Clight.Expr (Clight.Eunop (unop, e'), type_of_expr e') 153 154 | Clight.Ebinop (binop, e1, e2) -> 155 simplify_binop t binop e1 e2 156 157 | Clight.Ecast (Clight.Tint (Clight.I32, AST.Signed), e) -> simplify_expr e 158 159 | Clight.Ecast (t', e) -> 160 Clight.Expr (Clight.Ecast (t', simplify_expr e), t') 161 162 | Clight.Econdition (e1, e2, e3) -> 163 let e1' = simplify_expr e1 in 164 let (e2', e3', t') = simplify_and_same_type t e2 e3 in 165 Clight.Expr (Clight.Econdition (e1', e2', e3'), t') 166 167 | Clight.Eandbool (e1, e2) -> 168 simplify_bool_op (fun e1' e2' -> Clight.Eandbool (e1', e2')) t e1 e2 169 170 | Clight.Eorbool (e1, e2) -> 171 simplify_bool_op (fun e1' e2' -> Clight.Eorbool (e1', e2')) t e1 e2 172 173 | Clight.Efield (e, field) -> 174 Clight.Expr (Clight.Efield (simplify_expr e, field), t) 175 176 | Clight.Ecost (lbl, e) -> 177 Clight.Expr (Clight.Ecost (lbl, simplify_expr e), t) 178 179 | Clight.Ecall (id, e1, e2) -> 180 assert false (* should be impossible *) 181 182 8 183 let f_ctype ctype _ = ctype 9 184 10 (*11 let f_expr = ClightFold.expr_fill_subs12 13 let f_expr_descr e sub_ctypes_res sub_exprs_res =14 match e, sub_exprs_res with15 | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),16 Clight.Expr17 (Clight.Eunop18 (unop,19 Clight.Expr20 (Clight.Ecast21 (Clight.Tint (Clight.I32, _),22 (Clight.Expr (_, Clight.Tint (Clight.I8, signedness2)) as e)),23 _)),24 _) :: _ when signedness1 = signedness2 ->25 Clight.Eunop (unop, e)26 | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),27 Clight.Expr28 (Clight.Ebinop29 (binop,30 Clight.Expr31 (Clight.Ecast32 (Clight.Tint (Clight.I32, _),33 (Clight.Expr (_,34 Clight.Tint (Clight.I8, signedness2)) as e1)),35 _),36 Clight.Expr37 (Clight.Ecast38 (Clight.Tint (Clight.I32, _),39 (Clight.Expr (_,40 Clight.Tint (Clight.I8, signedness3)) as e2)),41 _)),42 _) :: _ when signedness1 = signedness2 && signedness2 = signedness3 ->43 Clight.Ebinop (binop, e1, e2)44 | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),45 Clight.Expr46 (Clight.Ebinop47 (binop,48 Clight.Expr49 (Clight.Ecast50 (Clight.Tint (Clight.I32, _),51 (Clight.Expr (_,52 Clight.Tint (Clight.I8, signedness2)) as e1)),53 _),54 Clight.Expr (Clight.Econst_int i, _)),55 _) :: _ when signedness1 = signedness2 ->56 Clight.Ebinop (binop, e1,57 Clight.Expr (Clight.Econst_int i,58 Clight.Tint (Clight.I8, signedness1)))59 | Clight.Ecast (Clight.Tint (Clight.I8, signedness1), _),60 Clight.Expr61 (Clight.Ebinop62 (binop,63 Clight.Expr (Clight.Econst_int i, _),64 Clight.Expr65 (Clight.Ecast66 (Clight.Tint (Clight.I32, _),67 (Clight.Expr (_,68 Clight.Tint (Clight.I8, signedness2)) as e1)),69 _)),sub_ctypes_res sub_exprs_res70 _) :: _ when signedness1 = signedness2 ->71 Clight.Ebinop (binop,72 Clight.Expr (Clight.Econst_int i,73 Clight.Tint (Clight.I8, signedness1)),74 e1)75 | _ -> ClightFold.expr_descr_fill_subs e sub_ctypes_res sub_exprs_res76 *)77 78 let simplify_exp ctype_opt e = e (* TODO *)79 80 185 let f_expr e _ _ = e 81 186 … … 83 188 84 189 let f_statement stmt _ sub_stmts_res = 85 let sub_exprs = match stmt with 86 | _ -> assert false in 190 let f_expr b e = 191 let e' = simplify_expr e in 192 if b then cast_if_needed (type_of_expr e) e' 193 else e' in 194 let f_exprs b = List.map (f_expr b) in 195 let f_sub_exprs = match stmt with 196 | Clight.Sassign _ | Clight.Scall _ | Clight.Sreturn _ -> f_exprs true 197 | _ -> f_exprs false in 198 let sub_exprs = f_sub_exprs (ClightFold.statement_sub_exprs stmt) in 87 199 ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res 88 200 … … 97 209 (id, fundef') 98 210 99 let simplify p = p 100 (* (* TODO: below *) 211 let simplify p = 101 212 { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct } 102 *) -
Deliverables/D2.2/8051/src/clight/clightFold.ml
r624 r818 75 75 | _ -> assert false (* wrong arguments, do not use on these values *) 76 76 77 let expr_fill_exprs (Clight.Expr (ed, t)) exprs = 78 let (sub_ctypes, _) = expr_descr_subs ed in 79 let ed = expr_descr_fill_subs ed sub_ctypes exprs in 80 Clight.Expr (ed, t) 81 77 82 let rec expr f_ctype f_expr f_expr_descr e = 78 83 let (sub_ctypes, sub_expr_descrs) = expr_subs e in … … 88 93 let sub_ctypes_res = List.map (ctype f_ctype) sub_ctypes in 89 94 f_expr_descr e sub_ctypes_res sub_exprs_res 95 96 97 let expr_subs2 e = 98 let (_, expr_descrs) = expr_subs e in 99 let l = List.map expr_descr_subs expr_descrs in 100 List.flatten (List.map snd l) 101 102 let rec expr2 f e = f e (List.map (expr2 f) (expr_subs2 e)) 90 103 91 104 … … 108 121 | Clight.Sswitch (e, lbl_stmts) -> ([e], labeled_statements_subs lbl_stmts) 109 122 | Clight.Slabel (_, stmt) | Clight.Scost (_, stmt) -> ([], [stmt]) 123 124 let statement_sub_exprs stmt = fst (statement_subs stmt) 110 125 111 126 let rec labeled_statements_fill_subs lbl_stmts sub_statements = … … 149 164 List.map (statement f_ctype f_expr f_expr_descr f_statement) sub_stmts in 150 165 f_statement stmt sub_exprs_res sub_stmts_res 166 167 let rec statement2 f_expr f_statement stmt = 168 let (sub_exprs, sub_stmts) = statement_subs stmt in 169 let sub_exprs_res = List.map (expr2 f_expr) sub_exprs in 170 let sub_stmts_res = List.map (statement2 f_expr f_statement) sub_stmts in 171 f_statement stmt sub_exprs_res sub_stmts_res -
Deliverables/D2.2/8051/src/clight/clightFold.mli
r740 r818 11 11 Clight.expr 12 12 13 val expr_fill_exprs : 14 Clight.expr -> Clight.expr list -> Clight.expr 15 13 16 val expr : 14 17 (Clight.ctype -> 'a list -> 'a) -> … … 17 20 Clight.expr -> 18 21 'c 22 23 val expr2 : 24 (Clight.expr -> 'a list -> 'a) -> Clight.expr -> 'a 25 26 val expr_descr_subs : 27 Clight.expr_descr -> Clight.ctype list * Clight.expr list 19 28 20 29 val expr_descr_fill_subs : … … 29 38 'b 30 39 40 val statement_subs : 41 Clight.statement -> 42 (Clight.expr list * Clight.statement list) 43 44 val statement_sub_exprs : Clight.statement -> Clight.expr list 45 31 46 val statement_fill_subs : 32 47 Clight.statement -> Clight.expr list -> Clight.statement list -> … … 40 55 Clight.statement -> 41 56 'd 57 58 val statement2 : 59 (Clight.expr -> 'a list -> 'a) -> 60 (Clight.statement -> 'a list -> 'b list -> 'b) -> 61 Clight.statement -> 62 'b -
Deliverables/D2.2/8051/src/clight/clightFromC.ml
r486 r818 110 110 111 111 let typeStringLiteral s = 112 Tarray(Tint(I8, Unsigned), String.length s + 1)112 Tarray(Tint(I8, AST.Unsigned), String.length s + 1) 113 113 114 114 let global_for_string s id = … … 170 170 171 171 let convertIkind = function 172 | C.IBool -> unsupported "'_Bool' type"; ( Unsigned, I8)173 | C.IChar -> ( Unsigned, I8)174 | C.ISChar -> ( Signed, I8)175 | C.IUChar -> ( Unsigned, I8)176 | C.IInt -> ( Signed, I32)177 | C.IUInt -> ( Unsigned, I32)178 | C.IShort -> ( Signed, I16)179 | C.IUShort -> ( Unsigned, I16)180 | C.ILong -> ( Signed, I32)181 | C.IULong -> ( Unsigned, I32)172 | C.IBool -> unsupported "'_Bool' type"; (AST.Unsigned, I8) 173 | C.IChar -> (AST.Unsigned, I8) 174 | C.ISChar -> (AST.Signed, I8) 175 | C.IUChar -> (AST.Unsigned, I8) 176 | C.IInt -> (AST.Signed, I32) 177 | C.IUInt -> (AST.Unsigned, I32) 178 | C.IShort -> (AST.Signed, I16) 179 | C.IUShort -> (AST.Unsigned, I16) 180 | C.ILong -> (AST.Signed, I32) 181 | C.IULong -> (AST.Unsigned, I32) 182 182 | C.ILongLong -> 183 183 if not !ClightFlags.option_flonglong then unsupported "'long long' type"; 184 ( Signed, I32)184 (AST.Signed, I32) 185 185 | C.IULongLong -> 186 186 if not !ClightFlags.option_flonglong then unsupported "'unsigned long long' type"; 187 ( Unsigned, I32)187 (AST.Unsigned, I32) 188 188 189 189 let convertFkind = function … … 268 268 (** Expressions *) 269 269 270 let ezero = Expr(Econst_int(0), Tint(I32, Signed))270 let ezero = Expr(Econst_int(0), Tint(I32, AST.Signed)) 271 271 272 272 let rec convertExpr env e = … … 393 393 let volatile_fun_suffix_type ty = 394 394 match ty with 395 | Tint(I8, Unsigned) -> ("int8unsigned", ty)396 | Tint(I8, Signed) -> ("int8signed", ty)397 | Tint(I16, Unsigned) -> ("int16unsigned", ty)398 | Tint(I16, Signed) -> ("int16signed", ty)399 | Tint(I32, _) -> ("int32", Tint(I32, Signed))395 | Tint(I8, AST.Unsigned) -> ("int8unsigned", ty) 396 | Tint(I8, AST.Signed) -> ("int8signed", ty) 397 | Tint(I16, AST.Unsigned) -> ("int16unsigned", ty) 398 | Tint(I16, AST.Signed) -> ("int16signed", ty) 399 | Tint(I32, _) -> ("int32", Tint(I32, AST.Signed)) 400 400 | Tfloat F32 -> ("float32", ty) 401 401 | Tfloat F64 -> ("float64", ty) -
Deliverables/D2.2/8051/src/clight/clightInterpret.ml
r740 r818 210 210 (* ctype functions *) 211 211 212 let rec sizeof = function 213 | Tint (I8, _) -> 1 214 | Tint (I16, _) -> 2 215 | Tint (I32, _) -> 4 216 | Tfloat _ -> error_float () 217 | Tcomp_ptr _ -> Mem.ptr_size 218 | Tpointer _ -> Mem.ptr_size 219 | Tarray (ty, n) -> n * (sizeof ty) 220 | Tstruct (_, fields) -> 221 let sizes = List.map sizeof (List.map snd fields) in 222 snd (Mem.align 0 sizes) 223 | Tunion (_, fields) -> 224 MiscPottier.max_list (List.map sizeof (List.map snd fields)) 225 | _ -> assert false (* do not use on these arguments *) 212 let sizeof ctype = Mem.concrete_size (ClightToCminor.sizeof_ctype ctype) 226 213 227 214 let size_of_ctype = function … … 279 266 (* Interpret *) 280 267 281 let int_of_intsize = function282 | I8 -> 8283 | I16 -> 16284 | I32 -> 32285 286 let choose_cast sign ednessn m v =287 let f = match sign ednesswith268 let byte_of_intsize = function 269 | I8 -> 1 270 | I16 -> 2 271 | I32 -> 4 272 273 let choose_cast sign n m v = 274 let f = match sign with 288 275 | Signed -> Value.sign_ext 289 276 | Unsigned -> Value.zero_ext in … … 292 279 let eval_cast = function 293 280 (* Cast Integer *) 294 | (v,Tint(isize,sign edness),Tint(isize',_)) ->295 choose_cast sign edness (int_of_intsize isize) (int_of_intsize isize') v281 | (v,Tint(isize,sign),Tint(isize',_)) -> 282 choose_cast sign (byte_of_intsize isize) (byte_of_intsize isize') v 296 283 | (v,_,_) -> v 297 284 298 let eval_unop = function 299 | Onotbool -> Value.notbool 300 | Onotint -> Value.notint 301 | Oneg -> Value.negint 285 let to_int32 (v, t) = eval_cast (v, t, Tint (I32, Signed)) 286 287 let eval_unop ret_ctype ((_, t) as e) op = 288 let v = to_int32 e in 289 let v = match op with 290 | Onotbool -> Value.notbool v 291 | Onotint -> Value.notint v 292 | Oneg -> Value.negint v in 293 eval_cast (v, t, ret_ctype) 302 294 303 295 let eval_add (v1,t1) (v2,t2) = match t1, t2 with … … 316 308 | _ -> Value.sub v1 v2 317 309 318 let choose_sign ednessop_signed op_unsigned v1 v2 t =310 let choose_sign op_signed op_unsigned v1 v2 t = 319 311 let op = match t with 320 312 | Tint (_, Signed) -> op_signed … … 323 315 op v1 v2 324 316 325 let eval_binop ret_ctype ((v1,t1) as e1) ((v2,t2) as e2) op = 317 let eval_binop ret_ctype ((_, t1) as e1) ((_, t2) as e2) op = 318 let v1 = to_int32 e1 in 319 let v2 = to_int32 e2 in 320 let e1 = (v1, t1) in 321 let e2 = (v2, t2) in 326 322 let v = match op with 327 323 | Oadd -> eval_add e1 e2 328 324 | Osub -> eval_sub e1 e2 329 325 | Omul -> Value.mul v1 v2 330 | Odiv -> choose_sign ednessValue.div Value.divu v1 v2 t1331 | Omod -> choose_sign ednessValue.modulo Value.modulou v1 v2 t1326 | Odiv -> choose_sign Value.div Value.divu v1 v2 t1 327 | Omod -> choose_sign Value.modulo Value.modulou v1 v2 t1 332 328 | Oand -> Value.and_op v1 v2 333 329 | Oor -> Value.or_op v1 v2 … … 335 331 | Oshl-> Value.shl v1 v2 336 332 | Oshr-> Value.shr v1 v2 337 | Oeq -> choose_sign ednessValue.cmp_eq Value.cmp_eq_u v1 v2 t1338 | One -> choose_sign ednessValue.cmp_ne Value.cmp_ne_u v1 v2 t1339 | Olt -> choose_sign ednessValue.cmp_lt Value.cmp_lt_u v1 v2 t1340 | Ole -> choose_sign ednessValue.cmp_le Value.cmp_le_u v1 v2 t1341 | Ogt -> choose_sign ednessValue.cmp_gt Value.cmp_gt_u v1 v2 t1342 | Oge -> choose_sign ednessValue.cmp_ge Value.cmp_ge_u v1 v2 t1 in333 | Oeq -> choose_sign Value.cmp_eq Value.cmp_eq_u v1 v2 t1 334 | One -> choose_sign Value.cmp_ne Value.cmp_ne_u v1 v2 t1 335 | Olt -> choose_sign Value.cmp_lt Value.cmp_lt_u v1 v2 t1 336 | Ole -> choose_sign Value.cmp_le Value.cmp_le_u v1 v2 t1 337 | Ogt -> choose_sign Value.cmp_gt Value.cmp_gt_u v1 v2 t1 338 | Oge -> choose_sign Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in 343 339 eval_cast (v, t1, ret_ctype) 344 340 345 let rec get_offset_struct v id fields = 346 let sizes = List.map (fun (_, ty) -> sizeof ty) fields in 347 let (offsets, _) = Mem.align 0 sizes in 348 let rec select = function 349 | (x, _) :: _, off :: _ when x = id -> off 350 | _ :: fields, _ :: offsets -> select (fields, offsets) 351 | _ -> assert false (* should be impossible *) in 352 let off = Value.of_int (select (fields, offsets)) in 341 let rec get_offset_struct v size id fields = 342 let offsets = fst (Mem.concrete_offsets_size size) in 343 let fields = List.combine (List.map fst fields) offsets in 344 let off = Value.of_int (List.assoc id fields) in 353 345 Value.add v off 354 346 355 347 let get_offset v id = function 356 | Tstruct (_, fields) -> get_offset_struct v id fields 348 | Tstruct (_, fields) as t -> 349 let size = ClightToCminor.sizeof_ctype t in 350 get_offset_struct v size id fields 357 351 | Tunion _ -> v 358 352 | _ -> assert false (* do not use on these arguments *) … … 390 384 ((eval_binop tt v1 v2 op,tt),l1@l2) 391 385 | Eunop (op,exp) -> 392 let ( (v1,_),l1) = eval_expr localenv m exp in393 ((eval_unop op v1,tt),l1)386 let (e1,l1) = eval_expr localenv m exp in 387 ((eval_unop tt e1 op,tt),l1) 394 388 | Econdition (e1,e2,e3) -> 395 389 let (v1,l1) = eval_expr localenv m e1 in … … 554 548 let interpret_external k mem f args = 555 549 let (mem', v) = match InterpretExternal.t mem f args with 556 | (mem', InterpretExternal.V v) -> (mem', v) 550 | (mem', InterpretExternal.V vs) -> 551 let v = if List.length vs = 0 then Value.undef else List.hd vs in 552 (mem', v) 557 553 | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in 558 554 Returnstate (v, k, mem') … … 583 579 | Init_float32 f -> error_float () 584 580 | Init_float64 f -> error_float () 585 | Init_space i -> Data_reserve i581 | Init_space i -> error "bad global initialization style." 586 582 | Init_addrof (x,off) -> assert false (* TODO: need the size of [x]'s cells *) 583 584 let datas_of_init_datas = function 585 | [Init_space _] -> None 586 | l -> Some (List.map data_of_init_data l) 587 587 588 588 let init_mem prog = 589 589 let f_var mem ((x, init_datas), ty) = 590 Mem.add_var mem x (List.map data_of_init_data init_datas) in 590 Mem.add_var mem x (ClightToCminor.sizeof_ctype ty) 591 (datas_of_init_datas init_datas) in 591 592 let mem = List.fold_left f_var Mem.empty prog.prog_vars in 592 593 let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in … … 594 595 595 596 let compute_result v = 596 if Value.is_int v then IntValue.Int 8.cast (Value.to_int_repr v)597 else IntValue.Int 8.zero597 if Value.is_int v then IntValue.Int32.cast (Value.to_int_repr v) 598 else IntValue.Int32.zero 598 599 599 600 let rec exec debug trace (state, l) = … … 601 602 let print_and_return_result res = 602 603 if debug then Printf.printf "Result = %s\n%!" 603 (IntValue.Int 8.to_string res) ;604 (IntValue.Int32.to_string res) ; 604 605 (res, cost_labels) in 605 606 if debug then print_state state ; … … 608 609 print_and_return_result (compute_result v) 609 610 | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *) 610 print_and_return_result IntValue.Int 8.zero611 print_and_return_result IntValue.Int32.zero 611 612 | state -> exec debug cost_labels (step state) 612 613 613 614 let interpret debug prog = 614 if debug then Printf.printf "*** Clight ***\n\n%!" ;615 Printf.printf "*** Clight interpret ***\n%!" ; 615 616 match prog.prog_main with 616 | None -> (IntValue.Int 8.zero, [])617 | None -> (IntValue.Int32.zero, []) 617 618 | Some main -> 618 619 let mem = init_mem prog in -
Deliverables/D2.2/8051/src/clight/clightLabelling.ml
r796 r818 17 17 18 18 19 let int_type = Tint (I32, Signed)19 let int_type = Tint (I32, AST.Signed) 20 20 let const_int i = Expr (Econst_int i, int_type) 21 21 … … 105 105 (Swhile (add_cost_labels_e cost_universe e, s')) 106 106 | Sdowhile (e,s) -> 107 let s' = add_cost_labels_st cost_universe s in 108 let s' = add_starting_cost_label cost_universe s' in 107 let s1 = add_cost_labels_st cost_universe s in 108 let s2 = add_cost_labels_st cost_universe s in 109 let s2' = add_starting_cost_label cost_universe s2 in 109 110 add_ending_cost_label cost_universe 110 (S dowhile (add_cost_labels_e cost_universe e, s'))111 (Ssequence (s1, Swhile (add_cost_labels_e cost_universe e, s2'))) 111 112 | Sfor (s1,e,s2,s3) -> 112 113 let s1' = add_cost_labels_st cost_universe s1 in -
Deliverables/D2.2/8051/src/clight/clightParser.ml
r740 r818 42 42 | None -> failwith "Error during C to Clight pass." 43 43 | Some(pp) -> pp 44 ) 44 ) -
Deliverables/D2.2/8051/src/clight/clightPrinter.ml
r486 r818 541 541 flush_str_formatter () 542 542 543 let print_ctype_prot = name_type 544 545 let print_ctype_def = function 546 | Tstruct (name, fld) | Tunion (name, fld) -> 547 let f_fld s (id, t) = s ^ " " ^ (print_ctype_prot t) ^ " " ^ id ^ ";\n" in 548 let s_fld = List.fold_left f_fld "" in 549 name ^ " {\n" ^ (s_fld fld) ^ "};\n" 550 | _ -> "" (* no definition associated to the other types *) -
Deliverables/D2.2/8051/src/clight/clightPrinter.mli
r486 r818 4 4 val print_program: Clight.program -> string 5 5 6 val print_expression 6 val print_expression: Clight.expr -> string 7 7 8 8 val string_of_ctype: Clight.ctype -> string 9 9 10 10 val print_statement: Clight.statement -> string 11 12 val print_ctype_prot: Clight.ctype -> string 13 14 val print_ctype_def: Clight.ctype -> string -
Deliverables/D2.2/8051/src/clight/clightToCminor.ml
r740 r818 1 open AST 2 open Cminor 3 open Clight 4 5 6 let error_prefix = "Cminor to RTLabs" 1 2 3 let error_prefix = "Clight to Cminor" 7 4 let error = Error.global_error error_prefix 8 5 let error_float () = error "float not supported." 9 6 10 7 11 (*For internal use*) 12 type var_type = 8 (* General helpers *) 9 10 let clight_type_of (Clight.Expr (_, t)) = t 11 12 let cminor_type_of (Cminor.Expr (_, t)) = t 13 14 15 (* Translate types *) 16 17 let byte_size_of_intsize = function 18 | Clight.I8 -> 1 19 | Clight.I16 -> 2 20 | Clight.I32 -> 4 21 22 let sig_type_of_ctype = function 23 | Clight.Tvoid -> assert false (* do not use on this argument *) 24 | Clight.Tint (intsize, sign) -> 25 AST.Sig_int (byte_size_of_intsize intsize, sign) 26 | Clight.Tfloat _ -> error_float () 27 | Clight.Tfunction _ | Clight.Tstruct _ | Clight.Tunion _ 28 | Clight.Tpointer _ | Clight.Tarray _ | Clight.Tcomp_ptr _ -> AST.Sig_ptr 29 30 let translate_args_types = List.map sig_type_of_ctype 31 32 let type_return_of_ctype = function 33 | Clight.Tvoid -> AST.Type_void 34 | t -> AST.Type_ret (sig_type_of_ctype t) 35 36 let quantity_of_sig_type = function 37 | AST.Sig_int (size, _) -> AST.QInt size 38 | AST.Sig_float _ -> error_float () 39 | AST.Sig_offset -> AST.QOffset 40 | AST.Sig_ptr -> AST.QPtr 41 42 let quantity_of_ctype t = quantity_of_sig_type (sig_type_of_ctype t) 43 44 let rec sizeof_ctype = function 45 | Clight.Tvoid | Clight.Tfunction _ -> AST.SQ (AST.QInt 1) 46 | Clight.Tfloat _ -> error_float () 47 | Clight.Tint (size, _) -> AST.SQ (AST.QInt (byte_size_of_intsize size)) 48 | Clight.Tpointer _ 49 | Clight.Tcomp_ptr _ -> AST.SQ AST.QPtr 50 | Clight.Tarray (t, n) -> AST.SArray (n, sizeof_ctype t) 51 | Clight.Tstruct (_, fields) -> 52 AST.SProd (List.map sizeof_ctype (List.map snd fields)) 53 | Clight.Tunion (_, fields) -> 54 AST.SSum (List.map sizeof_ctype (List.map snd fields)) 55 56 let global_size_of_ctype = sizeof_ctype 57 58 59 (** Helpers on abstract sizes and offsets *) 60 61 let max_stacksize size1 size2 = match size1, size2 with 62 | AST.SProd l1, AST.SProd l2 when List.length l1 > List.length l2 -> size1 63 | AST.SProd l1, AST.SProd l2 -> size2 64 | _ -> raise (Failure "ClightToCminor.max_stacksize") 65 66 (** Hypothesis: [offset1] is a prefix of [offset2] or vice-versa. *) 67 let max_offset offset1 offset2 = 68 if List.length offset1 > List.length offset2 then offset1 69 else offset2 70 71 let next_depth = function 72 | AST.SProd l -> List.length l 73 | _ -> raise (Failure "ClightToCminor.next_offset") 74 75 let add_stack offset = 76 let e1 = Cminor.Expr (Cminor.Cst AST.Cst_stack, AST.Sig_ptr) in 77 let e2 = Cminor.Expr (Cminor.Cst (AST.Cst_offset offset), AST.Sig_offset) in 78 Cminor.Op2 (AST.Op_addp, e1, e2) 79 80 let add_stacksize t = function 81 | AST.SProd l -> AST.SProd (l @ [sizeof_ctype t]) 82 | _ -> raise (Failure "ClightToCminor.add_stacksize") 83 84 let struct_depth field fields = 85 let rec aux i = function 86 | [] -> error ("unknown field " ^ field ^ ".") 87 | (field', t) :: _ when field' = field -> i 88 | (_, t) :: fields -> aux (i+1) fields in 89 aux 0 fields 90 91 let struct_offset t field fields = 92 let size = sizeof_ctype t in 93 let depth = struct_depth field fields in 94 let offset = (size, depth) in 95 let t = AST.Sig_offset in 96 Cminor.Expr (Cminor.Cst (AST.Cst_offset offset), t) 97 98 99 (** Sort variables: locals, parameters, globals, in stack. *) 100 101 type location = 102 | Local 103 | LocalStack of AST.abstract_offset 104 | Param 105 | ParamStack of AST.abstract_offset 13 106 | Global 14 | Stack of int (*Note: this is a constraint on the size of the stack.*) 15 | Param 16 | Local 17 18 (*Parametrisation by int and pointer size *) 19 let int_size = Driver.CminorMemory.int_size 20 let ptr_size = Driver.CminorMemory.ptr_size 21 let alignment = Driver.CminorMemory.alignment 22 23 let fresh_tmp variables = 24 let rec ft i = 25 let tmp = "tmp"^(string_of_int i) in 26 try (match Hashtbl.find variables tmp with _ -> ft (i+1)) 27 with Not_found -> tmp 28 in ft 0 29 30 let rec ctype_to_type_return t = match t with 31 | Tvoid -> Type_void 32 | Tfloat _ -> Type_ret Sig_float (*Not supported*) 33 | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_) -> Type_ret Sig_ptr 34 | _ -> Type_ret Sig_int 35 36 let rec ctype_to_sig_type t = match t with 37 | Tfloat _ -> 38 Sig_float (*Not supported but needed for external function from library*) 39 | Tvoid -> assert false 40 | Tpointer _ | Tstruct (_,_) | Tunion (_,_) | Tarray(_,_) -> Sig_ptr 41 | _ -> Sig_int 42 43 let rec size_of_ty = function 44 | Tvoid -> assert false 45 | Tfloat _ -> assert false (*Not supported*) 46 | Tfunction (_,_) -> assert false (*Not supported*) 47 | Tint (I8,Signed) -> 1 48 | Tint (I8,Unsigned) -> 1 49 | Tint (I16,Signed) -> 2 50 | Tint (I16,Unsigned) -> 2 51 (*FIXME MQ_int32 : signed or unsigned ? *) 52 | Tint (I32,Signed) -> 4 53 | Tint (I32,Unsigned) -> 4 54 | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_) 55 | Tcomp_ptr _ -> ptr_size 56 57 let size_of_intsize = function 58 | I8 -> 1 59 | I16 -> 2 60 | I32 -> 4 61 62 let quantity_of_ty = function 63 | Tvoid -> assert false (* do not use on this argument *) 64 | Tint (size,_) -> Memory.QInt (size_of_intsize size) 65 | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_) 66 | Tfunction (_,_) 67 | Tcomp_ptr _ -> Memory.QPtr 68 | Tfloat _ -> error_float () 69 70 let init_to_data l = List.map ( 107 108 (** Below are some helper definitions to ease the manipulation of a translation 109 environment for variables. *) 110 111 type var_locations = (location * Clight.ctype) StringTools.Map.t 112 113 let empty_var_locs : var_locations = StringTools.Map.empty 114 115 let add_var_locs : AST.ident -> (location * Clight.ctype) -> var_locations -> 116 var_locations = 117 StringTools.Map.add 118 119 let mem_var_locs : AST.ident -> var_locations -> bool = StringTools.Map.mem 120 121 let find_var_locs : AST.ident -> var_locations -> (location * Clight.ctype) = 122 StringTools.Map.find 123 124 let fold_var_locs : (AST.ident -> (location * Clight.ctype) -> 'a -> 'a) -> 125 var_locations -> 'a -> 'a = 126 StringTools.Map.fold 127 128 129 let is_local_or_param id var_locs = match find_var_locs id var_locs with 130 | (Local, _) | (Param, _) -> true 131 | _ -> false 132 133 let get_locals var_locs = 134 let f id (location, ctype) locals = 135 let added = match location with 136 | Local -> [(id, sig_type_of_ctype ctype)] 137 | _ -> [] in 138 locals @ added in 139 fold_var_locs f var_locs [] 140 141 let get_stacksize var_locs = 142 let f _ (location, _) res = match location with 143 | LocalStack (stacksize, _) | ParamStack (stacksize, _) -> 144 max_stacksize res stacksize 145 | _ -> res in 146 fold_var_locs f var_locs (AST.SProd []) 147 148 149 (* Variables of a function that will go in stack: variables of a complex type 150 (array, structure or union) and variables whose address is evaluated. *) 151 152 let is_function_ctype = function 153 | Clight.Tfunction _ -> true 154 | _ -> false 155 156 let is_scalar_ctype : Clight.ctype -> bool = function 157 | Clight.Tint _ | Clight.Tfloat _ | Clight.Tpointer _ -> true 158 | _ -> false 159 160 let is_complex_ctype : Clight.ctype -> bool = function 161 | Clight.Tarray _ | Clight.Tstruct _ | Clight.Tunion _ | Clight.Tfunction _ -> 162 true 163 | _ -> false 164 165 let complex_ctype_vars cfun = 166 let f set (x, t) = 167 if is_complex_ctype t then StringTools.Set.add x set else set in 168 (* Because of CIL, parameters should not have a complex type, but let's add 169 them just in case. *) 170 List.fold_left f StringTools.Set.empty 171 (cfun.Clight.fn_params @ cfun.Clight.fn_vars) 172 173 let union_list = List.fold_left StringTools.Set.union StringTools.Set.empty 174 175 let f_expr (Clight.Expr (ed, _)) sub_exprs_res = 176 let res_ed = match ed with 177 | Clight.Eaddrof (Clight.Expr (Clight.Evar id, _)) -> 178 StringTools.Set.singleton id 179 | _ -> StringTools.Set.empty in 180 union_list (res_ed :: sub_exprs_res) 181 182 let f_stmt _ sub_exprs_res sub_stmts_res = 183 union_list (sub_exprs_res @ sub_stmts_res) 184 185 let addr_vars_fun cfun = ClightFold.statement2 f_expr f_stmt cfun.Clight.fn_body 186 187 let stack_vars cfun = 188 StringTools.Set.union (complex_ctype_vars cfun) (addr_vars_fun cfun) 189 190 191 let sort_stacks stack_location vars var_locs = 192 let stacksize = get_stacksize var_locs in 193 let f (current_stacksize, var_locs) (id, t) = 194 let depth = next_depth current_stacksize in 195 let current_stacksize = add_stacksize t current_stacksize in 196 let offset = (current_stacksize, depth) in 197 let var_locs = add_var_locs id (stack_location offset, t) var_locs in 198 (current_stacksize, var_locs) in 199 snd (List.fold_left f (stacksize, var_locs) vars) 200 201 let sort_normals normal_location vars var_locs = 202 let f var_locs (id, ctype) = 203 add_var_locs id (normal_location, ctype) var_locs in 204 List.fold_left f var_locs vars 205 206 let sort_vars normal_location stack_location_opt stack_vars vars var_locs = 207 let f_stack (x, _) = StringTools.Set.mem x stack_vars in 208 let (f_normal, var_locs) = match stack_location_opt with 209 | None -> ((fun _ -> true), var_locs) 210 | Some stack_location -> 211 ((fun var -> not (f_stack var)), 212 sort_stacks stack_location (List.filter f_stack vars) var_locs) in 213 sort_normals normal_location (List.filter f_normal vars) var_locs 214 215 let sort_locals = sort_vars Local (Some (fun offset -> LocalStack offset)) 216 217 let sort_params = sort_vars Param (Some (fun offset -> ParamStack offset)) 218 219 let sort_globals stack_vars globals var_locs = 220 let globals = List.map (fun ((id, _), ctype) -> (id, ctype)) globals in 221 sort_vars Global None stack_vars globals var_locs 222 223 (* The order of insertion in the sorting environment is important: it follows 224 the scope conventions of C. Local variables hide parameters that hide 225 globals. *) 226 227 let sort_variables globals cfun = 228 let stack_vars = stack_vars cfun in 229 let var_locs = empty_var_locs in 230 let var_locs = sort_globals stack_vars globals var_locs in 231 let var_locs = sort_params stack_vars cfun.Clight.fn_params var_locs in 232 let var_locs = sort_locals stack_vars cfun.Clight.fn_vars var_locs in 233 var_locs 234 235 236 (* Translate globals *) 237 238 let init_to_data = function 239 | [Clight.Init_space _] -> None 240 | l -> Some (List.map ( 71 241 function 72 | Init_int8 i -> Data_int8 i 73 | Init_int16 i -> Data_int16 i 74 | Init_int32 i -> Data_int32 i 75 | Init_float32 _ 76 | Init_float64 _ -> assert false (*Not supported*) 77 | Init_space n -> Data_reserve n 78 | Init_addrof (_,_) -> assert false (*TODO*) 79 ) l 80 81 let rec size_of_ctype t = match t with 82 | Tvoid -> 0 83 | Tint (I8,_) -> 1 84 | Tint (I16,_) -> 2 85 | Tint (I32,_) -> 4 86 | Tpointer _ -> ptr_size 87 | Tarray (c,s) -> s*(size_of_ctype c) 88 | Tstruct (_,lst) -> 89 List.fold_left 90 (fun n (_,ty) -> n+(size_of_ctype ty)) 0 lst 91 | Tunion (_,lst) -> 92 List.fold_left 93 (fun n (_,ty) -> 94 let sz = (size_of_ctype ty) in (if n>sz then n else sz) 95 ) 0 lst 96 | Tfloat _ | Tfunction (_,_) -> assert false (*Not supported*) 97 | Tcomp_ptr _ -> ptr_size 98 99 let translate_global_vars ((id,lst),_) = (id,init_to_data lst) 100 101 let translate_unop t = function 102 | Onotbool -> Op_notbool 103 | Onotint -> Op_notint 104 | Oneg -> (match t with 105 | Tint (_,_) -> Op_negint 106 | Tfloat _ -> assert false (*Not supported*) 107 | _ -> assert false (*Type error*) 108 ) 109 110 let translate_cmp t1 t2 cmp = 111 match (t1,t2) with 112 | (Tint(_,Signed),Tint(_,Signed)) -> Op_cmp cmp 113 | (Tint(_,Unsigned),Tint(_,Unsigned)) -> Op_cmpu cmp 114 | (Tpointer _,Tpointer _) -> Op_cmpp cmp 115 | _ -> Op_cmp cmp 116 117 let translate_add e1 e2 = function 118 | (Tint(_,_),Tint(_,_)) -> Op2 (Op_add,e1,e2) 119 | (Tfloat _,Tfloat _) -> assert false (*Not supported*) 120 | (Tpointer t,Tint(_,_)) -> 121 Op2 (Op_addp,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t)))) 122 | (Tint(_,_),Tpointer t) -> 123 Op2 (Op_addp,e2,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t)))) 124 | (Tarray (t,_),Tint(_,_)) -> 125 Op2 (Op_addp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t))))) 126 | (Tint(_,_),Tarray(t,_)) -> 127 Op2 (Op_addp,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t))))) 128 | _ -> assert false (*Type error*) 129 130 let translate_sub e1 e2 = function 131 | (Tint(_,_),Tint(_,_)) -> Op2 (Op_sub,e1,e2) 132 | (Tfloat _,Tfloat _) -> assert false (*Not supported*) 133 | (Tpointer t,Tint(_,_)) -> 134 Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t))))) 135 | (Tarray (t,_),Tint(_,_)) -> 136 Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t))))) 137 | _ -> assert false (*Type error*) 138 139 let translate_mul e1 e2 = function 140 | (Tint(_,_),Tint(_,_)) -> Op2 (Op_mul,e1,e2) 141 | (Tfloat _,Tfloat _) -> assert false (*Not supported*) 142 | _ -> assert false (*Type error*) 143 144 let translate_div e1 e2 = function 145 | (Tint(_,Signed),Tint(_,Signed)) -> Op2 (Op_div,e1,e2) 146 | (Tint(_,Unsigned),Tint(_,Unsigned)) -> Op2 (Op_divu,e1,e2) 147 | (Tfloat _,Tfloat _) -> assert false (*Not supported*) 148 | _ -> assert false (*Type error*) 149 150 let translate_binop t1 e1 t2 e2 = function 151 | Oadd -> translate_add e1 e2 (t1,t2) 152 | Osub -> translate_sub e1 e2 (t1,t2) 153 | Omul -> translate_mul e1 e2 (t1,t2) 154 | Odiv -> translate_div e1 e2 (t1,t2) 155 | Omod -> Op2 (Op_mod,e1,e2) 156 | Oand -> Op2 (Op_and,e1,e2) 157 | Oor -> Op2 (Op_or,e1,e2) 158 | Oxor -> Op2 (Op_xor,e1,e2) 159 | Oshl -> Op2 (Op_shl,e1,e2) 160 | Oshr -> Op2 (Op_shr,e1,e2) 161 | Oeq -> Op2 (translate_cmp t1 t2 Cmp_eq,e1,e2) 162 | One -> Op2 (translate_cmp t1 t2 Cmp_ne,e1,e2) 163 | Olt -> Op2 (translate_cmp t1 t2 Cmp_lt,e1,e2) 164 | Ogt -> Op2 (translate_cmp t1 t2 Cmp_gt,e1,e2) 165 | Ole -> Op2 (translate_cmp t1 t2 Cmp_le,e1,e2) 166 | Oge -> Op2 (translate_cmp t1 t2 Cmp_ge,e1,e2) 167 168 let make_cast e = function 169 | (Tint(I8,Signed),Tint(_,_)) -> Op1 (Op_cast8signed,e) 170 | (Tint(I8,Unsigned),Tint(_,_)) -> Op1 (Op_cast8unsigned,e) 171 | (Tint(I16,Signed),Tint(_,_)) -> Op1 (Op_cast16signed,e) 172 | (Tint(I16,Unsigned),Tint(_,_)) -> Op1 (Op_cast16unsigned,e) 173 | _ -> e 174 175 let get_type (Expr (_,t)) = t 176 177 let rec get_offset_struct e id = function 178 | [] -> assert false (*Wrong id*) 179 | (fi,_)::_ when fi=id -> e 180 | (_,ty)::ll -> get_offset_struct (e+(size_of_ctype ty)) id ll 181 182 let is_struct = function 183 | Tarray(_,_) | Tstruct (_,_) | Tunion(_,_) -> true 242 | Clight.Init_int8 i -> AST.Data_int8 i 243 | Clight.Init_int16 i -> AST.Data_int16 i 244 | Clight.Init_int32 i -> AST.Data_int32 i 245 | Clight.Init_float32 _ 246 | Clight.Init_float64 _ -> error_float () 247 | Clight.Init_space n -> error "bad global initialization style." 248 | Clight.Init_addrof (_,_) -> assert false (*TODO*) 249 ) l) 250 251 let translate_global ((id,lst),t) = (id,global_size_of_ctype t,init_to_data lst) 252 253 254 (* Translate expression *) 255 256 let translate_unop = function 257 | Clight.Onotbool -> AST.Op_notbool 258 | Clight.Onotint -> AST.Op_notint 259 | Clight.Oneg -> AST.Op_negint 260 261 let esizeof_ctype res_type t = 262 Cminor.Expr (Cminor.Cst (AST.Cst_sizeof (sizeof_ctype t)), res_type) 263 264 let translate_add res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with 265 | Clight.Tint _, Clight.Tint _ -> 266 Cminor.Expr (Cminor.Op2 (AST.Op_add, e1, e2), res_type) 267 | Clight.Tfloat _, Clight.Tfloat _ -> error_float () 268 | Clight.Tpointer t, Clight.Tint _ 269 | Clight.Tarray (t, _), Clight.Tint _ -> 270 let t2 = cminor_type_of e2 in 271 let size = esizeof_ctype t2 t in 272 let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in 273 Cminor.Expr (Cminor.Op2 (AST.Op_addp, e1, index), res_type) 274 | Clight.Tint _, Clight.Tpointer t 275 | Clight.Tint _, Clight.Tarray (t, _) -> 276 let t1 = cminor_type_of e1 in 277 let size = esizeof_ctype t1 t in 278 let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e1, size), t1) in 279 Cminor.Expr (Cminor.Op2 (AST.Op_addp, e2, index), res_type) 280 | _ -> error "type error." 281 282 let translate_sub res_type ctype1 ctype2 e1 e2 = match ctype1, ctype2 with 283 | Clight.Tint _, Clight.Tint _ -> 284 Cminor.Expr (Cminor.Op2 (AST.Op_sub, e1, e2), res_type) 285 | Clight.Tfloat _, Clight.Tfloat _ -> error_float () 286 | Clight.Tpointer t, Clight.Tint _ 287 | Clight.Tarray (t, _), Clight.Tint _ -> 288 let t2 = cminor_type_of e2 in 289 let size = esizeof_ctype t2 t in 290 let index = Cminor.Expr (Cminor.Op2 (AST.Op_mul, e2, size), t2) in 291 Cminor.Expr (Cminor.Op2 (AST.Op_subp, e1, index), res_type) 292 | Clight.Tpointer _, Clight.Tpointer _ 293 | Clight.Tarray _, Clight.Tpointer _ 294 | Clight.Tpointer _, Clight.Tarray _ 295 | Clight.Tarray _, Clight.Tarray _ -> 296 Cminor.Expr (Cminor.Op2 (AST.Op_subpp, e1, e2), res_type) 297 | _ -> error "type error." 298 299 let is_signed = function 300 | Clight.Tint (_, AST.Signed) -> true 184 301 | _ -> false 185 302 186 let is_ptr_to_struct = function 187 | Tpointer t when is_struct t -> true 188 | _ -> false 189 190 let is_function = function 191 | Tfunction _ -> true 303 let is_pointer = function 304 | Clight.Tpointer _ | Clight.Tarray _ -> true 192 305 | _ -> false 193 306 194 let rec translate_expr variables expr = 195 let Expr(d,c) = expr in match d with 196 | Econst_int i -> Cst (Cst_int i) 197 | Econst_float f -> assert false (*Not supported*) 198 | Evar id when is_function c -> Cst (Cst_addrsymbol id) 199 | Evar id -> 200 (try (match Hashtbl.find variables id with 201 | (Local,_) -> Id id 202 | (Stack o,ty) when is_struct ty -> Cst (Cst_stackoffset o) 203 | (Stack o,_) -> 204 Mem (quantity_of_ty c,Cst (Cst_stackoffset o)) 205 | (Param,_) -> Id id 206 | (Global,ty) when is_struct ty -> Cst (Cst_addrsymbol id) 207 | (Global,_) -> 208 Mem (quantity_of_ty c,Cst (Cst_addrsymbol id)) 209 ) with Not_found -> assert false) 210 | Ederef e when is_ptr_to_struct (get_type e) -> 211 translate_expr variables e 212 | Ederef e -> Mem (quantity_of_ty c,translate_expr variables e) 213 | Eaddrof se -> ( 214 match se with 215 | Expr(Evar id,_) -> 216 (try (match Hashtbl.find variables id with 217 | (Local,_) -> assert false (*Impossible: see sort_variables*) 218 | (Stack o,_) -> Cst (Cst_stackoffset o) 219 | (Param,_) -> Cst (Cst_addrsymbol id) 220 | (Global,_) -> Cst (Cst_addrsymbol id) 221 ) with Not_found -> assert false) 222 | Expr(Ederef ee,_) -> 223 translate_expr variables ee 224 | Expr(Efield (str,fi),_) -> 225 (match str with 226 | Expr(_,Tstruct(_,b)) -> 227 Op2 (Op_add 228 ,translate_expr variables str 229 ,Cst (Cst_int (get_offset_struct 0 fi b))) 230 | Expr(_,Tunion(_,_)) -> 231 translate_expr variables str 232 | _ -> assert false (*Type Error*) 233 ) 234 | _ -> assert false (*Must be a lvalue*) 235 ) 236 | Eunop (op,e) -> 237 Op1 (translate_unop (get_type e) op ,translate_expr variables e) 238 | Ebinop (op,e1,e2) -> 239 translate_binop 240 (get_type e1) (translate_expr variables e1) 241 (get_type e2) (translate_expr variables e2) op 242 | Ecast (ty,e) -> make_cast (translate_expr variables e) (get_type e,ty) 243 | Econdition (e1,e2,e3) -> 244 Cond (translate_expr variables e1, 245 translate_expr variables e2, 246 translate_expr variables e3) 247 | Eandbool (e1,e2) -> 248 Cond ( 249 translate_expr variables e1, 250 Cond(translate_expr variables e2,Cst (Cst_int 1),Cst (Cst_int 0)), 251 Cst (Cst_int 0)) 252 | Eorbool (e1,e2) -> 253 Cond ( 254 translate_expr variables e1, 255 Cst (Cst_int 1), 256 Cond(translate_expr variables e2, Cst (Cst_int 1),Cst (Cst_int 0)) ) 257 | Esizeof cc -> Cst (Cst_int (size_of_ctype cc)) 258 | Efield (e,id) -> 259 (match get_type e with 260 | Tstruct(_,lst) -> 261 (try 262 Mem (quantity_of_ty (List.assoc id lst) 263 ,Op2(Op_add 264 ,translate_expr variables e 265 , Cst (Cst_int (get_offset_struct 0 id lst)) 266 ) 267 ) 268 with Not_found -> assert false (*field does not exists*) 269 ) 270 | Tunion(_,lst) -> 271 (try 272 Mem (quantity_of_ty (List.assoc id lst), translate_expr variables e) 273 with Not_found -> assert false (*field does not exists*) 274 ) 275 | _ -> assert false (*Type error*) 276 ) 277 | Ecost (lbl,e) -> Exp_cost (lbl,translate_expr variables e) 278 | Ecall _ -> assert false (* Only for annotations *) 279 280 let translate_assign variables e = function 281 | Expr (Evar v,t) -> 282 (try (match Hashtbl.find variables v with 283 | (Local,_) -> St_assign (v,translate_expr variables e) 284 | (Stack o,_) -> St_store (quantity_of_ty t 285 ,Cst (Cst_stackoffset o) 286 ,translate_expr variables e) 287 | (Param,_) -> St_assign (v,translate_expr variables e) 288 | (Global,_) -> St_store (quantity_of_ty t 289 ,Cst (Cst_addrsymbol v) 290 ,translate_expr variables e) 291 ) with Not_found -> assert false) 292 | Expr (Ederef ee,t) -> St_store (quantity_of_ty t 293 ,translate_expr variables ee 294 ,translate_expr variables e) 295 | Expr (Efield (ee,id),t) -> 296 (match ee with 297 | Expr (_,Tstruct(_,lst)) -> 298 St_store (quantity_of_ty t 299 ,Op2(Op_add,translate_expr variables ee 300 ,Cst(Cst_int (get_offset_struct 0 id lst ))) 301 ,translate_expr variables e) 302 | Expr (_,Tunion(_,_)) -> St_store (quantity_of_ty t 303 ,translate_expr variables ee 304 ,translate_expr variables e) 305 | _ -> assert false (*Type error*) 306 ) 307 | _ -> assert false (*lvalue error*) 308 309 let translate_call_name variables = function 310 | Expr (Evar id,_) -> Cst (Cst_addrsymbol id) 311 | _ -> assert false (*Not supported*) 312 313 let translate_call variables e1 e2 lst = 314 let st_call f_assign f_res = 315 St_call (f_assign 316 ,translate_expr variables e2 317 ,List.map (translate_expr variables) lst 318 ,{args=List.map (fun exp -> 319 let Expr(_,t) = exp in ctype_to_sig_type t 320 )lst;res=f_res} 321 ) in 322 match e1 with 323 | Some (Expr (se,tt)) -> ( 324 match se with 325 | Evar v -> 326 (try (match Hashtbl.find variables v with 327 | (Local,_) | (Param,_) -> 328 st_call (Some v) (Type_ret (ctype_to_sig_type tt)) 329 | (Stack o,_) -> 330 let tmp = fresh_tmp variables in 331 St_seq ( 332 st_call (Some tmp) (Type_ret (ctype_to_sig_type tt)) 333 ,St_store (quantity_of_ty tt,Cst (Cst_stackoffset o),Id tmp) 334 ) 335 | (Global,_) -> 336 let tmp = fresh_tmp variables in 337 St_seq ( 338 st_call (Some tmp) (Type_ret (ctype_to_sig_type tt)) 339 ,St_store (quantity_of_ty tt,Cst (Cst_addrsymbol v),Id tmp) 340 ) 341 ) with Not_found -> assert false ) 342 | Ederef ee -> assert false (*Not supported*) 343 | Efield (ee,id) -> assert false (*Not supported*) 344 | _ -> assert false (*Should be a lvalue*) 345 ) 346 | None -> st_call None Type_void 347 348 (*TODO rewrite this buggy function*) 349 let translate_switch expr (cases,default) = 350 let sz = List.length cases in 351 let sw = St_block (St_switch ( 352 expr, MiscPottier.mapi (fun i (n,_) -> (n,i)) cases, sz)) in 353 let rec add_block n e = function 354 | [] -> St_block (St_seq(e,default)) 355 | (_,st)::l -> 356 add_block (n-1) (St_block (St_seq(e,St_seq(st,St_exit n)))) l 357 in add_block sz sw cases 358 359 let rec translate_stmt variables = function 360 | Sskip -> St_skip 361 | Sassign (e1,e2) -> translate_assign variables e2 e1 362 | Scall (e1,e2,lst) -> translate_call variables e1 e2 lst 363 | Ssequence (s1,s2) -> 364 St_seq (translate_stmt variables s1, 365 translate_stmt variables s2) 366 | Sifthenelse (e,s1,s2) -> 367 St_ifthenelse (translate_expr variables e, 368 translate_stmt variables s1, 369 translate_stmt variables s2) 370 | Swhile (e,s) -> 371 St_block(St_loop(St_seq ( 372 St_ifthenelse ( 373 Op1 (Op_notbool,translate_expr variables e), 374 St_exit 0,St_skip), 375 St_block (translate_stmt variables s) 376 ))) 377 | Sdowhile (e,s) -> 378 St_block(St_loop(St_seq ( 379 St_block (translate_stmt variables s), 380 St_ifthenelse ( 381 Op1(Op_notbool, translate_expr variables e), 382 St_exit 0,St_skip) 383 ))) 384 | Sfor (s1,e,s2,s3) -> 385 let b = St_block (St_loop (St_seq ( 386 St_ifthenelse ( 387 Op1(Op_notbool,translate_expr variables e), 388 St_exit 0,St_skip), 389 St_seq (St_block (translate_stmt variables s3), 390 translate_stmt variables s2 391 )))) in 392 (match (translate_stmt variables s1) with 393 | St_skip -> b | ss -> St_seq (ss,b)) 394 | Sbreak -> St_exit(1) 395 | Scontinue -> St_exit(0) 396 | Sreturn (Some e) -> St_return (Some(translate_expr variables e)) 397 | Sreturn None -> St_return None 398 | Sswitch (e,lbl) -> 399 translate_switch (translate_expr variables e) (compute_lbl variables lbl) 400 | Slabel (lbl,st) -> 401 St_label(lbl,translate_stmt variables st) 402 | Sgoto lbl -> St_goto lbl 403 | Scost (lbl,s) -> St_cost(lbl,translate_stmt variables s) 404 405 and compute_lbl variables = function 406 | LSdefault s -> ([],translate_stmt variables s) 407 | LScase (i,s,l) -> 408 let (ll,def) = (compute_lbl variables l) in 409 ((i,translate_stmt variables s)::ll,def) 410 411 let rec get_stack_vars_expr (Expr (exp,_)) = match exp with 412 | Econst_int _ | Evar _ | Esizeof _ -> [] 413 | Ederef e -> (get_stack_vars_expr e) 414 | Eaddrof Expr(e,_) -> ( 415 match e with 416 | Evar id -> [id] 417 | Ederef ee | Efield (ee,_) -> (get_stack_vars_expr ee) 418 | _ -> assert false (*Should be a lvalue*) 419 ) 420 | Eunop (_,e) -> (get_stack_vars_expr e) 421 | Ebinop (_,e1,e2) -> (get_stack_vars_expr e1)@(get_stack_vars_expr e2) 422 | Ecast (_,e) -> (get_stack_vars_expr e) 423 | Econdition (e1,e2,e3) -> 424 (get_stack_vars_expr e1)@(get_stack_vars_expr e2) 425 @(get_stack_vars_expr e3) 426 | Eandbool (e1,e2) -> (get_stack_vars_expr e1)@(get_stack_vars_expr e2) 427 | Eorbool (e1,e2) -> (get_stack_vars_expr e1)@(get_stack_vars_expr e2) 428 | Ecost (_,e) -> (get_stack_vars_expr e) 429 | Efield (e,_) -> (get_stack_vars_expr e) 430 | Econst_float _ -> assert false (*Not supported*) 431 | Ecall _ -> assert false (* Should not happen *) 432