Re: feature/native-comp bddd7a2 3/4: Do not emit assumptions referencing clobbered mvars (bug#46670)

[Pip Cet]

On Tue, Feb 23, 2021 at 11:25 PM Andrea Corallo <akrl@savannah.gnu.org> wrote:
> branch: feature/native-comp
> commit bddd7a2d1376d8ee7a318fc837aaaa98b9d9ce49
> Author: Andrea Corallo <akrl@sdf.org>
> Commit: Andrea Corallo <akrl@sdf.org>
>
>     Do not emit assumptions referencing clobbered mvars (bug#46670)
>
>         * lisp/emacs-lisp/comp.el (comp-func): Add `vframe-size' slot.
>         (comp-new-frame): Add `vsize' parameter.

I don't understand the reasoning behind assigning integer (negative)
slot numbers to temporary variables created by compile passes: that
means we can add temporary variables, but we can't really remove them
because then there'd be gaps in the vector.

>         (comp-limplify-top-level, comp-limplify-function): Update for new
>         `comp-new-frame'.
>         (comp-maybe-add-vmvar): New function.
>         (comp-add-cond-cstrs): Logic update to emit assumptions not
>         referencing clobbered variables.

I'd just like to state once more that this change is unnecessarily
complicated, introducing a temporary variable whose only "use" is to
express a constraint assumption (which is then propagated back to a
real variable, which we should have emitted the assumption about in
the first place).

There are several simple ways to fix this problem; they prevent us
from performing some optimizations, but that can be fixed
unobtrusively.

The real problem here is that the byte compiler emits destructive
stack ops of the form

push a
push b
eq

which lead to false dependencies when we translate that to

stack[i] = a
stack[i+1] = b
stack[i] = EQ(stack[i], stack[i+1])

It would be better to have the byte compiler emit

push eq
push a
push b
call 2

which would translate to

stack[i+1] = a
stack[i+2] = b
stack[i] = EQ (stack[i+1], stack[i+2])

That's a trivial change to the byte compiler, essentially telling it
not to use the 'byte-compile property of `eq' when byte-compiling for
the native compiler. (Unfortunately, that runs into another bug in
nativecomp, or it would be a one-liner :-) ).

> diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el
> index b6451d5..f18f8e3 100644
> --- a/lisp/emacs-lisp/comp.el
> +++ b/lisp/emacs-lisp/comp.el
> @@ -809,6 +809,7 @@ non local exit (ends with an `unreachable' insn)."))
>  Once in SSA form this *must* be set to 'dirty' every time the topology of the
>  CFG is mutated by a pass.")
>    (frame-size nil :type integer)
> +  (vframe-size 0 :type integer)
>    (blocks (make-hash-table :test #'eq) :type hash-table
>            :documentation "Basic block symbol -> basic block.")
>    (lap-block (make-hash-table :test #'equal) :type hash-table

You should document somewhere what all the Vs you just introduced
mean. IIUC, they're negative stack index values for temporary
variables created by compiler passes. (I agree, FWIW, that compiler
passes should at some point gain the ability to create temporary
variables, but to fix this specific bug it's unnecessary and a major
design change). However, there are better ways to do it than to keep
them in a hash table indexed by negative numbers: we could use a hash
table set instead.

Can vframe-size be negative?

> @@ -1468,11 +1469,11 @@ STACK-OFF is the index of the first slot frame 
> involved."
>        (setf (comp-mvar-typeset mvar) (list type)))
>      mvar))
>
> -(defun comp-new-frame (size &optional ssa)
> +(defun comp-new-frame (size vsize &optional ssa)
>    "Return a clean frame of meta variables of size SIZE.
>  If SSA non-nil populate it of m-var in ssa form."

The docstring needs updating.

> @@ -2322,6 +2323,18 @@ The assume is emitted at the beginning of the block 
> BB."
>        (_ (cl-assert nil)))
>      (setf (comp-func-ssa-status comp-func) 'dirty)))
>
> +(defun comp-maybe-add-vmvar (op cmp-res insns-seq)
> +  "If CMP-RES is clobbering OP emit a new constrained MVAR and return it.

MVAR shouldn't be capitalized. Why is there a "v" in the function name?

> +Return OP otherwise."
> +  (if-let ((match (eql (comp-mvar-slot op) (comp-mvar-slot cmp-res)))
> +           (new-mvar (make-comp-mvar
> +                      :slot
> +                      (- (cl-incf (comp-func-vframe-size comp-func))))))

Again, I struggle to see why we have slot numbers instead of simply
keeping a set of used mvars.

> +      (progn
> +        (push `(assume ,new-mvar ,op) (cdr insns-seq))
> +        new-mvar)
> +    op))

Am I missing something here? You're emitting an assume about a
variable without ever setting it? That seems wrong.

>  (defun comp-add-new-block-between (bb-symbol bb-a bb-b)>    "Create a new 
> basic-block named BB-SYMBOL and add it between BB-A and BB-B."
>    (cl-loop
> @@ -2427,6 +2440,7 @@ TARGET-BB-SYM is the symbol name of the target block."
>     do
>     (cl-loop
>      named in-the-basic-block
> +    with prev-insns-seq
>      for insns-seq on (comp-block-insns b)
>      do
>      (pcase insns-seq

It would be nice to use comp-loop-insn-in-block here. It should not be
hard to modify so it allows modification of the insn sequence, and
that would seem a generally useful feature to me.

> @@ -2452,10 +2466,14 @@ TARGET-BB-SYM is the symbol name of the target block."
>          (let ((block-target (comp-add-cond-cstrs-target-block b 
> branch-target)))
>            (setf (car branch-target-cell) (comp-block-name block-target))
>            (when (comp-mvar-used-p target-mvar1)
> -            (comp-emit-assume kind target-mvar1 op2 block-target negated))
> +            (comp-emit-assume kind target-mvar1
> +                              (comp-maybe-add-vmvar op2 cmp-res 
> prev-insns-seq)
> +                              block-target negated))
>            (when (comp-mvar-used-p target-mvar2)
>              (comp-emit-assume (comp-reverse-cmp-fun kind)
> -                              target-mvar2 op1 block-target negated)))
> +                              target-mvar2
> +                              (comp-maybe-add-vmvar op1 cmp-res 
> prev-insns-seq)
> +                              block-target negated)))
>          finally (cl-return-from in-the-basic-block)))
>        (`((set ,(and (pred comp-mvar-p) cmp-res)
>                (,(pred comp-call-op-p)
>
>  (defsubst comp-insert-insn (insn insn-cell)
>    "Insert INSN as second insn of INSN-CELL."

> @@ -3094,6 +3120,8 @@ Fold the call in case."
>            (comp-fwprop-call insn lval f args)))
>         (_
>          (comp-mvar-propagate lval rval))))
> +    (`(assume ,lval ,(and (pred comp-mvar-p) rval))
> +     (comp-mvar-propagate lval rval))

I believe we often emit assumptions of the form (assume ,lval (and
,rval _)), and it would be nice to handle those analogously. IOW,
there should be no difference between

(assume mvar1 mvar2)

and

(assume mvar1 (and mvar2))

and

(assume mvar1 (and mvar1 mvar2))