Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre_verifier.ml @ ad4774b0

History | View | Annotate | Download (5.57 KB)

1
open LustreSpec
2
open Machine_code
3
open Format
4
open Horn_backend_common
5
open Horn_backend
6
   
7
let active = ref false
8
let ctx = ref (Z3.mk_context [])
9

    
10
let bool_sort = Z3.Boolean.mk_sort !ctx
11
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
12
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
13

    
14
let const_sorts = Hashtbl.create 13
15
let get_const_sort ty_name =
16
  Hashtbl.find const_sorts ty_name
17

    
18
let decl_sorts () =
19
  Hashtbl.iter (fun typ decl ->
20
    match typ with
21
    | Tydec_const var ->
22
      (match decl.top_decl_desc with
23
      | TypeDef tdef -> (
24
	match tdef.tydef_desc with
25
	| Tydec_enum tl ->
26
	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
27
          Hashtbl.add const_sorts var new_sort
28
	| _ -> assert false
29
      )
30
      | _ -> assert false
31
      )
32
    | _        -> ()) Corelang.type_table
33

    
34

    
35
let rec type_to_sort t =
36
  if Types.is_bool_type t  then bool_sort else
37
    if Types.is_int_type t then int_sort else 
38
  if Types.is_real_type t then real_sort else 
39
  match (Types.repr t).Types.tdesc with
40
  | Types.Tconst ty       -> get_const_sort ty
41
  | Types.Tclock t        -> type_to_sort t
42
  | Types.Tarray(dim,ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
43
  | Types.Tstatic(d, ty)-> type_to_sort ty
44
  | Types.Tarrow _
45
  | _                     -> Format.eprintf "internal error: pp_type %a@."
46
                               Types.print_ty t; assert false
47

    
48
  
49
let decl_var id =
50
  Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type)
51

    
52
let decl_machine machines m =
53
  if m.Machine_code.mname.node_id = Machine_code.arrow_id then
54
    (* We don't print arrow function *)
55
    ()
56
  else
57
    begin
58
      let _ = List.map decl_var 
59
      	(
60
	  (inout_vars machines m)@
61
	    (rename_current_list (full_memory_vars machines m)) @
62
	    (rename_mid_list (full_memory_vars machines m)) @
63
	    (rename_next_list (full_memory_vars machines m)) @
64
	    (rename_machine_list m.mname.node_id m.mstep.step_locals)
65
	)
66
      in
67
      ()
68
     (*
69
      if is_stateless m then
70
	begin
71
	  (* Declaring single predicate *)
72
	  fprintf fmt "(declare-rel %a (%a))@."
73
	    pp_machine_stateless_name m.mname.node_id
74
	    (Utils.fprintf_list ~sep:" " pp_type)
75
	    (List.map (fun v -> v.var_type) (inout_vars machines m));
76

    
77
          match m.mstep.step_asserts with
78
	  | [] ->
79
	     begin
80

    
81
	       (* Rule for single predicate *)
82
	       fprintf fmt "; Stateless step rule @.";
83
	       fprintf fmt "@[<v 2>(rule (=> @ ";
84
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
85
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
86
		 pp_machine_stateless_name m.mname.node_id
87
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
88
	     end
89
	  | assertsl ->
90
	     begin
91
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
92
	       
93
	       fprintf fmt "; Stateless step rule with Assertions @.";
94
	       (*Rule for step*)
95
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
96
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
97
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
98
		 pp_machine_stateless_name m.mname.node_id
99
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
100
	  
101
	     end
102
	       
103
	end
104
      else
105
	begin
106
	  (* Declaring predicate *)
107
	  fprintf fmt "(declare-rel %a (%a))@."
108
	    pp_machine_reset_name m.mname.node_id
109
	    (Utils.fprintf_list ~sep:" " pp_type)
110
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
111

    
112
	  fprintf fmt "(declare-rel %a (%a))@."
113
	    pp_machine_step_name m.mname.node_id
114
	    (Utils.fprintf_list ~sep:" " pp_type)
115
	    (List.map (fun v -> v.var_type) (step_vars machines m));
116

    
117
	  pp_print_newline fmt ();
118

    
119
	  (* Rule for reset *)
120
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
121
	    (pp_machine_reset machines) m 
122
	    pp_machine_reset_name m.mname.node_id
123
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
124

    
125
          match m.mstep.step_asserts with
126
	  | [] ->
127
	     begin
128
	       fprintf fmt "; Step rule @.";
129
	       (* Rule for step*)
130
	       fprintf fmt "@[<v 2>(rule (=> @ ";
131
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
132
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
133
		 pp_machine_step_name m.mname.node_id
134
		 (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
135
	     end
136
	  | assertsl -> 
137
	     begin
138
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
139
	       (* print_string pp_val; *)
140
	       fprintf fmt "; Step rule with Assertions @.";
141
	       
142
	       (*Rule for step*)
143
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
144
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
145
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
146
		 pp_machine_step_name m.mname.node_id
147
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
148
	     end
149
	       
150
     	       
151
	end
152
      *)  end
153

    
154
           
155
module Verifier =
156
  (struct
157
    include VerifierType.Default
158
    let name = "zustre"
159
    let options = []
160
    let activate () = (
161
        active := true;
162
        Options.output := "horn";
163
      )
164
    let is_active () = !active
165

    
166
    let get_normalization_params () =
167
      (* make sure the output is "Horn" *)
168
      assert(!Options.output = "horn");
169
      Backends.get_normalization_params ()
170

    
171
    let run basename prog machines =
172
      let machines = Machine_code.arrow_machine::machines in
173
      let machines = preprocess machines in
174
      decl_sorts ();
175
      List.iter (decl_machine machines) (List.rev machines);
176

    
177
      
178
      ()
179

    
180
  end: VerifierType.S)
181