Modify the cores pipeline to get cores info to Sterling (#312)

* fix: join parsing, regression test, note on 2nd issue

* add: semantics test

* add: tests, no-op change to parser for readability

* add: revisions to get core (strings, for the moment) to sterling

* fix: unsat but no core

* stop sending core in place of source

* Froglet Error Message Changes (#306)

* update: error messages

---------

Co-authored-by: shoujohnny <johnson_shou@brown.edu>

Author: tnelson

forge/froglet/lang/bsl-lang-specific-checks.rkt

@@ -140,22 +140,22 @@
 (define (check-node-expr-op-+ expr-node node-type child-types)
   (when (eq? (nodeinfo-lang (node-info expr-node)) LANG_ID)
     (define loc (nodeinfo-loc (node-info expr-node)))
-    (raise-bsl-relational-error "+" expr-node loc "You may have meant to use the `add` predicate instead.")))
+    (raise-bsl-relational-error "+" expr-node loc "The `+` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant addition, use the `add` predicate instead.")))
 
 (define (check-node-expr-op-- expr-node node-type child-types)
   (when (eq? (nodeinfo-lang (node-info expr-node)) LANG_ID)
     (define loc (nodeinfo-loc (node-info expr-node)))
-    (raise-bsl-relational-error "-" expr-node loc "You may have meant to use the `subtract` predicate instead.")))
+    (raise-bsl-relational-error "-" expr-node loc "The `-` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant subtraction, use the `subtract` predicate instead.")))
 
 (define (check-node-expr-op-& expr-node node-type child-types)
   (when (eq? (nodeinfo-lang (node-info expr-node)) LANG_ID)
     (define loc (nodeinfo-loc (node-info expr-node)))
-    (raise-bsl-relational-error "&" expr-node loc)))
+    (raise-bsl-relational-error "&" expr-node loc "The `&` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant logical-and, use `and` or `&&` instead.")))
 
 (define (check-node-expr-op--> expr-node node-type child-types)  
   (when (eq? (nodeinfo-lang (node-info expr-node)) LANG_ID)
     (define loc (nodeinfo-loc (node-info expr-node)))
-    (raise-bsl-error "Use of -> in expressions is not allowed in forge/bsl" expr-node loc)))
+    (raise-bsl-error "The `->` operator is only used for field declaration in Froglet." expr-node loc)))
 
 (define (check-node-expr-op-join expr-node node-type child-types)
   (when (eq? (nodeinfo-lang (node-info expr-node)) LANG_ID)
@@ -170,17 +170,17 @@
 (define (check-node-expr-op-^ expr-node node-type child-types)
   (when (eq? (nodeinfo-lang (node-info expr-node)) LANG_ID)
     (define loc (nodeinfo-loc (node-info expr-node)))
-    (raise-bsl-relational-error "^" expr-node loc)))
+    (raise-bsl-relational-error "^" expr-node loc "The `^` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant exclusive-or, use the `xor` operator instead.")))
 
 (define (check-node-expr-op-* expr-node node-type child-types)
   (when (eq? (nodeinfo-lang (node-info expr-node)) LANG_ID)
     (define loc (nodeinfo-loc (node-info expr-node)))
-    (raise-bsl-relational-error "*" expr-node loc)))
+    (raise-bsl-relational-error "*" expr-node loc "The `*` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant multiplication, use the `multiply` predicate instead.")))
 
 (define (check-node-expr-op-~ expr-node node-type child-types)
   (when (eq? (nodeinfo-lang (node-info expr-node)) LANG_ID)
     (define loc (nodeinfo-loc (node-info expr-node)))
-    (raise-bsl-relational-error "~~" expr-node loc)))
+    (raise-bsl-relational-error "~~" expr-node loc "The `~` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant logical-negation, use `not` or '!' instead.")))
 
 (define bsl-checker-hash (make-hash))
 (hash-set! bsl-checker-hash node/formula/multiplicity check-formula-mult)
