Changeset 619 for Deliverables/D2.2/8051/src/RTL

Timestamp:

Mar 2, 2011, 3:27:41 PM (9 years ago)

Author:

ayache

Message:

Update of D2.2 from Paris.

Location:

Deliverables/D2.2/8051/src/RTL

Files:

• RTLInterpret.ml (modified) (7 diffs)
• RTLInterpret.mli (modified) (1 diff)
• RTLToERTL.ml (modified) (3 diffs)

Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

@@ -41 +41 @@
 type state =
   | State of stack_frame list * RTL.graph * Label.t * Val.t (* sp *) *
-             local_env * Val.t (* carry *) * memory * AST.trace
+             local_env * Val.t (* carry *) * memory * CostLabel.t list
   | CallState of stack_frame list * RTL.function_def *
-                 Val.t list (* args *) * memory * AST.trace
+                 Val.t list (* args *) * memory * CostLabel.t list
   | ReturnState of stack_frame list * Val.t list (* return values *) *
-                   memory * AST.trace
+                   memory * CostLabel.t list
 
 
@@ -101 +101 @@
     (mem   : memory)
     (stmt  : RTL.statement)
-    (t     : AST.trace) :
+    (t     : CostLabel.t list) :
     state = match stmt with
 
@@ -269 +269 @@
     (args  : Val.t list)
     (mem   : memory)
-    (t     : AST.trace) :
+    (t     : CostLabel.t list) :
     state =
   match f_def with
@@ -286 +286 @@
     (ret_vals : Val.t list)
     (mem      : memory)
-    (t        : AST.trace) :
+    (t        : CostLabel.t list) :
     state =
   let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
@@ -311 +311 @@
     (Register.print r) (Val.to_string v))
 
-let rec iter_small_step st = match small_step st with
+let compute_result vs =
+  try
+    let v = MiscPottier.last vs in
+    if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
+    else IntValue.Int8.zero
+  with Not_found -> IntValue.Int8.zero
+
+let rec iter_small_step print_result st = match small_step st with
 (*
+  (* <DEBUG> *)
   | ReturnState ([], vs, mem, t) ->
     Mem.print mem ;
@@ -331 +339 @@
     Printf.printf "Carry = %s\n\n%!" (Val.to_string carry) ;
     iter_small_step st'
+  (* </DEBUG> *)
 *)
   | ReturnState ([], vs, mem, t) ->
-(*
-    Printf.printf "Return: %s\n%!" (print_ret_vals vs) ;
-*)
-    List.rev t
-  | st' -> iter_small_step st'
+    let (res, cost_labels) as trace = (compute_result vs, List.rev t) in
+    if print_result then
+      Printf.printf "RTL: %s\n%!" (IntValue.Int8.to_string res) ;
+    trace
+  | st' -> iter_small_step print_result st'
 
 
@@ -357 +366 @@
 (* Interpret the program only if it has a main. *)
 
-let interpret p = match p.RTL.main with
-  | None -> []
+let interpret print_result p = match p.RTL.main with
+  | None -> (IntValue.Int8.zero, [])
   | Some main ->
     let mem = init_mem p in
     let main_def = find_function mem main in
     let st = CallState ([], main_def, [], mem, []) in
-    iter_small_step st
+    iter_small_step print_result st

Deliverables/D2.2/8051/src/RTL/RTLInterpret.mli

@@ -3 +3 @@
     and return the trace of cost labels encountered. *)
 
-val interpret : RTL.program -> AST.trace
+val interpret : bool -> RTL.program -> AST.trace

Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

