Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / C / c_backend.ml @ 80f93e0a

History | View | Annotate | Download (6.05 KB)

1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
12 d4107cf2 ploc
open Format
13 22fe1c93 ploc
(********************************************************************************************)
14
(*                         Translation function                                             *)
15
(********************************************************************************************)
16 ef34b4ae xthirioux
(* USELESS
17 d4107cf2 ploc
let makefile_opt print basename dependencies makefile_fmt machines =
18
  (* If a main node is identified, generate a main target for it *)
19
  match !Options.main_node with
20
  | "" ->  ()
21
  | main_node -> (
22
    match Machine_code.get_machine_opt main_node machines with
23
    | None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; ()
24
    | Some _ -> print basename !Options.main_node dependencies makefile_fmt
25
  )
26 ef34b4ae xthirioux
*)
27 d4107cf2 ploc
28 dc893173 ploc
let gen_files funs basename prog machines dependencies =
29
  let destname = !Options.dest_dir ^ "/" ^ basename in
30
  
31 dcafc99b Ploc
  let print_header, print_lib_c, print_main_c, print_makefile(* , print_cmake *) = funs in
32 dc893173 ploc
33 d4107cf2 ploc
  (* Generating H file *)
34 dc893173 ploc
  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
35
  let header_out = open_out alloc_header_file in
36
  let header_fmt = formatter_of_out_channel header_out in
37 ef34b4ae xthirioux
  print_header header_fmt basename prog machines dependencies;
38 dc893173 ploc
  close_out header_out;
39
  
40 d4107cf2 ploc
  (* Generating Lib C file *)
41 dc893173 ploc
  let source_lib_file = destname ^ ".c" in (* Could be changed *)
42
  let source_lib_out = open_out source_lib_file in
43
  let source_lib_fmt = formatter_of_out_channel source_lib_out in
44 d4107cf2 ploc
  print_lib_c source_lib_fmt basename prog machines dependencies;
45 ef34b4ae xthirioux
  close_out source_lib_out;
46
47 bb1b5e04 Ploc
  (match !Options.main_node with
48
  | "" ->  () (* No main node: we do not generate main *)
49 d4107cf2 ploc
  | main_node -> (
50
    match Machine_code.get_machine_opt main_node machines with
51 04a63d25 xthirioux
    | None -> begin
52
      Global.main_node := main_node;
53
      Format.eprintf "Code generation error: %a@." Corelang.pp_error LustreSpec.Main_not_found;
54
      raise (Corelang.Error (Location.dummy_loc, LustreSpec.Main_not_found))
55
    end
56 d4107cf2 ploc
    | Some m -> begin
57 bb1b5e04 Ploc
      let source_main_file = destname ^ "_main.c" in (* Could be changed *)
58 d4107cf2 ploc
      let source_main_out = open_out source_main_file in
59
      let source_main_fmt = formatter_of_out_channel source_main_out in
60 13eb21df ploc
61 d4107cf2 ploc
      (* Generating Main C file *)
62
      print_main_c source_main_fmt m basename prog machines dependencies;
63 ef34b4ae xthirioux
64 bb1b5e04 Ploc
      close_out source_main_out;
65 d4107cf2 ploc
    end
66 bb1b5e04 Ploc
  ));
67
68
69
  (* Makefiles:
70
     - for the moment two cases
71
     1. Classical Makefile, only when provided with a main node
72
     May contain additional framac eacsl targets
73
     2. Cmake : 2 files
74
         - lustrec-basename.cmake describing all variables
75
         - the main CMakeLists.txt activating the first file
76
     - Later option 1 should be removed
77
  *)
78
  (* Case 1 *)
79
  (match !Options.main_node with
80
  | "" ->  () (* No main node: we do not generate main *)
81
  | main_node -> (
82
    let makefile_file = destname ^ ".makefile" in (* Could be changed *)
83
    let makefile_out = open_out makefile_file in
84
    let makefile_fmt = formatter_of_out_channel makefile_out in
85
    
86
    (* Generating Makefile *)
87
    print_makefile basename main_node dependencies makefile_fmt;
88
    
89
    close_out makefile_out
90 dcafc99b Ploc
  ))(* ; *)
