From c9acadca7c8d5d29dd57b9acba99369067f93ae1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 8 Sep 2010 16:50:23 +0000 Subject: Updates for IA32-Cygwin. cparser/Elab.ml: tolerate changes in qualifiers in ?: cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1506 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Makefile | 14 +++++++++++--- cfrontend/C2C.ml | 51 +++++++++++++++++++++++++++++++-------------------- configure | 11 +++++++++++ cparser/Elab.ml | 2 +- ia32/PrintAsm.ml | 18 +++++++++--------- 5 files changed, 63 insertions(+), 33 deletions(-) diff --git a/Makefile b/Makefile index 4237f2a..752a8e6 100644 --- a/Makefile +++ b/Makefile @@ -82,6 +82,14 @@ DRIVER=Compiler.v Complements.v FILES=$(LIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) +# Symbolic links vs. copy + +ifneq (,$(findstring CYGWIN,$(shell uname -s))) +SLN=cp +else +SLN=ln -s +endif + proof: $(FILES:.v=.vo) extraction: @@ -91,15 +99,15 @@ extraction: ccomp: driver/Configuration.ml $(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \ - && rm -f ccomp && ln -s _build/driver/Driver.native ccomp + && rm -f ccomp && $(SLN) _build/driver/Driver.native ccomp ccomp.prof: driver/Configuration.ml $(OCAMLBUILD) $(OCB_OPTIONS) Driver.p.native \ - && rm -f ccomp.prof && ln -s _build/driver/Driver.p.native ccomp.prof + && rm -f ccomp.prof && $(SLN) _build/driver/Driver.p.native ccomp.prof ccomp.byte: driver/Configuration.ml $(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \ - && rm -f ccomp.byte && ln -s _build/driver/Driver.d.byte ccomp.byte + && rm -f ccomp.byte && $(SLN) _build/driver/Driver.d.byte ccomp.byte runtime: $(MAKE) -C runtime diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 26815a1..b6ab3ba 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -25,7 +25,13 @@ open Csyntax (** Record the declarations of global variables and associate them with the corresponding atom. *) -let decl_atom : (AST.ident, Env.t * C.decl) Hashtbl.t = Hashtbl.create 103 +type atom_info = + { a_storage: C.storage; + a_env: Env.t; + a_type: C.typ; + a_fundef: C.fundef option } + +let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103 (** Hooks -- overriden in machine-dependent CPragmas module *) @@ -135,10 +141,10 @@ let name_for_string_literal env s = let name = Printf.sprintf "__stringlit_%d" !stringNum in let id = intern_string name in Hashtbl.add decl_atom id - (env, (C.Storage_static, - Env.fresh_ident name, - C.TPtr(C.TInt(C.IChar,[C.AConst]),[]), - None)); + { a_storage = C.Storage_static; + a_env = env; + a_type = C.TPtr(C.TInt(C.IChar,[C.AConst]),[]); + a_fundef = None }; Sections.define_stringlit id; Hashtbl.add stringTable s id; id @@ -701,9 +707,11 @@ let convertFundef env fd = fd.fd_locals in let body' = convertStmt env fd.fd_body in let id' = intern_string fd.fd_name.name in - let decl = - (fd.fd_storage, fd.fd_name, Cutil.fundef_typ fd, None) in - Hashtbl.add decl_atom id' (env, decl); + Hashtbl.add decl_atom id' + { a_storage = fd.fd_storage; + a_env = env; + a_type = Cutil.fundef_typ fd; + a_fundef = Some fd }; Sections.define_function id'; Datatypes.Coq_pair(id', Internal {fn_return = ret; fn_params = params; @@ -850,7 +858,7 @@ let rec type_is_volatile env t = | C.TArray(t', _, _) -> type_is_volatile env t' | _ -> false -let convertGlobvar env (sto, id, ty, optinit as decl) = +let convertGlobvar env (sto, id, ty, optinit) = let id' = intern_string id.name in let ty' = convertTyp env ty in let init' = @@ -859,7 +867,11 @@ let convertGlobvar env (sto, id, ty, optinit as decl) = if sto = C.Storage_extern then [] else [Init_space(Csyntax.sizeof ty')] | Some i -> convertInit env ty i in - Hashtbl.add decl_atom id' (env, decl); + Hashtbl.add decl_atom id' + { a_storage = sto; + a_env = env; + a_type = ty; + a_fundef = None }; Sections.define_variable id' (match Cutil.sizeof env ty with Some sz -> sz | None -> max_int) (type_is_readonly env ty); @@ -978,36 +990,35 @@ let convertProgram p = let atom_is_static a = try - let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in - sto = C.Storage_static + match Hashtbl.find decl_atom a with + | { a_storage = C.Storage_static } -> true + (* We do not inline functions, but at least let's not make them globals *) + | { a_fundef = Some { fd_inline = true } } -> true + | _ -> false with Not_found -> false let atom_is_extern a = try - let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in - sto = C.Storage_extern + let i = Hashtbl.find decl_atom a in i.a_storage = C.Storage_extern with Not_found -> false let atom_is_readonly a = try - let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in - type_is_readonly env ty + let i = Hashtbl.find decl_atom a in type_is_readonly i.a_env i.a_type with Not_found -> false let atom_sizeof a = try - let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in - Cutil.sizeof env ty + let i = Hashtbl.find decl_atom a in Cutil.sizeof i.a_env i.a_type with Not_found -> None let atom_alignof a = try - let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in - Cutil.alignof env ty + let i = Hashtbl.find decl_atom a in Cutil.alignof i.a_env i.a_type with Not_found -> None diff --git a/configure b/configure index d49428d..5744c54 100755 --- a/configure +++ b/configure @@ -36,6 +36,7 @@ Supported targets: ia32-linux (x86 32 bits, Linux) ia32-bsd (x86 32 bits, BSD) ia32-macosx (x86 32 bits, MacOS X) + ia32-cygwin (x86 32 bits, Cygwin environment under Windows) manual (edit configuration file by hand) Options: @@ -125,6 +126,16 @@ case "$target" in clinker="gcc -arch i386" libmath="" need_stdlib_wrapper="true";; + ia32-cygwin) + arch="ia32" + variant="standard" + system="cygwin" + cc="gcc -m32" + cprepro="gcc -m32 -U__GNUC__ -E" + casm="gcc -m32 -c" + clinker="gcc -m32" + libmath="-lm" + need_stdlib_wrapper="false";; manual) ;; "") diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 2ae7c7e..b79aa10 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1021,7 +1021,7 @@ let elab_expr loc env a = | TInt _, TPtr(ty2, a2) when is_literal_0 b2 -> { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, a2) } | ty1, ty2 -> - match combine_types env ty1 ty2 with + match combine_types ~noattrs:true env ty1 ty2 with | None -> error ("the second and third arguments of '? :' have incompatible types") | Some tyres -> diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 32bb073..f3cb519 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -20,14 +20,14 @@ open Asm (* Recognition of target ABI and asm syntax *) -type target = ELF | AOUT | MacOS +type target = ELF | MacOS | Cygwin let target = match Configuration.system with | "macosx" -> MacOS | "linux" -> ELF | "bsd" -> ELF - | "cygwin" -> AOUT + | "cygwin" -> Cygwin | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") (* On-the-fly label renaming *) @@ -55,7 +55,7 @@ let coqint oc n = let raw_symbol oc s = match target with | ELF -> fprintf oc "%s" s - | MacOS | AOUT -> fprintf oc "_%s" s + | MacOS | Cygwin -> fprintf oc "_%s" s let re_variadic_stub = Str.regexp "\\(.*\\)\\$[if]*$" @@ -72,7 +72,7 @@ let symbol_offset oc (symb, ofs) = let label oc lbl = match target with | ELF -> fprintf oc ".L%d" lbl - | MacOS | AOUT -> fprintf oc "L%d" lbl + | MacOS | Cygwin -> fprintf oc "L%d" lbl let comment = "#" @@ -146,7 +146,7 @@ let (text, data, const_data, float_literal, jumptable_literal) = ".const", ".const_data", ".text") - | AOUT -> + | Cygwin -> (".text", ".data", ".section .rdata,\"dr\"", @@ -157,8 +157,8 @@ let (text, data, const_data, float_literal, jumptable_literal) = let stack_alignment = match target with - | ELF | AOUT -> 8 (* minimum is 4, 8 is better for perfs *) - | MacOS -> 16 (* mandatory *) + | ELF | Cygwin -> 8 (* minimum is 4, 8 is better for perfs *) + | MacOS -> 16 (* mandatory *) let int32_align n a = if n >= 0l @@ -184,8 +184,8 @@ let rec log2 n = let print_align oc n = match target with - | ELF -> fprintf oc " .align %d\n" n - | AOUT | MacOS -> fprintf oc " .align %d\n" (log2 n) + | ELF | Cygwin -> fprintf oc " .align %d\n" n + | MacOS -> fprintf oc " .align %d\n" (log2 n) let need_masks = ref false -- cgit v1.2.3