summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/ConstpropOp.vp4
-rw-r--r--arm/ConstpropOpproof.v13
-rw-r--r--arm/PrintAsm.ml98
-rw-r--r--ia32/PrintAsm.ml4
-rw-r--r--powerpc/ConstpropOp.vp11
-rw-r--r--powerpc/ConstpropOpproof.v18
-rw-r--r--powerpc/PrintAsm.ml6
-rw-r--r--test/regression/Results/volatile214
-rw-r--r--test/regression/volatile2.c15
9 files changed, 93 insertions, 90 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index a9cbad5..7e3217e 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -335,8 +335,4 @@ Nondetfunction addr_strength_reduction
(addr, args)
end.
-Definition builtin_strength_reduction
- (ef: external_function) (args: list reg) (vl: list approx) :=
- (ef, args).
-
End STRENGTH_REDUCTION.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index e7e6a41..c7de86d 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -450,19 +450,6 @@ Proof.
auto.
Qed.
-Lemma builtin_strength_reduction_correct:
- forall ef args vl m t vres m',
- vl = approx_regs app args ->
- external_call ef ge rs##args m t vres m' ->
- let (ef', args') := builtin_strength_reduction ef args vl in
- external_call ef' ge rs##args' m t vres m'.
-Proof.
- (* force MATCH to be used *)
- assert (val_match_approx (approx_reg app 1%positive) rs#(1%positive))
- by (apply MATCH).
- unfold builtin_strength_reduction; intros; simpl; auto.
-Qed.
-
End STRENGTH_REDUCTION.
End ANALYSIS.
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 186e327..278b6b1 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -226,9 +226,9 @@ let call_helper oc fn dst arg1 arg2 =
(* Handling of annotations *)
-let print_annot_stmt oc txt args =
+let print_annot_stmt oc txt targs args =
fprintf oc "%s annotation: " comment;
- PrintAnnot.print_annot_stmt preg "sp" oc txt args
+ PrintAnnot.print_annot_stmt preg "sp" oc txt targs args
let print_annot_val oc txt args res =
fprintf oc "%s annotation: " comment;
@@ -306,50 +306,66 @@ let print_builtin_memcpy oc sz al args =
(* Handling of volatile reads and writes *)
+let print_builtin_vload_common oc chunk args res =
+ match chunk, args, res with
+ | Mint8unsigned, [IR addr], IR res ->
+ fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1
+ | Mint8signed, [IR addr], IR res ->
+ fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1
+ | Mint16unsigned, [IR addr], IR res ->
+ fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1
+ | Mint16signed, [IR addr], IR res ->
+ fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1
+ | Mint32, [IR addr], IR res ->
+ fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1
+ | Mfloat32, [IR addr], FR res ->
+ fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr;
+ fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2
+ | (Mfloat64 | Mfloat64al32), [IR addr], FR res ->
+ fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1
+ | _ ->
+ assert false
+
let print_builtin_vload oc chunk args res =
fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
- let n =
- begin match chunk, args, res with
- | Mint8unsigned, [IR addr], IR res ->
- fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint8signed, [IR addr], IR res ->
- fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint16unsigned, [IR addr], IR res ->
- fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint16signed, [IR addr], IR res ->
- fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint32, [IR addr], IR res ->
- fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mfloat32, [IR addr], FR res ->
- fprintf oc " flds %a, [%a, #0]\n" freg_single res ireg addr;
- fprintf oc " fcvtds %a, %a\n" freg res freg_single res; 2
- | (Mfloat64 | Mfloat64al32), [IR addr], FR res ->
- fprintf oc " fldd %a, [%a, #0]\n" freg res ireg addr; 1
- | _ ->
- assert false
- end in
+ let n = print_builtin_vload_common oc chunk args res in
fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n
+let print_builtin_vload_global oc chunk id ofs args res =
+ fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
+ let lbl = label_symbol id ofs in
+ fprintf oc " ldr %a, .L%d @ %a\n" ireg IR14 lbl print_symb_ofs (id, ofs);
+ let n = print_builtin_vload_common oc chunk [IR IR14] res in
+ fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n + 1
+
+let print_builtin_vstore_common oc chunk args =
+ match chunk, args with
+ | (Mint8signed | Mint8unsigned), [IR addr; IR src] ->
+ fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1
+ | (Mint16signed | Mint16unsigned), [IR addr; IR src] ->
+ fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1
+ | Mint32, [IR addr; IR src] ->
+ fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1
+ | Mfloat32, [IR addr; FR src] ->
+ fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src;
+ fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2
+ | (Mfloat64 | Mfloat64al32), [IR addr; FR src] ->
+ fprintf oc " fstd %a, [%a, #0]\n" freg src ireg addr; 1
+ | _ ->
+ assert false
+
let print_builtin_vstore oc chunk args =
fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
- let n =
- begin match chunk, args with
- | (Mint8signed | Mint8unsigned), [IR addr; IR src] ->
- fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1
- | (Mint16signed | Mint16unsigned), [IR addr; IR src] ->
- fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1
- | Mint32, [IR addr; IR src] ->
- fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1
- | Mfloat32, [IR addr; FR src] ->
- fprintf oc " fcvtsd %a, %a\n" freg_single FR6 freg src;
- fprintf oc " fsts %a, [%a, #0]\n" freg_single FR6 ireg addr; 2
- | (Mfloat64 | Mfloat64al32), [IR addr; FR src] ->
- fprintf oc " fstd %a, [%a, #0]\n" freg src ireg addr; 1
- | _ ->
- assert false
- end in
+ let n = print_builtin_vstore_common oc chunk args in
fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n
+let print_builtin_vstore_global oc chunk id ofs args =
+ fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
+ let lbl = label_symbol id ofs in
+ fprintf oc " ldr %a, .L%d @ %a\n" ireg IR14 lbl print_symb_ofs (id, ofs);
+ let n = print_builtin_vstore_common oc chunk (IR IR14 :: args) in
+ fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n + 1
+
(* Magic sequence for byte-swapping *)
let print_bswap oc src tmp dst =
@@ -612,6 +628,10 @@ let print_instruction oc = function
print_builtin_vload oc chunk args res
| EF_vstore chunk ->
print_builtin_vstore oc chunk args
+ | EF_vload_global(chunk, id, ofs) ->
+ print_builtin_vload_global oc chunk id ofs args res
+ | EF_vstore_global(chunk, id, ofs) ->
+ print_builtin_vstore_global oc chunk id ofs args
| EF_memcpy(sz, al) ->
print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz))
(Int32.to_int (camlint_of_coqint al)) args
@@ -628,7 +648,7 @@ let print_instruction oc = function
| Pannot(ef, args) ->
begin match ef with
| EF_annot(txt, targs) ->
- print_annot_stmt oc (extern_atom txt) args; 0
+ print_annot_stmt oc (extern_atom txt) targs args; 0
| _ ->
assert false
end
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 4f62640..4768606 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -231,9 +231,9 @@ let need_masks = ref false
(* Handling of annotations *)
-let print_annot_stmt oc txt args =
+let print_annot_stmt oc txt targs args =
fprintf oc "%s annotation: " comment;
- PrintAnnot.print_annot_stmt preg "ESP" oc txt args
+ PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args
let print_annot_val oc txt args res =
fprintf oc "%s annotation: " comment;
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 973be92..9131a46 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -293,15 +293,4 @@ 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.
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 7d557c6..84e1e5b 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -430,24 +430,6 @@ Proof.
auto.
Qed.
-Lemma builtin_strength_reduction_correct:
- forall ef args vl m t vres m',
- vl = approx_regs app args ->
- external_call ef ge rs##args m t vres m' ->
- let (ef', args') := builtin_strength_reduction ef args vl in
- external_call ef' ge rs##args' m t vres m'.
-Proof.
- intros until m'. unfold builtin_strength_reduction.
- destruct (builtin_strength_reduction_match ef args vl); simpl; intros; InvApproxRegs; SimplVMA.
- unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H in H0.
- rewrite volatile_load_global_charact. exists b; auto.
- inv H0.
- unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H1 in H0.
- rewrite volatile_store_global_charact. exists b; auto.
- inv H0.
- auto.
-Qed.
-
End STRENGTH_REDUCTION.
End ANALYSIS.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 9c0f471..c9203ec 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -231,9 +231,9 @@ let rolm_mask n =
(* Handling of annotations *)
-let print_annot_stmt oc txt args =
+let print_annot_stmt oc txt targs args =
fprintf oc "%s annotation: " comment;
- PrintAnnot.print_annot_stmt preg "R1" oc txt args
+ PrintAnnot.print_annot_stmt preg "R1" oc txt targs args
let print_annot_val oc txt args res =
fprintf oc "%s annotation: " comment;
@@ -737,7 +737,7 @@ let print_instruction oc tbl pc fallthrough = function
| Pannot(ef, args) ->
begin match ef with
| EF_annot(txt, targs) ->
- print_annot_stmt oc (extern_atom txt) args
+ print_annot_stmt oc (extern_atom txt) targs args
| _ ->
assert false
end
diff --git a/test/regression/Results/volatile2 b/test/regression/Results/volatile2
index 5f88874..e6a9903 100644
--- a/test/regression/Results/volatile2
+++ b/test/regression/Results/volatile2
@@ -12,3 +12,17 @@ float 1: OK
float 2: OK
double 1: OK
double 2: OK
+global signed char 1: OK
+global signed char 2: OK
+global unsigned char 1: OK
+global unsigned char 2: OK
+global signed short 1: OK
+global signed short 2: OK
+global unsigned short 1: OK
+global unsigned short 2: OK
+global int 1: OK
+global int 2: OK
+global float 1: OK
+global float 2: OK
+global double 1: OK
+global double 2: OK
diff --git a/test/regression/volatile2.c b/test/regression/volatile2.c
index 0608650..306eb8c 100644
--- a/test/regression/volatile2.c
+++ b/test/regression/volatile2.c
@@ -8,6 +8,14 @@
*((ty *) &x) = v2; \
printf("%s 2: %s\n", msg, *((volatile ty *) &x) == v2 ? "OK" : "FAILED");
+signed char gsc;
+unsigned char guc;
+signed short gss;
+unsigned short gus;
+int gi;
+float gf;
+double gd;
+
int main()
{
signed char sc;
@@ -25,6 +33,13 @@ int main()
TEST("int", int, i, 0x123456, 0x7890AB);
TEST("float", float, f, 0.5, 256.0);
TEST("double", double, d, 3.1415, 2.718);
+ TEST("global signed char", signed char, gsc, 12, 34);
+ TEST("global unsigned char", unsigned char, guc, 56, 78);
+ TEST("global signed short", signed short, gss, 1234, 5678);
+ TEST("global unsigned short", unsigned short, gus, 1357, 2468);
+ TEST("global int", int, gi, 0x123456, 0x7890AB);
+ TEST("global float", float, gf, 0.5, 256.0);
+ TEST("global double", double, gd, 3.1415, 2.718);
return 0;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-22 18:04:23 +0000