diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-14 22:41:24 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-14 22:41:24 +0200 |
| commit | 4c146156a36d48209a6206f61f80dc5d4c48ce93 (patch) | |
| tree | dc8e3b1c7daf41cdf965c9e3e6119dcb5d6a41e5 | |
| parent | d03d47c6e4ce9324d6d59ae36cb8db78b013be54 (diff) | |
| parent | f995a671ceb28c2a83e5e5574c3cdb46fd5e0f57 (diff) | |
| download | compcert-4c146156a36d48209a6206f61f80dc5d4c48ce93.tar.gz compcert-4c146156a36d48209a6206f61f80dc5d4c48ce93.zip | |
Merge branch 'master' into asmexpand
51 files changed, 1046 insertions, 241 deletions
@@ -41,9 +41,9 @@ cparser/pre_parser.ml cparser/pre_parser.mli lib/Readconfig.ml lib/Tokenize.ml +driver/Version.ml # Documentation doc/coq2html doc/coq2html.ml doc/html doc/html/ - @@ -135,22 +135,22 @@ extraction/STAMP: $(FILES:.v=.vo) extraction/extraction.v $(ARCH)/extractionMach $(COQEXEC) extraction/extraction.v touch extraction/STAMP -.depend.extr: extraction/STAMP tools/modorder +.depend.extr: extraction/STAMP tools/modorder driver/Version.ml $(MAKE) -f Makefile.extr depend -ccomp: .depend.extr compcert.ini FORCE +ccomp: .depend.extr compcert.ini driver/Version.ml FORCE $(MAKE) -f Makefile.extr ccomp -ccomp.byte: .depend.extr compcert.ini FORCE +ccomp.byte: .depend.extr compcert.ini driver/Version.ml FORCE $(MAKE) -f Makefile.extr ccomp.byte -cchecklink: .depend.extr compcert.ini FORCE +cchecklink: .depend.extr compcert.ini driver/Version.ml FORCE $(MAKE) -f Makefile.extr cchecklink -cchecklink.byte: .depend.extr compcert.ini FORCE +cchecklink.byte: .depend.extr compcert.ini driver/Version.ml FORCE $(MAKE) -f Makefile.extr cchecklink.byte -clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE +clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE $(MAKE) -f Makefile.extr clightgen -clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo FORCE +clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE $(MAKE) -f Makefile.extr clightgen.byte runtime: @@ -192,7 +192,7 @@ latexdoc: @tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; } @chmod -w $*.v -compcert.ini: Makefile.config VERSION +compcert.ini: Makefile.config (echo "stdlib_path=$(LIBDIR)"; \ echo "prepro=$(CPREPRO)"; \ echo "asm=$(CASM)"; \ @@ -206,11 +206,14 @@ compcert.ini: Makefile.config VERSION echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \ echo "advanced_debug=$(ADVANCED_DEBUG)"; \ echo "struct_passing_style=$(STRUCT_PASSING)"; \ - echo "struct_return_style=$(STRUCT_RETURN)"; \ - version=`cat VERSION`; \ - echo version=$$version) \ + echo "struct_return_style=$(STRUCT_RETURN)";) \ > compcert.ini +driver/Version.ml: VERSION + cat VERSION \ + | sed -e 's|\(.*\)=\(.*\)|let \1 = \"\2\"|g' \ + >driver/Version.ml + cparser/Parser.v: cparser/Parser.vy $(MENHIR) --coq cparser/Parser.vy @@ -233,6 +236,7 @@ clean: rm -f $(patsubst %, %/*.vo, $(DIRS)) rm -rf doc/html doc/*.glob rm -f doc/coq2html.ml doc/coq2html doc/*.cm? doc/*.o + rm -f driver/Version.ml rm -f compcert.ini rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o @@ -1 +1,3 @@ -2.4 +version=2.5 +buildnr= +tag=
\ No newline at end of file diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml new file mode 100644 index 00000000..75724d43 --- /dev/null +++ b/arm/AsmToJSON.ml @@ -0,0 +1,18 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +(* Simple functions to serialize powerpc Asm to JSON *) + +(* Dummy function *) + +let p_program oc prog = + () diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index e91b4e03..f3c80f3e 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -119,7 +119,7 @@ module Printer(Target:TARGET) = let get_end_addr = Target.get_end_addr let get_stmt_list_addr = Target.get_stmt_list_addr let name_of_section = Target.name_of_section - let get_fun_addr s = Hashtbl.find addr_mapping s + let get_fun_addr s = try Some (Hashtbl.find addr_mapping s) with Not_found -> None end module DebugPrinter = DwarfPrinter (DwarfTarget) (Target.DwarfAbbrevs) diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 497760c1..b54188ca 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -294,7 +294,7 @@ let print_inline_asm print_preg oc txt sg args res = (** Print CompCert version and command-line as asm comment *) let print_version_and_options oc comment = - fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version; + fprintf oc "%s File generated by CompCert %s\n" comment Version.version; fprintf oc "%s Command line:" comment; for i = 1 to Array.length Sys.argv - 1 do fprintf oc " %s" Sys.argv.(i) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 96a497bc..b919c1d4 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -572,6 +572,7 @@ let z_of_str hex str fst = done; !res + let checkFloatOverflow f = match f with | Fappli_IEEE.B754_finite _ -> () diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 6284660c..948ccaca 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -709,8 +709,10 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) match v1,v2 with | Vptr b1 ofs1, Vptr b2 ofs2 => if eq_block b1 b2 then - 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)))) + let sz := sizeof cenv ty in + if zlt 0 sz && zle sz Int.max_signed + then Some (Vint (Int.divs (Int.sub ofs1 ofs2) (Int.repr sz))) + else None else None | _, _ => None end @@ -1216,7 +1218,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 cenv ty)) Int.zero); inv H3. + destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3. rewrite Int.sub_shifted. TrivialInject. + inv H0; inv H1; inv H. TrivialInject. econstructor. eauto. rewrite Int.sub_add_l. auto. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index cb83731a..a80f4c15 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -260,7 +260,7 @@ Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in - OK (Ebinop Odivu (Ebinop Osub e1 e2) n) + OK (Ebinop Odiv (Ebinop Osub e1 e2) n) | sub_case_pl ty => let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2))) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 025d7b66..c69d0c0a 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -490,8 +490,19 @@ Proof. 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 ce ty)) Int.zero) eqn:E; inv H0. - econstructor; eauto with cshm. rewrite dec_eq_true. simpl. rewrite E; auto. + destruct (eq_block b0 b1); try discriminate. + set (sz := sizeof ce ty) in *. + destruct (zlt 0 sz); try discriminate. + destruct (zle sz Int.max_signed); simpl in H0; inv H0. + econstructor; eauto with cshm. + rewrite dec_eq_true; simpl. + assert (E: Int.signed (Int.repr sz) = sz). + { apply Int.signed_repr. generalize Int.min_signed_neg; omega. } + predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero. + rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction. + predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone. + rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction. + rewrite andb_false_r; auto. - destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - eapply make_binarith_correct; eauto; intros; auto. Qed. diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml index c475d7da..38a420f6 100644 --- a/checklink/Asm_printers.ml +++ b/checklink/Asm_printers.ml @@ -188,7 +188,7 @@ let string_of_instruction = function | Pcmplwi (i0, c1) -> "Pcmplwi(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ")" | Pcmpw (i0, i1) -> "Pcmpw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" | Pcmpwi (i0, c1) -> "Pcmpwi(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ")" -| Pcntlz (i0, i1) -> "Pcntlz(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" +| Pcntlzw (i0, i1) -> "Pcntlzw(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ")" | Pcreqv (c0, c1, c2) -> "Pcreqv(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" | Pcror (c0, c1, c2) -> "Pcror(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" | Pcrxor (c0, c1, c2) -> "Pcrxor(" ^ string_of_crbit c0 ^ ", " ^ string_of_crbit c1 ^ ", " ^ string_of_crbit c2 ^ ")" diff --git a/checklink/Check.ml b/checklink/Check.ml index bfd03c97..0e69ab72 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -1024,7 +1024,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pcntlz(r1, r2) -> + | Pcntlzw(r1, r2) -> begin match ecode with | CNTLZWx(rS, rA, rc) :: es -> OK(fw) @@ -2573,7 +2573,7 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework) (** Read a .sdump file *) -let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version +let sdump_magic_number = "CompCertSDUMP" ^ Version.version let read_sdump file = let ic = open_in_bin file in diff --git a/checklink/Validator.ml b/checklink/Validator.ml index 6969409a..f9ca0edb 100644 --- a/checklink/Validator.ml +++ b/checklink/Validator.ml @@ -97,7 +97,7 @@ let anonymous arg = set_elf_file arg let usage = - "The CompCert C post-linking validator, version " ^ Configuration.version ^ " + "The CompCert C post-linking validator, version " ^ Version.version ^ " Usage: cchecklink [options] <.sdump files> <ELF executable> In the absence of options, checks are performed and a short result is displayed. Options are:" @@ -113,7 +113,7 @@ case "$target" in struct_return="int1-8" system="diab" cc="${toolprefix}dcc" - cprepro="${toolprefix}dcc -E" + cprepro="${toolprefix}dcc -E -D__GNUC__" casm="${toolprefix}das" asm_supports_cfi=false clinker="${toolprefix}dcc" diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml index 570572fa..6569bb4c 100644 --- a/cparser/Bitfields.ml +++ b/cparser/Bitfields.ml @@ -31,7 +31,8 @@ type bitfield_info = bf_pos: int; (* start bit *) bf_size: int; (* size in bit *) bf_signed: bool; (* is field signed or unsigned? *) - bf_signed_res: bool (* is result of extracting field signed or unsigned? *) + bf_signed_res: bool; (* is result of extracting field signed or unsigned? *) + bf_bool: bool (* does field have type _Bool? *) } (* invariants: @@ -100,7 +101,13 @@ let pack_bitfields env sid ml = match unroll env (type_of_member env m) with | TInt(ik, _) -> is_signed_ikind ik | _ -> assert false (* should never happen, checked in Elab *) in - pack ((m.fld_name, pos, n, signed, signed2) :: accu) (pos + n) ms + let is_bool = + match unroll env m.fld_typ with + | TInt(IBool, _) -> true + | _ -> false in + + pack ((m.fld_name, pos, n, signed, signed2, is_bool) :: accu) + (pos + n) ms end in pack [] 0 ml @@ -121,7 +128,7 @@ let rec transf_members env id count = function let carrier_typ = TInt(carrier_ikind, []) in (* Enter each field with its bit position, size, signedness *) List.iter - (fun (name, pos, sz, signed, signed2) -> + (fun (name, pos, sz, signed, signed2, is_bool) -> if name <> "" then begin let pos' = if !config.bitfields_msb_first @@ -131,7 +138,8 @@ let rec transf_members env id count = function (id, name) {bf_carrier = carrier; bf_carrier_typ = carrier_typ; bf_pos = pos'; bf_size = sz; - bf_signed = signed; bf_signed_res = signed2} + bf_signed = signed; bf_signed_res = signed2; + bf_bool = is_bool} end) bitfields; { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None} @@ -208,13 +216,16 @@ unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y) return (x & ~mask) | ((y << ofs) & mask); } +If the bitfield is of type _Bool, the new value (y above) must be converted +to _Bool to normalize it to 0 or 1. *) 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 + ecast (TInt(IUInt,[])) + (if bf.bf_bool then ecast (TInt(IBool,[])) newval else newval) in let newval_shifted = eshift env Oshl newval_casted (intconst (Int64.of_int bf.bf_pos) IUInt) in let newval_masked = ebinint env Oand newval_shifted msk @@ -230,17 +241,22 @@ unsigned int bitfield_init(int ofs, int sz, unsigned int y) unsigned int mask = (1U << sz) - 1; return (y & mask) << ofs; } + +If the bitfield is of type _Bool, the new value (y above) must be converted +to _Bool to normalize it to 0 or 1. *) let bitfield_initializer bf i = match i with | Init_single e -> let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in + let e_cast = + if bf.bf_bool then ecast (TInt(IBool,[])) e else e in let e_mask = {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m)); etyp = TInt(IUInt, [])} in let e_and = - {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[])); + {edesc = EBinop(Oand, e_cast, e_mask, TInt(IUInt,[])); etyp = TInt(IUInt,[])} in {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt, TInt(IUInt, [])); diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 221bd7cc..a3c05c34 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -721,7 +721,8 @@ let type_of_member env fld = let find_matching_unsigned_ikind sz = assert (sz > 0); - if sz = !config.sizeof_int then IUInt + if sz = !config.sizeof_short then IUShort + else if sz = !config.sizeof_int then IUInt else if sz = !config.sizeof_long then IULong else if sz = !config.sizeof_longlong then IULongLong else assert false diff --git a/cparser/Elab.ml b/cparser/Elab.ml index d6b79780..9ff7823f 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1805,7 +1805,12 @@ let enter_or_refine_ident local loc env s sto ty = | Some new_ty -> new_ty | None -> - warning loc "redefinition of '%s' with incompatible type" s; ty in + error loc + "redefinition of '%s' with incompatible type.@ \ + Previous type: %a.@ \ + New type: %a" + s Cprint.typ old_ty Cprint.typ ty; + ty in let new_sto = (* The only case not allowed is removing static *) match old_sto,sto with @@ -1822,12 +1827,12 @@ let enter_or_refine_ident local loc env s sto ty = | _,Storage_register | Storage_register,_ -> Storage_register in - (id, new_sto, Env.add_ident env id new_sto new_ty) + (id, new_sto, Env.add_ident env id new_sto new_ty,new_ty) | Some(id, II_enum v) when Env.in_current_scope env id -> error loc "redefinition of enumerator '%s'" s; - (id, sto, Env.add_ident env id sto ty) + (id, sto, Env.add_ident env id sto ty,ty) | _ -> - let (id, env') = Env.enter_ident env s sto ty in (id, sto, env') + let (id, env') = Env.enter_ident env s sto ty in (id, sto, env',ty) let enter_decdefs local loc env sto dl = (* Sanity checks on storage class *) @@ -1845,7 +1850,7 @@ let enter_decdefs local loc env sto dl = let sto1 = if local && isfun then Storage_extern else sto in (* enter ident in environment with declared type, because initializer can refer to the ident *) - let (id, sto', env1) = enter_or_refine_ident local loc env s sto1 ty in + let (id, sto', env1,ty) = enter_or_refine_ident local loc env s sto1 ty in (* process the initializer *) let (ty', init') = elab_initializer loc env1 s ty init in (* update environment with refined type *) @@ -1882,18 +1887,30 @@ let elab_fundef env spec name body loc = | TFun(ty_ret, Some params, vararg, attr) -> (ty_ret, params, vararg, attr) | _ -> fatal_error loc "wrong type for function definition" in (* Enter function in the environment, for recursive references *) - let (fun_id, sto1, env1) = enter_or_refine_ident false loc env s sto ty in + let (fun_id, sto1, env1,ty) = enter_or_refine_ident false loc env1 s sto ty in (* Enter parameters in the environment *) let env2 = List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty) (Env.new_scope env1) params in (* Define "__func__" and enter it in the environment *) let (func_ty, func_init) = __func__type_and_init s in - let (func_id, _, env3) = + let (func_id, _, env3,func_ty) = enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in emit_elab loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) let body' = !elab_funbody_f ty_ret env3 body in + (* Special treatment of the "main" function *) + let body'' = + if s = "main" then begin + match unroll env ty_ret with + | TInt(IInt, []) -> + (* Add implicit "return 0;" at end of function body *) + sseq no_loc body' + {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc} + | _ -> + warning loc "return type of 'main' should be 'int'"; + body' + end else body' in (* Build and emit function definition *) let fn = { fd_storage = sto1; @@ -1904,7 +1921,7 @@ let elab_fundef env spec name body loc = fd_params = params; fd_vararg = vararg; fd_locals = []; - fd_body = body' } in + fd_body = body'' } in emit_elab loc (Gfundef fn); env1 diff --git a/cparser/Machine.ml b/cparser/Machine.ml index bd6489fd..7a12c649 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -170,6 +170,10 @@ let ppc_32_bigendian = bitfields_msb_first = true; supports_unaligned_accesses = true } +let ppc_32_diab_bigendian = + { ppc_32_bigendian with sizeof_wchar = 2; wchar_signed = false } + + let arm_littleendian = { ilp32ll64 with name = "arm" } diff --git a/cparser/Machine.mli b/cparser/Machine.mli index fb7321f9..277ac3fb 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -62,6 +62,7 @@ val x86_64 : t val win32 : t val win64 : t val ppc_32_bigendian : t +val ppc_32_diab_bigendian : t val arm_littleendian : t val gcc_extensions : t -> t diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 317847a7..c9564c08 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -29,7 +29,7 @@ let transform_program t p name = Some (CtoDwarf.program_to_dwarf p p1 name) else None in - (Rename.program p1),debug + (Rename.program p1 (Filename.chop_suffix name ".c")),debug let parse_transformations s = let t = ref CharSet.empty in diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 0d533b56..cf82bc9f 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -42,6 +42,16 @@ let enter_public env id = { re_id = IdentMap.add id id env.re_id; re_public = StringMap.add id.name id env.re_public; re_used = StringSet.add id.name env.re_used } + +let enter_static env id file = + try + let id' = StringMap.find id.name env.re_public in + { env with re_id = IdentMap.add id id' env.re_id } + with Not_found -> + let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in + { re_id = IdentMap.add id id' env.re_id; + re_public = env.re_public; + re_used = StringSet.add id'.name env.re_used } (* For static or local identifiers, we make up a new name if needed *) (* If the same identifier has already been declared, @@ -249,7 +259,7 @@ let reserve_builtins () = (* Reserve global declarations with public visibility *) -let rec reserve_public env = function +let rec reserve_public env file = function | [] -> env | dcl :: rem -> let env' = @@ -257,22 +267,28 @@ let rec reserve_public env = function | Gdecl(sto, id, _, _) -> begin match sto with | Storage_default | Storage_extern -> enter_public env id - | Storage_static -> env + | Storage_static -> if !Clflags.option_rename_static then + enter_static env id file + else + env | _ -> assert false end | Gfundef f -> begin match f.fd_storage with | Storage_default | Storage_extern -> enter_public env f.fd_name - | Storage_static -> env + | Storage_static -> if !Clflags.option_rename_static then + enter_static env f.fd_name file + else + env | _ -> assert false end | _ -> env in - reserve_public env' rem + reserve_public env' file rem (* Rename the program *) -let program p = +let program p file = globdecls - (reserve_public (reserve_builtins()) p) + (reserve_public (reserve_builtins()) file p) [] p diff --git a/cparser/Rename.mli b/cparser/Rename.mli index 818a51bc..c4ef2228 100644 --- a/cparser/Rename.mli +++ b/cparser/Rename.mli @@ -13,4 +13,4 @@ (* *) (* *********************************************************************) -val program : C.program -> C.program +val program : C.program -> string -> C.program diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml index 660f1d9b..5e5602f3 100644 --- a/cparser/StructReturn.ml +++ b/cparser/StructReturn.ml @@ -299,10 +299,15 @@ let rec transf_expr env ctx e = transf_call env ctx None fn args e.etyp (* Function calls returning a composite by reference: add first argument. - ctx = Effects: lv = f(...) -> f(&lv, ...) [copy optimization] + ctx = Effects: lv = f(...) -> f(&newtemp, ...), lv = newtemp f(...) -> f(&newtemp, ...) ctx = Val: lv = f(...) -> f(&newtemp, ...), lv = newtemp f(...) -> f(&newtemp, ...), newtemp + + We used to do a copy optimization: + ctx = Effects: lv = f(...) -> f(&lv, ...) + but it is not correct in case of overlap (see test/regression/struct12.c) + Function calls returning a composite by value: ctx = Effects: lv = f(...) -> newtemp = f(...), lv = newtemp f(...) -> f(...) @@ -332,13 +337,14 @@ and transf_call env ctx opt_lhs fn args ty = | Effects, None -> let tmp = new_temp ~name:"_res" ty in {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} - | Effects, Some lhs -> - {edesc = ECall(fn', eaddrof lhs :: args'); etyp = TVoid []} + (* Copy optimization, turned off as explained above *) + (* | Effects, Some lhs -> + {edesc = ECall(fn', eaddrof lhs :: args'); etyp = TVoid []} *) | Val, None -> let tmp = new_temp ~name:"_res" ty in ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} tmp - | Val, Some lhs -> + | _, Some lhs -> let tmp = new_temp ~name:"_res" ty in ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []} (eassign lhs tmp) diff --git a/cparser/validator/Tuples.v b/cparser/validator/Tuples.v index 88dc46e9..3fd2ec03 100644 --- a/cparser/validator/Tuples.v +++ b/cparser/validator/Tuples.v @@ -26,8 +26,11 @@ Definition arrows_right: Type -> list Type -> Type := fold_right (fun A B => A -> B). (** A tuple is a heterogeneous list. For convenience, we use pairs. **) -Definition tuple (types:list Type) : Type := - fold_right prod unit types. +Fixpoint tuple (types : list Type) : Type := + match types with + | nil => unit + | t::q => prod t (tuple q) + end. Fixpoint uncurry {args:list Type} {res:Type}: arrows_left args res -> tuple args -> res := diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml index a352e99f..cead6099 100644 --- a/debug/CtoDwarf.ml +++ b/debug/CtoDwarf.ml @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +open Builtins open C open Cprint open Cutil @@ -17,6 +18,7 @@ open C2C open DwarfTypes open DwarfUtil open Env +open Set (* Functions to translate a C Ast into Dwarf 2 debugging information *) @@ -28,10 +30,18 @@ let type_table: (string, int) Hashtbl.t = Hashtbl.create 7 let typedef_table: (string, int) Hashtbl.t = Hashtbl.create 7 (* Hashtable from composite table to entry id *) -let composite_types_table: (string, int) Hashtbl.t = Hashtbl.create 7 +let composite_types_table: (int, int) Hashtbl.t = Hashtbl.create 7 + +(* Hashtable from id of a defined composite types to minimal type info *) +let composite_declarations: (int, (struct_or_union * string * location)) Hashtbl.t = Hashtbl.create 7 + +module IntSet = Set.Make(struct type t = int let compare = compare end) + +(* Set of all declared composite_types *) +let composite_defined: IntSet.t ref = ref IntSet.empty (* Get the type id of a composite_type *) -let get_composite_type (name: string): int = +let get_composite_type (name: int): int = try Hashtbl.find composite_types_table name with Not_found -> @@ -231,7 +241,7 @@ and type_to_dwarf_entry typ typ_string= | TStruct (i,_) | TUnion (i,_) | TEnum (i,_) -> - let t = get_composite_type i.name in + let t = get_composite_type i.stamp in t,[] | TNamed (i,at) -> let t = Hashtbl.find typedef_table i.name in @@ -270,12 +280,12 @@ and type_to_dwarf (typ: typ): int * dw_entry list = attr_type_to_dwarf typ typ_string (* Translate a typedef to its corresponding dwarf representation *) -let typedef_to_dwarf (n,t) gloc = +let typedef_to_dwarf gloc (name,t) = let i,t = type_to_dwarf t in - Hashtbl.add typedef_table n.name i; + Hashtbl.add typedef_table name i; let td = { - typedef_file_loc = Some (gloc); - typedef_name = n.name; + typedef_file_loc = gloc; + typedef_name = name; typedef_type = i; } in let td = new_entry (DW_TAG_typedef td) in @@ -352,9 +362,9 @@ let enum_to_dwarf (n,at,e) gloc = enumeration_file_loc = Some gloc; enumeration_byte_size = bs; enumeration_declaration = Some false; - enumeration_name = n.name; + enumeration_name = if n.name <> "" then Some n.name else None; } in - let id = get_composite_type n.name in + let id = get_composite_type n.stamp in let child = List.map enumerator_to_dwarf e in let enum = { @@ -371,9 +381,9 @@ let struct_to_dwarf (n,at,m) env gloc = structure_file_loc = Some gloc; structure_byte_size = info.ci_sizeof; structure_declaration = Some false; - structure_name = n.name; + structure_name = if n.name <> "" then Some n.name else None; } in - let id = get_composite_type n.name in + let id = get_composite_type n.stamp in let rec pack acc bcc l m = match m with | [] -> acc,bcc,[] @@ -394,7 +404,7 @@ let struct_to_dwarf (n,at,m) env gloc = member_bit_size = Some n; member_data_member_location = None; member_declaration = None; - member_name = m.fld_name; + member_name = if m.fld_name <> "" then Some m.fld_name else None; member_type = t; } in pack ((new_entry (DW_TAG_member um))::acc) (e@bcc) (l + n) ms) @@ -412,7 +422,7 @@ let struct_to_dwarf (n,at,m) env gloc = member_bit_size = None; member_data_member_location = None; member_declaration = None; - member_name = m.fld_name; + member_name = if m.fld_name <> "" then Some m.fld_name else None; member_type = t; } in translate ((new_entry (DW_TAG_member um))::acc) (e@bcc) ms @@ -434,9 +444,9 @@ let union_to_dwarf (n,at,m) env gloc = union_file_loc = Some gloc; union_byte_size = info.ci_sizeof; union_declaration = Some false; - union_name = n.name; + union_name = if n.name <> "" then Some n.name else None; } in - let id = get_composite_type n.name in + let id = get_composite_type n.stamp in let children,e = mmap (fun acc f -> let t,e = type_to_dwarf f.fld_typ in @@ -447,7 +457,7 @@ let union_to_dwarf (n,at,m) env gloc = member_bit_size = None; member_data_member_location = None; member_declaration = None; - member_name = f.fld_name; + member_name = if f.fld_name <> "" then Some f.fld_name else None; member_type = t; } in new_entry (DW_TAG_member um),e@acc)[] m in @@ -461,21 +471,48 @@ let union_to_dwarf (n,at,m) env gloc = let globdecl_to_dwarf env (typs,decls) decl = PrintAsmaux.add_file (fst decl.gloc); match decl.gdesc with - | Gtypedef (n,t) -> let ret = typedef_to_dwarf (n,t) decl.gloc in + | Gtypedef (n,t) -> let ret = typedef_to_dwarf (Some decl.gloc) (n.name,t) in typs@ret,decls | Gdecl d -> let t,d = glob_var_to_dwarf d decl.gloc in typs@t,d::decls | Gfundef f -> let t,d = fundef_to_dwarf f decl.gloc in typs@t,d::decls - | Genumdef (n,at,e) ->let ret = enum_to_dwarf (n,at,e) decl.gloc in - typs@ret,decls - | Gcompositedef (Struct,n,at,m) -> let ret = struct_to_dwarf (n,at,m) env decl.gloc in - typs@ret,decls - | Gcompositedef (Union,n,at,m) -> let ret = union_to_dwarf (n,at,m) env decl.gloc in - typs@ret,decls - | Gcompositedecl _ + | Genumdef (n,at,e) -> + composite_defined:= IntSet.add n.stamp !composite_defined; + let ret = enum_to_dwarf (n,at,e) decl.gloc in + typs@ret,decls + | Gcompositedef (Struct,n,at,m) -> + composite_defined:= IntSet.add n.stamp !composite_defined; + let ret = struct_to_dwarf (n,at,m) env decl.gloc in + typs@ret,decls + | Gcompositedef (Union,n,at,m) -> + composite_defined:= IntSet.add n.stamp !composite_defined; + let ret = union_to_dwarf (n,at,m) env decl.gloc in + typs@ret,decls + | Gcompositedecl (sou,i,_) -> Hashtbl.add composite_declarations i.stamp (sou,i.name,decl.gloc); + typs,decls | Gpragma _ -> typs,decls +let forward_declaration_to_dwarf sou name loc stamp = + let id = get_composite_type stamp in + let tag = match sou with + | Struct -> + DW_TAG_structure_type{ + structure_file_loc = Some loc; + structure_byte_size = None; + structure_declaration = Some true; + structure_name = if name <> "" then Some name else None; + } + | Union -> + DW_TAG_union_type { + union_file_loc = Some loc; + union_byte_size = None; + union_declaration = Some true; + union_name = if name <> "" then Some name else None; + } in + {tag = tag; children = []; id = id} + + (* Compute the dwarf representations of global declarations. The second program argument is the program after the bitfield and packed struct transformation *) let program_to_dwarf prog prog1 name = @@ -485,8 +522,12 @@ let program_to_dwarf prog prog1 name = let prog = cleanupGlobals (prog) in let env = translEnv Env.empty prog1 in reset_id (); - let typs,defs = List.fold_left (globdecl_to_dwarf env) ([],[]) prog in - let defs = typs @ defs in + let typs = List.map (typedef_to_dwarf None) C2C.builtins.typedefs in + let typs = List.concat typs in + let typs,defs = List.fold_left (globdecl_to_dwarf env) (typs,[]) prog in + let typs = Hashtbl.fold (fun i (sou,name,loc) typs -> if not (IntSet.mem i !composite_defined) then + (forward_declaration_to_dwarf sou name loc i)::typs else typs) composite_declarations typs in + let defs = typs @ defs in let cp = { compile_unit_name = name; } in diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 13d4049e..9e565ee4 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -62,6 +62,11 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): let add_low_pc = add_abbr_entry (0x11,low_pc_type_abbr) + let add_fun_pc sp buf = + match get_fun_addr sp.subprogram_name with + | None ->() + | Some (a,b) -> add_high_pc buf; add_low_pc buf + let add_declaration = add_abbr_entry (0x3c,declaration_type_abbr) let add_location loc buf = @@ -112,7 +117,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): add_attr_some e.enumeration_file_loc add_file_loc; add_byte_size buf; add_attr_some e.enumeration_declaration add_declaration; - add_name buf + add_attr_some e.enumeration_name add_name | DW_TAG_enumerator e -> prologue 0x28; add_attr_some e.enumerator_file_loc add_file_loc; @@ -146,7 +151,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): | Some (DataLocBlock __) -> add_abbr_entry (0x38,data_location_block_type_abbr) buf | Some (DataLocRef _) -> add_abbr_entry (0x38,data_location_ref_type_abbr) buf); add_attr_some e.member_declaration add_declaration; - add_name buf; + add_attr_some e.member_name add_name; add_type buf | DW_TAG_pointer_type _ -> prologue 0xf; @@ -156,7 +161,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): add_attr_some e.structure_file_loc add_file_loc; add_attr_some e.structure_byte_size add_byte_size; add_attr_some e.structure_declaration add_declaration; - add_name buf + add_attr_some e.structure_name add_name | DW_TAG_subprogram e -> prologue 0x2e; add_attr_some e.subprogram_file_loc add_file_loc; @@ -187,7 +192,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): add_attr_some e.union_file_loc add_file_loc; add_attr_some e.union_byte_size add_byte_size; add_attr_some e.union_declaration add_declaration; - add_name buf + add_attr_some e.union_name add_name | DW_TAG_unspecified_parameter e -> prologue 0x18; add_attr_some e.unspecified_parameter_file_loc add_file_loc; @@ -328,7 +333,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_string oc bt.base_type_name let print_compilation_unit oc tag = - let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Configuration.version Configuration.arch in + let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Version.version Configuration.arch in print_string oc (Sys.getcwd ()); print_addr oc (get_start_addr ()); print_addr oc (get_end_addr ()); @@ -344,7 +349,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_file_loc oc et.enumeration_file_loc; print_uleb128 oc et.enumeration_byte_size; print_opt_value oc et.enumeration_declaration print_flag; - print_string oc et.enumeration_name + print_opt_value oc et.enumeration_name print_string let print_enumerator oc en = print_file_loc oc en.enumerator_file_loc; @@ -375,7 +380,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_opt_value oc mb.member_bit_size print_byte; print_opt_value oc mb.member_data_member_location print_data_location; print_opt_value oc mb.member_declaration print_flag; - print_string oc mb.member_name; + print_opt_value oc mb.member_name print_string; print_ref oc mb.member_type let print_pointer oc pt = @@ -385,15 +390,18 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_file_loc oc st.structure_file_loc; print_opt_value oc st.structure_byte_size print_uleb128; print_opt_value oc st.structure_declaration print_flag; - print_string oc st.structure_name + print_opt_value oc st.structure_name print_string + let print_subprogram_addr oc (s,e) = + fprintf oc " .4byte %a\n" label s; + fprintf oc " .4byte %a\n" label e + let print_subprogram oc sp = - let s,e = get_fun_addr sp.subprogram_name in + let addr = get_fun_addr sp.subprogram_name in print_file_loc oc sp.subprogram_file_loc; print_opt_value oc sp.subprogram_external print_flag; print_opt_value oc sp.subprogram_frame_base print_loc; - fprintf oc " .4byte %a\n" label s; - fprintf oc " .4byte %a\n" label e; + print_opt_value oc addr print_subprogram_addr; print_string oc sp.subprogram_name; print_flag oc sp.subprogram_prototyped; print_opt_value oc sp.subprogram_type print_ref @@ -415,7 +423,7 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS): print_file_loc oc ut.union_file_loc; print_opt_value oc ut.union_byte_size print_uleb128; print_opt_value oc ut.union_declaration print_flag; - print_string oc ut.union_name + print_opt_value oc ut.union_name print_string let print_unspecified_parameter oc up = print_file_loc oc up.unspecified_parameter_file_loc; diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index c02558b5..d6592bd9 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -80,7 +80,7 @@ type dw_tag_enumeration_type = enumeration_file_loc: file_loc option; enumeration_byte_size: constant; enumeration_declaration: flag option; - enumeration_name: string; + enumeration_name: string option; } type dw_tag_enumerator = @@ -121,7 +121,7 @@ type dw_tag_member = member_bit_size: constant option; member_data_member_location: data_location_value option; member_declaration: flag option; - member_name: string; + member_name: string option; member_type: reference; } @@ -135,7 +135,7 @@ type dw_tag_structure_type = structure_file_loc: file_loc option; structure_byte_size: constant option; structure_declaration: flag option; - structure_name: string; + structure_name: string option; } type dw_tag_subprogram = @@ -172,7 +172,7 @@ type dw_tag_union_type = union_file_loc: file_loc option; union_byte_size: constant option; union_declaration: flag option; - union_name: string; + union_name: string option; } type dw_tag_unspecified_parameter = @@ -268,5 +268,5 @@ module type DWARF_TARGET= val get_end_addr: unit -> int val get_stmt_list_addr: unit -> int val name_of_section: section_name -> string - val get_fun_addr: string -> int * int + val get_fun_addr: string -> (int * int) option end diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 8899c2b0..d9c21a9c 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -59,3 +59,4 @@ let option_small_data = then 8 else 0) let option_small_const = ref (!option_small_data) let option_timings = ref false +let option_rename_static = ref false diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 70131fc6..64f24820 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -104,7 +104,6 @@ let advanced_debug = | "false" -> false | v -> bad_config "advanced_debug" [v] -let version = get_config_string "version" type struct_passing_style = | SP_ref_callee (* by reference, callee takes copy *) diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 72810456..f82ce213 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -36,8 +36,6 @@ val has_standard_headers: bool val advanced_debug: bool (** True if advanced debug is implement for the Target *) -val version: string - (** CompCert version string *) type struct_passing_style = | SP_ref_callee (* by reference, callee takes copy *) diff --git a/driver/Driver.ml b/driver/Driver.ml index 805d5405..1dce08ac 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -145,7 +145,7 @@ let parse_c_file sourcename ifile = (* Dump Asm code in binary format for the validator *) -let sdump_magic_number = "CompCertSDUMP" ^ Configuration.version +let sdump_magic_number = "CompCertSDUMP" ^ Version.version let dump_asm asm destfile = let oc = open_out_bin destfile in @@ -155,6 +155,15 @@ let dump_asm asm destfile = output_value oc C2C.decl_atom; close_out oc +let jdump_magic_number = "CompCertJDUMP" ^ Version.version + +let dump_jasm asm destfile = + let oc = open_out_bin destfile in + fprintf oc "{\n\"Version\":\"%s\",\n\"Asm Ast\":%a}" + jdump_magic_number AsmToJSON.p_program asm; + close_out oc + + (* From CompCert C AST to asm *) let compile_c_ast sourcename csyntax ofile debug = @@ -176,9 +185,12 @@ let compile_c_ast sourcename csyntax ofile debug = | Errors.Error msg -> print_error stderr msg; exit 2 in - (* Dump Asm in binary format *) + (* Dump Asm in binary and JSON format *) if !option_sdump then - dump_asm asm (output_filename sourcename ".c" ".sdump"); + begin + dump_asm asm (output_filename sourcename ".c" ".sdump"); + dump_jasm asm (output_filename sourcename ".c" ".json") + end; (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm debug; @@ -387,7 +399,10 @@ let explode_comma_option s = | hd :: tl -> tl let version_string = - "The CompCert C verified compiler, version "^ Configuration.version ^ "\n" + if Version.buildnr <> "" && Version.tag <> "" then + sprintf "The CompCert verified compiler, %s, Build: %s, Tag: %s\n" Version.version Version.buildnr Version.tag + else + "The CompCert C verified compiler, version "^ Version.version ^ "\n" let usage_string = version_string ^ @@ -426,6 +441,7 @@ Language support options (use -fno-<opt> to turn off -f<opt>) : -fnone Turn off all language support options above Debugging options: -g Generate debugging information + -frename-static Rename static functions and declarations Optimization options: (use -fno-<opt> to turn off -f<opt>) -O Optimize the compiled code [on by default] -O0 Do not optimize the compiled code @@ -528,6 +544,7 @@ let cmdline_actions = Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) Exact "-g", Self (fun s -> option_g := true); + Exact "-frename-static", Self (fun s -> option_rename_static:= true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); Exact "-O", Self (fun _ -> set_all optimization_options); @@ -644,7 +661,9 @@ let _ = Printexc.record_backtrace true; Machine.config := begin match Configuration.arch with - | "powerpc" -> Machine.ppc_32_bigendian + | "powerpc" -> if Configuration.system = "linux" + then Machine.ppc_32_bigendian + else Machine.ppc_32_diab_bigendian | "arm" -> Machine.arm_littleendian | "ia32" -> if Configuration.abi = "macosx" then Machine.x86_32_macosx diff --git a/ia32/AsmToJSON.ml b/ia32/AsmToJSON.ml new file mode 100644 index 00000000..de39cb9d --- /dev/null +++ b/ia32/AsmToJSON.ml @@ -0,0 +1,17 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +(* Simple functions to serialize powerpc Asm to JSON *) + +(* Dummy function *) +let p_program oc prog = + () diff --git a/lib/Fappli_IEEE_extra.v b/lib/Fappli_IEEE_extra.v index 92ed11ae..3de7b103 100644 --- a/lib/Fappli_IEEE_extra.v +++ b/lib/Fappli_IEEE_extra.v @@ -1110,6 +1110,224 @@ Proof. + erewrite NAN; eauto. Qed. +(** ** Conversion from scientific notation *) + +(** Russian peasant exponentiation *) + +Fixpoint pos_pow (x y: positive) : positive := + match y with + | xH => x + | xO y => Pos.square (pos_pow x y) + | xI y => Pos.mul x (Pos.square (pos_pow x y)) + end. + +Lemma pos_pow_spec: + forall x y, Z.pos (pos_pow x y) = Z.pos x ^ Z.pos y. +Proof. + intros x. + assert (REC: forall y a, Pos.iter y (Pos.mul x) a = Pos.mul (pos_pow x y) a). + { induction y; simpl; intros. + - rewrite ! IHy, Pos.square_spec, ! Pos.mul_assoc. auto. + - rewrite ! IHy, Pos.square_spec, ! Pos.mul_assoc. auto. + - auto. + } + intros. simpl. rewrite <- Pos2Z.inj_pow_pos. unfold Pos.pow. rewrite REC. rewrite Pos.mul_1_r. auto. +Qed. + +(** Given a base [base], a mantissa [m] and an exponent [e], the following function + computes the FP number closest to [m * base ^ e], using round to odd, ties break to even. + The algorithm is naive, computing [base ^ |e|] exactly before doing a multiplication or + division with [m]. However, we treat specially very large or very small values of [e], + when the result is known to be [+infinity] or [0.0] respectively. *) + +Definition Bparse (base: positive) (m: positive) (e: Z): binary_float := + match e with + | Z0 => + BofZ (Zpos m) + | Zpos p => + if e * Z.log2 (Zpos base) <? emax + then BofZ (Zpos m * Zpos (pos_pow base p)) + else B754_infinity _ _ false + | Zneg p => + if e * Z.log2 (Zpos base) + Z.log2_up (Zpos m) <? emin + then B754_zero _ _ false + else FF2B prec emax _ (proj1 (Bdiv_correct_aux prec emax prec_gt_0_ Hmax mode_NE + false m Z0 false (pos_pow base p) Z0)) + end. + +(** Properties of [Z.log2] and [Z.log2_up]. *) + +Lemma Zpower_log: + forall (base: radix) n, + 0 < n -> + 2 ^ (n * Z.log2 base) <= base ^ n <= 2 ^ (n * Z.log2_up base). +Proof. + intros. + assert (A: 0 < base) by apply radix_gt_0. + assert (B: 0 <= Z.log2 base) by apply Z.log2_nonneg. + assert (C: 0 <= Z.log2_up base) by apply Z.log2_up_nonneg. + destruct (Z.log2_spec base) as [D E]; auto. + destruct (Z.log2_up_spec base) as [F G]. apply radix_gt_1. + assert (K: 0 <= 2 ^ Z.log2 base) by (apply Z.pow_nonneg; omega). + rewrite ! (Zmult_comm n). rewrite ! Z.pow_mul_r by omega. + split; apply Z.pow_le_mono_l; omega. +Qed. + +Lemma bpow_log_pos: + forall (base: radix) n, + 0 < n -> + (bpow radix2 (n * Z.log2 base)%Z <= bpow base n)%R. +Proof. + intros. rewrite <- ! Z2R_Zpower. apply Z2R_le; apply Zpower_log; auto. + omega. + rewrite Zmult_comm; apply Zmult_gt_0_le_0_compat. omega. apply Z.log2_nonneg. +Qed. + +Lemma bpow_log_neg: + forall (base: radix) n, + n < 0 -> + (bpow base n <= bpow radix2 (n * Z.log2 base)%Z)%R. +Proof. + intros. set (m := -n). replace n with (-m) by (unfold m; omega). + rewrite ! Z.mul_opp_l, ! bpow_opp. apply Rinv_le. + apply bpow_gt_0. + apply bpow_log_pos. unfold m; omega. +Qed. + +(** Overflow and underflow conditions. *) + +Lemma round_integer_overflow: + forall (base: radix) e m, + 0 < e -> + emax <= e * Z.log2 base -> + (bpow radix2 emax <= round radix2 fexp (round_mode mode_NE) (Z2R (Zpos m) * bpow base e))%R. +Proof. + intros. + rewrite <- (round_generic radix2 fexp (round_mode mode_NE) (bpow radix2 emax)); auto. + apply round_le; auto. apply fexp_correct; auto. apply valid_rnd_round_mode. + rewrite <- (Rmult_1_l (bpow radix2 emax)). apply Rmult_le_compat. + apply Rle_0_1. + apply bpow_ge_0. + apply (Z2R_le 1). zify; omega. + eapply Rle_trans. eapply bpow_le. eassumption. apply bpow_log_pos; auto. + apply generic_format_FLT. exists (Float radix2 1 emax). + split. unfold F2R; simpl. ring. + split. simpl. apply (Zpower_gt_1 radix2); auto. + simpl. unfold emin; red in prec_gt_0_; omega. +Qed. + +Lemma round_NE_underflows: + forall x, + (0 <= x <= bpow radix2 (emin - 1))%R -> + round radix2 fexp (round_mode mode_NE) x = 0%R. +Proof. + intros. + set (eps := bpow radix2 (emin - 1)) in *. + assert (A: round radix2 fexp (round_mode mode_NE) eps = 0%R). + { unfold round. simpl. + assert (E: canonic_exp radix2 fexp eps = emin). + { unfold canonic_exp, eps. rewrite ln_beta_bpow. unfold fexp, FLT_exp. zify; red in prec_gt_0_; omega. } + unfold scaled_mantissa; rewrite E. + assert (P: (eps * bpow radix2 (-emin) = / 2)%R). + { unfold eps. rewrite <- bpow_plus. replace (emin - 1 + -emin) with (-1) by omega. auto. } + rewrite P. unfold Znearest. + assert (F: Zfloor (/ 2)%R = 0). + { apply Zfloor_imp. + split. apply Rlt_le. apply Rinv_0_lt_compat. apply (Z2R_lt 0 2). omega. + change (Z2R (0 + 1)) with 1%R. rewrite <- Rinv_1 at 3. apply Rinv_1_lt_contravar. apply Rle_refl. apply (Z2R_lt 1 2). omega. + } + rewrite F. change (Z2R 0) with 0%R. rewrite Rminus_0_r. rewrite Rcompare_Eq by auto. + simpl. unfold F2R; simpl. apply Rmult_0_l. + } + apply Rle_antisym. +- rewrite <- A. apply round_le. apply fexp_correct; auto. apply valid_rnd_round_mode. tauto. +- rewrite <- (round_0 radix2 fexp (round_mode mode_NE)). + apply round_le. apply fexp_correct; auto. apply valid_rnd_round_mode. tauto. +Qed. + +Lemma round_integer_underflow: + forall (base: radix) e m, + e < 0 -> + e * Z.log2 base + Z.log2_up (Zpos m) < emin -> + round radix2 fexp (round_mode mode_NE) (Z2R (Zpos m) * bpow base e) = 0%R. +Proof. + intros. apply round_NE_underflows. split. +- apply Rmult_le_pos. apply (Z2R_le 0). zify; omega. apply bpow_ge_0. +- apply Rle_trans with (bpow radix2 (Z.log2_up (Z.pos m) + e * Z.log2 base)). ++ rewrite bpow_plus. apply Rmult_le_compat. + apply (Z2R_le 0); zify; omega. + apply bpow_ge_0. + rewrite <- Z2R_Zpower. apply Z2R_le. + destruct (Z.eq_dec (Z.pos m) 1). + rewrite e0. simpl. omega. + apply Z.log2_up_spec. zify; omega. + apply Z.log2_up_nonneg. + apply bpow_log_neg. auto. ++ apply bpow_le. omega. +Qed. + +(** Correctness of Bparse *) + +Theorem Bparse_correct: + forall b m e (BASE: 2 <= Zpos b), + let base := {| radix_val := Zpos b; radix_prop := Zle_imp_le_bool _ _ BASE |} in + let r := round radix2 fexp (round_mode mode_NE) (Z2R (Zpos m) * bpow base e) in + if Rlt_bool (Rabs r) (bpow radix2 emax) then + B2R _ _ (Bparse b m e) = r + /\ is_finite _ _ (Bparse b m e) = true + /\ Bsign _ _ (Bparse b m e) = false + else + B2FF _ _ (Bparse b m e) = F754_infinity false. +Proof. + intros. + assert (A: forall x, @F2R radix2 {| Fnum := x; Fexp := 0 |} = Z2R x). + { intros. unfold F2R, Fnum; simpl. ring. } + unfold Bparse, r. destruct e as [ | e | e]. +- (* e = Z0 *) + change (bpow base 0) with 1%R. rewrite Rmult_1_r. + exact (BofZ_correct (Z.pos m)). +- (* e = Zpos e *) + destruct (Z.ltb_spec (Z.pos e * Z.log2 (Z.pos b)) emax). ++ (* no overflow *) + rewrite pos_pow_spec. rewrite <- Z2R_Zpower by (zify; omega). rewrite <- Z2R_mult. + replace false with (Z.pos m * Z.pos b ^ Z.pos e <? 0). + exact (BofZ_correct (Z.pos m * Z.pos b ^ Z.pos e)). + rewrite Z.ltb_ge. rewrite Zmult_comm. apply Zmult_gt_0_le_0_compat. zify; omega. apply (Zpower_ge_0 base). ++ (* overflow *) + rewrite Rlt_bool_false. auto. eapply Rle_trans; [idtac|apply Rle_abs]. + apply (round_integer_overflow base). zify; omega. auto. +- (* e = Zneg e *) + destruct (Z.ltb_spec (Z.neg e * Z.log2 (Z.pos b) + Z.log2_up (Z.pos m)) emin). ++ (* undeflow *) + rewrite round_integer_underflow; auto. + rewrite Rlt_bool_true. auto. + replace (Rabs 0)%R with 0%R. apply bpow_gt_0. apply (Z2R_abs 0). + zify; omega. ++ (* no underflow *) + generalize (Bdiv_correct_aux prec emax prec_gt_0_ Hmax mode_NE false m 0 false (pos_pow b e) 0). + set (f := match Fdiv_core_binary prec (Z.pos m) 0 (Z.pos (pos_pow b e)) 0 with + | (0, _, _) => F754_nan false 1 + | (Z.pos mz0, ez, lz) => + binary_round_aux prec emax mode_NE (xorb false false) mz0 ez lz + | (Z.neg _, _, _) => F754_nan false 1 + end). + fold emin; fold fexp. rewrite ! A. unfold cond_Zopp. rewrite pos_pow_spec. + assert (B: (Z2R (Z.pos m) / Z2R (Z.pos b ^ Z.pos e) = + Z2R (Z.pos m) * bpow base (Z.neg e))%R). + { change (Z.neg e) with (- (Z.pos e)). rewrite bpow_opp. auto. } + rewrite B. intros [P Q]. + destruct (Rlt_bool + (Rabs + (round radix2 fexp (round_mode mode_NE) + (Z2R (Z.pos m) * bpow base (Z.neg e)))) + (bpow radix2 emax)). +* destruct Q as (Q1 & Q2 & Q3). + split. rewrite B2R_FF2B, Q1. auto. + split. rewrite is_finite_FF2B. auto. + rewrite Bsign_FF2B. auto. +* rewrite B2FF_FF2B. auto. +Qed. + End Extra_ops. (** ** Conversions between two FP formats *) diff --git a/lib/Floats.v b/lib/Floats.v index f86632b9..e893e3e7 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -92,100 +92,6 @@ Proof. destruct x as [[]|]; simpl; intros; discriminate. Qed. -Section FP_PARSING. - -Variables prec emax: Z. -Context (prec_gt_0 : Prec_gt_0 prec). -Hypothesis Hmax : (prec < emax)%Z. - -(** Function used to convert literals into FP numbers during parsing. - [intPart] is the mantissa - [expPart] is the exponent - [base] is the base for the exponent (usually 10 or 16). - The result is [intPart * base^expPart] rounded to the nearest FP number, - ties to even. *) - -Definition build_from_parsed (base:positive) (intPart:positive) (expPart:Z) : binary_float prec emax := - match expPart with - | Z0 => - binary_normalize prec emax prec_gt_0 Hmax mode_NE (Zpos intPart) Z0 false - | Zpos p => - binary_normalize prec emax prec_gt_0 Hmax mode_NE ((Zpos intPart) * Zpower_pos (Zpos base) p) Z0 false - | Zneg p => - FF2B prec emax _ (proj1 (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE - false intPart Z0 false (Pos.pow base p) Z0)) - end. - -Let emin := (3 - emax - prec)%Z. -Let fexp := FLT_exp emin prec. - -Theorem build_from_parsed_correct: - forall base m e (BASE: 2 <= Zpos base), - let base_r := {| radix_val := Zpos base; radix_prop := Zle_imp_le_bool _ _ BASE |} in - let r := round radix2 fexp (round_mode mode_NE) (Z2R (Zpos m) * bpow base_r e) in - if Rlt_bool (Rabs r) (bpow radix2 emax) then - B2R _ _ (build_from_parsed base m e) = r - /\ is_finite _ _ (build_from_parsed base m e) = true - /\ Bsign _ _ (build_from_parsed base m e) = false - else - B2FF _ _ (build_from_parsed base m e) = F754_infinity false. -Proof. - intros. - assert (A: forall x, @F2R radix2 {| Fnum := x; Fexp := 0 |} = Z2R x). - { intros. unfold F2R, Fnum; simpl. ring. } - unfold build_from_parsed, r; destruct e. -- change (bpow base_r 0) with (1%R). rewrite Rmult_1_r. - generalize (binary_normalize_correct _ _ _ Hmax mode_NE (Zpos m) 0 false). - fold emin; fold fexp. rewrite ! A. - destruct (Rlt_bool (Rabs (round radix2 fexp (round_mode mode_NE) (Z2R (Z.pos m)))) - (bpow radix2 emax)). - + intros (P & Q & R). split. auto. split. auto. rewrite R. rewrite Rcompare_Gt; auto. - apply (Z2R_lt 0). compute; auto. - + intros P; rewrite P. unfold binary_overflow. - replace (Rlt_bool (Z2R (Z.pos m)) 0%R) with false. auto. - rewrite Rlt_bool_false; auto. apply (Z2R_le 0). xomega. -- generalize (binary_normalize_correct _ _ _ Hmax mode_NE (Zpos m * Z.pow_pos (Zpos base) p) 0 false). - fold emin; fold fexp. rewrite ! A. - assert (B: Z2R (Z.pos m * Z.pow_pos (Z.pos base) p) = (Z2R (Z.pos m) * bpow base_r (Z.pos p))%R). - { unfold bpow. apply Z2R_mult. } - rewrite B. - destruct (Rlt_bool - (Rabs - (round radix2 fexp (round_mode mode_NE) - (Z2R (Z.pos m) * bpow base_r (Z.pos p)))) (bpow radix2 emax)). - + intros (P & Q & R). split. auto. split. auto. rewrite R. rewrite Rcompare_Gt; auto. - apply Rmult_lt_0_compat. apply (Z2R_lt 0). xomega. apply bpow_gt_0. - + intros P. rewrite P. unfold binary_overflow. - replace (Rlt_bool (Z2R (Z.pos m) * bpow base_r (Z.pos p)) 0) with false. - auto. - rewrite Rlt_bool_false; auto. apply Rlt_le. apply Rmult_lt_0_compat. apply (Z2R_lt 0). xomega. apply bpow_gt_0. -- generalize (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE false m 0 false (base ^ p) 0). - set (f := - match Fdiv_core_binary prec (Z.pos m) 0 (Z.pos (base ^ p)) 0 with - | (0, _, _) => F754_nan false 1 - | (Z.pos mz0, ez, lz) => - binary_round_aux prec emax mode_NE (xorb false false) mz0 ez lz - | (Z.neg _, _, _) => F754_nan false 1 - end). - fold emin; fold fexp. rewrite ! A. unfold cond_Zopp. - assert (B: (Z2R (Z.pos m) / Z2R (Z.pos (base ^ p)) = - Z2R (Z.pos m) * bpow base_r (Z.neg p))%R). - { change (Z.neg p) with (- (Z.pos p)). rewrite bpow_opp. unfold Rdiv. f_equal. f_equal. - unfold bpow. f_equal. simpl. apply Pos2Z.inj_pow_pos. } - rewrite ! B. - destruct (Rlt_bool - (Rabs - (round radix2 fexp (round_mode mode_NE) - (Z2R (Z.pos m) * bpow base_r (Z.neg p)))) (bpow radix2 emax)). - + intros (P & Q & R & S). - split. rewrite B2R_FF2B. exact Q. - split. rewrite is_finite_FF2B. auto. - rewrite Bsign_FF2B. auto. - + intros (P & Q). rewrite B2FF_FF2B. auto. -Qed. - -End FP_PARSING. - Local Notation __ := (refl_equal Datatypes.Lt). Local Hint Extern 1 (Prec_gt_0 _) => exact (refl_equal Datatypes.Lt). @@ -339,7 +245,7 @@ Definition of_longu (n:int64): float:= (**r conversion from unsigned 64-bit int BofZ 53 1024 __ __ (Int64.unsigned n). Definition from_parsed (base:positive) (intPart:positive) (expPart:Z) : float := - build_from_parsed 53 1024 __ __ base intPart expPart. + Bparse 53 1024 __ __ base intPart expPart. (** Conversions between floats and their concrete in-memory representation as a sequence of 64 bits. *) @@ -1004,7 +910,7 @@ Definition of_longu (n:int64): float32 := (**r conversion from unsigned 64-bit i BofZ 24 128 __ __ (Int64.unsigned n). Definition from_parsed (base:positive) (intPart:positive) (expPart:Z) : float32 := - build_from_parsed 24 128 __ __ base intPart expPart. + Bparse 24 128 __ __ base intPart expPart. (** Conversions between floats and their concrete in-memory representation as a sequence of 32 bits. *) diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 3fa7af31..a1d8338a 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -161,7 +161,7 @@ Inductive instruction : Type := | Pcmplwi: ireg -> constant -> instruction (**r same, with immediate argument *) | Pcmpw: ireg -> ireg -> instruction (**r signed integer comparison *) | Pcmpwi: ireg -> constant -> instruction (**r same, with immediate argument *) - | Pcntlz: ireg -> ireg -> instruction (**r count leading zeros *) + | Pcntlzw: ireg -> ireg -> instruction (**r count leading zeros *) | Pcreqv: crbit -> crbit -> crbit -> instruction (**r not-xor between condition bits *) | Pcror: crbit -> crbit -> crbit -> instruction (**r or between condition bits *) | Pcrxor: crbit -> crbit -> crbit -> instruction (**r xor between condition bits *) @@ -853,7 +853,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) | Pbdnz _ - | Pcntlz _ _ + | Pcntlzw _ _ | Pcreqv _ _ _ | Pcrxor _ _ _ | Peieio diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml new file mode 100644 index 00000000..520bc1ed --- /dev/null +++ b/powerpc/AsmToJSON.ml @@ -0,0 +1,362 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +(* Simple functions to serialize powerpc Asm to JSON *) + +open Asm +open AST +open BinNums +open C2C +open Camlcoq +open Printf +open Sections + +let p_ireg oc = function + | GPR0 -> fprintf oc "{\"Register\":\"r0\"}" + | GPR1 -> fprintf oc "{\"Register\":\"r1\"}" + | GPR2 -> fprintf oc "{\"Register\":\"r2\"}" + | GPR3 -> fprintf oc "{\"Register\":\"r3\"}" + | GPR4 -> fprintf oc "{\"Register\":\"r4\"}" + | GPR5 -> fprintf oc "{\"Register\":\"r5\"}" + | GPR6 -> fprintf oc "{\"Register\":\"r6\"}" + | GPR7 -> fprintf oc "{\"Register\":\"r7\"}" + | GPR8 -> fprintf oc "{\"Register\":\"r8\"}" + | GPR9 -> fprintf oc "{\"Register\":\"r9\"}" + | GPR10 -> fprintf oc "{\"Register\":\"r10\"}" + | GPR11 -> fprintf oc "{\"Register\":\"r11\"}" + | GPR12 -> fprintf oc "{\"Register\":\"r12\"}" + | GPR13 -> fprintf oc "{\"Register\":\"r13\"}" + | GPR14 -> fprintf oc "{\"Register\":\"r14\"}" + | GPR15 -> fprintf oc "{\"Register\":\"r15\"}" + | GPR16 -> fprintf oc "{\"Register\":\"r16\"}" + | GPR17 -> fprintf oc "{\"Register\":\"r17\"}" + | GPR18 -> fprintf oc "{\"Register\":\"r18\"}" + | GPR19 -> fprintf oc "{\"Register\":\"r19\"}" + | GPR20 -> fprintf oc "{\"Register\":\"r20\"}" + | GPR21 -> fprintf oc "{\"Register\":\"r21\"}" + | GPR22 -> fprintf oc "{\"Register\":\"r22\"}" + | GPR23 -> fprintf oc "{\"Register\":\"r23\"}" + | GPR24 -> fprintf oc "{\"Register\":\"r24\"}" + | GPR25 -> fprintf oc "{\"Register\":\"r25\"}" + | GPR26 -> fprintf oc "{\"Register\":\"r26\"}" + | GPR27 -> fprintf oc "{\"Register\":\"r27\"}" + | GPR28 -> fprintf oc "{\"Register\":\"r28\"}" + | GPR29 -> fprintf oc "{\"Register\":\"r29\"}" + | GPR30 -> fprintf oc "{\"Register\":\"r30\"}" + | GPR31 -> fprintf oc "{\"Register\":\"r31\"}" + +let p_freg oc = function + | FPR0 -> fprintf oc "{\"Register\":\"f0\"}" + | FPR1 -> fprintf oc "{\"Register\":\"f1\"}" + | FPR2 -> fprintf oc "{\"Register\":\"f2\"}" + | FPR3 -> fprintf oc "{\"Register\":\"f3\"}" + | FPR4 -> fprintf oc "{\"Register\":\"f4\"}" + | FPR5 -> fprintf oc "{\"Register\":\"f5\"}" + | FPR6 -> fprintf oc "{\"Register\":\"f6\"}" + | FPR7 -> fprintf oc "{\"Register\":\"f7\"}" + | FPR8 -> fprintf oc "{\"Register\":\"f8\"}" + | FPR9 -> fprintf oc "{\"Register\":\"f9\"}" + | FPR10 -> fprintf oc "{\"Register\":\"f10\"}" + | FPR11 -> fprintf oc "{\"Register\":\"f11\"}" + | FPR12 -> fprintf oc "{\"Register\":\"f12\"}" + | FPR13 -> fprintf oc "{\"Register\":\"f13\"}" + | FPR14 -> fprintf oc "{\"Register\":\"f14\"}" + | FPR15 -> fprintf oc "{\"Register\":\"f15\"}" + | FPR16 -> fprintf oc "{\"Register\":\"f16\"}" + | FPR17 -> fprintf oc "{\"Register\":\"f17\"}" + | FPR18 -> fprintf oc "{\"Register\":\"f18\"}" + | FPR19 -> fprintf oc "{\"Register\":\"f19\"}" + | FPR20 -> fprintf oc "{\"Register\":\"f20\"}" + | FPR21 -> fprintf oc "{\"Register\":\"f21\"}" + | FPR22 -> fprintf oc "{\"Register\":\"f22\"}" + | FPR23 -> fprintf oc "{\"Register\":\"f23\"}" + | FPR24 -> fprintf oc "{\"Register\":\"f24\"}" + | FPR25 -> fprintf oc "{\"Register\":\"f25\"}" + | FPR26 -> fprintf oc "{\"Register\":\"f26\"}" + | FPR27 -> fprintf oc "{\"Register\":\"f27\"}" + | FPR28 -> fprintf oc "{\"Register\":\"f28\"}" + | FPR29 -> fprintf oc "{\"Register\":\"f29\"}" + | FPR30 -> fprintf oc "{\"Register\":\"f30\"}" + | FPR31 -> fprintf oc "{\"Register\":\"f31\"}" + +let p_preg oc = function + | IR ir -> p_ireg oc ir + | FR fr -> p_freg oc fr + | _ -> assert false (* This registers should not be used. *) + +let p_atom oc a = fprintf oc "\"%s\"" (extern_atom a) + +let p_atom_constant oc a = fprintf oc "{\"Atom\":%a}" p_atom a + +let p_int oc i = fprintf oc "%ld" (camlint_of_coqint i) +let p_int64 oc i = fprintf oc "%Ld" (camlint64_of_coqint i) +let p_float32 oc f = fprintf oc "%ld" (camlint_of_coqint (Floats.Float32.to_bits f)) +let p_float64 oc f = fprintf oc "%Ld" (camlint64_of_coqint (Floats.Float.to_bits f)) +let p_z oc z = fprintf oc "%s" (Z.to_string z) + +let p_int_constant oc i = fprintf oc "{\"Integer\":%a}" p_int i +let p_float64_constant oc f = fprintf oc "{\"Float\":%a}" p_float64 f +let p_float32_constant oc f = fprintf oc "{\"Float\":%a}" p_float32 f +let p_z_constant oc z = fprintf oc "{\"Integer\":%s}" (Z.to_string z) + +let p_constant oc = function + | Cint i -> p_int_constant oc i + | Csymbol_low (i,c) -> fprintf oc "{\"Symbol_low\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c + | Csymbol_high (i,c) -> fprintf oc "{\"Symbol_high\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c + | Csymbol_sda (i,c) -> fprintf oc "{\"Symbol_sda\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c + | Csymbol_rel_low (i,c) -> fprintf oc "{\"Symbol_rel_low\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c + | Csymbol_rel_high (i,c) -> fprintf oc "{\"Symbol_rel_high\":{\"Name\":%a,\"Offset\":%a}}" p_atom i p_int c + +let p_crbit oc c = + let number = match c with + | CRbit_0 -> 0 + | CRbit_1 -> 1 + | CRbit_2 -> 2 + | CRbit_3 -> 3 + | CRbit_6 -> 6 in + fprintf oc "{\"CRbit\":%d}" number + + +let p_label oc l = fprintf oc "{\"Label\":%ld}" (P.to_int32 l) + +let p_char_list oc l = fprintf oc "{\"String\":\"%a\"}" (fun oc -> List.iter (output_char oc)) l + +let p_list elem oc l = + match l with + | [] -> fprintf oc "[]" + | hd::tail -> + output_string oc "["; elem oc hd;List.iter (fprintf oc ",%a" elem) tail;output_string oc "]" + +let p_list_cont elem oc l = + match l with + | [] -> () + | _ -> + List.iter (fprintf oc ",%a" elem) l + +let p_instruction oc ic = + output_string oc "\n"; + match ic with + | Padd (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Padd\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Paddc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Paddc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Padde (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Padde\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Paddi (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddi\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Paddic (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Paddis (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddis\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Paddze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Paddze\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pallocframe (c,i) -> assert false(* Should not occur *) + | Pand_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pand_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pandc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pandc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pandi_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandi_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Pandis_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandis_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Pb l -> fprintf oc "{\"Instruction Name\":\"Pb\",\"Args\":[%a]}" p_label l + | Pbctr s -> assert false (* Should not occur *) + | Pbctrl s -> fprintf oc "{\"Instruction Name\":\"Pbctrl\",\"Args\":[]}" + | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l + | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l + | Pbl (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbl\",\"Args\":[%a]}" p_atom_constant i + | Pbs (i,s) -> fprintf oc "{\"Instruction Name\":\"Pbs\",\"Args\":[%a]}" p_atom_constant i + | Pblr -> fprintf oc "{\"Instruction Name\":\"Pblr\",\"Args\":[]}" + | Pbt (cr,l) -> fprintf oc "{\"Instruction Name\":\"Pbt\",\"Args\":[%a,%a]}" p_crbit cr p_label l + | Pbtbl (i,lb) -> fprintf oc "{\"Instruction Name\":\"Pbtl\",\"Args\":[%a%a]}" p_ireg i (p_list_cont p_label) lb + | Pcmplw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmplw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pcmplwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmplwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c + | Pcmpw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmpw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pcmpwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmpwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c + | Pcntlzw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcntlzw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pcreqv (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcreqv\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 + | Pcror (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcror\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 + | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 + | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}" + | Peqv (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Peqv\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pextsb (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsb\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pextsh (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pextsh\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pfreeframe (c,i) -> assert false (* Should not occur *) + | Pfabs (fr1,fr2) + | Pfabss (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfabs\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfadd (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadd\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfadds (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfadds\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfcmpu (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfcmpu\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfcti (ir,fr) -> assert false (* Should not occur *) + | Pfctiw (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctiw\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfctiwz (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfctiwz\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfdiv (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfdiv\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfdivs (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfdivs\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfmake (fr,ir1,ir2) -> assert false (* Should not occur *) + | Pfmr (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfmr\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfmul (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfmul\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfmuls(fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfmuls\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfneg (fr1,fr2) + | Pfnegs (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfneg\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfrsp (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfrsp\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfxdp (fr1,fr2) -> assert false (* Should not occur *) + | Pfsub (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfsub\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfsubs (fr1,fr2,fr3) -> fprintf oc "{\"Instruction Name\":\"Pfsubs\",\"Args\":[%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 + | Pfmadd (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfmadd\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pfmsub (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfmsub\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pfnmadd (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfmadd\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pfnmsub (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfnmsub\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pfsqrt (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrt\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfrsqrte (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrte\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2 + | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4 + | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}" + | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Plbzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pblzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plfd (fr,c,ir) + | Plfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Plfdx (fr,ir1,ir2) + | Plfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Plfs (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfs\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Plfsx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Plfsx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Plha (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plha\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Plhax (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plhax\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plhbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plhbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plhz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plhz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Plhzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plhzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plfi (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfi\",\"Args\":[%a,%a]}" p_freg fr p_float64_constant fc + | Plfis (fr,fc) -> fprintf oc "{\"Instruction Name\":\"Plfis\",\"Args\":[%a,%a]}" p_freg fr p_float32_constant fc + | Plwz (ir1,ic,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant ic p_ireg ir2 + | Plwz_a (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Plwzu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plwzu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Plwzx (ir1,ir2,ir3) + | Plwzx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plwarx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwarx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Plwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pmfcr ir -> fprintf oc "{\"Instruction Name\":\"Pmfcr\",\"Args\":[%a]}" p_ireg ir + | Pmfcrbit (ir,crb) -> assert false (* Should not occur *) + | Pmflr ir -> fprintf oc "{\"Instruction Name\":\"Pmflr\",\"Args\":[%a]}" p_ireg ir + | Pmr (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pmr\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pmtctr ir -> fprintf oc "{\"Instruction Name\":\"Pmtctr\",\"Args\":[%a]}" p_ireg ir + | Pmtlr ir -> fprintf oc "{\"Instruction Name\":\"Pmtlr\",\"Args\":[%a]}" p_ireg ir + | Pmulli (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pmulli\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Pmullw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pmulhw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pmulhwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pnand (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pnand\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pnor (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pnor\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Por (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Por\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Porc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Porc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Poris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Poris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Prlwinm (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwinm\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic1 p_int_constant ic2 + | Prlwimi (ir1,ir2,ic1,ic2) -> fprintf oc "{\"Instruction Name\":\"Prlwimi\",\"Args\":[%a,%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic1 p_int_constant ic2 + | Pslw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pslw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psraw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psraw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psrawi (ir1,ir2,ic) -> fprintf oc "{\"Instruction Name\":\"Psrawi\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_int_constant ic + | Psrw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psrw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstb (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstb\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Pstbx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstbx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstfd (fr,c,ir) + | Pstfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Pstfdu (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstdu\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Pstfdx (fr,ir1,ir2) + | Pstfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Pstfs (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfs\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir + | Pstfsx (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstfsx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2 + | Psth (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Psth\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Psthx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psthx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psthbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psthbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstw (ir1,c,ir2) + | Pstw_a (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Pstwu (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2 + | Pstwx (ir1,ir2,ir3) + | Pstwx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstwux (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwux\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pstwcx_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstwc_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psubfc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psubfe (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Psubfze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Psubfe\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Psubfic (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Psubfic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Psync -> fprintf oc "{\"Instruction Name\":\"Psync\",\"Args\":[]}" + | Ptrap -> fprintf oc "{\"Instruction Name\":\"Ptrap\",\"Args\":[]}" + | Pxor (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pxor\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3 + | Pxori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Pxoris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxoris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c + | Plabel l -> fprintf oc "{\"Instruction Name\":\"Plabel\",\"Args\":[%a]}" p_label l + | Pbuiltin (ef,args1,args2) -> + begin match ef with + | EF_inline_asm (i,s,il) -> + fprintf oc "{\"Instruction Name\":\"Inline_asm\",\"Args\":[%a%a%a%a]}" p_atom_constant i (p_list_cont p_char_list) il + (p_list_cont p_preg) args1 (p_list_cont p_preg) args2 + | _ -> (* Should all be folded away *) + assert false + end + | Pannot _ (* We do not check the annotations *) + | Pcfi_adjust _ (* Only debug relevant *) + | Pcfi_rel_offset _ -> () (* Only debug relevant *) + +let p_storage oc static = + if static then + fprintf oc "\"Static\"" + else + fprintf oc "\"Extern\"" + +let p_section oc = function + | Section_text -> fprintf oc "{\"Section Name\":\"Text\"}" + | Section_data init -> fprintf oc "{\"Section Name\":\"Data\",\"Init\":%B}" init + | Section_small_data init -> fprintf oc "{\"Section Name\":\"Small Data\",\"Init\":%B}" init + | Section_const init -> fprintf oc "{\"Section Name\":\"Const\",\"Init\":%B}" init + | Section_small_const init -> fprintf oc "{\"Section Name\":\"Small Const\",\"Init\":%B}" init + | Section_string -> fprintf oc "{\"Section Name\":\"String\"}" + | Section_literal -> fprintf oc "{\"Section Name\":\"Literal\"}" + | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}" + | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e + | Section_debug_info + | Section_debug_abbrev -> () (* There should be no info in the debug sections *) + +let p_int_opt oc = function + | None -> fprintf oc "0" + | Some i -> fprintf oc "%d" i + + +let p_fundef oc (name,f) = + let alignment = atom_alignof name + and inline = atom_is_inline name + and static = atom_is_static name + and instr = List.filter (function Pannot _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in + let c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in + fprintf oc "{\"Fun Name\":%a,\n\"Fun Storage Class\":%a,\n\"Fun Alignment\":%a,\n\"Fun Section Code\":%a,\"Fun Section Literals\":%a,\"Fun Section Jumptable\":%a,\n\"Fun Inline\":%B,\n\"Fun Code\":%a}\n" + p_atom name p_storage static p_int_opt alignment + p_section c_section p_section l_section p_section j_section inline + (p_list p_instruction) instr + +let p_init_data oc = function + | Init_int8 ic -> fprintf oc "{\"Init_int8\":%a}" p_int ic + | Init_int16 ic -> fprintf oc "{\"Init_int16\":%a}" p_int ic + | Init_int32 ic -> fprintf oc "{\"Init_int32\":%a}" p_int ic + | Init_int64 lc -> fprintf oc "{\"Init_int64\":%a}" p_int64 lc + | Init_float32 f -> fprintf oc "{\"Init_float32\":%a}" p_float32 f + | Init_float64 f -> fprintf oc "{\"Init_float64\":%a}" p_float64 f + | Init_space z -> fprintf oc "{\"Init_space\":%a}" p_z z + | Init_addrof (p,i) -> fprintf oc "{\"Init_addrof\":{\"Addr\":%a,\"Offset\":%a}}" p_atom p p_int i + +let p_vardef oc (name,v) = + let alignment = atom_alignof name + and static = atom_is_static name + and section = match (atom_sections name) with [s] -> s | _ -> assert false (* Should only have one section *) in + fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\n\"Var Storage Class\":%a,\n\"Var Alignment\":%a,\n\"Var Section\":%a,\n\"Var Init\":%a}\n" + p_atom name v.gvar_readonly v.gvar_volatile + p_storage static p_int_opt alignment p_section section + (p_list p_init_data) v.gvar_init + +let p_program oc prog = + let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) -> + match def with + | Gfun (Internal f) -> vars,(ident,f)::funs + | Gvar v -> (ident,v)::vars,funs + | _ -> vars,funs) ([],[]) prog.prog_defs in + fprintf oc "{\"Global Variables\":%a,\n\"Functions\":%a}" + (p_list p_vardef) prog_vars + (p_list p_fundef) prog_funs diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index ec5a767f..b8d30ae3 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -313,7 +313,7 @@ let expand_builtin_inline name args res = | "__builtin_mulhwu", [IR a1; IR a2], [IR res] -> emit (Pmulhwu(res, a1, a2)) | "__builtin_clz", [IR a1], [IR res] -> - emit (Pcntlz(res, a1)) + emit (Pcntlzw(res, a1)) | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] -> emit (Pstwu(a1, Cint _m8, GPR1)); emit (Pcfi_adjust _8); @@ -397,11 +397,12 @@ let expand_builtin_inline name args res = (* Calls to variadic functions: condition bit 6 must be set if at least one argument is a float; clear otherwise. - Note that variadic functions cannot have arguments of type Tsingle. *) + For compatibility with other compilers, do the same if the called + function is unprototyped. *) let set_cr6 sg = - if sg.sig_cc.cc_vararg then begin - if List.mem Tfloat sg.sig_args + if sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto then begin + if List.exists (function Tfloat | Tsingle -> true | _ -> false) sg.sig_args then emit (Pcreqv(CRbit_6, CRbit_6, CRbit_6)) else emit (Pcrxor(CRbit_6, CRbit_6, CRbit_6)) end diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 2d47acb0..1cd7fe37 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -30,8 +30,8 @@ module type SYSTEM = val constant: out_channel -> constant -> unit val ireg: out_channel -> ireg -> unit val freg: out_channel -> freg -> unit - val creg: out_channel -> int -> unit val name_of_section: section_name -> string + val creg: out_channel -> int -> unit val print_file_line: out_channel -> string -> int -> unit val cfi_startproc: out_channel -> unit val cfi_endproc: out_channel -> unit @@ -40,6 +40,8 @@ module type SYSTEM = val print_prologue: out_channel -> unit val print_epilogue: out_channel -> unit val print_file_loc: out_channel -> DwarfTypes.file_loc -> unit + val section: out_channel -> section_name -> unit + val debug_section: out_channel -> section_name -> unit end let symbol = elf_symbol @@ -129,6 +131,11 @@ module Linux_System : SYSTEM = s (if wr then "w" else "") (if ex then "x" else "") | Section_debug_info -> ".debug_info,\"\",@progbits" | Section_debug_abbrev -> ".debug_abbrev,\"\",@progbits" + + let section oc sec = + let name = name_of_section sec in + assert (name <> "COMM"); + fprintf oc " %s\n" name let print_file_line oc file line = @@ -148,7 +155,8 @@ module Linux_System : SYSTEM = let print_epilogue oc = () let print_file_loc _ _ = () - + + let debug_section _ _ = () end module Diab_System : SYSTEM = @@ -202,6 +210,12 @@ module Diab_System : SYSTEM = | Section_debug_info -> ".debug_info,,n" | Section_debug_abbrev -> ".debug_abbrev,,n" + let section oc sec = + let name = name_of_section sec in + assert (name <> "COMM"); + fprintf oc " %s\n" name + + let print_file_line oc file line = print_file_line_d2 oc comment file line @@ -232,6 +246,9 @@ module Diab_System : SYSTEM = let filenum : (string,int) Hashtbl.t = Hashtbl.create 7 + let additional_debug_sections: StringSet.t ref = ref StringSet.empty + + let print_epilogue oc = if !Clflags.option_g then begin @@ -244,12 +261,35 @@ module Diab_System : SYSTEM = let label = new_label () in Hashtbl.add filenum file label; fprintf oc ".L%d: .d2filenum \"%s\"\n" label file) !all_files; - fprintf oc " .d2_line_end\n" + fprintf oc " .d2_line_end\n"; + StringSet.iter (fun s -> + fprintf oc " %s\n" s; + fprintf oc " .d2_line_end\n") !additional_debug_sections end let print_file_loc oc (file,col) = fprintf oc " .4byte %a\n" label (Hashtbl.find filenum file); fprintf oc " .uleb128 %d\n" col + + let debug_section oc sec = + if !Clflags.option_g && Configuration.advanced_debug then + match sec with + | Section_user (name,_,_) -> + let sec_name = name_of_section sec in + if not (StringSet.mem sec_name !additional_debug_sections) then + begin + let name = ".debug_line"^name in + additional_debug_sections := StringSet.add sec_name !additional_debug_sections; + fprintf oc " .section %s,,n\n" name; + fprintf oc " .sectionlink .debug_line\n"; + section oc sec; + fprintf oc " .d2_line_start %s\n" name + end + | _ -> () (* Only the case of a user section is interresting *) + else + () + + end module Target (System : SYSTEM):TARGET = @@ -296,11 +336,6 @@ module Target (System : SYSTEM):TARGET = | FR r -> fprintf oc "f%s" (float_reg_name r) | _ -> assert false - let section oc sec = - let name = name_of_section sec in - assert (name <> "COMM"); - fprintf oc " %s\n" name - let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) @@ -426,8 +461,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " cmpw %a, %a, %a\n" creg 0 ireg r1 ireg r2 | Pcmpwi(r1, c) -> fprintf oc " cmpwi %a, %a, %a\n" creg 0 ireg r1 constant c - | Pcntlz(r1, r2) -> - fprintf oc " cntlz %a, %a\n" ireg r1 ireg r2 + | Pcntlzw(r1, r2) -> + fprintf oc " cntlzw %a, %a\n" ireg r1 ireg r2 | Pcreqv(c1, c2, c3) -> fprintf oc " creqv %a, %a, %a\n" crbit c1 crbit c2 crbit c3 | Pcror(c1, c2, c3) -> @@ -806,7 +841,11 @@ module Target (System : SYSTEM):TARGET = module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs - let new_label = new_label + let new_label = new_label + + let section oc sec = + section oc sec; + debug_section oc sec end diff --git a/runtime/include/stdarg.h b/runtime/include/stdarg.h index b2e7eadd..3e9eaf95 100644 --- a/runtime/include/stdarg.h +++ b/runtime/include/stdarg.h @@ -45,10 +45,20 @@ typedef __builtin_va_list __gnuc_va_list; #ifdef _STDARG_H +#ifdef __DCC__ #ifndef _VA_LIST_T #define _VA_LIST_T +#endif +#ifndef __VA_LIST +#define __VA_LIST typedef __builtin_va_list va_list; #endif +#else +#ifndef _VA_LIST_T +#define _VA_LIST_T +typedef __builtin_va_list va_list; +#endif +#endif #define va_start(v,l) __builtin_va_start(v,l) #define va_end(v) __builtin_va_end(v) diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h index 3da06c6f..31edf4ef 100644 --- a/runtime/include/stddef.h +++ b/runtime/include/stddef.h @@ -38,6 +38,14 @@ #define _STDDEF_H #endif +#ifdef __DCC__ +#if !defined(__size_t) && !defined(_SIZE_T) +#define __size_t +#define _SIZE_T +typedef unsigned int size_t; +#endif +#undef __need_size_t +#else #if defined(_STDDEF_H) || defined(__need_size_t) #ifndef _SIZE_T #define _SIZE_T @@ -45,6 +53,7 @@ typedef unsigned long size_t; #endif #undef __need_size_t #endif +#endif #if defined(_STDDEF_H) || defined(__need_ptrdiff_t) #ifndef _PTRDIFF_T @@ -54,6 +63,20 @@ typedef signed long ptrdiff_t; #undef __need_ptrdiff_t #endif +#ifdef __DCC__ +#ifndef _WCHART +#define _WCHART +#ifndef __wchar_t +#define __wchar_t +#ifdef _TYPE_wchar_t +_TYPE_wchar_t; +#else +typedef unsigned short wchar_t; +#endif +#endif +#undef __need_wchar_t +#endif +#else #if defined(_STDDEF_H) || defined(__need_wchar_t) #ifndef _WCHAR_T #define _WCHAR_T @@ -65,6 +88,7 @@ typedef signed int wchar_t; #endif #undef __need_wchar_t #endif +#endif #if defined(_STDDEF_H) || defined(__need_NULL) #ifndef NULL @@ -74,7 +98,7 @@ typedef signed int wchar_t; #endif #if defined(_STDDEF_H) && !defined(offsetof) -#define offsetof(ty,member) ((size_t) &(((ty)*) NULL)->member) +#define offsetof(ty,member) ((size_t) &((ty*) NULL)->member) #endif #endif diff --git a/test/regression/Makefile b/test/regression/Makefile index 94c212d2..e2d94aa9 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -15,9 +15,9 @@ LIBS=$(LIBMATH) TESTS=int32 int64 floats floats-basics \ expr1 expr6 funptr2 initializers initializers2 initializers3 \ volatile1 volatile2 volatile3 \ - funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \ + funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \ sizeof1 sizeof2 binops bool for1 switch switch2 compound \ - decl1 interop1 bitfields9 + decl1 interop1 bitfields9 ptrs3 # Can run, but only in compiled mode, and have reference output in Results diff --git a/test/regression/Results/bitfields9 b/test/regression/Results/bitfields9 index ca74f1f4..a1d0e9fd 100644 --- a/test/regression/Results/bitfields9 +++ b/test/regression/Results/bitfields9 @@ -1,10 +1,10 @@ glob_s = { a = -12, b = 1 } -glob_t = { c = 123, d = 0, e = -45 } +glob_t = { c = 123, d = 1, e = -45 } loc_s = { a = 11, b = 2 } loc_t = { c = 11, d = 1, e = 2 } compound_s = { a = 2, b = 3 } -compound_t = { c = 2, d = 0, e = -11 } +compound_t = { c = 2, d = 1, e = -11 } loc_s = { a = 7, b = 2 } loc_t = { c = 7, d = 1, e = 50 } compound_s = { a = -14, b = 3 } -compound_t = { c = 50, d = 0, e = -7 } +compound_t = { c = 50, d = 1, e = -7 } diff --git a/test/regression/Results/builtins-powerpc b/test/regression/Results/builtins-powerpc index ac4240a8..0fd07f69 100644 --- a/test/regression/Results/builtins-powerpc +++ b/test/regression/Results/builtins-powerpc @@ -8,8 +8,8 @@ fmsub(3.141590, 2.718000, 1.414000) = 7.124842 fabs(3.141590) = 3.141590 fabs(-3.141590) = 3.141590 fsqrt(3.141590) = 1.772453 -frsqrte(3.141590) = 0.564198 -fres(3.141590) = 0.318311 +frsqrte(3.141590) = OK +fres(3.141590) = OK fsel(3.141590, 2.718000, 1.414000) = 2.718000 fsel(-3.141590, 2.718000, 1.414000) = 1.414000 fcti(3.141590) = 3 diff --git a/test/regression/Results/ptrs3 b/test/regression/Results/ptrs3 new file mode 100644 index 00000000..17af0459 --- /dev/null +++ b/test/regression/Results/ptrs3 @@ -0,0 +1,2 @@ +p - q = -9 +q - p = 9 diff --git a/test/regression/Results/struct12 b/test/regression/Results/struct12 new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/test/regression/Results/struct12 diff --git a/test/regression/bitfields1.c b/test/regression/bitfields1.c index c6022dd1..5f6dfdd1 100644 --- a/test/regression/bitfields1.c +++ b/test/regression/bitfields1.c @@ -7,7 +7,7 @@ struct s { struct t { unsigned int c: 16; - unsigned int d: 1; + _Bool d: 1; short e: 8; }; @@ -29,7 +29,7 @@ int main() y.c = 12345; y.d = 0; y.e = 89; - res = f(&x, &y, 1); + res = f(&x, &y, 2); printf("x = {a = %d, b = %d }\n", x.a, x.b); printf("y = {c = %d, d = %d, e = %d }\n", y.c, y.d, y.e); diff --git a/test/regression/bitfields9.c b/test/regression/bitfields9.c index b33c4064..be87057b 100644 --- a/test/regression/bitfields9.c +++ b/test/regression/bitfields9.c @@ -9,7 +9,7 @@ struct s { struct t { unsigned int c: 16; - unsigned int d: 1; + _Bool d: 1; short e: 8; }; @@ -25,25 +25,25 @@ void print_t(char * msg, struct t p) /* Global initialization */ struct s glob_s = { -12, 1 }; -struct t glob_t = { 123, 0, -45 }; +struct t glob_t = { 123, 2, -45 }; /* Local initialization */ -void f(int x, int y) +void f(int x, int y, int z) { struct s loc_s = { x, y }; - struct t loc_t = { x, 1, y }; + struct t loc_t = { x, z, y }; print_s("loc_s", loc_s); print_t("loc_t", loc_t); print_s("compound_s", (struct s) { y, x }); - print_t("compound_t", (struct t) { y, 0, -x }); + print_t("compound_t", (struct t) { y, ~z, -x }); } int main() { print_s("glob_s", glob_s); print_t("glob_t", glob_t); - f(11, 2); - f(7, 50); + f(11, 2, 3); + f(7, 50, 2); return 0; } diff --git a/test/regression/builtins-powerpc.c b/test/regression/builtins-powerpc.c index 17d4d3c5..acffa435 100644 --- a/test/regression/builtins-powerpc.c +++ b/test/regression/builtins-powerpc.c @@ -1,6 +1,13 @@ /* Fun with builtins */ #include <stdio.h> +#include <math.h> + +char * check_relative_error(double exact, double actual, double precision) +{ + double relative_error = (actual - exact) / exact; + return fabs(relative_error) <= precision ? "OK" : "ERROR"; +} int main(int argc, char ** argv) { @@ -22,8 +29,10 @@ int main(int argc, char ** argv) printf("fabs(%f) = %f\n", a, __builtin_fabs(a)); printf("fabs(%f) = %f\n", -a, __builtin_fabs(-a)); printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a)); - printf("frsqrte(%f) = %f\n", a, __builtin_frsqrte(a)); - printf("fres(%f) = %f\n", a, __builtin_fres(a)); + printf("frsqrte(%f) = %s\n", + a, check_relative_error(1.0 / sqrt(a), __builtin_frsqrte(a), 1./32.)); + printf("fres(%f) = %s\n", + a, check_relative_error(1.0 / a, __builtin_fres(a), 1./256.)); printf("fsel(%f, %f, %f) = %f\n", a, b, c, __builtin_fsel(a, b, c)); printf("fsel(%f, %f, %f) = %f\n", -a, b, c, __builtin_fsel(-a, b, c)); printf("fcti(%f) = %d\n", a, __builtin_fcti(a)); diff --git a/test/regression/ptrs3.c b/test/regression/ptrs3.c new file mode 100644 index 00000000..e0425af4 --- /dev/null +++ b/test/regression/ptrs3.c @@ -0,0 +1,10 @@ +#include <stdio.h> + +int main() { + int a[10]; + int *p = &a[0]; + int *q = &a[9]; + printf("p - q = %d\n", (int)(p - q)); + printf("q - p = %d\n", (int)(q - p)); + return 0; +} diff --git a/test/regression/sections.c b/test/regression/sections.c index 2e0e4e75..adf94e83 100644 --- a/test/regression/sections.c +++ b/test/regression/sections.c @@ -13,14 +13,14 @@ struct s { long long ll; }; -struct s x; /* normal absolute addressing */ +struct s x = {0, }; /* normal absolute addressing */ #pragma use_section SDATA y -struct s y; /* small data area */ +struct s y = {0, }; /* small data area */ #pragma section MYDATA ".mydata" ".mydata" far-data RW #pragma use_section MYDATA z -struct s z; /* far data area, relative addressing */ +struct s z = {0, }; /* far data area, relative addressing */ #define TEST(msg,ty,x,v1,v2,v3) \ x = v1; \ diff --git a/test/regression/struct12.c b/test/regression/struct12.c new file mode 100644 index 00000000..39e62b28 --- /dev/null +++ b/test/regression/struct12.c @@ -0,0 +1,39 @@ +/* This is was originally a regression test for bug 43784 of gcc. + See ISO/IEC 9899:TC3 ยง6.8.6.4p4 and footnote 139. */ + +#include <stdio.h> + +struct s { + unsigned char a[256]; +}; +union u { + struct { struct s b; int c; } d; + struct { int c; struct s b; } e; +}; + +static union u v; +static struct s *p = &v.d.b; +static struct s *q = &v.e.b; + +static struct s __attribute__((noinline)) rp(void) +{ + return *p; +} + +static void qp(void) +{ + *q = rp(); +} + +int main() +{ + int i; + for (i = 0; i < 256; i++) + p->a[i] = i; + qp(); + for (i = 0; i < 256; i++) + if (q->a[i] != i) + printf("ERROR at %d: %d\n", i, q->a[i]); + return 0; +} + |