From e89f1e606bc8c9c425628392adc9c69cec666b5e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 22 Dec 2014 19:34:45 +0100 Subject: Represent struct and union types by name instead of by structure. --- cfrontend/C2C.ml | 251 +++++------- cfrontend/Cexec.v | 80 ++-- cfrontend/Clight.v | 142 ++++--- cfrontend/ClightBigstep.v | 18 +- cfrontend/Cop.v | 82 ++-- cfrontend/Csem.v | 96 ++--- cfrontend/Cshmgen.v | 179 +++++---- cfrontend/Cshmgenproof.v | 154 ++++---- cfrontend/Cstrategy.v | 97 ++--- cfrontend/Csyntax.v | 45 ++- cfrontend/Ctypes.v | 883 ++++++++++++++++++++++++++---------------- cfrontend/Initializers.v | 115 +++--- cfrontend/Initializersproof.v | 162 ++++---- cfrontend/PrintClight.ml | 71 +--- cfrontend/PrintCsyntax.ml | 141 +------ cfrontend/SimplExpr.v | 9 +- cfrontend/SimplExprproof.v | 77 ++-- cfrontend/SimplExprspec.v | 4 +- cfrontend/SimplLocals.v | 18 +- cfrontend/SimplLocalsproof.v | 202 +++++----- 20 files changed, 1518 insertions(+), 1308 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4d5d6c07..ea278ac1 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -100,6 +100,10 @@ let atom_location a = with Not_found -> Cutil.no_loc +(** The current environment of composite definitions *) + +let comp_env : composite_env ref = ref Maps.PTree.empty + (** Hooks -- overriden in machine-dependent CPragmas module *) let process_pragma_hook = ref (fun (s: string) -> false) @@ -243,12 +247,12 @@ let make_builtin_memcpy args = match args with | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) -> let sz1 = - match Initializers.constval sz with + match Initializers.constval !comp_env sz with | Errors.OK(Vint n) -> n | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; Integers.Int.zero in let al1 = - match Initializers.constval al with + match Initializers.constval !comp_env al with | Errors.OK(Vint n) -> n | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; Integers.Int.one in @@ -270,7 +274,7 @@ let va_list_ptr e = let make_builtin_va_arg env ty e = let (helper, ty_ret) = match ty with - | Tint _ | Tpointer _ | Tcomp_ptr _ -> + | Tint _ | Tpointer _ -> ("__compcert_va_int32", Tint(I32, Unsigned, noattr)) | Tlong _ -> ("__compcert_va_int64", Tlong(Unsigned, noattr)) @@ -303,27 +307,6 @@ let convertAttr a = let n = Cutil.alignas_attribute a in if n > 0 then Some (N.of_int (log2 n)) else None } -let mergeAttr a1 a2 = - { attr_volatile = a1.attr_volatile || a2.attr_volatile; - attr_alignas = - match a1.attr_alignas, a2.attr_alignas with - | None, aa -> aa - | aa, None -> aa - | Some n1, Some n2 -> Some (if N.le n1 n2 then n1 else n2) } - -let mergeTypAttr ty a2 = - match ty with - | Tvoid -> ty - | Tint(sz, sg, a1) -> Tint(sz, sg, mergeAttr a1 a2) - | Tfloat(sz, a1) -> Tfloat(sz, mergeAttr a1 a2) - | Tlong(sg, a1) -> Tlong(sg, mergeAttr a1 a2) - | Tpointer(ty', a1) -> Tpointer(ty', mergeAttr a1 a2) - | Tarray(ty', sz, a1) -> Tarray(ty', sz, mergeAttr a1 a2) - | Tfunction(targs, tres, cc) -> ty - | Tstruct(id, fld, a1) -> Tstruct(id, fld, mergeAttr a1 a2) - | Tunion(id, fld, a1) -> Tunion(id, fld, mergeAttr a1 a2) - | Tcomp_ptr(id, a1) -> Tcomp_ptr(id, mergeAttr a1 a2) - let convertCallconv va attr = let sr = Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in @@ -353,93 +336,48 @@ let convertFkind = function if not !Clflags.option_flongdouble then unsupported "'long double' type"; F64 -(** A cache for structs and unions already converted *) - -let compositeCache : (C.ident, coq_type) Hashtbl.t = Hashtbl.create 77 - -let convertTyp env t = - - let rec convertTyp seen t = - match Cutil.unroll env t with - | C.TVoid a -> Tvoid - | C.TInt(C.ILongLong, a) -> - Tlong(Signed, convertAttr a) - | C.TInt(C.IULongLong, a) -> - Tlong(Unsigned, convertAttr a) - | C.TInt(ik, a) -> - let (sg, sz) = convertIkind ik in Tint(sz, sg, convertAttr a) - | C.TFloat(fk, a) -> - Tfloat(convertFkind fk, convertAttr a) - | C.TPtr(ty, a) -> - begin match Cutil.unroll env ty with - | C.TStruct(id, _) when List.mem id seen -> - Tcomp_ptr(intern_string ("struct " ^ id.name), convertAttr a) - | C.TUnion(id, _) when List.mem id seen -> - Tcomp_ptr(intern_string ("union " ^ id.name), convertAttr a) - | _ -> - Tpointer(convertTyp seen ty, convertAttr a) - end - | C.TArray(ty, None, a) -> - (* Cparser verified that the type ty[] occurs only in - contexts that are safe for Clight, so just treat as ty[0]. *) - (* warning "array type of unspecified size"; *) - Tarray(convertTyp seen ty, coqint_of_camlint 0l, convertAttr a) - | C.TArray(ty, Some sz, a) -> - Tarray(convertTyp seen ty, convertInt sz, convertAttr a) - | C.TFun(tres, targs, va, a) -> - if Cutil.is_composite_type env tres then - unsupported "return type is a struct or union (consider adding option -fstruct-return)"; - Tfunction(begin match targs with - | None -> Tnil - | Some tl -> convertParams seen tl - end, - convertTyp seen tres, - convertCallconv va a) - | C.TNamed _ -> - assert false - | C.TStruct(id, a) -> - let a' = convertAttr a in - begin try - merge_attributes (Hashtbl.find compositeCache id) a' - with Not_found -> - let flds = - try - convertFields (id :: seen) (Env.find_struct env id) - with Env.Error e -> - error (Env.error_message e); Fnil in - Tstruct(intern_string("struct " ^ id.name), flds, a') - end - | C.TUnion(id, a) -> - let a' = convertAttr a in - begin try - merge_attributes (Hashtbl.find compositeCache id) a' - with Not_found -> - let flds = - try - convertFields (id :: seen) (Env.find_union env id) - with Env.Error e -> - error (Env.error_message e); Fnil in - Tunion(intern_string("union " ^ id.name), flds, a') - end - | C.TEnum(id, a) -> - let (sg, sz) = convertIkind Cutil.enum_ikind in - Tint(sz, sg, convertAttr a) - - and convertParams seen = function +let rec convertTyp env t = + match t with + | C.TVoid a -> Tvoid + | C.TInt(C.ILongLong, a) -> + Tlong(Signed, convertAttr a) + | C.TInt(C.IULongLong, a) -> + Tlong(Unsigned, convertAttr a) + | C.TInt(ik, a) -> + let (sg, sz) = convertIkind ik in Tint(sz, sg, convertAttr a) + | C.TFloat(fk, a) -> + Tfloat(convertFkind fk, convertAttr a) + | C.TPtr(ty, a) -> + Tpointer(convertTyp env ty, convertAttr a) + | C.TArray(ty, None, a) -> + (* Cparser verified that the type ty[] occurs only in + contexts that are safe for Clight, so just treat as ty[0]. *) + (* warning "array type of unspecified size"; *) + Tarray(convertTyp env ty, coqint_of_camlint 0l, convertAttr a) + | C.TArray(ty, Some sz, a) -> + Tarray(convertTyp env ty, convertInt sz, convertAttr a) + | C.TFun(tres, targs, va, a) -> + if Cutil.is_composite_type env tres then + unsupported "return type is a struct or union (consider adding option -fstruct-return)"; + Tfunction(begin match targs with + | None -> Tnil + | Some tl -> convertParams env tl + end, + convertTyp env tres, + convertCallconv va a) + | C.TNamed _ -> + convertTyp env (Cutil.unroll env t) + | C.TStruct(id, a) -> + Tstruct(intern_string id.name, convertAttr a) + | C.TUnion(id, a) -> + Tunion(intern_string id.name, convertAttr a) + | C.TEnum(id, a) -> + let (sg, sz) = convertIkind Cutil.enum_ikind in + Tint(sz, sg, convertAttr a) + +and convertParams env = function | [] -> Tnil - | (id, ty) :: rem -> - Tcons(convertTyp seen ty, convertParams seen rem) - - and convertFields seen ci = - convertFieldList seen ci.Env.ci_members - - and convertFieldList seen = function - | [] -> Fnil - | f :: fl -> - Fcons(intern_string f.fld_name, convertTyp seen f.fld_typ, - convertFieldList seen fl) - - in convertTyp [] t + | (id, ty) :: rem -> Tcons(convertTyp env ty, convertParams env rem) let rec convertTypArgs env tl el = match tl, el with @@ -450,12 +388,16 @@ let rec convertTypArgs env tl el = | (id, t1) :: tl, e1 :: el -> Tcons(convertTyp env t1, convertTypArgs env tl el) -let cacheCompositeDef env su id attr flds = - let ty = - match su with - | C.Struct -> C.TStruct(id, attr) - | C.Union -> C.TUnion(id, attr) in - Hashtbl.add compositeCache id (convertTyp env ty) +let convertField env f = + if f.fld_bitfield <> None then + unsupported "bit field in struct or union (consider adding option -fbitfields)"; + (intern_string f.fld_name, convertTyp env f.fld_typ) + +let convertCompositedef env su id attr members = + Composite(intern_string id.name, + begin match su with C.Struct -> Struct | C.Union -> Union end, + List.map (convertField env) members, + convertAttr attr) let rec projFunType env ty = match Cutil.unroll env ty with @@ -958,7 +900,8 @@ and convertInitList env il = | i :: il' -> Init_cons(convertInit env i, convertInitList env il') let convertInitializer env ty i = - match Initializers.transl_init (convertTyp env ty) (convertInit env i) + match Initializers.transl_init + !comp_env (convertTyp env ty) (convertInit env i) with | Errors.OK init -> init | Errors.Error msg -> @@ -970,8 +913,8 @@ let convertInitializer env ty i = let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in let ty' = convertTyp env ty in - let sz = Ctypes.sizeof ty' in - let al = Ctypes.alignof ty' in + let sz = Ctypes.sizeof !comp_env ty' in + let al = Ctypes.alignof !comp_env ty' in let attr = Cutil.attributes_of_type env ty in let init' = match optinit with @@ -998,16 +941,6 @@ let convertGlobvar loc env (sto, id, ty, optinit) = (id', Gvar {gvar_info = ty'; gvar_init = init'; gvar_readonly = readonly; gvar_volatile = volatile}) -(** Sanity checks on composite declarations. *) - -let checkComposite env si id attr flds = - let checkField f = - if f.fld_bitfield <> None then - unsupported "bit field in struct or union (consider adding option -fbitfields)" in - List.iter checkField flds; - if Cutil.find_custom_attributes ["packed";"__packed__"] attr <> [] then - unsupported "packed struct (consider adding option -fpacked-struct)" - (** Convert a list of global declarations. Result is a list of CompCert C global declarations (functions + variables). *) @@ -1031,21 +964,31 @@ let rec convertGlobdecls env res gl = end | C.Gfundef fd -> convertGlobdecls env (convertFundef g.gloc env fd :: res) gl' - | C.Gcompositedecl _ | C.Gtypedef _ | C.Genumdef _ -> - (* typedefs are unrolled, structs are expanded inline, and - enum tags are folded. So we just skip their declarations. *) - convertGlobdecls env res gl' - | C.Gcompositedef(su, id, attr, flds) -> - (* sanity checks on fields *) - checkComposite env su id attr flds; - (* convert it to a CompCert C type and cache this type *) - cacheCompositeDef env su id attr flds; + | C.Gcompositedecl _ | C.Gcompositedef _ | C.Gtypedef _ | C.Genumdef _ -> + (* Composites are treated in a separate pass, + typedefs are unrolled, and enum tags are folded. + So we just skip their declarations. *) convertGlobdecls env res gl' | C.Gpragma s -> if not (!process_pragma_hook s) then warning ("'#pragma " ^ s ^ "' directive ignored"); convertGlobdecls env res gl' +(** Convert struct and union declarations. + Result is a list of CompCert C composite declarations. *) + +let rec convertCompositedefs env res gl = + match gl with + | [] -> List.rev res + | g :: gl' -> + updateLoc g.gloc; + match g.gdesc with + | C.Gcompositedef(su, id, a, m) -> + convertCompositedefs env + (convertCompositedef env su id a m :: res) gl' + | _ -> + convertCompositedefs env res gl' + (** Build environment of typedefs, structs, unions and enums *) let rec translEnv env = function @@ -1130,17 +1073,29 @@ let convertProgram p = stringNum := 0; Hashtbl.clear decl_atom; Hashtbl.clear stringTable; - Hashtbl.clear compositeCache; - let p = Builtins.declarations() @ p in + let p = cleanupGlobals (Builtins.declarations() @ p) in try - let gl1 = convertGlobdecls (translEnv Env.empty p) [] (cleanupGlobals p) in - let gl2 = globals_for_strings gl1 in - let p' = { AST.prog_defs = gl2; - AST.prog_public = public_globals gl2; - AST.prog_main = intern_string "main" } in - if !numErrors > 0 - then None - else Some p' + let env = translEnv Env.empty p in + let typs = convertCompositedefs env [] p in + match build_composite_env typs with + | Errors.Error msg -> + error (sprintf "Incorrect struct or union definition: %s" + (string_of_errmsg msg)); + None + | Errors.OK ce -> + comp_env := ce; + let gl1 = convertGlobdecls env [] p in + let gl2 = globals_for_strings gl1 in + comp_env := Maps.PTree.empty; + let p' = + { prog_defs = gl2; + prog_public = public_globals gl2; + prog_main = intern_string "main"; + prog_types = typs; + prog_comp_env = ce } in + if !numErrors > 0 + then None + else Some p' with Env.Error msg -> error (Env.error_message msg); None diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 5c062158..952d148d 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -284,31 +284,31 @@ Definition do_deref_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) : o end. Definition assign_copy_ok (ty: type) (b: block) (ofs: int) (b': block) (ofs': int) : Prop := - (alignof_blockcopy ty | Int.unsigned ofs') /\ (alignof_blockcopy ty | Int.unsigned ofs) /\ + (alignof_blockcopy ge ty | Int.unsigned ofs') /\ (alignof_blockcopy ge ty | Int.unsigned ofs) /\ (b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs - \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs - \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs'). + \/ Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs + \/ Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs'). Remark check_assign_copy: forall (ty: type) (b: block) (ofs: int) (b': block) (ofs': int), { assign_copy_ok ty b ofs b' ofs' } + {~ assign_copy_ok ty b ofs b' ofs' }. Proof with try (right; intuition omega). intros. unfold assign_copy_ok. - assert (alignof_blockcopy ty > 0) by apply alignof_blockcopy_pos. - destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs')); auto... - destruct (Zdivide_dec (alignof_blockcopy ty) (Int.unsigned ofs)); auto... + assert (alignof_blockcopy ge ty > 0) by apply alignof_blockcopy_pos. + destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs')); auto... + destruct (Zdivide_dec (alignof_blockcopy ge ty) (Int.unsigned ofs)); auto... assert (Y: {b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs \/ - Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/ - Int.unsigned ofs + sizeof ty <= Int.unsigned ofs'} + + Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs \/ + Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs'} + {~(b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs \/ - Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs \/ - Int.unsigned ofs + sizeof ty <= Int.unsigned ofs')}). + Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs \/ + Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs')}). destruct (eq_block b' b); auto. destruct (zeq (Int.unsigned ofs') (Int.unsigned ofs)); auto. - destruct (zle (Int.unsigned ofs' + sizeof ty) (Int.unsigned ofs)); auto. - destruct (zle (Int.unsigned ofs + sizeof ty) (Int.unsigned ofs')); auto. + destruct (zle (Int.unsigned ofs' + sizeof ge ty) (Int.unsigned ofs)); auto. + destruct (zle (Int.unsigned ofs + sizeof ge ty) (Int.unsigned ofs')); auto. right; intuition omega. destruct Y... left; intuition omega. Defined. @@ -324,7 +324,7 @@ Definition do_assign_loc (w: world) (ty: type) (m: mem) (b: block) (ofs: int) (v match v with | Vptr b' ofs' => if check_assign_copy ty b ofs b' ofs' then - do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty); + do bytes <- Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ge ty); do m' <- Mem.storebytes m b (Int.unsigned ofs) bytes; Some(w, E0, m') else None @@ -746,12 +746,14 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r with | Some(Vptr b ofs, ty') => match ty' with - | Tstruct id fList _ => - match field_offset f fList with + | Tstruct id _ => + do co <- ge.(genv_cenv)!id; + match field_offset ge f (co_members co) with | Error _ => stuck | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m) end - | Tunion id fList _ => + | Tunion id _ => + do co <- ge.(genv_cenv)!id; topred (Lred (Eloc b ofs ty) m) | _ => stuck end @@ -787,7 +789,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Ebinop op r1 r2 ty => match is_val r1, is_val r2 with | Some(v1, ty1), Some(v2, ty2) => - do v <- sem_binary_operation op v1 ty1 v2 ty2 m; + do v <- sem_binary_operation ge op v1 ty1 v2 ty2 m; topred (Rred (Eval v ty) m E0) | _, _ => incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m) @@ -828,9 +830,9 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) end | RV, Esizeof ty' ty => - topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m E0) + topred (Rred (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0) | RV, Ealignof ty' ty => - topred (Rred (Eval (Vint (Int.repr (alignof ty'))) ty) m E0) + topred (Rred (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0) | RV, Eassign l1 r2 ty => match is_loc l1, is_val r2 with | Some(b, ofs, ty1), Some(v2, ty2) => @@ -988,8 +990,8 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Efield (Eval v ty1) f ty => exists b, exists ofs, v = Vptr b ofs /\ match ty1 with - | Tstruct _ fList _ => exists delta, field_offset f fList = Errors.OK delta - | Tunion _ _ _ => True + | Tstruct id _ => exists co delta, ge.(genv_cenv)!id = Some co /\ field_offset ge f (co_members co) = OK delta + | Tunion id _ => exists co, ge.(genv_cenv)!id = Some co | _ => False end | Eval v ty => False @@ -998,7 +1000,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Eunop op (Eval v1 ty1) ty => exists v, sem_unary_operation op v1 ty1 = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => - exists v, sem_binary_operation op v1 ty1 v2 ty2 m = Some v + exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => exists v, sem_cast v1 ty1 ty = Some v | Eseqand (Eval v1 ty1) r2 ty => @@ -1043,8 +1045,8 @@ Proof. exists b; auto. exists b; auto. exists b; exists ofs; auto. - exists b; exists ofs; split; auto. exists delta; auto. - exists b; exists ofs; auto. + exists b; exists ofs; split; auto. exists co, delta; auto. + exists b; exists ofs; split; auto. exists co; auto. Qed. Lemma rred_invert: @@ -1385,10 +1387,12 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct v... destruct ty'... (* top struct *) - destruct (field_offset f f0) as [delta|] eqn:?... - apply topred_ok; auto. apply red_field_struct; auto. + destruct (ge.(genv_cenv)!i0) as [co|] eqn:?... + destruct (field_offset ge f (co_members co)) as [delta|] eqn:?... + apply topred_ok; auto. eapply red_field_struct; eauto. (* top union *) - apply topred_ok; auto. apply red_field_union; auto. + destruct (ge.(genv_cenv)!i0) as [co|] eqn:?... + apply topred_ok; auto. eapply red_field_union; eauto. (* in depth *) eapply incontext_ok; eauto. (* Evalof *) @@ -1425,7 +1429,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct (is_val a2) as [[v2 ty2] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). (* top *) - destruct (sem_binary_operation op v1 ty1 v2 ty2 m) as [v|] eqn:?... + destruct (sem_binary_operation ge op v1 ty1 v2 ty2 m) as [v|] eqn:?... apply topred_ok; auto. split. apply red_binop; auto. exists w; constructor. (* depth *) eapply incontext2_ok; eauto. @@ -1589,9 +1593,9 @@ Proof. (* deref *) auto. (* field struct *) - rewrite H; auto. + rewrite H, H0; auto. (* field union *) - auto. + rewrite H; auto. Qed. Lemma rred_topred: @@ -1895,21 +1899,21 @@ Fixpoint do_alloc_variables (e: env) (m: mem) (l: list (ident * type)) {struct l match l with | nil => (e,m) | (id, ty) :: l' => - let (m1,b1) := Mem.alloc m 0 (sizeof ty) in + let (m1,b1) := Mem.alloc m 0 (sizeof ge ty) in do_alloc_variables (PTree.set id (b1, ty) e) m1 l' end. Lemma do_alloc_variables_sound: - forall l e m, alloc_variables e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)). + forall l e m, alloc_variables ge e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)). Proof. induction l; intros; simpl. constructor. - destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ty)) as [m1 b1] eqn:?; simpl. + destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ge ty)) as [m1 b1] eqn:?; simpl. econstructor; eauto. Qed. Lemma do_alloc_variables_complete: - forall e1 m1 l e2 m2, alloc_variables e1 m1 l e2 m2 -> + forall e1 m1 l e2 m2, alloc_variables ge e1 m1 l e2 m2 -> do_alloc_variables e1 m1 l = (e2, m2). Proof. induction 1; simpl. @@ -1985,7 +1989,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) := if b then ret (State f s (Kfor3 a2 a3 s k) e m) else ret (State f Sskip k e m) | Kreturn k => do v' <- sem_cast v ty f.(fn_return); - do m' <- Mem.free_list m (blocks_of_env e); + do m' <- Mem.free_list m (blocks_of_env ge e); ret (Returnstate v' (call_cont k) m') | Kswitch1 sl k => do n <- sem_switch_arg v ty; @@ -2024,11 +2028,11 @@ Definition do_step (w: world) (s: state) : list (trace * state) := | State f Sskip (Kfor4 a2 a3 s k) e m => ret (State f (Sfor Sskip a2 a3 s) k e m) | State f (Sreturn None) k e m => - do m' <- Mem.free_list m (blocks_of_env e); + do m' <- Mem.free_list m (blocks_of_env ge e); ret (Returnstate Vundef (call_cont k) m') | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m) | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => - do m' <- Mem.free_list m (blocks_of_env e); + do m' <- Mem.free_list m (blocks_of_env ge e); ret (Returnstate Vundef k m') | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m) @@ -2209,7 +2213,7 @@ End EXEC. Local Open Scope option_monad_scope. Definition do_initial_state (p: program): option (genv * state) := - let ge := Genv.globalenv p in + let ge := globalenv p in do m0 <- Genv.init_mem p; do b <- Genv.find_symbol ge p.(prog_main); do f <- Genv.find_funct_ptr ge b; diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 40206d38..7a45b453 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -57,12 +57,9 @@ Inductive expr : Type := | Eunop: unary_operation -> expr -> type -> expr (**r unary operation *) | Ebinop: binary_operation -> expr -> expr -> type -> expr (**r binary operation *) | Ecast: expr -> type -> expr (**r type cast ([(ty) e]) *) - | Efield: expr -> ident -> type -> expr. (**r access to a member of a struct or union *) - -(** [sizeof] and [alignof] are derived forms. *) - -Definition Esizeof (ty' ty: type) : expr := Econst_int (Int.repr(sizeof ty')) ty. -Definition Ealignof (ty' ty: type) : expr := Econst_int (Int.repr(alignof ty')) ty. + | Efield: expr -> ident -> type -> expr (**r access to a member of a struct or union *) + | Esizeof: type -> type -> expr (**r size of a type *) + | Ealignof: type -> type -> expr. (**r alignment of a type *) (** Extract the type part of a type-annotated Clight expression. *) @@ -80,6 +77,8 @@ Definition typeof (e: expr) : type := | Ebinop _ _ _ ty => ty | Ecast _ ty => ty | Efield _ _ ty => ty + | Esizeof _ ty => ty + | Ealignof _ ty => ty end. (** ** Statements *) @@ -164,19 +163,57 @@ Definition type_of_fundef (f: fundef) : type := (** ** Programs *) -(** A program is a collection of named functions, plus a collection - of named global variables, carrying their types and optional initialization - data. See module [AST] for more details. *) +(** A program is composed of: +- a list of definitions of functions and global variables; +- the names of functions and global variables that are public (not static); +- the name of the function that acts as entry point ("main" function). +- a list of definitions for structure and union names; +- the corresponding composite environment; +*) + +Record program : Type := { + prog_defs: list (ident * globdef fundef type); + prog_public: list ident; + prog_main: ident; + prog_types: list composite_definition; + prog_comp_env: composite_env; + prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env +}. -Definition program : Type := AST.program fundef type. +Definition program_of_program (p: program) : AST.program fundef type := + {| AST.prog_defs := p.(prog_defs); + AST.prog_public := p.(prog_public); + AST.prog_main := p.(prog_main) |}. + +Coercion program_of_program: program >-> AST.program. + +Program Definition make_program (types: list composite_definition) + (defs: list (ident * globdef fundef type)) + (public: list ident) + (main: ident): res program := + match build_composite_env types with + | OK env => + OK {| prog_defs := defs; + prog_public := public; + prog_main := main; + prog_types := types; + prog_comp_env := env; + prog_comp_env_eq := _ |} + | Error msg => + Error msg + end. (** * Operational semantics *) (** The semantics uses two environments. The global environment maps names of functions and global variables to memory block references, - and function pointers to their definitions. (See module [Globalenvs].) *) + and function pointers to their definitions. (See module [Globalenvs].) + It also contains a composite environment, used by type-dependent operations. *) -Definition genv := Genv.t fundef type. +Record genv := { genv_genv :> Genv.t fundef type; genv_cenv :> composite_env }. + +Definition globalenv (p: program) := + {| genv_genv := Genv.globalenv p; genv_cenv := p.(prog_comp_env) |}. (** The local environment maps local variables to block references and types. The current value of the variable is stored in the @@ -214,22 +251,26 @@ Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : val -> Prop := This is allowed only if [ty] indicates an access by value or by copy. [m'] is the updated memory state. *) -Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int): +Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: int): val -> mem -> Prop := | assign_loc_value: forall v chunk m', access_mode ty = By_value chunk -> Mem.storev chunk m (Vptr b ofs) v = Some m' -> - assign_loc ty m b ofs v m' + assign_loc ce ty m b ofs v m' | assign_loc_copy: forall b' ofs' bytes m', access_mode ty = By_copy -> - (sizeof ty > 0 -> (alignof_blockcopy ty | Int.unsigned ofs')) -> - (sizeof ty > 0 -> (alignof_blockcopy ty | Int.unsigned ofs)) -> + (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Int.unsigned ofs')) -> + (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Int.unsigned ofs)) -> b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs - \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs - \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs' -> - Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty) = Some bytes -> + \/ Int.unsigned ofs' + sizeof ce ty <= Int.unsigned ofs + \/ Int.unsigned ofs + sizeof ce ty <= Int.unsigned ofs' -> + Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ce ty) = Some bytes -> Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' -> - assign_loc ty m b ofs (Vptr b' ofs') m'. + assign_loc ce ty m b ofs (Vptr b' ofs') m'. + +Section SEMANTICS. + +Variable ge: genv. (** Allocation of function-local variables. [alloc_variables e1 m1 vars e2 m2] allocates one memory block @@ -246,7 +287,7 @@ Inductive alloc_variables: env -> mem -> alloc_variables e m nil e m | alloc_variables_cons: forall e m id ty vars m1 b1 m2 e2, - Mem.alloc m 0 (sizeof ty) = (m1, b1) -> + Mem.alloc m 0 (sizeof ge ty) = (m1, b1) -> alloc_variables (PTree.set id (b1, ty) e) m1 vars e2 m2 -> alloc_variables e m ((id, ty) :: vars) e2 m2. @@ -264,7 +305,7 @@ Inductive bind_parameters (e: env): | bind_parameters_cons: forall m id ty params v1 vl b m1 m2, PTree.get id e = Some(b, ty) -> - assign_loc ty m b Int.zero v1 m1 -> + assign_loc ge ty m b Int.zero v1 m1 -> bind_parameters e m1 params vl m2 -> bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. @@ -289,7 +330,7 @@ Fixpoint bind_parameter_temps (formals: list (ident * type)) (args: list val) (** Return the list of blocks in the codomain of [e], with low and high bounds. *) Definition block_of_binding (id_b_ty: ident * (block * type)) := - match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ty) end. + match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ge ty) end. Definition blocks_of_env (e: env) : list (block * Z * Z) := List.map block_of_binding (PTree.elements e). @@ -333,10 +374,6 @@ Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement := | LScons _ s sl' => Ssequence s (seq_of_labeled_statement sl') end. -Section SEMANTICS. - -Variable ge: genv. - (** ** Evaluation of expressions *) Section EXPR. @@ -371,12 +408,16 @@ Inductive eval_expr: expr -> val -> Prop := | eval_Ebinop: forall op a1 a2 ty v1 v2 v, eval_expr a1 v1 -> eval_expr a2 v2 -> - sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v -> + sem_binary_operation ge op v1 (typeof a1) v2 (typeof a2) m = Some v -> 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 -> eval_expr (Ecast a ty) v + | eval_Esizeof: forall ty1 ty, + eval_expr (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) + | eval_Ealignof: forall ty1 ty, + eval_expr (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))) | eval_Elvalue: forall a loc ofs v, eval_lvalue a loc ofs -> deref_loc (typeof a) m loc ofs v -> @@ -397,14 +438,16 @@ with eval_lvalue: expr -> block -> int -> Prop := | eval_Ederef: forall a ty l ofs, eval_expr a (Vptr l ofs) -> eval_lvalue (Ederef a ty) l ofs - | eval_Efield_struct: forall a i ty l ofs id fList att delta, + | eval_Efield_struct: forall a i ty l ofs id co att delta, eval_expr a (Vptr l ofs) -> - typeof a = Tstruct id fList att -> - field_offset i fList = OK delta -> + typeof a = Tstruct id att -> + ge.(genv_cenv)!id = Some co -> + field_offset ge i (co_members co) = OK delta -> eval_lvalue (Efield a i ty) l (Int.add ofs (Int.repr delta)) - | eval_Efield_union: forall a i ty l ofs id fList att, + | eval_Efield_union: forall a i ty l ofs id co att, eval_expr a (Vptr l ofs) -> - typeof a = Tunion id fList att -> + typeof a = Tunion id att -> + ge.(genv_cenv)!id = Some co -> eval_lvalue (Efield a i ty) l ofs. Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop @@ -538,7 +581,7 @@ Inductive step: state -> trace -> state -> Prop := eval_lvalue e le m a1 loc ofs -> eval_expr e le m a2 v2 -> sem_cast v2 (typeof a2) (typeof a1) = Some v -> - assign_loc (typeof a1) m loc ofs v m' -> + 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') @@ -676,45 +719,48 @@ End SEMANTICS. (** The two semantics for function parameters. First, parameters as local variables. *) -Inductive function_entry1 (f: function) (vargs: list val) (m: mem) (e: env) (le: temp_env) (m': mem) : Prop := +Inductive function_entry1 (ge: genv) (f: function) (vargs: list val) (m: mem) (e: env) (le: temp_env) (m': mem) : Prop := | function_entry1_intro: forall m1, list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> - alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> - bind_parameters e m1 f.(fn_params) vargs m' -> + alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> + bind_parameters ge e m1 f.(fn_params) vargs m' -> le = create_undef_temps f.(fn_temps) -> - function_entry1 f vargs m e le m'. + function_entry1 ge f vargs m e le m'. -Definition step1 (ge: genv) := step ge function_entry1. +Definition step1 (ge: genv) := step ge (function_entry1 ge). (** Second, parameters as temporaries. *) -Inductive function_entry2 (f: function) (vargs: list val) (m: mem) (e: env) (le: temp_env) (m': mem) : Prop := +Inductive function_entry2 (ge: genv) (f: function) (vargs: list val) (m: mem) (e: env) (le: temp_env) (m': mem) : Prop := | function_entry2_intro: list_norepet (var_names f.(fn_vars)) -> list_norepet (var_names f.(fn_params)) -> list_disjoint (var_names f.(fn_params)) (var_names f.(fn_temps)) -> - alloc_variables empty_env m f.(fn_vars) e m' -> + alloc_variables ge empty_env m f.(fn_vars) e m' -> bind_parameter_temps f.(fn_params) vargs (create_undef_temps f.(fn_temps)) = Some le -> - function_entry2 f vargs m e le m'. + function_entry2 ge f vargs m e le m'. -Definition step2 (ge: genv) := step ge function_entry2. +Definition step2 (ge: genv) := step ge (function_entry2 ge). (** Wrapping up these definitions in two small-step semantics. *) Definition semantics1 (p: program) := - Semantics step1 (initial_state p) final_state (Genv.globalenv p). + let ge := globalenv p in + Semantics_gen step1 (initial_state p) final_state ge ge. Definition semantics2 (p: program) := - Semantics step2 (initial_state p) final_state (Genv.globalenv p). + let ge := globalenv p in + Semantics_gen step2 (initial_state p) final_state ge ge. (** This semantics is receptive to changes in events. *) Lemma semantics_receptive: forall (p: program), receptive (semantics1 p). Proof. - intros. constructor; simpl; intros. + intros. unfold semantics1. + set (ge := globalenv p). constructor; simpl; intros. (* receptiveness *) - assert (t1 = E0 -> exists s2, step1 (Genv.globalenv p) s t2 s2). + assert (t1 = E0 -> exists s2, step1 ge s t2 s2). intros. subst. inv H0. exists s1; auto. inversion H; subst; auto. (* builtin *) @@ -724,7 +770,7 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate vres2 k m2). econstructor; eauto. (* trace length *) - red; intros. inv H; simpl; try omega. + red; simpl; intros. inv H; simpl; try omega. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. Qed. diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index d61e4eef..5b092db7 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -82,7 +82,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> 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 -> - assign_loc (typeof a1) m loc ofs v m' -> + assign_loc ge (typeof a1) m loc ofs v m' -> exec_stmt e le m (Sassign a1 a2) E0 le m' Out_normal | exec_Sset: forall e le m id a v, @@ -164,12 +164,12 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := | eval_funcall_internal: forall le m f vargs t e m1 m2 m3 out vres m4, - alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> + alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> - bind_parameters e m1 f.(fn_params) vargs m2 -> + 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 -> - Mem.free_list m3 (blocks_of_env e) = Some m4 -> + 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', external_call ef ge vargs m t vres m' -> @@ -232,9 +232,9 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop := | evalinf_funcall_internal: forall m f vargs t e m1 m2, - alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> + alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> - bind_parameters e m1 f.(fn_params) vargs m2 -> + bind_parameters ge e m1 f.(fn_params) vargs m2 -> execinf_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t -> evalinf_funcall m (Internal f) vargs t. @@ -244,7 +244,7 @@ End BIGSTEP. Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := | bigstep_program_terminates_intro: forall b f m0 m1 t r, - let ge := Genv.globalenv p in + let ge := globalenv p in Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> @@ -254,7 +254,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Inductive bigstep_program_diverges (p: program): traceinf -> Prop := | bigstep_program_diverges_intro: forall b f m0 t, - let ge := Genv.globalenv p in + let ge := globalenv p in Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> @@ -270,7 +270,7 @@ Definition bigstep_semantics (p: program) := Section BIGSTEP_TO_TRANSITIONS. Variable prog: program. -Let ge : genv := Genv.globalenv prog. +Let ge : genv := globalenv prog. Inductive outcome_state_match (e: env) (le: temp_env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop := diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index a5d4c662..4e572277 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -93,17 +93,17 @@ Inductive classify_cast_cases : Type := | cast_case_s2bool (**r single -> bool *) | cast_case_l2bool (**r long -> bool *) | cast_case_p2bool (**r pointer -> bool *) - | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r struct -> struct *) - | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r union -> union *) + | cast_case_struct (id1 id2: ident) (**r struct -> struct *) + | cast_case_union (id1 id2: ident) (**r union -> union *) | cast_case_void (**r any -> void *) | cast_case_default. Definition classify_cast (tfrom tto: type) : classify_cast_cases := match tto, tfrom with - | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral + | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral | Tint IBool _ _, Tfloat F64 _ => cast_case_f2bool | Tint IBool _ _, Tfloat F32 _ => cast_case_s2bool - | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool + | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_p2bool | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2 | Tint sz2 si2 _, Tfloat F64 _ => cast_case_f2i sz2 si2 | Tint sz2 si2 _, Tfloat F32 _ => cast_case_s2i sz2 si2 @@ -113,7 +113,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases := | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s | Tfloat F64 _, Tint sz1 si1 _ => cast_case_i2f si1 | Tfloat F32 _, Tint sz1 si1 _ => cast_case_i2s si1 - | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral + | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_neutral | Tlong _ _, Tlong _ _ => cast_case_l2l | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1 | Tint IBool _ _, Tlong _ _ => cast_case_l2bool @@ -122,10 +122,10 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases := | Tlong si2 _, Tfloat F32 _ => cast_case_s2l si2 | Tfloat F64 _, Tlong si1 _ => cast_case_l2f si1 | Tfloat F32 _, Tlong si1 _ => cast_case_l2s si1 - | (Tpointer _ _ | Tcomp_ptr _ _), Tlong _ _ => cast_case_l2i I32 Unsigned - | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2 - | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2 - | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2 + | Tpointer _ _, Tlong _ _ => cast_case_l2i I32 Unsigned + | Tlong si2 _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_i2l si2 + | Tstruct id2 _, Tstruct id1 _ => cast_case_struct id1 id2 + | Tunion id2 _, Tunion id1 _ => cast_case_union id1 id2 | Tvoid, _ => cast_case_void | _, _ => cast_case_default end. @@ -325,16 +325,16 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := end | _ => None end - | cast_case_struct id1 fld1 id2 fld2 => + | cast_case_struct id1 id2 => match v with | Vptr b ofs => - if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None + if ident_eq id1 id2 then Some v else None | _ => None end - | cast_case_union id1 fld1 id2 fld2 => + | cast_case_union id1 id2 => match v with | Vptr b ofs => - if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None + if ident_eq id1 id2 then Some v else None | _ => None end | cast_case_void => @@ -359,7 +359,7 @@ Inductive classify_bool_cases : Type := Definition classify_bool (ty: type) : classify_bool_cases := match typeconv ty with | Tint _ _ _ => bool_case_i - | Tpointer _ _ | Tcomp_ptr _ _ => bool_case_p + | Tpointer _ _ => bool_case_p | Tfloat F64 _ => bool_case_f | Tfloat F32 _ => bool_case_s | Tlong _ _ => bool_case_l @@ -402,7 +402,6 @@ Definition bool_val (v: val) (t: type) : option bool := | bool_default => None end. - (** ** Unary operators *) (** *** Boolean negation *) @@ -639,32 +638,32 @@ Definition classify_add (ty1: type) (ty2: type) := | _, _ => add_default end. -Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val := match classify_add t1 t2 with | add_case_pi ty => (**r pointer plus integer *) match v1,v2 with | Vptr b1 ofs1, Vint n2 => - Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None end | add_case_ip ty => (**r integer plus pointer *) match v1,v2 with | Vint n1, Vptr b2 ofs2 => - Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1))) + Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) | _, _ => None end | add_case_pl ty => (**r pointer plus long *) match v1,v2 with | Vptr b1 ofs1, Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in - Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None end | add_case_lp ty => (**r long plus pointer *) match v1,v2 with | Vlong n1, Vptr b2 ofs2 => let n1 := Int.repr (Int64.unsigned n1) in - Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1))) + Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) | _, _ => None end | add_default => @@ -692,27 +691,27 @@ Definition classify_sub (ty1: type) (ty2: type) := | _, _ => sub_default end. -Definition sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val := match classify_sub t1 t2 with | sub_case_pi ty => (**r pointer minus integer *) match v1,v2 with | Vptr b1 ofs1, Vint n2 => - Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None end | sub_case_pl ty => (**r pointer minus long *) match v1,v2 with | Vptr b1 ofs1, Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in - Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None end | sub_case_pp ty => (**r pointer minus pointer *) match v1,v2 with | Vptr b1 ofs1, Vptr b2 ofs2 => if eq_block b1 b2 then - if Int.eq (Int.repr (sizeof ty)) Int.zero then None - else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty)))) + if Int.eq (Int.repr (sizeof cenv ty)) Int.zero then None + else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof cenv ty)))) else None | _, _ => None end @@ -983,12 +982,13 @@ Definition sem_unary_operation end. Definition sem_binary_operation + (cenv: composite_env) (op: binary_operation) (v1: val) (t1: type) (v2: val) (t2:type) (m: mem): option val := match op with - | Oadd => sem_add v1 t1 v2 t2 - | Osub => sem_sub v1 t1 v2 t2 + | 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 @@ -1005,10 +1005,10 @@ Definition sem_binary_operation | Oge => sem_cmp Cge v1 t1 v2 t2 m end. -Definition sem_incrdecr (id: incr_or_decr) (v: val) (ty: type) := +Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) := match id with - | Incr => sem_add v ty (Vint Int.one) type_int32s - | Decr => sem_sub v ty (Vint Int.one) type_int32s + | Incr => sem_add cenv v ty (Vint Int.one) type_int32s + | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s end. Definition incrdecr_type (ty: type) := @@ -1086,8 +1086,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 (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. -- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto. +- destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto. +- destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto. - econstructor; eauto. Qed. @@ -1191,10 +1191,10 @@ Proof. Qed. Lemma sem_binary_operation_inj: - forall op v1 ty1 v2 ty2 v tv1 tv2, - sem_binary_operation op v1 ty1 v2 ty2 m = Some v -> + forall cenv op v1 ty1 v2 ty2 v tv1 tv2, + sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> val_inject f v1 tv1 -> val_inject f v2 tv2 -> - exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. Proof. unfold sem_binary_operation; intros; destruct op. - (* add *) @@ -1215,7 +1215,7 @@ Proof. + inv H0; inv H1; inv H. TrivialInject. destruct (eq_block b1 b0); try discriminate. subst b1. rewrite H0 in H2; inv H2. rewrite dec_eq_true. - destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H3. + destruct (Int.eq (Int.repr (sizeof cenv ty)) Int.zero); inv H3. rewrite Int.sub_shifted. TrivialInject. + inv H0; inv H1; inv H. TrivialInject. econstructor. eauto. rewrite Int.sub_add_l. auto. @@ -1278,11 +1278,11 @@ Qed. End GENERIC_INJECTION. Lemma sem_binary_operation_inject: - forall f m m' op v1 ty1 v2 ty2 v tv1 tv2, - sem_binary_operation op v1 ty1 v2 ty2 m = Some v -> + forall f m m' cenv op v1 ty1 v2 ty2 v tv1 tv2, + sem_binary_operation cenv op v1 ty1 v2 ty2 m = Some v -> val_inject f v1 tv1 -> val_inject f v2 tv2 -> Mem.inject f m m' -> - exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. + exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv. Proof. intros. eapply sem_binary_operation_inj; eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. @@ -1309,7 +1309,7 @@ Proof. assert (A: classify_bool t = match t with | Tint _ _ _ => bool_case_i - | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p + | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p | Tfloat F64 _ => bool_case_f | Tfloat F32 _ => bool_case_s | Tlong _ _ => bool_case_l @@ -1332,7 +1332,6 @@ Proof. destruct (Int.eq i Int.zero); auto. destruct (Int.eq i Int.zero); auto. destruct (Int.eq i Int.zero); auto. - destruct (Int.eq i0 Int.zero); auto. Qed. (** Relation between Boolean value and Boolean negation. *) @@ -1528,5 +1527,4 @@ End ArithConv. - diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 06cea006..e6e3a321 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -34,9 +34,13 @@ Require Import Smallstep. (** The semantics uses two environments. The global environment maps names of functions and global variables to memory block references, - and function pointers to their definitions. (See module [Globalenvs].) *) + and function pointers to their definitions. (See module [Globalenvs].) + It also contains a composite environment, used by type-dependent operations. *) -Definition genv := Genv.t fundef type. +Record genv := { genv_genv :> Genv.t fundef type; genv_cenv :> composite_env }. + +Definition globalenv (p: program) := + {| genv_genv := Genv.globalenv p; genv_cenv := p.(prog_comp_env) |}. (** The local environment maps local variables to block references and types. The current value of the variable is stored in the associated memory @@ -46,6 +50,11 @@ Definition env := PTree.t (block * type). (* map variable -> location & type *) Definition empty_env: env := (PTree.empty (block * type)). + +Section SEMANTICS. + +Variable ge: genv. + (** [deref_loc ty m b ofs t v] computes the value of a datum of type [ty] residing in memory [m] at block [b], offset [ofs]. If the type [ty] indicates an access by value, the corresponding @@ -54,22 +63,22 @@ Definition empty_env: env := (PTree.empty (block * type)). returned, and [t] the trace of observables (nonempty if this is a volatile access). *) -Inductive deref_loc {F V: Type} (ge: Genv.t F V) (ty: type) (m: mem) (b: block) (ofs: int) : trace -> val -> Prop := +Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : trace -> val -> Prop := | deref_loc_value: forall chunk v, access_mode ty = By_value chunk -> type_is_volatile ty = false -> Mem.loadv chunk m (Vptr b ofs) = Some v -> - deref_loc ge ty m b ofs E0 v + deref_loc ty m b ofs E0 v | deref_loc_volatile: forall chunk t v, access_mode ty = By_value chunk -> type_is_volatile ty = true -> volatile_load ge chunk m b ofs t v -> - deref_loc ge ty m b ofs t v + deref_loc ty m b ofs t v | deref_loc_reference: access_mode ty = By_reference -> - deref_loc ge ty m b ofs E0 (Vptr b ofs) + deref_loc ty m b ofs E0 (Vptr b ofs) | deref_loc_copy: access_mode ty = By_copy -> - deref_loc ge ty m b ofs E0 (Vptr b ofs). + deref_loc ty m b ofs E0 (Vptr b ofs). (** Symmetrically, [assign_loc ty m b ofs v t m'] returns the memory state after storing the value [v] in the datum @@ -78,27 +87,27 @@ Inductive deref_loc {F V: Type} (ge: Genv.t F V) (ty: type) (m: mem) (b: block) [m'] is the updated memory state and [t] the trace of observables (nonempty if this is a volatile store). *) -Inductive assign_loc {F V: Type} (ge: Genv.t F V) (ty: type) (m: mem) (b: block) (ofs: int): +Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int): val -> trace -> mem -> Prop := | assign_loc_value: forall v chunk m', access_mode ty = By_value chunk -> type_is_volatile ty = false -> Mem.storev chunk m (Vptr b ofs) v = Some m' -> - assign_loc ge ty m b ofs v E0 m' + assign_loc ty m b ofs v E0 m' | assign_loc_volatile: forall v chunk t m', access_mode ty = By_value chunk -> type_is_volatile ty = true -> volatile_store ge chunk m b ofs v t m' -> - assign_loc ge ty m b ofs v t m' + assign_loc ty m b ofs v t m' | assign_loc_copy: forall b' ofs' bytes m', access_mode ty = By_copy -> - (alignof_blockcopy ty | Int.unsigned ofs') -> - (alignof_blockcopy ty | Int.unsigned ofs) -> + (alignof_blockcopy ge ty | Int.unsigned ofs') -> + (alignof_blockcopy ge ty | Int.unsigned ofs) -> b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs - \/ Int.unsigned ofs' + sizeof ty <= Int.unsigned ofs - \/ Int.unsigned ofs + sizeof ty <= Int.unsigned ofs' -> - Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ty) = Some bytes -> + \/ Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs + \/ Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs' -> + Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ge ty) = Some bytes -> Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' -> - assign_loc ge ty m b ofs (Vptr b' ofs') E0 m'. + assign_loc ty m b ofs (Vptr b' ofs') E0 m'. (** Allocation of function-local variables. [alloc_variables e1 m1 vars e2 m2] allocates one memory block @@ -115,7 +124,7 @@ Inductive alloc_variables: env -> mem -> alloc_variables e m nil e m | alloc_variables_cons: forall e m id ty vars m1 b1 m2 e2, - Mem.alloc m 0 (sizeof ty) = (m1, b1) -> + Mem.alloc m 0 (sizeof ge ty) = (m1, b1) -> alloc_variables (PTree.set id (b1, ty) e) m1 vars e2 m2 -> alloc_variables e m ((id, ty) :: vars) e2 m2. @@ -124,23 +133,23 @@ Inductive alloc_variables: env -> mem -> in the memory blocks corresponding to the variables [params]. [m1] is the initial memory state and [m2] the final memory state. *) -Inductive bind_parameters {F V: Type} (ge: Genv.t F V) (e: env): +Inductive bind_parameters (e: env): mem -> list (ident * type) -> list val -> mem -> Prop := | bind_parameters_nil: forall m, - bind_parameters ge e m nil nil m + bind_parameters e m nil nil m | bind_parameters_cons: forall m id ty params v1 vl b m1 m2, PTree.get id e = Some(b, ty) -> - assign_loc ge ty m b Int.zero v1 E0 m1 -> - bind_parameters ge e m1 params vl m2 -> - bind_parameters ge e m ((id, ty) :: params) (v1 :: vl) m2. + assign_loc ty m b Int.zero v1 E0 m1 -> + bind_parameters e m1 params vl m2 -> + bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. (** Return the list of blocks in the codomain of [e], with low and high bounds. *) Definition block_of_binding (id_b_ty: ident * (block * type)) := - match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ty) end. + match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ge ty) end. Definition blocks_of_env (e: env) : list (block * Z * Z) := List.map block_of_binding (PTree.elements e). @@ -185,10 +194,6 @@ Inductive cast_arguments: exprlist -> typelist -> list val -> Prop := sem_cast v ty targ1 = Some v1 -> cast_arguments el targs vl -> cast_arguments (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl). -Section SEMANTICS. - -Variable ge: genv. - (** ** Reduction semantics for expressions *) Section EXPR. @@ -215,19 +220,21 @@ Inductive lred: expr -> mem -> expr -> mem -> Prop := | red_deref: forall b ofs ty1 ty m, lred (Ederef (Eval (Vptr b ofs) ty1) ty) m (Eloc b ofs ty) m - | red_field_struct: forall b ofs id fList a f ty m delta, - field_offset f fList = OK delta -> - lred (Efield (Eval (Vptr b ofs) (Tstruct id fList a)) f ty) m + | red_field_struct: forall b ofs id co a f ty m delta, + ge.(genv_cenv)!id = Some co -> + field_offset ge f (co_members co) = OK delta -> + lred (Efield (Eval (Vptr b ofs) (Tstruct id a)) f ty) m (Eloc b (Int.add ofs (Int.repr delta)) ty) m - | red_field_union: forall b ofs id fList a f ty m, - lred (Efield (Eval (Vptr b ofs) (Tunion id fList a)) f ty) m + | red_field_union: forall b ofs id co a f ty m, + ge.(genv_cenv)!id = Some co -> + lred (Efield (Eval (Vptr b ofs) (Tunion id a)) f ty) m (Eloc b ofs ty) m. (** Head reductions for r-values *) Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := | red_rvalof: forall b ofs ty m t v, - deref_loc ge ty m b ofs t v -> + deref_loc ty m b ofs t v -> rred (Evalof (Eloc b ofs ty) ty) m t (Eval v ty) m | red_addrof: forall b ofs ty1 ty m, @@ -238,7 +245,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Eunop op (Eval v1 ty1) ty) m E0 (Eval v ty) m | red_binop: forall op v1 ty1 v2 ty2 ty m v, - sem_binary_operation op v1 ty1 v2 ty2 m = Some v -> + sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v -> rred (Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty) m E0 (Eval v ty) m | red_cast: forall ty v1 ty1 m v, @@ -267,22 +274,22 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := E0 (Eparen (if b then r1 else r2) ty ty) m | red_sizeof: forall ty1 ty m, rred (Esizeof ty1 ty) m - E0 (Eval (Vint (Int.repr (sizeof ty1))) ty) m + E0 (Eval (Vint (Int.repr (sizeof ge ty1))) ty) m | red_alignof: forall ty1 ty m, rred (Ealignof ty1 ty) m - E0 (Eval (Vint (Int.repr (alignof 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 -> - assign_loc ge ty1 m b ofs v t m' -> + 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' | red_assignop: forall op b ofs ty1 v2 ty2 tyres m t v1, - deref_loc ge ty1 m b ofs t v1 -> + deref_loc ty1 m b ofs t v1 -> rred (Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty1) m t (Eassign (Eloc b ofs ty1) (Ebinop op (Eval v1 ty1) (Eval v2 ty2) tyres) ty1) m | red_postincr: forall id b ofs ty m t v1 op, - deref_loc ge ty m b ofs t v1 -> + deref_loc ty m b ofs t v1 -> op = match id with Incr => Oadd | Decr => Osub end -> rred (Epostincr id (Eloc b ofs ty) ty) m t (Ecomma (Eassign (Eloc b ofs ty) @@ -739,7 +746,7 @@ Inductive sstep: state -> trace -> state -> Prop := | step_internal_function: forall f vargs k m e m1 m2, list_norepet (var_names (fn_params f) ++ var_names (fn_vars f)) -> alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> - bind_parameters ge e m1 f.(fn_params) vargs m2 -> + bind_parameters e m1 f.(fn_params) vargs m2 -> sstep (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k e m2) @@ -766,7 +773,7 @@ End SEMANTICS. Inductive initial_state (p: program): state -> Prop := | initial_state_intro: forall b f m0, - let ge := Genv.globalenv p in + let ge := globalenv p in Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> @@ -782,19 +789,20 @@ Inductive final_state: state -> int -> Prop := (** Wrapping up these definitions in a small-step semantics. *) Definition semantics (p: program) := - Semantics step (initial_state p) final_state (Genv.globalenv p). + Semantics_gen step (initial_state p) final_state (globalenv p) (globalenv p). (** This semantics has the single-event property. *) Lemma semantics_single_events: forall p, single_events (semantics p). Proof. - intros; red; intros. destruct H. - set (ge := globalenv (semantics p)) in *. + unfold semantics; intros; red; simpl; intros. + set (ge := globalenv p) in *. assert (DEREF: forall chunk m b ofs t v, deref_loc ge chunk m b ofs t v -> (length t <= 1)%nat). intros. inv H0; simpl; try omega. inv H3; simpl; try omega. assert (ASSIGN: forall chunk m b ofs t v m', assign_loc ge chunk m b ofs v t m' -> (length t <= 1)%nat). intros. inv H0; simpl; try omega. inv H3; simpl; try omega. + destruct H. inv H; simpl; try omega. inv H0; eauto; simpl; try omega. eapply external_call_trace_length; eauto. inv H; simpl; try omega. eapply external_call_trace_length; eauto. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 3b23a547..cb83731a 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -21,6 +21,7 @@ *) Require Import Coqlib. +Require Import Maps. Require Import Errors. Require Import Integers. Require Import Floats. @@ -160,8 +161,8 @@ Definition make_cast (from to: type) (e: expr) := | cast_case_s2bool => OK (Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero)) | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero)) | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero)) - | cast_case_struct id1 fld1 id2 fld2 => OK e - | cast_case_union id1 fld1 id2 fld2 => OK e + | cast_case_struct id1 id2 => OK e + | cast_case_union id1 id2 => OK e | cast_case_void => OK e | cast_case_default => Error (msg "Cshmgen.make_cast") end. @@ -234,34 +235,34 @@ Definition make_binarith (iop iopu fop sop lop lopu: binary_operation) | bin_default => Error (msg "Cshmgen.make_binarith") end. -Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) := +Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with | add_case_pi ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in OK (Ebinop Oadd e1 (Ebinop Omul n e2)) | add_case_ip ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in OK (Ebinop Oadd e2 (Ebinop Omul n e1)) | add_case_pl ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))) | add_case_lp ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1))) | add_default => make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2 end. -Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) := +Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_sub ty1 ty2 with | sub_case_pi ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in OK (Ebinop Odivu (Ebinop Osub e1 e2) n) | sub_case_pl ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in + let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2))) | sub_default => make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2 @@ -349,8 +350,8 @@ Definition make_load (addr: expr) (ty_res: type) := (** [make_memcpy dst src ty] returns a [memcpy] builtin appropriate for by-copy assignment of a value of Clight type [ty]. *) -Definition make_memcpy (dst src: expr) (ty: type) := - Sbuiltin None (EF_memcpy (Ctypes.sizeof ty) (Ctypes.alignof_blockcopy ty)) +Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) := + Sbuiltin None (EF_memcpy (Ctypes.sizeof ce ty) (Ctypes.alignof_blockcopy ce ty)) (dst :: src :: nil). (** [make_store addr ty rhs] stores the value of the @@ -358,10 +359,10 @@ Definition make_memcpy (dst src: expr) (ty: type) := Csharpminor expression [addr]. [ty] is the type of the memory location. *) -Definition make_store (addr: expr) (ty: type) (rhs: expr) := +Definition make_store (ce: composite_env) (addr: expr) (ty: type) (rhs: expr) := match access_mode ty with | By_value chunk => OK (Sstore chunk addr rhs) - | By_copy => OK (make_memcpy addr rhs ty) + | By_copy => OK (make_memcpy ce addr rhs ty) | _ => Error (msg "Cshmgen.make_store") end. @@ -375,12 +376,13 @@ Definition transl_unop (op: Cop.unary_operation) (a: expr) (ta: type) : res expr | Cop.Oabsfloat => make_absfloat a ta end. -Definition transl_binop (op: Cop.binary_operation) +Definition transl_binop (ce: composite_env) + (op: Cop.binary_operation) (a: expr) (ta: type) (b: expr) (tb: type) : res expr := match op with - | Cop.Oadd => make_add a ta b tb - | Cop.Osub => make_sub a ta b tb + | Cop.Oadd => make_add ce a ta b tb + | Cop.Osub => make_sub ce a ta b tb | Cop.Omul => make_mul a ta b tb | Cop.Odiv => make_div a ta b tb | Cop.Omod => make_mod a ta b tb @@ -397,13 +399,31 @@ Definition transl_binop (op: Cop.binary_operation) | Cop.Oge => make_cmp Cge a ta b tb end. +(** ** Translation of field accesses *) + +Definition make_field_access (ce: composite_env) (ty: type) (f: ident) (a: expr) : res expr := + match ty with + | Tstruct id _ => + match ce!id with + | None => + Error (MSG "Undefined struct " :: CTX id :: nil) + | Some co => + do ofs <- field_offset ce f (co_members co); + OK (Ebinop Oadd a (make_intconst (Int.repr ofs))) + end + | Tunion id _ => + OK a + | _ => + Error(msg "Cshmgen.make_field_access") + end. + (** * Translation of expressions *) (** [transl_expr a] returns the Csharpminor code that computes the value of expression [a]. The computation is performed in the error monad (see module [Errors]) to enable error reporting. *) -Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr := +Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr := match a with | Clight.Econst_int n _ => OK(make_intconst n) @@ -418,34 +438,28 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr := | Clight.Etempvar id ty => OK(Evar id) | Clight.Ederef b ty => - do tb <- transl_expr b; + do tb <- transl_expr ce b; make_load tb ty | Clight.Eaddrof b _ => - transl_lvalue b + transl_lvalue ce b | Clight.Eunop op b _ => - do tb <- transl_expr b; + do tb <- transl_expr ce b; transl_unop op tb (typeof b) | Clight.Ebinop op b c _ => - do tb <- transl_expr b; - do tc <- transl_expr c; - transl_binop op tb (typeof b) tc (typeof c) + do tb <- transl_expr ce b; + do tc <- transl_expr ce c; + transl_binop ce op tb (typeof b) tc (typeof c) | Clight.Ecast b ty => - do tb <- transl_expr b; + do tb <- transl_expr ce b; make_cast (typeof b) ty tb - | Clight.Efield b i ty => - match typeof b with - | Tstruct _ fld _ => - do tb <- transl_expr b; - do ofs <- field_offset i fld; - make_load - (Ebinop Oadd tb (make_intconst (Int.repr ofs))) - ty - | Tunion _ fld _ => - do tb <- transl_expr b; - make_load tb ty - | _ => - Error(msg "Cshmgen.transl_expr(field)") - end + | Clight.Efield b i ty => + do tb <- transl_expr ce b; + do addr <- make_field_access ce (typeof b) i tb; + make_load addr ty + | Clight.Esizeof ty' ty => + OK(make_intconst (Int.repr (sizeof ce ty'))) + | Clight.Ealignof ty' ty => + OK(make_intconst (Int.repr (alignof ce ty'))) end (** [transl_lvalue a] returns the Csharpminor code that evaluates @@ -453,23 +467,15 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr := where the value of [a] is stored. *) -with transl_lvalue (a: Clight.expr) {struct a} : res expr := +with transl_lvalue (ce: composite_env) (a: Clight.expr) {struct a} : res expr := match a with | Clight.Evar id _ => OK (Eaddrof id) | Clight.Ederef b _ => - transl_expr b + transl_expr ce b | Clight.Efield b i ty => - match typeof b with - | Tstruct _ fld _ => - do tb <- transl_expr b; - do ofs <- field_offset i fld; - OK (Ebinop Oadd tb (make_intconst (Int.repr ofs))) - | Tunion _ fld _ => - transl_expr b - | _ => - Error(msg "Cshmgen.transl_lvalue(field)") - end + do tb <- transl_expr ce b; + make_field_access ce (typeof b) i tb | _ => Error(msg "Cshmgen.transl_lvalue") end. @@ -479,20 +485,20 @@ with transl_lvalue (a: Clight.expr) {struct a} : res expr := casted to the corresponding types in [tyl]. Used for function applications. *) -Fixpoint transl_arglist (al: list Clight.expr) (tyl: typelist) +Fixpoint transl_arglist (ce: composite_env) (al: list Clight.expr) (tyl: typelist) {struct al}: res (list expr) := match al, tyl with | nil, Tnil => OK nil | a1 :: a2, Tcons ty1 ty2 => - do ta1 <- transl_expr a1; + do ta1 <- transl_expr ce a1; do ta1' <- make_cast (typeof a1) ty1 ta1; - do ta2 <- transl_arglist a2 ty2; + do ta2 <- transl_arglist ce a2 ty2; OK (ta1' :: ta2) | a1 :: a2, Tnil => (* Tolerance for calls to K&R or variadic functions *) - do ta1 <- transl_expr a1; + do ta1 <- transl_expr ce a1; do ta1' <- make_cast (typeof a1) (default_argument_conversion (typeof a1)) ta1; - do ta2 <- transl_arglist a2 Tnil; + do ta2 <- transl_arglist ce a2 Tnil; OK (ta1' :: ta2) | _, _ => Error(msg "Cshmgen.transl_arglist: arity mismatch") @@ -536,24 +542,24 @@ loop s1 s2 ---> block { // break in s1 and s2 branches here *) -Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat) +Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat) (s: Clight.statement) {struct s} : res stmt := match s with | Clight.Sskip => OK Sskip | Clight.Sassign b c => - do tb <- transl_lvalue b; - do tc <- transl_expr c; + do tb <- transl_lvalue ce b; + do tc <- transl_expr ce c; do tc' <- make_cast (typeof c) (typeof b) tc; - make_store tb (typeof b) tc' + make_store ce tb (typeof b) tc' | Clight.Sset x b => - do tb <- transl_expr b; + do tb <- transl_expr ce b; OK(Sset x tb) | Clight.Scall x b cl => match classify_fun (typeof b) with | fun_case_f args res cconv => - do tb <- transl_expr b; - do tcl <- transl_arglist cl args; + do tb <- transl_expr ce b; + do tcl <- transl_arglist ce cl args; OK(Scall x {| sig_args := typlist_of_arglist cl args; sig_res := opttyp_of_type res; sig_cc := cconv |} @@ -561,80 +567,80 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat) | _ => Error(msg "Cshmgen.transl_stmt(call)") end | Clight.Sbuiltin x ef tyargs bl => - do tbl <- transl_arglist bl tyargs; + do tbl <- transl_arglist ce bl tyargs; OK(Sbuiltin x ef tbl) | Clight.Ssequence s1 s2 => - do ts1 <- transl_statement tyret nbrk ncnt s1; - do ts2 <- transl_statement tyret nbrk ncnt s2; + do ts1 <- transl_statement ce tyret nbrk ncnt s1; + do ts2 <- transl_statement ce tyret nbrk ncnt s2; OK (Sseq ts1 ts2) | Clight.Sifthenelse e s1 s2 => - do te <- transl_expr e; - do ts1 <- transl_statement tyret nbrk ncnt s1; - do ts2 <- transl_statement tyret nbrk ncnt s2; + do te <- transl_expr ce e; + do ts1 <- transl_statement ce tyret nbrk ncnt s1; + do ts2 <- transl_statement ce tyret nbrk ncnt s2; OK (Sifthenelse (make_boolean te (typeof e)) ts1 ts2) | Clight.Sloop s1 s2 => - do ts1 <- transl_statement tyret 1%nat 0%nat s1; - do ts2 <- transl_statement tyret 0%nat (S ncnt) s2; + do ts1 <- transl_statement ce tyret 1%nat 0%nat s1; + do ts2 <- transl_statement ce tyret 0%nat (S ncnt) s2; OK (Sblock (Sloop (Sseq (Sblock ts1) ts2))) | Clight.Sbreak => OK (Sexit nbrk) | Clight.Scontinue => OK (Sexit ncnt) | Clight.Sreturn (Some e) => - do te <- transl_expr e; + do te <- transl_expr ce e; do te' <- make_cast (typeof e) tyret te; OK (Sreturn (Some te')) | Clight.Sreturn None => OK (Sreturn None) | Clight.Sswitch a sl => - do ta <- transl_expr a; - do tsl <- transl_lbl_stmt tyret 0%nat (S ncnt) sl; + do ta <- transl_expr ce a; + do tsl <- transl_lbl_stmt ce tyret 0%nat (S ncnt) sl; match classify_switch (typeof a) with | switch_case_i => OK (Sblock (Sswitch false ta tsl)) | switch_case_l => OK (Sblock (Sswitch true ta tsl)) | switch_default => Error(msg "Cshmgen.transl_stmt(switch)") end | Clight.Slabel lbl s => - do ts <- transl_statement tyret nbrk ncnt s; + do ts <- transl_statement ce tyret nbrk ncnt s; OK (Slabel lbl ts) | Clight.Sgoto lbl => OK (Sgoto lbl) end -with transl_lbl_stmt (tyret: type) (nbrk ncnt: nat) +with transl_lbl_stmt (ce: composite_env) (tyret: type) (nbrk ncnt: nat) (sl: Clight.labeled_statements) {struct sl}: res lbl_stmt := match sl with | Clight.LSnil => OK LSnil | Clight.LScons n s sl' => - do ts <- transl_statement tyret nbrk ncnt s; - do tsl' <- transl_lbl_stmt tyret nbrk ncnt sl'; + do ts <- transl_statement ce tyret nbrk ncnt s; + do tsl' <- transl_lbl_stmt ce tyret nbrk ncnt sl'; OK (LScons n ts tsl') end. (*** Translation of functions *) -Definition transl_var (v: ident * type) := (fst v, sizeof (snd v)). +Definition transl_var (ce: composite_env) (v: ident * type) := (fst v, sizeof ce (snd v)). Definition signature_of_function (f: Clight.function) := {| sig_args := map typ_of_type (map snd (Clight.fn_params f)); sig_res := opttyp_of_type (Clight.fn_return f); sig_cc := Clight.fn_callconv f |}. -Definition transl_function (f: Clight.function) : res function := - do tbody <- transl_statement f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f); +Definition transl_function (ce: composite_env) (f: Clight.function) : res function := + do tbody <- transl_statement ce f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f); OK (mkfunction (signature_of_function f) (map fst (Clight.fn_params f)) - (map transl_var (Clight.fn_vars f)) + (map (transl_var ce) (Clight.fn_vars f)) (map fst (Clight.fn_temps f)) tbody). -Definition transl_fundef (f: Clight.fundef) : res fundef := +Definition transl_fundef (ce: composite_env) (f: Clight.fundef) : res fundef := match f with | Clight.Internal g => - do tg <- transl_function g; OK(AST.Internal tg) + do tg <- transl_function ce g; OK(AST.Internal tg) | Clight.External ef args res cconv => if signature_eq (ef_sig ef) (signature_of_type args res cconv) then OK(AST.External ef) @@ -646,4 +652,5 @@ Definition transl_fundef (f: Clight.fundef) : res fundef := Definition transl_globvar (ty: type) := OK tt. Definition transl_program (p: Clight.program) : res program := - transform_partial_program2 transl_fundef transl_globvar p. + transform_partial_program2 (transl_fundef p.(prog_comp_env)) transl_globvar p. + diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index dc47df04..7f61c657 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -40,8 +40,8 @@ Proof. Qed. Lemma transl_fundef_sig1: - forall f tf args res cc, - transl_fundef f = OK tf -> + forall ce f tf args res cc, + transl_fundef ce f = OK tf -> classify_fun (type_of_fundef f) = fun_case_f args res cc -> funsig tf = signature_of_type args res cc. Proof. @@ -54,8 +54,8 @@ Proof. Qed. Lemma transl_fundef_sig2: - forall f tf args res cc, - transl_fundef f = OK tf -> + forall ce f tf args res cc, + transl_fundef ce f = OK tf -> type_of_fundef f = Tfunction args res cc -> funsig tf = signature_of_type args res cc. Proof. @@ -70,8 +70,8 @@ Qed. Lemma transl_expr_lvalue: forall ge e le m a loc ofs ta, Clight.eval_lvalue ge e le m a loc ofs -> - transl_expr a = OK ta -> - (exists tb, transl_lvalue a = OK tb /\ make_load tb (typeof a) = OK ta). + transl_expr ge a = OK ta -> + (exists tb, transl_lvalue ge a = OK tb /\ make_load tb (typeof a) = OK ta). Proof. intros until ta; intros EVAL TR. inv EVAL; simpl in TR. (* var local *) @@ -81,39 +81,36 @@ Proof. (* deref *) monadInv TR. exists x; auto. (* field struct *) - rewrite H0 in TR. monadInv TR. - econstructor; split. simpl. rewrite H0. - rewrite EQ; rewrite EQ1; simpl; eauto. auto. + monadInv TR. exists x0; split; auto. simpl; rewrite EQ; auto. (* field union *) - rewrite H0 in TR. monadInv TR. - econstructor; split. simpl. rewrite H0. rewrite EQ; simpl; eauto. auto. + monadInv TR. exists x0; split; auto. simpl; rewrite EQ; auto. Qed. (** Properties of labeled statements *) Lemma transl_lbl_stmt_1: - forall tyret nbrk ncnt n sl tsl, - transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> - transl_lbl_stmt tyret nbrk ncnt (Clight.select_switch n sl) = OK (select_switch n tsl). + forall ce tyret nbrk ncnt n sl tsl, + transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl -> + transl_lbl_stmt ce tyret nbrk ncnt (Clight.select_switch n sl) = OK (select_switch n tsl). Proof. intros until n. assert (DFL: forall sl tsl, - transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> - transl_lbl_stmt tyret nbrk ncnt (Clight.select_switch_default sl) = OK (select_switch_default tsl)). + transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl -> + transl_lbl_stmt ce tyret nbrk ncnt (Clight.select_switch_default sl) = OK (select_switch_default tsl)). { induction sl; simpl; intros. inv H; auto. monadInv H. simpl. destruct o; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto. } assert (CASE: forall sl tsl, - transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> + transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl -> match Clight.select_switch_case n sl with | None => select_switch_case n tsl = None | Some sl' => exists tsl', select_switch_case n tsl = Some tsl' - /\ transl_lbl_stmt tyret nbrk ncnt sl' = OK tsl' + /\ transl_lbl_stmt ce tyret nbrk ncnt sl' = OK tsl' end). { induction sl; simpl; intros. @@ -130,9 +127,9 @@ Proof. Qed. Lemma transl_lbl_stmt_2: - forall tyret nbrk ncnt sl tsl, - transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> - transl_statement tyret nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl). + forall ce tyret nbrk ncnt sl tsl, + transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl -> + transl_statement ce tyret nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl). Proof. induction sl; intros. monadInv H. auto. @@ -143,6 +140,7 @@ Qed. Section CONSTRUCTORS. +Variable ce: composite_env. Variable ge: genv. Lemma make_intconst_correct: @@ -305,9 +303,9 @@ Proof. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. destruct (Int.eq i Int.zero); auto. (* struct *) - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; auto. + destruct (ident_eq id1 id2); inv H2; auto. (* union *) - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; auto. + destruct (ident_eq id1 id2); inv H2; auto. Qed. Lemma make_boolean_correct: @@ -467,7 +465,7 @@ End MAKE_BIN. Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm. -Lemma make_add_correct: binary_constructor_correct make_add sem_add. +Lemma make_add_correct: binary_constructor_correct (make_add ce) (sem_add ce). Proof. red; unfold make_add, sem_add; intros until m; intros SEM MAKE EV1 EV2; @@ -479,14 +477,14 @@ Proof. - eapply make_binarith_correct; eauto; intros; auto. Qed. -Lemma make_sub_correct: binary_constructor_correct make_sub sem_sub. +Lemma make_sub_correct: binary_constructor_correct (make_sub ce) (sem_sub ce). Proof. red; unfold make_sub, sem_sub; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_sub tya tyb); inv MAKE. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - destruct va; try discriminate; destruct vb; inv SEM. - destruct (eq_block b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero) eqn:E; inv H0. + destruct (eq_block b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ce ty)) Int.zero) eqn:E; inv H0. econstructor; eauto with cshm. rewrite dec_eq_true. simpl. rewrite E; auto. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - eapply make_binarith_correct; eauto; intros; auto. @@ -648,8 +646,8 @@ Qed. Lemma transl_binop_correct: forall op a tya b tyb c va vb v e le m, - transl_binop op a tya b tyb = OK c -> - sem_binary_operation op va tya vb tyb m = Some v -> + transl_binop ce op a tya b tyb = OK c -> + sem_binary_operation ce op va tya vb tyb m = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m b vb -> eval_expr ge e le m c v. @@ -691,12 +689,12 @@ Proof. Qed. Lemma make_memcpy_correct: - forall f dst src ty k e le m b ofs v m', + forall ce f dst src ty k e le m b ofs v m', eval_expr ge e le m dst (Vptr b ofs) -> eval_expr ge e le m src v -> - assign_loc ty m b ofs v m' -> + assign_loc ce ty m b ofs v m' -> access_mode ty = By_copy -> - step ge (State f (make_memcpy dst src ty) k e le m) E0 (State f Sskip k e le m'). + step ge (State f (make_memcpy ce dst src ty) k e le m) E0 (State f Sskip k e le m'). Proof. intros. inv H1; try congruence. unfold make_memcpy. change le with (set_optvar None Vundef le) at 2. @@ -710,10 +708,10 @@ Qed. Lemma make_store_correct: forall addr ty rhs code e le m b ofs v m' f k, - make_store addr ty rhs = OK code -> + make_store ce addr ty rhs = OK code -> eval_expr ge e le m addr (Vptr b ofs) -> eval_expr ge e le m rhs v -> - assign_loc ty m b ofs v m' -> + assign_loc ce ty m b ofs v m' -> step ge (State f code k e le m) E0 (State f Sskip k e le m'). Proof. unfold make_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN. @@ -736,32 +734,32 @@ Variable prog: Clight.program. Variable tprog: Csharpminor.program. Hypothesis TRANSL: transl_program prog = OK tprog. -Let ge := Genv.globalenv prog. +Let ge := globalenv prog. Let tge := Genv.globalenv tprog. Lemma symbols_preserved: forall s, Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_transf_partial2 transl_fundef transl_globvar _ TRANSL). +Proof (Genv.find_symbol_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). Lemma public_preserved: forall s, Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof (Genv.public_symbol_transf_partial2 transl_fundef transl_globvar _ TRANSL). +Proof (Genv.public_symbol_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> - exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. -Proof (Genv.find_funct_transf_partial2 transl_fundef transl_globvar _ TRANSL). + exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef ge f = OK tf. +Proof (Genv.find_funct_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). Lemma function_ptr_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar _ TRANSL). + exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef ge f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). Lemma block_is_volatile_preserved: forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b. -Proof (Genv.block_is_volatile_transf_partial2 transl_fundef transl_globvar _ TRANSL). +Proof (Genv.block_is_volatile_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). (** * Matching between environments *) @@ -772,7 +770,7 @@ Record match_env (e: Clight.env) (te: Csharpminor.env) : Prop := mk_match_env { me_local: forall id b ty, - e!id = Some (b, ty) -> te!id = Some(b, sizeof ty); + e!id = Some (b, ty) -> te!id = Some(b, sizeof ge ty); me_local_inv: forall id b sz, te!id = Some (b, sz) -> exists ty, e!id = Some(b, ty) @@ -791,18 +789,18 @@ Qed. Lemma match_env_same_blocks: forall e te, match_env e te -> - blocks_of_env te = Clight.blocks_of_env e. + blocks_of_env te = Clight.blocks_of_env ge e. Proof. intros. set (R := fun (x: (block * type)) (y: (block * Z)) => match x, y with - | (b1, ty), (b2, sz) => b2 = b1 /\ sz = sizeof ty + | (b1, ty), (b2, sz) => b2 = b1 /\ sz = sizeof ge ty end). assert (list_forall2 (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) (PTree.elements e) (PTree.elements te)). apply PTree.elements_canonical_order. - intros id [b ty] GET. exists (b, sizeof ty); split. eapply me_local; eauto. red; auto. + intros id [b ty] GET. exists (b, sizeof ge ty); split. eapply me_local; eauto. red; auto. intros id [b sz] GET. exploit me_local_inv; eauto. intros [ty EQ]. exploit me_local; eauto. intros EQ1. exists (b, ty); split. auto. red; split; congruence. @@ -818,7 +816,7 @@ Qed. Lemma match_env_free_blocks: forall e te m m', match_env e te -> - Mem.free_list m (Clight.blocks_of_env e) = Some m' -> + Mem.free_list m (Clight.blocks_of_env ge e) = Some m' -> Mem.free_list m (blocks_of_env te) = Some m'. Proof. intros. rewrite (match_env_same_blocks _ _ H). auto. @@ -839,16 +837,16 @@ Qed. Lemma match_env_alloc_variables: forall e1 m1 vars e2 m2, - Clight.alloc_variables e1 m1 vars e2 m2 -> + Clight.alloc_variables ge e1 m1 vars e2 m2 -> forall te1, match_env e1 te1 -> exists te2, - Csharpminor.alloc_variables te1 m1 (map transl_var vars) te2 m2 + Csharpminor.alloc_variables te1 m1 (map (transl_var ge) vars) te2 m2 /\ match_env e2 te2. Proof. induction 1; intros; simpl. exists te1; split. constructor. auto. - exploit (IHalloc_variables (PTree.set id (b1, sizeof ty) te1)). + exploit (IHalloc_variables (PTree.set id (b1, sizeof ge ty) te1)). constructor. (* me_local *) intros until ty0. repeat rewrite PTree.gsspec. @@ -913,11 +911,11 @@ Hypothesis MENV: match_env e te. Lemma transl_expr_lvalue_correct: (forall a v, Clight.eval_expr ge e le m a v -> - forall ta (TR: transl_expr a = OK ta) , + forall ta (TR: transl_expr ge a = OK ta) , Csharpminor.eval_expr tge te le m ta v) /\(forall a b ofs, Clight.eval_lvalue ge e le m a b ofs -> - forall ta (TR: transl_lvalue a = OK ta), + forall ta (TR: transl_lvalue ge a = OK ta), Csharpminor.eval_expr tge te le m ta (Vptr b ofs)). Proof. apply eval_expr_lvalue_ind; intros; try (monadInv TR). @@ -939,6 +937,10 @@ Proof. eapply transl_binop_correct; eauto. (* cast *) eapply make_cast_correct; eauto. +(* sizeof *) + apply make_intconst_correct. +(* alignof *) + apply make_intconst_correct. (* rvalue out of lvalue *) exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]]. eapply make_load_correct; eauto. @@ -952,32 +954,34 @@ Proof. (* deref *) simpl in TR. eauto. (* field struct *) - simpl in TR. rewrite H1 in TR. monadInv TR. + change (prog_comp_env prog) with (genv_cenv ge) in EQ0. + unfold make_field_access in EQ0; rewrite H1, H2 in EQ0; monadInv EQ0. eapply eval_Ebinop; eauto. apply make_intconst_correct. simpl. congruence. (* field union *) - simpl in TR. rewrite H1 in TR. eauto. + unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0. + auto. Qed. Lemma transl_expr_correct: forall a v, Clight.eval_expr ge e le m a v -> - forall ta, transl_expr a = OK ta -> + forall ta, transl_expr ge a = OK ta -> Csharpminor.eval_expr tge te le m ta v. Proof (proj1 transl_expr_lvalue_correct). Lemma transl_lvalue_correct: forall a b ofs, Clight.eval_lvalue ge e le m a b ofs -> - forall ta, transl_lvalue a = OK ta -> + forall ta, transl_lvalue ge a = OK ta -> Csharpminor.eval_expr tge te le m ta (Vptr b ofs). Proof (proj2 transl_expr_lvalue_correct). Lemma transl_arglist_correct: forall al tyl vl, Clight.eval_exprlist ge e le m al tyl vl -> - forall tal, transl_arglist al tyl = OK tal -> + forall tal, transl_arglist ge al tyl = OK tal -> Csharpminor.eval_exprlist tge te le m tal vl. Proof. induction 1; intros. @@ -1035,21 +1039,21 @@ Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> P | match_Kstop: forall tyret nbrk ncnt, match_cont tyret nbrk ncnt Clight.Kstop Kstop | match_Kseq: forall tyret nbrk ncnt s k ts tk, - transl_statement tyret nbrk ncnt s = OK ts -> + transl_statement ge tyret nbrk ncnt s = OK ts -> match_cont tyret nbrk ncnt k tk -> match_cont tyret nbrk ncnt (Clight.Kseq s k) (Kseq ts tk) | match_Kloop1: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk, - transl_statement tyret 1%nat 0%nat s1 = OK ts1 -> - transl_statement tyret 0%nat (S ncnt) s2 = OK ts2 -> + transl_statement ge tyret 1%nat 0%nat s1 = OK ts1 -> + transl_statement ge tyret 0%nat (S ncnt) s2 = OK ts2 -> match_cont tyret nbrk ncnt k tk -> match_cont tyret 1%nat 0%nat (Clight.Kloop1 s1 s2 k) (Kblock (Kseq ts2 (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk)))) | match_Kloop2: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk, - transl_statement tyret 1%nat 0%nat s1 = OK ts1 -> - transl_statement tyret 0%nat (S ncnt) s2 = OK ts2 -> + transl_statement ge tyret 1%nat 0%nat s1 = OK ts1 -> + transl_statement ge tyret 0%nat (S ncnt) s2 = OK ts2 -> match_cont tyret nbrk ncnt k tk -> match_cont tyret 0%nat (S ncnt) (Clight.Kloop2 s1 s2 k) @@ -1060,7 +1064,7 @@ Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> P (Clight.Kswitch k) (Kblock tk) | match_Kcall_some: forall tyret nbrk ncnt nbrk' ncnt' f e k id tf te le tk, - transl_function f = OK tf -> + transl_function ge f = OK tf -> match_env e te -> match_cont (Clight.fn_return f) nbrk' ncnt' k tk -> match_cont tyret nbrk ncnt @@ -1070,8 +1074,8 @@ Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> P Inductive match_states: Clight.state -> Csharpminor.state -> Prop := | match_state: forall f nbrk ncnt s k e le m tf ts tk te ts' tk' - (TRF: transl_function f = OK tf) - (TR: transl_statement (Clight.fn_return f) nbrk ncnt s = OK ts) + (TRF: transl_function ge f = OK tf) + (TR: transl_statement ge (Clight.fn_return f) nbrk ncnt s = OK ts) (MTR: match_transl ts tk ts' tk') (MENV: match_env e te) (MK: match_cont (Clight.fn_return f) nbrk ncnt k tk), @@ -1079,7 +1083,7 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop := (State tf ts' tk' te le m) | match_callstate: forall fd args k m tfd tk targs tres cconv - (TR: transl_fundef fd = OK tfd) + (TR: transl_fundef ge fd = OK tfd) (MK: match_cont Tvoid 0%nat 0%nat k tk) (ISCC: Clight.is_call_cont k) (TY: type_of_fundef fd = Tfunction targs tres cconv), @@ -1093,7 +1097,7 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop := Remark match_states_skip: forall f e le te nbrk ncnt k tf tk m, - transl_function f = OK tf -> + transl_function ge f = OK tf -> match_env e te -> match_cont (Clight.fn_return f) nbrk ncnt k tk -> match_states (Clight.State f Clight.Sskip k e le m) (State tf Sskip tk te le m). @@ -1109,27 +1113,27 @@ Variable tyret: type. Lemma transl_find_label: forall s nbrk ncnt k ts tk - (TR: transl_statement tyret nbrk ncnt s = OK ts) + (TR: transl_statement ge tyret nbrk ncnt s = OK ts) (MC: match_cont tyret nbrk ncnt k tk), match Clight.find_label lbl s k with | None => find_label lbl ts tk = None | Some (s', k') => exists ts', exists tk', exists nbrk', exists ncnt', find_label lbl ts tk = Some (ts', tk') - /\ transl_statement tyret nbrk' ncnt' s' = OK ts' + /\ transl_statement ge tyret nbrk' ncnt' s' = OK ts' /\ match_cont tyret nbrk' ncnt' k' tk' end with transl_find_label_ls: forall ls nbrk ncnt k tls tk - (TR: transl_lbl_stmt tyret nbrk ncnt ls = OK tls) + (TR: transl_lbl_stmt ge tyret nbrk ncnt ls = OK tls) (MC: match_cont tyret nbrk ncnt k tk), match Clight.find_label_ls lbl ls k with | None => find_label_ls lbl tls tk = None | Some (s', k') => exists ts', exists tk', exists nbrk', exists ncnt', find_label_ls lbl tls tk = Some (ts', tk') - /\ transl_statement tyret nbrk' ncnt' s' = OK ts' + /\ transl_statement ge tyret nbrk' ncnt' s' = OK ts' /\ match_cont tyret nbrk' ncnt' k' tk' end. @@ -1340,7 +1344,8 @@ Proof. monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. constructor. - econstructor; eauto. + econstructor; eauto. +Local Opaque ge. simpl. rewrite H5; simpl. rewrite H7; simpl. eauto. constructor. @@ -1464,9 +1469,10 @@ Lemma transl_initial_states: Proof. intros. inv H. exploit function_ptr_translated; eauto. intros [tf [A B]]. - assert (C: Genv.find_symbol tge (prog_main tprog) = Some b). - rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). - auto. symmetry. unfold transl_program in TRANSL. + assert (C: Genv.find_symbol tge (AST.prog_main tprog) = Some b). + rewrite symbols_preserved. replace (AST.prog_main tprog) with (prog_main prog). + auto. symmetry. unfold transl_program in TRANSL. + change (prog_main prog) with (AST.prog_main (program_of_program prog)). eapply transform_partial_program2_main; eauto. assert (funsig tf = signature_of_type Tnil type_int32s cc_default). eapply transl_fundef_sig2; eauto. diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v index f8c3963e..3b0eb84f 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -97,13 +97,16 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop := | 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 r f ty b ofs id fList a delta, + | esl_field_struct: forall r f ty b ofs id co a delta, eval_simple_rvalue r (Vptr b ofs) -> - typeof r = Tstruct id fList a -> field_offset f fList = OK delta -> + typeof r = Tstruct id a -> + ge.(genv_cenv)!id = Some co -> + field_offset ge f (co_members co) = OK delta -> eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta)) - | esl_field_union: forall r f ty b ofs id fList a, + | esl_field_union: forall r f ty b ofs id co a, eval_simple_rvalue r (Vptr b ofs) -> - typeof r = Tunion id fList a -> + typeof r = Tunion id a -> + ge.(genv_cenv)!id = Some co -> eval_simple_lvalue (Efield r f ty) b ofs with eval_simple_rvalue: expr -> val -> Prop := @@ -123,16 +126,16 @@ with eval_simple_rvalue: expr -> val -> Prop := 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 -> + sem_binary_operation ge 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 -> sem_cast v1 (typeof r1) ty = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, - eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))) + eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) | esr_alignof: forall ty1 ty, - eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ty1))). + eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))). Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop := | esrl_nil: @@ -291,7 +294,7 @@ Inductive estep: state -> trace -> state -> Prop := eval_simple_lvalue e m l b ofs -> deref_loc ge (typeof l) m b ofs t1 v1 -> eval_simple_rvalue e m r v2 -> - sem_binary_operation op v1 (typeof l) v2 (typeof r) m = Some v3 -> + sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m = Some v3 -> sem_cast v3 tyres (typeof l) = Some v4 -> assign_loc ge (typeof l) m b ofs v4 t2 m' -> ty = typeof l -> @@ -304,7 +307,7 @@ Inductive estep: state -> trace -> state -> Prop := eval_simple_lvalue e m l b ofs -> deref_loc ge (typeof l) m b ofs t v1 -> eval_simple_rvalue e m r v2 -> - match sem_binary_operation op v1 (typeof l) v2 (typeof r) m with + 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 @@ -320,7 +323,7 @@ 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 id v1 ty = Some v2 -> + sem_incrdecr ge id v1 ty = Some v2 -> sem_cast v2 (incrdecr_type ty) ty = Some v3 -> assign_loc ge ty m b ofs v3 t2 m' -> ty = typeof l -> @@ -332,7 +335,7 @@ 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 id v1 ty with + match sem_incrdecr ge id v1 ty with | None => True | Some v2 => match sem_cast v2 (incrdecr_type ty) ty with @@ -525,8 +528,8 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Efield (Eval v ty1) f ty => exists b, exists ofs, v = Vptr b ofs /\ match ty1 with - | Tstruct _ fList _ => exists delta, field_offset f fList = Errors.OK delta - | Tunion _ _ _ => True + | Tstruct id _ => exists co delta, ge.(genv_cenv)!id = Some co /\ field_offset ge f (co_members co) = Errors.OK delta + | Tunion id _ => exists co, ge.(genv_cenv)!id = Some co | _ => False end | Eval v ty => False @@ -535,7 +538,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Eunop op (Eval v1 ty1) ty => exists v, sem_unary_operation op v1 ty1 = Some v | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => - exists v, sem_binary_operation op v1 ty1 v2 ty2 m = Some v + exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => exists v, sem_cast v1 ty1 ty = Some v | Eseqand (Eval v1 ty1) r2 ty => @@ -581,8 +584,8 @@ Proof. exists b; auto. exists b; auto. exists b; exists ofs; auto. - exists b; exists ofs; split; auto. exists delta; auto. - exists b; exists ofs; auto. + exists b; exists ofs; split; auto. exists co, delta; auto. + exists b; exists ofs; split; auto. exists co; auto. Qed. Lemma rred_invert: @@ -705,11 +708,11 @@ Lemma eval_simple_steps: (forall a v, eval_simple_rvalue e m a v -> forall C, context RV RV C -> star Csem.step ge (ExprState f (C a) k e m) - E0 (ExprState f (C (Eval v (typeof a))) k e m)) + E0 (ExprState f (C (Eval v (typeof a))) k e m)) /\ (forall a b ofs, eval_simple_lvalue e m a b ofs -> forall C, context LV RV C -> star Csem.step ge (ExprState f (C a) k e m) - E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m)). + E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m)). Proof. Ltac Steps REC C' := eapply star_trans; [apply (REC C'); eauto | idtac | simpl; reflexivity]. @@ -816,8 +819,8 @@ Ltac StepR REC C' a := StepR IHa (fun x => C(Efield x f0 ty)) a. exploit safe_inv. eexact SAFE0. eauto. simpl. intros [b [ofs [EQ TY]]]. subst v. destruct (typeof a) eqn:?; try contradiction. - destruct TY as [delta OFS]. exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto. - exists b; exists ofs; econstructor; eauto. + destruct TY as (co & delta & CE & OFS). exists b; exists (Int.add ofs (Int.repr delta)); econstructor; eauto. + destruct TY as (co & CE). exists b; exists ofs; econstructor; eauto. (* valof *) destruct (andb_prop _ _ S) as [S1 S2]. clear S. rewrite negb_true_iff in S2. StepL IHa (fun x => C(Evalof x ty)) a. @@ -1197,7 +1200,7 @@ Proof. eapply eval_simple_rvalue_steps with (C := fun x => C(Eassignop op (Eloc b ofs (typeof l)) x tyres (typeof l))); eauto. eapply plus_left. left; apply step_rred; auto. econstructor; eauto. - destruct (sem_binary_operation op v1 (typeof l) v2 (typeof r) m) as [v3|] eqn:?. + destruct (sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m) as [v3|] eqn:?. eapply star_left. left; apply step_rred with (C := fun x => C(Eassign (Eloc b ofs (typeof l)) x (typeof l))); eauto. econstructor; eauto. apply star_one. @@ -1230,10 +1233,10 @@ Proof. eapply plus_left. left; apply step_rred; auto. econstructor; eauto. set (op := match id with Incr => Oadd | Decr => Osub end). - assert (SEM: sem_binary_operation op v1 (typeof l) (Vint Int.one) type_int32s m = - sem_incrdecr id v1 (typeof l)). + assert (SEM: sem_binary_operation ge op v1 (typeof l) (Vint Int.one) type_int32s m = + sem_incrdecr ge id v1 (typeof l)). destruct id; auto. - destruct (sem_incrdecr id v1 (typeof l)) as [v2|]. + destruct (sem_incrdecr ge id v1 (typeof l)) 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. @@ -1325,7 +1328,7 @@ Proof. exploit (simple_can_eval_rval f k e m b2 (fun x => C(Eassignop op (Eloc b ofs (typeof b1)) x tyres ty))); eauto. intros [v [E2 S2]]. exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]]. - destruct (sem_binary_operation op v1 (typeof b1) v (typeof b2) m) as [v3|] eqn:?. + 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 (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')). destruct H2 as [t2 [m' D]]. @@ -1340,7 +1343,7 @@ 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 id v1 ty) as [v2|] eqn:?. + destruct (sem_incrdecr ge id v1 ty) as [v2|] eqn:?. destruct (sem_cast v2 (incrdecr_type ty) ty) 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]]. @@ -1431,12 +1434,13 @@ End STRATEGY. (** The semantics that follows the strategy. *) Definition semantics (p: program) := - Semantics step (initial_state p) final_state (Genv.globalenv p). + let ge := globalenv p in + Semantics_gen step (initial_state p) final_state ge ge. (** This semantics is receptive to changes in events. *) Remark deref_loc_trace: - forall F V (ge: Genv.t F V) ty m b ofs t v, + forall ge ty m b ofs t v, deref_loc ge ty m b ofs t v -> match t with nil => True | ev :: nil => True | _ => False end. Proof. @@ -1444,7 +1448,7 @@ Proof. Qed. Remark deref_loc_receptive: - forall F V (ge: Genv.t F V) ty m b ofs ev1 t1 v ev2, + forall ge ty m b ofs ev1 t1 v ev2, deref_loc ge ty m b ofs (ev1 :: t1) v -> match_traces ge (ev1 :: nil) (ev2 :: nil) -> t1 = nil /\ exists v', deref_loc ge ty m b ofs (ev2 :: nil) v'. @@ -1456,7 +1460,7 @@ Proof. Qed. Remark assign_loc_trace: - forall F V (ge: Genv.t F V) ty m b ofs t v m', + forall ge ty m b ofs t v m', assign_loc ge ty m b ofs v t m' -> match t with nil => True | ev :: nil => output_event ev | _ => False end. Proof. @@ -1464,7 +1468,7 @@ Proof. Qed. Remark assign_loc_receptive: - forall F V (ge: Genv.t F V) ty m b ofs ev1 t1 v m' ev2, + forall ge ty m b ofs ev1 t1 v m' ev2, assign_loc ge ty m b ofs v (ev1 :: t1) m' -> match_traces ge (ev1 :: nil) (ev2 :: nil) -> ev1 :: t1 = ev2 :: nil. @@ -1479,6 +1483,7 @@ Lemma semantics_strongly_receptive: Proof. intros. constructor; simpl; intros. (* receptiveness *) + set (ge := globalenv p) in *. inversion H; subst. inv H1. (* valof volatile *) @@ -1492,9 +1497,9 @@ Proof. subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H. econstructor; econstructor; eauto. inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. - destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?. + 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 (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')). + 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. econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. @@ -1505,9 +1510,9 @@ Proof. rewrite Heqo; auto. (* assignop stuck *) exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. - destruct (sem_binary_operation op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?. + 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 (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v4' t2' m'')). + 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. econstructor; econstructor. left; eapply step_assignop_stuck with (v1 := v1'); eauto. @@ -1521,9 +1526,9 @@ 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 id v1' (typeof l)) as [v2'|] eqn:?. + 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 (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')). + 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. econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. @@ -1534,9 +1539,9 @@ Proof. rewrite Heqo; auto. (* postincr stuck *) exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. - destruct (sem_incrdecr id v1' (typeof l)) as [v2'|] eqn:?. + 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 (classic (exists t2', exists m'', assign_loc (Genv.globalenv p) (typeof l) m b ofs v3' t2' m'')). + 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. econstructor; econstructor. left; eapply step_postincr_stuck with (v1 := v1'); eauto. @@ -1732,7 +1737,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_simple_lvalue ge e m2 l' b ofs -> deref_loc ge (typeof l) m2 b ofs t3 v1 -> eval_simple_rvalue ge e m2 r' v2 -> - sem_binary_operation op v1 (typeof l) v2 (typeof r) m2 = Some v3 -> + sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m2 = Some v3 -> sem_cast v3 tyres (typeof l) = Some v4 -> assign_loc ge (typeof l) m2 b ofs v4 t4 m3 -> ty = typeof l -> @@ -1741,7 +1746,7 @@ 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 id v1 ty = Some v2 -> + sem_incrdecr ge id v1 ty = Some v2 -> sem_cast v2 (incrdecr_type ty) ty = Some v3 -> assign_loc ge ty m1 b ofs v3 t3 m2 -> ty = typeof l -> @@ -1893,11 +1898,11 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres m4, list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> - alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> + 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 -> - Mem.free_list m3 (blocks_of_env e) = Some m4 -> + 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', external_call ef ge vargs m t vres m' -> @@ -2115,7 +2120,7 @@ with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop := | evalinf_funcall_internal: forall m f vargs t e m1 m2, list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> - alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> + alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> bind_parameters ge e m1 f.(fn_params) vargs m2 -> execinf_stmt e m2 f.(fn_body) t -> evalinf_funcall m (Internal f) vargs t. @@ -3019,7 +3024,7 @@ End BIGSTEP. Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := | bigstep_program_terminates_intro: forall b f m0 m1 t r, - let ge := Genv.globalenv p in + let ge := globalenv p in Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> @@ -3029,7 +3034,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Inductive bigstep_program_diverges (p: program): traceinf -> Prop := | bigstep_program_diverges_intro: forall b f m0 t, - let ge := Genv.globalenv p in + let ge := globalenv p in Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index fa74f11c..8ea4e077 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -20,6 +20,7 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import AST. +Require Import Errors. Require Import Ctypes. Require Import Cop. @@ -207,8 +208,44 @@ Definition type_of_fundef (f: fundef) : type := (** ** Programs *) -(** A program is a collection of named functions, plus a collection - of named global variables, carrying their types and optional initialization - data. See module [AST] for more details. *) +(** A program is composed of: +- a list of definitions of functions and global variables; +- the names of functions and global variables that are public (not static); +- the name of the function that acts as entry point ("main" function). +- a list of definitions for structure and union names; +- the corresponding composite environment; +*) + +Record program : Type := { + prog_defs: list (ident * globdef fundef type); + prog_public: list ident; + prog_main: ident; + prog_types: list composite_definition; + prog_comp_env: composite_env; + prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env +}. + +Definition program_of_program (p: program) : AST.program fundef type := + {| AST.prog_defs := p.(prog_defs); + AST.prog_public := p.(prog_public); + AST.prog_main := p.(prog_main) |}. + +Coercion program_of_program: program >-> AST.program. + +Program Definition make_program (types: list composite_definition) + (defs: list (ident * globdef fundef type)) + (public: list ident) + (main: ident): res program := + match build_composite_env types with + | OK env => + OK {| prog_defs := defs; + prog_public := public; + prog_main := main; + prog_types := types; + prog_comp_env := env; + prog_comp_env_eq := _ |} + | Error msg => + Error msg + end. + -Definition program : Type := AST.program fundef type. diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index c437a6bc..091c5276 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -16,6 +16,7 @@ (** Type expressions for the Compcert C and Clight languages *) Require Import Coqlib. +Require Import Maps. Require Import AST. Require Import Errors. Require Archi. @@ -63,32 +64,6 @@ Definition noattr := {| attr_volatile := false; attr_alignas := None |}. of the function arguments (list [targs]), and the type of the function result ([tres]). Variadic functions and old-style unprototyped functions are not supported. -- In C, struct and union types are named and compared by name. - This enables the definition of recursive struct types such as -<< - struct s1 { int n; struct * s1 next; }; ->> - Note that recursion within types must go through a pointer type. - For instance, the following is not allowed in C. -<< - struct s2 { int n; struct s2 next; }; ->> - In Compcert C, struct and union types [Tstruct id fields] and - [Tunion id fields] are compared by structure: the [fields] - argument gives the names and types of the members. The identifier - [id] is a local name which can be used in conjuction with the - [Tcomp_ptr] constructor to express recursive types. [Tcomp_ptr id] - stands for a pointer type to the nearest enclosing [Tstruct] - or [Tunion] type named [id]. For instance. the structure [s1] - defined above in C is expressed by -<< - Tstruct "s1" (Fcons "n" (Tint I32 Signed) - (Fcons "next" (Tcomp_ptr "s1") - Fnil)) ->> - Note that the incorrect structure [s2] above cannot be expressed at - all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing - structure or union, but not to the structure or union directly. *) Inductive type : Type := @@ -99,35 +74,27 @@ Inductive type : Type := | Tpointer: type -> attr -> type (**r pointer types ([*ty]) *) | Tarray: type -> Z -> attr -> type (**r array types ([ty[len]]) *) | Tfunction: typelist -> type -> calling_convention -> type (**r function types *) - | Tstruct: ident -> fieldlist -> attr -> type (**r struct types *) - | Tunion: ident -> fieldlist -> attr -> type (**r union types *) - | Tcomp_ptr: ident -> attr -> type (**r pointer to named struct or union *) - + | Tstruct: ident -> attr -> type (**r struct types *) + | Tunion: ident -> attr -> type (**r union types *) with typelist : Type := | Tnil: typelist - | Tcons: type -> typelist -> typelist - -with fieldlist : Type := - | Fnil: fieldlist - | Fcons: ident -> type -> fieldlist -> fieldlist. + | Tcons: type -> typelist -> typelist. Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2} -with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2} -with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}. +with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}. Proof. assert (forall (x y: intsize), {x=y} + {x<>y}) by decide equality. assert (forall (x y: signedness), {x=y} + {x<>y}) by decide equality. assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality. assert (forall (x y: attr), {x=y} + {x<>y}). { decide equality. decide equality. apply N.eq_dec. apply bool_dec. } - generalize ident_eq zeq bool_dec. intros E1 E2 E3. + generalize ident_eq zeq bool_dec ident_eq; intros. decide equality. decide equality. decide equality. - generalize ident_eq. intros E1. decide equality. Defined. -Opaque type_eq typelist_eq fieldlist_eq. +Opaque type_eq typelist_eq. (** Extract the attributes of a type. *) @@ -140,9 +107,8 @@ Definition attr_of_type (ty: type) := | Tpointer elt a => a | Tarray elt sz a => a | Tfunction args res cc => noattr - | Tstruct id fld a => a - | Tunion id fld a => a - | Tcomp_ptr id a => a + | Tstruct id a => a + | Tunion id a => a end. (** Change the top-level attributes of a type *) @@ -156,9 +122,8 @@ Definition change_attributes (f: attr -> attr) (ty: type) : type := | Tpointer elt a => Tpointer elt (f a) | Tarray elt sz a => Tarray elt sz (f a) | Tfunction args res cc => ty - | Tstruct id fld a => Tstruct id fld (f a) - | Tunion id fld a => Tunion id fld (f a) - | Tcomp_ptr id a => Tcomp_ptr id (f a) + | Tstruct id a => Tstruct id (f a) + | Tunion id a => Tunion id (f a) end. (** Erase the top-level attributes of a type *) @@ -181,6 +146,39 @@ Definition attr_union (a1 a2: attr) : attr := Definition merge_attributes (ty: type) (a: attr) : type := change_attributes (attr_union a) ty. +(** Syntax for [struct] and [union] definitions. [struct] and [union] + are collectively called "composites". Each compilation unit + comes with a list of top-level definitions of composites. *) + +Inductive struct_or_union : Type := Struct | Union. + +Definition members : Type := list (ident * type). + +Inductive composite_definition : Type := + Composite (id: ident) (su: struct_or_union) (m: members) (a: attr). + +(** For type-checking, compilation and semantics purposes, the composite + definitions are collected in the following [composite_env] environment. + The [composite] record contains additional information compared with + the [composite_definition], such as size and alignment information. *) + +Record composite : Type := { + co_su: struct_or_union; + co_members: members; + co_attr: attr; + co_sizeof: Z; + co_alignof: Z; + co_sizeof_pos: co_sizeof >= 0; + co_alignof_two_p: exists n, co_alignof = two_power_nat n; + co_sizeof_alignof: (co_alignof | co_sizeof) +}. + +Definition composite_env : Type := PTree.t composite. + +(** * Operations over types *) + +(** ** Conversions *) + Definition type_int32s := Tint I32 Signed noattr. Definition type_bool := Tint IBool Signed noattr. @@ -208,15 +206,51 @@ Definition default_argument_conversion (ty: type) : type := | _ => remove_attributes ty end. -(** * Operations over types *) +(** ** Complete types *) -(** Alignment of a type, in bytes. *) +(** A type is complete if it fully describes an object. + All struct and union names appearing in the type must be defined, + unless they occur under a pointer or function type. [void] and + function types are incomplete types. *) -Fixpoint alignof (t: type) : Z := - match attr_alignas (attr_of_type t) with +Fixpoint complete_type (env: composite_env) (t: type) : bool := + match t with + | Tvoid => false + | Tint _ _ _ => true + | Tlong _ _ => true + | Tfloat _ _ => true + | Tpointer _ _ => true + | Tarray t' _ _ => complete_type env t' + | Tfunction _ _ _ => false + | Tstruct id _ | Tunion id _ => + match env!id with Some co => true | None => false end + end. + +Definition complete_or_function_type (env: composite_env) (t: type) : bool := + match t with + | Tfunction _ _ _ => true + | _ => complete_type env t + end. + +(** ** Alignment of a type *) + +(** Adjust the natural alignment [al] based on the attributes [a] attached + to the type. If an "alignas" attribute is given, use it as alignment + in preference to [al]. *) + +Definition align_attr (a: attr) (al: Z) : Z := + match attr_alignas a with | Some l => two_p (Z.of_N l) - | None => - match t with + | None => al + end. + +(** In the ISO C standard, alignment is defined only for complete + types. However, it is convenient that [alignof] is a total + function. For incomplete types, it returns 1. *) + +Fixpoint alignof (env: composite_env) (t: type) : Z := + align_attr (attr_of_type t) + (match t with | Tvoid => 1 | Tint I8 _ _ => 1 | Tint I16 _ _ => 2 @@ -226,42 +260,26 @@ Fixpoint alignof (t: type) : Z := | Tfloat F32 _ => 4 | Tfloat F64 _ => Archi.align_float64 | Tpointer _ _ => 4 - | Tarray t' _ _ => alignof t' + | Tarray t' _ _ => alignof env t' | Tfunction _ _ _ => 1 - | Tstruct _ fld _ => alignof_fields fld - | Tunion _ fld _ => alignof_fields fld - | Tcomp_ptr _ _ => 4 - end - end - -with alignof_fields (f: fieldlist) : Z := - match f with - | Fnil => 1 - | Fcons id t f' => Zmax (alignof t) (alignof_fields f') - end. - -Scheme type_ind2 := Induction for type Sort Prop - with fieldlist_ind2 := Induction for fieldlist Sort Prop. + | Tstruct id _ | Tunion id _ => + match env!id with Some co => co_alignof co | None => 1 end + end). + +Remark align_attr_two_p: + forall al a, + (exists n, al = two_power_nat n) -> + (exists n, align_attr a al = two_power_nat n). +Proof. + intros. unfold align_attr. destruct (attr_alignas a). + exists (N.to_nat n). rewrite two_power_nat_two_p. rewrite N_nat_Z. auto. + auto. +Qed. Lemma alignof_two_p: - forall t, exists n, alignof t = two_power_nat n -with alignof_fields_two_p: - forall f, exists n, alignof_fields f = two_power_nat n. + forall env t, exists n, alignof env t = two_power_nat n. Proof. - assert (X: forall t a, - (exists n, a = two_power_nat n) -> - exists n, - match attr_alignas (attr_of_type t) with - | Some l => two_p (Z.of_N l) - | None => a - end = two_power_nat n). - { - intros. - destruct (attr_alignas (attr_of_type t)). - exists (N.to_nat n). rewrite two_power_nat_two_p. rewrite N_nat_Z. auto. - auto. - } - induction t; apply X; simpl; auto. + induction t; apply align_attr_two_p; simpl. exists 0%nat; auto. destruct i. exists 0%nat; auto. @@ -273,28 +291,28 @@ Proof. exists 2%nat; auto. (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity). exists 2%nat; auto. + apply IHt. exists 0%nat; auto. - exists 2%nat; auto. - induction f; simpl. - exists 0%nat; auto. - apply Z.max_case; auto. + destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto. + destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto. Qed. Lemma alignof_pos: - forall t, alignof t > 0. + forall env t, alignof env t > 0. Proof. - intros. destruct (alignof_two_p t) as [n EQ]. rewrite EQ. apply two_power_nat_pos. + intros. destruct (alignof_two_p env t) as [n EQ]. rewrite EQ. apply two_power_nat_pos. Qed. -Lemma alignof_fields_pos: - forall f, alignof_fields f > 0. -Proof. - intros. destruct (alignof_fields_two_p f) as [n EQ]. rewrite EQ. apply two_power_nat_pos. -Qed. +(** ** Size of a type *) -(** Size of a type, in bytes. *) +(** In the ISO C standard, size is defined only for complete + types. However, it is convenient that [sizeof] is a total + function. For [void] and function types, we follow GCC and define + their size to be 1. For undefined structures and unions, the size is + arbitrarily taken to be 0. +*) -Fixpoint sizeof (t: type) : Z := +Fixpoint sizeof (env: composite_env) (t: type) : Z := match t with | Tvoid => 1 | Tint I8 _ _ => 1 @@ -305,199 +323,217 @@ Fixpoint sizeof (t: type) : Z := | Tfloat F32 _ => 4 | Tfloat F64 _ => 8 | Tpointer _ _ => 4 - | Tarray t' n _ => sizeof t' * Zmax 0 n + | Tarray t' n _ => sizeof env t' * Z.max 0 n | Tfunction _ _ _ => 1 - | Tstruct _ fld _ => align (sizeof_struct fld 0) (alignof t) - | Tunion _ fld _ => align (sizeof_union fld) (alignof t) - | Tcomp_ptr _ _ => 4 - end - -with sizeof_struct (fld: fieldlist) (pos: Z) {struct fld} : Z := - match fld with - | Fnil => pos - | Fcons id t fld' => sizeof_struct fld' (align pos (alignof t) + sizeof t) - end - -with sizeof_union (fld: fieldlist) : Z := - match fld with - | Fnil => 0 - | Fcons id t fld' => Zmax (sizeof t) (sizeof_union fld') + | Tstruct id _ | Tunion id _ => + match env!id with Some co => co_sizeof co | None => 0 end end. Lemma sizeof_pos: - forall t, sizeof t >= 0 -with sizeof_struct_incr: - forall fld pos, pos <= sizeof_struct fld pos. + forall env t, sizeof env t >= 0. Proof. -- Local Opaque alignof. - assert (X: forall n t, n >= 0 -> align n (alignof t) >= 0). - { - intros. generalize (align_le n (alignof t) (alignof_pos t)). omega. - } - induction t; simpl; try xomega. + induction t; simpl; try omega. destruct i; omega. destruct f; omega. - change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega. - apply X. apply Zle_ge. apply sizeof_struct_incr. - apply X. induction f; simpl; xomega. -- induction fld; intros; simpl. - omega. - eapply Zle_trans. 2: apply IHfld. - apply Zle_trans with (align pos (alignof t)). - apply align_le. apply alignof_pos. - generalize (sizeof_pos t); omega. + change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega. + destruct (env!i). apply co_sizeof_pos. omega. + destruct (env!i). apply co_sizeof_pos. omega. Qed. +(** The size of a type is an integral multiple of its alignment, + unless the alignment was artificially increased with the [__Alignas] + attribute. *) + Fixpoint naturally_aligned (t: type) : Prop := + attr_alignas (attr_of_type t) = None /\ match t with - | Tint _ _ a | Tlong _ a | Tfloat _ a | Tpointer _ a | Tcomp_ptr _ a => - attr_alignas a = None - | Tarray t' _ a => - attr_alignas a = None /\ naturally_aligned t' - | Tvoid | Tfunction _ _ _ | Tstruct _ _ _ | Tunion _ _ _ => - True + | Tarray t' _ _ => naturally_aligned t' + | _ => True end. Lemma sizeof_alignof_compat: - forall t, naturally_aligned t -> (alignof t | sizeof t). + forall env t, naturally_aligned t -> (alignof env t | sizeof env t). Proof. -Local Transparent alignof. - induction t; simpl; intros. + induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. - apply Zdivide_refl. -- rewrite H. destruct i; apply Zdivide_refl. -- rewrite H. exists (8 / Archi.align_int64); reflexivity. -- rewrite H. destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. -- rewrite H; apply Zdivide_refl. -- destruct H. rewrite H. apply Z.divide_mul_l; auto. +- destruct i; apply Zdivide_refl. +- exists (8 / Archi.align_int64); reflexivity. +- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. - apply Zdivide_refl. -- change (alignof (Tstruct i f a) | align (sizeof_struct f 0) (alignof (Tstruct i f a))). - apply align_divides. apply alignof_pos. -- change (alignof (Tunion i f a) | align (sizeof_union f) (alignof (Tunion i f a))). - apply align_divides. apply alignof_pos. -- rewrite H; apply Zdivide_refl. +- apply Z.divide_mul_l; auto. +- apply Zdivide_refl. +- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. +- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. Qed. -(** Byte offset for a field in a struct or union. - Field are laid out consecutively, and padding is inserted - to align each field to the natural alignment for its type. *) +(** ** Size and alignment for composite definitions *) + +(** The alignment for a structure or union is the max of the alignment + of its members. *) -Open Local Scope string_scope. +Fixpoint alignof_composite (env: composite_env) (m: members) : Z := + match m with + | nil => 1 + | (id, t) :: m' => Z.max (alignof env t) (alignof_composite env m') + end. + +(** The size of a structure corresponds to its layout: fields are + laid out consecutively, and padding is inserted to align + each field to the alignment for its type. *) + +Fixpoint sizeof_struct (env: composite_env) (cur: Z) (m: members) : Z := + match m with + | nil => cur + | (id, t) :: m' => sizeof_struct env (align cur (alignof env t) + sizeof env t) m' + end. + +(** The size of an union is the max of the sizes of its members. *) -Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z) - {struct fld} : res Z := +Fixpoint sizeof_union (env: composite_env) (m: members) : Z := + match m with + | nil => 0 + | (id, t) :: m' => Z.max (sizeof env t) (sizeof_union env m') + end. + +Lemma alignof_composite_two_p: + forall env m, exists n, alignof_composite env m = two_power_nat n. +Proof. + induction m as [|[id t]]; simpl. +- exists 0%nat; auto. +- apply Z.max_case; auto. apply alignof_two_p. +Qed. + +Lemma alignof_composite_pos: + forall env m a, align_attr a (alignof_composite env m) > 0. +Proof. + intros. + exploit align_attr_two_p. apply (alignof_composite_two_p env m). + instantiate (1 := a). intros [n EQ]. + rewrite EQ; apply two_power_nat_pos. +Qed. + +Lemma sizeof_struct_incr: + forall env m cur, cur <= sizeof_struct env cur m. +Proof. + induction m as [|[id t]]; simpl; intros. +- omega. +- apply Zle_trans with (align cur (alignof env t)). + apply align_le. apply alignof_pos. + apply Zle_trans with (align cur (alignof env t) + sizeof env t). + generalize (sizeof_pos env t); omega. + apply IHm. +Qed. + +Lemma sizeof_union_pos: + forall env m, 0 <= sizeof_union env m. +Proof. + induction m as [|[id t]]; simpl; xomega. +Qed. + +(** ** Byte offset for a field of a structure *) + +(** [field_offset env id fld] returns the byte offset for field [id] + in a structure whose members are [fld]. Fields are laid out + consecutively, and padding is inserted to align each field to the + alignment for its type. *) + +Fixpoint field_offset_rec (env: composite_env) (id: ident) (fld: members) (pos: Z) + {struct fld} : res Z := match fld with - | Fnil => Error (MSG "Unknown field " :: CTX id :: nil) - | Fcons id' t fld' => + | nil => Error (MSG "Unknown field " :: CTX id :: nil) + | (id', t) :: fld' => if ident_eq id id' - then OK (align pos (alignof t)) - else field_offset_rec id fld' (align pos (alignof t) + sizeof t) + then OK (align pos (alignof env t)) + else field_offset_rec env id fld' (align pos (alignof env t) + sizeof env t) end. -Definition field_offset (id: ident) (fld: fieldlist) : res Z := - field_offset_rec id fld 0. +Definition field_offset (env: composite_env) (id: ident) (fld: members) : res Z := + field_offset_rec env id fld 0. -Fixpoint field_type (id: ident) (fld: fieldlist) {struct fld} : res type := +Fixpoint field_type (id: ident) (fld: members) {struct fld} : res type := match fld with - | Fnil => Error (MSG "Unknown field " :: CTX id :: nil) - | Fcons id' t fld' => if ident_eq id id' then OK t else field_type id fld' + | nil => Error (MSG "Unknown field " :: CTX id :: nil) + | (id', t) :: fld' => if ident_eq id id' then OK t else field_type id fld' end. (** Some sanity checks about field offsets. First, field offsets are within the range of acceptable offsets. *) Remark field_offset_rec_in_range: - forall id ofs ty fld pos, - field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty -> - pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos. + forall env id ofs ty fld pos, + field_offset_rec env id fld pos = OK ofs -> field_type id fld = OK ty -> + pos <= ofs /\ ofs + sizeof env ty <= sizeof_struct env pos fld. Proof. - intros until ty. induction fld; simpl. - congruence. - destruct (ident_eq id i); intros. - inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr. + intros until ty. induction fld as [|[i t]]; simpl; intros. +- discriminate. +- destruct (ident_eq id i); intros. + inv H. inv H0. split. + apply align_le. apply alignof_pos. apply sizeof_struct_incr. exploit IHfld; eauto. intros [A B]. split; auto. - eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)). - apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega. + eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof env t)). + apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega. Qed. Lemma field_offset_in_range: - forall sid fld a fid ofs ty, - field_offset fid fld = OK ofs -> field_type fid fld = OK ty -> - 0 <= ofs /\ ofs + sizeof ty <= sizeof (Tstruct sid fld a). + forall env fld id ofs ty, + field_offset env id fld = OK ofs -> field_type id fld = OK ty -> + 0 <= ofs /\ ofs + sizeof env ty <= sizeof_struct env 0 fld. Proof. - intros. exploit field_offset_rec_in_range; eauto. intros [A B]. - split. auto. -Local Opaque alignof. - simpl. eapply Zle_trans; eauto. - apply align_le. apply alignof_pos. + intros. eapply field_offset_rec_in_range; eauto. Qed. (** Second, two distinct fields do not overlap *) Lemma field_offset_no_overlap: - forall id1 ofs1 ty1 id2 ofs2 ty2 fld, - field_offset id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 -> - field_offset id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 -> + forall env id1 ofs1 ty1 id2 ofs2 ty2 fld, + field_offset env id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 -> + field_offset env id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 -> id1 <> id2 -> - ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1. + ofs1 + sizeof env ty1 <= ofs2 \/ ofs2 + sizeof env ty2 <= ofs1. Proof. - intros until ty2. intros fld0 A B C D NEQ. - assert (forall fld pos, - field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 -> - field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 -> - ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1). - induction fld; intro pos; simpl. congruence. - destruct (ident_eq id1 i); destruct (ident_eq id2 i). - congruence. - subst i. intros. inv H; inv H0. + intros until fld. unfold field_offset. generalize 0 as pos. + induction fld as [|[i t]]; simpl; intros. +- discriminate. +- destruct (ident_eq id1 i); destruct (ident_eq id2 i). ++ congruence. ++ subst i. inv H; inv H0. exploit field_offset_rec_in_range. eexact H1. eauto. tauto. - subst i. intros. inv H1; inv H2. ++ subst i. inv H1; inv H2. exploit field_offset_rec_in_range. eexact H. eauto. tauto. - intros. eapply IHfld; eauto. - - apply H with fld0 0; auto. ++ eapply IHfld; eauto. Qed. (** Third, if a struct is a prefix of another, the offsets of common fields are the same. *) -Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist := - match fld1 with - | Fnil => fld2 - | Fcons id ty fld => Fcons id ty (fieldlist_app fld fld2) - end. - Lemma field_offset_prefix: - forall id ofs fld2 fld1, - field_offset id fld1 = OK ofs -> - field_offset id (fieldlist_app fld1 fld2) = OK ofs. + forall env id ofs fld2 fld1, + field_offset env id fld1 = OK ofs -> + field_offset env id (fld1 ++ fld2) = OK ofs. Proof. - intros until fld2. - assert (forall fld1 pos, - field_offset_rec id fld1 pos = OK ofs -> - field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs). - induction fld1; intros pos; simpl. congruence. - destruct (ident_eq id i); auto. - intros. unfold field_offset; auto. + intros until fld1. unfold field_offset. generalize 0 as pos. + induction fld1 as [|[i t]]; simpl; intros. +- discriminate. +- destruct (ident_eq id i); auto. Qed. (** Fourth, the position of each field respects its alignment. *) Lemma field_offset_aligned: - forall id fld ofs ty, - field_offset id fld = OK ofs -> field_type id fld = OK ty -> - (alignof ty | ofs). + forall env id fld ofs ty, + field_offset env id fld = OK ofs -> field_type id fld = OK ty -> + (alignof env ty | ofs). Proof. - assert (forall id ofs ty fld pos, - field_offset_rec id fld pos = OK ofs -> field_type id fld = OK ty -> - (alignof ty | ofs)). - induction fld; simpl; intros. - discriminate. - destruct (ident_eq id i). inv H; inv H0. - apply align_divides. apply alignof_pos. - eapply IHfld; eauto. - intros. eapply H with (pos := 0); eauto. + intros until ty. unfold field_offset. generalize 0 as pos. revert fld. + induction fld as [|[i t]]; simpl; intros. +- discriminate. +- destruct (ident_eq id i). ++ inv H; inv H0. apply align_divides. apply alignof_pos. ++ eauto. Qed. +(** ** Access modes *) + (** The [access_mode] function describes how a l-value of the given type must be accessed: - [By_value ch]: access by value, i.e. by loading from the address @@ -530,9 +566,8 @@ Definition access_mode (ty: type) : mode := | Tpointer _ _ => By_value Mint32 | Tarray _ _ _ => By_reference | Tfunction _ _ _ => By_reference - | Tstruct _ _ _ => By_copy - | Tunion _ _ _ => By_copy - | Tcomp_ptr _ _ => By_nothing + | Tstruct _ _ => By_copy + | Tunion _ _ => By_copy end. (** For the purposes of the semantics and the compiler, a type denotes @@ -545,87 +580,13 @@ Definition type_is_volatile (ty: type) : bool := | _ => false end. -(** Unroll the type of a structure or union field, substituting - [Tcomp_ptr] by a pointer to the structure. *) - -Section UNROLL_COMPOSITE. - -Variable cid: ident. -Variable comp: type. - -Fixpoint unroll_composite (ty: type) : type := - match ty with - | Tvoid => ty - | Tint _ _ _ => ty - | Tlong _ _ => ty - | Tfloat _ _ => ty - | Tpointer t1 a => Tpointer (unroll_composite t1) a - | Tarray t1 sz a => Tarray (unroll_composite t1) sz a - | Tfunction t1 t2 a => Tfunction (unroll_composite_list t1) (unroll_composite t2) a - | Tstruct id fld a => if ident_eq id cid then ty else Tstruct id (unroll_composite_fields fld) a - | Tunion id fld a => if ident_eq id cid then ty else Tunion id (unroll_composite_fields fld) a - | Tcomp_ptr id a => if ident_eq id cid then Tpointer comp a else ty - end - -with unroll_composite_list (tl: typelist) : typelist := - match tl with - | Tnil => Tnil - | Tcons t1 tl' => Tcons (unroll_composite t1) (unroll_composite_list tl') - end - -with unroll_composite_fields (fld: fieldlist) : fieldlist := - match fld with - | Fnil => Fnil - | Fcons id ty fld' => Fcons id (unroll_composite ty) (unroll_composite_fields fld') - end. - -Lemma attr_of_type_unroll_composite: - forall ty, attr_of_type (unroll_composite ty) = attr_of_type ty. -Proof. - intros. destruct ty; simpl; auto; destruct (ident_eq i cid); auto. -Qed. - -Lemma alignof_unroll_composite: - forall ty, alignof (unroll_composite ty) = alignof ty. -Proof. -Local Transparent alignof. - apply (type_ind2 (fun ty => alignof (unroll_composite ty) = alignof ty) - (fun fld => alignof_fields (unroll_composite_fields fld) = alignof_fields fld)); - simpl; intros; auto. - rewrite H; auto. - destruct (ident_eq i cid); auto. simpl. rewrite H; auto. - destruct (ident_eq i cid); auto. simpl. rewrite H; auto. - destruct (ident_eq i cid); auto. congruence. -Qed. - -Lemma sizeof_unroll_composite: - forall ty, sizeof (unroll_composite ty) = sizeof ty. -Proof. -Local Opaque alignof. - apply (type_ind2 (fun ty => sizeof (unroll_composite ty) = sizeof ty) - (fun fld => - sizeof_union (unroll_composite_fields fld) = sizeof_union fld - /\ forall pos, - sizeof_struct (unroll_composite_fields fld) pos = sizeof_struct fld pos)); - simpl; intros; auto. -- rewrite H. auto. -- rewrite <- (alignof_unroll_composite (Tstruct i f a)). simpl. - destruct H. destruct (ident_eq i cid). auto. simpl. rewrite H0. auto. -- rewrite <- (alignof_unroll_composite (Tunion i f a)). simpl. - destruct H. destruct (ident_eq i cid). auto. simpl. rewrite H. auto. -- destruct (ident_eq i cid); auto. -- destruct H0. split. - + congruence. - + intros. rewrite H1. rewrite H. rewrite alignof_unroll_composite. auto. -Qed. - -End UNROLL_COMPOSITE. +(** ** Alignment for block copy operations *) (** A variant of [alignof] for use in block copy operations. Block copy operations do not support alignments greater than 8, and require the size to be an integral multiple of the alignment. *) -Fixpoint alignof_blockcopy (t: type) : Z := +Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z := match t with | Tvoid => 1 | Tint I8 _ _ => 1 @@ -636,20 +597,22 @@ Fixpoint alignof_blockcopy (t: type) : Z := | Tfloat F32 _ => 4 | Tfloat F64 _ => 8 | Tpointer _ _ => 4 - | Tarray t' _ _ => alignof_blockcopy t' + | Tarray t' _ _ => alignof_blockcopy env t' | Tfunction _ _ _ => 1 - | Tstruct _ fld _ => Zmin 8 (alignof t) - | Tunion _ fld _ => Zmin 8 (alignof t) - | Tcomp_ptr _ _ => 4 + | Tstruct id _ | Tunion id _ => + match env!id with + | Some co => Z.min 8 (co_alignof co) + | None => 1 + end end. Lemma alignof_blockcopy_1248: - forall ty, let a := alignof_blockcopy ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8. + forall env ty, let a := alignof_blockcopy env ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8. Proof. - assert (X: forall ty, let a := Zmin 8 (alignof ty) in + assert (X: forall co, let a := Zmin 8 (co_alignof co) in a = 1 \/ a = 2 \/ a = 4 \/ a = 8). { - intros. destruct (alignof_two_p ty) as [n EQ]. unfold a; rewrite EQ. + intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ. destruct n; auto. destruct n; auto. destruct n; auto. @@ -660,45 +623,47 @@ Proof. induction ty; simpl; auto. destruct i; auto. destruct f; auto. + destruct (env!i); auto. + destruct (env!i); auto. Qed. Lemma alignof_blockcopy_pos: - forall ty, alignof_blockcopy ty > 0. + forall env ty, alignof_blockcopy env ty > 0. Proof. - intros. generalize (alignof_blockcopy_1248 ty). simpl. intuition omega. + intros. generalize (alignof_blockcopy_1248 env ty). simpl. intuition omega. Qed. Lemma sizeof_alignof_blockcopy_compat: - forall ty, (alignof_blockcopy ty | sizeof ty). + forall env ty, (alignof_blockcopy env ty | sizeof env ty). Proof. - assert (X: forall ty sz, (alignof ty | sz) -> (Zmin 8 (alignof ty) | sz)). + assert (X: forall co, (Z.min 8 (co_alignof co) | co_sizeof co)). { - intros. destruct (alignof_two_p ty) as [n EQ]. rewrite EQ in *. - destruct n; auto. - destruct n; auto. - destruct n; auto. - eapply Zdivide_trans; eauto. + intros. apply Zdivide_trans with (co_alignof co). 2: apply co_sizeof_alignof. + destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. + destruct n. apply Zdivide_refl. + destruct n. apply Zdivide_refl. + destruct n. apply Zdivide_refl. apply Z.min_case. - replace (two_power_nat (S(S(S n)))) with (two_p (3 + Z.of_nat n)). - rewrite two_p_is_exp by omega. change (two_p 3) with 8. - exists (two_p (Z.of_nat n)). ring. + exists (two_p (Z.of_nat n)). + change 8 with (two_p 3). + rewrite <- two_p_is_exp by omega. rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega. apply Zdivide_refl. } - Local Opaque alignof. induction ty; simpl. apply Zdivide_refl. - destruct i; apply Zdivide_refl. apply Zdivide_refl. - destruct f; apply Zdivide_refl. apply Zdivide_refl. - apply Z.divide_mul_l. auto. apply Zdivide_refl. - apply X. apply align_divides. apply alignof_pos. - apply X. apply align_divides. apply alignof_pos. apply Zdivide_refl. + apply Z.divide_mul_l. auto. + apply Zdivide_refl. + destruct (env!i). apply X. apply Zdivide_0. + destruct (env!i). apply X. apply Zdivide_0. Qed. +(** ** C types and back-end types *) + (** Extracting a type list from a function parameter declaration. *) Fixpoint type_of_params (params: list (ident * type)) : typelist := @@ -735,3 +700,259 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature := mksignature (typlist_of_typelist args) (opttyp_of_type res) cc. +(** * Construction of the composite environment *) + +Definition sizeof_composite (env: composite_env) (su: struct_or_union) (m: members) : Z := + match su with + | Struct => sizeof_struct env 0 m + | Union => sizeof_union env m + end. + +Lemma sizeof_composite_pos: + forall env su m, 0 <= sizeof_composite env su m. +Proof. + intros. destruct su; simpl. + apply sizeof_struct_incr. + apply sizeof_union_pos. +Qed. + +Fixpoint complete_members (env: composite_env) (m: members) : bool := + match m with + | nil => true + | (id, t) :: m' => complete_type env t && complete_members env m' + end. + +(** Convert a composite definition to its internal representation. + The size and alignment of the composite are determined at this time. + The alignment takes into account the [__Alignas] attributes + associated with the definition. The size is rounded up to a multiple + of the alignment. + + The conversion fails if a type of a member is not complete. This rules + out incorrect recursive definitions such as +<< + struct s { int x; struct s next; } +>> + Here, when we process the definition of [struct s], the identifier [s] + is not bound yet in the composite environment, hence field [next] + has an incomplete type. However, recursions that go through a pointer type + are correctly handled: +<< + struct s { int x; struct s * next; } +>> + Here, [next] has a pointer type, which is always complete, even though + [s] is not yet bound to a composite. +*) + +Program Definition composite_of_def + (env: composite_env) (id: ident) (su: struct_or_union) (m: members) (a: attr) + : res composite := + match env!id, complete_members env m return _ with + | Some _, _ => + Error (MSG "Multiple definitions of struct or union " :: CTX id :: nil) + | None, false => + Error (MSG "Incomplete struct or union " :: CTX id :: nil) + | None, true => + let al := align_attr a (alignof_composite env m) in + OK {| co_su := su; + co_members := m; + co_attr := a; + co_sizeof := align (sizeof_composite env su m) al; + co_alignof := al; + co_sizeof_pos := _; + co_alignof_two_p := _; + co_sizeof_alignof := _ |} + end. +Next Obligation. + apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. + apply align_le; apply alignof_composite_pos. +Qed. +Next Obligation. + apply align_attr_two_p. apply alignof_composite_two_p. +Qed. +Next Obligation. + apply align_divides. apply alignof_composite_pos. +Qed. + +(** The composite environment for a program is obtained by entering + its composite definitions in sequence. The definitions are assumed + to be listed in dependency order: the definition of a composite + must precede all uses of this composite, unless the use is under + a pointer or function type. *) + +Local Open Scope error_monad_scope. + +Fixpoint add_composite_definitions (env: composite_env) (defs: list composite_definition) : res composite_env := + match defs with + | nil => OK env + | Composite id su m a :: defs => + do co <- composite_of_def env id su m a; + add_composite_definitions (PTree.set id co env) defs + end. + +Definition build_composite_env (defs: list composite_definition) := + add_composite_definitions (PTree.empty _) defs. + +(** Stability properties for alignments and sizes. If the type is + complete in a composite environment [env], its size and alignment + are unchanged if we add more definitions to [env]. *) + +Section STABILITY. + +Variables env env': composite_env. +Hypothesis extends: forall id co, env!id = Some co -> env'!id = Some co. + +Lemma alignof_stable: + forall t, complete_type env t = true -> alignof env' t = alignof env t. +Proof. + induction t; simpl; intros; f_equal; auto. + destruct (env!i) as [co|] eqn:E; try discriminate. + erewrite extends by eauto. auto. + destruct (env!i) as [co|] eqn:E; try discriminate. + erewrite extends by eauto. auto. +Qed. + +Lemma sizeof_stable: + forall t, complete_type env t = true -> sizeof env' t = sizeof env t. +Proof. + induction t; simpl; intros; auto. + rewrite IHt by auto. auto. + destruct (env!i) as [co|] eqn:E; try discriminate. + erewrite extends by eauto. auto. + destruct (env!i) as [co|] eqn:E; try discriminate. + erewrite extends by eauto. auto. +Qed. + +Lemma complete_type_stable: + forall t, complete_type env t = true -> complete_type env' t = true. +Proof. + induction t; simpl; intros; auto. + destruct (env!i) as [co|] eqn:E; try discriminate. + erewrite extends by eauto. auto. + destruct (env!i) as [co|] eqn:E; try discriminate. + erewrite extends by eauto. auto. +Qed. + +Lemma alignof_composite_stable: + forall m, complete_members env m = true -> alignof_composite env' m = alignof_composite env m. +Proof. + induction m as [|[id t]]; simpl; intros. + auto. + InvBooleans. rewrite alignof_stable by auto. rewrite IHm by auto. auto. +Qed. + +Lemma sizeof_struct_stable: + forall m pos, complete_members env m = true -> sizeof_struct env' pos m = sizeof_struct env pos m. +Proof. + induction m as [|[id t]]; simpl; intros. + auto. + InvBooleans. rewrite alignof_stable by auto. rewrite sizeof_stable by auto. + rewrite IHm by auto. auto. +Qed. + +Lemma sizeof_union_stable: + forall m, complete_members env m = true -> sizeof_union env' m = sizeof_union env m. +Proof. + induction m as [|[id t]]; simpl; intros. + auto. + InvBooleans. rewrite sizeof_stable by auto. rewrite IHm by auto. auto. +Qed. + +Lemma sizeof_composite_stable: + forall su m, complete_members env m = true -> sizeof_composite env' su m = sizeof_composite env su m. +Proof. + intros. destruct su; simpl. + apply sizeof_struct_stable; auto. + apply sizeof_union_stable; auto. +Qed. + +Lemma complete_members_stable: + forall m, complete_members env m = true -> complete_members env' m = true. +Proof. + induction m as [|[id t]]; simpl; intros. + auto. + InvBooleans. rewrite complete_type_stable by auto. rewrite IHm by auto. auto. +Qed. + +End STABILITY. + +Lemma add_composite_definitions_incr: + forall id co defs env1 env2, + add_composite_definitions env1 defs = OK env2 -> + env1!id = Some co -> env2!id = Some co. +Proof. + induction defs; simpl; intros. +- inv H; auto. +- destruct a; monadInv H. + eapply IHdefs; eauto. rewrite PTree.gso; auto. + red; intros; subst id0. unfold composite_of_def in EQ. rewrite H0 in EQ; discriminate. +Qed. + +(** It follows that the sizes and alignments contained in the composite + environment produced by [build_composite_env] are consistent with + the sizes and alignments of the members of the composite types. *) + +Definition composite_consistent (env: composite_env) (co: composite) : Prop := + complete_members env (co_members co) = true + /\ co_alignof co = align_attr (co_attr co) (alignof_composite env (co_members co)) + /\ co_sizeof co = align (sizeof_composite env (co_su co) (co_members co)) (co_alignof co). + +Definition composite_env_consistent (env: composite_env) : Prop := + forall id co, env!id = Some co -> composite_consistent env co. + +Theorem build_composite_env_consistent: + forall defs env, build_composite_env defs = OK env -> composite_env_consistent env. +Proof. + cut (forall defs env0 env, + add_composite_definitions env0 defs = OK env -> + composite_env_consistent env0 -> + composite_env_consistent env). + intros. eapply H; eauto. red; intros. rewrite PTree.gempty in H1; discriminate. + induction defs as [|d1 defs]; simpl; intros. +- inv H; auto. +- destruct d1; monadInv H. + eapply IHdefs; eauto. + set (env1 := PTree.set id x env0) in *. + unfold composite_of_def in EQ. + destruct (env0!id) eqn:E; try discriminate. + destruct (complete_members env0 m) eqn:C; inversion EQ; clear EQ. + assert (forall id1 co1, env0!id1 = Some co1 -> env1!id1 = Some co1). + { intros. unfold env1. rewrite PTree.gso; auto. congruence. } + red; intros. unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id). ++ subst id0. inversion H2; clear H2. subst co. + red; rewrite <- H1; simpl. + assert (A: alignof_composite env1 m = alignof_composite env0 m) + by (apply alignof_composite_stable; assumption). + rewrite A. + split. eapply complete_members_stable; eauto. + split. auto. + f_equal. symmetry. apply sizeof_composite_stable; assumption. ++ exploit H0; eauto. intros (P & Q & R). + assert (A: alignof_composite env1 (co_members co) = alignof_composite env0 (co_members co)) + by (apply alignof_composite_stable; assumption). + red. rewrite A. + split. eapply complete_members_stable; eauto. + split. auto. + rewrite R. f_equal. symmetry. apply sizeof_composite_stable; assumption. +Qed. + +(** Moreover, every composite definition is reflected in the composite environment. *) + +Theorem build_composite_env_charact: + forall id su m a defs env, + build_composite_env defs = OK env -> + In (Composite id su m a) defs -> + exists co, env!id = Some co /\ co_members co = m /\ co_attr co = a /\ co_su co = su. +Proof. + intros until defs. unfold build_composite_env. generalize (PTree.empty composite) as env0. + revert defs. induction defs as [|d1 defs]; simpl; intros. +- contradiction. +- destruct d1; monadInv H. + destruct H0; [idtac|eapply IHdefs;eauto]. inv H. + unfold composite_of_def in EQ. + destruct (env0!id) eqn:E; try discriminate. + destruct (complete_members env0 m) eqn:C; simplify_eq EQ. clear EQ; intros EQ. + exists x. + split. eapply add_composite_definitions_incr; eauto. apply PTree.gss. + subst x; auto. +Qed. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 6f193cd9..025960d7 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -13,6 +13,7 @@ (** Compile-time evaluation of initializers for global C variables. *) Require Import Coqlib. +Require Import Maps. Require Import Errors. Require Import Integers. Require Import Floats. @@ -51,7 +52,13 @@ Definition do_cast (v: val) (t1 t2: type) : res val := | None => Error(msg "undefined cast") end. -Fixpoint constval (a: expr) : res val := +Definition lookup_composite (ce: composite_env) (id: ident) : res composite := + match ce!id with + | Some co => OK co + | None => Error (MSG "Undefined struct or union " :: CTX id :: nil) + end. + +Fixpoint constval (ce: composite_env) (a: expr) : res val := match a with | Eval v ty => match v with @@ -60,74 +67,75 @@ Fixpoint constval (a: expr) : res val := end | Evalof l ty => match access_mode ty with - | By_reference | By_copy => constval l + | By_reference | By_copy => constval ce l | _ => Error(msg "dereferencing of an l-value") end | Eaddrof l ty => - constval l + constval ce l | Eunop op r1 ty => - do v1 <- constval r1; + do v1 <- constval ce 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 + do v1 <- constval ce r1; + do v2 <- constval ce r2; + match sem_binary_operation ce 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 v1 <- constval r; do_cast v1 (typeof r) ty + do v1 <- constval ce r; do_cast v1 (typeof r) ty | Esizeof ty1 ty => - OK (Vint (Int.repr (sizeof ty1))) + OK (Vint (Int.repr (sizeof ce ty1))) | Ealignof ty1 ty => - OK (Vint (Int.repr (alignof ty1))) + OK (Vint (Int.repr (alignof ce ty1))) | Eseqand r1 r2 ty => - do v1 <- constval r1; - do v2 <- constval r2; + do v1 <- constval ce r1; + do v2 <- constval ce r2; match bool_val v1 (typeof r1) with | Some true => do_cast v2 (typeof r2) type_bool | Some false => OK (Vint Int.zero) | None => Error(msg "undefined && operation") end | Eseqor r1 r2 ty => - do v1 <- constval r1; - do v2 <- constval r2; + do v1 <- constval ce r1; + do v2 <- constval ce r2; match bool_val v1 (typeof r1) with | Some false => do_cast v2 (typeof r2) type_bool | Some true => OK (Vint Int.one) | None => Error(msg "undefined || operation") end | Econdition r1 r2 r3 ty => - do v1 <- constval r1; - do v2 <- constval r2; - do v3 <- constval r3; + do v1 <- constval ce r1; + do v2 <- constval ce r2; + do v3 <- constval ce r3; match bool_val v1 (typeof r1) with | Some true => do_cast v2 (typeof r2) ty | Some false => do_cast v3 (typeof r3) ty | None => Error(msg "condition is undefined") end | Ecomma r1 r2 ty => - do v1 <- constval r1; constval r2 + do v1 <- constval ce r1; constval ce r2 | Evar x ty => OK(Vptr x Int.zero) | Ederef r ty => - constval r + constval ce r | Efield l f ty => match typeof l with - | Tstruct id fList _ => - do delta <- field_offset f fList; - do v <- constval l; + | Tstruct id _ => + do co <- lookup_composite ce id; + do delta <- field_offset ce f (co_members co); + do v <- constval ce l; OK (Val.add v (Vint (Int.repr delta))) - | Tunion id fList _ => - constval l + | Tunion id _ => + constval ce l | _ => Error(msg "ill-typed field access") end | Eparen r tycast ty => - do v <- constval r; do_cast v (typeof r) tycast + do v <- constval ce r; do_cast v (typeof r) tycast | _ => Error(msg "not a compile-time constant") end. @@ -146,21 +154,19 @@ with initializer_list := (** Translate an initializing expression [a] for a scalar variable of type [ty]. Return the corresponding initialization datum. *) -Definition transl_init_single (ty: type) (a: expr) : res init_data := - do v1 <- constval a; +Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res init_data := + do v1 <- constval ce a; do v2 <- do_cast v1 (typeof a) ty; match v2, ty with | Vint n, Tint (I8|IBool) 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) - | Vint n, Tcomp_ptr _ _ => OK(Init_int32 n) | Vlong n, Tlong _ _ => OK(Init_int64 n) | Vsingle f, Tfloat F32 _ => OK(Init_float32 f) | Vfloat f, Tfloat F64 _ => OK(Init_float64 f) | Vptr id ofs, Tint I32 sg _ => OK(Init_addrof id ofs) | Vptr id ofs, Tpointer _ _ => OK(Init_addrof id ofs) - | Vptr id ofs, Tcomp_ptr _ _ => OK(Init_addrof id ofs) | Vundef, _ => Error(msg "undefined operation in initializer") | _, _ => Error (msg "type mismatch in initializer") end. @@ -171,46 +177,55 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data := Definition padding (frm to: Z) : list init_data := if zlt frm to then Init_space (to - frm) :: nil else nil. -Fixpoint transl_init (ty: type) (i: initializer) +Fixpoint transl_init (ce: composite_env) (ty: type) (i: initializer) {struct i} : res (list init_data) := match i, ty with | Init_single a, _ => - do d <- transl_init_single ty a; OK (d :: nil) + do d <- transl_init_single ce ty a; OK (d :: nil) | Init_array il, Tarray tyelt nelt _ => - transl_init_array tyelt il (Zmax 0 nelt) - | Init_struct il, Tstruct id fl _ => - transl_init_struct id ty fl il 0 - | Init_union f i1, Tunion id fl _ => - do ty1 <- field_type f fl; - do d <- transl_init ty1 i1; - OK (d ++ padding (sizeof ty1) (sizeof ty)) + transl_init_array ce tyelt il (Zmax 0 nelt) + | Init_struct il, Tstruct id _ => + do co <- lookup_composite ce id; + match co_su co with + | Struct => transl_init_struct ce ty (co_members co) il 0 + | Union => Error (MSG "struct/union mismatch on " :: CTX id :: nil) + end + | Init_union f i1, Tunion id _ => + do co <- lookup_composite ce id; + match co_su co with + | Struct => Error (MSG "union/struct mismatch on " :: CTX id :: nil) + | Union => + do ty1 <- field_type f (co_members co); + do d <- transl_init ce ty1 i1; + OK (d ++ padding (sizeof ce ty1) (sizeof ce ty)) + end | _, _ => Error (msg "wrong type for compound initializer") end -with transl_init_array (ty: type) (il: initializer_list) (sz: Z) +with transl_init_array (ce: composite_env) (ty: type) (il: initializer_list) (sz: Z) {struct il} : res (list init_data) := match il with | Init_nil => if zeq sz 0 then OK nil - else if zle 0 sz then OK (Init_space (sz * sizeof ty) :: nil) + else if zle 0 sz then OK (Init_space (sz * sizeof ce ty) :: nil) else Error (msg "wrong number of elements in array initializer") | Init_cons i1 il' => - do d1 <- transl_init ty i1; - do d2 <- transl_init_array ty il' (sz - 1); + do d1 <- transl_init ce ty i1; + do d2 <- transl_init_array ce ty il' (sz - 1); OK (d1 ++ d2) end -with transl_init_struct (id: ident) (ty: type) - (fl: fieldlist) (il: initializer_list) (pos: Z) +with transl_init_struct (ce: composite_env) (ty: type) + (fl: members) (il: initializer_list) (pos: Z) {struct il} : res (list init_data) := match il, fl with - | Init_nil, Fnil => - OK (padding pos (sizeof ty)) - | Init_cons i1 il', Fcons _ ty1 fl' => - let pos1 := align pos (alignof ty1) in - do d1 <- transl_init ty1 i1; - do d2 <- transl_init_struct id ty fl' il' (pos1 + sizeof ty1); + | Init_nil, nil => + OK (padding pos (sizeof ce ty)) + | Init_cons i1 il', (_, ty1) :: fl' => + let pos1 := align pos (alignof ce ty1) in + do d1 <- transl_init ce ty1 i1; + do d2 <- transl_init_struct ce ty fl' il' (pos1 + sizeof ce ty1); OK (padding pos pos1 ++ d1 ++ d2) | _, _ => Error (msg "wrong number of elements in struct initializer") diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 73fd90b7..225dc23e 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -90,13 +90,13 @@ Inductive eval_simple_lvalue: expr -> block -> int -> Prop := | 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 r f ty b ofs id fList a delta, + | esl_field_struct: forall r f ty b ofs id co a delta, eval_simple_rvalue r (Vptr b ofs) -> - typeof r = Tstruct id fList a -> field_offset f fList = OK delta -> + typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta -> eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta)) - | esl_field_union: forall r f ty b ofs id fList a, + | esl_field_union: forall r f ty b ofs id a, eval_simple_rvalue r (Vptr b ofs) -> - typeof r = Tunion id fList a -> + typeof r = Tunion id a -> eval_simple_lvalue (Efield r f ty) b ofs with eval_simple_rvalue: expr -> val -> Prop := @@ -116,16 +116,16 @@ with eval_simple_rvalue: expr -> val -> Prop := 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 -> + sem_binary_operation ge 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 -> sem_cast v1 (typeof r1) ty = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, - eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))) + eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) | esr_alignof: forall ty1 ty, - eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ty1))) + eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))) | esr_seqand_true: forall r1 r2 ty v1 v2 v3, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) = Some true -> eval_simple_rvalue r2 v2 -> @@ -372,13 +372,13 @@ Lemma constval_rvalue: forall m a v, eval_simple_rvalue empty_env m a v -> forall v', - constval a = OK v' -> + constval ge a = OK v' -> val_inject inj 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' -> + constval ge a = OK v' -> val_inject inj v' (Vptr b ofs). Proof. (* rvalue *) @@ -394,7 +394,7 @@ Proof. exploit sem_unary_operation_inject. eexact E. eauto. intros [v' [A B]]. congruence. (* binop *) - destruct (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2. + destruct (sem_binary_operation ge op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2. exploit (sem_binary_operation_inj inj Mem.empty m). intros. rewrite mem_empty_not_valid_pointer in H3; discriminate. intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate. @@ -443,8 +443,9 @@ Proof. (* deref *) eauto. (* field struct *) - rewrite H0 in CV. monadInv CV. exploit constval_rvalue; eauto. intro MV. inv MV. - simpl. replace x with delta by congruence. econstructor; eauto. + rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ. + exploit constval_rvalue; eauto. intro MV. inv MV. + simpl. replace x0 with delta by congruence. econstructor; eauto. rewrite ! Int.add_assoc. f_equal. apply Int.add_commut. simpl. auto. (* field union *) @@ -452,7 +453,7 @@ Proof. Qed. Lemma constval_simple: - forall a v, constval a = OK v -> simple a. + forall a v, constval ge a = OK v -> simple a. Proof. induction a; simpl; intros vx CV; try (monadInv CV); eauto. destruct (typeof a); discriminate || eauto. @@ -466,7 +467,7 @@ Qed. Theorem constval_steps: forall f r m v v' ty m', star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') -> - constval r = OK v -> + constval ge r = OK v -> m' = m /\ ty = typeof r /\ val_inject inj v v'. Proof. intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. @@ -479,7 +480,7 @@ Qed. Theorem transl_init_single_steps: forall ty a data f m v1 ty1 m' v chunk b ofs m'', - transl_init_single ty a = OK data -> + 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 -> access_mode ty = By_value chunk -> @@ -522,15 +523,14 @@ Qed. Lemma transl_init_single_size: forall ty a data, - transl_init_single ty a = OK data -> - Genv.init_data_size data = sizeof ty. + transl_init_single ge ty a = OK data -> + Genv.init_data_size data = sizeof ge ty. Proof. intros. monadInv H. destruct x0. - monadInv EQ2. - destruct ty; try discriminate. destruct i0; inv EQ2; auto. inv EQ2; auto. - inv EQ2; auto. - destruct ty; inv EQ2; auto. - destruct ty; try discriminate. destruct f0; inv EQ2; auto. @@ -539,7 +539,6 @@ Proof. - destruct ty; try discriminate. destruct i0; inv EQ2; auto. inv EQ2; auto. - inv EQ2; auto. Qed. Notation idlsize := Genv.init_data_list_size. @@ -561,30 +560,32 @@ Proof. Qed. Remark union_field_size: - forall f ty fl, field_type f fl = OK ty -> sizeof ty <= sizeof_union fl. + forall f ty fl, field_type f fl = OK ty -> sizeof ge ty <= sizeof_union ge fl. Proof. - induction fl; simpl; intros. + induction fl as [|[i t]]; simpl; intros. - inv H. - destruct (ident_eq f i). + inv H. xomega. + specialize (IHfl H). xomega. Qed. +Hypothesis ce_consistent: composite_env_consistent ge. + Lemma transl_init_size: forall i ty data, - transl_init ty i = OK data -> - idlsize data = sizeof ty + transl_init ge ty i = OK data -> + idlsize data = sizeof ge ty with transl_init_list_size: forall il, (forall ty sz data, - transl_init_array ty il sz = OK data -> - idlsize data = sizeof ty * sz) + transl_init_array ge ty il sz = OK data -> + idlsize data = sizeof ge ty * sz) /\ - (forall id ty fl pos data, - transl_init_struct id ty fl il pos = OK data -> - sizeof_struct fl pos <= sizeof ty -> - idlsize data + pos = sizeof ty). + (forall ty fl pos data, + transl_init_struct ge ty fl il pos = OK data -> + sizeof_struct ge pos fl <= sizeof ge ty -> + idlsize data + pos = sizeof ge ty). Proof. - induction i; intros. @@ -595,27 +596,35 @@ Proof. simpl. eapply (proj1 (transl_init_list_size il)); eauto. + (* struct *) simpl in H. destruct ty; try discriminate. + monadInv H. destruct (co_su x) eqn:?; try discriminate. replace (idlsize data) with (idlsize data + 0) by omega. eapply (proj2 (transl_init_list_size il)). eauto. -Local Opaque alignof. - simpl. apply align_le. apply alignof_pos. + unfold lookup_composite in EQ. simpl. destruct (ge.(genv_cenv)!i) as [co|] eqn:?; inv EQ. + exploit ce_consistent; eauto. intros (A & B & C). + rewrite C. unfold sizeof_composite. rewrite Heqs. apply align_le. + destruct (co_alignof_two_p x) as [n EQ]. rewrite EQ. apply two_power_nat_pos. + (* union *) simpl in H. destruct ty; try discriminate. - set (sz := sizeof (Tunion i0 f0 a)) in *. - monadInv H. rewrite idlsize_app. rewrite (IHi _ _ EQ1). - rewrite padding_size. omega. unfold sz. simpl. - apply Zle_trans with (sizeof_union f0). eapply union_field_size; eauto. - apply align_le. apply alignof_pos. + monadInv H. destruct (co_su x) eqn:?; try discriminate. + monadInv EQ0. + rewrite idlsize_app. rewrite (IHi _ _ EQ0). + unfold lookup_composite in EQ. simpl. destruct (ge.(genv_cenv)!i0) as [co|] eqn:?; inv EQ. + rewrite padding_size. omega. + apply Zle_trans with (sizeof_union ge (co_members x)). + eapply union_field_size; eauto. + exploit ce_consistent; eauto. intros (A & B & C). + rewrite C. unfold sizeof_composite. rewrite Heqs. apply align_le. + destruct (co_alignof_two_p x) as [n EQ]. rewrite EQ. apply two_power_nat_pos. - induction il. + (* base cases *) - simpl. intuition. + simpl. intuition auto. * (* arrays *) destruct (zeq sz 0). inv H. simpl; ring. destruct (zle 0 sz); inv H. simpl. rewrite Z.mul_comm. - assert (0 <= sizeof ty * sz). - { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ty); omega. } + assert (0 <= sizeof ge ty * sz). + { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. } zify; omega. * (* structs *) destruct fl; inv H. @@ -629,12 +638,12 @@ Local Opaque alignof. rewrite (A _ _ _ EQ1). ring. * (* structs *) - intros. simpl in H. destruct fl; monadInv H. + intros. simpl in H. destruct fl as [|[i1 t1]]; monadInv H. rewrite ! idlsize_app. simpl in H0. rewrite padding_size. rewrite (transl_init_size _ _ _ EQ). - rewrite <- (B _ _ _ _ _ EQ1). omega. + rewrite <- (B _ _ _ _ EQ1). omega. auto. apply align_le. apply alignof_pos. Qed. @@ -642,11 +651,11 @@ Qed. Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip. -Fixpoint fields_of_struct (id: ident) (ty: type) (fl: fieldlist) (pos: Z) : list (Z * type) := +Fixpoint fields_of_struct (fl: members) (pos: Z) : list (Z * type) := match fl with - | Fnil => nil - | Fcons id1 ty1 fl' => - (align pos (alignof ty1), ty1) :: fields_of_struct id ty fl' (align pos (alignof ty1) + sizeof ty1) + | nil => nil + | (id1, ty1) :: fl' => + (align pos (alignof ge ty1), ty1) :: fields_of_struct fl' (align pos (alignof ge ty1) + sizeof ge ty1) end. Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := @@ -660,13 +669,15 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := | exec_init_array_: forall m b ofs ty sz a il m', exec_init_array m b ofs ty sz il m' -> exec_init m b ofs (Tarray ty sz a) (Init_array il) m' - | exec_init_struct: forall m b ofs id fl a il m', - exec_init_list m b ofs (fields_of_struct id (Tstruct id fl a) fl 0) il m' -> - exec_init m b ofs (Tstruct id fl a) (Init_struct il) m' - | exec_init_union: forall m b ofs id fl a f i ty m', - field_type f fl = OK ty -> + | exec_init_struct: forall m b ofs id a il co m', + ge.(genv_cenv)!id = Some co -> co_su co = Struct -> + exec_init_list m b ofs (fields_of_struct (co_members co) 0) il m' -> + exec_init m b ofs (Tstruct id a) (Init_struct il) m' + | exec_init_union: forall m b ofs id a f i ty co m', + ge.(genv_cenv)!id = Some co -> co_su co = Union -> + field_type f (co_members co) = OK ty -> exec_init m b ofs ty i m' -> - exec_init m b ofs (Tunion id fl a) (Init_union f i) m' + exec_init m b ofs (Tunion id a) (Init_union f i) m' with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop := | exec_init_array_nil: forall m b ofs ty sz, @@ -674,7 +685,7 @@ with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem exec_init_array m b ofs ty sz Init_nil m | exec_init_array_cons: forall m b ofs ty sz i1 il m' m'', exec_init m b ofs ty i1 m' -> - exec_init_array m' b (ofs + sizeof ty) ty (sz - 1) il m'' -> + exec_init_array m' b (ofs + sizeof ge ty) ty (sz - 1) il m'' -> exec_init_array m b ofs ty sz (Init_cons i1 il) m'' with exec_init_list: mem -> block -> Z -> list (Z * type) -> initializer_list -> mem -> Prop := @@ -718,15 +729,15 @@ Qed. Lemma transl_init_sound_gen: (forall m b ofs ty i m', exec_init m b ofs ty i m' -> - forall data, transl_init ty i = OK data -> + forall data, transl_init ge ty i = OK data -> Genv.store_init_data_list ge m b ofs data = Some m') /\(forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' -> - forall data, transl_init_array ty il sz = OK data -> + forall data, transl_init_array ge ty il sz = OK data -> Genv.store_init_data_list ge m b ofs data = Some m') /\(forall m b ofs l il m', exec_init_list m b ofs l il m' -> - forall id ty fl data pos, - l = fields_of_struct id ty fl pos -> - transl_init_struct id ty fl il pos = OK data -> + forall ty fl data pos, + l = fields_of_struct fl pos -> + transl_init_struct ge ty fl il pos = OK data -> Genv.store_init_data_list ge m b (ofs + pos) data = Some m'). Proof. Local Opaque sizeof. @@ -737,9 +748,11 @@ Local Opaque sizeof. replace (Z.max 0 sz) with sz in H1. eauto. assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. - (* struct *) + unfold lookup_composite in H3. rewrite H in H3. simpl in H3. rewrite H0 in H3. replace ofs with (ofs + 0) by omega. eauto. - (* union *) - rewrite H in H2. monadInv H2. inv EQ. + unfold lookup_composite in H4. rewrite H in H4. simpl in H4. rewrite H0 in H4. + monadInv H4. assert (x = ty) by congruence. subst x. eapply store_init_data_list_app. eauto. apply store_init_data_list_padding. @@ -753,15 +766,15 @@ Local Opaque sizeof. eauto. rewrite (transl_init_size _ _ _ EQ). eauto. - (* struct, empty *) - destruct fl; simpl in H; inv H. - inv H0. apply store_init_data_list_padding. + destruct fl as [|[i t]]; simpl in H0; inv H0. + apply store_init_data_list_padding. - (* struct, nonempty *) - destruct fl; simpl in H3; inv H3. - monadInv H4. + destruct fl as [|[i t]]; simpl in H4; monadInv H4. + simpl in H3; inv H3. eapply store_init_data_list_app. apply store_init_data_list_padding. rewrite padding_size. - replace (ofs + pos0 + (align pos0 (alignof t) - pos0)) - with (ofs + align pos0 (alignof t)) by omega. + replace (ofs + pos0 + (align pos0 (alignof ge t) - pos0)) + with (ofs + align pos0 (alignof ge t)) by omega. eapply store_init_data_list_app. eauto. rewrite (transl_init_size _ _ _ EQ). @@ -769,15 +782,18 @@ Local Opaque sizeof. apply align_le. apply alignof_pos. Qed. +End SOUNDNESS. + Theorem transl_init_sound: - forall m b ty i m' data, - exec_init m b 0 ty i m' -> - transl_init ty i = OK data -> - Genv.store_init_data_list ge m b 0 data = Some m'. + forall p m b ty i m' data, + exec_init (globalenv p) m b 0 ty i m' -> + transl_init (prog_comp_env p) ty i = OK data -> + Genv.store_init_data_list (globalenv p) m b 0 data = Some m'. Proof. - intros. eapply (proj1 transl_init_sound_gen); eauto. + intros. + set (ge := globalenv p) in *. + change (prog_comp_env p) with (genv_cenv ge) in H0. + destruct (transl_init_sound_gen ge) as (A & B & C). + eapply build_composite_env_consistent. apply prog_comp_env_eq. + eapply A; eauto. Qed. - -End SOUNDNESS. - - diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index c5a6e6e1..ebd06c54 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -45,6 +45,8 @@ let rec precedence = function | Econst_float _ -> (16, NA) | Econst_single _ -> (16, NA) | Econst_long _ -> (16, NA) + | Esizeof _ -> (15, RtoL) + | Ealignof _ -> (15, RtoL) | Eunop _ -> (15, RtoL) | Eaddrof _ -> (15, RtoL) | Ecast _ -> (14, RtoL) @@ -100,6 +102,10 @@ let rec expr p (prec, e) = expr (prec1, a1) (name_binop op) expr (prec2, a2) | Ecast(a1, ty) -> fprintf p "(%s) %a" (name_type ty) expr (prec', a1) + | Esizeof(ty, _) -> + fprintf p "sizeof(%s)" (name_type ty) + | Ealignof(ty, _) -> + fprintf p "__alignof__(%s)" (name_type ty) end; if prec' < prec then fprintf p ")@]" else fprintf p "@]" @@ -265,71 +271,10 @@ let print_globdef p (id, gd) = | Gfun f -> print_fundef p id f | Gvar v -> print_globvar p id v (* from PrintCsyntax *) -(* Collect struct and union types *) - -let rec collect_expr e = - collect_type (typeof e); - match e with - | Econst_int _ -> () - | Econst_float _ -> () - | Econst_single _ -> () - | Econst_long _ -> () - | Evar _ -> () - | Etempvar _ -> () - | Ederef(r, _) -> collect_expr r - | Efield(l, _, _) -> collect_expr l - | Eaddrof(l, _) -> collect_expr l - | Eunop(_, r, _) -> collect_expr r - | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2 - | Ecast(r, _) -> collect_expr r - -let rec collect_exprlist = function - | [] -> () - | r1 :: rl -> collect_expr r1; collect_exprlist rl - -let rec collect_stmt = function - | Sskip -> () - | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 - | Sset(id, e2) -> collect_expr e2 - | Scall(optid, e1, el) -> collect_expr e1; collect_exprlist el - | Sbuiltin(optid, ef, tyargs, el) -> collect_exprlist el - | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 - | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 - | Sloop(s1, s2) -> collect_stmt s1; collect_stmt s2 - | Sbreak -> () - | Scontinue -> () - | Sswitch(e, cases) -> collect_expr e; collect_cases cases - | Sreturn None -> () - | Sreturn (Some e) -> collect_expr e - | Slabel(lbl, s) -> collect_stmt s - | Sgoto lbl -> () - -and collect_cases = function - | LSnil -> () - | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem - -let collect_function f = - collect_type f.fn_return; - List.iter (fun (id, ty) -> collect_type ty) f.fn_params; - List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; - List.iter (fun (id, ty) -> collect_type ty) f.fn_temps; - collect_stmt f.fn_body - -let collect_globdef (id, gd) = - match gd with - | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res - | Gfun(Internal f) -> collect_function f - | Gvar v -> collect_type v.gvar_info - -let collect_program p = - List.iter collect_globdef p.prog_defs - let print_program p prog = - struct_unions := StructUnion.empty; - collect_program prog; fprintf p "@["; - StructUnion.iter (declare_struct_or_union p) !struct_unions; - StructUnion.iter (print_struct_or_union p) !struct_unions; + List.iter (declare_composite p) prog.prog_types; + List.iter (define_composite p) prog.prog_types; List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index e1b53af8..8a4d60a5 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -70,12 +70,6 @@ let name_longtype sg = | Signed -> "long long" | Unsigned -> "unsigned long long" -(* Collecting the names and fields of structs and unions *) - -module StructUnion = Map.Make(String) - -let struct_unions = ref StructUnion.empty - (* Declarator (identifier + type) *) let attributes a = @@ -132,12 +126,10 @@ let rec name_cdecl id ty = add_args true args; Buffer.add_char b ')'; name_cdecl (Buffer.contents b) res - | Tstruct(name, fld, a) -> - extern_atom name ^ attributes a ^ name_optid id - | Tunion(name, fld, a) -> - extern_atom name ^ attributes a ^ name_optid id - | Tcomp_ptr(name, a) -> - extern_atom name ^ " *" ^ attributes a ^ id + | Tstruct(name, a) -> + "struct " ^ extern_atom name ^ attributes a ^ name_optid id + | Tunion(name, a) -> + "union " ^ extern_atom name ^ attributes a ^ name_optid id (* Type *) @@ -466,7 +458,7 @@ let print_globvar p id v = fprintf p "@[%s = " (name_cdecl name2 v.gvar_info); begin match v.gvar_info, v.gvar_init with - | (Tint _ | Tlong _ | Tfloat _ | Tpointer _ | Tfunction _ | Tcomp_ptr _), + | (Tint _ | Tlong _ | Tfloat _ | Tpointer _ | Tfunction _), [i1] -> print_init p i1 | _, il -> @@ -482,119 +474,24 @@ let print_globdef p (id, gd) = | Gfun f -> print_fundef p id f | Gvar v -> print_globvar p id v -(* Collect struct and union types *) - -let rec collect_type = function - | Tvoid -> () - | Tint _ -> () - | Tfloat _ -> () - | Tlong _ -> () - | Tpointer(t, _) -> collect_type t - | Tarray(t, _, _) -> collect_type t - | Tfunction(args, res, _) -> collect_type_list args; collect_type res - | Tstruct(id, fld, _) | Tunion(id, fld, _) -> - let s = extern_atom id in - if not (StructUnion.mem s !struct_unions) then begin - struct_unions := StructUnion.add s fld !struct_unions; - collect_fields fld - end - | Tcomp_ptr _ -> () - -and collect_type_list = function - | Tnil -> () - | Tcons(hd, tl) -> collect_type hd; collect_type_list tl - -and collect_fields = function - | Fnil -> () - | Fcons(id, hd, tl) -> collect_type hd; collect_fields tl - -let rec collect_expr e = - collect_type (typeof e); - match e with - | Eloc _ -> assert false - | Evar _ -> () - | Ederef(r, _) -> collect_expr r - | Efield(l, _, _) -> collect_expr l - | Eval _ -> () - | Evalof(l, _) -> collect_expr l - | Eaddrof(l, _) -> collect_expr l - | Eunop(_, r, _) -> collect_expr r - | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2 - | Ecast(r, _) -> collect_expr r - | Eseqand(r1, r2, _) -> collect_expr r1; collect_expr r2 - | Eseqor(r1, r2, _) -> collect_expr r1; collect_expr r2 - | Econdition(r1, r2, r3, _) -> - collect_expr r1; collect_expr r2; collect_expr r3 - | Esizeof(ty, _) -> collect_type ty - | Ealignof(ty, _) -> collect_type ty - | Eassign(l, r, _) -> collect_expr l; collect_expr r - | Eassignop(_, l, r, _, _) -> collect_expr l; collect_expr r - | Epostincr(_, l, _) -> collect_expr l - | Ecomma(r1, r2, _) -> collect_expr r1; collect_expr r2 - | Ecall(r1, rl, _) -> collect_expr r1; collect_exprlist rl - | Ebuiltin(_, _, rl, _) -> collect_exprlist rl - | Eparen _ -> assert false - -and collect_exprlist = function - | Enil -> () - | Econs(r1, rl) -> collect_expr r1; collect_exprlist rl - -let rec collect_stmt = function - | Sskip -> () - | Sdo e -> collect_expr e - | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 - | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 - | Swhile(e, s) -> collect_expr e; collect_stmt s - | Sdowhile(e, s) -> collect_stmt s; collect_expr e - | Sfor(s_init, e, s_iter, s_body) -> - collect_stmt s_init; collect_expr e; - collect_stmt s_iter; collect_stmt s_body - | Sbreak -> () - | Scontinue -> () - | Sswitch(e, cases) -> collect_expr e; collect_cases cases - | Sreturn None -> () - | Sreturn (Some e) -> collect_expr e - | Slabel(lbl, s) -> collect_stmt s - | Sgoto lbl -> () - -and collect_cases = function - | LSnil -> () - | LScons(lbl, s, rem) -> collect_stmt s; collect_cases rem - -let collect_function f = - collect_type f.fn_return; - List.iter (fun (id, ty) -> collect_type ty) f.fn_params; - List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; - collect_stmt f.fn_body - -let collect_globdef (id, gd) = - match gd with - | Gfun(External(_, args, res, _)) -> collect_type_list args; collect_type res - | Gfun(Internal f) -> collect_function f - | Gvar v -> collect_type v.gvar_info - -let collect_program p = - List.iter collect_globdef p.prog_defs - -let declare_struct_or_union p name fld = - fprintf p "%s;@ @ " name - -let print_struct_or_union p name fld = - fprintf p "@[%s {" name; - let rec print_fields = function - | Fnil -> () - | Fcons(id, ty, rem) -> - fprintf p "@ %s;" (name_cdecl (extern_atom id) ty); - print_fields rem in - print_fields fld; +let struct_or_union = function Struct -> "struct" | Union -> "union" + +let declare_composite p (Composite(id, su, m, a)) = + fprintf p "%s %s;@ " (struct_or_union su) (extern_atom id) + +let define_composite p (Composite(id, su, m, a)) = + fprintf p "@[%s %s%s {" + (struct_or_union su) (extern_atom id) (attributes a); + List.iter + (fun (fid, fty) -> + fprintf p "@ %s;" (name_cdecl (extern_atom fid) fty)) + m; fprintf p "@;<0 -2>};@]@ @ " let print_program p prog = - struct_unions := StructUnion.empty; - collect_program prog; fprintf p "@["; - StructUnion.iter (declare_struct_or_union p) !struct_unions; - StructUnion.iter (print_struct_or_union p) !struct_unions; + List.iter (declare_composite p) prog.prog_types; + List.iter (define_composite p) prog.prog_types; List.iter (print_globdef p) prog.prog_defs; fprintf p "@]@." diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 089797f2..36fe07ae 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -540,5 +540,10 @@ Fixpoint transl_globdefs end. Definition transl_program (p: Csyntax.program) : res program := - do gl' <- transl_globdefs p.(prog_defs) (initial_generator tt); - OK (mkprogram gl' p.(prog_public) p.(prog_main)). + do gl' <- transl_globdefs (Csyntax.prog_defs p) (initial_generator tt); + OK {| prog_defs := gl'; + prog_public := Csyntax.prog_public p; + prog_main := Csyntax.prog_main p; + prog_types := Csyntax.prog_types p; + prog_comp_env := Csyntax.prog_comp_env p; + prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 6d8b5c86..74019061 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -37,11 +37,17 @@ Variable prog: Csyntax.program. Variable tprog: Clight.program. Hypothesis TRANSL: transl_program prog = OK tprog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. +Let ge := Csem.globalenv prog. +Let tge := Clight.globalenv tprog. (** Invariance properties. *) +Lemma comp_env_preserved: + Clight.genv_cenv tge = Csem.genv_cenv ge. +Proof. + monadInv TRANSL. unfold tge; rewrite <- H0; auto. +Qed. + Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. @@ -87,7 +93,7 @@ Proof. - destruct (Genv.find_var_info tge b) as [v'|] eqn:V'; auto. exploit Genv.find_var_info_rev_match. eapply transl_program_spec; eauto. eassumption. simpl. destruct (plt b (Genv.genv_next (Genv.globalenv prog))); try tauto. - intros [v [A B]]. inv B. fold ge in A. congruence. + intros [v [A B]]. inv B. change (Genv.globalenv prog) with (Csem.genv_genv ge) in A. congruence. Qed. Lemma block_is_volatile_preserved: @@ -173,7 +179,7 @@ Remark assign_loc_translated: forall ty m b ofs v t m', Csem.assign_loc ge ty m b ofs v t m' -> match chunk_for_volatile_type ty with - | None => t = E0 /\ Clight.assign_loc ty m b ofs v m' + | None => t = E0 /\ Clight.assign_loc tge ty m b ofs v m' | Some chunk => volatile_store tge chunk m b ofs v t m' end. Proof. @@ -184,7 +190,8 @@ Proof. rewrite H0; rewrite H1. eapply volatile_store_preserved with (ge1 := ge); auto. exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. (* By copy *) - rewrite H0. destruct (type_is_volatile ty); split; auto; eapply assign_loc_copy; eauto. + rewrite H0. rewrite <- comp_env_preserved in *. + destruct (type_is_volatile ty); split; auto; eapply assign_loc_copy; eauto. Qed. (** Evaluation of simple expressions and of their translation *) @@ -241,7 +248,7 @@ Opaque makeif. exploit H0; eauto. intros [A [B C]]. exploit H2; eauto. intros [D [E F]]. subst sl1 sl2; simpl. - assert (eval_expr tge e le m (Ebinop op a1 a2 ty) v). econstructor; eauto. congruence. + assert (eval_expr tge e le m (Ebinop op a1 a2 ty) v). econstructor; eauto. rewrite comp_env_preserved; congruence. destruct dst; auto. simpl; econstructor; eauto. (* cast *) exploit H0; eauto. intros [A [B C]]. @@ -249,11 +256,13 @@ Opaque makeif. assert (eval_expr tge e le m (Ecast a1 ty) v). econstructor; eauto. congruence. destruct dst; auto. simpl; econstructor; eauto. (* sizeof *) + rewrite <- comp_env_preserved. destruct dst. split; auto. split; auto. constructor. auto. exists (Esizeof ty1 ty). split. auto. split. auto. constructor. (* alignof *) + rewrite <- comp_env_preserved. destruct dst. split; auto. split; auto. constructor. auto. @@ -267,9 +276,11 @@ Opaque makeif. exploit H0; eauto. intros [A [B C]]. subst sl1. split; auto. split; auto. constructor; auto. (* field struct *) + rewrite <- comp_env_preserved in *. exploit H0; eauto. intros [A [B C]]. subst sl1. split; auto. split; auto. rewrite B in H1. eapply eval_Efield_struct; eauto. (* field union *) + rewrite <- comp_env_preserved in *. exploit H0; eauto. intros [A [B C]]. subst sl1. split; auto. split; auto. rewrite B in H1. eapply eval_Efield_union; eauto. Qed. @@ -1659,7 +1670,7 @@ Proof. left. eapply star_plus_trans. rewrite app_ass. rewrite Kseqlist_app. eexact EXEC. eapply plus_two. simpl. econstructor. eapply step_make_assign; eauto. econstructor. eexact EV3. eexact EV2. - rewrite TY3; rewrite <- TY1; rewrite <- TY2; eauto. + rewrite TY3; rewrite <- TY1; rewrite <- TY2; rewrite comp_env_preserved; auto. reflexivity. traceEq. econstructor. auto. change sl2 with (nil ++ sl2). apply S. constructor. auto. auto. auto. @@ -1680,7 +1691,7 @@ Proof. eapply star_plus_trans. eexact EXEC. simpl. eapply plus_four. econstructor. econstructor. econstructor. eexact EV3. eexact EV2. - rewrite TY3; rewrite <- TY1; rewrite <- TY2. eauto. + rewrite TY3; rewrite <- TY1; rewrite <- TY2; rewrite comp_env_preserved; eauto. econstructor. eapply step_make_assign; eauto. constructor. apply PTree.gss. reflexivity. traceEq. @@ -1729,8 +1740,8 @@ Proof. eapply plus_two. simpl. constructor. eapply step_make_assign; eauto. unfold transl_incrdecr. destruct id; simpl in H2. - econstructor. eauto. constructor. simpl. rewrite TY3; rewrite <- TY1. eauto. - econstructor. eauto. constructor. simpl. rewrite TY3; rewrite <- TY1. eauto. + econstructor. eauto. constructor. rewrite TY3; rewrite <- TY1; rewrite comp_env_preserved. simpl; eauto. + econstructor. eauto. constructor. rewrite TY3; rewrite <- TY1; rewrite comp_env_preserved. simpl; eauto. destruct id; auto. reflexivity. traceEq. econstructor. auto. change sl2 with (nil ++ sl2). apply S. @@ -1748,8 +1759,10 @@ Proof. constructor. eapply step_make_assign; eauto. unfold transl_incrdecr. destruct id; simpl in H2. - econstructor. constructor. apply PTree.gss. constructor. simpl. eauto. - econstructor. constructor. apply PTree.gss. constructor. simpl. eauto. + econstructor. constructor. apply PTree.gss. constructor. + rewrite comp_env_preserved; simpl; eauto. + econstructor. constructor. apply PTree.gss. constructor. + rewrite comp_env_preserved; simpl; eauto. destruct id; auto. traceEq. econstructor. auto. apply S. @@ -1900,24 +1913,31 @@ Qed. Lemma alloc_variables_preserved: forall e m params e' m', - Csem.alloc_variables e m params e' m' -> - alloc_variables e m params e' m'. + Csem.alloc_variables ge e m params e' m' -> + alloc_variables tge e m params e' m'. Proof. - induction 1; econstructor; eauto. + induction 1; econstructor; eauto. rewrite comp_env_preserved; auto. Qed. Lemma bind_parameters_preserved: forall e m params args m', Csem.bind_parameters ge e m params args m' -> - bind_parameters e m params args m'. + bind_parameters tge e m params args m'. Proof. - induction 1; econstructor; eauto. - inv H0. - eapply assign_loc_value; eauto. - inv H4. eapply assign_loc_value; eauto. - eapply assign_loc_copy; eauto. + induction 1; econstructor; eauto. inv H0. +- eapply assign_loc_value; eauto. +- inv H4. eapply assign_loc_value; eauto. +- rewrite <- comp_env_preserved in *. eapply assign_loc_copy; eauto. Qed. +Lemma blocks_of_env_preserved: + forall e, blocks_of_env tge e = Csem.blocks_of_env ge e. +Proof. + intros; unfold blocks_of_env, Csem.blocks_of_env. + unfold block_of_binding, Csem.block_of_binding. + rewrite comp_env_preserved. auto. +Qed. + Lemma sstep_simulation: forall S1 t S2, Csem.sstep ge S1 t S2 -> forall S1' (MS: match_states S1 S1'), @@ -2090,9 +2110,10 @@ Proof. left. apply plus_one. constructor. econstructor; eauto. constructor; auto. + (* return none *) inv H7. econstructor; split. - left. apply plus_one. econstructor; eauto. + left. apply plus_one. econstructor; eauto. rewrite blocks_of_env_preserved; eauto. constructor. apply match_cont_call; auto. (* return some 1 *) inv H6. inv H0. econstructor; split. @@ -2102,14 +2123,14 @@ Proof. inv H9. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. econstructor; split. left. eapply plus_two. constructor. econstructor. eauto. - erewrite function_return_preserved; eauto. + erewrite function_return_preserved; eauto. rewrite blocks_of_env_preserved; eauto. eauto. traceEq. constructor. apply match_cont_call; auto. (* skip return *) inv H8. assert (is_call_cont tk). inv H9; simpl in *; auto. econstructor; split. - left. apply plus_one. apply step_skip_call; eauto. + left. apply plus_one. apply step_skip_call; eauto. rewrite blocks_of_env_preserved; eauto. constructor. auto. (* switch *) @@ -2198,14 +2219,14 @@ Lemma transl_initial_states: Csem.initial_state prog S -> exists S', Clight.initial_state tprog S' /\ match_states S S'. Proof. - intros. inv H. + intros. inv H. generalize TRANSL; intros TR; monadInv TR. rewrite H4. exploit transl_program_spec; eauto. intros MP. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. econstructor; split. econstructor. - exploit Genv.init_mem_match; eauto. - simpl. fold tge. rewrite symbols_preserved. - destruct MP as (A & B & C). rewrite B; eexact H1. + exploit Genv.init_mem_match; eauto. + change (Genv.globalenv tprog) with (genv_genv tge). rewrite symbols_preserved. + rewrite <- H4; simpl; eauto. eexact FIND. rewrite <- H3. apply type_of_fundef_preserved. auto. constructor. auto. constructor. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 83ddd1f4..9f9fb450 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -1144,10 +1144,10 @@ Qed. Theorem transl_program_spec: forall p tp, transl_program p = OK tp -> - match_program tr_fundef (fun v1 v2 => v1 = v2) nil p.(prog_main) p tp. + match_program tr_fundef (fun v1 v2 => v1 = v2) nil (Csyntax.prog_main p) p tp. Proof. unfold transl_program; intros. - destruct (transl_globdefs (prog_defs p) (initial_generator tt)) eqn:E; simpl in H; inv H. + destruct (transl_globdefs (Csyntax.prog_defs p) (initial_generator tt)) eqn:E; simpl in H; inv H. split; auto. exists l; split. eapply transl_globdefs_spec; eauto. rewrite <- app_nil_end; auto. Qed. diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index 9c529280..52ee8377 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -48,8 +48,8 @@ Definition make_cast (a: expr) (tto: type) : expr := | cast_case_f2f => a | cast_case_s2s => a | cast_case_l2l => a - | cast_case_struct _ _ _ _ => a - | cast_case_union _ _ _ _ => a + | cast_case_struct _ _ => a + | cast_case_union _ _ => a | cast_case_void => a | _ => Ecast a tto end. @@ -70,6 +70,8 @@ Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr := | Ebinop op a1 a2 ty => Ebinop op (simpl_expr cenv a1) (simpl_expr cenv a2) ty | Ecast a1 ty => Ecast (simpl_expr cenv a1) ty | Efield a1 fld ty => Efield (simpl_expr cenv a1) fld ty + | Esizeof _ _ => a + | Ealignof _ _ => a end. Definition simpl_exprlist (cenv: compilenv) (al: list expr) : list expr := @@ -170,6 +172,8 @@ Fixpoint addr_taken_expr (a: expr): VSet.t := | Ebinop op a1 a2 ty => VSet.union (addr_taken_expr a1) (addr_taken_expr a2) | Ecast a1 ty => addr_taken_expr a1 | Efield a1 fld ty => addr_taken_expr a1 + | Esizeof _ _ => VSet.empty + | Ealignof _ _ => VSet.empty end. Fixpoint addr_taken_exprlist (l: list expr) : VSet.t := @@ -247,6 +251,10 @@ Definition transf_fundef (fd: fundef) : res fundef := end. Definition transf_program (p: program) : res program := - AST.transform_partial_program transf_fundef p. - - + do p1 <- AST.transform_partial_program transf_fundef p; + OK {| prog_defs := AST.prog_defs p1; + prog_public := AST.prog_public p1; + prog_main := AST.prog_main p1; + prog_types := prog_types p; + prog_comp_env := prog_comp_env p; + prog_comp_env_eq := prog_comp_env_eq p |}. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 15d0af06..5cf59d94 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -39,25 +39,37 @@ Section PRESERVATION. Variable prog: program. Variable tprog: program. Hypothesis TRANSF: transf_program prog = OK tprog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. +Let ge := globalenv prog. +Let tge := globalenv tprog. + +Lemma comp_env_preserved: + genv_cenv tge = genv_cenv ge. +Proof. + monadInv TRANSF. unfold tge; rewrite <- H0; auto. +Qed. + +Lemma transf_programs: + AST.transform_partial_program transf_fundef (program_of_program prog) = OK (program_of_program tprog). +Proof. + monadInv TRANSF. rewrite EQ. destruct x; reflexivity. +Qed. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. - exact (Genv.find_symbol_transf_partial _ _ TRANSF). + exact (Genv.find_symbol_transf_partial _ _ transf_programs). Qed. Lemma public_preserved: forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. Proof. - exact (Genv.public_symbol_transf_partial _ _ TRANSF). + exact (Genv.public_symbol_transf_partial _ _ transf_programs). Qed. Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. - exact (Genv.find_var_info_transf_partial _ _ TRANSF). + exact (Genv.find_var_info_transf_partial _ _ transf_programs). Qed. Lemma functions_translated: @@ -65,7 +77,7 @@ Lemma functions_translated: Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. Proof. - exact (Genv.find_funct_transf_partial _ _ TRANSF). + exact (Genv.find_funct_transf_partial _ _ transf_programs). Qed. Lemma function_ptr_translated: @@ -73,7 +85,7 @@ Lemma function_ptr_translated: Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. Proof. - exact (Genv.find_funct_ptr_transf_partial _ _ TRANSF). + exact (Genv.find_funct_ptr_transf_partial _ _ transf_programs). Qed. Lemma type_of_fundef_preserved: @@ -207,14 +219,10 @@ Inductive val_casted: val -> type -> Prop := 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_ptr_cptr: forall b ofs id attr, - val_casted (Vptr b ofs) (Tcomp_ptr id attr) - | val_casted_int_cptr: forall n id attr, - val_casted (Vint n) (Tcomp_ptr id attr) - | val_casted_struct: forall id fld attr b ofs, - val_casted (Vptr b ofs) (Tstruct id fld attr) - | val_casted_union: forall id fld attr b ofs, - val_casted (Vptr b ofs) (Tunion id fld 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. @@ -254,8 +262,6 @@ Proof. 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. @@ -266,8 +272,6 @@ Proof. constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. constructor; auto. - constructor. simpl. destruct (Int.eq i0 Int.zero); auto. - constructor; auto. (* long *) destruct ty; try (destruct f); try discriminate. destruct v; inv H. constructor. @@ -277,7 +281,6 @@ Proof. destruct v; 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 *) @@ -287,12 +290,10 @@ Proof. discriminate. (* structs *) destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i && fieldlist_eq f0 f); inv H; constructor. + destruct (ident_eq i0 i); inv H; constructor. (* unions *) destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i && fieldlist_eq f0 f); inv H; constructor. -(* comp_ptr *) - destruct ty; simpl in H; try discriminate; destruct v; inv H; constructor. + destruct (ident_eq i0 i); inv H; constructor. Qed. Lemma val_casted_load_result: @@ -316,8 +317,6 @@ Proof. discriminate. discriminate. discriminate. - discriminate. - discriminate. Qed. Lemma cast_val_casted: @@ -374,9 +373,9 @@ Proof. destruct v1; inv H0; auto. destruct v1; inv H0; auto. destruct v1; try discriminate. - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto. + destruct (ident_eq id1 id2); inv H0; auto. destruct v1; try discriminate. - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto. + destruct (ident_eq id1 id2); inv H0; auto. inv H0; auto. Qed. @@ -388,7 +387,7 @@ Lemma match_envs_assign_lifted: e!id = Some(b, ty) -> val_casted v ty -> val_inject f v tv -> - assign_loc ty m b Int.zero v m' -> + assign_loc ge ty m b Int.zero v m' -> VSet.mem id cenv = true -> match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi. Proof. @@ -582,8 +581,8 @@ Hint Resolve compat_cenv_union_l compat_cenv_union_r compat_cenv_empty: compat. (** Allocation and initialization of parameters *) Lemma alloc_variables_nextblock: - forall e m vars e' m', - alloc_variables e m vars e' m' -> Ple (Mem.nextblock m) (Mem.nextblock m'). + forall ge e m vars e' m', + alloc_variables ge e m vars e' m' -> Ple (Mem.nextblock m) (Mem.nextblock m'). Proof. induction 1. apply Ple_refl. @@ -591,8 +590,8 @@ Proof. Qed. Lemma alloc_variables_range: - forall id b ty e m vars e' m', - alloc_variables e m vars e' m' -> + forall ge id b ty e m vars e' m', + alloc_variables ge e m vars e' m' -> e'!id = Some(b, ty) -> e!id = Some(b, ty) \/ Ple (Mem.nextblock m) b /\ Plt b (Mem.nextblock m'). Proof. induction 1; intros. @@ -600,15 +599,15 @@ Proof. exploit IHalloc_variables; eauto. rewrite PTree.gsspec. intros [A|A]. destruct (peq id id0). inv A. right. exploit Mem.alloc_result; eauto. exploit Mem.nextblock_alloc; eauto. - generalize (alloc_variables_nextblock _ _ _ _ _ H0). intros A B C. + generalize (alloc_variables_nextblock _ _ _ _ _ _ H0). intros A B C. subst b. split. apply Ple_refl. eapply Plt_le_trans; eauto. rewrite B. apply Plt_succ. auto. right. exploit Mem.nextblock_alloc; eauto. intros B. rewrite B in A. xomega. Qed. Lemma alloc_variables_injective: - forall id1 b1 ty1 id2 b2 ty2 e m vars e' m', - alloc_variables e m vars e' m' -> + forall ge id1 b1 ty1 id2 b2 ty2 e m vars e' m', + alloc_variables ge e m vars e' m' -> (e!id1 = Some(b1, ty1) -> e!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2) -> (forall id b ty, e!id = Some(b, ty) -> Plt b (Mem.nextblock m)) -> (e'!id1 = Some(b1, ty1) -> e'!id2 = Some(b2, ty2) -> id1 <> id2 -> b1 <> b2). @@ -629,12 +628,12 @@ Qed. Lemma match_alloc_variables: forall cenv e m vars e' m', - alloc_variables e m vars e' m' -> + alloc_variables ge e m vars e' m' -> forall j tm te, list_norepet (var_names vars) -> Mem.inject j m tm -> exists j', exists te', exists tm', - alloc_variables te tm (remove_lifted cenv vars) te' tm' + alloc_variables tge te tm (remove_lifted cenv vars) te' tm' /\ Mem.inject j' m' tm' /\ inject_incr j j' /\ (forall b, Mem.valid_block m b -> j' b = j b) @@ -698,7 +697,7 @@ Proof. exploit IHalloc_variables; eauto. instantiate (1 := PTree.set id (tb1, ty) te). intros [j' [te' [tm' [J [K [L [M [N [Q [O P]]]]]]]]]]. exists j'; exists te'; exists tm'. - split. simpl. econstructor; eauto. + split. simpl. econstructor; eauto. rewrite comp_env_preserved; auto. split. auto. split. eapply inject_incr_trans; eauto. split. intros. transitivity (j1 b). apply M. eapply Mem.valid_block_alloc; eauto. @@ -737,7 +736,7 @@ Qed. Lemma alloc_variables_load: forall e m vars e' m', - alloc_variables e m vars e' m' -> + alloc_variables ge e m vars e' m' -> forall chunk b ofs v, Mem.load chunk m b ofs = Some v -> Mem.load chunk m' b ofs = Some v. @@ -749,10 +748,10 @@ Qed. Lemma sizeof_by_value: forall ty chunk, - access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ty. + access_mode ty = By_value chunk -> size_chunk chunk <= sizeof ge ty. Proof. unfold access_mode; intros. - assert (size_chunk chunk = sizeof ty). + assert (size_chunk chunk = sizeof ge ty). { destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto. } @@ -765,7 +764,7 @@ Definition env_initial_value (e: env) (m: mem) := Lemma alloc_variables_initial_value: forall e m vars e' m', - alloc_variables e m vars e' m' -> + alloc_variables ge e m vars e' m' -> env_initial_value e m -> env_initial_value e' m'. Proof. @@ -900,14 +899,14 @@ Qed. Theorem match_envs_alloc_variables: forall cenv m vars e m' temps j tm, - alloc_variables empty_env m vars e m' -> + alloc_variables ge empty_env m vars e m' -> list_norepet (var_names vars) -> Mem.inject j m tm -> (forall id ty, In (id, ty) vars -> VSet.mem id cenv = true -> exists chunk, access_mode ty = By_value chunk) -> (forall id, VSet.mem id cenv = true -> In id (var_names vars)) -> exists j', exists te, exists tm', - alloc_variables empty_env tm (remove_lifted cenv vars) te tm' + alloc_variables tge empty_env tm (remove_lifted cenv vars) te tm' /\ match_envs j' cenv e (create_undef_temps temps) m' (Mem.nextblock m) (Mem.nextblock m') te (create_undef_temps (add_lifted cenv vars temps)) (Mem.nextblock tm) (Mem.nextblock tm') /\ Mem.inject j' m' tm' @@ -996,12 +995,12 @@ Qed. Lemma assign_loc_inject: forall f ty m loc ofs v m' tm loc' ofs' v', - assign_loc ty m loc ofs v m' -> + assign_loc ge ty m loc ofs v m' -> val_inject f (Vptr loc ofs) (Vptr loc' ofs') -> val_inject f v v' -> Mem.inject f m tm -> exists tm', - assign_loc ty tm loc' ofs' v' tm' + assign_loc tge ty tm loc' ofs' v' tm' /\ Mem.inject f m' tm' /\ (forall b chunk v, f b = None -> Mem.load chunk m b 0 = Some v -> Mem.load chunk m' b 0 = Some v). @@ -1018,10 +1017,11 @@ Proof. rename b' into bsrc. rename ofs'0 into osrc. rename loc into bdst. rename ofs into odst. rename loc' into bdst'. rename b2 into bsrc'. - destruct (zeq (sizeof ty) 0). + rewrite <- comp_env_preserved in *. + destruct (zeq (sizeof tge ty) 0). + (* special case size = 0 *) assert (bytes = nil). - { exploit (Mem.loadbytes_empty m bsrc (Int.unsigned osrc) (sizeof ty)). + { exploit (Mem.loadbytes_empty m bsrc (Int.unsigned osrc) (sizeof tge ty)). omega. congruence. } subst. destruct (Mem.range_perm_storebytes tm bdst' (Int.unsigned (Int.add odst (Int.repr delta))) nil) @@ -1038,12 +1038,12 @@ Proof. left. congruence. + (* general case size > 0 *) exploit Mem.loadbytes_length; eauto. intros LEN. - assert (SZPOS: sizeof ty > 0). - { generalize (sizeof_pos ty); omega. } - assert (RPSRC: Mem.range_perm m bsrc (Int.unsigned osrc) (Int.unsigned osrc + sizeof ty) Cur Nonempty). + assert (SZPOS: sizeof tge ty > 0). + { generalize (sizeof_pos tge ty); omega. } + assert (RPSRC: Mem.range_perm m bsrc (Int.unsigned osrc) (Int.unsigned osrc + sizeof tge ty) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. - assert (RPDST: Mem.range_perm m bdst (Int.unsigned odst) (Int.unsigned odst + sizeof ty) Cur Nonempty). - replace (sizeof ty) with (Z_of_nat (length bytes)). + assert (RPDST: Mem.range_perm m bdst (Int.unsigned odst) (Int.unsigned odst + sizeof tge ty) Cur Nonempty). + replace (sizeof tge ty) with (Z_of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. rewrite LEN. apply nat_of_Z_eq. omega. assert (PSRC: Mem.perm m bsrc (Int.unsigned osrc) Cur Nonempty). @@ -1084,8 +1084,8 @@ Proof. Qed. Lemma assign_loc_nextblock: - forall ty m b ofs v m', - assign_loc ty m b ofs v m' -> Mem.nextblock m' = Mem.nextblock m. + forall ge ty m b ofs v m', + assign_loc ge ty m b ofs v m' -> Mem.nextblock m' = Mem.nextblock m. Proof. induction 1. simpl in H0. eapply Mem.nextblock_store; eauto. @@ -1094,7 +1094,7 @@ Qed. Theorem store_params_correct: forall j f k cenv le lo hi te tlo thi e m params args m', - bind_parameters e m params args m' -> + bind_parameters ge e m params args m' -> forall s tm tle1 tle2 targs, list_norepet (var_names params) -> list_forall2 val_casted args (map snd params) -> @@ -1105,7 +1105,7 @@ Theorem store_params_correct: (forall id, In id (var_names params) -> le!id = None) -> exists tle, exists tm', star step2 tge (State f (store_params cenv params s) k te tle tm) - E0 (State f s k te tle tm') + E0 (State f s k te tle tm') /\ bind_parameter_temps params targs tle2 = Some tle /\ Mem.inject j m' tm' /\ match_envs j cenv e le m' lo hi te tle tlo thi @@ -1157,12 +1157,12 @@ Proof. reflexivity. reflexivity. eexact U. traceEq. - rewrite (assign_loc_nextblock _ _ _ _ _ _ A) in Z. auto. + rewrite (assign_loc_nextblock _ _ _ _ _ _ _ A) in Z. auto. Qed. Lemma bind_parameters_nextblock: - forall e m params args m', - bind_parameters e m params args m' -> Mem.nextblock m' = Mem.nextblock m. + forall ge e m params args m', + bind_parameters ge e m params args m' -> Mem.nextblock m' = Mem.nextblock m. Proof. induction 1. auto. @@ -1170,10 +1170,10 @@ Proof. Qed. Lemma bind_parameters_load: - forall e chunk b ofs, + forall ge e chunk b ofs, (forall id b' ty, e!id = Some(b', ty) -> b <> b') -> forall m params args m', - bind_parameters e m params args m' -> + bind_parameters ge e m params args m' -> Mem.load chunk m' b ofs = Mem.load chunk m b ofs. Proof. induction 2. @@ -1188,16 +1188,16 @@ Qed. (** Freeing of local variables *) Lemma free_blocks_of_env_perm_1: - forall m e m' id b ty ofs k p, - Mem.free_list m (blocks_of_env e) = Some m' -> + forall ce m e m' id b ty ofs k p, + Mem.free_list m (blocks_of_env ce e) = Some m' -> e!id = Some(b, ty) -> Mem.perm m' b ofs k p -> - 0 <= ofs < sizeof ty -> + 0 <= ofs < sizeof ce ty -> False. Proof. intros. exploit Mem.perm_free_list; eauto. intros [A B]. - apply B with 0 (sizeof ty); auto. - unfold blocks_of_env. change (b, 0, sizeof ty) with (block_of_binding (id, (b, ty))). + apply B with 0 (sizeof ce ty); auto. + unfold blocks_of_env. change (b, 0, sizeof ce ty) with (block_of_binding ce (id, (b, ty))). apply in_map. apply PTree.elements_correct. auto. Qed. @@ -1216,13 +1216,13 @@ Proof. Qed. Lemma free_blocks_of_env_perm_2: - forall m e m' id b ty, - Mem.free_list m (blocks_of_env e) = Some m' -> + forall ce m e m' id b ty, + Mem.free_list m (blocks_of_env ce e) = Some m' -> e!id = Some(b, ty) -> - Mem.range_perm m b 0 (sizeof ty) Cur Freeable. + Mem.range_perm m b 0 (sizeof ce ty) Cur Freeable. Proof. intros. eapply free_list_perm'; eauto. - unfold blocks_of_env. change (b, 0, sizeof ty) with (block_of_binding (id, (b, ty))). + unfold blocks_of_env. change (b, 0, sizeof ce ty) with (block_of_binding ce (id, (b, ty))). apply in_map. apply PTree.elements_correct. auto. Qed. @@ -1252,15 +1252,15 @@ Proof. Qed. Lemma blocks_of_env_no_overlap: - forall j cenv e le m lo hi te tle tlo thi tm, + forall (ge: genv) j cenv e le m lo hi te tle tlo thi tm, match_envs j cenv e le m lo hi te tle tlo thi -> Mem.inject j m tm -> (forall id b ty, - e!id = Some(b, ty) -> Mem.range_perm m b 0 (sizeof ty) Cur Freeable) -> + e!id = Some(b, ty) -> Mem.range_perm m b 0 (sizeof ge ty) Cur Freeable) -> forall l, list_norepet (List.map fst l) -> (forall id bty, In (id, bty) l -> te!id = Some bty) -> - freelist_no_overlap (List.map block_of_binding l). + freelist_no_overlap (List.map (block_of_binding ge) l). Proof. intros until tm; intros ME MINJ PERMS. induction l; simpl; intros. - auto. @@ -1272,8 +1272,8 @@ Proof. assert (TE': te!id' = Some(b', ty')) by eauto. exploit me_mapped. eauto. eexact TE. intros [b0 [INJ E]]. exploit me_mapped. eauto. eexact TE'. intros [b0' [INJ' E']]. - destruct (zle (sizeof ty) 0); auto. - destruct (zle (sizeof ty') 0); auto. + destruct (zle (sizeof ge0 ty) 0); auto. + destruct (zle (sizeof ge0 ty') 0); auto. assert (b0 <> b0'). { eapply me_inj; eauto. red; intros; subst; elim H3. change id' with (fst (id', (b', ty'))). apply List.in_map; auto. } @@ -1302,26 +1302,34 @@ Proof. eapply Mem.free_right_inject; eauto. Qed. +Lemma blocks_of_env_translated: + forall e, blocks_of_env tge e = blocks_of_env ge e. +Proof. + intros. unfold blocks_of_env, block_of_binding. + rewrite comp_env_preserved; auto. +Qed. + Theorem match_envs_free_blocks: forall j cenv e le m lo hi te tle tlo thi m' tm, match_envs j cenv e le m lo hi te tle tlo thi -> Mem.inject j m tm -> - Mem.free_list m (blocks_of_env e) = Some m' -> + Mem.free_list m (blocks_of_env ge e) = Some m' -> exists tm', - Mem.free_list tm (blocks_of_env te) = Some tm' + Mem.free_list tm (blocks_of_env tge te) = Some tm' /\ Mem.inject j m' tm'. Proof. intros. - assert (X: exists tm', Mem.free_list tm (blocks_of_env te) = Some tm'). +Local Opaque ge tge. + assert (X: exists tm', Mem.free_list tm (blocks_of_env tge te) = Some tm'). { - apply can_free_list. + rewrite blocks_of_env_translated. apply can_free_list. - (* permissions *) intros. unfold blocks_of_env in H2. exploit list_in_map_inv; eauto. intros [[id [b' ty]] [EQ IN]]. - simpl in EQ; inv EQ. + unfold block_of_binding in EQ; inv EQ. exploit me_mapped; eauto. eapply PTree.elements_complete; eauto. intros [b [A B]]. - change 0 with (0 + 0). replace (sizeof ty) with (sizeof ty + 0) by omega. + change 0 with (0 + 0). replace (sizeof ge ty) with (sizeof ge ty + 0) by omega. eapply Mem.range_perm_inject; eauto. eapply free_blocks_of_env_perm_2; eauto. - (* no overlap *) @@ -1335,10 +1343,10 @@ Proof. eapply free_list_right_inject; eauto. eapply Mem.free_list_left_inject; eauto. intros. unfold blocks_of_env in H3. exploit list_in_map_inv; eauto. - intros [[id [b' ty]] [EQ IN]]. simpl in EQ. inv EQ. + intros [[id [b' ty]] [EQ IN]]. unfold block_of_binding in EQ. inv EQ. exploit me_flat; eauto. apply PTree.elements_complete; eauto. intros [P Q]. subst delta. eapply free_blocks_of_env_perm_1 with (m := m); eauto. - omega. + rewrite <- comp_env_preserved. omega. Qed. (** Matching global environments *) @@ -1434,11 +1442,16 @@ Proof. exploit eval_simpl_expr. eexact H. eauto with compat. intros [tv1 [A B]]. exploit eval_simpl_expr. eexact H0. eauto with compat. intros [tv2 [C D]]. exploit sem_binary_operation_inject; eauto. intros [tv [E F]]. - exists tv; split; auto. econstructor; eauto. repeat rewrite typeof_simpl_expr; auto. + exists tv; split; auto. econstructor; eauto. + repeat rewrite typeof_simpl_expr; rewrite comp_env_preserved; auto. (* cast *) exploit eval_simpl_expr; eauto. intros [tv1 [A B]]. exploit sem_cast_inject; eauto. intros [tv2 [C D]]. - exists tv2; split; auto. econstructor. eauto. rewrite typeof_simpl_expr; auto. + exists tv2; split; auto. econstructor. eauto. rewrite typeof_simpl_expr; auto. +(* sizeof *) + econstructor; split. constructor. rewrite comp_env_preserved; auto. +(* alignof *) + econstructor; split. constructor. rewrite comp_env_preserved; auto. (* rval *) assert (EITHER: (exists id, exists ty, a = Evar id ty /\ VSet.mem id cenv = true) \/ (match a with Evar id _ => VSet.mem id cenv = false | _ => True end)). @@ -1481,12 +1494,14 @@ Proof. inversion B. subst. econstructor; econstructor; split; eauto. econstructor; eauto. (* field struct *) + rewrite <- comp_env_preserved in *. exploit eval_simpl_expr; eauto. intros [tv [A B]]. inversion B. subst. econstructor; econstructor; split. eapply eval_Efield_struct; eauto. rewrite typeof_simpl_expr; eauto. econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. (* field union *) + rewrite <- comp_env_preserved in *. exploit eval_simpl_expr; eauto. intros [tv [A B]]. inversion B. subst. econstructor; econstructor; split. @@ -1583,7 +1598,7 @@ Qed. Lemma match_cont_assign_loc: forall f cenv k tk m bound tbound ty loc ofs v m', match_cont f cenv k tk m bound tbound -> - assign_loc ty m loc ofs v m' -> + assign_loc ge ty m loc ofs v m' -> Ple bound loc -> match_cont f cenv k tk m' bound tbound. Proof. @@ -1687,8 +1702,8 @@ Lemma match_cont_free_env: match_cont f cenv k tk m lo tlo -> Ple hi (Mem.nextblock m) -> Ple thi (Mem.nextblock tm) -> - Mem.free_list m (blocks_of_env e) = Some m' -> - Mem.free_list tm (blocks_of_env te) = Some tm' -> + Mem.free_list m (blocks_of_env ge e) = Some m' -> + Mem.free_list tm (blocks_of_env tge te) = Some tm' -> match_cont f cenv k tk m' (Mem.nextblock m') (Mem.nextblock tm'). Proof. intros. apply match_cont_incr_bounds with lo tlo. @@ -2183,7 +2198,7 @@ Proof. red; intros; subst b'. xomega. eapply alloc_variables_load; eauto. apply compat_cenv_for. - rewrite (bind_parameters_nextblock _ _ _ _ _ H2). xomega. + rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). xomega. rewrite T; xomega. (* external function *) @@ -2216,8 +2231,9 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [A B]]. econstructor; split. econstructor. - eapply Genv.init_mem_transf_partial; eauto. - rewrite (transform_partial_program_main _ _ TRANSF). + eapply Genv.init_mem_transf_partial. eexact transf_programs. eauto. + change (prog_main tprog) with (AST.prog_main tprog). + rewrite (transform_partial_program_main _ _ transf_programs). instantiate (1 := b). rewrite <- H1. apply symbols_preserved. eauto. rewrite <- H3; apply type_of_fundef_preserved; auto. -- cgit