Project

General

Profile

Revision 62f65f02 src/backends/Horn/horn_backend.ml

View differences:

src/backends/Horn/horn_backend.ml
65 65
let get_machine machines node_name =
66 66
  List.find (fun m  -> m.mname.node_id = node_name) machines
67 67

  
68

  
68 69
let full_memory_vars machines machine =
69 70
  let rec aux fst prefix m =
70 71
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
......
77 78
  in
78 79
  aux true machine.mname.node_id machine
79 80

  
81

  
80 82
let stateless_vars machines m =
81 83
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
82 84
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
......
338 340
       (*   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); *)
339 341

  
340 342

  
341
        (* Adding assertions *)
343
      (* Adding assertions *)
342 344
       (match m.mstep.step_asserts with
343 345
       | [] ->
344 346
          begin
347
            (* Rule for init *)
348
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
349
	                   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
350
	                   pp_machine_init_name m.mname.node_id
351
	                   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
352
            (* Rule for step*)
345 353
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
346 354
                           (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
347 355
                           pp_machine_step_name m.mname.node_id
......
349 357
          end
350 358
       | assertsl ->
351 359
          begin
352

  
353 360
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
354 361
            (* print_string pp_val; *)
355 362
            let instrs_concat = m.mstep.step_instrs in
356
            Format.fprintf fmt "; with Invariants @.";
363
            Format.fprintf fmt "; with Assertions @.";
364
            (*Rule for init*)
365
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
366
                           (pp_conj (pp_instr true m.mname.node_id)) instrs_concat
367
                           (pp_conj pp_val) assertsl
368
                           pp_machine_init_name m.mname.node_id
369
                           (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
370
            (*Rule for step*)
357 371
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
358 372
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
359 373
                           (pp_conj pp_val) assertsl
360 374
                           pp_machine_step_name m.mname.node_id
361 375
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
362

  
363

  
364 376
	    (* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *)
365 377
            (*                 (pp_conj pp_val) assertsl; *)
366 378

  
367 379
          end
368 380
       );
369 381

  
370
       (* (\* Adding assertions *\) *)
371
       (* (match m.mstep.step_asserts with *)
372
       (* | [] -> () *)
373
       (* | assertsl -> begin *)
374
       (*   let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in *)
375

  
376
       (*   Format.fprintf fmt "; Asserts@."; *)
377
       (*   Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@." *)
378
       (*     (pp_conj pp_val) assertsl; *)
379

  
380
       (*   (\** TEME: the following code is the one we described. But it generates a segfault in z3 *)
381
       (*   Format.fprintf fmt "; Asserts for init@."; *)
382
       (*   Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@." *)
383
       (*     (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs *)
384
       (*     pp_machine_init_name m.mname.node_id *)
385
       (*     (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m) *)
386
       (*     (pp_conj pp_val) assertsl; *)
387

  
388
       (*   Format.fprintf fmt "; Asserts for step@."; *)
389
       (*   Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@." *)
390
       (*     (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs *)
391

  
392
       (*     pp_machine_step_name m.mname.node_id *)
393
       (*     (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m) *)
394
       (*     (pp_conj pp_val) assertsl *)
395
       (*   *\) *)
396
       (* end *)
397
       (* ); *)
398

  
399
(*
400
       match m.mspec with
401
	 None -> () (* No node spec; we do nothing *)
402
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
403
	 (
404
       (* For the moment, we only deal with simple case: single ensures, no other parameters *)
405
	   ()
406 382

  
407
	 )
408
       | _ -> () (* Other cases give nothing *)
409
*)
410 383
     end
411 384
    end
412 385

  
......
472 445
    (pp_conj pp_var) main_output
473 446
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
474 447
    ;
475
  if !Options.horn_queries then
476
    Format.fprintf fmt "(query ERR)@."
448
   Format.fprintf fmt "(query ERR)@."
477 449

  
478 450

  
479 451
let cex_computation machines fmt node machine =
......
543 515
    (pp_conj pp_var) cex_output
544 516
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
545 517
    ;
546
  if !Options.horn_queries then
547
    Format.fprintf fmt "(query CEXTRACE)@."
518
  Format.fprintf fmt "(query CEXTRACE)@."
548 519

  
549 520

  
550 521
let main_print machines fmt =

Also available in: Unified diff