diff --git a/forge/evaluator.rkt b/forge/evaluator.rkt index 78ae13e0..2089d351 100644 --- a/forge/evaluator.rkt +++ b/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)) diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt index 63c62c9f..3f3fb324 100644 --- a/forge/last-checker.rkt +++ b/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 . +; On each visited sig, 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)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt index cc2fc948..9f8dd882 100644 --- a/forge/sigs-structs.rkt +++ b/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) diff --git a/forge/tests/forge-core/instances/atoms.rkt b/forge/tests/forge-core/instances/atoms.rkt index e08a1b15..abc66393 100644 --- a/forge/tests/forge-core/instances/atoms.rkt +++ b/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)))) +