From 33b742bb41725e47bd88dc12f2a4f40173023f83 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 27 Mar 2015 14:24:03 +0100 Subject: Updated the Caml part. Added some more tests in annot1.c. --- backend/CMparser.mly | 3 +-- backend/PrintAnnot.ml | 65 ++++++++++++++++++++++++------------------------ backend/PrintLTL.ml | 4 +-- backend/PrintMach.ml | 12 ++------- backend/Regalloc.ml | 26 ++++++------------- backend/Selection.v | 13 +++++++++- backend/Selectionproof.v | 31 +++++++++++++++++++---- backend/Splitting.ml | 2 ++ backend/XTL.ml | 4 +-- backend/XTL.mli | 1 + cfrontend/C2C.ml | 3 +-- common/PrintAST.ml | 6 +++-- ia32/TargetPrinter.ml | 2 +- test/regression/annot1.c | 36 +++++++++++++++++++++++++++ 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 "" 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 "" 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"); -- cgit