aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Changelog8
-rw-r--r--cfrontend/C2C.ml2
-rw-r--r--cfrontend/Cparser.mlpack1
-rw-r--r--cparser/SimplVolatile.ml30
-rw-r--r--driver/Clflags.ml1
-rw-r--r--driver/Driver.ml17
-rw-r--r--test/Makefile3
-rw-r--r--test/c/Makefile4
-rw-r--r--test/compression/Makefile2
-rw-r--r--test/raytracer/Makefile2
-rw-r--r--test/regression/Makefile6
-rw-r--r--test/regression/Results/volatile338
-rw-r--r--test/regression/volatile3.c77
-rw-r--r--test/spass/Makefile2
14 files changed, 171 insertions, 22 deletions
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-<opt> to turn off -f<opt>) :
-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-<opt> to turn off -f<opt>) :
-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 <stdio.h>
+
+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
generated by cgit (git 2.34.1) at 2024-06-02 19:42:33 +0000