diff --git a/include/arrow.cpp b/include/arrow.cpp new file mode 100644 index 0000000000000000000000000000000000000000..75fe2f4eed227ad234eed966c8049aa83ab032ca --- /dev/null +++ b/include/arrow.cpp @@ -0,0 +1,9 @@ +#include <stdlib.h> +#include "arrow.hpp" + +struct _arrow_mem *_arrow_alloc() { + struct _arrow_mem *_alloc; + _alloc = (struct _arrow_mem *) malloc(sizeof(struct _arrow_mem *)); + assert (_alloc); + return _alloc; +} diff --git a/include/arrow.hpp b/include/arrow.hpp new file mode 100644 index 0000000000000000000000000000000000000000..636c2301e5ca311f963dbc88cd5261c2d1048a07 --- /dev/null +++ b/include/arrow.hpp @@ -0,0 +1,38 @@ + +#ifndef _ARROW_CPP +#define _ARROW_CPP + +#include <stdlib.h> + +struct _arrow_mem { + struct _arrow_reg { + bool _first; + } _reg; +}; + +extern struct _arrow_mem *_arrow_alloc (); + +#define _arrow_DECLARE(attr, inst)\ + attr struct _arrow_mem inst; + +#define _arrow_LINK(inst) do {\ + ;\ +} while (0) + +#define _arrow_ALLOC(attr, inst)\ + _arrow_DECLARE(attr, inst);\ + _arrow_LINK(inst) + +#define _arrow_init(self) {} + +#define _arrow_clear(self) {} + +#define _arrow_step(x,y,output,self) ((self)->_reg._first?((self)->_reg._first=0,(*output = x)):(*output = y)) + +#define _arrow_reset(self) {(self)->_reg._first = 1;} + +/* Step macro for specialized arrows of the form: (true -> false) */ + +#define _once_step(output,self) { *output = (self)->_reg._first; if ((self)->_reg._first) { (self)->_reg._first=0; }; } + +#endif diff --git a/include/io_frontend.hpp b/include/io_frontend.hpp new file mode 100644 index 0000000000000000000000000000000000000000..0450f44dde9ccf4e80817f6b0071eae6cc517dcb --- /dev/null +++ b/include/io_frontend.hpp @@ -0,0 +1,94 @@ +#ifndef _IO_FRONTEND_HPP +#define _IO_FRONTEND_HPP + +#include <stdlib.h> /* Provides exit */ +#include <stdio.h> /* Provides printf, scanf, sscanf */ +#include <unistd.h> /* Provides isatty */ + +int ISATTY; + +/* Standard Input procedures **************/ +bool _get_bool(FILE* file, char* n){ + char b[512]; + bool r = 0; + int s = 1; + char c; + do { + if(ISATTY) { + if((s != 1)||(r == -1)) printf("\a"); + printf("%s (1,t,T/0,f,F) ? ", n); + } + if(scanf("%s", b)==EOF) exit(0); + s = sscanf(b, "%c", &c); + r = -1; + if((c == '0') || (c == 'f') || (c == 'F')) r = 0; + if((c == '1') || (c == 't') || (c == 'T')) r = 1; + } while((s != 1) || (r == -1)); + fprintf(file, "%i\n",r); + return r; +} + +int _get_int(FILE* file, char* n){ + char b[512]; + int r; + int s = 1; + do { + if(ISATTY) { + if(s != 1) printf("\a"); + printf("%s (integer) ? ", n); + } + if(scanf("%s", b)==EOF) exit(0); + s = sscanf(b, "%d", &r); + } while(s != 1); + fprintf(file, "%d\n", r); + return r; +} + +double _get_double(FILE* file, char* n){ + char b[512]; + double r; + int s = 1; + do { + if(ISATTY) { + if(s != 1) printf("\a"); + printf("%s (double) ? ", n); + } + if(scanf("%s", b)==EOF) exit(0); + s = sscanf(b, "%lf", &r); + } while(s != 1); + fprintf(file, "%f\n", r); + return r; +} +/* Standard Output procedures **************/ +void _put_bool(FILE* file, char* n, bool _V){ + if(ISATTY) { + printf("%s = ", n); + } else { + printf("'%s': ", n); + }; + printf("'%i' ", (_V)? 1 : 0); + printf("\n"); + fprintf(file, "%i\n", _V); +} +void _put_int(FILE* file, char* n, int _V){ + if(ISATTY) { + printf("%s = ", n); + } else { + printf("'%s': ", n); + }; + printf("'%d' ", _V); + printf("\n"); + fprintf(file, "%d\n", _V); +} +void _put_double(FILE* file, char* n, double _V){ + if(ISATTY) { + printf("%s = ", n); + } else { + printf("'%s': ", n); + }; + printf("'%f' ", _V); + printf("\n"); + fprintf(file, "%f\n", _V); +} + +#endif diff --git a/src/Makefile b/src/Makefile index 822ecdf695da2f7e61245dfadc973bcc501483c4..c401e4c638044b6e4ba6343f63447c5cdc710696 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,6 +1,6 @@ OCAMLBUILD=/usr/bin/ocamlbuild -classic-display -use-ocamlfind -no-links -prefix=/home/ploc/Local +prefix=/usr/local exec_prefix=${prefix} bindir=${exec_prefix}/bin datarootdir = ${prefix}/share diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml index 0fa4971b627338908b57d515ad828e6acb83216f..d5749dd57bb9e0400df2884940a4ee01ffbef593 100644 --- a/src/backends/C/c_backend.ml +++ b/src/backends/C/c_backend.ml @@ -38,7 +38,7 @@ let gen_files funs basename prog machines dependencies = close_out header_out; (* Generating Lib C file *) - let source_lib_file = destname ^ ".c" in (* Could be changed *) + let source_lib_file = (if !Options.cpp then destname ^ ".cpp" else destname ^ ".c") in (* Could be changed *) let source_lib_out = open_out source_lib_file in let source_lib_fmt = formatter_of_out_channel source_lib_out in print_lib_c source_lib_fmt basename prog machines dependencies; @@ -54,7 +54,7 @@ let gen_files funs basename prog machines dependencies = raise (Corelang.Error (Location.dummy_loc, LustreSpec.Main_not_found)) end | Some m -> begin - let source_main_file = destname ^ "_main.c" in (* Could be changed *) + let source_main_file = (if !Options.cpp then destname ^ "_main.cpp" else destname ^ "_main.c") in (* Could be changed *) let source_main_out = open_out source_main_file in let source_main_fmt = formatter_of_out_channel source_main_out in diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml index 78aa10088364499f844da5c110b063a8ec2340a2..803b426ee640779a47e4721bb19e27291975a1a2 100644 --- a/src/backends/C/c_backend_common.ml +++ b/src/backends/C/c_backend_common.ml @@ -124,14 +124,17 @@ let is_basic_c_type t = | Types.Tbool | Types.Treal | Types.Tint -> true | _ -> false -let pp_basic_c_type fmt t = - match (Types.repr t).Types.tdesc with - | Types.Tbool -> fprintf fmt "_Bool" - | Types.Treal when !Options.mpfr -> fprintf fmt "%s" Mpfr.mpfr_t - | Types.Treal -> fprintf fmt "double" - | Types.Tint -> fprintf fmt "int" +let pp_c_basic_type_desc t_dsec = + match (t_dsec) with + | Types.Tbool when !Options.cpp -> "bool" + | Types.Tbool -> "_Bool" + | Types.Tint -> !Options.int_type + | Types.Treal when !Options.mpfr -> Mpfr.mpfr_t + | Types.Treal -> !Options.real_type | _ -> assert false (* Not a basic C type. Do not handle arrays or pointers *) +let pp_basic_c_type fmt t = fprintf fmt "%s" (pp_c_basic_type_desc (Types.repr t).Types.tdesc) + let pp_c_type var fmt t = let rec aux t pp_suffix = match (Types.repr t).Types.tdesc with diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml index 09d4f683c738399bd691932db1af066d14866964..6b792a44d63508d782454468df52d64507757300 100644 --- a/src/backends/C/c_backend_header.ml +++ b/src/backends/C/c_backend_header.ml @@ -39,7 +39,10 @@ let print_import_standard fmt = begin fprintf fmt "#include <mpfr.h>@." end; - fprintf fmt "#include \"%s/arrow.h\"@.@." !Options.include_dir + if !Options.cpp then + fprintf fmt "#include \"%s/arrow.hpp\"@.@." !Options.include_dir + else + fprintf fmt "#include \"%s/arrow.h\"@.@." !Options.include_dir end diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml index 9283feaafebd56b05c40d3afd0b96df3d87117c6..6404ad13132519f7cdb87d1f95079a461735c3f7 100644 --- a/src/backends/C/c_backend_main.ml +++ b/src/backends/C/c_backend_main.ml @@ -179,7 +179,7 @@ let print_main_code fmt basename m = fprintf fmt "@]@ }@." let print_main_header fmt = - fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@." + fprintf fmt (if !Options.cpp then "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.hpp\"@." else "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@.") !Options.include_dir let print_main_c main_fmt main_machine basename prog machines _ (*dependencies*) = diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml index f4a3b532584d6505f3bb243fcae401b72235a30c..048de2a4f157c3f87f88e5dd4912d45b5a409b4f 100644 --- a/src/backends/C/c_backend_src.ml +++ b/src/backends/C/c_backend_src.ml @@ -588,8 +588,9 @@ let print_step_code dependencies fmt m self = let print_global_init_code fmt basename prog dependencies = let baseNAME = file_to_module_name basename in let constants = List.map const_of_top (get_consts prog) in - fprintf fmt "@[<v 2>%a {@,static _Bool init = 0;@,@[<v 2>if (!init) { @,init = 1;@,%a%t%a@]@,}@,return;@]@,}@.@." + fprintf fmt "@[<v 2>%a {@,static %s init = 0;@,@[<v 2>if (!init) { @,init = 1;@,%a%t%a@]@,}@,return;@]@,}@.@." print_global_init_prototype baseNAME + (pp_c_basic_type_desc Types.Tbool) (* constants *) (Utils.fprintf_list ~sep:"@," (pp_const_initialize (pp_c_var_read Machine_code.empty_machine))) constants (Utils.pp_final_char_if_non_empty "@," dependencies) @@ -599,8 +600,9 @@ let print_global_init_code fmt basename prog dependencies = let print_global_clear_code fmt basename prog dependencies = let baseNAME = file_to_module_name basename in let constants = List.map const_of_top (get_consts prog) in - fprintf fmt "@[<v 2>%a {@,static _Bool clear = 0;@,@[<v 2>if (!clear) { @,clear = 1;@,%a%t%a@]@,}@,return;@]@,}@.@." + fprintf fmt "@[<v 2>%a {@,static %s clear = 0;@,@[<v 2>if (!clear) { @,clear = 1;@,%a%t%a@]@,}@,return;@]@,}@.@." print_global_clear_prototype baseNAME + (pp_c_basic_type_desc Types.Tbool) (* constants *) (Utils.fprintf_list ~sep:"@," (pp_const_clear (pp_c_var_read Machine_code.empty_machine))) constants (Utils.pp_final_char_if_non_empty "@," dependencies) diff --git a/src/options.ml b/src/options.ml index 42d0071657ab6bb007bf1e3a31aff7d12af7ee6a..98d684e6253281282669fa9f108709e3c3f85875 100755 --- a/src/options.ml +++ b/src/options.ml @@ -51,6 +51,10 @@ let horn_query = ref true let salsa_enabled = ref true +let cpp = ref false +let int_type = ref "int" +let real_type = ref "double" + let sfunction = ref "" let set_mpfr prec = @@ -89,7 +93,12 @@ let options = "-print_clocks", Arg.Set print_clocks, "prints node clocks"; "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>"; "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>"; - "-version", Arg.Unit print_version, " displays the version";] + "-version", Arg.Unit print_version, " displays the version"; + + "-c++" , Arg.Set cpp , "c++ backend"; + "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")"; + "-real", Arg.Set_string real_type, "specifies the real type (default=\"double\" without mpfr option)"; +] let plugin_opt (name, activate, options) =