diff options
33 files changed, 503 insertions, 201 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/ - @@ -1,14 +1,21 @@ All files in this distribution are part of the CompCert verified compiler. -The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007, -2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Institut National de -Recherche en Informatique et en Automatique (INRIA). +The CompCert verified compiler is Copyright by Institut National de +Recherche en Informatique et en Automatique (INRIA) and +AbsInt Angewandte Informatik GmbH. The CompCert verified compiler is distributed under the terms of the -INRIA Non-Commercial License Agreement given below. This is a -non-free license that grants you the right to use the CompCert verified -compiler for educational, research or evaluation purposes only, but -prohibits commercial uses. +INRIA Non-Commercial License Agreement given below or under the terms +of a Software Usage Agreement of AbsInt Angewandte Informatik GmbH. +The latter is a separate contract document. + +The INRIA Non-Commercial License Agreement is a non-free license that +grants you the right to use the CompCert verified compiler for +educational, research or evaluation purposes only, but prohibits +any commercial uses. + +For commercial use you need a Software Usage Agreement from +AbsInt Angewandte Informatik GmbH. The following files in this distribution are dual-licensed both under the INRIA Non-Commercial License Agreement and under the Free Software @@ -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/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 71328c71..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 _ -> () @@ -897,6 +898,28 @@ let rec groupSwitch = function let (fst, cases) = groupSwitch rem in (Cutil.sseq s.sloc s fst, cases) +(* Test whether the statement contains case and give an *) +let rec contains_case s = + match s.sdesc with + | C.Sskip + | C.Sdo _ + | C.Sbreak + | C.Scontinue + | C.Sswitch _ (* Stop at a switch *) + | C.Sgoto _ + | C.Sreturn _ + | C.Sdecl _ + | C.Sasm _ -> () + | C.Sseq (s1,s2) + | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2 + | C.Swhile (_,s1) + | C.Sdowhile (s1,_) -> contains_case s1 + | C.Sfor (s1,e,s2,s3) -> contains_case s1; contains_case s2; contains_case s3 + | C.Slabeled(C.Scase _, _) -> + unsupported "'case' outside of 'switch'" + | C.Slabeled(_,s) -> contains_case s + | C.Sblock b -> List.iter contains_case b + (** Annotations for line numbers *) let add_lineno prev_loc this_loc s = @@ -953,7 +976,10 @@ let rec convertStmt ploc env s = | C.Sswitch(e, s1) -> let (init, cases) = groupSwitch (flattenSwitch s1) in if init.sdesc <> C.Sskip then - warning "ignored code at beginning of 'switch'"; + begin + warning "ignored code at beginning of 'switch'"; + contains_case init + end; let te = convertExpr env e in add_lineno ploc s.sloc (swrap (Ctyping.sswitch te 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:" diff --git a/cparser/Elab.ml b/cparser/Elab.ml index aa015b83..d6b79780 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1817,6 +1817,7 @@ let enter_or_refine_ident local loc env s sto ty = error loc "static redefinition of '%s' after non-static definition" s; sto | Storage_static,_ -> Storage_static (* Static stays static *) | Storage_extern,_ -> sto + | Storage_default,Storage_extern -> Storage_extern | _,Storage_extern -> old_sto | _,Storage_register | Storage_register,_ -> Storage_register 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/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 352483bf..1b58fe61 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -74,7 +74,7 @@ let print_error oc msg = let output_filename ?(final = false) source_file source_suffix output_suffix = match !option_o with | Some file when final -> file - | _ -> + | _ -> Filename.basename (Filename.chop_suffix source_file source_suffix) ^ output_suffix @@ -127,7 +127,7 @@ let parse_c_file sourcename ifile = let oc = open_out ofile in Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc - end; + end; (* Conversion to Csyntax *) let csyntax = match Timing.time "CompCert C generation" C2C.convertProgram ast with @@ -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,7 +155,7 @@ let dump_asm asm destfile = output_value oc C2C.decl_atom; close_out oc -let jdump_magic_number = "CompCertJDUMP" ^ Configuration.version +let jdump_magic_number = "CompCertJDUMP" ^ Version.version let dump_jasm asm destfile = let oc = open_out_bin destfile in @@ -231,7 +231,7 @@ let compile_cminor_file ifile ofile = eprintf "File %s, character %d: Syntax error\n" ifile (Lexing.lexeme_start lb); exit 2 - | CMlexer.Error msg -> + | CMlexer.Error msg -> eprintf "File %s, character %d: %s\n" ifile (Lexing.lexeme_start lb) msg; exit 2 @@ -373,7 +373,7 @@ let process_h_file sourcename = end else begin eprintf "Error: input file %s ignored (not in -E mode)\n" sourcename; exit 2 - end + end (* Record actions to be performed after parsing the command line *) @@ -398,9 +398,15 @@ let explode_comma_option s = | [] -> assert false | hd :: tl -> tl +let version_string = + 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 = -"The CompCert C verified compiler, version " ^ Configuration.version ^ " -Usage: ccomp [options] <source files> + version_string ^ + "Usage: ccomp [options] <source files> Recognized source files: .c C source file .i or .p C source file that should not be preprocessed @@ -477,6 +483,7 @@ General options: -stdlib <dir> Set the path of the Compcert run-time library -v Print external commands before invoking them -timings Show the time spent in various compiler passes + -version Print the version string and exit Interpreter mode: -interp Execute given .c files using the reference interpreter -quiet Suppress diagnostic messages for the interpreter @@ -488,6 +495,9 @@ Interpreter mode: let print_usage_and_exit _ = printf "%s" usage_string; exit 0 +let print_version_and_exit _ = + printf "%s" version_string; exit 0 + let language_support_options = [ option_fbitfields; option_flongdouble; option_fstruct_return; option_fvararg_calls; option_funprototyped; @@ -510,13 +520,16 @@ let cmdline_actions = (* Getting help *) Exact "-help", Self print_usage_and_exit; Exact "--help", Self print_usage_and_exit; +(* Getting version info *) + Exact "-version", Self print_version_and_exit; + Exact "--version", Self print_version_and_exit; (* Processing options *) Exact "-c", Set option_c; Exact "-E", Set option_E; Exact "-S", Set option_S; Exact "-o", String(fun s -> option_o := Some s); Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in - option_o := Some s); + option_o := Some s); (* Preprocessing options *) Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options); Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options); @@ -563,7 +576,7 @@ let cmdline_actions = Exact "-dmach", Set option_dmach; Exact "-dasm", Set option_dasm; Exact "-sdump", Set option_sdump; -(* General options *) +(* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); Exact "-timings", Set option_timings; 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 index 4c3f9d97..36960821 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -171,7 +171,7 @@ let p_instruction oc ic = | 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 - | Pcntlz (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcntlz\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | 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 diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 699c841f..3f4dc94b 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -343,7 +343,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); 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/stddef.h b/runtime/include/stddef.h index 0c3251f6..290434f4 100644 --- a/runtime/include/stddef.h +++ b/runtime/include/stddef.h @@ -63,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 signed int wchar_t; +#endif +#endif +#undef __need_wchar_t +#endif +#else #if defined(_STDDEF_H) || defined(__need_wchar_t) #ifndef _WCHAR_T #define _WCHAR_T @@ -74,6 +88,7 @@ typedef signed int wchar_t; #endif #undef __need_wchar_t #endif +#endif #if defined(_STDDEF_H) || defined(__need_NULL) #ifndef NULL diff --git a/test/compression/arcode.c b/test/compression/arcode.c index f915cc25..f915cc25 100755..100644 --- a/test/compression/arcode.c +++ b/test/compression/arcode.c diff --git a/test/compression/arcode.h b/test/compression/arcode.h index aac32080..aac32080 100755..100644 --- a/test/compression/arcode.h +++ b/test/compression/arcode.h diff --git a/test/compression/armain.c b/test/compression/armain.c index 8f37c4ff..8f37c4ff 100755..100644 --- a/test/compression/armain.c +++ b/test/compression/armain.c diff --git a/test/regression/Makefile b/test/regression/Makefile index 94c212d2..da7d5755 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -17,7 +17,7 @@ TESTS=int32 int64 floats floats-basics \ volatile1 volatile2 volatile3 \ funct3 expr5 struct7 struct8 struct11 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/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/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; +} |