Changeset 1679 for Deliverables/D5.1-5.3/cost-plug-in
- Timestamp:
- Feb 7, 2012, 6:01:43 PM (9 years ago)
- Location:
- Deliverables/D5.1-5.3/cost-plug-in
- Files:
-
- 10 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D5.1-5.3/cost-plug-in/Makefile
r1462 r1679 1 1 PACKAGE=cost-plug-in 2 2 PACKAGE_RES=$(PACKAGE).tgz 3 4 JESSIE=frama-c_jessie 3 5 4 6 all: … … 7 9 8 10 install: 11 mkdir -p /usr/local/bin 12 cp $(JESSIE) /usr/local/bin/ 9 13 make -C plugin install 10 14 make -C wrapper install -
Deliverables/D5.1-5.3/cost-plug-in/README
r1462 r1679 11 11 - CerCo 12 12 - Lustre compiler (for Lustre files only) 13 - Jessie plug-in and simplify (for verification o f Lustre files only)13 - Jessie plug-in and simplify (for verification only) 14 14 15 15 Compilation … … 33 33 Note: both the plug-in and the wrapper can be installed seperately. See their 34 34 README in their respective source folders ("plugin" for the plug-in and 35 "wrapper" for the Lustre wrapper). Note that the wrapper uses the plug-in.35 "wrapper" for the Lustre wrapper). Also note that the wrapper uses the plug-in. 36 36 37 37 Usage … … 66 66 67 67 % frama-c_lustre -help 68 69 - Jessie script 70 71 For verification through a graphical user interface, a script that calls the 72 Jessie plug-in of Frama-C with specific options is also provided. It can be 73 ran using the following command on an annotated C file (obtained with the 74 Cost plug-in for instance): 75 76 % frama-c_jessie annotated-file.c -
Deliverables/D5.1-5.3/cost-plug-in/distributed_files
r1462 r1679 2 2 README 3 3 distributed_files 4 frama-c_jessie 4 5 plugin/ 5 6 plugin/Makefile 6 7 plugin/README 8 plugin/arith.ml 9 plugin/arithSig.ml 7 10 plugin/cerco.ml 11 plugin/completeMap.ml 8 12 plugin/compute.ml 9 13 plugin/cost.ml 10 14 plugin/cost_value.ml 11 plugin/help/ 12 plugin/help/mailinglisthelp 13 plugin/stringTools.ml 15 plugin/emap.ml 16 plugin/eset.ml 17 plugin/misc.ml 18 plugin/multiset.ml 14 19 plugin/tests/ 15 plugin/tests/bubble_sort.c 20 plugin/tests/fail/ 21 plugin/tests/fail/blowfish.c 22 plugin/tests/fail/blowfish.h 23 plugin/tests/fail/bubble_sort.c 24 plugin/tests/success/ 25 plugin/tests/success/3-way.c 26 plugin/tests/success/LFSR.C 27 plugin/tests/success/LFSR2.C 28 plugin/tests/success/a5.c 29 plugin/tests/success/fact.c 30 plugin/tests/success/is_sorted.c 31 plugin/tests/success/random.c 32 plugin/tests/success/tab_sum.c 16 33 wrapper/ 17 34 wrapper/Makefile -
Deliverables/D5.1-5.3/cost-plug-in/plugin/Makefile
r1462 r1679 27 27 28 28 PLUGIN_NAME = Cost_synthesis 29 PLUGIN_CMO = stringTools cost_value compute cerco cost 29 PLUGIN_CMO = eset emap completeMap multiset misc arithSig arith \ 30 cost_value compute cerco cost 30 31 31 32 # PLUGIN_HAS_MLI := yes -
Deliverables/D5.1-5.3/cost-plug-in/plugin/cerco.ml
r1462 r1679 11 11 let fun_name = String.sub s 0 i in 12 12 let var_name = String.sub s (i+1) (String.length s - (i+1)) in 13 StringTools.Map.add fun_name var_name (extern_cost_variables cin)14 with End_of_file -> StringTools.Map.empty13 Misc.String.Map.add fun_name var_name (extern_cost_variables cin) 14 with End_of_file -> Misc.String.Map.empty 15 15 16 16 (** [multifile_exists exts filename] returns true if and only if the file name … … 56 56 57 57 let apply lustre_option lustre_verify_option lustre_test_option (filename, _) 58 : Cabs.file * string * string * string * string StringTools.Map.t =58 : Cabs.file * string * string * string * string Misc.String.Map.t = 59 59 let annotated_ext = "-annotated.c" in 60 60 let asm_ext = ".s" in -
Deliverables/D5.1-5.3/cost-plug-in/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 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 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 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." 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 (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 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 (n-1)) @ [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 Frama-C'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 (* Frama-C 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 Frama-C, 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 do-while 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 plug-in results in file %s \n%!" save_file2243 Printf.eprintf "Could not save plug-in 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) -
Deliverables/D5.1-5.3/cost-plug-in/plugin/cost.ml
r1462 r1679 28 28 Plugin.Register 29 29 (struct 30 let name = " Cost synthesis"30 let name = "cost synthesis" 31 31 let shortname = "cost" 32 32 let module_name = "Cost.Self" 33 let help = " Synthesis of the execution cost of each function"33 let help = "synthesis of the execution cost of each function" 34 34 let is_dynamic = true 35 35 end) … … 78 78 let files : Cabs.file list = Ast.UntypedFiles.get () in 79 79 let files : 80 (Cabs.file * string * string * string * string StringTools.Map.t) list =80 (Cabs.file * string * string * string * string Misc.String.Map.t) list = 81 81 List.map 82 82 (Cerco.apply lustre_option lustre_verify_option lustre_test_option) 83 83 files in 84 Compute.debug := Self.Debug.get () <> 0 ; 84 85 List.iter Compute.cost files 85 86 -
Deliverables/D5.1-5.3/cost-plug-in/plugin/cost_value.ml
r1462 r1679 2 2 (** This module describes the values manipulated by the plug-in. *) 3 3 4 5 type relation = Lt | Gt | Le | Ge6 7 let string_of_relation = function8 | Lt -> "<"9 | Le -> "<="10 | Gt -> ">"11 | Ge -> ">="12 13 let bool_fun_of_relation = function14 | Lt -> (<)15 | Le -> (<=)16 | Gt -> (>)17 | Ge -> (>=)18 19 let mk_strict = function20 | Lt | Le -> Lt21 | Gt | Ge -> Gt22 23 let mk_large = function24 | Lt | Le -> Le25 | Gt | Ge -> Ge26 27 let opposite = function28 | Lt -> Ge29 | Le -> Gt30 | Gt -> Le31 | Ge -> Lt32 33 type unop = Neg34 35 let string_of_unop = function36 | Neg -> "-"37 38 let int_fun_of_unop = function39 | Neg -> (fun x -> (-x))40 41 type binop = Add | Sub | Div | Mul | Mod | Max42 43 let string_of_binop = function44 | Add -> "+"45 | Sub -> "-"46 | Div -> "/"47 | Mul -> "*"48 | Mod -> "%"49 | Max -> "max"50 51 let int_fun_of_binop = function52 | Add -> (+)53 | Sub -> (-)54 | Div -> (/)55 | Mul -> ( * )56 | Mod -> (mod)57 | Max -> max58 59 (** Cost values *)60 61 type t =62 | Int of int63 | Var of string (* either a parameter or a global, but not a local *)64 | UnOp of unop * t65 | BinOp of binop * t * t66 | Cond of t * relation * t * t * t (* ternary expressions *)67 | CostOf of string * t list (* cost of a function: function name * args *)68 | Any (* any other C expression *)69 70 (** [abs v] return a cost value that represents the absolute value of [v]. *)71 72 let abs v = Cond (Int 0, Le, v, v, UnOp (Neg, v))73 74 75 (** [subs v] returns the sub-values of the cost value [v]. *)76 77 let subs = function78 | Int _ | Var _ | Any -> []79 | UnOp (_, v) -> [v]80 | BinOp (_, v1, v2) -> [v1 ; v2]81 | Cond (t1, _, t2, tif, telse) -> [t1 ; t2 ; tif ; telse]82 | CostOf (_, args) -> args83 84 (** [fill_subs s subs] replaces the sub-values of the cost value [v] with85 those in [subs]. *)86 87 let fill_subs v subs = match v, subs with88 | Int _, _ | Var _, _ | Any, _ -> v89 | UnOp (unop, _), v :: _ -> UnOp (unop, v)90 | BinOp (binop, _, _), v1 :: v2 :: _ -> BinOp (binop, v1, v2)91 | Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ ->92 Cond (t1, rel, t2, tif, telse)93 | CostOf (fun_name, _), _ -> CostOf (fun_name, subs)94 | _ -> raise (Failure "Cost_value.fill_subs") (* wrong number of arguments *)95 96 (** [fold f v] recursively apply the function [f] on the cost value [v] and its97 children, starting from the leaves and going up in the tree. [f]'s type is98 [t -> 'a list -> 'a], where the second argument is the results of the fold99 on [v]'s sub-values. *)100 101 let rec fold (f : t -> 'a list -> 'a) v =102 let subs_res = List.map (fold f) (subs v) in103 f v subs_res104 105 106 let rec f_to_string v subs_res = match v, subs_res with107 | Int i, _ -> string_of_int i108 | Var x, _ -> x109 | UnOp (unop, _), v :: _ -> (string_of_unop unop) ^ "(" ^ v ^ ")"110 | BinOp (binop, _, _), v1 :: v2 :: _ ->111 "(" ^ v1 ^ ")" ^ (string_of_binop binop) ^ "(" ^ v2 ^ ")"112 | Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ ->113 Printf.sprintf "(%s %s %s)? (%s) : (%s)"114 t1 (string_of_relation rel) t2 tif telse115 | CostOf (fun_name, _), args ->116 let f res v = res ^ v ^ ", " in117 fun_name ^ "(" ^ (List.fold_left f "" args) ^ ")"118 | Any, _ -> "any"119 | UnOp _, _ | BinOp _, _ | Cond _, _ ->120 assert false (* wrong number of arguments *)121 122 and to_string v = fold f_to_string v123 124 125 (* Variables of a cost value *)126 127 let union_list l =128 List.fold_left StringTools.Set.union StringTools.Set.empty l129 130 let f_vars v subs_res =131 let v_res = match v with132 | Var x -> StringTools.Set.singleton x133 | _ -> StringTools.Set.empty in134 union_list (v_res :: subs_res)135 136 (** [vars v] returns the set of variables of the cost value [v]. *)137 138 let vars = fold f_vars139 140 141 (* Replace variables by expressions *)142 143 (*144 let f_replace r_list v subs_res =145 let v = match v with146 | Var x when List.mem_assoc x r_list -> List.assoc x r_list147 | _ -> v in148 fill_subs v subs_res149 *)150 151 let f_replace r_list v subs_res = match fill_subs v subs_res with152 | Var x when List.mem_assoc x r_list -> List.assoc x r_list153 | v -> v154 155 (** [replace r_list v] replaces the variables of [v] that are in the association156 list [r_list] with their associated cost value. *)157 158 let replace (r_list : (string * t) list) = fold (f_replace r_list)159 160 161 (* Value reduction (or partial computation) *)162 163 (* Raised when a function is not found in the cost environment *)164 4 exception Unknown_cost of string 165 (* Raised when the prototype of a function is not found *)166 5 exception Unknown_prototype of string 167 6 168 let f_is_independent v subs_res = 169 let v_res = match v with 170 | CostOf _ -> false 171 | _ -> true in 172 List.fold_left (&&) true (v_res :: subs_res) 173 174 (** [is_independent v] returns true if and only if the cost value [v] is 175 independent of the cost of other functions (i.e. does not have a CostOf). *) 176 177 let is_independent = fold f_is_independent 178 179 (* Reduction of a cost in the case of a CostOf construct. Replace the formal 180 parameters of the function by the actual arguments. *) 181 182 let f_reduce_CostOf extern_costs costs prots fun_name args = 183 if StringTools.Map.mem fun_name extern_costs then 184 Var (StringTools.Map.find fun_name extern_costs) 185 else 186 if StringTools.Map.mem fun_name prots then 187 let formals = StringTools.Map.find fun_name prots in 188 if List.length formals = List.length args then 189 let r_list = List.combine formals args in 190 if StringTools.Map.mem fun_name costs then 191 let cost = StringTools.Map.find fun_name costs in 192 if is_independent cost then replace r_list cost 193 else CostOf (fun_name, args) 194 else raise (Unknown_cost fun_name) 7 8 let string_of_mset to_list sep f mset = 9 let filter (_, occ) = occ <> 0 in 10 let f' (elt, occ) = 11 if occ = 1 then (f elt) 12 else Printf.sprintf "%d*%s" occ (f elt) in 13 Misc.List.to_string sep f' (List.filter filter (to_list mset)) 14 15 type prototypes = string list Misc.String.Map.t 16 17 18 module type S = sig 19 20 type relation 21 val is_large : relation -> bool 22 val has_lower_type : relation -> bool 23 24 type t 25 26 val top : t 27 val of_int : int -> t 28 val of_var : string -> t 29 val add : t -> t -> t 30 val minus : t -> t -> t 31 val mul : t -> t -> t 32 val div : t -> t -> t 33 val max : t -> t -> t 34 val cond : t -> relation -> t -> t -> t -> t 35 val join : t -> t -> t 36 val widen : t -> t -> t 37 val narrow : t -> t -> t 38 39 val le : t -> t -> bool 40 41 val replace_vars : t Misc.String.Map.t -> t -> t 42 43 val to_string : t -> string 44 val string_of_relation : relation -> string 45 46 val compare : t -> t -> int 47 48 end 49 50 51 module Make (S : S) = struct 52 53 let s_add_list = function 54 | [] -> S.of_int 0 55 | e :: l -> List.fold_left S.add e l 56 57 module Args = struct 58 59 type t = S.t list 60 61 let compare = Misc.List.compare S.compare 62 63 let le args1 args2 = 64 if List.length args1 <> List.length args2 then false 195 65 else 196 raise 197 (Failure ("Cost_value.f_reduce_CostOf: formals and actuals for " ^ 198 "function " ^ fun_name ^ " have different sizes.")) 199 else raise (Unknown_prototype fun_name) 200 201 (* Reduction in the general case. When some specific patterns are found that 202 allow to perform a computation (for instance when applying an operation to 203 some integer values), return the result. *) 204 205 let f_reduce extern_costs costs prots v subs_res = match v, subs_res with 206 | UnOp (unop, _), (Int i) :: _ -> Int (int_fun_of_unop unop i) 207 | UnOp (Neg, _), (UnOp (Neg, v)) :: _ -> v 208 | BinOp (binop, _, _), (Int i1) :: (Int i2) :: _ -> 209 Int (int_fun_of_binop binop i1 i2) 210 | BinOp (Add, _, _), (BinOp (Add, v, Int i1)) :: (Int i2) :: _ 211 | BinOp (Add, _, _), (BinOp (Add, Int i1, v)) :: (Int i2) :: _ -> 212 BinOp (Add, Int (i1 + i2), v) 213 | BinOp (Add, _, _), v :: (Int 0) :: _ 214 | BinOp (Sub, _, _), v :: (Int 0) :: _ 215 | BinOp (Add, _, _), (Int 0) :: v :: _ 216 | BinOp (Div, _, _), v :: (Int 1) :: _ 217 | BinOp (Mul, _, _), v :: (Int 1) :: _ 218 | BinOp (Mul, _, _), (Int 1) :: v :: _ -> v 219 | BinOp (Sub, _, _), (Int 0) :: v :: _ 220 | BinOp (Div, _, _), v :: (Int (-1)) :: _ 221 | BinOp (Mul, _, _), v :: (Int (-1)) :: _ 222 | BinOp (Mul, _, _), (Int (-1)) :: v :: _ -> UnOp (Neg, v) 223 | BinOp (Div, _, _), (Int 0) :: _ :: _ 224 | BinOp (Mul, _, _), _ :: (Int 0) :: _ 225 | BinOp (Mul, _, _), (Int 0) :: _ :: _ 226 | BinOp (Mod, _, _), (Int 0) :: _ :: _ 227 | BinOp (Mod, _, _), _ :: (Int 1) :: _ -> Int 0 228 | Cond (_, rel, _, _, _), (Int i1) :: (Int i2) :: tif :: _ 229 when bool_fun_of_relation rel i1 i2 -> tif 230 | Cond (_, rel, _, _, _), (Int i1) :: (Int i2) :: _ :: telse :: _ 231 when not (bool_fun_of_relation rel i1 i2) -> telse 232 | CostOf (fun_name, _), args -> 233 f_reduce_CostOf extern_costs costs prots fun_name args 234 | _ -> fill_subs v subs_res 235 236 (** [reduce extern_costs costs prots v] apply a partial computation on the value 237 [v] when considering the cost associated to each function in [costs] and 238 their prototype [prots]. *) 239 240 let reduce 241 (extern_costs : string StringTools.Map.t) 242 (costs : t StringTools.Map.t) 243 (prots : string list StringTools.Map.t) 244 : t -> t = 245 fold (f_reduce extern_costs costs prots) 246 247 (** [reduces extern_costs costs prots costs_to_reduce] applies a cost reduction 248 on every cost in the mapping [costs_to_reduce]. *) 249 250 let reduces 251 (extern_costs : string StringTools.Map.t) 252 (costs : t StringTools.Map.t) 253 (prots : string list StringTools.Map.t) 254 (costs_to_reduce : t StringTools.Map.t) 255 : t StringTools.Map.t = 256 StringTools.Map.map (reduce extern_costs costs prots) costs_to_reduce 257 258 259 (* Raised when an unsupported expression is found. *) 260 exception Unsupported_exp 261 (* Raised when an unsupported comparison relation. *) 262 exception Unsupported_rel 263 264 265 let rel_of_cil_rel = function 266 | Cil_types.Lt -> Lt 267 | Cil_types.Gt -> Gt 268 | Cil_types.Le -> Le 269 | Cil_types.Ge -> Ge 270 | _ -> raise Unsupported_rel 271 272 let cil_rel_of_rel = function 273 | Lt -> Cil_types.Rlt 274 | Gt -> Cil_types.Rgt 275 | Le -> Cil_types.Rle 276 | Ge -> Cil_types.Rge 277 278 let cil_binop_of_rel = function 279 | Lt -> Cil_types.Lt 280 | Gt -> Cil_types.Gt 281 | Le -> Cil_types.Le 282 | Ge -> Cil_types.Ge 283 284 285 let unop_of_cil_unop = function 286 | Cil_types.Neg -> Neg 287 | _ -> raise (Failure "unop_of_cil_unop") 288 289 let binop_of_cil_binop = function 290 | Cil_types.PlusA -> Add 291 | Cil_types.MinusA -> Sub 292 | Cil_types.Mult -> Mul 293 | Cil_types.Div -> Div 294 | Cil_types.Mod -> Mod 295 | _ -> raise (Failure "binop_of_cil_binop") 296 297 (** [of_cil_exp e] returns a cost value equivalent to the CIL expression [e]. *) 298 299 let rec of_cil_exp e = 300 try match e.Cil_types.enode with 301 | Cil_types.Const (Cil_types.CInt64 (i, _, _)) -> Int (Int64.to_int i) 302 | Cil_types.Lval (Cil_types.Var var, _) -> Var (var.Cil_types.vname) 303 | Cil_types.UnOp (unop, e, _) -> UnOp (unop_of_cil_unop unop, of_cil_exp e) 304 | Cil_types.BinOp (binop, e1, e2, _) -> 305 BinOp (binop_of_cil_binop binop, of_cil_exp e1, of_cil_exp e2) 306 | Cil_types.Info (e, _) -> of_cil_exp e 307 | _ -> Any 308 with Failure ("unop_of_cil_unop" | "binop_of_cil_binop") -> Any 309 310 311 let cil_unop_of_unop = function 312 | Neg -> Cil_types.Neg 313 314 let cil_binop_of_binop = function 315 | Add -> Cil_types.PlusA 316 | Sub -> Cil_types.MinusA 317 | Mul -> Cil_types.Mult 318 | Div -> Cil_types.Div 319 | Mod -> Cil_types.Mod 320 (* No direct translation. Handle this case in the calling function. *) 321 | Max -> assert false 322 323 324 let integer_term term = Logic_const.term term Cil_types.Linteger 325 326 let tinteger i = 327 let cint64 = Cil_types.CInt64 (Int64.of_int i, Cil_types.IInt, None) in 328 let iterm = Cil_types.TConst cint64 in 329 integer_term iterm 330 331 let f_to_cil_term v subs_res = match v, subs_res with 332 | Int i, _ -> tinteger i 333 | Var x, _ -> Logic_const.tvar (Cil_const.make_logic_var x Cil_types.Linteger) 334 | UnOp (unop, _), t :: _ -> 335 integer_term (Cil_types.TUnOp (cil_unop_of_unop unop, t)) 336 | UnOp _, _ -> assert false (* wrong number of arguments *) 337 | BinOp (Max, _, _), t1 :: t2 :: _ -> 338 let test = integer_term (Cil_types.TBinOp (Cil_types.Ge, t1, t2)) in 339 integer_term (Cil_types.Tif (test, t1, t2)) 340 | BinOp (binop, _, _), t1 :: t2 :: _ -> 341 integer_term (Cil_types.TBinOp (cil_binop_of_binop binop, t1, t2)) 342 | BinOp _, _ -> assert false (* wrong number of arguments *) 343 | Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ -> 344 let test = integer_term (Cil_types.TBinOp (cil_binop_of_rel rel, t1, t2)) in 345 integer_term (Cil_types.Tif (test, tif, telse)) 346 | Cond _, _ -> assert false (* wrong number of arguments *) 347 | CostOf _, _ -> assert false (* should never be used on these arguments *) 348 | Any, _ -> raise Unsupported_exp 349 350 (** [to_cil_term v] returns a CIL logic term equivalent to the cost value 351 [v]. *) 352 353 let to_cil_term = fold f_to_cil_term 354 355 356 let f_has_locals locals e subs_res = 357 let e_res = match e with 358 | Var x -> StringTools.Set.mem x locals 359 | _ -> false in 360 List.fold_left (||) false (e_res :: subs_res) 361 362 (** [has_locals locals v] returns true if and only if the cost value [v] has a 363 variable in the set [locals]. *) 364 365 let has_locals locals = fold (f_has_locals locals) 366 367 368 let f_has_any e subs_res = List.fold_left (||) false ((e = Any) :: subs_res) 369 370 (** [has_any v] returns true if and only if the cost value [v] has an Any 371 construct. *) 372 373 let has_any = fold f_has_any 66 let f res arg1 arg2 = res && (S.le arg1 arg2) in 67 List.fold_left2 f true args1 args2 68 69 let replace_vars replacements = List.map (S.replace_vars replacements) 70 71 let to_string = Misc.List.to_string ", " S.to_string 72 73 end 74 75 76 module Externs = struct 77 78 module M = Misc.String.MSet 79 include M 80 81 let add = union 82 83 let le = subset 84 85 let replace_vars _ externs = externs 86 87 let to_string = string_of_mset to_list " + " (fun x -> x) 88 89 let to_ext externs = 90 let f x occ ext = S.add (S.mul (S.of_int occ) (S.of_var x)) ext in 91 fold f externs (S.of_int 0) 92 93 end 94 95 96 module FunCall = struct 97 98 type t = 99 { caller : string ; 100 id : int ; 101 callee : string ; 102 args : Args.t } 103 let compare = Pervasives.compare 104 105 let caller fun_call = fun_call.caller 106 let id fun_call = fun_call.id 107 let callee fun_call = fun_call.callee 108 let args fun_call = fun_call.args 109 110 let make caller id callee args = { caller ; id ; callee ; args } 111 112 let apply f f_caller f_id f_callee f_args fun_call = 113 let caller_res = f_caller (caller fun_call) in 114 let id_res = f_id (id fun_call) in 115 let callee_res = f_callee (callee fun_call) in 116 let args_res = f_args (args fun_call) in 117 f caller_res id_res callee_res args_res 118 119 let apply2 f f_caller f_id f_callee f_args fun_call1 fun_call2 = 120 let caller_res = f_caller (caller fun_call1) (caller fun_call2) in 121 let id_res = f_id (id fun_call1) (id fun_call2) in 122 let callee_res = f_callee (callee fun_call1) (callee fun_call2) in 123 let args_res = f_args (args fun_call1) (args fun_call2) in 124 f caller_res id_res callee_res args_res 125 126 let le = 127 let f b1 b2 b3 b4 = b1 && b2 && b3 && b4 in 128 apply2 f (=) (=) (=) Args.le 129 130 let replace_vars replacement = 131 apply make Misc.id Misc.id Misc.id (Args.replace_vars replacement) 132 133 let reduce 134 to_list is_solved replace_vars of_fun_call 135 prototypes costs fun_call = 136 let callee = callee fun_call in 137 let args = args fun_call in 138 if Misc.String.Map.mem callee prototypes then 139 let formals = Misc.String.Map.find callee prototypes in 140 if List.length formals = List.length args then 141 let replacements = 142 Misc.String.Map.of_list (List.combine formals args) in 143 if Misc.String.Map.mem callee costs then 144 let cost' = Misc.String.Map.find callee costs in 145 if is_solved cost' then to_list (replace_vars replacements cost') 146 else [of_fun_call fun_call] 147 else raise (Unknown_cost callee) 148 else 149 raise 150 (Failure ("FunCall.reduce: formals and actuals for " ^ 151 "function " ^ callee ^ " have different sizes.")) 152 else raise (Unknown_prototype callee) 153 154 let to_string fun_call = 155 Printf.sprintf "%s@[%s,%d](%s)" 156 (callee fun_call) (caller fun_call) (id fun_call) 157 (Args.to_string (args fun_call)) 158 159 end 160 161 module FunCalls = struct 162 163 module M = Multiset.Make (FunCall) 164 include M 165 166 let singleton_ fun_call = M.add fun_call empty 167 168 let singleton caller id callee args = 169 singleton (FunCall.make caller id callee args) 170 171 let add = union 172 173 let le1 fun_call occ fun_calls = 174 let f fun_call' occ' = (FunCall.le fun_call fun_call') && (occ <= occ') in 175 exists f fun_calls 176 177 let le fun_calls1 fun_calls2 = 178 let f fun_call occ = le1 fun_call occ fun_calls2 in 179 for_all f fun_calls1 180 181 let called_funs fun_calls = 182 let f fun_call _ called_funs = 183 Misc.String.Set.add (FunCall.callee fun_call) called_funs in 184 fold f fun_calls Misc.String.Set.empty 185 186 let replace_vars replacements fun_calls = 187 let f fun_call _ fun_calls = 188 let fun_call = FunCall.replace_vars replacements fun_call in 189 add (singleton_ fun_call) fun_calls in 190 fold f fun_calls empty 191 192 let to_string = string_of_mset to_list " + " FunCall.to_string 193 194 end 195 196 197 module rec LoopCost : sig 198 type t 199 val compare : t -> t -> int 200 val make : string -> int -> S.relation -> S.t -> S.t -> S.t -> Cost.t -> t 201 val le : t -> t -> bool 202 val called_funs : t -> Misc.String.Set.t 203 val replace_vars : S.t Misc.String.Map.t -> t -> t 204 val reduce : prototypes -> Cost.t Misc.String.Map.t -> t -> t 205 val to_string : t -> string 206 val to_ext : t -> S.t 207 end = struct 208 209 type t = 210 { fun_name : string ; 211 id : int ; 212 relation : S.relation ; 213 init_value : S.t ; 214 exit_value : S.t ; 215 increment : S.t ; 216 body_cost : Cost.t } 217 218 let make fun_name id relation init_value exit_value increment body_cost = 219 { fun_name ; id ; relation ; init_value ; exit_value ; increment ; 220 body_cost } 221 222 let fun_name loop_cost = loop_cost.fun_name 223 let id loop_cost = loop_cost.id 224 let relation loop_cost = loop_cost.relation 225 let init_value loop_cost = loop_cost.init_value 226 let exit_value loop_cost = loop_cost.exit_value 227 let increment loop_cost = loop_cost.increment 228 let body_cost loop_cost = loop_cost.body_cost 229 230 let compare = Pervasives.compare 231 232 let apply f 233 f_fun_name f_id f_relation f_init_value f_exit_value f_increment 234 f_body_cost loop_cost = 235 let fun_name_res = f_fun_name (fun_name loop_cost) in 236 let id_res = f_id (id loop_cost) in 237 let relation_res = f_relation (relation loop_cost) in 238 let init_value_res = f_init_value (init_value loop_cost) in 239 let exit_value_res = f_exit_value (exit_value loop_cost) in 240 let increment_res = f_increment (increment loop_cost) in 241 let body_cost_res = f_body_cost (body_cost loop_cost) in 242 f 243 fun_name_res id_res relation_res init_value_res exit_value_res 244 increment_res body_cost_res 245 246 let apply2 f 247 f_fun_name f_id f_relation f_init_value f_exit_value f_increment 248 f_body_cost loop_cost1 loop_cost2 = 249 let fun_name_res = 250 f_fun_name (fun_name loop_cost1) (fun_name loop_cost2) in 251 let id_res = f_id (id loop_cost1) (id loop_cost2) in 252 let relation_res = 253 f_relation (relation loop_cost1) (relation loop_cost2) in 254 let init_value_res = 255 f_init_value (init_value loop_cost1) (init_value loop_cost2) in 256 let exit_value_res = 257 f_exit_value (exit_value loop_cost1) (exit_value loop_cost2) in 258 let increment_res = 259 f_increment (increment loop_cost1) (increment loop_cost2) in 260 let body_cost_res = 261 f_body_cost (body_cost loop_cost1) (body_cost loop_cost2) in 262 f 263 fun_name_res id_res relation_res init_value_res exit_value_res 264 increment_res body_cost_res 265 266 let le = 267 let f b1 b2 b3 b4 b5 b6 b7 = b1 && b2 && b3 && b4 && b5 && b6 && b7 in 268 apply2 f (=) (=) (=) S.le S.le S.le Cost.le 269 270 let called_funs loop_cost = Cost.called_funs (body_cost loop_cost) 271 272 let replace_vars replacements = 273 let arg_replace_vars = S.replace_vars replacements in 274 apply make Misc.id Misc.id Misc.id arg_replace_vars arg_replace_vars 275 arg_replace_vars (Cost.replace_vars replacements) 276 277 let reduce prototypes costs = 278 apply make Misc.id Misc.id Misc.id Misc.id Misc.id Misc.id 279 (Cost.reduce prototypes costs) 280 281 let to_string loop_cost = 282 Printf.sprintf "%s@%d(%s %s %s %s (%s))" 283 (fun_name loop_cost) 284 (id loop_cost) 285 (S.string_of_relation (relation loop_cost)) 286 (S.to_string (init_value loop_cost)) 287 (S.to_string (exit_value loop_cost)) 288 (S.to_string (increment loop_cost)) 289 (Cost.to_string (body_cost loop_cost)) 290 291 let to_ext loop_cost = 292 let rel = relation loop_cost in 293 let init_value = init_value loop_cost in 294 let exit_value = exit_value loop_cost in 295 let increment = increment loop_cost in 296 let body_cost = body_cost loop_cost in 297 let rel_op = if S.has_lower_type rel then S.minus else S.add in 298 let rel_added = S.of_int (if S.is_large rel then 0 else 1) in 299 let iteration_nb = rel_op increment rel_added in 300 let iteration_nb = S.minus iteration_nb init_value in 301 let iteration_nb = S.add exit_value iteration_nb in 302 let iteration_nb = S.div iteration_nb increment in 303 let body_cost = Cost.to_ext body_cost in 304 let cond_body_cost = 305 S.cond init_value rel exit_value body_cost (S.of_int 0) in 306 S.mul iteration_nb cond_body_cost 307 308 end 309 310 311 and LoopCosts : sig 312 type t 313 val empty : t 314 val singleton : 315 string -> int -> S.relation -> S.t -> S.t -> S.t -> Cost.t -> t 316 val add : t -> t -> t 317 val replace_vars : S.t Misc.String.Map.t -> t -> t 318 val called_funs : t -> Misc.String.Set.t 319 val reduce : prototypes -> Cost.t Misc.String.Map.t -> t -> t 320 val to_string : t -> string 321 val le : t -> t -> bool 322 val to_ext : t -> S.t 323 end = struct 324 325 module M = Multiset.Make (LoopCost) 326 include M 327 328 let singleton_ loop_cost = M.add loop_cost empty 329 330 let singleton 331 fun_name id relation init_value exit_value increment body_cost = 332 let loop_cost = 333 LoopCost.make 334 fun_name id relation init_value exit_value increment body_cost in 335 singleton_ loop_cost 336 337 let add = union 338 339 let le1 loop_cost occ loop_costs = 340 let f loop_cost' occ' res = 341 res || ((LoopCost.le loop_cost loop_cost') && (occ <= occ')) in 342 fold f loop_costs false 343 344 let le loop_costs1 loop_costs2 = 345 let f loop_cost occ res = res && le1 loop_cost occ loop_costs2 in 346 fold f loop_costs1 true 347 348 let called_funs loop_costs = 349 let f loop_cost _ called_funs = 350 Misc.String.Set.union (LoopCost.called_funs loop_cost) called_funs in 351 fold f loop_costs Misc.String.Set.empty 352 353 let replace_vars replacements loop_costs = 354 let f loop_cost _ loop_costs = 355 let loop_cost = LoopCost.replace_vars replacements loop_cost in 356 add (singleton_ loop_cost) loop_costs in 357 fold f loop_costs empty 358 359 let reduce prototypes replacements loop_costs = 360 let f loop_cost occ loop_costs = 361 add_occ (LoopCost.reduce prototypes replacements loop_cost) occ 362 loop_costs in 363 fold f loop_costs empty 364 365 let to_string = string_of_mset to_list " + " LoopCost.to_string 366 367 let to_ext loop_costs = 368 let f loop_cost occ ext = 369 S.add (S.mul (S.of_int occ) (LoopCost.to_ext loop_cost)) ext in 370 fold f loop_costs (S.of_int 0) 371 372 end 373 374 375 and Base : sig 376 type t 377 val compare : t -> t -> int 378 val of_int : int -> t 379 val of_extern : string -> t 380 val of_fun_call_ : FunCall.t -> t 381 val of_fun_call : string -> int -> string -> Args.t -> t 382 val of_loop_cost : 383 string -> int -> S.relation -> S.t -> S.t -> S.t -> Cost.t -> t 384 val add : t -> t -> t 385 val called_funs : t -> Misc.String.Set.t 386 val replace_vars : S.t Misc.String.Map.t -> t -> t 387 val reduce : prototypes -> Cost.t Misc.String.Map.t -> t -> Base.t list 388 val le : t -> t -> bool 389 val to_string : t -> string 390 val to_ext : t -> S.t 391 end = struct 392 393 type t = 394 { constant : int ; 395 externs : Externs.t ; 396 fun_calls : FunCalls.t ; 397 loop_costs : LoopCosts.t } 398 399 let make constant externs fun_calls loop_costs = 400 { constant ; externs ; fun_calls ; loop_costs } 401 402 let compare = Pervasives.compare 403 404 let constant base = base.constant 405 let externs base = base.externs 406 let fun_calls base = base.fun_calls 407 let loop_costs base = base.loop_costs 408 409 let set_fun_calls fun_calls base = { base with fun_calls } 410 let set_loop_costs loop_costs base = { base with loop_costs } 411 412 let to_string base = 413 Printf.sprintf "%d + (%s) + (%s) + (%s)" 414 (constant base) 415 (Externs.to_string (externs base)) 416 (FunCalls.to_string (fun_calls base)) 417 (LoopCosts.to_string (loop_costs base)) 418 419 let of_int i = make i Externs.empty FunCalls.empty LoopCosts.empty 420 421 let of_extern x = 422 make 0 (Externs.singleton x) FunCalls.empty LoopCosts.empty 423 424 let of_fun_call_ fun_call = 425 make 0 Externs.empty (FunCalls.singleton_ fun_call) LoopCosts.empty 426 427 let of_fun_call caller id callee args = 428 let fun_call = FunCall.make caller id callee args in 429 of_fun_call_ fun_call 430 431 let of_loop_cost 432 fun_name id relation init_value exit_value increment body_cost = 433 let loop_costs = 434 LoopCosts.singleton 435 fun_name id relation init_value exit_value increment body_cost in 436 make 0 Externs.empty FunCalls.empty loop_costs 437 438 let apply f f_constant f_externs f_fun_calls f_loop_costs base = 439 let constant_res = f_constant (constant base) in 440 let externs_res = f_externs (externs base) in 441 let fun_calls_res = f_fun_calls (fun_calls base) in 442 let loop_costs_res = f_loop_costs (loop_costs base) in 443 f constant_res externs_res fun_calls_res loop_costs_res 444 445 let apply2 f f_constant f_externs f_fun_calls f_loop_costs base1 base2 = 446 let constant_res = f_constant (constant base1) (constant base2) in 447 let externs_res = f_externs (externs base1) (externs base2) in 448 let fun_calls_res = f_fun_calls (fun_calls base1) (fun_calls base2) in 449 let loop_costs_res = f_loop_costs (loop_costs base1) (loop_costs base2) in 450 f constant_res externs_res fun_calls_res loop_costs_res 451 452 let add = apply2 make (+) Externs.add FunCalls.add LoopCosts.add 453 454 let le = 455 let f b1 b2 b3 b4 = b1 && b2 && b3 && b4 in 456 apply2 f (<=) Externs.le FunCalls.le LoopCosts.le 457 458 let replace_vars replacements = 459 apply make Misc.id 460 (Externs.replace_vars replacements) 461 (FunCalls.replace_vars replacements) 462 (LoopCosts.replace_vars replacements) 463 464 let called_funs base = 465 Misc.String.Set.union 466 (FunCalls.called_funs (fun_calls base)) 467 (LoopCosts.called_funs (loop_costs base)) 468 469 let reduce prototypes costs base = 470 let f fun_call occ base_list = 471 let added_bases = 472 FunCall.reduce 473 Cost.to_list Cost.is_solved Cost.replace_vars of_fun_call_ 474 prototypes costs fun_call in 475 let added_bases = 476 if added_bases = [] then [of_int 0] else added_bases in 477 let added_bases = 478 let f base = Misc.repeat occ (add base) (of_int 0) in 479 List.map f added_bases in 480 let f_base_list res added_base = 481 res @ (List.map (add added_base) base_list) in 482 List.fold_left f_base_list [] added_bases in 483 let loop_costs = LoopCosts.reduce prototypes costs (loop_costs base) in 484 let base = set_loop_costs loop_costs base in 485 let base' = set_fun_calls FunCalls.empty base in 486 FunCalls.fold f (fun_calls base) [base'] 487 488 let to_ext base = 489 let f_fun_calls fun_calls = 490 if not (FunCalls.is_empty fun_calls) then 491 raise (Failure "Base.to_ext: function calls") 492 else S.of_int 0 in 493 let f ext1 ext2 ext3 ext4 = s_add_list [ext1 ; ext2 ; ext3 ; ext4] in 494 apply f S.of_int Externs.to_ext f_fun_calls LoopCosts.to_ext base 495 496 end 497 498 499 and Cost : sig 500 type t 501 val of_int : int -> t 502 val of_extern : string -> t 503 val of_fun_call : string -> int -> string -> Args.t -> t 504 val of_loop_cost : 505 string -> int -> S.relation -> S.t -> S.t -> S.t -> Cost.t -> t 506 val of_base : Base.t -> t 507 val empty : t 508 val add : t -> t -> t 509 val join : t -> t -> t 510 val widen : t -> t -> t 511 val narrow : t -> t -> t 512 val called_funs : t -> Misc.String.Set.t 513 val has_fun_calls : t -> bool 514 val replace_vars : S.t Misc.String.Map.t -> t -> t 515 val reduce : prototypes -> Cost.t Misc.String.Map.t -> t -> t 516 val is_solved : t -> bool 517 val to_list : t -> Base.t list 518 val to_string : t -> string 519 val le : t -> t -> bool 520 val to_ext : t -> S.t 521 end = struct 522 523 module M = Eset.Make (Base) 524 include M 525 526 let to_string cost = 527 if is_empty cost then "0" 528 else Misc.List.to_string " max " Base.to_string (to_list cost) 529 530 let of_base base = singleton base 531 532 let of_int i = of_base (Base.of_int i) 533 534 let of_extern x = of_base (Base.of_extern x) 535 536 let of_fun_call caller id callee args = 537 of_base (Base.of_fun_call caller id callee args) 538 539 let of_loop_cost 540 fun_name loop_id relation init_value exit_value increment body_cost = 541 of_base 542 (Base.of_loop_cost 543 fun_name loop_id relation init_value exit_value increment body_cost) 544 545 let join1 base cost = 546 let f_exists base' = Base.le base base' in 547 if exists f_exists cost then cost 548 else 549 let f_absorb base' = Base.le base' base in 550 M.add base (M.diff cost (M.filter f_absorb cost)) 551 552 let add cost1 cost2 = 553 if is_empty cost1 then cost2 554 else 555 if is_empty cost2 then cost1 556 else 557 let f2 base1 base2 = join1 (Base.add base1 base2) in 558 let f1 base1 = fold (f2 base1) cost2 in 559 fold f1 cost1 empty 560 561 let join cost1 cost2 = 562 if is_empty cost1 then cost2 563 else 564 if is_empty cost2 then cost1 565 else fold join1 cost1 cost2 566 567 let widen = join 568 569 let narrow = join (* TODO: improve *) 570 571 let mem base cost = 572 let f base' res = res || (Base.le base base') in 573 fold f cost false 574 575 let le cost1 cost2 = 576 let f base res = res && (mem base cost2) in 577 fold f cost1 true 578 579 580 let called_funs cost = 581 let f base called_funs = 582 Misc.String.Set.union (Base.called_funs base) called_funs in 583 fold f cost Misc.String.Set.empty 584 585 let has_fun_calls cost = not (Misc.String.Set.is_empty (called_funs cost)) 586 587 let replace_vars replacements cost = 588 let f base cost = join1 (Base.replace_vars replacements base) cost in 589 fold f cost empty 590 591 let reduce prototypes costs cost = 592 let f base cost = 593 let base_list = Base.reduce prototypes costs base in 594 let f_join cost base = join1 base cost in 595 List.fold_left f_join cost base_list in 596 fold f cost empty 597 598 let is_solved cost = not (has_fun_calls cost) 599 600 let to_ext cost = 601 if is_empty cost then S.of_int 0 602 else 603 let f base ext = S.max (Base.to_ext base) ext in 604 let base = choose cost in 605 let cost = remove base cost in 606 fold f cost (Base.to_ext base) 607 608 end 609 610 611 type t = Top | C of Cost.t 612 613 614 let to_string = function 615 | Top -> "top" 616 | C cost -> Cost.to_string cost 617 618 619 let of_int i = C (Cost.of_int i) 620 621 let of_extern fun_name = C (Cost.of_extern fun_name) 622 623 let of_fun_call caller id callee args = 624 C (Cost.of_fun_call caller id callee args) 625 626 let of_loop_cost 627 fun_name loop_id relation init_value exit_value increment body_cost = 628 C (Cost.of_loop_cost 629 fun_name loop_id relation init_value exit_value increment body_cost) 630 631 632 let is_top = function Top -> true | _ -> false 633 634 let extract = function 635 | Top -> raise (Failure "Cost_value.extract") 636 | C cost -> cost 637 638 let top = Top 639 640 let bot = of_int 0 641 642 643 let top_absorbs f = function 644 | Top -> Top 645 | C cost -> C (f cost) 646 647 let top_absorbs2 f cost1 cost2 = match cost1, cost2 with 648 | Top, _ | _, Top -> Top 649 | C cost1, C cost2 -> C (f cost1 cost2) 650 651 652 let add = top_absorbs2 Cost.add 653 654 let join = top_absorbs2 Cost.join 655 656 let widen = top_absorbs2 Cost.widen 657 658 let narrow cost1 cost2 = match cost1, cost2 with 659 | cost, Top | Top, cost -> cost 660 | C cost1, C cost2 -> C (Cost.narrow cost1 cost2) 661 662 let le cost1 cost2 = match cost1, cost2 with 663 | _, Top -> true 664 | Top, _ -> false 665 | C cost1, C cost2 -> Cost.le cost1 cost2 666 667 668 let reduce_ prototypes costs cost = 669 let called_funs = Cost.called_funs cost in 670 let costs = 671 let f fun_name _ = Misc.String.Set.mem fun_name called_funs in 672 Misc.String.Map.filter f costs in 673 let f fun_name cost costs = match cost, costs with 674 | _, None -> None 675 | Top, _ -> None 676 | C cost, Some costs -> Some (Misc.String.Map.add fun_name cost costs) in 677 match Misc.String.Map.fold f costs (Some Misc.String.Map.empty) with 678 | None -> Top 679 | Some costs -> C (Cost.reduce prototypes costs cost) 680 681 let reduce prototypes costs = function 682 | Top -> Top 683 | C cost -> reduce_ prototypes costs cost 684 685 let reduces prototypes costs = 686 Misc.String.Map.map (reduce prototypes costs) costs 687 688 689 let replace_vars replacements = top_absorbs (Cost.replace_vars replacements) 690 691 692 let has_fun_calls = function 693 | Top -> false 694 | C cost -> Cost.has_fun_calls cost 695 696 697 let is_concrete cost = (not (is_top cost)) && (not (has_fun_calls cost)) 698 699 let to_ext = function 700 | Top -> S.top 701 | C cost -> Cost.to_ext cost 702 703 704 end -
Deliverables/D5.1-5.3/cost-plug-in/wrapper/main.ml
r1462 r1679 138 138 (print_verbose1 "Done.\n" ; 139 139 Printf.printf 140 " The cost of the %s function is at most%s (not verified).\n%!"140 "WCET of %s: %s (not verified).\n%!" 141 141 fun_name cost ; 142 142 (fun_name, cost)) 143 143 else aux () 144 144 else error ("Bad format of result file " ^ filename ^ ".") 145 with End_of_file -> error "No step function found." in 145 with End_of_file -> 146 error "No step function found or its cost could not be computed." in 146 147 aux () 147 148 … … 168 169 let success_msg = "Done. Results are in file " ^ res_file ^ "." in 169 170 exec cmd error_callback error_msg success_callback success_msg 171 172 let string_starts_with prefix s = 173 let l = String.length prefix in 174 (l <= String.length s) && (String.sub s 0 l = prefix) 170 175 171 176 let read_jessie_results filename = … … 179 184 let rec aux () = 180 185 let s = input_line ic in 181 let string_dpoints = " : " in 182 let string_total = "total" ^ string_dpoints in 183 let string_valid = "valid" ^ string_dpoints in 184 let length_total = String.length string_total in 185 let regexp = Str.regexp ("^" ^ string_total ^ "[0-9]+$") in 186 if Str.string_match regexp s 0 then 187 let total = 188 String.sub s length_total ((String.length s) - length_total) in 189 let s = input_line ic in 190 let s_compare = string_valid ^ total in 191 if String.length s >= String.length s_compare && 192 String.sub s 0 (String.length s_compare) = s_compare then 186 if string_starts_with "valid" s then 187 let regexp = Str.regexp (".*100%.*") in 188 if Str.string_match regexp s 0 then 193 189 (print_verbose1 "Done.\n" ; 194 Printf.printf " Resultis proven correct.\n%!")190 Printf.printf "WCET is proven correct.\n%!") 195 191 else print_failed () 196 192 else aux () in -
Deliverables/D5.1-5.3/cost-plug-in/wrapper/options.ml
r1462 r1679 56 56 "-prover", Arg.String set_prover, 57 57 " Select a prover for verification through why."; 58 extra_doc " Needs the -verify option."; 58 59 extra_doc " [default is simplify]"; 59 60 60 61 "-gui", Arg.Set gui_flag, 61 62 " Do not select a prover: run a graphical user interface instead."; 63 extra_doc " Needs the -verify option."; 62 64 63 65 "-test", Arg.Set test_flag, … … 66 68 "-test-cases", Arg.Int set_test_cases, 67 69 " Number of test cases."; 70 extra_doc " Needs the -test option."; 68 71 extra_doc " [default is 10]"; 69 72 70 73 "-test-cycles", Arg.Int set_test_cycles, 71 74 " Number of cycles for each test case."; 75 extra_doc " Needs the -test option."; 72 76 extra_doc " [default is 10]"; 73 77 74 78 "-test-min-int", Arg.Int set_test_min_int, 75 79 " Random int minimum value."; 80 extra_doc " Needs the -test option."; 76 81 extra_doc " [default is -1000]"; 77 82 78 83 "-test-max-int", Arg.Int set_test_max_int, 79 84 " Random int maximum value."; 85 extra_doc " Needs the -test option."; 80 86 extra_doc " [default is 1000]"; 81 87 ]
Note: See TracChangeset
for help on using the changeset viewer.