From 49f759ebbb3eb569c456a9dbe6affd165f3fc8b5 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 4 Jun 2021 19:08:44 +0200 Subject: starting refinement of symbolic execution --- scheduling/BTL_SEsimuref.v | 109 +++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 106 insertions(+), 3 deletions(-) (limited to 'scheduling/BTL_SEsimuref.v') 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 +*) + -- cgit