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/Initializers.v | 115 ++++++++++++++++++++++++++--------------------- 1 file changed, 65 insertions(+), 50 deletions(-) (limited to 'cfrontend/Initializers.v') 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") -- cgit