Add collectTypeRefs for TCore (#630)

*Description of changes:* This PR adds collectTypeRefs for TCore, which
fix the bug of unrecognized dependency between Box and Any.
Thanks @keyboardDrummer.

This PR replaces #618


By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

Author: thanhnguyen-aws

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. -/

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. -/

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)

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
 
 

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])