go static analysis
mohiraREADME
mohiraこういうUnreachableなコードって静的解析で検知できますか？
package main
import "fmt"
func f(x int) {
if x > 99 { // どんな大きなintでも最大99に潰されるので、
x = 99
}
if x == 100 { // ここの条件に該当することはない
fmt.Println("Happy!!!")
}
}
func main() {
f(100)
}
参考: #ミノ駆動本 9章
mohiraどうやら静的解析のみでは難しいらしい。できるかもしれないが、どうも怪しい。
で、SMTソルバやSATソルバ と 静的解析 を組み合わせることで実現可能かもしれない。
静的解析で条件式とかを抜き取って、◯◯ソルバによって、条件を満たす場合があるかどうかを調べたりする。それで、条件を満たさない(充足しない？)場合、Unreachableでだよね。
的な雰囲気という予想。
mohiramohiraif文を消すと、SSAでいけそう説。最適化されて、fmt.Println("Happy")はデッドコードとして消えるっぽい。
package main
import "fmt"
// もっと弱めたバージョン。if文がないやつ。
func f(x int) {
x = 10 // 絶対10という定数になる
if x == 100 { // ここの条件に該当することはない
fmt.Println("Happy!!!")
}
}
func main() {
f(100)
}
Haskelだといけるみたいだぞ！(ただし、静的解析ではない。SMTソルバーは使っているけど)
thanks えびさん
https://discord.com/channels/508093437187457045/508123395905552385/999559250302992464
なるほど。最初のif文を通過した後は x <= 99 だということが分かって欲しいってことですね。
Refinement Types(篩型)で似たようなことができて、それはまさにSMTソルバを使ってるらしいので、できそうですね
Haskellの話でアレなんですが、実例を挙げておきます。
http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1658383474_10929.hs
最初の x' < 100 の状態だとCheckが通らなくて、 x' == 100 に変えるとCheckが通るようになります
(Haskellにこの機能があるわけじゃなくて、コンパイラにLiquidHaskellというプラグインを入れると使えるようになるやつ)
module SimpleRefinements where
import Language.Haskell.Liquid.Prelude
f :: Int -> IO ()
f x = do
let x' = if x > 99 then 99 else x
if x' < 100 then liquidError "Happy!!" else pure ()
とはいえ、静的解析ではない点は注意
説明不足だったので補足しておくと、こっちの例はUnreachableな箇所に静的解析でエラーになるコードを入れておくことで、「この箇所は絶対に通らないよ」ということを保証しています。Unreachableなコードを警告したり消去するような機能ではないです。