From 3540b1f167d63e1a38ec0719f909dcda60c77ad3 Mon Sep 17 00:00:00 2001 From: Andrea Corallo Date: Thu, 17 Dec 2020 17:31:22 +0100 Subject: [PATCH] * Guarantee fwprop convergence and termination * lisp/emacs-lisp/comp.el (comp-emit-call-cstr): Have new-mvar as LHS *and* RHS when constraining in and to ensure monotonicity and fwprop convergence. (comp-fwprop): Raise a warning for debug reasons in case fwprop does not converge within 100 iterations. --- lisp/emacs-lisp/comp.el | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el index 6f1ef26ac78..5d2f8d412fe 100644 --- a/lisp/emacs-lisp/comp.el +++ b/lisp/emacs-lisp/comp.el @@ -1982,9 +1982,11 @@ TARGET-BB-SYM is the symbol name of the target block." (defun comp-emit-call-cstr (mvar call-cell cstr) "Emit a constraint CSTR for MVAR after CALL-CELL." - (let ((next-cell (cdr call-cell)) - (new-cell `((assume ,(make-comp-mvar :slot (comp-mvar-slot mvar)) - (and ,mvar ,cstr))))) + (let* ((next-cell (cdr call-cell)) + (new-mvar (make-comp-mvar :slot (comp-mvar-slot mvar))) + ;; Have new-mvar as LHS *and* RHS to ensure monotonicity and + ;; fwprop convergence!! + (new-cell `((assume ,new-mvar (and ,new-mvar ,mvar ,cstr))))) (setf (cdr call-cell) new-cell (cdr new-cell) next-cell (comp-func-ssa-status comp-func) 'dirty))) @@ -2568,9 +2570,14 @@ Return t if something was changed." (let ((comp-func f)) (comp-fwprop-prologue) (cl-loop - for i from 1 + for i from 1 to 100 while (comp-fwprop*) - finally (comp-log (format "Propagation run %d times\n" i) 2)) + finally + (when (= i 100) + (display-warning + 'comp + (format "fwprop pass jammed into %s?" (comp-func-name f)))) + (comp-log (format "Propagation run %d times\n" i) 2)) (comp-log-func comp-func 3)))) (comp-ctxt-funcs-h comp-ctxt))) -- 2.39.5