1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
|
open Ast
open Ast_util
open Formula
open Typing
open Util
open Abs_domain
open Num_domain
module I (E : ENVIRONMENT_DOMAIN) : sig
type st
val do_prog : int -> rooted_prog -> unit
end = struct
type st = {
rp : rooted_prog;
widen_delay : int;
env : E.t;
f : bool_expr;
cl : conslist;
f_g : bool_expr;
cl_g : conslist;
guarantees : (id * bool_expr) list;
}
(* init state *)
let init_state widen_delay rp =
let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
let env = List.fold_left
(fun env (_, id, ty) -> E.addvar env id ty)
E.init
rp.all_vars
in
let init_f = Transform.init_f_of_prog rp in
let guarantees = Transform.guarantees_of_prog rp in
Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_typed_var ", ") rp.all_vars;
Format.printf "Guarantees:@.";
List.iter (fun (id, f) ->
Format.printf " %s: %a@." id Formula_printer.print_expr f)
guarantees;
Format.printf "@.";
let env = E.apply_f env init_f in
let cl = Formula.conslist_of_f f in
let cl_g = Formula.conslist_of_f f_g in
{ rp; widen_delay;
f; cl; f_g; cl_g;
guarantees; env }
(*
pass_cycle : var_def list -> E.t -> E.t
Does :
- x <- Nx, for all x
- ignore x for all x such that Nx does not exist
*)
let pass_cycle vars e =
let tr_assigns = List.fold_left
(fun q (_, id, _) ->
if id.[0] = 'N' then
(String.sub id 1 (String.length id - 1), NIdent id)::q
else
q)
[] vars
in
let e = E.assign e tr_assigns in
let forget_vars = List.map (fun (_, id, _) -> id)
(List.filter
(fun (_, id, _) ->
not (List.exists (fun (_, id2, _) -> id2 = "N"^id) vars))
vars) in
let e = List.fold_left E.forgetvar e forget_vars in
e
(* cycle : st -> cl -> env -> env *)
let cycle st cl i =
(pass_cycle st.rp.all_vars (E.apply_cl i cl))
(*
loop : st -> env -> env -> env
*)
let loop st pnew stay =
Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
Formula_printer.print_conslist st.cl
E.print_all pnew E.print_all stay;
let add_stay = cycle st st.cl pnew in
let acc0 = E.join stay add_stay in
let fsharp cl i =
Format.printf "Acc @[<hv>%a@]@." E.print_all i;
let j = cycle st cl i in
E.join acc0 j
in
let rec iter n i =
let i' =
if n < st.widen_delay
then E.join i (fsharp st.cl_g i)
else E.widen i (fsharp st.cl_g i)
in
if E.eq i i' then i else iter (n+1) i'
in
let x = iter 0 acc0 in
let y = fix E.eq (fsharp st.cl_g) x in (* decreasing iteration *)
let z = E.apply_cl y st.cl in
y, z
(*
do_prog : rooted_prog -> unit
*)
let do_prog widen_delay rp =
let st = init_state widen_delay rp in
let pnew = st.env in
let pnew_c = E.apply_cl pnew st.cl in
let stay, stay_c = loop st pnew (E.vbottom pnew) in
Format.printf "@.@[<hov>New %a@]@.@."
E.print_all pnew_c;
Format.printf "@[<hov>Stay %a@]@.@."
E.print_all stay_c;
let final = E.join pnew_c stay_c in
Format.printf "@[<hov>Final %a@]@.@."
E.print_all final;
let check_guarantee (id, f) =
let cl = Formula.conslist_of_f f in
Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ "
id Formula_printer.print_conslist cl;
let z = E.apply_cl final cl in
if E.is_bot z then
Format.printf "OK@]@ "
else
Format.printf "FAIL@]@ "
in
if st.guarantees <> [] then begin
Format.printf "Guarantee @[<v 0>";
List.iter check_guarantee st.guarantees;
Format.printf "@]@."
end;
if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin
Format.printf "Probes:@[<v>";
List.iter (fun (p, id, _) ->
if p then Format.printf " %a ∊ %a@ "
Formula_printer.print_id id
E.print_itv (E.var_itv final id))
st.rp.all_vars;
Format.printf "@]@."
end
end
|
