Ignore:
Timestamp:
Oct 25, 2011, 4:11:11 PM (9 years ago)
Author:
ayache
Message:

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

Location:
Deliverables/D2.2/8051/src/clight
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/clight/clightAnnotator.ml

    r818 r1462  
    130130  let Clight.Expr (e, t) = e in
    131131  match e with
    132     | Clight.Ecost (lbl, e) when CostLabel.Map.find lbl cost_mapping = 0 ->
     132    | Clight.Ecost (lbl, e)
     133        when CostLabel.Map.mem lbl cost_mapping &&
     134             CostLabel.Map.find lbl cost_mapping = 0 ->
    133135        e
    134136    | _ ->
     
    300302  (cost_incr, Clight.Internal cfun)
    301303
     304(* Create a fresh uninitialized cost variable for each external function. This
     305   will be used by the Cost plug-in of the Frama-C platform. *)
     306
     307let extern_cost_variables make_unique functs =
     308  let prefix = "_cost_of_" in
     309  let f (decls, map) (_, def) = match def with
     310    | Clight.Internal _ -> (decls, map)
     311    | Clight.External (id, _, _) ->
     312      let new_var = make_unique (prefix ^ id) in
     313      (decls @ [cost_decl new_var], StringTools.Map.add id new_var map) in
     314  List.fold_left f ([], StringTools.Map.empty) functs
     315
    302316let save_tmp tmp_file s =
    303317  let cout = open_out tmp_file in
     
    316330  (* Create a fresh 'cost' variable. *)
    317331  let names = names p in
    318   let cost_id = StringTools.Gen.fresh_prefix names cost_id_prefix in
     332  let make_unique = StringTools.make_unique names in
     333  let cost_id = make_unique cost_id_prefix in
    319334  let cost_decl = cost_decl cost_id in
     335
     336  (* Create a fresh uninitialized global variable for each extern function. *)
     337  let (extern_cost_decls, extern_cost_variables) =
     338    extern_cost_variables make_unique p.Clight.prog_funct in
    320339
    321340  (* Define an increment function for the cost variable. *)
     
    330349
    331350  (* Glue all this together. *)
    332   let prog_vars = cost_decl :: p.Clight.prog_vars in
     351  let prog_vars = cost_decl :: extern_cost_decls @ p.Clight.prog_vars in
    333352  let prog_funct = cost_incr_def :: prog_funct in
    334353  let p' =
     
    343362  let res = ClightParser.process tmp_file in
    344363  Misc.SysExt.safe_remove tmp_file ;
    345   (res, cost_id, cost_incr)
     364  (res, cost_id, cost_incr, extern_cost_variables)
  • Deliverables/D2.2/8051/src/clight/clightAnnotator.mli

    r818 r1462  
    66    Then, each cost label in the program is replaced by an increment of the cost
    77    variable, following the mapping [cost_map]. The function also returns the
    8     name of the cost variable and the name of the cost increment function. *)
     8    name of the cost variable, the name of the cost increment function, and a
     9    fresh uninitialized global (cost) variable associated to each extern
     10    function. *)
    911
    1012val instrument : Clight.program -> int CostLabel.Map.t ->
    11                  Clight.program * string * string
     13                 Clight.program * string * string * string StringTools.Map.t
    1214
    1315val cost_labels : Clight.program -> CostLabel.Set.t
  • Deliverables/D2.2/8051/src/clight/clightParser.ml

    r818 r1462  
    1 let process file =
    2   let tmp_file1 = Filename.temp_file "cparser1" ".c"
    3   and tmp_file2 = Filename.temp_file "cparser2" ".i"
     1
     2let process ?is_lustre_file ?remove_lustre_externals file =
     3  let temp_dir = Filename.dirname file in
     4  let tmp_file1 = Filename.temp_file ~temp_dir "cparser1" ".c"
     5  and tmp_file2 = Filename.temp_file ~temp_dir "cparser2" ".i"
    46  and prepro_opts = [] in
    57
     
    810    try
    911      let oc = open_out tmp_file1 in
     12      if is_lustre_file = Some true || remove_lustre_externals = Some true then
     13        output_string oc "#include<string.h>";
    1014      output_string oc Primitive.prototypes ;
    1115      close_out oc
     
    1519       (Filename.quote file) (Filename.quote tmp_file1)) in
    1620  if rc <> 0 then (
     21    (*
    1722    Misc.SysExt.safe_remove tmp_file1;
     23    *)
    1824    failwith "Error adding primitive prototypes."
    1925  );
     
    2632       (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in
    2733  if rc <> 0 then (
     34    (*
    2835    Misc.SysExt.safe_remove tmp_file1;
    2936    Misc.SysExt.safe_remove tmp_file2;
     37    *)
    3038    failwith "Error calling gcc."
    3139  );
     
    3341  (* C to Cil *)
    3442  let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in
    35   Misc.SysExt.safe_remove tmp_file1;
    36   Misc.SysExt.safe_remove tmp_file2;
    3743  match r with
    3844    | None -> failwith "Error during C parsing."
     
    4147      (match ClightFromC.convertProgram p with
    4248        | None -> failwith "Error during C to Clight pass."
    43         | Some(pp) -> pp
    44       )
     49        | Some(pp) ->
     50          Misc.SysExt.safe_remove tmp_file1;
     51          Misc.SysExt.safe_remove tmp_file2;
     52          if remove_lustre_externals = Some true then ClightLustre.simplify pp
     53          else pp)
  • Deliverables/D2.2/8051/src/clight/clightParser.mli

    r486 r1462  
     1
    12(** This module implements a parser for [C] based on [gcc] and
    23    [CIL]. *)
    34
    4 (** [process filename] parses the contents of [filename] to obtain
    5     an abstract syntax tree that represents a Clight program. *)
    6 val process : string -> Clight.program
     5(** [process ?is_lustre_file ?remove_lustre_externals filename] parses the
     6    contents of [filename] to obtain an abstract syntax tree that represents a
     7    Clight program. *)
     8val process :
     9  ?is_lustre_file:bool -> ?remove_lustre_externals:bool ->
     10  string -> Clight.program
  • Deliverables/D2.2/8051/src/clight/clightSwitch.ml

    r818 r1462  
    66let type_of (Clight.Expr (_, t)) = t
    77
    8 let rec simplify_switch e cases stmts = match cases, stmts with
    9   | Clight.LSdefault _, stmt :: _ -> stmt
    10   | Clight.LScase (i, _, lbl_stmts), stmt :: stmts ->
    11     let next_cases = simplify_switch e lbl_stmts stmts in
    12     let ret_type = Clight.Tint (Clight.I32, AST.Signed) in
    13     let cst_i = Clight.Expr (Clight.Econst_int i, type_of e) in
    14     let test = Clight.Expr (Clight.Ebinop (Clight.Oeq, e, cst_i), ret_type) in
    15     Clight.Sifthenelse (test, stmt, next_cases)
    16   | _ -> assert false (* do not use on these arguments *)
    178
    189let f_expr e _ = e
    1910
    20 let f_stmt stmt sub_exprs_res sub_stmts_res = match stmt, sub_stmts_res with
    21   | Clight.Sswitch (e, cases), sub_stmts -> simplify_switch e cases sub_stmts
    22   | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
     11let f_stmt lbl stmt sub_exprs_res sub_stmts_res =
     12  match stmt, sub_stmts_res with
     13    | Clight.Sbreak, _ -> Clight.Sgoto lbl
     14    | Clight.Swhile _, _ | Clight.Sdowhile _, _
     15    | Clight.Sfor _, _ | Clight.Sswitch _, _ -> stmt
     16    | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
    2317
    24 let simplify_statement = ClightFold.statement2 f_expr f_stmt
     18let replace_undeep_break lbl = ClightFold.statement2 f_expr (f_stmt lbl)
    2519
    26 let simplify_fundef = function
     20
     21let add_starting_lbl fresh stmt =
     22  let lbl = fresh () in
     23  (lbl, Clight.Slabel (lbl, stmt))
     24
     25let add_starting_lbl_list fresh stmts = List.map (add_starting_lbl fresh) stmts
     26
     27let add_ending_goto lbl stmt =
     28  Clight.Ssequence (stmt, Clight.Slabel (lbl, Clight.Sskip))
     29
     30let make_sequence stmts =
     31  let f sequence stmt = Clight.Ssequence (sequence, stmt) in
     32  List.fold_left f Clight.Sskip stmts
     33
     34let simplify_switch fresh e cases stmts =
     35  let exit_lbl = fresh () in
     36  let (lbls, stmts) = List.split (add_starting_lbl_list fresh stmts) in
     37  let stmts = List.map (replace_undeep_break exit_lbl) stmts in
     38  let rec aux cases lbls = match cases, lbls with
     39    | Clight.LSdefault _, lbl :: _ -> [Clight.Sgoto lbl]
     40    | Clight.LScase (i, _, cases), lbl :: lbls ->
     41      let next_cases = aux cases lbls in
     42      let ret_type = Clight.Tint (Clight.I32, AST.Signed) in
     43      let cst_i = Clight.Expr (Clight.Econst_int i, type_of e) in
     44      let test = Clight.Expr (Clight.Ebinop (Clight.Oeq, e, cst_i), ret_type) in
     45      Clight.Sifthenelse (test, Clight.Sgoto lbl, Clight.Sskip) :: next_cases
     46    | _ ->
     47      (* Do not use on these arguments: wrong list size. *)
     48      assert false in
     49  add_ending_goto exit_lbl (make_sequence ((aux cases lbls) @ stmts))
     50
     51let f_expr e _ = e
     52
     53let f_stmt fresh stmt sub_exprs_res sub_stmts_res =
     54  match stmt, sub_stmts_res with
     55    | Clight.Sswitch (e, cases), sub_stmts ->
     56      simplify_switch fresh e cases sub_stmts
     57    | _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
     58
     59let simplify_statement fresh = ClightFold.statement2 f_expr (f_stmt fresh)
     60
     61let simplify_fundef fresh = function
    2762  | Clight.Internal cfun ->
    28     let cfun =
    29       { cfun with Clight.fn_body = simplify_statement cfun.Clight.fn_body } in
    30     Clight.Internal cfun
     63    let fn_body = simplify_statement fresh cfun.Clight.fn_body in
     64    Clight.Internal { cfun with Clight.fn_body = fn_body }
    3165  | fundef -> fundef
    3266
    3367let simplify p =
    34   let f (id, fundef) = (id, simplify_fundef fundef) in
     68  let labels = ClightAnnotator.all_labels p in
     69  let fresh = StringTools.make_fresh labels "_tmp_switch" in
     70  let f (id, fundef) = (id, simplify_fundef fresh fundef) in
    3571  { p with Clight.prog_funct = List.map f p.Clight.prog_funct }
  • Deliverables/D2.2/8051/src/clight/clightToCminor.ml

    r818 r1462  
    217217let sort_params = sort_vars Param (Some (fun offset -> ParamStack offset))
    218218
    219 let sort_globals stack_vars globals var_locs =
     219let sort_globals stack_vars globals functs var_locs =
    220220  let globals = List.map (fun ((id, _), ctype) -> (id, ctype)) globals in
     221  let f_functs (id, fundef) =
     222    let (params, return) =  match fundef with
     223      | Clight.Internal cfun ->
     224        (List.map snd cfun.Clight.fn_params, cfun.Clight.fn_return)
     225      | Clight.External (_, params, return) -> (params, return) in
     226    (id, Clight.Tfunction (params, return)) in
     227  let functs = List.map f_functs functs in
     228  let globals = globals @ functs in
    221229  sort_vars Global None stack_vars globals var_locs
    222230
     
    225233   globals. *)
    226234
    227 let sort_variables globals cfun =
     235let sort_variables globals functs cfun =
    228236  let stack_vars = stack_vars cfun in
    229237  let var_locs = empty_var_locs in
    230   let var_locs = sort_globals stack_vars globals var_locs in
     238  let var_locs = sort_globals stack_vars globals functs var_locs in
    231239  let var_locs = sort_params stack_vars cfun.Clight.fn_params var_locs in
    232240  let var_locs = sort_locals stack_vars cfun.Clight.fn_vars var_locs in
     
    439447
    440448and translate_addrof_ident res_type var_locs id =
     449  assert (mem_var_locs id var_locs) ;
    441450  match find_var_locs id var_locs with
    442     | (Local, _) | (Param, _) -> assert false (* type error *)
     451    | (Local, _) | (Param, _) -> assert false (* location error *)
    443452    | (LocalStack off, _) | (ParamStack off, _) ->
    444453      Cminor.Expr (add_stack off, res_type)
     
    585594  fold_var_locs f var_locs body
    586595
    587 let translate_internal fresh globals cfun =
    588   let var_locs = sort_variables globals cfun in
     596let translate_internal fresh globals functs cfun =
     597  let var_locs = sort_variables globals functs cfun in
    589598  let params =
    590599    List.map (fun (x, t) -> (x, sig_type_of_ctype t)) cfun.Clight.fn_params in
     
    602611                   AST.res = type_return_of_ctype return } }
    603612
    604 let translate_funct fresh globals (id, def) =
     613let translate_funct fresh globals functs (id, def) =
    605614  let def = match def with
    606     | Clight.Internal ff -> Cminor.F_int (translate_internal fresh globals ff)
     615    | Clight.Internal ff ->
     616      Cminor.F_int (translate_internal fresh globals functs ff)
    607617    | Clight.External (i,p,r) -> Cminor.F_ext (translate_external i p r) in
    608618  (id, def)
     
    610620let translate p =
    611621  let fresh = ClightAnnotator.make_fresh "_tmp" p in
     622  let translate_funct =
     623    translate_funct fresh p.Clight.prog_vars p.Clight.prog_funct in
    612624  { Cminor.vars = List.map translate_global p.Clight.prog_vars ;
    613     Cminor.functs =
    614       List.map (translate_funct fresh p.Clight.prog_vars) p.Clight.prog_funct ;
     625    Cminor.functs = List.map translate_funct p.Clight.prog_funct ;
    615626    Cminor.main = p.Clight.prog_main }
Note: See TracChangeset for help on using the changeset viewer.