Ignore:
Timestamp:
Oct 5, 2011, 10:20:41 AM (9 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:
6 edited
1 copied

Legend:

Unmodified
Added
Removed

  • 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
Note: See TracChangeset for help on using the changeset viewer.