@@ -259,38 +259,38 @@
 (define (check-args-node-expr-op--> expr-args info)
   (when (eq? (nodeinfo-lang info) LANG_ID)
     (define loc (nodeinfo-loc info))
-    (raise-bsl-error-deparsed-str "Direct use of -> in a formula is not allowed in Froglet" (format "(~a->~a)" (deparse (first expr-args)) (deparse (second expr-args))) loc)))
+    (raise-bsl-error-deparsed-str "The `->` operator is only used for field declaration in Froglet." (format "(~a->~a)" (deparse (first expr-args)) (deparse (second expr-args))) loc)))
 
 (define (check-args-node-expr-op-+ expr-args info)
   (when (eq? (nodeinfo-lang info) LANG_ID)
     (define loc (nodeinfo-loc info))
-    (raise-bsl-relational-error-expr-args "+" expr-args loc "You may have meant to use the `add` predicate instead.")))
+    (raise-bsl-relational-error-expr-args "+" expr-args loc "The `+` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant addition, use the `add` predicate instead.")))
 
 
 (define (check-args-node-expr-op-- expr-args info)
   (when (eq? (nodeinfo-lang info) LANG_ID)
     (define loc (nodeinfo-loc info))
-    (raise-bsl-relational-error-expr-args "-" expr-args loc "You may have meant to use the `subtract` predicate instead.")))
+    (raise-bsl-relational-error-expr-args "-" expr-args loc "The `-` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant subtraction, use the `subtract` predicate instead.")))
 
 (define (check-args-node-expr-op-& expr-args info)
   (when (eq? (nodeinfo-lang info) LANG_ID)
     (define loc (nodeinfo-loc info))
-    (raise-bsl-relational-error-expr-args "&" expr-args loc)))
+    (raise-bsl-relational-error-expr-args "&" expr-args loc "The `&` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant logical-and, use `and` or `&&` instead.")))
 
 (define (check-args-node-expr-op-^ expr-args info)
   (when (eq? (nodeinfo-lang info) LANG_ID)
     (define loc (nodeinfo-loc info))
-    (raise-bsl-relational-error-expr-args "^" expr-args loc)))
+    (raise-bsl-relational-error-expr-args "^" expr-args loc "The `^` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant exclusive-or, use the `xor` operator instead.")))
 
 (define (check-args-node-expr-op-* expr-args info)
   (when (eq? (nodeinfo-lang info) LANG_ID)
     (define loc (nodeinfo-loc info))
-    (raise-bsl-relational-error-expr-args "*" expr-args loc)))
+    (raise-bsl-relational-error-expr-args "*" expr-args loc "The `*` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant multiplication, use the `multiply` predicate instead.")))
 
 (define (check-args-node-expr-op-~ expr-args info)
   (when (eq? (nodeinfo-lang info) LANG_ID)
     (define loc (nodeinfo-loc info))
-    (raise-bsl-relational-error-expr-args "~" expr-args loc)))
+    (raise-bsl-relational-error-expr-args "~" expr-args loc "The `~` operator is not used in Froglet, but is reserved for use in other Forge languages. If you meant logical-negation, use `not` or '!' instead.")))
 
 ; Prevent the forge/core arity error from appearing, since it breaks closure
 (define (check-args-node-formula-op-= expr-args info)

forge/server/forgeserver.rkt

@@ -14,7 +14,7 @@
 ;   should be called for any context where a menu of commands doesn't fit (such as a
 ;   failing test, perhaps). 
 
-(require (only-in forge/lang/ast relation-name raise-forge-error)
+(require (only-in forge/lang/ast relation-name raise-forge-error deparse node?)
          forge/server/modelToXML
          forge/evaluator
          xml
@@ -130,7 +130,7 @@
                   [else
                    (printf "Sterling: unexpected 'next' request type: ~a~n" json-m)]))
           (define xml (get-xml inst))
-          (define response (make-sterling-data xml datum-id name temporal? (Sat? inst) old-datum-id))
+          (define response (make-sterling-data xml datum-id name temporal? inst old-datum-id))
           (send-to-sterling response #:connection connection)]
          [else
           (printf "Sterling: unexpected onClick: ~a~n" json-m)])     
@@ -143,7 +143,7 @@
        (define inst (get-current-instance)) 
        (define id curr-datum-id)
        (define xml (get-xml inst))
