Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ 1bff14ac

History | View | Annotate | Download (4.24 KB)

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

    
18
open Format
19
open LustreSpec
20
open Corelang
21
open Machine_code
22

    
23
open Horn_backend_common
24
open Horn_backend_printers
25
open Horn_backend_collecting_sem
26

    
27
(*
28
TODO:
29
- gerer les traces. Ca merde pour l'instant dans le calcul des memoires sur les arrows
30
- gerer le reset --- DONE
31
- reconstruire les rechable states DONE
32
- reintroduire le cex/traces ... DONE
33
- traiter les types enum et les branchements sur ces types enum (en particulier les traitements des resets qui ont lieu dans certaines branches et pas dans d'autres )
34
*)
35

    
36
let main_print machines fmt =
37
if !Options.main_node <> "" then
38
  begin
39
    let node = !Options.main_node in
40
    let machine = get_machine machines node in
41
    if !Options.horn_cex then(
42
      cex_computation machines fmt node machine;
43
      get_cex machines fmt node machine)
44
    else (
45
      collecting_semantics machines fmt node machine;
46
      check_prop machines fmt node machine;
47
    )
48
end
49

    
50

    
51
let load_file f =
52
  let ic = open_in f in
53
  let n = in_channel_length ic in
54
  let s = Bytes.create n in
55
  really_input ic s 0 n;
56
  close_in ic;
57
  (s)
58

    
59
let print_type_definitions fmt =
60
  let cpt_type = ref 0 in
61
  Hashtbl.iter (fun typ decl ->
62
    match typ with
63
    | Tydec_const var ->
64
      (match decl.top_decl_desc with
65
      | TypeDef tdef -> (
66
	match tdef.tydef_desc with
67
	| Tydec_enum tl ->
68
	  incr cpt_type;
69
	  fprintf fmt "(declare-datatypes () ((%s %a)));@.@."
70
	    var
71
	    (Utils.fprintf_list ~sep:" " pp_print_string) tl
72
	| _ -> assert false
73
      )
74
      | _ -> assert false
75
      )
76
    | _        -> ()) type_table
77

    
78

    
79

    
80

    
81
let print_dep fmt prog =
82
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting Horn libraries@,");
83
  fprintf fmt "; Statically linked libraries@,";
84
  let dependencies = Corelang.get_dependencies prog in
85
  List.iter
86
    (fun dep ->
87
      let (local, s) = Corelang.dependency_of_top dep in
88
      let basename = (Options_management.name_dependency (local, s)) ^ ".smt2" in
89
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename);
90
      let horn = load_file basename in
91
      fprintf fmt "@.%s@." horn;
92
    )
93
    dependencies
94

    
95
let check_sfunction mannot =
96
 (*Check if its an sfunction*)
97
  match mannot with
98
    [] -> false
99
  | [x] ->
100
     begin
101
       match x.annots with
102
         [] -> false
103
        |[(key,va)] ->
104
          begin
105
            match key with
106
              [] -> false
107
            | [x]  -> x == "c_code" || x =="matlab"
108
            | _ -> false
109
          end
110
        |(_,_)::_ -> false
111
     end
112
  | _::_ -> false
113

    
114
let preprocess machines =
115
  List.fold_right (fun m res ->
116
    if List.mem m.mname.node_id registered_keywords then
117
      { m with mname  = { m.mname with node_id = protect_kwd m.mname.node_id }}::res
118
       else
119
	m :: res
120
  ) machines []
121
     
122
let translate fmt basename prog machines=
123
  let machines = preprocess machines in
124
  (* We print typedef *)
125
  print_dep fmt prog; (*print static library e.g. math*)
126
  print_type_definitions fmt;
127
  (*List.iter (print_machine machines fmt) (List.rev machines);*)
128
  List.iter(fun m ->
129
      let is_sfunction = check_sfunction m.mannot in
130
      if is_sfunction then(
131
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. detected sfunction: %s@," m.mname.node_id);
132
        print_sfunction machines fmt m
133
      ) else (
134
         print_machine machines fmt m)
135
         )
136
           (List.rev machines);
137
  main_print machines fmt
138

    
139
(* Local Variables: *)
140
(* compile-command:"make -C ../.." *)
141
(* End: *)