diff options
Diffstat (limited to 'backend/PrintAsmaux.ml')
-rw-r--r-- | backend/PrintAsmaux.ml | 86 |
1 files changed, 61 insertions, 25 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index efc8030f..324e7e66 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -138,9 +138,6 @@ let cfi_rel_offset = else (fun _ _ _ -> ()) -(* For handling of annotations *) -let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" - (* Basic printing functions *) let coqint oc n = fprintf oc "%ld" (camlint_of_coqint n) @@ -216,36 +213,35 @@ let print_file_line_d2 oc pref file line = | Some fb -> Printlines.copy oc pref fb line line end - -(** "True" annotations *) +(** Programmer-supplied annotations (__builtin_annot). *) let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" 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) -> + | BA x -> print_preg oc x + | BA_int n -> fprintf oc "%ld" (camlint_of_coqint n) + | BA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) + | BA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) + | BA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) + | BA_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 -> + | BA_addrstack ofs -> fprintf oc "(%s + %ld)" sp_reg_name (camlint_of_coqint ofs) - | AA_loadglobal(chunk, id, ofs) -> + | BA_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) -> + | BA_addrglobal(id, ofs) -> fprintf oc "(\"%s\" + %ld)" (extern_atom id) (camlint_of_coqint ofs) - | AA_longofwords(hi, lo) -> + | BA_splitlong(hi, lo) -> fprintf oc "(%a * 0x100000000 + %a)" (print_annot print_preg sp_reg_name) hi (print_annot print_preg sp_reg_name) lo @@ -265,32 +261,72 @@ let print_annot_text print_preg sp_reg_name oc txt args = List.iter print_fragment (Str.full_split re_annot_param txt); fprintf oc "\n" -let print_annot_stmt print_preg sp_reg_name oc txt tys args = - print_annot_text print_preg sp_reg_name oc txt args +(* Printing of [EF_debug] info. To be completed. *) -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) +let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" +let print_debug_info comment print_line print_preg sp_name oc kind txt args = + let print_debug_args oc args = + List.iter + (fun a -> fprintf oc " %a" (print_annot print_preg sp_name) a) + args in + match kind with + | 1 -> (* line number *) + if Str.string_match re_file_line txt 0 then + print_line oc (Str.matched_group 1 txt) + (int_of_string (Str.matched_group 2 txt)) + | 2 -> (* assignment to local variable, not useful *) + () + | 3 -> (* beginning of live range for local variable *) + fprintf oc "%s debug: start live range %s =%a\n" + comment txt print_debug_args args + | 4 -> (* end of live range for local variable *) + fprintf oc "%s debug: end live range %s\n" + comment txt + | 5 -> (* local variable preallocated in stack *) + fprintf oc "%s debug: %s resides at%a\n" + comment txt print_debug_args args + | _ -> + () + (** Inline assembly *) -let re_asm_param = Str.regexp "%%\\|%[0-9]+" +let print_asm_argument print_preg oc modifier = function + | BA r -> print_preg oc r + | BA_splitlong(BA hi, BA lo) -> + begin match modifier with + | "R" -> print_preg oc hi + | "Q" -> print_preg oc lo + | _ -> fprintf oc "%a:%a" print_preg hi print_preg lo + (* Probably not what was intended *) + end + | _ -> failwith "bad asm argument" + +let builtin_arg_of_res = function + | BR r -> BA r + | BR_splitlong(BR hi, BR lo) -> BA_splitlong(BA hi, BA lo) + | _ -> assert false + +let re_asm_param_1 = Str.regexp "%%\\|%[QR]?[0-9]+" +let re_asm_param_2 = Str.regexp "%\\([QR]?\\)\\([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 + if sg.sig_res = None then args else builtin_arg_of_res 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 + assert (Str.string_match re_asm_param_2 s 0); + let modifier = Str.matched_group 1 s + and number = int_of_string (Str.matched_group 2 s) in try - print_preg oc (List.nth operands n) + print_asm_argument print_preg oc modifier (List.nth operands number) with Failure _ -> fprintf oc "<bad parameter %s>" s in - List.iter print_fragment (Str.full_split re_asm_param txt); + List.iter print_fragment (Str.full_split re_asm_param_1 txt); fprintf oc "\n" |