diff options
| -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. |