Changeset 1539 for Deliverables/D2.2


Ignore:
Timestamp:
Nov 23, 2011, 1:55:12 PM (8 years ago)
Author:
tranquil
Message:

branch up to date

Location:
Deliverables/D2.2/8051-indexed-labels-branch/src
Files:
60 edited
6 copied

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASM.mli

    r1349 r1539  
    104104 | `Cost of CostLabel.t
    105105 | `Index of int
    106  | `Inc of int 
     106 | `Inc of int
    107107 | `Label of string
    108108 | `Jmp of string
    … …  
    127127      incs        : int BitVectors.WordMap.t ; (* loop index increments *)
    128128      cost_labels : CostLabel.t BitVectors.WordMap.t ;
     129      labels      : BitVectors.word StringTools.Map.t ;
     130
    129131      exit_addr   : BitVectors.word ;
    130132      has_main    : bool }

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMCosts.ml

    r643 r1539  
    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-indexed-labels-branch/src/ASM/ASMInterpret.ml

    r1357 r1539  
    133133       
    134134(*
    135         ind_0s      : int BitVectors.WordMap.t;
     135  ind_0s      : int BitVectors.WordMap.t;
    136136  ind_incs    : int BitVectors.WordMap.t;
    137137  cost_labels : CostLabel.t BitVectors.WordMap.t
    … …  
    966966      | `Label s -> pc, exit_addr, StringTools.Map.add s pc labels, inds, incs, costs
    967967      | `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
     968      | `Index i -> pc, exit_addr, labels, BitVectors.WordMap.add pc i inds, incs, costs
    969969      | `Inc i -> pc, exit_addr, labels, inds, BitVectors.WordMap.add pc i incs, costs
    970       | `Mov (_,_) -> (snd (half_add pc (vect_of_int 1 `Sixteen))), exit_addr, labels, inds, incs, costs
     970      | `Mov (_,_) -> (snd (half_add pc (vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs
     971
    971972      | `Jmp _
    972973      | `Call _ -> (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))), exit_addr, labels, inds, incs, costs
    … …  
    986987    (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen,
    987988     StringTools.Map.empty, BitVectors.WordMap.empty, BitVectors.WordMap.empty,
    988                 BitVectors.WordMap.empty) p.ASM.pcode
     989    BitVectors.WordMap.empty) p.ASM.pcode
    989990 in
    990991 let code =
    … …  
    993994        `Label _
    994995      | `Cost _
    995                         | `Index _
    996                         | `Inc _ -> []
     996      | `Index _
     997      | `Inc _ -> []
    997998      | `WithLabel i ->
    998999         (* We need to expand a conditional jump to a label to a machine language
    … …  
    10461047                 address, reconstructed
    10471048         in
    1048            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
    10491051           let translation = [ translated_jump; sjmp; jmp ] in
    10501052             List.flatten (List.map assembly1 translation)
    10511053      | `Mov (`DPTR,s) ->
    1052           let addrr16 = StringTools.Map.find s datalabels in
    1053            assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
     1054          (* let addr16 = StringTools.Map.find s datalabels in *)
     1055          let addrr16 =
     1056            try StringTools.Map.find s datalabels
     1057            with Not_found -> StringTools.Map.find s labels in
     1058          assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
    10541059      | `Jmp s ->
    10551060          let pc_offset = StringTools.Map.find s labels in
    … …  
    10591064            assembly1 (`LCALL (`ADDR16 pc_offset ))
    10601065      | #instruction as i -> assembly1 i) p.ASM.pcode) in
    1061  { ASM.code = code ; ASM.inds = inds; ASM.incs = incs; ASM.cost_labels = costs ;
     1066 { ASM.code = code ;
     1067   ASM.inds = inds; ASM.incs = incs; ASM.cost_labels = costs ;
     1068   ASM.labels = StringTools.Map.empty ;
    10621069   ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main }
    10631070;;
    … …  
    19881995
    19891996type cost_trace = {
    1990         mutable ct_labels : CostLabel.t list;
    1991         mutable ct_inds   : CostLabel.const_indexing list;
     1997  mutable ct_labels : CostLabel.t list;
     1998  mutable ct_inds   : CostLabel.const_indexing list;
    19921999}
    19932000
    1994 (* TODO: supposing only one index reset or increment per instruction *)
     2001(* FIXME: supposing only one index reset or increment per instruction *)
    19952002let update_indexes trace p st =
    19962003  try
    19972004    let i = BitVectors.WordMap.find st.pc p.ASM.inds in
    1998                 CostLabel.enter_loop trace.ct_inds i
     2005    CostLabel.enter_loop trace.ct_inds i
    19992006  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                 | _ -> ()
     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        | _ -> ()
    20112018
    20122019let update_labels trace p st =
    20132020  try
    20142021    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
     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
    20182025  with Not_found -> ()
    20192026
    … …  
    20212028
    20222029let update_trace trace p st =
    2023         update_labels trace p st;
    2024         update_indexes trace p st;
     2030  update_labels trace p st;
     2031  update_indexes trace p st;
    20252032  if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st
    20262033
    … …  
    20482055    (res, List.rev trace.ct_labels)
    20492056  else (IntValue.Int32.zero, [])
     2057
     2058
     2059let size_of_instr instr =
     2060  let exit_lbl = "exit" in
     2061  let p = { ASM.ppreamble = [] ; ASM.pexit_label = exit_lbl ;
     2062            ASM.pcode = [instr ; `Label exit_lbl] ; ASM.phas_main = false } in
     2063  let p = assembly p in
     2064  let status = load_program p in
     2065  let addr_zero = BitVectors.vect_of_int 0 `Sixteen in
     2066  let (_, size, _) = fetch status.code_memory addr_zero in
     2067  BitVectors.int_of_vect size
     2068
     2069let size_of_instrs instrs =
     2070  let f res instr = res + (size_of_instr instr) in
     2071  List.fold_left f 0 instrs

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/ASMInterpret.mli

    r1357 r1539  
    133133val load_program : ASM.program -> status
    134134val interpret    : bool -> ASM.program -> AST.trace
     135
     136val size_of_instrs : ASM.labelled_instruction list -> int

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/I8051.ml

    r818 r1539  
    170170let rets = [dpl ; dph ; r00 ; r01]
    171171
     172let spl_addr = spl
     173let spl_init = 255
     174let sph_addr = sph
     175let sph_init = 255
    172176let isp_addr = 129
    173177let isp_init = 47

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/I8051.mli

    r818 r1539  
    5555val carry : register (* only used for the liveness analysis *)
    5656
     57val spl_addr : int
     58val spl_init : int
     59val sph_addr : int
     60val sph_init : int
    5761val isp_addr : int
    5862val isp_init : int

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ASM/Pretty.ml

    r1357 r1539  
    4444    `Label l -> l ^ ":"
    4545  | `Cost l -> CostLabel.string_of_cost_label ~pretty:true l ^ ":"
    46         | `Index i -> "index " ^ string_of_int i ^ ":"
     46  | `Index i -> "index " ^ string_of_int i ^ ":"
    4747  | `Inc i -> "increment " ^ string_of_int i ^ ":"
    4848  | `Jmp j -> "ljmp  " ^ j
    … …  
    9999
    100100let find_comment p pc =
    101         let s1 =
    102                 try
    103                         let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in
     101  let s1 =
     102    try
     103      let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in
    104104      ", " ^ CostLabel.string_of_cost_label ~pretty:true lbl
    105105    with Not_found -> "" in
    106         let s2 =
     106  let s2 =
    107107    try
    108108      let i = BitVectors.WordMap.find pc p.ASM.inds in
    109109      ", index " ^ string_of_int i
    110110    with Not_found -> "" in
    111         let s3 =
     111  let s3 =
    112112    try
    113113      let i = BitVectors.WordMap.find pc p.ASM.incs in
    114114      ", inc " ^ string_of_int i
    115115    with Not_found -> "" in
    116         s1 ^ s2 ^ s3
     116  s1 ^ s2 ^ s3
    117117                       
    118118
    … …  
    126126       (pp_instruction inst)
    127127       cost
    128                         (find_comment p pc),
     128      (find_comment p pc),
    129129     new_pc) in
    130130  fst (List.fold_left f ("", BitVectors.zero `Sixteen) p.ASM.code)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTL.mli

    r1345 r1539  
    150150  | St_call_id of AST.ident * int * Label.t
    151151
     152  (* Call to a function given its address. Parameters are the registers holding
     153     the address of the function, the number of arguments of the function, and
     154     the label of the next statement. *)
     155  | St_call_ptr of Register.t * Register.t * int * Label.t
     156
    152157(*
    153   (* Call to a function given its address. Parameters are registers holding the
    154      address of the function, the arguments of the function, the destination
    155      registers, and the label of the next statement. *)
    156   | St_call_ptr of registers * register list * registers * Label.t
    157 
    158158  (* Tail call to a function given its name. Parameters are the name of the
    159      function, and the number of arguments of the function. *)
     159    function, and the number of arguments of the function. *)
    160160  | St_tailcall_id of AST.ident * int
    161161

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLInterpret.ml

    r1357 r1539  
    4646      renv   : hdw_reg_env ;
    4747      mem    : memory ;
    48                         inds   : indexing list;
     48      inds   : indexing list;
    4949      trace  : CostLabel.t list }
    5050
    … …  
    8080    renv   = I8051.RegisterMap.empty ;
    8181    mem    = Mem.empty ;
    82                 inds   = [] ;
     82    inds   = [] ;
    8383    trace  = [] }
    8484
    … …  
    127127  let lenv = Register.Set.fold f def.ERTL.f_locals Register.Map.empty in
    128128  let pc = entry_pc lbls_offs ptr def in
    129         let st = new_ind st in
     129  let st = new_ind st in
    130130  change_lenv (change_pc st pc) lenv
    131131
    … …  
    203203  st
    204204
     205let make_addr st r1 r2 = List.map (fun r -> get_reg (Psd r) st) [r1 ; r2]
     206
    205207
    206208module InterpretExternal = Primitive.Interpret (Mem)
    … …  
    226228  change_pc st next_pc
    227229
    228 let interpret_call lbls_offs st f ra =
    229   let ptr = Mem.find_global st.mem f in
     230let interpret_call lbls_offs st ptr ra =
     231  (* let ptr = Mem.find_global st.mem f in *)
    230232  match Mem.find_fun_def st.mem ptr with
    231233    | ERTL.F_int def ->
    … …  
    239241
    240242let interpret_return lbls_offs st =
    241         let st = forget_ind st in
     243  let st = forget_ind st in
    242244  let st = pop_st_frs st in
    243245  let (st, pch) = pop st in
    … …  
    263265
    264266    | ERTL.St_cost (cost_lbl, lbl) ->
    265                         let cost_lbl = ev_label st cost_lbl in
     267      let cost_lbl = ev_label st cost_lbl in
    266268      let st = add_trace st cost_lbl in
    267269      next_pc st lbl
    268270
    269271    | ERTL.St_ind_0 (i, lbl) ->
    270                         enter_loop st i;
    271                         next_pc st lbl
     272      enter_loop st i;
     273      next_pc st lbl
    272274
    273275    | ERTL.St_ind_inc (i, lbl) ->
    … …  
    373375
    374376    | ERTL.St_load (destr, addr1, addr2, lbl) ->
    375       let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
     377      let addr = make_addr st addr1 addr2 in
    376378      let v = Mem.load st.mem chunk addr in
    377379      let st = add_reg (Psd destr) v st in
    … …  
    379381
    380382    | ERTL.St_store (addr1, addr2, srcr, lbl) ->
    381       let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
     383      let addr = make_addr st addr1 addr2 in
    382384      let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
    383385      let st = change_mem st mem in
    … …  
    385387
    386388    | ERTL.St_call_id (f, _, lbl) ->
    387       interpret_call lbls_offs st f lbl
     389      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
     390
     391    | ERTL.St_call_ptr (f1, f2, _, lbl) ->
     392      interpret_call lbls_offs st (make_addr st f1 f2) lbl
    388393
    389394    | ERTL.St_cond (srcr, lbl_true, lbl_false) ->

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLPrinter.ml

    r1345 r1539  
    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
     45    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    4646    Printf.sprintf "emit %s --> %s" cost_lbl lbl
    4747  | ERTL.St_ind_0 (i, lbl) ->
    … …  
    121121      lbl
    122122  | ERTL.St_call_id (f, nb_args, lbl) ->
    123     Printf.sprintf "call \"%s\", %d --> %s"
    124       f
     123    Printf.sprintf "call \"%s\", %d --> %s" f nb_args lbl
     124  | ERTL.St_call_ptr (f1, f2, nb_args, lbl) ->
     125    Printf.sprintf "call_ptr [%s ; %s], %d --> %s"
     126      (Register.print f1)
     127      (Register.print f2)
    125128      nb_args
    126129      lbl
    127130(*
    128   | ERTL.St_call_ptr (f, args, dstrs, lbl) ->
    129     Printf.sprintf "call_ptr %s, %s, %s --> %s"
    130       (print_ptr f)
    131       (print_args args)
    132       (print_return dstrs)
    133       lbl
    134131  | ERTL.St_tailcall_id (f, nb_args) ->
    135132    Printf.sprintf "tailcall \"%s\", %d"

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/ERTLToLTLI.ml

    r1345 r1539  
    163163
    164164      | ERTL.St_cost (cost_lbl, l) ->
    165     LTL.St_cost (cost_lbl, l)
     165        LTL.St_cost (cost_lbl, l)
    166166
    167167      | ERTL.St_ind_0 (i, l) ->
    168     LTL.St_ind_0 (i, l)
     168        LTL.St_ind_0 (i, l)
    169169
    170170      | ERTL.St_ind_inc (i, l) ->
    171     LTL.St_ind_inc (i, l)
     171        LTL.St_ind_inc (i, l)
    172172
    173173      | ERTL.St_get_hdw (destr, sourcehwr, l) ->
    … …  
    289289        LTL.St_call_id (f, l)
    290290
     291      | ERTL.St_call_ptr (f1, f2, _, l) ->
     292        let l = generate (LTL.St_call_ptr l) in
     293        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
     294        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
     295        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
     296        let l = read f1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     297        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
     298        let l = read f2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
     299        LTL.St_skip l
     300
    291301      | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
    292302        let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/liveness.ml

    r1468 r1539  
    4040  | St_load (_, _, _, l)
    4141  | St_store (_, _, _, l)
    42   | St_call_id (_, _, l) ->
     42  | St_call_id (_, _, l)
     43  | St_call_ptr (_, _, _, l) ->
    4344    Label.Set.singleton l
    4445  | St_cond (_, l1, l2) ->
    … …  
    9394  | St_comment _
    9495  | St_cost _
    95         | St_ind_0 _
    96         | St_ind_inc _
     96  | St_ind_0 _
     97  | St_ind_inc _
    9798  | St_push _
    9899  | St_store _
    … …  
    124125  | St_hdw_to_hdw (r, _, _) ->
    125126    L.hsingleton r
    126   | St_call_id _ ->
     127  | St_call_id _ | St_call_ptr _  ->
    127128      (* Potentially destroys all caller-save hardware registers. *)
    128129    Register.Set.empty, I8051.caller_saved
    … …  
    160161    (* Reads the hardware registers that are used to pass parameters. *)
    161162    Register.Set.empty,
     163    set_of_list (MiscPottier.prefix nparams I8051.parameters)
     164  | St_call_ptr (r1, r2, nparams, _) ->
     165    (* Reads the hardware registers that are used to pass parameters. *)
     166    Register.Set.of_list [r1 ; r2],
    162167    set_of_list (MiscPottier.prefix nparams I8051.parameters)
    163168  | St_get_hdw (_, r, _)
    … …  
    213218  | St_store _
    214219  | St_call_id _
     220  | St_call_ptr _
    215221  | St_cond _
    216222  | St_return _ ->

  • Deliverables/D2.2/8051-indexed-labels-branch/src/ERTL/uses.ml

    r1345 r1539  
    4141    count r uses
    4242  | St_move (r1, r2, _)
    43   | St_op1 (_, r1, r2, _) ->
     43  | St_op1 (_, r1, r2, _)
     44  | St_call_ptr (r1, r2, _, _) ->
    4445    count r1 (count r2 uses)
    4546  | St_opaccsA (_, r1, r2, r3, _)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LIN.mli

    r1349 r1539  
    7373  | St_call_id of AST.ident
    7474
     75  (* Call to a function given its address in DPTR. *)
     76  | St_call_ptr
     77
    7578  (* Branch on A accumulator. Parameter is the label to go to when the A
    7679     accumulator is not 0. *)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINInterpret.ml

    r1357 r1539  
    3434      renv   : hdw_reg_env ;
    3535      mem    : memory ;
    36                         inds   : indexing list ;
     36      inds   : indexing list ;
    3737      trace  : CostLabel.t list }
    3838
    … …  
    6161    renv   = I8051.RegisterMap.empty ;
    6262    mem    = Mem.empty ;
    63                 inds   = [] ;
     63    inds   = [] ;
    6464    trace  = [] }
    6565
    … …  
    8181  else error msg
    8282
    83 let init_fun_call st ptr def =
    84         let st = new_ind st in
     83let init_fun_call st ptr =
     84  let st = new_ind st in
    8585  change_pc st (Val.change_address_offset ptr Val.Offset.zero)
    8686
    … …  
    177177  set_result st vs
    178178
    179 let interpret_call st f =
    180   let ptr = Mem.find_global st.mem f in
     179let interpret_call st ptr =
    181180  match Mem.find_fun_def st.mem ptr with
    182181    | LIN.F_int def ->
    183182      let st = save_ra st in
    184       init_fun_call st ptr def
     183      init_fun_call st ptr
    185184    | LIN.F_ext def ->
    186185      let st = next_pc st in
    … …  
    188187
    189188let interpret_return st =
    190         let st = forget_ind st in
     189  let st = forget_ind st in
    191190  let (st, pc) = return_pc st in
    192191  change_pc st pc
    … …  
    208207
    209208    | LIN.St_cost cost_lbl ->
    210                         let cost_lbl = ev_label st cost_lbl in
     209      let cost_lbl = ev_label st cost_lbl in
    211210      let st = add_trace st cost_lbl in
    212211      next_pc st
    213                        
    214                 | LIN.St_ind_0 i ->
    215                         enter_loop st i;
    216                         next_pc st
     212
     213    | LIN.St_ind_0 i ->
     214      enter_loop st i;
     215      next_pc st
    217216
    218217    | LIN.St_ind_inc i ->
    219             continue_loop st i;
    220             next_pc st
     218      continue_loop st i;
     219      next_pc st
    221220
    222221    | LIN.St_int (r, i) ->
    … …  
    292291
    293292    | LIN.St_call_id f ->
    294       interpret_call st f
     293      interpret_call st (Mem.find_global st.mem f)
     294
     295    | LIN.St_call_ptr ->
     296      interpret_call st (dptr st)
    295297
    296298    | LIN.St_condacc lbl_true ->
    … …  
    369371  match Mem.find_fun_def st.mem ptr with
    370372    | LIN.F_int def ->
    371       init_fun_call st ptr def
     373      init_fun_call st ptr
    372374    | _ -> error ("Cannot execute the main (\"" ^ main ^ "\"): it is external.")
    373375

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINPrinter.ml

    r1392 r1539  
    33
    44
    5 let n_spaces ?stmt n =
    6         let n = match stmt with
    7                 | Some (LIN.St_label _) | Some (LIN.St_cost _) -> n - 2
    8                 | _ -> n in
    9         String.make n ' '
     5let n_spaces n = String.make n ' '
    106
    117
    … …  
    3127  | LIN.St_cost cost_lbl ->
    3228    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    33                 Printf.sprintf "emit %s" cost_lbl
     29    Printf.sprintf "emit %s" cost_lbl
    3430  | LIN.St_ind_0 i ->
    3531    Printf.sprintf "index %d" i
    … …  
    6359    Printf.sprintf "movex @DPTR, %s" print_a
    6460  | LIN.St_call_id f -> Printf.sprintf "call \"%s\"" f
     61  | LIN.St_call_ptr ->
     62    Printf.sprintf "call_ptr DPTR"
    6563  | LIN.St_condacc lbl_true ->
    6664    Printf.sprintf "branch %s <> 0, %s" print_a lbl_true
    … …  
    7068let print_code n c =
    7169  let f s stmt =
    72     Printf.sprintf "%s\n%s%s" s (n_spaces ~stmt:stmt n) (print_statement stmt) in
     70    Printf.sprintf "%s\n%s%s" s (n_spaces n) (print_statement stmt) in
    7371  List.fold_left f "" c
    7472

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LIN/LINToASM.ml

    r1349 r1539  
    77
    88
     9(* Translation environment *)
     10
     11type env =
     12    { externals : AST.ident list ;
     13      exit_lbl : Label.t ;
     14      fresh : unit -> string }
     15
     16let make_env externals exit_lbl fresh =
     17  { externals = externals ;
     18    exit_lbl = exit_lbl ;
     19    fresh = fresh }
     20
     21
    922(* Fetch the labels found in a LIN program. *)
    1023
    … …  
    1326  | LIN.St_label lbl
    1427  | LIN.St_condacc lbl -> Label.Set.singleton lbl
    15         (* quite dubious about the following *)
    16   | LIN.St_cost lbl -> Label.Set.singleton (CostLabel.string_of_cost_label lbl)
     28    (* taking the atom as a fresh prefix will be generated *)
     29  | LIN.St_cost lbl -> Label.Set.singleton (lbl.CostLabel.name)
    1730  | _ -> Label.Set.empty
    1831
    … …  
    4457let data16_of_int i = `DATA16 (vect_of_int i `Sixteen)
    4558let acc_addr = I8051.reg_addr I8051.a
     59let dpl_addr = I8051.reg_addr I8051.dpl
     60let dph_addr = I8051.reg_addr I8051.dph
     61let st0_addr = I8051.reg_addr I8051.st0
     62let st1_addr = I8051.reg_addr I8051.st1
    4663
    4764
    48 let translate_statement glbls_addr = function
     65let translate_statement env = function
    4966  | LIN.St_goto lbl -> [`Jmp lbl]
    5067  | LIN.St_label lbl -> [`Label lbl]
    5168  | LIN.St_comment _ -> []
    52   | LIN.St_cost lbl -> [`Cost lbl ; `NOP (* TODO: hack! Need to make the difference between cost labels and regular labels. *)]
     69  | LIN.St_cost lbl ->
     70    (* TODO: hack! Need to make the difference between cost labels and regular
     71       labels. *)
     72    [`Cost lbl ; `NOP ]
    5373  | LIN.St_ind_0 i -> [`Index i ; `NOP (* TODO: hack! *)]
    5474  | LIN.St_ind_inc i -> [`Inc i ; `NOP (* TODO: hack! *)]
    … …  
    5979  | LIN.St_push ->
    6080    [`PUSH acc_addr]
    61   | LIN.St_addr x when List.mem_assoc x glbls_addr ->
    62     [`MOV (`U4 (`DPTR, data16_of_int (List.assoc x glbls_addr)))]
     81  | LIN.St_addr x when List.mem x env.externals ->
     82    error ("Primitive or external " ^ x ^ " is not supported.")
    6383  | LIN.St_addr x ->
    64     error ("unknown global " ^ x ^ ".")
     84    [`Mov (`DPTR, x)]
    6585  | LIN.St_from_acc r ->
    6686    [`MOV (`U3 (I8051.reg_addr r, `A))]
    … …  
    95115  | LIN.St_store ->
    96116    [`MOVX (`U2 (`EXT_IND_DPTR, `A))]
     117  | LIN.St_call_id x when List.mem x env.externals ->
     118    error ("Primitive or external " ^ x ^ " is not supported.")
    97119  | LIN.St_call_id f ->
    98120    [`Call f]
     121  | LIN.St_call_ptr ->
     122    let lbl = env.fresh () in
     123    [`MOV (`U3 (st0_addr, dpl_addr)) ; (* save DPL *)
     124     `MOV (`U3 (st1_addr, dph_addr)) ; (* save DPH *)
     125     `Mov (`DPTR, lbl) ;               (* DPTR <- return address *)
     126     `PUSH dpl_addr ;                  (* push DPL *)
     127     `PUSH dph_addr ;                  (* push DPH *)
     128     `MOV (`U3 (dpl_addr, st0_addr)) ; (* restore DPL *)
     129     `MOV (`U3 (dph_addr, st1_addr)) ; (* restore DPH *)
     130     `MOV (`U1 (`A, data_of_int 0)) ;  (* A <- 0 *)
     131     `JMP `IND_DPTR ;                  (* jump to A+DPTR *)
     132     `Label lbl]                       (* return address *)
    99133  | LIN.St_condacc lbl ->
    100134    [`WithLabel (`JNZ (`Label lbl))]
    … …  
    102136    [`RET]
    103137
    104 let translate_code glbls_addr code =
    105   List.flatten (List.map (translate_statement glbls_addr) code)
     138let translate_code env code =
     139  List.flatten (List.map (translate_statement env) code)
    106140
    107141
    108 let translate_fun_def glbls_addr (id, def) = match def with
    109   | LIN.F_int code -> (`Label id) :: (translate_code glbls_addr code)
    110   | LIN.F_ext ext ->
    111     error ("potential call to unsupported external " ^ ext.AST.ef_tag ^ ".")
     142let translate_fun_def env (id, def) =
     143  let code = match def with
     144  | LIN.F_int code -> translate_code env code
     145  | LIN.F_ext ext -> [`NOP] in
     146  ((`Label id) :: code)
    112147
    113 let translate_functs glbls_addr exit_label main functs =
     148let translate_functs env main functs =
    114149  let preamble = match main with
    115150    | None -> []
    … …  
    117152      [`MOV (`U3 (`DIRECT (byte_of_int I8051.isp_addr),
    118153                  data_of_int I8051.isp_init)) ;
     154       `MOV (`U3 (`DIRECT (byte_of_int I8051.spl_addr),
     155                  data_of_int I8051.spl_init)) ;
     156       `MOV (`U3 (`DIRECT (byte_of_int I8051.sph_addr),
     157                  data_of_int I8051.sph_init)) ;
    119158       `Call main ;
    120        `Label exit_label ; `Jmp exit_label] in
    121   preamble @
    122   (List.flatten (List.map (translate_fun_def glbls_addr) functs))
     159       `Label env.exit_lbl ; `Jmp env.exit_lbl] in
     160  preamble @ (List.flatten (List.map (translate_fun_def env) functs))
    123161
    124162
    125 let globals_addr l =
    126   let f (res, offset) (x, size) = ((x, offset) :: res, offset + size) in
    127   fst (List.fold_left f ([], 0) l)
     163let init_env p =
     164  let f_externals (id, def) = match def with LIN.F_ext _ -> [id] | _ -> [] in
     165  let externals =
     166    List.fold_left (fun res def -> res @ (f_externals def)) [] p.LIN.functs in
     167  let prog_lbls = prog_labels p in
     168  let exit_lbl = Label.Gen.fresh_prefix prog_lbls "_exit" in
     169  let fresh = Label.make_fresh prog_lbls "_call_ret" in
     170  make_env externals exit_lbl fresh
    128171
    129172
    … …  
    134177
    135178let translate p =
    136   let prog_lbls = prog_labels p in
    137   let exit_label = Label.Gen.fresh_prefix prog_lbls "_exit" in
    138   let glbls_addr = globals_addr p.LIN.vars in
     179  let env = init_env p in
    139180  let p =
    140181    { ASM.ppreamble = p.LIN.vars ;
    141       ASM.pexit_label = exit_label ;
    142       ASM.pcode =
    143         translate_functs glbls_addr exit_label p.LIN.main p.LIN.functs ;
     182      ASM.pexit_label = env.exit_lbl ;
     183      ASM.pcode = translate_functs env p.LIN.main p.LIN.functs ;
    144184      ASM.phas_main = p.LIN.main <> None } in
    145185  ASMInterpret.assembly p

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTL.mli

    r1345 r1539  
    8181  | St_call_id of AST.ident * Label.t
    8282
     83  (* Call to a function given its address in DPTR. Parameter is the label of the
     84     next statement. *)
     85  | St_call_ptr of Label.t
     86
    8387  (* Branch on A accumulator. Parameters are the label to go to when the A
    8488     accumulator is not 0, and the label to go to when the A accumulator is

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLInterpret.ml

    r1357 r1539  
    3131      renv   : hdw_reg_env ;
    3232      mem    : memory ;
    33                         inds   : CostLabel.const_indexing list ;
     33      inds   : CostLabel.const_indexing list ;
    3434      trace  : CostLabel.t list }
    3535
    … …  
    5858    renv   = I8051.RegisterMap.empty ;
    5959    mem    = Mem.empty ;
    60                 inds   = [] ;
     60    inds   = [] ;
    6161    trace  = [] }
    6262
    … …  
    102102let init_fun_call lbls_offs st ptr def =
    103103  let pc = entry_pc lbls_offs ptr def in
    104         let st = new_ind st in
     104  let st = new_ind st in
    105105  change_pc st pc
    106106
    … …  
    204204  change_pc st next_pc
    205205
    206 let interpret_call lbls_offs st f ra =
    207   let ptr = Mem.find_global st.mem f in
     206let interpret_call lbls_offs st ptr ra =
    208207  match Mem.find_fun_def st.mem ptr with
    209208    | LTL.F_int def ->
    … …  
    216215
    217216let interpret_return lbls_offs st =
    218         let st = forget_ind st in
     217  let st = forget_ind st in
    219218  let (st, pc) = return_pc st in
    220219  change_pc st pc
    … …  
    237236
    238237    | LTL.St_cost (cost_lbl, lbl) ->
    239                         let cost_lbl = ev_label st cost_lbl in
     238      let cost_lbl = ev_label st cost_lbl in
    240239      let st = add_trace st cost_lbl in
    241240      next_pc st lbl
    242241
    243242    | LTL.St_ind_0 (i, lbl) ->
    244             enter_loop st i;
    245             next_pc st lbl
     243      enter_loop st i;
     244      next_pc st lbl
    246245
    247246    | LTL.St_ind_inc (i, lbl) ->
    … …  
    249248      next_pc st lbl
    250249
    251                 | LTL.St_int (r, i, lbl) ->
     250    | LTL.St_int (r, i, lbl) ->
    252251      let st = add_reg r (Val.of_int i) st in
    253252      next_pc st lbl
    … …  
    321320
    322321    | LTL.St_call_id (f, lbl) ->
    323       interpret_call lbls_offs st f lbl
     322      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
     323
     324    | LTL.St_call_ptr lbl ->
     325      interpret_call lbls_offs st (dptr st) lbl
    324326
    325327    | LTL.St_condacc (lbl_true, lbl_false) ->

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLPrinter.ml

    r1345 r1539  
    6060    Printf.sprintf "movex @DPTR, %s --> %s" print_a lbl
    6161  | LTL.St_call_id (f, lbl) -> Printf.sprintf "call \"%s\" --> %s" f lbl
     62  | LTL.St_call_ptr lbl ->
     63    Printf.sprintf "call_ptr DPTR --> %s" lbl
    6264  | LTL.St_condacc (lbl_true, lbl_false) ->
    6365    Printf.sprintf "branch %s <> 0 --> %s, %s" print_a lbl_true lbl_false

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLToLIN.ml

    r1349 r1539  
    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
     24  | LTL.St_ind_0 (i, _) ->
     25    LIN.St_ind_0 i
     26  | LTL.St_ind_inc (i, _) ->
     27    LIN.St_ind_inc i
    2828  | LTL.St_int (r, i, _) ->
    2929    LIN.St_int (r, i)
    … …  
    5454  | LTL.St_call_id (f, _) ->
    5555    LIN.St_call_id f
     56  | LTL.St_call_ptr _ ->
     57    LIN.St_call_ptr
    5658
    5759  (* Conditional branch statement. In [LIN], control implicitly

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLToLINI.ml

    r1349 r1539  
    132132        | LTL.St_load l
    133133        | LTL.St_store l
    134         | LTL.St_call_id (_, l) ->
     134        | LTL.St_call_id (_, l)
     135        | LTL.St_call_ptr l ->
    135136
    136137          visit l

  • Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/branch.ml

    r1345 r1539  
    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)
     54    | LTL.St_ind_0 (i, l) ->
     55      LTL.St_ind_0 (i, rep l)
    5656    | LTL.St_ind_inc (i, l) ->
    57             LTL.St_ind_inc (i, rep l)
     57      LTL.St_ind_inc (i, rep l)
    5858    | LTL.St_int (r, i, l) ->
    5959      LTL.St_int (r, i, rep l)
    … …  
    8484    | LTL.St_call_id (f, l) ->
    8585      LTL.St_call_id (f, rep l)
     86    | LTL.St_call_ptr l ->
     87      LTL.St_call_ptr (rep l)
    8688    | LTL.St_condacc (lbl_true, lbl_false) ->
    8789      LTL.St_condacc (rep lbl_true, rep lbl_false)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLInterpret.ml

    r1357 r1539  
    6868      (string_of_local_env lenv)
    6969      (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%!"
     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%!"
    7373      lbl
    7474  | CallState (_, _, args, mem, _, _) ->
    … …  
    132132    (carry : Val.t)
    133133    (mem   : memory)
    134                 (inds  : indexing list)
     134    (inds  : indexing list)
    135135    (stmt  : RTL.statement)
    136136    (trace : CostLabel.t list) :
    … …  
    145145
    146146      | RTL.St_ind_0 (i, lbl) ->
    147   CostLabel.enter_loop inds i;
    148   State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
     147        CostLabel.enter_loop inds i;
     148        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    149149
    150150      | RTL.St_ind_inc (i, lbl) ->
    151   CostLabel.continue_loop inds i;
    152   State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
     151        CostLabel.continue_loop inds i;
     152        State (sfrs, graph, lbl, sp, lenv, carry, mem, inds, trace)
    153153
    154154      | RTL.St_addr (r1, r2, x, lbl) ->
    … …  
    262262    (args  : Val.t list)
    263263    (mem   : memory)
    264                 (inds  : indexing list)
     264    (inds  : indexing list)
    265265    (trace : CostLabel.t list) :
    266266    state =
    267267  match f_def with
    268268    | RTL.F_int def ->
    269                         let inds = new_ind inds in
     269      let inds = new_ind inds in
    270270      let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
    271271      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
    … …  
    281281    (ret_vals : Val.t list)
    282282    (mem      : memory)
    283                 (inds     : indexing list)
     283    (inds     : indexing list)
    284284    (trace    : CostLabel.t list) :
    285285    state =
    286286  let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
    287287  let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
    288         let inds = forget_ind inds in
     288  let inds = forget_ind inds in
    289289  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, inds, trace)
    290290

  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTL/RTLToERTL.ml

    r1345 r1539  
    5050    ERTL.St_store (addr1, addr2, srcrs, lbl)
    5151  | ERTL.St_call_id (f, nb_args, _) -> ERTL.St_call_id (f, nb_args, lbl)
     52  | ERTL.St_call_ptr (f1, f2, nb_args, _) ->
     53    ERTL.St_call_ptr (f1, f2, nb_args, lbl)
    5254  | ERTL.St_cond _ as inst -> inst
    5355  | ERTL.St_return _ as inst -> inst
    … …  
    295297   below. When the called function returns, we put the result where the calling
    296298   function expect it to be. *)
    297 let translate_call_id f args ret_regs start_lbl dest_lbl def =
     299let translate_call stmt args ret_regs start_lbl dest_lbl def =
    298300  let nb_args = List.length args in
    299301  add_translates
    … …  
    301303      adds_graph [ERTL.St_comment ("Setting up parameters", start_lbl)]] @
    302304     set_params args @
    303      [adds_graph [ERTL.St_call_id (f, nb_args, start_lbl)] ;
     305     [adds_graph [stmt nb_args] ;
    304306      adds_graph [ERTL.St_comment ("Fetching result", start_lbl)] ;
    305307      fetch_result ret_regs ;
    … …  
    366368
    367369  | RTL.St_call_id (f, args, ret_regs, lbl') ->
    368     translate_call_id f args ret_regs lbl lbl' def
    369 
    370   | RTL.St_call_ptr _ ->
    371     assert false (* TODO *)
     370    let stmt nb_args = ERTL.St_call_id (f, nb_args, lbl) in
     371    translate_call stmt args ret_regs lbl lbl' def
     372
     373  | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl') ->
     374    let stmt nb_args = ERTL.St_call_ptr (f1, f2, nb_args, lbl) in
     375    translate_call stmt args ret_regs lbl lbl' def
    372376
    373377  (*
    … …  
    436440      let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in
    437441      (Some cost_label, { def with ERTL.f_graph = graph })
    438                 | ERTL.St_ind_0 (_, lbl) | ERTL.St_ind_inc (_, lbl)
     442    | ERTL.St_ind_0 (_, lbl) | ERTL.St_ind_inc (_, lbl)
    439443    | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl)
    440444    | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)
    … …  
    447451    | ERTL.St_load (_, _, _, lbl)
    448452    | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl)
     453    | ERTL.St_call_ptr (_, _, _, lbl)
    449454    | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl)
    450455      ->

  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabs.mli

    r1477 r1539  
    1212
    1313type argument =
    14         | Reg of Register.t
    15         | Imm of AST.cst*AST.sig_type
     14  | Reg of Register.t
     15  | Imm of AST.cst*AST.sig_type
    1616
    1717(* A function in RTLabs is a mapping from labels to
    … …  
    2727
    2828  (* Reset to 0 a loop index *)
    29         | St_ind_0 of CostLabel.index * Label.t
     29  | St_ind_0 of CostLabel.index * Label.t
    3030
    3131  (* Increment a loop index *)
    32         | St_ind_inc of CostLabel.index * Label.t
     32  | St_ind_inc of CostLabel.index * Label.t
    3333
    3434  (* Assign a constant to registers. Parameters are the destination register,

  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsInterpret.ml

    r1477 r1539  
    5959  List.fold_left f "" args
    6060
    61 let print_state state = (match state with
     61let print_state state = match state with
    6262  | State (_, _, sp, lbl, lenv, mem, inds, _) ->
    6363    Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nIndexing:"
    … …  
    6565      (string_of_local_env lenv)
    6666      (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%!"
     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%!"
    7070      lbl
    7171  | CallState (_, _, args, mem, _, _) ->
    … …  
    7777      (Mem.to_string mem)
    7878      (Val.to_string v)
    79         ); Printf.printf "-----------------------------------------------------\n\n%!"
    8079
    8180
    … …  
    133132
    134133let eval_arg lenv mem sp = function
    135         | RTLabs.Reg r -> get_value lenv r
    136         | RTLabs.Imm (c, t) -> Eval.cst mem sp t c
     134  | RTLabs.Reg r -> get_value lenv r
     135  | RTLabs.Imm (c, t) -> Eval.cst mem sp t c
    137136
    138137let get_type_arg lenv = function
    139         | RTLabs.Reg r -> get_type lenv r
    140         | RTLabs.Imm (_, typ) -> typ
     138  | RTLabs.Reg r -> get_type lenv r
     139  | RTLabs.Imm (_, typ) -> typ
    141140
    142141(* Interpret statements. *)
    … …  
    149148    (mem   : memory)
    150149    (stmt  : RTLabs.statement)
    151                 (inds  : indexing list)
     150    (inds  : indexing list)
    152151    (trace : CostLabel.t list) :
    153152    state = match stmt with
    … …  
    157156
    158157      | RTLabs.St_cost (cost_lbl, lbl) ->
    159   let cost_lbl = CostLabel.ev_indexing (curr_ind inds) cost_lbl in
    160         State (sfrs, graph, sp, lbl, lenv, mem, inds, cost_lbl :: trace)
    161        
    162             | RTLabs.St_ind_0 (i, lbl) ->
     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) ->
    163164        CostLabel.enter_loop inds i;
    164   State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
     165        State (sfrs, graph, sp, lbl, lenv,
     166               mem, inds, trace)
    165167
    166168      | RTLabs.St_ind_inc (i, lbl) ->
    167   CostLabel.continue_loop inds i;
    168   State (sfrs, graph, sp, lbl, lenv, mem, inds, trace)
     169        CostLabel.continue_loop inds i;
     170        State (sfrs, graph, sp, lbl, lenv,
     171               mem, inds, trace)
    169172
    170173      | RTLabs.St_cst (destr, cst, lbl) ->
    … …  
    181184        let v =
    182185          Eval.op2
    183             (get_type lenv destr) (get_type_arg lenv srcr1) (get_type_arg lenv srcr2)
     186            (get_type lenv destr)
     187            (get_type_arg lenv srcr1)
     188            (get_type_arg lenv srcr2)
    184189            op2
    185190            (eval_arg lenv mem sp srcr1)
    … …  
    193198
    194199      | RTLabs.St_store (q, addr, srcr, lbl) ->
    195   let addr = address_of_value (eval_arg lenv mem sp addr) in
     200        let addr = address_of_value (eval_arg lenv mem sp addr) in
    196201        let v = eval_arg lenv mem sp srcr in
    197202        let mem = Mem.storeq mem q addr v in
    … …  
    203208        (* Save the stack frame. *)
    204209        let sf =
    205           {ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv} in
     210          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
     211        in
    206212        CallState (sf :: sfrs, f_def, args, mem, inds, trace)
    207213
    … …  
    302308    (args  : Val.t list)
    303309    (mem   : memory)
    304                 (inds  : indexing list)
     310    (inds  : indexing list)
    305311    (trace : CostLabel.t list) :
    306312    state =
    … …  
    310316        Mem.alloc mem (concrete_stacksize def.RTLabs.f_stacksize) in
    311317      let lenv = init_locals def.RTLabs.f_locals def.RTLabs.f_params args in
    312             (* allocate new constant indexing *)
    313                         let graph = def.RTLabs.f_graph in
    314                         let inds = new_ind inds in
     318      (* allocate new constant indexing *)
     319      let graph = def.RTLabs.f_graph in
     320      let inds = new_ind inds in
    315321      State (sfrs, graph, sp, def.RTLabs.f_entry, lenv, mem', inds, trace)
    316322    | RTLabs.F_ext def ->
    … …  
    324330    (ret_val : Val.t)
    325331    (mem     : memory)
    326                 (inds    : indexing list)
     332    (inds    : indexing list)
    327333    (trace   : CostLabel.t list) :
    328334    state =
    … …  
    330336    | None -> sf.lenv
    331337    | Some ret_reg -> update_local ret_reg ret_val sf.lenv in
    332         (* erase current indexing and revert to previous one *)
    333   let inds = forget_ind inds in
    334   State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, inds, 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)
    335342
    336343

  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsPrinter.ml

    r1477 r1539  
    9696
    9797let 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)
     98  | RTLabs.Reg r -> print_reg r
     99  | RTLabs.Imm (c, t) ->
     100    Printf.sprintf "(%s)%s" (Primitive.print_type t) (print_cst c)
    101101
    102102let print_op2 op r s = Printf.sprintf "%s %s %s"
    … …  
    122122  | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "p"
    123123  | AST.Op_cmpu cmp -> (print_cmp cmp) ^ "u")
    124         (print_arg s)
     124  (print_arg s)
    125125
    126126
    … …  
    169169  | RTLabs.St_load (q, addr, destr, lbl) ->
    170170      Printf.sprintf "%s := *(%s) %s --> %s"
    171   (print_reg destr)
     171        (print_reg destr)
    172172        (Memory.string_of_quantity q)
    173173        (print_arg addr)
    … …  
    175175  | RTLabs.St_store (q, addr, srcr, lbl) ->
    176176      Printf.sprintf "*(%s)%s := %s --> %s"
    177   (Memory.string_of_quantity q)
     177        (Memory.string_of_quantity q)
    178178        (print_arg addr)
    179179        (print_arg srcr)
    … …  
    181181  | RTLabs.St_call_id (f, args, Some r, sg, lbl) ->
    182182      Printf.sprintf "%s := \"%s\"(%s) : %s --> %s"
    183   (print_reg r)
    184   f
     183        (print_reg r)
     184        f
    185185        (print_args args)
    186186        (Primitive.print_sig sg)
    187187        lbl
    188188  | 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
     189      Printf.sprintf "\"%s\"(%s) : %s --> %s"
     190        f
     191        (print_args args)
     192        (Primitive.print_sig sg)
     193        lbl
    194194  | RTLabs.St_call_ptr (f, args, Some r, sg, lbl) ->
    195195      Printf.sprintf "%s := *%s (%s) : %s --> %s"
    196   (print_reg r)
    197     (print_reg f)
    198     (print_args args)
    199     (Primitive.print_sig sg)
    200     lbl
     196        (print_reg r)
     197        (print_reg f)
     198        (print_args args)
     199        (Primitive.print_sig sg)
     200        lbl
    201201  | RTLabs.St_call_ptr (f, args, None, sg, lbl) ->
    202     Printf.sprintf "*%s (%s) : %s --> %s"
    203     (print_reg f)
    204     (print_args args)
    205     (Primitive.print_sig sg)
    206     lbl
     202      Printf.sprintf "*%s (%s) : %s --> %s"
     203        (print_reg f)
     204        (print_args args)
     205        (Primitive.print_sig sg)
     206        lbl
    207207  | RTLabs.St_tailcall_id (f, args, sg) ->
    208208      Printf.sprintf "tailcall \"%s\" (%s) : %s"
    … …  
    256256      (print_statement stmt)
    257257      s in
    258         let f' lbl stmt (reach, s) =
     258  let f' lbl stmt (reach, s) =
    259259    (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'
     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'
    267267       
    268268let print_internal_decl n f def =

  • Deliverables/D2.2/8051-indexed-labels-branch/src/RTLabs/RTLabsToRTL.ml

    r1477 r1539  
    748748    add_graph lbl (RTL.St_return (find_local_env r lenv)) def
    749749               
    750         | _ -> assert false (*not possible because of previous removal of immediates*)
     750  | _ -> assert false (*not possible because of previous removal of immediates*)
    751751
    752752let 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) ->
     753  let load_arg a lbl g rs = match a with
     754    | RTLabs.Reg r -> (lbl, g, rs, r)
     755    | RTLabs.Imm (c, t) ->
    756756      let new_l = Label.Gen.fresh def.RTLabs.f_luniverse in
    757757      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
     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
    764764        let (lbl', g, rs, r2) = load_arg a2 lbl' g rs in
    765765        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)
     766        let g = Label.Map.add lbl' s g in
     767        (g, rs)
    768768      | RTLabs.St_store(q, a1, a2, l) ->
    769769        let (lbl', g, rs, r1) = load_arg a1 lbl g rs in
    … …  
    772772        let g = Label.Map.add lbl' s g in
    773773        (g, rs)
    774                         | RTLabs.St_load (q, a, r, l) ->
     774      | RTLabs.St_load (q, a, r, l) ->
    775775        let (lbl', g, rs, r1) = load_arg a lbl g rs in
    776776        let s = RTLabs.St_load (q, RTLabs.Reg r1, r, l) in
    777777        let g = Label.Map.add lbl' s g in
    778778        (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 }
     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 }
    784784 
    785785let translate_internal def =
    786         let def = remove_immediates def in
     786  let def = remove_immediates def in
    787787  let runiverse = def.RTLabs.f_runiverse in
    788788  let lenv =

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

    r1507 r1539  
    2323*)
    2424let process filename =
    25   let _ = Printf.eprintf "Processing %s.\n%!" filename in
    26   let src_language    = Options.get_source_language () in
    27   let tgt_language    = Options.get_target_language () in
    28   let input_ast       = Languages.parse src_language filename in
    29   let input_ast       = Languages.add_runtime input_ast in
    30   let input_ast       = Languages.labelize input_ast in
     25  let _ = Printf.printf "Processing %s.\n%!" filename in
     26  let src_language = Options.get_source_language () in
     27  let tgt_language = Options.get_target_language () in
     28  let is_lustre_file = Options.is_lustre_file () in
     29  let remove_lustre_externals = Options.is_remove_lustre_externals () in
     30  let input_ast =
     31    Languages.parse ~is_lustre_file ~remove_lustre_externals
     32      src_language filename in
     33  let input_ast = Languages.add_runtime input_ast in
     34  let input_ast = Languages.labelize input_ast in
    3135  let (exact_output, output_filename) = match Options.get_output_files () with
    3236    | None -> (false, filename)
    3337    | Some filename' -> (true, filename') in
    3438  let save ?(suffix="") ast =
    35     Languages.save exact_output output_filename suffix ast
     39    Languages.save
     40      (Options.is_asm_pretty ()) exact_output output_filename suffix ast
    3641  in
    3742  let target_asts =
    … …  
    4550  if Options.annotation_requested () then
    4651    begin
    47       let (annotated_input_ast, cost_id, cost_incr) =
     52      let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
    4853        let cost_tern = Options.is_cost_ternary_enabled () in
    4954        Languages.annotate cost_tern input_ast final_ast in (
    5055          save ~suffix:"-annotated" annotated_input_ast;
    51           Languages.save_cost output_filename cost_id cost_incr);
     56          Languages.save_cost exact_output output_filename cost_id cost_incr
     57            extern_cost_variables);
    5258    end;
    53                                              
    54   if Options.is_debug_enabled () then 
     59
     60  if Options.is_debug_enabled () then
    5561    List.iter save intermediate_asts;
    5662
    57   if Options.interpretation_requested () || Options.is_debug_enabled () ||
    58                Options.trace_requested () then
     63  if Options.interpretations_requested () then
    5964    begin
    6065      let asts = target_asts in
    … …  
    6267      let label_traces = List.map (Languages.interpret debug) asts in
    6368      Printf.eprintf "Checking execution traces...%!";
    64       if Options.trace_requested () then
    65         let print_l l =
    66           Printf.printf "%s, " (CostLabel.string_of_cost_label
    67                                   ~pretty:true l) in
    68         let print_ls ls = List.iter print_l ls in
    69         let print_trace (v, ls) =
    70           Printf.printf "%s | " (Big_int.string_of_big_int v);
    71           print_ls ls;
    72           Printf.printf "\n" in
    73         List.iter print_trace label_traces
    74       else ();
    7569      Checker.same_traces (List.combine asts label_traces);
    7670      Printf.eprintf "OK.\n%!";
    77     end
     71    end;
     72
     73  if Options.interpretation_requested () then
     74    ignore (Languages.interpret (Options.is_debug_enabled ()) final_ast)
     75
     76let lustre_test filename =
     77  let lustre_test       = match Options.get_lustre_test () with
     78    | None -> assert false (* do not use on this argument *)
     79    | Some lustre_test -> lustre_test in
     80  let lustre_test_cases = Options.get_lustre_test_cases () in
     81  let lustre_test_cycles = Options.get_lustre_test_cycles () in
     82  let lustre_test_min_int = Options.get_lustre_test_min_int () in
     83  let lustre_test_max_int = Options.get_lustre_test_max_int () in
     84  let src_language      = Languages.Clight in
     85  let tgt_language      = Languages.Clight in
     86  let input_ast         = Languages.parse src_language filename in
     87  let input_ast         =
     88    Languages.add_lustre_main lustre_test lustre_test_cases lustre_test_cycles
     89      lustre_test_min_int lustre_test_max_int input_ast in
     90  let (exact_output, output_filename) = match Options.get_output_files () with
     91    | None -> (false, filename)
     92    | Some filename' -> (true, filename') in
     93  let save ast =
     94    Languages.save
     95      (Options.is_asm_pretty ()) exact_output output_filename "" ast in
     96  let target_asts =
     97    Languages.compile false (Options.get_transformations ())
     98      src_language tgt_language input_ast
     99  in
     100  let final_ast, _ = Misc.ListExt.cut_last target_asts in
     101  save input_ast ;
     102  save final_ast
    78103
    79104let _ =
    80105  if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files
    81   else List.iter process input_files
     106  else
     107    if Options.get_lustre_test () <> None then List.iter lustre_test input_files
     108    else List.iter process input_files

  • Deliverables/D2.2/8051-indexed-labels-branch/src/checker.ml

    r1291 r1539  
    1414    in
    1515    let sentence (k, (v1, v2)) =
    16                         let k = CostLabel.string_of_cost_label ~pretty:true k in
     16      let k = CostLabel.string_of_cost_label ~pretty:true k in
    1717      Printf.sprintf "  Label %s %s in language `%s' \
    1818                        whereas it %s in language `%s'."
    19              k (string_of_value v1) lang1 (string_of_value v2) lang2
     19        k (string_of_value v1) lang1 (string_of_value v2) lang2
    2020    in
    2121    String.concat "\n" (List.map sentence ds)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clight.mli

    r1305 r1539  
    113113  | Eorbool of expr*expr                        (**r sequential or ([||]) *)
    114114  | Esizeof of ctype                            (**r size of a type *)
    115   | Efield of expr*ident                     (**r access to a member of a struct or union *)
     115  | Efield of expr*ident                        (**r access to a member of a struct or union *)
    116116
    117117  (** The following constructors are used by the annotation process only. *)
    … …  
    138138  | Ssequence of statement*statement            (**r sequence *)
    139139  | Sifthenelse of expr*statement*statement     (**r conditional *)
    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 *)
     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 *)
    143143  | Sbreak                                      (**r [break] statement *)
    144144  | Scontinue                                   (**r [continue] statement *)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.ml

    r1507 r1539  
    2626   Label.Set.union user_labels1 user_labels2)
    2727
    28 let empty_triple =
    29   (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
     28let empty_triple = (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
    3029
    3130let name_singleton id =
    3231  (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty)
    3332
    34 let cost_label_singleton lbl =
    35   (StringTools.Set.empty, CostLabel.Set.singleton lbl, Label.Set.empty)
     33let cost_label_singleton cost_lbl =
     34  (StringTools.Set.empty, CostLabel.Set.singleton cost_lbl, Label.Set.empty)
    3635
    3736let label_singleton lbl =
    … …  
    7978      (StringTools.Set.union vars names, cost_labels, user_labels)
    8079    | Clight.External (id, _, _) ->
    81       (StringTools.Set.singleton id, CostLabel.Set.empty,
    82        Label.Set.empty) in
     80      (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
    8381  let fun_idents (id, f_def) =
    8482    let (names, cost_labels, user_labels) = def_idents f_def in
    … …  
    191189(* Instrument an expression. *)
    192190
    193 (* FIXME: follow cost_tern option *)
     191(* FIXME: currently using a hack (reparsing) *)
    194192let instrument_expr cost_tern l_ind cost_mapping cost_incr =
    195193  let f_expr (Clight.Expr(ed, et) as e) sub_res = match ed, sub_res with
    … …  
    227225(* Instrument a statement. *)
    228226
    229 (* not using ClightFold as l_ind changes through loops *)
     227(* FIXME: use ClightFold, a much better option *)
    230228let rec instrument_body cost_tern l_ind cost_mapping cost_incr stmt =
    231229  let instr_expr = instrument_expr cost_tern l_ind cost_mapping cost_incr in
    … …  
    374372  (cost_incr, Clight.Internal cfun)
    375373
     374(* Create a fresh uninitialized cost variable for each external function. This
     375   will be used by the Cost plug-in of the Frama-C platform. *)
     376
     377let extern_cost_variables make_unique functs =
     378  let prefix = "_cost_of_" in
     379  let f (decls, map) (_, def) = match def with
     380    | Clight.Internal _ -> (decls, map)
     381    | Clight.External (id, _, _) ->
     382      let new_var = make_unique (prefix ^ id) in
     383      (decls @ [cost_decl new_var], StringTools.Map.add id new_var map) in
     384  List.fold_left f ([], StringTools.Map.empty) functs
     385
    376386let save_tmp tmp_file s =
    377387  let cout = open_out tmp_file in
    … …  
    379389  flush cout ;
    380390  close_out cout
    381    
    382    
     391
    383392(** [instrument prog cost_map] instruments the program [prog]. First a fresh
    384393    global variable --- the so-called cost variable --- is added to the program.
    … …  
    391400  (* Create a fresh 'cost' variable. *)
    392401  let names = names p in
    393   let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
     402  let make_unique = StringTools.make_unique names in
     403  let cost_id = make_unique cost_id_prefix in
    394404  let cost_decl = cost_decl cost_id in
    395405
    … …  
    397407  let names = StringTools.Set.add cost_id names in
    398408  let l_ind = StringTools.Gen.fresh_prefix names loop_id_prefix in
     409
     410  (* Create a fresh uninitialized global variable for each extern function. *)
     411  let (extern_cost_decls, extern_cost_variables) =
     412    extern_cost_variables make_unique p.Clight.prog_funct in
    399413
    400414  (* Define an increment function for the cost variable. *)
    … …  
    415429
    416430  (* Glue all this together. *)
    417   let prog_vars = cost_decl :: p.Clight.prog_vars in
     431  let prog_vars = cost_decl :: extern_cost_decls @ p.Clight.prog_vars in
    418432  let prog_funct = cost_incr_def :: prog_funct in
    419433  let p' =
    … …  
    426440  let tmp_file = Filename.temp_file "clight_instrument" ".c" in
    427441  save_tmp tmp_file (ClightPrinter.print_program p') ;
    428   let p' = ClightParser.process tmp_file in
     442  let res = ClightParser.process tmp_file in
    429443  Misc.SysExt.safe_remove tmp_file ;
    430   (p', cost_id, cost_incr)
     444  (res, cost_id, cost_incr, extern_cost_variables)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightAnnotator.mli

    r1507 r1539  
    66    program. Then, each cost label in the program is replaced by an increment of
    77    the cost variable, following the mapping [cost_map]. The function also
    8     returns the name of the cost variable and the name of the cost increment
    9     function. [cost_tern] rules whether cost increments are given by ternary
    10     expressions (more readable) or by branch statements (for frama-c
    11     itegration).
    12 
    13     TODO: int to expressions *)
     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). *)
    1413val instrument : bool -> Clight.program -> int CostLabel.Map.t ->
    15                  Clight.program * string * string
     14                 Clight.program * string * string * string StringTools.Map.t
    1615
    1716val cost_labels : Clight.program -> CostLabel.Set.t

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightFold.ml

    r1392 r1539  
    170170  let sub_stmts_res = List.map (statement2 f_expr f_statement) sub_stmts in
    171171  f_statement stmt sub_exprs_res sub_stmts_res
    172        

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightInterpret.ml

    r1357 r1539  
    106106  | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
    107107  | Ecost (cost_lbl, e) ->
    108                 let cost_lbl = CostLabel.string_of_cost_label cost_lbl in
    109                 "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
     108    let cost_lbl = CostLabel.string_of_cost_label cost_lbl in
     109    "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
    110110  | Ecall (f, arg, e) ->
    111111    "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
    … …  
    151151  LocalEnv.fold f lenv ""
    152152
    153 let print_state state = (match state with
     153let print_state state = match state with
    154154  | State (_, stmt, _, lenv, mem, c) ->
    155155    Printf.printf "Local environment:\n%s\n\nMemory:%s\nLoop indexing: "
    156156      (string_of_local_env lenv)
    157157      (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;
     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)
    … …  
    168168      (Mem.to_string mem)
    169169      (Value.to_string v)
    170         ); Printf.printf "---------------------------------------------------------\n"
    171170
    172171
    … …  
    426425      ((Mem.load m (size_of_ctype tt) addr, tt), l1)
    427426    | Ecost (lbl,e1) ->
    428                         (* applying current indexing on label *)
    429                         let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
     427      (* applying current indexing on label *)
     428      let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
    430429      let (v1,l1) = eval_expr localenv m c e1 in
    431430      (v1,lbl::l1)
    … …  
    486485  else error "undefined condition guard value."
    487486
    488 let eval_stmt f k e m s c =
    489         match s, k with
     487let eval_stmt f k e m s c = match s, k with
    490488  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m,c),[])
    491489  | Sskip, Kwhile(i,a,s,k') | Scontinue, Kwhile(i,a,s,k')
    492490  | Sskip, Kdowhile(i,a,s,k') | Scontinue, Kdowhile (i,a,s,k') ->
    493                 (* possibly continuing a loop *)
    494                 CostLabel.continue_loop_opt c i; (* if loop is not continued, this change
    495                                                 will have no effect in the following. *)
     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. *)
    496494    let ((v1,_),l1) = eval_expr e m c a in
    497495    let a_false = (State(f,Sskip,k',e,m,c),l1) in
    … …  
    504502    let a_true = (State(f,s,Kfor2(i,a2,a3,s,k),e,m,c),l1) in
    505503    condition v1 a_true a_false
    506   | Sskip, Kfor2(i,a2,a3,s,k) -> (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[])
     504  | Sskip, Kfor2(i,a2,a3,s,k) ->
     505    (State(f,a3,Kfor3(i,a2,a3,s,k),e,m,c),[])
    507506  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
    508507  | Sskip, Kcall _ ->
    … …  
    531530    condition v1 a_true a_false
    532531  | Swhile(i,a,s), _ ->
    533                 CostLabel.enter_loop_opt c i;
     532    CostLabel.enter_loop_opt c i;
    534533    let ((v1,_),l1) = eval_expr e m c a in
    535534    let a_false = (State(f,Sskip,k,e,m,c),l1) in
    … …  
    537536    condition v1 a_true a_false
    538537  | Sdowhile(i,a,s), _ ->
    539                 CostLabel.enter_loop_opt c i;
    540                 (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
     538    CostLabel.enter_loop_opt c i;
     539    (State(f,s,Kdowhile(i,a,s,k),e,m,c),[])
    541540  | Sfor(i,Sskip,a2,a3,s), _ ->
    542                 CostLabel.enter_loop_opt c i;
     541    CostLabel.enter_loop_opt c i;
    543542    let ((v1,_),l1) = eval_expr e m c a2 in
    544543    let a_false = (State(f,Sskip,k,e,m,c),l1) in
    … …  
    548547  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m,c),[])
    549548  | Sbreak, Kwhile(_,_,_,k) | Sbreak, Kdowhile(_,_,_,k)
    550         | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
     549  | Sbreak, Kfor2(_,_,_,_,k) | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m,c),[])
    551550  | Scontinue, Kseq(_,k)
    552         | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[])
     551  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m,c),[])
    553552  | Sreturn None, _ ->
    554553    let m' = free_local_env m e in
    … …  
    561560    let ((v,_),l) = eval_expr e m c a in
    562561    let n = Value.to_int v in
    563     (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l)
     562  (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m,c),l)
    564563  | Slabel(lbl,s), _ -> (State(f,s,k,e,m,c),[])
    565564  | Scost(lbl,s), _ ->
    566                 (* applying current indexing on label *)
    567                 let lbl = CostLabel.ev_indexing (CostLabel.curr_const_ind c) lbl in
    568                 (State(f,s,k,e,m,c),[lbl])
     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])
    569568  | Sgoto lbl, _ ->
    570                 (* if we exit an indexed loop, we don't care. It should not be possible to*)
    571                 (* enter an indexed loop that is not the current one, so we do nothing*)
    572                 (* to loop indexes *)
     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 *)
    573572    let (s', k') = find_label lbl f.fn_body (call_cont k) in
    574573    (State(f,s',k',e,m,c),[])
    … …  
    589588  | Internal f ->
    590589    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
    591                 (* initializing loop indices *)
    592                 let c = CostLabel.new_const_ind c in
     590    (* initializing loop indices *)
     591    let c = CostLabel.new_const_ind c in
    593592    State (f, f.fn_body, cont, e, mem', c)
    594593  | External(id,targs,tres) when List.length targs = List.length args ->
    … …  
    601600  | Callstate(fun_def,vargs,k,m,c) -> (step_call vargs k m c fun_def,[])
    602601  | 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),[])
     602    let c = CostLabel.forget_const_ind c in
     603    (State(f,Sskip,k,e,m,c),[])
    605604  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m,c) ->
    606605    let c = CostLabel.forget_const_ind c in

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightLabelling.ml

    r1421 r1539  
    1616
    1717let add_ending_cost_label indexing cost_universe stmt =
    18         let lbld_skip = add_starting_cost_label indexing cost_universe Clight.Sskip in
     18  let lbld_skip = add_starting_cost_label indexing cost_universe Clight.Sskip in
    1919  Clight.Ssequence (stmt, lbld_skip)
    2020
    … …  
    7575
    7676let add_cost_labels_opt ind cost_universe =
    77         Option.map (add_cost_labels_e ind cost_universe)
     77  Option.map (add_cost_labels_e ind cost_universe)
    7878
    7979let add_cost_labels_lst ind cost_universe l =
    … …  
    8282
    8383(* Add cost labels to a statement. *)
     84
     85let update_ind i ind =
     86  match i with
     87    | None -> ind
     88    | Some _ -> CostLabel.add_id_indexing ind
    8489
    8590let rec add_cost_labels_st ind cost_universe = function
    8691  | Sskip -> Sskip
    8792  | Sassign (e1,e2) ->
    88       Sassign (add_cost_labels_e ind cost_universe e1,
    89                add_cost_labels_e ind cost_universe e2)
     93    Sassign (add_cost_labels_e ind cost_universe e1,
     94             add_cost_labels_e ind cost_universe e2)
    9095  | Scall (e1,e2,lst) ->
    91       Scall (add_cost_labels_opt ind cost_universe e1,
    92              add_cost_labels_e ind cost_universe e2,
    93              add_cost_labels_lst ind 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)
    9499  | Ssequence (s1,s2) ->
    95       Ssequence (add_cost_labels_st ind cost_universe s1,
    96                  add_cost_labels_st ind cost_universe s2)
     100    Ssequence (add_cost_labels_st ind cost_universe s1,
     101               add_cost_labels_st ind cost_universe s2)
    97102  | Sifthenelse (e,s1,s2) ->
    98       let s1' = add_cost_labels_st ind cost_universe s1 in
    99       let s1' = add_starting_cost_label ind cost_universe s1' in
    100       let s2' = add_cost_labels_st ind cost_universe s2 in
    101       let s2' = add_starting_cost_label ind cost_universe s2' in
    102       Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2')
     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')
    103108  | Swhile (i,e,s) ->
    104                   let ind' = match i with
    105                                 | None -> ind
    106                                 | Some _ -> CostLabel.add_id_indexing ind in
    107       let s' = add_cost_labels_st ind' cost_universe s in
    108       let s' = add_starting_cost_label ind' cost_universe s' in
    109                         (* exit label indexed with outside indexing *)
    110       add_ending_cost_label ind cost_universe
    111         (Swhile (i,add_cost_labels_e ind cost_universe 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'))
    112115  | Sdowhile (i,e,s) ->
    113       let ind' = match i with
    114         | None -> ind
    115         | Some _ -> CostLabel.add_id_indexing ind in
    116       let s' = add_cost_labels_st ind' cost_universe s in
    117       let s' = add_starting_cost_label ind' cost_universe s' in
    118       add_ending_cost_label ind cost_universe
    119         (Sdowhile (i,add_cost_labels_e ind cost_universe 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'))
    120121  | Sfor (i,s1,e,s2,s3) ->
    121       let s1' = add_cost_labels_st ind cost_universe s1 in
    122       let ind' = match i with
    123         | None -> ind
    124         | Some _ -> CostLabel.add_id_indexing ind in
    125       let s2' = add_cost_labels_st ind' cost_universe s2 in
    126       let s3' = add_cost_labels_st ind' cost_universe s3 in
    127       let s3' = add_starting_cost_label ind' cost_universe s3' in
    128       add_ending_cost_label ind cost_universe
    129         (Sfor (i, s1', add_cost_labels_e ind cost_universe 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'))
    130129  | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e)
    131130  | Sswitch (e,ls) ->
    132       Sswitch (add_cost_labels_e ind cost_universe e,
    133                add_cost_labels_ls ind cost_universe ls)
     131    Sswitch (add_cost_labels_e ind cost_universe e,
     132             add_cost_labels_ls ind cost_universe ls)
    134133  | Slabel (lbl,s) ->
    135       let s' = add_cost_labels_st ind cost_universe s in
    136       let s' = add_starting_cost_label ind cost_universe s' in
    137       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')
    138137  | Scost (_,_) -> assert false
    139138  | _ as stmt -> stmt
    … …  
    152151(* traversal of code assigning to every label the "loop address" of it. *)
    153152(* A loop address like [2, 0, 1] means the corresponding label is in the *)
    154 (* third loop inside the first loop inside the second loop of the body. The *)
     153(* third loop inside the first loop inside the second loop of the body. *)
    155154let rec assign_loop_addrs_s
    156155    (current : int list)
    157                 (offset  : int)
    158                 (m       : int list Label.Map.t)
    159                 : Clight.statement -> int*int list Label.Map.t = 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)
     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)
    172172
    173173and assign_loop_addrs_ls current offset m = function
    174174  | LSdefault s -> assign_loop_addrs_s current offset m s
    175175  | 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
     176    let (offset, m) = assign_loop_addrs_s current offset m s in
     177    assign_loop_addrs_ls current offset m ls
    178178
    179179let 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
     180  | [], _ -> true
     181  | hd1 :: tl1, hd2 :: tl2 when hd1 = hd2 -> is_prefix tl1 tl2
     182  | _ -> false
    183183
    184184(* traversal of code which for every statement [s] returns the set of loop*)
    … …  
    186186let rec find_multi_entry_loops_s
    187187    (m       : int list Label.Map.t)
    188                 (current : int list)
    189                 (offset  : int)
    190                 : Clight.statement -> int*IntListSet.t = function
    191         (* I am supposing you cannot jump to the update statement of for loops... *)
    192         | Swhile(_,_,s) | Sdowhile(_,_,s) | Sfor(_,_,_,_,s) ->
    193                         let current' = offset :: current in
    194                         let (_, set) = find_multi_entry_loops_s m current' 0 s in
    195                         (offset + 1, set)
    196         | Ssequence(s1,s2) | Sifthenelse(_,s1,s2) ->
    197           let (offset, set1) = find_multi_entry_loops_s m current offset s1 in
    198           let (offset, set2) = find_multi_entry_loops_s m current offset s2 in
    199           (offset, IntListSet.union set1 set2)
    200         | Slabel(_,s) -> find_multi_entry_loops_s m current offset s
    201                 | Sgoto l ->
    202                         (* all labels should have a binding in m *)
    203                         let addr = Label.Map.find l m in
    204                         let cond = is_prefix addr current in
    205                         let set = if cond then IntListSet.empty else IntListSet.singleton addr in
    206                         (offset, set)   
    207         | Sswitch(_,ls) -> find_multi_entry_loops_ls m current offset ls
    208         | _ -> (offset, IntListSet.empty)
     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)
    209210
    210211and find_multi_entry_loops_ls m current offset = function
    … …  
    214215    let (offset, set2) = find_multi_entry_loops_ls m current offset ls in
    215216    (offset, IntListSet.union set1 set2)
    216                                
     217     
    217218(* final pass where loops are indexed *)
    218219let rec index_loops_s multi_entry current offset depth = function
    219         (* I am supposing you cannot jump to the update statement of for loops... *)
    220         | Swhile(_,b,s) ->
    221     let current' = offset :: current in
    222                 let is_bad = IntListSet.mem current' multi_entry in
    223                 let i, depth = if is_bad then None, depth else Some depth, depth + 1 in
    224           let (_, s) = index_loops_s multi_entry current' 0 depth s in
    225           (offset + 1, Swhile(i,b,s))
    226         | Sdowhile(_,b,s) ->
     220  (* I am supposing you cannot jump to the update statement of for loops... *)
     221  | Swhile(_,b,s) ->
    227222    let current' = offset :: current in
    228223    let is_bad = IntListSet.mem current' multi_entry in
    229224    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in
    230           let (_, s) = index_loops_s multi_entry current' 0 depth s in
    231           (offset + 1, Sdowhile(i,b,s))
    232         | Sfor(_,a1,a2,a3,s) ->
     225    let (_, s) = index_loops_s multi_entry current' 0 depth s in
     226    (offset + 1, Swhile(i,b,s))
     227  | Sdowhile(_,b,s) ->
    233228    let current' = offset :: current in
    234229    let is_bad = IntListSet.mem current' multi_entry in
    235230    let i, depth = if is_bad then None, depth else Some depth, depth + 1 in
    236           let (_, s) = index_loops_s multi_entry current' 0 depth s in
    237           (offset + 1, Sfor(i,a1,a2,a3,s))
    238         | Ssequence(s1,s2) ->
    239           let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
    240           let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
    241           (offset, Ssequence(s1,s2))
    242         | Sifthenelse(b,s1,s2) ->
    243           let (offset, s1) = index_loops_s multi_entry current offset depth s1 in
    244           let (offset, s2) = index_loops_s multi_entry current offset depth s2 in
    245           (offset, Sifthenelse(b,s1,s2))
    246         | Slabel(l,s) ->
    247                 let (offset, s) = index_loops_s multi_entry current offset depth s in
    248                 (offset, Slabel(l, s))
    249         | Sswitch(v,ls) ->
     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) ->
    250251    let (offset, s) = index_loops_ls multi_entry current offset depth ls in
    251                 (offset, Sswitch(v, ls))
    252         | _ as s -> (offset, s)
     252    (offset, Sswitch(v, ls))
     253  | _ as s -> (offset, s)
    253254
    254255and index_loops_ls multi_entry current offset depth = function
    255256  | LSdefault s ->
    256                 let (offset, s) =       index_loops_s multi_entry current offset depth s in
    257                 (offset, LSdefault s)
     257    let (offset, s) =
     258      index_loops_s multi_entry current offset depth s in
     259    (offset, LSdefault s)
    258260  | LScase(v,s,ls) ->
    259261    let (offset, s) = index_loops_s multi_entry current offset depth s in
    260262    let (offset, ls) = index_loops_ls multi_entry current offset depth ls in
    261                 (offset, LScase(v,s,ls))
     263    (offset, LScase(v,s,ls))
    262264
    263265(* Index loops and introduce cost labels in functions *)
    … …  
    271273    (* index loops accordingly *)
    272274    let (_, body) = index_loops_s multi_entry [] 0 0 body in
    273                 (* initialize indexing *)
    274                 let ind = CostLabel.empty_indexing in
    275                 (* add cost labels inside *)
    276                 let body = add_cost_labels_st ind cost_universe body in
    277                 (* add cost label in front *)
    278                 let body = add_starting_cost_label ind cost_universe body in
    279                 (id,Internal {fd with fn_body = body})
     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})
    280282  | _ as x -> x
    281283       
    … …  
    287289let add_cost_labels p =
    288290  let labs = ClightAnnotator.all_labels p in
    289         let add = CostLabel.Atom.Set.add in
    290         let empty = CostLabel.Atom.Set.empty in
     291  let add = CostLabel.Atom.Set.add in
     292  let empty = CostLabel.Atom.Set.empty in
    291293  let labs = StringTools.Set.fold add labs empty in
    292294  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
    293295  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
    294296  {p with prog_funct = List.map (process_f cost_universe) p.prog_funct}
    295 

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightParser.ml

    r818 r1539  
    1 let process file =
    2   let tmp_file1 = Filename.temp_file "cparser1" ".c"
    3   and tmp_file2 = Filename.temp_file "cparser2" ".i"
     1
     2let process ?is_lustre_file ?remove_lustre_externals file =
     3  let temp_dir = Filename.dirname file in
     4  let tmp_file1 = Filename.temp_file ~temp_dir "cparser1" ".c"
     5  and tmp_file2 = Filename.temp_file ~temp_dir "cparser2" ".i"
    46  and prepro_opts = [] in
    57
    … …  
    810    try
    911      let oc = open_out tmp_file1 in
     12      if is_lustre_file = Some true || remove_lustre_externals = Some true then
     13        output_string oc "#include<string.h>";
    1014      output_string oc Primitive.prototypes ;
    1115      close_out oc
    … …  
    1519       (Filename.quote file) (Filename.quote tmp_file1)) in
    1620  if rc <> 0 then (
     21    (*
    1722    Misc.SysExt.safe_remove tmp_file1;
     23    *)
    1824    failwith "Error adding primitive prototypes."
    1925  );
    … …  
    2632       (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in
    2733  if rc <> 0 then (
     34    (*
    2835    Misc.SysExt.safe_remove tmp_file1;
    2936    Misc.SysExt.safe_remove tmp_file2;
     37    *)
    3038    failwith "Error calling gcc."
    3139  );
    … …  
    3341  (* C to Cil *)
    3442  let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in
    35   Misc.SysExt.safe_remove tmp_file1;
    36   Misc.SysExt.safe_remove tmp_file2;
    3743  match r with
    3844    | None -> failwith "Error during C parsing."
    … …  
    4147      (match ClightFromC.convertProgram p with
    4248        | None -> failwith "Error during C to Clight pass."
    43         | Some(pp) -> pp
    44       )
     49        | Some(pp) ->
     50          Misc.SysExt.safe_remove tmp_file1;
     51          Misc.SysExt.safe_remove tmp_file2;
     52          if remove_lustre_externals = Some true then ClightLustre.simplify pp
     53          else pp)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightParser.mli

    r486 r1539  
    22    [CIL]. *)
    33
    4 (** [process filename] parses the contents of [filename] to obtain
    5     an abstract syntax tree that represents a Clight program. *)
    6 val process : string -> Clight.program
     4(** [process ?is_lustre_file ?remove_lustre_externals filename] parses the
     5    contents of [filename] to obtain an abstract syntax tree that represents a
     6    Clight program. *)
     7val process :
     8  ?is_lustre_file:bool -> ?remove_lustre_externals:bool ->
     9  string -> Clight.program

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightPrinter.ml

    r1392 r1539  
    197197      fprintf p "%a.%s" print_expr_prec (level, e1) id
    198198  | 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
     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
    202202  | Ecall(f, arg, e) ->
    203203      fprintf p "(%s(%a), %a)" f print_expr arg print_expr e
    … …  
    218218
    219219let print_loop_depth p = function
    220         | None -> fprintf p ""
    221         | Some x -> fprintf p "/* single entry loop depth: %d */@," x
     220  | None -> fprintf p ""
     221  | Some x -> fprintf p "/* single entry loop depth: %d */@," x
    222222
    223223let rec print_stmt p s =
    … …  
    248248              print_stmt s2
    249249  | 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
     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
    254254  | 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
     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
    259259  | 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
     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
    266266  | Sbreak ->
    267       fprintf p "break;"
     267    fprintf p "break;"
    268268  | Scontinue ->
    269       fprintf p "continue;"
     269    fprintf p "continue;"
    270270  | Sswitch(e, cases) ->
    271       fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
    272               print_expr e
    273               print_cases cases
     271    fprintf p "@[<v 2>switch (%a) {@ %a@;<0 -2>}@]"
     272      print_expr e
     273      print_cases cases
    274274  | Sreturn None ->
    275       fprintf p "return;"
     275    fprintf p "return;"
    276276  | Sreturn (Some e) ->
    277       fprintf p "return %a;" print_expr e
     277    fprintf p "return %a;" print_expr e
    278278  | Slabel(lbl, s1) ->
    279       fprintf p "%s:@ %a" lbl print_stmt s1
     279    fprintf p "%s:@ %a" lbl print_stmt s1
    280280  | Sgoto lbl ->
    281       fprintf p "goto %s;" lbl
    282  | Scost (lbl,s1) ->
    283            let lbl = CostLabel.string_of_cost_label lbl in
     281    fprintf p "goto %s;" lbl
     282  | Scost (lbl,s1) ->
     283    let lbl = CostLabel.string_of_cost_label lbl in
    284284     fprintf p "%s:@ %a" lbl print_stmt s1
    285285
    … …  
    481481  | Sdowhile(_, e, s) -> collect_stmt s; collect_expr e
    482482  | 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
     483    collect_stmt s_init; collect_expr e;
     484    collect_stmt s_iter; collect_stmt s_body
    485485  | Sbreak -> ()
    486486  | Scontinue -> ()

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightSwitch.ml

    r818 r1539  
    66let type_of (Clight.Expr (_, t)) = t
    77
    8 let rec simplify_switch e cases stmts = match cases, stmts with
    9   | Clight.LSdefault _, stmt :: _ -> stmt
    10   | Clight.LScase (i, _, lbl_stmts), stmt :: stmts ->
    11     let next_cases = simplify_switch e lbl_stmts stmts in
    12     let ret_type = Clight.Tint (Clight.I32, AST.Signed) in
    13     let cst_i = Clight.Expr (Clight.Econst_int i, type_of e) in
    14     let test = Clight.Expr (Clight.Ebinop (Clight.Oeq, e, cst_i), ret_type) in
    15     Clight.Sifthenelse (test, stmt, next_cases)
    16   | _ -> assert false (* do not use on these arguments *)
    178
    189let f_expr e _ = e
    1910
    20 let f_stmt stmt sub_exprs_res sub_stmts_res = match stmt, sub_stmts_res with
    21   | Clight.Sswitch (e, cases), sub_stmts -> simplify_switch e cases sub_stmts
    22   | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
     11let f_stmt lbl stmt sub_exprs_res sub_stmts_res =
     12  match stmt, sub_stmts_res with
     13    | Clight.Sbreak, _ -> Clight.Sgoto lbl
     14    | Clight.Swhile _, _ | Clight.Sdowhile _, _
     15    | Clight.Sfor _, _ | Clight.Sswitch _, _ -> stmt
     16    | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
    2317
    24 let simplify_statement = ClightFold.statement2 f_expr f_stmt
     18let replace_undeep_break lbl = ClightFold.statement2 f_expr (f_stmt lbl)
    2519
    26 let simplify_fundef = function
     20
     21let add_starting_lbl fresh stmt =
     22  let lbl = fresh () in
     23  (lbl, Clight.Slabel (lbl, stmt))
     24
     25let add_starting_lbl_list fresh stmts = List.map (add_starting_lbl fresh) stmts
     26
     27let add_ending_goto lbl stmt =
     28  Clight.Ssequence (stmt, Clight.Slabel (lbl, Clight.Sskip))
     29
     30let make_sequence stmts =
     31  let f sequence stmt = Clight.Ssequence (sequence, stmt) in
     32  List.fold_left f Clight.Sskip stmts
     33
     34let simplify_switch fresh e cases stmts =
     35  let exit_lbl = fresh () in
     36  let (lbls, stmts) = List.split (add_starting_lbl_list fresh stmts) in
     37  let stmts = List.map (replace_undeep_break exit_lbl) stmts in
     38  let rec aux cases lbls = match cases, lbls with
     39    | Clight.LSdefault _, lbl :: _ -> [Clight.Sgoto lbl]
     40    | Clight.LScase (i, _, cases), lbl :: lbls ->
     41      let next_cases = aux cases lbls in
     42      let ret_type = Clight.Tint (Clight.I32, AST.Signed) in
     43      let cst_i = Clight.Expr (Clight.Econst_int i, type_of e) in
     44      let test = Clight.Expr (Clight.Ebinop (Clight.Oeq, e, cst_i), ret_type) in
     45      Clight.Sifthenelse (test, Clight.Sgoto lbl, Clight.Sskip) :: next_cases
     46    | _ ->
     47      (* Do not use on these arguments: wrong list size. *)
     48      assert false in
     49  add_ending_goto exit_lbl (make_sequence ((aux cases lbls) @ stmts))
     50
     51let f_expr e _ = e
     52
     53let f_stmt fresh stmt sub_exprs_res sub_stmts_res =
     54  match stmt, sub_stmts_res with
     55    | Clight.Sswitch (e, cases), sub_stmts ->
     56      simplify_switch fresh e cases sub_stmts
     57    | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
     58
     59let simplify_statement fresh = ClightFold.statement2 f_expr (f_stmt fresh)
     60
     61let simplify_fundef fresh = function
    2762  | Clight.Internal cfun ->
    28     let cfun =
    29       { cfun with Clight.fn_body = simplify_statement cfun.Clight.fn_body } in
    30     Clight.Internal cfun
     63    let fn_body = simplify_statement fresh cfun.Clight.fn_body in
     64    Clight.Internal { cfun with Clight.fn_body = fn_body }
    3165  | fundef -> fundef
    3266
    3367let simplify p =
    34   let f (id, fundef) = (id, simplify_fundef fundef) in
     68  let labels = ClightAnnotator.all_labels p in
     69  let fresh = StringTools.make_fresh labels "_tmp_switch" in
     70  let f (id, fundef) = (id, simplify_fundef fresh fundef) in
    3571  { p with Clight.prog_funct = List.map f p.Clight.prog_funct }

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/clightToCminor.ml

    r1473 r1539  
    217217let sort_params = sort_vars Param (Some (fun offset -> ParamStack offset))
    218218
    219 let sort_globals stack_vars globals var_locs =
     219let sort_globals stack_vars globals functs var_locs =
    220220  let globals = List.map (fun ((id, _), ctype) -> (id, ctype)) globals in
     221  let f_functs (id, fundef) =
     222    let (params, return) =  match fundef with
     223      | Clight.Internal cfun ->
     224        (List.map snd cfun.Clight.fn_params, cfun.Clight.fn_return)
     225      | Clight.External (_, params, return) -> (params, return) in
     226    (id, Clight.Tfunction (params, return)) in
     227  let functs = List.map f_functs functs in
     228  let globals = globals @ functs in
    221229  sort_vars Global None stack_vars globals var_locs
    222230
    … …  
    225233   globals. *)
    226234
    227 let sort_variables globals cfun =
     235let sort_variables globals functs cfun =
    228236  let stack_vars = stack_vars cfun in
    229237  let var_locs = empty_var_locs in
    230   let var_locs = sort_globals stack_vars globals var_locs in
     238  let var_locs = sort_globals stack_vars globals functs var_locs in
    231239  let var_locs = sort_params stack_vars cfun.Clight.fn_params var_locs in
    232240  let var_locs = sort_locals stack_vars cfun.Clight.fn_vars var_locs in
    … …  
    439447
    440448and translate_addrof_ident res_type var_locs id =
     449  assert (mem_var_locs id var_locs) ;
    441450  match find_var_locs id var_locs with
    442     | (Local, _) | (Param, _) -> assert false (* type error *)
     451    | (Local, _) | (Param, _) -> assert false (* location error *)
    443452    | (LocalStack off, _) | (ParamStack off, _) ->
    444453      Cminor.Expr (add_stack off, res_type)
    … …  
    487496
    488497let ind_0 i stmt = match i with
    489         | None -> stmt
    490         | Some x -> Cminor.St_ind_0(x, stmt)
     498  | None -> stmt
     499  | Some x -> Cminor.St_ind_0(x, stmt)
    491500
    492501let ind_inc i stmt = match i with
    493         | None -> stmt
    494         | Some x -> Cminor.St_ind_inc(x, stmt)
     502  | None -> stmt
     503  | Some x -> Cminor.St_ind_inc(x, stmt)
    495504
    496505let trans_for =
    497         let f_expr e _ = e in
    498         let f_stmt stmt expr_res stmt_res = match expr_res, stmt_res, stmt with
    499                 | e::_, s1::s2::s3::_, Clight.Sfor(i,_,_,_,_) ->
    500                         Clight.Ssequence(s1,Clight.Swhile(i,e,
    501                          Clight.Ssequence(s3, s2)))
    502                 | exprs, sub_sts, stm -> ClightFold.statement_fill_subs stm exprs sub_sts in
    503         ClightFold.statement2 f_expr f_stmt
     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)
    504526
    505527let rec translate_stmt fresh var_locs cnt_lbl br_lbl = function
    … …  
    508530
    509531    | Clight.Sassign (e1, e2) ->
    510                         let e2 = translate_expr var_locs e2 in
     532      let e2 = translate_expr var_locs e2 in
    511533      ([], assign var_locs e1 e2)
    512534
    513535    | Clight.Scall (None, f, args) ->
    514                         let f = translate_expr var_locs f in
    515                         let args = List.map (translate_expr var_locs) args in
     536      let f = translate_expr var_locs f in
     537      let args = List.map (translate_expr var_locs) args in
    516538      ([], Cminor.St_call (None, f, args, call_sig AST.Type_void args))
    517539
    518540    | Clight.Scall (Some e, f, args) ->
    519             let f = translate_expr var_locs f in
    520             let args = List.map (translate_expr var_locs) args in
     541      let f = translate_expr var_locs f in
     542      let args = List.map (translate_expr var_locs) args in
    521543      let t = sig_type_of_ctype (clight_type_of e) in
    522544      let tmp = fresh () in
    … …  
    528550
    529551    | Clight.Swhile (i,e,stmt) ->
    530                         let loop_lbl = fresh () in
    531                         let llbl_opt = Some loop_lbl in
    532                         let exit_lbl = fresh () in
    533             let elbl_opt = Some exit_lbl in
    534             let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in
    535                         let e = translate_expr var_locs e in
    536                         let jmp lbl = Cminor.St_goto lbl in
     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 *)
    537560      let scond =
    538561        Cminor.St_ifthenelse (e, Cminor.St_skip, jmp exit_lbl) in
    539             let loop =
    540                                 Cminor.St_seq(scond,Cminor.St_seq (stmt, ind_inc i (jmp loop_lbl))) in
    541                         let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) 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
    542565      (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip)))
    543                        
     566       
    544567    | Clight.Sdowhile (i,e,stmt) ->
    545             let loop_lbl = fresh () in
    546             let llbl_opt = Some loop_lbl in
    547             let exit_lbl = fresh () in
    548             let elbl_opt = Some exit_lbl in
     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
    549572      let (tmps, stmt) = translate_stmt fresh var_locs llbl_opt elbl_opt stmt in
    550573      let e = translate_expr var_locs e in
    … …  
    552575      let scond =
    553576        Cminor.St_ifthenelse (e, ind_inc i (jmp loop_lbl), Cminor.St_skip) in
    554             let loop =
     577      let loop =
    555578        Cminor.St_seq (stmt, scond) in
    556579      let loop = ind_0 i (Cminor.St_label(loop_lbl,loop)) in
    557580      (tmps, Cminor.St_seq (loop, Cminor.St_label(exit_lbl,Cminor.St_skip)))
    558                        
     581       
    559582    | Clight.Sfor _ -> assert false (* transformed *)
    560583
    … …  
    571594
    572595    | Clight.Sbreak ->
    573                         let br_lbl = match br_lbl with
    574                                 | Some x -> x
    575                                 | None -> invalid_arg("break without enclosing scope") in
    576                         ([], Cminor.St_goto br_lbl)
     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)
    577600
    578601    | Clight.Scontinue ->
    579             let cnt_lbl = match cnt_lbl with
    580                 | Some x -> x
    581                 | None -> invalid_arg("continue without enclosing scope") in
     602      let cnt_lbl = match cnt_lbl with
     603        | Some x -> x
     604        | None -> invalid_arg("continue without enclosing scope") in
    582605      ([], Cminor.St_goto cnt_lbl)
    583606    | Clight.Sswitch _ ->
    … …  
    589612
    590613    | Clight.Sreturn (Some e) ->
    591                         let e = translate_expr var_locs e in
    592                         ([], Cminor.St_return (Some e))
     614      let e = translate_expr var_locs e in
     615      ([], Cminor.St_return (Some e))
    593616
    594617    | Clight.Slabel (lbl, stmt) ->
    595                         let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
    596                         (tmps, Cminor.St_label (lbl, stmt))
     618      let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
     619      (tmps, Cminor.St_label (lbl, stmt))
    597620
    598621    | Clight.Sgoto lbl -> ([], Cminor.St_goto lbl)
    599622
    600623    | Clight.Scost (lbl, stmt) ->
    601                         let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
    602                         (tmps, Cminor.St_cost (lbl, stmt))
     624      let (tmps, stmt) = translate_stmt fresh var_locs cnt_lbl br_lbl stmt in
     625      (tmps, Cminor.St_cost (lbl, stmt))
    603626
    604627(*    | _ -> assert false (* type error *) *)
    … …  
    619642  fold_var_locs f var_locs body
    620643
    621 let translate_internal fresh globals cfun =
    622   let var_locs = sort_variables globals cfun in
     644let translate_internal fresh globals functs cfun =
     645  let var_locs = sort_variables globals functs cfun in
    623646  let params =
    624647    List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in
    625         let body = cfun.Clight.fn_body in
    626         let body = trans_for body in
     648  let body = cfun.Clight.fn_body in
     649  let body = trans_for body in
    627650  let (tmps, body) = translate_stmt fresh var_locs None None body in
    628651  let body = add_stack_parameters_initialization var_locs body in
    … …  
    638661                   AST.res = type_return_of_ctype return } }
    639662
    640 let translate_funct fresh globals (id, def) =
     663let translate_funct fresh globals functs (id, def) =
    641664  let def = match def with
    642     | Clight.Internal ff -> Cminor.F_int (translate_internal fresh globals ff)
     665    | Clight.Internal ff ->
     666      Cminor.F_int (translate_internal fresh globals functs ff)
    643667    | Clight.External (i,p,r) -> Cminor.F_ext (translate_external i p r) in
    644668  (id, def)
    … …  
    646670let translate p =
    647671  let fresh = ClightAnnotator.make_fresh "_tmp" p in
     672  let translate_funct =
     673    translate_funct fresh p.Clight.prog_vars p.Clight.prog_funct in
    648674  { Cminor.vars = List.map translate_global p.Clight.prog_vars ;
    649     Cminor.functs =
    650       List.map (translate_funct fresh p.Clight.prog_vars) p.Clight.prog_funct ;
     675    Cminor.functs = List.map translate_funct p.Clight.prog_funct ;
    651676    Cminor.main = p.Clight.prog_main }

  • Deliverables/D2.2/8051-indexed-labels-branch/src/clight/runtime.ml

    r818 r1539  
    3636       function *)
    3737    (string -> string) *
    38     (* dependences *)
     38    (* dependencies *)
    3939    operation list
    4040

  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminor.mli

    r1392 r1539  
    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. *)
     41     table of cases and their corresponding labels to go to,
     42     and the label to go to in the default case. *)
    4343  | St_switch of expression * (int*Label.t) list * Label.t
    4444
    … …  
    4747  | St_goto of Label.t
    4848  | St_cost of CostLabel.t * statement
    49         | St_ind_0 of CostLabel.index * statement
     49  | St_ind_0 of CostLabel.index * statement
    5050  | St_ind_inc of CostLabel.index * statement
    5151

  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorAnnotator.ml

    r1291 r1539  
    204204let all_labels p =
    205205  let (cost_labels, user_labels) = prog_labels p in
    206         let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     206  let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
    207207  let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
    208208  Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all

  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorFold.ml

    r1392 r1539  
    4545  (*| Cminor.St_loop stmt | Cminor.St_block stmt *)
    4646  | Cminor.St_label (_, stmt) | Cminor.St_cost (_, stmt)
    47         | Cminor.St_ind_0 (_, stmt) | Cminor.St_ind_inc (_, stmt) ->
    48                 ([], [stmt])
     47  | Cminor.St_ind_0 (_, stmt) | Cminor.St_ind_inc (_, stmt) ->
     48    ([], [stmt])
    4949
    5050let statement_fill_subs stmt sub_es sub_stmts =

  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorInterpret.ml

    r1392 r1539  
    7070  | St_goto lbl -> "goto " ^ lbl
    7171  | 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
     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
    7676
    7777let print_state = function
    … …  
    8181      (Mem.to_string mem)
    8282      (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%!"
     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%!"
    8686      (string_of_statement stmt)
    8787  | State_call (_, args, _, mem,_) ->
    … …  
    233233let rec callcont = function
    234234  | Ct_cont(_,k) (*| Ct_endblock k *) -> callcont k
    235         | (Ct_stop | Ct_returnto _) as k -> k
     235  | (Ct_stop | Ct_returnto _) as k -> k
    236236
    237237let findlabel lbl st k =
    … …  
    244244  | St_seq(s1,s2)               ->
    245245      (match fdlbl (Ct_cont(s2,k)) s1 with
    246        None -> fdlbl k s2
    247     | Some(v) -> Some(v)
     246           None -> fdlbl k s2
     247        | Some(v) -> Some(v)
    248248      )
    249249  | St_ifthenelse(_,s1,s2)      ->
    250250      (match fdlbl k s1 with
    251        None -> fdlbl k s2
    252     | Some(v) -> Some(v)
     251           None -> fdlbl k s2
     252        | Some(v) -> Some(v)
    253253      )
    254254(*  | St_loop(s)                  -> fdlbl (Ct_cont(St_loop(s),k)) s
    … …  
    260260  | St_goto(_)                  -> None
    261261  | St_cost(_,s)  | St_label(_,s)
    262         | St_ind_0(_,s) | St_ind_inc(_,s) -> fdlbl k s
     262  | St_ind_0(_,s) | St_ind_inc(_,s) -> fdlbl k s
    263263  in match fdlbl k st with
    264264      None -> assert false (*Wrong label*)
    … …  
    315315    if Val.is_int v then
    316316      try
    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
     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
    323323        let (s',k') = findlabel lbl f.f_body (callcont k) in
    324               (State_regular(f, s', k', sigma, e, m, i),l)
     324        (State_regular(f, s', k', sigma, e, m, i),l)
    325325      with _ -> error "int value too big."
    326326    else error "undefined switch value."
    … …  
    333333    (* applying current indexing on label *)
    334334    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;
     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;
    341341    (State_regular(f,s,k,sigma,e,m,i), [])
    342342(*  | _ -> error "state malformation." *)
    … …  
    357357    let (m, sp) = Mem.alloc m (concrete_stacksize f.f_stacksize) in
    358358    let lenv = init_local_env vargs f.f_params f.f_vars in
    359                 let i = CostLabel.new_const_ind i in
     359    let i = CostLabel.new_const_ind i in
    360360    State_regular(f,f.f_body,k,sp,lenv,m,i)
    361361  | F_ext f -> interpret_external k m i f.ef_tag vargs
    … …  
    365365  | State_call(fun_def,vargs,k,m,i) -> (step_call vargs k m i fun_def,[])
    366366  | State_return(v,Ct_returnto(None,f,sigma,e,k),m,i) ->
    367                 let i = CostLabel.forget_const_ind i in
     367    let i = CostLabel.forget_const_ind i in
    368368    (State_regular(f,St_skip,k,sigma,e,m,i),[])
    369369  | State_return(v,Ct_returnto(Some x,f,sigma,e,k),m,i) ->
    … …  
    404404    | Some main ->
    405405      let mem = init_mem prog in
    406                         let main = find_fundef main mem in
     406      let main = find_fundef main mem in
    407407      let first_state = (State_call (main,[],Ct_stop,mem,[]),[]) in
    408408      exec debug [] first_state

  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorPrinter.ml

    r1392 r1539  
    116116        (add_parenthesis e3)
    117117  | Cminor.Exp_cost (lab, e) ->
    118                   let lab = CostLabel.string_of_cost_label lab in
     118      let lab = CostLabel.string_of_cost_label lab in
    119119      Printf.sprintf "/* %s */ %s" lab (print_expression e)
    120120and add_parenthesis (Cminor.Expr (ed, _) as e) = match ed with
    … …  
    215215      Printf.sprintf "%sgoto %s;\n" (n_spaces n) lbl
    216216  | Cminor.St_cost (lbl, s) ->
    217                   let lbl = CostLabel.string_of_cost_label lbl in
     217      let lbl = CostLabel.string_of_cost_label lbl in
    218218      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)
     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)
    223223
    224224let print_internal f_name f_def =
    … …  
    265265  | Cminor.St_goto(_) -> "goto"
    266266  | Cminor.St_cost(_,_) -> "cost"
    267         | Cminor.St_ind_0 _ -> "index"
    268         | Cminor.St_ind_inc _ -> "increment"
     267  | Cminor.St_ind_0 _ -> "index"
     268  | Cminor.St_ind_inc _ -> "increment"

  • Deliverables/D2.2/8051-indexed-labels-branch/src/cminor/cminorToRTLabs.ml

    r1477 r1539  
    194194      let (rtlabs_fun, r2) = choose_destination rtlabs_fun lenv e2 in
    195195      let old_entry = rtlabs_fun.RTLabs.f_entry in
    196                         let r1_arg = RTLabs.Reg r1 in
    197                         let r2_arg = RTLabs.Reg r2 in
     196      let r1_arg = RTLabs.Reg r1 in
     197      let r2_arg = RTLabs.Reg r2 in
    198198      let stmt = RTLabs.St_op2 (op2, destr, r1_arg, r2_arg, old_entry) in
    199199      let rtlabs_fun = generate rtlabs_fun stmt in
    … …  
    204204      let old_entry = rtlabs_fun.RTLabs.f_entry in
    205205      let stmt =
    206                                 RTLabs.St_load (chunk, RTLabs.Reg r, destr, old_entry) in
     206        RTLabs.St_load (chunk, RTLabs.Reg r, destr, old_entry) in
    207207      let rtlabs_fun = generate rtlabs_fun stmt in
    208208      translate_expr rtlabs_fun lenv r e
    … …  
    287287      let old_entry = rtlabs_fun.RTLabs.f_entry in
    288288      let stmt =
    289                                 RTLabs.St_store (chunk, RTLabs.Reg addr, RTLabs.Reg r, old_entry) in
     289        RTLabs.St_store (chunk, RTLabs.Reg addr, RTLabs.Reg r, old_entry) in
    290290      let rtlabs_fun = generate rtlabs_fun stmt in
    291291      translate_exprs rtlabs_fun lenv [addr ; r] [e1 ; e2]
    … …  
    325325
    326326    | Cminor.St_seq (s1, s2) ->
    327       let rtlabs_fun = translate_stmt rtlabs_fun lenv s2 in
    328       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
    329329
    330330    | Cminor.St_ifthenelse (e, s1, s2) ->
    331331      let old_entry = rtlabs_fun.RTLabs.f_entry in
    332       let rtlabs_fun = translate_stmt rtlabs_fun lenv s2 in
     332      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s2 in
    333333      let lbl_false = rtlabs_fun.RTLabs.f_entry in
    334334      let rtlabs_fun = change_entry rtlabs_fun old_entry in
    335       let rtlabs_fun = translate_stmt rtlabs_fun lenv s1 in
     335      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s1 in
    336336      let lbl_true = rtlabs_fun.RTLabs.f_entry in
    337337      translate_branch rtlabs_fun lenv e lbl_true lbl_false
    … …  
    366366
    367367    | Cminor.St_label (lbl, s) ->
    368       let rtlabs_fun = translate_stmt rtlabs_fun lenv s in
     368      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in
    369369      let old_entry = rtlabs_fun.RTLabs.f_entry in
    370370      add_graph rtlabs_fun lbl (RTLabs.St_skip old_entry)
    371371
    372372    | Cminor.St_cost (lbl, s) ->
    373       let rtlabs_fun = translate_stmt rtlabs_fun lenv s in
     373      let rtlabs_fun = translate_stmt rtlabs_fun lenv (*exits*) s in
    374374      let old_entry = rtlabs_fun.RTLabs.f_entry in
    375375      generate rtlabs_fun (RTLabs.St_cost (lbl, old_entry))
    … …  
    460460
    461461  (* Complete the graph *)
    462   translate_stmt rtlabs_fun lenv f_def.Cminor.f_body
     462  translate_stmt rtlabs_fun lenv (*[]*) f_def.Cminor.f_body
    463463
    464464

  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml

    r1433 r1539  
    11module Atom =
    2         struct
    3                 include StringTools
    4         end
     2  struct
     3    include StringTools
     4  end
    55
    66module StringMap = Map.Make(String)
    … …  
    3535
    3636let 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"
     37  try
     38    ExtArray.set indexing n (ExtArray.get indexing n + 1)
     39  with | _ ->
     40    invalid_arg "uninitialized loop index"
    4141
    4242let curr_ind = function
    … …  
    172172let constant_map d x =
    173173  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
    174 
    175        
    176                 (**  **)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.mli

    r1433 r1539  
    22(** This module provides functions to manipulate and create indexed cost
    33    labels. *)
    4                
     4
    55(** [Atom] provides functions for cost atoms, the root of indexed costs *)
    66module Atom : sig
    7         include StringSig.S
     7  include StringSig.S
    88end
    99
    … …  
    1212type sexpr = Sexpr of int*int
    1313
     14(** The identity simple expression, used in initialization. *)
    1415val sexpr_id : sexpr
    1516
    16 (* trying a nameless approach *)
     17(** Indexes are identified with (single-entry) loop depths. *)
    1718type index = int
    1819
     20(** [make_id prefix index] produces an identifier out of a
     21    prefix and a loop depth. *)
    1922val make_id : string -> index -> string
    2023
    2124type indexing = sexpr list
    2225
     26(** The type of constant indexings, to be used by interpreations *)
    2327type const_indexing
    2428
     29(** [const_ind_iter f c] iterates [f] over the values of indexes in c *)
    2530val const_ind_iter : (int -> unit) -> const_indexing -> unit
    2631
    27 (** Top of the stack.
    28     @raise [Invalid_argument "non-empty indexing stack"] if argument is empty *)
     32(** This is equivalent to [List.hd], but raises
     33    [Invalid_argument "non-empty indexing stack"] if argument is empty *)
    2934val curr_const_ind : const_indexing list -> const_indexing
    3035
    3136(** [enter_loop inds n] is used to update the indexing stack [ind] when one
    3237    is entering a loop indexed by [n]. Raises [Invalid_argument
    33                 "non-empty indexing stack"] if [inds] is empty. *)
     38    "non-empty indexing stack"] if [inds] is empty. *)
    3439val enter_loop : const_indexing list -> index -> unit
    3540
    3641(** [enter_loop_opt inds (Some n)] behaves like [enter_loop inds n], and does
    3742    nothing in case of [None].
    38                 @see enter_loop *)
     43    @see enter_loop *)
    3944val enter_loop_opt : const_indexing list -> index option -> unit
    4045
    4146(** [continue_loop inds n] is used to update the indexing stack [inds] when
    4247    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]. *)
     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]. *)
    4651val continue_loop : const_indexing list -> index -> unit
    4752
    … …  
    5762(** [forget_const_ind inds] pops and discards the top constant indexing from the
    5863    stack [inds].  Raises [Invalid_argument "non-empty indexing stack"] if
    59                 [inds] is empty. *)
     64    [inds] is empty. *)
    6065val forget_const_ind : const_indexing list -> const_indexing list
    6166
    62 
    63  
    64 
    65 (** [empty_indexing] generates an empty indexing *)
     67(** [empty_indexing] is the empty indexing *)
    6668val empty_indexing : indexing
    6769
    … …  
    7274
    7375type t = {
    74         name : Atom.t;
    75         i : indexing
     76  name : Atom.t;
     77  i : indexing
    7678}
    7779
    … …  
    8082val comp_index : index -> sexpr -> t -> t
    8183
    82 
    8384(** [ev_indexing ind lbl] returns [lbl] where its indexing has been
    8485    evaluated in the constant indexing [ind].
    85                 @raise  Invalid_argument "constant indexing not enough to be applied" if
    86                 [ind] does not contain enough mappings to evaluate [lbl]'s indexing. *)
     86    @raise  Invalid_argument "constant indexing not enough to be applied" if
     87    [ind] does not contain enough mappings to evaluate [lbl]'s indexing. *)
    8788val ev_indexing : const_indexing -> t -> t
    8889
    8990(** [string_of_cost_label pref t] converts an indexed label to a
    90     string suitable for a label name in source
    91                 [string_of_cost_label ~pretty:true t] prints a more readable form *)
     91    string suitable for a label name in C source.
     92    [string_of_cost_label ~pretty:true t] prints a more readable form *)
    9293val string_of_cost_label : ?pretty : bool -> t -> string
    9394
    … …  
    106107    [x] to every element of the set [d]. *)
    107108val constant_map : Set.t -> 'a -> 'a Map.t
    108 
    109 

  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/label.ml

    r1468 r1539  
    2626
    2727end
    28 

  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/label.mli

    r1468 r1539  
    77(** Imperative label maps for use with Fix *)
    88module ImpMap : (Fix.IMPERATIVE_MAPS with type key = t)
    9        

  • Deliverables/D2.2/8051-indexed-labels-branch/src/dev_test.ml

    r1433 r1539  
    88let do_dev_test (filenames : string list) : unit =
    99
     10  let main_lbl = "main" in
     11  let exit_lbl = "exit" in
     12  let lbl = "label" in
     13
     14  let code =
     15    [(* Prelude *)
     16      `Call main_lbl ; (* call main *)
     17      `Label exit_lbl ; (* when coming back from main, do an infinite
     18                           jump here *)
     19      `Jmp exit_lbl ;
     20    (* Main *)
     21      `Label main_lbl ;
     22      `Mov (`DPTR, lbl) ; (* fetch the address of lbl in DPTR *)
     23    (* Push the address of lbl on the stack. *)
     24      `PUSH (I8051.reg_addr I8051.dpl) ; (* low bytes first *)
     25      `PUSH (I8051.reg_addr I8051.dph) ; (* then high bytes *)
     26      `RET ; (* this should jump to lbl, i.e. right below *)
     27      `Label lbl ;
     28      `RET (* jump to the exit label *)] in
     29
     30  (* Create a labelled ASM program with the code. *)
     31  let prog =
     32    { ASM.ppreamble = [] ;
     33      ASM.pexit_label = exit_lbl ;
     34      ASM.pcode = code ;
     35      ASM.phas_main = true } in
     36
     37  (* Assemble it. *)
     38  let prog = Languages.AstASM (ASMInterpret.assembly prog) in
     39
     40  (* Save the result in a fresh file prefixed by "yop" and whose extension is
     41     "hex". *)
     42  Languages.save false false "yop" "" prog
     43
     44(*
    1045  let f filename =
    11     Printf.printf "Processing %s...\n%!" filename ;
    12     let target = Languages.RTL in
    13     let print = false in
    14     let debug = true in
    15     let interpret = true in
    16     let p = Languages.parse Languages.Clight filename in
    17     let p = Languages.add_runtime p in
    18     let p = Languages.labelize p in
    19     let ps = Languages.compile false [] Languages.Clight target p in
    20     let f f' p = match Languages.language_of_ast p with
    21       | l when l = target -> f' p
    22       | _ -> ()
    23     in
    24     let actions =
    25       [(print, Languages.save false filename "") ;
    26        (interpret, (fun p -> ignore (Languages.interpret debug p)))] in
    27     List.iter (fun (b, f') -> if b then List.iter (f f') ps else ()) actions
     46  Printf.printf "Processing %s...\n%!" filename ;
     47  let target = Languages.RTL in
     48  let print = false in
     49  let debug = true in
     50  let interpret = true in
     51  let p = Languages.parse Languages.Clight filename in
     52  let p = Languages.add_runtime p in
     53  let p = Languages.labelize p in
     54  let ps = Languages.compile false Languages.Clight target p in
     55  let f f' p = match Languages.language_of_ast p with
     56  | l when l = target -> f' p
     57  | _ -> ()
     58  in
     59  let actions =
     60  [(print, Languages.save false false filename "") ;
     61  (interpret, (fun p -> ignore (Languages.interpret debug p)))] in
     62  List.iter (fun (b, f') -> if b then List.iter (f f') ps else ()) actions
    2863  in
    2964
    3065  List.iter f filenames
     66*)

  • Deliverables/D2.2/8051-indexed-labels-branch/src/languages.ml

    r1507 r1539  
    5353  | language -> [to_string language]
    5454
    55 let parse = function
     55let parse ?is_lustre_file ?remove_lustre_externals = function
    5656  | Clight ->
    57     fun filename -> AstClight (ClightParser.process filename)
     57    fun filename ->
     58      AstClight
     59        (ClightParser.process ?is_lustre_file ?remove_lustre_externals filename)
    5860
    5961(*
    … …  
    113115
    114116let ltl_to_lin = function
    115   | AstLTL p -> 
     117  | AstLTL p ->
    116118    AstLIN (LTLToLIN.translate p)
    117119  | _ -> assert false
    118120
    119121let lin_to_asm = function
    120   | AstLIN p -> 
     122  | AstLIN p ->
    121123    AstASM (LINToASM.translate p)
    122124  | _ -> assert false
    … …  
    137139
    138140let insert_transformations ts chain =
    139         (* turn transformation into elements of the compilation chain *)
    140         let trans_to_comp (n, t) = (n, n, t) in
    141         let ts = List.map trans_to_comp ts in
    142         (* ts and chain are merged, and then sorted so that the resulting list is *)
    143         (* still a well formed compilation chain. Stable sort preserves order *)
    144         (* between transformations on the same language as appearing in ts *)
    145         let compare (n1, n2, s) (m1, m2, t) = compare (n1, n2) (m1, m2) in
    146         List.stable_sort compare (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)
    147149
    148150let compile debug ts src tgt =
    149         (* insert intermediate transformations *)
     151  (* insert intermediate transformations *)
    150152  let chain = insert_transformations ts compilation_chain in
    151         (* erase transformations whose source is strictly before src *)
    152         let chain = List.filter (function (l1, _, _) -> l1 >= src) chain in
     153  (* erase transformations whose source is strictly before src *)
     154  let chain = List.filter (function (l1, _, _) -> l1 >= src) chain in
    153155  (* erase transformations whose target is strictly after tgt *)
    154         let chain = List.filter (function (_, l2, _) -> l2 <= tgt) chain in
     156  let chain = List.filter (function (_, l2, _) -> l2 <= tgt) chain in
    155157  (* Compose the atomic translations to build a compilation function
    156158     from [src] to [tgt]. Again, we assume that the compilation chain
    … …  
    217219let instrument cost_tern costs_mapping = function
    218220  | AstClight p ->
    219     let (p', cost_id, cost_incr) =
     221    let (p', cost_id, cost_incr, extern_cost_variables) =
    220222      ClightAnnotator.instrument cost_tern p costs_mapping in
    221     (AstClight p', cost_id, cost_incr)
     223    (AstClight p', cost_id, cost_incr, extern_cost_variables)
    222224(*
    223225  | AstCminor p ->
    … …  
    230232         "Instrumentation is not implemented for source language `%s'."
    231233         (to_string (language_of_ast p)));
    232     (p, "", "")
     234    (p, "", "", StringTools.Map.empty)
    233235
    234236let annotate cost_tern input_ast final =
    … …  
    236238  instrument cost_tern costs_mapping input_ast
    237239
    238 let string_output = function
     240let string_output asm_pretty = function
    239241  | AstClight p ->
    240242    [ClightPrinter.print_program p]
    … …  
    252254    [LINPrinter.print_program p]
    253255  | AstASM p ->
    254     [Pretty.print_program p ; ASMPrinter.print_program p]
    255 
    256 let save exact_output filename suffix ast =
     256    (if asm_pretty then [Pretty.print_program p]
     257     else ["Pretty print not requested"]) @
     258    [ASMPrinter.print_program p]
     259
     260let save asm_pretty exact_output filename suffix ast =
    257261  let ext_chopped_filename =
    258262    if exact_output then filename
    … …  
    267271    if exact_output then ext_filenames
    268272    else List.map Misc.SysExt.alternative ext_filenames in
    269   let output_strings = string_output ast in
     273  let output_strings = string_output asm_pretty ast in
    270274  let f filename s =
    271275    let cout = open_out filename in
    … …  
    275279  List.iter2 f output_filenames output_strings
    276280
    277 let save_cost filename cost_id cost_incr =
     281let save_cost exact_name filename cost_id cost_incr extern_cost_variables =
     282  let filename =
     283    if exact_name then filename
     284    else
     285      try Filename.chop_extension filename
     286      with Invalid_argument ("Filename.chop_extension") -> filename in
    278287  let cout = open_out (filename ^ ".cerco") in
     288  let f fun_name cost_var =
     289    output_string cout (fun_name ^ " " ^ cost_var ^ "\n") in
    279290  output_string cout (cost_id ^ "\n");
    280291  output_string cout (cost_incr ^ "\n");
     292  StringTools.Map.iter f extern_cost_variables;
    281293  flush cout;
    282294  close_out cout
    … …  
    299311  | AstASM p ->
    300312    ASMInterpret.interpret debug p
     313
     314let add_lustre_main
     315    lustre_test lustre_test_cases lustre_test_cycles
     316    lustre_test_min_int lustre_test_max_int = function
     317  | AstClight p ->
     318    AstClight
     319      (ClightLustreMain.add lustre_test lustre_test_cases lustre_test_cycles
     320         lustre_test_min_int lustre_test_max_int p)
     321  | _ ->
     322    Error.global_error "during main generation"
     323      "Lustre testing is only available with C programs."

  • Deliverables/D2.2/8051-indexed-labels-branch/src/languages.mli

    r1507 r1539  
    3939val language_of_ast : ast -> name
    4040
    41 (** [parse name] returns the parsing function of the language
    42     [name]. *)
    43 val parse : name -> (string -> ast)
     41(** [parse ?is_lustre_file ?remove_lustre_externals name] returns the parsing
     42    function of the language [name]. *)
     43val parse : ?is_lustre_file:bool -> ?remove_lustre_externals:bool ->
     44  name -> (string -> ast)
    4445
    4546(** {2 Compilation} *)
    … …  
    4748(** [compile debug ts l1 l2] returns the compilation function that
    4849    translates the language [l1] to the language [l2], employing the
    49                 transformations in [ts] along the way . This may be the
     50    transformations in [ts] along the way . This may be the
    5051    composition of several compilation functions. If [debug] is
    5152    [true], all the intermediate programs are inserted in the
    … …  
    7374(** [annotate cost_tern input_ast target_ast] inserts cost annotations into the
    7475    input AST from the (final) target AST. It also returns the name of the cost
    75     variable and the name of the cost increment function. The [cost_tern] flag
     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
    7678    rules whether cost increments are given by ternary expressions or branch
    7779    statements. *)
    78 val annotate : bool -> ast -> ast -> (ast * string * string)
     80val annotate : bool -> ast -> ast -> (ast * string * string * string StringTools.Map.t)
    7981
    8082(** [interpret debug ast] runs the program [ast] from the default initial
    … …  
    8486(** {2 Serialization} *)
    8587
    86 (** [save exact_output filename input_ast] pretty prints [input_ast] in a file
    87     whose name is prefixed by [filename] and whose extension is deduced from the
    88     language of the AST. If [exact_output] is false then the written file will
    89     be fresh. *)
    90 val save : bool -> string -> string -> ast -> unit
     88(** [save asm_pretty exact_output filename suffix input_ast] prints [input_ast]
     89    in a file whose name is prefixed by [filename], suffixed by [suffix] and
     90    whose extension is deduced from the language of the AST. If [exact_output]
     91    is false then the written file will be fresh. If [asm_pretty] is true, then
     92    an additional pretty-printed assembly file is output. *)
     93val save : bool -> bool -> string -> string -> ast -> unit
    9194
    92 (** [save_cost_incr filename cost_id cost_incr] prints the name [cost_id] of the
    93     cost variable and then the name [cost_incr] of the cost increment function
    94     in a seperate line in the file prefixed by [filename] and extended with
     95(** [save_cost exact_name filename cost_id cost_incr extern_cost_variables]
     96    prints the name [cost_id] of the cost variable, then the name [cost_incr] of
     97    the cost increment function, and the entries of the mapping
     98    [extern_cost_variables] (key first, then binding, seperated by a space) in a
     99    seperate line in the file prefixed by [filename] and extended with
    95100    ".cost". If the file already exists, it is overwritten. *)
    96 val save_cost : string -> string -> string -> unit
     101val save_cost : bool -> string -> string -> string ->
     102  string StringTools.Map.t -> unit
    97103
    98104(** [from_string s] parses [s] as an intermediate language name. *)
    … …  
    101107(** [to_string n] prints [n] as a string. *)
    102108val to_string   : name -> string
     109
     110(** [add_lustre_main lustre_test lustre_test_cases lustre_test_cycles
     111    lustre_test_min_int lustre_test_max_int ast] adds a main function that tests
     112    a Lustre step function to a Clight AST. The file [lustre_test] contains
     113    CerCo information (e.g. the name of the cost variable). The integer
     114    [lustre_test_cases] is the number of test cases that are performed, and the
     115    integer [lustre_test_cycles] is the number of cycles per test
     116    case. [lustre_test_min_int] (resp. [lustre_test_max_int]) is the minimum
     117    (resp. maximum) integer value randomly generated during testing, and. *)
     118val add_lustre_main : string -> int -> int -> int -> int -> ast -> ast

  • Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml

    r1507 r1539  
    4040let interpretation_requested () = !interpretation_flag
    4141
    42 let trace_flag         = ref false
    43 let request_trace = (:=) trace_flag
    44 let trace_requested () = !trace_flag
     42let interpretations_flag         = ref false
     43let request_interpretations      = (:=) interpretations_flag
     44let interpretations_requested () = !interpretations_flag
    4545
    4646let debug_flag                  = ref false
    … …  
    5656let set_cost_ternary            = (:=) cost_ternary_flag
    5757let is_cost_ternary_enabled ()  = !cost_ternary_flag
     58
     59let asm_pretty_flag             = ref false
     60let set_asm_pretty              = (:=) asm_pretty_flag
     61let is_asm_pretty ()            = !asm_pretty_flag
     62
     63let lustre_flag                 = ref false
     64let set_lustre_file             = (:=) lustre_flag
     65let is_lustre_file ()           = !lustre_flag
     66
     67let remove_lustre_externals       = ref false
     68let set_remove_lustre_externals   = (:=) remove_lustre_externals
     69let is_remove_lustre_externals () = !remove_lustre_externals
     70
     71let lustre_test                 = ref None
     72let set_lustre_test s           = lustre_test := Some s
     73let get_lustre_test ()          = !lustre_test
     74
     75let lustre_test_cases           = ref 100
     76let set_lustre_test_cases       = (:=) lustre_test_cases
     77let get_lustre_test_cases ()    = !lustre_test_cases
     78
     79let lustre_test_cycles          = ref 100
     80let set_lustre_test_cycles      = (:=) lustre_test_cycles
     81let get_lustre_test_cycles ()   = !lustre_test_cycles
     82
     83let lustre_test_min_int         = ref (-1000)
     84let set_lustre_test_min_int     = (:=) lustre_test_min_int
     85let get_lustre_test_min_int ()  = !lustre_test_min_int
     86
     87let lustre_test_max_int         = ref 1000
     88let set_lustre_test_max_int     = (:=) lustre_test_max_int
     89let get_lustre_test_max_int ()  = !lustre_test_max_int
     90
    5891
    5992(*
    … …  
    71104
    72105let basic_optimizations =
    73         [
    74                 LoopPeeling.trans;
    75                 ConstPropagation.trans;
    76                 CopyPropagation.trans;
    77                 RedundancyElimination.trans;
     106  [
     107    LoopPeeling.trans;
     108    ConstPropagation.trans;
     109    CopyPropagation.trans;
     110    RedundancyElimination.trans;
    78111    CopyPropagation.trans;
    79112    RedundancyElimination.trans
    80         ]
     113  ]
    81114 
    82115
    83116let options = OptionsParsing.register [
     117(*
    84118  "-s", Arg.String set_source_language,
    85119  " Choose the source language between:";
    86120  extra_doc " Clight, Cminor";
    87121  extra_doc " [default is C]";
     122*)
    88123
    89124  "-l", Arg.String set_target_language,
    … …  
    98133  " Interpret the compiled code.";
    99134
    100   "-t", Arg.Set trace_flag,
    101   " Interpret the compiled code and print all label traces.";
     135  "-is", Arg.Set interpretations_flag,
     136  " Interpret all the compilation passes.";
    102137
    103138  "-d", Arg.Set debug_flag,
    … …  
    106141  "-o", Arg.String set_output_files,
    107142  " Prefix of the output files.";
     143
     144  "-asm-pretty", Arg.Set asm_pretty_flag,
     145  " Output a pretty-printed assembly file.";
     146
     147  "-lustre", Arg.Set lustre_flag,
     148  " Input file is a Lustre file.";
     149
     150  "-remove-lustre-externals", Arg.Set remove_lustre_externals,
     151  " Remove Lustre externals.";
     152
     153  "-lustre-test", Arg.String set_lustre_test,
     154  " Input file is a Lustre file, testing requested.";
     155
     156  "-lustre-test-cases", Arg.Int set_lustre_test_cases,
     157  " Set the number of test cases when testing a Lustre";
     158  extra_doc " file.";
     159  extra_doc " [default is 100]";
     160
     161  "-lustre-test-cycles", Arg.Int set_lustre_test_cycles,
     162  " Set the number of cycles for each case when testing";
     163  extra_doc " a Lustre file.";
     164  extra_doc " [default is 100]";
     165
     166  "-lustre-test-min-int", Arg.Int set_lustre_test_min_int,
     167  " Random int minimum value when testing a Lustre file.";
     168  extra_doc " [default is -1000]";
     169
     170  "-lustre-test-max-int", Arg.Int set_lustre_test_max_int,
     171  " Random int maximum value when testing a Lustre file.";
     172  extra_doc " [default is 1000]";
    108173
    109174  "-peel", Arg.Unit (add_transformation LoopPeeling.trans),

  • Deliverables/D2.2/8051-indexed-labels-branch/src/options.mli

    r1507 r1539  
    99val get_target_language : unit -> Languages.name
    1010
    11 (** {2 Interpretation requests} *)
     11(** {2 Interpretation request} *)
    1212val request_interpretation   : bool -> unit
    1313val interpretation_requested : unit -> bool
    1414
    15 (** {2 Trace requests} *)
    16 val request_trace   : bool -> unit
    17 val trace_requested : unit -> bool
     15(** {2 Interpretation requests} *)
     16val request_interpretations   : bool -> unit
     17val interpretations_requested : unit -> bool
    1818
    1919(** {2 Annotation requests} *)
    … …  
    3535val is_cost_ternary_enabled : unit -> bool
    3636
     37(** {2 Assembly pretty print} *)
     38val set_asm_pretty : bool -> unit
     39val is_asm_pretty  : unit -> bool
     40
     41(** {2 Lustre file} *)
     42val set_lustre_file : bool -> unit
     43val is_lustre_file  : unit -> bool
     44
     45(** {2 Remove Lustre externals} *)
     46val set_remove_lustre_externals : bool -> unit
     47val is_remove_lustre_externals  : unit -> bool
     48
     49(** {2 Lustre file and test requested} *)
     50val set_lustre_test : string -> unit
     51val get_lustre_test : unit -> string option
     52
     53(** {2 Lustre file: number of test cases} *)
     54val set_lustre_test_cases : int -> unit
     55val get_lustre_test_cases : unit -> int
     56
     57(** {2 Lustre file: number of cycles for each case} *)
     58val set_lustre_test_cycles : int -> unit
     59val get_lustre_test_cycles : unit -> int
     60
     61(** {2 Lustre file: random int minimum value} *)
     62val set_lustre_test_min_int : int -> unit
     63val get_lustre_test_min_int : unit -> int
     64
     65(** {2 Lustre file: random int maximum value} *)
     66val set_lustre_test_max_int : int -> unit
     67val get_lustre_test_max_int : unit -> int
     68
     69
    3770(** {2 Intermediate transformations } *)
    3871val get_transformations : unit -> Languages.transformation list

  • Deliverables/D2.2/8051-indexed-labels-branch/src/utilities/stringSig.mli

    r818 r1539  
    99  val compare : t -> t -> int
    1010
    11   module Set : Set.S with type elt = t
     11  module Set : sig
     12    include Set.S with type elt = t
     13    val of_list : elt list -> t
     14    val unionl : t list -> t
     15  end
    1216
    1317  module Map : Map.S with type key = t
    … …  
    2125
    2226  val make_unique : Set.t -> (string -> string)
     27  val make_fresh  : Set.t -> string -> (unit -> string)
    2328
    2429end

  • Deliverables/D2.2/8051-indexed-labels-branch/src/utilities/stringTools.ml

    r818 r1539  
    77
    88
    9 module Set = Set.Make (String)
     9module Set = struct
     10  include Set.Make (String)
     11  let of_list l =
     12    let f res e = add e res in
     13    List.fold_left f empty l
     14  let unionl l = List.fold_left union empty l
     15end
    1016
    1117
    … …  
    5056    res in
    5157  unique
     58
     59let make_fresh set prefix =
     60  let fresh_prefix = Gen.fresh_prefix set prefix in
     61  let universe = Gen.new_universe fresh_prefix in
     62  (fun () -> Gen.fresh universe)
Note: See TracChangeset for help on using the changeset viewer.