diff options
-rw-r--r-- | .depend | 18 | ||||
-rw-r--r-- | arm/CBuiltins.ml | 4 | ||||
-rw-r--r-- | arm/TargetPrinter.ml | 4 | ||||
-rw-r--r-- | backend/CMparser.mly | 2 | ||||
-rw-r--r-- | backend/CSE.v | 2 | ||||
-rw-r--r-- | backend/PrintAnnot.ml | 24 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 95 | ||||
-rw-r--r-- | cfrontend/Cexec.v | 16 | ||||
-rw-r--r-- | common/AST.v | 6 | ||||
-rw-r--r-- | common/Events.v | 8 | ||||
-rw-r--r-- | common/PrintAST.ml | 2 | ||||
-rw-r--r-- | cparser/C.mli | 6 | ||||
-rw-r--r-- | cparser/Cabs.v | 8 | ||||
-rw-r--r-- | cparser/Cabshelper.ml | 2 | ||||
-rw-r--r-- | cparser/Cprint.ml | 38 | ||||
-rw-r--r-- | cparser/Elab.ml | 35 | ||||
-rw-r--r-- | cparser/Parser.vy | 54 | ||||
-rw-r--r-- | cparser/Rename.ml | 8 | ||||
-rw-r--r-- | cparser/pre_parser.mly | 38 | ||||
-rw-r--r-- | driver/Interp.ml | 2 | ||||
-rw-r--r-- | ia32/CBuiltins.ml | 4 | ||||
-rw-r--r-- | ia32/TargetPrinter.ml | 5 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 2 | ||||
-rw-r--r-- | powerpc/CBuiltins.ml | 4 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 17 |
25 files changed, 341 insertions, 63 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 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 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 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 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 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 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 lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.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 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 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,12 +73,12 @@ 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 lib/Integers.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 $(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 backend/LTL.vo backend/LTL.glob backend/LTL.v.beautified: backend/LTL.v lib/Coqlib.vo lib/Maps.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/Locations.vo backend/Conventions.vo -backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo +backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Memdata.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v $(ARCH)/Archi.vo lib/Coqlib.vo lib/Ordered.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.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/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Allocation.vo backend/Tunneling.vo backend/Tunneling.glob backend/Tunneling.v.beautified: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo backend/LTL.vo backend/Tunnelingproof.vo backend/Tunnelingproof.glob backend/Tunnelingproof.v.beautified: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.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 common/Memdata.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 $(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/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 +$(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 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 @@ -107,7 +107,7 @@ cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob cfrontend/Cstrategy.v.beautified cfrontend/Cexec.vo cfrontend/Cexec.glob cfrontend/Cexec.v.beautified: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Initializers.vo cfrontend/Initializers.glob cfrontend/Initializers.v.beautified: cfrontend/Initializers.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob cfrontend/Initializersproof.v.beautified: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo -cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob cfrontend/SimplExpr.v.beautified: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo +cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob cfrontend/SimplExpr.v.beautified: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob cfrontend/SimplExprspec.v.beautified: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Memory.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob cfrontend/SimplExprproof.v.beautified: cfrontend/SimplExprproof.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/Smallstep.vo common/Globalenvs.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo cfrontend/Clight.vo cfrontend/Clight.glob cfrontend/Clight.v.beautified: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml index 17aa5115..00de4df7 100644 --- a/arm/CBuiltins.ml +++ b/arm/CBuiltins.ml @@ -55,3 +55,7 @@ let builtins = { let size_va_list = 4 let va_list_scalar = true + +(* Expand memory references inside extended asm statements. Used in C2C. *) + +let asm_mem_argument arg = Printf.sprintf "[%s, #0]" arg diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index df17e595..913bff9e 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -1003,9 +1003,9 @@ 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 -> + | EF_inline_asm(txt, sg) -> fprintf oc "%s begin inline assembly\n" comment; - fprintf oc " %s\n" (extern_atom txt); + PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; fprintf oc "%s end inline assembly\n" comment; 5 (* hoping this is an upper bound... *) | _ -> diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 69b70e72..bcfa4548 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -60,7 +60,7 @@ let mkef sg toks = if sg.sig_args = [] then raise Parsing.Parse_error; EF_annot_val(intern_string txt, List.hd sg.sig_args) | [EFT_tok "inline_asm"; EFT_string txt] -> - EF_inline_asm(intern_string txt) + EF_inline_asm(intern_string txt, sg) | _ -> raise Parsing.Parse_error diff --git a/backend/CSE.v b/backend/CSE.v index 2c0c5f33..9f295402 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/PrintAnnot.ml b/backend/PrintAnnot.ml index 995f22dd..88f5d8d6 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -148,7 +148,29 @@ 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) -(* Print CompCert version and command-line as asm comment *) +(** Inline assembly *) + +let re_asm_param = Str.regexp "%%\\|%[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 + 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 + try + print_preg oc (List.nth operands n) + with Failure _ -> + fprintf oc "<bad parameter %s>" s in + List.iter print_fragment (Str.full_split re_asm_param txt); + fprintf oc "\n" + + +(** Print CompCert version and command-line as asm comment *) let print_version_and_options oc comment = fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version; diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index fd10efb4..7413c443 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -831,6 +831,97 @@ 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 + + (* 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), + tinputs, + convertExprList env inputs', + convertTyp env ty_res) in + + (* Add an assignment to the output, if any *) + match output' with + | None -> e + | Some lhs -> Eassign (convertLvalue env lhs, e, typeof e) + (* Separate the cases of a switch statement body *) type switchlabel = @@ -940,11 +1031,11 @@ let rec convertStmt ploc env s = unsupported "nested blocks"; Sskip | C.Sdecl _ -> unsupported "inner declarations"; Sskip - | C.Sasm txt -> + | C.Sasm(attrs, txt, outputs, inputs, clobber) -> if not !Clflags.option_finline_asm then unsupported "inline 'asm' statement (consider adding option -finline-asm)"; add_lineno ploc s.sloc - (Sdo (Ebuiltin (EF_inline_asm (intern_string txt), Tnil, Enil, Tvoid))) + (Sdo (convertAsm env txt outputs inputs clobber)) and convertSwitch ploc env is_64 = function | [] -> diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 7c00ab47..487c0df6 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -405,18 +405,18 @@ Hypothesis do_external_function_complete: do_external_function id sg ge w vargs m = Some(w', t, vres, m'). Variable do_inline_assembly: - ident -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). + ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem). Hypothesis do_inline_assembly_sound: - forall txt ge vargs m t vres m' w w', - do_inline_assembly txt ge w vargs m = Some(w', t, vres, m') -> - inline_assembly_sem txt ge vargs m t vres m' /\ possible_trace w t w'. + forall txt sg ge vargs m t vres m' w w', + do_inline_assembly txt sg ge w vargs m = Some(w', t, vres, m') -> + inline_assembly_sem txt sg ge vargs m t vres m' /\ possible_trace w t w'. Hypothesis do_inline_assembly_complete: - forall txt ge vargs m t vres m' w w', - inline_assembly_sem txt ge vargs m t vres m' -> + forall txt sg ge vargs m t vres m' w w', + inline_assembly_sem txt sg ge vargs m t vres m' -> possible_trace w t w' -> - do_inline_assembly txt ge w vargs m = Some(w', t, vres, m'). + do_inline_assembly txt sg ge w vargs m = Some(w', t, vres, m'). Definition do_ef_volatile_load (chunk: memory_chunk) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := @@ -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 => do_inline_assembly text ge + | EF_inline_asm text sg => do_inline_assembly text sg ge end. Lemma do_ef_external_sound: diff --git a/common/AST.v b/common/AST.v index d2926178..1e1e2b9d 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). + | EF_inline_asm (text: ident) (sg: signature). (** 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 => mksignature nil None cc_default + | EF_inline_asm text sg => 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 => true + | EF_inline_asm text targs => true end. (** Whether an external function must reload its arguments. *) diff --git a/common/Events.v b/common/Events.v index 15bf4e12..62765fd3 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1449,10 +1449,10 @@ Axiom external_functions_properties: (** We treat inline assembly similarly. *) -Parameter inline_assembly_sem: ident -> extcall_sem. +Parameter inline_assembly_sem: ident -> signature -> extcall_sem. Axiom inline_assembly_properties: - forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default) nil. + forall id sg, extcall_properties (inline_assembly_sem id sg) sg nil. (** ** Combined semantics of external calls *) @@ -1479,8 +1479,8 @@ Definition external_call (ef: external_function): extcall_sem := | EF_free => extcall_free_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 => inline_assembly_sem txt + | EF_annot_val txt targ => extcall_annot_val_sem txt targ + | EF_inline_asm txt sg => inline_assembly_sem txt sg end. Theorem external_call_spec: diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 52aa963a..387bf261 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 -> sprintf "inline_asm %S" (extern_atom text) + | EF_inline_asm(text, sg) -> 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/C.mli b/cparser/C.mli index 71ab1d4d..72e1f787 100644 --- a/cparser/C.mli +++ b/cparser/C.mli @@ -190,6 +190,10 @@ and init = | Init_struct of ident * (field * init) list | Init_union of ident * field * init +(** GCC extended asm *) + +type asm_operand = string option * string * exp + (** Statements *) type stmt = { sdesc: stmt_desc; sloc: location } @@ -210,7 +214,7 @@ and stmt_desc = | Sreturn of exp option | Sblock of stmt list | Sdecl of decl - | Sasm of string + | Sasm of attributes * string * asm_operand list * asm_operand list * string list and slabel = | Slabel of string diff --git a/cparser/Cabs.v b/cparser/Cabs.v index 920f4603..6d9e95d5 100644 --- a/cparser/Cabs.v +++ b/cparser/Cabs.v @@ -180,6 +180,12 @@ Definition init_name_group := (list spec_elem * list init_name)%type. (* e.g.: int x, y; *) Definition name_group := (list spec_elem * list name)%type. +(* GCC extended asm *) +Inductive asm_operand := +| ASMOPERAND: option string -> bool -> list char_code -> expression -> asm_operand. + +Definition asm_flag := (bool * list char_code)%type. + (* ** Declaration definition (at toplevel) *) @@ -209,7 +215,7 @@ with statement := | DEFAULT : statement -> cabsloc -> statement | LABEL : string -> statement -> cabsloc -> statement | GOTO : string -> cabsloc -> statement - | ASM : bool -> list char_code -> cabsloc -> statement + | ASM : list cvspec -> bool -> list char_code -> list asm_operand -> list asm_operand -> list asm_flag -> cabsloc -> statement | DEFINITION : definition -> statement (*definition or declaration of a variable or type*) with for_clause := diff --git a/cparser/Cabshelper.ml b/cparser/Cabshelper.ml index 9d4a91f6..5e6a19d0 100644 --- a/cparser/Cabshelper.ml +++ b/cparser/Cabshelper.ml @@ -70,7 +70,7 @@ begin | LABEL(_,_,loc) -> loc | GOTO(_,loc) -> loc | DEFINITION d -> get_definitionloc d - | ASM(_,_,loc) -> loc + | ASM(_,_,_,_,_,_,loc) -> loc end let string_of_cabsloc l = diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index ee8002d4..4ceaa016 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -364,6 +364,27 @@ let full_decl pp (sto, id, ty, int) = end; fprintf pp ";@]" +let asm_operand pp (label, constr, e) = + begin match label with + | None -> () + | Some l -> fprintf pp "[%s] " l + end; + fprintf pp "%a (%a)" const (CStr constr) exp (0, e) + +let asm_operands pp = function + | [] -> () + | op1 :: ops -> + fprintf pp "@[<hov 0>%a" asm_operand op1; + List.iter (fun op -> fprintf pp ",@ %a" asm_operand op) ops; + fprintf pp "@]" + +let asm_flags pp = function + | [] -> () + | fl1 :: fls -> + fprintf pp "@[<hov 0>%a" const (CStr fl1); + List.iter (fun fl -> fprintf pp ",@ %a" const (CStr fl)) fls; + fprintf pp "@]" + exception Not_expr let rec exp_of_stmt s = @@ -429,8 +450,21 @@ let rec stmt pp s = fprintf pp "@[<v 2>{@ %a@;<0 -2>}@]" stmt_block s | Sdecl d -> full_decl pp d - | Sasm txt -> - fprintf pp "asm(%a);" const (CStr txt) + | Sasm(attrs, txt, [], [], []) -> + fprintf pp "asm%a(%a);" attributes attrs const (CStr txt) + | Sasm(attrs, txt, outputs, inputs, []) -> + fprintf pp "asm%a(@[<hov 0>%a@ :%a@ :%a@]);" + attributes attrs + const (CStr txt) + asm_operands outputs + asm_operands inputs + | Sasm(attrs, txt, outputs, inputs, flags) -> + fprintf pp "asm%a(@[<hov 0>%a@ :%a@ :%a@ : %a@]);" + attributes attrs + const (CStr txt) + asm_operands outputs + asm_operands inputs + asm_flags flags and slabel pp = function | Slabel s -> diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 612103a6..a1dd552b 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -270,6 +270,11 @@ let elab_constant loc = function | CONST_STRING(wide, s) -> elab_string_literal loc wide s +let elab_simple_string loc wide chars = + match elab_string_literal loc wide chars with + | CStr s -> s + | _ -> error loc "wide character string not allowed here"; "" + (** * Elaboration of type expressions, type specifiers, name declarations *) @@ -498,13 +503,16 @@ and elab_cvspec env = function | CV_RESTRICT -> [ARestrict] | CV_ATTR attr -> elab_attribute env attr +and elab_cvspecs env cv_specs = + List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) + (* Elaboration of a type declarator. C99 section 6.7.5. *) and elab_type_declarator loc env ty = function | Cabs.JUSTBASE -> (ty, env) | Cabs.ARRAY(d, cv_specs, sz) -> - let a = List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) in + let a = elab_cvspecs env cv_specs in let sz' = match sz with | None -> @@ -520,7 +528,7 @@ and elab_type_declarator loc env ty = function Some 1L in (* produces better error messages later *) elab_type_declarator loc env (TArray(ty, sz', a)) d | Cabs.PTR(cv_specs, d) -> - let a = List.fold_left add_attributes [] (List.map (elab_cvspec env) cv_specs) in + let a = elab_cvspecs env cv_specs in elab_type_declarator loc env (TPtr(ty, a)) d | Cabs.PROTO(d, (params, vararg)) -> begin match unroll env ty with @@ -1933,6 +1941,13 @@ and elab_definitions local env = function let (decl2, env2) = elab_definitions local env1 dl in (decl1 @ decl2, env2) +(* Extended asm *) + +let elab_asm_operand loc env (ASMOPERAND(label, wide, chars, e)) = + let s = elab_simple_string loc wide chars in + let e' = elab_expr loc env e in + (label, s, e') + (* Contexts for elaborating statements *) @@ -2118,14 +2133,14 @@ let rec elab_stmt env ctx s = { sdesc = Sskip; sloc = elab_loc loc } (* Traditional extensions *) - | ASM(wide, chars, loc) -> - begin match elab_string_literal loc wide chars with - | CStr s -> - { sdesc = Sasm s; sloc = elab_loc loc } - | _ -> - error loc "wide strings not supported in asm statement"; - sskip - end + | ASM(cv_specs, wide, chars, outputs, inputs, flags, loc) -> + let a = elab_cvspecs env cv_specs in + let s = elab_simple_string loc wide chars in + let outputs = List.map (elab_asm_operand loc env) outputs in + let inputs = List.map (elab_asm_operand loc env) inputs in + let flags = List.map (fun (w,c) -> elab_simple_string loc w c) flags in + { sdesc = Sasm(a, s, outputs, inputs, flags); + sloc = elab_loc loc } (* Unsupported *) | DEFINITION def -> diff --git a/cparser/Parser.vy b/cparser/Parser.vy index a058a8d1..7c0bfb55 100644 --- a/cparser/Parser.vy +++ b/cparser/Parser.vy @@ -97,6 +97,12 @@ Require Import List. %type<gcc_attribute_word> gcc_attribute_word %type<name * list string> old_function_declarator direct_old_function_declarator %type<list string (* Reverse order *)> identifier_list +%type<list asm_flag> asm_flags +%type<option string> asm_op_name +%type<asm_operand> asm_operand +%type<list asm_operand> asm_operands asm_operands_ne +%type<list asm_operand * list asm_operand * list asm_flag> asm_arguments +%type<list cvspec> asm_attributes %start<list definition> translation_unit_file %% @@ -820,10 +826,50 @@ jump_statement: (* Non-standard *) asm_statement: -| loc = ASM LPAREN template = STRING_LITERAL RPAREN SEMICOLON - { let '(wide, chars, _) := template in ASM wide chars loc } -| loc = ASM VOLATILE LPAREN template = STRING_LITERAL RPAREN SEMICOLON - { let '(wide, chars, _) := template in ASM wide chars loc } +| loc = ASM attr = asm_attributes LPAREN template = STRING_LITERAL args = asm_arguments RPAREN SEMICOLON + { let '(wide, chars, _) := template in + let '(outputs, inputs, flags) := args in + ASM attr wide chars outputs inputs flags loc } + +asm_attributes: +| /* empty */ + { [] } +| CONST attr = asm_attributes + { CV_CONST :: attr } +| VOLATILE attr = asm_attributes + { CV_VOLATILE :: attr } + +asm_arguments: +| /* empty */ + { ([], [], []) } +| COLON o = asm_operands + { (o, [], []) } +| COLON o = asm_operands COLON i = asm_operands + { (o, i, []) } +| COLON o = asm_operands COLON i = asm_operands COLON f = asm_flags + { (o, i, f) } + +asm_operands: +| /* empty */ { [] } +| ol = asm_operands_ne { rev' ol } + +asm_operands_ne: +| ol = asm_operands_ne COMMA o = asm_operand { o :: ol } +| o = asm_operand { [o] } + +asm_operand: +| n = asm_op_name cstr = STRING_LITERAL LPAREN e = expression RPAREN + { let '(wide, s, loc) := cstr in ASMOPERAND n wide s (fst e) } + +asm_op_name: +| /* empty */ { None } +| LBRACK n = OTHER_NAME RBRACK { Some (fst n) } + +asm_flags: +| f = STRING_LITERAL + { let '(wide, s, loc) := f in (wide, s) :: nil } +| f = STRING_LITERAL COMMA fl = asm_flags + { let '(wide, s, loc) := f in (wide, s) :: fl } (* 6.9 *) translation_unit_file: diff --git a/cparser/Rename.ml b/cparser/Rename.ml index 2b7ec2ca..0d533b56 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -150,6 +150,8 @@ let decl env (sto, id, ty, int) = match int with None -> None | Some i -> Some(init env' i)), env') +let asm_operand env (lbl, cstr, e) = (lbl, cstr, exp env e) + let rec stmt env s = { sdesc = stmt_desc env s.sdesc; sloc = s.sloc } @@ -170,7 +172,11 @@ and stmt_desc env = function | Sreturn a -> Sreturn (optexp env a) | Sblock sl -> let (sl', _) = mmap stmt_or_decl env sl in Sblock sl' | Sdecl d -> assert false - | Sasm txt -> Sasm txt + | Sasm(attr, txt, outputs, inputs, flags) -> + Sasm(attr, txt, + List.map (asm_operand env) outputs, + List.map (asm_operand env) inputs, + flags) and stmt_or_decl env s = match s.sdesc with diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly index ef356d3a..44a06f8a 100644 --- a/cparser/pre_parser.mly +++ b/cparser/pre_parser.mly @@ -616,7 +616,43 @@ jump_statement: {} asm_statement: -| ASM VOLATILE? LPAREN string_literals_list RPAREN SEMICOLON +| ASM asm_attributes LPAREN string_literals_list asm_arguments RPAREN SEMICOLON + {} + +asm_attributes: +| /* empty */ +| CONST asm_attributes +| VOLATILE asm_attributes + {} + +asm_arguments: +| /* empty */ +| COLON asm_operands +| COLON asm_operands COLON asm_operands +| COLON asm_operands COLON asm_operands COLON asm_flags + {} + +asm_operands: +| /* empty */ +| asm_operands_ne + {} + +asm_operands_ne: +| asm_operands_ne COMMA asm_operand +| asm_operand + {} + +asm_operand: +| asm_op_name string_literals_list LPAREN expression RPAREN + {} + +asm_op_name: +| /*empty*/ {} +| LBRACK i = general_identifier RBRACK { set_id_type i OtherId } + +asm_flags: +| string_literals_list +| string_literals_list COMMA asm_flags {} translation_unit_file: diff --git a/driver/Interp.ml b/driver/Interp.ml index 2725dbfe..b16d2cae 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -397,7 +397,7 @@ let do_external_function id sg ge w args m = | _ -> None -let do_inline_assembly txt ge w args m = None +let do_inline_assembly txt sg ge w args m = None (* Implementing external functions producing observable events *) diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml index 765f5b18..b1be612b 100644 --- a/ia32/CBuiltins.ml +++ b/ia32/CBuiltins.ml @@ -70,3 +70,7 @@ let builtins = { let size_va_list = 4 let va_list_scalar = true + +(* Expand memory references inside extended asm statements. Used in C2C. *) + +let asm_mem_argument arg = Printf.sprintf "0(%s)" arg diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 58b7aa37..7e9471a5 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -871,9 +871,10 @@ 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 -> + | EF_inline_asm(txt, sg) -> fprintf oc "%s begin inline assembly\n" comment; - fprintf oc " %s\n" (extern_atom txt); + fprintf oc "\t"; + PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 47895cb1..fbe5f782 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 -> + | EF_inline_asm(txt, sg) -> emit instr | _ -> assert false diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 8840d2c3..222a4d94 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -90,3 +90,7 @@ let builtins = { let size_va_list = 12 let va_list_scalar = false + +(* Expand memory references inside extended asm statements. Used in C2C. *) + +let asm_mem_argument arg = Printf.sprintf "0(%s)" arg diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index b3d228b3..49954998 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -284,10 +284,14 @@ module Target (System : SYSTEM):TARGET = let ireg_or_zero oc r = if r = GPR0 then output_string oc "0" else ireg oc r - (* [preg] is only used for printing annotations. - Use the full register names [rN] and [fN] to avoid - ambiguity with constants. *) let preg oc = function + | IR r -> ireg oc r + | FR r -> freg oc r + | _ -> assert false + + (* For printing annotations, use the full register names [rN] and [fN] + to avoid ambiguity with constants. *) + let preg_annot oc = function | IR r -> fprintf oc "r%s" (int_reg_name r) | FR r -> fprintf oc "f%s" (float_reg_name r) | _ -> assert false @@ -327,7 +331,7 @@ module Target (System : SYSTEM):TARGET = (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "R1" oc txt targs args + PrintAnnot.print_annot_stmt preg_annot "R1" oc txt targs args end (* Determine if the displacement of a conditional branch fits the short form *) @@ -646,9 +650,10 @@ 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 -> + | EF_inline_asm(txt, sg) -> fprintf oc "%s begin inline assembly\n" comment; - fprintf oc " %s\n" (extern_atom txt); + fprintf oc "\t"; + PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false |