aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend14
-rw-r--r--arm/TargetPrinter.ml2
-rw-r--r--backend/CSE.v2
-rw-r--r--backend/Regalloc.ml18
-rw-r--r--cfrontend/C2C.ml95
-rw-r--r--cfrontend/Cexec.v2
-rw-r--r--common/AST.v7
-rw-r--r--common/Events.v2
-rw-r--r--common/PrintAST.ml2
-rw-r--r--cparser/ExtendedAsm.ml183
-rw-r--r--ia32/Machregsaux.ml4
-rw-r--r--ia32/TargetPrinter.ml2
-rw-r--r--powerpc/Asmexpand.ml2
-rw-r--r--powerpc/TargetPrinter.ml2
-rw-r--r--test/regression/extasm.c70
15 files changed, 306 insertions, 101 deletions
diff --git a/.depend b/.depend
index 7f4bee68..394d99ec 100644
--- a/.depend
+++ b/.depend
@@ -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;
+}
+
generated by cgit (git 2.34.1) at 2024-06-02 14:54:01 +0000