From 318f28affd50e918de30e073d4c399ce55554c0c Mon Sep 17 00:00:00 2001 From: James Shubin Date: Tue, 29 Aug 2023 19:19:26 -0400 Subject: [PATCH] lang: unification, interfaces: Don't pass over generators We were skipping over being fully consistent with all of the generator invariants when running the solver. This allowed us to miss some of the conditions that a generator might impose. Usually this caused us to be "solved" when in fact we had an invalid program. --- lang/interfaces/unification.go | 5 ++ .../TestAstFunc2/printfempty.txtar | 10 ++++ .../TestAstFunc2/printfunificationerr0.txtar | 2 +- lang/unification/simplesolver.go | 59 ++++++++++++++++++- 4 files changed, 73 insertions(+), 3 deletions(-) create mode 100644 lang/interpret_test/TestAstFunc2/printfempty.txtar diff --git a/lang/interfaces/unification.go b/lang/interfaces/unification.go index 8bbcebb3..e7c0a23d 100644 --- a/lang/interfaces/unification.go +++ b/lang/interfaces/unification.go @@ -671,6 +671,11 @@ type GeneratorInvariant struct { // from the list. If we error, it's because we don't have any new // information to provide at this time... Func func(invariants []Invariant, solved map[Expr]*types.Type) ([]Invariant, error) + + // Inactive specifies that we tried to run this, but it didn't help us + // progress forwards. It can be reset if needed. It should only be set + // or read by the solver itself. + Inactive bool } // String returns a representation of this invariant. diff --git a/lang/interpret_test/TestAstFunc2/printfempty.txtar b/lang/interpret_test/TestAstFunc2/printfempty.txtar new file mode 100644 index 00000000..1b8b5f7d --- /dev/null +++ b/lang/interpret_test/TestAstFunc2/printfempty.txtar @@ -0,0 +1,10 @@ +-- main.mcl -- +import "fmt" + +# This should not unify, we need at least one arg. +# NOTE: We have historically needed to turn on the recursive solver to find that +# this was a bug! +test fmt.printf() {} + +-- OUTPUT -- +# err: errUnify: 2 unconsumed generators diff --git a/lang/interpret_test/TestAstFunc2/printfunificationerr0.txtar b/lang/interpret_test/TestAstFunc2/printfunificationerr0.txtar index 967055d8..a90c2b2a 100644 --- a/lang/interpret_test/TestAstFunc2/printfunificationerr0.txtar +++ b/lang/interpret_test/TestAstFunc2/printfunificationerr0.txtar @@ -2,4 +2,4 @@ import "fmt" test fmt.printf("%d%d", 42) {} # should not pass, missing second int -- OUTPUT -- -# err: errUnify: only recursive solutions left +# err: errUnify: 2 unconsumed generators diff --git a/lang/unification/simplesolver.go b/lang/unification/simplesolver.go index ad18c71b..6753bc4d 100644 --- a/lang/unification/simplesolver.go +++ b/lang/unification/simplesolver.go @@ -349,12 +349,39 @@ func SimpleInvariantSolver(invariants []interfaces.Invariant, expected []interfa } } + countGenerators := func() (int, int) { + active := 0 + total := 0 + for _, x := range equalities { + gen, ok := x.(*interfaces.GeneratorInvariant) + if !ok { + continue + } + total++ // total count + if gen.Inactive { + continue // skip inactive + } + active++ // active + } + return total, active + } + activeGenerators := func() int { + _, active := countGenerators() + return active + } + logf("%s: starting loop with %d equalities", Name, len(equalities)) // run until we're solved, stop consuming equalities, or type clash Loop: for { + // Once we're done solving everything else except the generators + // then we can exit, but we want to make sure the generators had + // a chance to "speak up" and make sure they were part of Unify. + // Every generator gets to run once, and if that does not change + // the result, then we mark it as inactive. + logf("%s: iterate...", Name) - if len(equalities) == 0 && len(exclusives) == 0 { + if len(equalities) == 0 && len(exclusives) == 0 && activeGenerators() == 0 { break // we're done, nothing left } used := []int{} @@ -988,6 +1015,13 @@ Loop: continue } + // skip if the inactive flag has been set, as it + // won't produce any new (novel) inequalities we + // can use to progress to a result at this time. + if eq.Inactive { + continue + } + // If this returns nil, we add the invariants // it returned and we remove it from the list. // If we error, it's because we don't have any @@ -995,6 +1029,8 @@ Loop: // XXX: should we pass in `invariants` instead? gi, err := eq.Func(equalities, solved) if err != nil { + // set the inactive flag of this generator + eq.Inactive = true continue } @@ -1008,6 +1044,15 @@ Loop: used = append(used, eqi) // mark equality as used up logf("%s: solved `generator` equality", Name) + // reset all other generator equality "inactive" flags + for _, x := range equalities { + gen, ok := x.(*interfaces.GeneratorInvariant) + if !ok { + continue + } + gen.Inactive = false + } + continue // wtf matching @@ -1033,7 +1078,7 @@ Loop: return nil, fmt.Errorf("unknown invariant type: %T", eqx) } } // end inner for loop - if len(used) == 0 { + if len(used) == 0 && activeGenerators() == 0 { // Looks like we're now ambiguous, but if we have any // exclusives, recurse into each possibility to see if // one of them can help solve this! first one wins. Add @@ -1066,6 +1111,16 @@ Loop: } } + total, active := countGenerators() + // we still have work to do for consistency + if active > 0 { + continue Loop + } + + if total > 0 { + return nil, fmt.Errorf("%d unconsumed generators", total) + } + // check for consistency against remaining invariants logf("%s: checking for consistency against %d exclusives...", Name, len(exclusives)) done := []int{}