From 7f308c4ae3cffe0ab02fe9f37f9826259ba2f8de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Thu, 11 May 2023 16:54:26 +0900
Subject: [PATCH] identifiers should not start with uppercase letters to cope
with recent versions of Velus
---
lustrec_tests/wcet/test.ml | 187 ++++++++++++++++++-------------------
src/velus_printer.ml | 18 ++--
2 files changed, 103 insertions(+), 102 deletions(-)
diff --git a/lustrec_tests/wcet/test.ml b/lustrec_tests/wcet/test.ml
index a2f381a1..ce1c1538 100644
--- a/lustrec_tests/wcet/test.ml
+++ b/lustrec_tests/wcet/test.ml
@@ -154,6 +154,21 @@ let has_velus_error log =
Some (matched_string log)
with Not_found -> None
+let pp_warning fmt =
+ fprintf fmt "@{<magenta>%s@}"
+
+let pp_error fmt =
+ fprintf fmt "@{<red>%s@}"
+
+let warning err_f =
+ let log = read_whole_file err_f in
+ printf "@ %a" pp_warning log
+
+(* let error err_f = *)
+(* let log = read_whole_file err_f in *)
+(* printf "@ %a" pp_error log; *)
+(* exit 1 *)
+
let lustrec_compile cfg o f =
let cmd =
Filename.quote_command
@@ -163,75 +178,92 @@ let lustrec_compile cfg o f =
in
let ic = open_process_in cmd in
match close_process_in ic with
- | WEXITED r -> r = 0
- | _ -> false
-
-let gcc_compile cfg o f =
+ | WEXITED 0 -> ()
+ | _ ->
+ let log = read_whole_file err_f in
+ match has_velus_error log with
+ | Some m ->
+ printf "@ %a" pp_warning m;
+ raise Exit
+ | None -> printf "@ %a" pp_error log
+
+let otawa_wcet cfg step =
let cmd =
Filename.quote_command
~stderr:err_f
- cfg.gcc
- (gcc_params cfg o f)
+ cfg.otawa
+ (otawa_params step)
in
let ic = open_process_in cmd in
+ let log = try input_line ic with _ -> "" in
match close_process_in ic with
- | WEXITED r -> r = 0
- | _ -> false
-
-let compcert_compile cfg f =
+ | WEXITED n when n <> 2 ->
+ Some (cycles log)
+ | _ ->
+ warning err_f;
+ None
+
+let gcc_compile cfg report_unit lustrec_o gcc_o f =
+ let f' = Filename.remove_extension f ^ ".c" in
+ let f_c = Filename.concat cfg.results_directory f' in
let cmd =
Filename.quote_command
~stderr:err_f
- cfg.compcert
- (compcert_params cfg f)
+ cfg.gcc
+ (gcc_params cfg gcc_o f_c)
in
let ic = open_process_in cmd in
match close_process_in ic with
- | WEXITED r -> r = 0
- | _ -> false
-
-let velus_compile cfg o f =
+ | WEXITED 0 ->
+ let step = get_step f ^ "_step" in
+ begin match otawa_wcet cfg step with
+ | Some wcet ->
+ report_unit.lustrec_gcc_wcet.(lustrec_o).(gcc_o) <- wcet
+ | None -> ()
+ end
+ | _ -> warning err_f
+
+let compcert_compile' cfg f_c step update =
let cmd =
Filename.quote_command
~stderr:err_f
- cfg.velus
- (velus_params o f)
+ cfg.compcert
+ (compcert_params cfg f_c)
in
let ic = open_process_in cmd in
match close_process_in ic with
| WEXITED 0 ->
- let f_s = Filename.remove_extension f ^ ".s" in
- compcert_compile cfg f_s
- | _ -> false
-
-let pp_warning fmt =
- fprintf fmt "@{<magenta>%s@}"
-
-let pp_error fmt =
- fprintf fmt "@{<red>%s@}"
-
-let warning err_f =
- let log = read_whole_file err_f in
- printf "@ %a" pp_warning log
-
-let error err_f =
- let log = read_whole_file err_f in
- printf "@ %a" pp_error log;
- exit 1
-
-let otawa_wcet update cfg step =
+ begin match otawa_wcet cfg step with
+ | Some wcet ->
+ update wcet
+ | None -> ()
+ end
+ | _ -> warning err_f
+
+let compcert_compile cfg report_unit lustrec_o f =
+ let f' = Filename.remove_extension f ^ ".c" in
+ let f_c = Filename.concat cfg.results_directory f' in
+ let step = get_step f ^ "_step" in
+ compcert_compile' cfg f_c step (fun wcet ->
+ report_unit.lustrec_compcert_wcet.(lustrec_o) <- wcet)
+
+let velus_compile cfg report_unit velus_o f =
+ let f' = Filename.remove_extension f ^ ".velus.lus" in
+ let f = Filename.concat cfg.results_directory f' in
let cmd =
Filename.quote_command
~stderr:err_f
- cfg.otawa
- (otawa_params step)
+ cfg.velus
+ (velus_params velus_o f)
in
let ic = open_process_in cmd in
- let log = try input_line ic with _ -> "" in
match close_process_in ic with
- | WEXITED n when n <> 2 ->
- update (cycles log)
- | _ -> error err_f
+ | WEXITED 0 ->
+ let f_s = Filename.remove_extension f ^ ".s" in
+ let step = "fun$step$" ^ get_step f in
+ compcert_compile' cfg f_s step (fun wcet ->
+ report_unit.velus_wcet.(velus_o) <- wcet)
+ | _ -> warning err_f
let compile cfg fs =
printf "@.%a@." pp_header "Compilation + WCET estimation tests";
@@ -243,66 +275,31 @@ let compile cfg fs =
let k = k + 1 in
let report_unit = empty_unit () in
- let b = try
+ let report = try
(* Compile with LustreC *)
for lustrec_o = 0 to 3 do
- if lustrec_compile cfg lustrec_o f then
- let f' = Filename.remove_extension f ^ ".c" in
- let f_c = Filename.concat cfg.results_directory f' in
- let step = get_step f ^ "_step" in
-
- (* Compile with GCC *)
- for gcc_o = 0 to 3 do
- if gcc_compile cfg gcc_o f_c then
- otawa_wcet (fun wcet ->
- report_unit.lustrec_gcc_wcet.(lustrec_o).(gcc_o) <- wcet)
- cfg step
- else
- error err_f
- done;
-
- (* Compile with CompCert *)
- if compcert_compile cfg f_c then
- (* let step = "fun$step$" ^ get_step f in *)
- otawa_wcet (fun wcet ->
- report_unit.lustrec_compcert_wcet.(lustrec_o) <- wcet)
- cfg step
- else
- error err_f
-
- else begin
- let log = read_whole_file err_f in
- match has_velus_error log with
- | Some m ->
- printf "@ %a" pp_warning m;
- raise Exit
- | None -> printf "@ %a" pp_error log
- end
+ lustrec_compile cfg lustrec_o f;
+
+ (* Compile with GCC *)
+ for gcc_o = 0 to 3 do
+ gcc_compile cfg report_unit lustrec_o gcc_o f;
+ done;
+
+ (* Compile with CompCert *)
+ compcert_compile cfg report_unit lustrec_o f;
+
done;
(* Compile with Velus *)
for velus_o = 0 to 1 do
- let f' = Filename.remove_extension f ^ ".velus.lus" in
- let f = Filename.concat cfg.results_directory f' in
- if velus_compile cfg velus_o f then
- let step = "fun$step$" ^ get_step f in
- otawa_wcet (fun wcet ->
- report_unit.velus_wcet.(velus_o) <- wcet)
- cfg step
- else
- warning err_f
+ velus_compile cfg report_unit velus_o f;
done;
- true
- with Exit -> false
- in
- printf "@]@.";
- let report =
- if b then
SMap.add Filename.(basename (remove_extension f)) report_unit report
- else report
+ with Exit -> report
in
- write_report cfg report;
- k, report)
+ printf "@]@.";
+ write_report cfg report;
+ k, report)
(0, empty_report) fs
(* let n = List.length fs in *)
diff --git a/src/velus_printer.ml b/src/velus_printer.ml
index 03d413e4..e60c1d58 100644
--- a/src/velus_printer.ml
+++ b/src/velus_printer.ml
@@ -21,11 +21,14 @@ let pp_var_type fmt id =
Types.pp_node_ty fmt id.var_type;
Options.kind2_print := b
+let pp_ident fmt x =
+ fprintf fmt "_%s" x
+
let rec print_carrier fmt cr =
let open Clocks in
match cr.carrier_desc with
| Carry_const id ->
- fprintf fmt "%s" id
+ pp_ident fmt id
| Carry_name
| Carry_var ->
assert false
@@ -56,7 +59,8 @@ let pp_node_var fmt id =
if Option.is_some id.var_dec_value then warning_ig "Parameter initializations";
fprintf
fmt
- "%s: %a%a"
+ "%a: %a%a"
+ pp_ident
id.var_id
pp_var_type
id
@@ -104,7 +108,7 @@ let rec pp_expr fmt expr =
| Expr_const c ->
pp_const fmt c
| Expr_ident id ->
- pp_print_string fmt id
+ pp_ident fmt id
| Expr_array _
| Expr_access _
| Expr_power _ ->
@@ -138,13 +142,13 @@ let rec pp_expr fmt expr =
warning "pre's are replaced by fby's";
pp fmt (Expr_fby (zero e, e))
| Expr_when (e, id, "true") ->
- fprintf fmt "(%a) when %s" pp_expr e id
+ fprintf fmt "(%a) when %a" pp_expr e pp_ident id
| Expr_when (e, id, "false") ->
- fprintf fmt "(%a) when not %s" pp_expr e id
+ fprintf fmt "(%a) when not %a" pp_expr e pp_ident id
| Expr_when _ ->
error_ns "Generalized clocks"
| Expr_merge (id, hl) ->
- fprintf fmt "merge %s %a" id pp_handlers hl
+ fprintf fmt "merge %a %a" pp_ident id pp_handlers hl
| Expr_appl (id, e, r) ->
pp_app fmt id e r
in
@@ -203,7 +207,7 @@ and pp_call fmt id e =
| _ ->
fprintf fmt "%s (%a)" id pp_expr e
-let pp_eq_lhs = pp_comma_list pp_print_string
+let pp_eq_lhs = pp_comma_list pp_ident
let pp_node_eq fmt eq =
fprintf fmt "%a = %a;" pp_eq_lhs eq.eq_lhs pp_expr eq.eq_rhs
--
GitLab