source: Deliverables/D5.1/cost-plug-in/wrapper/main.ml @ 1462

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

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

File size: 11.7 KB
Line 
1
2
3let error_prefix = "Main"
4let error = Error.global_error error_prefix
5
6
7let log_file = Filename.temp_file "log" ""
8
9
10let print_verbose i s =
11  if Options.get_verbose_level () >= i then Printf.printf "%s%!" s
12let print_verbose1 = print_verbose 1
13let print_verbose2 = print_verbose 2
14
15
16let exec cmd error_callback error_msg success_callback success_msg =
17  print_verbose2 ("  -> executing command \"" ^ cmd ^ "\"...\n") ;
18  let res = Sys.command cmd in
19  if res <> 0 then (error_callback () ; error error_msg)
20  else
21    (print_verbose1 (success_msg ^ "\n") ;
22     success_callback ())
23
24
25let has_extension filename =
26  try ignore (Filename.chop_extension filename) ; true
27  with Invalid_argument ("Filename.chop_extension") -> false
28
29let lustre_compilation filename node =
30  print_verbose1
31    ("Compiling node " ^ node ^ " of Lustre file " ^ filename ^ "...\n") ;
32  let filename_quote = Filename.quote filename in
33  let base =
34    if has_extension filename then Filename.chop_extension filename
35    else filename in
36  let base =
37    Misc.fresh_base base
38      [".c" ; "-annotated.c" ; ".s" ; ".hex" ; ".cerco" ; ".cost_results" ;
39       ".jessie_results" ; "-annotated_test.c" ; "-annotated_test.s" ;
40       "-annotated_test.hex" ; "-annotated_test.results"] in
41  let res_file = base ^ ".c" in
42  let res_file_quote = Filename.quote res_file in
43  let cmd =
44    "lus2c " ^ filename_quote ^ " " ^ node ^ " -o " ^ res_file_quote ^ " >> " ^
45      log_file in
46  let error_callback () = () in
47  let error_msg =
48    "Failed to compile node " ^ node ^ " of Lustre file " ^ filename ^ "." in
49  let success_callback () = res_file in
50  let success_msg = "Done. Result is in file " ^ res_file ^ "." in
51  exec cmd error_callback error_msg success_callback success_msg
52
53
54let extract_inputs_booleans filename =
55  print_verbose1
56    ("Extracting boolean inputs from file " ^ filename ^ "...\n") ;
57  try
58    let ic = open_in filename in
59    let rec inputs_booleans b =
60      try
61        let str_inputs = Str.regexp " *//INPUTS *" in
62        (* let str_registers = Str.regexp " *//REGISTERS *" in *)
63        let is_input_start s =
64          Str.string_match str_inputs s 0
65          (* || Str.string_match str_registers s 0 *) in
66        let str_outputs = Str.regexp " *//OUTPUTS *" in
67        let str_acc = Str.regexp ".*}.*" in
68        let is_input_end s =
69          Str.string_match str_outputs s 0 ||
70          Str.string_match str_acc s 0 in
71        let str_boolean = Str.regexp "   _boolean .*;" in
72        let str_input = Str.regexp "   [^ ]* .*;" in
73        let extract_input s =
74          let i = String.index_from s 3 ' ' in
75          String.sub s (i+1) (String.length s - (i+2)) in
76        let s = input_line ic in
77        let (added_input, added_boolean) =
78          let extract cond = if b && cond then [extract_input s] else [] in
79          (extract (Str.string_match str_input s 0),
80           extract (Str.string_match str_boolean s 0)) in
81        let next_b = (b || (is_input_start s)) && (not (is_input_end s)) in
82        let (inputs, booleans) = inputs_booleans next_b in
83        (added_input @ inputs, added_boolean @ booleans)
84      with End_of_file -> close_in ic ; ([], []) in
85    let res = inputs_booleans false in
86    print_verbose1 "Done.\n" ;
87    res
88  with Sys_error _ ->
89    error ("Could not extract boolean inputs from file " ^ filename ^ ".")
90
91
92let framac_option () =
93  "-cost-lustre " ^
94    (if Options.test_requested () then "-cost-lustre-test " else "") ^
95    (if Options.verify_requested () then "-cost-lustre-verify " else "")
96
97let cost_plugin filename =
98  print_verbose1 ("Running Cost plug-in on file " ^ filename ^ "...\n") ;
99  let filename_quote = Filename.quote filename in
100  let base =
101    if has_extension filename then Filename.chop_extension filename
102    else filename in
103  let annotated_file = base ^ "-annotated.c" in
104  let results_file = base ^ ".cost_results" in
105  let hex_file = base ^ ".hex" in
106  let cerco_file = base ^ ".cerco" in
107  let option = framac_option () in
108  let cmd = "frama-c -cost " ^ option ^ filename_quote ^ " >> " ^
109      log_file in
110  let error_callback () = () in
111  let error_msg = "Failed to run Cost plug-in on file " ^ filename ^ "." in
112  let success_callback () = (annotated_file, results_file, cerco_file) in
113  let success_msg =
114    "Done. Annotations are in file " ^ annotated_file ^
115      ", object code is in file " ^ hex_file ^
116      ", cost results are in file " ^ results_file ^
117      (if Options.test_requested () then
118          ", CerCo information is in file " ^ cerco_file
119       else "") ^
120      "." in
121  exec cmd error_callback error_msg success_callback success_msg
122
123
124let print_step_result filename =
125  print_verbose1 ("Reading the cost results in file " ^ filename ^ "...\n") ;
126  let ic = open_in filename in
127  let rec aux () =
128    try
129      let s = input_line ic in
130      if String.contains s ' ' then
131        let i = String.index s ' ' in
132        let fun_name = String.sub s 0 i in
133        let cost = String.sub s (i+1) ((String.length s) - (i+1)) in
134        let suffix = "_step" in
135        let l = String.length fun_name in
136        let l' = String.length suffix in
137        if l > l' && String.sub s (l - l') l' = suffix then
138          (print_verbose1 "Done.\n" ;
139           Printf.printf
140             "The cost of the %s function is at most %s (not verified).\n%!"
141             fun_name cost ;
142           (fun_name, cost))
143        else aux ()
144      else error ("Bad format of result file " ^ filename ^ ".")
145    with End_of_file -> error "No step function found." in
146  aux ()
147
148
149let prover () =
150  if Options.gui_requested () then ""
151  else "-jessie-atp " ^ (Options.get_prover ()) ^ " "
152
153let jessie filename =
154  print_verbose1 ("Running Frama-C/Jessie on file " ^ filename ^ "...\n") ;
155  let filename_quote = Filename.quote filename in
156  let base =
157    if has_extension filename then Filename.chop_extension filename
158    else filename in
159  let res_file = base ^ ".jessie_results" in
160  let timeout = string_of_int (Options.get_timeout ()) in
161  let cmd =
162    "TIMEOUT=" ^ timeout ^ " frama-c -jessie -jessie-behavior default " ^
163    "-jessie-why-opt=\"-fast-wp\" " ^ (prover ()) ^
164    filename_quote ^ " >> " ^ res_file in
165  let error_callback () = () in
166  let error_msg = "Failed to run Frama-C/Jessie on file " ^ filename ^ "." in
167  let success_callback () = res_file in
168  let success_msg = "Done. Results are in file " ^ res_file ^ "." in
169  exec cmd error_callback error_msg success_callback success_msg
170
171let read_jessie_results filename =
172  if not (Options.gui_requested ()) then
173    begin
174      print_verbose1
175        ("Reading Frama-C/Jessie results in file " ^ filename ^ "...\n" ) ;
176      let print_failed () = Printf.printf "Failed to prove the result.\n%!" in
177      try
178        let ic = open_in filename in
179        let rec aux () =
180          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
193              (print_verbose1 "Done.\n" ;
194               Printf.printf "Result is proven correct.\n%!")
195            else print_failed ()
196          else aux () in
197        aux ()
198      with Sys_error _ | End_of_file -> print_failed ()
199    end
200
201let verification filename =
202  Printf.printf "Verifying the result (this may take some time)...\n%!" ;
203  let res_file = jessie filename in
204  read_jessie_results res_file
205
206
207let cerco_test_info (inputs, booleans) step_fun step_cost cerco_file =
208  print_verbose1
209    ("Adding step function information to CerCo file " ^ cerco_file ^ "...\n") ;
210  try
211    let ic = open_in cerco_file in
212    let rec contents () =
213      try let s = input_line ic in s ^ "\n" ^ (contents ())
214      with End_of_file -> close_in ic ; "" in
215    let contents = step_fun ^ "\n" ^ step_cost ^ "\n" ^ contents () ^ "\n" in
216    let f contents s = contents ^ s ^ "\n" in
217    let contents = (List.fold_left f contents inputs) ^ "\n" in
218    let contents = List.fold_left f contents booleans in
219    let oc = open_out cerco_file in
220    output_string oc contents ;
221    close_out oc ;
222    print_verbose1 "Done.\n" ;
223    cerco_file
224  with Sys_error _ ->
225    error ("Could not add step function information to CerCo file " ^
226              cerco_file ^ ".")
227
228let cerco_test_file filename cerco_test_info =
229  print_verbose1 ("Adding a main to file " ^ filename ^ "...\n") ;
230  let filename_quote = Filename.quote filename in
231  let base =
232    if has_extension filename then Filename.chop_extension filename
233    else filename in
234  let res_base = base ^ "_test" in
235  let res_c = res_base ^ ".c" in
236  let cmd =
237    "acc -o " ^ res_base ^ " -lustre-test " ^ cerco_test_info ^
238      " -lustre-test-cases " ^ (string_of_int (Options.get_test_cases ())) ^
239      " -lustre-test-cycles " ^ (string_of_int (Options.get_test_cycles ())) ^
240      " -lustre-test-min-int " ^ (string_of_int (Options.get_test_min_int ())) ^
241      " -lustre-test-max-int " ^ (string_of_int (Options.get_test_max_int ())) ^
242      " " ^ filename_quote ^ " >> " ^ log_file in
243  let error_callback () = () in
244  let error_msg = "Failed to add a main to file " ^ filename ^ "." in
245  let success_callback () = res_c in
246  let success_msg = "Done. Result is in files " ^ res_c ^ "." in
247  exec cmd error_callback error_msg success_callback success_msg
248
249let test_exec filename =
250  print_verbose1 ("Simulating the generated code in file " ^ filename ^
251                  "...\n") ;
252  let filename_quote = Filename.quote filename in
253  let base =
254    if has_extension filename then Filename.chop_extension filename
255    else filename in
256  let res_file = base ^ ".results" in
257  let cmd = "acc -l Clight -i " ^ filename_quote ^ " > " ^ res_file in
258  let error_callback () = () in
259  let error_msg = "Failed to run acc on file " ^ filename ^ "." in
260  let success_callback () = res_file in
261  let success_msg = "Done. Results are in file " ^ res_file ^ "." in
262  exec cmd error_callback error_msg success_callback success_msg
263
264let read_test_results filename =
265  print_verbose1
266    ("Reading simulation results in file " ^ filename ^ "...\n" ) ;
267  try
268    let ic = open_in filename in
269    Misc.repeat 2 (fun () -> ignore (input_line ic)) () ;
270    let wcet = int_of_string (input_line ic) in
271    let min = int_of_string (input_line ic) in
272    let max = int_of_string (input_line ic) in
273    let average = int_of_string (input_line ic) in
274    let wcet_correct = max <= wcet in
275    print_verbose1 "Done.\n" ;
276    Printf.printf "Estimated WCET: %d\nMinimum: %d\nMaximum: %d\nAverage: %d\nEstimated WCET is %scorrect for these executions.\n%!"
277      wcet min max average (if wcet_correct then "" else "in")
278  with Sys_error _ | End_of_file | Failure "int_of_string" ->
279    error "Failed to test the result."
280
281let test filename inputs_booleans step_fun step_cost cerco_file =
282  Printf.printf "Testing the result (this may take some time)...\n%!" ;
283  let cerco_test_info =
284    cerco_test_info inputs_booleans step_fun step_cost cerco_file in
285  let cerco_test_file = cerco_test_file filename cerco_test_info in
286  let test_results = test_exec cerco_test_file in
287  read_test_results test_results
288
289
290let _ =
291  let args = OptionsParsing.results () in
292  if List.length args < 2 then error OptionsParsing.usage_msg
293  else
294    begin
295      let lustre_file = List.nth args 0 in
296      let node = List.nth args 1 in
297      print_verbose1
298        ("*** Processing node " ^ node ^ " of Lustre file " ^ lustre_file ^
299         ". ***\n") ;
300      let c_file = lustre_compilation lustre_file node in
301      let inputs_booleans = extract_inputs_booleans c_file in
302      let (c_annotated_file, cost_results_file, cerco_file) =
303        cost_plugin c_file in
304      let (step_fun, step_cost) = print_step_result cost_results_file in
305      if Options.verify_requested () then verification c_annotated_file ;
306      if Options.test_requested () then
307        test c_annotated_file inputs_booleans step_fun step_cost cerco_file ;
308    end
Note: See TracBrowser for help on using the repository browser.