Changeset 1679 for Deliverables/D5.15.3/costplugin/plugin/compute.ml
 Timestamp:
 Feb 7, 2012, 6:01:43 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D5.15.3/costplugin/plugin/compute.ml
r1462 r1679 1 1 2 (** This module adds ACSL annotations to a C file transformed by CerCo's 3 compiler. The annotations are a synthesis of the ones added by CerCo and 4 specify an upper bound of the WCET of each function of the input program. *) 5 6 (** Only a subset of the C constructions are supported: 7  everything that is not supported by CerCo is not supported by the plugin 8 (switches in particular); 9  gotos are not supported; 10  (potentially mutually) recursive functions are not supported; 11  pointer functions are not supported; 12  inside a function, parameters must not be assigned nor their address 13 accessed; 14  loops must start with an initialization (of the socalled loop counter), 15 have a guard condition comparing the loop counter with <, <=, > or >=, and 16 end with an incrementation (or a decrementation) of the loop counter. The 17 expressions in the initialization, the guard and the increment must only 18 refer to parameters, and the parameters cannot be assigned nor their 19 address accessed in the whole function, and the loop counter cannot be 20 assigned nor its address taken inside the loop's body (except in the 21 incrementation). *) 22 23 (** The synthesis proceeds as follows: 24 1 The synthesis environment is initialized. 25 2 The cost of each function is computed. At this stage, the costs may 26 depend on the cost of the other functions, but they are left abstract. 27 3 Using the results of 2, a system of equations is created and tried to 28 be solved. It is solved if the algorithm succeeds in computing the cost 29 of each function independently of the cost of the other functions. 30 4 Using the results of 3, annotations are added in the source code. *) 31 2 (* TODO: goto'ed label: top cost *) 32 3 33 4 (*** Exceptions ***) 34 5 35 (* Raised when the algorithm fails to solve the system of inequations made by 36 the cost of each function. *) 37 exception Unresolvable 38 (* Raised when the cost update function inside the source code is called with a 39 nonconstant argument. This should not occur if the code originates from 40 CerCo. *) 41 exception Cost_incr_arg_not_constant 42 (* Raised when a function pointer is found. *) 43 exception Unresolvable_function 44 exception Unsupported_exp 45 exception Unsupported_loop of string 46 exception Unknown_function of string 47 exception Nested_loops 48 (* Other unsupported cases. *) 49 exception Unsupported of string 50 51 let string_of_exception cost_incr = function 52  Unresolvable > "Costs are unresovable (recursion?)." 53  Cost_incr_arg_not_constant > 54 "Call to the update cost function " ^ cost_incr ^ 55 " with a nonconstant integer argument." 56  Unresolvable_function > "Cannot resolve call (function pointer?)." 57  Unsupported s > "Unsupported instruction: " ^ s ^ "." 58  Unsupported_loop s > "Unsupported loop: " ^ s ^ "." 59  Unknown_function f > "Unknown function definition " ^ f ^ "." 60  Nested_loops > "Nested loops." 61  Unsupported_exp  Cost_value.Unsupported_exp > "Unsupported expression." 62  Cost_value.Unsupported_rel > "Unsupported guard condition." 6 exception ASM_unsupported 7 exception Try_unsupported 8 9 let string_of_exception = function 10  ASM_unsupported > "ASM instructions not supported" 11  Try_unsupported > "Try instructions not supported" 12  Cost_value.Unknown_cost fun_name > 13 "Cost for function " ^ fun_name ^ " not found." 14  Cost_value.Unknown_prototype fun_name > 15 "Prototype for function " ^ fun_name ^ " not found." 63 16  e > raise e 64 17 65 18 19 (*** Debug flag ***) 20 21 let debug = ref false 22 23 66 24 (*** Helpers ***) 67 25 68 26 let identity x = x 69 27 28 let string_of_list sep f l = 29 let rec aux = function 30  [] > "" 31  [e] > f e 32  e :: l > (f e) ^ sep ^ (aux l) in 33 aux l 34 70 35 let integer_term term = Logic_const.term term Cil_types.Linteger 36 37 let tinteger i = 38 let cint64 = Cil_types.CInt64 (Int64.of_int i, Cil_types.IInt, None) in 39 let iterm = Cil_types.TConst cint64 in 40 integer_term iterm 41 42 let cil_logic_int_var x = 43 Logic_const.tvar (Cil_const.make_logic_var x Cil_types.Linteger) 44 45 type loops_annotation = 46 (string > string > 47 (Db_types.rooted_code_annotation Db_types.before_after) list) 48 49 type loops_annotations = loops_annotation list 71 50 72 51 let add_loop_annot obj stmt annot = 73 52 Queue.add (fun () > Annotations.add stmt [Ast.self] annot) 74 53 obj#get_filling_actions 54 55 let add_loop_annots obj stmt annots = List.iter (add_loop_annot obj stmt) annots 75 56 76 57 let loop_annotation annot = Db_types.Before (Db_types.User annot) … … 101 82 let cost_var = Cil_const.make_logic_var cost_id Cil_types.Linteger in 102 83 let cost_var = Logic_const.tvar cost_var in 103 let cost = Cost_value.to_cil_term cost in104 84 let old_cost = 105 85 Logic_const.term (Cil_types.Told cost_var) cost_var.Cil_types.term_type in … … 108 88 Logic_const.prel (rel, cost_var, new_cost) 109 89 110 let rec make_freshes fundec n prefix = 111 let name = prefix ^ "_tmp" ^ (string_of_int (n1)) in 112 if n <= 0 then [] 113 else (make_freshes fundec (n1) prefix) @ 114 [Cil.makeTempVar fundec ~name Cil.intType] 115 116 117 (*** Annotation environment ***) 118 119 type fun_info = 120 { (* Variables whose address may be accessed. *) 121 addressed : StringTools.Set.t ; 122 parameters : string list ; 123 locals : StringTools.Set.t ; 124 (* Variables that may be assigned. *) 125 modified : StringTools.Set.t ; 126 nb_loops : int } 127 128 let mk_fun_info addressed parameters locals modified nb_loops = 129 { addressed = addressed ; 130 parameters = parameters ; 131 locals = locals ; 132 modified = modified ; 133 nb_loops = nb_loops } 134 135 let init_fun_info = 136 mk_fun_info 137 StringTools.Set.empty [] StringTools.Set.empty StringTools.Set.empty 0 138 139 (** An environment associates to each function: the variables whose address may 140 be accessed, the list of its parameters, its locals, and the variables that 141 may be assigned. *) 142 143 type env = 144 { fun_infos : fun_info StringTools.Map.t ; 145 cost_varinfo : Cil_types.varinfo } 146 147 let mk_env fun_infos cost_varinfo = 148 { fun_infos = fun_infos ; cost_varinfo = cost_varinfo } 149 150 let init_env = 151 mk_env StringTools.Map.empty (Cil.makeVarinfo true false "dummy" Cil.intType) 152 153 let get_fun_infos env = env.fun_infos 154 155 let get_cost_varinfo env = env.cost_varinfo 156 157 let upd_fun_infos env fun_infos = { env with fun_infos = fun_infos } 158 159 let upd_cost_varinfo env cost_varinfo = 160 { env with cost_varinfo = cost_varinfo } 161 162 let get_fun_info env fun_name = 163 if StringTools.Map.mem fun_name (get_fun_infos env) then 164 StringTools.Map.find fun_name (get_fun_infos env) 165 else raise (Unknown_function fun_name) 166 167 let upd_fun_info env fun_name fun_info = 168 let fun_infos = StringTools.Map.add fun_name fun_info (get_fun_infos env) in 169 upd_fun_infos env fun_infos 170 171 let get_addressed env fun_name = 172 (get_fun_info env fun_name).addressed 173 174 (** [is_addressed_variable env fun_name x] returns true iff the address of the 175 variable [x] may be accessed in function [fun_name] considering the 176 environment [env]. *) 177 178 let is_addressed_variable env fun_name x = 179 StringTools.Set.mem x (get_addressed env fun_name) 180 181 (** [has_addressed env fun_name set] returns true iff the address of a variable 182 of the set [set] may be accessed in function [fun_name] considering the 183 environment [env]. *) 184 185 let has_addressed env fun_name set = 186 let f x res = res  (is_addressed_variable env fun_name x) in 187 StringTools.Set.fold f set false 188 189 let upd_addressed env fun_name addressed = 190 let fun_info = get_fun_info env fun_name in 191 let fun_info = { fun_info with addressed = addressed } in 192 upd_fun_info env fun_name fun_info 193 194 let get_parameters env fun_name = (get_fun_info env fun_name).parameters 195 196 (** [is_parameter env fun_name x] returns true iff [x] is a parameter of the 197 function [fun_name] considering the environment [env]. *) 198 199 let is_parameter env fun_name x = List.mem x (get_parameters env fun_name) 200 201 (** [are_parameters env fun_name set] returns true iff all variables in the set 202 [set] are parameters of the function [fun_name] considering the environment 203 [env]. *) 204 205 let are_parameters env fun_name set = 206 let f x res = res && (is_parameter env fun_name x) in 207 StringTools.Set.fold f set true 208 209 let prototypes env = 210 let f fun_info = fun_info.parameters in 211 StringTools.Map.map f (get_fun_infos env) 212 213 let get_locals env fun_name = (get_fun_info env fun_name).locals 214 215 let get_modified env fun_name = (get_fun_info env fun_name).modified 216 217 let upd_modified env fun_name modified = 218 let fun_info = get_fun_info env fun_name in 219 let fun_info = { fun_info with modified = modified } in 220 upd_fun_info env fun_name fun_info 221 222 let get_nb_loops env fun_name = 223 (get_fun_info env fun_name).nb_loops 224 225 let upd_nb_loops env fun_name nb_loops = 226 let fun_info = get_fun_info env fun_name in 227 let fun_info = { fun_info with nb_loops = nb_loops } in 228 upd_fun_info env fun_name fun_info 229 230 let add_nb_loops env fun_name = 231 upd_nb_loops env fun_name ((get_nb_loops env fun_name) + 1) 90 let rec remove_casts e = match e.Cil_types.enode with 91  Cil_types.Lval lval > 92 { e with Cil_types.enode = Cil_types.Lval (remove_casts_lval lval) } 93  Cil_types.SizeOfE e > 94 { e with Cil_types.enode = Cil_types.SizeOfE (remove_casts e) } 95  Cil_types.AlignOfE e > 96 { e with Cil_types.enode = Cil_types.AlignOfE (remove_casts e) } 97  Cil_types.UnOp (unop, e, typ) > 98 { e with Cil_types.enode = Cil_types.UnOp (unop, remove_casts e, typ) } 99  Cil_types.BinOp (binop, e1, e2, typ) > 100 let enode = 101 Cil_types.BinOp (binop, remove_casts e1, remove_casts e2, typ) in 102 { e with Cil_types.enode } 103  Cil_types.CastE (_, e) > remove_casts e 104  Cil_types.AddrOf lval > 105 { e with Cil_types.enode = Cil_types.AddrOf (remove_casts_lval lval) } 106  Cil_types.StartOf lval > 107 { e with Cil_types.enode = Cil_types.StartOf (remove_casts_lval lval) } 108  Cil_types.Info (e, info) > 109 { e with Cil_types.enode = Cil_types.Info (remove_casts e, info) } 110  _ > e 111 112 and remove_casts_lval (lhost, offset) = 113 (remove_casts_lhost lhost, remove_casts_offset offset) 114 115 and remove_casts_lhost = function 116  Cil_types.Mem e > Cil_types.Mem (remove_casts e) 117  lhost > lhost 118 119 and remove_casts_offset = function 120  Cil_types.Field (fieldinfo, offset) > 121 Cil_types.Field (fieldinfo, remove_casts_offset offset) 122  Cil_types.Index (e, offset) > 123 Cil_types.Index (remove_casts e, remove_casts_offset offset) 124  offset > offset 125 126 let rec exp_is_var name e = match (remove_casts e).Cil_types.enode with 127  Cil_types.Lval (Cil_types.Var v, _) > v.Cil_types.vname = name 128  Cil_types.Info (e, _) > exp_is_var name e 129  _ > false 130 131 let has_fun_type varinfo = match varinfo.Cil_types.vtype with 132  Cil_types.TFun _ > true 133  _ > false 134 135 let formals_of_varinfo varinfo = match varinfo.Cil_types.vtype with 136  Cil_types.TFun (_, None, _, _) > [] 137  Cil_types.TFun (_, Some l, _, _) > 138 List.map (fun (x, t, _) > Cil.makeVarinfo false true x t) l 139  _ > assert false (* do not use on these arguments *) 232 140 233 141 let dummy_location = (Lexing.dummy_pos, Lexing.dummy_pos) 234 142 235 236 (*** Initializations ***) 237 238 (* Initializing the environment simply consists in visiting every function and 239 set their information in the environment. *) 240 241 class initializations cost_id env prj = object (self) 242 inherit Visitor.frama_c_copy prj as super 243 244 (* Update the variables whose address may be accessed. This is done by 245 visiting every expression of the program. *) 246 method vexpr e = 247 let _ = match e.Cil_types.enode with 248  Cil_types.AddrOf (Cil_types.Var var, _) > 249 let fun_name = current_fun_name self in 250 let addressed = get_addressed !env fun_name in 251 let addressed = 252 StringTools.Set.add var.Cil_types.vname addressed in 253 env := upd_addressed !env fun_name addressed 143 let dummy_varinfo = Cil.makeVarinfo false false "" (Cil_types.TVoid []) 144 145 let make_list n a = 146 let rec aux acc i = if i >= n then acc else aux (a :: acc) (i+1) in 147 aux [] 0 148 149 let rec stmt_subs stmt = 150 let added = match stmt.Cil_types.skind with 151  Cil_types.If (_, block1, block2, _) 152  Cil_types.TryFinally (block1, block2, _) 153  Cil_types.TryExcept (block1, _, block2, _) > 154 (block_subs block1) @ (block_subs block2) 155  Cil_types.Switch (_, block, _, _) 156  Cil_types.Loop (_, block, _, _, _) 157  Cil_types.Block block > block_subs block 158  Cil_types.UnspecifiedSequence l > 159 List.map (fun (stmt, _, _, _, _) > stmt) l 160  _ > [] in 161 stmt :: added 162 163 and block_subs block = List.flatten (List.map stmt_subs block.Cil_types.bstmts) 164 165 let rec first_stmt block = match block.Cil_types.bstmts with 166  [] > None 167  stmt :: _ > match stmt.Cil_types.skind with 168  Cil_types.Block block > first_stmt block 169  _ > Some stmt 170 171 let stmt_is_break stmt = match stmt.Cil_types.skind with 172  Cil_types.Break _ > true 173  _ > false 174 175 let starts_with_break block = match first_stmt block with 176  Some stmt > 177 (match stmt.Cil_types.skind with 178  Cil_types.Goto (stmt_ref, _) > stmt_is_break !stmt_ref 179  _ > stmt_is_break stmt) 180  _ > false 181 182 let rec last = function 183  [] > None 184  [e] > Some e 185  _ :: l > last l 186 187 let rec last_stmt block = match last block.Cil_types.bstmts with 188  None > None 189  Some stmt > match stmt.Cil_types.skind with 190  Cil_types. Block block > last_stmt block 191  _ > Some stmt 192 193 module IntSet = Misc.Int.Set 194 module IntMap = Misc.Int.Map 195 module IntCMap = Misc.Int.CMap 196 197 198 (*** Temporary variable name generator ***) 199 200 module GenName = struct 201 202 let prefix = ref "" 203 let index = ref 0 204 205 let set_prefix prf = prefix := prf 206 let reset () = index := 0 207 208 let concat suffix = !prefix ^ "_" ^ suffix 209 210 let fresh () = 211 let s = !prefix ^ (string_of_int !index) in 212 index := !index + 1 ; 213 s 214 215 let rec freshes n = if n = 0 then [] else (freshes (n1)) @ [fresh ()] 216 217 let fresh_varinfo fundec = 218 Cil.makeTempVar fundec ~name:(fresh ()) Cil.intType 219 220 let freshes_varinfo fundec n = 221 let vars = freshes n in 222 List.map (fun name > Cil.makeTempVar fundec ~name Cil.intType) vars 223 224 end 225 226 227 (*** Debug helpers ***) 228 229 let string_of_intset set = 230 IntSet.fold (fun i s > s ^ (string_of_int i) ^ " ") set "" 231 let string_of_intset_intmap map = 232 let f i set s = Printf.sprintf "%s%d: %s\n" s i (string_of_intset set) in 233 IntMap.fold f map "" 234 235 class print_CFG prj = object inherit Visitor.frama_c_copy prj as super 236 237 method vfunc func = 238 Format.printf "*** %s ***\n\n%!" func.Cil_types.svar.Cil_types.vname ; 239 List.iter 240 (fun stmt > 241 Format.printf "%d: %a\n> %!" stmt.Cil_types.sid Cil.d_stmt stmt ; 242 List.iter (fun stmt > Format.printf "%d %!" stmt.Cil_types.sid) 243 stmt.Cil_types.succs ; 244 Format.printf "\n\n%!") 245 func.Cil_types.sallstmts ; 246 Format.printf "\n\n%!" ; 247 Cil.SkipChildren 248 249 end 250 251 let print_CFG () = 252 let print_CFG_prj = 253 File.create_project_from_visitor "print_CFG" (new print_CFG) in 254 let f () = () in 255 Project.on print_CFG_prj f () 256 257 class loop_exit prj = object inherit Visitor.frama_c_copy prj as super 258 259 method vstmt_aux stmt = 260 let _ = match stmt.Cil_types.skind with 261  Cil_types.Loop (_, block, _, _, _) > 262 (match first_stmt block with 263  Some stmt > 264 (match stmt.Cil_types.skind with 265  Cil_types.If (_, _, block, _) > 266 (match first_stmt block with 267  Some stmt > 268 (match stmt.Cil_types.skind with 269  Cil_types.Break _ > 270 Format.printf "Loop exit: %!" ; 271 List.iter 272 (fun stmt > Format.printf "%d %!" stmt.Cil_types.sid) 273 stmt.Cil_types.succs ; 274 Format.printf "\n%!" 275  _ > Format.printf "If but no break\n%!") 276  _ > Format.printf "If but no child\n%!") 277  _ > Format.printf "Loop but no if\n%!") 278  _ > Format.printf "Loop but no child\n%!") 254 279  _ > () in 255 280 Cil.DoChildren 256 281 257 (* Update the variables whose address may be accessed. This is done by 258 visiting every statement of the program. *) 282 end 283 284 let loop_exit () = 285 let loop_exit_prj = 286 File.create_project_from_visitor "loop_exit" (new loop_exit) in 287 let f () = () in 288 Format.printf "\n%!" ; 289 Project.on loop_exit_prj f () 290 291 292 (*** Make CFG ***) 293 294 class make_CFG prj = object inherit Visitor.frama_c_copy prj as super 295 296 method vfile file = 297 Cfg.clearFileCFG file ; 298 Cfg.computeFileCFG file ; 299 Cil.SkipChildren 300 301 end 302 303 let make_CFG () = 304 let make_CFG_prj = 305 File.create_project_from_visitor "make_CFG" (new make_CFG) in 306 let f () = () in 307 Project.on make_CFG_prj f () 308 309 310 (*** Control points that are goto'ed to, control points of a loop. ***) 311 312 module PointsInfo = struct 313 314 type t = { gotoed : IntSet.t IntMap.t ; loop_points : IntSet.t IntMap.t } 315 316 let empty = { gotoed = IntMap.empty ; loop_points = IntMap.empty } 317 318 let gotoed points_info = points_info.gotoed 319 320 let loop_points points_info = points_info.loop_points 321 322 let mem_gotoed to_id points_info = IntMap.mem to_id (gotoed points_info) 323 324 let find_gotoed to_id points_info = IntMap.find to_id (gotoed points_info) 325 326 let add_gotoed to_id to_from_ids points_info = 327 let gotoed = IntMap.add to_id to_from_ids (gotoed points_info) in 328 { points_info with gotoed } 329 330 let mem_loop_points loop_id points_info = 331 IntMap.mem loop_id (loop_points points_info) 332 333 let find_loop_points loop_id points_info = 334 IntMap.find loop_id (loop_points points_info) 335 336 let add_loop_points loop_id ids points_info = 337 let loop_points = IntMap.add loop_id ids (loop_points points_info) in 338 { points_info with loop_points } 339 340 end 341 342 module PointsInfos = struct 343 344 type t = PointsInfo.t Misc.String.Map.t 345 346 let empty = Misc.String.Map.empty 347 348 let mem = Misc.String.Map.mem 349 350 let add = Misc.String.Map.add 351 352 let find = Misc.String.Map.find 353 354 let add_gotoed fun_name to_id to_from_ids points_infos = 355 let points_info = 356 if mem fun_name points_infos then find fun_name points_infos 357 else PointsInfo.empty in 358 let points_info = PointsInfo.add_gotoed to_id to_from_ids points_info in 359 add fun_name points_info points_infos 360 361 let add_loop_points fun_name loop_id ids points_infos = 362 let points_info = 363 if mem fun_name points_infos then find fun_name points_infos 364 else PointsInfo.empty in 365 let points_info = PointsInfo.add_loop_points loop_id ids points_info in 366 add fun_name points_info points_infos 367 368 end 369 370 class points_infos points_infos prj = 371 object inherit Visitor.frama_c_copy prj as super 372 373 val mutable current_fun_name = "" 374 259 375 method vstmt_aux stmt = 260 let fun_name = current_fun_name self in 376 (* because it is initialized in vfunc *) 377 assert (PointsInfos.mem current_fun_name !points_infos) ; 378 let points_info = PointsInfos.find current_fun_name !points_infos in 261 379 let _ = match stmt.Cil_types.skind with 262  Cil_types.Instr (Cil_types.Set ((Cil_types.Var var, _), _, _)) > 263 let modified = get_modified !env fun_name in 264 let modified = StringTools.Set.add var.Cil_types.vname modified in 265 env := upd_modified !env fun_name modified 266  Cil_types.Loop _ > env := add_nb_loops !env fun_name 380  Cil_types.Goto (stmt_ref, _) > 381 let from_id = stmt.Cil_types.sid in 382 let to_id = !stmt_ref.Cil_types.sid in 383 let to_from_ids = 384 if PointsInfo.mem_gotoed to_id points_info then 385 PointsInfo.find_gotoed to_id points_info 386 else IntSet.empty in 387 let to_from_ids = IntSet.add from_id to_from_ids in 388 points_infos := 389 PointsInfos.add_gotoed current_fun_name to_id to_from_ids 390 !points_infos 391  Cil_types.Loop (_, block, _, _, _) > 392 let loop_id = stmt.Cil_types.sid in 393 let ids = 394 if PointsInfo.mem_loop_points loop_id points_info then 395 PointsInfo.find_loop_points loop_id points_info 396 else IntSet.empty in 397 let ids = IntSet.add loop_id ids in 398 let f_stmts stmt = stmt :: (stmt_subs stmt) in 399 let stmts = List.flatten (List.map f_stmts block.Cil_types.bstmts) in 400 let f ids stmt = IntSet.add stmt.Cil_types.sid ids in 401 let ids = List.fold_left f ids stmts in 402 points_infos := 403 PointsInfos.add_loop_points current_fun_name loop_id ids !points_infos 267 404  _ > () in 268 405 Cil.DoChildren 269 406 270 (* When a function is found, create its entry in the environment, set its 271 parameters and its locals (the information is already accessible), and 272 leave empty the set of assigned and addressed variables. The two latters 273 will be updated when visiting the statements and the expressions. *) 407 method vfunc fundec = 408 current_fun_name < fundec.Cil_types.svar.Cil_types.vname ; 409 points_infos := 410 PointsInfos.add current_fun_name PointsInfo.empty !points_infos ; 411 Cil.DoChildren 412 413 end 414 415 let points_infos () = 416 let map = ref PointsInfos.empty in 417 let points_infos_prj = 418 File.create_project_from_visitor "points_infos" (new points_infos map) in 419 let f () = !map in 420 Project.on points_infos_prj f () 421 422 423 (*** Value (flat) domain extremes ***) 424 425 module BotAndTop = struct 426 427 type t = Bot  Top 428 429 let compare = Pervasives.compare 430 431 let to_string = function 432  Bot > "bot" 433  Top > "top" 434 435 let to_cil_term _ = assert false (* should not be used *) 436 437 let top = ArithSig.A Top 438 let bot = ArithSig.A Bot 439 440 let neg = function 441  Top > top 442  Bot > bot 443 444 let addl a v = match a, v with 445  Bot, _  _, ArithSig.A Bot > bot 446  Top, _ > top 447 448 let addr v a = addl a v 449 450 let minusl a v = match a, v with 451  Bot, _  _, ArithSig.A Bot > bot 452  Top, _ > top 453 454 let minusr v a = match v, a with 455  _, Bot  ArithSig.A Bot, _ > bot 456  _, Top > top 457 458 let mull a v = match a, v with 459  Bot, _  _, ArithSig.A Bot > bot 460  _, ArithSig.Int 0 > ArithSig.Int 0 461  Top, _ > top 462 463 let mulr v a = mull a v 464 465 let divl a v = match a, v with 466  Bot, _  _, ArithSig.A Bot  _, ArithSig.Int 0 > bot 467  Top, _ > top 468 469 let divr v a = match v, a with 470  _, Bot  ArithSig.A Bot, _ > bot 471  _, Top > top 472 473 let modl a v = match a, v with 474  Bot, _  _, ArithSig.A Bot  _, ArithSig.Int 0 > bot 475  Top, _ > top 476 477 let modr v a = match v, a with 478  _, Bot  ArithSig.A Bot, _ > bot 479  _, Top > top 480 481 let maxl a v = match a, v with 482  Bot, _  _, ArithSig.A Bot > bot 483  Top, _ > top 484 485 let maxr v a = maxl a v 486 487 let lel a v = match a, v with 488  Bot, _ > true 489  Top, ArithSig.A Top > true 490  Top, _ > false 491 492 let ler v a = match v, a with 493  _, Top > true 494  ArithSig.A Bot, Bot > true 495  _, Bot > false 496 497 let ltl a v = match a, v with 498  Bot, ArithSig.A Bot > false 499  Bot, _ > true 500  Top, _ > false 501 502 let ltr v a = match v, a with 503  ArithSig.A Top, Top > false 504  _, Top > true 505  _, Bot > false 506 507 let gel a v = ler v a 508 509 let ger v a = lel a v 510 511 let gtl a v = ltr v a 512 513 let gtr v a = ltl a v 514 515 let compute v = v 516 517 end 518 519 520 (*** Arithmetic expressions flat domain ***) 521 522 module ArithValDom = struct 523 524 include Arith.Make (BotAndTop) 525 526 let top = A BotAndTop.Top 527 528 let bot = A BotAndTop.Bot 529 530 let join v1 v2 = match v1, v2 with 531  A BotAndTop.Bot, v  v, A BotAndTop.Bot > v 532  _ when v1 = v2 > v1 533  _ > A BotAndTop.Top 534 535 let widen = join 536 537 let narrow v1 v2 = match v1, v2 with 538  A BotAndTop.Top, A _ > v1 539  A BotAndTop.Top, _ > v2 540  _ > v1 541 542 let f_is_concrete v subs_res = 543 let b = match v with 544  A _ > false 545  _ > true in 546 List.fold_left (&&) true (b :: subs_res) 547 548 let is_concrete v = fold f_is_concrete v 549 550 let add_list l = List.fold_left add (Int 0) l 551 552 let last_value rel _ exit_value increment = 553 let rel_added = of_int (if is_large rel then 0 else 1) in 554 let rel_op = if has_lower_type rel then minus else add in 555 add (rel_op exit_value rel_added) increment 556 557 (* 558 let last_value rel init_value exit_value increment = 559 let (op1, v1, v2, v3) = match rel with 560  Le > (minus, exit_value, init_value, increment) 561  Lt > (add, init_value, exit_value, of_int 0) 562  Ge > (add, init_value, exit_value, increment) 563  Gt > (minus, exit_value, init_value, of_int 0) in 564 let res = minus v1 v2 in 565 let res = modulo res (abs increment) in 566 let res = op1 exit_value res in 567 add res v3 568 *) 569 570 let iteration_nb init_value counter increment = 571 div (minus (of_var counter) init_value) increment 572 573 end 574 575 module Domain = ArithValDom 576 577 578 (*** Abstract cost ***) 579 580 module AbsCost = struct 581 582 include (Cost_value.Make (ArithValDom)) 583 584 end 585 586 587 (*** Requirements for loop termination ***) 588 589 module Require = struct 590 591 type t = 592 { relation : Domain.relation ; 593 init_value : Domain.t ; 594 exit_value : Domain.t ; 595 increment : Domain.t } 596 597 let compare = Pervasives.compare 598 599 let relation require = require.relation 600 let init_value require = require.init_value 601 let exit_value require = require.exit_value 602 let increment require = require.increment 603 604 let merge f require1 require2 = 605 (* each loop has a single condition relation *) 606 assert (relation require1 = relation require2) ; 607 { relation = relation require1 ; 608 init_value = f (init_value require1) (init_value require2) ; 609 exit_value = f (exit_value require1) (exit_value require2) ; 610 increment = f (increment require1) (increment require2) } 611 612 let join = merge Domain.join 613 let widen = merge Domain.widen 614 let narrow = merge Domain.narrow 615 616 let le require1 require2 = 617 (* each loop has a single condition relation *) 618 (relation require1 = relation require2) && 619 (Domain.le (init_value require1) (init_value require2)) && 620 (Domain.le (exit_value require1) (exit_value require2)) && 621 (Domain.le (increment require1) (increment require2)) 622 623 let make relation init_value exit_value increment = 624 { relation ; init_value ; exit_value ; increment } 625 626 let replace_vars replacements require = 627 let init_value = Domain.replace_vars replacements (init_value require) in 628 let exit_value = Domain.replace_vars replacements (exit_value require) in 629 let increment = Domain.replace_vars replacements (increment require) in 630 { require with init_value ; exit_value ; increment } 631 632 let to_string require = 633 Printf.sprintf "%s %s %s %s" 634 (Domain.string_of_relation (relation require)) 635 (Domain.to_string (init_value require)) 636 (Domain.to_string (exit_value require)) 637 (Domain.to_string (increment require)) 638 639 end 640 641 module Requires = struct 642 643 module M = Misc.Int.Map 644 645 type t = Require.t M.t 646 647 let empty = M.empty 648 649 let mem = M.mem 650 651 let find = M.find 652 653 let merge f = 654 let f_merge _ require1 require2 = match require1, require2 with 655  None, None > None 656  Some require, None  None, Some require > Some require 657  Some require1, Some require2 > Some (f require1 require2) in 658 M.merge f_merge 659 660 let join = merge Require.join 661 let widen = merge Require.widen 662 let narrow = merge Require.narrow 663 664 let le requires1 requires2 = 665 let f id require1 res = 666 res && (mem id requires2) && (Require.le require1 (find id requires2)) in 667 M.fold f requires1 true 668 669 let cardinal = M.cardinal 670 671 let fold f requires a = 672 let f' _ require a = f require a in 673 M.fold f' requires a 674 675 let add = M.add 676 677 let replace_vars replacements = M.map (Require.replace_vars replacements) 678 679 let to_string requires = 680 let f id require res = 681 Printf.sprintf "%s%d: %s\n%!" res id (Require.to_string require) in 682 M.fold f requires "" 683 684 end 685 686 687 (*** Point kind ***) 688 689 module LoopInfo = struct 690 691 type t = 692 { tmp_loop : Cil_types.varinfo ; 693 counter : string ; 694 relation : Domain.relation ; 695 exit_exp : Cil_types.exp ; 696 increment : Cil_types.exp ; 697 prev_stmts : (Cil_types.stmt * int (* position *)) list ; 698 last_stmts : Cil_types.stmt list } 699 700 let tmp_loop loop_info = loop_info.tmp_loop 701 702 let counter loop_info = loop_info.counter 703 704 let relation loop_info = loop_info.relation 705 706 let exit_exp loop_info = loop_info.exit_exp 707 708 let increment loop_info = loop_info.increment 709 710 let prev_stmts loop_info = loop_info.prev_stmts 711 712 let last_stmts loop_info = loop_info.last_stmts 713 714 let make tmp_loop counter relation exit_exp increment prev_stmts last_stmts = 715 { tmp_loop ; counter ; relation ; exit_exp ; increment ; 716 prev_stmts ; last_stmts } 717 718 719 end 720 721 module PointKind = struct 722 723 type t = 724  LoopStart of LoopInfo.t 725  LoopExit of LoopInfo.t 726  ULoopStart (* start of an unrecognized loop *) 727  ULoopExit (* exit of an unrecognized loop *) 728  RegularPoint 729 730 let is_recognized_loop_start = function 731  LoopStart _ > true 732  _ > false 733 734 let tmp_loop = function 735  LoopStart loop_info > LoopInfo.tmp_loop loop_info 736  _ > raise (Invalid_argument "PointKind.tmp_loop") 737 738 end 739 740 module PointKinds = struct 741 742 type t = PointKind.t IntMap.t 743 744 let empty = IntMap.empty 745 let add = IntMap.add 746 let mem = IntMap.mem 747 let find = IntMap.find 748 let fold = IntMap.fold 749 let dom point_kinds = List.map fst (IntMap.bindings point_kinds) 750 751 let mem_loop_start point point_kinds = 752 mem point point_kinds && 753 (PointKind.is_recognized_loop_start (find point point_kinds)) 754 755 let find_tmp_loop point point_kinds = 756 let error = Invalid_argument "PointKinds.find_tmp_loop" in 757 PointKind.tmp_loop (IntMap.error_find point point_kinds error) 758 759 end 760 761 762 (*** Fun infos ***) 763 764 module FunInfo = struct 765 766 type local_vars = (Cil_types.varinfo * string) list * Cil_types.varinfo list 767 768 type t = 769 { prototype : local_vars ; 770 (* exactly one start and one end points in FramaC's CFG *) 771 start_and_end_points : (int * int) option ; 772 nb_loops : int ; 773 point_kinds : PointKinds.t } 774 775 let empty = 776 { prototype = ([], []) ; start_and_end_points = None ; nb_loops = 0 ; 777 point_kinds = PointKinds.empty } 778 779 let make formals locals nb_loops start_and_end_points point_kinds = 780 { prototype = (formals, locals) ; 781 nb_loops ; start_and_end_points ; point_kinds } 782 783 let prototype fun_info = 784 List.map (fun (x, _) > x.Cil_types.vname) (fst fun_info.prototype) 785 786 let start_and_end_points fun_info = fun_info.start_and_end_points 787 788 let formals_and_locals fun_info = fun_info.prototype 789 790 let point_kinds fun_info = fun_info.point_kinds 791 792 let mem_point point fun_info = PointKinds.mem point fun_info.point_kinds 793 794 let find_point point fun_info = PointKinds.find point fun_info.point_kinds 795 796 let points fun_info = PointKinds.dom fun_info.point_kinds 797 798 let nb_loops fun_info = fun_info.nb_loops 799 800 let add_nb_loops fun_info = 801 let nb_loops = fun_info.nb_loops + 1 in 802 { fun_info with nb_loops } 803 804 let mem_loop_start point fun_info = 805 PointKinds.mem_loop_start point fun_info.point_kinds 806 807 let find_tmp_loop point fun_info = 808 PointKinds.find_tmp_loop point fun_info.point_kinds 809 810 end 811 812 module FunInfos = struct 813 814 type t = FunInfo.t Misc.String.Map.t 815 816 let empty = Misc.String.Map.empty 817 818 let prototypes = Misc.String.Map.map FunInfo.prototype 819 820 let mem = Misc.String.Map.mem 821 822 let add 823 fun_name formals locals nb_loops start_and_end_points point_kinds 824 fun_infos = 825 let fun_info = 826 FunInfo.make formals locals nb_loops start_and_end_points point_kinds in 827 Misc.String.Map.add fun_name fun_info fun_infos 828 829 let start_and_end_points fun_name fun_infos = 830 let error = Invalid_argument "FunInfos.start_and_end_points" in 831 let fun_info = Misc.String.Map.error_find fun_name fun_infos error in 832 FunInfo.start_and_end_points fun_info 833 834 let formals_and_locals fun_name fun_infos = 835 let error = Invalid_argument "FunInfos.formals_and_locals" in 836 let fun_info = Misc.String.Map.error_find fun_name fun_infos error in 837 FunInfo.formals_and_locals fun_info 838 839 let mem_point fun_name point fun_infos = 840 Misc.String.Map.mem fun_name fun_infos && 841 FunInfo.mem_point point (Misc.String.Map.find fun_name fun_infos) 842 843 let find_point fun_name point fun_infos = 844 FunInfo.find_point point (Misc.String.Map.find fun_name fun_infos) 845 846 let points fun_name fun_infos = 847 let error = Invalid_argument "FunInfos.points" in 848 FunInfo.points (Misc.String.Map.error_find fun_name fun_infos error) 849 850 let nb_loops fun_name fun_infos = 851 let error = Invalid_argument "FunInfos.nb_loops" in 852 FunInfo.nb_loops (Misc.String.Map.error_find fun_name fun_infos error) 853 854 let add_nb_loops fun_name fun_infos = 855 let error = Invalid_argument "FunInfos.add_nb_loops" in 856 let fun_info = Misc.String.Map.error_find fun_name fun_infos error in 857 let fun_info = FunInfo.add_nb_loops fun_info in 858 Misc.String.Map.add fun_name fun_info fun_infos 859 860 let mem_loop_start fun_name point fun_infos = 861 Misc.String.Map.mem fun_name fun_infos && 862 FunInfo.mem_loop_start point (Misc.String.Map.find fun_name fun_infos) 863 864 let find_tmp_loop fun_name point fun_infos = 865 let error = Invalid_argument "FunInfos.find_tmp_loop" in 866 let fun_info = Misc.String.Map.error_find fun_name fun_infos error in 867 FunInfo.find_tmp_loop point fun_info 868 869 let point_kinds fun_name fun_infos = 870 let error = Invalid_argument "FunInfos.point_kinds" in 871 let fun_info = Misc.String.Map.error_find fun_name fun_infos error in 872 FunInfo.point_kinds fun_info 873 874 end 875 876 877 (*** Static environment ***) 878 879 module StaticEnv = struct 880 881 type t = 882 { fname : string ; 883 f_old_name : string ; 884 cost_id : string ; 885 cost_incr : string ; 886 cost_varinfo : Cil_types.varinfo ; 887 fun_infos : FunInfos.t ; 888 globals : Misc.String.Set.t ; 889 extern_costs : string Misc.String.Map.t } 890 891 let init fname f_old_name cost_id cost_incr extern_costs = 892 { fname ; f_old_name ; cost_id ; cost_incr ; cost_varinfo = dummy_varinfo ; 893 fun_infos = FunInfos.empty ; 894 globals = Misc.String.Set.empty ; extern_costs } 895 896 let fname static_env = static_env.fname 897 898 let f_old_name static_env = static_env.f_old_name 899 900 let prototypes static_env = FunInfos.prototypes static_env.fun_infos 901 902 let add_fun_infos 903 fun_name formals locals nb_loops start_and_end_points point_kinds 904 static_env = 905 let fun_infos = 906 FunInfos.add fun_name formals locals nb_loops start_and_end_points 907 point_kinds static_env.fun_infos in 908 { static_env with fun_infos } 909 910 let globals static_env = static_env.globals 911 912 let add_globals x static_env = 913 let globals = Misc.String.Set.add x (globals static_env) in 914 { static_env with globals } 915 916 let formals_and_locals fun_name static_env = 917 FunInfos.formals_and_locals fun_name static_env.fun_infos 918 919 let locals fun_name static_env = snd (formals_and_locals fun_name static_env) 920 let formals fun_name static_env = fst (formals_and_locals fun_name static_env) 921 922 let is_local fun_name x static_env = 923 let f varinfo = varinfo.Cil_types.vname = x in 924 List.exists f (locals fun_name static_env) 925 926 let is_formal fun_name x static_env = 927 let (formals, locals) = formals_and_locals fun_name static_env in 928 let f_local varinfo = varinfo.Cil_types.vname <> x in 929 let f_formal (varinfo, _) = varinfo.Cil_types.vname = x in 930 (List.for_all f_local locals) && (List.exists f_formal formals) 931 932 let is_global fun_name x static_env = 933 let (formals, locals) = formals_and_locals fun_name static_env in 934 let f_local varinfo = varinfo.Cil_types.vname <> x in 935 let f_formal (varinfo, _) = varinfo.Cil_types.vname <> x in 936 (List.for_all f_local locals) && (List.for_all f_formal formals) && 937 (Misc.String.Set.mem x (globals static_env)) 938 939 let cost_id static_env = static_env.cost_id 940 941 let cost_varinfo static_env = static_env.cost_varinfo 942 943 let cost_incr static_env = static_env.cost_incr 944 945 let set_cost_varinfo cost_varinfo static_env = 946 { static_env with cost_varinfo } 947 948 let mem_point fun_name point static_env = 949 FunInfos.mem_point fun_name point static_env.fun_infos 950 951 let find_point fun_name point static_env = 952 FunInfos.find_point fun_name point static_env.fun_infos 953 954 let extern_costs static_env = static_env.extern_costs 955 956 let start_and_end_points fun_name static_env = 957 FunInfos.start_and_end_points fun_name static_env.fun_infos 958 959 let mem_fun_name fun_name static_env = 960 FunInfos.mem fun_name static_env.fun_infos 961 962 let points fun_name static_env = 963 FunInfos.points fun_name static_env.fun_infos 964 965 let nb_loops fun_name static_env = 966 FunInfos.nb_loops fun_name static_env.fun_infos 967 968 let add_nb_loops fun_name static_env = 969 let fun_infos = FunInfos.add_nb_loops fun_name static_env.fun_infos in 970 { static_env with fun_infos } 971 972 let mem_loop_start fun_name point static_env = 973 FunInfos.mem_loop_start fun_name point static_env.fun_infos 974 975 let find_tmp_loop fun_name point static_env = 976 FunInfos.find_tmp_loop fun_name point static_env.fun_infos 977 978 let point_kinds fun_name static_env = 979 FunInfos.point_kinds fun_name static_env.fun_infos 980 981 end 982 983 984 (*** Initializations ***) 985 986 let special_point f body = match f body with 987  None > None 988  Some stmt > Some stmt.Cil_types.sid 989 990 let start_point = special_point first_stmt 991 992 let end_point = special_point last_stmt 993 994 let make_start_and_end_points start_point end_point = 995 match start_point, end_point with 996  None, _  _, None > None 997  Some start_point, Some end_point > Some (start_point, end_point) 998 999 let make_tmp_names formals = 1000 let f varinfo = (varinfo, GenName.concat varinfo.Cil_types.vname) in 1001 List.map f formals 1002 1003 let rec extract_added_value counter e = match e.Cil_types.enode with 1004  Cil_types.BinOp (Cil_types.PlusA, e1, e2, _) when exp_is_var counter e1 > 1005 Some (counter, e2) 1006  Cil_types.BinOp (Cil_types.MinusA, e1, e2, typ) 1007 when exp_is_var counter e1 > 1008 let enode = Cil_types.UnOp (Cil_types.Neg, e2, typ) in 1009 let e2 = { e2 with Cil_types.enode = enode } in 1010 Some (counter, e2) 1011  Cil_types.CastE (_, e) > extract_added_value counter e 1012  _ > 1013 if !debug then 1014 Format.printf 1015 "Could not find added increment value for counter %s in %a.\n%!" 1016 counter Cil.d_exp e ; 1017 None 1018 1019 let extract_increment block = 1020 let open Misc.Option in 1021 last_stmt block >>= 1022 (fun stmt > match stmt.Cil_types.skind with 1023  Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) > 1024 extract_added_value v.Cil_types.vname e 1025  _ > 1026 if !debug then 1027 Format.printf 1028 "Could not find increment instruction; found %a instead.\n%!" 1029 Cil.d_stmt stmt ; 1030 None) 1031 1032 let extract_guard block (counter, increment) = 1033 let open Misc.Option in 1034 first_stmt block >>= 1035 (fun stmt > match stmt.Cil_types.skind with 1036  Cil_types.If (e, _, block, _) when starts_with_break block > 1037 (match e.Cil_types.enode with 1038  Cil_types.BinOp (rel, e1, e2, _) 1039 when exp_is_var counter e1 && Domain.is_supported_rel rel > 1040 Some (counter, Domain.rel_of_cil_binop rel, e2, increment) 1041  Cil_types.BinOp (rel, e1, e2, _) 1042 when exp_is_var counter e2 && Domain.is_supported_rel rel > 1043 let rel = Domain.rel_of_cil_binop rel in 1044 let rel = Domain.opposite rel in 1045 Some (counter, rel, e1, increment) 1046  _ > 1047 if !debug then 1048 Format.printf "Unsupported guard condition %a on counter %s.\n%!" 1049 Cil.d_exp e counter ; 1050 None) 1051  Cil_types.If (_, _, block, _) > 1052 if !debug then 1053 Format.printf "Loop not guarded by a break:\n%a\n%!" Cil.d_block block ; 1054 None 1055  _ > 1056 if !debug then Format.printf "Loop not guarded:\n%a\n%!" Cil.d_stmt stmt ; 1057 None) 1058 1059 let add_point_kinds 1060 start_id loop_start_info last_stmts loop_exit_info point_kinds = 1061 let point_kinds = PointKinds.add start_id loop_start_info point_kinds in 1062 let f_last_stmts point_kinds stmt = 1063 PointKinds.add stmt.Cil_types.sid loop_exit_info point_kinds in 1064 List.fold_left f_last_stmts point_kinds last_stmts 1065 1066 let add_loop_point_kinds id tmp_loop exps prev_stmts last_stmts point_kinds = 1067 match exps with 1068  None > 1069 let loop_start_info = PointKind.ULoopStart in 1070 let loop_exit_info = PointKind.ULoopExit in 1071 add_point_kinds id loop_start_info last_stmts loop_exit_info point_kinds 1072  Some (counter, relation, exit_exp, increment) > 1073 let loop_info = 1074 LoopInfo.make 1075 tmp_loop counter relation exit_exp increment prev_stmts last_stmts in 1076 let loop_start_info = PointKind.LoopStart loop_info in 1077 let loop_exit_info = PointKind.LoopExit loop_info in 1078 add_point_kinds id loop_start_info last_stmts loop_exit_info point_kinds 1079 1080 let loop_exits loop_points body = 1081 let f_exists stmt = not (IntSet.mem stmt.Cil_types.sid loop_points) in 1082 let f stmt = List.exists f_exists stmt.Cil_types.succs in 1083 List.filter f (block_subs body) 1084 1085 let stmt_point_kinds fundec points_info point_kinds stmt = 1086 let id = stmt.Cil_types.sid in 1087 match stmt.Cil_types.skind with 1088  Cil_types.Loop (_, body, _, _, _) > 1089 let open Misc.Option in 1090 assert (PointsInfo.mem_loop_points id points_info) ; 1091 let loop_points = PointsInfo.find_loop_points id points_info in 1092 let tmp_loop = GenName.fresh_varinfo fundec in 1093 let exps = extract_increment body >>= extract_guard body in 1094 let f_preds res pred = 1095 let pred_id = pred.Cil_types.sid in 1096 if IntSet.mem pred_id loop_points then res 1097 else 1098 let succs_id = 1099 List.map (fun stmt > stmt.Cil_types.sid) pred.Cil_types.succs in 1100 let opt_pos = Misc.List.pos id succs_id in 1101 (* otherwise pred would not be a predecessor of the loop *) 1102 assert (opt_pos <> None) ; 1103 (pred, Misc.Option.extract opt_pos) :: res in 1104 let prev_stmts = 1105 List.fold_left f_preds [] stmt.Cil_types.preds in 1106 let last_stmts = loop_exits loop_points body in 1107 let last_stmts = match last_stmt body with 1108  None > last_stmts 1109  Some last_stmt > last_stmt :: last_stmts in 1110 add_loop_point_kinds id tmp_loop exps prev_stmts last_stmts point_kinds 1111  _ when PointKinds.mem id point_kinds > point_kinds 1112  _ > PointKinds.add id PointKind.RegularPoint point_kinds 1113 1114 class initialize points_infos static_env prj = 1115 object inherit Visitor.frama_c_copy prj as super 1116 1117 method vglob_aux glob = 1118 let _ = match glob with 1119  Cil_types.GVarDecl (_, varinfo, _) when has_fun_type varinfo > 1120 GenName.reset () ; 1121 GenName.set_prefix "__tmp" ; 1122 let fun_name = varinfo.Cil_types.vname in 1123 let formals = formals_of_varinfo varinfo in 1124 let formals = make_tmp_names formals in 1125 let locals = [] in 1126 let nb_loops = 0 in 1127 let start_and_end_points = None in 1128 let point_kinds = PointKinds.empty in 1129 static_env := 1130 StaticEnv.add_fun_infos 1131 fun_name formals locals nb_loops start_and_end_points point_kinds 1132 !static_env 1133  Cil_types.GFun (fundec, _) > 1134 GenName.reset () ; 1135 GenName.set_prefix "__tmp" ; 1136 let fun_name = fundec.Cil_types.svar.Cil_types.vname in 1137 (* supposes a good initialization of [points_infos] *) 1138 assert (PointsInfos.mem fun_name points_infos) ; 1139 let points_info = PointsInfos.find fun_name points_infos in 1140 let formals = fundec.Cil_types.sformals in 1141 let formals = make_tmp_names formals in 1142 let locals = fundec.Cil_types.slocals in 1143 let nb_loops = 0 in 1144 let start_point = start_point fundec.Cil_types.sbody in 1145 let end_point = end_point fundec.Cil_types.sbody in 1146 let start_and_end_points = 1147 make_start_and_end_points start_point end_point in 1148 GenName.set_prefix "__tmp_loop" ; 1149 let point_kinds = 1150 List.fold_left (stmt_point_kinds fundec points_info) PointKinds.empty 1151 fundec.Cil_types.sallstmts in 1152 static_env := 1153 StaticEnv.add_fun_infos 1154 fun_name formals locals nb_loops start_and_end_points point_kinds 1155 !static_env 1156  Cil_types.GVar (varinfo, _, _) 1157 when varinfo.Cil_types.vname = StaticEnv.cost_id !static_env > 1158 static_env := StaticEnv.set_cost_varinfo varinfo !static_env ; 1159 static_env := StaticEnv.add_globals varinfo.Cil_types.vname !static_env 1160  Cil_types.GVar (varinfo, _, _)  Cil_types.GVarDecl (_, varinfo, _) > 1161 static_env := StaticEnv.add_globals varinfo.Cil_types.vname !static_env 1162  _ > () in 1163 Cil.DoChildren 1164 1165 end 1166 1167 let initialize tmp_prefix fname f_old_name cost_id cost_incr extern_costs = 1168 let points_infos = points_infos () in 1169 GenName.set_prefix tmp_prefix ; 1170 let static_env_ref = 1171 ref (StaticEnv.init fname f_old_name cost_id cost_incr extern_costs) in 1172 let initialize_prj = 1173 File.create_project_from_visitor "initialize" 1174 (new initialize points_infos static_env_ref) in 1175 let f () = !static_env_ref in 1176 Project.on initialize_prj f () 1177 1178 1179 (*** Abstract domains and environments ***) 1180 1181 module type DOMAIN = sig 1182 type t 1183 val of_int : int > t 1184 val of_var : string > t 1185 val top : t 1186 val bot : t 1187 val join : t > t > t 1188 val widen : t > t > t 1189 val narrow : t > t > t 1190 val le : t > t > bool 1191 val to_string : t > string 1192 val neg : t > t 1193 val add : t > t > t 1194 val minus : t > t > t 1195 val mul : t > t > t 1196 val div : t > t > t 1197 val modulo : t > t > t 1198 end 1199 1200 module type VARABSENV = sig 1201 module Domain : DOMAIN 1202 type t 1203 val bot : t 1204 val top : t 1205 val upd : string > Domain.t > t > t 1206 val find : string > t > Domain.t 1207 val init : Misc.String.Set.t > (string * string) list > t 1208 val join : t > t > t 1209 val widen : t > t > t 1210 val narrow : t > t > t 1211 val le : t > t > bool 1212 val to_string : t > string 1213 end 1214 1215 module type ABSENV = sig 1216 module VarAbsEnv : VARABSENV 1217 module Domain : DOMAIN 1218 type t 1219 type addressed = Misc.String.Set.t 1220 val cost : t > AbsCost.t 1221 val requires : t > Requires.t 1222 val set_cost : t > AbsCost.t > t 1223 val add_cost : t > AbsCost.t > t 1224 val add_addressed : t > addressed > t 1225 val set_lval : t > Cil_types.lval > Domain.t > t 1226 val top_vars : t > Misc.String.Set.t > t 1227 val find : string > t > Domain.t 1228 val bot : t 1229 val init : Misc.String.Set.t > (string * string) list > t 1230 val join : t > t > t 1231 val widen : t > t > t 1232 val narrow : t > t > t 1233 val le : t > t > bool 1234 val add_require : t > int > Require.t > t 1235 val to_string : t > string 1236 end 1237 1238 module MakeVarAbsEnv (D : DOMAIN) : VARABSENV with module Domain = D = struct 1239 1240 module Domain = D 1241 1242 type t = Domain.t Misc.String.CMap.t 1243 1244 let bot = Misc.String.CMap.empty D.bot 1245 let upd = Misc.String.CMap.upd 1246 let find = Misc.String.CMap.find 1247 1248 let init globals formals = 1249 let f x env = Misc.String.CMap.upd x D.top env in 1250 let env = Misc.String.Set.fold f globals bot in 1251 let f env (x, tmp) = 1252 let env = Misc.String.CMap.upd x (D.of_var tmp) env in 1253 Misc.String.CMap.upd tmp (D.of_var tmp) env in 1254 List.fold_left f env formals 1255 1256 let join = Misc.String.CMap.merge D.join 1257 let widen = Misc.String.CMap.merge D.widen 1258 let narrow = Misc.String.CMap.merge D.narrow 1259 1260 let top = Misc.String.CMap.empty D.top 1261 1262 let le env1 env2 = 1263 let f v1 v2 res = res && (Domain.le v1 v2) in 1264 Misc.String.CMap.cmp f env1 env2 true 1265 1266 let to_string = 1267 Misc.String.CMap.to_string (fun x > x) (fun v > (D.to_string v) ^ "\n") 1268 1269 end 1270 1271 module MakeAbsEnv (VAE : VARABSENV) 1272 : ABSENV with module VarAbsEnv = VAE 1273 and module Domain = VAE.Domain = struct 1274 1275 module VarAbsEnv = VAE 1276 module Domain = VarAbsEnv.Domain 1277 1278 type addressed = Misc.String.Set.t 1279 1280 type t = 1281 { cost : AbsCost.t ; var_abs_env : VarAbsEnv.t ; addressed : addressed ; 1282 requires : Requires.t } 1283 1284 let init globals formals = 1285 let cost = AbsCost.bot in 1286 let var_abs_env = VarAbsEnv.init globals formals in 1287 let addressed = Misc.String.Set.empty in 1288 let requires = Requires.empty in 1289 { cost ; var_abs_env ; addressed ; requires } 1290 1291 let cost env = env.cost 1292 1293 let requires env = env.requires 1294 1295 let var_abs_env env = env.var_abs_env 1296 1297 let find x env = VarAbsEnv.find x (var_abs_env env) 1298 1299 let set_cost env cost = { env with cost } 1300 1301 let add_cost env cost = { env with cost = AbsCost.add env.cost cost } 1302 1303 let addressed env = env.addressed 1304 1305 let add_addressed env addressed = 1306 { env with addressed = Misc.String.Set.union env.addressed addressed } 1307 1308 let set_lval env lval v = match fst lval with 1309  Cil_types.Var x > 1310 let var_abs_env = VarAbsEnv.upd x.Cil_types.vname v env.var_abs_env in 1311 { env with var_abs_env } 1312  _ > env 1313 1314 let top_vars env vars = 1315 let f x var_abs_env = VarAbsEnv.upd x Domain.top var_abs_env in 1316 let var_abs_env = Misc.String.Set.fold f vars env.var_abs_env in 1317 { env with var_abs_env } 1318 1319 let bot = 1320 { cost = AbsCost.bot ; var_abs_env = VarAbsEnv.bot ; 1321 addressed = Misc.String.Set.empty ; requires = Requires.empty } 1322 1323 let join env1 env2 = 1324 { cost = AbsCost.join (cost env1) (cost env2) ; 1325 var_abs_env = VarAbsEnv.join (var_abs_env env1) (var_abs_env env2) ; 1326 addressed = Misc.String.Set.union (addressed env1) (addressed env2) ; 1327 requires = Requires.join (requires env1) (requires env2) } 1328 1329 let widen env1 env2 = 1330 { cost = AbsCost.widen (cost env1) (cost env2) ; 1331 var_abs_env = VarAbsEnv.widen (var_abs_env env1) (var_abs_env env2) ; 1332 addressed = Misc.String.Set.union (addressed env1) (addressed env2) ; 1333 requires = Requires.widen (requires env1) (requires env2) } 1334 1335 let narrow env1 env2 = 1336 { cost = AbsCost.narrow (cost env1) (cost env2) ; 1337 var_abs_env = VarAbsEnv.narrow (var_abs_env env1) (var_abs_env env2) ; 1338 addressed = addressed env1 ; 1339 requires = Requires.narrow (requires env1) (requires env2) } 1340 1341 let le env1 env2 = 1342 (AbsCost.le (cost env1) (cost env2)) && 1343 (VarAbsEnv.le (var_abs_env env1) (var_abs_env env2)) && 1344 (Misc.String.Set.is_subset (addressed env1) (addressed env2)) && 1345 (Requires.le (requires env1) (requires env2)) 1346 1347 let add_require env id require = 1348 { env with requires = Requires.add id require (requires env) } 1349 1350 let to_string env = 1351 let f_addressed x res = res ^ x ^ " " in 1352 "Cost: " ^ (AbsCost.to_string (cost env)) ^ "\n" ^ 1353 "Var env:\n" ^ (VarAbsEnv.to_string (var_abs_env env)) ^ 1354 "Addressed: " ^ (Misc.String.Set.fold f_addressed (addressed env) "") ^ 1355 "\n" ^ 1356 "Requires:\n" ^ (Requires.to_string (requires env)) ^ "\n" 1357 1358 end 1359 1360 module MakePointsAbsEnv (AE : ABSENV) = struct 1361 1362 module AbsEnv = AE 1363 module Domain = AbsEnv.Domain 1364 1365 type t = 1366 { abs_env : AbsEnv.t IntCMap.t } 1367 1368 let empty = { abs_env = IntCMap.empty AbsEnv.bot } 1369 let bot = empty 1370 1371 let abs_env env = env.abs_env 1372 1373 let find point env = IntCMap.find point env.abs_env 1374 1375 let add point abs_env env = 1376 let abs_env = IntCMap.upd point abs_env env.abs_env in 1377 { abs_env } 1378 1379 let le env1 env2 = 1380 let cmp abs_env1 abs_env2 res = res && (AbsEnv.le abs_env1 abs_env2) in 1381 IntCMap.cmp cmp (abs_env env1) (abs_env env2) true 1382 1383 let cost point env = AbsEnv.cost (find point env) 1384 1385 let requires point env = AbsEnv.requires (find point env) 1386 1387 let init start_point globals formals = 1388 add start_point (AbsEnv.init globals formals) empty 1389 1390 let to_string env = 1391 IntCMap.to_string string_of_int AbsEnv.to_string (abs_env env) 1392 1393 let widen env1 env2 = 1394 let abs_env = IntCMap.merge AbsEnv.widen (abs_env env1) (abs_env env2) in 1395 { abs_env } 1396 1397 let narrow env1 env2 = 1398 let abs_env = IntCMap.merge AbsEnv.narrow (abs_env env1) (abs_env env2) in 1399 { abs_env } 1400 1401 let set_cost id cost env = add id (AbsEnv.set_cost (find id env) cost) env 1402 1403 end 1404 1405 1406 module PointsAbsEnv = struct 1407 1408 module D = Domain 1409 1410 module VAE = MakeVarAbsEnv (D) 1411 1412 module AE = MakeAbsEnv (VAE) 1413 1414 include MakePointsAbsEnv (AE) 1415 1416 end 1417 1418 module AbsEnv = PointsAbsEnv.AbsEnv 1419 1420 1421 (*** Dependent cost results ***) 1422 1423 module LoopAnnotInfo = struct 1424 1425 type t = 1426 { counter : string ; 1427 relation : Domain.relation ; 1428 init_value : Domain.t ; 1429 exit_value : Domain.t ; 1430 increment : Domain.t ; 1431 last_value : Domain.t ; 1432 cost_id : string ; 1433 tmp_loop : string ; 1434 iteration_nb : Domain.t ; 1435 body_cost : AbsCost.t } 1436 1437 let counter loop_annot_info = loop_annot_info.counter 1438 1439 let relation loop_annot_info = loop_annot_info.relation 1440 1441 let init_value loop_annot_info = loop_annot_info.init_value 1442 1443 let exit_value loop_annot_info = loop_annot_info.exit_value 1444 1445 let increment loop_annot_info = loop_annot_info.increment 1446 1447 let last_value loop_annot_info = loop_annot_info.last_value 1448 1449 let cost_id loop_annot_info = loop_annot_info.cost_id 1450 1451 let tmp_loop loop_annot_info = loop_annot_info.tmp_loop 1452 1453 let iteration_nb loop_annot_info = loop_annot_info.iteration_nb 1454 1455 let body_cost loop_annot_info = loop_annot_info.body_cost 1456 1457 let make 1458 counter relation init_value exit_value increment last_value cost_id 1459 tmp_loop iteration_nb body_cost = 1460 { counter ; relation ; init_value ; exit_value ; increment ; last_value ; 1461 cost_id ; tmp_loop ; iteration_nb ; body_cost } 1462 1463 end 1464 1465 module LoopAnnot = struct 1466 1467 type t = 1468  Variant of Domain.t 1469  CounterMod of Domain.t * Domain.t 1470  CounterLastValue of 1471 string * Domain.relation * Domain.t * Domain.t * Domain.t 1472  NoIteration of string * Domain.relation * Domain.t * Domain.t 1473  Cost of string * string * Domain.t * AbsCost.t 1474 1475 let reduce prototypes costs = function 1476  Cost (cost_id, tmp_loop, iteration_nb, body_cost) > 1477 let body_cost = AbsCost.reduce prototypes costs body_cost in 1478 Cost (cost_id, tmp_loop, iteration_nb, body_cost) 1479  v > v 1480 1481 let compare = Pervasives.compare 1482 1483 let variant_to_cil v = 1484 if Domain.is_concrete v then Some (mk_variant (Domain.to_cil_term v)) 1485 else None 1486 1487 let counter_mod_to_cil v1 v2 = 1488 if Domain.is_concrete v1 && Domain.is_concrete v2 then 1489 if v1 = v2 then None 1490 else 1491 let v1 = Domain.to_cil_term v1 in 1492 let v2 = Domain.to_cil_term v2 in 1493 let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in 1494 Some (mk_invariant invariant) 1495 else None 1496 1497 let counter_last_value_to_cil counter rel init_value exit_value last_value = 1498 if Domain.is_concrete init_value && 1499 Domain.is_concrete exit_value && 1500 Domain.is_concrete last_value then 1501 let init_value = Domain.to_cil_term init_value in 1502 let exit_value = Domain.to_cil_term exit_value in 1503 let last_value = Domain.to_cil_term last_value in 1504 let rel' = Domain.cil_rel_of_rel rel in 1505 let require = Logic_const.prel (rel', init_value, exit_value) in 1506 let rel' = Domain.cil_rel_of_rel (Domain.mk_large rel) in 1507 let counter = cil_logic_int_var counter in 1508 let prop = Logic_const.prel (rel', counter, last_value) in 1509 let invariant = Logic_const.pimplies (require, prop) in 1510 Some (mk_invariant invariant) 1511 else None 1512 1513 let no_iteration_to_cil counter rel init_value exit_value = 1514 if Domain.is_concrete init_value && Domain.is_concrete exit_value then 1515 let rel = Domain.opposite rel in 1516 let rel' = Domain.cil_rel_of_rel rel in 1517 let init_value = Domain.to_cil_term init_value in 1518 let exit_value = Domain.to_cil_term exit_value in 1519 let require = Logic_const.prel (rel', init_value, exit_value) in 1520 let counter = cil_logic_int_var counter in 1521 let prop = Logic_const.prel (Cil_types.Req, counter, init_value) in 1522 let invariant = Logic_const.pimplies (require, prop) in 1523 Some (mk_invariant invariant) 1524 else None 1525 1526 let cost_to_cil cost_id tmp_loop iteration_nb body_cost = 1527 if Domain.is_concrete iteration_nb && AbsCost.is_concrete body_cost then 1528 let cost_var = cil_logic_int_var cost_id in 1529 let body_cost = AbsCost.to_ext body_cost in 1530 let loop_cost = Domain.mul iteration_nb body_cost in 1531 let cost = Domain.add (Domain.of_var tmp_loop) loop_cost in 1532 if Domain.is_concrete cost then 1533 let cost = Domain.to_cil_term cost in 1534 let invariant = Logic_const.prel (Cil_types.Rle, cost_var, cost) in 1535 Some (mk_invariant invariant) 1536 else None 1537 else None 1538 1539 let to_cil = function 1540  Variant v > variant_to_cil v 1541  CounterMod (v1, v2) > counter_mod_to_cil v1 v2 1542  CounterLastValue(counter, rel, init_value, exit_value, last_value) > 1543 counter_last_value_to_cil counter rel init_value exit_value last_value 1544  NoIteration (counter, rel, init_value, exit_value) > 1545 no_iteration_to_cil counter rel init_value exit_value 1546  Cost (cost_id, tmp_loop, iteration_nb, body_cost) > 1547 cost_to_cil cost_id tmp_loop iteration_nb body_cost 1548 1549 let make_variant loop_annot_info = 1550 let rel = LoopAnnotInfo.relation loop_annot_info in 1551 let counter = LoopAnnotInfo.counter loop_annot_info in 1552 let last_value = LoopAnnotInfo.last_value loop_annot_info in 1553 let counter_var = Domain.of_var counter in 1554 let (v1, v2) = match rel with 1555  Domain.Lt  Domain.Le > (last_value, counter_var) 1556  Domain.Gt  Domain.Ge > (counter_var, last_value) in 1557 Variant (Domain.minus v1 v2) 1558 1559 let make_counter_mod loop_annot_info = 1560 let counter = LoopAnnotInfo.counter loop_annot_info in 1561 let init_value = LoopAnnotInfo.init_value loop_annot_info in 1562 let increment = LoopAnnotInfo.increment loop_annot_info in 1563 let mk_value value = Domain.modulo value (Domain.abs increment) in 1564 let v1 = mk_value (Domain.of_var counter) in 1565 let v2 = mk_value init_value in 1566 CounterMod (v1, v2) 1567 1568 let make_counter_last_value loop_annot_info = 1569 let counter = LoopAnnotInfo.counter loop_annot_info in 1570 let rel = LoopAnnotInfo.relation loop_annot_info in 1571 let init_value = LoopAnnotInfo.init_value loop_annot_info in 1572 let exit_value = LoopAnnotInfo.exit_value loop_annot_info in 1573 let last_value = LoopAnnotInfo.last_value loop_annot_info in 1574 CounterLastValue (counter, rel, init_value, exit_value, last_value) 1575 1576 let make_no_iteration loop_annot_info = 1577 let counter = LoopAnnotInfo.counter loop_annot_info in 1578 let rel = LoopAnnotInfo.relation loop_annot_info in 1579 let init_value = LoopAnnotInfo.init_value loop_annot_info in 1580 let exit_value = LoopAnnotInfo.exit_value loop_annot_info in 1581 NoIteration (counter, rel, init_value, exit_value) 1582 1583 let make_cost loop_annot_info = 1584 let cost_id = LoopAnnotInfo.cost_id loop_annot_info in 1585 let tmp_loop = LoopAnnotInfo.tmp_loop loop_annot_info in 1586 let iteration_nb = LoopAnnotInfo.iteration_nb loop_annot_info in 1587 let body_cost = LoopAnnotInfo.body_cost loop_annot_info in 1588 Cost (cost_id, tmp_loop, iteration_nb, body_cost) 1589 1590 end 1591 1592 module LoopAnnots = struct 1593 1594 include Eset.Make (LoopAnnot) 1595 1596 let make loop_annot_info = 1597 let variant = LoopAnnot.make_variant loop_annot_info in 1598 (* let counter_mod = LoopAnnot.make_counter_mod loop_annot_info in *) 1599 let counter_last_value = 1600 LoopAnnot.make_counter_last_value loop_annot_info in 1601 let no_iteration = LoopAnnot.make_no_iteration loop_annot_info in 1602 let cost = LoopAnnot.make_cost loop_annot_info in 1603 of_list [variant ; (* counter_mod ; *) 1604 counter_last_value ; no_iteration ; cost] 1605 1606 let to_cil loop_annots = 1607 let f loop_annot res = match LoopAnnot.to_cil loop_annot with 1608  Some loop_annot > loop_annot :: res 1609  None > res in 1610 fold f loop_annots [] 1611 1612 let reduce prototypes costs loop_annots = 1613 let f loop_annot res = 1614 add (LoopAnnot.reduce prototypes costs loop_annot) res in 1615 fold f loop_annots empty 1616 1617 end 1618 1619 module LoopsAnnots = struct 1620 1621 type t = LoopAnnots.t IntMap.t 1622 1623 let empty = IntMap.empty 1624 1625 let mem = IntMap.mem 1626 1627 let find = IntMap.find 1628 1629 let add = IntMap.add 1630 1631 let to_cil loops_annots = 1632 IntMap.map LoopAnnots.to_cil loops_annots 1633 1634 let reduce prototypes costs loops_annots = 1635 IntMap.map (LoopAnnots.reduce prototypes costs) loops_annots 1636 1637 end 1638 1639 module CostInfo = struct 1640 1641 type t = { cost : AbsCost.t ; requires : Requires.t ; 1642 loops_annots : LoopsAnnots.t } 1643 1644 let cost cost_info = cost_info.cost 1645 1646 let requires cost_info = cost_info.requires 1647 1648 let make cost requires loops_annots = { cost ; requires ; loops_annots } 1649 1650 let set_cost cost_info cost = { cost_info with cost } 1651 1652 let init cost = 1653 { cost ; requires = Requires.empty ; loops_annots = LoopsAnnots.empty } 1654 1655 let loops_annots cost = cost.loops_annots 1656 1657 let mem_loop_annots id cost = LoopsAnnots.mem id (loops_annots cost) 1658 1659 let find_loop_annots id cost = LoopsAnnots.find id (loops_annots cost) 1660 1661 let to_string cost_info = AbsCost.to_string (cost cost_info) 1662 1663 let reduce_loops_annots prototypes costs cost_info = 1664 let loops_annots = 1665 LoopsAnnots.reduce prototypes costs cost_info.loops_annots in 1666 { cost_info with loops_annots } 1667 1668 let replace_vars replacements cost_info = 1669 let cost = AbsCost.replace_vars replacements (cost cost_info) in 1670 let requires = Requires.replace_vars replacements (requires cost_info) in 1671 { cost_info with cost ; requires } 1672 1673 end 1674 1675 module Costs = struct 1676 1677 type t = CostInfo.t Misc.String.Map.t 1678 1679 let empty = Misc.String.Map.empty 1680 1681 let init extern_costs = 1682 let f fun_name cost costs = 1683 let cost_info = CostInfo.init (AbsCost.of_extern cost) in 1684 Misc.String.Map.add fun_name cost_info costs in 1685 Misc.String.Map.fold f extern_costs empty 1686 1687 let mem = Misc.String.Map.mem 1688 1689 let add fun_name cost requires loops_annots costs = 1690 Misc.String.Map.add fun_name 1691 (CostInfo.make cost requires loops_annots) costs 1692 1693 let find_cost fun_name costs = 1694 CostInfo.cost (Misc.String.Map.find fun_name costs) 1695 1696 let find_requires fun_name costs = 1697 CostInfo.requires (Misc.String.Map.find fun_name costs) 1698 1699 let fun_costs = Misc.String.Map.map CostInfo.cost 1700 1701 let set_fun_costs costs fun_costs = 1702 let f fun_name cost_info = 1703 let cost = 1704 if Misc.String.Map.mem fun_name fun_costs then 1705 Misc.String.Map.find fun_name fun_costs 1706 else CostInfo.cost cost_info in 1707 CostInfo.set_cost cost_info cost in 1708 Misc.String.Map.mapi f costs 1709 1710 let fold = Misc.String.Map.fold 1711 1712 let to_string costs = 1713 let f fun_name cost_info res = 1714 res ^ "\n" ^ fun_name ^ ": " ^ (CostInfo.to_string cost_info) in 1715 fold f costs "" 1716 1717 let mem_loop_point fun_name id costs = 1718 (Misc.String.Map.mem fun_name costs) && 1719 (CostInfo.mem_loop_annots id (Misc.String.Map.find fun_name costs)) 1720 1721 let find_loop_annots fun_name id costs = 1722 let error = Invalid_argument "Costs.find_loop_annotations" in 1723 let fun_info = Misc.String.Map.error_find fun_name costs error in 1724 CostInfo.find_loop_annots id fun_info 1725 1726 let reduce_loops_annots prototypes costs = 1727 let fun_costs = fun_costs costs in 1728 Misc.String.Map.map 1729 (CostInfo.reduce_loops_annots prototypes fun_costs) costs 1730 1731 let restore_formals static_env costs = 1732 let f fun_name cost_info = 1733 if StaticEnv.mem_fun_name fun_name static_env then 1734 let formals = StaticEnv.formals fun_name static_env in 1735 let f (formal, tmp) = (tmp, Domain.of_var formal.Cil_types.vname) in 1736 let replacements = Misc.String.Map.of_list (List.map f formals) in 1737 CostInfo.replace_vars replacements cost_info 1738 else cost_info in 1739 Misc.String.Map.mapi f costs 1740 1741 end 1742 1743 1744 (*** Abstract interpretation ***) 1745 1746 module MakeAI (M : sig val static_env : StaticEnv.t end) = struct 1747 1748 let rec addressed e = match e.Cil_types.enode with 1749  Cil_types.Const _  Cil_types.SizeOf _  Cil_types.SizeOfStr _ 1750  Cil_types.AlignOf _ > 1751 Misc.String.Set.empty 1752  Cil_types.Lval lval  Cil_types.AddrOf lval  Cil_types.StartOf lval > 1753 lval_addressed lval 1754  Cil_types.SizeOfE e  Cil_types.AlignOfE e  Cil_types.UnOp (_, e, _) 1755  Cil_types.CastE (_, e)  Cil_types.Info (e, _) > addressed e 1756  Cil_types.BinOp (_, e1, e2, _) > 1757 Misc.String.Set.union (addressed e1) (addressed e2) 1758 1759 and lhost_addressed = function 1760  Cil_types.Var _ > Misc.String.Set.empty 1761  Cil_types.Mem e > addressed e 1762 1763 and offset_addressed = function 1764  Cil_types.Index (e, offset) > 1765 Misc.String.Set.union (addressed e) (offset_addressed offset) 1766  _ > Misc.String.Set.empty 1767 1768 and lval_addressed (lhost, offset) = 1769 Misc.String.Set.union (lhost_addressed lhost) (offset_addressed offset) 1770 1771 let branch abs_env _ = [abs_env ; abs_env] 1772 1773 let abs_fun_of_unop = function 1774  Cil_types.Neg > Domain.neg 1775  _ > (fun _ > Domain.top) 1776 1777 let abs_fun_of_binop = function 1778  Cil_types.PlusA > Domain.add 1779  Cil_types.MinusA > Domain.minus 1780  Cil_types.Mult > Domain.mul 1781  Cil_types.Div > Domain.div 1782  Cil_types.Mod > Domain.modulo 1783  _ > (fun _ _ > Domain.top) 1784 1785 let rec exp abs_env e = match e.Cil_types.enode with 1786  Cil_types.Const (Cil_types.CInt64 (i, _, _)) > 1787 Domain.of_int (Int64.to_int i) 1788  Cil_types.Lval (Cil_types.Var varinfo, _) > 1789 AbsEnv.find varinfo.Cil_types.vname abs_env 1790  Cil_types.Info (e, _) > exp abs_env e 1791  Cil_types.UnOp (unop, e, _) > 1792 abs_fun_of_unop unop (exp abs_env e) 1793  Cil_types.BinOp (binop, e1, e2, _) > 1794 abs_fun_of_binop binop (exp abs_env e1) (exp abs_env e2) 1795  Cil_types.CastE (_, e) > exp abs_env e (* TODO: maybe incorrect *) 1796  _ > Domain.top 1797 1798 let cost_incr_cost = function 1799  e :: _ > 1800 (match e.Cil_types.enode with 1801  Cil_types.Const (Cil_types.CInt64 (i, _, _)) > 1802 AbsCost.of_int (Int64.to_int i) 1803  _ > AbsCost.top) 1804  _ > AbsCost.top 1805 1806 let call_proc_cost fun_name abs_env sid f args = 1807 let f_add_addrd addrd e = Misc.String.Set.union addrd (addressed e) in 1808 let addrd = List.fold_left f_add_addrd Misc.String.Set.empty (f :: args) in 1809 let abs_env = AbsEnv.add_addressed abs_env addrd in 1810 let cost = match f.Cil_types.enode with 1811  Cil_types.Lval (Cil_types.Var var, _) 1812 when var.Cil_types.vname = StaticEnv.cost_incr M.static_env > 1813 cost_incr_cost args 1814  Cil_types.Lval (Cil_types.Var var, _) > 1815 AbsCost.of_fun_call 1816 fun_name sid var.Cil_types.vname (List.map (exp abs_env) args) 1817  _ > AbsCost.top in 1818 let vars_to_top = 1819 Misc.String.Set.union (StaticEnv.globals M.static_env) addrd in 1820 AbsEnv.add_cost (AbsEnv.top_vars abs_env vars_to_top) cost 1821 1822 let stmt fun_name abs_env stmt = match stmt.Cil_types.skind with 1823  Cil_types.Return _ > [] 1824  Cil_types.Goto _  Cil_types.Break _  Cil_types.Continue _ 1825  Cil_types.Loop _  Cil_types.Block _  Cil_types.Switch _ 1826  Cil_types.Instr (Cil_types.Skip _  Cil_types.Code_annot _) > [abs_env] 1827  Cil_types.UnspecifiedSequence l > make_list (List.length l) abs_env 1828  Cil_types.If (e, _, _, _) > branch abs_env e 1829  Cil_types.Instr (Cil_types.Set (lval, e, _)) > 1830 let addressed = 1831 Misc.String.Set.union (lval_addressed lval) (addressed e) in 1832 let v = exp abs_env e in 1833 let abs_env = AbsEnv.add_addressed abs_env addressed in 1834 [AbsEnv.set_lval abs_env lval v] 1835  Cil_types.Instr (Cil_types.Call (None, f, args, _)) > 1836 [call_proc_cost fun_name abs_env stmt.Cil_types.sid f args] 1837  Cil_types.Instr (Cil_types.Call (Some lval, f, args, _)) > 1838 let addressed = lval_addressed lval in 1839 let abs_env = AbsEnv.add_addressed abs_env addressed in 1840 let abs_env = call_proc_cost fun_name abs_env stmt.Cil_types.sid f args in 1841 [AbsEnv.set_lval abs_env lval Domain.top] 1842  Cil_types.Instr (Cil_types.Asm _) > raise ASM_unsupported 1843  Cil_types.TryFinally _  Cil_types.TryExcept _ > raise Try_unsupported 1844 1845 let merge_succ_regular points_abs_env abs_env stmt = 1846 let id = stmt.Cil_types.sid in 1847 let abs_env' = PointsAbsEnv.find id points_abs_env in 1848 let abs_env' = AbsEnv.join abs_env abs_env' in 1849 PointsAbsEnv.add id abs_env' points_abs_env 1850 1851 let merge_succ_uloop_start src_id points_abs_env abs_env = 1852 let points_abs_env = 1853 PointsAbsEnv.set_cost src_id AbsCost.top points_abs_env in 1854 let abs_env = AbsEnv.set_cost abs_env (AbsCost.of_int 0) in 1855 merge_succ_regular points_abs_env abs_env 1856 1857 let prev_init_and_cost fun_name counter points_abs_env prev_stmts = 1858 let f (init_value, before_cost) (stmt_, pos) = 1859 let abs_env = PointsAbsEnv.find (stmt_.Cil_types.sid) points_abs_env in 1860 let abs_env = List.nth (stmt fun_name abs_env stmt_) pos in 1861 let init_value = Domain.join init_value (AbsEnv.find counter abs_env) in 1862 let before_cost = AbsCost.join before_cost (AbsEnv.cost abs_env) in 1863 (init_value, before_cost) in 1864 List.fold_left f (Domain.bot, AbsCost.bot) prev_stmts 1865 1866 let body_cost points_abs_env last_stmts = 1867 (* Exiting of a loop can only be done through a break or a goto or whatever, 1868 but certainly not with a cost increment instruction. Thus executing the 1869 last statements of a loop should not change the cost information, so its 1870 unnecessary when this is all we care about. *) 1871 let f res stmt = 1872 let id = stmt.Cil_types.sid in 1873 AbsCost.join res (AbsEnv.cost (PointsAbsEnv.find id points_abs_env)) in 1874 List.fold_left f AbsCost.bot last_stmts 1875 1876 let loop_cost fun_name id loop_info points_abs_env abs_env = 1877 let cost_id = StaticEnv.cost_id M.static_env in 1878 let tmp_loop = LoopInfo.tmp_loop loop_info in 1879 let counter = LoopInfo.counter loop_info in 1880 let relation = LoopInfo.relation loop_info in 1881 let prev_stmts = LoopInfo.prev_stmts loop_info in 1882 let last_stmts = LoopInfo.last_stmts loop_info in 1883 let (init_value, before_cost) = 1884 prev_init_and_cost fun_name counter points_abs_env prev_stmts in 1885 let exit_value = exp abs_env (LoopInfo.exit_exp loop_info) in 1886 let increment = exp abs_env (LoopInfo.increment loop_info) in 1887 let last_value = 1888 Domain.last_value relation init_value exit_value increment in 1889 let iteration_nb = Domain.iteration_nb init_value counter increment in 1890 let body_cost = body_cost points_abs_env last_stmts in 1891 let loop_cost = 1892 if AbsCost.is_top body_cost then AbsCost.top 1893 else 1894 AbsCost.of_loop_cost 1895 fun_name id relation init_value exit_value increment 1896 (AbsCost.extract body_cost) in 1897 let succ_loop_cost = AbsCost.add before_cost loop_cost in 1898 (counter, relation, init_value, exit_value, increment, last_value, cost_id, 1899 tmp_loop, iteration_nb, body_cost, succ_loop_cost) 1900 1901 let merge_succ_loop_start 1902 fun_name src_id loop_info points_abs_env points_abs_env' abs_env = 1903 let src_abs_env = PointsAbsEnv.find src_id points_abs_env in 1904 let (_, rel, init_value, exit_value, increment, _, _, _, _, _, _) = 1905 loop_cost fun_name src_id loop_info points_abs_env src_abs_env in 1906 let require = Require.make rel init_value exit_value increment in 1907 let abs_env = AbsEnv.add_require abs_env src_id require in 1908 merge_succ_uloop_start src_id points_abs_env' abs_env 1909 1910 let merge_succ_loop_exit 1911 fun_name loop_start_id loop_info points_abs_env points_abs_env' 1912 abs_env stmt = 1913 let start_abs_env = PointsAbsEnv.find loop_start_id points_abs_env in 1914 let (_, _, _, _, _, _, _, _, _, _, succ_loop_cost) = 1915 loop_cost fun_name loop_start_id loop_info points_abs_env start_abs_env 1916 in 1917 let abs_env = AbsEnv.set_cost abs_env succ_loop_cost in 1918 merge_succ_regular points_abs_env' abs_env stmt 1919 1920 let merge_succ_uloop_exit points_abs_env abs_env = 1921 let abs_env = AbsEnv.set_cost abs_env AbsCost.top in 1922 merge_succ_regular points_abs_env abs_env 1923 1924 let merge_succ fun_name src_id points_abs_env = 1925 if StaticEnv.mem_point fun_name src_id M.static_env then 1926 match StaticEnv.find_point fun_name src_id M.static_env with 1927  PointKind.RegularPoint > merge_succ_regular 1928  PointKind.LoopStart loop_info > 1929 merge_succ_loop_start fun_name src_id loop_info points_abs_env 1930  PointKind.LoopExit loop_info > 1931 merge_succ_loop_exit fun_name src_id loop_info points_abs_env 1932  PointKind.ULoopStart > merge_succ_uloop_start src_id 1933  PointKind.ULoopExit > merge_succ_uloop_exit 1934 else raise (Invalid_argument "AI.merge_succ") 1935 1936 let fundec_stmt fun_name points_abs_env points_abs_env' stmt_ = 1937 let id = stmt_.Cil_types.sid in 1938 let abs_env = PointsAbsEnv.find id points_abs_env in 1939 let abs_envs = stmt fun_name abs_env stmt_ in 1940 (* Otherwise the [stmt] function is not correct. *) 1941 assert (List.length abs_envs = List.length stmt_.Cil_types.succs) ; 1942 let f = merge_succ fun_name id points_abs_env in 1943 List.fold_left2 f points_abs_env' abs_envs stmt_.Cil_types.succs 1944 1945 let rec fundec_stmts fun_name points_abs_env cmp merge stmts = 1946 if !debug then 1947 Printf.printf "%s\n%!" (PointsAbsEnv.to_string points_abs_env) ; 1948 let f = fundec_stmt fun_name points_abs_env in 1949 let points_abs_env' = List.fold_left f PointsAbsEnv.bot stmts in 1950 let points_abs_env' = merge points_abs_env points_abs_env' in 1951 if cmp points_abs_env' points_abs_env then 1952 (if !debug then 1953 Printf.printf "%s\n%!" (PointsAbsEnv.to_string points_abs_env') ; 1954 points_abs_env') 1955 else fundec_stmts fun_name points_abs_env' cmp merge stmts 1956 1957 let fundec_stmts_widen fun_name points_abs_env = 1958 fundec_stmts fun_name points_abs_env PointsAbsEnv.le PointsAbsEnv.widen 1959 1960 let fundec_stmts_narrow fun_name points_abs_env = 1961 let cmp env1 env2 = PointsAbsEnv.le env2 env1 in 1962 fundec_stmts fun_name points_abs_env cmp PointsAbsEnv.narrow 1963 1964 let loop_annot_info fun_name id points_abs_env loop_info = 1965 let abs_env = PointsAbsEnv.find id points_abs_env in 1966 let (counter, relation, init_value, exit_value, last_value, increment, 1967 cost_id, tmp_loop, iteration_nb, body_cost, _) = 1968 loop_cost fun_name id loop_info points_abs_env abs_env in 1969 LoopAnnotInfo.make 1970 counter relation init_value exit_value last_value increment cost_id 1971 tmp_loop.Cil_types.vname iteration_nb body_cost 1972 1973 let loop_annots fun_name points_abs_env id point_kind loops_annots = 1974 match point_kind with 1975  PointKind.LoopStart loop_info > 1976 let loop_annot_info = 1977 loop_annot_info fun_name id points_abs_env loop_info in 1978 let loop_annots = LoopAnnots.make loop_annot_info in 1979 LoopsAnnots.add id loop_annots loops_annots 1980  PointKind.ULoopStart > 1981 let loop_annots = LoopAnnots.empty in 1982 LoopsAnnots.add id loop_annots loops_annots 1983  _ > loops_annots 1984 1985 let loops_annots fun_name points_abs_env = 1986 PointKinds.fold (loop_annots fun_name points_abs_env) 1987 (StaticEnv.point_kinds fun_name M.static_env) LoopsAnnots.empty 1988 1989 end 1990 1991 1992 (*** Dependent costs computation ***) 1993 1994 class compute_costs widen narrow loops_annots static_env costs prj = 1995 object inherit Visitor.frama_c_copy prj as super 1996 274 1997 method vfunc fundec = 275 1998 let fun_name = fundec.Cil_types.svar.Cil_types.vname in 276 let addressed = StringTools.Set.empty in 277 let varinfo_to_string x = x.Cil_types.vname in 278 let parameters = List.map varinfo_to_string fundec.Cil_types.sformals in 279 let f_locals res x = StringTools.Set.add (varinfo_to_string x) res in 280 let locals = 281 List.fold_left f_locals StringTools.Set.empty fundec.Cil_types.slocals in 282 let modified = StringTools.Set.empty in 283 let nb_loops = 0 in 284 let fun_info = 285 mk_fun_info addressed parameters locals modified nb_loops in 286 let fun_infos = 287 StringTools.Map.add fun_name fun_info (get_fun_infos !env) in 288 env := upd_fun_infos !env fun_infos ; 289 Cil.DoChildren 290 291 (* Update the varinfo of the cost variable. *) 292 method vglob_aux glob = 293 let _ = match glob with 294  Cil_types.GVarDecl (_, varinfo, _) 295  Cil_types.GVar (varinfo, _, _) when varinfo.Cil_types.vname = cost_id > 296 env := upd_cost_varinfo !env varinfo 297  _ > () in 298 Cil.DoChildren 299 300 end 301 302 (** [initializations cost_id] consider the current file in the current project 303 and returns a corresponding initialized environment .*) 304 305 let initializations cost_id : env = 306 let env : env ref = ref init_env in 307 let initializations_prj = 1999 if fun_name = StaticEnv.cost_incr static_env then begin 2000 costs := Costs.add fun_name AbsCost.top Requires.empty 2001 LoopsAnnots.empty !costs ; 2002 Cil.SkipChildren end 2003 else begin 2004 (* The function should be in the static environment because of the 2005 initializations. *) 2006 assert (StaticEnv.mem_fun_name fun_name static_env) ; 2007 let _ = match StaticEnv.start_and_end_points fun_name static_env with 2008  None > 2009 costs := Costs.add fun_name AbsCost.top Requires.empty 2010 LoopsAnnots.empty !costs 2011  Some (start_point, end_point) > 2012 if !debug then Printf.printf "Interpreting %s\n%!" fun_name ; 2013 let formals = StaticEnv.formals fun_name static_env in 2014 let f_formals (varinfo, tmp) = (varinfo.Cil_types.vname, tmp) in 2015 let globals = StaticEnv.globals static_env in 2016 let formals = List.map f_formals formals in 2017 let env = PointsAbsEnv.init start_point globals formals in 2018 if !debug then Printf.printf "WIDEN\n%!" ; 2019 let env = widen fun_name env fundec.Cil_types.sallstmts in 2020 if !debug then Printf.printf "NARROW\n%!" ; 2021 let env = narrow fun_name env fundec.Cil_types.sallstmts in 2022 let cost = PointsAbsEnv.cost end_point env in 2023 let requires = PointsAbsEnv.requires end_point env in 2024 let loops_annots = loops_annots fun_name env in 2025 (* The last instruction should be a return. Executing it shouldn't 2026 change the environment. *) 2027 costs := Costs.add fun_name cost requires loops_annots !costs in 2028 Cil.SkipChildren end 2029 2030 end 2031 2032 let compute_costs static_env = 2033 let module AI = MakeAI (struct let static_env = static_env end) in 2034 let costs = ref (Costs.init (StaticEnv.extern_costs static_env)) in 2035 let compute_costs_prj = 308 2036 File.create_project_from_visitor 309 "cerco_initializations" (new initializations cost_id env) in 310 let f () = !env in 311 Project.on initializations_prj f () 312 313 314 (* Test if a block has a loop. Used to test the presence of nested 315 loops. Indeed, they not supported for now, until a bug in Jessie is fixed. *) 316 317 let rec has_loop_stmt stmt = match stmt.Cil_types.skind with 318  Cil_types.Instr _  Cil_types.Return _  Cil_types.Goto _ 319  Cil_types.Break _  Cil_types.Continue _ > false 320  Cil_types.If (_, block1, block2, _) 321  Cil_types.TryFinally (block1, block2, _) 322  Cil_types.TryExcept (block1, _, block2, _) > 323 (has_loop block1)  (has_loop block2) 324  Cil_types.Switch (_, block, _, _) 325  Cil_types.Block block > has_loop block 326  Cil_types.Loop _ > true 327  Cil_types.UnspecifiedSequence l > 328 has_loop_stmt_list (List.map (fun (stmt, _, _, _, _) > stmt) l) 329 330 and has_loop_stmt_list stmt_list = 331 let f res stmt = res  (has_loop_stmt stmt) in 332 List.fold_left f false stmt_list 333 334 (** [has_loop block] returns true iff the block of instructions [block] contains 335 a loop. *) 336 337 and has_loop block = has_loop_stmt_list block.Cil_types.bstmts 338 339 340 (*** Statement and block cost ***) 341 342 (* Requirement for loop termination. They have the form: 343 (guard relation, initialization value, exit value, increment) *) 344 345 type require = Cost_value.relation * Cost_value.t * Cost_value.t * Cost_value.t 346 347 (** [const_incr_cost e] extracts the integer constant that the expression [e] 348 represents. *) 349 350 let cost_incr_cost = function 351  e :: _ > 352 (match e.Cil_types.enode with 353  Cil_types.Const (Cil_types.CInt64 (i, _, _)) > 354 Cost_value.Int (Int64.to_int i) 355  _ > raise Cost_incr_arg_not_constant) 356  _ > raise Cost_incr_arg_not_constant 357 358 (** [call cost cost_incr f args] returns the cost of calling the function [f] on 359 arguments [args]. If the function is the cost update function [cost_incr], 360 then its cost is the value of its argument, which needs to be a constant 361 integer. Otherwise, it is simply the cost of executing [f] on its 362 arguments. *) 363 364 let call_cost cost_incr f args = match f.Cil_types.enode with 365  Cil_types.Lval (Cil_types.Var var, _) 366 when var.Cil_types.vname = cost_incr > 367 cost_incr_cost args 368  Cil_types.Lval (Cil_types.Var var, _) > 369 (try 370 let args = List.map Cost_value.of_cil_exp args in 371 Cost_value.CostOf (var.Cil_types.vname, args) 372 with Cost_value.Unsupported_exp > raise Unsupported_exp) 373  _ > raise Unresolvable_function 374 375 (** [instr_cost cost_incr instr] returns the cost of executing the simple 376 instruction [instr]. Only function calls do have a cost. *) 377 378 let instr_cost cost_incr = function 379  Cil_types.Call (_, f, args, _) > 380 call_cost cost_incr f args 381  _ > Cost_value.Int 0 382 383 (* FramaC sometimes transforms the control flow graph of a function by 384 factorizing a return instructions through added gotos. We handle this special 385 case of gotos with the function below, but other forms are not supported. *) 386 387 let goto_cost stmt = match stmt.Cil_types.skind with 388  Cil_types.Return _ > ([], Cost_value.Int 0) 389  _ > raise (Unsupported "goto") 390 391 (* In FramaC, every C loop construct is transformed into an infinite loop with 392 a break inside a conditional to exit. Initialization of a for loop are 393 located in the very previous instruction. The guard can either be at the 394 beginning of the loop in the cases of for and while loops, or at the end in 395 the case of a dowhile loop. Finally, the increment instruction is located at 396 the end in the case of a for loop. *) 397 398 (** [extract_counter_and_init stmt_opt] supposes that the optional statement 399 [stmt_opt] is in fact an assignment instruction. In this case, it returns 400 the assigned variable and the expression to assign, otherwise it raises an 401 error. It will be used to extract the loop counter and its first value in 402 the case of a loop initialization instruction. *) 403 404 let extract_counter_and_init stmt_opt = 405 let error () = raise (Unsupported_loop "no initialization found") in 406 match stmt_opt with 407  None > error () 408  Some stmt > match stmt.Cil_types.skind with 409  Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) > 410 (v.Cil_types.vname, Cost_value.of_cil_exp e) 411  _ > error () 412 413 (** [first_stmt block] returns the first statement of the block [block], if 414 any. *) 415 416 let first_stmt block = match block.Cil_types.bstmts with 417  [] > raise (Unsupported_loop "no guard") 418  instr :: _ > instr 419 420 (** [exp_is_var name e] returns true iff the expression [e] is in fact the 421 variable of name [name]. *) 422 423 let exp_is_var name e = match e.Cil_types.enode with 424  Cil_types.Lval (Cil_types.Var v, _) > v.Cil_types.vname = name 425  _ > false 426 427 (** [starts_with_break block] returns true iff the block [block] starts with a 428 break instruction. *) 429 430 let starts_with_break block = match (first_stmt block).Cil_types.skind with 431  Cil_types.Break _ > true 432  _ > false 433 434 (** [extract_guard counter block] supposes that the first statement of the block 435 [block] is a conditional with an exit instruction. It then supposes that the 436 conditional is a test on the variable [counter]. It returns the comparison 437 relation along with the expression that the counter is compared to. It will 438 be used to extract the guard condition of a loop. *) 439 440 let extract_guard counter block = match (first_stmt block).Cil_types.skind with 441  Cil_types.If (e, _, block, _) when starts_with_break block > 442 (match e.Cil_types.enode with 443  Cil_types.BinOp (rel, e1, e2, _) when exp_is_var counter e1 > 444 (Cost_value.rel_of_cil_rel rel, Cost_value.of_cil_exp e2) 445  _ > raise (Unsupported_loop "unsupported guard expression")) 446  _ > raise (Unsupported_loop "no guard found") 447 448 (** [last l] returns the last element of the list [l], if any. *) 449 450 let rec last = function 451  [] > raise (Failure "Compute.last") 452  [e] > e 453  _ :: l > last l 454 455 (** [last_stmt block] returns the last statement of the block [block], if 456 any. *) 457 458 let last_stmt block = match block.Cil_types.bstmts with 459  [] > raise (Unsupported_loop "no increment instruction") 460  stmts > last stmts 461 462 (** [extract_added_value counter e] supposes that the expression [e] is either 463 an addition or a substraction of the variable [counter]. It returns the 464 added value: exactly the value in case of an addition, and its opposite in 465 case of a substraction. It will be used to extract the increment of the 466 counter in a loop. *) 467 468 let extract_added_value counter e = match e.Cil_types.enode with 469  Cil_types.BinOp (Cil_types.PlusA, e1, e2, _) when exp_is_var counter e1 > 470 Cost_value.of_cil_exp e2 471  Cil_types.BinOp (Cil_types.MinusA, e1, e2, _) when exp_is_var counter e1 > 472 Cost_value.UnOp (Cost_value.Neg, Cost_value.of_cil_exp e2) 473  _ > raise (Unsupported_loop "unsupported increment expression") 474 475 (** [extract_increment counter block] supposes that the block [block] ends with 476 an increment of the variable [counter]. It returns the increment. It will be 477 used to extract the increment in a loop body. *) 478 479 let extract_increment counter block = 480 match (last_stmt block).Cil_types.skind with 481  Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) 482 when v.Cil_types.vname = counter > 483 extract_added_value counter e 484  _ > raise (Unsupported_loop "no increment instruction found") 485 486 let check b error = if not b then raise (Unsupported_loop error) 487 488 (** [counter_preserved_until_last counter block] returns true iff the variable 489 [counter] is not assigned in the block [block], except potentially at the 490 very last instruction. This is a support condition for loops. *) 491 492 let counter_preserved_until_last counter block = 493 let stmt_preserves stmt = match stmt.Cil_types.skind with 494  Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), _, _)) > 495 v.Cil_types.vname <> counter 496  _ > true in 497 let rec aux = function 498  []  [_] > true 499  stmt :: block > (stmt_preserves stmt) && (aux block) in 500 aux block.Cil_types.bstmts 501 502 (** [check supported_loop fun_name env counter init_value exit_value increment 503 block] raises an exception if the loop body [block] of the function 504 [fun_name] is not supported in the environment [env] and with regards to the 505 loop counter [counter], its initialization expression [init_value] and its 506 exit expression [exit_value]. We check that: the address of the loop counter 507 is not accessed in the whole function, the loop counter is not assigned in 508 the body (except at the end), the variables in the initialization and exit 509 expressions are parameters and their address is not accessed nor are they 510 assigned in the whole function. *) 511 512 let check_supported_loop 513 fun_name env counter init_value exit_value increment block = 514 let fun_info = get_fun_info env fun_name in 515 let addressed = fun_info.addressed in 516 let parameters = StringTools.Set.of_list fun_info.parameters in 517 let modified = fun_info.modified in 518 let init_value_vars = Cost_value.vars init_value in 519 let exit_value_vars = Cost_value.vars exit_value in 520 let increment_vars = Cost_value.vars increment in 521 let vars = StringTools.Set.union init_value_vars exit_value_vars in 522 let vars = StringTools.Set.union vars increment_vars in 523 let addressed_or_modified = StringTools.Set.union addressed modified in 524 check (not (StringTools.Set.mem counter addressed)) 525 "loop counter's address is accessed" ; 526 check (counter_preserved_until_last counter block) 527 "loop counter is modified inside loop body" ; 528 check (StringTools.Set.subset vars parameters) 529 "local or global inside a loop expression" ; 530 check (StringTools.Set.disjoint vars addressed_or_modified) 531 "the value of a parameter in a loop expression may be modified" 532 533 (** [mk_loop_cost init_value increment body_cost] returns a function that, when 534 providing a current value of the loop counter, returns the current cost of a 535 loop of first value [init_value], of increment [increment] and whose body 536 cost is [body_cost]. This function will be used with the loop counter for an 537 invariant of the loop, and with the final value of the counter for a total 538 cost of the loop. *) 539 540 let mk_loop_cost init_value increment body_cost = 541 fun i > 542 let v = Cost_value.BinOp (Cost_value.Sub, i, init_value) in 543 let v = Cost_value.BinOp (Cost_value.Div, v, increment) in 544 Cost_value.BinOp (Cost_value.Mul, v, body_cost) 545 546 (** [last_value rel init_value exit_value increment] returns the last value 547 taken by the counter of a loop when the first value is [init_value], the 548 comparison relation in the guard is [rel], the compared value is 549 [exit_value] and the increment is [increment]. *) 550 551 let last_value rel init_value exit_value increment = 552 let (op1, v1, v2, v3) = match rel with 553  Cost_value.Le > (Cost_value.Sub, exit_value, init_value, increment) 554  Cost_value.Lt > 555 (Cost_value.Add, init_value, exit_value, Cost_value.Int 0) 556  Cost_value.Ge > (Cost_value.Add, init_value, exit_value, increment) 557  Cost_value.Gt > 558 (Cost_value.Sub, exit_value, init_value, Cost_value.Int 0) in 559 let res = Cost_value.BinOp (Cost_value.Sub, v1, v2) in 560 let incr_mod = Cost_value.abs increment in 561 let res = Cost_value.BinOp (Cost_value.Mod, res, incr_mod) in 562 let res = Cost_value.BinOp (op1, exit_value, res) in 563 Cost_value.BinOp (Cost_value.Add, res, v3) 564 565 (** [stmt_cost fun_name cost_incr env previous_stmt stmt] returns the 566 requirements and the cost of the statement [stmt] of the function [fun_name] 567 in the environment [env] when [cost_incr] is the name of the cost update 568 function and [previous_stmt] is the (optional) previous statement. *) 569 570 let rec stmt_cost fun_name cost_incr env previous_stmt stmt 571 : require list * Cost_value.t = 572 let block_cost block = block_cost fun_name cost_incr env block in 573 574 let rec aux stmt = match stmt.Cil_types.skind with 575 576  Cil_types.Instr instr > ([], instr_cost cost_incr instr) 577 578  Cil_types.Goto (stmt_ref, _) > goto_cost !stmt_ref 579 580  Cil_types.If (_, block1, block2, _) > 581 let (requires1, cost1) = block_cost block1 in 582 let (requires2, cost2) = block_cost block2 in 583 (requires1 @ requires2, Cost_value.BinOp (Cost_value.Max, cost1, cost2)) 584 585  Cil_types.Loop (_, block, _, _, _) > 586 (* if has_loop block then raise Nested_loops 587 else *) loop_cost fun_name cost_incr env previous_stmt block 588 589  Cil_types.Block block > block_cost block 590 591  Cil_types.Return _  Cil_types.Break _  Cil_types.Continue _ > 592 ([], Cost_value.Int 0) 593 594  Cil_types.Switch _ > raise (Unsupported "switch") 595 596  Cil_types.UnspecifiedSequence _ > 597 raise (Unsupported "unspecified sequence") 598 599  Cil_types.TryFinally _ > raise (Unsupported "try finally") 600 601  Cil_types.TryExcept _ > raise (Unsupported "try except") in 602 603 aux stmt 604 605 (** [block_cost fun_name cost_incr env block] returns the requirements and the 606 cost of the block [block] of the function [fun_name] in the environment 607 [env] when [cost_incr] is the name of the cost update function. *) 608 609 and block_cost fun_name cost_incr env block : require list * Cost_value.t = 610 let f (previous_stmt, requires, cost) stmt = 611 let (added_requires, added_cost) = 612 stmt_cost fun_name cost_incr env previous_stmt stmt in 613 (Some stmt, 614 requires @ added_requires, 615 Cost_value.BinOp (Cost_value.Add, cost, added_cost)) in 616 let (_, requires, cost) = 617 List.fold_left f (None, [], Cost_value.Int 0) block.Cil_types.bstmts in 618 (requires, cost) 619 620 (** [loop_infos fun_name cost_incr env previous_stmt block] returns all the 621 extracted cost information of a loop in function [fun_name], in environment 622 [env], with [cost_incr] for the name of the cost update function, with 623 (optional) previous statement [previous_stmt] and of body [block]. The 624 returned information are: the requirements for the loop termination, the 625 loop counter, its first value, the comparison relation of the guard, the 626 compared value in the guard, the increment and a function that, provided a 627 current value for the loop counter, returns the current cost of the loop. *) 628 629 and loop_infos fun_name cost_incr env previous_stmt block 630 : require list * string * Cost_value.t * Cost_value.relation * 631 Cost_value.t * Cost_value.t * (Cost_value.t > Cost_value.t) = 632 let (counter, init_value) = extract_counter_and_init previous_stmt in 633 let (rel, exit_value) = extract_guard counter block in 634 let increment = extract_increment counter block in 635 check_supported_loop 636 fun_name env counter init_value exit_value increment block ; 637 let (requires, body_cost) = block_cost fun_name cost_incr env block in 638 let requires = [(rel, init_value, exit_value, increment)] @ requires in 639 let cost = mk_loop_cost init_value increment body_cost in 640 (requires, counter, init_value, rel, exit_value, increment, cost) 641 642 (** [loop_cost fun_name cost_incr env previous_stmt block] returns the 643 requirements and the cost of the loop of body [block] in the function 644 [fun_name] in the environment [env] when [cost_incr] is the name of the cost 645 update function and [previous_stmt] is the (optional) previous statement. *) 646 647 and loop_cost fun_name cost_incr env previous_stmt block 648 : require list * Cost_value.t = 649 let (requires, _, init_value, rel, exit_value, increment, cost) = 650 loop_infos fun_name cost_incr env previous_stmt block in 651 let cost = cost (last_value rel init_value exit_value increment) in 652 let cost = 653 Cost_value.Cond (init_value, rel, exit_value, cost, Cost_value.Int 0) in 654 (requires, cost) 655 656 657 (*** Costs computation ***) 658 659 (* Once a cost (that may depend on the cost of the other functions) has been 660 associated to each function of a program, we want to simplify them in order 661 to have independent costs. To this end, we simply apply a fixpoint where at 662 each step, the independent cost of a function is replaced in the cost of 663 whatever function mentions it. For exampe, in the following configuration: 664 cost of f(x) <= x*x + 3 665 cost of g() <= cost of h() 666 cost of h(y) <= 1 + cost of f(y) 667 then a step of the fixpoint will lead to: 668 cost of f(x) <= x*x + 3 669 cost of g() <= cost of h() 670 cost of h(y) <= 1 + y*y + 3 *) 671 672 (** [is_solved costs] returns true iff the system of inequations formed by the 673 costs [costs] is solved, i.e. if every cost is independent of the others and 674 does not mention to special cost value [Any]. *) 675 676 let is_solved costs = 677 let f _ cost res = 678 res && (Cost_value.is_independent cost) && 679 (not (Cost_value.has_any cost)) in 680 StringTools.Map.fold f costs true 681 682 (** [solve_end costs1 costs2] returns true iff a fixpoint has been reached, 683 i.e. if the costs [costs2] of the current iteration are the same as the 684 costs [costs1] of the previous iteration. *) 2037 "compute_costs" 2038 (new compute_costs AI.fundec_stmts_widen AI.fundec_stmts_narrow 2039 AI.loops_annots static_env costs) in 2040 let f () = !costs in 2041 Project.on compute_costs_prj f () 2042 2043 2044 (*** Costs solver ***) 685 2045 686 2046 let solve_end costs1 costs2 = 687 2047 let f fun_name cost res = 688 res && (StringTools.Map.mem fun_name costs1) && 689 (cost = StringTools.Map.find fun_name costs1) in 690 StringTools.Map.fold f costs2 true 691 692 (** [solve_costs extern_costs prototypes costs] solves the system of inequations 693 formed by the costs [costs]. It applies a reduction operation until a 694 fixpoint is reached. *) 695 696 let rec solve_costs extern_costs prototypes costs = 697 let costs' = Cost_value.reduces extern_costs costs prototypes costs in 698 if solve_end costs costs' then 699 if is_solved costs' then costs' 700 else raise Unresolvable 701 else solve_costs extern_costs prototypes costs' 702 703 class compute_costs cost_incr env costs prj = object 704 inherit Visitor.frama_c_copy prj as super 705 706 method vfunc fundec = 707 let fun_name = fundec.Cil_types.svar.Cil_types.vname in 708 let block = fundec.Cil_types.sbody in 709 let cost = block_cost fun_name cost_incr env block in 710 costs := StringTools.Map.add fun_name cost !costs ; 711 Cil.SkipChildren 712 713 end 714 715 (** [compute_costs extern_costs cost_incr env] computes the cost associated to 716 each function of the current program in the current project. First, it 717 computes the costs potentially depending on that of the other functions, and 718 then it tries to solve the system of inequations that this produces. *) 719 720 let compute_costs extern_costs cost_incr env 721 : (require list * Cost_value.t) StringTools.Map.t = 722 let costs : (require list * Cost_value.t) StringTools.Map.t ref = 723 ref StringTools.Map.empty in 724 let compute_costs_prj = 725 File.create_project_from_visitor 726 "cerco_compute_costs" 727 (new compute_costs cost_incr env costs) in 728 let f () = 729 let (requires, costs) = StringTools.Map.split_couple !costs in 730 let costs = solve_costs extern_costs (prototypes env) costs in 731 StringTools.Map.combine requires costs in 732 Project.on compute_costs_prj f () 2048 res && (Misc.String.Map.mem fun_name costs1) && 2049 (cost = Misc.String.Map.find fun_name costs1) in 2050 Misc.String.Map.fold f costs2 true 2051 2052 let string_of_fun_costs fun_costs = 2053 let f fun_name cost res = 2054 Printf.sprintf "%s%s: %s\n%!" res fun_name (AbsCost.to_string cost) in 2055 Misc.String.Map.fold f fun_costs "" 2056 2057 let solve_costs static_env costs = 2058 let costs = Costs.restore_formals static_env costs in 2059 let fun_costs = Costs.fun_costs costs in 2060 let prototypes = StaticEnv.prototypes static_env in 2061 let rec aux fun_costs = 2062 if !debug then Printf.printf "%s\n%!" (string_of_fun_costs fun_costs) ; 2063 let fun_costs' = AbsCost.reduces prototypes fun_costs in 2064 if solve_end fun_costs fun_costs' then fun_costs 2065 else aux fun_costs' in 2066 let fun_costs = aux fun_costs in 2067 let costs = Costs.set_fun_costs costs fun_costs in 2068 Costs.reduce_loops_annots prototypes costs 733 2069 734 2070 735 2071 (*** Add annotations ***) 736 2072 737 let add_tmp_ cost_init env tmp_coststmt =738 let lval = Cil.var tmp_ costin2073 let add_tmp_loop_init cost_varinfo tmp_loop stmt = 2074 let lval = Cil.var tmp_loop in 739 2075 let e = 740 Cil.new_exp dummy_location 741 (Cil_types.Lval (Cil.var (get_cost_varinfo env))) in 2076 Cil.new_exp dummy_location (Cil_types.Lval (Cil.var cost_varinfo)) in 742 2077 let new_stmt = 743 2078 Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in … … 745 2080 Cil.mkStmt (Cil_types.Block (Cil.mkBlock [new_stmt ; stmt])) 746 2081 2082 let make_tmp_formal_init fundec varinfo tmp_var = 2083 let tmp_var = Cil.makeTempVar fundec ~name:tmp_var varinfo.Cil_types.vtype in 2084 let lval = Cil.var tmp_var in 2085 let e = Cil.new_exp dummy_location (Cil_types.Lval (Cil.var varinfo)) in 2086 let new_stmt = Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in 2087 Cil.mkStmt new_stmt 2088 2089 let make_tmp_formals_init fundec l = 2090 let f (varinfo, tmp_var) = make_tmp_formal_init fundec varinfo tmp_var in 2091 List.map f l 2092 2093 let add_tmp_formals_init formals fundec = 2094 let tmp_formals_init = make_tmp_formals_init fundec formals in 2095 let block = tmp_formals_init @ fundec.Cil_types.sbody.Cil_types.bstmts in 2096 let body = { fundec.Cil_types.sbody with Cil_types.bstmts = block } in 2097 { fundec with Cil_types.sbody = body } 2098 2099 let make_require require = 2100 let rel = Require.relation require in 2101 let init_value = Require.init_value require in 2102 let exit_value = Require.exit_value require in 2103 let increment = Require.increment require in 2104 if Domain.is_concrete init_value && 2105 Domain.is_concrete exit_value && 2106 Domain.is_concrete increment then 2107 let zero = Domain.of_int 0 in 2108 let rel' = Domain.mk_strict rel in 2109 let cil_init_value = Domain.to_cil_term init_value in 2110 let cil_exit_value = Domain.to_cil_term exit_value in 2111 let cil_zero = Domain.to_cil_term zero in 2112 let cil_increment = Domain.to_cil_term increment in 2113 let cil_rel = Domain.cil_rel_of_rel rel in 2114 let cil_rel' = Domain.cil_rel_of_rel rel' in 2115 let t1 = Logic_const.prel (cil_rel, cil_init_value, cil_exit_value) in 2116 let t2 = Logic_const.prel (cil_rel', cil_zero, cil_increment) in 2117 let t3 = Logic_const.pimplies (t1, t2) in 2118 if Domain.bool_of_cond rel' zero increment then None 2119 else 2120 if Domain.bool_of_cond (Domain.opposite rel) init_value exit_value then 2121 None 2122 else 2123 if Domain.bool_of_cond rel init_value exit_value then Some t2 2124 else Some t3 2125 else None 2126 747 2127 let make_requires requires = 748 let f (rel, init_value, exit_value, increment) = 749 let init_value = Cost_value.to_cil_term init_value in 750 let exit_value = Cost_value.to_cil_term exit_value in 751 let increment = Cost_value.to_cil_term increment in 752 let rel' = Cost_value.mk_strict rel in 753 let rel = Cost_value.cil_rel_of_rel rel in 754 let rel' = Cost_value.cil_rel_of_rel rel' in 755 let t1 = Logic_const.prel (rel, init_value, exit_value) in 756 let t2 = Logic_const.prel (rel', Cost_value.tinteger 0, increment) in 757 Logic_const.pimplies (t1, t2) in 758 List.map f requires 2128 let f require res = 2129 let added_require = match make_require require with 2130  None > [] 2131  Some require > [require] in 2132 added_require @ res in 2133 Requires.fold f requires [] 759 2134 760 2135 let add_spec pres post spec = … … 769 2144 Cil.ChangeDoChildrenPost (spec, identity) 770 2145 771 let add_cost_incr_annotation cost_id spec =2146 let add_cost_incr_annotation cost_id fundec = 772 2147 let rel = Cil_types.Req in 773 let cost = Cost_value.Var "incr" in 774 add_cost_annotation [] rel cost_id cost spec 775 776 let add_regular_fun_annotation fun_name cost_id costs spec = 777 let rel = Cil_types.Rle in 778 let (requires, cost) = StringTools.Map.find fun_name costs in 779 add_cost_annotation requires rel cost_id cost spec 780 781 let add_fundec_annotation cost_id cost_incr costs fun_name spec = 2148 let cost = 2149 Logic_const.tvar (Cil_const.make_logic_var "incr" Cil_types.Linteger) in 2150 add_cost_annotation Requires.empty rel cost_id cost fundec 2151 2152 let add_regular_fun_annotation cost_id requires cost spec = 2153 if AbsCost.is_concrete cost then 2154 let cost = AbsCost.to_ext cost in 2155 let rel = Cil_types.Rle in 2156 if Domain.is_concrete cost then 2157 add_cost_annotation requires rel cost_id (Domain.to_cil_term cost) spec 2158 else Cil.DoChildren 2159 else Cil.DoChildren 2160 2161 let add_fundec_annotation static_env costs fun_name spec = 2162 assert (Costs.mem fun_name costs) ; 2163 let cost = Costs.find_cost fun_name costs in 2164 let requires = Costs.find_requires fun_name costs in 2165 let cost_id = StaticEnv.cost_id static_env in 2166 let cost_incr = StaticEnv.cost_incr static_env in 782 2167 if fun_name = cost_incr then add_cost_incr_annotation cost_id spec 783 else add_regular_fun_annotation fun_name cost_id costs spec 784 785 let mk_loop_invariant_counter_init_value 786 extern_costs costs prots counter init_value increment = 787 let mk_value value = 788 let incr_mod = Cost_value.abs increment in 789 let v = Cost_value.BinOp (Cost_value.Mod, value, incr_mod) in 790 Cost_value.to_cil_term (Cost_value.reduce extern_costs costs prots v) in 791 let v1 = mk_value (Cost_value.Var counter) in 792 let v2 = mk_value init_value in 793 let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in 794 mk_invariant invariant 795 796 let mk_loop_invariant_counter_last_value 797 extern_costs costs prots counter rel init_value exit_value increment = 798 let last_value = last_value rel init_value exit_value increment in 799 let last_value = Cost_value.reduce extern_costs costs prots last_value in 800 let last_value = Cost_value.to_cil_term last_value in 801 let rel' = Cost_value.cil_rel_of_rel rel in 802 let init_value = Cost_value.to_cil_term init_value in 803 let exit_value = Cost_value.to_cil_term exit_value in 804 let require = Logic_const.prel (rel', init_value, exit_value) in 805 let rel' = Cost_value.cil_rel_of_rel (Cost_value.mk_large rel) in 806 let counter = Cost_value.to_cil_term (Cost_value.Var counter) in 807 let prop = Logic_const.prel (rel', counter, last_value) in 808 let invariant = Logic_const.pimplies (require, prop) in 809 mk_invariant invariant 810 811 let mk_loop_invariant_counter_no_change counter rel init_value exit_value = 812 let rel = Cost_value.opposite rel in 813 let rel' = Cost_value.cil_rel_of_rel rel in 814 let init_value = Cost_value.to_cil_term init_value in 815 let exit_value = Cost_value.to_cil_term exit_value in 816 let require = Logic_const.prel (rel', init_value, exit_value) in 817 let counter = Cost_value.to_cil_term (Cost_value.Var counter) in 818 let prop = Logic_const.prel (Cil_types.Req, counter, init_value) in 819 let invariant = Logic_const.pimplies (require, prop) in 820 mk_invariant invariant 821 822 let mk_loop_invariant_cost 823 extern_costs tmp_cost costs prots cost_id counter cost = 824 let loop_cost = cost (Cost_value.Var counter) in 825 let loop_cost = Cost_value.reduce extern_costs costs prots loop_cost in 826 let loop_cost = Cost_value.to_cil_term loop_cost in 827 let cost_var = 828 Logic_const.tvar (Cil_const.make_logic_var cost_id Cil_types.Linteger) in 829 let tmp_cost = Cost_value.to_cil_term (Cost_value.Var tmp_cost) in 830 let new_cost = Cil_types.TBinOp (Cil_types.PlusA, tmp_cost, loop_cost) in 831 let new_cost = integer_term new_cost in 832 let invariant = Logic_const.prel (Cil_types.Rle, cost_var, new_cost) in 833 mk_invariant invariant 834 835 let mk_loop_variant 836 extern_costs costs prots counter init_value rel exit_value increment = 837 let last_value = last_value rel init_value exit_value increment in 838 let counter_var = Cost_value.Var counter in 839 let (v1, v2) = match rel with 840  Cost_value.Lt  Cost_value.Le > (last_value, counter_var) 841  Cost_value.Gt  Cost_value.Ge > (counter_var, last_value) in 842 let variant = Cost_value.BinOp (Cost_value.Sub, v1, v2) in 843 let variant = Cost_value.reduce extern_costs costs prots variant in 844 mk_variant (Cost_value.to_cil_term variant) 845 846 let annot_loop 847 extern_costs tmp_cost cost_id cost_incr env costs obj stmt 848 previous_stmt block = 849 let (_, costs) = StringTools.Map.split_couple costs in 850 let prots = prototypes env in 851 let fun_name = current_fun_name obj in 852 let (_, counter, init_value, rel, exit_value, increment, cost) = 853 loop_infos fun_name cost_incr env previous_stmt block in 854 let invariant_counter_init_value = 855 mk_loop_invariant_counter_init_value 856 extern_costs costs prots counter init_value increment in 857 let invariant_counter_last_value = 858 mk_loop_invariant_counter_last_value 859 extern_costs costs prots counter rel init_value exit_value increment in 860 let invariant_counter_no_change = 861 mk_loop_invariant_counter_no_change counter rel init_value exit_value in 862 let invariant_cost = 863 mk_loop_invariant_cost extern_costs tmp_cost costs prots cost_id 864 counter cost in 865 let variant = 866 mk_loop_variant extern_costs costs prots counter init_value rel exit_value 867 increment in 868 add_loop_annot obj stmt invariant_counter_init_value ; 869 add_loop_annot obj stmt invariant_counter_last_value ; 870 add_loop_annot obj stmt invariant_counter_no_change ; 871 add_loop_annot obj stmt invariant_cost ; 872 add_loop_annot obj stmt variant 873 874 class add_annotations extern_costs cost_id cost_incr env costs prj = 2168 else add_regular_fun_annotation cost_id requires cost spec 2169 2170 class add_annotations static_env costs prj = 875 2171 object (self) inherit Visitor.frama_c_copy prj as super 876 2172 877 val mutable tmp_costs : Cil_types.varinfo list = [] 878 val mutable previous_stmt = None 879 880 method vstmt_aux stmt = 881 let old_stmt = previous_stmt in 882 previous_stmt < Some stmt ; 883 match stmt.Cil_types.skind with 884  Cil_types.Loop (_, block, _, _, _) > 885 assert (List.length tmp_costs > 0) ; 886 let tmp_cost = List.hd tmp_costs in 887 tmp_costs < List.tl tmp_costs ; 888 let tmp_cost_id = tmp_cost.Cil_types.vname in 889 annot_loop 890 extern_costs tmp_cost_id cost_id cost_incr env costs self stmt 891 old_stmt block ; 892 Cil.ChangeDoChildrenPost (stmt, add_tmp_cost_init env tmp_cost) 893  _ > Cil.DoChildren 2173 val mutable current_fun_name : string = "" 2174 2175 method vstmt_aux stmt = match stmt.Cil_types.skind with 2176  Cil_types.Loop _ 2177 when StaticEnv.mem_loop_start current_fun_name stmt.Cil_types.sid 2178 static_env > 2179 let cost_varinfo = StaticEnv.cost_varinfo static_env in 2180 (* only use with costs correctly set and initialized *) 2181 assert (Costs.mem_loop_point current_fun_name stmt.Cil_types.sid costs) ; 2182 let tmp_loop = 2183 StaticEnv.find_tmp_loop current_fun_name stmt.Cil_types.sid 2184 static_env in 2185 let annots = 2186 Costs.find_loop_annots current_fun_name stmt.Cil_types.sid costs in 2187 add_loop_annots self stmt (LoopAnnots.to_cil annots) ; 2188 let change = add_tmp_loop_init cost_varinfo tmp_loop in 2189 Cil.ChangeDoChildrenPost (stmt, change) 2190  _ > Cil.DoChildren 2191 2192 method vfunc fundec = 2193 let fun_name = fundec.Cil_types.svar.Cil_types.vname in 2194 current_fun_name < fun_name ; 2195 if fun_name = StaticEnv.cost_incr static_env then Cil.SkipChildren 2196 else 2197 let formals = StaticEnv.formals fun_name static_env in 2198 Cil.ChangeDoChildrenPost (fundec, add_tmp_formals_init formals) 894 2199 895 2200 method vspec spec = match self#current_kf with … … 899 2204  Db_types.Definition (fundec, _) > 900 2205 let fun_name = fundec.Cil_types.svar.Cil_types.vname in 901 add_fundec_annotation cost_id cost_incr costs fun_name spec 902  Db_types.Declaration (_, f, _, _) when 903 StringTools.Map.mem f.Cil_types.vname extern_costs > 904 let cost = StringTools.Map.find f.Cil_types.vname extern_costs in 905 let cost = Cost_value.Var cost in 906 add_cost_annotation [] Cil_types.Rle cost_id cost spec 907  _ > Cil.JustCopy 908 909 method vfunc fundec = 910 let fun_name = fundec.Cil_types.svar.Cil_types.vname in 911 tmp_costs < make_freshes fundec (get_nb_loops env fun_name) cost_id ; 912 previous_stmt < None ; 913 Cil.DoChildren 914 915 end 916 917 let add_annotations extern_costs fname cost_id cost_incr env costs = 2206 add_fundec_annotation static_env costs fun_name spec 2207  Db_types.Declaration (_, f, _, _) > 2208 let fun_name = f.Cil_types.vname in 2209 add_fundec_annotation static_env costs fun_name spec 2210 2211 end 2212 2213 let add_annotations static_env costs = 918 2214 let add_annotations_prj = 919 2215 File.create_project_from_visitor 920 "cerco_add_annotations" 921 (new add_annotations extern_costs cost_id cost_incr env costs) in 2216 "add_annotations" (new add_annotations static_env costs) in 922 2217 let f () = 923 Parameters.CodeOutput.set fname;2218 Parameters.CodeOutput.set (StaticEnv.fname static_env) ; 924 2219 File.pretty_ast () in 925 2220 Project.on add_annotations_prj f () 926 2221 927 2222 928 (*** Saving cost results ***) 929 930 let save_results fname costs = 931 let f fun_name (_, cost) res = 932 res ^ fun_name ^ " " ^ (Cost_value.to_string cost) ^ "\n" in 933 let s = StringTools.Map.fold f costs "" in 2223 (*** Save results ***) 2224 2225 let save_results static_env costs = 2226 let fname = StaticEnv.f_old_name static_env in 2227 let f fun_name cost_info res = 2228 let cost = CostInfo.cost cost_info in 2229 res ^ 2230 (if AbsCost.is_concrete cost then 2231 fun_name ^ " " ^ (Domain.to_string (AbsCost.to_ext cost)) ^ "\n" 2232 else "") in 2233 let s = Costs.fold f costs "" in 934 2234 let save_file = 935 2235 try Filename.chop_extension fname … … 941 2241 close_out oc 942 2242 with Sys_error _ > 943 Printf.eprintf "Could not save plugin results in file %s \n%!" save_file2243 Printf.eprintf "Could not save plugin results in file %s.\n%!" save_file 944 2244 945 2245 … … 950 2250 Parameters.Files.set [fname] ; 951 2251 File.init_from_cmdline () ; 952 let env = initializations cost_id in 953 let costs = compute_costs extern_costs cost_incr env in 954 save_results f_old_name costs ; 955 add_annotations extern_costs fname cost_id cost_incr env costs 956 with e > Printf.eprintf "** ERROR: %s\n%!" (string_of_exception cost_incr e) 2252 if !debug then Printf.printf "Make CFG\n%!" ; 2253 make_CFG () ; 2254 if !debug then print_CFG () ; 2255 if !debug then Printf.printf "Initialize\n%!" ; 2256 let static_env = 2257 initialize "__tmp" fname f_old_name cost_id cost_incr extern_costs in 2258 if !debug then Printf.printf "Compute costs\n%!" ; 2259 let costs = compute_costs static_env in 2260 if !debug then Printf.printf "%s\n%!" (Costs.to_string costs) ; 2261 if !debug then Printf.printf "Solve costs\n%!" ; 2262 let costs = solve_costs static_env costs in 2263 if !debug then Printf.printf "Costs:\n%s\n%!" (Costs.to_string costs) ; 2264 if !debug then Printf.printf "Save results\n%!" ; 2265 save_results static_env costs ; 2266 if !debug then Printf.printf "Add annotations\n%!" ; 2267 add_annotations static_env costs 2268 with e > Printf.eprintf "** ERROR: %s.\n%!" (string_of_exception e)
Note: See TracChangeset
for help on using the changeset viewer.