Project

General

Profile

Download (7.8 KB) Statistics
| Branch: | Tag: | Revision:
1 0dee2bc1 ploc
(********************************************************************)
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 ca7ff3f7 Lélio Brun
   This is a modified version that handle reset *)
16 0dee2bc1 ploc
17
open Format
18 8446bf03 ploc
open Lustre_types
19 089f94be ploc
open Machine_code_types
20 0dee2bc1 ploc
open Horn_backend_common
21
open Horn_backend_printers
22
23
let collecting_semantics machines fmt node machine =
24
  fprintf fmt "; Collecting semantics for node %s@.@." node;
25
  (* We print the types of the main node "memory tree" TODO: add the output *)
26
  let main_output =
27
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
28
  in
29
  let main_output_dummy =
30 ca7ff3f7 Lélio Brun
    rename_machine_list
31
      ("dummy" ^ machine.mname.node_id)
32
      machine.mstep.step_outputs
33 0dee2bc1 ploc
  in
34
  let main_memory_next =
35 ca7ff3f7 Lélio Brun
    rename_next_list
36
      (* machine.mname.node_id *)
37
      (full_memory_vars machines machine)
38
    @ main_output
39 0dee2bc1 ploc
  in
40
  let main_memory_current =
41 ca7ff3f7 Lélio Brun
    rename_current_list
42
      (* machine.mname.node_id *)
43
      (full_memory_vars machines machine)
44
    @ main_output_dummy
45 0dee2bc1 ploc
  in
46
47
  fprintf fmt "(declare-rel MAIN (%a))@."
48
    (Utils.fprintf_list ~sep:" " pp_type)
49
    (List.map (fun v -> v.var_type) main_memory_next);
50
51 07ceae4c ploc
  (* Init case *)
52 ca7ff3f7 Lélio Brun
  let _ =
53 07ceae4c ploc
    (* Special case when the main node is stateless *)
54 e4edf171 ploc
    if Machine_code_common.is_stateless machine then (
55 07ceae4c ploc
      let step_name = pp_machine_stateless_name in
56
      fprintf fmt "; Initial set: One Step(m,x)  -- Stateless node! @.";
57
      fprintf fmt "(declare-rel INIT_STATE ())@.";
58
      fprintf fmt "(rule INIT_STATE)@.";
59
      fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
60
      fprintf fmt "INIT_STATE@ ";
61 ca7ff3f7 Lélio Brun
      fprintf fmt "(@[<v 0>%a %a@])" step_name node
62
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
63
        (step_vars_m_x machines machine);
64 07ceae4c ploc
      fprintf fmt "@]@ )@ ";
65
      fprintf fmt "(MAIN %a)@]@.))@.@."
66 ca7ff3f7 Lélio Brun
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
67
        main_memory_next)
68
    else
69
      let reset_name, step_name = pp_machine_reset_name, pp_machine_step_name in
70 07ceae4c ploc
      fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
71
      fprintf fmt "(declare-rel INIT_STATE ())@.";
72
      fprintf fmt "(rule INIT_STATE)@.";
73
      fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
74
      fprintf fmt "INIT_STATE@ ";
75 ca7ff3f7 Lélio Brun
      fprintf fmt "(@[<v 0>%a %a@])@ " reset_name node
76
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
77
        (reset_vars machines machine);
78
      fprintf fmt "(@[<v 0>%a %a@])" step_name node
79
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
80
        (step_vars_m_x machines machine);
81
82 07ceae4c ploc
      fprintf fmt "@]@ )@ ";
83
      fprintf fmt "(MAIN %a)@]@.))@.@."
84 ca7ff3f7 Lélio Brun
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
85
        main_memory_next
86 07ceae4c ploc
  in
87 0dee2bc1 ploc
88 ca7ff3f7 Lélio Brun
  let step_name =
89
    if Machine_code_common.is_stateless machine then pp_machine_stateless_name
90
    else pp_machine_step_name
91 07ceae4c ploc
  in
92 ca7ff3f7 Lélio Brun
93 0dee2bc1 ploc
  fprintf fmt "; Inductive def@.";
94 ca7ff3f7 Lélio Brun
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v))
95
    fmt main_output_dummy;
96 0dee2bc1 ploc
  fprintf fmt
97 ca7ff3f7 Lélio Brun
    "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN \
98
     %a)@]@.))@.@."
99
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
100
    main_memory_current step_name node
101
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
102
    (step_vars machines machine)
103
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
104
    main_memory_next
105 0dee2bc1 ploc
106 ca7e8027 Lélio Brun
let check_prop machines fmt machine =
107 0dee2bc1 ploc
  let main_output =
108
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
109
  in
110
  let main_memory_next =
111 ca7ff3f7 Lélio Brun
    rename_next_list (full_memory_vars machines machine) @ main_output
112 0dee2bc1 ploc
  in
113
  fprintf fmt "; Property def@.";
114
  fprintf fmt "(declare-rel ERR ())@.";
