From 3d25d06ec58f0527b6f0eee7e0df19c18f7133ed Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 14 Sep 2019 19:37:28 +0200 Subject: clightgen -dclight: print function parameters correctly The Clight output of clightgen is Clight version 2, after SimplLocals conversion, where function parameters are temporary variables, not variables. This commit makes sure the function parameters are printed as temporary variables and not as variables. In passing, it generalizes the Clight pretty-printer so that it can print both Clight version 1 and Clight version 2. Closes: #314 --- cfrontend/PrintClight.ml | 41 ++++++++++++++++++++++++++++++----------- cfrontend/PrintCsyntax.ml | 8 ++++---- 2 files changed, 34 insertions(+), 15 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index ca378c11..e63067a9 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -236,10 +236,20 @@ and print_stmt_for p s = | _ -> fprintf p "({ %a })" print_stmt s -let print_function p id f = +(* There are two versions of Clight, Clight1 and Clight2, that differ + only in the meaning of function parameters: + - in Clight1, function parameters are variables + - in Clight2, function parameters are temporaries. +*) + +type clight_version = Clight1 | Clight2 + +let name_param = function Clight1 -> extern_atom | Clight2 -> temp_name + +let print_function ver p id f = fprintf p "%s@ " - (name_cdecl (name_function_parameters (extern_atom id) - f.fn_params f.fn_callconv) + (name_cdecl (name_function_parameters (name_param ver) + (extern_atom id) f.fn_params f.fn_callconv) f.fn_return); fprintf p "@[{@ "; List.iter @@ -253,12 +263,12 @@ let print_function p id f = print_stmt p f.fn_body; fprintf p "@;<0 -2>}@]@ @ " -let print_fundef p id fd = +let print_fundef ver p id fd = match fd with | Ctypes.External(_, _, _, _) -> () | Internal f -> - print_function p id f + print_function ver p id f let print_fundecl p id fd = match fd with @@ -271,9 +281,9 @@ let print_fundecl p id fd = fprintf p "%s;@ " (name_cdecl (extern_atom id) (Clight.type_of_function f)) -let print_globdef p (id, gd) = +let print_globdef var p (id, gd) = match gd with - | AST.Gfun f -> print_fundef p id f + | AST.Gfun f -> print_fundef var p id f | AST.Gvar v -> print_globvar p id v (* from PrintCsyntax *) let print_globdecl p (id, gd) = @@ -281,20 +291,29 @@ let print_globdecl p (id, gd) = | AST.Gfun f -> print_fundecl p id f | AST.Gvar v -> () -let print_program p prog = +let print_program ver p prog = fprintf p "@["; List.iter (declare_composite p) prog.prog_types; List.iter (define_composite p) prog.prog_types; List.iter (print_globdecl p) prog.prog_defs; - List.iter (print_globdef p) prog.prog_defs; + List.iter (print_globdef ver p) prog.prog_defs; fprintf p "@]@." let destination : string option ref = ref None -let print_if prog = +let print_if_gen ver prog = match !destination with | None -> () | Some f -> let oc = open_out f in - print_program (formatter_of_out_channel oc) prog; + print_program ver (formatter_of_out_channel oc) prog; close_out oc + +(* print_if is called from driver/Compiler.v between the SimplExpr + and SimplLocals passes. It receives Clight1 syntax. *) +let print_if prog = print_if_gen Clight1 prog + +(* print_if_2 is called from clightgen/Clightgen.ml, after the + SimplLocals pass. It receives Clight2 syntax. *) +let print_if_2 prog = print_if_gen Clight2 prog + diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 3a44796c..1c9729c5 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -391,7 +391,7 @@ and print_stmt_for p s = | _ -> fprintf p "({ %a })" print_stmt s -let name_function_parameters fun_name params cconv = +let name_function_parameters name_param fun_name params cconv = let b = Buffer.create 20 in Buffer.add_string b fun_name; Buffer.add_char b '('; @@ -404,7 +404,7 @@ let name_function_parameters fun_name params cconv = if cconv.cc_vararg then Buffer.add_string b ",..." | (id, ty) :: rem -> if not first then Buffer.add_string b ", "; - Buffer.add_string b (name_cdecl (extern_atom id) ty); + Buffer.add_string b (name_cdecl (name_param id) ty); add_params false rem in add_params true params end; @@ -413,8 +413,8 @@ let name_function_parameters fun_name params cconv = let print_function p id f = fprintf p "%s@ " - (name_cdecl (name_function_parameters (extern_atom id) - f.fn_params f.fn_callconv) + (name_cdecl (name_function_parameters extern_atom + (extern_atom id) f.fn_params f.fn_callconv) f.fn_return); fprintf p "@[{@ "; List.iter -- cgit From 8ac255f207b6864fa22552a48f84ffcf23f747b4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 14 Sep 2019 19:42:25 +0200 Subject: -dclight output: use nicer names for temporary variables The temporary variables introduced by SimplLocals reuse the same integer identifiers as the local variables they come from. This commit ensures that these variables are printed as "$var", where "var" is the original variable name, instead of "$NNN" as before. The "$NNN" form is retained for temporary variables that do not correspond to a source-level local variable, such as the temporary variables introduced by SimplExpr. This commit should make no difference for "ccomp -dclight", because the Clight that is printed is the Clight version 1 produced by SimplExpr, where every temporary is fresh and does not correspond to a source-level local variable. This commit does change the output of "clightgen -dclight", because the Clight that is printed is the Clight version 2 produced by SimplLocals. The printed Clight is much more legible thanks to the more meaningful temporary variable names. --- cfrontend/PrintClight.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index e63067a9..0e735d2d 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -23,9 +23,18 @@ open Cop open PrintCsyntax open Clight -(* Naming temporaries *) +(* Naming temporaries. + Some temporaries are obtained by lifting variables in SimplLocals. + For these we use a meaningful name "$var", as found in the table of + atoms. Other temporaries are generated during SimplExpr, and are + not in the table of atoms. We print them as "$NNN" (a unique + integer). *) -let temp_name (id: AST.ident) = "$" ^ Z.to_string (Z.Zpos id) +let temp_name (id: AST.ident) = + try + "$" ^ Hashtbl.find string_of_atom id + with Not_found -> + Printf.sprintf "$%d" (P.to_int id) (* Declarator (identifier + type) -- reuse from PrintCsyntax *) -- cgit From a99406bbd9c01dc04e79b14681a254fe22c9d424 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 28 Nov 2019 17:00:27 +0100 Subject: Fix for AArch64 alignment problem (#206) In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time. This PR extends the check for a representable offset for the addressing of global variables to also check whether the variable is correctly aligned. Only if both conditions are met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic loadsymbol sequence. --- cfrontend/C2C.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c1dfa9f4..9ae7bbd9 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -61,6 +61,11 @@ let atom_alignof a = with Not_found -> None +let atom_is_aligned a sz = + match atom_alignof a with + | None -> false + | Some align -> align mod (Z.to_int sz) = 0 + let atom_sections a = try (Hashtbl.find decl_atom a).a_sections -- cgit From 9b881b7928ab7d21e9981133bef5b26e33b6cd9d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 11 Feb 2020 18:43:24 +0100 Subject: Take the sign into account for int to ptr cast. Casting from an integer constant to pointer on 64 bit architectures did not take the signedness into account and always interpreted the integer as unsigned which causes some incompatibility with libc implementations. --- cfrontend/Cop.v | 4 ++-- cfrontend/Ctyping.v | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index aa73abb0..143e87a3 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -140,8 +140,8 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases := | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s (* To pointer types *) - | Tpointer _ _, Tint _ _ _ => - if Archi.ptr64 then cast_case_i2l Unsigned else cast_case_pointer + | Tpointer _ _, Tint _ si _ => + if Archi.ptr64 then cast_case_i2l si else cast_case_pointer | Tpointer _ _, Tlong _ _ => if Archi.ptr64 then cast_case_pointer else cast_case_l2i I32 Unsigned | Tpointer _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_pointer diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index b92a9bac..29ea3bf2 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -987,6 +987,7 @@ Proof. classify_cast (Tint i s a) t2 <> cast_case_default). { unfold classify_cast. destruct t2; try congruence. destruct f; congruence. + destruct Archi.ptr64; congruence. } destruct i; auto. Qed. -- cgit From a9eaf4897c825093aba2137ff76e56bfbf1e72d5 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 20 Feb 2020 18:55:34 +0100 Subject: More precise determination of small data accesses (#220) We can get linker errors for addresses of the form "symbol + offset" where "symbol" is in the small data area and "offset" is large enough to overflow the relative displacement from the SDA base register. To avoid this, this commit enriches `C2C.atom_is_small_data`, which is the implementation of `Asm.symbol_is_small_data` in the PPC port, with a check that the offset is within the bounds of the symbol. If it is not, `Asm.symbol_is_small_data` returns `false` and Asmgen produces an absolute addressing instead of a SDA-relative addressing. To implement the check, we record the sizes of symbols in the atom table, just like we already record their alignments. --- cfrontend/C2C.ml | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 9ae7bbd9..293e79f0 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -33,6 +33,7 @@ type inline_status = type atom_info = { a_storage: C.storage; (* storage class *) + a_size: int64 option; (* size in bytes *) a_alignment: int option; (* alignment *) a_sections: Sections.section_name list; (* in which section to put it *) (* 1 section for data, 3 sections (code/lit/jumptbl) for functions *) @@ -72,9 +73,14 @@ let atom_sections a = with Not_found -> [] -let atom_is_small_data a ofs = +let atom_is_small_data a ofs = try - (Hashtbl.find decl_atom a).a_access = Sections.Access_near + let info = Hashtbl.find decl_atom a in + info.a_access = Sections.Access_near + && (match info.a_size with + | None -> false + | Some sz -> + let ofs = camlint64_of_ptrofs ofs in 0L <= ofs && ofs < sz) with Not_found -> false @@ -352,6 +358,7 @@ let name_for_string_literal s = Hashtbl.add decl_atom id { a_storage = C.Storage_static; a_alignment = Some 1; + a_size = Some (Int64.of_int (String.length s + 1)); a_sections = [Sections.for_stringlit()]; a_access = Sections.Access_default; a_inline = No_specifier; @@ -379,9 +386,12 @@ let name_for_wide_string_literal s = incr stringNum; let name = Printf.sprintf "__stringlit_%d" !stringNum in let id = intern_string name in + let wchar_size = Machine.((!config).sizeof_wchar) in Hashtbl.add decl_atom id { a_storage = C.Storage_static; - a_alignment = Some Machine.((!config).sizeof_wchar); + a_alignment = Some wchar_size; + a_size = Some (Int64.(mul (of_int (List.length s + 1)) + (of_int wchar_size))); a_sections = [Sections.for_stringlit()]; a_access = Sections.Access_default; a_inline = No_specifier; @@ -1223,6 +1233,7 @@ let convertFundef loc env fd = Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; + a_size = None; a_sections = Sections.for_function env id' fd.fd_attrib; a_access = Sections.Access_default; a_inline = inline; @@ -1309,6 +1320,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = Hashtbl.add decl_atom id' { a_storage = sto; a_alignment = Some (Z.to_int al); + a_size = Some (Z.to_int64 sz); a_sections = [section]; a_access = access; a_inline = No_specifier; -- cgit From be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 18 Feb 2020 16:57:17 +0100 Subject: Refine the type of function results in AST.signature Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions. --- cfrontend/Csem.v | 2 +- cfrontend/Cshmgen.v | 4 +-- cfrontend/Csyntax.v | 2 +- cfrontend/Ctypes.v | 19 +++++++++-- cfrontend/Ctyping.v | 86 ++++++++++++++++++++++++++++++----------------- cfrontend/PrintCsyntax.ml | 4 +-- 6 files changed, 78 insertions(+), 39 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index a76a14ba..6d2b470f 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -444,7 +444,7 @@ Lemma red_selection: Proof. intros. unfold Eselection. set (t := typ_of_type ty). - set (sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default). + set (sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default). assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select t))). { unfold sg, t; destruct ty as [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ]; simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. } diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 792a73f9..ee135dcd 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -602,7 +602,7 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat) 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_res := rettype_of_type res; sig_cc := cconv |} tb tcl) | _ => Error(msg "Cshmgen.transl_stmt(call)") @@ -667,7 +667,7 @@ Definition transl_var (ce: composite_env) (v: ident * type) := 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_res := rettype_of_type (Clight.fn_return f); sig_cc := Clight.fn_callconv f |}. Definition transl_function (ce: composite_env) (f: Clight.function) : res function := diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index c34a5e13..e3e2c1e9 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -106,7 +106,7 @@ Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) := Definition Eselection (r1 r2 r3: expr) (ty: type) := let t := typ_of_type ty in - let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in + let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in Ebuiltin (EF_builtin "__builtin_sel"%string sg) (Tcons type_bool (Tcons ty (Tcons ty Tnil))) (Econs r1 (Econs r2 (Econs r3 Enil))) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index bfc5daa9..664a60c5 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -732,8 +732,21 @@ Definition typ_of_type (t: type) : AST.typ := | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr end. -Definition opttyp_of_type (t: type) : option AST.typ := - if type_eq t Tvoid then None else Some (typ_of_type t). +Definition rettype_of_type (t: type) : AST.rettype := + match t with + | Tvoid => AST.Tvoid + | Tint I32 _ _ => AST.Tint + | Tint I8 Signed _ => AST.Tint8signed + | Tint I8 Unsigned _ => AST.Tint8unsigned + | Tint I16 Signed _ => AST.Tint16signed + | Tint I16 Unsigned _ => AST.Tint16unsigned + | Tint IBool _ _ => AST.Tint8unsigned + | Tlong _ _ => AST.Tlong + | Tfloat F32 _ => AST.Tsingle + | Tfloat F64 _ => AST.Tfloat + | Tpointer _ _ => AST.Tptr + | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tvoid + end. Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := match tl with @@ -742,7 +755,7 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := end. Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature := - mksignature (typlist_of_typelist args) (opttyp_of_type res) cc. + mksignature (typlist_of_typelist args) (rettype_of_type res) cc. (** * Construction of the composite environment *) diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 29ea3bf2..00fcf8ab 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -397,10 +397,10 @@ Inductive wt_rvalue : expr -> Prop := wt_arguments rargs tyargs -> (* This typing rule is specialized to the builtin invocations generated by C2C, which are either __builtin_sel or builtins returning void. *) - (ty = Tvoid /\ sig_res (ef_sig ef) = None) + (ty = Tvoid /\ sig_res (ef_sig ef) = AST.Tvoid) \/ (tyargs = Tcons type_bool (Tcons ty (Tcons ty Tnil)) /\ let t := typ_of_type ty in - let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in + let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in ef = EF_builtin "__builtin_sel"%string sg) -> wt_rvalue (Ebuiltin ef tyargs rargs ty) | wt_Eparen: forall r tycast ty, @@ -521,11 +521,20 @@ Fixpoint bind_globdef (e: typenv) (l: list (ident * globdef fundef type)) : type | (id, Gvar v) :: l => bind_globdef (PTree.set id v.(gvar_info) e) l end. +Inductive wt_fundef (ce: composite_env) (e: typenv) : fundef -> Prop := + | wt_fundef_internal: forall f, + wt_function ce e f -> + wt_fundef ce e (Internal f) + | wt_fundef_external: forall ef targs tres cc, + (ef_sig ef).(sig_res) = rettype_of_type tres -> + wt_fundef ce e (External ef targs tres cc). + Inductive wt_program : program -> Prop := | wt_program_intro: forall p, let e := bind_globdef (PTree.empty _) p.(prog_defs) in - (forall id f, In (id, Gfun (Internal f)) p.(prog_defs) -> - wt_function p.(prog_comp_env) e f) -> + (forall id fd, + In (id, Gfun fd) p.(prog_defs) -> + wt_fundef p.(prog_comp_env) e fd) -> wt_program p. Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty. @@ -745,7 +754,7 @@ Definition ebuiltin (ef: external_function) (tyargs: typelist) (args: exprlist) do x1 <- check_rvals args; do x2 <- check_arguments args tyargs; if type_eq tyres Tvoid - && opt_typ_eq (sig_res (ef_sig ef)) None + && AST.rettype_eq (sig_res (ef_sig ef)) AST.Tvoid then OK (Ebuiltin ef tyargs args tyres) else Error (msg "builtin: wrong type decoration"). @@ -915,7 +924,8 @@ Definition retype_function (ce: composite_env) (e: typenv) (f: function) : res f Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fundef := match fd with | Internal f => do f' <- retype_function ce e f; OK (Internal f') - | External id args res cc => OK fd + | External ef args res cc => + assertion (rettype_eq (ef_sig ef).(sig_res) (rettype_of_type res)); OK fd end. Definition typecheck_program (p: program) : res program := @@ -1241,7 +1251,7 @@ Lemma ebuiltin_sound: Proof. intros. monadInv H. destruct (type_eq tyres Tvoid); simpl in EQ2; try discriminate. - destruct (opt_typ_eq (sig_res (ef_sig ef)) None); inv EQ2. + destruct (rettype_eq (sig_res (ef_sig ef)) AST.Tvoid); inv EQ2. econstructor; eauto. eapply check_arguments_sound; eauto. Qed. @@ -1373,6 +1383,14 @@ Proof. intros. monadInv H. constructor; simpl. eapply retype_stmt_sound; eauto. Qed. +Lemma retype_fundef_sound: + forall ce e fd fd', retype_fundef ce e fd = OK fd' -> wt_fundef ce e fd'. +Proof. + intros. destruct fd; monadInv H. +- constructor; eapply retype_function_sound; eauto. +- constructor; auto. +Qed. + Theorem typecheck_program_sound: forall p p', typecheck_program p = OK p' -> wt_program p'. Proof. @@ -1395,11 +1413,11 @@ Proof. inv H1. simpl. auto. } rewrite ENVS. - intros id f. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp). + intros id fd. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp). induction 1; simpl; intros. contradiction. destruct H0; auto. subst b1; inv H. simpl in H1. inv H1. - destruct f1; monadInv H4. eapply retype_function_sound; eauto. + eapply retype_fundef_sound; eauto. Qed. (** * Subject reduction *) @@ -1711,6 +1729,26 @@ Proof. inv H; auto. Qed. +Lemma has_rettype_wt_val: + forall v ty, + Val.has_rettype v (rettype_of_type ty) -> wt_val v ty. +Proof. + unfold rettype_of_type, Val.has_rettype, Val.has_type; destruct ty; intros. +- destruct v; contradiction || constructor. +- destruct i. + + destruct s; destruct v; try contradiction; constructor; red; auto. + + destruct s; destruct v; try contradiction; constructor; red; auto. + + destruct v; try contradiction; constructor; auto. + + destruct v; try contradiction; constructor; red; auto. +- destruct v; try contradiction; constructor; auto. +- destruct f; destruct v; try contradiction; constructor. +- unfold Tptr in *; destruct v; destruct Archi.ptr64 eqn:P64; try contradiction; constructor; auto. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +Qed. + Lemma wt_rred: forall ge tenv a m t a' m', rred ge a m t a' m' -> wt_rvalue ge tenv a -> wt_rvalue ge tenv a'. @@ -1750,7 +1788,7 @@ Proof. - (* builtin *) subst. destruct H7 as [(A & B) | (A & B)]. + subst ty. auto with ty. + simpl in B. set (T := typ_of_type ty) in *. - set (sg := mksignature (AST.Tint :: T :: T :: nil) (Some T) cc_default) in *. + set (sg := mksignature (AST.Tint :: T :: T :: nil) T cc_default) in *. assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select T))). { unfold sg, T; destruct ty as [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ]; simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. } @@ -1896,12 +1934,6 @@ Hypothesis WTPROG: wt_program prog. Let ge := globalenv prog. Let gtenv := bind_globdef (PTree.empty _) prog.(prog_defs). -Hypothesis WT_EXTERNAL: - forall id ef args res cc vargs m t vres m', - In (id, Gfun (External ef args res cc)) prog.(prog_defs) -> - external_call ef ge vargs m t vres m' -> - wt_val vres res. - Inductive wt_expr_cont: typenv -> function -> cont -> Prop := | wt_Kdo: forall te f k, wt_stmt_cont te f k -> @@ -2000,12 +2032,6 @@ Proof. induction 1; simpl; auto; econstructor; eauto. Qed. -Definition wt_fundef (fd: fundef) := - match fd with - | Internal f => wt_function ge gtenv f - | External ef targs tres cc => True - end. - Definition fundef_return (fd: fundef) : type := match fd with | Internal f => f.(fn_return) @@ -2013,10 +2039,10 @@ Definition fundef_return (fd: fundef) : type := end. Lemma wt_find_funct: - forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef fd. + forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef ge gtenv fd. Proof. intros. apply Genv.find_funct_prop with (p := prog) (v := v); auto. - intros. inv WTPROG. destruct f; simpl; auto. apply H1 with id; auto. + intros. inv WTPROG. apply H1 with id; auto. Qed. Inductive wt_state: state -> Prop := @@ -2032,7 +2058,7 @@ Inductive wt_state: state -> Prop := wt_state (ExprState f r k e m) | wt_call_state: forall b fd vargs k m (WTK: wt_call_cont k (fundef_return fd)) - (WTFD: wt_fundef fd) + (WTFD: wt_fundef ge gtenv fd) (FIND: Genv.find_funct ge b = Some fd), wt_state (Callstate fd vargs k m) | wt_return_state: forall v k m ty @@ -2089,7 +2115,6 @@ Qed. End WT_FIND_LABEL. - Lemma preservation_estep: forall S t S', estep ge S t S' -> wt_state S -> wt_state S'. Proof. @@ -2164,9 +2189,10 @@ Proof. - inv WTS; eauto with ty. - exploit wt_find_label. eexact WTB. eauto. eapply call_cont_wt'; eauto. intros [A B]. eauto with ty. -- simpl in WTFD; inv WTFD. econstructor; eauto. apply wt_call_cont_stmt_cont; auto. -- exploit (Genv.find_funct_inversion prog); eauto. intros (id & A). - econstructor; eauto. +- inv WTFD. inv H3. econstructor; eauto. apply wt_call_cont_stmt_cont; auto. +- inv WTFD. econstructor; eauto. + apply has_rettype_wt_val. simpl; rewrite <- H1. + eapply external_call_well_typed_gen; eauto. - inv WTK. eauto with ty. Qed. @@ -2181,7 +2207,7 @@ Theorem wt_initial_state: Proof. intros. inv H. econstructor. constructor. apply Genv.find_funct_ptr_prop with (p := prog) (b := b); auto. - intros. inv WTPROG. destruct f0; simpl; auto. apply H4 with id; auto. + intros. inv WTPROG. apply H4 with id; auto. instantiate (1 := (Vptr b Ptrofs.zero)). rewrite Genv.find_funct_find_funct_ptr. auto. Qed. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 1c9729c5..03dc5837 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -19,7 +19,7 @@ open Format open Camlcoq open Values open AST -open Ctypes +open! Ctypes open Cop open Csyntax @@ -85,7 +85,7 @@ let name_optid id = let rec name_cdecl id ty = match ty with - | Tvoid -> + | Ctypes.Tvoid -> "void" ^ name_optid id | Ctypes.Tint(sz, sg, a) -> name_inttype sz sg ^ attributes a ^ name_optid id -- cgit From 28f235806aa0918499b2ef162110f513ebe4db30 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 19 Feb 2020 12:50:55 +0100 Subject: Support re-normalization of values returned by function calls Some ABIs leave more flexibility concerning function return values than CompCert expects. For example, the x86 ABI says that a function result of type "char" is returned in register AL, leaving the top 24 bits of register EAX unspecified, while CompCert expects EAX to contain 32 valid bits, namely the zero- or sign-extension of the 8-bit result. This commits adds a general mechanism to insert "re-normalization" conversions on the results of function calls. Currently, it only deals with results of small integer types, and inserts zero- or sign-extensions if so instructed by a platform-dependent function, Convention1.return_value_needs_normalization. The conversions in question are inserted early in the front-end, so that they can be optimized away in the back-end. The semantic preservation proof is still conducted against the CompCert model, where the return values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to return values that are not normalized. --- cfrontend/Cshmgen.v | 37 +++++++++++-- cfrontend/Cshmgenproof.v | 133 ++++++++++++++++++++++++++++++++++++----------- 2 files changed, 137 insertions(+), 33 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index ee135dcd..5bd12d00 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -23,6 +23,7 @@ Require Import Coqlib Maps Errors Integers Floats. Require Import AST Linking. Require Import Ctypes Cop Clight Cminor Csharpminor. +Require Import Conventions1. Local Open Scope string_scope. Local Open Scope error_monad_scope. @@ -558,6 +559,34 @@ Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist) typ_of_type (default_argument_conversion (typeof a1)) :: typlist_of_arglist a2 Tnil end. +(** Translate a function call. + Depending on the ABI, it may be necessary to normalize the value + returned by casting it to the return type of the function. + For example, in the x86 ABI, a return value of type "char" is + returned in register AL, leaving the top 24 bits of EAX + unspecified. Hence, a cast to type "char" is needed to sign- or + zero-extend the returned integer before using it. *) + +Definition make_normalization (t: type) (a: expr) := + match t with + | Tint IBool _ _ => Eunop Ocast8unsigned a + | Tint I8 Signed _ => Eunop Ocast8signed a + | Tint I8 Unsigned _ => Eunop Ocast8unsigned a + | Tint I16 Signed _ => Eunop Ocast16signed a + | Tint I16 Unsigned _ => Eunop Ocast16unsigned a + | _ => a + end. + +Definition make_funcall (x: option ident) (tres: type) (sg: signature) + (fn: expr) (args: list expr): stmt := + match x, return_value_needs_normalization sg.(sig_res) with + | Some id, true => + Sseq (Scall x sg fn args) + (Sset id (make_normalization tres (Evar id))) + | _, _ => + Scall x sg fn args + end. + (** * Translation of statements *) (** [transl_statement nbrk ncnt s] returns a Csharpminor statement @@ -601,10 +630,10 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat) | fun_case_f args res cconv => 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 := rettype_of_type res; - sig_cc := cconv |} - tb tcl) + let sg := {| sig_args := typlist_of_arglist cl args; + sig_res := rettype_of_type res; + sig_cc := cconv |} in + OK (make_funcall x res sg tb tcl) | _ => Error(msg "Cshmgen.transl_stmt(call)") end | Clight.Sbuiltin x ef tyargs bl => diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 09e31cb2..1ceb8e4d 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -15,7 +15,7 @@ Require Import Coqlib Errors Maps Integers Floats. Require Import AST Linking. Require Import Values Events Memory Globalenvs Smallstep. -Require Import Ctypes Cop Clight Cminor Csharpminor. +Require Import Ctypes Ctyping Cop Clight Cminor Csharpminor. Require Import Cshmgen. (** * Relational specification of the transformation *) @@ -996,6 +996,26 @@ Proof. eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto. Qed. +Lemma make_normalization_correct: + forall e le m a v t, + eval_expr ge e le m a v -> + wt_val v t -> + eval_expr ge e le m (make_normalization t a) v. +Proof. + intros. destruct t; simpl; auto. inv H0. +- destruct i; simpl in H3. + + destruct s; econstructor; eauto; simpl; congruence. + + destruct s; econstructor; eauto; simpl; congruence. + + auto. + + econstructor; eauto; simpl; congruence. +- auto. +- destruct i. + + destruct s; econstructor; eauto. + + destruct s; econstructor; eauto. + + auto. + + econstructor; eauto. +Qed. + End CONSTRUCTORS. (** * Basic preservation invariants *) @@ -1360,7 +1380,16 @@ Inductive match_cont: composite_env -> type -> nat -> nat -> Clight.cont -> Csha match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk -> match_cont ce tyret nbrk ncnt (Clight.Kcall id f e le k) - (Kcall id tf te le tk). + (Kcall id tf te le tk) + | match_Kcall_normalize: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id a tf te le tk cu, + linkorder cu prog -> + transl_function cu.(prog_comp_env) f = OK tf -> + match_env e te -> + match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk -> + (forall v e le m, wt_val v tyret -> le!id = Some v -> eval_expr tge e le m a v) -> + match_cont ce tyret nbrk ncnt + (Clight.Kcall (Some id) f e le k) + (Kcall (Some id) tf te le (Kseq (Sset id a) tk)). Inductive match_states: Clight.state -> Csharpminor.state -> Prop := | match_state: @@ -1377,14 +1406,15 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop := forall fd args k m tfd tk targs tres cconv cu ce (LINK: linkorder cu prog) (TR: match_fundef cu fd tfd) - (MK: match_cont ce Tvoid 0%nat 0%nat k tk) + (MK: match_cont ce tres 0%nat 0%nat k tk) (ISCC: Clight.is_call_cont k) (TY: type_of_fundef fd = Tfunction targs tres cconv), match_states (Clight.Callstate fd args k m) (Callstate tfd args tk m) | match_returnstate: - forall res k m tk ce - (MK: match_cont ce Tvoid 0%nat 0%nat k tk), + forall res tres k m tk ce + (MK: match_cont ce tres 0%nat 0%nat k tk) + (WT: wt_val res tres), match_states (Clight.Returnstate res k m) (Returnstate res tk m). @@ -1442,7 +1472,9 @@ Proof. - (* set *) auto. - (* call *) - simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto. + simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. + unfold make_funcall. + destruct o; auto; destruct Conventions1.return_value_needs_normalization; auto. - (* builtin *) auto. - (* seq *) @@ -1500,24 +1532,26 @@ End FIND_LABEL. (** Properties of call continuations *) Lemma match_cont_call_cont: - forall ce' tyret' nbrk' ncnt' ce tyret nbrk ncnt k tk, + forall ce' nbrk' ncnt' ce tyret nbrk ncnt k tk, match_cont ce tyret nbrk ncnt k tk -> - match_cont ce' tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk). + match_cont ce' tyret nbrk' ncnt' (Clight.call_cont k) (call_cont tk). Proof. induction 1; simpl; auto. - constructor. - econstructor; eauto. +- apply match_Kstop. +- eapply match_Kcall; eauto. +- eapply match_Kcall_normalize; eauto. Qed. Lemma match_cont_is_call_cont: - forall ce tyret nbrk ncnt k tk ce' tyret' nbrk' ncnt', + forall ce tyret nbrk ncnt k tk ce' nbrk' ncnt', match_cont ce tyret nbrk ncnt k tk -> Clight.is_call_cont k -> - match_cont ce' tyret' nbrk' ncnt' k tk /\ is_call_cont tk. + match_cont ce' tyret nbrk' ncnt' k tk /\ is_call_cont tk. Proof. intros. inv H; simpl in H0; try contradiction; simpl. - split; auto; constructor. - split; auto; econstructor; eauto. + split; auto; apply match_Kstop. + split; auto; eapply match_Kcall; eauto. + split; auto; eapply match_Kcall_normalize; eauto. Qed. (** The simulation proof *) @@ -1549,19 +1583,44 @@ Proof. - (* call *) revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence. - intros targs tres cc CF TR. monadInv TR. inv MTR. + intros targs tres cc CF TR. monadInv TR. exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK'). rewrite H in CF. simpl in CF. inv CF. - econstructor; split. - apply plus_one. econstructor; eauto. - eapply transl_expr_correct with (cunit := cu); eauto. - eapply transl_arglist_correct with (cunit := cu); eauto. - erewrite typlist_of_arglist_eq by eauto. - eapply transl_fundef_sig1; eauto. - rewrite H3. auto. - econstructor; eauto. - eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto. - simpl. auto. + set (sg := {| sig_args := typlist_of_arglist al targs; + sig_res := rettype_of_type tres; + sig_cc := cc |}) in *. + assert (SIG: funsig tfd = sg). + { unfold sg; erewrite typlist_of_arglist_eq by eauto. + eapply transl_fundef_sig1; eauto. rewrite H3; auto. } + assert (EITHER: tk' = tk /\ ts' = Scall optid sg x x0 + \/ exists id, optid = Some id /\ + tk' = tk /\ ts' = Sseq (Scall optid sg x x0) + (Sset id (make_normalization tres (Evar id)))). + { unfold make_funcall in MTR. + destruct optid. destruct Conventions1.return_value_needs_normalization. + inv MTR. right; exists i; auto. + inv MTR; auto. + inv MTR; auto. } + destruct EITHER as [(EK & ES) | (id & EI & EK & ES)]; rewrite EK, ES. + + (* without normalization of return value *) + econstructor; split. + apply plus_one. eapply step_call; eauto. + eapply transl_expr_correct with (cunit := cu); eauto. + eapply transl_arglist_correct with (cunit := cu); eauto. + econstructor; eauto. + eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto. + exact I. + + (* with normalization of return value *) + subst optid. + econstructor; split. + eapply plus_two. apply step_seq. eapply step_call; eauto. + eapply transl_expr_correct with (cunit := cu); eauto. + eapply transl_arglist_correct with (cunit := cu); eauto. + traceEq. + econstructor; eauto. + eapply match_Kcall_normalize with (ce := prog_comp_env cu') (cu := cu); eauto. + intros. eapply make_normalization_correct; eauto. constructor; eauto. + exact I. - (* builtin *) monadInv TR. inv MTR. @@ -1658,6 +1717,7 @@ Proof. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. + constructor. - (* return some *) monadInv TR. inv MTR. @@ -1667,6 +1727,7 @@ Proof. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. + apply wt_val_casted. eapply cast_val_is_casted; eauto. - (* skip call *) monadInv TR. inv MTR. @@ -1675,6 +1736,7 @@ Proof. apply plus_one. apply step_skip_call. auto. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. + constructor. - (* switch *) monadInv TR. @@ -1738,20 +1800,33 @@ Proof. simpl. econstructor; eauto. unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto. constructor. + replace (fn_return f) with tres. eassumption. + simpl in TY. unfold type_of_function in TY. congruence. - (* external function *) inv TR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. - apply plus_one. constructor. eauto. + apply plus_one. constructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. eapply match_returnstate with (ce := ce); eauto. + apply has_rettype_wt_val. + replace (rettype_of_type tres0) with (sig_res (ef_sig ef)). + eapply external_call_well_typed_gen; eauto. + rewrite H5. simpl. simpl in TY. congruence. - (* returnstate *) inv MK. - econstructor; split. - apply plus_one. constructor. - econstructor; eauto. simpl; reflexivity. constructor. + + (* without normalization *) + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl; reflexivity. constructor. + + (* with normalization *) + econstructor; split. + eapply plus_three. econstructor. econstructor. constructor. + simpl. apply H13. eauto. apply PTree.gss. + traceEq. + simpl. rewrite PTree.set2. econstructor; eauto. simpl; reflexivity. constructor. Qed. Lemma transl_initial_states: -- cgit From f8d3d265f6ef967acf6eea017cb472809096a135 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 2 Mar 2020 10:41:11 +0100 Subject: Define the semantics of `free(NULL)` (#226) According to ISO C, `free(NULL)` is correct and does nothing. This commit updates accordingly the formal semantics of the `free` external function and the reference interpreter. Closes: #334 --- cfrontend/Cexec.v | 73 +++++++++++++++++++++++++++++++++---------------------- 1 file changed, 44 insertions(+), 29 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 2942080b..b08c3ad7 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -460,6 +460,14 @@ Definition do_ef_free check (zlt 0 (Ptrofs.unsigned sz)); do m' <- Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz); Some(w, E0, Vundef, m') + | Vint n :: nil => + if Int.eq_dec n Int.zero && negb Archi.ptr64 + then Some(w, E0, Vundef, m) + else None + | Vlong n :: nil => + if Int64.eq_dec n Int64.zero && Archi.ptr64 + then Some(w, E0, Vundef, m) + else None | _ => None end. @@ -544,45 +552,51 @@ Proof with try congruence. - eapply do_external_function_sound; eauto. } destruct ef; simpl. -(* EF_external *) +- (* EF_external *) eapply do_external_function_sound; eauto. -(* EF_builtin *) +- (* EF_builtin *) eapply BF_EX; eauto. -(* EF_runtime *) +- (* EF_runtime *) eapply BF_EX; eauto. -(* EF_vload *) +- (* EF_vload *) unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... mydestr. destruct p as [[w'' t''] v]; mydestr. exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. - auto. -(* EF_vstore *) +- (* EF_vstore *) unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... mydestr. destruct p as [[w'' t''] m'']. mydestr. exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto. - auto. -(* EF_malloc *) +- (* EF_malloc *) unfold do_ef_malloc. destruct vargs... destruct vargs... mydestr. destruct (Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned i)) as [m1 b] eqn:?. mydestr. split. apply SIZE in Heqo. subst v. econstructor; eauto. constructor. -(* EF_free *) - unfold do_ef_free. destruct vargs... destruct v... destruct vargs... - mydestr. split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. constructor. -(* EF_memcpy *) +- (* EF_free *) + unfold do_ef_free. destruct vargs... destruct v... ++ destruct vargs... mydestr; InvBooleans; subst i. + replace (Vint Int.zero) with Vnullptr. split; constructor. + apply negb_true_iff in H0. unfold Vnullptr; rewrite H0; auto. ++ destruct vargs... mydestr; InvBooleans; subst i. + replace (Vlong Int64.zero) with Vnullptr. split; constructor. + unfold Vnullptr; rewrite H0; auto. ++ destruct vargs... mydestr. + split. apply SIZE in Heqo0. econstructor; eauto. congruence. omega. + constructor. +- (* EF_memcpy *) unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... destruct v... destruct vargs... mydestr. apply Decidable_sound in Heqb1. red in Heqb1. split. econstructor; eauto; tauto. constructor. -(* EF_annot *) +- (* EF_annot *) unfold do_ef_annot. mydestr. split. constructor. apply list_eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. -(* EF_annot_val *) +- (* EF_annot_val *) unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. split. constructor. apply eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. -(* EF_inline_asm *) +- (* EF_inline_asm *) eapply do_inline_assembly_sound; eauto. -(* EF_debug *) +- (* EF_debug *) unfold do_ef_debug. mydestr. split; constructor. Qed. @@ -605,37 +619,38 @@ Proof. - eapply do_external_function_complete; eauto. } destruct ef; simpl in *. -(* EF_external *) +- (* EF_external *) eapply do_external_function_complete; eauto. -(* EF_builtin *) +- (* EF_builtin *) eapply BF_EX; eauto. -(* EF_runtime *) +- (* EF_runtime *) eapply BF_EX; eauto. -(* EF_vload *) +- (* EF_vload *) inv H; unfold do_ef_volatile_load. exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto. -(* EF_vstore *) +- (* EF_vstore *) inv H; unfold do_ef_volatile_store. exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto. -(* EF_malloc *) +- (* EF_malloc *) inv H; unfold do_ef_malloc. inv H0. erewrite SIZE by eauto. rewrite H1, H2. auto. -(* EF_free *) +- (* EF_free *) inv H; unfold do_ef_free. - inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega. -(* EF_memcpy *) ++ inv H0. rewrite H1. erewrite SIZE by eauto. rewrite zlt_true. rewrite H3. auto. omega. ++ inv H0. unfold Vnullptr; destruct Archi.ptr64; auto. +- (* EF_memcpy *) inv H; unfold do_ef_memcpy. inv H0. rewrite Decidable_complete. rewrite H7; rewrite H8; auto. red. tauto. -(* EF_annot *) +- (* EF_annot *) inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. rewrite (list_eventval_of_val_complete _ _ _ H1). auto. -(* EF_annot_val *) +- (* EF_annot_val *) inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. rewrite (eventval_of_val_complete _ _ _ H1). auto. -(* EF_inline_asm *) +- (* EF_inline_asm *) eapply do_inline_assembly_complete; eauto. -(* EF_debug *) +- (* EF_debug *) inv H. inv H0. reflexivity. Qed. -- cgit From 14f89bf9c397a4268d2b47418de234992b008d6c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Sun, 29 Mar 2020 11:35:58 +0200 Subject: Explicit error messages for ill-formed section attributes (#232) Introduce an error message for section attributes with non string arguments,and another for multiple, ambiguous section attributes. This is more consistent with the handling of other attributes, like packed, than the old behavior of silently ignoring them. --- cfrontend/C2C.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 293e79f0..7f796fe3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1234,7 +1234,7 @@ let convertFundef loc env fd = { a_storage = fd.fd_storage; a_alignment = None; a_size = None; - a_sections = Sections.for_function env id' fd.fd_attrib; + a_sections = Sections.for_function env loc id' fd.fd_attrib; a_access = Sections.Access_default; a_inline = inline; a_loc = loc }; @@ -1311,7 +1311,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = | Some i -> convertInitializer env ty i in let (section, access) = - Sections.for_variable env id' ty (optinit <> None) in + Sections.for_variable env loc id' ty (optinit <> None) in if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then error "'%s' is too big (%s bytes)" id.name (Z.to_string sz); -- cgit