From 6fcb247abe8480600e3ddd1b0de1d5d7e628d772 Mon Sep 17 00:00:00 2001 From: Samuel Gruetter Date: Mon, 10 Jun 2024 18:05:31 -0400 Subject: [PATCH] support functions that don't use the heap --- LiveVerif/src/LiveVerif/LiveProgramLogic.v | 83 ++++++++++++++++++- LiveVerif/src/LiveVerif/PackageContext.v | 25 ++++-- LiveVerif/src/LiveVerifExamples/critbit.v | 11 +-- LiveVerif/src/LiveVerifExamples/fibonacci.v | 8 +- LiveVerif/src/LiveVerifExamples/linked_list.v | 3 - LiveVerif/src/LiveVerifExamples/min.v | 22 ++--- bedrock2/src/bedrock2/HeapletwiseHyps.v | 1 + 7 files changed, 114 insertions(+), 39 deletions(-) diff --git a/LiveVerif/src/LiveVerif/LiveProgramLogic.v b/LiveVerif/src/LiveVerif/LiveProgramLogic.v index 5bdb5179..9e16e651 100644 --- a/LiveVerif/src/LiveVerif/LiveProgramLogic.v +++ b/LiveVerif/src/LiveVerif/LiveProgramLogic.v @@ -431,7 +431,15 @@ Ltac call lhs fname arges := eapply H end | (* one dexprs1 goal containing argument evaluation, precondition, and continuation - after the call *) ]. + after the call: *) + lazymatch goal with + | |- dexprs1 ?m ?l ?es ?vs (?calleePre /\ enable_frame_trick.enable_frame_trick ?cont) => + lazymatch calleePre with + | context[m] => idtac (* default case: callee uses memory *) + | _ => (* special case: callee does not use memory *) + change (dexprs1 m l es vs (calleePre /\ cont)) + end + end ]. (* Assigns default well_founded relations to types. Use lower costs to override existing entries. *) @@ -1446,6 +1454,79 @@ Notation "'void' fname ( ) /* *# 'ghost_args' := g1 .. gn ; 'requires' t1 m1 := osemi custom optional_semicolon at level 1, only parsing). + +(* Same definitions but without ghost_args: *) + +(* One return value: *) +Notation "'uintptr_t' fname ( 'uintptr_t' a1 , 'uintptr_t' .. , 'uintptr_t' an ) /* *# 'requires' t1 m1 := pre ; 'ensures' t2 m2 r := post #* osemi *" := + (fun fname: String.string => + (fun fs => + (forall a1, .. (forall an, + (forall t1 m1, pre -> + WeakestPrecondition.call fs fname t1 m1 + (@cons (@word.rep _ _) a1 .. (@cons (@word.rep _ _) an nil) ..) + (fun t2 m2 retvs => exists r, retvs = cons r nil /\ post))) .. )) + : ProgramLogic.spec_of fname) +(in custom funspec at level 1, + fname name, + a1 closed binder, an closed binder, + t1 name, t2 name, m1 name, m2 name, r name, + pre constr at level 200, + post constr at level 200, + osemi custom optional_semicolon at level 1, + only parsing). + +(* One return value and no arguments: *) +Notation "'uintptr_t' fname ( ) /* *# 'requires' t1 m1 := pre ; 'ensures' t2 m2 r := post #* osemi *" := + (fun fname: String.string => + (fun fs => + (forall t1 m1, pre -> + WeakestPrecondition.call fs fname t1 m1 nil + (fun t2 m2 retvs => exists r, retvs = cons r nil /\ post))) + : ProgramLogic.spec_of fname) +(in custom funspec at level 1, + fname name, + t1 name, t2 name, m1 name, m2 name, r name, + pre constr at level 200, + post constr at level 200, + osemi custom optional_semicolon at level 1, + only parsing). + +(* No return value: *) +Notation "'void' fname ( 'uintptr_t' a1 , 'uintptr_t' .. , 'uintptr_t' an ) /* *# 'requires' t1 m1 := pre ; 'ensures' t2 m2 := post #* osemi *" := + (fun fname: String.string => + (fun fs => + (forall a1, .. (forall an, + (forall t1 m1, pre -> + WeakestPrecondition.call fs fname t1 m1 + (@cons (@word.rep _ _) a1 .. (@cons (@word.rep _ _) an nil) ..) + (fun t2 m2 retvs => retvs = nil /\ post))) .. )) + : ProgramLogic.spec_of fname) +(in custom funspec at level 1, + fname name, + a1 closed binder, an closed binder, + t1 name, t2 name, m1 name, m2 name, + pre constr at level 200, + post constr at level 200, + osemi custom optional_semicolon at level 1, + only parsing). + +(* No return value an no arguments: *) +Notation "'void' fname ( ) /* *# 'requires' t1 m1 := pre ; 'ensures' t2 m2 := post #* osemi *" := + (fun fname: String.string => + (fun fs => + (forall t1 m1, pre -> + WeakestPrecondition.call fs fname t1 m1 nil + (fun t2 m2 retvs => retvs = nil /\ post))) + : ProgramLogic.spec_of fname) +(in custom funspec at level 1, + fname name, + t1 name, t2 name, m1 name, m2 name, + pre constr at level 200, + post constr at level 200, + osemi custom optional_semicolon at level 1, + only parsing). + Notation ".* */ x" := (match x with (* <-- typecheck x before passing it to Ltac, to get better error messages *) | _ => ltac:(let r := with_ident_as_string_no_beta x in exact r) diff --git a/LiveVerif/src/LiveVerif/PackageContext.v b/LiveVerif/src/LiveVerif/PackageContext.v index cdda31ce..469e850b 100644 --- a/LiveVerif/src/LiveVerif/PackageContext.v +++ b/LiveVerif/src/LiveVerif/PackageContext.v @@ -192,12 +192,22 @@ Ltac add_equality_to_post x Post := (* y (t or m or l or measure) will be patterned out at end of package_context *) move y at top. +Ltac add_mem_equality_to_Post_or_move_at_top m Post := + lazymatch type of Post with + | context[m] => + (* current packaged context contains an assertion about memory (the usual case) *) + move m at top + | _ => + (* we're in a function that does not use the heap at all *) + add_equality_to_post m Post + end. + Ltac add_equalities_to_post Post := lazymatch goal with (* loop pre/post *) | |- ?E (?Ghosts, ?Measure, ?T, ?M, ?L) => add_equality_to_post L Post; - move M at top; + add_mem_equality_to_Post_or_move_at_top M Post; lazymatch type of Post with | context[T] => idtac (* current packaged context already says something about the trace, so only keep that *) @@ -208,13 +218,13 @@ Ltac add_equalities_to_post Post := (* loop invariant *) | |- ?E ?Measure ?T ?M ?L => add_equality_to_post L Post; - move M at top; + add_mem_equality_to_Post_or_move_at_top M Post; add_equality_to_post T Post; add_equality_to_post Measure Post (* if branch post *) | |- ?E ?T ?M ?L => add_equality_to_post L Post; - move M at top; + add_mem_equality_to_Post_or_move_at_top M Post; add_equality_to_post T Post end. @@ -237,7 +247,7 @@ Ltac move_mem_hyp_just_below_scope_marker := end (* Note: the two above moves should be replaced by one single `move H below s`, but `below` is not implemented yet: https://github.com/coq/coq/issues/15209 *) - | |- _ => fail "No separation logic hypothesis about" m "found" + | |- _ => idtac (* do nothing if this function does not use the heap *) end. (* can be overridden with @@ -700,12 +710,15 @@ Ltac merge_sep_pair_step := Ltac merge_seps_done := lazymatch goal with - | H: seps ((seps (if ?b then nil else nil)) :: ?Rs) ?m |- _ => + | H: seps ((seps (if ?b then nil else nil)) :: ?Rs) ?m |- exec _ _ _ ?m _ _ => (* memory was modified in different ways in then/else branch *) eapply merge_seps_done in H; cbn [seps] in H - | H: seps _ _ |- _ => + | H: seps _ ?m |- exec _ _ _ ?m _ _ => (* memory was not modified (or in exactly the same way in both branches) *) cbn [seps] in H + | H: ?m = _ |- exec _ _ _ ?m _ _ => + (* this function does not use the heap *) + idtac | |- _ => fail 1000 "failed to match the sepclauses of the then-branch and else-branch" end. diff --git a/LiveVerif/src/LiveVerifExamples/critbit.v b/LiveVerif/src/LiveVerifExamples/critbit.v index 7dce110d..83868ae8 100644 --- a/LiveVerif/src/LiveVerifExamples/critbit.v +++ b/LiveVerif/src/LiveVerifExamples/critbit.v @@ -2517,11 +2517,8 @@ Qed. #[export] Instance spec_of_critical_bit: fnspec := .**/ uintptr_t critical_bit(uintptr_t k1, uintptr_t k2) /**# - (* heaplet packaging doesn't work well then there's just one item in the heap - [or I was doing something wrong] *) - ghost_args := (R1 R2: mem -> Prop); - requires t m := <{ * R1 * R2 }> m /\ k1 <> k2; - ensures t' m' res := t = t' /\ <{ * R1 * R2 }> m' + requires t m := k1 <> k2; + ensures t' m' res := t = t' /\ m' = m /\ 0 <= \[res] < 32 /\ \[res] = pfx_len (pfx_meet (pfx_emb k1) (pfx_emb k2)) #**/ /**. @@ -2757,9 +2754,7 @@ Derive cbt_insert SuchThat (fun_correct! cbt_insert) As cbt_insert_ok. return tp; /**. .**/ } /**. .**/ else { /**. .**/ - uintptr_t cb = critical_bit(k, best_k); /**. - instantiate (3:=emp True). steps. - unfold enable_frame_trick.enable_frame_trick. steps. .**/ + uintptr_t cb = critical_bit(k, best_k); /**. .**/ uintptr_t result = cbt_insert_at(tp, cb, k, v); /**. subst. steps. unfold enable_frame_trick.enable_frame_trick. steps. .**/ return result; /**. .**/ diff --git a/LiveVerif/src/LiveVerifExamples/fibonacci.v b/LiveVerif/src/LiveVerifExamples/fibonacci.v index fde2d657..b3a1bbd3 100644 --- a/LiveVerif/src/LiveVerifExamples/fibonacci.v +++ b/LiveVerif/src/LiveVerifExamples/fibonacci.v @@ -16,9 +16,6 @@ Definition fib(n: word): word := /[Z.of_nat (fib_nat (Z.to_nat \[n]))]. Set Default Proof Mode "Classic". -(* TODO support functions that don't access any memory *) -Definition dummy: mem -> Prop := emp True. - Lemma fib_recursion: forall n, 0 < \[n] -> \[n] + 1 < 2 ^ 32 -> @@ -46,9 +43,8 @@ Proof. intros. destruct c; auto. Qed. #[export] Instance spec_of_fibonacci: fnspec := .**/ uintptr_t fibonacci(uintptr_t n) /**# - ghost_args := (R: mem -> Prop); - requires t m := sep dummy R m; - ensures t' m' res := t' = t /\ sep dummy R m' /\ res = fib n #**/ /**. + requires t m := True; + ensures t' m' res := t' = t /\ m' = m /\ res = fib n #**/ /**. Derive fibonacci SuchThat (fun_correct! fibonacci) As fibonacci_ok. .**/ { /**. .**/ if (n == 0) /* split */ { /**. .**/ diff --git a/LiveVerif/src/LiveVerifExamples/linked_list.v b/LiveVerif/src/LiveVerifExamples/linked_list.v index 0a74d550..043466b3 100644 --- a/LiveVerif/src/LiveVerifExamples/linked_list.v +++ b/LiveVerif/src/LiveVerifExamples/linked_list.v @@ -5,9 +5,6 @@ Require Import Lia. Load LiveVerif. -(* TODO support functions that don't access any memory *) -Definition dummy: mem -> Prop := emp True. - Record node := { data: word; next: word; diff --git a/LiveVerif/src/LiveVerifExamples/min.v b/LiveVerif/src/LiveVerifExamples/min.v index ef766743..b078f5d4 100644 --- a/LiveVerif/src/LiveVerifExamples/min.v +++ b/LiveVerif/src/LiveVerifExamples/min.v @@ -1,15 +1,11 @@ (* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *) Require Import LiveVerif.LiveVerifLib. Load LiveVerif. -(* TODO support functions that don't access any memory *) -Definition dummy: mem -> Prop := emp True. - #[export] Instance spec_of_u_min: fnspec := .**/ uintptr_t u_min (uintptr_t a, uintptr_t b) /**# - ghost_args := (R: mem -> Prop); - requires t m := sep dummy R m; - ensures t' m' retv := t' = t /\ sep dummy R m' /\ + requires t m := True; + ensures t' m' retv := t' = t /\ m' = m /\ (\[a] < \[b] /\ retv = a \/ \[b] <= \[a] /\ retv = b) #**/ /**. Derive u_min SuchThat (fun_correct! u_min) As u_min_ok. .**/ { /**. .**/ @@ -18,7 +14,7 @@ Derive u_min SuchThat (fun_correct! u_min) As u_min_ok. r = a; /**. .**/ } else { /**. .**/ r = b; /**. .**/ - } /**. .**/ + } /**. .**/ return r; /**. .**/ } /**. Qed. @@ -26,11 +22,8 @@ Qed. #[export] Instance spec_of_u_min3: fnspec := .**/ uintptr_t u_min3 (uintptr_t a, uintptr_t b, uintptr_t c) /**# - ghost_args := (R: mem -> Prop); - requires t m := sep dummy R m; - (* TODO make start_canceling work if just one R, or better, specialcase memoryless - functions with m'=m in postcondition? *) - ensures t' m' retv := t' = t /\ sep dummy R m' /\ + requires t m := True; + ensures t' m' retv := t' = t /\ m' = m /\ \[retv] = Z.min \[a] (Z.min \[b] \[c]) #**/ /**. Derive u_min3 SuchThat (fun_correct! u_min3) As u_min3_ok. .**/ { /**. .**/ @@ -43,9 +36,8 @@ Qed. #[export] Instance spec_of_u_min3_alt: fnspec := .**/ uintptr_t u_min3_alt (uintptr_t a, uintptr_t b, uintptr_t c) /**# - ghost_args := (R: mem -> Prop); - requires t m := sep dummy R m; - ensures t' m' retv := t' = t /\ sep dummy R m' /\ + requires t m := True; + ensures t' m' retv := t' = t /\ m' = m /\ \[retv] = Z.min \[a] (Z.min \[b] \[c]) #**/ /**. Derive u_min3_alt SuchThat (fun_correct! u_min3_alt) As u_min3_alt_ok. .**/ { /**. .**/ diff --git a/bedrock2/src/bedrock2/HeapletwiseHyps.v b/bedrock2/src/bedrock2/HeapletwiseHyps.v index c1067499..0b66a4c0 100644 --- a/bedrock2/src/bedrock2/HeapletwiseHyps.v +++ b/bedrock2/src/bedrock2/HeapletwiseHyps.v @@ -1231,6 +1231,7 @@ Ltac collect_heaplets_into_one_sepclause := eapply start_collecting_heaplets in D; repeat collecting_heaplets_step D; eapply done_collecting_heaplets in D + | |- _ => idtac (* do nothing if this function does not use the heap *) end. Ltac start_canceling_in_hyp H :=