Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Allow unfolding of basic non-recursive predicates #12

Open
wants to merge 6 commits into
base: StagedSL
Choose a base branch
from
Open

Allow unfolding of basic non-recursive predicates #12

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
5581a06
Allow unfolding of non-recursive predicates
EmilyOng Feb 3, 2024
a74f2f9
Check why3 only for Prusti's all example
EmilyOng Feb 3, 2024
21e6896
Remove unneeded visit and fix nits
EmilyOng Feb 7, 2024
c7642d1
Remove false
EmilyOng Feb 7, 2024
f92b4ec
Check atomics for names
EmilyOng Feb 20, 2024
1cb721f
Remove redundant string call
EmilyOng Feb 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
13 changes: 12 additions & 1 deletion parsing/Pretty.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -413,7 +413,7 @@ let rec kappaToPure kappa : pi =



let string_of_pred ({ p_name; p_params; p_body } : pred_def) : string =
let string_of_pred ({ p_name; p_params; p_body; _ } : pred_def) : string =
Format.asprintf "%s(%s) == %s" p_name (String.concat "," p_params) (string_of_spec_list p_body)

let string_of_inclusion (lhs:spec list) (rhs:spec list) :string =
Expand Down Expand Up @@ -599,10 +599,21 @@ let is_just_res_of pi t =
let lambda_to_pred_def name t =
match t with
| TLambda (_lid, params, spec, _body) ->
let find_rec p_name =
object(self)
inherit [_] reduce_spec as super
method zero = false
method plus = (||)

method! visit_HigherOrder _ ((_p, _h, (f, _a), _r) as fn) =
self#plus (f = p_name) (super#visit_HigherOrder () fn)
end
in
EmilyOng marked this conversation as resolved.
Show resolved Hide resolved
{
p_name = name;
p_params = params;
p_body = spec;
p_rec = (find_rec name)#visit_disj_spec () spec;
}
| _ ->
failwith
Expand Down
3 changes: 2 additions & 1 deletion parsing/core_lang.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -480,7 +480,8 @@ let transform_str bound_names (s : structure_item) =
| _ -> failwith (Format.asprintf "lemma %s should have function on the left" l_name)
in
Some (`Lem {l_name; l_params; l_left; l_right})
| Pstr_predicate (p_name, p_params, p_body) -> Some (`Pred {p_name; p_params; p_body})
| Pstr_predicate (p_name, p_params, p_body) ->
Some (`Pred {p_name; p_params; p_body; p_rec = (find_rec p_name)#visit_disj_spec () p_body})
| Pstr_SL_predicate (p_sl_ex, p_sl_name, p_sl_params, p_sl_body) -> Some (`SLPred {p_sl_ex; p_sl_name; p_sl_params; p_sl_body})

