src/annotStackSize.ml

   1
   2
   3 let error_prefix = "Clight Stack Size Annotator"
   4 let error = Error.global_error error_prefix
   5
   6
   7 let stack_id_prefix = "__stack_size"
   8 let stack_max_id_prefix = "__stack_size_max"
   9 let stack_incr_prefix = "__stack_size_incr"
  10
  11
  12 let fun_stack_size = Hashtbl.create 10
  13
  14 let add_stack_size s i =
  15   Hashtbl.add fun_stack_size s i
  16
  17 let get_stack_size s =
  18   try
  19     Hashtbl.find fun_stack_size s
  20   with Not_found ->
  21     Printf.eprintf
  22       "get_stack_size: the function %s has not a stack size associated\n%!"
  23       s;
  24     exit 1
  25
  26 (* Instrumentation *)
  27
  28 let int_typ = Clight.Tint (Clight.I32, AST.Signed)
  29
  30 let const_int i = Clight.Expr (Clight.Econst_int i, int_typ)
  31
  32 (* Instrument a statement. *)
  33
  34 let rec instrument_body stack_incr stack_size stmt = match stmt with
  35   | Clight.Sskip | Clight.Sbreak | Clight.Scontinue
  36   | Clight.Sgoto _ ->
  37     stmt
  38   | Clight.Sassign (e1, e2) -> Clight.Sassign (e1, e2)
  39   | Clight.Scall (eopt, f, args) -> stmt
  40   | Clight.Ssequence (s1, s2) ->
  41     Clight.Ssequence (instrument_body stack_incr stack_size s1,
  42                       instrument_body stack_incr stack_size s2)
  43   | Clight.Sifthenelse (e, s1, s2) ->
  44     let s1' = instrument_body stack_incr stack_size s1 in
  45     let s2' = instrument_body stack_incr stack_size s2 in
  46     Clight.Sifthenelse (e, s1', s2')
  47   | Clight.Swhile (e, s) ->
  48     let s' = instrument_body stack_incr stack_size s in
  49     Clight.Swhile (e, s')
  50   | Clight.Sdowhile (e, s) ->
  51     let s' = instrument_body stack_incr stack_size s in
  52     Clight.Sdowhile (e, s')
  53   | Clight.Sfor (s1, e, s2, s3) ->
  54     let s1' = instrument_body stack_incr stack_size s1 in
  55     let s2' = instrument_body stack_incr stack_size s2 in
  56     let s3' = instrument_body stack_incr stack_size s3 in
  57     Clight.Sfor (s1', e, s2', s3')
  58   | Clight.Sreturn _ ->
  59     let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
  60     let f = Clight.Expr (Clight.Evar stack_incr, fun_typ) in
  61     let ss = Clight.Expr (Clight.Econst_int stack_size, int_typ) in
  62     let args = [Clight.Expr (Clight.Eunop(Clight.Oneg,ss),int_typ)] in
  63     Clight.Ssequence (Clight.Scall (None, f, args), stmt)
  64   | Clight.Sswitch (e, ls) ->
  65     let ls' = instrument_ls stack_incr stack_size ls in
  66     Clight.Sswitch (e, ls')
  67   | Clight.Slabel (lbl, s) ->
  68     let s' = instrument_body stack_incr stack_size s in
  69     Clight.Slabel (lbl, s')
  70   | Clight.Scost (lbl, s) ->
  71     (* Keep the cost label in the code. *)
  72     let s' = instrument_body stack_incr stack_size s in
  73     Clight.Scost (lbl, s')
  74   (*
  75     instrument_body stack_incr s
  76   *)
  77 and instrument_ls stack_incr stack_size = function
  78   | Clight.LSdefault s ->
  79     let s' = instrument_body stack_incr stack_size s in
  80     Clight.LSdefault s'
  81   | Clight.LScase (i, s, ls) ->
  82     let s' = instrument_body stack_incr stack_size s in
  83     let ls' = instrument_ls stack_incr stack_size ls in
  84     Clight.LScase (i, s', ls')
  85
  86 (* Instrument a function. *)
  87
  88 let instrument_funct stack_incr (id, def) =
  89   let def = match def with
  90     | Clight.Internal def ->
  91       let stack_size = get_stack_size id in
  92       let body = instrument_body stack_incr
  93         stack_size def.Clight.fn_body in
  94       let body =
  95         let fun_typ = Clight.Tfunction ([int_typ], Clight.Tvoid) in
  96         let f = Clight.Expr (Clight.Evar stack_incr, fun_typ) in
  97         let args = [Clight.Expr (Clight.Econst_int stack_size, int_typ)] in
  98         Clight.Ssequence (Clight.Scall (None, f, args), body) in
  99       Clight.Internal { def with Clight.fn_body = body }
 100     | Clight.External _ -> def
 101   in
 102   (id, def)
 103
 104 (* This is the declaration of the cost variable. *)
 105
 106 let add_stack_decl stack_id =
 107   let init = [Clight.Init_int32 0] in
 108   ((stack_id, init), int_typ)
 109
 110 (* This is the definition of the increment cost function. *)
 111
 112 let stack_incr_def stack_id_max stack_id stack_incr =
 113   let int_var x = Clight.Expr (Clight.Evar x, int_typ) in
 114   let param = "incr" in
 115   let cost = int_var stack_id in
 116   let cost_max = int_var stack_id_max in
 117   let increment = int_var param in
 118   let stack_increment =
 119     Clight.Expr (Clight.Ebinop (Clight.Oadd, cost, increment), int_typ) in
 120   let stmt1 = Clight.Sassign (cost, stack_increment) in
 121   let stack_max =
 122     Clight.Expr (
 123       Clight.Econdition(
 124         Clight.Expr (Clight.Ebinop (Clight.Olt, cost_max, cost), int_typ),
 125           cost,cost_max), int_typ) in
 126   let stmt2 = Clight.Sassign (cost_max, stack_max) in
 127   let cfun =
 128     { Clight.fn_return = Clight.Tvoid ;
 129       Clight.fn_params = [(param, int_typ)] ;
 130       Clight.fn_vars   = [] ;
 131       Clight.fn_body = Clight.Ssequence(stmt1,stmt2) } in
 132   (stack_incr, Clight.Internal cfun)
 133
 134 (* Create a fresh uninitialized cost variable for each external function. This
 135    will be used by the Cost plug-in of the Frama-C platform. *)
 136
 137 let extern_stack_variables make_unique functs =
 138   let prefix = "_stack_of_" in
 139   let f (decls, map) (_, def) = match def with
 140     | Clight.Internal _ -> (decls, map)
 141     | Clight.External (id, _, _) ->
 142       let new_var = make_unique (prefix ^ id) in
 143       (decls @ [add_stack_decl new_var], StringTools.Map.add id new_var map) in
 144   List.fold_left f ([], StringTools.Map.empty) functs
 145
 146 let save_tmp tmp_file s =
 147   let cout = open_out tmp_file in
 148   output_string cout s ;
 149   flush cout ;
 150   close_out cout
 151
 152 (** [instrument prog stack_map] instruments the program [prog]. First a fresh
 153     global variable --- the so-called cost variable --- is added to the program.
 154     Then, each cost label in the program is replaced by an increment of the cost
 155     variable, following the mapping [stack_map]. The function also returns the
 156     name of the cost variable and the name of the cost increment function. *)
 157
 158 let instrument cost_incr p =
 159
 160   (* Create a fresh 'cost' variable. *)
 161   let names = ClightAnnotator.names p in
 162   let make_unique = StringTools.make_unique names in
 163   let stack_id = make_unique stack_id_prefix in
 164   let stack_max_id = make_unique stack_max_id_prefix in
 165   let stack_decl = add_stack_decl stack_id in
 166   let stack_max_decl = add_stack_decl stack_max_id in
 167
 168   (* Create a fresh uninitialized global variable for each extern function. *)
 169   let (extern_stack_decls, extern_stack_variables) =
 170     extern_stack_variables make_unique p.Clight.prog_funct in
 171
 172   (* Define an increment function for the cost variable. *)
 173   let stack_incr =
 174     StringTools.Gen.fresh_prefix (StringTools.Set.add stack_id names)
 175       stack_incr_prefix in
 176   let stack_incr_def = stack_incr_def stack_max_id stack_id stack_incr in
 177
 178   (* Instrument each function *)
 179   let prog_funct =
 180     List.map (fun ((id,_) as a) ->
 181       if id = cost_incr then a else instrument_funct stack_incr a)
 182       p.Clight.prog_funct in
 183
 184   (* Glue all this together. *)
 185   let prog_vars = stack_decl :: stack_max_decl
 186     :: extern_stack_decls @ p.Clight.prog_vars in
 187   let prog_funct = stack_incr_def :: prog_funct in
 188   let p' =
 189     { p with Clight.prog_vars = prog_vars ; Clight.prog_funct = prog_funct } in
 190
 191   (* Save the resulted program. Then re-parse it.
 192      Indeed, the instrumentation may add side-effects in expressions, which is
 193      not Clight compliant. Re-parsing the result with CIL will remove these
 194      side-effects in expressions to obtain a Clight program. *)
 195   let output = ClightPrinter.print_program p' in
 196   let res = ClightParser.process (`Source ("annotated", output)) in
 197   (res, stack_id, stack_max_id, stack_incr, extern_stack_variables)