From 17274e8744b983185fdde82300e752c491181a1c Mon Sep 17 00:00:00 2001 From: Florian Schanda Date: Wed, 8 Nov 2023 15:47:25 +0100 Subject: [PATCH] Write UG for the linter --- README.md | 1 + documentation/TUTORIAL-LINT.md | 8 +- documentation/linter.md | 359 ++++++++++++++++++ .../lint-ug-examples/abstract_leaf_types.rsl | 5 + tests-system/lint-ug-examples/always_true.rsl | 13 + .../lint-ug-examples/always_true_fixed.rsl | 13 + tests-system/lint-ug-examples/array_index.rsl | 9 + .../lint-ug-examples/array_index_fixed.rsl | 9 + .../lint-ug-examples/clarify_final.rsl | 8 + tests-system/lint-ug-examples/div_by_zero.rsl | 13 + .../lint-ug-examples/div_by_zero_fixed.rsl | 13 + .../lint-ug-examples/evaluation_of_null.rsl | 9 + .../evaluation_of_null_fixed.rsl | 9 + .../impossible_array_types.rsl | 6 + tests-system/lint-ug-examples/output | 47 +++ tests-system/lint-ug-examples/output.brief | 0 tests-system/lint-ug-examples/output.json | 2 + tests-system/lint-ug-examples/output.smtlib | 47 +++ .../separator_based_literal_ambiguity.rsl | 11 + .../unary_minus_precedence.rsl | 13 + .../lint-ug-examples/weird_array_types.rsl | 6 + 21 files changed, 597 insertions(+), 4 deletions(-) create mode 100644 documentation/linter.md create mode 100644 tests-system/lint-ug-examples/abstract_leaf_types.rsl create mode 100644 tests-system/lint-ug-examples/always_true.rsl create mode 100644 tests-system/lint-ug-examples/always_true_fixed.rsl create mode 100644 tests-system/lint-ug-examples/array_index.rsl create mode 100644 tests-system/lint-ug-examples/array_index_fixed.rsl create mode 100644 tests-system/lint-ug-examples/clarify_final.rsl create mode 100644 tests-system/lint-ug-examples/div_by_zero.rsl create mode 100644 tests-system/lint-ug-examples/div_by_zero_fixed.rsl create mode 100644 tests-system/lint-ug-examples/evaluation_of_null.rsl create mode 100644 tests-system/lint-ug-examples/evaluation_of_null_fixed.rsl create mode 100644 tests-system/lint-ug-examples/impossible_array_types.rsl create mode 100644 tests-system/lint-ug-examples/output create mode 100644 tests-system/lint-ug-examples/output.brief create mode 100644 tests-system/lint-ug-examples/output.json create mode 100644 tests-system/lint-ug-examples/output.smtlib create mode 100644 tests-system/lint-ug-examples/separator_based_literal_ambiguity.rsl create mode 100644 tests-system/lint-ug-examples/unary_minus_precedence.rsl create mode 100644 tests-system/lint-ug-examples/weird_array_types.rsl diff --git a/README.md b/README.md index 34a4d4a9..696bf728 100644 --- a/README.md +++ b/README.md @@ -32,6 +32,7 @@ The Python implementation can be used for several purposes: ### For normal users * [Tutorial](documentation/TUTORIAL.md) (read this as a first introduction) +* [User manual: TRLC linter](documentation/linter.md) (the user manual for the TRLC static analysis and linter) * [Release Notes](CHANGELOG.md) (read this to find out whats new) * [License](LICENSE) diff --git a/documentation/TUTORIAL-LINT.md b/documentation/TUTORIAL-LINT.md index 35040242..ed1a602e 100644 --- a/documentation/TUTORIAL-LINT.md +++ b/documentation/TUTORIAL-LINT.md @@ -4,10 +4,10 @@ This is part of the [TRLC Tutorial](TUTORIAL.md). ## Using the linter -The TRLC tools come with a static analysis tool that can diagnose some -potential issues with `.rsl` files before they are deployed and -used. This is enabled by default, but you can turn these off with the -`--no-lint` option. +The TRLC tools come with a [static analysis tool](linter.md) that can +diagnose some potential issues with `.rsl` files before they are +deployed and used. This is enabled by default, but you can turn these +off with the `--no-lint` option. To enable more detailed checks you can also use the `--verify` feature, but please note that this is only available on Linux, and diff --git a/documentation/linter.md b/documentation/linter.md new file mode 100644 index 00000000..79ee603d --- /dev/null +++ b/documentation/linter.md @@ -0,0 +1,359 @@ +# User guide: TRLC static analyser and linter + +## Purpose + +The TRLC static analyser and linter can be used to find misleading or +problematic types and user defined checks. It is recommended to use +it. + +## Usage + +The linter is enabled by default, so running `trlc filename.rsl` will +also run the linter. The static analyser can be enabled with the +`--verify` option, i.e: `trlc --verify filename.rsl`. + +You can explicitly turn the linter off with the `--no-lint` option. + +## Checks + +### Linter checks + +#### clarify_final + +Final is a type attribute that is inherited. However for readability +it is a good idea to explicitly state it again. + +```trlc +package Clarify_Final + +final type T { + x Integer +} + +type Q extends T { +} +``` + +Generates this message: + +```plain +type Q extends T { + ^ clarify_final.rsl:7: issue: consider clarifying that this record is final [clarify_final] + | Parent record Clarify_Final.T is final, making this record + | also final. Marking it explicitly as final + | clarifies this to casual readers. +``` + +#### unary_minus_precedence + +A curiosity of the TRLC expression grammar (which strongly derives +from the Ada grammar, which shares this particularity) is that unary +minus followed by a stronger binding operator doesn't have the +precedence you think it does. For example: + +```trlc +package Unary_Minus_Precedence + +type T { + x Integer +} + +checks T { + -x / 3 < 0, "non-obvious meaning" + + (-x) / 3 < 0, "clear meaning" + + -(x / 3) < 0, "clear meaning" +} +``` + +Will generate the following message: + +```plain +-x / 3 < 0, "non-obvious meaning" +^ unary_minus_precedence.rsl:8: issue: expression means -(x / 3), place explicit brackets to clarify intent [unary_minus_precedence] +``` + +#### abstract_leaf_types + +Abstract types that are never extended can't be used. Most likely they +are remnants of some refactoring. + +```trlc +package Abstract_Leaf_Types + +abstract type T { + description String +} +``` + +Will generate: + +```plain +abstract type T { + ^ abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types] +``` + +#### deprecated_feature + +Some features in TRLC are deprecated, that are scheduled to be removed +for version 2.0.0. The linter can notify you when you're using such a +construct, and how it should be done in the future. Right now these +two features are: + +* `.check` files (just move the check blocks into the `.rsl` file) +* The legacy `trlc:len` style of builtin functions (just use + e.g. `len` instead) + +#### separator_based_literal_ambiguity + +Tuple types with their custom separators offer a lot of potential for +convenient syntax. There is however a specific combination that is +problematic: + +```trlc +package Separator_Based_Literal_Ambiguity + +tuple T { + value_1 Integer + separator x + value_2 optional Integer +} + +type Q { + value T +} +``` + +Consider possible assignments to `value`: +* `0` (tuple where value_1 = integer 0) +* `0x0` (tuple where value_1 = hex integer 0x0, but value_2 is null) +* `0 x 0` (tuple where value_1 = integer 0, and value_2 is integer 0) + +This is only the case of literal separators `x` and `b`, and only when +they follow an integer or decimal type. The linter generates a message +in this case: + +```plain +separator x + ^ separator_based_literal_ambiguity.rsl:5: issue: x separator after integer component creates ambiguities [separator_based_literal_ambiguity] + | For example 0x100 would be a base 16 literal + | instead of the tuple segment 0 x 100. +``` + +#### impossible_array_types + +Some arrays bounds produce arrays that could never be written. For +example: + +```trlc +package Impossible_Array_Types + +type T { + x Integer [10 .. 3] + y Integer [0 .. 0] +} +``` + +This generates: + +```plain +x Integer [10 .. 3] + ^ impossible_array_types.rsl:4: issue: upper bound must be at least 10 [impossible_array_types] +y Integer [0 .. 0] + ^ impossible_array_types.rsl:5: issue: this array makes no sense [impossible_array_types] +``` + +#### weird_array_types + +Related to the check above, you could create arrays that shouldn't be +arrays. + +```trlc +package Weird_Array_Types + +type T { + x Integer [1 .. 1] + y Integer [0 .. 1] +} +``` + +Would produce the following messages: + +```plain +x Integer [1 .. 1] + ^ weird_array_types.rsl:4: issue: array of fixed size 1 should not be an array [weird_array_types] + | An array with a fixed size of 1 should not + | be an array at all. +y Integer [0 .. 1] + ^ weird_array_types.rsl:5: issue: consider making this array an optional Integer [weird_array_types] + | An array with 0 to 1 components should just + | be an optional Integer instead. +``` + +### TRLC static analyser checks + +#### vcg-evaluation-of-null + +Evaluating null in any context other than equality is an error. For +example: + +```trlc +package Evaluation_Of_Null + +type Requirement { + description optional String +} + +checks Requirement { + len(description) >= 10, "too short" +} +``` + +Would generate: + +```plain +len(description) >= 10, "too short" + ^^^^^^^^^^^ evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | Requirement bad_potato { + | /* description is null */ + | } +``` + +To fix this you should prefix the check with a guard, for example like +this: + +```trlc +checks Requirement { + description != null implies len(description) >= 10, "too short" +} +``` + +#### vcg-div-by-zero + +Dividing by zero is always bad. For example: + +```trlc +package Div_By_Zero + +type T { + x Integer + y Integer +} + +checks T { + x > 2, fatal "x too small" + y > 2, fatal "y too small" + + 100 / (111 - x * y) > 0, "example" +} +``` + +Would generate: + +```plain +100 / (111 - x * y) > 0, "example" + ^ div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero] + | example record_type triggering error: + | T bad_potato { + | x = 3 + | y = 37 + | } +``` + +To fix this either don't do such weird things ;) or perhaps use a +prime number instead of 111: + +```trlc +checks T { + x > 2, fatal "x too small" + y > 2, fatal "y too small" + + 100 / (113 - x * y) > 0, "example" +} +``` + +With that fix the static analyser doesn't complain anymore as there is +no way to get 113 by multiplying two numbers greater than 2. + +#### vcg-array-index + +Going out of bounds is also a classic error: + +```trlc +package Array_Index + +type T { + x Integer [1 .. 10] +} + +checks T { + len(x) >= 0 implies x[3] > 0, "too small" +} +``` + +Would generate: + +```plain +len(x) >= 3 implies x[3] > 0, "too small" + ^ array_index.rsl:8: issue: array index could be larger than len(x) [vcg-array-index] + | example record_type triggering error: + | T bad_potato { + | x = [1, 1, 1] + | } +``` + +You could fix this by either remembering that arrays start at 0 (so +change to `len(x) >= 4`) or perhaps by making sure the array is always +at least 4 elements long (i.e. `x Integer [4 .. 10]`). + +#### vcg-always-true + +Sometimes checks are just tautologies, and so they don't really serve +any purpose. + +```trlc +package Always_True + +type T { + description optional String +} + +type Q extends T { + freeze description = "potato" +} + +checks Q { + description != null, "description cannot be empty" +} +``` + +Would generate predictably: + +```plain +description != null, "description cannot be empty" + ^^ always_true.rsl:12: issue: expression is always true [vcg-always-true] +``` + +Maybe you meant to attach this check to type T instead of Q? I.e. like so: + +```trlc +package Always_True_Fixed + +type T { + description optional String +} + +checks T { + description != null, "description cannot be empty" +} + +type Q extends T { + freeze description = "potato" +} +``` + +The static analyser does not consider this check to be always true +now, since you could have instances of just T, even though Q would +always make it true. diff --git a/tests-system/lint-ug-examples/abstract_leaf_types.rsl b/tests-system/lint-ug-examples/abstract_leaf_types.rsl new file mode 100644 index 00000000..4fbb0cb1 --- /dev/null +++ b/tests-system/lint-ug-examples/abstract_leaf_types.rsl @@ -0,0 +1,5 @@ +package Abstract_Leaf_Types + +abstract type T { + description String +} diff --git a/tests-system/lint-ug-examples/always_true.rsl b/tests-system/lint-ug-examples/always_true.rsl new file mode 100644 index 00000000..0e9b92de --- /dev/null +++ b/tests-system/lint-ug-examples/always_true.rsl @@ -0,0 +1,13 @@ +package Always_True + +type T { + description optional String +} + +type Q extends T { + freeze description = "potato" +} + +checks Q { + description != null, "description cannot be empty" +} diff --git a/tests-system/lint-ug-examples/always_true_fixed.rsl b/tests-system/lint-ug-examples/always_true_fixed.rsl new file mode 100644 index 00000000..e0ad95de --- /dev/null +++ b/tests-system/lint-ug-examples/always_true_fixed.rsl @@ -0,0 +1,13 @@ +package Always_True_Fixed + +type T { + description optional String +} + +checks T { + description != null, "description cannot be empty" +} + +type Q extends T { + freeze description = "potato" +} diff --git a/tests-system/lint-ug-examples/array_index.rsl b/tests-system/lint-ug-examples/array_index.rsl new file mode 100644 index 00000000..9a59fa97 --- /dev/null +++ b/tests-system/lint-ug-examples/array_index.rsl @@ -0,0 +1,9 @@ +package Array_Index + +type T { + x Integer [1 .. 10] +} + +checks T { + len(x) >= 3 implies x[3] > 0, "too small" +} diff --git a/tests-system/lint-ug-examples/array_index_fixed.rsl b/tests-system/lint-ug-examples/array_index_fixed.rsl new file mode 100644 index 00000000..e14546c9 --- /dev/null +++ b/tests-system/lint-ug-examples/array_index_fixed.rsl @@ -0,0 +1,9 @@ +package Array_Index_Fixed + +type T { + x Integer [1 .. 10] +} + +checks T { + len(x) >= 4 implies x[3] > 0, "too small" +} diff --git a/tests-system/lint-ug-examples/clarify_final.rsl b/tests-system/lint-ug-examples/clarify_final.rsl new file mode 100644 index 00000000..29ea44d4 --- /dev/null +++ b/tests-system/lint-ug-examples/clarify_final.rsl @@ -0,0 +1,8 @@ +package Clarify_Final + +final type T { + x Integer +} + +type Q extends T { +} diff --git a/tests-system/lint-ug-examples/div_by_zero.rsl b/tests-system/lint-ug-examples/div_by_zero.rsl new file mode 100644 index 00000000..960d84c3 --- /dev/null +++ b/tests-system/lint-ug-examples/div_by_zero.rsl @@ -0,0 +1,13 @@ +package Div_By_Zero + +type T { + x Integer + y Integer +} + +checks T { + x > 2, fatal "x too small" + y > 2, fatal "y too small" + + 100 / (111 - x * y) > 0, "example" +} diff --git a/tests-system/lint-ug-examples/div_by_zero_fixed.rsl b/tests-system/lint-ug-examples/div_by_zero_fixed.rsl new file mode 100644 index 00000000..ea1f77b0 --- /dev/null +++ b/tests-system/lint-ug-examples/div_by_zero_fixed.rsl @@ -0,0 +1,13 @@ +package Div_By_Zero_Fixed + +type T { + x Integer + y Integer +} + +checks T { + x > 2, fatal "x too small" + y > 2, fatal "y too small" + + 100 / (113 - x * y) > 0, "example" +} diff --git a/tests-system/lint-ug-examples/evaluation_of_null.rsl b/tests-system/lint-ug-examples/evaluation_of_null.rsl new file mode 100644 index 00000000..aa72acc0 --- /dev/null +++ b/tests-system/lint-ug-examples/evaluation_of_null.rsl @@ -0,0 +1,9 @@ +package Evaluation_Of_Null + +type Requirement { + description optional String +} + +checks Requirement { + len(description) >= 10, "too short" +} diff --git a/tests-system/lint-ug-examples/evaluation_of_null_fixed.rsl b/tests-system/lint-ug-examples/evaluation_of_null_fixed.rsl new file mode 100644 index 00000000..f7635ae1 --- /dev/null +++ b/tests-system/lint-ug-examples/evaluation_of_null_fixed.rsl @@ -0,0 +1,9 @@ +package Evaluation_Of_Null_Fixed + +type Requirement { + description optional String +} + +checks Requirement { + description != null implies len(description) >= 10, "too short" +} diff --git a/tests-system/lint-ug-examples/impossible_array_types.rsl b/tests-system/lint-ug-examples/impossible_array_types.rsl new file mode 100644 index 00000000..3e1100dc --- /dev/null +++ b/tests-system/lint-ug-examples/impossible_array_types.rsl @@ -0,0 +1,6 @@ +package Impossible_Array_Types + +type T { + x Integer [10 .. 3] + y Integer [0 .. 0] +} diff --git a/tests-system/lint-ug-examples/output b/tests-system/lint-ug-examples/output new file mode 100644 index 00000000..c909f055 --- /dev/null +++ b/tests-system/lint-ug-examples/output @@ -0,0 +1,47 @@ +type Q extends T { + ^ lint-ug-examples/clarify_final.rsl:7: issue: consider clarifying that this record is final [clarify_final] + | Parent record Clarify_Final.T is final, making this record + | also final. Marking it explicitly as final + | clarifies this to casual readers. +-x / 3 < 0, "non-obvious meaning" +^ lint-ug-examples/unary_minus_precedence.rsl:8: issue: expression means -(x / 3), place explicit brackets to clarify intent [unary_minus_precedence] +description != null, "description cannot be empty" + ^^ lint-ug-examples/always_true.rsl:12: issue: expression is always true [vcg-always-true] +len(x) >= 3 implies x[3] > 0, "too small" + ^ lint-ug-examples/array_index.rsl:8: issue: array index could be larger than len(x) [vcg-array-index] + | example record_type triggering error: + | T bad_potato { + | x = [1, 1, 1] + | } +100 / (111 - x * y) > 0, "example" + ^ lint-ug-examples/div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero] + | example record_type triggering error: + | T bad_potato { + | x = 3 + | y = 37 + | } +len(description) >= 10, "too short" + ^^^^^^^^^^^ lint-ug-examples/evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | Requirement bad_potato { + | /* description is null */ + | } +x Integer [10 .. 3] + ^ lint-ug-examples/impossible_array_types.rsl:4: issue: upper bound must be at least 10 [impossible_array_types] +y Integer [0 .. 0] + ^ lint-ug-examples/impossible_array_types.rsl:5: issue: this array makes no sense [impossible_array_types] +separator x + ^ lint-ug-examples/separator_based_literal_ambiguity.rsl:5: issue: x separator after integer component creates ambiguities [separator_based_literal_ambiguity] + | For example 0x100 would be a base 16 literal + | instead of the tuple segment 0 x 100. +x Integer [1 .. 1] + ^ lint-ug-examples/weird_array_types.rsl:4: issue: array of fixed size 1 should not be an array [weird_array_types] + | An array with a fixed size of 1 should not + | be an array at all. +y Integer [0 .. 1] + ^ lint-ug-examples/weird_array_types.rsl:5: issue: consider making this array an optional Integer [weird_array_types] + | An array with 0 to 1 components should just + | be an optional Integer instead. +abstract type T { + ^ lint-ug-examples/abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types] +Processed 14 models, 0 checks and 0 requirement files and found 12 warnings diff --git a/tests-system/lint-ug-examples/output.brief b/tests-system/lint-ug-examples/output.brief new file mode 100644 index 00000000..e69de29b diff --git a/tests-system/lint-ug-examples/output.json b/tests-system/lint-ug-examples/output.json new file mode 100644 index 00000000..32da48be --- /dev/null +++ b/tests-system/lint-ug-examples/output.json @@ -0,0 +1,2 @@ +{} +Processed 14 models, 0 checks and 0 requirement files and found no issues diff --git a/tests-system/lint-ug-examples/output.smtlib b/tests-system/lint-ug-examples/output.smtlib new file mode 100644 index 00000000..c909f055 --- /dev/null +++ b/tests-system/lint-ug-examples/output.smtlib @@ -0,0 +1,47 @@ +type Q extends T { + ^ lint-ug-examples/clarify_final.rsl:7: issue: consider clarifying that this record is final [clarify_final] + | Parent record Clarify_Final.T is final, making this record + | also final. Marking it explicitly as final + | clarifies this to casual readers. +-x / 3 < 0, "non-obvious meaning" +^ lint-ug-examples/unary_minus_precedence.rsl:8: issue: expression means -(x / 3), place explicit brackets to clarify intent [unary_minus_precedence] +description != null, "description cannot be empty" + ^^ lint-ug-examples/always_true.rsl:12: issue: expression is always true [vcg-always-true] +len(x) >= 3 implies x[3] > 0, "too small" + ^ lint-ug-examples/array_index.rsl:8: issue: array index could be larger than len(x) [vcg-array-index] + | example record_type triggering error: + | T bad_potato { + | x = [1, 1, 1] + | } +100 / (111 - x * y) > 0, "example" + ^ lint-ug-examples/div_by_zero.rsl:12: issue: divisor could be 0 [vcg-div-by-zero] + | example record_type triggering error: + | T bad_potato { + | x = 3 + | y = 37 + | } +len(description) >= 10, "too short" + ^^^^^^^^^^^ lint-ug-examples/evaluation_of_null.rsl:8: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | Requirement bad_potato { + | /* description is null */ + | } +x Integer [10 .. 3] + ^ lint-ug-examples/impossible_array_types.rsl:4: issue: upper bound must be at least 10 [impossible_array_types] +y Integer [0 .. 0] + ^ lint-ug-examples/impossible_array_types.rsl:5: issue: this array makes no sense [impossible_array_types] +separator x + ^ lint-ug-examples/separator_based_literal_ambiguity.rsl:5: issue: x separator after integer component creates ambiguities [separator_based_literal_ambiguity] + | For example 0x100 would be a base 16 literal + | instead of the tuple segment 0 x 100. +x Integer [1 .. 1] + ^ lint-ug-examples/weird_array_types.rsl:4: issue: array of fixed size 1 should not be an array [weird_array_types] + | An array with a fixed size of 1 should not + | be an array at all. +y Integer [0 .. 1] + ^ lint-ug-examples/weird_array_types.rsl:5: issue: consider making this array an optional Integer [weird_array_types] + | An array with 0 to 1 components should just + | be an optional Integer instead. +abstract type T { + ^ lint-ug-examples/abstract_leaf_types.rsl:3: issue: abstract type T does not have any extensions [abstract_leaf_types] +Processed 14 models, 0 checks and 0 requirement files and found 12 warnings diff --git a/tests-system/lint-ug-examples/separator_based_literal_ambiguity.rsl b/tests-system/lint-ug-examples/separator_based_literal_ambiguity.rsl new file mode 100644 index 00000000..bfd43ac2 --- /dev/null +++ b/tests-system/lint-ug-examples/separator_based_literal_ambiguity.rsl @@ -0,0 +1,11 @@ +package Separator_Based_Literal_Ambiguity + +tuple T { + value_1 Integer + separator x + value_2 optional Integer +} + +type Q { + value T +} diff --git a/tests-system/lint-ug-examples/unary_minus_precedence.rsl b/tests-system/lint-ug-examples/unary_minus_precedence.rsl new file mode 100644 index 00000000..40e1a6d8 --- /dev/null +++ b/tests-system/lint-ug-examples/unary_minus_precedence.rsl @@ -0,0 +1,13 @@ +package Unary_Minus_Precedence + +type T { + x Integer +} + +checks T { + -x / 3 < 0, "non-obvious meaning" + + (-x) / 3 < 0, "clear meaning" + + -(x / 3) < 0, "clear meaning" +} diff --git a/tests-system/lint-ug-examples/weird_array_types.rsl b/tests-system/lint-ug-examples/weird_array_types.rsl new file mode 100644 index 00000000..eaf616fe --- /dev/null +++ b/tests-system/lint-ug-examples/weird_array_types.rsl @@ -0,0 +1,6 @@ +package Weird_Array_Types + +type T { + x Integer [1 .. 1] + y Integer [0 .. 1] +}