• 设为首页
  • 点击收藏
  • 手机版
    手机扫一扫访问
    迪恩网络手机版
  • 关注官方公众号
    微信扫一扫关注
    迪恩网络公众号

aviatesk/JET.jl: An experimental code analyzer for Julia, no need for additional ...

原作者: [db:作者] 来自: 网络 收藏 邀请

开源软件名称:

aviatesk/JET.jl

开源软件地址:

https://github.com/aviatesk/JET.jl

开源编程语言:

Julia 100.0%

开源软件介绍:

JET.jl

CI codecov

JET.jl employs Julia's type inference to detect potential bugs.

!!! note The latest version of JET requires Julia versions 1.7 and higher; JET is tested against the current stable release as well as nightly version.
Also note that JET deeply relies on the type inference routine implemented in the Julia compiler, and so the analysis result can vary depending on your Julia version. In general, the newer your Julia version is, more accurately and quickly your can expect JET to analyze your code, assuming the Julia compiler keeps evolving all the time from now on.

!!! tip Hold on tight and fasten your seatbelt while JET is analyzing your code for the first time. Once the caches get accumulated, subsequent analysis will run at speed.

Demo

Say you have this strange and buggy file and want to know where to fix:

demo.jl

# demo
# ====

# fibonacci
# ---------

fib(n) = n  2 ? n : fib(n-1) + fib(n-2)

fib(1000)   # never terminates in ordinal execution
fib(m)      # undef var
fib("1000") # obvious type error


# language features
# -----------------

# user-defined types, macros
struct Ty{T}
    fld::T
end

function foo(a)
    v = Ty(a)
    return bar(v)
end

# macros will be expanded
@inline bar(n::T)     where {T<:Number} = n < 0 ? zero(T) : one(T)
@inline bar(v::Ty{T}) where {T<:Number} = bar(v.fdl) # typo "fdl"
@inline bar(v::Ty)                      = bar(convert(Number, v.fld))

foo(1.2)
foo("1") # `String` can't be converted to `Number`

# even staged programming
# adapted from https://github.com/JuliaLang/julia/blob/9f665c19e076ab37cbca2d0cc99283b82e99c26f/base/namedtuple.jl#L253-L264
@generated function badmerge(a::NamedTuple{an}, b::NamedTuple{bn}) where {an, bn}
    names = Base.merge_names(an, bn)
    types = Base.merge_types(names, a, b)
    vals = Any[ :(getfield($(Base.sym_in(names[n], bn) ? :b : :a), $(names[n]))) for n in 1:length(names) ] # missing quote, just ends up with under vars
    :( NamedTuple{$names,$types}(($(vals...),)) )
end

badmerge((x=1,y=2), (y=3,z=1))

You can have JET.jl detect possible errors:

julia> using JET

julia> report_and_watch_file("demo.jl"; annotate_types = true)
[toplevel-info] virtualized the context of Main (took 0.013 sec)
[toplevel-info] entered into demo.jl
[toplevel-info]  exited from demo.jl (took 3.254 sec)
═════ 7 possible errors found ═════
┌ @ demo.jl:10 fib(m)
│ variable m is not defined
└──────────────
┌ @ demo.jl:11 fib("1000")
│┌ @ demo.jl:7 n::String : 2
││┌ @ operators.jl:392 x::String < y::Int64
│││┌ @ operators.jl:343 isless(x::String, y::Int64)
││││ no matching method found for `isless(::String, ::Int64)`: isless(x::String, y::Int64)
│││└────────────────────
┌ @ demo.jl:32 foo(1.2)
│┌ @ demo.jl:24 bar(v::Union{})
││┌ @ demo.jl:29 (v::Ty{Float64}).fdl
│││┌ @ Base.jl:37 Base.getfield(x::Ty{Float64}, f::Symbol)
││││ type Ty{Float64} has no field fdl
│││└──────────────
┌ @ demo.jl:33 foo("1")
│┌ @ demo.jl:24 bar(v::Union{})
││┌ @ demo.jl:30 convert(Number, (v::Ty{String}).fld)
│││ no matching method found for `convert(::Type{Number}, ::String)`: convert(Number, (v::Ty{String}).fld)
││└──────────────
┌ @ demo.jl:44 badmerge(NamedTuple{(:x, :y)}(tuple(1, 2)), NamedTuple{(:y, :z)}(tuple(3, 1)))
│┌ @ demo.jl:37 getfield(a::NamedTuple{(:x, :y), Tuple{Int64, Int64}}, x)
││ variable x is not defined
│└──────────────
│┌ @ demo.jl:37 getfield(b::NamedTuple{(:y, :z), Tuple{Int64, Int64}}, y)
││ variable y is not defined
│└──────────────
│┌ @ demo.jl:37 getfield(b::NamedTuple{(:y, :z), Tuple{Int64, Int64}}, z)
││ variable z is not defined
│└──────────────

Hooray! JET.jl found possible error points (e.g. MethodError: no method matching isless(::String, ::Int64)) given toplevel call signatures of generic functions (e.g. fib("1000")).

Note that JET can find these errors while demo.jl is so inefficient (especially the fib implementation) that it would never terminate in actual execution. That is possible because JET analyzes code only on type level. This technique is often called "abstract interpretation" and JET internally uses Julia's native type inference implementation, so it can analyze code as fast/correctly as Julia's code generation.

