From 388a5077d75e6021611abf1301e16ad39e9f3770 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 7 May 2021 15:52:44 +0200 Subject: start a model of symbolic execution in Continuation-Passing-Style --- scheduling/BTL_SEtheory.v | 251 ++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 233 insertions(+), 18 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 4d5314f2..8aa8f32b 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -13,12 +13,11 @@ Require Import RTL BTL OptionMonad. Ltac inversion_SOME := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) Ltac inversion_ASSERT := fail. (* deprecated tactic of OptionMonad: use autodestruct instead *) - Record iblock_exec_context := Bctx { cge: BTL.genv; - csp: val; cstk: list stackframe; cf: function; + csp: val; crs0: regset; cm0: mem }. @@ -454,17 +453,17 @@ Proof. reflexivity. Qed. -Variable sp: val. Variable stk stk': list stackframe. Variable f f': function. +Variable sp: val. Variable rs0: regset. Variable m0: mem. Lemma eval_sval_preserved sv: - eval_sval (Bctx ge sp stk f rs0 m0) sv = eval_sval (Bctx ge' sp stk' f' rs0 m0) sv. + eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv. Proof. - induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge sp stk f rs0 m0) lsv = eval_list_sval (Bctx ge' sp stk' f' rs0 m0) lsv) - (P1 := fun sm => eval_smem (Bctx ge sp stk f rs0 m0) sm = eval_smem (Bctx ge' sp stk' f' rs0 m0) sm); simpl; auto. + induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv) + (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto. + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto. rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto. erewrite eval_operation_preserved; eauto. @@ -482,8 +481,8 @@ Proof. Qed. Lemma seval_builtin_arg_preserved m: forall bs varg, - seval_builtin_arg (Bctx ge sp stk f rs0 m0) m bs varg -> - seval_builtin_arg (Bctx ge' sp stk' f' rs0 m0) m bs varg. + seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg -> + seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg. Proof. induction 1; simpl. all: try (constructor; auto). @@ -493,15 +492,15 @@ Proof. Qed. Lemma seval_builtin_args_preserved m lbs vargs: - seval_builtin_args (Bctx ge sp stk f rs0 m0) m lbs vargs -> - seval_builtin_args (Bctx ge' sp stk' f' rs0 m0) m lbs vargs. + seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs -> + seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs. Proof. induction 1; constructor; eauto. eapply seval_builtin_arg_preserved; auto. Qed. Lemma list_sval_eval_preserved lsv: - eval_list_sval (Bctx ge sp stk f rs0 m0) lsv = eval_list_sval (Bctx ge' sp stk' f' rs0 m0) lsv. + eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv. Proof. induction lsv; simpl; auto. rewrite eval_sval_preserved. destruct (eval_sval _ _); auto. @@ -509,7 +508,7 @@ Proof. Qed. Lemma smem_eval_preserved sm: - eval_smem (Bctx ge sp stk f rs0 m0) sm = eval_smem (Bctx ge' sp stk' f' rs0 m0) sm. + eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm. Proof. induction sm; simpl; auto. rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. @@ -520,7 +519,7 @@ Proof. Qed. Lemma seval_condition_preserved cond lsv sm: - seval_condition (Bctx ge sp stk f rs0 m0) cond lsv sm = seval_condition (Bctx ge' sp stk' f' rs0 m0) cond lsv sm. + seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm. Proof. unfold seval_condition. rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. @@ -618,19 +617,235 @@ Proof. congruence. Qed. + +(** * symbolic execution of basic instructions *) + +Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}. + +Lemma sis_init_correct ctx: + sem_sistate ctx sis_init (crs0 ctx) (cm0 ctx). +Proof. + unfold sis_init, sem_sistate; simpl; intuition eauto. +Qed. + +Definition set_sreg (r:reg) (sv:sval) (sis:sistate): sistate := + {| si_pre:=(fun ctx => eval_sval ctx (sis.(si_sreg) r) <> None /\ (sis.(si_pre) ctx)); + si_sreg:=fun y => if Pos.eq_dec r y then sv else sis.(si_sreg) y; + si_smem:= sis.(si_smem)|}. + +Lemma set_sreg_correct ctx dst sv sis (rs rs': regset) m: + sem_sistate ctx sis rs m -> + (eval_sval ctx sv = Some rs' # dst) -> + (forall r, r <> dst -> rs'#r = rs#r) -> + sem_sistate ctx (set_sreg dst sv sis) rs' m. +Proof. + intros (PRE&MEM®) NEW OLD. + unfold sem_sistate, set_sreg; simpl. + intuition. + - rewrite REG in *; congruence. + - destruct (Pos.eq_dec dst r); simpl; subst; eauto. + rewrite REG in *. rewrite OLD; eauto. +Qed. + +Definition set_smem (sm:smem) (sis:sistate): sistate := + {| si_pre:=(fun ctx => eval_smem ctx sis.(si_smem) <> None /\ (sis.(si_pre) ctx)); + si_sreg:= sis.(si_sreg); + si_smem:= sm |}. + +Lemma set_smem_correct ctx sm sis rs m m': + sem_sistate ctx sis rs m -> + eval_smem ctx sm = Some m' -> + sem_sistate ctx (set_smem sm sis) rs m'. +Proof. + intros (PRE&MEM®) NEW. + unfold sem_sistate, set_smem; simpl. + intuition. + rewrite MEM in *; congruence. +Qed. + +Definition sexec_op op args dst sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + set_sreg dst (Sop op args sis.(si_smem)) sis. + +Lemma sexec_op_correct ctx op args dst sis rs m v + (EVAL: eval_operation (cge ctx) (csp ctx) op rs ## args m = Some v) + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_op op args dst sis) (rs#dst <- v) m). +Proof. + eapply set_sreg_correct; eauto. + - simpl. destruct SIS as (PRE&MEM®). + rewrite Regmap.gss; simpl; auto. + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + - intros; rewrite Regmap.gso; auto. +Qed. + +Definition sexec_load trap chunk addr args dst sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + set_sreg dst (Sload sis.(si_smem) trap chunk addr args) sis. + +Lemma sexec_load_TRAP_correct ctx chunk addr args dst sis rs m a v + (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a) + (LOAD: Mem.loadv chunk m a = Some v) + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_load TRAP chunk addr args dst sis) (rs#dst <- v) m). +Proof. + eapply set_sreg_correct; eauto. + - simpl. destruct SIS as (PRE&MEM®). + rewrite Regmap.gss; simpl; auto. + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + - intros; rewrite Regmap.gso; auto. +Qed. + +Definition sexec_store chunk addr args src sis: sistate := + let args := list_sval_inj (List.map sis.(si_sreg) args) in + let src := sis.(si_sreg) src in + let sm := Sstore sis.(si_smem) chunk addr args src in + set_smem sm sis. + +Lemma sexec_store_correct ctx chunk addr args src sis rs m m' a + (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a) + (STORE: Mem.storev chunk m a (rs # src) = Some m') + (SIS: sem_sistate ctx sis rs m) + :(sem_sistate ctx (sexec_store chunk addr args src sis) rs m'). +Proof. + eapply set_smem_correct; eauto. + simpl. destruct SIS as (PRE&MEM®). + erewrite eval_list_sval_inj; simpl; auto. + try_simplify_someHyps. + rewrite REG; auto. +Qed. + +Lemma seval_condition_eq ctx cond args sis rs m + (SIS : sem_sistate ctx sis rs m) + :seval_condition ctx cond (list_sval_inj (map (si_sreg sis) args)) (si_smem sis) = eval_condition cond rs ## args m. +Proof. + destruct SIS as (PRE&MEM®); unfold seval_condition; simpl. + erewrite eval_list_sval_inj; simpl; auto. + erewrite MEM; auto. +Qed. + +(** * symbolic execution of blocks *) + (* symbolic state *) Inductive sstate := | Sfinal (sis: sistate) (sfv: sfval) | Scond (cond: condition) (args: list_sval) (sm: smem) (ifso ifnot: sstate) + | Sdead . -Inductive sem_internal_sstate ctx rs m t s: sstate -> Prop := - | sem_Sfinal sis sfv +(* transition (t,s) produced by a sstate in initial context ctx *) +Inductive sem_sstate ctx t s: sstate -> Prop := + | sem_Sfinal sis sfv rs m (SIS: sem_sistate ctx sis rs m) (SFV: sem_sfval ctx sfv rs m t s) - : sem_internal_sstate ctx rs m t s (Sfinal sis sfv) + : sem_sstate ctx t s (Sfinal sis sfv) | sem_Scond b cond args sm ifso ifnot (SEVAL: seval_condition ctx cond args sm = Some b) - (SELECT: sem_internal_sstate ctx rs m t s (if b then ifso else ifnot)) - : sem_internal_sstate ctx rs m t s (Scond cond args sm ifso ifnot) + (SELECT: sem_sstate ctx t s (if b then ifso else ifnot)) + : sem_sstate ctx t s (Scond cond args sm ifso ifnot) + (* NB: Sdead: fails to produce a transition *) . + +(** * Idée de l'execution symbolique en Continuation Passing Style + +[k] ci-dessous est la continuation (c-a-d. la suite de la construction de l'arbre qu'on va appliquer dans chaque branche) + +Rem: si manipuler une telle continuation s'avère compliqué dans les preuves, +il faudra faire autrement dans le modèle -- par exemple avec une structure de donnée +pour représenter l'ensemble des chemins. +(même si on peut conserver le CPS dans l'implem finale, pour l'efficacité). + +*) + +Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := + match ib with + | BF fin => Sfinal sis (sexec_final_sfv fin sis) + (* basic instructions *) + | Bnop => k sis + | Bop op args res => k (sexec_op op args res sis) + | Bload TRAP chunk addr args dst => k (sexec_load TRAP chunk addr args dst sis) + | Bload NOTRAP chunk addr args dst => Sdead (* TODO *) + | Bstore chunk addr args src => k (sexec_store chunk addr args src sis) + (* composed instructions *) + | Bseq ib1 ib2 => + sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) + | Bcond cond args ifso ifnot _ => + let args := list_sval_inj (List.map sis.(si_sreg) args) in + let ifso := sexec_rec ifso sis k in + let ifnot := sexec_rec ifnot sis k in + Scond cond args sis.(si_smem) ifso ifnot + end + . + +Definition sexec ib := sexec_rec ib sis_init (fun _ => Sdead). + +Local Hint Constructors sem_sstate: core. +Local Hint Resolve sexec_final_svf_correct sis_init_correct: core. + +Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin + (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): + forall k + (CONT: forall sis, ofin = None -> sem_sistate ctx sis rs1 m1 -> sem_sstate ctx t s (k sis)) + sis + (SIS: sem_sistate ctx sis rs m) + , match ofin with + | Some fin => + final_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s -> + sem_sstate ctx t s (sexec_rec ib sis k) + | None => sem_sstate ctx t s (sexec_rec ib sis k) + end. +Proof. + induction ISTEP; simpl; eauto. + - (* op *) + intros; eapply CONT; eauto. + eapply sexec_op_correct; eauto. + - (* load *) + intros; eapply CONT; eauto. + eapply sexec_load_TRAP_correct; eauto. + - (* store *) + intros; eapply CONT; eauto. + eapply sexec_store_correct; eauto. + - (* seq_stop *) + intros; eapply IHISTEP; eauto. + try congruence. + - (* seq_continue *) + intros. destruct ofin as [fin|]. + + (* Some *) + clear CONT. + intros; eapply IHISTEP1; eauto. + intros; eapply IHISTEP2; eauto. + try congruence. + + (* None *) + intros; eapply IHISTEP1; eauto. + - (* cond *) + intros. + assert (IFEQ: (if b then sexec_rec ifso sis k else sexec_rec ifnot sis k) = sexec_rec (if b then ifso else ifnot) sis k). + { destruct b; simpl; auto. } + destruct ofin as [fin|]. + + (* Some *) + clear CONT. + intro FSTEP; eapply sem_Scond; eauto. + * erewrite seval_condition_eq; eauto. + * rewrite IFEQ. + eapply IHISTEP; eauto. + try congruence. + + (* None *) + eapply sem_Scond; eauto. + * erewrite seval_condition_eq; eauto. + * rewrite IFEQ. + eapply IHISTEP; eauto. +Qed. + +(* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) + (sexec is a correct over-approximation) +*) +Theorem sexec_correct ctx ib t s: + iblock_step (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s -> + sem_sstate ctx t s (sexec ib). +Proof. + destruct 1 as (rs' & m' & fin & ISTEP & FSTEP). + unfold sexec. + exploit sexec_rec_correct; simpl; eauto || congruence. +Qed. -- cgit