diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-27 11:06:09 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-27 11:06:09 +0200 |
| commit | 883341719d7d6868f8165541e7e13ac45192a358 (patch) | |
| tree | 368ad6e0f2d8e4c99c13a68da0e92c7f00408ae5 | |
| parent | 88c717e497e0e8a2e6df12418833e46c56291724 (diff) | |
| download | compcert-kvx-883341719d7d6868f8165541e7e13ac45192a358.tar.gz compcert-kvx-883341719d7d6868f8165541e7e13ac45192a358.zip | |
Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 -> x86/x86_32/x86_64
Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq.
This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86.
While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures.
Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
| -rw-r--r-- | .depend | 348 | ||||
| -rw-r--r-- | .gitignore | 10 | ||||
| -rw-r--r-- | Makefile | 31 | ||||
| -rw-r--r-- | backend/SplitLongproof.v | 12 | ||||
| -rwxr-xr-x | configure | 58 | ||||
| -rw-r--r-- | driver/Driver.ml | 2 | ||||
| -rw-r--r-- | runtime/Makefile | 4 | ||||
| -rw-r--r-- | runtime/x86_32/i64_dtos.S (renamed from runtime/ia32/i64_dtos.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_dtou.S (renamed from runtime/ia32/i64_dtou.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_sar.S (renamed from runtime/ia32/i64_sar.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_sdiv.S (renamed from runtime/ia32/i64_sdiv.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_shl.S (renamed from runtime/ia32/i64_shl.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_shr.S (renamed from runtime/ia32/i64_shr.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_smod.S (renamed from runtime/ia32/i64_smod.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_smulh.S (renamed from runtime/ia32/i64_smulh.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_stod.S (renamed from runtime/ia32/i64_stod.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_stof.S (renamed from runtime/ia32/i64_stof.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_udiv.S (renamed from runtime/ia32/i64_udiv.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_udivmod.S (renamed from runtime/ia32/i64_udivmod.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_umod.S (renamed from runtime/ia32/i64_umod.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_umulh.S (renamed from runtime/ia32/i64_umulh.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_utod.S (renamed from runtime/ia32/i64_utod.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/i64_utof.S (renamed from runtime/ia32/i64_utof.S) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/sysdeps.h (renamed from runtime/ia32/sysdeps.h) | 0 | ||||
| -rw-r--r-- | runtime/x86_32/vararg.S (renamed from runtime/ia32/vararg.S) | 0 | ||||
| -rw-r--r-- | test/regression/Results/builtins-x86 (renamed from test/regression/Results/builtins-ia32) | 0 | ||||
| -rwxr-xr-x | test/regression/Runtest | 14 | ||||
| -rw-r--r-- | test/regression/builtins-x86.c (renamed from test/regression/builtins-ia32.c) | 0 | ||||
| -rw-r--r-- | x86/Asm.v (renamed from ia32/Asm.v) | 0 | ||||
| -rw-r--r-- | x86/AsmToJSON.ml (renamed from ia32/AsmToJSON.ml) | 0 | ||||
| -rw-r--r-- | x86/AsmToJSON.mli (renamed from ia32/AsmToJSON.mli) | 0 | ||||
| -rw-r--r-- | x86/Asmexpand.ml (renamed from ia32/Asmexpand.ml) | 0 | ||||
| -rw-r--r-- | x86/Asmgen.v (renamed from ia32/Asmgen.v) | 0 | ||||
| -rw-r--r-- | x86/Asmgenproof.v (renamed from ia32/Asmgenproof.v) | 0 | ||||
| -rw-r--r-- | x86/Asmgenproof1.v (renamed from ia32/Asmgenproof1.v) | 72 | ||||
| -rw-r--r-- | x86/CBuiltins.ml (renamed from ia32/CBuiltins.ml) | 0 | ||||
| -rw-r--r-- | x86/CombineOp.v (renamed from ia32/CombineOp.v) | 0 | ||||
| -rw-r--r-- | x86/CombineOpproof.v (renamed from ia32/CombineOpproof.v) | 0 | ||||
| -rw-r--r-- | x86/ConstpropOp.vp (renamed from ia32/ConstpropOp.vp) | 0 | ||||
| -rw-r--r-- | x86/ConstpropOpproof.v (renamed from ia32/ConstpropOpproof.v) | 30 | ||||
| -rw-r--r-- | x86/Conventions1.v (renamed from ia32/Conventions1.v) | 0 | ||||
| -rw-r--r-- | x86/Machregs.v (renamed from ia32/Machregs.v) | 0 | ||||
| -rw-r--r-- | x86/Machregsaux.ml (renamed from ia32/Machregsaux.ml) | 0 | ||||
| -rw-r--r-- | x86/Machregsaux.mli (renamed from ia32/Machregsaux.mli) | 0 | ||||
| -rw-r--r-- | x86/NeedOp.v (renamed from ia32/NeedOp.v) | 0 | ||||
| -rw-r--r-- | x86/Op.v (renamed from ia32/Op.v) | 37 | ||||
| -rw-r--r-- | x86/PrintOp.ml (renamed from ia32/PrintOp.ml) | 0 | ||||
| -rw-r--r-- | x86/SelectLong.vp (renamed from ia32/SelectLong.vp) | 0 | ||||
| -rw-r--r-- | x86/SelectLongproof.v (renamed from ia32/SelectLongproof.v) | 24 | ||||
| -rw-r--r-- | x86/SelectOp.vp (renamed from ia32/SelectOp.vp) | 0 | ||||
| -rw-r--r-- | x86/SelectOpproof.v (renamed from ia32/SelectOpproof.v) | 243 | ||||
| -rw-r--r-- | x86/Stacklayout.v (renamed from ia32/Stacklayout.v) | 0 | ||||
| -rw-r--r-- | x86/TargetPrinter.ml (renamed from ia32/TargetPrinter.ml) | 0 | ||||
| -rw-r--r-- | x86/ValueAOp.v (renamed from ia32/ValueAOp.v) | 2 | ||||
| -rw-r--r-- | x86/extractionMachdep.v (renamed from ia32/extractionMachdep.v) | 7 | ||||
| -rw-r--r-- | x86_32/Archi.v (renamed from ia32/Archi.v) | 8 | ||||
| -rw-r--r-- | x86_64/Archi.v | 54 |
57 files changed, 332 insertions, 624 deletions
diff --git a/.depend b/.depend deleted file mode 100644 index cb8fbab3..00000000 --- a/.depend +++ /dev/null @@ -1,348 +0,0 @@ -lib/Axioms.vo lib/Axioms.glob lib/Axioms.v.beautified: lib/Axioms.v -lib/Axioms.vio: lib/Axioms.v -lib/Coqlib.vo lib/Coqlib.glob lib/Coqlib.v.beautified: lib/Coqlib.v -lib/Coqlib.vio: lib/Coqlib.v -lib/Intv.vo lib/Intv.glob lib/Intv.v.beautified: lib/Intv.v lib/Coqlib.vo -lib/Intv.vio: lib/Intv.v lib/Coqlib.vio -lib/Maps.vo lib/Maps.glob lib/Maps.v.beautified: lib/Maps.v lib/Coqlib.vo -lib/Maps.vio: lib/Maps.v lib/Coqlib.vio -lib/Heaps.vo lib/Heaps.glob lib/Heaps.v.beautified: lib/Heaps.v lib/Coqlib.vo lib/Ordered.vo -lib/Heaps.vio: lib/Heaps.v lib/Coqlib.vio lib/Ordered.vio -lib/Lattice.vo lib/Lattice.glob lib/Lattice.v.beautified: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo -lib/Lattice.vio: lib/Lattice.v lib/Coqlib.vio lib/Maps.vio -lib/Ordered.vo lib/Ordered.glob lib/Ordered.v.beautified: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo -lib/Ordered.vio: lib/Ordered.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio -lib/Iteration.vo lib/Iteration.glob lib/Iteration.v.beautified: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo lib/Wfsimpl.vo -lib/Iteration.vio: lib/Iteration.v lib/Axioms.vio lib/Coqlib.vio lib/Wfsimpl.vio -lib/Integers.vo lib/Integers.glob lib/Integers.v.beautified: lib/Integers.v lib/Coqlib.vo $(ARCH)/Archi.vo -lib/Integers.vio: lib/Integers.v lib/Coqlib.vio $(ARCH)/Archi.vio -$(ARCH)/Archi.vo $(ARCH)/Archi.glob $(ARCH)/Archi.v.beautified: $(ARCH)/Archi.v flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo -$(ARCH)/Archi.vio: $(ARCH)/Archi.v flocq/Appli/Fappli_IEEE.vio flocq/Appli/Fappli_IEEE_bits.vio -lib/Fappli_IEEE_extra.vo lib/Fappli_IEEE_extra.glob lib/Fappli_IEEE_extra.v.beautified: lib/Fappli_IEEE_extra.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_digits.vo flocq/Calc/Fcalc_ops.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Prop/Fprop_Sterbenz.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_rnd_odd.vo -lib/Fappli_IEEE_extra.vio: lib/Fappli_IEEE_extra.v flocq/Core/Fcore.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_digits.vio flocq/Calc/Fcalc_ops.vio flocq/Calc/Fcalc_round.vio flocq/Calc/Fcalc_bracket.vio flocq/Prop/Fprop_Sterbenz.vio flocq/Appli/Fappli_IEEE.vio flocq/Appli/Fappli_rnd_odd.vio -lib/Floats.vo lib/Floats.glob lib/Floats.v.beautified: lib/Floats.v lib/Coqlib.vo lib/Integers.vo flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE_bits.vo lib/Fappli_IEEE_extra.vo flocq/Core/Fcore.vo $(ARCH)/Archi.vo -lib/Floats.vio: lib/Floats.v lib/Coqlib.vio lib/Integers.vio flocq/Appli/Fappli_IEEE.vio flocq/Appli/Fappli_IEEE_bits.vio lib/Fappli_IEEE_extra.vio flocq/Core/Fcore.vio $(ARCH)/Archi.vio -lib/Parmov.vo lib/Parmov.glob lib/Parmov.v.beautified: lib/Parmov.v lib/Axioms.vo lib/Coqlib.vo -lib/Parmov.vio: lib/Parmov.v lib/Axioms.vio lib/Coqlib.vio -lib/UnionFind.vo lib/UnionFind.glob lib/UnionFind.v.beautified: lib/UnionFind.v lib/Coqlib.vo -lib/UnionFind.vio: lib/UnionFind.v lib/Coqlib.vio -lib/Wfsimpl.vo lib/Wfsimpl.glob lib/Wfsimpl.v.beautified: lib/Wfsimpl.v lib/Axioms.vo -lib/Wfsimpl.vio: lib/Wfsimpl.v lib/Axioms.vio -lib/Postorder.vo lib/Postorder.glob lib/Postorder.v.beautified: lib/Postorder.v lib/Coqlib.vo lib/Maps.vo lib/Iteration.vo -lib/Postorder.vio: lib/Postorder.v lib/Coqlib.vio lib/Maps.vio lib/Iteration.vio -lib/FSetAVLplus.vo lib/FSetAVLplus.glob lib/FSetAVLplus.v.beautified: lib/FSetAVLplus.v lib/Coqlib.vo -lib/FSetAVLplus.vio: lib/FSetAVLplus.v lib/Coqlib.vio -lib/IntvSets.vo lib/IntvSets.glob lib/IntvSets.v.beautified: lib/IntvSets.v lib/Coqlib.vo -lib/IntvSets.vio: lib/IntvSets.v lib/Coqlib.vio -lib/Decidableplus.vo lib/Decidableplus.glob lib/Decidableplus.v.beautified: lib/Decidableplus.v lib/Coqlib.vo -lib/Decidableplus.vio: lib/Decidableplus.v lib/Coqlib.vio -common/Errors.vo common/Errors.glob common/Errors.v.beautified: common/Errors.v lib/Coqlib.vo -common/Errors.vio: common/Errors.v lib/Coqlib.vio -common/AST.vo common/AST.glob common/AST.v.beautified: common/AST.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Archi.vo -common/AST.vio: common/AST.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio $(ARCH)/Archi.vio -common/Linking.vo common/Linking.glob common/Linking.v.beautified: common/Linking.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo -common/Linking.vio: common/Linking.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio common/AST.vio -common/Events.vo common/Events.glob common/Events.v.beautified: 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/Events.vio: common/Events.v lib/Coqlib.vio lib/Intv.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio -common/Globalenvs.vo common/Globalenvs.glob common/Globalenvs.v.beautified: common/Globalenvs.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo common/Linking.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo -common/Globalenvs.vio: common/Globalenvs.v lib/Axioms.vio lib/Coqlib.vio common/Errors.vio lib/Maps.vio common/AST.vio common/Linking.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio -common/Memdata.vo common/Memdata.glob common/Memdata.v.beautified: common/Memdata.v lib/Coqlib.vo $(ARCH)/Archi.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo -common/Memdata.vio: common/Memdata.v lib/Coqlib.vio $(ARCH)/Archi.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio -common/Memtype.vo common/Memtype.glob common/Memtype.v.beautified: common/Memtype.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo -common/Memtype.vio: common/Memtype.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memdata.vio -common/Memory.vo common/Memory.glob common/Memory.v.beautified: common/Memory.v lib/Axioms.vo lib/Coqlib.vo lib/Intv.vo lib/Maps.vo $(ARCH)/Archi.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memtype.vo -common/Memory.vio: common/Memory.v lib/Axioms.vio lib/Coqlib.vio lib/Intv.vio lib/Maps.vio $(ARCH)/Archi.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memdata.vio common/Memtype.vio -common/Values.vo common/Values.glob common/Values.v.beautified: common/Values.v $(ARCH)/Archi.vo lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo -common/Values.vio: common/Values.v $(ARCH)/Archi.vio lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio -common/Smallstep.vo common/Smallstep.glob common/Smallstep.v.beautified: common/Smallstep.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo -common/Smallstep.vio: common/Smallstep.v lib/Coqlib.vio common/Events.vio common/Globalenvs.vio lib/Integers.vio -common/Behaviors.vo common/Behaviors.glob common/Behaviors.v.beautified: common/Behaviors.v lib/Coqlib.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo common/Smallstep.vo -common/Behaviors.vio: common/Behaviors.v lib/Coqlib.vio common/Events.vio common/Globalenvs.vio lib/Integers.vio common/Smallstep.vio -common/Switch.vo common/Switch.glob common/Switch.v.beautified: common/Switch.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo common/Values.vo -common/Switch.vio: common/Switch.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio common/Values.vio -common/Determinism.vo common/Determinism.glob common/Determinism.v.beautified: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo -common/Determinism.vio: common/Determinism.v lib/Coqlib.vio common/AST.vio lib/Integers.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio common/Behaviors.vio -common/Unityping.vo common/Unityping.glob common/Unityping.v.beautified: common/Unityping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo -common/Unityping.vio: common/Unityping.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio -common/Separation.vo common/Separation.glob common/Separation.v.beautified: common/Separation.v lib/Coqlib.vo lib/Decidableplus.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo -common/Separation.vio: common/Separation.v lib/Coqlib.vio lib/Decidableplus.vio common/AST.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio -backend/Cminor.vo backend/Cminor.glob backend/Cminor.v.beautified: 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 -backend/Cminor.vio: backend/Cminor.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Events.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Smallstep.vio common/Switch.vio -$(ARCH)/Op.vo $(ARCH)/Op.glob $(ARCH)/Op.v.beautified: $(ARCH)/Op.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 -$(ARCH)/Op.vio: $(ARCH)/Op.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio -backend/CminorSel.vo backend/CminorSel.glob backend/CminorSel.v.beautified: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Events.vo common/Values.vo common/Memory.vo backend/Cminor.vo $(ARCH)/Op.vo common/Globalenvs.vo common/Smallstep.vo -backend/CminorSel.vio: backend/CminorSel.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Events.vio common/Values.vio common/Memory.vio backend/Cminor.vio $(ARCH)/Op.vio common/Globalenvs.vio common/Smallstep.vio -$(ARCH)/SelectOp.vo $(ARCH)/SelectOp.glob $(ARCH)/SelectOp.v.beautified: $(ARCH)/SelectOp.v lib/Coqlib.vo driver/Compopts.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo -$(ARCH)/SelectOp.vio: $(ARCH)/SelectOp.v lib/Coqlib.vio driver/Compopts.vio common/AST.vio lib/Integers.vio lib/Floats.vio $(ARCH)/Op.vio backend/CminorSel.vio -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/SplitLong.vo $(ARCH)/SelectLong.vo -backend/SelectDiv.vio: backend/SelectDiv.v lib/Coqlib.vio driver/Compopts.vio common/AST.vio lib/Integers.vio lib/Floats.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio backend/SplitLong.vio $(ARCH)/SelectLong.vio -backend/SplitLong.vo backend/SplitLong.glob backend/SplitLong.v.beautified: backend/SplitLong.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo -backend/SplitLong.vio: backend/SplitLong.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio -$(ARCH)/SelectLong.vo $(ARCH)/SelectLong.glob $(ARCH)/SelectLong.v.beautified: $(ARCH)/SelectLong.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/SplitLong.vo -$(ARCH)/SelectLong.vio: $(ARCH)/SelectLong.v lib/Coqlib.vio driver/Compopts.vio common/AST.vio lib/Integers.vio lib/Floats.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio backend/SplitLong.vio -backend/Selection.vo backend/Selection.glob backend/Selection.v.beautified: backend/Selection.v lib/Coqlib.vo lib/Maps.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/SplitLong.vo $(ARCH)/SelectLong.vo backend/SelectDiv.vo $(ARCH)/Machregs.vo -backend/Selection.vio: backend/Selection.v lib/Coqlib.vio lib/Maps.vio common/AST.vio common/Errors.vio lib/Integers.vio common/Globalenvs.vio common/Switch.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio backend/SplitLong.vio $(ARCH)/SelectLong.vio backend/SelectDiv.vio $(ARCH)/Machregs.vio -$(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.vio: $(ARCH)/SelectOpproof.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio -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/SplitLong.vo backend/SplitLongproof.vo $(ARCH)/SelectLong.vo $(ARCH)/SelectLongproof.vo backend/SelectDiv.vo -backend/SelectDivproof.vio: backend/SelectDivproof.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio $(ARCH)/SelectOpproof.vio backend/SplitLong.vio backend/SplitLongproof.vio $(ARCH)/SelectLong.vio $(ARCH)/SelectLongproof.vio backend/SelectDiv.vio -backend/SplitLongproof.vo backend/SplitLongproof.glob backend/SplitLongproof.v.beautified: backend/SplitLongproof.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 common/Events.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo $(ARCH)/SelectOpproof.vo backend/SplitLong.vo -backend/SplitLongproof.vio: backend/SplitLongproof.v lib/Coqlib.vio lib/Maps.vio common/AST.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio $(ARCH)/SelectOpproof.vio backend/SplitLong.vio -$(ARCH)/SelectLongproof.vo $(ARCH)/SelectLongproof.glob $(ARCH)/SelectLongproof.v.beautified: $(ARCH)/SelectLongproof.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Errors.vo $(ARCH)/Archi.vo common/AST.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/SplitLong.vo backend/SplitLongproof.vo $(ARCH)/SelectLong.vo -$(ARCH)/SelectLongproof.vio: $(ARCH)/SelectLongproof.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Errors.vio $(ARCH)/Archi.vio common/AST.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio $(ARCH)/SelectOpproof.vio backend/SplitLong.vio backend/SplitLongproof.vio $(ARCH)/SelectLong.vio -backend/Selectionproof.vo backend/Selectionproof.glob backend/Selectionproof.v.beautified: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Linking.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/SplitLong.vo $(ARCH)/SelectLong.vo backend/Selection.vo $(ARCH)/SelectOpproof.vo backend/SelectDivproof.vo backend/SplitLongproof.vo $(ARCH)/SelectLongproof.vo -backend/Selectionproof.vio: backend/Selectionproof.v lib/Coqlib.vio lib/Maps.vio common/AST.vio common/Linking.vio common/Errors.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio common/Switch.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio $(ARCH)/SelectOp.vio backend/SelectDiv.vio backend/SplitLong.vio $(ARCH)/SelectLong.vio backend/Selection.vio $(ARCH)/SelectOpproof.vio backend/SelectDivproof.vio backend/SplitLongproof.vio $(ARCH)/SelectLongproof.vio -backend/Registers.vo backend/Registers.glob backend/Registers.v.beautified: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo common/Values.vo -backend/Registers.vio: backend/Registers.v lib/Coqlib.vio common/AST.vio lib/Maps.vio lib/Ordered.vio common/Values.vio -backend/RTL.vo backend/RTL.glob backend/RTL.v.beautified: 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/RTL.vio: backend/RTL.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Values.vio common/Events.vio common/Memory.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio -backend/RTLgen.vo backend/RTLgen.glob backend/RTLgen.v.beautified: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo -backend/RTLgen.vio: backend/RTLgen.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Switch.vio $(ARCH)/Op.vio backend/Registers.vio backend/CminorSel.vio backend/RTL.vio -backend/RTLgenspec.vo backend/RTLgenspec.glob backend/RTLgenspec.v.beautified: backend/RTLgenspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Switch.vo $(ARCH)/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo backend/RTLgen.vo -backend/RTLgenspec.vio: backend/RTLgenspec.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Switch.vio $(ARCH)/Op.vio backend/Registers.vio backend/CminorSel.vio backend/RTL.vio backend/RTLgen.vio -backend/RTLgenproof.vo backend/RTLgenproof.glob backend/RTLgenproof.v.beautified: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Linking.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/RTLgenproof.vio: backend/RTLgenproof.v lib/Coqlib.vio lib/Maps.vio common/AST.vio common/Linking.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Events.vio common/Smallstep.vio common/Globalenvs.vio common/Switch.vio backend/Registers.vio backend/Cminor.vio $(ARCH)/Op.vio backend/CminorSel.vio backend/RTL.vio backend/RTLgen.vio backend/RTLgenspec.vio common/Errors.vio -backend/Tailcall.vo backend/Tailcall.glob backend/Tailcall.v.beautified: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo -backend/Tailcall.vio: backend/Tailcall.v lib/Coqlib.vio lib/Maps.vio common/AST.vio backend/Registers.vio $(ARCH)/Op.vio backend/RTL.vio backend/Conventions.vio -backend/Tailcallproof.vo backend/Tailcallproof.glob backend/Tailcallproof.v.beautified: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo common/AST.vo common/Linking.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/Conventions.vo backend/Tailcall.vo -backend/Tailcallproof.vio: backend/Tailcallproof.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Conventions.vio backend/Tailcall.vio -backend/Inlining.vo backend/Inlining.glob backend/Inlining.v.beautified: backend/Inlining.v lib/Coqlib.vo lib/Wfsimpl.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo common/Linking.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo -backend/Inlining.vio: backend/Inlining.v lib/Coqlib.vio lib/Wfsimpl.vio lib/Maps.vio common/Errors.vio lib/Integers.vio common/AST.vio common/Linking.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio -backend/Inliningspec.vo backend/Inliningspec.glob backend/Inliningspec.v.beautified: backend/Inliningspec.v lib/Coqlib.vo lib/Wfsimpl.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo common/Linking.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Inlining.vo -backend/Inliningspec.vio: backend/Inliningspec.v lib/Coqlib.vio lib/Wfsimpl.vio lib/Maps.vio common/Errors.vio lib/Integers.vio common/AST.vio common/Linking.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Inlining.vio -backend/Inliningproof.vo backend/Inliningproof.glob backend/Inliningproof.v.beautified: backend/Inliningproof.v lib/Coqlib.vo lib/Wfsimpl.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo common/Linking.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/Inlining.vo backend/Inliningspec.vo -backend/Inliningproof.vio: backend/Inliningproof.v lib/Coqlib.vio lib/Wfsimpl.vio lib/Maps.vio common/Errors.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Inlining.vio backend/Inliningspec.vio -backend/Renumber.vo backend/Renumber.glob backend/Renumber.v.beautified: backend/Renumber.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo backend/RTL.vo -backend/Renumber.vio: backend/Renumber.v lib/Coqlib.vio lib/Maps.vio lib/Postorder.vio backend/RTL.vio -backend/Renumberproof.vo backend/Renumberproof.glob backend/Renumberproof.v.beautified: backend/Renumberproof.v lib/Coqlib.vo lib/Maps.vo lib/Postorder.vo common/AST.vo common/Linking.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/Renumber.vo -backend/Renumberproof.vio: backend/Renumberproof.v lib/Coqlib.vio lib/Maps.vio lib/Postorder.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Renumber.vio -backend/RTLtyping.vo backend/RTLtyping.glob backend/RTLtyping.v.beautified: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo common/Unityping.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo lib/Integers.vo common/Memory.vo common/Events.vo backend/RTL.vo backend/Conventions.vo -backend/RTLtyping.vio: backend/RTLtyping.v lib/Coqlib.vio common/Errors.vio common/Unityping.vio lib/Maps.vio common/AST.vio $(ARCH)/Op.vio backend/Registers.vio common/Globalenvs.vio common/Values.vio lib/Integers.vio common/Memory.vio common/Events.vio backend/RTL.vio backend/Conventions.vio -backend/Kildall.vo backend/Kildall.glob backend/Kildall.v.beautified: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo -backend/Kildall.vio: backend/Kildall.v lib/Coqlib.vio lib/Iteration.vio lib/Maps.vio lib/Lattice.vio lib/Heaps.vio -backend/Liveness.vo backend/Liveness.glob backend/Liveness.v.beautified: backend/Liveness.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Kildall.vo -backend/Liveness.vio: backend/Liveness.v lib/Coqlib.vio lib/Maps.vio lib/Lattice.vio common/AST.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Kildall.vio -backend/ValueDomain.vo backend/ValueDomain.glob backend/ValueDomain.v.beautified: backend/ValueDomain.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo driver/Compopts.vo common/AST.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Registers.vo backend/RTL.vo -backend/ValueDomain.vio: backend/ValueDomain.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio driver/Compopts.vio common/AST.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio backend/Registers.vio backend/RTL.vio -$(ARCH)/ValueAOp.vo $(ARCH)/ValueAOp.glob $(ARCH)/ValueAOp.v.beautified: $(ARCH)/ValueAOp.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 $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo -$(ARCH)/ValueAOp.vio: $(ARCH)/ValueAOp.v lib/Coqlib.vio driver/Compopts.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio $(ARCH)/Op.vio backend/RTL.vio backend/ValueDomain.vio -backend/ValueAnalysis.vo backend/ValueAnalysis.glob backend/ValueAnalysis.v.beautified: backend/ValueAnalysis.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo driver/Compopts.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/Liveness.vo lib/Axioms.vo -backend/ValueAnalysis.vio: backend/ValueAnalysis.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio driver/Compopts.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio backend/Registers.vio $(ARCH)/Op.vio backend/RTL.vio backend/ValueDomain.vio $(ARCH)/ValueAOp.vio backend/Liveness.vio lib/Axioms.vio -$(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 -$(ARCH)/ConstpropOp.vio: $(ARCH)/ConstpropOp.v lib/Coqlib.vio driver/Compopts.vio common/AST.vio lib/Integers.vio lib/Floats.vio $(ARCH)/Op.vio backend/Registers.vio backend/ValueDomain.vio -backend/Constprop.vo backend/Constprop.glob backend/Constprop.v.beautified: backend/Constprop.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.vo driver/Compopts.vo $(ARCH)/Machregs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Liveness.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo -backend/Constprop.vio: backend/Constprop.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio driver/Compopts.vio $(ARCH)/Machregs.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Liveness.vio backend/ValueDomain.vio $(ARCH)/ValueAOp.vio backend/ValueAnalysis.vio $(ARCH)/ConstpropOp.vio -$(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.vio: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vio driver/Compopts.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/ValueDomain.vio $(ARCH)/ConstpropOp.vio -backend/Constpropproof.vo backend/Constpropproof.glob backend/Constpropproof.v.beautified: backend/Constpropproof.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo driver/Compopts.vo $(ARCH)/Machregs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Liveness.vo backend/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo $(ARCH)/ConstpropOp.vo $(ARCH)/ConstpropOpproof.vo backend/Constprop.vo -backend/Constpropproof.vio: backend/Constpropproof.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio common/Values.vio common/Events.vio common/Memory.vio common/Globalenvs.vio common/Smallstep.vio driver/Compopts.vio $(ARCH)/Machregs.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Liveness.vio backend/ValueDomain.vio $(ARCH)/ValueAOp.vio backend/ValueAnalysis.vio $(ARCH)/ConstpropOp.vio $(ARCH)/ConstpropOpproof.vio backend/Constprop.vio -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 -backend/CSEdomain.vio: backend/CSEdomain.v lib/Coqlib.vio lib/Maps.vio common/AST.vio common/Values.vio common/Memory.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio -$(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 -$(ARCH)/CombineOp.vio: $(ARCH)/CombineOp.v lib/Coqlib.vio common/AST.vio lib/Integers.vio $(ARCH)/Op.vio backend/CSEdomain.vio -backend/CSE.vo backend/CSE.glob backend/CSE.v.beautified: backend/CSE.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.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 $(ARCH)/CombineOp.vo -backend/CSE.vio: backend/CSE.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/ValueDomain.vio backend/ValueAnalysis.vio backend/CSEdomain.vio $(ARCH)/CombineOp.vio -$(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.vio: $(ARCH)/CombineOpproof.v lib/Coqlib.vio lib/Integers.vio common/Values.vio common/Memory.vio $(ARCH)/Op.vio backend/RTL.vio backend/CSEdomain.vio $(ARCH)/CombineOp.vio -backend/CSEproof.vo backend/CSEproof.glob backend/CSEproof.v.beautified: backend/CSEproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.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/ValueDomain.vo $(ARCH)/ValueAOp.vo backend/ValueAnalysis.vo backend/CSEdomain.vo $(ARCH)/CombineOp.vo $(ARCH)/CombineOpproof.vo backend/CSE.vo -backend/CSEproof.vio: backend/CSEproof.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/ValueDomain.vio $(ARCH)/ValueAOp.vio backend/ValueAnalysis.vio backend/CSEdomain.vio $(ARCH)/CombineOp.vio $(ARCH)/CombineOpproof.vio backend/CSE.vio -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 -backend/NeedDomain.vio: backend/NeedDomain.v lib/Coqlib.vio lib/Maps.vio lib/IntvSets.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio lib/Lattice.vio backend/Registers.vio backend/ValueDomain.vio $(ARCH)/Op.vio backend/RTL.vio -$(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 -$(ARCH)/NeedOp.vio: $(ARCH)/NeedOp.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio $(ARCH)/Op.vio backend/NeedDomain.vio backend/RTL.vio -backend/Deadcode.vo backend/Deadcode.glob backend/Deadcode.v.beautified: backend/Deadcode.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.vo common/Memory.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo -backend/Deadcode.vio: backend/Deadcode.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio common/Memory.vio backend/Registers.vio $(ARCH)/Op.vio backend/RTL.vio backend/ValueDomain.vio backend/ValueAnalysis.vio backend/NeedDomain.vio $(ARCH)/NeedOp.vio -backend/Deadcodeproof.vo backend/Deadcodeproof.glob backend/Deadcodeproof.v.beautified: backend/Deadcodeproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/ValueDomain.vo backend/ValueAnalysis.vo backend/NeedDomain.vo $(ARCH)/NeedOp.vo backend/Deadcode.vo -backend/Deadcodeproof.vio: backend/Deadcodeproof.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio backend/Registers.vio $(ARCH)/Op.vio backend/RTL.vio backend/ValueDomain.vio backend/ValueAnalysis.vio backend/NeedDomain.vio $(ARCH)/NeedOp.vio backend/Deadcode.vio -backend/Unusedglob.vo backend/Unusedglob.glob backend/Unusedglob.v.beautified: backend/Unusedglob.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo lib/Iteration.vo common/Errors.vo common/AST.vo common/Linking.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo -backend/Unusedglob.vio: backend/Unusedglob.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio lib/Iteration.vio common/Errors.vio common/AST.vio common/Linking.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio -backend/Unusedglobproof.vo backend/Unusedglobproof.glob backend/Unusedglobproof.v.beautified: backend/Unusedglobproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo lib/Iteration.vo common/Errors.vo common/AST.vo common/Linking.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 -backend/Unusedglobproof.vio: backend/Unusedglobproof.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio lib/Iteration.vio common/Errors.vio common/AST.vio common/Linking.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Unusedglob.vio -$(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Decidableplus.vo lib/Maps.vo common/AST.vo lib/Integers.vo $(ARCH)/Op.vo -$(ARCH)/Machregs.vio: $(ARCH)/Machregs.v lib/Coqlib.vio lib/Decidableplus.vio lib/Maps.vio common/AST.vio lib/Integers.vio $(ARCH)/Op.vio -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 -backend/Locations.vio: backend/Locations.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio common/AST.vio common/Values.vio $(ARCH)/Machregs.vio -$(ARCH)/Conventions1.vo $(ARCH)/Conventions1.glob $(ARCH)/Conventions1.v.beautified: $(ARCH)/Conventions1.v lib/Coqlib.vo lib/Decidableplus.vo common/AST.vo $(ARCH)/Machregs.vo backend/Locations.vo -$(ARCH)/Conventions1.vio: $(ARCH)/Conventions1.v lib/Coqlib.vio lib/Decidableplus.vio common/AST.vio $(ARCH)/Machregs.vio backend/Locations.vio -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/Conventions.vio: backend/Conventions.v lib/Coqlib.vio common/AST.vio backend/Locations.vio $(ARCH)/Conventions1.vio -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/LTL.vio: backend/LTL.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Values.vio common/Events.vio common/Memory.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/Conventions.vio -backend/Allocation.vo backend/Allocation.glob backend/Allocation.v.beautified: backend/Allocation.v lib/FSetAVLplus.vo lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo lib/Lattice.vo backend/Kildall.vo common/Memdata.vo $(ARCH)/Archi.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo -backend/Allocation.vio: backend/Allocation.v lib/FSetAVLplus.vio lib/Coqlib.vio lib/Ordered.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio lib/Lattice.vio backend/Kildall.vio common/Memdata.vio $(ARCH)/Archi.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Locations.vio backend/Conventions.vio backend/RTLtyping.vio backend/LTL.vio -backend/Allocproof.vo backend/Allocproof.glob backend/Allocproof.v.beautified: backend/Allocproof.v lib/Coqlib.vo lib/Ordered.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo lib/Lattice.vo backend/Kildall.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Archi.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/Conventions.vo backend/RTLtyping.vo backend/LTL.vo backend/Allocation.vo -backend/Allocproof.vio: backend/Allocproof.v lib/Coqlib.vio lib/Ordered.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio lib/Lattice.vio backend/Kildall.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio $(ARCH)/Archi.vio $(ARCH)/Op.vio backend/Registers.vio backend/RTL.vio backend/Locations.vio backend/Conventions.vio backend/RTLtyping.vio backend/LTL.vio backend/Allocation.vio -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/Tunneling.vio: backend/Tunneling.v lib/Coqlib.vio lib/Maps.vio lib/UnionFind.vio common/AST.vio backend/LTL.vio -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/Linking.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/Tunnelingproof.vio: backend/Tunnelingproof.v lib/Coqlib.vio lib/Maps.vio lib/UnionFind.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/LTL.vio backend/Tunneling.vio -backend/Linear.vo backend/Linear.glob backend/Linear.v.beautified: backend/Linear.v lib/Coqlib.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/Linear.vio: backend/Linear.v lib/Coqlib.vio common/AST.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/LTL.vio backend/Conventions.vio -backend/Lineartyping.vo backend/Lineartyping.glob backend/Lineartyping.v.beautified: backend/Lineartyping.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo common/Memory.vo common/Events.vo $(ARCH)/Op.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Conventions.vo backend/LTL.vo backend/Linear.vo -backend/Lineartyping.vio: backend/Lineartyping.v lib/Coqlib.vio common/AST.vio lib/Integers.vio common/Values.vio common/Globalenvs.vio common/Memory.vio common/Events.vio $(ARCH)/Op.vio $(ARCH)/Machregs.vio backend/Locations.vio backend/Conventions.vio backend/LTL.vio backend/Linear.vio -backend/Linearize.vo backend/Linearize.glob backend/Linearize.v.beautified: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/Errors.vo lib/Lattice.vo backend/Kildall.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo -backend/Linearize.vio: backend/Linearize.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio common/Errors.vio lib/Lattice.vio backend/Kildall.vio common/AST.vio $(ARCH)/Op.vio backend/Locations.vio backend/LTL.vio backend/Linear.vio -backend/Linearizeproof.vo backend/Linearizeproof.glob backend/Linearizeproof.v.beautified: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/Errors.vo lib/Lattice.vo backend/Kildall.vo lib/Integers.vo common/AST.vo common/Linking.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/Linear.vo backend/Linearize.vo -backend/Linearizeproof.vio: backend/Linearizeproof.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio common/Errors.vio lib/Lattice.vio backend/Kildall.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/LTL.vio backend/Linear.vio backend/Linearize.vio -backend/CleanupLabels.vo backend/CleanupLabels.glob backend/CleanupLabels.v.beautified: backend/CleanupLabels.v lib/Coqlib.vo lib/Ordered.vo backend/Linear.vo -backend/CleanupLabels.vio: backend/CleanupLabels.v lib/Coqlib.vio lib/Ordered.vio backend/Linear.vio -backend/CleanupLabelsproof.vo backend/CleanupLabelsproof.glob backend/CleanupLabelsproof.v.beautified: backend/CleanupLabelsproof.v lib/Coqlib.vo lib/Ordered.vo lib/Integers.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/CleanupLabels.vo -backend/CleanupLabelsproof.vio: backend/CleanupLabelsproof.v lib/Coqlib.vio lib/Ordered.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/Linear.vio backend/CleanupLabels.vio -backend/Debugvar.vo backend/Debugvar.glob backend/Debugvar.v.beautified: backend/Debugvar.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo lib/Iteration.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Conventions.vo backend/Linear.vo -backend/Debugvar.vio: backend/Debugvar.v lib/Axioms.vio lib/Coqlib.vio lib/Maps.vio lib/Iteration.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio $(ARCH)/Machregs.vio backend/Locations.vio backend/Conventions.vio backend/Linear.vio -backend/Debugvarproof.vo backend/Debugvarproof.glob backend/Debugvarproof.v.beautified: backend/Debugvarproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo lib/Iteration.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Conventions.vo $(ARCH)/Op.vo backend/Linear.vo backend/Debugvar.vo -backend/Debugvarproof.vio: backend/Debugvarproof.v lib/Axioms.vio lib/Coqlib.vio lib/Maps.vio lib/Iteration.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Machregs.vio backend/Locations.vio backend/Conventions.vio $(ARCH)/Op.vio backend/Linear.vio backend/Debugvar.vio -backend/Mach.vo backend/Mach.glob backend/Mach.v.beautified: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo -backend/Mach.vio: backend/Mach.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/Conventions.vio $(ARCH)/Stacklayout.vio -backend/Bounds.vo backend/Bounds.glob backend/Bounds.v.beautified: backend/Bounds.v lib/Coqlib.vo lib/Ordered.vo lib/Intv.vo common/AST.vo $(ARCH)/Op.vo $(ARCH)/Machregs.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo -backend/Bounds.vio: backend/Bounds.v lib/Coqlib.vio lib/Ordered.vio lib/Intv.vio common/AST.vio $(ARCH)/Op.vio $(ARCH)/Machregs.vio backend/Locations.vio backend/Linear.vio backend/Conventions.vio -$(ARCH)/Stacklayout.vo $(ARCH)/Stacklayout.glob $(ARCH)/Stacklayout.v.beautified: $(ARCH)/Stacklayout.v lib/Coqlib.vo common/AST.vo common/Memory.vo common/Separation.vo backend/Bounds.vo -$(ARCH)/Stacklayout.vio: $(ARCH)/Stacklayout.v lib/Coqlib.vio common/AST.vio common/Memory.vio common/Separation.vio backend/Bounds.vio -backend/Stacking.vo backend/Stacking.glob backend/Stacking.v.beautified: backend/Stacking.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo common/AST.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo backend/Lineartyping.vo -backend/Stacking.vio: backend/Stacking.v lib/Coqlib.vio common/Errors.vio lib/Integers.vio common/AST.vio $(ARCH)/Op.vio backend/Locations.vio backend/Linear.vio backend/Mach.vio backend/Bounds.vio backend/Conventions.vio $(ARCH)/Stacklayout.vio backend/Lineartyping.vio -backend/Stackingproof.vo backend/Stackingproof.glob backend/Stackingproof.v.beautified: backend/Stackingproof.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Separation.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/LTL.vo $(ARCH)/Op.vo backend/Locations.vo backend/Linear.vo backend/Mach.vo backend/Bounds.vo backend/Conventions.vo $(ARCH)/Stacklayout.vo backend/Lineartyping.vo backend/Stacking.vo -backend/Stackingproof.vio: backend/Stackingproof.v lib/Coqlib.vio common/Errors.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Separation.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio backend/LTL.vio $(ARCH)/Op.vio backend/Locations.vio backend/Linear.vio backend/Mach.vio backend/Bounds.vio backend/Conventions.vio $(ARCH)/Stacklayout.vio backend/Lineartyping.vio backend/Stacking.vio -$(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)/Asm.vio: $(ARCH)/Asm.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio backend/Locations.vio $(ARCH)/Stacklayout.vio backend/Conventions.vio -$(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.vio: $(ARCH)/Asmgen.v lib/Coqlib.vio common/Errors.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Memdata.vio $(ARCH)/Op.vio backend/Locations.vio backend/Mach.vio $(ARCH)/Asm.vio -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 -backend/Asmgenproof0.vio: backend/Asmgenproof0.v lib/Coqlib.vio lib/Intv.vio common/AST.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio backend/Locations.vio backend/Mach.vio $(ARCH)/Asm.vio $(ARCH)/Asmgen.vio backend/Conventions.vio -$(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/Conventions.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo -$(ARCH)/Asmgenproof1.vio: $(ARCH)/Asmgenproof1.v lib/Coqlib.vio common/AST.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Globalenvs.vio $(ARCH)/Op.vio backend/Locations.vio backend/Conventions.vio backend/Mach.vio $(ARCH)/Asm.vio $(ARCH)/Asmgen.vio backend/Asmgenproof0.vio -$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob $(ARCH)/Asmgenproof.v.beautified: $(ARCH)/Asmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.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)/Asmgenproof.vio: $(ARCH)/Asmgenproof.v lib/Coqlib.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio $(ARCH)/Op.vio backend/Locations.vio backend/Mach.vio backend/Conventions.vio $(ARCH)/Asm.vio $(ARCH)/Asmgen.vio backend/Asmgenproof0.vio $(ARCH)/Asmgenproof1.vio -cfrontend/Ctypes.vo cfrontend/Ctypes.glob cfrontend/Ctypes.v.beautified: cfrontend/Ctypes.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Linking.vo $(ARCH)/Archi.vo -cfrontend/Ctypes.vio: cfrontend/Ctypes.v lib/Axioms.vio lib/Coqlib.vio lib/Maps.vio common/Errors.vio common/AST.vio common/Linking.vio $(ARCH)/Archi.vio -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 $(ARCH)/Archi.vo -cfrontend/Cop.vio: cfrontend/Cop.v lib/Coqlib.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio cfrontend/Ctypes.vio $(ARCH)/Archi.vio -cfrontend/Csyntax.vo cfrontend/Csyntax.glob cfrontend/Csyntax.v.beautified: cfrontend/Csyntax.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Errors.vo common/AST.vo common/Linking.vo common/Values.vo cfrontend/Ctypes.vo cfrontend/Cop.vo -cfrontend/Csyntax.vio: cfrontend/Csyntax.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Errors.vio common/AST.vio common/Linking.vio common/Values.vio cfrontend/Ctypes.vio cfrontend/Cop.vio -cfrontend/Csem.vo cfrontend/Csem.glob cfrontend/Csem.v.beautified: 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/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo common/Smallstep.vo -cfrontend/Csem.vio: cfrontend/Csem.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Events.vio common/Globalenvs.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio common/Smallstep.vio -cfrontend/Ctyping.vo cfrontend/Ctyping.glob cfrontend/Ctyping.v.beautified: cfrontend/Ctyping.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Errors.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo -cfrontend/Ctyping.vio: cfrontend/Ctyping.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Errors.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio -cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob cfrontend/Cstrategy.v.beautified: 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 cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo -cfrontend/Cstrategy.vio: cfrontend/Cstrategy.v lib/Axioms.vio lib/Coqlib.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio -cfrontend/Cexec.vo cfrontend/Cexec.glob cfrontend/Cexec.v.beautified: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo lib/Decidableplus.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.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/Cexec.vio: cfrontend/Cexec.v lib/Axioms.vio lib/Coqlib.vio lib/Decidableplus.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Determinism.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cstrategy.vio -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/Initializers.vio: cfrontend/Initializers.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Globalenvs.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio -cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob cfrontend/Initializersproof.v.beautified: cfrontend/Initializersproof.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 common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo -cfrontend/Initializersproof.vio: cfrontend/Initializersproof.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Initializers.vio -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/SimplExpr.vio: cfrontend/SimplExpr.v lib/Coqlib.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/AST.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Clight.vio -cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob cfrontend/SimplExprspec.v.beautified: cfrontend/SimplExprspec.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo common/Memory.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo -cfrontend/SimplExprspec.vio: cfrontend/SimplExprspec.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio common/Memory.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Clight.vio cfrontend/SimplExpr.vio -cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob cfrontend/SimplExprproof.v.beautified: cfrontend/SimplExprproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.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/SimplExprproof.vio: cfrontend/SimplExprproof.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cstrategy.vio cfrontend/Clight.vio cfrontend/SimplExpr.vio cfrontend/SimplExprspec.vio -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 -cfrontend/Clight.vio: cfrontend/Clight.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio -cfrontend/ClightBigstep.vo cfrontend/ClightBigstep.glob cfrontend/ClightBigstep.v.beautified: cfrontend/ClightBigstep.v lib/Coqlib.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 cfrontend/Clight.vo -cfrontend/ClightBigstep.vio: cfrontend/ClightBigstep.v lib/Coqlib.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/AST.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio -cfrontend/SimplLocals.vo cfrontend/SimplLocals.glob cfrontend/SimplLocals.v.beautified: cfrontend/SimplLocals.v lib/Coqlib.vo lib/Ordered.vo common/Errors.vo common/AST.vo common/Linking.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo driver/Compopts.vo -cfrontend/SimplLocals.vio: cfrontend/SimplLocals.v lib/Coqlib.vio lib/Ordered.vio common/Errors.vio common/AST.vio common/Linking.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio driver/Compopts.vio -cfrontend/SimplLocalsproof.vo cfrontend/SimplLocalsproof.glob cfrontend/SimplLocalsproof.v.beautified: cfrontend/SimplLocalsproof.v lib/Coqlib.vo common/Errors.vo lib/Ordered.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo cfrontend/SimplLocals.vo -cfrontend/SimplLocalsproof.vio: cfrontend/SimplLocalsproof.v lib/Coqlib.vio common/Errors.vio lib/Ordered.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Globalenvs.vio common/Events.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio cfrontend/SimplLocals.vio -cfrontend/Cshmgen.vo cfrontend/Cshmgen.glob cfrontend/Cshmgen.v.beautified: cfrontend/Cshmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo -cfrontend/Cshmgen.vio: cfrontend/Cshmgen.v lib/Coqlib.vio lib/Maps.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio backend/Cminor.vio cfrontend/Csharpminor.vio -cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob cfrontend/Cshmgenproof.v.beautified: cfrontend/Cshmgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo backend/Cminor.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo -cfrontend/Cshmgenproof.vio: cfrontend/Cshmgenproof.v lib/Coqlib.vio common/Errors.vio lib/Maps.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio common/Values.vio common/Events.vio common/Memory.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio backend/Cminor.vio cfrontend/Csharpminor.vio cfrontend/Cshmgen.vio -cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob cfrontend/Csharpminor.v.beautified: 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 common/Switch.vo backend/Cminor.vo common/Smallstep.vo -cfrontend/Csharpminor.vio: cfrontend/Csharpminor.v lib/Coqlib.vio lib/Maps.vio common/AST.vio lib/Integers.vio lib/Floats.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Switch.vio backend/Cminor.vio common/Smallstep.vio -cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob cfrontend/Cminorgen.v.beautified: cfrontend/Cminorgen.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Linking.vo cfrontend/Csharpminor.vo backend/Cminor.vo -cfrontend/Cminorgen.vio: cfrontend/Cminorgen.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio common/Errors.vio lib/Integers.vio lib/Floats.vio common/AST.vio common/Linking.vio cfrontend/Csharpminor.vio backend/Cminor.vio -cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob cfrontend/Cminorgenproof.v.beautified: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/Errors.vo lib/Integers.vo lib/Floats.vo lib/Intv.vo common/AST.vo common/Linking.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csharpminor.vo common/Switch.vo backend/Cminor.vo cfrontend/Cminorgen.vo -cfrontend/Cminorgenproof.vio: cfrontend/Cminorgenproof.v lib/Coqlib.vio lib/Maps.vio lib/Ordered.vio common/Errors.vio lib/Integers.vio lib/Floats.vio lib/Intv.vio common/AST.vio common/Linking.vio common/Values.vio common/Memory.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio cfrontend/Csharpminor.vio common/Switch.vio backend/Cminor.vio cfrontend/Cminorgen.vio -driver/Compopts.vo driver/Compopts.glob driver/Compopts.v.beautified: driver/Compopts.v -driver/Compopts.vio: driver/Compopts.v -driver/Compiler.vo driver/Compiler.glob driver/Compiler.v.beautified: driver/Compiler.v lib/Coqlib.vo common/Errors.vo common/AST.vo common/Linking.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/Linear.vo backend/Mach.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/SimplLocals.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/Inlining.vo backend/Renumber.vo backend/Constprop.vo backend/CSE.vo backend/Deadcode.vo backend/Unusedglob.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Debugvar.vo backend/Stacking.vo $(ARCH)/Asmgen.vo cfrontend/SimplExprproof.vo cfrontend/SimplLocalsproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/Inliningproof.vo backend/Renumberproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Deadcodeproof.vo backend/Unusedglobproof.vo backend/Allocproof.vo backend/Tunnelingproof.vo backend/Linearizeproof.vo backend/CleanupLabelsproof.vo backend/Debugvarproof.vo backend/Stackingproof.vo $(ARCH)/Asmgenproof.vo driver/Compopts.vo -driver/Compiler.vio: driver/Compiler.v lib/Coqlib.vio common/Errors.vio common/AST.vio common/Linking.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cstrategy.vio cfrontend/Cexec.vio cfrontend/Clight.vio cfrontend/Csharpminor.vio backend/Cminor.vio backend/CminorSel.vio backend/RTL.vio backend/LTL.vio backend/Linear.vio backend/Mach.vio $(ARCH)/Asm.vio cfrontend/Initializers.vio cfrontend/SimplExpr.vio cfrontend/SimplLocals.vio cfrontend/Cshmgen.vio cfrontend/Cminorgen.vio backend/Selection.vio backend/RTLgen.vio backend/Tailcall.vio backend/Inlining.vio backend/Renumber.vio backend/Constprop.vio backend/CSE.vio backend/Deadcode.vio backend/Unusedglob.vio backend/Allocation.vio backend/Tunneling.vio backend/Linearize.vio backend/CleanupLabels.vio backend/Debugvar.vio backend/Stacking.vio $(ARCH)/Asmgen.vio cfrontend/SimplExprproof.vio cfrontend/SimplLocalsproof.vio cfrontend/Cshmgenproof.vio cfrontend/Cminorgenproof.vio backend/Selectionproof.vio backend/RTLgenproof.vio backend/Tailcallproof.vio backend/Inliningproof.vio backend/Renumberproof.vio backend/Constpropproof.vio backend/CSEproof.vio backend/Deadcodeproof.vio backend/Unusedglobproof.vio backend/Allocproof.vio backend/Tunnelingproof.vio backend/Linearizeproof.vio backend/CleanupLabelsproof.vio backend/Debugvarproof.vio backend/Stackingproof.vio $(ARCH)/Asmgenproof.vio driver/Compopts.vio -driver/Complements.vo driver/Complements.glob driver/Complements.v.beautified: 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/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo -driver/Complements.vio: driver/Complements.v lib/Coqlib.vio common/AST.vio lib/Integers.vio common/Values.vio common/Events.vio common/Globalenvs.vio common/Smallstep.vio common/Behaviors.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cstrategy.vio cfrontend/Clight.vio backend/Cminor.vio backend/RTL.vio $(ARCH)/Asm.vio driver/Compiler.vio common/Errors.vio -flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_Raux.glob flocq/Core/Fcore_Raux.v.beautified: flocq/Core/Fcore_Raux.v flocq/Core/Fcore_Zaux.vo -flocq/Core/Fcore_Raux.vio: flocq/Core/Fcore_Raux.v flocq/Core/Fcore_Zaux.vio -flocq/Core/Fcore_Zaux.vo flocq/Core/Fcore_Zaux.glob flocq/Core/Fcore_Zaux.v.beautified: flocq/Core/Fcore_Zaux.v -flocq/Core/Fcore_Zaux.vio: flocq/Core/Fcore_Zaux.v -flocq/Core/Fcore_defs.vo flocq/Core/Fcore_defs.glob flocq/Core/Fcore_defs.v.beautified: flocq/Core/Fcore_defs.v flocq/Core/Fcore_Raux.vo -flocq/Core/Fcore_defs.vio: flocq/Core/Fcore_defs.v flocq/Core/Fcore_Raux.vio -flocq/Core/Fcore_digits.vo flocq/Core/Fcore_digits.glob flocq/Core/Fcore_digits.v.beautified: flocq/Core/Fcore_digits.v flocq/Core/Fcore_Zaux.vo -flocq/Core/Fcore_digits.vio: flocq/Core/Fcore_digits.v flocq/Core/Fcore_Zaux.vio -flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_float_prop.glob flocq/Core/Fcore_float_prop.v.beautified: flocq/Core/Fcore_float_prop.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo -flocq/Core/Fcore_float_prop.vio: flocq/Core/Fcore_float_prop.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio -flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_FIX.glob flocq/Core/Fcore_FIX.v.beautified: flocq/Core/Fcore_FIX.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_rnd_ne.vo -flocq/Core/Fcore_FIX.vio: flocq/Core/Fcore_FIX.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_rnd_ne.vio -flocq/Core/Fcore_FLT.vo flocq/Core/Fcore_FLT.glob flocq/Core/Fcore_FLT.v.beautified: flocq/Core/Fcore_FLT.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_rnd_ne.vo -flocq/Core/Fcore_FLT.vio: flocq/Core/Fcore_FLT.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_FLX.vio flocq/Core/Fcore_FIX.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_rnd_ne.vio -flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FLX.glob flocq/Core/Fcore_FLX.v.beautified: flocq/Core/Fcore_FLX.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_rnd_ne.vo -flocq/Core/Fcore_FLX.vio: flocq/Core/Fcore_FLX.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_FIX.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_rnd_ne.vio -flocq/Core/Fcore_FTZ.vo flocq/Core/Fcore_FTZ.glob flocq/Core/Fcore_FTZ.v.beautified: flocq/Core/Fcore_FTZ.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_FLX.vo -flocq/Core/Fcore_FTZ.vio: flocq/Core/Fcore_FTZ.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_FLX.vio -flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_generic_fmt.glob flocq/Core/Fcore_generic_fmt.v.beautified: flocq/Core/Fcore_generic_fmt.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_float_prop.vo -flocq/Core/Fcore_generic_fmt.vio: flocq/Core/Fcore_generic_fmt.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_float_prop.vio -flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_rnd.glob flocq/Core/Fcore_rnd.v.beautified: flocq/Core/Fcore_rnd.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo -flocq/Core/Fcore_rnd.vio: flocq/Core/Fcore_rnd.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio -flocq/Core/Fcore_rnd_ne.vo flocq/Core/Fcore_rnd_ne.glob flocq/Core/Fcore_rnd_ne.v.beautified: flocq/Core/Fcore_rnd_ne.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_ulp.vo -flocq/Core/Fcore_rnd_ne.vio: flocq/Core/Fcore_rnd_ne.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_ulp.vio -flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_ulp.glob flocq/Core/Fcore_ulp.v.beautified: flocq/Core/Fcore_ulp.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_float_prop.vo -flocq/Core/Fcore_ulp.vio: flocq/Core/Fcore_ulp.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_float_prop.vio -flocq/Core/Fcore.vo flocq/Core/Fcore.glob flocq/Core/Fcore.v.beautified: flocq/Core/Fcore.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_rnd.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_rnd_ne.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FLT.vo flocq/Core/Fcore_ulp.vo -flocq/Core/Fcore.vio: flocq/Core/Fcore.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_rnd.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_rnd_ne.vio flocq/Core/Fcore_FIX.vio flocq/Core/Fcore_FLX.vio flocq/Core/Fcore_FLT.vio flocq/Core/Fcore_ulp.vio -flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_bracket.glob flocq/Calc/Fcalc_bracket.v.beautified: flocq/Calc/Fcalc_bracket.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo -flocq/Calc/Fcalc_bracket.vio: flocq/Calc/Fcalc_bracket.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio -flocq/Calc/Fcalc_digits.vo flocq/Calc/Fcalc_digits.glob flocq/Calc/Fcalc_digits.v.beautified: flocq/Calc/Fcalc_digits.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_digits.vo -flocq/Calc/Fcalc_digits.vio: flocq/Calc/Fcalc_digits.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_digits.vio -flocq/Calc/Fcalc_div.vo flocq/Calc/Fcalc_div.glob flocq/Calc/Fcalc_div.v.beautified: flocq/Calc/Fcalc_div.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_digits.vo -flocq/Calc/Fcalc_div.vio: flocq/Calc/Fcalc_div.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_bracket.vio flocq/Calc/Fcalc_digits.vio -flocq/Calc/Fcalc_ops.vo flocq/Calc/Fcalc_ops.glob flocq/Calc/Fcalc_ops.v.beautified: flocq/Calc/Fcalc_ops.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo -flocq/Calc/Fcalc_ops.vio: flocq/Calc/Fcalc_ops.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio -flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_round.glob flocq/Calc/Fcalc_round.v.beautified: flocq/Calc/Fcalc_round.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_digits.vo -flocq/Calc/Fcalc_round.vio: flocq/Calc/Fcalc_round.v flocq/Core/Fcore.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_bracket.vio flocq/Calc/Fcalc_digits.vio -flocq/Calc/Fcalc_sqrt.vo flocq/Calc/Fcalc_sqrt.glob flocq/Calc/Fcalc_sqrt.v.beautified: flocq/Calc/Fcalc_sqrt.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_digits.vo flocq/Core/Fcore_float_prop.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_digits.vo -flocq/Calc/Fcalc_sqrt.vio: flocq/Calc/Fcalc_sqrt.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_digits.vio flocq/Core/Fcore_float_prop.vio flocq/Calc/Fcalc_bracket.vio flocq/Calc/Fcalc_digits.vio -flocq/Prop/Fprop_div_sqrt_error.vo flocq/Prop/Fprop_div_sqrt_error.glob flocq/Prop/Fprop_div_sqrt_error.v.beautified: flocq/Prop/Fprop_div_sqrt_error.v flocq/Core/Fcore.vo flocq/Calc/Fcalc_ops.vo flocq/Prop/Fprop_relative.vo -flocq/Prop/Fprop_div_sqrt_error.vio: flocq/Prop/Fprop_div_sqrt_error.v flocq/Core/Fcore.vio flocq/Calc/Fcalc_ops.vio flocq/Prop/Fprop_relative.vio -flocq/Prop/Fprop_mult_error.vo flocq/Prop/Fprop_mult_error.glob flocq/Prop/Fprop_mult_error.v.beautified: flocq/Prop/Fprop_mult_error.v flocq/Core/Fcore.vo flocq/Calc/Fcalc_ops.vo -flocq/Prop/Fprop_mult_error.vio: flocq/Prop/Fprop_mult_error.v flocq/Core/Fcore.vio flocq/Calc/Fcalc_ops.vio -flocq/Prop/Fprop_plus_error.vo flocq/Prop/Fprop_plus_error.glob flocq/Prop/Fprop_plus_error.v.beautified: flocq/Prop/Fprop_plus_error.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_float_prop.vo flocq/Core/Fcore_generic_fmt.vo flocq/Core/Fcore_FIX.vo flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FLT.vo flocq/Calc/Fcalc_ops.vo -flocq/Prop/Fprop_plus_error.vio: flocq/Prop/Fprop_plus_error.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_float_prop.vio flocq/Core/Fcore_generic_fmt.vio flocq/Core/Fcore_FIX.vio flocq/Core/Fcore_FLX.vio flocq/Core/Fcore_FLT.vio flocq/Calc/Fcalc_ops.vio -flocq/Prop/Fprop_relative.vo flocq/Prop/Fprop_relative.glob flocq/Prop/Fprop_relative.v.beautified: flocq/Prop/Fprop_relative.v flocq/Core/Fcore.vo -flocq/Prop/Fprop_relative.vio: flocq/Prop/Fprop_relative.v flocq/Core/Fcore.vio -flocq/Prop/Fprop_Sterbenz.vo flocq/Prop/Fprop_Sterbenz.glob flocq/Prop/Fprop_Sterbenz.v.beautified: flocq/Prop/Fprop_Sterbenz.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_generic_fmt.vo flocq/Calc/Fcalc_ops.vo -flocq/Prop/Fprop_Sterbenz.vio: flocq/Prop/Fprop_Sterbenz.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_generic_fmt.vio flocq/Calc/Fcalc_ops.vio -flocq/Appli/Fappli_rnd_odd.vo flocq/Appli/Fappli_rnd_odd.glob flocq/Appli/Fappli_rnd_odd.v.beautified: flocq/Appli/Fappli_rnd_odd.v flocq/Core/Fcore.vo flocq/Calc/Fcalc_ops.vo -flocq/Appli/Fappli_rnd_odd.vio: flocq/Appli/Fappli_rnd_odd.v flocq/Core/Fcore.vio flocq/Calc/Fcalc_ops.vio -flocq/Appli/Fappli_double_round.vo flocq/Appli/Fappli_double_round.glob flocq/Appli/Fappli_double_round.v.beautified: flocq/Appli/Fappli_double_round.v flocq/Core/Fcore_Raux.vo flocq/Core/Fcore_defs.vo flocq/Core/Fcore_generic_fmt.vo flocq/Calc/Fcalc_ops.vo flocq/Core/Fcore_ulp.vo flocq/Core/Fcore_FLX.vo flocq/Core/Fcore_FLT.vo flocq/Core/Fcore_FTZ.vo -flocq/Appli/Fappli_double_round.vio: flocq/Appli/Fappli_double_round.v flocq/Core/Fcore_Raux.vio flocq/Core/Fcore_defs.vio flocq/Core/Fcore_generic_fmt.vio flocq/Calc/Fcalc_ops.vio flocq/Core/Fcore_ulp.vio flocq/Core/Fcore_FLX.vio flocq/Core/Fcore_FLT.vio flocq/Core/Fcore_FTZ.vio -flocq/Appli/Fappli_IEEE.vo flocq/Appli/Fappli_IEEE.glob flocq/Appli/Fappli_IEEE.v.beautified: flocq/Appli/Fappli_IEEE.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_digits.vo flocq/Calc/Fcalc_round.vo flocq/Calc/Fcalc_bracket.vo flocq/Calc/Fcalc_ops.vo flocq/Calc/Fcalc_div.vo flocq/Calc/Fcalc_sqrt.vo flocq/Prop/Fprop_relative.vo -flocq/Appli/Fappli_IEEE.vio: flocq/Appli/Fappli_IEEE.v flocq/Core/Fcore.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_digits.vio flocq/Calc/Fcalc_round.vio flocq/Calc/Fcalc_bracket.vio flocq/Calc/Fcalc_ops.vio flocq/Calc/Fcalc_div.vio flocq/Calc/Fcalc_sqrt.vio flocq/Prop/Fprop_relative.vio -flocq/Appli/Fappli_IEEE_bits.vo flocq/Appli/Fappli_IEEE_bits.glob flocq/Appli/Fappli_IEEE_bits.v.beautified: flocq/Appli/Fappli_IEEE_bits.v flocq/Core/Fcore.vo flocq/Core/Fcore_digits.vo flocq/Calc/Fcalc_digits.vo flocq/Appli/Fappli_IEEE.vo -flocq/Appli/Fappli_IEEE_bits.vio: flocq/Appli/Fappli_IEEE_bits.v flocq/Core/Fcore.vio flocq/Core/Fcore_digits.vio flocq/Calc/Fcalc_digits.vio flocq/Appli/Fappli_IEEE.vio -cparser/validator/Alphabet.vo cparser/validator/Alphabet.glob cparser/validator/Alphabet.v.beautified: cparser/validator/Alphabet.v -cparser/validator/Alphabet.vio: cparser/validator/Alphabet.v -cparser/validator/Interpreter_complete.vo cparser/validator/Interpreter_complete.glob cparser/validator/Interpreter_complete.v.beautified: cparser/validator/Interpreter_complete.v cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Interpreter.vo cparser/validator/Validator_complete.vo -cparser/validator/Interpreter_complete.vio: cparser/validator/Interpreter_complete.v cparser/validator/Alphabet.vio cparser/validator/Grammar.vio cparser/validator/Automaton.vio cparser/validator/Interpreter.vio cparser/validator/Validator_complete.vio -cparser/validator/Interpreter.vo cparser/validator/Interpreter.glob cparser/validator/Interpreter.v.beautified: cparser/validator/Interpreter.v cparser/validator/Automaton.vo cparser/validator/Alphabet.vo -cparser/validator/Interpreter.vio: cparser/validator/Interpreter.v cparser/validator/Automaton.vio cparser/validator/Alphabet.vio -cparser/validator/Validator_complete.vo cparser/validator/Validator_complete.glob cparser/validator/Validator_complete.v.beautified: cparser/validator/Validator_complete.v cparser/validator/Automaton.vo cparser/validator/Alphabet.vo -cparser/validator/Validator_complete.vio: cparser/validator/Validator_complete.v cparser/validator/Automaton.vio cparser/validator/Alphabet.vio -cparser/validator/Automaton.vo cparser/validator/Automaton.glob cparser/validator/Automaton.v.beautified: cparser/validator/Automaton.v cparser/validator/Grammar.vo cparser/validator/Alphabet.vo -cparser/validator/Automaton.vio: cparser/validator/Automaton.v cparser/validator/Grammar.vio cparser/validator/Alphabet.vio -cparser/validator/Interpreter_correct.vo cparser/validator/Interpreter_correct.glob cparser/validator/Interpreter_correct.v.beautified: cparser/validator/Interpreter_correct.v cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Interpreter.vo -cparser/validator/Interpreter_correct.vio: cparser/validator/Interpreter_correct.v cparser/validator/Alphabet.vio cparser/validator/Grammar.vio cparser/validator/Automaton.vio cparser/validator/Interpreter.vio -cparser/validator/Main.vo cparser/validator/Main.glob cparser/validator/Main.v.beautified: cparser/validator/Main.v cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Interpreter_safe.vo cparser/validator/Interpreter_correct.vo cparser/validator/Interpreter_complete.vo -cparser/validator/Main.vio: cparser/validator/Main.v cparser/validator/Grammar.vio cparser/validator/Automaton.vio cparser/validator/Interpreter_safe.vio cparser/validator/Interpreter_correct.vio cparser/validator/Interpreter_complete.vio -cparser/validator/Validator_safe.vo cparser/validator/Validator_safe.glob cparser/validator/Validator_safe.v.beautified: cparser/validator/Validator_safe.v cparser/validator/Automaton.vo cparser/validator/Alphabet.vo -cparser/validator/Validator_safe.vio: cparser/validator/Validator_safe.v cparser/validator/Automaton.vio cparser/validator/Alphabet.vio -cparser/validator/Grammar.vo cparser/validator/Grammar.glob cparser/validator/Grammar.v.beautified: cparser/validator/Grammar.v cparser/validator/Alphabet.vo cparser/validator/Tuples.vo -cparser/validator/Grammar.vio: cparser/validator/Grammar.v cparser/validator/Alphabet.vio cparser/validator/Tuples.vio -cparser/validator/Interpreter_safe.vo cparser/validator/Interpreter_safe.glob cparser/validator/Interpreter_safe.v.beautified: cparser/validator/Interpreter_safe.v cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Validator_safe.vo cparser/validator/Interpreter.vo -cparser/validator/Interpreter_safe.vio: cparser/validator/Interpreter_safe.v cparser/validator/Alphabet.vio cparser/validator/Grammar.vio cparser/validator/Automaton.vio cparser/validator/Validator_safe.vio cparser/validator/Interpreter.vio -cparser/validator/Tuples.vo cparser/validator/Tuples.glob cparser/validator/Tuples.v.beautified: cparser/validator/Tuples.v -cparser/validator/Tuples.vio: cparser/validator/Tuples.v -cparser/Cabs.vo cparser/Cabs.glob cparser/Cabs.v.beautified: cparser/Cabs.v -cparser/Cabs.vio: cparser/Cabs.v -cparser/Parser.vo cparser/Parser.glob cparser/Parser.v.beautified: cparser/Parser.v cparser/Cabs.vo cparser/validator/Tuples.vo cparser/validator/Alphabet.vo cparser/validator/Grammar.vo cparser/validator/Automaton.vo cparser/validator/Main.vo -cparser/Parser.vio: cparser/Parser.v cparser/Cabs.vio cparser/validator/Tuples.vio cparser/validator/Alphabet.vio cparser/validator/Grammar.vio cparser/validator/Automaton.vio cparser/validator/Main.vio -exportclight/Clightdefs.vo exportclight/Clightdefs.glob exportclight/Clightdefs.v.beautified: exportclight/Clightdefs.v lib/Integers.vo lib/Floats.vo common/AST.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Clight.vo lib/Maps.vo common/Errors.vo -exportclight/Clightdefs.vio: exportclight/Clightdefs.v lib/Integers.vio lib/Floats.vio common/AST.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Clight.vio lib/Maps.vio common/Errors.vio @@ -24,20 +24,18 @@ tools/ndfun tools/modorder Makefile.config # Generated files +.depend .depend.extr compcert.ini -ia32/ConstpropOp.v -ia32/SelectOp.v -ia32/SelectLong.v +x86/ConstpropOp.v +x86/SelectOp.v +x86/SelectLong.v powerpc/ConstpropOp.v powerpc/SelectOp.v powerpc/SelectLong.v arm/ConstpropOp.v arm/SelectOp.v arm/SelectLong.v -x86_64/ConstpropOp.v -x86_64/SelectOp.v -x86_64/SelectLong.v backend/SelectDiv.v backend/SplitLong.v backend/CMlexer.ml @@ -15,11 +15,17 @@ include Makefile.config -DIRS=lib common $(ARCH) backend cfrontend driver debug\ +ifeq ($(wildcard $(ARCH)_$(BITSIZE)),) +ARCHDIRS=$(ARCH) +else +ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) +endif + +DIRS=lib common $(ARCHDIRS) backend cfrontend driver debug\ flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight \ cparser cparser/validator -RECDIRS=lib common $(ARCH) backend cfrontend driver flocq exportclight cparser +RECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclight cparser COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) @@ -119,7 +125,15 @@ DRIVER=Compopts.v Compiler.v Complements.v FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \ $(PARSERVALIDATOR) $(PARSER) +# Generated source files + +GENERATED=\ + $(ARCH)/ConstpropOp.v $(ARCH)/SelectOp.v $(ARCH)/SelectLong.v \ + backend/SelectDiv.v backend/SplitLong.v \ + cparser/Parser.v + all: + @test -f .depend || $(MAKE) depend $(MAKE) proof $(MAKE) extraction $(MAKE) ccomp @@ -221,10 +235,11 @@ driver/Version.ml: VERSION cparser/Parser.v: cparser/Parser.vy $(MENHIR) --coq cparser/Parser.vy -depend: $(FILES) exportclight/Clightdefs.v - $(COQDEP) $^ \ - | sed -e 's|$(ARCH)/|$$(ARCH)/|g' \ - > .depend +depend: $(GENERATED) depend1 + +depend1: $(FILES) exportclight/Clightdefs.v + @echo "Analyzing Coq dependencies" + @$(COQDEP) $^ > .depend install: install -d $(BINDIR) @@ -244,7 +259,7 @@ clean: rm -f compcert.ini rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o - rm -f $(ARCH)/ConstpropOp.v $(ARCH)/SelectOp.v backend/SelectDiv.v backend/SelectLong.v + rm -f $(GENERATED) .depend $(MAKE) -f Makefile.extr clean $(MAKE) -C runtime clean $(MAKE) -C test clean @@ -267,6 +282,6 @@ check-proof: $(FILES) print-includes: @echo $(COQINCLUDES) -include .depend +-include .depend FORCE: diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 48b8f3d6..8c8dea2f 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -176,7 +176,7 @@ Lemma eval_splitlong: Proof. intros until sem; intros EXEC UNDEF. unfold splitlong. case (splitlong_match a); intros. -- InvEval. subst v. +- InvEval; subst. exploit EXEC. eexact H2. eexact H3. intros [v' [A B]]. exists v'; split. auto. destruct v1; simpl in *; try (rewrite UNDEF; auto). @@ -224,7 +224,7 @@ Lemma eval_splitlong2: Proof. intros until sem; intros EXEC UNDEF. unfold splitlong2. case (splitlong2_match a b); intros. -- InvEval. subst va vb. +- InvEval; subst. exploit (EXEC le h1 l1 h2 l2); eauto. intros [v [A B]]. exists v; split; auto. destruct v1; simpl in *; try (rewrite UNDEF; auto). @@ -232,7 +232,7 @@ Proof. destruct v2; simpl in *; try (rewrite UNDEF; auto). destruct v3; try (rewrite UNDEF; auto). erewrite B; eauto. -- InvEval. subst va. +- InvEval; subst. exploit (EXEC (vb :: le) (lift h1) (lift l1) (Eop Ohighlong (Eletvar 0 ::: Enil)) (Eop Olowlong (Eletvar 0 ::: Enil))). EvalOp. EvalOp. EvalOp. EvalOp. @@ -243,7 +243,7 @@ Proof. destruct v0; try (rewrite UNDEF; auto). destruct vb; try (rewrite UNDEF; auto). erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto. -- InvEval. subst vb. +- InvEval; subst. exploit (EXEC (va :: le) (Eop Ohighlong (Eletvar 0 ::: Enil)) (Eop Olowlong (Eletvar 0 ::: Enil)) (lift h2) (lift l2)). @@ -322,7 +322,7 @@ Qed. Lemma eval_lowlong: unary_constructor_sound lowlong Val.loword. Proof. unfold lowlong; red. intros until x. destruct (lowlong_match a); intros. - InvEval. subst x. exists v0; split; auto. + InvEval; subst. exists v0; split; auto. destruct v1; simpl; auto. destruct v0; simpl; auto. rewrite Int64.lo_ofwords. auto. exists (Val.loword x); split; auto. EvalOp. @@ -331,7 +331,7 @@ Qed. Lemma eval_highlong: unary_constructor_sound highlong Val.hiword. Proof. unfold highlong; red. intros until x. destruct (highlong_match a); intros. - InvEval. subst x. exists v1; split; auto. + InvEval; subst. exists v1; split; auto. destruct v1; simpl; auto. destruct v0; simpl; auto. rewrite Int64.hi_ofwords. auto. exists (Val.hiword x); split; auto. EvalOp. @@ -103,31 +103,31 @@ done # case "$target" in arm-*|armv7a-*) - arch="arm"; model="armv7a"; endianness="little";; + arch="arm"; model="armv7a"; endianness="little"; bitsize=32;; armv6-*) - arch="arm"; model="armv6"; endianness="little";; + arch="arm"; model="armv6"; endianness="little"; bitsize=32;; armv7r-*) - arch="arm"; model="armv7r"; endianness="little";; + arch="arm"; model="armv7r"; endianness="little"; bitsize=32;; armv7m-*) - arch="arm"; model="armv7m"; endianness="little";; + arch="arm"; model="armv7m"; endianness="little"; bitsize=32;; armeb-*|armebv7a-*) - arch="arm"; model="armv7a"; endianness="big";; + arch="arm"; model="armv7a"; endianness="big"; bitsize=32;; armebv6-*) - arch="arm"; model="armv6"; endianness="big";; + arch="arm"; model="armv6"; endianness="big"; bitsize=32;; armebv7r-*) - arch="arm"; model="armv7r"; endianness="big";; + arch="arm"; model="armv7r"; endianness="big"; bitsize=32;; armebv7m-*) - arch="arm"; model="armv7m"; endianness="big";; - ia32-*) - arch="ia32"; model="32sse2"; endianness="little";; + arch="arm"; model="armv7m"; endianness="big"; bitsize=32;; + x86_32-*|ia32-*) + arch="x86"; model="32sse2"; endianness="little"; bitsize=32;; x86_64-*) - arch="ia32"; model="64"; endianness="little";; + arch="x86"; model="64"; endianness="little"; bitsize=64;; powerpc-*|ppc-*) - arch="powerpc"; model="ppc32"; endianness="big";; + arch="powerpc"; model="ppc32"; endianness="big"; bitsize=32;; powerpc64-*|ppc64-*) - arch="powerpc"; model="ppc64"; endianness="big";; + arch="powerpc"; model="ppc64"; endianness="big"; bitsize=32;; e5500-*) - arch="powerpc"; model="e5500"; endianness="big";; + arch="powerpc"; model="e5500"; endianness="big"; bitsize=32;; manual) ;; "") @@ -242,9 +242,9 @@ fi # -# IA32 (32 bits) Target Configuration +# x86 (32 bits) Target Configuration # -if test "$arch" = "ia32" -a "$model" != "64"; then +if test "$arch" = "x86" -a "$bitsize" = "32"; then case "$target" in bsd) @@ -323,7 +323,7 @@ fi # # IA32 (64 bits) Target Configuration # -if test "$arch" = "ia32" -a "$model" = "64"; then +if test "$arch" = "x86" -a "$bitsize" = "64"; then case "$target" in linux) @@ -501,6 +501,7 @@ cat >> Makefile.config <<EOF ABI=$abi ARCH=$arch ASM_SUPPORTS_CFI=$asm_supports_cfi +BITSIZE=$bitsize CASM=$casm CASM_OPTIONS=$casm_options CASMRUNTIME=$casmruntime @@ -526,7 +527,7 @@ cat >> Makefile.config <<'EOF' # Target architecture # ARCH=powerpc # ARCH=arm -# ARCH=ia32 +# ARCH=x86 ARCH= # Hardware variant @@ -537,20 +538,25 @@ ARCH= # MODEL=armv7a # for ARM # MODEL=armv7r # for ARM # MODEL=armv7m # for ARM -# MODEL=32sse2 # for IA32 in 32-bit mode -# MODEL=64 # for IA32 in 64-bit mode +# MODEL=32sse2 # for x86 in 32-bit mode +# MODEL=64 # for x86 in 64-bit mode MODEL= # Target ABI # ABI=eabi # for PowerPC / Linux and other SVR4 or EABI platforms # ABI=eabi # for ARM # ABI=hardfloat # for ARM -# ABI=standard # for IA32 +# ABI=standard # for x86 ABI= +# Target bit width +# BITSIZE=64 # for x86 in 64-bit mode +# BITSIZE=32 # otherwise +BITSIZE= + # Target endianness # ENDIANNESS=big # for ARM or PowerPC -# ENDIANNESS=little # for ARM or IA32 +# ENDIANNESS=little # for ARM or x86 ENDIANNESS= # Default calling conventions for passing structs and unions by value @@ -575,7 +581,7 @@ STRUCT_RETURN=ref # Possible choices for ARM: # SYSTEM=linux # -# Possible choices for IA32: +# Possible choices for x86: # SYSTEM=linux # SYSTEM=bsd # SYSTEM=macosx @@ -619,6 +625,10 @@ RESPONSEFILE="none" EOF fi +# +# Clean up target-dependent files to force their recompilation +# +rm -f .depend $arch/Archi.vo ${arch}_${bitsize}/Archi.vo runtime/*.o # # Summarize Configuration @@ -657,7 +667,5 @@ CompCert configuration: Standard headers installed in. $libdirexp/include Build command to use.......... $make -If anything above looks wrong, please edit file ./Makefile.config to correct. - EOF fi diff --git a/driver/Driver.ml b/driver/Driver.ml index 4bd08a88..3cc1bcad 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -536,7 +536,7 @@ let _ = | "arm" -> if Configuration.is_big_endian then Machine.arm_bigendian else Machine.arm_littleendian - | "ia32" -> if Configuration.model = "64" then + | "x86" -> if Configuration.model = "64" then Machine.x86_64 else if Configuration.abi = "macosx" diff --git a/runtime/Makefile b/runtime/Makefile index b94db3ca..641c9fdc 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -2,9 +2,11 @@ include ../Makefile.config CFLAGS=-O1 -g -Wall -ifeq ($(ARCH),ia32) +ifeq ($(ARCH),x86) ifeq ($(MODEL),64) ARCH=x86_64 +else +ARCH=x86_32 endif endif diff --git a/runtime/ia32/i64_dtos.S b/runtime/x86_32/i64_dtos.S index 3cc381bf..3cc381bf 100644 --- a/runtime/ia32/i64_dtos.S +++ b/runtime/x86_32/i64_dtos.S diff --git a/runtime/ia32/i64_dtou.S b/runtime/x86_32/i64_dtou.S index 4903f847..4903f847 100644 --- a/runtime/ia32/i64_dtou.S +++ b/runtime/x86_32/i64_dtou.S diff --git a/runtime/ia32/i64_sar.S b/runtime/x86_32/i64_sar.S index cf2233b1..cf2233b1 100644 --- a/runtime/ia32/i64_sar.S +++ b/runtime/x86_32/i64_sar.S diff --git a/runtime/ia32/i64_sdiv.S b/runtime/x86_32/i64_sdiv.S index f6551c7d..f6551c7d 100644 --- a/runtime/ia32/i64_sdiv.S +++ b/runtime/x86_32/i64_sdiv.S diff --git a/runtime/ia32/i64_shl.S b/runtime/x86_32/i64_shl.S index 1fabebce..1fabebce 100644 --- a/runtime/ia32/i64_shl.S +++ b/runtime/x86_32/i64_shl.S diff --git a/runtime/ia32/i64_shr.S b/runtime/x86_32/i64_shr.S index 34196f09..34196f09 100644 --- a/runtime/ia32/i64_shr.S +++ b/runtime/x86_32/i64_shr.S diff --git a/runtime/ia32/i64_smod.S b/runtime/x86_32/i64_smod.S index 28f47ad4..28f47ad4 100644 --- a/runtime/ia32/i64_smod.S +++ b/runtime/x86_32/i64_smod.S diff --git a/runtime/ia32/i64_smulh.S b/runtime/x86_32/i64_smulh.S index cc0f0167..cc0f0167 100644 --- a/runtime/ia32/i64_smulh.S +++ b/runtime/x86_32/i64_smulh.S diff --git a/runtime/ia32/i64_stod.S b/runtime/x86_32/i64_stod.S index d020e2fc..d020e2fc 100644 --- a/runtime/ia32/i64_stod.S +++ b/runtime/x86_32/i64_stod.S diff --git a/runtime/ia32/i64_stof.S b/runtime/x86_32/i64_stof.S index 25b1d4f7..25b1d4f7 100644 --- a/runtime/ia32/i64_stof.S +++ b/runtime/x86_32/i64_stof.S diff --git a/runtime/ia32/i64_udiv.S b/runtime/x86_32/i64_udiv.S index 75305433..75305433 100644 --- a/runtime/ia32/i64_udiv.S +++ b/runtime/x86_32/i64_udiv.S diff --git a/runtime/ia32/i64_udivmod.S b/runtime/x86_32/i64_udivmod.S index dccfc286..dccfc286 100644 --- a/runtime/ia32/i64_udivmod.S +++ b/runtime/x86_32/i64_udivmod.S diff --git a/runtime/ia32/i64_umod.S b/runtime/x86_32/i64_umod.S index a019df28..a019df28 100644 --- a/runtime/ia32/i64_umod.S +++ b/runtime/x86_32/i64_umod.S diff --git a/runtime/ia32/i64_umulh.S b/runtime/x86_32/i64_umulh.S index 449a0f8b..449a0f8b 100644 --- a/runtime/ia32/i64_umulh.S +++ b/runtime/x86_32/i64_umulh.S diff --git a/runtime/ia32/i64_utod.S b/runtime/x86_32/i64_utod.S index 428a3b94..428a3b94 100644 --- a/runtime/ia32/i64_utod.S +++ b/runtime/x86_32/i64_utod.S diff --git a/runtime/ia32/i64_utof.S b/runtime/x86_32/i64_utof.S index 0b58f48b..0b58f48b 100644 --- a/runtime/ia32/i64_utof.S +++ b/runtime/x86_32/i64_utof.S diff --git a/runtime/ia32/sysdeps.h b/runtime/x86_32/sysdeps.h index 9d957a88..9d957a88 100644 --- a/runtime/ia32/sysdeps.h +++ b/runtime/x86_32/sysdeps.h diff --git a/runtime/ia32/vararg.S b/runtime/x86_32/vararg.S index 78666c70..78666c70 100644 --- a/runtime/ia32/vararg.S +++ b/runtime/x86_32/vararg.S diff --git a/test/regression/Results/builtins-ia32 b/test/regression/Results/builtins-x86 index 393ac1fd..393ac1fd 100644 --- a/test/regression/Results/builtins-ia32 +++ b/test/regression/Results/builtins-x86 diff --git a/test/regression/Runtest b/test/regression/Runtest index 7cc6330b..9051b5b7 100755 --- a/test/regression/Runtest +++ b/test/regression/Runtest @@ -9,19 +9,13 @@ out="test$$.log" rm -f $out trap "rm -f $out" 0 INT QUIT -# The architecture and the model +# The architecture and the bitsize arch=`sed -n -e 's/^ARCH=//p' ../../Makefile.config` -model=`sed -n -e 's/^MODEL=//p' ../../Makefile.config` - -# Its bit size -case "$arch,$model" in - ia32,64) bits=64;; - *) bits=32;; -esac +bits=`sed -n -e 's/^BITSIZE=//p' ../../Makefile.config` # The reference output -if test -f "Results/$name-$arch-$model"; then - ref="Results/$name-$arch-$model" +if test -f "Results/$name-$arch-$bits"; then + ref="Results/$name-$arch-$bits" elif test -f "Results/$name-$arch"; then ref="Results/$name-$arch" elif test -f "Results/$name-$bits"; then diff --git a/test/regression/builtins-ia32.c b/test/regression/builtins-x86.c index 1ba213e7..1ba213e7 100644 --- a/test/regression/builtins-ia32.c +++ b/test/regression/builtins-x86.c diff --git a/ia32/AsmToJSON.ml b/x86/AsmToJSON.ml index 3214491f..3214491f 100644 --- a/ia32/AsmToJSON.ml +++ b/x86/AsmToJSON.ml diff --git a/ia32/AsmToJSON.mli b/x86/AsmToJSON.mli index 20bcba5e..20bcba5e 100644 --- a/ia32/AsmToJSON.mli +++ b/x86/AsmToJSON.mli diff --git a/ia32/Asmexpand.ml b/x86/Asmexpand.ml index 0436bc86..0436bc86 100644 --- a/ia32/Asmexpand.ml +++ b/x86/Asmexpand.ml diff --git a/ia32/Asmgen.v b/x86/Asmgen.v index bb26d507..bb26d507 100644 --- a/ia32/Asmgen.v +++ b/x86/Asmgen.v diff --git a/ia32/Asmgenproof.v b/x86/Asmgenproof.v index e56dc429..e56dc429 100644 --- a/ia32/Asmgenproof.v +++ b/x86/Asmgenproof.v diff --git a/ia32/Asmgenproof1.v b/x86/Asmgenproof1.v index 05b3176a..401be7d7 100644 --- a/ia32/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -18,7 +18,6 @@ Require Import Op Locations Conventions Mach Asm. Require Import Asmgen Asmgenproof0. Open Local Scope error_monad_scope. -Local Transparent Archi.ptr64. (** * Correspondence between Mach registers and x86 registers *) @@ -255,11 +254,11 @@ Proof. set (rs5 := nextinstr_nf (rs4#RAX <- v4)). assert (X: forall v1 v2, Val.addl v1 (Val.addl v2 (Vlong Int64.zero)) = Val.addl v1 v2). - { intros. destruct v0; simpl; auto; destruct v5; simpl; auto. + { intros. unfold Val.addl; destruct Archi.ptr64 eqn:SF, v0; auto; destruct v5; auto. rewrite Int64.add_zero; auto. - destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. - destruct Archi.ptr64; auto. rewrite Int64.add_zero; auto. - destruct Archi.ptr64; auto. } + rewrite Ptrofs.add_zero; auto. + rewrite Int64.add_zero; auto. + rewrite Int64.add_zero; auto. } exists rs5; split. eapply exec_straight_trans with (rs2 := rs3). eapply exec_straight_two with (rs2 := rs2); reflexivity. @@ -334,7 +333,7 @@ Proof. with (eval_addrmode ge addr rs1). rewrite H0. eauto. unfold eval_addrmode in *; rewrite H1 in *. - destruct (eval_addrmode32 ge addr rs1); simpl in H0; try discriminate. + destruct (eval_addrmode32 ge addr rs1); simpl in H0; try discriminate H0. simpl. rewrite H1. rewrite Ptrofs.add_zero; auto. auto. auto. auto. intros. destruct H4. Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs. @@ -428,19 +427,17 @@ Proof. { intros. destruct (zeq i 1); subst; auto. destruct v; simpl; auto. rewrite Int.mul_one; auto. } unfold transl_addressing; intros. - destruct addr; repeat (destruct args; try discriminate); simpl in H0; inv H0; + destruct addr; repeat (destruct args; try discriminate H); simpl in H0; FuncInv; monadInv H; try (erewrite ! ireg_of_eq by eauto); unfold eval_addrmode32. - simpl; rewrite Int.add_zero_l; auto. - rewrite Val.add_assoc. apply Val.add_lessdef; auto. - rewrite Val.add_permut. apply Val.add_lessdef; auto. simpl; rewrite Int.add_zero_l; auto. - apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. -- destruct Archi.ptr64 eqn:SF; inv H2. rewrite ! A by auto. auto. -- destruct Archi.ptr64 eqn:SF; inv H2. erewrite ireg_of_eq by eauto. - rewrite Val.add_commut. rewrite A by auto. auto. -- destruct Archi.ptr64 eqn:SF; inv H2. erewrite ireg_of_eq by eauto. - rewrite Val.add_permut. rewrite Val.add_commut. apply Val.add_lessdef; auto. rewrite A; auto. -- destruct Archi.ptr64 eqn:SF; inv H2. simpl. - destruct (rs RSP); simpl; auto; rewrite SF. +- rewrite ! A by auto. auto. +- rewrite Val.add_commut. rewrite A by auto. auto. +- rewrite Val.add_permut. rewrite Val.add_commut. apply Val.add_lessdef; auto. rewrite A; auto. +- simpl. unfold Val.add; rewrite Heqb. + destruct (rs RSP); simpl; auto. rewrite Int.add_zero_l. apply Val.lessdef_same; f_equal; f_equal. symmetry. transitivity (Ptrofs.repr (Ptrofs.signed i)). auto with ptrofs. auto with ints. Qed. @@ -461,15 +458,14 @@ Proof. { intros. destruct (zeq i 1); subst; auto. destruct v; simpl; auto. rewrite Int64.mul_one; auto. } unfold transl_addressing; intros. - destruct addr; repeat (destruct args; try discriminate); simpl in H0; inv H0; + destruct addr; repeat (destruct args; try discriminate H); simpl in H0; FuncInv; monadInv H; try (erewrite ! ireg_of_eq by eauto); unfold eval_addrmode64. - simpl; rewrite Int64.add_zero_l; auto. - rewrite Val.addl_assoc. apply Val.addl_lessdef; auto. - rewrite Val.addl_permut. apply Val.addl_lessdef; auto. simpl; rewrite Int64.add_zero_l; auto. - apply Val.addl_lessdef; auto. apply Val.addl_lessdef; auto. -- destruct Archi.ptr64 eqn:SF; inv H2. rewrite ! A by auto. auto. -- destruct Archi.ptr64 eqn:SF; inv H2. simpl. - destruct (rs RSP); simpl; auto; rewrite SF. +- rewrite ! A by auto. auto. +- unfold Val.addl; rewrite Heqb. destruct (rs RSP); auto. simpl. rewrite Int64.add_zero_l. apply Val.lessdef_same; f_equal; f_equal. symmetry. transitivity (Ptrofs.repr (Ptrofs.signed i)). auto with ptrofs. auto with ints. Qed. @@ -555,7 +551,7 @@ Proof. set (rs' := nextinstr (compare_ints v1 v2 rs m)). intros [A [B [C [D E]]]]. unfold eval_testcond. rewrite A; rewrite B. unfold Val.cmpu, Val.cmp. - destruct v1; destruct v2; simpl in H; inv H. + destruct v1; destruct v2; simpl in H; FuncInv; subst. - (* int int *) destruct c; simpl; auto. destruct (Int.eq i i0); reflexivity. @@ -565,22 +561,22 @@ Proof. rewrite (Int.ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity. destruct (Int.ltu i i0); reflexivity. - (* int ptr *) - unfold Val.cmpu_bool; destruct Archi.ptr64; try discriminate. + unfold Val.cmpu_bool; rewrite Heqb1. destruct (Int.eq i Int.zero && - (Mem.valid_pointer m b0 (Ptrofs.unsigned i0) || Mem.valid_pointer m b0 (Ptrofs.unsigned i0 - 1))); try discriminate. - destruct c; simpl in *; inv H1; reflexivity. + (Mem.valid_pointer m b0 (Ptrofs.unsigned i0) || Mem.valid_pointer m b0 (Ptrofs.unsigned i0 - 1))); try discriminate H. + destruct c; simpl in *; inv H; reflexivity. - (* ptr int *) - unfold Val.cmpu_bool; destruct Archi.ptr64; try discriminate. + unfold Val.cmpu_bool; rewrite Heqb1. destruct (Int.eq i0 Int.zero && - (Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); try discriminate. - destruct c; simpl in *; inv H1; reflexivity. + (Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); try discriminate H. + destruct c; simpl in *; inv H; reflexivity. - (* ptr ptr *) - unfold Val.cmpu_bool; destruct Archi.ptr64; try discriminate. + unfold Val.cmpu_bool; rewrite Heqb2. fold (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i)) in *. fold (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)) in *. destruct (eq_block b0 b1). destruct (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i) && - Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)); inv H1. + Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)); inv H. destruct c; simpl; auto. destruct (Ptrofs.eq i i0); auto. destruct (Ptrofs.eq i i0); auto. @@ -589,8 +585,8 @@ Proof. rewrite (Ptrofs.ltu_not i i0). destruct (Ptrofs.ltu i i0); destruct (Ptrofs.eq i i0); reflexivity. destruct (Ptrofs.ltu i i0); reflexivity. destruct (Mem.valid_pointer m b0 (Ptrofs.unsigned i) && - Mem.valid_pointer m b1 (Ptrofs.unsigned i0)); try discriminate. - destruct c; simpl in *; inv H1; reflexivity. + Mem.valid_pointer m b1 (Ptrofs.unsigned i0)); try discriminate H. + destruct c; simpl in *; inv H; reflexivity. Qed. Lemma compare_longs_spec: @@ -658,7 +654,7 @@ Proof. set (rs' := nextinstr (compare_longs v1 v2 rs m)). intros [A [B [C [D E]]]]. unfold eval_testcond. rewrite A; rewrite B. - destruct v1; destruct v2; simpl in H; inv H. + destruct v1; destruct v2; simpl in H; FuncInv; subst. - (* int int *) destruct c; simpl; auto. destruct (Int64.eq i i0); reflexivity. @@ -670,20 +666,20 @@ Proof. - (* int ptr *) unfold Val.cmplu; simpl; destruct Archi.ptr64; try discriminate. destruct (Int64.eq i Int64.zero && - (Mem.valid_pointer m b0 (Ptrofs.unsigned i0) || Mem.valid_pointer m b0 (Ptrofs.unsigned i0 - 1))) eqn:?; try discriminate. - destruct c; simpl in *; inv H1; auto. + (Mem.valid_pointer m b0 (Ptrofs.unsigned i0) || Mem.valid_pointer m b0 (Ptrofs.unsigned i0 - 1))) eqn:?; try discriminate H. + destruct c; simpl in *; inv H; auto. - (* ptr int *) unfold Val.cmplu; simpl; destruct Archi.ptr64; try discriminate. destruct (Int64.eq i0 Int64.zero && - (Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))) eqn:?; try discriminate. - destruct c; simpl in *; inv H1; auto. + (Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))) eqn:?; try discriminate H. + destruct c; simpl in *; inv H; auto. - (* ptr ptr *) - unfold Val.cmplu; simpl; destruct Archi.ptr64; try discriminate. + unfold Val.cmplu; simpl; destruct Archi.ptr64; try discriminate H. fold (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i)) in *. fold (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)) in *. destruct (eq_block b0 b1). destruct (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i) && - Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)); inv H1. + Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)); inv H. destruct c; simpl; auto. destruct (Ptrofs.eq i i0); auto. destruct (Ptrofs.eq i i0); auto. @@ -692,8 +688,8 @@ Proof. rewrite (Ptrofs.ltu_not i i0). destruct (Ptrofs.ltu i i0); destruct (Ptrofs.eq i i0); reflexivity. destruct (Ptrofs.ltu i i0); reflexivity. destruct (Mem.valid_pointer m b0 (Ptrofs.unsigned i) && - Mem.valid_pointer m b1 (Ptrofs.unsigned i0)); try discriminate. - destruct c; simpl in *; inv H1; reflexivity. + Mem.valid_pointer m b1 (Ptrofs.unsigned i0)); try discriminate H. + destruct c; simpl in *; inv H; reflexivity. Qed. Lemma compare_floats_spec: diff --git a/ia32/CBuiltins.ml b/x86/CBuiltins.ml index 09303223..09303223 100644 --- a/ia32/CBuiltins.ml +++ b/x86/CBuiltins.ml diff --git a/ia32/CombineOp.v b/x86/CombineOp.v index 34c1c9cc..34c1c9cc 100644 --- a/ia32/CombineOp.v +++ b/x86/CombineOp.v diff --git a/ia32/CombineOpproof.v b/x86/CombineOpproof.v index f59e582b..f59e582b 100644 --- a/ia32/CombineOpproof.v +++ b/x86/CombineOpproof.v diff --git a/ia32/ConstpropOp.vp b/x86/ConstpropOp.vp index 0bf143d2..0bf143d2 100644 --- a/ia32/ConstpropOp.vp +++ b/x86/ConstpropOp.vp diff --git a/ia32/ConstpropOpproof.v b/x86/ConstpropOpproof.v index 161b9579..4f582f86 100644 --- a/ia32/ConstpropOpproof.v +++ b/x86/ConstpropOpproof.v @@ -94,12 +94,12 @@ Lemma const_for_result_correct: vmatch bc v a -> exists v', eval_operation ge (Vptr sp Ptrofs.zero) op nil m = Some v' /\ Val.lessdef v v'. Proof. - unfold const_for_result; intros. + unfold const_for_result. generalize Archi.ptr64; intros ptr64; intros. destruct a; inv H; SimplVM. - (* integer *) exists (Vint n); auto. - (* long *) - destruct Archi.ptr64; inv H2. exists (Vlong n); auto. + destruct ptr64; inv H2. exists (Vlong n); auto. - (* float *) destruct (Compopts.generate_float_constants tt); inv H2. exists (Vfloat f); auto. - (* single *) @@ -110,12 +110,14 @@ Proof. destruct (symbol_is_external id). * revert H2; predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero; intros EQ; inv EQ. exists (Genv.symbol_address ge id Ptrofs.zero); auto. - * inv H2. exists (Genv.symbol_address ge id ofs); split; auto. - rewrite eval_Olea_ptr. apply eval_addressing_Aglobal. + * inv H2. exists (Genv.symbol_address ge id ofs); split. + rewrite eval_Olea_ptr. apply eval_addressing_Aglobal. + auto. + (* stack *) - inv H2. exists (Vptr sp ofs); split; auto. + inv H2. exists (Vptr sp ofs); split. rewrite eval_Olea_ptr. rewrite eval_addressing_Ainstack. - simpl. rewrite Ptrofs.add_zero_l; auto. + simpl. rewrite Ptrofs.add_zero_l; auto. + auto. Qed. Lemma cond_strength_reduction_correct: @@ -177,7 +179,7 @@ Proof. { intros. rewrite <- A. apply Genv.shift_symbol_address_32; auto. } Local Opaque Val.add. destruct (addr_strength_reduction_32_match addr args vl); - simpl in *; InvApproxRegs; SimplVM; try (inv EA); rewrite ? SF. + simpl in *; InvApproxRegs; SimplVM; FuncInv; subst; rewrite ?SF. - econstructor; split; eauto. rewrite B. apply Val.add_lessdef; auto. - econstructor; split; eauto. rewrite Ptrofs.add_zero_l. Local Transparent Val.add. @@ -207,9 +209,9 @@ Local Transparent Val.add. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. - econstructor; split; eauto. rewrite B. rewrite ! Val.add_assoc. rewrite (Val.add_commut (Vint (Int.repr ofs))). apply Val.add_lessdef; auto. -- rewrite SF in H1; inv H1. econstructor; split; eauto. +- econstructor; split; eauto. rewrite Genv.shift_symbol_address_32 by auto. auto. -- rewrite SF in H1; inv H1. econstructor; split; eauto. +- econstructor; split; eauto. rewrite Genv.shift_symbol_address_32 by auto. auto. - apply addr_strength_reduction_32_generic_correct; auto. Qed. @@ -255,7 +257,7 @@ Proof. { intros. rewrite <- A. apply Genv.shift_symbol_address_64; auto. } Local Opaque Val.addl. destruct (addr_strength_reduction_64_match addr args vl); - simpl in *; InvApproxRegs; SimplVM; try (inv EA); rewrite ? SF. + simpl in *; InvApproxRegs; SimplVM; FuncInv; subst; rewrite ?SF. - econstructor; split; eauto. rewrite B. apply Val.addl_lessdef; auto. - econstructor; split; eauto. rewrite Ptrofs.add_zero_l. Local Transparent Val.addl. @@ -348,7 +350,7 @@ Proof. intros. unfold make_addimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (e#r); split; auto. - destruct (e#r); simpl; auto. rewrite Int.add_zero; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. + destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. exists (Val.add e#r (Vint n)); split; auto. simpl. rewrite Int.repr_signed; auto. Qed. @@ -511,7 +513,7 @@ Proof. intros. unfold make_addlimm. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst. exists (e#r); split; auto. - destruct (e#r); simpl; auto. rewrite Int64.add_zero; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. + destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto. exists (Val.addl e#r (Vlong n)); split; auto. simpl. rewrite Int64.repr_signed; auto. Qed. @@ -828,10 +830,10 @@ Proof. InvApproxRegs; SimplVM; inv H0. replace (Val.subl e#r1 (Vlong n2)) with (Val.addl e#r1 (Vlong (Int64.neg n2))). apply make_addlimm_correct; auto. - destruct (e#r1); simpl; auto. + unfold Val.addl, Val.subl. destruct Archi.ptr64 eqn:SF, e#r1; auto. rewrite Int64.sub_add_opp; auto. - destruct Archi.ptr64 eqn:SF; auto. rewrite Ptrofs.sub_add_opp. do 2 f_equal. auto with ptrofs. + rewrite Int64.sub_add_opp; auto. (* mull *) rewrite Val.mull_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_mullimm_correct; auto. InvApproxRegs; SimplVM; inv H0. apply make_mullimm_correct; auto. diff --git a/ia32/Conventions1.v b/x86/Conventions1.v index dbc8b064..dbc8b064 100644 --- a/ia32/Conventions1.v +++ b/x86/Conventions1.v diff --git a/ia32/Machregs.v b/x86/Machregs.v index 741081a6..741081a6 100644 --- a/ia32/Machregs.v +++ b/x86/Machregs.v diff --git a/ia32/Machregsaux.ml b/x86/Machregsaux.ml index 473e0602..473e0602 100644 --- a/ia32/Machregsaux.ml +++ b/x86/Machregsaux.ml diff --git a/ia32/Machregsaux.mli b/x86/Machregsaux.mli index 9404568d..9404568d 100644 --- a/ia32/Machregsaux.mli +++ b/x86/Machregsaux.mli diff --git a/ia32/NeedOp.v b/x86/NeedOp.v index 09013cdd..09013cdd 100644 --- a/ia32/NeedOp.v +++ b/x86/NeedOp.v @@ -414,11 +414,11 @@ Qed. Ltac FuncInv := match goal with | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => - destruct x; simpl in H; try discriminate H; FuncInv + destruct x; simpl in H; FuncInv | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ => - destruct v; simpl in H; try discriminate H; FuncInv + destruct v; simpl in H; FuncInv | H: (if Archi.ptr64 then _ else _) = Some _ |- _ => - destruct Archi.ptr64 eqn:?; try discriminate H; FuncInv + destruct Archi.ptr64 eqn:?; FuncInv | H: (Some _ = Some _) |- _ => injection H; intros; clear H; FuncInv | H: (None = Some _) |- _ => @@ -614,7 +614,7 @@ Lemma type_of_operation_sound: op <> Omove -> eval_operation genv sp op vl m = Some v -> Val.has_type v (snd (type_of_operation op)). -Proof with (try exact I). +Proof with (try exact I; try reflexivity). intros. destruct op; simpl in H0; FuncInv; subst; simpl. congruence. @@ -623,15 +623,12 @@ Proof with (try exact I). exact I. exact I. unfold Genv.symbol_address; destruct (Genv.find_symbol genv id)... - unfold Val.has_type, Tptr; destruct Archi.ptr64; auto. destruct v0... destruct v0... destruct v0... destruct v0... destruct v0... - destruct v0; destruct v1; simpl... - unfold Val.has_type; destruct Archi.ptr64; auto. - unfold Val.has_type; destruct Archi.ptr64; auto. destruct (eq_block b b0); auto. + unfold Val.sub, Val.has_type; destruct Archi.ptr64, v0, v1... destruct (eq_block b b0)... destruct v0; destruct v1... destruct v0... destruct v0; destruct v1... @@ -666,10 +663,8 @@ Proof with (try exact I). destruct v0... destruct v0... destruct v0... - destruct v0; simpl... unfold Val.has_type; destruct Archi.ptr64; auto. - destruct v0; destruct v1; simpl... - unfold Val.has_type; destruct Archi.ptr64; auto. - unfold Val.has_type; destruct Archi.ptr64; simpl; auto. destruct (eq_block b b0); auto. + unfold Val.addl, Val.has_type; destruct Archi.ptr64, v0... + unfold Val.subl, Val.has_type; destruct Archi.ptr64, v0, v1... destruct (eq_block b b0)... destruct v0; destruct v1... destruct v0... destruct v0; destruct v1... @@ -820,9 +815,10 @@ Lemma eval_shift_stack_addressing32: eval_addressing32 ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = eval_addressing32 ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. - intros. destruct addr; simpl; auto. - destruct vl; auto. destruct Archi.ptr64 eqn:SF; auto. - do 2 f_equal. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut. + intros. + assert (A: forall i, Ptrofs.add Ptrofs.zero (Ptrofs.add i (Ptrofs.repr delta)) = Ptrofs.add (Ptrofs.repr delta) i). + { intros. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut. } + destruct addr; simpl; rewrite ?A; reflexivity. Qed. Lemma eval_shift_stack_addressing64: @@ -830,9 +826,10 @@ Lemma eval_shift_stack_addressing64: eval_addressing64 ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = eval_addressing64 ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. - intros. destruct addr; simpl; auto. - destruct vl; auto. destruct Archi.ptr64 eqn:SF; auto. - do 2 f_equal. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut. + intros. + assert (A: forall i, Ptrofs.add Ptrofs.zero (Ptrofs.add i (Ptrofs.repr delta)) = Ptrofs.add (Ptrofs.repr delta) i). + { intros. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut. } + destruct addr; simpl; rewrite ?A; reflexivity. Qed. Lemma eval_shift_stack_addressing: @@ -1023,10 +1020,8 @@ Lemma eval_operation_preserved: eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m. Proof. intros. - unfold eval_operation; destruct op; auto. + unfold eval_operation; destruct op; auto using eval_addressing32_preserved, eval_addressing64_preserved. unfold Genv.symbol_address. rewrite agree_on_symbols. auto. - apply eval_addressing32_preserved. - apply eval_addressing64_preserved. Qed. End GENV_TRANSF. diff --git a/ia32/PrintOp.ml b/x86/PrintOp.ml index faa5bb5f..faa5bb5f 100644 --- a/ia32/PrintOp.ml +++ b/x86/PrintOp.ml diff --git a/ia32/SelectLong.vp b/x86/SelectLong.vp index b213e23f..b213e23f 100644 --- a/ia32/SelectLong.vp +++ b/x86/SelectLong.vp diff --git a/ia32/SelectLongproof.v b/x86/SelectLongproof.v index a3d2bb19..f7d5df10 100644 --- a/ia32/SelectLongproof.v +++ b/x86/SelectLongproof.v @@ -221,10 +221,9 @@ Proof. destruct (Int.ltu n1 Int64.iwordsize') eqn:LT1; auto. simpl; rewrite LT. rewrite Int.add_commut, Int64.shl'_shl'; auto. rewrite Int.add_commut; auto. - destruct (shift_is_scale n); auto. - TrivialExists. simpl. subst x. destruct v1; simpl; auto. + TrivialExists. simpl. destruct v1; simpl; auto. rewrite LT. rewrite ! Int64.repr_unsigned. rewrite Int64.shl'_one_two_p. rewrite ! Int64.shl'_mul_two_p. rewrite Int64.mul_add_distr_l. auto. - destruct Archi.ptr64; reflexivity. - destruct (shift_is_scale n); auto. TrivialExists. simpl. destruct x; simpl; auto. rewrite LT. rewrite ! Int64.repr_unsigned. rewrite Int64.shl'_one_two_p. @@ -314,9 +313,7 @@ Proof. unfold addlimm; intros; red; intros. predSpec Int64.eq Int64.eq_spec n Int64.zero. subst. exists x; split; auto. - destruct x; simpl; auto. - rewrite Int64.add_zero; auto. - destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. + destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto. destruct (addlimm_match a); InvEval. - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto. - inv H. simpl in H6. TrivialExists. simpl. @@ -345,10 +342,12 @@ Proof. - subst. TrivialExists. - subst. TrivialExists. simpl. rewrite ! Val.addl_assoc. rewrite (Val.addl_commut y). auto. - subst. TrivialExists. simpl. rewrite ! Val.addl_assoc. auto. -- TrivialExists. simpl. destruct x; destruct y; simpl; auto. - rewrite Int64.add_zero; auto. - destruct Archi.ptr64 eqn:SF; simpl; auto. rewrite SF. rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto. - destruct Archi.ptr64 eqn:SF; simpl; auto. rewrite SF. rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto. +- TrivialExists. simpl. + unfold Val.addl. destruct Archi.ptr64, x, y; auto. + + rewrite Int64.add_zero; auto. + + rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto. + + rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto. + + rewrite Int64.add_zero; auto. Qed. Theorem eval_subl: binary_constructor_sound subl Val.subl. @@ -411,11 +410,10 @@ Proof. - econstructor; split. apply eval_longconst. rewrite Int64.mul_commut; auto. - exploit (eval_mullimm_base n); eauto. intros (v2 & A2 & B2). exploit (eval_addlimm (Int64.mul n (Int64.repr n2))). eexact A2. intros (v3 & A3 & B3). - exists v3; split; auto. subst x. + exists v3; split; auto. destruct v1; simpl; auto. simpl in B2; inv B2. simpl in B3; inv B3. rewrite Int64.mul_add_distr_l. rewrite (Int64.mul_commut n). auto. - destruct Archi.ptr64; auto. - apply eval_mullimm_base; auto. Qed. @@ -449,7 +447,7 @@ Theorem eval_shrxlimm: exists v, eval_expr ge sp e m le (shrxlimm a n) v /\ Val.lessdef z v. Proof. unfold shrxlimm; intros. destruct Archi.splitlong eqn:SL. -+ eapply SplitLongproof.eval_shrxlimm; eauto. apply Archi.splitlong_ptr32; auto. ++ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32. + predSpec Int.eq Int.eq_spec n Int.zero. - subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto. change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto. @@ -492,7 +490,7 @@ Theorem eval_cmplu: eval_expr ge sp e m le (cmplu c a b) v. Proof. unfold cmplu; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_cmplu; eauto. apply Archi.splitlong_ptr32; auto. + eapply SplitLongproof.eval_cmplu; eauto using Archi.splitlong_ptr32. unfold Val.cmplu in H1. destruct (Val.cmplu_bool (Mem.valid_pointer m) c x y) as [vb|] eqn:C; simpl in H1; inv H1. destruct (is_longconst a) as [n1|] eqn:LC1; destruct (is_longconst b) as [n2|] eqn:LC2; diff --git a/ia32/SelectOp.vp b/x86/SelectOp.vp index db546d99..db546d99 100644 --- a/ia32/SelectOp.vp +++ b/x86/SelectOp.vp diff --git a/ia32/SelectOpproof.v b/x86/SelectOpproof.v index e201d207..ce15b6e1 100644 --- a/ia32/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -25,7 +25,6 @@ Require Import CminorSel. Require Import SelectOp. Open Local Scope cminorsel_scope. -Local Transparent Archi.ptr64. (** * Useful lemmas and tactics *) @@ -54,7 +53,7 @@ Ltac InvEval1 := Ltac InvEval2 := match goal with | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] => - simpl in H; inv H + simpl in H; FuncInv | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] => simpl in H; FuncInv | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] => @@ -65,7 +64,7 @@ Ltac InvEval2 := idtac end. -Ltac InvEval := InvEval1; InvEval2; InvEval2. +Ltac InvEval := InvEval1; InvEval2; InvEval2; subst. Ltac TrivialExists := match goal with @@ -128,27 +127,28 @@ Proof. predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero. subst. EvalOp. EvalOp. econstructor. EvalOp. simpl; eauto. econstructor. - unfold Olea_ptr; destruct Archi.ptr64 eqn:SF; simpl. - unfold Genv.symbol_address; destruct (Genv.find_symbol ge id); simpl; auto. - rewrite SF. rewrite Ptrofs.add_zero_l. fold (Ptrofs.to_int64 ofs). rewrite Ptrofs.of_int64_to_int64 by auto. auto. - unfold Genv.symbol_address; destruct (Genv.find_symbol ge id); simpl; auto. - rewrite SF. rewrite Ptrofs.add_zero_l. fold (Ptrofs.to_int ofs). rewrite Ptrofs.of_int_to_int by auto. auto. - EvalOp. rewrite eval_Olea_ptr. apply eval_addressing_Aglobal. + unfold Olea_ptr; destruct Archi.ptr64 eqn:SF; simpl; + [ rewrite <- Genv.shift_symbol_address_64 by auto | rewrite <- Genv.shift_symbol_address_32 by auto ]; + f_equal; f_equal; + rewrite Ptrofs.add_zero_l; + [ apply Ptrofs.of_int64_to_int64 | apply Ptrofs.of_int_to_int ]; + auto. + EvalOp. (*rewrite eval_Olea_ptr. apply eval_addressing_Aglobal. *) Qed. Theorem eval_addrstack: forall le ofs, exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.offset_ptr sp ofs) v. Proof. - intros. unfold addrstack. TrivialExists. rewrite eval_Olea_ptr. apply eval_addressing_Ainstack. + intros. unfold addrstack. TrivialExists. (*rewrite eval_Olea_ptr. apply eval_addressing_Ainstack.*) Qed. Theorem eval_notint: unary_constructor_sound notint Val.notint. Proof. - unfold notint; red; intros until x. case (notint_match a); intros. - InvEval. TrivialExists. - InvEval. subst x. rewrite Val.not_xor. rewrite Val.xor_assoc. TrivialExists. - TrivialExists. + unfold notint; red; intros until x. case (notint_match a); intros; InvEval. +- TrivialExists. +- rewrite Val.not_xor. rewrite Val.xor_assoc. TrivialExists. +- TrivialExists. Qed. Theorem eval_addimm: @@ -156,13 +156,13 @@ Theorem eval_addimm: Proof. red; unfold addimm; intros until x. predSpec Int.eq Int.eq_spec n Int.zero. - subst n. intros. exists x; split; auto. - destruct x; simpl; auto. rewrite Int.add_zero; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. - case (addimm_match a); intros; InvEval; simpl. - TrivialExists; simpl. rewrite Int.add_commut. auto. - inv H0. simpl in H6. TrivialExists. simpl. +- subst n. intros. exists x; split; auto. + destruct x; simpl; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. +- case (addimm_match a); intros; InvEval. ++ TrivialExists; simpl. rewrite Int.add_commut. auto. ++ inv H0. simpl in H6. TrivialExists. simpl. erewrite eval_offset_addressing_total_32 by eauto. rewrite Int.repr_signed; auto. - TrivialExists. simpl. rewrite Int.repr_signed; auto. ++ TrivialExists. simpl. rewrite Int.repr_signed; auto. Qed. Theorem eval_add: binary_constructor_sound add Val.add. @@ -176,50 +176,52 @@ Proof. apply Genv.shift_symbol_address_32; auto. } red; intros until y. unfold add; case (add_match a b); intros; InvEval. - rewrite Val.add_commut. apply eval_addimm; auto. - apply eval_addimm; auto. -- subst. TrivialExists. simpl. rewrite A, Val.add_permut_4. auto. -- subst. TrivialExists. simpl. rewrite A, Val.add_assoc. decEq; decEq. rewrite Val.add_permut. auto. -- subst. TrivialExists. simpl. rewrite A, Val.add_permut_4. rewrite <- Val.add_permut. rewrite <- Val.add_assoc. auto. -- subst. TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite ! Val.add_assoc. +- rewrite Val.add_commut. apply eval_addimm; auto. +- apply eval_addimm; auto. +- TrivialExists. simpl. rewrite A, Val.add_permut_4. auto. +- TrivialExists. simpl. rewrite A, Val.add_assoc. decEq; decEq. rewrite Val.add_permut. auto. +- TrivialExists. simpl. rewrite A, Val.add_permut_4. rewrite <- Val.add_permut. rewrite <- Val.add_assoc. auto. +- TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite ! Val.add_assoc. rewrite (Val.add_commut v1). rewrite Val.add_permut. rewrite Val.add_assoc. auto. -- subst. TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite Val.add_assoc. do 2 f_equal. apply Val.add_commut. -- subst. TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite !Val.add_assoc. +- TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite Val.add_assoc. do 2 f_equal. apply Val.add_commut. +- TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite !Val.add_assoc. rewrite (Val.add_commut (Vint (Int.repr n1))). rewrite Val.add_permut. do 2 f_equal. apply Val.add_commut. -- subst. TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite !Val.add_assoc. +- TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite !Val.add_assoc. rewrite (Val.add_commut (Vint (Int.repr n2))). rewrite Val.add_permut. auto. -- subst. TrivialExists. simpl. rewrite Val.add_permut. rewrite Val.add_assoc. +- TrivialExists. simpl. rewrite Val.add_permut. rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. -- subst. TrivialExists. -- subst. TrivialExists. simpl. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. -- subst. TrivialExists. simpl. rewrite Val.add_assoc; auto. -- TrivialExists. simpl. destruct x; destruct y; simpl; auto. - rewrite Int.add_zero; auto. - destruct Archi.ptr64 eqn:SF; simpl; auto. rewrite SF. rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto. - destruct Archi.ptr64 eqn:SF; simpl; auto. rewrite SF. rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto. +- TrivialExists. +- TrivialExists. simpl. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. +- TrivialExists. simpl. rewrite Val.add_assoc; auto. +- TrivialExists. simpl. + unfold Val.add; destruct Archi.ptr64, x, y; auto. + + rewrite Int.add_zero; auto. + + rewrite Int.add_zero; auto. + + rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto. + + rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto. Qed. Theorem eval_sub: binary_constructor_sound sub Val.sub. Proof. red; intros until y. unfold sub; case (sub_match a b); intros; InvEval. - rewrite Val.sub_add_opp. apply eval_addimm; auto. - subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r. +- rewrite Val.sub_add_opp. apply eval_addimm; auto. +- rewrite Val.sub_add_l. rewrite Val.sub_add_r. rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp. replace (Int.repr (n1 - n2)) with (Int.sub (Int.repr n1) (Int.repr n2)). apply eval_addimm; EvalOp. apply Int.eqm_samerepr; auto with ints. - subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp. - subst. rewrite Val.sub_add_r. replace (Int.repr (-n2)) with (Int.neg (Int.repr n2)). apply eval_addimm; EvalOp. +- rewrite Val.sub_add_l. apply eval_addimm; EvalOp. +- rewrite Val.sub_add_r. replace (Int.repr (-n2)) with (Int.neg (Int.repr n2)). apply eval_addimm; EvalOp. apply Int.eqm_samerepr; auto with ints. - TrivialExists. +- TrivialExists. Qed. Theorem eval_negint: unary_constructor_sound negint Val.neg. Proof. red; intros until x. unfold negint. case (negint_match a); intros; InvEval. - TrivialExists. - TrivialExists. +- TrivialExists. +- TrivialExists. Qed. Theorem eval_shlimm: @@ -231,30 +233,29 @@ Proof. intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto. destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl. destruct (shlimm_match a); intros; InvEval. - exists (Vint (Int.shl n1 n)); split. EvalOp. +- exists (Vint (Int.shl n1 n)); split. EvalOp. simpl. rewrite LT. auto. - destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. - exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp. - subst. destruct v1; simpl; auto. +- destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. ++ exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp. + destruct v1; simpl; auto. rewrite Heqb. destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto. destruct (Int.ltu n Int.iwordsize) eqn:?; simpl; auto. rewrite Int.add_commut. rewrite Int.shl_shl; auto. rewrite Int.add_commut; auto. - subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. ++ TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. simpl. auto. - subst. destruct (shift_is_scale n). - econstructor; split. EvalOp. simpl. eauto. +- destruct (shift_is_scale n). ++ econstructor; split. EvalOp. simpl. eauto. rewrite ! Int.repr_unsigned. destruct v1; simpl; auto. rewrite LT. rewrite Int.shl_mul. rewrite Int.mul_add_distr_l. rewrite (Int.shl_mul (Int.repr n1)). auto. - destruct Archi.ptr64; simpl; auto. - TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. auto. - destruct (shift_is_scale n). - econstructor; split. EvalOp. simpl. eauto. ++ TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. auto. +- destruct (shift_is_scale n). ++ econstructor; split. EvalOp. simpl. eauto. destruct x; simpl; auto. rewrite LT. rewrite Int.repr_unsigned. rewrite Int.add_zero. rewrite Int.shl_mul. auto. - TrivialExists. - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. ++ TrivialExists. +- intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto. Qed. @@ -267,18 +268,18 @@ Proof. intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto. destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl. destruct (shruimm_match a); intros; InvEval. - exists (Vint (Int.shru n1 n)); split. EvalOp. +- exists (Vint (Int.shru n1 n)); split. EvalOp. simpl. rewrite LT; auto. - destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. - exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp. +- destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. ++ exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp. subst. destruct v1; simpl; auto. rewrite Heqb. destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto. rewrite LT. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto. - subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. ++ TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. simpl. auto. - TrivialExists. - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. +- TrivialExists. +- intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto. Qed. @@ -291,19 +292,19 @@ Proof. intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto. destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl. destruct (shrimm_match a); intros; InvEval. - exists (Vint (Int.shr n1 n)); split. EvalOp. +- exists (Vint (Int.shr n1 n)); split. EvalOp. simpl. rewrite LT; auto. - destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. - exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp. +- destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?. ++ exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp. subst. destruct v1; simpl; auto. rewrite Heqb. destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto. rewrite LT. rewrite Int.add_commut. rewrite Int.shr_shr; auto. rewrite Int.add_commut; auto. - subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. ++ TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. simpl. auto. - TrivialExists. - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. +- TrivialExists. +- intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto. Qed. @@ -343,23 +344,23 @@ Proof. predSpec Int.eq Int.eq_spec n Int.one. intros. exists x; split; auto. destruct x; simpl; auto. subst n. rewrite Int.mul_one. auto. - case (mulimm_match a); intros; InvEval. - TrivialExists. simpl. rewrite Int.mul_commut; auto. - subst. rewrite Val.mul_add_distr_l. +- case (mulimm_match a); intros; InvEval. ++ TrivialExists. simpl. rewrite Int.mul_commut; auto. ++ rewrite Val.mul_add_distr_l. exploit eval_mulimm_base; eauto. instantiate (1 := n). intros [v' [A1 B1]]. exploit (eval_addimm (Int.mul n (Int.repr n2)) le (mulimm_base n t2) v'). auto. intros [v'' [A2 B2]]. exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto. rewrite Val.mul_commut; auto. - apply eval_mulimm_base; auto. ++ apply eval_mulimm_base; auto. Qed. Theorem eval_mul: binary_constructor_sound mul Val.mul. Proof. red; intros until y. unfold mul; case (mul_match a b); intros; InvEval. - rewrite Val.mul_commut. apply eval_mulimm. auto. - apply eval_mulimm. auto. - TrivialExists. +- rewrite Val.mul_commut. apply eval_mulimm. auto. +- apply eval_mulimm. auto. +- TrivialExists. Qed. Theorem eval_andimm: @@ -373,21 +374,21 @@ Proof. intros. exists x; split; auto. destruct x; simpl; auto. subst n. rewrite Int.and_mone. auto. case (andimm_match a); intros; InvEval. - TrivialExists. simpl. rewrite Int.and_commut; auto. - subst. TrivialExists. simpl. rewrite Val.and_assoc. rewrite Int.and_commut. auto. - subst. rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. +- TrivialExists. simpl. rewrite Int.and_commut; auto. +- TrivialExists. simpl. rewrite Val.and_assoc. rewrite Int.and_commut. auto. +- rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. rewrite Int.and_commut. auto. compute; auto. - subst. rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. +- rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. rewrite Int.and_commut. auto. compute; auto. - TrivialExists. +- TrivialExists. Qed. Theorem eval_and: binary_constructor_sound and Val.and. Proof. red; intros until y; unfold and; case (and_match a b); intros; InvEval. - rewrite Val.and_commut. apply eval_andimm; auto. - apply eval_andimm; auto. - TrivialExists. +- rewrite Val.and_commut. apply eval_andimm; auto. +- apply eval_andimm; auto. +- TrivialExists. Qed. Theorem eval_orimm: @@ -401,9 +402,9 @@ Proof. intros. exists (Vint Int.mone); split. EvalOp. destruct x; simpl; auto. subst n. rewrite Int.or_mone. auto. destruct (orimm_match a); intros; InvEval. - TrivialExists. simpl. rewrite Int.or_commut; auto. - subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists. - TrivialExists. +- TrivialExists. simpl. rewrite Int.or_commut; auto. +- subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists. +- TrivialExists. Qed. Remark eval_same_expr: @@ -430,10 +431,10 @@ Qed. Lemma eval_or: binary_constructor_sound or Val.or. Proof. red; intros until y; unfold or; case (or_match a b); intros. -(* intconst *) - InvEval. rewrite Val.or_commut. apply eval_orimm; auto. - InvEval. apply eval_orimm; auto. -(* shlimm - shruimm *) + (* intconst *) +- InvEval. rewrite Val.or_commut. apply eval_orimm; auto. +- InvEval. apply eval_orimm; auto. +- (* shlimm - shruimm *) predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize. destruct (same_expr_pure t1 t2) eqn:?. InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. @@ -442,10 +443,10 @@ Proof. destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto. destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto. simpl. rewrite <- Int.or_ror; auto. - InvEval. exists (Val.or x y); split. EvalOp. - simpl. erewrite int_add_sub_eq; eauto. rewrite H0; rewrite H; auto. auto. + InvEval. econstructor; split; eauto. EvalOp. + simpl. erewrite int_add_sub_eq; eauto. TrivialExists. -(* shruimm - shlimm *) +- (* shruimm - shlimm *) predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize. destruct (same_expr_pure t1 t2) eqn:?. InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. @@ -454,11 +455,11 @@ Proof. destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto. destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto. simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto. - InvEval. exists (Val.or y x); split. EvalOp. - simpl. erewrite int_add_sub_eq; eauto. rewrite H0; rewrite H; auto. + InvEval. econstructor; split; eauto. EvalOp. + simpl. erewrite int_add_sub_eq; eauto. rewrite Val.or_commut; auto. TrivialExists. -(* default *) +- (* default *) TrivialExists. Qed. @@ -470,19 +471,19 @@ Proof. intros. exists x; split. auto. destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto. destruct (xorimm_match a); intros; InvEval. - TrivialExists. simpl. rewrite Int.xor_commut; auto. - subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. - subst. rewrite Val.not_xor. rewrite Val.xor_assoc. +- TrivialExists. simpl. rewrite Int.xor_commut; auto. +- rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. +- rewrite Val.not_xor. rewrite Val.xor_assoc. rewrite (Val.xor_commut (Vint Int.mone)). TrivialExists. - TrivialExists. +- TrivialExists. Qed. Theorem eval_xor: binary_constructor_sound xor Val.xor. Proof. red; intros until y; unfold xor; case (xor_match a b); intros; InvEval. - rewrite Val.xor_commut. apply eval_xorimm; auto. - apply eval_xorimm; auto. - TrivialExists. +- rewrite Val.xor_commut. apply eval_xorimm; auto. +- apply eval_xorimm; auto. +- TrivialExists. Qed. Theorem eval_divs_base: @@ -545,22 +546,22 @@ Qed. Theorem eval_shl: binary_constructor_sound shl Val.shl. Proof. red; intros until y; unfold shl; case (shl_match b); intros. - InvEval. apply eval_shlimm; auto. - TrivialExists. +- InvEval. apply eval_shlimm; auto. +- TrivialExists. Qed. Theorem eval_shr: binary_constructor_sound shr Val.shr. Proof. red; intros until y; unfold shr; case (shr_match b); intros. - InvEval. apply eval_shrimm; auto. - TrivialExists. +- InvEval. apply eval_shrimm; auto. +- TrivialExists. Qed. Theorem eval_shru: binary_constructor_sound shru Val.shru. Proof. red; intros until y; unfold shru; case (shru_match b); intros. - InvEval. apply eval_shruimm; auto. - TrivialExists. +- InvEval. apply eval_shruimm; auto. +- TrivialExists. Qed. Theorem eval_negf: unary_constructor_sound negf Val.negf. @@ -633,9 +634,9 @@ Lemma eval_compimm: Proof. intros until x. unfold compimm; case (compimm_match c a); intros. -(* constant *) +- (* constant *) InvEval. rewrite sem_int. TrivialExists. simpl. destruct (intsem c0 n1 n2); auto. -(* eq cmp *) +- (* eq cmp *) InvEval. inv H. simpl in H5. inv H5. destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. simpl. rewrite eval_negate_condition. @@ -650,7 +651,7 @@ Proof. destruct (eval_condition c0 vl m); simpl. unfold Vtrue, Vfalse. destruct b; rewrite sem_eq; rewrite Int.eq_false; auto. rewrite sem_undef; auto. -(* ne cmp *) +- (* ne cmp *) InvEval. inv H. simpl in H5. inv H5. destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists. simpl. destruct (eval_condition c0 vl m); simpl. @@ -664,19 +665,19 @@ Proof. destruct (eval_condition c0 vl m); simpl. unfold Vtrue, Vfalse. destruct b; rewrite sem_ne; rewrite Int.eq_false; auto. rewrite sem_undef; auto. -(* eq andimm *) +- (* eq andimm *) destruct (Int.eq_dec n2 Int.zero). InvEval; subst. econstructor; split. EvalOp. simpl; eauto. destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_eq. destruct (Int.eq (Int.and i n1) Int.zero); auto. TrivialExists. simpl. rewrite sem_default. auto. -(* ne andimm *) +- (* ne andimm *) destruct (Int.eq_dec n2 Int.zero). InvEval; subst. econstructor; split. EvalOp. simpl; eauto. destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_ne. destruct (Int.eq (Int.and i n1) Int.zero); auto. TrivialExists. simpl. rewrite sem_default. auto. -(* default *) +- (* default *) TrivialExists. simpl. rewrite sem_default. auto. Qed. @@ -944,12 +945,12 @@ Proof. intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval. - constructor. - constructor. -- destruct Archi.ptr64; inv H0. constructor. -- destruct Archi.ptr64; inv H0. constructor. -- destruct Archi.ptr64; inv H0. constructor. -- destruct Archi.ptr64; inv H0. constructor. +- constructor. +- constructor. +- constructor. +- constructor. - simpl in H5. inv H5. constructor. -- subst v. constructor; auto. +- constructor; auto. - inv H. InvEval. rewrite eval_addressing_Aglobal in H6. inv H6. constructor; auto. - inv H. InvEval. rewrite eval_addressing_Ainstack in H6. inv H6. constructor; auto. - constructor; auto. diff --git a/ia32/Stacklayout.v b/x86/Stacklayout.v index 44fd43b2..44fd43b2 100644 --- a/ia32/Stacklayout.v +++ b/x86/Stacklayout.v diff --git a/ia32/TargetPrinter.ml b/x86/TargetPrinter.ml index 33d47830..33d47830 100644 --- a/ia32/TargetPrinter.ml +++ b/x86/TargetPrinter.ml diff --git a/ia32/ValueAOp.v b/x86/ValueAOp.v index 98f0dbb1..1021a9c8 100644 --- a/ia32/ValueAOp.v +++ b/x86/ValueAOp.v @@ -14,8 +14,6 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats Values Memory Globalenvs. Require Import Op RTL ValueDomain. -Local Transparent Archi.ptr64. - (** Value analysis for x86_64 operators *) Definition eval_static_condition (cond: condition) (vl: list aval): abool := diff --git a/ia32/extractionMachdep.v b/x86/extractionMachdep.v index 8b395579..14cb6447 100644 --- a/ia32/extractionMachdep.v +++ b/x86/extractionMachdep.v @@ -12,12 +12,7 @@ (* Additional extraction directives specific to the x86-64 port *) -Require Archi SelectOp ConstpropOp. - -(* Archi *) - -Extract Constant Archi.ptr64 => - "Configuration.model = ""64"" ". +Require SelectOp ConstpropOp. (* SelectOp *) diff --git a/ia32/Archi.v b/x86_32/Archi.v index 936bacb3..29073be8 100644 --- a/ia32/Archi.v +++ b/x86_32/Archi.v @@ -14,18 +14,18 @@ (* *) (* *********************************************************************) -(** Architecture-dependent parameters for IA32 *) +(** Architecture-dependent parameters for x86 in 32-bit mode *) Require Import ZArith. Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. -Parameter ptr64: bool. +Definition ptr64 := false. Definition big_endian := false. -Definition align_int64 := if ptr64 then 8%Z else 4%Z. -Definition align_float64 := if ptr64 then 8%Z else 4%Z. +Definition align_int64 := 4%Z. +Definition align_float64 := 4%Z. Definition splitlong := negb ptr64. diff --git a/x86_64/Archi.v b/x86_64/Archi.v new file mode 100644 index 00000000..7b1136c8 --- /dev/null +++ b/x86_64/Archi.v @@ -0,0 +1,54 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris *) +(* Jacques-Henri Jourdan, INRIA Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Architecture-dependent parameters for x86 in 64-bit mode *) + +Require Import ZArith. +Require Import Fappli_IEEE. +Require Import Fappli_IEEE_bits. + +Definition ptr64 := true. + +Definition big_endian := false. + +Definition align_int64 := 8%Z. +Definition align_float64 := 8%Z. + +Definition splitlong := negb ptr64. + +Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. +Proof. + unfold splitlong. destruct ptr64; simpl; congruence. +Qed. + +Program Definition default_pl_64 : bool * nan_pl 53 := + (true, iter_nat 51 _ xO xH). + +Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) := + false. (**r always choose first NaN *) + +Program Definition default_pl_32 : bool * nan_pl 24 := + (true, iter_nat 22 _ xO xH). + +Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) := + false. (**r always choose first NaN *) + +Definition float_of_single_preserves_sNaN := false. + +Global Opaque ptr64 big_endian splitlong + default_pl_64 choose_binop_pl_64 + default_pl_32 choose_binop_pl_32 + float_of_single_preserves_sNaN. |