Lastly let's apply the following diff to demo.jl so that it works nicely:

fix-demo.jl.diff

diff --git a/demo.jl b/demo.jl
index f868d2f..634e130 100644
--- a/demo.jl
+++ b/demo.jl
@@ -4,11 +4,21 @@
 # fibonacci
 # ---------

-fib(n) = n ≤ 2 ? n : fib(n-1) + fib(n-2)
+# cache, cache, cache
+function fib(n::T) where {T<:Number}
+    cache = Dict(zero(T)=>zero(T), one(T)=>one(T))
+    return _fib(n, cache)
+end
+_fib(n, cache) = if haskey(cache, n)
+    cache[n]
+else
+    cache[n] = _fib(n-1, cache) + _fib(n-2, cache)
+end

-fib(1000)   # never terminates in ordinal execution
-fib(m)      # undef var
-fib("1000") # obvious type error
+fib(BigInt(1000)) # will terminate in ordinal execution as well
+m = 1000          # define m
+fib(m)
+fib(parse(Int, "1000"))


 # language features
@@ -26,19 +36,19 @@ end

 # macros will be expanded
 @inline bar(n::T)     where {T<:Number} = n < 0 ? zero(T) : one(T)
-@inline bar(v::Ty{T}) where {T<:Number} = bar(v.fdl) # typo "fdl"
+@inline bar(v::Ty{T}) where {T<:Number} = bar(v.fld) # typo fixed
 @inline bar(v::Ty)                      = bar(convert(Number, v.fld))

 foo(1.2)
-foo("1") # `String` can't be converted to `Number`
+foo('1') # `Char` will be converted to `UInt32`

 # even staged programming
 # adapted from https://github.com/JuliaLang/julia/blob/9f665c19e076ab37cbca2d0cc99283b82e99c26f/base/namedtuple.jl#L253-L264
-@generated function badmerge(a::NamedTuple{an}, b::NamedTuple{bn}) where {an, bn}
+@generated function goodmerge(a::NamedTuple{an}, b::NamedTuple{bn}) where {an, bn}
     names = Base.merge_names(an, bn)
     types = Base.merge_types(names, a, b)
-    vals = Any[ :(getfield($(Base.sym_in(names[n], bn) ? :b : :a), $(names[n]))) for n in 1:length(names) ] # missing quote, just ends up with under vars
+    vals = Any[ :(getfield($(Base.sym_in(names[n], bn) ? :b : :a), $(QuoteNode(names[n])))) for n in 1:length(names) ] # names quoted, should work as expected
     :( NamedTuple{$names,$types}(($(vals...),)) )
 end

-badmerge((x=1,y=2), (y=3,z=1))
+goodmerge((x=1,y=2), (y=3,z=1))

If you apply the diff (i.e. update and save the demo.jl), JET will automatically re-trigger analysis, and this time, won't complain anything:

git apply fix-demo.jl.diff

[toplevel-info] virtualized the context of Main (took 0.004 sec)
[toplevel-info] entered into demo.jl
[toplevel-info]  exited from demo.jl (took 1.375 sec)
No errors detected

Limitations

JET explores the functions you call directly as well as their inferrable callees. However, if the argument-types for a call cannot be inferred, JET does not analyze the callee. Consequently, a report of No errors detected does not imply that your entire codebase is free of errors.

JET integrates with SnoopCompile, and you can sometimes use SnoopCompile to collect the data to perform more comprehensive analyses. SnoopCompile's limitation is that it only collects data for calls that have not been previously inferred, so you must perform this type of analysis in a fresh session.

See SnoopCompile's JET-integration documentation for further details.

Roadmap

  • more accuracy: abstract interpretation can be improved yet more
    • switch to new type lattice design: to simplify the addition of further improvements
    • design and introduce a more proper backward-analysis pass, e.g. effect and escape analysis: to enable further constraint propagation
  • more performance: JET should be much faster
    • aggregate similar errors more smartly and aggressively
    • introduce parallelism to Julia's native type inference routine
  • better documentation: especially JET needs a specification of its error reports
  • editor/IDE integration: GUI would definitely be more appropriate for showing JET's analysis result
    • smarter code dependency tracking: the watch mode currently re-analyzes the whole code on each update, which is the most robust and least efficient option. When integrated with an IDE, fancier incremental analysis based on smarter code dependency tracking like what Revise.jl does would be needed
    • LSP support: ideally I hope to extend JET to provide some of LSP features other than diagnostics, e.g. auto-completions, rename refactor, taking type-level information into account

Acknowledgement

This project started as my undergrad thesis project at Kyoto University, supervised by Prof. Takashi Sakuragawa. We were heavily inspired by ruby/typeprof, an experimental type understanding/checking tool for Ruby. The grad thesis about this project is published at https://github.com/aviatesk/grad-thesis, but currently it's only available in Japanese.




鲜花

握手

雷人

路过

鸡蛋
该文章已有0人参与评论

请发表评论

全部评论

专题导读
热门推荐
阅读排行榜

扫描微信二维码

查看手机版网站

随时了解更新最新资讯

139-2527-9053

在线客服(服务时间 9:00~18:00)

在线QQ客服
地址:深圳市南山区西丽大学城创智工业园
电邮:jeky_zhao#qq.com
移动电话:139-2527-9053

Powered by 互联科技 X3.4© 2001-2213 极客世界.|Sitemap