| Pstr_effect { peff_name; peff_kind=_; _ } ->
Expand Down
16 changes: 11 additions & 5 deletions parsing/entail.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -305,7 +305,7 @@ let instantiate_pred : pred_def -> term list -> term -> pred_def =
(string_of_list (string_of_list string_of_staged_spec) bbody); *)
bbody
in
{ pred with p_body }
{ pred with p_body; p_rec = (find_rec pred.p_name)#visit_disj_spec () p_body }
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we need to set this here? Seems like it should already be set.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! It is not needed

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

On second thought, I think you were right to include it initially... I missed the call to instantiateStages, which can replace higher-order stages and change whether a predicate is recursive. Does that agree with your tests?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! Sorry for the late reply:

I think adding the assignment here might not help. For example, in this program:

let rec call_ret f n
= if n = 0 then f 100
  else let g = call_ret in g f (n - 1)

let test_non_rec_pred n
(*@ ens res=100 @*)
= let id i = i in

  call_ret id n

We will check if the predicate name call_ret occurs in the following staged specification:

ex v74; ens (n==0)=true; v54(100, v74); ens v52=v74 \/ ex v79 v80 v81; ens (n==0)=false/\v81=call_ret/\v80=n-1; v81(v54, v80, v79); ens v52=v79

Which will be false because call_ret != v81 so p_rec will be wrongly assigned as non-recursive.

I tried to fix this by including an additional visit_Atomic in the visitor, so that it can check for v81=call_ret.


let rec unfold_predicate_aux pred prefix (s : spec) : disj_spec =
match s with
Expand Down Expand Up @@ -587,8 +587,9 @@ and try_other_measures :
(c1, res)
with
| Some (c1, def)
(* always allow unfolding of non-recursive predicates *)
when List.length (List.filter (fun s -> s = (c1, `Left)) ctx.unfolded)
< unfolding_bound ->
< unfolding_bound || not def.p_rec ->
let unf = unfold_predicate_norm "left" def s1 in
let@ s1_1, ctx =
all_state ~name:(Format.asprintf "unfold lhs: %s" c1)~to_s:string_of_normalisedStagedSpec ~init:ctx ~pivot:(fun c -> { ctx with subsumption_obl = c.subsumption_obl }) unf
Expand All @@ -607,8 +608,9 @@ and try_other_measures :
(c2, res)
with
| Some (c2, pred_def)
(* always allow unfolding of non-recursive predicates *)
when List.length (List.filter (fun s -> s = (c2, `Right)) ctx.unfolded)
< unfolding_bound ->
< unfolding_bound || not pred_def.p_rec ->
let unf = unfold_predicate_norm "right" pred_def s2 in
let@ s2_1 =
any ~name:(Format.asprintf "unfold rhs: %s" c2)~to_s:string_of_normalisedStagedSpec unf
Expand Down Expand Up @@ -912,8 +914,12 @@ let derive_predicate m_name m_params disj =
List.map (fun (effs, (vs, pre, (p, h))) -> (effs, (vs, pre, (p, h)))) norm
|> List.map normalisedStagedSpec2Spec
in
let res =
{ p_name = m_name; p_params = m_params @ ["res"] ; p_body = new_spec } (* ASK Darius *)
let res = {
p_name = m_name;
p_params = m_params @ ["res"];
p_body = new_spec;
p_rec = (find_rec m_name)#visit_disj_spec () new_spec
} (* ASK Darius *)
in
debug ~at:2
~title:(Format.asprintf "derive predicate %s" m_name)
Expand Down
7 changes: 6 additions & 1 deletion parsing/hiplib.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -978,7 +978,12 @@ let process_items (strs: structure_item list) : unit =
let body' = replaceSLPredicatesWithDef p.p_body prog.cp_sl_predicates in
(*print_endline ("~~~> " ^ string_of_disj_spec body');
*)
let (p': pred_def) = {p_name =p.p_name; p_params = p.p_params; p_body = body'} in
let (p': pred_def) = {
p_name = p.p_name;
p_params = p.p_params;
p_body = body';
p_rec = (find_rec p.p_name)#visit_disj_spec () body';
} in
bound_names, { prog with cp_predicates = SMap.add p'.p_name p' prog.cp_predicates }

| Some (`SLPred p) ->
Expand Down
1 change: 1 addition & 0 deletions parsing/hiptypes.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -290,6 +290,7 @@ type pred_def = {
p_name: string;
p_params: string list; (* list to ensure ordering. last param is typically a return value *)
p_body: disj_spec;
p_rec: bool;
}

type sl_pred_def = {
Expand Down
10 changes: 10 additions & 0 deletions parsing/subst.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -277,3 +277,13 @@ let quantify_res_state (p, h) =

let contains_res_state (p, h) =
SSet.mem "res" (used_vars_state (p, h))

let find_rec p_name =
object(self)
inherit [_] reduce_spec as super
method zero = false
method plus = (||)

method! visit_HigherOrder _ ((_p, _h, (f, _a), _r) as fn) =
self#plus (f = p_name) (super#visit_HigherOrder () fn)
end
2 changes: 1 addition & 1 deletion src/programs.t/run.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ ALL OK!
$ check ../examples/exception.ml
ALL OK!

$ check ../prusti/all.ml
$ check_why3_only ../prusti/all.ml
ALL OK!

$ check ../prusti/blameassgn.ml
Expand Down
12 changes: 11 additions & 1 deletion src/programs.t/test_new_entail.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -286,4 +286,14 @@ let call_f_in_g ()
(*@ ens res=5 @*)
= let x = 3 in
let f x = x in
f 5
f 5

let call_ret f (* ex v; f(100,v); ens res=v *) =
f 100

let test_non_rec_pred ()
(*@ ens res=100 @*)
= let id i = i in
id 2;

call_ret id