rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
39 stars 17 forks source link

[CN] Flycheck support #221

Open cpitclaudel opened 3 months ago

cpitclaudel commented 3 months ago

Hey folks,

Here a small bit of Elisp to get real-time error reports as you type:

image

Parsing CN's output is a bit painful because they have three different formats (JSON output mixed with text headers; plain text; and OCaml backtraces. The code could be a lot simpler if these three formats were unified.

;;; cn.el --- CN support for Flycheck -*- lexical-binding: t; -*-

;;; Commentary:
;;
;; Use `flycheck-select-checker' to use the CN checker.

;;; Code:

(require 'flycheck) ;; Install `flycheck' from NonGNU ELPA / MELPA

(defun cn--parse-errors (output checker buffer)
  "Parse errors from cn CHECKER's OUTPUT for BUFFER."
  ;; Step 1: Remove the function name headers
  (setq output (replace-regexp-in-string "^\\[.*?\\]:.*\\(\n\\|\\'\\)" "" output t t))
  (setq output (string-trim output))
  ;; Step 2: Parse error reports
  (or
   ;; Parse well-behaved JSON messages first
   (mapcar
    (lambda (line)
      (let-alist line
        (let ((loc (cadr .loc)))
          (flycheck-error-new-at
           (let-alist loc .region_start.line)
           (let-alist loc .region_start.char)
           'error
           .descr
           :id .short
           :checker checker
           :buffer buffer
           :filename (let-alist loc .region_start.file)
           :end-line (let-alist loc .region_end.line)
           :end-column (let-alist loc .region_end.char)
           :end-column .loc.Region.region_end.char))))
    (flycheck-parse-json output))
   ;; If none are found, parse plain-text errors.
   ;; This mostly covers syntax errors
   (delq nil
         (list
          (flycheck-parse-error-with-patterns
           output
           `((,(flycheck-rx-to-string
                '(and line-start (file-name) ":" line ":" column ": "
                      (message) line-end)
                'no-group)
              . error))
           checker)))
   ;; If non are found, just report the whole thing as one error.
   ;; This covers CN crashes.
   (unless (string-empty-p output)
     (list
      (flycheck-error-new-at 1 0 'error output
                             :checker checker
                             :buffer buffer
                             :filename (buffer-file-name buffer))))))

(flycheck-define-checker cn
  "Flycheck checker for CN."
  :command ("cn" "--json" source)
  :error-parser cn--parse-errors
  :error-filter (lambda (errors)
                  (flycheck-sanitize-errors
                   (flycheck-increment-error-columns errors)))
  :modes (c-mode))

;; Register the checker
(add-to-list 'flycheck-checkers 'cn)

(provide 'cn)
;;; cn.el ends here

I didn't see how to make --batch report errors (instead of pass/fail).

Btw, here is a crash that I ran into while trying this:

int f(int x) {
  return 1 / (x != 0 ? x : 0);
}

Output:

cn: internal error, uncaught exception:
    Failure("todo")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Dune__exe__Typing.pure in file "backend/cn/typing.ml", line 102, characters 22-25
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 78, characters 8-11
    Called from Dune__exe__Typing.pure in file "backend/cn/typing.ml", line 102, characters 22-25
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 78, characters 8-11
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 78, characters 8-11
    Called from Dune__exe__Typing.pure in file "backend/cn/typing.ml", line 102, characters 22-25
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 78, characters 8-11
    Called from Dune__exe__Typing.pure in file "backend/cn/typing.ml", line 102, characters 22-25
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 78, characters 8-11
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 78, characters 8-11
    Called from Dune__exe__Typing.bind in file "backend/cn/typing.ml", line 78, characters 8-11
    Called from Dune__exe__Typing.run in file "backend/cn/typing.ml", line 44, characters 16-19
    Called from Dune__exe__Main.main in file "backend/cn/main.ml", line 182, characters 20-87
    Called from Dune__exe__Main.main in file "backend/cn/main.ml", line 178, characters 9-1023
    Re-raised at Dune__exe__Main.main in file "backend/cn/main.ml", line 222, characters 8-73
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 34, characters 37-44

And another note: if you run make install_cn without installing Cerberus first, then the cn binary crashes with ERROR: couldn't find the Core standard library file when you try to start it.

septract commented 2 months ago

The crashing case mentioned here is caused by the use of /, see #231

dc-mak commented 1 month ago

Thanks and yes to build upon the above: stack traces should not happen, and we should fail more gracefully (e.g. with a nicer return code and say what's unsupported).

cn --json should have all the information for an error and if it doesn't compared to the CLI output, then this is a bug that should be reported with a small test case to trigger the behaviour.