diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-03-12 14:41:07 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-03-12 14:41:07 +0000 |
| commit | 8fb2eba8404a1355d8867e0cfa0028ea941fcdaf (patch) | |
| tree | eb411ce6e7dfd0eb26b5d020549a6f07ac708ab2 | |
| parent | b683a90f06fd10e0b0defc176a15b7272564ffd9 (diff) | |
Initializers for global variables: compile-time evaluation of expressions done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
| -rw-r--r-- | .depend | 206 | ||||
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 79 | ||||
| -rw-r--r-- | cfrontend/Csem.v | 2 | ||||
| -rw-r--r-- | cfrontend/Initializers.v | 173 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 555 | ||||
| -rw-r--r-- | driver/Compiler.v | 5 | ||||
| -rw-r--r-- | extraction/extraction.v | 2 | ||||
| -rw-r--r-- | test/regression/Results/initializers | bin | 306 -> 404 bytes | |||
| -rw-r--r-- | test/regression/init3.c | 5 | ||||
| -rw-r--r-- | test/regression/initializers.c | 22 |
11 files changed, 891 insertions, 159 deletions
@@ -1,102 +1,104 @@ -lib/Axioms.vo: lib/Axioms.v -lib/Coqlib.vo: lib/Coqlib.v -lib/Intv.vo: lib/Intv.v lib/Coqlib.vo -lib/Maps.vo: lib/Maps.v lib/Coqlib.vo -lib/Heaps.vo: lib/Heaps.v lib/Coqlib.vo lib/Ordered.vo -lib/Lattice.vo: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo -lib/Ordered.vo: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo -lib/Iteration.vo: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo -lib/Integers.vo: lib/Integers.v lib/Axioms.vo lib/Coqlib.vo -lib/Floats.vo: lib/Floats.v lib/Coqlib.vo lib/Integers.vo -lib/Parmov.vo: lib/Parmov.v lib/Axioms.vo lib/Coqlib.vo -lib/UnionFind.vo: lib/UnionFind.v lib/Coqlib.vo -common/Errors.vo: common/Errors.v lib/Coqlib.vo -common/AST.vo: common/AST.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo -common/Events.vo: common/Events.v lib/Coqlib.vo lib/Intv.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Errors.vo -common/Globalenvs.vo: common/Globalenvs.v lib/Axioms.vo 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/Memdata.vo: common/Memdata.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo -common/Memtype.vo: common/Memtype.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo -common/Memory.vo: common/Memory.v lib/Axioms.vo lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo -common/Values.vo: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo -common/Smallstep.vo: common/Smallstep.v lib/Coqlib.vo common/AST.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo -common/Determinism.vo: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo -common/Switch.vo: common/Switch.v lib/Coqlib.vo lib/Integers.vo lib/Ordered.vo -backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo -$(ARCH)/Op.vo: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Globalenvs.vo -backend/CminorSel.vo: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo -$(ARCH)/SelectOp.vo: $(ARCH)/SelectOp.v lib/Coqlib.vo lib/Maps.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 -backend/Selection.vo: backend/Selection.v lib/Coqlib.vo lib/Maps.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.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/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo -backend/Selectionproof.vo: backend/Selectionproof.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/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo -backend/Registers.vo: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo -backend/RTL.vo: backend/RTL.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/Registers.vo -backend/RTLgen.vo: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo -backend/RTLgenspec.vo: backend/RTLgenspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo -backend/RTLgenproof.vo: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo common/Switch.vo backend/Registers.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenspec.vo common/Errors.vo -backend/Tailcall.vo: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Globalenvs.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo -backend/Tailcallproof.vo: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Tailcall.vo -backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo common/Memory.vo lib/Integers.vo common/Events.vo common/Smallstep.vo backend/RTL.vo backend/Conventions.vo -backend/Kildall.vo: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo -backend/CastOptim.vo: backend/CastOptim.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo -backend/CastOptimproof.vo: backend/CastOptimproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.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/CastOptim.vo -$(ARCH)/ConstpropOp.vo: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo -backend/Constprop.vo: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo -$(ARCH)/ConstpropOpproof.vo: $(ARCH)/ConstpropOpproof.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/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo -backend/Constpropproof.vo: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.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 $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo -backend/CSE.vo: backend/CSE.v lib/Coqlib.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/Registers.vo backend/RTL.vo backend/Kildall.vo -backend/CSEproof.vo: backend/CSEproof.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 $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/CSE.vo -$(ARCH)/Machregs.vo: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo -backend/Locations.vo: backend/Locations.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo -$(ARCH)/$(VARIANT)/Conventions1.vo: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo -backend/Conventions.vo: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo -backend/LTL.vo: 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/LTLtyping.vo: backend/LTLtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo -backend/InterfGraph.vo: backend/InterfGraph.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo backend/Registers.vo backend/Locations.vo -backend/Coloring.vo: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo -backend/Coloringproof.vo: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo -backend/Allocation.vo: backend/Allocation.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/LTL.vo -backend/Allocproof.vo: backend/Allocproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/LTL.vo -backend/Alloctyping.vo: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Conventions.vo -backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo -backend/Tunnelingproof.vo: 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 -backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo -backend/LTLin.vo: backend/LTLin.v lib/Coqlib.vo lib/Maps.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/Locations.vo backend/LTL.vo backend/Conventions.vo -backend/LTLintyping.vo: backend/LTLintyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTLin.vo backend/LTLtyping.vo backend/Conventions.vo -backend/Linearize.vo: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo common/Globalenvs.vo common/Errors.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLin.vo backend/Kildall.vo lib/Lattice.vo -backend/Linearizeproof.vo: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Errors.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo lib/Lattice.vo -backend/Linearizetyping.vo: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo backend/LTLintyping.vo backend/Conventions.vo -backend/Linear.vo: backend/Linear.v lib/Coqlib.vo lib/Maps.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/Locations.vo backend/LTL.vo backend/Conventions.vo -backend/Lineartyping.vo: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo -backend/Parallelmove.vo: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo common/Values.vo common/Events.vo common/AST.vo backend/Locations.vo backend/Conventions.vo -backend/Reload.vo: backend/Reload.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/Conventions.vo backend/Parallelmove.vo backend/Linear.vo -backend/Reloadproof.vo: backend/Reloadproof.v lib/Coqlib.vo lib/Maps.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/Locations.vo backend/Conventions.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Parallelmove.vo backend/Reload.vo -backend/Reloadtyping.vo: backend/Reloadtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Parallelmove.vo backend/Reload.vo backend/Reloadproof.vo -backend/Mach.vo: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo -backend/Machabstr.vo: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo -backend/Machtyping.vo: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machabstr.vo -backend/Bounds.vo: backend/Bounds.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo -$(ARCH)/$(VARIANT)/Stacklayout.vo: $(ARCH)/$(VARIANT)/Stacklayout.v lib/Coqlib.vo backend/Bounds.vo -backend/Stacking.vo: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo -backend/Stackingproof.vo: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.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/Machabstr.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo -backend/Stackingtyping.vo: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingproof.vo -backend/Machconcr.vo: backend/Machconcr.v lib/Coqlib.vo lib/Maps.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/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo -backend/Machabstr2concr.vo: backend/Machabstr2concr.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.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/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/Machabstr.vo backend/Machconcr.vo backend/Conventions.vo $(ARCH)/Asmgenretaddr.vo -$(ARCH)/Asm.vo: $(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)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo -$(ARCH)/Asmgen.vo: $(ARCH)/Asmgen.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/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo -$(ARCH)/Asmgenretaddr.vo: $(ARCH)/Asmgenretaddr.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/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo -$(ARCH)/Asmgenproof1.vo: $(ARCH)/Asmgenproof1.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/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machconcr.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo -$(ARCH)/Asmgenproof.vo: $(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/Mach.vo backend/Machconcr.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo -cfrontend/Csyntax.vo: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo -cfrontend/Csem.vo: cfrontend/Csem.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 cfrontend/Csyntax.vo common/Smallstep.vo -cfrontend/Cstrategy.vo: cfrontend/Cstrategy.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/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo -cfrontend/SimplExpr.vo: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo -cfrontend/SimplExprspec.vo: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo -cfrontend/SimplExprproof.vo: cfrontend/SimplExprproof.v lib/Axioms.vo 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 common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo -cfrontend/Clight.vo: 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/Csyntax.vo cfrontend/Csem.vo -cfrontend/Cshmgen.vo: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo -cfrontend/Cshmgenproof.vo: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo -cfrontend/Csharpminor.vo: cfrontend/Csharpminor.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 backend/Cminor.vo common/Smallstep.vo -cfrontend/Cminorgen.vo: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo -cfrontend/Cminorgenproof.vo: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo -driver/Compiler.vo: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2concr.vo $(ARCH)/Asmgenproof.vo -driver/Complements.vo: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo +lib/Axioms.vo lib/Axioms.glob: lib/Axioms.v +lib/Coqlib.vo lib/Coqlib.glob: lib/Coqlib.v +lib/Intv.vo lib/Intv.glob: lib/Intv.v lib/Coqlib.vo +lib/Maps.vo lib/Maps.glob: lib/Maps.v lib/Coqlib.vo +lib/Heaps.vo lib/Heaps.glob: lib/Heaps.v lib/Coqlib.vo lib/Ordered.vo +lib/Lattice.vo lib/Lattice.glob: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo +lib/Ordered.vo lib/Ordered.glob: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo +lib/Iteration.vo lib/Iteration.glob: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo +lib/Integers.vo lib/Integers.glob: lib/Integers.v lib/Axioms.vo lib/Coqlib.vo +lib/Floats.vo lib/Floats.glob: lib/Floats.v lib/Coqlib.vo lib/Integers.vo +lib/Parmov.vo lib/Parmov.glob: lib/Parmov.v lib/Axioms.vo lib/Coqlib.vo +lib/UnionFind.vo lib/UnionFind.glob: lib/UnionFind.v lib/Coqlib.vo +common/Errors.vo common/Errors.glob: common/Errors.v lib/Coqlib.vo +common/AST.vo common/AST.glob: common/AST.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo +common/Events.vo common/Events.glob: common/Events.v lib/Coqlib.vo lib/Intv.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Errors.vo +common/Globalenvs.vo common/Globalenvs.glob: common/Globalenvs.v lib/Axioms.vo 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/Memdata.vo common/Memdata.glob: common/Memdata.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo +common/Memtype.vo common/Memtype.glob: common/Memtype.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo +common/Memory.vo common/Memory.glob: common/Memory.v lib/Axioms.vo lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo +common/Values.vo common/Values.glob: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo +common/Smallstep.vo common/Smallstep.glob: common/Smallstep.v lib/Coqlib.vo common/AST.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo +common/Determinism.vo common/Determinism.glob: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo +common/Switch.vo common/Switch.glob: common/Switch.v lib/Coqlib.vo lib/Integers.vo lib/Ordered.vo +backend/Cminor.vo backend/Cminor.glob: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo +$(ARCH)/Op.vo $(ARCH)/Op.glob: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Globalenvs.vo +backend/CminorSel.vo backend/CminorSel.glob: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Memory.vo backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo +$(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob: $(ARCH)/SelectOp.v lib/Coqlib.vo lib/Maps.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 +backend/Selection.vo backend/Selection.glob: backend/Selection.v lib/Coqlib.vo lib/Maps.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 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/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo +backend/Selectionproof.vo backend/Selectionproof.glob: backend/Selectionproof.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/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo +backend/Registers.vo backend/Registers.glob: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo +backend/RTL.vo backend/RTL.glob: backend/RTL.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/Registers.vo +backend/RTLgen.vo backend/RTLgen.glob: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo +backend/RTLgenspec.vo backend/RTLgenspec.glob: backend/RTLgenspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo +backend/RTLgenproof.vo backend/RTLgenproof.glob: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo common/Switch.vo backend/Registers.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo backend/RTLgenspec.vo common/Errors.vo +backend/Tailcall.vo backend/Tailcall.glob: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Globalenvs.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo +backend/Tailcallproof.vo backend/Tailcallproof.glob: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Tailcall.vo +backend/RTLtyping.vo backend/RTLtyping.glob: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo common/Memory.vo lib/Integers.vo common/Events.vo common/Smallstep.vo backend/RTL.vo backend/Conventions.vo +backend/Kildall.vo backend/Kildall.glob: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo +backend/CastOptim.vo backend/CastOptim.glob: backend/CastOptim.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo +backend/CastOptimproof.vo backend/CastOptimproof.glob: backend/CastOptimproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.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/CastOptim.vo +$(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOp.glob: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo +backend/Constprop.vo backend/Constprop.glob: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo $(ARCH)/ConstpropOp.vo +$(ARCH)/ConstpropOpproof.vo $(ARCH)/ConstpropOpproof.glob: $(ARCH)/ConstpropOpproof.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/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo +backend/Constpropproof.vo backend/Constpropproof.glob: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.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 $(ARCH)/ConstpropOp.vo backend/Constprop.vo $(ARCH)/ConstpropOpproof.vo +backend/CSE.vo backend/CSE.glob: backend/CSE.v lib/Coqlib.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/Registers.vo backend/RTL.vo backend/Kildall.vo +backend/CSEproof.vo backend/CSEproof.glob: backend/CSEproof.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 $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo backend/CSE.vo +$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo +backend/Locations.vo backend/Locations.glob: backend/Locations.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo $(ARCH)/Machregs.vo +$(ARCH)/$(VARIANT)/Conventions1.vo $(ARCH)/$(VARIANT)/Conventions1.glob: $(ARCH)/$(VARIANT)/Conventions1.v lib/Coqlib.vo common/AST.vo backend/Locations.vo +backend/Conventions.vo backend/Conventions.glob: backend/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions1.vo +backend/LTL.vo backend/LTL.glob: 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/LTLtyping.vo backend/LTLtyping.glob: backend/LTLtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo +backend/InterfGraph.vo backend/InterfGraph.glob: backend/InterfGraph.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo backend/Registers.vo backend/Locations.vo +backend/Coloring.vo backend/Coloring.glob: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo +backend/Coloringproof.vo backend/Coloringproof.glob: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo +backend/Allocation.vo backend/Allocation.glob: backend/Allocation.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/LTL.vo +backend/Allocproof.vo backend/Allocproof.glob: backend/Allocproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/LTL.vo +backend/Alloctyping.vo backend/Alloctyping.glob: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Conventions.vo +backend/Tunneling.vo backend/Tunneling.glob: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo +backend/Tunnelingproof.vo backend/Tunnelingproof.glob: 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 +backend/Tunnelingtyping.vo backend/Tunnelingtyping.glob: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo +backend/LTLin.vo backend/LTLin.glob: backend/LTLin.v lib/Coqlib.vo lib/Maps.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/Locations.vo backend/LTL.vo backend/Conventions.vo +backend/LTLintyping.vo backend/LTLintyping.glob: backend/LTLintyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTLin.vo backend/LTLtyping.vo backend/Conventions.vo +backend/Linearize.vo backend/Linearize.glob: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo common/Globalenvs.vo common/Errors.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLin.vo backend/Kildall.vo lib/Lattice.vo +backend/Linearizeproof.vo backend/Linearizeproof.glob: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Errors.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo lib/Lattice.vo +backend/Linearizetyping.vo backend/Linearizetyping.glob: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo backend/LTLintyping.vo backend/Conventions.vo +backend/Linear.vo backend/Linear.glob: backend/Linear.v lib/Coqlib.vo lib/Maps.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/Locations.vo backend/LTL.vo backend/Conventions.vo +backend/Lineartyping.vo backend/Lineartyping.glob: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Memdata.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo +backend/Parallelmove.vo backend/Parallelmove.glob: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo common/Values.vo common/Events.vo common/AST.vo backend/Locations.vo backend/Conventions.vo +backend/Reload.vo backend/Reload.glob: backend/Reload.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/Conventions.vo backend/Parallelmove.vo backend/Linear.vo +backend/Reloadproof.vo backend/Reloadproof.glob: backend/Reloadproof.v lib/Coqlib.vo lib/Maps.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/Locations.vo backend/Conventions.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Parallelmove.vo backend/Reload.vo +backend/Reloadtyping.vo backend/Reloadtyping.glob: backend/Reloadtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTLin.vo backend/LTLintyping.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo backend/Parallelmove.vo backend/Reload.vo backend/Reloadproof.vo +backend/Mach.vo backend/Mach.glob: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo +backend/Machabstr.vo backend/Machabstr.glob: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo +backend/Machtyping.vo backend/Machtyping.glob: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Memory.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machabstr.vo +backend/Bounds.vo backend/Bounds.glob: backend/Bounds.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Lineartyping.vo backend/Conventions.vo +$(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Stacklayout.glob: $(ARCH)/$(VARIANT)/Stacklayout.v lib/Coqlib.vo backend/Bounds.vo +backend/Stacking.vo backend/Stacking.glob: backend/Stacking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Bounds.vo backend/Mach.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo +backend/Stackingproof.vo backend/Stackingproof.glob: backend/Stackingproof.v lib/Coqlib.vo lib/Maps.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/Machabstr.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo +backend/Stackingtyping.vo backend/Stackingtyping.glob: backend/Stackingtyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo backend/Lineartyping.vo backend/Mach.vo backend/Machtyping.vo backend/Bounds.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Stacking.vo backend/Stackingproof.vo +backend/Machconcr.vo backend/Machconcr.glob: backend/Machconcr.v lib/Coqlib.vo lib/Maps.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/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo +backend/Machabstr2concr.vo backend/Machabstr2concr.glob: backend/Machabstr2concr.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.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/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/Machabstr.vo backend/Machconcr.vo backend/Conventions.vo $(ARCH)/Asmgenretaddr.vo +$(ARCH)/Asm.vo $(ARCH)/Asm.glob: $(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)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo +$(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.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/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo +$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.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/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo +$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.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/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machconcr.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo +$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(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/Mach.vo backend/Machconcr.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo +cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo +cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.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 cfrontend/Csyntax.vo common/Smallstep.vo +cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.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/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo +cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Csyntax.vo cfrontend/Csem.vo +cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: 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/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo +cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo +cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo +cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo 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 common/Determinism.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 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/Csyntax.vo cfrontend/Csem.vo +cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob: cfrontend/Cshmgen.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo +cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo +cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.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 backend/Cminor.vo common/Smallstep.vo +cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo +cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo +driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo backend/Machabstr2concr.vo $(ARCH)/Asmgenproof.vo +driver/Complements.vo driver/Complements.glob: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo @@ -70,6 +70,7 @@ BACKEND=\ # C front-end modules (in cfrontend/) CFRONTEND=Csyntax.v Csem.v Cstrategy.v \ + Initializers.v Initializersproof.v \ SimplExpr.v SimplExprspec.v SimplExprproof.v \ Clight.v Cshmgen.v Cshmgenproof.v \ Csharpminor.v Cminorgen.v Cminorgenproof.v diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 23d0502..eefc813 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -12,6 +12,8 @@ open Printf +module CompcertErrors = Errors (* avoid shadowing by Cparser.Errors *) + open Cparser open Cparser.C open Cparser.Env @@ -743,14 +745,20 @@ let convertFundecl env (sto, id, ty, optinit) = (** Initializers *) -let init_data_of_string s = - let id = ref [] in - let enter_char c = - let n = coqint_of_camlint(Int32.of_int(Char.code c)) in - id := Init_int8 n :: !id in - enter_char '\000'; - for i = String.length s - 1 downto 0 do enter_char s.[i] done; - !id +let init_data_size = function + | Init_int8 _ -> 1 + | Init_int16 _ -> 2 + | Init_int32 _ -> 4 + | Init_float32 _ -> 4 + | Init_float64 _ -> 8 + | Init_addrof _ -> 4 + | Init_space _ -> assert false + +let string_of_errmsg msg = + let string_of_err = function + | CompcertErrors.MSG s -> camlstring_of_coqstring s + | CompcertErrors.CTX i -> extern_atom i + in String.concat "" (List.map string_of_err msg) let convertInit env ty init = @@ -767,54 +775,17 @@ let convertInit env ty init = let check_align size = assert (!pos land (size - 1) = 0) in - let rec reduceInitExpr = function - | { edesc = C.EVar id; etyp = ty } -> - begin match Cutil.unroll env ty with - | C.TArray _ | C.TFun _ -> Some id - | _ -> None - end - | {edesc = C.EUnop(C.Oaddrof, {edesc = C.EVar id})} -> Some id - | {edesc = C.ECast(ty, e)} -> reduceInitExpr e - | _ -> None in - let rec cvtInit ty = function | Init_single e -> - begin match reduceInitExpr e with - | Some id -> - check_align 4; - emit 4 (Init_addrof(intern_string id.name, coqint_of_camlint 0l)) - | None -> - match Ceval.constant_expr env ty e with - | Some(C.CInt(v, ik, _)) -> - begin match convertIkind ik with - | (_, I8) -> - emit 1 (Init_int8(convertInt v)) - | (_, I16) -> - check_align 2; - emit 2 (Init_int16(convertInt v)) - | (_, I32) -> - check_align 4; - emit 4 (Init_int32(convertInt v)) - end - | Some(C.CFloat(v, fk, _)) -> - begin match convertFkind fk with - | F32 -> - check_align 4; - emit 4 (Init_float32 v) - | F64 -> - check_align 8; - emit 8 (Init_float64 v) - end - | Some(C.CStr s) -> - check_align 4; - let id = name_for_string_literal env s in - emit 4 (Init_addrof(id, coqint_of_camlint 0l)) - | Some(C.CWStr _) -> - unsupported "wide character strings" - | Some(C.CEnum _) -> - error "enum tag after constant folding" - | None -> - error "initializer is not a compile-time constant" + begin match Initializers.transl_init_single + (convertTyp env ty) (convertExpr env e) with + | CompcertErrors.OK init -> + let sz = init_data_size init in + check_align sz; + emit sz init + | CompcertErrors.Error msg -> + Format.printf "%a@." Cprint.exp (0, e); + error ("in initializing expression above: " ^ string_of_errmsg msg) end | Init_array il -> let ty_elt = diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 927cd69..dff5fa2 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -13,7 +13,7 @@ (* *) (* *********************************************************************) -(** Dynamic semantics for the Clight language *) +(** Dynamic semantics for the Compcert C language *) Require Import Coqlib. Require Import Errors. diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v new file mode 100644 index 0000000..926a826 --- /dev/null +++ b/cfrontend/Initializers.v @@ -0,0 +1,173 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Compile-time evaluation of initializers for global C variables. *) + +Require Import Coqlib. +Require Import Errors. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import AST. +Require Import Memory. +Require Import Csyntax. +Require Import Csem. + +Open Scope error_monad_scope. + +(** * Evaluation of compile-time constant expressions *) + +(** Computing the predicates [cast], [is_true], and [is_false]. *) + +Definition bool_val (v: val) (t: type) : res bool := + match v, t with + | Vint n, Tint sz sg => OK (negb (Int.eq n Int.zero)) + | Vint n, Tpointer t' => OK (negb (Int.eq n Int.zero)) + | Vptr b ofs, Tint sz sg => OK true + | Vptr b ofs, Tpointer t' => OK true + | Vfloat f, Tfloat sz => OK (negb(Float.cmp Ceq f Float.zero)) + | _, _ => Error(msg "undefined conditional") + end. + +Definition is_neutral_for_cast (t: type) : bool := + match t with + | Tint I32 sg => true + | Tpointer ty => true + | Tarray ty sz => true + | Tfunction targs tres => true + | _ => false + end. + +Definition do_cast (v: val) (t1 t2: type) : res val := + match v, t1, t2 with + | Vint i, Tint sz1 si1, Tint sz2 si2 => + OK (Vint (cast_int_int sz2 si2 i)) + | Vfloat f, Tfloat sz1, Tint sz2 si2 => + match cast_float_int si2 f with + | Some i => OK (Vint (cast_int_int sz2 si2 i)) + | None => Error(msg "overflow in float-to-int cast") + end + | Vint i, Tint sz1 si1, Tfloat sz2 => + OK (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) + | Vfloat f, Tfloat sz1, Tfloat sz2 => + OK (Vfloat (cast_float_float sz2 f)) + | Vptr b ofs, _, _ => + if is_neutral_for_cast t1 && is_neutral_for_cast t2 + then OK(Vptr b ofs) else Error(msg "undefined cast") + | Vint n, _, _ => + if is_neutral_for_cast t1 && is_neutral_for_cast t2 + then OK(Vint n) else Error(msg "undefined cast") + | _, _, _ => + Error(msg "undefined cast") + end. + +(** To evaluate constant expressions at compile-time, we use the same [value] + type and the same [sem_*] functions that are used in CompCert C's semantics + (module [Csem]). However, we interpret pointer values symbolically: + [Vptr (Zpos id) ofs] represents the address of global variable [id] + plus byte offset [ofs]. *) + +(** [constval a] evaluates the constant expression [a]. + +If [a] is a r-value, the returned value denotes: +- [Vint n], [Vfloat f]: the corresponding number +- [Vptr id ofs]: address of global variable [id] plus byte offset [ofs] +- [Vundef]: erroneous expression + +If [a] is a l-value, the returned value denotes: +- [Vptr id ofs]: global variable [id] plus byte offset [ofs] +*) + +Fixpoint constval (a: expr) : res val := + match a with + | Eval v ty => + match v with + | Vint _ | Vfloat _ => OK v + | Vptr _ _ | Vundef => Error(msg "illegal constant") + end + | Evalof l ty => + match access_mode ty with + | By_reference => constval l + | _ => Error(msg "dereference operation") + end + | Eaddrof l ty => + constval l + | Eunop op r1 ty => + do v1 <- constval r1; + match sem_unary_operation op v1 (typeof r1) with + | Some v => OK v + | None => Error(msg "undefined unary operation") + end + | Ebinop op r1 r2 ty => + do v1 <- constval r1; + do v2 <- constval r2; + match sem_binary_operation op v1 (typeof r1) v2 (typeof r2) Mem.empty with + | Some v => OK v + | None => Error(msg "undefined binary operation") + end + | Ecast r ty => + do v <- constval r; do_cast v (typeof r) ty + | Esizeof ty1 ty => + OK (Vint (Int.repr (sizeof ty1))) + | Econdition r1 r2 r3 ty => + do v1 <- constval r1; + do b1 <- bool_val v1 (typeof r1); + do v2 <- constval r2; + do v3 <- constval r3; + OK (if b1 then v2 else v3) + | Ecomma r1 r2 ty => + do v1 <- constval r1; constval r2 + | Evar x ty => + OK(Vptr (Zpos x) Int.zero) + | Ederef r ty => + constval r + | Efield l f ty => + match typeof l with + | Tstruct id fList => + do delta <- field_offset f fList; + do v <- constval l; + OK (Val.add v (Vint (Int.repr delta))) + | Tunion id fList => + constval l + | _ => + Error(msg "ill-typed field access") + end + | Eparen r ty => + constval r + | _ => + Error(msg "not a compile-time constant") + end. + +(** * Translation of initializers *) + +(** Translate an initializing expression [a] for a scalar variable + of type [ty]. Return the corresponding [init_data]. *) + +Definition transl_init_single (ty: type) (a: expr) : res init_data := + do v1 <- constval a; + do v2 <- do_cast v1 (typeof a) ty; + match v2, ty with + | Vint n, Tint I8 sg => OK(Init_int8 n) + | Vint n, Tint I16 sg => OK(Init_int16 n) + | Vint n, Tint I32 sg => OK(Init_int32 n) + | Vint n, Tpointer _ => OK(Init_int32 n) + | Vfloat f, Tfloat F32 => OK(Init_float32 f) + | Vfloat f, Tfloat F64 => OK(Init_float64 f) + | Vptr (Zpos id) ofs, Tint I32 sg => OK(Init_addrof id ofs) + | Vptr (Zpos id) ofs, Tpointer _ => OK(Init_addrof id ofs) + | Vundef, _ => Error(msg "undefined operation in initializer") + | _, _ => Error (msg "type mismatch in initializer") + end. + +(** To come later: translation of compound initializers, currently + still done in Caml (module [C2C]). *) + diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v new file mode 100644 index 0000000..fde3c4e --- /dev/null +++ b/cfrontend/Initializersproof.v @@ -0,0 +1,555 @@ +(* *********************************************************************) +(* *) +(* 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 INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Compile-time evaluation of initializers for global C variables. *) + +Require Import Coq.Program.Equality. +Require Import Coqlib. +Require Import Errors. +Require Import Maps. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import AST. +Require Import Memory. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Csyntax. +Require Import Csem. +Require Import Initializers. + +Open Scope error_monad_scope. + +Section SOUNDNESS. + +Variable ge: genv. + +(** * Simple expressions and their big-step semantics *) + +(** An expression is simple if it contains no assignments and no + function calls. *) + +Fixpoint simple (a: expr) : Prop := + match a with + | Eloc _ _ _ => True + | Evar _ _ => True + | Ederef r _ => simple r + | Efield l1 _ _ => simple l1 + | Eval _ _ => True + | Evalof l _ => simple l + | Eaddrof l _ => simple l + | Eunop _ r1 _ => simple r1 + | Ebinop _ r1 r2 _ => simple r1 /\ simple r2 + | Ecast r1 _ => simple r1 + | Econdition r1 r2 r3 _ => simple r1 /\ simple r2 /\ simple r3 + | Esizeof _ _ => True + | Eassign _ _ _ => False + | Eassignop _ _ _ _ _ => False + | Epostincr _ _ _ => False + | Ecomma r1 r2 _ => simple r1 /\ simple r2 + | Ecall _ _ _ => False + | Eparen r1 _ => simple r1 + end. + +(** A big-step semantics for simple expressions. Similar to the + big-step semantics from [Cstrategy], with the addition of + conditionals, comma and paren operators. It is a pity we do not + share definitions with [Cstrategy], but such sharing raises + technical difficulties. *) + +Section SIMPLE_EXPRS. + +Variable e: env. +Variable m: mem. + +Inductive eval_simple_lvalue: expr -> block -> int -> Prop := + | esl_loc: forall b ofs ty, + eval_simple_lvalue (Eloc b ofs ty) b ofs + | esl_var_local: forall x ty b, + e!x = Some(b, ty) -> + eval_simple_lvalue (Evar x ty) b Int.zero + | esl_var_global: forall x ty b, + e!x = None -> + Genv.find_symbol ge x = Some b -> + type_of_global ge b = Some ty -> + eval_simple_lvalue (Evar x ty) b Int.zero + | esl_deref: forall r ty b ofs, + eval_simple_rvalue r (Vptr b ofs) -> + eval_simple_lvalue (Ederef r ty) b ofs + | esl_field_struct: forall l f ty b ofs id fList delta, + eval_simple_lvalue l b ofs -> + typeof l = Tstruct id fList -> field_offset f fList = OK delta -> + eval_simple_lvalue (Efield l f ty) b (Int.add ofs (Int.repr delta)) + | esl_field_union: forall l f ty b ofs id fList, + eval_simple_lvalue l b ofs -> + typeof l = Tunion id fList -> + eval_simple_lvalue (Efield l f ty) b ofs + +with eval_simple_rvalue: expr -> val -> Prop := + | esr_val: forall v ty, + eval_simple_rvalue (Eval v ty) v + | esr_rvalof: forall b ofs l ty v, + eval_simple_lvalue l b ofs -> + ty = typeof l -> + load_value_of_type ty m b ofs = Some v -> + eval_simple_rvalue (Evalof l ty) v + | esr_addrof: forall b ofs l ty, + eval_simple_lvalue l b ofs -> + eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) + | esr_unop: forall op r1 ty v1 v, + eval_simple_rvalue r1 v1 -> + sem_unary_operation op v1 (typeof r1) = Some v -> + eval_simple_rvalue (Eunop op r1 ty) v + | esr_binop: forall op r1 r2 ty v1 v2 v, + eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> + sem_binary_operation op v1 (typeof r1) v2 (typeof r2) m = Some v -> + eval_simple_rvalue (Ebinop op r1 r2 ty) v + | esr_cast: forall ty r1 v1 v, + eval_simple_rvalue r1 v1 -> + cast v1 (typeof r1) ty v -> + eval_simple_rvalue (Ecast r1 ty) v + | esr_sizeof: forall ty1 ty, + eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))) + | esr_condition_true: forall r1 r2 r3 ty v v1, + eval_simple_rvalue r1 v1 -> is_true v1 (typeof r1) -> eval_simple_rvalue r2 v -> + eval_simple_rvalue (Econdition r1 r2 r3 ty) v + | esr_condition_false: forall r1 r2 r3 ty v v1, + eval_simple_rvalue r1 v1 -> is_false v1 (typeof r1) -> eval_simple_rvalue r3 v -> + eval_simple_rvalue (Econdition r1 r2 r3 ty) v + | esr_comma: forall r1 r2 ty v1 v, + eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v -> + eval_simple_rvalue (Ecomma r1 r2 ty) v + | esr_paren: forall r ty v, + eval_simple_rvalue r v -> + eval_simple_rvalue (Eparen r ty) v. + +End SIMPLE_EXPRS. + +(** * Correctness of the big-step semantics with respect to reduction sequences *) + +(** In this section, we show that if a simple expression [a] reduces to + some value (with the transition semantics from module [Csem]), + then it evaluates to this value (with the big-step semantics above). *) + +Definition compat_eval (k: kind) (e: env) (a a': expr) (m: mem) : Prop := + typeof a = typeof a' /\ + match k with + | LV => forall b ofs, eval_simple_lvalue e m a' b ofs -> eval_simple_lvalue e m a b ofs + | RV => forall v, eval_simple_rvalue e m a' v -> eval_simple_rvalue e m a v + end. + +Lemma lred_simple: + forall e l m l' m', lred ge e l m l' m' -> simple l -> simple l'. +Proof. + induction 1; simpl; tauto. +Qed. + +Lemma lred_compat: + forall e l m l' m', lred ge e l m l' m' -> + m = m' /\ compat_eval LV e l l' m. +Proof. + induction 1; simpl; split; auto; split; auto; intros bx ofsx EV; inv EV. + apply esl_var_local; auto. + apply esl_var_global; auto. + constructor. constructor. + eapply esl_field_struct; eauto. constructor. simpl; eauto. + eapply esl_field_union; eauto. constructor. simpl; eauto. +Qed. + +Lemma rred_simple: + forall r m r' m', rred r m r' m' -> simple r -> simple r'. +Proof. + induction 1; simpl; tauto. +Qed. + +Lemma rred_compat: + forall e r m r' m', rred r m r' m' -> + simple r -> + m = m' /\ compat_eval RV e r r' m. +Proof. + induction 1; simpl; intro SIMP; try contradiction; split; auto; split; auto; intros vx EV. + inv EV. econstructor. constructor. auto. auto. + inv EV. econstructor. constructor. + inv EV. econstructor; eauto. constructor. + inv EV. econstructor; eauto. constructor. constructor. + inv EV. econstructor; eauto. constructor. + inv EV. eapply esr_condition_true; eauto. constructor. + inv EV. eapply esr_condition_false; eauto. constructor. + inv EV. constructor. + econstructor; eauto. constructor. + constructor; auto. +Qed. + +Lemma compat_eval_context: + forall e a a' m from to C, + context from to C -> + compat_eval from e a a' m -> + compat_eval to e (C a) (C a') m. +Proof. + induction 1; intros CE; auto; + try (generalize (IHcontext CE); intros [TY EV]; red; split; simpl; auto; intros). + inv H0. constructor; auto. + inv H0. + eapply esl_field_struct; eauto. rewrite TY; eauto. + eapply esl_field_union; eauto. rewrite TY; eauto. + inv H0. econstructor. eauto. auto. auto. + inv H0. econstructor; eauto. + inv H0. econstructor; eauto. congruence. + inv H0. econstructor; eauto. congruence. + inv H0. econstructor; eauto. congruence. + inv H0. econstructor; eauto. congruence. + inv H0. + eapply esr_condition_true; eauto. congruence. + eapply esr_condition_false; eauto. congruence. + inv H0. + inv H0. + inv H0. + inv H0. + inv H0. + inv H0. + red; split; intros. auto. inv H0. + inv H0. econstructor; eauto. + inv H0. constructor. auto. +Qed. + +Lemma simple_context_1: + forall a from to C, context from to C -> simple (C a) -> simple a. +Proof. + induction 1; simpl; tauto. +Qed. + +Lemma simple_context_2: + forall a a', simple a' -> forall from to C, context from to C -> simple (C a) -> simple (C a'). +Proof. + induction 2; simpl; tauto. +Qed. + +Lemma compat_eval_steps: + forall f r e m w r' m', + star step ge (ExprState f r Kstop e m) w (ExprState f r' Kstop e m') -> + simple r -> + m' = m /\ compat_eval RV e r r' m. +Proof. + intros. dependent induction H. + (* base case *) + split. auto. red; auto. + (* inductive case *) + destruct H. + (* expression step *) + assert (X: exists r1, s2 = ExprState f r1 Kstop e m /\ compat_eval RV e r r1 m /\ simple r1). + inv H. + (* lred *) + assert (S: simple a) by (eapply simple_context_1; eauto). + exploit lred_compat; eauto. intros [A B]. subst m'0. + econstructor; split. eauto. split. + eapply compat_eval_context; eauto. + eapply simple_context_2; eauto. eapply lred_simple; eauto. + (* rred *) + assert (S: simple a) by (eapply simple_context_1; eauto). + exploit rred_compat; eauto. intros [A B]. subst m'0. + econstructor; split. eauto. split. + eapply compat_eval_context; eauto. + eapply simple_context_2; eauto. eapply rred_simple; eauto. + (* callred *) + assert (S: simple a) by (eapply simple_context_1; eauto). + inv H9; simpl in S; contradiction. + destruct X as [r1 [A [B C]]]. subst s2. + exploit IHstar; eauto. intros [D E]. + split. auto. destruct B; destruct E. split. congruence. auto. + (* statement steps *) + inv H. +Qed. + +Theorem eval_simple_steps: + forall f r e m w v ty m', + star step ge (ExprState f r Kstop e m) w (ExprState f (Eval v ty) Kstop e m') -> + simple r -> + m' = m /\ ty = typeof r /\ eval_simple_rvalue e m r v. +Proof. + intros. exploit compat_eval_steps; eauto. intros [A [B C]]. + intuition. apply C. constructor. +Qed. + +(** * Soundness of the compile-time evaluator *) + +(** [match_val v v'] holds if the compile-time value [v] + (with symbolic pointers) matches the run-time value [v'] + (with concrete pointers). *) + +Inductive match_val: val -> val -> Prop := + | match_vint: forall n, + match_val (Vint n) (Vint n) + | match_vfloat: forall f, + match_val (Vfloat f) (Vfloat f) + | match_vptr: forall id b ofs, + Genv.find_symbol ge id = Some b -> + match_val (Vptr (Zpos id) ofs) (Vptr b ofs) + | match_vundef: + match_val Vundef Vundef. + +Lemma match_val_of_bool: + forall b, match_val (Val.of_bool b) (Val.of_bool b). +Proof. + destruct b; constructor. +Qed. + +Hint Constructors match_val: mval. +Hint Resolve match_val_of_bool: mval. + +(** The [match_val] relation commutes with the evaluation functions + from [Csem]. *) + +Lemma sem_unary_match: + forall op ty v1 v v1' v', + sem_unary_operation op v1 ty = Some v -> + sem_unary_operation op v1' ty = Some v' -> + match_val v1 v1' -> + match_val v v'. +Proof. + intros. destruct op; simpl in *. + unfold sem_notbool in *. destruct (classify_bool ty); inv H1; inv H; inv H0; auto with mval. constructor. + unfold sem_notint in *. destruct (classify_notint ty); inv H1; inv H; inv H0; auto with mval. + unfold sem_neg in *. destruct (classify_neg ty); inv H1; inv H; inv H0; auto with mval. +Qed. + +Lemma mem_empty_not_valid_pointer: + forall b ofs, Mem.valid_pointer Mem.empty b ofs = false. +Proof. + intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Nonempty); auto. + red in p. simpl in p. contradiction. +Qed. + +Lemma sem_cmp_match: + forall c v1 ty1 v2 ty2 m v v1' v2' v', + sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v -> + sem_cmp c v1' ty1 v2' ty2 m = Some v' -> + match_val v1 v1' -> match_val v2 v2' -> + match_val v v'. +Proof. + intros. unfold sem_cmp in *. + destruct (classify_cmp ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. + destruct (Int.eq n Int.zero); try discriminate. + unfold sem_cmp_mismatch in *. destruct c; inv H3; inv H2; constructor. + destruct (Int.eq n Int.zero); try discriminate. + unfold sem_cmp_mismatch in *. destruct c; inv H2; inv H1; constructor. + rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.signed ofs)) in H4. discriminate. +Qed. + +Lemma sem_binary_match: + forall op v1 ty1 v2 ty2 m v v1' v2' v', + sem_binary_operation op v1 ty1 v2 ty2 Mem.empty = Some v -> + sem_binary_operation op v1' ty1 v2' ty2 m = Some v' -> + match_val v1 v1' -> match_val v2 v2' -> + match_val v v'. +Proof. + intros. unfold sem_binary_operation in *; destruct op. +(* add *) + unfold sem_add in *. destruct (classify_add ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. +(* sub *) + unfold sem_sub in *. destruct (classify_sub ty1 ty2); inv H1; inv H2; try (inv H; inv H0; auto with mval; fail). + destruct (zeq (Zpos id) (Zpos id0)); try discriminate. + assert (b0 = b) by congruence. subst b0. rewrite zeq_true in H0. + destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H; inv H0; auto with mval. +(* mul *) + unfold sem_mul in *. destruct (classify_mul ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. +(* div *) + unfold sem_div in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0. + rewrite H11 in H2. inv H2. inv H12. constructor. + rewrite H11 in H2. inv H2. inv H12. constructor. + inv H11. constructor. + inv H11. constructor. + inv H11. constructor. +(* mod *) + unfold sem_mod in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0. + rewrite H11 in H2. inv H2. inv H12. constructor. + rewrite H11 in H2. inv H2. inv H12. constructor. +(* and *) + unfold sem_and in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. +(* or *) + unfold sem_or in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. +(* xor *) + unfold sem_xor in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. +(* shl *) + unfold sem_shl in *. destruct (classify_shift ty1 ty2); inv H1; inv H2; try discriminate. + destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. +(* shr *) + unfold sem_shr in *. destruct (classify_shift ty1 ty2); try discriminate; + destruct s; inv H1; inv H2; try discriminate. + destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. + destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. +(* comparisons *) + eapply sem_cmp_match; eauto. + eapply sem_cmp_match; eauto. + eapply sem_cmp_match; eauto. + eapply sem_cmp_match; eauto. + eapply sem_cmp_match; eauto. + eapply sem_cmp_match; eauto. +Qed. + +Lemma is_neutral_for_cast_correct: + forall t, neutral_for_cast t -> is_neutral_for_cast t = true. +Proof. + induction 1; simpl; auto. +Qed. + +Lemma cast_match: + forall v1 ty1 ty2 v2, cast v1 ty1 ty2 v2 -> + forall v1' v2', match_val v1' v1 -> do_cast v1' ty1 ty2 = OK v2' -> + match_val v2' v2. +Proof. + induction 1; intros v1' v2' MV DC; inv MV; simpl in DC. + inv DC; constructor. + rewrite H in DC. inv DC. constructor. + inv DC; constructor. + inv DC; constructor. + rewrite (is_neutral_for_cast_correct _ H) in DC. + rewrite (is_neutral_for_cast_correct _ H0) in DC. + simpl in DC. inv DC. constructor; auto. + rewrite (is_neutral_for_cast_correct _ H) in DC. + rewrite (is_neutral_for_cast_correct _ H0) in DC. + simpl in DC. + assert (OK v2' = OK (Vint n)). + inv H; auto. inv H0; auto. + inv H1. constructor. +Qed. + +Lemma bool_val_true: + forall v v' ty, is_true v' ty -> match_val v v' -> bool_val v ty = OK true. +Proof. + induction 1; intros MV; inv MV; simpl; auto. + predSpec Int.eq Int.eq_spec n Int.zero. congruence. auto. + predSpec Int.eq Int.eq_spec n Int.zero. congruence. auto. + rewrite H; auto. +Qed. + +Lemma bool_val_false: + forall v v' ty, is_false v' ty -> match_val v v' -> bool_val v ty = OK false. +Proof. + induction 1; intros MV; inv MV; simpl; auto. + rewrite H; auto. +Qed. + +(** Soundness of [constval] with respect to the big-step semantics *) + +Lemma constval_rvalue: + forall m a v, + eval_simple_rvalue empty_env m a v -> + forall v', + constval a = OK v' -> + match_val v' v +with constval_lvalue: + forall m a b ofs, + eval_simple_lvalue empty_env m a b ofs -> + forall v', + constval a = OK v' -> + match_val v' (Vptr b ofs). +Proof. + (* rvalue *) + induction 1; intros v' CV; simpl in CV; try (monadInv CV). + (* val *) + destruct v; monadInv CV; constructor. + (* rval *) + unfold load_value_of_type in H1. destruct (access_mode ty); try congruence. inv H1. + eauto. + (* addrof *) + eauto. + (* unop *) + revert EQ0. caseEq (sem_unary_operation op x (typeof r1)); intros; inv EQ0. + eapply sem_unary_match; eauto. + (* binop *) + revert EQ2. caseEq (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty); intros; inv EQ2. + eapply sem_binary_match; eauto. + (* cast *) + eapply cast_match; eauto. + (* sizeof *) + constructor. + (* conditional true *) + assert (x0 = true). exploit bool_val_true; eauto. congruence. subst x0. auto. + (* conditional false *) + assert (x0 = false). exploit bool_val_false; eauto. congruence. subst x0. auto. + (* comma *) + auto. + (* paren *) + auto. + + (* lvalue *) + induction 1; intros v' CV; simpl in CV; try (monadInv CV). + (* var local *) + unfold empty_env in H. rewrite PTree.gempty in H. congruence. + (* var_global *) + constructor; auto. + (* deref *) + eauto. + (* field struct *) + rewrite H0 in CV. monadInv CV. exploit IHeval_simple_lvalue; eauto. intro MV. inv MV. + simpl. replace x with delta by congruence. constructor. auto. + (* field union *) + rewrite H0 in CV. auto. +Qed. + +Lemma constval_simple: + forall a v, constval a = OK v -> simple a. +Proof. + induction a; simpl; intros vx CV; try (monadInv CV); eauto. + destruct (typeof a); discriminate || eauto. + monadInv CV. eauto. + destruct (access_mode ty); discriminate || eauto. + intuition eauto. +Qed. + +(** Soundness of [constval] with respect to the reduction semantics. *) + +Theorem constval_steps: + forall f r m w v v' ty m', + star step ge (ExprState f r Kstop empty_env m) w (ExprState f (Eval v' ty) Kstop empty_env m') -> + constval r = OK v -> + m' = m /\ ty = typeof r /\ match_val v v'. +Proof. + intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. + intros [A [B C]]. intuition. eapply constval_rvalue; eauto. +Qed. + +(** * Soundness of the translation of initializers *) + +Theorem transl_init_single_steps: + forall ty a data f m w v1 ty1 m' v b ofs m'', + transl_init_single ty a = OK data -> + star step ge (ExprState f a Kstop empty_env m) w (ExprState f (Eval v1 ty1) Kstop empty_env m') -> + cast v1 ty1 ty v -> + store_value_of_type ty m' b ofs v = Some m'' -> + Genv.store_init_data ge m b (Int.signed ofs) data = Some m''. +Proof. + intros. monadInv H. + exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1. + exploit cast_match; eauto. intros D. + unfold Genv.store_init_data. unfold store_value_of_type in H2. simpl in H2. + inv D. + (* int *) + destruct ty; try discriminate. + destruct i; inv EQ2. + destruct s; simpl in H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. + destruct s; simpl in H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto. + assumption. + inv EQ2. assumption. + (* float *) + destruct ty; try discriminate. + destruct f1; inv EQ2; assumption. + (* pointer *) + assert (data = Init_addrof id ofs0 /\ access_mode ty = By_value Mint32). + destruct ty; inv EQ2; auto. destruct i; inv H4; auto. + destruct H3; subst. rewrite H4 in H2. rewrite H. assumption. + (* undef *) + discriminate. +Qed. + +End SOUNDNESS. + diff --git a/driver/Compiler.v b/driver/Compiler.v index e57d80d..7849d64 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -35,6 +35,7 @@ Require Linear. Require Mach. Require Asm. (** Translation passes. *) +Require Initializers. Require SimplExpr. Require Cshmgen. Require Cminorgen. @@ -173,6 +174,10 @@ Definition transf_c_program (p: Csyntax.program) : res Asm.program := @@@ Cminorgen.transl_program @@@ transf_cminor_program. +(** Force [Initializers] to be extracted as well. *) + +Definition transl_single_init := Initializers.transl_init_single. + (** The following lemmas help reason over compositions of passes. *) Lemma print_identity: diff --git a/extraction/extraction.v b/extraction/extraction.v index 1689ad2..5fc6795 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -10,13 +10,13 @@ (* *) (* *********************************************************************) -Require List. Require Iteration. Require Floats. Require RTLgen. Require Coloring. Require Allocation. Require Compiler. +Require Initializers. (* Standard lib *) Extract Inductive unit => "unit" [ "()" ]. diff --git a/test/regression/Results/initializers b/test/regression/Results/initializers Binary files differindex 979eff3..b626a2a 100644 --- a/test/regression/Results/initializers +++ b/test/regression/Results/initializers diff --git a/test/regression/init3.c b/test/regression/init3.c index 00a36e2..3a15243 100644 --- a/test/regression/init3.c +++ b/test/regression/init3.c @@ -2,5 +2,8 @@ #define NULL ((void *) 0) -char x = NULL; int t[2] = { NULL, NULL }; + +/* But this is an error in CompCert */ + +/* char u = NULL; */ diff --git a/test/regression/initializers.c b/test/regression/initializers.c index 97ce99b..7384091 100644 --- a/test/regression/initializers.c +++ b/test/regression/initializers.c @@ -35,6 +35,17 @@ int * x14 = &x2; struct { char * y; int * z; float * u; double * v; } x15 = { x4, x5, &x11, &x12 }; +unsigned char * x16[3] = { + (unsigned char *) (x4 + 1), + (unsigned char *) &x4[2], + ((unsigned char *) x4) + 3 }; + +char x17[] = "Hello!"; + +char * x18 = "Hello!"; + +char * x19[2] = { "Hello", "world!" }; + int main(int argc, char ** argv) { int i; @@ -63,6 +74,17 @@ int main(int argc, char ** argv) printf("x15 ok\n"); else printf("x15 error\n"); + if (x16[0] == (unsigned char *) x4 + 1 + && x16[1] == (unsigned char *) x4 + 2 + && x16[2] == (unsigned char *) x4 + 3) + printf("x16 ok\n"); + else + printf("x16 error\n"); + printf("x17[%d] = { ", (int) sizeof(x17)); + for (i = 0; i < sizeof(x17); i++) printf("'%c', ", x17[i]); + printf("}\n"); + printf("x18 = \"%s\"\n", x18); + printf("x19 = { \"%s\", \"%s\" }\n", x19[0], x19[1]); return 0; } |