Revision b38ffff3
AUTHORS | ||
---|---|---|
1 |
Pierre-Loïc Garoche - ONERA |
|
2 |
Xavier Thirioux - ENSEEIHT/INPT |
|
1 |
Pierre-Loïc Garoche - ONERA, France |
|
2 |
Xavier Thirioux - ENSEEIHT/INPT, France |
|
3 |
|
|
4 |
Inital Typing/Clocking by Julien Forget - LIFL, France |
_tags | ||
---|---|---|
1 | 1 |
"src": include |
2 | 2 |
"src/backends/C": include |
3 |
"src/backends/Horn": include |
|
3 | 4 |
# OASIS_START |
4 | 5 |
# DO NOT EDIT (digest: df9189c6c6943133cb99a2bb11ba7f05) |
5 | 6 |
# Ignore VCS directories, you can use the same kind of rule outside |
doc/lustre_spec.org | ||
---|---|---|
1 | 1 |
Lustre annotation/specification language |
2 |
#+AUTHORS: Pierre-Loic Garoche, Rémi Delmas, Temesghen Kahsai |
|
2 | 3 |
#+LATEX_HEADER: \usepackage{tikz,listings,stmaryrd,pgfplots,mathrsfs,syntax} |
3 | 4 |
#+LATEX_HEADER: \input{lustre_lst} |
4 | 5 |
|
src/Print.ml | ||
---|---|---|
1 |
(* |
|
2 |
* Copyright (c) 2009 CNRS & Université Bordeaux 1. |
|
3 |
* |
|
4 |
* Author(s): Grégoire Sutre <gregoire.sutre@labri.fr>, |
|
5 |
* modified by Julien Forget <julien.forget@lifl.fr> |
|
6 |
* |
|
7 |
* Permission to use, copy, modify, and distribute this software for any |
|
8 |
* purpose with or without fee is hereby granted, provided that the above |
|
9 |
* copyright notice and this permission notice appear in all copies. |
|
10 |
* |
|
11 |
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES |
|
12 |
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF |
|
13 |
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR |
|
14 |
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES |
|
15 |
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN |
|
16 |
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF |
|
17 |
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. |
|
18 |
*) |
|
19 |
|
|
20 |
|
|
21 |
(* |
|
22 |
* Signatures and helper functions for pretty-printing. |
|
23 |
*) |
|
24 |
|
|
25 |
|
|
26 |
module type PRINTABLE_TYPE = |
|
27 |
sig |
|
28 |
type t |
|
29 |
val print : Format.formatter -> t -> unit |
|
30 |
end |
|
31 |
|
|
32 |
|
|
33 |
let string_converter_from_printer printer = |
|
34 |
function data -> |
|
35 |
Format.fprintf Format.str_formatter "@[%a@]" printer data ; |
|
36 |
Format.flush_str_formatter () |
|
37 |
|
|
38 |
let hashtbl_printer_from_printer beg_f sep_f end_f printer fmt hashtbl = |
|
39 |
let length = Hashtbl.length hashtbl in |
|
40 |
if length > 0 then |
|
41 |
begin |
|
42 |
Format.fprintf fmt beg_f; |
|
43 |
ignore( |
|
44 |
Hashtbl.fold |
|
45 |
(fun k v cpt -> |
|
46 |
if cpt < length then |
|
47 |
begin |
|
48 |
Format.fprintf fmt "@[%a@]" printer (k,v); |
|
49 |
Format.fprintf fmt sep_f; |
|
50 |
cpt+1 |
|
51 |
end |
|
52 |
else |
|
53 |
begin |
|
54 |
Format.fprintf fmt "@[%a@]" printer (k,v); |
|
55 |
Format.fprintf fmt end_f; |
|
56 |
cpt+1 |
|
57 |
end) |
|
58 |
hashtbl 1) |
|
59 |
end |
|
60 |
|
|
61 |
let list_printer_from_printer beg_f sep_f end_f printer fmt list = |
|
62 |
match list with |
|
63 |
[] -> () |
|
64 |
| head::tail -> |
|
65 |
Format.fprintf fmt beg_f; |
|
66 |
Format.fprintf fmt "@[%a@]" printer head; |
|
67 |
List.iter |
|
68 |
(function data -> |
|
69 |
begin |
|
70 |
Format.fprintf fmt sep_f; |
|
71 |
Format.fprintf fmt "@[%a@]" printer data |
|
72 |
end) |
|
73 |
tail; |
|
74 |
Format.fprintf fmt end_f |
|
75 |
|
|
76 |
let array_printer_from_printer beg_f sep_f end_f printer fmt array = |
|
77 |
if (Array.length array) > 0 then |
|
78 |
let n = Array.length array |
|
79 |
in |
|
80 |
Format.fprintf fmt beg_f; |
|
81 |
for i = 0 to n - 2 do |
|
82 |
Format.fprintf fmt "@[%a@]" printer (i, array.(i)) ; |
|
83 |
Format.fprintf fmt sep_f |
|
84 |
done ; |
|
85 |
Format.fprintf fmt "@[%a@]" printer (n-1, array.(n-1)); |
|
86 |
Format.fprintf fmt end_f |
|
87 |
|
|
88 |
(* Local Variables: *) |
|
89 |
(* compile-command:"make -C .." *) |
|
90 |
(* End: *) |
src/Print.mli | ||
---|---|---|
1 |
(* $Id$ *) |
|
2 |
|
|
3 |
(* |
|
4 |
* Copyright (c) 2009 CNRS & Université Bordeaux 1. |
|
5 |
* |
|
6 |
* Author(s): Grégoire Sutre <gregoire.sutre@labri.fr> |
|
7 |
* |
|
8 |
* Permission to use, copy, modify, and distribute this software for any |
|
9 |
* purpose with or without fee is hereby granted, provided that the above |
|
10 |
* copyright notice and this permission notice appear in all copies. |
|
11 |
* |
|
12 |
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES |
|
13 |
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF |
|
14 |
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR |
|
15 |
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES |
|
16 |
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN |
|
17 |
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF |
|
18 |
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. |
|
19 |
*) |
|
20 |
|
|
21 |
|
|
22 |
(** |
|
23 |
Signatures and helper functions for pretty-printing. |
|
24 |
|
|
25 |
This module follows the standard OCaml pretty-printing facility provided in |
|
26 |
the module [Format] of the standard library. In particular, pretty-printing |
|
27 |
commands assume that there is an opened pretty-printing box. This permits |
|
28 |
more flexibility, since the choice of the enclosing pretty-printing box may |
|
29 |
depend on the context. |
|
30 |
|
|
31 |
@see <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Format.html> Format |
|
32 |
*) |
|
33 |
|
|
34 |
|
|
35 |
(** Signature for a type equipped with a pretty-printing function. *) |
|
36 |
module type PRINTABLE_TYPE = |
|
37 |
sig |
|
38 |
(** The type. *) |
|
39 |
type t |
|
40 |
|
|
41 |
(** A pretty-printer for this type. This function prints values of |
|
42 |
type [t] in the current pretty-printing box. *) val print : |
|
43 |
Format.formatter -> t -> unit end |
|
44 |
|
|
45 |
|
|
46 |
(** Transform a pretty-printer into a string converter. *) |
|
47 |
val string_converter_from_printer : |
|
48 |
(Format.formatter -> 'a -> unit) -> 'a -> string |
|
49 |
|
|
50 |
(** [hashtbl_printer_from_printer beg sep endf printer] returns a |
|
51 |
pretty-printer for hashtbls of type [('a,'b) Hashtbl.t], given a three formatters |
|
52 |
[beg], [sep] and [endf], and a pretty-printer [printer] for values of |
|
53 |
type [('a,'b)]. The resulting pretty-printer first prints [beg], then each |
|
54 |
element of its argument list with [sep] between each element, and |
|
55 |
finally prints [endf]. Each element in the hashtbl is printed in a new |
|
56 |
enclosing pretty-printing box. In other words, |
|
57 |
[hashtbl_printer_from_printer sep printer fmt [{k1|->v1; ...; kn|->vn}]] is |
|
58 |
equivalent to [ |
|
59 |
begin |
|
60 |
Format.fprintf fmt beg; |
|
61 |
Format.fprintf fmt "@[%a@]" printer (k1,v1) ; |
|
62 |
Format.fprintf fmt sep ; |
|
63 |
... ; |
|
64 |
Format.fprintf fmt sep ; |
|
65 |
Format.fprintf fmt "@[%a@]" printer (kn,vn); |
|
66 |
Format.fprintf fmt endf; |
|
67 |
end |
|
68 |
]. Note that the separator [sep] may contain pretty-printing commands. For |
|
69 |
instance [";@ "] could be used as a separator argument to this function. |
|
70 |
*) |
|
71 |
val hashtbl_printer_from_printer : |
|
72 |
(unit, Format.formatter, unit) format -> |
|
73 |
(unit, Format.formatter, unit) format -> |
|
74 |
(unit, Format.formatter, unit) format -> |
|
75 |
(Format.formatter -> ('a*'b) -> unit) -> |
|
76 |
Format.formatter -> ('a,'b) Hashtbl.t -> unit |
|
77 |
|
|
78 |
(** [list_printer_from_printer beg sep endf printer] returns a |
|
79 |
pretty-printer for lists of type ['a list], given three formatters |
|
80 |
[beg], [sep] and [endf], and a pretty-printer [printer] for values of |
|
81 |
type ['a]. The resulting pretty-printer first prints [beg], then each |
|
82 |
element of its argument list with [sep] between each element, and |
|
83 |
finally prints [endf]. Each element in the list is printed in a new |
|
84 |
enclosing pretty-printing box. In other words, |
|
85 |
[list_printer_from_printer beg sep endf printer fmt [a1; ...; aN]] is |
|
86 |
equivalent to [ |
|
87 |
begin |
|
88 |
Format.fprintf fmt beg; |
|
89 |
Format.fprintf fmt "@[%a@]" printer a1 ; |
|
90 |
Format.fprintf fmt sep ; |
|
91 |
... ; |
|
92 |
Format.fprintf fmt sep ; |
|
93 |
Format.fprintf fmt "@[%a@]" printer aN |
|
94 |
Format.fprintf fmt endf; |
|
95 |
end |
|
96 |
]. Note that the separator [sep] may contain pretty-printing commands. For |
|
97 |
instance [";@ "] could be used as a separator argument to this function. |
|
98 |
*) |
|
99 |
val list_printer_from_printer : |
|
100 |
(unit, Format.formatter, unit) format -> |
|
101 |
(unit, Format.formatter, unit) format -> |
|
102 |
(unit, Format.formatter, unit) format -> |
|
103 |
(Format.formatter -> 'a -> unit) -> |
|
104 |
Format.formatter -> 'a list -> unit |
|
105 |
|
|
106 |
(** [array_printer_from_printer sep printer] returns a pretty-printer |
|
107 |
for arrays of type ['a array], given three formatters [beg], [sep] and |
|
108 |
[endf], and a pretty-printer [printer] for values of type [int * 'a]. |
|
109 |
The resulting pretty-printer first prints [beg], then prints each pair |
|
110 |
[(i, a.(i))] of its argument array [a] and prints [sep] between each |
|
111 |
pair and finally prints [endf]. Each pair in the array is printed in |
|
112 |
a new enclosing pretty-printing box. In other words, |
|
113 |
[array_printer_from_printer beg sep end printer fmt [|a1; ...; aN|]] is |
|
114 |
equivalent to [ |
|
115 |
begin |
|
116 |
Format.fprintf fmt beg; |
|
117 |
Format.fprintf fmt "@[%a@]" printer (0, a1) ; |
|
118 |
Format.fprintf fmt sep ; |
|
119 |
... ; |
|
120 |
Format.fprintf fmt sep ; |
|
121 |
Format.fprintf fmt "@[%a@]" printer (N-1, aN) |
|
122 |
Format.fprintf fmt endf; |
|
123 |
end |
|
124 |
]. Note that the separator [sep] may contain pretty-printing commands. |
|
125 |
For instance [";@ "] could be used as a separator argument to this function. |
|
126 |
*) |
|
127 |
val |
|
128 |
array_printer_from_printer : (unit, Format.formatter, unit) format -> |
|
129 |
(unit, Format.formatter, unit) format -> (unit, Format.formatter, |
|
130 |
unit) format -> (Format.formatter -> (int * 'a) -> unit) -> |
|
131 |
Format.formatter -> 'a array -> unit |
src/access.ml | ||
---|---|---|
1 |
(* ---------------------------------------------------------------------------- |
|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
|
3 |
* Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
|
4 |
* |
|
5 |
* This file is part of Prelude |
|
6 |
* |
|
7 |
* Prelude is free software; you can redistribute it and/or |
|
8 |
* modify it under the terms of the GNU Lesser General Public License |
|
9 |
* as published by the Free Software Foundation ; either version 2 of |
|
10 |
* the License, or (at your option) any later version. |
|
11 |
* |
|
12 |
* Prelude is distributed in the hope that it will be useful, but |
|
13 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
|
14 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
|
15 |
* Lesser General Public License for more details. |
|
16 |
* |
|
17 |
* You should have received a copy of the GNU Lesser General Public |
|
18 |
* License along with this program ; if not, write to the Free Software |
|
19 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
|
20 |
* USA |
|
21 |
*---------------------------------------------------------------------------- *) |
|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
22 | 11 |
|
23 | 12 |
(** Access checking module. Done after typing. Generates dimension constraints stored in nodes *) |
24 | 13 |
|
src/backends/C/c_backend.ml | ||
---|---|---|
1 |
(* ---------------------------------------------------------------------------- |
|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
|
3 |
* Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
|
4 |
* Copyright (C) 2012-2013, INPT, Toulouse, FRANCE |
|
5 |
* |
|
6 |
* This file is part of Prelude |
|
7 |
* |
|
8 |
* Prelude is free software; you can redistribute it and/or |
|
9 |
* modify it under the terms of the GNU Lesser General Public License |
|
10 |
* as published by the Free Software Foundation ; either version 2 of |
|
11 |
* the License, or (at your option) any later version. |
|
12 |
* |
|
13 |
* Prelude is distributed in the hope that it will be useful, but |
|
14 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
|
15 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
|
16 |
* Lesser General Public License for more details. |
|
17 |
* |
|
18 |
* You should have received a copy of the GNU Lesser General Public |
|
19 |
* License along with this program ; if not, write to the Free Software |
|
20 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
|
21 |
* USA |
|
22 |
*---------------------------------------------------------------------------- *) |
|
23 |
|
|
24 |
(* This module is used for the lustre to C compiler *) |
|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
25 | 11 |
|
26 | 12 |
open Format |
27 | 13 |
(********************************************************************************************) |
src/backends/C/c_backend_common.ml | ||
---|---|---|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
1 | 12 |
open Format |
2 | 13 |
open LustreSpec |
3 | 14 |
open Corelang |
src/backends/C/c_backend_header.ml | ||
---|---|---|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
1 | 12 |
open Format |
2 | 13 |
open LustreSpec |
3 | 14 |
open Corelang |
src/backends/C/c_backend_main.ml | ||
---|---|---|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
1 | 12 |
open LustreSpec |
2 | 13 |
open Corelang |
3 | 14 |
open Machine_code |
src/backends/C/c_backend_makefile.ml | ||
---|---|---|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
1 | 12 |
open Format |
2 | 13 |
open LustreSpec |
3 | 14 |
open Corelang |
src/backends/C/c_backend_spec.ml | ||
---|---|---|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
1 | 12 |
open Format |
2 | 13 |
open LustreSpec |
3 | 14 |
open Machine_code |
src/backends/C/c_backend_src.ml | ||
---|---|---|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
1 | 12 |
open Format |
2 | 13 |
open LustreSpec |
3 | 14 |
open Corelang |
src/backends/Horn/horn_backend.ml | ||
---|---|---|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
12 |
(* The compilation presented here is defined in Garoche, Gurfinkel, Kahsai, |
|
13 |
HCSV'14 *) |
|
14 |
|
|
15 |
open Format |
|
16 |
open LustreSpec |
|
17 |
open Corelang |
|
18 |
open Machine_code |
|
19 |
|
|
20 |
|
|
21 |
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id |
|
22 |
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id |
|
23 |
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id |
|
24 |
|
|
25 |
let pp_type fmt t = |
|
26 |
match (Types.repr t).Types.tdesc with |
|
27 |
| Types.Tbool -> Format.fprintf fmt "Bool" |
|
28 |
| Types.Tint -> Format.fprintf fmt "Int" |
|
29 |
| Types.Treal -> Format.fprintf fmt "Real" |
|
30 |
| Types.Tclock _ |
|
31 |
| Types.Tarray _ |
|
32 |
| Types.Tstatic _ |
|
33 |
| Types.Tconst _ |
|
34 |
| Types.Tarrow _ |
|
35 |
| _ -> Format.eprintf "internal error: pp_type %a@." |
|
36 |
Types.print_ty t; assert false |
|
37 |
|
|
38 |
let pp_decl_var fmt id = |
|
39 |
Format.fprintf fmt "(declare-var %s %a)" |
|
40 |
id.var_id |
|
41 |
pp_type id.var_type |
|
42 |
|
|
43 |
let pp_var fmt id = Format.pp_print_string fmt id.var_id |
|
44 |
|
|
45 |
|
|
46 |
let pp_conj pp fmt l = |
|
47 |
match l with |
|
48 |
[] -> assert false |
|
49 |
| [x] -> pp fmt x |
|
50 |
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l |
|
51 |
|
|
52 |
|
|
53 |
|
|
54 |
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x |
|
55 |
let rename f = (fun v -> {v with var_id = f v.var_id } ) |
|
56 |
let rename_machine p = rename (fun n -> concat p n) |
|
57 |
let rename_machine_list p = List.map (rename_machine p) |
|
58 |
|
|
59 |
let rename_current = rename (fun n -> n ^ "_c") |
|
60 |
let rename_current_list = List.map rename_current |
|
61 |
let rename_next = rename (fun n -> n ^ "_x") |
|
62 |
let rename_next_list = List.map rename_next |
|
63 |
|
|
64 |
|
|
65 |
let get_machine machines node_name = |
|
66 |
List.find (fun m -> m.mname.node_id = node_name) machines |
|
67 |
|
|
68 |
let full_memory_vars machines machine = |
|
69 |
let rec aux fst prefix m = |
|
70 |
(rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @ |
|
71 |
List.fold_left (fun accu (id, (n, _)) -> |
|
72 |
let name = node_name n in |
|
73 |
if name = "_arrow" then accu else |
|
74 |
let machine_n = get_machine machines name in |
|
75 |
( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu |
|
76 |
) [] (m.minstances) |
|
77 |
in |
|
78 |
aux true machine.mname.node_id machine |
|
79 |
|
|
80 |
let stateless_vars machines m = |
|
81 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
|
82 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs) |
|
83 |
|
|
84 |
let step_vars machines m = |
|
85 |
(stateless_vars machines m)@ |
|
86 |
(rename_current_list (full_memory_vars machines m)) @ |
|
87 |
(rename_next_list (full_memory_vars machines m)) |
|
88 |
|
|
89 |
let init_vars machines m = |
|
90 |
(stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m)) |
|
91 |
|
|
92 |
(********************************************************************************************) |
|
93 |
(* Instruction Printing functions *) |
|
94 |
(********************************************************************************************) |
|
95 |
|
|
96 |
let pp_horn_var m fmt id = |
|
97 |
if Types.is_array_type id.var_type |
|
98 |
then |
|
99 |
assert false (* no arrays in Horn output *) |
|
100 |
else |
|
101 |
Format.fprintf fmt "%s" id.var_id |
|
102 |
|
|
103 |
|
|
104 |
(* Used to print boolean constants *) |
|
105 |
let pp_horn_tag fmt t = |
|
106 |
pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t) |
|
107 |
|
|
108 |
(* Prints a constant value *) |
|
109 |
let rec pp_horn_const fmt c = |
|
110 |
match c with |
|
111 |
| Const_int i -> pp_print_int fmt i |
|
112 |
| Const_real r -> pp_print_string fmt r |
|
113 |
| Const_float r -> pp_print_float fmt r |
|
114 |
| Const_tag t -> pp_horn_tag fmt t |
|
115 |
| _ -> assert false |
|
116 |
|
|
117 |
(* Prints a value expression [v], with internal function calls only. |
|
118 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
|
119 |
but an offset suffix may be added for array variables |
|
120 |
*) |
|
121 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
|
122 |
match v with |
|
123 |
| Cst c -> pp_horn_const fmt c |
|
124 |
| Array _ |
|
125 |
| Access _ -> assert false (* no arrays *) |
|
126 |
| Power (v, n) -> assert false |
|
127 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
|
128 |
| StateVar v -> |
|
129 |
if Types.is_array_type v.var_type |
|
130 |
then assert false |
|
131 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
132 |
| Fun (n, vl) -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
|
133 |
|
|
134 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
|
135 |
let rec pp_value_suffix self pp_value fmt value = |
|
136 |
match value with |
|
137 |
| Fun (n, vl) -> |
|
138 |
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl |
|
139 |
| _ -> |
|
140 |
pp_horn_val self pp_value fmt value |
|
141 |
|
|
142 |
(* type_directed assignment: array vs. statically sized type |
|
143 |
- [var_type]: type of variable to be assigned |
|
144 |
- [var_name]: name of variable to be assigned |
|
145 |
- [value]: assigned value |
|
146 |
- [pp_var]: printer for variables |
|
147 |
*) |
|
148 |
let pp_assign m self pp_var fmt var_type var_name value = |
|
149 |
fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value |
|
150 |
|
|
151 |
let pp_instance_call |
|
152 |
machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) = |
|
153 |
try (* stateful node instance *) |
|
154 |
begin |
|
155 |
let (n,_) = List.assoc i m.minstances in |
|
156 |
match node_name n, inputs, outputs with |
|
157 |
| "_arrow", [i1; i2], [o] -> begin |
|
158 |
if init then |
|
159 |
pp_assign |
|
160 |
m |
|
161 |
self |
|
162 |
(pp_horn_var m) |
|
163 |
fmt |
|
164 |
o.var_type (LocalVar o) i1 |
|
165 |
else |
|
166 |
pp_assign |
|
167 |
m self (pp_horn_var m) fmt |
|
168 |
o.var_type (LocalVar o) i2 |
|
169 |
|
|
170 |
end |
|
171 |
| name, _, _ -> |
|
172 |
begin |
|
173 |
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in |
|
174 |
if init then |
|
175 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
|
176 |
pp_machine_init_name (node_name n) |
|
177 |
(* inputs *) |
|
178 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
179 |
inputs |
|
180 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
181 |
(* outputs *) |
|
182 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
183 |
(List.map (fun v -> LocalVar v) outputs) |
|
184 |
(Utils.pp_final_char_if_non_empty " " outputs) |
|
185 |
(* memories (next) *) |
|
186 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
|
187 |
rename_machine_list |
|
188 |
(concat m.mname.node_id i) |
|
189 |
(rename_next_list (full_memory_vars machines target_machine) |
|
190 |
) |
|
191 |
) |
|
192 |
else |
|
193 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
|
194 |
pp_machine_step_name (node_name n) |
|
195 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
|
196 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
197 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
198 |
(List.map (fun v -> LocalVar v) outputs) |
|
199 |
(Utils.pp_final_char_if_non_empty " " outputs) |
|
200 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
|
201 |
(rename_machine_list |
|
202 |
(concat m.mname.node_id i) |
|
203 |
(rename_current_list (full_memory_vars machines target_machine)) |
|
204 |
) @ |
|
205 |
(rename_machine_list |
|
206 |
(concat m.mname.node_id i) |
|
207 |
(rename_next_list (full_memory_vars machines target_machine)) |
|
208 |
) |
|
209 |
) |
|
210 |
|
|
211 |
end |
|
212 |
end |
|
213 |
with Not_found -> ( (* stateless node instance *) |
|
214 |
let (n,_) = List.assoc i m.mcalls in |
|
215 |
Format.fprintf fmt "(%s %a%t%a)" |
|
216 |
(node_name n) |
|
217 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
218 |
inputs |
|
219 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
220 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
221 |
(List.map (fun v -> LocalVar v) outputs) |
|
222 |
) |
|
223 |
|
|
224 |
let pp_machine_init (m: machine_t) self fmt inst = |
|
225 |
let (node, static) = List.assoc inst m.minstances in |
|
226 |
fprintf fmt "(%a %a%t%s->%s)" |
|
227 |
pp_machine_init_name (node_name node) |
|
228 |
(Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static |
|
229 |
(Utils.pp_final_char_if_non_empty " " static) |
|
230 |
self inst |
|
231 |
|
|
232 |
(* TODO *) |
|
233 |
let rec pp_conditional machines ?(init=false) (m: machine_t) self fmt c tl el = |
|
234 |
fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}" |
|
235 |
(pp_horn_val self (pp_horn_var m)) c |
|
236 |
(Utils.pp_newline_if_non_empty tl) |
|
237 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) tl |
|
238 |
(Utils.pp_newline_if_non_empty el) |
|
239 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) el |
|
240 |
|
|
241 |
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr = |
|
242 |
match instr with |
|
243 |
| MReset i -> |
|
244 |
pp_machine_init m self fmt i |
|
245 |
| MLocalAssign (i,v) -> |
|
246 |
pp_assign |
|
247 |
m self (pp_horn_var m) fmt |
|
248 |
i.var_type (LocalVar i) v |
|
249 |
| MStateAssign (i,v) -> |
|
250 |
pp_assign |
|
251 |
m self (pp_horn_var m) fmt |
|
252 |
i.var_type (StateVar i) v |
|
253 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
|
254 |
assert false (* This should not happen anymore *) |
|
255 |
| MStep (il, i, vl) -> |
|
256 |
pp_instance_call machines ~init:init m self fmt i vl il |
|
257 |
| MBranch (g,hl) -> |
|
258 |
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false |
|
259 |
then (* boolean case, needs special treatment in C because truth value is not unique *) |
|
260 |
(* may disappear if we optimize code by replacing last branch test with default *) |
|
261 |
let tl = try List.assoc tag_true hl with Not_found -> [] in |
|
262 |
let el = try List.assoc tag_false hl with Not_found -> [] in |
|
263 |
pp_conditional machines ~init:init m self fmt g tl el |
|
264 |
else assert false (* enum type case *) |
|
265 |
|
|
266 |
|
|
267 |
(**************************************************************) |
|
268 |
|
|
269 |
let is_stateless m = m.minstances = [] && m.mmemory = [] |
|
270 |
|
|
271 |
(* Print the machine m: |
|
272 |
two functions: m_init and m_step |
|
273 |
- m_init is a predicate over m memories |
|
274 |
- m_step is a predicate over old_memories, inputs, new_memories, outputs |
|
275 |
We first declare all variables then the two /rules/. |
|
276 |
*) |
|
277 |
let print_machine machines fmt m = |
|
278 |
let pp_instr init = pp_machine_instr machines ~init:init m in |
|
279 |
if m.mname.node_id = arrow_id then |
|
280 |
(* We don't print arrow function *) |
|
281 |
() |
|
282 |
else |
|
283 |
begin |
|
284 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
|
285 |
|
|
286 |
(* Printing variables *) |
|
287 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
288 |
((step_vars machines m)@ |
|
289 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
|
290 |
Format.pp_print_newline fmt (); |
|
291 |
|
|
292 |
|
|
293 |
|
|
294 |
if is_stateless m then |
|
295 |
begin |
|
296 |
(* Declaring single predicate *) |
|
297 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
298 |
pp_machine_stateless_name m.mname.node_id |
|
299 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
300 |
(List.map (fun v -> v.var_type) (stateless_vars machines m)); |
|
301 |
|
|
302 |
(* Rule for single predicate *) |
|
303 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
|
304 |
(pp_conj (pp_instr |
|
305 |
true (* In this case, the boolean init can be set to true or false. |
|
306 |
The node is stateless. *) |
|
307 |
m.mname.node_id) |
|
308 |
) |
|
309 |
m.mstep.step_instrs |
|
310 |
pp_machine_stateless_name m.mname.node_id |
|
311 |
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m); |
|
312 |
end |
|
313 |
else |
|
314 |
begin |
|
315 |
(* Declaring predicate *) |
|
316 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
317 |
pp_machine_init_name m.mname.node_id |
|
318 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
319 |
(List.map (fun v -> v.var_type) (init_vars machines m)); |
|
320 |
|
|
321 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
322 |
pp_machine_step_name m.mname.node_id |
|
323 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
324 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
325 |
|
|
326 |
Format.pp_print_newline fmt (); |
|
327 |
|
|
328 |
(* Rule for init *) |
|
329 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
|
330 |
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
|
331 |
pp_machine_init_name m.mname.node_id |
|
332 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
|
333 |
|
|
334 |
(* Rule for step *) |
|
335 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
|
336 |
(pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
|
337 |
pp_machine_step_name m.mname.node_id |
|
338 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
|
339 |
|
|
340 |
(* Adding assertions *) |
|
341 |
(match m.mstep.step_asserts with |
|
342 |
| [] -> () |
|
343 |
| assertsl -> begin |
|
344 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in |
|
345 |
|
|
346 |
Format.fprintf fmt "; Asserts@."; |
|
347 |
Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@." |
|
348 |
(pp_conj pp_val) assertsl; |
|
349 |
|
|
350 |
(** TEME: the following code is the one we described. But it generates a segfault in z3 |
|
351 |
Format.fprintf fmt "; Asserts for init@."; |
|
352 |
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@." |
|
353 |
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
|
354 |
pp_machine_init_name m.mname.node_id |
|
355 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m) |
|
356 |
(pp_conj pp_val) assertsl; |
|
357 |
|
|
358 |
Format.fprintf fmt "; Asserts for step@."; |
|
359 |
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@." |
|
360 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
|
361 |
|
|
362 |
pp_machine_step_name m.mname.node_id |
|
363 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m) |
|
364 |
(pp_conj pp_val) assertsl |
|
365 |
*) |
|
366 |
end |
|
367 |
); |
|
368 |
|
|
369 |
(* |
|
370 |
match m.mspec with |
|
371 |
None -> () (* No node spec; we do nothing *) |
|
372 |
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> |
|
373 |
( |
|
374 |
(* For the moment, we only deal with simple case: single ensures, no other parameters *) |
|
375 |
() |
|
376 |
|
|
377 |
) |
|
378 |
| _ -> () (* Other cases give nothing *) |
|
379 |
*) |
|
380 |
end |
|
381 |
end |
|
382 |
|
|
383 |
|
|
384 |
|
|
385 |
let collecting_semantics machines fmt node machine = |
|
386 |
Format.fprintf fmt "; Collecting semantics for node %s@.@." node; |
|
387 |
(* We print the types of the main node "memory tree" TODO: add the output *) |
|
388 |
let main_output = |
|
389 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
390 |
in |
|
391 |
let main_output_dummy = |
|
392 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
|
393 |
in |
|
394 |
let main_memory_next = |
|
395 |
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
|
396 |
main_output |
|
397 |
in |
|
398 |
let main_memory_current = |
|
399 |
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
|
400 |
main_output_dummy |
|
401 |
in |
|
402 |
|
|
403 |
(* Special case when the main node is stateless *) |
|
404 |
let init_name, step_name = |
|
405 |
if is_stateless machine then |
|
406 |
pp_machine_stateless_name, pp_machine_stateless_name |
|
407 |
else |
|
408 |
pp_machine_init_name, pp_machine_step_name |
|
409 |
in |
|
410 |
|
|
411 |
Format.fprintf fmt "(declare-rel MAIN (%a))@." |
|
412 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
413 |
(List.map (fun v -> v.var_type) main_memory_next); |
|
414 |
|
|
415 |
Format.fprintf fmt "; Initial set@."; |
|
416 |
Format.fprintf fmt "(declare-rel INIT_STATE ())@."; |
|
417 |
Format.fprintf fmt "(rule INIT_STATE)@."; |
|
418 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
|
419 |
init_name node |
|
420 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine) |
|
421 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ; |
|
422 |
|
|
423 |
Format.fprintf fmt "; Inductive def@."; |
|
424 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; |
|
425 |
Format.fprintf fmt |
|
426 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
|
427 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current |
|
428 |
step_name node |
|
429 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
|
430 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
|
431 |
|
|
432 |
let check_prop machines fmt node machine = |
|
433 |
let main_output = |
|
434 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
435 |
in |
|
436 |
let main_memory_next = |
|
437 |
(rename_next_list (full_memory_vars machines machine)) @ main_output |
|
438 |
in |
|
439 |
Format.fprintf fmt "; Property def@."; |
|
440 |
Format.fprintf fmt "(declare-rel ERR ())@."; |
|
441 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." |
|
442 |
(pp_conj pp_var) main_output |
|
443 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
|
444 |
; |
|
445 |
if !Options.horn_queries then |
|
446 |
Format.fprintf fmt "(query ERR)@." |
|
447 |
|
|
448 |
|
|
449 |
let cex_computation machines fmt node machine = |
|
450 |
Format.fprintf fmt "; CounterExample computation for node %s@.@." node; |
|
451 |
(* We print the types of the cex node "memory tree" TODO: add the output *) |
|
452 |
let cex_input = |
|
453 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
|
454 |
in |
|
455 |
let cex_input_dummy = |
|
456 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs |
|
457 |
in |
|
458 |
let cex_output = |
|
459 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
460 |
in |
|
461 |
let cex_output_dummy = |
|
462 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
|
463 |
in |
|
464 |
let cex_memory_next = |
|
465 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
|
466 |
in |
|
467 |
let cex_memory_current = |
|
468 |
cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy |
|
469 |
in |
|
470 |
|
|
471 |
(* Special case when the cex node is stateless *) |
|
472 |
let init_name, step_name = |
|
473 |
if is_stateless machine then |
|
474 |
pp_machine_stateless_name, pp_machine_stateless_name |
|
475 |
else |
|
476 |
pp_machine_init_name, pp_machine_step_name |
|
477 |
in |
|
478 |
|
|
479 |
Format.fprintf fmt "(declare-rel CEX (Int %a))@.@." |
|
480 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
481 |
(List.map (fun v -> v.var_type) cex_memory_next); |
|
482 |
|
|
483 |
Format.fprintf fmt "; Initial set@."; |
|
484 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@." |
|
485 |
init_name node |
|
486 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine) |
|
487 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ; |
|
488 |
|
|
489 |
Format.fprintf fmt "; Inductive def@."; |
|
490 |
(* Declare dummy inputs. Outputs should have been declared previously with collecting sem *) |
|
491 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy; |
|
492 |
Format.fprintf fmt "(declare-var cexcpt Int)@."; |
|
493 |
Format.fprintf fmt |
|
494 |
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@." |
|
495 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_current |
|
496 |
step_name node |
|
497 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
|
498 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next |
|
499 |
|
|
500 |
let get_cex machines fmt node machine = |
|
501 |
let cex_input = |
|
502 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
|
503 |
in |
|
504 |
let cex_output = |
|
505 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
506 |
in |
|
507 |
let cex_memory_next = |
|
508 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
|
509 |
in |
|
510 |
Format.fprintf fmt "; Property def@."; |
|
511 |
Format.fprintf fmt "(declare-rel CEXTRACE ())@."; |
|
512 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@." |
|
513 |
(pp_conj pp_var) cex_output |
|
514 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next |
|
515 |
; |
|
516 |
if !Options.horn_queries then |
|
517 |
Format.fprintf fmt "(query CEXTRACE)@." |
|
518 |
|
|
519 |
|
|
520 |
let main_print machines fmt = |
|
521 |
if !Options.main_node <> "" then |
|
522 |
begin |
|
523 |
let node = !Options.main_node in |
|
524 |
let machine = get_machine machines node in |
|
525 |
|
|
526 |
|
|
527 |
collecting_semantics machines fmt node machine; |
|
528 |
check_prop machines fmt node machine; |
|
529 |
if !Options.horn_cex then( |
|
530 |
cex_computation machines fmt node machine; |
|
531 |
get_cex machines fmt node machine) |
|
532 |
end |
|
533 |
|
|
534 |
|
|
535 |
let translate fmt basename prog machines = |
|
536 |
List.iter (print_machine machines fmt) (List.rev machines); |
|
537 |
|
|
538 |
main_print machines fmt |
|
539 |
|
|
540 |
|
|
541 |
let traces_file fmt basename prog machines = |
|
542 |
Format.fprintf fmt |
|
543 |
"; Horn code traceability generated by %s@.; SVN version number %s@.@." |
|
544 |
(Filename.basename Sys.executable_name) |
|
545 |
Version.number; |
|
546 |
|
|
547 |
(* We extract the annotation dealing with traceability *) |
|
548 |
let machines_traces = List.map (fun m -> |
|
549 |
let traces : (ident * expr) list= |
|
550 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
|
551 |
let filtered = |
|
552 |
List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots |
|
553 |
in |
|
554 |
let content = List.map snd filtered in |
|
555 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
|
556 |
List.map (fun ee -> |
|
557 |
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with |
|
558 |
| [], Expr_tuple [v;e] -> ( |
|
559 |
match v.expr_desc with |
|
560 |
| Expr_ident vid -> vid, e |
|
561 |
| _ -> assert false ) |
|
562 |
| _ -> assert false) |
|
563 |
content |
|
564 |
in |
|
565 |
|
|
566 |
m, traces |
|
567 |
|
|
568 |
) machines |
|
569 |
in |
|
570 |
|
|
571 |
(* Compute memories associated to each machine *) |
|
572 |
let compute_mems m = |
|
573 |
let rec aux fst prefix m = |
|
574 |
(List.map (fun mem -> (prefix, mem)) m.mmemory) @ |
|
575 |
List.fold_left (fun accu (id, (n, _)) -> |
|
576 |
let name = node_name n in |
|
577 |
if name = "_arrow" then accu else |
|
578 |
let machine_n = get_machine machines name in |
|
579 |
( aux false ((id,machine_n)::prefix) machine_n ) |
|
580 |
@ accu |
|
581 |
) [] m.minstances |
|
582 |
in |
|
583 |
aux true [] m |
|
584 |
in |
|
585 |
|
|
586 |
List.iter (fun m -> |
|
587 |
Format.fprintf fmt "; Node %s@." m.mname.node_id; |
|
588 |
|
|
589 |
let memories_old = |
|
590 |
List.map (fun (p, v) -> |
|
591 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
|
592 |
let traces = List.assoc machine machines_traces in |
|
593 |
if List.mem_assoc v.var_id traces then |
|
594 |
(* We take the expression associated to variable v in the trace info *) |
|
595 |
p, List.assoc v.var_id traces |
|
596 |
else |
|
597 |
(* We keep the variable as is: we create an expression v *) |
|
598 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
|
599 |
|
|
600 |
) (compute_mems m) |
|
601 |
in |
|
602 |
let memories_next = (* We remove the topest pre in each expression *) |
|
603 |
List.map |
|
604 |
(fun (prefix, ee) -> |
|
605 |
match ee.expr_desc with |
|
606 |
| Expr_pre e -> prefix, e |
|
607 |
| _ -> Format.eprintf |
|
608 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
|
609 |
(Utils.fprintf_list ~sep:"," |
|
610 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) |
|
611 |
(List.rev prefix) |
|
612 |
Printers.pp_expr ee; |
|
613 |
assert false) |
|
614 |
memories_old |
|
615 |
in |
|
616 |
|
|
617 |
let pp_prefix_rev fmt prefix = |
|
618 |
Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) |
|
619 |
in |
|
620 |
|
|
621 |
Format.fprintf fmt "; Init predicate@."; |
|
622 |
|
|
623 |
Format.fprintf fmt "; horn encoding@."; |
|
624 |
Format.fprintf fmt "(%a %a)@." |
|
625 |
pp_machine_init_name m.mname.node_id |
|
626 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
|
627 |
|
|
628 |
Format.fprintf fmt "; original expressions@."; |
|
629 |
Format.fprintf fmt "(%a %a%t%a)@." |
|
630 |
pp_machine_init_name m.mname.node_id |
|
631 |
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs) |
|
632 |
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ") |
|
633 |
(Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; |
|
634 |
|
|
635 |
Format.pp_print_newline fmt (); |
|
636 |
Format.fprintf fmt "; Step predicate@."; |
|
637 |
|
|
638 |
Format.fprintf fmt "; horn encoding@."; |
|
639 |
Format.fprintf fmt "(%a %a)@." |
|
640 |
pp_machine_step_name m.mname.node_id |
|
641 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
|
642 |
Format.fprintf fmt "; original expressions@."; |
|
643 |
Format.fprintf fmt "(%a %a%t%a)@." |
|
644 |
pp_machine_step_name m.mname.node_id |
|
645 |
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs) |
|
646 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ") |
|
647 |
(Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next); |
|
648 |
Format.pp_print_newline fmt (); |
|
649 |
) (List.rev machines); |
|
650 |
|
|
651 |
|
|
652 |
(* Local Variables: *) |
|
653 |
(* compile-command:"make -C .." *) |
|
654 |
(* End: *) |
src/backends/Java/java_backend.ml | ||
---|---|---|
1 |
(********************************************************************) |
|
2 |
(* *) |
|
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
|
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
|
5 |
(* *) |
|
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
|
7 |
(* under the terms of the GNU Lesser General Public License *) |
|
8 |
(* version 2.1. *) |
|
9 |
(* *) |
|
10 |
(********************************************************************) |
|
11 |
|
|
12 |
open Format |
|
13 |
open Utils |
|
14 |
open LustreSpec |
|
15 |
open Corelang |
|
16 |
open Machine_code |
|
17 |
|
|
18 |
|
|
19 |
(********************************************************************************************) |
|
20 |
(* Basic Printing functions *) |
|
21 |
(********************************************************************************************) |
|
22 |
|
|
23 |
let pp_final_char_if_non_empty c l = |
|
24 |
(fun fmt -> match l with [] -> () | _ -> fprintf fmt "%s" c) |
|
25 |
|
|
26 |
let pp_newline_if_non_empty l = |
|
27 |
(fun fmt -> match l with [] -> () | _ -> fprintf fmt "@,") |
|
28 |
|
|
29 |
let pp_dimension fmt d = |
|
30 |
Printers.pp_expr fmt (expr_of_dimension d) |
|
31 |
|
|
32 |
let pp_type fmt t = |
|
33 |
match (Types.repr t).Types.tdesc with |
|
34 |
| Types.Tbool -> pp_print_string fmt "boolean" |
|
35 |
| Types.Treal -> pp_print_string fmt "double" |
|
36 |
| _ -> Types.print_ty fmt t |
|
37 |
|
|
38 |
let pp_var fmt id = fprintf fmt "%a %s" pp_type id.var_type id.var_id |
|
39 |
|
|
40 |
let pp_tag fmt t = |
|
41 |
pp_print_string fmt t |
|
42 |
|
|
43 |
let rec pp_const fmt c = |
|
44 |
match c with |
|
45 |
| Const_int i -> pp_print_int fmt i |
|
46 |
| Const_real r -> pp_print_string fmt r |
|
47 |
| Const_float r -> pp_print_float fmt r |
|
48 |
| Const_tag t -> pp_tag fmt t |
|
49 |
| Const_array ca -> Format.fprintf fmt "{%a}" (Utils.fprintf_list ~sep:"," pp_const) ca |
|
50 |
|
|
51 |
let rec pp_val m fmt v = |
|
52 |
match v with |
|
53 |
| Cst c -> pp_const fmt c |
|
54 |
| LocalVar v -> |
|
55 |
if List.exists (fun o -> o.var_id = v) m.mstep.step_outputs then |
|
56 |
fprintf fmt "*%s" v |
|
57 |
else |
|
58 |
pp_print_string fmt v |
|
59 |
| StateVar v -> fprintf fmt "%s" v |
|
60 |
| Fun (n, vl) -> if Basic_library.is_internal_fun n then |
|
61 |
Basic_library.pp_java n (pp_val m) fmt vl |
|
62 |
else |
|
63 |
fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " (pp_val m)) vl |
|
64 |
|
|
65 |
let pp_add_val m fmt i = |
|
66 |
if List.exists (fun o -> o.var_id = i) m.mstep.step_outputs |
|
67 |
then |
|
68 |
fprintf fmt "%s" i |
|
69 |
else |
|
70 |
fprintf fmt "&%s" i |
|
71 |
|
|
72 |
(********************************************************************************************) |
|
73 |
(* Instruction Printing functions *) |
|
74 |
(********************************************************************************************) |
|
75 |
let get_output_of_machine machines i = |
|
76 |
try |
|
77 |
let m = List.find (fun m -> m.mname.node_id = i) machines in |
|
78 |
m.mstep.step_outputs |
|
79 |
with Not_found -> assert false |
|
80 |
|
|
81 |
let rec pp_machine_instr m machines instance_out_list fmt instr = |
|
82 |
match instr with |
|
83 |
| MReset i -> ( |
|
84 |
match List.assoc i m.minstances with |
|
85 |
| "_arrow" -> fprintf fmt "%s = true;" i |
|
86 |
| _ -> fprintf fmt "%s.reset();" i |
|
87 |
) |
|
88 |
| MLocalAssign (i,v) -> ( |
|
89 |
fprintf fmt "%s = %a;" |
|
90 |
i (pp_val m) v |
|
91 |
) |
|
92 |
| MStateAssign (i,v) -> |
|
93 |
fprintf fmt "%s = %a;" i (pp_val m) v |
|
94 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
|
95 |
fprintf fmt "%s = %a;" i0 (Basic_library.pp_java i (pp_val m)) vl |
|
96 |
| MStep ([i0], i, [init; step]) when ((List.assoc i m.minstances) = "_arrow") -> ( |
|
97 |
fprintf fmt "@[<v 2>if (%s) {@,%s = false;@,%s = %a;@]@,@[<v 2>} else {@,%s = %a;@]@,};@," |
|
98 |
i i i0 (pp_val m) init i0 (pp_val m) step |
|
99 |
) |
|
100 |
| MStep (il, i, vl) -> ( |
|
101 |
let out = |
|
102 |
try |
|
103 |
List.assoc i instance_out_list |
|
104 |
with Not_found -> (eprintf "impossible to find instance %s in the list@.@?" i; |
|
105 |
assert false) |
|
106 |
in |
|
107 |
fprintf fmt "%s = %s.step (%a);@," |
|
108 |
out i |
|
109 |
(Utils.fprintf_list ~sep:", " (pp_val m)) vl; |
|
110 |
Utils.fprintf_list ~sep:"@," |
|
111 |
(fun fmt (o, oname) -> fprintf fmt "%s = %s.%s;" o out oname) fmt |
|
112 |
(List.map2 |
|
113 |
(fun x y -> x, y.var_id) |
|
114 |
il |
|
115 |
(get_output_of_machine machines (List.assoc i m.minstances)) |
|
116 |
) |
|
117 |
) |
|
118 |
|
|
119 |
| MBranch (g,hl) -> |
|
120 |
Format.fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]" |
|
121 |
(pp_val m) g |
|
122 |
(Utils.fprintf_list ~sep:"@," (pp_machine_branch m machines instance_out_list)) hl |
|
123 |
|
|
124 |
and pp_machine_branch m machines instance_out_list fmt (t, h) = |
|
125 |
Format.fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_tag t (Utils.fprintf_list ~sep:"@," (pp_machine_instr m machines instance_out_list)) h |
|
126 |
|
|
127 |
(********************************************************************************************) |
|
128 |
(* Java file Printing functions *) |
|
129 |
(********************************************************************************************) |
|
130 |
|
|
131 |
let get_class_name n = match n with "_arrow" -> "boolean" | _ -> String.capitalize n |
|
132 |
|
|
133 |
let pp_local_fields visibility = |
|
134 |
fprintf_list ~sep:"@," (fun fmt v -> fprintf fmt "%s %a;" visibility pp_var v) |
|
135 |
|
|
136 |
let pp_local_field_instances = |
|
137 |
fprintf_list ~sep:"@," |
|
138 |
(fun fmt (node_inst, node_type) -> fprintf fmt "protected %s %s;" |
|
139 |
(get_class_name node_type) |
|
140 |
node_inst |
|
141 |
) |
|
142 |
|
|
143 |
let pp_output_constructor fmt outputs = |
|
144 |
fprintf fmt "@[<v 2>public Output(%a) {@,%a@]@,}" |
|
145 |
(fprintf_list ~sep:"; " pp_var) outputs |
|
146 |
(fprintf_list ~sep:"@," (fun fmt v -> fprintf fmt "this.%s = %s;" v.var_id v.var_id)) outputs |
|
147 |
|
|
148 |
let pp_output_class fmt step = |
|
149 |
fprintf fmt "@[<v 2>public class Output {@,%a@,@,%a@]@,}@," |
|
150 |
(pp_local_fields "public") step.step_outputs |
|
151 |
pp_output_constructor step.step_outputs |
|
152 |
|
|
153 |
let pp_constructor fmt (name, instances) = |
|
154 |
fprintf fmt "@[<v 2>public %s () {@,%a@]@,}@," |
|
155 |
(String.capitalize name) |
|
156 |
( |
|
157 |
fprintf_list ~sep:"@," |
|
158 |
(fun fmt (node_inst, node_type) -> |
|
159 |
match node_type with |
|
160 |
"_arrow" -> fprintf fmt "%s = true;" node_inst |
|
161 |
| _ -> fprintf fmt "%s = new %s();" node_inst (get_class_name node_type) |
|
162 |
) |
|
163 |
) |
|
164 |
instances |
|
165 |
|
|
166 |
let pp_reset machines fmt m = |
|
167 |
fprintf fmt "@[<v 2>public void reset () {@,%a@]@,}@," |
|
168 |
(fprintf_list ~sep:"@," (pp_machine_instr m machines [])) m.minit |
|
169 |
|
|
170 |
let pp_step machines fmt m : unit = |
|
171 |
let out_assoc_list = |
|
172 |
List.map (fun (node_inst, _) -> node_inst, "out_" ^ node_inst) m.minstances |
|
173 |
in |
|
174 |
fprintf fmt |
|
175 |
"@[<v 2>public Output step (%a) {@,%a%t@,%a%a%t@,%a@,%t@]@,}@," |
|
176 |
(Utils.fprintf_list ~sep:",@ " pp_var) m.mstep.step_inputs |
|
177 |
(* locals *) |
|
178 |
(Utils.fprintf_list ~sep:";@," pp_var) m.mstep.step_locals |
|
179 |
(pp_final_char_if_non_empty ";" m.mstep.step_locals) |
|
180 |
(* declare out variables of subnode instances + out of this node *) |
|
181 |
(fprintf_list ~sep:"" |
|
182 |
(fun fmt (ninst, ntype) -> fprintf fmt "%s.Output out_%s;@," (get_class_name ntype) ninst )) |
|
183 |
(List.filter (fun (_,ntyp) -> not (ntyp = "_arrow")) m.minstances) |
|
184 |
(fprintf_list ~sep:";@," pp_var) m.mstep.step_outputs |
|
185 |
(pp_final_char_if_non_empty ";" m.mstep.step_outputs) |
|
186 |
(* instructions *) |
|
187 |
(fprintf_list ~sep:"@," (pp_machine_instr m machines out_assoc_list)) m.mstep.step_instrs |
|
188 |
(* create out object and return it *) |
|
189 |
(fun fmt -> fprintf fmt "return new Output(%a);" |
|
190 |
(fprintf_list ~sep:"," (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_outputs |
|
191 |
) |
|
192 |
|
|
193 |
|
|
194 |
|
|
195 |
let print_machine machines fmt m = |
|
196 |
if m.mname.node_id = "_arrow" then () else ( (* We don't print arrow function *) |
|
197 |
fprintf fmt "@[<v 2>class %s {@,%a%t%a%t%t%a@,%a@,%a@,%a@]@,}@.@.@." |
|
198 |
(String.capitalize m.mname.node_id) (* class name *) |
|
199 |
(pp_local_fields "protected") m.mmemory (* fields *) |
|
200 |
(pp_newline_if_non_empty m.mmemory) |
|
201 |
pp_local_field_instances m.minstances (* object fields *) |
|
202 |
(pp_newline_if_non_empty m.minstances) |
|
203 |
(pp_newline_if_non_empty m.minstances) |
|
204 |
pp_output_class m.mstep (* class for output of step method *) |
|
205 |
pp_constructor (m.mname.node_id, m.minstances) (* constructor to instanciate object fields *) |
|
206 |
(pp_reset machines) m (* reset method *) |
|
207 |
(pp_step machines) m (* step method *) |
|
208 |
|
|
209 |
) |
|
210 |
|
|
211 |
(********************************************************************************************) |
|
212 |
(* Main related functions *) |
|
213 |
(********************************************************************************************) |
|
214 |
|
|
215 |
(* let print_get_input fmt v = *) |
|
216 |
(* match v.var_type.Types.tdesc with *) |
|
217 |
(* | Types.Tint -> fprintf fmt "_get_int(\"%s\")" v.var_id *) |
|
218 |
(* | Types.Tbool -> fprintf fmt "_get_bool(\"%s\")" v.var_id *) |
|
219 |
(* | Types.Treal -> fprintf fmt "_get_double(\"%s\")" v.var_id *) |
|
220 |
(* | _ -> assert false *) |
|
221 |
|
|
222 |
(* let print_put_outputs fmt ol = *) |
|
223 |
(* let po fmt o = *) |
|
224 |
(* match o.var_type.Types.tdesc with *) |
|
225 |
(* | Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o.var_id o.var_id *) |
|
226 |
(* | Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o.var_id o.var_id *) |
|
227 |
(* | Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o.var_id o.var_id *) |
|
228 |
(* | _ -> assert false *) |
|
229 |
(* in *) |
|
230 |
(* List.iter (fprintf fmt "@ %a;" po) ol *) |
|
231 |
|
|
232 |
let read_input fmt typ = match typ.Types.tdesc with |
|
233 |
| Types.Treal -> fprintf fmt "StdIn.readDouble()" |
|
234 |
| Types.Tint -> fprintf fmt "StdIn.readInt()" |
|
235 |
| Types.Tbool -> fprintf fmt "StdIn.readBoolean()" |
|
236 |
| _ -> assert false |
|
237 |
|
|
238 |
let print_main_fun basename machines m fmt = |
|
239 |
let m_class = String.capitalize m.mname.node_id in |
|
240 |
fprintf fmt "@[<v 2>class %s {@,@,@[<v 2>%s {@,%t@,%t@]@,}@,@]@,}@." |
|
241 |
(String.capitalize basename) |
|
242 |
"public static void main (String[] args)" |
|
243 |
(fun fmt -> fprintf fmt "%s main_node = new %s();" m_class m_class) |
|
244 |
(fun fmt -> fprintf fmt "@[<v 2>while (true) {@,%a@,%t@,%a@]@,}@," |
|
245 |
(fprintf_list ~sep:"@," |
|
246 |
(fun fmt v -> fprintf fmt "System.out.println(\"%s?\");@,%a = %a;" |
|
247 |
v.var_id pp_var v read_input v.var_type)) |
|
248 |
m.mstep.step_inputs |
|
249 |
(fun fmt -> fprintf fmt "%s.Output out = main_node.step(%a);" |
|
250 |
m_class |
|
251 |
(fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs |
|
252 |
) |
|
253 |
(fprintf_list ~sep:"@," (fun fmt v -> fprintf fmt "System.out.println(\"%s = \" + out.%s);" v.var_id v.var_id)) |
|
254 |
m.mstep.step_outputs |
|
255 |
) |
|
256 |
|
|
257 |
|
|
258 |
(* let print_main_fun machines m fmt = *) |
|
259 |
(* let mname = m.mname.node_id in *) |
|
260 |
(* let main_mem = *) |
|
261 |
(* if (!Options.static_mem && !Options.main_node <> "") *) |
|
262 |
(* then "&main_mem" *) |
|
263 |
(* else "main_mem" in *) |
|
264 |
(* fprintf fmt "@[<v 2>int main (int argc, char *argv[]) {@ "; *) |
|
265 |
(* fprintf fmt "/* Declaration of inputs/outputs variables */@ "; *) |
|
266 |
(* List.iter *) |
|
267 |
(* (fun v -> fprintf fmt "%a %s = %a;@ " pp_c_type v.var_type v.var_id pp_c_initialize v.var_type *) |
|
268 |
(* ) m.mstep.step_inputs; *) |
|
269 |
(* List.iter *) |
|
270 |
(* (fun v -> fprintf fmt "%a %s = %a;@ " pp_c_type v.var_type v.var_id pp_c_initialize v.var_type *) |
|
271 |
(* ) m.mstep.step_outputs; *) |
|
272 |
(* fprintf fmt "@ /* Main memory allocation */@ "; *) |
|
273 |
(* if (!Options.static_mem && !Options.main_node <> "") *) |
|
274 |
(* then (fprintf fmt "%a(main_mem);@ " pp_machine_static_alloc_name mname) *) |
|
275 |
(* else (fprintf fmt "%a *main_mem = %a();@ " pp_machine_memtype_name mname pp_machine_alloc_name mname); *) |
|
276 |
(* fprintf fmt "@ /* Initialize the main memory */@ "; *) |
|
277 |
(* fprintf fmt "%a(%s);@ " pp_machine_reset_name mname main_mem; *) |
|
278 |
(* fprintf fmt "@ ISATTY = isatty(0);@ "; *) |
|
279 |
(* fprintf fmt "@ /* Infinite loop */@ "; *) |
|
280 |
(* fprintf fmt "@[<v 2>while(1){@ "; *) |
|
281 |
(* fprintf fmt "fflush(stdout);@ "; *) |
|
282 |
(* List.iter *) |
|
283 |
(* (fun v -> fprintf fmt "%s = %a;@ " *) |
|
284 |
(* v.var_id *) |
|
285 |
(* print_get_input v *) |
|
286 |
(* ) m.mstep.step_inputs; *) |
|
287 |
(* (match m.mstep.step_outputs with *) |
|
288 |
(* | [] -> ( *) |
|
289 |
(* fprintf fmt "%a(%a%t%s);@ " *) |
|
290 |
(* pp_machine_step_name mname *) |
|
291 |
(* (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *) |
|
292 |
(* (pp_final_char_if_non_empty ", " m.mstep.step_inputs) *) |
|
293 |
(* main_mem *) |
|
294 |
(* ) *) |
|
295 |
(* | [o] -> ( *) |
|
296 |
(* fprintf fmt "%s = %a(%a%t%a, %s);%a" *) |
|
297 |
(* o.var_id *) |
|
298 |
(* pp_machine_step_name mname *) |
|
299 |
(* (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *) |
|
300 |
(* (pp_final_char_if_non_empty ", " m.mstep.step_inputs) *) |
|
301 |
(* (Utils.fprintf_list ~sep:", " (fun fmt v -> fprintf fmt "&%s" v.var_id)) m.mstep.step_outputs *) |
|
302 |
(* main_mem *) |
|
303 |
(* print_put_outputs [o]) *) |
|
304 |
(* | _ -> ( *) |
|
305 |
(* fprintf fmt "%a(%a%t%a, %s);%a" *) |
|
306 |
(* pp_machine_step_name mname *) |
|
307 |
(* (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *) |
|
308 |
(* (pp_final_char_if_non_empty ", " m.mstep.step_inputs) *) |
|
309 |
(* (Utils.fprintf_list ~sep:", " (fun fmt v -> fprintf fmt "&%s" v.var_id)) m.mstep.step_outputs *) |
|
310 |
(* main_mem *) |
|
311 |
(* print_put_outputs m.mstep.step_outputs) *) |
|
312 |
(* ); *) |
|
313 |
(* fprintf fmt "@]@ }@ "; *) |
|
314 |
(* fprintf fmt "return 1;"; *) |
|
315 |
(* fprintf fmt "@]@ }@." *) |
|
316 |
|
|
317 |
(* let print_main_header fmt = *) |
|
318 |
(* fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"io_frontend.h\"@." *) |
|
319 |
|
|
320 |
|
|
321 |
(********************************************************************************************) |
|
322 |
(* Translation function *) |
|
323 |
(********************************************************************************************) |
|
324 |
|
|
325 |
let translate_to_java source_fmt basename prog machines = |
|
326 |
|
|
327 |
|
|
328 |
(* If a main node is identified, generate a main function for it *) |
|
329 |
let main_print = |
|
330 |
match !Options.main_node with |
|
331 |
| "" -> (fun _ -> ()) |
|
332 |
| main_node -> ( |
|
333 |
let main_node_opt = |
|
334 |
List.fold_left |
|
335 |
(fun res m -> |
|
336 |
match res with |
|
337 |
| Some _ -> res |
|
338 |
| None -> if m.mname.node_id = main_node then Some m else None) |
|
339 |
None machines |
|
340 |
in |
|
341 |
match main_node_opt with |
|
342 |
| None -> eprintf "Unable to find a main node named %s@.@?" main_node; (fun _ -> ()) |
|
343 |
| Some m -> print_main_fun basename machines m |
|
344 |
) |
|
345 |
in |
|
346 |
|
|
347 |
(* Print nodes one by one (in the previous order) *) |
|
348 |
List.iter ((print_machine machines) source_fmt) machines; |
|
349 |
main_print source_fmt |
|
350 |
|
|
351 |
|
|
352 |
|
|
353 |
|
|
354 |
(* Local Variables: *) |
|
355 |
(* compile-command:"make -C .." *) |
|
356 |
(* End: *) |
src/basic_library.ml | ||
---|---|---|
1 |
(* ---------------------------------------------------------------------------- |
|
2 |
* SchedMCore - A MultiCore Scheduling Framework |
|
3 |
* Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
|
4 |
* Copyright (C) 2012-2013, INPT, Toulouse, FRANCE |
|
5 |
* |
|
6 |
* This file is part of Prelude |
|
7 |
* |
Also available in: Unified diff