Revision 86ae18b7
README.md | ||
---|---|---|
1 |
|
|
1 | 2 |
Current Status: [](https://travis-ci.org/coco-team/lustrec) |
3 |
|
|
4 |
[](https://waffle.io/coco-team/lustrec) |
|
5 |
[](https://waffle.io/coco-team/lustrec/metrics/throughput) |
|
6 |
|
|
2 | 7 |
# LustreC |
3 | 8 |
|
4 | 9 |
LustreC is a modular compiler of Lustre code into C and Horn Clauses. |
configure.ac | ||
---|---|---|
1 | 1 |
define([gitversion], esyscmd([sh -c "git log --oneline | wc -l | tr -d '\n'"])) |
2 | 2 |
|
3 |
AC_INIT([lustrec], [1.4-gitversion], [ploc@garoche.net])
|
|
4 |
AC_SUBST(VERSION_CODENAME, "Xia/Xiang-dev")
|
|
3 |
AC_INIT([lustrec], [1.3-gitversion], [ploc@garoche.net])
|
|
4 |
AC_SUBST(VERSION_CODENAME, "Xia/Zhong-Kang-dev")
|
|
5 | 5 |
# Next release will be |
6 |
#AC_INIT([lustrec], [1.5], [ploc@garoche.net]) |
|
7 |
#AC_SUBST(VERSION_CODENAME, "Xia/Shao Kang") |
|
6 |
#AC_INIT([lustrec], [1.3], [ploc@garoche.net]) |
|
7 |
#AC_SUBST(VERSION_CODENAME, "Xia/Zhong-Kang") |
|
8 |
|
|
9 |
#AC_DEFINE(SVN_REVISION, "svnversion", [SVN Revision]) |
|
10 |
#AC_SUBST(SVN_REVISION) |
|
8 | 11 |
|
9 | 12 |
AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml]) |
10 | 13 |
|
... | ... | |
98 | 101 |
# Instanciation |
99 | 102 |
AC_CONFIG_FILES([Makefile |
100 | 103 |
src/Makefile |
101 |
src/myocamlbuild.ml |
|
102 | 104 |
src/version.ml |
103 | 105 |
test/test-compile.sh |
104 | 106 |
]) |
include/io_frontend.c | ||
---|---|---|
6 | 6 |
int ISATTY; |
7 | 7 |
|
8 | 8 |
/* Standard Input procedures **************/ |
9 |
_Bool _get_bool(FILE* file, char* n){
|
|
9 |
_Bool _get_bool(char* n){ |
|
10 | 10 |
char b[512]; |
11 | 11 |
_Bool r = 0; |
12 | 12 |
int s = 1; |
... | ... | |
22 | 22 |
if((c == '0') || (c == 'f') || (c == 'F')) r = 0; |
23 | 23 |
if((c == '1') || (c == 't') || (c == 'T')) r = 1; |
24 | 24 |
} while((s != 1) || (r == -1)); |
25 |
fprintf(file, "%i\n",r); |
|
26 | 25 |
return r; |
27 | 26 |
} |
28 |
|
|
29 |
int _get_int(FILE* file, char* n){ |
|
27 |
int _get_int(char* n){ |
|
30 | 28 |
char b[512]; |
31 | 29 |
int r; |
32 | 30 |
int s = 1; |
... | ... | |
38 | 36 |
if(scanf("%s", b)==EOF) exit(0); |
39 | 37 |
s = sscanf(b, "%d", &r); |
40 | 38 |
} while(s != 1); |
41 |
fprintf(file, "%d\n", r); |
|
42 | 39 |
return r; |
43 | 40 |
} |
44 |
|
|
45 |
double _get_double(FILE* file, char* n){ |
|
41 |
double _get_double(char* n){ |
|
46 | 42 |
char b[512]; |
47 | 43 |
double r; |
48 | 44 |
int s = 1; |
... | ... | |
54 | 50 |
if(scanf("%s", b)==EOF) exit(0); |
55 | 51 |
s = sscanf(b, "%lf", &r); |
56 | 52 |
} while(s != 1); |
57 |
fprintf(file, "%f\n", r); |
|
58 | 53 |
return r; |
59 | 54 |
} |
60 | 55 |
/* Standard Output procedures **************/ |
61 |
void _put_bool(FILE* file, char* n, _Bool _V){
|
|
56 |
void _put_bool(char* n, _Bool _V){ |
|
62 | 57 |
if(ISATTY) { |
63 | 58 |
printf("%s = ", n); |
64 | 59 |
} else { |
... | ... | |
66 | 61 |
}; |
67 | 62 |
printf("'%i' ", (_V)? 1 : 0); |
68 | 63 |
printf("\n"); |
69 |
fprintf(file, "%i\n", _V); |
|
70 | 64 |
} |
71 |
void _put_int(FILE* file, char* n, int _V){
|
|
65 |
void _put_int(char* n, int _V){ |
|
72 | 66 |
if(ISATTY) { |
73 | 67 |
printf("%s = ", n); |
74 | 68 |
} else { |
... | ... | |
76 | 70 |
}; |
77 | 71 |
printf("'%d' ", _V); |
78 | 72 |
printf("\n"); |
79 |
fprintf(file, "%d\n", _V); |
|
80 | 73 |
} |
81 |
void _put_double(FILE* file, char* n, double _V){
|
|
74 |
void _put_double(char* n, double _V){ |
|
82 | 75 |
if(ISATTY) { |
83 | 76 |
printf("%s = ", n); |
84 | 77 |
} else { |
... | ... | |
86 | 79 |
}; |
87 | 80 |
printf("'%f' ", _V); |
88 | 81 |
printf("\n"); |
89 |
fprintf(file, "%f\n", _V); |
|
90 | 82 |
} |
include/io_frontend.h | ||
---|---|---|
7 | 7 |
/* Standard Input procedures **************/ |
8 | 8 |
|
9 | 9 |
/*@ assigns *n; */ |
10 |
extern _Bool _get_bool(FILE* file, char* n);
|
|
10 |
extern _Bool _get_bool(char* n); |
|
11 | 11 |
|
12 | 12 |
/*@ assigns *n; */ |
13 |
extern int _get_int(FILE* file, char* n);
|
|
13 |
extern int _get_int(char* n); |
|
14 | 14 |
|
15 | 15 |
/*@ assigns *n; */ |
16 |
extern double _get_double(FILE* file, char* n);
|
|
16 |
extern double _get_double(char* n); |
|
17 | 17 |
|
18 | 18 |
/* Standard Output procedures **************/ |
19 | 19 |
/*@ assigns \nothing; */ |
20 |
extern void _put_bool(FILE* file, char* n, _Bool _V);
|
|
20 |
extern void _put_bool(char* n, _Bool _V); |
|
21 | 21 |
|
22 | 22 |
/*@ assigns \nothing; */ |
23 |
extern void _put_int(FILE* file, char* n, int _V);
|
|
23 |
extern void _put_int(char* n, int _V); |
|
24 | 24 |
|
25 | 25 |
/*@ assigns \nothing; */ |
26 |
extern void _put_double(FILE* file, char* n, double _V);
|
|
26 |
extern void _put_double(char* n, double _V); |
|
27 | 27 |
|
28 | 28 |
#endif |
include/math.smt2 | ||
---|---|---|
1 |
(declare-rel cbrt (Real Real)) |
|
2 |
(declare-rel ceil (Real Real)) |
|
3 |
(declare-rel erf (Real Real)) |
|
4 |
(declare-rel fabs (Real Real)) |
|
5 |
(declare-rel pow (Real Real Real)) |
|
6 |
(declare-rel sqrt (Real Real)) |
lustrec.odocl | ||
---|---|---|
7 | 7 |
backends/C/C_backend_makefile |
8 | 8 |
backends/C/C_backend_spec |
9 | 9 |
backends/C/C_backend_src |
10 |
backends/Horn/Horn_backend_common |
|
11 |
backends/Horn/Horn_backend_printers |
|
12 |
backends/Horn/Horn_backend_collecting_sem |
|
13 | 10 |
backends/Horn/Horn_backend |
14 |
plugins/scopes/Scopes |
|
15 | 11 |
Basic_library |
16 | 12 |
Causality |
17 | 13 |
Clock_calculus |
... | ... | |
23 | 19 |
Delay_predef |
24 | 20 |
Dimension |
25 | 21 |
Env |
26 |
Global |
|
27 | 22 |
Inliner |
28 | 23 |
Lexer_lustre |
29 | 24 |
LexerLustreSpec |
... | ... | |
35 | 30 |
Machine_code |
36 | 31 |
Main_lustre_compiler |
37 | 32 |
Modules |
38 |
Mpfr |
|
39 | 33 |
Normalization |
40 | 34 |
Optimize_machine |
41 | 35 |
Optimize_prog |
42 | 36 |
Options |
43 | 37 |
Parse |
44 | 38 |
Parser_lustre |
45 |
Plugins |
|
46 | 39 |
Printers |
47 | 40 |
Scheduling |
48 | 41 |
SortProg |
share/FindLustre.cmake | ||
---|---|---|
17 | 17 |
# LUS_FILES <Lustre files> |
18 | 18 |
# [USER_C_FILES <C files>] |
19 | 19 |
# [VERBOSE <level>] |
20 |
# [LUSI] |
|
21 | 20 |
# LIBNAME <libraryName>) |
22 | 21 |
# |
23 | 22 |
# When used the Lustre_Compile macro define the variable |
... | ... | |
73 | 72 |
# Macros used to compile a lustre library |
74 | 73 |
include(CMakeParseArguments) |
75 | 74 |
function(Lustre_Compile) |
76 |
set(options LUSI)
|
|
75 |
set(options "")
|
|
77 | 76 |
set(oneValueArgs NODE LIBNAME VERBOSE) |
78 | 77 |
set(multiValueArgs LUS_FILES USER_C_FILES) |
79 | 78 |
cmake_parse_arguments(LUS "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN}) |
80 | 79 |
|
81 |
if(LUS_LUSI) |
|
82 |
set(LUSTRE_LUSI_OPT "-lusi") |
|
83 |
endif() |
|
84 |
|
|
85 | 80 |
if (NOT LUS_LIBNAME) |
86 | 81 |
message(FATAL_ERROR "You should specify LIBNAME for each Lustre_Compile call.") |
87 | 82 |
endif() |
88 | 83 |
|
89 | 84 |
if(LUS_NODE) |
90 |
set(LUSTRE_NODE_OPT "-node;${LUS_NODE}")
|
|
85 |
set(LUSTRE_NODE_OPT "-node ${LUS_NODE}")
|
|
91 | 86 |
set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/lus_${LUS_LIBNAME}/${LUS_NODE}") |
92 | 87 |
else() |
93 | 88 |
set(LUSTRE_NODE_OPT "") |
... | ... | |
95 | 90 |
endif() |
96 | 91 |
|
97 | 92 |
if (LUS_VERBOSE) |
98 |
set(LUSTRE_VERBOSE_OPT "-verbose;${LUS_VERBOSE}")
|
|
93 |
set(LUSTRE_VERBOSE_OPT "-verbose ${LUS_VERBOSE}")
|
|
99 | 94 |
else() |
100 | 95 |
# the default is to be quiet. |
101 | 96 |
set(LUSTRE_VERBOSE_OPT "-verbose;0") |
... | ... | |
110 | 105 |
get_filename_component(E ${LFILE} EXT) |
111 | 106 |
if ("${E}" STREQUAL ".lus") |
112 | 107 |
set(LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}.h ${LUSTRE_OUTPUT_DIR}/${L}.c ${LUSTRE_OUTPUT_DIR}/${L}_alloc.h) |
113 |
if(LUS_NODE) |
|
114 |
list(APPEND LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}_main.c) |
|
115 |
list(APPEND LUSTRE_GENERATED_FILES ${LUSTRE_INCLUDE_DIR}/io_frontend.c) |
|
116 |
endif() |
|
117 | 108 |
elseif("${E}" STREQUAL ".lusi") |
118 | 109 |
set(LUSTRE_GENERATED_FILES ${LUSTRE_OUTPUT_DIR}/${L}.h) |
119 | 110 |
endif() |
120 | 111 |
list(APPEND GLOBAL_LUSTRE_GENERATED_C_FILES ${LUSTRE_GENERATED_FILES}) |
121 | 112 |
set(LUSTRE_GENERATED_FILES ${LUSTRE_GENERATED_FILES} ${LUSTRE_OUTPUT_DIR}/${L}.lusic) |
122 |
if (LUS_LUSI) |
|
123 |
add_custom_command( |
|
124 |
OUTPUT ${CMAKE_CURRENT_SOURCE_DIR}/${LFILE}i |
|
125 |
COMMAND ${LUSTRE_COMPILER} ${LUSTRE_LUSI_OPT} ${LFILE} |
|
126 |
DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/${LFILE} |
|
127 |
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} |
|
128 |
COMMENT "Compile Lustre source(s): ${LFILE} with option -lusi." |
|
129 |
) |
|
130 |
message(STATUS "lustrec will produce lusi file: ${LFILE}i") |
|
131 |
endif() |
|
132 | 113 |
add_custom_command( |
133 | 114 |
OUTPUT ${LUSTRE_GENERATED_FILES} |
134 | 115 |
COMMAND ${LUSTRE_COMPILER} ${LUSTRE_VERBOSE_OPT} ${LUSTRE_NODE_OPT} -d ${LUSTRE_OUTPUT_DIR} ${LFILE} |
... | ... | |
140 | 121 |
endforeach() |
141 | 122 |
|
142 | 123 |
include_directories(${LUSTRE_INCLUDE_DIR} ${CMAKE_CURRENT_SOURCE_DIR} ${LUSTRE_OUTPUT_DIR}) |
143 |
if(LUS_NODE) |
|
144 |
add_executable(${LUS_LIBNAME} |
|
145 |
${GLOBAL_LUSTRE_GENERATED_C_FILES} ${LUS_USER_C_FILES} |
|
146 |
) |
|
147 |
else() |
|
148 | 124 |
add_library(${LUS_LIBNAME} SHARED |
149 | 125 |
${GLOBAL_LUSTRE_GENERATED_C_FILES} ${LUS_USER_C_FILES} |
150 | 126 |
) |
151 |
endif() |
|
152 | 127 |
set_target_properties(${LUS_LIBNAME} PROPERTIES COMPILE_FLAGS "-std=c99") |
153 | 128 |
set(LUSTRE_GENERATED_C_FILES_${LUS_LIBNAME} "${GLOBAL_LUSTRE_GENERATED_C_FILES}" PARENT_SCOPE) |
154 | 129 |
message(STATUS "Lustre: Added rule for building lustre library: ${LUS_LIBNAME}") |
src/_tags | ||
---|---|---|
2 | 2 |
"backends/Horn": include |
3 | 3 |
<**/.svn>: -traverse |
4 | 4 |
<**/.svn>: not_hygienic |
5 |
"main_lustre_compiler.native": use_graph
|
|
5 |
#"main_lustre_compiler.native": package(ocamlgraph)
|
|
6 | 6 |
"main_lustre_compiler.native": use_str |
7 | 7 |
"main_lustre_compiler.native": use_unix |
8 |
<*.ml{,i}>: use_graph
|
|
8 |
#<*.ml{,i}>: package(ocamlgraph)
|
|
9 | 9 |
<*.ml{,i}>: use_str |
10 | 10 |
<*.ml{,i}>: use_unix |
src/backends/C/c_backend.ml | ||
---|---|---|
27 | 27 |
|
28 | 28 |
let gen_files funs basename prog machines dependencies = |
29 | 29 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
30 |
|
|
31 |
let print_header, print_lib_c, print_main_c, print_makefile, print_cmake = funs in |
|
30 |
let source_main_file = destname ^ "_main.c" in (* Could be changed *) |
|
31 |
let makefile_file = destname ^ ".makefile" in (* Could be changed *) |
|
32 |
|
|
33 |
let print_header, print_lib_c, print_main_c, print_makefile = funs in |
|
32 | 34 |
|
33 | 35 |
(* Generating H file *) |
34 | 36 |
let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *) |
... | ... | |
36 | 38 |
let header_fmt = formatter_of_out_channel header_out in |
37 | 39 |
print_header header_fmt basename prog machines dependencies; |
38 | 40 |
close_out header_out; |
39 |
|
|
41 |
|
|
40 | 42 |
(* Generating Lib C file *) |
41 | 43 |
let source_lib_file = destname ^ ".c" in (* Could be changed *) |
42 | 44 |
let source_lib_out = open_out source_lib_file in |
... | ... | |
44 | 46 |
print_lib_c source_lib_fmt basename prog machines dependencies; |
45 | 47 |
close_out source_lib_out; |
46 | 48 |
|
47 |
(match !Options.main_node with
|
|
48 |
| "" -> () (* No main node: we do not generate main *) |
|
49 |
match !Options.main_node with |
|
50 |
| "" -> () (* No main node: we do not generate main nor makefile *)
|
|
49 | 51 |
| main_node -> ( |
50 | 52 |
match Machine_code.get_machine_opt main_node machines with |
51 | 53 |
| None -> begin |
... | ... | |
54 | 56 |
raise (Corelang.Error (Location.dummy_loc, LustreSpec.Main_not_found)) |
55 | 57 |
end |
56 | 58 |
| Some m -> begin |
57 |
let source_main_file = destname ^ "_main.c" in (* Could be changed *) |
|
58 | 59 |
let source_main_out = open_out source_main_file in |
59 | 60 |
let source_main_fmt = formatter_of_out_channel source_main_out in |
61 |
let makefile_out = open_out makefile_file in |
|
62 |
let makefile_fmt = formatter_of_out_channel makefile_out in |
|
60 | 63 |
|
61 | 64 |
(* Generating Main C file *) |
62 | 65 |
print_main_c source_main_fmt m basename prog machines dependencies; |
63 | 66 |
|
64 |
close_out source_main_out; |
|
67 |
(* Generating Makefile *) |
|
68 |
print_makefile basename main_node dependencies makefile_fmt; |
|
69 |
|
|
70 |
close_out source_main_out; |
|
71 |
close_out makefile_out |
|
72 |
|
|
65 | 73 |
end |
66 |
)); |
|
67 |
|
|
68 |
|
|
69 |
(* Makefiles: |
|
70 |
- for the moment two cases |
|
71 |
1. Classical Makefile, only when provided with a main node |
|
72 |
May contain additional framac eacsl targets |
|
73 |
2. Cmake : 2 files |
|
74 |
- lustrec-basename.cmake describing all variables |
|
75 |
- the main CMakeLists.txt activating the first file |
|
76 |
- Later option 1 should be removed |
|
77 |
*) |
|
78 |
(* Case 1 *) |
|
79 |
(match !Options.main_node with |
|
80 |
| "" -> () (* No main node: we do not generate main *) |
|
81 |
| main_node -> ( |
|
82 |
let makefile_file = destname ^ ".makefile" in (* Could be changed *) |
|
83 |
let makefile_out = open_out makefile_file in |
|
84 |
let makefile_fmt = formatter_of_out_channel makefile_out in |
|
85 |
|
|
86 |
(* Generating Makefile *) |
|
87 |
print_makefile basename main_node dependencies makefile_fmt; |
|
88 |
|
|
89 |
close_out makefile_out |
|
90 |
)); |
|
91 |
|
|
92 |
(* Case 2 *) |
|
93 |
let cmake_file = "lustrec-" ^ basename ^ ".cmake" in |
|
94 |
let cmake_file_full_path = !Options.dest_dir ^ "/" ^ cmake_file in |
|
95 |
let cmake_out = open_out cmake_file_full_path in |
|
96 |
let cmake_fmt = formatter_of_out_channel cmake_out in |
|
97 |
(* Generating Makefile *) |
|
98 |
print_cmake basename main_node dependencies makefile_fmt; |
|
99 |
|
|
100 |
close_out makefile_out |
|
101 |
|
|
74 |
) |
|
102 | 75 |
|
103 | 76 |
let translate_to_c basename prog machines dependencies = |
104 | 77 |
match !Options.spec with |
... | ... | |
112 | 85 |
let module Source = C_backend_src.Main (SourceMod) in |
113 | 86 |
let module SourceMain = C_backend_main.Main (SourceMainMod) in |
114 | 87 |
let module Makefile = C_backend_makefile.Main (MakefileMod) in |
115 |
let module CMakefile = C_backend_cmake.Main (MakefileMod) in |
|
116 |
|
|
117 |
let funs = |
|
118 |
Header.print_alloc_header, |
|
119 |
Source.print_lib_c, |
|
120 |
SourceMain.print_main_c, |
|
121 |
Makefile.print_makefile, |
|
122 |
CMakefile.print_makefile |
|
88 |
|
|
89 |
let funs = |
|
90 |
Header.print_alloc_header, |
|
91 |
Source.print_lib_c, |
|
92 |
SourceMain.print_main_c, |
|
93 |
Makefile.print_makefile |
|
123 | 94 |
in |
124 |
gen_files funs basename prog machines dependencies
|
|
95 |
gen_files funs basename prog machines dependencies |
|
125 | 96 |
|
126 | 97 |
end |
127 | 98 |
| "acsl" -> begin |
... | ... | |
135 | 106 |
let module Source = C_backend_src.Main (SourceMod) in |
136 | 107 |
let module SourceMain = C_backend_main.Main (SourceMainMod) in |
137 | 108 |
let module Makefile = C_backend_makefile.Main (MakefileMod) in |
138 |
let module CMakefile = C_backend_cmake.Main (MakefileMod) in |
|
139 |
|
|
140 |
let funs = |
|
141 |
Header.print_alloc_header, |
|
109 |
|
|
110 |
let funs = |
|
111 |
Header.print_alloc_header, |
|
142 | 112 |
Source.print_lib_c, |
143 | 113 |
SourceMain.print_main_c, |
144 |
Makefile.print_makefile, |
|
145 |
CMakefile.print_makefile |
|
114 |
Makefile.print_makefile |
|
146 | 115 |
in |
147 |
gen_files funs basename prog machines dependencies
|
|
116 |
gen_files funs basename prog machines dependencies |
|
148 | 117 |
|
149 | 118 |
end |
150 | 119 |
| "c" -> begin |
src/backends/C/c_backend_header.ml | ||
---|---|---|
39 | 39 |
begin |
40 | 40 |
fprintf fmt "#include <mpfr.h>@." |
41 | 41 |
end; |
42 |
fprintf fmt "#include \"%s/arrow.h\"@.@." Version.include_path |
|
42 |
(*fprintf fmt "#include \"%s/arrow.h\"@.@." Version.include_path*) |
|
43 |
fprintf fmt "#include \"%s/arrow.h\"@.@." !Options.include_dir |
|
43 | 44 |
end |
44 | 45 |
|
45 | 46 |
let rec print_static_val pp_var fmt v = |
src/backends/C/c_backend_main.ml | ||
---|---|---|
14 | 14 |
open Machine_code |
15 | 15 |
open Format |
16 | 16 |
open C_backend_common |
17 |
open Utils |
|
18 | 17 |
|
19 | 18 |
module type MODIFIERS_MAINSRC = |
20 | 19 |
sig |
... | ... | |
32 | 31 |
(********************************************************************************************) |
33 | 32 |
|
34 | 33 |
let print_get_inputs fmt m = |
35 |
let pi fmt (id, v', v) =
|
|
34 |
let pi fmt (v', v) = |
|
36 | 35 |
match (Types.unclock_type v.var_type).Types.tdesc with |
37 |
| Types.Tint -> fprintf fmt "%s = _get_int(f_in%i, \"%s\")" v.var_id id v'.var_id
|
|
38 |
| Types.Tbool -> fprintf fmt "%s = _get_bool(f_in%i, \"%s\")" v.var_id id v'.var_id
|
|
39 |
| Types.Treal when !Options.mpfr -> fprintf fmt "mpfr_set_d(%s, _get_double(f_in%i, \"%s\"), %i)" v.var_id id v'.var_id (Mpfr.mpfr_prec ())
|
|
40 |
| Types.Treal -> fprintf fmt "%s = _get_double(f_in%i, \"%s\")" v.var_id id v'.var_id
|
|
36 |
| Types.Tint -> fprintf fmt "%s = _get_int(\"%s\")" v.var_id v'.var_id
|
|
37 |
| Types.Tbool -> fprintf fmt "%s = _get_bool(\"%s\")" v.var_id v'.var_id
|
|
38 |
| Types.Treal when !Options.mpfr -> fprintf fmt "mpfr_set_d(%s, _get_double(\"%s\"), %i)" v.var_id v'.var_id (Mpfr.mpfr_prec ())
|
|
39 |
| Types.Treal -> fprintf fmt "%s = _get_double(\"%s\")" v.var_id v'.var_id
|
|
41 | 40 |
| _ -> |
42 | 41 |
begin |
43 | 42 |
Global.main_node := !Options.main_node; |
... | ... | |
47 | 46 |
raise (Error (v'.var_loc, Main_wrong_kind)) |
48 | 47 |
end |
49 | 48 |
in |
50 |
List.iteri2 (fun idx v' v -> |
|
51 |
fprintf fmt "@ %a;" pi ((idx+1), v', v); |
|
52 |
) m.mname.node_inputs m.mstep.step_inputs |
|
49 |
List.iter2 (fun v' v -> fprintf fmt "@ %a;" pi (v', v)) m.mname.node_inputs m.mstep.step_inputs |
|
53 | 50 |
|
54 | 51 |
let print_put_outputs fmt m = |
55 |
let po fmt (id, o', o) =
|
|
52 |
let po fmt (o', o) = |
|
56 | 53 |
match (Types.unclock_type o.var_type).Types.tdesc with |
57 |
| Types.Tint -> fprintf fmt "_put_int(f_out%i, \"%s\", %s)" id o'.var_id o.var_id
|
|
58 |
| Types.Tbool -> fprintf fmt "_put_bool(f_out%i, \"%s\", %s)" id o'.var_id o.var_id
|
|
59 |
| Types.Treal when !Options.mpfr -> fprintf fmt "_put_double(f_out%i, \"%s\", mpfr_get_d(%s, %s))" id o'.var_id o.var_id (Mpfr.mpfr_rnd ())
|
|
60 |
| Types.Treal -> fprintf fmt "_put_double(f_out%i, \"%s\", %s)" id o'.var_id o.var_id
|
|
54 |
| Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o'.var_id o.var_id
|
|
55 |
| Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o'.var_id o.var_id
|
|
56 |
| Types.Treal when !Options.mpfr -> fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s))" o'.var_id o.var_id (Mpfr.mpfr_rnd ())
|
|
57 |
| Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o'.var_id o.var_id
|
|
61 | 58 |
| _ -> assert false |
62 | 59 |
in |
63 |
Utils.List.iteri2 (fun idx v' v -> fprintf fmt "@ %a;" po ((idx+1), v', v)) m.mname.node_outputs m.mstep.step_outputs |
|
60 |
List.iter2 (fun v' v -> fprintf fmt "@ %a;" po (v', v)) m.mname.node_outputs m.mstep.step_outputs |
|
61 |
|
|
62 |
let print_main_inout_declaration fmt m = |
|
63 |
begin |
|
64 |
fprintf fmt "/* Declaration of inputs/outputs variables */@ "; |
|
65 |
List.iter |
|
66 |
(fun v -> fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type |
|
67 |
) m.mstep.step_inputs; |
|
68 |
List.iter |
|
69 |
(fun v -> fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type |
|
70 |
) m.mstep.step_outputs |
|
71 |
end |
|
64 | 72 |
|
65 |
let print_main_inout_declaration basename fmt m = |
|
66 |
let mname = m.mname.node_id in |
|
67 |
fprintf fmt "/* Declaration of inputs/outputs variables */@ "; |
|
68 |
List.iteri |
|
69 |
(fun idx v -> |
|
70 |
fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type; |
|
71 |
fprintf fmt "FILE *f_in%i;@ " (idx+1); (* we start from 1: in1, in2, ... *) |
|
72 |
fprintf fmt "f_in%i = fopen(\"%s_%s_simu.in%i\", \"w\");@ " (idx+1) basename mname (idx+1); |
|
73 |
) m.mstep.step_inputs; |
|
74 |
List.iteri |
|
75 |
(fun idx v -> |
|
76 |
fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type; |
|
77 |
fprintf fmt "FILE *f_out%i;@ " (idx+1); (* we start from 1: in1, in2, ... *) |
|
78 |
fprintf fmt "f_out%i = fopen(\"%s_%s_simu.out%i\", \"w\");@ " (idx+1) basename mname (idx+1); |
|
79 |
) m.mstep.step_outputs |
|
80 |
|
|
81 |
|
|
82 |
|
|
83 | 73 |
let print_main_memory_allocation mname main_mem fmt m = |
84 | 74 |
if not (fst (get_stateless_status m)) then |
85 | 75 |
begin |
... | ... | |
142 | 132 |
fprintf fmt "@ /* Infinite loop */@ "; |
143 | 133 |
fprintf fmt "@[<v 2>while(1){@ "; |
144 | 134 |
fprintf fmt "fflush(stdout);@ "; |
145 |
List.iteri (fun idx _ -> fprintf fmt "fflush(f_in%i);@ " (idx+1)) m.mstep.step_inputs; |
|
146 |
List.iteri (fun idx _ -> fprintf fmt "fflush(f_out%i);@ " (idx+1)) m.mstep.step_outputs; |
|
147 | 135 |
fprintf fmt "%a@ %t%a" |
148 | 136 |
print_get_inputs m |
149 | 137 |
(fun fmt -> pp_main_call mname main_mem fmt m input_values m.mstep.step_outputs) |
... | ... | |
157 | 145 |
then "&main_mem" |
158 | 146 |
else "main_mem" in |
159 | 147 |
fprintf fmt "@[<v 2>int main (int argc, char *argv[]) {@ "; |
160 |
print_main_inout_declaration basename fmt m;
|
|
148 |
print_main_inout_declaration fmt m; |
|
161 | 149 |
print_main_memory_allocation mname main_mem fmt m; |
162 | 150 |
if !Options.mpfr then |
163 | 151 |
begin |
... | ... | |
179 | 167 |
fprintf fmt "@]@ }@." |
180 | 168 |
|
181 | 169 |
let print_main_header fmt = |
182 |
fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@." Version.include_path |
|
170 |
(*fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@." Version.include_path*) |
|
171 |
fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@." !Options.include_dir |
|
183 | 172 |
|
184 | 173 |
|
185 | 174 |
let print_main_c main_fmt main_machine basename prog machines _ (*dependencies*) = |
src/backends/Horn/horn_backend.ml | ||
---|---|---|
48 | 48 |
) |
49 | 49 |
end |
50 | 50 |
|
51 |
|
|
52 |
let load_file f = |
|
53 |
let ic = open_in f in |
|
54 |
let n = in_channel_length ic in |
|
55 |
let s = String.create n in |
|
56 |
really_input ic s 0 n; |
|
57 |
close_in ic; |
|
58 |
(s) |
|
59 |
|
|
51 | 60 |
let print_type_definitions fmt = |
52 | 61 |
let cpt_type = ref 0 in |
53 | 62 |
Hashtbl.iter (fun typ decl -> |
... | ... | |
68 | 77 |
| _ -> ()) type_table |
69 | 78 |
|
70 | 79 |
|
71 |
let translate fmt basename prog machines = |
|
80 |
|
|
81 |
|
|
82 |
let print_dep fmt prog = |
|
83 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting Horn libraries@,"); |
|
84 |
fprintf fmt "; Statically linked libraries@"; |
|
85 |
let dependencies = Corelang.get_dependencies prog in |
|
86 |
List.iter |
|
87 |
(fun dep -> |
|
88 |
let (local, s) = Corelang.dependency_of_top dep in |
|
89 |
let basename = ((if local then !Options.dest_dir else !Options.include_dir)) ^ s ^ ".smt2" in |
|
90 |
Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename); |
|
91 |
let horn = load_file basename in |
|
92 |
fprintf fmt "@.%s@." horn; |
|
93 |
) |
|
94 |
dependencies |
|
95 |
|
|
96 |
let check_sfunction mannot = |
|
97 |
(*Check if its an sfunction*) |
|
98 |
match mannot with |
|
99 |
[] -> false |
|
100 |
| [x] -> |
|
101 |
begin |
|
102 |
match x.annots with |
|
103 |
[] -> false |
|
104 |
|[(key,va)] -> |
|
105 |
begin |
|
106 |
match key with |
|
107 |
[] -> false |
|
108 |
| [x] -> x == "c_code" || x =="matlab" |
|
109 |
| _ -> false |
|
110 |
end |
|
111 |
|(_,_)::_ -> false |
|
112 |
end |
|
113 |
| _::_ -> false |
|
114 |
|
|
115 |
let translate fmt basename prog machines= |
|
72 | 116 |
(* We print typedef *) |
117 |
print_dep fmt prog; (*print static library e.g. math*) |
|
73 | 118 |
print_type_definitions fmt; |
74 |
List.iter (print_machine machines fmt) (List.rev machines); |
|
119 |
(*List.iter (print_machine machines fmt) (List.rev machines);*) |
|
120 |
List.iter(fun m -> |
|
121 |
let is_sfunction = check_sfunction m.mannot in |
|
122 |
if is_sfunction then( |
|
123 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. detected sfunction: %s@," m.mname.node_id); |
|
124 |
print_sfunction machines fmt m |
|
125 |
) else ( |
|
126 |
print_machine machines fmt m) |
|
127 |
) |
|
128 |
(List.rev machines); |
|
75 | 129 |
main_print machines fmt |
76 | 130 |
|
77 | 131 |
(* Local Variables: *) |
src/backends/Horn/horn_backend_common.ml | ||
---|---|---|
25 | 25 |
| Types.Treal -> fprintf fmt "Real" |
26 | 26 |
| Types.Tconst ty -> pp_print_string fmt ty |
27 | 27 |
| Types.Tclock t -> pp_type fmt t |
28 |
| Types.Tarray _
|
|
29 |
| Types.Tstatic _
|
|
28 |
| Types.Tarray(dim,ty) -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
|
|
29 |
| Types.Tstatic(d, ty)-> pp_type fmt ty
|
|
30 | 30 |
| Types.Tarrow _ |
31 | 31 |
| _ -> eprintf "internal error: pp_type %a@." |
32 | 32 |
Types.print_ty t; assert false |
... | ... | |
69 | 69 |
|
70 | 70 |
let local_memory_vars machines machine = |
71 | 71 |
rename_machine_list machine.mname.node_id machine.mmemory |
72 |
|
|
72 |
|
|
73 | 73 |
let instances_memory_vars ?(without_arrow=false) machines machine = |
74 | 74 |
let rec aux fst prefix m = |
75 | 75 |
( |
... | ... | |
81 | 81 |
List.fold_left (fun accu (id, (n, _)) -> |
82 | 82 |
let name = node_name n in |
83 | 83 |
if without_arrow && name = "_arrow" then |
84 |
accu
|
|
84 |
accu |
|
85 | 85 |
else |
86 | 86 |
let machine_n = get_machine machines name in |
87 |
( aux false (concat prefix
|
|
87 |
( aux false (concat prefix |
|
88 | 88 |
(if fst then id else concat m.mname.node_id id)) |
89 | 89 |
machine_n ) @ accu |
90 | 90 |
) [] (m.minstances) |
... | ... | |
101 | 101 |
|
102 | 102 |
let step_vars machines m = |
103 | 103 |
(inout_vars machines m) |
104 |
@ (rename_current_list (full_memory_vars machines m))
|
|
104 |
@ (rename_current_list (full_memory_vars machines m)) |
|
105 | 105 |
@ (rename_next_list (full_memory_vars machines m)) |
106 | 106 |
|
107 | 107 |
let step_vars_m_x machines m = |
108 | 108 |
(inout_vars machines m) |
109 |
@ (rename_mid_list (full_memory_vars machines m))
|
|
109 |
@ (rename_mid_list (full_memory_vars machines m)) |
|
110 | 110 |
@ (rename_next_list (full_memory_vars machines m)) |
111 | 111 |
|
112 | 112 |
let reset_vars machines m = |
113 |
(rename_current_list (full_memory_vars machines m))
|
|
113 |
(rename_current_list (full_memory_vars machines m)) |
|
114 | 114 |
@ (rename_mid_list (full_memory_vars machines m)) |
115 | 115 |
|
116 | 116 |
|
src/backends/Horn/horn_backend_printers.ml | ||
---|---|---|
21 | 21 |
open Machine_code |
22 | 22 |
|
23 | 23 |
open Horn_backend_common |
24 |
|
|
24 |
open Types |
|
25 | 25 |
|
26 | 26 |
(********************************************************************************************) |
27 | 27 |
(* Instruction Printing functions *) |
28 | 28 |
(********************************************************************************************) |
29 | 29 |
|
30 | 30 |
let pp_horn_var m fmt id = |
31 |
if Types.is_array_type id.var_type |
|
31 |
(*if Types.is_array_type id.var_type
|
|
32 | 32 |
then |
33 | 33 |
assert false (* no arrays in Horn output *) |
34 |
else |
|
34 |
else*)
|
|
35 | 35 |
fprintf fmt "%s" id.var_id |
36 | 36 |
|
37 | 37 |
(* Used to print boolean constants *) |
... | ... | |
46 | 46 |
| Const_tag t -> pp_horn_tag fmt t |
47 | 47 |
| _ -> assert false |
48 | 48 |
|
49 |
(* PL comment 2017/01/03: Useless code, the function existed before in typing.ml *) |
|
50 |
(* let rec get_type_cst c = *) |
|
51 |
(* match c with *) |
|
52 |
(* | Const_int(n) -> new_ty Tint *) |
|
53 |
(* | Const_real _ -> new_ty Treal *) |
|
54 |
(* (\* | Const_float _ -> new_ty Treal *\) *) |
|
55 |
(* | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), *) |
|
56 |
(* get_type_cst (List.hd l))) *) |
|
57 |
(* | Const_tag(tag) -> new_ty Tbool *) |
|
58 |
(* | Const_string(str) -> assert false(\* used only for annotations *\) *) |
|
59 |
(* | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) *) |
|
60 |
|
|
61 |
(* PL comment 2017/01/03: the following function get_type seems useless to me: it looks like computing the type of a machine code expression v while v.value_type should contain this information. The code is kept for the moment in case I missed something *) |
|
62 |
|
|
63 |
(* |
|
64 |
let rec get_type v = |
|
65 |
match v with |
|
66 |
| Cst c -> Typing.type_const Location.dummy_loc c (* get_type_cst c*) |
|
67 |
| Access(tab, index) -> begin |
|
68 |
let rec remove_link ltype = |
|
69 |
match (dynamic_type ltype).tdesc with |
|
70 |
| Tlink t -> t |
|
71 |
| _ -> ltype |
|
72 |
in |
|
73 |
match (dynamic_type (remove_link (get_type tab))).tdesc with |
|
74 |
| Tarray(size, t) -> remove_link t |
|
75 |
| Tvar -> Format.eprintf "Type of access is a variable... "; assert false |
|
76 |
| Tunivar -> Format.eprintf "Type of access is a variable... "; assert false |
|
77 |
| _ -> Format.eprintf "Type of access is not an array "; assert false |
|
78 |
end |
|
79 |
| Power(v, n) -> assert false |
|
80 |
| LocalVar v -> v.var_type |
|
81 |
| StateVar v -> v.var_type |
|
82 |
| Fun(n, vl) -> begin match n with |
|
83 |
| "+" |
|
84 |
| "-" |
|
85 |
| "*" -> get_type (List.hd vl) |
|
86 |
| _ -> Format.eprintf "Function undealt with : %s" n ;assert false |
|
87 |
end |
|
88 |
| Array(l) -> new_ty (Tarray(Dimension.mkdim_int |
|
89 |
(Location.dummy_loc) |
|
90 |
(List.length l), |
|
91 |
get_type (List.hd l))) |
|
92 |
| _ -> assert false |
|
93 |
*) |
|
94 |
|
|
95 |
(* Default value for each type, used when building arrays. Eg integer array |
|
96 |
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value |
|
97 |
for the type integer (arrays). |
|
98 |
*) |
|
99 |
let rec pp_default_val fmt t = |
|
100 |
match (dynamic_type t).tdesc with |
|
101 |
| Tint -> fprintf fmt "0" |
|
102 |
| Treal -> fprintf fmt "0" |
|
103 |
| Tbool -> fprintf fmt "true" |
|
104 |
| Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *) |
|
105 |
let valt = array_element_type t in |
|
106 |
fprintf fmt "((as const (Array Int %a)) %a)" |
|
107 |
pp_type valt |
|
108 |
pp_default_val valt |
|
109 |
| Tstruct(l) -> assert false |
|
110 |
| Ttuple(l) -> assert false |
|
111 |
|_ -> assert false |
|
112 |
|
|
113 |
|
|
49 | 114 |
(* Prints a value expression [v], with internal function calls only. |
50 | 115 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
51 | 116 |
but an offset suffix may be added for array variables |
52 | 117 |
*) |
53 | 118 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
54 | 119 |
match v.value_desc with |
55 |
| Cst c -> pp_horn_const fmt c |
|
56 |
| Array _ |
|
57 |
| Access _ -> assert false (* no arrays *) |
|
58 |
| Power (v, n) -> assert false |
|
59 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
|
60 |
| StateVar v -> |
|
61 |
if Types.is_array_type v.var_type |
|
62 |
then assert false |
|
63 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
64 |
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
|
120 |
| Cst c -> pp_horn_const fmt c |
|
121 |
|
|
122 |
(* Code specific for arrays *) |
|
123 |
| Array il -> |
|
124 |
(* An array definition: |
|
125 |
(store ( |
|
126 |
... |
|
127 |
(store ( |
|
128 |
store ( |
|
129 |
default_val |
|
130 |
) |
|
131 |
idx_n val_n |
|
132 |
) |
|
133 |
idx_n-1 val_n-1) |
|
134 |
... |
|
135 |
idx_1 val_1 |
|
136 |
) *) |
|
137 |
let rec print fmt (tab, x) = |
|
138 |
match tab with |
|
139 |
| [] -> pp_default_val fmt v.value_type(* (get_type v) *) |
|
140 |
| h::t -> |
|
141 |
fprintf fmt "(store %a %i %a)" |
|
142 |
print (t, (x+1)) |
|
143 |
x |
|
144 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) h |
|
145 |
in |
|
146 |
print fmt (il, 0) |
|
147 |
|
|
148 |
| Access(tab,index) -> |
|
149 |
fprintf fmt "(select %a %a)" |
|
150 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) tab |
|
151 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) index |
|
152 |
|
|
153 |
(* Code specific for arrays *) |
|
154 |
|
|
155 |
| Power (v, n) -> assert false |
|
156 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
|
157 |
| StateVar v -> |
|
158 |
if Types.is_array_type v.var_type |
|
159 |
then assert false |
|
160 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
161 |
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
|
65 | 162 |
|
66 | 163 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
67 | 164 |
let rec pp_value_suffix self pp_value fmt value = |
... | ... | |
79 | 176 |
*) |
80 | 177 |
let pp_assign m pp_var fmt var_name value = |
81 | 178 |
let self = m.mname.node_id in |
82 |
fprintf fmt "(= %a %a)"
|
|
179 |
fprintf fmt "(= %a %a)" |
|
83 | 180 |
(pp_horn_val ~is_lhs:true self pp_var) var_name |
84 | 181 |
(pp_value_suffix self pp_var) value |
85 |
|
|
182 |
|
|
86 | 183 |
|
87 | 184 |
(* In case of no reset call, we define mid_mem = current_mem *) |
88 | 185 |
let pp_no_reset machines m fmt i = |
89 | 186 |
let (n,_) = List.assoc i m.minstances in |
90 | 187 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
91 | 188 |
|
92 |
let m_list =
|
|
189 |
let m_list = |
|
93 | 190 |
rename_machine_list |
94 | 191 |
(concat m.mname.node_id i) |
95 | 192 |
(rename_mid_list (full_memory_vars machines target_machine)) |
... | ... | |
104 | 201 |
fprintf fmt "(= %a %a)" |
105 | 202 |
(pp_horn_var m) mhd |
106 | 203 |
(pp_horn_var m) chd |
107 |
|
|
204 |
|
|
108 | 205 |
| _ -> ( |
109 | 206 |
fprintf fmt "@[<v 0>(and @[<v 0>"; |
110 |
List.iter2 (fun mhd chd ->
|
|
207 |
List.iter2 (fun mhd chd -> |
|
111 | 208 |
fprintf fmt "(= %a %a)@ " |
112 | 209 |
(pp_horn_var m) mhd |
113 | 210 |
(pp_horn_var m) chd |
... | ... | |
120 | 217 |
let pp_instance_reset machines m fmt i = |
121 | 218 |
let (n,_) = List.assoc i m.minstances in |
122 | 219 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
123 |
|
|
220 |
|
|
124 | 221 |
fprintf fmt "(%a @[<v 0>%a)@]" |
125 | 222 |
pp_machine_reset_name (node_name n) |
126 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
223 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
127 | 224 |
( |
128 | 225 |
(rename_machine_list |
129 | 226 |
(concat m.mname.node_id i) |
130 | 227 |
(rename_current_list (full_memory_vars machines target_machine)) |
131 |
)
|
|
228 |
) |
|
132 | 229 |
@ |
133 | 230 |
(rename_machine_list |
134 | 231 |
(concat m.mname.node_id i) |
... | ... | |
146 | 243 |
if not (List.mem i reset_instances) then |
147 | 244 |
(* If not, declare mem_m = mem_c *) |
148 | 245 |
pp_no_reset machines m fmt i; |
149 |
|
|
246 |
|
|
150 | 247 |
let mems = full_memory_vars machines target_machine in |
151 | 248 |
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in |
152 | 249 |
let mid_mems = rename_mems rename_mid_list in |
... | ... | |
157 | 254 |
fprintf fmt "@[<v 5>(and "; |
158 | 255 |
fprintf fmt "(= %a (ite %a %a %a))" |
159 | 256 |
(pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *) |
160 |
(pp_horn_var m) mem_m
|
|
257 |
(pp_horn_var m) mem_m |
|
161 | 258 |
(pp_horn_val self (pp_horn_var m)) i1 |
162 | 259 |
(pp_horn_val self (pp_horn_var m)) i2 |
163 | 260 |
; |
... | ... | |
175 | 272 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs) |
176 | 273 |
(Utils.pp_final_char_if_non_empty "@ " outputs) |
177 | 274 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems) |
178 |
|
|
275 |
|
|
179 | 276 |
end |
180 | 277 |
end |
181 | 278 |
with Not_found -> ( (* stateless node instance *) |
... | ... | |
188 | 285 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
189 | 286 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs) |
190 | 287 |
) |
191 |
|
|
192 |
|
|
288 |
|
|
289 |
|
|
193 | 290 |
(* Print the instruction and update the set of reset instances *) |
194 | 291 |
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list = |
195 | 292 |
match instr with |
... | ... | |
230 | 327 |
statement. *) |
231 | 328 |
let self = m.mname.node_id in |
232 | 329 |
let pp_branch fmt (tag, instrs) = |
233 |
fprintf fmt
|
|
234 |
"@[<v 3>(or (not (= %a %s))@ "
|
|
330 |
fprintf fmt |
|
331 |
"@[<v 3>(or (not (= %a %s))@ " |
|
235 | 332 |
(*"@[<v 3>(=> (= %a %s)@ "*) (* Issues with some versions of Z3. It |
236 | 333 |
seems that => within Horn predicate |
237 | 334 |
may cause trouble. I have hard time |
... | ... | |
244 | 341 |
() (* rs *) |
245 | 342 |
in |
246 | 343 |
pp_conj pp_branch fmt hl; |
247 |
reset_instances
|
|
344 |
reset_instances |
|
248 | 345 |
|
249 |
and pp_machine_instrs machines reset_instances m fmt instrs =
|
|
346 |
and pp_machine_instrs machines reset_instances m fmt instrs = |
|
250 | 347 |
let ppi rs fmt i = pp_machine_instr machines rs m fmt i in |
251 | 348 |
match instrs with |
252 |
| [x] -> ppi reset_instances fmt x
|
|
349 |
| [x] -> ppi reset_instances fmt x |
|
253 | 350 |
| _::_ -> |
254 | 351 |
fprintf fmt "(and @[<v 0>"; |
255 |
let rs = List.fold_left (fun rs i ->
|
|
352 |
let rs = List.fold_left (fun rs i -> |
|
256 | 353 |
let rs = ppi rs fmt i in |
257 | 354 |
fprintf fmt "@ "; |
258 | 355 |
rs |
259 | 356 |
) |
260 |
reset_instances instrs
|
|
357 |
reset_instances instrs |
|
261 | 358 |
in |
262 | 359 |
fprintf fmt "@])"; |
263 | 360 |
rs |
... | ... | |
269 | 366 |
fprintf fmt "@[<v 5>(and @ "; |
270 | 367 |
|
271 | 368 |
(* print "x_m = x_c" for each local memory *) |
272 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v ->
|
|
369 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v -> |
|
273 | 370 |
fprintf fmt "(= %a %a)" |
274 | 371 |
(pp_horn_var m) (rename_mid v) |
275 | 372 |
(pp_horn_var m) (rename_current v) |
... | ... | |
281 | 378 |
*) |
282 | 379 |
(Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) -> |
283 | 380 |
let name = node_name n in |
284 |
if name = "_arrow" then (
|
|
381 |
if name = "_arrow" then ( |
|
285 | 382 |
fprintf fmt "(= %s._arrow._first_m true)" |
286 |
(concat m.mname.node_id id)
|
|
383 |
(concat m.mname.node_id id) |
|
287 | 384 |
) else ( |
288 |
let machine_n = get_machine machines name in
|
|
289 |
fprintf fmt "(%s_reset @[<hov 0>%a@])"
|
|
385 |
let machine_n = get_machine machines name in |
|
386 |
fprintf fmt "(%s_reset @[<hov 0>%a@])" |
|
290 | 387 |
name |
291 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
388 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
292 | 389 |
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) |
293 | 390 |
) |
294 | 391 |
)) fmt m.minstances; |
... | ... | |
314 | 411 |
else |
315 | 412 |
begin |
316 | 413 |
fprintf fmt "; %s@." m.mname.node_id; |
317 |
|
|
414 |
|
|
318 | 415 |
(* Printing variables *) |
319 | 416 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
320 | 417 |
( |
... | ... | |
358 | 455 |
|
359 | 456 |
(* Rule for reset *) |
360 | 457 |
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." |
361 |
(pp_machine_reset machines) m
|
|
458 |
(pp_machine_reset machines) m |
|
362 | 459 |
pp_machine_reset_name m.mname.node_id |
363 | 460 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m); |
364 | 461 |
|
... | ... | |
373 | 470 |
pp_machine_step_name m.mname.node_id |
374 | 471 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
375 | 472 |
end |
376 |
| assertsl ->
|
|
473 |
| assertsl -> |
|
377 | 474 |
begin |
378 | 475 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
379 | 476 |
(* print_string pp_val; *) |
380 | 477 |
fprintf fmt "; with Assertions @."; |
381 |
|
|
478 |
|
|
382 | 479 |
(*Rule for step*) |
383 | 480 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
384 | 481 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
... | ... | |
386 | 483 |
pp_machine_step_name m.mname.node_id |
387 | 484 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
388 | 485 |
end |
389 |
|
|
390 |
|
|
486 |
|
|
487 |
|
|
391 | 488 |
end |
392 | 489 |
end |
393 | 490 |
|
394 | 491 |
|
492 |
let mk_flags arity = |
|
493 |
let b_range = |
|
494 |
let rec range i j = |
|
495 |
if i > arity then [] else i :: (range (i+1) j) in |
|
496 |
range 2 arity; |
|
497 |
in |
|
498 |
List.fold_left (fun acc x -> acc ^ " false") "true" b_range |
|
499 |
|
|
500 |
|
|
501 |
(*Get sfunction infos from command line*) |
|
502 |
let get_sf_info() = |
|
503 |
let splitted = Str.split (Str.regexp "@") !Options.sfunction in |
|
504 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction); |
|
505 |
let sf_name, flags, arity = match splitted with |
|
506 |
[h;flg;par] -> h, flg, par |
|
507 |
| _ -> failwith "Wrong Sfunction info" |
|
508 |
|
|
509 |
in |
|
510 |
Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity); |
|
511 |
sf_name, flags, arity |
|
512 |
|
|
513 |
|
|
514 |
(*a function to print the rules in case we have an s-function*) |
|
515 |
let print_sfunction machines fmt m = |
|
516 |
if m.mname.node_id = arrow_id then |
|
517 |
(* We don't print arrow function *) |
|
518 |
() |
|
519 |
else |
|
520 |
begin |
|
521 |
Format.fprintf fmt "; SFUNCTION@."; |
|
522 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
|
523 |
Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction; |
|
524 |
|
|
525 |
(* Check if there is annotation for s-function *) |
|
526 |
if m.mannot != [] then( |
|
527 |
Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot; |
|
528 |
); |
|
529 |
|
|
530 |
(* Printing variables *) |
|
531 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
532 |
((step_vars machines m)@ |
|
533 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
|
534 |
Format.pp_print_newline fmt (); |
|
535 |
let sf_name, flags, arity = get_sf_info() in |
|
536 |
|
|
537 |
if is_stateless m then |
|
538 |
begin |
|
539 |
(* Declaring single predicate *) |
|
540 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
541 |
pp_machine_stateless_name m.mname.node_id |
|
542 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
543 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
|
544 |
Format.pp_print_newline fmt (); |
|
545 |
(* Rule for single predicate *) |
|
546 |
let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in |
|
547 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@." |
|
548 |
str_flags |
|
549 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m) |
|
550 |
pp_machine_stateless_name m.mname.node_id |
|
551 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m); |
|
552 |
end |
|
553 |
else |
|
554 |
begin |
|
555 |
(* Declaring predicate *) |
|
556 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
557 |
pp_machine_reset_name m.mname.node_id |
|
558 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
559 |
(List.map (fun v -> v.var_type) (inout_vars machines m)); |
|
560 |
|
|
561 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
562 |
pp_machine_step_name m.mname.node_id |
|
563 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
564 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
565 |
|
|
566 |
Format.pp_print_newline fmt (); |
|
567 |
(* Adding assertions *) |
|
568 |
match m.mstep.step_asserts with |
|
569 |
| [] -> |
|
570 |
begin |
|
571 |
|
|
572 |
(* Rule for step*) |
|
573 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
574 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
575 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
576 |
pp_machine_step_name m.mname.node_id |
|
577 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
|
578 |
end |
|
579 |
| assertsl -> |
|
580 |
begin |
|
581 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
|
582 |
(* print_string pp_val; *) |
|
583 |
fprintf fmt "; with Assertions @."; |
|
584 |
|
|
585 |
(*Rule for step*) |
|
586 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
587 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
588 |
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
589 |
pp_machine_step_name m.mname.node_id |
|
590 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
|
591 |
end |
|
592 |
|
|
593 |
end |
|
594 |
|
|
595 |
end |
|
395 | 596 |
(* Local Variables: *) |
396 | 597 |
(* compile-command:"make -C ../../.." *) |
397 | 598 |
(* End: *) |
src/backends/Horn/horn_backend_traces.ml | ||
---|---|---|
39 | 39 |
|
40 | 40 |
|
41 | 41 |
(* We extract the annotation dealing with traceability *) |
42 |
let machines_traces machines =
|
|
42 |
let machines_traces machines = |
|
43 | 43 |
List.map (fun m -> |
44 | 44 |
let traces : (ident * expr) list= |
45 | 45 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
... | ... | |
61 | 61 |
m, traces |
62 | 62 |
|
63 | 63 |
) machines |
64 |
|
|
64 |
|
|
65 | 65 |
let memories_old machines m = |
66 | 66 |
List.map (fun (p, v) -> |
67 | 67 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
68 | 68 |
let traces = List.assoc machine (machines_traces machines) in |
69 |
if List.mem_assoc v.var_id traces then
|
|
69 |
if List.mem_assoc v.var_id traces then |
|
70 | 70 |
( |
71 | 71 |
(* We take the expression associated to variable v in the trace |
72 | 72 |
info *) |
... | ... | |
75 | 75 |
Printers.pp_expr (List.assoc v.var_id traces); *) |
76 | 76 |
p, List.assoc v.var_id traces |
77 | 77 |
) |
78 |
else
|
|
78 |
else |
|
79 | 79 |
begin |
80 | 80 |
|
81 | 81 |
(* We keep the variable as is: we create an expression v *) |
82 | 82 |
|
83 | 83 |
(* eprintf "Unable to found variable %a in traces (%a)@." pp_var v |
84 | 84 |
(Utils.fprintf_list ~sep:", " pp_print_string) (List.map fst |
85 |
traces); *)
|
|
85 |
traces); *) |
|
86 | 86 |
|
87 | 87 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
88 | 88 |
end |
89 | 89 |
|
90 | 90 |
) (compute_mems machines m) |
91 |
|
|
91 |
|
|
92 | 92 |
let memories_next machines m = (* We remove the topest pre in each expression *) |
93 | 93 |
List.map |
94 | 94 |
(fun (prefix, ee) -> |
... | ... | |
102 | 102 |
Printers.pp_expr ee; |
103 | 103 |
assert false) |
104 | 104 |
(memories_old machines m) |
105 |
|
|
105 |
|
|
106 | 106 |
|
107 | 107 |
|
108 | 108 |
let pp_prefix_rev fmt prefix = |
109 |
Utils.fprintf_list ~sep:"."
|
|
110 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id)
|
|
111 |
fmt
|
|
109 |
Utils.fprintf_list ~sep:"." |
|
110 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) |
|
111 |
fmt |
|
112 | 112 |
(List.rev prefix) |
113 |
|
|
113 |
|
|
114 | 114 |
|
115 | 115 |
let traces_file fmt basename prog machines = |
116 | 116 |
fprintf fmt "<?xml version=\"1.0\"?>@."; |
... | ... | |
120 | 120 |
let pp_var = pp_horn_var m in |
121 | 121 |
let memories_old = memories_old machines m in |
122 | 122 |
let memories_next = memories_next machines m in |
123 |
|
|
123 |
|
|
124 | 124 |
(* fprintf fmt "; Node %s@." m.mname.node_id; *) |
125 | 125 |
fprintf fmt "@[<v 2><Node name=\"%s\">@ " m.mname.node_id; |
126 |
|
|
126 |
|
|
127 | 127 |
let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in |
128 | 128 |
let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in |
129 | 129 |
fprintf fmt "<input name=\"%a\" type=\"%a\">%a</input>@ " |
... | ... | |
135 | 135 |
(Utils.fprintf_list ~sep:" | " pp_var) output_vars |
136 | 136 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) output_vars |
137 | 137 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs); |
138 |
|
|
139 |
let init_local_vars =
|
|
140 |
|
|
141 |
(rename_next_list (try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false))
|
|
142 |
|
|
138 |
|
|
139 |
let init_local_vars = |
|
140 |
(rename_next_list |
|
141 |
(try full_memory_vars ~without_arrow:true machines m with Not_found -> Format.eprintf "mahine %s@.@?" m.mname.node_id; assert false))
|
|
142 |
|
|
143 | 143 |
|
144 | 144 |
in |
145 | 145 |
let step_local_vars = (rename_current_list (full_memory_vars ~without_arrow:true machines m)) in |
... | ... | |
160 | 160 |
fprintf fmt "@]@ </Node>"; |
161 | 161 |
)) (List.rev machines); |
162 | 162 |
fprintf fmt "</Traces>@." |
163 |
|
|
163 |
|
|
164 | 164 |
|
165 | 165 |
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt |
166 | 166 |
"%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *) |
src/compiler_common.ml | ||
---|---|---|
10 | 10 |
(********************************************************************) |
11 | 11 |
|
12 | 12 |
open Utils |
13 |
open Format
|
|
13 |
open Format |
|
14 | 14 |
open LustreSpec |
15 | 15 |
open Corelang |
16 | 16 |
|
... | ... | |
50 | 50 |
close_in h_in; |
51 | 51 |
header |
52 | 52 |
with |
53 |
| (Parse.Error err) as exc ->
|
|
53 |
| (Parse.Error err) as exc -> |
|
54 | 54 |
Parse.report_error err; |
55 | 55 |
raise exc |
56 | 56 |
| Corelang.Error (loc, err) as exc -> ( |
... | ... | |
68 | 68 |
Location.init lexbuf source_name; |
69 | 69 |
|
70 | 70 |
(* Parsing *) |
71 |
Log.report ~level:1
|
|
71 |
Log.report ~level:1 |
|
72 | 72 |
(fun fmt -> fprintf fmt ".. parsing source file %s@," source_name); |
73 | 73 |
try |
74 | 74 |
let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in |
... | ... | |
76 | 76 |
close_in s_in; |
77 | 77 |
prog |
78 | 78 |
with |
79 |
| (Parse.Error err) as exc ->
|
|
79 |
| (Parse.Error err) as exc -> |
|
80 | 80 |
Parse.report_error err; |
81 | 81 |
raise exc |
82 | 82 |
| Corelang.Error (loc, err) as exc -> |
... | ... | |
115 | 115 |
Location.pp_loc loc; |
116 | 116 |
raise exc |
117 | 117 |
|
118 |
let type_decls env decls =
|
|
118 |
let type_decls env decls = |
|
119 | 119 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ "); |
120 |
let new_env =
|
|
120 |
let new_env = |
|
121 | 121 |
begin |
122 | 122 |
try |
123 | 123 |
Typing.type_prog env decls |
... | ... | |
126 | 126 |
Types.pp_error err |
127 | 127 |
Location.pp_loc loc; |
128 | 128 |
raise exc |
129 |
end
|
|
129 |
end |
|
130 | 130 |
in |
131 | 131 |
if !Options.print_types then |
132 | 132 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_type decls); |
133 | 133 |
new_env |
134 |
|
|
135 |
let clock_decls env decls =
|
|
134 |
|
|
135 |
let clock_decls env decls = |
|
136 | 136 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@ "); |
137 | 137 |
let new_env = |
138 | 138 |
begin |
... | ... | |
221 | 221 |
let is_stateful topdecl = |
222 | 222 |
match topdecl.top_decl_desc with |
223 | 223 |
| Node nd -> (match nd.node_stateless with Some b -> not b | None -> not nd.node_dec_stateless) |
224 |
| ImportedNode nd -> not nd.nodei_stateless
|
|
224 |
| ImportedNode nd -> not nd.nodei_stateless |
|
225 | 225 |
| _ -> false |
226 | 226 |
|
227 | 227 |
|
... | ... | |
248 | 248 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ "); |
249 | 249 |
deps |
250 | 250 |
end |
251 |
|
src/corelang.ml | ||
---|---|---|
241 | 241 |
|
242 | 242 |
(* alias and type definition table *) |
243 | 243 |
|
244 |
let mktop = mktop_decl Location.dummy_loc Version.include_path false |
|
244 |
(*let mktop = mktop_decl Location.dummy_loc Version.include_path false *) |
|
245 |
|
|
246 |
let mktop = mktop_decl Location.dummy_loc !Options.include_dir false |
|
245 | 247 |
|
246 | 248 |
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int}) |
247 | 249 |
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool}) |
src/lexerLustreSpec.mll | ||
---|---|---|
66 | 66 |
"assumes", ASSUMES; |
67 | 67 |
"exists", EXISTS; |
68 | 68 |
"forall", FORALL; |
69 |
"c_code", CCODE; |
|
70 |
"matlab", MATLAB; |
|
69 | 71 |
] |
70 | 72 |
|
71 | 73 |
} |
src/lexer_lustre.mll | ||
---|---|---|
63 | 63 |
"assert", ASSERT; |
64 | 64 |
"lib", LIB; |
65 | 65 |
"prototype", PROTOTYPE; |
66 |
"c_code", CCODE; |
|
67 |
"matlab", MATLAB; |
|
66 | 68 |
] |
67 | 69 |
|
68 | 70 |
|
src/machine_code.ml | ||
---|---|---|
161 | 161 |
node_spec = None; |
162 | 162 |
node_annot = []; } |
163 | 163 |
|
164 |
let arrow_top_decl = |
|
164 |
(*let arrow_top_decl =
|
|
165 | 165 |
{ |
166 | 166 |
top_decl_desc = Node arrow_desc; |
167 | 167 |
top_decl_owner = Version.include_path; |
168 | 168 |
top_decl_itf = false; |
169 | 169 |
top_decl_loc = Location.dummy_loc |
170 |
}*) |
|
171 |
|
|
172 |
let arrow_top_decl = |
|
173 |
{ |
|
174 |
top_decl_desc = Node arrow_desc; |
|
175 |
top_decl_owner = !Options.include_dir; |
|
176 |
top_decl_itf = false; |
|
177 |
top_decl_loc = Location.dummy_loc |
|
170 | 178 |
} |
171 | 179 |
|
180 |
|
|
172 | 181 |
let mk_val v t = { value_desc = v; |
173 | 182 |
value_type = t; |
174 | 183 |
value_annot = None } |
src/main_lustre_compiler.ml | ||
---|---|---|
15 | 15 |
open Utils |
16 | 16 |
open LustreSpec |
17 | 17 |
open Compiler_common |
18 |
|
|
18 |
|
|
19 | 19 |
exception StopPhase1 of program |
20 | 20 |
|
21 | 21 |
let usage = "Usage: lustrec [options] \x1b[4msource file\x1b[0m" |
... | ... | |
88 | 88 |
end |
89 | 89 |
|
90 | 90 |
|
91 |
let functional_backend () =
|
|
91 |
let functional_backend () = |
|
92 | 92 |
match !Options.output with |
93 | 93 |
| "horn" | "lustre" | "acsl" -> true |
94 | 94 |
| _ -> false |
95 | 95 |
|
96 | 96 |
(* From prog to prog *) |
97 | 97 |
let stage1 prog dirname basename = |
98 |
(* Removing automata *)
|
|
98 |
(* Removing automata *) |
|
99 | 99 |
let prog = expand_automata prog in |
100 | 100 |
|
101 | 101 |
Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog); |
... | ... | |
137 | 137 |
exported as a lusi *) |
138 | 138 |
raise (StopPhase1 prog); |
139 | 139 |
|
140 |
(* Optimization of prog:
|
|
141 |
- Unfold consts
|
|
140 |
(* Optimization of prog: |
|
141 |
- Unfold consts |
|
142 | 142 |
- eliminate trivial expressions |
143 | 143 |
*) |
144 | 144 |
(* |
145 |
let prog =
|
|
145 |
let prog = |
|
146 | 146 |
if !Options.const_unfold || !Options.optimization >= 5 then |
147 | 147 |
begin |
148 | 148 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,"); |
Also available in: Unified diff