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
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;
18 - add the annotations on the program. *)
21 (** Function computing cost of special instruction *)
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;
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)
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)
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
48 Logic_const.new_code_annotation
49 (AInvariant ([stack_cost_behavior],true,invariant)) in
50 Annotations.add kern_fun stmt [Ast.self] (User annot);
52 let invariant = Logic_const.prel (Req, cost_var, old_cost) in
54 Logic_const.new_code_annotation
55 (AInvariant ([stack_cost_behavior],true,invariant)) in
56 Annotations.add kern_fun stmt [Ast.self] (User annot);
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 *)
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))
73 let subst = List.fold_left2 (fun map vi v ->
74 Varinfo.Map.add vi v map) Varinfo.Map.empty formals letvars in
76 Visitor.visitFramacTerm (new subst_lval subst (Project.current ()))
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 = [];
82 let arg = term_of_exp arg in
84 Logic_const.term (Tlet (logic_info, arg))
87 cost letvars args in*)
88 let subst = List.fold_left2 (fun map vi arg ->
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
96 Visitor.visitFramacTerm (new subst_lval subst (Project.current ()))
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
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)
110 break_statement in which statement to stop the sum (for loop)
114 let rec find_variant = function
116 | {annot_content = AVariant (t,_)}::_ -> Some t
117 | _::l -> find_variant l
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
123 let rec cfg_sum env kern_fun bad_stmts stop_stmts stmt =
125 Format.printf "sid: %i,@ bad_stmts: %a,@ stop_stmts: %a,@\n"
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
136 let succs_bad_stmts =
137 match stmt.skind with
138 | Loop (_,_,_,_,_) -> Stmt.Set.add stmt bad_stmts
140 (** Cost of the successors of the instruction *)
142 cfg_sum_succs env kern_fun succs_bad_stmts stop_stmts
144 match cost_succs with
145 | None -> None (** can't go in a good state so count nothing *)
147 (** normalize the cost of the instruction regarding the labels *)
148 let labels = NormAtLabels.labels_stmt_pre stmt in
149 (** Cost of the instruction *)
152 match stmt.skind with
153 (* (\** call to cost_incr *\) *)
154 (** cost_stack_incr is not an usual function *)
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))
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
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
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)::
185 let label_before_loop = StmtLabel (ref stmt) in
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
191 (** try to propagate \at(i,Label) *)
192 let sum = match stmt.skind with
193 | Instr (Set ((Var vi,_),e,_)) ->
195 let t = term_of_exp e in
196 let subst = Varinfo.Map.singleton vi t in
198 Visitor.visitFramacTerm
199 (new subst_with_label stmt subst (Project.current ()))
203 if !debug then Format.eprintf "can't convert exp %a to term: %a.@."
204 Cil.defaultCilPrinter#pExp e print_exception exn;
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?? ) *)
211 Visitor.visitFramacTerm
212 (new remove_stmt_label stmt (Project.current ()))
216 and cfg_sum_succs env kern_fun bad_stmts stop_stmts stmts =
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
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
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
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?? *)
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
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
268 Cil.mk_behavior ~name:stack_cost_behavior ~post_cond:[Normal, post;
270 {funspec with spec_behavior = behavior::funspec.spec_behavior;}
272 Kernel_function.set_spec kernel_fun mod_funspec;
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
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
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
295 | _ -> () (** put an undefined constant here for top *)
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
313 Kernel_function.set_spec (Globals.Functions.get cost_incr) (fun funspec ->
315 Writes [Logic_const.(new_identified_term (tvar cost_var_max)), FromAny;
316 Logic_const.(new_identified_term (tvar cost_var)), FromAny] in
318 Cil.mk_behavior ~name:stack_cost_behavior
319 ~post_cond:[Normal, post_cost_incr;Normal, post_cost_incr2]
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
327 let save_file fname =
328 Kernel.CodeOutput.set fname ;
333 exception NoStackInst
335 let cost ((fname, _), _, _cost_time, cost_stack) =
336 match cost_stack with
338 | Some (cost_stack_max, cost_stack_id) ->
340 if !debug then Printf.printf "Initialize stack size\n%!" ;
343 Cil.cvar_to_lvar (Globals.Vars.find_from_astinfo
344 cost_stack_max.Cerco.cost_id VGlobal)
345 with _ -> raise NoStackInst in
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;
355 Format.eprintf "No stack information found.\n%!"
356 | e -> Format.eprintf "** ERROR: %a.@." print_exception_raise e