start to ensure that top nodes and filenames coincide to ease analysis

design a "mock" libgcc because OTAWA can get lost in the standard one

lustrec_tests/lustre_files/SYNAPSE_1.lus

@@ -42,7 +42,7 @@ let
 
 tel
 
-node top(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
+node SYNAPSE_1(e_s1, e_s2, e_s3 : bool; init_invalid_s : int)
 returns( OK : bool );
 --@ contract guarantee OK by 2-induction;
     var invalid_s, valid_s, dirty_s : int; mem_init_s : int;

lustrec_tests/lustre_files/_6counter.lus

 -- a simple 0 to 5 boolean counter (A is LSB, C is MSB)
 -- property is that it should never reach 6 or 7
 
-node top (x:bool) returns (OK:bool);
+node _6counter (x:bool) returns (OK:bool);
 --@ contract guarantee OK;
 var a,b,c:bool;
 let

lustrec_tests/lustre_files/hysteresis_1.lus

@@ -26,7 +26,7 @@ let
                     else diff <= -10;
 tel
 
-node top( beacon, second : bool ) returns ( OK : bool );
+node hysteresis_1( beacon, second : bool ) returns ( OK : bool );
 --@ contract guarantee OK by 1-induction;
     var late, early : bool;
 let

lustrec_tests/lustre_files/two_counters.lus

@@ -17,7 +17,7 @@ let
 tel
 
 
-node top (x:bool) returns (OK:bool);
+node two_counters (x:bool) returns (OK:bool);
 --@ contract guarantee OK by 5-induction;
 var b,d:bool;
 let

lustrec_tests/wcet/dune

@@ -4,6 +4,7 @@
  (deps
   (:lus
    (glob_files *.lus))
+   eabi_mock.c
   ; (:cfg config.json)
  )
  (action

lustrec_tests/wcet/eabi_mock.c

+/* 5.1.2   The floating-point helper functions */
+/* https://github.com/ARM-software/abi-aa/blob/844a79fd4c77252a11342709e3b27b2c9f590cf1/rtabi32/rtabi32.rst#id33 */
+
+// Standard double precision floating-point arithmetic helper functions
+double __aeabi_dadd(double, double) {}
+double __aeabi_ddiv(double, double) {}
+double __aeabi_dmul(double, double) {}
+double __aeabi_drsub(double, double) {}
+double __aeabi_dsub(double, double) {}
+
+// Standard double precision floating-point comparison helper functions
+void __aeabi_cdcmpeq(double, double) {}
+void __aeabi_cdcmple(double, double) {}
+void __aeabi_cdrcmple(double, double) {}
+int __aeabi_dcmpeq(double, double) {}
+int __aeabi_dcmplt(double, double) {}
+int __aeabi_dcmple(double, double) {}
+int __aeabi_dcmpge(double, double) {}
+int __aeabi_dcmpgt(double, double) {}
+int __aeabi_dcmpun(double, double) {}
+
+/* 5.3.1   Integer (32/32 → 32) division functions */
+/* https://github.com/ARM-software/abi-aa/blob/844a79fd4c77252a11342709e3b27b2c9f590cf1/rtabi32/rtabi32.rst#531integer-3232--32-division-functions */
+
+int __aeabi_idiv(int, int) {}
+unsigned __aeabi_uidiv(unsigned, unsigned) {}
+
+typedef struct { int quot; int rem; } idiv_return;
+typedef struct { unsigned quot; unsigned rem; } uidiv_return;
+
+idiv_return __aeabi_idivmod(int, int) {}
+uidiv_return __aeabi_uidivmod(unsigned, unsigned) {}
+
+
+int main () {}

lustrec_tests/wcet/test.ml

@@ -26,9 +26,17 @@ module SMap = Map.Make(String)
 
 let empty_report = SMap.empty
 
-let pp fmt =
+let pp_report fmt =
   fprintf fmt "@[<v>@[<h>#file -1x0 -1x1 -1x2 -1x3 1x0 1x1 1x2 1x3 2x0 2x1 2x2 2x3 3x0 3x1 3x2 3x3 Vnf V@]@ %a@]@."
-    (fun fmt -> SMap.iter (fun x -> fprintf fmt "%s %a" x pp_report_unit))
+    (fun fmt -> SMap.iter (fun x -> fprintf fmt "@[<h>%s %a@]@ " x pp_report_unit))
+
+let report_file cfg = Filename.concat cfg.results_directory "report"
+
+let write_report cfg report =
+  let oc = open_out (report_file cfg) in
+  let fmt = formatter_of_out_channel oc in
+  pp_report fmt report;
+  close_out oc
 
 let config_format_tags =
   set_tags true;
@@ -74,14 +82,15 @@ let lustrec_params cfg o f =
 let gcc_params cfg o f =
   [
     "-O" ^ string_of_int o;
-    "-mfloat-abi=hard";
-    "-march=armv7-a";
-    "-mfpu=vfpv3-d16";
+    (* "-mfloat-abi=hard"; *)
+    (* "-march=armv7-a"; *)
+    (* "-mfpu=vfpv3-d16"; *)
     "-nostdlib";
     "-I" ^ cfg.include_directory;
     cfg.include_directory ^ "/arrow_noalloc.c";
+    "eabi_mock.c";
     f;
-    "-lgcc"
+    (* "-lgcc" *)
   ]
 
 let gcc = "arm-none-eabi-gcc"
@@ -108,6 +117,16 @@ let cycles log =
   search_forward (regexp reg) log 0 |> ignore;
   matched_group 1 log |> int_of_string
 
+let has_velus_error log =
+  let open Re.Str in
+  let reg =
+    "Velus output Error:.+"
+  in
+  try
+    search_forward (regexp reg) log 0 |> ignore;
+    Some (matched_string log)
+  with Not_found -> None
+
 let compile cfg lustrec fs =
   printf "@.%a@." pp_header "Compilation tests";
   let n = List.length fs in
@@ -120,61 +139,75 @@ let compile cfg lustrec fs =
   (*     0 *)
   (*     fs; *)
   List.fold_left (fun (k, report) f ->
-      printf "%s@." f;
+      let p = float_of_int k *. 100. /. n_f in
+      printf "%3.0f%% @[<v 2>%s" p f;
       let k = k + 1 in
       let report_unit = empty_unit in
       (* Compile with LustreC *)
-      for lustrec_o = 0 to 3 do
-        printf "  LustreC-%d@.    " lustrec_o;
-        let cmd =
-          Filename.quote_command
-            ~stderr:err_f
-            lustrec
-            (lustrec_params cfg lustrec_o f)
-        in
-        let ic = open_process_in cmd in
-        let b = match close_process_in ic with WEXITED r -> r = 0 | _ -> false in
-        if b then
-          let f' = Filename.remove_extension f ^ ".c" in
-          let f_c = Filename.concat cfg.results_directory f' in
-          (* Compile with GCC *)
-          for gcc_o = 0 to 3 do
-            printf "GCC-%d  " gcc_o;
-            let cmd =
-              Filename.quote_command
-                ~stderr:err_f
-                gcc
-                (gcc_params cfg gcc_o f_c)
-            in
-            let ic = open_process_in cmd in
-            let b = match close_process_in ic with WEXITED r -> r = 0 | _ -> false in
-            if b then
-              let step = get_step f ^ "_step" in
+      (* begin try *)
+      (try
+        for lustrec_o = 0 to 3 do
+          (* printf "  LustreC-%d@.    " lustrec_o; *)
+          let cmd =
+            Filename.quote_command
+              ~stderr:err_f
+              lustrec
+              (lustrec_params cfg lustrec_o f)
+          in
+          let ic = open_process_in cmd in
+          let b = match close_process_in ic with WEXITED r -> r = 0 | _ -> false in
+          if b then
+            let f' = Filename.remove_extension f ^ ".c" in
+            let f_c = Filename.concat cfg.results_directory f' in
+            (* Compile with GCC *)
+            for gcc_o = 0 to 3 do
+              (* printf "GCC-%d  " gcc_o; *)
               let cmd =
                 Filename.quote_command
                   ~stderr:err_f
-                  ~stdout:out_f
-                  otawa
-                  (otawa_params step)
+                  gcc
+                  (gcc_params cfg gcc_o f_c)
               in
               let ic = open_process_in cmd in
-              (match close_process_in ic with
-              | WEXITED _ ->
-                let log = read_whole_file out_f in
-                report_unit.lustrec_gcc.(lustrec_o).(gcc_o) <- cycles log
-              | WSIGNALED n ->
-                print_endline ("OTAWA sig" ^ string_of_int n)
-              | WSTOPPED n ->
-                print_endline ("OTAWA stp" ^ string_of_int n)
-              )
-            else print_endline "GCC ko"
-          done;
-          printf "@."
-        else print_endline "LustreC ko"
-      done;
-      let p = float_of_int k *. 100. /. n_f in
-      printf "@.%3.0f%%@." p;
-      k, SMap.add Filename.(basename (remove_extension f)) report_unit report)
+              let b = match close_process_in ic with WEXITED r -> r = 0 | _ -> false in
+              if b then
+                let step = get_step f ^ "_step" in
+                let cmd =
+                  Filename.quote_command
+                    ~stderr:err_f
+                    ~stdout:out_f
+                    otawa
+                    (otawa_params step)
+                in
+                let ic = open_process_in cmd in
+                (match close_process_in ic with
+                 | WEXITED n when n <> 2 ->
+                   let log = read_whole_file out_f in
+                   report_unit.lustrec_gcc.(lustrec_o).(gcc_o) <- cycles log
+                 | _ ->
+                   print_endline "OTAWA ko"
+                )
+              else begin
+                let log = read_whole_file err_f in
+                print_endline log;
+                exit 1
+              end
+            done;
+            (* printf "@." *)
+          else begin
+            let log = read_whole_file err_f in
+            match has_velus_error log with
+            | Some m ->
+              printf "@ %s" m;
+              raise Exit
+            | None -> printf "@ %s" log
+          end
+        done
+       with Exit -> ());
+      printf "@]@.";
+      let report = SMap.add Filename.(basename (remove_extension f)) report_unit report in
+     write_report cfg report;
+      k, report)
     (0, empty_report) fs
 
       (* let n = List.length fs in *)