Skip to content

Commit

Permalink
Fix lots of small bugs, add higher-order tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@dariusf
dariusf committed May 10, 2023
1 parent d188b5f commit efcd33c
Show file tree
Hide file tree
Showing 12 changed files with 359 additions and 75 deletions.
15 changes: 9 additions & 6 deletions parsing/Pretty.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -293,15 +293,15 @@ let string_of_stages (st:stagedSpec) : string =
| Require (p, h) ->
Format.asprintf "req %s" (string_of_state (p, h))
| HigherOrder (pi, h, (f, args), ret) ->
Format.asprintf "%s /\\ %s$(%s, %s); " (string_of_state (pi, h)) f (string_of_args args) (string_of_term ret)
Format.asprintf "%s(%s, %s, %s)" f (string_of_state (pi, h)) (string_of_args args) (string_of_term ret)
| NormalReturn (pi, heap, ret) ->
Format.asprintf "Norm(%s, %s)" (string_of_state (pi, heap)) (string_of_term ret)
| RaisingEff (pi, heap, (name, args), ret) ->
Format.asprintf "%s(%s, %s, %s)" name (string_of_state (pi, heap)) (string_of_args args) (string_of_term ret)
| Exists vs ->
Format.asprintf "ex %s" (String.concat " " vs)
| Pred {name; vars} ->
Format.asprintf "%s(%s)" name (String.concat " " vars)
(* | IndPred {name; args} -> *)
(* Format.asprintf "%s(%s)" name (String.concat " " (List.map string_of_term args)) *)

