From 786482bba26b8583f31e6414bde0d87f89b399ef Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 1 Nov 2026 17:31:49 +0000 Subject: [PATCH] feat(rules): empty (U018), a kept length compared to zero is is_empty `empty` reports `Nat.is_eq(List.length(.., x), 0n)` and `Nat.is_eq(String.length(x), 0n)` when the test is an argument (right after `(`, `[`, `{` or `,`) and x, a plain name, is read again after it in the same group. Base's lengths count every cell and are not tail calls; `List.is_empty(.., x)` / `String.is_empty(x)` take the same arguments, look at one cell and give the same Bool. Only a kept x is reported: when the test is x's last use, the native lane frees a list the program never walked more slowly than it walks one, so the fix loses there (bend 2.0.38, a 0-1000 char String: kept 1.57x native and 1.31x JS; dropped 0.27x native, 1.65x JS). A law, a def that is a proof (no type, or `-> {..}`), a LAWS.bend and a PROOF.bend are skipped. Over the public Bend 2 corpus it reports 8 sites in 2 repos (BendKV 6, birc 2), each read by hand. On in `suspicious` by default. Laws: empty_reports_{list,string}_kept, empty_reports_in_typed_def, empty_skips_{list,string}_{dropped,before,bare} (no read after, a read only before, outside any group), empty_skips_in_{law,untyped_def,proof_def}, empty_exempt, role_empty, role_empty_exempt and inert_empty (comments and string contents never change the findings). The code table proof gains its 37th row. bolt's own dir_of tested a kept list's length; it uses List.is_empty now. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0186KEnst9PZ9GVQD8BtKhu4 --- LAWS.bend | 7 + PROOF.bend | 7 + laws/CodeRulesIgnoreCommentsAndStrings.bend | 3 +- laws/EmptyExempt.bend | 20 + laws/EmptyReportsKeptTest.bend | 60 ++ laws/EmptySkipsProofs.bend | 61 ++ laws/EmptySkipsUnkeptTest.bend | 100 ++++ laws/ExemptPathsYieldNoFindings.bend | 3 +- laws/InertEmpty.bend | 27 + laws/RoleEmpty.bend | 20 + laws/RoleEmptyExempt.bend | 21 + laws/defs/EmptyTests.bend | 65 ++ proofs/EmptyExempt.bend | 14 + proofs/EmptyReportsKeptTest.bend | 52 ++ proofs/EmptySkipsProofs.bend | 31 + proofs/EmptySkipsUnkeptTest.bend | 46 ++ proofs/InertEmpty.bend | 625 ++++++++++++++++++++ proofs/OutputCodesMapOneToOne.bend | 10 +- proofs/RoleEmpty.bend | 17 + proofs/RoleEmptyExempt.bend | 10 + src/README.md | 23 +- src/codes.bend | 1 + src/rules.bend | 4 +- src/rules/imports.bend | 2 +- src/rules/suspicious/empty.bend | 372 ++++++++++++ 25 files changed, 1593 insertions(+), 8 deletions(-) create mode 100644 laws/EmptyExempt.bend create mode 100644 laws/EmptyReportsKeptTest.bend create mode 100644 laws/EmptySkipsProofs.bend create mode 100644 laws/EmptySkipsUnkeptTest.bend create mode 100644 laws/InertEmpty.bend create mode 100644 laws/RoleEmpty.bend create mode 100644 laws/RoleEmptyExempt.bend create mode 100644 laws/defs/EmptyTests.bend create mode 100644 proofs/EmptyExempt.bend create mode 100644 proofs/EmptyReportsKeptTest.bend create mode 100644 proofs/EmptySkipsProofs.bend create mode 100644 proofs/EmptySkipsUnkeptTest.bend create mode 100644 proofs/InertEmpty.bend create mode 100644 proofs/RoleEmpty.bend create mode 100644 proofs/RoleEmptyExempt.bend create mode 100644 src/rules/suspicious/empty.bend diff --git a/LAWS.bend b/LAWS.bend index 688cad8..f6eadab 100644 --- a/LAWS.bend +++ b/LAWS.bend @@ -158,3 +158,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 diff --git a/PROOF.bend b/PROOF.bend index 90d84bb..4f23368 100644 --- a/PROOF.bend +++ b/PROOF.bend @@ -143,3 +143,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 diff --git a/laws/CodeRulesIgnoreCommentsAndStrings.bend b/laws/CodeRulesIgnoreCommentsAndStrings.bend index 5bb81be..1d42004 100644 --- a/laws/CodeRulesIgnoreCommentsAndStrings.bend +++ b/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 diff --git a/laws/EmptyExempt.bend b/laws/EmptyExempt.bend new file mode 100644 index 0000000..21fa190 --- /dev/null +++ b/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>} diff --git a/laws/EmptyReportsKeptTest.bend b/laws/EmptyReportsKeptTest.bend new file mode 100644 index 0000000..f41e2da --- /dev/null +++ b/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} diff --git a/laws/EmptySkipsProofs.bend b/laws/EmptySkipsProofs.bend new file mode 100644 index 0000000..b7470ac --- /dev/null +++ b/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} diff --git a/laws/EmptySkipsUnkeptTest.bend b/laws/EmptySkipsUnkeptTest.bend new file mode 100644 index 0000000..4cfe70b --- /dev/null +++ b/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} diff --git a/laws/ExemptPathsYieldNoFindings.bend b/laws/ExemptPathsYieldNoFindings.bend index d238fad..1bb502d 100644 --- a/laws/ExemptPathsYieldNoFindings.bend +++ b/laws/ExemptPathsYieldNoFindings.bend @@ -6,7 +6,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 diff --git a/laws/InertEmpty.bend b/laws/InertEmpty.bend new file mode 100644 index 0000000..57ec100 --- /dev/null +++ b/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>} diff --git a/laws/RoleEmpty.bend b/laws/RoleEmpty.bend new file mode 100644 index 0000000..6241f8e --- /dev/null +++ b/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>} diff --git a/laws/RoleEmptyExempt.bend b/laws/RoleEmptyExempt.bend new file mode 100644 index 0000000..01f7034 --- /dev/null +++ b/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>} diff --git a/laws/defs/EmptyTests.bend b/laws/defs/EmptyTests.bend new file mode 100644 index 0000000..d520c62 --- /dev/null +++ b/laws/defs/EmptyTests.bend @@ -0,0 +1,65 @@ +# the tokens of the tests `empty` reads, as the lexer makes them, every token +# at line l, column c: the laws about `empty` build their sources from these +import Base +import ../../src/syntax/lex.bend as Lex + +# `Nat.is_eq(List.length(&2, U32, x), 0n)` +def empty.list_test(+xx: String, +ll: U32, +cc: U32) -> List<&2, Lex.Tok>: + [Lex.Tok{Lex.TDotted{}, "Nat.is_eq", ll, cc}, Lex.Tok{Lex.TOpen{}, "(", ll, cc}, + Lex.Tok{Lex.TDotted{}, "List.length", ll, cc}, Lex.Tok{Lex.TOpen{}, "(", ll, cc}, + Lex.Tok{Lex.TAmp{}, "&", ll, cc}, Lex.Tok{Lex.TNum{}, "2", ll, cc}, Lex.Tok{Lex.TComma{}, ",", ll, cc}, + Lex.Tok{Lex.TUpper{}, "U32", ll, cc}, Lex.Tok{Lex.TComma{}, ",", ll, cc}, + Lex.Tok{Lex.TName{}, xx, ll, cc}, Lex.Tok{Lex.TClose{}, ")", ll, cc}, + Lex.Tok{Lex.TComma{}, ",", ll, cc}, Lex.Tok{Lex.TNum{}, "0n", ll, cc}, Lex.Tok{Lex.TClose{}, ")", ll, cc}] + +# `Nat.is_eq(String.length(x), 0n)` +def empty.str_test(+xx: String, +ll: U32, +cc: U32) -> List<&2, Lex.Tok>: + [Lex.Tok{Lex.TDotted{}, "Nat.is_eq", ll, cc}, Lex.Tok{Lex.TOpen{}, "(", ll, cc}, + Lex.Tok{Lex.TDotted{}, "String.length", ll, cc}, Lex.Tok{Lex.TOpen{}, "(", ll, cc}, + Lex.Tok{Lex.TName{}, xx, ll, cc}, Lex.Tok{Lex.TClose{}, ")", ll, cc}, + Lex.Tok{Lex.TComma{}, ",", ll, cc}, Lex.Tok{Lex.TNum{}, "0n", ll, cc}, Lex.Tok{Lex.TClose{}, ")", ll, cc}] + +# a test as the first argument of a call whose next argument is x: `(`, the +# test, `,`, x and `)` +def empty.kept(test: List<&2, Lex.Tok>, +xx: String, +ll: U32, +cc: U32) -> List<&2, Lex.Tok>: + Lex.Tok{Lex.TOpen{}, "(", ll, cc} <> List.append(&2, Lex.Tok, test, + [Lex.Tok{Lex.TComma{}, ",", ll, cc}, Lex.Tok{Lex.TName{}, xx, ll, cc}, Lex.Tok{Lex.TClose{}, ")", ll, cc}]) + +# a test as the first argument of a call whose next argument is no name: +# `(`, the test, `,`, `1` and `)` +def empty.dropped(test: List<&2, Lex.Tok>, +ll: U32, +cc: U32) -> List<&2, Lex.Tok>: + Lex.Tok{Lex.TOpen{}, "(", ll, cc} <> List.append(&2, Lex.Tok, test, + [Lex.Tok{Lex.TComma{}, ",", ll, cc}, Lex.Tok{Lex.TNum{}, "1", ll, cc}, Lex.Tok{Lex.TClose{}, ")", ll, cc}]) + +# a test as the last argument of a call whose first is x: `(`, x, `,`, the +# test and `)` +def empty.before(test: List<&2, Lex.Tok>, +xx: String, +ll: U32, +cc: U32) -> List<&2, Lex.Tok>: + Lex.Tok{Lex.TOpen{}, "(", ll, cc} <> Lex.Tok{Lex.TName{}, xx, ll, cc} <> Lex.Tok{Lex.TComma{}, ",", ll, cc} + <> List.append(&2, Lex.Tok, test, [Lex.Tok{Lex.TClose{}, ")", ll, cc}]) + +# a test bound by a let, then x: `v`, `=`, the test and x +def empty.bare(test: List<&2, Lex.Tok>, +xx: String, +ll: U32, +cc: U32) -> List<&2, Lex.Tok>: + Lex.Tok{Lex.TName{}, "v", ll, cc} <> Lex.Tok{Lex.TEq{}, "=", ll, cc} + <> List.append(&2, Lex.Tok, test, [Lex.Tok{Lex.TName{}, xx, ll, cc}]) + +# the tokens after the head of a law: `law`, `n` and `:` +def empty.in_law(+ts: List<&2, Lex.Tok>, +ll: U32, +cc: U32) -> List<&2, Lex.Tok>: + Lex.Tok{Lex.TKey{}, "law", ll, cc} <> Lex.Tok{Lex.TName{}, "n", ll, cc} <> Lex.Tok{Lex.TColon{}, ":", ll, cc} <> ts + +# the tokens after the head of a def with no type, which fills a law: +# `def f(s):` +def empty.in_untyped(+ts: List<&2, Lex.Tok>, +ll: U32, +cc: U32) -> List<&2, Lex.Tok>: + Lex.Tok{Lex.TKey{}, "def", ll, cc} <> Lex.Tok{Lex.TName{}, "f", ll, cc} <> Lex.Tok{Lex.TOpen{}, "(", ll, cc} + <> Lex.Tok{Lex.TName{}, "s", ll, cc} <> Lex.Tok{Lex.TClose{}, ")", ll, cc} <> Lex.Tok{Lex.TColon{}, ":", ll, cc} <> ts + +# the tokens after the head of a def that returns a proof: `def f() -> {} :` +def empty.in_proof(+ts: List<&2, Lex.Tok>, +ll: U32, +cc: U32) -> List<&2, Lex.Tok>: + Lex.Tok{Lex.TKey{}, "def", ll, cc} <> Lex.Tok{Lex.TName{}, "f", ll, cc} <> Lex.Tok{Lex.TOpen{}, "(", ll, cc} + <> Lex.Tok{Lex.TClose{}, ")", ll, cc} <> Lex.Tok{Lex.TArrow{}, "->", ll, cc} <> Lex.Tok{Lex.TOpen{}, "{", ll, cc} + <> Lex.Tok{Lex.TClose{}, "}", ll, cc} <> Lex.Tok{Lex.TColon{}, ":", ll, cc} <> ts + +# the tokens after the head of a def that runs: `def f() -> U32:` +def empty.in_typed(+ts: List<&2, Lex.Tok>, +ll: U32, +cc: U32) -> List<&2, Lex.Tok>: + Lex.Tok{Lex.TKey{}, "def", ll, cc} <> Lex.Tok{Lex.TName{}, "f", ll, cc} <> Lex.Tok{Lex.TOpen{}, "(", ll, cc} + <> Lex.Tok{Lex.TClose{}, ")", ll, cc} <> Lex.Tok{Lex.TArrow{}, "->", ll, cc} <> Lex.Tok{Lex.TUpper{}, "U32", ll, cc} + <> Lex.Tok{Lex.TColon{}, ":", ll, cc} <> ts diff --git a/proofs/EmptyExempt.bend b/proofs/EmptyExempt.bend new file mode 100644 index 0000000..9300cc4 --- /dev/null +++ b/proofs/EmptyExempt.bend @@ -0,0 +1,14 @@ +# proofs of laws/EmptyExempt.bend +import Base +import ../src/finding.bend as F +import ../src/rules/tokens.bend as T +import ../src/paths.bend as Paths +import ../src/lazy/lazy.bend as Lazy +import ../src/rules/suspicious/empty.bend as Empty +import ../laws/EmptyExempt.bend as Laws + +def Laws.empty_exempt(path, _text, toks, _tree, _bound, _items, e): + %Equal.sym(Bool, Paths.is_law_file(path), True{}, e) : {Lazy.stop(List<&2, F.Finding>, _, [], + _u => Empty.walk(T.sig(toks), path, False{})) == Nil{} + : List<&2, F.Finding>} + {==} diff --git a/proofs/EmptyReportsKeptTest.bend b/proofs/EmptyReportsKeptTest.bend new file mode 100644 index 0000000..a1da469 --- /dev/null +++ b/proofs/EmptyReportsKeptTest.bend @@ -0,0 +1,52 @@ +# proofs of laws/EmptyReportsKeptTest.bend +import Base +import ../src/syntax/lex.bend as Lex +import ../src/finding.bend as F +import ../src/rules/tokens.bend as T +import ../src/paths.bend as Paths +import ../src/lazy/lazy.bend as Lazy +import ../src/rules/suspicious/empty.bend as Empty +import ../laws/defs/EmptyTests.bend as D1 +import ../laws/EmptyReportsKeptTest.bend as Laws +import ./lemmas/UnsafeStringCompare.bend as M1 + +# what follows the test in the kept sources: `,`, x and `)` +def empty.after(+x: String, +l: U32, +c: U32) -> List<&2, Lex.Tok>: + [Lex.Tok{Lex.TComma{}, ",", l, c}, Lex.Tok{Lex.TName{}, x, l, c}, Lex.Tok{Lex.TClose{}, ")", l, c}] + +# x is read in what follows the test +law empty.kept_x: + for +x: String + for +l: U32 + for +c: U32 + {Empty.kept(empty.after(x, l, c), x, 0n, False{}, True{}) == True{} : Bool} + +def empty.kept_x(x, l, c): + %Equal.sym(Bool, String.eq(x, x), True{}, M1.unsafe.srefl(x)) : + {Empty.kept([Lex.Tok{Lex.TClose{}, ")", l, c}], x, 0n, _, True{}) == True{} : Bool} + {==} + +def Laws.empty_reports_list_kept(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.kept(D1.empty.list_test(x, l, c), x, l, c)), path, False{}))) == 1n : Nat} + %Equal.sym(Bool, Empty.kept(empty.after(x, l, c), x, 0n, False{}, True{}), True{}, empty.kept_x(x, l, c)) : + {List.length(&2, F.Finding, Empty.hit(Empty.tail.go(_, Empty.FList{}, x, l, c), path, Nil{})) == 1n : Nat} + {==} + +def Laws.empty_reports_string_kept(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.kept(D1.empty.str_test(x, l, c), x, l, c)), path, False{}))) == 1n : Nat} + %Equal.sym(Bool, Empty.kept(empty.after(x, l, c), x, 0n, False{}, True{}), True{}, empty.kept_x(x, l, c)) : + {List.length(&2, F.Finding, Empty.hit(Empty.tail.go(_, Empty.FStr{}, x, l, c), path, Nil{})) == 1n : Nat} + {==} + +def Laws.empty_reports_in_typed_def(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.in_typed(D1.empty.kept(D1.empty.list_test(x, l, c), x, l, c), l, c)), path, + False{}))) == 1n : Nat} + %Equal.sym(Bool, Empty.kept(empty.after(x, l, c), x, 0n, False{}, True{}), True{}, empty.kept_x(x, l, c)) : + {List.length(&2, F.Finding, Empty.hit(Empty.tail.go(_, Empty.FList{}, x, l, c), path, Nil{})) == 1n : Nat} + {==} diff --git a/proofs/EmptySkipsProofs.bend b/proofs/EmptySkipsProofs.bend new file mode 100644 index 0000000..143d1d0 --- /dev/null +++ b/proofs/EmptySkipsProofs.bend @@ -0,0 +1,31 @@ +# proofs of laws/EmptySkipsProofs.bend +import Base +import ../src/syntax/lex.bend as Lex +import ../src/finding.bend as F +import ../src/rules/tokens.bend as T +import ../src/paths.bend as Paths +import ../src/lazy/lazy.bend as Lazy +import ../src/rules/suspicious/empty.bend as Empty +import ../laws/defs/EmptyTests.bend as D1 +import ../laws/EmptySkipsProofs.bend as Laws + +def Laws.empty_skips_in_law(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.in_law(D1.empty.kept(D1.empty.list_test(x, l, c), x, l, c), l, c)), path, + False{}))) == 0n : Nat} + {==} + +def Laws.empty_skips_in_untyped_def(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.in_untyped(D1.empty.kept(D1.empty.list_test(x, l, c), x, l, c), l, c)), path, + False{}))) == 0n : Nat} + {==} + +def Laws.empty_skips_in_proof_def(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.in_proof(D1.empty.kept(D1.empty.list_test(x, l, c), x, l, c), l, c)), path, + False{}))) == 0n : Nat} + {==} diff --git a/proofs/EmptySkipsUnkeptTest.bend b/proofs/EmptySkipsUnkeptTest.bend new file mode 100644 index 0000000..59d25f4 --- /dev/null +++ b/proofs/EmptySkipsUnkeptTest.bend @@ -0,0 +1,46 @@ +# proofs of laws/EmptySkipsUnkeptTest.bend +import Base +import ../src/syntax/lex.bend as Lex +import ../src/finding.bend as F +import ../src/rules/tokens.bend as T +import ../src/paths.bend as Paths +import ../src/lazy/lazy.bend as Lazy +import ../src/rules/suspicious/empty.bend as Empty +import ../laws/defs/EmptyTests.bend as D1 +import ../laws/EmptySkipsUnkeptTest.bend as Laws + +def Laws.empty_skips_list_dropped(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.dropped(D1.empty.list_test(x, l, c), l, c)), path, False{}))) == 0n : Nat} + {==} + +def Laws.empty_skips_string_dropped(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.dropped(D1.empty.str_test(x, l, c), l, c)), path, False{}))) == 0n : Nat} + {==} + +def Laws.empty_skips_list_before(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.before(D1.empty.list_test(x, l, c), x, l, c)), path, False{}))) == 0n : Nat} + {==} + +def Laws.empty_skips_string_before(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.before(D1.empty.str_test(x, l, c), x, l, c)), path, False{}))) == 0n : Nat} + {==} + +def Laws.empty_skips_list_bare(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.bare(D1.empty.list_test(x, l, c), x, l, c)), path, False{}))) == 0n : Nat} + {==} + +def Laws.empty_skips_string_bare(path, e, x, l, c, _text, _tree, _bound, _items): + %Equal.sym(Bool, Paths.is_law_file(path), False{}, e) : {List.length(&2, F.Finding, Lazy.stop(List<&2, F.Finding>, + _, [], + _u => Empty.walk(T.sig(D1.empty.bare(D1.empty.str_test(x, l, c), x, l, c)), path, False{}))) == 0n : Nat} + {==} diff --git a/proofs/InertEmpty.bend b/proofs/InertEmpty.bend new file mode 100644 index 0000000..9ebdbf3 --- /dev/null +++ b/proofs/InertEmpty.bend @@ -0,0 +1,625 @@ +# proofs of laws/InertEmpty.bend +import Base +import ../src/syntax/lex.bend as Lex +import ../src/finding.bend as F +import ../src/rules/tokens.bend as T +import ../src/paths.bend as Paths +import ../src/lazy/lazy.bend as Lazy +import ../src/rules/suspicious/empty.bend as Empty +import ../laws/InertEmpty.bend as Laws +import ../laws/defs/InertText.bend as D1 +import ./lemmas/InertTextFacts.bend as M1 + +# a found name with the tokens after it read that way +def inert.empty.taken(mm: Maybe<&2, Empty.Taken>) -> Maybe<&2, Empty.Taken>: + match mm: + case None{}: + None{} + case Some{Empty.Taken{x, r}}: + Some{Empty.Taken{x, D1.inert.toks(r)}} + +# a token's text read that way is the same code: a comment or a string is +# none either way, anything else is kept as it is +law inert.empty.code: + for k: Lex.TokKind + for +t: String + {Empty.code(k, D1.inert.keep(D1.inert.blanks(k), t)) == Empty.code(k, t) : String} + +def inert.empty.code(k, _t): + match k: + case Lex.TName{}: + {==} + case Lex.TUpper{}: + {==} + case Lex.TDotted{}: + {==} + case Lex.TWild{}: + {==} + case Lex.TKey{}: + {==} + case Lex.TNum{}: + {==} + case Lex.TStr{}: + {==} + case Lex.TChar{}: + {==} + case Lex.TComment{}: + {==} + case Lex.TSpace{}: + {==} + case Lex.TNewline{}: + {==} + case Lex.TOp{}: + {==} + case Lex.TColon{}: + {==} + case Lex.TEq{}: + {==} + case Lex.TBind{}: + {==} + case Lex.TArrow{}: + {==} + case Lex.TLam{}: + {==} + case Lex.TAll{}: + {==} + case Lex.TAmp{}: + {==} + case Lex.TOpen{}: + {==} + case Lex.TClose{}: + {==} + case Lex.TComma{}: + {==} + +# the last tokens of a length's arguments are what they were +law inert.empty.last: + for k: Lex.TokKind + for +t: String + for +ll: Empty.Last + {Empty.last.step(k, D1.inert.keep(D1.inert.blanks(k), t), ll) == Empty.last.step(k, t, ll) : Empty.Last} + +def inert.empty.last(k, _t, _ll): + match k: + case Lex.TName{}: + {==} + case Lex.TUpper{}: + {==} + case Lex.TDotted{}: + {==} + case Lex.TWild{}: + {==} + case Lex.TKey{}: + {==} + case Lex.TNum{}: + {==} + case Lex.TStr{}: + {==} + case Lex.TChar{}: + {==} + case Lex.TComment{}: + {==} + case Lex.TSpace{}: + {==} + case Lex.TNewline{}: + {==} + case Lex.TOp{}: + {==} + case Lex.TColon{}: + {==} + case Lex.TEq{}: + {==} + case Lex.TBind{}: + {==} + case Lex.TArrow{}: + {==} + case Lex.TLam{}: + {==} + case Lex.TAll{}: + {==} + case Lex.TAmp{}: + {==} + case Lex.TOpen{}: + {==} + case Lex.TClose{}: + {==} + case Lex.TComma{}: + {==} + +# the name a length's arguments end in, before tokens read that way +law inert.empty.name: + for +ll: Empty.Last + for r: List<&2, Lex.Tok> + {Empty.last.name(ll, D1.inert.toks(r)) == inert.empty.taken(Empty.last.name(ll, r)) : Maybe<&2, Empty.Taken>} + +def inert.empty.name(ll, _r): + match ll: + case Empty.LComma{}: + {==} + case Empty.LName{_n}: + {==} + case Empty.LOther{}: + {==} + +# a pick of that name, or none +law inert.empty.name_pick: + for h: Bool + for +ll: Empty.Last + for r: List<&2, Lex.Tok> + {Bool.pick(Maybe<&2, Empty.Taken>, h, Empty.last.name(ll, D1.inert.toks(r)), None{}) + == inert.empty.taken(Bool.pick(Maybe<&2, Empty.Taken>, h, Empty.last.name(ll, r), None{})) : Maybe<&2, Empty.Taken>} + +def inert.empty.name_pick(h, ll, r): + match h: + case True{}: + inert.empty.name(ll, r) + case False{}: + {==} + +# whether x is kept does not read what a comment or string says +law inert.empty.kept: + for ts: List<&2, Lex.Tok> + for +x: String + for +d: Nat + for found: Bool + for live: Bool + {Empty.kept(D1.inert.toks(ts), x, d, found, live) == Empty.kept(ts, x, d, found, live) : Bool} + +def inert.empty.kept(ts, x, d, found, live): + match ts: + case Nil{}: + {==} + case Con{Lex.Tok{+k, +t, +l, +c}, +rest}: + match found: + case True{}: + {==} + case False{}: + match live: + case False{}: + {==} + case True{}: + +dep = Empty.close.depth(k, d) + +nh = Bool.not(Empty.close.here(k, d)) + +ck = Empty.code(k, D1.inert.keep(D1.inert.blanks(k), t)) + %inert.empty.code(k, t) : {Empty.kept(D1.inert.toks(rest), x, dep, Bool.and(Empty.plain(k), + String.eq(ck, x)), nh) + == Empty.kept(rest, x, dep, Bool.and(Empty.plain(k), String.eq(_, x)), nh) : Bool} + inert.empty.kept(rest, x, dep, Bool.and(Empty.plain(k), String.eq(ck, x)), nh) + +# a List.length's arguments end in the same name, the tokens after it read +# that way +law inert.empty.list: + for ts: List<&2, Lex.Tok> + for +d: Nat + for +ll: Empty.Last + for done: Bool + for got: Maybe<&2, Empty.Taken> + {Empty.close.list(D1.inert.toks(ts), d, ll, done, inert.empty.taken(got)) + == inert.empty.taken(Empty.close.list(ts, d, ll, done, got)) : Maybe<&2, Empty.Taken>} + +def inert.empty.list(ts, d, ll, done, _got): + match ts: + case Nil{}: + {==} + case Con{Lex.Tok{+k, +t, +l, +c}, +rest}: + match done: + case True{}: + {==} + case False{}: + +dep = Empty.close.depth(k, d) + +h = Empty.close.here(k, d) + +lk = Empty.last.step(k, D1.inert.keep(D1.inert.blanks(k), t), ll) + +ls = Empty.last.step(k, t, ll) + +pk = Bool.pick(Maybe<&2, Empty.Taken>, h, Empty.last.name(ll, D1.inert.toks(rest)), None{}) + +ps = Bool.pick(Maybe<&2, Empty.Taken>, h, Empty.last.name(ll, rest), None{}) + +rhs = inert.empty.taken(Empty.close.list(rest, dep, ls, h, ps)) + %Equal.sym(Empty.Last, lk, ls, inert.empty.last(k, t, ll)) : + {Empty.close.list(D1.inert.toks(rest), dep, _, h, pk) == rhs : Maybe<&2, Empty.Taken>} + %Equal.sym(Maybe<&2, Empty.Taken>, pk, inert.empty.taken(ps), inert.empty.name_pick(h, ll, rest)) : + {Empty.close.list(D1.inert.toks(rest), dep, ls, h, _) == rhs : Maybe<&2, Empty.Taken>} + inert.empty.list(rest, dep, ls, h, ps) + +# a pick of a found name, the tokens after it read that way +law inert.empty.found: + for b: Bool + for +y: String + for r: List<&2, Lex.Tok> + {Bool.pick(Maybe<&2, Empty.Taken>, b, Some{Empty.Taken{y, D1.inert.toks(r)}}, None{}) + == inert.empty.taken(Bool.pick(Maybe<&2, Empty.Taken>, b, Some{Empty.Taken{y, r}}, + None{})) : Maybe<&2, Empty.Taken>} + +def inert.empty.found(b, _y, _r): + match b: + case True{}: + {==} + case False{}: + {==} + +# a String.length's argument is the same name, the tokens after it read +# that way +law inert.empty.str: + for ts: List<&2, Lex.Tok> + {Empty.close.str(D1.inert.toks(ts)) == inert.empty.taken(Empty.close.str(ts)) : Maybe<&2, Empty.Taken>} + +def inert.empty.str(ts): + match ts: + case Nil{}: + {==} + case Con{Lex.Tok{+k1, +t1, +l1, +c1}, +r1}: + match r1: + case Nil{}: + {==} + case Con{Lex.Tok{+k2, +t2, +l2, +c2}, +rest}: + +c1k = Empty.code(k1, D1.inert.keep(D1.inert.blanks(k1), t1)) + +c2k = Empty.code(k2, D1.inert.keep(D1.inert.blanks(k2), t2)) + +rhs = inert.empty.taken(Bool.pick(Maybe<&2, Empty.Taken>, Bool.and(Empty.plain(k1), + String.eq(Empty.code(k2, t2), ")")), + Some{Empty.Taken{Empty.code(k1, t1), rest}}, None{})) + %Equal.sym(String, c1k, Empty.code(k1, t1), inert.empty.code(k1, t1)) : + {Bool.pick(Maybe<&2, Empty.Taken>, Bool.and(Empty.plain(k1), String.eq(c2k, ")")), + Some{Empty.Taken{_, D1.inert.toks(rest)}}, None{}) == rhs : Maybe<&2, Empty.Taken>} + %Equal.sym(String, c2k, Empty.code(k2, t2), inert.empty.code(k2, t2)) : + {Bool.pick(Maybe<&2, Empty.Taken>, Bool.and(Empty.plain(k1), String.eq(_, ")")), + Some{Empty.Taken{Empty.code(k1, t1), D1.inert.toks(rest)}}, None{}) == rhs : Maybe<&2, Empty.Taken>} + inert.empty.found(Bool.and(Empty.plain(k1), String.eq(Empty.code(k2, t2), ")")), Empty.code(k1, t1), rest) + +# a length's argument is the same name, the tokens after it read that way +law inert.empty.taken_of: + for +fm: Empty.Form + for ts: List<&2, Lex.Tok> + {Empty.taken(fm, D1.inert.toks(ts)) == inert.empty.taken(Empty.taken(fm, ts)) : Maybe<&2, Empty.Taken>} + +def inert.empty.taken_of(fm, ts): + match fm: + case Empty.FList{}: + inert.empty.list(ts, 0n, Empty.LOther{}, False{}, None{}) + case Empty.FStr{}: + inert.empty.str(ts) + case Empty.FNone{}: + {==} + +# the test's end and the read of x after it give the same finding +law inert.empty.tail: + for mm: Maybe<&2, Empty.Taken> + for +fm: Empty.Form + for +l: U32 + for +c: U32 + {Empty.tail(inert.empty.taken(mm), fm, l, c) == Empty.tail(mm, fm, l, c) : Maybe<&2, Empty.Hit>} + +def inert.empty.tail(mm, fm, l, c): + match mm: + case None{}: + {==} + case Some{Empty.Taken{+x, +r}}: + match r: + case Nil{}: + {==} + case Con{Lex.Tok{+k1, +t1, +l1, +c1}, +r1}: + match r1: + case Nil{}: + {==} + case Con{Lex.Tok{+k2, +t2, +l2, +c2}, +r2}: + match r2: + case Nil{}: + {==} + case Con{Lex.Tok{+k3, +t3, +l3, +c3}, +rest}: + +s1 = Empty.code(k1, t1) + +s2 = Empty.code(k2, t2) + +s3 = Empty.code(k3, t3) + +rhs = Empty.tail.go(Bool.and(String.eq(s1, ","), Bool.and(String.eq(s2, "0n"), Bool.and(String.eq(s3, + ")"), + Empty.kept(rest, x, 0n, False{}, True{})))), fm, x, l, c) + %Equal.sym(String, Empty.code(k1, D1.inert.keep(D1.inert.blanks(k1), t1)), s1, inert.empty.code(k1, + t1)) : + {Empty.tail.go(Bool.and(String.eq(_, ","), Bool.and(String.eq(Empty.code(k2, + D1.inert.keep(D1.inert.blanks(k2), t2)), "0n"), + Bool.and(String.eq(Empty.code(k3, D1.inert.keep(D1.inert.blanks(k3), t3)), ")"), + Empty.kept(D1.inert.toks(rest), x, 0n, False{}, + True{})))), fm, x, l, c) == rhs : Maybe<&2, Empty.Hit>} + %Equal.sym(String, Empty.code(k2, D1.inert.keep(D1.inert.blanks(k2), t2)), s2, inert.empty.code(k2, + t2)) : + {Empty.tail.go(Bool.and(String.eq(s1, ","), Bool.and(String.eq(_, "0n"), + Bool.and(String.eq(Empty.code(k3, D1.inert.keep(D1.inert.blanks(k3), t3)), ")"), + Empty.kept(D1.inert.toks(rest), x, 0n, False{}, + True{})))), fm, x, l, c) == rhs : Maybe<&2, Empty.Hit>} + %Equal.sym(String, Empty.code(k3, D1.inert.keep(D1.inert.blanks(k3), t3)), s3, inert.empty.code(k3, + t3)) : + {Empty.tail.go(Bool.and(String.eq(s1, ","), Bool.and(String.eq(s2, "0n"), Bool.and(String.eq(_, ")"), + Empty.kept(D1.inert.toks(rest), x, 0n, False{}, + True{})))), fm, x, l, c) == rhs : Maybe<&2, Empty.Hit>} + %Equal.sym(Bool, Empty.kept(D1.inert.toks(rest), x, 0n, False{}, True{}), Empty.kept(rest, x, 0n, + False{}, True{}), + inert.empty.kept(rest, x, 0n, False{}, True{})) : + {Empty.tail.go(Bool.and(String.eq(s1, ","), Bool.and(String.eq(s2, "0n"), Bool.and(String.eq(s3, ")"), + _))), + fm, x, l, c) == rhs : Maybe<&2, Empty.Hit>} + {==} + +# the test, its head read, gives the same finding +law inert.empty.at_go: + for ok: Bool + for +fm: Empty.Form + for +l: U32 + for +c: U32 + for +r: List<&2, Lex.Tok> + {Empty.at.go(ok, fm, l, c, D1.inert.toks(r)) == Empty.at.go(ok, fm, l, c, r) : Maybe<&2, Empty.Hit>} + +def inert.empty.at_go(ok, fm, l, c, r): + match ok: + case True{}: + %Equal.sym(Maybe<&2, Empty.Taken>, Empty.taken(fm, D1.inert.toks(r)), inert.empty.taken(Empty.taken(fm, r)), + inert.empty.taken_of(fm, r)) : + {Empty.tail(_, fm, l, c) == Empty.tail(Empty.taken(fm, r), fm, l, c) : Maybe<&2, Empty.Hit>} + inert.empty.tail(Empty.taken(fm, r), fm, l, c) + case False{}: + {==} + +# a token's kind, then tokens read that way: the same kept test, if any +law inert.empty.at: + for k0: Lex.TokKind + for ts: List<&2, Lex.Tok> + {Empty.at(k0, D1.inert.toks(ts)) == Empty.at(k0, ts) : Maybe<&2, Empty.Hit>} + +def inert.empty.at(k0, ts): + match ts: + case Nil{}: + {==} + case Con{Lex.Tok{+k1, +t1, +l1, +c1}, +r1}: + match r1: + case Nil{}: + {==} + case Con{Lex.Tok{+k2, +t2, +l2, +c2}, +r2}: + match r2: + case Nil{}: + {==} + case Con{Lex.Tok{+k3, +t3, +l3, +c3}, +r3}: + match r3: + case Nil{}: + {==} + case Con{Lex.Tok{+k4, +t4, +l4, +c4}, +r4}: + +q1 = Empty.code(k1, D1.inert.keep(D1.inert.blanks(k1), t1)) + +q2 = Empty.code(k2, D1.inert.keep(D1.inert.blanks(k2), t2)) + +q3 = Empty.code(k3, D1.inert.keep(D1.inert.blanks(k3), t3)) + +q4 = Empty.code(k4, D1.inert.keep(D1.inert.blanks(k4), t4)) + +ok = Bool.and(Empty.opener(k0), Bool.and(Empty.dotted(k1), Bool.and(Empty.dotted(k3), + Bool.and(String.eq(q1, "Nat.is_eq"), Bool.and(String.eq(q2, "("), String.eq(q4, "(")))))) + +lhs = Empty.at.go(ok, Empty.form(q3), l1, c1, D1.inert.toks(r4)) + %inert.empty.code(k1, t1) : {lhs == Empty.at.go(Bool.and(Empty.opener(k0), Bool.and(Empty.dotted(k1), + Bool.and(Empty.dotted(k3), Bool.and(String.eq(_, "Nat.is_eq"), Bool.and(String.eq(Empty.code(k2, t2), "("), + String.eq(Empty.code(k4, t4), + "(")))))), Empty.form(Empty.code(k3, t3)), l1, c1, r4) : Maybe<&2, Empty.Hit>} + %inert.empty.code(k2, t2) : {lhs == Empty.at.go(Bool.and(Empty.opener(k0), Bool.and(Empty.dotted(k1), + Bool.and(Empty.dotted(k3), Bool.and(String.eq(q1, "Nat.is_eq"), Bool.and(String.eq(_, "("), + String.eq(Empty.code(k4, t4), + "(")))))), Empty.form(Empty.code(k3, t3)), l1, c1, r4) : Maybe<&2, Empty.Hit>} + %inert.empty.code(k4, t4) : {lhs == Empty.at.go(Bool.and(Empty.opener(k0), Bool.and(Empty.dotted(k1), + Bool.and(Empty.dotted(k3), Bool.and(String.eq(q1, "Nat.is_eq"), Bool.and(String.eq(q2, "("), + String.eq(_, "(")))))), Empty.form(Empty.code(k3, t3)), l1, c1, r4) : Maybe<&2, Empty.Hit>} + %inert.empty.code(k3, t3) : {lhs == Empty.at.go(ok, Empty.form(_), l1, c1, r4) : Maybe<&2, Empty.Hit>} + inert.empty.at_go(ok, Empty.form(q3), l1, c1, r4) + +# what follows a def's parameters says the same +law inert.empty.head: + for k1: Lex.TokKind + for +k2: Lex.TokKind + for +t2: String + {Empty.proofy.head(k1, k2, D1.inert.keep(D1.inert.blanks(k2), t2)) == Empty.proofy.head(k1, k2, t2) : Bool} + +def inert.empty.head(k1, k2, t2): + match k1: + case Lex.TName{}: + {==} + case Lex.TUpper{}: + {==} + case Lex.TDotted{}: + {==} + case Lex.TWild{}: + {==} + case Lex.TKey{}: + {==} + case Lex.TNum{}: + {==} + case Lex.TStr{}: + {==} + case Lex.TChar{}: + {==} + case Lex.TComment{}: + {==} + case Lex.TSpace{}: + {==} + case Lex.TNewline{}: + {==} + case Lex.TOp{}: + {==} + case Lex.TColon{}: + {==} + case Lex.TEq{}: + {==} + case Lex.TBind{}: + {==} + case Lex.TArrow{}: + %inert.empty.code(k2, t2) : {String.eq(Empty.code(k2, D1.inert.keep(D1.inert.blanks(k2), t2)), + "{") == String.eq(_, "{") : Bool} + {==} + case Lex.TLam{}: + {==} + case Lex.TAll{}: + {==} + case Lex.TAmp{}: + {==} + case Lex.TOpen{}: + {==} + case Lex.TClose{}: + {==} + case Lex.TComma{}: + {==} + +# a def's header ends the same way +law inert.empty.end: + for ts: List<&2, Lex.Tok> + {Empty.proofy.end(D1.inert.toks(ts)) == Empty.proofy.end(ts) : Bool} + +def inert.empty.end(ts): + match ts: + case Nil{}: + {==} + case Con{Lex.Tok{+k1, +t1, +l1, +c1}, +r1}: + match r1: + case Nil{}: + {==} + case Con{Lex.Tok{+k2, +t2, +l2, +c2}, +rest}: + inert.empty.head(k1, k2, t2) + +# a def is a proof or not the same way +law inert.empty.proofy: + for ts: List<&2, Lex.Tok> + for +d: Nat + for fin: Bool + {Empty.proofy(D1.inert.toks(ts), d, fin) == Empty.proofy(ts, d, fin) : Bool} + +def inert.empty.proofy(ts, d, fin): + match ts: + case Nil{}: + {==} + case Con{Lex.Tok{+k, +t, +l, +c}, +rest}: + match fin: + case True{}: + inert.empty.end(Lex.Tok{k, t, l, c} <> rest) + case False{}: + inert.empty.proofy(rest, Empty.close.depth(k, d), Empty.proofy.fin(k, d)) + +# what a keyword leaves skipped is the same +law inert.empty.word: + for isdef: Bool + for +word: String + for rest: List<&2, Lex.Tok> + for skip: Bool + {Empty.item.word(isdef, word, D1.inert.toks(rest), skip) == Empty.item.word(isdef, word, rest, skip) : Bool} + +def inert.empty.word(isdef, _word, rest, _skip): + match isdef: + case True{}: + inert.empty.proofy(rest, 0n, False{}) + case False{}: + {==} + +# what a token leaves skipped is the same +law inert.empty.item: + for k: Lex.TokKind + for +t: String + for rest: List<&2, Lex.Tok> + for skip: Bool + {Empty.item(k, D1.inert.keep(D1.inert.blanks(k), t), D1.inert.toks(rest), skip) == Empty.item(k, t, rest, + skip) : Bool} + +def inert.empty.item(k, t, rest, skip): + match k: + case Lex.TName{}: + {==} + case Lex.TUpper{}: + {==} + case Lex.TDotted{}: + {==} + case Lex.TWild{}: + {==} + case Lex.TKey{}: + inert.empty.word(String.eq(t, "def"), t, rest, skip) + case Lex.TNum{}: + {==} + case Lex.TStr{}: + {==} + case Lex.TChar{}: + {==} + case Lex.TComment{}: + {==} + case Lex.TSpace{}: + {==} + case Lex.TNewline{}: + {==} + case Lex.TOp{}: + {==} + case Lex.TColon{}: + {==} + case Lex.TEq{}: + {==} + case Lex.TBind{}: + {==} + case Lex.TArrow{}: + {==} + case Lex.TLam{}: + {==} + case Lex.TAll{}: + {==} + case Lex.TAmp{}: + {==} + case Lex.TOpen{}: + {==} + case Lex.TClose{}: + {==} + case Lex.TComma{}: + {==} + +# the test a token opens, outside what is skipped, is the same +law inert.empty.opens: + for sk: Bool + for k: Lex.TokKind + for rest: List<&2, Lex.Tok> + {Empty.found(sk, k, D1.inert.toks(rest)) == Empty.found(sk, k, rest) : Maybe<&2, Empty.Hit>} + +def inert.empty.opens(sk, k, rest): + match sk: + case True{}: + {==} + case False{}: + inert.empty.at(k, rest) + +# the walk finds the same tests in tokens read that way +law inert.empty.walk: + for ts: List<&2, Lex.Tok> + for +path: String + for +skip: Bool + {Empty.walk(D1.inert.toks(ts), path, skip) == Empty.walk(ts, path, skip) : List<&2, F.Finding>} + +def inert.empty.walk(ts, path, skip): + match ts: + case Nil{}: + {==} + case Con{Lex.Tok{+k, +t, +l, +c}, +rest}: + +sk = Empty.item(k, t, rest, skip) + %Equal.sym(Bool, Empty.item(k, D1.inert.keep(D1.inert.blanks(k), t), D1.inert.toks(rest), skip), sk, + inert.empty.item(k, t, rest, skip)) : + {Empty.hit(Empty.found(_, k, D1.inert.toks(rest)), path, Empty.walk(D1.inert.toks(rest), path, _)) + == Empty.hit(Empty.found(sk, k, rest), path, Empty.walk(rest, path, sk)) : List<&2, F.Finding>} + %Equal.sym(Maybe<&2, Empty.Hit>, Empty.found(sk, k, D1.inert.toks(rest)), Empty.found(sk, k, rest), + inert.empty.opens(sk, k, rest)) : + {Empty.hit(_, path, Empty.walk(D1.inert.toks(rest), path, sk)) + == Empty.hit(Empty.found(sk, k, rest), path, Empty.walk(rest, path, sk)) : List<&2, F.Finding>} + %Equal.sym(List<&2, F.Finding>, Empty.walk(D1.inert.toks(rest), path, sk), Empty.walk(rest, path, sk), + inert.empty.walk(rest, path, sk)) : + {Empty.hit(Empty.found(sk, k, rest), path, _) == Empty.hit(Empty.found(sk, k, rest), path, Empty.walk(rest, + path, sk)) + : List<&2, F.Finding>} + {==} + +# the walk of the significant tokens reads no comment or string +law inert.empty.on: + for +ts: List<&2, Lex.Tok> + for +path: String + {Empty.walk(T.sig(D1.inert.toks(ts)), path, False{}) == Empty.walk(T.sig(ts), path, False{}) : List<&2, F.Finding>} + +def inert.empty.on(ts, path): + +s = T.sig(ts) + %Equal.sym(List<&2, Lex.Tok>, T.sig(D1.inert.toks(ts)), D1.inert.toks(s), M1.inert.put.sig(ts)) : + {Empty.walk(_, path, False{}) == Empty.walk(s, path, False{}) : List<&2, F.Finding>} + inert.empty.walk(s, path, False{}) + +def Laws.inert_empty(path, _text, toks, _tree, _bound, _items, _text2, toks2, _tree2, _bound2, _items2, e): + M1.inert.via(List<&2, Lex.Tok>, z => Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], + _u => Empty.walk(T.sig(z), path, False{})), toks, toks2, D1.inert.toks(toks), D1.inert.toks(toks2), + Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, w => Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), + [], _u => w), Empty.walk(T.sig(D1.inert.toks(toks)), path, False{}), Empty.walk(T.sig(toks), path, False{}), + inert.empty.on(toks, path)), + Equal.cong(List<&2, F.Finding>, List<&2, F.Finding>, w => Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), + [], _u => w), Empty.walk(T.sig(D1.inert.toks(toks2)), path, False{}), Empty.walk(T.sig(toks2), path, False{}), + inert.empty.on(toks2, path)), + e) diff --git a/proofs/OutputCodesMapOneToOne.bend b/proofs/OutputCodesMapOneToOne.bend index f2e8e3a..c267e84 100644 --- a/proofs/OutputCodesMapOneToOne.bend +++ b/proofs/OutputCodesMapOneToOne.bend @@ -2,7 +2,7 @@ import Base import ../laws/OutputCodesMapOneToOne.bend as Laws -# one arm per row of the code table (35), each checked by evaluation, and one +# one arm per row of the code table (36), each checked by evaluation, and one # past its end, where both sides are none: a new rule is a new arm here def Laws.slug_finds_row(n): match n: @@ -78,7 +78,9 @@ def Laws.slug_finds_row(n): {==} case 35n: {==} - case 36n+_p: + case 36n: + {==} + case 37n+_p: {==} # the same arms, looked up by code @@ -156,5 +158,7 @@ def Laws.code_finds_row(n): {==} case 35n: {==} - case 36n+_p: + case 36n: + {==} + case 37n+_p: {==} diff --git a/proofs/RoleEmpty.bend b/proofs/RoleEmpty.bend new file mode 100644 index 0000000..d08328a --- /dev/null +++ b/proofs/RoleEmpty.bend @@ -0,0 +1,17 @@ +# proofs of laws/RoleEmpty.bend +import Base +import ../src/finding.bend as F +import ../src/rules/tokens.bend as T +import ../src/paths.bend as Paths +import ../src/role.bend as Role +import ../src/lazy/lazy.bend as Lazy +import ../src/rules/suspicious/empty.bend as Empty +import ../laws/RoleEmpty.bend as Laws +import ../laws/RoleLawFileNamed.bend as L1 +import ./lemmas/RoleLawFilePicked.bend as M1 + +def Laws.role_empty(path, _text, toks, _tree, _bound, _items): + Equal.cong(Bool, List<&2, F.Finding>, + z => Lazy.stop(List<&2, F.Finding>, z, [], _u => Empty.walk(T.sig(toks), path, False{})), + Role.is_law_file(Role.of_path(path)), Paths.is_law_file(path), + L1.role_law_file_named(path)) diff --git a/proofs/RoleEmptyExempt.bend b/proofs/RoleEmptyExempt.bend new file mode 100644 index 0000000..e21bda3 --- /dev/null +++ b/proofs/RoleEmptyExempt.bend @@ -0,0 +1,10 @@ +# proofs of laws/RoleEmptyExempt.bend +import Base +import ../src/rules/tokens.bend as T +import ../src/role.bend as Role +import ../src/rules/suspicious/empty.bend as Empty +import ../laws/RoleEmptyExempt.bend as Laws +import ./lemmas/LawFileExemptions.bend as M1 + +def Laws.role_empty_exempt(rr, e, path, _text, toks, _tree, _bound, _items): + M1.ex.stop(Role.is_law_file(rr), e, _u => Empty.walk(T.sig(toks), path, False{})) diff --git a/src/README.md b/src/README.md index e4b3d0b..6feb181 100644 --- a/src/README.md +++ b/src/README.md @@ -51,7 +51,7 @@ unset group has its default. The groups: | group | rules | default | |---------------|----------------------------------------------------------------------------------|---------| | `correctness` | `hole` `pick` `put` `arms` `escape` `twice` `strings` `chars` `foreign` `setting` | error | -| `suspicious` | `unused` `strict` `eager` `concat` `fuel` `index` `table` `hoist` `ring` `rewalk` `unit` `fromrev` `prefix` (`scan`, `thunk`: opt-in) | warn | +| `suspicious` | `unused` `strict` `eager` `concat` `fuel` `index` `table` `hoist` `ring` `rewalk` `unit` `fromrev` `prefix` `empty` (`scan`, `thunk`: opt-in) | warn | | `style` | `doc` `space` `wrap` `param` `noqa` (`transcong`: opt-in) | warn | | `laws` | `coverage` `closed` `unsafe` | warn | | `pedantic` | `tail` | off | @@ -77,6 +77,7 @@ The stable codes, assigned once (do not renumber): | | | U015 | `thunk` | | | | | | U016 | `fromrev` | | | | | | U017 | `prefix` | | | +| | | U018 | `empty` | | | Letters: `C` correctness, `U` suspicious, `S` style, `L` laws, `P` pedantic. @@ -397,6 +398,26 @@ parameters and no `->`), which is how Bend fills the law named `f`. another length is a different bug and is left alone, and so is a qualified or aliased name and a non-literal on the other side. A law file or a proof file is exempt. +- `empty` — `Nat.is_eq(List.length(.., x), 0n)` or + `Nat.is_eq(String.length(x), 0n)` as an argument (right after a `(`, `[`, + `{` or `,`), x a plain name read again after it in the same group: among + the significant tokens, a dotted `Nat.is_eq`, `(`, then a dotted + `List.length`, `(`, tokens up to its matching `)` whose last two are `,` + and x, or a dotted `String.length`, `(`, x and `)`; then `,`, `0n` and + `)`; then x as a plain name before the bracket that closes the group. + One finding on `Nat.is_eq`. Base's lengths count every cell (and are not + tail calls); `List.is_empty(.., x)` and `String.is_empty(x)` take the same + arguments, look at one cell and give the same Bool. Only a kept x is + reported, because only then does the fix pay on both lanes: the native + lane frees a list the program never walked more slowly than it walks one, + so where the test is x's last use the walk is the cheaper way to free it + (bend 2.0.38, a 0-1000 char String: kept 1.57x faster native and 1.31x + JS; dropped 0.27x native, 1.65x JS). A test whose group reads no x after + it, one that reads x only before it, and one outside any group (`v = + Nat.is_eq(..)`) are left alone. A law file or a proof file is exempt, and + so is a `law` and a def that is a proof (`def f(x):`, or one that returns + `-> {..}`) in any file: from its keyword to the next `def`, `type` or + `import`. - `put` — `Map.put`. It is Base's internal helper: at a leaf it keeps the old key and replaces the value without comparing, so a new key silently overwrites another entry. `Map.set` compares. A file that defines diff --git a/src/codes.bend b/src/codes.bend index a6fbd84..d95b54e 100644 --- a/src/codes.bend +++ b/src/codes.bend @@ -43,6 +43,7 @@ def table() -> List<&2, Entry>: Entry{"thunk", "U015", "suspicious"}, Entry{"fromrev", "U016", "suspicious"}, Entry{"prefix", "U017", "suspicious"}, + Entry{"empty", "U018", "suspicious"}, Entry{"doc", "S001", "style"}, Entry{"space", "S002", "style"}, Entry{"wrap", "S003", "style"}, diff --git a/src/rules.bend b/src/rules.bend index 09a0343..c780097 100644 --- a/src/rules.bend +++ b/src/rules.bend @@ -46,6 +46,7 @@ import ./rules/suspicious/scan.bend as Scan import ./rules/suspicious/thunk.bend as Thunk import ./rules/suspicious/fromrev.bend as Fromrev import ./rules/suspicious/prefix.bend as Prefix +import ./rules/suspicious/empty.bend as Empty import ./rules/correctness/put.bend as Put import ./rules/correctness/escape.bend as Escape import ./rules/correctness/strings.bend as Strings @@ -73,7 +74,7 @@ def on.at(+path: String, fs: List<&2, F.Finding>) -> List<&2, F.Finding>: # every per-file rule on a file, told its role (src/role.bend): the rules a # law or proof file changes (doc, hole, param, scan, fromrev, prefix, -# closed) read the role, never the path, and the cost rules check nothing +# empty, closed) read the role, never the path, and the cost rules check nothing # in a law or proof file def on.rules.role(+rr: Role.Role, +ss: Src.Src) -> List<&2, F.Finding>: List.concat(&2, F.Finding, [ @@ -100,6 +101,7 @@ def on.rules.role(+rr: Role.Role, +ss: Src.Src) -> List<&2, F.Finding>: Role.skip(rr, _u => Thunk.check(ss)), Fromrev.check.role(rr, ss), Prefix.check.role(rr, ss), + Empty.check.role(rr, ss), Put.check(ss), Escape.check(ss), Strings.check(ss), diff --git a/src/rules/imports.bend b/src/rules/imports.bend index dfee61d..6e23295 100644 --- a/src/rules/imports.bend +++ b/src/rules/imports.bend @@ -45,7 +45,7 @@ def init(segs: List<&2, String>) -> List<&2, String>: # a path's directory, with its slash (`src/lsp/`; `` at the root) def dir_of(path: String) -> String: +segs = init(String.split(norm(path), '/')) - Bool.pick(String, Nat.is_eq(List.length(&2, String, segs), 0n), "", String.join(segs, "/") ++ "/") + Bool.pick(String, List.is_empty(&2, String, segs), "", String.join(segs, "/") ++ "/") # a path imported from a file, normalized def resolve(+from: String, rel: String) -> String: diff --git a/src/rules/suspicious/empty.bend b/src/rules/suspicious/empty.bend new file mode 100644 index 0000000..d0f8654 --- /dev/null +++ b/src/rules/suspicious/empty.bend @@ -0,0 +1,372 @@ +# rule empty: a length compared to zero when the value is kept. Among the +# significant tokens (spaces, newlines and comments dropped): a `(`, `[`, +# `{` or `,`, then a dotted `Nat.is_eq`, `(`, and either a dotted +# `List.length`, `(`, any tokens up to its matching `)` whose last two are a +# `,` and a plain name x, or a dotted `String.length`, `(`, a plain name x +# and `)`; then `,`, `0n` and `)`; and x again, as a plain name, among the +# tokens after that `)` and before the bracket that closes the group the +# test sits in (brackets opened on the way are skipped over, not ended on). +# One finding, on the `Nat.is_eq` token, for each such test. +# Base's List.length and String.length count every cell (and are not tail +# calls); List.is_empty and String.is_empty, which take the same arguments, +# look at one and give the same Bool. The second read is what makes the fix +# pay on both lanes: x is kept past the test, so the test's own reference is +# dropped by a count, never by freeing x. Where the test is x's last use, +# the native lane frees the cells the walk would have, and freeing a list +# the program never walked costs more than walking it (bend 2.0.38: a +# 0-1000 char String tested then dropped ran 0.27x as fast as a length, +# kept 1.57x; JS 1.65x and 1.31x), so a test with no read after it in its +# group, a test outside any group, and a read before the test are left +# alone. A LAWS.bend or a PROOF.bend, which never runs, is exempt, and so +# is a `law` and a def that is a proof (no type, `def f(x):`, or one that +# returns `-> {..}`) in any file, from its keyword to the next `def`, `type` +# or `import`. A comment is never read, and a string literal is one token +# that is no name. +import Base +import ../../src.bend as Src +import ../../paths.bend as Paths +import ../../role.bend as Role +import ../../lazy/lazy.bend as Lazy +import ../../finding.bend as F +import ../../syntax/lex.bend as Lex +import ../tokens.bend as T + +# which length a test takes: a list's, a String's, or neither +type Form is Data: + FList{} + FStr{} + FNone{} + +# what the last tokens of a List.length's arguments were: a comma, a plain +# name right after a comma, or anything else +type Last is Data: + LComma{} + LName{name: String} + LOther{} + +# the name a test takes the length of, and the tokens after its `)` +type Taken is Data: + Taken{name: String, rest: List<&2, Lex.Tok>} + +# where a finding goes and what it says +type Hit is Data: + Hit{line: U32, col: U32, msg: String} + +# a bracket that opens a group, or a comma inside one: what may stand right +# before a test +def opener(kk: Lex.TokKind) -> Bool: + match kk: + case Lex.TOpen{}: + True{} + case Lex.TComma{}: + True{} + case other: + False{} + +# a token's text where it is code: a string literal or a comment says +# nothing the rule reads +def code(kk: Lex.TokKind, tt: String) -> String: + match kk: + case Lex.TStr{}: + "" + case Lex.TComment{}: + "" + case other: + tt + +# a dotted name +def dotted(kk: Lex.TokKind) -> Bool: + match kk: + case Lex.TDotted{}: + True{} + case other: + False{} + +# a plain name +def plain(kk: Lex.TokKind) -> Bool: + match kk: + case Lex.TName{}: + True{} + case other: + False{} + +# the length a dotted name takes +def form(+tt: String) -> Form: + Bool.pick(Form, String.eq(tt, "List.length"), FList{}, Bool.pick(Form, String.eq(tt, "String.length"), FStr{}, FNone{})) + +# an opener, `Nat.is_eq`, `(`, a dotted name and `(`? +def head( + k0: Lex.TokKind, + +k1: Lex.TokKind, + +t1: String, + k2: Lex.TokKind, + +t2: String, + +k3: Lex.TokKind, + k4: Lex.TokKind, + +t4: String +) -> Bool: + Bool.and(opener(k0), Bool.and(dotted(k1), Bool.and(dotted(k3), Bool.and(String.eq(code(k1, t1), "Nat.is_eq"), + Bool.and(String.eq(code(k2, t2), "("), String.eq(code(k4, t4), "(")))))) + +# what a token leaves of the last tokens: a comma, a name after a comma, or +# anything else +def last.step(+kk: Lex.TokKind, +tt: String, ll: Last) -> Last: + match kk: + case Lex.TComma{}: + LComma{} + case Lex.TName{}: + match ll: + case LComma{}: + LName{code(kk, tt)} + case other: + LOther{} + case other: + LOther{} + +# the name a List.length's arguments end in, when the last two were a comma +# and a plain name +def last.name(ll: Last, rest: List<&2, Lex.Tok>) -> Maybe<&2, Taken>: + match ll: + case LName{nn}: + Some{Taken{nn, rest}} + case other: + None{} + +# a bracket at the depth: the length's own `)` at depth zero; else the depth +# it leaves +def close.depth(kk: Lex.TokKind, dd: Nat) -> Nat: + match kk: + case Lex.TOpen{}: + 1n+dd + case Lex.TClose{}: + match dd: + case 0n: + 0n + case 1n+p: + p + case other: + dd + +# is the token the bracket that closes the arguments, at depth zero? +def close.here(kk: Lex.TokKind, dd: Nat) -> Bool: + match kk: + case Lex.TClose{}: + match dd: + case 0n: + True{} + case 1n+p: + False{} + case other: + False{} + +# a List.length's arguments, scanned to the `)` that closes them: the name +# they end in and the tokens after that `)`; none when they end otherwise +# or run out. done carries whether the last token read was that `)`. +def close.list(toks: List<&2, Lex.Tok>, +dd: Nat, +ll: Last, done: Bool, got: Maybe<&2, Taken>) -> Maybe<&2, Taken>: + match toks: + case Nil{}: + got + case Con{Lex.Tok{+k, +t, l, c}, +rest}: + match done: + case True{}: + got + case False{}: + +here = close.here(k, dd) + close.list(rest, close.depth(k, dd), last.step(k, t, ll), here, Bool.pick(Maybe<&2, Taken>, here, + last.name(ll, rest), None{})) + +# a String.length's argument: a plain name and `)`, then the tokens after +def close.str(toks: List<&2, Lex.Tok>) -> Maybe<&2, Taken>: + match toks: + case Con{Lex.Tok{+k1, +t1, l1, c1}, Con{Lex.Tok{k2, +t2, l2, c2}, rest}}: + Bool.pick(Maybe<&2, Taken>, Bool.and(plain(k1), String.eq(code(k2, t2), ")")), Some{Taken{code(k1, t1), rest}}, + None{}) + case other: + None{} + +# the length's argument, by its form +def taken(fm: Form, +toks: List<&2, Lex.Tok>) -> Maybe<&2, Taken>: + match fm: + case FList{}: + close.list(toks, 0n, LOther{}, False{}, None{}) + case FStr{}: + close.str(toks) + case FNone{}: + None{} + +# a plain name with x's text? +def same(+kk: Lex.TokKind, +tt: String, +xx: String) -> Bool: + Bool.and(plain(kk), String.eq(code(kk, tt), xx)) + +# is x read among the tokens before the bracket that closes the group they +# sit in? found carries whether the last token read was x, live whether that +# bracket is still ahead +def kept(toks: List<&2, Lex.Tok>, +xx: String, +dd: Nat, found: Bool, live: Bool) -> Bool: + match toks: + case Nil{}: + found + case Con{Lex.Tok{+k, +t, l, c}, rest}: + match found: + case True{}: + True{} + case False{}: + match live: + case False{}: + False{} + case True{}: + kept(rest, xx, close.depth(k, dd), same(k, t, xx), Bool.not(close.here(k, dd))) + +# what a finding says: the test, its fix and why +def say(fm: Form, +xx: String) -> String: + match fm: + case FList{}: + "Nat.is_eq(List.length(.., " ++ xx ++ "), 0n) counts every cell of " ++ xx ++ ", which is read again; List.is_empty(.., " + ++ xx ++ ") looks at one and gives the same answer." + case other: + "Nat.is_eq(String.length(" ++ xx ++ "), 0n) counts every char of " ++ xx ++ ", which is read again; String.is_empty(" + ++ xx ++ ") looks at one and gives the same answer." + +# a finding, if the test is whole and x kept +def tail.go(ok: Bool, fm: Form, xx: String, ll: U32, cc: U32) -> Maybe<&2, Hit>: + match ok: + case True{}: + Some{Hit{ll, cc, say(fm, xx)}} + case False{}: + None{} + +# the test's end, `,`, `0n` and `)`, then x kept: the finding, if any +def tail(mm: Maybe<&2, Taken>, +fm: Form, +ll: U32, +cc: U32) -> Maybe<&2, Hit>: + match mm: + case None{}: + None{} + case Some{Taken{+xx, r}}: + match r: + case Con{Lex.Tok{k1, +t1, l1, c1}, Con{Lex.Tok{k2, +t2, l2, c2}, Con{Lex.Tok{k3, +t3, l3, c3}, rest}}}: + tail.go(Bool.and(String.eq(code(k1, t1), ","), Bool.and(String.eq(code(k2, t2), "0n"), + Bool.and(String.eq(code(k3, t3), ")"), + kept(rest, xx, 0n, False{}, True{})))), fm, xx, ll, cc) + case other: + None{} + +# the test, its head read: the finding, if any +def at.go(ok: Bool, +fm: Form, +ll: U32, +cc: U32, r4: List<&2, Lex.Tok>) -> Maybe<&2, Hit>: + match ok: + case True{}: + tail(taken(fm, r4), fm, ll, cc) + case False{}: + None{} + +# a token of kind k0, then these: a kept test? +def at(k0: Lex.TokKind, toks: List<&2, Lex.Tok>) -> Maybe<&2, Hit>: + match toks: + case Con{Lex.Tok{k1, +t1, +l1, +c1}, Con{Lex.Tok{k2, +t2, l2, c2}, Con{Lex.Tok{+k3, +t3, l3, c3}, + Con{Lex.Tok{k4, +t4, l4, c4}, r4}}}}: + at.go(head(k0, k1, t1, k2, t2, k3, k4, t4), form(code(k3, t3)), l1, c1, r4) + case other: + None{} + +# the finding a test makes, if any, before the rest +def hit(mm: Maybe<&2, Hit>, +path: String, more: List<&2, F.Finding>) -> List<&2, F.Finding>: + match mm: + case None{}: + more + case Some{Hit{ll, cc, msg}}: + F.Finding{path, ll, cc, 9, "empty", msg} <> more + +# what the two tokens after a def's parameters say: a `:` (no type: the +# def fills a law) or `->` then `{` (it returns a proof) +def proofy.head(k1: Lex.TokKind, +k2: Lex.TokKind, +t2: String) -> Bool: + match k1: + case Lex.TColon{}: + True{} + case Lex.TArrow{}: + String.eq(code(k2, t2), "{") + case other: + False{} + +# what a def's header says once its parameters close +def proofy.end(toks: List<&2, Lex.Tok>) -> Bool: + match toks: + case Con{Lex.Tok{k1, t1, l1, c1}, Con{Lex.Tok{k2, t2, l2, c2}, rest}}: + proofy.head(k1, k2, t2) + case Con{Lex.Tok{k1, t1, l1, c1}, Nil{}}: + proofy.head(k1, Lex.TSpace{}, "") + case other: + False{} + +# does the token close the parameters: a bracket closing at depth one? +def proofy.fin(kk: Lex.TokKind, dd: Nat) -> Bool: + match kk: + case Lex.TClose{}: + match dd: + case 1n: + True{} + case other: + False{} + case other: + False{} + +# is the def these tokens head (after `def`) a proof? Its tokens are read to +# the bracket that closes its parameters, at depth zero; fin carries whether +# the last token read was that bracket +def proofy(toks: List<&2, Lex.Tok>, +dd: Nat, fin: Bool) -> Bool: + match toks: + case Nil{}: + False{} + case Con{Lex.Tok{+k, t, l, c}, +rest}: + match fin: + case True{}: + proofy.end(Lex.Tok{k, t, l, c} <> rest) + case False{}: + proofy(rest, close.depth(k, dd), proofy.fin(k, dd)) + +# what is skipped after a token that is no def: inside a law, from `law` on; +# code again from `type` or `import`; else as before +def item.other(+word: String, skip: Bool) -> Bool: + Bool.pick(Bool, String.eq(word, "law"), True{}, Bool.pick(Bool, Bool.or(String.eq(word, "type"), + String.eq(word, "import")), False{}, skip)) + +# what is skipped after a keyword: a def is skipped when it is a proof +def item.word(isdef: Bool, +word: String, rest: List<&2, Lex.Tok>, skip: Bool) -> Bool: + match isdef: + case True{}: + proofy(rest, 0n, False{}) + case False{}: + item.other(word, skip) + +# what is skipped after a token: a law, and a def that is a proof, never run +def item(+kk: Lex.TokKind, +tt: String, rest: List<&2, Lex.Tok>, skip: Bool) -> Bool: + match kk: + case Lex.TKey{}: + item.word(String.eq(code(kk, tt), "def"), code(kk, tt), rest, skip) + case other: + skip + +# the kept test a token opens, if any, outside what is skipped +def found(skip: Bool, kk: Lex.TokKind, rest: List<&2, Lex.Tok>) -> Maybe<&2, Hit>: + match skip: + case True{}: + None{} + case False{}: + at(kk, rest) + +# every kept test among the tokens, in order; skip says whether the tokens +# so far sit in a law or a def that is a proof +def walk(toks: List<&2, Lex.Tok>, +path: String, skip: Bool) -> List<&2, F.Finding>: + match toks: + case Nil{}: + Nil{} + case Con{Lex.Tok{+k, +t, l, c}, +rest}: + +sk = item(k, t, rest, skip) + hit(found(sk, k, rest), path, walk(rest, path, sk)) + +# the rule +def check(ss: Src.Src) -> List<&2, F.Finding>: + Src.Src{+path, text, toks, tree, bound, items} = ss + Lazy.stop(List<&2, F.Finding>, Paths.is_law_file(path), [], _u => walk(T.sig(toks), path, False{})) + +# the rule, told the file's role (src/role.bend): a law or proof file is +# skipped +def check.role(rr: Role.Role, ss: Src.Src) -> List<&2, F.Finding>: + Src.Src{path, text, toks, tree, bound, items} = ss + Lazy.stop(List<&2, F.Finding>, Role.is_law_file(rr), [], _u => walk(T.sig(toks), path, False{}))