| 1 |
0cbf0839
|
ploc
|
(* ----------------------------------------------------------------------------
|
| 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 *)
|
| 25 |
|
|
|
| 26 |
e95470b3
|
ploc
|
open Format
|
| 27 |
dae9db56
|
ploc
|
open LustreSpec
|
| 28 |
|
|
open Machine_code
|
| 29 |
0cbf0839
|
ploc
|
(********************************************************************************************)
|
| 30 |
|
|
(* Translation function *)
|
| 31 |
|
|
(********************************************************************************************)
|
| 32 |
d2be420e
|
ploc
|
|
| 33 |
e95470b3
|
ploc
|
let makefile_opt print basename dependencies makefile_fmt machines =
|
| 34 |
|
|
(* If a main node is identified, generate a main target for it *)
|
| 35 |
|
|
match !Options.main_node with
|
| 36 |
|
|
| "" -> ()
|
| 37 |
|
|
| main_node -> (
|
| 38 |
|
|
match Machine_code.get_machine_opt main_node machines with
|
| 39 |
|
|
| None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; ()
|
| 40 |
|
|
| Some _ -> print basename !Options.main_node dependencies makefile_fmt
|
| 41 |
|
|
)
|
| 42 |
|
|
|
| 43 |
e3945827
|
gdavy
|
module type MODIFIER = sig
|
| 44 |
|
|
module HdrMod : C_backend_header.MODIFIERS_HDR
|
| 45 |
|
|
module SrcMod : C_backend_src.MODIFIERS_SRC
|
| 46 |
|
|
module MainMod : C_backend_main.MODIFIERS_MAINSRC
|
| 47 |
|
|
module MakefileMod : C_backend_makefile.MODIFIERS_MKF
|
| 48 |
bd09b789
|
gdavy
|
module CoqMod : C_backend_coq.MODIFIERS_COQ
|
| 49 |
e3945827
|
gdavy
|
|
| 50 |
|
|
val init : machine_t list -> unit
|
| 51 |
|
|
end
|
| 52 |
e95470b3
|
ploc
|
|
| 53 |
e3945827
|
gdavy
|
module EmptyMod = struct
|
| 54 |
|
|
module HdrMod = C_backend_header.EmptyMod
|
| 55 |
|
|
module SrcMod = C_backend_src.EmptyMod
|
| 56 |
|
|
module MainMod = C_backend_main.EmptyMod
|
| 57 |
|
|
module MakefileMod = C_backend_makefile.EmptyMod
|
| 58 |
bd09b789
|
gdavy
|
module CoqMod = C_backend_coq.EmptyMod
|
| 59 |
713176a4
|
ploc
|
|
| 60 |
e3945827
|
gdavy
|
let init machines = ()
|
| 61 |
|
|
end
|
| 62 |
|
|
|
| 63 |
|
|
module Backend = functor (Mod:MODIFIER) ->
|
| 64 |
|
|
struct
|
| 65 |
|
|
module Header = C_backend_header.Main (Mod.HdrMod)
|
| 66 |
|
|
module Source = C_backend_src.Main (Mod.SrcMod)
|
| 67 |
|
|
module SourceMain = C_backend_main.Main (Mod.MainMod)
|
| 68 |
|
|
module Makefile = C_backend_makefile.Main (Mod.MakefileMod)
|
| 69 |
bd09b789
|
gdavy
|
module Coq = C_backend_coq.Main (Mod.CoqMod)
|
| 70 |
d2be420e
|
ploc
|
|
| 71 |
bd09b789
|
gdavy
|
let gen_files basename prog machines dependencies header_file source_lib_file source_main_file makefile_file coq_file machines =
|
| 72 |
e3945827
|
gdavy
|
Mod.init machines;
|
| 73 |
e95470b3
|
ploc
|
|
| 74 |
e3945827
|
gdavy
|
let header_out = open_out header_file in
|
| 75 |
|
|
let header_fmt = formatter_of_out_channel header_out in
|
| 76 |
|
|
let source_lib_out = open_out source_lib_file in
|
| 77 |
|
|
let source_lib_fmt = formatter_of_out_channel source_lib_out in
|
| 78 |
|
|
|
| 79 |
|
|
(* Generating H file *)
|
| 80 |
|
|
Header.print_header header_fmt basename prog machines;
|
| 81 |
|
|
|
| 82 |
|
|
(* Generating Lib C file *)
|
| 83 |
|
|
Source.print_lib_c source_lib_fmt basename prog machines dependencies;
|
| 84 |
bd09b789
|
gdavy
|
|
| 85 |
|
|
(match coq_file with
|
| 86 |
|
|
| None -> ()
|
| 87 |
|
|
| Some path ->
|
| 88 |
|
|
let coq_lib_out = open_out path in
|
| 89 |
|
|
let coq_lib_fmt = formatter_of_out_channel coq_lib_out in
|
| 90 |
|
|
Coq.print_lib_coq coq_lib_fmt basename prog machines
|
| 91 |
|
|
);
|
| 92 |
e3945827
|
gdavy
|
match !Options.main_node with
|
| 93 |
|
|
| "" -> () (* No main node: we do not genenrate main nor makefile *)
|
| 94 |
|
|
| main_node -> (
|
| 95 |
|
|
match Machine_code.get_machine_opt main_node machines with
|
| 96 |
|
|
| None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; assert false
|
| 97 |
|
|
| Some m -> begin
|
| 98 |
|
|
let source_main_out = open_out source_main_file in
|
| 99 |
|
|
let source_main_fmt = formatter_of_out_channel source_main_out in
|
| 100 |
|
|
let makefile_out = open_out makefile_file in
|
| 101 |
|
|
let makefile_fmt = formatter_of_out_channel makefile_out in
|
| 102 |
713176a4
|
ploc
|
|
| 103 |
e3945827
|
gdavy
|
(* Generating Main C file *)
|
| 104 |
|
|
SourceMain.print_main_c source_main_fmt m basename prog machines dependencies;
|
| 105 |
|
|
|
| 106 |
|
|
(* Generating Makefile *)
|
| 107 |
|
|
Makefile.print_makefile basename main_node dependencies makefile_fmt
|
| 108 |
|
|
end
|
| 109 |
|
|
)
|
| 110 |
|
|
end
|
| 111 |
713176a4
|
ploc
|
|
| 112 |
bd09b789
|
gdavy
|
let translate_to_c header source_lib source_main makefile coq_file basename prog machines dependencies =
|
| 113 |
e3945827
|
gdavy
|
Format.printf "%a" (Utils.fprintf_list ~sep:"\n@ " pp_machine) machines;
|
| 114 |
|
|
let module SpecArg = struct
|
| 115 |
|
|
let prog = prog
|
| 116 |
|
|
let machines = arrow_machine::machines
|
| 117 |
|
|
end in
|
| 118 |
|
|
let module ProofArg = struct
|
| 119 |
|
|
let prog = prog
|
| 120 |
|
|
let machines = arrow_machine::machines
|
| 121 |
|
|
end in
|
| 122 |
|
|
let module SpecMod = C_backend_spec.Make (SpecArg) in
|
| 123 |
|
|
let module ProofMod = C_backend_proof.Make (ProofArg) in
|
| 124 |
|
|
|
| 125 |
e95470b3
|
ploc
|
match !Options.spec with
|
| 126 |
|
|
| "no" -> begin
|
| 127 |
e3945827
|
gdavy
|
let module B = Backend(EmptyMod) in
|
| 128 |
bd09b789
|
gdavy
|
B.gen_files basename prog machines dependencies header source_lib source_main makefile None machines
|
| 129 |
e95470b3
|
ploc
|
end
|
| 130 |
|
|
| "acsl" -> begin
|
| 131 |
e3945827
|
gdavy
|
let module B = Backend(SpecMod) in
|
| 132 |
bd09b789
|
gdavy
|
B.gen_files basename prog machines dependencies header source_lib source_main makefile None machines
|
| 133 |
e3945827
|
gdavy
|
end
|
| 134 |
|
|
| "proof" -> begin
|
| 135 |
|
|
let module B = Backend(ProofMod) in
|
| 136 |
bd09b789
|
gdavy
|
B.gen_files basename prog machines dependencies header source_lib source_main makefile (Some coq_file) machines
|
| 137 |
e95470b3
|
ploc
|
end
|
| 138 |
|
|
| "c" -> begin
|
| 139 |
|
|
assert false (* not implemented yet *)
|
| 140 |
|
|
end
|
| 141 |
|
|
| _ -> assert false
|
| 142 |
0cbf0839
|
ploc
|
(* Local Variables: *)
|
| 143 |
522938b5
|
ploc
|
(* compile-command:"make -C ../../.." *)
|
| 144 |
0cbf0839
|
ploc
|
(* End: *)
|