VSU_stdlibAxiomatization of malloc/free/exit
Require Import VST.floyd.proofauto.
Require Import VST.floyd.VSU.
Require Import VC.stdlib.
Require Import VC.Spec_stdlib.
#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Require Import VST.floyd.VSU.
Require Import VC.stdlib.
Require Import VC.Spec_stdlib.
#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
The VSU for external axiomatized functions is much like any
other VSU, except that we use Axioms instead of Definitions
and Lemmas.
Because this VSU does not import any APDs, we don't need a Section.
Normally at this point, we would construct an M showing how the
mem_mgr predicate is implemented. But here we just axiomatize:
Normally at this point, we would prove a semax_body lemma for each
function that the module exports. But here, we use body_lemma_of_funspec
for external functions; and we write this as an axiom:
Axiom body_malloc:
∀ {Espec: OracleKind} {cs: compspecs} ,
VST.floyd.library.body_lemma_of_funspec EF_malloc (snd (malloc_spec_sz M)).
Axiom body_free:
∀ {Espec: OracleKind} {cs: compspecs} ,
VST.floyd.library.body_lemma_of_funspec EF_free (snd (free_spec_sz M)).
Axiom body_exit:
∀ {Espec: OracleKind},
VST.floyd.library.body_lemma_of_funspec
(EF_external "exit" (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
(snd (exit_spec)).
∀ {Espec: OracleKind} {cs: compspecs} ,
VST.floyd.library.body_lemma_of_funspec EF_malloc (snd (malloc_spec_sz M)).
Axiom body_free:
∀ {Espec: OracleKind} {cs: compspecs} ,
VST.floyd.library.body_lemma_of_funspec EF_free (snd (free_spec_sz M)).
Axiom body_exit:
∀ {Espec: OracleKind},
VST.floyd.library.body_lemma_of_funspec
(EF_external "exit" (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
(snd (exit_spec)).
Internal functions
Definition MF_ASI: funspecs := MallocFreeASI M.
Definition MF_imported_specs:funspecs := nil.
Definition MF_internal_specs: funspecs := placeholder_spec::MF_ASI.
Definition MF_globals: globals → mpred:= Spec_stdlib.mem_mgr M.
Definition MFVprog : varspecs. mk_varspecs prog. Defined.
Definition MFGprog: funspecs := MF_imported_specs ++ MF_internal_specs.
Definition MF_imported_specs:funspecs := nil.
Definition MF_internal_specs: funspecs := placeholder_spec::MF_ASI.
Definition MF_globals: globals → mpred:= Spec_stdlib.mem_mgr M.
Definition MFVprog : varspecs. mk_varspecs prog. Defined.
Definition MFGprog: funspecs := MF_imported_specs ++ MF_internal_specs.
Constructing the Component and the VSU
Lemma semax_func_cons_malloc_aux {cs: compspecs} (gv: globals)
(gx : genviron) (ret : option val) n:
(EX x : val,
(PROP ( )
RETURN (x) SEP (mem_mgr M gv;
if eq_dec x nullval
then emp
else malloc_token_sz M Ews n x × memory_block Ews n x))
(make_ext_rval gx (rettype_of_type (tptr tvoid)) ret)) &&
!! Builtins0.val_opt_has_rettype ret
(rettype_of_type (tptr tvoid))
|-- !! tc_option_val (tptr tvoid) ret.
Proof.
intros.
Intros p.
rewrite <- insert_local.
rewrite lower_andp.
apply derives_extract_prop; intro.
red in H0; unfold_lift in H0; destruct H0.
destruct ret; try contradiction.
unfold eval_id in H0; simpl in H0. subst v.
if_tac. rewrite H0; entailer!.
renormalize. entailer!.
simpl. auto.
Qed.
Definition MF_E : funspecs := MF_ASI.
(gx : genviron) (ret : option val) n:
(EX x : val,
(PROP ( )
RETURN (x) SEP (mem_mgr M gv;
if eq_dec x nullval
then emp
else malloc_token_sz M Ews n x × memory_block Ews n x))
(make_ext_rval gx (rettype_of_type (tptr tvoid)) ret)) &&
!! Builtins0.val_opt_has_rettype ret
(rettype_of_type (tptr tvoid))
|-- !! tc_option_val (tptr tvoid) ret.
Proof.
intros.
Intros p.
rewrite <- insert_local.
rewrite lower_andp.
apply derives_extract_prop; intro.
red in H0; unfold_lift in H0; destruct H0.
destruct ret; try contradiction.
unfold eval_id in H0; simpl in H0. subst v.
if_tac. rewrite H0; entailer!.
renormalize. entailer!.
simpl. auto.
Qed.
Definition MF_E : funspecs := MF_ASI.
Each VSU may have private global variables that constitute its
"local state". This VSU_initializer lemma calculates how to
reason about their initial values. But the module stdlib.c does
not have any global variables, so this initialize lemma is
rather trivial here. See VSU_stdlib2.v, lemma initialize,
for a more interesting example.
Now that all the subcomponents are ready, we can bundle up the VSU:
Definition MallocFreeVSU: @VSU NullExtension.Espec
MF_E MF_imported_specs ltac:(QPprog prog) MF_ASI MF_globals.
Proof.
mkVSU prog MF_internal_specs.
- solve_SF_external (@body_malloc NullExtension.Espec CompSpecs).
apply (semax_func_cons_malloc_aux gv gx ret n).
- solve_SF_external (@body_free NullExtension.Espec CompSpecs).
- solve_SF_external (@body_exit NullExtension.Espec).
- apply initialize.
Qed.
MF_E MF_imported_specs ltac:(QPprog prog) MF_ASI MF_globals.
Proof.
mkVSU prog MF_internal_specs.
- solve_SF_external (@body_malloc NullExtension.Espec CompSpecs).
apply (semax_func_cons_malloc_aux gv gx ret n).
- solve_SF_external (@body_free NullExtension.Espec CompSpecs).
- solve_SF_external (@body_exit NullExtension.Espec).
- apply initialize.
Qed.
Next Chapter: VSU_main
(* 2023-03-25 11:30 *)