Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ bde99c3f

History | View | Annotate | Download (3.98 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

    
31
- gerer le reset --- DONE
32
- reconstruire les rechable states DONE
33
- reintroduire le cex/traces ... DONE
34
- 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 )
35
*)
36

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

    
51

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

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

    
79

    
80

    
81

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

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

    
115
let translate fmt basename prog machines=
116
  (* We print typedef *)
117
  print_dep fmt prog; (*print static library e.g. math*)
118
  print_type_definitions fmt;
119
  (*List.iter (print_machine machines fmt) (List.rev machines);*)
120
  List.iter(fun m ->
121
      let is_sfunction = check_sfunction m.mannot in
122
      if is_sfunction then(
123
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. detected sfunction: %s@," m.mname.node_id);
124
        print_sfunction machines fmt m
125
      ) else (
126
         print_machine machines fmt m)
127
         )
128
           (List.rev machines);
129
  main_print machines fmt
130

    
131
(* Local Variables: *)
132
(* compile-command:"make -C ../.." *)
133
(* End: *)