From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 2 +- cfrontend/Cminorgenproof.v | 41 ++++++++++++++++++++++------------------- cfrontend/Csem.v | 17 +++++++++++------ cfrontend/Csharpminor.v | 12 +----------- cfrontend/Cshmgen.v | 5 +++-- cfrontend/Cshmgenproof.v | 12 +++++++----- cfrontend/Csyntax.v | 16 ++++++++-------- cfrontend/Initializersproof.v | 5 +++-- 8 files changed, 56 insertions(+), 54 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 22c3a5a8..c293efbe 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -489,7 +489,7 @@ Definition transl_funbody Definition transl_function (gce: compilenv) (f: Csharpminor.function): res function := let (cenv, stacksize) := build_compilenv gce f in - if zle stacksize Int.max_signed + if zle stacksize Int.max_unsigned then transl_funbody cenv stacksize f else Error(msg "Cminorgen: too many local variables, stack size exceeded"). diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 480acbb9..ba51310f 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -76,7 +76,7 @@ Lemma sig_preserved: Proof. intros until tf; destruct f; simpl. unfold transl_function. destruct (build_compilenv gce f). - case (zle z Int.max_signed); simpl bind; try congruence. + case (zle z Int.max_unsigned); simpl bind; try congruence. intros. monadInv H. simpl. eapply sig_preserved_body; eauto. intro. inv H. reflexivity. Qed. @@ -1265,7 +1265,7 @@ Lemma eval_binop_compat: val_inject f v2 tv2 -> Mem.inject f m tm -> exists tv, - Cminor.eval_binop op tv1 tv2 = Some tv + Cminor.eval_binop op tv1 tv2 tm = Some tv /\ val_inject f v tv. Proof. destruct op; simpl; intros. @@ -1302,19 +1302,25 @@ Proof. inv H0; try discriminate; inv H1; inv H; TrivialOp. inv H0; try discriminate; inv H1; inv H; TrivialOp. inv H0; try discriminate; inv H1; inv H; TrivialOp. - exists v; split; auto. eapply val_inject_eval_compare_null; eauto. - exists v; split; auto. eapply val_inject_eval_compare_null; eauto. - (* cmp ptr ptr *) - caseEq (Mem.valid_pointer m b1 (Int.signed ofs1) && Mem.valid_pointer m b0 (Int.signed ofs0)); +(* cmpu *) + inv H0; try discriminate; inv H1; inv H; TrivialOp. + exists v; split; auto. eapply val_inject_eval_compare_null; eauto. + exists v; split; auto. eapply val_inject_eval_compare_null; eauto. + (* cmpu ptr ptr *) + caseEq (Mem.valid_pointer m b1 (Int.unsigned ofs1) && Mem.valid_pointer m b0 (Int.unsigned ofs0)); intro EQ; rewrite EQ in H4; try discriminate. elim (andb_prop _ _ EQ); intros. + exploit Mem.valid_pointer_inject_val. eauto. eexact H. econstructor; eauto. + intros V1. rewrite V1. + exploit Mem.valid_pointer_inject_val. eauto. eexact H1. econstructor; eauto. + intros V2. rewrite V2. simpl. destruct (eq_block b1 b0); inv H4. (* same blocks in source *) assert (b3 = b2) by congruence. subst b3. assert (delta0 = delta) by congruence. subst delta0. - exists (Val.of_bool (Int.cmp c ofs1 ofs0)); split. + exists (Val.of_bool (Int.cmpu c ofs1 ofs0)); split. unfold eq_block; rewrite zeq_true; simpl. - decEq. decEq. rewrite Int.translate_cmp. auto. + decEq. decEq. rewrite Int.translate_cmpu. auto. eapply Mem.valid_pointer_inject_no_overflow; eauto. eapply Mem.valid_pointer_inject_no_overflow; eauto. apply val_inject_val_of_bool. @@ -1323,13 +1329,11 @@ Proof. destruct (eq_block b2 b3); auto. exploit Mem.different_pointers_inject; eauto. intros [A|A]. congruence. - decEq. destruct c; simpl in H6; inv H6; unfold Int.cmp. + decEq. destruct c; simpl in H6; inv H6; unfold Int.cmpu. predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr delta)) (Int.add ofs0 (Int.repr delta0)). congruence. auto. predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr delta)) (Int.add ofs0 (Int.repr delta0)). congruence. auto. - (* cmpu *) - inv H0; try discriminate; inv H1; inv H; TrivialOp. (* cmpf *) inv H0; try discriminate; inv H1; inv H; TrivialOp. Qed. @@ -1831,7 +1835,7 @@ Lemma match_callstack_alloc_variable: Mem.valid_block tm sp -> Mem.bounds tm sp = (0, tf.(fn_stackspace)) -> Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable -> - tf.(fn_stackspace) <= Int.max_signed -> + tf.(fn_stackspace) <= Int.max_unsigned -> Mem.alloc m 0 (sizeof lv) = (m', b) -> match_callstack f m tm (Frame cenv tf e le te sp lo (Mem.nextblock m) :: cs) @@ -1862,9 +1866,8 @@ Proof. generalize (align_le sz (size_chunk chunk) SIZEPOS). fold ofs. intro SZOFS. exploit Mem.alloc_left_mapped_inject. eauto. eauto. eauto. - instantiate (1 := ofs). - generalize Int.min_signed_neg. omega. - right; rewrite BOUNDS; simpl. generalize Int.min_signed_neg. omega. + instantiate (1 := ofs). omega. + right; rewrite BOUNDS; simpl. omega. intros. apply Mem.perm_implies with Freeable; auto with mem. apply PERMS. rewrite LV in H1. simpl in H1. omega. rewrite LV; simpl. rewrite Zminus_0_r. unfold ofs. @@ -1923,7 +1926,7 @@ Lemma match_callstack_alloc_variables_rec: Mem.valid_block tm sp -> Mem.bounds tm sp = (0, tf.(fn_stackspace)) -> Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable -> - tf.(fn_stackspace) <= Int.max_signed -> + tf.(fn_stackspace) <= Int.max_unsigned -> forall e m vars e' m', alloc_variables e m vars e' m' -> forall f cenv sz, @@ -2016,7 +2019,7 @@ Qed. Lemma match_callstack_alloc_variables: forall fn cenv tf m e m' tm tm' sp f cs targs, build_compilenv gce fn = (cenv, tf.(fn_stackspace)) -> - tf.(fn_stackspace) <= Int.max_signed -> + tf.(fn_stackspace) <= Int.max_unsigned -> list_norepet (fn_params_names fn ++ fn_vars_names fn) -> alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' -> Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) -> @@ -2200,7 +2203,7 @@ Lemma function_entry_ok: bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 -> match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) -> build_compilenv gce fn = (cenv, tf.(fn_stackspace)) -> - tf.(fn_stackspace) <= Int.max_signed -> + tf.(fn_stackspace) <= Int.max_unsigned -> Mem.alloc tm 0 tf.(fn_stackspace) = (tm1, sp) -> let tparams := List.map for_var (fn_params_names fn) in let tvars := List.map for_var (fn_vars_names fn) in @@ -2924,7 +2927,7 @@ Proof. (* internal call *) monadInv TR. generalize EQ; clear EQ; unfold transl_function. caseEq (build_compilenv gce f). intros ce sz BC. - destruct (zle sz Int.max_signed); try congruence. + destruct (zle sz Int.max_unsigned); try congruence. intro TRBODY. generalize TRBODY; intro TMP. monadInv TMP. set (tf := mkfunction (Csharpminor.fn_sig f) diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index dff5fa26..3a3ba3b0 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -413,19 +413,24 @@ Function sem_cmp (c:comparison) (v1: val) (t1: type) (v2: val) (t2: type) (m: mem): option val := match classify_cmp t1 t2 with - | cmp_case_iiu => + | cmp_case_ii Signed => + match v1,v2 with + | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2)) + | _, _ => None + end + | cmp_case_ii Unsigned => match v1,v2 with | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2)) | _, _ => None end - | cmp_case_ipip => + | cmp_case_pp => match v1,v2 with - | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2)) + | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2)) | Vptr b1 ofs1, Vptr b2 ofs2 => - if Mem.valid_pointer m b1 (Int.signed ofs1) - && Mem.valid_pointer m b2 (Int.signed ofs2) then + if Mem.valid_pointer m b1 (Int.unsigned ofs1) + && Mem.valid_pointer m b2 (Int.unsigned ofs2) then if zeq b1 b2 - then Some (Val.of_bool (Int.cmp c ofs1 ofs2)) + then Some (Val.of_bool (Int.cmpu c ofs1 ofs2)) else sem_cmp_mismatch c else None | Vptr b ofs, Vint n => diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 2f05678e..d2eb3c1e 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -267,17 +267,7 @@ Definition eval_constant (cst: constant) : option val := Definition eval_unop := Cminor.eval_unop. -Definition eval_binop (op: binary_operation) - (arg1 arg2: val) (m: mem): option val := - match op, arg1, arg2 with - | Cminor.Ocmp c, Vptr b1 n1, Vptr b2 n2 => - if Mem.valid_pointer m b1 (Int.signed n1) - && Mem.valid_pointer m b2 (Int.signed n2) - then Cminor.eval_binop op arg1 arg2 - else None - | _, _, _ => - Cminor.eval_binop op arg1 arg2 - end. +Definition eval_binop := Cminor.eval_binop. (** Allocation of local variables at function entry. Each variable is bound to the reference to a fresh block of the appropriate size. *) diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 87dfc877..f1f7c0ac 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -199,8 +199,9 @@ Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) := Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_cmp ty1 ty2 with - | cmp_case_iiu => OK (Ebinop (Ocmpu c) e1 e2) - | cmp_case_ipip => OK (Ebinop (Ocmp c) e1 e2) + | cmp_case_ii Signed => OK (Ebinop (Ocmp c) e1 e2) + | cmp_case_ii Unsigned => OK (Ebinop (Ocmpu c) e1 e2) + | cmp_case_pp => OK (Ebinop (Ocmpu c) e1 e2) | cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2) | cmp_case_if sg => OK (Ebinop (Ocmpf c) (make_floatofint e1 sg) e2) | cmp_case_fi sg => OK (Ebinop (Ocmpf c) e1 (make_floatofint e2 sg)) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 3f6aa62e..457f0d16 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -585,19 +585,21 @@ Lemma make_cmp_correct: Proof. intros until m. intro SEM. unfold make_cmp. functional inversion SEM; rewrite H0; intros. - (* iiu *) + (** ii Signed *) + inversion H8; eauto with cshm. + (* ii Unsigned *) inversion H8. eauto with cshm. - (* ipip int int *) + (* pp int int *) inversion H8. eauto with cshm. - (* ipip ptr ptr *) + (* pp ptr ptr *) inversion H10. eapply eval_Ebinop; eauto with cshm. simpl. rewrite H3. unfold eq_block. rewrite H9. auto. inversion H10. eapply eval_Ebinop; eauto with cshm. simpl. rewrite H3. unfold eq_block. rewrite H9. auto. - (* ipip ptr int *) + (* pp ptr int *) inversion H9. eapply eval_Ebinop; eauto with cshm. simpl. unfold eval_compare_null. rewrite H8. auto. - (* ipip int ptr *) + (* pp int ptr *) inversion H9. eapply eval_Ebinop; eauto with cshm. simpl. unfold eval_compare_null. rewrite H8. auto. (* ff *) diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 8560d5e6..a199f33e 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -893,8 +893,8 @@ Definition classify_shift (ty1: type) (ty2: type) := end. Inductive classify_cmp_cases : Type:= - | cmp_case_iiu (**r unsigned int, unsigned int *) - | cmp_case_ipip (**r int-or-pointer, int-or-pointer *) + | cmp_case_ii(s: signedness) (**r int, int *) + | cmp_case_pp (**r pointer, pointer *) | cmp_case_ff (**r float , float *) | cmp_case_if(s: signedness) (**r int, float *) | cmp_case_fi(s: signedness) (**r float, int *) @@ -902,15 +902,15 @@ Inductive classify_cmp_cases : Type:= Definition classify_cmp (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tint I32 Unsigned , Tint _ _ => cmp_case_iiu - | Tint _ _ , Tint I32 Unsigned => cmp_case_iiu - | Tint _ _ , Tint _ _ => cmp_case_ipip + | Tint I32 Unsigned , Tint _ _ => cmp_case_ii Unsigned + | Tint _ _ , Tint I32 Unsigned => cmp_case_ii Unsigned + | Tint _ _ , Tint _ _ => cmp_case_ii Signed | Tfloat _ , Tfloat _ => cmp_case_ff | Tint _ sg, Tfloat _ => cmp_case_if sg | Tfloat _, Tint _ sg => cmp_case_fi sg - | Tpointer _ , Tpointer _ => cmp_case_ipip - | Tpointer _ , Tint _ _ => cmp_case_ipip - | Tint _ _, Tpointer _ => cmp_case_ipip + | Tpointer _ , Tpointer _ => cmp_case_pp + | Tpointer _ , Tint _ _ => cmp_case_pp + | Tint _ _, Tpointer _ => cmp_case_pp | _ , _ => cmp_default end. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index e8f1f9f1..10206afc 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -336,13 +336,14 @@ Lemma sem_cmp_match: match_val v1 v1' -> match_val v2 v2' -> match_val v v'. Proof. +Opaque zeq. intros. unfold sem_cmp in *. - destruct (classify_cmp ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. + destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval. destruct (Int.eq n Int.zero); try discriminate. unfold sem_cmp_mismatch in *. destruct c; inv H3; inv H2; constructor. destruct (Int.eq n Int.zero); try discriminate. unfold sem_cmp_mismatch in *. destruct c; inv H2; inv H1; constructor. - rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.signed ofs)) in H4. discriminate. + rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. discriminate. Qed. Lemma sem_binary_match: -- cgit