91 bb1b5e04 Ploc
  
92 dcafc99b Ploc
  (* (\* Case 2 *\) *)
93
  (* let cmake_file = "lustrec-" ^ basename ^ ".cmake" in *)
94
  (* let cmake_file_full_path = !Options.dest_dir ^ "/" ^ cmake_file in *)
95
  (* let cmake_out = open_out cmake_file_full_path in *)
96
  (* let cmake_fmt = formatter_of_out_channel cmake_out in *)
97
  (* (\* Generating Makefile *\) *)
98
  (* print_cmake basename main_node dependencies makefile_fmt; *)
99 bb1b5e04 Ploc
    
100 dcafc99b Ploc
  (*   close_out makefile_out *)
101 bb1b5e04 Ploc
  
102 cefc3744 ploc
103 dc893173 ploc
let translate_to_c basename prog machines dependencies =
104 d4107cf2 ploc
  match !Options.spec with
105
  | "no" -> begin
106
    let module HeaderMod = C_backend_header.EmptyMod in
107
    let module SourceMod = C_backend_src.EmptyMod in
108
    let module SourceMainMod = C_backend_main.EmptyMod in
109
    let module MakefileMod = C_backend_makefile.EmptyMod in
110 cefc3744 ploc
111 d4107cf2 ploc
    let module Header = C_backend_header.Main (HeaderMod) in
112
    let module Source = C_backend_src.Main (SourceMod) in
113
    let module SourceMain = C_backend_main.Main (SourceMainMod) in
114
    let module Makefile = C_backend_makefile.Main (MakefileMod) in
115 dcafc99b Ploc
    (* let module CMakefile = C_backend_cmake.Main (MakefileMod) in *)
116 bb1b5e04 Ploc
    
117 58a463e7 ploc
    let funs = 
118
      Header.print_alloc_header, 
119
      Source.print_lib_c, 
120
      SourceMain.print_main_c, 
121 dcafc99b Ploc
      Makefile.print_makefile(* , *)
122
      (* CMakefile.print_makefile *)
123 58a463e7 ploc
    in
124 dc893173 ploc
    gen_files funs basename prog machines dependencies 
125 cefc3744 ploc
126 d4107cf2 ploc
  end
127
  | "acsl" -> begin
128 13eb21df ploc
129 d4107cf2 ploc
    let module HeaderMod = C_backend_header.EmptyMod in
130
    let module SourceMod = C_backend_src.EmptyMod in
131
    let module SourceMainMod = C_backend_main.EmptyMod in
132
    let module MakefileMod = C_backend_spec.MakefileMod in
133 22fe1c93 ploc
134 d4107cf2 ploc
    let module Header = C_backend_header.Main (HeaderMod) in
135
    let module Source = C_backend_src.Main (SourceMod) in
136
    let module SourceMain = C_backend_main.Main (SourceMainMod) in
137
    let module Makefile = C_backend_makefile.Main (MakefileMod) in
138 dcafc99b Ploc
    (* let module CMakefile = C_backend_cmake.Main (MakefileMod) in *)
139 bb1b5e04 Ploc
    
140 58a463e7 ploc
    let funs = 
141
      Header.print_alloc_header, 
142
      Source.print_lib_c,
143
      SourceMain.print_main_c,
144 dcafc99b Ploc
      Makefile.print_makefile(* , *)
145
      (* CMakefile.print_makefile  *)
146 58a463e7 ploc
    in
147 dc893173 ploc
    gen_files funs basename prog machines dependencies 
148 22fe1c93 ploc
149 d4107cf2 ploc
  end
150
  | "c" -> begin
151
    assert false (* not implemented yet *)
152
  end
153
  | _ -> assert false
154 22fe1c93 ploc
(* Local Variables: *)
155 cd670fe1 ploc
(* compile-command:"make -C ../../.." *)
156 22fe1c93 ploc
(* End: *)