[1462] | 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 plug-in |
---|
| 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 so-called 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 | |
---|
| 32 | |
---|
| 33 | (*** Exceptions ***) |
---|
| 34 | |
---|
| 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 | non-constant 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 non-constant 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." |
---|
| 63 | | e -> raise e |
---|
| 64 | |
---|
| 65 | |
---|
| 66 | (*** Helpers ***) |
---|
| 67 | |
---|
| 68 | let identity x = x |
---|
| 69 | |
---|
| 70 | let integer_term term = Logic_const.term term Cil_types.Linteger |
---|
| 71 | |
---|
| 72 | let add_loop_annot obj stmt annot = |
---|
| 73 | Queue.add (fun () -> Annotations.add stmt [Ast.self] annot) |
---|
| 74 | obj#get_filling_actions |
---|
| 75 | |
---|
| 76 | let loop_annotation annot = Db_types.Before (Db_types.User annot) |
---|
| 77 | |
---|
| 78 | let mk_invariant pred = |
---|
| 79 | let annot = |
---|
| 80 | Logic_const.new_code_annotation (Cil_types.AInvariant ([], true, pred)) in |
---|
| 81 | loop_annotation annot |
---|
| 82 | |
---|
| 83 | let mk_variant term = |
---|
| 84 | let annot = |
---|
| 85 | Logic_const.new_code_annotation (Cil_types.AVariant (term, None)) in |
---|
| 86 | loop_annotation annot |
---|
| 87 | |
---|
| 88 | let current_kf obj = match obj#current_kf with |
---|
| 89 | | None -> raise (Failure "Compute.current_kf") |
---|
| 90 | | Some kf -> kf |
---|
| 91 | |
---|
| 92 | let current_fundec obj = match (current_kf obj).Db_types.fundec with |
---|
| 93 | | Db_types.Definition (fundec, _) -> fundec |
---|
| 94 | | _ -> raise (Failure "Compute.current_fundec") |
---|
| 95 | |
---|
| 96 | let current_fun_name obj = (current_fundec obj).Cil_types.svar.Cil_types.vname |
---|
| 97 | |
---|
| 98 | let current_spec obj = (current_fundec obj).Cil_types.sspec |
---|
| 99 | |
---|
| 100 | let mk_fun_cost_pred rel cost_id cost = |
---|
| 101 | let cost_var = Cil_const.make_logic_var cost_id Cil_types.Linteger in |
---|
| 102 | let cost_var = Logic_const.tvar cost_var in |
---|
| 103 | let cost = Cost_value.to_cil_term cost in |
---|
| 104 | let old_cost = |
---|
| 105 | Logic_const.term (Cil_types.Told cost_var) cost_var.Cil_types.term_type in |
---|
| 106 | let new_cost = Cil_types.TBinOp (Cil_types.PlusA, old_cost, cost) in |
---|
| 107 | let new_cost = integer_term new_cost in |
---|
| 108 | Logic_const.prel (rel, cost_var, new_cost) |
---|
| 109 | |
---|
| 110 | let rec make_freshes fundec n prefix = |
---|
| 111 | let name = prefix ^ "_tmp" ^ (string_of_int (n-1)) in |
---|
| 112 | if n <= 0 then [] |
---|
| 113 | else (make_freshes fundec (n-1) 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 | |
---|
[1508] | 205 | let are_parameters env fun_name = |
---|
| 206 | StringTools.Set.for_all (is_parameter env fun_name) |
---|
[1462] | 207 | |
---|
| 208 | let prototypes env = |
---|
| 209 | let f fun_info = fun_info.parameters in |
---|
| 210 | StringTools.Map.map f (get_fun_infos env) |
---|
| 211 | |
---|
| 212 | let get_locals env fun_name = (get_fun_info env fun_name).locals |
---|
| 213 | |
---|
| 214 | let get_modified env fun_name = (get_fun_info env fun_name).modified |
---|
| 215 | |
---|
| 216 | let upd_modified env fun_name modified = |
---|
| 217 | let fun_info = get_fun_info env fun_name in |
---|
| 218 | let fun_info = { fun_info with modified = modified } in |
---|
| 219 | upd_fun_info env fun_name fun_info |
---|
| 220 | |
---|
| 221 | let get_nb_loops env fun_name = |
---|
| 222 | (get_fun_info env fun_name).nb_loops |
---|
| 223 | |
---|
| 224 | let upd_nb_loops env fun_name nb_loops = |
---|
| 225 | let fun_info = get_fun_info env fun_name in |
---|
| 226 | let fun_info = { fun_info with nb_loops = nb_loops } in |
---|
| 227 | upd_fun_info env fun_name fun_info |
---|
| 228 | |
---|
| 229 | let add_nb_loops env fun_name = |
---|
| 230 | upd_nb_loops env fun_name ((get_nb_loops env fun_name) + 1) |
---|
| 231 | |
---|
| 232 | let dummy_location = (Lexing.dummy_pos, Lexing.dummy_pos) |
---|
| 233 | |
---|
| 234 | |
---|
| 235 | (*** Initializations ***) |
---|
| 236 | |
---|
| 237 | (* Initializing the environment simply consists in visiting every function and |
---|
| 238 | set their information in the environment. *) |
---|
| 239 | |
---|
| 240 | class initializations cost_id env prj = object (self) |
---|
| 241 | inherit Visitor.frama_c_copy prj as super |
---|
| 242 | |
---|
| 243 | (* Update the variables whose address may be accessed. This is done by |
---|
| 244 | visiting every expression of the program. *) |
---|
| 245 | method vexpr e = |
---|
| 246 | let _ = match e.Cil_types.enode with |
---|
| 247 | | Cil_types.AddrOf (Cil_types.Var var, _) -> |
---|
| 248 | let fun_name = current_fun_name self in |
---|
| 249 | let addressed = get_addressed !env fun_name in |
---|
| 250 | let addressed = |
---|
| 251 | StringTools.Set.add var.Cil_types.vname addressed in |
---|
| 252 | env := upd_addressed !env fun_name addressed |
---|
| 253 | | _ -> () in |
---|
| 254 | Cil.DoChildren |
---|
| 255 | |
---|
| 256 | (* Update the variables whose address may be accessed. This is done by |
---|
| 257 | visiting every statement of the program. *) |
---|
| 258 | method vstmt_aux stmt = |
---|
| 259 | let fun_name = current_fun_name self in |
---|
| 260 | let _ = match stmt.Cil_types.skind with |
---|
| 261 | | Cil_types.Instr (Cil_types.Set ((Cil_types.Var var, _), _, _)) -> |
---|
| 262 | let modified = get_modified !env fun_name in |
---|
| 263 | let modified = StringTools.Set.add var.Cil_types.vname modified in |
---|
| 264 | env := upd_modified !env fun_name modified |
---|
| 265 | | Cil_types.Loop _ -> env := add_nb_loops !env fun_name |
---|
| 266 | | _ -> () in |
---|
| 267 | Cil.DoChildren |
---|
| 268 | |
---|
| 269 | (* When a function is found, create its entry in the environment, set its |
---|
| 270 | parameters and its locals (the information is already accessible), and |
---|
| 271 | leave empty the set of assigned and addressed variables. The two latters |
---|
| 272 | will be updated when visiting the statements and the expressions. *) |
---|
| 273 | method vfunc fundec = |
---|
| 274 | let fun_name = fundec.Cil_types.svar.Cil_types.vname in |
---|
| 275 | let addressed = StringTools.Set.empty in |
---|
| 276 | let varinfo_to_string x = x.Cil_types.vname in |
---|
| 277 | let parameters = List.map varinfo_to_string fundec.Cil_types.sformals in |
---|
| 278 | let f_locals res x = StringTools.Set.add (varinfo_to_string x) res in |
---|
| 279 | let locals = |
---|
| 280 | List.fold_left f_locals StringTools.Set.empty fundec.Cil_types.slocals in |
---|
| 281 | let modified = StringTools.Set.empty in |
---|
| 282 | let nb_loops = 0 in |
---|
| 283 | let fun_info = |
---|
| 284 | mk_fun_info addressed parameters locals modified nb_loops in |
---|
| 285 | let fun_infos = |
---|
| 286 | StringTools.Map.add fun_name fun_info (get_fun_infos !env) in |
---|
| 287 | env := upd_fun_infos !env fun_infos ; |
---|
| 288 | Cil.DoChildren |
---|
| 289 | |
---|
| 290 | (* Update the varinfo of the cost variable. *) |
---|
| 291 | method vglob_aux glob = |
---|
| 292 | let _ = match glob with |
---|
| 293 | | Cil_types.GVarDecl (_, varinfo, _) |
---|
| 294 | | Cil_types.GVar (varinfo, _, _) when varinfo.Cil_types.vname = cost_id -> |
---|
| 295 | env := upd_cost_varinfo !env varinfo |
---|
| 296 | | _ -> () in |
---|
| 297 | Cil.DoChildren |
---|
| 298 | |
---|
| 299 | end |
---|
| 300 | |
---|
| 301 | (** [initializations cost_id] consider the current file in the current project |
---|
| 302 | and returns a corresponding initialized environment .*) |
---|
| 303 | |
---|
| 304 | let initializations cost_id : env = |
---|
| 305 | let env : env ref = ref init_env in |
---|
| 306 | let initializations_prj = |
---|
| 307 | File.create_project_from_visitor |
---|
| 308 | "cerco_initializations" (new initializations cost_id env) in |
---|
| 309 | let f () = !env in |
---|
| 310 | Project.on initializations_prj f () |
---|
| 311 | |
---|
| 312 | |
---|
| 313 | (* Test if a block has a loop. Used to test the presence of nested |
---|
| 314 | loops. Indeed, they not supported for now, until a bug in Jessie is fixed. *) |
---|
| 315 | |
---|
| 316 | let rec has_loop_stmt stmt = match stmt.Cil_types.skind with |
---|
| 317 | | Cil_types.Instr _ | Cil_types.Return _ | Cil_types.Goto _ |
---|
| 318 | | Cil_types.Break _ | Cil_types.Continue _ -> false |
---|
| 319 | | Cil_types.If (_, block1, block2, _) |
---|
| 320 | | Cil_types.TryFinally (block1, block2, _) |
---|
| 321 | | Cil_types.TryExcept (block1, _, block2, _) -> |
---|
| 322 | (has_loop block1) || (has_loop block2) |
---|
| 323 | | Cil_types.Switch (_, block, _, _) |
---|
| 324 | | Cil_types.Block block -> has_loop block |
---|
| 325 | | Cil_types.Loop _ -> true |
---|
| 326 | | Cil_types.UnspecifiedSequence l -> |
---|
| 327 | has_loop_stmt_list (List.map (fun (stmt, _, _, _, _) -> stmt) l) |
---|
| 328 | |
---|
| 329 | and has_loop_stmt_list stmt_list = |
---|
| 330 | let f res stmt = res || (has_loop_stmt stmt) in |
---|
| 331 | List.fold_left f false stmt_list |
---|
| 332 | |
---|
| 333 | (** [has_loop block] returns true iff the block of instructions [block] contains |
---|
| 334 | a loop. *) |
---|
| 335 | |
---|
| 336 | and has_loop block = has_loop_stmt_list block.Cil_types.bstmts |
---|
| 337 | |
---|
| 338 | |
---|
| 339 | (*** Statement and block cost ***) |
---|
| 340 | |
---|
| 341 | (* Requirement for loop termination. They have the form: |
---|
| 342 | (guard relation, initialization value, exit value, increment) *) |
---|
| 343 | |
---|
| 344 | type require = Cost_value.relation * Cost_value.t * Cost_value.t * Cost_value.t |
---|
| 345 | |
---|
| 346 | (** [const_incr_cost e] extracts the integer constant that the expression [e] |
---|
| 347 | represents. *) |
---|
| 348 | |
---|
[1508] | 349 | let cost_incr_cost e = |
---|
| 350 | match e.Cil_types.enode with |
---|
| 351 | | Cil_types.Const (Cil_types.CInt64 (i, _, _)) -> |
---|
| 352 | Cost_value.Int (Int64.to_int i) |
---|
| 353 | | _ -> raise Cost_incr_arg_not_constant |
---|
[1462] | 354 | |
---|
| 355 | (** [call cost cost_incr f args] returns the cost of calling the function [f] on |
---|
| 356 | arguments [args]. If the function is the cost update function [cost_incr], |
---|
| 357 | then its cost is the value of its argument, which needs to be a constant |
---|
| 358 | integer. Otherwise, it is simply the cost of executing [f] on its |
---|
| 359 | arguments. *) |
---|
| 360 | |
---|
| 361 | let call_cost cost_incr f args = match f.Cil_types.enode with |
---|
[1508] | 362 | | Cil_types.Lval (Cil_types.Var var, Cil_types.NoOffset) |
---|
[1462] | 363 | when var.Cil_types.vname = cost_incr -> |
---|
[1508] | 364 | cost_incr_cost (List.hd args) |
---|
| 365 | | Cil_types.Lval (Cil_types.Var var, Cil_types.NoOffset) -> |
---|
[1462] | 366 | (try |
---|
| 367 | let args = List.map Cost_value.of_cil_exp args in |
---|
| 368 | Cost_value.CostOf (var.Cil_types.vname, args) |
---|
| 369 | with Cost_value.Unsupported_exp -> raise Unsupported_exp) |
---|
| 370 | | _ -> raise Unresolvable_function |
---|
| 371 | |
---|
| 372 | (** [instr_cost cost_incr instr] returns the cost of executing the simple |
---|
| 373 | instruction [instr]. Only function calls do have a cost. *) |
---|
| 374 | |
---|
| 375 | let instr_cost cost_incr = function |
---|
| 376 | | Cil_types.Call (_, f, args, _) -> |
---|
| 377 | call_cost cost_incr f args |
---|
| 378 | | _ -> Cost_value.Int 0 |
---|
| 379 | |
---|
| 380 | (* Frama-C sometimes transforms the control flow graph of a function by |
---|
| 381 | factorizing a return instructions through added gotos. We handle this special |
---|
| 382 | case of gotos with the function below, but other forms are not supported. *) |
---|
| 383 | |
---|
| 384 | let goto_cost stmt = match stmt.Cil_types.skind with |
---|
| 385 | | Cil_types.Return _ -> ([], Cost_value.Int 0) |
---|
| 386 | | _ -> raise (Unsupported "goto") |
---|
| 387 | |
---|
| 388 | (* In Frama-C, every C loop construct is transformed into an infinite loop with |
---|
| 389 | a break inside a conditional to exit. Initialization of a for loop are |
---|
| 390 | located in the very previous instruction. The guard can either be at the |
---|
| 391 | beginning of the loop in the cases of for and while loops, or at the end in |
---|
| 392 | the case of a do-while loop. Finally, the increment instruction is located at |
---|
| 393 | the end in the case of a for loop. *) |
---|
| 394 | |
---|
| 395 | (** [extract_counter_and_init stmt_opt] supposes that the optional statement |
---|
| 396 | [stmt_opt] is in fact an assignment instruction. In this case, it returns |
---|
| 397 | the assigned variable and the expression to assign, otherwise it raises an |
---|
| 398 | error. It will be used to extract the loop counter and its first value in |
---|
| 399 | the case of a loop initialization instruction. *) |
---|
| 400 | |
---|
[1508] | 401 | let extract_counter_and_init stmt2_opt stmt1_opt = |
---|
[1462] | 402 | let error () = raise (Unsupported_loop "no initialization found") in |
---|
[1508] | 403 | match stmt2_opt, stmt1_opt with |
---|
| 404 | | None, _ | _, None -> error () |
---|
| 405 | | Some stmt2, Some stmt1 -> |
---|
| 406 | match stmt2.Cil_types.skind, stmt1.Cil_types.skind with |
---|
| 407 | | Cil_types.Instr (Cil_types.Set ((Cil_types.Var i, _), z, _)), |
---|
| 408 | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) -> |
---|
| 409 | (match Cost_value.of_cil_exp z with |
---|
| 410 | | Cost_value.Int 0 -> |
---|
| 411 | (v.Cil_types.vname, i.Cil_types.vname, Cost_value.of_cil_exp e) |
---|
| 412 | | _ -> error()) |
---|
[1462] | 413 | | _ -> error () |
---|
| 414 | |
---|
| 415 | (** [first_stmt block] returns the first statement of the block [block], if |
---|
| 416 | any. *) |
---|
| 417 | |
---|
| 418 | let first_stmt block = match block.Cil_types.bstmts with |
---|
| 419 | | [] -> raise (Unsupported_loop "no guard") |
---|
| 420 | | instr :: _ -> instr |
---|
| 421 | |
---|
| 422 | (** [exp_is_var name e] returns true iff the expression [e] is in fact the |
---|
| 423 | variable of name [name]. *) |
---|
| 424 | |
---|
| 425 | let exp_is_var name e = match e.Cil_types.enode with |
---|
[1508] | 426 | | Cil_types.Lval (Cil_types.Var v, Cil_types.NoOffset) -> |
---|
| 427 | v.Cil_types.vname = name |
---|
[1462] | 428 | | _ -> false |
---|
| 429 | |
---|
[1508] | 430 | let var_of_exp e = match e.Cil_types.enode with |
---|
| 431 | | Cil_types.Lval (Cil_types.Var v, Cil_types.NoOffset) -> |
---|
| 432 | v.Cil_types.vname |
---|
| 433 | | _ -> invalid_arg "var_of_exp" |
---|
| 434 | |
---|
| 435 | let const_of_exp e = |
---|
| 436 | match e.Cil_types.enode with |
---|
| 437 | | Cil_types.Const (Cil_types.CInt64 (i, _, _)) -> |
---|
| 438 | Int64.to_int i |
---|
| 439 | | _ -> invalid_arg "const_of_exp" |
---|
| 440 | |
---|
[1462] | 441 | (** [starts_with_break block] returns true iff the block [block] starts with a |
---|
| 442 | break instruction. *) |
---|
| 443 | |
---|
| 444 | let starts_with_break block = match (first_stmt block).Cil_types.skind with |
---|
| 445 | | Cil_types.Break _ -> true |
---|
| 446 | | _ -> false |
---|
| 447 | |
---|
| 448 | (** [extract_guard counter block] supposes that the first statement of the block |
---|
| 449 | [block] is a conditional with an exit instruction. It then supposes that the |
---|
| 450 | conditional is a test on the variable [counter]. It returns the comparison |
---|
| 451 | relation along with the expression that the counter is compared to. It will |
---|
| 452 | be used to extract the guard condition of a loop. *) |
---|
| 453 | |
---|
| 454 | let extract_guard counter block = match (first_stmt block).Cil_types.skind with |
---|
| 455 | | Cil_types.If (e, _, block, _) when starts_with_break block -> |
---|
| 456 | (match e.Cil_types.enode with |
---|
| 457 | | Cil_types.BinOp (rel, e1, e2, _) when exp_is_var counter e1 -> |
---|
| 458 | (Cost_value.rel_of_cil_rel rel, Cost_value.of_cil_exp e2) |
---|
| 459 | | _ -> raise (Unsupported_loop "unsupported guard expression")) |
---|
| 460 | | _ -> raise (Unsupported_loop "no guard found") |
---|
| 461 | |
---|
| 462 | (** [last l] returns the last element of the list [l], if any. *) |
---|
| 463 | |
---|
| 464 | let rec last = function |
---|
| 465 | | [] -> raise (Failure "Compute.last") |
---|
| 466 | | [e] -> e |
---|
| 467 | | _ :: l -> last l |
---|
| 468 | |
---|
[1508] | 469 | let rec last_2 = function |
---|
| 470 | | [] | [_] -> raise (Failure "Compute.last_2") |
---|
| 471 | | [e1 ; e2] -> (e1, e2) |
---|
| 472 | | _ :: l -> last_2 l |
---|
| 473 | |
---|
| 474 | let rec last_stmt stmt = match stmt.Cil_types.skind with |
---|
| 475 | | Cil_types.Block block -> |
---|
| 476 | last_stmt (last block.Cil_types.bstmts) |
---|
| 477 | | _ -> stmt |
---|
| 478 | |
---|
| 479 | (** [last_2_stmt block] returns the last two statement of the block [block], if |
---|
[1462] | 480 | any. *) |
---|
| 481 | |
---|
[1508] | 482 | let last_2_stmt block = match block.Cil_types.bstmts with |
---|
| 483 | | [] | [_] -> raise (Unsupported_loop "no increment instruction") |
---|
| 484 | | stmts -> |
---|
| 485 | let (snd_last, last) = last_2 stmts in |
---|
| 486 | (last_stmt snd_last, last) |
---|
[1462] | 487 | |
---|
[1508] | 488 | |
---|
[1462] | 489 | (** [extract_added_value counter e] supposes that the expression [e] is either |
---|
| 490 | an addition or a substraction of the variable [counter]. It returns the |
---|
| 491 | added value: exactly the value in case of an addition, and its opposite in |
---|
| 492 | case of a substraction. It will be used to extract the increment of the |
---|
| 493 | counter in a loop. *) |
---|
| 494 | |
---|
| 495 | let extract_added_value counter e = match e.Cil_types.enode with |
---|
| 496 | | Cil_types.BinOp (Cil_types.PlusA, e1, e2, _) when exp_is_var counter e1 -> |
---|
| 497 | Cost_value.of_cil_exp e2 |
---|
| 498 | | Cil_types.BinOp (Cil_types.MinusA, e1, e2, _) when exp_is_var counter e1 -> |
---|
| 499 | Cost_value.UnOp (Cost_value.Neg, Cost_value.of_cil_exp e2) |
---|
| 500 | | _ -> raise (Unsupported_loop "unsupported increment expression") |
---|
| 501 | |
---|
| 502 | (** [extract_increment counter block] supposes that the block [block] ends with |
---|
| 503 | an increment of the variable [counter]. It returns the increment. It will be |
---|
| 504 | used to extract the increment in a loop body. *) |
---|
| 505 | |
---|
[1508] | 506 | let extract_increment counter index block = |
---|
| 507 | let (snd_last, last) = last_2_stmt block in |
---|
| 508 | match snd_last.Cil_types.skind, last.Cil_types.skind with |
---|
| 509 | | Cil_types.Instr (Cil_types.Set ((Cil_types.Var i, _), o, _)), |
---|
| 510 | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), e, _)) |
---|
| 511 | when v.Cil_types.vname = counter && i.Cil_types.vname = index -> |
---|
| 512 | (match extract_added_value index o with |
---|
| 513 | | Cost_value.Int 1 -> extract_added_value counter e |
---|
| 514 | | _ -> raise (Unsupported_loop "loop index malformation")) |
---|
[1462] | 515 | | _ -> raise (Unsupported_loop "no increment instruction found") |
---|
| 516 | |
---|
| 517 | let check b error = if not b then raise (Unsupported_loop error) |
---|
| 518 | |
---|
| 519 | (** [counter_preserved_until_last counter block] returns true iff the variable |
---|
| 520 | [counter] is not assigned in the block [block], except potentially at the |
---|
| 521 | very last instruction. This is a support condition for loops. *) |
---|
| 522 | |
---|
| 523 | let counter_preserved_until_last counter block = |
---|
| 524 | let stmt_preserves stmt = match stmt.Cil_types.skind with |
---|
| 525 | | Cil_types.Instr (Cil_types.Set ((Cil_types.Var v, _), _, _)) -> |
---|
| 526 | v.Cil_types.vname <> counter |
---|
| 527 | | _ -> true in |
---|
| 528 | let rec aux = function |
---|
| 529 | | [] | [_] -> true |
---|
| 530 | | stmt :: block -> (stmt_preserves stmt) && (aux block) in |
---|
| 531 | aux block.Cil_types.bstmts |
---|
| 532 | |
---|
| 533 | (** [check supported_loop fun_name env counter init_value exit_value increment |
---|
| 534 | block] raises an exception if the loop body [block] of the function |
---|
| 535 | [fun_name] is not supported in the environment [env] and with regards to the |
---|
| 536 | loop counter [counter], its initialization expression [init_value] and its |
---|
| 537 | exit expression [exit_value]. We check that: the address of the loop counter |
---|
| 538 | is not accessed in the whole function, the loop counter is not assigned in |
---|
| 539 | the body (except at the end), the variables in the initialization and exit |
---|
| 540 | expressions are parameters and their address is not accessed nor are they |
---|
| 541 | assigned in the whole function. *) |
---|
| 542 | |
---|
| 543 | let check_supported_loop |
---|
| 544 | fun_name env counter init_value exit_value increment block = |
---|
| 545 | let fun_info = get_fun_info env fun_name in |
---|
| 546 | let addressed = fun_info.addressed in |
---|
| 547 | let parameters = StringTools.Set.of_list fun_info.parameters in |
---|
| 548 | let modified = fun_info.modified in |
---|
| 549 | let init_value_vars = Cost_value.vars init_value in |
---|
| 550 | let exit_value_vars = Cost_value.vars exit_value in |
---|
| 551 | let increment_vars = Cost_value.vars increment in |
---|
| 552 | let vars = StringTools.Set.union init_value_vars exit_value_vars in |
---|
| 553 | let vars = StringTools.Set.union vars increment_vars in |
---|
| 554 | let addressed_or_modified = StringTools.Set.union addressed modified in |
---|
| 555 | check (not (StringTools.Set.mem counter addressed)) |
---|
| 556 | "loop counter's address is accessed" ; |
---|
| 557 | check (counter_preserved_until_last counter block) |
---|
| 558 | "loop counter is modified inside loop body" ; |
---|
| 559 | check (StringTools.Set.subset vars parameters) |
---|
| 560 | "local or global inside a loop expression" ; |
---|
| 561 | check (StringTools.Set.disjoint vars addressed_or_modified) |
---|
| 562 | "the value of a parameter in a loop expression may be modified" |
---|
| 563 | |
---|
[1508] | 564 | let rec mk_loop_cost_index index k v inc cost = |
---|
| 565 | let round_up h a b = |
---|
| 566 | let h_mod_a = h mod a in |
---|
| 567 | let b_mod_a = b mod a in |
---|
| 568 | h - h_mod_a + b_mod_a + if h_mod_a <= b_mod_a then 0 else a in |
---|
| 569 | match cost with |
---|
| 570 | | Cost_value.CostCond (i, cond, tif, telse) when i <> index -> |
---|
| 571 | let tif = mk_loop_cost_index index k v inc tif in |
---|
| 572 | let telse = mk_loop_cost_index index k v inc telse in |
---|
| 573 | Cost_value.CostCond (i, cond, tif, telse) |
---|
| 574 | | Cost_value.CostCond (_, Cost_value.Ceq h, _, telse) when k > h -> |
---|
| 575 | mk_loop_cost_index index k v inc telse |
---|
| 576 | | Cost_value.CostCond (_, Cost_value.Ceq h, tif, telse) when k = h -> |
---|
| 577 | (* let sum = *) |
---|
| 578 | Cost_value.add tif (mk_loop_cost_index index (k+inc) v inc telse) (* in *) |
---|
| 579 | (* Cost_value.Cond(v, Cost_value.Le, Cost_value.Int k, Cost_value.Int 0, sum) *) |
---|
| 580 | | Cost_value.CostCond (_, Cost_value.Ceq h, tif, telse) |
---|
| 581 | when (h - k) mod inc = 0 -> |
---|
| 582 | let tif' = mk_loop_cost_index index k v inc telse in |
---|
| 583 | let h_val = Cost_value.Int h in |
---|
| 584 | let sum = |
---|
| 585 | Cost_value.add tif (mk_loop_cost_index index (h + inc) v inc telse) in |
---|
| 586 | let telse' = |
---|
| 587 | Cost_value.add (mk_loop_cost_index index k h_val inc telse) sum in |
---|
| 588 | Cost_value.Cond(v, Cost_value.Lt, Cost_value.Int h, tif', telse') |
---|
| 589 | | Cost_value.CostCond (_, Cost_value.Ceq _, _, telse) -> |
---|
| 590 | mk_loop_cost_index index k v inc telse |
---|
| 591 | | Cost_value.CostCond (_, Cost_value.Cgeq h, tif, _) when k >= h -> |
---|
| 592 | mk_loop_cost_index index k v inc tif |
---|
| 593 | | Cost_value.CostCond (_, Cost_value.Cgeq h, tif, telse) -> |
---|
| 594 | let tif' = mk_loop_cost_index index k v inc telse in |
---|
| 595 | let h_val = Cost_value.Int h in |
---|
| 596 | let telse' = |
---|
| 597 | Cost_value.add |
---|
| 598 | (mk_loop_cost_index index k h_val inc telse) |
---|
| 599 | (mk_loop_cost_index index (round_up h inc k) v inc tif) in |
---|
| 600 | Cost_value.Cond(v, Cost_value.Lt, Cost_value.Int h, tif', telse') |
---|
| 601 | (* I'm supposing unrolling is never repeated *) |
---|
| 602 | | Cost_value.CostCond (_, Cost_value.Cmod (a, b), tif, telse) when inc = 1 -> |
---|
| 603 | let k' = round_up k a b in |
---|
| 604 | let sub = Cost_value.sub |
---|
| 605 | (mk_loop_cost_index index k' v a tif) |
---|
| 606 | (mk_loop_cost_index index k' v a telse) in |
---|
| 607 | Cost_value.add (mk_loop_cost_index index k v 1 telse) sub |
---|
| 608 | | Cost_value.CostCond (_, Cost_value.Cmod (a, b), tif, telse) |
---|
| 609 | when inc = a -> |
---|
| 610 | let next = if k mod inc = b then tif else telse in |
---|
| 611 | mk_loop_cost_index index k v inc next |
---|
| 612 | | Cost_value.CostCond (_, Cost_value.Cmod _, _, _) -> |
---|
| 613 | raise (Unsupported_loop "possible repeated unrolling") |
---|
| 614 | | Cost_value.CostCond (_, Cost_value.Cgeqmod (h, a, b), tif, telse) |
---|
| 615 | when k >= h -> |
---|
| 616 | let next = |
---|
| 617 | Cost_value.CostCond (index, Cost_value.Cmod (a, b), tif, telse) in |
---|
| 618 | mk_loop_cost_index index k v inc next |
---|
| 619 | | Cost_value.CostCond (_, Cost_value.Cgeqmod (h, a, b), tif, telse) -> |
---|
| 620 | let tif' = mk_loop_cost_index index k v inc telse in |
---|
| 621 | let h_val = Cost_value.Int h in |
---|
| 622 | let next = |
---|
| 623 | Cost_value.CostCond (index, Cost_value.Cmod (a, b), tif, telse) in |
---|
| 624 | let telse' = |
---|
| 625 | Cost_value.add |
---|
| 626 | (mk_loop_cost_index index k h_val inc telse) |
---|
| 627 | (mk_loop_cost_index index (round_up h inc k) v inc next) in |
---|
| 628 | Cost_value.Cond(v, Cost_value.Lt, Cost_value.Int h, tif', telse') |
---|
| 629 | | Cost_value.CostCond _ -> |
---|
| 630 | raise (Unsupported_loop "unsupported cost condition") |
---|
| 631 | | _ -> |
---|
| 632 | let k_val = Cost_value.Int k in |
---|
| 633 | let inc_val = Cost_value.Int inc in |
---|
| 634 | let inc_val_m_1 = Cost_value.sub inc_val (Cost_value.Int 1) in |
---|
| 635 | let n = Cost_value.add (Cost_value.sub v k_val) inc_val_m_1 in |
---|
| 636 | let n = Cost_value.div n inc_val in |
---|
| 637 | Cost_value.mul n cost |
---|
| 638 | (* let zero = Cost_value.Int 0 in *) |
---|
| 639 | (* Cost_value.Cond (v, Cost_value.Gt, k_val, Cost_value.mul n cost, zero) *) |
---|
| 640 | |
---|
[1462] | 641 | (** [mk_loop_cost init_value increment body_cost] returns a function that, when |
---|
| 642 | providing a current value of the loop counter, returns the current cost of a |
---|
| 643 | loop of first value [init_value], of increment [increment] and whose body |
---|
| 644 | cost is [body_cost]. This function will be used with the loop counter for an |
---|
| 645 | invariant of the loop, and with the final value of the counter for a total |
---|
| 646 | cost of the loop. *) |
---|
| 647 | |
---|
[1508] | 648 | let mk_loop_cost init_value increment index body_cost = |
---|
[1462] | 649 | fun i -> |
---|
| 650 | let v = Cost_value.BinOp (Cost_value.Sub, i, init_value) in |
---|
| 651 | let v = Cost_value.BinOp (Cost_value.Div, v, increment) in |
---|
[1508] | 652 | (* this will in general reduce the steps and the size of amalgamation *) |
---|
| 653 | let e = StringTools.Map.empty in |
---|
| 654 | let body_cost = Cost_value.reduce e e e body_cost in |
---|
| 655 | let body_cost = Cost_value.amalgamation body_cost in |
---|
[1689] | 656 | Printf.printf "%s\n" (to_string body_cost); |
---|
[1508] | 657 | mk_loop_cost_index index 0 v 1 body_cost |
---|
[1462] | 658 | |
---|
[1508] | 659 | |
---|
| 660 | |
---|
[1462] | 661 | (** [last_value rel init_value exit_value increment] returns the last value |
---|
| 662 | taken by the counter of a loop when the first value is [init_value], the |
---|
| 663 | comparison relation in the guard is [rel], the compared value is |
---|
| 664 | [exit_value] and the increment is [increment]. *) |
---|
| 665 | |
---|
| 666 | let last_value rel init_value exit_value increment = |
---|
| 667 | let (op1, v1, v2, v3) = match rel with |
---|
| 668 | | Cost_value.Le -> (Cost_value.Sub, exit_value, init_value, increment) |
---|
| 669 | | Cost_value.Lt -> |
---|
| 670 | (Cost_value.Add, init_value, exit_value, Cost_value.Int 0) |
---|
| 671 | | Cost_value.Ge -> (Cost_value.Add, init_value, exit_value, increment) |
---|
| 672 | | Cost_value.Gt -> |
---|
| 673 | (Cost_value.Sub, exit_value, init_value, Cost_value.Int 0) in |
---|
| 674 | let res = Cost_value.BinOp (Cost_value.Sub, v1, v2) in |
---|
| 675 | let incr_mod = Cost_value.abs increment in |
---|
| 676 | let res = Cost_value.BinOp (Cost_value.Mod, res, incr_mod) in |
---|
| 677 | let res = Cost_value.BinOp (op1, exit_value, res) in |
---|
| 678 | Cost_value.BinOp (Cost_value.Add, res, v3) |
---|
| 679 | |
---|
[1508] | 680 | (** [stmt_cost fun_name cost_incr ind_set env prev2 prev1 stmt] returns the |
---|
[1462] | 681 | requirements and the cost of the statement [stmt] of the function [fun_name] |
---|
| 682 | in the environment [env] when [cost_incr] is the name of the cost update |
---|
[1508] | 683 | function, [ind_set] is the set of loop indices encountered at this point |
---|
| 684 | (which will be at most a singleton until nested loops are not supported) |
---|
| 685 | and [prev2] and [prev1] are the (optional) previous statements. *) |
---|
[1462] | 686 | |
---|
[1508] | 687 | let rec stmt_cost fun_name cost_incr ind_set env prev2 prev1 stmt |
---|
[1462] | 688 | : require list * Cost_value.t = |
---|
[1508] | 689 | let block_cost block = block_cost fun_name cost_incr ind_set env block in |
---|
[1462] | 690 | |
---|
| 691 | let rec aux stmt = match stmt.Cil_types.skind with |
---|
| 692 | | Cil_types.Instr instr -> ([], instr_cost cost_incr instr) |
---|
| 693 | |
---|
| 694 | | Cil_types.Goto (stmt_ref, _) -> goto_cost !stmt_ref |
---|
| 695 | |
---|
[1508] | 696 | | Cil_types.If (e, block1, block2, _) -> |
---|
[1462] | 697 | let (requires1, cost1) = block_cost block1 in |
---|
| 698 | let (requires2, cost2) = block_cost block2 in |
---|
[1508] | 699 | let cost = |
---|
| 700 | match Cost_value.mk_cost_cond e with |
---|
| 701 | | Some (ind, cost_cond) when List.mem ind ind_set -> |
---|
| 702 | Cost_value.CostCond (ind, cost_cond, cost1, cost2) |
---|
| 703 | | _ -> Cost_value.max cost1 cost2 in |
---|
| 704 | (requires1 @ requires2, cost) |
---|
[1462] | 705 | |
---|
| 706 | | Cil_types.Loop (_, block, _, _, _) -> |
---|
| 707 | (* if has_loop block then raise Nested_loops |
---|
[1508] | 708 | else *) loop_cost fun_name cost_incr ind_set env prev2 prev1 block |
---|
[1462] | 709 | |
---|
| 710 | | Cil_types.Block block -> block_cost block |
---|
| 711 | |
---|
| 712 | | Cil_types.Return _ | Cil_types.Break _ | Cil_types.Continue _ -> |
---|
| 713 | ([], Cost_value.Int 0) |
---|
| 714 | |
---|
| 715 | | Cil_types.Switch _ -> raise (Unsupported "switch") |
---|
| 716 | |
---|
[1508] | 717 | | Cil_types.UnspecifiedSequence l -> |
---|
| 718 | (* not interested in execution order, costs should reflect the |
---|
| 719 | particular order chosen by the compiler *) |
---|
| 720 | block_cost (Cil.block_from_unspecified_sequence l) |
---|
[1462] | 721 | |
---|
| 722 | | Cil_types.TryFinally _ -> raise (Unsupported "try finally") |
---|
| 723 | |
---|
| 724 | | Cil_types.TryExcept _ -> raise (Unsupported "try except") in |
---|
| 725 | |
---|
| 726 | aux stmt |
---|
| 727 | |
---|
[1508] | 728 | (** [block_cost fun_name cost_incr ind_set env block] returns the requirements |
---|
| 729 | and the cost of the block [block] of the function [fun_name] in the |
---|
| 730 | environment [env] when [cost_incr] is the name of the cost update function |
---|
| 731 | and [ind_set] is the set of loop indices whose scope we are in. *) |
---|
[1462] | 732 | |
---|
[1508] | 733 | and block_cost fun_name cost_incr ind_set env block |
---|
| 734 | : require list * Cost_value.t = |
---|
| 735 | let f (prev2, prev1, requires, cost) stmt = |
---|
[1462] | 736 | let (added_requires, added_cost) = |
---|
[1508] | 737 | stmt_cost fun_name cost_incr ind_set env prev2 prev1 stmt in |
---|
| 738 | (prev1, Some stmt, |
---|
[1462] | 739 | requires @ added_requires, |
---|
[1508] | 740 | Cost_value.add cost added_cost) in |
---|
| 741 | let (_, _, requires, cost) = |
---|
| 742 | List.fold_left f (None,None,[],Cost_value.Int 0) block.Cil_types.bstmts in |
---|
[1462] | 743 | (requires, cost) |
---|
| 744 | |
---|
[1508] | 745 | (** [loop_infos fun_name cost_incr ind_set env prev2 prev1 block] returns all |
---|
| 746 | the extracted cost information of a loop in function [fun_name], in |
---|
| 747 | environment [env], with [cost_incr] for the name of the cost update |
---|
| 748 | function and [ind_set] for the loop indexes whose scope we are in, with |
---|
| 749 | (optional) previous statements [prev2], [prev1] and of body [block]. The |
---|
[1462] | 750 | returned information are: the requirements for the loop termination, the |
---|
[1508] | 751 | loop counter, the loop index, its first value, the comparison relation of |
---|
| 752 | the guard, the compared value in the guard, the increment and a function |
---|
| 753 | that, provided a current value for the loop counter, returns the current |
---|
| 754 | cost of the loop. *) |
---|
[1462] | 755 | |
---|
[1508] | 756 | and loop_infos fun_name cost_incr ind_set env prev2 prev1 block |
---|
| 757 | : require list * string * string * Cost_value.t * Cost_value.relation * |
---|
[1462] | 758 | Cost_value.t * Cost_value.t * (Cost_value.t -> Cost_value.t) = |
---|
[1508] | 759 | let (counter, index, init_value) = extract_counter_and_init prev2 prev1 in |
---|
| 760 | let ind_set = index :: ind_set in |
---|
[1462] | 761 | let (rel, exit_value) = extract_guard counter block in |
---|
[1508] | 762 | let increment = extract_increment counter index block in |
---|
[1462] | 763 | check_supported_loop |
---|
| 764 | fun_name env counter init_value exit_value increment block ; |
---|
[1508] | 765 | let (requires, body_cost) = block_cost fun_name cost_incr ind_set env block in |
---|
| 766 | let requires = (rel, init_value, exit_value, increment) :: requires in |
---|
| 767 | let cost = mk_loop_cost init_value increment index body_cost in |
---|
| 768 | (requires, counter, index, init_value, rel, exit_value, increment, cost) |
---|
[1462] | 769 | |
---|
[1508] | 770 | (** [loop_cost fun_name cost_incr ind_set env prev2 prev1 block] returns the |
---|
[1462] | 771 | requirements and the cost of the loop of body [block] in the function |
---|
| 772 | [fun_name] in the environment [env] when [cost_incr] is the name of the cost |
---|
[1508] | 773 | update function, [ind_set] is the set of loop indexes whose scope we are in |
---|
| 774 | and [prev2] and [prev1] are the (optional) previous statements. *) |
---|
[1462] | 775 | |
---|
[1508] | 776 | and loop_cost fun_name cost_incr ind_set env prev2 prev1 block |
---|
[1462] | 777 | : require list * Cost_value.t = |
---|
[1508] | 778 | let (requires, _, _, init_value, rel, exit_value, increment, cost) = |
---|
| 779 | loop_infos fun_name cost_incr ind_set env prev2 prev1 block in |
---|
[1462] | 780 | let cost = cost (last_value rel init_value exit_value increment) in |
---|
| 781 | let cost = |
---|
| 782 | Cost_value.Cond (init_value, rel, exit_value, cost, Cost_value.Int 0) in |
---|
| 783 | (requires, cost) |
---|
| 784 | |
---|
| 785 | |
---|
| 786 | (*** Costs computation ***) |
---|
| 787 | |
---|
| 788 | (* Once a cost (that may depend on the cost of the other functions) has been |
---|
| 789 | associated to each function of a program, we want to simplify them in order |
---|
| 790 | to have independent costs. To this end, we simply apply a fixpoint where at |
---|
| 791 | each step, the independent cost of a function is replaced in the cost of |
---|
| 792 | whatever function mentions it. For exampe, in the following configuration: |
---|
| 793 | cost of f(x) <= x*x + 3 |
---|
| 794 | cost of g() <= cost of h() |
---|
| 795 | cost of h(y) <= -1 + cost of f(y) |
---|
| 796 | then a step of the fixpoint will lead to: |
---|
| 797 | cost of f(x) <= x*x + 3 |
---|
| 798 | cost of g() <= cost of h() |
---|
| 799 | cost of h(y) <= -1 + y*y + 3 *) |
---|
| 800 | |
---|
| 801 | (** [is_solved costs] returns true iff the system of inequations formed by the |
---|
| 802 | costs [costs] is solved, i.e. if every cost is independent of the others and |
---|
| 803 | does not mention to special cost value [Any]. *) |
---|
| 804 | |
---|
| 805 | let is_solved costs = |
---|
| 806 | let f _ cost res = |
---|
| 807 | res && (Cost_value.is_independent cost) && |
---|
| 808 | (not (Cost_value.has_any cost)) in |
---|
| 809 | StringTools.Map.fold f costs true |
---|
| 810 | |
---|
| 811 | (** [solve_end costs1 costs2] returns true iff a fixpoint has been reached, |
---|
| 812 | i.e. if the costs [costs2] of the current iteration are the same as the |
---|
| 813 | costs [costs1] of the previous iteration. *) |
---|
| 814 | |
---|
| 815 | let solve_end costs1 costs2 = |
---|
| 816 | let f fun_name cost res = |
---|
| 817 | res && (StringTools.Map.mem fun_name costs1) && |
---|
| 818 | (cost = StringTools.Map.find fun_name costs1) in |
---|
| 819 | StringTools.Map.fold f costs2 true |
---|
| 820 | |
---|
| 821 | (** [solve_costs extern_costs prototypes costs] solves the system of inequations |
---|
| 822 | formed by the costs [costs]. It applies a reduction operation until a |
---|
| 823 | fixpoint is reached. *) |
---|
| 824 | |
---|
| 825 | let rec solve_costs extern_costs prototypes costs = |
---|
| 826 | let costs' = Cost_value.reduces extern_costs costs prototypes costs in |
---|
| 827 | if solve_end costs costs' then |
---|
| 828 | if is_solved costs' then costs' |
---|
| 829 | else raise Unresolvable |
---|
| 830 | else solve_costs extern_costs prototypes costs' |
---|
| 831 | |
---|
| 832 | class compute_costs cost_incr env costs prj = object |
---|
| 833 | inherit Visitor.frama_c_copy prj as super |
---|
| 834 | |
---|
| 835 | method vfunc fundec = |
---|
| 836 | let fun_name = fundec.Cil_types.svar.Cil_types.vname in |
---|
| 837 | let block = fundec.Cil_types.sbody in |
---|
[1508] | 838 | let cost = block_cost fun_name cost_incr [] env block in |
---|
[1462] | 839 | costs := StringTools.Map.add fun_name cost !costs ; |
---|
| 840 | Cil.SkipChildren |
---|
| 841 | |
---|
| 842 | end |
---|
| 843 | |
---|
| 844 | (** [compute_costs extern_costs cost_incr env] computes the cost associated to |
---|
| 845 | each function of the current program in the current project. First, it |
---|
| 846 | computes the costs potentially depending on that of the other functions, and |
---|
| 847 | then it tries to solve the system of inequations that this produces. *) |
---|
| 848 | |
---|
| 849 | let compute_costs extern_costs cost_incr env |
---|
| 850 | : (require list * Cost_value.t) StringTools.Map.t = |
---|
| 851 | let costs : (require list * Cost_value.t) StringTools.Map.t ref = |
---|
| 852 | ref StringTools.Map.empty in |
---|
| 853 | let compute_costs_prj = |
---|
| 854 | File.create_project_from_visitor |
---|
| 855 | "cerco_compute_costs" |
---|
| 856 | (new compute_costs cost_incr env costs) in |
---|
| 857 | let f () = |
---|
| 858 | let (requires, costs) = StringTools.Map.split_couple !costs in |
---|
| 859 | let costs = solve_costs extern_costs (prototypes env) costs in |
---|
| 860 | StringTools.Map.combine requires costs in |
---|
| 861 | Project.on compute_costs_prj f () |
---|
| 862 | |
---|
| 863 | |
---|
| 864 | (*** Add annotations ***) |
---|
| 865 | |
---|
[1508] | 866 | let add_tmp_cost_init env tmp_cost obj stmt = |
---|
[1462] | 867 | let lval = Cil.var tmp_cost in |
---|
| 868 | let e = |
---|
| 869 | Cil.new_exp dummy_location |
---|
| 870 | (Cil_types.Lval (Cil.var (get_cost_varinfo env))) in |
---|
| 871 | let new_stmt = |
---|
| 872 | Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in |
---|
| 873 | let new_stmt = Cil.mkStmt new_stmt in |
---|
[1508] | 874 | obj#chop_index ; |
---|
[1462] | 875 | Cil.mkStmt (Cil_types.Block (Cil.mkBlock [new_stmt ; stmt])) |
---|
| 876 | |
---|
[1508] | 877 | (* will transform requirements (rel, init_value, exit_value, increment) *) |
---|
| 878 | (* into (init_value rel exit_value) ⇒ (increment rel' 0) where rel' is *) |
---|
| 879 | (* the strict version of rel. If this requirement is trivially satisfied *) |
---|
| 880 | (* it is suppressed *) |
---|
[1462] | 881 | let make_requires requires = |
---|
[1508] | 882 | let f (rel, init_value, exit_value, increment) reqs = |
---|
[1462] | 883 | let rel' = Cost_value.mk_strict rel in |
---|
[1508] | 884 | match init_value, exit_value, increment with |
---|
| 885 | | _, _, Cost_value.Int i |
---|
| 886 | when Cost_value.bool_fun_of_relation rel' 0 i -> |
---|
| 887 | reqs |
---|
| 888 | | Cost_value.Int i, Cost_value.Int e, _ |
---|
| 889 | when not (Cost_value.bool_fun_of_relation rel i e) -> |
---|
| 890 | reqs |
---|
| 891 | | _ -> |
---|
| 892 | let rel = Cost_value.cil_rel_of_rel rel in |
---|
| 893 | let rel' = Cost_value.cil_rel_of_rel rel' in |
---|
| 894 | let init_value = Cost_value.to_cil_term init_value in |
---|
| 895 | let exit_value = Cost_value.to_cil_term exit_value in |
---|
| 896 | let increment = Cost_value.to_cil_term increment in |
---|
| 897 | let t1 = Logic_const.prel (rel, init_value, exit_value) in |
---|
| 898 | let t2 = Logic_const.prel (rel', Cost_value.tinteger 0, increment) in |
---|
| 899 | Logic_const.pimplies (t1, t2) :: reqs in |
---|
| 900 | List.fold_right f requires [] |
---|
[1462] | 901 | |
---|
| 902 | let add_spec pres post spec = |
---|
| 903 | let requires = List.map Logic_const.new_predicate pres in |
---|
| 904 | let post_cond = [(Cil_types.Normal, Logic_const.new_predicate post)] in |
---|
| 905 | let new_behavior = Cil.mk_behavior ~requires ~post_cond () in |
---|
| 906 | spec.Cil_types.spec_behavior <- new_behavior :: spec.Cil_types.spec_behavior |
---|
| 907 | |
---|
| 908 | let add_cost_annotation requires rel cost_id cost spec = |
---|
| 909 | let post = mk_fun_cost_pred rel cost_id cost in |
---|
| 910 | add_spec (make_requires requires) post spec ; |
---|
| 911 | Cil.ChangeDoChildrenPost (spec, identity) |
---|
| 912 | |
---|
| 913 | let add_cost_incr_annotation cost_id spec = |
---|
| 914 | let rel = Cil_types.Req in |
---|
| 915 | let cost = Cost_value.Var "incr" in |
---|
| 916 | add_cost_annotation [] rel cost_id cost spec |
---|
| 917 | |
---|
| 918 | let add_regular_fun_annotation fun_name cost_id costs spec = |
---|
| 919 | let rel = Cil_types.Rle in |
---|
| 920 | let (requires, cost) = StringTools.Map.find fun_name costs in |
---|
| 921 | add_cost_annotation requires rel cost_id cost spec |
---|
| 922 | |
---|
| 923 | let add_fundec_annotation cost_id cost_incr costs fun_name spec = |
---|
| 924 | if fun_name = cost_incr then add_cost_incr_annotation cost_id spec |
---|
| 925 | else add_regular_fun_annotation fun_name cost_id costs spec |
---|
| 926 | |
---|
| 927 | let mk_loop_invariant_counter_init_value |
---|
| 928 | extern_costs costs prots counter init_value increment = |
---|
| 929 | let mk_value value = |
---|
| 930 | let incr_mod = Cost_value.abs increment in |
---|
| 931 | let v = Cost_value.BinOp (Cost_value.Mod, value, incr_mod) in |
---|
| 932 | Cost_value.to_cil_term (Cost_value.reduce extern_costs costs prots v) in |
---|
| 933 | let v1 = mk_value (Cost_value.Var counter) in |
---|
| 934 | let v2 = mk_value init_value in |
---|
| 935 | let invariant = Logic_const.prel (Cil_types.Req, v1, v2) in |
---|
| 936 | mk_invariant invariant |
---|
| 937 | |
---|
| 938 | let mk_loop_invariant_counter_last_value |
---|
| 939 | extern_costs costs prots counter rel init_value exit_value increment = |
---|
| 940 | let last_value = last_value rel init_value exit_value increment in |
---|
| 941 | let last_value = Cost_value.reduce extern_costs costs prots last_value in |
---|
| 942 | let last_value = Cost_value.to_cil_term last_value in |
---|
| 943 | let rel' = Cost_value.cil_rel_of_rel rel in |
---|
| 944 | let init_value = Cost_value.to_cil_term init_value in |
---|
| 945 | let exit_value = Cost_value.to_cil_term exit_value in |
---|
| 946 | let require = Logic_const.prel (rel', init_value, exit_value) in |
---|
| 947 | let rel' = Cost_value.cil_rel_of_rel (Cost_value.mk_large rel) in |
---|
| 948 | let counter = Cost_value.to_cil_term (Cost_value.Var counter) in |
---|
| 949 | let prop = Logic_const.prel (rel', counter, last_value) in |
---|
| 950 | let invariant = Logic_const.pimplies (require, prop) in |
---|
| 951 | mk_invariant invariant |
---|
| 952 | |
---|
| 953 | let mk_loop_invariant_counter_no_change counter rel init_value exit_value = |
---|
| 954 | let rel = Cost_value.opposite rel in |
---|
| 955 | let rel' = Cost_value.cil_rel_of_rel rel in |
---|
| 956 | let init_value = Cost_value.to_cil_term init_value in |
---|
| 957 | let exit_value = Cost_value.to_cil_term exit_value in |
---|
| 958 | let require = Logic_const.prel (rel', init_value, exit_value) in |
---|
| 959 | let counter = Cost_value.to_cil_term (Cost_value.Var counter) in |
---|
| 960 | let prop = Logic_const.prel (Cil_types.Req, counter, init_value) in |
---|
| 961 | let invariant = Logic_const.pimplies (require, prop) in |
---|
| 962 | mk_invariant invariant |
---|
| 963 | |
---|
| 964 | let mk_loop_invariant_cost |
---|
| 965 | extern_costs tmp_cost costs prots cost_id counter cost = |
---|
| 966 | let loop_cost = cost (Cost_value.Var counter) in |
---|
| 967 | let loop_cost = Cost_value.reduce extern_costs costs prots loop_cost in |
---|
| 968 | let loop_cost = Cost_value.to_cil_term loop_cost in |
---|
| 969 | let cost_var = |
---|
| 970 | Logic_const.tvar (Cil_const.make_logic_var cost_id Cil_types.Linteger) in |
---|
| 971 | let tmp_cost = Cost_value.to_cil_term (Cost_value.Var tmp_cost) in |
---|
| 972 | let new_cost = Cil_types.TBinOp (Cil_types.PlusA, tmp_cost, loop_cost) in |
---|
| 973 | let new_cost = integer_term new_cost in |
---|
| 974 | let invariant = Logic_const.prel (Cil_types.Rle, cost_var, new_cost) in |
---|
| 975 | mk_invariant invariant |
---|
| 976 | |
---|
| 977 | let mk_loop_variant |
---|
| 978 | extern_costs costs prots counter init_value rel exit_value increment = |
---|
| 979 | let last_value = last_value rel init_value exit_value increment in |
---|
| 980 | let counter_var = Cost_value.Var counter in |
---|
| 981 | let (v1, v2) = match rel with |
---|
| 982 | | Cost_value.Lt | Cost_value.Le -> (last_value, counter_var) |
---|
| 983 | | Cost_value.Gt | Cost_value.Ge -> (counter_var, last_value) in |
---|
| 984 | let variant = Cost_value.BinOp (Cost_value.Sub, v1, v2) in |
---|
| 985 | let variant = Cost_value.reduce extern_costs costs prots variant in |
---|
| 986 | mk_variant (Cost_value.to_cil_term variant) |
---|
| 987 | |
---|
| 988 | let annot_loop |
---|
| 989 | extern_costs tmp_cost cost_id cost_incr env costs obj stmt |
---|
[1508] | 990 | prev2 prev1 block = |
---|
[1462] | 991 | let (_, costs) = StringTools.Map.split_couple costs in |
---|
| 992 | let prots = prototypes env in |
---|
| 993 | let fun_name = current_fun_name obj in |
---|
[1508] | 994 | let (_, counter, index, init_value, rel, exit_value, increment, cost) = |
---|
| 995 | loop_infos fun_name cost_incr obj#get_ind_set env prev2 prev1 block in |
---|
[1462] | 996 | let invariant_counter_init_value = |
---|
| 997 | mk_loop_invariant_counter_init_value |
---|
| 998 | extern_costs costs prots counter init_value increment in |
---|
| 999 | let invariant_counter_last_value = |
---|
| 1000 | mk_loop_invariant_counter_last_value |
---|
| 1001 | extern_costs costs prots counter rel init_value exit_value increment in |
---|
| 1002 | let invariant_counter_no_change = |
---|
| 1003 | mk_loop_invariant_counter_no_change counter rel init_value exit_value in |
---|
| 1004 | let invariant_cost = |
---|
[1689] | 1005 | mk_loop_invariant_cost extern_costs tmp_cost costs prots cost_id |
---|
[1462] | 1006 | counter cost in |
---|
| 1007 | let variant = |
---|
| 1008 | mk_loop_variant extern_costs costs prots counter init_value rel exit_value |
---|
| 1009 | increment in |
---|
[1508] | 1010 | obj#push_index index; |
---|
[1462] | 1011 | add_loop_annot obj stmt invariant_counter_init_value ; |
---|
| 1012 | add_loop_annot obj stmt invariant_counter_last_value ; |
---|
| 1013 | add_loop_annot obj stmt invariant_counter_no_change ; |
---|
| 1014 | add_loop_annot obj stmt invariant_cost ; |
---|
| 1015 | add_loop_annot obj stmt variant |
---|
| 1016 | |
---|
| 1017 | class add_annotations extern_costs cost_id cost_incr env costs prj = |
---|
| 1018 | object (self) inherit Visitor.frama_c_copy prj as super |
---|
| 1019 | |
---|
| 1020 | val mutable tmp_costs : Cil_types.varinfo list = [] |
---|
[1508] | 1021 | val mutable prev2 = None |
---|
| 1022 | val mutable prev1 = None |
---|
| 1023 | val mutable ind_set : string list = [] |
---|
[1462] | 1024 | |
---|
[1508] | 1025 | method get_ind_set = ind_set |
---|
| 1026 | method push_index index = ind_set <- index :: ind_set |
---|
| 1027 | method chop_index = ind_set <- List.tl ind_set |
---|
| 1028 | |
---|
[1462] | 1029 | method vstmt_aux stmt = |
---|
[1508] | 1030 | let snd_last_stmt = prev2 in |
---|
| 1031 | let last_stmt = prev1 in |
---|
| 1032 | prev2 <- last_stmt ; |
---|
| 1033 | prev1 <- Some stmt ; |
---|
[1462] | 1034 | match stmt.Cil_types.skind with |
---|
| 1035 | | Cil_types.Loop (_, block, _, _, _) -> |
---|
| 1036 | assert (List.length tmp_costs > 0) ; |
---|
| 1037 | let tmp_cost = List.hd tmp_costs in |
---|
| 1038 | tmp_costs <- List.tl tmp_costs ; |
---|
| 1039 | let tmp_cost_id = tmp_cost.Cil_types.vname in |
---|
| 1040 | annot_loop |
---|
| 1041 | extern_costs tmp_cost_id cost_id cost_incr env costs self stmt |
---|
[1508] | 1042 | snd_last_stmt last_stmt block ; |
---|
| 1043 | Cil.ChangeDoChildrenPost (stmt, add_tmp_cost_init env tmp_cost self) |
---|
[1462] | 1044 | | _ -> Cil.DoChildren |
---|
| 1045 | |
---|
| 1046 | method vspec spec = match self#current_kf with |
---|
| 1047 | | None -> Cil.JustCopy |
---|
| 1048 | | Some kf -> |
---|
| 1049 | match kf.Db_types.fundec with |
---|
| 1050 | | Db_types.Definition (fundec, _) -> |
---|
| 1051 | let fun_name = fundec.Cil_types.svar.Cil_types.vname in |
---|
| 1052 | add_fundec_annotation cost_id cost_incr costs fun_name spec |
---|
| 1053 | | Db_types.Declaration (_, f, _, _) when |
---|
| 1054 | StringTools.Map.mem f.Cil_types.vname extern_costs -> |
---|
| 1055 | let cost = StringTools.Map.find f.Cil_types.vname extern_costs in |
---|
| 1056 | let cost = Cost_value.Var cost in |
---|
| 1057 | add_cost_annotation [] Cil_types.Rle cost_id cost spec |
---|
| 1058 | | _ -> Cil.JustCopy |
---|
| 1059 | |
---|
| 1060 | method vfunc fundec = |
---|
| 1061 | let fun_name = fundec.Cil_types.svar.Cil_types.vname in |
---|
| 1062 | tmp_costs <- make_freshes fundec (get_nb_loops env fun_name) cost_id ; |
---|
[1508] | 1063 | prev2 <- None ; |
---|
| 1064 | prev1 <- None ; |
---|
[1462] | 1065 | Cil.DoChildren |
---|
| 1066 | |
---|
| 1067 | end |
---|
| 1068 | |
---|
| 1069 | let add_annotations extern_costs fname cost_id cost_incr env costs = |
---|
[1508] | 1070 | let add_annotations_prj = |
---|
| 1071 | let visitor = |
---|
| 1072 | new add_annotations extern_costs cost_id cost_incr env costs in |
---|
| 1073 | File.create_project_from_visitor "cerco_add_annotations" |
---|
| 1074 | (visitor :> Project.t -> Visitor.frama_c_visitor) in |
---|
[1462] | 1075 | let f () = |
---|
| 1076 | Parameters.CodeOutput.set fname ; |
---|
| 1077 | File.pretty_ast () in |
---|
| 1078 | Project.on add_annotations_prj f () |
---|
| 1079 | |
---|
| 1080 | |
---|
| 1081 | (*** Saving cost results ***) |
---|
| 1082 | |
---|
| 1083 | let save_results fname costs = |
---|
| 1084 | let f fun_name (_, cost) res = |
---|
| 1085 | res ^ fun_name ^ " " ^ (Cost_value.to_string cost) ^ "\n" in |
---|
| 1086 | let s = StringTools.Map.fold f costs "" in |
---|
| 1087 | let save_file = |
---|
| 1088 | try Filename.chop_extension fname |
---|
| 1089 | with Invalid_argument "Filename.chop_extension" -> fname in |
---|
| 1090 | let save_file = save_file ^ ".cost_results" in |
---|
| 1091 | try |
---|
| 1092 | let oc = open_out save_file in |
---|
| 1093 | output_string oc s ; |
---|
| 1094 | close_out oc |
---|
| 1095 | with Sys_error _ -> |
---|
| 1096 | Printf.eprintf "Could not save plug-in results in file %s\n%!" save_file |
---|
| 1097 | |
---|
| 1098 | |
---|
| 1099 | (*** Main ***) |
---|
| 1100 | |
---|
| 1101 | let cost ((fname, _), f_old_name, cost_id, cost_incr, extern_costs) = |
---|
| 1102 | try |
---|
| 1103 | Parameters.Files.set [fname] ; |
---|
| 1104 | File.init_from_cmdline () ; |
---|
| 1105 | let env = initializations cost_id in |
---|
| 1106 | let costs = compute_costs extern_costs cost_incr env in |
---|
| 1107 | save_results f_old_name costs ; |
---|
| 1108 | add_annotations extern_costs fname cost_id cost_incr env costs |
---|
| 1109 | with e -> Printf.eprintf "** ERROR: %s\n%!" (string_of_exception cost_incr e) |
---|