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. --- backend/Selectionproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/Selectionproof.v') 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. -- cgit