diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-04-17 16:30:43 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-04-17 16:30:43 +0200 |
| commit | 1b5db339bb05f773a6a132be4c0b8cea54d50461 (patch) | |
| tree | 5c7c767bc107eca66fdf6795777821572c5ec5af /backend | |
| parent | 3d751c114fe4611a5b72e160127be09cf6c6cfec (diff) | |
| download | compcert-kvx-1b5db339bb05f773a6a132be4c0b8cea54d50461.tar.gz compcert-kvx-1b5db339bb05f773a6a132be4c0b8cea54d50461.zip | |
Experiment: support a subset of GCC's extended asm statements.
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CMparser.mly | 2 | ||||
| -rw-r--r-- | backend/CSE.v | 2 | ||||
| -rw-r--r-- | backend/PrintAnnot.ml | 24 |
3 files changed, 25 insertions, 3 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 69b70e72..bcfa4548 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -60,7 +60,7 @@ let mkef sg toks = if sg.sig_args = [] then raise Parsing.Parse_error; EF_annot_val(intern_string txt, List.hd sg.sig_args) | [EFT_tok "inline_asm"; EFT_string txt] -> - EF_inline_asm(intern_string txt) + EF_inline_asm(intern_string txt, sg) | _ -> raise Parsing.Parse_error diff --git a/backend/CSE.v b/backend/CSE.v index 2c0c5f33..9f295402 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -476,7 +476,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb empty_numbering | Ibuiltin ef args res s => match ef with - | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ => + | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ _ => empty_numbering | EF_builtin _ _ | EF_vstore _ | EF_vstore_global _ _ _ => set_unknown (kill_all_loads before) res diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml index 995f22dd..88f5d8d6 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -148,7 +148,29 @@ let print_annot_val print_preg oc txt args = print_annot_text print_preg "<internal error>" oc txt (List.map (fun r -> AA_base r) args) -(* Print CompCert version and command-line as asm comment *) +(** Inline assembly *) + +let re_asm_param = Str.regexp "%%\\|%[0-9]+" + +let print_inline_asm print_preg oc txt sg args res = + let operands = + if sg.sig_res = None then args else res @ args in + let print_fragment = function + | Str.Text s -> + output_string oc s + | Str.Delim "%%" -> + output_char oc '%' + | Str.Delim s -> + let n = int_of_string (String.sub s 1 (String.length s - 1)) in + try + print_preg oc (List.nth operands n) + with Failure _ -> + fprintf oc "<bad parameter %s>" s in + List.iter print_fragment (Str.full_split re_asm_param txt); + fprintf oc "\n" + + +(** Print CompCert version and command-line as asm comment *) let print_version_and_options oc comment = fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version; |