Project

General

Profile

Revision ff2d7a82

View differences:

src/tools/zustre_verifier.ml
20 20
let active = ref false
21 21
let ctx = ref (Z3.mk_context [])
22 22
let machine_reset_name = HBC.machine_reset_name 
23
let machine_stateless_name = HBC.machine_stateless_name 
23 24

  
24 25
(** Sorts
25 26

  
......
415 416
             (get_fdecl (machine_step_name (node_name n)))
416 417
             ( (* Arguments are input, output, mid_mems, next_mems *)
417 418
               (
418
                 List.map (horn_val_to_expr self (pp_horn_var m)) (
419
                 List.map (horn_val_to_expr self) (
419 420
                     inputs @
420 421
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
421 422
                   )
......
447 448
    
448 449

  
449 450
(* Convert instruction to Z3.Expr and update the set of reset instances *)
450
let rec instr_to_expr machines reset_instances (m: machine_t) instr : expr list * ident list =
451
  match get_instr_desc instr with
451
let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
452
  match Corelang.get_instr_desc instr with
452 453
  | MComment _ -> [], reset_instances
453 454
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
454 455
    no_reset_to_exprs machines m i,
......
511 512
  | [] -> [], reset_instances
512 513

  
513 514

  
515
let basic_library_to_horn_expr i vl =
516
  match i, vl with
517
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
518

  
519
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
520
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
521
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
522
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
523
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
524
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
525
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
526
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
527
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
528
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
529
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
530
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
531
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
532
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
533

  
534
*)
535

  
536
        
537
(* Prints a [value] indexed by the suffix list [loop_vars] *)
538
let rec value_suffix_to_expr self value =
539
 match value.value_desc with
540
 | Fun (n, vl)  -> 
541
   basic_library_to_horn_expr n (value_suffix_to_expr self vl)
542
 |  _            ->
543
   horn_val_to_expr self value
544

  
545
        
546
(* type_directed assignment: array vs. statically sized type
547
   - [var_type]: type of variable to be assigned
548
   - [var_name]: name of variable to be assigned
549
   - [value]: assigned value
550
   - [pp_var]: printer for variables
551
*)
552
let assign_to_exprs m var_name value =
553
  let self = m.mname.node_id in
554
  let e =
555
    Z3.Boolean.mk_eq
556
      !ctx
557
      (horn_val_to_expr ~is_lhs:true self var_name)
558
      (value_suffix_to_expr self value)
559
  in
560
  [e]
561

  
514 562
(*                TODO: empty list means true statement *)
515 563
let decl_machine machines m =
516 564
  if m.Machine_code.mname.node_id = Machine_code.arrow_id then

Also available in: Unified diff