diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-15 08:57:09 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-01-15 08:57:09 +0000 |
commit | c4877832826fa26aea9c236f16bdc2de16c98150 (patch) | |
tree | d25f713d4c6f4cf6126ad0451b80b32138eac84a /powerpc/ConstpropOp.vp | |
parent | a82c9c0e4a0b8e37c9c3ea5ae99714982563606f (diff) |
Added volatile_read_global and volatile_store_global builtins.
Finished updating IA32 and ARM ports.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/ConstpropOp.vp')
-rw-r--r-- | powerpc/ConstpropOp.vp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 22e89e3..cb958d4 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -274,4 +274,15 @@ Nondetfunction addr_strength_reduction (addr, args) end. +Nondetfunction builtin_strength_reduction + (ef: external_function) (args: list reg) (vl: list approx) := + match ef, args, vl with + | EF_vload chunk, r1 :: nil, G symb n1 :: nil => + (EF_vload_global chunk symb n1, nil) + | EF_vstore chunk, r1 :: r2 :: nil, G symb n1 :: v2 :: nil => + (EF_vstore_global chunk symb n1, r2 :: nil) + | _, _, _ => + (ef, args) + end. + End STRENGTH_REDUCTION. |