diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 777db69..064e2aa 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -11,6 +11,7 @@ repos: rev: v1.0.0-rc.1 hooks: - id: go-test-mod + args: [ --run=Test_ ] - repo: https://github.com/golangci/golangci-lint rev: v1.57.1 hooks: diff --git a/pkg/table/constraints.go b/pkg/table/constraints.go index 89662cb..d8bcb9e 100644 --- a/pkg/table/constraints.go +++ b/pkg/table/constraints.go @@ -117,10 +117,13 @@ func (p *RowConstraint[T]) Accepts(tr Trace) error { func HoldsGlobally[T Testable](handle string, constraint T, tr Trace) error { // Determine well-definedness bounds for this constraint bounds := constraint.Bounds() - // Check all in-bounds values - for k := bounds.Start; k < (tr.Height() - bounds.End); k++ { - if err := HoldsLocally(int(k), handle, constraint, tr); err != nil { - return err + // Sanity check enough rows + if bounds.End < tr.Height() { + // Check all in-bounds values + for k := bounds.Start; k < (tr.Height() - bounds.End); k++ { + if err := HoldsLocally(int(k), handle, constraint, tr); err != nil { + return err + } } } // Success diff --git a/pkg/test/ir_test.go b/pkg/test/ir_test.go index 71cb8a7..eef73e0 100644 --- a/pkg/test/ir_test.go +++ b/pkg/test/ir_test.go @@ -137,6 +137,18 @@ func Test_Spillage_01(t *testing.T) { Check(t, "spillage_01") } +func Test_Spillage_02(t *testing.T) { + Check(t, "spillage_02") +} + +func Test_Spillage_03(t *testing.T) { + Check(t, "spillage_03") +} + +func Test_Spillage_04(t *testing.T) { + Check(t, "spillage_04") +} + // =================================================================== // Normalisation Tests // =================================================================== diff --git a/pkg/util/bounds.go b/pkg/util/bounds.go new file mode 100644 index 0000000..d8b19ff --- /dev/null +++ b/pkg/util/bounds.go @@ -0,0 +1,47 @@ +package util + +// EMPTY_BOUND is the bound which overlaps exactly with the original range. It +// represents the maximum possible bound. +var EMPTY_BOUND Bounds = Bounds{0, 0} + +// Bounds captures the subrange of rows for which a computation is well-defined. +type Bounds struct { + // Number of rows from first row where computation starts being defined. + Start uint + // Number of rows before last row where computation is no longer defined. + End uint +} + +// NewBounds constructs a new set of bounds. +func NewBounds(start uint, end uint) Bounds { + return Bounds{start, end} +} + +// Union merges one set of bounds into another. +func (p *Bounds) Union(q *Bounds) { + p.Start = max(p.Start, q.Start) + p.End = max(p.End, q.End) +} + +// Boundable captures computations which are well-defined only for a specific +// subrange of rows (the bounds). +type Boundable interface { + // Determine the well-definedness bounds for this expression for both the + // negative (left) or positive (right) directions. For example, consider an + // expression such as "(shift X -1)". This is technically undefined for the + // first row of any trace and, by association, any constraint evaluating + // this expression on that first row is also undefined (and hence must pass). + Bounds() Bounds +} + +// BoundsForArray determines the bounds for an array of expressions. +func BoundsForArray[E Boundable](args []E) Bounds { + bounds := Bounds{0, 0} + + for _, e := range args { + ith := e.Bounds() + bounds.Union(&ith) + } + // Done + return bounds +} diff --git a/testdata/spillage_02.accepts b/testdata/spillage_02.accepts new file mode 100644 index 0000000..c03607d --- /dev/null +++ b/testdata/spillage_02.accepts @@ -0,0 +1,10 @@ +{ "ST": [], "A": [] } +{ "ST": [1], "A": [0] } +{ "ST": [1,1], "A": [0,0] } +{ "ST": [1,1], "A": [0,1] } +{ "ST": [1,1], "A": [1,0] } +{ "ST": [1,1,1], "A": [0,0,0] } +{ "ST": [1,1,1], "A": [0,0,1] } +{ "ST": [1,1,1], "A": [0,1,0] } +{ "ST": [1,1,1], "A": [1,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1] } diff --git a/testdata/spillage_02.lisp b/testdata/spillage_02.lisp index 659f74b..1fcc586 100644 --- a/testdata/spillage_02.lisp +++ b/testdata/spillage_02.lisp @@ -1,2 +1,3 @@ +(column ST) (column A) -(vanish spills (~ (shift A 2))) +(vanish spills (* ST (* A (~ (shift A 2))))) diff --git a/testdata/spillage_02.rejects b/testdata/spillage_02.rejects new file mode 100644 index 0000000..9efe7e5 --- /dev/null +++ b/testdata/spillage_02.rejects @@ -0,0 +1,5 @@ +{ "ST": [1,1,1], "A": [1,0,1] } +{ "ST": [1,1,1], "A": [1,1,1] } +{ "ST": [1,1,1], "A": [1,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,1] } diff --git a/testdata/spillage_03.accepts b/testdata/spillage_03.accepts new file mode 100644 index 0000000..d647246 --- /dev/null +++ b/testdata/spillage_03.accepts @@ -0,0 +1,15 @@ +{ "ST": [], "A": [] } +{ "ST": [1], "A": [0] } +{ "ST": [1,1], "A": [0,0] } +{ "ST": [1,1], "A": [0,1] } +{ "ST": [1,1], "A": [1,0] } +{ "ST": [1,1,1], "A": [0,0,0] } +{ "ST": [1,1,1], "A": [0,0,1] } +{ "ST": [1,1,1], "A": [0,1,0] } +{ "ST": [1,1,1], "A": [1,0,0] } +{ "ST": [1,1,1], "A": [1,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [1,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,1] } +{ "ST": [1,1,1,1,1], "A": [1,0,1,0,1] } diff --git a/testdata/spillage_03.lisp b/testdata/spillage_03.lisp index 1c421a2..9004671 100644 --- a/testdata/spillage_03.lisp +++ b/testdata/spillage_03.lisp @@ -1,2 +1,3 @@ +(column ST) (column A) -(vanish spills (~ (shift A 3))) +(vanish spills (* ST A (~ (shift A 3)))) diff --git a/testdata/spillage_03.rejects b/testdata/spillage_03.rejects new file mode 100644 index 0000000..069db67 --- /dev/null +++ b/testdata/spillage_03.rejects @@ -0,0 +1,7 @@ +{ "ST": [1,1,1,1], "A": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,1,1] } +{ "ST": [1,1,0,1], "A": [1,0,0,1] } +{ "ST": [1,0,1,1], "A": [1,0,0,1] } +{ "ST": [1,0,0,1], "A": [1,0,0,1] } diff --git a/testdata/spillage_04.accepts b/testdata/spillage_04.accepts new file mode 100644 index 0000000..ebca25a --- /dev/null +++ b/testdata/spillage_04.accepts @@ -0,0 +1,144 @@ +{ "ST": [], "A": [], "B": [] } +{ "ST": [1], "A": [1], "B": [1] } +{ "ST": [1], "A": [0], "B": [1] } +{ "ST": [1], "A": [1], "B": [0] } +{ "ST": [1], "A": [0], "B": [0] } +;; +{ "ST": [1,1], "A": [0,0], "B": [0,0] } +{ "ST": [1,1], "A": [0,1], "B": [0,0] } +{ "ST": [1,1], "A": [1,0], "B": [0,0] } +{ "ST": [1,1], "A": [1,1], "B": [0,0] } +{ "ST": [1,1], "A": [0,0], "B": [1,0] } +{ "ST": [1,1], "A": [0,1], "B": [1,0] } +{ "ST": [1,1], "A": [1,0], "B": [1,0] } +{ "ST": [1,1], "A": [1,1], "B": [1,0] } +{ "ST": [1,1], "A": [0,0], "B": [0,1] } +{ "ST": [1,1], "A": [0,1], "B": [0,1] } +{ "ST": [1,1], "A": [1,0], "B": [0,1] } +{ "ST": [1,1], "A": [1,1], "B": [0,1] } +;; +{ "ST": [1,1,1], "A": [0,0,0], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [1,0,0], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [0,1,0], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [0,0,1], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [1,1,0], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [0,1,1], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [1,1,1], "B": [0,0,0] } +{ "ST": [1,1,1], "A": [0,0,0], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [1,0,0], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [0,1,0], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [0,0,1], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [1,1,0], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [0,1,1], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [1,1,1], "B": [1,0,0] } +{ "ST": [1,1,1], "A": [0,0,0], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [1,0,0], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [0,1,0], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [0,0,1], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [1,1,0], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [0,1,1], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [1,1,1], "B": [0,1,0] } +{ "ST": [1,1,1], "A": [0,0,0], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [1,0,0], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [0,1,0], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [0,0,1], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [1,1,0], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [0,1,1], "B": [0,0,1] } +{ "ST": [1,1,1], "A": [1,1,1], "B": [0,0,1] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,0,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,0,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,0,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,0,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,0,1,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,0,1] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,1,0,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,1,0,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,0,1,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [1,0,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,0,1] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,1,1,0] } +;; +{ "ST": [1,1,1,1], "A": [0,0,0,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,0,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,0,1], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [0,1,1,0], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [0,0,1,1], "B": [0,1,0,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,0,1] } diff --git a/testdata/spillage_04.lisp b/testdata/spillage_04.lisp index 5aa6837..a16fbb8 100644 --- a/testdata/spillage_04.lisp +++ b/testdata/spillage_04.lisp @@ -1,3 +1,4 @@ +(column ST) (column A) (column B) -(vanish spills (~ (* (shift A 3) (shift B 2)))) +(vanish spills (* ST A (~ (* (shift A 3) (shift B 2))))) diff --git a/testdata/spillage_04.rejects b/testdata/spillage_04.rejects new file mode 100644 index 0000000..0babfaa --- /dev/null +++ b/testdata/spillage_04.rejects @@ -0,0 +1,31 @@ +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [0,1,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,0,1], "B": [1,1,1,1] } +;; +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [1,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [0,1,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,0,1], "B": [1,1,1,1] } +;; +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [1,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [0,1,1,1] } +{ "ST": [1,1,1,1], "A": [1,0,1,1], "B": [1,1,1,1] } +;; +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [1,0,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,1,1,0] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [1,0,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [0,1,1,1] } +{ "ST": [1,1,1,1], "A": [1,1,1,1], "B": [1,1,1,1] } diff --git a/testdata/spillage_05.lisp b/testdata/spillage_05.lisp deleted file mode 100644 index 4de8730..0000000 --- a/testdata/spillage_05.lisp +++ /dev/null @@ -1,3 +0,0 @@ -(column A) -(column B) -(vanish spills (~ (* (shift A 2) (shift B 3))))