Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ 990210f3

History | View | Annotate | Download (3.95 KB)

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
   This is a modified version that handles reset and automaton
16
*)
17 b701409d tkahsai
18
open Format
19
open LustreSpec
20
open Corelang
21
open Machine_code
22
23 fea041c5 xthirioux
open Horn_backend_common
24
open Horn_backend_printers
25
open Horn_backend_collecting_sem
26 b701409d tkahsai
27 fea041c5 xthirioux
(*
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 b701409d tkahsai
*)
35 af5af1e8 ploc
36 5cf953ec tkahsai
let main_print machines fmt =
37
if !Options.main_node <> "" then
38 af5af1e8 ploc
  begin
39
    let node = !Options.main_node in
40
    let machine = get_machine machines node in
41 43aa67ec tkahsai
    if !Options.horn_cex then(
42
      cex_computation machines fmt node machine;
43
      get_cex machines fmt node machine)
44 fea041c5 xthirioux
    else (
45
      collecting_semantics machines fmt node machine;
46
      check_prop machines fmt node machine;
47
    )
48 20e9de2d ploc
end
49
50 2dd3d358 Teme
51
let load_file f =
52
  let ic = open_in f in
53
  let n = in_channel_length ic in
54 bde99c3f xavier.thirioux
  let s = Bytes.create n in
55 2dd3d358 Teme
  really_input ic s 0 n;
56
  close_in ic;
57
  (s)
58
59 fea041c5 xthirioux
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 dcbf9d3a ploc
79 2dd3d358 Teme
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 990210f3 ploc
      let basename = (Options.name_dependency (local, s)) ^ ".smt2" in
89 2dd3d358 Teme
      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 1b57e111 Teme
let check_sfunction mannot =
96
 (*Check if its an sfunction*)
97
  match mannot with
98
    [] -> false
99 d128bbd4 Teme
  | [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 1b57e111 Teme
114 2dd3d358 Teme
let translate fmt basename prog machines=
115 fea041c5 xthirioux
  (* We print typedef *)
116 1b57e111 Teme
  print_dep fmt prog; (*print static library e.g. math*)
117 fea041c5 xthirioux
  print_type_definitions fmt;
118 1b57e111 Teme
  (*List.iter (print_machine machines fmt) (List.rev machines);*)
119
  List.iter(fun m ->
120
      let is_sfunction = check_sfunction m.mannot in
121
      if is_sfunction then(
122
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. detected sfunction: %s@," m.mname.node_id);
123
        print_sfunction machines fmt m
124
      ) else (
125
         print_machine machines fmt m)
126
         )
127
           (List.rev machines);
128 5cf953ec tkahsai
  main_print machines fmt
129 dcbf9d3a ploc
130
(* Local Variables: *)
131 3ca6d126 ploc
(* compile-command:"make -C ../.." *)
132 dcbf9d3a ploc
(* End: *)