From 5b0f823c2eb6d99f03ce8f546d422be82d7c4052 Mon Sep 17 00:00:00 2001 From: christophkloeffel Date: Mon, 16 Oct 2023 13:00:15 +0200 Subject: [PATCH] adds tracing for conditional expressions --- language-reference-manual/lrm.trlc | 2 +- tests-system/if_expressions/foo.check | 6 ------ tests-system/if_expressions/foo.rsl | 7 ------- tests-system/if_expressions/output | 7 ------- tests-system/if_expressions/output.brief | 2 -- tests-system/if_expressions/output.json | 5 ----- tests-system/if_expressions/output.smtlib | 7 ------- .../rbt-conditional-expression-types/foo.rsl | 11 +++++++++++ .../foo.trlc | 0 .../rbt-conditional-expression-types/output | 3 +++ .../rbt-conditional-expression-types/output.brief | 1 + .../rbt-conditional-expression-types/output.json | 3 +++ .../output.smtlib | 3 +++ tests-system/rbt-conditional-expression/foo.rsl | 15 +++++++++++++++ tests-system/rbt-conditional-expression/foo.trlc | 8 ++++++++ tests-system/rbt-conditional-expression/output | 9 +++++++++ .../rbt-conditional-expression/output.brief | 4 ++++ .../rbt-conditional-expression/output.json | 9 +++++++++ .../rbt-conditional-expression/output.smtlib | 9 +++++++++ tests-system/rbt-conditional-expression/tracing | 2 ++ trlc/ast.py | 5 ++++- trlc/parser.py | 1 + 22 files changed, 83 insertions(+), 36 deletions(-) delete mode 100644 tests-system/if_expressions/foo.check delete mode 100644 tests-system/if_expressions/foo.rsl delete mode 100644 tests-system/if_expressions/output delete mode 100644 tests-system/if_expressions/output.brief delete mode 100644 tests-system/if_expressions/output.json delete mode 100644 tests-system/if_expressions/output.smtlib create mode 100644 tests-system/rbt-conditional-expression-types/foo.rsl rename tests-system/{if_expressions => rbt-conditional-expression-types}/foo.trlc (100%) create mode 100644 tests-system/rbt-conditional-expression-types/output create mode 100644 tests-system/rbt-conditional-expression-types/output.brief create mode 100644 tests-system/rbt-conditional-expression-types/output.json create mode 100644 tests-system/rbt-conditional-expression-types/output.smtlib create mode 100644 tests-system/rbt-conditional-expression/foo.rsl create mode 100644 tests-system/rbt-conditional-expression/foo.trlc create mode 100644 tests-system/rbt-conditional-expression/output create mode 100644 tests-system/rbt-conditional-expression/output.brief create mode 100644 tests-system/rbt-conditional-expression/output.json create mode 100644 tests-system/rbt-conditional-expression/output.smtlib create mode 100644 tests-system/rbt-conditional-expression/tracing diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index 5c927315..453ae851 100644 --- a/language-reference-manual/lrm.trlc +++ b/language-reference-manual/lrm.trlc @@ -1650,7 +1650,7 @@ section "Conditional expressions" { } Dynamic_Semantics Conditional_Expression_Else { - text = '''If all condition are evaluated to false, then the else + text = '''If all conditions are evaluated to false, then the else dependent expression is evaluated and returned.''' } diff --git a/tests-system/if_expressions/foo.check b/tests-system/if_expressions/foo.check deleted file mode 100644 index 3c0d1e9c..00000000 --- a/tests-system/if_expressions/foo.check +++ /dev/null @@ -1,6 +0,0 @@ -package Foo - -checks T { - (if x > y then x else y) <= x, "potato" - (if b then b else x > 5), "kitten" -} diff --git a/tests-system/if_expressions/foo.rsl b/tests-system/if_expressions/foo.rsl deleted file mode 100644 index 813c5d1b..00000000 --- a/tests-system/if_expressions/foo.rsl +++ /dev/null @@ -1,7 +0,0 @@ -package Foo - -type T { - x Integer - y Integer - b Boolean -} diff --git a/tests-system/if_expressions/output b/tests-system/if_expressions/output deleted file mode 100644 index cdffde7c..00000000 --- a/tests-system/if_expressions/output +++ /dev/null @@ -1,7 +0,0 @@ -checks T { - ^ if_expressions/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] -T test_01 { - ^^^^^^^ if_expressions/foo.trlc:3: check error: potato -T test_01 { - ^^^^^^^ if_expressions/foo.trlc:3: check error: kitten -Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 2 error(s) diff --git a/tests-system/if_expressions/output.brief b/tests-system/if_expressions/output.brief deleted file mode 100644 index 4532a9fb..00000000 --- a/tests-system/if_expressions/output.brief +++ /dev/null @@ -1,2 +0,0 @@ -if_expressions/foo.trlc:3:3: trlc check error: potato -if_expressions/foo.trlc:3:3: trlc check error: kitten diff --git a/tests-system/if_expressions/output.json b/tests-system/if_expressions/output.json deleted file mode 100644 index 667589c7..00000000 --- a/tests-system/if_expressions/output.json +++ /dev/null @@ -1,5 +0,0 @@ -T test_01 { - ^^^^^^^ if_expressions/foo.trlc:3: check error: potato -T test_01 { - ^^^^^^^ if_expressions/foo.trlc:3: check error: kitten -Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 2 error(s) diff --git a/tests-system/if_expressions/output.smtlib b/tests-system/if_expressions/output.smtlib deleted file mode 100644 index cdffde7c..00000000 --- a/tests-system/if_expressions/output.smtlib +++ /dev/null @@ -1,7 +0,0 @@ -checks T { - ^ if_expressions/foo.check:3: issue: move this check block into foo.rsl:1 [deprecated_feature] -T test_01 { - ^^^^^^^ if_expressions/foo.trlc:3: check error: potato -T test_01 { - ^^^^^^^ if_expressions/foo.trlc:3: check error: kitten -Processed 1 model(s), 1 check(s) and 1 requirement file(s) and found 1 warning(s) and 2 error(s) diff --git a/tests-system/rbt-conditional-expression-types/foo.rsl b/tests-system/rbt-conditional-expression-types/foo.rsl new file mode 100644 index 00000000..bfb403a3 --- /dev/null +++ b/tests-system/rbt-conditional-expression-types/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + x Integer + y Integer + b Boolean +} + +checks T { + (if x then x elsif y > x then y else y) <= x, "potato type" +} diff --git a/tests-system/if_expressions/foo.trlc b/tests-system/rbt-conditional-expression-types/foo.trlc similarity index 100% rename from tests-system/if_expressions/foo.trlc rename to tests-system/rbt-conditional-expression-types/foo.trlc diff --git a/tests-system/rbt-conditional-expression-types/output b/tests-system/rbt-conditional-expression-types/output new file mode 100644 index 00000000..d70b7e74 --- /dev/null +++ b/tests-system/rbt-conditional-expression-types/output @@ -0,0 +1,3 @@ +(if x then x elsif y > x then y else y) <= x, "potato type" + ^ rbt-conditional-expression-types/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-conditional-expression-types/output.brief b/tests-system/rbt-conditional-expression-types/output.brief new file mode 100644 index 00000000..ea9c7f4d --- /dev/null +++ b/tests-system/rbt-conditional-expression-types/output.brief @@ -0,0 +1 @@ +rbt-conditional-expression-types/foo.rsl:10:8: trlc error: expected expression of type Builtin_Boolean, got Builtin_Integer instead diff --git a/tests-system/rbt-conditional-expression-types/output.json b/tests-system/rbt-conditional-expression-types/output.json new file mode 100644 index 00000000..d70b7e74 --- /dev/null +++ b/tests-system/rbt-conditional-expression-types/output.json @@ -0,0 +1,3 @@ +(if x then x elsif y > x then y else y) <= x, "potato type" + ^ rbt-conditional-expression-types/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-conditional-expression-types/output.smtlib b/tests-system/rbt-conditional-expression-types/output.smtlib new file mode 100644 index 00000000..d70b7e74 --- /dev/null +++ b/tests-system/rbt-conditional-expression-types/output.smtlib @@ -0,0 +1,3 @@ +(if x then x elsif y > x then y else y) <= x, "potato type" + ^ rbt-conditional-expression-types/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-conditional-expression/foo.rsl b/tests-system/rbt-conditional-expression/foo.rsl new file mode 100644 index 00000000..15b9b25d --- /dev/null +++ b/tests-system/rbt-conditional-expression/foo.rsl @@ -0,0 +1,15 @@ +package Foo + +type T { + x Integer + y Integer + z Integer + b Boolean +} + +checks T { + (if b then b else x > 5), "kitten" + (if y > x then x elsif x > y then x else y) < x, "foobar evaluation if" + (if x > y then x elsif y > x then y else z) <= x, "foobar evaluation elsif" + (if x > y then x elsif y == x then y else z) >= x, "potato else" +} diff --git a/tests-system/rbt-conditional-expression/foo.trlc b/tests-system/rbt-conditional-expression/foo.trlc new file mode 100644 index 00000000..68cf349b --- /dev/null +++ b/tests-system/rbt-conditional-expression/foo.trlc @@ -0,0 +1,8 @@ +package Foo + +T test_01 { + x = 5 + y = 10 + z = 1 + b = false +} diff --git a/tests-system/rbt-conditional-expression/output b/tests-system/rbt-conditional-expression/output new file mode 100644 index 00000000..dc4c8af6 --- /dev/null +++ b/tests-system/rbt-conditional-expression/output @@ -0,0 +1,9 @@ +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: kitten +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation if +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation elsif +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: potato else +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 4 error(s) diff --git a/tests-system/rbt-conditional-expression/output.brief b/tests-system/rbt-conditional-expression/output.brief new file mode 100644 index 00000000..1b000d7b --- /dev/null +++ b/tests-system/rbt-conditional-expression/output.brief @@ -0,0 +1,4 @@ +rbt-conditional-expression/foo.trlc:3:3: trlc check error: kitten +rbt-conditional-expression/foo.trlc:3:3: trlc check error: foobar evaluation if +rbt-conditional-expression/foo.trlc:3:3: trlc check error: foobar evaluation elsif +rbt-conditional-expression/foo.trlc:3:3: trlc check error: potato else diff --git a/tests-system/rbt-conditional-expression/output.json b/tests-system/rbt-conditional-expression/output.json new file mode 100644 index 00000000..dc4c8af6 --- /dev/null +++ b/tests-system/rbt-conditional-expression/output.json @@ -0,0 +1,9 @@ +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: kitten +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation if +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation elsif +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: potato else +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 4 error(s) diff --git a/tests-system/rbt-conditional-expression/output.smtlib b/tests-system/rbt-conditional-expression/output.smtlib new file mode 100644 index 00000000..dc4c8af6 --- /dev/null +++ b/tests-system/rbt-conditional-expression/output.smtlib @@ -0,0 +1,9 @@ +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: kitten +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation if +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: foobar evaluation elsif +T test_01 { + ^^^^^^^ rbt-conditional-expression/foo.trlc:3: check error: potato else +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 4 error(s) diff --git a/tests-system/rbt-conditional-expression/tracing b/tests-system/rbt-conditional-expression/tracing new file mode 100644 index 00000000..0744c3b8 --- /dev/null +++ b/tests-system/rbt-conditional-expression/tracing @@ -0,0 +1,2 @@ +LRM.Conditional_Expression_Evaluation +LRM.Conditional_Expression_Else diff --git a/trlc/ast.py b/trlc/ast.py index 080c1cd7..f35ab46f 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -480,6 +480,7 @@ def to_string(self): # pragma: no cover self.__class__.__name__ def ensure_type(self, mh, typ): + # lobster-trace: LRM.Conditional_Expression_Types assert isinstance(typ, (type, Type)) if self.typ is None: mh.error(self.location, @@ -1817,7 +1818,7 @@ def __init__(self, mh, t_kind, n_condition, n_expression): self.kind = t_kind.value self.n_cond = n_condition self.n_expr = n_expression - + # lobster-trace: LRM.Conditional_Expression_Types self.n_cond.ensure_type(mh, Builtin_Boolean) def dump(self, indent=0): # pragma: no cover @@ -1875,6 +1876,7 @@ def add_elsif(self, mh, n_action): self.actions.append(n_action) def set_else_part(self, mh, n_expr): + # lobster-trace: LRM.Conditional_Expression_Else assert isinstance(mh, Message_Handler) assert isinstance(n_expr, Expression) @@ -1897,6 +1899,7 @@ def to_string(self): return rv def evaluate(self, mh, context): + # lobster-trace: LRM.Conditional_Expression_Evaluation assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) diff --git a/trlc/parser.py b/trlc/parser.py index dfeb1226..08e54511 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -966,6 +966,7 @@ def parse_quantified_expression(self, scope): n_expr = n_expr) def parse_conditional_expression(self, scope): + # lobster-trace: LRM.Conditional_Expression assert isinstance(scope, ast.Scope) self.match_kw("if")