Changeset 1585 for Deliverables/D2.2


Ignore:
Timestamp:
Dec 2, 2011, 7:49:19 PM (9 years ago)
Author:
tranquil
Message:

fighting with a bug of the translation from RTL to ERTL

Location:
Deliverables/D2.2/8051/src
Files:
2 added
11 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.mli

    r486 r1585  
    22(** This module provides a function to print [ERTL] programs.  *)
    33
     4val print_statement : ERTL.statement -> string
     5
    46val print_program : ERTL.program -> string

  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTL.ml

    r1272 r1585  
    104104        match Liveness.eliminable (G.liveafter label) stmt with
    105105        | Some successor ->
    106             LTL.St_skip successor
     106          Printf.printf "dead %s!\n%!" (ERTLPrinter.print_statement stmt);
     107          LTL.St_skip successor
    107108        | None ->
    108109            I.translate_statement stmt

  • Deliverables/D2.2/8051/src/ERTL/liveness.ml

    r1580 r1585  
    207207
    208208let eliminable ((pliveafter, hliveafter) : L.t) (stmt : statement) =
     209  let res =
    209210  match stmt with
    210211  | St_skip _
    … …  
    240241  | St_set_hdw (r, _, l)
    241242  | St_hdw_to_hdw (r, _, l) ->
    242     if I8051.RegisterSet.mem r hliveafter then None else Some l
     243    if I8051.RegisterSet.mem r hliveafter then None else Some l in
     244  Printf.printf "%s %sfound eliminable\n"
     245    (ERTLPrinter.print_statement stmt)
     246    (match res with
     247      | Some _ -> ""
     248      | _ -> "not "); res
    243249
    244250(* This is the abstract semantics of instructions. It defines the

  • Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

    r1572 r1585  
    4747let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
    4848let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
    49 let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
     49let forget_ind st =   Printf.printf "forgetting\n";
     50{ st with inds = CostLabel.forget_const_ind st.inds }
    5051let enter_loop st = CostLabel.enter_loop st.inds
    5152let continue_loop st = CostLabel.continue_loop st.inds
    … …  
    101102  Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)
    102103
    103 let init_fun_call lbls_offs st ptr def =
     104let init_fun_call name lbls_offs st ptr def =
    104105  let pc = entry_pc lbls_offs ptr def in
    105106  let st = new_ind st in
     107  Printf.printf "calling %s\n" name;
    106108  change_pc st pc
    107109
    … …  
    209211  change_pc st next_pc
    210212
    211 let interpret_call lbls_offs st ptr ra =
     213let interpret_call name lbls_offs st ptr ra =
    212214  match Mem.find_fun_def st.mem ptr with
    213215    | LTL.F_int def ->
    214216      let st = save_ra lbls_offs st ra in
    215       init_fun_call lbls_offs st ptr def
     217      init_fun_call name lbls_offs st ptr def
    216218    | LTL.F_ext def ->
    217219      let next_pc =
    … …  
    220222
    221223let interpret_return lbls_offs st =
     224  Printf.printf "returning\n";
    222225  let st = forget_ind st in
    223226  let (st, pc) = return_pc st in
    … …  
    325328
    326329    | LTL.St_call_id (f, lbl) ->
    327       interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
     330      interpret_call f lbls_offs st (Mem.find_global st.mem f) lbl
    328331
    329332    | LTL.St_call_ptr lbl ->
    330       interpret_call lbls_offs st (dptr st) lbl
     333      interpret_call (Val.string_of_address (dptr st)) lbls_offs st (dptr st) lbl
    331334
    332335    | LTL.St_condacc (lbl_true, lbl_false) ->
    … …  
    359362    (res, cost_labels) in
    360363  if debug then print_state lbls_offs st ;
     364  Printf.printf "%s\n" (Val.string_of_address st.pc);
    361365  match fetch_stmt lbls_offs st with
    362366    | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
    … …  
    407411  match Mem.find_fun_def st.mem ptr with
    408412    | LTL.F_int def ->
    409       init_fun_call lbls_offs st ptr def
     413      init_fun_call main lbls_offs st ptr def
    410414    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
    411415

  • Deliverables/D2.2/8051/src/RTL/RTLConstPropagation.ml

    r1584 r1585  
    3838  val bind_2
    3939    : Register.t -> Register.t -> t option * t option -> property -> property
    40   val find : Register.t -> property -> t option
     40  val find_in : Register.t -> property -> t option
     41  val find_out : Register.t -> property -> t option
    4142  val find_carry_in : property -> t option
    4243  val equal : property -> property -> bool
    4344  val is_maximal : property -> bool
    44   val is_cst : Register.t -> property -> bool
    45   val find_cst : Register.t -> property -> int
    46   val find_cst_opt : Register.t -> property -> int option
     45  val is_cst_in : Register.t -> property -> bool
     46  val find_cst_in : Register.t -> property -> int
     47  val find_cst_opt_in : Register.t -> property -> int option
     48  val is_cst_out : Register.t -> property -> bool
     49  val find_cst_out : Register.t -> property -> int
     50  val find_cst_opt_out : Register.t -> property -> int option
    4751  val find_cst_carry_in : property -> int option
    4852
    … …  
    5660
    5761  type property = {
    58     regs : t Register.FlexMap.t ; (* no need to have out and in *)
     62    in_regs : t Register.FlexMap.t ;
     63    out_regs : t Register.FlexMap.t ;
    5964    in_c : t option ;
    6065    out_c : t option
    … …  
    6267
    6368  let bottom : property =
    64     { regs = Register.FlexMap.empty; in_c = None; out_c = None }
     69    { in_regs = Register.FlexMap.empty;
     70      out_regs = Register.FlexMap.empty;
     71      in_c = None; out_c = None }
    6572
    6673  let join_t x y = match x, y with
    … …  
    7279    let choose _ = join_t in
    7380    let carry = join_t p.out_c q.out_c in
    74     { regs = Register.FlexMap.merge choose p.regs q.regs;
     81    let regs = Register.FlexMap.merge choose p.out_regs q.out_regs in
     82    {
     83      in_regs = regs;
     84      out_regs = regs;
    7585      in_c = carry;
    7686      out_c = carry
    … …  
    7989  let bind r t p =
    8090    let regs = match t with
    81       | Some v -> Register.FlexMap.add r v p.regs
    82       | None -> Register.FlexMap.remove r p.regs in
    83     { p with regs = regs }
     91      | Some v -> Register.FlexMap.add r v p.out_regs
     92      | None -> Register.FlexMap.remove r p.out_regs in
     93    { p with out_regs = regs }
    8494
    8595  let bind_carry t p = { p with out_c = t }
    … …  
    94104    bind s u (bind r v p)
    95105
    96   let find r p = to_opt_2 Register.FlexMap.find r p.regs
     106  let find_in r p = to_opt_2 Register.FlexMap.find r p.in_regs
     107  let find_out r p = to_opt_2 Register.FlexMap.find r p.out_regs
    97108  let find_carry_in p = p.in_c
    98109
    … …  
    112123    equal_t_opt_as_bool p.in_c q.in_c &&
    113124      equal_t_opt_as_bool p.out_c q.out_c &&
    114       Register.FlexMap.equal equal_t p.regs q.regs
     125      Register.FlexMap.equal equal_t p.in_regs q.in_regs &&
     126      Register.FlexMap.equal equal_t p.out_regs q.out_regs
     127
    115128
    116129  let is_maximal _ = false
    117130
    118   let is_cst r p =
     131  let is_cst_in r p =
    119132    try
    120       match Register.FlexMap.find r p.regs with
     133      match Register.FlexMap.find r p.in_regs with
    121134        | V _ -> true
    122135        | T -> false
    … …  
    124137      | Not_found -> false
    125138
    126   let find_cst r p =
    127     match find r p with
     139  let is_cst_out r p =
     140    try
     141      match Register.FlexMap.find r p.out_regs with
     142        | V _ -> true
     143        | T -> false
     144    with
     145      | Not_found -> false
     146
     147  let find_cst_in r p =
     148    match find_in r p with
    128149      | Some (V v) -> Val.to_int v
    129150      | _ -> raise Not_found
    130151
    131   let find_cst_opt r p =
    132     try Some (find_cst r p) with
     152  let find_cst_out r p =
     153    match find_out r p with
     154      | Some (V v) -> Val.to_int v
     155      | _ -> raise Not_found
     156
     157  let find_cst_opt_in r p =
     158    try Some (find_cst_in r p) with
     159      | Not_found -> None
     160
     161  let find_cst_opt_out r p =
     162    try Some (find_cst_in r p) with
    133163      | Not_found -> None
    134164
    … …  
    150180let cst i =  L.V (Val.of_int i)
    151181
    152 let find_arg a prop = match a with
    153   | Reg r -> L.find r prop
     182let find_arg_in a prop = match a with
     183  | Reg r -> L.find_in r prop
    154184  | Imm k -> Some (cst k)
    155185
    … …  
    159189    (j : Register.t)
    160190    : L.t option =
    161   let x = L.find j prop in
     191  let x = L.find_in j prop in
    162192  match x with
    163193    | Some (L.V v) -> Some (L.V (Eval.op1 op v))
    … …  
    173203    (b : argument)
    174204    : L.t option * L.t option =
    175   let x = find_arg a prop in
    176   let y = find_arg b prop in
     205  let x = find_arg_in a prop in
     206  let y = find_arg_in b prop in
    177207  let c = L.find_carry_in prop in
    178208  match x, y, c, op with
    … …  
    243273    (b : argument)
    244274    : L.t option * L.t option =
    245   let x = find_arg a prop in
    246   let y = find_arg b prop in
     275  let x = find_arg_in a prop in
     276  let y = find_arg_in b prop in
    247277  match x, y, op with
    248278    | _, Some (L.V v2), I8051.DivuModu when Val.is_false v2 ->
    … …  
    285315  match Label.Map.find lbl graph with
    286316
    287     | St_move (r, a, _) -> L.bind r (find_arg a pred_prop) pred_prop
     317    | St_move (r, a, _) -> L.bind r (find_arg_in a pred_prop) pred_prop
    288318    | St_op1 (op, r, s, _) -> L.bind r (do_the_op1 op pred_prop s) pred_prop
    289319    | St_op2 (op, r, a, b, _) ->
    … …  
    317347(* now that the info for constants can be gathered, let's put that to use *)
    318348
    319 let find_cst_arg prop = function
     349let find_cst_arg_in prop = function
    320350  | Imm k -> Some k
    321   | Reg r -> L.find_cst_opt r prop
     351  | Reg r -> L.find_cst_opt_in r prop
    322352
    323353let arg_from_arg prop a =
    324   match find_cst_arg prop a with
     354  match find_cst_arg_in prop a with
    325355    | Some k -> Imm k
    326356    | None -> a
    327357
     358let move i a prop =
     359  match arg_from_arg prop a with
     360    | Reg j when i = j -> []
     361    | Imm k when L.find_cst_opt_in i prop = Some k -> []
     362    | a' -> [St_move (i, a', Label.dummy)]
     363
    328364let simpl_imm_op2 op i a b prop l =
    329   match find_cst_arg prop a, find_cst_arg prop b,
     365  match find_cst_arg_in prop a, find_cst_arg_in prop b,
    330366    L.find_cst_carry_in prop, op with
    331367    | Some 0, _, _, (I8051.Or | I8051.Xor)
    … …  
    336372    | Some 255, _, Some 1, I8051.Addc
    337373    | Some 255, _, _, I8051.And ->
    338       St_move (i, b, l)
     374      move i b prop
    339375    | _, Some 0, _, (I8051.Or | I8051.Xor)
    340376    | _, Some 0, Some 0, (I8051.Addc | I8051.Sub | I8051.Add)
    341377    | _, Some 255, Some 1, I8051.Addc
    342378    | _, Some 255, _, I8051.And ->
    343       St_move (i, a, l)
     379      move i a prop
    344380    | _, _, Some 0, I8051.Addc ->
    345381      (* does not change time, but maybe helps getting better results
    346382         with liveness analysis *)
    347       St_op2 (I8051.Add, i, arg_from_arg prop a, arg_from_arg prop b, l)
     383      [St_op2 (I8051.Add, i, arg_from_arg prop a, arg_from_arg prop b, l)]
    348384    | _ ->
    349       St_op2 (op, i, arg_from_arg prop a, arg_from_arg prop b, l)
     385      [St_op2 (op, i, arg_from_arg prop a, arg_from_arg prop b, l)]
    350386
    351387let simpl_imm_opaccs op i j a b prop l =
    352   match find_cst_arg prop a, find_cst_arg prop b, op with
     388  match find_cst_arg_in prop a, find_cst_arg_in prop b, op with
    353389    | Some 1, _, I8051.Mul ->
    354       [St_move (i, b, l) ; St_move (j, Imm 0, l)]
     390      move i b prop @ move j (Imm 0) prop
    355391    |  _, Some 1, (I8051.Mul | I8051.DivuModu) ->
    356       [St_move (i, a, l) ; St_move (j, Imm 0, l)]
     392      move i a prop @ move j (Imm 0) prop
    357393    | _ ->
    358394      [St_opaccs (op, i, j, arg_from_arg prop a, arg_from_arg prop b, l)]
     395
    359396
    360397(* we transform statements according to the valuation found out by analyze *)
    … …  
    369406    (stmt : statement) : statement list * Label.t list option =
    370407  match stmt with
    371     | (St_op1 (_,i,_,l) | St_op2(_,i,_,_,l) | St_move (i, _, l))
    372         when L.is_cst i (valu p) ->
    373       ([St_move (i, Imm (L.find_cst i (valu p)), p)], None)
     408    | St_move (i, a, l) ->
     409      (move i a (valu p), None)
     410    | (St_op1 (_,i,_,l) | St_op2(_,i,_,_,l))
     411        when L.is_cst_out i (valu p) ->
     412      (move i (Imm (L.find_cst_out i (valu p))) (valu p), None)
    374413    | St_op2 (op, i, a, b, l) ->
    375       ([simpl_imm_op2 op i a b (valu p) l], None)
     414      (simpl_imm_op2 op i a b (valu p) l, None)
    376415    | St_opaccs (op, i, j, a, b, l) ->
    377416      (simpl_imm_opaccs op i j a b (valu p) l, None)
    … …  
    383422                 arg_from_arg (valu p) c, l)], None)
    384423    | St_cond (i, if_true, if_false) as s ->
    385       (match L.find_cst_opt i (valu p) with
     424      (match L.find_cst_opt_in i (valu p) with
    386425        | Some 0 -> ([], Some [if_false])
    387426        | Some _ -> ([], Some [if_true])

  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r1584 r1585  
    294294      | I8051.Add ->
    295295        (* we perform a first add followed by Addc's *)
    296         let f destr srcr1 srcr2 (op, insts) =
    297           (I8051.Addc, f_add op destr srcr1 srcr2 :: insts) in
    298         snd (MiscPottier.fold3_right
    299           f destrs_common srcrs1_common srcrs2_common (I8051.Add, []))
     296        begin match destrs_common, srcrs1_common, srcrs2_common with
     297          | destr :: destrs, srcr1 :: srcrs1, srcr2 :: srcrs2 ->
     298            f_add op destr srcr1 srcr2 ::
     299              MiscPottier.map3 (f_add I8051.Addc) destrs srcrs1 srcrs2
     300          | [], [], [] -> []
     301          | _ -> assert false
     302        end
    300303      | _ ->
    301304        (* we just do the same operation on all *)
    … …  
    332335  (* the next must be an invariant *)
    333336  assert (srcrs1_n = destrs_n && destrs_n = srcrs1_n);
    334   (* we pad destrs with a copy of itself that will be added to it at the end
    335      (when the multiplication overflows) and then three more. The routine
    336      should thus handle overflow nicely, but it must be checked *)
    337   let all_destrs = MiscPottier.fill destrs (2 * destrs_n + 3) in
     337  (* we pad destrs with itself until we have two times as much
     338     registers. The routine should thus handle overflow nicely. *)
     339  let all_destrs = MiscPottier.fill destrs (2 * destrs_n) in
    338340  let init = translate_cst (AST.Cst_int 0) destrs :: init in
    339341  (* the registries to hold the temporary results of 8-bit mutliplication *)
    340342  let (def, a) = fresh_reg def in
    341343  let (def, b) = fresh_reg def in
    342   (* when getting the result, this is what is used (padded to 3 bytes *)
    343   let mul_arg = [RTL.Reg a ; RTL.Reg b ; RTL.Imm 0] in
     344  (* when getting the result, this is what is used (padded as necessary) *)
     345  let mul_arg k = [RTL.Reg a ; RTL.Reg b] @
     346    MiscPottier.make (RTL.Imm 0) (2*destrs_n - k - 2) in
     347  (* multiplication between the ith byte of srcrs1 and the jth byte of
     348     srcrs2 *)
    344349  let mul i j =
    345     let s1i, s2j = List.nth fresh_srcrs1 i, List.nth fresh_srcrs2 i in
     350    let s1i, s2j = List.nth fresh_srcrs1 i, List.nth fresh_srcrs2 j in
     351    (* the position in the result where the resulting bytes must be added *)
    346352    let k = i + j in
    347     let dloc = MiscPottier.sublist all_destrs k (k+3) in
     353    let dloc = MiscPottier.sublist all_destrs k (2*destrs_n) in
    348354    let dloc_arg = List.map (fun r -> RTL.Reg r) dloc in
     355    (* we add until the end to propagate the carry bit.
     356       At the beginning this will be useless, but we rely on
     357       RTL's constant propagation and later dead register elimination
     358       to amend that *)
    349359    [ adds_graph [RTL.St_opaccs (I8051.Mul, a, b, s1i, s2j, start_lbl)] ;
    350       translate_op I8051.Add dloc dloc_arg mul_arg ] in
     360      translate_op I8051.Add dloc dloc_arg (mul_arg k)] in
    351361  let insts = List.flatten (List.flatten
    352362    (MiscPottier.makei (fun i ->

  • Deliverables/D2.2/8051/src/checker.ml

    r1542 r1585  
    55    Misc.ListExt.assoc_diff occs_trace1 occs_trace2
    66  in
    7   let check_trace (_, (_, trace1)) (_, (_, trace2)) =
     7  let check_trace (_, (res1, trace1)) (_, (res2, trace2)) =
     8    IntValue.Int32.eq res1 res2 &&
    89    compare_trace trace1 trace2 = []
    910  in
    … …  
    2829      let diff = compare_trace trace1 trace2 in
    2930      Error.global_error "during trace comparison"
    30         (Printf.sprintf
    31            "The traces of two intermediate programs differ:\n%s"
    32            (print_trace lang1 lang2 diff))
     31        (Printf.sprintf "%s%s"
     32           (if res1 != res2 then
     33               Printf.sprintf
     34                 "The results of two intermediate programs differ:\n
     35                  in %s it was %d, in %s it was %d\n"
     36                 lang1
     37                 (IntValue.Int32.to_int res1)
     38                 lang2
     39                 (IntValue.Int32.to_int res2) else "")
     40           (Printf.sprintf "The traces of the two intermediate programs:\n%s"
     41           (print_trace lang1 lang2 diff)))

  • Deliverables/D2.2/8051/src/common/costLabel.ml

    r1542 r1585  
    4242let curr_ind = function
    4343    | hd :: _ -> hd
    44     | _ -> invalid_arg "non-empty indexing stack"
     44    | _ -> invalid_arg "empty indexing stack"
    4545
    4646let enter_loop inds = enter_loop_single (curr_ind inds)
    … …  
    5656let forget_const_ind = function
    5757        | _ :: inds -> inds
    58         | _ -> invalid_arg "non-empty indexing stack"
     58        | _ -> invalid_arg "empty indexing stack"
    5959
    6060let sexpr_of i l =

  • Deliverables/D2.2/8051/src/common/costLabel.mli

    r1542 r1585  
    3131
    3232(** This is equivalent to [List.hd], but raises
    33     [Invalid_argument "non-empty indexing stack"] if argument is empty *)
     33    [Invalid_argument "empty indexing stack"] if argument is empty *)
    3434val curr_const_ind : const_indexing list -> const_indexing
    3535
    … …  
    4646(** [continue_loop inds n] is used to update the indexing stack [inds] when
    4747    one is continuing a loop indexed by [n].
    48     @raise [Invalid_argument "non-empty indexing stack"] if [inds] is empty.
     48    @raise [Invalid_argument "empty indexing stack"] if [inds] is empty.
    4949    @raise [Invalid_argument "uninitialized loop index"] if the head of
    5050    [inds] has no value for [index]. *)
    … …  
    6161
    6262(** [forget_const_ind inds] pops and discards the top constant indexing from the
    63     stack [inds].  Raises [Invalid_argument "non-empty indexing stack"] if
     63    stack [inds].  Raises [Invalid_argument "empty indexing stack"] if
    6464    [inds] is empty. *)
    6565val forget_const_ind : const_indexing list -> const_indexing list

  • Deliverables/D2.2/8051/src/utilities/miscPottier.ml

    r1584 r1585  
    44  List.map f' (List.combine (List.combine al bl) cl)
    55
    6 let fold3_right f al bl cl =
    7   let f' ((a, b), c) d = f a b c d in
    8   List.fold_right f' (List.combine (List.combine al bl) cl)
     6let rec fold3_right f al bl cl d = match al, bl, cl with
     7  | a :: al, b :: bl, c :: cl ->
     8    f a b c (fold3_right f al bl cl d)
     9  | [], [], [] -> d
     10  | _ -> invalid_arg "fold3_right: list lengths do not match"
     11
     12let rec fold3_left f a bl cl dl = match bl, cl, dl with
     13  | b :: bl, c :: cl, d :: dl ->
     14    fold3_left f (f a b c d) bl cl dl
     15  | [], [], [] -> a
     16  | _ -> invalid_arg "fold3_left: list lengths do not match"
    917
    1018let rec max_list = function

  • Deliverables/D2.2/8051/src/utilities/miscPottier.mli

    r1584 r1585  
    1010   size. *)
    1111val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
     12val fold3_left : ('a -> 'b -> 'c -> 'd -> 'a) ->
     13  'a -> 'b list -> 'c list -> 'd list -> 'a
    1214val fold3_right : ('a -> 'b -> 'c -> 'd -> 'd) ->
    1315  'a list -> 'b list -> 'c list -> 'd -> 'd
Note: See TracChangeset for help on using the changeset viewer.