source: Deliverables/D5.1-5.3/cost-plug-in/plugin/cerco.ml @ 1679

Last change on this file since 1679 was 1679, checked in by ayache, 9 years ago

Frama-C plug-in (sources+documentation)

File size: 3.5 KB
Line 
1
2(** This file makes the interface between the cost plug-in and CerCo's
3    compiler. *)
4
5let rec extern_cost_variables cin =
6  try
7    let s = input_line cin in
8    assert (String.contains s ' ') ;
9    let i = String.index s ' ' in
10    assert (String.length s > i + 1) ;
11    let fun_name = String.sub s 0 i in
12    let var_name = String.sub s (i+1) (String.length s - (i+1)) in
13    Misc.String.Map.add fun_name var_name (extern_cost_variables cin)
14  with End_of_file -> Misc.String.Map.empty
15
16(** [multifile_exists exts filename] returns true if and only if the file name
17    [filename] concatenated with an extension from the list [exts] exists. *)
18
19let multifile_exists exts filename =
20  let f b ext = b || (Sys.file_exists (filename ^ ext)) in
21  List.fold_left f false exts
22
23(** [fresh_multifile exts filename] returns a file name whose base is [filename]
24    and suffixed with an integer such that the result is fresh when concatenated
25    with any extension from the list [exts]. *)
26
27let fresh_multifile exts filename =
28  if not (multifile_exists exts filename) then filename
29  else
30    let rec aux i =
31      let new_filename = filename ^ (string_of_int i) in
32      if not (multifile_exists exts new_filename) then new_filename
33      else aux (i+1) in
34    aux 0
35
36(** [index_of e l] returns the index of the element [e] in the list [l], if
37    any. *)
38
39let index_of e l =
40  let f (i, res) e' =
41    let res' = if e' = e then Some i else res in
42    (i+1, res') in
43  match snd (List.fold_left f (0, None) l) with
44    | None -> raise (Failure "Cerco.index_of")
45    | Some i -> i
46
47let acc_option lustre_option lustre_verify_option lustre_test_option =
48  if lustre_verify_option || lustre_test_option then "-remove-lustre-externals "
49  else
50    if lustre_option then "-lustre "
51    else ""
52
53(** [apply (filename, _)] apply CerCo's compiler on the file [filename]. The
54    result is a new C file with cost annotations, the name of the cost
55    variable, and the name of the cost update function. *)
56
57let apply lustre_option lustre_verify_option lustre_test_option (filename, _)
58    : Cabs.file * string * string * string * string Misc.String.Map.t =
59  let annotated_ext = "-annotated.c" in
60  let asm_ext = ".s" in
61  let cerco_ext = ".cerco" in
62  let hex_ext = ".hex" in
63  let exts = [annotated_ext ; asm_ext ; cerco_ext ; hex_ext] in
64  let tmp_filename = Filename.chop_extension filename in
65  let tmp_filename = fresh_multifile exts tmp_filename in
66  let acc_option =
67    acc_option lustre_option lustre_verify_option lustre_test_option in
68  let com_acc =
69    "acc -a " ^ acc_option ^ "-o " ^ tmp_filename ^ " " ^ filename in
70  let ext_tmp_filename ext = tmp_filename ^ ext in
71  let tmp_filenames = List.map ext_tmp_filename exts in
72  let index_of s = List.nth tmp_filenames (index_of s exts) in
73  let c_tmp_filename = index_of annotated_ext in
74  let s_tmp_filename = index_of asm_ext in
75  let cerco_tmp_filename = index_of cerco_ext in
76  (* let hex_tmp_filename = index_of hex_ext in *)
77  let rm () =
78    let com =
79      "rm -rf " ^ s_tmp_filename ^ " " ^
80        (if lustre_test_option then "" else cerco_tmp_filename)
81    (* ^ " " ^ hex_tmp_filename *) in
82    ignore (Sys.command com) in
83  if Sys.command com_acc <> 0 then
84    (rm () ; failwith "Error calling acc.")
85  else
86    (let (_, file) = Frontc.parse c_tmp_filename () in
87     let cin = open_in cerco_tmp_filename in
88     let cost_id = input_line cin in
89     let cost_incr = input_line cin in
90     let extern_cost_variables = extern_cost_variables cin in
91     close_in cin ;
92     rm () ;
93     (file, filename, cost_id, cost_incr, extern_cost_variables))
Note: See TracBrowser for help on using the repository browser.