diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cexec.v | 58 | ||||
-rw-r--r-- | cfrontend/Clight.v | 8 | ||||
-rw-r--r-- | cfrontend/ClightBigstep.v | 8 | ||||
-rw-r--r-- | cfrontend/Cop.v | 226 | ||||
-rw-r--r-- | cfrontend/Csem.v | 37 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 40 | ||||
-rw-r--r-- | cfrontend/Cstrategy.v | 80 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 17 | ||||
-rw-r--r-- | cfrontend/Initializers.v | 2 | ||||
-rw-r--r-- | cfrontend/Initializersproof.v | 24 | ||||
-rw-r--r-- | cfrontend/SimplExpr.v | 16 | ||||
-rw-r--r-- | cfrontend/SimplExprproof.v | 37 | ||||
-rw-r--r-- | cfrontend/SimplExprspec.v | 29 | ||||
-rw-r--r-- | cfrontend/SimplLocalsproof.v | 109 |
14 files changed, 368 insertions, 323 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 7e966ffe..00d77b00 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -645,11 +645,11 @@ Section EXPRS. Variable e: env. Variable w: world. -Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) : option (list val) := +Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) (m: mem) : option (list val) := match vtl, tl with | nil, Tnil => Some nil | (v1,t1)::vtl, Tcons t1' tl => - do v <- sem_cast v1 t1 t1'; do vl <- sem_cast_arguments vtl tl; Some(v::vl) + do v <- sem_cast v1 t1 t1' m; do vl <- sem_cast_arguments vtl tl m; Some(v::vl) | _, _ => None end. @@ -772,7 +772,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Ecast r1 ty => match is_val r1 with | Some(v1, ty1) => - do v <- sem_cast v1 ty1 ty; + do v <- sem_cast v1 ty1 ty m; topred (Rred "red_cast" (Eval v ty) m E0) | None => incontext (fun x => Ecast x ty) (step_expr RV r1 m) @@ -811,7 +811,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_loc l1, is_val r2 with | Some(b, ofs, ty1), Some(v2, ty2) => check type_eq ty1 ty; - do v <- sem_cast v2 ty2 ty1; + do v <- sem_cast v2 ty2 ty1 m; do w',t,m' <- do_assign_loc w ty1 m b ofs v; topred (Rred "red_assign" (Eval v ty) m' t) | _, _ => @@ -856,7 +856,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eparen r1 tycast ty => match is_val r1 with | Some (v1, ty1) => - do v <- sem_cast v1 ty1 tycast; + do v <- sem_cast v1 ty1 tycast m; topred (Rred "red_paren" (Eval v ty) m E0) | None => incontext (fun x => Eparen x tycast ty) (step_expr RV r1 m) @@ -867,7 +867,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match classify_fun tyf with | fun_case_f tyargs tyres cconv => do fd <- Genv.find_funct ge vf; - do vargs <- sem_cast_arguments vtl tyargs; + do vargs <- sem_cast_arguments vtl tyargs m; check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv); topred (Callred "red_call" fd vargs ty m) | _ => stuck @@ -879,7 +879,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Ebuiltin ef tyargs rargs ty => match is_val_list rargs with | Some vtl => - do vargs <- sem_cast_arguments vtl tyargs; + do vargs <- sem_cast_arguments vtl tyargs m; match do_external ef w vargs m with | None => stuck | Some(w',t,v,m') => topred (Rred "red_builtin" (Eval v ty) m' t) @@ -915,7 +915,7 @@ Inductive imm_safe_t: kind -> expr -> mem -> Prop := context RV to C -> imm_safe_t to (C r) m | imm_safe_t_callred: forall to C r m fd args ty, - callred ge r fd args ty -> + callred ge r m fd args ty -> context RV to C -> imm_safe_t to (C r) m. @@ -961,7 +961,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | 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 + exists v, sem_cast v1 ty1 ty m = Some v | Eseqand (Eval v1 ty1) r2 ty => exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => @@ -970,7 +970,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := 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' + ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w' | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty => exists t, exists v1, exists w', ty = ty1 /\ deref_loc ge ty1 m b ofs t v1 /\ possible_trace w t w' @@ -980,18 +980,18 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Ecomma (Eval v ty1) r2 ty => typeof r2 = ty | Eparen (Eval v1 ty1) tycast ty => - exists v, sem_cast v1 ty1 tycast = Some v + exists v, sem_cast v1 ty1 tycast m = Some v | Ecall (Eval vf tyf) rargs ty => exprlist_all_values rargs -> exists tyargs tyres cconv fd vl, classify_fun tyf = fun_case_f tyargs tyres cconv /\ Genv.find_funct ge vf = Some fd - /\ cast_arguments rargs tyargs vl + /\ cast_arguments m rargs tyargs vl /\ type_of_fundef fd = Tfunction tyargs tyres cconv | Ebuiltin ef tyargs rargs ty => exprlist_all_values rargs -> exists vargs t vres m' w', - cast_arguments rargs tyargs vargs + cast_arguments m rargs tyargs vargs /\ external_call ef ge vargs m t vres m' /\ possible_trace w t w' | _ => True @@ -1028,7 +1028,7 @@ Qed. Lemma callred_invert: forall r fd args ty m, - callred ge r fd args ty -> + callred ge r m fd args ty -> invert_expr_prop r m. Proof. intros. inv H. simpl. @@ -1124,7 +1124,7 @@ Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop := match k, rd with | LV, Lred _ l' m' => lred ge e a m l' m' | RV, Rred _ r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w' - | RV, Callred _ fd args tyres m' => callred ge a fd args tyres /\ m' = m + | RV, Callred _ fd args tyres m' => callred ge a m fd args tyres /\ m' = m | LV, Stuckred => ~imm_safe_t k a m | RV, Stuckred => ~imm_safe_t k a m | _, _ => False @@ -1152,10 +1152,10 @@ Ltac monadInv := end. Lemma sem_cast_arguments_sound: - forall rargs vtl tyargs vargs, + forall m rargs vtl tyargs vargs, is_val_list rargs = Some vtl -> - sem_cast_arguments vtl tyargs = Some vargs -> - cast_arguments rargs tyargs vargs. + sem_cast_arguments vtl tyargs m = Some vargs -> + cast_arguments m rargs tyargs vargs. Proof. induction rargs; simpl; intros. inv H. destruct tyargs; simpl in H0; inv H0. constructor. @@ -1164,9 +1164,9 @@ Proof. Qed. Lemma sem_cast_arguments_complete: - forall al tyl vl, - cast_arguments al tyl vl -> - exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl. + forall m al tyl vl, + cast_arguments m al tyl vl -> + exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl m = Some vl. Proof. induction 1. exists (@nil (val * type)); auto. @@ -1396,7 +1396,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* cast *) destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (sem_cast v ty' ty) as [v'|] eqn:?... + destruct (sem_cast v ty' ty m) as [v'|] eqn:?... apply topred_ok; auto. split. apply red_cast; 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; rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). (* top *) destruct (type_eq ty1 ty)... subst ty1. - destruct (sem_cast v2 ty2 ty) as [v|] eqn:?... + destruct (sem_cast v2 ty2 ty m) as [v|] eqn:?... destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|] eqn:?. exploit do_assign_loc_sound; eauto. intros [P Q]. apply topred_ok; auto. split. apply red_assign; auto. exists w'; auto. @@ -1478,7 +1478,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* top *) destruct (classify_fun tyf) as [tyargs tyres cconv|] eqn:?... destruct (Genv.find_funct ge vf) as [fd|] eqn:?... - destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... + destruct (sem_cast_arguments vtl tyargs m) as [vargs|] eqn:?... destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))... apply topred_ok; auto. red. split; auto. eapply red_call; eauto. eapply sem_cast_arguments_sound; eauto. @@ -1494,7 +1494,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct (is_val_list rargs) as [vtl | ] eqn:?. exploit is_val_list_all_values; eauto. intros ALLVAL. (* top *) - destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... + destruct (sem_cast_arguments vtl tyargs m) as [vargs|] eqn:?... destruct (do_external ef w vargs m) as [[[[? ?] v] m'] | ] eqn:?... exploit do_ef_external_sound; eauto. intros [EC PT]. apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto. @@ -1514,7 +1514,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* paren *) destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (sem_cast v ty' tycast) as [v'|] eqn:?... + destruct (sem_cast v ty' tycast m) as [v'|] eqn:?... apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1607,7 +1607,7 @@ Qed. Lemma callred_topred: forall a fd args ty m, - callred ge a fd args ty -> + callred ge a m fd args ty -> exists rule, step_expr RV a m = topred (Callred rule fd args ty m). Proof. induction 1; simpl. @@ -1961,7 +1961,7 @@ Definition do_step (w: world) (s: state) : list transition := 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) | Kreturn k => - do v' <- sem_cast v ty f.(fn_return); + do v' <- sem_cast v ty f.(fn_return) m; do m' <- Mem.free_list m (blocks_of_env ge e); ret "step_return_2" (Returnstate v' (call_cont k) m') | Kswitch1 sl k => @@ -2165,7 +2165,7 @@ Proof with (unfold ret; eauto with coqlib). apply extensionality; auto. (* callred *) unfold do_step; rewrite NOTVAL. - exploit callred_topred; eauto. instantiate (1 := m). instantiate (1 := w). instantiate (1 := e). + exploit callred_topred; eauto. instantiate (1 := w). instantiate (1 := e). intros (rule & STEP). exists rule. change (TR rule E0 (Callstate fd vargs (Kcall f e C ty k) m)) with (expr_final_state f k e (C, Callred rule fd vargs ty m)). apply in_map. diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 8722da69..086f4654 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -412,7 +412,7 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr (Ebinop op a1 a2 ty) v | eval_Ecast: forall a ty v1 v, eval_expr a v1 -> - sem_cast v1 (typeof a) ty = Some v -> + sem_cast v1 (typeof a) ty m = Some v -> eval_expr (Ecast a ty) v | eval_Esizeof: forall ty1 ty, eval_expr (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) @@ -464,7 +464,7 @@ Inductive eval_exprlist: list expr -> typelist -> list val -> Prop := eval_exprlist nil Tnil nil | eval_Econs: forall a bl ty tyl v1 v2 vl, eval_expr a v1 -> - sem_cast v1 (typeof a) ty = Some v2 -> + sem_cast v1 (typeof a) ty m = Some v2 -> eval_exprlist bl tyl vl -> eval_exprlist (a :: bl) (Tcons ty tyl) (v2 :: vl). @@ -580,7 +580,7 @@ Inductive step: state -> trace -> state -> Prop := | step_assign: forall f a1 a2 k e le m loc ofs v2 v m', eval_lvalue e le m a1 loc ofs -> eval_expr e le m a2 v2 -> - sem_cast v2 (typeof a2) (typeof a1) = Some v -> + sem_cast v2 (typeof a2) (typeof a1) m = Some v -> assign_loc ge (typeof a1) m loc ofs v m' -> step (State f (Sassign a1 a2) k e le m) E0 (State f Sskip k e le m') @@ -647,7 +647,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (Returnstate Vundef (call_cont k) m') | step_return_1: forall f a k e le m v v' m', eval_expr e le m a v -> - sem_cast v (typeof a) f.(fn_return) = Some v' -> + sem_cast v (typeof a) f.(fn_return) m = Some v' -> Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn (Some a)) k e le m) E0 (Returnstate v' (call_cont k) m') diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index ee653d50..92457586 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -60,11 +60,11 @@ Definition outcome_switch (out: outcome) : outcome := | o => o end. -Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := +Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem): Prop := match out, t with | Out_normal, Tvoid => v = Vundef | Out_return None, Tvoid => v = Vundef - | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t = Some v + | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t m = Some v | _, _ => False end. @@ -81,7 +81,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> | exec_Sassign: forall e le m a1 a2 loc ofs v2 v m', eval_lvalue ge e le m a1 loc ofs -> eval_expr ge e le m a2 v2 -> - sem_cast v2 (typeof a2) (typeof a1) = Some v -> + sem_cast v2 (typeof a2) (typeof a1) m = Some v -> assign_loc ge (typeof a1) m loc ofs v m' -> exec_stmt e le m (Sassign a1 a2) E0 le m' Out_normal @@ -168,7 +168,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> bind_parameters ge e m1 f.(fn_params) vargs m2 -> exec_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t le m3 out -> - outcome_result_value out f.(fn_return) vres -> + outcome_result_value out f.(fn_return) vres m3 -> Mem.free_list m3 (blocks_of_env ge e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres | eval_funcall_external: forall m ef targs tres cconv vargs t vres m', diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index b4784028..8b3421e8 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -130,7 +130,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases := | _, _ => cast_case_default end. -(** Semantics of casts. [sem_cast v1 t1 t2 = Some v2] if value [v1], +(** Semantics of casts. [sem_cast v1 t1 t2 m = Some v2] if value [v1], viewed with static type [t1], can be converted to type [t2], resulting in value [v2]. *) @@ -198,7 +198,7 @@ Definition cast_single_long (si : signedness) (f: float32) : option int64 := | Unsigned => Float32.to_longu f end. -Definition sem_cast (v: val) (t1 t2: type) : option val := +Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := match classify_cast t1 t2 with | cast_case_neutral => match v with @@ -273,6 +273,7 @@ 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 b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vone else None | _ => None end | cast_case_l2l => @@ -586,13 +587,13 @@ Definition sem_binarith (sem_long: signedness -> int64 -> int64 -> option val) (sem_float: float -> float -> option val) (sem_single: float32 -> float32 -> option val) - (v1: val) (t1: type) (v2: val) (t2: type) : option val := + (v1: val) (t1: type) (v2: val) (t2: type) (m: mem): option val := let c := classify_binarith t1 t2 in let t := binarith_type c in - match sem_cast v1 t1 t with + match sem_cast v1 t1 t m with | None => None | Some v1' => - match sem_cast v2 t2 t with + match sem_cast v2 t2 t m with | None => None | Some v2' => match c with @@ -637,7 +638,7 @@ Definition classify_add (ty1: type) (ty2: type) := | _, _ => add_default end. -Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m: mem): option val := match classify_add t1 t2 with | add_case_pi ty => (**r pointer plus integer *) match v1,v2 with @@ -671,7 +672,7 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (fun sg n1 n2 => Some(Vlong(Int64.add n1 n2))) (fun n1 n2 => Some(Vfloat(Float.add n1 n2))) (fun n1 n2 => Some(Vsingle(Float32.add n1 n2))) - v1 t1 v2 t2 + v1 t1 v2 t2 m end. (** *** Subtraction *) @@ -690,7 +691,7 @@ Definition classify_sub (ty1: type) (ty2: type) := | _, _ => sub_default end. -Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m:mem): option val := match classify_sub t1 t2 with | sub_case_pi ty => (**r pointer minus integer *) match v1,v2 with @@ -722,20 +723,20 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (fun sg n1 n2 => Some(Vlong(Int64.sub n1 n2))) (fun n1 n2 => Some(Vfloat(Float.sub n1 n2))) (fun n1 n2 => Some(Vsingle(Float32.sub n1 n2))) - v1 t1 v2 t2 + v1 t1 v2 t2 m end. (** *** Multiplication, division, modulus *) -Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => Some(Vint(Int.mul n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.mul n1 n2))) (fun n1 n2 => Some(Vfloat(Float.mul n1 n2))) (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2))) - v1 t1 v2 t2. + v1 t1 v2 t2 m. -Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => match sg with @@ -759,9 +760,9 @@ Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := end) (fun n1 n2 => Some(Vfloat(Float.div n1 n2))) (fun n1 n2 => Some(Vsingle(Float32.div n1 n2))) - v1 t1 v2 t2. + v1 t1 v2 t2 m. -Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => match sg with @@ -785,31 +786,31 @@ Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := end) (fun n1 n2 => None) (fun n1 n2 => None) - v1 t1 v2 t2. + v1 t1 v2 t2 m. -Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => Some(Vint(Int.and n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.and n1 n2))) (fun n1 n2 => None) (fun n1 n2 => None) - v1 t1 v2 t2. + v1 t1 v2 t2 m. -Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => Some(Vint(Int.or n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.or n1 n2))) (fun n1 n2 => None) (fun n1 n2 => None) - v1 t1 v2 t2. + v1 t1 v2 t2 m. -Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => Some(Vint(Int.xor n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.xor n1 n2))) (fun n1 n2 => None) (fun n1 n2 => None) - v1 t1 v2 t2. + v1 t1 v2 t2 m. (** *** Shifts *) @@ -931,7 +932,7 @@ Definition sem_cmp (c:comparison) Some(Val.of_bool(Float.cmp c n1 n2))) (fun n1 n2 => Some(Val.of_bool(Float32.cmp c n1 n2))) - v1 t1 v2 t2 + v1 t1 v2 t2 m end. (** ** Function applications *) @@ -988,14 +989,14 @@ Definition sem_binary_operation (v1: val) (t1: type) (v2: val) (t2:type) (m: mem): option val := match op with - | Oadd => sem_add cenv v1 t1 v2 t2 - | Osub => sem_sub cenv v1 t1 v2 t2 - | Omul => sem_mul v1 t1 v2 t2 - | Omod => sem_mod v1 t1 v2 t2 - | Odiv => sem_div v1 t1 v2 t2 - | Oand => sem_and v1 t1 v2 t2 - | Oor => sem_or v1 t1 v2 t2 - | Oxor => sem_xor v1 t1 v2 t2 + | Oadd => sem_add cenv v1 t1 v2 t2 m + | Osub => sem_sub cenv v1 t1 v2 t2 m + | Omul => sem_mul v1 t1 v2 t2 m + | Omod => sem_mod v1 t1 v2 t2 m + | Odiv => sem_div v1 t1 v2 t2 m + | Oand => sem_and v1 t1 v2 t2 m + | Oor => sem_or v1 t1 v2 t2 m + | Oxor => sem_xor v1 t1 v2 t2 m | Oshl => sem_shl v1 t1 v2 t2 | Oshr => sem_shr v1 t1 v2 t2 | Oeq => sem_cmp Ceq v1 t1 v2 t2 m @@ -1006,10 +1007,10 @@ Definition sem_binary_operation | Oge => sem_cmp Cge v1 t1 v2 t2 m end. -Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) := +Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) (m: mem) := match id with - | Incr => sem_add cenv v ty (Vint Int.one) type_int32s - | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s + | Incr => sem_add cenv v ty (Vint Int.one) type_int32s m + | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s m end. Definition incrdecr_type (ty: type) := @@ -1074,11 +1075,11 @@ Ltac TrivialInject := | _ => idtac end. -Lemma sem_cast_inject: +Lemma sem_cast_inj: forall v1 ty1 ty v tv1, - sem_cast v1 ty1 ty = Some v -> + sem_cast v1 ty1 ty m = Some v -> Val.inject f v1 tv1 -> - exists tv, sem_cast tv1 ty1 ty = Some tv /\ Val.inject f v tv. + exists tv, sem_cast tv1 ty1 ty m'= Some tv /\ Val.inject f v tv. Proof. unfold sem_cast; intros; destruct (classify_cast ty1 ty); inv H0; inv H; TrivialInject. @@ -1087,6 +1088,8 @@ Proof. - destruct (cast_single_int si2 f0); inv H1; TrivialInject. - destruct (cast_float_long si2 f0); inv H1; TrivialInject. - destruct (cast_single_long si2 f0); inv H1; TrivialInject. +- destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VALID; inv H2. + erewrite weak_valid_pointer_inj by eauto. TrivialInject. - destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto. - destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto. - econstructor; eauto. @@ -1119,13 +1122,13 @@ Definition optval_self_injects (ov: option val) : Prop := Remark sem_binarith_inject: forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2', - sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 = Some v -> + sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 m = Some v -> Val.inject f v1 v1' -> Val.inject f v2 v2' -> (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) -> (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) -> (forall n1 n2, optval_self_injects (sem_float n1 n2)) -> (forall n1 n2, optval_self_injects (sem_single n1 n2)) -> - exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ Val.inject f v v'. + exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 m' = Some v' /\ Val.inject f v v'. Proof. intros. assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> Val.inject f v v). @@ -1135,10 +1138,10 @@ Proof. unfold sem_binarith in *. set (c := classify_binarith t1 t2) in *. set (t := binarith_type c) in *. - destruct (sem_cast v1 t1 t) as [w1|] eqn:C1; try discriminate. - destruct (sem_cast v2 t2 t) as [w2|] eqn:C2; try discriminate. - exploit (sem_cast_inject v1); eauto. intros (w1' & C1' & INJ1). - exploit (sem_cast_inject v2); eauto. intros (w2' & C2' & INJ2). + destruct (sem_cast v1 t1 t m) as [w1|] eqn:C1; try discriminate. + destruct (sem_cast v2 t2 t m) as [w2|] eqn:C2; try discriminate. + exploit (sem_cast_inj v1); eauto. intros (w1' & C1' & INJ1). + exploit (sem_cast_inj v2); eauto. intros (w2' & C2' & INJ2). rewrite C1'; rewrite C2'. destruct c; inv INJ1; inv INJ2; discriminate || eauto. Qed. @@ -1282,6 +1285,17 @@ Qed. End GENERIC_INJECTION. +Lemma sem_cast_inject: + forall f v1 ty1 ty m v tv1 tm, + sem_cast v1 ty1 ty m = Some v -> + Val.inject f v1 tv1 -> + Mem.inject f m tm -> + exists tv, sem_cast tv1 ty1 ty tm = Some tv /\ Val.inject f v tv. +Proof. + intros. eapply sem_cast_inj; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. +Qed. + Lemma sem_unary_operation_inject: forall f m m' op v1 ty1 v tv1, sem_unary_operation op v1 ty1 m = Some v -> @@ -1321,20 +1335,16 @@ Qed. (** * Some properties of operator semantics *) (** This section collects some common-sense properties about the type - classification and semantic functions above. These properties are - not used in the CompCert semantics preservation proofs, but increase + classification and semantic functions above. Some properties are used + in the CompCert semantics preservation proofs. Others are not, but increase confidence in the specification and its relation with the ISO C99 standard. *) (** Relation between Boolean value and casting to [_Bool] type. *) Lemma cast_bool_bool_val: 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. + sem_cast v t (Tint IBool Signed noattr) m = + match bool_val v t m with None => None | Some b => Some(Val.of_bool b) end. intros. assert (A: classify_bool t = match t with @@ -1360,8 +1370,11 @@ Proof. destruct (Float32.cmp Ceq f0 Float32.zero); auto. destruct f; auto. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. Qed. (** Relation between Boolean value and Boolean negation. *) @@ -1376,6 +1389,119 @@ Proof. destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. Qed. +(** Properties of values obtained by casting to a given type. *) + +Inductive val_casted: val -> type -> Prop := + | val_casted_int: forall sz si attr n, + cast_int_int sz si n = n -> + val_casted (Vint n) (Tint sz si attr) + | val_casted_float: forall attr n, + val_casted (Vfloat n) (Tfloat F64 attr) + | val_casted_single: forall attr n, + val_casted (Vsingle n) (Tfloat F32 attr) + | val_casted_long: forall si attr n, + val_casted (Vlong n) (Tlong si attr) + | val_casted_ptr_ptr: forall b ofs ty attr, + val_casted (Vptr b ofs) (Tpointer ty attr) + | val_casted_int_ptr: forall n ty attr, + val_casted (Vint n) (Tpointer ty attr) + | val_casted_ptr_int: forall b ofs si attr, + val_casted (Vptr b ofs) (Tint I32 si attr) + | val_casted_struct: forall id attr b ofs, + val_casted (Vptr b ofs) (Tstruct id attr) + | val_casted_union: forall id attr b ofs, + val_casted (Vptr b ofs) (Tunion id attr) + | val_casted_void: forall v, + val_casted v Tvoid. + +Remark cast_int_int_idem: + forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i. +Proof. + intros. destruct sz; simpl; auto. + destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence. + destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence. + destruct (Int.eq i Int.zero); auto. +Qed. + +Lemma cast_val_is_casted: + forall v ty ty' v' m, sem_cast v ty ty' m = Some v' -> val_casted v' ty'. +Proof. + unfold sem_cast; intros. destruct ty'; simpl in *. +- (* void *) + constructor. +- (* int *) + destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H. + constructor. apply (cast_int_int_idem I8 s). + constructor. apply (cast_int_int_idem I8 s). + destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). + destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). + constructor. apply (cast_int_int_idem I16 s). + constructor. apply (cast_int_int_idem I16 s). + destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). + destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). + constructor. auto. + constructor. + constructor. auto. + destruct (cast_single_int s f); inv H1. constructor. auto. + destruct (cast_float_int s f); inv H1. constructor; auto. + constructor; auto. + constructor. + constructor; auto. + constructor. + constructor; auto. + constructor. + constructor. simpl. destruct (Int.eq i0 Int.zero); auto. + constructor. simpl. destruct (Int64.eq i Int64.zero); auto. + 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. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. + constructor. simpl. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. + constructor. simpl. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. +- (* long *) + destruct ty; try (destruct f); try discriminate. + destruct v; inv H. constructor. + destruct v; inv H. constructor. + destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor. + destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor. + destruct v; inv H. constructor. + destruct v; inv H. constructor. + destruct v; inv H. constructor. +- (* float *) + destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor. +- (* pointer *) + destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor. +- (* array (impossible case) *) + discriminate. +- (* function (impossible case) *) + discriminate. +- (* structs *) + destruct ty; try discriminate; destruct v; try discriminate. + destruct (ident_eq i0 i); inv H; constructor. +- (* unions *) + destruct ty; try discriminate; destruct v; try discriminate. + destruct (ident_eq i0 i); inv H; constructor. +Qed. + +(** As a consequence, casting twice is equivalent to casting once. *) + +Lemma cast_val_casted: + forall v ty m, val_casted v ty -> sem_cast v ty ty m = Some v. +Proof. + intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto. + destruct sz; congruence. + unfold proj_sumbool; repeat rewrite dec_eq_true; auto. + unfold proj_sumbool; repeat rewrite dec_eq_true; auto. +Qed. + +Lemma cast_idempotent: + forall v ty ty' v' m, sem_cast v ty ty' m = Some v' -> sem_cast v' ty' ty' m = Some v'. +Proof. + intros. apply cast_val_casted. eapply cast_val_is_casted; eauto. +Qed. + (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *) Module ArithConv. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 539b6826..30e6200d 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -187,12 +187,12 @@ Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement := (** Extract the values from a list of function arguments *) -Inductive cast_arguments: exprlist -> typelist -> list val -> Prop := +Inductive cast_arguments (m: mem): exprlist -> typelist -> list val -> Prop := | cast_args_nil: - cast_arguments Enil Tnil nil + cast_arguments m Enil Tnil nil | cast_args_cons: forall v ty el targ1 targs v1 vl, - sem_cast v ty targ1 = Some v1 -> cast_arguments el targs vl -> - cast_arguments (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl). + sem_cast v ty targ1 m = Some v1 -> cast_arguments m el targs vl -> + cast_arguments m (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl). (** ** Reduction semantics for expressions *) @@ -249,7 +249,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty) m E0 (Eval v ty) m | red_cast: forall ty v1 ty1 m v, - sem_cast v1 ty1 ty = Some v -> + sem_cast v1 ty1 ty m = Some v -> rred (Ecast (Eval v1 ty1) ty) m E0 (Eval v ty) m | red_seqand_true: forall v1 ty1 r2 ty m, @@ -279,7 +279,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Ealignof ty1 ty) m E0 (Eval (Vint (Int.repr (alignof ge ty1))) ty) m | red_assign: forall b ofs ty1 v2 ty2 m v t m', - sem_cast v2 ty2 ty1 = Some v -> + sem_cast v2 ty2 ty1 m = Some v -> assign_loc ty1 m b ofs v t m' -> rred (Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty1) m t (Eval v ty1) m' @@ -303,11 +303,11 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Ecomma (Eval v ty1) r2 ty) m E0 r2 m | red_paren: forall v1 ty1 ty2 ty m v, - sem_cast v1 ty1 ty2 = Some v -> + sem_cast v1 ty1 ty2 m = Some v -> rred (Eparen (Eval v1 ty1) ty2 ty) m E0 (Eval v ty) m | red_builtin: forall ef tyargs el ty m vargs t vres m', - cast_arguments el tyargs vargs -> + cast_arguments m el tyargs vargs -> external_call ef ge vargs m t vres m' -> rred (Ebuiltin ef tyargs el ty) m t (Eval vres ty) m'. @@ -316,13 +316,13 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := (** Head reduction for function calls. (More exactly, identification of function calls that can reduce.) *) -Inductive callred: expr -> fundef -> list val -> type -> Prop := - | red_call: forall vf tyf tyargs tyres cconv el ty fd vargs, +Inductive callred: expr -> mem -> fundef -> list val -> type -> Prop := + | red_call: forall vf tyf m tyargs tyres cconv el ty fd vargs, Genv.find_funct ge vf = Some fd -> - cast_arguments el tyargs vargs -> + cast_arguments m el tyargs vargs -> type_of_fundef fd = Tfunction tyargs tyres cconv -> classify_fun tyf = fun_case_f tyargs tyres cconv -> - callred (Ecall (Eval vf tyf) el ty) + callred (Ecall (Eval vf tyf) el ty) m fd vargs ty. (** Reduction contexts. In accordance with C's nondeterministic semantics, @@ -429,17 +429,14 @@ Inductive imm_safe: kind -> expr -> mem -> Prop := context RV to C -> imm_safe to (C e) m | imm_safe_callred: forall to C e m fd args ty, - callred e fd args ty -> + callred e m fd args ty -> context RV to C -> imm_safe to (C e) m. -(* An expression is not stuck if none of the potential redexes contained within - is immediately stuck. *) -(* Definition not_stuck (e: expr) (m: mem) : Prop := forall k C e' , - context k RV C -> e = C e' -> not_imm_stuck k e' m. -*) + context k RV C -> e = C e' -> imm_safe k e' m. + End EXPR. (** ** Transition semantics. *) @@ -597,7 +594,7 @@ Inductive estep: state -> trace -> state -> Prop := t (ExprState f (C a') k e m') | step_call: forall C f a k e m fd vargs ty, - callred a fd vargs ty -> + callred a m fd vargs ty -> context RV RV C -> estep (ExprState f (C a) k e m) E0 (Callstate fd vargs (Kcall f e C ty k) m) @@ -709,7 +706,7 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Sreturn (Some x)) k e m) E0 (ExprState f x (Kreturn k) e m) | step_return_2: forall f v1 ty k e m v2 m', - sem_cast v1 ty f.(fn_return) = Some v2 -> + sem_cast v1 ty f.(fn_return) m = Some v2 -> Mem.free_list m (blocks_of_env e) = Some m' -> sstep (ExprState f (Eval v1 ty) (Kreturn k) e m) E0 (Returnstate v2 (call_cont k) m') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index e25e21c9..4f067fad 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -255,7 +255,7 @@ Lemma make_cast_correct: forall e le m a b v ty1 ty2 v', make_cast ty1 ty2 a = OK b -> eval_expr ge e le m a v -> - sem_cast v ty1 ty2 = Some v' -> + sem_cast v ty1 ty2 m = Some v' -> eval_expr ge e le m b v'. Proof. intros. unfold make_cast, sem_cast in *; @@ -302,6 +302,12 @@ Proof. econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. destruct (Int.eq i Int.zero); auto. + (* pointer -> bool *) + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:VALID; inv H2. + econstructor; eauto with cshm. + simpl. unfold Val.cmpu. simpl. rewrite Int.eq_true. + unfold Mem.weak_valid_pointer in VALID; rewrite VALID. + auto. (* struct *) destruct (ident_eq id1 id2); inv H2; auto. (* union *) @@ -394,6 +400,16 @@ Qed. Definition binary_constructor_correct (make: expr -> type -> expr -> type -> res expr) + (sem: val -> type -> val -> type -> mem -> option val): Prop := + forall a tya b tyb c va vb v e le m, + sem va tya vb tyb m = Some v -> + make a tya b tyb = OK c -> + eval_expr ge e le m a va -> + eval_expr ge e le m b vb -> + eval_expr ge e le m c v. + +Definition shift_constructor_correct + (make: expr -> type -> expr -> type -> res expr) (sem: val -> type -> val -> type -> option val): Prop := forall a tya b tyb c va vb v e le m, sem va tya vb tyb = Some v -> @@ -433,8 +449,8 @@ Proof. set (cls := classify_binarith tya tyb) in *. set (ty := binarith_type cls) in *. monadInv MAKE. - destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. - destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. + destruct (sem_cast va tya ty m) as [va'|] eqn:Ca; try discriminate. + destruct (sem_cast vb tyb ty m) as [vb'|] eqn:Cb; try discriminate. exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. @@ -456,8 +472,8 @@ Proof. set (cls := classify_binarith tya tyb) in *. set (ty := binarith_type cls) in *. monadInv MAKE. - destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. - destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. + destruct (sem_cast va tya ty m) as [va'|] eqn:Ca; try discriminate. + destruct (sem_cast vb tyb ty m) as [vb'|] eqn:Cb; try discriminate. exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. @@ -578,7 +594,7 @@ Proof. apply Int64.unsigned_repr. comput Int64.max_unsigned; omega. Qed. -Lemma make_shl_correct: binary_constructor_correct make_shl sem_shl. +Lemma make_shl_correct: shift_constructor_correct make_shl sem_shl. Proof. red; unfold make_shl, sem_shl, sem_shift; intros until m; intros SEM MAKE EV1 EV2; @@ -597,7 +613,7 @@ Proof. unfold Int64.shl', Int64.shl. rewrite small_shift_amount_3; auto. Qed. -Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr. +Lemma make_shr_correct: shift_constructor_correct make_shr sem_shr. Proof. red; unfold make_shr, sem_shr, sem_shift; intros until m; intros SEM MAKE EV1 EV2; @@ -619,15 +635,9 @@ Proof. unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto. Qed. -Lemma make_cmp_correct: - forall cmp a tya b tyb c va vb v e le m, - sem_cmp cmp va tya vb tyb m = Some v -> - make_cmp cmp a tya b tyb = OK c -> - eval_expr ge e le m a va -> - eval_expr ge e le m b vb -> - eval_expr ge e le m c v. +Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp). Proof. - unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2; + red; unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_cmp tya tyb). - inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; simpl in SEM; inv SEM. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index b3cbacca..2650e0a8 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -130,7 +130,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Ebinop op r1 r2 ty) v | esr_cast: forall ty r1 v1 v, eval_simple_rvalue r1 v1 -> - sem_cast v1 (typeof r1) ty = Some v -> + sem_cast v1 (typeof r1) ty m = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) @@ -141,7 +141,7 @@ Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop := | esrl_nil: eval_simple_list Enil Tnil nil | esrl_cons: forall r rl ty tyl v vl v', - eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty = Some v -> + eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty m = Some v -> eval_simple_list rl tyl vl -> eval_simple_list (Econs r rl) (Tcons ty tyl) (v :: vl). @@ -283,7 +283,7 @@ Inductive estep: state -> trace -> state -> Prop := leftcontext RV RV C -> eval_simple_lvalue e m l b ofs -> eval_simple_rvalue e m r v -> - sem_cast v (typeof r) (typeof l) = Some v' -> + sem_cast v (typeof r) (typeof l) m = Some v' -> assign_loc ge (typeof l) m b ofs v' t m' -> ty = typeof l -> estep (ExprState f (C (Eassign l r ty)) k e m) @@ -295,7 +295,7 @@ Inductive estep: state -> trace -> state -> Prop := deref_loc ge (typeof l) m b ofs t1 v1 -> eval_simple_rvalue e m r v2 -> sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m = Some v3 -> - sem_cast v3 tyres (typeof l) = Some v4 -> + sem_cast v3 tyres (typeof l) m = Some v4 -> assign_loc ge (typeof l) m b ofs v4 t2 m' -> ty = typeof l -> t = t1 ** t2 -> @@ -310,7 +310,7 @@ Inductive estep: state -> trace -> state -> Prop := match sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m with | None => True | Some v3 => - match sem_cast v3 tyres (typeof l) with + match sem_cast v3 tyres (typeof l) m with | None => True | Some v4 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v4 t2 m') end @@ -323,8 +323,8 @@ Inductive estep: state -> trace -> state -> Prop := leftcontext RV RV C -> eval_simple_lvalue e m l b ofs -> deref_loc ge ty m b ofs t1 v1 -> - sem_incrdecr ge id v1 ty = Some v2 -> - sem_cast v2 (incrdecr_type ty) ty = Some v3 -> + sem_incrdecr ge id v1 ty m = Some v2 -> + sem_cast v2 (incrdecr_type ty) ty m = Some v3 -> assign_loc ge ty m b ofs v3 t2 m' -> ty = typeof l -> t = t1 ** t2 -> @@ -335,10 +335,10 @@ Inductive estep: state -> trace -> state -> Prop := leftcontext RV RV C -> eval_simple_lvalue e m l b ofs -> deref_loc ge ty m b ofs t v1 -> - match sem_incrdecr ge id v1 ty with + match sem_incrdecr ge id v1 ty m with | None => True | Some v2 => - match sem_cast v2 (incrdecr_type ty) ty with + match sem_cast v2 (incrdecr_type ty) ty m with | None => True | Some v3 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v3 t2 m') end @@ -357,7 +357,7 @@ Inductive estep: state -> trace -> state -> Prop := | step_paren: forall f C r tycast ty k e m v1 v, leftcontext RV RV C -> eval_simple_rvalue e m r v1 -> - sem_cast v1 (typeof r) tycast = Some v -> + sem_cast v1 (typeof r) tycast m = Some v -> estep (ExprState f (C (Eparen r tycast ty)) k e m) E0 (ExprState f (C (Eval v ty)) k e m) @@ -472,7 +472,7 @@ Proof. Qed. Lemma callred_kind: - forall a fd args ty, callred ge a fd args ty -> expr_kind a = RV. + forall a m fd args ty, callred ge a m fd args ty -> expr_kind a = RV. Proof. induction 1; auto. Qed. @@ -540,7 +540,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | 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 + exists v, sem_cast v1 ty1 ty m = Some v | Eseqand (Eval v1 ty1) r2 ty => exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => @@ -549,7 +549,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := 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' + ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m' | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty => exists t, exists v1, ty = ty1 @@ -561,18 +561,18 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Ecomma (Eval v ty1) r2 ty => typeof r2 = ty | Eparen (Eval v1 ty1) ty2 ty => - exists v, sem_cast v1 ty1 ty2 = Some v + exists v, sem_cast v1 ty1 ty2 m = Some v | Ecall (Eval vf tyf) rargs ty => exprlist_all_values rargs -> exists tyargs tyres cconv fd vl, classify_fun tyf = fun_case_f tyargs tyres cconv /\ Genv.find_funct ge vf = Some fd - /\ cast_arguments rargs tyargs vl + /\ cast_arguments m rargs tyargs vl /\ type_of_fundef fd = Tfunction tyargs tyres cconv | Ebuiltin ef tyargs rargs ty => exprlist_all_values rargs -> exists vargs, exists t, exists vres, exists m', - cast_arguments rargs tyargs vargs + cast_arguments m rargs tyargs vargs /\ external_call ef ge vargs m t vres m' | _ => True end. @@ -608,7 +608,7 @@ Qed. Lemma callred_invert: forall r fd args ty m, - callred ge r fd args ty -> + callred ge r m fd args ty -> invert_expr_prop r m. Proof. intros. inv H. simpl. @@ -893,7 +893,7 @@ Inductive eval_simple_list': exprlist -> list val -> Prop := Lemma eval_simple_list_implies: forall rl tyl vl, eval_simple_list e m rl tyl vl -> - exists vl', cast_arguments (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'. + exists vl', cast_arguments m (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'. Proof. induction 1. exists (@nil val); split. constructor. constructor. @@ -905,7 +905,7 @@ Lemma can_eval_simple_list: forall rl vl, eval_simple_list' rl vl -> forall tyl vl', - cast_arguments (rval_list vl rl) tyl vl' -> + cast_arguments m (rval_list vl rl) tyl vl' -> eval_simple_list e m rl tyl vl'. Proof. induction 1; simpl; intros. @@ -1234,9 +1234,9 @@ Proof. left; apply step_rred; auto. econstructor; eauto. set (op := match id with Incr => Oadd | Decr => Osub end). assert (SEM: sem_binary_operation ge op v1 (typeof l) (Vint Int.one) type_int32s m = - sem_incrdecr ge id v1 (typeof l)). + sem_incrdecr ge id v1 (typeof l) m). destruct id; auto. - destruct (sem_incrdecr ge id v1 (typeof l)) as [v2|]. + destruct (sem_incrdecr ge id v1 (typeof l) m) as [v2|]. eapply star_left. left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto. econstructor; eauto. @@ -1329,7 +1329,7 @@ Proof. intros [v [E2 S2]]. exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]]. destruct (sem_binary_operation ge op v1 (typeof b1) v (typeof b2) m) as [v3|] eqn:?. - destruct (sem_cast v3 tyres (typeof b1)) as [v4|] eqn:?. + destruct (sem_cast v3 tyres (typeof b1) m) as [v4|] eqn:?. destruct (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')). destruct H2 as [t2 [m' D]]. econstructor; econstructor; eapply step_assignop; eauto. @@ -1343,8 +1343,8 @@ Proof. exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto. intros [b1 [ofs [E1 S1]]]. exploit safe_inv. eexact S1. eauto. simpl. intros [t [v1 [A B]]]. - destruct (sem_incrdecr ge id v1 ty) as [v2|] eqn:?. - destruct (sem_cast v2 (incrdecr_type ty) ty) as [v3|] eqn:?. + destruct (sem_incrdecr ge id v1 ty m) as [v2|] eqn:?. + destruct (sem_cast v2 (incrdecr_type ty) ty m) as [v3|] eqn:?. destruct (classic (exists t2, exists m', assign_loc ge ty m b1 ofs v3 t2 m')). destruct H0 as [t2 [m' D]]. econstructor; econstructor; eapply step_postincr; eauto. @@ -1498,7 +1498,7 @@ Proof. econstructor; econstructor; eauto. inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?. - destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?. + destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. @@ -1511,7 +1511,7 @@ Proof. (* assignop stuck *) exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?. - destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?. + destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. @@ -1526,8 +1526,8 @@ Proof. subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H. econstructor; econstructor; eauto. inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. - destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?. - destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?. + destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?. + destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. @@ -1539,8 +1539,8 @@ Proof. rewrite Heqo; auto. (* postincr stuck *) exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. - destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?. - destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?. + destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?. + destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. @@ -1641,11 +1641,11 @@ Definition outcome_switch (out: outcome) : outcome := | o => o end. -Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := +Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem) : Prop := match out, t with | Out_normal, Tvoid => v = Vundef | Out_return None, Tvoid => v = Vundef - | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty = Some v + | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty m = Some v | _, _ => False end. @@ -1697,7 +1697,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> 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 -> + sem_cast v2 (typeof a2) type_bool m'' = 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 -> @@ -1707,7 +1707,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> 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 -> + sem_cast v2 (typeof a2) type_bool m'' = 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 -> @@ -1717,7 +1717,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> 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 -> + sem_cast v' (typeof (if b then a2 else a3)) ty m'' = Some v -> eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) | eval_sizeof: forall e m ty' ty, eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty) @@ -1727,7 +1727,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' -> eval_simple_lvalue ge e m2 l' b ofs -> eval_simple_rvalue ge e m2 r' v -> - sem_cast v (typeof r) (typeof l) = Some v' -> + sem_cast v (typeof r) (typeof l) m2 = Some v' -> assign_loc ge (typeof l) m2 b ofs v' t3 m3 -> ty = typeof l -> eval_expr e m RV (Eassign l r ty) (t1**t2**t3) m3 (Eval v' ty) @@ -1738,7 +1738,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := deref_loc ge (typeof l) m2 b ofs t3 v1 -> eval_simple_rvalue ge e m2 r' v2 -> sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m2 = Some v3 -> - sem_cast v3 tyres (typeof l) = Some v4 -> + sem_cast v3 tyres (typeof l) m2 = Some v4 -> assign_loc ge (typeof l) m2 b ofs v4 t4 m3 -> ty = typeof l -> eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2**t3**t4) m3 (Eval v4 ty) @@ -1746,8 +1746,8 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m LV l t1 m1 l' -> eval_simple_lvalue ge e m1 l' b ofs -> deref_loc ge ty m1 b ofs t2 v1 -> - sem_incrdecr ge id v1 ty = Some v2 -> - sem_cast v2 (incrdecr_type ty) ty = Some v3 -> + sem_incrdecr ge id v1 ty m1 = Some v2 -> + sem_cast v2 (incrdecr_type ty) ty m1 = Some v3 -> assign_loc ge ty m1 b ofs v3 t3 m2 -> ty = typeof l -> eval_expr e m RV (Epostincr id l ty) (t1**t2**t3) m2 (Eval v1 ty) @@ -1901,7 +1901,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> bind_parameters ge e m1 f.(fn_params) vargs m2 -> exec_stmt e m2 f.(fn_body) t m3 out -> - outcome_result_value out f.(fn_return) vres -> + outcome_result_value out f.(fn_return) vres m3 -> Mem.free_list m3 (blocks_of_env ge e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres | eval_funcall_external: forall m ef targs tres cconv vargs t vres m', 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. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index b1a39c64..7228cd75 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -47,7 +47,7 @@ If [a] is a l-value, the returned value denotes: *) Definition do_cast (v: val) (t1 t2: type) : res val := - match sem_cast v t1 t2 with + match sem_cast v t1 t2 Mem.empty with | Some v' => OK v' | None => Error(msg "undefined cast") end. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 9c662f5e..e6fcad8c 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -120,7 +120,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Ebinop op r1 r2 ty) v | esr_cast: forall ty r1 v1 v, eval_simple_rvalue r1 v1 -> - sem_cast v1 (typeof r1) ty = Some v -> + sem_cast v1 (typeof r1) ty m = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) @@ -129,7 +129,7 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_seqand_true: forall r1 r2 ty v1 v2 v3, 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 -> + sem_cast v2 (typeof r2) type_bool m = 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) m = Some false -> @@ -137,7 +137,7 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_seqor_false: forall r1 r2 ty v1 v2 v3, 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 -> + sem_cast v2 (typeof r2) type_bool m = 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) m = Some true -> @@ -145,13 +145,13 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_condition: forall r1 r2 r3 ty v v1 b v', 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 -> + sem_cast v' (typeof (if b then r2 else r3)) ty m = Some v -> eval_simple_rvalue (Econdition r1 r2 r3 ty) v | esr_comma: forall r1 r2 ty v1 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v -> eval_simple_rvalue (Ecomma r1 r2 ty) v | esr_paren: forall r tycast ty v v', - eval_simple_rvalue r v -> sem_cast v (typeof r) tycast = Some v' -> + eval_simple_rvalue r v -> sem_cast v (typeof r) tycast m = Some v' -> eval_simple_rvalue (Eparen r tycast ty) v'. End SIMPLE_EXPRS. @@ -355,14 +355,16 @@ Proof. Qed. Lemma sem_cast_match: - forall v1 ty1 ty2 v2 v1' v2', - sem_cast v1 ty1 ty2 = Some v2 -> + forall v1 ty1 ty2 m v2 v1' v2', + sem_cast v1 ty1 ty2 m = Some v2 -> do_cast v1' ty1 ty2 = OK v2' -> Val.inject inj v1' v1 -> Val.inject inj v2' v2. Proof. - intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0. - exploit sem_cast_inject. eexact E. eauto. + intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2 Mem.empty) as [v2''|] eqn:E; inv H0. + exploit (sem_cast_inj inj Mem.empty m). + intros. rewrite mem_empty_not_weak_valid_pointer in H2. discriminate. + eexact E. eauto. intros [v' [A B]]. congruence. Qed. @@ -605,7 +607,7 @@ Theorem transl_init_single_steps: forall ty a data f m v1 ty1 m' v chunk b ofs m'', transl_init_single ge ty a = OK data -> star step ge (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') -> - sem_cast v1 ty1 ty = Some v -> + sem_cast v1 ty1 ty m' = Some v -> access_mode ty = By_value chunk -> Mem.store chunk m' b ofs v = Some m'' -> Genv.store_init_data ge m b ofs data = Some m''. @@ -760,7 +762,7 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'', star step ge (ExprState dummy_function a Kstop empty_env m) E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') -> - sem_cast v1 ty1 ty = Some v -> + sem_cast v1 ty1 ty m' = Some v -> access_mode ty = By_value chunk -> Mem.store chunk m' b ofs v = Some m'' -> exec_init m b ofs ty (Init_single a) m'' diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index a5a6ad66..a3af8114 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -114,7 +114,7 @@ Fixpoint eval_simpl_expr (a: expr) : option val := | Ecast b ty => match eval_simpl_expr b with | None => None - | Some v => sem_cast v (typeof b) ty + | Some v => sem_cast v (typeof b) ty Mem.empty end | _ => None end. @@ -327,10 +327,10 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement let ty2 := Csyntax.typeof r2 in match dst with | For_val | For_set _ => - do t <- gensym ty2; + do t <- gensym ty1; ret (finish dst - (sl1 ++ sl2 ++ Sset t a2 :: make_assign a1 (Etempvar t ty2) :: nil) - (Ecast (Etempvar t ty2) ty1)) + (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: make_assign a1 (Etempvar t ty1) :: nil) + (Etempvar t ty1)) | For_effects => ret (sl1 ++ sl2 ++ make_assign a1 a2 :: nil, dummy_expr) @@ -342,12 +342,12 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement do (sl3, a3) <- transl_valof ty1 a1; match dst with | For_val | For_set _ => - do t <- gensym tyres; + do t <- gensym ty1; ret (finish dst (sl1 ++ sl2 ++ sl3 ++ - Sset t (Ebinop op a3 a2 tyres) :: - make_assign a1 (Etempvar t tyres) :: nil) - (Ecast (Etempvar t tyres) ty1)) + Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) :: + make_assign a1 (Etempvar t ty1) :: nil) + (Etempvar t ty1)) | For_effects => ret (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil, dummy_expr) diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 0c7c9ce7..8baa7d46 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -752,12 +752,27 @@ Qed. (** Semantics of smart constructors *) +Remark sem_cast_deterministic: + forall v ty ty' m1 v1 m2 v2, + sem_cast v ty ty' m1 = Some v1 -> + sem_cast v ty ty' m2 = Some v2 -> + v1 = v2. +Proof. + unfold sem_cast; intros. destruct (classify_cast ty ty'); try congruence. + destruct v; try congruence. + destruct (Mem.weak_valid_pointer m1 b (Int.unsigned i)); inv H. + destruct (Mem.weak_valid_pointer m2 b (Int.unsigned i)); inv H0. + auto. +Qed. + Lemma eval_simpl_expr_sound: forall e le m a v, eval_expr tge e le m a v -> match eval_simpl_expr a with Some v' => v' = v | None => True end. Proof. induction 1; simpl; auto. - destruct (eval_simpl_expr a); auto. subst. rewrite H0. auto. + destruct (eval_simpl_expr a); auto. subst. + destruct (sem_cast v1 (typeof a) ty Mem.empty) as [v'|] eqn:C; auto. + eapply sem_cast_deterministic; eauto. inv H; simpl; auto. Qed. @@ -811,7 +826,7 @@ Lemma step_make_assign: Csem.assign_loc ge ty m b ofs v t m' -> eval_lvalue tge e le m a1 b ofs -> eval_expr tge e le m a2 v2 -> - sem_cast v2 (typeof a2) ty = Some v -> + sem_cast v2 (typeof a2) ty m = Some v -> typeof a1 = ty -> step1 tge (State f (make_assign a1 a2) k e le m) t (State f Sskip k e le m'). @@ -1649,18 +1664,19 @@ Proof. (* for value *) exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]]. exploit tr_simple_lvalue. eauto. - eapply tr_expr_invariant with (le' := PTree.set t0 v le). eauto. + eapply tr_expr_invariant with (le' := PTree.set t0 v' le). eauto. intros. apply PTree.gso. intuition congruence. intros [SL1 [TY1 EV1]]. subst; simpl Kseqlist. econstructor; split. left. eapply plus_left. constructor. - eapply star_left. constructor. eauto. + eapply star_left. constructor. econstructor. eauto. rewrite <- TY2; eauto. eapply star_left. constructor. apply star_one. eapply step_make_assign; eauto. - constructor. apply PTree.gss. reflexivity. reflexivity. traceEq. + constructor. apply PTree.gss. simpl. eapply cast_idempotent; eauto. + reflexivity. reflexivity. traceEq. econstructor. auto. apply S. - apply tr_val_gen. auto. intros. econstructor; eauto. constructor. + apply tr_val_gen. auto. intros. constructor. rewrite H4; auto. apply PTree.gss. intros. apply PTree.gso. intuition congruence. auto. auto. @@ -1692,7 +1708,7 @@ Proof. exploit tr_simple_rvalue. eauto. eapply tr_expr_invariant with (le := le) (le' := le'). eauto. intros. apply INV. NOTIN. simpl. intros [SL2 [TY2 EV2]]. exploit tr_simple_lvalue. eauto. - eapply tr_expr_invariant with (le := le) (le' := PTree.set t v3 le'). eauto. + eapply tr_expr_invariant with (le := le) (le' := PTree.set t v4 le'). eauto. intros. rewrite PTree.gso. apply INV. NOTIN. intuition congruence. intros [? [? EV1'']]. subst; simpl Kseqlist. @@ -1700,13 +1716,14 @@ Proof. left. rewrite app_ass. rewrite Kseqlist_app. eapply star_plus_trans. eexact EXEC. simpl. eapply plus_four. econstructor. econstructor. - econstructor. eexact EV3. eexact EV2. + econstructor. econstructor. eexact EV3. eexact EV2. rewrite TY3; rewrite <- TY1; rewrite <- TY2; rewrite comp_env_preserved; eauto. + eassumption. econstructor. eapply step_make_assign; eauto. - constructor. apply PTree.gss. + constructor. apply PTree.gss. simpl. eapply cast_idempotent; eauto. reflexivity. traceEq. econstructor. auto. apply S. - apply tr_val_gen. auto. intros. econstructor; eauto. constructor. + apply tr_val_gen. auto. intros. constructor. rewrite H10; auto. apply PTree.gss. intros. rewrite PTree.gso. apply INV. red; intros; elim H10; auto. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 4077d7df..b94465a1 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -222,10 +222,10 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> ty2 = Csyntax.typeof e2 -> tr_expr le dst (Csyntax.Eassign e1 e2 ty) (sl1 ++ sl2 ++ - Sset t a2 :: - make_assign a1 (Etempvar t ty2) :: - final dst (Ecast (Etempvar t ty2) ty1)) - (Ecast (Etempvar t ty2) ty1) tmp + Sset t (Ecast a2 ty1) :: + make_assign a1 (Etempvar t ty1) :: + final dst (Etempvar t ty1)) + (Etempvar t ty1) tmp | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> @@ -246,10 +246,10 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> ty1 = Csyntax.typeof e1 -> tr_expr le dst (Csyntax.Eassignop op e1 e2 tyres ty) (sl1 ++ sl2 ++ sl3 ++ - Sset t (Ebinop op a3 a2 tyres) :: - make_assign a1 (Etempvar t tyres) :: - final dst (Ecast (Etempvar t tyres) ty1)) - (Ecast (Etempvar t tyres) ty1) tmp + Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) :: + make_assign a1 (Etempvar t ty1) :: + final dst (Etempvar t ty1)) + (Etempvar t ty1) tmp | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_rvalof ty1 a1 sl2 a2 tmp2 -> @@ -375,8 +375,7 @@ Qed. between Csyntax values and Cminor expressions: in the case of [tr_expr], the Cminor expression must not depend on memory, while in the case of [tr_top] it can depend on the current memory - state. This special case is extended to values occurring under - one or several [Csyntax.Eparen]. *) + state. *) Section TR_TOP. @@ -389,19 +388,9 @@ Inductive tr_top: destination -> Csyntax.expr -> list statement -> expr -> list | tr_top_val_val: forall v ty a tmp, typeof a = ty -> eval_expr ge e le m a v -> tr_top For_val (Csyntax.Eval v ty) nil a tmp -(* - | tr_top_val_set: forall t tyl v ty a any tmp, - typeof a = ty -> eval_expr ge e le m a v -> - tr_top (For_set tyl t) (Csyntax.Eval v ty) (Sset t (fold_left Ecast tyl a) :: nil) any tmp -*) | tr_top_base: forall dst r sl a tmp, tr_expr le dst r sl a tmp -> tr_top dst r sl a tmp. -(* - | tr_top_paren_test: forall tyl t r ty sl a tmp, - tr_top (For_set (ty :: tyl) t) r sl a tmp -> - tr_top (For_set tyl t) (Csyntax.Eparen r ty) sl a tmp. -*) End TR_TOP. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index a47036bf..a86e3a01 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -201,97 +201,7 @@ Proof. xomegaContradiction. Qed. -(** Properties of values obtained by casting to a given type. *) - -Inductive val_casted: val -> type -> Prop := - | val_casted_int: forall sz si attr n, - cast_int_int sz si n = n -> - val_casted (Vint n) (Tint sz si attr) - | val_casted_float: forall attr n, - val_casted (Vfloat n) (Tfloat F64 attr) - | val_casted_single: forall attr n, - val_casted (Vsingle n) (Tfloat F32 attr) - | val_casted_long: forall si attr n, - val_casted (Vlong n) (Tlong si attr) - | val_casted_ptr_ptr: forall b ofs ty attr, - val_casted (Vptr b ofs) (Tpointer ty attr) - | val_casted_int_ptr: forall n ty attr, - val_casted (Vint n) (Tpointer ty attr) - | val_casted_ptr_int: forall b ofs si attr, - val_casted (Vptr b ofs) (Tint I32 si attr) - | val_casted_struct: forall id attr b ofs, - val_casted (Vptr b ofs) (Tstruct id attr) - | val_casted_union: forall id attr b ofs, - val_casted (Vptr b ofs) (Tunion id attr) - | val_casted_void: forall v, - val_casted v Tvoid. - -Remark cast_int_int_idem: - forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i. -Proof. - intros. destruct sz; simpl; auto. - destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence. - destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence. - destruct (Int.eq i Int.zero); auto. -Qed. - -Lemma cast_val_is_casted: - forall v ty ty' v', sem_cast v ty ty' = Some v' -> val_casted v' ty'. -Proof. - unfold sem_cast; intros. destruct ty'; simpl in *. -(* void *) - constructor. -(* int *) - destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H. - constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I8 s). - destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). - destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I16 s). - constructor. apply (cast_int_int_idem I16 s). - destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). - destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). - constructor. auto. - constructor. - constructor. auto. - destruct (cast_single_int s f); inv H1. constructor. auto. - destruct (cast_float_int s f); inv H1. constructor; auto. - constructor; auto. - constructor. - constructor; auto. - constructor. - constructor; auto. - constructor. - constructor. simpl. destruct (Int.eq i0 Int.zero); auto. - constructor. simpl. destruct (Int64.eq i Int64.zero); auto. - 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. simpl. destruct (Int.eq i Int.zero); auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. -(* long *) - destruct ty; try (destruct f); try discriminate. - destruct v; inv H. constructor. - destruct v; inv H. constructor. - destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor. - destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor. - destruct v; inv H. constructor. - destruct v; inv H. constructor. - destruct v; inv H. constructor. -(* float *) - destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor. -(* pointer *) - destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor. -(* impossible cases *) - discriminate. - discriminate. -(* structs *) - destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i); inv H; constructor. -(* unions *) - destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i); inv H; constructor. -Qed. +(** Properties of values resulting from a cast *) Lemma val_casted_load_result: forall v ty chunk, @@ -316,15 +226,6 @@ Proof. discriminate. Qed. -Lemma cast_val_casted: - forall v ty, val_casted v ty -> sem_cast v ty ty = Some v. -Proof. - intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto. - destruct sz; congruence. - unfold proj_sumbool; repeat rewrite dec_eq_true; auto. - unfold proj_sumbool; repeat rewrite dec_eq_true; auto. -Qed. - Lemma val_casted_inject: forall f v v' ty, Val.inject f v v' -> val_casted v ty -> val_casted v' ty. @@ -363,7 +264,7 @@ Qed. Lemma make_cast_correct: forall e le m a v1 tto v2, eval_expr tge e le m a v1 -> - sem_cast v1 (typeof a) tto = Some v2 -> + sem_cast v1 (typeof a) tto m = Some v2 -> eval_expr tge e le m (make_cast a tto) v2. Proof. intros. @@ -386,9 +287,9 @@ Qed. (** Debug annotations. *) Lemma cast_typeconv: - forall v ty, + forall v ty m, val_casted v ty -> - sem_cast v ty (typeconv ty) = Some v. + sem_cast v ty (typeconv ty) m = Some v. Proof. induction 1; simpl; auto. - destruct sz; auto. @@ -423,7 +324,7 @@ Qed. Lemma step_Sset_debug: forall f id ty a k e le m v v', eval_expr tge e le m a v -> - sem_cast v (typeof a) ty = Some v' -> + sem_cast v (typeof a) ty m = Some v' -> plus step2 tge (State f (Sset_debug id ty a) k e le m) E0 (State f Sskip k e (PTree.set id v' le) m). Proof. |