Infer type of atoms sent from evaluator (#249)

forge/evaluator.rkt

@@ -21,21 +21,21 @@
     (raise-user-error (format "Can't evaluate on unsat run. Expression: ~a" expression)))
   (define-values (expr-name interpretter)
     (cond [(node/expr? expression)
-           (checkExpression (Run-run-spec run) expression '() (get-checker-hash))
+           (checkExpression run expression '() (get-checker-hash))
            (define currents (Run-kodkod-currents run))
            (define expression-number (Kodkod-current-expression currents)) 
            (set-Kodkod-current-expression! currents (add1 expression-number))
            (values (pardinus:e expression-number)
                    interpret-expr)]
           [(node/formula? expression)
-           (checkFormula (Run-run-spec run) expression '() (get-checker-hash))
+           (checkFormula run expression '() (get-checker-hash))
            (define currents (Run-kodkod-currents run))
            (define formula-number (Kodkod-current-formula currents)) 
            (set-Kodkod-current-formula! currents (add1 formula-number))
            (values (pardinus:f formula-number)
                    interpret-formula)]
           [(node/int? expression)
-           ; ? No last-checker?
+           (checkInt run expression '() (get-checker-hash))
            (define currents (Run-kodkod-currents run))
            (define int-number (Kodkod-current-int currents)) 
            (set-Kodkod-current-int! currents (add1 int-number))

forge/last-checker.rkt

@@ -3,6 +3,7 @@
 (require 
   forge/sigs-structs
   forge/lang/ast
+  forge/lang/bounds
   forge/shared
   racket/syntax
   syntax/srcloc
@@ -13,7 +14,7 @@
   (except-in racket/set set)
   (only-in racket/contract define/contract or/c listof any))
 
-(provide checkFormula checkExpression primify)
+(provide checkFormula checkExpression checkInt primify infer-atom-type dfs-sigs deprimify)
 
 ; This function only exists for code-reuse - it's so that we don't
 ; need to use begin and hash-ref in every single branch of the match
@@ -290,6 +291,56 @@
                                 "_remainder")))
                          all-primitive-descendants)])])))
 
