Warn if non-anonymous variable appears only once. (#1310)

* cleanup checks a bit

* add check for unused variables

* beef up test some more

* fix crash in test

* fix warnings

* fix bug with contexts

* handle fresh anonymous constants

* add test

* update test

* update output file

* fix another false positive

* more warnings in prelude

* update tests more

* fix test

* update test

* add more tests

* don't make warnings fatal

Co-authored-by: rv-jenkins <admin@runtimeverification.com>

k-distribution/include/kframework/builtin/domains.k

@@ -468,9 +468,9 @@ module INT-SYMBOLIC [symbolic, kore]
 
   // Bit-shifts
   rule X <<Int 0 => X [simplification]
-  rule 0 <<Int X => 0 [simplification]
+  rule 0 <<Int _ => 0 [simplification]
   rule X >>Int 0 => X [simplification]
-  rule 0 >>Int X => 0 [simplification]
+  rule 0 >>Int _ => 0 [simplification]
 endmodule
 
 module INT-KAST [kast]
@@ -543,7 +543,6 @@ module FLOAT
   syntax Bool ::= signFloat(Float)      [function, functional, hook(FLOAT.sign)]
                 | isNaN(Float)          [function, functional, smt-hook(fp.isNaN), hook(FLOAT.isNaN)]
                 | isInfinite(Float)     [function, functional]
-  syntax MInt ::= significandFloat(Float) [function, hook(FLOAT.significand)]
 
   syntax Float ::= "--Float" Float             [function, functional, smt-hook(fp.neg), hook(FLOAT.neg)]
                  > Float "^Float" Float        [function, left, latex({#1}^{#2}), hook(FLOAT.pow)]
@@ -811,12 +810,12 @@ module BYTES-IN-K
   rule BS [ N <- M ] => substrBytes(BS, 0, N) +Bytes M : substrBytes(BS, N +Int 1, lengthBytes(BS))
 
   syntax Int ::= Bytes "[" Int "]" [function]
-  rule (B : BS) [ 0 ] => B
+  rule (B : _) [ 0 ] => B
   rule (_ : BS) [ I ] => BS [ I -Int 1] requires I >Int 0
 
   syntax Bytes ::= substrBytes(Bytes, Int, Int) [function]
-  rule substrBytes(BS, 0, 0) => nilBytes
-  rule substrBytes(B : BS, N, M) => substrBytes(BS, N -Int 1, M -Int 1) requires N >Int 0
+  rule substrBytes(_, 0, 0) => nilBytes
+  rule substrBytes(_ : BS, N, M) => substrBytes(BS, N -Int 1, M -Int 1) requires N >Int 0
   rule substrBytes(B : BS, 0, M) => B : substrBytes(BS, 0, M -Int 1) requires M >Int 0
 
   syntax Bytes ::= replaceAtBytes(Bytes, Int, Bytes) [function]
@@ -827,7 +826,7 @@ module BYTES-IN-K
   syntax Bytes ::= padRightBytes(Bytes, Int, Int) [function]
                  | padLeftBytes(Bytes, Int, Int) [function]
   rule padRightBytes(BS, LEN, VAL) => reverseBytes(padLeftBytes(reverseBytes(BS), LEN, VAL))
-  rule padLeftBytes(BS, LEN, VAL) => BS requires lengthBytes(BS) >=Int LEN
+  rule padLeftBytes(BS, LEN, _) => BS requires lengthBytes(BS) >=Int LEN
   rule padLeftBytes(BS, LEN, VAL) => padLeftBytes(VAL : BS, LEN, VAL) requires lengthBytes(BS) <Int LEN
 
   syntax Bytes ::= reverseBytes(Bytes) [function, functional]
@@ -840,7 +839,7 @@ module BYTES-IN-K
   syntax Int ::= lengthBytes(Bytes, Int) [function, klabel(lengthBytesAux), smtlib(lengthBytesAux)]
   rule lengthBytes(BS) => lengthBytes(BS, 0)
   rule lengthBytes(nilBytes, SIZE) => SIZE
-  rule lengthBytes(B : BS, SIZE) => lengthBytes(BS, SIZE +Int 1)
+  rule lengthBytes(_ : BS, SIZE) => lengthBytes(BS, SIZE +Int 1)
 
   syntax Bytes ::= Bytes "+Bytes" Bytes [function, functional, right]
   rule nilBytes +Bytes B2 => B2

k-distribution/include/kframework/builtin/rat.k

@@ -130,7 +130,7 @@ module RAT
    * exponentiation
    */
 
-  rule X ^Rat 0 => 1
+  rule _ ^Rat 0 => 1
   rule 0 ^Rat N => 0 requires N =/=Int 0
 
   rule < I , J >Rat ^Rat N => powRat(< I , J >Rat, N) requires N >Int 0

k-distribution/tests/regression-new/checkWarns/Makefile

@@ -0,0 +1,4 @@
+KOMPILE_FLAGS=-w2e
+KOMPILE_BACKEND=llvm
+
+include ../../../include/kframework/ktest-fail.mak

k-distribution/tests/regression-new/checkWarns/checkUnusedVar.k

@@ -0,0 +1,29 @@
+module CHECKUNUSEDVAR-SYNTAX
+
+endmodule
+
+module MOD
+  imports INT
+  configuration <bar> 0 </bar>
+endmodule
+
+module CHECKUNUSEDVAR
+  imports INT
+  imports MOD
+
+  syntax KItem ::= foo(Int)
+
+  rule foo(X) => 0
+  rule foo(0) => !_:Int
+
+  rule foo(X) => 0
+    requires X >Int 0
+  rule foo(X) => 1
+    requires 0 >Int 0
+
+  rule foo(X) => ?X:Int
+    ensures X >Int 0
+
+  configuration <k> $PGM:K </k> <foo multiplicity="?"> <bar/> </foo>
+
+endmodule

k-distribution/tests/regression-new/checkWarns/checkUnusedVar.k.out

@@ -0,0 +1,10 @@
+[Error] Compiler: Had 3 structural errors.
+[Error] Compiler: Variable '?X' defined but not used.
+	Source(checkUnusedVar.k)
+	Location(24,18,24,20)
+[Error] Compiler: Variable 'X' defined but not used.
+	Source(checkUnusedVar.k)
+	Location(16,12,16,13)
+[Error] Compiler: Variable 'X' defined but not used.
+	Source(checkUnusedVar.k)
+	Location(21,12,21,13)

k-distribution/tests/regression-new/checks/intOperationInLHS.k

@@ -4,7 +4,7 @@ module INTOPERATIONINLHS
 
 syntax Int ::= "foo" "(" Int ")" [function]
 
-rule foo(A +Int 1) => 0
+rule foo(_ +Int 1) => 0
 
 syntax Int ::= bar(Map) [function]
 

k-distribution/tests/regression-new/kprove-java/rhs-vars-broken-spec.k.out

@@ -1,4 +1,7 @@
 #True
+[Warning] Compiler: Variable 'A' defined but not used.
+	Source(rhs-vars-broken-spec.k)
+	Location(12,20,12,21)
 [Warning] Critical: Found variable A on right hand side of rule, not bound on
 left hand side. Did you mean "?A"?
 Note: this warning will become an error in subsequent releases.

k-distribution/tests/regression-new/nonexhaustive/test.k

@@ -42,49 +42,49 @@ syntax Int ::= foo4(Bytes) [function, functional]
 
 syntax Int ::= foo5(List) [function, functional]
 rule foo5(.List) => 0
-rule foo5(ListItem(X)) => 0
-rule foo5(ListItem(X) ListItem(Y) ListItem(Z) L) => 0
-rule foo5(ListItem(X) ListItem(0)) => 0
+rule foo5(ListItem(_)) => 0
+rule foo5(ListItem(_) ListItem(_) ListItem(_) _) => 0
+rule foo5(ListItem(_) ListItem(0)) => 0
 
 syntax Int ::= foo6(Map, KItem) [function, functional]
 rule foo6(.Map, _) => 0
-rule foo6(X |-> Y Z::Map, X) => 0
+rule foo6(X |-> _ _::Map, X) => 0
 
 syntax Int ::= foo7(Map) [function, functional]
 rule foo7(.Map) => 0
-rule foo7(X |-> Y) => 0
-rule foo7(X |-> Y A |-> B C |-> D Z::Map) => 0
-rule foo7(X |-> Y 0 |-> B) => 0
+rule foo7(_ |-> _) => 0
+rule foo7(_ |-> _ _ |-> _ _ |-> _ _::Map) => 0
+rule foo7(_ |-> _ 0 |-> _) => 0
 
 syntax Int ::= foo8(Map, KItem) [function, functional]
 rule foo8(.Map, _) => 0
-rule foo8(X |-> Y, X) => 0
-rule foo8(Y |-> Z, X) => 0
-rule foo8(Y |-> Z A |-> B W::Map, X) => 0
+rule foo8(X |-> _, X) => 0
+rule foo8(_ |-> _, _) => 0
+rule foo8(_ |-> _ _ |-> _ _::Map, _) => 0
 
 syntax Int ::= foo9(Map) [function, functional]
-rule foo9(X |-> Y) => 0
-rule foo9(A |-> B C |-> D M::Map) => 0
+rule foo9(_ |-> _) => 0
+rule foo9(_ |-> _ _ |-> _ _::Map) => 0
 
 syntax Int ::= foo6(Set, KItem) [function, functional]
 rule foo6(.Set, _) => 0
-rule foo6(SetItem(X) Z::Set, X) => 0
+rule foo6(SetItem(X) _::Set, X) => 0
 
 syntax Int ::= foo7(Set) [function, functional]
 rule foo7(.Set) => 0
-rule foo7(SetItem(X)) => 0
-rule foo7(SetItem(X) SetItem(A) SetItem(C) Z::Set) => 0
-rule foo7(SetItem(X) SetItem(0)) => 0
+rule foo7(SetItem(_)) => 0
+rule foo7(SetItem(_) SetItem(_) SetItem(_) _::Set) => 0
+rule foo7(SetItem(_) SetItem(0)) => 0
 
 syntax Int ::= foo8(Set, KItem) [function, functional]
 rule foo8(.Set, _) => 0
 rule foo8(SetItem(X), X) => 0
-rule foo8(SetItem(Y), X) => 0
-rule foo8(SetItem(Y) SetItem(A) W::Set, X) => 0
+rule foo8(SetItem(_), _) => 0
+rule foo8(SetItem(_) SetItem(_) _::Set, _) => 0
 
 syntax Int ::= foo9(Set) [function, functional]
-rule foo9(SetItem(X)) => 0
-rule foo9(SetItem(A) SetItem(C) M) => 0
+rule foo9(SetItem(_)) => 0
+rule foo9(SetItem(_) SetItem(_) _) => 0
 
 syntax Int ::= foo10(Float) [function, functional]
 rule foo10(0.0) => 0

k-distribution/tests/regression-new/prelude-warnings/test.k

@@ -1,3 +1,8 @@
+require "ffi.k"
+require "json.k"
+require "rat.k"
+require "substitution.k"
+
 module TEST-SYNTAX
 endmodule
 
@@ -10,7 +15,15 @@ module TEST
   imports BYTES
   imports K-IO
   imports DEFAULT-STRATEGY
+  imports MINT
+  imports FFI
+  imports JSON
+  imports RAT
+  imports SUBSTITUTION
   imports TEST-SYNTAX
 
+  syntax MInt{8}
+  rule I:Int => Int2MInt(I)::MInt{8}
+
   configuration <k> $PGM:K </k> <s/>
 endmodule

k-distribution/tests/regression-new/useless/test.k

@@ -17,52 +17,52 @@ module TEST
   imports STRING-BUFFER
 
 syntax Int ::= foo(Int) [function]
-rule foo(A) => 0
-rule foo(B) => 0
+rule foo(A) => A
+rule foo(B) => B
 
 syntax Int ::= foo2(Foo) [function]
 syntax Foo ::= bar() | baz()
 
 rule foo2(bar()) => 0
-rule foo2(BAR) => 0
+rule foo2(_) => 0
 
 syntax Int ::= foo3(String) [function]
 rule foo3("") => 0
-rule foo3(BAR) => 0
+rule foo3(_) => 0
 
 syntax Int ::= foo4(Bytes) [function]
-rule foo4(BAR) => 0
-rule foo4(BAZ) => 0
+rule foo4(BAR) => lengthBytes(BAR)
+rule foo4(BAZ) => lengthBytes(BAZ)
 
 syntax Int ::= foo5(List) [function]
-rule foo5(ListItem(X)) => 0
-rule foo5(ListItem(Y) L) => 0
+rule foo5(ListItem(_)) => 0
+rule foo5(ListItem(_) _) => 0
 
 syntax Int ::= foo6(Map, KItem) [function]
-rule foo6(X |-> Y, X) => 0
-rule foo6(X |-> Y Z::Map, X) => 0
+rule foo6(X |-> _, X) => 0
+rule foo6(X |-> _ _::Map, X) => 0
 
 syntax Int ::= foo7(Map) [function]
-rule foo7(X |-> Y) => 0
-rule foo7(X |-> Y Z::Map) => 0
+rule foo7(_ |-> _) => 0
+rule foo7(_ |-> _ _::Map) => 0
 
 syntax Int ::= foo8(Map, KItem) [function]
-rule foo8(X |-> Y, X) => 0
-rule foo8(Y |-> Z, X) => 0
-rule foo8(Y |-> Z W::Map, X) => 0
+rule foo8(X |-> _, X) => 0
+rule foo8(_ |-> _, _) => 0
+rule foo8(_ |-> _ _::Map, _) => 0
 
 syntax Int ::= foo6(Set, KItem) [function]
 rule foo6(SetItem(X), X) => 0
-rule foo6(SetItem(X) Z, X) => 0
+rule foo6(SetItem(X) _, X) => 0
 
 syntax Int ::= foo7(Set) [function]
-rule foo7(SetItem(X)) => 0
-rule foo7(SetItem(X) Z) => 0
+rule foo7(SetItem(_)) => 0
+rule foo7(SetItem(_) _) => 0
 
 syntax Int ::= foo8(Set, KItem) [function]
 rule foo8(SetItem(X), X) => 0
-rule foo8(SetItem(Y), X) => 0
-rule foo8(SetItem(Y) W, X) => 0
+rule foo8(SetItem(_), _) => 0
+rule foo8(SetItem(_) _, _) => 0
 
 syntax Int ::= foo10(Float) [function]
 rule foo10(0.0) => 0
@@ -76,15 +76,15 @@ rule foo10a(0.0p53x11) => 0
 
 syntax Int ::= foo11(Bool) [function]
 rule foo11(true) => 0
-rule foo11(B) => 0
+rule foo11(_) => 0
 
 syntax KVar ::= "x" [token]
 syntax Int ::= foo12(KVar) [function]
 rule foo12(x) => 0
-rule foo12(X) => 0
+rule foo12(_) => 0
 
 syntax Int ::= foo13(StringBuffer) [function]
-rule foo13(BAR) => 0
-rule foo13(BAZ) => 0
+rule foo13(BAR) => lengthString(StringBuffer2String(BAR))
+rule foo13(BAZ) => lengthString(StringBuffer2String(BAZ))
 
 endmodule

k-distribution/tests/regression-new/useless/test.k.out

@@ -13,10 +13,10 @@
 	Location(30,6,30,19)
 [Error] Compiler: Potentially useless rule detected.
 	Source(test.k)
-	Location(34,6,34,20)
+	Location(34,6,34,35)
 [Error] Compiler: Potentially useless rule detected.
 	Source(test.k)
-	Location(35,6,35,20)
+	Location(35,6,35,35)
 [Error] Compiler: Potentially useless rule detected.
 	Source(test.k)
 	Location(38,6,38,28)
@@ -58,7 +58,7 @@
 	Location(83,6,83,19)
 [Error] Compiler: Potentially useless rule detected.
 	Source(test.k)
-	Location(87,6,87,21)
+	Location(87,6,87,58)
 [Error] Compiler: Potentially useless rule detected.
 	Source(test.k)
-	Location(88,6,88,21)
+	Location(88,6,88,58)

kernel/src/main/java/org/kframework/compile/GatherVarsVisitor.java

@@ -20,7 +20,7 @@ public GatherVarsVisitor(boolean isBody, Set<KEMException> errors, Set<KVariable
 
     @Override
     public void apply(KVariable v) {
-        if (isLHS() && !v.equals(ResolveAnonVar.ANON_VAR) && !v.equals(ResolveAnonVar.FRESH_ANON_VAR))
+        if (isLHS() && !ResolveAnonVar.isAnonVar(v))
             vars.add(v);
         super.apply(v);
     }