Clozure / ccl

Clozure Common Lisp
http://ccl.clozure.com
Apache License 2.0
857 stars 103 forks source link

assert handling of places #367

Open informatimago opened 3 years ago

informatimago commented 3 years ago

In a similar way to https://github.com/Clozure/ccl/issues/366 there's also an improper handling of places in ASSERT:

(pprint (macroexpand-1 '(assert (equal (aref v (decf i 2)) (aref v (incf i))) ((aref v (decf i)) (aref v (incf i))))))

(ccl:without-compiling-code-coverage
  (tagbody
   #:g8228 (unless (equal (aref v (decf i 2)) (aref v (incf i)))
             (ccl::%assertion-failure t '(equal (aref v (decf i 2)) (aref v (incf i))) nil)
             (write-line "Type expressions to set places to, or nothing to leave them alone." *query-io*)
             (multiple-value-bind (#:g8229 #:g8230)
                 (ccl::assertion-value-prompt '(aref v (decf i)))
               (when #:g8230 (setf (aref v (decf i)) (values-list #:g8229))))
             (multiple-value-bind (#:g8231 #:g8232)
                 (ccl::assertion-value-prompt '(aref v (incf i)))
               (when #:g8232 (setf (aref v (incf i)) (values-list #:g8231))))
             (go #:g8228))))

The semantics of :

(assert (equal (aref v (decf i 2)) (aref v (incf i))) ((aref v (decf i)) (aref v (incf i))))

are clear.

Assuming i = i₀ as pre-condition, it's equivalent to:

(assert (equal (aref v i₀-2) (aref v i₀-1)) ((aref v i₀-2) (aref v i₀-1)))

as can be check with:

(let ((i 6)) (list (decf i 2) (incf i) (decf i) (incf i)))
--> (4 5 4 5)

And the postcondition is that i=i₀-1.

However, the macro-expansion of ASSERT above show that if the user doesn't give a new value for the first place (aref v i₀-2) designated by the first expresson (aref v (decf i)), then the wrong place will be modified by the second update code, the post condition won't be verified!

For example:

(let ((v (vector 0 0 0 1 2 3 4 5))
      (i 6))
  (assert (equal (aref v (decf i 2)) (aref v (incf i)))
          ((aref v (decf i)) (aref v (incf i))))
  (values i v))

After selecting the continue restart and entering:

RET
0 RET

we have:

        v = #(0 0 0 1 2 3 0 5)
        i = 5

and the assert is not fulfilled, but now it's tested on the wrong places!

After selecting the continue restart and entering:

1 RET
RET

we have:

        v = #(0 0 0 1 1 3 0 5)
        i = 3

and the assert is still not fulfilled,

And we can only exit with luck since we reach an area of the vector where the condition is verified, but not thanks to our input.

If there wasn't a range of equal values, we'd go with negative I and an out-of-bound error.

I would advise a global revision of the missing cases of get-setf-expansion for place processing...

informatimago commented 3 years ago

Err, my example, need to be revised to be conforming, since ASSERT specifies that the The order of evaluation of the places is not specified; But it remains that the place should be evaluated unconditionnally when the test is false.