Project

General

Profile

Revision b38ffff3

View differences:

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
 *
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff