Project

General

Profile

Download (3.22 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

    
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 = String.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 translate fmt basename prog machines=
97
  (* We print typedef *)
98
  print_dep fmt prog;
99
  print_type_definitions fmt;
100
  List.iter (print_machine machines fmt) (List.rev machines);
101
  main_print machines fmt
102

    
103
(* Local Variables: *)
104
(* compile-command:"make -C ../.." *)
105
(* End: *)
(1-1/5)