From f21a6b181dded86ef0e5c7ab94f74e5b960fd510 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 2 Oct 2016 16:17:51 +0200 Subject: Improve code generation for 64-bit signed integer division Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv. --- .depend | 40 +++++++------- backend/SelectDiv.vp | 65 ++++++++++++++++++++--- backend/SelectDivproof.v | 119 +++++++++++++++++++++++++++++++++++++++++- backend/Selection.v | 6 +-- backend/Selectionproof.v | 4 +- backend/SplitLong.vp | 43 ++++----------- backend/SplitLongproof.v | 133 +++++++++++++++++------------------------------ backend/ValueDomain.v | 18 ++++++- common/Values.v | 100 +++++++++++++++++++++++++++++++++++ ia32/Asmgen.v | 11 ++++ ia32/Asmgenproof.v | 7 +++ ia32/Asmgenproof1.v | 41 +++++++++++++++ ia32/ConstpropOp.vp | 9 ++++ ia32/ConstpropOpproof.v | 17 ++++++ ia32/Machregs.v | 3 ++ ia32/NeedOp.v | 1 + ia32/Op.v | 5 ++ ia32/PrintOp.ml | 1 + ia32/SelectLong.vp | 51 +++++------------- ia32/SelectLongproof.v | 38 +++++++++----- ia32/ValueAOp.v | 1 + lib/Integers.v | 37 +++++++++++++ 22 files changed, 547 insertions(+), 203 deletions(-) diff --git a/.depend b/.depend index d4e6961e..cb8fbab3 100644 --- a/.depend +++ b/.depend @@ -74,18 +74,18 @@ backend/CminorSel.vo backend/CminorSel.glob backend/CminorSel.v.beautified: back 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/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/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/SelectDiv.vo backend/SplitLong.vo $(ARCH)/SelectLong.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/SelectDiv.vio backend/SplitLong.vio $(ARCH)/SelectLong.vio $(ARCH)/Machregs.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/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/SelectDiv.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 @@ -124,8 +124,8 @@ backend/Liveness.vo backend/Liveness.glob backend/Liveness.v.beautified: backend 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/ValueDomain.vo backend/RTL.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/ValueDomain.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 @@ -162,8 +162,8 @@ $(ARCH)/Machregs.vo $(ARCH)/Machregs.glob $(ARCH)/Machregs.v.beautified: $(ARCH) $(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 common/Events.vo backend/Locations.vo -$(ARCH)/Conventions1.vio: $(ARCH)/Conventions1.v lib/Coqlib.vio lib/Decidableplus.vio common/AST.vio common/Events.vio backend/Locations.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 @@ -196,20 +196,20 @@ backend/Mach.vo backend/Mach.glob backend/Mach.v.beautified: backend/Mach.v lib/ 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/Memory.vo common/Separation.vo backend/Bounds.vo -$(ARCH)/Stacklayout.vio: $(ARCH)/Stacklayout.v lib/Coqlib.vio common/Memory.vio common/Separation.vio backend/Bounds.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 lib/Integers.vo lib/Floats.vo common/AST.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 lib/Integers.vio lib/Floats.vio common/AST.vio common/Memdata.vio $(ARCH)/Op.vio backend/Locations.vio backend/Mach.vio $(ARCH)/Asm.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/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Asmgenproof0.vo backend/Conventions.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/Mach.vio $(ARCH)/Asm.vio $(ARCH)/Asmgen.vio backend/Asmgenproof0.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 @@ -224,12 +224,12 @@ cfrontend/Ctyping.vo cfrontend/Ctyping.glob cfrontend/Ctyping.v.beautified: cfro 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 common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo -cfrontend/Cexec.vio: cfrontend/Cexec.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/Determinism.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Cstrategy.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 common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Ctypes.vo cfrontend/Cop.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo -cfrontend/Initializersproof.vio: cfrontend/Initializersproof.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/Globalenvs.vio common/Events.vio common/Smallstep.vio cfrontend/Ctypes.vio cfrontend/Cop.vio cfrontend/Csyntax.vio cfrontend/Csem.vio cfrontend/Initializers.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 diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index d708afb7..1fc0b689 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -14,12 +14,8 @@ Require Import Coqlib. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. -Require Import SelectOp. +Require Import AST Integers Floats. +Require Import Op CminorSel SelectOp SplitLong SelectLong. Open Local Scope cminorsel_scope. @@ -201,6 +197,63 @@ Nondetfunction mods (e1: expr) (e2: expr) := | _ => mods_base e1 e2 end. +(** 64-bit integer divisions *) + +Section SELECT. + +Context {hf: helper_functions}. + +Definition modl_from_divl (equo: expr) (n: int64) := + subl (Eletvar O) (mullimm n equo). + +Definition divlu (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.divu n1 n2) + | Some n2, _ => + match Int64.is_power2' n2 with + | Some l => shrluimm e1 l + | None => divlu_base e1 e2 + end (* TODO: multiply-high *) + | _, _ => divlu_base e1 e2 + end. + +Definition modlu (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.modu n1 n2) + | Some n2, _ => + match Int64.is_power2 n2 with + | Some l => andl e1 (longconst (Int64.sub n2 Int64.one)) + | None => modlu_base e1 e2 + end + | _, _ => modlu_base e1 e2 + end. + +Definition divls (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.divs n1 n2) + | Some n2, _ => + match Int64.is_power2' n2 with + | Some l => if Int.ltu l (Int.repr 63) then shrxlimm e1 l else divls_base e1 e2 + | None => divls_base e1 e2 + end (* TODO: multiply-high *) + | _, _ => divls_base e1 e2 + end. + +Definition modls (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.mods n1 n2) + | Some n2, _ => + match Int64.is_power2' n2 with + | Some l => if Int.ltu l (Int.repr 63) + then Elet e1 (modl_from_divl (shrxlimm (Eletvar O) l) n2) + else modls_base e1 e2 + | None => modls_base e1 e2 + end + | _, _ => modls_base e1 e2 + end. + +End SELECT. + (** Floating-point division by a constant can also be turned into a FP multiplication by the inverse constant, but only for powers of 2. *) diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 5621acd5..441f69b1 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -15,7 +15,7 @@ Require Import Zquot Coqlib. Require Import AST Integers Floats Values Memory Globalenvs Events. Require Import Cminor Op CminorSel. -Require Import SelectOp SelectOpproof SelectDiv. +Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv. Open Local Scope cminorsel_scope. @@ -321,7 +321,10 @@ Qed. Section CMCONSTRS. -Variable ge: genv. +Variable prog: program. +Variable hf: helper_functions. +Hypothesis HELPERS: helper_functions_declared prog hf. +Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. @@ -543,6 +546,118 @@ Proof. - eapply eval_mods_base; eauto. Qed. +Lemma eval_modl_from_divl: + forall le a n x y, + eval_expr ge sp e m le a (Vlong y) -> + nth_error le O = Some (Vlong x) -> + eval_expr ge sp e m le (modl_from_divl a n) (Vlong (Int64.sub x (Int64.mul y n))). +Proof. + unfold modl_from_divl; intros. + exploit eval_mullimm; eauto. instantiate (1 := n). intros (v1 & A1 & B1). + exploit (eval_subl prog sp e m le (Eletvar O)). constructor; eauto. eexact A1. + intros (v2 & A2 & B2). + simpl in B1; inv B1. simpl in B2; inv B2. exact A2. +Qed. + +Theorem eval_divlu: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.divlu x y = Some z -> + exists v, eval_expr ge sp e m le (divlu a b) v /\ Val.lessdef z v. +Proof. + unfold divlu; intros. + destruct (is_longconst b) as [n2|] eqn:N2. +- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y. + destruct (is_longconst a) as [n1|] eqn:N1. ++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x. + simpl in H1. destruct (Int64.eq n2 Int64.zero); inv H1. + econstructor; split. apply eval_longconst. constructor. ++ destruct (Int64.is_power2' n2) as [l|] eqn:POW. +* exploit Val.divlu_pow2; eauto. intros EQ; subst z. apply eval_shrluimm; auto. +* eapply eval_divlu_base; eauto. +- eapply eval_divlu_base; eauto. +Qed. + +Theorem eval_modlu: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.modlu x y = Some z -> + exists v, eval_expr ge sp e m le (modlu a b) v /\ Val.lessdef z v. +Proof. + unfold modlu; intros. + destruct (is_longconst b) as [n2|] eqn:N2. +- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y. + destruct (is_longconst a) as [n1|] eqn:N1. ++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x. + simpl in H1. destruct (Int64.eq n2 Int64.zero); inv H1. + econstructor; split. apply eval_longconst. constructor. ++ destruct (Int64.is_power2 n2) as [l|] eqn:POW. +* exploit Val.modlu_pow2; eauto. intros EQ; subst z. eapply eval_andl; eauto. apply eval_longconst. +* eapply eval_modlu_base; eauto. +- eapply eval_modlu_base; eauto. +Qed. + +Theorem eval_divls: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.divls x y = Some z -> + exists v, eval_expr ge sp e m le (divls a b) v /\ Val.lessdef z v. +Proof. + unfold divls; intros. + destruct (is_longconst b) as [n2|] eqn:N2. +- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y. + destruct (is_longconst a) as [n1|] eqn:N1. ++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x. + simpl in H1. + destruct (Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1. + econstructor; split. apply eval_longconst. constructor. ++ destruct (Int64.is_power2' n2) as [l|] eqn:POW. +* destruct (Int.ltu l (Int.repr 63)) eqn:LT. +** exploit Val.divls_pow2; eauto. intros EQ. eapply eval_shrxlimm; eauto. +** eapply eval_divls_base; eauto. +* eapply eval_divls_base; eauto. +- eapply eval_divls_base; eauto. +Qed. + +Theorem eval_modls: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.modls x y = Some z -> + exists v, eval_expr ge sp e m le (modls a b) v /\ Val.lessdef z v. +Proof. + unfold modls; intros. + destruct (is_longconst b) as [n2|] eqn:N2. +- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y. + destruct (is_longconst a) as [n1|] eqn:N1. ++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x. + simpl in H1. + destruct (Int64.eq n2 Int64.zero + || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1. + econstructor; split. apply eval_longconst. constructor. ++ destruct (Int64.is_power2' n2) as [l|] eqn:POW. +* destruct (Int.ltu l (Int.repr 63)) eqn:LT. +**destruct x; simpl in H1; try discriminate. + destruct (Int64.eq n2 Int64.zero + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone) eqn:D; inv H1. + assert (Val.divls (Vlong i) (Vlong n2) = Some (Vlong (Int64.divs i n2))). + { simpl; rewrite D; auto. } + exploit Val.divls_pow2; eauto. intros EQ. + set (le' := Vlong i :: le). + assert (A: eval_expr ge sp e m le' (Eletvar O) (Vlong i)) by (constructor; auto). + exploit eval_shrxlimm; eauto. intros (v1 & A1 & B1). inv B1. + econstructor; split. + econstructor. eauto. eapply eval_modl_from_divl. eexact A1. reflexivity. + rewrite Int64.mods_divs. auto. +**eapply eval_modls_base; eauto. +* eapply eval_modls_base; eauto. +- eapply eval_modls_base; eauto. +Qed. + (** * Floating-point division *) Theorem eval_divf: diff --git a/backend/Selection.v b/backend/Selection.v index 3aff446e..5cb5d119 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -27,7 +27,7 @@ Require Import Coqlib Maps. Require Import AST Errors Integers Globalenvs Switch. Require Cminor. Require Import Op CminorSel. -Require Import SelectOp SelectDiv SplitLong SelectLong. +Require Import SelectOp SplitLong SelectLong SelectDiv. Require Machregs. Local Open Scope cminorsel_scope. @@ -138,9 +138,9 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := | Cminor.Oaddl => addl arg1 arg2 | Cminor.Osubl => subl arg1 arg2 | Cminor.Omull => mull arg1 arg2 - | Cminor.Odivl => divl arg1 arg2 + | Cminor.Odivl => divls arg1 arg2 | Cminor.Odivlu => divlu arg1 arg2 - | Cminor.Omodl => modl arg1 arg2 + | Cminor.Omodl => modls arg1 arg2 | Cminor.Omodlu => modlu arg1 arg2 | Cminor.Oandl => andl arg1 arg2 | Cminor.Oorl => orl arg1 arg2 diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 34157553..90e50338 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -305,9 +305,9 @@ Proof. eapply eval_addl; eauto. eapply eval_subl; eauto. eapply eval_mull; eauto. - eapply eval_divl; eauto. + eapply eval_divls; eauto. eapply eval_divlu; eauto. - eapply eval_modl; eauto. + eapply eval_modls; eauto. eapply eval_modlu; eauto. eapply eval_andl; eauto. eapply eval_orl; eauto. diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index 305e20f3..5891adef 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -255,38 +255,17 @@ Definition mull (e1 e2: expr) := | _, _ => mull_base e1 e2 end. -Definition binop_long (id: ident) (sem: int64 -> int64 -> int64) (e1 e2: expr) := - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (sem n1 n2) - | _, _ => Eexternal id sig_ll_l (e1 ::: e2 ::: Enil) - end. - -Definition divl e1 e2 := binop_long i64_sdiv Int64.divs e1 e2. -Definition modl e1 e2 := binop_long i64_smod Int64.mods e1 e2. - -Definition divlu (e1 e2: expr) := - let default := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil) in - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.divu n1 n2) - | _, Some n2 => - match Int64.is_power2' n2 with - | Some l => shrluimm e1 l - | None => default - end - | _, _ => default - end. - -Definition modlu (e1 e2: expr) := - let default := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil) in - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.modu n1 n2) - | _, Some n2 => - match Int64.is_power2 n2 with - | Some l => andl e1 (longconst (Int64.sub n2 Int64.one)) - | None => default - end - | _, _ => default - end. +Definition shrxlimm (e: expr) (n: int) := + if Int.eq n Int.zero then e else + Elet e (shrlimm (addl (Eletvar O) + (shrluimm (shrlimm (Eletvar O) (Int.repr 63)) + (Int.sub (Int.repr 64) n))) + n). + +Definition divlu_base (e1 e2: expr) := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil). +Definition modlu_base (e1 e2: expr) := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil). +Definition divls_base (e1 e2: expr) := Eexternal i64_sdiv sig_ll_l (e1 ::: e2 ::: Enil). +Definition modls_base (e1 e2: expr) := Eexternal i64_smod sig_ll_l (e1 ::: e2 ::: Enil). Definition cmpl_eq_zero (e: expr) := splitlong e (fun h l => comp Ceq (or h l) (Eop (Ointconst Int.zero) Enil)). diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v index 1dbe25bd..57fc6b56 100644 --- a/backend/SplitLongproof.v +++ b/backend/SplitLongproof.v @@ -823,118 +823,79 @@ Proof. - apply eval_mull_base; auto. Qed. -Lemma eval_binop_long: - forall id name sem le a b x y z, - (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) -> - helper_declared prog id name sig_ll_l -> - external_implements name sig_ll_l (x::y::nil) z -> +Theorem eval_shrxlimm: + forall le a n x z, + Archi.ptr64 = false -> eval_expr ge sp e m le a x -> - eval_expr ge sp e m le b y -> - exists v, eval_expr ge sp e m le (binop_long id sem a b) v /\ Val.lessdef z v. + Val.shrxl x (Vint n) = Some z -> + exists v, eval_expr ge sp e m le (shrxlimm a n) v /\ Val.lessdef z v. Proof. - intros. unfold binop_long. - destruct (is_longconst a) as [p|] eqn:LC1. - destruct (is_longconst b) as [q|] eqn:LC2. - exploit is_longconst_sound. eexact LC1. eauto. intros EQ; subst x. - exploit is_longconst_sound. eexact LC2. eauto. intros EQ; subst y. - econstructor; split. EvalOp. erewrite H by eauto. rewrite Int64.ofwords_recompose. auto. - econstructor; split. eapply eval_helper_2; eauto. auto. - econstructor; split. eapply eval_helper_2; eauto. auto. + intros. + apply Val.shrxl_shrl_2 in H1. unfold shrxlimm. + destruct (Int.eq n Int.zero). +- subst z; exists x; auto. +- set (le' := x :: le). + edestruct (eval_shrlimm (Int.repr 63) le' (Eletvar O)) as (v1 & A1 & B1). + constructor. reflexivity. + edestruct (eval_shrluimm (Int.sub (Int.repr 64) n) le') as (v2 & A2 & B2). + eexact A1. + edestruct (eval_addl H le' (Eletvar 0)) as (v3 & A3 & B3). + constructor. reflexivity. eexact A2. + edestruct (eval_shrlimm n le') as (v4 & A4 & B4). eexact A3. + exists v4; split. + econstructor; eauto. + assert (X: forall v1 v2 n, Val.lessdef v1 v2 -> Val.lessdef (Val.shrl v1 (Vint n)) (Val.shrl v2 (Vint n))). + { intros. inv H2; auto. } + assert (Y: forall v1 v2 n, Val.lessdef v1 v2 -> Val.lessdef (Val.shrlu v1 (Vint n)) (Val.shrlu v2 (Vint n))). + { intros. inv H2; auto. } + subst z. eapply Val.lessdef_trans; [|eexact B4]. apply X. + eapply Val.lessdef_trans; [|eexact B3]. apply Val.addl_lessdef; auto. + eapply Val.lessdef_trans; [|eexact B2]. apply Y. + auto. Qed. -Theorem eval_divl: +Theorem eval_divlu_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> - Val.divls x y = Some z -> - exists v, eval_expr ge sp e m le (divl a b) v /\ Val.lessdef z v. + Val.divlu x y = Some z -> + exists v, eval_expr ge sp e m le (divlu_base a b) v /\ Val.lessdef z v. Proof. - intros. eapply eval_binop_long; eauto. - intros; subst; simpl in H1. - destruct (Int64.eq q Int64.zero - || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. - auto. - DeclHelper. UseHelper. + intros; unfold divlu_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. -Theorem eval_modl: +Theorem eval_modlu_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> - Val.modls x y = Some z -> - exists v, eval_expr ge sp e m le (modl a b) v /\ Val.lessdef z v. + Val.modlu x y = Some z -> + exists v, eval_expr ge sp e m le (modlu_base a b) v /\ Val.lessdef z v. Proof. - intros. eapply eval_binop_long; eauto. - intros; subst; simpl in H1. - destruct (Int64.eq q Int64.zero - || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. - auto. - DeclHelper. UseHelper. + intros; unfold modlu_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. -Theorem eval_divlu: +Theorem eval_divsu_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> - Val.divlu x y = Some z -> - exists v, eval_expr ge sp e m le (divlu a b) v /\ Val.lessdef z v. + Val.divls x y = Some z -> + exists v, eval_expr ge sp e m le (divls_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold divlu. - set (default := Eexternal i64_udiv sig_ll_l (a ::: b ::: Enil)). - assert (DEFAULT: - exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v). - { - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. - } - destruct (is_longconst a) as [p|] eqn:LC1; - destruct (is_longconst b) as [q|] eqn:LC2. -- exploit (is_longconst_sound le a); eauto. intros EQ; subst x. - exploit (is_longconst_sound le b); eauto. intros EQ; subst y. - econstructor; split. apply eval_longconst. - simpl in H1. destruct (Int64.eq q Int64.zero); inv H1. auto. -- auto. -- destruct (Int64.is_power2' q) as [l|] eqn:P2; auto. - exploit (is_longconst_sound le b); eauto. intros EQ; subst y. - replace z with (Val.shrlu x (Vint l)). - apply eval_shrluimm. auto. - destruct x; simpl in H1; try discriminate. - destruct (Int64.eq q Int64.zero); inv H1. - simpl. erewrite Int64.is_power2'_range by eauto. - erewrite Int64.divu_pow2' by eauto. - auto. -- auto. + intros; unfold divls_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. -Theorem eval_modlu: +Theorem eval_modls_base: forall le a b x y z, eval_expr ge sp e m le a x -> eval_expr ge sp e m le b y -> - Val.modlu x y = Some z -> - exists v, eval_expr ge sp e m le (modlu a b) v /\ Val.lessdef z v. + Val.modls x y = Some z -> + exists v, eval_expr ge sp e m le (modls_base a b) v /\ Val.lessdef z v. Proof. - intros. unfold modlu. - set (default := Eexternal i64_umod sig_ll_l (a ::: b ::: Enil)). - assert (DEFAULT: - exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v). - { - econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. - } - destruct (is_longconst a) as [p|] eqn:LC1; - destruct (is_longconst b) as [q|] eqn:LC2. -- exploit (is_longconst_sound le a); eauto. intros EQ; subst x. - exploit (is_longconst_sound le b); eauto. intros EQ; subst y. - econstructor; split. apply eval_longconst. - simpl in H1. destruct (Int64.eq q Int64.zero); inv H1. auto. -- auto. -- destruct (Int64.is_power2 q) as [l|] eqn:P2; auto. - exploit (is_longconst_sound le b); eauto. intros EQ; subst y. - replace z with (Val.andl x (Vlong (Int64.sub q Int64.one))). - apply eval_andl. auto. apply eval_longconst. - destruct x; simpl in H1; try discriminate. - destruct (Int64.eq q Int64.zero); inv H1. - simpl. - erewrite Int64.modu_and by eauto. auto. -- auto. + intros; unfold modls_base. + econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. Qed. Remark decompose_cmpl_eq_zero: diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 6b314904..bf88a450 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -1938,6 +1938,22 @@ Proof. inv H; inv H0; auto with va. simpl. rewrite E. constructor. Qed. +Definition shrxl (v w: aval) := + match v, w with + | L i, I j => if Int.ltu j (Int.repr 63) then L(Int64.shrx' i j) else ntop + | _, _ => ntop1 v + end. + +Lemma shrxl_sound: + forall v w u x y, vmatch v x -> vmatch w y -> Val.shrxl v w = Some u -> vmatch u (shrxl x y). +Proof. + intros. + destruct v; destruct w; try discriminate; simpl in H1. + destruct (Int.ltu i0 (Int.repr 63)) eqn:LTU; inv H1. + unfold shrxl; inv H; auto with va; inv H0; auto with va. + rewrite LTU; auto with va. +Qed. + (** Floating-point arithmetic operations *) Definition negf := unop_float Float.neg. @@ -4544,7 +4560,7 @@ Hint Resolve cnot_sound symbol_address_sound shll_sound shrl_sound shrlu_sound andl_sound orl_sound xorl_sound notl_sound roll_sound rorl_sound negl_sound addl_sound subl_sound mull_sound - divls_sound divlu_sound modls_sound modlu_sound + divls_sound divlu_sound modls_sound modlu_sound shrxl_sound negf_sound absf_sound addf_sound subf_sound mulf_sound divf_sound negfs_sound absfs_sound diff --git a/common/Values.v b/common/Values.v index d1058fe8..88506bab 100644 --- a/common/Values.v +++ b/common/Values.v @@ -713,6 +713,15 @@ Definition shrlu (v1 v2: val): val := | _, _ => Vundef end. +Definition shrxl (v1 v2: val): option val := + match v1, v2 with + | Vlong n1, Vint n2 => + if Int.ltu n2 (Int.repr 63) + then Some(Vlong(Int64.shrx' n1 n2)) + else None + | _, _ => None + end. + Definition roll (v1 v2: val): val := match v1, v2 with | Vlong n1, Vint n2 => Vlong(Int64.rol n1 (Int64.repr (Int.unsigned n2))) @@ -1240,6 +1249,32 @@ Proof. rewrite Int.shrx_shr; auto. destruct (Int.lt i Int.zero); simpl; rewrite H0; auto. Qed. +Theorem shrx_shr_2: + forall n x z, + shrx x (Vint n) = Some z -> + z = (if Int.eq n Int.zero then x else + shr (add x (shru (shr x (Vint (Int.repr 31))) + (Vint (Int.sub (Int.repr 32) n)))) + (Vint n)). +Proof. + intros. destruct x; simpl in H; try discriminate. + destruct (Int.ltu n (Int.repr 31)) eqn:LT; inv H. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31; intros LT'. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. change (Int.signed Int.one) with 1. + rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. +- simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl. + replace (Int.ltu n Int.iwordsize) with true. + f_equal; apply Int.shrx_shr_2; assumption. + symmetry; apply zlt_true. change (Int.unsigned n < 32); omega. + symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32. + assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } + rewrite Int.unsigned_repr. + change (Int.unsigned Int.iwordsize) with 32; omega. + assert (32 < Int.max_unsigned) by reflexivity. omega. +Qed. + Theorem or_rolm: forall x n m1 m2, or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2). @@ -1404,6 +1439,71 @@ Proof. destruct x; simpl; auto. Qed. +Theorem divls_pow2: + forall x n logn y, + Int64.is_power2' n = Some logn -> Int.ltu logn (Int.repr 63) = true -> + divls x (Vlong n) = Some y -> + shrxl x (Vint logn) = Some y. +Proof. + intros; destruct x; simpl in H1; inv H1. + destruct (Int64.eq n Int64.zero + || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n Int64.mone); inv H3. + simpl. rewrite H0. decEq. decEq. + generalize (Int64.is_power2'_correct _ _ H); intro. + unfold Int64.shrx'. rewrite Int64.shl'_mul_two_p. rewrite <- H1. + rewrite Int64.mul_commut. rewrite Int64.mul_one. + rewrite Int64.repr_unsigned. auto. +Qed. + +Theorem divlu_pow2: + forall x n logn y, + Int64.is_power2' n = Some logn -> + divlu x (Vlong n) = Some y -> + shrlu x (Vint logn) = y. +Proof. + intros; destruct x; simpl in H0; inv H0. + destruct (Int64.eq n Int64.zero); inv H2. + simpl. + rewrite (Int64.is_power2'_range _ _ H). + decEq. symmetry. apply Int64.divu_pow2'. auto. +Qed. + +Theorem modlu_pow2: + forall x n logn y, + Int64.is_power2 n = Some logn -> + modlu x (Vlong n) = Some y -> + andl x (Vlong (Int64.sub n Int64.one)) = y. +Proof. + intros; destruct x; simpl in H0; inv H0. + destruct (Int64.eq n Int64.zero); inv H2. + simpl. decEq. symmetry. eapply Int64.modu_and; eauto. +Qed. + +Theorem shrxl_shrl_2: + forall n x z, + shrxl x (Vint n) = Some z -> + z = (if Int.eq n Int.zero then x else + shrl (addl x (shrlu (shrl x (Vint (Int.repr 63))) + (Vint (Int.sub (Int.repr 64) n)))) + (Vint n)). +Proof. + intros. destruct x; simpl in H; try discriminate. + destruct (Int.ltu n (Int.repr 63)) eqn:LT; inv H. + exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63; intros LT'. + predSpec Int.eq Int.eq_spec n Int.zero. +- subst n. rewrite Int64.shrx'_zero. auto. +- simpl. change (Int.ltu (Int.repr 63) Int64.iwordsize') with true. simpl. + replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl. + replace (Int.ltu n Int64.iwordsize') with true. + f_equal; apply Int64.shrx'_shr_2; assumption. + symmetry; apply zlt_true. change (Int.unsigned n < 64); omega. + symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64. + assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } + rewrite Int.unsigned_repr. + change (Int.unsigned Int64.iwordsize') with 64; omega. + assert (64 < Int.max_unsigned) by reflexivity. omega. +Qed. + Theorem negate_cmp_bool: forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y). Proof. diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 4662f964..ccf2e6fd 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -53,6 +53,13 @@ Definition mk_shrximm (n: int) (k: code) : res code := Pcmov Cond_l RAX RCX :: Psarl_ri RAX n :: k). +Definition mk_shrxlimm (n: int) (k: code) : res code := + OK (if Int.eq n Int.zero then Pmov_rr RAX RAX :: k else + Pcqto :: + Pshrq_ri RDX (Int.sub (Int.repr 64) n) :: + Pleaq RAX (Addrmode (Some RAX) (Some(RDX, 1)) (inl _ 0)) :: + Psarq_ri RAX n :: k). + Definition low_ireg (r: ireg) : bool := match r with RAX | RBX | RCX | RDX => true | _ => false end. @@ -501,6 +508,10 @@ Definition transl_op | Oshrlimm n, a1 :: nil => assertion (mreg_eq a1 res); do r <- ireg_of res; OK (Psarq_ri r n :: k) + | Oshrxlimm n, a1 :: nil => + assertion (mreg_eq a1 AX); + assertion (mreg_eq res AX); + mk_shrxlimm n k | Oshrlu, a1 :: a2 :: nil => assertion (mreg_eq a1 res); assertion (mreg_eq a2 CX); diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index bf14f010..79602e52 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -132,6 +132,13 @@ Proof. Qed. Hint Resolve mk_shrximm_label: labels. +Remark mk_shrxlimm_label: + forall n k c, mk_shrxlimm n k = OK c -> tail_nolabel k c. +Proof. + intros. monadInv H. destruct (Int.eq n Int.zero); TailNoLabel. +Qed. +Hint Resolve mk_shrxlimm_label: labels. + Remark mk_intconv_label: forall f r1 r2 k c, mk_intconv f r1 r2 k = OK c -> (forall r r', nolabel (f r r')) -> diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index fa75e7e7..99d0680d 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -230,6 +230,45 @@ Proof. unfold compare_ints. Simplifs. Qed. +(** Smart constructor for [shrxl] *) + +Lemma mk_shrxlimm_correct: + forall n k c (rs1: regset) v m, + mk_shrxlimm n k = OK c -> + Val.shrxl (rs1#RAX) (Vint n) = Some v -> + exists rs2, + exec_straight ge fn c rs1 m k rs2 m + /\ rs2#RAX = v + /\ forall r, data_preg r = true -> r <> RAX -> r <> RDX -> rs2#r = rs1#r. +Proof. + unfold mk_shrxlimm; intros. exploit Val.shrxl_shrl_2; eauto. intros EQ. + destruct (Int.eq n Int.zero); inv H. +- econstructor; split. apply exec_straight_one. simpl; reflexivity. auto. + split. Simplifs. intros; Simplifs. +- set (v1 := Val.shrl (rs1 RAX) (Vint (Int.repr 63))) in *. + set (v2 := Val.shrlu v1 (Vint (Int.sub (Int.repr 64) n))) in *. + set (v3 := Val.addl (rs1 RAX) v2) in *. + set (v4 := Val.shrl v3 (Vint n)) in *. + set (rs2 := nextinstr_nf (rs1#RDX <- v1)). + set (rs3 := nextinstr_nf (rs2#RDX <- v2)). + set (rs4 := nextinstr (rs3#RAX <- v3)). + 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. + 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. } + exists rs5; split. + eapply exec_straight_trans with (rs2 := rs3). + eapply exec_straight_two with (rs2 := rs2); reflexivity. + eapply exec_straight_two with (rs2 := rs4). + simpl. rewrite X. reflexivity. reflexivity. reflexivity. reflexivity. + split. unfold rs5; Simplifs. + intros. unfold rs5; Simplifs. unfold rs4; Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs. +Qed. + (** Smart constructor for integer conversions *) Lemma mk_intconv_correct: @@ -1321,6 +1360,8 @@ Transparent destroyed_by_op. rewrite D. reflexivity. auto. auto. split. change (Vlong r = v). congruence. simpl; intros. destruct H2. unfold rs1; Simplifs. +(* shrxlimm *) + apply SAME. eapply mk_shrxlimm_correct; eauto. (* leal *) exploit transl_addressing_mode_64_correct; eauto. intros EA. generalize (normalize_addrmode_64_correct x rs). destruct (normalize_addrmode_64 x) as [am' [delta|]]; intros EV. diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index c35d3def..0bf143d2 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -311,6 +311,14 @@ Definition make_xorlimm (n: int64) (r: reg) := else if Int64.eq n Int64.mone then (Onotl, r :: nil) else (Oxorlimm n, r :: nil). +Definition make_divlimm n (r1 r2: reg) := + match Int64.is_power2' n with + | Some l => if Int.ltu l (Int.repr 63) + then (Oshrxlimm l, r1 :: nil) + else (Odivl, r1 :: r2 :: nil) + | None => (Odivl, r1 :: r2 :: nil) + end. + Definition make_divluimm n (r1 r2: reg) := match Int64.is_power2' n with | Some l => (Oshrluimm l, r1 :: nil) @@ -371,6 +379,7 @@ Nondetfunction op_strength_reduction | Osubl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_addlimm (Int64.neg n2) r1 | Omull, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_mullimm n1 r2 | Omull, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_mullimm n2 r1 + | Odivl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_divlimm n2 r1 r2 | Odivlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_divluimm n2 r1 r2 | Omodlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_modluimm n2 r1 r2 | Oandl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_andlimm n1 r2 v2 diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v index 4175d2f9..161b9579 100644 --- a/ia32/ConstpropOpproof.v +++ b/ia32/ConstpropOpproof.v @@ -578,6 +578,20 @@ Proof. econstructor; split; eauto. auto. Qed. +Lemma make_divlimm_correct: + forall n r1 r2 v, + Val.divls e#r1 e#r2 = Some v -> + e#r2 = Vlong n -> + let (op, args) := make_divlimm n r1 r2 in + exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w. +Proof. + intros; unfold make_divlimm. + destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?. + rewrite H0 in H. econstructor; split. simpl; eauto. eapply Val.divls_pow2; eauto. auto. + exists v; auto. + exists v; auto. +Qed. + Lemma make_divluimm_correct: forall n r1 r2 v, Val.divlu e#r1 e#r2 = Some v -> @@ -821,6 +835,9 @@ Proof. (* 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. +(* divl *) + assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto. + apply make_divlimm_correct; auto. (* divlu *) assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_divluimm_correct; auto. diff --git a/ia32/Machregs.v b/ia32/Machregs.v index 34d88328..a9383d18 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -137,6 +137,7 @@ Definition destroyed_by_op (op: operation): list mreg := | Odivlu => AX :: DX :: nil | Omodl => AX :: DX :: nil | Omodlu => AX :: DX :: nil + | Oshrxlimm _ => DX :: nil | Ocmp _ => AX :: CX :: nil | _ => nil end. @@ -217,6 +218,7 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg | Oshll => (None :: Some CX :: nil, None) | Oshrl => (None :: Some CX :: nil, None) | Oshrlu => (None :: Some CX :: nil, None) + | Oshrxlimm _ => (Some AX :: nil, Some AX) | _ => (nil, None) end. @@ -313,6 +315,7 @@ Definition two_address_op (op: operation) : bool := | Oshllimm _ => true | Oshrl => true | Oshrlimm _ => true + | Oshrxlimm _ => false | Oshrlu => true | Oshrluimm _ => true | Ororlimm _ => true diff --git a/ia32/NeedOp.v b/ia32/NeedOp.v index 9a75cba8..575532b1 100644 --- a/ia32/NeedOp.v +++ b/ia32/NeedOp.v @@ -110,6 +110,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshllimm _ => op1 (default nv) | Oshrl => op2 (default nv) | Oshrlimm _ => op1 (default nv) + | Oshrxlimm n => op1 (default nv) | Oshrlu => op2 (default nv) | Oshrluimm _ => op1 (default nv) | Ororlimm _ => op1 (default nv) diff --git a/ia32/Op.v b/ia32/Op.v index ed96c132..1d0e8472 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -135,6 +135,7 @@ Inductive operation : Type := | Oshllimm (n: int) (**r [rd = r1 << n] *) | Oshrl (**r [rd = r1 >> r2] (signed) *) | Oshrlimm (n: int) (**r [rd = r1 >> n] (signed) *) + | Oshrxlimm (n: int) (**r [rd = r1 / 2^n] (signed) *) | Oshrlu (**r [rd = r1 >> r2] (unsigned) *) | Oshrluimm (n: int) (**r [rd = r1 >> n] (unsigned) *) | Ororlimm (n: int) (**r rotate right immediate *) @@ -353,6 +354,7 @@ Definition eval_operation | Oshllimm n, v1::nil => Some (Val.shll v1 (Vint n)) | Oshrl, v1::v2::nil => Some (Val.shrl v1 v2) | Oshrlimm n, v1::nil => Some (Val.shrl v1 (Vint n)) + | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n) | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2) | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n)) | Ororlimm n, v1::nil => Some (Val.rorl v1 (Vint n)) @@ -521,6 +523,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshllimm _ => (Tlong :: nil, Tlong) | Oshrl => (Tlong :: Tint :: nil, Tlong) | Oshrlimm _ => (Tlong :: nil, Tlong) + | Oshrxlimm _ => (Tlong :: nil, Tlong) | Oshrlu => (Tlong :: Tint :: nil, Tlong) | Oshrluimm _ => (Tlong :: nil, Tlong) | Ororlimm _ => (Tlong :: nil, Tlong) @@ -680,6 +683,7 @@ Proof with (try exact I). destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... + destruct v0; inv H0. destruct (Int.ltu n (Int.repr 63)); inv H2... destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')... destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')... destruct v0... @@ -1225,6 +1229,7 @@ Proof. inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. + inv H4; simpl in H1; try discriminate. simpl. destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. inv H4; simpl; auto. diff --git a/ia32/PrintOp.ml b/ia32/PrintOp.ml index 42c8b3e5..b6147197 100644 --- a/ia32/PrintOp.ml +++ b/ia32/PrintOp.ml @@ -134,6 +134,7 @@ let print_operation reg pp = function | Oshllimm n, [r1] -> fprintf pp "%a < fprintf pp "%a >>ls %a" reg r1 reg r2 | Oshrlimm n, [r1] -> fprintf pp "%a >>ls %ld" reg r1 (camlint_of_coqint n) + | Oshrxlimm n, [r1] -> fprintf pp "%a >>lx %ld" reg r1 (camlint_of_coqint n) | Oshrlu, [r1;r2] -> fprintf pp "%a >>lu %a" reg r1 reg r2 | Oshrluimm n, [r1] -> fprintf pp "%a >>lu %ld" reg r1 (camlint_of_coqint n) | Ororlimm n, [r1] -> fprintf pp "%a rorl %ld" reg r1 (camlint_of_coqint n) diff --git a/ia32/SelectLong.vp b/ia32/SelectLong.vp index c28777e8..32fd9aca 100644 --- a/ia32/SelectLong.vp +++ b/ia32/SelectLong.vp @@ -286,45 +286,18 @@ Nondetfunction mull (e1: expr) (e2: expr) := | _, _ => Eop Omull (e1:::e2:::Enil) end. -Definition divl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.divl e1 e2 else - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.divs n1 n2) - | _, _ => Eop Odivl (e1:::e2:::Enil) - end. - -Definition modl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.modl e1 e2 else - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.mods n1 n2) - | _, _ => Eop Omodl (e1:::e2:::Enil) - end. - -Definition divlu (e1 e2: expr) := - if Archi.splitlong then SplitLong.divlu e1 e2 else - let default := Eop Odivlu (e1:::e2:::Enil) in - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.divu n1 n2) - | _, Some n2 => - match Int64.is_power2 n2 with - | Some l => shrluimm e1 (Int.repr (Int64.unsigned l)) - | None => default - end - | _, _ => default - end. - -Definition modlu (e1 e2: expr) := - if Archi.splitlong then SplitLong.modlu e1 e2 else - let default := Eop Omodlu (e1:::e2:::Enil) in - match is_longconst e1, is_longconst e2 with - | Some n1, Some n2 => longconst (Int64.modu n1 n2) - | _, Some n2 => - match Int64.is_power2 n2 with - | Some l => andl e1 (longconst (Int64.sub n2 Int64.one)) - | None => default - end - | _, _ => default - end. +Definition shrxlimm (e: expr) (n: int) := + if Archi.splitlong then SplitLong.shrxlimm e n else + if Int.eq n Int.zero then e else Eop (Oshrxlimm n) (e ::: Enil). + +Definition divlu_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.divlu_base e1 e2 else Eop Odivlu (e1:::e2:::Enil). +Definition modlu_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.modlu_base e1 e2 else Eop Omodu (e1:::e2:::Enil). +Definition divls_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.divls_base e1 e2 else Eop Odivl (e1:::e2:::Enil). +Definition modls_base (e1: expr) (e2: expr) := + if Archi.splitlong then SplitLong.modls_base e1 e2 else Eop Omodl (e1:::e2:::Enil). Definition cmplu (c: comparison) (e1 e2: expr) := if Archi.splitlong then SplitLong.cmplu c e1 e2 else diff --git a/ia32/SelectLongproof.v b/ia32/SelectLongproof.v index 634da83a..db3dd835 100644 --- a/ia32/SelectLongproof.v +++ b/ia32/SelectLongproof.v @@ -66,24 +66,24 @@ Proof. EvalOp. Qed. -Lemma is_longconst_sound: +Lemma is_longconst_sound_1: forall a n, is_longconst a = Some n -> a = Eop (Olongconst n) Enil. Proof with (try discriminate). unfold is_longconst; intros. destruct a... destruct o... destruct e0... congruence. Qed. -Lemma is_longconst_inv: +Lemma is_longconst_sound: forall v a n le, is_longconst a = Some n -> eval_expr ge sp e m le a v -> v = Vlong n. Proof. - intros. rewrite (is_longconst_sound _ _ H) in H0. InvEval. auto. + intros. rewrite (is_longconst_sound_1 _ _ H) in H0. InvEval. auto. Qed. Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword. Proof. unfold intoflong; destruct Archi.splitlong. apply SplitLongproof.eval_intoflong. red; intros. destruct (is_longconst a) as [n|] eqn:C. -- TrivialExists. simpl. erewrite (is_longconst_inv x) by eauto. auto. +- TrivialExists. simpl. erewrite (is_longconst_sound x) by eauto. auto. - TrivialExists. Qed. @@ -235,16 +235,30 @@ Admitted. Theorem eval_mull: binary_constructor_sound mull Val.mull. Admitted. -Theorem eval_divl: partial_binary_constructor_sound divl Val.divls. +Theorem eval_shrxlimm: + forall le a n x z, + eval_expr ge sp e m le a x -> + Val.shrxl x (Vint n) = Some z -> + 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. ++ 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. +- TrivialExists. +Qed. + +Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls. Admitted. -Theorem eval_modl: partial_binary_constructor_sound modl Val.modls. +Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls. Admitted. -Theorem eval_divlu: partial_binary_constructor_sound divlu Val.divlu. +Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu. Admitted. -Theorem eval_modlu: partial_binary_constructor_sound modlu Val.modlu. +Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu. Admitted. Theorem eval_cmplu: @@ -259,8 +273,8 @@ Proof. 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; - try (assert (x = Vlong n1) by (eapply is_longconst_inv; eauto)); - try (assert (y = Vlong n2) by (eapply is_longconst_inv; eauto)); + try (assert (x = Vlong n1) by (eapply is_longconst_sound; eauto)); + try (assert (y = Vlong n2) by (eapply is_longconst_sound; eauto)); subst. - simpl in C; inv C. EvalOp. destruct (Int64.cmpu c n1 n2); reflexivity. - EvalOp. simpl. rewrite Val.swap_cmplu_bool. rewrite C; auto. @@ -280,8 +294,8 @@ Proof. unfold Val.cmpl in H1. destruct (Val.cmpl_bool 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; - try (assert (x = Vlong n1) by (eapply is_longconst_inv; eauto)); - try (assert (y = Vlong n2) by (eapply is_longconst_inv; eauto)); + try (assert (x = Vlong n1) by (eapply is_longconst_sound; eauto)); + try (assert (y = Vlong n2) by (eapply is_longconst_sound; eauto)); subst. - simpl in C; inv C. EvalOp. destruct (Int64.cmp c n1 n2); reflexivity. - EvalOp. simpl. rewrite Val.swap_cmpl_bool. rewrite C; auto. diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v index ce33341e..c8b3278e 100644 --- a/ia32/ValueAOp.v +++ b/ia32/ValueAOp.v @@ -132,6 +132,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshllimm n, v1::nil => shll v1 (I n) | Oshrl, v1::v2::nil => shrl v1 v2 | Oshrlimm n, v1::nil => shrl v1 (I n) + | Oshrxlimm n, v1::nil => shrxl v1 (I n) | Oshrlu, v1::v2::nil => shrlu v1 v2 | Oshrluimm n, v1::nil => shrlu v1 (I n) | Ororlimm n, v1::nil => rorl v1 (I n) diff --git a/lib/Integers.v b/lib/Integers.v index 593f0ccc..6001caa5 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -4014,6 +4014,8 @@ Definition shru' (x: int) (y: Int.int): int := repr (Z.shiftr (unsigned x) (Int.unsigned y)). Definition shr' (x: int) (y: Int.int): int := repr (Z.shiftr (signed x) (Int.unsigned y)). +Definition shrx' (x: int) (y: Int.int): int := + divs x (shl' one y). Lemma bits_shl': forall x y i, @@ -4075,6 +4077,41 @@ Proof. intros. rewrite shl'_one_two_p. apply shl'_mul_two_p. Qed. +Theorem shrx'_zero: + forall x, shrx' x Int.zero = x. +Proof. + intros. unfold shrx'. rewrite shl'_one_two_p. unfold divs. + change (signed (repr (two_p (Int.unsigned Int.zero)))) with 1. + rewrite Z.quot_1_r. apply repr_signed. +Qed. + +Theorem shrx'_shr_2: + forall x y, + Int.ltu y (Int.repr 63) = true -> + shrx' x y = shr' (add x (shru' (shr' x (Int.repr 63)) (Int.sub (Int.repr 64) y))) y. +Proof. + intros. + set (z := repr (Int.unsigned y)). + apply Int.ltu_inv in H. change (Int.unsigned (Int.repr 63)) with 63 in H. + assert (N1: 63 < max_unsigned) by reflexivity. + assert (N2: 63 < Int.max_unsigned) by reflexivity. + assert (A: unsigned z = Int.unsigned y). + { unfold z; apply unsigned_repr; omega. } + assert (B: unsigned (sub (repr 64) z) = Int.unsigned (Int.sub (Int.repr 64) y)). + { unfold z. unfold sub, Int.sub. + change (unsigned (repr 64)) with 64. + change (Int.unsigned (Int.repr 64)) with 64. + rewrite (unsigned_repr (Int.unsigned y)) by omega. + rewrite unsigned_repr, Int.unsigned_repr by omega. + auto. } + unfold shrx', shr', shru', shl'. + rewrite <- A. + change (Int.unsigned (Int.repr 63)) with (unsigned (repr 63)). + rewrite <- B. + apply shrx_shr_2. + unfold ltu. apply zlt_true. change (unsigned z < 63). rewrite A; omega. +Qed. + (** Powers of two with exponents given as 32-bit ints *) Definition one_bits' (x: int) : list Int.int := -- cgit