115
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
116 ca7ff3f7 Lélio Brun
    (pp_conj (pp_horn_var machine))
117
    main_output
118
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
119
    main_memory_next;
120
  if !Options.horn_query then fprintf fmt "(query ERR)@."
121 0dee2bc1 ploc
122
let cex_computation machines fmt node machine =
123
  fprintf fmt "; CounterExample computation for node %s@.@." node;
124 ca7ff3f7 Lélio Brun
  (* We print the types of the cex node "memory tree" TODO: add the output *)
125 0dee2bc1 ploc
  let cex_input =
126
    rename_machine_list machine.mname.node_id machine.mstep.step_inputs
127
  in
128
  let cex_input_dummy =
129 ca7ff3f7 Lélio Brun
    rename_machine_list
130
      ("dummy" ^ machine.mname.node_id)
131
      machine.mstep.step_inputs
132 0dee2bc1 ploc
  in
133
  let cex_output =
134
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
135
  in
136
  let cex_output_dummy =
137 ca7ff3f7 Lélio Brun
    rename_machine_list
138
      ("dummy" ^ machine.mname.node_id)
139
      machine.mstep.step_outputs
140 0dee2bc1 ploc
  in
141
  let cex_memory_next =
142 ca7ff3f7 Lélio Brun
    cex_input
143
    @ rename_next_list (full_memory_vars machines machine)
144
    @ cex_output
145 0dee2bc1 ploc
  in
146
  let cex_memory_current =
147 ca7ff3f7 Lélio Brun
    cex_input_dummy
148
    @ rename_current_list (full_memory_vars machines machine)
149
    @ cex_output_dummy
150 0dee2bc1 ploc
  in
151
152 ca7ff3f7 Lélio Brun
  (* Special case when the cex node is stateless *)
153 0dee2bc1 ploc
  let reset_name, step_name =
154 e4edf171 ploc
    if Machine_code_common.is_stateless machine then
155 0dee2bc1 ploc
      pp_machine_stateless_name, pp_machine_stateless_name
156 ca7ff3f7 Lélio Brun
    else pp_machine_reset_name, pp_machine_step_name
157 0dee2bc1 ploc
  in
158
159
  fprintf fmt "(declare-rel CEX (Int %a))@.@."
160
    (Utils.fprintf_list ~sep:" " pp_type)
161
    (List.map (fun v -> v.var_type) cex_memory_next);
162
163
  fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
164
  fprintf fmt "(declare-rel INIT_STATE_CEX ())@.";
165
  fprintf fmt "(rule INIT_STATE_CEX)@.";
166
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
167
  fprintf fmt "INIT_STATE_CEX@ ";
168 ca7ff3f7 Lélio Brun
  fprintf fmt "(@[<v 0>%a %a@])@ " reset_name node
169
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
170
    (reset_vars machines machine);
171
  fprintf fmt "(@[<v 0>%a %a@])" step_name node
172
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
173
    (step_vars_m_x machines machine);
174
175 0dee2bc1 ploc
  fprintf fmt "@]@ )@ ";
176
  fprintf fmt "(CEX 0 %a)@]@.))@.@."
177 ca7ff3f7 Lélio Brun
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
178
    cex_memory_next;
179 0dee2bc1 ploc
180
  fprintf fmt "; Inductive def@.";
181 ca7ff3f7 Lélio Brun
  (* Declare dummy inputs. Outputs should have been declared previously with
182
     collecting sem *)
183
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v))
184
    fmt cex_input_dummy;
185 0dee2bc1 ploc
  fprintf fmt "(declare-var cexcpt Int)@.";
186
  fprintf fmt
187 ca7ff3f7 Lélio Brun
    "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ \
188
     (CEX (+ 1 cexcpt) %a)@]@.))@.@."
189
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
190
    cex_memory_current step_name node
191
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
192
    (step_vars machines machine)
193
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
194
    cex_memory_next
195 0dee2bc1 ploc
196 ca7e8027 Lélio Brun
let get_cex machines fmt machine =
197 ca7ff3f7 Lélio Brun
  let cex_input =
198
    rename_machine_list machine.mname.node_id machine.mstep.step_inputs
199
  in
200
  let cex_output =
201
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
202
  in
203 0dee2bc1 ploc
  let cex_memory_next =
204 ca7ff3f7 Lélio Brun
    cex_input
205
    @ rename_next_list (full_memory_vars machines machine)
206
    @ cex_output
207 0dee2bc1 ploc
  in
208
  fprintf fmt "; Property def@.";
209
  fprintf fmt "(declare-rel CEXTRACE ())@.";
210 ca7ff3f7 Lélio Brun
  fprintf fmt
211
    "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
212
    (pp_conj (pp_horn_var machine))
213
    cex_output
214
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
215
    cex_memory_next;
216 0dee2bc1 ploc
  fprintf fmt "(query CEXTRACE)@."
217
218
(* Local Variables: *)
219
(* compile-command:"make -C ../.." *)
220
(* End: *)