Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/backends/Horn/horn_backend.ml
12 12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13 13
   Kahsai, HCSV'14.
14 14

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

  
18 17
open Format
19 18
open Lustre_types
20 19
open Corelang
21 20
open Machine_code_types
22

  
23 21
open Horn_backend_common
24 22
open Horn_backend_printers
25 23
open Horn_backend_collecting_sem
26 24

  
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
*)
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 ) *)
35 30

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

  
40
      check_prop machines fmt machine)
50 41

  
51 42
let load_file f =
52 43
  let ic = open_in f in
......
58 49

  
59 50
let print_type_definitions fmt =
60 51
  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

  
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
80 71

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

  
95 89
let check_sfunction mannot =
96
 (*Check if its an sfunction*)
90
  (*Check if its an sfunction*)
97 91
  match mannot with
98
    [] -> false
99
  | [x] ->
100
     begin
101
       match x.annots with
102
         [] -> false
103
        |[(key, _)] ->
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
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
113 110

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

  
139 141
(* Local Variables: *)

Also available in: Unified diff