diff options
35 files changed, 311 insertions, 274 deletions
@@ -1,9 +1,15 @@ -Release 2.7.1, 2016-07-10 +Release 2.7.1, 2016-07-18 ========================= -- Ported to Coq 8.5pl2. No other changes in functionality. +- Ported to Coq 8.5pl2. +Bug fixing: +- Fixed a compile-time assertion failure involving builtins + taking a 64-bit integer parameter and given an unsigned 32-bit integer + argument. +- Updates to the Cminor parser. + Release 2.7, 2016-06-29 ======================= diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index c82f5401..65f244b5 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -136,6 +136,7 @@ rule token = parse | "]" { RBRACKET } | "readonly" { READONLY } | "return" { RETURN } + | "runtime" { RUNTIME } | ")" { RPAREN } | ";" { SEMICOLON } | "/" { SLASH } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 7fa6500a..94b50810 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -38,6 +38,8 @@ let mkef sg toks = EF_external(coqstring_of_camlstring s, sg) | [EFT_tok "builtin"; EFT_string s] -> EF_builtin(coqstring_of_camlstring s, sg) + | [EFT_tok "runtime"; EFT_string s] -> + EF_runtime(coqstring_of_camlstring s, sg) | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c] -> EF_vload c | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c] -> @@ -348,6 +350,7 @@ let mkmatch expr cases = %token READONLY %token RETURN %token RPAREN +%token RUNTIME %token SEMICOLON %token SINGLE %token SINGLEOFINT @@ -719,6 +722,7 @@ eftok: | VOLATILE { EFT_tok "volatile" } | EXTERN { EFT_tok "extern" } | BUILTIN { EFT_tok "builtin" } + | RUNTIME { EFT_tok "runtime" } | memory_chunk { EFT_chunk $1 } ; diff --git a/cparser/Cerrors.ml b/cparser/Cerrors.ml index 5c077f37..a4d1a3f8 100644 --- a/cparser/Cerrors.ml +++ b/cparser/Cerrors.ml @@ -30,7 +30,7 @@ exception Abort to print its message, as opposed to [Format], and does not automatically introduce indentation and a final dot into the message. This is useful for multi-line messages. *) - + let fatal_error_raw fmt = incr num_errors; Printf.kfprintf @@ -67,4 +67,6 @@ let check_errors () = (if !num_warnings = 1 then "" else "s"); !num_errors > 0 || (!warn_error && !num_warnings > 0) - +let raise_on_errors () = + if !num_errors > 0 || (!warn_error && !num_warnings > 0) then + raise Abort diff --git a/cparser/Cerrors.mli b/cparser/Cerrors.mli index 3e315fad..313573c3 100644 --- a/cparser/Cerrors.mli +++ b/cparser/Cerrors.mli @@ -22,3 +22,4 @@ val error : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a val warning : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a val info : ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a val check_errors : unit -> bool +val raise_on_errors : unit -> unit diff --git a/cparser/Elab.ml b/cparser/Elab.ml index a2a84970..1586f142 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -56,13 +56,28 @@ let elab_loc l = (l.filename, l.lineno) let top_declarations = ref ([] : globdecl list) -let emit_elab ?(enter:bool=true) env loc td = +(* Environment that records the top declarations of functions and + variables with external or internal linkage. Used for + analyzing "extern" declarations. *) + +let top_environment = ref Env.empty + +let emit_elab ?(debuginfo = true) ?(linkage = false) env loc td = let loc = elab_loc loc in let dec ={ gdesc = td; gloc = loc } in - if enter then Debug.insert_global_declaration env dec; - top_declarations := dec :: !top_declarations + if debuginfo then Debug.insert_global_declaration env dec; + top_declarations := dec :: !top_declarations; + if linkage then begin + match td with + | Gdecl(sto, id, ty, init) -> + top_environment := Env.add_ident !top_environment id sto ty + | Gfundef f -> + top_environment := + Env.add_ident !top_environment f.fd_name f.fd_storage (fundef_typ f) + | _ -> () + end -let reset() = top_declarations := [] +let reset() = top_declarations := []; top_environment := Env.empty let elaborated_program () = let p = !top_declarations in @@ -92,6 +107,78 @@ let redef fn env arg = | None -> false | Some(id, info) -> Env.in_current_scope env id +(* Auxiliaries for handling declarations and redeclarations *) + +let combine_toplevel_definitions loc env s old_sto old_ty sto ty = + let new_ty = + match combine_types AttrCompat env old_ty ty with + | Some new_ty -> + new_ty + | None -> + let id = Env.fresh_ident s in + error loc + "redefinition of '%s' with incompatible type.@ \ + Previous declaration: %a.@ \ + New declaration: %a" + s Cprint.simple_decl (id, old_ty) Cprint.simple_decl (id, ty); + ty in + let new_sto = + (* The only case not allowed is removing static *) + match old_sto,sto with + | Storage_static,Storage_static + | Storage_extern,Storage_extern + | Storage_register,Storage_register + | Storage_default,Storage_default -> sto + | _,Storage_static -> + 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 + in + (new_sto, new_ty) + +let enter_or_refine_ident local loc env s sto ty = + (* Check for illegal redefinitions: + - a name that was previously a typedef + - a variable that was already declared in the same local scope + (unless both old and new declarations are extern) + - an enum that was already declared in the same scope. + Redefinition of a variable at global scope (or extern) is treated below. *) + if redef Env.lookup_typedef env s then + error loc "redefinition of typedef '%s' as different kind of symbol" s; + begin match previous_def Env.lookup_ident env s with + | Some(id, II_ident(old_sto, old_ty)) + when local && Env.in_current_scope env id + && not (sto = Storage_extern && old_sto = Storage_extern) -> + error loc "redefinition of local variable '%s'" s + | Some(id, II_enum _) when Env.in_current_scope env id -> + error loc "redefinition of enumerator '%s'" s + | _ -> + () + end; + (* For a block-scoped, non-"extern" variable, a new declaration + is entered, and it has no linkage. *) + if local && sto <> Storage_extern then begin + let (id, env') = Env.enter_ident env s sto ty in + (id, sto, env', ty, false) + end else begin + (* For a file-scoped or "extern" variable, we need to check against + prior declarations of this variable with internal or external linkage. + The variable has linkage. *) + match previous_def Env.lookup_ident !top_environment s with + | Some(id, II_ident(old_sto, old_ty)) -> + let (new_sto, new_ty) = + combine_toplevel_definitions loc env s old_sto old_ty sto ty in + (id, new_sto, Env.add_ident env id new_sto new_ty, new_ty, true) + | _ -> + let (id, env') = Env.enter_ident env s sto ty in + (id, sto, env', ty, true) + end + (* Forward declarations *) let elab_expr_f : (cabsloc -> Env.t -> Cabs.expression -> C.exp * Env.t) ref @@ -346,6 +433,7 @@ let elab_attribute env = function begin match elab_attr_arg loc env a with | AInt n when is_power_of_two n -> [AAlignas (Int64.to_int n)] | _ -> warning loc "bad _Alignas value, ignored"; [] + | exception Wrong_attr_arg -> warning loc "bad _Alignas value, ignored"; [] end | ALIGNAS_ATTR (_, loc) -> warning loc "_Alignas takes exactly one parameter, ignored"; [] @@ -1338,9 +1426,11 @@ let elab_expr loc env a = | VARIABLE n when not (Env.ident_is_bound env n) -> warning "implicit declaration of function '%s'" n; let ty = TFun(TInt(IInt, []), None, false, []) in + (* Check against other definitions and enter in env *) + let (id, sto, env, ty, linkage) = + enter_or_refine_ident true loc env n Storage_extern ty in (* Emit an extern declaration for it *) - let id = Env.fresh_ident n in - emit_elab env loc (Gdecl(Storage_extern, id, ty, None)); + emit_elab ~linkage env loc (Gdecl(sto, id, ty, None)); { edesc = EVar id; etyp = ty },env | _ -> elab env a1 in let bl = mmap elab env al in @@ -1830,48 +1920,6 @@ let enter_typedefs loc env sto dl = emit_elab env loc (Gtypedef(id, ty)); env') env dl -let enter_or_refine_ident local loc env s sto ty = - if redef Env.lookup_typedef env s then - error loc "redefinition of typedef '%s' as different kind of symbol" s; - match previous_def Env.lookup_ident env s with - | Some(id, II_ident(old_sto, old_ty)) - when sto = Storage_extern || Env.in_current_scope env id -> - if local && Env.in_current_scope env id then - error loc "redefinition of local variable '%s'" s; - let new_ty = - match combine_types AttrCompat env old_ty ty with - | Some new_ty -> - new_ty - | None -> - 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 - | Storage_static,Storage_static - | Storage_extern,Storage_extern - | Storage_register,Storage_register - | Storage_default,Storage_default -> sto - | _,Storage_static -> - 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 - in - (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,ty) - | _ -> - 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 *) if sto = Storage_register && not local then @@ -1888,7 +1936,8 @@ 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,ty) = enter_or_refine_ident local loc env s sto1 ty in + let (id, sto', env1, ty, linkage) = + 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 *) @@ -1903,7 +1952,7 @@ let enter_decdefs local loc env sto dl = ((sto', id, ty', init') :: decls, env2) else begin (* Global definition *) - emit_elab env2 loc (Gdecl(sto', id, ty', init')); + emit_elab ~linkage env2 loc (Gdecl(sto', id, ty', init')); (decls, env2) end in let (decls, env') = List.fold_left enter_decdef ([], env) dl in @@ -2048,7 +2097,8 @@ let elab_fundef env spec name defs body loc = | _ -> 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 env1 s sto ty in + let (fun_id, sto1, env1, _, _) = + enter_or_refine_ident false loc env1 s sto ty in (* Enter parameters and extra declarations in the environment *) let env2 = List.fold_left (fun e (id, ty) -> Env.add_ident e id Storage_default ty) @@ -2058,9 +2108,10 @@ let elab_fundef env spec name defs body loc = env2 extra_decls in (* Define "__func__" and enter it in the environment *) let (func_ty, func_init) = __func__type_and_init s in - let (func_id, _, env3, func_ty) = + let (func_id, _, env3, func_ty, _) = enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in - emit_elab ~enter:false env3 loc (Gdecl(Storage_static, func_id, func_ty, Some func_init)); + emit_elab ~debuginfo:false env3 loc + (Gdecl(Storage_static, func_id, func_ty, Some func_init)); (* Elaborate function body *) let body1 = !elab_funbody_f ty_ret env3 body in (* Special treatment of the "main" function *) @@ -2095,7 +2146,7 @@ let elab_fundef env spec name defs body loc = fd_vararg = vararg; fd_locals = []; fd_body = body3 } in - emit_elab env1 loc (Gfundef fn); + emit_elab ~linkage:true env1 loc (Gfundef fn); env1 (* Definitions *) diff --git a/cparser/Parse.ml b/cparser/Parse.ml index c125e653..3f60ebb4 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -74,6 +74,7 @@ let preprocessed_file transfs name sourcefile = | Parser.Parser.Inter.Timeout_pr -> assert false | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in let p1 = Timing.time "Elaboration" Elab.elab_file ast in + Cerrors.raise_on_errors (); Timing.time2 "Emulations" transform_program t p1 name with | Cerrors.Abort -> diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index 471318af..dfde9136 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -53,13 +53,10 @@ let lookup_types: (string, int) Hashtbl.t = Hashtbl.create 7 (* Translate a C.typ to a string needed for hashing *) let typ_to_string ty = - let buf = Buffer.create 7 in - let chan = Format.formatter_of_buffer buf in Cprint.print_debug_idents := true; - Cprint.typ chan ty; + let s = Format.asprintf "%a" Cprint.typ ty in Cprint.print_debug_idents := false; - Format.pp_print_flush chan (); - Buffer.contents buf + s (* Helper functions for the attributes *) let strip_attributes typ = strip_attributes_type typ [AConst; AVolatile] diff --git a/driver/Driver.ml b/driver/Driver.ml index 6d8cf9ac..eccd233c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -86,29 +86,35 @@ let compile_cminor_file ifile ofile = Sections.initialize(); let ic = open_in ifile in let lb = Lexing.from_channel ic in - try - match Compiler.transf_cminor_program - (CMtypecheck.type_program - (CMparser.prog CMlexer.token lb)) with + (* Parse cminor *) + let cm = + try CMtypecheck.type_program (CMparser.prog CMlexer.token lb) + with Parsing.Parse_error -> + eprintf "File %s, character %d: Syntax error\n" + ifile (Lexing.lexeme_start lb); + exit 2 + | CMlexer.Error msg -> + eprintf "File %s, character %d: %s\n" + ifile (Lexing.lexeme_start lb) msg; + exit 2 + | CMtypecheck.Error msg -> + eprintf "File %s, type-checking error:\n%s" + ifile msg; + exit 2 in + (* Convert to Asm *) + let asm = + match Compiler.apply_partial + (Compiler.transf_cminor_program cm) + Asmexpand.expand_program with + | Errors.OK asm -> + asm | Errors.Error msg -> eprintf "%s: %a" ifile print_error msg; - exit 2 - | Errors.OK p -> - let oc = open_out ofile in - PrintAsm.print_program oc p; - close_out oc - with Parsing.Parse_error -> - eprintf "File %s, character %d: Syntax error\n" - ifile (Lexing.lexeme_start lb); - exit 2 - | CMlexer.Error msg -> - eprintf "File %s, character %d: %s\n" - ifile (Lexing.lexeme_start lb) msg; - exit 2 - | CMtypecheck.Error msg -> - eprintf "File %s, type-checking error:\n%s" - ifile msg; - exit 2 + exit 2 in + (* Print Asm in text form *) + let oc = open_out ofile in + PrintAsm.print_program oc asm; + close_out oc (* Processing of a .c file *) @@ -327,6 +333,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)\n\ \ -dltl Save LTL after register allocation in <file>.ltl\n\ \ -dmach Save generated Mach code in <file>.mach\n\ \ -dasm Save generated assembly in <file>.s\n\ +\ -dall Save all generated intermidate files in <file>.<ext>\n\ \ -sdump Save info for post-linking validation in <file>.json\n\ \ -doptions Save the compiler configurations in <file>.opt.json\n\ General options:\n\ @@ -435,6 +442,17 @@ let cmdline_actions = Exact "-dalloctrace", Set option_dalloctrace; Exact "-dmach", Set option_dmach; Exact "-dasm", Set option_dasm; + Exact "-dall", Self (fun _ -> + option_dprepro := true; + option_dparse := true; + option_dcmedium := true; + option_dclight := true; + option_dcminor := true; + option_drtl := true; + option_dalloctrace := true; + option_dmach := true; + option_dasm := true; + dump_options:=true); Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); Exact "-doptions", Set dump_options; diff --git a/driver/Interp.ml b/driver/Interp.ml index 5c2158ae..f42bed32 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -387,10 +387,12 @@ let do_external_function id sg ge w args m = match camlstring_of_coqstring id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> - print_string (do_printf m fmt args'); + let fmt' = do_printf m fmt args' in + let len = coqint_of_camlint (Int32.of_int (String.length fmt')) in + print_string fmt'; flush stdout; convert_external_args ge args sg.sig_args >>= fun eargs -> - Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m) + Some(((w, [Event_syscall(id, eargs, EVint len)]), Vint len), m) | _ -> None diff --git a/test/Makefile b/test/Makefile index 5aa115d8..b469eec2 100644 --- a/test/Makefile +++ b/test/Makefile @@ -11,6 +11,3 @@ bench: clean: for i in $(DIRS); do $(MAKE) -C $$i clean; done - -ccheck: - for i in $(DIRS); do $(MAKE) -C $$i ccheck; done diff --git a/test/c/Makefile b/test/c/Makefile index 59a0d834..c0794ff3 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -1,11 +1,7 @@ include ../../Makefile.config CCOMP=../../ccomp -CCOMPFLAGS=-stdlib ../../runtime -dc -dclight -dasm -ifeq ($(CCHECKLINK),true) -CCHECK=../../cchecklink -CCOMPFLAGS+= -sdump -endif +CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime -dc -dclight -dasm CFLAGS=-O1 -Wall @@ -42,12 +38,6 @@ test: fi; \ done -ccheck: - @for i in $(PROGS); do \ - echo "---- $$i"; \ - $(CCHECK) -exe $$i.compcert $$i.sdump; \ - done - test_gcc: @for i in $(PROGS); do \ if ./$$i.gcc | cmp -s - Results/$$i; \ diff --git a/test/c/Results/fannkuch b/test/c/Results/fannkuch index be1815d4..15d56d61 100644 --- a/test/c/Results/fannkuch +++ b/test/c/Results/fannkuch @@ -1,31 +1,31 @@ -12345678910 -21345678910 -23145678910 -32145678910 -31245678910 -13245678910 -23415678910 -32415678910 -34215678910 -43215678910 -42315678910 -24315678910 -34125678910 -43125678910 -41325678910 -14325678910 -13425678910 -31425678910 -41235678910 -14235678910 -12435678910 -21435678910 -24135678910 -42135678910 -23451678910 -32451678910 -34251678910 -43251678910 -42351678910 -24351678910 -Pfannkuchen(10) = 38 +1234567891011 +2134567891011 +2314567891011 +3214567891011 +3124567891011 +1324567891011 +2341567891011 +3241567891011 +3421567891011 +4321567891011 +4231567891011 +2431567891011 +3412567891011 +4312567891011 +4132567891011 +1432567891011 +1342567891011 +3142567891011 +4123567891011 +1423567891011 +1243567891011 +2143567891011 +2413567891011 +4213567891011 +2345167891011 +3245167891011 +3425167891011 +4325167891011 +4235167891011 +2435167891011 +Pfannkuchen(11) = 51 diff --git a/test/c/Results/fib b/test/c/Results/fib index 3ed84615..53a71233 100644 --- a/test/c/Results/fib +++ b/test/c/Results/fib @@ -1 +1 @@ -fib(36) = 24157817 +fib(40) = 165580141 diff --git a/test/c/fannkuch.c b/test/c/fannkuch.c index 9cc7a693..7feaf6d7 100644 --- a/test/c/fannkuch.c +++ b/test/c/fannkuch.c @@ -98,7 +98,7 @@ fannkuch( int n ) int main( int argc, char* argv[] ) { - int n = (argc>1) ? atoi(argv[1]) : 10; + int n = (argc>1) ? atoi(argv[1]) : 11; printf("Pfannkuchen(%d) = %ld\n", n, fannkuch(n)); return 0; diff --git a/test/c/fft.c b/test/c/fft.c index 884a8568..a4755044 100644 --- a/test/c/fft.c +++ b/test/c/fft.c @@ -143,13 +143,13 @@ int dfft(double x[], double y[], int np) /* Test harness */ -double * xr, * xi; +#define NRUNS 20 int main(int argc, char ** argv) { - int n, np, npm, n2, i, j; + int n, np, npm, n2, i, j, nruns; double enp, t, y, z, zr, zi, zm, a; - double * pxr, * pxi; + double * xr, * xi, * pxr, * pxi; if (argc >= 2) n = atoi(argv[1]); else n = 18; np = 1 << n; @@ -160,21 +160,23 @@ int main(int argc, char ** argv) xi = calloc(np, sizeof(double)); pxr = xr; pxi = xi; - *pxr = (enp - 1.0) * 0.5; - *pxi = 0.0; - n2 = np / 2; - *(pxr+n2) = -0.5; - *(pxi+n2) = 0.0; - for (i = 1; i <= npm; i++) { - j = np - i; - *(pxr+i) = -0.5; - *(pxr+j) = -0.5; - z = t * (double)i; - y = -0.5*(cos(z)/sin(z)); - *(pxi+i) = y; - *(pxi+j) = -y; + for (nruns = 0; nruns < NRUNS; nruns++) { + *pxr = (enp - 1.0) * 0.5; + *pxi = 0.0; + n2 = np / 2; + *(pxr+n2) = -0.5; + *(pxi+n2) = 0.0; + for (i = 1; i <= npm; i++) { + j = np - i; + *(pxr+i) = -0.5; + *(pxr+j) = -0.5; + z = t * (double)i; + y = -0.5*(cos(z)/sin(z)); + *(pxi+i) = y; + *(pxi+j) = -y; + } + dfft(xr,xi,np); } - dfft(xr,xi,np); zr = 0.0; zi = 0.0; npm = np-1; diff --git a/test/c/fftsp.c b/test/c/fftsp.c index 3c7c23c3..f83bd41f 100644 --- a/test/c/fftsp.c +++ b/test/c/fftsp.c @@ -145,13 +145,13 @@ int dfft(float x[], float y[], int np) /* Test harness */ -float * xr, * xi; +#define NRUNS 3000 int main(int argc, char ** argv) { - int n, np, npm, n2, i, j; + int n, np, npm, n2, i, j, nruns; float enp, t, y, z, zr, zi, zm, a; - float * pxr, * pxi; + float * xr, * xi, * pxr, * pxi; if (argc >= 2) n = atoi(argv[1]); else n = 12; np = 1 << n; @@ -162,21 +162,23 @@ int main(int argc, char ** argv) xi = calloc(np, sizeof(float)); pxr = xr; pxi = xi; - *pxr = (enp - 1.0) * 0.5f; - *pxi = 0.0; - n2 = np / 2; - *(pxr+n2) = -0.5; - *(pxi+n2) = 0.0; - for (i = 1; i <= npm; i++) { - j = np - i; - *(pxr+i) = -0.5; - *(pxr+j) = -0.5; - z = t * (float)i; - y = -0.5f*(cosf(z)/sinf(z)); - *(pxi+i) = y; - *(pxi+j) = -y; + for (nruns = 0; nruns < NRUNS; nruns++) { + *pxr = (enp - 1.0) * 0.5f; + *pxi = 0.0; + n2 = np / 2; + *(pxr+n2) = -0.5; + *(pxi+n2) = 0.0; + for (i = 1; i <= npm; i++) { + j = np - i; + *(pxr+i) = -0.5; + *(pxr+j) = -0.5; + z = t * (float)i; + y = -0.5f*(cosf(z)/sinf(z)); + *(pxi+i) = y; + *(pxi+j) = -y; + } + dfft(xr,xi,np); } - dfft(xr,xi,np); zr = 0.0; zi = 0.0; npm = np-1; diff --git a/test/c/fftw.c b/test/c/fftw.c index 0b414956..40648257 100644 --- a/test/c/fftw.c +++ b/test/c/fftw.c @@ -74,14 +74,16 @@ const E KP1_847759065 = ((E) +1.847759065022573512256366378793576573644833252); /* Test harness */ +#define NRUNS (1024 * 1024) + int main() { - INT s[8] = { 0,1,2,3,4,5,6,7 }; + static INT s[8] = { 0,1,2,3,4,5,6,7 }; static R i[1024]; static R o[1024]; int k; for (k = 0; k < 1024; ++k) i[k] = k; - for (k = 0; k < 1024 * 1024 * 2; ++k) + for (k = 0; k < NRUNS; ++k) e01_8(i, o, s, s, 64, 8, 8); for (k = 0; k < 16; ++k) printf("o[%d] = %.6e\n", k, o[k]); diff --git a/test/c/fib.c b/test/c/fib.c index a9052029..23460a1d 100644 --- a/test/c/fib.c +++ b/test/c/fib.c @@ -12,7 +12,7 @@ int fib(int n) int main(int argc, char ** argv) { int n, r; - if (argc >= 2) n = atoi(argv[1]); else n = 36; + if (argc >= 2) n = atoi(argv[1]); else n = 40; r = fib(n); printf("fib(%d) = %d\n", n, r); return 0; diff --git a/test/c/knucleotide.c b/test/c/knucleotide.c index 6bd0e9e7..ef909e0e 100644 --- a/test/c/knucleotide.c +++ b/test/c/knucleotide.c @@ -41,15 +41,15 @@ struct ht_ht { #endif /* HT_DEBUG */ }; -/*inline*/ int ht_val(struct ht_node *node) { +static inline int ht_val(struct ht_node *node) { return(node->val); } -/*inline*/ char *ht_key(struct ht_node *node) { +static inline char *ht_key(struct ht_node *node) { return(node->key); } -/*inline*/ int ht_hashcode(struct ht_ht *ht, char *key) { +static inline int ht_hashcode(struct ht_ht *ht, char *key) { unsigned long val = 0; for (; *key; ++key) val = 5 * val + *key; return(val % ht->size); @@ -129,7 +129,7 @@ void ht_destroy(struct ht_ht *ht) { #endif /* HT_DEBUG */ } -/*inline*/ struct ht_node *ht_find(struct ht_ht *ht, char *key) { +struct ht_node *ht_find(struct ht_ht *ht, char *key) { int hash_code = ht_hashcode(ht, key); struct ht_node *node = ht->tbl[hash_code]; while (node) { @@ -139,7 +139,7 @@ void ht_destroy(struct ht_ht *ht) { return((struct ht_node *)NULL); } -/*inline*/ struct ht_node *ht_find_new(struct ht_ht *ht, char *key) { +struct ht_node *ht_find_new(struct ht_ht *ht, char *key) { int hash_code = ht_hashcode(ht, key); struct ht_node *prev = 0, *node = ht->tbl[hash_code]; while (node) { @@ -161,7 +161,7 @@ void ht_destroy(struct ht_ht *ht) { /* * Hash Table iterator data/functions */ -/*inline*/ struct ht_node *ht_next(struct ht_ht *ht) { +struct ht_node *ht_next(struct ht_ht *ht) { unsigned long index; struct ht_node *node = ht->iter_next; if (node) { @@ -179,13 +179,13 @@ void ht_destroy(struct ht_ht *ht) { return((struct ht_node *)NULL); } -/*inline*/ struct ht_node *ht_first(struct ht_ht *ht) { +struct ht_node *ht_first(struct ht_ht *ht) { ht->iter_index = 0; ht->iter_next = (struct ht_node *)NULL; return(ht_next(ht)); } -/*inline*/ int ht_count(struct ht_ht *ht) { +static inline int ht_count(struct ht_ht *ht) { return(ht->items); } @@ -281,6 +281,8 @@ write_count (char *searchFor, char *buffer, long buflen) ht_destroy (ht); } +#define NRUNS 500 + int main () { @@ -347,6 +349,10 @@ main () write_count ("GGTATT", buffer, seqlen); write_count ("GGTATTTTAATT", buffer, seqlen); write_count ("GGTATTTTAATTTATAGT", buffer, seqlen); + for (i = 0; i < NRUNS; i++) { + struct ht_ht * ht = generate_frequencies (6, buffer, seqlen); + ht_destroy(ht); + } free (buffer); fclose (f); return 0; diff --git a/test/c/lists.c b/test/c/lists.c index 350d1f0a..fc974539 100644 --- a/test/c/lists.c +++ b/test/c/lists.c @@ -59,7 +59,7 @@ int main(int argc, char ** argv) struct list * l; if (argc >= 2) n = atoi(argv[1]); else n = 1000; - if (argc >= 3) niter = atoi(argv[1]); else niter = 100000; + if (argc >= 3) niter = atoi(argv[1]); else niter = 200000; l = buildlist(n); if (checklist(n, reverselist(l))) { printf("OK\n"); diff --git a/test/c/nsieve.c b/test/c/nsieve.c index d0d59b2b..79e95024 100644 --- a/test/c/nsieve.c +++ b/test/c/nsieve.c @@ -10,7 +10,7 @@ typedef unsigned char boolean; -static void nsieve(int m) { +static unsigned int nsieve(int m) { unsigned int count = 0, i, j; boolean * flags = (boolean *) malloc(m * sizeof(boolean)); memset(flags, 1, m); @@ -23,14 +23,20 @@ static void nsieve(int m) { } free(flags); - printf("Primes up to %8u %8u\n", m, count); + return count; } +#define NITER 10 + int main(int argc, char * argv[]) { int m = argc < 2 ? 9 : atoi(argv[1]); - int i; - for (i = 0; i < 3; i++) - nsieve(10000 << (m-i)); + int i, j; + for (i = 0; i < 3; i++) { + int n = 10000 << (m-i); + unsigned count; + for (j = 0; j < NITER; j++) { count = nsieve(n); } + printf("Primes up to %8d %8u\n", n, count); + } return 0; } diff --git a/test/c/nsievebits.c b/test/c/nsievebits.c index 9ce6aaa0..ed9cde52 100644 --- a/test/c/nsievebits.c +++ b/test/c/nsievebits.c @@ -30,13 +30,16 @@ nsieve(unsigned int m) return (count); } +#define NITER 10 + static void test(unsigned int n) { unsigned int count, m; + int i; m = (1 << n) * 10000; - count = nsieve(m); + for (i = 0; i < NITER; i++) { count = nsieve(m); } printf("Primes up to %8u %8u\n", m, count); } diff --git a/test/c/qsort.c b/test/c/qsort.c index 802ef9ce..50b60be6 100644 --- a/test/c/qsort.c +++ b/test/c/qsort.c @@ -27,24 +27,24 @@ int cmpint(const void * i, const void * j) return 1; } +#define NITER 100 + int main(int argc, char ** argv) { - int n, i; + int n, i, j; int * a, * b; - int bench = 0; - if (argc >= 2) n = atoi(argv[1]); else n = 1000000; - if (argc >= 3) bench = 1; + if (argc >= 2) n = atoi(argv[1]); else n = 100000; a = malloc(n * sizeof(int)); b = malloc(n * sizeof(int)); - for (i = 0; i < n; i++) b[i] = a[i] = rand() & 0xFFFF; - quicksort(0, n - 1, a); - if (!bench) { - qsort(b, n, sizeof(int), cmpint); - for (i = 0; i < n; i++) { - if (a[i] != b[i]) { printf("Bug!\n"); return 2; } - } - printf("OK\n"); + for (j = 0; j < NITER; j++) { + for (i = 0; i < n; i++) b[i] = a[i] = rand() & 0xFFFF; + quicksort(0, n - 1, a); + } + qsort(b, n, sizeof(int), cmpint); + for (i = 0; i < n; i++) { + if (a[i] != b[i]) { printf("Bug!\n"); return 2; } } + printf("OK\n"); return 0; } diff --git a/test/c/sha1.c b/test/c/sha1.c index 84d0072c..dff32a8e 100644 --- a/test/c/sha1.c +++ b/test/c/sha1.c @@ -231,6 +231,6 @@ int main(int argc, char ** argv) } do_test(test_input_1, test_output_1); do_test(test_input_2, test_output_2); - do_bench(1000000); + do_bench(2000000); return 0; } diff --git a/test/c/sha3.c b/test/c/sha3.c index 29b8769e..93b8ba4a 100644 --- a/test/c/sha3.c +++ b/test/c/sha3.c @@ -191,7 +191,7 @@ test_triplet_t testvec[4] = { }; #define DATALEN 100000 -#define NITER 1000 +#define NITER 250 int main() { diff --git a/test/c/siphash24.c b/test/c/siphash24.c index 0ed1841f..3af4aa04 100644 --- a/test/c/siphash24.c +++ b/test/c/siphash24.c @@ -242,6 +242,7 @@ int speed_test(void) for(i = 0; i < 16; ++i ) k[i] = i; for(i = 0; i < 10000000; i++) { + testdata[99] = (u8) i; crypto_auth(out, testdata, 100, k); } return out[0]; diff --git a/test/c/spectral.c b/test/c/spectral.c index 29499fd8..aa1bf397 100644 --- a/test/c/spectral.c +++ b/test/c/spectral.c @@ -10,7 +10,7 @@ #include <stdlib.h> #include <math.h> -inline double eval_A(int i, int j) { return 1.0/((i+j)*(i+j+1)/2+i+1); } +static inline double eval_A(int i, int j) { return 1.0/((i+j)*(i+j+1)/2+i+1); } void eval_A_times_u(int N, const double u[], double Au[]) { diff --git a/test/c/vmach.c b/test/c/vmach.c index 49c120dd..84ab1f94 100644 --- a/test/c/vmach.c +++ b/test/c/vmach.c @@ -207,8 +207,8 @@ int main(int argc, char ** argv) printf("fib(30) = %ld\n", wordcode_interp(wordcode_fib)); printf("tak(18, 12, 6) = %ld\n", wordcode_interp(wordcode_tak)); - for (i = 0; i < 20; i++) (void) wordcode_interp(wordcode_fib); - for (i = 0; i < 1000; i++) (void) wordcode_interp(wordcode_tak); + for (i = 0; i < 10; i++) (void) wordcode_interp(wordcode_fib); + for (i = 0; i < 500; i++) (void) wordcode_interp(wordcode_tak); return 0; } diff --git a/test/compression/Makefile b/test/compression/Makefile index d951c08f..784f7e73 100644 --- a/test/compression/Makefile +++ b/test/compression/Makefile @@ -4,10 +4,6 @@ CC=../../ccomp CFLAGS=-U__GNUC__ -stdlib ../../runtime -dclight -dasm LIBS= TIME=xtime -o /dev/null -mintime 1.0 -ifeq ($(CCHECKLINK),true) -CCHECK=../../cchecklink -CFLAGS+= -sdump -endif EXE=arcode lzw lzss @@ -35,7 +31,7 @@ TESTCOMPR=/tmp/testcompr.out TESTEXPND=/tmp/testexpnd.out test: - rm -f $(TESTCOMPR) $(TESTEXPND) + @rm -f $(TESTCOMPR) $(TESTEXPND) @echo "Test data: $(TESTFILE)" @for i in $(EXE); do \ echo "$$i: compression..."; \ @@ -47,23 +43,15 @@ test: else echo "$$i: FAILED"; exit 2; \ fi; \ done - rm -f $(TESTCOMPR) $(TESTEXPND) + @rm -f $(TESTCOMPR) $(TESTEXPND) bench: - rm -f $(TESTCOMPR) + @rm -f $(TESTCOMPR) @for i in $(EXE); do \ - echo -n "$$i "; \ + echo -n "$$i: "; \ $(TIME) sh -c "./$$i -c -i $(TESTFILE) -o $(TESTCOMPR) && ./$$i -d -i $(TESTCOMPR) -o /dev/null"; \ done - rm -f $(TESTCOMPR) - -ccheck: - @echo "---- arcode" - @$(CCHECK) -exe arcode $(ARCODE_OBJS:.o=.sdump) - @echo "---- lzw" - @$(CCHECK) -exe lzw $(LZW_OBJS:.o=.sdump) - @echo "---- lzss" - @$(CCHECK) -exe lzss $(LZSS_OBJS:.o=.sdump) + @rm -f $(TESTCOMPR) include .depend diff --git a/test/compression/arcode.c b/test/compression/arcode.c index f915cc25..9a9847f8 100644 --- a/test/compression/arcode.c +++ b/test/compression/arcode.c @@ -702,7 +702,7 @@ int ReadHeader(bit_file_t *bfpIn) cumulativeProb = 0; - for (c = 0; c <= UPPER(EOF_CHAR); c++) + for (c = 0; c < UPPER(EOF_CHAR); c++) { ranges[UPPER(c)] = 0; } diff --git a/test/raytracer/Makefile b/test/raytracer/Makefile index 1d4882bc..dc007fd7 100644 --- a/test/raytracer/Makefile +++ b/test/raytracer/Makefile @@ -3,11 +3,7 @@ include ../../Makefile.config CC=../../ccomp CFLAGS=-stdlib ../../runtime -dparse -dclight -dasm -fstruct-return LIBS=$(LIBMATH) -TIME=xtime -mintime 2.0 -ifeq ($(CCHECKLINK),true) -CCHECK=../../cchecklink -CFLAGS+= -sdump -endif +TIME=xtime OBJS=memory.o gmllexer.o gmlparser.o eval.o \ arrays.o vector.o matrix.o object.o intersect.o surface.o light.o \ @@ -26,30 +22,6 @@ include .depend depend: gcc -MM *.c > .depend -gcc0: - $(MAKE) clean - $(MAKE) CC=gcc CFLAGS="-O0 -Wall" - mv render render.gcc0 - $(MAKE) clean - -gcc1: - $(MAKE) clean - $(MAKE) CC=gcc CFLAGS="-O1 -Wall" - mv render render.gcc1 - $(MAKE) clean - -gcc2: - $(MAKE) clean - $(MAKE) CC=gcc CFLAGS="-O2 -Wall" - mv render render.gcc2 - $(MAKE) clean - -gcc3: - $(MAKE) clean - $(MAKE) CC=gcc CFLAGS="-O3 -Wall" - mv render render.gcc3 - $(MAKE) clean - test: ./render < kal.gml @if cmp kal.ppm Results/kal.ppm; \ @@ -58,9 +30,4 @@ test: fi bench: - @echo -n "raytracer: "; $(TIME) ./render < kal.gml - -ccheck: - @echo "---- render" - @$(CCHECK) -exe render *.sdump - + @echo -n "raytracer: "; $(TIME) sh -c './render < kal.gml' diff --git a/test/raytracer/gmllexer.c b/test/raytracer/gmllexer.c index a8594dd3..befad28d 100644 --- a/test/raytracer/gmllexer.c +++ b/test/raytracer/gmllexer.c @@ -147,6 +147,14 @@ static void get_number(int firstchar) exit(2); } +static char * my_strdup(char * s) +{ + size_t l = strlen(s); + char * t = malloc(l + 1); + if (t != NULL) memcpy(t, s, l + 1); + return t; +} + static void get_string() { int c, pos; @@ -159,7 +167,7 @@ static void get_string() } buffer[pos] = 0; current_lexeme.kind = STRING; - current_lexeme.u.s = strdup(buffer); + current_lexeme.u.s = my_strdup(buffer); return; bad_string: fprintf(stderr, "Illegal string literal\n"); diff --git a/test/regression/Makefile b/test/regression/Makefile index 335a136b..88f50466 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -2,10 +2,6 @@ include ../../Makefile.config CCOMP=../../ccomp CCOMPFLAGS=-stdlib ../../runtime -dparse -dc -dclight -dasm -fall -ifeq ($(CCHECKLINK),true) -CCHECK=../../cchecklink -CCOMPFLAGS+= -sdump -endif LIBS=$(LIBMATH) @@ -104,9 +100,3 @@ test: bench: -ccheck: - @for i in $(TESTS) $(TESTS_COMP); do \ - echo "---- $$i"; \ - $(CCHECK) -exe $$i.compcert $$i.sdump; \ - done - diff --git a/test/spass/Makefile b/test/spass/Makefile index 6a4cd598..f6acc551 100644 --- a/test/spass/Makefile +++ b/test/spass/Makefile @@ -2,10 +2,6 @@ include ../../Makefile.config CC=../../ccomp CFLAGS=-stdlib ../../runtime -dparse -dclight -dasm -fstruct-return -ifeq ($(CCHECKLINK),true) -CCHECK=../../cchecklink -CFLAGS+= -sdump -endif SRCS=analyze.c clause.c clock.c closure.c cnf.c component.c \ condensing.c context.c defs.c dfgparser.c dfgscanner.c doc-proof.c \ @@ -34,10 +30,6 @@ TIME=xtime -o /dev/null # Xavier's hack bench: @echo -n "spass: "; $(TIME) ./spass problem.dfg -ccheck: - @echo "---- spass" - @$(CCHECK) -exe spass *.sdump - depend: gcc -MM $(SRCS) > .depend |