Commit 97ad17dc authored by Andrei Paskevich's avatar Andrei Paskevich

Vc: local let-lemmas and let-functions

Also, put the call-site locations at the instantiated
pre- and post- conditions.
parent b661007c
......@@ -1344,24 +1344,10 @@ let cty_tuple args =
let frz = List.fold_right freeze_pv args isb_empty in
cty_unsafe [] [] [post] Mexn.empty Mpv.empty eff res mask frz
let cty_exec ({cty_effect = eff} as c) =
(* we do not purify the signature, so the regions will be frozen
in the resulting pvsymbol. Thus, we have to forbid all effects,
including allocation. TODO/FIXME: we should probably forbid
the rest of the signature to contain regions at all. *)
if eff.eff_oneway then Loc.errorm
"This function may not terminate, it cannot be used as pure";
if not (eff_pure eff && Sreg.is_empty eff.eff_resets) then Loc.errorm
"This function has side effects, it cannot be used as pure";
if not (Mreg.is_empty c.cty_freeze.isb_reg) then Loc.errorm
"This function is stateful, it cannot be used as pure";
let cty_exec_post_raw c =
let ity = List.fold_right (fun a ity ->
ity_func a.pv_ity ity) c.cty_args c.cty_result in
let gh = List.exists (fun a -> a.pv_ghost) c.cty_args in
let eff = eff_ghostify (gh || mask_ghost c.cty_mask) eff in
(* translate the specification *)
let al = List.map (fun a -> a.pv_vs) c.cty_args in
let pre = List.map (fun f -> t_forall_close_simp al [] f) c.cty_pre in
let res = create_vsymbol (id_fresh "result") (ty_of_ity ity) in
let res_al = t_func_app_l (t_var res) (List.map t_var al) in
let oldies = Mpv.fold (fun {pv_vs = o} {pv_vs = v} s ->
......@@ -1388,9 +1374,31 @@ let cty_exec ({cty_effect = eff} as c) =
down h s (List.rev tl) (List.rev al)
| Tbinop (Tand, f, g) -> t_and (conv f) (conv g)
| _ -> t_subst_single v res_al h) in
let h = t_forall_close_simp al [] (conv (t_subst oldies h)) in
create_post res h in
let post = List.map conv_post c.cty_post in
conv (t_subst oldies h) in
al, ity, res, List.map conv_post c.cty_post
let cty_exec_post c =
let _, _, res, ql = cty_exec_post_raw c in
List.map (create_post res) ql
let cty_exec ({cty_effect = eff} as c) =
(* we do not purify the signature, so the regions will be frozen
in the resulting pvsymbol. Thus, we have to forbid all effects,
including allocation. TODO/FIXME: we should probably forbid
the rest of the signature to contain regions at all. *)
if eff.eff_oneway then Loc.errorm
"This function may not terminate, it cannot be used as pure";
if not (eff_pure eff && Sreg.is_empty eff.eff_resets) then Loc.errorm
"This function has side effects, it cannot be used as pure";
if not (Mreg.is_empty c.cty_freeze.isb_reg) then Loc.errorm
"This function is stateful, it cannot be used as pure";
let gh = List.exists (fun a -> a.pv_ghost) c.cty_args in
let eff = eff_ghostify (gh || mask_ghost c.cty_mask) eff in
(* translate the specification *)
let al, ity, res, ql = cty_exec_post_raw c in
let pre = List.map (t_forall_close_simp al []) c.cty_pre in
let conv q = create_post res (t_forall_close_simp al [] q) in
let post = List.map conv ql in
(* we do not modify cty_freeze to respect the invariants of the cty type.
It is sound to assume that the resulting cty can be executed multiple
times, producing mappings with different type variables and regions.
......
......@@ -433,6 +433,10 @@ val cty_exec : cty -> cty
a cty of a fully applied application, returning a mapping.
The original cty must be effectless. *)
val cty_exec_post : cty -> post list
(** [cty_exec_post cty] returns a post-condition appropriate
for use with local let-functions in VC generation. *)
val cty_ghost : cty -> bool
(** [cty_ghost cty] returns [cty.cty_effect.eff_ghost] *)
......
......@@ -354,12 +354,14 @@ let rec t_subst_fmla v t f = t_label_copy f (match f.t_node with
| _ -> t_map (t_subst_fmla v t) f)
let create_let_decl ld =
let conv_post t q = match t.t_ty with
let conv_post t ql =
let conv q = match t.t_ty with
| Some _ -> open_post_with t q
| None -> let v,f = open_post q in
t_subst_fmla v t f in
let conv_post t ql = List.map (conv_post t) ql in
let cty_axiom id cty f =
List.map conv ql in
let cty_axiom id cty f axms =
if t_equal f t_true then axms else
(* we do not care about aliases for pure symbols *)
let add_old o v m = Mvs.add o.pv_vs (t_var v.pv_vs) m in
let sbs = Mpv.fold add_old cty.cty_oldies Mvs.empty in
......@@ -367,11 +369,8 @@ let create_let_decl ld =
let args = List.map (fun v -> v.pv_vs) cty.cty_args in
let f = t_forall_close args [] f in
let f = t_forall_close (Mvs.keys (t_vars f)) [] f in
create_prop_decl Paxiom (create_prsymbol id) f in
let cty_axiom id cty f axms =
if t_equal f t_true then axms
else cty_axiom id cty f :: axms in
let add_ls sm s ({c_cty = cty} as c) (abst,defn,axms) =
create_prop_decl Paxiom (create_prsymbol id) f :: axms in
let add_rs sm s ({c_cty = cty} as c) (abst,defn,axms) =
match s.rs_logic with
| RLpv _ -> invalid_arg "Pdecl.create_let_decl"
| RLnone -> abst, defn, axms
......@@ -387,30 +386,37 @@ let create_let_decl ld =
abst, defn, cty_axiom (id_clone s.rs_name) cty f axms
| RLls ({ls_name = id} as ls) ->
let vl = List.map (fun v -> v.pv_vs) cty.cty_args in
let t = t_app ls (List.map t_var vl) ls.ls_value in
let f = t_and_simp_l (conv_post t cty.cty_post) in
let hd = t_app ls (List.map t_var vl) ls.ls_value in
let f = t_and_simp_l (conv_post hd cty.cty_post) in
let nm = id.id_string ^ "_spec" in
let axms = cty_axiom (id_derive nm id) cty f axms in
let c = if Mrs.is_empty sm then c else c_rs_subst sm c in
begin match c.c_node with
| Cany | Capp _ | Cpur _ ->
(* TODO: should we produce definitions for Capp and Cpur
when possible? If yes, remove the redundant axioms. *)
(* the full spec of c is inherited by the rsymbol and
so appears in the "_spec" axiom above. Even if this
spec contains "result = ...", we do not try to extract
a definition from it. We only produce definitions via
term_of_expr from a Cfun, and the user must eta-expand
to obtain one. *)
create_param_decl ls :: abst, defn, axms
| Cfun e ->
(* TODO/FIXME: should we do any of this when the user
supplied explicit post-conditions to the definition? *)
let res = if c.c_cty.cty_pre <> [] then None else
term_of_expr ~prop:(ls.ls_value = None) e in
begin match res with
| Some f -> abst, (ls, vl, f) :: defn, axms
| None ->
let axms = match post_of_expr t e with
begin match term_of_expr ~prop:(ls.ls_value = None) e with
| Some f when cty.cty_pre = [] ->
abst, (ls, vl, f) :: defn, axms
| Some f ->
let f = t_insert hd f and nm = id.id_string ^ "_def" in
let axms = cty_axiom (id_derive nm id) cty f axms in
create_param_decl ls :: abst, defn, axms
| None when cty.cty_post = [] ->
let axms = match post_of_expr hd e with
| Some f ->
let nm = id.id_string ^ "_def" in
cty_axiom (id_derive nm id) cty f axms
| None -> axms in
create_param_decl ls :: abst, defn, axms
| None ->
create_param_decl ls :: abst, defn, axms
end
end in
let abst, defn, axms = match ld with
......@@ -423,10 +429,10 @@ let create_let_decl ld =
| LDrec rdl ->
let add_rd sm d = Mrs.add d.rec_rsym d.rec_sym sm in
let sm = List.fold_left add_rd Mrs.empty rdl in
let add_rd d dl = add_ls sm d.rec_sym d.rec_fun dl in
let add_rd d dl = add_rs sm d.rec_sym d.rec_fun dl in
List.fold_right add_rd rdl ([],[],[])
| LDsym (s,c) ->
add_ls Mrs.empty s c ([],[],[]) in
add_rs Mrs.empty s c ([],[],[]) in
let fail_trusted_rec ls =
Loc.error ?loc:ls.ls_name.id_loc (Decl.NoTerminationProof ls) in
let is_trusted_rec = match ld with
......
This diff is collapsed.
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