Repair board atom vector calls
ober
9e19257b6d12a1e2697115d4cc534a9030dfb0d2
--- a/src/jcode/core/verified-run.ss +++ b/src/jcode/core/verified-run.ss @@ -1831,6 +1831,42 @@ path first last first 'piece-random candidate))))))))) +(def (board-atom-vector-repair detail cwd) + (and (string-contains detail "Exception in vector-ref:") + (string-contains detail "atom-rec") + (string-contains detail "is not a vector") + (let ((source (source-containing-symbol cwd "(clear-lines! board)"))) + (and source + (let* ((path (car source)) + (content (cadr source)) + (lines (string-split content #\newline)) + (first #f) + (last #f)) + (let loop ((rest lines) (line-no 1)) + (unless (null? rest) + (when (string-contains (car rest) + "(clear-lines! board)") + (unless first (set! first line-no)) + (set! last line-no)) + (loop (cdr rest) (+ line-no 1)))) + (and first last + (string-contains content "(atom-deref board)") + (let* ((span + (string-join + (take-up-to + (list-tail lines (- first 1)) + (+ (- last first) 1)) + "\n")) + (candidate + (replace-all + span + "(clear-lines! board)" + "(clear-lines! b)"))) + (and (not (string=? span candidate)) + (make-required-range-repair + path first last first + 'atom-board candidate))))))))) + (def (self-test-game-over-repair detail cwd) (and (string-contains detail "Exception in self-test: expected game over") @@ -1866,6 +1902,7 @@ (self-test-command-line-repair detail cwd) (self-test-game-over-repair detail cwd) (piece-type-random-index-repair detail cwd) + (board-atom-vector-repair detail cwd) (piece-shapes-index-repair detail cwd) (unexpected-close-repair detail cwd))) @@ -2245,6 +2282,14 @@ (best-repair-candidate-text cwd repair (required-repair-label repair)))))) +(def (board-atom-vector-diagnosis detail cwd) + (let ((repair (board-atom-vector-repair detail cwd))) + (and repair + (string-append + "\n\nBoard atom/vector diagnosis: the verifier printed a Jerboa atom record as the value passed to `vector-ref`. The board state cell itself was passed where a board vector was required. jcode constructed the local repair to pass the already dereferenced `b` binding to `clear-lines!` instead of the `board` atom. Apply it and verify immediately." + (best-repair-candidate-text + cwd repair (required-repair-label repair)))))) + (def (augment-verify-detail detail cwd) (let* ((diagnosis (or (invalid-context-diagnosis detail cwd) (empty-body-diagnosis detail cwd) @@ -2258,6 +2303,7 @@ (self-test-command-line-diagnosis detail cwd) (self-test-game-over-diagnosis detail cwd) (piece-type-random-index-diagnosis detail cwd) + (board-atom-vector-diagnosis detail cwd) (unexpected-close-diagnosis detail cwd))) (base (if diagnosis (string-append detail diagnosis) @@ -3343,7 +3389,7 @@ (member (repair-ref repair 'kind) '(syntax syntax-auto call-arity unbound-symbol runtime-arity qt-lifecycle command-line self-test-logic piece-index - piece-random))) + piece-random atom-board))) (def (automatic-required-repair-call) (let* ((repair (current-required-range-repair)) @@ -3353,7 +3399,7 @@ (member kind '(syntax-auto call-arity unbound-symbol runtime-arity qt-lifecycle command-line self-test-logic - piece-index piece-random delimiter)) + piece-index piece-random atom-board delimiter)) (list (make-wtool-call "replace_range" --- a/test/run.ss +++ b/test/run.ss @@ -3645,6 +3645,46 @@ (safe-delete-test-file! target-path)) (let* ([vr-dir "/tmp"] + [target "jcode-local-board-atom-vector-auto-repair.ss"] + [target-path (string-append vr-dir "/" target)] + [initial + (string-append + "(import (jerboa prelude))\n" + "(def board (atom (vector (make-vector 10 0))))\n" + "(def (clear-lines! b) (vector-ref b 0))\n" + "(def (lock-and-spawn!)\n" + " (let* ([b (atom-deref board)]\n" + " [n (clear-lines! board)])\n" + " n))\n")] + [responder + (scripted-responder + (list (list (make-wtool-call "verify" '() #f))))] + [verify-command + (string-append + "if grep -F -q '(clear-lines! board)' " target + "; then echo 'Exception in vector-ref: #[#{atom-rec demo} #(#(0 0 0)) #<mutex> () #f] is not a vector'; echo 'FAIL: self-test command failed'; exit 1; fi")]) + (safe-delete-test-file! target-path) + (call-with-output-file target-path + (lambda (p) (display initial p)) 'replace) + (let ([result + (verified-run responder "repair board atom vector call" + (list + (cons 'cwd vr-dir) + (cons 'verify-command verify-command) + (cons 'write-scope (parse-write-scope target)) + (cons 'local-model? #t) + (cons 'max-iterations 5) + (cons 'max-tool-errors 2)))]) + (check! "verified-run: automatic board atom vector repair verifies" + result "VERIFIED: exit 0\n")) + (check-pred! "verified-run: board atom vector repair passes deref binding" + (call-with-input-file target-path (lambda (p) (get-string-all p))) + (lambda (s) + (and (str-contains? s "(clear-lines! b)") + (not (str-contains? s "(clear-lines! board)"))))) + (safe-delete-test-file! target-path)) + + (let* ([vr-dir "/tmp"] [target "jcode-local-runtime-arity-repair.ss"] [target-path (string-append vr-dir "/" target)] [initial