diff options
-rw-r--r-- | .depend | 14 | ||||
-rw-r--r-- | arm/TargetPrinter.ml | 2 | ||||
-rw-r--r-- | backend/CSE.v | 2 | ||||
-rw-r--r-- | backend/Regalloc.ml | 18 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 95 | ||||
-rw-r--r-- | cfrontend/Cexec.v | 2 | ||||
-rw-r--r-- | common/AST.v | 7 | ||||
-rw-r--r-- | common/Events.v | 2 | ||||
-rw-r--r-- | common/PrintAST.ml | 2 | ||||
-rw-r--r-- | cparser/ExtendedAsm.ml | 183 | ||||
-rw-r--r-- | ia32/Machregsaux.ml | 4 | ||||
-rw-r--r-- | ia32/TargetPrinter.ml | 2 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 2 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 2 | ||||
-rw-r--r-- | test/regression/extasm.c | 70 |
15 files changed, 306 insertions, 101 deletions
@@ -36,7 +36,7 @@ $(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH) backend/SelectDiv.vo backend/SelectDiv.glob backend/SelectDiv.v.beautified: backend/SelectDiv.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectLong.vo backend/SelectLong.glob backend/SelectLong.v.beautified: backend/SelectLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo common/Errors.vo common/Globalenvs.vo backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Globalenvs.vo common/Switch.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo -$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo +$(ARCH)/SelectOpproof.vo $(ARCH)/SelectOpproof.glob $(ARCH)/SelectOpproof.v.beautified: $(ARCH)/SelectOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDivproof.vo backend/SelectDivproof.glob backend/SelectDivproof.v.beautified: backend/SelectDivproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectDiv.vo backend/SelectLongproof.vo backend/SelectLongproof.glob backend/SelectLongproof.v.beautified: backend/SelectLongproof.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SelectLong.vo backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/SelectDiv.vo backend/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectDivproof.vo backend/SelectLongproof.vo @@ -60,12 +60,12 @@ $(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH) backend/ValueAnalysis.vo backend/ValueAnalysis.glob backend/ValueAnalysis.v.beautified: backend/ValueAnalysis.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Kildall.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/Liveness.vo lib/Axioms.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob $(ARCH)/ConstpropOp.v.beautified: $(ARCH)/ConstpropOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/ValueDomain.vo backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/Liveness.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo -$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo +$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob $(ARCH)/ConstpropOpproof.v.beautified: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo driver/Compopts.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ConstpropOp.vo backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo driver/Compopts.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo backend/CSEdomain.vo backend/CSEdomain.glob backend/CSEdomain.v.beautified: backend/CSEdomain.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOp.glob $(ARCH)/CombineOp.v.beautified: $(ARCH)/CombineOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/CSEdomain.vo backend/CSE.vo backend/CSE.glob backend/CSE.v.beautified: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/CSEdomain.vo backend/Kildall.vo $(ARCH)/CombineOp.vo -$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo +$(ARCH)/CombineOpproof.vo $(ARCH)/CombineOpproof.glob $(ARCH)/CombineOpproof.v.beautified: $(ARCH)/CombineOpproof.v lib/Coqlib.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo backend/RTL.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo backend/CSEproof.vo backend/CSEproof.glob backend/CSEproof.v.beautified: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo backend/NeedDomain.vo backend/NeedDomain.glob backend/NeedDomain.v.beautified: backend/NeedDomain.v lib/Coqlib.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo lib/Lattice.vo backend/Registers.vo backend/ValueDomain.vo $(ARCH)/Op.vo backend/RTL.vo $(ARCH)/NeedOp.vo $(ARCH)/NeedOp.glob $(ARCH)/NeedOp.v.beautified: $(ARCH)/NeedOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/NeedDomain.vo backend/RTL.vo @@ -73,7 +73,7 @@ backend/Deadcode.vo backend/Deadcode.glob backend/Deadcode.v.beautified: backend backend/Deadcodeproof.vo backend/Deadcodeproof.glob backend/Deadcodeproof.v.beautified: backend/Deadcodeproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/IntvSets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcode.vo backend/Unusedglob.vo backend/Unusedglob.glob backend/Unusedglob.v.beautified: backend/Unusedglob.v lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo lib/Iteration.vo common/AST.vo common/Errors.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Unusedglobproof.vo backend/Unusedglobproof.glob backend/Unusedglobproof.v.beautified: backend/Unusedglobproof.v lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo lib/Iteration.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Unusedglob.vo -$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo +$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Locations.glob backend/Locations.v.beautified: backend/Locations.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo $(ARCH)/Conventions1.vo $(ARCH)/Conventions1.glob $(ARCH)/Conventions1.v.beautified: $(ARCH)/Conventions1.v lib/Coqlib.vo common/AST.vo common/Events.vo backend/Locations.vo backend/Conventions.vo backend/Conventions.glob backend/Conventions.v.beautified: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/Conventions1.vo @@ -94,10 +94,10 @@ $(ARCH)/Stacklayout.vo $(ARCH)/Stacklayout.glob $(ARCH)/Stacklayout.v.beautified backend/Stacking.vo backend/Stacking.glob backend/Stacking.v.beautified: backend/Stacking.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo backend/Lineartyping.vo backend/Stackingproof.vo backend/Stackingproof.glob backend/Stackingproof.v.beautified: backend/Stackingproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo common/Values.vo $(ARCH)/Op.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo backend/Stacking.vo $(ARCH)/Asm.vo $(ARCH)/Asm.glob $(ARCH)/Asm.v.beautified: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/Stacklayout.vo backend/Conventions.vo -$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo +$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob $(ARCH)/Asmgen.v.beautified: $(ARCH)/Asmgen.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo backend/Asmgenproof0.vo backend/Asmgenproof0.glob backend/Asmgenproof0.v.beautified: backend/Asmgenproof0.v lib/Coqlib.vo lib/Intv.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo -$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo backend/Asmgenproof0.vo -$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo +$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob $(ARCH)/Asmgenproof1.v.beautified: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo backend/Conventions.vo +$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo $(ARCH)/Asmgenproof1.vo cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo $(ARCH)/Archi.vo cfrontend/Cop.vo cfrontend/Cop.glob cfrontend/Cop.v.beautified: cfrontend/Cop.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Errors.vo cfrontend/Ctypes.vo cfrontend/Cop.vo diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 913bff9e..85e3f919 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -1003,7 +1003,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (Int32.to_int (camlint_of_coqint al)) args | EF_annot_val(txt, targ) -> print_annot_val oc (extern_atom txt) args res - | EF_inline_asm(txt, sg) -> + | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n" comment; PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; fprintf oc "%s end inline assembly\n" comment; diff --git a/backend/CSE.v b/backend/CSE.v index 9f295402..e9006d4f 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/Regalloc.ml b/backend/Regalloc.ml index 3a7f5d99..c286e946 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -510,6 +510,9 @@ let add_interfs_live g live v = let add_interfs_list g v vl = List.iter (IRC.add_interf g v) vl +let add_interfs_list_mreg g vl mr = + List.iter (fun v -> IRC.add_interf g v (L (R mr))) vl + let rec add_interfs_pairwise g = function | [] -> () | v1 :: vl -> add_interfs_list g v1 vl; add_interfs_pairwise g vl @@ -578,7 +581,20 @@ let add_interfs_instr g instr live = add_interfs_pairwise g res; add_interfs_destroyed g across (destroyed_by_builtin ef); begin match ef, args, res with - | EF_annot_val _, [arg], [res] -> IRC.add_pref g arg res (* like a move *) + | EF_annot_val _, [arg], [res] -> + (* like a move *) + IRC.add_pref g arg res + | EF_inline_asm(txt, sg, clob), _, _ -> + (* clobbered regs interfere with live set + and also with res and args for GCC compatibility *) + List.iter (fun c -> + match Machregsaux.register_by_name (extern_atom c) with + | None -> () + | Some mr -> + add_interfs_destroyed g across [mr]; + add_interfs_list_mreg g args mr; + if sg.sig_res <> None then add_interfs_list_mreg g res mr) + clob | _ -> () end | Xannot(ef, args) -> diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 7413c443..44d16502 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -831,92 +831,25 @@ 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 - +(* Extended assembly *) + +let convertAsm loc env txt outputs inputs clobber = + let (txt', output', inputs') = + ExtendedAsm.transf_asm loc env txt outputs inputs clobber in + let clobber' = + List.map intern_string clobber in + let ty_res = + match output' with None -> TVoid [] | Some e -> e.etyp 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), + signature_of_type tinputs toutput cc_default, + clobber'), tinputs, convertExprList env inputs', convertTyp env ty_res) in - (* Add an assignment to the output, if any *) match output' with | None -> e @@ -982,7 +915,9 @@ let rec convertStmt ploc env s = | C.Sdo e -> add_lineno ploc s.sloc (swrap (Ctyping.sdo (convertExpr env e))) | C.Sseq(s1, s2) -> - Ssequence(convertStmt ploc env s1, convertStmt s1.sloc env s2) + let s1' = convertStmt ploc env s1 in + let s2' = convertStmt s1.sloc env s2 in + Ssequence(s1', s2') | C.Sif(e, s1, s2) -> let te = convertExpr env e in add_lineno ploc s.sloc @@ -1035,7 +970,7 @@ let rec convertStmt ploc env s = if not !Clflags.option_finline_asm then unsupported "inline 'asm' statement (consider adding option -finline-asm)"; add_lineno ploc s.sloc - (Sdo (convertAsm env txt outputs inputs clobber)) + (Sdo (convertAsm s.sloc env txt outputs inputs clobber)) and convertSwitch ploc env is_64 = function | [] -> diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 487c0df6..aba3c094 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -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 sg => do_inline_assembly text sg ge + | EF_inline_asm text sg clob => do_inline_assembly text sg ge end. Lemma do_ef_external_sound: diff --git a/common/AST.v b/common/AST.v index 1e1e2b9d..2550844b 100644 --- a/common/AST.v +++ b/common/AST.v @@ -584,7 +584,7 @@ Inductive external_function : Type := (** Another form of annotation that takes one argument, produces an event carrying the text and the value of this argument, and returns the value of the argument. *) - | EF_inline_asm (text: ident) (sg: signature). + | EF_inline_asm (text: ident) (sg: signature) (clobbers: list ident). (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic @@ -606,7 +606,7 @@ Definition ef_sig (ef: external_function): signature := | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default | EF_annot text targs => mksignature targs None cc_default | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default - | EF_inline_asm text sg => sg + | EF_inline_asm text sg clob => sg end. (** Whether an external function should be inlined by the compiler. *) @@ -624,7 +624,7 @@ Definition ef_inline (ef: external_function) : bool := | EF_memcpy sz al => true | EF_annot text targs => true | EF_annot_val text targ => true - | EF_inline_asm text targs => true + | EF_inline_asm text sg clob => true end. (** Whether an external function must reload its arguments. *) @@ -642,6 +642,7 @@ Proof. generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros. decide equality. apply list_eq_dec. auto. + apply list_eq_dec. auto. Defined. Global Opaque external_function_eq. diff --git a/common/Events.v b/common/Events.v index 62765fd3..3bec15db 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1480,7 +1480,7 @@ Definition external_call (ef: external_function): extcall_sem := | EF_memcpy sz al => extcall_memcpy_sem sz al | EF_annot txt targs => extcall_annot_sem txt targs | EF_annot_val txt targ => extcall_annot_val_sem txt targ - | EF_inline_asm txt sg => inline_assembly_sem txt sg + | EF_inline_asm txt sg clb => inline_assembly_sem txt sg end. Theorem external_call_spec: diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 387bf261..76305d02 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -53,7 +53,7 @@ let name_of_external = function sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string al) | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text) | EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text) - | EF_inline_asm(text, sg) -> sprintf "inline_asm %S" (extern_atom text) + | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (extern_atom text) let rec print_annot_arg px oc = function | AA_base x -> px oc x diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml new file mode 100644 index 00000000..4cd5fc21 --- /dev/null +++ b/cparser/ExtendedAsm.ml @@ -0,0 +1,183 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Partial emulation of GCC's extended inline assembly (experimental). *) + +(* The [transf_asm] function in this module takes a full GCC-style + extended asm statement and puts it in the form supported by + CompCert, namely: + - 0 or 1 output of kind "r" + - 0, 1 or several inputs of kind "r". + Inputs and outputs of kind "m" (memory location) are emulated + by taking the address of the operand and treating it as + an input of kind "r". + Inputs of kind "i" and "n" (integer immediates) are evaluated + at compile-time and textually substituted in the asm template. + + Extended asm statements that do not fit the forms above are rejected + with diagnostics. *) + +open Printf +open Machine +open C +open Cutil +open Env +open Cerrors + +(* Renaming of labeled and numbered operands *) + +module StringMap = Map.Make(String) + +let name_of_label ?(modifier = "") lbl pos = + match lbl with + | None -> (* numbered argument *) + sprintf "%%%s%d" modifier pos + | Some l -> (* named argument *) + sprintf "%%%s[%s]" modifier l + +let set_label_reg lbl pos pos' subst = + StringMap.add (name_of_label lbl pos) (sprintf "%%%d" pos') subst + +(* These are the modifiers used by GCC for ARM: + %Rxxx is the most significant half of a register pair + %Qxxx is the least significant half of a register pair. + They are not documented, and it is unclear whether other GCC ports + have this feature and with which syntax. *) + +let set_label_regpair lbl pos pos' subst = + StringMap.add (name_of_label ~modifier:"R" lbl pos) (sprintf "%%%d" pos') + (StringMap.add (name_of_label ~modifier:"Q" lbl pos) + (sprintf "%%%d" (pos' + 1)) + subst) + +let set_label_mem lbl pos pos' subst = + StringMap.add (name_of_label lbl pos) + (CBuiltins.asm_mem_argument (sprintf "%%%d" pos')) + subst + +let set_label_const lbl pos n subst = + StringMap.add (name_of_label lbl pos) (sprintf "%Ld" n) subst + +(* Operands of 64-bit integer type get split into a pair of registers + on 32-bit platforms *) + +let is_reg_pair env ty = + match unroll env ty with + | TInt(ik, _) -> sizeof_ikind ik > !config.sizeof_ptr + | _ -> false + +(* Transform the input operands: + - add "&" for inputs of kind "m" + - evaluate constants for inputs of kind "i" *) + +let rec transf_inputs loc env accu pos pos' subst = function + | [] -> + (List.rev accu, subst) + | (lbl, cstr, e) :: inputs -> + match cstr with + | "r" -> + if is_reg_pair env e.etyp then + transf_inputs loc env (e :: accu) (pos + 1) (pos' + 2) + (set_label_regpair lbl pos pos' subst) inputs + else + transf_inputs loc env (e :: accu) (pos + 1) (pos' + 1) + (set_label_reg lbl pos pos' subst) inputs + | "m" -> + transf_inputs loc env (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 "%aError: asm argument of kind '%s' is not a constant" + formatloc loc cstr; + 0L in + transf_inputs loc env accu (pos + 1) pos' + (set_label_const lbl pos n subst) inputs + | _ -> + error "%aUnsupported feature: asm argument of kind '%s'" + formatloc loc cstr; + transf_inputs loc env (e :: accu) (pos + 1) (pos' + 1) + (set_label_reg lbl pos pos' subst) inputs + +(* Transform the output operands: + - outputs of kind "=m" become an input (equal to the address of the output) +*) + +let transf_outputs loc env = function + | [] -> + (None, [], StringMap.empty, 0, 0) + | [(lbl, cstr, e)] -> + if not (is_modifiable_lvalue env e) then + error "%aError: asm output is not a modifiable l-value" formatloc loc; + begin match cstr with + | "=r" -> + if is_reg_pair env e.etyp then + (Some e, [], set_label_regpair lbl 0 0 StringMap.empty, 1, 2) + else + (Some e, [], set_label_reg lbl 0 0 StringMap.empty, 1, 1) + | "=m" -> + (None, [eaddrof e], + set_label_mem lbl 0 0 StringMap.empty, 1, 1) + | _ -> + error "%aUnsupported feature: asm result of kind '%s'" + formatloc loc cstr; + (None, [], set_label_reg lbl 0 0 StringMap.empty, 1, 1) + end + | _ -> + error "%aUnsupported feature: asm statement with 2 or more outputs" + formatloc loc; + (None, [], StringMap.empty, 0, 0) + +(* Check the clobber list *) + +let check_clobbers loc clob = + List.iter + (fun c -> + if Machregsaux.register_by_name c <> None + || c = "memory" || c = "cc" + then () + else error "%aError: unrecognized asm register clobber '%s'" + formatloc loc c) + clob + +(* Renaming of the %nnn and %[ident] placeholders in the asm text *) + +let re_asm_placeholder = + Str.regexp "\\(%[QR]?\\([0-9]+\\|\\[[a-zA-Z_][a-zA-Z_0-9]*\\]\\)\\|%%\\)" + +let rename_placeholders loc template subst = + let rename p = + if p = "%%" then p else + try + StringMap.find p subst + with Not_found -> + error "%aError: '%s' in asm text does not designate any operand" + formatloc loc p; + "%<error>" + in + Str.global_substitute re_asm_placeholder + (fun txt -> rename (Str.matched_group 1 txt)) + template + +(* All together *) + +let transf_asm loc env template outputs inputs clobbers = + let (outputs', inputs1, subst1, pos, pos') = + transf_outputs loc env outputs in + let (inputs', subst) = + transf_inputs loc env inputs1 pos pos' subst1 inputs in + check_clobbers loc clobbers; + (rename_placeholders loc template subst, outputs', inputs') diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml index 8403746a..3083cf3e 100644 --- a/ia32/Machregsaux.ml +++ b/ia32/Machregsaux.ml @@ -15,8 +15,8 @@ open Machregs let register_names = [ - ("AX", AX); ("BX", BX); ("CX", CX); ("DX", DX); - ("SI", SI); ("DI", DI); ("BP", BP); + ("EAX", AX); ("EBX", BX); ("ECX", CX); ("EDX", DX); + ("ESI", SI); ("EDI", DI); ("EBP", BP); ("XMM0", X0); ("XMM1", X1); ("XMM2", X2); ("XMM3", X3); ("XMM4", X4); ("XMM5", X5); ("XMM6", X6); ("XMM7", X7); ("ST0", FP0) diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 7e9471a5..09411fee 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -871,7 +871,7 @@ module Target(System: SYSTEM):TARGET = (Int32.to_int (camlint_of_coqint al)) args | EF_annot_val(txt, targ) -> print_annot_val oc (extern_atom txt) args res - | EF_inline_asm(txt, sg) -> + | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n" comment; fprintf oc "\t"; PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index fbe5f782..aec8f66e 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -523,7 +523,7 @@ let expand_instruction instr = expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args | EF_annot_val(txt, targ) -> expand_annot_val txt targ args res - | EF_inline_asm(txt, sg) -> + | EF_inline_asm(txt, sg, clob) -> emit instr | _ -> assert false diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 49954998..99e2479d 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -650,7 +650,7 @@ module Target (System : SYSTEM):TARGET = fprintf oc "%a:\n" label (transl_label lbl) | Pbuiltin(ef, args, res) -> begin match ef with - | EF_inline_asm(txt, sg) -> + | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n" comment; fprintf oc "\t"; PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; diff --git a/test/regression/extasm.c b/test/regression/extasm.c new file mode 100644 index 00000000..a69b3e79 --- /dev/null +++ b/test/regression/extasm.c @@ -0,0 +1,70 @@ +/* Testing extended asm. + To run the test, compile with -S and grep "TEST" in the generated .s */ + +int clobbers(int x) +{ + int y; + asm("TEST0 out:%0 in:%1" : "=r"(y) : "r"(x) : "cc" +#if defined(__i386__) + , "eax", "edx", "ecx" +#elif defined(__arm__) + , "r0", "r1", "r2" +#elif defined(__PPC__) + , "r3", "r4", "r5" +#endif +); + return y; +} + +int main() +{ + int x; + void * y; + long long z; + double f; + char c[16]; + + /* No inputs, no outputs */ + asm("TEST1 %%"); + /* r inputs */ + asm("TEST2 in:%0" : : "r" (x)); + asm("TEST3 in:%0,%1" : : "r" (x), "r" (f)); + /* r output */ + asm("TEST4 out:%0" : "=r" (x)); + /* r inputs and outputs */ + asm("TEST5 out:%0 in:%1" : "=r" (f) : "r" (y)); + /* m inputs */ + asm("TEST6 in:%0" : : "m" (c[2])); + asm("TEST7 out:%0 in:%1,%2" : "=r"(x) : "m" (c[0]), "r" (y)); + /* m output */ + asm("TEST8 out:%0 in:%1" : "=m" (c[4]) : "r" (f)); + /* i input */ + asm("TEST9 in:%0,%1,%2" : : "r"(x), "i"(sizeof(x) + 2), "r"(y)); +#ifdef FAILURES + asm("FAIL1 in:%0" : : "i"(x)); +#endif + /* 64-bit output */ + asm("TEST10 out: high %R0,lo %Q0" : "=r" (z)); + /* 64-bit input */ + asm("TEST11 out:%0 in:%1,high %R2,lo %Q2,%3" + : "=r"(x) : "r"(y), "r"(z), "r"(f)); +#ifdef FAILURES + asm("FAIL2 out:%0" : "=r"(z)); + asm("FAIL3 in:%0" : : "r"(z)); +#endif + /* Named arguments */ + asm("TEST12 a:%[a] b:%[b] c:%[c]" : : [a]"i"(12), [b]"i"(34), [c]"i"(56)); + asm("TEST13 a:%[a] x:%[x]" : [x]"=r"(x) : [a]"i"(78)); + asm("TEST14 a:%[a] in2:%1 c:%[c]" : : [a]"i"(12), "i"(34), [c]"i"(56)); +#ifdef FAILURES + asm("FAIL4 a:%[a]" : "=r"(x) : [z]"i"(0)); +#endif + /* Various failures */ +#ifdef FAILURES + asm("FAIL5 out:%0,%1" : "=r"(x), "=r"(y)); + asm("FAIL6 in:%0" : : "g"(x)); + asm("FAIL7 out:%0" : "=r" (x+1)); +#endif + return 0; +} + |