From 1ef9d158d0736b798fd1dc3ebc07faf6828a0bd1 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Tue, 28 Jan 2025 09:21:24 -0500 Subject: [PATCH 1/5] forge/domains/abac updates, fix import namespace clash, misc improvements (#291) * Refactor ABAC language to use a .frg domain model that can be extended into an assignment none inferred multiplicity is no longer set * Somewhat improved Froglet errors in narrow cases, re-enabled corresponding test cases * Fix issue recently introduced where using a Forge internal ID as a sig, field, etc. name would cause an error, but only if the file making the definition was imported into another. * Minor fixes (e.g., License registration for Racket package server) --- forge/breaks.rkt | 14 ++- forge/domains/abac/abac.frg | 90 ++++++++++++++ forge/domains/abac/helpers.rkt | 29 +++-- forge/domains/abac/lexparse.rkt | 2 +- forge/domains/abac/pretty-formatting.rkt | 7 +- forge/domains/abac/runner.rkt | 111 +++++++----------- forge/domains/abac/tests/abac2.rkt | 27 +++-- forge/domains/abac/tests/emcstests.rkt | 8 +- .../froglet/lang/bsl-lang-specific-checks.rkt | 29 +++-- forge/info.rkt | 4 +- forge/lang/ast.rkt | 2 +- forge/lang/expander.rkt | 24 +++- forge/lang/reader.rkt | 7 +- forge/last-checker.rkt | 105 +++-------------- forge/server/forgeserver.rkt | 23 +--- forge/sigs-structs.rkt | 89 +++++++++++++- forge/sigs.rkt | 5 + forge/tests/error/abstract.frg | 2 +- forge/tests/error/bsl-join-right.frg | 2 +- forge/tests/error/bsl-join-right2.frg | 2 +- forge/tests/error/bsl-join-right3.frg | 2 +- forge/tests/error/bsl-join-right4.frg | 2 +- forge/tests/error/bsl-join-right5.frg | 2 +- forge/tests/error/bsl-join-right6.frg | 2 +- forge/tests/error/bsl-join.frg | 2 +- forge/tests/error/bsl-join2.frg | 1 + forge/tests/error/bsl-join3.frg | 2 +- forge/tests/error/bsl-reachable.frg | 2 +- forge/tests/error/bsl-set-singleton-equal.frg | 2 +- forge/tests/error/bsl-set.frg | 2 +- forge/tests/error/froglet-compareop0.frg | 15 --- forge/tests/error/froglet-compareop1.frg | 15 --- forge/tests/error/froglet-compareop2.frg | 15 --- forge/tests/error/froglet-compareop3.frg | 15 --- forge/tests/error/froglet-field-shadow.frg | 7 +- forge/tests/error/froglet-is-linear0.frg | 6 +- forge/tests/error/froglet-is-linear1.frg | 2 + forge/tests/error/froglet-join-right3.frg | 1 + forge/tests/error/froglet-join-right4.frg | 1 + forge/tests/error/froglet-join-right5.frg | 1 + forge/tests/error/froglet-join-right6.frg | 1 + forge/tests/error/froglet-join.frg | 1 + forge/tests/error/froglet-join2.frg | 1 + forge/tests/error/froglet-join3.frg | 1 + forge/tests/error/froglet-no-field.frg | 13 -- forge/tests/error/froglet-pred.frg | 2 + forge/tests/error/froglet-pubkey2.frg | 21 ---- ...reachable2.frg => froglet-reachable-2.frg} | 3 +- forge/tests/error/froglet-reachable-3.frg | 17 +++ ...reachable4.frg => froglet-reachable-4.frg} | 4 +- forge/tests/error/froglet-reachable5.frg | 3 +- forge/tests/error/froglet-reachable6.frg | 2 +- forge/tests/error/froglet-uni-0.frg | 16 --- forge/tests/error/froglet-uni-1.frg | 15 --- forge/tests/error/froglet-uni-2.frg | 15 --- forge/tests/error/froglet-uni-3.frg | 15 --- forge/tests/error/froglet-uni-4.frg | 15 --- forge/tests/error/froglet-uni-5.frg | 15 --- forge/tests/error/main.rkt | 107 +++++++---------- .../tests/error/mismatched-arg-type-arity.frg | 1 + .../error/mismatched-arg-type-basic-univ.frg | 1 + .../tests/error/mismatched-arg-type-basic.frg | 1 + .../error/mismatched-arg-type-fun-arity.frg | 1 + .../mismatched-arg-type-fun-codomain-int.frg | 1 + ...ched-arg-type-fun-codomain-non-primsig.frg | 1 + .../mismatched-arg-type-fun-codomain.frg | 1 + .../mismatched-arg-type-fun-output-int.frg | 1 + ...atched-arg-type-fun-output-non-primsig.frg | 1 + .../error/mismatched-arg-type-fun-output.frg | 1 + .../mismatched-arg-type-fun-univ-output.frg | 1 + forge/tests/error/mismatched-arg-type-fun.frg | 1 + forge/tests/error/mismatched-arg-type-int.frg | 1 + .../error/mismatched-arg-type-no-quant.frg | 1 + .../error/mismatched-arg-type-no-quant2.frg | 1 + .../error/mismatched-arg-type-non-primsig.frg | 1 + .../mismatched-arg-type-non-primsig2.frg | 1 + forge/tests/error/priming-basic.frg | 2 +- forge/tests/error/tree-type-error.frg | 1 + forge/tests/error/unstated_bounds.frg | 1 + forge/tests/froglet/froglet-errors.frg | 52 ++++++++ forge/tests/froglet/froglet-in-checks.frg | 72 ++++++++++++ .../froglet/import_internal_identifiers.frg | 10 ++ forge/tests/froglet/internal_identifiers.frg | 11 ++ 83 files changed, 609 insertions(+), 503 deletions(-) create mode 100644 forge/domains/abac/abac.frg delete mode 100644 forge/tests/error/froglet-compareop0.frg delete mode 100644 forge/tests/error/froglet-compareop1.frg delete mode 100644 forge/tests/error/froglet-compareop2.frg delete mode 100644 forge/tests/error/froglet-compareop3.frg delete mode 100644 forge/tests/error/froglet-no-field.frg delete mode 100644 forge/tests/error/froglet-pubkey2.frg rename forge/tests/error/{froglet-reachable2.frg => froglet-reachable-2.frg} (78%) create mode 100644 forge/tests/error/froglet-reachable-3.frg rename forge/tests/error/{froglet-reachable4.frg => froglet-reachable-4.frg} (80%) delete mode 100644 forge/tests/error/froglet-uni-0.frg delete mode 100644 forge/tests/error/froglet-uni-1.frg delete mode 100644 forge/tests/error/froglet-uni-2.frg delete mode 100644 forge/tests/error/froglet-uni-3.frg delete mode 100644 forge/tests/error/froglet-uni-4.frg delete mode 100644 forge/tests/error/froglet-uni-5.frg create mode 100644 forge/tests/froglet/froglet-errors.frg create mode 100644 forge/tests/froglet/froglet-in-checks.frg create mode 100644 forge/tests/froglet/import_internal_identifiers.frg create mode 100644 forge/tests/froglet/internal_identifiers.frg diff --git a/forge/breaks.rkt b/forge/breaks.rkt index 9a666ec86..75378f6a3 100644 --- a/forge/breaks.rkt +++ b/forge/breaks.rkt @@ -9,7 +9,8 @@ set-subtract! set-map list->mutable-set set-remove! append* set-member? set-empty? set-union! drop-right take-right for/set for*/set filter-not second set-add match identity) - racket/contract) + racket/contract + racket/hash) (require (only-in forge/shared get-verbosity VERBOSITY_HIGH)) (provide constrain-bounds (rename-out [break-rel break]) break-bound break-formulas) @@ -204,7 +205,7 @@ (define break-key (cond [(symbol? break) break] [(@node/breaking/break? break) (@node/breaking/break-break break)] - [else (raise-user-error (format "Not a valid break name: ~a~n" break))])) + [else (@raise-forge-error #:msg (format "Not a valid break name: ~a~n" break) #:context #f)])) (unless (hash-has-key? strategies break-key) (error (format "break not implemented among ~a" strategies) break-key)) (hash-add! rel-breaks rel break) @@ -254,7 +255,7 @@ (for ([bound total-bounds]) ; get declared breaks for the relation associated with this bound - (define rel (bound-relation bound)) + (define rel (bound-relation bound)) (define breaks (hash-ref rel-breaks rel (set))) (define break-pris (hash-ref rel-break-pri rel (make-hash))) ; compose breaks @@ -264,6 +265,9 @@ (cond [(set-empty? breaks) (unless defined (cons! new-total-bounds bound)) ][else + (unless (hash-has-key? relations-store rel) + (@raise-forge-error #:msg (format "Attempted to set or modify bounds of ~a, but the annotation given was of the wrong form (sig vs. field).~n" rel) + #:context #f)) (define rel-list (hash-ref relations-store rel)) (define atom-lists (map (λ (b) (hash-ref bounds-store b)) rel-list)) @@ -272,8 +276,8 @@ (define break-sym (cond [(symbol? break) break] [(@node/breaking/break? break) (@node/breaking/break-break break)] - [else (raise-user-error (format "constrain-bounds: not a valid break name: ~a~n" - break))])) + [else (@raise-forge-error #:msg (format "constrain-bounds: not a valid break name: ~a~n" break) + #:context #f)])) (define loc (if (@node? break) (@nodeinfo-loc (@node-info break)) #f)) diff --git a/forge/domains/abac/abac.frg b/forge/domains/abac/abac.frg new file mode 100644 index 000000000..67f2db997 --- /dev/null +++ b/forge/domains/abac/abac.frg @@ -0,0 +1,90 @@ +#lang forge/froglet + +/* + Domain model for attribute-based access control, specialized to the setting of the + Logic for systems ABAC homework. This file is imported by the runner for the + #lang forge/domains/abac DSL. +*/ + +/////////////////////// +// Datatype definitions +/////////////////////// + +// We'll model booleans as presence/non-presence of an entry in a partial function. +one sig True {} +// Notice that there's no "one sig False {}". One reason is that it's not necessary. +// But a better reason is that if we have False we'd need _total_, not partial, functions, +// which would make writing concrete examples more verbose. + +// Components of requests (S, A, R) +sig Subject, Action, Resource {} + +// Subjects: the entity requesting access +sig Customer extends Subject {} +sig Employee extends Subject { + // Notice we don't say "one Boolean" here. + // We *could*, but in *this* specific example it might make testing more elaborate. + training: lone True +} +sig Accountant, Admin extends Employee {} + +// Actions: the nature of the access +sig Read, Write extends Action {} + +// Resources: the target of the requested access +sig File extends Resource { + // Every File is owned by some entity. Note that we don't allow shared ownership. + owner: one Subject, + // Every file is under audit or not. Again, notice that we don't say "one Boolean". + audit: lone True +} + +// This model works with a single request at a time +one sig Request { + // Every request has a single subject, action, and resource. + reqS: one Subject, + reqA: one Action, + reqR: one Resource +} + +/////////////////////// +// Policy predicates +/////////////////////// + +// These are currently all done in the parser/expander for #lang forge/domains/abac +// But let's try to approximate them in Froglet! Here are two very basic policies: + +/* +policy original + permit if: s is admin, a is read, r is file. +end; + +policy modified + permit if: s is admin, a is read, r is file. + deny if: s is accountant, a is write. + permit if: s is accountant, a is read, r is under-audit. +end; +*/ + +pred original_permits_request { + // TASK: write a constraint that evaluates to true exactly when the 'original' + // policy would permit the request. + + // FILL +} + +pred modified_permits_request { + // TASK: write a constraint that evaluates to true exactly when the 'modified' + // policy would permit the request. + + // FILL +} + +// This won't run when the file is imported by the abac language. It will only +// run (and load the visualizer) if the Forge file is run directly. +difference_original_modified: run { + // TASK: write a constraint that evaluates to true exactly when the two policies + // disagree on permitting some request. + + // FILL +} diff --git a/forge/domains/abac/helpers.rkt b/forge/domains/abac/helpers.rkt index a36be93c3..b7be4f555 100644 --- a/forge/domains/abac/helpers.rkt +++ b/forge/domains/abac/helpers.rkt @@ -2,7 +2,18 @@ (require (only-in racket remove-duplicates flatten last)) (require forge/domains/abac/lexparse) -(provide (all-defined-out)) + +; Import the domain model. This contains sig and field definitions. +(require "abac.frg") + +(provide build-rule-matches + build-condition + apply-quantifiers + condition->atomic-fmla + rel->unary + list->product + (struct-out atomic-fmla) + (all-from-out "abac.frg")) ; Build a formula that is true IFF this rule matches (define (build-rule-matches r request-vars relations var->maybe-skolem) @@ -12,7 +23,7 @@ (append (extract-atomic-formulas-rule r)))))) (define to-quantify (filter (lambda (v) (equal? #f (member v request-vars))) vars-used)) ;(printf "to quantify: ~a~n" to-quantify) - (define basef (&& (map (lambda (rc) (build-condition rc relations var->maybe-skolem)) (rule-conditions r)))) + (define basef (&& (map (lambda (rc) (build-condition relations var->maybe-skolem rc)) (rule-conditions r)))) (apply-quantifiers to-quantify basef)) ; Datatype to represent an atomic formula @@ -29,12 +40,15 @@ (policy-rules pol)))) ; Build a formula (Forge AST) for a specific rule condition given by the parser -(define (build-condition c relations var->maybe-skolem) +(define (build-condition relations var->maybe-skolem c) + (define args (condition-args c)) (cond [(condition-sign c) - (in (list->product (map var->maybe-skolem (condition-args c))) + ; Build positive Forge literal formula + (in (list->product (map var->maybe-skolem args)) (rel->unary (hash-ref relations (string-titlecase (symbol->string (condition-pred c))))))] [else - (! (build-condition (condition #t (condition-pred c) (condition-args c)) relations var->maybe-skolem))])) + ; Build negative Forge literal formula + (! (build-condition relations var->maybe-skolem (condition #t (condition-pred c) args)))])) (define (apply-quantifiers todo f) (if (empty? todo) @@ -46,15 +60,12 @@ (define (list->product l) (foldl (lambda (i acc) (-> acc i)) (first l) (rest l))) -; Mechanism for building subsets of a sig (which might overlap) in forge/core -(sig True #:one) - ; Replace a 2+-ary relation that has a "fake" column on True with (join R True) (define (rel->unary r) (define types ((relation-typelist-thunk r))) (cond [(and (node/expr/relation? r) (> (node/expr-arity r) 1) (equal? "True" (last types))) - (join r True)] + (join r True)] [else r])) \ No newline at end of file diff --git a/forge/domains/abac/lexparse.rkt b/forge/domains/abac/lexparse.rkt index 003f5ef9e..5885c041b 100644 --- a/forge/domains/abac/lexparse.rkt +++ b/forge/domains/abac/lexparse.rkt @@ -157,7 +157,7 @@ (define allowed-relations-lc '("admin" "accountant" "customer" "read" "write" "file" "under-audit" - "owner-of" "in-training")) + "owned-by" "in-training")) (define (command-parser source-name) diff --git a/forge/domains/abac/pretty-formatting.rkt b/forge/domains/abac/pretty-formatting.rkt index 391714c62..341e5291e 100644 --- a/forge/domains/abac/pretty-formatting.rkt +++ b/forge/domains/abac/pretty-formatting.rkt @@ -49,7 +49,12 @@ (when msg (printf "~a~n" msg)) ] - [else (printf "-----------------------------------~nNo scenario existed matching those conditions.~n")])) + [else + (define sol (tree:get-value (forge:Run-result run))) + + (when (and (Unsat? sol) (Unsat-core sol)) + (printf "The solver had core-extraction enabled; printing core information.~n~a~n" sol (Unsat-core sol))) + (printf "-----------------------------------~nNo scenario existed matching those conditions.~n")])) (define (pretty-format-condition c) (define signis (cond [(condition-sign c) "is"] diff --git a/forge/domains/abac/runner.rkt b/forge/domains/abac/runner.rkt index c5c186ba1..5d69221c8 100644 --- a/forge/domains/abac/runner.rkt +++ b/forge/domains/abac/runner.rkt @@ -4,6 +4,7 @@ ; Because this DSL is built for a narrow set of exercises, there is no support ; for equality or arbitrary queries; only conjunctive queries are supported. ; Adapted by Tim from EMCSABAC (which used Rosette/Ocelot) in January 2024 +; Adapted again in January 2025 to factor out the domain model. (require forge/domains/abac/lexparse forge/domains/abac/pretty-formatting @@ -11,62 +12,38 @@ (require (only-in racket second string-join remove-duplicates flatten cartesian-product)) -(provide run-commands - boxed-env) +(provide run-commands boxed-env) +; Options other than 'verbose will not be carried into make-run, as that +; is from forge/functional and expects a #:options parameter. This is why the +; calls below explicitly pass the current-state's options. (set-option! 'verbose 0) +; For debugging only +;(set-option! 'solver 'MiniSatProver) +;(set-option! 'logtranslation 2) +;(set-option! 'coregranularity 2) +;(set-option! 'core_minimization 'rce) + + ; State of policy environment, so that REPL can access it after definitions have been run (define boxed-env (box empty)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; We know what the relations are in advance (since this is just for one exercise). -; We do NOT necessarily know what rules they might write/modify. But we're working in EPL, -; so just count unique identifiers (will possibly over-estimate). - -(sig Subject) -(sig Action) -(sig Resource) -(sig Employee #:extends Subject) -(sig Admin #:extends Employee) -(sig Accountant #:extends Employee) -(sig Customer #:extends Subject) -(sig Read #:extends Action) -(sig Write #:extends Action) -(sig File #:extends Resource) - -; As of January 2024, forge/core requires relations to be 2-ary or greater. -; Thus, we'll model these subsets as boolean-valued relations. -(relation Audit (File True)) ; file under audit -(relation Training (Employee True)) ; employee in training - -(relation Owner (Customer File)) ; customer file ownership - -; Skolem relations for the scenario's request -(sig Request #:one) -(relation reqS_rel (Request Subject) #:is func) -(relation reqA_rel (Request Action)) -(relation reqR_rel (Request Resource)) -(define reqS (join Request reqS_rel)) -(define reqA (join Request reqA_rel)) -(define reqR (join Request reqR_rel)) +; We do NOT necessarily know what rules users might write/modify. But we're working in EPL, +; so just count unique identifiers to be complete (will possibly over-estimate). (define request-vars '(s a r)) (define REQUEST-SKOLEM-RELATIONS (list reqS reqA reqR)) -;(define structural-axioms -; (&& (one reqS) ; Skolem constants -; (one reqA) -; (one reqR))) - - (define relations (hash "Admin" Admin "Employee" Employee "Accountant" Accountant "Customer" Customer "Read" Read "Write" Write - "File" File "Under-Audit" Audit "Owner-Of" Owner - "In-Training" Training + "File" File "Under-Audit" audit "Owned-By" owner + "In-Training" training "Subject" Subject "Action" Action "Resource" Resource - "reqS_rel" reqS_rel "reqA_rel" reqA_rel "reqR_rel" reqR_rel + "reqS" reqS "reqA" reqA "reqR" reqR "True" True "Request" Request)) (define the-sigs (filter (lambda (r) (equal? (node/expr-arity r) 1)) (hash-values relations))) (define the-fields (filter (lambda (r) (> (node/expr-arity r) 1)) (hash-values relations))) @@ -90,7 +67,7 @@ (define polname (first args)) (define decname (second args)) (define conditions (rest (rest args))) - (define conditions-fmla (&& (map (lambda (c) (build-condition c relations var->maybe-skolem)) conditions))) + (define conditions-fmla (&& (map (lambda (c) (build-condition relations var->maybe-skolem c)) conditions))) (define pol (find-pol env polname)) (cond [(equal? pol #f) (raise-user-error (format "Unknown policy: ~a" polname))] @@ -117,12 +94,12 @@ (make-bound U File) (make-bound U True) (make-bound U Request) - (make-bound U reqS_rel) - (make-bound U reqA_rel) - (make-bound U reqR_rel) - (make-bound U Owner) - (make-bound U Training) - (make-bound U Audit))) + (make-bound U reqS) + (make-bound U reqA) + (make-bound U reqR) + (make-bound U owner) + (make-bound U training) + (make-bound U audit))) ;(printf "decision: ~a; ~a~n" decision (node? decision)) ;(printf "cf: ~a; ~a~n" conditions-fmla (node? conditions-fmla)) @@ -140,6 +117,7 @@ #:preds (list query) #:sigs the-sigs #:relations the-fields + #:options (forge:State-options forge:curr-state) ;#:scope (list (list Node 6)) #:bounds the-bounds)) @@ -180,9 +158,9 @@ ; Replace variable names with Skolem relation if called for (define (var->maybe-skolem v) - (cond [(equal? v 's) reqS] - [(equal? v 'a) reqA] - [(equal? v 'r) reqR] + (cond [(equal? v 's) (join Request reqS)] + [(equal? v 'a) (join Request reqA)] + [(equal? v 'r) (join Request reqR)] [else v])) ; construct set of atoms to use in bounds @@ -210,12 +188,12 @@ (list (in (atom 'r$0) Resource) (in Resource (+ atoms)))] ; Skolem relations: - [(equal? (relation-name r) "reqS_rel") - (list (= reqS_rel (-> (atom 'Request) (atom 's$0))))] - [(equal? (relation-name r) "reqA_rel") - (list (= reqA_rel (-> (atom 'Request) (atom 'a$0))))] - [(equal? (relation-name r) "reqR_rel") - (list (= reqR_rel (-> (atom 'Request) (atom 'r$0))))] + [(equal? (relation-name r) "reqS") + (list (= reqS (-> (atom 'Request) (atom 's$0))))] + [(equal? (relation-name r) "reqA") + (list (= reqA (-> (atom 'Request) (atom 'a$0))))] + [(equal? (relation-name r) "reqR") + (list (= reqR (-> (atom 'Request) (atom 'r$0))))] [(equal? (relation-name r) "True") (list (= r (atom 'True)))] [(equal? (relation-name r) "Request") @@ -256,7 +234,7 @@ (define queryP1NP2 (&& permit1 (! permit2))) ; first (define queryP2NP1 (&& permit2 (! permit1))) ; second (define where-fmlas (map (lambda (c) - (build-condition c relations var->maybe-skolem)) where)) ; added constraints (if any) + (build-condition relations var->maybe-skolem c)) where)) ; added constraints (if any) (define the-bounds (append (make-bound U Subject) @@ -271,12 +249,12 @@ (make-bound U File) (make-bound U True) (make-bound U Request) - (make-bound U reqS_rel) - (make-bound U reqA_rel) - (make-bound U reqR_rel) - (make-bound U Owner) - (make-bound U Training) - (make-bound U Audit))) + (make-bound U reqS) + (make-bound U reqA) + (make-bound U reqR) + (make-bound U owner) + (make-bound U training) + (make-bound U audit))) ; Try each direction separately so that we can print out which policy decides what. ; (1) P1.permit is not subset of P2.permit @@ -287,12 +265,10 @@ #:preds (cons queryP1NP2 where-fmlas) #:sigs the-sigs #:relations the-fields + #:options (forge:State-options forge:curr-state) ;#:scope (list (list Node 6)) #:bounds the-bounds)) - ;(define solver-result-stream (forge:Run-result p1_notin_p2)) - ;(define first-solution (tree:get-value solver-result-stream)) - (cond [(forge:is-sat? p1_notin_p2) (pretty-printf-result #:bounds the-bounds #:run p1_notin_p2 @@ -311,11 +287,10 @@ #:preds (cons queryP2NP1 where-fmlas) #:sigs the-sigs #:relations the-fields + #:options (forge:State-options forge:curr-state) ;#:scope (list (list Node 6)) #:bounds the-bounds)) -; (define solver-result-stream (forge:Run-result p2_notin_p1)) -; (define first-solution (tree:get-value solver-result-stream)) (pretty-printf-result #:bounds the-bounds #:run p2_notin_p1 #:request-vars request-vars diff --git a/forge/domains/abac/tests/abac2.rkt b/forge/domains/abac/tests/abac2.rkt index b6545355d..5c62c6750 100644 --- a/forge/domains/abac/tests/abac2.rkt +++ b/forge/domains/abac/tests/abac2.rkt @@ -7,11 +7,11 @@ policy original // Administrators can read and write anything permit if: s is admin, a is read. permit if: s is admin, a is write. - // Files being audited can't be changed by customers + // Files being audited can't be changed deny if: a is write, r is file, r is under-audit. // Customers have full access to files they own - permit if: s is customer, a is read, s is owner-of r. - permit if: s is customer, a is write, s is owner-of r. + permit if: s is customer, a is read, r is owned-by s. + permit if: s is customer, a is write, r is owned-by s. end; // Cloud services company. Customers store/update their data. Sometimes audits need to be performed. At first the company is small, @@ -23,11 +23,11 @@ policy modified // Administrators can read and write anything permit if: s is admin, a is read. permit if: s is admin, a is write. - // Files being audited can't be changed by customers + // Files being audited can't be changed deny if: a is write, r is file, r is under-audit. // Customers have full access to files they own - permit if: s is customer, a is read, s is owner-of r. - permit if: s is customer, a is write, s is owner-of r. + permit if: s is customer, a is read, r is owned-by s. + permit if: s is customer, a is write, r is owned-by s. // Once completing training, accountants can read and write (for annotation) to files under audit deny if: s is in-training. @@ -48,15 +48,18 @@ policy modified2 // Files being audited can't be changed by customers deny if: a is write, r is file, r is under-audit. // Customers have full access to files they own - permit if: s is customer, a is read, s is owner-of r. - permit if: s is customer, a is write, s is owner-of r. + permit if: s is customer, a is read, r is owned-by s. + permit if: s is customer, a is write, r is owned-by s. end; - -// compare x; // error +// Expect to see an instance compare original modified; -query original yields permit where s is not admin; -compare original modified2 where s is not accountant; + +// Expect to see an instance +//query original yields permit where s is not admin; + +// Expect to see unsatisfiable +//compare original modified2 where s is not accountant; diff --git a/forge/domains/abac/tests/emcstests.rkt b/forge/domains/abac/tests/emcstests.rkt index e884565ef..f49caa7d9 100644 --- a/forge/domains/abac/tests/emcstests.rkt +++ b/forge/domains/abac/tests/emcstests.rkt @@ -7,8 +7,8 @@ policy filesystem // Files being audited can't be changed by customers deny if: a is write, r is file, r is under-audit. // Customers have full access to files they own - permit if: s is customer, a is read, s is owner-of r. - permit if: s is customer, a is write, s is owner-of r. + permit if: s is customer, a is read, r is owned-by s. + permit if: s is customer, a is write, r is owned-by s. end; query filesystem yields permit where s is customer, a is read; @@ -20,8 +20,8 @@ policy filesystem2 // Files being audited can't be changed by customers deny if: a is write, r is file, r is under-audit. // Customers have full access to files they own - permit if: s is customer, a is read, s is owner-of r. - permit if: s is customer, a is write, s is owner-of r. + permit if: s is customer, a is read, r is owned-by s. + permit if: s is customer, a is write, r is owned-by s. // Accountants can read and write files under audit // but only after completing training diff --git a/forge/froglet/lang/bsl-lang-specific-checks.rkt b/forge/froglet/lang/bsl-lang-specific-checks.rkt index f69a4de6e..f661df4a8 100644 --- a/forge/froglet/lang/bsl-lang-specific-checks.rkt +++ b/forge/froglet/lang/bsl-lang-specific-checks.rkt @@ -25,14 +25,14 @@ (define (raise-bsl-relational-error rel-str node loc [optional-str #f]) (raise-bsl-error - (format "forge/bsl didn't recognize the ~a operator ~a" + (format "Froglet: invalid use of the ~a operator ~a" rel-str (if optional-str (format "; ~a" optional-str) "")) node loc)) (define (raise-bsl-relational-error-expr-args rel-str args loc [optional-str #f]) (raise-bsl-error-deparsed-str - (format "forge/bsl didn't recognize the ~a operator~a" + (format "Froglet: invalid use of the ~a operator~a" rel-str (if optional-str (format "; ~a" optional-str) "")) (cond @@ -46,9 +46,18 @@ (define (srcloc->string loc) (format "line ~a, col ~a, span: ~a" (source-location-line loc) (source-location-column loc) (source-location-span loc))) -(define (err-empty-join expr-node) +; TODO: Special case: take only the node and child-types +; Should be unified with other registered functions +(define (err-empty-join expr-node child-types #:run-or-state [run-or-state #f]) (define loc (nodeinfo-loc (node-info expr-node))) - (raise-bsl-error "Sig does not have such a field" expr-node loc)) + ; Deprimification lets us print, e.g., "Animal" rather than "(Dog Cat Human ...)" + (define lhs-type (if run-or-state + (deprimify run-or-state (expression-type-type (first child-types))) + (expression-type-type (first child-types)))) + (if (and (equal? 1 (length lhs-type)) + (symbol? (first lhs-type))) + (raise-bsl-error (format "Sig ~a does not have such a field" (first lhs-type)) expr-node loc) + (raise-bsl-error (format "No such field in possible types of left-hand-side (~a)" lhs-type) expr-node loc))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Checker functions and checker-hash definitions @@ -83,10 +92,16 @@ ; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; The "in" operator is not allowed in Froglet, except when the LHS is a singleton and the +; RHS is a sig. I.e., it is allowed only when it is used as a type predicate. + (define (check-node-formula-op-in formula-node node-type child-types) (when (eq? (nodeinfo-lang (node-info formula-node)) LANG_ID) - (define loc (nodeinfo-loc (node-info formula-node))) - (raise-bsl-relational-error "\"in\"" formula-node loc))) + (define lhs-multiplicity (expression-type-multiplicity (first child-types))) + (unless (and (equal? lhs-multiplicity 'one) + (Sig? (second (node/formula/op-children formula-node)))) + (define loc (nodeinfo-loc (node-info formula-node))) + (raise-bsl-relational-error "\"in\"" formula-node loc)))) (define (check-top-expression formula-parent expr-node t #:allow-sigs [allow-sigs #f]) (when (and (member t '(func pfunc)) @@ -275,7 +290,7 @@ (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))) ; TODO: add a global field-decl check outside bsl (define (bsl-field-decl-func true-breaker) diff --git a/forge/info.rkt b/forge/info.rkt index 9bb64173f..8f7226d80 100644 --- a/forge/info.rkt +++ b/forge/info.rkt @@ -30,7 +30,7 @@ ;(define scribblings '(("doc/quickstart.scrbl" ()))) -(define license '(MIT)) +(define license 'MIT) ;;;;;;;;;;;;;;;;;;;;;;;;; ; compile-omit-paths @@ -69,4 +69,6 @@ #rx"tests/forge-core/*" #rx"tests/forge-functional/*" "tests/error/" + #rx"domains/abac/tests/*" + #rx"domains/crypto/examples/*" "OLD")) diff --git a/forge/lang/ast.rkt b/forge/lang/ast.rkt index db408ed87..47122d229 100644 --- a/forge/lang/ast.rkt +++ b/forge/lang/ast.rkt @@ -1238,7 +1238,7 @@ ;; BREAKERS -------------------------------------------------------------------- (struct node/breaking node () #:transparent) -(struct node/breaking/op node (children) #:transparent) +(struct node/breaking/op node/breaking (children) #:transparent) (define-node-op is node/breaking/op #f #:max-length 2 #:type (lambda (n) (@or (node/expr? n) (node/breaking/break? n)))) (struct node/breaking/break node/breaking (break) #:transparent) (define-syntax (make-breaker stx) diff --git a/forge/lang/expander.rkt b/forge/lang/expander.rkt index 499995ee5..772c9a3e5 100644 --- a/forge/lang/expander.rkt +++ b/forge/lang/expander.rkt @@ -1190,14 +1190,22 @@ [(and (equal? 1 (length xs)) (node/int? (first xs))) (first xs)] [else + ; *** Error cases *** ; First, check and see whether any individual member of xs is a procedure. If so, it's likely ; the model is using a helper function or predicate incorrectly. (for ([x xs] - [i (build-list 5 (lambda (x) (@+ x 1)))]) + [i (build-list (length xs) (lambda (x) (@+ x 1)))]) (when (procedure? x) (raise-forge-error #:msg (format "Element ~a of this block was an ill-formed predicate or helper function call. Check that the number of arguments given matches the declaration." i) #:context stx))) + ; Next, is there an element of the block that is a binding expression (i.e., meant for inst/example)? + (for ([x xs] + [i (build-list (length xs) (lambda (x) (@+ x 1)))]) + (when (node/breaking? x) + (raise-forge-error + #:msg (format "Element ~a of this block was a binding expression, which should only appear in an `example`, an `inst` declaration, or the bounds annotations of a command. " i) + #:context stx))) ; Otherwise, give a general error message. (raise-forge-error #:msg (format "Ill-formed block: expected either one expression or any number of formulas; got ~a" xs) @@ -1388,13 +1396,16 @@ (syntax/loc stx (join (#:lang (get-check-lang)) expr1 expr2)))] [((~datum Expr) name:NameClass "[" exprs:ExprListClass "]") + ; Is this production ever used? Both box join and helper use seem to use the Expr version below. + ; (printf "expander: Name[Expr...]: ~a~n" #'name) (with-syntax ([name #'name.name] [(exprs ...) (datum->syntax #f (map my-expand (syntax->list #'(exprs.exprs ...))))]) (syntax/loc stx (name exprs ...)))] - - [((~datum Expr) expr1:ExprClass "[" exprs:ExprListClass "]") - (with-syntax ([expr1 (my-expand #'expr1)] + [((~datum Expr) expr1orig:ExprClass "[" exprs:ExprListClass "]") + ; This might be a helper function or predicate invocation (with arguments), or a box join. + ; Note that expr1 might be a macro name *or* a procedure, so we can't necessarily "apply" it. + (with-syntax ([expr1 (my-expand #'expr1orig)] [(exprs ...) (datum->syntax #f (map my-expand (syntax->list #'(exprs.exprs ...))))]) (syntax/loc stx (expr1 exprs ...)))] @@ -1419,9 +1430,11 @@ [((~datum Expr) name:QualNameClass) (define local-value (syntax-local-value #'name.name (lambda () #f))) - ;(printf "local-value for ~a: ~a~n" #'name.name local-value) + ; (printf "local-value for ~a: ~a~n" #'name.name local-value) (if local-value ; if we have a local-value, it's likely a Forge macro or Forge-defined helper procedure + ; (Node ops in the AST are defined as _macros_ to allow the capture of stx location. Thus, + ; e.g., `add` is a macro.) (syntax/loc stx name.name) ; otherwise, it's likely an AST node (to be functionally updated with proper syntax ; location at runtime). Note this is a QualName at compile time, but may be substituted @@ -1444,7 +1457,6 @@ [((~datum Expr) sexpr:SexprClass) (syntax/loc stx (read sexpr))])) - ; struct-copy would not retain the sub-struct identity and fields, producing just a node ; ditto the struct-update-lib library ; struct-set requires using a special form to create the struct. diff --git a/forge/lang/reader.rkt b/forge/lang/reader.rkt index a664b58ed..d084d5225 100644 --- a/forge/lang/reader.rkt +++ b/forge/lang/reader.rkt @@ -128,8 +128,9 @@ (define final `((provide (except-out (all-defined-out) ; So other programs can require it forge:n)) ; but don't share the namespace anchor - (require (only-in racket/base unless hash-empty?)) ; needed to use "unless" etc. - (require forge/sigs-structs) ; needed to access State struct + ; Most Forge stuff should be available via the module language below. But some + ; Racket functions are needed too. + (require (only-in racket/base unless hash-empty?)) (require (only-in forge/shared do-time)) (do-time "forge-mod toplevel") @@ -167,7 +168,7 @@ (output-all-test-failures) ; At this point, all commands should be defined. Open Sterling, if there ; are commands to visualize. If not, don't try to open Sterling. - (unless (hash-empty? (State-runmap forge:curr-state)) + (unless (hash-empty? (forge:State-runmap forge:curr-state)) (start-sterling-menu forge:curr-state forge:nsa))) ;; Declare submodule "main" diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt index f7b7b8e76..92d3f493f 100644 --- a/forge/last-checker.rkt +++ b/forge/last-checker.rkt @@ -16,7 +16,7 @@ (require forge/utils/collector) -(provide checkFormula checkExpression checkInt primify infer-atom-type dfs-sigs deprimify) +(provide checkFormula checkExpression checkInt infer-atom-type) ; 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 @@ -240,10 +240,14 @@ ; IN (atomic fmla) [(? node/formula/op/in?) + (define child-types (map (lambda (x) (checkExpression run-or-state x quantvars checker-hash)) args)) (check-and-output formula node/formula/op/in checker-hash - (for-each (lambda (x) (expression-type-type (checkExpression run-or-state x quantvars checker-hash))) args))] + ;(for-each (lambda (x) (expression-type-type (checkExpression run-or-state x quantvars checker-hash))) args) + (void) + child-types + )] ; EQUALS [(? node/formula/op/=?) @@ -269,41 +273,6 @@ (checkInt run-or-state (first (node/formula/op-children formula)) quantvars checker-hash) (checkInt run-or-state (second (node/formula/op-children formula)) quantvars checker-hash)])) -; Turn signame into list of all primsigs it contains -; Note we use Alloy-style "_remainder" names here; these aren't necessarily embodied in Forge -(define/contract (primify run-or-state raw-signame) - (@-> (or/c Run? State? Run-spec?) (or/c symbol? string?) (listof symbol?)) - (let ([signame (cond [(string? raw-signame) (string->symbol raw-signame)] - [(Sig? raw-signame) (Sig-name raw-signame)] - [else raw-signame])]) - (cond [(equal? 'Int signame) - '(Int)] - [(equal? 'univ signame) - (if (member (get-option (get-run-spec run-or-state) 'backend) UNBOUNDED_INT_BACKENDS) - (remove-duplicates (flatten (map (lambda (n) (primify run-or-state n)) (remove 'Int (map Sig-name (get-sigs run-or-state)))))) - (remove-duplicates (flatten (map (lambda (n) (primify run-or-state n)) (cons 'Int (map Sig-name (get-sigs run-or-state)))))))] - [else - (define the-sig (get-sig run-or-state signame)) - (define all-primitive-descendants - (remove-duplicates - (flatten - (map (lambda (n) (primify run-or-state n)) - (get-children run-or-state signame))))) - (cond - [(Sig-abstract the-sig) - - (if (empty? (get-children run-or-state signame)) - (raise-forge-error - #:msg (format "The abstract sig ~a is not extended by any children" (symbol->string signame)) - #:context the-sig) - all-primitive-descendants)] - [else (cons - (string->symbol (string-append (symbol->string signame) - (if (empty? (get-children run-or-state signame)) - "" - "_remainder"))) - all-primitive-descendants)])]))) - ; Infer a type for an atom node. ; Best data source: the last Sterling instance of this run. @@ -350,43 +319,6 @@ [(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] - [else (define next (first todo)) - (define-values (new-acc stop) - (func next acc)) ; use define-values with the return of func - (cond [stop (dfs-sigs-helper (rest todo) new-acc)] - [else (define next-list (if (empty? (get-children run-or-state next)) ; empty? - (rest todo) - (append (get-children run-or-state next) (rest todo)))) ; append instead - (dfs-sigs-helper next-list new-acc)])])) - (dfs-sigs-helper sigs init-acc)) ; maybe take in initial accumulator as well for more flexibility - -; Be robust to callers who pass quantifier-vars as either (var . domain) or as '(var domain). -(define (second/safe list-or-pair) - (cond [(list? list-or-pair) (second list-or-pair)] - [else (cdr list-or-pair)])) - -(define (deprimify run-or-state primsigs) - (let ([all-sigs (map Sig-name (get-sigs run-or-state))]) - (cond - [(equal? primsigs '(Int)) - 'Int] - [(equal? primsigs (remove-duplicates (flatten (map (lambda (n) (primify run-or-state n)) (cons 'Int all-sigs))))) - 'univ] - [else (define top-level (get-top-level-sigs run-or-state)) - (define pseudo-fold-lambda (lambda (sig acc) (if (or (subset? (primify run-or-state (Sig-name sig)) (flatten primsigs)) - (equal? (list (car (primify run-or-state (Sig-name sig)))) (flatten primsigs))) - ; the above check is added for when you have the parent sig, but are expecting the child - (values (append acc (list (Sig-name sig))) #t) ; replace cons with values - (values acc #f)))) - (define final-list (dfs-sigs run-or-state pseudo-fold-lambda top-level '())) - final-list]))) ; wrap around checkExpression-mult to provide check for multiplicity, ; while throwing the multiplicity away in output; DO NOT CALL THIS AS PASSTHROUGH! @@ -489,6 +421,7 @@ [(node/expr/ite info arity a b c) (let ([b-potentials (checkExpression-mult run-or-state b quantvars checker-hash)] [c-potentials (checkExpression-mult run-or-state c quantvars checker-hash)]) + (check-and-output expr node/expr/ite checker-hash @@ -524,7 +457,7 @@ (expression-type (let ([prims (primify run-or-state 'univ)]) (cond [(equal? arity 1) (map list prims)] [else (cartesian-product prims prims)])) - 'set + (if (equal? type 'none) 'lone 'set) ; If any of the sigs are "var", then univ and iden may vary. (if (and (member type '(univ iden)) (not (empty? (andmap (lambda (s) (node/expr/relation-is-variable s)) (get-sigs run-or-state))))) @@ -768,10 +701,11 @@ checker-hash (let* ([join-result (check-join (map expression-type-type child-types))] [join-top-level (check-join (map (lambda (x) (list (expression-type-top-level-types x))) child-types))]) - (when (@>= (get-verbosity) VERBOSITY_LASTCHECK) (when (empty? join-result) - (if (eq? (nodeinfo-lang (node-info expr)) 'bsl) - ((hash-ref checker-hash 'empty-join) expr) + ; The last-checker doesn't issue many errors on its own, but this is one such situation. + ; Make sure the language doesn't want to produce its own custom error in this case. + (if (hash-has-key? checker-hash 'empty-join) + ((hash-ref checker-hash 'empty-join) expr child-types #:run-or-state run-or-state) (raise-forge-error #:msg (format "Join always results in an empty relation:\ Left argument of join \"~a\" is in ~a.\ @@ -780,17 +714,9 @@ (map (lambda (lst) (string-join (map (lambda (c) (symbol->string c)) lst) " -> " #:before-first "(" #:after-last ")")) (expression-type-type (first child-types))) (deparse (second (node/expr/op-children expr))) (map (lambda (lst) (string-join (map (lambda (c) (symbol->string c)) lst) " -> " #:before-first "(" #:after-last ")")) (expression-type-type (second child-types)))) - #:context expr)))) - - ; If we are in Froglet ("bsl"), and the LHS expression is not a singleton or empty, lang-specific check - ; TODO: disentangle this; it should be handled by the join case of the checker hash - ;(when (and (not (member (expression-type-multiplicity (first child-types)) '(one lone))) - ; (eq? (nodeinfo-lang (node-info expr)) 'bsl) - ; (hash-has-key? checker-hash 'relation-join)) - ; ((hash-ref checker-hash 'relation-join) expr args)) - + #:context expr))) + (define join-multip (join-multiplicity args child-types join-result expr)) - ;(printf "***** ~a~n ~a ~a~n" expr args join-multip) (expression-type join-result join-multip @@ -949,9 +875,6 @@ (cons (list var domain) quantvars)) (void)])) -; Do not check integer literals with respect to bitwidth for these backends -(define UNBOUNDED_INT_BACKENDS '(smtlibtor)) - ; Is this integer literal safe under the current bitwidth? (define/contract (check-int-literal run-or-state expr) (@-> (or/c Run? State? Run-spec?) diff --git a/forge/server/forgeserver.rkt b/forge/server/forgeserver.rkt index d974de326..d097f603b 100644 --- a/forge/server/forgeserver.rkt +++ b/forge/server/forgeserver.rkt @@ -509,25 +509,4 @@ ; Now, serve the static sterling website files (this will be a different server/port). (unless (equal? 'off (get-option curr-state 'run_sterling)) - (serve-sterling-static #:provider-port port))) - -;; (cond [(string? port) -;; (displayln "NO PORTS AVAILABLE. Unable to start web server that listens for Sterling messages.")] -;; [(equal? 'off (get-option curr-state 'run_sterling)) -;; (void)] -;; [else -;; ; Attempt to open a browser to the Sterling index.html, with the proper port -;; ; If this cannot be opened for whatever reason, keep the server open but print -;; ; a warning, allowing the user a workaround. -;; (with-handlers ([exn? -;; (lambda (e) (printf "Racket could not open a browser on your system; you may be able manually navigate to this address, which is where Forge expects Sterling to load:~n ~a~n" -;; (string-append (path->string sterling-path) "?" (number->string port))))]) -;; (send-url/file sterling-path #f #:query (number->string port))) -;; -;; (printf "Sterling running. Hit enter to stop service.\n") -;; (when (> (get-verbosity) VERBOSITY_LOW) -;; (printf "Using port: ~a~n" (number->string port))) -;; (flush-output) -;; (void (read-char)) -;; ; Once a character is read, stop the server -;; (stop-service)])) \ No newline at end of file + (serve-sterling-static #:provider-port port))) \ No newline at end of file diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt index 175a5bb1c..e0d5ab6a8 100644 --- a/forge/sigs-structs.rkt +++ b/forge/sigs-structs.rkt @@ -3,15 +3,17 @@ ; Structures and helper functions for running Forge, along with some constants and ; configuration code (e.g., most options). -(require (except-in forge/lang/ast ->) +(require (except-in forge/lang/ast -> set) forge/lang/bounds forge/breaks (only-in forge/shared get-verbosity VERBOSITY_HIGH)) (require (prefix-in @ (only-in racket hash not +)) - (only-in racket nonnegative-integer? thunk curry first) + (only-in racket nonnegative-integer? thunk curry) (prefix-in @ racket/set)) (require racket/contract - racket/match) + racket/match + racket/set + racket/list) (require (for-syntax racket/base racket/syntax syntax/srcloc syntax/parse)) (require (prefix-in tree: forge/utils/lazy-tree)) (require syntax/srcloc) @@ -838,4 +840,83 @@ Returns whether the given run resulted in sat or unsat, respectively. (define (Relation-is? r sym-list) (and (Relation? r) (node/breaking/break? (Relation-breaker r)) - (member (node/breaking/break-break (Relation-breaker r)) sym-list))) \ No newline at end of file + (member (node/breaking/break-break (Relation-breaker r)) sym-list))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; "Primification"-related utilities +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; Do not check integer literals with respect to bitwidth for these backends +(define UNBOUNDED_INT_BACKENDS '(smtlibtor)) + +; Turn signame into list of all primsigs it contains +; Note we use Alloy-style "_remainder" names here; these aren't necessarily embodied in Forge +(define/contract (primify run-or-state raw-signame) + (-> (or/c Run? State? Run-spec?) (or/c symbol? string?) (listof symbol?)) + (let ([signame (cond [(string? raw-signame) (string->symbol raw-signame)] + [(Sig? raw-signame) (Sig-name raw-signame)] + [else raw-signame])]) + (cond [(equal? 'Int signame) + '(Int)] + [(equal? 'univ signame) + (if (member (get-option (get-run-spec run-or-state) 'backend) UNBOUNDED_INT_BACKENDS) + (remove-duplicates (flatten (map (lambda (n) (primify run-or-state n)) (remove 'Int (map Sig-name (get-sigs run-or-state)))))) + (remove-duplicates (flatten (map (lambda (n) (primify run-or-state n)) (cons 'Int (map Sig-name (get-sigs run-or-state)))))))] + [else + (define the-sig (get-sig run-or-state signame)) + (define all-primitive-descendants + (remove-duplicates + (flatten + (map (lambda (n) (primify run-or-state n)) + (get-children run-or-state signame))))) + (cond + [(Sig-abstract the-sig) + + (if (empty? (get-children run-or-state signame)) + (raise-forge-error + #:msg (format "The abstract sig ~a is not extended by any children" (symbol->string signame)) + #:context the-sig) + all-primitive-descendants)] + [else (cons + (string->symbol (string-append (symbol->string signame) + (if (empty? (get-children run-or-state signame)) + "" + "_remainder"))) + all-primitive-descendants)])]))) + +(define (deprimify run-or-state primsigs) + (let ([all-sigs (map Sig-name (get-sigs run-or-state))]) + (cond + [(equal? primsigs '(Int)) + 'Int] + [(equal? primsigs (remove-duplicates (flatten (map (lambda (n) (primify run-or-state n)) (cons 'Int all-sigs))))) + 'univ] + [else (define top-level (get-top-level-sigs run-or-state)) + (define pseudo-fold-lambda (lambda (sig acc) (if (or (subset? (primify run-or-state (Sig-name sig)) (flatten primsigs)) + (equal? (list (car (primify run-or-state (Sig-name sig)))) (flatten primsigs))) + ; the above check is added for when you have the parent sig, but are expecting the child + (values (append acc (list (Sig-name sig))) #t) ; replace cons with values + (values acc #f)))) + (define final-list (dfs-sigs run-or-state pseudo-fold-lambda top-level '())) + final-list]))) + +; 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] + [else (define next (first todo)) + (define-values (new-acc stop) + (func next acc)) ; use define-values with the return of func + (cond [stop (dfs-sigs-helper (rest todo) new-acc)] + [else (define next-list (if (empty? (get-children run-or-state next)) ; empty? + (rest todo) + (append (get-children run-or-state next) (rest todo)))) ; append instead + (dfs-sigs-helper next-list new-acc)])])) + (dfs-sigs-helper sigs init-acc)) ; maybe take in initial accumulator as well for more flexibility + +; Be robust to callers who pass quantifier-vars as either (var . domain) or as '(var domain). +(define (second/safe list-or-pair) + (cond [(list? list-or-pair) (second list-or-pair)] + [else (cdr list-or-pair)])) diff --git a/forge/sigs.rkt b/forge/sigs.rkt index 5846780cc..eaeca3c4f 100644 --- a/forge/sigs.rkt +++ b/forge/sigs.rkt @@ -660,6 +660,9 @@ ; (N.B., this assumes the run isn't actually created or sent to the solver.) (define run-reference #f) + ; `is forge_error` should be satisfied by an error produced via raise-forge-error. These + ; are exn:fail:user values. Other Racket errors, such as arity errors, use a different + ; error value type, and so would not be considered valid for `is forge_error` testing. (with-handlers ([exn:fail:user? (lambda (e) (unless (or (not expected-details) @@ -1138,6 +1141,8 @@ (printf "Test ~a failed. Stopping execution.~n" name)) (when (and (Run? run-or-state) sterling) (true-display run-or-state)) + ;; !!!!! ^^^^ This is a problem! Because the error is raised only after Sterling terminates. + ;; (and this is a single thread only) (raise-forge-error #:msg msg #:context context)])) ; To be run at the very end of the Forge execution; reports test failures and opens diff --git a/forge/tests/error/abstract.frg b/forge/tests/error/abstract.frg index 8218ed972..be1fd3448 100644 --- a/forge/tests/error/abstract.frg +++ b/forge/tests/error/abstract.frg @@ -1,6 +1,6 @@ #lang forge option run_sterling off - +option verbose 0 one sig A { field: one B} abstract sig B{ diff --git a/forge/tests/error/bsl-join-right.frg b/forge/tests/error/bsl-join-right.frg index 28a324dc6..3b1279a73 100644 --- a/forge/tests/error/bsl-join-right.frg +++ b/forge/tests/error/bsl-join-right.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Node { next: one Node diff --git a/forge/tests/error/bsl-join-right2.frg b/forge/tests/error/bsl-join-right2.frg index 9ae6b4a9d..46bda8276 100644 --- a/forge/tests/error/bsl-join-right2.frg +++ b/forge/tests/error/bsl-join-right2.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Node { next: one Node, diff --git a/forge/tests/error/bsl-join-right3.frg b/forge/tests/error/bsl-join-right3.frg index 4b7a28b85..f6dd592fc 100644 --- a/forge/tests/error/bsl-join-right3.frg +++ b/forge/tests/error/bsl-join-right3.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Node { next: one Node, diff --git a/forge/tests/error/bsl-join-right4.frg b/forge/tests/error/bsl-join-right4.frg index 1b5a05e41..27373d530 100644 --- a/forge/tests/error/bsl-join-right4.frg +++ b/forge/tests/error/bsl-join-right4.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Course {} sig Grade {} diff --git a/forge/tests/error/bsl-join-right5.frg b/forge/tests/error/bsl-join-right5.frg index 23bf5cf02..78c1d98a1 100644 --- a/forge/tests/error/bsl-join-right5.frg +++ b/forge/tests/error/bsl-join-right5.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Node { next: lone Node, diff --git a/forge/tests/error/bsl-join-right6.frg b/forge/tests/error/bsl-join-right6.frg index daa2063ae..0965d5414 100644 --- a/forge/tests/error/bsl-join-right6.frg +++ b/forge/tests/error/bsl-join-right6.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Node { next: one Node, diff --git a/forge/tests/error/bsl-join.frg b/forge/tests/error/bsl-join.frg index 4f9291370..8815426eb 100644 --- a/forge/tests/error/bsl-join.frg +++ b/forge/tests/error/bsl-join.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Node { next: one Node diff --git a/forge/tests/error/bsl-join2.frg b/forge/tests/error/bsl-join2.frg index ea8014598..ff705f7ef 100644 --- a/forge/tests/error/bsl-join2.frg +++ b/forge/tests/error/bsl-join2.frg @@ -1,5 +1,6 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { field: pfunc Node -> Node diff --git a/forge/tests/error/bsl-join3.frg b/forge/tests/error/bsl-join3.frg index e4b75096c..3ee08da21 100644 --- a/forge/tests/error/bsl-join3.frg +++ b/forge/tests/error/bsl-join3.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Node { next: one Node diff --git a/forge/tests/error/bsl-reachable.frg b/forge/tests/error/bsl-reachable.frg index ebd016f4d..9a7dedde2 100644 --- a/forge/tests/error/bsl-reachable.frg +++ b/forge/tests/error/bsl-reachable.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Node { next: lone Node diff --git a/forge/tests/error/bsl-set-singleton-equal.frg b/forge/tests/error/bsl-set-singleton-equal.frg index 35a659900..866f670d2 100644 --- a/forge/tests/error/bsl-set-singleton-equal.frg +++ b/forge/tests/error/bsl-set-singleton-equal.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Node { next: one Node diff --git a/forge/tests/error/bsl-set.frg b/forge/tests/error/bsl-set.frg index f278d2f8d..5555e52e7 100644 --- a/forge/tests/error/bsl-set.frg +++ b/forge/tests/error/bsl-set.frg @@ -1,6 +1,6 @@ #lang forge/froglet option run_sterling off - +option verbose 0 sig Node { next: one Node diff --git a/forge/tests/error/froglet-compareop0.frg b/forge/tests/error/froglet-compareop0.frg deleted file mode 100644 index 4ebfab02b..000000000 --- a/forge/tests/error/froglet-compareop0.frg +++ /dev/null @@ -1,15 +0,0 @@ -#lang forge/froglet - -abstract sig Position {} -one sig Near extends Position {} -one sig Far extends Position {} - -sig State { - torch: one Position, - spent: one Int -} - -pred ValidState[s: State] { - s.torch = 0 -} - diff --git a/forge/tests/error/froglet-compareop1.frg b/forge/tests/error/froglet-compareop1.frg deleted file mode 100644 index 904662fd1..000000000 --- a/forge/tests/error/froglet-compareop1.frg +++ /dev/null @@ -1,15 +0,0 @@ -#lang forge/froglet - -abstract sig Position {} -one sig Near extends Position {} -one sig Far extends Position {} - -sig State { - torch: one Position, - spent: one Int -} - -pred ValidState[s: State] { - s.spent = Near -} - diff --git a/forge/tests/error/froglet-compareop2.frg b/forge/tests/error/froglet-compareop2.frg deleted file mode 100644 index 1bf5d24ec..000000000 --- a/forge/tests/error/froglet-compareop2.frg +++ /dev/null @@ -1,15 +0,0 @@ -#lang forge/froglet - -abstract sig Position {} -one sig Near extends Position {} -one sig Far extends Position {} - -sig State { - torch: one Position, - spent: one Int -} - -pred ValidState[s: State] { - s.torch <= 2 -} - diff --git a/forge/tests/error/froglet-compareop3.frg b/forge/tests/error/froglet-compareop3.frg deleted file mode 100644 index ffa34321e..000000000 --- a/forge/tests/error/froglet-compareop3.frg +++ /dev/null @@ -1,15 +0,0 @@ -#lang forge/froglet - -abstract sig Position {} -one sig Near extends Position {} -one sig Far extends Position {} - -sig State { - torch: one Position, - spent: one Int -} - -pred ValidState[s: State] { - s.spent <= Near -} - diff --git a/forge/tests/error/froglet-field-shadow.frg b/forge/tests/error/froglet-field-shadow.frg index 398cd8497..a652b6ffa 100644 --- a/forge/tests/error/froglet-field-shadow.frg +++ b/forge/tests/error/froglet-field-shadow.frg @@ -1,6 +1,7 @@ #lang forge/froglet -// Student created a quantified variable that's named the same as a field, then tried to use the field. (https://edstem.org/us/courses/31922/discussion/2548781?comment=5844098). +// Student created a quantified variable that's named the same as a field, then tried to use the field. +// (https://edstem.org/us/courses/31922/discussion/2548781?comment=5844098). // https://edstem.org/us/courses/31922/discussion/2548781?comment=5844098 sig Person { @@ -13,6 +14,10 @@ pred ownGrandparent { } } +run {ownGrandparent} +// TODO: this won't error without the join issue; shadowing isn't being warned + + //pred oG2 { // some me: Person, spouse: Person | { // spouse.spouse = me diff --git a/forge/tests/error/froglet-is-linear0.frg b/forge/tests/error/froglet-is-linear0.frg index cd57ce53e..c8b83045e 100644 --- a/forge/tests/error/froglet-is-linear0.frg +++ b/forge/tests/error/froglet-is-linear0.frg @@ -1,11 +1,13 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { next: lone Node } -pred pp { +// Attempt to use a binding expression in a predicate, rather than inst/example +pred ppred { next is linear } - +run {ppred} diff --git a/forge/tests/error/froglet-is-linear1.frg b/forge/tests/error/froglet-is-linear1.frg index a9061b7b0..aa5bcdf72 100644 --- a/forge/tests/error/froglet-is-linear1.frg +++ b/forge/tests/error/froglet-is-linear1.frg @@ -1,9 +1,11 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { next: lone Node } +// Attempt to use "is linear" binding expression on a sig, not a field check {} for { Node is linear } diff --git a/forge/tests/error/froglet-join-right3.frg b/forge/tests/error/froglet-join-right3.frg index 4176883ff..bac757214 100644 --- a/forge/tests/error/froglet-join-right3.frg +++ b/forge/tests/error/froglet-join-right3.frg @@ -1,5 +1,6 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { next: one Node, diff --git a/forge/tests/error/froglet-join-right4.frg b/forge/tests/error/froglet-join-right4.frg index 9130162cb..04b1ed675 100644 --- a/forge/tests/error/froglet-join-right4.frg +++ b/forge/tests/error/froglet-join-right4.frg @@ -1,5 +1,6 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Course {} sig Grade {} diff --git a/forge/tests/error/froglet-join-right5.frg b/forge/tests/error/froglet-join-right5.frg index 52924ee43..08333f7ed 100644 --- a/forge/tests/error/froglet-join-right5.frg +++ b/forge/tests/error/froglet-join-right5.frg @@ -1,5 +1,6 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { next: lone Node, diff --git a/forge/tests/error/froglet-join-right6.frg b/forge/tests/error/froglet-join-right6.frg index 375e12cd0..9b201a3e7 100644 --- a/forge/tests/error/froglet-join-right6.frg +++ b/forge/tests/error/froglet-join-right6.frg @@ -1,5 +1,6 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { next: one Node, diff --git a/forge/tests/error/froglet-join.frg b/forge/tests/error/froglet-join.frg index ea3031e2e..8e7449d88 100644 --- a/forge/tests/error/froglet-join.frg +++ b/forge/tests/error/froglet-join.frg @@ -1,5 +1,6 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { next: one Node diff --git a/forge/tests/error/froglet-join2.frg b/forge/tests/error/froglet-join2.frg index d792e7c0d..1094c1c7a 100644 --- a/forge/tests/error/froglet-join2.frg +++ b/forge/tests/error/froglet-join2.frg @@ -1,5 +1,6 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { field: pfunc Node -> Node diff --git a/forge/tests/error/froglet-join3.frg b/forge/tests/error/froglet-join3.frg index 8da975cbf..3ee08da21 100644 --- a/forge/tests/error/froglet-join3.frg +++ b/forge/tests/error/froglet-join3.frg @@ -1,5 +1,6 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { next: one Node diff --git a/forge/tests/error/froglet-no-field.frg b/forge/tests/error/froglet-no-field.frg deleted file mode 100644 index 7afaaa4ed..000000000 --- a/forge/tests/error/froglet-no-field.frg +++ /dev/null @@ -1,13 +0,0 @@ -#lang forge/froglet - -// no father = disallowed at toplevel - -sig Person { - father: lone Person -} -one sig Tim extends Person {} - -pred myPred { - no father -} - diff --git a/forge/tests/error/froglet-pred.frg b/forge/tests/error/froglet-pred.frg index 4430795d7..565b640ed 100644 --- a/forge/tests/error/froglet-pred.frg +++ b/forge/tests/error/froglet-pred.frg @@ -8,3 +8,5 @@ pred foo { a a } + +run { foo } \ No newline at end of file diff --git a/forge/tests/error/froglet-pubkey2.frg b/forge/tests/error/froglet-pubkey2.frg deleted file mode 100644 index 93f061126..000000000 --- a/forge/tests/error/froglet-pubkey2.frg +++ /dev/null @@ -1,21 +0,0 @@ -#lang forge/froglet -- forge - -abstract sig Key {} -sig Pubk, Privk extends Key {} - -one sig Authority { - pairs: func Pubk -> Privk -} - -fun counterpart[k: one Key]: one Key { - -- this produces an error, since k is known to be a Pubk - /* - join always results in an empty relation: - Left argument of join "(Authority.pairs)" is in ((Pubk -> Privk)) - Right argument of join "k" is in ((Pubk)) - There is no possible join result - in: "(Authority.pairs.k)" - */ - Authority.pairs.k -} - diff --git a/forge/tests/error/froglet-reachable2.frg b/forge/tests/error/froglet-reachable-2.frg similarity index 78% rename from forge/tests/error/froglet-reachable2.frg rename to forge/tests/error/froglet-reachable-2.frg index 65748e57c..fd885feda 100644 --- a/forge/tests/error/froglet-reachable2.frg +++ b/forge/tests/error/froglet-reachable-2.frg @@ -1,5 +1,6 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { next: lone Node @@ -13,4 +14,4 @@ pred cycle { all n: Node | reachable[next, n, next] } -test expect {{cycle} is sat} +test expect {{cycle} is sat} \ No newline at end of file diff --git a/forge/tests/error/froglet-reachable-3.frg b/forge/tests/error/froglet-reachable-3.frg new file mode 100644 index 000000000..72e003f0e --- /dev/null +++ b/forge/tests/error/froglet-reachable-3.frg @@ -0,0 +1,17 @@ +#lang forge/froglet +option run_sterling off +option verbose 0 + +sig Node { + next: lone Node +} + +sig A { + field: one Node +} + +pred cycle { + reachable[] +} + +assert {cycle} is sat \ No newline at end of file diff --git a/forge/tests/error/froglet-reachable4.frg b/forge/tests/error/froglet-reachable-4.frg similarity index 80% rename from forge/tests/error/froglet-reachable4.frg rename to forge/tests/error/froglet-reachable-4.frg index 0570f0a0c..402c68e8e 100644 --- a/forge/tests/error/froglet-reachable4.frg +++ b/forge/tests/error/froglet-reachable-4.frg @@ -1,5 +1,6 @@ #lang forge/froglet option run_sterling off +option verbose 0 sig Node { next: lone Node @@ -12,5 +13,4 @@ sig A { pred cycle { all n: Node | reachable[n.next] } - - +assert {cycle} is sat \ No newline at end of file diff --git a/forge/tests/error/froglet-reachable5.frg b/forge/tests/error/froglet-reachable5.frg index 0ff81bbd6..ba28a21e8 100644 --- a/forge/tests/error/froglet-reachable5.frg +++ b/forge/tests/error/froglet-reachable5.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 option run_sterling off -- error: cannot reach target because types don't line up @@ -15,7 +16,7 @@ sig NC extends Node { nc: lone NA } -pred cycle { +reach5: run { all n: NA | reachable[n, n.na, na, nb] } diff --git a/forge/tests/error/froglet-reachable6.frg b/forge/tests/error/froglet-reachable6.frg index 8881941a7..d3e47a4ff 100644 --- a/forge/tests/error/froglet-reachable6.frg +++ b/forge/tests/error/froglet-reachable6.frg @@ -11,7 +11,7 @@ sig NB extends Node { nb: lone NB } -pred cycle { +reach6: run { all n: NA | reachable[n, n.na, na, nb] } diff --git a/forge/tests/error/froglet-uni-0.frg b/forge/tests/error/froglet-uni-0.frg deleted file mode 100644 index 8c306efa8..000000000 --- a/forge/tests/error/froglet-uni-0.frg +++ /dev/null @@ -1,16 +0,0 @@ -#lang forge/froglet -option run_sterling off - -sig University {} -one sig BrownU extends University {} -sig Person { - father: lone Person, - mother: lone Person, - grad: lone University -} -one sig Tim extends Person {} - -pred myPred { - father.grad = mother.grad -} - diff --git a/forge/tests/error/froglet-uni-1.frg b/forge/tests/error/froglet-uni-1.frg deleted file mode 100644 index 20336e55d..000000000 --- a/forge/tests/error/froglet-uni-1.frg +++ /dev/null @@ -1,15 +0,0 @@ -#lang forge/froglet -option run_sterling off - -sig University {} -one sig BrownU extends University {} -sig Person { - father: lone Person, - mother: lone Person, - grad: lone University -} -one sig Tim extends Person {} - -pred myPred { - some father.grad -} diff --git a/forge/tests/error/froglet-uni-2.frg b/forge/tests/error/froglet-uni-2.frg deleted file mode 100644 index 7a3b2cc42..000000000 --- a/forge/tests/error/froglet-uni-2.frg +++ /dev/null @@ -1,15 +0,0 @@ -#lang forge/froglet -option run_sterling off - -sig University {} -one sig BrownU extends University {} -sig Person { - father: lone Person, - mother: lone Person, - grad: lone University -} -one sig Tim extends Person {} - -pred myPred { - some father -} diff --git a/forge/tests/error/froglet-uni-3.frg b/forge/tests/error/froglet-uni-3.frg deleted file mode 100644 index 65d07a68b..000000000 --- a/forge/tests/error/froglet-uni-3.frg +++ /dev/null @@ -1,15 +0,0 @@ -#lang forge/froglet -option run_sterling off - -sig University {} -one sig BrownU extends University {} -sig Person { - father: lone Person, - mother: lone Person, - grad: lone University -} -one sig Tim extends Person {} - -pred myPred { - some father.Tim -} diff --git a/forge/tests/error/froglet-uni-4.frg b/forge/tests/error/froglet-uni-4.frg deleted file mode 100644 index 9fbb727dd..000000000 --- a/forge/tests/error/froglet-uni-4.frg +++ /dev/null @@ -1,15 +0,0 @@ -#lang forge/froglet -option run_sterling off - -sig University {} -one sig BrownU extends University {} -sig Person { - father: lone Person, - mother: lone Person, - grad: lone University -} -one sig Tim extends Person {} - -pred myPred { - some p: Person | reachable[p, father.Tim, father, mother] -} diff --git a/forge/tests/error/froglet-uni-5.frg b/forge/tests/error/froglet-uni-5.frg deleted file mode 100644 index d8c9f44f9..000000000 --- a/forge/tests/error/froglet-uni-5.frg +++ /dev/null @@ -1,15 +0,0 @@ -#lang forge/froglet -option run_sterling off - -sig University {} -one sig BrownU extends University {} -sig Person { - father: lone Person, - mother: lone Person, - grad: lone University -} -one sig Tim extends Person {} - -pred myPred { - some Tim.Tim -} diff --git a/forge/tests/error/main.rkt b/forge/tests/error/main.rkt index c01ba2cf0..83d7e6718 100644 --- a/forge/tests/error/main.rkt +++ b/forge/tests/error/main.rkt @@ -29,8 +29,8 @@ (list "expect-predicate-args.frg" #rx"Element 1 of this block was an ill-formed") (list "expect-predicate-no-args.frg" #rx"expect-predicate-no-args.frg:13:45.*Tried to give arguments to a predicate, but it takes none") - ; TODO: needs switch to raise-forge-error so the proper location is in the message - ; (list "expect-fun-args.frg" #rx"Racket procedure, which is likely.*expect-fun-args.frg:11") + (list "expect-fun-args.frg" #rx".*expect-fun-args.frg:11.*got unknown expression type") + ; TODO: needs to confirm that equality is irrespective of source location (it should be) ;(list "expect-fun-no-args.frg" #rx"TODO") @@ -82,68 +82,49 @@ (list "bsl-reachable-nonfield.frg" #rx"Field argument given to reachable is not a field") (list "bsl-reachable-too-few-arguments.frg" #rx"The reachable predicate expected at least three arguments, given 2") -; (list "froglet-ast-arrow.frg" #rx"-> operator is not") + (list "froglet-ast-arrow.frg" #rx"-> in a formula") + (list "froglet-ast-intersect.frg" #rx"invalid use of the &") + (list "froglet-ast-minus.frg" #rx"invalid use of the -") + (list "froglet-ast-plus.frg" #rx"invalid use of the \\+") + (list "froglet-ast-star.frg" #rx"invalid use of the \\*") + (list "froglet-ast-transitive-closure.frg" #rx"invalid use of the \\^") + (list "froglet-ast-transpose.frg" #rx"invalid use of the ~ operator") + (list "froglet-ast-notimplies.frg" #rx"parsing error") + (list "froglet-arrow.frg" #rx"->") + (list "froglet-http.frg" #rx"Field declaration") + (list "froglet-int-minus.frg" #rx"invalid use of the -") + (list "froglet-pred.frg" #rx"ill-formed predicate") + (list "froglet-is-linear0.frg" #rx"was a binding expression") + (list "froglet-join-right.frg" #rx"not an object") + (list "froglet-join-right2.frg" #rx"not an object") + (list "froglet-join-right3.frg" #rx"not an object") + (list "froglet-join-right4.frg" #rx"not an object") + (list "froglet-join-right5.frg" #rx"not an object") + (list "froglet-join-right6.frg" #rx"not an object") + (list "froglet-join.frg" #rx"not an object") + (list "froglet-join2.frg" #rx"did not result in a singleton") + (list "froglet-join3.frg" #rx"not an object") + (list "froglet-set-singleton-equal.frg" #rx"not a singleton") + (list "froglet-set.frg" #rx"not a singleton") + (list "froglet-is-linear1.frg" #rx"Attempted to set or modify bound") + + (list "froglet-reachable-2.frg" #rx"is not a singleton") + (list "froglet-reachable-3.frg" #rx"parsing error") + (list "froglet-reachable-4.frg" #rx"expected: at least 2") + + +; These checks are not implemented in the runtime last-checker +; (list "froglet-reachable5.frg" #rx"reachable found no path to target") +; (list "froglet-reachable6.frg" #rx"reachable cannot use field") + +; This keyword is unsupported. ; (list "froglet-ast-bind.frg" #rx"bind is not part of the language") -; (list "froglet-ast-intersect.frg" #rx"& operator is not") -; (list "froglet-ast-minus.frg" #rx"- operator is not") -; (list "froglet-ast-plus.frg" #rx"\\+ operator is not") -; (list "froglet-ast-star.frg" #rx"\\* operator is not") -; (list "froglet-ast-transitive-closure.frg" #rx"\\^ operator is not") -; (list "froglet-ast-transpose.frg" #rx"~ operator is not") -; (list "froglet-ast-notimplies.frg" #rx"parsing error") -; (list "froglet-arrow.frg" #rx"-> operator is not") -; (list "froglet-compareop0.frg" #rx"inputs to = must have similar type") -; (list "froglet-compareop1.frg" #rx"inputs to = must have similar type") -; (list "froglet-compareop2.frg" #rx"expected an Int") -; (list "froglet-compareop3.frg" #rx"expected an Int") -; (list "froglet-http.frg" #rx"field declaration") -; (list "froglet-int-minus.frg" #rx"- operator is not") + +; TODO: shadowing error is being pre-empted by bad join error ; (list "froglet-field-shadow.frg" #rx"expected a field") -; (list "froglet-is-linear0.frg" #rx"outside of bounds block") -; (list "froglet-is-linear1.frg" #rx"expected a field") -; (list "froglet-join-right.frg" #rx"not an object") -; (list "froglet-join-right2.frg" #rx"not an object") -; (list "froglet-join-right3.frg" #rx"not an object") -; (list "froglet-join-right4.frg" #rx"not an object") -; (list "froglet-join-right5.frg" #rx"not an object") ;;(#rx"Expected a singleton sig") ;; TODO is not a Node -; (list "froglet-join-right6.frg" #rx"not an object") -; (list "froglet-join.frg" #rx"not an object") -; (list "froglet-join2.frg" #rx"not a singleton") ;; TODO incomplete or partial? -; (list "froglet-join3.frg" #rx"not an object") -; (list "froglet-no-field.frg" #rx"expected an object") -; (list "froglet-pred.frg" #rx"expected a formula") + +; TODO: this error is bad (? because the join is within the reachable?) ; (list "froglet-reachable1.frg" #rx"no field match") -; (list "froglet-reachable2.frg" #rx"expected an object") -; (list "froglet-reachable3.frg" #rx"parsing error") -; (list "froglet-reachable4.frg" #rx"reachable expects 2 or more arguments") -; (list "froglet-reachable5.frg" #rx"reachable found no path to target") -; (list "froglet-reachable6.frg" #rx"reachable cannot use field") -; (list "froglet-set-singleton-equal.frg" #rx"not a singleton") ;;(#rx"= expects two objects, sig Node is not an object") -; (list "froglet-set.frg" #rx"not a singleton") #;( "pred must return an object, not a set") -; (list "froglet-uni-0.frg" #rx"expected an object") -; (list "froglet-uni-1.frg" #rx"expected an object") -; (list "froglet-uni-2.frg" #rx"expected an object") ;; or, a singleton -; (list "froglet-uni-3.frg" #rx"expected an object") -; (list "froglet-uni-4.frg" #rx"expected a field") -; (list "froglet-uni-5.frg" #rx"expected a field") -; (list "froglet-pubkey2.frg" #rx"field 'k' not found") - - ;; challenge - ;; - [X] pubkey2 froglet expected a field got k - ;; ... lookup works for `pairs`, not for `k`, - ;; should find the k parameter in the environment! - ;; - [X] expected a formula (why?!) given a name in k - ;; - [X] pubkey2: why unknown type for 1st branch - ;; - [ ] pubkey2 - ;; froglet: binop-check: (# '#s(type #) - ;; '#s((nametype type 1) #)) - ;; - [ ] pubkey2: refine branch type - ;; - [ ] pubkey2: is function type parsing broken? - ;; TODO catch all bsl errors from here - ;; TODO check Ed for bounds errors - ;; TODO modeling in anger ... invalid bounds - - ;; FYI forge has an evaluator, used to eval in inst specs, typechecker may need it too! (list "example_electrum.frg" #rx"example foo: .* temporal") (list "example_impossible.frg" #rx"Invalid example 'onlyBabies'") @@ -153,8 +134,9 @@ (list "failed_sat.frg" #rx"Failed test") (list "failed_unsat.frg" #rx"Failed test") (list "failed_sat.frg" #rx"Failed test") - ;;; ? after * makes the match lazy, meaning it will match as few characters as possible while still allowing the remainder of the regular expression to match. + ;;; ? after * makes the match lazy, meaning it will match as few characters as + ;;; possible while still allowing the remainder of the regular expression to match. (list "multiple_test_failures.frg" #rx".*?quantified_necessary_assertion_for_isNotRoot.*? failed.*?Invalid example 'thisIsNotATree'.*?Test t1 failed") (list "properties_undirected_tree_underconstraint_multiple_errors.frg" #rx".*?necessary_assertion_for_isUndirectedTree.*? failed.*?quantified_necessary_assertion_for_isUndirectedTree.*?failed") @@ -163,6 +145,7 @@ (list "consistency-error.frg" #rx"Failed test consistent_assertion_for_q_") (list "inconsistency-error.frg" #rx"Failed test inconsistent_assertion_for_q_") (list "properties_directed_tree_necessity_error.frg" #rx".*?quantified_necessary_assertion_for_isNotRoot.*?failed.") + ;;; And these tests ensure that you cannot have arbitrary expressions on the RHS of assertions (list "exp-on-rhs-assert.frg" #rx"parsing error") (list "exp-on-rhs-quantified-assert.frg" #rx"parsing error") diff --git a/forge/tests/error/mismatched-arg-type-arity.frg b/forge/tests/error/mismatched-arg-type-arity.frg index 30984f398..a5a18c758 100644 --- a/forge/tests/error/mismatched-arg-type-arity.frg +++ b/forge/tests/error/mismatched-arg-type-arity.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-basic-univ.frg b/forge/tests/error/mismatched-arg-type-basic-univ.frg index 8b49d42cd..adf84b40c 100644 --- a/forge/tests/error/mismatched-arg-type-basic-univ.frg +++ b/forge/tests/error/mismatched-arg-type-basic-univ.frg @@ -1,4 +1,5 @@ #lang forge +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-basic.frg b/forge/tests/error/mismatched-arg-type-basic.frg index 9009ff81e..cd745c4d6 100644 --- a/forge/tests/error/mismatched-arg-type-basic.frg +++ b/forge/tests/error/mismatched-arg-type-basic.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-fun-arity.frg b/forge/tests/error/mismatched-arg-type-fun-arity.frg index 72d8ef7a9..76e038153 100644 --- a/forge/tests/error/mismatched-arg-type-fun-arity.frg +++ b/forge/tests/error/mismatched-arg-type-fun-arity.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-fun-codomain-int.frg b/forge/tests/error/mismatched-arg-type-fun-codomain-int.frg index 48c5dff1f..1b47268de 100644 --- a/forge/tests/error/mismatched-arg-type-fun-codomain-int.frg +++ b/forge/tests/error/mismatched-arg-type-fun-codomain-int.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-fun-codomain-non-primsig.frg b/forge/tests/error/mismatched-arg-type-fun-codomain-non-primsig.frg index 50560204d..0c4550cfd 100644 --- a/forge/tests/error/mismatched-arg-type-fun-codomain-non-primsig.frg +++ b/forge/tests/error/mismatched-arg-type-fun-codomain-non-primsig.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } one sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-fun-codomain.frg b/forge/tests/error/mismatched-arg-type-fun-codomain.frg index 0186a3f17..7f761d00b 100644 --- a/forge/tests/error/mismatched-arg-type-fun-codomain.frg +++ b/forge/tests/error/mismatched-arg-type-fun-codomain.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-fun-output-int.frg b/forge/tests/error/mismatched-arg-type-fun-output-int.frg index 7d1ccad98..a9c309274 100644 --- a/forge/tests/error/mismatched-arg-type-fun-output-int.frg +++ b/forge/tests/error/mismatched-arg-type-fun-output-int.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-fun-output-non-primsig.frg b/forge/tests/error/mismatched-arg-type-fun-output-non-primsig.frg index d8a176317..cf6db12b3 100644 --- a/forge/tests/error/mismatched-arg-type-fun-output-non-primsig.frg +++ b/forge/tests/error/mismatched-arg-type-fun-output-non-primsig.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } one sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-fun-output.frg b/forge/tests/error/mismatched-arg-type-fun-output.frg index 2f35be6c6..49276761c 100644 --- a/forge/tests/error/mismatched-arg-type-fun-output.frg +++ b/forge/tests/error/mismatched-arg-type-fun-output.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-fun-univ-output.frg b/forge/tests/error/mismatched-arg-type-fun-univ-output.frg index 7c0501835..1303dd892 100644 --- a/forge/tests/error/mismatched-arg-type-fun-univ-output.frg +++ b/forge/tests/error/mismatched-arg-type-fun-univ-output.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { } diff --git a/forge/tests/error/mismatched-arg-type-fun.frg b/forge/tests/error/mismatched-arg-type-fun.frg index 9157d6206..7e7fbe7c4 100644 --- a/forge/tests/error/mismatched-arg-type-fun.frg +++ b/forge/tests/error/mismatched-arg-type-fun.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-int.frg b/forge/tests/error/mismatched-arg-type-int.frg index c36a0bd22..0a5a13b30 100644 --- a/forge/tests/error/mismatched-arg-type-int.frg +++ b/forge/tests/error/mismatched-arg-type-int.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-no-quant.frg b/forge/tests/error/mismatched-arg-type-no-quant.frg index 06425d7fb..45059d2fe 100644 --- a/forge/tests/error/mismatched-arg-type-no-quant.frg +++ b/forge/tests/error/mismatched-arg-type-no-quant.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-no-quant2.frg b/forge/tests/error/mismatched-arg-type-no-quant2.frg index 4c6d0caeb..d8aec6d53 100644 --- a/forge/tests/error/mismatched-arg-type-no-quant2.frg +++ b/forge/tests/error/mismatched-arg-type-no-quant2.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f1: lone B } sig B { f2: lone A } diff --git a/forge/tests/error/mismatched-arg-type-non-primsig.frg b/forge/tests/error/mismatched-arg-type-non-primsig.frg index f25bacf5a..c3871a120 100644 --- a/forge/tests/error/mismatched-arg-type-non-primsig.frg +++ b/forge/tests/error/mismatched-arg-type-non-primsig.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f2: lone B diff --git a/forge/tests/error/mismatched-arg-type-non-primsig2.frg b/forge/tests/error/mismatched-arg-type-non-primsig2.frg index c741fc6e9..c90c30d76 100644 --- a/forge/tests/error/mismatched-arg-type-non-primsig2.frg +++ b/forge/tests/error/mismatched-arg-type-non-primsig2.frg @@ -1,4 +1,5 @@ #lang forge/froglet +option verbose 0 sig A { f2: lone B diff --git a/forge/tests/error/priming-basic.frg b/forge/tests/error/priming-basic.frg index 9b4104e34..8abc6cd73 100644 --- a/forge/tests/error/priming-basic.frg +++ b/forge/tests/error/priming-basic.frg @@ -1,5 +1,5 @@ #lang forge/temporal - +option verbose 0 sig Person {} diff --git a/forge/tests/error/tree-type-error.frg b/forge/tests/error/tree-type-error.frg index 743d56d4a..d4ecd4db3 100644 --- a/forge/tests/error/tree-type-error.frg +++ b/forge/tests/error/tree-type-error.frg @@ -1,4 +1,5 @@ #lang forge +option verbose 0 sig A{ } sig A_child1 extends A { } diff --git a/forge/tests/error/unstated_bounds.frg b/forge/tests/error/unstated_bounds.frg index 1356b6dd1..f2129b913 100644 --- a/forge/tests/error/unstated_bounds.frg +++ b/forge/tests/error/unstated_bounds.frg @@ -1,4 +1,5 @@ #lang forge +option verbose 0 // Detect when sufficient bounds have not been provided. diff --git a/forge/tests/froglet/froglet-errors.frg b/forge/tests/froglet/froglet-errors.frg new file mode 100644 index 000000000..46c861ea3 --- /dev/null +++ b/forge/tests/froglet/froglet-errors.frg @@ -0,0 +1,52 @@ +#lang forge/froglet +option run_sterling off + +/* + This module combines a number of tests that were originally separate files. +*/ + +sig University {} +one sig BrownU extends University {} +sig Person { + father: lone Person, + mother: lone Person, + grad: lone University +} +one sig Tim extends Person {} + +sig Node {next: lone Node} + +pred helper[n1,n2: Node] { + n1 = n2 +} + +test expect { + uni0: {father.grad = mother.grad} is forge_error + uni1: {some father.grad} is forge_error + uni2some: {some father} is forge_error + uni2no: {no father} is forge_error + uni2one: {one father} is forge_error + uni2lone: {lone father} is forge_error + uni3: {some father.Tim} is forge_error + uni4: {some p: Person | reachable[p, father.Tim, father, mother]} is forge_error + uni5: {some Tim.Tim} is forge_error + + reach2: {all n: Node | reachable[next, n, next]} is forge_error "not a singleton" + + ///////////////////////////////////////////////////////////////////////////// + // We currently trust *Racket*'s arity errors when a model gives the wrong number + // of arguments to a helper predicate. + // These should not be caught by `is forge_error`; to avoid regressions, we're going to keep + // that satisfied only by actual raise-forge-error errors. Instead, see tests/error/main.rkt. + + // This one isn't ideal, because reachable actually requires _3_, but *Racket* checks for 2+ + // reach4: {all n: Node | reachable[n.next]} is forge_error "expected: at least 2" + // If only 2 are given, the reachable *procedure* will throw this error. + // reach2plus: {some n1, n2: Node | reachable[n1, n2]} is forge_error "reachable predicate expected at least three arguments" + // 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" + +} + + + diff --git a/forge/tests/froglet/froglet-in-checks.frg b/forge/tests/froglet/froglet-in-checks.frg new file mode 100644 index 000000000..217a8e8e1 --- /dev/null +++ b/forge/tests/froglet/froglet-in-checks.frg @@ -0,0 +1,72 @@ +#lang forge/froglet + +/* + Froglet allows the "in" operator to be used under very specific circumstances. + This suite is meant to check that this feature doesn't negatively impact things + like error messages, and to confirm that the desired functionality actually works. + + To test this, we need a fairly deep type hierarchy, so let's use a small subset of + the taxonomy. We'll (arbitrarily) say that animals can have best friends, and chordates + can eat cakes. +*/ + +sig Eukaryote {} +sig Animal extends Eukaryote { + bestFriend: lone Animal +} +sig Ctenophore extends Animal {} +sig Chordate extends Animal { + cakesEaten: one Int +} +sig Dog extends Chordate { + buddy: one Cat +} +sig Cat extends Chordate { + bff: one Dog +} +one sig Boatswain extends Dog {} + +option run_sterling off + +pred hasFriend[e: Eukaryote] { some e.bestFriend } +pred eatenCakes[e: Eukaryote] { some e.cakesEaten } +pred eatenCakesImpossible[c: Ctenophore] { some c.cakesEaten } + +/* This "narrowing" will not occur as of January 2025. */ +fun getBuddyOrBFF[c: Chordate]: lone Chordate { + (c in Dog => c.buddy else c in Cat => c.bff else none) +} + +test expect { + disallowRHS_unary_join: {some e: Eukaryote | e in cakesEaten.Int} + is forge_error "was not an object" + disallowLHS_non_singleton: { Animal in Eukaryote } is forge_error + disallowLHS_non_singleton_op: { Dog+Cat in Eukaryote } is forge_error + + allow_basic: {some e: Eukaryote | e in Animal} is sat + allow_pred1: {some e: Eukaryote | hasFriend[e]} is sat + allow_pred2: {some e: Eukaryote | eatenCakes[e]} is sat + error_pred: {some c: Ctenophore | eatenCakesImpossible[c]} + is forge_error "Sig Ctenophore does not have such a field" + + // Tests for non-existence of "narrowing" behavior (related, but not same as "in") + no_narrowing_needed: {some c: Chordate | some getBuddyOrBFF[c]} is sat + no_narrowing_option1: {some d: Dog | some getBuddyOrBFF[d]} + is forge_error "Sig Dog does not have such a field in \(d.bff\)" + no_narrowing_option2: {some c: Cat | some getBuddyOrBFF[c]} + is forge_error "Sig Cat does not have such a field in \(c.buddy\)" + + // Tests for unusual LHS terms + no_general_sig_lhs: {Dog in Chordate} is forge_error "invalid use of" + ok_one_sig_lhs: {Boatswain in Chordate} is sat + + // #{...} is allowed in Froglet, and we should allow proper "in" use inside and outside. + singleton_in_numeric: {#{a: Animal | a in Dog} in Int} is sat + // No Forge error expected here; for the moment we are allowing always-false "instanceof" + nonsingleton_in_numeric: {#{a: Animal | a in Dog} in Animal} is unsat + + + +} + + diff --git a/forge/tests/froglet/import_internal_identifiers.frg b/forge/tests/froglet/import_internal_identifiers.frg new file mode 100644 index 000000000..792931ff7 --- /dev/null +++ b/forge/tests/froglet/import_internal_identifiers.frg @@ -0,0 +1,10 @@ +#lang forge/froglet + +open "internal_identifiers.frg" +// Expect "option run_sterling off" to be imported with this. +assert {} is sat + +// Workaround (open needs to be at start, so to run this, move to top): +//open "internal_identifiers.frg" as internal +// option run_sterling off +// assert {some internalState} is sat diff --git a/forge/tests/froglet/internal_identifiers.frg b/forge/tests/froglet/internal_identifiers.frg new file mode 100644 index 000000000..d055ea011 --- /dev/null +++ b/forge/tests/froglet/internal_identifiers.frg @@ -0,0 +1,11 @@ +#lang forge/froglet + +/* + There are many identifiers bound by Forge internals. These should be + prefixed to avoid overlap in the namespace with sig names etc. that + users pick. +*/ + +option run_sterling off +one sig State {} +assert {} is sat \ No newline at end of file From cbcd2ed6d0d9a54148d7a40e1a2b05fdc20a2f4b Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Fri, 31 Jan 2025 15:28:41 -0500 Subject: [PATCH 2/5] widen exclusion of abac domain from auto-test --- forge/info.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/forge/info.rkt b/forge/info.rkt index d1df1ce7b..25de11fe5 100644 --- a/forge/info.rkt +++ b/forge/info.rkt @@ -69,6 +69,6 @@ #rx"tests/forge-core/*" #rx"tests/forge-functional/*" "tests/error/" - #rx"domains/abac/tests/*" + #rx"domains/abac/*" #rx"domains/crypto/examples/*" "OLD")) From 5c6675b7ef2f85ce39da6c7768c93cb4070dd959 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Sun, 9 Feb 2025 17:25:56 -0500 Subject: [PATCH 3/5] Feat 41 tests (#295) --- e2e/README.md | 5 ++ e2e/sat_pass_unsat_pass_2_runs.frg | 19 ++++++ .../examples/lights_puzzle/ring_of_lights.frg | 1 + forge/pardinus-cli/server/kks.rkt | 4 +- forge/pardinus-cli/server/pardinus-server.rkt | 11 +++- forge/send-to-solver.rkt | 4 +- forge/server/forgeserver.rkt | 62 ++++++++++--------- forge/server/serve-sterling-static.rkt | 2 +- forge/shared.rkt | 2 +- forge/sigs-structs.rkt | 20 ++++-- forge/sigs.rkt | 42 +++++++++---- forge/solver-specific/cvc5-server.rkt | 2 +- forge/utils/lazy-tree.rkt | 8 ++- 13 files changed, 126 insertions(+), 56 deletions(-) create mode 100644 e2e/README.md create mode 100644 e2e/sat_pass_unsat_pass_2_runs.frg diff --git a/e2e/README.md b/e2e/README.md new file mode 100644 index 000000000..62fb58cce --- /dev/null +++ b/e2e/README.md @@ -0,0 +1,5 @@ +# Forge models for end-to-end testing + +These models aren't meant to illustrate any particular concept, but rather are used for +end-to-end testing of the Sterling<->Forge<->Solver workflow. They may use unusual syntax, +unsafe features, etc. diff --git a/e2e/sat_pass_unsat_pass_2_runs.frg b/e2e/sat_pass_unsat_pass_2_runs.frg new file mode 100644 index 000000000..9e18e9def --- /dev/null +++ b/e2e/sat_pass_unsat_pass_2_runs.frg @@ -0,0 +1,19 @@ +#lang forge + +option no_overflow true // disallow integer overflow + +sig Pigeon {location: one Pigeonhole} +sig Pigeonhole {} + +pred some_roommates { + some disj p1, p2: Pigeon | p1.location = p2.location +} +test expect { + -- This is satisfiable, and so should appear in the run menu. + not_vacuous: {#Pigeon > #Pigeonhole} is sat + -- This is unsatisfiable, and so wouldn't be useful to visualize. + should_be_unsat: {Pigeon != Pigeon} is unsat +} + +see_principle_1: run {} for exactly 5 Pigeon, exactly 4 Pigeonhole +see_principle_2: run {} for exactly 4 Pigeon, exactly 3 Pigeonhole diff --git a/forge/examples/lights_puzzle/ring_of_lights.frg b/forge/examples/lights_puzzle/ring_of_lights.frg index 19bd540c1..1f614cc3e 100644 --- a/forge/examples/lights_puzzle/ring_of_lights.frg +++ b/forge/examples/lights_puzzle/ring_of_lights.frg @@ -2,6 +2,7 @@ option run_sterling "lights.js" + /* When using the custom vis script, remember to click "Run" after asking for a new trace or config! (the script doesn't re-run automatically) diff --git a/forge/pardinus-cli/server/kks.rkt b/forge/pardinus-cli/server/kks.rkt index a2633d2dc..1c1ebfe50 100755 --- a/forge/pardinus-cli/server/kks.rkt +++ b/forge/pardinus-cli/server/kks.rkt @@ -19,12 +19,12 @@ (define server-name "Pardinus") (provide start-server) ; stdin stdout) -(define (start-server [solver-type 'stepper] [solver-subtype 'default]) +(define (start-server [solver-type 'stepper] [solver-subtype 'default] [java-exe #f]) (when (>= (get-verbosity) VERBOSITY_HIGH) (printf "Starting ~a server.~n" server-name)) (define kks (new server% [name server-name] - [initializer (thunk (pardinus-initializer solver-type solver-subtype))])) + [initializer (thunk (pardinus-initializer solver-type solver-subtype java-exe))])) (send kks initialize) (define stdin-val (send kks stdin)) (define stderr-val (send kks stderr)) diff --git a/forge/pardinus-cli/server/pardinus-server.rkt b/forge/pardinus-cli/server/pardinus-server.rkt index 09c4d5f2b..957f8d1ee 100755 --- a/forge/pardinus-cli/server/pardinus-server.rkt +++ b/forge/pardinus-cli/server/pardinus-server.rkt @@ -10,7 +10,7 @@ (define-runtime-path pardinus (build-path "..")) -(define (pardinus-initializer solver-type solver-subtype) +(define (pardinus-initializer solver-type solver-subtype java-exe) (unless (member solver-type '(incremental stepper)) (raise (format "Invalid solver type: ~a" solver-type))) @@ -19,7 +19,9 @@ (filter (curry regexp-match #rx".+\\.jar") (directory-list pardinus/jar)))] [windows? (equal? (system-type) 'windows)] - [java (find-executable-path (if windows? "java.exe" "java"))] + [java (if (and java-exe (> (string-length java-exe) 0)) + (build-path java-exe) + (find-executable-path (if windows? "java.exe" "java")))] [path-separator (if windows? ";" ":")] [cp (foldl string-append "" (add-between (map path->string jars) path-separator))] ;[lib (path->string (build-path pardinus/jni (case (system-type) @@ -27,7 +29,7 @@ ;[(unix) "linux_x86_64"] ;[(windows) "win_x86_64"])))] ;[-Djava.library.path (string-append "-Djava.library.path=" lib)] - [error-out (build-path (find-system-path 'home-dir) "error-output.txt")]) + [error-out (build-path (find-system-path 'home-dir) "forge-pardinus-error-output.txt")]) (when (> (get-verbosity) VERBOSITY_LOW) (printf " Starting solver process. subtype: ~a~n" solver-subtype)) @@ -37,6 +39,9 @@ [(equal? solver-subtype 'temporal) "-temporal"] [(equal? solver-subtype 'default) ""] [else (error (format "Bad solver subtype: ~a" solver-subtype))])) + + (unless (file-exists? java) + (raise-user-error 'start-server "Could not find a Java executable. Given or inferred location was: ~a. Type was: ~a" java (file-or-directory-type java))) (when (>= (get-verbosity) VERBOSITY_HIGH) (printf " Subprocess invocation information: ~a~n" diff --git a/forge/send-to-solver.rkt b/forge/send-to-solver.rkt index 219c15b69..528bf8e8f 100644 --- a/forge/send-to-solver.rkt +++ b/forge/send-to-solver.rkt @@ -190,7 +190,9 @@ 'stepper ; always a stepper problem (there is a "next" button) ; 'default, 'temporal, or 'target (tells Pardinus which solver to load, ; and affects parsing so needs to be known at invocation time) - (get-option run-spec 'problem_type))] + (get-option run-spec 'problem_type) + ; control version of java used (by path string) + (get-option run-spec 'java_exe_location))] [else (raise (format "Invalid backend: ~a" backend))])) diff --git a/forge/server/forgeserver.rkt b/forge/server/forgeserver.rkt index d097f603b..8682dc69f 100644 --- a/forge/server/forgeserver.rkt +++ b/forge/server/forgeserver.rkt @@ -71,7 +71,9 @@ (define returned-instance (tree:get-value current-tree)) (set-box! (Run-last-sterling-instance the-run) returned-instance) returned-instance) - (define (get-next-instance [next-mode 'P]) + (define (get-next-instance [next-mode 'P]) + (when (@>= (get-verbosity) VERBOSITY_LOW) + (printf "Solving for next instance.~n")) (set! current-tree (tree:get-child current-tree next-mode)) (set! curr-datum-id (+ curr-datum-id 1)) ; get-current-instance updates the Run's last sterling instance cursor when called @@ -190,26 +192,12 @@ #:port (get-option the-run 'sterling_port) #:confirmation-channel chan)) (define port (async-channel-get chan)) - (cond [(string? port) - (displayln "NO PORTS AVAILABLE. Unable to start web server and Sterling visualizer.")] - [(equal? 'off (get-option the-run 'run_sterling)) - (void)] - [else - ; Attempt to open a browser to the Sterling index.html, with the proper port - ; If this cannot be opened for whatever reason, keep the server open but print - ; a warning, allowing the user a workaround. - (with-handlers ([exn? - (lambda (e) (printf "Racket could not open a browser on your system; you may be able manually navigate to this address, which is where Forge expects Sterling to load:~n ~a~n" - (string-append (path->string sterling-path) "?" (number->string port))))]) - (send-url/file sterling-path #f #:query (number->string port))) - - (printf "Sterling running. Hit enter to stop service.\n") - (when (> (get-verbosity) VERBOSITY_LOW) - (printf "Using port: ~a~n" (number->string port))) - (flush-output) - (void (read-char)) - ; Once a character is read, stop the server - (stop-service)])) + (when (string? port) + (printf "NO PORTS AVAILABLE. Could not start provider server.~n")) + + ; Now, serve the static sterling website files (this will be a different server/port). + (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]) (jsexpr->string @@ -249,7 +237,7 @@ 'payload (hash 'id (->string id) 'result (->string result))))) -(define/contract (make-sterling-meta defined-run-names) +(define/contract (make-sterling-meta included-run-names) (-> (listof symbol?) string?) (jsexpr->string (hash 'type "meta" @@ -257,7 +245,7 @@ 'payload (hash 'name "Forge" 'evaluator #t 'views (list "graph" "table" "script") - 'generators (map ->string defined-run-names))))) + 'generators (map ->string included-run-names))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Infrastructure for starting up sterling in "command selector" mode @@ -268,6 +256,17 @@ (define runmap (State-runmap curr-state)) (define defined-run-names (hash-keys runmap)) + ; Filter out runs that are not useful to visualize, like tests that failed due to unsat. + ; ASSUME: non-tests (e.g., `run`) won't have been invoked yet. + ; It is *VITAL* that `or` short-circuits, since Sat? will invoke the solver if needed. + (define useful-run-names (filter + (lambda (rn) + (define this-run (hash-ref runmap rn)) + ; Include if this run hasn't been solved yet, or if it's solved and sat. + (or (not (tree:is-evaluated? (Run-result this-run))) + (is-sat? this-run))) + defined-run-names)) + ; Assumption: if Sterling is the source of instance requests, there will be no ; instance requests seen from any other sources. @@ -278,7 +277,7 @@ (when (> (get-verbosity) VERBOSITY_LOW) (printf "Starting Sterling in command-selection mode...~n") - (printf "Available commands: ~a~n" defined-run-names)) + (printf "Available commands: ~a~n" useful-run-names)) (define (send-to-sterling m #:connection connection) (when (@>= (get-verbosity) VERBOSITY_STERLING) @@ -356,6 +355,9 @@ ; Get the next instance of this run's lazy result tree. Advance the tree pointer. (define (get-next-instance [next-mode 'P]) + (when (@>= (get-verbosity) VERBOSITY_LOW) + (printf "Solving for next instance.~n")) + (define next-tree (get-next-tree next-mode)) (set! curr-datum-id (+ curr-datum-id 1)) @@ -421,7 +423,8 @@ ;;(define xml (get-xml inst)) ;;(define response (make-sterling-data xml id name temporal?)) ;;(send-to-sterling response #:connection connection) - (printf "Ignoring Sterling 'data' request...~n") + (when (@>= (get-verbosity) VERBOSITY_STERLING) + (printf "Ignoring Sterling 'data' request...~n")) ] [(equal? (hash-ref json-m 'type) "eval") ; A message requesting that the provider evaluate some expression @@ -475,7 +478,7 @@ [(equal? (hash-ref json-m 'type) "meta") ; A message requesting data about the data provider, such as the provider's ; name and the types of views it supports. Respond in turn with a meta message. - (send-to-sterling (make-sterling-meta defined-run-names) #:connection connection)] + (send-to-sterling (make-sterling-meta useful-run-names) #:connection connection)] [else (send-to-sterling "BAD REQUEST" #:connection connection) (raise-forge-error @@ -508,5 +511,8 @@ (printf "NO PORTS AVAILABLE. Could not start provider server.~n")) ; Now, serve the static sterling website files (this will be a different server/port). - (unless (equal? 'off (get-option curr-state 'run_sterling)) - (serve-sterling-static #:provider-port port))) \ No newline at end of file + (unless (or (equal? 'off (get-option curr-state 'run_sterling)) + (empty? useful-run-names)) + (serve-sterling-static #:provider-port port)) + (when (empty? useful-run-names) + (printf "There was nothing useful to visualize: all commads were already executed and produced no instances.~n"))) \ No newline at end of file diff --git a/forge/server/serve-sterling-static.rkt b/forge/server/serve-sterling-static.rkt index 1756c184f..891d886fe 100644 --- a/forge/server/serve-sterling-static.rkt +++ b/forge/server/serve-sterling-static.rkt @@ -57,7 +57,7 @@ e))]) (send-url sterling-url)) - (printf "Opening Forge menu in Sterling (static server port=~a). Press enter to stop Forge.~n" port) + (printf "Opening Forge menu in Sterling (static server port=~a). Press enter to stop Forge (or click 'Stop' in VSCode).~n" port) (flush-output) ; On Windows, this blocks all Racket threads, which delays output until input is read. diff --git a/forge/shared.rkt b/forge/shared.rkt index e6e2ddcd5..aea305749 100644 --- a/forge/shared.rkt +++ b/forge/shared.rkt @@ -149,7 +149,7 @@ (set-box! success? (apply system* exe cmd*)))))) (if (unbox success?) str - (raise-user-error 'shell "failed to apply '~a' to arguments '~a'" exe cmd*))) + (raise-user-error 'shell "failed to apply '~a' to arguments '~a': got ~a" exe cmd* (unbox success?)))) ;; --- timing diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt index e0d5ab6a8..e0c7318ce 100644 --- a/forge/sigs-structs.rkt +++ b/forge/sigs-structs.rkt @@ -169,6 +169,7 @@ ; -- DEFAULT_OPTIONS ; -- symbol->proc ; -- option-types +; -- option-types-names ; -- state-set-option (in sigs.rkt) (struct/contract Options ( [eval-language symbol?] @@ -189,6 +190,7 @@ [engine_verbosity nonnegative-integer?] [test_keep symbol?] [no_overflow symbol?] + [java_exe_location (or/c false/c string?)] ) #:transparent) (struct/contract State ( @@ -229,14 +231,17 @@ [name symbol?] [command syntax?] [run-spec Run-spec?] - ; This is the *start* of the exploration tree + ; This is the *start* of the exploration tree. [result tree:node?] [server-ports Server-ports?] [atoms (listof (or/c symbol? number?))] [kodkod-currents Kodkod-current?] [kodkod-bounds (listof any/c)] ; This is Sterling's current cursor into the exploration tree. - ; It is mutated whenever Sterling asks for a new instance. + ; It is mutated whenever Sterling asks for a new instance. We keep this + ; separately, since there may be multiple cursors into the lazy tree if + ; the run is also being processed in a script, but the programmatic cursor + ; and the Sterling cursor should not interfere. [last-sterling-instance (box/c (or/c Sat? Unsat? Unknown? false/c))] ) #:transparent) @@ -249,7 +254,7 @@ ; an engine_verbosity of 1 logs SEVERE level in the Java engine; ; this will send back info about crashes, but shouldn't spam (and possibly overfill) stderr. (define DEFAULT-OPTIONS (Options 'surface 'SAT4J 'pardinus 20 0 0 1 5 'default - 'close-noretarget 'fast 0 'off 'on 0 1 'first 'false)) + 'close-noretarget 'fast 0 'off 'on 0 1 'first 'false #f)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;; Constants ;;;;;;; @@ -282,7 +287,8 @@ 'sterling_port Options-sterling_port 'engine_verbosity Options-engine_verbosity 'test_keep Options-test_keep - 'no_overflow Options-no_overflow)) + 'no_overflow Options-no_overflow + 'java_exe_location Options-java_exe_location)) (define (oneof-pred lst) (lambda (x) (member x lst))) @@ -306,7 +312,8 @@ 'sterling_port exact-nonnegative-integer? 'engine_verbosity exact-nonnegative-integer? 'test_keep (oneof-pred '(first last)) - 'no_overflow (oneof-pred '(false true)))) + 'no_overflow (oneof-pred '(false true)) + 'java_exe_location (lambda (x) (or (equal? x #f) (string? x))))) (define option-types-names (hash 'eval-language "symbol" @@ -326,7 +333,8 @@ 'sterling_port "non-negative integer" 'engine_verbosity "non-negative integer" 'test_keep "one of: first or last" - 'no_overflow "one of: false or true")) + 'no_overflow "one of: false or true" + 'java_exe_location "string")) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/forge/sigs.rkt b/forge/sigs.rkt index eaeca3c4f..cc8a5f605 100644 --- a/forge/sigs.rkt +++ b/forge/sigs.rkt @@ -276,7 +276,11 @@ [test_keep value])] [(equal? option 'no_overflow) (struct-copy Options options - [no_overflow value])])) + [no_overflow value])] + [(equal? option 'java_exe_location) + (struct-copy Options options + [java_exe_location value])] + )) (struct-copy State state [options new-options])) @@ -642,6 +646,10 @@ ; Primary testing form: check whether a constraint-set, under ; some provided bounds, is sat, unsat, or an error. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(define (report-passing-test #:name name) + (when (>= (get-verbosity) VERBOSITY_LOW) + (printf " Test passed: ~a~n" name))) + (define-syntax (test stx) (syntax-case stx () [(test name args ... #:expect expected) @@ -688,7 +696,8 @@ #:run run-reference #:sterling #f)) (when (member 'name (hash-keys (State-runmap curr-state))) - (printf "Warning: successful `is forge_error` test run left in state environment: ~a.~n" 'name))] + (printf "Warning: successful `is forge_error` test run left in state environment: ~a.~n" 'name)) + (report-passing-test #:name 'name)] ; It may not be immediately obvious why we would ever test for unknown, ; but it seems reasonable to support it in the engine, regardless. @@ -711,7 +720,8 @@ #:context loc #:instance first-instance #:run name) - (close-run name))] + (begin (report-passing-test #:name 'name) + (close-run name)))] [(equal? 'expected 'checked) ;#,(syntax/loc stx (check name args ...)) @@ -731,8 +741,9 @@ #:context loc #:instance first-instance #:run name)] - [else - (close-run name)])] + [else + (begin (report-passing-test #:name 'name) + (close-run name))])] [(equal? 'expected 'theorem) (raise-forge-error #:msg "The syntax 'is theorem' is deprecated and will be re-enabled in a future version for complete solver backends only; use 'is checked' instead." @@ -1138,11 +1149,18 @@ [else ; Raise a Forge error and stop execution; show Sterling if enabled. (when (>= (get-verbosity) 1) - (printf "Test ~a failed. Stopping execution.~n" name)) - (when (and (Run? run-or-state) sterling) - (true-display run-or-state)) - ;; !!!!! ^^^^ This is a problem! Because the error is raised only after Sterling terminates. - ;; (and this is a single thread only) + (printf "******************** TEST FAILED *******************~nTest ~a failed. Stopping execution.~n" name)) + (cond [(and (Run? run-or-state) sterling (Sat? instance)) + (when (>= (get-verbosity) 1) + (printf "Test failed due to finding a counterexample, which will be displayed in Sterling.~n") + (printf "*****************************************************~n")) + (true-display run-or-state)] + [else + (when (>= (get-verbosity) 1) + (printf "Test failed due to unsat/inconsistency. No counterexample to display.~n") + (printf "*****************************************************~n"))]) + + ;; The error below is raised only after Sterling terminates, so messaging above is vital. (raise-forge-error #:msg msg #:context context)])) ; To be run at the very end of the Forge execution; reports test failures and opens @@ -1253,9 +1271,9 @@ ; Don't allow the Forge file to reset this option. (set-box! option-overrides (cons (string->symbol OPTION-NAME) (unbox option-overrides))))] [("-N" "--notests") - "Disable tests for this model execution" + "Disable tests for this model execution (NOT YET SUPPORTED)" (begin - (printf "Tests disabled.~n") + (printf "(NOT YET SUPPORTED) Tests disabled.~n") (set-box! disable-tests #t))] diff --git a/forge/solver-specific/cvc5-server.rkt b/forge/solver-specific/cvc5-server.rkt index e24f4943e..ca397f69c 100644 --- a/forge/solver-specific/cvc5-server.rkt +++ b/forge/solver-specific/cvc5-server.rkt @@ -23,7 +23,7 @@ ; assume that cvc5 is on the user's path. (let* ([windows? (equal? (system-type) 'windows)] [path-separator (if windows? ";" ":")] - [error-out (build-path (find-system-path 'home-dir) "error-output.txt")]) + [error-out (build-path (find-system-path 'home-dir) "forge-cvc5-error-output.txt")]) (when (> (get-verbosity) VERBOSITY_LOW) (printf " Starting solver process for ~a. subtype: ~a~n" server-name solver-subtype)) diff --git a/forge/utils/lazy-tree.rkt b/forge/utils/lazy-tree.rkt index 314829e3b..896df3d1e 100644 --- a/forge/utils/lazy-tree.rkt +++ b/forge/utils/lazy-tree.rkt @@ -4,7 +4,7 @@ (require syntax/parse/define) (require (only-in racket empty? match cons? first thunk)) -(provide node? make-node get-child get-children get-value lazy-tree-map) +(provide node? make-node get-child get-children get-value lazy-tree-map is-evaluated?) (struct computation ()) (struct computation/delayed computation (thnk)) @@ -18,6 +18,12 @@ (struct node ([datum #:mutable] child-generator children [ancestors #:mutable])) +; Has get-value been called on this node yet? +(define/contract (is-evaluated? a-node) + (node? . -> . any/c) + (match (node-datum a-node) + [(computation/evaluated value) #t] + [else #f])) (define/contract (root-node? node) (any/c . -> . boolean?) From bc9a09e9ce80429612b1011ba8937ceff08b9510 Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Sun, 9 Feb 2025 17:30:31 -0500 Subject: [PATCH 4/5] fix: remember passing-test message for examples, too --- forge/sigs.rkt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/forge/sigs.rkt b/forge/sigs.rkt index cc8a5f605..b517e8d24 100644 --- a/forge/sigs.rkt +++ b/forge/sigs.rkt @@ -795,7 +795,9 @@ #:context #,(build-source-location stx) #:instance first-instance #:run name)])] - [else (close-run name)])))))])) + [else + (report-passing-test #:name 'name) + (close-run name)])))))])) ; Checks that some predicates are always true. (define-syntax (check stx) From f1caa866099c843215d5ce7e4fdd99d874d9d94b Mon Sep 17 00:00:00 2001 From: Tim Nelson Date: Mon, 10 Feb 2025 06:39:03 -0500 Subject: [PATCH 5/5] add: 4 e2e examples --- e2e/fail_assertion.frg | 16 ++++++++++++++++ e2e/failing_decls_example.frg | 21 +++++++++++++++++++++ e2e/failing_example.frg | 19 +++++++++++++++++++ e2e/passing_example.frg | 18 ++++++++++++++++++ 4 files changed, 74 insertions(+) create mode 100644 e2e/fail_assertion.frg create mode 100644 e2e/failing_decls_example.frg create mode 100644 e2e/failing_example.frg create mode 100644 e2e/passing_example.frg diff --git a/e2e/fail_assertion.frg b/e2e/fail_assertion.frg new file mode 100644 index 000000000..4746a801e --- /dev/null +++ b/e2e/fail_assertion.frg @@ -0,0 +1,16 @@ +#lang forge + +option no_overflow true // disallow integer overflow + +sig Pigeon {location: one Pigeonhole} +sig Pigeonhole {} + +pred some_roommates { + some disj p1, p2: Pigeon | p1.location = p2.location +} +-- This should pass; we don't expect Sterling to open at all. +assert {#Pigeon > #Pigeonhole} is sufficient for some_roommates +-- This should fail; we expect Sterling to open with **only one command**, +-- and for the instance to auto-load. **The evaluator should be usable**. +assert {#Pigeon >= #Pigeonhole} is sufficient for some_roommates + diff --git a/e2e/failing_decls_example.frg b/e2e/failing_decls_example.frg new file mode 100644 index 000000000..b46455d34 --- /dev/null +++ b/e2e/failing_decls_example.frg @@ -0,0 +1,21 @@ +#lang forge + +option no_overflow true // disallow integer overflow + +sig Pigeon {location: one Pigeonhole} +sig Pigeonhole {} + +pred some_roommates { + some disj p1, p2: Pigeon | p1.location = p2.location +} + +// This fails because the instance given violates the type definitions +// The solver yields unsat, so Sterling should not open. +example threePigeons is {some_roommates} for { + Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2 + Pigeonhole = `Pigeonhole0 + `Pigeonhole1 + // This violates the type declarations: + location = `Pigeon0 -> (`Pigeonhole0 + `Pigeonhole1) + + `Pigeon1 -> `Pigeonhole0 + + `Pigeon2 -> `Pigeonhole0 +} diff --git a/e2e/failing_example.frg b/e2e/failing_example.frg new file mode 100644 index 000000000..15fa8c157 --- /dev/null +++ b/e2e/failing_example.frg @@ -0,0 +1,19 @@ +#lang forge + +option no_overflow true // disallow integer overflow + +sig Pigeon {location: one Pigeonhole} +sig Pigeonhole {} + +pred some_roommates { + some disj p1, p2: Pigeon | p1.location = p2.location +} + +// This fails. Since the solver has yielded unsat, Sterling shouldn't open. +example threePigeons is {not some_roommates} for { + Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2 + Pigeonhole = `Pigeonhole0 + `Pigeonhole1 + location = `Pigeon0 -> `Pigeonhole0 + + `Pigeon1 -> `Pigeonhole0 + + `Pigeon2 -> `Pigeonhole1 +} diff --git a/e2e/passing_example.frg b/e2e/passing_example.frg new file mode 100644 index 000000000..c8f1c3d04 --- /dev/null +++ b/e2e/passing_example.frg @@ -0,0 +1,18 @@ +#lang forge + +option no_overflow true // disallow integer overflow + +sig Pigeon {location: one Pigeonhole} +sig Pigeonhole {} + +pred some_roommates { + some disj p1, p2: Pigeon | p1.location = p2.location +} + +example threePigeons is some_roommates for { + Pigeon = `Pigeon0 + `Pigeon1 + `Pigeon2 + Pigeonhole = `Pigeonhole0 + `Pigeonhole1 + location = `Pigeon0 -> `Pigeonhole0 + + `Pigeon1 -> `Pigeonhole0 + + `Pigeon2 -> `Pigeonhole1 +}