diff --git a/Strata/Languages/Laurel/DatatypeGrouping.lean b/Strata/Languages/Laurel/DatatypeGrouping.lean index 61686c6ca..a3fab9d29 100644 --- a/Strata/Languages/Laurel/DatatypeGrouping.lean +++ b/Strata/Languages/Laurel/DatatypeGrouping.lean @@ -31,6 +31,7 @@ def collectTypeRefs : HighTypeMd → List String collectTypeRefs base ++ args.flatMap collectTypeRefs | ⟨.Pure base, _⟩ => collectTypeRefs base | ⟨.Intersection ts, _⟩ => ts.flatMap collectTypeRefs + | ⟨.TCore name, _⟩ => [name] | _ => [] /-- Get all datatype names that a `DatatypeDefinition` references in its constructor args. -/ diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 5b3843f88..fe442a52a 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -255,6 +255,7 @@ def wrapFieldInAny (ty : HighType) (expr : StmtExprMd) : Except TranslationError | .TFloat64 => .ok <| mkStmtExprMd (.StaticCall "from_float" [expr]) | .TReal => .ok <| mkStmtExprMd (.StaticCall "from_float" [expr]) | .TString => .ok <| mkStmtExprMd (.StaticCall "from_string" [expr]) + | .TCore "Any" => .ok expr | other => .error (.typeError s!"wrapFieldInAny: no Any constructor for field type '{repr other}'") /-- Look up a field's HighType, returning `none` if the class or field is not found. -/ diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected new file mode 100644 index 000000000..64218f0a9 --- /dev/null +++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected @@ -0,0 +1,30 @@ + +==== Verification Results ==== +List_get_body_calls_List_get_0: ✅ pass +List_take_body_calls_List_take_0: ✅ pass +List_drop_body_calls_List_drop_0: ✅ pass +List_slice_body_calls_List_drop_0: ✅ pass +List_slice_body_calls_List_take_1: ✅ pass +List_set_body_calls_List_set_0: ✅ pass +DictStrAny_get_body_calls_DictStrAny_get_0: ✅ pass +Any_get_body_calls_DictStrAny_get_0: ✅ pass +Any_get_body_calls_List_get_1: ✅ pass +Any_get_body_calls_List_slice_2: ✅ pass +Any_get_body_calls_List_drop_3: ✅ pass +Any_get!_body_calls_DictStrAny_get_0: ✅ pass +Any_get!_body_calls_List_get_1: ✅ pass +Any_set_body_calls_List_set_0: ✅ pass +Any_set!_body_calls_List_set_0: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_0: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_1: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_2: ✅ pass +PFloorDiv_body_calls_Int.SafeDiv_3: ✅ pass +PAnd_body_calls_Any_to_bool_0: ✅ pass +POr_body_calls_Any_to_bool_0: ✅ pass +ret_type: ✅ pass (in prelude file) +ret_type: ✅ pass (in prelude file) +ret_pos: ✅ pass (in prelude file) +assert_name_is_foo: ✅ pass (in prelude file) +assert_opt_name_none_or_str: ✅ pass (in prelude file) +assert_opt_name_none_or_bar: ✅ pass (in prelude file) +ensures_maybe_except_none: ✅ pass (in prelude file) diff --git a/StrataTest/Languages/Python/run_py_analyze_sarif.py b/StrataTest/Languages/Python/run_py_analyze_sarif.py index 328c775bb..ce4048e0e 100755 --- a/StrataTest/Languages/Python/run_py_analyze_sarif.py +++ b/StrataTest/Languages/Python/run_py_analyze_sarif.py @@ -21,7 +21,7 @@ BOTH_SKIP = {"test_foo_client_folder", "test_invalid_client_type", "test_unsupported_config"} SKIP_TESTS = BOTH_SKIP | {"test_class_field_use", "test_list", "test_subscription", "test_with_statement", "test_class_field_init", "test_break_continue", "test_try_except", "test_try_except_scoping", "test_loops", - "test_augmented_assign", "test_list_slice"} # sarif pipeline uses PythonToCore which doesn't yet support AugAssign + "test_augmented_assign", "test_list_slice", "test_class_field_any"} # sarif pipeline uses PythonToCore which doesn't yet support AugAssign SKIP_TESTS_LAUREL = BOTH_SKIP diff --git a/StrataTest/Languages/Python/tests/test_class_field_any.py b/StrataTest/Languages/Python/tests/test_class_field_any.py new file mode 100644 index 000000000..48137b164 --- /dev/null +++ b/StrataTest/Languages/Python/tests/test_class_field_any.py @@ -0,0 +1,5 @@ +class MyClass: + def __init__(self, some_field): + self.some_field: Any = some_field + +c = MyClass([1,2])