From 1b5db339bb05f773a6a132be4c0b8cea54d50461 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 17 Apr 2015 16:30:43 +0200 Subject: Experiment: support a subset of GCC's extended asm statements. --- cfrontend/C2C.ml | 95 +++++++++++++++++++++++++++++++++++++++++++++++++++++-- cfrontend/Cexec.v | 16 +++++----- 2 files changed, 101 insertions(+), 10 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index fd10efb4..7413c443 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -831,6 +831,97 @@ and convertExprList env el = | [] -> Enil | e1 :: el' -> Econs(convertExpr env e1, convertExprList env el') +(** ** Extended assembly *) + +module StringMap = Map.Make(String) + +let re_asm_placeholder = + Str.regexp "\\(%[0-9]+\\|%\\[[a-zA-Z_][a-zA-Z_0-9]*\\]\\|%%\\)" + +let convertAsm env txt outputs inputs clobber = + + (* On the fly renaming of labeled and numbered arguments *) + let name_of_label lbl pos = + match lbl with + | None -> sprintf "%%%d" pos + | Some l -> sprintf "%%[%s]" l in + let set_label_reg lbl pos pos' subst = + StringMap.add (name_of_label lbl pos) (sprintf "%%%d" pos') subst + and set_label_mem lbl pos pos' subst = + StringMap.add (name_of_label lbl pos) + (CBuiltins.asm_mem_argument (sprintf "%%%d" pos')) + subst + and set_label_const lbl pos n subst = + StringMap.add (name_of_label lbl pos) (sprintf "%Ld" n) subst in + + (* Fix up the input expressions: + - add "&" for inputs of kind "m" + - evaluate constants for inputs of kind "i" *) + let rec fixupInputs accu pos pos' subst = function + | [] -> + (List.rev accu, subst) + | (lbl, cstr, e) :: inputs -> + match cstr with + | "r" | "rm" -> + fixupInputs (e :: accu) (pos + 1) (pos' + 1) + (set_label_reg lbl pos pos' subst) inputs + | "m" | "o" -> + fixupInputs (Cutil.eaddrof e :: accu) (pos + 1) (pos' + 1) + (set_label_mem lbl pos pos' subst) inputs + | "i" | "n" -> + let n = + match Ceval.integer_expr env e with + | Some n -> n + | None -> error "asm argument of kind 'i'/'n' is not a constant"; 0L in + fixupInputs accu (pos + 1) pos' + (set_label_const lbl pos n subst) inputs + | _ -> + unsupported ("asm argument of kind '" ^ cstr ^ "'"); + ([], subst) in + + (* Check the output expressions *) + let (output', ty_res, (inputs', subst)) = + match outputs with + | [] -> + (None, TVoid [], fixupInputs [] 0 0 StringMap.empty inputs) + | [(lbl, cstr, e)] -> + if not (cstr = "=r" || cstr = "=rm") then + unsupported ("asm result of kind '" ^ cstr ^ "'"); + (Some e, e.etyp, + fixupInputs [] 1 1 (set_label_reg lbl 0 0 StringMap.empty) inputs) + | _ -> + error "asm statement with 2 or more results"; + (None, TVoid [], ([], StringMap.empty)) in + + (* Check the clobber list *) + List.iter + (fun c -> + if not (c = "memory" || c = "cc") then + unsupported ("asm register clobber '" ^ c ^ "'")) + clobber; + + (* Rename the %[ident] and %nnn placeholders in the asm text *) + let txt' = + Str.global_substitute re_asm_placeholder + (fun txt -> let s = Str.matched_group 1 txt in + try StringMap.find s subst with Not_found -> s) + txt in + + (* Build the Ebuiltin expression *) + let e = + let tinputs = convertTypArgs env [] inputs' in + let toutput = convertTyp env ty_res in + Ebuiltin(EF_inline_asm(intern_string txt', + signature_of_type tinputs toutput cc_default), + tinputs, + convertExprList env inputs', + convertTyp env ty_res) in + + (* Add an assignment to the output, if any *) + match output' with + | None -> e + | Some lhs -> Eassign (convertLvalue env lhs, e, typeof e) + (* Separate the cases of a switch statement body *) type switchlabel = @@ -940,11 +1031,11 @@ let rec convertStmt ploc env s = unsupported "nested blocks"; Sskip | C.Sdecl _ -> unsupported "inner declarations"; Sskip - | C.Sasm txt -> + | C.Sasm(attrs, txt, outputs, inputs, clobber) -> if not !Clflags.option_finline_asm then unsupported "inline 'asm' statement (consider adding option -finline-asm)"; add_lineno ploc s.sloc - (Sdo (Ebuiltin (EF_inline_asm (intern_string txt), Tnil, Enil, Tvoid))) + (Sdo (convertAsm env txt outputs inputs clobber)) and convertSwitch ploc env is_64 = function | [] -> diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 7c00ab47..487c0df6 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -405,18 +405,18 @@ Hypothesis do_external_function_complete: do_external_function id sg ge w vargs m = Some(w', t, vres, m'). Variable do_inline_assembly: - ident -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). + ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). Hypothesis do_inline_assembly_sound: - forall txt ge vargs m t vres m' w w', - do_inline_assembly txt ge w vargs m = Some(w', t, vres, m') -> - inline_assembly_sem txt ge vargs m t vres m' /\ possible_trace w t w'. + forall txt sg ge vargs m t vres m' w w', + do_inline_assembly txt sg ge w vargs m = Some(w', t, vres, m') -> + inline_assembly_sem txt sg ge vargs m t vres m' /\ possible_trace w t w'. Hypothesis do_inline_assembly_complete: - forall txt ge vargs m t vres m' w w', - inline_assembly_sem txt ge vargs m t vres m' -> + forall txt sg ge vargs m t vres m' w w', + inline_assembly_sem txt sg ge vargs m t vres m' -> possible_trace w t w' -> - do_inline_assembly txt ge w vargs m = Some(w', t, vres, m'). + do_inline_assembly txt sg ge w vargs m = Some(w', t, vres, m'). Definition do_ef_volatile_load (chunk: memory_chunk) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := @@ -541,7 +541,7 @@ Definition do_external (ef: external_function): | EF_memcpy sz al => do_ef_memcpy sz al | EF_annot text targs => do_ef_annot text targs | EF_annot_val text targ => do_ef_annot_val text targ - | EF_inline_asm text => do_inline_assembly text ge + | EF_inline_asm text sg => do_inline_assembly text sg ge end. Lemma do_ef_external_sound: -- cgit