Project

General

Profile

Download (4.36 KB) Statistics
| Branch: | Tag: | Revision:
1 b701409d tkahsai
(********************************************************************)
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 fea041c5 xthirioux
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14
15 ca7ff3f7 Lélio Brun
   This is a modified version that handles reset and automaton *)
16 b701409d tkahsai
17
open Format
18 8446bf03 ploc
open Lustre_types
19 b701409d tkahsai
open Corelang
20 089f94be ploc
open Machine_code_types
21 fea041c5 xthirioux
open Horn_backend_common
22
open Horn_backend_printers
23
open Horn_backend_collecting_sem
24 b701409d tkahsai
25 ca7ff3f7 Lélio Brun
(* TODO: - gerer les traces. Ca merde pour l'instant dans le calcul des memoires
26
   sur les arrows - gerer le reset --- DONE - reconstruire les rechable states
27
   DONE - reintroduire le cex/traces ... DONE - traiter les types enum et les
28
   branchements sur ces types enum (en particulier les traitements des resets
29
   qui ont lieu dans certaines branches et pas dans d'autres ) *)
30 af5af1e8 ploc
31 5cf953ec tkahsai
let main_print machines fmt =
32 ca7ff3f7 Lélio Brun
  if !Options.main_node <> "" then
33 af5af1e8 ploc
    let node = !Options.main_node in
34
    let machine = get_machine machines node in
35 ca7ff3f7 Lélio Brun
    if !Options.horn_cex then (
36 43aa67ec tkahsai
      cex_computation machines fmt node machine;
37 ca7e8027 Lélio Brun
      get_cex machines fmt machine)
38 fea041c5 xthirioux
    else (
39
      collecting_semantics machines fmt node machine;
40 ca7ff3f7 Lélio Brun
      check_prop machines fmt machine)
41 2dd3d358 Teme
42
let load_file f =
43
  let ic = open_in f in
44
  let n = in_channel_length ic in
45 bde99c3f xavier.thirioux
  let s = Bytes.create n in
46 2dd3d358 Teme
  really_input ic s 0 n;
47
  close_in ic;
48 185ddf4d ploc
  Bytes.to_string s
49 2dd3d358 Teme
50 fea041c5 xthirioux
let print_type_definitions fmt =
51
  let cpt_type = ref 0 in
52 ca7ff3f7 Lélio Brun
  Hashtbl.iter
53
    (fun typ decl ->
54
      match typ with
55
      | Tydec_const var -> (
56
        match decl.top_decl_desc with
57
        | TypeDef tdef -> (
58
          match tdef.tydef_desc with
59
          | Tydec_enum tl ->
60
            incr cpt_type;
61
            fprintf fmt "(declare-datatypes () ((%s %a)));@.@." var
62
              (Utils.fprintf_list ~sep:" " pp_print_string)
63
              tl
64
          | _ ->
65
            assert false)
66
        | _ ->
67
          assert false)
68
      | _ ->
69
        ())
70
    type_table
71 2dd3d358 Teme
72
let print_dep fmt prog =
73 ca7ff3f7 Lélio Brun
  Log.report ~level:1 (fun fmt ->
74
      fprintf fmt "@[<v 2>.. extracting Horn libraries@,");
75 5d08c49e ploc
  fprintf fmt "; Statically linked libraries@,";
76 2dd3d358 Teme
  let dependencies = Corelang.get_dependencies prog in
77
  List.iter
78
    (fun dep ->
79 ca7ff3f7 Lélio Brun
      let local, s = Corelang.dependency_of_top dep in
80
      let basename =
81
        Options_management.name_dependency (local, s) ".lusic" ^ ".smt2"
82
      in
83
      Log.report ~level:1 (fun fmt ->
84
          Format.fprintf fmt "@[<v 0> Horn Library %s@," basename);
85 2dd3d358 Teme
      let horn = load_file basename in
86 ca7ff3f7 Lélio Brun
      fprintf fmt "@.%s@." horn)
87 2dd3d358 Teme
    dependencies
88
89 1b57e111 Teme
let check_sfunction mannot =
90 ca7ff3f7 Lélio Brun
  (*Check if its an sfunction*)
91 1b57e111 Teme
  match mannot with
92 ca7ff3f7 Lélio Brun
  | [] ->
93
    false
94
  | [ x ] -> (
95
    match x.annots with
96
    | [] ->
97
      false
98
    | [ (key, _) ] -> (
99
      match key with
100
      | [] ->
101
        false
102
      | [ x ] ->
103
        x == "c_code" || x == "matlab"
104
      | _ ->
105
        false)
106
    | (_, _) :: _ ->
107
      false)
108
  | _ :: _ ->
109
    false
110 1b57e111 Teme
111 a6974c82 ploc
let preprocess machines =
112 ca7ff3f7 Lélio Brun
  List.fold_right
113
    (fun m res ->
114
      if List.mem m.mname.node_id registered_keywords then
115
        {
116
          m with
117
          mname = { m.mname with node_id = protect_kwd m.mname.node_id };
118
        }
119
        :: res
120
      else m :: res)
121
    machines []
122
123
let translate fmt prog machines =
124 a6974c82 ploc
  let machines = preprocess machines in
125 fea041c5 xthirioux
  (* We print typedef *)
126 ca7ff3f7 Lélio Brun
  print_dep fmt prog;
127
  (*print static library e.g. math*)
128 fea041c5 xthirioux
  print_type_definitions fmt;
129 1b57e111 Teme
  (*List.iter (print_machine machines fmt) (List.rev machines);*)
130 ca7ff3f7 Lélio Brun
  List.iter
131
    (fun m ->
132 1b57e111 Teme
      let is_sfunction = check_sfunction m.mannot in
133 ca7ff3f7 Lélio Brun
      if is_sfunction then (
134
        Log.report ~level:1 (fun fmt ->
135
            fprintf fmt ".. detected sfunction: %s@," m.mname.node_id);
136
        print_sfunction machines fmt m)
137
      else print_machine machines fmt m)
138
    (List.rev machines);
139 5cf953ec tkahsai
  main_print machines fmt
140 dcbf9d3a ploc
141
(* Local Variables: *)
142 3ca6d126 ploc
(* compile-command:"make -C ../.." *)
143 dcbf9d3a ploc
(* End: *)