Ignore:
Timestamp:
Feb 7, 2012, 6:01:43 PM (8 years ago)
Author:
ayache
Message:

Frama-C plug-in (sources+documentation)

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  
    11PACKAGE=cost-plug-in
    22PACKAGE_RES=$(PACKAGE).tgz
     3
     4JESSIE=frama-c_jessie
    35
    46all:
    … …  
    79
    810install:
     11        mkdir -p /usr/local/bin
     12        cp $(JESSIE) /usr/local/bin/
    913        make -C plugin install
    1014        make -C wrapper install

  • Deliverables/D5.1-5.3/cost-plug-in/README

    r1462 r1679  
    1111  - CerCo
    1212  - Lustre compiler (for Lustre files only)
    13   - Jessie plug-in and simplify (for verification of Lustre files only)
     13  - Jessie plug-in and simplify (for verification only)
    1414
    1515 Compilation
    … …  
    3333Note: both the plug-in and the wrapper can be installed seperately. See their
    3434README 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.
    3636
    3737 Usage
    … …  
    6666
    6767    % 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  
    22README
    33distributed_files
     4frama-c_jessie
    45plugin/
    56plugin/Makefile
    67plugin/README
     8plugin/arith.ml
     9plugin/arithSig.ml
    710plugin/cerco.ml
     11plugin/completeMap.ml
    812plugin/compute.ml
    913plugin/cost.ml
    1014plugin/cost_value.ml
    11 plugin/help/
    12 plugin/help/mailinglisthelp
    13 plugin/stringTools.ml
     15plugin/emap.ml
     16plugin/eset.ml
     17plugin/misc.ml
     18plugin/multiset.ml
    1419plugin/tests/
    15 plugin/tests/bubble_sort.c
     20plugin/tests/fail/
     21plugin/tests/fail/blowfish.c
     22plugin/tests/fail/blowfish.h
     23plugin/tests/fail/bubble_sort.c
     24plugin/tests/success/
     25plugin/tests/success/3-way.c
     26plugin/tests/success/LFSR.C
     27plugin/tests/success/LFSR2.C
     28plugin/tests/success/a5.c
     29plugin/tests/success/fact.c
     30plugin/tests/success/is_sorted.c
     31plugin/tests/success/random.c
     32plugin/tests/success/tab_sum.c
    1633wrapper/
    1734wrapper/Makefile

  • Deliverables/D5.1-5.3/cost-plug-in/plugin/Makefile

    r1462 r1679  
    2727
    2828PLUGIN_NAME = Cost_synthesis
    29 PLUGIN_CMO  = stringTools cost_value compute cerco cost
     29PLUGIN_CMO  =  eset emap completeMap multiset misc arithSig arith       \
     30        cost_value compute cerco cost
    3031
    3132# PLUGIN_HAS_MLI := yes

  • Deliverables/D5.1-5.3/cost-plug-in/plugin/cerco.ml

    r1462 r1679  
    1111    let fun_name = String.sub s 0 i in
    1212    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.empty
     13    Misc.String.Map.add fun_name var_name (extern_cost_variables cin)
     14  with End_of_file -> Misc.String.Map.empty
    1515
    1616(** [multifile_exists exts filename] returns true if and only if the file name
    … …  
    5656
    5757let 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 =
    5959  let annotated_ext = "-annotated.c" in
    6060  let asm_ext = ".s" in

  • Deliverables/D5.1-5.3/cost-plug-in/plugin/compute.ml

    r1462 r1679  
    11
    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 *)
    323
    334(*** Exceptions ***)
    345
    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."
     6exception ASM_unsupported
     7exception Try_unsupported
     8
     9let 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."
    6316  | e -> raise e
    6417
    6518
     19(*** Debug flag ***)
     20
     21let debug = ref false
     22
     23
    6624(*** Helpers ***)
    6725
    6826let identity x = x
    6927
     28let 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
    7035let integer_term term = Logic_const.term term Cil_types.Linteger
     36
     37let 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
     42let cil_logic_int_var x =
     43  Logic_const.tvar (Cil_const.make_logic_var x Cil_types.Linteger)
     44
     45type loops_annotation =
     46    (string -> string ->
     47     (Db_types.rooted_code_annotation Db_types.before_after) list)
     48
     49type loops_annotations = loops_annotation list
    7150
    7251let add_loop_annot obj stmt annot =
    7352  Queue.add (fun () -> Annotations.add stmt [Ast.self] annot)
    7453    obj#get_filling_actions
     54
     55let add_loop_annots obj stmt annots = List.iter (add_loop_annot obj stmt) annots
    7556
    7657let loop_annotation annot = Db_types.Before (Db_types.User annot)
    … …  
    10182  let cost_var = Cil_const.make_logic_var cost_id Cil_types.Linteger in
    10283  let cost_var = Logic_const.tvar cost_var in
    103   let cost = Cost_value.to_cil_term cost in
    10484  let old_cost =
    10585    Logic_const.term (Cil_types.Told cost_var) cost_var.Cil_types.term_type in
    … …  
    10888  Logic_const.prel (rel, cost_var, new_cost)
    10989
    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)
     90let 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
     112and remove_casts_lval (lhost, offset) =
     113  (remove_casts_lhost lhost, remove_casts_offset offset)
     114
     115and remove_casts_lhost = function
     116  | Cil_types.Mem e -> Cil_types.Mem (remove_casts e)
     117  | lhost -> lhost
     118
     119and 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
     126let 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
     131let has_fun_type varinfo = match varinfo.Cil_types.vtype with
     132  | Cil_types.TFun _ -> true
     133  | _ -> false
     134
     135let 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 *)
    232140
    233141let dummy_location = (Lexing.dummy_pos, Lexing.dummy_pos)
    234142
    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
     143let dummy_varinfo = Cil.makeVarinfo false false "" (Cil_types.TVoid [])
     144
     145let 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
     149let 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
     163and block_subs block = List.flatten (List.map stmt_subs block.Cil_types.bstmts)
     164
     165let 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
     171let stmt_is_break stmt = match stmt.Cil_types.skind with
     172  | Cil_types.Break _ -> true
     173  | _ -> false
     174
     175let 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
     182let rec last = function
     183  | [] -> None
     184  | [e] -> Some e
     185  | _ :: l -> last l
     186
     187let 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
     193module IntSet = Misc.Int.Set
     194module IntMap = Misc.Int.Map
     195module IntCMap = Misc.Int.CMap
     196
     197
     198(*** Temporary variable name generator ***)
     199
     200module 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
     224end
     225
     226
     227(*** Debug helpers ***)
     228
     229let string_of_intset set =
     230  IntSet.fold (fun i s -> s ^ (string_of_int i) ^ " ") set ""
     231let 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
     235class 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
     249end
     250
     251let 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
     257class 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%!")
    254279      | _ -> () in
    255280    Cil.DoChildren
    256281
    257   (* Update the variables whose address may be accessed. This is done by
    258      visiting every statement of the program. *)
     282end
     283
     284let 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
     294class 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
     301end
     302
     303let 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
     312module 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
     340end
     341
     342module 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
     368end
     369
     370class points_infos points_infos prj =
     371object inherit Visitor.frama_c_copy prj as super
     372
     373  val mutable current_fun_name = ""
     374
    259375  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
    261379    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
    267404      | _ -> () in
    268405    Cil.DoChildren
    269406
    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
     413end
     414
     415let 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
     425module 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
     517end
     518
     519
     520(*** Arithmetic expressions flat domain ***)
     521
     522module 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
     573end
     574
     575module Domain = ArithValDom
     576
     577
     578(*** Abstract cost ***)
     579
     580module AbsCost = struct
     581
     582  include (Cost_value.Make (ArithValDom))
     583
     584end
     585
     586
     587(*** Requirements for loop termination ***)
     588
     589module 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
     639end
     640
     641module 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
     684end
     685
     686
     687(*** Point kind ***)
     688
     689module 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
     719end
     720
     721module 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
     738end
     739
     740module 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
     759end
     760
     761
     762(*** Fun infos ***)
     763
     764module 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
     810end
     811
     812module 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
     874end
     875
     876
     877(*** Static environment ***)
     878
     879module 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
     981end
     982
     983
     984(*** Initializations ***)
     985
     986let special_point f body = match f body with
     987  | None -> None
     988  | Some stmt -> Some stmt.Cil_types.sid
     989
     990let start_point = special_point first_stmt
     991
     992let end_point = special_point last_stmt
     993
     994let 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
     999let make_tmp_names formals =
     1000  let f varinfo = (varinfo, GenName.concat varinfo.Cil_types.vname) in
     1001  List.map f formals
     1002
     1003let 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
     1019let 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
     1032let 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
     1059let 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
     1066let 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
     1080let 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
     1085let 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
     1114class initialize points_infos static_env prj =
     1115object 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
     1165end
     1166
     1167let 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
     1181module 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
     1198end
     1199
     1200module 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
     1213end
     1214
     1215module 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
     1236end
     1237
     1238module 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
     1269end
     1270
     1271module 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
     1358end
     1359
     1360module 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
     1403end
     1404
     1405
     1406module 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
     1416end
     1417
     1418module AbsEnv  = PointsAbsEnv.AbsEnv
     1419
     1420
     1421(*** Dependent cost results ***)
     1422
     1423module 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
     1463end
     1464
     1465module 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
     1590end
     1591
     1592module 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
     1617end
     1618
     1619module 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
     1637end
     1638
     1639module 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
     1673end
     1674
     1675module 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
     1741end
     1742
     1743
     1744(*** Abstract interpretation ***)
     1745
     1746module 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
     1989end
     1990
     1991
     1992(*** Dependent costs computation ***)
     1993
     1994class compute_costs widen narrow loops_annots static_env costs prj =
     1995object inherit Visitor.frama_c_copy prj as super
     1996
    2741997  method vfunc fundec =
    2751998    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
     2030end
     2031
     2032let 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 =       
    3082036    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 ***)
    6852045
    6862046let solve_end costs1 costs2 =
    6872047  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
     2052let 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
     2057let 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
    7332069
    7342070
    7352071(*** Add annotations ***)
    7362072
    737 let add_tmp_cost_init env tmp_cost stmt =
    738   let lval = Cil.var tmp_cost in
     2073let add_tmp_loop_init cost_varinfo tmp_loop stmt =
     2074  let lval = Cil.var tmp_loop in
    7392075  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
    7422077  let new_stmt =
    7432078    Cil_types.Instr (Cil_types.Set (lval, e, dummy_location)) in
    … …  
    7452080  Cil.mkStmt (Cil_types.Block (Cil.mkBlock [new_stmt ; stmt]))
    7462081
     2082let 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
     2089let 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
     2093let 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
     2099let 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
    7472127let 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 []
    7592134
    7602135let add_spec pres post spec =
    … …  
    7692144  Cil.ChangeDoChildrenPost (spec, identity)
    7702145
    771 let add_cost_incr_annotation cost_id spec =
     2146let add_cost_incr_annotation cost_id fundec =
    7722147  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
     2152let 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
     2161let 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
    7822167  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
     2170class add_annotations static_env costs prj =
    8752171object (self) inherit Visitor.frama_c_copy prj as super
    8762172
    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)
    8942199
    8952200  method vspec spec = match self#current_kf with
    … …  
    8992204        | Db_types.Definition (fundec, _) ->
    9002205          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
     2211end
     2212
     2213let add_annotations static_env costs =
    9182214  let add_annotations_prj =     
    9192215    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
    9222217  let f () =
    923     Parameters.CodeOutput.set fname ;
     2218    Parameters.CodeOutput.set (StaticEnv.fname static_env) ;
    9242219    File.pretty_ast () in
    9252220  Project.on add_annotations_prj f ()
    9262221
    9272222
    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
     2225let 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
    9342234  let save_file =
    9352235    try Filename.chop_extension fname
    … …  
    9412241    close_out oc
    9422242  with Sys_error _ ->
    943     Printf.eprintf "Could not save plug-in results in file %s\n%!" save_file
     2243    Printf.eprintf "Could not save plug-in results in file %s.\n%!" save_file
    9442244
    9452245
    … …  
    9502250    Parameters.Files.set [fname] ;
    9512251    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  
    2828  Plugin.Register
    2929    (struct
    30       let name = "Cost synthesis"
     30      let name = "cost synthesis"
    3131      let shortname = "cost"
    3232      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"
    3434      let is_dynamic = true
    3535     end)
    … …  
    7878    let files : Cabs.file list = Ast.UntypedFiles.get () in
    7979    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 =
    8181      List.map
    8282        (Cerco.apply lustre_option lustre_verify_option lustre_test_option)
    8383        files in
     84    Compute.debug := Self.Debug.get () <> 0 ;
    8485    List.iter Compute.cost files
    8586

  • Deliverables/D5.1-5.3/cost-plug-in/plugin/cost_value.ml

    r1462 r1679  
    22(** This module describes the values manipulated by the plug-in. *)
    33
    4 
    5 type relation = Lt | Gt | Le | Ge
    6 
    7 let string_of_relation = function
    8   | Lt -> "<"
    9   | Le -> "<="
    10   | Gt -> ">"
    11   | Ge -> ">="
    12 
    13 let bool_fun_of_relation = function
    14   | Lt -> (<)
    15   | Le -> (<=)
    16   | Gt -> (>)
    17   | Ge -> (>=)
    18 
    19 let mk_strict = function
    20   | Lt | Le -> Lt
    21   | Gt | Ge -> Gt
    22 
    23 let mk_large = function
    24   | Lt | Le -> Le
    25   | Gt | Ge -> Ge
    26 
    27 let opposite = function
    28   | Lt -> Ge
    29   | Le -> Gt
    30   | Gt -> Le
    31   | Ge -> Lt
    32 
    33 type unop = Neg
    34 
    35 let string_of_unop = function
    36   | Neg -> "-"
    37 
    38 let int_fun_of_unop = function
    39   | Neg -> (fun x -> (-x))
    40 
    41 type binop = Add | Sub | Div | Mul | Mod | Max
    42 
    43 let string_of_binop = function
    44   | Add -> "+"
    45   | Sub -> "-"
    46   | Div -> "/"
    47   | Mul -> "*"
    48   | Mod -> "%"
    49   | Max -> "max"
    50 
    51 let int_fun_of_binop = function
    52   | Add -> (+)
    53   | Sub -> (-)
    54   | Div -> (/)
    55   | Mul -> ( * )
    56   | Mod -> (mod)
    57   | Max -> max
    58 
    59 (** Cost values *)
    60 
    61 type t =
    62   | Int of int
    63   | Var of string (* either a parameter or a global, but not a local *)
    64   | UnOp of unop * t
    65   | BinOp of binop * t * t
    66   | 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 = function
    78   | 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) -> args
    83 
    84 (** [fill_subs s subs] replaces the sub-values of the cost value [v] with
    85     those in [subs]. *)
    86 
    87 let fill_subs v subs = match v, subs with
    88   | Int _, _ | Var _, _ | Any, _ -> v
    89   | 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 its
    97     children, starting from the leaves and going up in the tree. [f]'s type is
    98     [t -> 'a list -> 'a], where the second argument is the results of the fold
    99     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) in
    103   f v subs_res
    104 
    105 
    106 let rec f_to_string v subs_res = match v, subs_res with
    107   | Int i, _ -> string_of_int i
    108   | Var x, _ -> x
    109   | 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 telse
    115   | CostOf (fun_name, _), args ->
    116     let f res v = res ^ v ^ ", " in
    117     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 v
    123 
    124 
    125 (* Variables of a cost value *)
    126 
    127 let union_list l =
    128   List.fold_left StringTools.Set.union StringTools.Set.empty l
    129 
    130 let f_vars v subs_res =
    131   let v_res = match v with
    132     | Var x -> StringTools.Set.singleton x
    133     | _ -> StringTools.Set.empty in
    134   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_vars
    139 
    140 
    141 (* Replace variables by expressions *)
    142 
    143 (*
    144 let f_replace r_list v subs_res =
    145   let v = match v with
    146     | Var x when List.mem_assoc x r_list -> List.assoc x r_list
    147     | _ -> v in
    148   fill_subs v subs_res
    149 *)
    150 
    151 let f_replace r_list v subs_res = match fill_subs v subs_res with
    152   | Var x when List.mem_assoc x r_list -> List.assoc x r_list
    153   | v -> v
    154 
    155 (** [replace r_list v] replaces the variables of [v] that are in the association
    156     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 *)
    1644exception Unknown_cost of string
    165 (* Raised when the prototype of a function is not found *)
    1665exception Unknown_prototype of string
    1676
    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
     8let 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
     15type prototypes = string list Misc.String.Map.t
     16
     17
     18module 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
     48end
     49
     50
     51module 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
    19565      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
     704end

  • Deliverables/D5.1-5.3/cost-plug-in/wrapper/main.ml

    r1462 r1679  
    138138          (print_verbose1 "Done.\n" ;
    139139           Printf.printf
    140              "The cost of the %s function is at most %s (not verified).\n%!"
     140             "WCET of %s: %s (not verified).\n%!"
    141141             fun_name cost ;
    142142           (fun_name, cost))
    143143        else aux ()
    144144      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
    146147  aux ()
    147148
    … …  
    168169  let success_msg = "Done. Results are in file " ^ res_file ^ "." in
    169170  exec cmd error_callback error_msg success_callback success_msg
     171
     172let string_starts_with prefix s =
     173  let l = String.length prefix in
     174  (l <= String.length s) && (String.sub s 0 l = prefix)
    170175
    171176let read_jessie_results filename =
    … …  
    179184        let rec aux () =
    180185          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
    193189              (print_verbose1 "Done.\n" ;
    194                Printf.printf "Result is proven correct.\n%!")
     190               Printf.printf "WCET is proven correct.\n%!")
    195191            else print_failed ()
    196192          else aux () in

  • Deliverables/D5.1-5.3/cost-plug-in/wrapper/options.ml

    r1462 r1679  
    5656  "-prover", Arg.String set_prover,
    5757  " Select a prover for verification through why.";
     58  extra_doc " Needs the -verify option.";
    5859  extra_doc " [default is simplify]";
    5960
    6061  "-gui", Arg.Set gui_flag,
    6162  " Do not select a prover: run a graphical user interface instead.";
     63  extra_doc " Needs the -verify option.";
    6264
    6365  "-test", Arg.Set test_flag,
    … …  
    6668  "-test-cases", Arg.Int set_test_cases,
    6769  " Number of test cases.";
     70  extra_doc " Needs the -test option.";
    6871  extra_doc " [default is 10]";
    6972
    7073  "-test-cycles", Arg.Int set_test_cycles,
    7174  " Number of cycles for each test case.";
     75  extra_doc " Needs the -test option.";
    7276  extra_doc " [default is 10]";
    7377
    7478  "-test-min-int", Arg.Int set_test_min_int,
    7579  " Random int minimum value.";
     80  extra_doc " Needs the -test option.";
    7681  extra_doc " [default is -1000]";
    7782
    7883  "-test-max-int", Arg.Int set_test_max_int,
    7984  " Random int maximum value.";
     85  extra_doc " Needs the -test option.";
    8086  extra_doc " [default is 1000]";
    8187]
Note: See TracChangeset for help on using the changeset viewer.