feat(rules): empty (U018), a kept length compared to zero is is_empty

LAWS.bend

@@ -148,3 +148,10 @@ import ./laws/PrefixReportsTakeComparedToLiteral.bend as PrefixReportsTakeCompar
 import ./laws/PrefixSkipsOtherLengths.bend as PrefixSkipsOtherLengths
 import ./laws/RolePrefix.bend as RolePrefix
 import ./laws/RolePrefixExempt.bend as RolePrefixExempt
+import ./laws/EmptyExempt.bend as EmptyExempt
+import ./laws/EmptyReportsKeptTest.bend as EmptyReportsKeptTest
+import ./laws/EmptySkipsUnkeptTest.bend as EmptySkipsUnkeptTest
+import ./laws/RoleEmpty.bend as RoleEmpty
+import ./laws/RoleEmptyExempt.bend as RoleEmptyExempt
+import ./laws/InertEmpty.bend as InertEmpty
+import ./laws/EmptySkipsProofs.bend as EmptySkipsProofs

PROOF.bend

@@ -133,3 +133,10 @@ import ./proofs/PrefixReportsTakeComparedToLiteral.bend as PPrefixReportsTakeCom
 import ./proofs/PrefixSkipsOtherLengths.bend as PPrefixSkipsOtherLengths
 import ./proofs/RolePrefix.bend as PRolePrefix
 import ./proofs/RolePrefixExempt.bend as PRolePrefixExempt
+import ./proofs/EmptyExempt.bend as PEmptyExempt
+import ./proofs/EmptyReportsKeptTest.bend as PEmptyReportsKeptTest
+import ./proofs/EmptySkipsUnkeptTest.bend as PEmptySkipsUnkeptTest
+import ./proofs/RoleEmpty.bend as PRoleEmpty
+import ./proofs/RoleEmptyExempt.bend as PRoleEmptyExempt
+import ./proofs/InertEmpty.bend as PInertEmpty
+import ./proofs/EmptySkipsProofs.bend as PEmptySkipsProofs

laws/CodeRulesIgnoreCommentsAndStrings.bend

@@ -4,7 +4,8 @@
 # changing the contents of a comment or string literal does not change the
 # findings.
 #
-# also rests on: laws/InertFromrev.bend, laws/InertTranscong.bend
+# also rests on: laws/InertFromrev.bend, laws/InertTranscong.bend,
+# laws/InertEmpty.bend
 import Base
 import ../src/syntax/lex.bend as Lex
 import ../src/finding.bend as F

laws/EmptyExempt.bend

@@ -0,0 +1,20 @@
+import Base
+import ../src/syntax/lex.bend as Lex
+import ../src/finding.bend as F
+import ../src/syntax/bind.bend as Bind
+import ../src/paths.bend as Paths
+import ../src/src.bend as Src
+import ../src/syntax/tree.bend as Tree
+import ../src/syntax/outline.bend as Outline
+import ../src/rules/suspicious/empty.bend as Empty
+
+# LAW: empty reports nothing in a LAWS.bend or a PROOF.bend, which never run, whatever the source holds
+law empty_exempt:
+  for +path: String
+  for text: String
+  for toks: List<&2, Lex.Tok>
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  for e: {Paths.is_law_file(path) == True{} : Bool}
+  {Empty.check(Src.Src{path, text, toks, tree, bound, items}) == Nil{} : List<&2, F.Finding>}

laws/EmptyReportsKeptTest.bend

@@ -0,0 +1,60 @@
+# `empty` reports `Nat.is_eq(List.length(.., x), 0n)` and
+# `Nat.is_eq(String.length(x), 0n)`, once each, outside a LAWS.bend or a
+# PROOF.bend, when the test is an argument (here the first, after a `(`) and
+# x, a plain name, is read again later in the same group: there the test's
+# reference to x is dropped by a count, and List.is_empty or String.is_empty
+# gives the same Bool from one cell. Every token at line l, column c
+# (laws/defs/EmptyTests.bend).
+import Base
+import ../src/syntax/lex.bend as Lex
+import ../src/finding.bend as F
+import ../src/syntax/bind.bend as Bind
+import ../src/paths.bend as Paths
+import ../src/src.bend as Src
+import ../src/syntax/tree.bend as Tree
+import ../src/syntax/outline.bend as Outline
+import ../src/rules/suspicious/empty.bend as Empty
+import ./defs/EmptyTests.bend as D1
+
+# LAW: empty reports a List.length test that is an argument, x read later in its group, once
+law empty_reports_list_kept:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text, D1.empty.kept(D1.empty.list_test(x, l, c), x, l, c),
+    tree, bound, items})) == 1n : Nat}
+
+# LAW: empty reports a String.length test that is an argument, x read later in its group, once
+law empty_reports_string_kept:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text, D1.empty.kept(D1.empty.str_test(x, l, c), x, l, c),
+    tree, bound, items})) == 1n : Nat}
+
+# LAW: empty reports a kept test in a def that runs, once
+law empty_reports_in_typed_def:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text,
+    D1.empty.in_typed(D1.empty.kept(D1.empty.list_test(x, l, c), x, l, c), l, c),
+    tree, bound, items})) == 1n : Nat}

