fixed bug in WP

parent e294f64d
......@@ -24,14 +24,15 @@ module Decrease1
{ decrease1 a }
let i = ref 0 in
while !i < length a do
invariant { 0 <= i and forall j: int. 0 <= j < i -> a[j] <> 0 }
invariant { 0 <= i and
forall j: int. 0 <= j < i -> j < length a -> a[j] <> 0 }
variant { length a - i }
if get a !i = 0 then raise (Found !i);
if get a !i > 0 then i := !i + get a !i else i := !i + 1
done
{ forall j: int. 0 <= j < length a -> a[j] <> 0 }
| Found -> { 0 <= result < length a and a[result] = 0 and
forall j: int. 0 <= j < result -> a[j] <> 1 }
forall j: int. 0 <= j < result -> a[j] <> 0 }
end
......
......@@ -1398,16 +1398,16 @@ let t_map_simp fn = t_map_simp (fun t ->
(** Traversal with separate functions for value-typed and prop-typed terms *)
module TermTF = struct
let t_map fnT fnF = t_map (e_map fnT fnF)
let t_fold fnT fnF = t_fold (e_fold fnT fnF)
let t_map_fold fnT fnF = t_map_fold (e_fold fnT fnF)
let t_all prT prF = t_all (e_map prT prF)
let t_any prT prF = t_any (e_map prT prF)
let t_map_simp fnT fnF = t_map_simp (e_map fnT fnF)
let t_map_sign fnT fnF = t_map_sign (e_fold fnT fnF)
let t_map_cont fnT fnF = t_map_cont (e_fold fnT fnF)
let tr_map fnT fnF = tr_map (e_map fnT fnF)
let tr_fold fnT fnF = tr_fold (e_fold fnT fnF)
let tr_map_fold fnT fnF = tr_map_fold (e_fold fnT fnF)
let t_map fnT fnF = t_map (e_map fnT fnF)
let t_fold fnT fnF = t_fold (e_fold fnT fnF)
let t_map_fold fnT fnF = t_map_fold (e_fold fnT fnF)
let t_all prT prF = t_all (e_map prT prF)
let t_any prT prF = t_any (e_map prT prF)
let t_map_simp fnT fnF = t_map_simp (e_map fnT fnF)
let t_map_sign fnT fnF = t_map_sign (e_fold fnT fnF)
let t_map_cont fnT fnF = t_map_cont (e_fold fnT fnF)
let tr_map fnT fnF = tr_map (e_map fnT fnF)
let tr_fold fnT fnF = tr_fold (e_fold fnT fnF)
let tr_map_fold fnT fnF = tr_map_fold (e_fold fnT fnF)
end
......@@ -332,30 +332,30 @@ val tr_map_fold : ('a -> term -> 'a * term) -> 'a -> trigger -> 'a * trigger
module TermTF : sig
val t_map : (term -> term) -> (fmla -> fmla) -> term -> term
val t_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> term -> 'a
val t_map_fold : ('a -> term -> 'a * term) ->
('a -> fmla -> 'a * fmla) -> 'a -> term -> 'a * term
val t_all : (term -> bool) -> (fmla -> bool) -> term -> bool
val t_any : (term -> bool) -> (fmla -> bool) -> term -> bool
val t_map_simp : (term -> term) -> (fmla -> fmla) -> term -> term
val t_map_sign : (bool -> term -> term) ->
(bool -> fmla -> fmla) -> bool -> term -> term
val t_map_cont : ((term -> 'a) -> term -> 'a) ->
((fmla -> 'a) -> fmla -> 'a) -> (term -> 'a) -> term -> 'a
val tr_map : (term -> term) -> (fmla -> fmla) -> trigger -> trigger
val tr_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> trigger -> 'a
val tr_map_fold : ('a -> term -> 'a * term) ->
('a -> fmla -> 'a * fmla) -> 'a -> trigger -> 'a * trigger
val t_map : (term -> term) -> (fmla -> fmla) -> term -> term
val t_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> term -> 'a
val t_map_fold : ('a -> term -> 'a * term) ->
('a -> fmla -> 'a * fmla) -> 'a -> term -> 'a * term
val t_all : (term -> bool) -> (fmla -> bool) -> term -> bool
val t_any : (term -> bool) -> (fmla -> bool) -> term -> bool
val t_map_simp : (term -> term) -> (fmla -> fmla) -> term -> term
val t_map_sign : (bool -> term -> term) ->
(bool -> fmla -> fmla) -> bool -> term -> term
val t_map_cont : ((term -> 'a) -> term -> 'a) ->
((fmla -> 'a) -> fmla -> 'a) -> (term -> 'a) -> term -> 'a
val tr_map : (term -> term) -> (fmla -> fmla) -> trigger -> trigger
val tr_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> trigger -> 'a
val tr_map_fold : ('a -> term -> 'a * term) ->
('a -> fmla -> 'a * fmla) -> 'a -> trigger -> 'a * trigger
end
(** Map/fold over free variables *)
......
......@@ -592,7 +592,7 @@ and E : sig
val add_write : R.t -> t -> t
val add_raise : T.esymbol -> t -> t
val remove_reference : R.t -> t -> t
val remove : Sreg.t -> t -> t
val filter : (R.t -> bool) -> t -> t
val remove_raise : T.esymbol -> t -> t
......@@ -633,8 +633,8 @@ end = struct
let add_raise e t = { t with raises = Sexn.add e t.raises }
let add_glob pv t = { t with globals = Spv.add pv t.globals }
let remove_reference r t =
{ t with reads = Sreg.remove r t.reads; writes = Sreg.remove r t.writes }
let remove s t =
{ t with reads = Sreg.diff t.reads s; writes = Sreg.diff t.writes s }
let filter p t =
{ t with reads = Sreg.filter p t.reads; writes = Sreg.filter p t.writes }
......
......@@ -178,7 +178,7 @@ and E : sig
val add_write : R.t -> t -> t
val add_raise : T.esymbol -> t -> t
val remove_reference : R.t -> t -> t
val remove : Sreg.t -> t -> t
val filter : (R.t -> bool) -> t -> t
val remove_raise : T.esymbol -> t -> t
......
......@@ -1516,7 +1516,7 @@ and expr_desc gl env loc ty = function
let ef = E.union e1.expr_effect e2.expr_effect in
if Sreg.exists (fun r -> occur_type_v r e2.expr_type_v) v.pv_regions then
errorm ~loc "local reference would escape its scope";
(* let ef = E.remove_reference r ef in *)
let ef = E.remove v.pv_regions ef in
Elet (v, e1, e2), e2.expr_type_v, ef
| IEletrec (dl, e1) ->
let env, dl = letrec gl env dl in
......
......@@ -172,8 +172,6 @@ let has_singleton_type pv = is_singleton_ty pv.pv_effect.vs_ty
*)
let quantify ?(all=false) env rm ef f =
eprintf "@[<hov 2>quantify: all=%b ef=%a f=@[%a@]@]@."
all E.print ef Pretty.print_term f;
let sreg = ef.E.writes in
let sreg =
if all then
......@@ -192,7 +190,9 @@ let quantify ?(all=false) env rm ef f =
in
(* all program variables involving these regions *)
let vars =
let add r _ s = try Spv.union (Mreg.find r rm) s with Not_found -> s in
let add r _ s =
try Spv.union (Mreg.find r rm) s with Not_found -> assert false
in
Mreg.fold add mreg Spv.empty
in
(* s: v -> r'/v' and vars': pv -> v' *)
......@@ -219,6 +219,12 @@ let quantify ?(all=false) env rm ef f =
let quantify_r _ r' f = wp_forall r' f in
Mreg.fold quantify_r mreg f
(* let quantify ?(all=false) env rm ef f = *)
(* let r = quantify ~all env rm ef f in *)
(* eprintf "@[<hov 2>quantify: all=%b ef=%a f=@[%a@] ==>@\n%a@]@." *)
(* all E.print ef Pretty.print_term f Pretty.print_term r; *)
(* r *)
let abstract_wp env rm ef (q',ql') (q,ql) =
assert (List.length ql' = List.length ql);
let quantify_res f' f res =
......@@ -369,7 +375,7 @@ let rec wp_expr env rm e q =
if Debug.test_flag debug then begin
eprintf "@[--------@\n@[<hov 2>e = %a@]@\n" Pgm_pretty.print_expr e;
eprintf "@[<hov 2>q = %a@]@\n" Pretty.print_term (snd (fst q));
eprintf "@[<hov 2>f = %a@]@\n----@]@\n" Pretty.print_term f;
eprintf "@[<hov 2>f = %a@]@\n----@]@." Pretty.print_term f;
end;
f
......@@ -392,7 +398,10 @@ and wp_desc env rm e q = match e.expr_desc with
let f = wp_triple env rm bl t in
wp_and q f
| Elet (x, e1, e2) ->
let w2 = wp_expr env rm e2 (filter_post e2.expr_effect q) in
let w2 =
let rm = add_binder x rm in
wp_expr env rm e2 (filter_post e2.expr_effect q)
in
let v1 = v_result x.pv_pure.vs_ty in
let t1 = t_label ~loc:e1.expr_loc ["let"] (t_var v1) in
let q1 = v1, t_subst (subst1 x.pv_pure t1) w2 in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment