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

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

Frama-C plug-in (sources+documentation)

File size: 11.4 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             "WCET of %s: %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 ->
146      error "No step function found or its cost could not be computed." in
147  aux ()
148
149
150let prover () =
151  if Options.gui_requested () then ""
152  else "-jessie-atp " ^ (Options.get_prover ()) ^ " "
153
154let jessie filename =
155  print_verbose1 ("Running Frama-C/Jessie on file " ^ filename ^ "...\n") ;
156  let filename_quote = Filename.quote filename in
157  let base =
158    if has_extension filename then Filename.chop_extension filename
159    else filename in
160  let res_file = base ^ ".jessie_results" in
161  let timeout = string_of_int (Options.get_timeout ()) in
162  let cmd =
163    "TIMEOUT=" ^ timeout ^ " frama-c -jessie -jessie-behavior default " ^
164    "-jessie-why-opt=\"-fast-wp\" " ^ (prover ()) ^
165    filename_quote ^ " >> " ^ res_file in
166  let error_callback () = () in
167  let error_msg = "Failed to run Frama-C/Jessie on file " ^ filename ^ "." in
168  let success_callback () = res_file in
169  let success_msg = "Done. Results are in file " ^ res_file ^ "." in
170  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)
175
176let read_jessie_results filename =
177  if not (Options.gui_requested ()) then
178    begin
179      print_verbose1
180        ("Reading Frama-C/Jessie results in file " ^ filename ^ "...\n" ) ;
181      let print_failed () = Printf.printf "Failed to prove the result.\n%!" in
182      try
183        let ic = open_in filename in
184        let rec aux () =
185          let s = input_line ic in
186          if string_starts_with "valid" s then
187            let regexp = Str.regexp (".*100%.*") in
188            if Str.string_match regexp s 0 then
189              (print_verbose1 "Done.\n" ;
190               Printf.printf "WCET is proven correct.\n%!")
191            else print_failed ()
192          else aux () in
193        aux ()
194      with Sys_error _ | End_of_file -> print_failed ()
195    end
196
197let verification filename =
198  Printf.printf "Verifying the result (this may take some time)...\n%!" ;
199  let res_file = jessie filename in
200  read_jessie_results res_file
201
202
203let cerco_test_info (inputs, booleans) step_fun step_cost cerco_file =
204  print_verbose1
205    ("Adding step function information to CerCo file " ^ cerco_file ^ "...\n") ;
206  try
207    let ic = open_in cerco_file in
208    let rec contents () =
209      try let s = input_line ic in s ^ "\n" ^ (contents ())
210      with End_of_file -> close_in ic ; "" in
211    let contents = step_fun ^ "\n" ^ step_cost ^ "\n" ^ contents () ^ "\n" in
212    let f contents s = contents ^ s ^ "\n" in
213    let contents = (List.fold_left f contents inputs) ^ "\n" in
214    let contents = List.fold_left f contents booleans in
215    let oc = open_out cerco_file in
216    output_string oc contents ;
217    close_out oc ;
218    print_verbose1 "Done.\n" ;
219    cerco_file
220  with Sys_error _ ->
221    error ("Could not add step function information to CerCo file " ^
222              cerco_file ^ ".")
223
224let cerco_test_file filename cerco_test_info =
225  print_verbose1 ("Adding a main to file " ^ filename ^ "...\n") ;
226  let filename_quote = Filename.quote filename in
227  let base =
228    if has_extension filename then Filename.chop_extension filename
229    else filename in
230  let res_base = base ^ "_test" in
231  let res_c = res_base ^ ".c" in
232  let cmd =
233    "acc -o " ^ res_base ^ " -lustre-test " ^ cerco_test_info ^
234      " -lustre-test-cases " ^ (string_of_int (Options.get_test_cases ())) ^
235      " -lustre-test-cycles " ^ (string_of_int (Options.get_test_cycles ())) ^
236      " -lustre-test-min-int " ^ (string_of_int (Options.get_test_min_int ())) ^
237      " -lustre-test-max-int " ^ (string_of_int (Options.get_test_max_int ())) ^
238      " " ^ filename_quote ^ " >> " ^ log_file in
239  let error_callback () = () in
240  let error_msg = "Failed to add a main to file " ^ filename ^ "." in
241  let success_callback () = res_c in
242  let success_msg = "Done. Result is in files " ^ res_c ^ "." in
243  exec cmd error_callback error_msg success_callback success_msg
244
245let test_exec filename =
246  print_verbose1 ("Simulating the generated code in file " ^ filename ^
247                  "...\n") ;
248  let filename_quote = Filename.quote filename in
249  let base =
250    if has_extension filename then Filename.chop_extension filename
251    else filename in
252  let res_file = base ^ ".results" in
253  let cmd = "acc -l Clight -i " ^ filename_quote ^ " > " ^ res_file in
254  let error_callback () = () in
255  let error_msg = "Failed to run acc on file " ^ filename ^ "." in
256  let success_callback () = res_file in
257  let success_msg = "Done. Results are in file " ^ res_file ^ "." in
258  exec cmd error_callback error_msg success_callback success_msg
259
260let read_test_results filename =
261  print_verbose1
262    ("Reading simulation results in file " ^ filename ^ "...\n" ) ;
263  try
264    let ic = open_in filename in
265    Misc.repeat 2 (fun () -> ignore (input_line ic)) () ;
266    let wcet = int_of_string (input_line ic) in
267    let min = int_of_string (input_line ic) in
268    let max = int_of_string (input_line ic) in
269    let average = int_of_string (input_line ic) in
270    let wcet_correct = max <= wcet in
271    print_verbose1 "Done.\n" ;
272    Printf.printf "Estimated WCET: %d\nMinimum: %d\nMaximum: %d\nAverage: %d\nEstimated WCET is %scorrect for these executions.\n%!"
273      wcet min max average (if wcet_correct then "" else "in")
274  with Sys_error _ | End_of_file | Failure "int_of_string" ->
275    error "Failed to test the result."
276
277let test filename inputs_booleans step_fun step_cost cerco_file =
278  Printf.printf "Testing the result (this may take some time)...\n%!" ;
279  let cerco_test_info =
280    cerco_test_info inputs_booleans step_fun step_cost cerco_file in
281  let cerco_test_file = cerco_test_file filename cerco_test_info in
282  let test_results = test_exec cerco_test_file in
283  read_test_results test_results
284
285
286let _ =
287  let args = OptionsParsing.results () in
288  if List.length args < 2 then error OptionsParsing.usage_msg
289  else
290    begin
291      let lustre_file = List.nth args 0 in
292      let node = List.nth args 1 in
293      print_verbose1
294        ("*** Processing node " ^ node ^ " of Lustre file " ^ lustre_file ^
295         ". ***\n") ;
296      let c_file = lustre_compilation lustre_file node in
297      let inputs_booleans = extract_inputs_booleans c_file in
298      let (c_annotated_file, cost_results_file, cerco_file) =
299        cost_plugin c_file in
300      let (step_fun, step_cost) = print_step_result cost_results_file in
301      if Options.verify_requested () then verification c_annotated_file ;
302      if Options.test_requested () then
303        test c_annotated_file inputs_booleans step_fun step_cost cerco_file ;
304    end
Note: See TracBrowser for help on using the repository browser.