Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/backends/Horn/horn_backend_collecting_sem.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 handle reset
16
*)
15
   This is a modified version that handle reset *)
17 16

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

  
22 20
open Horn_backend_common
23 21
open Horn_backend_printers
24 22

  
......
29 27
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
30 28
  in
31 29
  let main_output_dummy =
32
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
30
    rename_machine_list
31
      ("dummy" ^ machine.mname.node_id)
32
      machine.mstep.step_outputs
33 33
  in
34 34
  let main_memory_next =
35
    (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
36
      main_output
35
    rename_next_list
36
      (* machine.mname.node_id *)
37
      (full_memory_vars machines machine)
38
    @ main_output
37 39
  in
38 40
  let main_memory_current =
39
    (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
40
      main_output_dummy
41
    rename_current_list
42
      (* machine.mname.node_id *)
43
      (full_memory_vars machines machine)
44
    @ main_output_dummy
41 45
  in
42 46

  
43 47
  fprintf fmt "(declare-rel MAIN (%a))@."
44 48
    (Utils.fprintf_list ~sep:" " pp_type)
45 49
    (List.map (fun v -> v.var_type) main_memory_next);
46 50

  
47
  
48 51
  (* Init case *)
49
  let _ = 
52
  let _ =
50 53
    (* Special case when the main node is stateless *)
51 54
    if Machine_code_common.is_stateless machine then (
52 55
      let step_name = pp_machine_stateless_name in
......
55 58
      fprintf fmt "(rule INIT_STATE)@.";
56 59
      fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
57 60
      fprintf fmt "INIT_STATE@ ";
58
      fprintf fmt "(@[<v 0>%a %a@])"
59
	step_name node
60
	(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);    
61
      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);
61 64
      fprintf fmt "@]@ )@ ";
62 65
      fprintf fmt "(MAIN %a)@]@.))@.@."
63
	(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ;
64
    )
65
    else (
66
      let reset_name, step_name =
67
	pp_machine_reset_name, pp_machine_step_name
68
      in
66
        (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
69 70
      fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @.";
70 71
      fprintf fmt "(declare-rel INIT_STATE ())@.";
71 72
      fprintf fmt "(rule INIT_STATE)@.";
72 73
      fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
73 74
      fprintf fmt "INIT_STATE@ ";
74
      fprintf fmt "(@[<v 0>%a %a@])@ "
75
	reset_name node
76
	(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
77
      fprintf fmt "(@[<v 0>%a %a@])"
78
	step_name node
79
	(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
80
      
75
      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

  
81 82
      fprintf fmt "@]@ )@ ";
82 83
      fprintf fmt "(MAIN %a)@]@.))@.@."
83
	(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ;
84
    )
84
        (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
85
        main_memory_next
85 86
  in
86 87

  
87
  let step_name = 
88
    if Machine_code_common.is_stateless machine then 
89
      pp_machine_stateless_name
90
    else
91
      pp_machine_step_name
88
  let step_name =
89
    if Machine_code_common.is_stateless machine then pp_machine_stateless_name
90
    else pp_machine_step_name
92 91
  in
93
  
92

  
94 93
  fprintf fmt "; Inductive def@.";
95
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
94
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v))
95
    fmt main_output_dummy;
96 96
  fprintf fmt
97
    "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
98
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current
99
    step_name node
100
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
101
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
102

  
97
    "@[<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
103 105

  
104 106
let check_prop machines fmt machine =
105 107
  let main_output =
106 108
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
107 109
  in
108 110
  let main_memory_next =
109
    (rename_next_list (full_memory_vars machines machine)) @ main_output
111
    rename_next_list (full_memory_vars machines machine) @ main_output
110 112
  in
111 113
  fprintf fmt "; Property def@.";
112 114
  fprintf fmt "(declare-rel ERR ())@.";
113 115
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
114
    (pp_conj (pp_horn_var machine)) main_output
115
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
116
    ;
117
   if !Options.horn_query then fprintf fmt "(query ERR)@."
118

  
116
    (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)@."
119 121

  
120 122
let cex_computation machines fmt node machine =
121 123
  fprintf fmt "; CounterExample computation for node %s@.@." node;
122
    (* We print the types of the cex node "memory tree" TODO: add the output *)
124
  (* We print the types of the cex node "memory tree" TODO: add the output *)
123 125
  let cex_input =
124 126
    rename_machine_list machine.mname.node_id machine.mstep.step_inputs
125 127
  in
126 128
  let cex_input_dummy =
127
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
129
    rename_machine_list
130
      ("dummy" ^ machine.mname.node_id)
131
      machine.mstep.step_inputs
128 132
  in
129 133
  let cex_output =
130 134
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
131 135
  in
132 136
  let cex_output_dummy =
133
    rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
137
    rename_machine_list
138
      ("dummy" ^ machine.mname.node_id)
139
      machine.mstep.step_outputs
134 140
  in
135 141
  let cex_memory_next =
136
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
142
    cex_input
143
    @ rename_next_list (full_memory_vars machines machine)
144
    @ cex_output
137 145
  in
138 146
  let cex_memory_current =
139
    cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
147
    cex_input_dummy
148
    @ rename_current_list (full_memory_vars machines machine)
149
    @ cex_output_dummy
140 150
  in
141 151

  
142
    (* Special case when the cex node is stateless *)
152
  (* Special case when the cex node is stateless *)
143 153
  let reset_name, step_name =
144 154
    if Machine_code_common.is_stateless machine then
145 155
      pp_machine_stateless_name, pp_machine_stateless_name
146
    else
147
      pp_machine_reset_name, pp_machine_step_name
156
    else pp_machine_reset_name, pp_machine_step_name
148 157
  in
149 158

  
150 159
  fprintf fmt "(declare-rel CEX (Int %a))@.@."
......
156 165
  fprintf fmt "(rule INIT_STATE_CEX)@.";
157 166
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>";
158 167
  fprintf fmt "INIT_STATE_CEX@ ";
159
  fprintf fmt "(@[<v 0>%a %a@])@ "
160
    reset_name node
161
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine);
162
  fprintf fmt "(@[<v 0>%a %a@])"
163
    step_name node
164
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine);
165
  
168
  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

  
166 175
  fprintf fmt "@]@ )@ ";
167 176
  fprintf fmt "(CEX 0 %a)@]@.))@.@."
168
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next ;
177
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine))
178
    cex_memory_next;
169 179

  
170 180
  fprintf fmt "; Inductive def@.";
171
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
172
  (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
181
  (* 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;
173 185
  fprintf fmt "(declare-var cexcpt Int)@.";
174 186
  fprintf fmt
175
    "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
176
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_current
177
    step_name node
178
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
179
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
187
    "@[<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
180 195

  
181 196
let get_cex machines fmt machine =
182
    let cex_input =
183
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
184
    in
185
    let cex_output =
186
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
187
    in
197
  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
188 203
  let cex_memory_next =
189
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
204
    cex_input
205
    @ rename_next_list (full_memory_vars machines machine)
206
    @ cex_output
190 207
  in
191 208
  fprintf fmt "; Property def@.";
192 209
  fprintf fmt "(declare-rel CEXTRACE ())@.";
193
  fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
194
    (pp_conj (pp_horn_var machine)) cex_output
195
    (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
196
    ;
210
  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;
197 216
  fprintf fmt "(query CEXTRACE)@."
198 217

  
199 218
(* Local Variables: *)

Also available in: Unified diff