diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-04 19:08:44 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-04 19:10:51 +0200 |
commit | 49f759ebbb3eb569c456a9dbe6affd165f3fc8b5 (patch) | |
tree | a006b0005d5c14a11460598855af9a26ad75baea /scheduling | |
parent | 867aba987318b55173514a6a91859cfb1eeba900 (diff) | |
download | compcert-kvx-49f759ebbb3eb569c456a9dbe6affd165f3fc8b5.tar.gz compcert-kvx-49f759ebbb3eb569c456a9dbe6affd165f3fc8b5.zip |
starting refinement of symbolic execution
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/BTL_SEsimuref.v | 109 | ||||
-rw-r--r-- | scheduling/BTL_SEtheory.v | 18 |
2 files changed, 115 insertions, 12 deletions
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index a4da4291..6d74ccf9 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -1,13 +1,18 @@ (** Refinement of BTL_SEtheory data-structures in order to introduce (and prove correct) a lower-level specification of the simulation test. - Ceci est un "bac à sable". TODO: A REVOIR COMPLETEMENT. Introduire "fake" hash-consing + Ceci est un "bac à sable". - On introduit une représentation plus concrète pour les types d'état symbolique [sistate] et [sstate]. - Etant donné une spécification intuitive "*_simu" pour tester la simulation sur cette représentation des états symboliques, on essaye déjà de trouver les bonnes notions de raffinement "*_refines" qui permette de prouver les lemmes "*_simu_correct". - Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement ! + TODO: A REVOIR COMPLETEMENT. + - essayer de découper chaque relation de raffinement en une fonction "projection/abstraction" (à la "hsval_proj" à renommer en "hsval_abstract") + et une équivalence sur la représentation abstraite. + - introduire "fake" hash-consed values (à renommer en "refined" plutôt que "fake"). + *) Require Import Coqlib Maps Floats. @@ -15,7 +20,7 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import Op Registers. Require Import RTL BTL OptionMonad BTL_SEtheory. -(** * ... *) +(** * Refinement of data-structures and of the specification of the simulation test *) Record sis_ok ctx (sis: sistate): Prop := { OK_PRE: (sis.(si_pre) ctx); @@ -254,6 +259,103 @@ Proof. * exploit IHrst_simu2; eauto. Qed. +(** * Refinement of the symbolic execution *) + +Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core. + +Lemma eval_list_sval_refpreserv ctx args ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + eval_list_sval ctx (list_sval_inj (map ris args)) = + eval_list_sval ctx (list_sval_inj (map sis args)). +Proof. + intros REF OK. + induction args; simpl; eauto. + intros; erewrite REG_EQ, IHargs; eauto. +Qed. + +Local Hint Resolve eval_list_sval_refpreserv: core. + +Lemma eval_builtin_sval_refpreserv ctx arg ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + eval_builtin_sval ctx (builtin_arg_map ris arg) = eval_builtin_sval ctx (builtin_arg_map sis arg). +Proof. + intros REF OK; induction arg; simpl; eauto. + + erewrite REG_EQ; eauto. + + erewrite IHarg1, IHarg2; eauto. + + erewrite IHarg1, IHarg2; eauto. +Qed. + +Lemma bargs_refpreserv ctx args ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + bargs_refines ctx (map (builtin_arg_map ris) args) (map (builtin_arg_map sis) args). +Proof. + unfold bargs_refines. intros REF OK. + induction args; simpl; eauto. + erewrite eval_builtin_sval_refpreserv, IHargs; eauto. +Qed. + +Local Hint Resolve bargs_refpreserv: core. + +Lemma exec_final_refpreserv ctx i ris sis: + ris_refines ctx ris sis -> + ris_ok ctx ris -> + rfv_refines ctx (sexec_final_sfv i ris) (sexec_final_sfv i sis). +Proof. + destruct i; simpl; unfold sum_left_map; try autodestruct; eauto. +Qed. + +Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ris_ok_sval := nil; ris_sreg := PTree.empty _ |}. + +Lemma ris_init_correct ctx: + ris_refines ctx ris_init sis_init. +Proof. + unfold ris_init, sis_init; econstructor; simpl in *; eauto. + + split; destruct 1; econstructor; simpl in *; eauto. + congruence. + + destruct 1; simpl in *. unfold ris_sreg_get; simpl. + intros; rewrite PTree.gempty; eauto. + + try_simplify_someHyps. +Qed. + +Definition rset_smem rm (ris:ristate): ristate := + {| ris_smem := rm; + ris_input_init := ris.(ris_input_init); + ris_ok_sval := ris.(ris_ok_sval); + ris_sreg:= ris.(ris_sreg) + |}. + +Lemma sis_ok_set_mem ctx sm sis: + sis_ok ctx (set_smem sm sis) + <-> (sis_ok ctx sis /\ eval_smem ctx sm <> None). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. + intuition eauto. +Qed. + +Lemma ris_ok_set_mem ctx rm (ris: ristate): + (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) -> + ris_ok ctx (rset_smem rm ris) + <-> (ris_ok ctx ris /\ eval_smem ctx rm <> None). +Proof. + split; destruct 1; econstructor; simpl in *; eauto. +Qed. + +Lemma rset_mem_refpreserv ctx rm sm ris sis: + (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) -> + (forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs) -> + ris_refines ctx ris sis -> + (ris_ok ctx ris -> eval_smem ctx rm = eval_smem ctx sm) -> + ris_refines ctx (rset_smem rm ris) (set_smem sm sis). +Proof. + destruct 3; intros. + econstructor; eauto. + + rewrite sis_ok_set_mem, ris_ok_set_mem; intuition congruence. + + rewrite ris_ok_set_mem; intuition eauto. + + rewrite ris_ok_set_mem; intuition eauto. +Qed. (** TODO: could be useful ? Lemma seval_condition_valid_preserv ctx cond args sm b @@ -268,4 +370,5 @@ Proof. eapply cond_valid_pointer_eq; intros. exploit VALID_PRESERV; eauto. Qed. -*)
\ No newline at end of file +*) + diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 9ab64d7d..4b4571e4 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -437,7 +437,7 @@ Inductive sem_sfval ctx stk: sfval -> regset -> mem -> trace -> state -> Prop := (* Syntax and Semantics of symbolic internal states *) (* [si_pre] is a precondition on initial context *) -Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg: reg -> sval; si_smem: smem }. +Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg:> reg -> sval; si_smem: smem }. (* Predicate on which (rs, m) is a possible final state after evaluating [st] on ((crs0 ctx), (cm0 ctx)) *) Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop := @@ -446,25 +446,25 @@ Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop := /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r). (** * Symbolic execution of final step *) -Definition sexec_final_sfv (i: final) (sis: sistate): sfval := +Definition sexec_final_sfv (i: final) (sreg: reg -> sval): sfval := match i with | Bgoto pc => Sgoto pc | Bcall sig ros args res pc => - let svos := sum_left_map sis.(si_sreg) ros in - let sargs := list_sval_inj (List.map sis.(si_sreg) args) in + let svos := sum_left_map sreg ros in + let sargs := list_sval_inj (List.map sreg args) in Scall sig svos sargs res pc | Btailcall sig ros args => - let svos := sum_left_map sis.(si_sreg) ros in - let sargs := list_sval_inj (List.map sis.(si_sreg) args) in + let svos := sum_left_map sreg ros in + let sargs := list_sval_inj (List.map sreg args) in Stailcall sig svos sargs | Bbuiltin ef args res pc => - let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in + let sargs := List.map (builtin_arg_map sreg) args in Sbuiltin ef sargs res pc | Breturn or => - let sor := SOME r <- or IN Some (sis.(si_sreg) r) in + let sor := SOME r <- or IN Some (sreg r) in Sreturn sor | Bjumptable reg tbl => - let sv := sis.(si_sreg) reg in + let sv := sreg reg in Sjumptable sv tbl end. |