From 50ee6bdf639ffba989968abb9c24a57126ab35a4 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 18 Aug 2011 14:50:19 +0000 Subject: Presimplification SimplVolatile: cleaned up and integrated. test/*/Makefile: normalized 'bench' target git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1717 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 8 ++++ cfrontend/C2C.ml | 2 +- cfrontend/Cparser.mlpack | 1 + cparser/SimplVolatile.ml | 30 +++++++++------ driver/Clflags.ml | 1 + driver/Driver.ml | 17 ++++++++- test/Makefile | 3 ++ test/c/Makefile | 4 +- test/compression/Makefile | 2 +- test/raytracer/Makefile | 2 +- test/regression/Makefile | 6 +-- test/regression/Results/volatile3 | 38 +++++++++++++++++++ test/regression/volatile3.c | 77 +++++++++++++++++++++++++++++++++++++++ test/spass/Makefile | 2 +- 14 files changed, 171 insertions(+), 22 deletions(-) create mode 100644 test/regression/Results/volatile3 create mode 100644 test/regression/volatile3.c diff --git a/Changelog b/Changelog index e49f310c..cebff9ab 100644 --- a/Changelog +++ b/Changelog @@ -24,6 +24,14 @@ Release 1.9, 2011-xx-xx . Conditional expressions "e1 ? e2 : e3" where e2 and e3 have different types were missing a cast to their common type. +- Support for "read-modify-write" operations over volatiles + (such as e++ or --e or e |= 1 where e has volatile type) + through a new presimplification (flag -fvolatile-rmw, "on" by default). + +- New optimization pass: Redundant Reload Elimination, which fixes up + inefficiencies introduced during the Reload pass. On x86, it increases + performance by up to 10%. On PowerPC and ARM, the effect is negligible. + - Revised handling of annotation statements. Now they come in two forms: 1. __builtin_annot("format", x1, ..., xN) (arbitrarily many arguments; no code generated, even if some diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bdddd14a..9340cc50 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -491,7 +491,7 @@ let rec convertExpr env e = if is_volatile_access env e1 then Ecall(volatile_write_fun (typeof e1'), Econs(Eaddrof(e1', Tpointer(typeof e1')), Econs(e2', Enil)), - Tvoid) (* typing issue here *) + Tvoid) (* SimplVolatile guarantees that ret. value is unused *) else Eassign(e1', e2', ty) | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| diff --git a/cfrontend/Cparser.mlpack b/cfrontend/Cparser.mlpack index 291b551a..e6bbdc61 100644 --- a/cfrontend/Cparser.mlpack +++ b/cfrontend/Cparser.mlpack @@ -22,5 +22,6 @@ cparser/StructByValue cparser/StructAssign cparser/Bitfields cparser/PackedStructs +cparser/SimplVolatile cparser/Parse diff --git a/cparser/SimplVolatile.ml b/cparser/SimplVolatile.ml index c6ebd347..b155a3c4 100644 --- a/cparser/SimplVolatile.ml +++ b/cparser/SimplVolatile.ml @@ -23,19 +23,25 @@ open Transform (* Expansion of read-write-modify constructs. *) +(* Temporaries must not be [const] because we assign into them, + and should not be [volatile] because they are private. *) + +let mk_temp env ty = + new_temp (erase_attributes_type env ty) + (** [l = r]. *) -let mk_assign ctx l r = +let mk_assign env ctx l r = match ctx with | Effects -> eassign l r | Val -> - let tmp = new_temp l.etyp in + let tmp = mk_temp env l.etyp in ecomma (eassign tmp r) (ecomma (eassign l tmp) tmp) (** [l op= r]. Warning: [l] is evaluated twice. *) -let mk_assignop ctx op l r ty = +let mk_assignop env ctx op l r ty = let op' = match op with | Oadd_assign -> Oadd | Osub_assign -> Osub @@ -48,22 +54,22 @@ let mk_assignop ctx op l r ty = | Effects -> eassign l res | Val -> - let tmp = new_temp l.etyp in + let tmp = mk_temp env l.etyp in ecomma (eassign tmp res) (ecomma (eassign l tmp) tmp) (** [++l] or [--l]. Warning: [l] is evaluated twice. *) -let mk_preincrdecr ctx op l ty = +let mk_preincrdecr env ctx op l ty = let op' = match op with | Opreincr -> Oadd_assign | Opredecr -> Osub_assign | _ -> assert false in - mk_assignop ctx op' l (intconst 1L IInt) ty + mk_assignop env ctx op' l (intconst 1L IInt) ty (** [l++] or [l--]. Warning: [l] is evaluated twice. *) -let mk_postincrdecr ctx op l ty = +let mk_postincrdecr env ctx op l ty = let op' = match op with | Opostincr -> Oadd @@ -74,7 +80,7 @@ let mk_postincrdecr ctx op l ty = let newval = {edesc = EBinop(op', l, intconst 1L IInt, ty); etyp = ty} in eassign l newval | Val -> - let tmp = new_temp l.etyp in + let tmp = mk_temp env l.etyp in let newval = {edesc = EBinop(op', tmp, intconst 1L IInt, ty); etyp = ty} in ecomma (eassign tmp l) (ecomma (eassign l newval) tmp) @@ -92,21 +98,21 @@ let transf_expr loc env ctx e = | EVar _ -> e | EUnop((Opreincr|Opredecr as op), e1) when is_volatile e1.etyp -> bind_lvalue env (texp Val e1) - (fun l -> mk_preincrdecr ctx op l (unary_conversion env l.etyp)) + (fun l -> mk_preincrdecr env ctx op l (unary_conversion env l.etyp)) | EUnop((Opostincr|Opostdecr as op), e1) when is_volatile e1.etyp -> bind_lvalue env (texp Val e1) - (fun l -> mk_postincrdecr ctx op l (unary_conversion env l.etyp)) + (fun l -> mk_postincrdecr env ctx op l (unary_conversion env l.etyp)) | EUnop(op, e1) -> {edesc = EUnop(op, texp Val e1); etyp = e.etyp} | EBinop(Oassign, e1, e2, ty) when is_volatile e1.etyp -> - mk_assign ctx (texp Val e1) (texp Val e2) + mk_assign env ctx (texp Val e1) (texp Val e2) | EBinop((Oadd_assign | Osub_assign | Omul_assign | Odiv_assign | Omod_assign | Oand_assign | Oor_assign | Oxor_assign | Oshl_assign | Oshr_assign) as op, e1, e2, ty) when is_volatile e1.etyp -> bind_lvalue env (texp Val e1) - (fun l -> mk_assignop ctx op l (texp Val e2) ty) + (fun l -> mk_assignop env ctx op l (texp Val e2) ty) | EBinop(Ocomma, e1, e2, ty) -> {edesc = EBinop(Ocomma, texp Effects e1, texp ctx e2, ty); etyp = e.etyp} diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 87de59f9..fe14ba7c 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -21,6 +21,7 @@ let option_fstruct_assign = ref false let option_fbitfields = ref false let option_fvararg_calls = ref true let option_fpacked_structs = ref false +let option_fvolatile_rmw = ref true let option_fmadd = ref false let option_fsse = ref true let option_dparse = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index d5a659d7..1139e7a4 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -73,6 +73,7 @@ let parse_c_file sourcename ifile = ^ (if !option_fstruct_assign then "S" else "") ^ (if !option_fbitfields then "f" else "") ^ (if !option_fpacked_structs then "p" else "") + ^ (if !option_fvolatile_rmw then "v" else "") in (* Parsing and production of a simplified C AST *) let ast = @@ -340,7 +341,10 @@ Language support options (use -fno- to turn off -f) : -fstruct-passing Emulate passing structs and unions by value [off] -fstruct-assign Emulate assignment between structs or unions [off] -fvararg-calls Emulate calls to variable-argument functions [on] + -fvolatile-rmw Emulate ++, -- and op= on volatile l-values [on] -fpacked-structs Emulate packed structs [off] + -fall Activate all language support options above + -fnone Turn off all language support options above Code generation options: (use -fno- to turn off -f) : -fmadd (PowerPC) Use fused multiply-add and multiply-sub instructions [off] -fsse (IA32) Use SSE2 instructions for some integer operations [on] @@ -374,6 +378,12 @@ Interpreter mode: -all Simulate all possible execution orders " +let language_support_options = [ + option_fbitfields; option_flonglong; option_fstruct_passing; + option_fstruct_assign; option_fvararg_calls; option_fpacked_structs; + option_fvolatile_rmw +] + let cmdline_actions = let f_opt name ref = ["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in @@ -421,7 +431,11 @@ let cmdline_actions = ".*\\.[oa]$", Self (fun s -> linker_options := s :: !linker_options); "-fsmall-data$", Integer(fun n -> option_small_data := n); - "-fsmall-const$", Integer(fun n -> option_small_const := n) + "-fsmall-const$", Integer(fun n -> option_small_const := n); + "-fall$", Self (fun _ -> + List.iter (fun r -> r := true) language_support_options); + "-fnone$", Self (fun _ -> + List.iter (fun r -> r := false) language_support_options); ] @ f_opt "longlong" option_flonglong @ f_opt "struct-passing" option_fstruct_passing @@ -431,6 +445,7 @@ let cmdline_actions = @ f_opt "madd" option_fmadd @ f_opt "packed-structs" option_fpacked_structs @ f_opt "sse" option_fsse + @ f_opt "volatile-rmw" option_fvolatile_rmw let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 }; diff --git a/test/Makefile b/test/Makefile index d29cd8d0..5771523e 100644 --- a/test/Makefile +++ b/test/Makefile @@ -6,5 +6,8 @@ all: test: for i in $(DIRS); do $(MAKE) -C $$i test; done +bench: + for i in $(DIRS); do $(MAKE) -C $$i bench; done + clean: for i in $(DIRS); do $(MAKE) -C $$i clean; done diff --git a/test/c/Makefile b/test/c/Makefile index ed70d18e..9c57a3f1 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -46,12 +46,12 @@ test_gcc: fi; \ done -time_gcc: +bench_gcc: @for i in $(PROGS); do \ echo -n "$$i: "; $(TIME) ./$$i.gcc; \ done -time: +bench: @for i in $(PROGS); do \ echo -n "$$i: "; $(TIME) ./$$i.compcert; \ done diff --git a/test/compression/Makefile b/test/compression/Makefile index e211a58d..8db55dd9 100644 --- a/test/compression/Makefile +++ b/test/compression/Makefile @@ -24,7 +24,7 @@ LZSS_OBJS=$(COMMON_OBJS) lzvars.o lzhash.o lzencode.o lzdecode.o lzssmain.o lzss: $(LZSS_OBJS) $(CC) $(CFLAGS) -o $@ $(LZSS_OBJS) $(LIBS) -TESTFILE:=$(firstword $(wildcard /mach_kernel) $(wildcard /boot/vmlinuz) ./lzss) +TESTFILE:=$(firstword $(wildcard /usr/share/dict/words) ./lzss) TESTCOMPR=/tmp/testcompr.out TESTEXPND=/tmp/testexpnd.out diff --git a/test/raytracer/Makefile b/test/raytracer/Makefile index f209bb48..db359b13 100644 --- a/test/raytracer/Makefile +++ b/test/raytracer/Makefile @@ -54,4 +54,4 @@ test: fi bench: - $(TIME) ./render < kal.gml + @echo -n "raytracer: "; $(TIME) ./render < kal.gml diff --git a/test/regression/Makefile b/test/regression/Makefile index eb50defc..aeba3bd3 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -1,8 +1,7 @@ include ../../Makefile.config CCOMP=../../ccomp -CCOMPFLAGS=-stdlib ../../runtime -dparse -dc -dclight -dasm \ - -fstruct-passing -fstruct-assign -fbitfields -fpacked-structs +CCOMPFLAGS=-stdlib ../../runtime -dparse -dc -dclight -dasm -fall LIBS=$(LIBMATH) @@ -10,7 +9,7 @@ LIBS=$(LIBMATH) TESTS=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \ bitfields5 bitfields6 bitfields7 \ - expr1 expr6 initializers volatile2 \ + expr1 expr6 initializers volatile2 volatile3 \ funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \ sizeof1 sizeof2 packedstruct1 @@ -44,3 +43,4 @@ test: fi; \ done +bench: diff --git a/test/regression/Results/volatile3 b/test/regression/Results/volatile3 new file mode 100644 index 00000000..3d1f786b --- /dev/null +++ b/test/regression/Results/volatile3 @@ -0,0 +1,38 @@ +x = 0 +x = 1 +x++ = 1 +x = 2 +x = 44 +x += 12 = 56 +x = 56 +x = 55 +x-- = 55 +x = 54 +x = 47 +x -= 3 = 44 +x = 44 +x = 45 +++x = 46 +x = 46 +x = 45 +--x = 44 +x = 44 +c = 0 +c = 1 +c++ = 1 +c = 2 +c = 252 +c += 42 = 38 +c = 38 +c = 37 +c-- = 37 +c = 36 +c = 29 +c -= 3 = 26 +c = 26 +c = 27 +++c = 28 +c = 28 +c = 27 +--c = 26 +c = 26 diff --git a/test/regression/volatile3.c b/test/regression/volatile3.c new file mode 100644 index 00000000..2999609a --- /dev/null +++ b/test/regression/volatile3.c @@ -0,0 +1,77 @@ +/* Expansion of read-modify-write operations on volatiles */ + +#include + +volatile int x; +volatile unsigned char c; + +int main() +{ + x = 0; + printf("x = %d\n", x); + + x++; + printf("x = %d\n", x); + printf ("x++ = %d\n", x++); + printf("x = %d\n", x); + + x += 42; + printf("x = %d\n", x); + printf ("x += 12 = %d\n", x += 12); + printf("x = %d\n", x); + + x--; + printf("x = %d\n", x); + printf ("x-- = %d\n", x--); + printf("x = %d\n", x); + + x -= 7; + printf("x = %d\n", x); + printf ("x -= 3 = %d\n", x -= 3); + printf("x = %d\n", x); + + ++x; + printf("x = %d\n", x); + printf ("++x = %d\n", ++x); + printf("x = %d\n", x); + + --x; + printf("x = %d\n", x); + printf ("--x = %d\n", --x); + printf("x = %d\n", x); + + c = 0; + printf("c = %d\n", c); + + c++; + printf("c = %d\n", c); + printf ("c++ = %d\n", c++); + printf("c = %d\n", c); + + c += 250; + printf("c = %d\n", c); + printf ("c += 42 = %d\n", c += 42); + printf("c = %d\n", c); + + c--; + printf("c = %d\n", c); + printf ("c-- = %d\n", c--); + printf("c = %d\n", c); + + c -= 7; + printf("c = %d\n", c); + printf ("c -= 3 = %d\n", c -= 3); + printf("c = %d\n", c); + + ++c; + printf("c = %d\n", c); + printf ("++c = %d\n", ++c); + printf("c = %d\n", c); + + --c; + printf("c = %d\n", c); + printf ("--c = %d\n", --c); + printf("c = %d\n", c); + + return 0; +} diff --git a/test/spass/Makefile b/test/spass/Makefile index 30832f82..536488bd 100644 --- a/test/spass/Makefile +++ b/test/spass/Makefile @@ -28,7 +28,7 @@ TIME=xtime -o /dev/null # Xavier's hack #TIME=time >/dev/null # Otherwise bench: - $(TIME) ./spass problem.dfg + @echo -n "spass: "; $(TIME) ./spass problem.dfg depend: gcc -MM $(SRCS) > .depend -- cgit