diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-03 11:08:25 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-03 11:08:25 +0200 |
commit | 38959ad2b2d35a7d1b3479ef4298a5d754350cd8 (patch) | |
tree | bfbdcf57b3035b1de721b6a900c70f1ddf94e3b7 /powerpc/Asmexpand.ml | |
parent | cfee340dc514e2cfbc5df910f7aa687e78a54d41 (diff) | |
download | compcert-38959ad2b2d35a7d1b3479ef4298a5d754350cd8.tar.gz compcert-38959ad2b2d35a7d1b3479ef4298a5d754350cd8.zip |
New builtin for dcbz instruction.
This commit adds a builtin for the dcbz instructions. Additionally
the dcbt,dcbtst,dcbtls and icbtls instruction are changed to their
actually form all taking one additional register in Asm.v.
Diffstat (limited to 'powerpc/Asmexpand.ml')
-rw-r--r-- | powerpc/Asmexpand.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 43d8fc6e..f266f3ec 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -354,9 +354,9 @@ let expand_builtin_prefetch addr rw loc = raise (Error "the last argument of __builtin_prefetch must be a constant between 0 and 2"); let emit_prefetch_instr addr = if Int.eq rw _0 then begin - emit (Pdcbt (loc,addr)); + emit (Pdcbt (loc,GPR0,addr)); end else if Int.eq rw _1 then begin - emit (Pdcbtst (loc,addr)); + emit (Pdcbtst (loc,GPR0,addr)); end else raise (Error "the second argument of __builtin_prefetch must be either 0 or 1") in @@ -365,13 +365,13 @@ let expand_builtin_prefetch addr rw loc = let expand_builtin_dcbtls addr loc = if not ((loc == _0) || (loc = _2)) then raise (Error "the second argument of __builtin_dcbtls must be a constant between 0 and 2"); - let emit_inst addr = emit (Pdcbtls (loc,addr)) in + let emit_inst addr = emit (Pdcbtls (loc,GPR0,addr)) in expand_builtin_cache_common addr emit_inst let expand_builtin_icbtls addr loc = if not ((loc == _0) || (loc = _2)) then raise (Error "the second argument of __builtin_icbtls must be a constant between 0 and 2"); - let emit_inst addr = emit (Picbtls (loc,addr)) in + let emit_inst addr = emit (Picbtls (loc,GPR0,addr)) in expand_builtin_cache_common addr emit_inst (* Handling of compiler-inlined builtins *) @@ -490,6 +490,8 @@ let expand_builtin_inline name args res = expand_builtin_prefetch a1 rw loc | "__builtin_prefetch" ,_,_ -> raise (Error "the second and third argument of __builtin_prefetch must be a constant") + | "__builtin_dcbz",[BA (IR a1)],_ -> + emit (Pdcbz (GPR0,a1)) (* Special registers *) | "__builtin_get_spr", [BA_int n], BR(IR res) -> emit (Pmfspr(res, n)) |