[patch] Detection for cyclic references in pred, fun (#297)

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

@@ -292,6 +292,23 @@
     (define loc (nodeinfo-loc info))
     (raise-bsl-relational-error-expr-args "~" expr-args loc)))
 
+; Prevent the forge/core arity error from appearing, since it breaks closure
+(define (check-args-node-formula-op-= expr-args info)
+  (when (eq? (nodeinfo-lang info) LANG_ID)
+    (when (or (not (equal? (length expr-args) 2))
+              (not (equal? (node/expr-arity (first expr-args))
+                           (node/expr-arity (second expr-args)))))
+      (cond
+        [(> (node/expr-arity (first expr-args)) 1)
+         (raise-forge-error #:msg (format "Left-hand side of equality was not a singleton atom.")
+                            #:context info)]
+        [(> (node/expr-arity (second expr-args)) 1)
+         (raise-forge-error #:msg (format "Right-hand side of equality was not a singleton atom.")
+                            #:context info)]
+        [else
+         (raise-forge-error #:msg (format "Froglet could not equate these expressions.")
+                            #:context info)]))))
+
 ; TODO: add a global field-decl check outside bsl
 (define (bsl-field-decl-func true-breaker)
   (unless (or (equal? 'func (node/breaking/break-break true-breaker)) (equal? 'pfunc (node/breaking/break-break true-breaker))) 
@@ -302,6 +319,7 @@
 
 (define bsl-ast-checker-hash (make-hash))
 (hash-set! bsl-ast-checker-hash 'field-decl bsl-field-decl-func)
+(hash-set! bsl-ast-checker-hash node/formula/op/= check-args-node-formula-op-=)
 (hash-set! bsl-ast-checker-hash node/expr/op/-> check-args-node-expr-op-->)
 (hash-set! bsl-ast-checker-hash node/expr/op/+ check-args-node-expr-op-+)
 (hash-set! bsl-ast-checker-hash node/expr/op/- check-args-node-expr-op--)

forge/lang/expander.rkt

@@ -919,16 +919,20 @@
 (define-syntax (FunDecl stx)
   (syntax-parse stx
   ; TODO: output type declared is currently being lost
+
+  ; 0-ary function
   [((~datum FunDecl) (~optional (~seq prefix:QualNameClass "."))
                        name:NameClass
                        (~optional output-mult:HelperMultClass)
                        output-expr:ExprClass
                        body:ExprClass)
+
    (with-syntax ([body #'body])
      (syntax/loc stx (begin
        (~? (raise (format "Prefixes not allowed: ~a" 'prefix)))
        (const name.name body))))]
 
+  ; >0-ary function
   [((~datum FunDecl) (~optional (~seq prefix:QualNameClass "."))
                        name:NameClass
                        decls:ParaDeclsClass

forge/sigs.rkt

@@ -441,31 +441,54 @@
       #:attr mexpr #'(mexpr expr (if (> (node/expr-arity expr) 1) 'set 'one))))
   )
 
+; A list of helper names that have been expanded to reach the current context.
+; (This is roughly analogous to a call-stack in programming, although there is
+;  no actual stack.) Used to detect cyclic predicate references.
+;
+; The check is done in phase 0, when all macros are done expanding and AST 
+; construction is just a series of nested procedure calls, and `parameterize`
+; will keep the stack context for checking. That is, if referencing or altering
+; this parameter, make sure it is done in a normal function, not a macro.
+(define helpers-enclosing (make-parameter '()))
+
 ; Declare a new predicate
 ; Two cases: one with args, and one with no args
 (define-syntax (pred stx)
   (syntax-parse stx
-    ; no decls: predicate is already the AST node value, without calling it
+    ;;;;;;;;;;;;;;;;;
+    ; 0-args case: predicate is already the AST node value, without calling it
     [(pred pt:pred-type
            (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck]))
            name:id conds:expr ...+)
      (with-syntax ([decl-info #`(nodeinfo #,(build-source-location stx) check-lang #f)]
-                   [inner-unsyntax #'unsyntax])
+                   [inner-unsyntax #'unsyntax]
+                   [functionname (format-id #'name "~a/func" #'name)])
        (quasisyntax/loc stx
          (begin
+           ; Break the chain of macro expansions with a runtime procedure.
+           (define (functionname #:info [the-info #f])
+             ; Check: cyclic references?
+             (when (member 'name (helpers-enclosing))
+               (raise-forge-error #:msg (format "recursive predicate detected: ~a eventually called itself. The chain of calls involved: ~a.~n"
+                                                'name (helpers-enclosing))
+                                  #:context the-info))
+             (parameterize ([helpers-enclosing (cons 'name (helpers-enclosing))])
+               (pt.seal (node/fmla/pred-spacer the-info 'name '() (&&/info the-info conds ...)))))
+
            ; - Use a macro in order to capture the location of the _use_.
-           ; For 0-arg predicates, produce the AST node immediately
+           ; For 0-arg predicates, produce the AST node immediately.
            (define-syntax (name stx2)
              (syntax-parse stx2
                [name
                 (quasisyntax/loc stx2
-                  ; - "pred spacer" still present, even if no arguments, to consistently record use of a predicate
-                  (let* ([the-info (nodeinfo (inner-unsyntax (build-source-location stx2)) check-lang #f)]
-                        [ast-node (pt.seal (node/fmla/pred-spacer the-info 'name '() (&&/info the-info conds ...)))])
+                  (let ([ast-node (functionname #:info (nodeinfo (inner-unsyntax (build-source-location stx2)) check-lang #f))])
                     (update-state! (state-add-pred curr-state 'name ast-node))
-                    ast-node))])) )))]
+                    ast-node))]))
+
+           (update-state! (state-add-pred curr-state 'name functionname)))))]
 
-    ; some decls: predicate must be called to evaluate it
+    ;;;;;;;;;;;;;;;;;
+    ; >= 1-args case: predicate must be called to evaluate it
     [(pred pt:pred-type
            (~optional (#:lang check-lang) #:defaults ([check-lang #''checklangNoCheck]))
            (name:id decls:param-decl-class  ...+) conds:expr ...+)
@@ -476,9 +499,7 @@
            (quasisyntax/loc stx
              (begin
                ; - Use a macro in order to capture the location of the _use_.
-
                (define-syntax (name stx2)
-                 ;(printf "in macro: ~a~n" stx2)
                  (syntax-parse stx2
                    ; If it's the macro name and all the args, expand to an invocation of the procedure
                    [(name args (... ...))
@@ -491,20 +512,22 @@
                       (lambda (decls.name ...)
                         (functionname decls.name ...
                                       #:info (nodeinfo
-                                              (inner-unsyntax (build-source-location stx2)) check-lang #f))))]
-                   ))
+                                              (inner-unsyntax (build-source-location stx2)) check-lang #f))))]))
 
                ; - "pred spacer" added to record use of predicate along with original argument declarations etc.
                (define (functionname decls.name ... #:info [the-info #f])
                  (unless (or (integer? decls.name) (node/expr? decls.name) (node/int? decls.name))
                    (error (format "Argument '~a' to pred ~a was not a Forge expression, integer-expression, or Racket integer. Got ~v instead."
                                   'decls.name 'name decls.name)))
                  ...
-                 (pt.seal (node/fmla/pred-spacer the-info 'name (list (apply-record 'decls.name decls.mexpr decls.name) ...)
-                                                 (&&/info the-info conds ...))))
-
-
-
+                 ; Check: cyclic references?
+                 (when (member 'name (helpers-enclosing))
+                   (raise-forge-error #:msg (format "recursive predicate detected: ~a eventually called itself. The chain of calls involved: ~a.~n"
+                                                    'name (helpers-enclosing))
+                                      #:context the-info))
+                 (parameterize ([helpers-enclosing (cons 'name (helpers-enclosing))])
+                   (pt.seal (node/fmla/pred-spacer the-info 'name (list (apply-record 'decls.name decls.mexpr decls.name) ...)
+                                                   (&&/info the-info conds ...)))))
 
                (update-state! (state-add-pred curr-state 'name functionname)))))) 
        result-stx)]))
@@ -526,52 +549,62 @@
           (~optional (~seq #:codomain codomain:codomain-class)
                      #:defaults ([codomain.mexpr #'(mexpr (repeat-product univ (node/expr-arity result))
                                                           (if (> (node/expr-arity result) 1) 'set 'one))])))
-
      ; TODO: there is no check-lang in this macro; does that mean that language-level details are lost within a helper fun?
-
-     (with-syntax ([decl-info #`(nodeinfo #,(build-source-location stx) 'checklangNoCheck #f)]
-                   [functionname (format-id #'name "~a/func" #'name)]
-                   [inner-unsyntax #'unsyntax])
-       (quasisyntax/loc stx
-         (begin
-           ; - create a macro that captures the syntax location of the _use_
-           (define-syntax (name stx2)
-             (syntax-parse stx2
-               [(name args (... ...))
-                (quasisyntax/loc stx2
-                  (functionname args (... ...) #:info (nodeinfo
+     (define result-syntax
+       (with-syntax ([decl-info #`(nodeinfo #,(build-source-location stx) 'checklangNoCheck #f)]
+                     [functionname (format-id #'name "~a/func" #'name)]
+                     [inner-unsyntax #'unsyntax])
+         (quasisyntax/loc stx
+           (begin
+             ; - create a macro that captures the syntax location of the _use_
+             (define-syntax (name stx2)
+               (syntax-parse stx2
+                 [(name args (... ...))
+                  (quasisyntax/loc stx2
+                    (functionname args (... ...) #:info (nodeinfo
                                                        (inner-unsyntax (build-source-location stx2)) 'checklangNoCheck #f)))]
-               [name:id
-                (quasisyntax/loc stx2
-                  (lambda (decls.name ...)
-                    (functionname decls.name ... #:info (nodeinfo (inner-unsyntax (build-source-location stx2)) 'checklangNoCheck #f))))]))
-
-           ; - "fun spacer" added to record use of function along with original argument declarations etc.           
-           (define (functionname decls.name ... #:info [the-info #f])
-             (unless (or (integer? decls.name) (node/expr? decls.name) (node/int? decls.name))
-               (error (format "Argument '~a' to fun ~a was not a Forge expression, integer-expression, or Racket integer. Got ~v instead."
-                              'decls.name 'name decls.name)))
-             ...
-             ; maintain the invariant that helper functions are always rel-expression valued
-             (define safe-result
-               (cond [(node/int? result)
-                      (node/expr/op/sing (node-info result) 1 (list result))]
-                     [else result]))
-             (node/expr/fun-spacer
-              the-info                      ; from node
-              (node/expr-arity safe-result) ; from node/expr
-              'name
-              (list (apply-record 'decls.name decls.mexpr decls.name) ...)
-              codomain.mexpr
-              safe-result))
-           (update-state! (state-add-fun curr-state 'name name)))))]))
+                 [name:id
+                  (quasisyntax/loc stx2
+                    (lambda (decls.name ...)
+                      (functionname decls.name ... #:info (nodeinfo (inner-unsyntax (build-source-location stx2)) 'checklangNoCheck #f))))]))
+
+             (define (functionname decls.name ... #:info [the-info #f])
+               (unless (or (integer? decls.name) (node/expr? decls.name) (node/int? decls.name))
+                 (error (format "Argument '~a' to fun ~a was not a Forge expression, integer-expression, or Racket integer. Got ~v instead."
+                                'decls.name 'name decls.name)))
+               ...
+               (when (member 'name (helpers-enclosing))
+                 (raise-forge-error #:msg (format "recursive helper function detected: ~a eventually called itself. The chain of calls involved: ~a.~n"
+                                                  'name (helpers-enclosing))
+                                    #:context the-info))
+               (parameterize ([helpers-enclosing (cons 'name (helpers-enclosing))])
+                 ; avoid expanding result more than once
+                 (define result-once result)
+                 ; maintain the invariant that helper functions are always rel-expression valued
+                 (define safe-result
+                   (cond [(node/int? result-once)
+                          (node/expr/op/sing (node-info result-once) 1 (list result-once))]
+                         [else result-once]))
+                 ; - "fun spacer" added to record use of function along with original argument declarations etc.           
+                 (node/expr/fun-spacer
+                  the-info                      ; from node
+                  (node/expr-arity safe-result) ; from node/expr
+                  'name
+                  (list (apply-record 'decls.name decls.mexpr decls.name) ...)
+                  codomain.mexpr
+                  safe-result)))
+             (update-state! (state-add-fun curr-state 'name functionname))))))
+     result-syntax]))
 
 ; Declare a new constant
 ; (const name value)
 (define-syntax (const stx)
   (syntax-parse stx
-    [(const name:id value:expr) 
-      #'(begin 
+    [(const name:id value:expr)
+      #'(begin
+          ; TODO: this requires 0-ary helper functions to be defined in order.
+          ; Note that if this issue is fixed, suitable checks for cyclic reference
+          ; must be added (see the `pred` and `fun` macros).
           (define name value)
           (update-state! (state-add-const curr-state 'name name)))]))
 

forge/tests/forge/other/recursive-error.frg

@@ -0,0 +1,76 @@
+#lang forge/froglet 
+option verbose 0
+option run_sterling off
+
+/*
+  While syntactically, one can write recursive Forge predicates, this won't 
+  actually have the desired meaning. Alloy has an "unroll depth" for these,
+  but we would like to disable them entirely in this context.
+*/
+
+sig A {}
+
+-- arity 0, immediate cycle
+pred r { r }
+-- lasso with self-loop
+pred q { r }
+-- arity 0, delayed cycle 
+pred p1 { p2 }
+pred p2 { p1 }
+
+// 1-call cycles, test direct and within boolean expression
+pred r1[a: A] { r1[a] }
+pred r2[a: A] { some a: A | {some a and r2[a]} }
+
+// 2-call cycle
+pred r3x[a: A] { r3y[a] }
+pred r3y[a: A] { r3x[a] }
+
+// 3-call cycle
+pred r4x[a: A] { r4y[a] }
+pred r4y[a: A] { r4z[a] }
+pred r4z[a: A] { r4x[a] }
+
+// 1-arg pred invoking self-loop 0-arg pred
+pred r5[a: A] { r }
+
+// 2-arg pred invoking 1-arg pred in cycle 
+pred r6x[a1: A, a2: A] { r6y[a1] }
+pred r6y[a: A] { r6x[a, a] }
+
+
+// 0-arg function is harder to self-loop, 
+// because we get an identifier-ref-before-definition error
+// See the comments in `const` in sigs.rkt.
+//fun i: one A { i }
+//fun j1: one A { j2 }
+//fun j2: one A { j1 }
+
+
+// 1-arg function, self loop
+fun h[a: A]: one A { h[a] }
+// 1-arg functions, 2-call loop
+fun f[a: A]: one A { g[a] }
+fun g[a: A]: one A { f[a] }
+
+
+
+
+
+test expect {
+    recur_pred_0arg_self:       {r} is forge_error "r eventually called itself"
+    recur_pred_0arg_1lead_self: {q} is forge_error "r eventually called itself"
+    recur_pred0_2loop:          {p1} is forge_error "p1 eventually called itself"
+
+    recur_pred_1arg_self:      {some a: A | r1[a] } is forge_error "r1 eventually called itself"
+    recur_pred_1arg_self_bool: {some a: A | r2[a] } is forge_error "r2 eventually called itself"
+    recur_pred_1arg_2loop:     {some a: A | r3x[a] } is forge_error "r3x eventually called itself"
+    recur_pred_1arg_3loop:     {some a: A | r4x[a] } is forge_error "r4x eventually called itself"
+
+    recur_pred_1arg_0arg:       {some a: A | r5[a] } is forge_error "r eventually called itself"
+    recur_pred_1arg_2arg_2loop: {some a: A | r6y[a] } is forge_error "r6y eventually called itself"
+    recur_pred_2arg_1arg_2loop: {some a: A | r6x[a,a] } is forge_error "r6x eventually called itself"
+
+    recur_fun_2loop: {some a: A | f[a]} is forge_error "f eventually called itself"
+    recur_fun_self:  {some a: A | h[a]} is forge_error "h eventually called itself"
+}

forge/tests/froglet/froglet-errors.frg

@@ -1,4 +1,5 @@
 #lang forge/froglet 
+option verbose 0
 option run_sterling off
 
 /*
@@ -14,7 +15,10 @@ sig Person {
 }
 one sig Tim extends Person {}
 
-sig Node {next: lone Node}
+sig Node {
+  next: lone Node,
+  weights: pfunc Node -> Int
+}
 
 pred helper[n1,n2: Node] {
   n1 = n2
@@ -46,6 +50,9 @@ test expect {
   // Check that user-defined helper predicates (not just internally defined helpers) give this error, too
   //   helper_arity: {some n: Node | helper[n]} is forge_error "expected: 2"
 
+  // Check order of error production. weights[n2] desugars to n2.weights.
+  forgot_start_of_chain_left: {some n1,n2: Node | weights[n2] = 0} is forge_error "Left-hand side of equality was not a singleton atom"
+  forgot_start_of_chain_right: {some n1,n2: Node | 0 = weights[n2]} is forge_error "Right-hand side of equality was not a singleton atom"
 }