|
| 1 | +# pylint: disable=missing-docstring |
| 2 | + |
| 3 | +import unittest |
| 4 | +from typing import List |
| 5 | + |
| 6 | +from aas_core_codegen.common import Stripped, Identifier |
| 7 | +from aas_core_codegen.cpp.verification import _generate as cpp_verification_generate |
| 8 | +from aas_core_codegen.intermediate import type_inference as intermediate_type_inference |
| 9 | +from tests import common as tests_common |
| 10 | + |
| 11 | + |
| 12 | +class Test_against_recorded(unittest.TestCase): |
| 13 | + def test_optional_vector_in_invariant_not_deferenced(self) -> None: |
| 14 | + # NOTE (mristin): |
| 15 | + # This is a regression test where we check that an optional list without |
| 16 | + # implication is not de-referenced in the invariant's transpiled code. |
| 17 | + |
| 18 | + source = """\ |
| 19 | +class Item: |
| 20 | + value: str |
| 21 | + |
| 22 | + def __init__(self, value: str) -> None: |
| 23 | + self.value = value |
| 24 | +
|
| 25 | +@verification |
| 26 | +@implementation_specific |
| 27 | +def check_something(value: Optional[List[Item]]) -> bool: |
| 28 | + pass |
| 29 | +
|
| 30 | +@invariant( |
| 31 | + lambda self: |
| 32 | + check_something(self.value), |
| 33 | + "Some description" |
| 34 | +) |
| 35 | +class Something: |
| 36 | + value: Optional[List[Item]] |
| 37 | + |
| 38 | + def __init__(self, value: Optional[List[Item]] = None) -> None: |
| 39 | + self.value = value |
| 40 | + |
| 41 | +__version__ = "dummy" |
| 42 | +__xml_namespace__ = "https://dummy.com" |
| 43 | +""" |
| 44 | + |
| 45 | + symbol_table = tests_common.must_translate_source_to_intermediate(source=source) |
| 46 | + |
| 47 | + base_environment = intermediate_type_inference.populate_base_environment( |
| 48 | + symbol_table=symbol_table |
| 49 | + ) |
| 50 | + |
| 51 | + something_cls = symbol_table.must_find_concrete_class( |
| 52 | + name=Identifier("Something") |
| 53 | + ) |
| 54 | + |
| 55 | + environment = intermediate_type_inference.MutableEnvironment( |
| 56 | + parent=base_environment |
| 57 | + ) |
| 58 | + environment.set( |
| 59 | + identifier=Identifier("self"), |
| 60 | + type_annotation=intermediate_type_inference.OurTypeAnnotation( |
| 61 | + our_type=something_cls |
| 62 | + ), |
| 63 | + ) |
| 64 | + |
| 65 | + blocks = [] # type: List[Stripped] |
| 66 | + for invariant in something_cls.invariants: |
| 67 | + ( |
| 68 | + condition_expr, |
| 69 | + error, |
| 70 | + ) = cpp_verification_generate._transpile_class_invariant( |
| 71 | + invariant=invariant, symbol_table=symbol_table, environment=environment |
| 72 | + ) |
| 73 | + assert error is None, ( |
| 74 | + f"Unexpected generation error for an invariant: " |
| 75 | + f"{tests_common.most_underlying_messages(error)}" |
| 76 | + ) |
| 77 | + assert condition_expr is not None |
| 78 | + |
| 79 | + blocks.append(condition_expr) |
| 80 | + |
| 81 | + assert len(blocks) == 1, ( |
| 82 | + f"Expected only a single block for a single invariant " |
| 83 | + f"in the class {something_cls.name!r}" |
| 84 | + ) |
| 85 | + |
| 86 | + # NOTE (mristin): |
| 87 | + # The implementation of ``CheckSomething`` needs to deal with the optional |
| 88 | + # values. As soon as something is optional in C++, it will be provided to |
| 89 | + # the function as-is. This is intentional. |
| 90 | + self.assertEqual( |
| 91 | + """\ |
| 92 | +CheckSomething( |
| 93 | + instance_->value() |
| 94 | +)""", |
| 95 | + blocks[0], |
| 96 | + ) |
| 97 | + |
| 98 | + def test_optional_in_invariant_dereferenced_if_certainly_not_null( |
| 99 | + self, |
| 100 | + ) -> None: |
| 101 | + # NOTE (mristin): |
| 102 | + # This is a regression test where we check that an optional value is correctly |
| 103 | + # de-referenced in the invariant's transpiled code if type inference determines |
| 104 | + # that it is certainly not null. |
| 105 | + |
| 106 | + source = """\ |
| 107 | +class Item: |
| 108 | + value: str |
| 109 | +
|
| 110 | + def __init__(self, value: str) -> None: |
| 111 | + self.value = value |
| 112 | +
|
| 113 | +@verification |
| 114 | +@implementation_specific |
| 115 | +def check_something(value: Optional[List[Item]]) -> bool: |
| 116 | + pass |
| 117 | +
|
| 118 | +@invariant( |
| 119 | + lambda self: |
| 120 | + (self.value is None) or check_something(self.value), |
| 121 | + "Some description" |
| 122 | +) |
| 123 | +class Something: |
| 124 | + value: Optional[List[Item]] |
| 125 | +
|
| 126 | + def __init__(self, value: Optional[List[Item]] = None) -> None: |
| 127 | + self.value = value |
| 128 | +
|
| 129 | +__version__ = "dummy" |
| 130 | +__xml_namespace__ = "https://dummy.com" |
| 131 | +""" |
| 132 | + |
| 133 | + symbol_table = tests_common.must_translate_source_to_intermediate(source=source) |
| 134 | + |
| 135 | + base_environment = intermediate_type_inference.populate_base_environment( |
| 136 | + symbol_table=symbol_table |
| 137 | + ) |
| 138 | + |
| 139 | + something_cls = symbol_table.must_find_concrete_class( |
| 140 | + name=Identifier("Something") |
| 141 | + ) |
| 142 | + |
| 143 | + environment = intermediate_type_inference.MutableEnvironment( |
| 144 | + parent=base_environment |
| 145 | + ) |
| 146 | + environment.set( |
| 147 | + identifier=Identifier("self"), |
| 148 | + type_annotation=intermediate_type_inference.OurTypeAnnotation( |
| 149 | + our_type=something_cls |
| 150 | + ), |
| 151 | + ) |
| 152 | + |
| 153 | + blocks = [] # type: List[Stripped] |
| 154 | + for invariant in something_cls.invariants: |
| 155 | + ( |
| 156 | + condition_expr, |
| 157 | + error, |
| 158 | + ) = cpp_verification_generate._transpile_class_invariant( |
| 159 | + invariant=invariant, symbol_table=symbol_table, environment=environment |
| 160 | + ) |
| 161 | + assert error is None, ( |
| 162 | + f"Unexpected generation error for an invariant: " |
| 163 | + f"{tests_common.most_underlying_messages(error)}" |
| 164 | + ) |
| 165 | + assert condition_expr is not None |
| 166 | + |
| 167 | + blocks.append(condition_expr) |
| 168 | + |
| 169 | + assert len(blocks) == 1, ( |
| 170 | + f"Expected only a single block for a single invariant " |
| 171 | + f"in the class {something_cls.name!r}" |
| 172 | + ) |
| 173 | + |
| 174 | + # NOTE (mristin): |
| 175 | + # If we know that the value is not optional, we explicitly de-reference it. |
| 176 | + self.assertEqual( |
| 177 | + """\ |
| 178 | +( |
| 179 | + (!(instance_->value().has_value())) |
| 180 | + || CheckSomething( |
| 181 | + (*(instance_->value())) |
| 182 | + ) |
| 183 | +)""", |
| 184 | + blocks[0], |
| 185 | + ) |
| 186 | + |
| 187 | + |
| 188 | +if __name__ == "__main__": |
| 189 | + unittest.main() |
0 commit comments