plugin/compute_simple_stack_size.ml

   1 open Parameters
   2 open Cil_types
   3 open Simplify_terms
   4 module Varinfo = Cil_datatype.Varinfo
   5 module Stmt = Cil_datatype.Stmt
   6 module Term = Cil_datatype.Term
   7 module Logic_label = Cil_datatype.Logic_label
   8
   9
  10 (** This module defines the main analysis of the plug-in. Its actions are:
  11     - build the CFG of the program;
  12     - initialize the static environment of analysis (parameters of the
  13     functions, number of loops, etc);
  14     - compute the cost of each function depending on the costs of the others;
  15     - try to solve the inequations formed from the previous step so as to obtain
  16       an independent cost for each function;
  17     - save the results;
  18     - add the annotations on the program. *)
  19
  20
  21 (** Function computing cost of special instruction  *)
  22
  23 type env =
  24   { env_fun_cost : term Varinfo.Hashtbl.t;
  25     env_cost_incr_name : string; (* TODO put the varinfo *)
  26     env_cost_var_max : logic_var;
  27     env_cost_var : logic_var;
  28   }
  29
  30
  31 let cost_loop env kern_fun stmt lab_before_loop cost_body =
  32   (** invariant cost_max <= max(\old(cost_max), \old(cost) + [cost_body])
  33       invariant cost = \old(cost)
  34   *)
  35   (** first *)
  36   let cost_var_max = Logic_const.tvar env.env_cost_var_max in
  37   let old_cost_max = make_at lab_before_loop cost_var_max in
  38   let cost_var = Logic_const.tvar env.env_cost_var in
  39   let old_cost = make_at lab_before_loop cost_var in
  40   let cost_iterations = make_binop PlusA old_cost cost_body in
  41   let invariant = if Term.equal old_cost cost_iterations
  42     then Logic_const.prel (Req, cost_var_max, old_cost_max)
  43     else
  44       let new_cost = make_max old_cost_max cost_iterations in
  45       let new_cost = simplify_term new_cost in
  46       Logic_const.prel (Rle, cost_var_max, new_cost) in
  47   let annot =
  48     Logic_const.new_code_annotation
  49       (AInvariant ([stack_cost_behavior],true,invariant)) in
  50   Annotations.add kern_fun stmt [Ast.self] (User annot);
  51   (** second *)
  52   let invariant = Logic_const.prel (Req, cost_var, old_cost) in
  53   let annot =
  54     Logic_const.new_code_annotation
  55       (AInvariant ([stack_cost_behavior],true,invariant)) in
  56   Annotations.add kern_fun stmt [Ast.self] (User annot);
  57   cost_body
  58
  59 (** computing cost of fundec which contain a call to funvar *)
  60 let cost_of_fun_call env funvar args =
  61   (** can't fail since we use the callgraph *)
  62   let cost = Varinfo.Hashtbl.find env.env_fun_cost funvar in
  63   (* match cost.term_node with *)
  64   (* | TConst (CInt64 (_,_,_)) -> cost *)
  65   (* | _ -> *)
  66   (** arguments of the function *)
  67   let formals = Cil.getFormalsDecl funvar in
  68 (*  (** The real arguments are binded using a let and the formal argument are
  69       replaced by fresh variable *)
  70   let letvars = List.map
  71     (fun vi -> Cil.make_temp_logic_var (Ctype vi.vtype))
  72     formals in
  73   let subst = List.fold_left2 (fun map vi v ->
  74     Varinfo.Map.add vi v map) Varinfo.Map.empty formals letvars in
  75   let cost =
  76     Visitor.visitFramacTerm (new subst_lval subst (Project.current ()))
  77       cost in
  78   let cost = List.fold_left2 (fun tlet v arg ->
  79     let logic_info = { l_var_info = v; l_type = None; l_tparams = [];
  80                        l_labels = []; l_profile = [];
  81                        l_body = LBnone; } in
  82     let arg = term_of_exp arg in
  83     let tlet =
  84       Logic_const.term (Tlet (logic_info, arg))
  85         tlet.term_type in
  86     tlet)
  87     cost letvars args in*)
  88   let subst = List.fold_left2 (fun map vi arg ->
  89     try
  90       Varinfo.Map.add vi (term_of_exp arg) map
  91     with Untranslatable_expr _ -> map (** TODO verify that this formal doesn't
  92                                           appear in the cost of the function *)
  93   ) Varinfo.Map.empty formals args in
  94   let cost = remove_logic_label Logic_const.pre_label cost in
  95   let cost =
  96     Visitor.visitFramacTerm (new subst_lval subst (Project.current ()))
  97       cost in
  98   cost
  99
 100
 101 (** We go through the cfg we assume that:
 102     - all functions called have a cost already computed
 103     - no implicit loop (goto), all are explicit Loop
 104     - all loops have an invariant (given by the user or previously computed for
 105     for-loops)
 106
 107     We iterate on the cfg except when arriving on a loop where we compute the
 108     body alone and after that go to the next statements (the break statement)
 109
 110    break_statement in which statement to stop the sum (for loop)
 111  *)
 112
 113
 114 let rec find_variant = function
 115   | [] -> None
 116   | {annot_content = AVariant (t,_)}::_ -> Some t
 117   | _::l -> find_variant l
 118
 119 (** TODO: cache the statement already done after if-then-else
 120     (otherwise exponential) *)
 121 (** return None if no path arrive to a good_statement or don't go through
 122     a bad_statetement *)
 123 let rec cfg_sum env kern_fun bad_stmts stop_stmts stmt =
 124   if !debug then
 125     Format.printf "sid: %i,@ bad_stmts: %a,@ stop_stmts: %a,@\n"
 126       stmt.sid
 127       Stmt.Set.pretty bad_stmts
 128       Stmt.Set.pretty stop_stmts;
 129   (** statement in last statement *)
 130   if Stmt.Set.mem stmt stop_stmts
 131   then Some (Cil.lzero ())
 132   else if Stmt.Set.mem stmt bad_stmts
 133   then None
 134   else
 135   (** successors *)
 136   let succs_bad_stmts =
 137     match stmt.skind with
 138     | Loop (_,_,_,_,_) -> Stmt.Set.add stmt bad_stmts
 139     | _ -> bad_stmts in
 140   (** Cost of the successors of the instruction *)
 141   let cost_succs =
 142     cfg_sum_succs env kern_fun succs_bad_stmts stop_stmts
 143       stmt.succs in
 144   match cost_succs with
 145   | None -> None (** can't go in a good state so count nothing *)
 146   | Some cost_succs ->
 147   (** normalize the cost of the instruction regarding the labels *)
 148   let labels = NormAtLabels.labels_stmt_pre stmt in
 149   (** Cost of the instruction *)
 150
 151   let sum =
 152     match stmt.skind with
 153     (* (\** call to cost_incr *\) *)
 154     (** cost_stack_incr is not an usual function *)
 155     | Instr
 156         (Call (None,
 157                          { enode =
 158                              Lval (Var var, _)} ,
 159                          [cost], _))
 160         when var.vname = env.env_cost_incr_name ->
 161       make_binop PlusA cost_succs
 162         (make_max (Cil.lzero ()) (term_of_cost_expr cost))
 163     (** function call *)
 164     | Instr
 165         (Call (_, { enode =
 166             Lval (Var var, _)},
 167                          args,_)) ->
 168       let cost_instr = NormAtLabels.preproc_annot_term labels
 169         (cost_of_fun_call env var args) in
 170       make_max cost_succs cost_instr
 171     (** loops *)
 172     | Loop (_,_,_,_,_) ->
 173       (** the first one perhaps not needed *)
 174       let bad_stmts = Stmt.Set.union bad_stmts stop_stmts in
 175       let stop_stmts = Stmt.Set.singleton stmt in
 176       let cost_body =
 177         cfg_sum_succs env kern_fun bad_stmts stop_stmts stmt.succs in
 178       let cost_body = match cost_body with
 179         | None -> (* no cycle in fact *) Cil.lzero ()
 180         | Some cost -> simplify_term cost in
 181       if stmt.labels = [] then
 182         stmt.labels <- (** ugly but... *)
 183           Label("__stmt_"^(string_of_int stmt.sid),Cil.builtinLoc,false)::
 184           stmt.labels;
 185       let label_before_loop = StmtLabel (ref stmt) in
 186       let cost_instr =
 187         cost_loop env kern_fun stmt label_before_loop cost_body in
 188       let cost_instr = NormAtLabels.preproc_annot_term labels cost_instr in
 189       make_max cost_instr cost_succs
 190     | _ -> cost_succs in
 191   (** try to propagate \at(i,Label) *)
 192   let sum = match stmt.skind with
 193     | Instr (Set ((Var vi,_),e,_)) ->
 194       begin try
 195         let t = term_of_exp e in
 196         let subst = Varinfo.Map.singleton vi t in
 197         let sum =
 198           Visitor.visitFramacTerm
 199             (new subst_with_label stmt subst (Project.current ()))
 200             sum in
 201         sum
 202       with exn ->
 203         if !debug then Format.eprintf "can't convert exp %a to term: %a.@."
 204           Cil.defaultCilPrinter#pExp e print_exception exn;
 205         sum end
 206       | _ -> sum
 207   in
 208   (** remove the at that point to this statement we don't know the value at
 209       this point perhaps we will know before ( use Here?? ) *)
 210   let sum =
 211     Visitor.visitFramacTerm
 212       (new remove_stmt_label stmt (Project.current ()))
 213       sum in
 214   Some sum
 215
 216 and cfg_sum_succs env kern_fun bad_stmts stop_stmts stmts =
 217   let fold cost stmt =
 218     let cost_succ = cfg_sum env kern_fun bad_stmts stop_stmts stmt in
 219     make_max_opt cost cost_succ in
 220   List.fold_left fold None stmts
 221
 222 let make_leq_cost env sum =
 223     (** ensures cost_max <= max(\old(cost_max), [sum] + cost) *)
 224     let cost_var_max = Logic_const.tvar env.env_cost_var_max in
 225     let cost_var = Logic_const.tvar env.env_cost_var in
 226     let old_cost = Logic_const.told cost_var in
 227     let old_cost_max = Logic_const.told cost_var_max in
 228     let expr = make_binop PlusA sum old_cost in
 229     let expr = make_max old_cost_max expr in
 230     let post = Logic_const.prel (Rle, cost_var_max, expr) in
 231     let post = Logic_const.new_predicate post in
 232     post
 233
 234 let make_eq_cost env =
 235   (** ensures cost = old cost *)
 236   let cost_var = Logic_const.tvar env.env_cost_var in
 237   let old_cost = Logic_const.told cost_var in
 238   let post = Logic_const.prel (Req, cost_var, old_cost) in
 239   let post = Logic_const.new_predicate post in
 240   post
 241
 242
 243 let fun_sum env vi =
 244   let kernel_fun = Globals.Functions.get vi in
 245   let fst_stmt = Kernel_function.find_first_stmt kernel_fun in
 246   let last_stmt = Kernel_function.find_return kernel_fun in
 247   let bad_stmts = Stmt.Set.empty in
 248   let stop_stmts = Stmt.Set.singleton last_stmt in
 249   let sum = cfg_sum env kernel_fun bad_stmts stop_stmts fst_stmt in
 250   let sum = match sum with
 251     | None -> assert false (* Oups return not achievable?? *)
 252           (* Infinity!! *)
 253     | Some sum ->
 254       let sum = simplify_term sum in
 255       let sum = Logic_const.told sum in (** add old and push it *)
 256       let labels = NormAtLabels.labels_fct_post in
 257       let sum = NormAtLabels.preproc_annot_term labels sum in
 258       sum in
 259   if !debug then
 260     Format.printf "@[<hov 3>sum of %a: %a@]@."
 261       Cil.defaultCilPrinter#pVar vi
 262       Cil.defaultCilPrinter#pTerm sum;
 263 (** add postcondition about cost *)
 264   let mod_funspec funspec =
 265     let post = make_leq_cost env sum in
 266     let post2 = make_eq_cost env in
 267     let behavior =
 268       Cil.mk_behavior ~name:stack_cost_behavior ~post_cond:[Normal, post;
 269                                                       Normal, post2] () in
 270     {funspec with spec_behavior = behavior::funspec.spec_behavior;}
 271   in
 272   Kernel_function.set_spec kernel_fun mod_funspec;
 273   sum
 274
 275
 276 let initialize _tmp_prefix _fname
 277     cost_var cost_var_max cost_incr _extern_costs =
 278   (** TODO? use extern_costs for initializing env_fun_cost ? *)
 279   let callgraph = Callgraph.computeGraph (Ast.get ()) in
 280   if !debug then
 281     Printf.printf "callgraph size: %a\n%!" Callgraph.printGraph callgraph;
 282   let env = { env_fun_cost = Varinfo.Hashtbl.create 10;
 283               env_cost_incr_name = cost_incr;
 284               env_cost_var_max = cost_var_max;
 285               env_cost_var = cost_var
 286             } in
 287   let rec iter : 'a. 'a -> Callgraph.callnode -> unit = fun _ callnode ->
 288     match callnode.Callgraph.cnInfo with
 289     | Callgraph.NIVar (vi,{contents = true }) ->
 290       if not (Varinfo.Hashtbl.mem env.env_fun_cost vi) then begin
 291         Inthash.iter iter callnode.Callgraph.cnCallees;
 292         let sum = fun_sum env vi in
 293         Varinfo.Hashtbl.add env.env_fun_cost vi sum
 294       end
 295     | _ -> () (** put an undefined constant here for top *)
 296   in
 297   (** add the cost of cost_incr *)
 298   let cost_incr = Hashtbl.find callgraph cost_incr in
 299   let cost_incr = match cost_incr.Callgraph.cnInfo with
 300     | Callgraph.NIVar (vi,_) -> vi
 301     | _ -> assert false (* cost_incr must be at least declared *) in
 302   let arg_cost_incr = List.hd (Cil.getFormalsDecl cost_incr) in
 303   let sum_cost_incr = Logic_const.tvar (Cil.cvar_to_lvar arg_cost_incr) in
 304   let post_cost_incr = make_leq_cost env sum_cost_incr in
 305   let post_cost_incr2 =
 306     (** ensures cost = cost + incr *)
 307     let cost_var = Logic_const.tvar env.env_cost_var in
 308     let old_cost = Logic_const.told cost_var in
 309     let expr = make_binop PlusA sum_cost_incr old_cost in
 310     let post = Logic_const.prel (Req, cost_var, expr) in
 311     let post = Logic_const.new_predicate post in
 312     post in
 313   Kernel_function.set_spec (Globals.Functions.get cost_incr) (fun funspec ->
 314     let assigns =
 315       Writes [Logic_const.(new_identified_term (tvar cost_var_max)), FromAny;
 316               Logic_const.(new_identified_term (tvar cost_var)), FromAny] in
 317     let behavior =
 318       Cil.mk_behavior ~name:stack_cost_behavior
 319         ~post_cond:[Normal, post_cost_incr;Normal, post_cost_incr2]
 320         ~assigns () in
 321     {funspec with spec_behavior = behavior::funspec.spec_behavior;} );
 322   Varinfo.Hashtbl.add env.env_fun_cost cost_incr sum_cost_incr;
 323   (** make the other functions *)
 324   Hashtbl.iter iter callgraph
 325
 326 (** Save file *)
 327 let save_file fname =
 328   Kernel.CodeOutput.set fname ;
 329   File.pretty_ast ()
 330
 331 (*** Main ***)
 332
 333 exception NoStackInst
 334
 335 let cost ((fname, _), _, _cost_time, cost_stack) =
 336   match cost_stack with
 337   | None -> ()
 338   | Some (cost_stack_max, cost_stack_id) ->
 339     try
 340       if !debug then Printf.printf "Initialize stack size\n%!" ;
 341       let cost_var_max =
 342         try
 343           Cil.cvar_to_lvar (Globals.Vars.find_from_astinfo
 344                               cost_stack_max.Cerco.cost_id VGlobal)
 345         with _ -> raise NoStackInst in
 346       let cost_var =
 347         Cil.cvar_to_lvar (Globals.Vars.find_from_astinfo
 348                             cost_stack_id VGlobal) in
 349       initialize "__tmp" fname
 350         cost_var cost_var_max
 351         cost_stack_max.Cerco.cost_incr
 352         cost_stack_max.Cerco.extern_costs;
 353     with
 354     | NoStackInst ->
 355       Format.eprintf "No stack information found.\n%!"
 356     | e -> Format.eprintf "** ERROR: %a.@." print_exception_raise e