laws/EmptySkipsProofs.bend

@@ -0,0 +1,61 @@
+# `empty` reports nothing in a law, or in a def that is a proof: one written
+# with no type (`def f(s):`, which fills the law named f) or one that returns
+# a proof (`-> {a == b : T}`). Neither runs, so what a test there costs does
+# not matter, and a law states the test as it means it. Every token at line
+# l, column c (laws/defs/EmptyTests.bend).
+import Base
+import ../src/syntax/lex.bend as Lex
+import ../src/finding.bend as F
+import ../src/syntax/bind.bend as Bind
+import ../src/paths.bend as Paths
+import ../src/src.bend as Src
+import ../src/syntax/tree.bend as Tree
+import ../src/syntax/outline.bend as Outline
+import ../src/rules/suspicious/empty.bend as Empty
+import ./defs/EmptyTests.bend as D1
+
+
+# LAW: empty skips a kept test in a law
+law empty_skips_in_law:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text,
+    D1.empty.in_law(D1.empty.kept(D1.empty.list_test(x, l, c), x, l, c), l, c),
+    tree, bound, items})) == 0n : Nat}
+
+# LAW: empty skips a kept test in a def with no type
+law empty_skips_in_untyped_def:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text,
+    D1.empty.in_untyped(D1.empty.kept(D1.empty.list_test(x, l, c), x, l, c), l, c),
+    tree, bound, items})) == 0n : Nat}
+
+# LAW: empty skips a kept test in a def that returns a proof
+law empty_skips_in_proof_def:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text,
+    D1.empty.in_proof(D1.empty.kept(D1.empty.list_test(x, l, c), x, l, c), l, c),
+    tree, bound, items})) == 0n : Nat}

laws/EmptySkipsUnkeptTest.bend

@@ -0,0 +1,100 @@
+# `empty` reports nothing for a length test whose x is not read after it in
+# its group: one whose group reads no name after it (x is dropped there, and
+# on the native lane freeing a list the program never walked costs more than
+# the walk the test would have made), one that reads x only before it, and
+# one outside any group (bound by a let). Every token at line l, column c
+# (laws/defs/EmptyTests.bend).
+import Base
+import ../src/syntax/lex.bend as Lex
+import ../src/finding.bend as F
+import ../src/syntax/bind.bend as Bind
+import ../src/paths.bend as Paths
+import ../src/src.bend as Src
+import ../src/syntax/tree.bend as Tree
+import ../src/syntax/outline.bend as Outline
+import ../src/rules/suspicious/empty.bend as Empty
+import ./defs/EmptyTests.bend as D1
+
+# LAW: empty skips a List.length test whose group reads no name after it
+law empty_skips_list_dropped:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text, D1.empty.dropped(D1.empty.list_test(x, l, c), l, c),
+    tree, bound, items})) == 0n : Nat}
+
+# LAW: empty skips a String.length test whose group reads no name after it
+law empty_skips_string_dropped:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text, D1.empty.dropped(D1.empty.str_test(x, l, c), l, c),
+    tree, bound, items})) == 0n : Nat}
+
+# LAW: empty skips a List.length test whose x is read only before it
+law empty_skips_list_before:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text, D1.empty.before(D1.empty.list_test(x, l, c), x, l, c),
+    tree, bound, items})) == 0n : Nat}
+
+# LAW: empty skips a String.length test whose x is read only before it
+law empty_skips_string_before:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text, D1.empty.before(D1.empty.str_test(x, l, c), x, l, c),
+    tree, bound, items})) == 0n : Nat}
+
+# LAW: empty skips a List.length test outside any group
+law empty_skips_list_bare:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text, D1.empty.bare(D1.empty.list_test(x, l, c), x, l, c),
+    tree, bound, items})) == 0n : Nat}
+
+# LAW: empty skips a String.length test outside any group
+law empty_skips_string_bare:
+  for +path: String
+  for e: {Paths.is_law_file(path) == False{} : Bool}
+  for +x: String
+  for +l: U32
+  for +c: U32
+  for text: String
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  {List.length(&2, F.Finding, Empty.check(Src.Src{path, text, D1.empty.bare(D1.empty.str_test(x, l, c), x, l, c),
+    tree, bound, items})) == 0n : Nat}

