From 2f643e4419e8237c63d6823720da8100da9c8b11 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Apr 2014 09:18:51 +0000 Subject: Clean-up pass on C types: - Ctypes: add useful functions on attributes; remove attrs in typeconv (because attributes are meaningless on r-values) - C2C: fixed missing or redundant Evalof - Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values); add sanity check between typeconv/classify_binarith and the C99 standard. - cparser: fixed several cases where incorrect type annotations were put on expressions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2457 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/C2C.ml | 39 +++--- cfrontend/Cop.v | 319 +++++++++++++++++++++++++++++++++++++++--------- cfrontend/Cshmgen.v | 12 +- cfrontend/Ctypes.v | 45 ++++++- cparser/Bitfields.ml | 51 ++++---- cparser/Cutil.ml | 20 ++- cparser/Cutil.mli | 2 + cparser/Elab.ml | 26 ++-- extraction/extraction.v | 2 + 9 files changed, 381 insertions(+), 135 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index f767372..8799bc0 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -200,9 +200,10 @@ a constant)"; Integers.Int.one in (** ** Translation of [va_arg] for variadic functions. *) let va_list_ptr e = - if CBuiltins.va_list_scalar - then Eaddrof(e, Tpointer(typeof e, noattr)) - else e + if not CBuiltins.va_list_scalar then e else + match e with + | Evalof(e', _) -> Eaddrof(e', Tpointer(typeof e, noattr)) + | _ -> error "bad use of a va_list object"; e let make_builtin_va_arg env ty e = let (helper, ty_ret) = @@ -215,15 +216,14 @@ let make_builtin_va_arg env ty e = ("__compcert_va_float64", Tfloat(F64, noattr)) | _ -> unsupported "va_arg at this type"; - ("", Tvoid) - in - Ecast - (Ecall(Evar (intern_string helper, - Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, - cc_default)), - Econs(va_list_ptr e, Enil), - ty_ret), - ty) + ("", Tvoid) in + let ty_fun = + Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in + Ecast + (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), + Econs(va_list_ptr e, Enil), + ty_ret), + ty) (** ** Translation functions *) @@ -338,7 +338,7 @@ let convertTyp env t = | C.TStruct(id, a) -> let a' = convertAttr a in begin try - mergeTypAttr (Hashtbl.find compositeCache id) a' + merge_attributes (Hashtbl.find compositeCache id) a' with Not_found -> let flds = try @@ -350,7 +350,7 @@ let convertTyp env t = | C.TUnion(id, a) -> let a' = convertAttr a in begin try - mergeTypAttr (Hashtbl.find compositeCache id) a' + merge_attributes (Hashtbl.find compositeCache id) a' with Not_found -> let flds = try @@ -379,12 +379,6 @@ let convertTyp env t = in convertTyp [] t -(* -let rec convertTypList env = function - | [] -> Tnil - | t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl) -*) - let rec convertTypArgs env tl el = match tl, el with | _, [] -> Tnil @@ -1062,10 +1056,11 @@ let convertProgram p = 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_main = intern_string "main" } in if !numErrors > 0 then None - else Some { AST.prog_defs = gl2; - AST.prog_main = intern_string "main" } + else Some p' with Env.Error msg -> error (Env.error_message msg); None diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index f2550ef..83fe772 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -115,7 +115,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases := end. (** Semantics of casts. [sem_cast v1 t1 t2 = Some v2] if value [v1], - viewed with static type [t1], can be cast to type [t2], + viewed with static type [t1], can be converted to type [t2], resulting in value [v2]. *) Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int := @@ -266,7 +266,8 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := (** The following describes types that can be interpreted as a boolean: integers, floats, pointers. It is used for the semantics of - the [!] and [?] operators, as well as the [if], [while], [for] statements. *) + the [!] and [?] operators, as well as the [if], [while], + and [for] statements. *) Inductive classify_bool_cases : Type := | bool_case_i (**r integer *) @@ -315,34 +316,6 @@ Definition bool_val (v: val) (t: type) : option bool := | bool_default => None end. -(** Common-sense relation between Boolean value and casting to [_Bool] type. *) - -Lemma cast_bool_bool_val: - forall v t, - sem_cast v t (Tint IBool Signed noattr) = - match bool_val v t with None => None | Some b => Some(Val.of_bool b) end. -Proof. - intros. - assert (A: classify_bool t = - match t with - | Tint _ _ _ => bool_case_i - | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p - | Tfloat _ _ => bool_case_f - | Tlong _ _ => bool_case_l - | _ => bool_default - end). - { - unfold classify_bool; destruct t; simpl; auto. destruct i; auto. - } - unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto. - destruct (Int.eq i0 Int.zero); auto. - destruct (Int64.eq i Int64.zero); auto. - destruct (Float.cmp Ceq f0 Float.zero); auto. - 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. (** ** Unary operators *) @@ -374,17 +347,6 @@ Definition sem_notbool (v: val) (ty: type) : option val := | bool_default => None end. -(** Common-sense relation between Boolean value and Boolean negation. *) - -Lemma notbool_bool_val: - forall v t, - sem_notbool v t = - match bool_val v t with None => None | Some b => Some(Val.of_bool (negb b)) end. -Proof. - intros. unfold sem_notbool, bool_val. - destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto. -Qed. - (** *** Opposite and absolute value *) Inductive classify_neg_cases : Type := @@ -503,6 +465,16 @@ Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases := | _, _ => bin_default end. +(** The static type of the result. *) + +Definition binarith_result_type (c: binarith_cases) : option type := + match c with + | bin_case_i sg => Some(Tint I32 sg noattr) + | bin_case_l sg => Some(Tlong sg noattr) + | bin_case_f sz => Some(Tfloat sz noattr) + | bin_default => None + end. + (** The type at which the computation is done. Both arguments are converted to this type before the actual computation. *) @@ -549,43 +521,43 @@ Definition sem_binarith (** *** Addition *) Inductive classify_add_cases : Type := - | add_case_pi(ty: type)(a: attr) (**r pointer, int *) - | add_case_ip(ty: type)(a: attr) (**r int, pointer *) - | add_case_pl(ty: type)(a: attr) (**r pointer, long *) - | add_case_lp(ty: type)(a: attr) (**r long, pointer *) + | add_case_pi(ty: type) (**r pointer, int *) + | add_case_ip(ty: type) (**r int, pointer *) + | add_case_pl(ty: type) (**r pointer, long *) + | add_case_lp(ty: type) (**r long, pointer *) | add_default. (**r numerical type, numerical type *) Definition classify_add (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tpointer ty a, Tint _ _ _ => add_case_pi ty a - | Tint _ _ _, Tpointer ty a => add_case_ip ty a - | Tpointer ty a, Tlong _ _ => add_case_pl ty a - | Tlong _ _, Tpointer ty a => add_case_lp ty a + | Tpointer ty _, Tint _ _ _ => add_case_pi ty + | Tint _ _ _, Tpointer ty _ => add_case_ip ty + | Tpointer ty _, Tlong _ _ => add_case_pl ty + | Tlong _ _, Tpointer ty _ => add_case_lp ty | _, _ => add_default end. Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := match classify_add t1 t2 with - | add_case_pi ty _ => (**r pointer plus integer *) + | 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))) | _, _ => None end - | add_case_ip ty _ => (**r integer plus pointer *) + | 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))) | _, _ => None end - | add_case_pl ty _ => (**r pointer plus long *) + | 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))) | _, _ => None end - | add_case_lp ty _ => (**r long plus pointer *) + | 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 @@ -603,28 +575,28 @@ Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := (** *** Subtraction *) Inductive classify_sub_cases : Type := - | sub_case_pi(ty: type)(a: attr) (**r pointer, int *) + | sub_case_pi(ty: type) (**r pointer, int *) | sub_case_pp(ty: type) (**r pointer, pointer *) - | sub_case_pl(ty: type)(a: attr) (**r pointer, long *) + | sub_case_pl(ty: type) (**r pointer, long *) | sub_default. (**r numerical type, numerical type *) Definition classify_sub (ty1: type) (ty2: type) := match typeconv ty1, typeconv ty2 with - | Tpointer ty a, Tint _ _ _ => sub_case_pi ty a + | Tpointer ty _, Tint _ _ _ => sub_case_pi ty | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty - | Tpointer ty a, Tlong _ _ => sub_case_pl ty a + | Tpointer ty _, Tlong _ _ => sub_case_pl ty | _, _ => sub_default end. Definition sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := match classify_sub t1 t2 with - | sub_case_pi ty attr => (**r pointer minus integer *) + | 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))) | _, _ => None end - | sub_case_pl ty attr => (**r pointer minus long *) + | 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 @@ -1177,5 +1149,234 @@ Proof. intros; eapply Mem.different_pointers_inject; eauto. Qed. +(** * Some properties of operator semantics *) + +(** This section collects some common-sense properties about the type + classification and semantic functions above. These properties are + not used in the CompCert semantics preservation proofs, but increase + confidence in the specification and its relation with the ISO C99 standard. *) + +(** Relation between Boolean value and casting to [_Bool] type. *) + +Lemma cast_bool_bool_val: + forall v t, + sem_cast v t (Tint IBool Signed noattr) = + match bool_val v t with None => None | Some b => Some(Val.of_bool b) end. +Proof. + intros. + assert (A: classify_bool t = + match t with + | Tint _ _ _ => bool_case_i + | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ _ => bool_case_p + | Tfloat _ _ => bool_case_f + | Tlong _ _ => bool_case_l + | _ => bool_default + end). + { + unfold classify_bool; destruct t; simpl; auto. destruct i; auto. + } + unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto. + destruct (Int.eq i0 Int.zero); auto. + destruct (Int64.eq i Int64.zero); auto. + destruct (Float.cmp Ceq f0 Float.zero); auto. + 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. *) +Lemma notbool_bool_val: + forall v t, + sem_notbool v t = + match bool_val v t with None => None | Some b => Some(Val.of_bool (negb b)) end. +Proof. + intros. unfold sem_notbool, bool_val. + destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto. +Qed. +(** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *) + +Module ArithConv. + +(** This is the ISO C algebra of arithmetic types, without qualifiers. + [S] stands for "signed" and [U] for "unsigned". *) + +Inductive int_type : Type := + | _Bool + | Char | SChar | UChar + | Short | UShort + | Int | UInt + | Long | ULong + | Longlong | ULonglong. + +Inductive arith_type : Type := + | I (it: int_type) + | Float + | Double + | Longdouble. + +Definition eq_int_type: forall (x y: int_type), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +Definition is_unsigned (t: int_type) : bool := + match t with + | _Bool => true + | Char => false (**r as in most of CompCert's target ABIs *) + | SChar => false + | UChar => true + | Short => false + | UShort => true + | Int => false + | UInt => true + | Long => false + | ULong => true + | Longlong => false + | ULonglong => true + end. + +Definition unsigned_type (t: int_type) : int_type := + match t with + | Char => UChar + | SChar => UChar + | Short => UShort + | Int => UInt + | Long => ULong + | Longlong => ULonglong + | _ => t + end. + +Definition int_sizeof (t: int_type) : Z := + match t with + | _Bool | Char | SChar | UChar => 1 + | Short | UShort => 2 + | Int | UInt | Long | ULong => 4 + | Longlong | ULonglong => 8 + end. + +(** 6.3.1.1 para 1: integer conversion rank *) + +Definition rank (t: int_type) : Z := + match t with + | _Bool => 1 + | Char | SChar | UChar => 2 + | Short | UShort => 3 + | Int | UInt => 4 + | Long | ULong => 5 + | Longlong | ULonglong => 6 + end. + +(** 6.3.1.1 para 2: integer promotions, a.k.a. usual unary conversions *) + +Definition integer_promotion (t: int_type) : int_type := + if zlt (rank t) (rank Int) then Int else t. + +(** 6.3.1.8: Usual arithmetic conversions, a.k.a. binary conversions. + This function returns the type to which the two operands must be + converted. *) + +Definition usual_arithmetic_conversion (t1 t2: arith_type) : arith_type := + match t1, t2 with + (* First, if the corresponding real type of either operand is long + double, the other operand is converted, without change of type domain, + to a type whose corresponding real type is long double. *) + | Longdouble, _ | _, Longdouble => Longdouble + (* Otherwise, if the corresponding real type of either operand is + double, the other operand is converted, without change of type domain, + to a type whose corresponding real type is double. *) + | Double, _ | _, Double => Double + (* Otherwise, if the corresponding real type of either operand is + float, the other operand is converted, without change of type domain, + to a type whose corresponding real type is float. *) + | Float, _ | _, Float => Float + (* Otherwise, the integer promotions are performed on both operands. *) + | I i1, I i2 => + let j1 := integer_promotion i1 in + let j2 := integer_promotion i2 in + (* Then the following rules are applied to the promoted operands: + If both operands have the same type, then no further conversion + is needed. *) + if eq_int_type j1 j2 then I j1 else + match is_unsigned j1, is_unsigned j2 with + (* Otherwise, if both operands have signed integer types or both + have unsigned integer types, the operand with the type of lesser + integer conversion rank is converted to the type of the operand with + greater rank. *) + | true, true | false, false => + if zlt (rank j1) (rank j2) then I j2 else I j1 + | true, false => + (* Otherwise, if the operand that has unsigned integer type has + rank greater or equal to the rank of the type of the other operand, + then the operand with signed integer type is converted to the type of + the operand with unsigned integer type. *) + if zle (rank j2) (rank j1) then I j1 else + (* Otherwise, if the type of the operand with signed integer type + can represent all of the values of the type of the operand with + unsigned integer type, then the operand with unsigned integer type is + converted to the type of the operand with signed integer type. *) + if zlt (int_sizeof j1) (int_sizeof j2) then I j2 else + (* Otherwise, both operands are converted to the unsigned integer type + corresponding to the type of the operand with signed integer type. *) + I (unsigned_type j2) + | false, true => + (* Same logic as above, swapping the roles of j1 and j2 *) + if zle (rank j1) (rank j2) then I j2 else + if zlt (int_sizeof j2) (int_sizeof j1) then I j1 else + I (unsigned_type j1) + end + end. + +(** Mapping ISO arithmetic types to CompCert types *) + +Definition proj_type (t: arith_type) : type := + match t with + | I _Bool => Tint IBool Unsigned noattr + | I Char => Tint I8 Unsigned noattr + | I SChar => Tint I8 Signed noattr + | I UChar => Tint I8 Unsigned noattr + | I Short => Tint I16 Signed noattr + | I UShort => Tint I16 Unsigned noattr + | I Int => Tint I32 Signed noattr + | I UInt => Tint I32 Unsigned noattr + | I Long => Tint I32 Signed noattr + | I ULong => Tint I32 Unsigned noattr + | I Longlong => Tlong Signed noattr + | I ULonglong => Tlong Unsigned noattr + | Float => Tfloat F32 noattr + | Double => Tfloat F64 noattr + | Longdouble => Tfloat F64 noattr + end. + +(** Relation between [typeconv] and integer promotion. *) + +Lemma typeconv_integer_promotion: + forall i, typeconv (proj_type (I i)) = proj_type (I (integer_promotion i)). +Proof. + destruct i; reflexivity. +Qed. + +(** Relation between [classify_binarith] and arithmetic conversion. *) + +Lemma classify_binarith_arithmetic_conversion: + forall t1 t2, + binarith_result_type (classify_binarith (proj_type t1) (proj_type t2)) = + Some (proj_type (usual_arithmetic_conversion t1 t2)). +Proof. + destruct t1; destruct t2; try reflexivity. +- destruct it; destruct it0; reflexivity. +- destruct it; reflexivity. +- destruct it; reflexivity. +- destruct it; reflexivity. +- destruct it; reflexivity. +- destruct it; reflexivity. +- destruct it; reflexivity. +Qed. + +End ArithConv. + + + + + + diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index c97e881..685fa71 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -203,16 +203,16 @@ Definition make_binarith (iop iopu fop lop lopu: binary_operation) Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with - | add_case_pi ty _ => + | add_case_pi ty => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Oadd e1 (Ebinop Omul n e2)) - | add_case_ip ty _ => + | add_case_ip ty => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Oadd e2 (Ebinop Omul n e1)) - | add_case_pl ty _ => + | add_case_pl ty => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))) - | add_case_lp ty _ => + | add_case_lp ty => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1))) | add_default => @@ -221,13 +221,13 @@ Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) := Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_sub ty1 ty2 with - | sub_case_pi ty _ => + | sub_case_pi ty => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Odivu (Ebinop Osub e1 e2) n) - | sub_case_pl ty _ => + | sub_case_pl ty => let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2))) | sub_default => diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 5cd032d..41d0dcb 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -145,18 +145,55 @@ Definition attr_of_type (ty: type) := | Tcomp_ptr id a => a end. +(** Change the top-level attributes of a type *) + +Definition change_attributes (f: attr -> attr) (ty: type) : type := + match ty with + | Tvoid => ty + | Tint sz si a => Tint sz si (f a) + | Tlong si a => Tlong si (f a) + | Tfloat sz a => Tfloat sz (f a) + | 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) + end. + +(** Erase the top-level attributes of a type *) + +Definition remove_attributes (ty: type) : type := + change_attributes (fun _ => noattr) ty. + +(** Add extra attributes to the top-level attributes of a type *) + +Definition attr_union (a1 a2: attr) : attr := + {| attr_volatile := a1.(attr_volatile) || a2.(attr_volatile); + attr_alignas := + match a1.(attr_alignas), a2.(attr_alignas) with + | None, al => al + | al, None => al + | Some n1, Some n2 => Some (N.max n1 n2) + end + |}. + +Definition merge_attributes (ty: type) (a: attr) : type := + change_attributes (attr_union a) ty. + Definition type_int32s := Tint I32 Signed noattr. Definition type_bool := Tint IBool Signed noattr. (** The usual unary conversion. Promotes small integer types to [signed int32] - and degrades array types and function types to pointer types. *) + and degrades array types and function types to pointer types. + Attributes are erased. *) Definition typeconv (ty: type) : type := match ty with - | Tint (I8 | I16 | IBool) _ a => Tint I32 Signed a - | Tarray t sz a => Tpointer t a + | Tint (I8 | I16 | IBool) _ _ => Tint I32 Signed noattr + | Tarray t sz a => Tpointer t noattr | Tfunction _ _ _ => Tpointer ty noattr - | _ => ty + | _ => remove_attributes ty end. (** * Operations over types *) diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 71404b2..14c9314 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -161,6 +161,14 @@ let insertion_mask bf = (* Give the mask an hexadecimal string representation, nicer to read *) {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])} +let eshift env op a b = + let ty = unary_conversion env a.etyp in + { edesc = EBinop(op, a, b, ty); etyp = ty } + +let ebinint env op a b = + let ty = binary_conversion env a.etyp b.etyp in + { edesc = EBinop(op, a, b, ty); etyp = ty } + (* Extract the value of a bitfield *) (* Reference C code: @@ -178,15 +186,11 @@ signed int bitfield_signed_extract(unsigned int x, int ofs, int sz) *) -let bitfield_extract bf carrier = - let e1 = - {edesc = EBinop(Oshl, carrier, left_shift_count bf, TInt(IUInt, [])); - etyp = carrier.etyp} in +let bitfield_extract env bf carrier = + let e1 = eshift env Oshl carrier (left_shift_count bf) in let ty = TInt((if bf.bf_signed then IInt else IUInt), []) in let e2 = ecast ty e1 in - let e3 = - {edesc = EBinop(Oshr, e2, right_shift_count bf, e2.etyp); - etyp = ty} in + let e3 = eshift env Oshr e2 (right_shift_count bf) in if bf.bf_signed_res = bf.bf_signed then e3 else ecast (TInt((if bf.bf_signed_res then IInt else IUInt), [])) e3 @@ -203,23 +207,16 @@ unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y) *) -let bitfield_assign bf carrier newval = +let bitfield_assign env bf carrier newval = let msk = insertion_mask bf in let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in let newval_casted = ecast (TInt(IUInt,[])) newval in let newval_shifted = - {edesc = EBinop(Oshl, newval_casted, intconst (Int64.of_int bf.bf_pos) IUInt, - TInt(IUInt,[])); - etyp = TInt(IUInt,[])} in - let newval_masked = - {edesc = EBinop(Oand, newval_shifted, msk, TInt(IUInt,[])); - etyp = TInt(IUInt,[])} - and oldval_masked = - {edesc = EBinop(Oand, carrier, notmsk, TInt(IUInt,[])); - etyp = TInt(IUInt,[])} in - {edesc = EBinop(Oor, oldval_masked, newval_masked, TInt(IUInt,[])); - etyp = TInt(IUInt,[])} + eshift env Oshl newval_casted (intconst (Int64.of_int bf.bf_pos) IUInt) in + let newval_masked = ebinint env Oand newval_shifted msk + and oldval_masked = ebinint env Oand carrier notmsk in + ebinint env Oor oldval_masked newval_masked (* Check whether a field access (e.f or e->f) is a bitfield access. If so, return carrier expression (e and *e, respectively) @@ -322,7 +319,7 @@ let transf_expr env ctx e = {edesc = ECall(texp Val e1, List.map (texp Val) el); etyp = e.etyp} and transf_read e bf = - bitfield_extract bf + bitfield_extract env bf {edesc = EUnop(Odot bf.bf_carrier, texp Val e); etyp = bf.bf_carrier_typ} and transf_assign ctx e1 bf e2 = @@ -330,19 +327,19 @@ let transf_expr env ctx e = let carrier = {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in let asg = - eassign carrier (bitfield_assign bf carrier (texp Val e2)) in - if ctx = Val then ecomma asg (bitfield_extract bf carrier) else asg) + eassign carrier (bitfield_assign env bf carrier (texp Val e2)) in + if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) and transf_assignop ctx op e1 bf e2 tyres = bind_lvalue env (texp Val e1) (fun base -> let carrier = {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in let rhs = - {edesc = EBinop(op, bitfield_extract bf carrier, texp Val e2, tyres); + {edesc = EBinop(op, bitfield_extract env bf carrier, texp Val e2, tyres); etyp = tyres} in let asg = - eassign carrier (bitfield_assign bf carrier rhs) in - if ctx = Val then ecomma asg (bitfield_extract bf carrier) else asg) + eassign carrier (bitfield_assign env bf carrier rhs) in + if ctx = Val then ecomma asg (bitfield_extract env bf carrier) else asg) and transf_pre ctx op e1 bf tyfield = transf_assignop ctx op e1 bf (intconst 1L IInt) @@ -357,11 +354,11 @@ let transf_expr env ctx e = {edesc = EUnop(Odot bf.bf_carrier, base); etyp = bf.bf_carrier_typ} in let temp = mk_temp env tyfield in let tyres = unary_conversion env tyfield in - let settemp = eassign temp (bitfield_extract bf carrier) in + let settemp = eassign temp (bitfield_extract env bf carrier) in let rhs = {edesc = EBinop(op, temp, intconst 1L IInt, tyres); etyp = tyres} in let asg = - eassign carrier (bitfield_assign bf carrier rhs) in + eassign carrier (bitfield_assign env bf carrier rhs) in ecomma (ecomma settemp asg) temp) end diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 22ef187..1169346 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -92,6 +92,13 @@ let attr_array_applicable = function | AConst | AVolatile | ARestrict | AAlignas _ -> false | Attr _ -> true +(* Is an attribute of a composite type applicable to members of this type + when they are accessed? *) + +let attr_inherited_by_members = function + | AConst | AVolatile | ARestrict -> true + | AAlignas _ | Attr _ -> false + (* Adding top-level attributes to a type. Doesn't need to unroll defns. *) (* For array types, standard attrs are pushed to the element type. *) @@ -574,17 +581,20 @@ let unary_conversion env t = | TInt(kind, attr) -> begin match kind with | IBool | IChar | ISChar | IUChar | IShort | IUShort -> - TInt(IInt, attr) + TInt(IInt, []) | IInt | IUInt | ILong | IULong | ILongLong | IULongLong -> - TInt(kind, attr) + TInt(kind, []) end (* Enums are like signed ints *) - | TEnum(id, attr) -> TInt(enum_ikind, attr) + | TEnum(id, attr) -> TInt(enum_ikind, []) (* Arrays and functions decay automatically to pointers *) | TArray(ty, _, _) -> TPtr(ty, []) | TFun _ as ty -> TPtr(ty, []) - (* Other types are not changed *) - | t -> t + (* Float types and pointer types lose their attributes *) + | TFloat(kind, attr) -> TFloat(kind, []) + | TPtr(ty, attr) -> TPtr(ty, []) + (* Other types should not occur, but in doubt... *) + | _ -> t (* The usual binary conversions (H&S 6.3.4). Applies only to arithmetic types. diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 9f59a76..0de0c82 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -54,6 +54,8 @@ val change_attributes_type : Env.t -> (attributes -> attributes) -> typ -> typ (* Apply the given function to the top-level attributes of the given type *) val attr_is_type_related: attribute -> bool (* Is an attribute type-related (true) or variable-related (false)? *) +val attr_inherited_by_members: attribute -> bool + (* Is an attribute of a composite inherited by members of the composite? *) (* Type compatibility *) val compatible_types : ?noattrs: bool -> Env.t -> typ -> typ -> bool diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 0d2cb89..ecc97a7 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -805,7 +805,8 @@ let elab_expr loc env a = error "left-hand side of '.' is not a struct or union" in (* A field of a const/volatile struct or union is itself const/volatile *) { edesc = EUnop(Odot fieldname, b1); - etyp = add_attributes_type attrs (type_of_member env fld) } + etyp = add_attributes_type (List.filter attr_inherited_by_members attrs) + (type_of_member env fld) } | MEMBEROFPTR(a1, fieldname) -> let b1 = elab a1 in @@ -823,7 +824,8 @@ let elab_expr loc env a = | _ -> error "left-hand side of '->' is not a pointer " in { edesc = EUnop(Oarrow fieldname, b1); - etyp = add_attributes_type attrs (type_of_member env fld) } + etyp = add_attributes_type (List.filter attr_inherited_by_members attrs) + (type_of_member env fld) } (* Hack to treat vararg.h functions the GCC way. Helps with testing. va_start(ap,n) @@ -996,14 +998,14 @@ let elab_expr loc env a = if is_arith_type env b1.etyp && is_arith_type env b2.etyp then binary_conversion env b1.etyp b2.etyp else begin - let (ty, attr) = + let ty = match unroll env b1.etyp, unroll env b2.etyp with - | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> (ty, a) - | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> (ty, a) + | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> ty + | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> ty | _, _ -> error "type error in binary '+'" in if not (pointer_arithmetic_ok env ty) then err "illegal pointer arithmetic in binary '+'"; - TPtr(ty, attr) + TPtr(ty, []) end in { edesc = EBinop(Oadd, b1, b2, tyres); etyp = tyres } @@ -1019,11 +1021,11 @@ let elab_expr loc env a = | (TPtr(ty, a) | TArray(ty, _, a)), (TInt _ | TEnum _) -> if not (pointer_arithmetic_ok env ty) then err "illegal pointer arithmetic in binary '-'"; - (TPtr(ty, a), TPtr(ty, a)) + (TPtr(ty, []), TPtr(ty, [])) | (TInt _ | TEnum _), (TPtr(ty, a) | TArray(ty, _, a)) -> if not (pointer_arithmetic_ok env ty) then err "illegal pointer arithmetic in binary '-'"; - (TPtr(ty, a), TPtr(ty, a)) + (TPtr(ty, []), TPtr(ty, [])) | (TPtr(ty1, a1) | TArray(ty1, _, a1)), (TPtr(ty2, a2) | TArray(ty2, _, a2)) -> if not (compatible_types ~noattrs:true env ty1 ty2) then @@ -1084,7 +1086,7 @@ let elab_expr loc env a = | TPtr(ty1, a1), TPtr(ty2, a2) -> let tyres = if is_void_type env ty1 || is_void_type env ty2 then - TPtr(TVoid [], add_attributes a1 a2) + TPtr(TVoid (add_attributes a1 a2), []) else match combine_types ~noattrs:true env (TPtr(ty1, a1)) (TPtr(ty2, a2)) with @@ -1095,9 +1097,9 @@ let elab_expr loc env a = in { edesc = EConditional(b1, b2, b3); etyp = tyres } | TPtr(ty1, a1), TInt _ when is_literal_0 b3 -> - { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, a1) } + { edesc = EConditional(b1, b2, nullconst); etyp = TPtr(ty1, []) } | TInt _, TPtr(ty2, a2) when is_literal_0 b2 -> - { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, a2) } + { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) } | ty1, ty2 -> match combine_types ~noattrs:true env ty1 ty2 with | None -> @@ -1312,7 +1314,7 @@ let init_char_array_string opt_size s = if i < 0L then init else begin let c = if i < len then Int64.of_int (Char.code s.[Int64.to_int i]) else 0L in - add_chars (Int64.pred i) (Init_single (intconst c IChar) :: init) + add_chars (Int64.pred i) (Init_single (intconst c IInt) :: init) end in Init_array (add_chars (Int64.pred size) []) diff --git a/extraction/extraction.v b/extraction/extraction.v index b9f684e..344a00f 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -21,6 +21,7 @@ Require Inlining. Require ValueDomain. Require Tailcall. Require Allocation. +Require Ctypes. Require Compiler. (* Standard lib *) @@ -125,6 +126,7 @@ Cd "extraction". Separate Extraction Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state + Ctypes.merge_attributes Ctypes.remove_attributes Initializers.transl_init Initializers.constval Csyntax.Eindex Csyntax.Epreincr Conventions1.dummy_int_reg Conventions1.dummy_float_reg -- cgit v1.2.3