wrapper/main.ml

   1
   2
   3 let error_prefix = "Main"
   4 let error = Error.global_error error_prefix
   5
   6
   7 let log_file = Filename.temp_file "log" ""
   8
   9
  10 let print_verbose i s =
  11   if Options.get_verbose_level () >= i then Printf.printf "%s%!" s
  12 let print_verbose1 = print_verbose 1
  13 let print_verbose2 = print_verbose 2
  14
  15
  16 let 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
  25 let has_extension filename =
  26   try ignore (Filename.chop_extension filename) ; true
  27   with Invalid_argument ("Filename.chop_extension") -> false
  28
  29 let 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
  54 let 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
  92 let 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
  97 let 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
 124 let 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
 150 let prover () =
 151   if Options.gui_requested () then ""
 152   else "-jessie-atp " ^ (Options.get_prover ()) ^ " "
 153
 154 let 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
 172 let string_starts_with prefix s =
 173   let l = String.length prefix in
 174   (l <= String.length s) && (String.sub s 0 l = prefix)
 175
 176 let 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
 197 let 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
 203 let 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
 224 let 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
 245 let 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
 260 let 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
 277 let 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
 286 let _ =
 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