Changeset 740 for Deliverables/D2.2
- Timestamp:
- Apr 4, 2011, 5:18:15 PM (9 years ago)
- Location:
- Deliverables/D2.2/8051/src
- Files:
-
- 50 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml
r631 r740 1986 1986 1987 1987 let interpret print_result p = 1988 if print_result then Printf.printf "8051: %!" ; 1988 1989 if p.ASM.has_main then 1989 1990 let st = load_program p in … … 1993 1994 let res = result st in 1994 1995 if print_result then 1995 Printf.printf " 8051:%s\n%!" (IntValue.Int8.to_string res) ;1996 Printf.printf "%s\n%!" (IntValue.Int8.to_string res) ; 1996 1997 (res, List.rev !trace) 1997 1998 else (IntValue.Int8.zero, []) -
Deliverables/D2.2/8051/src/ASM/I8051.ml
r619 r740 183 183 184 184 let reg_addr r = `DIRECT (BitVectors.vect_of_int r `Eight) 185 186 (* External RAM size *) 187 let ext_ram_size = MiscPottier.pow 2 16 188 (* Internal RAM size *) 189 let int_ram_size = MiscPottier.pow 2 8 -
Deliverables/D2.2/8051/src/ASM/I8051.mli
r486 r740 60 60 61 61 val reg_addr : register -> [> ASM.direct] 62 63 val ext_ram_size : int 64 val int_ram_size : int -
Deliverables/D2.2/8051/src/ERTL/ERTL.mli
r486 r740 121 121 122 122 (* Load from external memory. Parameters are the destination register, the 123 address registers, and the label of the next statement. *) 123 address registers (low bytes first), and the label of the next 124 statement. *) 124 125 | St_load of Register.t * Register.t * Register.t * Label.t 125 126 126 (* Store to external memory. Parameters are the address registers , the source127 register, and the label of the next statement. *)127 (* Store to external memory. Parameters are the address registers (low bytes 128 first), the source register, and the label of the next statement. *) 128 129 | St_store of Register.t * Register.t * Register.t * Label.t 129 130 -
Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml
r619 r740 12 12 module Eval = I8051.Eval (Val) 13 13 14 (* External RAM size *)15 let ext_ram_size = 100016 (* Internal RAM size *)17 let int_ram_size = 10018 19 20 let change_offset v off =21 if Val.is_pointer v then22 let (b, _) = Val.to_pointer v in23 Val.of_pointer (b, off)24 else error ((Val.to_string v) ^ " is not a pointer.")25 26 14 27 15 (* Memory *) … … 49 37 type state = 50 38 { st_frs : stack_frame list ; 51 pc : Val.t ; 52 isp : Val.t ; 39 pc : Val.address ; 40 isp : Val.address ; 41 exit : Val.address ; 53 42 lenv : local_env ; 54 43 carry : Val.t ; … … 66 55 let change_pc st pc = { st with pc = pc } 67 56 let change_isp st isp = { st with isp = isp } 57 let change_exit st exit = { st with exit = exit } 68 58 let change_lenv st lenv = { st with lenv = lenv } 69 59 let change_carry st carry = { st with carry = carry } … … 71 61 let change_mem st mem = { st with mem = mem } 72 62 let change_trace st trace = { st with trace = trace } 63 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace) 73 64 74 65 let empty_state = 75 66 { st_frs = [] ; 76 pc = Val.undef ; 77 isp = Val.undef ; 67 pc = Val.null ; 68 isp = Val.null ; 69 exit = Val.null ; 78 70 lenv = Register.Map.empty ; 79 71 carry = Val.undef ; … … 83 75 84 76 85 (* Each label of each function is associated a pointer. The base of this pointer86 is the base of the function in memory. Inside a function, offsets are77 (* Each label of each function is associated an address. The base of this 78 address is the base of the function in memory. Inside a function, offsets are 87 79 bijectively associated to labels. *) 88 80 … … 95 87 96 88 (* [labels_offsets p] builds a bijection between the labels found in the 97 functions of [p] and some offsets. *)89 functions of [p] and some memory addresses. *) 98 90 99 91 let labels_offsets p = … … 109 101 let fetch_stmt lbls_offs st = 110 102 let msg = 111 Printf.sprintf "%s does not point to a statement." (Val.to_string st.pc) in112 let error () = error msgin113 if Val.is_ pointerst.pc then114 let (_, off) = Val.to_pointerst.pc in103 Printf.sprintf "%s does not point to a statement." 104 (Val.string_of_address st.pc) in 105 if Val.is_mem_address st.pc then 106 let off = Val.offset_of_address st.pc in 115 107 let def = fun_def_of_ptr st.mem st.pc in 116 108 let lbl = Labels_Offsets.find2 off lbls_offs in 117 109 Label.Map.find lbl def.ERTL.f_graph 118 else error ()110 else error msg 119 111 120 112 let entry_pc lbls_offs ptr def = 121 change_offset ptr (Labels_Offsets.find1 def.ERTL.f_entry lbls_offs) 113 let off = Labels_Offsets.find1 def.ERTL.f_entry lbls_offs in 114 Val.change_address_offset ptr off 122 115 123 116 let init_fun_call lbls_offs st ptr def = … … 129 122 let next_pc lbls_offs st lbl = 130 123 let off = Labels_Offsets.find1 lbl lbls_offs in 131 change_pc st ( change_offset st.pc off)124 change_pc st (Val.change_address_offset st.pc off) 132 125 133 126 let framesize st = 134 if Val.is_ pointerst.pc then127 if Val.is_mem_address st.pc then 135 128 let def = fun_def_of_ptr st.mem st.pc in 136 129 def.ERTL.f_stacksize … … 156 149 157 150 let push st v = 158 let mem = Mem.store 2st.mem chunk st.isp v in159 let isp = Val. succ st.ispin151 let mem = Mem.store st.mem chunk st.isp v in 152 let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in 160 153 change_mem (change_isp st isp) mem 161 154 162 155 let pop st = 163 let isp = Val. pred st.ispin156 let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in 164 157 let st = change_isp st isp in 165 let v = Mem.load 2st.mem chunk st.isp in158 let v = Mem.load st.mem chunk st.isp in 166 159 (st, v) 167 160 161 let get_ra st = 162 let (st, pch) = pop st in 163 let (st, pcl) = pop st in 164 [pcl ; pch] 165 168 166 let save_ra lbls_offs st lbl = 169 let ra = change_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in170 let vs = Val.break ra 2in171 let st = push st (List.nth vs 1) in172 let st = push st (List.nth vs 0) in167 let ra = 168 Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in 169 let st = push st (List.nth ra 0) in 170 let st = push st (List.nth ra 1) in 173 171 st 174 172 175 let save_frame st = 176 add_st_frs st st.lenv 173 let save_frame st = add_st_frs st st.lenv 177 174 178 175 let label_of_pointer lbls_offs ptr = … … 180 177 Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ; 181 178 *) 182 let (_, off) = Val.to_pointerptr in179 let off = Val.offset_of_address ptr in 183 180 Labels_Offsets.find2 off lbls_offs 184 181 185 182 let pointer_of_label lbls_offs ptr lbl = 186 let (b, _) = Val.to_pointer ptr in 187 let off = Labels_Offsets.find1 lbl lbls_offs in 188 Val.of_pointer (b, off) 183 Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs) 189 184 190 185 let get_sp st = 191 let sph = get_reg (Hdw I8051.sph) st in 192 let spl = get_reg (Hdw I8051.spl) st in 193 Val.merge [sph ; spl] 194 195 let set_sp v st = 196 let vs = Val.break v 2 in 197 let sph = List.nth vs 0 in 198 let spl = List.nth vs 1 in 186 List.map (fun r -> get_reg (Hdw r) st) [I8051.spl ; I8051.sph] 187 188 let set_sp vs st = 189 let spl = List.nth vs 0 in 190 let sph = List.nth vs 1 in 191 let st = add_reg (Hdw I8051.spl) spl st in 199 192 let st = add_reg (Hdw I8051.sph) sph st in 200 let st = add_reg (Hdw I8051.spl) spl st in201 193 st 202 194 203 195 204 (* 205 let get_int () = 206 try Val.of_int (int_of_string (read_line ())) 207 with Failure "int_of_string" -> error "Failed to scan an integer." 208 let get_float () = 209 try Val.of_float (float_of_string (read_line ())) 210 with Failure "float_of_string" -> error "Failed to scan a float." 211 212 let interpret_external 213 (mem : memory) 214 (def : AST.external_function) 215 (args : Val.t list) : 216 memory * Val.t list = 217 match def.AST.ef_tag, args with 218 | s, _ when s = Primitive.scan_int -> 219 (mem, [get_int ()]) 220 | "scan_float", _ -> 221 (mem, [get_float ()]) 222 | s, v :: _ when s = Primitive.print_int && Val.is_int v -> 223 Printf.printf "%d" (Val.to_int v) ; 224 (mem, [Val.zero]) 225 | "print_float", v :: _ when Val.is_float v -> 226 Printf.printf "%f" (Val.to_float v) ; 227 (mem, [Val.zero]) 228 | "print_ptr", v :: _ when Val.is_pointer v -> 229 let (b, off) = Val.to_pointer v in 230 Printf.printf "block: %s, offset: %s" 231 (Val.Block.to_string b) (Val.Offset.to_string off) ; 232 (mem, [Val.zero]) 233 | s, v :: _ when s = Primitive.print_intln && Val.is_int v -> 234 Printf.printf "%d\n" (Val.to_int v) ; 235 (mem, [Val.zero]) 236 | "print_floatln", v :: _ when Val.is_float v -> 237 Printf.printf "%f" (Val.to_float v) ; 238 (mem, [Val.zero]) 239 | "print_ptrln", v :: _ when Val.is_pointer v -> 240 let (b, off) = Val.to_pointer v in 241 Printf.printf "block: %s, offset: %s\n" 242 (Val.Block.to_string b) (Val.Offset.to_string off) ; 243 (mem, [Val.zero]) 244 | s, v :: _ when s = Primitive.alloc -> 245 let (mem, ptr) = Mem.alloc mem v in 246 let vs = Val.break ptr 2 in 247 (mem, vs) 248 | s, v1 :: v2 :: _ when s = Primitive.modulo -> 249 (mem, [Val.modulo v1 v2]) 250 251 (* The other cases are either a type error (only integers and pointers 252 may not be differenciated during type checking) or an unknown 253 function. *) 254 | "print_int", _ | "print_intln", _ -> 255 error "Illegal cast from pointer to integer." 256 | "print_ptr", _ | "print_ptrln", _ -> 257 error "Illegal cast from integer to pointer." 258 | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".") 259 *) 260 196 module InterpretExternal = Primitive.Interpret (Mem) 197 198 let interpret_external mem f args = match InterpretExternal.t mem f args with 199 | (mem', InterpretExternal.V v) -> (mem', [v]) 200 | (mem', InterpretExternal.A addr) -> (mem', addr) 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 212 213 let interpret_external_call st f next_pc = 214 let args = fetch_external_args st in 215 let (mem, vs) = interpret_external st.mem f args in 216 let st = change_mem st mem in 217 let st = set_result st vs in 218 change_pc st next_pc 261 219 262 220 let interpret_call lbls_offs st f ra = … … 264 222 match Mem.find_fun_def st.mem ptr with 265 223 | ERTL.F_int def -> 266 (*267 Printf.printf "Pushing return address in IRAM: %s = %s\n%!"268 ra (Val.to_string (pointer_of_label lbls_offs st.pc ra)) ;269 *)270 224 let st = save_ra lbls_offs st ra in 271 225 let st = save_frame st in 272 226 init_fun_call lbls_offs st ptr def 273 | ERTL.F_ext def -> assert false (* TODO *) 227 | ERTL.F_ext def -> 228 let next_pc = 229 Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in 230 interpret_external_call st def.AST.ef_tag next_pc 274 231 275 232 let interpret_return lbls_offs st = … … 277 234 let (st, pch) = pop st in 278 235 let (st, pcl) = pop st in 279 let pc = Val.merge [pch ; pcl] in 280 (* 281 Printf.printf "Returning to %s = %s\n%!" 282 (Val.to_string pc) (label_of_pointer lbls_offs pc) ; 283 *) 236 let pc = [pcl ; pch] in 284 237 change_pc st pc 285 238 … … 301 254 302 255 | ERTL.St_cost (cost_lbl, lbl) -> 303 let st = change_trace st (cost_lbl :: st.trace)in256 let st = add_trace st cost_lbl in 304 257 next_pc st lbl 305 258 … … 319 272 let size = framesize st in 320 273 let sp = get_sp st in 321 let new_sp = Val. sub sp (Val.of_int size) in274 let new_sp = Val.add_address sp (Val.Offset.of_int (-size)) in 322 275 let st = set_sp new_sp st in 323 276 next_pc st lbl … … 326 279 let size = framesize st in 327 280 let sp = get_sp st in 328 let new_sp = Val.add sp (Val.of_int size) in281 let new_sp = Val.add_address sp (Val.Offset.of_int size) in 329 282 let st = set_sp new_sp st in 330 283 next_pc st lbl … … 346 299 347 300 | ERTL.St_addrH (r, x, lbl) -> 348 let v = Mem.find_global st.mem x in 349 let vs = Val.break v 2 in 301 let vs = Mem.find_global st.mem x in 302 let st = add_reg (Psd r) (List.nth vs 1) st in 303 next_pc st lbl 304 305 | ERTL.St_addrL (r, x, lbl) -> 306 let vs = Mem.find_global st.mem x in 350 307 let st = add_reg (Psd r) (List.nth vs 0) st in 351 next_pc st lbl352 353 | ERTL.St_addrL (r, x, lbl) ->354 let v = Mem.find_global st.mem x in355 let vs = Val.break v 2 in356 let st = add_reg (Psd r) (List.nth vs 1) st in357 308 next_pc st lbl 358 309 … … 392 343 393 344 | ERTL.St_load (destr, addr1, addr2, lbl) -> 394 let addr = 395 Val.merge (List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2]) in 396 let v = Mem.load2 st.mem chunk addr in 345 let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in 346 let v = Mem.load st.mem chunk addr in 397 347 let st = add_reg (Psd destr) v st in 398 348 next_pc st lbl 399 349 400 350 | ERTL.St_store (addr1, addr2, srcr, lbl) -> 401 let addr = 402 Val.merge (List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2]) in 403 let mem = Mem.store2 st.mem chunk addr (get_reg (Psd srcr) st) in 351 let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in 352 let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in 404 353 let st = change_mem st mem in 405 354 next_pc st lbl … … 421 370 422 371 423 let fetch_result renv ret_regs = match ret_regs with424 | [] -> Val.undef425 | [_] -> I8051.RegisterMap.find I8051.dpl renv426 | _ -> Val.merge [I8051.RegisterMap.find I8051.dph renv ;427 I8051.RegisterMap.find I8051.dpl renv]428 429 430 372 let print_lenv lenv = 431 373 let f r v = … … 441 383 442 384 let current_label lbls_offs st = 443 let (_, off) = Val.to_pointer st.pc in 444 Labels_Offsets.find2 off lbls_offs 385 Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs 445 386 446 387 let print_state lbls_offs st = 447 388 Printf.printf "PC: %s (%s)\n%!" 448 (Val.to_string st.pc) (current_label lbls_offs st) ; 449 Printf.printf "SP: %s\n%!" 450 (Val.to_string (Val.merge [get_reg (Hdw I8051.sph) st ; 451 get_reg (Hdw I8051.spl) st])) ; 452 Printf.printf "ISP: %s%!" (Val.to_string st.isp) ; 389 (Val.string_of_address st.pc) (current_label lbls_offs st) ; 390 Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ; 391 Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ; 453 392 print_lenv st.lenv ; 454 393 print_renv st.renv ; … … 458 397 let compute_result st ret_regs = 459 398 try 460 let v = get_reg (Psd ( MiscPottier.lastret_regs)) st in399 let v = get_reg (Psd (List.hd ret_regs)) st in 461 400 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 462 401 else IntValue.Int8.zero 463 402 with Not_found -> IntValue.Int8.zero 464 403 465 let rec iter_small_step print_result lbls_offs st = 404 let rec iter_small_step debug lbls_offs st = 405 if debug then print_state lbls_offs st ; 466 406 match fetch_stmt lbls_offs st with 467 | ERTL.St_return ret_regs when st.st_frs = [] -> 468 let (res, cost_labels) as trace = 469 (compute_result st ret_regs, List.rev st.trace) in 470 if print_result then 471 Printf.printf "ERTL: %s\n%!" (IntValue.Int8.to_string res) ; 472 trace 407 | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit -> 408 (compute_result st ret_regs, List.rev st.trace) 473 409 | stmt -> 474 (*475 print_state lbls_offs st ;476 *)477 410 let st' = interpret_stmt lbls_offs st stmt in 478 iter_small_step print_resultlbls_offs st'411 iter_small_step debug lbls_offs st' 479 412 480 413 … … 490 423 change_mem st mem 491 424 425 let init_sp st = 426 let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in 427 let sp = 428 Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in 429 let st = change_mem st mem in 430 (st, sp) 431 432 let init_isp st = 433 let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in 434 let st = change_mem (change_isp st isp) mem in 435 let (mem, exit) = Mem.alloc st.mem 1 in 436 let st = change_exit st exit in 437 let st = push st (List.nth exit 0) in 438 let st = push st (List.nth exit 1) in 439 st 440 492 441 let init_renv st sp = 493 442 let f r renv = I8051.RegisterMap.add r Val.undef renv in 494 443 let renv = I8051.RegisterSet.fold f I8051.registers I8051.RegisterMap.empty in 495 let vs = Val.break sp 2 in 496 let sph = List.nth vs 0 in 497 let spl = List.nth vs 1 in 444 let spl = List.nth sp 0 in 445 let sph = List.nth sp 1 in 498 446 let renv = I8051.RegisterMap.add I8051.sph sph renv in 499 447 let renv = I8051.RegisterMap.add I8051.spl spl renv in 500 448 change_renv st renv 501 502 let init_sp st =503 let (mem, sp) = Mem.alloc st.mem ext_ram_size in504 let (b, _) = Val.to_pointer sp in505 let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in506 let st = change_mem st mem in507 (st, sp)508 509 let init_isp st =510 let (mem, isp) = Mem.alloc st.mem int_ram_size in511 let st = change_mem (change_isp st isp) mem in512 let st = push st Val.zero in513 let st = push st Val.zero in514 st515 449 516 450 let init_main_call lbls_offs st main = … … 537 471 - Initialize the carry flag to 0. *) 538 472 539 let interpret print_result p = match p.ERTL.main with 540 | None -> (IntValue.Int8.zero (* TODO *), []) 541 | Some main -> 542 let lbls_offs = labels_offsets p in 543 let st = empty_state in 544 let st = init_prog st p in 545 let (st, sp) = init_sp st in 546 let st = init_isp st in 547 let st = init_renv st sp in 548 let st = init_main_call lbls_offs st main in 549 let st = change_carry st Val.zero in 550 iter_small_step print_result lbls_offs st 473 let interpret debug p = 474 if debug then Printf.printf "*** ERTL ***\n\n%!" ; 475 match p.ERTL.main with 476 | None -> (IntValue.Int8.zero, []) 477 | Some main -> 478 let lbls_offs = labels_offsets p in 479 let st = empty_state in 480 let st = init_prog st p in 481 let (st, sp) = init_sp st in 482 let st = init_isp st in 483 let st = init_renv st sp in 484 let st = init_main_call lbls_offs st main in 485 let st = change_carry st Val.zero in 486 iter_small_step debug lbls_offs st -
Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml
r486 r740 259 259 let l = generate (LTL.St_to_acc (I8051.st0, l)) in 260 260 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 261 let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in 262 let l = generate (LTL.St_from_acc (I8051.st0, l)) in 261 263 let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in 262 let l = generate (LTL.St_from_acc (I8051.st0, l)) in263 let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in264 264 LTL.St_skip l 265 265 … … 270 270 let l = generate (LTL.St_to_acc (I8051.st0, l)) in 271 271 let l = generate (LTL.St_from_acc (I8051.dpl, l)) in 272 let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in 273 let l = generate (LTL.St_from_acc (I8051.st0, l)) in 272 274 let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in 273 let l = generate (LTL.St_from_acc (I8051.st0, l)) in274 let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in275 275 let l = generate (LTL.St_from_acc (I8051.st1, l)) in 276 276 let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in -
Deliverables/D2.2/8051/src/LIN/LINInterpret.ml
r619 r740 12 12 module Eval = I8051.Eval (Val) 13 13 14 (* External RAM size *)15 let ext_ram_size = 100016 (* Internal RAM size *)17 let int_ram_size = 10018 19 20 let change_offset v off =21 if Val.is_pointer v then22 let (b, _) = Val.to_pointer v in23 Val.of_pointer (b, off)24 else error ((Val.to_string v) ^ " is not a pointer.")25 26 14 27 15 (* Memory *) … … 29 17 type memory = LIN.function_def Mem.memory 30 18 31 (* Hardware registers environments. They associate a value to theeach hardware19 (* Hardware registers environments. They associate a value to each hardware 32 20 register. *) 33 21 … … 37 25 38 26 type state = 39 { pc : Val.t ; 40 isp : Val.t ; 27 { pc : Val.address ; 28 isp : Val.address ; 29 exit : Val.address ; 41 30 carry : Val.t ; 42 31 renv : hdw_reg_env ; … … 49 38 let change_pc st pc = { st with pc = pc } 50 39 let change_isp st isp = { st with isp = isp } 40 let change_exit st exit = { st with exit = exit } 51 41 let change_carry st carry = { st with carry = carry } 52 42 let change_renv st renv = { st with renv = renv } 53 43 let change_mem st mem = { st with mem = mem } 54 44 let change_trace st trace = { st with trace = trace } 45 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace) 55 46 56 47 let empty_state = 57 { pc = Val.undef ; 58 isp = Val.undef ; 48 { pc = Val.null ; 49 isp = Val.null ; 50 exit = Val.null ; 59 51 carry = Val.undef ; 60 52 renv = I8051.RegisterMap.empty ; … … 71 63 let fetch_stmt st = 72 64 let msg = 73 Printf.sprintf "%s does not point to a statement." (Val.to_string st.pc) in74 let error () = error msgin75 if Val.is_ pointerst.pc then76 let (_, off) = Val.to_pointerst.pc in65 Printf.sprintf "%s does not point to a statement." 66 (Val.string_of_address st.pc) in 67 if Val.is_mem_address st.pc then 68 let off = Val.offset_of_address st.pc in 77 69 let def = int_fun_of_ptr st.mem st.pc in 78 70 List.nth def (Val.Offset.to_int off) 79 else error ()71 else error msg 80 72 81 73 let init_fun_call st ptr = 82 change_pc st ( change_offset ptr Val.Offset.zero)74 change_pc st (Val.change_address_offset ptr Val.Offset.zero) 83 75 84 76 let next_pc st = 85 change_pc st (Val. succ st.pc)77 change_pc st (Val.add_address st.pc Val.Offset.one) 86 78 87 79 let add_reg r v st = … … 94 86 95 87 let push st v = 96 let mem = Mem.store 2st.mem chunk st.isp v in97 let isp = Val. succ st.ispin88 let mem = Mem.store st.mem chunk st.isp v in 89 let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in 98 90 change_mem (change_isp st isp) mem 99 91 100 92 let pop st = 101 let isp = Val. pred st.ispin93 let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in 102 94 let st = change_isp st isp in 103 let v = Mem.load 2st.mem chunk st.isp in95 let v = Mem.load st.mem chunk st.isp in 104 96 (st, v) 105 97 106 98 let save_ra st = 107 let ra = Val.succ st.pc in 108 let vs = Val.break ra 2 in 109 let st = push st (List.nth vs 1) in 110 let st = push st (List.nth vs 0) in 99 let ra = Val.add_address st.pc Val.Offset.one in 100 let st = push st (List.nth ra 0) in 101 let st = push st (List.nth ra 1) in 111 102 st 112 103 … … 122 113 let code = current_int_fun st in 123 114 let off = find_label lbl code in 124 change_offset st.pc (Val.Offset.of_int off)115 Val.change_address_offset st.pc (Val.Offset.of_int off) 125 116 126 117 let goto st lbl = … … 130 121 let (st, pch) = pop st in 131 122 let (st, pcl) = pop st in 132 Val.merge [pch ; pcl] 133 134 135 (* 136 let get_int () = 137 try Val.of_int (int_of_string (read_line ())) 138 with Failure "int_of_string" -> error "Failed to scan an integer." 139 let get_float () = 140 try Val.of_float (float_of_string (read_line ())) 141 with Failure "float_of_string" -> error "Failed to scan a float." 142 143 let interpret_external 144 (mem : memory) 145 (def : AST.external_function) 146 (args : Val.t list) : 147 memory * Val.t list = 148 match def.AST.ef_tag, args with 149 | s, _ when s = Primitive.scan_int -> 150 (mem, [get_int ()]) 151 | "scan_float", _ -> 152 (mem, [get_float ()]) 153 | s, v :: _ when s = Primitive.print_int && Val.is_int v -> 154 Printf.printf "%d" (Val.to_int v) ; 155 (mem, [Val.zero]) 156 | "print_float", v :: _ when Val.is_float v -> 157 Printf.printf "%f" (Val.to_float v) ; 158 (mem, [Val.zero]) 159 | "print_ptr", v :: _ when Val.is_pointer v -> 160 let (b, off) = Val.to_pointer v in 161 Printf.printf "block: %s, offset: %s" 162 (Val.Block.to_string b) (Val.Offset.to_string off) ; 163 (mem, [Val.zero]) 164 | s, v :: _ when s = Primitive.print_intln && Val.is_int v -> 165 Printf.printf "%d\n" (Val.to_int v) ; 166 (mem, [Val.zero]) 167 | "print_floatln", v :: _ when Val.is_float v -> 168 Printf.printf "%f" (Val.to_float v) ; 169 (mem, [Val.zero]) 170 | "print_ptrln", v :: _ when Val.is_pointer v -> 171 let (b, off) = Val.to_pointer v in 172 Printf.printf "block: %s, offset: %s\n" 173 (Val.Block.to_string b) (Val.Offset.to_string off) ; 174 (mem, [Val.zero]) 175 | s, v :: _ when s = Primitive.alloc -> 176 let (mem, ptr) = Mem.alloc mem v in 177 let vs = Val.break ptr 2 in 178 (mem, vs) 179 | s, v1 :: v2 :: _ when s = Primitive.modulo -> 180 (mem, [Val.modulo v1 v2]) 181 182 (* The other cases are either a type error (only integers and pointers 183 may not be differenciated during type checking) or an unknown 184 function. *) 185 | "print_int", _ | "print_intln", _ -> 186 error "Illegal cast from pointer to integer." 187 | "print_ptr", _ | "print_ptrln", _ -> 188 error "Illegal cast from integer to pointer." 189 | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".") 190 *) 191 123 (st, [pcl ; pch]) 124 125 let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph] 126 127 128 (* State pretty-printing *) 129 130 let print_renv renv = 131 let f r v = 132 if not (Val.eq v Val.undef) then 133 Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in 134 I8051.RegisterMap.iter f renv 135 136 let print_state st = 137 Printf.printf "PC: %s\n%!" (Val.string_of_address st.pc) ; 138 Printf.printf "SP: %s\n%!" 139 (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ; 140 Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ; 141 print_renv st.renv ; 142 Printf.printf "\nC = %s%!" (Val.to_string st.carry) ; 143 Mem.print st.mem ; 144 Printf.printf "\n%!" 145 146 147 module InterpretExternal = Primitive.Interpret (Mem) 148 149 let interpret_external mem f args = match InterpretExternal.t mem f args with 150 | (mem', InterpretExternal.V v) -> (mem', [v]) 151 | (mem', InterpretExternal.A addr) -> (mem', addr) 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 163 164 let interpret_external_call st f = 165 let args = fetch_external_args st in 166 let (mem, vs) = interpret_external st.mem f args in 167 let st = change_mem st mem in 168 set_result st vs 192 169 193 170 let interpret_call st f = … … 197 174 let st = save_ra st in 198 175 init_fun_call st ptr 199 | LIN.F_ext def -> assert false (* TODO *) 176 | LIN.F_ext def -> 177 let st = next_pc st in 178 interpret_external_call st def.AST.ef_tag 200 179 201 180 let interpret_return st = 202 let pc= return_pc st in181 let (st, pc) = return_pc st in 203 182 change_pc st pc 204 183 … … 219 198 220 199 | LIN.St_cost cost_lbl -> 221 let st = change_trace st (cost_lbl :: st.trace)in200 let st = add_trace st cost_lbl in 222 201 next_pc st 223 202 … … 237 216 238 217 | LIN.St_addr x -> 239 let v = Mem.find_global st.mem x in 240 let vs = Val.break v 2 in 241 let st = add_reg I8051.dph (List.nth vs 0) st in 242 let st = add_reg I8051.dpl (List.nth vs 1) st in 218 let vs = Mem.find_global st.mem x in 219 let st = add_reg I8051.dpl (List.nth vs 0) st in 220 let st = add_reg I8051.dph (List.nth vs 1) st in 243 221 next_pc st 244 222 … … 278 256 279 257 | LIN.St_load -> 280 let addr = 281 Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in 282 let v = Mem.load2 st.mem chunk addr in 258 let addr = dptr st in 259 let v = Mem.load st.mem chunk addr in 283 260 let st = add_reg I8051.a v st in 284 261 next_pc st 285 262 286 263 | LIN.St_store -> 287 let addr = 288 Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in 289 let mem = Mem.store2 st.mem chunk addr (get_reg I8051.a st) in 264 let addr = dptr st in 265 let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in 290 266 let st = change_mem st mem in 291 267 next_pc st … … 305 281 306 282 307 let print_renv renv =308 let f r v =309 if not (Val.eq v Val.undef) then310 Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in311 I8051.RegisterMap.iter f renv312 313 let print_state st =314 Printf.printf "PC: %s\n%!" (Val.to_string st.pc) ;315 Printf.printf "SP: %s\n%!"316 (Val.to_string (Val.merge [get_reg I8051.sph st ; get_reg I8051.spl st])) ;317 Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;318 print_renv st.renv ;319 Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;320 Mem.print st.mem ;321 Printf.printf "\n%!"322 323 283 let compute_result st = 324 284 let v = get_reg I8051.dpl st in … … 326 286 else IntValue.Int8.zero 327 287 328 let rec iter_small_step print_result st = 329 (* 330 (* <DEBUG> *) 331 print_state st ; 332 (* </DEBUG> *) 333 *) 288 let rec iter_small_step debug st = 289 if debug then print_state st ; 334 290 match fetch_stmt st with 335 | LIN.St_return when Val.eq (return_pc st) Val.zero -> 336 let (res, cost_labels) as trace = 337 (compute_result st, List.rev st.trace) in 338 if print_result then 339 Printf.printf "LIN: %s\n%!" (IntValue.Int8.to_string res) ; 340 trace 291 | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit -> 292 (compute_result st, List.rev st.trace) 341 293 | stmt -> 342 294 let st' = interpret_stmt st stmt in 343 iter_small_step print_resultst'295 iter_small_step debug st' 344 296 345 297 … … 355 307 change_mem st mem 356 308 309 let init_sp st = 310 let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in 311 let sp = 312 Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in 313 let st = change_mem st mem in 314 (st, sp) 315 316 let init_isp st = 317 let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in 318 let st = change_mem (change_isp st isp) mem in 319 let (mem, exit) = Mem.alloc st.mem 1 in 320 let st = change_exit st exit in 321 let st = push st (List.nth exit 0) in 322 let st = push st (List.nth exit 1) in 323 st 324 357 325 let init_renv st sp = 358 326 let f r st = add_reg r Val.undef st in 359 327 let st = I8051.RegisterSet.fold f I8051.registers st in 360 let vs = Val.break sp 2in361 let sph = List.nth vs 0in362 let s pl = List.nth vs 1in328 let spl = List.nth sp 0 in 329 let sph = List.nth sp 1 in 330 let st = add_reg I8051.spl spl st in 363 331 let st = add_reg I8051.sph sph st in 364 let st = add_reg I8051.spl spl st in365 332 st 366 367 let init_sp st =368 let (mem, sp) = Mem.alloc st.mem ext_ram_size in369 let (b, _) = Val.to_pointer sp in370 let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in371 let st = change_mem st mem in372 (st, sp)373 374 let init_isp st =375 let (mem, isp) = Mem.alloc st.mem int_ram_size in376 let st = change_mem (change_isp st isp) mem in377 let vs = Val.break Val.zero 2 in378 let st = push st (List.nth vs 1) in379 let st = push st (List.nth vs 0) in380 st381 333 382 334 let init_main_call st main = … … 401 353 - Initialize the carry flag to 0. *) 402 354 403 let interpret print_result p = match p.LIN.main with 404 | None -> (IntValue.Int8.zero, []) 405 | Some main -> 406 let st = empty_state in 407 let st = init_prog st p in 408 let (st, sp) = init_sp st in 409 let st = init_isp st in 410 let st = init_renv st sp in 411 let st = init_main_call st main in 412 let st = change_carry st Val.zero in 413 iter_small_step print_result st 355 let interpret debug p = 356 if debug then Printf.printf "*** LIN ***\n\n%!" ; 357 match p.LIN.main with 358 | None -> (IntValue.Int8.zero, []) 359 | Some main -> 360 let st = empty_state in 361 let st = init_prog st p in 362 let (st, sp) = init_sp st in 363 let st = init_isp st in 364 let st = init_renv st sp in 365 let st = init_main_call st main in 366 let st = change_carry st Val.zero in 367 iter_small_step debug st -
Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml
r619 r740 10 10 module Val = Mem.Value 11 11 let chunk = Driver.LTLMemory.int_size 12 (*13 let load mem = Mem.load2 st.mem chunk st.isp14 *)15 12 module Eval = I8051.Eval (Val) 16 17 (* External RAM size *)18 let ext_ram_size = 100019 (* Internal RAM size *)20 let int_ram_size = 10021 22 23 let change_offset v off =24 if Val.is_pointer v then25 let (b, _) = Val.to_pointer v in26 Val.of_pointer (b, off)27 else error ((Val.to_string v) ^ " is not a pointer.")28 13 29 14 … … 40 25 41 26 type state = 42 { pc : Val.t ; 43 isp : Val.t ; 27 { pc : Val.address ; 28 isp : Val.address ; 29 exit : Val.address ; 44 30 carry : Val.t ; 45 31 renv : hdw_reg_env ; … … 52 38 let change_pc st pc = { st with pc = pc } 53 39 let change_isp st isp = { st with isp = isp } 40 let change_exit st exit = { st with exit = exit } 54 41 let change_carry st carry = { st with carry = carry } 55 42 let change_renv st renv = { st with renv = renv } 56 43 let change_mem st mem = { st with mem = mem } 57 44 let change_trace st trace = { st with trace = trace } 45 let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace) 58 46 59 47 let empty_state = 60 { pc = Val.undef ; 61 isp = Val.undef ; 48 { pc = Val.null ; 49 isp = Val.null ; 50 exit = Val.null ; 62 51 carry = Val.undef ; 63 52 renv = I8051.RegisterMap.empty ; … … 92 81 let fetch_stmt lbls_offs st = 93 82 let msg = 94 Printf.sprintf "%s does not point to a statement." (Val.to_string st.pc) in95 let error () = error msgin96 if Val.is_ pointerst.pc then97 let (_, off) = Val.to_pointerst.pc in83 Printf.sprintf "%s does not point to a statement." 84 (Val.string_of_address st.pc) in 85 if Val.is_mem_address st.pc then 86 let off = Val.offset_of_address st.pc in 98 87 let def = fun_def_of_ptr st.mem st.pc in 99 88 let lbl = Labels_Offsets.find2 off lbls_offs in 100 89 Label.Map.find lbl def.LTL.f_graph 101 else error ()90 else error msg 102 91 103 92 let entry_pc lbls_offs ptr def = 104 change_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)93 Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs) 105 94 106 95 let init_fun_call lbls_offs st ptr def = … … 110 99 let next_pc lbls_offs st lbl = 111 100 let off = Labels_Offsets.find1 lbl lbls_offs in 112 change_pc st ( change_offset st.pc off)101 change_pc st (Val.change_address_offset st.pc off) 113 102 114 103 let framesize st = 115 if Val.is_ pointerst.pc then104 if Val.is_mem_address st.pc then 116 105 let def = fun_def_of_ptr st.mem st.pc in 117 106 def.LTL.f_stacksize … … 127 116 128 117 let push st v = 129 let mem = Mem.store 2st.mem chunk st.isp v in130 let isp = Val. succ st.ispin118 let mem = Mem.store st.mem chunk st.isp v in 119 let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in 131 120 change_mem (change_isp st isp) mem 132 121 133 122 let pop st = 134 let isp = Val. pred st.ispin123 let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in 135 124 let st = change_isp st isp in 136 let v = Mem.load 2st.mem chunk st.isp in125 let v = Mem.load st.mem chunk st.isp in 137 126 (st, v) 138 127 139 128 let save_ra lbls_offs st lbl = 140 let ra = change_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in141 let vs = Val.break ra 2in142 let st = push st (List.nth vs 1) in143 let st = push st (List.nth vs 0) in129 let ra = 130 Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in 131 let st = push st (List.nth ra 0) in 132 let st = push st (List.nth ra 1) in 144 133 st 145 134 … … 148 137 Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ; 149 138 *) 150 let (_, off) = Val.to_pointerptr in139 let off = Val.offset_of_address ptr in 151 140 Labels_Offsets.find2 off lbls_offs 152 141 153 142 let pointer_of_label lbls_offs ptr lbl = 154 let (b, _) = Val.to_pointer ptr in 155 let off = Labels_Offsets.find1 lbl lbls_offs in 156 Val.of_pointer (b, off) 143 Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs) 157 144 158 145 let return_pc st = 159 146 let (st, pch) = pop st in 160 147 let (st, pcl) = pop st in 161 Val.merge [pch ; pcl] 162 163 164 (* 165 let get_int () = 166 try Val.of_int (int_of_string (read_line ())) 167 with Failure "int_of_string" -> error "Failed to scan an integer." 168 let get_float () = 169 try Val.of_float (float_of_string (read_line ())) 170 with Failure "float_of_string" -> error "Failed to scan a float." 171 172 let interpret_external 173 (mem : memory) 174 (def : AST.external_function) 175 (args : Val.t list) : 176 memory * Val.t list = 177 match def.AST.ef_tag, args with 178 | s, _ when s = Primitive.scan_int -> 179 (mem, [get_int ()]) 180 | "scan_float", _ -> 181 (mem, [get_float ()]) 182 | s, v :: _ when s = Primitive.print_int && Val.is_int v -> 183 Printf.printf "%d" (Val.to_int v) ; 184 (mem, [Val.zero]) 185 | "print_float", v :: _ when Val.is_float v -> 186 Printf.printf "%f" (Val.to_float v) ; 187 (mem, [Val.zero]) 188 | "print_ptr", v :: _ when Val.is_pointer v -> 189 let (b, off) = Val.to_pointer v in 190 Printf.printf "block: %s, offset: %s" 191 (Val.Block.to_string b) (Val.Offset.to_string off) ; 192 (mem, [Val.zero]) 193 | s, v :: _ when s = Primitive.print_intln && Val.is_int v -> 194 Printf.printf "%d\n" (Val.to_int v) ; 195 (mem, [Val.zero]) 196 | "print_floatln", v :: _ when Val.is_float v -> 197 Printf.printf "%f" (Val.to_float v) ; 198 (mem, [Val.zero]) 199 | "print_ptrln", v :: _ when Val.is_pointer v -> 200 let (b, off) = Val.to_pointer v in 201 Printf.printf "block: %s, offset: %s\n" 202 (Val.Block.to_string b) (Val.Offset.to_string off) ; 203 (mem, [Val.zero]) 204 | s, v :: _ when s = Primitive.alloc -> 205 let (mem, ptr) = Mem.alloc mem v in 206 let vs = Val.break ptr 2 in 207 (mem, vs) 208 | s, v1 :: v2 :: _ when s = Primitive.modulo -> 209 (mem, [Val.modulo v1 v2]) 210 211 (* The other cases are either a type error (only integers and pointers 212 may not be differenciated during type checking) or an unknown 213 function. *) 214 | "print_int", _ | "print_intln", _ -> 215 error "Illegal cast from pointer to integer." 216 | "print_ptr", _ | "print_ptrln", _ -> 217 error "Illegal cast from integer to pointer." 218 | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".") 219 *) 220 148 (st, [pcl ; pch]) 149 150 let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph] 151 152 153 (* State pretty-printing *) 154 155 let current_label lbls_offs st = 156 Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs 157 158 let print_renv renv = 159 let f r v = 160 if not (Val.eq v Val.undef) then 161 Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in 162 I8051.RegisterMap.iter f renv 163 164 let print_state lbls_offs st = 165 Printf.printf "PC: %s (%s)\n%!" 166 (Val.string_of_address st.pc) (current_label lbls_offs st) ; 167 Printf.printf "SP: %s\n%!" 168 (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ; 169 Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ; 170 print_renv st.renv ; 171 Printf.printf "\nC = %s%!" (Val.to_string st.carry) ; 172 Mem.print st.mem ; 173 Printf.printf "\n%!" 174 175 176 module InterpretExternal = Primitive.Interpret (Mem) 177 178 let interpret_external mem f args = match InterpretExternal.t mem f args with 179 | (mem', InterpretExternal.V v) -> (mem', [v]) 180 | (mem', InterpretExternal.A addr) -> (mem', addr) 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 192 193 let interpret_external_call st f next_pc = 194 let args = fetch_external_args st in 195 let (mem, vs) = interpret_external st.mem f args in 196 let st = change_mem st mem in 197 let st = set_result st vs in 198 change_pc st next_pc 221 199 222 200 let interpret_call lbls_offs st f ra = … … 224 202 match Mem.find_fun_def st.mem ptr with 225 203 | LTL.F_int def -> 226 (*227 Printf.printf "Pushing return address in IRAM: %s = %s\n%!"228 ra (Val.to_string (pointer_of_label lbls_offs st.pc ra)) ;229 *)230 204 let st = save_ra lbls_offs st ra in 231 205 init_fun_call lbls_offs st ptr def 232 | LTL.F_ext def -> assert false (* TODO *) 206 | LTL.F_ext def -> 207 let next_pc = 208 Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in 209 interpret_external_call st def.AST.ef_tag next_pc 233 210 234 211 let interpret_return lbls_offs st = 235 let pc = return_pc st in 236 (* 237 Printf.printf "Returning to %s = %s\n%!" 238 (Val.to_string pc) (label_of_pointer lbls_offs pc) ; 239 *) 212 let (st, pc) = return_pc st in 240 213 change_pc st pc 241 214 … … 257 230 258 231 | LTL.St_cost (cost_lbl, lbl) -> 259 let st = change_trace st (cost_lbl :: st.trace)in232 let st = add_trace st cost_lbl in 260 233 next_pc st lbl 261 234 … … 275 248 276 249 | LTL.St_addr (x, lbl) -> 277 let v = Mem.find_global st.mem x in 278 let vs = Val.break v 2 in 279 let st = add_reg I8051.dph (List.nth vs 0) st in 280 let st = add_reg I8051.dpl (List.nth vs 1) st in 250 let vs = Mem.find_global st.mem x in 251 let st = add_reg I8051.dpl (List.nth vs 0) st in 252 let st = add_reg I8051.dph (List.nth vs 1) st in 281 253 next_pc st lbl 282 254 … … 316 288 317 289 | LTL.St_load lbl -> 318 let addr = 319 Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in 320 let v = Mem.load2 st.mem chunk addr in 290 let addr = dptr st in 291 let v = Mem.load st.mem chunk addr in 321 292 let st = add_reg I8051.a v st in 322 293 next_pc st lbl 323 294 324 295 | LTL.St_store lbl -> 325 let addr = 326 Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in 327 let mem = Mem.store2 st.mem chunk addr (get_reg I8051.a st) in 296 let addr = dptr st in 297 let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in 328 298 let st = change_mem st mem in 329 299 next_pc st lbl … … 345 315 346 316 347 let current_label lbls_offs st =348 let (_, off) = Val.to_pointer st.pc in349 Labels_Offsets.find2 off lbls_offs350 351 let print_renv renv =352 let f r v =353 if not (Val.eq v Val.undef) then354 Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in355 I8051.RegisterMap.iter f renv356 357 let print_state lbls_offs st =358 Printf.printf "PC: %s (%s)\n%!"359 (Val.to_string st.pc) (current_label lbls_offs st) ;360 Printf.printf "SP: %s\n%!"361 (Val.to_string (Val.merge [get_reg I8051.sph st ; get_reg I8051.spl st])) ;362 Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;363 print_renv st.renv ;364 Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;365 Mem.print st.mem ;366 Printf.printf "\n%!"367 368 let print_result st =369 let string_of_reg r = Val.to_string (get_reg r st) in370 Printf.printf "DPH: %s - DPL: %s\n%!"371 (string_of_reg I8051.dph) (string_of_reg I8051.dpl)372 373 317 let compute_result st = 374 318 let v = get_reg I8051.dpl st in … … 376 320 else IntValue.Int8.zero 377 321 378 let rec iter_small_step print_result lbls_offs st = 379 (* 380 print_state lbls_offs st ; 381 *) 322 let rec iter_small_step debug lbls_offs st = 323 if debug then print_state lbls_offs st ; 382 324 match fetch_stmt lbls_offs st with 383 | LTL.St_return when Val.eq (return_pc st) Val.zero -> 384 let (res, cost_labels) as trace = 385 (compute_result st, List.rev st.trace) in 386 if print_result then 387 Printf.printf "LTL: %s\n%!" (IntValue.Int8.to_string res) ; 388 trace 325 | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit -> 326 (compute_result st, List.rev st.trace) 389 327 | stmt -> 390 328 let st' = interpret_stmt lbls_offs st stmt in 391 iter_small_step print_resultlbls_offs st'329 iter_small_step debug lbls_offs st' 392 330 393 331 … … 403 341 change_mem st mem 404 342 343 let init_sp st = 344 let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in 345 let sp = 346 Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in 347 let st = change_mem st mem in 348 (st, sp) 349 350 let init_isp st = 351 let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in 352 let st = change_mem (change_isp st isp) mem in 353 let (mem, exit) = Mem.alloc st.mem 1 in 354 let st = change_exit st exit in 355 let st = push st (List.nth exit 0) in 356 let st = push st (List.nth exit 1) in 357 st 358 405 359 let init_renv st sp = 406 360 let f r st = add_reg r Val.undef st in 407 361 let st = I8051.RegisterSet.fold f I8051.registers st in 408 let vs = Val.break sp 2in409 let sph = List.nth vs 0in410 let s pl = List.nth vs 1in362 let spl = List.nth sp 0 in 363 let sph = List.nth sp 1 in 364 let st = add_reg I8051.spl spl st in 411 365 let st = add_reg I8051.sph sph st in 412 let st = add_reg I8051.spl spl st in413 366 st 414 415 let init_sp st =416 let (mem, sp) = Mem.alloc st.mem ext_ram_size in417 let (b, _) = Val.to_pointer sp in418 let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in419 let st = change_mem st mem in420 (st, sp)421 422 let init_isp st =423 let (mem, isp) = Mem.alloc st.mem int_ram_size in424 let st = change_mem (change_isp st isp) mem in425 let vs = Val.break Val.zero 2 in426 let st = push st (List.nth vs 1) in427 let st = push st (List.nth vs 0) in428 st429 367 430 368 let init_main_call lbls_offs st main = … … 451 389 - Initialize the carry flag to 0. *) 452 390 453 let interpret print_result p = match p.LTL.main with 454 | None -> (IntValue.Int8.zero, []) 455 | Some main -> 456 let lbls_offs = labels_offsets p in 457 let st = empty_state in 458 let st = init_prog st p in 459 let (st, sp) = init_sp st in 460 let st = init_isp st in 461 let st = init_renv st sp in 462 let st = init_main_call lbls_offs st main in 463 let st = change_carry st Val.zero in 464 iter_small_step print_result lbls_offs st 391 let interpret debug p = 392 if debug then Printf.printf "*** LTL ***\n\n%!" ; 393 match p.LTL.main with 394 | None -> (IntValue.Int8.zero, []) 395 | Some main -> 396 let lbls_offs = labels_offsets p in 397 let st = empty_state in 398 let st = init_prog st p in 399 let (st, sp) = init_sp st in 400 let st = init_isp st in 401 let st = init_renv st sp in 402 let st = init_main_call lbls_offs st main in 403 let st = change_carry st Val.zero in 404 iter_small_step debug lbls_offs st -
Deliverables/D2.2/8051/src/RTL/RTL.mli
r486 r740 18 18 19 19 (* Assign the address of a symbol to registers. Parameters are the destination 20 registers, the symbol and the label of the next statement. *) 20 registers (low bytes first), the symbol and the label of the next 21 statement. *) 21 22 | St_addr of Register.t * Register.t * AST.ident * Label.t 22 23 23 24 (* Assign the stack pointer to registers. Parameters are the destination 24 registers , and the label of the next statement. *)25 registers (low bytes first), and the label of the next statement. *) 25 26 | St_stackaddr of Register.t * Register.t * Label.t 26 27 … … 51 52 52 53 (* Load from external memory. Parameters are the destination register, the 53 address registers, and the label of the next statement. *) 54 address registers (low bytes first), and the label of the next 55 statement. *) 54 56 | St_load of Register.t * Register.t * Register.t * Label.t 55 57 56 (* Store to external memory. Parameters are the address registers , the source57 register, and the label of the next statement. *)58 (* Store to external memory. Parameters are the address registers (low bytes 59 first), the source register, and the label of the next statement. *) 58 60 | St_store of Register.t * Register.t * Register.t * Label.t 59 61 … … 64 66 65 67 (* Call to a function given its address. Parameters are the registers holding 66 the address of the function, the arguments of the function, the destination 67 registers, and the label of the next statement. *) 68 the address of the function (low bytes first), the arguments of the 69 function, the destination registers, and the label of the next 70 statement. *) 68 71 | St_call_ptr of Register.t * Register.t * Register.t list * registers * 69 72 Label.t 70 73 71 74 (* Tail call to a function given its name. Parameters are the name of the … … 74 77 75 78 (* Tail call to a function given its address. Parameters are the registers 76 holding the address of the function, and the arguments of the function. *) 79 holding the address of the function (low bytes first), and the arguments of 80 the function. *) 77 81 | St_tailcall_ptr of Register.t * Register.t * Register.t list 78 82 … … 84 88 (* Return the value of some registers. Their may be no register in case of 85 89 procedures, one register when returning an integer, or two registers when 86 returning an address . *)90 returning an address (low bytes first). *) 87 91 | St_return of registers 88 92 … … 94 98 f_runiverse : Register.universe ; 95 99 f_sig : AST.signature ; 96 f_result : Register.t list ;100 f_result : Register.t list (* low byte first *) ; 97 101 f_params : Register.t list ; 98 102 f_locals : Register.Set.t ; -
Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml
r619 r740 30 30 graph : RTL.graph ; 31 31 pc : Label.t ; 32 sp : Val. t;32 sp : Val.address ; 33 33 lenv : local_env ; 34 34 carry : Val.t } … … 40 40 41 41 type state = 42 | State of stack_frame list * RTL.graph * Label.t * Val. t(* sp *) *42 | State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) * 43 43 local_env * Val.t (* carry *) * memory * CostLabel.t list 44 44 | CallState of stack_frame list * RTL.function_def * … … 47 47 memory * CostLabel.t list 48 48 49 let string_of_local_env lenv = 50 let f x v s = 51 s ^ 52 (if Val.eq v Val.undef then "" 53 else (Register.print x) ^ " = " ^ (Val.to_string v) ^ " ") in 54 Register.Map.fold f lenv "" 55 56 let string_of_args args = 57 let f s v = s ^ " " ^ (Val.to_string v) in 58 List.fold_left f "" args 59 60 let print_state = function 61 | State (_, _, lbl, sp, lenv, carry, mem, _) -> 62 Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!" 63 (Val.string_of_address sp) 64 (Val.to_string carry) 65 (string_of_local_env lenv) 66 (Mem.to_string mem) 67 lbl 68 | CallState (_, _, args, mem, _) -> 69 Printf.printf "Memory:%s\nCall state: %s\n\n%!" 70 (Mem.to_string mem) 71 (string_of_args args) 72 | ReturnState (_, vs, mem, _) -> 73 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 74 (Mem.to_string mem) 75 (string_of_args vs) 76 49 77 50 78 let find_function mem f = 51 let v= Mem.find_global mem f in52 Mem.find_fun_def mem v79 let addr = Mem.find_global mem f in 80 Mem.find_fun_def mem addr 53 81 54 82 let get_local_value (lenv : local_env) (r : Register.t) : Val.t = … … 58 86 59 87 let get_local_addr lenv f1 f2 = 60 Val.merge (List.map (get_local_value lenv) [f1 ; f2]) 61 62 (* An address is represented by two pseudo-registers (because in 8051, addresses 63 are coded on two bytes). Thus, assignments may involve several 64 registers. When we want to assign a single value to several registers, we 65 break the value into as many parts as there are registers, and then we update 66 each register with a part of the value. *) 67 68 let adds rs v lenv = match rs with 69 | [] -> lenv 70 | _ -> 71 let vs = Val.break v (List.length rs) in 72 let f lenv r v = Register.Map.add r v lenv in 73 List.fold_left2 f lenv rs vs 88 List.map (get_local_value lenv) [f1 ; f2] 89 90 91 let adds rs vs lenv = 92 let f lenv r v = Register.Map.add r v lenv in 93 List.fold_left2 f lenv rs vs 74 94 75 95 76 96 (* Assign a value to some destinations registers. *) 77 97 78 let assign_state cs c lbl sp lenv carry mem t destrs v=79 let lenv = adds destrs v lenv in80 State ( cs, c, lbl, sp, lenv, carry, mem, t)98 let assign_state sfrs graph lbl sp lenv carry mem trace destrs vs = 99 let lenv = adds destrs vs lenv in 100 State (sfrs, graph, lbl, sp, lenv, carry, mem, trace) 81 101 82 102 (* Branch on a value. *) 83 103 84 let branch_state cs c lbl_true lbl_false sp lenv carry mem tv =104 let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v = 85 105 let next_lbl = 86 106 if Val.is_true v then lbl_true … … 88 108 if Val.is_false v then lbl_false 89 109 else error "Undefined conditional value." in 90 State ( cs, c, next_lbl, sp, lenv, carry, mem, t)110 State (sfrs, graph, next_lbl, sp, lenv, carry, mem, trace) 91 111 92 112 … … 94 114 95 115 let interpret_statement 96 ( cs: stack_frame list)97 ( c: RTL.graph)98 (sp : Val. t)116 (sfrs : stack_frame list) 117 (graph : RTL.graph) 118 (sp : Val.address) 99 119 (lenv : local_env) 100 120 (carry : Val.t) 101 121 (mem : memory) 102 122 (stmt : RTL.statement) 103 (t 123 (trace : CostLabel.t list) : 104 124 state = match stmt with 105 125 106 126 | RTL.St_skip lbl -> 107 State ( cs, c, lbl, sp, lenv, carry, mem, t)127 State (sfrs, graph, lbl, sp, lenv, carry, mem, trace) 108 128 109 129 | RTL.St_cost (cost_lbl, lbl) -> 110 State ( cs, c, lbl, sp, lenv, carry, mem, cost_lbl :: t)130 State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace) 111 131 112 132 | RTL.St_addr (r1, r2, x, lbl) -> 113 assign_state cs c lbl sp lenv carry mem t[r1 ; r2]133 assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] 114 134 (Mem.find_global mem x) 115 135 116 136 | RTL.St_stackaddr (r1, r2, lbl) -> 117 assign_state cs c lbl sp lenv carry mem t[r1 ; r2] sp137 assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp 118 138 119 139 | RTL.St_int (r, i, lbl) -> 120 assign_state cs c lbl sp lenv carry mem t [r] (Val.of_int i)140 assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i] 121 141 122 142 | RTL.St_move (destr, srcr, lbl) -> 123 assign_state cs c lbl sp lenv carry mem t[destr]124 (get_local_value lenv srcr)143 assign_state sfrs graph lbl sp lenv carry mem trace [destr] 144 [get_local_value lenv srcr] 125 145 126 146 | RTL.St_opaccs (opaccs, destr, srcr1, srcr2, lbl) -> … … 129 149 (get_local_value lenv srcr1) 130 150 (get_local_value lenv srcr2) in 131 assign_state cs c lbl sp lenv carry mem t [destr] v151 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v] 132 152 133 153 | RTL.St_op1 (op1, destr, srcr, lbl) -> 134 154 let v = Eval.op1 op1 (get_local_value lenv srcr) in 135 assign_state cs c lbl sp lenv carry mem t [destr] v155 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v] 136 156 137 157 | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) -> … … 140 160 (get_local_value lenv srcr1) 141 161 (get_local_value lenv srcr2) in 142 assign_state cs c lbl sp lenv carry mem t [destr] v162 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v] 143 163 144 164 | RTL.St_clear_carry lbl -> 145 State ( cs, c, lbl, sp, lenv, Val.zero, mem, t)165 State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace) 146 166 147 167 | RTL.St_load (destr, addr1, addr2, lbl) -> 148 let dph = get_local_value lenv addr1 in 149 let dpl = get_local_value lenv addr2 in 150 let addr = Val.merge [dph ; dpl] in 151 let v = Mem.load2 mem chunk addr in 152 assign_state cs c lbl sp lenv carry mem t [destr] v 168 let addr = get_local_addr lenv addr1 addr2 in 169 let v = Mem.load mem chunk addr in 170 assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v] 153 171 154 172 | RTL.St_store (addr1, addr2, srcr, lbl) -> 155 let dph = get_local_value lenv addr1 in 156 let dpl = get_local_value lenv addr2 in 157 let addr = Val.merge [dph ; dpl] in 158 let mem = Mem.store2 mem chunk addr (get_local_value lenv srcr) in 159 State (cs, c, lbl, sp, lenv, carry, mem, t) 173 let addr = get_local_addr lenv addr1 addr2 in 174 let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in 175 State (sfrs, graph, lbl, sp, lenv, carry, mem, trace) 160 176 161 177 | RTL.St_call_id (f, args, ret_regs, lbl) -> … … 163 179 let args = get_arg_values lenv args in 164 180 let sf = 165 { ret_regs = ret_regs ; graph = c; pc = lbl ;181 { ret_regs = ret_regs ; graph = graph ; pc = lbl ; 166 182 sp = sp ; lenv = lenv ; carry = carry } 167 183 in 168 CallState (sf :: cs, f_def, args, mem, t)184 CallState (sf :: sfrs, f_def, args, mem, trace) 169 185 170 186 | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) -> … … 172 188 let f_def = Mem.find_fun_def mem addr in 173 189 let args = get_arg_values lenv args in 174 let sf = { ret_regs = ret_regs ; graph = c; pc = lbl ;190 let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ; 175 191 sp = sp ; lenv = lenv ; carry = carry } in 176 CallState (sf :: cs, f_def, args, mem, t)192 CallState (sf :: sfrs, f_def, args, mem, trace) 177 193 178 194 | RTL.St_tailcall_id (f, args) -> … … 180 196 let args = get_arg_values lenv args in 181 197 let mem = Mem.free mem sp in 182 CallState ( cs, f_def, args, mem, t)198 CallState (sfrs, f_def, args, mem, trace) 183 199 184 200 | RTL.St_tailcall_ptr (f1, f2, args) -> … … 187 203 let args = get_arg_values lenv args in 188 204 let mem = Mem.free mem sp in 189 CallState ( cs, f_def, args, mem, t)205 CallState (sfrs, f_def, args, mem, trace) 190 206 191 207 | RTL.St_condacc (srcr, lbl_true, lbl_false) -> 192 208 let v = get_local_value lenv srcr in 193 branch_state cs c lbl_true lbl_false sp lenv carry mem tv209 branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v 194 210 195 211 | RTL.St_return rl -> 196 212 let vl = List.map (get_local_value lenv) rl in 197 213 let mem = Mem.free mem sp in 198 ReturnState (cs, vl, mem, t) 199 200 201 let get_int () = 202 try Val.of_int (int_of_string (read_line ())) 203 with Failure "int_of_string" -> error "Failed to scan an integer." 204 let get_float () = 205 try Val.of_float (float_of_string (read_line ())) 206 with Failure "float_of_string" -> error "Failed to scan a float." 207 208 let interpret_external 209 (mem : memory) 210 (def : AST.external_function) 211 (args : Val.t list) : 212 memory * Val.t list = 213 match def.AST.ef_tag, args with 214 | s, _ when s = Primitive.scan_int -> 215 (mem, [get_int ()]) 216 | "scan_float", _ -> 217 (mem, [get_float ()]) 218 | s, v :: _ when s = Primitive.print_int && Val.is_int v -> 219 Printf.printf "%d" (Val.to_int v) ; 220 (mem, [Val.zero]) 221 | "print_float", v :: _ when Val.is_float v -> 222 Printf.printf "%f" (Val.to_float v) ; 223 (mem, [Val.zero]) 224 | "print_ptr", v :: _ when Val.is_pointer v -> 225 let (b, off) = Val.to_pointer v in 226 Printf.printf "block: %s, offset: %s" 227 (Val.Block.to_string b) (Val.Offset.to_string off) ; 228 (mem, [Val.zero]) 229 | s, v :: _ when s = Primitive.print_intln && Val.is_int v -> 230 Printf.printf "%d\n" (Val.to_int v) ; 231 (mem, [Val.zero]) 232 | "print_floatln", v :: _ when Val.is_float v -> 233 Printf.printf "%f" (Val.to_float v) ; 234 (mem, [Val.zero]) 235 | "print_ptrln", v :: _ when Val.is_pointer v -> 236 let (b, off) = Val.to_pointer v in 237 Printf.printf "block: %s, offset: %s\n" 238 (Val.Block.to_string b) (Val.Offset.to_string off) ; 239 (mem, [Val.zero]) 240 | s, v :: _ when s = Primitive.alloc -> 241 let (mem, ptr) = Mem.alloc mem (Val.to_int v) in 242 let vs = Val.break ptr 2 in 243 (mem, vs) 244 | s, v1 :: v2 :: _ when s = Primitive.modulo -> 245 (mem, [Val.modulo v1 v2]) 246 247 (* The other cases are either a type error (only integers and pointers 248 may not be differenciated during type checking) or an unknown 249 function. *) 250 | "print_int", _ | "print_intln", _ -> 251 error "Illegal cast from pointer to integer." 252 | "print_ptr", _ | "print_ptrln", _ -> 253 error "Illegal cast from integer to pointer." 254 | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".") 214 ReturnState (sfrs, vl, mem, trace) 215 216 217 module InterpretExternal = Primitive.Interpret (Mem) 218 219 let interpret_external mem f args = match InterpretExternal.t mem f args with 220 | (mem', InterpretExternal.V v) -> (mem', [v]) 221 | (mem', InterpretExternal.A addr) -> (mem', addr) 255 222 256 223 let init_locals … … 265 232 266 233 let state_after_call 267 ( cs: stack_frame list)234 (sfrs : stack_frame list) 268 235 (f_def : RTL.function_def) 269 236 (args : Val.t list) 270 237 (mem : memory) 271 (t 238 (trace : CostLabel.t list) : 272 239 state = 273 240 match f_def with 274 241 | RTL.F_int def -> 275 242 let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in 276 State ( cs, def.RTL.f_graph, def.RTL.f_entry, sp,243 State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp, 277 244 init_locals def.RTL.f_locals def.RTL.f_params args, 278 Val.undef, mem', t )245 Val.undef, mem', trace) 279 246 | RTL.F_ext def -> 280 let (mem', vs) = interpret_external mem def args in281 ReturnState ( cs, vs, mem', t)247 let (mem', vs) = interpret_external mem def.AST.ef_tag args in 248 ReturnState (sfrs, vs, mem', trace) 282 249 283 250 let state_after_return 284 251 (sf : stack_frame) 285 ( cs: stack_frame list)252 (sfrs : stack_frame list) 286 253 (ret_vals : Val.t list) 287 254 (mem : memory) 288 (t 255 (trace : CostLabel.t list) : 289 256 state = 290 257 let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in 291 258 let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in 292 State ( cs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, t)259 State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace) 293 260 294 261 295 262 let small_step (st : state) : state = match st with 296 | State ( cs, graph, pc, sp, lenv, carry, mem, t) ->263 | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) -> 297 264 let stmt = Label.Map.find pc graph in 298 interpret_statement cs graph sp lenv carry mem stmt t299 | CallState ( cs, f_def, args, mem, t) ->300 state_after_call cs f_def args mem t301 | ReturnState ([], ret_vals, mem, t ) ->265 interpret_statement sfrs graph sp lenv carry mem stmt trace 266 | CallState (sfrs, f_def, args, mem, trace) -> 267 state_after_call sfrs f_def args mem trace 268 | ReturnState ([], ret_vals, mem, trace) -> 302 269 assert false (* End of execution; handled in iter_small_step. *) 303 | ReturnState (sf :: cs, ret_vals, mem, t) -> 304 state_after_return sf cs ret_vals mem t 305 306 307 let print_args = MiscPottier.string_of_list ", " Val.to_string 308 let print_ret_vals = MiscPottier.string_of_list ", " Val.to_string 309 let print_lenv = 310 Register.Map.iter (fun r v -> Printf.printf "%s = %s\n%!" 311 (Register.print r) (Val.to_string v)) 270 | ReturnState (sf :: sfrs, ret_vals, mem, trace) -> 271 state_after_return sf sfrs ret_vals mem trace 272 312 273 313 274 let compute_result vs = 314 275 try 315 let v = MiscPottier.lastvs in276 let v = List.hd vs in 316 277 if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v) 317 278 else IntValue.Int8.zero 318 279 with Not_found -> IntValue.Int8.zero 319 280 320 let rec iter_small_step print_result st = match small_step st with 321 (* 322 (* <DEBUG> *) 323 | ReturnState ([], vs, mem, t) -> 324 Mem.print mem ; 325 Printf.printf "Return: %s\n%!" (print_ret_vals vs) ; 326 List.rev t 327 | CallState (_, _, args, mem, _) as st' -> 328 Printf.printf "Call state: %s\n%!" (print_args args) ; 329 Mem.print mem ; 330 iter_small_step st' 331 | ReturnState (_, ret_vals, mem, _) as st' -> 332 Printf.printf "Return state: %s\n%!" (print_ret_vals ret_vals) ; 333 Mem.print mem ; 334 iter_small_step st' 335 | State (_, _, pc, sp, lenv, carry, mem, _) as st' -> 336 Printf.printf "State: PC = %s ; SP = %s\n%!" pc (Val.to_string sp) ; 337 Mem.print mem ; 338 print_lenv lenv ; 339 Printf.printf "Carry = %s\n\n%!" (Val.to_string carry) ; 340 iter_small_step st' 341 (* </DEBUG> *) 342 *) 343 | ReturnState ([], vs, mem, t) -> 344 let (res, cost_labels) as trace = (compute_result vs, List.rev t) in 345 if print_result then 346 Printf.printf "RTL: %s\n%!" (IntValue.Int8.to_string res) ; 347 trace 348 | st' -> iter_small_step print_result st' 281 let rec iter_small_step debug st = 282 if debug then print_state st ; 283 match small_step st with 284 | ReturnState ([], vs, mem, trace) -> (compute_result vs, List.rev trace) 285 | st' -> iter_small_step debug st' 349 286 350 287 … … 357 294 358 295 359 (* The memory is initialized by load the code into it, and by reserving space296 (* The memory is initialized by loading the code into it, and by reserving space 360 297 for the global variables. *) 361 298 … … 366 303 (* Interpret the program only if it has a main. *) 367 304 368 let interpret print_result p = match p.RTL.main with 369 | None -> (IntValue.Int8.zero, []) 370 | Some main -> 371 let mem = init_mem p in 372 let main_def = find_function mem main in 373 let st = CallState ([], main_def, [], mem, []) in 374 iter_small_step print_result st 305 let interpret debug p = 306 if debug then Printf.printf "*** RTL ***\n\n%!" ; 307 match p.RTL.main with 308 | None -> (IntValue.Int8.zero, []) 309 | Some main -> 310 let mem = init_mem p in 311 let main_def = find_function mem main in 312 let st = CallState ([], main_def, [], mem, []) in 313 iter_small_step debug st -
Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml
r624 r740 110 110 let (def, tmpr) = fresh_reg def in 111 111 adds_graph 112 [ERTL.St_framesize (addr 2, start_lbl) ;112 [ERTL.St_framesize (addr1, start_lbl) ; 113 113 ERTL.St_int (tmpr, off+I8051.int_size, start_lbl) ; 114 ERTL.St_op2 (I8051.Sub, addr 2, addr2, tmpr, start_lbl) ;114 ERTL.St_op2 (I8051.Sub, addr1, addr1, tmpr, start_lbl) ; 115 115 ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ; 116 ERTL.St_op2 (I8051.Add, addr 2, addr2, tmpr, start_lbl) ;117 ERTL.St_int (addr 1, 0, start_lbl) ;116 ERTL.St_op2 (I8051.Add, addr1, addr1, tmpr, start_lbl) ; 117 ERTL.St_int (addr2, 0, start_lbl) ; 118 118 ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ; 119 ERTL.St_op2 (I8051.Addc, addr 1, addr1, tmpr, start_lbl) ;119 ERTL.St_op2 (I8051.Addc, addr2, addr2, tmpr, start_lbl) ; 120 120 ERTL.St_load (destr, addr1, addr2, start_lbl)] 121 121 start_lbl dest_lbl def … … 137 137 (get_params_hdw hdw_params) @ (get_params_stack stack_params) 138 138 139 let add_prologue params sra h sralsregs def =139 let add_prologue params sral srah sregs def = 140 140 let start_lbl = def.ERTL.f_entry in 141 141 let tmp_lbl = fresh_label def in … … 174 174 let (def, r_tmp) = fresh_reg def in 175 175 adds_graph [ERTL.St_int (r_tmp, 0, start_lbl) ; 176 ERTL.St_set_hdw (I8051.st 1, r_tmp, start_lbl) ;177 ERTL.St_set_hdw (I8051.st 0, r, start_lbl)]176 ERTL.St_set_hdw (I8051.st0, r, start_lbl) ; 177 ERTL.St_set_hdw (I8051.st1, r_tmp, start_lbl)] 178 178 start_lbl dest_lbl def] 179 179 | r1 :: r2 :: _ -> 180 180 [(fun start_lbl -> 181 adds_graph [ERTL.St_set_hdw (I8051.st 1, r1, start_lbl) ;182 ERTL.St_set_hdw (I8051.st 0, r2, start_lbl)] start_lbl)]183 184 let add_epilogue ret_regs sra h sralsregs def =181 adds_graph [ERTL.St_set_hdw (I8051.st0, r1, start_lbl) ; 182 ERTL.St_set_hdw (I8051.st1, r2, start_lbl)] start_lbl)] 183 184 let add_epilogue ret_regs sral srah sregs def = 185 185 let start_lbl = def.ERTL.f_exit in 186 186 let tmp_lbl = fresh_label def in … … 204 204 (* assign the result to actual return registers *) 205 205 [adds_graph [ERTL.St_comment ("Set result", start_lbl)]] @ 206 [adds_graph [ERTL.St_hdw_to_hdw (I8051.dp h, I8051.st1, start_lbl) ;207 ERTL.St_hdw_to_hdw (I8051.dp l, I8051.st0, 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 208 ERTL.St_comment ("End Epilogue", start_lbl)]]) 209 209 start_lbl tmp_lbl def in … … 221 221 (* Allocate registers to hold the return address. *) 222 222 let (def, sra) = fresh_regs def 2 in 223 let sra h= List.nth sra 0 in224 let sra l= List.nth sra 1 in223 let sral = List.nth sra 0 in 224 let srah = List.nth sra 1 in 225 225 (* Allocate registers to save callee-saved registers. *) 226 226 let (def, sregs) = allocate_regs I8051.callee_saved def in 227 227 (* Add a prologue and a epilogue. *) 228 let def = add_prologue params sra h sralsregs def in229 let def = add_epilogue ret_regs sra h sralsregs def in228 let def = add_prologue params sral srah sregs def in 229 let def = add_epilogue ret_regs sral srah sregs def in 230 230 def 231 231 … … 246 246 ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ; 247 247 ERTL.St_clear_carry start_lbl ; 248 ERTL.St_op2 (I8051.Sub, addr1, tmpr, addr1, start_lbl) ; 249 ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ; 250 ERTL.St_int (addr2, 0, start_lbl) ; 248 251 ERTL.St_op2 (I8051.Sub, addr2, tmpr, addr2, start_lbl) ; 249 ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;250 ERTL.St_int (addr1, 0, start_lbl) ;251 ERTL.St_op2 (I8051.Sub, addr1, tmpr, addr1, start_lbl) ;252 252 ERTL.St_store (addr1, addr2, srcr, start_lbl)] 253 253 start_lbl dest_lbl def … … 284 284 | r1 :: r2 :: _ -> 285 285 adds_graph 286 [ERTL.St_hdw_to_hdw (I8051.st 1, I8051.dph, start_lbl) ;287 ERTL.St_hdw_to_hdw (I8051.st 0, I8051.dpl, start_lbl) ;288 ERTL.St_get_hdw (r1, I8051.st 1, start_lbl) ;289 ERTL.St_get_hdw (r2, I8051.st 0, start_lbl)]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 290 start_lbl 291 291 … … 319 319 | RTL.St_addr (r1, r2, x, lbl') -> 320 320 adds_graph 321 [ERTL.St_addr H (r1, x, lbl) ; ERTL.St_addrL(r2, x, lbl) ;]321 [ERTL.St_addrL (r1, x, lbl) ; ERTL.St_addrH (r2, x, lbl) ;] 322 322 lbl lbl' def 323 323 324 324 | RTL.St_stackaddr (r1, r2, lbl') -> 325 325 adds_graph 326 [ERTL.St_get_hdw (r1, I8051.sp h, lbl) ;327 ERTL.St_get_hdw (r2, I8051.sp l, lbl)]326 [ERTL.St_get_hdw (r1, I8051.spl, lbl) ; 327 ERTL.St_get_hdw (r2, I8051.sph, lbl)] 328 328 lbl lbl' def 329 329 -
Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli
r486 r740 9 9 RTLabs is the last language of the frontend. It is intended to 10 10 ease retargetting. *) 11 12 13 (* From the RTLabs point of view, a pseudo-register can represent a physical14 location or a pointer. When instruction selection is over, a pseudo-register15 represents a physical location. Thus, some operations --- those on pointers16 --- may involve several pseudo-registers when a pointer value is more than17 one physical location (which is the case of the 8051). *)18 19 type registers = Register.t list20 11 21 12 … … 52 43 | St_cost of CostLabel.t * Label.t 53 44 54 (* Assign a constant to registers. Parameters are the destination register s,45 (* Assign a constant to registers. Parameters are the destination register, 55 46 the constant and the label of the next statement. *) 56 | St_cst of registers* AST.cst * Label.t47 | St_cst of Register.t * AST.cst * Label.t 57 48 58 49 (* Application of an unary operation. Parameters are the operation, the 59 destination register s, the argument registersand the label of the next50 destination register, the argument register and the label of the next 60 51 statement. *) 61 | St_op1 of AST.op1 * registers * registers* Label.t52 | St_op1 of AST.op1 * Register.t * Register.t * Label.t 62 53 63 54 (* Application of a binary operation. Parameters are the operation, the 64 destination register, the argument registers and the label of the next55 destination register, the two argument registers and the label of the next 65 56 statement. *) 66 | St_op2 of AST.op2 * registers * registers * registers* Label.t57 | St_op2 of AST.op2 * Register.t * Register.t * Register.t * Label.t 67 58 68 (* Memory load. Parameters are the size and type of what to load,69 the addressing mode and its arguments, the destination register70 and the labelof the next statement. *)71 | St_load of Memory. memory_q * addressing * registers list *72 registers *Label.t59 (* Memory load. Parameters are the size in bytes of what to load, the 60 addressing mode and its arguments, the destination register and the label 61 of the next statement. *) 62 | St_load of Memory.quantity * addressing * Register.t list * Register.t * 63 Label.t 73 64 74 (* Memory store. Parameters are the size and type of what to store,75 the addressing mode and its arguments, the source register76 and the label of thenext statement. *)77 | St_store of Memory. memory_q * addressing * registers list *78 registers *Label.t65 (* 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 the 67 next statement. *) 68 | St_store of Memory.quantity * addressing * Register.t list * Register.t * 69 Label.t 79 70 80 71 (* Call to a function given its name. Parameters are the name of the 81 72 function, the arguments of the function, the destination 82 register s, the signature of the function and the label of the next73 register, the signature of the function and the label of the next 83 74 statement. *) 84 | St_call_id of AST.ident * registers list * registers*75 | St_call_id of AST.ident * Register.t list * Register.t * 85 76 AST.signature * Label.t 86 77 87 (* Call to a function given its address. Parameters are registers78 (* Call to a function given its address. Parameters are the register 88 79 holding the address of the function, the arguments of the 89 function, the destination register s, the signature of the function80 function, the destination register, the signature of the function 90 81 and the label of the next statement. This statement with an 91 82 [St_op] before can represent a [St_call_id]. However, we 92 83 differenciate the two to allow translation to a formalism with no 93 84 function pointer. *) 94 | St_call_ptr of registers * registers list * registers*85 | St_call_ptr of Register.t * Register.t list * Register.t * 95 86 AST.signature * Label.t 96 87 97 (* Tail call to a function given its name. Parameters are the name 98 of the function, the arguments of the function, the destination 99 register, the signature of the function and the label of the next 100 statement. *) 101 | St_tailcall_id of AST.ident * registers list * AST.signature 88 (* Tail call to a function given its name. Parameters are the name of the 89 function, the arguments of the function, the signature of the function and 90 the label of the next statement. *) 91 | St_tailcall_id of AST.ident * Register.t list * AST.signature 102 92 103 (* Tail call to a function given its address. Parameters are a 104 register holding the address of the function, the arguments of 105 the function, the destination register, the signature of the 106 function and the label of the next statement. Same remark as for 107 the [St_call_ptr]. *) 108 | St_tailcall_ptr of registers * registers list * AST.signature 93 (* Tail call to a function given its address. Parameters are a register 94 holding the address of the function, the arguments of the function, the 95 signature of the function and the label of the next statement. Same remark 96 as for the [St_call_ptr]. *) 97 | St_tailcall_ptr of Register.t * Register.t list * AST.signature 109 98 110 99 (* Constant branch. Parameters are the constant, the label to go to when the … … 117 106 true (not 0), and the label to go to when the operation on the 118 107 argument evaluates to false (0). *) 119 | St_cond1 of AST.op1 * registers* Label.t * Label.t108 | St_cond1 of AST.op1 * Register.t * Label.t * Label.t 120 109 121 110 (* Binary branch. Parameters are the operation, its arguments, the … … 123 112 true (not 0), and the label to go to when the operation on the 124 113 arguments evaluates to false (0). *) 125 | St_cond2 of AST.op2 * registers * registers* Label.t * Label.t114 | St_cond2 of AST.op2 * Register.t * Register.t * Label.t * Label.t 126 115 127 116 (* Jump statement. Parameters are a register and a list of 128 117 labels. The execution will go to the [n]th label of the list of 129 118 labels, where [n] is the natural value held in the register. *) 130 | St_jumptable of registers* Label.t list119 | St_jumptable of Register.t * Label.t list 131 120 132 121 (* Return statement. *) 133 | St_return of registers122 | St_return of Register.t 134 123 135 124 … … 140 129 f_runiverse : Register.universe ; 141 130 f_sig : AST.signature ; 142 f_result : registers ; 143 f_params : registers list ; 144 f_locals : registers list ; 131 f_result : Register.t ; 132 f_params : Register.t list ; 133 f_locals : Register.t list ; 134 f_ptrs : Register.t list ; 145 135 f_stacksize : int ; 146 136 f_graph : graph ; -
Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml
r619 r740 9 9 module Mem = Driver.RTLabsMemory 10 10 module Val = Mem.Value 11 12 let error_float () = error "float not supported" 11 13 12 14 … … 25 27 26 28 type stack_frame = 27 { ret_reg s : Register.t list ;29 { ret_reg : Register.t ; 28 30 graph : RTLabs.graph ; 29 sp : Val. t;31 sp : Val.address ; 30 32 pc : Label.t ; 31 33 lenv : local_env } … … 37 39 38 40 type state = 39 | State of stack_frame list * RTLabs.graph * Val. t(* stack pointer *) *41 | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) * 40 42 Label.t * local_env * memory * CostLabel.t list 41 43 | CallState of stack_frame list * RTLabs.function_def * … … 44 46 memory * CostLabel.t list 45 47 48 let string_of_local_env lenv = 49 let f x v s = 50 s ^ 51 (if Val.eq v Val.undef then "" 52 else (Register.print x) ^ " = " ^ (Val.to_string v) ^ " ") in 53 Register.Map.fold f lenv "" 54 55 let string_of_args args = 56 let f s v = s ^ " " ^ (Val.to_string v) in 57 List.fold_left f "" args 58 59 let print_state = function 60 | State (_, _, sp, lbl, lenv, mem, _) -> 61 Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!" 62 (Val.string_of_address sp) 63 (string_of_local_env lenv) 64 (Mem.to_string mem) 65 lbl 66 | CallState (_, _, args, mem, _) -> 67 Printf.printf "Memory:%s\nCall state: %s\n\n%!" 68 (Mem.to_string mem) 69 (string_of_args args) 70 | ReturnState (_, v, mem, _) -> 71 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 72 (Mem.to_string mem) 73 (Val.to_string v) 74 46 75 47 76 let find_function mem f = 48 let v= Mem.find_global mem f in49 Mem.find_fun_def mem v77 let addr = Mem.find_global mem f in 78 Mem.find_fun_def mem addr 50 79 51 80 let get_local_value (lenv : local_env) (r : Register.t) : Val.t = … … 54 83 let get_arg_values lenv args = List.map (get_local_value lenv) args 55 84 56 let get_local_valuel (lenv : local_env) (rl : Register.t list) : Val.t = 57 let vl = List.map (get_local_value lenv) rl in 58 Val.merge vl 59 let get_arg_valuesl lenv argsl = List.map (get_local_valuel lenv) argsl 60 61 (* An address is represented by two pseudo-registers (because in 8051, addresses 62 are coded on two bytes). Thus, assignments may involve several 63 registers. When we want to assign a single value to several registers, we 64 break the value into as many parts as there are registers, and then we update 65 each register with a part of the value. *) 66 67 let adds rs v lenv = match rs with 68 | [] -> lenv 69 | _ -> 70 let vs = Val.break v (List.length rs) in 71 let f lenv r v = Register.Map.add r v lenv in 72 List.fold_left2 f lenv rs vs 85 let adds rs vs lenv = 86 let f lenv r v = Register.Map.add r v lenv in 87 List.fold_left2 f lenv rs vs 88 89 let value_of_address = List.hd 90 let address_of_value v = [v] 73 91 74 92 75 93 let eval_addressing 76 94 (mem : memory) 77 (sp : Val. t)95 (sp : Val.address) 78 96 (mode : RTLabs.addressing) 79 97 (args : Val.t list) : 80 Val.t = match mode, args with 81 82 | RTLabs.Aindexed off, addr :: _ when Val.is_pointer addr -> 83 Val.add addr (Val.of_int off) 84 85 | RTLabs.Aindexed2, addr :: shift :: _ 86 when Val.is_pointer addr && Val.is_int shift -> 87 Val.add addr shift 88 89 | RTLabs.Aindexed2, shift :: addr :: _ 90 when Val.is_pointer addr && Val.is_int shift -> 91 Val.add addr shift 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) 92 105 93 106 | RTLabs.Aglobal (id, off), _ -> 94 Val.add (Mem.find_global mem id) (Val.of_int off)107 Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off) 95 108 96 109 | RTLabs.Abased (id, off), v :: _ -> 97 let addr = Val.add (Mem.find_global mem id) (Val.of_int off) in 98 Val.add addr 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) 99 113 100 114 | RTLabs.Ainstack off, _ -> 101 Val.add sp (Val.of_int off)115 Val.add_address sp (Val.Offset.of_int off) 102 116 103 117 | _, _ -> error "Bad addressing mode." … … 106 120 let eval_cst mem sp = function 107 121 | AST.Cst_int i -> Val.of_int i 108 | AST.Cst_float f -> Val.of_float f 109 | AST.Cst_addrsymbol id -> Mem.find_global mem id 110 | AST.Cst_stackoffset shift -> Val.add sp (Val.of_int shift) 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)) 111 126 112 127 let eval_op1 = function … … 118 133 | AST.Op_notbool -> Val.notbool 119 134 | AST.Op_notint -> Val.notint 120 | AST.Op_negf -> Val.negf121 | AST.Op_absf -> Val.absf122 | AST.Op_singleoffloat -> Val.singleoffloat123 | AST.Op_intoffloat -> Val.intoffloat124 | AST.Op_intuoffloat -> Val.intuoffloat125 | AST.Op_floatofint -> Val.floatofint126 | AST.Op_floatofintu -> Val.floatofintu135 | 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 () 127 142 | AST.Op_id -> (fun (v : Val.t) -> v) 128 | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO ? *)143 | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO or not? *) 129 144 130 145 let rec eval_op2 = function … … 142 157 | AST.Op_shr -> Val.shr 143 158 | AST.Op_shru -> Val.shru 144 | AST.Op_addf -> Val.addf145 | AST.Op_subf -> Val.subf146 | AST.Op_mulf -> Val.mulf147 | AST.Op_divf -> Val.divf148 159 | AST.Op_cmp AST.Cmp_eq -> Val.cmp_eq 149 160 | AST.Op_cmp AST.Cmp_ne -> Val.cmp_ne … … 158 169 | AST.Op_cmpu AST.Cmp_gt -> Val.cmp_gt_u 159 170 | AST.Op_cmpu AST.Cmp_ge -> Val.cmp_ge_u 160 | AST.Op_cmpf AST.Cmp_eq -> Val.cmp_eq_f161 | AST.Op_cmpf AST.Cmp_ne -> Val.cmp_ne_f162 | AST.Op_cmpf AST.Cmp_lt -> Val.cmp_lt_f163 | AST.Op_cmpf AST.Cmp_le -> Val.cmp_le_f164 | AST.Op_cmpf AST.Cmp_gt -> Val.cmp_gt_f165 | AST.Op_cmpf AST.Cmp_ge -> Val.cmp_ge_f166 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 () 167 177 168 178 (* Assign a value to some destinations registers. *) 169 179 170 let assign_state cs c sp lbl lenv mem t destrsv =171 let lenv = adds destrsv lenv in172 State ( cs, c, sp, lbl, lenv, mem, t)180 let assign_state sfrs graph sp lbl lenv mem trace destr v = 181 let lenv = Register.Map.add destr v lenv in 182 State (sfrs, graph, sp, lbl, lenv, mem, trace) 173 183 174 184 (* Branch on a value. *) 175 185 176 let branch_state cs c sp lbl_true lbl_false lenv mem tv =186 let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v = 177 187 let next_lbl = 178 188 if Val.is_true v then lbl_true … … 180 190 if Val.is_false v then lbl_false 181 191 else error "Undefined conditional value." in 182 State ( cs, c, sp, next_lbl, lenv, mem, t)192 State (sfrs, graph, sp, next_lbl, lenv, mem, trace) 183 193 184 194 … … 186 196 187 197 let interpret_statement 188 ( cs: stack_frame list)189 ( c: RTLabs.graph)190 (sp : Val.t)191 (lenv : local_env)192 (mem : memory)193 (stmt : RTLabs.statement)194 (t 198 (sfrs : stack_frame list) 199 (graph : RTLabs.graph) 200 (sp : Val.address) 201 (lenv : local_env) 202 (mem : memory) 203 (stmt : RTLabs.statement) 204 (trace : CostLabel.t list) : 195 205 state = match stmt with 196 206 197 | RTLabs.St_skip lbl -> State ( cs, c, sp, lbl, lenv, mem, t)207 | RTLabs.St_skip lbl -> State (sfrs, graph, sp, lbl, lenv, mem, trace) 198 208 199 209 | RTLabs.St_cost (cost_lbl, lbl) -> 200 State ( cs, c, sp, lbl, lenv, mem, cost_lbl :: t)201 202 | RTLabs.St_cst (destr s, cst, lbl) ->210 State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace) 211 212 | RTLabs.St_cst (destr, cst, lbl) -> 203 213 let v = eval_cst mem sp cst in 204 assign_state cs c sp lbl lenv mem t destrsv205 206 | RTLabs.St_op1 (op1, destr s, srcrs, lbl) ->207 let v = eval_op1 op1 (get_local_value l lenv srcrs) in208 assign_state cs c sp lbl lenv mem t destrsv209 210 | RTLabs.St_op2 (op2, destr s, srcrs1, srcrs2, lbl) ->214 assign_state sfrs graph sp lbl lenv mem trace destr v 215 216 | RTLabs.St_op1 (op1, destr, srcr, lbl) -> 217 let v = eval_op1 op1 (get_local_value lenv srcr) in 218 assign_state sfrs graph sp lbl lenv mem trace destr v 219 220 | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) -> 211 221 let v = 212 222 eval_op2 op2 213 (get_local_valuel lenv srcrs1) 214 (get_local_valuel lenv srcrs2) in 215 assign_state cs c sp lbl lenv mem t destrs v 216 217 | RTLabs.St_load (chunk, mode, args, destrs, lbl) -> 218 let addr = eval_addressing mem sp mode (get_arg_valuesl lenv args) in 219 let v = Mem.load mem chunk addr in 220 assign_state cs c sp lbl lenv mem t destrs v 221 222 | RTLabs.St_store (chunk, mode, args, srcrs, lbl) -> 223 let addr = eval_addressing mem sp mode (get_arg_valuesl lenv args) in 224 let mem = Mem.store mem chunk addr (get_local_valuel lenv srcrs) in 225 State (cs, c, sp, lbl, lenv, mem, t) 223 (get_local_value lenv srcr1) 224 (get_local_value lenv srcr2) in 225 assign_state sfrs graph sp lbl lenv mem trace destr v 226 227 | RTLabs.St_load (q, mode, args, destr, lbl) -> 228 let addr = eval_addressing mem sp mode (get_arg_values lenv args) in 229 let v = Mem.loadq mem q addr in 230 assign_state sfrs graph sp lbl lenv mem trace destr v 231 232 | RTLabs.St_store (q, mode, args, srcr, lbl) -> 233 let addr = eval_addressing mem sp mode (get_arg_values lenv args) in 234 let v = get_local_value lenv srcr in 235 let mem = Mem.storeq mem q addr v in 236 State (sfrs, graph, sp, lbl, lenv, mem, trace) 226 237 227 238 | RTLabs.St_call_id (f, args, destr, sg, lbl) -> 228 239 let f_def = find_function mem f in 229 let args = get_arg_values llenv args in240 let args = get_arg_values lenv args in 230 241 (* Save the stack frame. *) 231 242 let sf = 232 { ret_reg s = destr ; graph = c; sp = sp ; pc = lbl ; lenv = lenv }243 { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } 233 244 in 234 CallState (sf :: cs, f_def, args, mem, t)235 236 | RTLabs.St_call_ptr (r s, args, destrs, sg, lbl) ->237 let addr = get_local_value l lenv rsin238 let f_def = Mem.find_fun_def mem addrin239 let args = get_arg_values llenv args in245 CallState (sf :: sfrs, f_def, args, mem, trace) 246 247 | RTLabs.St_call_ptr (r, args, destr, sg, lbl) -> 248 let addr = get_local_value lenv r in 249 let f_def = Mem.find_fun_def mem (address_of_value addr) in 250 let args = get_arg_values lenv args in 240 251 (* Save the stack frame. *) 241 252 let sf = 242 { ret_reg s = destrs ; graph = c; sp = sp ; pc = lbl ; lenv = lenv }253 { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv } 243 254 in 244 CallState (sf :: cs, f_def, args, mem, t)255 CallState (sf :: sfrs, f_def, args, mem, trace) 245 256 246 257 | RTLabs.St_tailcall_id (f, args, sg) -> 247 258 let f_def = find_function mem f in 248 let args = get_arg_values llenv args in259 let args = get_arg_values lenv args in 249 260 (* No need to save the stack frame. But free the stack. *) 250 261 let mem = Mem.free mem sp in 251 CallState ( cs, f_def, args, mem, t)252 253 | RTLabs.St_tailcall_ptr (r s, args, sg) ->254 let addr = get_local_value l lenv rsin255 let f_def = Mem.find_fun_def mem addrin256 let args = get_arg_values llenv args in262 CallState (sfrs, f_def, args, mem, trace) 263 264 | RTLabs.St_tailcall_ptr (r, args, sg) -> 265 let addr = get_local_value lenv r in 266 let f_def = Mem.find_fun_def mem (address_of_value addr) in 267 let args = get_arg_values lenv args in 257 268 (* No need to save the stack frame. But free the stack. *) 258 269 let mem = Mem.free mem sp in 259 CallState ( cs, f_def, args, mem, t)270 CallState (sfrs, f_def, args, mem, trace) 260 271 261 272 | RTLabs.St_condcst (cst, lbl_true, lbl_false) -> 262 273 let v = eval_cst mem sp cst in 263 branch_state cs c sp lbl_true lbl_false lenv mem tv264 265 | RTLabs.St_cond1 (op1, srcr s, lbl_true, lbl_false) ->266 let v = eval_op1 op1 (get_local_value l lenv srcrs) in267 branch_state cs c sp lbl_true lbl_false lenv mem tv268 269 | RTLabs.St_cond2 (op2, srcr s1, srcrs2, lbl_true, lbl_false) ->274 branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v 275 276 | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) -> 277 let v = eval_op1 op1 (get_local_value lenv srcr) in 278 branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v 279 280 | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) -> 270 281 let v = 271 282 eval_op2 op2 272 (get_local_value l lenv srcrs1)273 (get_local_value l lenv srcrs2) in274 branch_state cs c sp lbl_true lbl_false lenv mem tv275 276 | RTLabs.St_jumptable (r, table) -> assert false (* TODO *)283 (get_local_value lenv srcr1) 284 (get_local_value lenv srcr2) in 285 branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v 286 287 | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *) 277 288 (* 278 289 let i = match get_local_value lenv r with … … 282 293 (try 283 294 let next_lbl = List.nth table i in 284 State ( cs, c, sp, next_lbl, lenv, mem, t)295 State (sfrs, graph, sp, next_lbl, lenv, mem, trace) 285 296 with 286 297 | Failure "nth" | Invalid_argument "List.nth" -> … … 288 299 *) 289 300 290 | RTLabs.St_return r s->291 let v = get_local_value l lenv rsin301 | RTLabs.St_return r -> 302 let v = get_local_value lenv r in 292 303 let mem = Mem.free mem sp in 293 ReturnState (cs, v, mem, t) 294 295 296 let get_int () = 297 try Val.of_int (int_of_string (read_line ())) 298 with Failure "int_of_string" -> error "Failed to scan an integer." 299 let get_float () = 300 try Val.of_float (float_of_string (read_line ())) 301 with Failure "float_of_string" -> error "Failed to scan a float." 302 303 let interpret_external 304 (mem : memory) 305 (def : AST.external_function) 306 (args : Val.t list) : 307 memory * Val.t = 308 match def.AST.ef_tag, args with 309 | s, _ when s = Primitive.scan_int -> 310 (mem, get_int ()) 311 | "scan_float", _ -> 312 (mem, get_float ()) 313 | s, v :: _ when s = Primitive.print_int && Val.is_int v -> 314 Printf.printf "%d" (Val.to_int v) ; 315 (mem, Val.zero) 316 | "print_float", v :: _ when Val.is_float v -> 317 Printf.printf "%f" (Val.to_float v) ; 318 (mem, Val.zero) 319 | "print_ptr", v :: _ when Val.is_pointer v -> 320 let (b, off) = Val.to_pointer v in 321 Printf.printf "block: %s, offset: %s" 322 (Val.Block.to_string b) (Val.Offset.to_string off) ; 323 (mem, Val.zero) 324 | s, v :: _ when s = Primitive.print_intln && Val.is_int v -> 325 Printf.printf "%d\n" (Val.to_int v) ; 326 (mem, Val.zero) 327 | "print_floatln", v :: _ when Val.is_float v -> 328 Printf.printf "%f" (Val.to_float v) ; 329 (mem, Val.zero) 330 | "print_ptrln", v :: _ when Val.is_pointer v -> 331 let (b, off) = Val.to_pointer v in 332 Printf.printf "block: %s, offset: %s\n" 333 (Val.Block.to_string b) (Val.Offset.to_string off) ; 334 (mem, Val.zero) 335 | s, v :: _ when s = Primitive.alloc -> 336 let (mem, ptr) = Mem.alloc mem (Val.to_int v) in 337 (mem, ptr) 338 | s, v1 :: v2 :: _ when s = Primitive.modulo -> 339 (mem, Val.modulo v1 v2) 340 341 (* The other cases are either a type error (only integers and pointers 342 may not be differenciated during type checking) or an unknown 343 function. *) 344 | "print_int", _ | "print_intln", _ -> 345 error "Illegal cast from pointer to integer." 346 | "print_ptr", _ | "print_ptrln", _ -> 347 error "Illegal cast from integer to pointer." 348 | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".") 349 304 ReturnState (sfrs, v, mem, trace) 305 306 307 module InterpretExternal = Primitive.Interpret (Mem) 308 309 let interpret_external mem f args = match InterpretExternal.t mem f args with 310 | (mem', InterpretExternal.V v) -> (mem', v) 311 | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) 350 312 351 313 let init_locals 352 (locals : Register.t list list)353 (params : Register.t list list)314 (locals : Register.t list) 315 (params : Register.t list) 354 316 (args : Val.t list) : 355 317 local_env = 356 let f lenv r s = adds rsVal.undef lenv in318 let f lenv r = Register.Map.add r Val.undef lenv in 357 319 let lenv = List.fold_left f Register.Map.empty locals in 358 let f lenv r s v = adds rsv lenv in320 let f lenv r v = Register.Map.add r v lenv in 359 321 List.fold_left2 f lenv params args 360 322 361 323 let state_after_call 362 ( cs: stack_frame list)324 (sfrs : stack_frame list) 363 325 (f_def : RTLabs.function_def) 364 326 (args : Val.t list) 365 327 (mem : memory) 366 (t 328 (trace : CostLabel.t list) : 367 329 state = 368 330 match f_def with 369 331 | RTLabs.F_int def -> 370 332 let (mem', sp) = Mem.alloc mem def.RTLabs.f_stacksize in 371 State ( cs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry,333 State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry, 372 334 init_locals def.RTLabs.f_locals def.RTLabs.f_params args, 373 mem', t )335 mem', trace) 374 336 | RTLabs.F_ext def -> 375 let (mem', v) = interpret_external mem def args in376 ReturnState ( cs, v, mem', t)337 let (mem', v) = interpret_external mem def.AST.ef_tag args in 338 ReturnState (sfrs, v, mem', trace) 377 339 378 340 379 341 let state_after_return 380 342 (sf : stack_frame) 381 ( cs: stack_frame list)343 (sfrs : stack_frame list) 382 344 (ret_val : Val.t) 383 345 (mem : memory) 384 (t 346 (trace : CostLabel.t list) : 385 347 state = 386 let lenv = adds sf.ret_regsret_val sf.lenv in387 State ( cs, sf.graph, sf.sp, sf.pc, lenv, mem, t)348 let lenv = Register.Map.add sf.ret_reg ret_val sf.lenv in 349 State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace) 388 350 389 351 390 352 let small_step (st : state) : state = match st with 391 | State ( cs, graph, sp, pc, lenv, mem, t) ->353 | State (sfrs, graph, sp, pc, lenv, mem, trace) -> 392 354 let stmt = Label.Map.find pc graph in 393 interpret_statement cs graph sp lenv mem stmt t394 | CallState ( cs, f_def, args, mem, t) ->395 state_after_call cs f_def args mem t396 | ReturnState ([], ret_val, mem, t ) ->355 interpret_statement sfrs graph sp lenv mem stmt trace 356 | CallState (sfrs, f_def, args, mem, trace) -> 357 state_after_call sfrs f_def args mem trace 358 | ReturnState ([], ret_val, mem, trace) -> 397 359 assert false (* End of execution; handled in iter_small_step. *) 398 | ReturnState (sf :: cs, ret_val, mem, t) ->399 state_after_return sf cs ret_val mem t360 | ReturnState (sf :: sfrs, ret_val, mem, trace) -> 361 state_after_return sf sfrs ret_val mem trace 400 362 401 363 … … 404 366 else IntValue.Int8.zero 405 367 406 let rec iter_small_step print_result st = match small_step st with 407 (* 408 (* <DEBUG> *) 409 | ReturnState ([], v, mem, t) -> 410 Mem.print mem ; 411 Printf.printf "Return: %s\n%!" (Val.to_string v) ; 412 List.rev t 413 | CallState (_, _, _, mem, _) 414 | ReturnState (_, _, mem, _) 415 | State (_, _, _, _, _, mem, _) as st' -> Mem.print mem ; iter_small_step st' 416 (* </DEBUG> *) 417 *) 418 | ReturnState ([], v, mem, t) -> 419 let (res, cost_labels) as trace = (compute_result v, List.rev t) in 420 if print_result then 421 Printf.printf "RTLabs: %s\n%!" (IntValue.Int8.to_string res) ; 422 trace 423 | st' -> iter_small_step print_result st' 368 let rec iter_small_step debug st = 369 if debug then print_state st ; 370 match small_step st with 371 | ReturnState ([], v, mem, trace) -> (compute_result v, List.rev trace) 372 | st' -> iter_small_step debug st' 424 373 425 374 … … 441 390 (* Interpret the program only if it has a main. *) 442 391 443 let interpret print_result p = match p.RTLabs.main with 444 | None -> (IntValue.Int8.zero, []) 445 | Some main -> 446 let mem = init_mem p in 447 let main_def = find_function mem main in 448 let st = CallState ([], main_def, [], mem, []) in 449 iter_small_step print_result st 392 let interpret debug p = 393 if debug then Printf.printf "*** RTLabs ***\n\n%!" ; 394 match p.RTLabs.main with 395 | None -> (IntValue.Int8.zero, []) 396 | Some main -> 397 let mem = init_mem p in 398 let main_def = find_function mem main in 399 let st = CallState ([], main_def, [], mem, []) in 400 iter_small_step debug st -
Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml
r486 r740 12 12 13 13 14 let print_reg_list rl = 15 Printf.sprintf "[%s]" (MiscPottier.string_of_list " ; " Register.print rl) 14 let print_reg = Register.print 16 15 17 16 let rec print_args args = 18 Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg_list args) 19 20 let print_result rl = print_reg_list rl 21 22 let print_params rl = 23 Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_reg_list rl) 24 25 let print_locals rl = 26 Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_reg_list rl) 27 28 29 let print_memory_q = Memory.string_of_memory_q 17 Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args) 18 19 let print_result r = print_reg r 20 21 let print_params r = 22 Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_reg r) 23 24 let print_locals r = 25 Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_reg r) 30 26 31 27 … … 59 55 | AST.Op_floatofint -> "floatofint" 60 56 | AST.Op_floatofintu -> "floatofintu" 61 | AST.Op_id -> " mov"57 | AST.Op_id -> "id" 62 58 | AST.Op_ptrofint -> "ptrofint" 63 59 | AST.Op_intofptr -> "intofptr" … … 107 103 | RTLabs.St_cost (cost_lbl, lbl) -> 108 104 Printf.sprintf "emit %s --> %s" cost_lbl lbl 109 | RTLabs.St_cst (dest s, cst, lbl) ->105 | RTLabs.St_cst (destr, cst, lbl) -> 110 106 Printf.sprintf "imm %s, %s --> %s" 111 (print_reg _list dests)107 (print_reg destr) 112 108 (print_cst cst) 113 109 lbl 114 | RTLabs.St_op1 (op1, dest s, srcs, lbl) ->110 | RTLabs.St_op1 (op1, destr, srcr, lbl) -> 115 111 Printf.sprintf "%s %s, %s --> %s" 116 112 (print_op1 op1) 117 (print_reg _list dests)118 (print_reg _list srcs)119 lbl 120 | RTLabs.St_op2 (op2, dest s, srcs1, srcs2, lbl) ->113 (print_reg destr) 114 (print_reg srcr) 115 lbl 116 | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) -> 121 117 Printf.sprintf "%s %s, %s, %s --> %s" 122 118 (print_op2 op2) 123 (print_reg _list dests)124 (print_reg _list srcs1)125 (print_reg _list srcs2)126 lbl 127 | RTLabs.St_load ( chunk, mode, args, dests, lbl) ->119 (print_reg destr) 120 (print_reg srcr1) 121 (print_reg srcr2) 122 lbl 123 | RTLabs.St_load (q, mode, args, destr, lbl) -> 128 124 Printf.sprintf "load %s, %s, %s, %s --> %s" 129 ( print_memory_q chunk)125 (Memory.string_of_quantity q) 130 126 (print_addressing mode) 131 127 (print_args args) 132 (print_reg _list dests)133 lbl 134 | RTLabs.St_store ( chunk, mode, args, srcs, lbl) ->128 (print_reg destr) 129 lbl 130 | RTLabs.St_store (q, mode, args, srcr, lbl) -> 135 131 Printf.sprintf "store %s, %s, %s, %s --> %s" 136 ( print_memory_q chunk)132 (Memory.string_of_quantity q) 137 133 (print_addressing mode) 138 134 (print_args args) 139 (print_reg _list srcs)135 (print_reg srcr) 140 136 lbl 141 137 | RTLabs.St_call_id (f, args, res, sg, lbl) -> … … 143 139 f 144 140 (print_params args) 145 (print_reg _listres)141 (print_reg res) 146 142 (Primitive.print_sig sg) 147 143 lbl 148 144 | RTLabs.St_call_ptr (f, args, res, sg, lbl) -> 149 145 Printf.sprintf "call_ptr %s, %s, %s: %s --> %s" 150 (print_reg _listf)151 (print_params args) 152 (print_reg _listres)146 (print_reg f) 147 (print_params args) 148 (print_reg res) 153 149 (Primitive.print_sig sg) 154 150 lbl … … 160 156 | RTLabs.St_tailcall_ptr (f, args, sg) -> 161 157 Printf.sprintf "tailcall_ptr \"%s\", %s: %s" 162 (print_reg _listf)158 (print_reg f) 163 159 (print_params args) 164 160 (Primitive.print_sig sg) … … 168 164 lbl_true 169 165 lbl_false 170 | RTLabs.St_cond1 (op1, src s, lbl_true, lbl_false) ->166 | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) -> 171 167 Printf.sprintf "%s %s --> %s, %s" 172 168 (print_op1 op1) 173 (print_reg _list srcs)169 (print_reg srcr) 174 170 lbl_true 175 171 lbl_false 176 | RTLabs.St_cond2 (op2, src s1, srcs2, lbl_true, lbl_false) ->172 | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) -> 177 173 Printf.sprintf "%s %s, %s --> %s, %s" 178 174 (print_op2 op2) 179 (print_reg _list srcs1)180 (print_reg _list srcs2)175 (print_reg srcr1) 176 (print_reg srcr2) 181 177 lbl_true 182 178 lbl_false 183 | RTLabs.St_jumptable (r s, tbl) ->179 | RTLabs.St_jumptable (r, tbl) -> 184 180 Printf.sprintf "j_tbl %s --> %s" 185 (print_reg _list rs)181 (print_reg r) 186 182 (print_table tbl) 187 | RTLabs.St_return r s -> Printf.sprintf "return %s" (print_reg_list rs)183 | RTLabs.St_return r -> Printf.sprintf "return %s" (print_reg r) 188 184 189 185 … … 201 197 202 198 Printf.sprintf 203 "%s\"%s\"%s: %s\n%slocals: %s\n%s result: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"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" 204 200 (n_spaces n) 205 201 f … … 208 204 (n_spaces (n+2)) 209 205 (print_locals def.RTLabs.f_locals) 206 (n_spaces (n+2)) 207 (print_locals def.RTLabs.f_ptrs) 210 208 (n_spaces (n+2)) 211 209 (print_result def.RTLabs.f_result) -
Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.mli
r486 r740 2 2 (** This module provides a function to print [RTLabs] programs. *) 3 3 4 val print_statement : RTLabs.statement -> string 5 4 6 val print_program : RTLabs.program -> string -
Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml
r486 r740 28 28 (def, r :: res) 29 29 30 let rtl_args regs_list = List.flatten regs_list31 32 30 let addr_regs regs = match regs with 33 31 | r1 :: r2 :: _ -> (r1, r2) 34 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 50 List.fold_left f Register.Map.empty registers 51 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 69 | r1 :: r2 :: _ -> (r1, r2) 70 | _ -> assert false (* do not use on these arguments *) 71 72 let rtl_args regs_list lenv = List.flatten (find_and_list_args regs_list lenv) 73 35 74 36 75 … … 112 151 [RTL.St_stackaddr (r1, r2, start_lbl) ; 113 152 RTL.St_int (tmpr, off, start_lbl) ; 114 RTL.St_op2 (I8051.Add, r 2, r2, tmpr, start_lbl) ;153 RTL.St_op2 (I8051.Add, r1, r1, tmpr, start_lbl) ; 115 154 RTL.St_int (tmpr, 0, start_lbl) ; 116 RTL.St_op2 (I8051.Addc, r 1, r1, tmpr, start_lbl)]155 RTL.St_op2 (I8051.Addc, r2, r2, tmpr, start_lbl)] 117 156 start_lbl dest_lbl def 118 157 … … 128 167 | AST.Op_cast8unsigned, _, _ | AST.Op_cast8signed, _, _ 129 168 | AST.Op_cast16unsigned, _, _ | AST.Op_cast16signed, _, _ -> 130 def169 translate_move destrs srcrs start_lbl dest_lbl def 131 170 132 171 | AST.Op_negint, [destr], [srcr] -> … … 146 185 | AST.Op_ptrofint, [destr1 ; destr2], [srcr] -> 147 186 adds_graph 148 [RTL.St_move (destr 2, srcr, dest_lbl) ;149 RTL.St_int (destr 1, 0, start_lbl)]150 start_lbl dest_lbl def 151 152 | AST.Op_intofptr, [destr], [ _ ; srcr] ->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 ; _] -> 153 192 add_graph start_lbl (RTL.St_move (destr, srcr, dest_lbl)) def 154 193 … … 230 269 error_float () 231 270 232 | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] -> 271 | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] 272 | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] -> 233 273 let (def, tmpr1) = fresh_reg def in 234 274 let (def, tmpr2) = fresh_reg def in 235 275 adds_graph 236 [RTL.St_op2 (I8051.Add, tmpr 2, srcr12, srcr2, start_lbl) ;237 RTL.St_int (tmpr 1, 0, start_lbl) ;238 RTL.St_op2 (I8051.Addc, destr 1, tmpr1, srcr11, start_lbl) ;239 RTL.St_move (destr 2, tmpr2, start_lbl)]240 start_lbl dest_lbl def 241 242 | AST.Op_subp, [destr], [ _ ; srcr1], [_ ; srcr2] ->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 ; _] -> 243 283 let (def, tmpr1) = fresh_reg def in 244 284 let (def, tmpr2) = fresh_reg def in … … 251 291 252 292 | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] -> 253 let (def, tmpr1) = fresh_reg def in254 let (def, tmpr2) = fresh_reg def in255 let (def, tmpr3) = fresh_reg def in256 293 adds_graph 257 294 [RTL.St_clear_carry start_lbl ; 258 RTL.St_op2 (I8051.Sub, destr 2, srcr12, srcr2, start_lbl) ;259 RTL.St_int (destr 1, 0, start_lbl) ;260 RTL.St_op2 (I8051.Sub, destr 1, srcr11, destr1, 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)] 261 298 start_lbl dest_lbl def 262 299 … … 282 319 283 320 | AST.Op_cmpu AST.Cmp_gt, _, _, _ -> 284 translate_op2 (AST.Op_cmp AST.Cmp_lt)321 translate_op2 (AST.Op_cmpu AST.Cmp_lt) 285 322 destrs srcrs2 srcrs1 start_lbl dest_lbl def 286 323 … … 322 359 let (def, tmpr2) = fresh_reg def in 323 360 add_translates 324 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr1 1] [srcr21] ;325 translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr1 1] [srcr21] ;326 translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr1 2] [srcr22] ;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] ; 327 364 translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ; 328 365 translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]] … … 366 403 367 404 | AST.Cst_addrsymbol x -> 368 let (def, rs) = fresh_regs def 2 in 369 let r1 = List.nth rs 0 in 370 let r2 = List.nth rs 1 in 405 let (def, r1) = fresh_reg def in 406 let (def, r2) = fresh_reg def in 371 407 let lbl = fresh_label def in 372 408 let def = add_graph start_lbl (RTL.St_addr (r1, r2, x, lbl)) def in … … 417 453 | AST.Op_id, _ -> assert false (* wrong number of arguments *) 418 454 419 | _, _->455 | _, srcrs -> 420 456 let (def, destrs) = fresh_regs def (size_of_op1_ret op1) in 421 457 let lbl = fresh_label def in … … 443 479 | AST.Op_addp -> 2 444 480 | AST.Op_subp -> 445 if n = 1 (* sub between pointer and integer *) then 2446 else (* sub between two pointers *) 1481 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 447 483 | AST.Op_addf 448 484 | AST.Op_subf … … 463 499 464 500 | _, _, _ -> 465 let n = List.length srcrs2in501 let n = (List.length srcrs1) + (List.length srcrs2) in 466 502 let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in 467 503 let lbl = fresh_label def in … … 513 549 514 550 515 let translate_load chunk mode args destrs start_lbl dest_lbl def = 516 match chunk, destrs with 517 518 | Memory.MQ_pointer, [destr1 ; destr2] -> 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] -> 519 563 let (def, addr1) = fresh_reg def in 520 564 let (def, addr2) = fresh_reg def in … … 523 567 add_translates 524 568 [addressing_pointer mode args addr1 addr2 ; 525 adds_graph [RTL.St_load (destr 2, addr1, addr2, start_lbl) ;569 adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ; 526 570 RTL.St_int (tmpr, 1, start_lbl)] ; 527 571 translate_op2 AST.Op_addp addr addr [tmpr] ; 528 adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl)]] 529 start_lbl dest_lbl def 530 531 | Memory.MQ_int8signed, [destr] 532 | Memory.MQ_int8unsigned, [destr] -> 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] -> 533 582 let (def, addr1) = fresh_reg def in 534 583 let (def, addr2) = fresh_reg def in 535 584 add_translates 536 585 [addressing_pointer mode args addr1 addr2 ; 537 adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]] 538 start_lbl dest_lbl def 539 540 | Memory.MQ_int16signed, _ | Memory.MQ_int16unsigned, _ 541 | Memory.MQ_int32, _ -> 542 error_int () 543 544 | Memory.MQ_float32, _ | Memory.MQ_float64, _ -> 545 error_float () 546 547 | _ -> assert false (* wrong number of argument *) 548 549 550 let translate_store chunk mode args srcrs start_lbl dest_lbl def = 551 match chunk, srcrs with 552 553 | Memory.MQ_pointer, [srcr1 ; srcr2] -> 586 adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]] 587 start_lbl dest_lbl def 588 589 | Memory.QPtr, [srcr1 ; srcr2] -> 554 590 let (def, addr1) = fresh_reg def in 555 591 let (def, addr2) = fresh_reg def in … … 558 594 add_translates 559 595 [addressing_pointer mode args addr1 addr2 ; 560 adds_graph [RTL.St_store (addr1, addr2, srcr 2, start_lbl) ;596 adds_graph [RTL.St_store (addr1, addr2, srcr1, start_lbl) ; 561 597 RTL.St_int (tmpr, 1, start_lbl)] ; 562 598 translate_op2 AST.Op_addp addr addr [tmpr] ; 563 adds_graph [RTL.St_store (addr1, addr2, srcr1, dest_lbl)]] 564 start_lbl dest_lbl def 565 566 | Memory.MQ_int8signed, [srcr] 567 | Memory.MQ_int8unsigned, [srcr] -> 568 let (def, addr1) = fresh_reg def in 569 let (def, addr2) = fresh_reg def in 570 add_translates 571 [addressing_pointer mode args addr1 addr2 ; 572 adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]] 573 start_lbl dest_lbl def 574 575 | Memory.MQ_int16signed, _ | Memory.MQ_int16unsigned, _ 576 | Memory.MQ_int32, _ -> 577 error_int () 578 579 | Memory.MQ_float32, _ | Memory.MQ_float64, _ -> 580 error_float () 581 582 | _ -> assert false (* wrong number of argument *) 583 584 585 let translate_stmt lbl stmt def = match stmt with 599 adds_graph [RTL.St_store (addr1, addr2, srcr2, dest_lbl)]] 600 start_lbl dest_lbl def 601 602 | _ -> error "Size error in store." 603 604 605 let translate_stmt lenv lbl stmt def = match stmt with 586 606 587 607 | RTLabs.St_skip lbl' -> … … 591 611 add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def 592 612 593 | RTLabs.St_cst (destrs, cst, lbl') -> 594 translate_cst cst destrs lbl lbl' def 595 596 | RTLabs.St_op1 (op1, destrs, srcrs, lbl') -> 597 translate_op1 op1 destrs srcrs lbl lbl' def 598 599 | RTLabs.St_op2 (op2, destrs, srcrs1, srcrs2, lbl') -> 600 translate_op2 op2 destrs srcrs1 srcrs2 lbl lbl' def 601 602 | RTLabs.St_load (chunk, mode, args, destrs, lbl') -> 603 translate_load chunk mode args destrs lbl lbl' def 604 605 | RTLabs.St_store (chunk, mode, args, srcrs, lbl') -> 606 translate_store chunk mode args srcrs lbl lbl' def 607 608 | RTLabs.St_call_id (f, args, retrs, _, lbl') -> 609 add_graph lbl (RTL.St_call_id (f, rtl_args args, retrs, lbl')) def 610 611 | RTLabs.St_call_ptr (f, args, retrs, _, lbl') -> 612 let (f1, f2) = addr_regs f in 613 | RTLabs.St_cst (destr, cst, lbl') -> 614 translate_cst cst (find_and_list destr lenv) lbl lbl' def 615 616 | RTLabs.St_op1 (op1, destr, srcr, lbl') -> 617 translate_op1 op1 (find_and_list destr lenv) (find_and_list srcr lenv) 618 lbl lbl' def 619 620 | 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') -> 633 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') -> 637 let (f1, f2) = find_and_addr f lenv in 613 638 add_graph lbl 614 (RTL.St_call_ptr (f1, f2, rtl_args args, retrs, lbl')) def 639 (RTL.St_call_ptr 640 (f1, f2, rtl_args args lenv, find_and_list retr lenv, lbl')) def 615 641 616 642 | RTLabs.St_tailcall_id (f, args, _) -> 617 add_graph lbl (RTL.St_tailcall_id (f, rtl_args args )) def643 add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def 618 644 619 645 | RTLabs.St_tailcall_ptr (f, args, _) -> 620 let (f1, f2) = addr_regs fin621 add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args )) def646 let (f1, f2) = find_and_addr f lenv in 647 add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def 622 648 623 649 | RTLabs.St_condcst (cst, lbl_true, lbl_false) -> 624 650 translate_condcst cst lbl lbl_true lbl_false def 625 651 626 | RTLabs.St_cond1 (op1, srcrs, lbl_true, lbl_false) -> 627 translate_cond1 op1 srcrs lbl lbl_true lbl_false def 628 629 | RTLabs.St_cond2 (op2, srcrs1, srcrs2, lbl_true, lbl_false) -> 630 translate_cond2 op2 srcrs1 srcrs2 lbl lbl_true lbl_false def 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 631 659 632 660 | RTLabs.St_jumptable _ -> 633 661 error "Jump tables not supported yet." 634 662 635 | RTLabs.St_return r egs->636 add_graph lbl (RTL.St_return regs) def663 | RTLabs.St_return r -> 664 add_graph lbl (RTL.St_return (find_and_list r lenv)) def 637 665 638 666 639 667 let translate_internal def = 640 let set_of_list_list l = 641 let l = List.flatten l in 642 List.fold_left (fun res x -> Register.Set.add x res) Register.Set.empty l 643 in 668 let runiverse = def.RTLabs.f_runiverse in 669 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 673 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_params in 675 let locals = filter_and_to_list_local_env lenv def.RTLabs.f_locals in 676 let locals = set_of_list locals in 644 677 let res = 645 678 { RTL.f_luniverse = def.RTLabs.f_luniverse ; 646 RTL.f_runiverse = def.RTLabs.f_runiverse ;679 RTL.f_runiverse = runiverse ; 647 680 RTL.f_sig = def.RTLabs.f_sig ; 648 RTL.f_result = def.RTLabs.f_result ;649 RTL.f_params = List.flatten def.RTLabs.f_params ;650 RTL.f_locals = set_of_list_list def.RTLabs.f_locals ;681 RTL.f_result = result ; 682 RTL.f_params = params ; 683 RTL.f_locals = locals ; 651 684 RTL.f_stacksize = def.RTLabs.f_stacksize ; 652 685 RTL.f_graph = Label.Map.empty ; 653 686 RTL.f_entry = def.RTLabs.f_entry ; 654 687 RTL.f_exit = def.RTLabs.f_exit } in 655 Label.Map.fold translate_stmtdef.RTLabs.f_graph res688 Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res 656 689 657 690 -
Deliverables/D2.2/8051/src/acc.ml
r640 r740 29 29 | None -> (false, filename) 30 30 | Some filename' -> (true, filename') in 31 let save = Languages.save exact_output output_filename in 31 let save ?(suffix="") ast = 32 Languages.save exact_output output_filename suffix ast 33 in 32 34 let target_asts = 33 35 (** If debugging is enabled, the compilation function returns all … … 37 39 in 38 40 let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in 39 save final_ast; 40 (if Options.annotation_requested () then 41 let (annotated_input_ast, cost_id, cost_incr) = 42 Languages.annotate input_ast final_ast in 43 save annotated_input_ast; 44 Languages.save_cost output_filename cost_id cost_incr); 45 (if Options.is_debug_enabled () then 46 List.iter save intermediate_asts); 47 if Options.interpretation_requested () || Options.is_debug_enabled () then 48 begin 49 let asts = input_ast :: target_asts in 50 let print_result = Options.is_print_result_enabled () in 51 let label_traces = List.map (Languages.interpret print_result) asts in 52 Printf.eprintf "Checking execution traces...%!"; 53 Checker.same_traces (List.combine asts label_traces); 54 Printf.eprintf "OK.\n%!"; 55 end 41 save final_ast; 42 if Options.annotation_requested () then 43 begin 44 let (annotated_input_ast, cost_id, cost_incr) = 45 Languages.annotate input_ast final_ast in ( 46 save ~suffix:"-annotated" annotated_input_ast; 47 Languages.save_cost output_filename cost_id cost_incr); 48 end; 49 50 if Options.is_debug_enabled () then 51 List.iter save intermediate_asts; 52 53 if Options.interpretation_requested () || Options.is_debug_enabled () then 54 begin 55 let asts = input_ast :: target_asts in 56 let label_traces = List.map (Languages.interpret false) asts in 57 Printf.eprintf "Checking execution traces...%!"; 58 Checker.same_traces (List.combine asts label_traces); 59 Printf.eprintf "OK.\n%!"; 60 end 56 61 57 62 let _ = -
Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml
r619 r740 203 203 204 204 let translate p = 205 (* TODO: restore below *) 206 (* 205 207 let (p, unop_assoc, binop_assoc) = Runtime.add p in 206 208 let p = ClightCasts.simplify p in … … 212 214 (* TODO: do the translation *) 213 215 p 216 *) 217 ClightCasts.simplify p -
Deliverables/D2.2/8051/src/clight/clightCasts.ml
r624 r740 3 3 4 4 Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char] 5 will be transformed into [x + y]. *) 5 will be transformed into [x + y]. Primitive operations are thus supposed to 6 be polymorphic, but working only on homogene types. *) 6 7 7 8 let f_ctype ctype _ = ctype 8 9 10 (* 9 11 let f_expr = ClightFold.expr_fill_subs 10 12 … … 65 67 (Clight.Expr (_, 66 68 Clight.Tint (Clight.I8, signedness2)) as e1)), 67 _)), 69 _)),sub_ctypes_res sub_exprs_res 68 70 _) :: _ when signedness1 = signedness2 -> 69 71 Clight.Ebinop (binop, … … 72 74 e1) 73 75 | _ -> ClightFold.expr_descr_fill_subs e sub_ctypes_res sub_exprs_res 76 *) 74 77 75 let f_statement = ClightFold.statement_fill_subs 78 let simplify_exp ctype_opt e = e (* TODO *) 79 80 let f_expr e _ _ = e 81 82 let f_expr_descr e _ _ = e 83 84 let f_statement stmt _ sub_stmts_res = 85 let sub_exprs = match stmt with 86 | _ -> assert false in 87 ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res 76 88 77 89 let simplify_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_statement … … 85 97 (id, fundef') 86 98 87 let simplify p = 99 let simplify p = p 100 (* (* TODO: below *) 88 101 { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct } 102 *) -
Deliverables/D2.2/8051/src/clight/clightCasts.mli
r619 r740 3 3 4 4 Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char] 5 will be transformed into [x + y]. *) 5 will be transformed into [x + y]. Primitive operations are thus supposed to 6 be polymorphic, but working only on homogene types. *) 6 7 7 8 val simplify : Clight.program -> Clight.program -
Deliverables/D2.2/8051/src/clight/clightFold.mli
r619 r740 7 7 val ctype : (Clight.ctype -> 'a list -> 'a) -> Clight.ctype -> 'a 8 8 9 val expr : (Clight.expr_descr -> 'a list -> 'b list -> 'c) -> 10 (Clight.ctype -> 'a list -> 'a) -> 11 (Clight.expr -> 'c list -> 'a list -> 'b) -> 12 Clight.expr -> 13 'b 9 val expr_fill_subs : 10 Clight.expr -> Clight.ctype list -> Clight.expr_descr list -> 11 Clight.expr 14 12 15 val expr_descr : (Clight.ctype -> 'a list -> 'a) -> 16 (Clight.expr -> 'b list -> 'a list -> 'c) -> 17 (Clight.expr_descr -> 'a list -> 'c list -> 'b) -> 18 Clight.expr_descr -> 19 'b 13 val expr : 14 (Clight.ctype -> 'a list -> 'a) -> 15 (Clight.expr -> 'a list -> 'b list -> 'c) -> 16 (Clight.expr_descr -> 'a list -> 'c list -> 'b) -> 17 Clight.expr -> 18 'c 20 19 21 (* 22 (* In [statement_left f_expr f_stmt stmt], [f_stmt]'s second argument is the 23 list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and 24 [f_stmt]'s third argument is the list of [statement_left]'s results 25 on [stmt]'s sub-statements. The results are computed from left to right 26 following their appearance order in the [Cminor.statement] type. *) 20 val expr_descr_fill_subs : 21 Clight.expr_descr -> Clight.ctype list -> Clight.expr list -> 22 Clight.expr_descr 27 23 28 val statement_left : (Cminor.expression -> 'a list -> 'a) -> 29 (Cminor.statement -> 'a list -> 'b list -> 'b) -> 30 Cminor.statement -> 31 'b 32 *) 24 val expr_descr : 25 (Clight.ctype -> 'a list -> 'a) -> 26 (Clight.expr -> 'a list -> 'b list -> 'c) -> 27 (Clight.expr_descr -> 'a list -> 'c list -> 'b) -> 28 Clight.expr_descr -> 29 'b 30 31 val statement_fill_subs : 32 Clight.statement -> Clight.expr list -> Clight.statement list -> 33 Clight.statement 34 35 val statement : 36 (Clight.ctype -> 'a list -> 'a) -> 37 (Clight.expr -> 'a list -> 'b list -> 'c) -> 38 (Clight.expr_descr -> 'a list -> 'c list -> 'b) -> 39 (Clight.statement -> 'c list -> 'd list -> 'd) -> 40 Clight.statement -> 41 'd -
Deliverables/D2.2/8051/src/clight/clightInterpret.ml
r630 r740 1 1 module Mem = Driver.ClightMemory 2 2 module Value = Driver.ClightMemory.Value 3 module Valtbl = Hashtbl.Make(Value) 3 module LocalEnv = Map.Make(String) 4 type localEnv = Value.address LocalEnv.t 5 type memory = Clight.fundef Mem.memory 4 6 5 7 open Clight 6 8 open AST 7 9 8 let warning msg = print_string ("Warning: "^msg^" (clightInterpret.ml)\n") 9 10 type localEnv = (ident,Value.t) Hashtbl.t 10 11 let error_prefix = "Clight interpret" 12 let error s = Error.global_error error_prefix s 13 let warning s = Error.warning error_prefix s 14 let error_float () = error "float not supported." 15 16 17 (* Helpers *) 18 19 let value_of_address = List.hd 20 let address_of_value v = [v] 21 22 23 (* State of execution *) 11 24 12 25 type continuation = … … 18 31 | Kfor3 of expr*statement*statement*continuation 19 32 | Kswitch of continuation 20 | Kcall of (Value. t*ctype) option*cfunction*localEnv*continuation33 | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation 21 34 22 35 type state = 23 | State of cfunction*statement*continuation*localEnv*(fundef Mem.memory) 24 | Callstate of fundef*Value.t list*continuation*(fundef Mem.memory) 25 | Returnstate of Value.t*continuation*(fundef Mem.memory) 26 27 (* ctype functions *) 28 29 let rec sizeof = function 30 | Tvoid -> 0 31 | Tint (I8,_) -> 1 32 | Tint (I16,_) -> 2 33 | Tint (I32,_) -> 4 34 | Tfloat _ -> assert false (* Not supported *) 35 | Tpointer _ -> Mem.ptr_size 36 | Tarray (t,s) -> s*(sizeof t) 37 | Tfunction (_,_) -> assert false (* Not supported *) 38 | Tstruct (_,lst) -> 39 List.fold_left 40 (fun n (_,ty) -> (fun a b -> a+b) n (sizeof ty)) 0 lst 41 | Tunion (_,lst) -> 42 List.fold_left 43 (fun n (_,ty) -> 44 let sz = (sizeof ty) in (if n>sz then n else sz) 45 ) 0 lst 46 | Tcomp_ptr _ -> Mem.ptr_size 47 48 let rec mq_of_ty = function 49 | Tvoid -> assert false 50 | Tint (I8,Signed) -> Memory.MQ_int8signed 51 | Tint (I8,Unsigned) -> Memory.MQ_int8unsigned 52 | Tint (I16,Signed) -> Memory.MQ_int16signed 53 | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned 54 (*FIXME MQ_int32 : signed or unsigned ?*) 55 | Tint (I32,Signed) -> Memory.MQ_int32 56 | Tint (I32,Unsigned) -> Memory.MQ_int32 57 | Tfloat _ -> assert false (* Not supported *) 58 | Tpointer _ -> Mem.mq_of_ptr 59 | Tarray (c,s) -> Mem.mq_of_ptr 60 | Tfunction (_,_) -> assert false (* Not supported *) 61 | Tstruct (_,_) -> Mem.mq_of_ptr 62 | Tunion (_,_) -> Mem.mq_of_ptr 63 | Tcomp_ptr _ -> Mem.mq_of_ptr 64 65 (* Pretty printing for Clight states *) 66 67 let string_s = function 68 | Sskip -> "skip" 69 | Sassign (Expr (Evar id,_),_) -> "assign "^id 70 | Sassign (_,_) -> "assign" 71 | Scall (_,_,_) -> "call" 72 | Ssequence (_,_) -> "seq" 73 | Sifthenelse (_,_,_) -> "ifthenelse" 74 | Swhile (_,_) -> "while" 75 | Sdowhile (_,_) -> "dowhile" 76 | Sfor (_,_,_,_) -> "for" 77 | Sbreak -> "break" 78 | Scontinue -> "continue" 79 | Sreturn _ -> "return" 80 | Sswitch (_,_) -> "switch" 81 | Slabel (_,_) -> "label" 82 | Sgoto _ -> "goto" 83 | Scost (_,_) -> "cost" 84 85 let string_f = function 86 | Internal _ -> "func" 87 | External (id,_,_) -> id 88 89 let string_c = function 90 | Kstop -> "stop" 91 | Kseq (_,_) -> "seq" 92 | Kwhile (_,_,_) -> "while" 93 | Kdowhile (_,_,_) -> "dowhile" 94 | Kfor2 (_,_,_,_) -> "for2" 95 | Kfor3 (_,_,_,_) -> "for3" 96 | Kswitch _ -> "switch" 97 | Kcall (_,_,_,_) -> "call" 98 99 let string_of_state = function 100 | State (_,s,c,_,_) -> "Regular("^(string_s s)^","^(string_c c)^")" 101 | Callstate (f,_,c,_) -> "Call("^(string_f f)^","^(string_c c)^")" 102 | Returnstate (v,c,_) -> 103 "Return("^(Value.to_string v)^","^(string_c c)^")" 104 105 (* Global and local environment management *) 106 107 let find_funct_id g id = 108 try Valtbl.find (snd g) (Hashtbl.find (fst g) id) 109 with Not_found -> assert false 110 111 let find_funct g v = 112 try Valtbl.find (snd g) (fst v) 113 with Not_found -> assert false 114 115 let find_symbol globalenv localenv id = 116 try Hashtbl.find localenv id 117 with Not_found -> ( 118 try Hashtbl.find (fst globalenv) id 119 with Not_found -> 120 Printf.eprintf "Error: cannot find symbol %s\n" id; 121 assert false 122 ) 36 | State of cfunction*statement*continuation*localEnv*memory 37 | Callstate of fundef*Value.t list*continuation*memory 38 | Returnstate of Value.t*continuation*memory 39 40 let string_of_unop = function 41 | Onotbool -> "!" 42 | Onotint -> "~" 43 | Oneg -> "-" 44 45 let string_of_binop = function 46 | Oadd -> "+" 47 | Osub -> "-" 48 | Omul -> "*" 49 | Odiv -> "/" 50 | Omod -> "%" 51 | Oand -> "&" 52 | Oor -> "|" 53 | Oxor -> "^" 54 | Oshl -> "<<" 55 | Oshr -> ">>" 56 | Oeq -> "==" 57 | One -> "!=" 58 | Olt -> "<" 59 | Ogt -> ">" 60 | Ole -> "<=" 61 | Oge -> ">=" 62 63 let string_of_signedness = function 64 | Signed -> "signed" 65 | Unsigned -> "unsigned" 66 67 let string_of_sized_int = function 68 | I8 -> "char" 69 | I16 -> "short" 70 | I32 -> "int" 71 72 let rec string_of_ctype = function 73 | Tvoid -> "void" 74 | Tint (size, sign) -> 75 (string_of_signedness sign) ^ " " ^ (string_of_sized_int size) 76 | Tfloat _ -> error_float () 77 | Tpointer ty -> (string_of_ctype ty) ^ "*" 78 | Tarray (ty, _) -> (string_of_ctype ty) ^ "[]" 79 | Tfunction _ -> assert false (* do not cast to a function type *) 80 | Tstruct (id, _) 81 | Tunion (id, _) -> id 82 | Tcomp_ptr id -> id ^ "*" 83 84 let rec string_of_expr (Expr (e, _)) = string_of_expr_descr e 85 and string_of_expr_descr = function 86 | Econst_int i -> string_of_int i 87 | Econst_float _ -> error_float () 88 | Evar x -> x 89 | Ederef e -> "*(" ^ (string_of_expr e) ^ ")" 90 | Eaddrof e -> "&(" ^ (string_of_expr e) ^ ")" 91 | Eunop (unop, e) -> (string_of_unop unop) ^ "(" ^ (string_of_expr e) ^ ")" 92 | Ebinop (binop, e1, e2) -> 93 "(" ^ (string_of_expr e1) ^ ")" ^ (string_of_binop binop) ^ 94 "(" ^ (string_of_expr e2) ^ ")" 95 | Ecast (ty, e) -> 96 "(" ^ (string_of_ctype ty) ^ ") (" ^ (string_of_expr e) ^ ")" 97 | Econdition (e1, e2, e3) -> 98 "(" ^ (string_of_expr e1) ^ ") ? (" ^ (string_of_expr e2) ^ 99 ") : (" ^ (string_of_expr e3) ^ ")" 100 | Eandbool (e1, e2) -> 101 "(" ^ (string_of_expr e1) ^ ") && (" ^ (string_of_expr e2) ^ ")" 102 | Eorbool (e1, e2) -> 103 "(" ^ (string_of_expr e1) ^ ") || (" ^ (string_of_expr e2) ^ ")" 104 | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")" 105 | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field 106 | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e) 107 | Ecall (f, arg, e) -> 108 "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")" 109 110 let string_of_args args = 111 "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")" 112 113 let rec string_of_statement = function 114 | Sskip -> "skip" 115 | Sassign (e1, e2) -> (string_of_expr e1) ^ " = " ^ (string_of_expr e2) 116 | Scall (None, f, args) -> (string_of_expr f) ^ (string_of_args args) 117 | Scall (Some e, f, args) -> 118 (string_of_expr e) ^ " = " ^ (string_of_expr f) ^ (string_of_args args) 119 | Ssequence _ -> "sequence" 120 | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")" 121 | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")" 122 | Sdowhile _ -> "dowhile" 123 | Sfor (s, _, _, _) -> "for (" ^ (string_of_statement s) ^ "; ...)" 124 | Sbreak -> "break" 125 | Scontinue -> "continue" 126 | Sreturn None -> "return" 127 | Sreturn (Some e) -> "return (" ^ (string_of_expr e) ^ ")" 128 | Sswitch (e, _) -> "switch (" ^ (string_of_expr e) ^ ")" 129 | Slabel (lbl, _) -> "label " ^ lbl 130 | Sgoto lbl -> "goto " ^ lbl 131 | Scost (lbl, _) -> "cost " ^ lbl 132 133 let string_of_local_env lenv = 134 let f x addr s = 135 s ^ x ^ " = " ^ (Value.to_string (value_of_address addr)) ^ " " in 136 LocalEnv.fold f lenv "" 137 138 let print_state = function 139 | State (_, stmt, _, lenv, mem) -> 140 Printf.printf "Local environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!" 141 (string_of_local_env lenv) 142 (Mem.to_string mem) 143 (string_of_statement stmt) 144 | Callstate (_, args, _, mem) -> 145 Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!" 146 (Mem.to_string mem) 147 (MiscPottier.string_of_list " " Value.to_string args) 148 | Returnstate (v, _, mem) -> 149 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 150 (Mem.to_string mem) 151 (Value.to_string v) 152 123 153 124 154 (* Continuations and labels *) 125 155 126 156 let rec call_cont = function 127 | Kseq (_,k) -> call_cont k 128 | Kwhile (_,_,k) -> call_cont k 129 | Kdowhile (_,_,k) -> call_cont k 130 | Kfor2 (_,_,_,k) -> call_cont k 131 | Kfor3 (_,_,_,k) -> call_cont k 132 | Kswitch k -> call_cont k 133 | k -> k 134 135 let is_call_cont = function 136 | Kstop | Kcall (_,_,_,_) -> true 137 | _ -> false 157 | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k) 158 | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k 159 | k -> k 138 160 139 161 let rec seq_of_labeled_statement = function 140 162 | LSdefault s -> s 141 163 | LScase (c,s,sl') -> Ssequence (s,(seq_of_labeled_statement sl')) 164 165 let rec find_label1 lbl s k = match s with 166 | Ssequence (s1,s2) -> 167 (match find_label1 lbl s1 (Kseq (s2,k)) with 168 | Some sk -> Some sk 169 | None -> find_label1 lbl s2 k 170 ) 171 | Sifthenelse (a,s1,s2) -> 172 (match find_label1 lbl s1 k with 173 | Some sk -> Some sk 174 | None -> find_label1 lbl s2 k 175 ) 176 | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k)) 177 | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k)) 178 | Sfor (a1,a2,a3,s1) -> 179 (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with 180 | Some sk -> Some sk 181 | None -> 182 (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with 183 | Some sk -> Some sk 184 | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k)) 185 )) 186 | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k) 187 | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label1 lbl s' k 188 | Scost (_,s') -> find_label1 lbl s' k 189 | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak 190 | Scontinue | Sreturn _ | Sgoto _ -> None 191 192 and find_label_ls lbl sl k = match sl with 193 | LSdefault s -> find_label1 lbl s k 194 | LScase (_,s,sl') -> 195 (match find_label1 lbl s (Kseq((seq_of_labeled_statement sl'),k)) with 196 | Some sk -> Some sk 197 | None -> find_label_ls lbl sl' k 198 ) 199 200 let find_label lbl s k = match find_label1 lbl s k with 201 | Some res -> res 202 | _ -> assert false (* should be impossible *) 142 203 143 204 let rec select_switch i = function … … 146 207 | LScase (_,_,sl') -> select_switch i sl' 147 208 148 let rec find_label lbl s k = match s with 149 | Ssequence (s1,s2) -> 150 (match find_label lbl s1 (Kseq (s2,k)) with 151 | Some sk -> Some sk 152 | None -> find_label lbl s2 k 153 ) 154 | Sifthenelse (a,s1,s2) -> 155 (match find_label lbl s1 k with 156 | Some sk -> Some sk 157 | None -> find_label lbl s2 k 158 ) 159 | Swhile (a,s1) -> find_label lbl s1 (Kwhile(a,s1,k)) 160 | Sdowhile (a,s1) -> find_label lbl s1 (Kdowhile(a,s1,k)) 161 | Sfor (a1,a2,a3,s1) -> 162 (match find_label lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with 163 | Some sk -> Some sk 164 | None -> 165 (match find_label lbl s1 (Kfor2(a2,a3,s1,k)) with 166 | Some sk -> Some sk 167 | None -> find_label lbl a3 (Kfor3(a2,a3,s1,k)) 168 )) 169 | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k) 170 | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label lbl s' k 171 | Scost (_,s') -> find_label lbl s' k 172 | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak 173 | Scontinue | Sreturn _ | Sgoto _ -> None 174 175 and find_label_ls lbl sl k = match sl with 176 | LSdefault s -> find_label lbl s k 177 | LScase (_,s,sl') -> 178 (match find_label lbl s (Kseq((seq_of_labeled_statement sl'),k)) with 179 | Some sk -> Some sk 180 | None -> find_label_ls lbl sl' k 181 ) 209 210 (* ctype functions *) 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 *) 226 227 let size_of_ctype = function 228 | Tint (I8, _) -> 1 229 | Tint (I16, _) -> 2 230 | Tint (I32, _) -> 4 231 | Tfloat _ -> error_float () 232 | Tcomp_ptr _ 233 | Tpointer _ 234 | Tarray _ 235 | Tstruct _ 236 | Tunion _ -> Mem.ptr_size 237 | _ -> assert false (* do not use on these arguments *) 238 239 let is_function_type = function 240 | Tfunction _ -> true 241 | _ -> false 242 243 let is_array_type = function 244 | Tarray _ -> true 245 | _ -> false 246 247 let is_complex_type = function 248 | Tstruct _ | Tunion _ -> true 249 | _ -> false 250 251 let is_big_type t = (is_array_type t) || (is_complex_type t) 252 253 let dest_type = function 254 | Tpointer ty | Tarray (ty, _) -> ty 255 | _ -> assert false (* do not use on these arguments *) 256 257 258 (* Global and local environment management *) 259 260 let find_local x lenv = 261 if LocalEnv.mem x lenv then LocalEnv.find x lenv 262 else error ("Unknown local variable " ^ x ^ ".") 263 264 let find_global x mem = 265 if Mem.mem_global mem x then Mem.find_global mem x 266 else error ("Unknown global variable " ^ x ^ ".") 267 268 let find_symbol lenv mem x = 269 if LocalEnv.mem x lenv then LocalEnv.find x lenv 270 else 271 if Mem.mem_global mem x then Mem.find_global mem x 272 else error ("Unknown variable " ^ x ^ ".") 273 274 let find_fundef f mem = 275 let addr = Mem.find_global mem f in 276 Mem.find_fun_def mem addr 277 182 278 183 279 (* Interpret *) 184 280 185 let is_int_type = function 186 | Tint (_,_) -> true 187 | _ -> false 188 let is_float_type = function 189 | Tfloat _ -> true 190 | _ -> false 191 let is_pointer_type = function 192 | Tpointer _ | Tarray (_,_) | Tstruct (_,_) 193 | Tunion (_,_) | Tcomp_ptr _ -> true 194 | _ -> false 195 196 let eval_cast = function 197 (* no cast *) 198 | (e,a,b) when a=b -> e 281 let int_of_intsize = function 282 | I8 -> 8 283 | I16 -> 16 284 | I32 -> 32 285 286 let choose_cast signedness n m v = 287 let f = match signedness with 288 | Signed -> Value.sign_ext 289 | Unsigned -> Value.zero_ext in 290 f v n m 291 292 let eval_cast = function 199 293 (* Cast Integer *) 200 | (v,_,Tint(I8,Signed)) -> Value.cast8signed v 201 | (v,_,Tint(I8,Unsigned)) -> Value.cast8unsigned v 202 | (v,_,Tint(I16,Signed)) -> Value.cast16signed v 203 | (v,_,Tint(I16,Unsigned)) -> Value.cast16unsigned v 204 | (v,_,Tint(I32,Signed)) when Value.is_int v -> v 205 | (v,_,Tint(I32,Unsigned)) when Value.is_int v-> v (*FIXME*) 206 (* Cast float*) 207 | (v,_,Tfloat _) -> assert false(*Not supported*) 208 (* Cast pointeur *) 209 | (v,Tarray(_,_),Tpointer _) -> v 210 | (v,Tpointer _,Tarray(_,_)) -> v 211 | (v,Tpointer _,Tpointer _) -> v 212 | (v,Tarray (_,_),Tarray(_,_)) -> v 213 | (v,Tstruct(a,b),Tpointer (Tstruct(c,d))) when a=c && b=d -> v (*FIXME is it correct ?*) 214 | (v,Tpointer (Tstruct(a,b)),Tstruct(c,d)) when a=c && b=d -> v (*FIXME is it correct ?*) 215 | (v,Tunion(a,b),Tpointer (Tunion(c,d))) when a=c && b=d -> v (*FIXME is it correct ?*) 216 | (v,Tpointer (Tunion(a,b)),Tunion(c,d)) when a=c && b=d -> v (*FIXME is it correct ?*) 217 (* error *) 218 | (e,_,_) -> 219 warning "eval_cast";e (*Value.undef*) 220 221 let eval_unop (v,t) = function 222 | Onotbool when is_int_type t -> Value.notbool v 223 | Onotint when is_int_type t -> Value.notint v 224 | Oneg when is_int_type t -> Value.negint v 225 | Oneg when is_float_type t -> assert false (*Not supported*) 226 | _ -> assert false (*Type error*) 227 228 let get_subtype = function 229 | Tarray(t,_) -> t 230 | Tpointer t -> t 231 | _ -> assert false (*Misuse of get_subtype*) 232 233 let eval_add = function 234 (*Integer*) 235 | ((v1,t1) , (v2,t2)) when t1=t2 && is_int_type t1 -> 236 let v = Value.add v1 v2 in 237 (match t1 with 238 | Tint(I8,Signed) -> Value.cast8signed v 239 | Tint(I8,Unsigned) -> Value.cast8unsigned v 240 | Tint(I16,Signed) -> Value.cast16signed v 241 | Tint(I16,Unsigned) -> Value.cast16unsigned v 242 | Tint(I32,Signed) -> v 243 | Tint(I32,Unsigned) -> v (*FIXME*) 244 | _ -> assert false (*Prevented by is_int_type*)) 245 (*Float*) 246 | ((v1,t1) , (v2,t2)) when t1=t2 && is_float_type t1 -> 247 assert false (*Not supported*) 248 (*Pointer*) 249 | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 -> 250 Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1)))) 251 | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 -> 252 Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1)))) 253 (*Error*) 254 | _ -> assert false (*Type error*) 255 256 let eval_sub = function 257 (*Integer*) 258 | ((v1,t1) , (v2,t2)) when t1=t2 && is_int_type t1 -> 259 let v = Value.sub v1 v2 in 260 (match t1 with 261 | Tint(I8,Signed) -> Value.cast8signed v 262 | Tint(I8,Unsigned) -> Value.cast8unsigned v 263 | Tint(I16,Signed) -> Value.cast16signed v 264 | Tint(I16,Unsigned) -> Value.cast16unsigned v 265 | Tint(I32,Signed) -> v 266 | Tint(I32,Unsigned) -> v (*FIXME*) 267 | _ -> assert false (*Prevented by is_int_type*)) 268 (*Float*) 269 | ((v1,t1) , (v2,t2)) when t1=t2 && is_float_type t1 -> 270 assert false (*Not supported*) 271 (*Pointer*) 272 | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 -> 273 Value.sub v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1)))) 274 (*Error*) 275 | _ -> assert false (*Type error*) 276 277 let eval_mul = function 278 | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> 279 let v = Value.mul v1 v2 in 280 (match t1 with 281 | Tint(I8,Signed) -> Value.cast8signed v 282 | Tint(I8,Unsigned) -> Value.cast8unsigned v 283 | Tint(I16,Signed) -> Value.cast16signed v 284 | Tint(I16,Unsigned) -> Value.cast16unsigned v 285 | Tint(I32,Signed) -> v 286 | Tint(I32,Unsigned) -> v (*FIXME*) 287 | _ -> assert false (*Prevented by is_int_type*)) 288 | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 -> 289 assert false (*Not supported*) 290 | _ -> assert false (*Type error*) 291 292 let eval_mod = function 293 | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> 294 Value.modulo v1 v2 295 | _ -> assert false (*Type error*) 296 297 let eval_div = function 298 | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.div v1 v2 299 | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 -> 300 assert false (*Not supported*) 301 | _ -> assert false (*Type error*) 302 303 let eval_and = function 304 | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.and_op v1 v2 305 | _ -> assert false (*Type error*) 306 307 let eval_or = function 308 | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.or_op v1 v2 309 | _ -> assert false (*Type error*) 310 311 let eval_xor = function 312 | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.xor v1 v2 313 | _ -> assert false (*Type error*) 314 315 let eval_shl = function 316 | ((v1,t1),(v2,t2)) when is_int_type t2 && is_int_type t1 -> Value.shl v1 v2 317 | _ -> assert false (*Type error*) 318 319 let eval_shr = function 320 | ((v1,t1),(v2,t2)) when is_int_type t2 && is_int_type t1 -> Value.shr v1 v2 321 | _ -> assert false (*Type error*) 322 323 let eval_eq = function 324 | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_eq v1 v2 325 | _ -> assert false (*Type error*) 326 327 let eval_ne = function 328 | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ne v1 v2 329 | _ -> assert false (*Type error*) 330 331 let eval_lt = function 332 | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_lt v1 v2 333 | _ -> assert false (*Type error*) 334 335 let eval_gt = function 336 | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_gt v1 v2 337 | _ -> assert false (*Type error*) 338 339 let eval_le = function 340 | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_le v1 v2 341 | _ -> assert false (*Type error*) 342 343 let eval_ge = function 344 | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ge v1 v2 345 | _ -> assert false (*Type error*) 346 347 let eval_binop e1 e2 = function 348 | Oadd -> eval_add (e1,e2) 349 | Osub -> eval_sub (e1,e2) 350 | Omul -> eval_mul (e1,e2) 351 | Odiv -> eval_div (e1,e2) 352 | Omod -> eval_mod (e1,e2) 353 | Oand -> eval_and (e1,e2) 354 | Oor -> eval_or (e1,e2) 355 | Oxor-> eval_xor (e1,e2) 356 | Oshl-> eval_shl (e1,e2) 357 | Oshr-> eval_shr (e1,e2) 358 | Oeq -> eval_eq (e1,e2) 359 | One -> eval_ne (e1,e2) 360 | Olt -> eval_lt (e1,e2) 361 | Ogt -> eval_gt (e1,e2) 362 | Ole -> eval_le (e1,e2) 363 | Oge -> eval_ge (e1,e2) 364 365 let rec get_offset_struct v id = function 366 | [] -> assert false (*Wrong id*) 367 | (fi,_)::_ when fi=id -> v 368 | (_,ty)::ll -> get_offset_struct 369 (Value.add v (Value.of_int (sizeof ty))) id ll 370 371 let is_true (v,_) = Value.is_true v 372 373 let is_false (v,_) = Value.is_false v 374 375 let rec eval_expr globalenv localenv m e = let Expr (ee,tt) = e in 294 | (v,Tint(isize,signedness),Tint(isize',_)) -> 295 choose_cast signedness (int_of_intsize isize) (int_of_intsize isize') v 296 | (v,_,_) -> v 297 298 let eval_unop = function 299 | Onotbool -> Value.notbool 300 | Onotint -> Value.notint 301 | Oneg -> Value.negint 302 303 let eval_add (v1,t1) (v2,t2) = match t1, t2 with 304 | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ -> 305 let v = Value.mul (Value.of_int (sizeof ty)) v2 in 306 Value.add v1 v 307 | Tint _, Tpointer ty | Tint _, Tarray (ty, _) -> 308 let v = Value.mul (Value.of_int (sizeof ty)) v1 in 309 Value.add v2 v 310 | _ -> Value.add v1 v2 311 312 let eval_sub (v1,t1) (v2,t2) = match t1, t2 with 313 | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ -> 314 let v = Value.mul (Value.of_int (sizeof ty)) v2 in 315 Value.sub v1 v 316 | _ -> Value.sub v1 v2 317 318 let choose_signedness op_signed op_unsigned v1 v2 t = 319 let op = match t with 320 | Tint (_, Signed) -> op_signed 321 | Tint (_, Unsigned) -> op_unsigned 322 | _ -> op_unsigned in 323 op v1 v2 324 325 let eval_binop ret_ctype ((v1,t1) as e1) ((v2,t2) as e2) op = 326 let v = match op with 327 | Oadd -> eval_add e1 e2 328 | Osub -> eval_sub e1 e2 329 | Omul -> Value.mul v1 v2 330 | Odiv -> choose_signedness Value.div Value.divu v1 v2 t1 331 | Omod -> choose_signedness Value.modulo Value.modulou v1 v2 t1 332 | Oand -> Value.and_op v1 v2 333 | Oor -> Value.or_op v1 v2 334 | Oxor -> Value.xor v1 v2 335 | Oshl-> Value.shl v1 v2 336 | Oshr-> Value.shr v1 v2 337 | Oeq -> choose_signedness Value.cmp_eq Value.cmp_eq_u v1 v2 t1 338 | One -> choose_signedness Value.cmp_ne Value.cmp_ne_u v1 v2 t1 339 | Olt -> choose_signedness Value.cmp_lt Value.cmp_lt_u v1 v2 t1 340 | Ole -> choose_signedness Value.cmp_le Value.cmp_le_u v1 v2 t1 341 | Ogt -> choose_signedness Value.cmp_gt Value.cmp_gt_u v1 v2 t1 342 | Oge -> choose_signedness Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in 343 eval_cast (v, t1, ret_ctype) 344 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 353 Value.add v off 354 355 let get_offset v id = function 356 | Tstruct (_, fields) -> get_offset_struct v id fields 357 | Tunion _ -> v 358 | _ -> assert false (* do not use on these arguments *) 359 360 let is_true (v, _) = Value.is_true v 361 let is_false (v, _) = Value.is_false v 362 363 let rec eval_expr localenv m (Expr (ee, tt)) = 376 364 match ee with 377 | Econst_int i -> 378 let v = (match tt with 379 | Tint(I8,Signed) -> Value.cast8signed (Value.of_int i) 380 | Tint(I8,Unsigned) -> Value.cast8unsigned (Value.of_int i) 381 | Tint(I16,Signed) -> Value.cast16signed (Value.of_int i) 382 | Tint(I16,Unsigned) -> Value.cast16unsigned (Value.of_int i) 383 | Tint(I32,Signed) -> Value.of_int i 384 | Tint(I32,Unsigned) -> Value.of_int i (*FIXME*) 385 | _ -> assert false (*Type error*)) 386 in ((v,tt),[]) 387 | Econst_float _ -> assert false (*Not supported *) 388 | Evar id -> 389 (match tt with 390 | Tfunction (_,_) -> ((find_symbol globalenv localenv id,tt),[]) 391 | _ -> 392 ((Mem.load m (mq_of_ty tt) (find_symbol globalenv localenv id),tt),[]) 393 ) 394 | Ederef exp -> let ((v1,t1),l1) = eval_expr globalenv localenv m exp in 395 ((Mem.load m (mq_of_ty tt) v1,tt),l1) 396 | Eaddrof exp -> eval_lvalue globalenv localenv m exp 365 | Econst_int i -> 366 let v = eval_cast (Value.of_int i, Tint(I32, Signed), tt) in 367 ((v, tt),[]) 368 | Econst_float _ -> error_float () 369 | Evar id when is_function_type tt || is_big_type tt -> 370 let v = value_of_address (find_symbol localenv m id) in 371 ((v, tt), []) 372 | Evar id -> 373 let addr = find_symbol localenv m id in 374 let v = Mem.load m (size_of_ctype tt) addr in 375 ((v, tt), []) 376 | Ederef e when is_function_type tt || is_big_type tt -> 377 let ((v1,_),l1) = eval_expr localenv m e in 378 ((v1,tt),l1) 379 | Ederef e -> 380 let ((v1,_),l1) = eval_expr localenv m e in 381 let addr = address_of_value v1 in 382 let v = Mem.load m (size_of_ctype tt) addr in 383 ((v,tt),l1) 384 | Eaddrof exp -> 385 let ((addr,_),l) = eval_lvalue localenv m exp in 386 ((value_of_address addr,tt),l) 387 | Ebinop (op,exp1,exp2) -> 388 let (v1,l1) = eval_expr localenv m exp1 in 389 let (v2,l2) = eval_expr localenv m exp2 in 390 ((eval_binop tt v1 v2 op,tt),l1@l2) 397 391 | Eunop (op,exp) -> 398 let (v1,l1) = eval_expr globalenv localenv m exp in 399 ((eval_unop v1 op,tt),l1) 400 | Ebinop (op,exp1,exp2) -> 401 let (v1,l1) = eval_expr globalenv localenv m exp1 402 and (v2,l2) = eval_expr globalenv localenv m exp2 in 403 ((eval_binop v1 v2 op,tt),l1@l2) 404 | Ecast (cty,exp) -> 405 let ((v,ty),l1) = eval_expr globalenv localenv m exp in 406 ((eval_cast (v,ty,cty),tt),l1) 392 let ((v1,_),l1) = eval_expr localenv m exp in 393 ((eval_unop op v1,tt),l1) 407 394 | Econdition (e1,e2,e3) -> 408 let (v1,l1) = eval_expr globalenv localenv m e1 in 409 if is_true v1 then 410 let (v2,l2) = eval_expr globalenv localenv m e2 in 411 (v2,l1@l2) 412 else if is_false v1 then 413 let (v2,l2) = eval_expr globalenv localenv m e3 in 414 (v2,l1@l2) 415 else ((Value.undef,tt),l1) 395 let (v1,l1) = eval_expr localenv m e1 in 396 if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2) 397 else 398 if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3) 399 else (v1,l1) 416 400 | Eandbool (e1,e2) -> 417 let (v1,l1) = eval_expr globalenv localenv m e1 in 418 if is_true v1 then ( 419 let (v2,l2) = eval_expr globalenv localenv m e2 in 420 if is_true v2 then 421 ((Value.val_true,tt),l1@l2) 422 else ( 423 if is_false v2 then ((Value.val_false,tt),l1@l2) 424 else ((Value.undef,tt),l1@l2) 425 )) else ( 426 if is_false v1 then ((Value.val_false,tt),l1) 427 else ((Value.undef,tt),l1)) 401 let (v1,l1) = eval_expr localenv m e1 in 402 if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2) 403 else (v1,l1) 428 404 | Eorbool (e1,e2) -> 429 let (v1,l1) = eval_expr globalenv localenv m e1 in 430 if is_false v1 then ( 431 let (v2,l2) = eval_expr globalenv localenv m e2 in 432 if is_true v2 then ((Value.val_true,tt),l1@l2) 433 else ( 434 if is_false v2 then ((Value.val_false,tt),l1@l2) 435 else ((Value.undef,tt),l1@l2) 436 )) else ( 437 if is_true v1 then ((Value.val_true,tt),l1) 438 else ((Value.undef,tt),l1)) 405 let (v1,l1) = eval_expr localenv m e1 in 406 if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2) 407 else (v1,l1) 439 408 | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[]) 440 409 | Efield (e1,id) -> 441 let (v1,l1) = eval_expr globalenv localenv m e1 in 442 (match v1 with 443 | (v,Tstruct(_,lst)) when List.mem (id,tt) lst -> 444 ((Mem.load m (mq_of_ty tt) (get_offset_struct v id lst),tt),l1) 445 | (v,Tunion(_,lst)) when List.mem (id,tt) lst -> 446 ((Mem.load m (mq_of_ty tt) v,tt),l1) 447 | _ -> ((Value.undef,tt),l1) 448 ) 449 | Ecost (lbl,e1) -> let (v1,l1) = eval_expr globalenv localenv m e1 in 450 (v1,lbl::l1) 451 | Ecall _ -> assert false (*For annotations only*) 452 453 and eval_lvalue globalenv localenv m expr = 454 let Expr (e,t) = expr in match e with 455 | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_) 456 | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_) | Eorbool (_,_) 457 | Esizeof _ -> assert false (*Not allowed in left side of assignement*) 458 | Efield (ee,id) -> let (v1,l1) = eval_expr globalenv localenv m ee in 459 (match v1 with 460 | (v,Tstruct(_,lst)) when List.mem (id,t) lst -> 461 ((get_offset_struct v id lst,t),l1) 462 | (v,Tunion(_,lst)) when List.mem (id,t) lst -> ((v,t),l1) 463 | _ -> ((Value.undef,t),l1) 464 ) 465 | Evar id -> ((find_symbol globalenv localenv id,t),[]) 466 | Ederef ee -> let ((v,_),l1) = eval_expr globalenv localenv m ee in 467 ((v,t),l1) 468 | Ecost (lbl,ee) -> let (v,l) = eval_lvalue globalenv localenv m ee in 469 (v,lbl::l) 470 | Ecall _ -> assert false (*For annotation only*) 471 472 let eval_exprlist globalenv localenv m l = 473 let rec eval_exprlist_rec vl ll = function 474 | [] -> (vl,ll) 475 | e::lst -> 476 let (vl0,ll0) = eval_exprlist_rec vl ll lst 477 and ((v,_),t) = eval_expr globalenv localenv m e in 478 (v::vl0,t@ll0) 479 in eval_exprlist_rec [] [] l 480 481 let is_struct = function 482 | Tarray (_,_) | Tunion (_,_) | Tstruct (_,_) -> true 483 | _ -> false 484 485 let bind_parameters m param_l arg_l var_l = 486 let bind (m,e) (id,ty) arg = 487 if is_struct ty then ( 488 assert (arg=Value.undef); (*a parameter can't be a struct/union/array*) 489 let (m2,ptr2) = Mem.alloc m (sizeof ty) 490 in let (m3,ptr3) = Mem.alloc m2 (Mem.ptr_size) 491 in let m4 = Mem.store m3 (Mem.mq_of_ptr) ptr3 ptr2 492 in (m4, (Hashtbl.add e id ptr3;e) )) 493 else 494 let (m2,ptr) = Mem.alloc m (sizeof ty) in 495 let m3 = Mem.store m2 (mq_of_ty ty) ptr arg 496 in (m3, (Hashtbl.add e id ptr;e) ) 497 in 498 List.fold_left 499 (fun a b -> bind a b Value.undef) 500 (try List.fold_left2 bind (m,Hashtbl.create 13) param_l arg_l 501 with (Invalid_argument _) -> assert false) 502 var_l 503 504 let assign m v ty ptr = Mem.store m (mq_of_ty ty) ptr v 505 506 507 let type_of_fundef = function 508 | Internal f -> Tfunction (List.map snd f.fn_params,f.fn_return) 509 | External (_,p,t) -> Tfunction (p,t) 510 511 let rec free_list m = function 512 | [] -> m 513 | v::l -> free_list (Mem.free m v) l 514 515 let blocks_of_env e = 516 let l = ref [] in 517 Hashtbl.iter (fun _ b -> l:=b::(!l)) e;!l 518 519 let typeof e = let Expr (_,t) = e in t 520 521 let interpret_external vargs k m = function 522 | "scan_int" -> 523 Returnstate (Value.of_int (int_of_string (read_line ())), k, m) 524 | "print_int" when List.length vargs = 1 -> 525 Printf.printf "%d" (Value.to_int (List.hd vargs)) ; 526 Returnstate (Value.zero, k, m) 527 | "print_intln" when List.length vargs = 1 -> 528 Printf.printf "%d\n" (Value.to_int (List.hd vargs)) ; 529 Returnstate (Value.zero, k, m) 530 | "malloc" | "alloc" when List.length vargs = 1 -> 531 let (m',vv) = Mem.alloc m (Value.to_int (List.hd vargs)) in 532 Returnstate (vv, k, m') 533 | "exit" when List.length vargs = 1 -> Returnstate(List.hd vargs,Kstop,m) 534 | s -> Printf.eprintf "Error: unknown external function: %s\n" s; 535 assert false (*Unknown external function*) 536 537 let next_step globalenv = function 538 | State(f,Sassign(a1,a2),k,e,m) -> 539 let ((v1,t1),l1) = (eval_lvalue globalenv e m a1) 540 and ((v2,t2),l2) = eval_expr globalenv e m a2 541 in (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2) 542 | State(f,Scall(None,a,al),k,e,m) -> 543 let (v1,l1) = eval_expr globalenv e m a in 544 let fd = find_funct globalenv v1 545 and (vargs,l2) = (eval_exprlist globalenv e m al) in 546 if type_of_fundef fd = typeof a 547 then (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2) 548 else assert false (*Signature mismatches*) 549 | State(f,Scall(Some lhs,a,al),k,e,m) -> 550 let (v1,l1) = eval_expr globalenv e m a in 551 let fd = find_funct globalenv v1 552 and (vargs,l2) = (eval_exprlist globalenv e m al) 553 and ((v3,t3),l3) = eval_lvalue globalenv e m lhs in 554 if type_of_fundef fd = typeof a then 555 (Callstate(fd,vargs,Kcall(Some (v3, t3),f,e,k),m),l1@l2@l3) 556 else assert false (*Signature mismatches*) 557 | State(f,Ssequence(s1,s2),k,e,m) -> (State(f,s1,Kseq(s2,k),e,m),[]) 558 | State(f,Sskip,Kseq(s,k),e,m) -> (State(f,s,k,e,m),[]) 559 | State(f,Scontinue,Kseq(s,k),e,m) -> (State(f,Scontinue,k,e,m),[]) 560 | State(f,Sbreak,Kseq(s,k),e,m) -> (State(f,Sbreak,k,e,m),[]) 561 | State(f,Sifthenelse(a,s1,s2),k,e,m) -> 562 let (v1,l1) = eval_expr globalenv e m a in 563 if is_true v1 then (State(f,s1,k,e,m),l1) 564 else if is_false v1 then (State(f,s2,k,e,m),l1) 565 else assert false (*Wrong condition guard*) 566 | State(f,Swhile(a,s),k,e,m) -> 567 let (v1,l1) = eval_expr globalenv e m a in 568 if is_false v1 then (State(f,Sskip,k,e,m),l1) 569 else if is_true v1 then (State(f,s,Kwhile(a,s,k),e,m),l1) 570 else assert false (*Wrong condition guard*) 571 | State(f,Sskip,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[]) 572 | State(f,Scontinue,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[]) 573 | State(f,Sbreak,Kwhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[]) 574 | State(f,Sdowhile(a,s),k,e,m) -> (State(f,s,Kdowhile(a,s,k),e,m),[]) 575 | State(f,Sskip,Kdowhile(a,s,k),e,m) -> 576 let (v1,l1) = eval_expr globalenv e m a in 577 if is_false v1 then (State(f,Sskip,k,e,m),l1) 578 else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1) 579 else assert false (*Wrong condition guard*) 580 | State(f,Scontinue,Kdowhile(a,s,k),e,m) -> 581 let (v1,l1) = eval_expr globalenv e m a in 582 if is_false v1 then (State(f,Sskip,k,e,m),l1) 583 else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1) 584 else assert false (*Wrong condition guard*) 585 | State(f,Sbreak,Kdowhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[]) 586 | State(f,Sfor(a1,a2,a3,s),k,e,m) when a1<>Sskip -> 587 (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[]) 588 | State(f,Sfor(Sskip,a2,a3,s),k,e,m) -> 589 let (v1,l1) = eval_expr globalenv e m a2 in 590 if is_false v1 then (State(f,Sskip,k,e,m),l1) 591 else if is_true v1 then (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) 592 else assert false (*Wrong condition guard*) 593 | State(f,Sskip,Kfor2(a2,a3,s,k),e,m) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[]) 594 | State(f,Scontinue,Kfor2(a2,a3,s,k),e,m) -> 595 (State(f,a3,Kfor3(a2,a3,s,k),e,m),[]) 596 | State(f,Sbreak,Kfor2(a2,a3,s,k),e,m) -> (State(f,Sskip,k,e,m),[]) 597 | State(f,Sskip,Kfor3(a2,a3,s,k),e,m) -> 598 (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[]) 599 | State(f,Sreturn None,k,e,m) when f.fn_return = Tvoid -> 600 let m' = free_list m (blocks_of_env e) in 601 (Returnstate(Value.undef,(call_cont k),m'),[]) 602 | State(f,Sreturn (Some a),k,e,m) when f.fn_return<>Tvoid -> 603 let (v1,l1) = eval_expr globalenv e m a 604 and m' = free_list m (blocks_of_env e) in 605 (Returnstate(fst v1,call_cont k,m'),l1) 606 | State(f,Sskip,k,e,m) when f.fn_return = Tvoid && is_call_cont k -> 607 let m' = free_list m (blocks_of_env e) in 608 (Returnstate(Value.undef,k,m'),[]) 609 | State(f,Sswitch(a,sl),k,e,m) -> 610 let (n,l) = (match eval_expr globalenv e m a with 611 | ((v,_),ll) when Value.is_int v -> (Value.to_int v,ll) 612 | _ -> assert false (*Wrong switch index*) 613 ) in 614 (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l) 615 | State(f,Sskip,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[]) 616 | State(f,Sbreak,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[]) 617 | State(f,Scontinue,Kswitch k,e,m) -> (State(f,Scontinue,k,e,m),[]) 618 | State(f,Slabel(lbl,s),k,e,m) -> (State(f,s,k,e,m),[]) 619 | State(f,Scost(lbl,s),k,e,m) -> (State(f,s,k,e,m),[lbl]) 620 | State(f,Sgoto lbl,k,e,m) -> 621 (match find_label lbl f.fn_body (call_cont k) with 622 | Some (s',k') -> (State(f,s',k',e,m),[]) 623 | None -> assert false (*Label does not exist*)) 624 | Callstate(Internal f,vargs,k,m) -> 625 let (m',e) = bind_parameters m f.fn_params vargs f.fn_vars in 626 (State(f,f.fn_body,k,e,m'),[]) 627 | Callstate(External(id,targs,tres),vargs,k,m) 628 when List.length targs = List.length vargs -> 629 (interpret_external vargs k m id,[]) 410 let ((v1,t1),l1) = eval_expr localenv m e1 in 411 let addr = address_of_value (get_offset v1 id t1) in 412 ((Mem.load m (size_of_ctype tt) addr, tt), l1) 413 | Ecost (lbl,e1) -> 414 let (v1,l1) = eval_expr localenv m e1 in 415 (v1,lbl::l1) 416 | Ecall _ -> assert false (* only used by the annotation process *) 417 | Ecast (cty,exp) -> 418 let ((v,ty),l1) = eval_expr localenv m exp in 419 ((eval_cast (v,ty,cty),tt),l1) 420 421 and eval_lvalue localenv m (Expr (e,t)) = match e with 422 | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_) 423 | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_) | Eorbool (_,_) 424 | Esizeof _ -> assert false (*Not allowed in left side of assignement*) 425 | Evar id -> ((find_symbol localenv m id,t),[]) 426 | Ederef ee -> 427 let ((v,_),l1) = eval_expr localenv m ee in 428 ((address_of_value v,t),l1) 429 | Efield (ee,id) -> 430 let ((v,tt),l1) = eval_expr localenv m ee in 431 let v' = get_offset v id tt in 432 ((address_of_value v', t), l1) 433 | Ecost (lbl,ee) -> 434 let (v,l) = eval_lvalue localenv m ee in 435 (v,lbl::l) 436 | Ecall _ -> assert false (* only used in the annotation process *) 437 438 let eval_exprlist lenv mem es = 439 let f (vs, cost_lbls) e = 440 let ((v, _), cost_lbls') = eval_expr lenv mem e in 441 (vs @ [v], cost_lbls @ cost_lbls') in 442 List.fold_left f ([], []) es 443 444 445 let bind (mem, lenv) (x, ty) v = 446 let (mem, addr) = Mem.alloc mem (sizeof ty) in 447 let mem = Mem.store mem (sizeof ty) addr v in 448 let lenv = LocalEnv.add x addr lenv in 449 (mem, lenv) 450 451 let bind_var (mem, lenv) (x, ty) = bind (mem, lenv) (x, ty) Value.undef 452 453 let init_fun_env mem params args vars = 454 let lenv = LocalEnv.empty in 455 let (mem, lenv) = 456 try List.fold_left2 bind (mem, lenv) params args 457 with Invalid_argument _ -> error "wrong size of arguments." in 458 List.fold_left bind_var (mem, lenv) vars 459 460 let assign m v ty ptr = Mem.store m (size_of_ctype ty) ptr v 461 462 463 let free_local_env mem lenv = 464 let f _ addr mem = Mem.free mem addr in 465 LocalEnv.fold f lenv mem 466 467 let condition v a_true a_false = 468 if Value.is_false v then a_false 469 else if Value.is_true v then a_true 470 else error "undefined condition guard value." 471 472 let eval_stmt f k e m s = match s, k with 473 | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[]) 474 | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[]) 475 | Sskip, Kdowhile(a,s,k) -> 476 let ((v1, _),l1) = eval_expr e m a in 477 let a_false = (State(f,Sskip,k,e,m),l1) in 478 let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in 479 condition v1 a_true a_false 480 | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[]) 481 | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[]) 482 | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[]) 483 | Sskip, Kcall _ -> 484 let m' = free_local_env m e in 485 (Returnstate(Value.undef,k,m'),[]) 486 | Sassign(a1, a2), _ -> 487 let ((v1,t1),l1) = (eval_lvalue e m a1) in 488 let ((v2,t2),l2) = eval_expr e m a2 in 489 (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2) 490 | Scall(None,a,al), _ -> 491 let ((v1,_),l1) = eval_expr e m a in 492 let fd = Mem.find_fun_def m (address_of_value v1) in 493 let (vargs,l2) = eval_exprlist e m al in 494 (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2) 495 | Scall(Some lhs,a,al), _ -> 496 let ((v1,_),l1) = eval_expr e m a in 497 let fd = Mem.find_fun_def m (address_of_value v1) in 498 let (vargs,l2) = eval_exprlist e m al in 499 let (vt3,l3) = eval_lvalue e m lhs in 500 (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m),l1@l2@l3) 501 | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m),[]) 502 | Sifthenelse(a,s1,s2), _ -> 503 let ((v1,_),l1) = eval_expr e m a in 504 let a_true = (State(f,s1,k,e,m),l1) in 505 let a_false = (State(f,s2,k,e,m),l1) in 506 condition v1 a_true a_false 507 | Swhile(a,s), _ -> 508 let ((v1,_),l1) = eval_expr e m a in 509 let a_false = (State(f,Sskip,k,e,m),l1) in 510 let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in 511 condition v1 a_true a_false 512 | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[]) 513 | Sfor(Sskip,a2,a3,s), _ -> 514 let ((v1,_),l1) = eval_expr e m a2 in 515 let a_false = (State(f,Sskip,k,e,m),l1) in 516 let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in 517 condition v1 a_true a_false 518 | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[]) 519 | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[]) 520 | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[]) 521 | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[]) 522 | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[]) 523 | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[]) 524 | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[]) 525 | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[]) 526 | Scontinue, Kdowhile(a,s,k) -> 527 let ((v1,_),l1) = eval_expr e m a in 528 let a_false = (State(f,Sskip,k,e,m),l1) in 529 let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in 530 condition v1 a_true a_false 531 | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[]) 532 | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[]) 533 | Sreturn None, _ -> 534 let m' = free_local_env m e in 535 (Returnstate(Value.undef,(call_cont k),m'),[]) 536 | Sreturn (Some a), _ -> 537 let ((v1,_),l1) = eval_expr e m a in 538 let m' = free_local_env m e in 539 (Returnstate(v1,call_cont k,m'),l1) 540 | Sswitch(a,sl), _ -> 541 let ((v,_),l) = eval_expr e m a in 542 let n = Value.to_int v in 543 (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l) 544 | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[]) 545 | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl]) 546 | Sgoto lbl, _ -> 547 let (s', k') = find_label lbl f.fn_body (call_cont k) in 548 (State(f,s',k',e,m),[]) 549 | _ -> assert false (* should be impossible *) 550 551 552 module InterpretExternal = Primitive.Interpret (Mem) 553 554 let interpret_external k mem f args = 555 let (mem', v) = match InterpretExternal.t mem f args with 556 | (mem', InterpretExternal.V v) -> (mem', v) 557 | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in 558 Returnstate (v, k, mem') 559 560 let step_call args cont mem = function 561 | Internal f -> 562 let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in 563 State (f, f.fn_body, cont, e, mem') 564 | External(id,targs,tres) when List.length targs = List.length args -> 565 interpret_external cont mem id args 566 | External(id,_,_) -> 567 error ("wrong size of arguments when calling external " ^ id ^ ".") 568 569 let step = function 570 | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt 571 | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[]) 630 572 | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[]) 631 573 | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) -> 632 let m' = assign m v ty vv in 633 (State(f,Sskip,k,e,m'),[]) 634 | st -> 635 Printf.eprintf "Error: no transition for %s\n" (string_of_state st); 636 assert false 637 638 let init_to_data = function 574 let m' = assign m v ty vv in 575 (State(f,Sskip,k,e,m'),[]) 576 | _ -> error "state malformation." 577 578 579 let data_of_init_data = function 639 580 | Init_int8 i -> Data_int8 i 640 581 | Init_int16 i -> Data_int16 i 641 582 | Init_int32 i -> Data_int32 i 642 | Init_float32 f -> assert false (* Not supported *)643 | Init_float64 f -> assert false (* Not supported *)583 | Init_float32 f -> error_float () 584 | Init_float64 f -> error_float () 644 585 | Init_space i -> Data_reserve i 645 | Init_addrof (_,_) -> assert false (*TODO*) 646 647 let alloc_datas m ((_,lst),ty) = 648 let store_data (m,ptr) = function (*FIXME signed or unsigned ?*) 649 | Init_int8 i -> (Mem.store m Memory.MQ_int8signed ptr (Value.of_int i) 650 ,Value.add ptr (Value.of_int 1)) 651 | Init_int16 i -> (Mem.store m Memory.MQ_int16signed ptr (Value.of_int i) 652 ,Value.add ptr (Value.of_int 2)) 653 | Init_int32 i -> (Mem.store m Memory.MQ_int32 ptr (Value.of_int i) 654 ,Value.add ptr (Value.of_int 4)) 655 | Init_float32 _ -> assert false (*Not supported*) 656 | Init_float64 _ -> assert false (*Not supported*) 657 | Init_space n -> (m,Value.add ptr (Value.of_int n)) 658 | Init_addrof (_,_) -> assert false (*TODO*) 659 in let (m2,ptr) = (Mem.alloc m (sizeof ty)) 660 in (fst (List.fold_left store_data (m2,ptr) lst),ptr) 661 662 let initmem_clight prog = 663 let alloc_funct i (g,f) (id,fct) = 664 Hashtbl.add g id (Value.of_int (-i-1)); 665 Valtbl.add f (Value.of_int (-i-1)) fct; 666 (g,f) 667 and alloc_var (m,g) v = 668 let (m',ptr) = alloc_datas m v in 669 if is_struct (snd v) then 670 let (m2,ptr2) = Mem.alloc m' (Mem.ptr_size) in 671 let m3 = Mem.store m2 Mem.mq_of_ptr ptr2 ptr in 672 Hashtbl.add g (fst (fst v)) ptr2;(m3,g) 673 else 674 ( (Hashtbl.add g (fst (fst v)) ptr);(m',g) ) 675 in let (m,g) = 676 List.fold_left alloc_var (Mem.empty,Hashtbl.create 13) prog.prog_vars 677 in let (g2,f) = 678 MiscPottier.foldi alloc_funct (g,Valtbl.create 13) prog.prog_funct 679 in 680 (m,(g2,f)) 586 | Init_addrof (x,off) -> assert false (* TODO: need the size of [x]'s cells *) 587 588 let init_mem prog = 589 let f_var mem ((x, init_datas), ty) = 590 Mem.add_var mem x (List.map data_of_init_data init_datas) in 591 let mem = List.fold_left f_var Mem.empty prog.prog_vars in 592 let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in 593 List.fold_left f_fun_def mem prog.prog_funct 681 594 682 595 let compute_result v = … … 684 597 else IntValue.Int8.zero 685 598 686 let interpret debug prog = match prog.prog_main with 687 | None -> (IntValue.Int8.zero, []) 688 | Some main -> 689 let (m,g) = initmem_clight prog in 690 let first_state = (Callstate(find_funct_id g main,[],Kstop,m),[]) in 691 let rec exec trace = function 692 | (Returnstate(v,Kstop,m),l) -> 693 (* 694 if debug then ( 695 print_string ("Result: "^(Value.to_string v)); 696 print_string ("\nMemory dump: \n"); 697 Mem.print m 698 ); 699 *) 700 let (res, cost_labels) as trace = (compute_result v, l@trace) in 701 if debug then 702 Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ; 703 trace 704 | (State(_,Sskip,Kstop,_,m),l) -> (*Implicit return in main*) 705 (* 706 if debug then ( 707 print_string ("Result: (implicit return)"); 708 print_string ("\nMemory dump: \n"); 709 Mem.print m 710 ); 711 *) 712 let (res, cost_labels) as trace = (IntValue.Int8.zero, l@trace) in 713 if debug then 714 Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ; 715 trace 716 | (state,l) -> 717 (* 718 if debug then print_string ((string_of_state state)^"\n"); 719 *) 720 exec (l@trace) (next_step g state) 721 in 722 (* 723 if debug then print_string "> --- Interpret Clight --- <\n"; 724 *) 725 exec [] first_state 599 let rec exec debug trace (state, l) = 600 let cost_labels = l @ trace in 601 let print_and_return_result res = 602 if debug then Printf.printf "Result = %s\n%!" 603 (IntValue.Int8.to_string res) ; 604 (res, cost_labels) in 605 if debug then print_state state ; 606 match state with 607 | Returnstate(v,Kstop,_) -> (* Explicit return in main *) 608 print_and_return_result (compute_result v) 609 | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *) 610 print_and_return_result IntValue.Int8.zero 611 | state -> exec debug cost_labels (step state) 612 613 let interpret debug prog = 614 if debug then Printf.printf "*** Clight ***\n\n%!" ; 615 match prog.prog_main with 616 | None -> (IntValue.Int8.zero, []) 617 | Some main -> 618 let mem = init_mem prog in 619 let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in 620 exec debug [] first_state -
Deliverables/D2.2/8051/src/clight/clightInterpret.mli
r486 r740 3 3 can also print debug informations. *) 4 4 5 (** [interpret debug p] returns the trace of execution of program [p]. *) 6 5 7 val interpret: bool -> Clight.program -> AST.trace -
Deliverables/D2.2/8051/src/clight/clightParser.ml
r486 r740 1 1 let process file = 2 let tmp_file = Filename.temp_file "cparser" ".i" 2 let tmp_file1 = Filename.temp_file "cparser1" ".c" 3 and tmp_file2 = Filename.temp_file "cparser2" ".i" 3 4 and prepro_opts = [] in 5 6 (* Add CerCo's primitives *) 7 let _ = 8 try 9 let oc = open_out tmp_file1 in 10 output_string oc Primitive.prototypes ; 11 close_out oc 12 with Sys_error _ -> failwith "Error adding primitive prototypes." in 13 let rc = Sys.command 14 (Printf.sprintf "cat %s >> %s" 15 (Filename.quote file) (Filename.quote tmp_file1)) in 16 if rc <> 0 then ( 17 Misc.SysExt.safe_remove tmp_file1; 18 failwith "Error adding primitive prototypes." 19 ); 4 20 5 21 (* Preprocessing *) … … 8 24 (Printf.sprintf "gcc -E -U__GNUC__ %s %s > %s" 9 25 (String.concat " " (List.map Filename.quote prepro_opts)) 10 (Filename.quote file) (Filename.quote tmp_file)) in26 (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in 11 27 if rc <> 0 then ( 12 Misc.SysExt.safe_remove tmp_file; failwith "Error calling gcc." 28 Misc.SysExt.safe_remove tmp_file1; 29 Misc.SysExt.safe_remove tmp_file2; 30 failwith "Error calling gcc." 13 31 ); 14 32 15 33 (* C to Cil *) 16 let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file in 17 Misc.SysExt.safe_remove tmp_file; 34 let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in 35 Misc.SysExt.safe_remove tmp_file1; 36 Misc.SysExt.safe_remove tmp_file2; 18 37 match r with 19 38 | None -> failwith "Error during C parsing." -
Deliverables/D2.2/8051/src/clight/clightToCminor.ml
r624 r740 2 2 open Cminor 3 3 open Clight 4 5 6 let error_prefix = "Cminor to RTLabs" 7 let error = Error.global_error error_prefix 8 let error_float () = error "float not supported." 9 4 10 5 11 (*For internal use*) … … 14 20 let ptr_size = Driver.CminorMemory.ptr_size 15 21 let alignment = Driver.CminorMemory.alignment 16 let ptr_mq = Memory.MQ_pointer17 22 18 23 let fresh_tmp variables = … … 36 41 | _ -> Sig_int 37 42 38 let rec mq_of_ty = function43 let rec size_of_ty = function 39 44 | Tvoid -> assert false 40 45 | Tfloat _ -> assert false (*Not supported*) 41 46 | Tfunction (_,_) -> assert false (*Not supported*) 42 | Tint (I8,Signed) -> Memory.MQ_int8signed43 | Tint (I8,Unsigned) -> Memory.MQ_int8unsigned44 | Tint (I16,Signed) -> Memory.MQ_int16signed45 | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned47 | Tint (I8,Signed) -> 1 48 | Tint (I8,Unsigned) -> 1 49 | Tint (I16,Signed) -> 2 50 | Tint (I16,Unsigned) -> 2 46 51 (*FIXME MQ_int32 : signed or unsigned ? *) 47 | Tint (I32,Signed) -> Memory.MQ_int3248 | Tint (I32,Unsigned) -> Memory.MQ_int3252 | Tint (I32,Signed) -> 4 53 | Tint (I32,Unsigned) -> 4 49 54 | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_) 50 | Tcomp_ptr _ -> ptr_mq 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 () 51 69 52 70 let init_to_data l = List.map ( … … 103 121 Op2 (Op_addp,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t)))) 104 122 | (Tint(_,_),Tpointer t) -> 105 Op2 (Op_addp, Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))),e2)123 Op2 (Op_addp,e2,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t)))) 106 124 | (Tarray (t,_),Tint(_,_)) -> 107 125 Op2 (Op_addp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t))))) … … 115 133 | (Tpointer t,Tint(_,_)) -> 116 134 Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t))))) 117 | (Tint(_,_),Tpointer t) ->118 Op2 (Op_subp,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))),e2)119 135 | (Tarray (t,_),Tint(_,_)) -> 120 136 Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t))))) 121 | (Tint(_,_),Tarray(t,_)) ->122 Op2 (Op_subp,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))123 137 | _ -> assert false (*Type error*) 124 138 … … 129 143 130 144 let translate_div e1 e2 = function 131 (*132 145 | (Tint(_,Signed),Tint(_,Signed)) -> Op2 (Op_div,e1,e2) 133 *)134 (* TODO: temporary hack! *)135 | (Tint(_,Signed),Tint(_,Signed)) -> Op2 (Op_divu,e1,e2)136 146 | (Tint(_,Unsigned),Tint(_,Unsigned)) -> Op2 (Op_divu,e1,e2) 137 147 | (Tfloat _,Tfloat _) -> assert false (*Not supported*) … … 157 167 158 168 let make_cast e = function 159 | (Tint( _,_),Tint(I8,Signed)) when int_size>8-> Op1 (Op_cast8signed,e)160 | (Tint( _,_),Tint(I8,Unsigned)) when int_size>8-> Op1 (Op_cast8unsigned,e)161 | (Tint( _,_),Tint(I16,Signed)) when int_size>16-> Op1 (Op_cast16signed,e)162 | (Tint( _,_),Tint(I16,Unsigned)) when int_size>16-> Op1 (Op_cast16unsigned,e)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) 163 173 | _ -> e 164 174 … … 191 201 | (Local,_) -> Id id 192 202 | (Stack o,ty) when is_struct ty -> Cst (Cst_stackoffset o) 193 | (Stack o,_) -> Mem (mq_of_ty c,Cst (Cst_stackoffset o)) 203 | (Stack o,_) -> 204 Mem (quantity_of_ty c,Cst (Cst_stackoffset o)) 194 205 | (Param,_) -> Id id 195 206 | (Global,ty) when is_struct ty -> Cst (Cst_addrsymbol id) 196 | (Global,_) -> Mem (mq_of_ty c,Cst (Cst_addrsymbol id)) 207 | (Global,_) -> 208 Mem (quantity_of_ty c,Cst (Cst_addrsymbol id)) 197 209 ) with Not_found -> assert false) 198 210 | Ederef e when is_ptr_to_struct (get_type e) -> 199 211 translate_expr variables e 200 | Ederef e -> Mem ( mq_of_ty c,translate_expr variables e)212 | Ederef e -> Mem (quantity_of_ty c,translate_expr variables e) 201 213 | Eaddrof se -> ( 202 214 match se with … … 248 260 | Tstruct(_,lst) -> 249 261 (try 250 Mem ( mq_of_ty (List.assoc id lst)262 Mem (quantity_of_ty (List.assoc id lst) 251 263 ,Op2(Op_add 252 264 ,translate_expr variables e … … 258 270 | Tunion(_,lst) -> 259 271 (try 260 Mem ( mq_of_ty (List.assoc id lst), translate_expr variables e)272 Mem (quantity_of_ty (List.assoc id lst), translate_expr variables e) 261 273 with Not_found -> assert false (*field does not exists*) 262 274 ) … … 270 282 (try (match Hashtbl.find variables v with 271 283 | (Local,_) -> St_assign (v,translate_expr variables e) 272 | (Stack o,_) -> St_store ( mq_of_ty t284 | (Stack o,_) -> St_store (quantity_of_ty t 273 285 ,Cst (Cst_stackoffset o) 274 286 ,translate_expr variables e) 275 287 | (Param,_) -> St_assign (v,translate_expr variables e) 276 | (Global,_) -> St_store ( mq_of_ty t288 | (Global,_) -> St_store (quantity_of_ty t 277 289 ,Cst (Cst_addrsymbol v) 278 290 ,translate_expr variables e) 279 291 ) with Not_found -> assert false) 280 | Expr (Ederef ee,t) -> St_store ( mq_of_ty t292 | Expr (Ederef ee,t) -> St_store (quantity_of_ty t 281 293 ,translate_expr variables ee 282 294 ,translate_expr variables e) … … 284 296 (match ee with 285 297 | Expr (_,Tstruct(_,lst)) -> 286 St_store ( mq_of_ty t298 St_store (quantity_of_ty t 287 299 ,Op2(Op_add,translate_expr variables ee 288 300 ,Cst(Cst_int (get_offset_struct 0 id lst ))) 289 301 ,translate_expr variables e) 290 | Expr (_,Tunion(_,_)) -> St_store ( mq_of_ty t302 | Expr (_,Tunion(_,_)) -> St_store (quantity_of_ty t 291 303 ,translate_expr variables ee 292 304 ,translate_expr variables e) … … 319 331 St_seq ( 320 332 st_call (Some tmp) (Type_ret (ctype_to_sig_type tt)) 321 ,St_store ( mq_of_ty tt,Cst (Cst_stackoffset o),Id tmp)333 ,St_store (quantity_of_ty tt,Cst (Cst_stackoffset o),Id tmp) 322 334 ) 323 335 | (Global,_) -> … … 325 337 St_seq ( 326 338 st_call (Some tmp) (Type_ret (ctype_to_sig_type tt)) 327 ,St_store ( mq_of_ty tt,Cst (Cst_addrsymbol v),Id tmp)339 ,St_store (quantity_of_ty tt,Cst (Cst_addrsymbol v),Id tmp) 328 340 ) 329 341 ) with Not_found -> assert false ) … … 526 538 527 539 let translate p = 528 (* TODO: Clight32 to Clight8 transformation *)529 (*530 540 let p = Clight32ToClight8.translate p in 531 *)532 (* <DEBUG> *)533 (*534 Printf.printf "%s\n%!" (ClightPrinter.print_program p) ;535 *)536 (* </DEBUG> *)537 541 let globals = List.map (fun p -> (fst (fst p),snd p) ) p.prog_vars in 538 542 let p = … … 540 544 Cminor.functs = List.map (translate_funct globals ) p.prog_funct; 541 545 Cminor.main = p.prog_main } in 546 (* TODO: find a better solution to get the pointers in the result. *) 542 547 CminorPointers.fill p -
Deliverables/D2.2/8051/src/cminor/cminor.mli
r486 r740 10 10 | Op1 of AST.op1 * expression 11 11 | Op2 of AST.op2 * expression * expression 12 | Mem of Memory. memory_q* expression (* Memory read *)12 | Mem of Memory.quantity * expression (* Memory read *) 13 13 | Cond of expression * expression * expression (* Ternary expression *) 14 14 | Exp_cost of CostLabel.t * expression (* Labelled expression *) … … 17 17 | St_skip 18 18 | St_assign of AST.ident * expression 19 | St_store of Memory. memory_q* expression * expression19 | St_store of Memory.quantity * expression * expression 20 20 21 21 (* Function call. Parameters are an optional variable to store the -
Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml
r640 r740 20 20 let increment cost_id incr = 21 21 let cost = Cminor.Cst (AST.Cst_addrsymbol cost_id) in 22 let load = Cminor.Mem (Memory. MQ_int32, cost) in22 let load = Cminor.Mem (Memory.QInt 4, cost) in 23 23 let incr = Cminor.Op2 (AST.Op_add, load, Cminor.Cst (AST.Cst_int incr)) in 24 Cminor.St_store (Memory. MQ_int32, cost, incr)24 Cminor.St_store (Memory.QInt 4, cost, incr) 25 25 26 26 -
Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml
r619 r740 4 4 module Mem = Driver.CminorMemory 5 5 module Value = Mem.Value 6 module Valtbl = Hashtbl.Make(Value) 7 8 9 let print_hashtbl h name = 10 print_string ("Hashtbl "^name^":\n"); 11 Hashtbl.iter (fun a _ -> print_string (" - "^a^"\n") ) h 12 13 (* Type definition *) 14 15 type local_env = (ident,Value.t) Hashtbl.t 6 module LocalEnv = Map.Make(String) 7 type local_env = Value.t LocalEnv.t 8 type memory = Cminor.function_def Mem.memory 9 10 11 let error_prefix = "Cminor interpret" 12 let error s = Error.global_error error_prefix s 13 let warning s = Error.warning error_prefix s 14 let error_float () = error "float not supported." 15 16 17 (* Helpers *) 18 19 let value_of_address = List.hd 20 let address_of_value v = [v] 21 22 23 (* State of execution *) 16 24 17 25 type continuation = … … 20 28 | Ct_endblock of continuation 21 29 | Ct_returnto of 22 ident option*internal_function*Value. t*local_env*continuation30 ident option*internal_function*Value.address*local_env*continuation 23 31 24 32 type state = 25 33 State_regular of 26 internal_function*statement*continuation*Value. t*local_env*(function_def Mem.memory)34 internal_function*statement*continuation*Value.address*local_env*(function_def Mem.memory) 27 35 | State_call of function_def*Value.t list*continuation*(function_def Mem.memory) 28 36 | State_return of Value.t*continuation*(function_def Mem.memory) 29 37 30 (* Local environment abstraction *) 31 32 let get_local_value e id = 33 try Hashtbl.find e id 34 with Not_found -> assert false (*Wrong ident*) 35 36 let set_local_value e id v = Hashtbl.add e id v 37 38 (* Create_local_env : 39 * constructs the local environement from effective parameters. *) 40 let create_local_env arg params vars = 41 let h = Hashtbl.create 11 in 42 if List.length params = List.length arg then 43 ( 44 for i=1 to (List.length params) do 45 Hashtbl.add h (List.nth params (i-1)) (List.nth arg (i-1)) 46 done; 47 for i=1 to (List.length vars) do 48 Hashtbl.add h (List.nth vars (i-1)) Value.undef 49 done; 50 h 51 ) 52 else assert false (*Wrong number of parameters*) 53 54 (* Pretty Printing and debug *) 55 56 let string_of_cont = function 57 Ct_stop -> "stop" 58 | Ct_cont(s1,_) -> (CminorPrinter.string_of_statement s1)^"::cont" 59 | Ct_endblock(_) -> "endblock" 60 | Ct_returnto(_,_,_,_,_) -> "returnto" 61 62 let string_of_state = function 63 State_regular(_,s,c,_,_,_) -> 64 "State_regular { " 65 ^(CminorPrinter.string_of_statement s)^" - "^(string_of_cont c)^" }" 66 | State_call(F_ext(e),v,c,_) -> 67 "State_call { extern " 68 ^e.ef_tag 69 ^"(" 70 ^(String.concat "," (List.map (fun vv -> Value.to_string vv) v)) 71 ^") - " 72 ^(string_of_cont c)^" }" 73 | State_call(F_int(i),v,c,_) -> 74 "State_call { function(" 75 ^(String.concat "," (List.map (fun vv -> Value.to_string vv) v)) 76 ^") - " 77 ^(string_of_cont c)^" }" 78 | State_return(v,c,_) -> 79 "State_return { "^(Value.to_string v)^" - "^(string_of_cont c)^" }" 80 81 (* Global environment abstraction *) 82 83 (* Symbol : returns the block corresponding to the identifier 84 * id in the global environement g *) 85 let symbol g id = let (id_b,b_fd) = g in 86 try Hashtbl.find id_b id 87 with Not_found -> assert false 88 89 (* Funct : returns the definition of the function located in block b *) 90 let funct g b = let (id_b,b_fd) = g in 91 try Valtbl.find b_fd b 92 with Not_found -> assert false 93 38 let string_of_local_env lenv = 39 let f x v s = s ^ x ^ " = " ^ (Value.to_string v) ^ " " in 40 LocalEnv.fold f lenv "" 41 42 let string_of_expr = CminorPrinter.print_expression 43 44 let string_of_args args = 45 "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")" 46 47 let rec string_of_statement = function 48 | St_skip -> "skip" 49 | St_assign (x, e) -> x ^ " = " ^ (string_of_expr e) 50 | St_store (q, e1, e2) -> 51 Printf.sprintf "%s[%s] = %s" 52 (Memory.string_of_quantity q) (string_of_expr e1) (string_of_expr e2) 53 | St_call (None, f, args, _) 54 | St_tailcall (f, args, _) -> (string_of_expr f) ^ (string_of_args args) 55 | St_call (Some x, f, args, _) -> 56 x ^ " = " ^ (string_of_expr f) ^ (string_of_args args) 57 | St_seq _ -> "sequence" 58 | St_ifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")" 59 | St_loop _ -> "loop" 60 | St_block _ -> "block" 61 | St_exit n -> "exit " ^ (string_of_int n) 62 | St_switch (e, _, _) -> "switch (" ^ (string_of_expr e) ^ ")" 63 | St_return None -> "return" 64 | St_return (Some e) -> "return (" ^ (string_of_expr e) ^ ")" 65 | St_label (lbl, _) -> "label " ^ lbl 66 | St_goto lbl -> "goto " ^ lbl 67 | St_cost (lbl, _) -> "cost " ^ lbl 68 69 let print_state = function 70 | State_regular (_, stmt, _, sp, lenv, mem) -> 71 Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\n\nRegular state: %s\n\n%!" 72 (string_of_local_env lenv) 73 (Mem.to_string mem) 74 (Value.to_string (value_of_address sp)) 75 (string_of_statement stmt) 76 | State_call (_, args, _, mem) -> 77 Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!" 78 (Mem.to_string mem) 79 (MiscPottier.string_of_list " " Value.to_string args) 80 | State_return (v, _, mem) -> 81 Printf.printf "Memory:%s\nReturn state: %s\n\n%!" 82 (Mem.to_string mem) 83 (Value.to_string v) 84 85 86 (* Global and local environment management *) 87 88 let init_local_env args params vars = 89 let f_param lenv x v = LocalEnv.add x v lenv in 90 let f_var lenv x = LocalEnv.add x Value.undef lenv in 91 let lenv = List.fold_left2 f_param LocalEnv.empty params args in 92 List.fold_left f_var lenv vars 93 94 let find_fundef f mem = 95 let addr = Mem.find_global mem f in 96 Mem.find_fun_def mem addr 94 97 95 98 96 99 (* Expression evaluation *) 97 100 98 let eval_constant global_env stack = function 99 Cst_int i -> Value.of_int i 100 | Cst_float _ -> assert false 101 | Cst_addrsymbol id -> symbol global_env id 102 | Cst_stackoffset o -> stack 103 104 let eval_unop arg = function 105 Op_cast8unsigned -> Value.cast8unsigned arg 106 | Op_cast8signed -> Value.cast8signed arg 107 | Op_cast16unsigned -> Value.cast16unsigned arg 108 | Op_cast16signed -> Value.cast16signed arg 109 | Op_negint -> Value.negint arg 110 | Op_notbool -> Value.notbool arg 111 | Op_notint -> Value.notint arg 112 | Op_negf -> assert false (*Not supported*) 113 | Op_absf -> assert false (*Not supported*) 114 | Op_singleoffloat -> assert false (*Not supported*) 115 | Op_intoffloat -> assert false (*Not supported*) 116 | Op_intuoffloat -> assert false (*Not supported*) 117 | Op_floatofint -> assert false (*Not supported*) 118 | Op_floatofintu -> assert false (*Not supported*) 119 | Op_id -> arg 120 | Op_ptrofint -> assert false (*Not supported*) 121 | Op_intofptr -> assert false (*Not supported*) 122 123 let eval_binop arg1 arg2 = function 124 Op_add -> Value.add arg1 arg2 125 | Op_sub -> Value.sub arg1 arg2 126 | Op_mul -> Value.mul arg1 arg2 127 | Op_div -> Value.div arg1 arg2 128 | Op_divu -> Value.divu arg1 arg2 129 | Op_mod -> Value.modulo arg1 arg2 130 | Op_modu -> Value.modulou arg1 arg2 131 | Op_and -> Value.and_op arg1 arg2 132 | Op_or -> Value.or_op arg1 arg2 133 | Op_xor -> Value.xor arg1 arg2 134 | Op_shl -> Value.shl arg1 arg2 135 | Op_shr -> Value.shr arg1 arg2 136 | Op_shru -> Value.shru arg1 arg2 137 | Op_addf -> assert false (*Not supported*) 138 | Op_subf -> assert false (*Not supported*) 139 | Op_mulf -> assert false (*Not supported*) 140 | Op_divf -> assert false (*Not supported*) 141 | Op_cmp(Cmp_eq) -> Value.cmp_eq arg1 arg2 142 | Op_cmp(Cmp_ne) -> Value.cmp_ne arg1 arg2 143 | Op_cmp(Cmp_gt) -> Value.cmp_gt arg1 arg2 144 | Op_cmp(Cmp_ge) -> Value.cmp_ge arg1 arg2 145 | Op_cmp(Cmp_lt) -> Value.cmp_lt arg1 arg2 146 | Op_cmp(Cmp_le) -> Value.cmp_le arg1 arg2 147 | Op_cmpu(Cmp_eq) -> Value.cmp_eq_u arg1 arg2 148 | Op_cmpu(Cmp_ne) -> Value.cmp_ne_u arg1 arg2 149 | Op_cmpu(Cmp_gt) -> Value.cmp_gt_u arg1 arg2 150 | Op_cmpu(Cmp_ge) -> Value.cmp_ge_u arg1 arg2 151 | Op_cmpu(Cmp_lt) -> Value.cmp_lt_u arg1 arg2 152 | Op_cmpu(Cmp_le) -> Value.cmp_le_u arg1 arg2 153 | Op_cmpf(_) -> assert false (*Not supported*) 154 | Op_addp -> Value.add arg1 arg2 155 | Op_subp -> Value.sub arg1 arg2 156 | Op_cmpp(Cmp_eq) -> Value.cmp_eq arg1 arg2 157 | Op_cmpp(Cmp_ne) -> Value.cmp_ne arg1 arg2 158 | Op_cmpp(Cmp_gt) -> Value.cmp_gt arg1 arg2 159 | Op_cmpp(Cmp_ge) -> Value.cmp_ge arg1 arg2 160 | Op_cmpp(Cmp_lt) -> Value.cmp_lt arg1 arg2 161 | Op_cmpp(Cmp_le) -> Value.cmp_le arg1 arg2 162 163 let rec eval_expression global_env stack local_env memory = function 164 Id(str) -> (get_local_value local_env str,[]) 165 | Cst(c) -> (eval_constant global_env stack c,[]) 101 let eval_constant stack m = function 102 | Cst_int i -> Value.of_int i 103 | Cst_float _ -> error_float () 104 | Cst_addrsymbol id when Mem.mem_global m id -> 105 value_of_address (Mem.find_global m id) 106 | Cst_addrsymbol id -> error ("unknown global variable " ^ id ^ ".") 107 | Cst_stackoffset o -> Value.add (value_of_address stack) (Value.of_int o) 108 109 let eval_unop = function 110 | Op_negf 111 | Op_absf 112 | Op_singleoffloat 113 | Op_intoffloat 114 | Op_intuoffloat 115 | Op_floatofint 116 | Op_floatofintu -> error_float () 117 | Op_cast8unsigned -> Value.cast8unsigned 118 | Op_cast8signed -> Value.cast8signed 119 | Op_cast16unsigned -> Value.cast16unsigned 120 | Op_cast16signed -> Value.cast16signed 121 | Op_negint -> Value.negint 122 | Op_notbool -> Value.notbool 123 | Op_notint -> Value.notint 124 | Op_id -> (fun v -> v) 125 | Op_ptrofint -> assert false (*Not supported yet*) 126 | Op_intofptr -> assert false (*Not supported yet*) 127 128 let eval_binop = function 129 | Op_add 130 | Op_addp -> Value.add 131 | Op_sub 132 | Op_subp -> Value.sub 133 | Op_mul -> Value.mul 134 | Op_div -> Value.div 135 | Op_divu -> Value.divu 136 | Op_mod -> Value.modulo 137 | Op_modu -> Value.modulou 138 | Op_and -> Value.and_op 139 | Op_or -> Value.or_op 140 | Op_xor -> Value.xor 141 | Op_shl -> Value.shl 142 | Op_shr -> Value.shr 143 | Op_shru -> Value.shru 144 | Op_addf 145 | Op_subf 146 | Op_mulf 147 | Op_divf 148 | Op_cmpf _ -> error_float () 149 | Op_cmp(Cmp_eq) 150 | Op_cmpp(Cmp_eq) -> Value.cmp_eq 151 | Op_cmp(Cmp_ne) 152 | Op_cmpp(Cmp_ne) -> Value.cmp_ne 153 | Op_cmp(Cmp_gt) 154 | Op_cmpp(Cmp_gt) -> Value.cmp_gt 155 | Op_cmp(Cmp_ge) 156 | Op_cmpp(Cmp_ge) -> Value.cmp_ge 157 | Op_cmp(Cmp_lt) 158 | Op_cmpp(Cmp_lt) -> Value.cmp_lt 159 | Op_cmp(Cmp_le) 160 | Op_cmpp(Cmp_le) -> Value.cmp_le 161 | Op_cmpu(Cmp_eq) -> Value.cmp_eq_u 162 | Op_cmpu(Cmp_ne) -> Value.cmp_ne_u 163 | Op_cmpu(Cmp_gt) -> Value.cmp_gt_u 164 | Op_cmpu(Cmp_ge) -> Value.cmp_ge_u 165 | Op_cmpu(Cmp_lt) -> Value.cmp_lt_u 166 | Op_cmpu(Cmp_le) -> Value.cmp_le_u 167 168 let rec eval_expression stack local_env memory = function 169 | Id x when LocalEnv.mem x local_env -> (LocalEnv.find x local_env,[]) 170 | Id x -> error ("unknown local variable " ^ x ^ ".") 171 | Cst(c) -> (eval_constant stack memory c,[]) 166 172 | Op1(op,arg) -> 167 let (v,l) = eval_expression global_envstack local_env memory arg in168 (eval_unop v op,l)173 let (v,l) = eval_expression stack local_env memory arg in 174 (eval_unop op v,l) 169 175 | Op2(op,arg1,arg2) -> 170 let (v1,l1) = eval_expression global_env stack local_env memory arg1171 and (v2,l2) = eval_expression global_envstack local_env memory arg2 in172 (eval_binop v1 v2 op,l1@l2)173 | Mem( k,a) ->174 let (v,l) = (eval_expression global_env stack local_env memory a)in175 (Mem.load memory k v,l)176 let (v1,l1) = eval_expression stack local_env memory arg1 in 177 let (v2,l2) = eval_expression stack local_env memory arg2 in 178 (eval_binop op v1 v2,l1@l2) 179 | Mem(q,a) -> 180 let (v,l) = eval_expression stack local_env memory a in 181 (Mem.loadq memory q (address_of_value v),l) 176 182 | Cond(a1,a2,a3) -> 177 let (v1,l1) = eval_expression global_env stack local_env memory a1 in 178 if Value.is_true v1 then 179 let (v2,l2) = eval_expression global_env stack local_env memory a2 in 180 (v2,l1@l2) 181 else if Value.is_false v1 then 182 let (v2,l2) = eval_expression global_env stack local_env memory a3 in 183 (v2,l1@l2) 184 else assert false (*A boolean value is expected*) 183 let (v1,l1) = eval_expression stack local_env memory a1 in 184 if Value.is_true v1 then 185 let (v2,l2) = eval_expression stack local_env memory a2 in 186 (v2,l1@l2) 187 else 188 if Value.is_false v1 then 189 let (v3,l3) = eval_expression stack local_env memory a3 in 190 (v3,l1@l3) 191 else error "undefined conditional value." 185 192 | Exp_cost(lbl,e) -> 186 let (v,l) = eval_expression global_env stack local_env memory e in 187 (v,l@[lbl]) 193 let (v,l) = eval_expression stack local_env memory e in 194 (v,l@[lbl]) 195 196 let eval_exprlist sp lenv mem es = 197 let f (vs, cost_lbls) e = 198 let (v, cost_lbls') = eval_expression sp lenv mem e in 199 (vs @ [v], cost_lbls @ cost_lbls') in 200 List.fold_left f ([], []) es 188 201 189 202 (* State transition *) … … 224 237 | Some(v) -> v 225 238 226 (*FIXME To move in AST*) 227 let string_of_sig sign = 228 let rec tmp = function 229 | [] -> "" 230 | Sig_int::l -> "int "^(tmp l) 231 | Sig_float::l -> "float "^(tmp l) 232 | Sig_ptr::l -> "ptr "^(tmp l) 233 in 234 match sign.res with 235 | Type_void -> (tmp sign.args)^" -> void" 236 | Type_ret Sig_int ->(tmp sign.args)^" -> int" 237 | Type_ret Sig_float ->(tmp sign.args)^" -> float" 238 | Type_ret Sig_ptr ->(tmp sign.args)^" -> ptr" 239 240 241 let call_state global_env sigma e m a1 params sgn cont = 242 let (f,l) = eval_expression global_env sigma e m a1 in 243 match funct global_env f with 244 | F_int(fi) -> 245 if fi.f_sig = sgn then ( 246 let tmp = List.map (eval_expression global_env sigma e m) params in 247 (State_call(F_int(fi),(List.map fst tmp),cont,m), 248 l@(List.flatten (List.map snd tmp))) 249 ) else ( 250 Printf.eprintf "Error: signature (%s) different from (%s) \n" 251 (string_of_sig fi.f_sig) 252 (string_of_sig sgn); 253 assert false) (*Signatures mismatche*) 254 | F_ext(fe) -> 255 if fe.ef_sig = sgn then ( 256 let tmp = List.map (eval_expression global_env sigma e m) params in 257 (State_call(F_ext(fe), (List.map fst tmp) ,cont,m), 258 l@(List.flatten (List.map snd tmp))) 259 ) else ( 260 Printf.eprintf "Error: signature (%s) different from (%s) \n" 261 (string_of_sig fe.ef_sig) 262 (string_of_sig sgn); 263 assert false) (*Signatures mismatche*) 264 265 let interpret_external f v k m = 266 try match f.ef_tag with 267 | "scan_int" -> 268 let res = Value.of_int (int_of_string (read_line ())) in 269 State_return (res, k, m) 270 | "print_int" -> 271 Printf.printf "%d" (Value.to_int (List.hd v)) ; 272 State_return (Value.zero, k, m) 273 | "print_intln" -> 274 Printf.printf "%d\n" (Value.to_int (List.hd v)) ; 275 State_return (Value.zero, k, m) 276 | "alloc" | "malloc" -> 277 let (m',vv) = Mem.alloc m (Value.to_int (List.hd v)) in 278 State_return (vv, k, m') 279 | "exit" -> 280 State_return (List.hd v,Ct_stop,m) 281 | s -> 282 Printf.eprintf "Error: unknown external function: %s\n" s; 283 assert false (*Unknown external function*) 284 with 285 Failure _ -> assert false (*Wrong number of arguments*) 286 287 let state_transition state global_env = match state with 288 289 (* Transition semantics for Cminor, part 1: statements *) 290 291 State_regular(f,St_skip,Ct_cont(s,k),sigma,e,m) -> 292 (State_regular(f, s, k, sigma, e, m),[]) 293 | State_regular(f,St_skip,Ct_endblock(k),sigma,e,m) -> 294 (State_regular(f, St_skip, k, sigma, e, m),[]) 295 | State_regular(f,St_assign(str,exp),k,sigma,e,m) -> 296 let (v,l) = eval_expression global_env sigma e m exp in 297 set_local_value e str v; 298 (State_regular(f, St_skip, k, sigma, e, m),l) 299 | State_regular(f,St_store(q,a1,a2),k,sigma,e,m) -> 300 let (v1,l1) = eval_expression global_env sigma e m a1 in 301 let (v2,l2) = eval_expression global_env sigma e m a2 in 302 (State_regular(f, St_skip, k, sigma, e, Mem.store m q v1 v2),l1@l2) 303 | State_regular(f,St_seq(s1,s2),k,sigma,e,m) -> 304 (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[]) 305 | State_regular(f,St_ifthenelse(exp,s1,s2),k,sigma,e,m) -> 306 let (v,l) = eval_expression global_env sigma e m exp in 307 if Value.is_true v then (State_regular(f,s1,k,sigma,e,m),l) 308 else if Value.is_false v then (State_regular(f,s2,k,sigma,e,m),l) 309 else ( 310 Printf.eprintf "Error: %s is not a boolean.\n" (Value.to_string v); 311 assert false (*boolean value expected*)) 312 | State_regular(f,St_loop(s),k,sigma,e,m) -> 313 (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[]) 314 | State_regular(f,St_block(s),k,sigma,e,m) -> 315 (State_regular(f,s,(Ct_endblock k),sigma,e,m),[]) 316 | State_regular(f,St_exit(n),Ct_cont(s,k),sigma,e,m) -> 317 (State_regular(f,(St_exit n),k,sigma,e,m),[]) 318 | State_regular(f,St_exit(n),Ct_endblock(k),sigma,e,m) when n=0 -> 319 (State_regular(f,St_skip,k,sigma,e,m),[]) 320 | State_regular(f,St_exit(n),Ct_endblock(k),sigma,e,m) when (n>0) -> 321 (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[]) 322 | State_regular(f,St_switch(exp,lst,def),k,sigma,e,m) -> 323 let (v,l) = eval_expression global_env sigma e m exp in 324 (try (State_regular 325 (f, St_exit (List.assoc (Value.to_int v) lst),k, sigma, e, m),l) 326 with Not_found -> 327 (State_regular (f, St_exit def, k, sigma, e, m),l) ) 328 | State_regular(f,St_label(_,s),k,sigma,e,m) -> 329 (State_regular(f,s,k,sigma,e,m),[]) 330 | State_regular(f,St_cost(lbl,s),k,sigma,e,m) -> 331 (State_regular(f,s,k,sigma,e,m),[lbl]) 332 | State_regular(f,St_goto(lbl),k,sigma,e,m) -> 333 let (s2,k2) = findlabel lbl f.f_body (callcont k) 334 in (State_regular(f,s2,k2,sigma,e,m),[]) 335 336 (* Transition semantics for Cminor, part 2: 337 * functions, initial states, final states *) 338 339 | State_regular(f,St_call(id,a1,params,sgn),k,sigma,e,m) -> 340 call_state global_env sigma e m a1 params sgn (Ct_returnto(id,f,sigma,e,k)) 341 | State_regular(f,St_tailcall(a1,params,sgn),k,sigma,e,m) -> 342 call_state global_env sigma e m a1 params sgn (callcont k) 343 | State_regular(f,St_skip,Ct_returnto(p1,p2,p3,p4,p5),sigma,e,m) 344 when f.f_sig.res = Type_void -> 345 (State_return (Value.undef,Ct_returnto(p1,p2,p3,p4,p5),Mem.free m sigma),[]) 346 | State_regular(f,St_skip,Ct_stop,sigma,e,m) when f.f_sig.res = Type_void -> 347 (State_return (Value.undef,Ct_stop,Mem.free m sigma),[]) 348 | State_regular(f,St_return(_),k,sigma,e,m) when f.f_sig.res = Type_void -> 349 (State_return (Value.undef,callcont k,Mem.free m sigma),[]) 350 | State_regular(f,St_return(Some(a)),k,sigma,e,m) 351 when f.f_sig.res != Type_void -> 352 let (v,l) = eval_expression global_env sigma e m a in 239 240 let call_state sigma e m f params cont = 241 let (addr,l1) = eval_expression sigma e m f in 242 let fun_def = Mem.find_fun_def m (address_of_value addr) in 243 let (args,l2) = eval_exprlist sigma e m params in 244 (State_call(fun_def,args,cont,m),l1@l2) 245 246 let eval_stmt f k sigma e m s = match s, k with 247 | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m),[]) 248 | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[]) 249 | St_skip, (Ct_returnto _ as k) -> 250 (State_return (Value.undef,k,Mem.free m sigma),[]) 251 | St_skip,Ct_stop -> 252 (State_return (Value.undef,Ct_stop,Mem.free m sigma),[]) 253 | St_assign(x,exp),_ -> 254 let (v,l) = eval_expression sigma e m exp in 255 let e = LocalEnv.add x v e in 256 (State_regular(f, St_skip, k, sigma, e, m),l) 257 | St_store(q,a1,a2),_ -> 258 let (v1,l1) = eval_expression sigma e m a1 in 259 let (v2,l2) = eval_expression sigma e m a2 in 260 let m = Mem.storeq m q (address_of_value v1) v2 in 261 (State_regular(f, St_skip, k, sigma, e, m),l1@l2) 262 | St_call(xopt,f',params,_),_ -> 263 call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,k)) 264 | St_tailcall(f',params,_),_ -> 265 call_state sigma e m f' params (callcont k) 266 | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[]) 267 | St_ifthenelse(exp,s1,s2),_ -> 268 let (v,l) = eval_expression sigma e m exp in 269 let next_stmt = 270 if Value.is_true v then s1 271 else 272 if Value.is_false v then s2 273 else error "undefined conditional value." in 274 (State_regular(f,next_stmt,k,sigma,e,m),l) 275 | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[]) 276 | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m),[]) 277 | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m),[]) 278 | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m),[]) 279 | St_exit(n),Ct_endblock(k) -> 280 (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[]) 281 | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m),[]) 282 | St_goto(lbl),_ -> 283 let (s2,k2) = findlabel lbl f.f_body (callcont k) in 284 (State_regular(f,s2,k2,sigma,e,m),[]) 285 | St_switch(exp,lst,def),_ -> 286 let (v,l) = eval_expression sigma e m exp in 287 if Value.is_int v then 288 try 289 let i = Value.to_int v in 290 let nb_exit = 291 if List.mem_assoc i lst then List.assoc i lst 292 else def in 293 (State_regular(f, St_exit nb_exit,k, sigma, e, m),l) 294 with _ -> error "int value too big." 295 else error "undefined switch value." 296 | St_return(None),_ -> 297 (State_return (Value.undef,callcont k,Mem.free m sigma),[]) 298 | St_return(Some(a)),_ -> 299 let (v,l) = eval_expression sig