Changeset 1291 for Deliverables/D2.2


Ignore:
Timestamp:
Oct 5, 2011, 10:20:41 AM (8 years ago)
Author:
tranquil
Message:

Started branch of untrusted compiler with indexed labels

  • added indexing structure to CostLabel?
  • propagated changes to other modules
  • added indexing as parameter to labelling
  • loop indexes not implemented yet, so behaviour is still the same
Location:
Deliverables/D2.2/8051-indexed-labels-branch
Files:
22 edited
1 copied

Legend:

Unmodified
Added
Removed

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

    r619 r1291  
    102102type labelled_instruction =
    103103 [ instruction
    104  | `Cost of string
     104 | `Cost of CostLabel.t
    105105 | `Label of string
    106106 | `Jmp of string
    … …  
    122122type program =
    123123    { code        : BitVectors.byte list ;
    124       cost_labels : string BitVectors.WordMap.t ;
     124      cost_labels : CostLabel.t BitVectors.WordMap.t ;
    125125      exit_addr   : BitVectors.word ;
    126126      has_main    : bool }

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

    r818 r1291  
    131131
    132132  exit_addr   : BitVectors.word;
    133   cost_labels : string BitVectors.WordMap.t
     133  cost_labels : CostLabel.t BitVectors.WordMap.t
    134134}
    135135

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

    r743 r1291  
    9898
    9999      exit_addr   : BitVectors.word;
    100       cost_labels : string BitVectors.WordMap.t
     100      cost_labels : CostLabel.t BitVectors.WordMap.t
    101101    }
    102102     

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

    r818 r1291  
    4343 function
    4444    `Label l -> l ^ ":"
    45   | `Cost l -> l ^ ":"
     45                (* ugly-printing *)
     46  | `Cost l -> CostLabel.string_of_cost_label l ^ ":"
    4647  | `Jmp j -> "ljmp  " ^ j
    4748  | `Call j -> "lcall " ^ j
    … …  
    106107       cost
    107108       (if BitVectors.WordMap.mem pc p.ASM.cost_labels then
    108            (BitVectors.WordMap.find pc p.ASM.cost_labels)
    109         else ""),
     109                                 let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in
     110               CostLabel.string_of_cost_label ~pretty:true lbl
     111              else ""),
    110112     new_pc) in
    111113  fst (List.fold_left f ("", BitVectors.zero `Sixteen) p.ASM.code)

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

    r818 r1291  
    4343    Printf.sprintf "*** %s *** --> %s" s lbl
    4444  | ERTL.St_cost (cost_lbl, lbl) ->
     45                let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    4546    Printf.sprintf "emit %s --> %s" cost_lbl lbl
    4647  | ERTL.St_get_hdw (r1, r2, lbl) ->

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

    r818 r1291  
    2626    Printf.sprintf "*** %s ***" s
    2727  | LIN.St_cost cost_lbl ->
    28     Printf.sprintf "emit %s" cost_lbl
     28    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
     29                Printf.sprintf "emit %s" cost_lbl
    2930  | LIN.St_int (dstr, i) ->
    3031    Printf.sprintf "imm %s, %d" (print_reg dstr) i

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

    r818 r1291  
    1212  | LIN.St_goto lbl
    1313  | LIN.St_label lbl
    14   | LIN.St_cost lbl
    1514  | 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)
    1617  | _ -> Label.Set.empty
    1718

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

    r818 r1291  
    2525    Printf.sprintf "*** %s *** --> %s" s lbl
    2626  | LTL.St_cost (cost_lbl, lbl) ->
     27    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    2728    Printf.sprintf "emit %s --> %s" cost_lbl lbl
    2829  | LTL.St_int (dstr, i, lbl) ->

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

    r818 r1291  
    4343  | RTL.St_skip lbl -> "--> " ^ lbl
    4444  | RTL.St_cost (cost_lbl, lbl) ->
     45    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
    4546    Printf.sprintf "emit %s --> %s" cost_lbl lbl
    4647  | RTL.St_addr (dstr1, dstr2, id, lbl) ->

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

    r818 r1291  
    136136  | RTLabs.St_skip lbl -> "--> " ^ lbl
    137137  | RTLabs.St_cost (cost_lbl, lbl) ->
    138       Printf.sprintf "emit %s --> %s" cost_lbl lbl
     138    let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
     139    Printf.sprintf "emit %s --> %s" cost_lbl lbl
    139140  | RTLabs.St_cst (destr, cst, lbl) ->
    140141      Printf.sprintf "imm %s, %s --> %s"

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

    r619 r1291  
    1414    in
    1515    let sentence (k, (v1, v2)) =
     16                        let k = CostLabel.string_of_cost_label ~pretty:true k in
    1617      Printf.sprintf "  Label %s %s in language `%s' \
    1718                        whereas it %s in language `%s'."
    18         k (string_of_value v1) lang1 (string_of_value v2) lang2
     19             k (string_of_value v1) lang1 (string_of_value v2) lang2
    1920    in
    2021    String.concat "\n" (List.map sentence ds)

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

    r818 r1291  
    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. *)
    118118
    119   | Ecost of CostLabel.t*expr                   (**r cost label. *)
     119  | Ecost of CostLabel.t * expr                 (**r cost label. *)
    120120  | Ecall of ident * expr * expr
    121121

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

    r818 r1291  
    2525   Label.Set.union user_labels1 user_labels2)
    2626
    27 let empty_triple = (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
     27let empty_triple =
     28        (StringTools.Set.empty, CostLabel.Set.empty, Label.Set.empty)
    2829
    2930let name_singleton id =
    3031  (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty)
    3132
    32 let cost_label_singleton cost_lbl =
    33   (StringTools.Set.empty, CostLabel.Set.singleton cost_lbl, Label.Set.empty)
     33let cost_label_singleton lbl =
     34  (StringTools.Set.empty, CostLabel.Set.singleton lbl, Label.Set.empty)
    3435
    3536let label_singleton lbl =
    … …  
    7778        (StringTools.Set.union vars names, cost_labels, user_labels)
    7879    | Clight.External (id, _, _) ->
    79         (StringTools.Set.singleton id, CostLabel.Set.empty, Label.Set.empty) in
     80        (StringTools.Set.singleton id, CostLabel.Set.empty,
     81         Label.Set.empty) in
    8082  let fun_idents (id, f_def) =
    8183    let (names, cost_labels, user_labels) = def_idents f_def in
    … …  
    9395let all_labels p =
    9496  let (_, cost_labels, user_labels) = prog_idents p in
    95   let all =
    96     CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
    97       cost_labels StringTools.Set.empty in
    98   Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all
     97        let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     98  let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
     99  Label.Set.fold StringTools.Set.add user_labels all
    99100
    100101let all_idents p =
    101102  let (names, cost_labels, user_labels) = prog_idents p in
     103        let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in
     104  let cost_labels = CostLabel.Set.fold f cost_labels StringTools.Set.empty in
    102105  let to_string_set fold set =
    103106    fold (fun lbl idents -> StringTools.Set.add lbl idents) set
    104107      StringTools.Set.empty in
    105   let cost_labels = to_string_set CostLabel.Set.fold cost_labels in
    106108  let user_labels = to_string_set Label.Set.fold user_labels in
    107109  StringTools.Set.union names (StringTools.Set.union cost_labels user_labels)

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

    r818 r1291  
    66    Then, each cost label in the program is replaced by an increment of the cost
    77    variable, following the mapping [cost_map]. The function also returns the
    8     name of the cost variable and the name of the cost increment function. *)
    9 
     8    name of the cost variable and the name of the cost increment function.
     9               
     10    TODO: int to expressions *)
    1011val instrument : Clight.program -> int CostLabel.Map.t ->
    1112                 Clight.program * string * string

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

    r818 r1291  
    104104  | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
    105105  | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
    106   | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
     106  | Ecost (cost_lbl, e) ->
     107                let cost_lbl = CostLabel.string_of_cost_label cost_lbl in
     108                "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
    107109  | Ecall (f, arg, e) ->
    108110    "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
    … …  
    129131  | Slabel (lbl, _) -> "label " ^ lbl
    130132  | Sgoto lbl -> "goto " ^ lbl
    131   | Scost (lbl, _) -> "cost " ^ lbl
     133  | Scost (lbl, _) ->
     134    let lbl = CostLabel.string_of_cost_label lbl in
     135                "cost " ^ lbl
    132136
    133137let string_of_local_env lenv =

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

    r818 r1291  
    66
    77
    8 (* Add a cost label in front of a statement. *)
     8(* Add a cost label in front of a statement with the current indexing. *)
    99
    10 let add_starting_cost_label cost_universe stmt =
    11   Clight.Scost (CostLabel.Gen.fresh cost_universe, stmt)
     10let add_starting_cost_label indexing cost_universe stmt =
     11  Clight.Scost (CostLabel.fresh indexing cost_universe, stmt)
    1212
    1313(* Add a cost label at the end of a statement. *)
    1414
    15 let add_ending_cost_label cost_universe stmt =
    16   Clight.Ssequence (stmt, add_starting_cost_label cost_universe Clight.Sskip)
     15let add_ending_cost_label indexing cost_universe stmt =
     16        let lbld_skip = add_starting_cost_label indexing cost_universe Clight.Sskip in
     17  Clight.Ssequence (stmt, lbld_skip)
    1718
    1819
    … …  
    2425
    2526
    26 let add_cost_label_e cost_universe e =
    27   Expr (Ecost (CostLabel.Gen.fresh cost_universe, e), typeof e)
     27let add_cost_label_e indexing cost_universe e =
     28  Expr (Ecost (CostLabel.fresh indexing cost_universe, e), typeof e)
    2829
    2930
    3031(* Add cost labels to an expression. *)
    3132
    32 let rec add_cost_labels_e cost_universe = function 
    33   | Expr (exp,cty) -> Expr (add_cost_labels_expr cost_universe exp,cty)
     33let rec add_cost_labels_e ind cost_universe = function 
     34  | Expr (exp,cty) -> Expr (add_cost_labels_expr ind cost_universe exp,cty)
    3435
    35 and add_cost_labels_expr cost_universe exp = match exp with
     36and add_cost_labels_expr ind cost_universe exp = match exp with
    3637  | Econst_int _ | Econst_float _ | Evar _ | Esizeof _ -> exp
    37   | Ederef e -> Ederef (add_cost_labels_e cost_universe e)
    38   | Eaddrof e -> Eaddrof (add_cost_labels_e cost_universe e)
    39   | Eunop (op,e) -> Eunop (op,(add_cost_labels_e cost_universe e))
     38  | Ederef e -> Ederef (add_cost_labels_e ind cost_universe e)
     39  | Eaddrof e -> Eaddrof (add_cost_labels_e ind cost_universe e)
     40  | Eunop (op,e) -> Eunop (op,(add_cost_labels_e ind cost_universe e))
    4041  | Ebinop (op,e1,e2) ->
    4142      Ebinop (op,
    42               add_cost_labels_e cost_universe e1,
    43               add_cost_labels_e cost_universe e2)
    44   | Ecast (t,e) -> Ecast (t, add_cost_labels_e cost_universe e)
     43              add_cost_labels_e ind cost_universe e1,
     44              add_cost_labels_e ind cost_universe e2)
     45  | Ecast (t,e) -> Ecast (t, add_cost_labels_e ind cost_universe e)
    4546  | Eandbool (e1,e2) ->
    46       let e1' = add_cost_labels_e cost_universe e1 in
    47       let e2' = add_cost_labels_e cost_universe e2 in
    48       let b1 = add_cost_label_e cost_universe (const_int 1) in
    49       let b2 = add_cost_label_e cost_universe (const_int 0) in
     47      let e1' = add_cost_labels_e ind cost_universe e1 in
     48      let e2' = add_cost_labels_e ind cost_universe e2 in
     49      let b1 = add_cost_label_e ind cost_universe (const_int 1) in
     50      let b2 = add_cost_label_e ind cost_universe (const_int 0) in
    5051      let e2' = Expr (Econdition (e2', b1, b2), int_type) in
    51       let e2' = add_cost_label_e cost_universe e2' in
    52       let e3' = add_cost_label_e cost_universe (const_int 0) in
     52      let e2' = add_cost_label_e ind cost_universe e2' in
     53      let e3' = add_cost_label_e ind cost_universe (const_int 0) in
    5354      Econdition (e1', e2', e3')
    5455  | Eorbool (e1,e2) ->
    55       let e1' = add_cost_labels_e cost_universe e1 in
    56       let e2' = add_cost_label_e cost_universe (const_int 1) in
    57       let e3' = add_cost_labels_e cost_universe e2 in
    58       let b1 = add_cost_label_e cost_universe (const_int 1) in
    59       let b2 = add_cost_label_e cost_universe (const_int 0) in
     56      let e1' = add_cost_labels_e ind cost_universe e1 in
     57      let e2' = add_cost_label_e ind cost_universe (const_int 1) in
     58      let e3' = add_cost_labels_e ind cost_universe e2 in
     59      let b1 = add_cost_label_e ind cost_universe (const_int 1) in
     60      let b2 = add_cost_label_e ind cost_universe (const_int 0) in
    6061      let e3' = Expr (Econdition (e3', b1, b2), int_type) in
    61       let e3' = add_cost_label_e cost_universe e3' in
     62      let e3' = add_cost_label_e ind cost_universe e3' in
    6263      Econdition (e1', e2', e3')
    63   | Efield (e,id) -> Efield (add_cost_labels_e cost_universe e,id)
     64  | Efield (e,id) -> Efield (add_cost_labels_e ind cost_universe e,id)
    6465  | Econdition (e1,e2,e3) ->
    65       let e1' = add_cost_labels_e cost_universe e1 in
    66       let e2' = add_cost_labels_e cost_universe e2 in
    67       let e2' = add_cost_label_e cost_universe e2' in
    68       let e3' = add_cost_labels_e cost_universe e3 in
    69       let e3' = add_cost_label_e cost_universe e3' in
     66      let e1' = add_cost_labels_e ind cost_universe e1 in
     67      let e2' = add_cost_labels_e ind cost_universe e2 in
     68      let e2' = add_cost_label_e ind cost_universe e2' in
     69      let e3' = add_cost_labels_e ind cost_universe e3 in
     70      let e3' = add_cost_label_e ind cost_universe e3' in
    7071      Econdition (e1', e2', e3')
    7172  | Ecost (_,_) | Ecall _ -> assert false (* Should not happen *)
    7273
    73 let add_cost_labels_opt cost_universe = function
    74   | None -> None
    75   | Some e -> Some (add_cost_labels_e cost_universe e)
     74let add_cost_labels_opt ind cost_universe =
     75        Option.map (add_cost_labels_e ind cost_universe)
    7676
    77 let add_cost_labels_lst cost_universe l =
    78   List.map (add_cost_labels_e cost_universe) l
     77let add_cost_labels_lst ind cost_universe l =
     78  List.map (add_cost_labels_e ind cost_universe) l
    7979
    8080
    8181(* Add cost labels to a statement. *)
    8282
    83 let rec add_cost_labels_st cost_universe = function
     83let rec add_cost_labels_st ind cost_universe = function
    8484  | Sskip -> Sskip
    8585  | Sassign (e1,e2) ->
    86       Sassign (add_cost_labels_e cost_universe e1,
    87                add_cost_labels_e cost_universe e2)
     86      Sassign (add_cost_labels_e ind cost_universe e1,
     87               add_cost_labels_e ind cost_universe e2)
    8888  | Scall (e1,e2,lst) ->
    89       Scall (add_cost_labels_opt cost_universe e1,
    90              add_cost_labels_e cost_universe e2,
    91              add_cost_labels_lst cost_universe lst)
     89      Scall (add_cost_labels_opt ind cost_universe e1,
     90             add_cost_labels_e ind cost_universe e2,
     91             add_cost_labels_lst ind cost_universe lst)
    9292  | Ssequence (s1,s2) ->
    93       Ssequence (add_cost_labels_st cost_universe s1,
    94                  add_cost_labels_st cost_universe s2)
     93      Ssequence (add_cost_labels_st ind cost_universe s1,
     94                 add_cost_labels_st ind cost_universe s2)
    9595  | Sifthenelse (e,s1,s2) ->
    96       let s1' = add_cost_labels_st cost_universe s1 in
    97       let s1' = add_starting_cost_label cost_universe s1' in
    98       let s2' = add_cost_labels_st cost_universe s2 in
    99       let s2' = add_starting_cost_label cost_universe s2' in
    100       Sifthenelse (add_cost_labels_e cost_universe e, s1', s2')
     96      let s1' = add_cost_labels_st ind cost_universe s1 in
     97      let s1' = add_starting_cost_label ind cost_universe s1' in
     98      let s2' = add_cost_labels_st ind cost_universe s2 in
     99      let s2' = add_starting_cost_label ind cost_universe s2' in
     100      Sifthenelse (add_cost_labels_e ind cost_universe e, s1', s2')
    101101  | Swhile (e,s) ->
    102       let s' = add_cost_labels_st cost_universe s in
    103       let s' = add_starting_cost_label cost_universe s' in
    104       add_ending_cost_label cost_universe
    105         (Swhile (add_cost_labels_e cost_universe e, s'))
     102      let s' = add_cost_labels_st ind cost_universe s in
     103      let s' = add_starting_cost_label ind cost_universe s' in
     104      add_ending_cost_label ind cost_universe
     105        (Swhile (add_cost_labels_e ind cost_universe e, s'))
    106106  | Sdowhile (e,s) ->
    107       let s1 = add_cost_labels_st cost_universe s in
    108       let s2 = add_cost_labels_st cost_universe s in
    109       let s2' = add_starting_cost_label cost_universe s2 in
    110       add_ending_cost_label cost_universe
    111         (Ssequence (s1, Swhile (add_cost_labels_e cost_universe e, s2')))
     107      let s1 = add_cost_labels_st ind cost_universe s in
     108      let s2 = add_cost_labels_st ind cost_universe s in
     109      let s2' = add_starting_cost_label ind cost_universe s2 in
     110      add_ending_cost_label ind cost_universe
     111        (Ssequence (s1, Swhile (add_cost_labels_e ind cost_universe e, s2')))
    112112  | Sfor (s1,e,s2,s3) ->
    113       let s1' = add_cost_labels_st cost_universe s1 in
    114       let s2' = add_cost_labels_st cost_universe s2 in
    115       let s3' = add_cost_labels_st cost_universe s3 in
    116       let s3' = add_starting_cost_label cost_universe s3' in
    117       add_ending_cost_label cost_universe
    118         (Sfor (s1', add_cost_labels_e cost_universe e, s2', s3'))
    119   | Sreturn e -> Sreturn (add_cost_labels_opt cost_universe e)
     113      let s1' = add_cost_labels_st ind cost_universe s1 in
     114      let s2' = add_cost_labels_st ind cost_universe s2 in
     115      let s3' = add_cost_labels_st ind cost_universe s3 in
     116      let s3' = add_starting_cost_label ind cost_universe s3' in
     117      add_ending_cost_label ind cost_universe
     118        (Sfor (s1', add_cost_labels_e ind cost_universe e, s2', s3'))
     119  | Sreturn e -> Sreturn (add_cost_labels_opt ind cost_universe e)
    120120  | Sswitch (e,ls) ->
    121       Sswitch (add_cost_labels_e cost_universe e,
    122                add_cost_labels_ls cost_universe ls)
     121      Sswitch (add_cost_labels_e ind cost_universe e,
     122               add_cost_labels_ls ind cost_universe ls)
    123123  | Slabel (lbl,s) ->
    124       let s' = add_cost_labels_st cost_universe s in
    125       let s' = add_starting_cost_label cost_universe s' in
     124      let s' = add_cost_labels_st ind cost_universe s in
     125      let s' = add_starting_cost_label ind cost_universe s' in
    126126      Slabel (lbl,s')
    127127  | Scost (_,_) -> assert false
    128128  | _ as stmt -> stmt
    129129
    130 and add_cost_labels_ls cost_universe = function
     130and add_cost_labels_ls ind cost_universe = function
    131131  | LSdefault s ->
    132       let s' = add_cost_labels_st cost_universe s in
    133       let s' = add_starting_cost_label cost_universe s' in
     132      let s' = add_cost_labels_st ind cost_universe s in
     133      let s' = add_starting_cost_label ind cost_universe s' in
    134134      LSdefault s'
    135135  | LScase (i,s,ls) ->
    136       let s' = add_cost_labels_st cost_universe s in
    137       let s' = add_starting_cost_label cost_universe s' in
    138       LScase (i, s', add_cost_labels_ls cost_universe ls)
     136      let s' = add_cost_labels_st ind cost_universe s in
     137      let s' = add_starting_cost_label ind cost_universe s' in
     138      LScase (i, s', add_cost_labels_ls ind cost_universe ls)
    139139
    140140
    141141(* Add cost labels to a function. *)
    142142
    143 let add_cost_labels_f cost_universe = function
     143let add_cost_labels_f ind cost_universe = function
    144144  | (id,Internal fd) -> (id,Internal {
    145145      fn_return = fd.fn_return ;
    146146      fn_params = fd.fn_params ;
    147147      fn_vars = fd.fn_vars ;
    148       fn_body = add_starting_cost_label cost_universe
    149                              (add_cost_labels_st cost_universe fd.fn_body)
     148      fn_body = add_starting_cost_label ind cost_universe
     149                             (add_cost_labels_st ind cost_universe fd.fn_body)
    150150    })
    151151  | (id,External (a,b,c)) -> (id,External (a,b,c))
    … …  
    157157let add_cost_labels p =
    158158  let labs = ClightAnnotator.all_labels p in
    159   let labs = StringTools.Set.fold CostLabel.Set.add labs CostLabel.Set.empty in
    160   let cost_prefix = CostLabel.Gen.fresh_prefix labs "_cost" in
    161   let cost_universe = CostLabel.Gen.new_universe cost_prefix in
     159        let add = CostLabel.Atom.Set.add in
     160        let empty = CostLabel.Atom.Set.empty in
     161  let labs = StringTools.Set.fold add labs empty in
     162  let cost_prefix = CostLabel.Atom.Gen.fresh_prefix labs "_cost" in
     163  let cost_universe = CostLabel.Atom.Gen.new_universe cost_prefix in
     164        let ind = CostLabel.Indexing.empty in
    162165  {
    163     prog_funct = List.map (add_cost_labels_f cost_universe) p.prog_funct;
     166    prog_funct = List.map (add_cost_labels_f ind cost_universe) p.prog_funct;
    164167    prog_main = p.prog_main;
    165168    prog_vars = p.prog_vars

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

    r818 r1291  
    196196  | Efield(e1, id) ->
    197197      fprintf p "%a.%s" print_expr_prec (level, e1) id
    198   | Ecost (lbl,e1) ->
    199       fprintf p "(/* %s */ %a)" lbl print_expr e1
    200   | Ecall (f, arg, e) ->
     198  | Ecost(lbl, e1) ->
     199                  (* printing label uglily even if in comment for consistence *)
     200                  let lbl = CostLabel.string_of_cost_label lbl in
     201                        fprintf p "(/* %s */ %a)" lbl print_expr e1
     202  | Ecall(f, arg, e) ->
    201203      fprintf p "(%s(%a), %a)" f print_expr arg print_expr e
    202204
    … …  
    272274      fprintf p "goto %s;" lbl
    273275 | Scost (lbl,s1) ->
     276           let lbl = CostLabel.string_of_cost_label lbl in
    274277     fprintf p "%s:@ %a" lbl print_stmt s1
    275278

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

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

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

    r818 r1291  
    6565  | St_label (lbl, _) -> "label " ^ lbl
    6666  | St_goto lbl -> "goto " ^ lbl
    67   | St_cost (lbl, _) -> "cost " ^ lbl
     67  | St_cost (lbl, _) ->
     68                let lbl = CostLabel.string_of_cost_label lbl in
     69                "cost " ^ lbl
    6870
    6971let print_state = function

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

    r818 r1291  
    116116        (add_parenthesis e3)
    117117  | Cminor.Exp_cost (lab, e) ->
     118                  let lab = CostLabel.string_of_cost_label lab in
    118119      Printf.sprintf "/* %s */ %s" lab (print_expression e)
    119120and add_parenthesis (Cminor.Expr (ed, _) as e) = match ed with
    … …  
    208209      Printf.sprintf "%sgoto %s;\n" (n_spaces n) lbl
    209210  | Cminor.St_cost (lbl, s) ->
    210       Printf.sprintf "%s%s:\n%s"
    211         (n_spaces n) lbl (print_body n s)
     211                  let lbl = CostLabel.string_of_cost_label lbl in
     212      Printf.sprintf "%s%s:\n%s" (n_spaces n) lbl (print_body n s)
    212213
    213214let print_internal f_name f_def =

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

    r486 r1291  
     1module Atom =
     2        struct
     3                include StringTools
     4        end
    15
    2 include StringTools
     6module StringMap = Map.Make(String)
     7
     8module Index =
     9        struct
     10                include StringTools
     11        end
     12
     13(** Simple expressions are for now affine maps of the form a*_+b *)
     14type sexpr =
     15    | Sexpr of int*int
     16
     17let sexpr_id = Sexpr(1, 0)
     18
     19let sexpr_of i l = snd (List.find (function (j, _) -> j = i) l)
     20
     21(** not using Map as insertion order matters *)
     22module Indexing =
     23        struct
     24                type t = (Index.t * sexpr) list
     25                let compare = compare (* built-in lexicographic order *)
     26                let empty = []
     27        end
     28
     29(* a*_+b is composed with c*_+d by substitution: *)
     30(* namely a*_+b ° c*_+d = c*(a*_+b)+d              *)
     31let compose_sexpr (Sexpr(a, b)) (Sexpr(c, d)) =
     32    Sexpr (a * c, b * c + d)
     33
     34(* i|-->e ° j|-->f = j|-->e°f   if i=j,  j|-->f otherwise *)
     35(* NB: if simple expressions are changed to more complex ones,*)
     36(* this must change *)
     37let compose_index_singl i1 s1 (i2,s2) =
     38    (i2, if i1 = i2 then compose_sexpr s1 s2 else s2)
     39
     40(* i|-->e ° I *)
     41let compose_index i s = List.map (compose_index_singl i s)
     42
     43(* I°J applies every mapping in I to every mapping in J *)
     44(* TODO: can we use the shape indexings have in actual usage? *)
     45let compose_indexing = List.fold_right (function (i,s) -> compose_index i s)
     46
     47
     48module IndexingSet = Set.Make(Indexing)
     49
     50
     51type t = {
     52    name : Atom.t;
     53    i : Indexing.t
     54}
     55
     56(* if [pretty] is false then a name suitable for labels is given*)
     57(* ('P' replaces '+') *)
     58let string_of_sexpr pretty id (Sexpr(a, b)) =
     59        let plus = if pretty then "+" else "P" in
     60  let a_id_s = if a = 1 then id else string_of_int a^id in
     61        let b_s = string_of_int b in
     62        if a = 0 then b_s else
     63        if b = 0 then a_id_s else a_id_s^plus^b_s
     64       
     65(* examples:*)
     66(* [pretty] true:  (0,i+1,2j+2)*)
     67(* [pretty] false: _0_iP1_2jP2 *)
     68let string_of_indexing pretty = function
     69        | [] -> ""
     70        | (i, s) :: l ->
     71                (* !!! assuming i starts with '_' which can be omitted !!! *)
     72                let i = String.sub i 1 (String.length i) in
     73                let left = if pretty then "(" else "_" in
     74                let right = if pretty then ")" else "" in
     75                let sep = if pretty then "," else "_" in
     76                let first = string_of_sexpr pretty i s in
     77                let f accu (j, t) = accu ^ sep ^ (string_of_sexpr pretty j t) in
     78                left ^ List.fold_left f first l ^ right
     79               
     80let string_of_cost_label ?(pretty = false) lab =
     81        lab.name ^ string_of_indexing pretty lab.i
     82
     83let fresh l universe =
     84        {name = Atom.Gen.fresh universe; i = l} 
     85
     86(* TODO: urgh. Necessary? *)
     87type aux_t = t
     88                                                       
     89(** labels are endowed with a lexicographical ordering *)
     90module T : Map.OrderedType with type t = aux_t =
     91    struct
     92        type t = aux_t
     93        let compare = compare (* uses the built-in lexicographical comparison *)
     94    end
     95
     96module Map = Map.Make(T)   
     97module Set = Set.Make(T)
     98(** [constant_map d x] produces a finite map which associates
     99    [x] to every element of the set [d]. *)
     100
     101let indexings_of atom s =
     102        let f k accu = if k.name = atom then IndexingSet.add k.i accu else accu in
     103        Set.fold f s IndexingSet.empty
    3104
    4105let constant_map d x =
    5106  Set.fold (fun k accu -> Map.add k x accu) d Map.empty
     107       
     108        (**  **)

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

    r486 r1291  
    11
    2 (** This module provides functions to manipulate and create fresh cost
     2(** This module provides functions to manipulate and create indexed cost
    33    labels. *)
     4               
     5(** [Atom] provides functions for cost atoms, the root of indexed costs *)
     6module Atom : sig
     7        include StringSig.S
     8end
    49
    5 include StringSig.S
     10(** Loop indices, to be identified with Clight identifiers *)
     11module Index : sig
     12        include StringSig.S
     13end
     14
     15(** Simple expressions corresponding to loop tranformations. *)
     16type sexpr
     17
     18val sexpr_id : sexpr
     19
     20module Indexing : sig
     21        include Set.OrderedType
     22        val empty : t
     23end
     24
     25(** [sexpr_of i l] extracts the simple expression relative to [i] in [l].
     26    It raises an [Invalid_argument] exception if [i] is not handled by [l] *)
     27val sexpr_of : Index.t -> Indexing.t -> sexpr
     28
     29(** [compose_index i s l] applies the transformation [i] |--> [s] to [l] *)
     30val compose_index : Index.t -> sexpr -> Indexing.t -> Indexing.t
     31
     32(** [compose_index l m] applies all the transformations in  [l] to [m] *)
     33val compose_indexing : Indexing.t -> Indexing.t -> Indexing.t
     34
     35module IndexingSet : Set.S with type elt = Indexing.t
     36
     37type t = {
     38        name : Atom.t;
     39        i : Indexing.t
     40}
     41
     42(** [string_of_cost_label t] converts an indexed label to a
     43    string suitable for a label name in source.
     44                [string_of_cost_label ~pretty:true t] prints a more readable form *)
     45val string_of_cost_label : ?pretty : bool -> t -> string
     46
     47(** [fresh i u] creates a fresh label using [u] as name universe, inside
     48    the indexing [i] (which represents the nested loops containing the label) *)
     49val fresh : Indexing.t -> Atom.Gen.universe -> t
     50
     51module Set : Set.S with type elt = t
     52module Map : Map.S with type key = t
     53
     54(** [indexings_of a s] produces the set of indexings of an atom [a] occurring
     55    in the set of indexed labels [s]. *)
     56val indexings_of : Atom.t -> Set.t -> IndexingSet.t
    657
    758(** [constant_map d x] produces a finite map which associates
    859    [x] to every element of the set [d]. *)
    960val constant_map : Set.t -> 'a -> 'a Map.t
     61
Note: See TracChangeset for help on using the changeset viewer.