Changeset 1328


Ignore:
Timestamp:
Oct 7, 2011, 5:47:39 PM (8 years ago)
Author:
tranquil
Message:
  • bug in ClightUtilities?.find_max_depth_lbld fixed
  • single-entry loop detection completed
  • work on Clight completed
Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/acc.ml

    r818 r1328  
    5454    List.iter save intermediate_asts;
    5555
    56   if Options.interpretation_requested () || Options.is_debug_enabled () then
     56  if Options.interpretation_requested () || Options.is_debug_enabled () ||
     57               Options.trace_requested () then
    5758    begin
    5859      let asts = target_asts in
     
    6061      let label_traces = List.map (Languages.interpret debug) asts in
    6162      Printf.eprintf "Checking execution traces...%!";
     63                        if Options.trace_requested () then
     64                                let print_l l =
     65                                        Printf.printf "%s, " (CostLabel.string_of_cost_label
     66                                                               ~pretty:true l) in
     67                          let print_ls ls = List.iter print_l (List.rev ls) in
     68                                let print_trace (v, ls) =
     69                                        Printf.printf "%s | " (Big_int.string_of_big_int v);
     70                                        print_ls ls;
     71                                        Printf.printf "\n" in
     72                                List.iter print_trace label_traces
     73                        else ();
    6274      Checker.same_traces (List.combine asts label_traces);
    6375      Printf.eprintf "OK.\n%!";
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightInterpret.ml

    r1319 r1328  
    152152  LocalEnv.fold f lenv ""
    153153
    154 let print_state = function
     154let print_state state = (match state with
    155155  | State (_, stmt, _, lenv, mem, c) ->
    156     Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing:"
     156    Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing: "
    157157      (string_of_local_env lenv)
    158158      (Mem.to_string mem);
     
    168168      (Mem.to_string mem)
    169169      (Value.to_string v)
     170        ); Printf.printf "---------------------------------------------------------\n"
    170171
    171172
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml

    r1319 r1328  
    11
    22(** This module defines the labelling of a [Clight] program. *)
     3
     4module IntListSet = Set.Make(struct type t = int list let compare = compare end)
    35
    46open Clight
     
    100102      Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2')
    101103  | Swhile (i,e,s) ->
    102                   let ind = match i with
     104                  let ind' = match i with
    103105                                | None -> ind
    104106                                | Some _ -> CostLabel.add_id_indexing ind in
    105       let s' = add_cost_labels_st ind cost_universe s in
    106       let s' = add_starting_cost_label ind cost_universe s' in
     107      let s' = add_cost_labels_st ind' cost_universe s in
     108      let s' = add_starting_cost_label ind' cost_universe s' in
     109                        (* exit label indexed with outside indexing *)
    107110      add_ending_cost_label ind cost_universe
    108111        (Swhile (i,add_cost_labels_e ind cost_universe e, s'))
    109112  | Sdowhile (i,e,s) ->
    110       let ind = match i with
     113      let ind' = match i with
    111114        | None -> ind
    112115        | Some _ -> CostLabel.add_id_indexing ind in
    113       let s' = add_cost_labels_st ind cost_universe s in
    114       let s' = add_starting_cost_label ind cost_universe s' in
     116      let s' = add_cost_labels_st ind' cost_universe s in
     117      let s' = add_starting_cost_label ind' cost_universe s' in
    115118      add_ending_cost_label ind cost_universe
    116119        (Sdowhile (i,add_cost_labels_e ind cost_universe e, s'))
    117120  | Sfor (i,s1,e,s2,s3) ->
    118121      let s1' = add_cost_labels_st ind cost_universe s1 in
    119       let ind = match i with
     122      let ind' = match i with
    120123        | None -> ind
    121124        | Some _ -> CostLabel.add_id_indexing ind in
    122       let s2' = add_cost_labels_st ind cost_universe s2 in
    123       let s3' = add_cost_labels_st ind cost_universe s3 in
    124       let s3' = add_starting_cost_label ind cost_universe s3' in
     125      let s2' = add_cost_labels_st ind' cost_universe s2 in
     126      let s3' = add_cost_labels_st ind' cost_universe s3 in
     127      let s3' = add_starting_cost_label ind' cost_universe s3' in
    125128      add_ending_cost_label ind cost_universe
    126129        (Sfor (i, s1', add_cost_labels_e ind cost_universe e, s2', s3'))
     
    147150
    148151
    149 (* Add cost labels to a function. *)
    150 
    151 let add_cost_labels_f ind cost_universe = function
    152   | (id,Internal fd) -> (id,Internal {
    153       fn_return = fd.fn_return ;
    154       fn_params = fd.fn_params ;
    155       fn_vars = fd.fn_vars ;
    156       fn_body = add_starting_cost_label ind cost_universe
    157                              (add_cost_labels_st ind cost_universe fd.fn_body)
    158     })
    159   | (id,External (a,b,c)) -> (id,External (a,b,c))
    160 
     152(* traversal of code assigning to every label the "loop address" of it. *)
     153(* A loop address like [2, 0, 1] means the corresponding label is in the *)
     154(* third loop inside the first loop inside the second loop of the body. The *)
     155(* type is *)
     156(* int list -> int -> map -> Clight.statement -> int * map *)
     157(* where map = int list Label.Map.t *)
     158let rec assign_loop_addrs_s current offset m = function
     159        (* I am supposing you cannot jump to the update statement of for loops... *)
     160        | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
     161                let (_, m) = assign_loop_addrs_s (offset :: current) 0 m s in
     162                (offset + 1, m)
     163        | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
     164                let (offset, m) = assign_loop_addrs_s current offset m s1 in
     165                assign_loop_addrs_s current offset m s2
     166        | Slabel(l,s) ->
     167                let (offset, m) = assign_loop_addrs_s current offset m s in
     168                (offset, Label.Map.add l current m)
     169        | Sswitch(_,ls) -> assign_loop_addrs_ls current offset m ls
     170        | _ -> (offset, m)
     171
     172and assign_loop_addrs_ls current offset m = function
     173  | LSdefault s -> assign_loop_addrs_s current offset m s
     174  | LScase(_,s,ls) ->
     175                let (offset, m) = assign_loop_addrs_s current offset m s in
     176                assign_loop_addrs_ls current offset m ls
     177
     178let rec is_prefix l1 l2 = match l1, l2 with
     179        | [], _ -> true
     180        | hd1 :: tl1, hd2 :: tl2 when hd1 = hd2 -> is_prefix tl1 tl2
     181        | _ -> false
     182
     183(* traversal of code which for every statement [s] returns the set of loop*)
     184(* addresses which are multi-entry due to a goto in [s]. The type is *)
     185(* map -> int list -> int -> statement -> int*set *)
     186(* where maps is as above, set = InListSet.t *)
     187let rec find_multi_entry_loops_s m current offset = function
     188        (* I am supposing you cannot jump to the update statement of for loops... *)
     189        | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
     190                        let current' = offset :: current in
     191                        let (_, set) = find_multi_entry_loops_s m current' 0 s in
     192                        (offset + 1, set)
     193        | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
     194          let (offset, set1) = find_multi_entry_loops_s m current offset s1 in
     195          let (offset, set2) = find_multi_entry_loops_s m current offset s2 in
     196          (offset, IntListSet.union set1 set2)
     197        | Slabel(_,s) -> find_multi_entry_loops_s m current offset s
     198                | Sgoto l ->
     199                        (* all labels should have a binding in m *)
     200                        let addr = Label.Map.find l m in
     201                        let cond = is_prefix addr current in
     202                        let set = if cond then IntListSet.empty else IntListSet.singleton addr in
     203                        (offset, set)   
     204        | Sswitch(_,ls) -> find_multi_entry_loops_ls m current offset ls
     205        | _ -> (offset, IntListSet.empty)
     206
     207and find_multi_entry_loops_ls m current offset = function
     208  | LSdefault s -> find_multi_entry_loops_s m current offset s
     209  | LScase(_,s,ls) ->
     210    let (offset, set1) = find_multi_entry_loops_s m current offset s in
     211    let (offset, set2) = find_multi_entry_loops_ls m current offset ls in
     212    (offset, IntListSet.union set1 set2)
     213                               
     214(* final pass where loops are indexed *)
     215let rec index_loops_s multi_entry current offset depth = function
     216        (* I am supposing you cannot jump to the update statement of for loops... *)
     217        | Swhile(_,b,s) ->
     218    let current' = offset :: current in
     219                let is_bad = IntListSet.mem current' multi_entry in
     220                let i, depth = if is_bad then None, depth else Some depth, depth + 1 in
     221          let (_, s) = index_loops_s multi_entry current' 0 depth s in
     222          (offset + 1, Swhile(i,b,s))
     223        | Sdowhile(_,b,s) ->
     224    let current' = offset :: current in
     225    let is_bad = IntListSet.mem current' multi_entry in
     226    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in
     227          let (_, s) = index_loops_s multi_entry current' 0 depth s in
     228          (offset + 1, Sdowhile(i,b,s))
     229        | Sfor(_,a1,a2,a3,s) ->
     230    let current' = offset :: current in
     231    let is_bad = IntListSet.mem current' multi_entry in
     232    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in
     233          let (_, s) = index_loops_s multi_entry current' 0 depth s in
     234          (offset + 1, Sfor(i,a1,a2,a3,s))
     235        | Ssequence(s1,s2) ->
     236          let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
     237          let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
     238          (offset, Ssequence(s1,s2))
     239        | Sifthenelse(b,s1,s2) ->
     240          let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
     241          let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
     242          (offset, Sifthenelse(b,s1,s2))
     243        | Slabel(l,s) ->
     244                let (offset, s) = index_loops_s multi_entry current offset depth s in
     245                (offset, Slabel(l, s))
     246        | Sswitch(v,ls) ->
     247    let (offset, s) = index_loops_ls multi_entry current offset depth ls in
     248                (offset, Sswitch(v, ls))
     249        | _ as s -> (offset, s)
     250
     251and index_loops_ls multi_entry current offset depth = function
     252  | LSdefault s ->
     253                let (offset, s) =       index_loops_s multi_entry current offset depth s in
     254                (offset, LSdefault s)
     255  | LScase(v,s,ls) ->
     256    let (offset, s) = index_loops_s multi_entry current offset depth s in
     257    let (offset, ls) = index_loops_ls multi_entry current offset depth ls in
     258                (offset, LScase(v,s,ls))
     259
     260(* Index loops and introduce cost labels in functions *)
     261let process_f cost_universe = function
     262  | (id,Internal fd) ->
     263    let body = fd.fn_body in
     264    (* assign loop addresses to labels *)
     265    let (_, m) = assign_loop_addrs_s [] 0 Label.Map.empty body in
     266    (* find which loops are potentially multi-entry *)
     267    let (_, multi_entry) = find_multi_entry_loops_s m [] 0 body in
     268    (* index loops accordingly *)
     269    let (_, body) = index_loops_s multi_entry [] 0 0 body in
     270                (* initialize indexing *)
     271                let ind = CostLabel.empty_indexing in
     272                (* add cost labels inside *)
     273                let body = add_cost_labels_st ind cost_universe body in
     274                (* add cost label in front *)
     275                let body = add_starting_cost_label ind cost_universe body in
     276                (id,Internal {fd with fn_body = body})
     277  | _ as x -> x
     278       
     279         
    161280
    162281(** [add_cost_labels prog] inserts some labels to enable
     
    170289  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
    171290  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
    172         let ind = CostLabel.empty_indexing in
    173   {
    174     prog_funct = List.map (add_cost_labels_f ind cost_universe) p.prog_funct;
    175     prog_main = p.prog_main;
    176     prog_vars = p.prog_vars
    177   }
     291  {p with prog_funct = List.map (process_f cost_universe) p.prog_funct}
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightPrinter.ml

    r1305 r1328  
    217217      print_expr_list p (false, et)
    218218
     219let print_loop_depth p = function
     220        | None -> fprintf p ""
     221        | Some x -> fprintf p "/* single entry loop depth: %d */@," x
     222
    219223let rec print_stmt p s =
    220         let print_loop_depth = function
    221     | None -> ()
    222     | Some x -> fprintf p "/* single entry loop depth: %d */@" x in
    223224  match s with
    224225  | Sskip ->
     
    247248              print_stmt s2
    248249  | Swhile(i, e, s) ->
    249                   print_loop_depth i;
    250       fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
     250      fprintf p "@[<v 2>%a@ while (%a) {@ %a@;<0 -2>}@]"
     251                                print_loop_depth i
    251252              print_expr e
    252253              print_stmt s
    253254  | Sdowhile(i, e, s) ->
    254       print_loop_depth i;
    255       fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]"
     255      fprintf p "@[<v 2>%a@ do {@ %a@;<0 -2>} while(%a);@]"
     256                                print_loop_depth i
    256257              print_stmt s
    257258              print_expr e
    258259  | Sfor(i, s_init, e, s_iter, s_body) ->
    259       print_loop_depth i;
    260       fprintf p "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]"
     260      fprintf p "@[<v 0>%a@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]@]"
     261                                print_loop_depth i
    261262              print_stmt_for s_init
    262263              print_expr e
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightUtils.ml

    r1319 r1328  
    8080        match stmt with
    8181          | Clight.Swhile (Some x, _, _) | Clight.Sdowhile (Some x, _, _)
    82           | Clight.Sfor (Some x, _, _, _, _) -> max x curr_max (* = curr_max+1 ? *)
    83             | _ -> curr_max in
     82          | Clight.Sfor (Some x, _, _, _, _) -> max (x+1) curr_max
     83          | _ -> curr_max in
    8484  ClightFold.statement2 f_expr f_stmt
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml

    r1319 r1328  
    2727let rec enter_loop n indexing = match n with
    2828        | None -> ()
    29         | Some x -> indexing.(x) <- 0
     29        | Some x -> try indexing.(x) <- 0 with | _ -> assert false
    3030
    3131(** [enter_loop n indexing] is used to update indexing when one is continuing a
     
    3333let rec continue_loop n indexing = match n with
    3434        | None -> ()
    35         | Some x -> indexing.(x) <- indexing.(x) + 1
     35        | Some x -> try indexing.(x) <- indexing.(x) + 1 with | _ -> assert false
    3636
    3737let sexpr_of i l =
     
    6868        | [] -> []
    6969        | s :: l ->
    70                 const_sexpr (ev_sexpr c.(i) s) :: compose_const_indexing_i (i+1) c l
     70                try
     71                  const_sexpr (ev_sexpr c.(i) s) :: compose_const_indexing_i (i+1) c l
     72                with
     73                        | Invalid_argument _ -> assert false
    7174
    7275module IndexingSet = Set.Make(struct
  • Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml

    r740 r1328  
    4040let interpretation_requested () = !interpretation_flag
    4141
     42let trace_flag         = ref false
     43let request_trace = (:=) trace_flag
     44let trace_requested () = !trace_flag
     45
    4246let debug_flag                  = ref false
    4347let set_debug                   = (:=) debug_flag
     
    7175  " Interpret the compiled code.";
    7276
     77  "-t", Arg.Set trace_flag,
     78  " Interpret the compiled code and print all label traces.";
     79
    7380  "-d", Arg.Set debug_flag,
    7481  " Debugging mode.";
  • Deliverables/D2.2/8051-indexed-labels-branch/src/options.mli

    r740 r1328  
    1212val request_interpretation   : bool -> unit
    1313val interpretation_requested : unit -> bool
     14
     15(** {2 Trace requests} *)
     16val request_trace   : bool -> unit
     17val trace_requested : unit -> bool
    1418
    1519(** {2 Annotation requests} *)
Note: See TracChangeset for help on using the changeset viewer.