let string_of_spec (spec:spec) :string =
match spec with
Expand All @@ -317,6 +317,9 @@ let rec string_of_spec_list (specs:spec list) : string =
| [x] -> string_of_spec x
| x :: xs -> string_of_spec x ^ " \\/ " ^ string_of_spec_list xs

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 =
string_of_spec_list lhs ^" |- " ^string_of_spec_list rhs
;;
Expand Down Expand Up @@ -524,8 +527,8 @@ let normalise_stagedSpec (acc:normalisedStagedSpec) (stagedSpec:stagedSpec) : no
| HigherOrder (pi, heap, ins, ret') ->
let v = verifier_getAfreeVar ~from:"n" () in
(effectStages@[(existential, req, mergeState ens (pi, heap), ins , ret')], freshNormStageVar v)
| Pred {name; _} ->
failwith (Format.asprintf "cannot normalise predicate %s" name)
(* | IndPred {name; _} -> *)
(* failwith (Format.asprintf "cannot normalise predicate %s" name) *)

let rec normalise_spec_ (acc:normalisedStagedSpec) (spec:spec) : normalisedStagedSpec =
match spec with
Expand Down Expand Up @@ -757,7 +760,7 @@ let%expect_test "normalise spec" =
==>
req 1=1; E(x->1 /\ 1=1, [3], ()); req emp; Norm(y->2, ())

Norm(x->1, ()); emp /\ f$([3], ()); ; Norm(y->2, ())
Norm(x->1, ()); f(emp, [3], ()); Norm(y->2, ())
==>
req emp; f(x->1, [3], ()); req emp; Norm(y->2, ())
|}]
Expand Down
150 changes: 115 additions & 35 deletions parsing/entail.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,50 @@ let string_of_instantiations kvs =
List.map (fun (k, v) -> Format.asprintf "%s := %s" k v) kvs
|> String.concat ", " |> Format.asprintf "[%s]"

(** a lemma is a formula such as f$(a, r) |= c(a, r) *)
type lemma = {
l_name : string;
l_vars : string list;
l_left : stagedSpec;
l_right : spec;
}

let instantiate_lemma : lemma -> term list -> lemma =
fun lem args ->
let bs = List.map2 (fun a b -> (a, b)) lem.l_vars args in
{
lem with
l_left = (Forward_rules.instantiateStages bs) lem.l_left;
l_right = List.map (Forward_rules.instantiateStages bs) lem.l_right;
}

let instantiate_pred : pred_def -> term list -> pred_def =
fun pred args ->
let bs = List.map2 (fun a b -> (a, b)) pred.p_params args in
{
pred with
p_body =
List.map
(fun b -> List.map (Forward_rules.instantiateStages bs) b)
pred.p_body;
}

(** single application *)
let apply_lemma : lemma -> spec -> spec =
fun lem sp ->
let tr s =
(* for now, lemmas are only applied from left to right, and the left side must be a predicate *)
match (s, lem.l_left) with
| Exists _, _ | Require (_, _), _ | NormalReturn _, _ | RaisingEff _, _ ->
[s]
| ( HigherOrder (_p, _h, (name, args), _r),
HigherOrder (_, _, (name1, _args1), _) )
when String.equal name name1 ->
(instantiate_lemma lem args).l_right
| HigherOrder _, _ -> [s]
in
List.concat_map tr sp

let conj xs =
match xs with
| [] -> True
Expand Down Expand Up @@ -490,15 +534,22 @@ let rec check_staged_subsumption_ :
(* let debug = false *)
let ( let@ ) f x = f x

(** Given two heap formulae, matches points-to predicates
may backtrack if the locations are quantified.
returns (by invoking the continuation) when matching is complete (when right is empty).
id: human-readable name
vs: quantified variables
k: continuation
*)
let rec check_qf2 :
string ->
pi ->
string list ->
state ->
state ->
(pi * pi -> 'a Res.pf) ->
'a Res.pf =
fun id eqs vs ante conseq k ->
fun id vs ante conseq k ->
let a = Heap.normalize ante in
let c = Heap.normalize conseq in
match (a, c) with
Expand Down Expand Up @@ -536,7 +587,7 @@ let rec check_qf2 :
let _unifier = Atomic (EQ, Var fl, Var fr) in
let triv = Atomic (EQ, v, v1) in
(* matching ptr values are added as an eq to the right side, since we don't have a term := term substitution function *)
check_qf2 id True vs (conj [p1], h1') (conj [p2; triv], h2') k)
check_qf2 id vs (conj [p1], h1') (conj [p2; triv], h2') k)
in
begin
match r1 with
Expand All @@ -557,7 +608,7 @@ let rec check_qf2 :
(* let *)
(* And (p1, Atomic (EQ, v, v1)) *)
(* match *)
check_qf2 (* (SepConj (k, PointsTo (x, v))) *) id eqs vs
check_qf2 (* (SepConj (k, PointsTo (x, v))) *) id vs
(conj [p1], h1')
(conj [p2], h2')
k
Expand All @@ -583,6 +634,17 @@ let rec check_qf2 :
| None -> failwith (Format.asprintf "could not split LHS, bug?")
end

(** recurses down a normalised staged spec, matching stages,
translating away heap predicates to build a pure formula,
then proving it at the end.
quantifiers are left to z3 to instantiate because they are shared across stages,
so instantiation has to be delayed until we know the entire formula.
i: index of stage
all_vars: quantified variables
so_far: conjuncts of the formula we're building, together with human-readable form
*)
let rec check_staged_subsumption2 :
int ->
string list ->
Expand All @@ -598,12 +660,11 @@ let rec check_staged_subsumption2 :

let triv = Atomic (EQ, r1, r2) in

(* let _ = *)
let@ pre_l, pre_r =
check_qf2 (Format.asprintf "pre%d" i) True all_vars (p2, h2) (p1, h1)
check_qf2 (Format.asprintf "pre%d" i) all_vars (p2, h2) (p1, h1)
in
let@ post_l, post_r =
check_qf2 (Format.asprintf "post%d" i) True all_vars (qp1, qh1) (qp2, qh2)
check_qf2 (Format.asprintf "post%d" i) all_vars (qp1, qh1) (qp2, qh2)
in
let fml =
[
Expand Down Expand Up @@ -638,11 +699,9 @@ let rec check_staged_subsumption2 :
in

(* contra *)
let@ pre_l, pre_r = check_qf2 "pren" True all_vars (p2, h2) (p1, h1) in
let@ pre_l, pre_r = check_qf2 "pren" all_vars (p2, h2) (p1, h1) in
(* cov *)
let@ post_l, post_r =
check_qf2 "postn" True all_vars (qp1, qh1) (qp2, qh2)
in
let@ post_l, post_r = check_qf2 "postn" all_vars (qp1, qh1) (qp2, qh2) in
let fml =
[
( Format.asprintf "norm res eq: %s = %s" (string_of_term r1)
Expand Down Expand Up @@ -683,31 +742,62 @@ let rec check_staged_subsumption2 :
else Error (rule ~name:"subsumption-base" ~success:false "fail")
| _ -> Error (rule ~name:"subsumption-stage" ~success:false "unequal length")

let check_staged_subsumption : spec -> spec -> state Res.pf =
fun n1 n2 ->
(* replace quantified variables on the left side with fresh variables *)
let es1, ns1 =
let norm = normalise_spec n1 in
norm
(* let vars = Forward_rules.getExistientalVar norm in
let vars_fresh =
List.map (fun v -> (v, Var (verifier_getAfreeVar ()))) vars
in
let es1, (_, pre, post, ret) = instantiate_existentials vars_fresh norm in
( List.map (fun (_, pre, post, eff, ret) -> ([], pre, post, eff, ret)) es1,
([], pre, post, ret) ) *)
(** f;a;e \/ b and a == c \/ d
=> f;(c \/ d);e \/ b
=> f;c;e \/ f;d;e \/ b *)
let unfold_predicate : pred_def -> disj_spec -> disj_spec =
fun pred ds ->
let rec loop prefix already s =
match s with
| [] -> List.map List.rev prefix
| HigherOrder (_p, _h, (name, args), _r) :: s1
when String.equal name pred.p_name && not (List.mem name already) ->
(* unfold *)
let pred1 = instantiate_pred pred args in
let pref : disj_spec =
List.concat_map (fun p -> List.map (fun b -> b @ p) pred1.p_body) prefix
in
loop pref already s1
| c :: s1 ->
let pref = List.map (fun p -> c :: p) prefix in
loop pref already s1
in
List.concat_map (fun s -> loop [] [] s) ds

let check_staged_subsumption : lemma list -> spec -> spec -> state Res.pf =
fun lems n1 n2 ->
(* apply lemmas once *)
let n1 = List.fold_right apply_lemma lems n1 in
let n2 = List.fold_right apply_lemma lems n2 in
(* proceed *)
let es1, ns1 = normalise_spec n1 in
let es2, ns2 = normalise_spec n2 in
(* check_staged_subsumption_ (es1, ns1) (es2, ns2) *)
check_staged_subsumption2 0
(Forward_rules.getExistientalVar (es1, ns1)
@ Forward_rules.getExistientalVar (es2, ns2))
[] (es1, ns1) (es2, ns2)

(**
Subsumption between disjunctive specs.
S1 \/ S2 |= S3 \/ S4
*)
let subsumes_disj :
lemma list -> pred_def list -> disj_spec -> disj_spec -> state list Res.pf =
fun lems preds ds1 ds2 ->
(* unfold all predicates once *)
let ds1 = List.fold_right unfold_predicate preds ds1 in
let ds2 = List.fold_right unfold_predicate preds ds2 in
(* proceed *)
Res.all ~may_elide:true ~name:"subsumes-disj-lhs-all" ~to_s:string_of_spec ds1
(fun s1 ->
Res.any ~may_elide:true ~name:"subsumes-disj-rhs-any" ~to_s:string_of_spec
ds2 (fun s2 -> check_staged_subsumption lems s1 s2))

let%expect_test "staged subsumption" =
verifier_counter_reset ();
let test name l r =
let res = check_staged_subsumption l r in
let res = check_staged_subsumption [] l r in
Format.printf "\n--- %s\n%s\n%s\n%s%s@." name (string_of_spec l)
(match res with Ok _ -> "|--" | Error _ -> "|-/-")
(string_of_spec r)
Expand Down Expand Up @@ -813,16 +903,6 @@ let%expect_test "staged subsumption" =
==> emp
│[subsumption-stage] E(x->a+1, [], r); req x->a; Norm(x->a+1, r) |= E(x->a+1, [], r); req x->1; Norm(x->1, r) |}]

(**
Subsumption between disjunctive specs.
S1 \/ S2 |= S3 \/ S4
*)
let subsumes_disj ds1 ds2 =
Res.all ~may_elide:true ~name:"subsumes-disj-lhs-all" ~to_s:string_of_spec ds1
(fun s1 ->
Res.any ~may_elide:true ~name:"subsumes-disj-rhs-any" ~to_s:string_of_spec
ds2 (fun s2 -> check_staged_subsumption s1 s2))

module Normalize = struct
let rec sl_dom (h : kappa) =
match h with
Expand Down
45 changes: 26 additions & 19 deletions parsing/forward_rules.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,12 +19,13 @@ let concatenateSpecsWithSpec (current:spec list) (event:spec list) : spec list
let temp = List.map (fun a -> concatenateSpecsWithEvent current a) event in
List.flatten temp

let rec retriveNormalStage (spec:spec) : (pi * kappa * term) =
let rec retrieve_return_value (spec:spec) : term =
match spec with
| [] -> failwith "retriveNormalStage empty spec"
| [NormalReturn (pN, hN, retN)]
| [RaisingEff(pN, hN,_ , retN)] -> (pN, hN, retN)
| _ :: xs -> retriveNormalStage xs
| [] -> failwith "retrieve_return_value empty spec"
| [HigherOrder (_, _, _, retN)]
| [NormalReturn (_, _, retN)]
| [RaisingEff(_, _, _, retN)] -> retN
| _ :: xs -> retrieve_return_value xs

let rec retriveSpecFromEnv (fname: string) (env:meth_def list) : (string list * spec list) option =
match env with
Expand Down Expand Up @@ -109,6 +110,9 @@ let instantiateStages (bindings:((string * core_value) list)) (stagedSpec:stage
RaisingEff (instantiatePure bindings pi, instantiateHeap bindings kappa, (label,
List.map (fun bt -> instantiateTerms bindings bt) basic_t_list
), instantiateTerms bindings ret)
(* | Pred {name; args} -> *)
(* Pred {name; args = List.map (instantiateTerms bindings) args} *)



let instantiateSpec (bindings:((string * core_value) list)) (sepc:spec) : spec =
Expand Down Expand Up @@ -258,7 +262,7 @@ and infer_of_expression (env:meth_def list) (current:spec list) (expr:core_lang)
let phi1 = infer_of_expression env current expr1 in
List.flatten (List.map (fun spec ->
(*print_endline (string_of_spec(spec)); *)
let (_, _, retN) = retriveNormalStage spec in
let retN = retrieve_return_value spec in
match retN with
| UNIT -> infer_of_expression env [spec] expr2
(*| Var freshV ->
Expand Down Expand Up @@ -370,17 +374,20 @@ and infer_of_expression (env:meth_def list) (current:spec list) (expr:core_lang)
| _ -> failwith ("wrong aruguments of - " )

else
(match retriveSpecFromEnv fname env with
| None -> failwith ("no implemnetation of " ^ fname )
| Some (formalArgs, spec_of_fname) ->
(*print_endline (string_of_spec_list spec_of_fname);*)
let spec_of_fname =renamingexistientalVar spec_of_fname in
(*print_endline ("====\n"^ string_of_spec_list spec_of_fname);*)

let bindings = bindFormalNActual (formalArgs) (actualArgs) in
let instantiatedSpec = instantiateSpecList bindings spec_of_fname in
concatenateSpecsWithSpec current instantiatedSpec
)
let spec_of_fname =
match retriveSpecFromEnv fname env with
| None ->
let ret = verifier_getAfreeVar () in
[[Exists [ret]; HigherOrder (True, EmptyHeap, (fname, actualArgs), Var ret)]]
| Some (formalArgs, spec_of_fname) ->
(*print_endline (string_of_spec_list spec_of_fname);*)
let spec = renamingexistientalVar spec_of_fname in
let bindings = bindFormalNActual (formalArgs) (actualArgs) in
let instantiatedSpec = instantiateSpecList bindings spec in
instantiatedSpec
(*print_endline ("====\n"^ string_of_spec_list spec_of_fname);*)
in
concatenateSpecsWithSpec current spec_of_fname

(*
ex i; Norm(i->0, i); ex f4;
Expand All @@ -400,8 +407,8 @@ Norm(i->f5+1, ()); Norm(emp, f4)


| CIfELse (v, expr2, expr3) ->
let eventThen = NormalReturn (Atomic(GT, v, Num 0), EmptyHeap, UNIT) in
let eventElse = NormalReturn (Atomic(LT, v, Num 0), EmptyHeap, UNIT) in
let eventThen = NormalReturn (Atomic(EQ, v, Num 0), EmptyHeap, UNIT) in
let eventElse = NormalReturn (Not(Atomic(EQ, v, Num 0)), EmptyHeap, UNIT) in
let currentThen = concatenateSpecsWithEvent current [eventThen] in
let currentElse = concatenateSpecsWithEvent current [eventElse] in
(infer_of_expression env currentThen expr2) @
Expand Down

0 comments on commit efcd33c

Please sign in to comment.