aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/CMparser.mly3
-rw-r--r--backend/PrintAnnot.ml65
-rw-r--r--backend/PrintLTL.ml4
-rw-r--r--backend/PrintMach.ml12
-rw-r--r--backend/Regalloc.ml26
-rw-r--r--backend/Selection.v13
-rw-r--r--backend/Selectionproof.v31
-rw-r--r--backend/Splitting.ml2
-rw-r--r--backend/XTL.ml4
-rw-r--r--backend/XTL.mli1
-rw-r--r--cfrontend/C2C.ml3
-rw-r--r--common/PrintAST.ml6
-rw-r--r--ia32/TargetPrinter.ml2
-rw-r--r--test/regression/annot1.c36
14 files changed, 130 insertions, 78 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 10cf8bf4..69b70e72 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -55,8 +55,7 @@ let mkef sg toks =
| [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] ->
EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al)
| [EFT_tok "annot"; EFT_string txt] ->
- EF_annot(intern_string txt,
- List.map (fun t -> AA_arg t) sg.sig_args)
+ EF_annot(intern_string txt, sg.sig_args)
| [EFT_tok "annot_val"; EFT_string txt] ->
if sg.sig_args = [] then raise Parsing.Parse_error;
EF_annot_val(intern_string txt, List.hd sg.sig_args)
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml
index 54174b9f..0176224d 100644
--- a/backend/PrintAnnot.ml
+++ b/backend/PrintAnnot.ml
@@ -90,11 +90,34 @@ let print_file_line_d1 oc pref file line =
let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
-type arg_value =
- | Reg of preg
- | Stack of memory_chunk * Int.int
- | Intconst of Int.int
- | Floatconst of float
+let rec print_annot print_preg sp_reg_name oc = function
+ | AA_base x -> print_preg oc x
+ | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n)
+ | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n)
+ | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n)
+ | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n)
+ | AA_loadstack(chunk, ofs) ->
+ fprintf oc "mem(%s + %ld, %ld)"
+ sp_reg_name
+ (camlint_of_coqint ofs)
+ (camlint_of_coqint (size_chunk chunk))
+ | AA_addrstack ofs ->
+ fprintf oc "(%s + %ld)"
+ sp_reg_name
+ (camlint_of_coqint ofs)
+ | AA_loadglobal(chunk, id, ofs) ->
+ fprintf oc "mem(\"%s\" + %ld, %ld)"
+ (extern_atom id)
+ (camlint_of_coqint ofs)
+ (camlint_of_coqint (size_chunk chunk))
+ | AA_addrglobal(id, ofs) ->
+ fprintf oc "(\"%s\" + %ld)"
+ (extern_atom id)
+ (camlint_of_coqint ofs)
+ | AA_longofwords(hi, lo) ->
+ fprintf oc "(%a * 0x100000000 + %a)"
+ (print_annot print_preg sp_reg_name) hi
+ (print_annot print_preg sp_reg_name) lo
let print_annot_text print_preg sp_reg_name oc txt args =
let print_fragment = function
@@ -105,42 +128,18 @@ let print_annot_text print_preg sp_reg_name oc txt args =
| Str.Delim s ->
let n = int_of_string (String.sub s 1 (String.length s - 1)) in
try
- match List.nth args (n-1) with
- | Reg r ->
- print_preg oc r
- | Stack(chunk, ofs) ->
- fprintf oc "mem(%s + %ld, %ld)"
- sp_reg_name
- (camlint_of_coqint ofs)
- (camlint_of_coqint (size_chunk chunk))
- | Intconst n ->
- fprintf oc "%ld" (camlint_of_coqint n)
- | Floatconst n ->
- fprintf oc "%.18g" (camlfloat_of_coqfloat n)
+ print_annot print_preg sp_reg_name oc (List.nth args (n-1))
with Failure _ ->
fprintf oc "<bad parameter %s>" s in
List.iter print_fragment (Str.full_split re_annot_param txt);
fprintf oc "\n"
-let rec annot_args tmpl args =
- match tmpl, args with
- | [], _ -> []
- | AA_arg _ :: tmpl', APreg r :: args' ->
- Reg r :: annot_args tmpl' args'
- | AA_arg _ :: tmpl', APstack(chunk, ofs) :: args' ->
- Stack(chunk, ofs) :: annot_args tmpl' args'
- | AA_arg _ :: tmpl', [] -> [] (* should never happen *)
- | AA_int n :: tmpl', _ ->
- Intconst n :: annot_args tmpl' args
- | AA_float n :: tmpl', _ ->
- Floatconst n :: annot_args tmpl' args
-
-let print_annot_stmt print_preg sp_reg_name oc txt tmpl args =
- print_annot_text print_preg sp_reg_name oc txt (annot_args tmpl args)
+let print_annot_stmt print_preg sp_reg_name oc txt tys args =
+ print_annot_text print_preg sp_reg_name oc txt args
let print_annot_val print_preg oc txt args =
print_annot_text print_preg "<internal error>" oc txt
- (List.map (fun r -> Reg r) args)
+ (List.map (fun r -> AA_base r) args)
(* Print CompCert version and command-line as asm comment *)
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index 52e51309..27936f9b 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -81,8 +81,8 @@ let print_instruction pp succ = function
fprintf pp "%a = %s(%a)"
mregs res (name_of_external ef) mregs args
| Lannot(ef, args) ->
- fprintf pp "%s(%a)"
- (name_of_external ef) locs args
+ fprintf pp "%s(%a)\n"
+ (name_of_external ef) (print_annot_args loc) args
| Lbranch s ->
print_succ pp s succ
| Lcond(cond, args, s1, s2) ->
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index b356ca9e..8484a5c3 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -34,15 +34,6 @@ let rec regs pp = function
| [r] -> reg pp r
| r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
-let annot_param pp = function
- | APreg r -> reg pp r
- | APstack(chunk, ofs) -> fprintf pp "stack(%s,%ld)" (name_of_chunk chunk) (camlint_of_coqint ofs)
-
-let rec annot_params pp = function
- | [] -> ()
- | [r] -> annot_param pp r
- | r1::rl -> fprintf pp "%a, %a" annot_param r1 annot_params rl
-
let ros pp = function
| Coq_inl r -> reg pp r
| Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
@@ -78,7 +69,8 @@ let print_instruction pp i =
fprintf pp "\t%a = %s(%a)\n"
regs res (name_of_external ef) regs args
| Mannot(ef, args) ->
- fprintf pp "\t%s(%a)\n" (name_of_external ef) annot_params args
+ fprintf pp "\t%s(%a)\n"
+ (name_of_external ef) (print_annot_args reg) args
| Mlabel lbl ->
fprintf pp "%5d:" (P.to_int lbl)
| Mgoto lbl ->
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 6c15e15e..3a7f5d99 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -114,10 +114,11 @@ let xparmove srcs dsts k =
| [src], [dst] -> move src dst k
| _, _ -> Xparmove(srcs, dsts, new_temp Tint, new_temp Tfloat) :: k
-let convert_annot_arg tyenv = function
+let rec convert_annot_arg tyenv = function
| AA_base r ->
begin match tyenv r with
- | Tlong -> AA_longofwords(V(r, Tint), V(twin_reg r, Tint))
+ | Tlong -> AA_longofwords(AA_base(V(r, Tint)),
+ AA_base(V(twin_reg r, Tint)))
| ty -> AA_base(V(r, ty))
end
| AA_int n -> AA_int n
@@ -128,7 +129,8 @@ let convert_annot_arg tyenv = function
| AA_addrstack(ofs) -> AA_addrstack(ofs)
| AA_loadglobal(chunk, id, ofs) -> AA_loadglobal(chunk, id, ofs)
| AA_addrglobal(id, ofs) -> AA_addrglobal(id, ofs)
- | AA_longofwords(hi, lo) -> AA_longofwords(vreg tyenv hi, vreg tyenv lo)
+ | AA_longofwords(hi, lo) ->
+ AA_longofwords(convert_annot_arg tyenv hi, convert_annot_arg tyenv lo)
(* Return the XTL basic block corresponding to the given RTL instruction.
Move and parallel move instructions are introduced to honor calling
@@ -249,10 +251,10 @@ let vset_removelist vl after = List.fold_right VSet.remove vl after
let vset_addlist vl after = List.fold_right VSet.add vl after
let vset_addros vos after =
match vos with Coq_inl v -> VSet.add v after | Coq_inr id -> after
-let vset_addannot a after =
+let rec vset_addannot a after =
match a with
| AA_base v -> VSet.add v after
- | AA_longofwords(hi, lo) -> VSet.add hi (VSet.add lo after)
+ | AA_longofwords(hi, lo) -> vset_addannot hi (vset_addannot lo after)
| _ -> after
let live_before instr after =
@@ -932,18 +934,6 @@ let make_parmove srcs dsts itmp ftmp k =
done;
List.rev_append !code k
-let transl_annot_arg alloc = function
- | AA_base v -> AA_base (alloc v)
- | AA_int n -> AA_int n
- | AA_long n -> AA_long n
- | AA_float n -> AA_float n
- | AA_single n -> AA_single n
- | AA_loadstack(chunk, ofs) -> AA_loadstack(chunk, ofs)
- | AA_addrstack(ofs) -> AA_addrstack(ofs)
- | AA_loadglobal(chunk, id, ofs) -> AA_loadglobal(chunk, id, ofs)
- | AA_addrglobal(id, ofs) -> AA_addrglobal(id, ofs)
- | AA_longofwords(hi, lo) -> AA_longofwords(alloc hi, alloc lo)
-
let transl_instr alloc instr k =
match instr with
| Xmove(src, dst) | Xreload(src, dst) | Xspill(src, dst) ->
@@ -975,7 +965,7 @@ let transl_instr alloc instr k =
| Xbuiltin(ef, args, res) ->
LTL.Lbuiltin(ef, mregs_of alloc args, mregs_of alloc res) :: k
| Xannot(ef, args) ->
- LTL.Lannot(ef, List.map (transl_annot_arg alloc) args) :: k
+ LTL.Lannot(ef, List.map (AST.map_annot_arg alloc) args) :: k
| Xbranch s ->
LTL.Lbranch s :: []
| Xcond(cond, args, s1, s2) ->
diff --git a/backend/Selection.v b/backend/Selection.v
index 5cec6e00..ae9da0a7 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -203,12 +203,23 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind :=
end
end.
+(** Annotations *)
+
Definition builtin_is_annot (ef: external_function) (optid: option ident) : bool :=
match ef, optid with
| EF_annot _ _, None => true
| _, _ => false
end.
+Function sel_annot_arg (e: Cminor.expr) : AST.annot_arg expr :=
+ match e with
+ | Cminor.Econst (Cminor.Oaddrsymbol id ofs) => AA_addrglobal id ofs
+ | Cminor.Econst (Cminor.Oaddrstack ofs) => AA_addrstack ofs
+ | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrsymbol id ofs)) => AA_loadglobal chunk id ofs
+ | Cminor.Eload chunk (Cminor.Econst (Cminor.Oaddrstack ofs)) => AA_loadstack chunk ofs
+ | _ => annot_arg (sel_expr e)
+ end.
+
(** Conversion of Cminor [switch] statements to decision trees. *)
Parameter compile_switch: Z -> nat -> table -> comptree.
@@ -270,7 +281,7 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt :=
end)
| Cminor.Sbuiltin optid ef args =>
OK (if builtin_is_annot ef optid
- then Sannot ef (List.map (fun e => annot_arg (sel_expr e)) args)
+ then Sannot ef (List.map sel_annot_arg args)
else Sbuiltin optid ef (sel_exprlist args))
| Cminor.Stailcall sg fn args =>
OK (match classify_call ge fn with
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index d755d46d..392959d4 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -598,6 +598,29 @@ Proof.
exists (v1' :: vl'); split; auto. constructor; eauto.
Qed.
+Lemma sel_annot_arg_correct:
+ forall sp e e' m m',
+ env_lessdef e e' -> Mem.extends m m' ->
+ forall a v,
+ Cminor.eval_expr ge sp e m a v ->
+ exists v',
+ CminorSel.eval_annot_arg tge sp e' m' (sel_annot_arg a) v'
+ /\ Val.lessdef v v'.
+Proof.
+ intros until v. functional induction (sel_annot_arg a); intros EV.
+- inv EV. simpl in H2; inv H2. econstructor; split. constructor.
+ unfold Genv.symbol_address. rewrite symbols_preserved. auto.
+- inv EV. simpl in H2; inv H2. econstructor; split. constructor. auto.
+- inv EV. inv H3. exploit Mem.loadv_extends; eauto. intros (v' & A & B).
+ exists v'; split; auto. constructor.
+ replace (Genv.symbol_address tge id ofs) with vaddr; auto.
+ simpl in H2; inv H2. unfold Genv.symbol_address. rewrite symbols_preserved. auto.
+- inv EV. inv H3. simpl in H2; inv H2. exploit Mem.loadv_extends; eauto. intros (v' & A & B).
+ exists v'; split; auto. constructor; auto.
+- exploit sel_expr_correct; eauto. intros (v1 & A & B).
+ exists v1; split; auto. eapply eval_annot_arg; eauto.
+Qed.
+
Lemma sel_annot_args_correct:
forall sp e e' m m',
env_lessdef e e' -> Mem.extends m m' ->
@@ -605,16 +628,15 @@ Lemma sel_annot_args_correct:
Cminor.eval_exprlist ge sp e m al vl ->
exists vl',
list_forall2 (CminorSel.eval_annot_arg tge sp e' m')
- (List.map (fun a => annot_arg (sel_expr a)) al)
+ (List.map sel_annot_arg al)
vl'
/\ Val.lessdef_list vl vl'.
Proof.
induction 3; simpl.
- exists (@nil val); split; constructor.
-- exploit sel_expr_correct; eauto. intros (v1' & A & B).
+- exploit sel_annot_arg_correct; eauto. intros (v1' & A & B).
destruct IHeval_exprlist as (vl' & C & D).
- exists (v1' :: vl'); split; auto.
- constructor; auto. eapply eval_annot_arg; eauto.
+ exists (v1' :: vl'); split; auto. constructor; auto.
Qed.
(** Semantic preservation for functions and statements. *)
@@ -813,7 +835,6 @@ Proof.
assert (Y: optid = None).
{ destruct ef; try discriminate. destruct optid; try discriminate. auto. }
exploit sel_annot_args_correct; eauto.
- set (bl' := map (fun e => annot_arg (sel_expr e)) bl).
intros (vargs' & P & Q).
exploit external_call_mem_extends; eauto.
intros [vres' [m2 [A [B [C D]]]]].
diff --git a/backend/Splitting.ml b/backend/Splitting.ml
index 3530ba99..53600c98 100644
--- a/backend/Splitting.ml
+++ b/backend/Splitting.ml
@@ -163,6 +163,8 @@ let ren_instr f maps pc i =
Itailcall(sg, ren_ros before ros, ren_regs before args)
| Ibuiltin(ef, args, res, s) ->
Ibuiltin(ef, ren_regs before args, ren_reg after res, s)
+ | Iannot(ef, args, s) ->
+ Iannot(ef, List.map (AST.map_annot_arg (ren_reg before)) args, s)
| Icond(cond, args, s1, s2) ->
Icond(cond, ren_regs before args, s1, s2)
| Ijumptable(arg, tbl) ->
diff --git a/backend/XTL.ml b/backend/XTL.ml
index 30c09fdf..0e5ce0c4 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -125,10 +125,10 @@ let rec set_vars_type vl tyl =
let unify_var_type v1 v2 =
if typeof v1 <> typeof v2 then raise Type_error
-let type_annot_arg a ty =
+let rec type_annot_arg a ty =
match a with
| AA_base v -> set_var_type v ty
- | AA_longofwords(v1, v2) -> set_var_type v1 Tint; set_var_type v2 Tint
+ | AA_longofwords(a1, a2) -> type_annot_arg a1 Tint; type_annot_arg a2 Tint
| _ -> ()
let type_instr = function
diff --git a/backend/XTL.mli b/backend/XTL.mli
index 75a3d657..9794565c 100644
--- a/backend/XTL.mli
+++ b/backend/XTL.mli
@@ -36,6 +36,7 @@ type instruction =
| Xcall of signature * (var, ident) sum * var list * var list
| Xtailcall of signature * (var, ident) sum * var list
| Xbuiltin of external_function * var list * var list
+ | Xannot of external_function * var annot_arg list
| Xbranch of node
| Xcond of condition * var list * node * node
| Xjumptable of var * node list
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 2b9a54a4..47e876f7 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -713,8 +713,7 @@ let rec convertExpr env e =
| {edesc = C.EConst(CStr txt)} :: args1 ->
let targs1 = convertTypArgs env [] args1 in
Ebuiltin(
- EF_annot(intern_string txt,
- List.map (fun t -> AA_arg t) (typlist_of_typelist targs1)),
+ EF_annot(intern_string txt, typlist_of_typelist targs1),
targs1, convertExprList env args1, convertTyp env e.etyp)
| _ ->
error "ill-formed __builtin_annot (first argument must be string literal)";
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index e4d79c3e..52aa963a 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -55,7 +55,7 @@ let name_of_external = function
| EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text)
| EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text)
-let print_annot_arg px oc = function
+let rec print_annot_arg px oc = function
| AA_base x -> px oc x
| AA_int n -> fprintf oc "int %ld" (camlint_of_coqint n)
| AA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n)
@@ -70,7 +70,9 @@ let print_annot_arg px oc = function
(name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs)
| AA_addrglobal(id, ofs) ->
fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs)
- | AA_longofwords(hi, lo) -> fprintf oc "longofwords %a %a" px hi px lo
+ | AA_longofwords(hi, lo) ->
+ fprintf oc "longofwords(%a, %a)"
+ (print_annot_arg px) hi (print_annot_arg px) lo
let rec print_annot_args px oc = function
| [] -> ()
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 888a7e72..0de38471 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -339,7 +339,7 @@ module Target(System: SYSTEM):TARGET =
(int_of_string (Str.matched_group 2 txt))
end else begin
fprintf oc "%s annotation: " comment;
- PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args
+ PrintAnnot.print_annot_stmt preg "%esp" oc txt targs args
end
let print_annot_val oc txt args res =
diff --git a/test/regression/annot1.c b/test/regression/annot1.c
index 9bdf14eb..b60f8a64 100644
--- a/test/regression/annot1.c
+++ b/test/regression/annot1.c
@@ -58,6 +58,42 @@ void k(int arg)
C1 + 1, arg, C2 * 2);
}
+int j(int a)
+{
+ /* Local variables that are stack-allocated early */
+ short b = 0, c = 0;
+ char d[4];
+ *(a ? &b : &c) = 42;
+ __builtin_annot("j %1 %2 %3 %4", b, c, d[0], d[3]);
+ return b;
+}
+
+long long ll(long long a)
+{
+ /* Force spilling */
+ long long b = a+1;
+ long long c = b+1;
+ long long d = c+1;
+ long long e = d+1;
+ long long f = e+1;
+ long long g = f+1;
+ long long h = g+1;
+ long long i = h+1;
+ long long j = i+1;
+ long long k = j+1;
+ long long l = k+1;
+ long long m = l+1;
+ long long n = m+1;
+ long long o = n+1;
+ long long p = o+1;
+ long long q = p+1;
+ long long r = q+1;
+ long long s = r+1;
+ long long t = s+1;
+ __builtin_annot("ll %1 %2 %3 %4 %5 %6 %7 %8 %9 %10 %11 %12 %13 %14 %15 %16 %17 %18 %19 %20", a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t);
+ return t;
+}
+
int main()
{
__builtin_annot("calling f");
generated by cgit (git 2.34.1) at 2024-06-11 22:35:12 +0000