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.

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 <<l %ld" reg r1 (camlint_of_coqint n)
   | Oshrl, [r1;r2] -> 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 :=