From 549c2098fc0f066c9a5e42b013ff976fa96538ef Mon Sep 17 00:00:00 2001 From: Florian Schanda Date: Tue, 24 Oct 2023 10:40:35 +0200 Subject: [PATCH] Tracing/chapter 20 (#44) Co-authored-by: christophkloeffel --- tests-system/rbt-restricted-null-1/foo.rsl | 14 ++++++++++++++ tests-system/rbt-restricted-null-1/foo.trlc | 6 ++++++ tests-system/rbt-restricted-null-1/output | 5 +++++ .../rbt-restricted-null-1/output.brief | 1 + .../rbt-restricted-null-1/output.json | 3 +++ .../rbt-restricted-null-1/output.smtlib | 5 +++++ tests-system/rbt-restricted-null-1/tracing | 2 ++ tests-system/rbt-restricted-null-2/foo.rsl | 19 +++++++++++++++++++ tests-system/rbt-restricted-null-2/foo.trlc | 5 +++++ tests-system/rbt-restricted-null-2/output | 5 +++++ .../rbt-restricted-null-2/output.brief | 2 ++ .../rbt-restricted-null-2/output.json | 5 +++++ .../rbt-restricted-null-2/output.smtlib | 5 +++++ tests-system/rbt-restricted-null-2/tracing | 1 + trlc/ast.py | 13 ++++++++++++- trlc/parser.py | 1 + 16 files changed, 91 insertions(+), 1 deletion(-) create mode 100644 tests-system/rbt-restricted-null-1/foo.rsl create mode 100644 tests-system/rbt-restricted-null-1/foo.trlc create mode 100644 tests-system/rbt-restricted-null-1/output create mode 100644 tests-system/rbt-restricted-null-1/output.brief create mode 100644 tests-system/rbt-restricted-null-1/output.json create mode 100644 tests-system/rbt-restricted-null-1/output.smtlib create mode 100644 tests-system/rbt-restricted-null-1/tracing create mode 100644 tests-system/rbt-restricted-null-2/foo.rsl create mode 100644 tests-system/rbt-restricted-null-2/foo.trlc create mode 100644 tests-system/rbt-restricted-null-2/output create mode 100644 tests-system/rbt-restricted-null-2/output.brief create mode 100644 tests-system/rbt-restricted-null-2/output.json create mode 100644 tests-system/rbt-restricted-null-2/output.smtlib create mode 100644 tests-system/rbt-restricted-null-2/tracing diff --git a/tests-system/rbt-restricted-null-1/foo.rsl b/tests-system/rbt-restricted-null-1/foo.rsl new file mode 100644 index 00000000..d8545866 --- /dev/null +++ b/tests-system/rbt-restricted-null-1/foo.rsl @@ -0,0 +1,14 @@ +package Foo + +type T { + a optional Integer + b optional Integer + d optional Integer +} + +checks T { + a != null, "a is null", a + a == null, "a is not null", a + null == null, "null is not null" + d == null, "d is not null", d +} diff --git a/tests-system/rbt-restricted-null-1/foo.trlc b/tests-system/rbt-restricted-null-1/foo.trlc new file mode 100644 index 00000000..3eccf96e --- /dev/null +++ b/tests-system/rbt-restricted-null-1/foo.trlc @@ -0,0 +1,6 @@ +package Foo + +T Test { + a = 1 + b = 2 +} diff --git a/tests-system/rbt-restricted-null-1/output b/tests-system/rbt-restricted-null-1/output new file mode 100644 index 00000000..2c6caea1 --- /dev/null +++ b/tests-system/rbt-restricted-null-1/output @@ -0,0 +1,5 @@ +null == null, "null is not null" + ^^ rbt-restricted-null-1/foo.rsl:12: issue: expression is always true [vcg-always-true] +a = 1 + ^ rbt-restricted-null-1/foo.trlc:4: check error: a is not null +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/rbt-restricted-null-1/output.brief b/tests-system/rbt-restricted-null-1/output.brief new file mode 100644 index 00000000..7d865467 --- /dev/null +++ b/tests-system/rbt-restricted-null-1/output.brief @@ -0,0 +1 @@ +rbt-restricted-null-1/foo.trlc:4:9: trlc check error: a is not null diff --git a/tests-system/rbt-restricted-null-1/output.json b/tests-system/rbt-restricted-null-1/output.json new file mode 100644 index 00000000..1898d0f9 --- /dev/null +++ b/tests-system/rbt-restricted-null-1/output.json @@ -0,0 +1,3 @@ +a = 1 + ^ rbt-restricted-null-1/foo.trlc:4: check error: a is not null +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 error(s) diff --git a/tests-system/rbt-restricted-null-1/output.smtlib b/tests-system/rbt-restricted-null-1/output.smtlib new file mode 100644 index 00000000..2c6caea1 --- /dev/null +++ b/tests-system/rbt-restricted-null-1/output.smtlib @@ -0,0 +1,5 @@ +null == null, "null is not null" + ^^ rbt-restricted-null-1/foo.rsl:12: issue: expression is always true [vcg-always-true] +a = 1 + ^ rbt-restricted-null-1/foo.trlc:4: check error: a is not null +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 1 warning(s) and 1 error(s) diff --git a/tests-system/rbt-restricted-null-1/tracing b/tests-system/rbt-restricted-null-1/tracing new file mode 100644 index 00000000..63f05bf2 --- /dev/null +++ b/tests-system/rbt-restricted-null-1/tracing @@ -0,0 +1,2 @@ +LRM.Null_Equivalence +LRM.Unspecified_Optional_Components diff --git a/tests-system/rbt-restricted-null-2/foo.rsl b/tests-system/rbt-restricted-null-2/foo.rsl new file mode 100644 index 00000000..8ce485c8 --- /dev/null +++ b/tests-system/rbt-restricted-null-2/foo.rsl @@ -0,0 +1,19 @@ +package Foo + +type A { + a optional Integer + b optional Integer +} + +type T { + c optional Integer + d optional Integer +} + +checks A { + (a + b) > null, "(a+b) < null", a +} + +checks T { + d == (if c then null else d), "not permitted" +} diff --git a/tests-system/rbt-restricted-null-2/foo.trlc b/tests-system/rbt-restricted-null-2/foo.trlc new file mode 100644 index 00000000..a8181b4b --- /dev/null +++ b/tests-system/rbt-restricted-null-2/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Test { + c = 3 +} diff --git a/tests-system/rbt-restricted-null-2/output b/tests-system/rbt-restricted-null-2/output new file mode 100644 index 00000000..5ce8c4ec --- /dev/null +++ b/tests-system/rbt-restricted-null-2/output @@ -0,0 +1,5 @@ +(a + b) > null, "(a+b) < null", a + ^^^^ rbt-restricted-null-2/foo.rsl:14: error: null is not permitted here +d == (if c then null else d), "not permitted" + ^^^^ rbt-restricted-null-2/foo.rsl:18: error: null is not permitted here +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s) diff --git a/tests-system/rbt-restricted-null-2/output.brief b/tests-system/rbt-restricted-null-2/output.brief new file mode 100644 index 00000000..9cc291dc --- /dev/null +++ b/tests-system/rbt-restricted-null-2/output.brief @@ -0,0 +1,2 @@ +rbt-restricted-null-2/foo.rsl:14:15: trlc error: null is not permitted here +rbt-restricted-null-2/foo.rsl:18:21: trlc error: null is not permitted here diff --git a/tests-system/rbt-restricted-null-2/output.json b/tests-system/rbt-restricted-null-2/output.json new file mode 100644 index 00000000..5ce8c4ec --- /dev/null +++ b/tests-system/rbt-restricted-null-2/output.json @@ -0,0 +1,5 @@ +(a + b) > null, "(a+b) < null", a + ^^^^ rbt-restricted-null-2/foo.rsl:14: error: null is not permitted here +d == (if c then null else d), "not permitted" + ^^^^ rbt-restricted-null-2/foo.rsl:18: error: null is not permitted here +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s) diff --git a/tests-system/rbt-restricted-null-2/output.smtlib b/tests-system/rbt-restricted-null-2/output.smtlib new file mode 100644 index 00000000..5ce8c4ec --- /dev/null +++ b/tests-system/rbt-restricted-null-2/output.smtlib @@ -0,0 +1,5 @@ +(a + b) > null, "(a+b) < null", a + ^^^^ rbt-restricted-null-2/foo.rsl:14: error: null is not permitted here +d == (if c then null else d), "not permitted" + ^^^^ rbt-restricted-null-2/foo.rsl:18: error: null is not permitted here +Processed 1 model(s), 0 check(s) and 1 requirement file(s) and found 2 error(s) diff --git a/tests-system/rbt-restricted-null-2/tracing b/tests-system/rbt-restricted-null-2/tracing new file mode 100644 index 00000000..0e2082ea --- /dev/null +++ b/tests-system/rbt-restricted-null-2/tracing @@ -0,0 +1 @@ +LRM.Null_Is_Invalid diff --git a/trlc/ast.py b/trlc/ast.py index e815a213..a5f6dccc 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -487,6 +487,8 @@ def to_string(self): # pragma: no cover self.__class__.__name__ def ensure_type(self, mh, typ): + # lobster-trace: LRM.Restricted_Null + # lobster-trace: LRM.Null_Is_Invalid assert isinstance(typ, (type, Type)) if self.typ is None: mh.error(self.location, @@ -550,7 +552,7 @@ class Implicit_Null(Expression): """ def __init__(self, composite_object, composite_component): - # lobster-exclude: Constructor only declares variables + # lobster-trace: LRM.Unspecified_Optional_Components assert isinstance(composite_object, (Record_Object, Tuple_Aggregate)) assert isinstance(composite_component, Composite_Component) @@ -560,6 +562,7 @@ def to_string(self): return "null" def evaluate(self, mh, context): + # lobster-trace: LRM.Unspecified_Optional_Components assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) return Value(self.location, None, None) @@ -942,6 +945,7 @@ class Tuple_Aggregate(Expression): """ def __init__(self, location, typ): + # lobster-trace: LRM.Unspecified_Optional_Components super().__init__(location, typ) self.value = {n_field.name : Implicit_Null(self, n_field) for n_field in self.typ.components.values()} @@ -1223,6 +1227,7 @@ def dump(self, indent=0): # pragma: no cover self.n_operand.dump(indent + 1) def evaluate(self, mh, context): + # lobster-trace: LRM.Null_Is_Invalid assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) @@ -1457,6 +1462,8 @@ def to_string(self): assert False def evaluate(self, mh, context): + # lobster-trace: LRM.Null_Equivalence + # lobster-trace: LRM.Null_Is_Invalid assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) @@ -1758,6 +1765,7 @@ def dump(self, indent=0): # pragma: no cover self.n_upper.dump(indent + 1) def evaluate(self, mh, context): + # lobster-trace: LRM.Null_Is_Invalid assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) @@ -1911,6 +1919,7 @@ def to_string(self): def evaluate(self, mh, context): # lobster-trace: LRM.Conditional_Expression_Else # lobster-trace: LRM.Conditional_Expression_Evaluation + # lobster-trace: LRM.Null_Is_Invalid assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) @@ -1996,6 +2005,7 @@ def to_string(self): self.n_expr.to_string()) def evaluate(self, mh, context): + # lobster-trace: LRM.Null_Is_Invalid assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) @@ -2832,6 +2842,7 @@ class Record_Object(Typed_Entity): """ def __init__(self, name, location, n_typ, section, n_package): # lobster-trace: LRM.Section_Declaration + # lobster-trace: LRM.Unspecified_Optional_Components assert isinstance(n_typ, Record_Type) assert isinstance(section, Section) or section is None assert isinstance(n_package, Package) diff --git a/trlc/parser.py b/trlc/parser.py index 97508968..9316db50 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -967,6 +967,7 @@ def parse_quantified_expression(self, scope): def parse_conditional_expression(self, scope): # lobster-trace: LRM.Conditional_Expression + # lobster-trace: LRM.Restricted_Null assert isinstance(scope, ast.Scope) self.match_kw("if")