Project

General

Profile

Download (4.36 KB) Statistics
| Branch: | Tag: | Revision:
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 was first defined in Garoche, Gurfinkel,
13
   Kahsai, HCSV'14.
14

    
15
   This is a modified version that handles reset and automaton *)
16

    
17
open Format
18
open Lustre_types
19
open Corelang
20
open Machine_code_types
21
open Horn_backend_common
22
open Horn_backend_printers
23
open Horn_backend_collecting_sem
24

    
25
(* 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

    
31
let main_print machines fmt =
32
  if !Options.main_node <> "" then
33
    let node = !Options.main_node in
34
    let machine = get_machine machines node in
35
    if !Options.horn_cex then (
36
      cex_computation machines fmt node machine;
37
      get_cex machines fmt machine)
38
    else (
39
      collecting_semantics machines fmt node machine;
40
      check_prop machines fmt machine)
41

    
42
let load_file f =
43
  let ic = open_in f in
44
  let n = in_channel_length ic in
45
  let s = Bytes.create n in
46
  really_input ic s 0 n;
47
  close_in ic;
48
  Bytes.to_string s
49

    
50
let print_type_definitions fmt =
51
  let cpt_type = ref 0 in
52
  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

    
72
let print_dep fmt prog =
73
  Log.report ~level:1 (fun fmt ->
74
      fprintf fmt "@[<v 2>.. extracting Horn libraries@,");
75
  fprintf fmt "; Statically linked libraries@,";
76
  let dependencies = Corelang.get_dependencies prog in
77
  List.iter
78
    (fun dep ->
79
      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
      let horn = load_file basename in
86
      fprintf fmt "@.%s@." horn)
87
    dependencies
88

    
89
let check_sfunction mannot =
90
  (*Check if its an sfunction*)
91
  match mannot with
92
  | [] ->
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

    
111
let preprocess machines =
112
  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
  let machines = preprocess machines in
125
  (* We print typedef *)
126
  print_dep fmt prog;
127
  (*print static library e.g. math*)
128
  print_type_definitions fmt;
129
  (*List.iter (print_machine machines fmt) (List.rev machines);*)
130
  List.iter
131
    (fun m ->
132
      let is_sfunction = check_sfunction m.mannot in
133
      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
  main_print machines fmt
140

    
141
(* Local Variables: *)
142
(* compile-command:"make -C ../.." *)
143
(* End: *)
(1-1/5)