laws/ExemptPathsYieldNoFindings.bend

@@ -5,7 +5,8 @@
 # among its parameters and no `->`, as `def f(x, y):`), which is how Bend
 # fills the law named f; their "reports exactly" rows are read with that skip.
 #
-# also rests on: laws/FromrevExempt.bend, laws/PrefixExempt.bend
+# also rests on: laws/FromrevExempt.bend, laws/PrefixExempt.bend,
+# laws/EmptyExempt.bend
 import Base
 import ../src/syntax/lex.bend as Lex
 import ../src/finding.bend as F

laws/InertEmpty.bend

@@ -0,0 +1,27 @@
+import Base
+import ../src/syntax/lex.bend as Lex
+import ../src/finding.bend as F
+import ../src/syntax/bind.bend as Bind
+import ../src/src.bend as Src
+import ../src/syntax/tree.bend as Tree
+import ../src/syntax/outline.bend as Outline
+import ../src/rules/suspicious/empty.bend as Empty
+import ./defs/InertText.bend as D1
+
+# LAW: empty reads what no comment or string says: two sources whose tokens
+# read the same with comments and strings cut have the same findings
+law inert_empty:
+  for +path: String
+  for text: String
+  for toks: List<&2, Lex.Tok>
+  for tree: Tree.Node
+  for bound: Bind.Bound
+  for items: List<&2, Outline.Item>
+  for text2: String
+  for toks2: List<&2, Lex.Tok>
+  for tree2: Tree.Node
+  for bound2: Bind.Bound
+  for items2: List<&2, Outline.Item>
+  for e: {D1.inert.toks(toks) == D1.inert.toks(toks2) : List<&2, Lex.Tok>}
+  {Empty.check(Src.Src{path, text, toks, tree, bound, items})
+    == Empty.check(Src.Src{path, text2, toks2, tree2, bound2, items2}) : List<&2, F.Finding>}

laws/RoleEmpty.bend

@@ -0,0 +1,20 @@
+import Base
+import ../src/syntax/lex.bend as Lex
+import ../src/finding.bend as F
+import ../src/syntax/bind.bend as Bind
+import ../src/role.bend as Role
+import ../src/src.bend as Src
+import ../src/syntax/tree.bend as Tree
+import ../src/syntax/outline.bend as Outline
+import ../src/rules/suspicious/empty.bend as Empty
+
+# LAW: empty told a file's role by its name finds what empty finds
+law role_empty:
+  for +path: String
+  for +text: String
+  for +toks: List<&2, Lex.Tok>
+  for +tree: Tree.Node
+  for +bound: Bind.Bound
+  for +items: List<&2, Outline.Item>
+  {Empty.check.role(Role.of_path(path), Src.Src{path, text, toks, tree, bound, items})
+    == Empty.check(Src.Src{path, text, toks, tree, bound, items}) : List<&2, F.Finding>}

laws/RoleEmptyExempt.bend

@@ -0,0 +1,21 @@
+import Base
+import ../src/syntax/lex.bend as Lex
+import ../src/finding.bend as F
+import ../src/syntax/bind.bend as Bind
+import ../src/role.bend as Role
+import ../src/src.bend as Src
+import ../src/syntax/tree.bend as Tree
+import ../src/syntax/outline.bend as Outline
+import ../src/rules/suspicious/empty.bend as Empty
+
+# LAW: empty reports nothing in a law or proof file, whatever the source holds
+law role_empty_exempt:
+  for rr: Role.Role
+  for e: {Role.is_law_file(rr) == True{} : Bool}
+  for +path: String
+  for +text: String
+  for +toks: List<&2, Lex.Tok>
+  for +tree: Tree.Node
+  for +bound: Bind.Bound
+  for +items: List<&2, Outline.Item>
+  {Empty.check.role(rr, Src.Src{path, text, toks, tree, bound, items}) == Nil{} : List<&2, F.Finding>}