plugin/compute_simple.ml

   1
   2 open Parameters
   3 open Cil_types
   4 open Simplify_terms
   5 module Varinfo = Cil_datatype.Varinfo
   6 module Logic_var = Cil_datatype.Logic_var
   7 module Stmt = Cil_datatype.Stmt
   8 module Term = Cil_datatype.Term
   9 module Logic_label = Cil_datatype.Logic_label
  10
  11 (** This module defines the main analysis of the plug-in. Its actions are:
  12     - build the CFG of the program;
  13     - compute the cost of each function depending on the costs of the others
  14     at the same time add the needed invariant and at the cost of each function
  15 *)
  16
  17
  18 (*** Helpers ***)
  19
  20 let identity x = x
  21
  22 let string_of_list sep f l =
  23   let rec aux = function
  24     | [] -> ""
  25     | [e] -> f e
  26     | e :: l -> (f e) ^ sep ^ (aux l) in
  27   aux l
  28
  29 let integer_term term = Logic_const.term term Linteger
  30
  31 let tinteger i =
  32   let cint64 = CInt64 (My_bigint.of_int i, IInt, None) in
  33   let iterm = TConst cint64 in
  34   integer_term iterm
  35
  36 let cil_logic_int_var x =
  37   Logic_const.tvar (Cil_const.make_logic_var x Linteger)
  38
  39 let current_kf obj = match obj#current_kf with
  40   | None -> raise (Failure "Compute.current_kf")
  41   | Some kf -> kf
  42
  43 let add_loop_annot obj stmt annot =
  44   let annot = User annot in
  45   let kf =
  46     Cil.get_original_kernel_function (Cil.copy_visit ()) (current_kf obj) in
  47   Queue.add (fun () -> Annotations.add kf stmt [Ast.self] annot)
  48     obj#get_filling_actions
  49
  50 let add_loop_annots obj stmt annots = List.iter (add_loop_annot obj stmt) annots
  51
  52 let mk_invariant pred =
  53   Logic_const.new_code_annotation (AInvariant ([], true, pred))
  54
  55 let mk_variant term =
  56   Logic_const.new_code_annotation (AVariant (term, None))
  57
  58 let mk_fun_cost_pred rel cost_id cost =
  59   let cost_var = Cil_const.make_logic_var cost_id Linteger in
  60   let cost_var = Logic_const.tvar cost_var in
  61   let old_cost = Logic_const.told cost_var in
  62   let new_cost = TBinOp (PlusA, old_cost, cost) in
  63   let new_cost = integer_term new_cost in
  64   Logic_const.prel (rel, cost_var, new_cost)
  65
  66 let rec exp_is_var name e = match (remove_casts e).enode with
  67   | Lval (Var v, _) -> v.vname = name
  68   | Info (e, _) -> exp_is_var name e
  69   | _ -> false
  70
  71 let has_fun_type varinfo = match varinfo.vtype with
  72   | TFun _ -> true
  73   | _ -> false
  74
  75 let formals_of_varinfo varinfo = match varinfo.vtype with
  76   | TFun (_, args, _, _) ->
  77     List.map (fun (x, t, _) -> Cil.makeVarinfo false true x t)
  78       (Cil.argsToList args)
  79   | _ -> assert false (* do not use on these arguments *)
  80
  81 let dummy_location = (Lexing.dummy_pos, Lexing.dummy_pos)
  82
  83 let dummy_varinfo = Cil.makeVarinfo false false "" (TVoid [])
  84
  85 let make_list n a =
  86   let rec aux acc i = if i >= n then acc else aux (a :: acc) (i+1) in
  87   aux [] 0
  88
  89 let rec stmt_subs stmt =
  90   let added = match stmt.skind with
  91     | If (_, block1, block2, _)
  92     | TryFinally (block1, block2, _)
  93     | TryExcept (block1, _, block2, _) ->
  94       (block_subs block1) @ (block_subs block2)
  95     | Switch (_, block, _, _)
  96     | Loop (_, block, _, _, _)
  97     | Block block -> block_subs block
  98     | UnspecifiedSequence l ->
  99       List.map (fun (stmt, _, _, _, _) -> stmt) l
 100     | _ -> [] in
 101   stmt :: added
 102
 103 and block_subs block = List.flatten (List.map stmt_subs block.bstmts)
 104
 105 let rec first_stmt block = match block.bstmts with
 106   | [] -> None
 107   | stmt :: _ -> match stmt.skind with
 108       | Block block -> first_stmt block
 109       | _ -> Some stmt
 110
 111 let stmt_is_break stmt = match stmt.skind with
 112   | Break _ -> true
 113   | _ -> false
 114
 115 let starts_with_break block = match first_stmt block with
 116   | Some stmt ->
 117     (match stmt.skind with
 118       | Goto (stmt_ref, _) -> stmt_is_break !stmt_ref
 119       | _ -> stmt_is_break stmt)
 120   | _ -> false
 121
 122 let rec last = function
 123   | [] -> None
 124   | [e] -> Some e
 125   | _ :: l -> last l
 126
 127 let rec last_stmt block = match last block.bstmts with
 128   | None -> None
 129   | Some stmt -> match stmt.skind with
 130       |  Block block -> last_stmt block
 131       | _ -> Some stmt
 132
 133 class print_CFG = object inherit Visitor.frama_c_inplace as super
 134
 135   method vfunc func =
 136     Format.printf "*** %s ***\n\n%!" func.svar.vname ;
 137     List.iter
 138       (fun stmt ->
 139         Format.printf "%d: %a\n--> %!" stmt.sid Cil.d_stmt stmt ;
 140         List.iter (fun stmt -> Format.printf "%d %!" stmt.sid)
 141           stmt.succs ;
 142         Format.printf "\n\n%!")
 143       func.sallstmts ;
 144     Format.printf "\n\n%!" ;
 145     Cil.SkipChildren
 146
 147 end
 148
 149 let print_CFG () =
 150   Visitor.visitFramacFile (new print_CFG) (Ast.get ())
 151
 152 (*** Make CFG ***)
 153
 154 class make_CFG = object inherit Visitor.frama_c_inplace as super
 155
 156   method vfile file =
 157     Cfg.clearFileCFG ~clear_id:false file ;
 158     Cfg.computeFileCFG file ;
 159     Cil.SkipChildren
 160
 161 end
 162
 163 let make_CFG () =
 164   Visitor.visitFramacFile (new make_CFG) (Ast.get ())
 165
 166 (** Extract variant *)
 167
 168 let rec extract_added_value counter e = match e.enode with
 169   | BinOp (PlusA, e1, e2, _) when exp_is_var counter e1 ->
 170     Some (counter, e2)
 171   | BinOp (MinusA, e1, e2, typ)
 172       when exp_is_var counter e1 ->
 173     let enode = UnOp (Neg, e2, typ) in
 174     let e2 = { e2 with enode = enode } in
 175     Some (counter, e2)
 176   | CastE (_, e) -> extract_added_value counter e
 177   | _ ->
 178     if !debug then
 179       Format.printf
 180         "Could not find added increment value for counter %s in %a.\n%!"
 181         counter Cil.d_exp e ;
 182     None
 183
 184 let extract_increment block =
 185   let open Misc.Option in
 186   last_stmt block >>=
 187   (fun stmt -> match stmt.skind with
 188     | Instr (Set ((Var v, _), e, _)) ->
 189       extract_added_value v.vname e
 190     | _ ->
 191       if !debug then
 192         Format.printf
 193           "Could not find increment instruction; found %a instead.\n%!"
 194           Cil.d_stmt stmt ;
 195       None)
 196
 197 let gen_variant counter rel guard increment =
 198   let counter = term_of_exp counter in
 199   let guard   = term_of_exp guard in
 200   let increment = term_of_exp increment in
 201   let guard = match rel with
 202     | Lt | Gt | Ne -> guard
 203     | Le | Ge | Eq -> make_binop PlusA (Cil.lconstant My_bigint.one) guard
 204     | _ -> assert false (* not implemented TODO be gentle *) in
 205   let variant = make_binop MinusA guard counter in
 206   let variant =
 207     if no_division_in_generated_variant
 208     then make_binop Mult variant (make_sign increment)
 209     else make_binop Div variant increment in
 210   simplify_term variant
 211
 212 let opposite = function
 213   | Lt -> Gt
 214   | Gt -> Lt
 215   | Le -> Ge
 216   | Ge -> Le
 217   | Eq -> Eq
 218   | Ne -> Ne
 219   | _ -> assert false (* not implemented TODO be gentle *)
 220
 221
 222 let extract_guard block (counter, increment) =
 223   let open Misc.Option in
 224   first_stmt block >>=
 225   (fun stmt -> match stmt.skind with
 226     | If (e, _, block, _) when starts_with_break block ->
 227       (match e.enode with
 228         | BinOp (rel, e1, e2, _)
 229             when exp_is_var counter e1 (* && Domain.is_supported_rel rel *) ->
 230           (*Some (counter, rel, e2, increment)*)
 231           Some (gen_variant e1 rel e2 increment)
 232         | BinOp (rel, e1, e2, _)
 233             when exp_is_var counter e2 (* && Domain.is_supported_rel rel *) ->
 234           (* let rel = rel in *)
 235           (* let rel = Domain.opposite rel in *)
 236           (* Some (counter, rel, e1, increment) *)
 237           let rel = opposite rel in
 238           Some (gen_variant e2 rel e1 increment)
 239         | _ ->
 240           if !debug then
 241             Format.printf "Unsupported guard condition %a on counter %s.\n%!"
 242               Cil.d_exp e counter ;
 243           None)
 244     | If (_, _, block, _) ->
 245       if !debug then
 246         Format.printf "Loop not guarded by a break:\n%a\n%!" Cil.d_block block ;
 247       None
 248     | _ ->
 249       if !debug then Format.printf "Loop not guarded:\n%a\n%!" Cil.d_stmt stmt ;
 250       None)
 251
 252 let extract_variant body =
 253   let open Misc.Option in
 254   extract_increment body >>= extract_guard body
 255
 256 let rec find_variant = function
 257   | [] -> None
 258   | {annot_content = AVariant (t,_)}::_ -> Some t
 259   | _::l -> find_variant l
 260
 261
 262 (** Function computing cost of special instruction  *)
 263
 264 type env =
 265   { env_fun_cost : term Varinfo.Hashtbl.t;
 266     env_cost_incr_name : string; (* TODO put the varinfo *)
 267     env_cost_var : logic_var;
 268     mutable env_loop_name : unit -> string;
 269   }
 270
 271 let init_loop_name env file =
 272   let i = ref 0 in
 273   let f () =
 274     incr i;
 275     Format.sprintf "__cost_%s_loop_%i" file !i in
 276   env.env_loop_name <- f
 277
 278 let dumb_env_loop_name () : string = assert false
 279
 280 let linteger t = Logic_const.term t Linteger
 281
 282 (** Create a function which compute the cost of a loop.
 283 It uses the variant as the strictly decreasing positive argument.
 284 The cost depend of the other arguments \vec x.
 285
 286 \bcost if the cost of the body of the loop (must be always positive!)
 287 \phi compute the modification of \vec x by one turn of the loop
 288
 289 f(v,\vec x) =
 290   if v < 0 then 0
 291   else (f(v-1,\phi(\vec x)) + \bcost(\vec x))
 292
 293 It also create some needed lemmas:
 294  - f is always positive
 295
 296 or simplifying lemmas:
 297  - simpler (eg. algebraic) formulation of f:
 298    * \vec x = \empty, \phi = identity, \bcost = c >= 0
 299      f(v) = c (v + 1)
 300    * \phi = identity
 301      f(v,\vec x) = \bcost(\vec x) * (v + 1)
 302    * \phi(\vec x) = x_1 + 1,x_2,...,x_n
 303      \bcost(\vec x) = max(c x_1,0) + \phi(x_2,...,x_n)
 304      \phi(x_2,...,x_n) >= 0, c >= 0
 305     f(v,\vec x) = \phi(x_2,...,x_n) (v + 1)
 306       + c * [y(y+1) - (max(y-v-1,0)(y-v)]/2
 307 *)
 308 let create_fun_loop env dep bcost =
 309   let v  = Cil_const.make_logic_var "v" Linteger in
 310   let tv = Logic_const.tvar v in
 311   let xargs = List.map fst dep in   (** \vec x *)
 312   let mod_dep = List.map snd dep in (** \phi *)
 313   let args = v::xargs in
 314   let targs = List.map Logic_const.tvar args in
 315   (** The function *)
 316   let signature = Larrow (List.map (fun _ -> Linteger) args, Linteger) in
 317   let new_loop_name = env.env_loop_name () in
 318   let li = { l_var_info = Cil_const.make_logic_var new_loop_name signature;
 319              l_labels = [];
 320              l_tparams = [];
 321              l_type = Some Linteger;
 322              l_profile = args;
 323              l_body = LBnone (* temporary *) } in
 324   let lzero = Cil.lzero () in
 325   let tvminusone =
 326     linteger (TBinOp(MinusA, tv, Cil.lconstant (My_bigint.one))) in
 327   (* let body = linteger (Tapp(li,[],tvminusone::mod_dep)) in *)
 328   let body = linteger (tapp li (tvminusone::mod_dep)) in
 329   let body = linteger (TBinOp(PlusA, body, bcost)) in
 330   let body =
 331     Tif(linteger (TBinOp(Lt, tv, lzero)), lzero, body) in
 332   li.l_body <- LBterm (linteger body);
 333   (** Axiom positive *)
 334   let lemma = Logic_const.unamed
 335     (Pforall(args,
 336              Logic_const.unamed
 337                (Prel (Rge, linteger (Tapp(li, [], targs)), lzero)))) in
 338   let lemma = Dlemma (new_loop_name ^ "_is_positive", false, [], [], lemma,
 339                       Cil_datatype.Location.unknown) in
 340   (** Register them as global (in reverse order) *)
 341   Globals.Annotations.add_generated lemma;
 342   Globals.Annotations.add_generated
 343     (Dfun_or_pred (li, Cil_datatype.Location.unknown));
 344   li
 345
 346 (** TODO: extend it to some more interesting cases *)
 347 let cost_loop_term_simple env kern_fun stmt lab_before_loop variant cost_body =
 348   (** The number of iteration is bounded by the variant + 1, because
 349       the variant must be positive at the *start* of an iteration *)
 350   let variant = make_binop PlusA variant (Cil.lconstant (My_bigint.one)) in
 351   (** Simple version, just do the multiplication *)
 352   let nbr_iteration = make_at lab_before_loop variant in
 353   (** the nbr_iteration must be positive *)
 354   let nbr_iteration = make_max nbr_iteration (Cil.lzero ()) in
 355   let sum = make_binop Mult nbr_iteration cost_body in
 356
 357   (** make the cost invariant of the loop *)
 358   let remaining_nbr_iteration = make_max variant (Cil.lzero ()) in
 359   (** ensures cost <= \old(cost) +
 360       ([nbr_iteration]-[remaining_nbr_iteration]) * [cost_body] *)
 361   let cost_var = Logic_const.tvar env.env_cost_var in
 362   let old_cost = make_at lab_before_loop cost_var in
 363   let cost_iterations =
 364     make_binop Mult
 365       (make_binop MinusA nbr_iteration remaining_nbr_iteration)
 366       cost_body in
 367   let new_cost = make_binop PlusA old_cost cost_iterations in
 368   let new_cost = simplify_term new_cost in
 369   let invariant = Logic_const.prel (Rle, cost_var, new_cost) in
 370   let annot =
 371     Logic_const.new_code_annotation
 372       (AInvariant ([time_cost_behavior],true,invariant)) in
 373   Annotations.add kern_fun stmt [Ast.self] (User annot);
 374   sum
 375
 376 let cost_loop_term_complexe
 377     env kern_fun stmt lab_before_loop variant deps cost_body =
 378   (** the nbr_iteration must be positive *)
 379   let variant = make_max variant (Cil.lzero ()) in
 380   let args = List.map fst deps in (** \phi *)
 381   let targs = List.map Logic_const.tvar args in
 382   let fl = create_fun_loop env deps cost_body in
 383   let app = linteger (tapp fl (variant::targs)) in
 384   let sum = make_at lab_before_loop app in
 385
 386   (** make the cost invariant of the loop *)
 387   (** ensures cost <= \old(cost) +
 388       ([nbr_iteration]-[remaining_nbr_iteration]) * [cost_body] *)
 389   let cost_var = Logic_const.tvar env.env_cost_var in
 390   let old_cost = make_at lab_before_loop cost_var in
 391   let cost_iterations = make_binop MinusA sum app in
 392   let new_cost = make_binop PlusA old_cost cost_iterations in
 393   let new_cost = simplify_term new_cost in
 394   let invariant = Logic_const.prel (Rle, cost_var, new_cost) in
 395   let annot =
 396     Logic_const.new_code_annotation
 397       (AInvariant ([time_cost_behavior],true,invariant)) in
 398   Annotations.add kern_fun stmt [Ast.self] (User annot);
 399   sum
 400
 401 let cost_loop_term env kern_fun stmt lab_before_loop variant deps cost_body =
 402 (*
 403   let const_during_loop = List.for_all (fun (_,_) -> (** TODO *) false) deps in
 404   if const_during_loop
 405   then cost_loop_term_simple env kern_fun stmt lab_before_loop variant cost_body
 406   else cost_loop_term_complexe
 407     env kern_fun stmt lab_before_loop variant deps cost_body
 408 *)
 409   let cost_body = simplify_term cost_body in
 410   match cost_body.term_node with
 411   | TConst _ ->
 412     cost_loop_term_simple env kern_fun stmt lab_before_loop variant cost_body
 413   | _ ->
 414     cost_loop_term_complexe
 415       env kern_fun stmt lab_before_loop variant deps cost_body
 416
 417
 418 (** computing cost of fundec which contain a call to funvar *)
 419 let cost_of_fun_call env funvar args =
 420   (** can't fail since we use the callgraph *)
 421   let cost = Varinfo.Hashtbl.find env.env_fun_cost funvar in
 422   (* match cost.term_node with *)
 423   (* | TConst (CInt64 (_,_,_)) -> cost *)
 424   (* | _ -> *)
 425   (** arguments of the function *)
 426   let formals = Cil.getFormalsDecl funvar in
 427 (*  (** The real arguments are binded using a let and the formal argument are
 428       replaced by fresh variable *)
 429   let letvars = List.map
 430     (fun vi -> Cil.make_temp_logic_var (Ctype vi.vtype))
 431     formals in
 432   let subst = List.fold_left2 (fun map vi v ->
 433     Varinfo.Map.add vi v map) Varinfo.Map.empty formals letvars in
 434   let cost =
 435     Visitor.visitFramacTerm (new subst_lval subst (Project.current ()))
 436       cost in
 437   let cost = List.fold_left2 (fun tlet v arg ->
 438     let logic_info = { l_var_info = v; l_type = None; l_tparams = [];
 439                        l_labels = []; l_profile = [];
 440                        l_body = LBnone; } in
 441     let arg = term_of_exp arg in
 442     let tlet =
 443       Logic_const.term (Tlet (logic_info, arg))
 444         tlet.term_type in
 445     tlet)
 446     cost letvars args in*)
 447   let subst = List.fold_left2 (fun map vi arg ->
 448     try
 449       Varinfo.Map.add vi (term_of_exp arg) map
 450     with Untranslatable_expr _ -> map (** TODO verify that this formal doesn't
 451                                           appear in the cost of the function *)
 452   ) Varinfo.Map.empty formals args in
 453   let cost = remove_logic_label Logic_const.pre_label cost in
 454   let cost =
 455     Visitor.visitFramacTerm (new subst_lval subst (Project.current ()))
 456       cost in
 457   cost
 458
 459 (** Compute the "wp" of a stmt, in fact just make some substitution *)
 460 let stmt_wp stmt term =
 461   (** try to propagate \at(i,Label) *)
 462   match stmt.skind with
 463   | Instr (Set ((Var vi,_),e,_)) ->
 464     begin
 465       try
 466         let t = term_of_exp e in
 467         let subst = Varinfo.Map.singleton vi t in
 468         let term =
 469           Visitor.visitFramacTerm
 470             (new subst_with_label stmt subst (Project.current ()))
 471             term in
 472         term
 473       with exn ->
 474         if !debug then Format.eprintf "can't convert exp %a to term: %a.@."
 475           Cil.defaultCilPrinter#pExp e print_exception exn;
 476         term
 477     end
 478   | _ -> term
 479
 480 let rec stmts_wp bad_stmts stop_stmts stmt term =
 481   if !debug then
 482     Format.printf "stmts_wp sid: %i,@ bad_stmts: %a,@ stop_stmts: %a,@\n"
 483       stmt.sid
 484       Stmt.Set.pretty bad_stmts
 485       Stmt.Set.pretty stop_stmts;
 486   (** statement in last statement *)
 487   if Stmt.Set.mem stmt stop_stmts
 488   then Some term
 489   else if Stmt.Set.mem stmt bad_stmts
 490   then None
 491   else
 492   (** successors *)
 493   let succs_bad_stmts =
 494     match stmt.skind with
 495     | Loop (_,_,_,_,_) -> Stmt.Set.add stmt bad_stmts
 496     | _ -> bad_stmts in
 497   (** Cost of the successors of the instruction *)
 498   let cost_succs =
 499     stmts_wp_succs succs_bad_stmts stop_stmts stmt.succs term in
 500   match cost_succs with
 501   | [] -> None (** can't go in a good state so count nothing *)
 502   | (a::l) -> (** TODO take care of conditions *)
 503     assert (l = []);
 504     let a' = stmt_wp stmt a in
 505     if !debug then
 506       Format.printf "[WP]stmt:@,%a@.a:@,%a@.a':@,%a@."
 507         Cil.defaultCilPrinter#pStmt stmt
 508         Cil.defaultCilPrinter#pTerm a
 509         Cil.defaultCilPrinter#pTerm a';
 510     Some a'
 511
 512 and stmts_wp_succs bad_stmts stop_stmts stmts term =
 513   let fold acc stmt =
 514     match stmts_wp bad_stmts stop_stmts stmt term with
 515     | None -> acc
 516     | Some t -> t::acc in
 517   List.fold_left fold [] stmts
 518
 519
 520 (** We go through the cfg we assume that:
 521     - all functions called have a cost already computed
 522     - no implicit loop (goto), all are explicit Loop
 523     - all loops have an invariant (given by the user or previously computed for
 524     for-loops)
 525
 526     We iterate on the cfg except when arriving on a loop where we compute the
 527     body alone and after that go to the next statements (the break statement)
 528
 529    break_statement in which statement to stop the sum (for loop)
 530  *)
 531
 532
 533 let rec find_variant = function
 534   | [] -> None
 535   | {annot_content = AVariant (t,_)}::_ -> Some t
 536   | _::l -> find_variant l
 537
 538 (** TODO: cache the statement already done after if-then-else
 539     (otherwise exponential) *)
 540 (** return None if no path arrive to a good_statement or don't go through
 541     a bad_statetement *)
 542 let rec cfg_sum env kern_fun bad_stmts stop_stmts stmt =
 543   if !debug then
 544     Format.printf "sid: %i,@ bad_stmts: %a,@ stop_stmts: %a,@\n"
 545       stmt.sid
 546       Stmt.Set.pretty bad_stmts
 547       Stmt.Set.pretty stop_stmts;
 548   (** statement in last statement *)
 549   if Stmt.Set.mem stmt stop_stmts
 550   then Some (Cil.lzero ())
 551   else if Stmt.Set.mem stmt bad_stmts
 552   then None
 553   else
 554   (** successors *)
 555   let succs_bad_stmts =
 556     match stmt.skind with
 557     | Loop (_,_,_,_,_) -> Stmt.Set.add stmt bad_stmts
 558     | _ -> bad_stmts in
 559   (** Cost of the successors of the instruction *)
 560   let cost_succs =
 561     cfg_sum_succs env kern_fun succs_bad_stmts stop_stmts
 562       stmt.succs in
 563   match cost_succs with
 564   | None -> None (** can't go in a good state so count nothing *)
 565   | Some cost_succs ->
 566   (** Cost of the instruction *)
 567   let cost_instr =
 568     match stmt.skind with
 569     (* (\** call to cost_incr *\) *) (** cost_incr is an usual function *)
 570     (* | Instr *)
 571     (*     (Call (None, *)
 572     (*                      { enode = *)
 573     (*                          Lval (Var var, _)} , *)
 574     (*                      [cost], _)) *)
 575     (*     when var.vname = env.env_cost_incr_name -> *)
 576     (*   term_of_cost_expr cost *)
 577     (** function call *)
 578     | Instr
 579         (Call (_, { enode =
 580             Lval (Var var, _)},
 581                          args,_)) ->
 582       cost_of_fun_call env var args
 583     (** loops *)
 584     | Loop (_,body,_,_,_) ->
 585       cost_loop env kern_fun bad_stmts stop_stmts stmt body
 586     | _ -> Cil.lzero () in
 587   (** normalize the cost of the instruction regarding the labels *)
 588   let labels = NormAtLabels.labels_stmt_pre stmt in
 589   let cost_instr = NormAtLabels.preproc_annot_term labels cost_instr in
 590   let cost_succs = stmt_wp stmt cost_succs in
 591   let sum = make_binop PlusA cost_instr cost_succs in
 592   (** remove the at that point to this statement we don't know the value at
 593       this point perhaps we will know before ( use Here?? ) *)
 594   let sum =
 595     Visitor.visitFramacTerm
 596       (new remove_stmt_label stmt (Project.current ()))
 597       sum in
 598   if !debug then
 599     Format.printf "Stmt %i sum=%a@."
 600       stmt.sid Term.pretty sum;
 601   Some sum
 602
 603 and cfg_sum_succs env kern_fun bad_stmts stop_stmts stmts =
 604   let fold cost stmt =
 605     let cost_succ = cfg_sum env kern_fun bad_stmts stop_stmts stmt in
 606     make_max_opt cost cost_succ in
 607   List.fold_left fold None stmts
 608
 609 and cost_loop env kern_fun bad_stmts stop_stmts stmt body =
 610   (** the first one perhaps not needed *)
 611   let bad_stmts = Stmt.Set.union bad_stmts stop_stmts in
 612   let stop_stmts = Stmt.Set.singleton stmt in
 613   let cost_body =
 614     cfg_sum_succs env kern_fun bad_stmts stop_stmts stmt.succs in
 615   let cost_body = match cost_body with
 616     | None -> (* no cycle in fact *) Cil.lzero ()
 617     | Some cost -> simplify_term cost in
 618   (** compute free variable and compute their modification by the loop body *)
 619   let deps = freevar Logic_var.Set.empty cost_body in
 620   let deps =
 621     let fold e acc =
 622       let result =
 623         stmts_wp_succs bad_stmts stop_stmts stmt.succs (Logic_const.tvar e)  in
 624       match result with
 625       | [] -> assert false (** No cycle? impossible it find one before *)
 626       | t::l ->
 627         assert (l = []); (* TODO *)
 628         (e, t)::acc in
 629     Logic_var.Set.fold fold deps [] in
 630   (** this stmt is the continue *)
 631   let annots = Annotations.get_filter Logic_utils.is_variant stmt in
 632   let variant = match annots with
 633     | [] -> (** TODO put it somewhere else *)
 634       begin match extract_variant body with
 635       | None ->
 636         Format.printf
 637           "Can't@ compute@ cost@ without@ variant@ for@ statement:@,%a@."
 638           Stmt.pretty stmt; exit 1
 639       | Some variant ->
 640         let annot =
 641           Logic_const.new_code_annotation (AVariant (variant,None)) in
 642         Annotations.add kern_fun stmt [Ast.self] (User annot);
 643         variant end
 644     | ( User { annot_content =
 645         AVariant (v,_) }
 646           | AI (_, { annot_content =
 647               AVariant (v,_) }) (** usefule case ? *)
 648     )
 649       :: _ ->
 650       let v = NormAtLabels.preproc_annot_term
 651         (NormAtLabels.labels_loop_inv stmt) v in
 652       let v = remove_logic_label Logic_const.here_label v in
 653       v
 654     | _ -> assert false (* result of the filter *)
 655   in
 656   if stmt.labels = [] then
 657     stmt.labels <- (** ugly but... *)
 658       Label("__stmt_"^(string_of_int stmt.sid),Cil.builtinLoc,false)::
 659       stmt.labels;
 660   let label_before_loop = StmtLabel (ref stmt) in
 661   cost_loop_term env kern_fun stmt label_before_loop variant deps cost_body
 662
 663 let make_leq_cost env sum =
 664     (** ensures cost <= \old(cost) + [sum] *)
 665     let cost_var = Logic_const.tvar env.env_cost_var in
 666     let old_cost = Logic_const.told cost_var in
 667     let new_cost = Logic_const.term
 668       (Cil_types.TBinOp (Cil_types.PlusA, old_cost, sum)) Linteger in
 669     let post = Logic_const.prel (Rle, cost_var, new_cost) in
 670     let post = Logic_const.new_predicate post in
 671     post
 672
 673 let fun_sum env vi kernel_fun =
 674   let fst_stmt = Kernel_function.find_first_stmt kernel_fun in
 675   let last_stmt = Kernel_function.find_return kernel_fun in
 676   let bad_stmts = Stmt.Set.empty in
 677   let stop_stmts = Stmt.Set.singleton last_stmt in
 678   let sum = cfg_sum env kernel_fun bad_stmts stop_stmts fst_stmt in
 679   let sum = match sum with
 680     | None -> assert false (* Oups return not achievable?? *)
 681           (* Infinity!! *)
 682     | Some sum ->
 683       let sum = simplify_term sum in
 684       let sum = Logic_const.told sum in (** add old and push it *)
 685       let labels = NormAtLabels.labels_fct_post in
 686       let sum = NormAtLabels.preproc_annot_term labels sum in
 687       sum in
 688   if !debug then
 689     Format.printf "@[<hov 3>sum of %a: %a@]@."
 690       Cil.defaultCilPrinter#pVar vi
 691       Cil.defaultCilPrinter#pTerm sum;
 692 (** add postcondition about cost *)
 693   let mod_funspec funspec =
 694     let post = make_leq_cost env sum in
 695     let behavior =
 696       Cil.mk_behavior ~name:time_cost_behavior ~post_cond:[Normal, post] () in
 697     {funspec with spec_behavior = behavior::funspec.spec_behavior;}
 698   in
 699   Kernel_function.set_spec kernel_fun mod_funspec;
 700   sum
 701
 702 (** Before computing the sum check that the user doesn't specify the cost.
 703     In this case use it *)
 704 let fun_sum env vi =
 705   init_loop_name env "fun_sum";
 706   let kernel_fun = Globals.Functions.get vi in
 707   let funspec = Kernel_function.get_spec kernel_fun in
 708   let rec find_cost = function
 709     | [] -> None
 710     | {b_name = name;
 711        b_requires = [];
 712        b_assumes = []; (** TODO? allow more general contract? *)
 713        (** ensores __cost <= \old(__cost) + t; *)
 714        b_post_cond = [_,{ip_content=Prel
 715            (Rle,
 716             {term_node = (TLval(TVar cost_var,TNoOffset))},
 717             {term_node = TBinOp(PlusA,{term_node = Tat(
 718               {term_node = (TLval(TVar cost_var2,TNoOffset))}, old_label)},
 719                                 t)})}]
 720       }::_ when name = time_cost_behavior &&
 721              Logic_var.equal cost_var  env.env_cost_var &&
 722              Logic_var.equal cost_var2 env.env_cost_var &&
 723              Logic_label.equal old_label Logic_const.old_label
 724            -> Some t
 725     | _::l -> find_cost l in
 726   match find_cost funspec.spec_behavior with
 727   | None -> fun_sum env vi kernel_fun
 728   | Some sum ->
 729     if !debug then
 730       Format.printf "@[<hov 3>User sum of %a: %a@]@."
 731         Cil.defaultCilPrinter#pVar vi
 732         Cil.defaultCilPrinter#pTerm sum;
 733     let labels = NormAtLabels.labels_fct_post in
 734     let sum = NormAtLabels.preproc_annot_term labels sum in
 735     sum
 736
 737 let initialize _tmp_prefix _fname cost_var cost_incr _extern_costs =
 738   (** TODO? use extern_costs for initializing env_fun_cost ? *)
 739   let callgraph = Callgraph.computeGraph (Ast.get ()) in
 740   if !debug then
 741     Printf.printf "callgraph size: %a\n%!" Callgraph.printGraph callgraph;
 742   let env = { env_fun_cost = Varinfo.Hashtbl.create 10;
 743               env_cost_incr_name = cost_incr;
 744               env_cost_var = cost_var;
 745               env_loop_name = dumb_env_loop_name} in
 746   let rec iter : 'a. 'a -> Callgraph.callnode -> unit = fun _ callnode ->
 747     match callnode.Callgraph.cnInfo with
 748     | Callgraph.NIVar (vi,{contents = true }) ->
 749       if not (Varinfo.Hashtbl.mem env.env_fun_cost vi) then begin
 750         Inthash.iter iter callnode.Callgraph.cnCallees;
 751         let sum = fun_sum env vi in
 752         Varinfo.Hashtbl.add env.env_fun_cost vi sum
 753       end
 754     | _ -> () (** put an undefined constant here for top *)
 755   in
 756   (** add the cost of cost_incr *)
 757   let cost_incr = Hashtbl.find callgraph cost_incr in
 758   let cost_incr = match cost_incr.Callgraph.cnInfo with
 759     | Callgraph.NIVar (vi,_) -> vi
 760     | _ -> assert false (* cost_incr must be at least declared *) in
 761   let arg_cost_incr = List.hd (Cil.getFormalsDecl cost_incr) in
 762   let sum_cost_incr = Logic_const.tvar (Cil.cvar_to_lvar arg_cost_incr) in
 763   let post_cost_incr = make_leq_cost env sum_cost_incr in
 764   Kernel_function.set_spec (Globals.Functions.get cost_incr) (fun funspec ->
 765     let assigns =
 766       Writes [Logic_const.(new_identified_term (tvar cost_var)), FromAny] in
 767     let behavior =
 768       Cil.mk_behavior ~name:time_cost_behavior
 769         ~post_cond:[Normal, post_cost_incr]
 770         ~assigns () in
 771     {funspec with spec_behavior = behavior::funspec.spec_behavior;} );
 772   Varinfo.Hashtbl.add env.env_fun_cost cost_incr sum_cost_incr;
 773   (** make the other functions *)
 774   Hashtbl.iter iter callgraph
 775
 776
 777 (*** Main ***)
 778
 779 let cost ((fname, _), _, cost_time, _) =
 780   try
 781     if !debug then Printf.printf "Initialize Cost\n%!" ;
 782     let cost_var =
 783       Cil.cvar_to_lvar (Globals.Vars.find_from_astinfo
 784                           cost_time.Cerco.cost_id VGlobal) in
 785     initialize "__tmp" fname cost_var
 786       cost_time.Cerco.cost_incr cost_time.Cerco.extern_costs;
 787   with e -> Format.eprintf "** ERROR: %a.@." print_exception_raise e