aboutsummaryrefslogtreecommitdiffstats
path: root/common
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 /common
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.
Diffstat (limited to 'common')
-rw-r--r--common/AST.v20
-rw-r--r--common/Events.v4
-rw-r--r--common/PrintAST.ml8
3 files changed, 16 insertions, 16 deletions
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