diff options
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/debug/Asmgen.ml | 126 | ||||
| -rw-r--r-- | extraction/extraction.v | 22 |
2 files changed, 146 insertions, 2 deletions
diff --git a/extraction/debug/Asmgen.ml b/extraction/debug/Asmgen.ml new file mode 100644 index 00000000..e8dfde13 --- /dev/null +++ b/extraction/debug/Asmgen.ml @@ -0,0 +1,126 @@ +(* Replace transl_op by this wrapper to print the op *) + +let transl_op op args res0 k = + match op with + | Omove -> (Printf.eprintf "Omove\n"; thereal_transl_op op args res0 k) + | Ointconst _ -> (Printf.eprintf "Ointconst _\n"; thereal_transl_op op args res0 k) + | Olongconst _ -> (Printf.eprintf "Olongconst _\n"; thereal_transl_op op args res0 k) + | Ofloatconst _ -> (Printf.eprintf "Ofloatconst _\n"; thereal_transl_op op args res0 k) + | Osingleconst _ -> (Printf.eprintf "Osingleconst _\n"; thereal_transl_op op args res0 k) + | Oaddrsymbol _ -> (Printf.eprintf "Oaddrsymbol _ _\n"; thereal_transl_op op args res0 k) + | Oaddrstack _ -> (Printf.eprintf "Oaddrstack _\n"; thereal_transl_op op args res0 k) + | Ocast8signed -> (Printf.eprintf "Ocast8signed\n"; thereal_transl_op op args res0 k) + | Ocast16signed -> (Printf.eprintf "Ocast16signed\n"; thereal_transl_op op args res0 k) + | Oadd -> (Printf.eprintf "Oadd\n"; thereal_transl_op op args res0 k) + | Oaddimm _ -> (Printf.eprintf "Oaddimm _\n"; thereal_transl_op op args res0 k) + | Oneg -> (Printf.eprintf "Oneg\n"; thereal_transl_op op args res0 k) + | Osub -> (Printf.eprintf "Osub\n"; thereal_transl_op op args res0 k) + | Omul -> (Printf.eprintf "Omul\n"; thereal_transl_op op args res0 k) + | Omulhs -> (Printf.eprintf "Omulhs\n"; thereal_transl_op op args res0 k) + | Omulhu -> (Printf.eprintf "Omulhu\n"; thereal_transl_op op args res0 k) + | Odiv -> (Printf.eprintf "Odiv\n"; thereal_transl_op op args res0 k) + | Odivu -> (Printf.eprintf "Odivu\n"; thereal_transl_op op args res0 k) + | Omod -> (Printf.eprintf "Omod\n"; thereal_transl_op op args res0 k) + | Omodu -> (Printf.eprintf "Omodu\n"; thereal_transl_op op args res0 k) + | Oand -> (Printf.eprintf "Oand\n"; thereal_transl_op op args res0 k) + | Oandimm _ -> (Printf.eprintf "Oandimm _\n"; thereal_transl_op op args res0 k) + | Oor -> (Printf.eprintf "Oor\n"; thereal_transl_op op args res0 k) + | Oorimm _ -> (Printf.eprintf "Oorimm _\n"; thereal_transl_op op args res0 k) + | Oxor -> (Printf.eprintf "Oxor\n"; thereal_transl_op op args res0 k) + | Oxorimm _ -> (Printf.eprintf "Oxorimm _\n"; thereal_transl_op op args res0 k) + | Oshl -> (Printf.eprintf "Oshl\n"; thereal_transl_op op args res0 k) + | Oshlimm _ -> (Printf.eprintf "Oshlimm _\n"; thereal_transl_op op args res0 k) + | Oshr -> (Printf.eprintf "Oshr\n"; thereal_transl_op op args res0 k) + | Oshrimm _ -> (Printf.eprintf "Oshrimm _\n"; thereal_transl_op op args res0 k) + | Oshruimm _ -> (Printf.eprintf "Oshruimm _\n"; thereal_transl_op op args res0 k) + | Oshrximm _ -> (Printf.eprintf "Oshrximm _\n"; thereal_transl_op op args res0 k) + | Olowlong -> (Printf.eprintf "Olowlong\n"; thereal_transl_op op args res0 k) + | Ocast32signed -> (Printf.eprintf "Ocast32signed\n"; thereal_transl_op op args res0 k) + | Ocast32unsigned -> (Printf.eprintf "Ocast32unsigned\n"; thereal_transl_op op args res0 k) + | Oaddl -> (Printf.eprintf "Oaddl\n"; thereal_transl_op op args res0 k) + | Oaddlimm _ -> (Printf.eprintf "Oaddlimm _\n"; thereal_transl_op op args res0 k) + | Onegl -> (Printf.eprintf "Onegl\n"; thereal_transl_op op args res0 k) + | Osubl -> (Printf.eprintf "Osubl\n"; thereal_transl_op op args res0 k) + | Omull -> (Printf.eprintf "Omull\n"; thereal_transl_op op args res0 k) + | Omullhs -> (Printf.eprintf "Omullhs\n"; thereal_transl_op op args res0 k) + | Omullhu -> (Printf.eprintf "Omullhu\n"; thereal_transl_op op args res0 k) + | Odivl -> (Printf.eprintf "Odivl\n"; thereal_transl_op op args res0 k) + | Odivlu -> (Printf.eprintf "Odivlu\n"; thereal_transl_op op args res0 k) + | Omodl -> (Printf.eprintf "Omodl\n"; thereal_transl_op op args res0 k) + | Omodlu -> (Printf.eprintf "Omodlu\n"; thereal_transl_op op args res0 k) + | Oandl -> (Printf.eprintf "Oandl\n"; thereal_transl_op op args res0 k) + | Oandlimm _ -> (Printf.eprintf "Oandlimm _\n"; thereal_transl_op op args res0 k) + | Oorl -> (Printf.eprintf "Oorl\n"; thereal_transl_op op args res0 k) + | Oorlimm _ -> (Printf.eprintf "Oorlimm _\n"; thereal_transl_op op args res0 k) + | Oxorl -> (Printf.eprintf "Oxorl\n"; thereal_transl_op op args res0 k) + | Oxorlimm _ -> (Printf.eprintf "Oxorlimm _\n"; thereal_transl_op op args res0 k) + | Oshll -> (Printf.eprintf "Oshll\n"; thereal_transl_op op args res0 k) + | Oshllimm _ -> (Printf.eprintf "Oshllimm _\n"; thereal_transl_op op args res0 k) + | Oshrlu -> (Printf.eprintf "Oshrlu\n"; thereal_transl_op op args res0 k) + | Oshrluimm _ -> (Printf.eprintf "Oshrluimm\n"; thereal_transl_op op args res0 k) + | Oshrxlimm _ -> (Printf.eprintf "Oshrxlimm\n"; thereal_transl_op op args res0 k) + | Onegf -> (Printf.eprintf "Onegf\n"; thereal_transl_op op args res0 k) + | Oabsf -> (Printf.eprintf "Oabsf\n"; thereal_transl_op op args res0 k) + | Oaddf -> (Printf.eprintf "Oaddf\n"; thereal_transl_op op args res0 k) + | Osubf -> (Printf.eprintf "Osubf\n"; thereal_transl_op op args res0 k) + | Omulf -> (Printf.eprintf "Omulf\n"; thereal_transl_op op args res0 k) + | Odivf -> (Printf.eprintf "Odivf\n"; thereal_transl_op op args res0 k) + | Onegfs -> (Printf.eprintf "Onegfs\n"; thereal_transl_op op args res0 k) + | Oabsfs -> (Printf.eprintf "Oabsfs\n"; thereal_transl_op op args res0 k) + | Oaddfs -> (Printf.eprintf "Oaddfs\n"; thereal_transl_op op args res0 k) + | Osubfs -> (Printf.eprintf "Osubfs\n"; thereal_transl_op op args res0 k) + | Omulfs -> (Printf.eprintf "Omulfs\n"; thereal_transl_op op args res0 k) + | Odivfs -> (Printf.eprintf "Odivfs\n"; thereal_transl_op op args res0 k) + | Osingleoffloat -> (Printf.eprintf "Osingleoffloat\n"; thereal_transl_op op args res0 k) + | Ofloatofsingle -> (Printf.eprintf "Ofloatofsingle\n"; thereal_transl_op op args res0 k) + | Ointoffloat -> (Printf.eprintf "Ointoffloat\n"; thereal_transl_op op args res0 k) + | Ointuoffloat -> (Printf.eprintf "Ointuoffloat\n"; thereal_transl_op op args res0 k) + | Ofloatofint -> (Printf.eprintf "Ofloatofint\n"; thereal_transl_op op args res0 k) + | Ofloatofintu -> (Printf.eprintf "Ofloatofintu\n"; thereal_transl_op op args res0 k) + | Ointofsingle -> (Printf.eprintf "Ointofsingle\n"; thereal_transl_op op args res0 k) + | Ointuofsingle -> (Printf.eprintf "Ointuofsingle\n"; thereal_transl_op op args res0 k) + | Osingleofint -> (Printf.eprintf "Osingleofint\n"; thereal_transl_op op args res0 k) + | Osingleofintu -> (Printf.eprintf "Osingleofintu\n"; thereal_transl_op op args res0 k) + | Olongoffloat -> (Printf.eprintf "Olongoffloat\n"; thereal_transl_op op args res0 k) + | Olonguoffloat -> (Printf.eprintf "Olonguoffloat\n"; thereal_transl_op op args res0 k) + | Ofloatoflong -> (Printf.eprintf "Ofloatoflong\n"; thereal_transl_op op args res0 k) + | Ofloatoflongu -> (Printf.eprintf "Ofloatoflongu\n"; thereal_transl_op op args res0 k) + | Olongofsingle -> (Printf.eprintf "Olongofsingle\n"; thereal_transl_op op args res0 k) + | Olonguofsingle -> (Printf.eprintf "Olonguofsingle\n"; thereal_transl_op op args res0 k) + | Osingleoflong -> (Printf.eprintf "Osingleoflong\n"; thereal_transl_op op args res0 k) + | Osingleoflongu -> (Printf.eprintf "Osingleoflongu\n"; thereal_transl_op op args res0 k) + | Ocmp _ -> (Printf.eprintf "Ocmp _\n"; thereal_transl_op op args res0 k) + | _ -> (Printf.eprintf "_\n"; thereal_transl_op op args res0 k) + +let transl_instr f i x k = + match i with + | Mgetstack _ -> (Printf.eprintf "Mgetstack\n"; thereal_transl_instr f i x k) + | Msetstack _ -> (Printf.eprintf "Msetstack\n"; thereal_transl_instr f i x k) + | Mgetparam _ -> (Printf.eprintf "Mgetparam\n"; thereal_transl_instr f i x k) + | Mop _ -> (Printf.eprintf "Mop\n"; thereal_transl_instr f i x k) + | Mload _ -> (Printf.eprintf "Mload\n"; thereal_transl_instr f i x k) + | Mstore _ -> (Printf.eprintf "Mstore\n"; thereal_transl_instr f i x k) + | Mcall _ -> (Printf.eprintf "Mcall\n"; thereal_transl_instr f i x k) + | Mtailcall _ -> (Printf.eprintf "Mtailcall\n"; thereal_transl_instr f i x k) + | Mbuiltin _ -> (Printf.eprintf "Mbuiltin\n"; thereal_transl_instr f i x k) + | Mlabel _ -> (Printf.eprintf "Mlabel\n"; thereal_transl_instr f i x k) + | Mgoto _ -> (Printf.eprintf "Mgoto\n"; thereal_transl_instr f i x k) + | Mcond _ -> (Printf.eprintf "Mcond\n"; thereal_transl_instr f i x k) + | Mjumptable _ -> (Printf.eprintf "Mjumptable\n"; thereal_transl_instr f i x k) + | Mreturn -> (Printf.eprintf "Mreturn\n"; thereal_transl_instr f i x k) + +let transl_cbranch c a l k = + match c, a with + | Ccomp _, _ :: _ :: [] -> (Printf.eprintf "Ccomp\n"; thereal_transl_cbranch c a l k) + | Ccompu _, _ :: _ :: [] -> (Printf.eprintf "Ccompu\n"; thereal_transl_cbranch c a l k) + | Ccompimm (_, _), _ :: [] -> (Printf.eprintf "Ccompimm\n"; thereal_transl_cbranch c a l k) + | Ccompuimm (_, _), _ :: [] -> (Printf.eprintf "Ccompuimm\n"; thereal_transl_cbranch c a l k) + | Ccompl _, _ :: _ :: [] -> (Printf.eprintf "Ccompl\n"; thereal_transl_cbranch c a l k) + | Ccomplu _, _ :: _ :: [] -> (Printf.eprintf "Ccomplu\n"; thereal_transl_cbranch c a l k) + | Ccomplimm (_, _), _ :: [] -> (Printf.eprintf "Ccomplimm\n"; thereal_transl_cbranch c a l k) + | Ccompluimm (_, _), _ :: [] -> (Printf.eprintf "Ccompulimm\n"; thereal_transl_cbranch c a l k) + | Ccompf _, _ :: _ :: [] -> (Printf.eprintf "Ccompf\n"; thereal_transl_cbranch c a l k) + | Cnotcompf _, _ :: _ :: [] -> (Printf.eprintf "Cnotcompf\n"; thereal_transl_cbranch c a l k) + | Ccompfs _, _ :: _ :: [] -> (Printf.eprintf "Ccomps\n"; thereal_transl_cbranch c a l k) + | Cnotcompfs _, _ :: _ :: [] -> (Printf.eprintf "Cnotcomps\n"; thereal_transl_cbranch c a l k) + | _ -> (Printf.eprintf "OOPS\n"; thereal_transl_cbranch c a l k) diff --git a/extraction/extraction.v b/extraction/extraction.v index 521c0cdd..5a1ca0be 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -34,6 +34,11 @@ Require Clight. Require Compiler. Require Parser. Require Initializers. +<<<<<<< HEAD +Require Int31. +Require Asmaux. +======= +>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf (* Standard lib *) Require Import ExtrOcamlBasic. @@ -110,10 +115,22 @@ Extract Constant Compopts.optim_CSE => "fun _ -> !Clflags.option_fcse". Extract Constant Compopts.optim_redundancy => "fun _ -> !Clflags.option_fredundancy". +Extract Constant Compopts.optim_postpass => + "fun _ -> !Clflags.option_fpostpass". Extract Constant Compopts.thumb => "fun _ -> !Clflags.option_mthumb". Extract Constant Compopts.debug => "fun _ -> !Clflags.option_g". +Extract Constant Compopts.optim_globaladdrtmp => + "fun _ -> !Clflags.option_fglobaladdrtmp". +Extract Constant Compopts.optim_globaladdroffset => + "fun _ -> !Clflags.option_fglobaladdroffset". +Extract Constant Compopts.optim_xsaddr => + "fun _ -> !Clflags.option_fxsaddr". +Extract Constant Compopts.optim_addx => + "fun _ -> !Clflags.option_faddx". +Extract Constant Compopts.optim_coalesce_mem => + "fun _ -> !Clflags.option_fcoalesce_mem". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". @@ -176,7 +193,8 @@ Separate Extraction Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg Machregs.destroyed_at_indirect_call - AST.signature_main + AST.signature_main Asmaux Floats.Float32.from_parsed Floats.Float.from_parsed Globalenvs.Senv.invert_symbol - Parser.translation_unit_file. + Parser.translation_unit_file + Compopts.optim_postpass. |