diff --git a/rflx/specification/parser.py b/rflx/specification/parser.py index 1619ba79a..7315d4f59 100644 --- a/rflx/specification/parser.py +++ b/rflx/specification/parser.py @@ -142,7 +142,7 @@ def create_statement(statement: lang.Statement, filename: Path) -> stmt.Statemen return handlers[statement.kind_name](statement, filename) -def create_state(state: lang.State, filename: Path) -> model.State: +def create_state(state: lang.State, package: ID, filename: Path) -> model.State: location = node_location(state, filename) identifier = create_id(state.f_identifier, filename) if isinstance(state.f_body, lang.NullStateBody): @@ -170,7 +170,7 @@ def create_state(state: lang.State, filename: Path) -> model.State: actions.append(create_statement(a, filename)) declarations = [] for d in state.f_body.f_declarations: - declarations.append(create_declaration(d, filename)) + declarations.append(create_declaration(d, package, filename)) description = create_description(state.f_description) return model.State( identifier=identifier, @@ -206,9 +206,9 @@ def create_unproven_session( package * create_id(session.f_identifier, filename), create_id(session.f_aspects.f_initial, filename), create_id(session.f_aspects.f_final, filename), - [create_state(s, filename) for s in session.f_states], - [create_declaration(d, filename) for d in session.f_declarations], - [create_formal_declaration(p, filename) for p in session.f_parameters], + [create_state(s, package, filename) for s in session.f_states], + [create_declaration(d, package, filename) for d in session.f_declarations], + [create_formal_declaration(p, package, filename) for p in session.f_parameters], types or [], node_location(session, filename), ) @@ -496,7 +496,9 @@ def create_binding(expression: lang.Expr, filename: Path) -> expr.Expr: ) -def create_variable_decl(declaration: lang.LocalDecl, filename: Path) -> decl.BasicDeclaration: +def create_variable_decl( + declaration: lang.LocalDecl, package: ID, filename: Path +) -> decl.BasicDeclaration: assert isinstance(declaration, lang.VariableDecl) initializer = ( create_expression(declaration.f_initializer, filename) @@ -505,19 +507,21 @@ def create_variable_decl(declaration: lang.LocalDecl, filename: Path) -> decl.Ba ) return decl.VariableDeclaration( create_id(declaration.f_identifier, filename), - model.qualified_type_identifier(create_id(declaration.f_type_identifier, filename)), + model.qualified_type_identifier( + create_id(declaration.f_type_identifier, filename), package + ), initializer, location=node_location(declaration, filename), ) def create_private_type_decl( - declaration: lang.FormalDecl, filename: Path + declaration: lang.FormalDecl, package: ID, filename: Path ) -> decl.FormalDeclaration: assert isinstance(declaration, lang.FormalPrivateTypeDecl) return decl.TypeDeclaration( model.Private( - create_id(declaration.f_identifier, filename), + model.qualified_type_identifier(create_id(declaration.f_identifier, filename), package), location=node_location(declaration, filename), ) ) @@ -525,6 +529,7 @@ def create_private_type_decl( def create_channel_decl( declaration: lang.FormalDecl, + _package: ID, filename: Path, ) -> decl.FormalDeclaration: assert isinstance(declaration, lang.FormalChannelDecl) @@ -545,13 +550,17 @@ def create_channel_decl( ) -def create_renaming_decl(declaration: lang.LocalDecl, filename: Path) -> decl.BasicDeclaration: +def create_renaming_decl( + declaration: lang.LocalDecl, package: ID, filename: Path +) -> decl.BasicDeclaration: assert isinstance(declaration, lang.RenamingDecl) selected = create_expression(declaration.f_expression, filename) assert isinstance(selected, expr.Selected) return decl.RenamingDeclaration( create_id(declaration.f_identifier, filename), - model.qualified_type_identifier(create_id(declaration.f_type_identifier, filename), None), + model.qualified_type_identifier( + create_id(declaration.f_type_identifier, filename), package + ), selected, location=node_location(declaration, filename), ) @@ -559,6 +568,7 @@ def create_renaming_decl(declaration: lang.LocalDecl, filename: Path) -> decl.Ba def create_function_decl( declaration: lang.FormalDecl, + package: ID, filename: Path, ) -> decl.FormalDeclaration: assert isinstance(declaration, lang.FormalFunctionDecl) @@ -568,13 +578,17 @@ def create_function_decl( arguments.append( decl.Argument( create_id(p.f_identifier, filename), - model.qualified_type_identifier(create_id(p.f_type_identifier, filename)), + model.qualified_type_identifier( + create_id(p.f_type_identifier, filename), package + ), ) ) return decl.FunctionDeclaration( create_id(declaration.f_identifier, filename), arguments, - model.qualified_type_identifier(create_id(declaration.f_return_type_identifier, filename)), + model.qualified_type_identifier( + create_id(declaration.f_return_type_identifier, filename), package + ), location=node_location(declaration, filename), ) @@ -675,23 +689,25 @@ def create_expression(expression: lang.Expr, filename: Path) -> expr.Expr: return EXPRESSION_MAP[expression.kind_name](expression, filename) -def create_declaration(declaration: lang.LocalDecl, filename: Path) -> decl.BasicDeclaration: +def create_declaration( + declaration: lang.LocalDecl, package: ID, filename: Path +) -> decl.BasicDeclaration: handlers = { "VariableDecl": create_variable_decl, "RenamingDecl": create_renaming_decl, } - return handlers[declaration.kind_name](declaration, filename) + return handlers[declaration.kind_name](declaration, package, filename) def create_formal_declaration( - declaration: lang.FormalDecl, filename: Path + declaration: lang.FormalDecl, package: ID, filename: Path ) -> decl.FormalDeclaration: handlers = { "FormalChannelDecl": create_channel_decl, "FormalFunctionDecl": create_function_decl, "FormalPrivateTypeDecl": create_private_type_decl, } - return handlers[declaration.kind_name](declaration, filename) + return handlers[declaration.kind_name](declaration, package, filename) def create_math_expression(expression: lang.Expr, filename: Path) -> expr.Expr: diff --git a/tests/integration/parameterized_messages/generated/rflx-test-session.ads b/tests/integration/parameterized_messages/generated/rflx-test-session.ads index ed25e3419..608f57f90 100644 --- a/tests/integration/parameterized_messages/generated/rflx-test-session.ads +++ b/tests/integration/parameterized_messages/generated/rflx-test-session.ads @@ -110,10 +110,10 @@ private and not Test.Message.Has_Buffer (M_S_Ctx)); function Initialized return Boolean is - (Message.Has_Buffer (M_R_Ctx) + (Test.Message.Has_Buffer (M_R_Ctx) and then M_R_Ctx.Buffer_First = RFLX_Types.Index'First and then M_R_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095 - and then Message.Has_Buffer (M_S_Ctx) + and then Test.Message.Has_Buffer (M_S_Ctx) and then M_S_Ctx.Buffer_First = RFLX_Types.Index'First and then M_S_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095 and then Test.Session_Allocator.Global_Allocated); diff --git a/tests/integration/session_functions/generated/rflx-test-session.adb b/tests/integration/session_functions/generated/rflx-test-session.adb index 19d70a4d0..4ff7a9add 100644 --- a/tests/integration/session_functions/generated/rflx-test-session.adb +++ b/tests/integration/session_functions/generated/rflx-test-session.adb @@ -1,8 +1,10 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); pragma Warnings (Off, "redundant conversion"); with RFLX.Universal; +with RFLX.Test; use type RFLX.Universal.Message_Type; use type RFLX.Universal.Length; +use type RFLX.Test.Result; with RFLX.RFLX_Types; use type RFLX.RFLX_Types.Bit_Length; @@ -35,7 +37,7 @@ is Post => Initialized is - Valid : Boolean; + Valid : Test.Result; Message_Type : Universal.Option_Type; begin Get_Message_Type (Message_Type); @@ -51,7 +53,7 @@ is P_Next_State := S_Terminated; return; end if; - if not Valid then + if Valid = M_Valid then P_Next_State := S_Terminated; else P_Next_State := S_Reply; diff --git a/tests/integration/session_functions/generated/rflx-test-session.ads b/tests/integration/session_functions/generated/rflx-test-session.ads index 4608e092b..eb0204e9c 100644 --- a/tests/integration/session_functions/generated/rflx-test-session.ads +++ b/tests/integration/session_functions/generated/rflx-test-session.ads @@ -6,11 +6,12 @@ with RFLX.Universal; with RFLX.Universal.Message; with RFLX.Fixed_Size; with RFLX.Fixed_Size.Simple_Message; +with RFLX.Test; generic with procedure Get_Message_Type (Get_Message_Type : out RFLX.Universal.Option_Type); with procedure Create_Message (Create_Message : out RFLX.Fixed_Size.Simple_Message.Structure; Message_Type : RFLX.Universal.Option_Type; Data : RFLX_Types.Bytes); - with procedure Valid_Message (Valid_Message : out Boolean; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean); + with procedure Valid_Message (Valid_Message : out RFLX.Test.Result; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean); package RFLX.Test.Session with SPARK_Mode, Initial_Condition => diff --git a/tests/integration/session_functions/generated/rflx-test.ads b/tests/integration/session_functions/generated/rflx-test.ads index 5c577e81f..0bff88b69 100644 --- a/tests/integration/session_functions/generated/rflx-test.ads +++ b/tests/integration/session_functions/generated/rflx-test.ads @@ -5,4 +5,41 @@ package RFLX.Test with SPARK_Mode is + type Result_Base is mod 2**2; + + type Result is (M_Valid, M_Invalid) with + Size => + 2; + for Result use (M_Valid => 0, M_Invalid => 1); + + function Valid (Val : RFLX.Test.Result_Base) return Boolean is + ((case Val is + when 0 | 1 => + True, + when others => + False)); + + function To_Base (Enum : RFLX.Test.Result) return RFLX.Test.Result_Base is + ((case Enum is + when M_Valid => + 0, + when M_Invalid => + 1)); + + pragma Warnings (Off, "unreachable branch"); + + function To_Actual (Val : RFLX.Test.Result_Base) return RFLX.Test.Result is + ((case Val is + when 0 => + M_Valid, + when 1 => + M_Invalid, + when others => + raise Program_Error)) + with + Pre => + Valid (Val); + + pragma Warnings (On, "unreachable branch"); + end RFLX.Test; diff --git a/tests/integration/session_functions/src/func.adb b/tests/integration/session_functions/src/func.adb index d389c18d1..942952b8c 100644 --- a/tests/integration/session_functions/src/func.adb +++ b/tests/integration/session_functions/src/func.adb @@ -22,13 +22,15 @@ is end Create_Message; procedure Valid_Message - (Valid_Message : out Boolean; + (Valid_Message : out RFLX.Test.Result; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean) is use type RFLX.Universal.Option_Type; begin - Valid_Message := Strict and then Message_Type = (Known => True, Enum => RFLX.Universal.OT_Data); + Valid_Message := (if Strict and then Message_Type = (Known => True, Enum => RFLX.Universal.OT_Data) + then RFLX.Test.M_Invalid + else RFLX.Test.M_Valid); end Valid_Message; end Func; diff --git a/tests/integration/session_functions/src/func.ads b/tests/integration/session_functions/src/func.ads index 6a8469adb..c010a0dc7 100644 --- a/tests/integration/session_functions/src/func.ads +++ b/tests/integration/session_functions/src/func.ads @@ -1,6 +1,7 @@ pragma Style_Checks ("N3aAbcdefhiIklnOprStux"); with RFLX.RFLX_Types; +with RFLX.Test; with RFLX.Universal; with RFLX.Fixed_Size.Simple_Message; @@ -14,6 +15,6 @@ is procedure Create_Message (Result : out RFLX.Fixed_Size.Simple_Message.Structure; Message_Type : RFLX.Universal.Option_Type; Data : RFLX.RFLX_Types.Bytes); - procedure Valid_Message (Valid_Message : out Boolean; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean); + procedure Valid_Message (Valid_Message : out RFLX.Test.Result; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean); end Func; diff --git a/tests/integration/specification_model_test.py b/tests/integration/specification_model_test.py index fd2804586..cee8832e9 100644 --- a/tests/integration/specification_model_test.py +++ b/tests/integration/specification_model_test.py @@ -572,14 +572,14 @@ def test_consistency_specification_parsing_generation(tmp_path: Path) -> None: State("C"), ], [ - decl.VariableDeclaration("M", "Message"), + decl.VariableDeclaration("M", "Test::Message"), decl.VariableDeclaration("Y", BOOLEAN.identifier, expr.FALSE), ], [ decl.ChannelDeclaration("X", readable=True, writable=True), - decl.TypeDeclaration(Private("T")), - decl.FunctionDeclaration("F", [], "T"), - decl.FunctionDeclaration("G", [decl.Argument("P", "T")], BOOLEAN.identifier), + decl.TypeDeclaration(Private("Test::T")), + decl.FunctionDeclaration("F", [], "Test::T"), + decl.FunctionDeclaration("G", [decl.Argument("P", "Test::T")], BOOLEAN.identifier), ], [BOOLEAN, OPAQUE, tag, length, message], ) diff --git a/tests/unit/specification/grammar_test.py b/tests/unit/specification/grammar_test.py index 879981fe6..69a38343b 100644 --- a/tests/unit/specification/grammar_test.py +++ b/tests/unit/specification/grammar_test.py @@ -33,7 +33,7 @@ def parse_statement(data: str) -> stmt.Statement: def parse_declaration(data: str) -> decl.Declaration: parser_declaration, filename = parse(data, lang.GrammarRule.declaration_rule) assert isinstance(parser_declaration, lang.LocalDecl) - declaration = create_declaration(parser_declaration, filename) + declaration = create_declaration(parser_declaration, ID("Package"), filename) assert isinstance(declaration, decl.Declaration) return declaration @@ -41,7 +41,7 @@ def parse_declaration(data: str) -> decl.Declaration: def parse_formal_declaration(data: str) -> decl.Declaration: parser_declaration, filename = parse(data, lang.GrammarRule.session_parameter_rule) assert isinstance(parser_declaration, lang.FormalDecl) - declaration = create_formal_declaration(parser_declaration, filename) + declaration = create_formal_declaration(parser_declaration, ID("Package"), filename) assert isinstance(declaration, decl.Declaration) return declaration @@ -49,7 +49,7 @@ def parse_formal_declaration(data: str) -> decl.Declaration: def parse_state(data: str) -> State: parser_state, source = parse(data, lang.GrammarRule.state_rule) assert isinstance(parser_state, lang.State) - state = create_state(parser_state, source) + state = create_state(parser_state, ID("Package"), source) assert isinstance(state, State) return state @@ -562,7 +562,9 @@ def test_expression_complex(string: str, expected: expr.Expr) -> None: def test_private_type_declaration() -> None: string = "type X is private" - expected = decl.TypeDeclaration(model.Private("X", location=Location((1, 1), None, (1, 17)))) + expected = decl.TypeDeclaration( + model.Private("Package::X", location=Location((1, 1), None, (1, 17))) + ) actual = parse_formal_declaration(string) assert actual == expected assert actual.location @@ -588,10 +590,15 @@ def test_channel_declaration(string: str, expected: decl.Declaration) -> None: @pytest.mark.parametrize( "string,expected", [ - ("with function X return Y", decl.FunctionDeclaration("X", [], "Y")), + ("with function X return Y", decl.FunctionDeclaration("X", [], "Package::Y")), + ("with function X return Package::Y", decl.FunctionDeclaration("X", [], "Package::Y")), ( "with function X (A : B; C : D) return Y", - decl.FunctionDeclaration("X", [decl.Argument("A", "B"), decl.Argument("C", "D")], "Y"), + decl.FunctionDeclaration( + "X", + [decl.Argument("A", "Package::B"), decl.Argument("C", "Package::D")], + "Package::Y", + ), ), ( "with function X (A : Boolean) return Boolean", @@ -612,9 +619,9 @@ def test_formal_function_declaration(string: str, expected: decl.Declaration) -> @pytest.mark.parametrize( "string,expected", [ - ("A : B", decl.VariableDeclaration("A", "B")), - ("A : B := C", decl.VariableDeclaration("A", "B", expr.Variable("C"))), - ("A : B := 1", decl.VariableDeclaration("A", "B", expr.Number(1))), + ("A : B", decl.VariableDeclaration("A", "Package::B")), + ("A : B := C", decl.VariableDeclaration("A", "Package::B", expr.Variable("C"))), + ("A : B := 1", decl.VariableDeclaration("A", "Package::B", expr.Number(1))), ], ) def test_variable_declaration(string: str, expected: decl.Declaration) -> None: @@ -628,7 +635,7 @@ def test_variable_declaration(string: str, expected: decl.Declaration) -> None: [ ( "A : B renames C.D", - decl.RenamingDeclaration("A", "B", expr.Selected(expr.Variable("C"), "D")), + decl.RenamingDeclaration("A", "Package::B", expr.Selected(expr.Variable("C"), "D")), ), ], ) @@ -862,8 +869,8 @@ def test_state_error(string: str, error: str) -> None: [decl.VariableDeclaration("Y", "__BUILTINS__::Boolean", expr.Variable("True"))], [ decl.ChannelDeclaration("X", readable=True, writable=True), - decl.TypeDeclaration(model.Private("T")), - decl.FunctionDeclaration("F", [], "T"), + decl.TypeDeclaration(model.Private("Package::T")), + decl.FunctionDeclaration("F", [], "Package::T"), ], [], location=Location((2, 16), None, (23, 27)),