From f0a5038b4e4220300637d3e9e918d9ec31623108 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 8 Oct 2015 15:33:47 +0200 Subject: Added versions of the tranform_* functions in AST to work with functions taking the ident as argument. This functions are currently not used inside the proven part but it is nice to have them already there, when they are used by some future pass. They also come equiped with the corresponding proofs. --- arm/Asmexpand.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/Asmexpand.ml') diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index d13015ff..da08bf7c 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -403,7 +403,7 @@ let expand_function fn = with Error s -> Errors.Error (Errors.msg (coqstring_of_camlstring s)) -let expand_fundef = function +let expand_fundef _ = function | Internal f -> begin match expand_function f with | Errors.OK tf -> Errors.OK (Internal tf) @@ -413,4 +413,4 @@ let expand_fundef = function Errors.OK (External ef) let expand_program (p: Asm.program) : Asm.program Errors.res = - AST.transform_partial_program expand_fundef p + AST.transform_partial_ident_program expand_fundef p -- cgit From 0ffd562ae1941e37471ac0c2b8f93bed1de26441 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 9 Oct 2015 11:06:24 +0200 Subject: Filled in the rest of the funciton needed for thte debug info under arm. The name_of_section function no returns the correct name for the debug sections, the prologue and epilogue directives are added and the labels for the live ranges are introduced in the Asmexpand pass. --- arm/Asmexpand.ml | 50 ++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 46 insertions(+), 4 deletions(-) (limited to 'arm/Asmexpand.ml') diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index da08bf7c..b5bbc664 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -395,17 +395,59 @@ let expand_instruction instr = | _ -> emit instr -let expand_function fn = +let int_reg_to_dwarf = function + | IR0 -> 0 | IR1 -> 1 | IR2 -> 2 | IR3 -> 3 + | IR4 -> 4 | IR5 -> 5 | IR6 -> 6 | IR7 -> 7 + | IR8 -> 8 | IR9 -> 9 | IR10 -> 10 | IR11 -> 11 + | IR12 -> 12 | IR13 -> 13 | IR14 -> 14 + +let float_reg_to_dwarf = function + | FR0 -> 64 | FR1 -> 65 | FR2 -> 66 | FR3 -> 67 + | FR4 -> 68 | FR5 -> 69 | FR6 -> 70 | FR7 -> 71 + | FR8 -> 72 | FR9 -> 73 | FR10 -> 74 | FR11 -> 75 + | FR12 -> 76 | FR13 -> 77 | FR14 -> 78 | FR15 -> 79 + +let preg_to_dwarf_int = function + | IR r -> int_reg_to_dwarf r + | FR r -> float_reg_to_dwarf r + | _ -> assert false + +let translate_annot annot = + let rec aux = function + | BA x -> Some (13,BA (preg_to_dwarf_int x)) + | BA_int _ + | BA_long _ + | BA_float _ + | BA_single _ + | BA_loadglobal _ + | BA_addrglobal _ + | BA_loadstack _ -> None + | BA_addrstack ofs -> Some (13,BA_addrstack ofs) + | BA_splitlong (hi,lo) -> + begin + match (aux hi,aux lo) with + | Some (_,hi) ,Some (_,lo) -> Some (13,BA_splitlong (hi,lo)) + | _,_ -> None + end in + (match annot with + | [] -> None + | a::_ -> aux a) + + +let expand_function id fn = try set_current_function fn; - List.iter expand_instruction fn.fn_code; + if !Clflags.option_g then + expand_debug id translate_annot expand_instruction fn.fn_code + else + List.iter expand_instruction fn.fn_code; Errors.OK (get_current_function ()) with Error s -> Errors.Error (Errors.msg (coqstring_of_camlstring s)) -let expand_fundef _ = function +let expand_fundef id = function | Internal f -> - begin match expand_function f with + begin match expand_function id f with | Errors.OK tf -> Errors.OK (Internal tf) | Errors.Error msg -> Errors.Error msg end -- cgit From b0c47e12f2bbff0905ad853b90169df16d87f6be Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 9 Oct 2015 16:36:16 +0200 Subject: Filled in missing functions for debug information on ia32. Like for arm and ppc the functions for section names and start and end addresses of compilation units are defined and the print_annot function is moved to Asmexpandaux.ml. --- arm/Asmexpand.ml | 25 ++----------------------- 1 file changed, 2 insertions(+), 23 deletions(-) (limited to 'arm/Asmexpand.ml') diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index b5bbc664..990f207d 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -407,38 +407,17 @@ let float_reg_to_dwarf = function | FR8 -> 72 | FR9 -> 73 | FR10 -> 74 | FR11 -> 75 | FR12 -> 76 | FR13 -> 77 | FR14 -> 78 | FR15 -> 79 -let preg_to_dwarf_int = function +let preg_to_dwarf = function | IR r -> int_reg_to_dwarf r | FR r -> float_reg_to_dwarf r | _ -> assert false -let translate_annot annot = - let rec aux = function - | BA x -> Some (13,BA (preg_to_dwarf_int x)) - | BA_int _ - | BA_long _ - | BA_float _ - | BA_single _ - | BA_loadglobal _ - | BA_addrglobal _ - | BA_loadstack _ -> None - | BA_addrstack ofs -> Some (13,BA_addrstack ofs) - | BA_splitlong (hi,lo) -> - begin - match (aux hi,aux lo) with - | Some (_,hi) ,Some (_,lo) -> Some (13,BA_splitlong (hi,lo)) - | _,_ -> None - end in - (match annot with - | [] -> None - | a::_ -> aux a) - let expand_function id fn = try set_current_function fn; if !Clflags.option_g then - expand_debug id translate_annot expand_instruction fn.fn_code + expand_debug id 13 preg_to_dwarf expand_instruction fn.fn_code else List.iter expand_instruction fn.fn_code; Errors.OK (get_current_function ()) -- cgit From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 11 Oct 2015 17:43:59 +0200 Subject: Use Coq strings instead of idents to name external and builtin functions. The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables. --- arm/Asmexpand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'arm/Asmexpand.ml') diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 990f207d..fad13c9f 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -377,7 +377,7 @@ let expand_instruction instr = | Pbuiltin (ef,args,res) -> begin match ef with | EF_builtin (name,sg) -> - expand_builtin_inline (extern_atom name) args res + expand_builtin_inline (camlstring_of_coqstring name) args res | EF_vload chunk -> expand_builtin_vload chunk args res | EF_vstore chunk -> -- cgit From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- arm/Asmexpand.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/Asmexpand.ml') diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index fad13c9f..2b19cbe8 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -106,7 +106,7 @@ let memcpy_small_arg sz arg tmp = assert false let expand_builtin_memcpy_small sz al src dst = - let (tsrc, tdst) = + let (tsrc, tdst) = if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in let (rsrc, osrc) = memcpy_small_arg sz src tsrc in let (rdst, odst) = memcpy_small_arg sz dst tdst in @@ -142,7 +142,7 @@ let memcpy_big_arg arg tmp = let expand_builtin_memcpy_big sz al src dst = assert (sz >= al); assert (sz mod al = 0); - let (s, d) = + let (s, d) = if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in memcpy_big_arg src s; memcpy_big_arg dst d; -- cgit