+
+; Infer a type for an atom node. 
+;   Best data source: the last Sterling instance of this run.
+;   Not ideal data source (e.g., sterling hasn't been run): the Kodkod bounds generated for this run,
+;     from which we can at least get the top-level sig to use.
+;   Fallback data source (e.g., run hasn't been generated): none, just use univ.
+(define (infer-atom-type run atom [in-instance #f])
+
+  (define (infer-from-instance)
+    (define tlsigs (if (Run? run) (get-top-level-sigs run) '()))
+    (define last-matched
+      (dfs-sigs run (lambda (s acc)
+                      (if (member (list (atom-name atom)) (hash-ref in-instance (Sig-name s)))
+                          (values s #f) ; try to find something more specific, don't stop
+                          (values acc #t))) ; nothing to find, since this atom isn't in the parent
+                (remove Int tlsigs)
+                #f))
+    (cond
+      ; If most-specific sig has no children, just use that sig name
+      [(and last-matched (empty? (get-children run last-matched)))
+       (list (list (Sig-name last-matched)))]
+      ; If most-specific sig has children, just the remainder
+      [last-matched
+       (list (list (string->symbol (string-append (symbol->string (Sig-name last-matched)) "_remainder"))))]
+      ; Otherwise, we can infer nothing
+      [else 
+        (map list (primify run 'univ))]))
+
+  ; Consider top-level sigs only
+  (define (infer-from-bounds)
+    (define kodkod-bounds (if (Run? run) (Run-kodkod-bounds run) '()))
+    (define tlsigs-with-atom-in-bounds
+      (filter-map (lambda (tlsig)
+                    (define b (findf (lambda (b) (equal? tlsig (bound-relation b))) kodkod-bounds))
+                    (if (and b (bound? b) (member (list (atom-name atom)) (bound-upper b)))
+                        tlsig
+                        #f))
+                  (get-top-level-sigs run)))
+    (if (empty? tlsigs-with-atom-in-bounds)
+        (map list (primify run 'univ)) ; no match, cannot infer anything
+        (map list (primify run (Sig-name (first tlsigs-with-atom-in-bounds)))))) ; we have a match
+
+  (cond [(and in-instance (hash? in-instance)) (infer-from-instance)]
+        [(Run? run) (infer-from-bounds)]
+        [else (map list (primify run 'univ))]))
+
+
+; Runs a DFS over the sigs tree, starting from sigs in <sigs>.
+; On each visited sig, <func> is called to obtain a new accumulated value
+; and whether the search should continue to that sig's children.
 (define (dfs-sigs run-or-state func sigs init-acc)
     (define (dfs-sigs-helper todo acc)
       (cond [(equal? (length todo) 0) acc]
@@ -370,9 +421,8 @@
     [(node/expr/atom info arity name)
      (check-and-output expr
                        node/expr/atom
-                       checker-hash
-                       ; overapproximate for now (TODO: get atom's sig)     
-                       (cons (map list (primify run-or-state 'univ))
+                       checker-hash   
+                       (cons (infer-atom-type run-or-state expr)
                              #t))]
 
     [(node/expr/fun-spacer info arity name args codomain expanded)
@@ -735,21 +785,18 @@
   (@-> (or/c Run? State? Run-spec?)
        node/int/constant?
        any)
-
-  (cond [(not (Run-spec? run-or-state))
-         (printf "Warning: integer literals not checked.~n")]
-        [else 
-         (define val (node/int/constant-value expr))
-         ; Note: get-scope will return number of int atoms, not the range we want. Hence, compute it ourselves.
-         (define max-int (sub1 (expt 2 (sub1 (get-bitwidth run-or-state)))))
-         (define min-int (@- (expt 2 (sub1 (get-bitwidth run-or-state)))))
-         (when (or (@> val max-int) (@> min-int val))
-           (raise-forge-error
-            #:msg (format "Integer literal (~a) could not be represented in the current bitwidth (~a through ~a)"
-                          val min-int max-int)
-            #:context expr))
-
-         (void)]))
+
+  (define run-spec (get-run-spec run-or-state))
+  (define val (node/int/constant-value expr))
+  ; Note: get-scope will return number of int atoms, not the range we want. Hence, compute it ourselves.
+  (define max-int (sub1 (expt 2 (sub1 (get-bitwidth run-spec)))))
+  (define min-int (@- (expt 2 (sub1 (get-bitwidth run-spec)))))
+  (when (or (@> val max-int) (@> min-int val))
+    (raise-forge-error
+     #:msg (format "Integer literal (~a) could not be represented in the current bitwidth (~a through ~a)"
+                   val min-int max-int)
+     #:context expr))
+  (void))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

forge/sigs-structs.rkt

@@ -358,6 +358,13 @@ Returns whether the given run resulted in sat or unsat, respectively.
         [(State? run-or-state)
          run-or-state]))
 
+; get-run-spec :: Run-or-State -> Run-spec
+(define (get-run-spec run-or-state)
+    (cond [(Run? run-or-state)
+         (Run-run-spec run-or-state)]
+        [(Run-spec? run-or-state)
+         run-or-state]))
+
 ; get-sig :: Run-or-State (|| Symbol Sig*) -> Sig
 ; Returns the Sig of a given name/ast-relation from a run/state.
 (define (get-sig run-or-state sig-name-or-rel)

forge/tests/forge-core/instances/atoms.rkt

@@ -1,4 +1,7 @@
 #lang forge/core
+(require (only-in rackunit check-true check-equal?))
+(require (only-in forge/last-checker infer-atom-type))
+(require (only-in racket/set list->set))
 
 (set-option! 'verbose 0)
 
@@ -17,7 +20,8 @@
     (! (in        (atom 'Node2) Node))
     (some Node))
 
-; Dangerous to use atom names without a concrete instance to force existence
+; Dangerous to use atom names without a concrete instance to force existence.
+; These symbols are what, at the moment, Forge will name atoms for the given scope.
 
 (test explicitAtomsSat3
       #:preds [AtomsIn]
@@ -39,3 +43,94 @@
       #:scope ([Node 4])
       #:expect sat)
 ; Potential bug: [Node 3 4] doesn't mean 3--4 anymore; it means 3
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Test that inference for an atom's most-specific sig is working
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(sig NodeA #:extends Node)
+(sig NodeB #:extends Node)
+(sig NodeC #:extends Node)
+(sig NodeAA #:extends NodeA)
+(sig NodeBA #:extends NodeA)
+(sig NodeCA #:extends NodeA)
+(sig Person)
+(sig Apple)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Test *from bounds*, no instance generated yet
+
+; Require atom to be only in top-level Node sig
+(run testingAtomSigInference_top
+      #:preds [(&& (in (atom 'Node0) Node)
+                   (! (in (atom 'Node0) (+ NodeA NodeB NodeC))))]
+      #:scope ([Node 3]))
+(check-true (forge:Run? testingAtomSigInference_top))
+(check-true (is-sat? testingAtomSigInference_top))
+(check-equal? (list->set (infer-atom-type testingAtomSigInference_top (atom 'Node0)))
+              ; infer-atom-type is based on kodkod-bounds, not the specific instance.
+              ; thus, we only know that the atom is a _Node_. We are not using the
+              ; added restrictions in the constraints (yet, anyway).
+              (list->set '((Node_remainder)
+                           (NodeA_remainder) 
+                           (NodeAA)
+                           (NodeBA)
+                           (NodeCA)
+                           (NodeB)
+                           (NodeC))))
+
+; Require atom to be only in mid-level NodeA sig.
+; This will be the same, since inference is only based on upper bounds, and only queries
+; top-level sigs anyway.
+(run testingAtomSigInference_middle
+      #:preds [(&& (in (atom 'Node0) NodeA)
+                   (! (in (atom 'Node0) (+ NodeAA NodeBA NodeAA))))]
+      #:scope ([Node 3]))
+(check-true (forge:Run? testingAtomSigInference_middle))
+(check-true (is-sat? testingAtomSigInference_middle))
+(check-equal? (list->set (infer-atom-type testingAtomSigInference_middle (atom 'Node0)))
+              ; See above for rationale; this is based on upper bounds not actual instance
+              (list->set '((Node_remainder)
+                           (NodeA_remainder)
+                           (NodeAA)
+                           (NodeBA)
+                           (NodeCA)
+                           (NodeB)
+                           (NodeC))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; Test *from instance* that's been generated
+
+; Here, the instance will only have Node0 in Node, not in any of its child sigs. 
+(run testingAtomSigInference_frominst_top
+      #:preds [(&& (in (atom 'Node0) Node)
+                   (! (in (atom 'Node0) (+ NodeA NodeB NodeC))))]
+      #:scope ([Node 3]))
+(check-true (forge:Run? testingAtomSigInference_frominst_top))
+(check-true (is-sat? testingAtomSigInference_frominst_top))
+
+(define top-gen (forge:make-model-generator (forge:get-result testingAtomSigInference_frominst_top) 'next))
+(define inst-top (top-gen))
+(define inst-top0 (first (Sat-instances inst-top)))
+(check-equal? (list->set (infer-atom-type testingAtomSigInference_frominst_top (atom 'Node0) inst-top0))
+              (list->set '((Node_remainder))))
+
+
+; Here, Node0 is found deeper in the tree. We know the atom is in NodeA, but not any of its children,
+; so we expect '(NodeA_remainder) as the only option.
+(run testingAtomSigInference_frominst_middle
+      #:preds [(&& (in (atom 'Node0) Node)
+                   (! (in (atom 'Node0) (+ NodeB NodeC)))
+                   (in (atom 'Node0) NodeA)
+                   (! (in (atom 'Node0) (+ NodeAA NodeBA NodeCA))))]
+      #:scope ([Node 3]))
+(check-true (forge:Run? testingAtomSigInference_frominst_middle))
+(check-true (is-sat? testingAtomSigInference_frominst_middle))
+
+(define middle-gen (forge:make-model-generator (forge:get-result testingAtomSigInference_frominst_middle) 'next))
+(define inst-middle (middle-gen))
+(define inst-middle0 (first (Sat-instances inst-middle)))
+(check-equal? (list->set (infer-atom-type testingAtomSigInference_frominst_middle (atom 'Node0) inst-middle0))
+              (list->set '((NodeA_remainder))))
+