diff options
| -rw-r--r-- | Makefile.menhir | 37 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 9 | ||||
| -rwxr-xr-x | configure | 4 | ||||
| -rw-r--r-- | cparser/Cerrors.ml | 7 | ||||
| -rw-r--r-- | cparser/Parse.ml | 2 | ||||
| -rw-r--r-- | cparser/Rename.ml | 29 | ||||
| -rw-r--r-- | cparser/Rename.mli | 2 | ||||
| -rw-r--r-- | debug/DebugInit.ml | 38 | ||||
| -rw-r--r-- | driver/Clflags.ml | 3 | ||||
| -rw-r--r-- | driver/Driver.ml | 39 | ||||
| -rw-r--r-- | driver/Optionsprinter.ml | 1 |
11 files changed, 66 insertions, 105 deletions
diff --git a/Makefile.menhir b/Makefile.menhir index b72c52f3..1530536f 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -47,40 +47,3 @@ endif %.ml %.mli: %.mly $(MENHIR) $(MENHIR_MODE) $(MENHIR_FLAGS) $< - -# Note 1: finding where MenhirLib has been installed would be easier if we -# could depend on ocamlfind, but as far as I understand and as of today, -# CompCert can be compiled and linked even in the absence of ocamlfind. -# So, we should not require ocamlfind. - -# Note 2: Menhir has options --suggest-comp-flags and --suggest-link-flags -# which we are supposed to help solve this difficulty. However, they don't -# work for us out of the box, because if Menhir has been installed using -# ocamlfind, then Menhir will suggest using ocamlfind (i.e. it will suggest -# -package and -linkpkg options), which we don't want to do. - -# Solution: Ask Menhir first. If Menhir answers "-package menhirLib", then -# Menhir was installed with ocamlfind, so we should not ask Menhir, but we -# can instead ask ocamlfind where Menhir's library was installed. Otherwise, -# Menhir answers directly with a "-I ..." directive, which we use. - -ifndef MENHIR_INCLUDES - -ifeq ($(MENHIR_TABLE),true) - - MENHIR_SUGGESTION = $(MENHIR) $(MENHIR_MODE) --suggest-comp-flags - - MENHIR_INCLUDES := $(shell \ - if $(MENHIR_SUGGESTION) | grep -e "-package" >/dev/null ; then \ - echo "-I `ocamlfind query menhirLib`" ; \ - else \ - $(MENHIR_SUGGESTION) ; \ - fi) - -else - - MENHIR_INCLUDES = - -endif - -endif diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 14976d01..5d75aa6a 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -357,12 +357,15 @@ let make_builtin_memcpy args = let sz1 = match Initializers.constval !comp_env sz with | Errors.OK(Vint n) -> n - | _ -> error "argument 3 of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.zero in + | _ -> error "size argument of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.zero in let al1 = match Initializers.constval !comp_env al with | Errors.OK(Vint n) -> n - | _ -> error "argument 4 of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.one in - (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *) + | _ -> error "alignment argument of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.one in + if Integers.Int.is_power2 al1 = None then + error "alignment argument of '__builtin_memcpy_aligned' must be a power of 2"; + if Integers.Int.modu sz1 al1 <> Integers.Int.zero then + error "alignment argument of '__builtin_memcpy_aligned' must be a divisor of the size"; (* Issue #28: must decay array types to pointer types *) Ebuiltin(EF_memcpy(sz1, al1), Tcons(typeconv(typeof dst), @@ -404,8 +404,9 @@ echo "Testing Menhir... " | tr -d '\n' menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` case "$menhir_ver" in 20[0-9][0-9][0-9][0-9][0-9][0-9]) - if test "$menhir_ver" -ge $MENHIR_REQUIRED; then + if test "$menhir_ver" -ge $MENHIR_REQUIRED; then echo "version $menhir_ver -- good!" + menhir_includes="-I `menhir --suggest-menhirLib`" else echo "version $menhir_ver -- UNSUPPORTED" echo "Error: CompCert requires Menhir version $MENHIR_REQUIRED or later." @@ -479,6 +480,7 @@ LIBDIR=$libdir MANDIR=$sharedir/man SHAREDIR=$sharedir OCAML_OPT_COMP=$ocaml_opt_comp +MENHIR_INCLUDES=$menhir_includes EOF if $merlin; then cat >> Makefile.config <<EOF diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index c50e12d9..a38cceee 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -21,7 +21,10 @@ open Commandline let error_fatal = ref false let color_diagnostics = let term = try Sys.getenv "TERM" with Not_found -> "" in - ref (Unix.isatty Unix.stderr && term <> "dumb" && term <>"") + let activate = try + (Unix.isatty Unix.stderr && term <> "dumb" && term <>"") + with _ -> false in + ref activate let num_errors = ref 0 let num_warnings = ref 0 @@ -197,7 +200,7 @@ let classify_warning w = SuppressedMsg,None let cprintf fmt c = - if Unix.isatty Unix.stderr && !color_diagnostics then + if !color_diagnostics then fprintf fmt c else ifprintf fmt c diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 507aea36..dceb9b11 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -24,7 +24,7 @@ let transform_program t p name = (run_pass Unblock.program 'b' (run_pass Bitfields.program 'f' p)))) in - (Rename.program p1 (Filename.chop_suffix name ".c")) + (Rename.program p1) let parse_transformations s = let t = ref CharSet.empty in diff --git a/cparser/Rename.ml b/cparser/Rename.ml index c62c6763..c1f31977 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -43,17 +43,6 @@ let enter_public env 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 file = String.map (fun a -> match a with 'a'..'z' | 'A'..'Z' | '0'..'9' -> a | _ -> '_') file in - 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, don't rename a second time *) @@ -260,7 +249,7 @@ let reserve_builtins () = (* Reserve global declarations with public visibility *) -let rec reserve_public env file = function +let rec reserve_public env = function | [] -> env | dcl :: rem -> let env' = @@ -268,27 +257,21 @@ let rec reserve_public env file = function | Gdecl(sto, id, _, _) -> begin match sto with | Storage_default | Storage_extern -> enter_public env id - | Storage_static -> if !Clflags.option_rename_static then - enter_static env id file - else - env + | Storage_static -> env | _ -> assert false end | Gfundef f -> begin match f.fd_storage with | Storage_default | Storage_extern -> enter_public env f.fd_name - | Storage_static -> if !Clflags.option_rename_static then - enter_static env f.fd_name file - else - env + | Storage_static -> env | _ -> assert false end | _ -> env in - reserve_public env' file rem + reserve_public env' rem (* Rename the program *) -let program p file = +let program p = globdecls - (reserve_public (reserve_builtins()) file p) + (reserve_public (reserve_builtins()) p) [] p diff --git a/cparser/Rename.mli b/cparser/Rename.mli index c4ef2228..818a51bc 100644 --- a/cparser/Rename.mli +++ b/cparser/Rename.mli @@ -13,4 +13,4 @@ (* *) (* *********************************************************************) -val program : C.program -> string -> C.program +val program : C.program -> C.program diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml index b3fedb00..ed22f7c2 100644 --- a/debug/DebugInit.ml +++ b/debug/DebugInit.ml @@ -10,7 +10,10 @@ (* *) (* *********************************************************************) +open Clflags +open Commandline open Debug +open Driveraux let default_debug = { @@ -48,7 +51,6 @@ let init_debug () = implem := if Configuration.system = "diab" then let gen = (fun a b -> Some (Dwarfgen.gen_diab_debug_info a b)) in - Clflags.option_gdwarf := 2; (* Dwarf 2 is the only supported target *) {default_debug with generate_debug_info = gen; add_diab_info = DebugInformation.add_diab_info; add_fun_addr = DebugInformation.diab_add_fun_addr;} @@ -60,7 +62,39 @@ let init_none () = implem := default_implem let init () = - if !Clflags.option_g then + if !option_g then init_debug () else init_none () + +let gnu_debugging_help = +" -gdwarf- Generate debug information in DWARF v2 or DWARF v3\n" + +let debugging_help = +"Debugging options:\n\ +\ -g Generate debugging information\n\ +\ -g<n> Control generation of debugging information\n\ +\ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals \n\ +\ without locations, <n>=3: full;)\n" +^ (if gnu_system then gnu_debugging_help else "") + +let gnu_debugging_actions = + let version version () = + option_g:=true; + option_gdwarf:=version + in + [Exact "-gdwarf-2", Unit (version 2); + Exact "-gdwarf-3", Unit (version 3);] + +let debugging_actions = + let depth depth () = + option_g:=true; + option_gdepth := depth + in + [Exact "-g", Unit (depth 3); + Exact "-g0", Unset option_g; + Exact "-g1", Unit (depth 1); + Exact "-g2", Unit (depth 2); + Exact "-g3", Unit (depth 3);] + @ + (if gnu_system then gnu_debugging_actions else []) diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6a695aa4..c7a5d3bf 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -45,7 +45,7 @@ let option_dmach = ref false let option_dasm = ref false let option_sdump = ref false let option_g = ref false -let option_gdwarf = ref 2 +let option_gdwarf = ref (if Configuration.system = "diab" then 2 else 3) let option_gdepth = ref 3 let option_o = ref (None: string option) let option_E = ref false @@ -60,6 +60,5 @@ 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 let stdlib_path = ref Configuration.stdlib_path let use_standard_headers = ref Configuration.has_standard_headers diff --git a/driver/Driver.ml b/driver/Driver.ml index edee32cf..a273a91a 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -255,20 +255,6 @@ let version_string = else "The CompCert C verified compiler, version "^ Version.version ^ "\n" -let gnu_system = Configuration.system <> "diab" - -let gnu_debugging_help = -" -gdwarf- Generate debug information in DWARF v2 or DWARF v3\n" - -let debugging_help = -"Debugging options:\n\ -\ -g Generate debugging information\n\ -\ -gdepth <n> Control generation of debugging information\n\ -\ (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals\n\ -\ without locations, <n>=3: full;)\n" -^ (if gnu_system then gnu_debugging_help else "")^ -" -frename-static Rename static functions and declarations\n" - let target_help = if Configuration.arch = "arm" then "Target processor options:\n\ \ -mthumb Use Thumb2 instruction encoding\n\ @@ -305,7 +291,7 @@ Processing options:\n\ \ -finline-asm Support inline 'asm' statements [off]\n\ \ -fall Activate all language support options above\n\ \ -fnone Turn off all language support options above\n" ^ - debugging_help ^ + DebugInit.debugging_help ^ "Optimization options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -O Optimize the compiled code [on by default]\n\ \ -O0 Do not optimize the compiled code\n\ @@ -345,6 +331,8 @@ General options:\n\ \ -v Print external commands before invoking them\n\ \ -timings Show the time spent in various compiler passes\n\ \ -version Print the version string and exit\n\ +\ -target <value> Generate code for the given target\n\ +\ -conf <file> Read configuration from file\n\ \ @<file> Read command line options from <file>\n" ^ Cerrors.warning_help ^ "Interpreter mode:\n\ @@ -380,9 +368,6 @@ let num_input_files = ref 0 let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in - let dwarf_version version () = - option_g:=true; - option_gdwarf := version in [ (* Getting help *) Exact "-help", Unit print_usage_and_exit; @@ -401,21 +386,11 @@ let cmdline_actions = @ prepro_actions @ (* Language support options -- more below *) [ Exact "-fall", Unit (set_all language_support_options); - Exact "-fnone", Unit (unset_all language_support_options); -(* Debugging options *) - Exact "-g", Unit (dwarf_version 3);] @ - (if gnu_system then - [ Exact "-gdwarf-2", Unit (dwarf_version 2); - Exact "-gdwarf-3", Unit (dwarf_version 3);] - else []) @ - [ Exact "-frename-static", Set option_rename_static; - Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin - option_g := false - end else begin - option_g := true; - option_gdepth := if n > 3 then 3 else n - end); + Exact "-fnone", Unit (unset_all language_support_options);] + (* Debugging options *) + @ DebugInit.debugging_actions @ (* Code generation options -- more below *) + [ Exact "-O0", Unit (unset_all optimization_options); Exact "-O", Unit (set_all optimization_options); _Regexp "-O[123]$", Unit (set_all optimization_options); diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml index 9dce8592..00b5f5ec 100644 --- a/driver/Optionsprinter.ml +++ b/driver/Optionsprinter.ml @@ -64,7 +64,6 @@ let print_clflags oc = p_jmember oc "small_data" p_jint !option_small_data; p_jmember oc "small_data" p_jint !option_small_const; p_jmember oc "timings" p_jbool !option_timings; - p_jmember oc "rename_static" p_jbool !option_rename_static; fprintf oc "\n}" let print_struct_passing_style oc = function |