From 06d0b56996873fe2f8f7e96e95f9fd2357af2823 Mon Sep 17 00:00:00 2001
From: Artem Pelenitsyn <a.pelenitsyn@gmail.com>
Date: Fri, 8 Sep 2023 10:38:06 -0400
Subject: [PATCH] fix fuel more; fix parameters setting at types DB creation

---
 src/enumeration.jl | 48 +++++++++++++++++++++++++++++++++-------------
 src/types.jl       | 10 ++++++----
 src/utils.jl       |  1 +
 test/runtests.jl   | 11 ++++++-----
 4 files changed, 48 insertions(+), 22 deletions(-)

diff --git a/src/enumeration.jl b/src/enumeration.jl
index beb0ee29f..c7ca9d032 100644
--- a/src/enumeration.jl
+++ b/src/enumeration.jl
@@ -49,7 +49,18 @@ all_subtypes(ts::Vector, scfg :: SearchCfg, result :: Channel) = begin
         isconc = all(is_concrete_type, tv)
         if isconc
             @debug "[ all_subtypes ] concrete"
-            put!(result, tv)
+
+            # Manage fuel w.r.t. reaching concrete types
+            global stepCount
+            stepCount += 1
+            @debug "[ all_subtypes ]" stepCount scfg.fuel
+            if stepCount > scfg.fuel
+                put!(result, OutOfFuel())
+                scfg.failfast &&
+                    break
+            else
+                put!(result, tv)
+            end
         # otherwise, get some subtypes, add to worklist, loop
         else
             @debug "[ all_subtypes ] abstract"
@@ -122,22 +133,33 @@ end
 direct_subtypes1(t::Any, scfg :: SearchCfg) = begin
     @debug "direct_subtypes1: $t"
 
-    # it is hear where we decided to manage fuel
+    # It is here where we decided to manage fuel w.r.t. traversing lattice.
+    # There's another point, which has to do with reaching concrete types,
+    # inside all_subtypes
     global stepCount
     stepCount += 1
+    @debug "direct_subtypes1" stepCount scfg.fuel
     stepCount > scfg.fuel && return nothing
 
-    if t isa UnionAll
-        ss_first = subtype_unionall(t, scfg)
-    elseif t isa Union
-        ss_first = subtype_union(t)
-    elseif is_concrete_type(t)
-        [t]
-    elseif t == Any # if Any got here, we're asked to sample
-        scfg.typesDBcfg.types_db
-    else
-        subtypes(t)
-    end
+    ss = subtypes(t)
+
+    res =
+        # NOTE: the order of if-branches is important
+        if t == Any         # if Any got here, we're asked to sample
+            scfg.typesDBcfg.types_db
+        elseif !isempty(ss) # we try to crawl nominal hierarchy all the way first
+            ss
+        elseif t isa UnionAll
+            subtype_unionall(t, scfg)
+        elseif t isa Union
+            subtype_union(t)
+        elseif is_concrete_type(t)
+            [t]
+        else
+            @assert false "direct_subtypes1: can't subtype $t (should not happen)"
+        end
+    # @info "" res
+    return res
 end
 
 #
diff --git a/src/types.jl b/src/types.jl
index c76004ae6..b6d4faf3e 100644
--- a/src/types.jl
+++ b/src/types.jl
@@ -117,7 +117,7 @@ Base.@kwdef struct SearchCfg
     failfast :: Bool = true
 #   ^--- exit when find the first counterexample
 
-    fuel :: Int = 100 #typemax(Int)
+    fuel :: Int = 1000 #typemax(Int)
 #   ^--- search fuel, i.e. how many types we want to enumerate before give up
 
     typesDBcfg :: TypesDBCfg = TypesDBCfg()
@@ -132,10 +132,12 @@ default_scfg = SearchCfg()
 fast_scfg = SearchCfg(fuel=30)
 
 build_typesdb_scfg(inFile = intypesCsvFileDefault; sample_count :: Int = 100000) = begin
+    tdbFull = typesDB(inFile)
+    sampleCountActual = min(length(tdbFull),sample_count)
+    tdb = tdbFull[1:sampleCountActual]
     scfg = @set default_scfg.typesDBcfg.use_types_db = true
-    scfg = @set scfg.typesDBcfg.types_db            = typesDB(inFile)[1:min(end,sample_count)]
-    scfg = @set scfg.typesDBcfg.sample_count        = sample_count
-    scfg = @set scfg.fuel                           = length(scfg.typesDBcfg.types_db)
+    scfg = @set scfg.typesDBcfg.types_db            = tdb
+    scfg = @set scfg.typesDBcfg.sample_count        = length(tdb)
     scfg
 end
 
diff --git a/src/utils.jl b/src/utils.jl
index 0f3ceed5a..1a2ca6138 100644
--- a/src/utils.jl
+++ b/src/utils.jl
@@ -41,6 +41,7 @@ is_stable_call(@nospecialize(f :: Function), @nospecialize(ts :: Vector)) = begi
     end
     (_ #=code=#, res_type) = ct[1] # we ought to have just one method body, I think
     res = is_concrete_type(res_type)
+    # @info "[ is_stable_call ]" res_type
     #print_stable_check(f,ts,res_type,res)
     res
 end
diff --git a/test/runtests.jl b/test/runtests.jl
index 03a4ffb6d..c999c9f4a 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -290,14 +290,15 @@ end
     # See also "Special (Any, Varargs, Generic)" testset above.
     #
     typesdb_cfg = build_typesdb_scfg("merged-small.csv")
-    @test Stb(1) == is_stable_method((@which id1(1)), typesdb_cfg)
+    @test Stb(3) == is_stable_method((@which id1(1)), typesdb_cfg)
+    # We count fuel in a tricky way: it's
+    # number of calls to direct_subtypes1 + number of concrete
+    # tuple types (corresponding to signatures).
+    # The example DB has 2 types.
 
     myplus(x,y)=x+y
     res = is_stable_method((@which id1(1)), typesdb_cfg)
-    @info res
-    @test Stb(1) == res # 1 is weird but that's  how we count fuel:
-    # number of calls to direct_subtypes1, and that one returns
-    # the types DB in whole at once
+    @test Stb(3) == res
 end
 
 module ImportBase; import Base.push!; push!(::Int)=1; end