diff options
| -rw-r--r-- | backend/RTLgen.v | 72 | ||||
| -rw-r--r-- | backend/RTLgenproof.v | 103 | ||||
| -rw-r--r-- | backend/RTLgenspec.v | 215 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 6 | ||||
| -rw-r--r-- | common/Events.v | 34 | ||||
| -rw-r--r-- | common/Values.v | 6 |
6 files changed, 142 insertions, 294 deletions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 8b11022b..b1c36513 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -457,52 +457,35 @@ with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) (** Translation of arguments to annotations. *) -Fixpoint convert_annot_arg (map: mapping) (a: annot_arg expr) : mon (annot_arg reg) := +Definition exprlist_of_expr_list (l: list expr) : exprlist := + List.fold_right Econs Enil l. + +Fixpoint convert_annot_arg {A: Type} (a: annot_arg expr) (rl: list A) : annot_arg A * list A := match a with - | AA_base a => do rd <- alloc_reg map a; ret (AA_base rd) - | AA_int n => ret (AA_int n) - | AA_long n => ret (AA_long n) - | AA_float n => ret (AA_float n) - | AA_single n => ret (AA_single n) - | AA_loadstack chunk ofs => ret (AA_loadstack chunk ofs) - | AA_addrstack ofs => ret (AA_addrstack ofs) - | AA_loadglobal chunk id ofs => ret (AA_loadglobal chunk id ofs) - | AA_addrglobal id ofs => ret (AA_addrglobal id ofs) + | AA_base a => + match rl with + | r :: rs => (AA_base r, rs) + | nil => (AA_int Int.zero, nil) (**r never happens *) + end + | AA_int n => (AA_int n, rl) + | AA_long n => (AA_long n, rl) + | AA_float n => (AA_float n, rl) + | AA_single n => (AA_single n, rl) + | AA_loadstack chunk ofs => (AA_loadstack chunk ofs, rl) + | AA_addrstack ofs => (AA_addrstack ofs, rl) + | AA_loadglobal chunk id ofs => (AA_loadglobal chunk id ofs, rl) + | AA_addrglobal id ofs => (AA_addrglobal id ofs, rl) | AA_longofwords hi lo => - do hi' <- convert_annot_arg map hi; - do lo' <- convert_annot_arg map lo; - ret (AA_longofwords hi' lo') + let (hi', rl1) := convert_annot_arg hi rl in + let (lo', rl2) := convert_annot_arg lo rl1 in + (AA_longofwords hi' lo', rl2) end. -Fixpoint convert_annot_args (map: mapping) (al: list (annot_arg expr)) : mon (list (annot_arg reg)) := +Fixpoint convert_annot_args {A: Type} (al: list (annot_arg expr)) (rl: list A) : list (annot_arg A) := match al with - | nil => ret nil + | nil => nil | a1 :: al => - do a1' <- convert_annot_arg map a1; - do al' <- convert_annot_args map al; - ret (a1' :: al') - end. - -Fixpoint transl_annot_arg - (map: mapping) (a: annot_arg expr) (d: annot_arg reg) (nd: node) - : mon node := - match a, d with - | AA_base a, AA_base r => transl_expr map a r nd - | AA_longofwords hi lo, AA_longofwords hi' lo' => - do no <- transl_annot_arg map lo lo' nd; - transl_annot_arg map hi hi' no - | _, _ => ret nd - end. - -Fixpoint transl_annot_args - (map: mapping) (al: list (annot_arg expr)) (dl: list (annot_arg reg)) (nd: node) - : mon node := - match al, dl with - | a1 :: al, d1 :: dl => - do no <- transl_annot_args map al dl nd; - transl_annot_arg map a1 d1 no - | _, _ => - ret nd + let (a1', rl1) := convert_annot_arg a1 rl in a1' :: convert_annot_args al rl1 end. (** Auxiliary for translating exit expressions. *) @@ -608,10 +591,11 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do r <- alloc_optreg map optid; do n1 <- add_instr (Ibuiltin ef rargs r nd); transl_exprlist map al rargs n1 - | Sannot ef al => - do dl <- convert_annot_args map al; - do n1 <- add_instr (Iannot ef dl nd); - transl_annot_args map al dl n1 + | Sannot ef args => + let al := exprlist_of_expr_list (params_of_annot_args args) in + do rargs <- alloc_regs map al; + do n1 <- add_instr (Iannot ef (convert_annot_args args rargs) nd); + transl_exprlist map al rargs n1 | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index db55c8e8..02460f67 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -974,6 +974,94 @@ Qed. (** Annotation arguments. *) +Lemma eval_exprlist_append: + forall le al1 vl1 al2 vl2, + eval_exprlist ge sp e m le (exprlist_of_expr_list al1) vl1 -> + eval_exprlist ge sp e m le (exprlist_of_expr_list al2) vl2 -> + eval_exprlist ge sp e m le (exprlist_of_expr_list (al1 ++ al2)) (vl1 ++ vl2). +Proof. + induction al1; simpl; intros vl1 al2 vl2 E1 E2; inv E1. +- auto. +- simpl. constructor; eauto. +Qed. + +Lemma invert_eval_annot_arg: + forall a v, + eval_annot_arg ge sp e m a v -> + exists vl, + eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_annot_arg a)) vl + /\ Events.eval_annot_arg ge (fun v => v) sp m (fst (convert_annot_arg a vl)) v + /\ (forall vl', convert_annot_arg a (vl ++ vl') = (fst (convert_annot_arg a vl), vl')). +Proof. + induction 1; simpl; econstructor; intuition eauto with evalexpr aarg. + constructor. + constructor. + repeat constructor. +Qed. + +Lemma invert_eval_annot_args: + forall al vl, + list_forall2 (eval_annot_arg ge sp e m) al vl -> + exists vl', + eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_annot_args al)) vl' + /\ Events.eval_annot_args ge (fun v => v) sp m (convert_annot_args al vl') vl. +Proof. + induction 1; simpl. +- exists (@nil val); split; constructor. +- exploit invert_eval_annot_arg; eauto. intros (vl1 & A & B & C). + destruct IHlist_forall2 as (vl2 & D & E). + exists (vl1 ++ vl2); split. + apply eval_exprlist_append; auto. + rewrite C; simpl. constructor; auto. +Qed. + +Lemma transl_eval_annot_arg: + forall rs a vl rl v, + Val.lessdef_list vl rs##rl -> + Events.eval_annot_arg ge (fun v => v) sp m (fst (convert_annot_arg a vl)) v -> + exists v', + Events.eval_annot_arg ge (fun r => rs#r) sp m (fst (convert_annot_arg a rl)) v' + /\ Val.lessdef v v' + /\ Val.lessdef_list (snd (convert_annot_arg a vl)) rs##(snd (convert_annot_arg a rl)). +Proof. + induction a; simpl; intros until v; intros LD EV; + try (now (inv EV; econstructor; eauto with aarg)). +- destruct rl; simpl in LD; inv LD; inv EV; simpl. + econstructor; eauto with aarg. + exists (rs#p); intuition auto. constructor. +- destruct (convert_annot_arg a1 vl) as [a1' vl1] eqn:CV1; simpl in *. + destruct (convert_annot_arg a2 vl1) as [a2' vl2] eqn:CV2; simpl in *. + destruct (convert_annot_arg a1 rl) as [a1'' rl1] eqn:CV3; simpl in *. + destruct (convert_annot_arg a2 rl1) as [a2'' rl2] eqn:CV4; simpl in *. + inv EV. + exploit IHa1; eauto. rewrite CV1; simpl; eauto. + rewrite CV1, CV3; simpl. intros (v1' & A1 & B1 & C1). + exploit IHa2. eexact C1. rewrite CV2; simpl; eauto. + rewrite CV2, CV4; simpl. intros (v2' & A2 & B2 & C2). + exists (Val.longofwords v1' v2'); split. constructor; auto. + split; auto. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma transl_eval_annot_args: + forall rs al vl1 rl vl, + Val.lessdef_list vl1 rs##rl -> + Events.eval_annot_args ge (fun v => v) sp m (convert_annot_args al vl1) vl -> + exists vl', + Events.eval_annot_args ge (fun r => rs#r) sp m (convert_annot_args al rl) vl' + /\ Val.lessdef_list vl vl'. +Proof. + induction al; simpl; intros until vl; intros LD EV. +- inv EV. exists (@nil val); split; constructor. +- destruct (convert_annot_arg a vl1) as [a1' vl2] eqn:CV1; simpl in *. + inv EV. + exploit transl_eval_annot_arg. eauto. instantiate (2 := a). rewrite CV1; simpl; eauto. + rewrite CV1; simpl. intros (v1' & A1 & B1 & C1). + exploit IHal. eexact C1. eauto. intros (vl' & A2 & B2). + destruct (convert_annot_arg a rl) as [a1'' rl2]; simpl in *. + exists (v1' :: vl'); split; constructor; auto. +Qed. + + (* Definition transl_annot_arg_prop (a: annot_arg expr) (v: val): Prop := forall tm cs f map pr ns nd a' rs @@ -1024,7 +1112,7 @@ Proof. rewrite (D2 r) by auto with coqlib. apply Val.longofwords_lessdef; auto. transitivity rs1#r1; auto with coqlib. Qed. -*) + Definition transl_annot_args_prop (l: list (annot_arg expr)) (vl: list val): Prop := forall tm cs f map pr ns nd l' rs @@ -1110,6 +1198,7 @@ Proof. rewrite E3; auto. transitivity rs1#r1; auto. transitivity rs2#r1; auto. Qed. +*) End CORRECTNESS_EXPR. @@ -1444,13 +1533,19 @@ Proof. eapply match_env_update_dest; eauto. (* annot *) - inv TS. - exploit transl_annot_args_correct; eauto. - intros [rs' [tm' [vl' [E [F [G [J [K L]]]]]]]]. + inv TS. exploit invert_eval_annot_args; eauto. intros (vparams & P & Q). + exploit transl_exprlist_correct; eauto. + intros [rs' [tm' [E [F [G [J K]]]]]]. + exploit transl_eval_annot_args; eauto. + intros (vargs' & U & V). + exploit (@eval_annot_args_lessdef _ ge (fun r => rs'#r) (fun r => rs'#r)); eauto. + intros (vargs'' & X & Y). + assert (Z: Val.lessdef_list vl vargs'') by (eapply Val.lessdef_list_trans; eauto). edestruct external_call_mem_extends as [tv [tm'' [A [B [C D]]]]]; eauto. econstructor; split. left. eapply plus_right. eexact E. eapply exec_Iannot; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved. eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. traceEq. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index e78c6c59..1ca9faa0 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -807,49 +807,6 @@ Inductive tr_exitexpr (c: code): tr_exitexpr c (add_letvar map r) b n1 nexits -> tr_exitexpr c map (XElet a b) ns nexits. -(** Translation of arguments to annotations. - [tr_annot_args c map pr al ns nd al'] holds if the graph [c], - starting at node [ns], contains instructions that evaluate the - expressions contained in the built-in argument list [al], - then terminate on node [nd]. When [nd] is reached, the registers - contained in [al'] hold the values of the corresponding expressions - in [al]. Registers in [pr] are not modified. *) - -Inductive tr_annot_arg (c: code): - mapping -> list reg -> annot_arg expr -> node -> node -> annot_arg reg -> Prop := - | tr_AA_base: forall map pr a ns nd r, - tr_expr c map pr a ns nd r None -> - tr_annot_arg c map pr (AA_base a) ns nd (AA_base r) - | tr_AA_int: forall map pr i n, - tr_annot_arg c map pr (AA_int i) n n (AA_int i) - | tr_AA_long: forall map pr i n, - tr_annot_arg c map pr (AA_long i) n n (AA_long i) - | tr_AA_float: forall map pr i n, - tr_annot_arg c map pr (AA_float i) n n (AA_float i) - | tr_AA_single: forall map pr i n, - tr_annot_arg c map pr (AA_single i) n n (AA_single i) - | tr_AA_loadstack: forall map pr chunk ofs n, - tr_annot_arg c map pr (AA_loadstack chunk ofs) n n (AA_loadstack chunk ofs) - | tr_AA_addrstack: forall map pr ofs n, - tr_annot_arg c map pr (AA_addrstack ofs) n n (AA_addrstack ofs) - | tr_AA_loadglobal: forall map pr chunk id ofs n, - tr_annot_arg c map pr (AA_loadglobal chunk id ofs) n n (AA_loadglobal chunk id ofs) - | tr_AA_addrglobal: forall map pr id ofs n, - tr_annot_arg c map pr (AA_addrglobal id ofs) n n (AA_addrglobal id ofs) - | tr_AA_longofwords: forall map pr hi lo ns nd n1 hi' lo', - tr_annot_arg c map pr hi ns n1 hi' -> - tr_annot_arg c map (params_of_annot_arg hi' ++ pr) lo n1 nd lo' -> - tr_annot_arg c map pr (AA_longofwords hi lo) ns nd (AA_longofwords hi' lo'). - -Inductive tr_annot_args (c: code): - mapping -> list reg -> list (annot_arg expr) -> node -> node -> list (annot_arg reg) -> Prop := - | tr_AA_nil: forall map pr n, - tr_annot_args c map pr nil n n nil - | tr_AA_cons: forall map pr a ns n1 a' al nd al', - tr_annot_arg c map pr a ns n1 a' -> - tr_annot_args c map (params_of_annot_arg a' ++ pr) al n1 nd al' -> - tr_annot_args c map pr (a :: al) ns nd (a' :: al'). - (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c], starting at node [ns], contains instructions that perform the Cminor statement [stmt]. These instructions branch to node [ncont] if @@ -897,9 +854,9 @@ Inductive tr_stmt (c: code) (map: mapping): c!n1 = Some (Ibuiltin ef rargs rd nd) -> reg_map_ok map rd optid -> tr_stmt c map (Sbuiltin optid ef al) ns nd nexits ngoto nret rret - | tr_Sannot: forall ef al ns nd nexits ngoto nret rret n1 al', - tr_annot_args c map nil al ns n1 al' -> - c!n1 = Some (Iannot ef al' nd) -> + | tr_Sannot: forall ef al ns nd nexits ngoto nret rret n1 rargs, + tr_exprlist c map nil (exprlist_of_expr_list (params_of_annot_args al)) ns n1 rargs -> + c!n1 = Some (Iannot ef (convert_annot_args al rargs) nd) -> tr_stmt c map (Sannot ef al) ns nd nexits ngoto nret rret | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n, tr_stmt c map s2 n nd nexits ngoto nret rret -> @@ -1190,28 +1147,6 @@ Proof. induction 1; econstructor; eauto with rtlg. Qed. -Lemma tr_annot_arg_incr: - forall s1 s2, state_incr s1 s2 -> - forall map pr a ns nd a', - tr_annot_arg s1.(st_code) map pr a ns nd a' -> - tr_annot_arg s2.(st_code) map pr a ns nd a'. -Proof. - intros s1 s2 EXT. - generalize tr_expr_incr; intros I1. - induction 1; econstructor; eauto with rtlg. -Qed. - -Lemma tr_annot_args_incr: - forall s1 s2, state_incr s1 s2 -> - forall map pr al ns nd al', - tr_annot_args s1.(st_code) map pr al ns nd al' -> - tr_annot_args s2.(st_code) map pr al ns nd al'. -Proof. - intros s1 s2 EXT. - generalize tr_annot_arg_incr; intros I1. - induction 1; econstructor; eauto with rtlg. -Qed. - Lemma tr_stmt_incr: forall s1 s2, state_incr s1 s2 -> forall map s ns nd nexits ngoto nret rret, @@ -1219,7 +1154,7 @@ Lemma tr_stmt_incr: tr_stmt s2.(st_code) map s ns nd nexits ngoto nret rret. Proof. intros s1 s2 EXT. - generalize tr_expr_incr tr_condition_incr tr_exprlist_incr tr_exitexpr_incr tr_annot_args_incr; intros I1 I2 I3 I4 I5. + generalize tr_expr_incr tr_condition_incr tr_exprlist_incr tr_exitexpr_incr; intros I1 I2 I3 I4. pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). induction 1; econstructor; eauto. Qed. @@ -1273,142 +1208,6 @@ Proof. apply add_letvar_valid; eauto with rtlg. Qed. -Lemma convert_annot_arg_valid: - forall map a s1 a' s2 i, - convert_annot_arg map a s1 = OK a' s2 i -> - map_valid map s1 -> - regs_valid (params_of_annot_arg a') s2. -Proof. - induction a; simpl; intros; monadInv H; simpl; auto using regs_valid_nil. -- apply regs_valid_cons. eauto with rtlg. apply regs_valid_nil. -- apply regs_valid_app. eauto with rtlg. eapply IHa2; eauto with rtlg. -Qed. - -Lemma convert_annot_args_valid: - forall map l s1 l' s2 i, - convert_annot_args map l s1 = OK l' s2 i -> - map_valid map s1 -> - regs_valid (params_of_annot_args l') s2. -Proof. - induction l; simpl; intros. -- monadInv H. apply regs_valid_nil. -- monadInv H. simpl. apply regs_valid_app. - + apply regs_valid_incr with s; auto. eapply convert_annot_arg_valid; eauto. - + eapply IHl; eauto with rtlg. -Qed. - -Inductive target_annot_arg_ok (map: mapping): list reg -> annot_arg expr -> annot_arg reg -> Prop := - | taa_AA_base: forall pr a r, - target_reg_ok map pr a r -> - target_annot_arg_ok map pr (AA_base a) (AA_base r) - | taa_AA_int: forall pr i, - target_annot_arg_ok map pr (AA_int i) (AA_int i) - | taa_AA_long: forall pr i, - target_annot_arg_ok map pr (AA_long i) (AA_long i) - | taa_AA_float: forall pr i, - target_annot_arg_ok map pr (AA_float i) (AA_float i) - | taa_AA_single: forall pr i, - target_annot_arg_ok map pr (AA_single i) (AA_single i) - | taa_AA_loadstack: forall pr chunk ofs, - target_annot_arg_ok map pr (AA_loadstack chunk ofs) (AA_loadstack chunk ofs) - | taa_AA_addrstack: forall pr ofs, - target_annot_arg_ok map pr (AA_addrstack ofs) (AA_addrstack ofs) - | taa_AA_loadglobal: forall pr chunk id ofs, - target_annot_arg_ok map pr (AA_loadglobal chunk id ofs) (AA_loadglobal chunk id ofs) - | taa_AA_addrglobal: forall pr id ofs, - target_annot_arg_ok map pr (AA_addrglobal id ofs) (AA_addrglobal id ofs) - | taa_AA_longofwords: forall pr hi lo hi' lo', - target_annot_arg_ok map pr hi hi' -> - target_annot_arg_ok map (params_of_annot_arg hi' ++ pr) lo lo' -> - target_annot_arg_ok map pr (AA_longofwords hi lo) (AA_longofwords hi' lo'). - -Lemma convert_annot_arg_ok: - forall map a pr s1 a' s2 i, - map_valid map s1 -> - regs_valid pr s1 -> - convert_annot_arg map a s1 = OK a' s2 i -> - target_annot_arg_ok map pr a a'. -Proof. - induction a; simpl; intros until i; intros MAP PR CVT; monadInv CVT; try (now constructor). -- constructor. eauto with rtlg. -- constructor. - eapply IHa1 with (s1 := s1); eauto. - eapply IHa2 with (s1 := s); eauto with rtlg. - apply regs_valid_app; eauto using convert_annot_arg_valid with rtlg. -Qed. - -Inductive target_annot_args_ok (map: mapping): list reg -> list (annot_arg expr) -> list (annot_arg reg) -> Prop := - | taa_AA_nil: forall pr, - target_annot_args_ok map pr nil nil - | taa_AA_cons: forall pr a a' l l', - target_annot_arg_ok map pr a a' -> - target_annot_args_ok map (params_of_annot_arg a' ++ pr) l l' -> - target_annot_args_ok map pr (a :: l) (a' :: l'). - -Lemma convert_annot_args_ok: - forall map l pr s1 l' s2 i, - map_valid map s1 -> - regs_valid pr s1 -> - convert_annot_args map l s1 = OK l' s2 i -> - target_annot_args_ok map pr l l'. -Proof. - induction l; simpl; intros until i; intros MAP PR CVT; monadInv CVT. -- constructor. -- constructor. - eapply convert_annot_arg_ok with (s1 := s1); eauto. - eapply IHl with (s1 := s); eauto with rtlg. - apply regs_valid_app; eauto using convert_annot_arg_valid with rtlg. -Qed. - -Lemma transl_annot_arg_charact: - forall map a a' nd s ns s' i pr - (TR: transl_annot_arg map a a' nd s = OK ns s' i) - (WF: map_valid map s) - (OK: target_annot_arg_ok map pr a a') - (VALID: regs_valid pr s) - (VALID2: regs_valid (params_of_annot_arg a') s), - tr_annot_arg s'.(st_code) map pr a ns nd a'. -Proof. - induction a; intros; inv OK; simpl in TR; try (monadInv TR); simpl in VALID2. -- assert (reg_valid r s) by auto with coqlib. - constructor. eapply transl_expr_charact; eauto with rtlg. -- constructor. -- constructor. -- constructor. -- constructor. -- constructor. -- constructor. -- constructor. -- constructor. -- econstructor. - eapply IHa1; eauto with rtlg. - red; intros. apply reg_valid_incr with s; auto using in_or_app. - apply tr_annot_arg_incr with s0; auto. - eapply IHa2; eauto with rtlg. - apply regs_valid_app; auto. red; intros; auto using in_or_app. - red; intros; auto using in_or_app. -Qed. - -Lemma transl_annot_args_charact: - forall map al al' nd s ns s' i pr - (TR: transl_annot_args map al al' nd s = OK ns s' i) - (WF: map_valid map s) - (OK: target_annot_args_ok map pr al al') - (VALID: regs_valid pr s) - (VALID2: regs_valid (params_of_annot_args al') s), - tr_annot_args s'.(st_code) map pr al ns nd al'. -Proof. - induction al as [|a al]; intros; inv OK; monadInv TR; simpl in VALID2. -- constructor. -- econstructor. - eapply transl_annot_arg_charact; eauto with rtlg. - red; intros. apply reg_valid_incr with s; auto using in_or_app. - apply tr_annot_args_incr with s0; auto. - eapply IHal; eauto with rtlg. - apply regs_valid_app; auto. red; intros; auto using in_or_app. - red; intros; auto using in_or_app. -Qed. - Lemma transl_stmt_charact: forall map stmt nd nexits ngoto nret rret s ns s' INCR (TR: transl_stmt map stmt nd nexits ngoto nret rret s = OK ns s' INCR) @@ -1463,10 +1262,8 @@ Proof. eapply transl_exprlist_charact; eauto 3 with rtlg. eapply alloc_optreg_map_ok with (s1 := s0); eauto with rtlg. (* Sannot *) - econstructor; eauto 4 with rtlg. - eapply transl_annot_args_charact; eauto 3 with rtlg. - eapply convert_annot_args_ok; eauto 3 with rtlg. - apply regs_valid_incr with s0; auto. eapply convert_annot_args_valid; eauto. + econstructor; eauto 4 with rtlg. + eapply transl_exprlist_charact; eauto 3 with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index ed67286f..66427b76 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -513,10 +513,10 @@ Definition do_ef_memcpy (sz al: Z) | _ => None end. -Definition do_ef_annot (text: ident) (targs: list annot_arg) +Definition do_ef_annot (text: ident) (targs: list typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - do args <- list_eventval_of_val vargs (annot_args_typ targs); - Some(w, Event_annot text (annot_eventvals targs args) :: E0, Vundef, m). + do args <- list_eventval_of_val vargs targs; + Some(w, Event_annot text args :: E0, Vundef, m). Definition do_ef_annot_val (text: ident) (targ: typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := diff --git a/common/Events.v b/common/Events.v index ad59ece9..15bf4e12 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1915,37 +1915,3 @@ Qed. End EVAL_ANNOT_ARG_LESSDEF. -(** Extensionality *) - -Section EVAL_ANNOT_ARG_EXTEN. - -Variable A: Type. -Variable ge: Senv.t. -Variables e1 e2: A -> val. -Variable sp: val. -Variable m: mem. - -Lemma eval_annot_arg_exten: - forall a v, eval_annot_arg ge e1 sp m a v -> - (forall x, In x (params_of_annot_arg a) -> e2 x = e1 x) -> - eval_annot_arg ge e2 sp m a v. -Proof. - induction 1; simpl; intros EXT; try (now constructor). -- rewrite <- EXT by auto. constructor. -- constructor; eauto using in_or_app. -Qed. - -Lemma eval_annot_args_exten: - forall a v, eval_annot_args ge e1 sp m a v -> - (forall x, In x (params_of_annot_args a) -> e2 x = e1 x) -> - eval_annot_args ge e2 sp m a v. -Proof. - induction 1; simpl; intros EXT; constructor. - eapply eval_annot_arg_exten; eauto using in_or_app. - eapply IHlist_forall2; eauto using in_or_app. -Qed. - -End EVAL_ANNOT_ARG_EXTEN. - - - diff --git a/common/Values.v b/common/Values.v index a12fb636..984da4ed 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1381,6 +1381,12 @@ Proof. left; congruence. tauto. tauto. Qed. +Lemma lessdef_list_trans: + forall vl1 vl2, lessdef_list vl1 vl2 -> forall vl3, lessdef_list vl2 vl3 -> lessdef_list vl1 vl3. +Proof. + induction 1; intros vl3 LD; inv LD; constructor; eauto using lessdef_trans. +Qed. + (** Compatibility of operations with the [lessdef] relation. *) Lemma load_result_lessdef: |