-       (define response (make-sterling-data xml id name temporal? (Sat? inst)))
+       (define response (make-sterling-data xml id name temporal? inst))
        (send-to-sterling response #:connection connection)     
        ]
       [(equal? (hash-ref json-m 'type) "eval")
@@ -199,7 +199,22 @@
   (unless (equal? 'off (get-option state-for-run 'run_sterling))
     (serve-sterling-static #:provider-port port)))
 
-(define (make-sterling-data xml id run-name temporal? not-done? [old-id #f])
+(define (make-status-value inst) 
+  (cond [(Sat? inst) "sat"]
+        [(Unsat? inst) "unsat"]
+        [(Unknown? inst) "unknown"]
+        [else "error"]))
+(define (make-core-value inst)
+  (if (and (Unsat? inst) (Unsat-core inst))
+      (map (lambda (cr) (cond [(node? cr) (deparse cr)]
+                              [(string? cr) cr]
+                              [else (raise-forge-error #:msg (format "Unexpected core value sending to Sterling: ~a" cr)
+                                                       #:context #f)]))
+           (Unsat-core inst))
+      #f))
+
+(define (make-sterling-data xml id run-name temporal? inst [old-id #f])
+  (define not-done? (Sat? inst))
   (jsexpr->string
    (hash
     'type "data"
@@ -210,6 +225,8 @@
                             'generatorName (->string run-name)
                             'format "alloy"
                             'data xml
+                            'status (make-status-value inst)
+                            'core (make-core-value inst)
                             'buttons (cond [(not not-done?) (list)]
                                            [temporal?
                                             (list (hash 'text "Next Trace"
@@ -407,7 +424,7 @@
          ; is-run-closed? is about whether this specific run has been terminated
          ; Sat? is about whether the solution we have is Sat.
          (define response (make-sterling-data xml datum-id name temporal?
-                                              (and (is-running? the-run) (not (is-run-closed? the-run)) (Sat? inst))
+                                              (and (is-running? the-run) (not (is-run-closed? the-run)) inst)
                                               old-datum-id))
         (send-to-sterling response #:connection connection)]
        [else

forge/server/modelToXML.rkt

@@ -110,12 +110,16 @@
     [(list? rs-opt) (apply string-append (map single-path-to-xml rs-opt))]
     [else ""]))
 
-(define (clean str)
-  (string-replace
-   (string-replace
-    (string-replace
+(define (clean ele)
+  (cond
+    [(string? ele) 
      (string-replace
-      (string-replace str "\"" "&quot;") ">" "&gt;") "<" "&lt;") "&" "&amp;") "\n" "&#xA;"))
+      (string-replace
+       (string-replace
+        (string-replace
+         (string-replace ele "\"" "&quot;") ">" "&gt;") "<" "&lt;") "&" "&amp;") "\n" "&#xA;")]
+    [(node? ele) (deparse ele)]
+    [else ele]))
 
 (define (agg-lines lines)
   (if (empty? lines)
@@ -221,11 +225,11 @@ here-string-delimiter
                         "<atom label=\"Unsatisfiable\"/>"
                         "</sig>\n"
                         "\n</instance>\n"
-                        (if data
-                            (string-append "<source filename=\"Unsat Core\" content=\""
-                                           (agg-lines
-                                            (map clean data))
-                                           "\"></source>\n") "")
+                        "<source filename=\"" filepath "\" content=\""
+                           (with-handlers ([exn:fail:filesystem:errno?
+                                            (λ (exn) (format "// Couldn't open source file (~a) (info: ~a). Is the file saved?" filepath (exn:fail:filesystem:errno-errno exn)))])
+                             (clean (agg-lines (port->lines (open-input-file filepath)))))
+                           "\"></source>\n"
                         "</alloy>")]
 
         ; ** Special display for "out of instances" vs. "unsat" **

forge/sigs-structs.rkt

@@ -38,7 +38,11 @@
   ) #:transparent)
 
 (struct/contract Unsat (               
-  [core (or/c #f (listof any/c))]; list-of-Formula-string-or-formulaID)]
+  ;[core (or/c #f (listof any/c))]; list-of-Formula-string-or-formulaID)]
+  ; If there's a core, there are two cases per component:
+  ;  (1) a node: a known formula
+  ;  (2) a string: an unknown formula (Kodkod couldn't map back this part of the core)
+  [core (or/c #f (listof (or/c node? string?)))]
   [stats any/c] ; association list
   [kind symbol?] ; symbol
   ) #:transparent)

forge/solver-specific/pardinus-cores.rkt

@@ -0,0 +1,91 @@
+#lang racket/base 
+
+(require forge/lang/ast)
+(require racket/string 
+         (only-in racket first empty? rest)
+         (except-in racket/contract ->)
+         (prefix-in @ (only-in racket/contract ->))
+         
+         (prefix-in @ (only-in racket +))
+         (only-in forge/shared get-verbosity VERBOSITY_HIGH))
+(provide pretty-print-core-formula process-core-formula pretty-format-core-formula)
+
+  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+  ; Note on cores: if core granularity is high, Kodkod may return a formula we do not have an ID for.
+  ; In these cases, the engine should be passing something like "f:0,0" which indexes _child_ formulas.
+  ; (In *very* rare cases, Kodkod may not be able to blame a subformula, and just give us a string.)
+  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+  (define (traverse-path-list path core-map [fmla #f])
+    ;; Cannot use for/fold or fold here, because we need to _not_ move down the list for
+    ;; a node/fmla/pred-spacer node (and any other node that is invisible to Pardinus).
+    (cond
+      ; Base case: no more indexes to process
+      [(empty? path) fmla]
+      ; We have an index, descend as appropriate
+      [else 
+       (define idx-str (first path))
+       (define idx (string->number idx-str))
+       (cond [(not fmla)
+              (traverse-path-list (rest path) 
+                                  core-map
+                                  (hash-ref core-map idx))]
+             [(node/formula/quantified? fmla)
+              ; Quantified: decls formulas first, then sub-formula last
+              (cond [(>= idx (length (node/formula/quantified-decls fmla)))
+                     (traverse-path-list (rest path)
+                                         core-map
+                                         (node/formula/quantified-formula fmla))]
+                    [else
+                     (define decl (list-ref (node/formula/quantified-decls fmla) idx))
+                     (traverse-path-list (rest path)
+                                         core-map
+                                         (car decl))])]
+             [(node/formula/op? fmla)
+              ; Operator formula: sub-formulas in order. Note that this layer isn't shown
+              ; to Pardinus, so we cannot move down the path index list for this.
+              (traverse-path-list (rest path) 
+                                  core-map
+                                  (list-ref (node/formula/op-children fmla) idx))]
+             [(node/fmla/pred-spacer? fmla)
+              ; Predicate spacer, just use internal formula, and don't move forward in the path
+              (traverse-path-list path
+                                  core-map
+                                  (node/fmla/pred-spacer-expanded fmla))]
+             [else
+              (raise-user-error (format "Unsupported formula type in core: ~a" fmla))])])) 
+
+(define (find-core-formula id core-map)
+  (unless (string-prefix? id "f:")
+    (raise-user-error (format "Unexpected error: invalid formula path ID: ~a" id)))
+  (define path (string-split (first (string-split id "f:")) ","))
+  (when (>= (get-verbosity) VERBOSITY_HIGH)
+    (printf "core path: ~a~n" path))
+  (unless (and (> (length path) 0) (member (string->number (first path)) (hash-keys core-map)))
+    (raise-user-error (format "Unexpected error: solver path ID prefix was invalid: ~a; valid prefixes: ~a" id (hash-keys core-map))))
+  (traverse-path-list path core-map #f))
+
+; A processed core formula will hopefully be a node, but it might also be a string
+; describing a formula that Kodkod couldn't map back. (This happens sometimes when using 
+; temporal operators, but it's rare.)  
+(define/contract (process-core-formula fmla-or-id core-map) 
+  (@-> (or/c node? string?) hash? (or/c string? node?))
+  ; (printf "***~n*** process-core-formula ~a ~a~n" fmla-or-id core-map)
+  ;(define fmla-num (if (string-prefix? id "f:") (string->number (substring id 2)) #f)]
+  (cond [(and (string? fmla-or-id) (string-prefix? fmla-or-id "f:")) 
+         (find-core-formula fmla-or-id core-map)]
+         ; Otherwise, it might be a node already, or else a string with a formula 
+         ; Kodkod couldn't find a blame path for. 
+        [else fmla-or-id]))
+
+(define (pretty-format-core-formula idx max fmla-or-id core-map)
+  (define fmla-or-string (process-core-formula fmla-or-id core-map))
+  (cond [(node? fmla-or-string)
+         (format "Core(part ~a/~a): [~a] ~a~n" (@+ idx 1) max
+                  (pretty-loc fmla-or-string) (deparse fmla-or-string))]
+        [else
+          (format "Core(part ~a/~a): [UNKNOWN] ~a~n" (@+ idx 1) max
+                  fmla-or-string)]))
+
+(define (pretty-print-core-formula idx max fmla-or-id core-map)
+  (fprintf (current-error-port) (pretty-format-core-formula idx max fmla-or-id core-map)))
+