diff options
88 files changed, 1973 insertions, 682 deletions
@@ -1,7 +1,7 @@ - The CompCert C verified compiler - -OVERVIEW: +# CompCert +The verified C compiler. +## Overview The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM and x86 processors. @@ -17,18 +17,13 @@ purposes. For more information on CompCert (supported platforms, supported C features, installation instructions, using the compiler, etc), please -refer to the user's manual: http://compcert.inria.fr/man/ - - -COPYRIGHT: +refer to the [user's manual](http://compcert.inria.fr/man/). +## Copyright The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut National de Recherche en Informatique et en Automatique (INRIA). It is distributed under the -conditions stated in file LICENSE. - - -CONTACT: - -The authors can be contacted by e-mail at compcert@yquem.inria.fr +conditions stated in file `LICENSE`. +## Contact +The authors can be contacted by e-mail at compcert@yquem.inria.fr. @@ -204,11 +204,7 @@ Inductive instruction : Type := | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function *) - | Pannot: external_function -> list annot_param -> instruction (**r annotation statement *) - -with annot_param : Type := - | APreg: preg -> annot_param - | APstack: memory_chunk -> Z -> annot_param. + | Pannot: external_function -> list (annot_arg preg) -> instruction. (**r annotation statement *) (** The pseudo-instructions are the following: @@ -766,20 +762,6 @@ Definition extcall_arguments Definition loc_external_result (sg: signature) : list preg := map preg_of (loc_result sg). -(** Extract the values of the arguments of an annotation. *) - -Inductive annot_arg (rs: regset) (m: mem): annot_param -> val -> Prop := - | annot_arg_reg: forall r, - annot_arg rs m (APreg r) (rs r) - | annot_arg_stack: forall chunk ofs stk base v, - rs (IR IR13) = Vptr stk base -> - Mem.load chunk m stk (Int.unsigned base + ofs) = Some v -> - annot_arg rs m (APstack chunk ofs) v. - -Definition annot_arguments - (rs: regset) (m: mem) (params: list annot_param) (args: list val) : Prop := - list_forall2 (annot_arg rs m) params args. - (** Execution of the instruction at [rs#PC]. *) Inductive state: Type := @@ -808,8 +790,8 @@ Inductive step: state -> trace -> state -> Prop := rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_instr (Int.unsigned ofs) (fn_code f) = Some (Pannot ef args) -> - annot_arguments rs m args vargs -> - external_call' ef ge vargs m t v m' -> + eval_annot_args ge rs (rs SP) m args vargs -> + external_call ef ge vargs m t v m' -> step (State rs m) t (State (nextinstr rs) m') | exec_step_external: forall b ef args res rs m t rs' m', @@ -860,16 +842,6 @@ Proof. intros. red in H0; red in H1. eauto. Qed. -Remark annot_arguments_determ: - forall rs m params args1 args2, - annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2. -Proof. - unfold annot_arguments. intros. revert params args1 H args2 H0. - induction 1; intros. - inv H0; auto. - inv H1. decEq; eauto. inv H; inv H4. auto. congruence. -Qed. - Lemma semantics_determinate: forall p, determinate (semantics p). Proof. Ltac Equalities := @@ -888,8 +860,8 @@ Ltac Equalities := exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. inv H12. - assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. - exploit external_call_determ'. eexact H5. eexact H13. intros [A B]. + assert (vargs0 = vargs) by (eapply eval_annot_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H13. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. exploit external_call_determ'. eexact H3. eexact H8. intros [A B]. @@ -898,7 +870,7 @@ Ltac Equalities := red; intros; inv H; simpl. omega. inv H3; eapply external_call_trace_length; eauto. - inv H4; eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. inv H2; eapply external_call_trace_length; eauto. (* initial states *) inv H; inv H0. f_equal. congruence. diff --git a/arm/Asmgen.v b/arm/Asmgen.v index de4b87fb..5a3a48e1 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -695,14 +695,6 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) Error (msg "Asmgen.transl_store") end. -(** Translation of arguments to annotations *) - -Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param := - match p with - | Mach.APreg r => APreg (preg_of r) - | Mach.APstack chunk ofs => APstack chunk ofs - end. - (** Translation of a Mach instruction. *) Definition transl_instr (f: Mach.function) (i: Mach.instruction) @@ -737,7 +729,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mbuiltin ef args res => OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k) | Mannot ef args => - OK (Pannot ef (map transl_annot_param args) :: k) + OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k) | Mlabel lbl => OK (Plabel lbl :: k) | Mgoto lbl => diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index c687722c..6d9b134f 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -771,13 +771,16 @@ Opaque loadind. inv AT. monadInv H4. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends'; eauto. + exploit annot_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. - eapply external_call_symbols_preserved'; eauto. + erewrite <- sp_val by 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. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 6102d82d..fea99ef5 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -489,3 +489,16 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := | _ => (Aindexed Int.zero, e:::Enil) end. +(** ** Arguments of annotations *) + +Nondetfunction annot_arg (e: expr) := + match e with + | Eop (Ointconst n) Enil => AA_int n + | Eop (Oaddrsymbol id ofs) Enil => AA_addrglobal id ofs + | Eop (Oaddrstack ofs) Enil => AA_addrstack ofs + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => + AA_long (Int64.ofwords h l) + | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l) + | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs + | _ => AA_base e + end. diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index c68d2277..d3c3239a 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -864,4 +864,19 @@ Proof. exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Int.add_zero; auto. Qed. +Theorem eval_annot_arg: + forall a v, + eval_expr ge sp e m nil a v -> + CminorSel.eval_annot_arg ge sp e m (annot_arg a) v. +Proof. + intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval. +- constructor. +- constructor. +- constructor. +- simpl in H5. inv H5. constructor. +- subst v. constructor; auto. +- inv H. InvEval. simpl in H6; inv H6. constructor; auto. +- constructor; auto. +Qed. + End CMCONSTR. diff --git a/backend/Allocation.v b/backend/Allocation.v index 919843b5..37b79a1a 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -22,6 +22,7 @@ Require Import Maps. Require Import Lattice. Require Import AST. Require Import Integers. +Require Import Floats. Require Import Memdata. Require Import Op. Require Import Registers. @@ -95,8 +96,9 @@ Inductive block_shape: Type := | BSbuiltin (ef: external_function) (args: list reg) (res: reg) (mv1: moves) (args': list mreg) (res': list mreg) (mv2: moves) (s: node) - | BSannot (text: ident) (targs: list annot_arg) (args: list reg) (res: reg) - (mv: moves) (args': list loc) (s: node) + | BSannot (ef: external_function) + (args: list (annot_arg reg)) (args': list (annot_arg loc)) + (s: node) | BScond (cond: condition) (args: list reg) (mv: moves) (args': list mreg) (s1 s2: node) | BSjumptable (arg: reg) @@ -276,13 +278,14 @@ Definition pair_instr_block assertion (external_function_eq ef ef'); assertion (check_succ s b3); Some(BSbuiltin ef args res mv1 args' res' mv2 s) - | Lannot ef' args' :: b2 => + | _ => None + end + | Iannot ef args s => + match b with + | Lannot ef' args' :: b1 => assertion (external_function_eq ef ef'); - assertion (check_succ s b2); - match ef with - | EF_annot txt typ => Some(BSannot txt typ args res mv1 args' s) - | _ => None - end + assertion (check_succ s b1); + Some(BSannot ef args args' s) | _ => None end | Icond cond args s1 s2 => @@ -696,6 +699,57 @@ Definition add_equation_ros (ros: reg + ident) (ros': mreg + ident) (e: eqs) : o | _, _ => None end. +(** [add_equations_annot_arg] adds the needed equations for annotation + arguments. *) + +Fixpoint add_equations_annot_arg (env: regenv) (arg: annot_arg reg) (arg': annot_arg loc) (e: eqs) : option eqs := + match arg, arg' with + | AA_base r, AA_base l => + Some (add_equation (Eq Full r l) e) + | AA_base r, AA_longofwords (AA_base lhi) (AA_base llo) => + assertion (typ_eq (env r) Tlong); + Some (add_equation (Eq Low r llo) (add_equation (Eq High r lhi) e)) + | AA_int n, AA_int n' => + assertion (Int.eq_dec n n'); Some e + | AA_long n, AA_long n' => + assertion (Int64.eq_dec n n'); Some e + | AA_float f, AA_float f' => + assertion (Float.eq_dec f f'); Some e + | AA_single f, AA_single f' => + assertion (Float32.eq_dec f f'); Some e + | AA_loadstack chunk ofs, AA_loadstack chunk' ofs' => + assertion (chunk_eq chunk chunk'); + assertion (Int.eq_dec ofs ofs'); + Some e + | AA_addrstack ofs, AA_addrstack ofs' => + assertion (Int.eq_dec ofs ofs'); + Some e + | AA_loadglobal chunk id ofs, AA_loadglobal chunk' id' ofs' => + assertion (chunk_eq chunk chunk'); + assertion (ident_eq id id'); + assertion (Int.eq_dec ofs ofs'); + Some e + | AA_addrglobal id ofs, AA_addrglobal id' ofs' => + assertion (ident_eq id id'); + assertion (Int.eq_dec ofs ofs'); + Some e + | AA_longofwords hi lo, AA_longofwords hi' lo' => + do e1 <- add_equations_annot_arg env hi hi' e; + add_equations_annot_arg env lo lo' e1 + | _, _ => + None + end. + +Fixpoint add_equations_annot_args (env: regenv) + (args: list(annot_arg reg)) (args': list(annot_arg loc)) (e: eqs) : option eqs := + match args, args' with + | nil, nil => Some e + | a1 :: al, a1' :: al' => + do e1 <- add_equations_annot_arg env a1 a1' e; + add_equations_annot_args env al al' e1 + | _, _ => None + end. + (** [can_undef ml] returns true if all machine registers in [ml] are unconstrained and can harmlessly be undefined. *) @@ -926,9 +980,8 @@ Definition transfer_aux (f: RTL.function) (env: regenv) assertion (can_undef (destroyed_by_builtin ef) e2); do e3 <- add_equations_args args (sig_args (ef_sig ef)) args' e2; track_moves env mv1 e3 - | BSannot txt typ args res mv1 args' s => - do e1 <- add_equations_args args (annot_args_typ typ) args' e; - track_moves env mv1 e1 + | BSannot ef args args' s => + add_equations_annot_args env args args' e | BScond cond args mv args' s1 s2 => assertion (can_undef (destroyed_by_cond cond) e); do e1 <- add_equations args args' e; @@ -1099,7 +1152,7 @@ Definition successors_block_shape (bsh: block_shape) : list node := | BScall sg ros args res mv1 ros' mv2 s => s :: nil | BStailcall sg ros args mv1 ros' => nil | BSbuiltin ef args res mv1 args' res' mv2 s => s :: nil - | BSannot txt typ args res mv1 args' s => s :: nil + | BSannot ef args args' s => s :: nil | BScond cond args mv args' s1 s2 => s1 :: s2 :: nil | BSjumptable arg mv arg' tbl => tbl | BSreturn optarg mv => nil diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 2612ebf2..875d4929 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -165,12 +165,10 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr (Ibuiltin ef args res s) (expand_moves mv1 (Lbuiltin ef args' res' :: expand_moves mv2 (Lbranch s :: k))) - | ebs_annot: forall txt typ args res mv args' s k, - wf_moves mv -> - expand_block_shape (BSannot txt typ args res mv args' s) - (Ibuiltin (EF_annot txt typ) args res s) - (expand_moves mv - (Lannot (EF_annot txt typ) args' :: Lbranch s :: k)) + | ebs_annot: forall ef args args' s k, + expand_block_shape (BSannot ef args args' s) + (Iannot ef args s) + (Lannot ef args' :: Lbranch s :: k) | ebs_cond: forall cond args mv args' s1 s2 k, wf_moves mv -> expand_block_shape (BScond cond args mv args' s1 s2) @@ -322,7 +320,8 @@ Proof. (* builtin *) destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. econstructor; eauto. - destruct ef; inv H. econstructor; eauto. +(* annot *) + destruct b; MonadInv. destruct i; MonadInv. UseParsingLemmas. constructor. (* cond *) destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. econstructor; eauto. (* jumptable *) @@ -1348,6 +1347,75 @@ Proof. rewrite Int64.hi_ofwords, Int64.lo_ofwords; auto. Qed. +Lemma add_equations_annot_arg_satisf: + forall env rs ls arg arg' e e', + add_equations_annot_arg env arg arg' e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +Proof. + induction arg; destruct arg'; simpl; intros; MonadInv; eauto. + eapply add_equation_satisf; eauto. + destruct arg'1; MonadInv. destruct arg'2; MonadInv. eauto using add_equation_satisf. +Qed. + +Lemma add_equations_annot_arg_lessdef: + forall env (ge: RTL.genv) sp rs ls m arg v, + eval_annot_arg ge (fun r => rs#r) sp m arg v -> + forall e e' arg', + add_equations_annot_arg env arg arg' e = Some e' -> + satisf rs ls e' -> + wt_regset env rs -> + exists v', eval_annot_arg ge ls sp m arg' v' /\ Val.lessdef v v'. +Proof. + induction 1; simpl; intros e e' arg' AE SAT WT; destruct arg'; MonadInv. +- exploit add_equation_lessdef; eauto. simpl; intros. + exists (ls x0); auto with aarg. +- destruct arg'1; MonadInv. destruct arg'2; MonadInv. + exploit add_equation_lessdef. eauto. simpl; intros LD1. + exploit add_equation_lessdef. eapply add_equation_satisf. eauto. simpl; intros LD2. + exists (Val.longofwords (ls x0) (ls x1)); split; auto with aarg. + rewrite <- (val_longofwords_eq rs#x). apply Val.longofwords_lessdef; auto. + rewrite <- e0; apply WT. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- exploit IHeval_annot_arg1; eauto. eapply add_equations_annot_arg_satisf; eauto. + intros (v1 & A & B). + exploit IHeval_annot_arg2; eauto. intros (v2 & C & D). + exists (Val.longofwords v1 v2); split; auto with aarg. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma add_equations_annot_args_satisf: + forall env rs ls arg arg' e e', + add_equations_annot_args env arg arg' e = Some e' -> + satisf rs ls e' -> satisf rs ls e. +Proof. + induction arg; destruct arg'; simpl; intros; MonadInv; eauto using add_equations_annot_arg_satisf. +Qed. + +Lemma add_equations_annot_args_lessdef: + forall env (ge: RTL.genv) sp rs ls m tm arg vl, + eval_annot_args ge (fun r => rs#r) sp m arg vl -> + forall arg' e e', + add_equations_annot_args env arg arg' e = Some e' -> + satisf rs ls e' -> + wt_regset env rs -> + Mem.extends m tm -> + exists vl', eval_annot_args ge ls sp tm arg' vl' /\ Val.lessdef_list vl vl'. +Proof. + induction 1; simpl; intros; destruct arg'; MonadInv. +- exists (@nil val); split; constructor. +- exploit IHlist_forall2; eauto. intros (vl' & A & B). + exploit add_equations_annot_arg_lessdef; eauto. + eapply add_equations_annot_args_satisf; eauto. intros (v1' & C & D). + exploit (@eval_annot_arg_lessdef _ ge ls ls); eauto. intros (v1'' & E & F). + exists (v1'' :: vl'); split; constructor; auto. eapply Val.lessdef_trans; eauto. +Qed. + (** * Properties of the dataflow analysis *) Lemma analyze_successors: @@ -2035,27 +2103,21 @@ Proof. econstructor; eauto. (* annot *) -- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. - exploit external_call_mem_extends; eauto. eapply add_equations_args_lessdef; eauto. - inv WTI. simpl in H4. rewrite <- H4. apply wt_regset_list; auto. - intros [v' [m'' [F [G [J K]]]]]. - assert (v = Vundef). red in H0; inv H0. auto. +- exploit add_equations_annot_args_lessdef; eauto. + intros (vargs' & A & B). + exploit external_call_mem_extends; eauto. + intros [vres' [m'' [F [G [J K]]]]]. econstructor; split. eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. eapply star_two. econstructor. - eapply external_call_symbols_preserved' with (ge1 := ge). - econstructor; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved with (ge1 := ge); eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - eauto. constructor. eauto. eauto. traceEq. + constructor. eauto. traceEq. exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. - eapply satisf_undef_reg with (r := res). - eapply add_equations_args_satisf; eauto. + eapply add_equations_annot_args_satisf; eauto. intros [enext [U V]]. econstructor; eauto. - change (destroyed_by_builtin (EF_annot txt typ)) with (@nil mreg). - simpl. subst v. assumption. - apply wt_regset_assign; auto. subst v. constructor. (* cond *) - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 3801a4f6..ba7fa3a6 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -358,34 +358,27 @@ Qed. (** Translation of arguments to annotations. *) -Lemma annot_arg_match: - forall ms sp rs m m' p v, - agree ms sp rs -> - Mem.extends m m' -> - Mach.annot_arg ms m sp p v -> - exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'. +Remark annot_arg_match: + forall ge (rs: regset) sp m a v, + eval_annot_arg ge (fun r => rs (preg_of r)) sp m a v -> + eval_annot_arg ge rs sp m (map_annot_arg preg_of a) v. Proof. - intros. inv H1; simpl. -(* reg *) - exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto. -(* stack *) - exploit Mem.load_extends; eauto. intros [v' [A B]]. - exists v'; split; auto. - inv H. econstructor; eauto. + induction 1; simpl; eauto with aarg. Qed. -Lemma annot_arguments_match: - forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> - forall pl vl, - Mach.annot_arguments ms m sp pl vl -> - exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl' +Lemma annot_args_match: + forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> + forall al vl, eval_annot_args ge ms sp m al vl -> + exists vl', eval_annot_args ge rs sp m' (map (map_annot_arg preg_of) al) vl' /\ Val.lessdef_list vl vl'. Proof. - induction 3; intros. - exists (@nil val); split. constructor. constructor. - exploit annot_arg_match; eauto. intros [v1' [A B]]. + induction 3; intros; simpl. + exists (@nil val); split; constructor. + exploit (@eval_annot_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto. + intros; eapply preg_val; eauto. + intros (v1' & A & B). destruct IHlist_forall2 as [vl' [C D]]. - exists (v1' :: vl'); split; constructor; auto. + exists (v1' :: vl'); split; constructor; auto. apply annot_arg_match; auto. Qed. (** * Correspondence between Mach code and Asm code *) diff --git a/backend/Bounds.v b/backend/Bounds.v index bcd28487..249ff796 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -69,7 +69,7 @@ Definition instr_within_bounds (i: instruction) := | Lbuiltin ef args res => forall r, In r res \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r | Lannot ef args => - forall sl ofs ty, In (S sl ofs ty) args -> slot_within_bounds sl ofs ty + forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args args) -> slot_within_bounds sl ofs ty | _ => True end. @@ -121,7 +121,7 @@ Definition slots_of_instr (i: instruction) : list (slot * Z * typ) := match i with | Lgetstack sl ofs ty r => (sl, ofs, ty) :: nil | Lsetstack r sl ofs ty => (sl, ofs, ty) :: nil - | Lannot ef args => slots_of_locs args + | Lannot ef args => slots_of_locs (params_of_annot_args args) | _ => nil end. diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 10cf8bf4..69b70e72 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -55,8 +55,7 @@ let mkef sg toks = | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] -> EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al) | [EFT_tok "annot"; EFT_string txt] -> - EF_annot(intern_string txt, - List.map (fun t -> AA_arg t) sg.sig_args) + EF_annot(intern_string txt, sg.sig_args) | [EFT_tok "annot_val"; EFT_string txt] -> if sg.sig_args = [] then raise Parsing.Parse_error; EF_annot_val(intern_string txt, List.hd sg.sig_args) diff --git a/backend/CSE.v b/backend/CSE.v index fa229871..2c0c5f33 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -492,6 +492,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb | EF_vload _ | EF_vload_global _ _ _ | EF_annot _ _ | EF_annot_val _ _ => set_unknown before res end + | Iannot ef args s => + before | Icond cond args ifso ifnot => before | Ijumptable arg tbl => diff --git a/backend/CSEproof.v b/backend/CSEproof.v index ae8052be..74e3ceca 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1144,6 +1144,21 @@ Proof. + apply CASE1. * apply set_reg_lessdef; auto. +- (* Iannot *) + exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. + intros (vargs' & A & B). + exploit external_call_mem_extends; eauto. + intros (v' & m1' & P & Q & R & S). + econstructor; split. + 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. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. replace m' with m; auto. + destruct ef; try contradiction. inv H2; auto. + - (* Icond *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. elim SAT; intros valu1 NH1. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index f952f1ea..d48a0553 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -296,7 +296,9 @@ Proof. econstructor; eauto with coqlib. (* Lannot *) left; econstructor; split. - econstructor; eauto. eapply external_call_symbols_preserved'; eauto. + econstructor; 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. econstructor; eauto with coqlib. (* Llabel *) diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 03ef0926..668eb808 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -79,6 +79,7 @@ Inductive stmt : Type := | Scall : option ident -> signature -> expr + ident -> exprlist -> stmt | Stailcall: signature -> expr + ident -> exprlist -> stmt | Sbuiltin : option ident -> external_function -> exprlist -> stmt + | Sannot : external_function -> list (annot_arg expr) -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -248,6 +249,32 @@ Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop := Genv.find_symbol ge id = Some b -> eval_expr_or_symbol le (inr _ id) (Vptr b Int.zero). +Inductive eval_annot_arg: annot_arg expr -> val -> Prop := + | eval_AA_base: forall a v, + eval_expr nil a v -> + eval_annot_arg (AA_base a) v + | eval_AA_int: forall n, + eval_annot_arg (AA_int n) (Vint n) + | eval_AA_long: forall n, + eval_annot_arg (AA_long n) (Vlong n) + | eval_AA_float: forall n, + eval_annot_arg (AA_float n) (Vfloat n) + | eval_AA_single: forall n, + eval_annot_arg (AA_single n) (Vsingle n) + | eval_AA_loadstack: forall chunk ofs v, + Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v -> + eval_annot_arg (AA_loadstack chunk ofs) v + | eval_AA_addrstack: forall ofs, + eval_annot_arg (AA_addrstack ofs) (Val.add sp (Vint ofs)) + | eval_AA_loadglobal: forall chunk id ofs v, + Mem.loadv chunk m (Genv.symbol_address ge id ofs) = Some v -> + eval_annot_arg (AA_loadglobal chunk id ofs) v + | eval_AA_addrglobal: forall id ofs, + eval_annot_arg (AA_addrglobal id ofs) (Genv.symbol_address ge id ofs) + | eval_AA_longofwords: forall a1 a2 v1 v2, + eval_expr nil a1 v1 -> eval_expr nil a2 v2 -> + eval_annot_arg (AA_longofwords (AA_base a1) (AA_base a2)) (Val.longofwords v1 v2). + End EVAL_EXPR. (** Pop continuation until a call or stop *) @@ -343,6 +370,13 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sbuiltin optid ef al) k sp e m) t (State f Sskip k sp (set_optvar optid v e) m') + | step_annot: forall f ef al k sp e m vl t v m', + match ef with EF_annot _ _ => True | _ => False end -> + list_forall2 (eval_annot_arg sp e m) al vl -> + external_call ef ge vl m t v m' -> + step (State f (Sannot ef al) k sp e m) + t (State f Sskip k sp e m') + | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) diff --git a/backend/Constprop.v b/backend/Constprop.v index bdfc4b17..ce56ff62 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -102,23 +102,22 @@ Definition num_iter := 10%nat. Definition successor (f: function) (ae: AE.t) (pc: node) : node := successor_rec num_iter f ae pc. -Fixpoint annot_strength_reduction - (ae: AE.t) (targs: list annot_arg) (args: list reg) := - match targs, args with - | AA_arg ty :: targs', arg :: args' => - let (targs'', args'') := annot_strength_reduction ae targs' args' in - match ty, areg ae arg with - | Tint, I n => (AA_int n :: targs'', args'') - | Tfloat, F n => if Compopts.generate_float_constants tt - then (AA_float n :: targs'', args'') - else (AA_arg ty :: targs'', arg :: args'') - | _, _ => (AA_arg ty :: targs'', arg :: args'') +Fixpoint annot_strength_reduction (ae: AE.t) (a: annot_arg reg) := + match a with + | AA_base r => + match areg ae r with + | I n => AA_int n + | L n => AA_long n + | F n => if Compopts.generate_float_constants tt then AA_float n else a + | FS n => if Compopts.generate_float_constants tt then AA_single n else a + | _ => a end - | targ :: targs', _ => - let (targs'', args'') := annot_strength_reduction ae targs' args in - (targ :: targs'', args'') - | _, _ => - (targs, args) + | AA_longofwords hi lo => + match annot_strength_reduction ae hi, annot_strength_reduction ae lo with + | AA_int nhi, AA_int nlo => AA_long (Int64.ofwords nhi nlo) + | hi', lo' => AA_longofwords hi' lo' + end + | _ => a end. Function builtin_strength_reduction @@ -134,9 +133,6 @@ Function builtin_strength_reduction | Ptr(Gl symb n1) => (EF_vstore_global chunk symb n1, r2 :: nil) | _ => (ef, args) end - | EF_annot text targs, args => - let (targs', args') := annot_strength_reduction ae targs args in - (EF_annot text targs', args') | _, _ => (ef, args) end. @@ -180,6 +176,8 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem) | Ibuiltin ef args res s => let (ef', args') := builtin_strength_reduction ae ef args in Ibuiltin ef' args' res s + | Iannot ef args s => + Iannot ef (List.map (annot_strength_reduction ae) args) s | Icond cond args s1 s2 => let aargs := aregs ae args in match resolve_branch (eval_static_condition cond aargs) with diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 450050de..30bdd674 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -211,83 +211,56 @@ Proof. unfold successor; intros. apply match_successor_rec. Qed. -Section BUILTIN_STRENGTH_REDUCTION. - -Variable bc: block_classification. -Hypothesis GE: genv_match bc ge. -Variable ae: AE.t. -Variable rs: regset. -Hypothesis MATCH: ematch bc rs ae. - Lemma annot_strength_reduction_correct: - forall targs args targs' args' eargs, - annot_strength_reduction ae targs args = (targs', args') -> - eventval_list_match ge eargs (annot_args_typ targs) rs##args -> - exists eargs', - eventval_list_match ge eargs' (annot_args_typ targs') rs##args' - /\ annot_eventvals targs' eargs' = annot_eventvals targs eargs. + forall bc sp m rs ae, ematch bc rs ae -> + forall a v, + eval_annot_arg ge (fun r => rs#r) sp m a v -> + eval_annot_arg ge (fun r => rs#r) sp m (annot_strength_reduction ae a) v. Proof. - induction targs; simpl; intros. -- inv H. simpl. exists eargs; auto. -- destruct a. - + destruct args as [ | arg args0]; simpl in H0; inv H0. - destruct (annot_strength_reduction ae targs args0) as [targs'' args''] eqn:E. - exploit IHtargs; eauto. intros [eargs'' [A B]]. - assert (DFL: - exists eargs', - eventval_list_match ge eargs' (annot_args_typ (AA_arg ty :: targs'')) rs##(arg :: args'') - /\ annot_eventvals (AA_arg ty :: targs'') eargs' = ev1 :: annot_eventvals targs evl). - { - exists (ev1 :: eargs''); split. - simpl; constructor; auto. simpl. congruence. - } - destruct ty; destruct (areg ae arg) as [] eqn:E2; inv H; auto. - * exists eargs''; split; auto; simpl; f_equal; auto. - generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM. - inv VM. rewrite <- H0 in *. inv H5; auto. - * destruct (Compopts.generate_float_constants tt); inv H1; auto. - exists eargs''; split; auto; simpl; f_equal; auto. - generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM. - inv VM. rewrite <- H0 in *. inv H5; auto. - + destruct (annot_strength_reduction ae targs args) as [targs'' args''] eqn:E. - inv H. - exploit IHtargs; eauto. intros [eargs'' [A B]]. - exists eargs''; simpl; split; auto. congruence. - + destruct (annot_strength_reduction ae targs args) as [targs'' args''] eqn:E. - inv H. - exploit IHtargs; eauto. intros [eargs'' [A B]]. - exists eargs''; simpl; split; auto. congruence. + induction 2; simpl; eauto with aarg. +- specialize (H x). unfold areg. destruct (AE.get x ae); try constructor. + + inv H. constructor. + + inv H. constructor. + + destruct (Compopts.generate_float_constants tt); [inv H|idtac]; constructor. + + destruct (Compopts.generate_float_constants tt); [inv H|idtac]; constructor. +- destruct (annot_strength_reduction ae hi); auto with aarg. + destruct (annot_strength_reduction ae lo); auto with aarg. + inv IHeval_annot_arg1; inv IHeval_annot_arg2. constructor. Qed. -Lemma vmatch_ptr_gl': - forall v id ofs, - vmatch bc v (Ptr (Gl id ofs)) -> - v = Vundef \/ exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b ofs. +Lemma annot_strength_reduction_correct_2: + forall bc sp m rs ae, ematch bc rs ae -> + forall al vl, + eval_annot_args ge (fun r => rs#r) sp m al vl -> + eval_annot_args ge (fun r => rs#r) sp m (List.map (annot_strength_reduction ae) al) vl. Proof. - intros. inv H; auto. inv H2. right; exists b; split; auto. eapply GE; eauto. -Qed. + induction 2; simpl; constructor; auto. eapply annot_strength_reduction_correct; eauto. +Qed. Lemma builtin_strength_reduction_correct: - forall ef args m t vres m', + forall bc ae rs ef args m t vres m', + genv_match bc ge -> + ematch bc rs ae -> external_call ef ge rs##args m t vres m' -> let (ef', args') := builtin_strength_reduction ae ef args in external_call ef' ge rs##args' m t vres m'. Proof. - intros until m'. functional induction (builtin_strength_reduction ae ef args); intros; auto. + intros until m'. intros GE MATCH. + assert (M: forall v id ofs, + vmatch bc v (Ptr (Gl id ofs)) -> + v = Vundef \/ exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b ofs). + { intros. inv H; auto. inv H2. right; exists b; split; auto. eapply GE; eauto. } + functional induction (builtin_strength_reduction ae ef args); intros; auto. + simpl in H. assert (V: vmatch bc (rs#r1) (Ptr (Gl symb n1))) by (rewrite <- e1; apply MATCH). - exploit vmatch_ptr_gl'; eauto. intros [A | [b [A B]]]. + exploit M; eauto. intros [A | [b [A B]]]. * simpl in H; rewrite A in H; inv H. * simpl; rewrite volatile_load_global_charact; simpl. exists b; split; congruence. + simpl in H. assert (V: vmatch bc (rs#r1) (Ptr (Gl symb n1))) by (rewrite <- e1; apply MATCH). - exploit vmatch_ptr_gl'; eauto. intros [A | [b [A B]]]. + exploit M; eauto. intros [A | [b [A B]]]. * simpl in H; rewrite A in H; inv H. * simpl; rewrite volatile_store_global_charact; simpl. exists b; split; congruence. -+ inv H. exploit annot_strength_reduction_correct; eauto. intros [eargs' [A B]]. - rewrite <- B. econstructor; eauto. Qed. -End BUILTIN_STRENGTH_REDUCTION. - (** The proof of semantic preservation is a simulation argument based on "option" diagrams of the following form: << @@ -521,6 +494,21 @@ Opaque builtin_strength_reduction. eapply match_states_succ; eauto. simpl; auto. apply set_reg_lessdef; auto. + (* Iannot *) + rename pc'0 into pc. TransfInstr; intros. + exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)). + apply REGS. eauto. + eapply annot_strength_reduction_correct_2 with (ae := ae); eauto. + intros (vargs' & A & B). + exploit external_call_mem_extends; eauto. + intros (v' & P & Q & R & S & T). + left; econstructor; econstructor; split. + eapply exec_Iannot; eauto. + eapply eval_annot_args_preserved. eexact symbols_preserved. eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply match_states_succ; eauto. + (* Icond, preserved *) rename pc' into pc. TransfInstr. set (ac := eval_static_condition cond (aregs ae args)). diff --git a/backend/Deadcode.v b/backend/Deadcode.v index 98bc14a8..9a8f85d2 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -70,6 +70,17 @@ Definition is_dead (v: nval) := Definition is_int_zero (v: nval) := match v with I n => Int.eq n Int.zero | _ => false end. +Fixpoint transfer_annot_arg (na: NA.t) (a: annot_arg reg) : NA.t := + let (ne, nm) := na in + match a with + | AA_base r => (add_need_all r ne, nm) + | AA_int _ | AA_long _ | AA_float _ | AA_single _ + | AA_addrstack _ | AA_addrglobal _ _ => (ne, nm) + | AA_loadstack chunk ofs => (ne, nmem_add nm (Stk ofs) (size_chunk chunk)) + | AA_loadglobal chunk id ofs => (ne, nmem_add nm (Gl id ofs) (size_chunk chunk)) + | AA_longofwords hi lo => transfer_annot_arg (transfer_annot_arg na hi) lo + end. + Function transfer_builtin (app: VA.t) (ef: external_function) (args: list reg) (res: reg) (ne: NE.t) (nm: nmem) : NA.t := match ef, args with @@ -128,6 +139,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t) nmem_dead_stack f.(fn_stacksize)) | Some(Ibuiltin ef args res s) => transfer_builtin approx!!pc ef args res ne nm + | Some(Iannot ef args s) => + List.fold_left transfer_annot_arg args after | Some(Icond cond args s1 s2) => (add_needs args (needs_of_condition cond) ne, nm) | Some(Ijumptable arg tbl) => diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 4d09c5ba..b998c631 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -547,39 +547,77 @@ Proof. eapply magree_monotone; eauto. intros; apply B; auto. Qed. -(** Properties of volatile memory accesses *) - -(* -Lemma transf_volatile_load: - - forall s f sp pc e m te r tm nm chunk t v m', - - volatile_load_sem chunk ge (addr :: nil) m t v m' -> - Val.lessdef addr taddr -> +(** Annotation arguments *) + +Lemma transfer_annot_arg_sound: + forall bc e e' sp m m' a v, + eval_annot_arg ge (fun r => e#r) (Vptr sp Int.zero) m a v -> + forall ne1 nm1 ne2 nm2, + transfer_annot_arg (ne1, nm1) a = (ne2, nm2) -> + eagree e e' ne2 -> + magree m m' (nlive ge sp nm2) -> genv_match bc ge -> bc sp = BCstack -> - pmatch - - sound_state prog (State s f (Vptr sp Int.zero) pc e m) -> - Val.lessdef e#r te#r -> - magree m tm - (nlive ge sp - (nmem_add nm (aaddr (vanalyze rm f) # pc r) (size_chunk chunk))) -> - m' = m /\ - exists tv, volatile_load_sem chunk ge (te#r :: nil) tm t tv tm /\ Val.lessdef v tv. + exists v', + eval_annot_arg ge (fun r => e'#r) (Vptr sp Int.zero) m' a v' + /\ Val.lessdef v v' + /\ eagree e e' ne1 + /\ magree m m' (nlive ge sp nm1). Proof. - intros. inv H2. split; auto. rewrite <- H3 in H0; inv H0. inv H4. -- (* volatile *) - exists (Val.load_result chunk v0); split; auto. - constructor. constructor; auto. -- (* not volatile *) + induction 1; simpl; intros until nm2; intros TR EA MA GM SPM; inv TR. +- exists e'#x; intuition auto. constructor. eauto 2 with na. eauto 2 with na. +- exists (Vint n); intuition auto. constructor. +- exists (Vlong n); intuition auto. constructor. +- exists (Vfloat n); intuition auto. constructor. +- exists (Vsingle n); intuition auto. constructor. +- simpl in H. exploit magree_load; eauto. + intros. eapply nlive_add; eauto with va. rewrite Int.add_zero_l in H0; auto. + intros (v' & A & B). + exists v'; intuition auto. constructor; auto. + eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto. +- exists (Vptr sp (Int.add Int.zero ofs)); intuition auto with na. constructor. +- unfold Senv.symbol_address in H; simpl in H. + destruct (Genv.find_symbol ge id) as [b|] eqn:FS; simpl in H; try discriminate. exploit magree_load; eauto. - exploit aaddr_sound; eauto. intros (bc & P & Q & R). - intros. eapply nlive_add; eauto. - intros (v' & P & Q). - exists v'; split. constructor. econstructor; eauto. auto. + intros. eapply nlive_add; eauto. constructor. apply GM; auto. + intros (v' & A & B). + exists v'; intuition auto. + constructor. simpl. unfold Senv.symbol_address; simpl; rewrite FS; auto. + eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto. +- exists (Senv.symbol_address ge id ofs); intuition auto with na. constructor. +- destruct (transfer_annot_arg (ne1, nm1) hi) as [ne' nm'] eqn:TR. + exploit IHeval_annot_arg2; eauto. intros (vlo' & A & B & C & D). + exploit IHeval_annot_arg1; eauto. intros (vhi' & P & Q & R & S). + exists (Val.longofwords vhi' vlo'); intuition auto. + constructor; auto. + apply Val.longofwords_lessdef; auto. +Qed. + +Lemma transfer_annot_args_sound: + forall e sp m e' m' bc al vl, + eval_annot_args ge (fun r => e#r) (Vptr sp Int.zero) m al vl -> + forall ne1 nm1 ne2 nm2, + List.fold_left transfer_annot_arg al (ne1, nm1) = (ne2, nm2) -> + eagree e e' ne2 -> + magree m m' (nlive ge sp nm2) -> + genv_match bc ge -> + bc sp = BCstack -> + exists vl', + eval_annot_args ge (fun r => e'#r) (Vptr sp Int.zero) m' al vl' + /\ Val.lessdef_list vl vl' + /\ eagree e e' ne1 + /\ magree m m' (nlive ge sp nm1). +Proof. +Local Opaque transfer_annot_arg. + induction 1; simpl; intros. +- inv H. exists (@nil val); intuition auto. constructor. +- destruct (transfer_annot_arg (ne1, nm1) a1) as [ne' nm'] eqn:TR. + exploit IHlist_forall2; eauto. intros (vs' & A1 & B1 & C1 & D1). + exploit transfer_annot_arg_sound; eauto. intros (v1' & A2 & B2 & C2 & D2). + exists (v1' :: vs'); intuition auto. constructor; auto. Qed. -*) + +(** Properties of volatile memory accesses *) Lemma transf_volatile_store: forall v1 v2 v1' v2' m tm chunk sp nm t v m', @@ -930,6 +968,21 @@ Ltac UseTransfer := apply eagree_update; eauto 3 with na. eapply mextends_agree; eauto. +- (* annot *) + TransfInstr; UseTransfer. + destruct (fold_left transfer_annot_arg args (ne, nm)) as [ne1 nm1] eqn:TR; simpl in *. + inv SS. exploit transfer_annot_args_sound; eauto. intros (vargs' & A & B & C & D). + assert (EC: m' = m /\ external_call ef ge vargs' tm t Vundef tm). + { destruct ef; try contradiction. inv H2. split; auto. simpl. constructor. + eapply eventval_list_match_lessdef; eauto. } + destruct EC as [EC1 EC2]; subst m'. + econstructor; split. + eapply exec_Iannot. eauto. auto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved with (ge1 := ge); eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply match_succ_states; eauto. simpl; auto. + - (* conditional *) TransfInstr; UseTransfer. econstructor; split. diff --git a/backend/Inlining.v b/backend/Inlining.v index cd347345..4f17d59c 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -203,6 +203,15 @@ Definition sop (ctx: context) (op: operation) := Definition saddr (ctx: context) (addr: addressing) := shift_stack_addressing (Int.repr ctx.(dstk)) addr. +Fixpoint sannotarg (ctx: context) (a: annot_arg reg) : annot_arg reg := + match a with + | AA_base x => AA_base (sreg ctx x) + | AA_loadstack chunk ofs => AA_loadstack chunk (Int.add ofs (Int.repr ctx.(dstk))) + | AA_addrstack ofs => AA_addrstack (Int.add ofs (Int.repr ctx.(dstk))) + | AA_longofwords hi lo => AA_longofwords (sannotarg ctx hi) (sannotarg ctx lo) + | _ => a + end. + (** The initial context, used to copy the CFG of a toplevel function. *) Definition initcontext (dpc dreg nreg: positive) (sz: Z) := @@ -382,6 +391,9 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit := | Ibuiltin ef args res s => set_instr (spc ctx pc) (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s)) + | Iannot ef args s => + set_instr (spc ctx pc) + (Iannot ef (map (sannotarg ctx) args) (spc ctx s)) | Icond cond args s1 s2 => set_instr (spc ctx pc) (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2)) diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 9b1aec4c..e3c5bf2a 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -400,6 +400,63 @@ Proof. eapply function_ptr_translated; eauto. Qed. +(** Translation of annotation arguments. *) + +Lemma tr_annot_arg: + forall F bound ctx rs rs' sp sp' m m', + match_globalenvs F bound -> + agree_regs F ctx rs rs' -> + F sp = Some(sp', ctx.(dstk)) -> + Mem.inject F m m' -> + forall a v, + eval_annot_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v -> + exists v', eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (sannotarg ctx a) v' + /\ val_inject F v v'. +Proof. + intros until m'; intros MG AG SP MI. induction 1; simpl. +- exists rs'#(sreg ctx x); split. constructor. eapply agree_val_reg; eauto. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- exploit Mem.loadv_inject; eauto. + instantiate (1 := Vptr sp' (Int.add ofs (Int.repr (dstk ctx)))). + simpl. econstructor; eauto. rewrite Int.add_zero_l; auto. + intros (v' & A & B). exists v'; split; auto. constructor. simpl. rewrite Int.add_zero_l; auto. +- econstructor; split. constructor. simpl. econstructor; eauto. rewrite ! Int.add_zero_l; auto. +- assert (val_inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). + { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. + inv MG. econstructor. eauto. rewrite Int.add_zero; auto. } + exploit Mem.loadv_inject; eauto. intros (v' & A & B). + exists v'; eauto with aarg. +- econstructor; split. constructor. + unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. + inv MG. econstructor. eauto. rewrite Int.add_zero; auto. +- destruct IHeval_annot_arg1 as (v1 & A1 & B1). + destruct IHeval_annot_arg2 as (v2 & A2 & B2). + econstructor; split. eauto with aarg. apply val_longofwords_inject; auto. +Qed. + +Lemma tr_annot_args: + forall F bound ctx rs rs' sp sp' m m', + match_globalenvs F bound -> + agree_regs F ctx rs rs' -> + F sp = Some(sp', ctx.(dstk)) -> + Mem.inject F m m' -> + forall al vl, + eval_annot_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl -> + exists vl', eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (map (sannotarg ctx) al) vl' + /\ val_list_inject F vl vl'. +Proof. + induction 5; simpl. +- exists (@nil val); split; constructor. +- exploit tr_annot_arg; eauto. intros (v1' & A & B). + destruct IHlist_forall2 as (vl' & C & D). + exists (v1' :: vl'); split; constructor; auto. +Qed. + (** ** Relating stacks *) Inductive match_stacks (F: meminj) (m m': mem): @@ -1030,6 +1087,29 @@ Proof. auto. intros. apply SSZ2. eapply external_call_max_perm; eauto. +(* annot *) + exploit tr_funbody_inv; eauto. intros TR; inv TR. + exploit match_stacks_inside_globalenvs; eauto. intros [bound MG]. + exploit tr_annot_args; eauto. intros (vargs' & P & Q). + exploit external_call_mem_inject; eauto. + eapply match_stacks_inside_globals; eauto. + intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]]. + left; econstructor; split. + eapply plus_one. eapply exec_Iannot; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + econstructor. + eapply match_stacks_inside_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. + intros; eapply external_call_max_perm; eauto. + intros; eapply external_call_max_perm; eauto. + auto. + eapply agree_regs_incr; eauto. auto. auto. + eapply external_call_valid_block; eauto. + eapply range_private_extcall; eauto. + intros; eapply external_call_max_perm; eauto. + auto. + intros. apply SSZ2. eapply external_call_max_perm; eauto. + (* cond *) exploit tr_funbody_inv; eauto. intros TR; inv TR. assert (eval_condition cond rs'##(sregs ctx args) m' = Some b). diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index b5948a22..f7e6c317 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -316,6 +316,9 @@ Inductive tr_instr: context -> node -> instruction -> code -> Prop := Ple res ctx.(mreg) -> c!(spc ctx pc) = Some (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s)) -> tr_instr ctx pc (Ibuiltin ef args res s) c + | tr_annot: forall ctx pc c ef args s, + c!(spc ctx pc) = Some (Iannot ef (map (sannotarg ctx) args) (spc ctx s)) -> + tr_instr ctx pc (Iannot ef args s) c | tr_cond: forall ctx pc cond args s1 s2 c, c!(spc ctx pc) = Some (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2)) -> tr_instr ctx pc (Icond cond args s1 s2) c diff --git a/backend/LTL.v b/backend/LTL.v index dd79c8e3..8c2749a7 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -45,7 +45,7 @@ Inductive instruction: Type := | Lcall (sg: signature) (ros: mreg + ident) | Ltailcall (sg: signature) (ros: mreg + ident) | Lbuiltin (ef: external_function) (args: list mreg) (res: list mreg) - | Lannot (ef: external_function) (args: list loc) + | Lannot (ef: external_function) (args: list (annot_arg loc)) | Lbranch (s: node) | Lcond (cond: condition) (args: list mreg) (s1 s2: node) | Ljumptable (arg: mreg) (tbl: list node) @@ -244,8 +244,9 @@ Inductive step: state -> trace -> state -> Prop := rs' = Locmap.setlist (map R res) vl (undef_regs (destroyed_by_builtin ef) rs) -> step (Block s f sp (Lbuiltin ef args res :: bb) rs m) t (Block s f sp bb rs' m') - | exec_Lannot: forall s f sp ef args bb rs m t vl m', - external_call' ef ge (map rs args) m t vl m' -> + | exec_Lannot: forall s f sp ef args bb rs vl m t v' m', + eval_annot_args ge rs sp m args vl -> + external_call ef ge vl m t v' m' -> step (Block s f sp (Lannot ef args :: bb) rs m) t (Block s f sp bb rs m') | exec_Lbranch: forall s f sp pc bb rs m, diff --git a/backend/Linear.v b/backend/Linear.v index 56d1eb99..5d1fc0d8 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -42,7 +42,7 @@ Inductive instruction: Type := | Lcall: signature -> mreg + ident -> instruction | Ltailcall: signature -> mreg + ident -> instruction | Lbuiltin: external_function -> list mreg -> list mreg -> instruction - | Lannot: external_function -> list loc -> instruction + | Lannot: external_function -> list (annot_arg loc) -> instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list mreg -> label -> instruction @@ -204,8 +204,9 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Lbuiltin ef args res :: b) rs m) t (State s f sp b rs' m') | exec_Lannot: - forall s f sp rs m ef args b t v m', - external_call' ef ge (map rs args) m t v m' -> + forall s f sp rs m ef args vl b t v m', + eval_annot_args ge rs sp m args vl -> + external_call ef ge vl m t v m' -> step (State s f sp (Lannot ef args :: b) rs m) t (State s f sp b rs m') | exec_Llabel: diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 63fa6565..08bcd3f3 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -651,7 +651,8 @@ Proof. (* Lannot *) left; econstructor; split. simpl. apply plus_one. eapply exec_Lannot; eauto. - eapply external_call_symbols_preserved'; 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. econstructor; eauto. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index ccf17e1e..c093b62d 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -76,7 +76,7 @@ Definition wt_instr (i: instruction) : bool := | Lbuiltin ef args res => subtype_list (proj_sig_res' (ef_sig ef)) (map mreg_type res) | Lannot ef args => - forallb loc_valid args + forallb loc_valid (params_of_annot_args args) | _ => true end. @@ -365,7 +365,7 @@ Qed. Lemma wt_state_annot: forall s f sp ef args c rs m, wt_state (State s f sp (Lannot ef args :: c) rs m) -> - forallb (loc_valid f) args = true. + forallb (loc_valid f) (params_of_annot_args args) = true. Proof. intros. inv H. simpl in WTC; InvBooleans. auto. Qed. diff --git a/backend/Liveness.v b/backend/Liveness.v index 3a5bde97..ce1a798a 100644 --- a/backend/Liveness.v +++ b/backend/Liveness.v @@ -93,6 +93,8 @@ Definition transfer reg_list_live args (reg_sum_live ros Regset.empty) | Ibuiltin ef args res s => reg_list_live args (reg_dead res after) + | Iannot ef args s => + reg_list_live (params_of_annot_args args) after | Icond cond args ifso ifnot => reg_list_live args after | Ijumptable arg tbl => diff --git a/backend/Mach.v b/backend/Mach.v index ff72a828..fe00d42d 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -61,16 +61,12 @@ Inductive instruction: Type := | Mcall: signature -> mreg + ident -> instruction | Mtailcall: signature -> mreg + ident -> instruction | Mbuiltin: external_function -> list mreg -> list mreg -> instruction - | Mannot: external_function -> list annot_param -> instruction + | Mannot: external_function -> list (annot_arg mreg) -> instruction | Mlabel: label -> instruction | Mgoto: label -> instruction | Mcond: condition -> list mreg -> label -> instruction | Mjumptable: mreg -> list label -> instruction - | Mreturn: instruction - -with annot_param: Type := - | APreg: mreg -> annot_param - | APstack: memory_chunk -> Z -> annot_param. + | Mreturn: instruction. Definition code := list instruction. @@ -225,19 +221,6 @@ Definition extcall_arguments (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := list_forall2 (extcall_arg rs m sp) (loc_arguments sg) args. -(** Extract the values of the arguments to an annotation. *) - -Inductive annot_arg: regset -> mem -> val -> annot_param -> val -> Prop := - | annot_arg_reg: forall rs m sp r, - annot_arg rs m sp (APreg r) (rs r) - | annot_arg_stack: forall rs m stk base chunk ofs v, - Mem.load chunk m stk (Int.unsigned base + ofs) = Some v -> - annot_arg rs m (Vptr stk base) (APstack chunk ofs) v. - -Definition annot_arguments - (rs: regset) (m: mem) (sp: val) (params: list annot_param) (args: list val) : Prop := - list_forall2 (annot_arg rs m sp) params args. - (** Mach execution states. *) (** Mach execution states. *) @@ -352,8 +335,8 @@ Inductive step: state -> trace -> state -> Prop := t (State s f sp b rs' m') | exec_Mannot: forall s f sp rs m ef args b vargs t v m', - annot_arguments rs m sp args vargs -> - external_call' ef ge vargs m t v m' -> + eval_annot_args ge rs sp m args vargs -> + external_call ef ge vargs m t v m' -> step (State s f sp (Mannot ef args :: b) rs m) t (State s f sp b rs m') | exec_Mgoto: diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml index 7b0c1083..995f22dd 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -97,11 +97,34 @@ let print_file_line_d2 oc pref file line = let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" -type arg_value = - | Reg of preg - | Stack of memory_chunk * Int.int - | Intconst of Int.int - | Floatconst of float +let rec print_annot print_preg sp_reg_name oc = function + | AA_base x -> print_preg oc x + | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n) + | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) + | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) + | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) + | AA_loadstack(chunk, ofs) -> + fprintf oc "mem(%s + %ld, %ld)" + sp_reg_name + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | AA_addrstack ofs -> + fprintf oc "(%s + %ld)" + sp_reg_name + (camlint_of_coqint ofs) + | AA_loadglobal(chunk, id, ofs) -> + fprintf oc "mem(\"%s\" + %ld, %ld)" + (extern_atom id) + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | AA_addrglobal(id, ofs) -> + fprintf oc "(\"%s\" + %ld)" + (extern_atom id) + (camlint_of_coqint ofs) + | AA_longofwords(hi, lo) -> + fprintf oc "(%a * 0x100000000 + %a)" + (print_annot print_preg sp_reg_name) hi + (print_annot print_preg sp_reg_name) lo let print_annot_text print_preg sp_reg_name oc txt args = let print_fragment = function @@ -112,42 +135,18 @@ let print_annot_text print_preg sp_reg_name oc txt args = | Str.Delim s -> let n = int_of_string (String.sub s 1 (String.length s - 1)) in try - match List.nth args (n-1) with - | Reg r -> - print_preg oc r - | Stack(chunk, ofs) -> - fprintf oc "mem(%s + %ld, %ld)" - sp_reg_name - (camlint_of_coqint ofs) - (camlint_of_coqint (size_chunk chunk)) - | Intconst n -> - fprintf oc "%ld" (camlint_of_coqint n) - | Floatconst n -> - fprintf oc "%.18g" (camlfloat_of_coqfloat n) + print_annot print_preg sp_reg_name oc (List.nth args (n-1)) with Failure _ -> fprintf oc "<bad parameter %s>" s in List.iter print_fragment (Str.full_split re_annot_param txt); fprintf oc "\n" -let rec annot_args tmpl args = - match tmpl, args with - | [], _ -> [] - | AA_arg _ :: tmpl', APreg r :: args' -> - Reg r :: annot_args tmpl' args' - | AA_arg _ :: tmpl', APstack(chunk, ofs) :: args' -> - Stack(chunk, ofs) :: annot_args tmpl' args' - | AA_arg _ :: tmpl', [] -> [] (* should never happen *) - | AA_int n :: tmpl', _ -> - Intconst n :: annot_args tmpl' args - | AA_float n :: tmpl', _ -> - Floatconst n :: annot_args tmpl' args - -let print_annot_stmt print_preg sp_reg_name oc txt tmpl args = - print_annot_text print_preg sp_reg_name oc txt (annot_args tmpl args) +let print_annot_stmt print_preg sp_reg_name oc txt tys args = + print_annot_text print_preg sp_reg_name oc txt args let print_annot_val print_preg oc txt args = print_annot_text print_preg "<internal error>" oc txt - (List.map (fun r -> Reg r) args) + (List.map (fun r -> AA_base r) args) (* Print CompCert version and command-line as asm comment *) diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index 52e51309..27936f9b 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -81,8 +81,8 @@ let print_instruction pp succ = function fprintf pp "%a = %s(%a)" mregs res (name_of_external ef) mregs args | Lannot(ef, args) -> - fprintf pp "%s(%a)" - (name_of_external ef) locs args + fprintf pp "%s(%a)\n" + (name_of_external ef) (print_annot_args loc) args | Lbranch s -> print_succ pp s succ | Lcond(cond, args, s1, s2) -> diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index b356ca9e..8484a5c3 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -34,15 +34,6 @@ let rec regs pp = function | [r] -> reg pp r | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl -let annot_param pp = function - | APreg r -> reg pp r - | APstack(chunk, ofs) -> fprintf pp "stack(%s,%ld)" (name_of_chunk chunk) (camlint_of_coqint ofs) - -let rec annot_params pp = function - | [] -> () - | [r] -> annot_param pp r - | r1::rl -> fprintf pp "%a, %a" annot_param r1 annot_params rl - let ros pp = function | Coq_inl r -> reg pp r | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) @@ -78,7 +69,8 @@ let print_instruction pp i = fprintf pp "\t%a = %s(%a)\n" regs res (name_of_external ef) regs args | Mannot(ef, args) -> - fprintf pp "\t%s(%a)\n" (name_of_external ef) annot_params args + fprintf pp "\t%s(%a)\n" + (name_of_external ef) (print_annot_args reg) args | Mlabel lbl -> fprintf pp "%5d:" (P.to_int lbl) | Mgoto lbl -> diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 5c8347cb..ce2275cf 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -74,6 +74,10 @@ let print_instruction pp (pc, i) = fprintf pp "%a = %s(%a)\n" reg res (name_of_external ef) regs args; print_succ pp s (pc - 1) + | Iannot(ef, args, s) -> + fprintf pp "%s(%a)\n" + (name_of_external ef) (print_annot_args reg) args; + print_succ pp s (pc - 1) | Icond(cond, args, s1, s2) -> fprintf pp "if (%a) goto %d else goto %d\n" (PrintOp.print_condition reg) (cond, args) diff --git a/backend/RTL.v b/backend/RTL.v index e8ec1391..83761c42 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -74,6 +74,9 @@ Inductive instruction: Type := (** [Ibuiltin ef args dest succ] calls the built-in function identified by [ef], giving it the values of [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) + | Iannot: external_function -> list (annot_arg reg) -> node -> instruction + (** [Iannot ef args succ] is similar to [Ibuiltin] but specialized + to annotations. *) | Icond: condition -> list reg -> node -> node -> instruction (** [Icond cond args ifso ifnot] evaluates the boolean condition [cond] over the values of registers [args]. If the condition @@ -255,6 +258,14 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge rs##args m t v m' -> step (State s f sp pc rs m) t (State s f sp pc' (rs#res <- v) m') + | exec_Iannot: + forall s f sp pc rs m ef args pc' vargs vres t m', + (fn_code f)!pc = Some(Iannot ef args pc') -> + match ef with EF_annot _ _ => True | _ => False end -> + eval_annot_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + step (State s f sp pc rs m) + t (State s f sp pc' rs m') | exec_Icond: forall s f sp pc rs m cond args ifso ifnot b pc', (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> @@ -358,11 +369,14 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (State s0 f sp pc' (rs#res <- vres2) m2). eapply exec_Ibuiltin; eauto. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (State s0 f sp pc' rs m2). eapply exec_Iannot; eauto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate s0 vres2 m2). econstructor; eauto. (* trace length *) red; intros; inv H; simpl; try omega. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. Qed. (** * Operations on RTL abstract syntax *) @@ -397,6 +411,7 @@ Definition successors_instr (i: instruction) : list node := | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil | Ibuiltin ef args res s => s :: nil + | Iannot ef args s => s :: nil | Icond cond args ifso ifnot => ifso :: ifnot :: nil | Ijumptable arg tbl => tbl | Ireturn optarg => nil @@ -418,6 +433,7 @@ Definition instr_uses (i: instruction) : list reg := | Itailcall sig (inl r) args => r :: args | Itailcall sig (inr id) args => args | Ibuiltin ef args res s => args + | Iannot ef args s => params_of_annot_args args | Icond cond args ifso ifnot => args | Ijumptable arg tbl => arg :: nil | Ireturn None => nil @@ -435,6 +451,7 @@ Definition instr_defs (i: instruction) : option reg := | Icall sig ros args res s => Some res | Itailcall sig ros args => None | Ibuiltin ef args res s => Some res + | Iannot ef args s => None | Icond cond args ifso ifnot => None | Ijumptable arg tbl => None | Ireturn optarg => None @@ -476,6 +493,7 @@ Definition max_reg_instr (m: positive) (pc: node) (i: instruction) := | Itailcall sig (inl r) args => fold_left Pmax args (Pmax r m) | Itailcall sig (inr id) args => fold_left Pmax args m | Ibuiltin ef args res s => fold_left Pmax args (Pmax res m) + | Iannot ef args s => fold_left Pmax (params_of_annot_args args) m | Icond cond args ifso ifnot => fold_left Pmax args m | Ijumptable arg tbl => Pmax arg m | Ireturn None => m diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 26f51e3f..b1c36513 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -455,6 +455,39 @@ with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) transl_expr map b r nc end. +(** Translation of arguments to annotations. *) + +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 => + 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 => + 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 {A: Type} (al: list (annot_arg expr)) (rl: list A) : list (annot_arg A) := + match al with + | nil => nil + | a1 :: al => + let (a1', rl1) := convert_annot_arg a1 rl in a1' :: convert_annot_args al rl1 + end. + (** Auxiliary for translating exit expressions. *) Definition transl_exit (nexits: list node) (n: nat) : mon node := @@ -558,6 +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 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 8acce510..02460f67 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -972,6 +972,234 @@ Proof. auto. 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 + (MWF: map_wf map) + (TR: tr_annot_arg f.(fn_code) map pr a ns nd a') + (ME: match_env map e nil rs) + (EXT: Mem.extends m tm), + exists rs', exists tm', exists v', + star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm') + /\ match_env map e nil rs' + /\ Events.eval_annot_arg tge (fun r => rs'#r) sp tm' a' v' + /\ Val.lessdef v v' + /\ (forall r, In r pr -> rs'#r = rs#r) + /\ Mem.extends m tm'. + +Theorem transl_annot_arg_correct: + forall a v, + eval_annot_arg ge sp e m a v -> + transl_annot_arg_prop a v. +Proof. + induction 1; red; intros; inv TR. +- exploit transl_expr_correct; eauto. intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exists rs1, tm1, rs1#r; intuition eauto. constructor. +- exists rs, tm, (Vint n); intuition auto using star_refl with aarg. +- exists rs, tm, (Vlong n); intuition auto using star_refl with aarg. +- exists rs, tm, (Vfloat n); intuition auto using star_refl with aarg. +- exists rs, tm, (Vsingle n); intuition auto using star_refl with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). + exists rs, tm, v'; intuition auto using star_refl with aarg. +- exists rs, tm, (Val.add sp (Vint ofs)); intuition auto using star_refl with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). + replace (Genv.symbol_address ge id ofs) + with (Senv.symbol_address tge id ofs) in P. + exists rs, tm, v'; intuition auto using star_refl with aarg. + unfold Genv.symbol_address, Senv.symbol_address. simpl. + rewrite symbols_preserved; auto. +- exists rs, tm, (Senv.symbol_address tge id ofs); intuition auto using star_refl with aarg. + unfold Genv.symbol_address, Senv.symbol_address. simpl. + rewrite symbols_preserved; auto. +- inv H5. inv H9. simpl in H5. + exploit transl_expr_correct. eexact H. eauto. eauto. eauto. eauto. + intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exploit transl_expr_correct. eexact H0. eauto. eauto. eauto. eauto. + intros (rs2 & tm2 & A2 & B2 & C2 & D2 & E2). + exists rs2, tm2, (Val.longofwords rs2#r rs2#r0); intuition auto. + eapply star_trans; eauto. + constructor. constructor. constructor. + 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 + (MWF: map_wf map) + (TR: tr_annot_args f.(fn_code) map pr l ns nd l') + (ME: match_env map e nil rs) + (EXT: Mem.extends m tm), + exists rs', exists tm', exists vl', + star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm') + /\ match_env map e nil rs' + /\ eval_annot_args tge (fun r => rs'#r) sp tm' l' vl' + /\ Val.lessdef_list vl vl' + /\ (forall r, In r pr -> rs'#r = rs#r) + /\ Mem.extends m tm'. + +Theorem transl_annot_args_correct: + forall l vl, + list_forall2 (eval_annot_arg ge sp e m) l vl -> + transl_annot_args_prop l vl. +Proof. + induction 1; red; intros. +- inv TR. exists rs, tm, (@nil val). + split. constructor. + split. auto. + split. constructor. + split. constructor. + split. auto. + auto. +- inv TR. inv H; inv H5. + + exploit transl_expr_correct; eauto. + intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exploit (IHlist_forall2 tm1 cs); eauto. + intros (rs2 & tm2 & vl2 & A2 & B2 & C2 & D2 & E2 & F2). simpl in E2. + exists rs2, tm2, (rs2#r :: vl2); intuition auto. + eapply star_trans; eauto. + constructor; auto. constructor. + rewrite E2; auto. + transitivity rs1#r0; auto. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vint n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vlong n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vfloat n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Vsingle n :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exploit Mem.loadv_extends; eauto. intros (v1' & P & Q). + exists rs', tm', (v1' :: vl'); simpl; intuition auto. constructor; eauto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Val.add sp (Vint ofs) :: vl'); simpl; intuition auto. constructor; auto with aarg. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exploit Mem.loadv_extends; eauto. intros (v1' & P & Q). + replace (Genv.symbol_address ge id ofs) + with (Senv.symbol_address tge id ofs) in P. + exists rs', tm', (v1' :: vl'); simpl; intuition auto. constructor; auto with aarg. + unfold Genv.symbol_address, Senv.symbol_address. simpl. + rewrite symbols_preserved; auto. + + exploit (IHlist_forall2 tm cs); eauto. + intros (rs' & tm' & vl' & A & B & C & D & E & F). + exists rs', tm', (Genv.symbol_address tge id ofs :: vl'); simpl; intuition auto. + constructor; auto with aarg. constructor. + unfold Genv.symbol_address. rewrite symbols_preserved; auto. + + inv H7. inv H12. + exploit transl_expr_correct. eexact H1. eauto. eauto. eauto. eauto. + intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1). + exploit transl_expr_correct. eexact H2. eauto. eauto. eauto. eexact E1. + intros (rs2 & tm2 & A2 & B2 & C2 & D2 & E2). simpl in D2. + exploit (IHlist_forall2 tm2 cs); eauto. + intros (rs3 & tm3 & vl3 & A3 & B3 & C3 & D3 & E3 & F3). simpl in E3. + exists rs3, tm3, (Val.longofwords rs3#r rs3#r0 :: vl3); intuition auto. + eapply star_trans; eauto. eapply star_trans; eauto. auto. + constructor; auto with aarg. constructor. constructor. constructor. + constructor; auto. apply Val.longofwords_lessdef. + rewrite E3, D2; auto. + rewrite E3; auto. + transitivity rs1#r1; auto. transitivity rs2#r1; auto. +Qed. +*) + End CORRECTNESS_EXPR. (** ** Measure over CminorSel states *) @@ -1304,6 +1532,25 @@ Proof. econstructor; eauto. constructor. eapply match_env_update_dest; eauto. + (* annot *) + 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. + econstructor; eauto. constructor. + (* seq *) inv TS. econstructor; split. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 32f35bb4..1ca9faa0 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -220,6 +220,13 @@ Proof. intros; red; intros. elim H1; intro. subst r1; auto. auto. Qed. +Lemma regs_valid_app: + forall rl1 rl2 s, + regs_valid rl1 s -> regs_valid rl2 s -> regs_valid (rl1 ++ rl2) s. +Proof. + intros; red; intros. apply in_app_iff in H1. destruct H1; auto. +Qed. + Lemma regs_valid_incr: forall s1 s2 rl, state_incr s1 s2 -> regs_valid rl s1 -> regs_valid rl s2. Proof. @@ -847,6 +854,10 @@ 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 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 -> tr_stmt c map s1 ns n nexits ngoto nret rret -> @@ -1196,7 +1207,7 @@ Proof. apply tr_exitexpr_incr with s1; auto. eapply IHa; eauto with rtlg. apply add_letvar_valid; eauto with rtlg. 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) @@ -1250,6 +1261,9 @@ Proof. econstructor; eauto 4 with rtlg. 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_exprlist_charact; eauto 3 with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 5042c775..8961fc0b 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -65,6 +65,20 @@ Variable env: regenv. Definition valid_successor (s: node) : Prop := exists i, funct.(fn_code)!s = Some i. +Definition type_of_annot_arg (a: annot_arg reg) : typ := + match a with + | AA_base r => env r + | AA_int _ => Tint + | AA_long _ => Tlong + | AA_float _ => Tfloat + | AA_single _ => Tsingle + | AA_loadstack chunk ofs => type_of_chunk chunk + | AA_addrstack ofs => Tint + | AA_loadglobal chunk id ofs => type_of_chunk chunk + | AA_addrglobal id ofs => Tint + | AA_longofwords hi lo => Tlong + end. + Inductive wt_instr : instruction -> Prop := | wt_Inop: forall s, @@ -114,6 +128,11 @@ Inductive wt_instr : instruction -> Prop := env res = proj_sig_res (ef_sig ef) -> valid_successor s -> wt_instr (Ibuiltin ef args res s) + | wt_Iannot: + forall ef args s, + map type_of_annot_arg args = (ef_sig ef).(sig_args) -> + valid_successor s -> + wt_instr (Iannot ef args s) | wt_Icond: forall cond args s1 s2, map env args = type_of_condition cond -> @@ -211,6 +230,32 @@ Definition type_ros (e: S.typenv) (ros: reg + ident) : res S.typenv := Definition is_move (op: operation) : bool := match op with Omove => true | _ => false end. +Definition type_expect (e: S.typenv) (t1 t2: typ) : res S.typenv := + if typ_eq t1 t2 then OK e else Error(msg "unexpected type"). + +Definition type_annot_arg (e: S.typenv) (a: annot_arg reg) (ty: typ) : res S.typenv := + match a with + | AA_base r => S.set e r ty + | AA_int _ => type_expect e ty Tint + | AA_long _ => type_expect e ty Tlong + | AA_float _ => type_expect e ty Tfloat + | AA_single _ => type_expect e ty Tsingle + | AA_loadstack chunk ofs => type_expect e ty (type_of_chunk chunk) + | AA_addrstack ofs => type_expect e ty Tint + | AA_loadglobal chunk id ofs => type_expect e ty (type_of_chunk chunk) + | AA_addrglobal id ofs => type_expect e ty Tint + | AA_longofwords hi lo => type_expect e ty Tlong + end. + +Fixpoint type_annot_args (e: S.typenv) (al: list (annot_arg reg)) (tyl: list typ) : res S.typenv := + match al, tyl with + | nil, nil => OK e + | a1 :: al, ty1 :: tyl => + do e1 <- type_annot_arg e a1 ty1; type_annot_args e1 al tyl + | _, _ => + Error (msg "annotation arity mismatch") + end. + Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := match i with | Inop s => @@ -251,6 +296,9 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := do x <- check_successor s; do e1 <- S.set_list e args sig.(sig_args); S.set e1 res (proj_sig_res sig) + | Iannot ef args s => + do x <- check_successor s; + type_annot_args e args (sig_args (ef_sig ef)) | Icond cond args s1 s2 => do x1 <- check_successor s1; do x2 <- check_successor s2; @@ -332,6 +380,55 @@ Proof. monadInv H. destruct H0. subst a; eauto with ty. eauto. Qed. +Remark type_expect_incr: + forall e ty1 ty2 e' te, type_expect e ty1 ty2 = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + unfold type_expect; intros. destruct (typ_eq ty1 ty2); inv H. auto. +Qed. + +Hint Resolve type_expect_incr: ty. + +Lemma type_expect_sound: + forall e ty1 ty2 e', type_expect e ty1 ty2 = OK e' -> ty1 = ty2. +Proof. + unfold type_expect; intros. destruct (typ_eq ty1 ty2); inv H. auto. +Qed. + +Lemma type_annot_arg_incr: + forall e a ty e' te, type_annot_arg e a ty = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + unfold type_annot_arg; intros; destruct a; eauto with ty. +Qed. + +Lemma type_annot_args_incr: + forall a ty e e' te, type_annot_args e a ty = OK e' -> S.satisf te e' -> S.satisf te e. +Proof. + induction a; destruct ty; simpl; intros; try discriminate. + inv H; auto. + monadInv H. eapply type_annot_arg_incr; eauto. +Qed. + +Hint Resolve type_annot_args_incr: ty. + +Lemma type_annot_arg_sound: + forall e a ty e' te, + type_annot_arg e a ty = OK e' -> S.satisf te e' -> type_of_annot_arg te a = ty. +Proof. + intros. destruct a; simpl in *; try (symmetry; eapply type_expect_sound; eassumption). + eapply S.set_sound; eauto. +Qed. + +Lemma type_annot_args_sound: + forall al tyl e e' te, + type_annot_args e al tyl = OK e' -> S.satisf te e' -> List.map (type_of_annot_arg te) al = tyl. +Proof. + induction al as [|a al]; destruct tyl as [|ty tyl]; simpl; intros; try discriminate. +- auto. +- monadInv H. f_equal. + eapply type_annot_arg_sound; eauto with ty. + eauto. +Qed. + Lemma type_instr_incr: forall e i e' te, type_instr e i = OK e' -> S.satisf te e' -> S.satisf te e. @@ -403,6 +500,10 @@ Proof. eapply S.set_list_sound; eauto with ty. eapply S.set_sound; eauto with ty. eauto with ty. +- (* annot *) + constructor. + eapply type_annot_args_sound; eauto. + eauto with ty. - (* cond *) constructor. eapply S.set_list_sound; eauto with ty. @@ -483,6 +584,33 @@ Proof. destruct H as [i EQ]; rewrite EQ; auto. Qed. +Lemma type_expect_complete: + forall e ty, type_expect e ty ty = OK e. +Proof. + unfold type_expect; intros. rewrite dec_eq_true; auto. +Qed. + +Lemma type_annot_arg_complete: + forall te a e, + S.satisf te e -> + exists e', type_annot_arg e a (type_of_annot_arg te a) = OK e' /\ S.satisf te e'. +Proof. + intros. destruct a; simpl; try (exists e; split; [apply type_expect_complete|assumption]). + apply S.set_complete; auto. +Qed. + +Lemma type_annot_args_complete: + forall te al e, + S.satisf te e -> + exists e', type_annot_args e al (List.map (type_of_annot_arg te) al) = OK e' /\ S.satisf te e'. +Proof. + induction al; simpl; intros. +- exists e; auto. +- destruct (type_annot_arg_complete te a e) as (e1 & A & B); auto. + destruct (IHal e1) as (e2 & C & D); auto. + exists e2; split; auto. rewrite A. auto. +Qed. + Lemma type_instr_complete: forall te e i, S.satisf te e -> @@ -539,6 +667,10 @@ Proof. exists e2; split; auto. rewrite check_successor_complete by auto; simpl. rewrite A; simpl; rewrite C; auto. +- (* annot *) + exploit type_annot_args_complete; eauto. intros [e1 [A B]]. + exists e1; split; auto. rewrite check_successor_complete by auto. + simpl; rewrite <- H0; eauto. - (* cond *) exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. exists e1; split; auto. @@ -782,6 +914,8 @@ Proof. inv WTI. rewrite <- H7. apply wt_regset_list. auto. (* Ibuiltin *) econstructor; eauto. eapply wt_exec_Ibuiltin; eauto. + (* Iannot *) + econstructor; eauto. (* Icond *) econstructor; eauto. (* Ijumptable *) diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 687cbbd3..3a7f5d99 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -114,6 +114,24 @@ let xparmove srcs dsts k = | [src], [dst] -> move src dst k | _, _ -> Xparmove(srcs, dsts, new_temp Tint, new_temp Tfloat) :: k +let rec convert_annot_arg tyenv = function + | AA_base r -> + begin match tyenv r with + | Tlong -> AA_longofwords(AA_base(V(r, Tint)), + AA_base(V(twin_reg r, Tint))) + | ty -> AA_base(V(r, ty)) + end + | AA_int n -> AA_int n + | AA_long n -> AA_long n + | AA_float n -> AA_float n + | AA_single n -> AA_single n + | AA_loadstack(chunk, ofs) -> AA_loadstack(chunk, ofs) + | AA_addrstack(ofs) -> AA_addrstack(ofs) + | AA_loadglobal(chunk, id, ofs) -> AA_loadglobal(chunk, id, ofs) + | AA_addrglobal(id, ofs) -> AA_addrglobal(id, ofs) + | AA_longofwords(hi, lo) -> + AA_longofwords(convert_annot_arg tyenv hi, convert_annot_arg tyenv lo) + (* Return the XTL basic block corresponding to the given RTL instruction. Move and parallel move instructions are introduced to honor calling conventions and register constraints on some operations. @@ -192,6 +210,8 @@ let block_of_RTL_instr funsig tyenv = function let args2 = constrain_regs args1 cargs and res2 = constrain_regs res1 cres in movelist args1 args2 (Xbuiltin(ef, args2, res2) :: movelist res2 res1 [Xbranch s]) + | RTL.Iannot(ef, args, s) -> + [Xannot(ef, List.map (convert_annot_arg tyenv) args); Xbranch s] | RTL.Icond(cond, args, s1, s2) -> [Xcond(cond, vregs tyenv args, s1, s2)] | RTL.Ijumptable(arg, tbl) -> @@ -231,6 +251,11 @@ let vset_removelist vl after = List.fold_right VSet.remove vl after let vset_addlist vl after = List.fold_right VSet.add vl after let vset_addros vos after = match vos with Coq_inl v -> VSet.add v after | Coq_inr id -> after +let rec vset_addannot a after = + match a with + | AA_base v -> VSet.add v after + | AA_longofwords(hi, lo) -> vset_addannot hi (vset_addannot lo after) + | _ -> after let live_before instr after = match instr with @@ -256,6 +281,8 @@ let live_before instr after = vset_addlist args (vset_addros ros VSet.empty) | Xbuiltin(ef, args, res) -> vset_addlist args (vset_removelist res after) + | Xannot(ef, args) -> + List.fold_right vset_addannot args after | Xbranch s -> after | Xcond(cond, args, s1, s2) -> @@ -431,16 +458,14 @@ let spill_costs f = | EF_vstore _ | EF_vstore_global _ | EF_memcpy _ -> (* result is not used but should not be spilled *) charge_list 10 1 args; charge_list max_int 0 res - | EF_annot _ -> - (* arguments are not actually used, so don't charge; - result is never used but should not be spilled *) - charge_list max_int 0 res | EF_annot_val _ -> (* like a move *) charge_list 1 1 args; charge_list 1 1 res | _ -> charge_list 10 1 args; charge_list 10 1 res end + | Xannot(ef, args) -> + () | Xbranch _ -> () | Xcond(cond, args, _, _) -> charge_list 10 1 args @@ -556,6 +581,8 @@ let add_interfs_instr g instr live = | EF_annot_val _, [arg], [res] -> IRC.add_pref g arg res (* like a move *) | _ -> () end + | Xannot(ef, args) -> + () | Xbranch s -> () | Xcond(cond, args, s1, s2) -> @@ -631,10 +658,9 @@ let tospill_instr alloc instr ts = | Xtailcall(sg, vos, args) -> addros_tospill alloc vos ts | Xbuiltin(ef, args, res) -> - begin match ef with - | EF_annot _ -> ts - | _ -> addlist_tospill alloc args (addlist_tospill alloc res ts) - end + addlist_tospill alloc args (addlist_tospill alloc res ts) + | Xannot(ef, args) -> + ts | Xbranch s -> ts | Xcond(cond, args, s1, s2) -> @@ -794,14 +820,11 @@ let spill_instr tospill eqs instr = | Xtailcall(sg, Coq_inr id, args) -> ([instr], []) | Xbuiltin(ef, args, res) -> - begin match ef with - | EF_annot _ -> - ([instr], eqs) - | _ -> - let (args', c1, eqs1) = reload_vars tospill eqs args in - let (res', c2, eqs2) = save_vars tospill eqs1 res in - (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2) - end + let (args', c1, eqs1) = reload_vars tospill eqs args in + let (res', c2, eqs2) = save_vars tospill eqs1 res in + (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2) + | Xannot(ef, args) -> + ([instr], eqs) | Xbranch s -> ([instr], eqs) | Xcond(cond, args, s1, s2) -> @@ -940,12 +963,9 @@ let transl_instr alloc instr k = | Xtailcall(sg, vos, args) -> LTL.Ltailcall(sg, mros_of alloc vos) :: [] | Xbuiltin(ef, args, res) -> - begin match ef with - | EF_annot _ -> - LTL.Lannot(ef, List.map alloc args) :: k - | _ -> - LTL.Lbuiltin(ef, mregs_of alloc args, mregs_of alloc res) :: k - end + LTL.Lbuiltin(ef, mregs_of alloc args, mregs_of alloc res) :: k + | Xannot(ef, args) -> + LTL.Lannot(ef, List.map (AST.map_annot_arg alloc) args) :: k | Xbranch s -> LTL.Lbranch s :: [] | Xcond(cond, args, s1, s2) -> diff --git a/backend/Renumber.v b/backend/Renumber.v index 0a2c2f12..634fe56a 100644 --- a/backend/Renumber.v +++ b/backend/Renumber.v @@ -48,6 +48,7 @@ Definition renum_instr (i: instruction) : instruction := | Icall sg ros args res s => Icall sg ros args res (renum_pc s) | Itailcall sg ros args => i | Ibuiltin ef args res s => Ibuiltin ef args res (renum_pc s) + | Iannot ef args s => Iannot ef args (renum_pc s) | Icond cond args s1 s2 => Icond cond args (renum_pc s1) (renum_pc s2) | Ijumptable arg tbl => Ijumptable arg (List.map renum_pc tbl) | Ireturn or => i diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 19c3b680..09faa131 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -201,6 +201,13 @@ Proof. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. eapply reach_succ; eauto. simpl; auto. +(* annot *) + econstructor; split. + 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. + constructor; auto. eapply reach_succ; eauto. simpl; auto. (* cond *) econstructor; split. eapply exec_Icond; eauto. diff --git a/backend/Selection.v b/backend/Selection.v index 11125856..ae9da0a7 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -203,6 +203,23 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind := end end. +(** Annotations *) + +Definition builtin_is_annot (ef: external_function) (optid: option ident) : bool := + match ef, optid with + | EF_annot _ _, None => true + | _, _ => false + end. + +Function sel_annot_arg (e: Cminor.expr) : AST.annot_arg expr := + match e with + | Cminor.Econst (Cminor.Oaddrsymbol id ofs) => AA_addrglobal id ofs + | Cminor.Econst (Cminor.Oaddrstack ofs) => AA_addrstack ofs + | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrsymbol id ofs)) => AA_loadglobal chunk id ofs + | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrstack ofs)) => AA_loadstack chunk ofs + | _ => annot_arg (sel_expr e) + end. + (** Conversion of Cminor [switch] statements to decision trees. *) Parameter compile_switch: Z -> nat -> table -> comptree. @@ -263,7 +280,9 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := | Call_builtin ef => Sbuiltin optid ef (sel_exprlist args) end) | Cminor.Sbuiltin optid ef args => - OK (Sbuiltin optid ef (sel_exprlist args)) + OK (if builtin_is_annot ef optid + then Sannot ef (List.map sel_annot_arg args) + else Sbuiltin optid ef (sel_exprlist args)) | Cminor.Stailcall sg fn args => OK (match classify_call ge fn with | Call_imm id => Stailcall sg (inr _ id) (sel_exprlist args) diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index bb9bd592..d7b1e675 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -135,7 +135,7 @@ Proof. inv H. econstructor; eauto. (* default *) econstructor. constructor. eauto. constructor. - simpl. inv H0. auto. auto. + simpl. inv H0. auto. Qed. Lemma eval_load: @@ -520,6 +520,14 @@ Proof. auto. Qed. +Lemma set_optvar_lessdef: + forall e1 e2 optid v1 v2, + env_lessdef e1 e2 -> Val.lessdef v1 v2 -> + env_lessdef (set_optvar optid v1 e1) (set_optvar optid v2 e2). +Proof. + unfold set_optvar; intros. destruct optid; auto. apply set_var_lessdef; auto. +Qed. + Lemma set_params_lessdef: forall il vl1 vl2, Val.lessdef_list vl1 vl2 -> @@ -590,6 +598,47 @@ Proof. exists (v1' :: vl'); split; auto. constructor; eauto. Qed. +Lemma sel_annot_arg_correct: + forall sp e e' m m', + env_lessdef e e' -> Mem.extends m m' -> + forall a v, + Cminor.eval_expr ge sp e m a v -> + exists v', + CminorSel.eval_annot_arg tge sp e' m' (sel_annot_arg a) v' + /\ Val.lessdef v v'. +Proof. + intros until v. functional induction (sel_annot_arg a); intros EV. +- inv EV. simpl in H2; inv H2. econstructor; split. constructor. + unfold Genv.symbol_address. rewrite symbols_preserved. auto. +- inv EV. simpl in H2; inv H2. econstructor; split. constructor. auto. +- inv EV. inv H3. exploit Mem.loadv_extends; eauto. intros (v' & A & B). + exists v'; split; auto. constructor. + replace (Genv.symbol_address tge id ofs) with vaddr; auto. + simpl in H2; inv H2. unfold Genv.symbol_address. rewrite symbols_preserved. auto. +- inv EV. inv H3. simpl in H2; inv H2. exploit Mem.loadv_extends; eauto. intros (v' & A & B). + exists v'; split; auto. constructor; auto. +- exploit sel_expr_correct; eauto. intros (v1 & A & B). + exists v1; split; auto. eapply eval_annot_arg; eauto. +Qed. + +Lemma sel_annot_args_correct: + forall sp e e' m m', + env_lessdef e e' -> Mem.extends m m' -> + forall al vl, + Cminor.eval_exprlist ge sp e m al vl -> + exists vl', + list_forall2 (CminorSel.eval_annot_arg tge sp e' m') + (List.map sel_annot_arg al) + vl' + /\ Val.lessdef_list vl vl'. +Proof. + induction 3; simpl. +- exists (@nil val); split; constructor. +- exploit sel_annot_arg_correct; eauto. intros (v1' & A & B). + destruct IHeval_exprlist as (vl' & C & D). + exists (v1' :: vl'); split; auto. constructor; auto. +Qed. + (** Semantic preservation for functions and statements. *) Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop := @@ -675,6 +724,8 @@ Proof. destruct (classify_call ge e); simpl; auto. (* tailcall *) destruct (classify_call ge e); simpl; auto. +(* builtin *) + destruct (builtin_is_annot e); simpl; auto. (* seq *) exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; @@ -776,14 +827,32 @@ Proof. econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. constructor; auto. apply call_cont_commut; auto. - (* Sbuiltin *) + destruct (builtin_is_annot ef optid) eqn:ISANNOT. ++ (* annotation *) + assert (X: exists text targs, ef = EF_annot text targs). + { destruct ef; try discriminate. econstructor; econstructor; eauto. } + destruct X as (text & targs & EQ). + assert (Y: optid = None). + { destruct ef; try discriminate. destruct optid; try discriminate. auto. } + exploit sel_annot_args_correct; eauto. + intros (vargs' & P & Q). + exploit external_call_mem_extends; eauto. + intros [vres' [m2 [A [B [C D]]]]]. + left; econstructor; split. + econstructor. + rewrite EQ; auto. + eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + rewrite Y. constructor; auto. ++ (* other builtin *) exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]]. exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - constructor; auto. - destruct optid; simpl; auto. apply set_var_lessdef; auto. + constructor; auto. apply set_optvar_lessdef; auto. - (* Seq *) left; econstructor; split. constructor. constructor; auto. constructor; auto. diff --git a/backend/Splitting.ml b/backend/Splitting.ml index 3530ba99..53600c98 100644 --- a/backend/Splitting.ml +++ b/backend/Splitting.ml @@ -163,6 +163,8 @@ let ren_instr f maps pc i = Itailcall(sg, ren_ros before ros, ren_regs before args) | Ibuiltin(ef, args, res, s) -> Ibuiltin(ef, ren_regs before args, ren_reg after res, s) + | Iannot(ef, args, s) -> + Iannot(ef, List.map (AST.map_annot_arg (ren_reg before)) args, s) | Icond(cond, args, s1, s2) -> Icond(cond, ren_regs before args, s1, s2) | Ijumptable(arg, tbl) -> diff --git a/backend/Stacking.v b/backend/Stacking.v index 4ee43bb1..c17dc038 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -130,14 +130,26 @@ Definition transl_addr (fe: frame_env) (addr: addressing) := (** Translation of an annotation argument. *) -Definition transl_annot_param (fe: frame_env) (l: loc) : annot_param := - match l with - | R r => APreg r - | S Local ofs ty => APstack (chunk_of_type ty) (offset_of_index fe (FI_local ofs ty)) - | S _ _ _ => APstack Mint32 (-1) (**r never happens *) +Fixpoint transl_annot_arg (fe: frame_env) (a: annot_arg loc) : annot_arg mreg := + match a with + | AA_base (R r) => AA_base r + | AA_base (S Local ofs ty) => + AA_loadstack (chunk_of_type ty) (Int.repr (offset_of_index fe (FI_local ofs ty))) + | AA_base (S _ _ __) => AA_int Int.zero (**r never happens *) + | AA_int n => AA_int n + | AA_long n => AA_long n + | AA_float n => AA_float n + | AA_single n => AA_single n + | AA_loadstack chunk ofs => + AA_loadstack chunk (Int.add ofs (Int.repr fe.(fe_stack_data))) + | AA_addrstack ofs => + AA_addrstack (Int.add ofs (Int.repr fe.(fe_stack_data))) + | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs + | AA_addrglobal id ofs => AA_addrglobal id ofs + | AA_longofwords hi lo => + AA_longofwords (transl_annot_arg fe hi) (transl_annot_arg fe lo) end. - (** Translation of a Linear instruction. Prepends the corresponding Mach instructions to the given list of instructions. [Lgetstack] and [Lsetstack] moves between registers and stack slots @@ -182,7 +194,7 @@ Definition transl_instr | Lbuiltin ef args dst => Mbuiltin ef args dst :: k | Lannot ef args => - Mannot ef (map (transl_annot_param fe) args) :: k + Mannot ef (map (transl_annot_arg fe) args) :: k | Llabel lbl => Mlabel lbl :: k | Lgoto lbl => diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index e3e3a0d0..f4a1935f 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -2382,6 +2382,8 @@ Section ANNOT_ARGUMENTS. Variable f: Linear.function. Let b := function_bounds f. Let fe := make_env b. +Variable tf: Mach.function. +Hypothesis TRANSF_F: transf_function f = OK tf. Variable j: meminj. Variables m m': mem. Variables ls ls0: locset. @@ -2390,39 +2392,67 @@ Variables sp sp': block. Variables parent retaddr: val. Hypothesis AGR: agree_regs j ls rs. Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent retaddr. - -Lemma transl_annot_param_correct: - forall l, - loc_valid f l = true -> - match l with S sl ofs ty => slot_within_bounds b sl ofs ty | _ => True end -> - exists v, annot_arg rs m' (Vptr sp' Int.zero) (transl_annot_param fe l) v - /\ val_inject j (ls l) v. -Proof. - intros. destruct l; simpl in H. -(* reg *) - exists (rs r); split. constructor. auto. -(* stack *) - destruct sl; try discriminate. - exploit agree_locals; eauto. intros [v [A B]]. inv A. - exists v; split. constructor. rewrite Zplus_0_l. auto. auto. -Qed. - -Lemma transl_annot_params_correct: - forall ll, - forallb (loc_valid f) ll = true -> - (forall sl ofs ty, In (S sl ofs ty) ll -> slot_within_bounds b sl ofs ty) -> - exists vl, - annot_arguments rs m' (Vptr sp' Int.zero) (map (transl_annot_param fe) ll) vl - /\ val_list_inject j (map ls ll) vl. -Proof. - induction ll; simpl; intros. - exists (@nil val); split; constructor. - InvBooleans. - exploit (transl_annot_param_correct a). auto. destruct a; auto. - intros [v1 [A B]]. - exploit IHll. auto. auto. - intros [vl [C D]]. - exists (v1 :: vl); split; constructor; auto. +Hypothesis MINJ: Mem.inject j m m'. +Hypothesis GINJ: meminj_preserves_globals ge j. + +Lemma transl_annot_arg_correct: + forall a v, + eval_annot_arg ge ls (Vptr sp Int.zero) m a v -> + (forall l, In l (params_of_annot_arg a) -> loc_valid f l = true) -> + (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_arg a) -> slot_within_bounds b sl ofs ty) -> + exists v', + eval_annot_arg ge rs (Vptr sp' Int.zero) m' (transl_annot_arg fe a) v' + /\ val_inject j v v'. +Proof. +Local Opaque fe offset_of_index. + induction 1; simpl; intros VALID BOUNDS. +- assert (loc_valid f x = true) by auto. + destruct x as [r | [] ofs ty]; try discriminate. + + exists (rs r); auto with aarg. + + exploit agree_locals; eauto. intros [v [A B]]. inv A. + exists v; split; auto. constructor. simpl. rewrite Int.add_zero_l. +Local Transparent fe. + unfold fe, b. erewrite offset_of_index_no_overflow by eauto. exact H1. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- simpl in H. exploit Mem.load_inject; eauto. eapply agree_inj; eauto. + intros (v' & A & B). exists v'; split; auto. constructor. + unfold Mem.loadv, Val.add. rewrite <- Int.add_assoc. + unfold fe, b; erewrite shifted_stack_offset_no_overflow; eauto. + eapply agree_bounds; eauto. eapply Mem.valid_access_perm. eapply Mem.load_valid_access; eauto. +- econstructor; split; eauto with aarg. + unfold Val.add. rewrite ! Int.add_zero_l. econstructor. eapply agree_inj; eauto. auto. +- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)). + { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + destruct (Genv.find_symbol ge id) eqn:FS; auto. + econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto. } + exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; auto with aarg. +- econstructor; split; eauto with aarg. + unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + destruct (Genv.find_symbol ge id) eqn:FS; auto. + econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto. +- destruct IHeval_annot_arg1 as (v1 & A1 & B1); auto using in_or_app. + destruct IHeval_annot_arg2 as (v2 & A2 & B2); auto using in_or_app. + exists (Val.longofwords v1 v2); split; auto with aarg. + apply val_longofwords_inject; auto. +Qed. + +Lemma transl_annot_args_correct: + forall al vl, + eval_annot_args ge ls (Vptr sp Int.zero) m al vl -> + (forall l, In l (params_of_annot_args al) -> loc_valid f l = true) -> + (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args al) -> slot_within_bounds b sl ofs ty) -> + exists vl', + eval_annot_args ge rs (Vptr sp' Int.zero) m' (List.map (transl_annot_arg fe) al) vl' + /\ val_list_inject j vl vl'. +Proof. + induction 1; simpl; intros VALID BOUNDS. +- exists (@nil val); split; constructor. +- exploit transl_annot_arg_correct; eauto using in_or_app. intros (v1' & A & B). + exploit IHlist_forall2; eauto using in_or_app. intros (vl' & C & D). + exists (v1'::vl'); split; constructor; auto. Qed. End ANNOT_ARGUMENTS. @@ -2705,25 +2735,28 @@ Proof. eapply agree_valid_mach; eauto. - (* Lannot *) - exploit transl_annot_params_correct; eauto. eapply wt_state_annot; eauto. + exploit transl_annot_args_correct; eauto. + eapply match_stacks_preserves_globals; eauto. + rewrite <- forallb_forall. eapply wt_state_annot; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_inject'; eauto. + exploit external_call_mem_inject; eauto. eapply match_stacks_preserves_globals; eauto. intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]]. econstructor; split. - apply plus_one. econstructor; eauto. - eapply external_call_symbols_preserved'; eauto. + apply plus_one. econstructor; 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. econstructor; eauto with coqlib. - inv H; inv A. eapply match_stack_change_extcall; eauto. + eapply match_stack_change_extcall; eauto. apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. apply Plt_Ple. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto. eapply agree_regs_inject_incr; eauto. eapply agree_frame_inject_incr; eauto. apply agree_frame_extcall_invariant with m m'0; auto. - eapply external_call_valid_block'; eauto. - intros. inv H; eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto. - eapply external_call_valid_block'; eauto. + eapply external_call_valid_block; eauto. + intros. eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto. + eapply external_call_valid_block; eauto. eapply agree_valid_mach; eauto. - (* Llabel *) diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 5ee7ccc1..bd9b227f 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -513,6 +513,19 @@ Proof. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. apply regset_set; auto. +(* annot *) + TransfInstr. + exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. + intros (vargs' & P & Q). + exploit external_call_mem_extends; eauto. + intros [v' [m'1 [A [B [C D]]]]]. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' rs' m'1); split. + 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. + econstructor; eauto. + (* cond *) TransfInstr. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index e6588938..52318ede 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -344,8 +344,9 @@ Proof. econstructor; eauto. (* Lannot *) left; simpl; econstructor; split. - eapply exec_Lannot; eauto. - eapply external_call_symbols_preserved'; eauto. + eapply exec_Lannot; 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. econstructor; eauto. diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v index 55a093a4..400c19d9 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -60,6 +60,7 @@ Definition ref_instruction (i: instruction) : list ident := | Itailcall _ (inl r) _ => nil | Itailcall _ (inr id) _ => id :: nil | Ibuiltin ef _ _ _ => globals_external ef + | Iannot _ args _ => globals_of_annot_args args | Icond cond _ _ _ => nil | Ijumptable _ _ => nil | Ireturn _ => nil diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index fbf43866..90d7f270 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -741,6 +741,64 @@ Proof. auto. Qed. +Lemma eval_annot_arg_inject: + forall rs sp m j rs' sp' m' a v, + eval_annot_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v -> + j sp = Some(sp', 0) -> + meminj_preserves_globals j -> + regset_inject j rs rs' -> + Mem.inject j m m' -> + (forall id, In id (globals_of_annot_arg a) -> kept id) -> + exists v', + eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' a v' + /\ val_inject j v v'. +Proof. + induction 1; intros SP GL RS MI K; simpl in K. +- exists rs'#x; split; auto. constructor. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r. + intros (v' & A & B). exists v'; auto with aarg. +- econstructor; split; eauto with aarg. simpl. econstructor; eauto. rewrite Int.add_zero; auto. +- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)). + { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. + exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. + econstructor; eauto. rewrite Int.add_zero; auto. } + exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; auto with aarg. +- econstructor; split; eauto with aarg. + unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. + destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto. + exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. + econstructor; eauto. rewrite Int.add_zero; auto. +- destruct IHeval_annot_arg1 as (v1' & A1 & B1); eauto using in_or_app. + destruct IHeval_annot_arg2 as (v2' & A2 & B2); eauto using in_or_app. + exists (Val.longofwords v1' v2'); split; auto with aarg. + apply val_longofwords_inject; auto. +Qed. + +Lemma eval_annot_args_inject: + forall rs sp m j rs' sp' m' al vl, + eval_annot_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl -> + j sp = Some(sp', 0) -> + meminj_preserves_globals j -> + regset_inject j rs rs' -> + Mem.inject j m m' -> + (forall id, In id (globals_of_annot_args al) -> kept id) -> + exists vl', + eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' al vl' + /\ val_list_inject j vl vl'. +Proof. + induction 1; intros. +- exists (@nil val); split; constructor. +- simpl in H5. + exploit eval_annot_arg_inject; eauto using in_or_app. intros (v1' & A & B). + destruct IHlist_forall2 as (vl' & C & D); eauto using in_or_app. + exists (v1' :: vl'); split; constructor; auto. +Qed. + Theorem step_simulation: forall S1 t S2, step ge S1 t S2 -> forall S1' (MS: match_states S1 S1'), @@ -845,6 +903,25 @@ Proof. unfold Mem.valid_block in *; xomega. apply set_reg_inject; auto. apply regset_inject_incr with j; auto. +- (* annot *) + exploit eval_annot_args_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + intros. apply KEPT. red. econstructor; econstructor; eauto. + intros (vargs' & P & Q). + exploit external_call_inject; eauto. + eapply match_stacks_preserves_globals; eauto. + destruct ef; contradiction. + intros (j' & tv & tm' & A & B & C & D & E & F & G). + econstructor; split. + eapply exec_Iannot; eauto. + eapply match_states_regular with (j := j'); eauto. + apply match_stacks_incr with j; auto. + intros. exploit G; eauto. intros [U V]. + assert (Mem.valid_block m sp0) by (eapply Mem.valid_block_inject_1; eauto). + assert (Mem.valid_block tm tsp) by (eapply Mem.valid_block_inject_2; eauto). + unfold Mem.valid_block in *; xomega. + apply regset_inject_incr with j; auto. + - (* cond *) assert (C: eval_condition cond trs##args tm = Some b). { eapply eval_condition_inject; eauto. apply regs_inject; auto. } diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 4249a8da..8720ce50 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -55,7 +55,6 @@ Inductive builtin_kind : Type := | Builtin_vload (chunk: memory_chunk) (aaddr: aval) | Builtin_vstore (chunk: memory_chunk) (aaddr av: aval) | Builtin_memcpy (sz al: Z) (adst asrc: aval) - | Builtin_annot | Builtin_annot_val (av: aval) | Builtin_default. @@ -66,7 +65,6 @@ Definition classify_builtin (ef: external_function) (args: list reg) (ae: aenv) | EF_vstore chunk, a1::a2::nil => Builtin_vstore chunk (areg ae a1) (areg ae a2) | EF_vstore_global chunk id ofs, a1::nil => Builtin_vstore chunk (Ptr (Gl id ofs)) (areg ae a1) | EF_memcpy sz al, a1::a2::nil => Builtin_memcpy sz al (areg ae a1) (areg ae a2) - | EF_annot _ _, _ => Builtin_annot | EF_annot_val _ _, a1::nil => Builtin_annot_val (areg ae a1) | _, _ => Builtin_default end. @@ -86,8 +84,6 @@ Definition transfer_builtin (ae: aenv) (am: amem) (rm: romem) (ef: external_func let p := loadbytes am rm (aptr_of_aval asrc) in let am' := storebytes am (aptr_of_aval adst) sz p in VA.State (AE.set res itop ae) am' - | Builtin_annot => - VA.State (AE.set res itop ae) am | Builtin_annot_val av => VA.State (AE.set res av ae) am | Builtin_default => @@ -115,6 +111,8 @@ Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) : VA.Bot | Some(Ibuiltin ef args res s) => transfer_builtin ae am rm ef args res + | Some(Iannot ef args s) => + VA.State ae am | Some(Icond cond args s1 s2) => VA.State ae am | Some(Ijumptable arg tbl) => @@ -306,7 +304,6 @@ Lemma classify_builtin_sound: exists dst, exists src, extcall_memcpy_sem sz al ge (dst::src::nil) m t res m' /\ vmatch bc dst adst /\ vmatch bc src asrc - | Builtin_annot => m' = m /\ res = Vundef | Builtin_annot_val av => m' = m /\ vmatch bc res av | Builtin_default => True end. @@ -329,8 +326,6 @@ Proof. - (* memcpy *) destruct args; auto. destruct args; auto. destruct args; auto. exists (e#p), (e#p0); eauto. -- (* annot *) - simpl in H1. inv H1. auto. - (* annot val *) destruct args; auto. destruct args; auto. simpl in H1. inv H1. eauto. @@ -1303,10 +1298,6 @@ Proof. intros. eapply loadbytes_sound; eauto. apply match_aptr_of_aval; auto. eapply romatch_storebytes; eauto. eapply sound_stack_storebytes; eauto. -+ (* annot *) - intros (A & B); subst. - eapply sound_succ_state; eauto. simpl; auto. - apply ematch_update; auto. constructor. + (* annot val *) intros (A & B); subst. eapply sound_succ_state; eauto. simpl; auto. @@ -1359,6 +1350,11 @@ Proof. rewrite C; auto. exact AA. +- (* annot *) + destruct ef; try contradiction. inv H2. + eapply sound_succ_state; eauto. simpl; auto. + unfold transfer; rewrite H; eauto. + - (* cond *) eapply sound_succ_state; eauto. simpl. destruct b; auto. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 92004a2f..ff3ccfa1 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -2121,12 +2121,14 @@ Proof. assert (IP: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vint i) (Vptr b ofs)) (cmp_different_blocks c)). { - intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. + intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))). + apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } assert (PI: forall i b ofs, cmatch (Val.cmpu_bool valid c (Vptr b ofs) (Vint i)) (cmp_different_blocks c)). { - intros. simpl. destruct (Int.eq i Int.zero). apply cmp_different_blocks_sound. apply cmp_different_blocks_none. + intros. simpl. destruct (Int.eq i Int.zero && (valid b (Int.unsigned ofs) || valid b (Int.unsigned ofs - 1))). + apply cmp_different_blocks_sound. apply cmp_different_blocks_none. } unfold cmpu_bool; inversion H; subst; inversion H0; subst; auto using cmatch_top, cmp_different_blocks_none, pcmp_none, diff --git a/backend/XTL.ml b/backend/XTL.ml index 9cb8e0a1..0e5ce0c4 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -35,6 +35,7 @@ type instruction = | Xcall of signature * (var, ident) sum * var list * var list | Xtailcall of signature * (var, ident) sum * var list | Xbuiltin of external_function * var list * var list + | Xannot of external_function * var annot_arg list | Xbranch of node | Xcond of condition * var list * node * node | Xjumptable of var * node list @@ -124,6 +125,12 @@ let rec set_vars_type vl tyl = let unify_var_type v1 v2 = if typeof v1 <> typeof v2 then raise Type_error +let rec type_annot_arg a ty = + match a with + | AA_base v -> set_var_type v ty + | AA_longofwords(a1, a2) -> type_annot_arg a1 Tint; type_annot_arg a2 Tint + | _ -> () + let type_instr = function | Xmove(src, dst) | Xspill(src, dst) | Xreload(src, dst) -> unify_var_type src dst @@ -153,6 +160,11 @@ let type_instr = function let sg = ef_sig ef in set_vars_type args sg.sig_args; set_vars_type res (Events.proj_sig_res' sg) + | Xannot(ef, args) -> + let sg = ef_sig ef in + if List.length args = List.length sg.sig_args + then List.iter2 type_annot_arg args sg.sig_args + else raise Type_error | Xbranch s -> () | Xcond(cond, args, s1, s2) -> diff --git a/backend/XTL.mli b/backend/XTL.mli index 75a3d657..9794565c 100644 --- a/backend/XTL.mli +++ b/backend/XTL.mli @@ -36,6 +36,7 @@ type instruction = | Xcall of signature * (var, ident) sum * var list * var list | Xtailcall of signature * (var, ident) sum * var list | Xbuiltin of external_function * var list * var list + | Xannot of external_function * var annot_arg list | Xbranch of node | Xcond of condition * var list * node * node | Xjumptable of var * node list diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4cb4ded6..fd10efb4 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -737,8 +737,7 @@ let rec convertExpr env e = | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypArgs env [] args1 in Ebuiltin( - EF_annot(intern_string txt, - List.map (fun t -> AA_arg t) (typlist_of_typelist targs1)), + EF_annot(intern_string txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index ed67286f..7c00ab47 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) := @@ -785,7 +785,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eunop op r1 ty => match is_val r1 with | Some(v1, ty1) => - do v <- sem_unary_operation op v1 ty1; + do v <- sem_unary_operation op v1 ty1 m; topred (Rred "red_unop" (Eval v ty) m E0) | None => incontext (fun x => Eunop op x ty) (step_expr RV r1 m) @@ -810,7 +810,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eseqand r1 r2 ty => match is_val r1 with | Some(v1, ty1) => - do b <- bool_val v1 ty1; + do b <- bool_val v1 ty1 m; if b then topred (Rred "red_seqand_true" (Eparen r2 type_bool ty) m E0) else topred (Rred "red_seqand_false" (Eval (Vint Int.zero) ty) m E0) | None => @@ -819,7 +819,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eseqor r1 r2 ty => match is_val r1 with | Some(v1, ty1) => - do b <- bool_val v1 ty1; + do b <- bool_val v1 ty1 m; if b then topred (Rred "red_seqor_true" (Eval (Vint Int.one) ty) m E0) else topred (Rred "red_seqor_false" (Eparen r2 type_bool ty) m E0) | None => @@ -828,7 +828,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Econdition r1 r2 r3 ty => match is_val r1 with | Some(v1, ty1) => - do b <- bool_val v1 ty1; + do b <- bool_val v1 ty1 m; topred (Rred "red_condition" (Eparen (if b then r2 else r3) ty ty) m E0) | None => incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) @@ -987,17 +987,17 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Evalof (Eloc b ofs ty') ty => ty' = ty /\ exists t, exists v, exists w', deref_loc ge ty m b ofs t v /\ possible_trace w t w' | Eunop op (Eval v1 ty1) ty => - exists v, sem_unary_operation op v1 ty1 = Some v + exists v, sem_unary_operation op v1 ty1 m = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => exists v, sem_cast v1 ty1 ty = Some v | Eseqand (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Econdition (Eval v1 ty1) r1 r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => exists v, exists m', exists t, exists w', ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w' @@ -1409,7 +1409,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* unop *) destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (sem_unary_operation op v ty') as [v'|] eqn:?... + destruct (sem_unary_operation op v ty' m) as [v'|] eqn:?... apply topred_ok; auto. split. apply red_unop; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1433,7 +1433,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* seqand *) destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (bool_val v ty') as [v'|] eqn:?... destruct v'. + destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'. apply topred_ok; auto. split. eapply red_seqand_true; eauto. exists w; constructor. apply topred_ok; auto. split. eapply red_seqand_false; eauto. exists w; constructor. (* depth *) @@ -1441,7 +1441,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* seqor *) destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (bool_val v ty') as [v'|] eqn:?... destruct v'. + destruct (bool_val v ty' m) as [v'|] eqn:?... destruct v'. apply topred_ok; auto. split. eapply red_seqor_true; eauto. exists w; constructor. apply topred_ok; auto. split. eapply red_seqor_false; eauto. exists w; constructor. (* depth *) @@ -1449,7 +1449,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* condition *) destruct (is_val a1) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (bool_val v ty') as [v'|] eqn:?... + destruct (bool_val v ty' m) as [v'|] eqn:?... apply topred_ok; auto. split. eapply red_condition; eauto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1973,20 +1973,20 @@ Definition do_step (w: world) (s: state) : list transition := match k with | Kdo k => ret "step_do_2" (State f Sskip k e m ) | Kifthenelse s1 s2 k => - do b <- bool_val v ty; + do b <- bool_val v ty m; ret "step_ifthenelse_2" (State f (if b then s1 else s2) k e m) | Kwhile1 x s k => - do b <- bool_val v ty; + do b <- bool_val v ty m; if b then ret "step_while_true" (State f s (Kwhile2 x s k) e m) else ret "step_while_false" (State f Sskip k e m) | Kdowhile2 x s k => - do b <- bool_val v ty; + do b <- bool_val v ty m; if b then ret "step_dowhile_true" (State f (Sdowhile x s) k e m) else ret "step_dowhile_false" (State f Sskip k e m) | Kfor2 a2 a3 s k => - do b <- bool_val v ty; + do b <- bool_val v ty m; if b then ret "step_for_true" (State f s (Kfor3 a2 a3 s k) e m) else ret "step_for_false" (State f Sskip k e m) diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 7a45b453..77511b2c 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -403,7 +403,7 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr (Eaddrof a ty) (Vptr loc ofs) | eval_Eunop: forall op a ty v1 v, eval_expr a v1 -> - sem_unary_operation op v1 (typeof a) = Some v -> + sem_unary_operation op v1 (typeof a) m = Some v -> eval_expr (Eunop op a ty) v | eval_Ebinop: forall op a1 a2 ty v1 v2 v, eval_expr a1 v1 -> @@ -620,7 +620,7 @@ Inductive step: state -> trace -> state -> Prop := | step_ifthenelse: forall f a s1 s2 k e le m v1 b, eval_expr e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> step (State f (Sifthenelse a s1 s2) k e le m) E0 (State f (if b then s1 else s2) k e le m) diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index 5b092db7..ac8931e5 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -115,7 +115,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> t1 le1 m1 out | exec_Sifthenelse: forall e le m a s1 s2 v1 b t le' m' out, eval_expr ge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> exec_stmt e le m (if b then s1 else s2) t le' m' out -> exec_stmt e le m (Sifthenelse a s1 s2) t le' m' out @@ -204,7 +204,7 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro execinf_stmt e le m (Ssequence s1 s2) (t1 *** t2) | execinf_Sifthenelse: forall e le m a s1 s2 v1 b t, eval_expr ge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> execinf_stmt e le m (if b then s1 else s2) t -> execinf_stmt e le m (Sifthenelse a s1 s2) t | execinf_Sloop_body1: forall e le m s1 s2 t, diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 4e572277..2a5d17bc 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -273,7 +273,6 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := | cast_case_p2bool => match v with | Vint i => Some (Vint (cast_int_int IBool Signed i)) - | Vptr _ _ => Some (Vint Int.one) | _ => None end | cast_case_l2l => @@ -371,7 +370,7 @@ Definition classify_bool (ty: type) : classify_bool_cases := considered as true. The integer zero (which also represents the null pointer) and the float 0.0 are false. *) -Definition bool_val (v: val) (t: type) : option bool := +Definition bool_val (v: val) (t: type) (m: mem) : option bool := match classify_bool t with | bool_case_i => match v with @@ -391,7 +390,7 @@ Definition bool_val (v: val) (t: type) : option bool := | bool_case_p => match v with | Vint n => Some (negb (Int.eq n Int.zero)) - | Vptr b ofs => Some true + | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some true else None | _ => None end | bool_case_l => @@ -406,7 +405,7 @@ Definition bool_val (v: val) (t: type) : option bool := (** *** Boolean negation *) -Definition sem_notbool (v: val) (ty: type) : option val := +Definition sem_notbool (v: val) (ty: type) (m: mem): option val := match classify_bool ty with | bool_case_i => match v with @@ -426,7 +425,7 @@ Definition sem_notbool (v: val) (ty: type) : option val := | bool_case_p => match v with | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) - | Vptr _ _ => Some Vfalse + | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vfalse else None | _ => None end | bool_case_l => @@ -973,9 +972,9 @@ Definition sem_switch_arg (v: val) (ty: type): option Z := (** * Combined semantics of unary and binary operators *) Definition sem_unary_operation - (op: unary_operation) (v: val) (ty: type): option val := + (op: unary_operation) (v: val) (ty: type) (m: mem): option val := match op with - | Onotbool => sem_notbool v ty + | Onotbool => sem_notbool v ty m | Onotint => sem_notint v ty | Oneg => sem_neg v ty | Oabsfloat => sem_absfloat v ty @@ -1091,15 +1090,17 @@ Proof. - econstructor; eauto. Qed. -Lemma sem_unary_operation_inject: +Lemma sem_unary_operation_inj: forall op v1 ty v tv1, - sem_unary_operation op v1 ty = Some v -> + sem_unary_operation op v1 ty m = Some v -> val_inject f v1 tv1 -> - exists tv, sem_unary_operation op tv1 ty = Some tv /\ val_inject f v tv. + exists tv, sem_unary_operation op tv1 ty m' = Some tv /\ val_inject f v tv. Proof. unfold sem_unary_operation; intros. destruct op. (* notbool *) unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject. + destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H2. + erewrite weak_valid_pointer_inj by eauto. TrivialInject. (* notint *) unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject. (* neg *) @@ -1265,18 +1266,31 @@ Proof. - eapply sem_cmp_inj; eauto. Qed. -Lemma bool_val_inject: +Lemma bool_val_inj: forall v ty b tv, - bool_val v ty = Some b -> + bool_val v ty m = Some b -> val_inject f v tv -> - bool_val tv ty = Some b. + bool_val tv ty m' = Some b. Proof. unfold bool_val; intros. - destruct (classify_bool ty); inv H0; congruence. + destruct (classify_bool ty); inv H0; try congruence. + destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VP; inv H. + erewrite weak_valid_pointer_inj by eauto. auto. Qed. End GENERIC_INJECTION. +Lemma sem_unary_operation_inject: + forall f m m' op v1 ty1 v tv1, + sem_unary_operation op v1 ty1 m = Some v -> + val_inject f v1 tv1 -> + Mem.inject f m m' -> + exists tv, sem_unary_operation op tv1 ty1 m' = Some tv /\ val_inject f v tv. +Proof. + intros. eapply sem_unary_operation_inj; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. +Qed. + Lemma sem_binary_operation_inject: forall f m m' cenv op v1 ty1 v2 ty2 v tv1 tv2, sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> @@ -1291,6 +1305,17 @@ Proof. intros; eapply Mem.different_pointers_inject; eauto. Qed. +Lemma bool_val_inject: + forall f m m' v ty b tv, + bool_val v ty m = Some b -> + val_inject f v tv -> + Mem.inject f m m' -> + bool_val tv ty m' = Some b. +Proof. + intros. eapply bool_val_inj; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. +Qed. + (** * Some properties of operator semantics *) (** This section collects some common-sense properties about the type @@ -1301,9 +1326,12 @@ Qed. (** Relation between Boolean value and casting to [_Bool] type. *) Lemma cast_bool_bool_val: - forall v t, - sem_cast v t (Tint IBool Signed noattr) = - match bool_val v t with None => None | Some b => Some(Val.of_bool b) end. + forall v t m, + match sem_cast v t (Tint IBool Signed noattr), bool_val v t m with + | Some v', Some b => v' = Val.of_bool b + | Some v', None => False + | None, _ => True + end. Proof. intros. assert (A: classify_bool t = @@ -1337,12 +1365,13 @@ Qed. (** Relation between Boolean value and Boolean negation. *) Lemma notbool_bool_val: - forall v t, - sem_notbool v t = - match bool_val v t with None => None | Some b => Some(Val.of_bool (negb b)) end. + forall v t m, + sem_notbool v t m = + match bool_val v t m with None => None | Some b => Some(Val.of_bool (negb b)) end. Proof. intros. unfold sem_notbool, bool_val. - destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto. + destruct (classify_bool t); auto; destruct v; auto; rewrite ? negb_involutive; auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. Qed. (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *) diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index fafbf29f..3e9017c9 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -241,7 +241,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Eaddrof (Eloc b ofs ty1) ty) m E0 (Eval (Vptr b ofs) ty) m | red_unop: forall op v1 ty1 ty m v, - sem_unary_operation op v1 ty1 = Some v -> + sem_unary_operation op v1 ty1 m = Some v -> rred (Eunop op (Eval v1 ty1) ty) m E0 (Eval v ty) m | red_binop: forall op v1 ty1 v2 ty2 ty m v, @@ -253,23 +253,23 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Ecast (Eval v1 ty1) ty) m E0 (Eval v ty) m | red_seqand_true: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some true -> + bool_val v1 ty1 m = Some true -> rred (Eseqand (Eval v1 ty1) r2 ty) m E0 (Eparen r2 type_bool ty) m | red_seqand_false: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some false -> + bool_val v1 ty1 m = Some false -> rred (Eseqand (Eval v1 ty1) r2 ty) m E0 (Eval (Vint Int.zero) ty) m | red_seqor_true: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some true -> + bool_val v1 ty1 m = Some true -> rred (Eseqor (Eval v1 ty1) r2 ty) m E0 (Eval (Vint Int.one) ty) m | red_seqor_false: forall v1 ty1 r2 ty m, - bool_val v1 ty1 = Some false -> + bool_val v1 ty1 m = Some false -> rred (Eseqor (Eval v1 ty1) r2 ty) m E0 (Eparen r2 type_bool ty) m | red_condition: forall v1 ty1 r1 r2 ty b m, - bool_val v1 ty1 = Some b -> + bool_val v1 ty1 m = Some b -> rred (Econdition (Eval v1 ty1) r1 r2 ty) m E0 (Eparen (if b then r1 else r2) ty ty) m | red_sizeof: forall ty1 ty m, @@ -633,7 +633,7 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Sifthenelse a s1 s2) k e m) E0 (ExprState f a (Kifthenelse s1 s2 k) e m) | step_ifthenelse_2: forall f v ty s1 s2 k e m b, - bool_val v ty = Some b -> + bool_val v ty m = Some b -> sstep (ExprState f (Eval v ty) (Kifthenelse s1 s2 k) e m) E0 (State f (if b then s1 else s2) k e m) @@ -641,11 +641,11 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Swhile x s) k e m) E0 (ExprState f x (Kwhile1 x s k) e m) | step_while_false: forall f v ty x s k e m, - bool_val v ty = Some false -> + bool_val v ty m = Some false -> sstep (ExprState f (Eval v ty) (Kwhile1 x s k) e m) E0 (State f Sskip k e m) | step_while_true: forall f v ty x s k e m , - bool_val v ty = Some true -> + bool_val v ty m = Some true -> sstep (ExprState f (Eval v ty) (Kwhile1 x s k) e m) E0 (State f s (Kwhile2 x s k) e m) | step_skip_or_continue_while: forall f s0 x s k e m, @@ -664,11 +664,11 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f s0 (Kdowhile1 x s k) e m) E0 (ExprState f x (Kdowhile2 x s k) e m) | step_dowhile_false: forall f v ty x s k e m, - bool_val v ty = Some false -> + bool_val v ty m = Some false -> sstep (ExprState f (Eval v ty) (Kdowhile2 x s k) e m) E0 (State f Sskip k e m) | step_dowhile_true: forall f v ty x s k e m, - bool_val v ty = Some true -> + bool_val v ty m = Some true -> sstep (ExprState f (Eval v ty) (Kdowhile2 x s k) e m) E0 (State f (Sdowhile x s) k e m) | step_break_dowhile: forall f a s k e m, @@ -683,11 +683,11 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Sfor Sskip a2 a3 s) k e m) E0 (ExprState f a2 (Kfor2 a2 a3 s k) e m) | step_for_false: forall f v ty a2 a3 s k e m, - bool_val v ty = Some false -> + bool_val v ty m = Some false -> sstep (ExprState f (Eval v ty) (Kfor2 a2 a3 s k) e m) E0 (State f Sskip k e m) | step_for_true: forall f v ty a2 a3 s k e m, - bool_val v ty = Some true -> + bool_val v ty m = Some true -> sstep (ExprState f (Eval v ty) (Kfor2 a2 a3 s k) e m) E0 (State f s (Kfor3 a2 a3 s k) e m) | step_skip_or_continue_for3: forall f x a2 a3 s k e m, diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 7f61c657..025d7b66 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -311,7 +311,7 @@ Qed. Lemma make_boolean_correct: forall e le m a v ty b, eval_expr ge e le m a v -> - bool_val v ty = Some b -> + bool_val v ty m = Some b -> exists vb, eval_expr ge e le m (make_boolean a ty) vb /\ Val.bool_of_val vb b. @@ -333,7 +333,10 @@ Proof. econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpu, Val.cmpu_bool. simpl. destruct (Int.eq i Int.zero); simpl; constructor. - exists Vtrue; split. econstructor; eauto with cshm. constructor. + econstructor; split. econstructor; eauto with cshm. simpl. eauto. + destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i)) eqn:V; inv H2. + unfold Val.cmpu, Val.cmpu_bool. simpl. + unfold Mem.weak_valid_pointer in V; rewrite V. constructor. (* long *) econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor. @@ -366,13 +369,16 @@ Qed. Lemma make_notbool_correct: forall a tya c va v e le m, - sem_notbool va tya = Some v -> + sem_notbool va tya m = Some v -> make_notbool a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1; destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:V; inv H0. + econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. + unfold Mem.weak_valid_pointer in V; rewrite V. auto. Qed. Lemma make_notint_correct: @@ -633,7 +639,7 @@ Qed. Lemma transl_unop_correct: forall op a tya c va v e le m, transl_unop op a tya = OK c -> - sem_unary_operation op va tya = Some v -> + sem_unary_operation op va tya m = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index 3b0eb84f..b082ea56 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -122,7 +122,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) | esr_unop: forall op r1 ty v1 v, eval_simple_rvalue r1 v1 -> - sem_unary_operation op v1 (typeof r1) = Some v -> + sem_unary_operation op v1 (typeof r1) m = Some v -> eval_simple_rvalue (Eunop op r1 ty) v | esr_binop: forall op r1 r2 ty v1 v2 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> @@ -249,33 +249,33 @@ Inductive estep: state -> trace -> state -> Prop := | step_seqand_true: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some true -> + bool_val v (typeof r1) m = Some true -> estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m) | step_seqand_false: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some false -> + bool_val v (typeof r1) m = Some false -> estep (ExprState f (C (Eseqand r1 r2 ty)) k e m) E0 (ExprState f (C (Eval (Vint Int.zero) ty)) k e m) | step_seqor_true: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some true -> + bool_val v (typeof r1) m = Some true -> estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) E0 (ExprState f (C (Eval (Vint Int.one) ty)) k e m) | step_seqor_false: forall f C r1 r2 ty k e m v, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some false -> + bool_val v (typeof r1) m = Some false -> estep (ExprState f (C (Eseqor r1 r2 ty)) k e m) E0 (ExprState f (C (Eparen r2 type_bool ty)) k e m) | step_condition: forall f C r1 r2 r3 ty k e m v b, leftcontext RV RV C -> eval_simple_rvalue e m r1 v -> - bool_val v (typeof r1) = Some b -> + bool_val v (typeof r1) m = Some b -> estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m) E0 (ExprState f (C (Eparen (if b then r2 else r3) ty ty)) k e m) @@ -536,17 +536,17 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Evalof (Eloc b ofs ty') ty => ty' = ty /\ exists t, exists v, deref_loc ge ty m b ofs t v | Eunop op (Eval v1 ty1) ty => - exists v, sem_unary_operation op v1 ty1 = Some v + exists v, sem_unary_operation op v1 ty1 m = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => exists v, sem_cast v1 ty1 ty = Some v | Eseqand (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Econdition (Eval v1 ty1) r1 r2 ty => - exists b, bool_val v1 ty1 = Some b + exists b, bool_val v1 ty1 m = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => exists v, exists m', exists t, ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' @@ -1695,27 +1695,27 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty) | eval_seqand_true: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> sem_cast v2 (typeof a2) type_bool = Some v -> eval_expr e m RV (Eseqand a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqand_false: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> eval_expr e m RV (Eseqand a1 a2 ty) t1 m' (Eval (Vint Int.zero) ty) | eval_seqor_false: forall e m a1 a2 ty t1 m' a1' v1 t2 m'' a2' v2 v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> sem_cast v2 (typeof a2) type_bool = Some v -> eval_expr e m RV (Eseqor a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqor_true: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> eval_expr e m RV (Eseqor a1 a2 ty) t1 m' (Eval (Vint Int.one) ty) | eval_condition: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a' v' b v, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some b -> + bool_val v1 (typeof a1) m' = Some b -> eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' -> sem_cast v' (typeof (if b then a2 else a3)) ty = Some v -> eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) @@ -1801,7 +1801,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := t1 m1 out | exec_Sifthenelse: forall e m a s1 s2 t1 m1 v1 t2 m2 b out, eval_expression e m a t1 m1 v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m1 = Some b -> exec_stmt e m1 (if b then s1 else s2) t2 m2 out -> exec_stmt e m (Sifthenelse a s1 s2) (t1**t2) m2 out @@ -1820,19 +1820,19 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := E0 m Out_continue | exec_Swhile_false: forall e m a s t m' v, eval_expression e m a t m' v -> - bool_val v (typeof a) = Some false -> + bool_val v (typeof a) m' = Some false -> exec_stmt e m (Swhile a s) t m' Out_normal | exec_Swhile_stop: forall e m a s t1 m1 v t2 m2 out' out, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out' -> out_break_or_return out' out -> exec_stmt e m (Swhile a s) (t1**t2) m2 out | exec_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3 m3 out, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 (Swhile a s) t3 m3 out -> @@ -1842,7 +1842,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some false -> + bool_val v (typeof a) m2 = Some false -> exec_stmt e m (Sdowhile a s) (t1 ** t2) m2 Out_normal | exec_Sdowhile_stop: forall e m s a t m1 out1 out, @@ -1854,7 +1854,7 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m2 = Some true -> exec_stmt e m2 (Sdowhile a s) t3 m3 out -> exec_stmt e m (Sdowhile a s) (t1 ** t2 ** t3) m3 out @@ -1865,19 +1865,19 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := (t1 ** t2) m2 out | exec_Sfor_false: forall e m s a2 a3 t m' v, eval_expression e m a2 t m' v -> - bool_val v (typeof a2) = Some false -> + bool_val v (typeof a2) m' = Some false -> exec_stmt e m (Sfor Sskip a2 a3 s) t m' Out_normal | exec_Sfor_stop: forall e m s a2 a3 t1 m1 v t2 m2 out1 out, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_break_or_return out1 out -> exec_stmt e m (Sfor Sskip a2 a3 s) (t1 ** t2) m2 out | exec_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4 m4 out, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 a3 t3 m3 Out_normal -> @@ -1952,7 +1952,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Eseqand a1 a2 ty) t1 | evalinf_seqand_2: forall e m a1 a2 ty t1 m' a1' v1 t2, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some true -> + bool_val v1 (typeof a1) m' = Some true -> evalinf_expr e m' RV a2 t2 -> evalinf_expr e m RV (Eseqand a1 a2 ty) (t1***t2) | evalinf_seqor: forall e m a1 a2 ty t1, @@ -1960,7 +1960,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Eseqor a1 a2 ty) t1 | evalinf_seqor_2: forall e m a1 a2 ty t1 m' a1' v1 t2, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some false -> + bool_val v1 (typeof a1) m' = Some false -> evalinf_expr e m' RV a2 t2 -> evalinf_expr e m RV (Eseqor a1 a2 ty) (t1***t2) | evalinf_condition: forall e m a1 a2 a3 ty t1, @@ -1968,7 +1968,7 @@ CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := evalinf_expr e m RV (Econdition a1 a2 a3 ty) t1 | evalinf_condition_2: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 b, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> - bool_val v1 (typeof a1) = Some b -> + bool_val v1 (typeof a1) m' = Some b -> evalinf_expr e m' RV (if b then a2 else a3) t2 -> evalinf_expr e m RV (Econdition a1 a2 a3 ty) (t1***t2) | evalinf_assign_left: forall e m a1 t1 a2 ty, @@ -2039,7 +2039,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Sifthenelse a s1 s2) t1 | execinf_Sifthenelse: forall e m a s1 s2 t1 m1 v1 t2 b, eval_expression e m a t1 m1 v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m1 = Some b -> execinf_stmt e m1 (if b then s1 else s2) t2 -> execinf_stmt e m (Sifthenelse a s1 s2) (t1***t2) | execinf_Sreturn_some: forall e m a t, @@ -2050,12 +2050,12 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Swhile a s) t1 | execinf_Swhile_body: forall e m a s t1 m1 v t2, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> execinf_stmt e m1 s t2 -> execinf_stmt e m (Swhile a s) (t1***t2) | execinf_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3, eval_expression e m a t1 m1 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> execinf_stmt e m2 (Swhile a s) t3 -> @@ -2072,7 +2072,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> eval_expression e m1 a t2 m2 v -> - bool_val v (typeof a) = Some true -> + bool_val v (typeof a) m2 = Some true -> execinf_stmt e m2 (Sdowhile a s) t3 -> execinf_stmt e m (Sdowhile a s) (t1***t2***t3) | execinf_Sfor_start_1: forall e m s a1 a2 a3 t1, @@ -2087,19 +2087,19 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := execinf_stmt e m (Sfor Sskip a2 a3 s) t | execinf_Sfor_body: forall e m s a2 a3 t1 m1 v t2, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> execinf_stmt e m1 s t2 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2) | execinf_Sfor_next: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> execinf_stmt e m2 a3 t3 -> execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2***t3) | execinf_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4, eval_expression e m a2 t1 m1 v -> - bool_val v (typeof a2) = Some true -> + bool_val v (typeof a2) m1 = Some true -> exec_stmt e m1 s t2 m2 out1 -> out_normal_or_continue out1 -> exec_stmt e m2 a3 t3 m3 Out_normal -> diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 43d34007..2582fff8 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1376,9 +1376,9 @@ Proof. Qed. Lemma pres_sem_unop: - forall op ty1 ty v1 v, + forall op ty1 ty v1 m v, type_unop op ty1 = OK ty -> - sem_unary_operation op v1 ty1 = Some v -> + sem_unary_operation op v1 ty1 m = Some v -> wt_val v1 ty1 -> wt_val v ty. Proof. @@ -1390,7 +1390,7 @@ Proof. destruct (Float.cmp Ceq f Float.zero); constructor; auto with ty. destruct (Float32.cmp Ceq f Float32.zero); constructor; auto with ty. destruct (Int.eq i Int.zero); constructor; auto with ty. - constructor; auto with ty. + constructor. constructor. destruct (Int64.eq i Int64.zero); constructor; auto with ty. - (* notint *) unfold sem_notint in SEM; DestructCases; auto with ty. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 025960d7..7af4792a 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -74,7 +74,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := constval ce l | Eunop op r1 ty => do v1 <- constval ce r1; - match sem_unary_operation op v1 (typeof r1) with + match sem_unary_operation op v1 (typeof r1) Mem.empty with | Some v => OK v | None => Error(msg "undefined unary operation") end @@ -94,7 +94,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := | Eseqand r1 r2 ty => do v1 <- constval ce r1; do v2 <- constval ce r2; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some true => do_cast v2 (typeof r2) type_bool | Some false => OK (Vint Int.zero) | None => Error(msg "undefined && operation") @@ -102,7 +102,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := | Eseqor r1 r2 ty => do v1 <- constval ce r1; do v2 <- constval ce r2; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some false => do_cast v2 (typeof r2) type_bool | Some true => OK (Vint Int.one) | None => Error(msg "undefined || operation") @@ -111,7 +111,7 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := do v1 <- constval ce r1; do v2 <- constval ce r2; do v3 <- constval ce r3; - match bool_val v1 (typeof r1) with + match bool_val v1 (typeof r1) Mem.empty with | Some true => do_cast v2 (typeof r2) ty | Some false => do_cast v3 (typeof r3) ty | None => Error(msg "condition is undefined") diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 02a453cf..e0fcb210 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -112,7 +112,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) | esr_unop: forall op r1 ty v1 v, eval_simple_rvalue r1 v1 -> - sem_unary_operation op v1 (typeof r1) = Some v -> + sem_unary_operation op v1 (typeof r1) m = Some v -> eval_simple_rvalue (Eunop op r1 ty) v | esr_binop: forall op r1 r2 ty v1 v2 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> @@ -127,23 +127,23 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_alignof: forall ty1 ty, eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))) | esr_seqand_true: forall r1 r2 ty v1 v2 v3, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue r2 v2 -> sem_cast v2 (typeof r2) type_bool = Some v3 -> eval_simple_rvalue (Eseqand r1 r2 ty) v3 | esr_seqand_false: forall r1 r2 ty v1, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some false -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false -> eval_simple_rvalue (Eseqand r1 r2 ty) (Vint Int.zero) | esr_seqor_false: forall r1 r2 ty v1 v2 v3, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some false -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false -> eval_simple_rvalue r2 v2 -> sem_cast v2 (typeof r2) type_bool = Some v3 -> eval_simple_rvalue (Eseqor r1 r2 ty) v3 | esr_seqor_true: forall r1 r2 ty v1, - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue (Eseqor r1 r2 ty) (Vint Int.one) | esr_condition: forall r1 r2 r3 ty v v1 b v', - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some b -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some b -> eval_simple_rvalue (if b then r2 else r3) v' -> sem_cast v' (typeof (if b then r2 else r3)) ty = Some v -> eval_simple_rvalue (Econdition r1 r2 r3 ty) v @@ -366,6 +366,15 @@ Proof. intros [v' [A B]]. congruence. Qed. +Lemma bool_val_match: + forall v ty b v' m, + bool_val v ty Mem.empty = Some b -> + val_inject inj v v' -> + bool_val v' ty m = Some b. +Proof. + intros. eapply bool_val_inj; eauto. intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. +Qed. + (** Soundness of [constval] with respect to the big-step semantics *) Lemma constval_rvalue: @@ -390,8 +399,10 @@ Proof. (* addrof *) eauto. (* unop *) - destruct (sem_unary_operation op x (typeof r1)) as [v1'|] eqn:E; inv EQ0. - exploit sem_unary_operation_inject. eexact E. eauto. + destruct (sem_unary_operation op x (typeof r1) Mem.empty) as [v1'|] eqn:E; inv EQ0. + exploit (sem_unary_operation_inj inj Mem.empty m). + intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. + eexact E. eauto. intros [v' [A B]]. congruence. (* binop *) destruct (sem_binary_operation ge op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2. @@ -409,24 +420,24 @@ Proof. (* alignof *) constructor. (* seqand *) - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = true) by congruence. subst b. eapply sem_cast_match; eauto. - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = false) by congruence. subst b. inv H2. auto. (* seqor *) - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = false) by congruence. subst b. eapply sem_cast_match; eauto. - destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = true) by congruence. subst b. inv H2. auto. (* conditional *) - destruct (bool_val x (typeof r1)) as [b'|] eqn:E; inv EQ3. - exploit bool_val_inject. eexact E. eauto. intros E'. + destruct (bool_val x (typeof r1) Mem.empty) as [b'|] eqn:E; inv EQ3. + exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b' = b) by congruence. subst b'. destruct b; eapply sem_cast_match; eauto. (* comma *) diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 36fe07ae..097dc589 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -18,6 +18,7 @@ Require Import Errors. Require Import Integers. Require Import Floats. Require Import Values. +Require Import Memory. Require Import AST. Require Import Ctypes. Require Import Cop. @@ -129,7 +130,7 @@ Function eval_simpl_expr (a: expr) : option val := Function makeif (a: expr) (s1 s2: statement) : statement := match eval_simpl_expr a with | Some v => - match bool_val v (typeof a) with + match bool_val v (typeof a) Mem.empty with | Some b => if b then s1 else s2 | None => Sifthenelse a s1 s2 end diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 74019061..7ef1cbe2 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -761,20 +761,30 @@ Proof. inv H; simpl; auto. Qed. +Lemma static_bool_val_sound: + forall v t m b, bool_val v t Mem.empty = Some b -> bool_val v t m = Some b. +Proof. + intros until b; unfold bool_val. destruct (classify_bool t); destruct v; auto. + intros E. unfold Mem.weak_valid_pointer, Mem.valid_pointer, proj_sumbool in E. + rewrite ! pred_dec_false in E by (apply Mem.perm_empty). discriminate. +Qed. + Lemma step_makeif: forall f a s1 s2 k e le m v1 b, eval_expr tge e le m a v1 -> - bool_val v1 (typeof a) = Some b -> + bool_val v1 (typeof a) m = Some b -> star step1 tge (State f (makeif a s1 s2) k e le m) E0 (State f (if b then s1 else s2) k e le m). Proof. intros. functional induction (makeif a s1 s2). - exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. - rewrite e1 in H0. inv H0. constructor. - exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. - rewrite e1 in H0. inv H0. constructor. - apply star_one. eapply step_ifthenelse; eauto. - apply star_one. eapply step_ifthenelse; eauto. +- exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. + assert (bool_val v1 (typeof a) m = Some true) by (apply static_bool_val_sound; auto). + replace b with true by congruence. constructor. +- exploit eval_simpl_expr_sound; eauto. rewrite e0. intro EQ; subst v. + assert (bool_val v1 (typeof a) m = Some false) by (apply static_bool_val_sound; auto). + replace b with false by congruence. constructor. +- apply star_one. eapply step_ifthenelse; eauto. +- apply star_one. eapply step_ifthenelse; eauto. Qed. Lemma step_make_set: diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 5cf59d94..3364ec6a 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -267,11 +267,8 @@ Proof. constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor; auto. (* long *) destruct ty; try (destruct f); try discriminate. destruct v; inv H. constructor. diff --git a/common/AST.v b/common/AST.v index 9c29a374..d2926178 100644 --- a/common/AST.v +++ b/common/AST.v @@ -576,7 +576,7 @@ Inductive external_function : Type := Produces no observable event. *) | EF_memcpy (sz: Z) (al: Z) (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *) - | EF_annot (text: ident) (targs: list annot_arg) + | EF_annot (text: ident) (targs: list typ) (** A programmer-supplied annotation. Takes zero, one or several arguments, produces an event carrying the text and the values of these arguments, and returns no value. *) @@ -584,27 +584,15 @@ Inductive external_function : Type := (** Another form of annotation that takes one argument, produces an event carrying the text and the value of this argument, and returns the value of the argument. *) - | EF_inline_asm (text: ident) + | EF_inline_asm (text: ident). (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic preservation theorem. Generated only if [-finline-asm] is given. *) -with annot_arg : Type := - | AA_arg (ty: typ) - | AA_int (n: int) - | AA_float (n: float). - (** The type signature of an external function. *) -Fixpoint annot_args_typ (targs: list annot_arg) : list typ := - match targs with - | nil => nil - | AA_arg ty :: targs' => ty :: annot_args_typ targs' - | _ :: targs' => annot_args_typ targs' - end. - Definition ef_sig (ef: external_function): signature := match ef with | EF_external name sg => sg @@ -616,7 +604,7 @@ Definition ef_sig (ef: external_function): signature := | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default | EF_free => mksignature (Tint :: nil) None cc_default | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default - | EF_annot text targs => mksignature (annot_args_typ targs) None cc_default + | EF_annot text targs => mksignature targs None cc_default | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default | EF_inline_asm text => mksignature nil None cc_default end. @@ -653,7 +641,7 @@ Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} Proof. generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros. decide equality. - apply list_eq_dec. decide equality. apply Float.eq_dec. + apply list_eq_dec. auto. Defined. Global Opaque external_function_eq. @@ -699,3 +687,56 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := end. End TRANSF_PARTIAL_FUNDEF. + +(** * Arguments to annotations *) + +Set Contextual Implicit. + +Inductive annot_arg (A: Type) : Type := + | AA_base (x: A) + | AA_int (n: int) + | AA_long (n: int64) + | AA_float (f: float) + | AA_single (f: float32) + | AA_loadstack (chunk: memory_chunk) (ofs: int) + | AA_addrstack (ofs: int) + | AA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int) + | AA_addrglobal (id: ident) (ofs: int) + | AA_longofwords (hi lo: annot_arg A). + +Fixpoint globals_of_annot_arg (A: Type) (a: annot_arg A) : list ident := + match a with + | AA_loadglobal chunk id ofs => id :: nil + | AA_addrglobal id ofs => id :: nil + | AA_longofwords hi lo => globals_of_annot_arg hi ++ globals_of_annot_arg lo + | _ => nil + end. + +Definition globals_of_annot_args (A: Type) (al: list (annot_arg A)) : list ident := + List.fold_right (fun a l => globals_of_annot_arg a ++ l) nil al. + +Fixpoint params_of_annot_arg (A: Type) (a: annot_arg A) : list A := + match a with + | AA_base x => x :: nil + | AA_longofwords hi lo => params_of_annot_arg hi ++ params_of_annot_arg lo + | _ => nil + end. + +Definition params_of_annot_args (A: Type) (al: list (annot_arg A)) : list A := + List.fold_right (fun a l => params_of_annot_arg a ++ l) nil al. + +Fixpoint map_annot_arg (A B: Type) (f: A -> B) (a: annot_arg A) : annot_arg B := + match a with + | AA_base x => AA_base (f x) + | AA_int n => AA_int n + | AA_long n => AA_long n + | AA_float n => AA_float n + | AA_single n => AA_single n + | AA_loadstack chunk ofs => AA_loadstack chunk ofs + | AA_addrstack ofs => AA_addrstack ofs + | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs + | AA_addrglobal id ofs => AA_addrglobal id ofs + | AA_longofwords hi lo => + AA_longofwords (map_annot_arg f hi) (map_annot_arg f lo) + end. + diff --git a/common/Events.v b/common/Events.v index 3fb58806..15bf4e12 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1344,25 +1344,16 @@ Qed. (** ** Semantics of annotations. *) -Fixpoint annot_eventvals (targs: list annot_arg) (vargs: list eventval) : list eventval := - match targs, vargs with - | AA_arg ty :: targs', varg :: vargs' => varg :: annot_eventvals targs' vargs' - | AA_int n :: targs', _ => EVint n :: annot_eventvals targs' vargs - | AA_float n :: targs', _ => EVfloat n :: annot_eventvals targs' vargs - | _, _ => vargs - end. - -Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (ge: Senv.t): +Inductive extcall_annot_sem (text: ident) (targs: list typ) (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := | extcall_annot_sem_intro: forall vargs m args, - eventval_list_match ge args (annot_args_typ targs) vargs -> - extcall_annot_sem text targs ge vargs m - (Event_annot text (annot_eventvals targs args) :: E0) Vundef m. + eventval_list_match ge args targs vargs -> + extcall_annot_sem text targs ge vargs m (Event_annot text args :: E0) Vundef m. Lemma extcall_annot_ok: forall text targs, extcall_properties (extcall_annot_sem text targs) - (mksignature (annot_args_typ targs) None cc_default) + (mksignature targs None cc_default) nil. Proof. intros; constructor; intros. @@ -1794,9 +1785,133 @@ Proof. split; congruence. Qed. +(** * Evaluation of annotation arguments *) + +Section EVAL_ANNOT_ARG. + +Variable A: Type. +Variable ge: Senv.t. +Variable e: A -> val. +Variable sp: val. +Variable m: mem. + +Inductive eval_annot_arg: annot_arg A -> val -> Prop := + | eval_AA_base: forall x, + eval_annot_arg (AA_base x) (e x) + | eval_AA_int: forall n, + eval_annot_arg (AA_int n) (Vint n) + | eval_AA_long: forall n, + eval_annot_arg (AA_long n) (Vlong n) + | eval_AA_float: forall n, + eval_annot_arg (AA_float n) (Vfloat n) + | eval_AA_single: forall n, + eval_annot_arg (AA_single n) (Vsingle n) + | eval_AA_loadstack: forall chunk ofs v, + Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v -> + eval_annot_arg (AA_loadstack chunk ofs) v + | eval_AA_addrstack: forall ofs, + eval_annot_arg (AA_addrstack ofs) (Val.add sp (Vint ofs)) + | eval_AA_loadglobal: forall chunk id ofs v, + Mem.loadv chunk m (Senv.symbol_address ge id ofs) = Some v -> + eval_annot_arg (AA_loadglobal chunk id ofs) v + | eval_AA_addrglobal: forall id ofs, + eval_annot_arg (AA_addrglobal id ofs) (Senv.symbol_address ge id ofs) + | eval_AA_longofwords: forall hi lo vhi vlo, + eval_annot_arg hi vhi -> eval_annot_arg lo vlo -> + eval_annot_arg (AA_longofwords hi lo) (Val.longofwords vhi vlo). + +Definition eval_annot_args (al: list (annot_arg A)) (vl: list val) : Prop := + list_forall2 eval_annot_arg al vl. + +Lemma eval_annot_arg_determ: + forall a v, eval_annot_arg a v -> forall v', eval_annot_arg a v' -> v' = v. +Proof. + induction 1; intros v' EV; inv EV; try congruence. + f_equal; eauto. +Qed. + +Lemma eval_annot_args_determ: + forall al vl, eval_annot_args al vl -> forall vl', eval_annot_args al vl' -> vl' = vl. +Proof. + induction 1; intros v' EV; inv EV; f_equal; eauto using eval_annot_arg_determ. +Qed. + +End EVAL_ANNOT_ARG. + +Hint Constructors eval_annot_arg: aarg. + +(** Invariance by change of global environment. *) + +Section EVAL_ANNOT_ARG_PRESERVED. + +Variables A F1 V1 F2 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. +Variable e: A -> val. +Variable sp: val. +Variable m: mem. + +Hypothesis symbols_preserved: + forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id. + +Lemma eval_annot_arg_preserved: + forall a v, eval_annot_arg ge1 e sp m a v -> eval_annot_arg ge2 e sp m a v. +Proof. + assert (EQ: forall id ofs, Senv.symbol_address ge2 id ofs = Senv.symbol_address ge1 id ofs). + { unfold Senv.symbol_address; simpl; intros. rewrite symbols_preserved; auto. } + induction 1; eauto with aarg. rewrite <- EQ in H; eauto with aarg. rewrite <- EQ; eauto with aarg. +Qed. +Lemma eval_annot_args_preserved: + forall al vl, eval_annot_args ge1 e sp m al vl -> eval_annot_args ge2 e sp m al vl. +Proof. + induction 1; constructor; auto; eapply eval_annot_arg_preserved; eauto. +Qed. +End EVAL_ANNOT_ARG_PRESERVED. +(** Compatibility with the "is less defined than" relation. *) +Section EVAL_ANNOT_ARG_LESSDEF. +Variable A: Type. +Variable ge: Senv.t. +Variables e1 e2: A -> val. +Variable sp: val. +Variables m1 m2: mem. + +Hypothesis env_lessdef: forall x, Val.lessdef (e1 x) (e2 x). +Hypothesis mem_extends: Mem.extends m1 m2. + +Lemma eval_annot_arg_lessdef: + forall a v1, eval_annot_arg ge e1 sp m1 a v1 -> + exists v2, eval_annot_arg ge e2 sp m2 a v2 /\ Val.lessdef v1 v2. +Proof. + induction 1. +- exists (e2 x); auto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg. +- econstructor; eauto with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg. +- econstructor; eauto with aarg. +- destruct IHeval_annot_arg1 as (vhi' & P & Q). + destruct IHeval_annot_arg2 as (vlo' & R & S). + econstructor; split; eauto with aarg. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma eval_annot_args_lessdef: + forall al vl1, eval_annot_args ge e1 sp m1 al vl1 -> + exists vl2, eval_annot_args ge e2 sp m2 al vl2 /\ Val.lessdef_list vl1 vl2. +Proof. + induction 1. +- econstructor; split. constructor. auto. +- exploit eval_annot_arg_lessdef; eauto. intros (v1' & P & Q). + destruct IHlist_forall2 as (vl' & U & V). + exists (v1'::vl'); split; constructor; auto. +Qed. + +End EVAL_ANNOT_ARG_LESSDEF. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index c0eab04f..52aa963a 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -54,3 +54,28 @@ let name_of_external = function | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text) | EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text) | EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text) + +let rec print_annot_arg px oc = function + | AA_base x -> px oc x + | AA_int n -> fprintf oc "int %ld" (camlint_of_coqint n) + | AA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n) + | AA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n) + | AA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n) + | AA_loadstack(chunk, ofs) -> + fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs) + | AA_addrstack(ofs) -> + fprintf oc "sp + %ld" (camlint_of_coqint ofs) + | AA_loadglobal(chunk, id, ofs) -> + fprintf oc "%s[&%s + %ld]" + (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) + | AA_addrglobal(id, ofs) -> + fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs) + | AA_longofwords(hi, lo) -> + fprintf oc "longofwords(%a, %a)" + (print_annot_arg px) hi (print_annot_arg px) lo + +let rec print_annot_args px oc = function + | [] -> () + | [a] -> print_annot_arg px oc a + | a1 :: al -> + fprintf oc "%a, %a" (print_annot_arg px) a1 (print_annot_args px) al diff --git a/common/Values.v b/common/Values.v index a12fb636..12b380b7 100644 --- a/common/Values.v +++ b/common/Values.v @@ -111,15 +111,13 @@ Proof. simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto. Qed. -(** Truth values. Pointers and non-zero integers are treated as [True]. +(** Truth values. Non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. - [Vundef] and floats are neither true nor false. *) + Other values are neither true nor false. *) Inductive bool_of_val: val -> bool -> Prop := | bool_of_val_int: - forall n, bool_of_val (Vint n) (negb (Int.eq n Int.zero)) - | bool_of_val_ptr: - forall b ofs, bool_of_val (Vptr b ofs) true. + forall n, bool_of_val (Vint n) (negb (Int.eq n Int.zero)). (** Arithmetic operations *) @@ -695,7 +693,9 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool := | Vint n1, Vint n2 => Some (Int.cmpu c n1 n2) | Vint n1, Vptr b2 ofs2 => - if Int.eq n1 Int.zero then cmp_different_blocks c else None + if Int.eq n1 Int.zero && weak_valid_ptr b2 (Int.unsigned ofs2) + then cmp_different_blocks c + else None | Vptr b1 ofs1, Vptr b2 ofs2 => if eq_block b1 b2 then if weak_valid_ptr b1 (Int.unsigned ofs1) @@ -708,7 +708,9 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool := then cmp_different_blocks c else None | Vptr b1 ofs1, Vint n2 => - if Int.eq n2 Int.zero then cmp_different_blocks c else None + if Int.eq n2 Int.zero && weak_valid_ptr b1 (Int.unsigned ofs1) + then cmp_different_blocks c + else None | _, _ => None end. @@ -1175,8 +1177,8 @@ Proof. destruct c; auto. destruct x; destruct y; simpl; auto. rewrite Int.negate_cmpu. auto. - destruct (Int.eq i Int.zero); auto. - destruct (Int.eq i0 Int.zero); auto. + destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. + destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto. destruct (eq_block b b0). destruct ((valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1)) && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))). @@ -1222,8 +1224,8 @@ Proof. destruct c; auto. destruct x; destruct y; simpl; auto. rewrite Int.swap_cmpu. auto. - case (Int.eq i Int.zero); auto. - case (Int.eq i0 Int.zero); auto. + destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. + destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto. destruct (eq_block b b0); subst. rewrite dec_eq_true. destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)); @@ -1381,6 +1383,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: @@ -1423,19 +1431,23 @@ Lemma cmpu_bool_lessdef: cmpu_bool valid_ptr' c v1' v2' = Some b. Proof. intros. + assert (A: forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> + valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). + { intros until ofs. rewrite ! orb_true_iff. intuition. } destruct v1; simpl in H2; try discriminate; destruct v2; simpl in H2; try discriminate; inv H0; inv H1; simpl; auto. + destruct (Int.eq i Int.zero && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))) eqn:E; try discriminate. + InvBooleans. rewrite H0, A by auto. auto. + destruct (Int.eq i0 Int.zero && (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1))) eqn:E; try discriminate. + InvBooleans. rewrite H0, A by auto. auto. destruct (eq_block b0 b1). - assert (forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> - valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). - intros until ofs. rewrite ! orb_true_iff. intuition. destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)) eqn:?; try discriminate. destruct (valid_ptr b1 (Int.unsigned i0) || valid_ptr b1 (Int.unsigned i0 - 1)) eqn:?; try discriminate. - erewrite !H0 by eauto. auto. + erewrite ! A by eauto. auto. destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate. destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate. - erewrite !H by eauto. auto. + erewrite ! H by eauto. auto. Qed. Lemma of_optbool_lessdef: @@ -1599,7 +1611,17 @@ Lemma val_cmpu_bool_inject: Proof. Local Opaque Int.add. intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. - fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. +- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. + fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). + destruct (Int.eq i Int.zero); auto. + destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate. + erewrite weak_valid_ptr_inj by eauto. auto. +- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. + fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). + destruct (Int.eq i Int.zero); auto. + destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate. + erewrite weak_valid_ptr_inj by eauto. auto. +- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. fold (weak_valid_ptr1 b0 (Int.unsigned ofs0)) in H1. fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))). @@ -212,11 +212,7 @@ Inductive instruction: Type := | Pallocframe(sz: Z)(ofs_ra ofs_link: int) | Pfreeframe(sz: Z)(ofs_ra ofs_link: int) | Pbuiltin(ef: external_function)(args: list preg)(res: list preg) - | Pannot(ef: external_function)(args: list annot_param) - -with annot_param : Type := - | APreg: preg -> annot_param - | APstack: memory_chunk -> Z -> annot_param. + | Pannot(ef: external_function)(args: list (annot_arg preg)). Definition code := list instruction. Record function : Type := mkfunction { fn_sig: signature; fn_code: code }. @@ -798,20 +794,6 @@ Definition extcall_arguments Definition loc_external_result (sg: signature) : list preg := map preg_of (loc_result sg). -(** Extract the values of the arguments of an annotation. *) - -Inductive annot_arg (rs: regset) (m: mem): annot_param -> val -> Prop := - | annot_arg_reg: forall r, - annot_arg rs m (APreg r) (rs r) - | annot_arg_stack: forall chunk ofs stk base v, - rs (IR ESP) = Vptr stk base -> - Mem.load chunk m stk (Int.unsigned base + ofs) = Some v -> - annot_arg rs m (APstack chunk ofs) v. - -Definition annot_arguments - (rs: regset) (m: mem) (params: list annot_param) (args: list val) : Prop := - list_forall2 (annot_arg rs m) params args. - (** Execution of the instruction at [rs#PC]. *) Inductive state: Type := @@ -840,8 +822,8 @@ Inductive step: state -> trace -> state -> Prop := rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) -> - annot_arguments rs m args vargs -> - external_call' ef ge vargs m t v m' -> + eval_annot_args ge rs (rs ESP) m args vargs -> + external_call ef ge vargs m t v m' -> step (State rs m) t (State (nextinstr rs) m') | exec_step_external: @@ -893,16 +875,6 @@ Proof. intros. red in H0; red in H1. eauto. Qed. -Remark annot_arguments_determ: - forall rs m params args1 args2, - annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2. -Proof. - unfold annot_arguments. intros. revert params args1 H args2 H0. - induction 1; intros. - inv H0; auto. - inv H1. decEq; eauto. inv H; inv H4. auto. congruence. -Qed. - Lemma semantics_determinate: forall p, determinate (semantics p). Proof. Ltac Equalities := @@ -912,32 +884,32 @@ Ltac Equalities := | _ => idtac end. intros; constructor; simpl; intros. -(* determ *) +- (* determ *) inv H; inv H0; Equalities. - split. constructor. auto. - discriminate. - discriminate. - inv H11. - exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. ++ split. constructor. auto. ++ discriminate. ++ discriminate. ++ inv H11. ++ exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. - inv H12. - assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. - exploit external_call_determ'. eexact H5. eexact H13. intros [A B]. ++ inv H12. ++ assert (vargs0 = vargs) by (eapply eval_annot_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H13. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. - assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. ++ assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. -(* trace length *) +- (* trace length *) red; intros; inv H; simpl. omega. inv H3. eapply external_call_trace_length; eauto. - inv H4. eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. inv H3. eapply external_call_trace_length; eauto. -(* initial states *) +- (* initial states *) inv H; inv H0. f_equal. congruence. -(* final no step *) +- (* final no step *) inv H. unfold Vzero in H0. red; intros; red; intros. inv H; congruence. -(* final states *) +- (* final states *) inv H; inv H0. congruence. Qed. diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 9c0a76e0..2c1afc11 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -492,14 +492,6 @@ Definition transl_store (chunk: memory_chunk) Error (msg "Asmgen.transl_store") end. -(** Translation of arguments to annotations *) - -Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param := - match p with - | Mach.APreg r => APreg (preg_of r) - | Mach.APstack chunk ofs => APstack chunk ofs - end. - (** Translation of a Mach instruction. *) Definition transl_instr (f: Mach.function) (i: Mach.instruction) @@ -546,7 +538,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mbuiltin ef args res => OK (Pbuiltin ef (List.map preg_of args) (List.map preg_of res) :: k) | Mannot ef args => - OK (Pannot ef (map transl_annot_param args) :: k) + OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k) end. (** Translation of a code sequence *) diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 57d7de4a..3570da2e 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -700,13 +700,16 @@ Opaque loadind. inv AT. monadInv H4. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends'; eauto. + exploit annot_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. - eapply external_call_symbols_preserved'; eauto. + erewrite <- sp_val by 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. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 7d71d1a2..0ca343fb 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -462,12 +462,14 @@ Proof. rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity. destruct (Int.ltu i i0); reflexivity. (* int ptr *) - destruct (Int.eq i Int.zero) eqn:?; try discriminate. + destruct (Int.eq i Int.zero && + (Mem.valid_pointer m b0 (Int.unsigned i0) || Mem.valid_pointer m b0 (Int.unsigned i0 - 1))) eqn:?; try discriminate. destruct c; simpl in *; inv H1. rewrite Heqb1; reflexivity. rewrite Heqb1; reflexivity. (* ptr int *) - destruct (Int.eq i0 Int.zero) eqn:?; try discriminate. + destruct (Int.eq i0 Int.zero && + (Mem.valid_pointer m b0 (Int.unsigned i) || Mem.valid_pointer m b0 (Int.unsigned i - 1))) eqn:?; try discriminate. destruct c; simpl in *; inv H1. rewrite Heqb1; reflexivity. rewrite Heqb1; reflexivity. @@ -647,6 +647,7 @@ Definition is_trivial_op (op: operation) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with | Ocmp (Ccompu _) => true + | Ocmp (Ccompuimm _ _) => true | _ => false end. @@ -656,7 +657,7 @@ Lemma op_depends_on_memory_correct: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence. - destruct c; simpl; try congruence. reflexivity. + destruct c; simpl; auto; congruence. Qed. (** Global variables mentioned in an operation or addressing mode *) diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index b6aef725..74e3fbd7 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -507,3 +507,17 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := | _ => (Aindexed Int.zero, e:::Enil) end. +(** ** Arguments of annotations *) + +Nondetfunction annot_arg (e: expr) := + match e with + | Eop (Ointconst n) Enil => AA_int n + | Eop (Olea (Aglobal id ofs)) Enil => AA_addrglobal id ofs + | Eop (Olea (Ainstack ofs)) Enil => AA_addrstack ofs + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => + AA_long (Int64.ofwords h l) + | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l) + | Eload chunk (Aglobal id ofs) Enil => AA_loadglobal chunk id ofs + | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs + | _ => AA_base e + end. diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 50688621..50f0d9b6 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -898,4 +898,20 @@ Proof. exists (v :: nil); split. constructor; auto. constructor. subst; simpl. rewrite Int.add_zero; auto. Qed. +Theorem eval_annot_arg: + forall a v, + eval_expr ge sp e m nil a v -> + CminorSel.eval_annot_arg ge sp e m (annot_arg a) v. +Proof. + intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval. +- constructor. +- constructor. +- constructor. +- simpl in H5. inv H5. constructor. +- subst v. constructor; auto. +- inv H. InvEval. simpl in H6; inv H6. constructor; auto. +- inv H. InvEval. simpl in H6. inv H6. constructor; auto. +- constructor; auto. +Qed. + End CMCONSTR. diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 71e6cba6..92be0ff3 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -339,7 +339,7 @@ module Target(System: SYSTEM):TARGET = (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args + PrintAnnot.print_annot_stmt preg "%esp" oc txt targs args end let print_annot_val oc txt args res = diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 18316fb0..d707b2b5 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -276,13 +276,9 @@ Inductive instruction : Type := | Pxoris: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate high *) | Plabel: label -> instruction (**r define a code label *) | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function (pseudo) *) - | Pannot: external_function -> list annot_param -> instruction (**r annotation statement (pseudo) *) + | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement (pseudo) *) | Pcfi_adjust: int -> instruction (**r .cfi_adjust debug directive *) - | Pcfi_rel_offset: int -> instruction (**r .cfi_rel_offset lr debug directive *) - -with annot_param : Type := - | APreg: preg -> annot_param - | APstack: memory_chunk -> Z -> annot_param. + | Pcfi_rel_offset: int -> instruction. (**r .cfi_rel_offset lr debug directive *) (** The pseudo-instructions are the following: @@ -936,20 +932,6 @@ Definition extcall_arguments Definition loc_external_result (sg: signature) : list preg := map preg_of (loc_result sg). -(** Extract the values of the arguments of an annotation. *) - -Inductive annot_arg (rs: regset) (m: mem): annot_param -> val -> Prop := - | annot_arg_reg: forall r, - annot_arg rs m (APreg r) (rs r) - | annot_arg_stack: forall chunk ofs stk base v, - rs (IR GPR1) = Vptr stk base -> - Mem.load chunk m stk (Int.unsigned base + ofs) = Some v -> - annot_arg rs m (APstack chunk ofs) v. - -Definition annot_arguments - (rs: regset) (m: mem) (params: list annot_param) (args: list val) : Prop := - list_forall2 (annot_arg rs m) params args. - (** Execution of the instruction at [rs#PC]. *) Inductive state: Type := @@ -978,8 +960,8 @@ Inductive step: state -> trace -> state -> Prop := rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) -> - annot_arguments rs m args vargs -> - external_call' ef ge vargs m t v m' -> + eval_annot_args ge rs (rs GPR1) m args vargs -> + external_call ef ge vargs m t v m' -> step (State rs m) t (State (nextinstr rs) m') | exec_step_external: @@ -1031,16 +1013,6 @@ Proof. intros. red in H0; red in H1. eauto. Qed. -Remark annot_arguments_determ: - forall rs m params args1 args2, - annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2. -Proof. - unfold annot_arguments. intros. revert params args1 H args2 H0. - induction 1; intros. - inv H0; auto. - inv H1. decEq; eauto. inv H; inv H4. auto. congruence. -Qed. - Lemma semantics_determinate: forall p, determinate (semantics p). Proof. Ltac Equalities := @@ -1059,8 +1031,8 @@ Ltac Equalities := exploit external_call_determ'. eexact H4. eexact H9. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. inv H12. - assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0. - exploit external_call_determ'. eexact H5. eexact H13. intros [A B]. + assert (vargs0 = vargs) by (eapply eval_annot_args_determ; eauto). subst vargs0. + exploit external_call_determ. eexact H5. eexact H13. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. exploit external_call_determ'. eexact H3. eexact H8. intros [A B]. @@ -1069,7 +1041,7 @@ Ltac Equalities := red; intros. inv H; simpl. omega. inv H3; eapply external_call_trace_length; eauto. - inv H4; eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. inv H2; eapply external_call_trace_length; eauto. (* initial states *) inv H; inv H0. f_equal. congruence. diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index c003bcd1..47895cb1 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -74,7 +74,7 @@ let _m8 = coqint_of_camlint (-8l) (* Handling of annotations *) let expand_annot_val txt targ args res = - emit (Pannot(EF_annot(txt, [AA_arg targ]), List.map (fun r -> APreg r) args)); + emit (Pannot(EF_annot(txt, [targ]), List.map (fun r -> AA_base r) args)); begin match args, res with | [IR src], [IR dst] -> if dst <> src then emit (Pmr(dst, src)) diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 2bd69d91..7ee6c770 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -610,14 +610,6 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) Error (msg "Asmgen.transl_store") end. -(** Translation of arguments to annotations *) - -Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param := - match p with - | Mach.APreg r => APreg (preg_of r) - | Mach.APstack chunk ofs => APstack chunk ofs - end. - (** Translation of a Mach instruction. *) Definition transl_instr (f: Mach.function) (i: Mach.instruction) @@ -658,7 +650,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mbuiltin ef args res => OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k) | Mannot ef args => - OK (Pannot ef (map transl_annot_param args) :: k) + OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k) | Mlabel lbl => OK (Plabel lbl :: k) | Mgoto lbl => diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index c7439c3d..27b32ba1 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -778,13 +778,16 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. inv AT. monadInv H4. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends'; eauto. + exploit annot_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. - eapply external_call_symbols_preserved'; eauto. + erewrite <- sp_val by 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. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. diff --git a/powerpc/Op.v b/powerpc/Op.v index 3d5b1fc5..4c1168cd 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -569,6 +569,7 @@ Definition is_trivial_op (op: operation) : bool := Definition op_depends_on_memory (op: operation) : bool := match op with | Ocmp (Ccompu _) => true + | Ocmp (Ccompuimm _ _) => true | _ => false end. @@ -577,8 +578,8 @@ Lemma op_depends_on_memory_correct: op_depends_on_memory op = false -> eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. - intros until m2. destruct op; simpl; try congruence. - destruct c; simpl; auto; discriminate. + intros until m2. destruct op; simpl; try congruence. unfold eval_condition. + destruct c; simpl; auto; try discriminate. Qed. (** Global variables mentioned in an operation or addressing mode *) diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 70b1feb6..618643b8 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -523,3 +523,18 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil) | _ => (Aindexed Int.zero, e:::Enil) end. + +(** ** Arguments of annotations *) + +Nondetfunction annot_arg (e: expr) := + match e with + | Eop (Ointconst n) Enil => AA_int n + | Eop (Oaddrsymbol id ofs) Enil => AA_addrglobal id ofs + | Eop (Oaddrstack ofs) Enil => AA_addrstack ofs + | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => + AA_long (Int64.ofwords h l) + | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l) + | Eload chunk (Aglobal id ofs) Enil => AA_loadglobal chunk id ofs + | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs + | _ => AA_base e + end. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 8311b82c..c51b650b 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -999,5 +999,21 @@ Proof. rewrite Int.add_zero. auto. Qed. +Theorem eval_annot_arg: + forall a v, + eval_expr ge sp e m nil a v -> + CminorSel.eval_annot_arg ge sp e m (annot_arg a) v. +Proof. + intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval. +- constructor. +- constructor. +- constructor. +- simpl in H5. inv H5. constructor. +- subst v. constructor; auto. +- inv H. InvEval. simpl in H6; inv H6. constructor; auto. +- inv H. InvEval. simpl in H6. inv H6. constructor; auto. +- constructor; auto. +Qed. + End CMCONSTR. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 013eefc2..b3d228b3 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -284,9 +284,12 @@ module Target (System : SYSTEM):TARGET = let ireg_or_zero oc r = if r = GPR0 then output_string oc "0" else ireg oc r + (* [preg] is only used for printing annotations. + Use the full register names [rN] and [fN] to avoid + ambiguity with constants. *) let preg oc = function - | IR r -> ireg oc r - | FR r -> freg oc r + | IR r -> fprintf oc "r%s" (int_reg_name r) + | FR r -> fprintf oc "f%s" (float_reg_name r) | _ -> assert false let section oc sec = diff --git a/test/regression/annot1.c b/test/regression/annot1.c index 9bdf14eb..b60f8a64 100644 --- a/test/regression/annot1.c +++ b/test/regression/annot1.c @@ -58,6 +58,42 @@ void k(int arg) C1 + 1, arg, C2 * 2); } +int j(int a) +{ + /* Local variables that are stack-allocated early */ + short b = 0, c = 0; + char d[4]; + *(a ? &b : &c) = 42; + __builtin_annot("j %1 %2 %3 %4", b, c, d[0], d[3]); + return b; +} + +long long ll(long long a) +{ + /* Force spilling */ + long long b = a+1; + long long c = b+1; + long long d = c+1; + long long e = d+1; + long long f = e+1; + long long g = f+1; + long long h = g+1; + long long i = h+1; + long long j = i+1; + long long k = j+1; + long long l = k+1; + long long m = l+1; + long long n = m+1; + long long o = n+1; + long long p = o+1; + long long q = p+1; + long long r = q+1; + long long s = r+1; + long long t = s+1; + __builtin_annot("ll %1 %2 %3 %4 %5 %6 %7 %8 %9 %10 %11 %12 %13 %14 %15 %16 %17 %18 %19 %20", a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t); + return t; +} + int main() { __builtin_annot("calling f"); |