diff --git a/lib/licEvalConst.ml b/lib/licEvalConst.ml
index b6dd1cadb1a11ea803e36e5556108a67aae38914..3686668478c9d97a6eb0805986a19e729d3dbbba 100644
--- a/lib/licEvalConst.ml
+++ b/lib/licEvalConst.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 29/08/2019 (at 16:16) by Erwan Jahier> *)
+(* Time-stamp: <modified the 01/07/2022 (at 11:04) by Erwan Jahier> *)
open AstPredef
open Lic
@@ -11,7 +11,7 @@ type const_evaluator = Lic.const evaluator
exception EvalConst_error of string
let eval_real_error () =
- raise (EvalConst_error ("expression involving reals are not evaluated\n***"^
+ raise (EvalConst_error ("only expression involving ints are statically evaluated\n***"^
" to avoid semantics issues, sorry."))
(* exported *)
@@ -50,7 +50,8 @@ let (iii_evaluator:(int -> int -> int) -> const_evaluator) =
let (aab_evaluator:('a -> 'a -> bool) -> const_evaluator) =
fun op -> fun ll -> match List.flatten ll with
- | [v0; v1] -> [Bool_const_eff (op v0 v1)]
+ | [Int_const_eff v0; Int_const_eff v1] -> [Bool_const_eff (op (int_of_string v0) (int_of_string v1))]
+ | [_; _] -> eval_real_error ()
| _ -> assert false (* should not occur because eval_type is called before *)
let (fff_evaluator:(float -> float -> float) -> const_evaluator) =
diff --git a/lib/soc2c.ml b/lib/soc2c.ml
index 4b9b6c411b547f67265a209f1a220e2a683dba53..12cc427fa6ab73fa42d39705d1837fc17e154e31 100644
--- a/lib/soc2c.ml
+++ b/lib/soc2c.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 28/06/2022 (at 16:51) by Erwan Jahier> *)
+(* Time-stamp: <modified the 08/07/2022 (at 11:04) by Erwan Jahier> *)
(* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
@@ -243,21 +243,21 @@ let one_file() = Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_one_file
- updates/returns the list of created C files *)
let (soc2c : int -> out_channel -> out_channel -> Soc.tbl -> Soc.key ->
string list -> Soc.t -> string list) =
- fun pass hfile cfile stbl msoc_key cfiles_acc soc ->
+ fun pass hfile_main_oc cfile_main_oc stbl msoc_key cfiles_acc soc ->
if inlined_soc soc.key then cfiles_acc (* don't generate code if inlined *) else
let ctx_name = get_ctx_name soc.key in
let ctx_name_type = ctx_name^"_type" in
if pass=1 then (
(* Only for ctx of memoryless nodes + main node *)
if SocUtils.ctx_is_global soc then
- Printf.kprintf (fun t -> output_string cfile t) "static %s %s;\n" ctx_name_type ctx_name;
+ Printf.kprintf (fun t -> output_string cfile_main_oc t) "static %s %s;\n" ctx_name_type ctx_name;
cfiles_acc
) else (
let dir = Lv6MainArgs.global_opt.Lv6MainArgs.dir in
let base0 = (string_of_soc_key soc.key) in
let base = Filename.concat dir base0 in
let cfile,hfile,cfiles_acc =
- if one_file() || msoc_key = soc.key then cfile, hfile, cfiles_acc else
+ if one_file() || msoc_key = soc.key then cfile_main_oc, hfile_main_oc, cfiles_acc else
let _cfile0 = (base0^".c") in
let hfile0 = (base0^".h") in
let cfile = (base^".c") in
@@ -268,8 +268,6 @@ let (soc2c : int -> out_channel -> out_channel -> Soc.tbl -> Soc.key ->
Lv6util.entete cfile_oc "/*" "*/" ;
Lv6util.entete hfile_oc "/*" "*/" ;
Printf.fprintf cfile_oc "#include \"%s\"\n" hfile0;
- Printf.fprintf hfile_oc "#include \"lustre_types.h\"\n";
- Printf.fprintf hfile_oc "#include \"lustre_consts.h\"\n";
Printf.fprintf hfile_oc "#ifndef _%s_H_FILE \n" base0;
Printf.fprintf hfile_oc "#define _%s_H_FILE \n" base0;
flush cfile_oc;
@@ -278,6 +276,7 @@ let (soc2c : int -> out_channel -> out_channel -> Soc.tbl -> Soc.key ->
(if List.mem cfile cfiles_acc then cfiles_acc else cfile::cfiles_acc)
in
let hfmt fmt = Printf.kprintf (fun t -> output_string hfile t) fmt in
+ let main_hfmt fmt = Printf.kprintf (fun t -> output_string hfile_main_oc t) fmt in
let cfmt fmt = Printf.kprintf (fun t -> output_string cfile t) fmt in
let hput str = output_string hfile str in
let cput str = output_string cfile str in
@@ -287,12 +286,14 @@ let (soc2c : int -> out_channel -> out_channel -> Soc.tbl -> Soc.key ->
let (used_soc:Soc.key list) = KeySet.elements (get_used_soc soc) in
List.iter
(fun sk -> if inlined_soc sk then () else
- hfmt "#include \"%s.h\"\n" (string_of_soc_key sk)
+ hfmt "#include \"%s.h\"\n" (string_of_soc_key sk)
)
used_soc;
- if msoc_key <> soc.key then hfmt "%s\n" (Soc2cDep.typedef_of_soc soc);
+ if msoc_key <> soc.key then hfmt "#include \"%s.h\"\n" (string_of_soc_key msoc_key)
);
-
+
+ main_hfmt "/* Soc2cDep.typedef_of_soc XXX */ \n%s\n" "" ;
+ (* (Soc2cDep.typedef_of_soc soc); *)
if SocUtils.is_memory_less soc then () else (
cfmt "// Memory initialisation for %s\n" ctx_name;
hfmt "void %s_reset(%s_type* ctx);\n" ctx_name ctx_name;
@@ -430,13 +431,14 @@ let (typedef_all : LicPrg.t -> Soc.tbl -> Soc.t -> string) =
)
(acc,visited) soc.instances
in
- let acc = acc ^ (
- if one_file() || soc.key = main_soc.key then
+ let acc = acc ^ "/* Soc2cDep.typedef_of_soc YYY */\n" ^(
+ (* if one_file() || soc.key = main_soc.key then *)
Soc2cDep.typedef_of_soc soc
- else
- (Printf.sprintf "#include \"%s.h\"\n" (string_of_soc_key soc.key))
+ (* else *)
+ (* (Printf.sprintf "#include \"%s.h\"\n" (string_of_soc_key soc.key)) *)
)
in
+
acc,visited
in
let soc_ctx_typedef_with_mem =
@@ -444,7 +446,7 @@ let (typedef_all : LicPrg.t -> Soc.tbl -> Soc.t -> string) =
fst (soc_with_mem ("",visited) main_soc)
in
(* Then we still have to print memoryless soc that can not appear
- as a soc instance *)
+ as a soc instance
let soc_ctx_typedef_without_mem =
let socs = Soc.SocMap.bindings soc_tbl in
let socs = snd (List.split socs) in
@@ -453,8 +455,10 @@ let (typedef_all : LicPrg.t -> Soc.tbl -> Soc.t -> string) =
in
List.fold_left memless_soc_to_string "" socs
in
-"// Memoryless soc ctx typedef \n"^soc_ctx_typedef_without_mem
- ^"// Memoryfull soc ctx typedef \n"^soc_ctx_typedef_with_mem
+ "// Memoryless soc ctx typedef \n"^soc_ctx_typedef_without_mem
+ ^
+*)
+ "// Memoryfull soc ctx typedef \n"^soc_ctx_typedef_with_mem
@@ -644,11 +648,14 @@ int main(){" ^ (gen_main_loop_body inputs outputs soc ctx));
close_out oc
-let (gen_loop_file : string -> LicPrg.t -> Soc.t -> string -> out_channel -> Soc.tbl
- -> unit) =
- fun fn licprg soc base oc stbl ->
+(* generate a node_loop.c and a node_loop_io.{ch} *)
+let (gen_loop_file : string -> LicPrg.t -> Soc.t -> string ->
+ out_channel -> out_channel -> out_channel -> Soc.tbl -> unit) =
+ fun fn licprg soc base main_oc readinput_oc_c readinput_oc_h stbl ->
let base0 = Filename.basename base in
- let putc s = output_string oc s in
+ let putc s = output_string main_oc s in
+ let putc_ri s = output_string readinput_oc_c s in
+ let puth_ri s = output_string readinput_oc_h s in
let ctx = get_ctx_name soc.key in
let step = Soc2cDep.step_name soc.key "step" in
let inputs,outputs = soc.profile in
@@ -657,14 +664,12 @@ let (gen_loop_file : string -> LicPrg.t -> Soc.t -> string -> out_channel -> Soc
let inputs_exp = SocVar.expand_profile true true inputs in
let outputs_exp= SocVar.expand_profile true true outputs in
- Lv6util.entete oc "/*" "*/";
- putc ("
-#include <stdlib.h>
-#include <stdio.h>
-#include <unistd.h>
-#include \""^base0 ^".h\"
-/* Print a promt ? ************************/
-static int ISATTY;
+ Lv6util.entete main_oc "/*" "*/";
+ Lv6util.entete readinput_oc_c "/*" "*/";
+ Lv6util.entete readinput_oc_h "/*" "*/";
+ putc_ri ("
+#include \""^base0 ^"_loop_io.h\"\
+
/* MACROS DEFINITIONS ****************/
#ifndef TT
#define TT \"1\"
@@ -675,9 +680,6 @@ static int ISATTY;
#ifndef BB
#define BB \"bottom\"
#endif
-#ifdef CKCHECK
-/* set this macro for testing output clocks */
-#endif
void _read_pragma("^ (
if SocUtils.is_memory_less soc then "" else
@@ -797,13 +799,43 @@ void _put_string(char* n, char* _V){
}
"^(Soc2cExtern.gen_getters fn licprg soc)^"
/* Output procedures **********************/
-#ifdef CKCHECK
-void %s_BOT_n(void* cdata){
- _put_bottom(\"n\");
-}
-#endif
-"^ (gen_memoryless_ctx stbl) ^
-"
+"^ (gen_memoryless_ctx stbl)
+ );
+ puth_ri ("
+#include <stdlib.h>
+#include <stdio.h>
+#include <unistd.h>
+#include <string.h>
+#include \""^base0 ^".h\"
+
+void _read_pragma("^(
+ if SocUtils.is_memory_less soc then "" else
+ ctx^"_type*,"
+ ) ^"char []);
+_boolean _get_bool("^(
+ if SocUtils.is_memory_less soc then "" else
+ ctx^"_type*,"
+ ) ^"char*);
+_integer _get_int("^(
+ if SocUtils.is_memory_less soc then "" else
+ ctx^"_type*,"
+ ) ^"char*);
+_real _get_real("^(
+ if SocUtils.is_memory_less soc then "" else
+ ctx^"_type*,"
+ ) ^"char*);
+void _put_bottom(char*);
+void _put_bool(char*, _boolean);
+void _put_int(char*, _integer);
+void _put_real(char*, _real);
+void _put_string(char*, char*);
+
+/* Print a promt ? ************************/
+static int ISATTY;
+ ");
+ putc ("
+#include \""^base0 ^"_loop_io.h\"\
+
/* Main procedure *************************/
int main(){
int _s = 0;" ^ (
@@ -820,8 +852,8 @@ int main(){
printf(\""^inputs_decl^"\\n\");
printf(\""^outputs_decl^"\\n\");
- /* Main loop */
ISATTY = isatty(0);
+ /* Main loop */
while(1){
if (ISATTY) printf(\"#step %d \\n\", _s+1);
else if(_s) printf(\"\\n\");
@@ -894,12 +926,13 @@ let (gen_loop_file4ogensim : Soc.t -> string -> out_channel -> Soc.tbl -> unit)
let outputs_io = SocVar.expand_profile true false outputs in
let inputs_exp = SocVar.expand_profile true true inputs in
let outputs_exp= SocVar.expand_profile true true outputs in
+ let base0 = Filename.basename base in
let define_define i (var_name,_) =
putc (Printf.sprintf "#define _%s\t 0xe%07X\n" var_name ((i+1)*8));
in
Lv6util.entete oc "/*" "*/";
- putc ("#include \""^base ^".h\"
+ putc ("#include \""^base0 ^".h\"
#define tickBegin 0xe0000000
");
@@ -971,11 +1004,13 @@ let (f : Lv6MainArgs.t -> Soc.key -> Soc.tbl -> LicPrg.t -> unit) =
let ext_hfile0 = Printf.sprintf "%s_ext.h" base0 in
let ext_hfile = Printf.sprintf "%s_ext.h" base in
let loopfile = base^"_loop.c" in
+ let loop_readinput_cfile = base^"_loop_io.c" in
+ let loop_readinput_hfile = base^"_loop_io.h" in
let occ = open_out cfile in
let och = open_out hfile in
- let ocl =
- if Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_dro then stdout else
- open_out loopfile
+ let ocl, ocl_readinput_c, ocl_readinput_h =
+ if Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_dro then stdout, stdout, stdout else
+ open_out loopfile, open_out loop_readinput_cfile, open_out loop_readinput_hfile
in
let types_h_oc = open_out (Filename.concat dir "lustre_types.h") in
let consts_h_oc = open_out (Filename.concat dir "lustre_consts.h") in
@@ -1024,10 +1059,7 @@ typedef float _float;
#define _"^base0^"_TYPES\n");
output_string och (user_typedef licprg); flush och;
- output_string och ((typedef_all licprg stbl main_soc )
- ^ "#endif // end of _"^base0^"_TYPES
-");
-
+
if needs_hfile || args.Lv6MainArgs.ext_types then (
puth (Printf.sprintf "\n#ifndef _%s_H_FILE\n" base0);
puth (Printf.sprintf "#include \"%s\"\n" ext_hfile0);
@@ -1044,7 +1076,7 @@ typedef float _float;
gen_main_wcet_file main_soc base stbl
)
else
- gen_loop_file loopfile licprg main_soc base ocl stbl;
+ gen_loop_file loopfile licprg main_soc base ocl ocl_readinput_c ocl_readinput_h stbl;
putc (Printf.sprintf "#include \"%s\"\n" hfile0);
(* putc (Soc2cExtern.cpy_declaration licprg); *)
@@ -1060,6 +1092,8 @@ typedef float _float;
);
) else cfiles_acc
in
+ output_string och (typedef_all licprg stbl main_soc);
+
putc "//// Defining step functions\n";
let cfiles_acc = List.fold_left (soc2c 2 och occ stbl msoc) cfiles_acc socs in
@@ -1158,9 +1192,15 @@ struct dro_desc_t DRO_DESC_NAME = {
List.iter (fun t -> output_string och (Soc2cGenAssign.f t))
assign_ext_types_list
);
+ output_string och ("#endif // end of _"^base0^"_TYPES\n");
+
flush occ; close_out occ;
flush och; close_out och;
- if not Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_dro then (flush ocl; close_out ocl);
+ if not Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_dro then (
+ flush ocl; close_out ocl;
+ flush ocl_readinput_c; close_out ocl_readinput_c;
+ flush ocl_readinput_h; close_out ocl_readinput_h
+ );
flush consts_h_oc; close_out consts_h_oc;
flush consts_c_oc; close_out consts_c_oc;
if not Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_dro then
@@ -1177,11 +1217,11 @@ struct dro_desc_t DRO_DESC_NAME = {
in
let cflags = try Sys.getenv "CFLAGS" with Not_found -> "" in
let ocsh = open_out (Filename.concat dir (node ^".sh")) in
- let main_file, ogensim_main_file, gcc =
+ let main_files, ogensim_main_file, gcc =
if Lv6MainArgs.global_opt.Lv6MainArgs.gen_wcet then
base^"_main.c",base^"_loop.c","gcc --specs=linux.specs -g"
else
- loopfile, "I am a dead string...", "$C_COMPILER"
+ (loopfile^ " " ^ loop_readinput_cfile), "I am a dead string...", "$C_COMPILER"
in
let ogensim_exe = node^"4ogensim.exec" in
let cfiles_acc = if needs_cfile then ext_cfile::cfiles_acc else cfiles_acc in
@@ -1192,8 +1232,7 @@ struct dro_desc_t DRO_DESC_NAME = {
"dead string"
) else
Printf.sprintf "if [ -z ${C_COMPILER} ]; then C_COMPILER=gcc; fi
-%s -o %s \\\n\t%s %s %s"
- gcc execfile cfiles cflags main_file,
+%s -o %s \\\n\t%s %s %s" gcc execfile cfiles cflags main_files,
Printf.sprintf "%s -o %s \\\n\t%s %s %s"
gcc ogensim_exe cfiles cflags ogensim_main_file
in
@@ -1292,7 +1331,8 @@ fi
else gcc
in
output_string ocsh (gcc^"\n\n");
- flush ocsh;
+ flush ocsh;
+
close_out types_h_oc;
close_out ocsh;
let call_script = Printf.sprintf "sh %s.sh" (Filename.concat dir node) in
@@ -1317,6 +1357,8 @@ fi
close_out occ;
close_out och;
if not Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_dro then close_out ocl;
+ if not Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_dro then close_out ocl_readinput_c;
+ if not Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_dro then close_out ocl_readinput_h;
if Sys.file_exists hfile then Sys.remove hfile;
if Sys.file_exists cfile then Sys.remove cfile;
if Sys.file_exists ext_cfile then Sys.remove ext_cfile;
diff --git a/lib/soc2cExtern.ml b/lib/soc2cExtern.ml
index 49d52b6ad5669f5fb1159fb862602609d000fb27..5464b39372a04818811300d8b2822f3710a581e1 100644
--- a/lib/soc2cExtern.ml
+++ b/lib/soc2cExtern.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 13/03/2020 (at 11:44) by Erwan Jahier> *)
+(* Time-stamp: <modified the 07/07/2022 (at 10:28) by Erwan Jahier> *)
open Soc2cIdent
@@ -158,10 +158,11 @@ let (gen_files : Soc.t -> Soc.tbl -> LicPrg.t -> string -> string -> string ->
close_out ext_och;
Printf.eprintf "W: %s has been generated.\n%!" ext_hfile;
);
+ let hfile0 = Filename.basename hfile in
if not (Sys.file_exists ext_cfile) && needs_cfile then (
let ext_occ = open_out ext_cfile in
if needs_hfile then
- output_string ext_occ (Printf.sprintf "#include \"%s\"\n" hfile);
+ output_string ext_occ (Printf.sprintf "#include \"%s\"\n" hfile0);
(* output_string ext_occ (cpy_def licprg); *)
Printf.eprintf "W: please check the def of FAKE_CONST_DEF_2FIX in %s.\n%!"
ext_cfile;
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index a42a1a6d7df258d25a6f813541776d51f5025858..1bd1a7c2aff01baeb13fcd6ab937773c0fc674fe 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,5 +1,5 @@
==> lus2lic0.sum <==
-Test run by jahier on Mon Jun 20 17:30:38
+Test run by jahier on Fri Jul 8 11:05:01
Native configuration is x86_64-pc-linux-gnu
=== lus2lic0 tests ===
@@ -66,7 +66,7 @@ XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/lecte
XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/s.lus
==> lus2lic1.sum <==
-Test run by jahier on Mon Jun 20 17:30:39
+Test run by jahier on Fri Jul 8 11:05:02
Native configuration is x86_64-pc-linux-gnu
=== lus2lic1 tests ===
@@ -626,7 +626,7 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {}
PASS: /home/jahier/lus2lic/test/../utils/compare_lv6_and_lv6_en multipar.lus {}
==> lus2lic2.sum <==
-Test run by jahier on Mon Jun 20 17:36:32
+Test run by jahier on Fri Jul 8 11:10:45
Native configuration is x86_64-pc-linux-gnu
=== lus2lic2 tests ===
@@ -1171,7 +1171,7 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_lv6_and_lv6_en zzz2.lus {}
PASS: /home/jahier/lus2lic/test/../utils/compare_gcc_and_clang zzz2.lus {}
==> lus2lic3.sum <==
-Test run by jahier on Mon Jun 20 17:43:24
+Test run by jahier on Fri Jul 8 11:17:46
Native configuration is x86_64-pc-linux-gnu
=== lus2lic3 tests ===
@@ -1686,7 +1686,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
-Test run by jahier on Mon Jun 20 17:44:34
+Test run by jahier on Fri Jul 8 11:19:06
Native configuration is x86_64-pc-linux-gnu
=== lus2lic4 tests ===
@@ -2211,11 +2211,11 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_gcc_and_clang multipar.lus {}
===============================
# Total number of failures: 17
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 353 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 412 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 70 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 62 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 343 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 421 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 80 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 67 seconds
* Ref time:
-322.91user 81.61system 14:58.21elapsed 45%CPU (0avgtext+0avgdata 77544maxresident)k
-50792inputs+458048outputs (203major+19437060minor)pagefaults 0swaps
+326.87user 90.70system 15:12.28elapsed 45%CPU (0avgtext+0avgdata 77356maxresident)k
+36856inputs+488872outputs (79major+22973722minor)pagefaults 0swaps
* Quick time (-j 4):