From 513489eb97c2b99f5ad901a0f26b493e99bbec1a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 2 Mar 2016 10:35:21 +0100 Subject: Make casts of pointers to _Bool semantically well defined (again). In compCert 2.5 the semantics of pointer comparisons against the NULL pointer was made more accurate by making it undefined if the pointer is invalid (outside bounds). Technical difficulties prevented this change from being propagated to the semantics of casts from pointer types to the _Bool type, which involves an implicit pointer comparison against NULL. Hence, this kind of casts was temporarily given undefined semantics. This commit makes pointer-to-_Bool casts semantically defined (again), provided the pointer is valid. This reinstates the equivalence between casts to _Bool and comparisons != 0. The technical difficulties mentioned above came from the translation of assignments in a value context in the SimplExpr pass. The pass was lightly modified to work around the issue. --- cfrontend/Ctyping.v | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'cfrontend/Ctyping.v') diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index aa320f20..f59fb396 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -1370,7 +1370,7 @@ Qed. Hint Resolve pres_cast_int_int: ty. Lemma pres_sem_cast: - forall v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 = Some v2 -> wt_val v2 ty2. + forall m v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 m = Some v2 -> wt_val v2 ty2. Proof. unfold sem_cast, classify_cast; induction 1; simpl; intros; DestructCases; auto with ty. - constructor. apply (pres_cast_int_int I8 s). @@ -1385,7 +1385,10 @@ Proof. - constructor. apply (pres_cast_int_int I8 s). - constructor. apply (pres_cast_int_int I16 s). - destruct (Float32.cmp Ceq f Float32.zero); auto with ty. +- constructor. reflexivity. - destruct (Int.eq n Int.zero); auto with ty. +- constructor. reflexivity. +- constructor. reflexivity. Qed. Lemma pres_sem_binarith: @@ -1394,7 +1397,7 @@ Lemma pres_sem_binarith: (sem_long: signedness -> int64 -> int64 -> option val) (sem_float: float -> float -> option val) (sem_single: float32 -> float32 -> option val) - v1 ty1 v2 ty2 v ty msg, + v1 ty1 v2 ty2 m v ty msg, (forall sg n1 n2, match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) -> (forall sg n1 n2, @@ -1403,14 +1406,14 @@ Lemma pres_sem_binarith: match sem_float n1 n2 with None | Some (Vfloat _) | Some Vundef => True | _ => False end) -> (forall n1 n2, match sem_single n1 n2 with None | Some (Vsingle _) | Some Vundef => True | _ => False end) -> - sem_binarith sem_int sem_long sem_float sem_single v1 ty1 v2 ty2 = Some v -> + sem_binarith sem_int sem_long sem_float sem_single v1 ty1 v2 ty2 m = Some v -> binarith_type ty1 ty2 msg = OK ty -> wt_val v ty. Proof with (try discriminate). intros. unfold sem_binarith, binarith_type in *. set (ty' := Cop.binarith_type (classify_binarith ty1 ty2)) in *. - destruct (sem_cast v1 ty1 ty') as [v1'|] eqn:CAST1... - destruct (sem_cast v2 ty2 ty') as [v2'|] eqn:CAST2... + destruct (sem_cast v1 ty1 ty' m) as [v1'|] eqn:CAST1... + destruct (sem_cast v2 ty2 ty' m) as [v2'|] eqn:CAST2... DestructCases. - specialize (H s i i0). rewrite H3 in H. destruct v; auto with ty; contradiction. @@ -1426,12 +1429,12 @@ Lemma pres_sem_binarith_int: forall (sem_int: signedness -> int -> int -> option val) (sem_long: signedness -> int64 -> int64 -> option val) - v1 ty1 v2 ty2 v ty msg, + v1 ty1 v2 ty2 m v ty msg, (forall sg n1 n2, match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) -> (forall sg n1 n2, match sem_long sg n1 n2 with None | Some (Vlong _) | Some Vundef => True | _ => False end) -> - sem_binarith sem_int sem_long (fun n1 n2 => None) (fun n1 n2 => None) v1 ty1 v2 ty2 = Some v -> + sem_binarith sem_int sem_long (fun n1 n2 => None) (fun n1 n2 => None) v1 ty1 v2 ty2 m = Some v -> binarith_int_type ty1 ty2 msg = OK ty -> wt_val v ty. Proof. -- cgit From 21613d7ad098ce4a080963aa4210ce208d24e9b3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:33:19 +0100 Subject: Update the proofs of the C front-end to the new linking framework. --- cfrontend/Ctyping.v | 80 ++++++++++++++--------------------------------------- 1 file changed, 21 insertions(+), 59 deletions(-) (limited to 'cfrontend/Ctyping.v') diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index aa320f20..6e2749bd 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -15,21 +15,11 @@ (** Typing rules and type-checking for the Compcert C language *) -Require Import Coqlib. Require Import String. -Require Import Maps. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import AST. -Require Import Ctypes. -Require Import Cop. -Require Import Csyntax. -Require Import Csem. -Require Import Errors. +Require Import Coqlib Maps Integers Floats Errors. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events. +Require Import Ctypes Cop Csyntax Csem. Local Open Scope error_monad_scope. @@ -911,8 +901,8 @@ Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fund Definition typecheck_program (p: program) : res program := let e := bind_globdef (PTree.empty _) p.(prog_defs) in let ce := p.(prog_comp_env) in - do defs <- transf_globdefs (retype_fundef ce e) (fun v => OK v) p.(prog_defs); - OK {| prog_defs := defs; + do tp <- transform_partial_program (retype_fundef ce e) p; + OK {| prog_defs := tp.(AST.prog_defs); prog_public := p.(prog_public); prog_main := p.(prog_main); prog_types := p.(prog_types); @@ -1325,32 +1315,29 @@ Theorem typecheck_program_sound: forall p p', typecheck_program p = OK p' -> wt_program p'. Proof. unfold typecheck_program; intros. monadInv H. - rename x into defs. + rename x into tp. constructor; simpl. set (ce := prog_comp_env p) in *. set (e := bind_globdef (PTree.empty type) (prog_defs p)) in *. - set (e' := bind_globdef (PTree.empty type) defs) in *. - assert (MATCH: - list_forall2 (match_globdef (fun f tf => retype_fundef ce e f = OK tf) (fun v tv => tv = v)) (prog_defs p) defs). - { - revert EQ; generalize (prog_defs p) defs. - induction l as [ | [id gd] l ]; intros l'; simpl; intros. - inv EQ. constructor. - destruct gd as [f | v]. - destruct (retype_fundef ce e f) as [tf|msg] eqn:R; monadInv EQ. - constructor; auto. constructor; auto. - monadInv EQ. constructor; auto. destruct v; constructor; auto. } + set (e' := bind_globdef (PTree.empty type) (AST.prog_defs tp)) in *. + assert (M: match_program (fun ctx f tf => retype_fundef ce e f = OK tf) eq p tp) + by (eapply match_transform_partial_program; eauto). + destruct M as (MATCH & _). simpl in MATCH. assert (ENVS: e' = e). - { unfold e, e'. revert MATCH; generalize (prog_defs p) defs (PTree.empty type). + { unfold e, e'. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp) (PTree.empty type). induction l as [ | [id gd] l ]; intros l' t M; inv M. - auto. inv H1; simpl; auto. replace (type_of_fundef f2) with (type_of_fundef f1); auto. - unfold retype_fundef in H4. destruct f1; monadInv H4; auto. monadInv EQ0; auto. + auto. + destruct b1 as [id' gd']; destruct H1; simpl in *. inv H0; simpl. + replace (type_of_fundef f2) with (type_of_fundef f1); auto. + unfold retype_fundef in H2. destruct f1; monadInv H2; auto. monadInv EQ0; auto. + inv H1. simpl. auto. } rewrite ENVS. - intros id f. revert MATCH; generalize (prog_defs p) defs. induction 1; simpl; intros. + intros id f. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp). + induction 1; simpl; intros. contradiction. - destruct H0; auto. subst b1; inv H. destruct f1; simpl in H2. - monadInv H2. eapply retype_function_sound; eauto. congruence. + destruct H0; auto. subst b1; inv H. simpl in H1. inv H1. + destruct f1; monadInv H4. eapply retype_function_sound; eauto. Qed. (** * Subject reduction *) @@ -2119,28 +2106,3 @@ Proof. Qed. End PRESERVATION. - - - - - - - - - - - - - - - - - - - - - - - - - -- cgit