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. --- ia32/Asmgenproof.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'ia32/Asmgenproof.v') 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')) -> -- cgit