Changeset 1357


Ignore:
Timestamp:
Oct 11, 2011, 5:42:20 PM (8 years ago)
Author:
tranquil
Message:
  • changed implementation of constant indexings with extensible arrays
  • work on ASM completed
  • next: optimizations!
Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
15 edited

Legend:

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

    r1349 r1357  
    132132  exit_addr   : BitVectors.word;
    133133       
     134(*
    134135        ind_0s      : int BitVectors.WordMap.t;
    135136  ind_incs    : int BitVectors.WordMap.t;
    136137  cost_labels : CostLabel.t BitVectors.WordMap.t
     138*)     
    137139}
    138140
     
    287289
    288290  exit_addr = BitVectors.zero `Sixteen;
     291(*
    289292  ind_0s = BitVectors.WordMap.empty;
    290293  ind_incs = BitVectors.WordMap.empty;
    291294  cost_labels = BitVectors.WordMap.empty
     295*)
    292296}
    293297
     
    19811985let load_program p =
    19821986  let st = load p.ASM.code initialize in
    1983   { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels }
     1987  { st with exit_addr = p.ASM.exit_addr (* ; cost_labels = p.ASM.cost_labels *)}
    19841988
    19851989type cost_trace = {
     
    19881992}
    19891993
    1990 (* TODO: indexes *)
    1991 let observe_trace trace st =
    1992         let update_ct_labels =
    1993           try
    1994                         let cost_label = BitVectors.WordMap.find st.pc st.cost_labels in
    1995             trace.ct_labels <- cost_label :: trace.ct_labels
    1996           with Not_found -> () in
    1997         update_ct_labels;
     1994(* TODO: supposing only one index reset or increment per instruction *)
     1995let update_indexes trace p st =
     1996  try
     1997    let i = BitVectors.WordMap.find st.pc p.ASM.inds in
     1998                CostLabel.enter_loop trace.ct_inds i
     1999  with Not_found -> ();
     2000  try
     2001    let i = BitVectors.WordMap.find st.pc p.ASM.incs in
     2002    CostLabel.continue_loop trace.ct_inds i
     2003  with Not_found -> ();
     2004  let instr,_,_ = fetch st.code_memory st.pc in
     2005        match instr with
     2006                | `ACALL _ | `LCALL _ ->
     2007      trace.ct_inds <- CostLabel.new_const_ind trace.ct_inds
     2008                | `RET ->
     2009                        trace.ct_inds <- CostLabel.forget_const_ind trace.ct_inds
     2010                | _ -> ()
     2011
     2012let update_labels trace p st =
     2013  try
     2014    let cost_label = BitVectors.WordMap.find st.pc p.cost_labels in
     2015        let ind = CostLabel.curr_const_ind trace.ct_inds in
     2016        let cost_label = CostLabel.ev_indexing ind cost_label in
     2017        trace.ct_labels <- cost_label :: trace.ct_labels
     2018  with Not_found -> ()
     2019
     2020
     2021
     2022let update_trace trace p st =
     2023        update_labels trace p st;
     2024        update_indexes trace p st;
    19982025  if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st
    19992026
     
    20142041    let st = load_program p in
    20152042    let trace = {ct_labels = []; ct_inds = []} in
    2016     let callback = observe_trace trace in
     2043    let callback = update_trace trace p in
    20172044    let st = execute callback st in
    20182045    let res = result st in
  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMInterpret.mli

    r1349 r1357  
    9898
    9999      exit_addr   : BitVectors.word;
    100 
     100(*
    101101      ind_0s      : int BitVectors.WordMap.t;
    102102      ind_incs    : int BitVectors.WordMap.t;
    103103      cost_labels : CostLabel.t BitVectors.WordMap.t
     104*)
    104105    }
    105106     
  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/Pretty.ml

    r1349 r1357  
    4343 function
    4444    `Label l -> l ^ ":"
    45                 (* ugly-printing *)
    46   | `Cost l -> CostLabel.string_of_cost_label l ^ ":"
     45  | `Cost l -> CostLabel.string_of_cost_label ~pretty:true l ^ ":"
    4746        | `Index i -> "index " ^ string_of_int i ^ ":"
    4847  | `Inc i -> "increment " ^ string_of_int i ^ ":"
     
    9998  | `XRL(`U2(a1,a2)) -> "xrl   " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    10099
     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
    101119let print_program p =
    102120  let mem = ASMInterpret.load_code_memory p.ASM.code in
    103121  let f (s, pc) _ =
    104122    let (inst, new_pc, cost) = ASMInterpret.fetch mem pc in
    105     (Printf.sprintf "%s% 6X:  %- 18s ;; %d  %s\n"
     123    (Printf.sprintf "%s% 6X:  %- 18s ;; %d%s\n"
    106124       s
    107125       (BitVectors.int_of_vect pc)
    108126       (pp_instruction inst)
    109127       cost
    110        (if BitVectors.WordMap.mem pc p.ASM.cost_labels then
    111                                  let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in
    112                CostLabel.string_of_cost_label ~pretty:true lbl
    113               else ""),
     128                         (find_comment p pc),
    114129     new_pc) in
    115130  fst (List.fold_left f ("", BitVectors.zero `Sixteen) p.ASM.code)
  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLInterpret.ml

    r1345 r1357  
    6565let change_trace st trace = { st with trace = trace }
    6666let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    67 
    68 let forget_ind st = match st.inds with
    69         | _ :: tail -> {st with inds = tail}
    70         | _ -> assert false (* indexing list must be non-empty *)
    71 let curr_ind st = match st.inds with
    72         | ind :: _ -> ind
    73         | _ -> assert false (* indexing list must be non-empty *)
    74 let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds }
    75 
    76 let max_depth graph =
    77     let f_stmt _ = function
    78         | ERTL.St_ind_0(i,_) | ERTL.St_ind_inc(i,_) -> max (i + 1)
    79         | _ -> fun x -> x in
    80     Label.Map.fold f_stmt graph 0
     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
    8172
    8273let empty_state =
     
    136127  let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in
    137128  let pc = entry_pc lbls_offs ptr def in
    138         let st = allocate_ind st (max_depth def.ERTL.f_graph) in
     129        let st = new_ind st in
    139130  change_lenv (change_pc st pc) lenv
    140131
     
    241232      let st = save_ra lbls_offs st ra in
    242233      let st = save_frame st in
    243                         let max_depth = max_depth def.ERTL.f_graph in
    244234      init_fun_call lbls_offs st ptr def
    245235    | ERTL.F_ext def ->
     
    273263
    274264    | ERTL.St_cost (cost_lbl, lbl) ->
    275                         let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in
     265                        let cost_lbl = ev_label st cost_lbl in
    276266      let st = add_trace st cost_lbl in
    277267      next_pc st lbl
    278268
    279269    | ERTL.St_ind_0 (i, lbl) ->
    280                         CostLabel.enter_loop (Some i) (curr_ind st);
     270                        enter_loop st i;
    281271                        next_pc st lbl
    282272
    283273    | ERTL.St_ind_inc (i, lbl) ->
    284       CostLabel.continue_loop (Some i) (curr_ind st);
     274      continue_loop st i;
    285275      next_pc st lbl
    286276
  • Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINInterpret.ml

    r1349 r1357  
    4848let change_trace st trace = { st with trace = trace }
    4949let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    50 
    51 let forget_ind st = match st.inds with
    52     | _ :: tail -> {st with inds = tail}
    53     | _ -> assert false (* indexing list must be non-empty *)
    54 let curr_ind st = match st.inds with
    55     | ind :: _ -> ind
    56     | _ -> assert false (* indexing list must be non-empty *)
    57 let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds }
    58 
    59 let max_depth =
    60     let f_stmt j = function
    61         | LIN.St_ind_0 i | LIN.St_ind_inc i -> max (i + 1) j
    62         | _ -> j in
    63     List.fold_left f_stmt 0
     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
    6455
    6556let empty_state =
     
    9182
    9283let init_fun_call st ptr def =
    93         let st = allocate_ind st (max_depth def) in
     84        let st = new_ind st in
    9485  change_pc st (Val.change_address_offset ptr Val.Offset.zero)
    9586
     
    217208
    218209    | LIN.St_cost cost_lbl ->
    219                         let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in
     210                        let cost_lbl = ev_label st cost_lbl in
    220211      let st = add_trace st cost_lbl in
    221212      next_pc st
    222213                       
    223214                | LIN.St_ind_0 i ->
    224                         CostLabel.enter_loop (Some i) (curr_ind st);
     215                        enter_loop st i;
    225216                        next_pc st
    226217
    227218    | LIN.St_ind_inc i ->
    228             CostLabel.continue_loop (Some i) (curr_ind st);
     219            continue_loop st i;
    229220            next_pc st
    230221
  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLInterpret.ml

    r1345 r1357  
    4545let change_trace st trace = { st with trace = trace }
    4646let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
    47 
    48 let forget_ind st = match st.inds with
    49     | _ :: tail -> {st with inds = tail}
    50     | _ -> assert false (* indexing list must be non-empty *)
    51 let curr_ind st = match st.inds with
    52     | ind :: _ -> ind
    53     | _ -> assert false (* indexing list must be non-empty *)
    54 let allocate_ind st n = { st with inds = Array.make n 0 :: st.inds }
    55 
    56 let max_depth graph =
    57     let f_stmt _ = function
    58         | LTL.St_ind_0(i,_) | LTL.St_ind_inc(i,_) -> max (i + 1)
    59         | _ -> fun x -> x in
    60     Label.Map.fold f_stmt graph 0
     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
    6152
    6253let empty_state =
     
    111102let init_fun_call lbls_offs st ptr def =
    112103  let pc = entry_pc lbls_offs ptr def in
    113         let st = allocate_ind st (max_depth def.LTL.f_graph) in
     104        let st = new_ind st in
    114105  change_pc st pc
    115106
     
    246237
    247238    | LTL.St_cost (cost_lbl, lbl) ->
    248                         let cost_lbl = CostLabel.apply_const_indexing (curr_ind st) cost_lbl in
     239                        let cost_lbl = ev_label st cost_lbl in
    249240      let st = add_trace st cost_lbl in
    250241      next_pc st lbl
    251242
    252243    | LTL.St_ind_0 (i, lbl) ->
    253             CostLabel.enter_loop (Some i) (curr_ind st);
     244            enter_loop st i;
    254245            next_pc st lbl
    255246
    256247    | LTL.St_ind_inc (i, lbl) ->
    257       CostLabel.continue_loop (Some i) (curr_ind st);
     248      continue_loop st i;
    258249      next_pc st lbl
    259250
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLInterpret.ml

    r1345 r1357  
    6262
    6363let print_state = function
    64   | State (_, _, lbl, sp, lenv, carry, mem, ind::_, _) ->
     64  | State (_, _, lbl, sp, lenv, carry, mem, ind, _) ->
    6565    Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
    6666      (Val.string_of_address sp)
     
    6868      (string_of_local_env lenv)
    6969      (Mem.to_string mem);
    70                         Array.iter (fun a -> Printf.printf "%d, " a) ind;
     70                        let i = CostLabel.curr_const_ind ind in
     71                        CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
    7172                        Printf.printf "Regular state: %s\n\n%!"
    7273      lbl
    73         | State (_, _, _, _, _, _, _, [], _) -> assert false (* indexings non-empty *)
    7474  | CallState (_, _, args, mem, _, _) ->
    7575    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
     
    116116  State (sfrs, graph, next_lbl, sp, lenv, carry, mem, inds, trace)
    117117
    118 let curr_ind : indexing list -> indexing = function
    119     | ind :: _ -> ind
    120     | _ -> assert false (* indexing list must be non-empty *)
    121 
    122 let forget_ind : indexing list -> indexing list = function
    123     | _ :: tail -> tail
    124     | _ -> assert false (* indexing list must be non-empty *)
    125 
    126 let max_depth graph =
    127     let f_stmt _ = function
    128         | RTL.St_ind_0(i,_) | RTL.St_ind_inc(i,_) -> max (i + 1)
    129         | _ -> fun x -> x in
    130     Label.Map.fold f_stmt graph 0
     118let curr_ind = CostLabel.curr_const_ind
     119
     120let forget_ind = CostLabel.forget_const_ind
     121
     122let new_ind = CostLabel.new_const_ind
    131123
    132124
     
    149141
    150142      | RTL.St_cost (cost_lbl, lbl) ->
    151         let cost_lbl = CostLabel.apply_const_indexing (curr_ind inds) cost_lbl in
     143        let cost_lbl = CostLabel.ev_indexing (curr_ind inds) cost_lbl in
    152144        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, cost_lbl :: trace)
    153145
    154146      | RTL.St_ind_0 (i, lbl) ->
    155   CostLabel.enter_loop (Some i) (curr_ind inds);
     147  CostLabel.enter_loop inds i;
    156148  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    157149
    158150      | RTL.St_ind_inc (i, lbl) ->
    159   CostLabel.continue_loop (Some i) (curr_ind inds);
     151  CostLabel.continue_loop inds i;
    160152  State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    161153
     
    275267  match f_def with
    276268    | RTL.F_int def ->
    277                         let ind = Array.make (max_depth def.RTL.f_graph) 0 in
     269                        let inds = new_ind inds in
    278270      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
    279271      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
    280272             init_locals def.RTL.f_locals def.RTL.f_params args,
    281              Val.undef, mem', ind::inds, trace)
     273             Val.undef, mem', inds, trace)
    282274    | RTL.F_ext def ->
    283275      let (mem', vs) = interpret_external mem def.AST.ef_tag args in
  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsInterpret.ml

    r1345 r1357  
    6060
    6161let print_state state = (match state with
    62   | State (_, _, sp, lbl, lenv, mem, ind::_, _) ->
     62  | State (_, _, sp, lbl, lenv, mem, inds, _) ->
    6363    Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
    6464      (Val.string_of_address sp)
    6565      (string_of_local_env lenv)
    6666      (Mem.to_string mem);
    67                         Array.iter (fun a -> Printf.printf "%d, " a) ind;
     67                        let i = CostLabel.curr_const_ind inds in
     68                        CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
    6869                        Printf.printf "Regular state: %s\n\n%!"
    6970      lbl
     
    7677      (Mem.to_string mem)
    7778      (Val.to_string v)
    78         | _ -> assert false (* list of indexings in State should be non-empty *)
    7979        ); Printf.printf "-----------------------------------------------------\n\n%!"
    8080
     
    126126  State (sfrs, graph, sp, next_lbl, lenv, mem, inds, trace)
    127127
    128 
    129 let curr_ind : indexing list -> indexing = function
    130         | ind :: _ -> ind
    131         | _ -> assert false (* indexing list must be non-empty *)
    132 
    133 let forget_ind : indexing list -> indexing list = function
    134         | _ :: tail -> tail
    135         | _ -> assert false (* indexing list must be non-empty *)
    136 
    137 let max_depth graph =
    138         let f_stmt _ = function
    139                 | RTLabs.St_ind_0(i,_) | RTLabs.St_ind_inc(i,_) -> max (i + 1)
    140                 | _ -> fun x -> x in
    141         Label.Map.fold f_stmt graph 0
     128let curr_ind = CostLabel.curr_const_ind
     129
     130let forget_ind = CostLabel.forget_const_ind
     131
     132let new_ind = CostLabel.new_const_ind
    142133
    143134(* Interpret statements. *)
     
    158149
    159150      | RTLabs.St_cost (cost_lbl, lbl) ->
    160   let cost_lbl = CostLabel.apply_const_indexing (curr_ind inds) cost_lbl in
     151  let cost_lbl = CostLabel.ev_indexing (curr_ind inds) cost_lbl in
    161152        State (sfrs, graph, sp, lbl, lenv, mem, inds, cost_lbl :: trace)
    162153       
    163154            | RTLabs.St_ind_0 (i, lbl) ->
    164         CostLabel.enter_loop (Some i) (curr_ind inds);
     155        CostLabel.enter_loop inds i;
    165156  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    166157
    167158      | RTLabs.St_ind_inc (i, lbl) ->
    168   CostLabel.continue_loop (Some i) (curr_ind inds);
     159  CostLabel.continue_loop inds i;
    169160  State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
    170161
     
    313304            (* allocate new constant indexing *)
    314305                        let graph = def.RTLabs.f_graph in
    315                         let ind = Array.make (max_depth graph) 0 in
    316       State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', ind::inds, trace)
     306                        let inds = new_ind inds in
     307      State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace)
    317308    | RTLabs.F_ext def ->
    318309      let (mem', v) = interpret_external mem def.AST.ef_tag args in
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml

    r1319 r1357  
    296296        (id, uint) :: loop_indexes_defs prefix max_depth
    297297
     298let max_depth =
     299        let f_expr _ _ = () in
     300        let f_stmt stmt _ res_stmts =
     301                let curr_max = List.fold_left max 0 res_stmts in
     302                if curr_max > 0 then curr_max else     
     303                match stmt with
     304                | Clight.Swhile(Some x,_,_) | Clight.Sdowhile(Some x,_,_)
     305                | Clight.Sfor(Some x,_,_,_,_) -> x + 1
     306                | _ -> 0 in
     307        ClightFold.statement2 f_expr f_stmt
     308
    298309(* Instrument a function. *)
    299310
     
    301312  let def = match def with
    302313    | Clight.Internal def ->
    303         let max_depth = ClightUtils.max_loop_index_lbld def.Clight.fn_body in
     314        let max_depth = max_depth def.Clight.fn_body in
    304315        let vars = loop_indexes_defs l_ind max_depth in
    305316        let vars = List.rev_append vars def.Clight.fn_vars in
  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightInterpret.ml

    r1345 r1357  
    3232  | Kfor3 of int option*expr*statement*statement*continuation
    3333  | Kswitch of continuation
    34   | Kcall of (Value.address*ctype) option*cfunction*localEnv*
    35         indexing*continuation
     34  | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
    3635
    3736type state =
    38   | State of cfunction*statement*continuation*localEnv*memory*indexing
    39   | Callstate of fundef*Value.t list*continuation*memory
    40   | 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
    4140
    4241let string_of_unop = function
     
    157156      (string_of_local_env lenv)
    158157      (Mem.to_string mem);
    159                 Array.iteri (fun a -> Printf.printf "%d,") c;
     158                let i = CostLabel.curr_const_ind c in
     159                CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) i;
    160160    Printf.printf "\nRegular state: %s\n\n%!"
    161161      (string_of_statement stmt)
    162   | Callstate (_, args, _, mem) ->
     162  | Callstate (_, args, _, mem, _) ->
    163163    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
    164164      (Mem.to_string mem)
    165165      (MiscPottier.string_of_list " " Value.to_string args)
    166   | Returnstate (v, _, mem) ->
     166  | Returnstate (v, _, mem, _) ->
    167167    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    168168      (Mem.to_string mem)
     
    427427    | Ecost (lbl,e1) ->
    428428                        (* applying current indexing on label *)
    429                         let lbl = CostLabel.apply_const_indexing c lbl in
     429                        let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
    430430      let (v1,l1) = eval_expr localenv m c e1 in
    431431      (v1,lbl::l1)
     
    492492  | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') ->
    493493                (* possibly continuing a loop *)
    494                 CostLabel.continue_loop i c; (* if loop is not continued, this change
     494                CostLabel.continue_loop_opt c i; (* if loop is not continued, this change
    495495                                                will have no effect in the following. *)
    496496    let ((v1,_),l1) = eval_expr e m c a in
     
    499499    condition v1 a_true a_false
    500500  | Sskip, Kfor3(i,a2,a3,s,k) | Scontinue, Kfor3(i,a2,a3,s,k) ->
    501     CostLabel.continue_loop i c;
     501    CostLabel.continue_loop_opt c i;
    502502    let ((v1,_),l1) = eval_expr e m c a2 in
    503503    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     
    508508  | Sskip, Kcall _ ->
    509509    let m' = free_local_env m e in
    510     (Returnstate(Value.undef,k,m'),[])
     510    (Returnstate(Value.undef,k,m',c),[])
    511511  | Sassign(a1, a2), _ ->
    512512    let ((v1,t1),l1) = (eval_lvalue e m c a1) in
     
    517517    let fd = Mem.find_fun_def m (address_of_value v1) in
    518518    let (vargs,l2) = eval_exprlist e m c al in
    519     (Callstate(fd,vargs,Kcall(None,f,e,c,k),m),l1@l2)
     519    (Callstate(fd,vargs,Kcall(None,f,e,k),m,c),l1@l2)
    520520  | Scall(Some lhs,a,al), _ ->
    521521    let ((v1,_),l1) = eval_expr e m c a in
     
    523523    let (vargs,l2) = eval_exprlist e m c al in
    524524    let (vt3,l3) = eval_lvalue e m c lhs in
    525     (Callstate(fd,vargs,Kcall(Some vt3,f,e,c,k),m),l1@l2@l3)
     525    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m,c),l1@l2@l3)
    526526  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m,c),[])
    527527  | Sifthenelse(a,s1,s2), _ ->
     
    531531    condition v1 a_true a_false
    532532  | Swhile(i,a,s), _ ->
    533                 CostLabel.enter_loop i c;
     533                CostLabel.enter_loop_opt c i;
    534534    let ((v1,_),l1) = eval_expr e m c a in
    535535    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     
    537537    condition v1 a_true a_false
    538538  | Sdowhile(i,a,s), _ ->
    539                 CostLabel.enter_loop i c;
     539                CostLabel.enter_loop_opt c i;
    540540                (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
    541541  | Sfor(i,Sskip,a2,a3,s), _ ->
    542                 CostLabel.enter_loop i c;
     542                CostLabel.enter_loop_opt c i;
    543543    let ((v1,_),l1) = eval_expr e m c a2 in
    544544    let a_false = (State(f,Sskip,k,e,m,c),l1) in
     
    553553  | Sreturn None, _ ->
    554554    let m' = free_local_env m e in
    555     (Returnstate(Value.undef,(call_cont k),m'),[])
     555    (Returnstate(Value.undef,(call_cont k),m',c),[])
    556556  | Sreturn (Some a), _ ->
    557557    let ((v1,_),l1) = eval_expr e m c a  in
    558558    let m' = free_local_env m e in
    559     (Returnstate(v1,call_cont k,m'),l1)
     559    (Returnstate(v1,call_cont k,m',c),l1)
    560560  | Sswitch(a,sl), _ ->
    561561    let ((v,_),l) = eval_expr e m c a in
     
    565565  | Scost(lbl,s), _ ->
    566566                (* applying current indexing on label *)
    567                 let lbl = CostLabel.apply_const_indexing c lbl in
     567                let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
    568568                (State(f,s,k,e,m,c),[lbl])
    569569  | Sgoto lbl, _ ->
     
    578578module InterpretExternal = Primitive.Interpret (Mem)
    579579
    580 let interpret_external k mem f args =
     580let interpret_external k mem c f args =
    581581  let (mem', v) = match InterpretExternal.t mem f args with
    582582    | (mem', InterpretExternal.V vs) ->
     
    584584      (mem', v)
    585585    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    586   Returnstate (v, k, mem')
    587 
    588 let step_call args cont mem = function
     586  Returnstate (v, k, mem',c)
     587
     588let step_call args cont mem c = function
    589589  | Internal f ->
    590590    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
    591591                (* initializing loop indices *)
    592                 let max_depth = ClightUtils.max_loop_index_lbld f.fn_body in
    593                 let c = Array.make max_depth 0 in
     592                let c = CostLabel.new_const_ind c in
    594593    State (f, f.fn_body, cont, e, mem', c)
    595594  | External(id,targs,tres) when List.length targs = List.length args ->
    596     interpret_external cont mem id args
     595    interpret_external cont mem c id args
    597596  | External(id,_,_) ->
    598597    error ("wrong size of arguments when calling external " ^ id ^ ".")
     
    600599let step = function
    601600  | State(f,stmt,k,e,m,c) -> eval_stmt f k e m stmt c
    602   | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    603   | Returnstate(v,Kcall(None,f,e,c,k),m) -> (State(f,Sskip,k,e,m,c),[])
    604   | Returnstate(v,Kcall((Some(vv, ty)),f,e,c,k),m) ->
     601  | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[])
     602  | Returnstate(v,Kcall(None,f,e,k),m,c) ->
     603                let c = CostLabel.forget_const_ind c in
     604                (State(f,Sskip,k,e,m,c),[])
     605  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) ->
     606    let c = CostLabel.forget_const_ind c in
    605607    let m' = assign m v ty vv in
    606608    (State(f,Sskip,k,e,m',c),[])
     
    641643  if debug then print_state state ;
    642644  match state with
    643     | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
     645    | Returnstate(v,Kstop,_,_) -> (* Explicit return in main *)
    644646      print_and_return_result (compute_result v)
    645647    | State(_,Sskip,Kstop,_,_,_) -> (* Implicit return in main *)
     
    653655    | Some main ->
    654656      let mem = init_mem prog in
    655       let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
     657      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem,[]),[]) in
    656658      exec debug [] first_state
  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorInterpret.ml

    r1345 r1357  
    3131  | Ct_endblock of continuation
    3232  | Ct_returnto of
    33       ident option*internal_function*Val.address*local_env*indexing*continuation
     33      ident option*internal_function*Val.address*local_env*continuation
    3434
    3535type state =
    3636    State_regular of
    3737      internal_function*statement*continuation*Val.address*local_env*
    38                          (function_def Mem.memory)*indexing
    39   | State_call of function_def*Val.t list*continuation*(function_def Mem.memory)
    40   | State_return of Val.t*continuation*(function_def Mem.memory)
     38                         (function_def Mem.memory)*indexing list
     39  | State_call of function_def*Val.t list*continuation*
     40             (function_def Mem.memory)*indexing list
     41  | State_return of Val.t*continuation*(function_def Mem.memory)*indexing list
    4142
    4243let string_of_local_env lenv =
     
    8182      (Mem.to_string mem)
    8283      (Val.to_string (value_of_address sp));
    83                         Array.iter (fun a -> Printf.printf "%d, " a) i;
     84                        let ind = CostLabel.curr_const_ind i in
     85                        CostLabel.const_ind_iter (fun a -> Printf.printf "%d, " a) ind;
    8486                        Printf.printf "\nRegular state: %s\n\n%!"
    8587      (string_of_statement stmt)
    86   | State_call (_, args, _, mem) ->
     88  | State_call (_, args, _, mem,_) ->
    8789    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
    8890      (Mem.to_string mem)
    8991      (MiscPottier.string_of_list " " Val.to_string args)
    90   | State_return (v, _, mem) ->
     92  | State_return (v, _, mem,_) ->
    9193    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
    9294      (Mem.to_string mem)
     
    264266
    265267
    266 let call_state sigma e m f params cont =
     268let call_state sigma e m i f params cont =
    267269  let (addr,l1) = eval_expression sigma e m f in
    268270  let fun_def = Mem.find_fun_def m (address_of_value addr) in
    269271  let (args,l2) = eval_exprlist sigma e m params in
    270   (State_call(fun_def,args,cont,m),l1@l2)
     272  (State_call(fun_def,args,cont,m,i),l1@l2)
    271273
    272274let eval_stmt f k sigma e m i s = match s, k with
     
    274276  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m, i),[])
    275277  | St_skip, (Ct_returnto _ as k) ->
    276     (State_return (Val.undef,k,Mem.free m sigma),[])
     278    (State_return (Val.undef,k,Mem.free m sigma,i),[])
    277279  | St_skip,Ct_ind_inc(ind,k) ->
    278                 CostLabel.continue_loop (Some ind) i;
     280                CostLabel.continue_loop i ind;
    279281                (State_regular(f, s, k, sigma, e, m, i),[])
    280282  | St_skip,Ct_stop ->
    281     (State_return (Val.undef,Ct_stop,Mem.free m sigma),[])
     283    (State_return (Val.undef,Ct_stop,Mem.free m sigma,i),[])
    282284  | St_assign(x,exp),_ ->
    283285    let (v,l) = eval_expression sigma e m exp in
     
    290292    (State_regular(f, St_skip, k, sigma, e, m, i),l1@l2)
    291293  | St_call(xopt,f',params,_),_ ->
    292     call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,i,k))
     294    call_state sigma e m i f' params (Ct_returnto(xopt,f,sigma,e,k))
    293295  | St_tailcall(f',params,_),_ ->
    294     call_state sigma e m f' params (callcont k)
     296    call_state sigma e m i f' params (callcont k)
    295297  | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m, i),[])
    296298  | St_ifthenelse(exp,s1,s2),_ ->
     
    324326    else error "undefined switch value."
    325327  | St_return(None),_ ->
    326     (State_return (Val.undef,callcont k,Mem.free m sigma),[])
     328    (State_return (Val.undef,callcont k,Mem.free m sigma,i),[])
    327329  | St_return(Some(a)),_ ->
    328330      let (v,l) = eval_expression sigma e m a in
    329       (State_return (v,callcont k,Mem.free m sigma),l)
     331      (State_return (v,callcont k,Mem.free m sigma,i),l)
    330332  | St_cost(lbl,s),_ ->
    331333    (* applying current indexing on label *)
    332     let lbl = CostLabel.apply_const_indexing i lbl in
     334    let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind i) lbl in
    333335                (State_regular(f,s,k,sigma,e,m,i),[lbl])
    334336        | St_ind_0(ind,s),_ ->
    335                 CostLabel.enter_loop (Some ind) i;
     337                CostLabel.enter_loop i ind;
    336338                (State_regular(f,s,k,sigma,e,m,i), [])
    337339        | St_ind_inc(s,ind),_ ->
     
    342344module InterpretExternal = Primitive.Interpret (Mem)
    343345
    344 let interpret_external k mem f args =
     346let interpret_external k mem i f args =
    345347  let (mem', v) = match InterpretExternal.t mem f args with
    346348    | (mem', InterpretExternal.V vs) ->
     
    348350      (mem', v)
    349351    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
    350   State_return (v, k, mem')
    351 
    352 let max_loop_index =
    353   let f_expr _ _ = () in
    354   let f_stmt stmt _ sub_stmts_res =
    355         let curr_max = List.fold_left max 0 sub_stmts_res in
    356         match stmt with
    357           | Cminor.St_ind_0 (x, _) | Cminor.St_ind_inc (_, x) ->
    358                                                  max (x+1) curr_max
    359           | _ -> curr_max in
    360   CminorFold.statement f_expr f_stmt
    361 
    362 let step_call vargs k m = function
     352  State_return (v, k, mem', i)
     353
     354let step_call vargs k m i = function
    363355  | F_int f ->
    364356    let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in
    365357    let lenv = init_local_env vargs f.f_params f.f_vars in
    366                 let i = Array.make (max_loop_index f.f_body) 0 in
     358                let i = CostLabel.new_const_ind i in
    367359    State_regular(f,f.f_body,k,sp,lenv,m,i)
    368   | F_ext f -> interpret_external k m f.ef_tag vargs
     360  | F_ext f -> interpret_external k m i f.ef_tag vargs
    369361
    370362let step = function
    371363  | State_regular(f,stmt,k,sp,e,m,i) -> eval_stmt f k sp e m i stmt
    372   | State_call(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    373   | State_return(v,Ct_returnto(None,f,sigma,e,i,k),m) ->
     364  | State_call(fun_def,vargs,k,m,i) -> (step_call vargs k m i fun_def,[])
     365  | State_return(v,Ct_returnto(None,f,sigma,e,k),m,i) ->
     366                let i = CostLabel.forget_const_ind i in
    374367    (State_regular(f,St_skip,k,sigma,e,m,i),[])
    375   | State_return(v,Ct_returnto(Some x,f,sigma,e,i,k),m) ->
     368  | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m,i) ->
    376369    let e = LocalEnv.add x v e in
     370    let i = CostLabel.forget_const_ind i in
    377371    (State_regular(f,St_skip,k,sigma,e,m,i),[])
    378372  | _ -> error "state malformation."
     
    397391  if debug then print_state state ;
    398392  match state with
    399     | State_return(v,Ct_stop,_) -> (* Explicit return in main *)
     393    | State_return(v,Ct_stop,_,_) -> (* Explicit return in main *)
    400394      print_and_return_result (compute_result v)
    401395    | State_regular(_,St_skip,Ct_stop,_,_,_,_) -> (* Implicit return in main *)
     
    409403    | Some main ->
    410404      let mem = init_mem prog in
    411       let first_state = (State_call (find_fundef main mem,[],Ct_stop,mem),[]) in
     405                        let main = find_fundef main mem in
     406      let first_state = (State_call (main,[],Ct_stop,mem,[]),[]) in
    412407      exec debug [] first_state
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml

    r1328 r1357  
    2020type indexing = sexpr list
    2121
    22 type const_indexing = int array
     22type const_indexing = int ExtArray.t
    2323
    24 (** [enter_loop n indexing] is used to update indexing when one is entering a
    25     loop indexed by [n].
    26                 The function recycles the same constant indexing *)
    27 let rec enter_loop n indexing = match n with
    28         | None -> ()
    29         | Some x -> try indexing.(x) <- 0 with | _ -> assert false
     24let const_ind_iter = ExtArray.iter
    3025
    31 (** [enter_loop n indexing] is used to update indexing when one is continuing a
    32     loop indexed by [n]. *)
    33 let rec continue_loop n indexing = match n with
    34         | None -> ()
    35         | Some x -> try indexing.(x) <- indexing.(x) + 1 with | _ -> assert false
     26let curr_const_ind = function
     27    | hd :: _ -> hd
     28    | _ -> invalid_arg "curr_const_ind applied to non-empty list"
     29
     30let init_const_indexing () = ExtArray.make ~buff:1 0 0
     31
     32let enter_loop_single indexing n = ExtArray.set indexing n 0
     33
     34let continue_loop_single indexing n =
     35        try
     36                ExtArray.set indexing n (ExtArray.get indexing n + 1)
     37        with | _ ->
     38          invalid_arg "uninitialized loop index"
     39
     40let curr_ind = function
     41    | hd :: _ -> hd
     42    | _ -> invalid_arg "non-empty indexing stack"
     43
     44let enter_loop inds = enter_loop_single (curr_ind inds)
     45
     46let continue_loop inds = continue_loop_single (curr_ind inds)
     47
     48let enter_loop_opt indexing = Option.iter (enter_loop indexing)
     49
     50let continue_loop_opt indexing = Option.iter (continue_loop indexing)
     51
     52let new_const_ind inds = init_const_indexing () :: inds
     53
     54let forget_const_ind = function
     55        | _ :: inds -> inds
     56        | _ -> invalid_arg "non-empty indexing stack"
    3657
    3758let sexpr_of i l =
     
    6990        | s :: l ->
    7091                try
    71                   const_sexpr (ev_sexpr c.(i) s) :: compose_const_indexing_i (i+1) c l
     92                  const_sexpr (ev_sexpr (ExtArray.get c i) s) ::
     93                         compose_const_indexing_i (i+1) c l
    7294                with
    73                         | Invalid_argument _ -> assert false
     95                        | Invalid_argument _ ->
     96                                invalid_arg "constant indexing not enough to be applied"
    7497
    7598module IndexingSet = Set.Make(struct
     
    83106}
    84107
    85 let apply_const_indexing c lbl =
     108let ev_indexing c lbl =
    86109    {lbl with i = compose_const_indexing_i 0 c lbl.i}
    87110
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli

    r1319 r1357  
    2121type indexing = sexpr list
    2222
    23 type const_indexing = int array
     23type const_indexing
    2424
    25 (** [enter_loop n indexing] is used to update indexing when one is entering a
    26     loop indexed by [n].
    27         The function recycles the same constant indexing *)
    28 val enter_loop : index option -> const_indexing -> unit
     25val const_ind_iter : (int -> unit) -> const_indexing -> unit
    2926
    30 (** [continue_loop n indexing] is used to update indexing when one is continuing a
    31     loop indexed by [n]. *)
    32 val continue_loop : index option -> const_indexing -> unit
     27(** Top of the stack.
     28    @raise [Invalid_argument "non-empty indexing stack"] if argument is empty *)
     29val curr_const_ind : const_indexing list -> const_indexing
     30
     31(** [enter_loop inds n] is used to update the indexing stack [ind] when one
     32    is entering a loop indexed by [n]. Raises [Invalid_argument
     33                "non-empty indexing stack"] if [inds] is empty. *)
     34val enter_loop : const_indexing list -> index -> unit
     35
     36(** [enter_loop_opt inds (Some n)] behaves like [enter_loop inds n], and does
     37    nothing in case of [None].
     38                @see enter_loop *)
     39val enter_loop_opt : const_indexing list -> index option -> unit
     40
     41(** [continue_loop inds n] is used to update the indexing stack [inds] when
     42    one is continuing a loop indexed by [n].
     43                @raise [Invalid_argument "non-empty indexing stack"] if [inds] is empty.
     44                @raise [Invalid_argument "uninitialized loop index"] if the head of
     45                [inds] has no value for [index]. *)
     46val continue_loop : const_indexing list -> index -> unit
     47
     48(** [continue_loop_opt inds (Some n)] behaves like [continue_loop inds n], and
     49    does nothing in case of [None].
     50    @see continue_loop *)
     51val continue_loop_opt : const_indexing list -> index option -> unit
     52
     53(** [new_const_ind inds] pushes a new empty constant indexing on top of the
     54    stack [inds]. *)
     55val new_const_ind : const_indexing list -> const_indexing list
     56
     57(** [forget_const_ind inds] pops and discards the top constant indexing from the
     58    stack [inds].  Raises [Invalid_argument "non-empty indexing stack"] if
     59                [inds] is empty. *)
     60val forget_const_ind : const_indexing list -> const_indexing list
     61
     62
     63 
    3364
    3465(** [empty_indexing] generates an empty indexing *)
     
    4576}
    4677
    47 val apply_const_indexing : const_indexing -> t -> t
    48 
     78(** [apply_const_indexing ind lbl] returns [lbl] where its indexing has been
     79    evaluated in the constant indexing [ind].
     80                @raise  Invalid_argument "constant indexing not enough to be applied" if
     81                [ind] does not contain enough mappings to evaluate [lbl]'s indexing. *)
     82val ev_indexing : const_indexing -> t -> t
    4983
    5084(** [string_of_cost_label pref t] converts an indexed label to a
  • Deliverables/D2.2/8051-indexed-labels-branch/src/utilities/extArray.ml

    r1349 r1357  
    1 type +'a t = {
     1type 'a t = {
    22        mutable t_cont : 'a array;
    33        mutable t_length : int;
     
    55}
    66
    7 let default_buffer_size = 4
    8 
    9 let make n a =
    10         let m = min default_buffer_size n in
     7let make ?(buff = 16) n a =
     8        let m = max 1 (max buff n) in
    119        {t_cont = Array.make m a; t_length = n; t_def = a}
    1210       
     
    2018let length v = v.t_length
    2119
    22 let chop v n = v.t_length <- max 0 (v.t_length - n)
     20let chop v n =
     21        let n = min n v.t_length in
     22        Array.fill v.t_cont (v.t_length - n) v.t_length v.t_def; 
     23        v.t_length <- v.t_length - n
    2324
    24 let assure v n =
     25let ensure v n =
    2526        let m = Array.length v.t_cont in
    26         (if n >= m then
     27        if n >= m then
    2728                let d = n / m + 1 in
    2829                let new_arr = Array.make (d * m) v.t_def in
    2930                Array.blit v.t_cont 0 new_arr 0 m;
    30                 v.t_cont <- new_arr);
    31    v.t_length <- max v.t_length (m + 1)
     31                v.t_cont <- new_arr;
     32        else ();
     33  v.t_length <- max (n + 1) v.t_length
    3234
    3335       
    3436       
    35 let extend v n = assure v (v.t_length + n)
     37let extend v n = ensure v (v.t_length + n - 1)
    3638
    3739let set v n a =
    3840          (if n < 0 then invalid_arg "out of bounds");
    39     assure v n;
    40                 v.t_cont.(n) <- a;
     41    ensure v n;
     42                v.t_cont.(n) <- a
    4143
    4244let append v a = set v (v.t_length) a
    43        
     45
     46let reclaim ?(packet = 16) v =
     47  let new_l = v.t_length - (v.t_length - 1) mod packet + packet - 1 in
     48        let new_l = max 1 new_l in
     49        if new_l <> Array.length v.t_cont then
     50                let new_cont = Array.make new_l v.t_def in
     51                Array.blit v.t_cont 0 new_cont 0 v.t_length;
     52                v.t_cont <- new_cont
     53
     54exception Finish_iter
     55
     56let iteri f v =
     57        let f' i a = if i < v.t_length then f i a else raise Finish_iter in
     58        try Array.iteri f' v.t_cont with Finish_iter -> ()
     59       
     60let iter f = iteri (fun _ -> f)
     61
     62let fold_left f a v =
     63        let res = ref a in
     64        let f' b = res := f !res b in
     65        iter f' v; !res
     66
     67let fold_right f v a =
     68        let funct = ref (fun x -> x) in
     69        let f' b = let funct' = !funct in funct := fun x -> funct' (f b x) in
     70        iter f' v; !funct a
     71
     72       
    4473       
    4574
  • Deliverables/D2.2/8051-indexed-labels-branch/src/utilities/extArray.mli

    r1349 r1357  
    1 (** This module provides extensible arrays with limited functionality. *)
     1(** This module provides simple extensible arrays. *)
    22
    33(** The type of extensible arrays with elements in ['a]. *)
    4 type +'a t
     4type 'a t
    55
    66(** [make n a] creates an extensible array with initial size [n]
    7     and default element [a]. *) 
    8 val make : int -> 'a -> 'a t
     7    and default element [a]. The optional argument [buff] sets the
     8                initial buffer size (16 by default, set to 1 if [buff < 1]). *) 
     9val make : ?buff:int -> int -> 'a -> 'a t
    910
    10 (** [detault v] returns the current default element of v **)
     11(** [detault v] returns the default element of v, which fills unspecified
     12    cells when extending the array. *)
    1113val default : 'a t -> 'a
    1214
     15(** [get v n] gets the element in [v] at [n]. Raises
     16    [Invalid_argument "out of bounds"] if [n < 0] or [n >= length v]. *)
    1317val get : 'a t -> int -> 'a
    1418
    15 val set : 'a t -> int -> a -> unit
     19(** [set v n x] sets the element in [v] at [n] to [x]. Raises
     20    [Invalid_argument "out of bounds"] if [n < 0], but fills the
     21                array as needed with [default v] if [n >= length v]. The final length
     22                is thus [max (length v) (n + 1)]. *)
     23val set : 'a t -> int -> 'a -> unit
    1624
     25(** [length v] returns the current length of the array. *)
    1726val length : 'a t -> int
    1827
     28(** [chop v n] erases the last [n] elements of [v], or all the elements of [v]
     29    if [n >= length v]. The final length is thus [max 0 (length v - n)].
     30                Implementation note: this function does not free any memory. *)
    1931val chop : 'a t -> int -> unit
    2032
     33(** [extend v n] adds [n] default elements at the end of the array. It is
     34    equivalent to [append v (default v); ... ; append v (default v)] [n]
     35                times. *) 
    2136val extend : 'a t -> int -> unit
    2237
    23 val assure : 'a t -> int -> unit
     38(** [ensure v n] will ensure [n >= 0] is inside the bounds of the array [v].
     39    To this end it will add [default v] elements at the end of [v] if necessary.
     40                It does nothing if [n < 0]. *)
     41val ensure : 'a t -> int -> unit
    2442
     43(** [append v a] appends [a] at the end of [v], with the length of [v] being
     44    thus raised by [1]. It is equivalent to [set v (length v) a]. *)
    2545val append : 'a t -> 'a -> unit
     46
     47(** [reclaim v] will shrink the memory imprint of [v] roughly to a multiple
     48    of [packet] (16 by default), without changinb [v]'s content. The effect
     49                depends on garbage collection. *)
     50val reclaim : ?packet:int -> 'a t -> unit
     51
     52(** [iter f v] iterates [f] over the elements of [v]. *)
     53val iter : ('a -> unit) -> 'a t -> unit
     54(** [fold_left f x v] computes [f (... (f (f x (get v 0)) (get v 1)) ...)
     55    (get v (n-1))], where [n] is the length of [v]. *)
     56val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a   
     57
     58(** [fold_right f v x] computes [f (get v 0) (... (f (get v (n-1)) x)...)],
     59    where [n] is the length of [v]. *)
     60val fold_right : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
Note: See TracChangeset for help on using the changeset viewer.