Changeset 1542 for Deliverables/D2.2


Ignore:
Timestamp:
Nov 23, 2011, 5:43:24 PM (8 years ago)
Author:
tranquil
Message:

merge of indexed labels branch

Location:
Deliverables/D2.2/8051/src
Files:
56 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/ASM/ASM.mli

    r1462 r1542  
    102102type labelled_instruction =
    103103 [ instruction
    104  | `Cost of string
     104 | `Cost of CostLabel.t
     105 | `Index of int
     106 | `Inc of int
    105107 | `Label of string
    106108 | `Jmp of string
     
    122124type program =
    123125    { code        : BitVectors.byte list ;
    124       cost_labels : string BitVectors.WordMap.t ;
     126      inds        : int BitVectors.WordMap.t ; (* loop index resets *)
     127      incs        : int BitVectors.WordMap.t ; (* loop index increments *)
     128      cost_labels : CostLabel.t BitVectors.WordMap.t ;
    125129      labels      : BitVectors.word StringTools.Map.t ;
     130
    126131      exit_addr   : BitVectors.word ;
    127132      has_main    : bool }
  • Deliverables/D2.2/8051/src/ASM/ASMCosts.ml

    r643 r1542  
    5050    warning
    5151      (Printf.sprintf
    52          "Warning: branching to %s has cost %d, branching to %s has cost %d"
    53          (string_of_int (BitVectors.int_of_vect pc1)) cost1
    54          (string_of_int (BitVectors.int_of_vect pc2)) cost2) ;
     52         "Warning: branching to %X has cost %d, branching to %X has cost %d"
     53         (BitVectors.int_of_vect pc1) cost1
     54         (BitVectors.int_of_vect pc2) cost2) ;
    5555    max cost1 (compare ((pc2, cost2) :: l))
    5656  | _ :: l -> compare l
  • Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml

    r1490 r1542  
    131131
    132132  exit_addr   : BitVectors.word;
    133   cost_labels : string BitVectors.WordMap.t
     133       
     134(*
     135  ind_0s      : int BitVectors.WordMap.t;
     136  ind_incs    : int BitVectors.WordMap.t;
     137  cost_labels : CostLabel.t BitVectors.WordMap.t
     138*)     
    134139}
    135140
     
    284289
    285290  exit_addr = BitVectors.zero `Sixteen;
     291(*
     292  ind_0s = BitVectors.WordMap.empty;
     293  ind_incs = BitVectors.WordMap.empty;
    286294  cost_labels = BitVectors.WordMap.empty
     295*)
    287296}
    288297
     
    950959   ) (StringTools.Map.empty,0) p.ASM.ppreamble
    951960 in
    952  let pc,exit_addr,labels,costs =
     961 let pc,exit_addr,labels,inds,incs,costs =
    953962  List.fold_left
    954    (fun (pc,exit_addr,labels,costs) i ->
     963   (fun (pc,exit_addr,labels,inds,incs,costs) i ->
    955964     match i with
    956         `Label s when s = p.ASM.pexit_label -> pc, pc, StringTools.Map.add s pc labels, costs
    957       | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, costs
    958       | `Cost s -> pc, exit_addr, labels, BitVectors.WordMap.add pc s costs
    959       | `Mov (_,_) -> (snd (half_add pc (vect_of_int 3 `Sixteen))), exit_addr, labels, costs
     965        `Label s when s = p.ASM.pexit_label -> pc, pc, StringTools.Map.add s pc labels, inds, incs, costs
     966      | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, inds, incs, costs
     967      | `Cost s -> pc, exit_addr, labels, inds, incs, BitVectors.WordMap.add pc s costs
     968      | `Index i -> pc, exit_addr, labels, BitVectors.WordMap.add pc i inds, incs, costs
     969      | `Inc i -> pc, exit_addr, labels, inds, BitVectors.WordMap.add pc i incs, costs
     970      | `Mov (_,_) -> (snd (half_add pc (vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs
     971
    960972      | `Jmp _
    961       | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, costs
     973      | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs
    962974      (*CSC: very stupid: always expand to worst opcode *)
    963975      | `WithLabel i ->
     
    967979        assert (fake_jump = i');
    968980        let pc' = snd (half_add pc' (vect_of_int 5 `Sixteen)) in
    969           (snd (half_add pc pc'), exit_addr, labels, costs)
     981          (snd (half_add pc pc'), exit_addr, labels, inds, incs, costs)
    970982      | #instruction as i ->
    971983        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
    972984         assert (i = i');
    973          (snd (half_add pc pc'),exit_addr,labels, costs)
     985         (snd (half_add pc pc'),exit_addr,labels, inds, incs, costs)
    974986   )
    975987    (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen,
    976      StringTools.Map.empty, BitVectors.WordMap.empty) p.ASM.pcode
     988     StringTools.Map.empty, BitVectors.WordMap.empty, BitVectors.WordMap.empty,
     989     BitVectors.WordMap.empty) p.ASM.pcode
    977990 in
    978991 let code =
     
    980993     (function
    981994        `Label _
    982       | `Cost _ -> []
     995      | `Cost _
     996      | `Index _
     997      | `Inc _ -> []
    983998      | `WithLabel i ->
    984999         (* We need to expand a conditional jump to a label to a machine language
     
    10321047                 address, reconstructed
    10331048         in
    1034            let sjmp, jmp = `SJMP (`REL (vect_of_int 3 `Eight)), `LJMP (`ADDR16 jmp_address) in
     1049           let sjmp = `SJMP (`REL (vect_of_int 3 `Eight)) in
     1050           let jmp = `LJMP (`ADDR16 jmp_address) in
    10351051           let translation = [ translated_jump; sjmp; jmp ] in
    10361052             List.flatten (List.map assembly1 translation)
     
    10481064            assembly1 (`LCALL (`ADDR16 pc_offset ))
    10491065      | #instruction as i -> assembly1 i) p.ASM.pcode) in
    1050  { ASM.code = code ; ASM.cost_labels = costs ;
     1066 { ASM.code = code ;
     1067   ASM.inds = inds; ASM.incs = incs; ASM.cost_labels = costs ;
    10511068   ASM.labels = StringTools.Map.empty ;
    10521069   ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main }
     
    19751992let load_program p =
    19761993  let st = load p.ASM.code initialize in
    1977   { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels }
    1978 
    1979 let observe_trace trace_ref st =
    1980   let cost_label =
    1981     if BitVectors.WordMap.mem st.pc st.cost_labels then
    1982       [BitVectors.WordMap.find st.pc st.cost_labels]
    1983     else [] in
    1984   trace_ref := cost_label @ !trace_ref ;
     1994  { st with exit_addr = p.ASM.exit_addr (* ; cost_labels = p.ASM.cost_labels *)}
     1995
     1996type cost_trace = {
     1997  mutable ct_labels : CostLabel.t list;
     1998  mutable ct_inds   : CostLabel.const_indexing list;
     1999}
     2000
     2001(* FIXME: supposing only one index reset or increment per instruction *)
     2002let update_indexes trace p st =
     2003  try
     2004    let i = BitVectors.WordMap.find st.pc p.ASM.inds in
     2005    CostLabel.enter_loop trace.ct_inds i
     2006  with Not_found -> ();
     2007    try
     2008      let i = BitVectors.WordMap.find st.pc p.ASM.incs in
     2009      CostLabel.continue_loop trace.ct_inds i
     2010    with Not_found -> ();
     2011      let instr,_,_ = fetch st.code_memory st.pc in
     2012      match instr with
     2013        | `ACALL _ | `LCALL _ ->
     2014          trace.ct_inds <- CostLabel.new_const_ind trace.ct_inds
     2015        | `RET ->
     2016          trace.ct_inds <- CostLabel.forget_const_ind trace.ct_inds
     2017        | _ -> ()
     2018
     2019let update_labels trace p st =
     2020  try
     2021    let cost_label = BitVectors.WordMap.find st.pc p.cost_labels in
     2022    let ind = CostLabel.curr_const_ind trace.ct_inds in
     2023    let cost_label = CostLabel.ev_indexing ind cost_label in
     2024    trace.ct_labels <- cost_label :: trace.ct_labels
     2025  with Not_found -> ()
     2026
     2027
     2028
     2029let update_trace trace p st =
     2030  update_labels trace p st;
     2031  update_indexes trace p st;
    19852032  if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st
    19862033
     
    20002047  if p.ASM.has_main then
    20012048    let st = load_program p in
    2002     let trace = ref [] in
    2003     let callback = observe_trace trace in
     2049    let trace = {ct_labels = []; ct_inds = []} in
     2050    let callback = update_trace trace p in
    20042051    let st = execute callback st in
    20052052    let res = result st in
    20062053    if debug then
    20072054      Printf.printf "Result = %s\n%!" (IntValue.Int32.to_string res) ;
    2008     (res, List.rev !trace)
     2055    (res, List.rev trace.ct_labels)
    20092056  else (IntValue.Int32.zero, [])
    20102057
  • Deliverables/D2.2/8051/src/ASM/ASMInterpret.mli

    r1488 r1542  
    9898
    9999      exit_addr   : BitVectors.word;
    100       cost_labels : string BitVectors.WordMap.t
     100(*
     101      ind_0s      : int BitVectors.WordMap.t;
     102      ind_incs    : int BitVectors.WordMap.t;
     103      cost_labels : CostLabel.t BitVectors.WordMap.t
     104*)
    101105    }
    102106     
  • Deliverables/D2.2/8051/src/ASM/Pretty.ml

    r818 r1542  
    4343 function
    4444    `Label l -> l ^ ":"
    45   | `Cost l -> l ^ ":"
     45  | `Cost l -> CostLabel.string_of_cost_label ~pretty:true l ^ ":"
     46  | `Index i -> "index " ^ string_of_int i ^ ":"
     47  | `Inc i -> "increment " ^ string_of_int i ^ ":"
    4648  | `Jmp j -> "ljmp  " ^ j
    4749  | `Call j -> "lcall " ^ j
     
    9698  | `XRL(`U2(a1,a2)) -> "xrl   " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    9799
     100let find_comment p pc =
     101  let s1 =
     102    try
     103      let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in
     104      ", " ^ CostLabel.string_of_cost_label ~pretty:true lbl
     105    with Not_found -> "" in
     106  let s2 =
     107    try
     108      let i = BitVectors.WordMap.find pc p.ASM.inds in
     109      ", index " ^ string_of_int i
     110    with Not_found -> "" in
     111  let s3 =
     112    try
     113      let i = BitVectors.WordMap.find pc p.ASM.incs in
     114      ", inc " ^ string_of_int i
     115    with Not_found -> "" in
     116  s1 ^ s2 ^ s3
     117                       
     118
    98119let print_program p =
    99120  let mem = ASMInterpret.load_code_memory p.ASM.code in
    100121  let f (s, pc) _ =
    101122    let (inst, new_pc, cost) = ASMInterpret.fetch mem pc in
    102     (Printf.sprintf "%s% 6X:  %- 18s ;; %d  %s\n"
     123    (Printf.sprintf "%s% 6X:  %- 18s ;; %d%s\n"
    103124       s
    104125       (BitVectors.int_of_vect pc)
    105126       (pp_instruction inst)
    106127       cost
    107        (if BitVectors.WordMap.mem pc p.ASM.cost_labels then
    108            (BitVectors.WordMap.find pc p.ASM.cost_labels)
    109         else ""),
     128       (find_comment p pc),
    110129     new_pc) in
    111130  fst (List.fold_left f ("", BitVectors.zero `Sixteen) p.ASM.code)
  • Deliverables/D2.2/8051/src/ERTL/ERTL.mli

    r1462 r1542  
    4848  (* Emit a cost label. *)
    4949  | St_cost of CostLabel.t * Label.t
     50
     51  (* Reset to 0 a loop index *)
     52  | St_ind_0 of CostLabel.index * Label.t
     53
     54  (* Increment a loop index *)
     55  | St_ind_inc of CostLabel.index * Label.t
    5056
    5157  (* Assign the content of a hardware register to a pseudo register. Parameters
  • Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml

    r1462 r1542  
    3232
    3333type stack_frame = local_env
     34
     35type indexing = CostLabel.const_indexing
    3436
    3537(* Execution states. *)
     
    4446      renv   : hdw_reg_env ;
    4547      mem    : memory ;
     48      inds   : indexing list;
    4649      trace  : CostLabel.t list }
    4750
     
    6265let change_trace st trace = { st with trace = trace }
    6366let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
     67let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
     68let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
     69let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
     70let enter_loop st = CostLabel.enter_loop st.inds
     71let continue_loop st = CostLabel.continue_loop st.inds
    6472
    6573let empty_state =
     
    7280    renv   = I8051.RegisterMap.empty ;
    7381    mem    = Mem.empty ;
     82    inds   = [] ;
    7483    trace  = [] }
    7584
     
    118127  let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in
    119128  let pc = entry_pc lbls_offs ptr def in
     129  let st = new_ind st in
    120130  change_lenv (change_pc st pc) lenv
    121131
     
    231241
    232242let interpret_return lbls_offs st =
     243  let st = forget_ind st in
    233244  let st = pop_st_frs st in
    234245  let (st, pch) = pop st in
     
    254265
    255266    | ERTL.St_cost (cost_lbl, lbl) ->
     267      let cost_lbl = ev_label st cost_lbl in
    256268      let st = add_trace st cost_lbl in
     269      next_pc st lbl
     270
     271    | ERTL.St_ind_0 (i, lbl) ->
     272      enter_loop st i;
     273      next_pc st lbl
     274
     275    | ERTL.St_ind_inc (i, lbl) ->
     276      continue_loop st i;
    257277      next_pc st lbl
    258278
  • Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml

    r1462 r1542  
    4343    Printf.sprintf "*** %s *** --> %s" s lbl
    4444  | ERTL.St_cost (cost_lbl, lbl) ->
     45    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    4546    Printf.sprintf "emit %s --> %s" cost_lbl lbl
     47  | ERTL.St_ind_0 (i, lbl) ->
     48    Printf.sprintf "index %d --> %s" i lbl
     49  | ERTL.St_ind_inc (i, lbl) ->
     50    Printf.sprintf "increment %d --> %s" i lbl
    4651  | ERTL.St_get_hdw (r1, r2, lbl) ->
    4752    Printf.sprintf "move %s, %s --> %s"
  • Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

    r1488 r1542  
    163163
    164164      | ERTL.St_cost (cost_lbl, l) ->
    165         LTL.St_cost (cost_lbl, l)
     165        LTL.St_cost (cost_lbl, l)
     166
     167      | ERTL.St_ind_0 (i, l) ->
     168        LTL.St_ind_0 (i, l)
     169
     170      | ERTL.St_ind_inc (i, l) ->
     171        LTL.St_ind_inc (i, l)
    166172
    167173      | ERTL.St_get_hdw (destr, sourcehwr, l) ->
  • Deliverables/D2.2/8051/src/ERTL/liveness.ml

    r1462 r1542  
    1818  | St_comment (_, l)
    1919  | St_cost (_, l)
     20  | St_ind_0 (_, l)
     21  | St_ind_inc (_, l)
    2022  | St_set_hdw (_, _, l)
    2123  | St_get_hdw (_, _, l)
     
    8385end
    8486
    85 module Label_ImperativeMap = struct
    86 
    87   type key =
    88       Label.Map.key
    89  
    90   type 'data t =
    91       'data Label.Map.t ref
    92      
    93   let create () =
    94     ref Label.Map.empty
    95 
    96   let clear t =
    97     t := Label.Map.empty
    98    
    99   let add k d t =
    100     t := Label.Map.add k d !t
    101 
    102   let find k t =
    103     Label.Map.find k !t
    104 
    105   let iter f t =
    106     Label.Map.iter f !t
    107 
    108 end
    109 
    110 module F = Fix.Make (Label_ImperativeMap) (L)
     87module F = Fix.Make (Label.ImpMap) (L)
    11188
    11289(* These are the sets of variables defined at (written by) a statement. *)
     
    11794  | St_comment _
    11895  | St_cost _
     96  | St_ind_0 _
     97  | St_ind_inc _
    11998  | St_push _
    12099  | St_store _
     
    169148  | St_comment _
    170149  | St_cost _
     150  | St_ind_0 _
     151  | St_ind_inc _
    171152  | St_framesize _
    172153  | St_pop _
     
    227208  | St_comment _
    228209  | St_cost _
     210  | St_ind_0 _
     211  | St_ind_inc _
    229212  | St_newframe _
    230213  | St_delframe _
  • Deliverables/D2.2/8051/src/ERTL/uses.ml

    r1462 r1542  
    2020  | St_comment _
    2121  | St_cost _
     22  | St_ind_0 _
     23  | St_ind_inc _
    2224  | St_hdw_to_hdw _
    2325  | St_newframe _
  • Deliverables/D2.2/8051/src/LIN/LIN.mli

    r1488 r1542  
    1818  (* Emit a cost label. *)
    1919  | St_cost of CostLabel.t
     20
     21  (* Reset to 0 a loop index *)
     22  | St_ind_0 of CostLabel.index
     23
     24  (* Increment a loop index *)
     25  | St_ind_inc of CostLabel.index
    2026
    2127  (* Assign an integer constant to a register. Parameters are the destination
  • Deliverables/D2.2/8051/src/LIN/LINInterpret.ml

    r1488 r1542  
    2121
    2222type hdw_reg_env = Val.t I8051.RegisterMap.t
     23
     24
     25type indexing = CostLabel.const_indexing
    2326
    2427(* Execution states. *)
     
    3134      renv   : hdw_reg_env ;
    3235      mem    : memory ;
     36      inds   : indexing list ;
    3337      trace  : CostLabel.t list }
    3438
     
    4448let change_trace st trace = { st with trace = trace }
    4549let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
     50let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
     51let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
     52let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
     53let enter_loop st = CostLabel.enter_loop st.inds
     54let continue_loop st = CostLabel.continue_loop st.inds
    4655
    4756let empty_state =
     
    5261    renv   = I8051.RegisterMap.empty ;
    5362    mem    = Mem.empty ;
     63    inds   = [] ;
    5464    trace  = [] }
    5565
     
    7282
    7383let init_fun_call st ptr =
     84  let st = new_ind st in
    7485  change_pc st (Val.change_address_offset ptr Val.Offset.zero)
    7586
     
    176187
    177188let interpret_return st =
     189  let st = forget_ind st in
    178190  let (st, pc) = return_pc st in
    179191  change_pc st pc
     
    195207
    196208    | LIN.St_cost cost_lbl ->
     209      let cost_lbl = ev_label st cost_lbl in
    197210      let st = add_trace st cost_lbl in
     211      next_pc st
     212
     213    | LIN.St_ind_0 i ->
     214      enter_loop st i;
     215      next_pc st
     216
     217    | LIN.St_ind_inc i ->
     218      continue_loop st i;
    198219      next_pc st
    199220
  • Deliverables/D2.2/8051/src/LIN/LINPrinter.ml

    r1488 r1542  
    2626    Printf.sprintf "*** %s ***" s
    2727  | LIN.St_cost cost_lbl ->
     28    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    2829    Printf.sprintf "emit %s" cost_lbl
     30  | LIN.St_ind_0 i ->
     31    Printf.sprintf "index %d" i
     32  | LIN.St_ind_inc i ->
     33    Printf.sprintf "increment %d" i
    2934  | LIN.St_int (dstr, i) ->
    3035    Printf.sprintf "imm %s, %d" (print_reg dstr) i
  • Deliverables/D2.2/8051/src/LIN/LINToASM.ml

    r1525 r1542  
    2525  | LIN.St_goto lbl
    2626  | LIN.St_label lbl
    27   | LIN.St_cost lbl
    2827  | LIN.St_condacc lbl -> Label.Set.singleton lbl
     28    (* taking the atom as a fresh prefix will be generated *)
     29  | LIN.St_cost lbl -> Label.Set.singleton (lbl.CostLabel.name)
    2930  | _ -> Label.Set.empty
    3031
     
    6970    (* TODO: hack! Need to make the difference between cost labels and regular
    7071       labels. *)
    71     [`Cost lbl ; `NOP]
     72    [`Cost lbl ; `NOP ]
     73  | LIN.St_ind_0 i -> [`Index i ; `NOP (* TODO: hack! *)]
     74  | LIN.St_ind_inc i -> [`Inc i ; `NOP (* TODO: hack! *)]
    7275  | LIN.St_int (r, i) ->
    7376    [`MOV (`U3 (I8051.reg_addr r, data_of_int i))]
  • Deliverables/D2.2/8051/src/LTL/LTL.mli

    r1488 r1542  
    1818  (* Emit a cost label. *)
    1919  | St_cost of CostLabel.t * Label.t
     20
     21  (* Reset to 0 a loop index *)
     22  | St_ind_0 of CostLabel.index * Label.t
     23
     24  (* Increment a loop index *)
     25  | St_ind_inc of CostLabel.index * Label.t
    2026
    2127  (* Assign an integer constant to a register. Parameters are the destination
  • Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

    r1488 r1542  
    3131      renv   : hdw_reg_env ;
    3232      mem    : memory ;
     33      inds   : CostLabel.const_indexing list ;
    3334      trace  : CostLabel.t list }
    3435
     
    4445let change_trace st trace = { st with trace = trace }
    4546let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
     47let ev_label st = CostLabel.ev_indexing (CostLabel.curr_const_ind st.inds)
     48let new_ind st = { st with inds = CostLabel.new_const_ind st.inds }
     49let forget_ind st = { st with inds = CostLabel.forget_const_ind st.inds }
     50let enter_loop st = CostLabel.enter_loop st.inds
     51let continue_loop st = CostLabel.continue_loop st.inds
    4652
    4753let empty_state =
     
    5258    renv   = I8051.RegisterMap.empty ;
    5359    mem    = Mem.empty ;
     60    inds   = [] ;
    5461    trace  = [] }
    5562
     
    95102let init_fun_call lbls_offs st ptr def =
    96103  let pc = entry_pc lbls_offs ptr def in
     104  let st = new_ind st in
    97105  change_pc st pc
    98106
     
    207215
    208216let interpret_return lbls_offs st =
     217  let st = forget_ind st in
    209218  let (st, pc) = return_pc st in
    210219  change_pc st pc
     
    227236
    228237    | LTL.St_cost (cost_lbl, lbl) ->
     238      let cost_lbl = ev_label st cost_lbl in
    229239      let st = add_trace st cost_lbl in
     240      next_pc st lbl
     241
     242    | LTL.St_ind_0 (i, lbl) ->
     243      enter_loop st i;
     244      next_pc st lbl
     245
     246    | LTL.St_ind_inc (i, lbl) ->
     247      continue_loop st i;
    230248      next_pc st lbl
    231249
  • Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml

    r1488 r1542  
    2525    Printf.sprintf "*** %s *** --> %s" s lbl
    2626  | LTL.St_cost (cost_lbl, lbl) ->
     27    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    2728    Printf.sprintf "emit %s --> %s" cost_lbl lbl
     29  | LTL.St_ind_0 (i, lbl) ->
     30    Printf.sprintf "index %d --> %s" i lbl
     31  | LTL.St_ind_inc (i, lbl) ->
     32    Printf.sprintf "increment %d --> %s" i lbl
    2833  | LTL.St_int (dstr, i, lbl) ->
    2934    Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl
  • Deliverables/D2.2/8051/src/LTL/LTLToLIN.ml

    r1488 r1542  
    2222  | LTL.St_cost (lbl, _) ->
    2323    LIN.St_cost lbl
     24  | LTL.St_ind_0 (i, _) ->
     25    LIN.St_ind_0 i
     26  | LTL.St_ind_inc (i, _) ->
     27    LIN.St_ind_inc i
    2428  | LTL.St_int (r, i, _) ->
    2529    LIN.St_int (r, i)
  • Deliverables/D2.2/8051/src/LTL/LTLToLINI.ml

    r1488 r1542  
    117117        | LTL.St_comment (_, l)
    118118        | LTL.St_cost (_, l)
     119        | LTL.St_ind_0 (_, l)
     120        | LTL.St_ind_inc (_, l)
    119121        | LTL.St_int (_, _, l)
    120122        | LTL.St_pop l
  • Deliverables/D2.2/8051/src/LTL/branch.ml

    r1488 r1542  
    5252    | LTL.St_cost (lbl, l) ->
    5353      LTL.St_cost (lbl, rep l)
     54    | LTL.St_ind_0 (i, l) ->
     55      LTL.St_ind_0 (i, rep l)
     56    | LTL.St_ind_inc (i, l) ->
     57      LTL.St_ind_inc (i, rep l)
    5458    | LTL.St_int (r, i, l) ->
    5559      LTL.St_int (r, i, rep l)
  • Deliverables/D2.2/8051/src/RTL/RTL.mli

    r818 r1542  
    1616  (* Emit a cost label. *)
    1717  | St_cost of CostLabel.t * Label.t
     18
     19  (* Reset to 0 a loop index *)
     20  | St_ind_0 of CostLabel.index * Label.t
     21
     22  (* Increment a loop index *)
     23  | St_ind_inc of CostLabel.index * Label.t
    1824
    1925  (* Assign the address of a symbol to registers. Parameters are the destination
  • Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

    r818 r1542  
    3434      carry    : Val.t }
    3535
     36type indexing = CostLabel.const_indexing
     37
    3638(* Execution states. There are three possible states :
    3739   - The constructor [State] represents a state when executing a function
     
    4143type state =
    4244  | State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) *
    43              local_env * Val.t (* carry *) * memory * CostLabel.t list
     45             local_env * Val.t (* carry *) * memory * indexing list *
     46                                                 CostLabel.t list
    4447  | CallState of stack_frame list * RTL.function_def *
    45                  Val.t list (* args *) * memory * CostLabel.t list
     48              Val.t list (* args *) * memory * indexing list * CostLabel.t list
    4649  | ReturnState of stack_frame list * Val.t list (* return values *) *
    47                    memory * CostLabel.t list
     50                   memory * indexing list * CostLabel.t list
    4851
    4952let string_of_local_env lenv =
     
    5962
    6063let 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%!"
     64  | State (_, _, lbl, sp, lenv, carry, mem, ind, _) ->
     65    Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
    6366      (Val.string_of_address sp)
    6467      (Val.to_string carry)
    6568      (string_of_local_env lenv)
    66       (Mem.to_string mem)
     69      (Mem.to_string mem);
     70    let i = CostLabel.curr_const_ind ind in
     71    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
     72    Printf.printf "Regular state: %s\n\n%!"
    6773      lbl
    68   | CallState (_, _, args, mem, _) ->
     74  | CallState (_, _, args, mem, _, _) ->
    6975    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
    7076      (Mem.to_string mem)
    7177      (string_of_args args)
    72   | ReturnState (_, vs, mem, _) ->
     78  | ReturnState (_, vs, mem, _, _) ->
    7379    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    7480      (Mem.to_string mem)
     
    96102(* Assign a value to some destinations registers. *)
    97103
    98 let assign_state sfrs graph lbl sp lenv carry mem trace destrs vs =
     104let assign_state sfrs graph lbl sp lenv carry mem inds trace destrs vs =
    99105  let lenv = adds destrs vs lenv in
    100   State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
     106  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    101107
    102108(* Branch on a value. *)
    103109
    104 let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v =
     110let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v =
    105111  let next_lbl =
    106112    if Val.is_true v then lbl_true
     
    108114      if Val.is_false v then lbl_false
    109115      else error "Undefined conditional value." in
    110   State (sfrs, graph, next_lbl, sp, lenv, carry, mem, trace)
     116  State (sfrs, graph, next_lbl, sp, lenv, carry, mem, inds, trace)
     117
     118let curr_ind = CostLabel.curr_const_ind
     119
     120let forget_ind = CostLabel.forget_const_ind
     121
     122let new_ind = CostLabel.new_const_ind
    111123
    112124
     
    120132    (carry : Val.t)
    121133    (mem   : memory)
     134    (inds  : indexing list)
    122135    (stmt  : RTL.statement)
    123136    (trace : CostLabel.t list) :
     
    125138
    126139      | RTL.St_skip lbl ->
    127         State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
     140        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    128141
    129142      | RTL.St_cost (cost_lbl, lbl) ->
    130         State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace)
     143        let cost_lbl = CostLabel.ev_indexing (curr_ind inds) cost_lbl in
     144        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, cost_lbl :: trace)
     145
     146      | RTL.St_ind_0 (i, lbl) ->
     147        CostLabel.enter_loop inds i;
     148        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
     149
     150      | RTL.St_ind_inc (i, lbl) ->
     151        CostLabel.continue_loop inds i;
     152        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    131153
    132154      | RTL.St_addr (r1, r2, x, lbl) ->
    133         assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2]
     155        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2]
    134156          (Mem.find_global mem x)
    135157
    136158      | RTL.St_stackaddr (r1, r2, lbl) ->
    137         assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp
     159        assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp
    138160
    139161      | RTL.St_int (r, i, lbl) ->
    140         assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i]
     162        assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i]
    141163
    142164      | RTL.St_move (destr, srcr, lbl) ->
    143         assign_state sfrs graph lbl sp lenv carry mem trace [destr]
     165        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr]
    144166          [get_local_value lenv srcr]
    145167
     
    149171            (get_local_value lenv srcr1)
    150172            (get_local_value lenv srcr2) in
    151         assign_state sfrs graph lbl sp lenv carry mem trace
     173        assign_state sfrs graph lbl sp lenv carry mem inds trace
    152174          [destr1 ; destr2] [v1 ; v2]
    153175
    154176      | RTL.St_op1 (op1, destr, srcr, lbl) ->
    155177        let v = Eval.op1 op1 (get_local_value lenv srcr) in
    156         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
     178        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
    157179
    158180      | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
     
    161183            (get_local_value lenv srcr1)
    162184            (get_local_value lenv srcr2) in
    163         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
     185        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
    164186
    165187      | RTL.St_clear_carry lbl ->
    166         State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)
     188        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, inds, trace)
    167189
    168190      | RTL.St_set_carry lbl ->
    169         State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, trace)
     191        State (sfrs, graph, lbl, sp, lenv, Val.of_int 1, mem, inds, trace)
    170192
    171193      | RTL.St_load (destr, addr1, addr2, lbl) ->
    172194        let addr = get_local_addr lenv addr1 addr2 in
    173195        let v = Mem.load mem chunk addr in
    174         assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
     196        assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
    175197
    176198      | RTL.St_store (addr1, addr2, srcr, lbl) ->
    177199        let addr = get_local_addr lenv addr1 addr2 in
    178200        let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
    179         State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
     201        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    180202
    181203      | RTL.St_call_id (f, args, ret_regs, lbl) ->
     
    186208            sp = sp ; lenv = lenv ; carry = carry }
    187209        in
    188         CallState (sf :: sfrs, f_def, args, mem, trace)
     210        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    189211
    190212      | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
     
    194216        let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
    195217                   sp = sp ; lenv = lenv ; carry = carry } in
    196         CallState (sf :: sfrs, f_def, args, mem, trace)
     218        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    197219
    198220      | RTL.St_tailcall_id (f, args) ->
     
    200222        let args = get_arg_values lenv args in
    201223        let mem = Mem.free mem sp in
    202         CallState (sfrs, f_def, args, mem, trace)
     224        CallState (sfrs, f_def, args, mem, inds, trace)
    203225
    204226      | RTL.St_tailcall_ptr (f1, f2, args) ->
     
    207229        let args = get_arg_values lenv args in
    208230        let mem = Mem.free mem sp in
    209         CallState (sfrs, f_def, args, mem, trace)
     231        CallState (sfrs, f_def, args, mem, inds, trace)
    210232
    211233      | RTL.St_cond (srcr, lbl_true, lbl_false) ->
    212234        let v = get_local_value lenv srcr in
    213         branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v
     235        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem inds trace v
    214236
    215237      | RTL.St_return rl ->
    216238        let vl = List.map (get_local_value lenv) rl in
    217239        let mem = Mem.free mem sp in
    218         ReturnState (sfrs, vl, mem, trace)
     240        ReturnState (sfrs, vl, mem, inds, trace)
    219241
    220242
     
    240262    (args  : Val.t list)
    241263    (mem   : memory)
     264    (inds  : indexing list)
    242265    (trace : CostLabel.t list) :
    243266    state =
    244267  match f_def with
    245268    | RTL.F_int def ->
     269      let inds = new_ind inds in
    246270      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
    247271      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
    248272             init_locals def.RTL.f_locals def.RTL.f_params args,
    249              Val.undef, mem', trace)
     273             Val.undef, mem', inds, trace)
    250274    | RTL.F_ext def ->
    251275      let (mem', vs) = interpret_external mem def.AST.ef_tag args in
    252       ReturnState (sfrs, vs, mem', trace)
     276      ReturnState (sfrs, vs, mem', inds, trace)
    253277
    254278let state_after_return
     
    257281    (ret_vals : Val.t list)
    258282    (mem      : memory)
     283    (inds     : indexing list)
    259284    (trace    : CostLabel.t list) :
    260285    state =
    261286  let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
    262287  let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
    263   State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace)
     288  let inds = forget_ind inds in
     289  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace)
    264290
    265291
    266292let small_step (st : state) : state = match st with
    267   | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) ->
     293  | State (sfrs, graph, pc, sp, lenv, carry, mem, inds, trace) ->
    268294    let stmt = Label.Map.find pc graph in
    269     interpret_statement sfrs graph sp lenv carry mem stmt trace
    270   | CallState (sfrs, f_def, args, mem, trace) ->
    271     state_after_call sfrs f_def args mem trace
    272   | ReturnState ([], ret_vals, mem, trace) ->
     295    interpret_statement sfrs graph sp lenv carry mem inds stmt trace
     296  | CallState (sfrs, f_def, args, mem, inds, trace) ->
     297    state_after_call sfrs f_def args mem inds trace
     298  | ReturnState ([], ret_vals, mem, inds, trace) ->
    273299    assert false (* End of execution; handled in iter_small_step. *)
    274   | ReturnState (sf :: sfrs, ret_vals, mem, trace) ->
    275     state_after_return sf sfrs ret_vals mem trace
     300  | ReturnState (sf :: sfrs, ret_vals, mem, inds, trace) ->
     301    state_after_return sf sfrs ret_vals mem inds trace
    276302
    277303
     
    292318  if debug then print_state st ;
    293319  match small_step st with
    294     | ReturnState ([], vs, mem, trace) ->
     320    | ReturnState ([], vs, mem, _, trace) ->
    295321      print_and_return_result (compute_result vs, List.rev trace)
    296322    | st' -> iter_small_step debug st'
     
    321347      let mem = init_mem p in
    322348      let main_def = find_function mem main in
    323       let st = CallState ([], main_def, [], mem, []) in
     349      let st = CallState ([], main_def, [], mem, [], []) in
    324350      iter_small_step debug st
  • Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml

    r818 r1542  
    4343  | RTL.St_skip lbl -> "--> " ^ lbl
    4444  | RTL.St_cost (cost_lbl, lbl) ->
     45    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    4546    Printf.sprintf "emit %s --> %s" cost_lbl lbl
     47  | RTL.St_ind_0 (i, lbl) ->
     48    Printf.sprintf "index %d --> %s" i lbl
     49  | RTL.St_ind_inc (i, lbl) ->
     50    Printf.sprintf "increment %d --> %s" i lbl
    4651  | RTL.St_addr (dstr1, dstr2, id, lbl) ->
    4752    Printf.sprintf "imm (%s, %s), %s --> %s"
  • Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

    r1462 r1542  
    2222  | ERTL.St_comment (s, _) -> ERTL.St_comment (s, lbl)
    2323  | ERTL.St_cost (cost_lbl, _) -> ERTL.St_cost (cost_lbl, lbl)
     24  | ERTL.St_ind_0 (i, _) -> ERTL.St_ind_0 (i, lbl)
     25  | ERTL.St_ind_inc (i, _) -> ERTL.St_ind_inc (i, lbl)
    2426  | ERTL.St_get_hdw (r1, r2, _) -> ERTL.St_get_hdw (r1, r2, lbl)
    2527  | ERTL.St_set_hdw (r1, r2, _) -> ERTL.St_set_hdw (r1, r2, lbl)
     
    319321    add_graph lbl (ERTL.St_cost (cost_lbl, lbl')) def
    320322
     323  | RTL.St_ind_0 (i, lbl') ->
     324    add_graph lbl (ERTL.St_ind_0 (i, lbl')) def
     325
     326  | RTL.St_ind_inc (i, lbl') ->
     327    add_graph lbl (ERTL.St_ind_inc (i, lbl')) def
     328
    321329  | RTL.St_addr (r1, r2, x, lbl') ->
    322330    adds_graph
     
    432440      let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in
    433441      (Some cost_label, { def with ERTL.f_graph = graph })
     442    | ERTL.St_ind_0 (_, lbl) | ERTL.St_ind_inc (_, lbl)
    434443    | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl)
    435444    | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)
  • Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli

    r818 r1542  
    1111
    1212
     13type argument =
     14  | Reg of Register.t
     15  | Imm of AST.cst*AST.sig_type
     16
    1317(* A function in RTLabs is a mapping from labels to
    1418   statements. Statements explicitely mention their successors. *)
     
    2226  | St_cost of CostLabel.t * Label.t
    2327
     28  (* Reset to 0 a loop index *)
     29  | St_ind_0 of CostLabel.index * Label.t
     30
     31  (* Increment a loop index *)
     32  | St_ind_inc of CostLabel.index * Label.t
     33
    2434  (* Assign a constant to registers. Parameters are the destination register,
    2535     the constant and the label of the next statement. *)
     
    3242
    3343  (* Application of a binary operation. Parameters are the operation, the
    34      destination register, the two argument registers and the label of the next
     44     destination register, the two arguments and the label of the next
    3545     statement. *)
    36   | St_op2 of AST.op2 * Register.t * Register.t * Register.t * Label.t
     46  | St_op2 of AST.op2 * Register.t * argument * argument * Label.t
    3747
    3848  (* Memory load. Parameters are the size in bytes of what to load, the
    3949     register containing the address, the destination register and the label
    4050     of the next statement. *)
    41   | St_load of AST.quantity * Register.t * Register.t * Label.t
     51  | St_load of AST.quantity * argument * Register.t * Label.t
    4252
    4353  (* Memory store. Parameters are the size in bytes of what to store, the
    4454     register containing the address, the source register and the label of the
    4555     next statement. *)
    46   | St_store of AST.quantity * Register.t * Register.t * Label.t
     56  | St_store of AST.quantity * argument * argument * Label.t
    4757
    4858  (* Call to a function given its name. Parameters are the name of the
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

    r818 r1542  
    3333      lenv     : local_env }
    3434
     35type indexing = CostLabel.const_indexing
     36
    3537(* Execution states. There are three possible states :
    3638   - The constructor [State] represents a state when executing a function
     
    4042type state =
    4143  | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) *
    42              Label.t * local_env * memory * CostLabel.t list
     44       Label.t * local_env * memory * indexing list * CostLabel.t list
    4345  | CallState of stack_frame list * RTLabs.function_def *
    44                  Val.t list (* args *) * memory * CostLabel.t list
     46              Val.t list (* args *) * memory * indexing list * CostLabel.t list
    4547  | ReturnState of stack_frame list * Val.t (* return value *) *
    46                    memory * CostLabel.t list
     48        memory * indexing list * CostLabel.t list
    4749
    4850let string_of_local_env lenv =
     
    5759  List.fold_left f "" args
    5860
    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%!"
     61let print_state state = match state with
     62  | State (_, _, sp, lbl, lenv, mem, inds, _) ->
     63    Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
    6264      (Val.string_of_address sp)
    6365      (string_of_local_env lenv)
    64       (Mem.to_string mem)
     66      (Mem.to_string mem);
     67    let i = CostLabel.curr_const_ind inds in
     68    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
     69    Printf.printf "Regular state: %s\n\n%!"
    6570      lbl
    66   | CallState (_, _, args, mem, _) ->
     71  | CallState (_, _, args, mem, _, _) ->
    6772    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
    6873      (Mem.to_string mem)
    6974      (string_of_args args)
    70   | ReturnState (_, v, mem, _) ->
     75  | ReturnState (_, v, mem, _, _) ->
    7176    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    7277      (Mem.to_string mem)
     
    106111(* Assign a value to some destinations registers. *)
    107112
    108 let assign_state sfrs graph sp lbl lenv mem trace destr v =
     113let assign_state sfrs graph sp lbl lenv mem inds trace destr v =
    109114  let lenv = update_local destr v lenv in
    110   State (sfrs, graph, sp, lbl, lenv, mem, trace)
     115  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    111116
    112117(* Branch on a value. *)
    113118
    114 let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v =
     119let branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v =
    115120  let next_lbl =
    116121    if Val.is_true v then lbl_true
     
    118123      if Val.is_false v then lbl_false
    119124      else error "Undefined conditional value." in
    120   State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
    121 
     125  State (sfrs, graph, sp, next_lbl, lenv, mem, inds, trace)
     126
     127let curr_ind = CostLabel.curr_const_ind
     128
     129let forget_ind = CostLabel.forget_const_ind
     130
     131let new_ind = CostLabel.new_const_ind
     132
     133let eval_arg lenv mem sp = function
     134  | RTLabs.Reg r -> get_value lenv r
     135  | RTLabs.Imm (c, t) -> Eval.cst mem sp t c
     136
     137let get_type_arg lenv = function
     138  | RTLabs.Reg r -> get_type lenv r
     139  | RTLabs.Imm (_, typ) -> typ
    122140
    123141(* Interpret statements. *)
     
    130148    (mem   : memory)
    131149    (stmt  : RTLabs.statement)
     150    (inds  : indexing list)
    132151    (trace : CostLabel.t list) :
    133152    state = match stmt with
    134153
    135154      | RTLabs.St_skip lbl ->
    136         State (sfrs, graph, sp, lbl, lenv, mem, trace)
     155        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    137156
    138157      | RTLabs.St_cost (cost_lbl, lbl) ->
    139         State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace)
     158        let cost_lbl =
     159          CostLabel.ev_indexing (curr_ind inds) cost_lbl in
     160        State (sfrs, graph, sp, lbl, lenv,
     161               mem, inds, cost_lbl :: trace)
     162
     163      | RTLabs.St_ind_0 (i, lbl) ->
     164        CostLabel.enter_loop inds i;
     165        State (sfrs, graph, sp, lbl, lenv,
     166               mem, inds, trace)
     167
     168      | RTLabs.St_ind_inc (i, lbl) ->
     169        CostLabel.continue_loop inds i;
     170        State (sfrs, graph, sp, lbl, lenv,
     171               mem, inds, trace)
    140172
    141173      | RTLabs.St_cst (destr, cst, lbl) ->
    142174        let v = Eval.cst mem sp (get_type lenv destr) cst in
    143         assign_state sfrs graph sp lbl lenv mem trace destr v
     175        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    144176
    145177      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
     
    147179          Eval.op1 (get_type lenv destr) (get_type lenv srcr) op1
    148180            (get_value lenv srcr) in
    149         assign_state sfrs graph sp lbl lenv mem trace destr v
     181        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    150182
    151183      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
    152184        let v =
    153185          Eval.op2
    154             (get_type lenv destr) (get_type lenv srcr1) (get_type lenv srcr2)
     186            (get_type lenv destr)
     187            (get_type_arg lenv srcr1)
     188            (get_type_arg lenv srcr2)
    155189            op2
    156             (get_value lenv srcr1)
    157             (get_value lenv srcr2) in
    158         assign_state sfrs graph sp lbl lenv mem trace destr v
     190            (eval_arg lenv mem sp srcr1)
     191            (eval_arg lenv mem sp srcr2) in
     192        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    159193
    160194      | RTLabs.St_load (q, addr, destr, lbl) ->
    161         let addr = address_of_value (get_value lenv addr) in
     195        let addr = address_of_value (eval_arg lenv mem sp addr) in
    162196        let v = Mem.loadq mem q addr in
    163         assign_state sfrs graph sp lbl lenv mem trace destr v
     197        assign_state sfrs graph sp lbl lenv mem inds trace destr v
    164198
    165199      | RTLabs.St_store (q, addr, srcr, lbl) ->
    166         let addr = address_of_value (get_value lenv addr) in
    167         let v = get_value lenv srcr in
     200        let addr = address_of_value (eval_arg lenv mem sp addr) in
     201        let v = eval_arg lenv mem sp srcr in
    168202        let mem = Mem.storeq mem q addr v in
    169         State (sfrs, graph, sp, lbl, lenv, mem, trace)
     203        State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    170204
    171205      | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
     
    176210          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    177211        in
    178         CallState (sf :: sfrs, f_def, args, mem, trace)
     212        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    179213
    180214      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
     
    186220          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
    187221        in
    188         CallState (sf :: sfrs, f_def, args, mem, trace)
     222        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    189223
    190224      | RTLabs.St_tailcall_id (f, args, sg) ->
     
    193227        (* No need to save the stack frame. But free the stack. *)
    194228        let mem = Mem.free mem sp in
    195         CallState (sfrs, f_def, args, mem, trace)
     229        CallState (sfrs, f_def, args, mem, inds, trace)
    196230
    197231      | RTLabs.St_tailcall_ptr (r, args, sg) ->
     
    201235        (* No need to save the stack frame. But free the stack. *)
    202236        let mem = Mem.free mem sp in
    203         CallState (sfrs, f_def, args, mem, trace)
     237        CallState (sfrs, f_def, args, mem, inds, trace)
    204238
    205239      | RTLabs.St_cond (srcr, lbl_true, lbl_false) ->
    206240        let v = get_value lenv srcr in
    207         branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
     241        branch_state sfrs graph sp lbl_true lbl_false lenv mem inds trace v
    208242
    209243(*
     
    242276      | RTLabs.St_return None ->
    243277        let mem = Mem.free mem sp in
    244         ReturnState (sfrs, Val.undef, mem, trace)
     278        ReturnState (sfrs, Val.undef, mem, inds, trace)
    245279
    246280      | RTLabs.St_return (Some r) ->
    247281        let v = get_value lenv r in
    248282        let mem = Mem.free mem sp in
    249         ReturnState (sfrs, v, mem, trace)
     283        ReturnState (sfrs, v, mem, inds, trace)
    250284
    251285
     
    274308    (args  : Val.t list)
    275309    (mem   : memory)
     310    (inds  : indexing list)
    276311    (trace : CostLabel.t list) :
    277312    state =
     
    281316        Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
    282317      let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in
    283       State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry, lenv, mem',
    284              trace)
     318      (* allocate new constant indexing *)
     319      let graph = def.RTLabs.f_graph in
     320      let inds = new_ind inds in
     321      State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace)
    285322    | RTLabs.F_ext def ->
    286323      let (mem', v) = interpret_external mem def.AST.ef_tag args in
    287       ReturnState (sfrs, v, mem', trace)
     324      ReturnState (sfrs, v, mem', inds, trace)
    288325
    289326
     
    293330    (ret_val : Val.t)
    294331    (mem     : memory)
     332    (inds    : indexing list)
    295333    (trace   : CostLabel.t list) :
    296334    state =
     
    298336    | None -> sf.lenv
    299337    | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
    300   State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
     338      (* erase current indexing and revert to previous one *)
     339      let inds = forget_ind inds in
     340      State (sfrs, sf.graph, sf.sp, sf.pc, lenv,
     341             mem, inds, trace)
    301342
    302343
    303344let small_step (st : state) : state = match st with
    304   | State (sfrs, graph, sp, pc, lenv, mem, trace) ->
     345  | State (sfrs, graph, sp, pc, lenv, mem, inds, trace) ->
    305346    let stmt = Label.Map.find pc graph in
    306     interpret_statement sfrs graph sp lenv mem stmt trace
    307   | CallState (sfrs, f_def, args, mem, trace) ->
    308     state_after_call sfrs f_def args mem trace
    309   | ReturnState ([], ret_val, mem, trace) ->
     347    interpret_statement sfrs graph sp lenv mem stmt inds trace
     348  | CallState (sfrs, f_def, args, mem, inds, trace) ->
     349    state_after_call sfrs f_def args mem inds trace
     350  | ReturnState ([], ret_val, mem, inds, trace) ->
    310351    assert false (* End of execution; handled in iter_small_step. *)
    311   | ReturnState (sf :: sfrs, ret_val, mem, trace) ->
    312     state_after_return sf sfrs ret_val mem trace
     352  | ReturnState (sf :: sfrs, ret_val, mem, inds, trace) ->
     353    state_after_return sf sfrs ret_val mem inds trace
    313354
    314355
     
    324365  if debug then print_state st ;
    325366  match small_step st with
    326     | ReturnState ([], v, mem, trace) ->
     367    | ReturnState ([], v, mem, inds, trace) ->
    327368      print_and_return_result (compute_result v, List.rev trace)
    328369    | st' -> iter_small_step debug st'
     
    352393      let mem = init_mem p in
    353394      let main_def = find_function mem main in
    354       let st = CallState ([], main_def, [], mem, []) in
     395      let st = CallState ([], main_def, [], mem, [], []) in
    355396      iter_small_step debug st
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

    r818 r1542  
    4545
    4646let print_cmp = function
    47   | AST.Cmp_eq -> "eq"
    48   | AST.Cmp_ne -> "ne"
    49   | AST.Cmp_gt -> "gt"
    50   | AST.Cmp_ge -> "ge"
    51   | AST.Cmp_lt -> "lt"
    52   | AST.Cmp_le -> "le"
     47  | AST.Cmp_eq -> "="
     48  | AST.Cmp_ne -> "!="
     49  | AST.Cmp_gt -> ">"
     50  | AST.Cmp_ge -> ">="
     51  | AST.Cmp_lt -> "<"
     52  | AST.Cmp_le -> "<="
    5353
    5454let rec print_size = function
     
    8383  Printf.sprintf "%d%s" size (string_of_signedness sign)
    8484
    85 let print_op1 = function
     85let print_op1 op r = Printf.sprintf "%s %s"
     86  (match op with
    8687  | AST.Op_cast (int_type, dest_size) ->
    8788    Printf.sprintf "int%sto%d" (string_of_int_type int_type) dest_size
    88   | AST.Op_negint -> "negint"
    89   | AST.Op_notbool -> "notbool"
    90   | AST.Op_notint -> "notint"
    91   | AST.Op_id -> "id"
     89  | AST.Op_negint -> "-"
     90  | AST.Op_notbool -> "!"
     91  | AST.Op_notint -> "!i"
     92  | AST.Op_id -> ""
    9293  | AST.Op_ptrofint -> "ptrofint"
    93   | AST.Op_intofptr -> "intofptr"
    94 
    95 let print_op2 = function
    96   | AST.Op_add -> "add"
    97   | AST.Op_sub -> "sub"
    98   | AST.Op_mul -> "mul"
    99   | AST.Op_div -> "div"
     94  | AST.Op_intofptr -> "intofptr")
     95        (print_reg r)
     96
     97let print_arg = function
     98  | RTLabs.Reg r -> print_reg r
     99  | RTLabs.Imm (c, t) ->
     100    Printf.sprintf "(%s)%s" (Primitive.print_type t) (print_cst c)
     101
     102let print_op2 op r s = Printf.sprintf "%s %s %s"
     103  (print_arg r)
     104  (match op with
     105  | AST.Op_add -> "+"
     106  | AST.Op_sub -> "-"
     107  | AST.Op_mul -> "*"
     108  | AST.Op_div -> "/"
    100109  | AST.Op_divu -> "/u"
    101110  | AST.Op_mod -> "mod"
     
    104113  | AST.Op_or -> "or"
    105114  | AST.Op_xor -> "xor"
    106   | AST.Op_shl -> "shl"
    107   | AST.Op_shr -> "shr"
    108   | AST.Op_shru -> "shru"
     115  | AST.Op_shl -> "<<"
     116  | AST.Op_shr -> ">>"
     117  | AST.Op_shru -> ">>u"
    109118  | AST.Op_cmp cmp -> print_cmp cmp
    110   | AST.Op_addp -> "addp"
    111   | AST.Op_subp -> "subp"
    112   | AST.Op_subpp -> "subpp"
     119  | AST.Op_addp -> "+p"
     120  | AST.Op_subp -> "-p"
     121  | AST.Op_subpp -> "-pp"
    113122  | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p"
    114   | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u"
     123  | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u")
     124  (print_arg s)
    115125
    116126
     
    136146  | RTLabs.St_skip lbl -> "--> " ^ lbl
    137147  | RTLabs.St_cost (cost_lbl, lbl) ->
    138       Printf.sprintf "emit %s --> %s" cost_lbl lbl
     148    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
     149    Printf.sprintf "emit %s --> %s" cost_lbl lbl
     150  | RTLabs.St_ind_0 (i, lbl) ->
     151    Printf.sprintf "index %d --> %s" i lbl
     152  | RTLabs.St_ind_inc (i, lbl) ->
     153    Printf.sprintf "increment %d --> %s" i lbl
    139154  | RTLabs.St_cst (destr, cst, lbl) ->
    140       Printf.sprintf "imm %s, %s --> %s"
     155      Printf.sprintf "%s := %s --> %s"
    141156        (print_reg destr)
    142157        (print_cst cst)
    143158        lbl
    144159  | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
    145       Printf.sprintf "%s %s, %s --> %s"
    146         (print_op1 op1)
     160      Printf.sprintf "%s := %s --> %s"
    147161        (print_reg destr)
    148         (print_reg srcr)
     162  (print_op1 op1 srcr)
    149163        lbl
    150164  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
    151       Printf.sprintf "%s %s, %s, %s --> %s"
    152         (print_op2 op2)
     165      Printf.sprintf "%s := %s --> %s"
    153166        (print_reg destr)
    154         (print_reg srcr1)
    155         (print_reg srcr2)
     167  (print_op2 op2 srcr1 srcr2)
    156168        lbl
    157169  | RTLabs.St_load (q, addr, destr, lbl) ->
    158       Printf.sprintf "load %s, %s, %s --> %s"
     170      Printf.sprintf "%s := *(%s) %s --> %s"
     171        (print_reg destr)
    159172        (Memory.string_of_quantity q)
    160         (print_reg addr)
    161         (print_reg destr)
     173        (print_arg addr)
    162174        lbl
    163175  | RTLabs.St_store (q, addr, srcr, lbl) ->
    164       Printf.sprintf "store %s, %s, %s --> %s"
    165         (Memory.string_of_quantity q)
    166         (print_reg addr)
    167         (print_reg srcr)
    168         lbl
    169   | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    170       Printf.sprintf "call \"%s\", %s, %s: %s --> %s"
     176      Printf.sprintf "*(%s)%s := %s --> %s"
     177        (Memory.string_of_quantity q)
     178        (print_arg addr)
     179        (print_arg srcr)
     180        lbl
     181  | RTLabs.St_call_id (f, args, Some r, sg, lbl) ->
     182      Printf.sprintf "%s := \"%s\"(%s) : %s --> %s"
     183        (print_reg r)
    171184        f
    172185        (print_args args)
    173         (print_oreg res)
    174         (Primitive.print_sig sg)
    175         lbl
    176   | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    177       Printf.sprintf "call_ptr %s, %s, %s: %s --> %s"
     186        (Primitive.print_sig sg)
     187        lbl
     188  | RTLabs.St_call_id (f, args, None, sg, lbl) ->
     189      Printf.sprintf "\"%s\"(%s) : %s --> %s"
     190        f
     191        (print_args args)
     192        (Primitive.print_sig sg)
     193        lbl
     194  | RTLabs.St_call_ptr (f, args, Some r, sg, lbl) ->
     195      Printf.sprintf "%s := *%s (%s) : %s --> %s"
     196        (print_reg r)
    178197        (print_reg f)
    179198        (print_args args)
    180         (print_oreg res)
     199        (Primitive.print_sig sg)
     200        lbl
     201  | RTLabs.St_call_ptr (f, args, None, sg, lbl) ->
     202      Printf.sprintf "*%s (%s) : %s --> %s"
     203        (print_reg f)
     204        (print_args args)
    181205        (Primitive.print_sig sg)
    182206        lbl
    183207  | RTLabs.St_tailcall_id (f, args, sg) ->
    184       Printf.sprintf "tailcall \"%s\", %s: %s"
     208      Printf.sprintf "tailcall \"%s\" (%s) : %s"
    185209        f
    186210        (print_args args)
    187211        (Primitive.print_sig sg)
    188212  | RTLabs.St_tailcall_ptr (f, args, sg) ->
    189       Printf.sprintf "tailcall_ptr \"%s\", %s: %s"
     213      Printf.sprintf "tailcall *%s (%s) : %s"
    190214        (print_reg f)
    191215        (print_args args)
     
    225249
    226250
    227 let print_graph n c =
     251let print_graph n c entry =
    228252  let f lbl stmt s =
    229253    Printf.sprintf "%s%s: %s\n%s"
     
    232256      (print_statement stmt)
    233257      s in
    234   Label.Map.fold f c ""
    235 
    236 
     258  let f' lbl stmt (reach, s) =
     259    (Label.Set.add lbl reach, f lbl stmt s) in
     260  let (reachable, str) =
     261    RTLabsUtilities.dfs_fold f' c entry (Label.Set.empty, "") in
     262  let filter lbl _ = not (Label.Set.mem lbl reachable) in
     263  let c_rest = Label.Map.filter filter c in
     264  if Label.Map.is_empty c_rest then str else
     265    let str' = Label.Map.fold f c_rest "" in
     266    str ^ "DEAD NODES:\n" ^ str'
     267       
    237268let print_internal_decl n f def =
    238269
     
    252283    (n_spaces (n+2))
    253284    def.RTLabs.f_exit
    254     (print_graph (n+2) def.RTLabs.f_graph)
     285    (print_graph (n+2) def.RTLabs.f_graph def.RTLabs.f_entry)
    255286
    256287
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.mli

    r740 r1542  
    44val print_statement : RTLabs.statement -> string
    55
     6val print_cst : AST.cst -> string
     7
     8val print_op1 : AST.op1 -> Register.t -> string
     9
     10val print_op2 : AST.op2 -> RTLabs.argument -> RTLabs.argument -> string
     11
    612val print_program : RTLabs.program -> string
  • Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

    r818 r1542  
    9393  | RTL.St_skip _ -> RTL.St_skip lbl
    9494  | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl)
     95  | RTL.St_ind_0 (i, _) -> RTL.St_ind_0 (i, lbl)
     96  | RTL.St_ind_inc (i, _) -> RTL.St_ind_inc (i, lbl)
    9597  | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
    9698  | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
     
    685687    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
    686688
     689  | RTLabs.St_ind_0 (i, lbl') ->
     690    add_graph lbl (RTL.St_ind_0 (i, lbl')) def
     691
     692  | RTLabs.St_ind_inc (i, lbl') ->
     693    add_graph lbl (RTL.St_ind_inc (i, lbl')) def
     694
    687695  | RTLabs.St_cst (destr, cst, lbl') ->
    688696    translate_cst cst (find_local_env destr lenv) lbl lbl' def
     
    692700      lbl lbl' def
    693701
    694   | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
     702  | RTLabs.St_op2 (op2, destr, RTLabs.Reg srcr1, RTLabs.Reg srcr2, lbl') ->
    695703    translate_op2 op2 (find_local_env destr lenv)
    696704      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
    697705
    698   | RTLabs.St_load (_, addr, destr, lbl') ->
     706  | RTLabs.St_load (_, RTLabs.Reg addr, destr, lbl') ->
    699707    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
    700708      lbl lbl' def
    701709
    702   | RTLabs.St_store (_, addr, srcr, lbl') ->
     710  | RTLabs.St_store (_, RTLabs.Reg addr, RTLabs.Reg srcr, lbl') ->
    703711    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
    704712      lbl lbl' def
     
    739747  | RTLabs.St_return (Some r) ->
    740748    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
    741 
    742 
     749               
     750  | _ -> assert false (*not possible because of previous removal of immediates*)
     751
     752let remove_immediates def =
     753  let load_arg a lbl g rs = match a with
     754    | RTLabs.Reg r -> (lbl, g, rs, r)
     755    | RTLabs.Imm (c, t) ->
     756      let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in
     757      let new_r = Register.fresh def.RTLabs.f_runiverse in
     758      let g = Label.Map.add lbl (RTLabs.St_cst (new_r, c, new_l)) g in
     759      (new_l, g, (new_r, t) :: rs, new_r) in
     760  let f lbl stmt (g, rs) =
     761    match stmt with
     762      | RTLabs.St_op2(op, r, a1, a2, l) ->
     763        let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
     764        let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
     765        let s = RTLabs.St_op2 (op, r, RTLabs.Reg r1, RTLabs.Reg r2, l) in
     766        let g = Label.Map.add lbl' s g in
     767        (g, rs)
     768      | RTLabs.St_store(q, a1, a2, l) ->
     769        let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
     770        let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
     771        let s = RTLabs.St_store (q, RTLabs.Reg r1, RTLabs.Reg r2, l) in
     772        let g = Label.Map.add lbl' s g in
     773        (g, rs)
     774      | RTLabs.St_load (q, a, r, l) ->
     775        let (lbl', g, rs, r1) = load_arg a lbl g rs in
     776        let s = RTLabs.St_load (q, RTLabs.Reg r1, r, l) in
     777        let g = Label.Map.add lbl' s g in
     778        (g, rs)
     779      | _ -> (g, rs) in
     780  let g = def.RTLabs.f_graph in
     781  let (g, rs) = Label.Map.fold f g (g, []) in
     782  let locals = List.rev_append rs def.RTLabs.f_locals in
     783  { def with RTLabs.f_graph = g; RTLabs.f_locals = locals }
     784 
    743785let translate_internal def =
     786  let def = remove_immediates def in
    744787  let runiverse = def.RTLabs.f_runiverse in
    745788  let lenv =
  • Deliverables/D2.2/8051/src/acc.ml

    r1462 r1542  
    4444        the intermediate programs. *)
    4545    Languages.compile (Options.is_debug_enabled ())
    46       src_language tgt_language input_ast
     46      (Options.get_transformations ()) src_language tgt_language input_ast
    4747  in
    4848  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
     
    5151    begin
    5252      let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
    53         Languages.annotate input_ast final_ast in (
     53        let cost_tern = Options.is_cost_ternary_enabled () in
     54        Languages.annotate cost_tern input_ast final_ast in (
    5455          save ~suffix:"-annotated" annotated_input_ast;
    5556          Languages.save_cost exact_output output_filename cost_id cost_incr
    5657            extern_cost_variables);
    5758    end;
    58                                              
    59   if Options.is_debug_enabled () then 
     59
     60  if Options.is_debug_enabled () then
    6061    List.iter save intermediate_asts;
    6162
     
    9394    Languages.save
    9495      (Options.is_asm_pretty ()) exact_output output_filename "" ast in
    95   let target_asts = Languages.compile false src_language tgt_language input_ast
     96  let target_asts =
     97    Languages.compile false (Options.get_transformations ())
     98      src_language tgt_language input_ast
    9699  in
    97100  let final_ast, _ = Misc.ListExt.cut_last target_asts in
  • Deliverables/D2.2/8051/src/checker.ml

    r619 r1542  
    1414    in
    1515    let sentence (k, (v1, v2)) =
     16      let k = CostLabel.string_of_cost_label ~pretty:true k in
    1617      Printf.sprintf "  Label %s %s in language `%s' \
    1718                        whereas it %s in language `%s'."
  • Deliverables/D2.2/8051/src/clight/clight.mli

    r818 r1542  
    117117  (** The following constructors are used by the annotation process only. *)
    118118
    119   | Ecost of CostLabel.t*expr                   (**r cost label. *)
     119  | Ecost of CostLabel.t * expr                 (**r cost label. *)
    120120  | Ecall of ident * expr * expr
    121121
     
    130130type label = Label.t
    131131
     132type loop_index = CostLabel.index option
     133
    132134type statement =
    133135  | Sskip                                       (**r do nothing *)
     
    136138  | Ssequence of statement*statement            (**r sequence *)
    137139  | Sifthenelse of expr*statement*statement     (**r conditional *)
    138   | Swhile of expr*statement                    (**r [while] loop *)
    139   | Sdowhile of expr*statement                  (**r [do] loop *)
    140   | Sfor of statement*expr*statement*statement  (**r [for] loop *)
     140  | Swhile of loop_index*expr*statement         (**r [while] loop *)
     141  | Sdowhile of loop_index*expr*statement       (**r [do] loop *)
     142  | Sfor of loop_index*statement*expr*statement*statement (**r [for] loop *)
    141143  | Sbreak                                      (**r [break] statement *)
    142144  | Scontinue                                   (**r [continue] statement *)
  • Deliverables/D2.2/8051/src/clight/clightAnnotator.ml

    r1462 r1542  
    1010let cost_id_prefix = "_cost"
    1111let cost_incr_prefix = "_cost_incr"
     12let loop_id_prefix = "_i"
    1213
    1314
     
    7071  let def_idents = function
    7172    | Clight.Internal def ->
    72         let vars =
    73           string_set_of_list
    74             (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
    75         let (names, cost_labels, user_labels) =
    76           body_idents def.Clight.fn_body in
    77         (StringTools.Set.union vars names, cost_labels, user_labels)
     73      let vars =
     74        string_set_of_list
     75          (List.map fst (def.Clight.fn_params @ def.Clight.fn_vars)) in
     76      let (names, cost_labels, user_labels) =
     77        body_idents def.Clight.fn_body in
     78      (StringTools.Set.union vars names, cost_labels, user_labels)
    7879    | Clight.External (id, _, _) ->
    79         (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
     80      (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
    8081  let fun_idents (id, f_def) =
    8182    let (names, cost_labels, user_labels) = def_idents f_def in
     
    9394let all_labels p =
    9495  let (_, cost_labels, user_labels) = prog_idents p in
    95   let all =
    96     CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
    97       cost_labels StringTools.Set.empty in
    98   Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all
     96  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     97  let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
     98  Label.Set.fold StringTools.Set.add user_labels all
    9999
    100100let all_idents p =
    101101  let (names, cost_labels, user_labels) = prog_idents p in
     102  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     103  let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
    102104  let to_string_set fold set =
    103105    fold (fun lbl idents -> StringTools.Set.add lbl idents) set
    104106      StringTools.Set.empty in
    105   let cost_labels = to_string_set CostLabel.Set.fold cost_labels in
    106107  let user_labels = to_string_set Label.Set.fold user_labels in
    107108  StringTools.Set.union names (StringTools.Set.union cost_labels user_labels)
     
    125126let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
    126127
     128let expr_of_cost_cond var = function
     129  | CostExpr.Ceq k ->
     130    Clight.Expr(Clight.Ebinop(Clight.Oeq, var, const_int k),int_typ)
     131  | CostExpr.Cgeq k ->
     132    Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ)
     133  | CostExpr.Cmod (a, b) ->
     134    let modulus =
     135      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
     136    Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ)
     137  | CostExpr.Cgeqmod (k, a, b) ->
     138    let modulus =
     139      Clight.Expr(Clight.Ebinop(Clight.Omod, var, const_int a), int_typ) in
     140    let modulus_eq =
     141      Clight.Expr(Clight.Ebinop(Clight.Oeq, modulus, const_int b),int_typ) in
     142    let greater =
     143      Clight.Expr(Clight.Ebinop(Clight.Oge, var, const_int k),int_typ) in
     144    Clight.Expr(Clight.Eandbool(modulus_eq, greater),int_typ)
     145
     146let rec expr_of_cost_gen_cond var gc =
     147  assert (not (CostExpr.CondSet.is_empty gc));
     148  let c = CostExpr.CondSet.min_elt gc in
     149  let c_expr = expr_of_cost_cond var c in
     150  let rest = CostExpr.CondSet.remove c gc in
     151  if CostExpr.CondSet.is_empty rest then c_expr else
     152    let rest_expr = expr_of_cost_gen_cond var rest in
     153    Clight.Expr(Clight.Eandbool(c_expr, rest_expr), int_typ)
     154
     155let rec expr_of_cost_expr prefix = function
     156  | CostExpr.Exact k -> const_int k
     157  | CostExpr.Ternary(index, cond, if_true, if_false) ->
     158    let id = CostLabel.make_id prefix index in
     159    let var = Clight.Expr(Clight.Evar id, int_typ) in
     160    let cond_e = expr_of_cost_gen_cond var cond in
     161    let if_true_e = expr_of_cost_expr prefix if_true in
     162    let if_false_e = expr_of_cost_expr prefix if_false in
     163    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
     164
     165(* as long as Clight parser will be called at the end, this hack works *)
     166(* this will be called in case -no-cost-tern is active. *)
     167let rec side_effect_expr_of_cost_expr prefix cost_incr cont e_type = function
     168  | CostExpr.Exact k ->
     169    Clight.Expr(Clight.Ecall (cost_incr, const_int k, cont), e_type)
     170  | CostExpr.Ternary(index, cond, if_true, if_false) ->
     171    let id = CostLabel.make_id prefix index in
     172    let var = Clight.Expr(Clight.Evar id, int_typ) in
     173    let cond_e = expr_of_cost_gen_cond var cond in
     174    let rec_call = side_effect_expr_of_cost_expr prefix cost_incr cont e_type in
     175    let if_true_e = rec_call if_true in
     176    let if_false_e = rec_call if_false in
     177    Clight.Expr(Clight.Econdition(cond_e, if_true_e, if_false_e), int_typ)
     178
     179let rec stmt_of_cost_expr prefix cost_incr = function
     180  | CostExpr.Exact k -> Clight.Scall (None, cost_incr, [const_int k])
     181  | CostExpr.Ternary(index, cond, if_true, if_false) ->
     182    let id = CostLabel.make_id prefix index in
     183    let var = Clight.Expr(Clight.Evar id, int_typ) in
     184    let cond_e = expr_of_cost_gen_cond var cond in
     185    let if_true_s = stmt_of_cost_expr prefix cost_incr if_true in
     186    let if_false_s = stmt_of_cost_expr prefix cost_incr if_false in
     187    Clight.Sifthenelse (cond_e, if_true_s, if_false_s)
     188
    127189(* Instrument an expression. *)
    128190
    129 let rec instrument_expr cost_mapping cost_incr e =
    130   let Clight.Expr (e, t) = e in
    131   match e with
    132     | Clight.Ecost (lbl, e)
    133         when CostLabel.Map.mem lbl cost_mapping &&
    134              CostLabel.Map.find lbl cost_mapping = 0 ->
    135         e
    136     | _ ->
    137         let e' = instrument_expr_descr cost_mapping cost_incr e in
    138         Clight.Expr (e', t)
    139 and instrument_expr_descr cost_mapping cost_incr e = match e with
    140   | Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
    141   | Clight.Esizeof _ -> e
    142   | Clight.Ederef e ->
    143       let e' = instrument_expr cost_mapping cost_incr e in
    144       Clight.Ederef e'
    145   | Clight.Eaddrof e ->
    146       let e' = instrument_expr cost_mapping cost_incr e in
    147       Clight.Eaddrof e'
    148   | Clight.Eunop (op, e) ->
    149       let e' = instrument_expr cost_mapping cost_incr e in
    150       Clight.Eunop (op, e')
    151   | Clight.Ebinop (op, e1, e2) ->
    152       let e1' = instrument_expr cost_mapping cost_incr e1 in
    153       let e2' = instrument_expr cost_mapping cost_incr e2 in
    154       Clight.Ebinop (op, e1', e2')
    155   | Clight.Ecast (t, e) ->
    156       let e' = instrument_expr cost_mapping cost_incr e in
    157       Clight.Ecast (t, e')
    158   | Clight.Econdition (e1, e2, e3) ->
    159       let e1' = instrument_expr cost_mapping cost_incr e1 in
    160       let e2' = instrument_expr cost_mapping cost_incr e2 in
    161       let e3' = instrument_expr cost_mapping cost_incr e3 in
    162       Clight.Econdition (e1', e2', e3')
    163   | Clight.Eandbool (e1, e2) ->
    164       let e1' = instrument_expr cost_mapping cost_incr e1 in
    165       let e2' = instrument_expr cost_mapping cost_incr e2 in
    166       Clight.Eandbool (e1', e2')
    167   | Clight.Eorbool (e1, e2) ->
    168       let e1' = instrument_expr cost_mapping cost_incr e1 in
    169       let e2' = instrument_expr cost_mapping cost_incr e2 in
    170       Clight.Eorbool (e1', e2')
    171   | Clight.Efield (e, x) ->
    172       let e' = instrument_expr cost_mapping cost_incr e in
    173       Clight.Efield (e', x)
    174   | Clight.Ecost (lbl, e) when CostLabel.Map.mem lbl cost_mapping ->
    175       let e' = instrument_expr cost_mapping cost_incr e in
    176       let incr = CostLabel.Map.find lbl cost_mapping in
    177       if incr = 0 then let Clight.Expr (e'', _) = e' in e''
    178       else Clight.Ecall (cost_incr, const_int incr, e')
    179   | Clight.Ecost (_, e) ->
    180     let Clight.Expr (e', _) = instrument_expr cost_mapping cost_incr e in
    181     e'
    182   | Clight.Ecall (x, e1, e2) -> assert false (* Should not happen. *)
     191(* FIXME: currently using a hack (reparsing) *)
     192let instrument_expr cost_tern l_ind cost_mapping cost_incr =
     193  let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with
     194  | Clight.Ecost (lbl, _), e' :: _ ->
     195    let atom = lbl.CostLabel.name in
     196    let cost =
     197      try
     198        CostLabel.Atom.Map.find atom cost_mapping
     199      with (* if atom is not present, then map to 0 *)
     200        | Not_found -> CostExpr.Exact 0 in
     201    if cost = CostExpr.Exact 0 then e' else
     202      if cost_tern then
     203        let cost = expr_of_cost_expr l_ind cost in
     204        Clight.Expr(Clight.Ecall (cost_incr, cost, e'), et)
     205      else
     206        side_effect_expr_of_cost_expr l_ind cost_incr e' et cost
     207  | Clight.Ecall (_, _, _), _ -> assert false (* Should not happen. *)
     208  | _ -> ClightFold.expr_fill_exprs e sub_res in
     209  ClightFold.expr2 f_expr
     210
     211let loop_increment prefix depth body = match depth  with
     212  | None -> body
     213  | Some d ->
     214    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
     215    let add a b = Clight.Expr(Clight.Ebinop(Clight.Oadd, a, b), int_typ) in
     216    Clight.Ssequence(body, Clight.Sassign(id, add id (const_int 1)))
     217     
     218let loop_reset_index prefix depth loop = match depth with
     219  | None -> loop
     220  | Some d ->
     221    let id = Clight.Expr(Clight.Evar (CostLabel.make_id prefix d), int_typ) in
     222    Clight.Ssequence(Clight.Sassign(id, const_int 0), loop)
     223
    183224
    184225(* Instrument a statement. *)
    185226
    186 let rec instrument_body cost_mapping cost_incr stmt = match stmt with
    187   | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
    188   | Clight.Sgoto _ ->
    189     stmt
    190   | Clight.Sassign (e1, e2) ->
    191     let e1' = instrument_expr cost_mapping cost_incr e1 in
    192     let e2' = instrument_expr cost_mapping cost_incr e2 in
    193     Clight.Sassign (e1', e2')
    194   | Clight.Scall (eopt, f, args) ->
    195     let eopt' = match eopt with
    196       | None -> None
    197       | Some e -> Some (instrument_expr cost_mapping cost_incr e) in
    198     let f' = instrument_expr cost_mapping cost_incr f in
    199     let args' = List.map (instrument_expr cost_mapping cost_incr) args in
    200     Clight.Scall (eopt', f', args')
    201   | Clight.Ssequence (s1, s2) ->
    202     Clight.Ssequence (instrument_body cost_mapping cost_incr s1,
    203                       instrument_body cost_mapping cost_incr s2)
    204   | Clight.Sifthenelse (e, s1, s2) ->
    205     let e' = instrument_expr cost_mapping cost_incr e in
    206     let s1' = instrument_body cost_mapping cost_incr s1 in
    207     let s2' = instrument_body cost_mapping cost_incr s2 in
    208     Clight.Sifthenelse (e', s1', s2')
    209   | Clight.Swhile (e, s) ->
    210     let e' = instrument_expr cost_mapping cost_incr e in
    211     let s' = instrument_body cost_mapping cost_incr s in
    212     Clight.Swhile (e', s')
    213   | Clight.Sdowhile (e, s) ->
    214     let e' = instrument_expr cost_mapping cost_incr e in
    215     let s' = instrument_body cost_mapping cost_incr s in
    216     Clight.Sdowhile (e', s')
    217   | Clight.Sfor (s1, e, s2, s3) ->
    218     let s1' = instrument_body cost_mapping cost_incr s1 in
    219     let e' = instrument_expr cost_mapping cost_incr e in
    220     let s2' = instrument_body cost_mapping cost_incr s2 in
    221     let s3' = instrument_body cost_mapping cost_incr s3 in
    222     Clight.Sfor (s1', e', s2', s3')
    223   | Clight.Sreturn (Some e) ->
    224     let e' = instrument_expr cost_mapping cost_incr e in
    225     Clight.Sreturn (Some e')
    226   | Clight.Sswitch (e, ls) ->
    227     let e' = instrument_expr cost_mapping cost_incr e in
    228     let ls' = instrument_ls cost_mapping cost_incr ls in
    229     Clight.Sswitch (e', ls')
    230   | Clight.Slabel (lbl, s) ->
    231     let s' = instrument_body cost_mapping cost_incr s in
    232     Clight.Slabel (lbl, s')
    233   | Clight.Scost (lbl, s) when CostLabel.Map.mem lbl cost_mapping ->
     227(* FIXME: use ClightFold, a much better option *)
     228let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt =
     229  let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in
     230  let instr_body = instrument_body cost_tern l_ind cost_mapping cost_incr in
     231  match stmt with
     232    | Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sreturn None
     233    | Clight.Sgoto _ ->
     234      stmt
     235    | Clight.Sassign (e1, e2) ->
     236      let e1' = instr_expr e1 in
     237      let e2' = instr_expr e2 in
     238      Clight.Sassign (e1', e2')
     239    | Clight.Scall (eopt, f, args) ->
     240      let eopt' = Option.map instr_expr eopt in
     241      let f' = instr_expr f in
     242      let args = List.map (instr_expr) args in
     243      Clight.Scall (eopt', f', args)
     244    | Clight.Ssequence (s1, s2) ->
     245      Clight.Ssequence (
     246        instr_body s1,
     247        instr_body s2)
     248    | Clight.Sifthenelse (e, s1, s2) ->
     249      let e' = instr_expr e in
     250      let s1' = instr_body s1 in
     251      let s2' = instr_body s2 in
     252      Clight.Sifthenelse (e', s1', s2')
     253    | Clight.Swhile (i, e, s) ->
     254      let e' = instr_expr e in
     255      let s' = instr_body s in
     256      let s' = loop_increment l_ind i s' in
     257      loop_reset_index l_ind i (Clight.Swhile (None, e', s'))
     258    | Clight.Sdowhile (i, e, s) ->
     259      let e' = instr_expr e in
     260      let s' = instr_body s in
     261      let s' = loop_increment l_ind i s' in
     262      loop_reset_index l_ind i (Clight.Sdowhile (None, e', s'))
     263    | Clight.Sfor (i, s1, e, s2, s3) ->
     264      let s1' = instr_body s1 in
     265      let e' = instr_expr e in
     266      let s2' = instr_body s2 in
     267      let s3' = instr_body s3 in
     268      let s3' = loop_increment l_ind i s3' in
     269      loop_reset_index l_ind i (Clight.Sfor (None, s1', e', s2', s3'))
     270    | Clight.Sreturn (Some e) ->
     271      let e' = instr_expr e in
     272      Clight.Sreturn (Some e')
     273    | Clight.Sswitch (e, ls) ->
     274      let e' = instr_expr e in
     275      let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
     276      Clight.Sswitch (e', ls')
     277    | Clight.Slabel (lbl, s) ->
     278      let s' = instr_body s in
     279      Clight.Slabel (lbl, s')
     280    | Clight.Scost (lbl, s) ->
    234281    (* Keep the cost label in the code. *)
    235     let s' = instrument_body cost_mapping cost_incr s in
    236     let incr = CostLabel.Map.find lbl cost_mapping in
    237     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    238     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    239     let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
    240     Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
    241   (*
    242     let s' = instrument_body cost_mapping cost_incr s in
    243     let incr = CostLabel.Map.find lbl cost_mapping in
    244     if incr = 0 then s'
    245     else
    246     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    247     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    248     let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
    249     Clight.Ssequence (Clight.Scall (None, f, args), s')
    250   *)
    251   | Clight.Scost (lbl, s) ->
    252     (* Keep the cost label in the code and show the increment of 0. *)
    253     let s' = instrument_body cost_mapping cost_incr s in
    254     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
    255     let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
    256     let args = [Clight.Expr (Clight.Econst_int 0, int_typ)] in
    257     Clight.Scost (lbl, Clight.Ssequence (Clight.Scall (None, f, args), s'))
    258   (*
    259     instrument_body cost_mapping cost_incr s
    260   *)
    261 and instrument_ls cost_mapping cost_incr = function
     282      let s' = instr_body s in
     283      let atom = lbl.CostLabel.name in
     284      let cost =
     285        try
     286          CostLabel.Atom.Map.find atom cost_mapping
     287        with (* if atom is not present, then map to 0 *)
     288          | Not_found -> CostExpr.Exact 0 in
     289      let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
     290      let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
     291      let cost_stmt =
     292        if not cost_tern then stmt_of_cost_expr l_ind f cost else
     293        let cost = expr_of_cost_expr l_ind cost in
     294        Clight.Scall(None, f, [cost]) in
     295      Clight.Scost (lbl, Clight.Ssequence (cost_stmt, s'))
     296(*
     297  let s' = instrument_body l_ind cost_mapping cost_incr s in
     298  let incr = CostLabel.Map.find lbl cost_mapping in
     299  if incr = 0 then s'
     300  else
     301  let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
     302  let f = Clight.Expr (Clight.Evar cost_incr, fun_typ) in
     303  let args = [Clight.Expr (Clight.Econst_int incr, int_typ)] in
     304  Clight.Ssequence (Clight.Scall (None, f, args), s')
     305*)
     306(*
     307  instrument_body l_ind cost_mapping cost_incr s
     308*)
     309and instrument_ls cost_tern l_ind cost_mapping cost_incr = function
    262310  | Clight.LSdefault s ->
    263     let s' = instrument_body cost_mapping cost_incr s in
     311    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
    264312    Clight.LSdefault s'
    265313  | Clight.LScase (i, s, ls) ->
    266     let s' = instrument_body cost_mapping cost_incr s in
    267     let ls' = instrument_ls cost_mapping cost_incr ls in
     314    let s' = instrument_body cost_tern l_ind cost_mapping cost_incr s in
     315    let ls' = instrument_ls cost_tern l_ind cost_mapping cost_incr ls in
    268316    Clight.LScase (i, s', ls')
     317     
     318let rec loop_indexes_defs prefix max_depth =
     319  if max_depth = 0 then [] else
     320    let max_depth = max_depth - 1 in
     321    let id = CostLabel.make_id prefix max_depth in
     322    (id, int_typ) :: loop_indexes_defs prefix max_depth
     323
     324let max_depth =
     325  let f_expr _ _ = () in
     326  let f_stmt stmt _ res_stmts =
     327    let curr_max = List.fold_left max 0 res_stmts in
     328    if curr_max > 0 then curr_max else 
     329      match stmt with
     330        | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
     331        | Clight.Sfor(Some x,_,_,_,_) -> x + 1
     332        | _ -> 0 in
     333  ClightFold.statement2 f_expr f_stmt
    269334
    270335(* Instrument a function. *)
    271336
    272 let instrument_funct cost_mapping cost_incr (id, def) =
     337let instrument_funct cost_tern  l_ind cost_mapping cost_incr (id, def) =
    273338  let def = match def with
    274339    | Clight.Internal def ->
    275         let body = instrument_body cost_mapping cost_incr def.Clight.fn_body in
    276         Clight.Internal { def with Clight.fn_body = body }
     340      let max_depth = max_depth def.Clight.fn_body in
     341      let vars = loop_indexes_defs l_ind max_depth in
     342      let vars = List.rev_append vars def.Clight.fn_vars in
     343      let body = def.Clight.fn_body in
     344      let body =
     345        instrument_body cost_tern l_ind cost_mapping cost_incr body in
     346      Clight.Internal { def with Clight.fn_body = body; Clight.fn_vars = vars}
    277347    | Clight.External _ -> def
    278348  in
     
    326396    name of the cost variable and the name of the cost increment function. *)
    327397
    328 let instrument p cost_mapping =
     398let instrument cost_tern p cost_mapping =
    329399
    330400  (* Create a fresh 'cost' variable. *)
     
    334404  let cost_decl = cost_decl cost_id in
    335405
     406  (* Create a fresh loop index prefix *)
     407  let names = StringTools.Set.add cost_id names in
     408  let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in
     409
    336410  (* Create a fresh uninitialized global variable for each extern function. *)
    337411  let (extern_cost_decls, extern_cost_variables) =
     
    344418  let cost_incr_def = cost_incr_def cost_id cost_incr in
    345419
     420  (* Turn the mapping from indexed cost labels to integers into one from *)
     421  (* cost atoms to cost expresisons *)
     422  let cost_mapping = CostExpr.cost_expr_mapping_of_cost_mapping cost_mapping in
     423
    346424  (* Instrument each function *)
     425  let prog_funct = p.Clight.prog_funct in
    347426  let prog_funct =
    348     List.map (instrument_funct cost_mapping cost_incr) p.Clight.prog_funct in
     427    let f = instrument_funct cost_tern l_ind cost_mapping cost_incr in
     428    List.map f prog_funct in
    349429
    350430  (* Glue all this together. *)
  • Deliverables/D2.2/8051/src/clight/clightAnnotator.mli

    r1462 r1542  
    22(** This module defines the instrumentation of a [Clight] program. *)
    33
    4 (** [instrument prog cost_map] instruments the program [prog]. First a fresh
    5     global variable --- the so-called cost variable --- is added to the program.
    6     Then, each cost label in the program is replaced by an increment of the cost
    7     variable, following the mapping [cost_map]. The function also returns the
    8     name of the cost variable, the name of the cost increment function, and a
    9     fresh uninitialized global (cost) variable associated to each extern
    10     function. *)
    11 
    12 val instrument : Clight.program -> int CostLabel.Map.t ->
     4(** [instrument cost_tern prog cost_map] instruments the program [prog]. First a
     5    fresh global variable --- the so-called cost variable --- is added to the
     6    program. Then, each cost label in the program is replaced by an increment of
     7    the cost variable, following the mapping [cost_map]. The function also
     8    returns the name of the cost variable, the name of the cost increment
     9    function, and a fresh uninitialized global (cost) variable associated to each
     10    extern function. [cost_tern] rules whether cost increments are given by
     11    ternary expressions (more readable) or by branch statements (for frama-c
     12    itegration). *)
     13val instrument : bool -> Clight.program -> int CostLabel.Map.t ->
    1314                 Clight.program * string * string * string StringTools.Map.t
    1415
  • Deliverables/D2.2/8051/src/clight/clightFold.ml

    r818 r1542  
    116116  | Clight.Ssequence (stmt1, stmt2) -> ([], [stmt1 ; stmt2])
    117117  | Clight.Sifthenelse (e, stmt1, stmt2) -> ([e], [stmt1 ; stmt2])
    118   | Clight.Swhile (e, stmt) | Clight.Sdowhile (e, stmt) -> ([e], [stmt])
    119   | Clight.Sfor (stmt1, e, stmt2, stmt3) -> ([e], [stmt1 ; stmt2 ; stmt3])
     118  | Clight.Swhile (_, e, stmt) | Clight.Sdowhile (_, e, stmt) -> ([e], [stmt])
     119  | Clight.Sfor (_, stmt1, e, stmt2, stmt3) -> ([e], [stmt1 ; stmt2 ; stmt3])
    120120  | Clight.Sreturn (Some e) -> ([e], [])
    121121  | Clight.Sswitch (e, lbl_stmts) -> ([e], labeled_statements_subs lbl_stmts)
     
    145145    | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
    146146      Clight.Sifthenelse (e, stmt1, stmt2)
    147     | Clight.Swhile _, e :: _, stmt :: _ ->
    148       Clight.Swhile (e, stmt)
    149     | Clight.Sdowhile _, e :: _, stmt :: _ ->
    150       Clight.Sdowhile (e, stmt)
    151     | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
    152       Clight.Sfor (stmt1, e, stmt2, stmt3)
     147    | Clight.Swhile (i, _, _), e :: _, stmt :: _ ->
     148      Clight.Swhile (i, e, stmt)
     149    | Clight.Sdowhile (i, _, _), e :: _, stmt :: _ ->
     150      Clight.Sdowhile (i, e, stmt)
     151    | Clight.Sfor (i, _, _, _, _), e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
     152      Clight.Sfor (i, stmt1, e, stmt2, stmt3)
    153153    | Clight.Sreturn (Some _), e :: _, _ -> Clight.Sreturn (Some e)
    154154    | Clight.Sswitch (_, lbl_stmts), e :: _, _ ->
  • Deliverables/D2.2/8051/src/clight/clightFromC.ml

    r818 r1542  
    490490      Sifthenelse(convertExpr env e, convertStmt env s1, convertStmt env s2)
    491491  | C.Swhile(e, s1) ->
    492       Swhile(convertExpr env e, convertStmt env s1)
     492      Swhile(None, convertExpr env e, convertStmt env s1)
    493493  | C.Sdowhile(s1, e) ->
    494       Sdowhile(convertExpr env e, convertStmt env s1)
     494      Sdowhile(None, convertExpr env e, convertStmt env s1)
    495495  | C.Sfor(s1, e, s2, s3) ->
    496       Sfor(convertStmt env s1, convertExpr env e, convertStmt env s2,
     496      Sfor(None, convertStmt env s1, convertExpr env e, convertStmt env s2,
    497497           convertStmt env s3)
    498498  | C.Sbreak ->
  • Deliverables/D2.2/8051/src/clight/clightInterpret.ml

    r818 r1542  
    44type localEnv = Value.address LocalEnv.t
    55type memory = Clight.fundef Mem.memory
     6type indexing = CostLabel.const_indexing
    67
    78open Clight
     
    2627  | Kstop
    2728  | Kseq of statement*continuation
    28   | Kwhile of expr*statement*continuation
    29   | Kdowhile of expr*statement*continuation
    30   | Kfor2 of expr*statement*statement*continuation
    31   | Kfor3 of expr*statement*statement*continuation
     29  | Kwhile of int option*expr*statement*continuation
     30  | Kdowhile of int option*expr*statement*continuation
     31  | Kfor2 of int option*expr*statement*statement*continuation
     32  | Kfor3 of int option*expr*statement*statement*continuation
    3233  | Kswitch of continuation
    3334  | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
    3435
    3536type state =
    36   | State of cfunction*statement*continuation*localEnv*memory
    37   | Callstate of fundef*Value.t list*continuation*memory
    38   | Returnstate of Value.t*continuation*memory
     37  | State of cfunction*statement*continuation*localEnv*memory*indexing list
     38  | Callstate of fundef*Value.t list*continuation*memory*indexing list
     39  | Returnstate of Value.t*continuation*memory*indexing list
    3940
    4041let string_of_unop = function
     
    104105  | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
    105106  | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
    106   | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
     107  | Ecost (cost_lbl, e) ->
     108    let cost_lbl = CostLabel.string_of_cost_label cost_lbl in
     109    "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
    107110  | Ecall (f, arg, e) ->
    108111    "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
     
    110113let string_of_args args =
    111114  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
     115
     116let string_of_loop_depth = function
     117        | None -> ""
     118        | Some d -> " at " ^ string_of_int d
    112119
    113120let rec string_of_statement = function
     
    119126  | Ssequence _ -> "sequence"
    120127  | 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) ^ "; ...)"
     128  | Swhile (i, e, _) ->
     129                let d = string_of_loop_depth i in
     130                "while" ^ d ^ " (" ^ (string_of_expr e) ^ ")"
     131  | Sdowhile (i, _, _) ->
     132    let d = string_of_loop_depth i in
     133    "dowhile" ^ d
     134  | Sfor (i, s, _, _, _) ->
     135                let d = string_of_loop_depth i in
     136                "for" ^ d ^ " (" ^ (string_of_statement s) ^ "; ...)"
    124137  | Sbreak -> "break"
    125138  | Scontinue -> "continue"
     
    129142  | Slabel (lbl, _) -> "label " ^ lbl
    130143  | Sgoto lbl -> "goto " ^ lbl
    131   | Scost (lbl, _) -> "cost " ^ lbl
     144  | Scost (lbl, _) ->
     145    let lbl = CostLabel.string_of_cost_label lbl in
     146                "cost " ^ lbl
    132147
    133148let string_of_local_env lenv =
     
    136151  LocalEnv.fold f lenv ""
    137152
    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%!"
     153let print_state state = match state with
     154  | State (_, stmt, _, lenv, mem, c) ->
     155    Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing: "
    141156      (string_of_local_env lenv)
    142       (Mem.to_string mem)
     157      (Mem.to_string mem);
     158    let i = CostLabel.curr_const_ind c in
     159    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
     160    Printf.printf "\nRegular state: %s\n\n%!"
    143161      (string_of_statement stmt)
    144   | Callstate (_, args, _, mem) ->
     162  | Callstate (_, args, _, mem, _) ->
    145163    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
    146164      (Mem.to_string mem)
    147165      (MiscPottier.string_of_list " " Value.to_string args)
    148   | Returnstate (v, _, mem) ->
     166  | Returnstate (v, _, mem, _) ->
    149167    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    150168      (Mem.to_string mem)
     
    155173
    156174let rec call_cont = function
    157   | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
    158   | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
     175  | Kseq (_,k) | Kwhile (_, _,_,k) | Kdowhile (_, _,_,k)
     176  | Kfor2 (_, _,_,_,k) | Kfor3 (_, _,_,_,k) | Kswitch k -> call_cont k
    159177  | k -> k
    160178
     
    174192      | None -> find_label1 lbl s2 k
    175193      )
    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
     194  | Swhile (i,a,s1) -> find_label1 lbl s1 (Kwhile(i,a,s1,k))
     195  | Sdowhile (i,a,s1) -> find_label1 lbl s1 (Kdowhile(i,a,s1,k))
     196  | Sfor (i,a1,a2,a3,s1) ->
     197                (* doubt: should we search for labels in a1? *)
     198      (match find_label1 lbl a1 (Kseq ((Sfor(i,Sskip,a2,a3,s1)),k)) with
    180199      | Some sk -> Some sk
    181200      | None ->
    182           (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
     201          (match find_label1 lbl s1 (Kfor2(i,a2,a3,s1,k)) with
    183202          | Some sk -> Some sk
    184           | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
     203          | None -> find_label1 lbl a3 (Kfor3(i,a2,a3,s1,k))
    185204          ))
    186205  | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
     
    355374let is_false (v, _) = Value.is_false v
    356375
    357 let rec eval_expr localenv m (Expr (ee, tt)) =
     376let rec eval_expr localenv m c (Expr (ee, tt)) =
    358377  match ee with
    359378    | Econst_int i ->
     
    369388      ((v, tt), [])
    370389    | Ederef e when is_function_type tt || is_big_type tt ->
    371       let ((v1,_),l1) = eval_expr localenv m e in
     390      let ((v1,_),l1) = eval_expr localenv m c e in
    372391      ((v1,tt),l1)
    373392    | Ederef e ->
    374       let ((v1,_),l1) = eval_expr localenv m e in
     393      let ((v1,_),l1) = eval_expr localenv m c e in
    375394      let addr = address_of_value v1 in
    376395      let v = Mem.load m (size_of_ctype tt) addr in
    377396      ((v,tt),l1)
    378397    | Eaddrof exp ->
    379       let ((addr,_),l) = eval_lvalue localenv m exp in
     398      let ((addr,_),l) = eval_lvalue localenv m c exp in
    380399      ((value_of_address addr,tt),l)
    381400    | Ebinop (op,exp1,exp2) -> 
    382       let (v1,l1) = eval_expr localenv m exp1 in
    383       let (v2,l2) = eval_expr localenv m exp2 in
     401      let (v1,l1) = eval_expr localenv m c exp1 in
     402      let (v2,l2) = eval_expr localenv m c exp2 in
    384403      ((eval_binop tt v1 v2 op,tt),l1@l2)
    385404    | Eunop (op,exp) ->
    386       let (e1,l1) = eval_expr localenv m exp in
     405      let (e1,l1) = eval_expr localenv m c exp in
    387406      ((eval_unop tt e1 op,tt),l1)
    388407    | Econdition (e1,e2,e3) ->
    389       let (v1,l1) = eval_expr localenv m e1 in
    390       if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     408      let (v1,l1) = eval_expr localenv m c e1 in
     409      if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
    391410      else
    392         if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)
     411        if is_false v1 then let (v3,l3) = eval_expr localenv m c e3 in (v3,l1@l3)
    393412      else (v1,l1)
    394413    | Eandbool (e1,e2) ->
    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)
     414      let (v1,l1) = eval_expr localenv m c e1 in
     415      if is_true v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
    397416      else (v1,l1)
    398417    | Eorbool (e1,e2) ->
    399       let (v1,l1) = eval_expr localenv m e1 in
    400       if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     418      let (v1,l1) = eval_expr localenv m c e1 in
     419      if is_false v1 then let (v2,l2) = eval_expr localenv m c e2 in (v2,l1@l2)
    401420      else (v1,l1)
    402421    | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
    403422    | Efield (e1,id) ->
    404       let ((v1,t1),l1) = eval_expr localenv m e1 in
     423      let ((v1,t1),l1) = eval_expr localenv m c e1 in
    405424      let addr = address_of_value (get_offset v1 id t1) in
    406425      ((Mem.load m (size_of_ctype tt) addr, tt), l1)
    407426    | Ecost (lbl,e1) ->
    408       let (v1,l1) = eval_expr localenv m e1 in
     427      (* applying current indexing on label *)
     428      let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
     429      let (v1,l1) = eval_expr localenv m c e1 in
    409430      (v1,lbl::l1)
    410431    | Ecall _ -> assert false (* only used by the annotation process *)
    411432    | Ecast (cty,exp) ->
    412       let ((v,ty),l1) = eval_expr localenv m exp in
     433      let ((v,ty),l1) = eval_expr localenv m c exp in
    413434      ((eval_cast (v,ty,cty),tt),l1)
    414435
    415 and eval_lvalue localenv m (Expr (e,t)) = match e with
     436and eval_lvalue localenv m c (Expr (e,t)) = match e with
    416437  | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
    417438  | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
     
    419440  | Evar id -> ((find_symbol localenv m id,t),[])
    420441  | Ederef ee ->
    421     let ((v,_),l1) = eval_expr localenv m ee in
     442    let ((v,_),l1) = eval_expr localenv m c ee in
    422443    ((address_of_value v,t),l1)
    423444  | Efield (ee,id) ->
    424     let ((v,tt),l1) = eval_expr localenv m ee in
     445    let ((v,tt),l1) = eval_expr localenv m c ee in
    425446    let v' = get_offset v id tt in
    426447    ((address_of_value v', t), l1)
    427448  | Ecost (lbl,ee) ->
    428     let (v,l) = eval_lvalue localenv m ee in
     449    let (v,l) = eval_lvalue localenv m c ee in
    429450    (v,lbl::l)
    430451  | Ecall _ -> assert false (* only used in the annotation process *)
    431452
    432 let eval_exprlist lenv mem es =
     453let eval_exprlist lenv mem c es =
    433454  let f (vs, cost_lbls) e =
    434     let ((v, _), cost_lbls') = eval_expr lenv mem e in
     455    let ((v, _), cost_lbls') = eval_expr lenv mem c e in
    435456    (vs @ [v], cost_lbls @ cost_lbls') in
    436457  List.fold_left f ([], []) es
     
    464485  else error "undefined condition guard value."
    465486
    466 let eval_stmt f k e m s = match s, k with
    467   | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[])
    468   | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
    469   | Sskip, Kdowhile(a,s,k) ->
    470     let ((v1, _),l1) = eval_expr e m a in
    471     let a_false = (State(f,Sskip,k,e,m),l1) in
    472     let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
     487let eval_stmt f k e m s c = match s, k with
     488  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[])
     489  | Sskip, Kwhile(i,a,s,k') | Scontinue, Kwhile(i,a,s,k')
     490  | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') ->
     491    (* possibly continuing a loop *)
     492    CostLabel.continue_loop_opt c i; (* if loop is not continued, this change
     493                                        will have no effect in the following. *)
     494    let ((v1,_),l1) = eval_expr e m c a in
     495    let a_false = (State(f,Sskip,k',e,m,c),l1) in
     496    let a_true = (State(f,s,k,e,m,c),l1) in
    473497    condition v1 a_true a_false
    474   | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
    475   | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    476   | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
     498  | Sskip, Kfor3(i,a2,a3,s,k) | Scontinue, Kfor3(i,a2,a3,s,k) ->
     499    CostLabel.continue_loop_opt c i;
     500    let ((v1,_),l1) = eval_expr e m c a2 in
     501    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     502    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
     503    condition v1 a_true a_false
     504  | Sskip, Kfor2(i,a2,a3,s,k) ->
     505    (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[])
     506  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
    477507  | Sskip, Kcall _ ->
    478508    let m' = free_local_env m e in
    479     (Returnstate(Value.undef,k,m'),[])
     509    (Returnstate(Value.undef,k,m',c),[])
    480510  | Sassign(a1, a2), _ ->
    481     let ((v1,t1),l1) = (eval_lvalue e m a1) in
    482     let ((v2,t2),l2) = eval_expr e m a2 in
    483     (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
     511    let ((v1,t1),l1) = (eval_lvalue e m c a1) in
     512    let ((v2,t2),l2) = eval_expr e m c a2 in
     513    (State(f,Sskip,k,e,assign m v2 t1 v1,c),l1@l2)
    484514  | Scall(None,a,al), _ ->
    485     let ((v1,_),l1) = eval_expr e m a in
     515    let ((v1,_),l1) = eval_expr e m c a in
    486516    let fd = Mem.find_fun_def m (address_of_value v1) in
    487     let (vargs,l2) = eval_exprlist e m al in
    488     (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
     517    let (vargs,l2) = eval_exprlist e m c al in
     518    (Callstate(fd,vargs,Kcall(None,f,e,k),m,c),l1@l2)
    489519  | Scall(Some lhs,a,al), _ ->
    490     let ((v1,_),l1) = eval_expr e m a in
     520    let ((v1,_),l1) = eval_expr e m c a in
    491521    let fd = Mem.find_fun_def m (address_of_value v1) in
    492     let (vargs,l2) = eval_exprlist e m al in
    493     let (vt3,l3) = eval_lvalue e m lhs in
    494     (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m),l1@l2@l3)
    495   | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m),[])
     522    let (vargs,l2) = eval_exprlist e m c al in
     523    let (vt3,l3) = eval_lvalue e m c lhs in
     524    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m,c),l1@l2@l3)
     525  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m,c),[])
    496526  | Sifthenelse(a,s1,s2), _ ->
    497     let ((v1,_),l1) = eval_expr e m a in
    498     let a_true = (State(f,s1,k,e,m),l1) in
    499     let a_false = (State(f,s2,k,e,m),l1) in
     527    let ((v1,_),l1) = eval_expr e m c a in
     528    let a_true = (State(f,s1,k,e,m,c),l1) in
     529    let a_false = (State(f,s2,k,e,m,c),l1) in
    500530    condition v1 a_true a_false
    501   | Swhile(a,s), _ ->
    502     let ((v1,_),l1) = eval_expr e m a in
    503     let a_false = (State(f,Sskip,k,e,m),l1) in
    504     let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in
     531  | Swhile(i,a,s), _ ->
     532    CostLabel.enter_loop_opt c i;
     533    let ((v1,_),l1) = eval_expr e m c a in
     534    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     535    let a_true = (State(f,s,Kwhile(i,a,s,k),e,m,c),l1) in
    505536    condition v1 a_true a_false
    506   | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
    507   | Sfor(Sskip,a2,a3,s), _ ->
    508     let ((v1,_),l1) = eval_expr e m a2 in
    509     let a_false = (State(f,Sskip,k,e,m),l1) in
    510     let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in
     537  | Sdowhile(i,a,s), _ ->
     538    CostLabel.enter_loop_opt c i;
     539    (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
     540  | Sfor(i,Sskip,a2,a3,s), _ ->
     541    CostLabel.enter_loop_opt c i;
     542    let ((v1,_),l1) = eval_expr e m c a2 in
     543    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     544    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
    511545    condition v1 a_true a_false
    512   | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
    513   | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[])
    514   | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
    515   | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
    516   | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[])
    517   | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[])
    518   | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[])
    519   | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
    520   | Scontinue, Kdowhile(a,s,k) ->
    521     let ((v1,_),l1) = eval_expr e m a in
    522     let a_false = (State(f,Sskip,k,e,m),l1) in
    523     let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
    524     condition v1 a_true a_false
    525   | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    526   | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[])
     546  | Sfor(i,a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(i,Sskip,a2,a3,s),k),e,m,c),[])
     547  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m,c),[])
     548  | Sbreak, Kwhile(_,_,_,k) | Sbreak, Kdowhile(_,_,_,k)
     549  | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
     550  | Scontinue, Kseq(_,k)
     551  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[])
    527552  | Sreturn None, _ ->
    528553    let m' = free_local_env m e in
    529     (Returnstate(Value.undef,(call_cont k),m'),[])
     554    (Returnstate(Value.undef,(call_cont k),m',c),[])
    530555  | Sreturn (Some a), _ ->
    531     let ((v1,_),l1) = eval_expr e m a  in
     556    let ((v1,_),l1) = eval_expr e m c a  in
    532557    let m' = free_local_env m e in
    533     (Returnstate(v1,call_cont k,m'),l1)
     558    (Returnstate(v1,call_cont k,m',c),l1)
    534559  | Sswitch(a,sl), _ ->
    535     let ((v,_),l) = eval_expr e m a in
     560    let ((v,_),l) = eval_expr e m c a in
    536561    let n = Value.to_int v in
    537     (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
    538   | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[])
    539   | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl])
     562  (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l)
     563  | Slabel(lbl,s), _ -> (State(f,s,k,e,m,c),[])
     564  | Scost(lbl,s), _ ->
     565    (* applying current indexing on label *)
     566    let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
     567    (State(f,s,k,e,m,c),[lbl])
    540568  | Sgoto lbl, _ ->
     569    (* if we exit an indexed loop, we don't care. It should not be possible to *)
     570    (* enter an indexed loop that is not the current one, so we do nothing *)
     571    (* to loop indexes *)
    541572    let (s', k') = find_label lbl f.fn_body (call_cont k) in
    542     (State(f,s',k',e,m),[])
     573    (State(f,s',k',e,m,c),[])
    543574  | _ -> assert false (* should be impossible *)
    544575
     
    546577module InterpretExternal = Primitive.Interpret (Mem)
    547578
    548 let interpret_external k mem f args =
     579let interpret_external k mem c f args =
    549580  let (mem', v) = match InterpretExternal.t mem f args with
    550581    | (mem', InterpretExternal.V vs) ->
     
    552583      (mem', v)
    553584    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    554   Returnstate (v, k, mem')
    555 
    556 let step_call args cont mem = function
     585  Returnstate (v, k, mem',c)
     586
     587let step_call args cont mem c = function
    557588  | Internal f ->
    558589    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
    559     State (f, f.fn_body, cont, e, mem')
     590    (* initializing loop indices *)
     591    let c = CostLabel.new_const_ind c in
     592    State (f, f.fn_body, cont, e, mem', c)
    560593  | External(id,targs,tres) when List.length targs = List.length args ->
    561     interpret_external cont mem id args
     594    interpret_external cont mem c id args
    562595  | External(id,_,_) ->
    563596    error ("wrong size of arguments when calling external " ^ id ^ ".")
    564597
    565598let step = function
    566   | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt
    567   | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    568   | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
    569   | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) ->
     599  | State(f,stmt,k,e,m,c) -> eval_stmt f k e m stmt c
     600  | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[])
     601  | Returnstate(v,Kcall(None,f,e,k),m,c) ->
     602    let c = CostLabel.forget_const_ind c in
     603    (State(f,Sskip,k,e,m,c),[])
     604  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) ->
     605    let c = CostLabel.forget_const_ind c in
    570606    let m' = assign m v ty vv in
    571     (State(f,Sskip,k,e,m'),[])
     607    (State(f,Sskip,k,e,m',c),[])
    572608  | _ -> error "state malformation."
    573609
     
    603639    if debug then Printf.printf "Result = %s\n%!"
    604640      (IntValue.Int32.to_string res) ;
    605     (res, cost_labels) in
     641    (res, List.rev cost_labels) in
    606642  if debug then print_state state ;
    607643  match state with
    608     | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
     644    | Returnstate(v,Kstop,_,_) -> (* Explicit return in main *)
    609645      print_and_return_result (compute_result v)
    610     | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
     646    | State(_,Sskip,Kstop,_,_,_) -> (* Implicit return in main *)
    611647      print_and_return_result IntValue.Int32.zero
    612648    | state -> exec debug cost_labels (step state)
     
    618654    | Some main ->
    619655      let mem = init_mem prog in
    620       let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
     656      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem,[]),[]) in
    621657      exec debug [] first_state
  • Deliverables/D2.2/8051/src/clight/clightLabelling.ml

    r1504 r1542  
    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
     
    68
    79
    8 (* Add a cost label in front of a statement. *)
    9 
    10 let add_starting_cost_label cost_universe stmt =
    11   Clight.Scost (CostLabel.Gen.fresh cost_universe, stmt)
     10(* Add a cost label in front of a statement with the current indexing. *)
     11
     12let add_starting_cost_label indexing cost_universe stmt =
     13  Clight.Scost (CostLabel.fresh indexing cost_universe, stmt)
    1214
    1315(* Add a cost label at the end of a statement. *)
    1416
    15 let add_ending_cost_label cost_universe stmt =
    16   Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip)
     17let add_ending_cost_label indexing cost_universe stmt =
     18  let lbld_skip = add_starting_cost_label indexing cost_universe Clight.Sskip in
     19  Clight.Ssequence (stmt, lbld_skip)
    1720
    1821
     
    2427
    2528
    26 let add_cost_label_e cost_universe e =
    27   Expr (Ecost (CostLabel.Gen.fresh cost_universe, e), typeof e)
     29let add_cost_label_e indexing cost_universe e =
     30  Expr (Ecost (CostLabel.fresh indexing cost_universe, e), typeof e)
    2831
    2932
    3033(* Add cost labels to an expression. *)
    3134
    32 let rec add_cost_labels_e cost_universe = function 
    33   | Expr (exp,cty) -> Expr (add_cost_labels_expr cost_universe exp,cty)
    34 
    35 and add_cost_labels_expr cost_universe exp = match exp with
     35let rec add_cost_labels_e ind cost_universe = function 
     36  | Expr (exp,cty) -> Expr (add_cost_labels_expr ind cost_universe exp,cty)
     37
     38and add_cost_labels_expr ind cost_universe exp = match exp with
    3639  | Econst_int _ | Econst_float _ | Evar _ | Esizeof _ -> exp
    37   | Ederef e -> Ederef (add_cost_labels_e cost_universe e)
    38   | Eaddrof e -> Eaddrof (add_cost_labels_e cost_universe e)
    39   | Eunop (op,e) -> Eunop (op,(add_cost_labels_e cost_universe e))
     40  | Ederef e -> Ederef (add_cost_labels_e ind cost_universe e)
     41  | Eaddrof e -> Eaddrof (add_cost_labels_e ind cost_universe e)
     42  | Eunop (op,e) -> Eunop (op,(add_cost_labels_e ind cost_universe e))
    4043  | Ebinop (op,e1,e2) ->
    4144      Ebinop (op,
    42               add_cost_labels_e cost_universe e1,
    43               add_cost_labels_e cost_universe e2)
    44   | Ecast (t,e) -> Ecast (t, add_cost_labels_e cost_universe e)
     45              add_cost_labels_e ind cost_universe e1,
     46              add_cost_labels_e ind cost_universe e2)
     47  | Ecast (t,e) -> Ecast (t, add_cost_labels_e ind cost_universe e)
    4548  | Eandbool (e1,e2) ->
    46       let e1' = add_cost_labels_e cost_universe e1 in
    47       let e2' = add_cost_labels_e cost_universe e2 in
    48       let b1 = add_cost_label_e cost_universe (const_int 1) in
    49       let b2 = add_cost_label_e cost_universe (const_int 0) in
     49      let e1' = add_cost_labels_e ind cost_universe e1 in
     50      let e2' = add_cost_labels_e ind cost_universe e2 in
     51      let b1 = add_cost_label_e ind cost_universe (const_int 1) in
     52      let b2 = add_cost_label_e ind cost_universe (const_int 0) in
    5053      let e2' = Expr (Econdition (e2', b1, b2), int_type) in
    51       let e2' = add_cost_label_e cost_universe e2' in
    52       let e3' = add_cost_label_e cost_universe (const_int 0) in
     54      let e2' = add_cost_label_e ind cost_universe e2' in
     55      let e3' = add_cost_label_e ind cost_universe (const_int 0) in
    5356      Econdition (e1', e2', e3')
    5457  | Eorbool (e1,e2) ->
    55       let e1' = add_cost_labels_e cost_universe e1 in
    56       let e2' = add_cost_label_e cost_universe (const_int 1) in
    57       let e3' = add_cost_labels_e cost_universe e2 in
    58       let b1 = add_cost_label_e cost_universe (const_int 1) in
    59       let b2 = add_cost_label_e cost_universe (const_int 0) in
     58      let e1' = add_cost_labels_e ind cost_universe e1 in
     59      let e2' = add_cost_label_e ind cost_universe (const_int 1) in
     60      let e3' = add_cost_labels_e ind cost_universe e2 in
     61      let b1 = add_cost_label_e ind cost_universe (const_int 1) in
     62      let b2 = add_cost_label_e ind cost_universe (const_int 0) in
    6063      let e3' = Expr (Econdition (e3', b1, b2), int_type) in
    61       let e3' = add_cost_label_e cost_universe e3' in
     64      let e3' = add_cost_label_e ind cost_universe e3' in
    6265      Econdition (e1', e2', e3')
    63   | Efield (e,id) -> Efield (add_cost_labels_e cost_universe e,id)
     66  | Efield (e,id) -> Efield (add_cost_labels_e ind cost_universe e,id)
    6467  | Econdition (e1,e2,e3) ->
    65       let e1' = add_cost_labels_e cost_universe e1 in
    66       let e2' = add_cost_labels_e cost_universe e2 in
    67       let e2' = add_cost_label_e cost_universe e2' in
    68       let e3' = add_cost_labels_e cost_universe e3 in
    69       let e3' = add_cost_label_e cost_universe e3' in
     68      let e1' = add_cost_labels_e ind cost_universe e1 in
     69      let e2' = add_cost_labels_e ind cost_universe e2 in
     70      let e2' = add_cost_label_e ind cost_universe e2' in
     71      let e3' = add_cost_labels_e ind cost_universe e3 in
     72      let e3' = add_cost_label_e ind cost_universe e3' in
    7073      Econdition (e1', e2', e3')
    7174  | Ecost (_,_) | Ecall _ -> assert false (* Should not happen *)
    7275
    73 let add_cost_labels_opt cost_universe = function
    74   | None -> None
    75   | Some e -> Some (add_cost_labels_e cost_universe e)
    76 
    77 let add_cost_labels_lst cost_universe l =
    78   List.map (add_cost_labels_e cost_universe) l
     76let add_cost_labels_opt ind cost_universe =
     77  Option.map (add_cost_labels_e ind cost_universe)
     78
     79let add_cost_labels_lst ind cost_universe l =
     80  List.map (add_cost_labels_e ind cost_universe) l
    7981
    8082
    8183(* Add cost labels to a statement. *)
    8284
    83 let rec add_cost_labels_st cost_universe = function
     85let update_ind i ind =
     86  match i with
     87    | None -> ind
     88    | Some _ -> CostLabel.add_id_indexing ind
     89
     90let rec add_cost_labels_st ind cost_universe = function
    8491  | Sskip -> Sskip
    8592  | Sassign (e1,e2) ->
    86       Sassign (add_cost_labels_e cost_universe e1,
    87                add_cost_labels_e cost_universe e2)
     93    Sassign (add_cost_labels_e ind cost_universe e1,
     94             add_cost_labels_e ind cost_universe e2)
    8895  | Scall (e1,e2,lst) ->
    89       Scall (add_cost_labels_opt cost_universe e1,
    90              add_cost_labels_e cost_universe e2,
    91              add_cost_labels_lst cost_universe lst)
     96    Scall (add_cost_labels_opt ind cost_universe e1,
     97           add_cost_labels_e ind cost_universe e2,
     98           add_cost_labels_lst ind cost_universe lst)
    9299  | Ssequence (s1,s2) ->
    93       Ssequence (add_cost_labels_st cost_universe s1,
    94                  add_cost_labels_st cost_universe s2)
     100    Ssequence (add_cost_labels_st ind cost_universe s1,
     101               add_cost_labels_st ind cost_universe s2)
    95102  | Sifthenelse (e,s1,s2) ->
    96       let s1' = add_cost_labels_st cost_universe s1 in
    97       let s1' = add_starting_cost_label cost_universe s1' in
    98       let s2' = add_cost_labels_st cost_universe s2 in
    99       let s2' = add_starting_cost_label cost_universe s2' in
    100       Sifthenelse (add_cost_labels_e cost_universe e, s1', s2')
    101   | Swhile (e,s) ->
    102       let s' = add_cost_labels_st cost_universe s in
    103       let s' = add_starting_cost_label cost_universe s' in
    104       add_ending_cost_label cost_universe
    105         (Swhile (add_cost_labels_e cost_universe e, s'))
    106   | Sdowhile (e,s) ->
    107       let s = add_cost_labels_st cost_universe s in
    108       let s' = add_starting_cost_label cost_universe s in
    109       add_ending_cost_label cost_universe
    110         (Sdowhile (add_cost_labels_e cost_universe e, s'))
    111   | Sfor (s1,e,s2,s3) ->
    112       let s1' = add_cost_labels_st cost_universe s1 in
    113       let s2' = add_cost_labels_st cost_universe s2 in
    114       let s3' = add_cost_labels_st cost_universe s3 in
    115       let s3' = add_starting_cost_label cost_universe s3' in
    116       add_ending_cost_label cost_universe
    117         (Sfor (s1', add_cost_labels_e cost_universe e, s2', s3'))
    118   | Sreturn e -> Sreturn (add_cost_labels_opt cost_universe e)
     103    let s1' = add_cost_labels_st ind cost_universe s1 in
     104    let s1' = add_starting_cost_label ind cost_universe s1' in
     105    let s2' = add_cost_labels_st ind cost_universe s2 in
     106    let s2' = add_starting_cost_label ind cost_universe s2' in
     107    Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2')
     108  | Swhile (i,e,s) ->
     109    let ind' = update_ind i ind in
     110    let s' = add_cost_labels_st ind' cost_universe s in
     111    let s' = add_starting_cost_label ind' cost_universe s' in
     112      (* exit label indexed with outside indexing *)
     113    add_ending_cost_label ind cost_universe
     114      (Swhile (i,add_cost_labels_e ind cost_universe e, s'))
     115  | Sdowhile (i,e,s) ->
     116    let ind' = update_ind i ind in
     117    let s' = add_cost_labels_st ind' cost_universe s in
     118    let s' = add_starting_cost_label ind' cost_universe s' in
     119    add_ending_cost_label ind cost_universe
     120      (Sdowhile (i,add_cost_labels_e ind cost_universe e, s'))
     121  | Sfor (i,s1,e,s2,s3) ->
     122    let s1' = add_cost_labels_st ind cost_universe s1 in
     123    let ind' = update_ind i ind in
     124    let s2' = add_cost_labels_st ind' cost_universe s2 in
     125    let s3' = add_cost_labels_st ind' cost_universe s3 in
     126    let s3' = add_starting_cost_label ind' cost_universe s3' in
     127    add_ending_cost_label ind cost_universe
     128      (Sfor (i, s1', add_cost_labels_e ind cost_universe e, s2', s3'))
     129  | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e)
    119130  | Sswitch (e,ls) ->
    120       Sswitch (add_cost_labels_e cost_universe e,
    121                add_cost_labels_ls cost_universe ls)
     131    Sswitch (add_cost_labels_e ind cost_universe e,
     132             add_cost_labels_ls ind cost_universe ls)
    122133  | Slabel (lbl,s) ->
    123       let s' = add_cost_labels_st cost_universe s in
    124       let s' = add_starting_cost_label cost_universe s' in
    125       Slabel (lbl,s')
     134    let s' = add_cost_labels_st ind cost_universe s in
     135    let s' = add_starting_cost_label ind cost_universe s' in
     136    Slabel (lbl,s')
    126137  | Scost (_,_) -> assert false
    127138  | _ as stmt -> stmt
    128139
    129 and add_cost_labels_ls cost_universe = function
     140and add_cost_labels_ls ind cost_universe = function
    130141  | LSdefault s ->
    131       let s' = add_cost_labels_st cost_universe s in
    132       let s' = add_starting_cost_label cost_universe s' in
     142      let s' = add_cost_labels_st ind cost_universe s in
     143      let s' = add_starting_cost_label ind cost_universe s' in
    133144      LSdefault s'
    134145  | LScase (i,s,ls) ->
    135       let s' = add_cost_labels_st cost_universe s in
    136       let s' = add_starting_cost_label cost_universe s' in
    137       LScase (i, s', add_cost_labels_ls cost_universe ls)
    138 
    139 
    140 (* Add cost labels to a function. *)
    141 
    142 let add_cost_labels_f cost_universe = function
    143   | (id,Internal fd) -> (id,Internal {
    144       fn_return = fd.fn_return ;
    145       fn_params = fd.fn_params ;
    146       fn_vars = fd.fn_vars ;
    147       fn_body = add_starting_cost_label cost_universe
    148                              (add_cost_labels_st cost_universe fd.fn_body)
    149     })
    150   | (id,External (a,b,c)) -> (id,External (a,b,c))
    151 
     146      let s' = add_cost_labels_st ind cost_universe s in
     147      let s' = add_starting_cost_label ind cost_universe s' in
     148      LScase (i, s', add_cost_labels_ls ind cost_universe ls)
     149
     150
     151(* traversal of code assigning to every label the "loop address" of it. *)
     152(* A loop address like [2, 0, 1] means the corresponding label is in the *)
     153(* third loop inside the first loop inside the second loop of the body. *)
     154let rec assign_loop_addrs_s
     155    (current : int list)
     156    (offset  : int)
     157    (m       : int list Label.Map.t)
     158    : Clight.statement -> int*int list Label.Map.t =
     159  function
     160      (* I am supposing you cannot jump to the update statement of for loops... *)
     161    | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
     162      let (_, m) = assign_loop_addrs_s (offset :: current) 0 m s in
     163      (offset + 1, m)
     164    | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
     165      let (offset, m) = assign_loop_addrs_s current offset m s1 in
     166      assign_loop_addrs_s current offset m s2
     167    | Slabel(l,s) ->
     168      let (offset, m) = assign_loop_addrs_s current offset m s in
     169      (offset, Label.Map.add l current m)
     170    | Sswitch(_,ls) -> assign_loop_addrs_ls current offset m ls
     171    | _ -> (offset, m)
     172
     173and assign_loop_addrs_ls current offset m = function
     174  | LSdefault s -> assign_loop_addrs_s current offset m s
     175  | LScase(_,s,ls) ->
     176    let (offset, m) = assign_loop_addrs_s current offset m s in
     177    assign_loop_addrs_ls current offset m ls
     178
     179let rec is_prefix l1 l2 = match l1, l2 with
     180  | [], _ -> true
     181  | hd1 :: tl1, hd2 :: tl2 when hd1 = hd2 -> is_prefix tl1 tl2
     182  | _ -> false
     183
     184(* traversal of code which for every statement [s] returns the set of loop*)
     185(* addresses which are multi-entry due to a goto in [s]. *)
     186let rec find_multi_entry_loops_s
     187    (m       : int list Label.Map.t)
     188    (current : int list)
     189    (offset  : int)
     190    : Clight.statement -> int*IntListSet.t =
     191  function
     192      (* I am supposing you cannot jump to the update statement of for loops... *)
     193    | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
     194      let current' = offset :: current in
     195      let (_, set) = find_multi_entry_loops_s m current' 0 s in
     196      (offset + 1, set)
     197    | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
     198      let (offset, set1) = find_multi_entry_loops_s m current offset s1 in
     199      let (offset, set2) = find_multi_entry_loops_s m current offset s2 in
     200      (offset, IntListSet.union set1 set2)
     201    | Slabel(_,s) -> find_multi_entry_loops_s m current offset s
     202    | Sgoto l ->
     203        (* all labels should have a binding in m *)
     204      let addr = Label.Map.find l m in
     205      let cond = is_prefix addr current in
     206      let set = if cond then IntListSet.empty else IntListSet.singleton addr in
     207      (offset, set)   
     208    | Sswitch(_,ls) -> find_multi_entry_loops_ls m current offset ls
     209    | _ -> (offset, IntListSet.empty)
     210
     211and find_multi_entry_loops_ls m current offset = function
     212  | LSdefault s -> find_multi_entry_loops_s m current offset s
     213  | LScase(_,s,ls) ->
     214    let (offset, set1) = find_multi_entry_loops_s m current offset s in
     215    let (offset, set2) = find_multi_entry_loops_ls m current offset ls in
     216    (offset, IntListSet.union set1 set2)
     217     
     218(* final pass where loops are indexed *)
     219let rec index_loops_s multi_entry current offset depth = function
     220  (* I am supposing you cannot jump to the update statement of for loops... *)
     221  | Swhile(_,b,s) ->
     222    let current' = offset :: current in
     223    let is_bad = IntListSet.mem current' multi_entry in
     224    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in
     225    let (_, s) = index_loops_s multi_entry current' 0 depth s in
     226    (offset + 1, Swhile(i,b,s))
     227  | Sdowhile(_,b,s) ->
     228    let current' = offset :: current in
     229    let is_bad = IntListSet.mem current' multi_entry in
     230    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in
     231    let (_, s) = index_loops_s multi_entry current' 0 depth s in
     232    (offset + 1, Sdowhile(i,b,s))
     233  | Sfor(_,a1,a2,a3,s) ->
     234    let current' = offset :: current in
     235    let is_bad = IntListSet.mem current' multi_entry in
     236    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in
     237    let (_, s) = index_loops_s multi_entry current' 0 depth s in
     238    (offset + 1, Sfor(i,a1,a2,a3,s))
     239  | Ssequence(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, Ssequence(s1,s2))
     243  | Sifthenelse(b,s1,s2) ->
     244    let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
     245    let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
     246    (offset, Sifthenelse(b,s1,s2))
     247  | Slabel(l,s) ->
     248    let (offset, s) = index_loops_s multi_entry current offset depth s in
     249    (offset, Slabel(l, s))
     250  | Sswitch(v,ls) ->
     251    let (offset, s) = index_loops_ls multi_entry current offset depth ls in
     252    (offset, Sswitch(v, ls))
     253  | _ as s -> (offset, s)
     254
     255and index_loops_ls multi_entry current offset depth = function
     256  | LSdefault s ->
     257    let (offset, s) =
     258      index_loops_s multi_entry current offset depth s in
     259    (offset, LSdefault s)
     260  | LScase(v,s,ls) ->
     261    let (offset, s) = index_loops_s multi_entry current offset depth s in
     262    let (offset, ls) = index_loops_ls multi_entry current offset depth ls in
     263    (offset, LScase(v,s,ls))
     264
     265(* Index loops and introduce cost labels in functions *)
     266let process_f cost_universe = function
     267  | (id,Internal fd) ->
     268    let body = fd.fn_body in
     269    (* assign loop addresses to labels *)
     270    let (_, m) = assign_loop_addrs_s [] 0 Label.Map.empty body in
     271    (* find which loops are potentially multi-entry *)
     272    let (_, multi_entry) = find_multi_entry_loops_s m [] 0 body in
     273    (* index loops accordingly *)
     274    let (_, body) = index_loops_s multi_entry [] 0 0 body in
     275    (* initialize indexing *)
     276    let ind = CostLabel.empty_indexing in
     277    (* add cost labels inside *)
     278    let body = add_cost_labels_st ind cost_universe body in
     279    (* add cost label in front *)
     280    let body = add_starting_cost_label ind cost_universe body in
     281    (id,Internal {fd with fn_body = body})
     282  | _ as x -> x
     283       
     284         
    152285
    153286(** [add_cost_labels prog] inserts some labels to enable
     
    156289let add_cost_labels p =
    157290  let labs = ClightAnnotator.all_labels p in
    158   let labs = StringTools.Set.fold CostLabel.Set.add labs CostLabel.Set.empty in
    159   let cost_prefix = CostLabel.Gen.fresh_prefix labs "_cost" in
    160   let cost_universe = CostLabel.Gen.new_universe cost_prefix in
    161   {
    162     prog_funct = List.map (add_cost_labels_f cost_universe) p.prog_funct;
    163     prog_main = p.prog_main;
    164     prog_vars = p.prog_vars
    165   }
     291  let add = CostLabel.Atom.Set.add in
     292  let empty = CostLabel.Atom.Set.empty in
     293  let labs = StringTools.Set.fold add labs empty in
     294  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
     295  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
     296  {p with prog_funct = List.map (process_f cost_universe) p.prog_funct}
  • Deliverables/D2.2/8051/src/clight/clightParser.mli

    r1462 r1542  
    1 
    21(** This module implements a parser for [C] based on [gcc] and
    32    [CIL]. *)
  • Deliverables/D2.2/8051/src/clight/clightPrinter.ml

    r818 r1542  
    196196  | Efield(e1, id) ->
    197197      fprintf p "%a.%s" print_expr_prec (level, e1) id
    198   | Ecost (lbl,e1) ->
    199       fprintf p "(/* %s */ %a)" lbl print_expr e1
    200   | Ecall (f, arg, e) ->
     198  | Ecost(lbl, e1) ->
     199    (* printing label uglily even if in comment for consistence *)
     200    let lbl = CostLabel.string_of_cost_label lbl in
     201    fprintf p "(/* %s */ %a)" lbl print_expr e1
     202  | Ecall(f, arg, e) ->
    201203      fprintf p "(%s(%a), %a)" f print_expr arg print_expr e
    202204
     
    214216      print_expr p e1;
    215217      print_expr_list p (false, et)
     218
     219let print_loop_depth p = function
     220  | None -> fprintf p ""
     221  | Some x -> fprintf p "/* single entry loop depth: %d */@," x
    216222
    217223let rec print_stmt p s =
     
    241247              print_stmt s1
    242248              print_stmt s2
    243   | Swhile(e, s) ->
    244       fprintf p "@[<v 2>while (%a) {@ %a@;<0 -2>}@]"
    245               print_expr e
    246               print_stmt s
    247   | Sdowhile(e, s) ->
    248       fprintf p "@[<v 2>do {@ %a@;<0 -2>} while(%a);@]"
    249               print_stmt s
    250               print_expr e
    251   | Sfor(s_init, e, s_iter, s_body) ->
    252       fprintf p "@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]"
    253               print_stmt_for s_init
    254               print_expr e
    255               print_stmt_for s_iter
    256               print_stmt s_body
     249  | Swhile(i, e, s) ->
     250    fprintf p "@[<v 0>%a@[<v 2>while (%a) {@ %a@;<0 -2>}@]@]"
     251      print_loop_depth i
     252      print_expr e
     253      print_stmt s
     254  | Sdowhile(i, e, s) ->
     255    fprintf p "@[<v 0>%a@[<v 2>do {@ %a@;<0 -2>} while(%a);@]@]"
     256      print_loop_depth i
     257      print_stmt s
     258      print_expr e
     259  | Sfor(i, s_init, e, s_iter, s_body) ->
     260    fprintf p "@[<v 0>%a@[<v 2>for (@[<hv 0>%a;@ %a;@ %a) {@]@ %a@;<0 -2>}@]@]"
     261      print_loop_depth i
     262      print_stmt_for s_init
     263      print_expr e
     264      print_stmt_for s_iter
     265      print_stmt s_body
    257266  | Sbreak ->
    258       fprintf p "break;"
     267    fprintf p "break;"
    259268  | Scontinue ->
    260       fprintf p "continue;"
     269    fprintf p "continue;"
    261270  | Sswitch(e, cases) ->
    262       fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
    263               print_expr e
    264               print_cases cases
     271    fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
     272      print_expr e
     273      print_cases cases
    265274  | Sreturn None ->
    266       fprintf p "return;"
     275    fprintf p "return;"
    267276  | Sreturn (Some e) ->
    268       fprintf p "return %a;" print_expr e
     277    fprintf p "return %a;" print_expr e
    269278  | Slabel(lbl, s1) ->
    270       fprintf p "%s:@ %a" lbl print_stmt s1
     279    fprintf p "%s:@ %a" lbl print_stmt s1
    271280  | Sgoto lbl ->
    272       fprintf p "goto %s;" lbl
    273  | Scost (lbl,s1) ->
     281    fprintf p "goto %s;" lbl
     282  | Scost (lbl,s1) ->
     283    let lbl = CostLabel.string_of_cost_label lbl in
    274284     fprintf p "%s:@ %a" lbl print_stmt s1
    275285
     
    468478  | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2
    469479  | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2
    470   | Swhile(e, s) -> collect_expr e; collect_stmt s
    471   | Sdowhile(e, s) -> collect_stmt s; collect_expr e
    472   | Sfor(s_init, e, s_iter, s_body) ->
    473       collect_stmt s_init; collect_expr e;
    474       collect_stmt s_iter; collect_stmt s_body
     480  | Swhile(_, e, s) -> collect_expr e; collect_stmt s
     481  | Sdowhile(_, e, s) -> collect_stmt s; collect_expr e
     482  | Sfor(_, s_init, e, s_iter, s_body) ->
     483    collect_stmt s_init; collect_expr e;
     484    collect_stmt s_iter; collect_stmt s_body
    475485  | Sbreak -> ()
    476486  | Scontinue -> ()
  • Deliverables/D2.2/8051/src/clight/clightToCminor.ml

    r1462 r1542  
    495495    AST.res = ret_type }
    496496
    497 let f_stmt fresh var_locs stmt sub_exprs_res sub_stmts_res =
    498   let (tmps, sub_stmts_res) = List.split sub_stmts_res in
    499   let tmps = List.flatten tmps in
    500 
    501   let (added_tmps, stmt) = match stmt, sub_exprs_res, sub_stmts_res with
    502 
    503     | Clight.Sskip, _, _ -> ([], Cminor.St_skip)
    504 
    505     | Clight.Sassign (e1, _), _ :: e2 :: _, _ ->
     497let ind_0 i stmt = match i with
     498  | None -> stmt
     499  | Some x -> Cminor.St_ind_0(x, stmt)
     500
     501let ind_inc i stmt = match i with
     502  | None -> stmt
     503  | Some x -> Cminor.St_ind_inc(x, stmt)
     504
     505let trans_for =
     506  let f_expr e _ = e in
     507  let f_stmt stmt expr_res stmt_res = match expr_res, stmt_res, stmt with
     508    | e::_, s1::s2::s3::_, Clight.Sfor(i,_,_,_,_) ->
     509      Clight.Ssequence(s1,Clight.Swhile(i,e,
     510                                        Clight.Ssequence(s3, s2)))
     511    | exprs, sub_sts, stm ->
     512      ClightFold.statement_fill_subs stm exprs sub_sts in
     513  ClightFold.statement2 f_expr f_stmt
     514
     515let cmp_complement = function
     516  | AST.Cmp_eq -> AST.Cmp_ne
     517  | AST.Cmp_ne -> AST.Cmp_eq
     518  | AST.Cmp_gt -> AST.Cmp_le
     519  | AST.Cmp_ge -> AST.Cmp_lt
     520  | AST.Cmp_lt -> AST.Cmp_ge
     521  | AST.Cmp_le -> AST.Cmp_gt
     522
     523let negate_expr (Cminor.Expr (_, et) as e) =
     524  let ed' = Cminor.Op1 (AST.Op_notbool, e) in
     525  Cminor.Expr(ed', et)
     526
     527let rec translate_stmt fresh var_locs cnt_lbl br_lbl = function
     528
     529    | Clight.Sskip -> ([], Cminor.St_skip)
     530
     531    | Clight.Sassign (e1, e2) ->
     532      let e2 = translate_expr var_locs e2 in
    506533      ([], assign var_locs e1 e2)
    507534
    508     | Clight.Scall (None, _, _), f :: args, _ ->
     535    | Clight.Scall (None, f, args) ->
     536      let f = translate_expr var_locs f in
     537      let args = List.map (translate_expr var_locs) args in
    509538      ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args))
    510539
    511     | Clight.Scall (Some e, _, _), _ :: f :: args, _ ->
     540    | Clight.Scall (Some e, f, args) ->
     541      let f = translate_expr var_locs f in
     542      let args = List.map (translate_expr var_locs) args in
    512543      let t = sig_type_of_ctype (clight_type_of e) in
    513544      let tmp = fresh () in
     
    518549      ([(tmp, t)], Cminor.St_seq (stmt_call, stmt_assign))
    519550
    520     | Clight.Swhile _, e :: _, stmt :: _ ->
    521       let econd =
    522         Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
     551    | Clight.Swhile (i,e,stmt) ->
     552      let loop_lbl = fresh () in
     553      let llbl_opt = Some loop_lbl in
     554      let exit_lbl = fresh () in
     555      let elbl_opt = Some exit_lbl in
     556      let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in
     557      let e = translate_expr var_locs e in
     558      let jmp lbl = Cminor.St_goto lbl in
     559      (* let econd = negate_expr e in *)
    523560      let scond =
    524         Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
    525       ([],
    526        Cminor.St_block (Cminor.St_loop (Cminor.St_seq (scond,
    527                                                        Cminor.St_block stmt))))
    528 
    529     | Clight.Sdowhile _, e :: _, stmt :: _ ->
    530       let econd =
    531         Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
     561        Cminor.St_ifthenelse (e, Cminor.St_skip, jmp exit_lbl) in
     562      let loop =
     563        Cminor.St_seq(scond,Cminor.St_seq (stmt, ind_inc i (jmp loop_lbl))) in
     564      let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in
     565      (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip)))
     566       
     567    | Clight.Sdowhile (i,e,stmt) ->
     568      let loop_lbl = fresh () in
     569      let llbl_opt = Some loop_lbl in
     570      let exit_lbl = fresh () in
     571      let elbl_opt = Some exit_lbl in
     572      let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in
     573      let e = translate_expr var_locs e in
     574      let jmp lbl = Cminor.St_goto lbl in
    532575      let scond =
    533         Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
    534       ([],
    535        Cminor.St_block (Cminor.St_loop (Cminor.St_seq (Cminor.St_block stmt,
    536                                                        scond))))
    537 
    538     | Clight.Sfor _, e :: _, stmt1 :: stmt2 :: stmt3 :: _ ->
    539       let econd =
    540         Cminor.Expr (Cminor.Op1 (AST.Op_notbool, e), cminor_type_of e) in
    541       let scond =
    542         Cminor.St_ifthenelse (econd, Cminor.St_exit 0, Cminor.St_skip) in
    543       let body = Cminor.St_seq (Cminor.St_block stmt3, stmt2) in
    544       ([],
    545        Cminor.St_seq (stmt1,
    546                       Cminor.St_block
    547                         (Cminor.St_loop (Cminor.St_seq (scond, body)))))
    548 
    549     | Clight.Sifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
    550       ([], Cminor.St_ifthenelse (e, stmt1, stmt2))
    551 
    552     | Clight.Ssequence _, _, stmt1 :: stmt2 :: _ ->
    553       ([], Cminor.St_seq (stmt1, stmt2))
    554 
    555     | Clight.Sbreak, _, _ -> ([], Cminor.St_exit 1)
    556 
    557     | Clight.Scontinue, _, _ -> ([], Cminor.St_exit 0)
    558 
    559     | Clight.Sswitch _, _, _ ->
     576        Cminor.St_ifthenelse (e, ind_inc i (jmp loop_lbl), Cminor.St_skip) in
     577      let loop =
     578        Cminor.St_seq (stmt, scond) in
     579      let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in
     580      (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip)))
     581       
     582    | Clight.Sfor _ -> assert false (* transformed *)
     583
     584    | Clight.Sifthenelse (e, stmt1, stmt2) ->
     585      let (tmps1, stmt1) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt1 in
     586      let (tmps2, stmt2) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt2 in
     587      let e = translate_expr var_locs e in
     588      (tmps1 @ tmps2, Cminor.St_ifthenelse (e, stmt1, stmt2))
     589
     590    | Clight.Ssequence(stmt1,stmt2) ->
     591      let (tmps1, stmt1) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt1 in
     592      let (tmps2, stmt2) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt2 in
     593      (tmps1 @ tmps2, Cminor.St_seq (stmt1, stmt2))
     594
     595    | Clight.Sbreak ->
     596      let br_lbl = match br_lbl with
     597        | Some x -> x
     598        | None -> invalid_arg("break without enclosing scope") in
     599      ([], Cminor.St_goto br_lbl)
     600
     601    | Clight.Scontinue ->
     602      let cnt_lbl = match cnt_lbl with
     603        | Some x -> x
     604        | None -> invalid_arg("continue without enclosing scope") in
     605      ([], Cminor.St_goto cnt_lbl)
     606    | Clight.Sswitch _ ->
    560607      (* Should not appear because of switch transformation performed
    561608         beforehand. *)
    562609      assert false
    563610
    564     | Clight.Sreturn None, _, _ -> ([], Cminor.St_return None)
    565 
    566     | Clight.Sreturn (Some _), e :: _, _ -> ([], Cminor.St_return (Some e))
    567 
    568     | Clight.Slabel (lbl, _), _, stmt :: _ -> ([], Cminor.St_label (lbl, stmt))
    569 
    570     | Clight.Sgoto lbl, _, _ -> ([], Cminor.St_goto lbl)
    571 
    572     | Clight.Scost (lbl, _), _, stmt :: _ -> ([], Cminor.St_cost (lbl, stmt))
    573 
    574     | _ -> assert false (* type error *) in
    575 
    576   (tmps @ added_tmps, stmt)
    577 
    578 let translate_statement fresh var_locs =
    579   ClightFold.statement2 (f_expr var_locs) (f_stmt fresh var_locs)
     611    | Clight.Sreturn None -> ([], Cminor.St_return None)
     612
     613    | Clight.Sreturn (Some e) ->
     614      let e = translate_expr var_locs e in
     615      ([], Cminor.St_return (Some e))
     616
     617    | Clight.Slabel (lbl, stmt) ->
     618      let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
     619      (tmps, Cminor.St_label (lbl, stmt))
     620
     621    | Clight.Sgoto lbl -> ([], Cminor.St_goto lbl)
     622
     623    | Clight.Scost (lbl, stmt) ->
     624      let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
     625      (tmps, Cminor.St_cost (lbl, stmt))
     626
     627(*    | _ -> assert false (* type error *) *)
    580628
    581629
     
    598646  let params =
    599647    List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in
    600   let (tmps, body) = translate_statement fresh var_locs cfun.Clight.fn_body in
     648  let body = cfun.Clight.fn_body in
     649  let body = trans_for body in
     650  let (tmps, body) = translate_stmt fresh var_locs None None body in
    601651  let body = add_stack_parameters_initialization var_locs body in
    602652  { Cminor.f_return = type_return_of_ctype cfun.Clight.fn_return ;
  • Deliverables/D2.2/8051/src/cminor/cminor.mli

    r818 r1542  
    3434  | St_seq of statement * statement
    3535  | St_ifthenelse of expression * statement * statement
    36   | St_loop of statement
     36(*  | St_loop of statement
    3737  | St_block of statement
    38   | St_exit of int
     38  | St_exit of int *)
    3939
    4040  (* Switch. Parameters are the expression whose value is switch, a
    41      table of cases and their corresponding number of blocks to exit,
    42      and the number of block to exit in the default case. *)
    43   | St_switch of expression * (int*int) list * int
     41     table of cases and their corresponding labels to go to,
     42     and the label to go to in the default case. *)
     43  | St_switch of expression * (int*Label.t) list * Label.t
    4444
    4545  | St_return of expression option
    4646  | St_label of AST.ident * statement
    47   | St_goto of string
     47  | St_goto of Label.t
    4848  | St_cost of CostLabel.t * statement
     49  | St_ind_0 of CostLabel.index * statement
     50  | St_ind_inc of CostLabel.index * statement
    4951
    5052
  • Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml

    r818 r1542  
    204204let all_labels p =
    205205  let (cost_labels, user_labels) = prog_labels p in
    206   let all =
    207     CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
    208       cost_labels StringTools.Set.empty in
     206  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     207  let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
    209208  Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all
  • Deliverables/D2.2/8051/src/cminor/cminorFold.ml

    r818 r1542  
    3131
    3232let statement_subs = function
    33   | Cminor.St_skip | Cminor.St_exit _ | Cminor.St_return None
     33  | Cminor.St_skip | (*Cminor.St_exit _ |*) Cminor.St_return None
    3434  | Cminor.St_goto _ -> ([], [])
    3535  | Cminor.St_assign (_, e) | Cminor.St_switch (e, _, _)
     
    4343  | Cminor.St_ifthenelse (e, stmt1, stmt2) ->
    4444    ([e], [stmt1 ; stmt2])
    45   | Cminor.St_loop stmt | Cminor.St_block stmt
    46   | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt) ->
     45  (*| Cminor.St_loop stmt | Cminor.St_block stmt *)
     46  | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt)
     47  | Cminor.St_ind_0 (_, stmt) | Cminor.St_ind_inc (_, stmt) ->
    4748    ([], [stmt])
    4849
    4950let statement_fill_subs stmt sub_es sub_stmts =
    5051  match stmt, sub_es, sub_stmts with
    51     | (  Cminor.St_skip | Cminor.St_exit _ | Cminor.St_return None
     52    | (  Cminor.St_skip | (*Cminor.St_exit _ |*) Cminor.St_return None
    5253       | Cminor.St_goto _), _, _ -> stmt
    5354    | Cminor.St_assign (x, _), e :: _, _ ->
     
    6768    | Cminor.St_ifthenelse _, e :: _, stmt1 :: stmt2 :: _ ->
    6869      Cminor.St_ifthenelse (e, stmt1, stmt2)
    69     | Cminor.St_loop _, _, stmt :: _ ->
     70 (*   | Cminor.St_loop _, _, stmt :: _ ->
    7071      Cminor.St_loop stmt
    7172    | Cminor.St_block _, _, stmt :: _ ->
    72       Cminor.St_block stmt
     73      Cminor.St_block stmt *)
    7374    | Cminor.St_label (lbl, _), _, stmt :: _ ->
    7475      Cminor.St_label (lbl, stmt)
    7576    | Cminor.St_cost (lbl, _), _, stmt :: _ ->
    7677      Cminor.St_cost (lbl, stmt)
     78    | Cminor.St_ind_0 (i, _), _, stmt :: _ ->
     79      Cminor.St_ind_0 (i, stmt)
     80    | Cminor.St_ind_inc (i, _), _, stmt :: _ ->
     81      Cminor.St_ind_inc (i, stmt)
    7782    | _ -> assert false (* do not use on these arguments *)
    7883
  • Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml

    r1462 r1542  
    2323(* State of execution *)
    2424
     25type indexing = CostLabel.const_indexing
     26
    2527type continuation =
    2628    Ct_stop
    2729  | Ct_cont of statement*continuation
    28   | Ct_endblock of continuation
     30(*  | Ct_endblock of continuation *)
    2931  | Ct_returnto of
    3032      ident option*internal_function*Val.address*local_env*continuation
     
    3234type state =
    3335    State_regular of
    34       internal_function*statement*continuation*Val.address*local_env*(function_def Mem.memory)
    35   | State_call of function_def*Val.t list*continuation*(function_def Mem.memory)
    36   | State_return of Val.t*continuation*(function_def Mem.memory)
     36      internal_function*statement*continuation*Val.address*local_env*
     37                         (function_def Mem.memory)*indexing list
     38  | State_call of function_def*Val.t list*continuation*
     39             (function_def Mem.memory)*indexing list
     40  | State_return of Val.t*continuation*(function_def Mem.memory)*indexing list
    3741
    3842let string_of_local_env lenv =
     
    5761  | St_seq _ -> "sequence"
    5862  | St_ifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
    59   | St_loop _ -> "loop"
     63(*  | St_loop _ -> "loop"
    6064  | St_block _ -> "block"
    61   | St_exit n -> "exit " ^ (string_of_int n)
     65  | St_exit n -> "exit " ^ (string_of_int n) *)
    6266  | St_switch (e, _, _) -> "switch (" ^ (string_of_expr e) ^ ")"
    6367  | St_return None -> "return"
     
    6569  | St_label (lbl, _) -> "label " ^ lbl
    6670  | St_goto lbl -> "goto " ^ lbl
    67   | St_cost (lbl, _) -> "cost " ^ lbl
     71  | St_cost (lbl, _) ->
     72    let lbl = CostLabel.string_of_cost_label lbl in
     73    "cost " ^ lbl
     74  | St_ind_0 (i, _) -> "reset " ^ string_of_int i ^ " to 0"
     75  | St_ind_inc (i, _) -> "post-increment " ^ string_of_int i
    6876
    6977let 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%!"
     78  | State_regular (_, stmt, _, sp, lenv, mem, i) ->
     79    Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\nIndexing:"
    7280      (string_of_local_env lenv)
    7381      (Mem.to_string mem)
    74       (Val.to_string (value_of_address sp))
     82      (Val.to_string (value_of_address sp));
     83    let ind = CostLabel.curr_const_ind i in
     84    CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) ind;
     85    Printf.printf "\nRegular state: %s\n\n%!"
    7586      (string_of_statement stmt)
    76   | State_call (_, args, _, mem) ->
     87  | State_call (_, args, _, mem,_) ->
    7788    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
    7889      (Mem.to_string mem)
    7990      (MiscPottier.string_of_list " " Val.to_string args)
    80   | State_return (v, _, mem) ->
     91  | State_return (v, _, mem,_) ->
    8192    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    8293      (Mem.to_string mem)
     
    221232
    222233let rec callcont = function
    223     Ct_stop                     -> Ct_stop
    224   | Ct_cont(_,k)                -> callcont k
    225   | Ct_endblock(k)              -> callcont k
    226   | Ct_returnto(a,b,c,d,e)      -> Ct_returnto(a,b,c,d,e)
     234  | Ct_cont(_,k) (*| Ct_endblock k *) -> callcont k
     235  | (Ct_stop | Ct_returnto _) as k -> k
    227236
    228237let findlabel lbl st k =
     
    243252         | Some(v) -> Some(v)
    244253      )
    245   | St_loop(s)                     -> fdlbl (Ct_cont(St_loop(s),k)) s
    246   | St_block(s)                    -> fdlbl (Ct_endblock(k)) s
    247   | St_exit(_)                     -> None
    248   | St_switch(_,_,_)               -> None
    249   | St_return(_)                   -> None
    250   | St_label(l,s) when l = lbl     -> Some((s,k))
    251   | St_goto(_)                     -> None
    252   | St_cost (_,s) | St_label (_,s) -> fdlbl k s
     254(*  | St_loop(s)                  -> fdlbl (Ct_cont(St_loop(s),k)) s
     255  | St_block(s)                 -> fdlbl (Ct_endblock(k)) s
     256  | St_exit(_)                  -> None *)
     257  | St_switch(_,_,_)            -> None
     258  | St_return(_)                -> None
     259  | St_label(l,s) when l = lbl  -> Some((s,k))
     260  | St_goto(_)                  -> None
     261  | St_cost(_,s)  | St_label(_,s)
     262  | St_ind_0(_,s) | St_ind_inc(_,s) -> fdlbl k s
    253263  in match fdlbl k st with
    254264      None -> assert false (*Wrong label*)
     
    256266
    257267
    258 let call_state sigma e m f params cont =
     268let call_state sigma e m i f params cont =
    259269  let (addr,l1) = eval_expression sigma e m f in
    260270  let fun_def = Mem.find_fun_def m (address_of_value addr) in
    261271  let (args,l2) = eval_exprlist sigma e m params in
    262   (State_call(fun_def,args,cont,m),l1@l2)
    263 
    264 let eval_stmt f k sigma e m s = match s, k with
    265   | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m),[])
    266   | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[])
     272  (State_call(fun_def,args,cont,m,i),l1@l2)
     273
     274let eval_stmt f k sigma e m i s = match s, k with
     275  | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m, i),[])
     276(*  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m, i),[]) *)
    267277  | St_skip, (Ct_returnto _ as k) ->
    268     (State_return (Val.undef,k,Mem.free m sigma),[])
     278    (State_return (Val.undef,k,Mem.free m sigma,i),[])
    269279  | St_skip,Ct_stop ->
    270     (State_return (Val.undef,Ct_stop,Mem.free m sigma),[])
     280    (State_return (Val.undef,Ct_stop,Mem.free m sigma,i),[])
    271281  | St_assign(x,exp),_ ->
    272282    let (v,l) = eval_expression sigma e m exp in
    273283    let e = LocalEnv.add x v e in
    274     (State_regular(f, St_skip, k, sigma, e, m),l)
     284    (State_regular(f, St_skip, k, sigma, e, m, i),l)
    275285  | St_store(q,a1,a2),_ ->
    276286    let (v1,l1) = eval_expression sigma e m a1 in
    277287    let (v2,l2) = eval_expression sigma e m a2 in
    278288    let m = Mem.storeq m q (address_of_value v1) v2 in
    279     (State_regular(f, St_skip, k, sigma, e, m),l1@l2)
     289    (State_regular(f, St_skip, k, sigma, e, m, i),l1@l2)
    280290  | St_call(xopt,f',params,_),_ ->
    281     call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,k))
     291    call_state sigma e m i f' params (Ct_returnto(xopt,f,sigma,e,k))
    282292  | St_tailcall(f',params,_),_ ->
    283     call_state sigma e m f' params (callcont k)
    284   | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
     293    call_state sigma e m i f' params (callcont k)
     294  | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m, i),[])
    285295  | St_ifthenelse(exp,s1,s2),_ ->
    286296    let (v,l) = eval_expression sigma e m exp in
     
    290300        if Val.is_false v then s2
    291301        else error "undefined conditional value." in
    292       (State_regular(f,next_stmt,k,sigma,e,m),l)
    293   | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
    294   | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
    295   | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m),[])
    296   | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m),[])
     302      (State_regular(f,next_stmt,k,sigma,e,m,i),l)
     303(*  | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m,i),[])
     304  | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m,i),[])
     305  | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m,i),[])
     306  | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m,i),[])
    297307  | St_exit(n),Ct_endblock(k) ->
    298     (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
    299   | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m),[])
    300   | St_goto(lbl),_ -> 
     308    (State_regular(f,(St_exit (n-1)),k,sigma,e,m,i),[]) *)
     309  | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m,i),[])
     310  | St_goto(lbl),_ ->
    301311    let (s2,k2) = findlabel lbl f.f_body (callcont k) in
    302     (State_regular(f,s2,k2,sigma,e,m),[])
     312    (State_regular(f,s2,k2,sigma,e,m,i),[])
    303313  | St_switch(exp,lst,def),_ ->
    304314    let (v,l) = eval_expression sigma e m exp in
    305315    if Val.is_int v then
    306316      try
    307         let i = Val.to_int v in
    308         let nb_exit =
    309           if List.mem_assoc i lst then List.assoc i lst
    310           else def in
    311         (State_regular(f, St_exit nb_exit,k, sigma, e, m),l)
     317        let v = Val.to_int v in
     318        let lbl =
     319          try
     320            List.assoc v lst
     321          with
     322            | Not_found -> def in
     323        let (s',k') = findlabel lbl f.f_body (callcont k) in
     324        (State_regular(f, s', k', sigma, e, m, i),l)
    312325      with _ -> error "int value too big."
    313326    else error "undefined switch value."
    314327  | St_return(None),_ ->
    315     (State_return (Val.undef,callcont k,Mem.free m sigma),[])
     328    (State_return (Val.undef,callcont k,Mem.free m sigma,i),[])
    316329  | St_return(Some(a)),_ ->
    317330      let (v,l) = eval_expression sigma e m a in
    318       (State_return (v,callcont k,Mem.free m sigma),l)
    319   | St_cost(lbl,s),_ -> (State_regular(f,s,k,sigma,e,m),[lbl])
    320   | _ -> error "state malformation."
     331      (State_return (v,callcont k,Mem.free m sigma,i),l)
     332  | St_cost(lbl,s),_ ->
     333    (* applying current indexing on label *)
     334    let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind i) lbl in
     335    (State_regular(f,s,k,sigma,e,m,i),[lbl])
     336  | St_ind_0(ind,s),_ ->
     337    CostLabel.enter_loop i ind;
     338    (State_regular(f,s,k,sigma,e,m,i), [])
     339  | St_ind_inc(ind,s),_ ->
     340    CostLabel.continue_loop i ind;
     341    (State_regular(f,s,k,sigma,e,m,i), [])
     342(*  | _ -> error "state malformation." *)
    321343
    322344
    323345module InterpretExternal = Primitive.Interpret (Mem)
    324346
    325 let interpret_external k mem f args =
     347let interpret_external k mem i f args =
    326348  let (mem', v) = match InterpretExternal.t mem f args with
    327349    | (mem', InterpretExternal.V vs) ->
     
    329351      (mem', v)
    330352    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    331   State_return (v, k, mem')
    332 
    333 let step_call vargs k m = function
     353  State_return (v, k, mem', i)
     354
     355let step_call vargs k m i = function
    334356  | F_int f ->
    335357    let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in
    336358    let lenv = init_local_env vargs f.f_params f.f_vars in
    337     State_regular(f,f.f_body,k,sp,lenv,m)
    338   | F_ext f -> interpret_external k m f.ef_tag vargs
     359    let i = CostLabel.new_const_ind i in
     360    State_regular(f,f.f_body,k,sp,lenv,m,i)
     361  | F_ext f -> interpret_external k m i f.ef_tag vargs
    339362
    340363let step = function
    341   | State_regular(f,stmt,k,sp,e,m) -> eval_stmt f k sp e m stmt
    342   | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    343   | State_return(v,Ct_returnto(None,f,sigma,e,k),m) ->
    344     (State_regular(f,St_skip,k,sigma,e,m),[])
    345   | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m) ->
     364  | State_regular(f,stmt,k,sp,e,m,i) -> eval_stmt f k sp e m i stmt
     365  | State_call(fun_def,vargs,k,m,i) -> (step_call vargs k m i fun_def,[])
     366  | State_return(v,Ct_returnto(None,f,sigma,e,k),m,i) ->
     367    let i = CostLabel.forget_const_ind i in
     368    (State_regular(f,St_skip,k,sigma,e,m,i),[])
     369  | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m,i) ->
    346370    let e = LocalEnv.add x v e in
    347     (State_regular(f,St_skip,k,sigma,e,m),[])
     371    let i = CostLabel.forget_const_ind i in
     372    (State_regular(f,St_skip,k,sigma,e,m,i),[])
    348373  | _ -> error "state malformation."
    349374
     
    364389    if debug then Printf.printf "Result = %s\n%!"
    365390      (IntValue.Int32.to_string res) ;
    366     (res, cost_labels) in
     391    (res, List.rev cost_labels) in
    367392  if debug then print_state state ;
    368393  match state with
    369     | State_return(v,Ct_stop,_) -> (* Explicit return in main *)
     394    | State_return(v,Ct_stop,_,_) -> (* Explicit return in main *)
    370395      print_and_return_result (compute_result v)
    371     | State_regular(_,St_skip,Ct_stop,_,_,_) -> (* Implicit return in main *)
     396    | State_regular(_,St_skip,Ct_stop,_,_,_,_) -> (* Implicit return in main *)
    372397      print_and_return_result IntValue.Int32.zero
    373398    | state -> exec debug cost_labels (step state)
     
    379404    | Some main ->
    380405      let mem = init_mem prog in
    381       let first_state = (State_call (find_fundef main mem,[],Ct_stop,mem),[]) in
     406      let main = find_fundef main mem in
     407      let first_state = (State_call (main,[],Ct_stop,mem,[]),[]) in
    382408      exec debug [] first_state
  • Deliverables/D2.2/8051/src/cminor/cminorPrinter.ml

    r818 r1542  
    116116        (add_parenthesis e3)
    117117  | Cminor.Exp_cost (lab, e) ->
     118      let lab = CostLabel.string_of_cost_label lab in
    118119      Printf.sprintf "/* %s */ %s" lab (print_expression e)
    119120and add_parenthesis (Cminor.Expr (ed, _) as e) = match ed with
     
    136137let print_table n =
    137138  let f s (case, exit) =
    138     Printf.sprintf "%s%scase %d: exit %d;\n" s (n_spaces n) case exit
     139    Printf.sprintf "%s%scase %d: goto %s;\n" s (n_spaces n) case exit
    139140  in
    140141  List.fold_left f ""
     
    171172        (Primitive.print_sig sg)
    172173  | Cminor.St_seq (s1, s2) -> (print_body n s1) ^ (print_body n s2)
     174  | Cminor.St_ifthenelse (e, s1, Cminor.St_skip) ->
     175    Printf.sprintf "%sif (%s) {\n%s%s}\n"
     176    (n_spaces n)
     177    (print_expression e)
     178    (print_body (n+2) s1)
     179    (n_spaces n)
    173180  | Cminor.St_ifthenelse (e, s1, s2) ->
    174181      Printf.sprintf "%sif (%s) {\n%s%s}\n%selse {\n%s%s}\n"
     
    180187        (print_body (n+2) s2)
    181188        (n_spaces n)
    182   | Cminor.St_loop s ->
     189(*  | Cminor.St_loop s ->
    183190      Printf.sprintf "%sloop {\n%s%s}\n"
    184191        (n_spaces n)
     
    191198        (n_spaces n)
    192199  | Cminor.St_exit i ->
    193       Printf.sprintf "%sexit %d;\n" (n_spaces n) i
     200      Printf.sprintf "%sexit %d;\n" (n_spaces n) i *)
    194201  | Cminor.St_switch (e, tbl, dflt) ->
    195       Printf.sprintf "%sswitch (%s) {\n%s%sdefault: exit %d;\n%s}\n"
     202      Printf.sprintf "%sswitch (%s) {\n%s%sdefault: goto %s;\n%s}\n"
    196203        (n_spaces n)
    197204        (print_expression e)
     
    208215      Printf.sprintf "%sgoto %s;\n" (n_spaces n) lbl
    209216  | Cminor.St_cost (lbl, s) ->
    210       Printf.sprintf "%s%s:\n%s"
    211         (n_spaces n) lbl (print_body n s)
     217      let lbl = CostLabel.string_of_cost_label lbl in
     218      Printf.sprintf "%s%s:\n%s" (n_spaces n) lbl (print_body n s)
     219  | Cminor.St_ind_0 (i, s) ->
     220      Printf.sprintf "%sindex %d:\n%s" (n_spaces n) i (print_body n s)
     221  | Cminor.St_ind_inc (i,s) ->
     222      Printf.sprintf "%sincrement %d:\n%s\n" (n_spaces n) i (print_body n s)
    212223
    213224let print_internal f_name f_def =
     
    246257  | Cminor.St_seq(_,_) -> "seq"
    247258  | Cminor.St_ifthenelse(_,_,_) -> "ifthenelse"
    248   | Cminor.St_loop(_) -> "loop"
     259(*  | Cminor.St_loop(_) -> "loop"
    249260  | Cminor.St_block(_) -> "block"
    250   | Cminor.St_exit(_) -> "exit"
     261  | Cminor.St_exit(_) -> "exit" *)
    251262  | Cminor.St_switch(_,_,_) -> "switch"
    252263  | Cminor.St_return(_) -> "return"
     
    254265  | Cminor.St_goto(_) -> "goto"
    255266  | Cminor.St_cost(_,_) -> "cost"
     267  | Cminor.St_ind_0 _ -> "index"
     268  | Cminor.St_ind_inc _ -> "increment"
  • Deliverables/D2.2/8051/src/cminor/cminorToRTLabs.ml

    r818 r1542  
    194194      let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in
    195195      let old_entry = rtlabs_fun.RTLabs.f_entry in
    196       let stmt = RTLabs.St_op2 (op2, destr, r1, r2, old_entry) in
     196      let r1_arg = RTLabs.Reg r1 in
     197      let r2_arg = RTLabs.Reg r2 in
     198      let stmt = RTLabs.St_op2 (op2, destr, r1_arg, r2_arg, old_entry) in
    197199      let rtlabs_fun = generate rtlabs_fun stmt in
    198200      translate_exprs rtlabs_fun lenv [r1 ; r2] [e1 ; e2]
     
    201203      let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e in
    202204      let old_entry = rtlabs_fun.RTLabs.f_entry in
    203       let stmt = RTLabs.St_load (chunk, r, destr, old_entry) in
     205      let stmt =
     206        RTLabs.St_load (chunk, RTLabs.Reg r, destr, old_entry) in
    204207      let rtlabs_fun = generate rtlabs_fun stmt in
    205208      translate_expr rtlabs_fun lenv r e
     
    269272    (rtlabs_fun : RTLabs.internal_function)
    270273    (lenv       : local_env)
    271     (exits      : Label.t list)
     274(*    (exits      : Label.t list) *)
    272275    (stmt       : Cminor.statement)
    273276    : RTLabs.internal_function =
     
    283286      let (rtlabs_fun, r) = choose_destination rtlabs_fun lenv e2 in
    284287      let old_entry = rtlabs_fun.RTLabs.f_entry in
    285       let stmt = RTLabs.St_store (chunk, addr, r, old_entry) in
     288      let stmt =
     289        RTLabs.St_store (chunk, RTLabs.Reg addr, RTLabs.Reg r, old_entry) in
    286290      let rtlabs_fun = generate rtlabs_fun stmt in
    287291      translate_exprs rtlabs_fun lenv [addr ; r] [e1 ; e2]
     
    321325
    322326    | Cminor.St_seq (s1, s2) ->
    323       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in
    324       translate_stmt rtlabs_fun lenv exits s1
     327      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in
     328      translate_stmt rtlabs_fun lenv (*exits*) s1
    325329
    326330    | Cminor.St_ifthenelse (e, s1, s2) ->
    327331      let old_entry = rtlabs_fun.RTLabs.f_entry in
    328       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s2 in
     332      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in
    329333      let lbl_false = rtlabs_fun.RTLabs.f_entry in
    330334      let rtlabs_fun = change_entry rtlabs_fun old_entry in
    331       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s1 in
     335      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s1 in
    332336      let lbl_true = rtlabs_fun.RTLabs.f_entry in
    333337      translate_branch rtlabs_fun lenv e lbl_true lbl_false
    334338
    335     | Cminor.St_loop s ->
     339(*    | Cminor.St_loop s ->
    336340      let loop_start = fresh_label rtlabs_fun in
    337341      let rtlabs_fun = change_entry rtlabs_fun loop_start in
     
    345349
    346350    | Cminor.St_exit n ->
    347       change_entry rtlabs_fun (List.nth exits n)
     351      change_entry rtlabs_fun (List.nth exits n) *)
    348352
    349353    | Cminor.St_return eopt ->
     
    362366
    363367    | Cminor.St_label (lbl, s) ->
    364       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
     368      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in
    365369      let old_entry = rtlabs_fun.RTLabs.f_entry in
    366370      add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry)
    367371
    368372    | Cminor.St_cost (lbl, s) ->
    369       let rtlabs_fun = translate_stmt rtlabs_fun lenv exits s in
     373      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in
    370374      let old_entry = rtlabs_fun.RTLabs.f_entry in
    371375      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
     376
     377    | Cminor.St_ind_0 (i, s) ->
     378      let rtlabs_fun = translate_stmt rtlabs_fun lenv s in
     379      let old_entry = rtlabs_fun.RTLabs.f_entry in
     380      generate rtlabs_fun (RTLabs.St_ind_0 (i, old_entry))
     381
     382    | Cminor.St_ind_inc (i, s) ->
     383      let rtlabs_fun = translate_stmt rtlabs_fun lenv s in
     384      let old_entry = rtlabs_fun.RTLabs.f_entry in
     385      generate rtlabs_fun (RTLabs.St_ind_inc (i, old_entry))
    372386
    373387    | Cminor.St_goto lbl ->
     
    446460
    447461  (* Complete the graph *)
    448   translate_stmt rtlabs_fun lenv [] f_def.Cminor.f_body
     462  translate_stmt rtlabs_fun lenv (*[]*) f_def.Cminor.f_body
    449463
    450464
  • Deliverables/D2.2/8051/src/common/costLabel.ml

    r486 r1542  
     1module Atom =
     2  struct
     3    include StringTools
     4  end
    15
    2 include StringTools
     6module StringMap = Map.Make(String)
     7
     8(** Simple expressions are for now affine maps of the form a*_+b *)
     9type sexpr =
     10    | Sexpr of int*int
     11
     12let is_const_sexpr (Sexpr(a, _)) = (a = 0)
     13
     14let sexpr_id = Sexpr(1, 0)
     15
     16let const_sexpr n = Sexpr(0, n)
     17
     18type index = int
     19
     20let make_id prefix depth = prefix ^ string_of_int depth
     21
     22type indexing = sexpr list
     23
     24type const_indexing = int ExtArray.t
     25
     26let const_ind_iter = ExtArray.iter
     27
     28let curr_const_ind = function
     29    | hd :: _ -> hd
     30    | _ -> invalid_arg "curr_const_ind applied to non-empty list"
     31
     32let init_const_indexing () = ExtArray.make ~buff:1 0 0
     33
     34let enter_loop_single indexing n = ExtArray.set indexing n 0
     35
     36let continue_loop_single indexing n =
     37  try
     38    ExtArray.set indexing n (ExtArray.get indexing n + 1)
     39  with | _ ->
     40    invalid_arg "uninitialized loop index"
     41
     42let curr_ind = function
     43    | hd :: _ -> hd
     44    | _ -> invalid_arg "non-empty indexing stack"
     45
     46let enter_loop inds = enter_loop_single (curr_ind inds)
     47
     48let continue_loop inds = continue_loop_single (curr_ind inds)
     49
     50let enter_loop_opt indexing = Option.iter (enter_loop indexing)
     51
     52let continue_loop_opt indexing = Option.iter (continue_loop indexing)
     53
     54let new_const_ind inds = init_const_indexing () :: inds
     55
     56let forget_const_ind = function
     57        | _ :: inds -> inds
     58        | _ -> invalid_arg "non-empty indexing stack"
     59
     60let sexpr_of i l =
     61    try
     62        List.nth l i
     63    with
     64                        | Failure _
     65      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"
     66
     67let empty_indexing = []
     68
     69let add_id_indexing ind = sexpr_id :: ind
     70
     71(* a*_+b is composed with c*_+d by substitution: *)
     72(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
     73let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
     74    Sexpr (a * c, b * c + d)
     75               
     76let ev_sexpr i (Sexpr(a, b)) = a*i+b
     77
     78(* i|-->e ° I *)
     79let rec compose_index_indexing i s l = match i, l with
     80        | 0, s' :: l' -> compose_sexpr s s' :: l'
     81        | x, s' :: l' -> s' :: compose_index_indexing (i-1) s l'
     82        | _ -> l
     83
     84
     85(* I°J applies every mapping in I to every mapping in J *)
     86let rec compose_indexing m n = match m, n with
     87        | s1 :: l1, s2 :: l2 -> compose_sexpr s1 s2 :: compose_indexing l1 l2
     88        | _ -> n 
     89
     90let rec compose_const_indexing_i i c = function
     91        | [] -> []
     92        | s :: l ->
     93                let head =
     94                        (* if s is constant leave it be. In particular, avoid raising the error *)
     95                        if is_const_sexpr s then s else
     96                        try
     97                          const_sexpr (ev_sexpr (ExtArray.get c i) s)
     98                        with
     99                                | Invalid_argument _ ->
     100                                        invalid_arg "constant indexing not enough to be applied" in
     101          head :: compose_const_indexing_i (i+1) c l
     102
     103module IndexingSet = Set.Make(struct
     104    type t = indexing
     105                let compare = compare
     106        end)
     107
     108type t = {
     109    name : Atom.t;
     110    i : indexing
     111}
     112
     113let comp_index i s lbl =
     114        {lbl with i = compose_index_indexing i s lbl.i}
     115
     116let ev_indexing c lbl =
     117    {lbl with i = compose_const_indexing_i 0 c lbl.i}
     118
     119
     120(* if [pretty] is false then a name suitable for labels is given*)
     121(* ('P' replaces '+') *)
     122let string_of_sexpr pretty prefix i (Sexpr(a, b)) =
     123        let plus = if pretty then "+" else "P" in
     124        let id = prefix ^ string_of_int i in
     125  let a_id_s = if a = 1 then id else string_of_int a ^ id in
     126        let b_s = string_of_int b in
     127        if a = 0 then b_s else
     128        if b = 0 then a_id_s else a_id_s ^ plus ^ b_s
     129       
     130(* examples:*)
     131(* [pretty] true:  (0,i1+1,2i2+2)*)
     132(* [pretty] false: _0_i1P1_2i2P2 *)
     133let rec string_of_indexing_tl pretty prefix i = function
     134        | [] -> if pretty then ")" else ""
     135        | hd :: tl ->
     136                let sep = if pretty then "," else "_" in
     137                let str = string_of_sexpr pretty prefix i hd in
     138                sep ^ str ^ string_of_indexing_tl pretty prefix (i+1) tl
     139
     140let string_of_indexing pretty prefix = function
     141        | [] -> ""
     142        | hd :: tl ->
     143                let start = if pretty then "(" else "_" in
     144    let str = string_of_sexpr pretty prefix 0 hd in
     145                start ^ str ^ string_of_indexing_tl pretty prefix 1 tl
     146               
     147let string_of_cost_label ?(pretty = false) lab =
     148        lab.name ^ string_of_indexing pretty "i" lab.i
     149
     150let fresh l universe =
     151        {name = Atom.Gen.fresh universe; i = l} 
     152
     153(* TODO: urgh. Necessary? *)
     154type aux_t = t
     155                                                       
     156(** labels are endowed with a lexicographical ordering *)
     157module T : Map.OrderedType with type t = aux_t =
     158    struct
     159        type t = aux_t
     160        let compare = compare (* uses the built-in lexicographical comparison *)
     161    end
     162
     163module Map = Map.Make(T)   
     164module Set = Set.Make(T)
     165(** [constant_map d x] produces a finite map which associates
     166    [x] to every element of the set [d]. *)
     167
     168let indexings_of atom s =
     169        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
     170        Set.fold f s IndexingSet.empty
    3171
    4172let constant_map d x =
  • Deliverables/D2.2/8051/src/common/costLabel.mli

    r486 r1542  
    11
    2 (** This module provides functions to manipulate and create fresh cost
     2(** This module provides functions to manipulate and create indexed cost
    33    labels. *)
    44
    5 include StringSig.S
     5(** [Atom] provides functions for cost atoms, the root of indexed costs *)
     6module Atom : sig
     7  include StringSig.S
     8end
     9
     10(** Simple expressions corresponding to loop tranformations.
     11    TODO: abstract or not? *)
     12type sexpr = Sexpr of int*int
     13
     14(** The identity simple expression, used in initialization. *)
     15val sexpr_id : sexpr
     16
     17(** Indexes are identified with (single-entry) loop depths. *)
     18type index = int
     19
     20(** [make_id prefix index] produces an identifier out of a
     21    prefix and a loop depth. *)
     22val make_id : string -> index -> string
     23
     24type indexing = sexpr list
     25
     26(** The type of constant indexings, to be used by interpreations *)
     27type const_indexing
     28
     29(** [const_ind_iter f c] iterates [f] over the values of indexes in c *)
     30val const_ind_iter : (int -> unit) -> const_indexing -> unit
     31
     32(** This is equivalent to [List.hd], but raises
     33    [Invalid_argument "non-empty indexing stack"] if argument is empty *)
     34val curr_const_ind : const_indexing list -> const_indexing
     35
     36(** [enter_loop inds n] is used to update the indexing stack [ind] when one
     37    is entering a loop indexed by [n]. Raises [Invalid_argument
     38    "non-empty indexing stack"] if [inds] is empty. *)
     39val enter_loop : const_indexing list -> index -> unit
     40
     41(** [enter_loop_opt inds (Some n)] behaves like [enter_loop inds n], and does
     42    nothing in case of [None].
     43    @see enter_loop *)
     44val enter_loop_opt : const_indexing list -> index option -> unit
     45
     46(** [continue_loop inds n] is used to update the indexing stack [inds] when
     47    one is continuing a loop indexed by [n].
     48    @raise [Invalid_argument "non-empty indexing stack"] if [inds] is empty.
     49    @raise [Invalid_argument "uninitialized loop index"] if the head of
     50    [inds] has no value for [index]. *)
     51val continue_loop : const_indexing list -> index -> unit
     52
     53(** [continue_loop_opt inds (Some n)] behaves like [continue_loop inds n], and
     54    does nothing in case of [None].
     55    @see continue_loop *)
     56val continue_loop_opt : const_indexing list -> index option -> unit
     57
     58(** [new_const_ind inds] pushes a new empty constant indexing on top of the
     59    stack [inds]. *)
     60val new_const_ind : const_indexing list -> const_indexing list
     61
     62(** [forget_const_ind inds] pops and discards the top constant indexing from the
     63    stack [inds].  Raises [Invalid_argument "non-empty indexing stack"] if
     64    [inds] is empty. *)
     65val forget_const_ind : const_indexing list -> const_indexing list
     66
     67(** [empty_indexing] is the empty indexing *)
     68val empty_indexing : indexing
     69
     70(** [add_id_indexing ind] adds an identity mapping in front of ind **)
     71val add_id_indexing : indexing -> indexing
     72
     73module IndexingSet : Set.S with type elt = indexing
     74
     75type t = {
     76  name : Atom.t;
     77  i : indexing
     78}
     79
     80(** [comp_index i s lbl] gives back the label [lbl] where index [i] is remapped
     81    to the simple expression [s]. *)
     82val comp_index : index -> sexpr -> t -> t
     83
     84(** [ev_indexing ind lbl] returns [lbl] where its indexing has been
     85    evaluated in the constant indexing [ind].
     86    @raise  Invalid_argument "constant indexing not enough to be applied" if
     87    [ind] does not contain enough mappings to evaluate [lbl]'s indexing. *)
     88val ev_indexing : const_indexing -> t -> t
     89
     90(** [string_of_cost_label pref t] converts an indexed label to a
     91    string suitable for a label name in C source.
     92    [string_of_cost_label ~pretty:true t] prints a more readable form *)
     93val string_of_cost_label : ?pretty : bool -> t -> string
     94
     95(** [fresh i u] creates a fresh label using [u] as name universe, inside
     96    the indexing [i] (which represents the nested loops containing the label) *)
     97val fresh : indexing -> Atom.Gen.universe -> t
     98
     99module Set : Set.S with type elt = t
     100module Map : Map.S with type key = t
     101
     102(** [indexings_of a s] produces the set of indexings of an atom [a] occurring
     103    in the set of indexed labels [s]. *)
     104val indexings_of : Atom.t -> Set.t -> IndexingSet.t
    6105
    7106(** [constant_map d x] produces a finite map which associates
  • Deliverables/D2.2/8051/src/common/label.ml

    r486 r1542  
    11
    22include StringTools
     3
     4module ImpMap = struct
     5
     6  type key =
     7      Map.key
     8 
     9  type 'data t =
     10      'data Map.t ref
     11     
     12  let create () =
     13    ref Map.empty
     14
     15  let clear t =
     16    t := Map.empty
     17   
     18  let add k d t =
     19    t := Map.add k d !t
     20
     21  let find k t =
     22    Map.find k !t
     23
     24  let iter f t =
     25    Map.iter f !t
     26
     27end
  • Deliverables/D2.2/8051/src/common/label.mli

    r486 r1542  
    44
    55include StringSig.S
     6
     7(** Imperative label maps for use with Fix *)
     8module ImpMap : (Fix.IMPERATIVE_MAPS with type key = t)
  • Deliverables/D2.2/8051/src/languages.ml

    r1462 r1542  
    3535  | AstLIN    of LIN.program
    3636  | AstASM    of ASM.program
     37
     38type transformation = name * (ast -> ast)
    3739
    3840let language_of_ast = function
     
    136138]
    137139
    138 let compile debug src tgt =
    139   (* Find the maximal suffix of the chain that starts with the
    140      language [src]. *)
    141   let rec subchain = function
    142     | [] ->
    143       (* The chain is assumed to be well-formed: such a suffix
    144          exists. *)
    145       assert false
    146     | ((l, _, _) :: _) as chain when l = src -> chain
    147     | _ :: chain -> subchain chain
    148   in
     140let insert_transformations ts chain =
     141  (* turn transformation into elements of the compilation chain *)
     142  let trans_to_comp (n, t) = (n, n, t) in
     143  let ts = List.map trans_to_comp ts in
     144  (* ts and chain are merged, and then sorted so that the resulting list is *)
     145  (* still a well formed compilation chain. Stable sort preserves order *)
     146  (* between transformations on the same language as appearing in ts *)
     147  let compare (n1, n2, s) (m1, m2, t) = compare (n1, n2) (m1, m2) in
     148  List.stable_sort compare (ts @ chain)
     149
     150let compile debug ts src tgt =
     151  (* insert intermediate transformations *)
     152  let chain = insert_transformations ts compilation_chain in
     153  (* erase transformations whose source is strictly before src *)
     154  let chain = List.filter (function (l1, _, _) -> l1 >= src) chain in
     155  (* erase transformations whose target is strictly after tgt *)
     156  let chain = List.filter (function (_, l2, _) -> l2 <= tgt) chain in
    149157  (* Compose the atomic translations to build a compilation function
    150158     from [src] to [tgt]. Again, we assume that the compilation chain
     
    153161     translation from [src] to [tgt]. *)
    154162  let rec compose iprogs src tgt chains ast =
    155     if src = tgt then List.rev (ast :: iprogs)
    156     else
    157       match chains with
    158         | [] ->
     163    match chains with
     164        | [] when src = tgt -> List.rev (ast :: iprogs)
     165        | [] -> 
    159166          Error.global_error "During compilation configuration"
    160167            (Printf.sprintf "It is not possible to compile from `%s' to `%s'."
     
    168175          ast :: l2_to_tgt iprog
    169176  in
    170   compose [] src tgt (subchain compilation_chain)
     177  compose [] src tgt chain
    171178
    172179
     
    210217
    211218(* FIXME *)
    212 let instrument costs_mapping = function
     219let instrument cost_tern costs_mapping = function
    213220  | AstClight p ->
    214221    let (p', cost_id, cost_incr, extern_cost_variables) =
    215       ClightAnnotator.instrument p costs_mapping in
     222      ClightAnnotator.instrument cost_tern p costs_mapping in
    216223    (AstClight p', cost_id, cost_incr, extern_cost_variables)
    217224(*
     
    227234    (p, "", "", StringTools.Map.empty)
    228235
    229 let annotate input_ast final =
     236let annotate cost_tern input_ast final =
    230237  let costs_mapping = compute_costs final in
    231   instrument costs_mapping input_ast
     238  instrument cost_tern costs_mapping input_ast
    232239
    233240let string_output asm_pretty = function
  • Deliverables/D2.2/8051/src/languages.mli

    r1488 r1542  
    3030  | AstASM     of ASM.program
    3131
     32
     33(** The type of additional transfromations, with the language they take place
     34    in and the actual transformation *)
     35type transformation = name * (ast -> ast)
     36
    3237(** [language_of_ast ast] returns the programming language of the
    3338    abstract syntax tree [ast]. *)
     
    4146(** {2 Compilation} *)
    4247
    43 (** [compile debug l1 l2] returns the compilation function that
    44     translates the language [l1] to the language [l2]. This may be the
     48(** [compile debug ts l1 l2] returns the compilation function that
     49    translates the language [l1] to the language [l2], employing the
     50    transformations in [ts] along the way . This may be the
    4551    composition of several compilation functions. If [debug] is
    4652    [true], all the intermediate programs are inserted in the
    4753    output. *)
    48 val compile : bool -> name -> name -> (ast -> ast list)
     54val compile : bool -> transformation list -> name -> name -> (ast -> ast list)
    4955
    5056(** [add_runtime ast] adds runtime functions for the operations not supported by
     
    6672val labelize : ast -> ast
    6773
    68 (** [annotate input_ast target_ast] inserts cost annotations into the input AST
    69     from the (final) target AST. It also returns the name of the cost variable,
    70     the name of the cost increment function, and a the name of a fresh
    71     uninitialized global variable for each external function. *)
    72 val annotate : ast -> ast -> (ast * string * string * string StringTools.Map.t)
     74(** [annotate cost_tern input_ast target_ast] inserts cost annotations into the
     75    input AST from the (final) target AST. It also returns the name of the cost
     76    variable and the name of the cost increment function, and a the name of a fresh
     77    uninitialized global variable for each external function. The [cost_tern] flag
     78    rules whether cost increments are given by ternary expressions or branch
     79    statements. *)
     80val annotate : bool -> ast -> ast -> (ast * string * string * string StringTools.Map.t)
    7381
    7482(** [interpret debug ast] runs the program [ast] from the default initial
  • Deliverables/D2.2/8051/src/options.ml

    r1462 r1542  
    4848let is_debug_enabled ()         = !debug_flag
    4949
     50let transformations = ref []
     51let add_transformation t () = transformations := !transformations @ [t]
     52let add_transformations ts () = transformations := !transformations @ ts
     53let get_transformations () = !transformations
     54
     55let cost_ternary_flag           = ref true
     56let set_cost_ternary            = (:=) cost_ternary_flag
     57let is_cost_ternary_enabled ()  = !cost_ternary_flag
     58
    5059let asm_pretty_flag             = ref false
    5160let set_asm_pretty              = (:=) asm_pretty_flag
     
    7988let set_lustre_test_max_int     = (:=) lustre_test_max_int
    8089let get_lustre_test_max_int ()  = !lustre_test_max_int
     90
    8191
    8292(*
     
    8999let set_dev_test                = (:=) dev_test
    90100let is_dev_test_enabled ()      = !dev_test
     101
     102let help_specify_opt_stage (trans : Languages.transformation) =
     103        Printf.sprintf "(done at the %s stage)." (Languages.to_string (fst trans))
     104
     105let basic_optimizations =
     106  [
     107    LoopPeeling.trans;
     108    ConstPropagation.trans;
     109    CopyPropagation.trans;
     110    RedundancyElimination.trans;
     111    CopyPropagation.trans;
     112    RedundancyElimination.trans
     113  ]
     114 
    91115
    92116let options = OptionsParsing.register [
     
    148172  extra_doc " [default is 1000]";
    149173
     174  "-peel", Arg.Unit (add_transformation LoopPeeling.trans),
     175  " Apply loop peeling " ^
     176    help_specify_opt_stage LoopPeeling.trans;
     177
     178  "-cst-prop", Arg.Unit (add_transformation ConstPropagation.trans),
     179  " Apply constant propagation " ^
     180    help_specify_opt_stage ConstPropagation.trans;
     181
     182  "-cpy-prop", Arg.Unit (add_transformation CopyPropagation.trans),
     183  " Apply copy propagation " ^
     184    help_specify_opt_stage CopyPropagation.trans;
     185
     186  "-pre", Arg.Unit (add_transformation RedundancyElimination.trans),
     187  " Apply partial redundancy elimination " ^
     188    help_specify_opt_stage RedundancyElimination.trans;
     189
     190  "-unroll-for",
     191  Arg.Int (fun i -> add_transformation (LoopUnrolling.trans ~factor:i ()) ()),
     192  " Apply loop unrolling, specifying factor " ^
     193  help_specify_opt_stage (LoopUnrolling.trans ());
     194
     195  "-unroll", Arg.Unit (add_transformation (LoopUnrolling.trans ())),
     196  " Apply loop unrolling " ^
     197  help_specify_opt_stage (LoopUnrolling.trans ());
     198
     199  "-O", Arg.Unit (add_transformations basic_optimizations),
     200  " Apply some optimizations.";
     201
     202  "-no-cost-tern",  Arg.Clear cost_ternary_flag,
     203  " Replace cost ternary expressions with equivalent branch statements.";
     204 
    150205(*
    151206  "-res", Arg.Set print_result_flag,
  • Deliverables/D2.2/8051/src/options.mli

    r1462 r1542  
    3232val is_debug_enabled : unit -> bool
    3333
     34(** {2 Cost ternary expressions} *)
     35val is_cost_ternary_enabled : unit -> bool
     36
    3437(** {2 Assembly pretty print} *)
    3538val set_asm_pretty : bool -> unit
     
    6467val get_lustre_test_max_int : unit -> int
    6568
     69
     70(** {2 Intermediate transformations } *)
     71val get_transformations : unit -> Languages.transformation list
    6672(*
    6773(** {2 Print results requests} *)
Note: See TracChangeset for help on using the changeset viewer.