diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 16:25:33 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 16:25:33 +0200 |
commit | 9c01536d6bb0696091228cb4a4d52cdcd0c55416 (patch) | |
tree | cb4d817bc4c899c8e32a6694a00295b18a78b40f /scheduling | |
parent | b03e5a23bbe1370ba0cbb417d81a4505c317da9a (diff) | |
download | compcert-kvx-9c01536d6bb0696091228cb4a4d52cdcd0c55416.tar.gz compcert-kvx-9c01536d6bb0696091228cb4a4d52cdcd0c55416.zip |
add hid in BTL_SEtheory: this avoids duplication of types (and should not be harmful)
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/BTL_SEsimuref.v | 38 | ||||
-rw-r--r-- | scheduling/BTL_SEtheory.v | 269 |
2 files changed, 157 insertions, 150 deletions
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index da680e63..9c84532b 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -1,13 +1,5 @@ (** 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". - - - 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 ! - *) Require Import Coqlib Maps Floats. @@ -41,7 +33,7 @@ Record ristate := Definition ris_sreg_get (ris: ristate) r: sval := match PTree.get r ris with - | None => if ris_input_init ris then Sinput r else Sundef + | None => if ris_input_init ris then fSinput r else fSundef | Some sv => sv end. Coercion ris_sreg_get: ristate >-> Funclass. @@ -211,7 +203,7 @@ Fixpoint get_routcome ctx (rst:rstate): option routcome := match rst with | Rfinal ris rfv => Some (rout ris rfv) | Rcond cond args ifso ifnot => - SOME b <- seval_condition ctx cond args IN + SOME b <- eval_scondition ctx cond args IN get_routcome ctx (if b then ifso else ifnot) | Rabort => None end. @@ -241,7 +233,7 @@ Lemma rst_simu_lroutcome rst1 rst2: exists ris2 rfv2, get_routcome (bctx2 ctx) rst2 = Some (rout ris2 rfv2) /\ ris_simu ris1 ris2 /\ rfv_simu rfv1 rfv2. Proof. induction 1; simpl; intros f1 f2 ctx lris1 lrfv1 ROUT; try_simplify_someHyps. - erewrite <- seval_condition_preserved. + erewrite <- eval_scondition_preserved. autodestruct. destruct b; simpl; auto. Qed. @@ -252,9 +244,9 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop := (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv) : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv) | Refcond cond rargs args rifso rifnot ifso ifnot - (RCOND: seval_condition ctx cond rargs = seval_condition ctx cond args) - (REFso: seval_condition ctx cond rargs = Some true -> rst_refines ctx rifso ifso) - (REFnot: seval_condition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot) + (RCOND: eval_scondition ctx cond rargs = eval_scondition ctx cond args) + (REFso: eval_scondition ctx cond rargs = Some true -> rst_refines ctx rifso ifso) + (REFnot: eval_scondition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot) : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args ifso ifnot) | Refabort : rst_refines ctx Rabort Sabort @@ -464,7 +456,7 @@ Proof. destruct i; simpl; unfold sum_left_map; try autodestruct; eauto. Qed. -Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ok_rsval := nil; ris_sreg := PTree.empty _ |}. +Definition ris_init: ristate := {| ris_smem:= fSinit; ris_input_init:=true; ok_rsval := nil; ris_sreg := PTree.empty _ |}. Lemma ris_init_correct ctx: ris_refines ctx ris_init sis_init. @@ -507,7 +499,7 @@ Qed. Definition rexec_store chunk addr args src ris: ristate := let args := list_sval_inj (List.map (ris_sreg_get ris) args) in let src := ris_sreg_get ris src in - let rm := Sstore ris.(ris_smem) chunk addr args src in + let rm := fSstore ris.(ris_smem) chunk addr args src in rset_smem rm ris. Lemma rexec_store_correct ctx chunk addr args src ris sis: @@ -554,7 +546,7 @@ Qed. Definition rexec_op op args dst (ris:ristate): ristate := let args := list_sval_inj (List.map ris args) in - rset_sreg dst (Sop op args) ris. + rset_sreg dst (fSop op args) ris. Lemma rexec_op_correct ctx op args dst ris sis: ris_refines ctx ris sis -> @@ -566,7 +558,7 @@ Qed. Definition rexec_load trap chunk addr args dst (ris:ristate): ristate := let args := list_sval_inj (List.map ris args) in - rset_sreg dst (Sload ris.(ris_smem) trap chunk addr args) ris. + rset_sreg dst (fSload ris.(ris_smem) trap chunk addr args) ris. Lemma rexec_load_correct ctx trap chunk addr args dst ris sis: ris_refines ctx ris sis -> @@ -576,12 +568,12 @@ Proof. intros OK; erewrite eval_list_sval_refpreserv, MEM_EQ; eauto. Qed. -Lemma seval_condition_refpreserv ctx cond args ris sis: +Lemma eval_scondition_refpreserv ctx cond args ris sis: ris_refines ctx ris sis -> ris_ok ctx ris -> - seval_condition ctx cond (list_sval_inj (map ris args)) = seval_condition ctx cond (list_sval_inj (map sis args)). + eval_scondition ctx cond (list_sval_inj (map ris args)) = eval_scondition ctx cond (list_sval_inj (map sis args)). Proof. - intros; unfold seval_condition. + intros; unfold eval_scondition. erewrite eval_list_sval_refpreserv; eauto. Qed. @@ -745,7 +737,7 @@ Proof. generalize OUT; clear OUT; simpl. autodestruct. intros COND; generalize COND. - erewrite <- seval_condition_refpreserv; eauto. + erewrite <- eval_scondition_refpreserv; eauto. econstructor; try_simplify_someHyps. Qed. @@ -823,7 +815,7 @@ Proof. generalize OUT; clear OUT; simpl. autodestruct. intros COND; generalize COND. - erewrite seval_condition_refpreserv; eauto. + erewrite eval_scondition_refpreserv; eauto. econstructor; try_simplify_someHyps. Qed. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 5a94b235..2a335790 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -13,54 +13,77 @@ Require Import Coqlib Maps Floats. Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import Op Registers. Require Import RTL BTL OptionMonad. +Require Export Impure.ImpHCons. +Import HConsing. +(** * Syntax and semantics of symbolic values *) + +(** The semantics of symbolic execution is parametrized by the context of the execution of a block *) Record iblock_exec_context := Bctx { - cge: BTL.genv; - (* cstk: list stackframe; *) (* having the stack here does seem not a good idea *) - cf: function; - csp: val; - crs0: regset; - cm0: mem + cge: BTL.genv; (** usual environment for identifiers *) + cf: function; (** ambient function of the block *) + csp: val; (** stack pointer *) + crs0: regset; (** initial state of registers (at the block entry) *) + cm0: mem (** initial memory state *) }. -(** * Syntax and semantics of symbolic values *) -(* TODO: introduire les hash-code directement ici - avec les "fake" smart constructors qui mettent un unknown_hid ? *) - -(* symbolic value *) +(** symbolic value *) Inductive sval := - | Sundef - | Sinput (r: reg) - | Sop (op:operation) (lsv: list_sval) - | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) -with list_sval := - | Snil - | Scons (sv: sval) (lsv: list_sval) -(* symbolic memory *) + | Sundef (hid: hashcode) + | Sinput (r: reg) (hid: hashcode) + | Sop (op:operation) (lsv: list_sval) (hid: hashcode) + | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (hid: hashcode) +(** list of symbolic values *) +with list_sval := + | Snil (hid: hashcode) + | Scons (sv: sval) (lsv: list_sval) (hid: hashcode) +(** symbolic memory *) with smem := - | Sinit - | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval). + | Sinit (hid: hashcode) + | Sstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval) (hid: hashcode) +. Scheme sval_mut := Induction for sval Sort Prop with list_sval_mut := Induction for list_sval Sort Prop with smem_mut := Induction for smem Sort Prop. +(** "fake" smart-constructors using an [unknown_hid] instead of the one provided by hash-consing. +These smart-constructors are those used in the abstract model of symbolic execution. +They will also appear in the implementation of rewriting rules (in order to avoid hash-consing handling +in proofs of rewriting rules). +*) + +Definition fSundef := Sundef unknown_hid. +Definition fSinput (r: reg) := Sinput r unknown_hid. +Definition fSop (op:operation) (lsv: list_sval) := Sop op lsv unknown_hid. +Definition fSload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) + := Sload sm trap chunk addr lsv unknown_hid. + +Definition fSnil := Snil unknown_hid. +Definition fScons (sv: sval) (lsv: list_sval) := Scons sv lsv unknown_hid. + +Definition fSinit := Sinit unknown_hid. +Definition fSstore (sm: smem) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) (srce: sval) + := Sstore sm chunk addr lsv srce unknown_hid. + Fixpoint list_sval_inj (l: list sval): list_sval := match l with - | nil => Snil - | v::l => Scons v (list_sval_inj l) + | nil => fSnil + | v::l => fScons v (list_sval_inj l) end. Local Open Scope option_monad_scope. +(** Semantics *) Fixpoint eval_sval ctx (sv: sval): option val := match sv with - | Sundef => Some Vundef - | Sinput r => Some ((crs0 ctx)#r) - | Sop op l => + | Sundef _ => Some Vundef + | Sinput r _ => Some ((crs0 ctx)#r) + | Sop op l _ => SOME args <- eval_list_sval ctx l IN eval_operation (cge ctx) (csp ctx) op args (cm0 ctx) - | Sload sm trap chunk addr lsv => + | Sload sm trap chunk addr lsv _ => match trap with | TRAP => SOME args <- eval_list_sval ctx lsv IN @@ -82,16 +105,16 @@ Fixpoint eval_sval ctx (sv: sval): option val := end with eval_list_sval ctx (lsv: list_sval): option (list val) := match lsv with - | Snil => Some nil - | Scons sv lsv' => + | Snil _ => Some nil + | Scons sv lsv' _ => SOME v <- eval_sval ctx sv IN SOME lv <- eval_list_sval ctx lsv' IN Some (v::lv) end with eval_smem ctx (sm: smem): option mem := match sm with - | Sinit => Some (cm0 ctx) - | Sstore sm chunk addr lsv srce => + | Sinit _ => Some (cm0 ctx) + | Sstore sm chunk addr lsv srce _ => SOME args <- eval_list_sval ctx lsv IN SOME a <- eval_addressing (cge ctx) (csp ctx) addr args IN SOME m <- eval_smem ctx sm IN @@ -99,7 +122,12 @@ with eval_smem ctx (sm: smem): option mem := Mem.storev chunk m a sv end. +(** The symbolic memory preserves predicate Mem.valid_pointer with respect to initial memory. + Hence, arithmetic operations and Boolean conditions do not depend on the current memory of the block + (their semantics only depends on the initial memory of the block). + The correctness of this idea is proved on lemmas [sexec_op_correct] and [eval_scondition_eq]. +*) Lemma valid_pointer_preserv ctx sm: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer (cm0 ctx) b ofs = Mem.valid_pointer m b ofs. Proof. @@ -116,7 +144,7 @@ Proof. intros H; induction l as [|r l]; simpl; repeat autodestruct; auto. Qed. -Definition seval_condition ctx (cond: condition) (lsv: list_sval): option bool := +Definition eval_scondition ctx (cond: condition) (lsv: list_sval): option bool := SOME args <- eval_list_sval ctx lsv IN eval_condition cond args (cm0 ctx). @@ -124,60 +152,60 @@ Definition seval_condition ctx (cond: condition) (lsv: list_sval): option bool : (** * Auxiliary definitions on Builtins *) (* TODO: clean this. Some generic stuffs could be put in [AST.v] *) -Section SEVAL_BUILTIN_ARG. (* adapted from Events.v *) +Section EVAL_BUILTIN_SARG. (* adapted from Events.v *) Variable ctx: iblock_exec_context. Variable m: mem. -Inductive seval_builtin_arg: builtin_arg sval -> val -> Prop := +Inductive eval_builtin_sarg: builtin_arg sval -> val -> Prop := | seval_BA: forall x v, eval_sval ctx x = Some v -> - seval_builtin_arg (BA x) v + eval_builtin_sarg (BA x) v | seval_BA_int: forall n, - seval_builtin_arg (BA_int n) (Vint n) + eval_builtin_sarg (BA_int n) (Vint n) | seval_BA_long: forall n, - seval_builtin_arg (BA_long n) (Vlong n) + eval_builtin_sarg (BA_long n) (Vlong n) | seval_BA_float: forall n, - seval_builtin_arg (BA_float n) (Vfloat n) + eval_builtin_sarg (BA_float n) (Vfloat n) | seval_BA_single: forall n, - seval_builtin_arg (BA_single n) (Vsingle n) + eval_builtin_sarg (BA_single n) (Vsingle n) | seval_BA_loadstack: forall chunk ofs v, Mem.loadv chunk m (Val.offset_ptr (csp ctx) ofs) = Some v -> - seval_builtin_arg (BA_loadstack chunk ofs) v + eval_builtin_sarg (BA_loadstack chunk ofs) v | seval_BA_addrstack: forall ofs, - seval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs) + eval_builtin_sarg (BA_addrstack ofs) (Val.offset_ptr (csp ctx) ofs) | seval_BA_loadglobal: forall chunk id ofs v, Mem.loadv chunk m (Senv.symbol_address (cge ctx) id ofs) = Some v -> - seval_builtin_arg (BA_loadglobal chunk id ofs) v + eval_builtin_sarg (BA_loadglobal chunk id ofs) v | seval_BA_addrglobal: forall id ofs, - seval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address (cge ctx) id ofs) + eval_builtin_sarg (BA_addrglobal id ofs) (Senv.symbol_address (cge ctx) id ofs) | seval_BA_splitlong: forall hi lo vhi vlo, - seval_builtin_arg hi vhi -> seval_builtin_arg lo vlo -> - seval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo) + eval_builtin_sarg hi vhi -> eval_builtin_sarg lo vlo -> + eval_builtin_sarg (BA_splitlong hi lo) (Val.longofwords vhi vlo) | seval_BA_addptr: forall a1 a2 v1 v2, - seval_builtin_arg a1 v1 -> seval_builtin_arg a2 v2 -> - seval_builtin_arg (BA_addptr a1 a2) + eval_builtin_sarg a1 v1 -> eval_builtin_sarg a2 v2 -> + eval_builtin_sarg (BA_addptr a1 a2) (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2) . -Definition seval_builtin_args (al: list (builtin_arg sval)) (vl: list val) : Prop := - list_forall2 seval_builtin_arg al vl. +Definition eval_builtin_sargs (al: list (builtin_arg sval)) (vl: list val) : Prop := + list_forall2 eval_builtin_sarg al vl. -Lemma seval_builtin_arg_determ: - forall a v, seval_builtin_arg a v -> forall v', seval_builtin_arg a v' -> v' = v. +Lemma eval_builtin_sarg_determ: + forall a v, eval_builtin_sarg a v -> forall v', eval_builtin_sarg a v' -> v' = v. Proof. induction 1; intros v' EV; inv EV; try congruence. f_equal; eauto. - apply IHseval_builtin_arg1 in H3. apply IHseval_builtin_arg2 in H5. subst; auto. + apply IHeval_builtin_sarg1 in H3. apply IHeval_builtin_sarg2 in H5. subst; auto. Qed. -Lemma eval_builtin_args_determ: - forall al vl, seval_builtin_args al vl -> forall vl', seval_builtin_args al vl' -> vl' = vl. +Lemma eval_builtin_sargs_determ: + forall al vl, eval_builtin_sargs al vl -> forall vl', eval_builtin_sargs al vl' -> vl' = vl. Proof. - induction 1; intros v' EV; inv EV; f_equal; eauto using seval_builtin_arg_determ. + induction 1; intros v' EV; inv EV; f_equal; eauto using eval_builtin_sarg_determ. Qed. -End SEVAL_BUILTIN_ARG. +End EVAL_BUILTIN_SARG. (* NB: generic function that could be put into [AST] file *) Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B := @@ -195,10 +223,10 @@ Fixpoint builtin_arg_map {A B} (f: A -> B) (arg: builtin_arg A) : builtin_arg B | BA_addptr ba1 ba2 => BA_addptr (builtin_arg_map f ba1) (builtin_arg_map f ba2) end. -Lemma seval_builtin_arg_correct ctx rs m sreg: forall arg varg, +Lemma eval_builtin_sarg_correct ctx rs m sreg: forall arg varg, (forall r, eval_sval ctx (sreg r) = Some rs # r) -> eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg -> - seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg. + eval_builtin_sarg ctx m (builtin_arg_map sreg arg) varg. Proof. induction arg. all: try (intros varg SEVAL BARG; inv BARG; constructor; congruence). @@ -208,20 +236,20 @@ Proof. eapply IHarg1; eauto. eapply IHarg2; eauto. Qed. -Lemma seval_builtin_args_correct ctx rs m sreg args vargs: +Lemma eval_builtin_sargs_correct ctx rs m sreg args vargs: (forall r, eval_sval ctx (sreg r) = Some rs # r) -> eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs -> - seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs. + eval_builtin_sargs ctx m (map (builtin_arg_map sreg) args) vargs. Proof. induction 2. - constructor. - simpl. constructor; [| assumption]. - eapply seval_builtin_arg_correct; eauto. + eapply eval_builtin_sarg_correct; eauto. Qed. -Lemma seval_builtin_arg_exact ctx rs m sreg: forall arg varg, +Lemma eval_builtin_sarg_exact ctx rs m sreg: forall arg varg, (forall r, eval_sval ctx (sreg r) = Some rs # r) -> - seval_builtin_arg ctx m (builtin_arg_map sreg arg) varg -> + eval_builtin_sarg ctx m (builtin_arg_map sreg arg) varg -> eval_builtin_arg (cge ctx) (fun r => rs # r) (csp ctx) m arg varg. Proof. induction arg. @@ -233,16 +261,16 @@ Proof. eapply IHarg1; eauto. eapply IHarg2; eauto. Qed. -Lemma seval_builtin_args_exact ctx rs m sreg: forall args vargs, +Lemma eval_builtin_sargs_exact ctx rs m sreg: forall args vargs, (forall r, eval_sval ctx (sreg r) = Some rs # r) -> - seval_builtin_args ctx m (map (builtin_arg_map sreg) args) vargs -> + eval_builtin_sargs ctx m (map (builtin_arg_map sreg) args) vargs -> eval_builtin_args (cge ctx) (fun r => rs # r) (csp ctx) m args vargs. Proof. induction args. - simpl. intros. inv H0. constructor. - intros vargs SEVAL BARG. simpl in BARG. inv BARG. constructor; [| eapply IHargs; eauto]. - eapply seval_builtin_arg_exact; eauto. + eapply eval_builtin_sarg_exact; eauto. Qed. Fixpoint eval_builtin_sval ctx bsv := @@ -285,7 +313,7 @@ Lemma eval_builtin_sval_arg ctx bs: forall ba m v, eval_builtin_sval ctx bs = Some ba -> eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v -> - seval_builtin_arg ctx m bs v. + eval_builtin_sarg ctx m bs v. Proof. induction bs; simpl; try (intros ba m v H; inversion H; subst; clear H; @@ -309,8 +337,8 @@ Proof. econstructor; eauto. Qed. -Lemma seval_builtin_arg_sval ctx m v: forall bs, - seval_builtin_arg ctx m bs v -> +Lemma eval_builtin_sarg_sval ctx m v: forall bs, + eval_builtin_sarg ctx m bs v -> exists ba, eval_builtin_sval ctx bs = Some ba /\ eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m ba v. @@ -321,13 +349,13 @@ Proof. - eexists. constructor. + simpl. rewrite H. reflexivity. + constructor. - - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1). - destruct IHseval_builtin_arg2 as (ba2 & A2 & B2). + - destruct IHeval_builtin_sarg1 as (ba1 & A1 & B1). + destruct IHeval_builtin_sarg2 as (ba2 & A2 & B2). eexists. constructor. + simpl. rewrite A1. rewrite A2. reflexivity. + constructor; assumption. - - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1). - destruct IHseval_builtin_arg2 as (ba2 & A2 & B2). + - destruct IHeval_builtin_sarg1 as (ba1 & A1 & B1). + destruct IHeval_builtin_sarg2 as (ba2 & A2 & B2). eexists. constructor. + simpl. rewrite A1. rewrite A2. reflexivity. + constructor; assumption. @@ -337,9 +365,9 @@ Lemma eval_builtin_sval_args ctx lbs: forall lba m v, eval_list_builtin_sval ctx lbs = Some lba -> list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba v -> - seval_builtin_args ctx m lbs v. + eval_builtin_sargs ctx m lbs v. Proof. - unfold seval_builtin_args; induction lbs; simpl; intros lba m v. + unfold eval_builtin_sargs; induction lbs; simpl; intros lba m v. - intros H; inversion H; subst; clear H. intros H; inversion H. econstructor. - destruct (eval_builtin_sval _ _) eqn:SV; try congruence. @@ -350,8 +378,8 @@ Proof. eapply eval_builtin_sval_arg; eauto. Qed. -Lemma seval_builtin_args_sval ctx m lv: forall lbs, - seval_builtin_args ctx m lbs lv -> +Lemma eval_builtin_sargs_sval ctx m lv: forall lbs, + eval_builtin_sargs ctx m lbs lv -> exists lba, eval_list_builtin_sval ctx lbs = Some lba /\ list_forall2 (eval_builtin_arg (cge ctx) (fun id => id) (csp ctx) m) lba lv. @@ -361,29 +389,29 @@ Proof. + simpl. reflexivity. + constructor. - destruct IHlist_forall2 as (lba & A & B). - apply seval_builtin_arg_sval in H. destruct H as (ba & A' & B'). + apply eval_builtin_sarg_sval in H. destruct H as (ba & A' & B'). eexists. constructor. + simpl. rewrite A'. rewrite A. reflexivity. + constructor; assumption. Qed. Lemma eval_builtin_sval_correct ctx m: forall bs1 v bs2, - seval_builtin_arg ctx m bs1 v -> + eval_builtin_sarg ctx m bs1 v -> (eval_builtin_sval ctx bs1) = (eval_builtin_sval ctx bs2) -> - seval_builtin_arg ctx m bs2 v. + eval_builtin_sarg ctx m bs2 v. Proof. - intros. exploit seval_builtin_arg_sval; eauto. + intros. exploit eval_builtin_sarg_sval; eauto. intros (ba & X1 & X2). eapply eval_builtin_sval_arg; eauto. congruence. Qed. Lemma eval_list_builtin_sval_correct ctx m vargs: forall lbs1, - seval_builtin_args ctx m lbs1 vargs -> + eval_builtin_sargs ctx m lbs1 vargs -> forall lbs2, (eval_list_builtin_sval ctx lbs1) = (eval_list_builtin_sval ctx lbs2) -> - seval_builtin_args ctx m lbs2 vargs. + eval_builtin_sargs ctx m lbs2 vargs. Proof. - intros. exploit seval_builtin_args_sval; eauto. + intros. exploit eval_builtin_sargs_sval; eauto. intros (ba & X1 & X2). eapply eval_builtin_sval_args; eauto. congruence. @@ -391,6 +419,9 @@ Qed. (** * Symbolic (final) value of a block *) +(** TODO: faut-il hash-conser les valeurs symboliques finales. Pas très utile si pas de join interne. +Mais peut être utile dans le cas contraire. *) + Inductive sfval := | Sgoto (pc: exit) | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit) @@ -434,7 +465,7 @@ Inductive sem_sfval ctx stk: sfval -> regset -> mem -> trace -> state -> Prop := sem_sfval ctx stk (Stailcall sig svos lsv) rs m E0 (Callstate stk fd args m') | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs: - seval_builtin_args ctx m sargs vargs -> + eval_builtin_sargs ctx m sargs vargs -> external_call ef (cge ctx) vargs m t vres m' -> sem_sfval ctx stk (Sbuiltin ef sargs res pc) rs m t (State stk (cf ctx) (csp ctx) pc (regmap_setres res vres (tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs)) m') @@ -496,12 +527,12 @@ Proof. rewrite REG; eauto. - erewrite eval_list_sval_inj; simpl; auto. + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto. - eapply seval_builtin_args_correct; eauto. + eapply eval_builtin_sargs_correct; eauto. + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence. Qed. Local Hint Constructors final_step: core. -Local Hint Resolve seval_builtin_args_exact: core. +Local Hint Resolve eval_builtin_sargs_exact: core. Lemma sexec_final_sfv_exact ctx stk i sis t rs m s: sem_sistate ctx sis rs m -> @@ -530,7 +561,7 @@ Qed. (** * symbolic execution of basic instructions *) -Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}. +Definition sis_init : sistate := {| si_pre:= fun _ => True; si_sreg:= fun r => fSinput r; si_smem:= fSinit |}. Lemma sis_init_correct ctx: sem_sistate ctx sis_init (crs0 ctx) (cm0 ctx). @@ -575,7 +606,7 @@ 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. + set_sreg dst (fSop op args) 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) @@ -593,7 +624,7 @@ 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. + set_sreg dst (fSload 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) @@ -612,7 +643,7 @@ 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 + let sm := fSstore 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 @@ -628,11 +659,11 @@ Proof. rewrite REG; auto. Qed. -Lemma seval_condition_eq ctx cond args sis rs m +Lemma eval_scondition_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)) = eval_condition cond rs ## args m. + :eval_scondition ctx cond (list_sval_inj (map (si_sreg sis) args)) = eval_condition cond rs ## args m. Proof. - destruct SIS as (PRE&MEM®); unfold seval_condition; simpl. + destruct SIS as (PRE&MEM®); unfold eval_scondition; simpl. erewrite eval_list_sval_inj; simpl; auto. eapply cond_valid_pointer_eq; eauto. Qed. @@ -640,7 +671,7 @@ Qed. (** * Compute sistate associated to final values *) Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval := match inputs with - | nil => fun r => Sundef + | nil => fun r => fSundef | r1::l => fun r => if Pos.eq_dec r1 r then sreg r1 else transfer_sreg l sreg r end. @@ -723,7 +754,7 @@ Fixpoint get_soutcome ctx (st:sstate): option soutcome := match st with | Sfinal sis sfv => Some (sout sis sfv) | Scond cond args ifso ifnot => - SOME b <- seval_condition ctx cond args IN + SOME b <- eval_scondition ctx cond args IN get_soutcome ctx (if b then ifso else ifnot) | Sabort => None end. @@ -735,7 +766,7 @@ Inductive sem_sstate ctx stk t s: sstate -> Prop := (SFV: sem_sfval ctx stk sfv rs m t s) : sem_sstate ctx stk t s (Sfinal sis sfv) | sem_Scond b cond args ifso ifnot - (SEVAL: seval_condition ctx cond args = Some b) + (SEVAL: eval_scondition ctx cond args = Some b) (SELECT: sem_sstate ctx stk t s (if b then ifso else ifnot)) : sem_sstate ctx stk t s (Scond cond args ifso ifnot) (* NB: Sabort: fails to produce a transition *) @@ -768,14 +799,10 @@ Proof. Qed. -(** * 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) +(** * Model of Symbolic Execution with Continuation Passing Style -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é). +Parameter [k] is the continuation, i.e. the [sstate] construction that will be applied in each execution branch. +Its input parameter is the symbolic internal state of the branch. *) @@ -821,7 +848,7 @@ Proof. (* condition *) all: intros; eapply sem_Scond; eauto; [ - erewrite seval_condition_eq; eauto | + erewrite eval_scondition_eq; eauto | replace (if b then sexec_rec (cf ctx) ifso sis k else sexec_rec (cf ctx) ifnot sis k) with (sexec_rec (cf ctx) (if b then ifso else ifnot) sis k); try autodestruct; eauto ]. Qed. @@ -1044,7 +1071,7 @@ Proof. exploit IHib2; eauto. - (* Bcond *) inv SEXEC. - erewrite seval_condition_eq in SEVAL; eauto. + erewrite eval_scondition_eq in SEVAL; eauto. rewrite SEVAL. destruct b. + exploit IHib1; eauto. @@ -1139,7 +1166,6 @@ Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Pr Definition sistate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (sis1 sis2:sistate): Prop := forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sem_sistate (bctx2 ctx) sis2 rs m. - Record si_ok ctx (sis: sistate): Prop := { OK_PRE: (sis.(si_pre) ctx); OK_SMEM: eval_smem ctx sis.(si_smem) <> None; @@ -1154,7 +1180,6 @@ Proof. intuition congruence. Qed. - Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): Prop := forall sis1 sfv1, get_soutcome (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> si_ok (bctx1 ctx) sis1 -> exists sis2 sfv2, get_soutcome (bctx2 ctx) st2 = Some (sout sis2 sfv2) @@ -1255,23 +1280,13 @@ Proof. reflexivity. Qed. -Lemma seval_condition_preserved cond lsv: - seval_condition (bctx1 ctx) cond lsv = seval_condition (bctx2 ctx) cond lsv. +Lemma eval_scondition_preserved cond lsv: + eval_scondition (bctx1 ctx) cond lsv = eval_scondition (bctx2 ctx) cond lsv. Proof. - unfold seval_condition. + unfold eval_scondition. rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto. Qed. -(* TODO: useless ? -Lemma get_soutcome_preserved sis: - get_soutcome (bctx1 ctx) sis = get_soutcome (bctx2 ctx) sis. -Proof. - induction sis; simpl; eauto. - erewrite seval_condition_preserved. - repeat (autodestruct; auto). -Qed. -*) - (* additional preservation properties under this additional hypothesis *) Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx). @@ -1288,9 +1303,9 @@ Proof. reflexivity. Qed. -Lemma seval_builtin_arg_preserved m: forall bs varg, - seval_builtin_arg (bctx1 ctx) m bs varg -> - seval_builtin_arg (bctx2 ctx) m bs varg. +Lemma eval_builtin_sarg_preserved m: forall bs varg, + eval_builtin_sarg (bctx1 ctx) m bs varg -> + eval_builtin_sarg (bctx2 ctx) m bs varg. Proof. induction 1; simpl. all: try (constructor; auto). @@ -1299,12 +1314,12 @@ Proof. - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal. Qed. -Lemma seval_builtin_args_preserved m lbs vargs: - seval_builtin_args (bctx1 ctx) m lbs vargs -> - seval_builtin_args (bctx2 ctx) m lbs vargs. +Lemma eval_builtin_sargs_preserved m lbs vargs: + eval_builtin_sargs (bctx1 ctx) m lbs vargs -> + eval_builtin_sargs (bctx2 ctx) m lbs vargs. Proof. induction 1; constructor; eauto. - eapply seval_builtin_arg_preserved; auto. + eapply eval_builtin_sarg_preserved; auto. Qed. End SymbValPreserved. |