@@ -171 +171 @@
   | [] -> [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
   | [r] ->
-    [fun start_lbl ->
-      adds_graph [ERTL.St_set_hdw (I8051.st0, r, start_lbl)] start_lbl]
+    [fun start_lbl dest_lbl def ->
+      let (def, r_tmp) = fresh_reg def in
+      adds_graph [ERTL.St_int (r_tmp, 0, start_lbl) ;
+                  ERTL.St_set_hdw (I8051.st1, r_tmp, start_lbl) ;
+                  ERTL.St_set_hdw (I8051.st0, r, start_lbl)]
+        start_lbl dest_lbl def]
   | r1 :: r2 :: _ ->
     [(fun start_lbl ->
-      adds_graph [ERTL.St_set_hdw (I8051.st1, r1, start_lbl)] start_lbl) ;
-     (fun start_lbl ->
-       adds_graph [ERTL.St_set_hdw (I8051.st0, r2, start_lbl)] start_lbl)]
+      adds_graph [ERTL.St_set_hdw (I8051.st1, r1, start_lbl) ;
+                  ERTL.St_set_hdw (I8051.st0, r2, start_lbl)] start_lbl)]
 
 let add_epilogue ret_regs srah sral sregs def =
@@ -267 +270 @@
 
 (* Fetching the result depends on the type of the function, or say, the number
-   of registers that are waiting for a value. *)
+   of registers that are waiting for a value. Temporary non allocatable
+   registers are used. Indeed, moving directly from DPL to a pseudo-register may
+   cause a bug: DPL might be used to compute the address of the
+   pseudo-register. *)
 
 let fetch_result ret_regs start_lbl = match ret_regs with
   | [] -> adds_graph [ERTL.St_skip start_lbl] start_lbl
   | [r] ->
-    adds_graph
+      adds_graph
       [ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ;
        ERTL.St_get_hdw (r, I8051.st0, start_lbl)]
@@ -401 +407 @@
 
 
+(* Move the first cost label of each function at the beginning of the
+   function. Indeed, the instructions for calling conventions (stack allocation
+   for example) are added at the very beginning of the function, thus before the
+   first cost label. *)
+
+let generate stmt def =
+  let entry = Label.Gen.fresh def.ERTL.f_luniverse in
+  let def =
+    { def with ERTL.f_graph = Label.Map.add entry stmt def.ERTL.f_graph } in
+  { def with ERTL.f_entry = entry }
+
+let find_and_remove_first_cost_label def =
+  let rec aux lbl = match Label.Map.find lbl def.ERTL.f_graph with
+    | ERTL.St_cost (cost_label, next_lbl) ->
+      let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in
+      (cost_label, { def with ERTL.f_graph = graph })
+    | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl)
+    | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)
+    | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl)
+    | ERTL.St_addrL (_, _, lbl) | ERTL.St_int (_, _, lbl)
+    | ERTL.St_move (_, _, lbl) | ERTL.St_opaccs (_, _, _, _, lbl)
+    | ERTL.St_op1 (_, _, _, lbl) | ERTL.St_op2 (_, _, _, _, lbl)
+    | ERTL.St_clear_carry lbl | ERTL.St_load (_, _, _, lbl)
+    | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl)
+    | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl)
+      ->
+      aux lbl
+    | ERTL.St_condacc _ | ERTL.St_return _ ->
+      (* Should be impossible: the first cost label is found after some linear
+         instructions. *)
+      assert false in
+  aux def.ERTL.f_entry
+
+let move_first_cost_label_up_internal def =
+  let (cost_label, def) = find_and_remove_first_cost_label def in
+  generate (ERTL.St_cost (cost_label, def.ERTL.f_entry)) def
+
+let move_first_cost_label_up (id, def) =
+  let def' = match def with
+    | ERTL.F_int int_fun ->
+      ERTL.F_int (move_first_cost_label_up_internal int_fun)
+    | _ -> def in
+  (id, def')
+
+
 let translate p =
   (* We simplify tail calls as regular calls for now. *)
   let p = RTLtailcall.simplify p in
+  (* The tranformation on each RTL function: create an ERTL function and move
+     its first cost label at the very beginning. *)
+  let f funct = move_first_cost_label_up (translate_funct funct) in
   { ERTL.vars   = p.RTL.vars ;
-    ERTL.functs = List.map translate_funct p.RTL.functs ;
+    ERTL.functs = List.map f p.RTL.functs ;
     ERTL.main   = p.RTL.main }