aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-08-22 09:46:37 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-08-22 09:46:37 +0200
commit33dfbe7601ad16fcea5377563fa7ceb4053cb85a (patch)
tree962468d4f01ae9620441a97082c826bc6fdf8c5a
parent4f187fdafdac0cf4a8b83964c89d79741dbd813e (diff)
downloadcompcert-kvx-33dfbe7601ad16fcea5377563fa7ceb4053cb85a.tar.gz
compcert-kvx-33dfbe7601ad16fcea5377563fa7ceb4053cb85a.zip
Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.
Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small.
-rw-r--r--backend/Allocation.v6
-rw-r--r--backend/CminorSel.v4
-rw-r--r--backend/Constprop.v4
-rw-r--r--backend/Deadcode.v2
-rw-r--r--backend/Inlining.v2
-rw-r--r--backend/Lineartyping.v2
-rw-r--r--backend/Locations.v2
-rw-r--r--backend/Mach.v2
-rw-r--r--backend/PrintAsmaux.ml31
-rw-r--r--backend/RTLgen.v4
-rw-r--r--backend/RTLtyping.v4
-rw-r--r--backend/Regalloc.ml32
-rw-r--r--backend/Stacking.v4
-rw-r--r--backend/ValueAnalysis.v2
-rw-r--r--backend/XTL.ml4
-rw-r--r--cfrontend/C2C.ml2
-rw-r--r--common/AST.v20
-rw-r--r--common/Events.v4
-rw-r--r--common/PrintAST.ml8
-rw-r--r--ia32/Asm.v2
-rw-r--r--ia32/Asmexpand.ml22
-rw-r--r--ia32/SelectOp.vp2
-rw-r--r--ia32/TargetPrinter.ml17
-rw-r--r--powerpc/Asm.v2
-rw-r--r--powerpc/Asmexpand.ml36
-rw-r--r--powerpc/SelectOp.vp2
-rw-r--r--powerpc/TargetPrinter.ml17
27 files changed, 114 insertions, 125 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v
index 5499c1c5..196a4075 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -697,7 +697,7 @@ Fixpoint add_equations_builtin_arg
match arg, arg' with
| BA r, BA l =>
Some (add_equation (Eq Full r l) e)
- | BA r, BA_longofwords (BA lhi) (BA llo) =>
+ | BA r, BA_splitlong (BA lhi) (BA llo) =>
assertion (typ_eq (env r) Tlong);
Some (add_equation (Eq Low r llo) (add_equation (Eq High r lhi) e))
| BA_int n, BA_int n' =>
@@ -724,7 +724,7 @@ Fixpoint add_equations_builtin_arg
assertion (ident_eq id id');
assertion (Int.eq_dec ofs ofs');
Some e
- | BA_longofwords hi lo, BA_longofwords hi' lo' =>
+ | BA_splitlong hi lo, BA_splitlong hi' lo' =>
do e1 <- add_equations_builtin_arg env hi hi' e;
add_equations_builtin_arg env lo lo' e1
| _, _ =>
@@ -763,7 +763,7 @@ Definition remove_equations_builtin_res
(env: regenv) (res: builtin_res reg) (res': builtin_res mreg) (e: eqs) : option eqs :=
match res, res' with
| BR r, BR r' => Some (remove_equation (Eq Full r (R r')) e)
- | BR r, BR_longofwords (BR rhi) (BR rlo) =>
+ | BR r, BR_splitlong (BR rhi) (BR rlo) =>
assertion (typ_eq (env r) Tlong);
if mreg_eq rhi rlo then None else
Some (remove_equation (Eq Low r (R rlo))
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index ad1cbd14..6a43eccd 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -270,9 +270,9 @@ Inductive eval_builtin_arg: builtin_arg expr -> val -> Prop :=
eval_builtin_arg (BA_loadglobal chunk id ofs) v
| eval_BA_addrglobal: forall id ofs,
eval_builtin_arg (BA_addrglobal id ofs) (Genv.symbol_address ge id ofs)
- | eval_BA_longofwords: forall a1 a2 v1 v2,
+ | eval_BA_splitlong: forall a1 a2 v1 v2,
eval_expr nil a1 v1 -> eval_expr nil a2 v2 ->
- eval_builtin_arg (BA_longofwords (BA a1) (BA a2)) (Val.longofwords v1 v2).
+ eval_builtin_arg (BA_splitlong (BA a1) (BA a2)) (Val.longofwords v1 v2).
End EVAL_EXPR.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 3a238b95..cd844d30 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -113,10 +113,10 @@ Fixpoint builtin_arg_reduction (ae: AE.t) (a: builtin_arg reg) :=
| FS n => if Compopts.generate_float_constants tt then BA_single n else a
| _ => a
end
- | BA_longofwords hi lo =>
+ | BA_splitlong hi lo =>
match builtin_arg_reduction ae hi, builtin_arg_reduction ae lo with
| BA_int nhi, BA_int nlo => BA_long (Int64.ofwords nhi nlo)
- | hi', lo' => BA_longofwords hi' lo'
+ | hi', lo' => BA_splitlong hi' lo'
end
| _ => a
end.
diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index 32bc26fb..9bf17d1d 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -78,7 +78,7 @@ Fixpoint transfer_builtin_arg (nv: nval) (na: NA.t) (a: builtin_arg reg) : NA.t
| BA_addrstack _ | BA_addrglobal _ _ => (ne, nm)
| BA_loadstack chunk ofs => (ne, nmem_add nm (Stk ofs) (size_chunk chunk))
| BA_loadglobal chunk id ofs => (ne, nmem_add nm (Gl id ofs) (size_chunk chunk))
- | BA_longofwords hi lo =>
+ | BA_splitlong hi lo =>
transfer_builtin_arg All (transfer_builtin_arg All na hi) lo
end.
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 98436bf5..08f2bfc4 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -208,7 +208,7 @@ Fixpoint sbuiltinarg (ctx: context) (a: builtin_arg reg) : builtin_arg reg :=
| BA x => BA (sreg ctx x)
| BA_loadstack chunk ofs => BA_loadstack chunk (Int.add ofs (Int.repr ctx.(dstk)))
| BA_addrstack ofs => BA_addrstack (Int.add ofs (Int.repr ctx.(dstk)))
- | BA_longofwords hi lo => BA_longofwords (sbuiltinarg ctx hi) (sbuiltinarg ctx lo)
+ | BA_splitlong hi lo => BA_splitlong (sbuiltinarg ctx hi) (sbuiltinarg ctx lo)
| _ => a
end.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 2c8de98e..62a0c585 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -59,7 +59,7 @@ Fixpoint wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool :=
match res with
| BR r => subtype ty (mreg_type r)
| BR_none => true
- | BR_longofwords hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo
+ | BR_splitlong hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo
end.
Definition wt_instr (i: instruction) : bool :=
diff --git a/backend/Locations.v b/backend/Locations.v
index 4ec24a14..439cd2dc 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -381,7 +381,7 @@ Module Locmap.
match res with
| BR r => set (R r) v m
| BR_none => m
- | BR_longofwords hi lo =>
+ | BR_splitlong hi lo =>
setres lo (Val.loword v) (setres hi (Val.hiword v) m)
end.
diff --git a/backend/Mach.v b/backend/Mach.v
index 08fe7c0a..8853d9da 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -166,7 +166,7 @@ Fixpoint set_res (res: builtin_res mreg) (v: val) (rs: regset) : regset :=
match res with
| BR r => Regmap.set r v rs
| BR_none => rs
- | BR_longofwords hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+ | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
end.
Definition is_label (lbl: label) (instr: instruction) : bool :=
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index b842f86d..883b5477 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -135,9 +135,6 @@ let cfi_rel_offset =
else
(fun _ _ _ -> ())
-(* For handling of annotations *)
-let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
-
(* Basic printing functions *)
let coqint oc n =
fprintf oc "%ld" (camlint_of_coqint n)
@@ -213,8 +210,7 @@ let print_file_line_d2 oc pref file line =
| Some fb -> Printlines.copy oc pref fb line line
end
-
-(** "True" annotations *)
+(** Programmer-supplied annotations (__builtin_annot). *)
let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
@@ -242,7 +238,7 @@ let rec print_annot print_preg sp_reg_name oc = function
fprintf oc "(\"%s\" + %ld)"
(extern_atom id)
(camlint_of_coqint ofs)
- | BA_longofwords(hi, lo) ->
+ | BA_splitlong(hi, lo) ->
fprintf oc "(%a * 0x100000000 + %a)"
(print_annot print_preg sp_reg_name) hi
(print_annot print_preg sp_reg_name) lo
@@ -262,18 +258,27 @@ let print_annot_text print_preg sp_reg_name oc txt args =
List.iter print_fragment (Str.full_split re_annot_param txt);
fprintf oc "\n"
-let print_annot_stmt print_preg sp_reg_name oc txt tys args =
- print_annot_text print_preg sp_reg_name oc txt args
+(* Printing of [EF_debug] info. To be completed. *)
-let print_annot_val print_preg oc txt args =
- print_annot_text print_preg "<internal error>" oc txt
- (List.map (fun r -> BA r) args)
+let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
+let print_debug_info comment print_line print_preg sp_name oc kind txt args =
+ if kind = 1 && Str.string_match re_file_line txt 0 then begin
+ print_line oc (Str.matched_group 1 txt)
+ (int_of_string (Str.matched_group 2 txt))
+ end else begin
+ fprintf oc "%s debug%d: %s" comment kind txt;
+ List.iter
+ (fun a -> fprintf oc " %a" (print_annot print_preg sp_name) a)
+ args;
+ fprintf oc "\n"
+ end
+
(** Inline assembly *)
let print_asm_argument print_preg oc modifier = function
| BA r -> print_preg oc r
- | BA_longofwords(BA hi, BA lo) ->
+ | BA_splitlong(BA hi, BA lo) ->
begin match modifier with
| "R" -> print_preg oc hi
| "Q" -> print_preg oc lo
@@ -284,7 +289,7 @@ let print_asm_argument print_preg oc modifier = function
let builtin_arg_of_res = function
| BR r -> BA r
- | BR_longofwords(BR hi, BR lo) -> BA_longofwords(BA hi, BA lo)
+ | BR_splitlong(BR hi, BR lo) -> BA_splitlong(BA hi, BA lo)
| _ -> assert false
let re_asm_param_1 = Str.regexp "%%\\|%[QR]?[0-9]+"
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 45ad8e19..d818de58 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -401,10 +401,10 @@ Fixpoint convert_builtin_arg {A: Type} (a: builtin_arg expr) (rl: list A) : buil
| BA_addrstack ofs => (BA_addrstack ofs, rl)
| BA_loadglobal chunk id ofs => (BA_loadglobal chunk id ofs, rl)
| BA_addrglobal id ofs => (BA_addrglobal id ofs, rl)
- | BA_longofwords hi lo =>
+ | BA_splitlong hi lo =>
let (hi', rl1) := convert_builtin_arg hi rl in
let (lo', rl2) := convert_builtin_arg lo rl1 in
- (BA_longofwords hi' lo', rl2)
+ (BA_splitlong hi' lo', rl2)
end.
Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list A) : list (builtin_arg A) :=
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 8635ed53..8b30b44f 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -76,7 +76,7 @@ Definition type_of_builtin_arg (a: builtin_arg reg) : typ :=
| BA_addrstack ofs => Tint
| BA_loadglobal chunk id ofs => type_of_chunk chunk
| BA_addrglobal id ofs => Tint
- | BA_longofwords hi lo => Tlong
+ | BA_splitlong hi lo => Tlong
end.
Definition type_of_builtin_res (r: builtin_res reg) : typ :=
@@ -245,7 +245,7 @@ Definition type_builtin_arg (e: S.typenv) (a: builtin_arg reg) (ty: typ) : res S
| BA_addrstack ofs => type_expect e ty Tint
| BA_loadglobal chunk id ofs => type_expect e ty (type_of_chunk chunk)
| BA_addrglobal id ofs => type_expect e ty Tint
- | BA_longofwords hi lo => type_expect e ty Tlong
+ | BA_splitlong hi lo => type_expect e ty Tlong
end.
Fixpoint type_builtin_args (e: S.typenv) (al: list (builtin_arg reg)) (tyl: list typ) : res S.typenv :=
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index b901076e..76288fb5 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -117,7 +117,7 @@ let xparmove srcs dsts k =
let rec convert_builtin_arg tyenv = function
| BA r ->
begin match tyenv r with
- | Tlong -> BA_longofwords(BA(V(r, Tint)), BA(V(twin_reg r, Tint)))
+ | Tlong -> BA_splitlong(BA(V(r, Tint)), BA(V(twin_reg r, Tint)))
| ty -> BA(V(r, ty))
end
| BA_int n -> BA_int n
@@ -128,26 +128,26 @@ let rec convert_builtin_arg tyenv = function
| BA_addrstack(ofs) -> BA_addrstack(ofs)
| BA_loadglobal(chunk, id, ofs) -> BA_loadglobal(chunk, id, ofs)
| BA_addrglobal(id, ofs) -> BA_addrglobal(id, ofs)
- | BA_longofwords(hi, lo) ->
- BA_longofwords(convert_builtin_arg tyenv hi, convert_builtin_arg tyenv lo)
+ | BA_splitlong(hi, lo) ->
+ BA_splitlong(convert_builtin_arg tyenv hi, convert_builtin_arg tyenv lo)
let convert_builtin_res tyenv = function
| BR r ->
begin match tyenv r with
- | Tlong -> BR_longofwords(BR(V(r, Tint)), BR(V(twin_reg r, Tint)))
+ | Tlong -> BR_splitlong(BR(V(r, Tint)), BR(V(twin_reg r, Tint)))
| ty -> BR(V(r, ty))
end
| BR_none -> BR_none
- | BR_longofwords _ -> assert false
+ | BR_splitlong _ -> assert false
let rec constrain_builtin_arg a cl =
match a, cl with
| BA x, None :: cl' -> (a, cl')
| BA x, Some mr :: cl' -> (BA (L(R mr)), cl')
- | BA_longofwords(hi, lo), _ ->
+ | BA_splitlong(hi, lo), _ ->
let (hi', cl1) = constrain_builtin_arg hi cl in
let (lo', cl2) = constrain_builtin_arg lo cl1 in
- (BA_longofwords(hi', lo'), cl2)
+ (BA_splitlong(hi', lo'), cl2)
| _, _ -> (a, cl)
let rec constrain_builtin_args al cl =
@@ -162,10 +162,10 @@ let rec constrain_builtin_res a cl =
match a, cl with
| BR x, None :: cl' -> (a, cl')
| BR x, Some mr :: cl' -> (BR (L(R mr)), cl')
- | BR_longofwords(hi, lo), _ ->
+ | BR_splitlong(hi, lo), _ ->
let (hi', cl1) = constrain_builtin_res hi cl in
let (lo', cl2) = constrain_builtin_res lo cl1 in
- (BR_longofwords(hi', lo'), cl2)
+ (BR_splitlong(hi', lo'), cl2)
| _, _ -> (a, cl)
(* Return the XTL basic block corresponding to the given RTL instruction.
@@ -294,7 +294,7 @@ let vset_addros vos after =
let rec vset_addarg a after =
match a with
| BA v -> VSet.add v after
- | BA_longofwords(hi, lo) -> vset_addarg hi (vset_addarg lo after)
+ | BA_splitlong(hi, lo) -> vset_addarg hi (vset_addarg lo after)
| _ -> after
let vset_addargs al after = List.fold_right vset_addarg al after
@@ -303,7 +303,7 @@ let rec vset_removeres r after =
match r with
| BR v -> VSet.remove v after
| BR_none -> after
- | BR_longofwords(hi, lo) -> vset_removeres hi (vset_removeres lo after)
+ | BR_splitlong(hi, lo) -> vset_removeres hi (vset_removeres lo after)
let live_before instr after =
match instr with
@@ -392,7 +392,7 @@ let rec dce_parmove srcs dsts after =
let rec keep_builtin_arg after = function
| BA v -> VSet.mem v after
- | BA_longofwords(hi, lo) ->
+ | BA_splitlong(hi, lo) ->
keep_builtin_arg after hi && keep_builtin_arg after lo
| _ -> true
@@ -800,10 +800,10 @@ let rec reload_arg tospill eqs = function
| BA v ->
let (t, c1, eqs1) = reload_var tospill eqs v in
(BA t, c1, eqs1)
- | BA_longofwords(hi, lo) ->
+ | BA_splitlong(hi, lo) ->
let (hi', c1, eqs1) = reload_arg tospill eqs hi in
let (lo', c2, eqs2) = reload_arg tospill eqs1 lo in
- (BA_longofwords(hi', lo'), c1 @ c2, eqs2)
+ (BA_splitlong(hi', lo'), c1 @ c2, eqs2)
| a -> (a, [], eqs)
let rec reload_args tospill eqs = function
@@ -827,10 +827,10 @@ let rec save_res tospill eqs = function
(BR t, c1, eqs1)
| BR_none ->
(BR_none, [], eqs)
- | BR_longofwords(hi, lo) ->
+ | BR_splitlong(hi, lo) ->
let (hi', c1, eqs1) = save_res tospill eqs hi in
let (lo', c2, eqs2) = save_res tospill eqs1 lo in
- (BR_longofwords(hi', lo'), c1 @ c2, eqs2)
+ (BR_splitlong(hi', lo'), c1 @ c2, eqs2)
(* Trimming equations when we have too many or when they are too old.
The goal is to limit the live range of unspillable temporaries.
diff --git a/backend/Stacking.v b/backend/Stacking.v
index caf0ae59..ef96e4b3 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -146,8 +146,8 @@ Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg m
BA_addrstack (Int.add ofs (Int.repr fe.(fe_stack_data)))
| BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs
| BA_addrglobal id ofs => BA_addrglobal id ofs
- | BA_longofwords hi lo =>
- BA_longofwords (transl_builtin_arg fe hi) (transl_builtin_arg fe lo)
+ | BA_splitlong hi lo =>
+ BA_splitlong (transl_builtin_arg fe hi) (transl_builtin_arg fe lo)
end.
(** Translation of a Linear instruction. Prepends the corresponding
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 3b0e7133..22121075 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -71,7 +71,7 @@ Fixpoint abuiltin_arg (ae: aenv) (am: amem) (rm: romem) (ba: builtin_arg reg) :
| BA_addrstack ofs => Ptr (Stk ofs)
| BA_loadglobal chunk id ofs => loadv chunk rm am (Ptr (Gl id ofs))
| BA_addrglobal id ofs => Ptr (Gl id ofs)
- | BA_longofwords hi lo => longofwords (abuiltin_arg ae am rm hi) (abuiltin_arg ae am rm lo)
+ | BA_splitlong hi lo => longofwords (abuiltin_arg ae am rm hi) (abuiltin_arg ae am rm lo)
end.
Definition set_builtin_res (br: builtin_res reg) (av: aval) (ae: aenv) : aenv :=
diff --git a/backend/XTL.ml b/backend/XTL.ml
index e05b90d1..dde9bdb0 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -127,7 +127,7 @@ let unify_var_type v1 v2 =
let rec type_builtin_arg a ty =
match a with
| BA v -> set_var_type v ty
- | BA_longofwords(a1, a2) -> type_builtin_arg a1 Tint; type_builtin_arg a2 Tint
+ | BA_splitlong(a1, a2) -> type_builtin_arg a1 Tint; type_builtin_arg a2 Tint
| _ -> ()
let rec type_builtin_args al tyl =
@@ -139,7 +139,7 @@ let rec type_builtin_args al tyl =
let rec type_builtin_res a ty =
match a with
| BR v -> set_var_type v ty
- | BR_longofwords(a1, a2) -> type_builtin_res a1 Tint; type_builtin_res a2 Tint
+ | BR_splitlong(a1, a2) -> type_builtin_res a1 Tint; type_builtin_res a2 Tint
| _ -> ()
let type_instr = function
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index b919c1d4..5cd5997d 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -926,7 +926,7 @@ let add_lineno prev_loc this_loc s =
if !Clflags.option_g && prev_loc <> this_loc && this_loc <> Cutil.no_loc
then begin
let txt = sprintf "#line:%s:%d" (fst this_loc) (snd this_loc) in
- Ssequence(Sdo(Ebuiltin(EF_annot(intern_string txt, []),
+ Ssequence(Sdo(Ebuiltin(EF_debug(P.one, intern_string txt, []),
Tnil, Enil, Tvoid)),
s)
end else
diff --git a/common/AST.v b/common/AST.v
index 1f393c72..4d929f13 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -691,18 +691,18 @@ Inductive builtin_arg (A: Type) : Type :=
| BA_addrstack (ofs: int)
| BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int)
| BA_addrglobal (id: ident) (ofs: int)
- | BA_longofwords (hi lo: builtin_arg A).
+ | BA_splitlong (hi lo: builtin_arg A).
Inductive builtin_res (A: Type) : Type :=
| BR (x: A)
| BR_none
- | BR_longofwords (hi lo: builtin_res A).
+ | BR_splitlong (hi lo: builtin_res A).
Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident :=
match a with
| BA_loadglobal chunk id ofs => id :: nil
| BA_addrglobal id ofs => id :: nil
- | BA_longofwords hi lo => globals_of_builtin_arg hi ++ globals_of_builtin_arg lo
+ | BA_splitlong hi lo => globals_of_builtin_arg hi ++ globals_of_builtin_arg lo
| _ => nil
end.
@@ -712,7 +712,7 @@ Definition globals_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list i
Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A :=
match a with
| BA x => x :: nil
- | BA_longofwords hi lo => params_of_builtin_arg hi ++ params_of_builtin_arg lo
+ | BA_splitlong hi lo => params_of_builtin_arg hi ++ params_of_builtin_arg lo
| _ => nil
end.
@@ -723,7 +723,7 @@ Fixpoint params_of_builtin_res (A: Type) (a: builtin_res A) : list A :=
match a with
| BR x => x :: nil
| BR_none => nil
- | BR_longofwords hi lo => params_of_builtin_res hi ++ params_of_builtin_res lo
+ | BR_splitlong hi lo => params_of_builtin_res hi ++ params_of_builtin_res lo
end.
Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_arg B :=
@@ -737,16 +737,16 @@ Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_ar
| BA_addrstack ofs => BA_addrstack ofs
| BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs
| BA_addrglobal id ofs => BA_addrglobal id ofs
- | BA_longofwords hi lo =>
- BA_longofwords (map_builtin_arg f hi) (map_builtin_arg f lo)
+ | BA_splitlong hi lo =>
+ BA_splitlong (map_builtin_arg f hi) (map_builtin_arg f lo)
end.
Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B :=
match a with
| BR x => BR (f x)
| BR_none => BR_none
- | BR_longofwords hi lo =>
- BR_longofwords (map_builtin_res f hi) (map_builtin_res f lo)
+ | BR_splitlong hi lo =>
+ BR_splitlong (map_builtin_res f hi) (map_builtin_res f lo)
end.
(** Which kinds of builtin arguments are supported by which external function. *)
@@ -762,7 +762,7 @@ Inductive builtin_arg_constraint : Type :=
Definition builtin_arg_ok
(A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
match ba, c with
- | (BA _ | BA_longofwords _ _), _ => true
+ | (BA _ | BA_splitlong _ _), _ => true
| (BA_int _ | BA_long _ | BA_float _ | BA_single _), OK_const => true
| BA_addrstack _, (OK_addrstack | OK_addrany) => true
| BA_addrglobal _ _, (OK_addrglobal | OK_addrany) => true
diff --git a/common/Events.v b/common/Events.v
index ab418ba5..7cd9155e 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1724,9 +1724,9 @@ Inductive eval_builtin_arg: builtin_arg A -> val -> Prop :=
eval_builtin_arg (BA_loadglobal chunk id ofs) v
| eval_BA_addrglobal: forall id ofs,
eval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address ge id ofs)
- | eval_BA_longofwords: forall hi lo vhi vlo,
+ | eval_BA_splitlong: forall hi lo vhi vlo,
eval_builtin_arg hi vhi -> eval_builtin_arg lo vlo ->
- eval_builtin_arg (BA_longofwords hi lo) (Val.longofwords vhi vlo).
+ eval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo).
Definition eval_builtin_args (al: list (builtin_arg A)) (vl: list val) : Prop :=
list_forall2 eval_builtin_arg al vl.
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 5f1db76b..aea8ff0f 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -66,8 +66,8 @@ let rec print_builtin_arg px oc = function
(name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs)
| BA_addrglobal(id, ofs) ->
fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs)
- | BA_longofwords(hi, lo) ->
- fprintf oc "long(%a, %a)"
+ | BA_splitlong(hi, lo) ->
+ fprintf oc "splitlong(%a, %a)"
(print_builtin_arg px) hi (print_builtin_arg px) lo
let rec print_builtin_args px oc = function
@@ -79,7 +79,7 @@ let rec print_builtin_args px oc = function
let rec print_builtin_res px oc = function
| BR x -> px oc x
| BR_none -> fprintf oc "_"
- | BR_longofwords(hi, lo) ->
- fprintf oc "long(%a, %a)"
+ | BR_splitlong(hi, lo) ->
+ fprintf oc "splitlong(%a, %a)"
(print_builtin_res px) hi (print_builtin_res px) lo
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 96a49005..979041ba 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -293,7 +293,7 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
match res with
| BR r => rs#r <- v
| BR_none => rs
- | BR_longofwords hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+ | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
end.
Section RELSEM.
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index 8996794b..a2a7a9be 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -140,7 +140,7 @@ let expand_builtin_vload_common chunk addr res =
emit (Pmovsw_rm (res,addr))
| Mint32, BR(IR res) ->
emit (Pmov_rm (res,addr))
- | Mint64, BR_longofwords(BR(IR res1), BR(IR res2)) ->
+ | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) ->
let addr' = offset_addressing addr _4 in
if not (Asmgen.addressing_mentions addr res2) then begin
emit (Pmov_rm (res2,addr));
@@ -176,7 +176,7 @@ let expand_builtin_vstore_common chunk addr src tmp =
emit (Pmovw_mr (addr,src))
| Mint32, BA(IR src) ->
emit (Pmov_mr (addr,src))
- | Mint64, BA_longofwords(BA(IR src1), BA(IR src2)) ->
+ | Mint64, BA_splitlong(BA(IR src1), BA(IR src2)) ->
let addr' = offset_addressing addr _4 in
emit (Pmov_mr (addr,src2));
emit (Pmov_mr (addr',src1))
@@ -293,26 +293,26 @@ let expand_builtin_inline name args res =
(fun r1 r2 r3 -> Pfnmsub213(r1, r2, r3))
(fun r1 r2 r3 -> Pfnmsub231(r1, r2, r3))
(* 64-bit integer arithmetic *)
- | "__builtin_negl", [BA_longofwords(BA(IR ah), BA(IR al))],
- BR_longofwords(BR(IR rh), BR(IR rl)) ->
+ | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))],
+ BR_splitlong(BR(IR rh), BR(IR rl)) ->
assert (ah = EDX && al = EAX && rh = EDX && rl = EAX);
emit (Pneg EAX);
emit (Padc_ri (EDX,_0));
emit (Pneg EDX)
- | "__builtin_addl", [BA_longofwords(BA(IR ah), BA(IR al));
- BA_longofwords(BA(IR bh), BA(IR bl))],
- BR_longofwords(BR(IR rh), BR(IR rl)) ->
+ | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al));
+ BA_splitlong(BA(IR bh), BA(IR bl))],
+ BR_splitlong(BR(IR rh), BR(IR rl)) ->
assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX);
emit (Padd_rr (EAX,EBX));
emit (Padc_rr (EDX,ECX))
- | "__builtin_subl", [BA_longofwords(BA(IR ah), BA(IR al));
- BA_longofwords(BA(IR bh), BA(IR bl))],
- BR_longofwords(BR(IR rh), BR(IR rl)) ->
+ | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al));
+ BA_splitlong(BA(IR bh), BA(IR bl))],
+ BR_splitlong(BR(IR rh), BR(IR rl)) ->
assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX);
emit (Psub_rr (EAX,EBX));
emit (Psbb_rr (EDX,ECX))
| "__builtin_mull", [BA(IR a); BA(IR b)],
- BR_longofwords(BR(IR rh), BR(IR rl)) ->
+ BR_splitlong(BR(IR rh), BR(IR rl)) ->
assert (a = EAX && b = EDX && rh = EDX && rl = EAX);
emit (Pmul_r EDX)
(* Memory accesses *)
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 744902ec..bc331b9c 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -516,7 +516,7 @@ Nondetfunction builtin_arg (e: expr) :=
| Eop (Olea (Ainstack ofs)) Enil => BA_addrstack ofs
| Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
BA_long (Int64.ofwords h l)
- | Eop Omakelong (h ::: l ::: Enil) => BA_longofwords (BA h) (BA l)
+ | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
| Eload chunk (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs
| Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
| _ => BA e
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index beddd1e8..9e4babb7 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -337,17 +337,6 @@ module Target(System: SYSTEM):TARGET =
- inlined by the compiler: take their arguments in arbitrary
registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *)
-(* Handling of annotations *)
-
- let print_annot_stmt oc txt targs args =
- if Str.string_match re_file_line txt 0 then begin
- print_file_line oc (Str.matched_group 1 txt)
- (int_of_string (Str.matched_group 2 txt))
- end else begin
- fprintf oc "%s annotation: " comment;
- print_annot_stmt preg "%esp" oc txt targs args
- end
-
(* Handling of varargs *)
let print_builtin_va_start oc r =
@@ -658,7 +647,11 @@ module Target(System: SYSTEM):TARGET =
| Pbuiltin(ef, args, res) ->
begin match ef with
| EF_annot(txt, targs) ->
- print_annot_stmt oc (extern_atom txt) targs args
+ fprintf oc "%s annotation: " comment;
+ print_annot_text preg_annot "%esp" oc (extern_atom txt) args
+ | EF_debug(kind, txt, targs) ->
+ print_debug_info comment print_file_line preg "%esp" oc
+ (P.to_int kind) (extern_atom txt) args
| EF_inline_asm(txt, sg, clob) ->
fprintf oc "%s begin inline assembly\n\t" comment;
print_inline_asm preg oc (extern_atom txt) sg args res;
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index a724f932..589d66fe 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -393,7 +393,7 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
match res with
| BR r => rs#r <- v
| BR_none => rs
- | BR_longofwords hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+ | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
end.
Section RELSEM.
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 9f6c5f76..e09291cc 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -62,7 +62,7 @@ let expand_annot_val txt targ args res =
So, use 64-bit accesses only if alignment >= 4.
Note that lfd and stfd cannot trap on ill-formed floats. *)
-let memcpy_small_arg sz arg otherarg tmp1 tmp2 =
+let memcpy_small_arg sz arg tmp =
match arg with
| BA (IR r) ->
(r, _0)
@@ -71,17 +71,15 @@ let memcpy_small_arg sz arg otherarg tmp1 tmp2 =
&& Int.eq (Asmgen.high_s (Int.add ofs (Int.repr (Z.of_uint sz))))
Int.zero
then (GPR1, ofs)
- else begin
- let tmp = if otherarg = BA (IR tmp1) then tmp2 else tmp1 in
- emit_addimm tmp GPR1 ofs;
- (tmp, _0)
- end
+ else begin emit_addimm tmp GPR1 ofs; (tmp, _0) end
| _ ->
assert false
let expand_builtin_memcpy_small sz al src dst =
- let (rsrc, osrc) = memcpy_small_arg sz src dst GPR11 GPR12 in
- let (rdst, odst) = memcpy_small_arg sz dst src GPR12 GPR11 in
+ let (tsrc, tdst) =
+ if dst <> BA (IR GPR11) then (GPR11, GPR12) else (GPR12, GPR11) in
+ let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
+ let (rdst, odst) = memcpy_small_arg sz dst tdst in
let rec copy osrc odst sz =
if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
emit (Plfd(FPR13, Cint osrc, rsrc));
@@ -174,7 +172,7 @@ let rec expand_builtin_vload_common chunk base offset res =
emit (Plfs(res, offset, base))
| (Mfloat64 | Many64), BR(FR res) ->
emit (Plfd(res, offset, base))
- | Mint64, BR_longofwords(BR(IR hi), BR(IR lo)) ->
+ | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) ->
begin match offset_constant offset _4 with
| Some offset' ->
if hi <> base then begin
@@ -232,7 +230,7 @@ let expand_builtin_vstore_common chunk base offset src =
emit (Pstfs(src, offset, base))
| (Mfloat64 | Many64), BA(FR src) ->
emit (Pstfd(src, offset, base))
- | Mint64, BA_longofwords(BA(IR hi), BA(IR lo)) ->
+ | Mint64, BA_splitlong(BA(IR hi), BA(IR lo)) ->
begin match offset_constant offset _4 with
| Some offset' ->
emit (Pstw(hi, offset, base));
@@ -371,25 +369,25 @@ let expand_builtin_inline name args res =
emit (Paddi(GPR1, GPR1, Cint _8));
emit (Pcfi_adjust _m8)
(* 64-bit integer arithmetic *)
- | "__builtin_negl", [BA_longofwords(BA(IR ah), BA(IR al))],
- BR_longofwords(BR(IR rh), BR(IR rl)) ->
+ | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))],
+ BR_splitlong(BR(IR rh), BR(IR rl)) ->
expand_int64_arith (rl = ah) rl (fun rl ->
emit (Psubfic(rl, al, Cint _0));
emit (Psubfze(rh, ah)))
- | "__builtin_addl", [BA_longofwords(BA(IR ah), BA(IR al));
- BA_longofwords(BA(IR bh), BA(IR bl))],
- BR_longofwords(BR(IR rh), BR(IR rl)) ->
+ | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al));
+ BA_splitlong(BA(IR bh), BA(IR bl))],
+ BR_splitlong(BR(IR rh), BR(IR rl)) ->
expand_int64_arith (rl = ah || rl = bh) rl (fun rl ->
emit (Paddc(rl, al, bl));
emit (Padde(rh, ah, bh)))
- | "__builtin_subl", [BA_longofwords(BA(IR ah), BA(IR al));
- BA_longofwords(BA(IR bh), BA(IR bl))],
- BR_longofwords(BR(IR rh), BR(IR rl)) ->
+ | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al));
+ BA_splitlong(BA(IR bh), BA(IR bl))],
+ BR_splitlong(BR(IR rh), BR(IR rl)) ->
expand_int64_arith (rl = ah || rl = bh) rl (fun rl ->
emit (Psubfc(rl, bl, al));
emit (Psubfe(rh, bh, ah)))
| "__builtin_mull", [BA(IR a); BA(IR b)],
- BR_longofwords(BR(IR rh), BR(IR rl)) ->
+ BR_splitlong(BR(IR rh), BR(IR rl)) ->
expand_int64_arith (rl = a || rl = b) rl (fun rl ->
emit (Pmullw(rl, a, b));
emit (Pmulhwu(rh, a, b)))
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 31f7e2e4..6d39569e 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -533,7 +533,7 @@ Nondetfunction builtin_arg (e: expr) :=
| Eop (Oaddrstack ofs) Enil => BA_addrstack ofs
| Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
BA_long (Int64.ofwords h l)
- | Eop Omakelong (h ::: l ::: Enil) => BA_longofwords (BA h) (BA l)
+ | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
| Eload chunk (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs
| Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
| _ => BA e
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 5431d88d..ced26783 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -358,17 +358,6 @@ module Target (System : SYSTEM):TARGET =
assert (!count = 2 || (!count = 0 && !last));
(!mb, !me-1)
- (* Handling of annotations *)
-
- let print_annot_stmt oc txt targs args =
- if Str.string_match re_file_line txt 0 then begin
- print_file_line oc (Str.matched_group 1 txt)
- (int_of_string (Str.matched_group 2 txt))
- end else begin
- fprintf oc "%s annotation: " comment;
- print_annot_stmt preg_annot "R1" oc txt targs args
- end
-
(* Determine if the displacement of a conditional branch fits the short form *)
let short_cond_branch tbl pc lbl_dest =
@@ -698,7 +687,11 @@ module Target (System : SYSTEM):TARGET =
| Pbuiltin(ef, args, res) ->
begin match ef with
| EF_annot(txt, targs) ->
- print_annot_stmt oc (extern_atom txt) targs args
+ fprintf oc "%s annotation: " comment;
+ print_annot_text preg_annot "r1" oc (extern_atom txt) args
+ | EF_debug(kind, txt, targs) ->
+ print_debug_info comment print_file_line preg_annot "r1" oc
+ (P.to_int kind) (extern_atom txt) args
| EF_inline_asm(txt, sg, clob) ->
fprintf oc "%s begin inline assembly\n\t" comment;
print_inline_asm preg oc (extern_atom txt) sg args res;