diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 79 | ||||
-rw-r--r-- | cfrontend/Csem.v | 2 | ||||
-rw-r--r-- | cfrontend/Initializers.v | 173 | ||||
-rw-r--r-- | cfrontend/Initializersproof.v | 555 |
4 files changed, 754 insertions, 55 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 23d05029..eefc813c 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -12,6 +12,8 @@ open Printf +module CompcertErrors = Errors (* avoid shadowing by Cparser.Errors *) + open Cparser open Cparser.C open Cparser.Env @@ -743,14 +745,20 @@ let convertFundecl env (sto, id, ty, optinit) = (** Initializers *) -let init_data_of_string s = - let id = ref [] in - let enter_char c = - let n = coqint_of_camlint(Int32.of_int(Char.code c)) in - id := Init_int8 n :: !id in - enter_char '\000'; - for i = String.length s - 1 downto 0 do enter_char s.[i] done; - !id +let init_data_size = function + | Init_int8 _ -> 1 + | Init_int16 _ -> 2 + | Init_int32 _ -> 4 + | Init_float32 _ -> 4 + | Init_float64 _ -> 8 + | Init_addrof _ -> 4 + | Init_space _ -> assert false + +let string_of_errmsg msg = + let string_of_err = function + | CompcertErrors.MSG s -> camlstring_of_coqstring s + | CompcertErrors.CTX i -> extern_atom i + in String.concat "" (List.map string_of_err msg) let convertInit env ty init = @@ -767,54 +775,17 @@ let convertInit env ty init = let check_align size = assert (!pos land (size - 1) = 0) in - let rec reduceInitExpr = function - | { edesc = C.EVar id; etyp = ty } -> - begin match Cutil.unroll env ty with - | C.TArray _ | C.TFun _ -> Some id - | _ -> None - end - | {edesc = C.EUnop(C.Oaddrof, {edesc = C.EVar id})} -> Some id - | {edesc = C.ECast(ty, e)} -> reduceInitExpr e - | _ -> None in - let rec cvtInit ty = function | Init_single e -> - begin match reduceInitExpr e with - | Some id -> - check_align 4; - emit 4 (Init_addrof(intern_string id.name, coqint_of_camlint 0l)) - | None -> - match Ceval.constant_expr env ty e with - | Some(C.CInt(v, ik, _)) -> - begin match convertIkind ik with - | (_, I8) -> - emit 1 (Init_int8(convertInt v)) - | (_, I16) -> - check_align 2; - emit 2 (Init_int16(convertInt v)) - | (_, I32) -> - check_align 4; - emit 4 (Init_int32(convertInt v)) - end - | Some(C.CFloat(v, fk, _)) -> - begin match convertFkind fk with - | F32 -> - check_align 4; - emit 4 (Init_float32 v) - | F64 -> - check_align 8; - emit 8 (Init_float64 v) - end - | Some(C.CStr s) -> - check_align 4; - let id = name_for_string_literal env s in - emit 4 (Init_addrof(id, coqint_of_camlint 0l)) - | Some(C.CWStr _) -> - unsupported "wide character strings" - | Some(C.CEnum _) -> - error "enum tag after constant folding" - | None -> - error "initializer is not a compile-time constant" + begin match Initializers.transl_init_single + (convertTyp env ty) (convertExpr env e) with + | CompcertErrors.OK init -> + let sz = init_data_size init in + check_align sz; + emit sz init + | CompcertErrors.Error msg -> + Format.printf "%a@." Cprint.exp (0, e); + error ("in initializing expression above: " ^ string_of_errmsg msg) end | Init_array il -> let ty_elt = diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 927cd69d..dff5fa26 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -13,7 +13,7 @@ (* *) (* *********************************************************************) -(** Dynamic semantics for the Clight language *) +(** Dynamic semantics for the Compcert C language *) Require Import Coqlib. Require Import Errors. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v new file mode 100644 index 00000000..926a8267 --- /dev/null +++ b/cfrontend/Initializers.v @@ -0,0 +1,173 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Compile-time evaluation of initializers for global C variables. *) + +Require Import Coqlib. +Require Import Errors. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import AST. +Require Import Memory. +Require Import Csyntax. +Require Import Csem. + +Open Scope error_monad_scope. + +(** * Evaluation of compile-time constant expressions *) + +(** Computing the predicates [cast], [is_true], and [is_false]. *) + +Definition bool_val (v: val) (t: type) : res bool := + match v, t with + | Vint n, Tint sz sg => OK (negb (Int.eq n Int.zero)) + | Vint n, Tpointer t' => OK (negb (Int.eq n Int.zero)) + | Vptr b ofs, Tint sz sg => OK true + | Vptr b ofs, Tpointer t' => OK true + | Vfloat f, Tfloat sz => OK (negb(Float.cmp Ceq f Float.zero)) + | _, _ => Error(msg "undefined conditional") + end. + +Definition is_neutral_for_cast (t: type) : bool := + match t with + | Tint I32 sg => true + | Tpointer ty => true + | Tarray ty sz => true + | Tfunction targs tres => true + | _ => false + end. + +Definition do_cast (v: val) (t1 t2: type) : res val := + match v, t1, t2 with + | Vint i, Tint sz1 si1, Tint sz2 si2 => + OK (Vint (cast_int_int sz2 si2 i)) + | Vfloat f, Tfloat sz1, Tint sz2 si2 => + match cast_float_int si2 f with + | Some i => OK (Vint (cast_int_int sz2 si2 i)) + | None => Error(msg "overflow in float-to-int cast") + end + | Vint i, Tint sz1 si1, Tfloat sz2 => + OK (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) + | Vfloat f, Tfloat sz1, Tfloat sz2 => + OK (Vfloat (cast_float_float sz2 f)) + | Vptr b ofs, _, _ => + if is_neutral_for_cast t1 && is_neutral_for_cast t2 + then OK(Vptr b ofs) else Error(msg "undefined cast") + | Vint n, _, _ => + if is_neutral_for_cast t1 && is_neutral_for_cast t2 + then OK(Vint n) else Error(msg "undefined cast") + | _, _, _ => + Error(msg "undefined cast") + end. + +(** To evaluate constant expressions at compile-time, we use the same [value] + type and the same [sem_*] functions that are used in CompCert C's semantics + (module [Csem]). However, we interpret pointer values symbolically: + [Vptr (Zpos id) ofs] represents the address of global variable [id] + plus byte offset [ofs]. *) + +(** [constval a] evaluates the constant expression [a]. + +If [a] is a r-value, the returned value denotes: +- [Vint n], [Vfloat f]: the corresponding number +- [Vptr id ofs]: address of global variable [id] plus byte offset [ofs] +- [Vundef]: erroneous expression + +If [a] is a l-value, the returned value denotes: +- [Vptr id ofs]: global variable [id] plus byte offset [ofs] +*) + +Fixpoint constval (a: expr) : res val := + match a with + | Eval v ty => + match v with + | Vint _ | Vfloat _ => OK v + | Vptr _ _ | Vundef => Error(msg "illegal constant") + end + | Evalof l ty => + match access_mode ty with + | By_reference => constval l + | _ => Error(msg "dereference operation") + end + | Eaddrof l ty => + constval l + | Eunop op r1 ty => + do v1 <- constval r1; + match sem_unary_operation op v1 (typeof r1) with + | Some v => OK v + | None => Error(msg "undefined unary operation") + end + | Ebinop op r1 r2 ty => + do v1 <- constval r1; + do v2 <- constval r2; + match sem_binary_operation op v1 (typeof r1) v2 (typeof r2) Mem.empty with + | Some v => OK v + | None => Error(msg "undefined binary operation") + end + | Ecast r ty => + do v <- constval r; do_cast v (typeof r) ty + | Esizeof ty1 ty => + OK (Vint (Int.repr (sizeof ty1))) + | Econdition r1 r2 r3 ty => + do v1 <- constval r1; + do b1 <- bool_val v1 (typeof r1); + do v2 <- constval r2; + do v3 <- constval r3; + OK (if b1 then v2 else v3) + | Ecomma r1 r2 ty => + do v1 <- constval r1; constval r2 + | Evar x ty => + OK(Vptr (Zpos x) Int.zero) + | Ederef r ty => + constval r + | Efield l f ty => + match typeof l with + | Tstruct id fList => + do delta <- field_offset f fList; + do v <- constval l; + OK (Val.add v (Vint (Int.repr delta))) + | Tunion id fList => + constval l + | _ => + Error(msg "ill-typed field access") + end + | Eparen r ty => + constval r + | _ => + Error(msg "not a compile-time constant") + end. + +(** * Translation of initializers *) + +(** Translate an initializing expression [a] for a scalar variable + of type [ty]. Return the corresponding [init_data]. *) + +Definition transl_init_single (ty: type) (a: expr) : res init_data := + do v1 <- constval a; + do v2 <- do_cast v1 (typeof a) ty; + match v2, ty with + | Vint n, Tint I8 sg => OK(Init_int8 n) + | Vint n, Tint I16 sg => OK(Init_int16 n) + | Vint n, Tint I32 sg => OK(Init_int32 n) + | Vint n, Tpointer _ => OK(Init_int32 n) + | Vfloat f, Tfloat F32 => OK(Init_float32 f) + | Vfloat f, Tfloat F64 => OK(Init_float64 f) + | Vptr (Zpos id) ofs, Tint I32 sg => OK(Init_addrof id ofs) + | Vptr (Zpos id) ofs, Tpointer _ => OK(Init_addrof id ofs) + | Vundef, _ => Error(msg "undefined operation in initializer") + | _, _ => Error (msg "type mismatch in initializer") + end. + +(** To come later: translation of compound initializers, currently + still done in Caml (module [C2C]). *) + diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v new file mode 100644 index 00000000..fde3c4ed --- /dev/null +++ b/cfrontend/Initializersproof.v @@ -0,0 +1,555 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Compile-time evaluation of initializers for global C variables. *) + +Require Import Coq.Program.Equality. +Require Import Coqlib. +Require Import Errors. +Require Import Maps. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import AST. +Require Import Memory. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Csyntax. +Require Import Csem. +Require Import Initializers. + +Open Scope error_monad_scope. + +Section SOUNDNESS. + +Variable ge: genv. + +(** * Simple expressions and their big-step semantics *) + +(** An expression is simple if it contains no assignments and no + function calls. *) + +Fixpoint simple (a: expr) : Prop := + match a with + | Eloc _ _ _ => True + | Evar _ _ => True + | Ederef r _ => simple r + | Efield l1 _ _ => simple l1 + | Eval _ _ => True + | Evalof l _ => simple l + | Eaddrof l _ => simple l + | Eunop _ r1 _ => simple r1 + | Ebinop _ r1 r2 _ => simple r1 /\ simple r2 + | Ecast r1 _ => simple r1 + | Econdition r1 r2 r3 _ => simple r1 /\ simple r2 /\ simple r3 + | Esizeof _ _ => True + | Eassign _ _ _ => False + | Eassignop _ _ _ _ _ => False + | Epostincr _ _ _ => False + | Ecomma r1 r2 _ => simple r1 /\ simple r2 + | Ecall _ _ _ => False + | Eparen r1 _ => simple r1 + end. + +(** A big-step semantics for simple expressions. Similar to the + big-step semantics from [Cstrategy], with the addition of + conditionals, comma and paren operators. It is a pity we do not + share definitions with [Cstrategy], but such sharing raises + technical difficulties. *) + +Section SIMPLE_EXPRS. + +Variable e: env. +Variable m: mem. + +Inductive eval_simple_lvalue: expr -> block -> int -> Prop := + | esl_loc: forall b ofs ty, + eval_simple_lvalue (Eloc b ofs ty) b ofs + | esl_var_local: forall x ty b, + e!x = Some(b, ty) -> + eval_simple_lvalue (Evar x ty) b Int.zero + | esl_var_global: forall x ty b, + e!x = None -> + Genv.find_symbol ge x = Some b -> + type_of_global ge b = Some ty -> + eval_simple_lvalue (Evar x ty) b Int.zero + | esl_deref: forall r ty b ofs, + eval_simple_rvalue r (Vptr b ofs) -> + eval_simple_lvalue (Ederef r ty) b ofs + | esl_field_struct: forall l f ty b ofs id fList delta, + eval_simple_lvalue l b ofs -> + typeof l = Tstruct id fList -> field_offset f fList = OK delta -> + eval_simple_lvalue (Efield l f ty) b (Int.add ofs (Int.repr delta)) + | esl_field_union: forall l f ty b ofs id fList, + eval_simple_lvalue l b ofs -> + typeof l = Tunion id fList -> + eval_simple_lvalue (Efield l f ty) b ofs + +with eval_simple_rvalue: expr -> val -> Prop := + | esr_val: forall v ty, + eval_simple_rvalue (Eval v ty) v + | esr_rvalof: forall b ofs l ty v, + eval_simple_lvalue l b ofs -> + ty = typeof l -> + load_value_of_type ty m b ofs = Some v -> + eval_simple_rvalue (Evalof l ty) v + | esr_addrof: forall b ofs l ty, + eval_simple_lvalue l b ofs -> + eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) + | esr_unop: forall op r1 ty v1 v, + eval_simple_rvalue r1 v1 -> + sem_unary_operation op v1 (typeof r1) = Some v -> + eval_simple_rvalue (Eunop op r1 ty) v + | esr_binop: forall op r1 r2 ty v1 v2 v, + eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> + sem_binary_operation op v1 (typeof r1) v2 (typeof r2) m = Some v -> + eval_simple_rvalue (Ebinop op r1 r2 ty) v + | esr_cast: forall ty r1 v1 v, + eval_simple_rvalue r1 v1 -> + cast v1 (typeof r1) ty v -> + eval_simple_rvalue (Ecast r1 ty) v + | esr_sizeof: forall ty1 ty, + eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))) + | esr_condition_true: forall r1 r2 r3 ty v v1, + eval_simple_rvalue r1 v1 -> is_true v1 (typeof r1) -> eval_simple_rvalue r2 v -> + eval_simple_rvalue (Econdition r1 r2 r3 ty) v + | esr_condition_false: forall r1 r2 r3 ty v v1, + eval_simple_rvalue r1 v1 -> is_false v1 (typeof r1) -> eval_simple_rvalue r3 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 ty v, + eval_simple_rvalue r v -> + eval_simple_rvalue (Eparen r ty) v. + +End SIMPLE_EXPRS. + +(** * Correctness of the big-step semantics with respect to reduction sequences *) + +(** In this section, we show that if a simple expression [a] reduces to + some value (with the transition semantics from module [Csem]), + then it evaluates to this value (with the big-step semantics above). *) + +Definition compat_eval (k: kind) (e: env) (a a': expr) (m: mem) : Prop := + typeof a = typeof a' /\ + match k with + | LV => forall b ofs, eval_simple_lvalue e m a' b ofs -> eval_simple_lvalue e m a b ofs + | RV => forall v, eval_simple_rvalue e m a' v -> eval_simple_rvalue e m a v + end. + +Lemma lred_simple: + forall e l m l' m', lred ge e l m l' m' -> simple l -> simple l'. +Proof. + induction 1; simpl; tauto. +Qed. + +Lemma lred_compat: + forall e l m l' m', lred ge e l m l' m' -> + m = m' /\ compat_eval LV e l l' m. +Proof. + induction 1; simpl; split; auto; split; auto; intros bx ofsx EV; inv EV. + apply esl_var_local; auto. + apply esl_var_global; auto. + constructor. constructor. + eapply esl_field_struct; eauto. constructor. simpl; eauto. + eapply esl_field_union; eauto. constructor. simpl; eauto. +Qed. + +Lemma rred_simple: + forall r m r' m', rred r m r' m' -> simple r -> simple r'. +Proof. + induction 1; simpl; tauto. +Qed. + +Lemma rred_compat: + forall e r m r' m', rred r m r' m' -> + simple r -> + m = m' /\ compat_eval RV e r r' m. +Proof. + induction 1; simpl; intro SIMP; try contradiction; split; auto; split; auto; intros vx EV. + inv EV. econstructor. constructor. auto. auto. + inv EV. econstructor. constructor. + inv EV. econstructor; eauto. constructor. + inv EV. econstructor; eauto. constructor. constructor. + inv EV. econstructor; eauto. constructor. + inv EV. eapply esr_condition_true; eauto. constructor. + inv EV. eapply esr_condition_false; eauto. constructor. + inv EV. constructor. + econstructor; eauto. constructor. + constructor; auto. +Qed. + +Lemma compat_eval_context: + forall e a a' m from to C, + context from to C -> + compat_eval from e a a' m -> + compat_eval to e (C a) (C a') m. +Proof. + induction 1; intros CE; auto; + try (generalize (IHcontext CE); intros [TY EV]; red; split; simpl; auto; intros). + inv H0. constructor; auto. + inv H0. + eapply esl_field_struct; eauto. rewrite TY; eauto. + eapply esl_field_union; eauto. rewrite TY; eauto. + inv H0. econstructor. eauto. auto. auto. + inv H0. econstructor; eauto. + inv H0. econstructor; eauto. congruence. + inv H0. econstructor; eauto. congruence. + inv H0. econstructor; eauto. congruence. + inv H0. econstructor; eauto. congruence. + inv H0. + eapply esr_condition_true; eauto. congruence. + eapply esr_condition_false; eauto. congruence. + inv H0. + inv H0. + inv H0. + inv H0. + inv H0. + inv H0. + red; split; intros. auto. inv H0. + inv H0. econstructor; eauto. + inv H0. constructor. auto. +Qed. + +Lemma simple_context_1: + forall a from to C, context from to C -> simple (C a) -> simple a. +Proof. + induction 1; simpl; tauto. +Qed. + +Lemma simple_context_2: + forall a a', simple a' -> forall from to C, context from to C -> simple (C a) -> simple (C a'). +Proof. + induction 2; simpl; tauto. +Qed. + +Lemma compat_eval_steps: + forall f r e m w r' m', + star step ge (ExprState f r Kstop e m) w (ExprState f r' Kstop e m') -> + simple r -> + m' = m /\ compat_eval RV e r r' m. +Proof. + intros. dependent induction H. + (* base case *) + split. auto. red; auto. + (* inductive case *) + destruct H. + (* expression step *) + assert (X: exists r1, s2 = ExprState f r1 Kstop e m /\ compat_eval RV e r r1 m /\ simple r1). + inv H. + (* lred *) + assert (S: simple a) by (eapply simple_context_1; eauto). + exploit lred_compat; eauto. intros [A B]. subst m'0. + econstructor; split. eauto. split. + eapply compat_eval_context; eauto. + eapply simple_context_2; eauto. eapply lred_simple; eauto. + (* rred *) + assert (S: simple a) by (eapply simple_context_1; eauto). + exploit rred_compat; eauto. intros [A B]. subst m'0. + econstructor; split. eauto. split. + eapply compat_eval_context; eauto. + eapply simple_context_2; eauto. eapply rred_simple; eauto. + (* callred *) + assert (S: simple a) by (eapply simple_context_1; eauto). + inv H9; simpl in S; contradiction. + destruct X as [r1 [A [B C]]]. subst s2. + exploit IHstar; eauto. intros [D E]. + split. auto. destruct B; destruct E. split. congruence. auto. + (* statement steps *) + inv H. +Qed. + +Theorem eval_simple_steps: + forall f r e m w v ty m', + star step ge (ExprState f r Kstop e m) w (ExprState f (Eval v ty) Kstop e m') -> + simple r -> + m' = m /\ ty = typeof r /\ eval_simple_rvalue e m r v. +Proof. + intros. exploit compat_eval_steps; eauto. intros [A [B C]]. + intuition. apply C. constructor. +Qed. + +(** * Soundness of the compile-time evaluator *) + +(** [match_val v v'] holds if the compile-time value [v] + (with symbolic pointers) matches the run-time value [v'] + (with concrete pointers). *) + +Inductive match_val: val -> val -> Prop := + | match_vint: forall n, + match_val (Vint n) (Vint n) + | match_vfloat: forall f, + match_val (Vfloat f) (Vfloat f) + | match_vptr: forall id b ofs, + Genv.find_symbol ge id = Some b -> + match_val (Vptr (Zpos id) ofs) (Vptr b ofs) + | match_vundef: + match_val Vundef Vundef. + +Lemma match_val_of_bool: + forall b, match_val (Val.of_bool b) (Val.of_bool b). +Proof. + destruct b; constructor. +Qed. + +Hint Constructors match_val: mval. +Hint Resolve match_val_of_bool: mval. + +(** The [match_val] relation commutes with the evaluation functions + from [Csem]. *) + +Lemma sem_unary_match: + forall op ty v1 v v1' v', + sem_unary_operation op v1 ty = Some v -> + sem_unary_operation op v1' ty = Some v' -> + match_val v1 v1' -> + match_val v v'. +Proof. + intros. destruct op; simpl in *. + unfold sem_notbool in *. destruct (classify_bool ty); inv H1; inv H; inv H0; auto with mval. constructor. + unfold sem_notint in *. destruct (classify_notint ty); inv H1; inv H; inv H0; auto with mval. + unfold sem_neg in *. destruct (classify_neg ty); inv H1; inv H; inv H0; auto with mval. +Qed. + +Lemma mem_empty_not_valid_pointer: + forall b ofs, Mem.valid_pointer Mem.empty b ofs = false. +Proof. + intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Nonempty); auto. + red in p. simpl in p. contradiction. +Qed. + +Lemma sem_cmp_match: + forall c v1 ty1 v2 ty2 m v v1' v2' v', + sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v -> + sem_cmp c v1' ty1 v2' ty2 m = Some v' -> + match_val v1 v1' -> match_val v2 v2' -> + match_val v v'. +Proof. + intros. unfold sem_cmp in *. + destruct (classify_cmp ty1 ty2); 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. +Qed. + +Lemma sem_binary_match: + forall op v1 ty1 v2 ty2 m v v1' v2' v', + sem_binary_operation op v1 ty1 v2 ty2 Mem.empty = Some v -> + sem_binary_operation op v1' ty1 v2' ty2 m = Some v' -> + match_val v1 v1' -> match_val v2 v2' -> + match_val v v'. +Proof. + intros. unfold sem_binary_operation in *; destruct op. +(* add *) + unfold sem_add in *. destruct (classify_add ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. +(* sub *) + unfold sem_sub in *. destruct (classify_sub ty1 ty2); inv H1; inv H2; try (inv H; inv H0; auto with mval; fail). + destruct (zeq (Zpos id) (Zpos id0)); try discriminate. + assert (b0 = b) by congruence. subst b0. rewrite zeq_true in H0. + destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H; inv H0; auto with mval. +(* mul *) + unfold sem_mul in *. destruct (classify_mul ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. +(* div *) + unfold sem_div in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0. + rewrite H11 in H2. inv H2. inv H12. constructor. + rewrite H11 in H2. inv H2. inv H12. constructor. + inv H11. constructor. + inv H11. constructor. + inv H11. constructor. +(* mod *) + unfold sem_mod in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0. + rewrite H11 in H2. inv H2. inv H12. constructor. + rewrite H11 in H2. inv H2. inv H12. constructor. +(* and *) + unfold sem_and in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. +(* or *) + unfold sem_or in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. +(* xor *) + unfold sem_xor in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. +(* shl *) + unfold sem_shl in *. destruct (classify_shift ty1 ty2); inv H1; inv H2; try discriminate. + destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. +(* shr *) + unfold sem_shr in *. destruct (classify_shift ty1 ty2); try discriminate; + destruct s; inv H1; inv H2; try discriminate. + destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. + destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. +(* comparisons *) + eapply sem_cmp_match; eauto. + eapply sem_cmp_match; eauto. + eapply sem_cmp_match; eauto. + eapply sem_cmp_match; eauto. + eapply sem_cmp_match; eauto. + eapply sem_cmp_match; eauto. +Qed. + +Lemma is_neutral_for_cast_correct: + forall t, neutral_for_cast t -> is_neutral_for_cast t = true. +Proof. + induction 1; simpl; auto. +Qed. + +Lemma cast_match: + forall v1 ty1 ty2 v2, cast v1 ty1 ty2 v2 -> + forall v1' v2', match_val v1' v1 -> do_cast v1' ty1 ty2 = OK v2' -> + match_val v2' v2. +Proof. + induction 1; intros v1' v2' MV DC; inv MV; simpl in DC. + inv DC; constructor. + rewrite H in DC. inv DC. constructor. + inv DC; constructor. + inv DC; constructor. + rewrite (is_neutral_for_cast_correct _ H) in DC. + rewrite (is_neutral_for_cast_correct _ H0) in DC. + simpl in DC. inv DC. constructor; auto. + rewrite (is_neutral_for_cast_correct _ H) in DC. + rewrite (is_neutral_for_cast_correct _ H0) in DC. + simpl in DC. + assert (OK v2' = OK (Vint n)). + inv H; auto. inv H0; auto. + inv H1. constructor. +Qed. + +Lemma bool_val_true: + forall v v' ty, is_true v' ty -> match_val v v' -> bool_val v ty = OK true. +Proof. + induction 1; intros MV; inv MV; simpl; auto. + predSpec Int.eq Int.eq_spec n Int.zero. congruence. auto. + predSpec Int.eq Int.eq_spec n Int.zero. congruence. auto. + rewrite H; auto. +Qed. + +Lemma bool_val_false: + forall v v' ty, is_false v' ty -> match_val v v' -> bool_val v ty = OK false. +Proof. + induction 1; intros MV; inv MV; simpl; auto. + rewrite H; auto. +Qed. + +(** Soundness of [constval] with respect to the big-step semantics *) + +Lemma constval_rvalue: + forall m a v, + eval_simple_rvalue empty_env m a v -> + forall v', + constval a = OK v' -> + match_val v' v +with constval_lvalue: + forall m a b ofs, + eval_simple_lvalue empty_env m a b ofs -> + forall v', + constval a = OK v' -> + match_val v' (Vptr b ofs). +Proof. + (* rvalue *) + induction 1; intros v' CV; simpl in CV; try (monadInv CV). + (* val *) + destruct v; monadInv CV; constructor. + (* rval *) + unfold load_value_of_type in H1. destruct (access_mode ty); try congruence. inv H1. + eauto. + (* addrof *) + eauto. + (* unop *) + revert EQ0. caseEq (sem_unary_operation op x (typeof r1)); intros; inv EQ0. + eapply sem_unary_match; eauto. + (* binop *) + revert EQ2. caseEq (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty); intros; inv EQ2. + eapply sem_binary_match; eauto. + (* cast *) + eapply cast_match; eauto. + (* sizeof *) + constructor. + (* conditional true *) + assert (x0 = true). exploit bool_val_true; eauto. congruence. subst x0. auto. + (* conditional false *) + assert (x0 = false). exploit bool_val_false; eauto. congruence. subst x0. auto. + (* comma *) + auto. + (* paren *) + auto. + + (* lvalue *) + induction 1; intros v' CV; simpl in CV; try (monadInv CV). + (* var local *) + unfold empty_env in H. rewrite PTree.gempty in H. congruence. + (* var_global *) + constructor; auto. + (* deref *) + eauto. + (* field struct *) + rewrite H0 in CV. monadInv CV. exploit IHeval_simple_lvalue; eauto. intro MV. inv MV. + simpl. replace x with delta by congruence. constructor. auto. + (* field union *) + rewrite H0 in CV. auto. +Qed. + +Lemma constval_simple: + forall a v, constval a = OK v -> simple a. +Proof. + induction a; simpl; intros vx CV; try (monadInv CV); eauto. + destruct (typeof a); discriminate || eauto. + monadInv CV. eauto. + destruct (access_mode ty); discriminate || eauto. + intuition eauto. +Qed. + +(** Soundness of [constval] with respect to the reduction semantics. *) + +Theorem constval_steps: + forall f r m w v v' ty m', + star step ge (ExprState f r Kstop empty_env m) w (ExprState f (Eval v' ty) Kstop empty_env m') -> + constval r = OK v -> + m' = m /\ ty = typeof r /\ match_val v v'. +Proof. + intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. + intros [A [B C]]. intuition. eapply constval_rvalue; eauto. +Qed. + +(** * Soundness of the translation of initializers *) + +Theorem transl_init_single_steps: + forall ty a data f m w v1 ty1 m' v b ofs m'', + transl_init_single ty a = OK data -> + star step ge (ExprState f a Kstop empty_env m) w (ExprState f (Eval v1 ty1) Kstop empty_env m') -> + cast v1 ty1 ty v -> + store_value_of_type ty m' b ofs v = Some m'' -> + Genv.store_init_data ge m b (Int.signed ofs) data = Some m''. +Proof. + intros. monadInv H. + exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1. + exploit cast_match; eauto. intros D. + unfold Genv.store_init_data. unfold store_value_of_type in H2. simpl in H2. + inv D. + (* int *) + destruct ty; try discriminate. + destruct i; inv EQ2. + destruct s; simpl in H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. + destruct s; simpl in H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto. + assumption. + inv EQ2. assumption. + (* float *) + destruct ty; try discriminate. + destruct f1; inv EQ2; assumption. + (* pointer *) + assert (data = Init_addrof id ofs0 /\ access_mode ty = By_value Mint32). + destruct ty; inv EQ2; auto. destruct i; inv H4; auto. + destruct H3; subst. rewrite H4 in H2. rewrite H. assumption. + (* undef *) + discriminate. +Qed. + +End SOUNDNESS. + |