From 9c01536d6bb0696091228cb4a4d52cdcd0c55416 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 11 Jun 2021 16:25:33 +0200 Subject: add hid in BTL_SEtheory: this avoids duplication of types (and should not be harmful) --- scheduling/BTL_SEtheory.v | 269 ++++++++++++++++++++++++---------------------- 1 file changed, 142 insertions(+), 127 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') 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. -- cgit