Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ 97d3f81a

History | View | Annotate | Download (13.3 KB)

1
	 m.mstep.step_instrs
2
	 pp_machine_stateless_name m.mname.node_id
3
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
4
     end
5
   else
6
     begin
7
       (* Declaring predicate *)
8
       Format.fprintf fmt "(declare-rel %a (%a))@."
9
	 pp_machine_init_name m.mname.node_id
10
	 (Utils.fprintf_list ~sep:" " pp_type)
11
	 (List.map (fun v -> v.var_type) (init_vars machines m));
12

    
13
       Format.fprintf fmt "(declare-rel %a (%a))@."
14
	 pp_machine_step_name m.mname.node_id
15
	 (Utils.fprintf_list ~sep:" " pp_type)
16
	 (List.map (fun v -> v.var_type) (step_vars machines m));
17

    
18
       Format.pp_print_newline fmt ();
19

    
20
       (* Rule for init *)
21
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
22
	 (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
23
	 pp_machine_init_name m.mname.node_id
24
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
25

    
26
       (* (\* Rule for step *\) *)
27
       (* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
28
       (*   (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs *)
29
       (*   pp_machine_step_name m.mname.node_id *)
30
       (*   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); *)
31

    
32

    
33
      (* Adding assertions *)
34
       (match m.mstep.step_asserts with
35
       | [] ->
36
          begin
37
            (* Rule for init *)
38
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
39
	                   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
40
	                   pp_machine_init_name m.mname.node_id
41
	                   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
42
            (* Rule for step*)
43
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
44
                           (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
45
                           pp_machine_step_name m.mname.node_id
46
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
47
          end
48
       | assertsl ->
49
          begin
50
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
51
            (* print_string pp_val; *)
52
            let instrs_concat = m.mstep.step_instrs in
53
            Format.fprintf fmt "; with Assertions @.";
54
            (*Rule for init*)
55
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
56
                           (pp_conj (pp_instr true m.mname.node_id)) instrs_concat
57
                           (pp_conj pp_val) assertsl
58
                           pp_machine_init_name m.mname.node_id
59
                           (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
60
            (*Rule for step*)
61
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
62
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
63
                           (pp_conj pp_val) assertsl
64
                           pp_machine_step_name m.mname.node_id
65
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
66
	    (* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *)
67
            (*                 (pp_conj pp_val) assertsl; *)
68

    
69
          end
70
       );
71

    
72

    
73
     end
74
    end
75

    
76

    
77

    
78
let collecting_semantics machines fmt node machine =
79
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
80
    (* We print the types of the main node "memory tree" TODO: add the output *)
81
    let main_output =
82
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
83
    in
84
    let main_output_dummy =
85
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
86
    in
87
    let main_memory_next =
88
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
89
      main_output
90
    in
91
    let main_memory_current =
92
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
93
      main_output_dummy
94
    in
95

    
96
    (* Special case when the main node is stateless *)
97
    let init_name, step_name =
98
      if is_stateless machine then
99
	pp_machine_stateless_name, pp_machine_stateless_name
100
      else
101
	pp_machine_init_name, pp_machine_step_name
102
    in
103

    
104
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
105
      (Utils.fprintf_list ~sep:" " pp_type)
106
      (List.map (fun v -> v.var_type) main_memory_next);
107

    
108
    Format.fprintf fmt "; Initial set@.";
109
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
110
    Format.fprintf fmt "(rule INIT_STATE)@.";
111
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
112
      init_name node
113
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
114
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
115

    
116
    Format.fprintf fmt "; Inductive def@.";
117
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
118
    Format.fprintf fmt
119
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
120
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
121
      step_name node
122
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
123
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
124

    
125
let check_prop machines fmt node machine =
126
  let main_output =
127
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
128
  in
129
  let main_memory_next =
130
    (rename_next_list (full_memory_vars machines machine)) @ main_output
131
  in
132
  Format.fprintf fmt "; Property def@.";
133
  Format.fprintf fmt "(declare-rel ERR ())@.";
134
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
135
    (pp_conj pp_var) main_output
136
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
137
    ;
138
   Format.fprintf fmt "(query ERR)@."
139

    
140

    
141
let cex_computation machines fmt node machine =
142
    Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
143
    (* We print the types of the cex node "memory tree" TODO: add the output *)
144
    let cex_input =
145
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
146
    in
147
    let cex_input_dummy =
148
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
149
    in
150
    let cex_output =
151
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
152
    in
153
    let cex_output_dummy =
154
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
155
    in
156
    let cex_memory_next =
157
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
158
    in
159
    let cex_memory_current =
160
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
161
    in
162

    
163
    (* Special case when the cex node is stateless *)
164
    let init_name, step_name =
165
      if is_stateless machine then
166
	pp_machine_stateless_name, pp_machine_stateless_name
167
      else
168
	pp_machine_init_name, pp_machine_step_name
169
    in
170

    
171
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
172
      (Utils.fprintf_list ~sep:" " pp_type)
173
      (List.map (fun v -> v.var_type) cex_memory_next);
174

    
175
    Format.fprintf fmt "; Initial set@.";
176
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
177
      init_name node
178
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
179
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
180

    
181
    Format.fprintf fmt "; Inductive def@.";
182
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
183
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
184
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
185
    Format.fprintf fmt
186
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
187
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
188
      step_name node
189
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
190
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
191

    
192
let get_cex machines fmt node machine =
193
    let cex_input =
194
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
195
    in
196
    let cex_output =
197
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
198
    in
199
  let cex_memory_next =
200
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
201
  in
202
  Format.fprintf fmt "; Property def@.";
203
  Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
204
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
205
    (pp_conj pp_var) cex_output
206
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
207
    ;
208
  Format.fprintf fmt "(query CEXTRACE)@."
209

    
210

    
211
let main_print machines fmt =
212
if !Options.main_node <> "" then
213
  begin
214
    let node = !Options.main_node in
215
    let machine = get_machine machines node in
216

    
217

    
218
    collecting_semantics machines fmt node machine;
219
    check_prop machines fmt node machine;
220
    if !Options.horn_cex then(
221
      cex_computation machines fmt node machine;
222
      get_cex machines fmt node machine)
223
end
224

    
225

    
226
let translate fmt basename prog machines =
227
  List.iter (print_machine machines fmt) (List.rev machines);
228
  main_print machines fmt
229

    
230

    
231
let traces_file fmt basename prog machines =
232
  Format.fprintf fmt
233
    "; Horn code traceability generated by %s@.; SVN version number %s@.@."
234
    (Filename.basename Sys.executable_name)
235
    Version.number;
236

    
237
  (* We extract the annotation dealing with traceability *)
238
  let machines_traces = List.map (fun m ->
239
    let traces : (ident * expr) list=
240
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
241
      let filtered =
242
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
243
      in
244
      let content = List.map snd filtered in
245
      (* Elements are supposed to be a pair (tuple): variable, expression *)
246
      List.map (fun ee ->
247
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
248
	| [], Expr_tuple [v;e] -> (
249
	  match v.expr_desc with
250
	  | Expr_ident vid -> vid, e
251
	  | _ -> assert false )
252
	| _ -> assert false)
253
	content
254
    in
255

    
256
    m, traces
257

    
258
  ) machines
259
  in
260

    
261
  (* Compute memories associated to each machine *)
262
  let compute_mems m =
263
    let rec aux fst prefix m =
264
      (List.map (fun mem -> (prefix, mem)) m.mmemory) @
265
	List.fold_left (fun accu (id, (n, _)) ->
266
	  let name = node_name n in
267
	  if name = "_arrow" then accu else
268
	    let machine_n = get_machine machines name in
269
	    ( aux false ((id,machine_n)::prefix) machine_n )
270
	    @ accu
271
	) [] m.minstances
272
    in
273
    aux true [] m
274
  in
275

    
276
  List.iter (fun m ->
277
    Format.fprintf fmt "; Node %s@." m.mname.node_id;
278

    
279
    let memories_old =
280
      List.map (fun (p, v) ->
281
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
282
	let traces = List.assoc machine machines_traces in
283
	if List.mem_assoc v.var_id traces then (
284
	  (* We take the expression associated to variable v in the trace info *)
285
	  (* Format.eprintf "Found variable %a in traces: %a@."  pp_var v Printers.pp_expr (List.assoc v.var_id traces); *)
286
	  p, List.assoc v.var_id traces
287
      )
288
	else (
289
	  (* We keep the variable as is: we create an expression v *)
290
	  (* Format.eprintf "Unable to found variable %a in traces (%a)@."  pp_var v (Utils.fprintf_list ~sep:", " Format.pp_print_string) (List.map fst traces); *)
291
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
292
	)
293

    
294
      ) (compute_mems m)
295
    in
296
    let memories_next = (* We remove the topest pre in each expression *)
297
      List.map
298
      	(fun (prefix, ee) ->
299
      	  match ee.expr_desc with
300
      	  | Expr_pre e -> prefix, e
301
      	  | _ -> Format.eprintf
302
      	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
303
      	    (Utils.fprintf_list ~sep:","
304
      	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
305
      	    (List.rev prefix)
306
      	    Printers.pp_expr ee;
307
      	    assert false)
308
	memories_old
309
    in
310

    
311
    let pp_prefix_rev fmt prefix =
312
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
313
    in
314

    
315
    Format.fprintf fmt "; Init predicate@.";
316

    
317
    Format.fprintf fmt "; horn encoding@.";
318
    Format.fprintf fmt "(%a %a)@."
319
      pp_machine_init_name m.mname.node_id
320
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
321

    
322
    Format.fprintf fmt "; original expressions@.";
323
    Format.fprintf fmt "(%a %a%t%a)@."
324
      pp_machine_init_name m.mname.node_id
325
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
326
      (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ")
327
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next;
328

    
329
    Format.pp_print_newline fmt ();
330
    Format.fprintf fmt "; Step predicate@.";
331

    
332
    Format.fprintf fmt "; horn encoding@.";
333
    Format.fprintf fmt "(%a %a)@."
334
      pp_machine_step_name m.mname.node_id
335
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
336
    Format.fprintf fmt "; original expressions@.";
337
    Format.fprintf fmt "(%a %a%t%a)@."
338
      pp_machine_step_name m.mname.node_id
339
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
340
      (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
341
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
342
    Format.pp_print_newline fmt ();
343
  ) (List.rev machines);
344

    
345

    
346
(* Local Variables: *)
347
(* compile-command:"make -C ../.." *)
348
(* End: *)