From 465c53c92be497dd4d8e1d53ad04b245d1c000f4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Wed, 10 May 2023 01:12:47 +0900
Subject: [PATCH] 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 | 2 +-
lustrec_tests/lustre_files/_6counter.lus | 2 +-
lustrec_tests/lustre_files/hysteresis_1.lus | 2 +-
lustrec_tests/lustre_files/two_counters.lus | 2 +-
lustrec_tests/wcet/dune | 1 +
lustrec_tests/wcet/eabi_mock.c | 35 +++++
lustrec_tests/wcet/test.ml | 139 ++++++++++++--------
7 files changed, 126 insertions(+), 57 deletions(-)
create mode 100644 lustrec_tests/wcet/eabi_mock.c
diff --git a/lustrec_tests/lustre_files/SYNAPSE_1.lus b/lustrec_tests/lustre_files/SYNAPSE_1.lus
index 7bc737ff..beb5669f 100644
--- a/lustrec_tests/lustre_files/SYNAPSE_1.lus
+++ b/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;
diff --git a/lustrec_tests/lustre_files/_6counter.lus b/lustrec_tests/lustre_files/_6counter.lus
index 3eff24be..bf2c3824 100644
--- a/lustrec_tests/lustre_files/_6counter.lus
+++ b/lustrec_tests/lustre_files/_6counter.lus
@@ -1,7 +1,7 @@
-- 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
diff --git a/lustrec_tests/lustre_files/hysteresis_1.lus b/lustrec_tests/lustre_files/hysteresis_1.lus
index c741b3ea..9bd23a9b 100644
--- a/lustrec_tests/lustre_files/hysteresis_1.lus
+++ b/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
diff --git a/lustrec_tests/lustre_files/two_counters.lus b/lustrec_tests/lustre_files/two_counters.lus
index 1886c4a5..afe166ed 100644
--- a/lustrec_tests/lustre_files/two_counters.lus
+++ b/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
diff --git a/lustrec_tests/wcet/dune b/lustrec_tests/wcet/dune
index 97943571..76c6b87c 100644
--- a/lustrec_tests/wcet/dune
+++ b/lustrec_tests/wcet/dune
@@ -4,6 +4,7 @@
(deps
(:lus
(glob_files *.lus))
+ eabi_mock.c
; (:cfg config.json)
)
(action
diff --git a/lustrec_tests/wcet/eabi_mock.c b/lustrec_tests/wcet/eabi_mock.c
new file mode 100644
index 00000000..4257f37e
--- /dev/null
+++ b/lustrec_tests/wcet/eabi_mock.c
@@ -0,0 +1,35 @@
+/* 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 () {}
diff --git a/lustrec_tests/wcet/test.ml b/lustrec_tests/wcet/test.ml
index 0c63de1c..7d7a12f0 100644
--- a/lustrec_tests/wcet/test.ml
+++ b/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 *)
--
GitLab